Added Dettman CLI things.

Changed implementation of value_at_weight function in Core.v to make it reifiable.
Added stuff in Makefile.examples to generate dettman mul functions - renamed already-existing secp256k1 generated files to clarify that they're montgomery implementations, as opposed to the dettman secp256k1 functions that we now have as well.

Makefile.config

@@ -50,7 +50,7 @@ else
 if_SKIP_BEDROCK2 = $(1)
 endif
 
-BASE_STANDALONE := unsaturated_solinas saturated_solinas word_by_word_montgomery base_conversion solinas_reduction
+BASE_STANDALONE := unsaturated_solinas saturated_solinas dettman_multiplication word_by_word_montgomery base_conversion solinas_reduction
 BEDROCK2_STANDALONE := $(addprefix bedrock2_,$(BASE_STANDALONE)) $(addprefix with_bedrock2_,$(BASE_STANDALONE))
 STANDALONE := $(BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_STANDALONE) $(WITH_BEDROCK2_STANDALONE))
 PERF_STANDALONE := perf_unsaturated_solinas perf_word_by_word_montgomery

Makefile.examples

@@ -88,8 +88,10 @@ UNSATURATED_SOLINAS_FUNCTIONS := carry_mul carry_square carry add sub opp select
 FUNCTIONS_FOR_25519 := $(UNSATURATED_SOLINAS_FUNCTIONS) carry_scmul121666
 WORD_BY_WORD_MONTGOMERY_FUNCTIONS := mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp
 SOLINAS_REDUCTION_FUNCTIONS := mul square
+DETTMAN_MULTIPLICATION_FUNCTIONS := mul
 UNSATURATED_SOLINAS := src/ExtractionOCaml/unsaturated_solinas
 WORD_BY_WORD_MONTGOMERY := src/ExtractionOCaml/word_by_word_montgomery
+DETTMAN_MULTIPLICATION := src/ExtractionOCaml/dettman_multiplication
 SOLINAS_REDUCTION := src/ExtractionOCaml/solinas_reduction
 
 UNSATURATED_SOLINAS_BASE_FILES := # p224_solinas_64
