Verified linking lemma for secp256k1 64 bits scalar multiplication

mit-plv · May 27, 2024 · 1369d76 · 1369d76
1 parent d255ce2
commit 1369d76
Show file tree

Hide file tree

Showing 4 changed files with 114 additions and 94 deletions.
diff --git a/src/Bedrock/End2End/Secp256k1/Addchain.v b/src/Bedrock/End2End/Secp256k1/Addchain.v
@@ -1,5 +1,5 @@
 Require Import bedrock2.Array.
-Require Import bedrock2.FE310CSemantics.
+Require Import bedrock2.BasicC64Semantics.
 Require Import bedrock2.Loops.
 Require Import bedrock2.Map.Separation.
 Require Import bedrock2.Map.SeparationLogic.
@@ -18,7 +18,7 @@ Require Import coqutil.Byte.
 Require Import coqutil.Map.Interface.
 Require Import coqutil.Map.OfListWord.
 From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string.
-Require Import coqutil.Word.Bitwidth32.
+Require Import coqutil.Word.Bitwidth64.
 Require Import coqutil.Word.Bitwidth.
 Require Import coqutil.Word.Interface.
 Require Import Coq.Init.Byte.
@@ -165,7 +165,7 @@ Section WithParameters.
   Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
 
   Local Notation FElem := (FElem(FieldRepresentation:=frep256k1)).
-  Local Notation word := (Naive.word 32).
+  Local Notation word := (Naive.word 64).
   Local Notation felem := (felem(FieldRepresentation:=frep256k1)).
 
   Local Instance spec_of_secp256k1_square : spec_of "secp256k1_square" := Field.spec_of_UnOp un_square.
@@ -211,7 +211,7 @@ Section WithParameters.
     cbv [FElem];
     match goal with
     | H: _%sep ?m |- (Bignum.Bignum felem_size_in_words ?a _ * _)%sep ?m =>
-        seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 8 a) H
+        seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 4 a) H
     end;
     [> transitivity 32%nat; trivial | ];
     (* proves the memory matches up *)
@@ -244,7 +244,7 @@ Section WithParameters.
                 }) tr mem loc post.
   Proof.
     intros. repeat straightline.
