From 1369d76d8038e859b265da49dff9032ddc994a71 Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Mon, 27 May 2024 11:15:11 +0200 Subject: [PATCH] Verified linking lemma for secp256k1 64 bits scalar multiplication --- src/Bedrock/End2End/Secp256k1/Addchain.v | 12 +-- src/Bedrock/End2End/Secp256k1/Field256k1.v | 57 ++++++----- src/Bedrock/End2End/Secp256k1/JacobianCoZ.v | 35 ++----- src/Bedrock/End2End/Secp256k1/JoyeLadder.v | 104 ++++++++++++++------ 4 files changed, 114 insertions(+), 94 deletions(-) diff --git a/src/Bedrock/End2End/Secp256k1/Addchain.v b/src/Bedrock/End2End/Secp256k1/Addchain.v index 9fe442abb5..67729db445 100644 --- 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 index 86925cb2ce..f2055c0273 100644 --- 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 index b4a0db1ec0..f02a138dc3 100644 --- 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 => diff --git a/src/Bedrock/End2End/Secp256k1/JoyeLadder.v b/src/Bedrock/End2End/Secp256k1/JoyeLadder.v index 9259b7cc74..cc15f56be6 100644 --- a/src/Bedrock/End2End/Secp256k1/JoyeLadder.v +++ b/src/Bedrock/End2End/Secp256k1/JoyeLadder.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. @@ -107,7 +107,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 Notation Wpoint := (WeierstrassCurve.W.point(F:=F M_pos)(Feq:=Logic.eq)(Fadd:=F.add)(Fmul:=F.mul)(a:=a)(b:=b)). Local Notation Wzero := (WeierstrassCurve.W.zero(F:=F M_pos)(Feq:=Logic.eq)(Fadd:=F.add)(Fmul:=F.mul)(a:=a)(b:=b)). @@ -154,7 +154,7 @@ Section WithParameters. (* Rewrites the `stack$@a` term in H to use a Bignum instead *) 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 *) @@ -200,7 +200,7 @@ Section WithParameters. (kbytes$@kptr * R)%sep mem -> LittleEndianList.le_combine kbytes = k -> wi = word.of_Z i -> - (0 <= i < 2 ^ 32)%Z -> + (0 <= i < 2 ^ 64)%Z -> (i < 8 * Z.of_nat (List.length kbytes)) -> (forall tr' mem' loc', @@ -388,7 +388,7 @@ Section WithParameters. let swap := b in let i := Z.succ i in (R1R0, swap, i)):(co_z_points*bool*BinInt.Z)->(co_z_points*bool*BinInt.Z)). - pose (inv := fun (v: nat) (t: trace) (m: @map.rep word byte BasicC32Semantics.mem) (l: @map.rep string word locals) => + pose (inv := fun (v: nat) (t: trace) (m: @map.rep word byte _) (l: @map.rep string word locals) => t = tr /\ exists i (Hi: 2 <= i <= scalarbitsz), v = Z.to_nat (scalarbitsz - i) /\ @@ -423,7 +423,7 @@ Section WithParameters. fold iter_res in Hiter. rewrite (surjective_pairing iter_res) in Hiter. rewrite (surjective_pairing (fst iter_res)) in Hiter. destruct Hiter as (Hvi' & loc' & Hloc' & -> & Hmem). - assert (Hsmall: scalarbitsz < 2 ^ 32) by (rewrite <- scalarbitsz_small; apply Z.mod_pos_bound; lia). + assert (Hsmall: scalarbitsz < 2 ^ 64) by (rewrite <- scalarbitsz_small; apply Z.mod_pos_bound; lia). eexists ?[b]; ssplit. eexists; split; [apply map.get_put_same|]. eapply Core.WeakestPrecondition_dexpr_expr; [|apply ExprCompiler.expr_compile_Z_literal]. @@ -576,7 +576,7 @@ Section WithParameters. 1-2: solve_bounds. repeat match goal with | H: context [Array.array ptsto _ ?a _] |- context [Field.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 => @@ -675,7 +675,7 @@ Section WithParameters. 1-3:solve_bounds. repeat match goal with | H: context [Array.array ptsto _ ?a _] |- context [Field.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 => @@ -733,7 +733,7 @@ Section WithParameters. 1-3: solve_bounds. repeat match goal with | H: context [Array.array ptsto _ ?a _] |- context [Field.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 => @@ -944,27 +944,67 @@ Section WithParameters. End WithParameters. -(* Require Import bedrock2.ToCString. *) -(* Require Import coqutil.Macros.WithBaseName. *) -(* Definition funcs := *) -(* List.app *) -(* [ secp256k1_opp; *) -(* secp256k1_mul; *) -(* secp256k1_add; *) -(* secp256k1_sub; *) -(* secp256k1_square; *) -(* secp256k1_to_bytes; *) -(* secp256k1_from_bytes; *) -(* secp256k1_from_mont; *) -(* secp256k1_to_mont; *) -(* secp256k1_select_znz] *) -(* &[,secp256k1_make_co_z; *) -(* secp256k1_felem_cswap; *) -(* secp256k1_zaddu; *) -(* secp256k1_dblu; *) -(* secp256k1_tplu; *) -(* secp256k1_zdau; *) -(* secp256k1_inv; *) -(* (secp256k1_laddermul 256%Z)]. *) +Require Import bedrock2.ToCString. +Require Import coqutil.Macros.WithBaseName. +Definition funcs := + let secp256k1_laddermul := (secp256k1_laddermul 256%Z) in + List.app + [ secp256k1_opp; + secp256k1_mul; + secp256k1_add; + secp256k1_sub; + secp256k1_square; + secp256k1_to_bytes; + secp256k1_from_bytes; + secp256k1_from_mont; + secp256k1_to_mont; + secp256k1_select_znz; + secp256k1_felem_copy; + ("felem_cswap", secp256k1_felem_cswap)] + &[,secp256k1_make_co_z; + secp256k1_zaddu; + secp256k1_dblu; + secp256k1_tplu; + secp256k1_zdau; + secp256k1_inv; + secp256k1_laddermul + ]. + +Lemma link_secp256k1_felem_copy : + spec_of_secp256k1_felem_copy (map.of_list funcs). +Proof. apply secp256k1_felem_copy_correct. reflexivity. Qed. +(* ^-- Why is only felem_copy so slow ???!!! *) + +(* Assume m = 2 ^ 256 - 2 ^ 32 - 977 is prime *) +Lemma link_secp256k1_laddermul (secp256k1_prime: Znumtheory.prime m) : + @spec_of_laddermul (F.field_modulo M_pos) (0%F) (F.of_Z _ 7%Z) (256%Z) (map.of_list funcs). +Proof. + eapply spec_of_laddermul_ok; repeat + match goal with + | |- map.get _ _ = _ => reflexivity + | |- spec_of_secp256k1_tplu _ => eapply secp256k1_tplu_ok + | |- spec_of_dblu _ => eapply secp256k1_dblu_ok + | |- spec_of_zaddu _ => eapply secp256k1_zaddu_ok + | |- spec_of_secp256k1_opp _ => eapply secp256k1_opp_correct + | |- spec_of_secp256k1_zaddu _ => eapply secp256k1_zaddu_ok + | |- spec_of_secp256k1_zdau _ => eapply secp256k1_zdau_ok + | |- spec_of_secp256k1_make_co_z _ => eapply secp256k1_make_co_z_ok + | |- spec_of_secp256k1_inv _ => eapply secp256k1_inv_ok + | |- JacobianCoZ.spec_of_secp256k1_add _ => eapply secp256k1_add_correct + | |- JacobianCoZ.spec_of_secp256k1_sub _ => eapply secp256k1_sub_correct + | |- spec_of_secp256k1_mul _ => eapply secp256k1_mul_correct + | |- JacobianCoZ.spec_of_secp256k1_mul _ => eapply secp256k1_mul_correct + | |- JacobianCoZ.spec_of_secp256k1_square _ => eapply secp256k1_square_correct + | |- Addchain.spec_of_secp256k1_mul _ => eapply secp256k1_mul_correct + | |- Addchain.spec_of_secp256k1_square _ => eapply secp256k1_square_correct + | |- spec_of_secp256k1_cswap _ => eapply cswap_body_correct + | |- spec_of_secp256k1_felem_copy _ => apply link_secp256k1_felem_copy + | |- Z.of_nat _ < 2 ^ 64 => unfold field_representation, Signature.field_representation, Representation.frep; cbn; cbv; trivial + | |- Core.__rupicola_program_marker _ => cbv [Core.__rupicola_program_marker]; tauto + | _ => idtac + end. + Unshelve. + all: cbn; reflexivity. +Qed. (* Compute (ToCString.c_module funcs). *)