@@ -110,15 +112,17 @@ $(eval $(call add_curve_keys,p521_64,UNSATURATED_SOLINAS,'p521',64,'9' '2^521 -
 $(eval $(call add_curve_keys,p448_solinas_64,UNSATURATED_SOLINAS,'p448',64,'8' '2^448 - 2^224 - 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
 $(eval $(call add_curve_keys,p448_solinas_32,UNSATURATED_SOLINAS,'p448',32,'16' '2^448 - 2^224 - 1',$(UNSATURATED_SOLINAS_FUNCTIONS),UNSATURATED_SOLINAS))
 $(foreach bw,64 32,$(eval $(call add_curve_keys,p256_$(bw),WORD_BY_WORD_MONTGOMERY,'p256',$(bw),'2^256 - 2^224 + 2^192 + 2^96 - 1',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
-$(foreach bw,64 32,$(eval $(call add_curve_keys,secp256k1_$(bw),WORD_BY_WORD_MONTGOMERY,'secp256k1',$(bw),'2^256 - 2^32 - 977',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
+$(foreach bw,64 32,$(eval $(call add_curve_keys,secp256k1_montgomery_$(bw),WORD_BY_WORD_MONTGOMERY,'secp256k1_montgomery',$(bw),'2^256 - 2^32 - 977',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
 $(foreach bw,64 32,$(eval $(call add_curve_keys,p384_$(bw),WORD_BY_WORD_MONTGOMERY,'p384',$(bw),'2^384 - 2^128 - 2^96 + 2^32 - 1',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
 $(foreach bw,64 32,$(eval $(call add_curve_keys,p224_$(bw),WORD_BY_WORD_MONTGOMERY,'p224',$(bw),'2^224 - 2^96 + 1',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
 $(foreach bw,64,$(eval $(call add_curve_keys,p434_$(bw),WORD_BY_WORD_MONTGOMERY,'p434',$(bw),'2^216 * 3^137 - 1',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY))) # 32 is a bit too heavy
 
 $(foreach bw,64 32,$(eval $(call add_curve_keys,curve25519_scalar_$(bw),WORD_BY_WORD_MONTGOMERY,'25519_scalar',$(bw),'2^252 + 27742317777372353535851937790883648493',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
 $(foreach bw,64 32,$(eval $(call add_curve_keys,p256_scalar_$(bw),WORD_BY_WORD_MONTGOMERY,'p256_scalar',$(bw),'2^256 - 2^224 + 2^192 - 89188191075325690597107910205041859247',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
 $(foreach bw,64 32,$(eval $(call add_curve_keys,p384_scalar_$(bw),WORD_BY_WORD_MONTGOMERY,'p384_scalar',$(bw),'2^384 - 1388124618062372383947042015309946732620727252194336364173',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
-$(foreach bw,64 32,$(eval $(call add_curve_keys,secp256k1_scalar_$(bw),WORD_BY_WORD_MONTGOMERY,'secp256k1_scalar',$(bw),'2^256 - 432420386565659656852420866394968145599',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
+$(foreach bw,64 32,$(eval $(call add_curve_keys,secp256k1_montgomery_scalar_$(bw),WORD_BY_WORD_MONTGOMERY,'secp256k1_montgomery_scalar',$(bw),'2^256 - 432420386565659656852420866394968145599',$(WORD_BY_WORD_MONTGOMERY_FUNCTIONS),WORD_BY_WORD_MONTGOMERY)))
+
+$(foreach bw,64,$(eval $(call add_curve_keys,secp256k1_dettman_$(bw),DETTMAN_MULTIPLICATION,'secp256k1_dettman',$(bw),5 52 '2^256 - 4294968273' 1,$(DETTMAN_MULTIPLICATION_FUNCTIONS),DETTMAN_MULTIPLICATION)))
 
 $(foreach bw,64,$(eval $(call add_curve_keys,curve25519_solinas_$(bw),SOLINAS_REDUCTION,'curve25519_solinas',$(bw),'2^255 - 19',$(SOLINAS_REDUCTION_FUNCTIONS),SOLINAS_REDUCTION)))
 
@@ -147,6 +151,7 @@ LITE_ZIG_FILES := $(patsubst %,$(ZIG_DIR)%.zig,$(LITE_BASE_FILES))
 
 BEDROCK2_UNSATURATED_SOLINAS := src/ExtractionOCaml/bedrock2_unsaturated_solinas
 BEDROCK2_WORD_BY_WORD_MONTGOMERY := src/ExtractionOCaml/bedrock2_word_by_word_montgomery
+BEDROCK2_DETTMAN_MULTIPLICATION := src/ExtractionOCaml/bedrock2_dettman_multiplication
 BEDROCK2_SOLINAS_REDUCTION := src/ExtractionOCaml/bedrock2_solinas_reduction
 
 C_EXTRA_ARGS := --inline --static --use-value-barrier

src/Arithmetic/Core.v

@@ -528,23 +528,23 @@ Module Associational.
   Qed.
 
   Definition value_at_weight (a : list (Z * Z)) (d : Z) :=
-    fold_right Z.add 0 (map snd (filter (fun p => fst p =? d) a)).
+    fold_right (fun p sum => if (d =? fst p) then (sum + snd p) else sum) 0 a.
 
-  Lemma value_at_weight_works a d : d * (value_at_weight a d) = Associational.eval (filter (fun p => fst p =? d) a).
+  Lemma value_at_weight_works a d : d * (value_at_weight a d) = Associational.eval (filter (fun p => d =? fst p) a).
   Proof.
     induction a as [| a0 a' IHa'].
-    - cbv [Associational.eval value_at_weight]. simpl. lia.
-    - cbv [value_at_weight]. simpl. destruct (fst a0 =? d) eqn:E.
-      + rewrite Associational.eval_cons. simpl. rewrite <- IHa'. cbv [value_at_weight]. lia.
+    - cbv [Associational.eval]. simpl. lia.
+    - simpl. destruct (d =? fst a0) eqn:E.
+      + rewrite Associational.eval_cons. rewrite <- IHa'. apply Z.eqb_eq in E. rewrite E. lia.
       + apply IHa'.
   Qed.
 
-  Lemma not_in_value_0 a d : ~ In d (map fst a) -> value_at_weight a d = 0.
+ Lemma not_in_value_0 a d : ~ In d (map fst a) -> value_at_weight a d = 0.
   Proof.
     intros H. induction a as [| x a' IHa'].
     - reflexivity.
-    - cbv [value_at_weight]. simpl. destruct (fst x =? d) eqn:E.
-      + exfalso. apply H. simpl. lia.
+    - simpl. destruct (d =? fst x) eqn:E.
+      + exfalso. apply H. simpl. left. apply Z.eqb_eq in E. symmetry. apply E.
       + apply IHa'. intros H'. apply H. simpl. right. apply H'.
   Qed.
 
@@ -556,7 +556,7 @@ Module Associational.
   forall d, In d l ->
   (fun d : Z => (d, value_at_weight (a0 :: a') d)) d = (fun d => (d, value_at_weight a' d)) d.
   Proof.
-    intros H d H'. simpl. f_equal. cbv [value_at_weight]. simpl. destruct (fst a0 =? d) eqn:E.
+    intros H d H'. simpl. f_equal. cbv [value_at_weight]. destruct (d =? fst a0) eqn:E.
     - exfalso. rewrite Z.eqb_eq in E. subst. apply (H H').
     - reflexivity.
   Qed.
@@ -565,15 +565,16 @@ Module Associational.
   Proof.
     induction a as [| a0 a' IHa'].
     - reflexivity.
-    - cbv [dedup_weights]. simpl. destruct (existsb (Z.eqb (fst a0)) (nodupb Z.eqb (map fst a'))) eqn:E.
+    - cbv [dedup_weights]. remember (value_at_weight (a0 :: a')) as x eqn:Ex.
+      simpl. destruct (existsb (Z.eqb (fst a0)) (nodupb Z.eqb (map fst a'))) eqn:E.
       + apply (existsb_eqb_true_iff Z.eqb Z.eqb_eq) in E. rewrite <- (nodupb_in_iff Z.eqb Z.eqb_eq) in E.
         apply (nodupb_split Z.eqb Z.eqb_eq) in E. destruct E as [l1 [l2 [H1 [H2 H3] ] ] ]. rewrite H1.
-        repeat rewrite map_app. rewrite (map_ext_in _ _ l1 (funs_same l1 a0 a' H2)).
+        repeat rewrite map_app. rewrite Ex; clear Ex x. rewrite (map_ext_in _ _ l1 (funs_same l1 a0 a' H2)).
         rewrite (map_ext_in _ _ l2 (funs_same l2 a0 a' H3)). repeat rewrite Associational.eval_app. simpl.
         repeat rewrite Associational.eval_cons. simpl. rewrite <- IHa'. simpl. rewrite Associational.eval_nil. 
         cbv [dedup_weights]. rewrite H1. repeat rewrite map_app. repeat rewrite Associational.eval_app.
-        cbv [value_at_weight]. simpl. rewrite Z.eqb_refl. simpl. cbv [Associational.eval]. simpl. lia.
-      + simpl. apply (existsb_eqb_false_iff Z.eqb Z.eqb_eq) in E. rewrite (map_ext_in _ _ _ (funs_same _ _ _ E)).
+        cbv [value_at_weight]. rewrite Z.eqb_refl. simpl. cbv [Associational.eval]. simpl. lia.
+      + simpl. apply (existsb_eqb_false_iff Z.eqb Z.eqb_eq) in E. rewrite Ex; clear x Ex. rewrite (map_ext_in _ _ _ (funs_same _ _ _ E)).
         repeat rewrite Associational.eval_cons. simpl. rewrite <- IHa'. cbv [dedup_weights]. f_equal. f_equal.
         rewrite <- (nodupb_in_iff Z.eqb Z.eqb_eq) in E. cbv [value_at_weight]. simpl. rewrite Z.eqb_refl.
         apply not_in_value_0 in E. cbv [value_at_weight] in E. simpl. rewrite E. lia.

src/Bedrock/Standalone/StandaloneHaskellMain.v

@@ -29,6 +29,11 @@ Module Bedrock2First.
       := main_gen ForExtraction.SaturatedSolinas.PipelineMain.
   End SaturatedSolinas.
 
+  Module DettmanMultiplication.
+    Definition main : IO_unit
+      := main_gen ForExtraction.DettmanMultiplication.PipelineMain.
+  End DettmanMultiplication.
+
   Module SolinasReduction.
     Definition main : IO_unit
       := main_gen ForExtraction.SolinasReduction.PipelineMain.
@@ -63,6 +68,11 @@ Module Bedrock2Later.
       := main_gen ForExtraction.SaturatedSolinas.PipelineMain.
   End SaturatedSolinas.
 
+  Module DettmanMultiplication.
+    Definition main : IO_unit
+      := main_gen ForExtraction.DettmanMultiplication.PipelineMain.
+  End DettmanMultiplication.
+
   Module SolinasReduction.
     Definition main : IO_unit
       := main_gen ForExtraction.SolinasReduction.PipelineMain.

src/Bedrock/Standalone/StandaloneOCamlMain.v

@@ -32,6 +32,11 @@ Module Bedrock2First.
       := main_gen ForExtraction.SaturatedSolinas.PipelineMain.
   End SaturatedSolinas.
 
+  Module DettmanMultiplication.
+    Definition main : unit
+      := main_gen ForExtraction.DettmanMultiplication.PipelineMain.
+  End DettmanMultiplication.
+
   Module SolinasReduction.
     Definition main : unit
       := main_gen ForExtraction.SolinasReduction.PipelineMain.
@@ -66,6 +71,11 @@ Module Bedrock2Later.
       := main_gen ForExtraction.SaturatedSolinas.PipelineMain.
   End SaturatedSolinas.
 
+  Module DettmanMultiplication.
+    Definition main : unit
+      := main_gen ForExtraction.SaturatedSolinas.PipelineMain.
+  End DettmanMultiplication.
+
   Module SolinasReduction.
     Definition main : unit
       := main_gen ForExtraction.SolinasReduction.PipelineMain.

src/CLI.v

@@ -25,6 +25,7 @@ Require Crypto.PushButtonSynthesis.SaturatedSolinas.
 Require Crypto.PushButtonSynthesis.UnsaturatedSolinas.
 Require Crypto.PushButtonSynthesis.WordByWordMontgomery.
 Require Crypto.PushButtonSynthesis.BaseConversion.
+Require Crypto.PushButtonSynthesis.DettmanMultiplication.
 Require Crypto.PushButtonSynthesis.SolinasReduction.
 Require Import Crypto.UnsaturatedSolinasHeuristics.
 Require Import Crypto.Stringification.Language.
@@ -95,7 +96,16 @@ Module ForExtraction.
                  option_map Auto numv
             else None
        end.
+
+  Definition parse_n_nat (s : string) : option nat
+    := parse_nat s.
 
+  Definition parse_nat_limbwidth (s : string) : option nat
+    := parse_nat s.
+
+  Definition parse_input_magnitude (s : string) : option nat
+    := parse_nat s.
+
   Definition parse_sc (s : string) : option (Z * list (Z * Z))
     := parseZ_arith_to_taps s.
 
@@ -393,7 +403,21 @@ Module ForExtraction.
   Definition n_spec : anon_argT
     := ("n",
         Arg.Custom (parse_string_and parse_n) "an ℕ or the literal '(auto)' or '(autoN)' for a non-negative number N",
-        ["The number of limbs, or the literal '(auto)' or '(autoN)' for a non-negative number N, to automatically guess the number of limbs"]).
+         ["The number of limbs, or the literal '(auto)' or '(autoN)' for a non-negative number N, to automatically guess the number of limbs"]).
+  Definition n_nat_spec : anon_argT
+    := ("n",
+        Arg.Custom (parse_string_and parse_nat) "ℕ",
+        ["The number of limbs"]).
+  Definition limbwidth_spec : anon_argT
+    := ("limbwidth",
+        Arg.Custom (parse_string_and parse_nat) "ℕ",
+        ["The limb width"]).
+  Definition input_magnitude_spec : anon_argT
+    := ("input_magnitude",
+        Arg.Custom (parse_string_and parse_input_magnitude) "ℕ",
+        ["This number determines the input bounds to the dettman multiplication function.  If the input magnitude is M, the limbwidth argument (which determines the width of all limbs except the most significant limb) has a value a, and the most significant limb has a limbwidth b, then the input bounds are as follows: 
+          - 2*M*(2^b-1) is the max (inclusive) of the most significant limb
+          - 2*M*(2^a-1) is the max (inclusive) of the remaining limbs"]).
   Definition sc_spec : anon_argT
     := ("s-c",
         Arg.Custom (parse_string_and parse_sc) "an integer expression",
@@ -1177,6 +1201,45 @@ Module ForExtraction.
       := Parameterized.PipelineMain argv.
   End SaturatedSolinas.
 
+  Module DettmanMultiplication.
+    Local Instance api : PipelineAPI
+      := {
+          spec :=
+            {| Arg.named_args := []
+               ; Arg.anon_args := [n_nat_spec; limbwidth_spec; sc_spec; input_magnitude_spec]
+               ; Arg.anon_opt_args := []
+               ; Arg.anon_opt_repeated_arg := Some (function_to_synthesize_spec DettmanMultiplication.valid_names) |};
+
+          parse_args opts args
+          := let '(tt, ((str_n, n), (str_limbwidth, limbwidth), (str_sc, (s, c)), (str_input_magnitude, input_magnitude)),
+                   tt, requests) := args in
+             let show_requests := match requests with nil => "(all)" | _ => String.concat ", " requests end in
+             inl ((str_n, str_limbwidth, str_sc, str_input_magnitude, show_requests),
+                  (n, limbwidth, s, c, input_magnitude, requests));
+
+          show_lines_args :=
+            fun '((str_n, str_limbwidth, str_sc, str_input_magnitude, show_requests),
+                  (n, limbwidth, s, c, input_magnitude, requests))
+            => ["requested operations: " ++ show_requests;
+                "n = " ++ show n ++ " (from """ ++ str_n ++ """)";
+                "limbwidth = " ++ show limbwidth ++ " (from """ ++ str_limbwidth ++ """)";
+                "s-c = " ++ PowersOfTwo.show_Z s ++ " - " ++ show_c c ++ " (from """ ++ str_sc ++ """)";
+                "input magnitude: " ++ show input_magnitude ++ " (from """ ++ str_input_magnitude ++ """)"];
+
+          Synthesize
+          := fun _ opts '(n, limbwidth, s, c, input_magnitude, requests) comment_header prefix
+             => DettmanMultiplication.Synthesize machine_wordsize s c n limbwidth input_magnitude comment_header prefix requests
+        }.
+
+    Definition PipelineMain
+               {supported_languages : supported_languagesT}
+               {A}
+               {io_driver : IODriverAPI A}
+               (argv : list string)
+      : A
+      := Parameterized.PipelineMain argv.
+  End DettmanMultiplication.
+
   Module SolinasReduction.
     Local Instance api : PipelineAPI
       := {

src/COperationSpecifications.v

@@ -494,6 +494,27 @@ Module SaturatedSolinas.
   End __.
 End SaturatedSolinas.
 
+Module DettmanMultiplication.
+  Section __.
+    Context (wt : nat -> Z)
+            (n : nat)
+            (m : Z)
+            (input_bounds : list (option zrange))
+            (output_bounds : list (option zrange))
+            (length_input_bounds : length input_bounds = n)
+            (length_output_bounds : length output_bounds = n).
+    Local Notation eval := (Positional.eval wt n).
+
+    Definition mul_correct
+               (mul : list Z -> list Z -> list Z)
+      := forall x y,
+        list_Z_bounded_by input_bounds x
+        -> list_Z_bounded_by input_bounds y
+        -> eval (mul x y) mod m = ((eval x) * (eval y)) mod m
+           /\ list_Z_bounded_by output_bounds (mul x y).
+  End __.
+End DettmanMultiplication.
+
 Module SolinasReduction.
   Section __.
     Context (wt : nat -> Z)

src/ExtractionHaskell/bedrock2_dettman_multiplication.v

@@ -0,0 +1,5 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2First.
+
+(*Redirect "/tmp/bedrock2_dettman_multiplication.hs"*) Recursive Extraction DettmanMultiplication.main.
+(* cat /tmp/bedrock2_dettman_multiplication.hs.out | sed -f haskell.sed  > ../../bedrock2_dettman_multiplication.hs *)

src/ExtractionHaskell/dettman_multiplication.v

@@ -0,0 +1,4 @@
+Require Import Crypto.StandaloneHaskellMain.
+
+(*Redirect "/tmp/dettman_multiplication.hs"*) Recursive Extraction DettmanMultiplication.main.
+(* cat /tmp/dettman_multiplication.hs.out | sed -f haskell.sed  > ../../dettman_multiplication.hs *)

src/ExtractionHaskell/with_bedrock2_dettman_multiplication.v

@@ -0,0 +1,5 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain.
+Import Bedrock2Later.
+
+(*Redirect "/tmp/bedrock2_dettman_multiplication.hs"*) Recursive Extraction DettmanMultiplication.main.
+(* cat /tmp/bedrock2_dettman_multiplication.hs.out | sed -f haskell.sed  > ../../bedrock2_dettman_multiplication.hs *)

src/ExtractionOCaml/bedrock2_dettman_multiplication.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2First.
+
+Extraction "src/ExtractionOCaml/bedrock2_dettman_multiplication.tmp" DettmanMultiplication.main.

src/ExtractionOCaml/dettman_multiplication.v

@@ -0,0 +1,3 @@
+Require Import Crypto.StandaloneOCamlMain.
+
+Extraction "src/ExtractionOCaml/dettman_multiplication.tmp" DettmanMultiplication.main.

src/ExtractionOCaml/with_bedrock2_dettman_multiplication.v

@@ -0,0 +1,4 @@
+Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain.
+Import Bedrock2Later.
+
+Extraction "src/ExtractionOCaml/with_bedrock2_dettman_multiplication.tmp" DettmanMultiplication.main.