-    pose (inv := fun (v: nat) (t: trace) (m: @map.rep word byte BasicC32Semantics.mem) (l: @map.rep string word locals) => t = tr /\
+    pose (inv := fun (v: nat) (t: trace) (m: @map.rep word byte _) (l: @map.rep string word locals) => t = tr /\
                           exists i (Hi: 1 <= i <= to),
                           v = Z.to_nat (to - i) /\
                           (exists vx, ((FElem pvar vx) * R)%sep m /\
@@ -386,5 +386,3 @@ Section WithParameters.
   Qed.
 
 End WithParameters.
-
-
diff --git a/src/Bedrock/End2End/Secp256k1/Field256k1.v b/src/Bedrock/End2End/Secp256k1/Field256k1.v
@@ -5,17 +5,16 @@ Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Bedrock.Field.Interface.Representation.
 Require Import Crypto.Bedrock.Field.Synthesis.New.ComputedOp.
 Require Import Crypto.Bedrock.Field.Synthesis.New.WordByWordMontgomery.
-Require Import Crypto.Bedrock.Field.Translation.Parameters.Defaults32.
+Require Import Crypto.Bedrock.Field.Translation.Parameters.Defaults64.
 Require Import Crypto.Bedrock.Specs.Field.
 Import ListNotations.
 
 (* Parameters for Secp256k1 field. *)
 Section Field.
-  Definition n : nat := 10.
   Definition m : Z := (2^256 - 2^32 - 977)%Z.
 
-  Existing Instances Bitwidth32.BW32
-    Defaults32.default_parameters Defaults32.default_parameters_ok.
+  Existing Instances Bitwidth64.BW64
+    Defaults64.default_parameters Defaults64.default_parameters_ok.
   Definition prefix : string := "secp256k1_"%string.
 
   (* Define Secp256k1 field *)
@@ -40,7 +39,7 @@ Section Field.
   (**** Translate each field operation into bedrock2 and apply bedrock2 backend
         field pipeline proofs to prove the bedrock2 functions are correct. ****)
 
-        Local Ltac begin_derive_bedrock2_func :=
+  Local Ltac begin_derive_bedrock2_func :=
         lazymatch goal with
         | |- context [spec_of_BinOp bin_mul] => eapply mul_func_correct
         | |- context [spec_of_UnOp un_square] => eapply square_func_correct
@@ -55,30 +54,30 @@ Section Field.
         | |- context [spec_of_UnOp un_to_mont] => eapply (to_mont_func_correct _ _ _ from_mont_string to_mont_string)
         end.
 
-        Ltac epair :=
-          lazymatch goal with
-          | f := _ : string * Syntax.func |- _ =>
-            let p := open_constr:((_, _)) in
-            unify f p;
-            subst f
-          end.
-
-        Ltac derive_bedrock2_func op :=
-        epair;
-        begin_derive_bedrock2_func;
-        (* this goal fills in the evar, so do it first for [abstract] to be happy *)
-        try lazymatch goal with
-            | |- _ = b2_func _ => vm_compute; reflexivity
-            end;
-        (* solve all the remaining goals *)
-        lazymatch goal with
-        | |- _ = @ErrorT.Success ?ErrT unit tt =>
-          abstract (vm_cast_no_check (@eq_refl _ (@ErrorT.Success ErrT unit tt)))
-        | |- Func.valid_func _ =>
-          eapply Func.valid_func_bool_iff;
-          abstract vm_cast_no_check (eq_refl true)
-        | |- (_ = _)%Z => vm_compute; reflexivity
-        end.
+  Ltac epair :=
+    lazymatch goal with
+    | f := _ : string * Syntax.func |- _ =>
+             let p := open_constr:((_, _)) in
+             unify f p;
+             subst f
+    end.
+
+  Ltac derive_bedrock2_func op :=
+    epair;
+    begin_derive_bedrock2_func;
+    (* this goal fills in the evar, so do it first for [abstract] to be happy *)
+    try lazymatch goal with
+      | |- _ = b2_func _ => vm_compute; reflexivity
+      end;
+    (* solve all the remaining goals *)
+    lazymatch goal with
+    | |- _ = @ErrorT.Success ?ErrT unit tt =>
+        abstract (vm_cast_no_check (@eq_refl _ (@ErrorT.Success ErrT unit tt)))
+    | |- Func.valid_func _ =>
+        eapply Func.valid_func_bool_iff;
+        abstract vm_cast_no_check (eq_refl true)
+    | |- (_ = _)%Z => vm_compute; reflexivity
+    end.
 
   Local Notation functions_contain functions f :=
     (Interface.map.get functions (fst f) = Some (snd f)).

diff --git a/src/Bedrock/End2End/Secp256k1/JacobianCoZ.v b/src/Bedrock/End2End/Secp256k1/JacobianCoZ.v
@@ -18,7 +18,7 @@ Require Import coqutil.Byte.
 Require Import coqutil.Map.Interface.
 Require Import coqutil.Map.OfListWord.
 From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string.
-Require Import coqutil.Word.Bitwidth32.
+Require Import coqutil.Word.Bitwidth64.
 Require Import coqutil.Word.Bitwidth.
 Require Import coqutil.Word.Interface.
 Require Import Coq.Init.Byte.
@@ -233,7 +233,7 @@ Definition secp256k1_zdau :=
     secp256k1_sub(Y2, T7, T5)     (* let t5 := t7 - t5 in *)
 }.
 
-Definition secp256k1_felem_cswap := CSwap.felem_cswap(word:=Naive.word32)(field_parameters:=field_parameters)(field_representaton:=frep256k1).
+Definition secp256k1_felem_cswap := CSwap.felem_cswap(word:=Naive.word64)(field_parameters:=field_parameters)(field_representaton:=frep256k1).
 
 (* Compute ToCString.c_func ("secp256k1_zaddu", secp256k1_zaddu). *)
 (* Compute ToCString.c_func ("secp256k1_felem_cswap", secp256k1_felem_cswap). *)
@@ -243,15 +243,15 @@ Section WithParameters.
   Context {char_ge_3 : (@Ring.char_ge (F M_pos) Logic.eq F.zero F.one F.opp F.add F.sub F.mul (BinNat.N.succ_pos BinNat.N.two))}.
   Context {field:@Algebra.Hierarchy.field (F M_pos) Logic.eq F.zero F.one F.opp F.add F.sub F.mul F.inv F.div}.
   Context {a b : F M_pos}.
-  Context {zero_a : a = F.zero}
-          {seven_b : b = F.of_Z _ 7}.
+  Context {zero_a : id a = F.zero}
+          {seven_b : id b = F.of_Z _ 7}.
 
   Local Coercion F.to_Z : F >-> Z.
   Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing).
   Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
 
   Local Notation FElem := (FElem(FieldRepresentation:=frep256k1)).
-  Local Notation word := (Naive.word 32).
+  Local Notation word := (Naive.word 64).
   Local Notation felem := (felem(FieldRepresentation:=frep256k1)).
   Local Notation point := (Jacobian.point(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fadd:=F.add)(Fmul:=F.mul)(a:=a)(b:=b)(Feq_dec:=F.eq_dec)).
   Local Notation co_z := (Jacobian.co_z(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fadd:=F.add)(Fmul:=F.mul)(a:=a)(b:=b)(Feq_dec:=F.eq_dec)).
@@ -510,7 +510,7 @@ Section WithParameters.
     cbv [FElem];
     match goal with
     | H: _%sep ?m |- (Bignum.Bignum felem_size_in_words ?a _ * _)%sep ?m =>
-        seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 8 a) H
+        seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 4 a) H
     end;
     [> transitivity 32%nat; trivial | ];
     (* proves the memory matches up *)
@@ -519,22 +519,6 @@ Section WithParameters.
   Local Ltac single_step :=
     repeat straightline; straightline_call; ssplit; try solve_mem; try solve_bounds; try solve_stack.
 
-  Local Ltac single_copy_step :=
-    repeat straightline; straightline_call; first (
-    match goal with
-    | H: context [array ptsto _ ?a _] |- context [FElem ?a _] =>
-        seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 8 a) H; [trivial|]
-    end;
-    multimatch goal with
-    | |- _ ?m1 =>
-        multimatch goal with
-        | H:_ ?m2
-          |- _ =>
-            syntactic_unify._syntactic_unify_deltavar m1 m2;
-            refine (Lift1Prop.subrelation_iff1_impl1 _ _ _ _ _ H); clear H
-        end
-    end; cancel; repeat ecancel_step; cancel_seps_at_indices 0%nat 0%nat; [reflexivity|]; solve [ecancel]).
-
   Lemma secp256k1_jopp_ok : program_logic_goal_for_function! secp256k1_jopp.
   Proof.
     Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds].
@@ -653,7 +637,7 @@ Section WithParameters.
 
     do 9 single_step.
     single_step.
-    seprewrite_in (Bignum.Bignum_of_bytes 8 a4) H72; [ trivial |  ];
+    seprewrite_in (Bignum.Bignum_of_bytes 4 a4) H72; [ trivial |  ];
     multimatch goal with
     | |- _ ?m1 =>
         multimatch goal with
@@ -684,7 +668,7 @@ Section WithParameters.
     1,2: cbv match beta delta [dblu proj1_sig fst snd].
     1,2: destruct P; cbv [proj1_sig] in H24.
     1,2: rewrite H24; cbv match zeta.
-    1,2: rewrite F.pow_2_r in *; subst a; repeat (apply pair_equal_spec; split); try congruence.
+    1,2: rewrite F.pow_2_r in *; cbv [id] in zero_a; subst a; repeat (apply pair_equal_spec; split); try congruence.
     1,2,3: repeat match goal with
                   | H: feval ?x = _ |- context [feval ?x] => rewrite H
                   end; ring.
@@ -696,13 +680,12 @@ Section WithParameters.
   Proof.
     Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds].
 
-    clear zero_a seven_b.
     repeat straightline.
     eapply Proper_call; cycle -1; [eapply H|try eabstract (solve [ Morphisms.solve_proper ])..]; [ .. | intros ? ? ? ? ].
     ssplit; [eexists; eassumption|..]; try eassumption.
     repeat match goal with
     | H: context [array ptsto _ ?a _] |- context [FElem ?a _] =>
-        seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 8 a) H; [trivial|]
+        seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 4 a) H; [trivial|]
     end.
     multimatch goal with
     | |- _ ?m1 =>