From ec85f83d554f8fff4ca6ec2972fd7d6dcf2bb2d4 Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Fri, 8 Mar 2024 14:20:46 +0100 Subject: [PATCH 01/10] Point doubling formula in jacobian coordinates for short Weierstrass curves when a=0 --- src/Curves/Weierstrass/Jacobian/Jacobian.v | 38 ++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/src/Curves/Weierstrass/Jacobian/Jacobian.v b/src/Curves/Weierstrass/Jacobian/Jacobian.v index 562ee287db..f10b5f37b6 100644 --- a/src/Curves/Weierstrass/Jacobian/Jacobian.v +++ b/src/Curves/Weierstrass/Jacobian/Jacobian.v @@ -588,5 +588,43 @@ Module Jacobian. eq (double P) (double_minus_3 P). Proof. faster_t. Qed. End AEqMinus3. + (** If [a] is 0, one can substitute a faster implementation of [double]. *) + Section AEqZero. + Context (a_eq_zero : a = Fzero). + + (** See http://hyperelliptic.org/EFD/g1p/auto-shortw-jacobian-0.html#doubling-dbl-2009-l *) + Program Definition double_aeq0 (P : point) : point := + match proj1_sig P return F*F*F with + | (x_in, y_in, z_in) => + let A := x_in^2 in + let B := y_in^2 in + let C := B^2 in + let t0 := x_in + B in + let t1 := t0^2 in + let t2 := t1 - A in + let t3 := t2 - C in + let D := t3 + t3 in + let E := A + A + A in + let F := E^2 in + let t4 := D + D in + let x_out := F - t4 in + let t5 := D - x_out in + let four_C := C + C in + let four_C := four_C + four_C in + let t6 := four_C + four_C in + let t7 := E * t5 in + let y_out := t7 - t6 in + let t8 := y_in * z_in in + let z_out := t8 + t8 in + (x_out, y_out, z_out) + end. + Next Obligation. Proof. t. Qed. + + Hint Unfold double_aeq0 : points_as_coordinates. + + Lemma double_aeq0_eq_double (P : point) : + eq (double P) (double_aeq0 P). + Proof. faster_t. Qed. + End AEqZero. End Jacobian. End Jacobian. From 8efb0dce85f6c9a7bdccf5ad7b5a4cdaeac958ec Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Fri, 12 Apr 2024 17:26:29 +0200 Subject: [PATCH 02/10] WIP --- src/Bedrock/End2End/Secp256k1/Field256k1.v | 199 +++++++++++++++++ src/Bedrock/End2End/Secp256k1/JacobianCoZ.v | 229 ++++++++++++++++++++ 2 files changed, 428 insertions(+) create mode 100644 src/Bedrock/End2End/Secp256k1/Field256k1.v create mode 100644 src/Bedrock/End2End/Secp256k1/JacobianCoZ.v diff --git a/src/Bedrock/End2End/Secp256k1/Field256k1.v b/src/Bedrock/End2End/Secp256k1/Field256k1.v new file mode 100644 index 0000000000..1085f0e5a2 --- /dev/null +++ b/src/Bedrock/End2End/Secp256k1/Field256k1.v @@ -0,0 +1,199 @@ +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +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.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. + Definition prefix : string := "secp256k1_"%string. + + (* Define Secp256k1 field *) + Instance field_parameters : FieldParameters. + Proof using Type. + let M := (eval vm_compute in (Z.to_pos (m))) in + (* 'A' parameter *) + let a := constr:(F.of_Z M 0) in + let prefix := constr:("secp256k1_"%string) in + eapply + (field_parameters_prefixed + M ((a + F.of_Z _ 2) / F.of_Z _ 4)%F prefix). + Defined. + + Definition to_mont_string := (prefix ++ "to_mont")%string. + Definition from_mont_string := (prefix ++ "from_mont")%string. + + (* Call fiat-crypto pipeline on all field operations *) + Instance secp256k1_ops : @word_by_word_Montgomery_ops from_mont_string to_mont_string _ _ _ _ _ _ _ _ _ _ (WordByWordMontgomery.n m machine_wordsize) m. + Proof using Type. Time constructor; make_computed_op. Defined. + + (**** 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 := + lazymatch goal with + | |- context [spec_of_BinOp bin_mul] => eapply mul_func_correct + | |- context [spec_of_UnOp un_square] => eapply square_func_correct + | |- context [spec_of_BinOp bin_add] => eapply add_func_correct + | |- context [spec_of_BinOp bin_sub] => eapply sub_func_correct + | |- context [spec_of_UnOp un_opp] => eapply opp_func_correct + | |- context [spec_of_from_bytes] => eapply from_bytes_func_correct + | |- context [spec_of_to_bytes] => eapply to_bytes_func_correct + | |- context [spec_of_selectznz] => eapply select_znz_func_correct + | |- context [spec_of_UnOp un_from_mont] => eapply (from_mont_func_correct _ _ _ from_mont_string to_mont_string) + | |- 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. + + Local Notation functions_contain functions f := + (Interface.map.get functions (fst f) = Some (snd f)). + + + + Derive secp256k1_from_bytes + SuchThat (forall functions, + functions_contain functions secp256k1_from_bytes -> + spec_of_from_bytes + (field_representation:=field_representation_raw m) + functions) + As secp256k1_from_bytes_correct. + Proof. Time derive_bedrock2_func from_bytes_op. Qed. + + Derive secp256k1_to_bytes + SuchThat (forall functions, + functions_contain functions secp256k1_to_bytes -> + spec_of_to_bytes + (field_representation:=field_representation_raw m) + functions) + As secp256k1_to_bytes_correct. + Proof. Time derive_bedrock2_func to_bytes_op. Qed. + + Derive secp256k1_opp + SuchThat (forall functions, + functions_contain functions secp256k1_opp -> + spec_of_UnOp un_opp + (field_representation:=field_representation m) + functions) + As secp256k1_opp_correct. + Proof. Time derive_bedrock2_func opp_op. Qed. + + Derive secp256k1_mul + SuchThat (forall functions, + functions_contain functions secp256k1_mul -> + spec_of_BinOp bin_mul + (field_representation:=field_representation m) + functions) + As secp256k1_mul_correct. + Proof. Time derive_bedrock2_func mul_op. Qed. + + Derive secp256k1_square + SuchThat (forall functions, + functions_contain functions secp256k1_square -> + spec_of_UnOp un_square + (field_representation:=field_representation m) + functions) + As secp256k1_square_correct. + Proof. Time derive_bedrock2_func square_op. Qed. + + Derive secp256k1_add + SuchThat (forall functions, + functions_contain functions secp256k1_add -> + spec_of_BinOp bin_add + (field_representation:=field_representation m) + functions) + As secp256k1_add_correct. + Proof. Time derive_bedrock2_func add_op. Qed. + + Derive secp256k1_sub + SuchThat (forall functions, + functions_contain functions secp256k1_sub -> + spec_of_BinOp bin_sub + (field_representation:=field_representation m) + functions) + As secp256k1_sub_correct. + Proof. Time derive_bedrock2_func sub_op. Qed. + + Derive secp256k1_select_znz + SuchThat (forall functions, + functions_contain functions secp256k1_select_znz -> + spec_of_selectznz + (field_representation:=field_representation m) + functions) + As secp256k1_select_znz_correct. + Proof. Time derive_bedrock2_func select_znz_op. Qed. + + Derive secp256k1_from_mont + SuchThat (forall functions, + functions_contain functions secp256k1_from_mont -> + spec_of_UnOp un_from_mont + (field_representation:=field_representation m) + functions) + As secp256k1_from_mont_correct. + Proof. Time derive_bedrock2_func from_mont_op. Unshelve. 1,2: auto. Qed. + + Derive secp256k1_to_mont + SuchThat (forall functions, + functions_contain functions secp256k1_to_mont -> + spec_of_UnOp un_to_mont + (field_representation:=field_representation m) + functions) + As secp256k1_to_mont_correct. + Proof. Time derive_bedrock2_func to_mont_op. Unshelve. 1,2: auto. Qed. + + #[export] Instance frep256k1_ok : FieldRepresentation_ok(field_representation:=field_representation m). + Proof. + apply Crypto.Bedrock.Field.Synthesis.New.Signature.field_representation_ok. + auto. + Qed. +End Field. + +(* Require Import bedrock2.Syntax. *) + +(* Definition funcs : list (string * func) := *) +(* [ 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 *) +(* ]. *) + +(* Compute ToCString.c_module funcs. *) diff --git a/src/Bedrock/End2End/Secp256k1/JacobianCoZ.v b/src/Bedrock/End2End/Secp256k1/JacobianCoZ.v new file mode 100644 index 0000000000..f2cbe647d2 --- /dev/null +++ b/src/Bedrock/End2End/Secp256k1/JacobianCoZ.v @@ -0,0 +1,229 @@ +Require Import bedrock2.Array. +Require Import bedrock2.FE310CSemantics. +Require Import bedrock2.Loops. +Require Import bedrock2.Map.Separation. +Require Import bedrock2.Map.SeparationLogic. +Require Import bedrock2.NotationsCustomEntry. +Require Import bedrock2.ProgramLogic. +Require Import bedrock2.Scalars. +Require Import bedrock2.Semantics. +Require Import bedrock2.Syntax. +Require Import bedrock2.WeakestPrecondition. +Require Import bedrock2.WeakestPreconditionProperties. +Require Import bedrock2.ZnWords. +Require Import compiler.MMIO. +Require Import compiler.Pipeline. +Require Import compiler.Symbols. +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.Bitwidth. +Require Import coqutil.Word.Interface. +Require Import Coq.Init.Byte. +Require Import Coq.Lists.List. +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Bedrock.Field.Interface.Compilation2. +Require Import Crypto.Bedrock.Field.Synthesis.New.WordByWordMontgomery. +Require Import Crypto.Bedrock.Group.ScalarMult.CSwap. +Require Import Crypto.Bedrock.End2End.Secp256k1.Field256k1. +Require Import Crypto.Bedrock.Specs.Field. +Require Import Crypto.Util.Decidable. +Require Import Curves.Weierstrass.Jacobian.Jacobian. +Require Import Curves.Weierstrass.Jacobian.CoZ. +Require Import Lia. +Require Crypto.Bedrock.Field.Synthesis.New.Signature. +Local Open Scope string_scope. +Local Open Scope Z_scope. +Import LittleEndianList. +Import ListNotations. +Import ProgramLogic.Coercions. +Import WeakestPrecondition. + +Local Existing Instance field_parameters. +Local Instance frep256k1 : Field.FieldRepresentation := field_representation Field256k1.m. +Local Existing Instance frep256k1_ok. + +(* P = (X1, Y1, Z1) + Q = (X2, Y2, Z2) + Returns P + Q = (OX1, OY1, OZ1) + P = (OX2, OY2, OZ2) +*) +Definition secp256k1_zaddu := + func! (OX1, OY1, OZ1, OX2, OY2, OZ2, X1, Y1, Z1, X2, Y2, Z2) { + stackalloc 32 as T1; + stackalloc 32 as T2; + stackalloc 32 as T3; + stackalloc 32 as T4; + stackalloc 32 as T5; + stackalloc 32 as T6; + secp256k1_felem_copy(T1, X1); + secp256k1_felem_copy(T2, Y1); + secp256k1_felem_copy(T3, Z1); + secp256k1_felem_copy(T4, X2); + secp256k1_felem_copy(T5, Y2); + secp256k1_sub(T6, T1, T4); (* let t6 := t1 - t4 in *) + secp256k1_mul(T3, T3, T6); (* let t3 := t3 * t6 in *) + secp256k1_square(T6, T6); (* let t6 := t6^2 in *) + secp256k1_mul(T1, T1, T6); (* let t1 := t1 * t6 in *) + secp256k1_mul(T6, T6, T4); (* let t6 := t6 * t4 in *) + secp256k1_sub(T5, T2, T5); (* let t5 := t2 - t5 in *) + secp256k1_square(T4, T5); (* let t4 := t5^2 in *) + secp256k1_sub(T4, T4, T1); (* let t4 := t4 - t1 in *) + secp256k1_sub(T4, T4, T6); (* let t4 := t4 - t6 in *) + secp256k1_sub(T6, T1, T6); (* let t6 := t1 - t6 in *) + secp256k1_mul(T2, T2, T6); (* let t2 := t2 * t6 in *) + secp256k1_sub(T6, T1, T4); (* let t6 := t1 - t4 in *) + secp256k1_mul(T5, T5, T6); (* let t5 := t5 * t6 in *) + secp256k1_sub(T5, T5, T2); (* let t5 := t5 - t2 in *) + secp256k1_felem_copy(OX1, T4); (* ((t4, t5, t3), (t1, t2, t3)) *) + secp256k1_felem_copy(OY1, T5); + secp256k1_felem_copy(OZ1, T3); + secp256k1_felem_copy(OX2, T1); + secp256k1_felem_copy(OY2, T2); + secp256k1_felem_copy(OZ2, T3) +}. + +(* Compute ToCString.c_func ("secp256k1_zaddu", secp256k1_zaddu). *) + +Section WithParameters. + Context {two_lt_M: 2 < M_pos}. + (* TODO: Can we provide actual values/proofs for these, rather than just sticking them in the context? *) + 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} + {zero_a : a = F.zero} + {seven_b : 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 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)). + Local Notation zaddu := + (Jacobian.zaddu(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one) + (Fopp:=F.opp)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div) + (a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). + + Global Instance spec_of_zaddu : spec_of "secp256k1_zaddu" := + fnspec! "secp256k1_zaddu" + (OX1K OY1K OZ1K OX2K OY2K OZ2K X1K Y1K Z1K X2K Y2K Z2K : word) / + (OX1 OY1 OZ1 OX2 OY2 OZ2 X1 Y1 Z1 X2 Y2 Z2 : felem) (P Q : point) + (HPQ : co_z P Q) (R : _ -> Prop), + { requires t m := + proj1_sig P = ((feval X1), (feval Y1), (feval Z1)) /\ + proj1_sig Q = ((feval X2), (feval Y2), (feval Z2)) /\ + (* bounded_by loose_bounds X1 /\ *) + (* bounded_by loose_bounds Y1 /\ *) + (* bounded_by loose_bounds Z1 /\ *) + (* bounded_by loose_bounds X2 /\ *) + (* bounded_by loose_bounds Y2 /\ *) + (* bounded_by loose_bounds Z2 /\ *) + m =* (FElem OX1K OX1) * (FElem OY1K OY1) * (FElem OZ1K OZ1) * + (FElem OX2K OX2) * (FElem OY2K OY2) * (FElem OZ2K OZ2) * + (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * + (FElem X2K X2) * (FElem Y2K Y2) * (FElem Z2K Z2) * R; + ensures t' m' := + t = t' /\ + exists OX1' OY1' OZ1' OX2' OY2' OZ2', + proj1_sig (fst (zaddu P Q HPQ)) = ((feval OX1'), (feval OY1'), (feval OZ1')) /\ + proj1_sig (snd (zaddu P Q HPQ)) = ((feval OX2'), (feval OY2'), (feval OZ2')) /\ + (* bounded_by tight_bounds OX1' /\ *) + (* bounded_by tight_bounds OY1' /\ *) + (* bounded_by tight_bounds OZ1' /\ *) + (* bounded_by tight_bounds OX2' /\ *) + (* bounded_by tight_bounds OY2' /\ *) + (* bounded_by tight_bounds OZ2' /\ *) + m' =* (FElem OX1K OX1') * (FElem OY1K OY1') * (FElem OZ1K OZ1') * + (FElem OX2K OX2') * (FElem OY2K OY2') * (FElem OZ2K OZ2') * + (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * + (FElem X2K X2) * (FElem Y2K Y2) * (FElem Z2K Z2) * R + }. + + Local Instance spec_of_secp256k1_opp : spec_of "secp256k1_opp" := Field.spec_of_UnOp un_opp. + Local Instance spec_of_secp256k1_square : spec_of "secp256k1_square" := Field.spec_of_UnOp un_square. + Local Instance spec_of_secp256k1_mul : spec_of "secp256k1_mul" := Field.spec_of_BinOp bin_mul. + Local Instance spec_of_secp256k1_add : spec_of "secp256k1_add" := Field.spec_of_BinOp bin_add. + Local Instance spec_of_secp256k1_sub : spec_of "secp256k1_sub" := Field.spec_of_BinOp bin_carry_sub. + Local Instance spec_of_secp256k1_felem_copy : spec_of "secp256k1_felem_copy" := Field.spec_of_felem_copy. + + Local Arguments word.rep : simpl never. + Local Arguments word.wrap : simpl never. + Local Arguments word.unsigned : simpl never. + Local Arguments word.of_Z : simpl never. + + Local Ltac solve_mem := + repeat match goal with + | |- exists _ : _ -> Prop, _%sep _ => eexists + | |- _%sep _ => ecancel_assumption + end. + + Local Ltac cbv_bounds H := + cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds] in H; + cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds]. + + Local Ltac solve_bounds := + repeat match goal with + | H: bounded_by loose_bounds ?x |- bounded_by loose_bounds ?x => apply H + | H: bounded_by tight_bounds ?x |- bounded_by tight_bounds ?x => apply H + | H: bounded_by tight_bounds ?x |- bounded_by loose_bounds ?x => apply relax_bounds + | H: bounded_by _ ?x |- bounded_by _ ?x => cbv_bounds H + end. + + Local Ltac solve_stack := + (* Rewrites the `stack$@a` term in H to use a Bignum instead *) + 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 + end; + [> transitivity 32%nat; trivial | ]; + (* proves the memory matches up *) + use_sep_assumption; cancel; cancel_seps_at_indices 0%nat 0%nat; cbn; [> trivial | eapply RelationClasses.reflexivity]. + + Local Ltac single_step := + repeat straightline; straightline_call; ssplit; try solve_mem; try solve_bounds; try solve_stack. + + Lemma zaddu_ok : program_logic_goal_for_function! secp256k1_zaddu. + Proof. + Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds]. + Compute felem_copy. + single_step. + + repeat straightline. + eapply Proper_call; cycle -1; + [ | try eabstract (solve [ Morphisms.solve_proper ]).. ]; + [ .. | intros ? ? ? ? ]. + eapply H12. + + + + eapply Proper_call; [try eabstract (solve [ Morphisms.solve_proper ]).. |]. + intros ? ? ? ?. eexists. split. cbv. + + + unfold program_logic_goal_for. intros. + unfold spec_of_zaddu. intros. eapply Proper_call; cycle -1. + eapply start_func; eauto. unfold func. + + + + repeat straightline. + eapply Proper_call; cycle -1. + unfold call. + eapply spec_of_secp256k1_sub. + + straightline_call. + single_step. + + + + +Compute (ToCString.c_func ("ZADDU", ZADDU)). From 73a2220a6c0826b1d41048dab666730fe19b7164 Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Thu, 25 Apr 2024 22:39:08 +0200 Subject: [PATCH 03/10] Bedrock2 secp256k1 point operations --- src/Bedrock/End2End/Secp256k1/Field256k1.v | 10 +- src/Bedrock/End2End/Secp256k1/JacobianCoZ.v | 720 ++++++++++++++++++-- 2 files changed, 654 insertions(+), 76 deletions(-) diff --git a/src/Bedrock/End2End/Secp256k1/Field256k1.v b/src/Bedrock/End2End/Secp256k1/Field256k1.v index 1085f0e5a2..86925cb2ce 100644 --- a/src/Bedrock/End2End/Secp256k1/Field256k1.v +++ b/src/Bedrock/End2End/Secp256k1/Field256k1.v @@ -50,6 +50,7 @@ Section Field. | |- context [spec_of_from_bytes] => eapply from_bytes_func_correct | |- context [spec_of_to_bytes] => eapply to_bytes_func_correct | |- context [spec_of_selectznz] => eapply select_znz_func_correct + | |- context [spec_of_felem_copy] => eapply felem_copy_func_correct | |- context [spec_of_UnOp un_from_mont] => eapply (from_mont_func_correct _ _ _ from_mont_string to_mont_string) | |- context [spec_of_UnOp un_to_mont] => eapply (to_mont_func_correct _ _ _ from_mont_string to_mont_string) end. @@ -82,7 +83,14 @@ Section Field. Local Notation functions_contain functions f := (Interface.map.get functions (fst f) = Some (snd f)). - + Derive secp256k1_felem_copy + SuchThat (forall functions, + functions_contain functions secp256k1_felem_copy -> + spec_of_felem_copy + (field_representation:=field_representation_raw m) + functions) + As secp256k1_felem_copy_correct. + Proof. Time derive_bedrock2_func felem_copy_op. Qed. Derive secp256k1_from_bytes SuchThat (forall functions, diff --git a/src/Bedrock/End2End/Secp256k1/JacobianCoZ.v b/src/Bedrock/End2End/Secp256k1/JacobianCoZ.v index f2cbe647d2..b4a0db1ec0 100644 --- a/src/Bedrock/End2End/Secp256k1/JacobianCoZ.v +++ b/src/Bedrock/End2End/Secp256k1/JacobianCoZ.v @@ -47,55 +47,203 @@ Local Existing Instance field_parameters. Local Instance frep256k1 : Field.FieldRepresentation := field_representation Field256k1.m. Local Existing Instance frep256k1_ok. -(* P = (X1, Y1, Z1) - Q = (X2, Y2, Z2) - Returns P + Q = (OX1, OY1, OZ1) - P = (OX2, OY2, OZ2) -*) +Definition secp256k1_jopp := + func! (OX, OY, OZ, X, Y, Z) { + secp256k1_felem_copy(OX, X); + secp256k1_opp(OY, Y); + secp256k1_felem_copy(OZ, Z) +}. + +Definition secp256k1_make_co_z := + func! (OX, OY, X, Y, Z) { + stackalloc 32 as T; + secp256k1_square(T, Z); + secp256k1_mul(OX, X, T); + secp256k1_mul(T, T, Z); + secp256k1_mul(OY, Y, T) +}. + +(* TODO: Can we optimize away the felem_copy? *) Definition secp256k1_zaddu := - func! (OX1, OY1, OZ1, OX2, OY2, OZ2, X1, Y1, Z1, X2, Y2, Z2) { + func! (OX1, OY1, OX2, OY2, OZ, X1, Y1, X2, Y2, Z) { stackalloc 32 as T1; stackalloc 32 as T2; - stackalloc 32 as T3; stackalloc 32 as T4; stackalloc 32 as T5; stackalloc 32 as T6; - secp256k1_felem_copy(T1, X1); - secp256k1_felem_copy(T2, Y1); - secp256k1_felem_copy(T3, Z1); - secp256k1_felem_copy(T4, X2); - secp256k1_felem_copy(T5, Y2); - secp256k1_sub(T6, T1, T4); (* let t6 := t1 - t4 in *) - secp256k1_mul(T3, T3, T6); (* let t3 := t3 * t6 in *) + secp256k1_sub(T6, X1, X2); (* let t6 := t1 - t4 in *) + secp256k1_mul(OZ, Z, T6); (* let t3 := t3 * t6 in *) secp256k1_square(T6, T6); (* let t6 := t6^2 in *) - secp256k1_mul(T1, T1, T6); (* let t1 := t1 * t6 in *) - secp256k1_mul(T6, T6, T4); (* let t6 := t6 * t4 in *) - secp256k1_sub(T5, T2, T5); (* let t5 := t2 - t5 in *) + secp256k1_mul(T1, X1, T6); (* let t1 := t1 * t6 in *) + secp256k1_mul(T6, T6, X2); (* let t6 := t6 * t4 in *) + secp256k1_sub(T5, Y1, Y2); (* let t5 := t2 - t5 in *) secp256k1_square(T4, T5); (* let t4 := t5^2 in *) secp256k1_sub(T4, T4, T1); (* let t4 := t4 - t1 in *) secp256k1_sub(T4, T4, T6); (* let t4 := t4 - t6 in *) secp256k1_sub(T6, T1, T6); (* let t6 := t1 - t6 in *) - secp256k1_mul(T2, T2, T6); (* let t2 := t2 * t6 in *) + secp256k1_mul(T2, Y1, T6); (* let t2 := t2 * t6 in *) secp256k1_sub(T6, T1, T4); (* let t6 := t1 - t4 in *) secp256k1_mul(T5, T5, T6); (* let t5 := t5 * t6 in *) secp256k1_sub(T5, T5, T2); (* let t5 := t5 - t2 in *) secp256k1_felem_copy(OX1, T4); (* ((t4, t5, t3), (t1, t2, t3)) *) secp256k1_felem_copy(OY1, T5); - secp256k1_felem_copy(OZ1, T3); secp256k1_felem_copy(OX2, T1); - secp256k1_felem_copy(OY2, T2); - secp256k1_felem_copy(OZ2, T3) + secp256k1_felem_copy(OY2, T2) +}. + +(* TODO: Can we optimize away the felem_copy? *) +Definition secp256k1_zaddc := + func! (OX1, OY1, OX2, OY2, OZ, X1, Y1, X2, Y2, Z) { + stackalloc 32 as T1; + stackalloc 32 as T2; + stackalloc 32 as T4; + stackalloc 32 as T5; + stackalloc 32 as T6; + secp256k1_sub(T6, X1, X2); (* let t6 := t1 - t4 in *) + secp256k1_mul(OZ, Z, T6); (* let t3 := t3 * t6 in *) + secp256k1_square(T6, T6); (* let t6 := t6^2 in *) + stackalloc 32 as T7; + secp256k1_mul(T7, X1, T6); (* let t7 := t1 * t6 in *) + secp256k1_mul(T6, T6, X2); (* let t6 := t6 * t4 in *) + secp256k1_add(T1, Y1, Y2); (* let t1 := t2 + t5 in *) + secp256k1_square(T4, T1); (* let t4 := t1^2 in *) + secp256k1_sub(T4, T4, T7); (* let t4 := t4 - t7 in *) + secp256k1_sub(T4, T4, T6); (* let t4 := t4 - t6 in *) + secp256k1_sub(T1, Y1, Y2); (* let t1 := t2 - t5 in *) + secp256k1_square(T1, T1); (* let t1 := t1^2 in *) + secp256k1_sub(T1, T1, T7); (* let t1 := t1 - t7 in *) + secp256k1_sub(T1, T1, T6); (* let t1 := t1 - t6 in *) + secp256k1_sub(T6, T6, T7); (* let t6 := t6 - t7 in *) + secp256k1_mul(T6, T6, Y1); (* let t6 := t6 * t2 in *) + secp256k1_sub(T2, Y1, Y2); (* let t2 := t2 - t5 in *) + secp256k1_add(T5, Y2, Y2); (* let t5 := t5 + t5 in *) + secp256k1_add(T5, T2, T5); (* let t5 := t2 + t5 in *) + secp256k1_sub(T7, T7, T4); (* let t7 := t7 - t4 in *) + secp256k1_mul(T5, T5, T7); (* let t5 := t5 * t7 in *) + secp256k1_add(T5, T5, T6); (* let t5 := t5 + t6 in *) + secp256k1_add(T7, T4, T7); (* let t7 := t4 + t7 in *) + secp256k1_sub(T7, T7, T1); (* let t7 := t7 - t1 in *) + secp256k1_mul(T2, T2, T7); (* let t2 := t2 * t7 in *) + secp256k1_add(T2, T2, T6); (* let t2 := t2 + t6 in *) + secp256k1_felem_copy(OX1, T1); (* ((t1, t2, t3), (t4, t5, t3)) *) + secp256k1_felem_copy(OY1, T2); + secp256k1_felem_copy(OX2, T4); + secp256k1_felem_copy(OY2, T5) }. +(* Specialized with a=0 *) +Definition secp256k1_dblu := + func! (OX1, OY1, OX2, OY2, OZ, X1, Y1) { + stackalloc 32 as T1; + stackalloc 32 as T2; + secp256k1_add(OZ, Y1, Y1); (* let t3 := t2 + t2 in *) + secp256k1_square(T2, Y1); (* let t2 := t2^2 in *) + stackalloc 32 as T4; + secp256k1_add(T4, X1, T2); (* let t4 := t1 + t2 in *) + secp256k1_square(T4, T4); (* let t4 := t4^2 in *) + stackalloc 32 as T5; + secp256k1_square(T5, X1); (* let t5 := t1^2 in *) + secp256k1_sub(T4, T4, T5); (* let t4 := t4 - t5 in *) + secp256k1_square(T2, T2); (* let t2 := t2^2 in *) + secp256k1_sub(T4, T4, T2); (* let t4 := t4 - t2 in *) + secp256k1_add(T1, T4, T4); (* let t1 := t4 + t4 in *) + (* secp256k1_add(T0, T0, T5); *) (* let t0 := t0 + t5 in *) + stackalloc 32 as T0; + secp256k1_felem_copy(T0, T5); (* a = 0 for secp256k1 *) + secp256k1_add(T5, T5, T5); (* let t5 := t5 + t5 in *) + secp256k1_add(T0, T0, T5); (* let t0 := t0 + t5 in *) + secp256k1_square(T4, T0); (* let t4 := t0^2 in *) + secp256k1_add(T5, T1, T1); (* let t5 := t1 + t1 in *) + secp256k1_sub(T4, T4, T5); (* let t4 := t4 - t5 in *) + secp256k1_add(T2, T2, T2); + secp256k1_add(T2, T2, T2); + secp256k1_add(T2, T2, T2); (* let t2 := 8 * t2 in *) + secp256k1_sub(T5, T1, T4); (* let t5 := t1 - t4 in *) + secp256k1_mul(T5, T5, T0); (* let t5 := t5 * t0 in *) + secp256k1_sub(T5, T5, T2); (* let t5 := t5 - t2 in *) + secp256k1_felem_copy(OX1, T4); (* ((t4, t5, t3), (t1, t2, t3)) *) + secp256k1_felem_copy(OY1, T5); + secp256k1_felem_copy(OX2, T1); + secp256k1_felem_copy(OY2, T2) +}. + +(* TODO: it should be possible to not use any temp field registers *) +Definition secp256k1_tplu := + func! (OX1, OY1, OX2, OY2, OZ, X1, Y1) { + stackalloc 32 as T1; + stackalloc 32 as T2; + stackalloc 32 as T3; + stackalloc 32 as T4; + stackalloc 32 as T5; + secp256k1_dblu(T1, T2, T3, T4, T5, X1, Y1); + secp256k1_zaddu(OX1, OY1, OX2, OY2, OZ, T3, T4, T1, T2, T5) +}. + +Definition secp256k1_zdau := + func! (X1, Y1, X2, Y2, Z) { + stackalloc 32 as T1; + stackalloc 32 as T2; + stackalloc 32 as T4; + stackalloc 32 as T5; + stackalloc 32 as T6; + secp256k1_sub(T6, X1, X2); (* let t6 := t1 - t4 in *) + stackalloc 32 as T7; + secp256k1_square(T7, T6); (* let t7 := t6^2 in *) + secp256k1_mul(T1, X1, T7); (* let t1 := t1 * t7 in *) + secp256k1_mul(T4, X2, T7); (* let t4 := t4 * t7 in *) + secp256k1_sub(T5, Y1, Y2); (* let t5 := t2 - t5 in *) + stackalloc 32 as T8; + secp256k1_sub(T8, T1, T4); (* let t8 := t1 - t4 in *) + secp256k1_mul(T2, Y1, T8); (* let t2 := t2 * t8 in *) + secp256k1_add(T2, T2, T2); (* let t2 := t2 + t2 in *) + secp256k1_square(T8, T5); (* let t8 := t5^2 in *) + secp256k1_sub(T4, T8, T4); (* let t4 := t8 - t4 in *) + secp256k1_sub(T4, T4, T1); (* let t4 := t4 - t1 in *) + secp256k1_sub(T4, T4, T1); (* let t4 := t4 - t1 in *) + secp256k1_add(T6, T4, T6); (* let t6 := t4 + t6 in *) + secp256k1_square(T6, T6); (* let t6 := t6^2 in *) + secp256k1_sub(T6, T6, T7); (* let t6 := t6 - t7 in *) + secp256k1_sub(T5, T5, T4); (* let t5 := t5 - t4 in *) + secp256k1_square(T5, T5); (* let t5 := t5^2 in *) + secp256k1_sub(T5, T5, T8); (* let t5 := t5 - t8 in *) + secp256k1_sub(T5, T5, T2); (* let t5 := t5 - t2 in *) + secp256k1_square(T7, T4); (* let t7 := t4^2 in *) + secp256k1_sub(T5, T5, T7); (* let t5 := t5 - t7 in *) + secp256k1_add(T8, T7, T7); (* let t8 := t7 + t7 in *) + secp256k1_add(T8, T8, T8); (* let t8 := t8 + t8 in *) + secp256k1_sub(T6, T6, T7); (* let t6 := t6 - t7 in *) + secp256k1_mul(Z, Z, T6); (* let t3 := t3 * t6 in *) + secp256k1_mul(T6, T1, T8); (* let t6 := t1 * t8 in *) + secp256k1_add(T1, T1, T4); (* let t1 := t1 + t4 in *) + secp256k1_mul(T8, T8, T1); (* let t8 := t8 * t1 in *) + secp256k1_add(T7, T2, T5); (* let t7 := t2 + t5 in *) + secp256k1_sub(T2, T5, T2); (* let t2 := t5 - t2 in *) + secp256k1_sub(T1, T8, T6); (* let t1 := t8 - t6 in *) + secp256k1_mul(T5, T5, T1); (* let t5 := t5 * t1 in *) + secp256k1_add(T6, T6, T8); (* let t6 := t6 + t8 in *) + secp256k1_square(T1, T2); (* let t1 := t2^2 in *) + secp256k1_sub(X1, T1, T6); (* let t1 := t1 - t6 in *) + secp256k1_sub(T4, T8, X1); (* let t4 := t8 - t1 in *) + secp256k1_mul(T2, T2, T4); (* let t2 := t2 * t4 in *) + secp256k1_sub(Y1, T2, T5); (* let t2 := t2 - t5 in *) + secp256k1_square(T4, T7); (* let t4 := t7^2 in *) + secp256k1_sub(X2, T4, T6); (* let t4 := t4 - t6 in *) + secp256k1_sub(T8, T8, X2); (* let t8 := t8 - t4 in *) + secp256k1_mul(T7, T7, T8); (* let t7 := t7 * t8 in *) + 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). + (* Compute ToCString.c_func ("secp256k1_zaddu", secp256k1_zaddu). *) +(* Compute ToCString.c_func ("secp256k1_felem_cswap", secp256k1_felem_cswap). *) Section WithParameters. Context {two_lt_M: 2 < M_pos}. - (* TODO: Can we provide actual values/proofs for these, rather than just sticking them in the context? *) 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} - {zero_a : a = F.zero} + Context {a b : F M_pos}. + Context {zero_a : a = F.zero} {seven_b : b = F.of_Z _ 7}. Local Coercion F.to_Z : F >-> Z. @@ -107,51 +255,234 @@ Section WithParameters. 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)). + Local Notation z_of := (Jacobian.z_of(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 jopp := + (Jacobian.opp(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one) + (Fopp:=F.opp)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div) + (a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). + Local Notation make_co_z := + (Jacobian.make_co_z(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one) + (Fopp:=F.opp)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div) + (a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). Local Notation zaddu := (Jacobian.zaddu(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one) (Fopp:=F.opp)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div) (a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). + Local Notation zaddc := + (Jacobian.zaddc(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one) + (Fopp:=F.opp)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div) + (a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). + Local Notation dblu := + (Jacobian.dblu(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one) + (Fopp:=F.opp)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div) + (a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). + Local Notation tplu := + (Jacobian.tplu(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one) + (Fopp:=F.opp)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div) + (a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). + Local Notation zdau := + (Jacobian.zdau(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one) + (Fopp:=F.opp)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div) + (a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). + + Global Instance spec_of_jopp : spec_of "secp256k1_jopp" := + fnspec! "secp256k1_jopp" + (OXK OYK OZK XK YK ZK : word) / (OX OY OZ X Y Z : felem) (P : point) + (R : _ -> Prop), + { requires t m := + proj1_sig P = ((feval X), (feval Y), (feval Z)) /\ + bounded_by loose_bounds X /\ + bounded_by loose_bounds Y /\ + bounded_by loose_bounds Z /\ + m =* (FElem OXK OX) * (FElem OYK OY) * (FElem OZK OZ) * + (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * R; + ensures t' m' := + t = t' /\ + exists OX' OY' OZ', + proj1_sig (jopp P) = ((feval OX'), (feval OY'), (feval OZ')) /\ + bounded_by tight_bounds OX' /\ + bounded_by tight_bounds OY' /\ + bounded_by tight_bounds OZ' /\ + m' =* (FElem OXK OX') * (FElem OYK OY') * (FElem OZK OZ') * + (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * R + }. + + Global Instance spec_of_make_co_z : spec_of "secp256k1_make_co_z" := + fnspec! "secp256k1_make_co_z" + (OXK OYK XK YK ZK : word) / (OX OY X Y Z : felem) + (P Q : point) (HQaff: z_of Q = 1%F) (R : _ -> Prop), + { requires t m := + (exists x y, proj1_sig P = (x, y, (feval Z))) /\ + (exists z, proj1_sig Q = ((feval X), (feval Y), z)) /\ + bounded_by loose_bounds X /\ + bounded_by loose_bounds Y /\ + bounded_by loose_bounds Z /\ + m =* (FElem OXK OX) * (FElem OYK OY) * + (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * R; + ensures t' m' := + t = t' /\ + exists OX' OY', + proj1_sig (snd (make_co_z P Q HQaff)) = ((feval OX'), (feval OY'), (feval Z)) /\ + bounded_by tight_bounds OX' /\ + bounded_by tight_bounds OY' /\ + m' =* (FElem OXK OX') * (FElem OYK OY') * + (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * R + }. Global Instance spec_of_zaddu : spec_of "secp256k1_zaddu" := fnspec! "secp256k1_zaddu" - (OX1K OY1K OZ1K OX2K OY2K OZ2K X1K Y1K Z1K X2K Y2K Z2K : word) / - (OX1 OY1 OZ1 OX2 OY2 OZ2 X1 Y1 Z1 X2 Y2 Z2 : felem) (P Q : point) + (OX1K OY1K OX2K OY2K OZK X1K Y1K X2K Y2K ZK : word) / + (OX1 OY1 OX2 OY2 OZ X1 Y1 X2 Y2 Z : felem) (P Q : point) (HPQ : co_z P Q) (R : _ -> Prop), { requires t m := - proj1_sig P = ((feval X1), (feval Y1), (feval Z1)) /\ - proj1_sig Q = ((feval X2), (feval Y2), (feval Z2)) /\ - (* bounded_by loose_bounds X1 /\ *) - (* bounded_by loose_bounds Y1 /\ *) - (* bounded_by loose_bounds Z1 /\ *) - (* bounded_by loose_bounds X2 /\ *) - (* bounded_by loose_bounds Y2 /\ *) - (* bounded_by loose_bounds Z2 /\ *) - m =* (FElem OX1K OX1) * (FElem OY1K OY1) * (FElem OZ1K OZ1) * - (FElem OX2K OX2) * (FElem OY2K OY2) * (FElem OZ2K OZ2) * - (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * - (FElem X2K X2) * (FElem Y2K Y2) * (FElem Z2K Z2) * R; + proj1_sig P = ((feval X1), (feval Y1), (feval Z)) /\ + proj1_sig Q = ((feval X2), (feval Y2), (feval Z)) /\ + bounded_by loose_bounds X1 /\ + bounded_by loose_bounds Y1 /\ + bounded_by loose_bounds X2 /\ + bounded_by loose_bounds Y2 /\ + bounded_by loose_bounds Z /\ + m =* (FElem OX1K OX1) * (FElem OY1K OY1) * + (FElem OX2K OX2) * (FElem OY2K OY2) * (FElem OZK OZ) * + (FElem X1K X1) * (FElem Y1K Y1) * + (FElem X2K X2) * (FElem Y2K Y2) * (FElem ZK Z) * R; + ensures t' m' := + t = t' /\ + exists OX1' OY1' OX2' OY2' OZ', + proj1_sig (fst (zaddu P Q HPQ)) = ((feval OX1'), (feval OY1'), (feval OZ')) /\ + proj1_sig (snd (zaddu P Q HPQ)) = ((feval OX2'), (feval OY2'), (feval OZ')) /\ + bounded_by tight_bounds OX1' /\ + bounded_by tight_bounds OY1' /\ + bounded_by tight_bounds OX2' /\ + bounded_by tight_bounds OY2' /\ + bounded_by tight_bounds OZ' /\ + m' =* (FElem OX1K OX1') * (FElem OY1K OY1') * + (FElem OX2K OX2') * (FElem OY2K OY2') * (FElem OZK OZ') * + (FElem X1K X1) * (FElem Y1K Y1) * + (FElem X2K X2) * (FElem Y2K Y2) * (FElem ZK Z) * R + }. + + Global Instance spec_of_zaddc : spec_of "secp256k1_zaddc" := + fnspec! "secp256k1_zaddc" + (OX1K OY1K OX2K OY2K OZK X1K Y1K X2K Y2K ZK : word) / + (OX1 OY1 OX2 OY2 OZ X1 Y1 X2 Y2 Z : felem) (P Q : point) + (HPQ : co_z P Q) (R : _ -> Prop), + { requires t m := + proj1_sig P = ((feval X1), (feval Y1), (feval Z)) /\ + proj1_sig Q = ((feval X2), (feval Y2), (feval Z)) /\ + bounded_by loose_bounds X1 /\ + bounded_by loose_bounds Y1 /\ + bounded_by loose_bounds X2 /\ + bounded_by loose_bounds Y2 /\ + bounded_by loose_bounds Z /\ + m =* (FElem OX1K OX1) * (FElem OY1K OY1) * + (FElem OX2K OX2) * (FElem OY2K OY2) * (FElem OZK OZ) * + (FElem X1K X1) * (FElem Y1K Y1) * + (FElem X2K X2) * (FElem Y2K Y2) * (FElem ZK Z) * R; + ensures t' m' := + t = t' /\ + exists OX1' OY1' OX2' OY2' OZ', + proj1_sig (fst (zaddc P Q HPQ)) = ((feval OX1'), (feval OY1'), (feval OZ')) /\ + proj1_sig (snd (zaddc P Q HPQ)) = ((feval OX2'), (feval OY2'), (feval OZ')) /\ + bounded_by tight_bounds OX1' /\ + bounded_by tight_bounds OY1' /\ + bounded_by tight_bounds OX2' /\ + bounded_by tight_bounds OY2' /\ + bounded_by tight_bounds OZ' /\ + m' =* (FElem OX1K OX1') * (FElem OY1K OY1') * + (FElem OX2K OX2') * (FElem OY2K OY2') * (FElem OZK OZ') * + (FElem X1K X1) * (FElem Y1K Y1) * + (FElem X2K X2) * (FElem Y2K Y2) * (FElem ZK Z) * R + }. + + Global Instance spec_of_dblu: spec_of "secp256k1_dblu" := + fnspec! "secp256k1_dblu" + (OX1K OY1K OX2K OY2K OZK X1K Y1K : word) / + (OX1 OY1 OX2 OY2 OZ X1 Y1 : felem) (P : point) + (HPaff : z_of P = F.one) (R : _ -> Prop), + { requires t m := + (exists z, proj1_sig P = ((feval X1), (feval Y1), z)) /\ + bounded_by loose_bounds X1 /\ + bounded_by loose_bounds Y1 /\ + m =* (FElem OX1K OX1) * (FElem OY1K OY1) * + (FElem OX2K OX2) * (FElem OY2K OY2) * (FElem OZK OZ) * + (FElem X1K X1) * (FElem Y1K Y1) * R; ensures t' m' := t = t' /\ - exists OX1' OY1' OZ1' OX2' OY2' OZ2', - proj1_sig (fst (zaddu P Q HPQ)) = ((feval OX1'), (feval OY1'), (feval OZ1')) /\ - proj1_sig (snd (zaddu P Q HPQ)) = ((feval OX2'), (feval OY2'), (feval OZ2')) /\ - (* bounded_by tight_bounds OX1' /\ *) - (* bounded_by tight_bounds OY1' /\ *) - (* bounded_by tight_bounds OZ1' /\ *) - (* bounded_by tight_bounds OX2' /\ *) - (* bounded_by tight_bounds OY2' /\ *) - (* bounded_by tight_bounds OZ2' /\ *) - m' =* (FElem OX1K OX1') * (FElem OY1K OY1') * (FElem OZ1K OZ1') * - (FElem OX2K OX2') * (FElem OY2K OY2') * (FElem OZ2K OZ2') * - (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * - (FElem X2K X2) * (FElem Y2K Y2) * (FElem Z2K Z2) * R + exists OX1' OY1' OX2' OY2' OZ', + proj1_sig (fst (dblu P HPaff)) = ((feval OX1'), (feval OY1'), (feval OZ')) /\ + proj1_sig (snd (dblu P HPaff)) = ((feval OX2'), (feval OY2'), (feval OZ')) /\ + bounded_by tight_bounds OX1' /\ + bounded_by tight_bounds OY1' /\ + bounded_by tight_bounds OX2' /\ + bounded_by tight_bounds OY2' /\ + bounded_by tight_bounds OZ' /\ + m' =* (FElem OX1K OX1') * (FElem OY1K OY1') * + (FElem OX2K OX2') * (FElem OY2K OY2') * (FElem OZK OZ') * + (FElem X1K X1) * (FElem Y1K Y1) * R + }. + + Global Instance spec_of_tplu : spec_of "secp256k1_tplu" := + fnspec! "secp256k1_tplu" + (OX1K OY1K OX2K OY2K OZK X1K Y1K : word) / + (OX1 OY1 OX2 OY2 OZ X1 Y1 : felem) (P : point) + (HPaff : z_of P = F.one) (R : _ -> Prop), + { requires t m := + (exists z, proj1_sig P = ((feval X1), (feval Y1), z)) /\ + bounded_by loose_bounds X1 /\ + bounded_by loose_bounds Y1 /\ + m =* (FElem OX1K OX1) * (FElem OY1K OY1) * + (FElem OX2K OX2) * (FElem OY2K OY2) * (FElem OZK OZ) * + (FElem X1K X1) * (FElem Y1K Y1) * R; + ensures t' m' := + t = t' /\ + exists OX1' OY1' OX2' OY2' OZ', + proj1_sig (fst (tplu P HPaff)) = ((feval OX1'), (feval OY1'), (feval OZ')) /\ + proj1_sig (snd (tplu P HPaff)) = ((feval OX2'), (feval OY2'), (feval OZ')) /\ + bounded_by tight_bounds OX1' /\ + bounded_by tight_bounds OY1' /\ + bounded_by tight_bounds OX2' /\ + bounded_by tight_bounds OY2' /\ + bounded_by tight_bounds OZ' /\ + m' =* (FElem OX1K OX1') * (FElem OY1K OY1') * + (FElem OX2K OX2') * (FElem OY2K OY2') * (FElem OZK OZ') * + (FElem X1K X1) * (FElem Y1K Y1) * R + }. + + Global Instance spec_of_zdau : spec_of "secp256k1_zdau" := + fnspec! "secp256k1_zdau" + (X1K Y1K X2K Y2K ZK : word) / + (X1 Y1 X2 Y2 Z : felem) (P Q : point) + (HPQ : co_z P Q) (R : _ -> Prop), + { requires t m := + proj1_sig P = ((feval X1), (feval Y1), (feval Z)) /\ + proj1_sig Q = ((feval X2), (feval Y2), (feval Z)) /\ + bounded_by loose_bounds X1 /\ + bounded_by loose_bounds Y1 /\ + bounded_by loose_bounds X2 /\ + bounded_by loose_bounds Y2 /\ + bounded_by loose_bounds Z /\ + m =* (FElem X1K X1) * (FElem Y1K Y1) * + (FElem X2K X2) * (FElem Y2K Y2) * (FElem ZK Z) * R; + ensures t' m' := + t = t' /\ + exists OX1 OY1 OX2 OY2 OZ, + proj1_sig (fst (zdau P Q HPQ)) = ((feval OX1), (feval OY1), (feval OZ)) /\ + proj1_sig (snd (zdau P Q HPQ)) = ((feval OX2), (feval OY2), (feval OZ)) /\ + bounded_by tight_bounds OX1 /\ + bounded_by tight_bounds OY1 /\ + bounded_by tight_bounds OX2 /\ + bounded_by tight_bounds OY2 /\ + bounded_by tight_bounds OZ /\ + m' =* (FElem X1K OX1) * (FElem Y1K OY1) * + (FElem X2K OX2) * (FElem Y2K OY2) * (FElem ZK OZ) * R }. Local Instance spec_of_secp256k1_opp : spec_of "secp256k1_opp" := Field.spec_of_UnOp un_opp. Local Instance spec_of_secp256k1_square : spec_of "secp256k1_square" := Field.spec_of_UnOp un_square. Local Instance spec_of_secp256k1_mul : spec_of "secp256k1_mul" := Field.spec_of_BinOp bin_mul. Local Instance spec_of_secp256k1_add : spec_of "secp256k1_add" := Field.spec_of_BinOp bin_add. - Local Instance spec_of_secp256k1_sub : spec_of "secp256k1_sub" := Field.spec_of_BinOp bin_carry_sub. + Local Instance spec_of_secp256k1_sub : spec_of "secp256k1_sub" := Field.spec_of_BinOp bin_sub. Local Instance spec_of_secp256k1_felem_copy : spec_of "secp256k1_felem_copy" := Field.spec_of_felem_copy. Local Arguments word.rep : simpl never. @@ -170,11 +501,8 @@ Section WithParameters. cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds]. Local Ltac solve_bounds := - repeat match goal with - | H: bounded_by loose_bounds ?x |- bounded_by loose_bounds ?x => apply H - | H: bounded_by tight_bounds ?x |- bounded_by tight_bounds ?x => apply H - | H: bounded_by tight_bounds ?x |- bounded_by loose_bounds ?x => apply relax_bounds - | H: bounded_by _ ?x |- bounded_by _ ?x => cbv_bounds H + match goal with + | H: bounded_by _ ?x |- bounded_by _ ?x => apply H end. Local Ltac solve_stack := @@ -191,39 +519,281 @@ Section WithParameters. Local Ltac single_step := repeat straightline; straightline_call; ssplit; try solve_mem; try solve_bounds; try solve_stack. - Lemma zaddu_ok : program_logic_goal_for_function! secp256k1_zaddu. + 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]. - Compute felem_copy. - single_step. + + do 3 single_step. + repeat straightline. + + exists X, x, Z; ssplit. 2-4:solve_bounds. + cbv [bin_model bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_model un_square] in *. + cbv match beta delta [jopp proj1_sig fst snd]. + destruct P; cbv [proj1_sig] in H2. + rewrite H2; cbv match zeta. rewrite H10. reflexivity. + + ecancel_assumption. + Qed. + + Add Ring Private_ring : (F.ring_theory M_pos) (morphism (F.ring_morph M_pos), constants [F.is_constant]). + + Lemma secp256k1_make_co_z_ok : program_logic_goal_for_function! secp256k1_make_co_z. + Proof. + Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds]. + + do 4 single_step. + repeat straightline. + + cbv [FElem] in *. + match goal with + | |- context [anybytes ?a _ _] => + match goal with + | H: _ ?a' |- context [map.split ?a' _ _] => + seprewrite_in (@Bignum.Bignum_to_bytes _ _ _ _ _ _ felem_size_in_words a) H + end + end. + extract_ex1_and_emp_in H26. repeat straightline. - eapply Proper_call; cycle -1; - [ | try eabstract (solve [ Morphisms.solve_proper ]).. ]; - [ .. | intros ? ? ? ? ]. - eapply H12. + exists x3, x5; ssplit. 2-3:solve_bounds. + cbv [bin_model bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_model un_square] in *. + cbv match beta delta [make_co_z proj1_sig fst snd]. + destruct P; destruct Q; cbv [proj1_sig] in H3, H4. + rewrite H3, H4; cbv match zeta. + repeat match goal with + | H: feval ?x = _ |- context [feval ?x] => rewrite H + end. + rewrite F.pow_2_r in *; repeat (apply pair_equal_spec; split); ring. + + ecancel_assumption. + Qed. + + Lemma secp256k1_zaddu_ok : program_logic_goal_for_function! secp256k1_zaddu. + Proof. + Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds]. + + do 14 single_step. + do 4 single_step. + + repeat straightline. + (* Rewrites the FElems for the stack to be about bytes instead *) + cbv [FElem] in *. + repeat match goal with + | |- context [anybytes ?a _ _] => + match goal with + | H: _ ?a' |- context [map.split ?a' _ _] => + seprewrite_in (@Bignum.Bignum_to_bytes _ _ _ _ _ _ felem_size_in_words a) H + end + end. + extract_ex1_and_emp_in H92. + (* Solve stack/memory stuff *) + repeat straightline. + (* Post-conditions *) + exists x7,x12,x2,x9,x0; ssplit. 3-7:solve_bounds. + (* Correctness: result matches Gallina *) + 1,2: cbv [bin_model bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_model un_square] in *. + 1,2: cbv match beta delta [zaddu proj1_sig fst snd]. + 1,2: destruct P; destruct Q; cbv [proj1_sig] in H17, H18. + 1,2: rewrite H17, H18; cbv match zeta. + 1,2: rewrite F.pow_2_r in *; congruence. - eapply Proper_call; [try eabstract (solve [ Morphisms.solve_proper ]).. |]. - intros ? ? ? ?. eexists. split. cbv. + ecancel_assumption. + Qed. + Lemma secp256k1_zaddc_ok: program_logic_goal_for_function! secp256k1_zaddc. + Proof. + Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds]. - unfold program_logic_goal_for. intros. - unfold spec_of_zaddu. intros. eapply Proper_call; cycle -1. - eapply start_func; eauto. unfold func. - + do 25 single_step. + do 4 single_step. + repeat straightline. + cbv [FElem] in *. + repeat match goal with + | |- context [anybytes ?a _ _] => + match goal with + | H: _ ?a' |- context [map.split ?a' _ _] => + seprewrite_in (@Bignum.Bignum_to_bytes _ _ _ _ _ _ felem_size_in_words a) H + end + end. + extract_ex1_and_emp_in H140. repeat straightline. - eapply Proper_call; cycle -1. - unfold call. - eapply spec_of_secp256k1_sub. + exists x11,x23,x7,x19,x0; ssplit. 3-7:solve_bounds. + 1,2: cbv [bin_model bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_model un_square] in *. + 1,2: cbv match beta delta [zaddc proj1_sig fst snd]. + 1,2: destruct P; destruct Q; cbv [proj1_sig] in H28, H29. + 1,2: rewrite H28, H29; cbv match zeta. + 1,2: rewrite F.pow_2_r in *; congruence. - straightline_call. + ecancel_assumption. + Qed. + + Lemma secp256k1_dblu_ok: program_logic_goal_for_function! secp256k1_dblu. + Proof. + Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds]. + + do 9 single_step. single_step. + seprewrite_in (Bignum.Bignum_of_bytes 8 a4) H72; [ trivial | ]; + 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 ]). + do 11 single_step. + do 4 single_step. + + repeat straightline. + cbv [FElem] in *. + repeat match goal with + | |- context [anybytes ?a _ _] => + match goal with + | H: _ ?a' |- context [map.split ?a' _ _] => + seprewrite_in (@Bignum.Bignum_to_bytes _ _ _ _ _ _ felem_size_in_words a) H + end + end. + extract_ex1_and_emp_in H114. + + repeat straightline. + exists x13,x19,x8,x16,x0; ssplit. 3-7:solve_bounds. + 1,2: cbv [bin_model bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_model un_square] in *. + 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,3: repeat match goal with + | H: feval ?x = _ |- context [feval ?x] => rewrite H + end; ring. + + ecancel_assumption. + Qed. + + Lemma secp256k1_tplu_ok: program_logic_goal_for_function! secp256k1_tplu. + 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|] + 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. + cancel_seps_at_indices 4%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 3%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 2%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 1%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 0%nat 0%nat; [reflexivity|]. + solve [ecancel]. + + repeat straightline. + eapply Proper_call; cycle -1; [eapply H0|try eabstract (solve [ Morphisms.solve_proper ])..]; [ .. | intros ? ? ? ? ]. + ssplit; [exact H28|exact H27|..]; try solve_bounds. + ecancel_assumption. + + repeat straightline. + cbv [FElem] in *. + repeat match goal with + | |- context [anybytes ?a _ _] => + match goal with + | H: _ ?a' |- context [map.split ?a' _ _] => + seprewrite_in (@Bignum.Bignum_to_bytes _ _ _ _ _ _ felem_size_in_words a) H + end + end. + extract_ex1_and_emp_in H42. + + repeat straightline. + exists x5,x6,x7,x8,x9; ssplit. 3-7:solve_bounds. + exact H35. exact H36. + + ecancel_assumption. + Qed. + + Lemma secp256k1_zdau_ok: program_logic_goal_for_function! secp256k1_zdau. + Proof. + Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds]. + + do 43 single_step. + + repeat straightline. + cbv [FElem] in *. + repeat match goal with + | |- context [anybytes ?a _ _] => + match goal with + | H: _ ?a' |- context [map.split ?a' _ _] => + seprewrite_in (@Bignum.Bignum_to_bytes _ _ _ _ _ _ felem_size_in_words a) H + end + end. + extract_ex1_and_emp_in H208. + + repeat straightline. + exists x33,x36,x38,x41,x23; ssplit. 3-7:solve_bounds. + 1,2: cbv [bin_model bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_model un_square] in *. + 1,2: cbv match beta delta [zdau proj1_sig fst snd]. + 1,2: destruct P; destruct Q; cbv [proj1_sig] in H42, H43. + 1,2: rewrite H42, H43; cbv match zeta. + 1,2: rewrite F.pow_2_r in *; congruence. + ecancel_assumption. + Qed. +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_jopp; *) +(* secp256k1_make_co_z; *) +(* secp256k1_felem_cswap; *) +(* secp256k1_zaddu; *) +(* secp256k1_zaddc; *) +(* secp256k1_dblu; *) +(* secp256k1_tplu; *) +(* secp256k1_zdau]. *) -Compute (ToCString.c_func ("ZADDU", ZADDU)). +(* Compute (ToCString.c_module funcs). *) From 7eda4aa551732480a78549f838f96c098b21ce22 Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Fri, 26 Apr 2024 22:53:40 +0200 Subject: [PATCH 04/10] Bedrock2 WordByWordMontgomery felem_copy_func_correct --- .../Synthesis/New/WordByWordMontgomery.v | 42 ++++++++++++++++++- 1 file changed, 41 insertions(+), 1 deletion(-) diff --git a/src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v b/src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v index 2ddae62112..fe61c358b8 100644 --- a/src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v +++ b/src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v @@ -55,6 +55,10 @@ Class word_by_word_Montgomery_ops (WordByWordMontgomery.square m width) Field.square list_unop_insizes list_unop_outsizes (list_unop_inlengths n); + felem_copy_op : + computed_op + (WordByWordMontgomery.copy m width) Field.felem_copy + list_unop_insizes list_unop_outsizes (list_unop_inlengths n); from_bytes_op : computed_op (WordByWordMontgomery.from_bytes m width) @@ -165,13 +169,14 @@ Section WordByWordMontgomery. (to_mont : string) (ops : word_by_word_Montgomery_ops n m) mul_func add_func sub_func opp_func square_func - from_bytes_func to_bytes_func + felem_copy_func from_bytes_func to_bytes_func from_mont_func to_mont_func select_znz_func (mul_func_eq : mul_func = b2_func mul_op) (add_func_eq : add_func = b2_func add_op) (sub_func_eq : sub_func = b2_func sub_op) (opp_func_eq : opp_func = b2_func opp_op) (square_func_eq : square_func = b2_func square_op) + (felem_copy_func_eq : felem_copy_func = b2_func felem_copy_op) (from_bytes_func_eq : from_bytes_func = b2_func from_bytes_op) (to_bytes_func_eq : to_bytes_func = b2_func to_bytes_op) (from_mont_func_eq : from_mont_func = b2_func from_mont_op) @@ -492,6 +497,41 @@ Qed. intros. apply Hcorrect; auto. } Qed. + Lemma list_Z_bounded_by_unsigned (xs : list (@Interface.word.rep _ word)) : + list_Z_bounded_by + (Primitives.saturated_bounds (List.length xs) width) + (map Interface.word.unsigned xs). + Proof using parameters_sentinel ok. + induction xs; cbn; [reflexivity|]. + eapply list_Z_bounded_by_cons; split; [|assumption]. + eapply Bool.andb_true_iff; split; eapply Z.leb_le; + cbv [Primitives.word_bound]; cbn. + { eapply Properties.word.unsigned_range. } + { eapply Le.Z.le_sub_1_iff, Properties.word.unsigned_range. } + Qed. + + Lemma felem_copy_func_correct : + valid_func (res felem_copy_op _) -> + forall functions, + Interface.map.get functions Field.felem_copy = Some felem_copy_func -> + (@spec_of_felem_copy _ _ _ _ _ _ _ field_representation_raw) functions. + Proof using M_eq check_args_ok felem_copy_func_eq ok. + cbv [spec_of_felem_copy]. rewrite felem_copy_func_eq. intros. + pose proof copy_correct + _ _ _ ltac:(eassumption) _ (res_eq felem_copy_op) + as Hcorrect. + + eapply felem_copy_correct; [ .. | eassumption | eassumption ]; + repeat handle_side_conditions; [ | ]; intros. + { (* output *value* is correct *) + unshelve erewrite (proj1 (Hcorrect _ _)); cycle 1. + { rewrite map_map, List.map_ext_id; trivial; intros. + rewrite ?Word.Interface.word.of_Z_unsigned; trivial. } + { rewrite <- H2. exact (list_Z_bounded_by_unsigned x0). } } + { (* output *bounds* are correct *) + intros. apply Hcorrect; auto. } + Qed. + Lemma from_bytes_func_correct : valid_func (res from_bytes_op _) -> forall functions, From bade6e14d45dc3e5ef34e067cefc9a55ad8576fa Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Fri, 26 Apr 2024 23:05:53 +0200 Subject: [PATCH 05/10] secp256k1 scalarmult wip --- src/Bedrock/End2End/Secp256k1/JoyeLadder.v | 107 +++++++++++++++++++++ 1 file changed, 107 insertions(+) create mode 100644 src/Bedrock/End2End/Secp256k1/JoyeLadder.v diff --git a/src/Bedrock/End2End/Secp256k1/JoyeLadder.v b/src/Bedrock/End2End/Secp256k1/JoyeLadder.v new file mode 100644 index 0000000000..453c4f119d --- /dev/null +++ b/src/Bedrock/End2End/Secp256k1/JoyeLadder.v @@ -0,0 +1,107 @@ +Require Import bedrock2.Array. +Require Import bedrock2.FE310CSemantics. +Require Import bedrock2.Loops. +Require Import bedrock2.Map.Separation. +Require Import bedrock2.Map.SeparationLogic. +Require Import bedrock2.NotationsCustomEntry. +Require Import bedrock2.ProgramLogic. +Require Import bedrock2.Scalars. +Require Import bedrock2.Semantics. +Require Import bedrock2.Syntax. +Require Import bedrock2.WeakestPrecondition. +Require Import bedrock2.WeakestPreconditionProperties. +Require Import bedrock2.ZnWords. +Require Import compiler.MMIO. +Require Import compiler.Pipeline. +Require Import compiler.Symbols. +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.Bitwidth. +Require Import coqutil.Word.Interface. +Require Import Coq.Init.Byte. +Require Import Coq.Lists.List. +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Bedrock.Field.Interface.Compilation2. +Require Import Crypto.Bedrock.Field.Synthesis.New.WordByWordMontgomery. +Require Import Crypto.Bedrock.Group.ScalarMult.CSwap. +Require Import Crypto.Bedrock.End2End.Secp256k1.Field256k1. +Require Import Crypto.Bedrock.End2End.Secp256k1.JacobianCoZ. +Require Import Crypto.Bedrock.Specs.Field. +Require Import Crypto.Util.Decidable. +Require Import Curves.Weierstrass.Jacobian.Jacobian. +Require Import Curves.Weierstrass.Jacobian.CoZ. +Require Import Curves.Weierstrass.Jacobian.ScalarMult. +Require Import Lia. +Require Crypto.Bedrock.Field.Synthesis.New.Signature. +Local Open Scope string_scope. +Local Open Scope Z_scope. +Import LittleEndianList. +Import ListNotations. +Import ProgramLogic.Coercions. +Import WeakestPrecondition. + +Local Existing Instance field_parameters. +Local Instance frep256k1 : Field.FieldRepresentation := field_representation Field256k1.m. +Local Existing Instance frep256k1_ok. + +Definition laddermul := + func! (oX, oY, oZ, k, X, Y) { + i = coq:(2); + swap = (load1(k+coq:(1)>>coq:(3))>>(coq:(1)&coq:(7)))&coq:(1); + stackalloc 32 as X0; + stackalloc 32 as Y0; + stackalloc 32 as X1; + stackalloc 32 as Y1; + stackalloc 32 as Z; + secp256k1_tplu(X1, Y1, X0, Y0, Z, X, Y); + secp256k1_felem_cswap(swap, X0, X1); + secp256k1_felem_cswap(swap, Y0, Y1); + while (i < coq:(256)) { + swap = (load1(k+i>>coq:(3))>>(i&coq:(7)))&coq:(1); + secp256k1_felem_cswap(swap, X0, X1); + secp256k1_felem_cswap(swap, Y0, Y1); + secp256k1_zdau(X1, Y1, X0, Y0, Z); + secp256k1_felem_cswap(swap, X0, X1); + secp256k1_felem_cswap(swap, Y0, Y1); + i = i+coq:(1) + }; + stackalloc 32 as tX; + stackalloc 32 as tY; + secp256k1_make_co_z(tX, tY, X, Y, Z); + secp256k1_opp(tY, tY); + secp256k1_zaddu(X1, Y1, oX, oY, oZ, X0, Y0, tX, tY, Z); + swap = (load1(k+coq:(0)>>coq:(3))>>(coq:(0)&coq:(7)))&coq:(1); + secp256k1_felem_cswap(swap, oX, X1); + secp256k1_felem_cswap(swap, oY, Y1) +}. + +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_zaddc; *) + secp256k1_dblu; + secp256k1_tplu; + secp256k1_zdau; + laddermul]. + +Compute (ToCString.c_module funcs). + From 08b3424c09c7fe774167fe949ae8157e9b7938dd Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Thu, 2 May 2024 16:00:33 +0200 Subject: [PATCH 06/10] secp256k1_inv using addchain --- src/Bedrock/End2End/Secp256k1/Addchain.v | 390 +++++++++++++++++++++++ 1 file changed, 390 insertions(+) create mode 100644 src/Bedrock/End2End/Secp256k1/Addchain.v diff --git a/src/Bedrock/End2End/Secp256k1/Addchain.v b/src/Bedrock/End2End/Secp256k1/Addchain.v new file mode 100644 index 0000000000..ed5742df8f --- /dev/null +++ b/src/Bedrock/End2End/Secp256k1/Addchain.v @@ -0,0 +1,390 @@ +Require Import bedrock2.Array. +Require Import bedrock2.FE310CSemantics. +Require Import bedrock2.Loops. +Require Import bedrock2.Map.Separation. +Require Import bedrock2.Map.SeparationLogic. +Require Import bedrock2.NotationsCustomEntry. +Require Import bedrock2.ProgramLogic. +Require Import bedrock2.Scalars. +Require Import bedrock2.Semantics. +Require Import bedrock2.Syntax. +Require Import bedrock2.WeakestPrecondition. +Require Import bedrock2.WeakestPreconditionProperties. +Require Import bedrock2.ZnWords. +Require Import compiler.MMIO. +Require Import compiler.Pipeline. +Require Import compiler.Symbols. +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.Bitwidth. +Require Import coqutil.Word.Interface. +Require Import Coq.Init.Byte. +Require Import Coq.Lists.List. +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Bedrock.Field.Interface.Compilation2. +Require Import Crypto.Bedrock.Field.Synthesis.New.WordByWordMontgomery. +Require Import Crypto.Bedrock.Group.ScalarMult.CSwap. +Require Import Crypto.Bedrock.End2End.Secp256k1.Field256k1. +Require Import Crypto.Bedrock.Specs.Field. +Require Import Crypto.Arithmetic.FLia. +Require Import Crypto.Algebra.Hierarchy. +Require Import Numbers.DecimalString. +Require Import Crypto.Util.Decidable. +Require Import Lia. +Require Crypto.Bedrock.Field.Synthesis.New.Signature. +Local Open Scope string_scope. +Local Open Scope Z_scope. +Import LittleEndianList. +Import ListNotations. +Import ProgramLogic.Coercions. +Import WeakestPrecondition. + +(* +addchain: expr: "2^256 - 2^32 - 977 - 2" +addchain: hex: fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2d +addchain: dec: 115792089237316195423570985008687907853269984665640564039457584007908834671661 +addchain: best: opt(dictionary(hybrid(3,0),continued_fractions(dichotomic))) +addchain: cost: 270 +*) +(* +tmp t0 t1 t2 t3 t4 +double t0 x +double z t0 +add z x z +add t1 t0 z +double t0 t1 +shift t2 t0 2 +add t2 t1 t2 +shift t2 t2 4 +add t0 t0 t2 +shift t2 t0 2 +add t2 t1 t2 +shift t2 t2 10 +add t0 t0 t2 +add t0 x t0 +double t3 t0 +shift t2 t3 2 +shift t4 t2 22 +add t2 t2 t4 +shift t4 t2 20 +add t3 t3 t4 +shift t3 t3 46 +add t2 t2 t3 +shift t3 t2 110 +add t2 t2 t3 +add t1 t1 t2 +shift t1 t1 23 +add t0 t0 t1 +shift t0 t0 7 +add t0 z t0 +shift t0 t0 3 +add z z t0 +*) + +Local Existing Instance field_parameters. +Local Instance frep256k1 : Field.FieldRepresentation := field_representation Field256k1.m. +Local Existing Instance frep256k1_ok. + +(* TODO: This could probably be automated *) + +(* Renders program way too long for the program logic to handle. *) +(* Unroll the loop *) +(* Fixpoint secp256k1_shift x y n := *) +(* match n with *) +(* | O => cmd.skip *) +(* | S n => (cmd.seq bedrock_cmd:(secp256k1_square(coq:(expr.var x), coq:(expr.var y))) *) +(* bedrock_cmd:(coq:(secp256k1_shift x x n))) *) +(* end. *) + +(* Peel off one iteration in all cases. *) +Definition secp256k1_shift x y (n: nat) := + cmd.seq bedrock_cmd:(secp256k1_square(coq:(expr.var x), coq:(expr.var y))) + (cmd.seq bedrock_cmd:(i = $1) + bedrock_cmd:(while (i < coq:(n)) { + secp256k1_square(coq:(expr.var x), coq:(expr.var x)); + i = i + $1 + })). + +Definition secp256k1_inv := + func! (z, x) { + stackalloc 32 as t0; + stackalloc 32 as t1; + stackalloc 32 as t2; + stackalloc 32 as t3; + stackalloc 32 as t4; + secp256k1_square(t0, x); (* double t0 x *) + secp256k1_square(z, t0); (* double z t0 *) + secp256k1_mul(z, x, z); (* add z x z *) + secp256k1_mul(t1, t0, z); (* add t1 t0 z *) + secp256k1_square(t0, t1); (* double t0 t1 *) + coq:(secp256k1_shift "t2" "t0" 2); (* shift t2 t0 2 *) + secp256k1_mul(t2, t1, t2); (* add t2 t1 t2 *) + coq:(secp256k1_shift "t2" "t2" 4); (* shift t2 t2 4 *) + secp256k1_mul(t0, t0, t2); (* add t0 t0 t2 *) + coq:(secp256k1_shift "t2" "t0" 2); (* shift t2 t0 2 *) + secp256k1_mul(t2, t1, t2); (* add t2 t1 t2 *) + coq:(secp256k1_shift "t2" "t2" 10); (* shift t2 t2 10 *) + secp256k1_mul(t0, t0, t2); (* add t0 t0 t2 *) + secp256k1_mul(t0, x, t0); (* add t0 x t0 *) + secp256k1_square(t3, t0); (* double t3 t0 *) + coq:(secp256k1_shift "t2" "t3" 2); (* shift t2 t3 2 *) + coq:(secp256k1_shift "t4" "t2" 22); (* shift t4 t2 22 *) + secp256k1_mul(t2, t2, t4); (* add t2 t2 t4 *) + coq:(secp256k1_shift "t4" "t2" 20); (* shift t4 t2 20 *) + secp256k1_mul(t3, t3, t4); (* add t3 t3 t4 *) + coq:(secp256k1_shift "t3" "t3" 46); (* shift t3 t3 46 *) + secp256k1_mul(t2, t2, t3); (* add t2 t2 t3 *) + coq:(secp256k1_shift "t3" "t2" 110);(* shift t3 t2 110 *) + secp256k1_mul(t2, t2, t3); (* add t2 t2 t3 *) + secp256k1_mul(t1, t1, t2); (* add t1 t1 t2 *) + coq:(secp256k1_shift "t1" "t1" 23); (* shift t1 t1 23 *) + secp256k1_mul(t0, t0, t1); (* add t0 t0 t1 *) + coq:(secp256k1_shift "t0" "t0" 7); (* shift t0 t0 7 *) + secp256k1_mul(t0, z, t0); (* add t0 z t0 *) + coq:(secp256k1_shift "t0" "t0" 3); (* shift t0 t0 3 *) + secp256k1_mul(z, z, t0) (* add z z t0 *) +}. + +(* Compute ToCString.c_func ("secp256k1_inv", secp256k1_inv). *) + +Section WithParameters. + Context {two_lt_M: 2 < M_pos}. + 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 {secp256k1_prime: prime m}. + Context {F_M_pos : Z.pos M_pos = m}. + + 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 felem := (felem(FieldRepresentation:=frep256k1)). + + Local Instance spec_of_secp256k1_square : spec_of "secp256k1_square" := Field.spec_of_UnOp un_square. + Local Instance spec_of_secp256k1_mul : spec_of "secp256k1_mul" := Field.spec_of_BinOp bin_mul. + + Global Instance spec_of_inv : spec_of "secp256k1_inv" := + fnspec! "secp256k1_inv" + (zK xK : word) / (z x : felem) (vx : F M_pos) (R : _ -> Prop), + { requires t m := + vx = feval x /\ + bounded_by loose_bounds x /\ + m =* (FElem zK z) * (FElem xK x) * R; + ensures t' m' := + t = t' /\ + exists z', + feval z' = (F.pow vx (2^256 - 2^32 - 977 - 2)) /\ + bounded_by tight_bounds z' /\ + m' =* (FElem zK z') * (FElem xK x) * R + }. + + Local Arguments word.rep : simpl never. + Local Arguments word.wrap : simpl never. + Local Arguments word.unsigned : simpl never. + Local Arguments word.of_Z : simpl never. + + Local Ltac solve_mem := + repeat match goal with + | |- exists _ : _ -> Prop, _%sep _ => eexists + | |- _%sep _ => ecancel_assumption + end. + + Local Ltac cbv_bounds H := + cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds] in H; + cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds]. + + Local Ltac solve_bounds := + match goal with + | H: bounded_by _ ?x |- bounded_by _ ?x => apply H + end. + + Local Ltac solve_stack := + (* Rewrites the `stack$@a` term in H to use a Bignum instead *) + 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 + end; + [> transitivity 32%nat; trivial | ]; + (* proves the memory matches up *) + use_sep_assumption; cancel; cancel_seps_at_indices 0%nat 0%nat; cbn; [> trivial | eapply RelationClasses.reflexivity]. + + Local Ltac single_step := + repeat straightline; straightline_call; ssplit; try solve_mem; try solve_bounds; try solve_stack. + + Lemma spec_of_shift functions tr mem loc post : + forall var to (Hvar: var <> "i") (Hto: 2 <= to < 2^32) pvar vvar R, + spec_of_secp256k1_square functions -> + map.get loc var = Some pvar -> + (FElem pvar vvar * R)%sep mem -> + bounded_by un_outbounds vvar -> + (forall tr' mem' loc', + (tr' = tr /\ + loc' = map.put loc "i" (word.of_Z to) /\ + exists vvar', + (FElem pvar vvar' * R)%sep mem' /\ + feval vvar' = F.pow (feval vvar) (N.pow 2%N (Z.to_N (to - 1))) /\ + bounded_by un_outbounds vvar') -> + post tr' mem' loc' + ) -> + cmd functions + bedrock_func_body:( + {$"i" = coq:(expr.literal 1)}; + while coq:(expr.var "i") < coq:(expr.literal to) { + {$"secp256k1_square"(coq:(expr.var var), coq:(expr.var var))}; + $"i" = coq:(expr.var "i") + coq:(expr.literal 1) + }) 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 /\ + exists i (Hi: 1 <= i <= to), + v = Z.to_nat (to - i) /\ + (* TODO: automate how to recover the frame *) + (exists vx, ((FElem pvar vx) * R)%sep m /\ + feval vx = F.pow (feval vvar) (N.pow 2%N (Z.to_N (i - 1))) /\ + bounded_by un_outbounds vx) /\ + l = map.put loc "i" (word.of_Z i)). + eapply wp_while. exists nat, lt, inv. ssplit; [eapply lt_wf|..]. + eexists. unfold inv; ssplit; [reflexivity|..]. + exists 1. exists (ltac:(lia): 1 <= 1 <= to). ssplit; [reflexivity|..]. + eexists. ssplit. + ecancel_assumption. rewrite F.pow_1_r. reflexivity. auto. + reflexivity. + intros fuel * Hinv. + destruct Hinv as (-> & vi & Hvi & -> & Hmem & ->). + eexists ?[b]; ssplit. + eexists; split; [apply map.get_put_same|]. + eapply Core.WeakestPrecondition_dexpr_expr; [|apply ExprCompiler.expr_compile_Z_literal]. + cbn. rewrite <- Core.word.morph_ltu by lia. + reflexivity. + all: pose proof Zlt_cases vi to; + intros Hnz; destruct (vi rewrite H + end. cbv [un_model un_square]. + rewrite F.pow_pow_l, N.mul_comm, <- N.pow_succ_r', <- Z2N.inj_succ. + f_equal. f_equal. lia. lia. auto. + unfold l'. rewrite <- word.ring_morph_add, map.put_put_same. reflexivity. + lia. assert (vi = to) as -> by lia. + destruct Hmem as (? & ? & ? & ?). + apply H3. + ssplit; [reflexivity|reflexivity|]. + eexists; ssplit; eassumption. + Qed. + + Lemma secp256k1_inv_ok : program_logic_goal_for_function! secp256k1_inv. + Proof. + Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds]. + + repeat single_step. + destruct H64 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + destruct H82 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + destruct H91 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + destruct H100 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + destruct H109 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + destruct H124 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + destruct H130 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + destruct H139 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + destruct H148 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + destruct H157 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + destruct H169 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + destruct H178 as (-> & -> & ? & ? & ? & ?). + eexists; split; [reflexivity|]. + eapply spec_of_shift. congruence. lia. auto. reflexivity. + ecancel_assumption. eassumption. + repeat single_step. + + repeat straightline. + cbv [FElem] in *. + repeat match goal with + | |- context [anybytes ?a _ _] => + match goal with + | H: _ ?a' |- context [map.split ?a' _ _] => + seprewrite_in (@Bignum.Bignum_to_bytes _ _ _ _ _ _ felem_size_in_words a) H + end + end. + extract_ex1_and_emp_in H194. + + repeat straightline. + exists x42. ssplit; [|solve_bounds|ecancel_assumption]. + repeat match goal with + | H : feval ?a = _ |- context [feval ?a] => rewrite H + end. + cbv [un_model bin_model un_square bin_mul]. + unfold vx. + repeat match goal with + | |- context [F.pow (F.pow (feval x) ?a) ?b] => rewrite (F.pow_pow_l (feval x) a b) + | |- context [F.mul (feval x) (F.pow (feval x) ?n)] => rewrite <- (F.pow_succ_r (feval x) n) + | |- context [F.mul (F.pow (feval x) ?n1) (F.pow (feval x) ?n2)] => rewrite <- (F.pow_add_r (feval x) n1 n2) + end. + f_equal. + Qed. + +End WithParameters. + + From 08b5bdeb2f617e68ec4e4f95e1c2797dfffae77e Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Thu, 2 May 2024 16:50:05 +0200 Subject: [PATCH 07/10] Change spec_of_secp256k1_inv to make F.inv appear --- src/Bedrock/End2End/Secp256k1/Addchain.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Bedrock/End2End/Secp256k1/Addchain.v b/src/Bedrock/End2End/Secp256k1/Addchain.v index ed5742df8f..404364cfcd 100644 --- a/src/Bedrock/End2End/Secp256k1/Addchain.v +++ b/src/Bedrock/End2End/Secp256k1/Addchain.v @@ -181,7 +181,7 @@ Section WithParameters. ensures t' m' := t = t' /\ exists z', - feval z' = (F.pow vx (2^256 - 2^32 - 977 - 2)) /\ + feval z' = (F.inv vx) /\ bounded_by tight_bounds z' /\ m' =* (FElem zK z') * (FElem xK x) * R }. @@ -376,7 +376,8 @@ Section WithParameters. | H : feval ?a = _ |- context [feval ?a] => rewrite H end. cbv [un_model bin_model un_square bin_mul]. - unfold vx. + unfold vx. rewrite (@F.Fq_inv_fermat _ _ two_lt_M). + rewrite F_M_pos. repeat match goal with | |- context [F.pow (F.pow (feval x) ?a) ?b] => rewrite (F.pow_pow_l (feval x) a b) | |- context [F.mul (feval x) (F.pow (feval x) ?n)] => rewrite <- (F.pow_succ_r (feval x) n) From ad9b3f1eec5bd6e1cf1d929972a3e9dead27a720 Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Thu, 2 May 2024 16:51:15 +0200 Subject: [PATCH 08/10] update unverified secp256k1 ladder --- src/Bedrock/End2End/Secp256k1/JoyeLadder.v | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/Bedrock/End2End/Secp256k1/JoyeLadder.v b/src/Bedrock/End2End/Secp256k1/JoyeLadder.v index 453c4f119d..e2a65a1613 100644 --- a/src/Bedrock/End2End/Secp256k1/JoyeLadder.v +++ b/src/Bedrock/End2End/Secp256k1/JoyeLadder.v @@ -31,6 +31,7 @@ Require Import Crypto.Bedrock.Field.Synthesis.New.WordByWordMontgomery. Require Import Crypto.Bedrock.Group.ScalarMult.CSwap. Require Import Crypto.Bedrock.End2End.Secp256k1.Field256k1. Require Import Crypto.Bedrock.End2End.Secp256k1.JacobianCoZ. +Require Import Crypto.Bedrock.End2End.Secp256k1.Addchain. Require Import Crypto.Bedrock.Specs.Field. Require Import Crypto.Util.Decidable. Require Import Curves.Weierstrass.Jacobian.Jacobian. @@ -49,8 +50,8 @@ Local Existing Instance field_parameters. Local Instance frep256k1 : Field.FieldRepresentation := field_representation Field256k1.m. Local Existing Instance frep256k1_ok. -Definition laddermul := - func! (oX, oY, oZ, k, X, Y) { +Definition secp256k1_laddermul := + func! (oX, oY, k, X, Y) { i = coq:(2); swap = (load1(k+coq:(1)>>coq:(3))>>(coq:(1)&coq:(7)))&coq:(1); stackalloc 32 as X0; @@ -58,6 +59,7 @@ Definition laddermul := stackalloc 32 as X1; stackalloc 32 as Y1; stackalloc 32 as Z; + stackalloc 32 as oZ; secp256k1_tplu(X1, Y1, X0, Y0, Z, X, Y); secp256k1_felem_cswap(swap, X0, X1); secp256k1_felem_cswap(swap, Y0, Y1); @@ -77,7 +79,10 @@ Definition laddermul := secp256k1_zaddu(X1, Y1, oX, oY, oZ, X0, Y0, tX, tY, Z); swap = (load1(k+coq:(0)>>coq:(3))>>(coq:(0)&coq:(7)))&coq:(1); secp256k1_felem_cswap(swap, oX, X1); - secp256k1_felem_cswap(swap, oY, Y1) + secp256k1_felem_cswap(swap, oY, Y1); + secp256k1_inv(Z, oZ); + secp256k1_mul(oX, oX, Z); + secp256k1_mul(oY, oY, Z) }. Require Import bedrock2.ToCString. @@ -97,11 +102,11 @@ Definition funcs := &[,secp256k1_make_co_z; secp256k1_felem_cswap; secp256k1_zaddu; - (* secp256k1_zaddc; *) secp256k1_dblu; secp256k1_tplu; secp256k1_zdau; - laddermul]. + secp256k1_inv; + secp256k1_laddermul]. Compute (ToCString.c_module funcs). From d255ce2fb6dd2c284613ef3b9c0e8a5056416f3d Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Thu, 23 May 2024 11:31:25 +0200 Subject: [PATCH 09/10] Verified secp256k1_laddermul --- src/Bedrock/End2End/Secp256k1/Addchain.v | 1 - src/Bedrock/End2End/Secp256k1/JoyeLadder.v | 936 ++++++++++++++++++- src/Curves/Weierstrass/Jacobian/ScalarMult.v | 124 +-- 3 files changed, 962 insertions(+), 99 deletions(-) diff --git a/src/Bedrock/End2End/Secp256k1/Addchain.v b/src/Bedrock/End2End/Secp256k1/Addchain.v index 404364cfcd..9fe442abb5 100644 --- a/src/Bedrock/End2End/Secp256k1/Addchain.v +++ b/src/Bedrock/End2End/Secp256k1/Addchain.v @@ -247,7 +247,6 @@ Section WithParameters. pose (inv := fun (v: nat) (t: trace) (m: @map.rep word byte BasicC32Semantics.mem) (l: @map.rep string word locals) => t = tr /\ exists i (Hi: 1 <= i <= to), v = Z.to_nat (to - i) /\ - (* TODO: automate how to recover the frame *) (exists vx, ((FElem pvar vx) * R)%sep m /\ feval vx = F.pow (feval vvar) (N.pow 2%N (Z.to_N (i - 1))) /\ bounded_by un_outbounds vx) /\ diff --git a/src/Bedrock/End2End/Secp256k1/JoyeLadder.v b/src/Bedrock/End2End/Secp256k1/JoyeLadder.v index e2a65a1613..9259b7cc74 100644 --- a/src/Bedrock/End2End/Secp256k1/JoyeLadder.v +++ b/src/Bedrock/End2End/Secp256k1/JoyeLadder.v @@ -50,10 +50,10 @@ Local Existing Instance field_parameters. Local Instance frep256k1 : Field.FieldRepresentation := field_representation Field256k1.m. Local Existing Instance frep256k1_ok. -Definition secp256k1_laddermul := +Definition secp256k1_laddermul (scalarbitsz : Z) := func! (oX, oY, k, X, Y) { - i = coq:(2); - swap = (load1(k+coq:(1)>>coq:(3))>>(coq:(1)&coq:(7)))&coq:(1); + i = coq:(1); + swap = (load1(k+i>>coq:(3))>>(i&coq:(7)))&coq:(1); stackalloc 32 as X0; stackalloc 32 as Y0; stackalloc 32 as X1; @@ -61,52 +61,910 @@ Definition secp256k1_laddermul := stackalloc 32 as Z; stackalloc 32 as oZ; secp256k1_tplu(X1, Y1, X0, Y0, Z, X, Y); - secp256k1_felem_cswap(swap, X0, X1); - secp256k1_felem_cswap(swap, Y0, Y1); - while (i < coq:(256)) { - swap = (load1(k+i>>coq:(3))>>(i&coq:(7)))&coq:(1); - secp256k1_felem_cswap(swap, X0, X1); - secp256k1_felem_cswap(swap, Y0, Y1); + i = coq:(2); + while (i < coq:(scalarbitsz)) { + b = (load1(k+i>>coq:(3))>>(i&coq:(7)))&coq:(1); + swap = swap ^ b; + felem_cswap(swap, X0, X1); + felem_cswap(swap, Y0, Y1); secp256k1_zdau(X1, Y1, X0, Y0, Z); - secp256k1_felem_cswap(swap, X0, X1); - secp256k1_felem_cswap(swap, Y0, Y1); + swap = b; i = i+coq:(1) }; + felem_cswap(swap, X0, X1); + felem_cswap(swap, Y0, Y1); stackalloc 32 as tX; stackalloc 32 as tY; secp256k1_make_co_z(tX, tY, X, Y, Z); secp256k1_opp(tY, tY); - secp256k1_zaddu(X1, Y1, oX, oY, oZ, X0, Y0, tX, tY, Z); - swap = (load1(k+coq:(0)>>coq:(3))>>(coq:(0)&coq:(7)))&coq:(1); - secp256k1_felem_cswap(swap, oX, X1); - secp256k1_felem_cswap(swap, oY, Y1); + secp256k1_zaddu(oX, oY, X1, Y1, oZ, X0, Y0, tX, tY, Z); + i = coq:(0); + swap = (load1(k+i>>coq:(3))>>(i&coq:(7)))&coq:(1); + felem_cswap(swap, oX, X1); + felem_cswap(swap, oY, Y1); secp256k1_inv(Z, oZ); + secp256k1_mul(oY, oY, Z); + secp256k1_mul(Z, Z, Z); secp256k1_mul(oX, oX, Z); secp256k1_mul(oY, oY, Z) }. -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]. - -Compute (ToCString.c_module funcs). +Section WithParameters. + Context {two_lt_M: 2 < M_pos}. + 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 {secp256k1_prime: Znumtheory.prime m}. + Context {F_M_pos : Z.pos M_pos = m}. + Context {a b : F M_pos}. + Context {zero_a : id a = F.zero} + {seven_b : id b = F.of_Z _ 7}. + Context {scalarbitsz : Z} {scalarbitsz_small : word.wrap scalarbitsz = scalarbitsz}. + + Add Ring Private_ring : (F.ring_theory M_pos) (morphism (F.ring_morph M_pos), constants [F.is_constant]). + + 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 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)). + 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_points := (ScalarMult.co_z_points(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 zaddu_co_z_points := (ScalarMult.zaddu_co_z_points(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one)(Fopp:=F.opp)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div)(a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). + Local Notation zdau_co_z_points := (ScalarMult.zdau_co_z_points(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div)(a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). + Local Notation cswap_co_z_points := (ScalarMult.cswap_co_z_points(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div)(a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). + Local Notation make_co_z_points := (ScalarMult.make_co_z_points(F:=F M_pos)(Feq:=Logic.eq)(Fzero:=F.zero)(Fone:=F.one)(Fadd:=F.add)(Fsub:=F.sub)(Fmul:=F.mul)(Finv:=F.inv)(Fdiv:=F.div)(a:=a)(b:=b)(field:=field)(Feq_dec:=F.eq_dec)). + + Local Instance spec_of_secp256k1_opp : spec_of "secp256k1_opp" := Field.spec_of_UnOp un_opp. + Local Instance spec_of_secp256k1_square : spec_of "secp256k1_square" := Field.spec_of_UnOp un_square. + Local Instance spec_of_secp256k1_mul : spec_of "secp256k1_mul" := Field.spec_of_BinOp bin_mul. + Local Instance spec_of_secp256k1_add : spec_of "secp256k1_add" := Field.spec_of_BinOp bin_add. + Local Instance spec_of_secp256k1_sub : spec_of "secp256k1_sub" := Field.spec_of_BinOp bin_sub. + Local Instance spec_of_secp256k1_inv : spec_of "secp256k1_inv" := Addchain.spec_of_inv. + Local Instance spec_of_secp256k1_cswap : spec_of "felem_cswap" := CSwap.spec_of_cswap. + Local Instance spec_of_secp256k1_tplu : spec_of "secp256k1_tplu" := (@spec_of_tplu field a b). + Local Instance spec_of_secp256k1_make_co_z : spec_of "secp256k1_make_co_z" := (@spec_of_make_co_z field a b). + Local Instance spec_of_secp256k1_zaddu : spec_of "secp256k1_zaddu" := (@spec_of_zaddu field a b). + Local Instance spec_of_secp256k1_zdau : spec_of "secp256k1_zdau" := (@spec_of_zdau field a b). + + Local Arguments word.rep : simpl never. + Local Arguments word.wrap : simpl never. + Local Arguments word.unsigned : simpl never. + Local Arguments word.of_Z : simpl never. + + Local Ltac solve_mem := + repeat match goal with + | |- exists _ : _ -> Prop, _%sep _ => eexists + | |- _%sep _ => ecancel_assumption + end. + + Local Ltac cbv_bounds H := + cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds] in H; + cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds]. + + Local Ltac solve_bounds := + match goal with + | H: bounded_by _ ?x |- bounded_by _ ?x => apply H + end. + + Local Ltac solve_stack := + (* 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 + end; + [> transitivity 32%nat; trivial | ]; + (* proves the memory matches up *) + use_sep_assumption; cancel; cancel_seps_at_indices 0%nat 0%nat; cbn; [> trivial | eapply RelationClasses.reflexivity]. + + Local Ltac single_step := + repeat straightline; straightline_call; ssplit; try solve_mem; try solve_bounds; try solve_stack. + + Local Instance spec_of_laddermul : spec_of "secp256k1_laddermul" := + fnspec! "secp256k1_laddermul" + (OXptr OYptr kptr Xptr Yptr : word) / + (OX OY X Y : felem) (P : Wpoint) (HPnz : P <> Wzero) kbytes (k : Z) (R : _ -> Prop), + { requires t m := + proj1_sig P = inl ((feval X), (feval Y)) /\ + bounded_by loose_bounds X /\ + bounded_by loose_bounds Y /\ + LittleEndianList.le_combine kbytes = k /\ + 2 <= scalarbitsz <= 8*Z.of_nat (List.length kbytes) /\ + m =* (FElem OXptr OX) * (FElem OYptr OY) * kbytes$@kptr * + (FElem Xptr X) * (FElem Yptr Y) * R; + ensures t' m' := + t = t' /\ + match proj1_sig (ScalarMult.joye_ladder scalarbitsz (Z.testbit k) P HPnz) with + | inl (X', Y') => + exists OX' OY', + X' = (feval OX') /\ Y' = (feval OY') /\ + bounded_by tight_bounds OX' /\ + bounded_by tight_bounds OY' /\ + m' =* (FElem OXptr OX') * (FElem OYptr OY') * kbytes$@kptr * + (FElem Xptr X) * (FElem Yptr Y) * R + | _ => (* result is point at infinity *) + exists OX' OY', + 0%F = (feval OX') /\ 0%F = (feval OY') /\ + m' =* (FElem OXptr OX') * (FElem OYptr OY') * kbytes$@kptr * + (FElem Xptr X) * (FElem Yptr Y) * R + end + }. + + Lemma spec_of_testbit functions tr mem loc post : + forall var kptr kbytes k wi i R, + map.get loc "k" = Some kptr -> + map.get loc "i" = Some wi -> + (kbytes$@kptr * R)%sep mem -> + LittleEndianList.le_combine kbytes = k -> + wi = word.of_Z i -> + (0 <= i < 2 ^ 32)%Z -> + (i < 8 * Z.of_nat (List.length kbytes)) -> + + (forall tr' mem' loc', + (tr' = tr /\ + mem' = mem /\ + loc' = map.put loc var (Core.word.b2w (Z.testbit k i))) -> + post tr' mem' loc') -> + + cmd functions + bedrock_func_body:( + $var = load1(coq:(expr.var "k") + coq:(expr.var "i") >> coq:(expr.literal 3)) >> (coq:(expr.var "i") & coq:(expr.literal 7)) & coq:(expr.literal 1)) + tr mem loc post. + Proof. + repeat straightline. + repeat (eexists; split; repeat Tactics.straightline'; eauto); cbn [Semantics.interp_binop]. + + - subst wi. + eapply load_one_of_sep. + unshelve ( + let Hrw := open_constr:(@bytearray_index_inbounds _ _ _ _ _ _ _ _ _ : Lift1Prop.iff1 _ _) in + seprewrite0_in Hrw H1; ecancel_assumption). + all: repeat rewrite ?Core.word.unsigned_of_Z_b2z, ?word.unsigned_of_Z, ?word.unsigned_and_nowrap, ?word.unsigned_sru_nowrap. + all: cbv [word.wrap]; rewrite ?Z.mod_small; try lia. + rewrite ?Z.shiftr_div_pow2 by lia; change (2^3) with 8. lia. + - eapply H6. ssplit; auto. + f_equal. + eapply word.unsigned_inj. + unfold Core.word.b2w, wi. + repeat rewrite ?Core.word.unsigned_of_Z_b2z, ?word.unsigned_of_Z, ?word.unsigned_and_nowrap, ?word.unsigned_sru_nowrap. + all: cbv [word.wrap]; repeat rewrite ?Z.mod_small; try lia. + 2: match goal with | |- context [byte.unsigned ?n] => generalize (byte.unsigned_range n); lia end. + all: change 7 with (Z.ones 3); change 1 with (Z.ones 1); rewrite ?Z.land_ones by lia. + 2: lia. + rewrite ?Z.shiftr_div_pow2 by lia; change (2^3) with 8; change (2^1) with 2. + rewrite <-?List.hd_skipn_nth_default. + rewrite <- Z.testbit_spec' by lia; f_equal. + rewrite <- (LittleEndianList.split_le_combine kbytes), H2. + rewrite LittleEndianList.nth_default_le_split, byte.unsigned_of_Z, Z2Nat.id by lia. + cbv [byte.wrap]; rewrite <-Z.land_ones, Z.land_spec, Z.ones_spec_low by lia. + rewrite Z.shiftr_spec, Bool.andb_true_r by lia; f_equal. lia. + Qed. + + Lemma while_is_iter {A:Type} test body fuel s: + @Loops.while.while A test body fuel s = Nat.iter (S fuel) (fun s => if test s then body s else s) s. + Proof. + revert s; induction fuel; [reflexivity|]; intros. + rewrite Nat.iter_succ_r. + simpl Loops.while.while. rewrite IHfuel. + destruct (test s) eqn:Htest; [reflexivity|]. + clear -Htest. + induction fuel; [simpl; rewrite Htest; reflexivity|]. + rewrite Nat.iter_succ_r, Htest. apply IHfuel. + Qed. + + Lemma car_cswap {A} swap x y : + Core.P2.car (@cswap A swap x y) = if swap then y else x. + Proof. destruct swap; reflexivity. Qed. + + Lemma cdr_cswap {A} swap x y : + Core.P2.cdr (@cswap A swap x y) = if swap then x else y. + Proof. destruct swap; reflexivity. Qed. + + Lemma co_z_conv (PQ: co_z_points) : Jacobian.co_z (fst (proj1_sig PQ)) (snd (proj1_sig PQ)). + Proof. + generalize (proj2_sig PQ). rewrite (surjective_pairing (proj1_sig PQ)) at 1. + auto. + Qed. + + Lemma proj1_sig_zdau_co_z_points PQ : + proj1_sig (zdau_co_z_points PQ) = (fst (Jacobian.zdau (fst (proj1_sig PQ)) (snd (proj1_sig PQ)) (co_z_conv PQ)), snd (Jacobian.zdau (fst (proj1_sig PQ)) (snd (proj1_sig PQ)) (co_z_conv PQ))). + Proof. + destruct PQ as (PQ' & ?). destruct PQ' as (P & Q). + unfold zdau_co_z_points. cbv [proj1_sig]. + rewrite (surjective_pairing (Jacobian.zdau P Q _)). + repeat f_equal; apply Eqdep_dec.UIP_dec; apply F.eq_dec. + Qed. + + Lemma proj1_sig_cswap_co_z_points swap PQ : + proj1_sig (cswap_co_z_points swap PQ) = (if swap then snd (proj1_sig PQ) else fst (proj1_sig PQ), if swap then fst (proj1_sig PQ) else snd (proj1_sig PQ)). + Proof. + destruct PQ as (PQ' & ?). destruct PQ' as (P & Q). + unfold cswap_co_z_points. cbv [proj1_sig]. + destruct swap; reflexivity. + Qed. + + Lemma proj1_sig_zaddu_co_z_points PQ : + proj1_sig (zaddu_co_z_points PQ) = (fst (Jacobian.zaddu (fst (proj1_sig PQ)) (snd (proj1_sig PQ)) (co_z_conv PQ)), snd (Jacobian.zaddu (fst (proj1_sig PQ)) (snd (proj1_sig PQ)) (co_z_conv PQ))). + Proof. + destruct PQ as (PQ' & ?). destruct PQ' as (P & Q). + unfold zaddu_co_z_points. cbv [proj1_sig]. + rewrite (surjective_pairing (Jacobian.zaddu P Q _)). + repeat f_equal; apply Eqdep_dec.UIP_dec; apply F.eq_dec. + Qed. + + Lemma zdau_eq (P: point) P' Q Q' HPQ HPQ' : + P = P' -> + Q = Q' -> + Jacobian.zdau P Q HPQ = Jacobian.zdau P' Q' HPQ'. + Proof. + intros. subst P' Q'. + assert (HPQ = HPQ') as -> by (apply Eqdep_dec.UIP_dec; apply F.eq_dec). + reflexivity. + Qed. + + Lemma zaddu_eq (P: point) P' Q Q' HPQ HPQ' : + P = P' -> + Q = Q' -> + Jacobian.zaddu P Q HPQ = Jacobian.zaddu P' Q' HPQ'. + Proof. + intros. subst P' Q'. + assert (HPQ = HPQ') as -> by (apply Eqdep_dec.UIP_dec; apply F.eq_dec). + reflexivity. + Qed. + + Lemma spec_of_inner_loop functions tr mem loc post : + forall kptr kbytes k X0ptr X1ptr Y0ptr Y1ptr Zptr X0 X1 Y0 Y1 Z (R0 R1:point) R, + spec_of_secp256k1_cswap functions -> + spec_of_secp256k1_zdau functions -> + map.get loc "k" = Some kptr -> + map.get loc "i" = Some (word.of_Z 2) -> + map.get loc "swap" = Some (Core.word.b2w (Z.testbit k 1)) -> + map.get loc "X0" = Some X0ptr -> + map.get loc "Y0" = Some Y0ptr -> + map.get loc "X1" = Some X1ptr -> + map.get loc "Y1" = Some Y1ptr -> + map.get loc "Z" = Some Zptr -> + LittleEndianList.le_combine kbytes = k -> + 2 <= scalarbitsz <= 8*Z.of_nat (List.length kbytes) -> + (kbytes$@kptr * FElem X0ptr X0 * FElem Y0ptr Y0 * FElem X1ptr X1 * FElem Y1ptr Y1 * FElem Zptr Z * R)%sep mem -> + proj1_sig R0 = (feval X0, feval Y0, feval Z) -> + proj1_sig R1 = (feval X1, feval Y1, feval Z) -> + bounded_by loose_bounds X0 -> + bounded_by loose_bounds Y0 -> + bounded_by loose_bounds X1 -> + bounded_by loose_bounds Y1 -> + bounded_by loose_bounds Z -> + + (forall tr' mem' loc', + (tr' = tr) -> + (exists (R1R0_co_z : Jacobian.co_z R1 R0), + let R1R0 := exist (fun '(P, Q) => Jacobian.co_z P Q) (R1, R0) R1R0_co_z in + let '(R1R0', vswap, _) := + Loops.while.while (fun '(_, _, i) => i (zdau_co_z_points (cswap_co_z_points (xorb swap (Z.testbit k i)) R1R0), Z.testbit k i, Z.succ i)) (Z.to_nat (scalarbitsz - 2)) (R1R0, Z.testbit k 1, 2) in + exists l, (forall s, s <> "b" -> map.get l s = map.get loc s) /\ + loc' = map.put (map.put l "swap" (Core.word.b2w vswap)) "i" (word.of_Z scalarbitsz) /\ + exists X0' Y0' X1' Y1' Z', + (kbytes$@kptr * FElem X0ptr X0' * FElem Y0ptr Y0' * FElem X1ptr X1' * FElem Y1ptr Y1' * FElem Zptr Z' * R)%sep mem' /\ + bounded_by loose_bounds X0' /\ + bounded_by loose_bounds Y0' /\ + bounded_by loose_bounds X1' /\ + bounded_by loose_bounds Y1' /\ + bounded_by loose_bounds Z' /\ + let '(R1', R0') := proj1_sig R1R0' in + proj1_sig R0' = (feval X0', feval Y0', feval Z') /\ + proj1_sig R1' = (feval X1', feval Y1', feval Z')) -> + post tr' mem' loc' + ) -> + + cmd functions + bedrock_func_body:( + while coq:(expr.var "i") < coq:(expr.literal scalarbitsz) { + {$"b" = load1(coq:(expr.var "k") + + coq:(expr.var "i") >> coq:(expr.literal 3)) >> + (coq:(expr.var "i") & coq:(expr.literal 7)) & coq:(expr.literal 1)}; + {$"swap" = coq:(expr.var "swap") ^ coq:(expr.var "b")}; + {$"felem_cswap"(coq:(expr.var "swap"), coq:(expr.var "X0"), coq:(expr.var "X1"))}; + {$"felem_cswap"(coq:(expr.var "swap"), coq:(expr.var "Y0"), coq:(expr.var "Y1"))}; + {$"secp256k1_zdau"(coq:(expr.var "X1"), coq:(expr.var "Y1"), + coq:(expr.var "X0"), coq:(expr.var "Y0"), + coq:(expr.var "Z"))}; + {$"swap" = coq:(expr.var "b")}; + $"i" = coq:(expr.var "i") + coq:(expr.literal 1) + }) tr mem loc post. + Proof. + intros. repeat straightline. + assert (R1R0_z : Jacobian.co_z R1 R0) by (unfold Jacobian.co_z, Jacobian.z_of; rewrite H12, H13; reflexivity). + pose (R1R0 := exist (fun '(P, Q) => Jacobian.co_z P Q) (R1, R0) R1R0_z). + pose (test := (fun '(_, _, i) => (Z.ltb i scalarbitsz)):(co_z_points*bool*BinInt.Z)->bool). + pose (body := (fun '(R1R0, swap, i) => + let b := Z.testbit k i in + let swap := xorb swap b in + let R1R0 := cswap_co_z_points swap R1R0 in + let R1R0 := zdau_co_z_points R1R0 in + 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) => + t = tr /\ + exists i (Hi: 2 <= i <= scalarbitsz), + v = Z.to_nat (scalarbitsz - i) /\ + let '(R1R0', swap', i') := Nat.iter (Z.to_nat (i - 2)) (fun s => if test s then body s else s) (R1R0, Z.testbit k 1, 2%Z) in + i' = i /\ + exists loc', (forall s, s <> "b" -> map.get loc' s = map.get loc s) /\ + l = map.put (map.put loc' "swap" (Core.word.b2w swap')) "i" (word.of_Z i) /\ + exists X0' Y0' X1' Y1' Z', + (kbytes$@kptr * FElem X0ptr X0' * FElem Y0ptr Y0' * FElem X1ptr X1' * FElem Y1ptr Y1' * FElem Zptr Z' * R)%sep m /\ + bounded_by loose_bounds X0' /\ + bounded_by loose_bounds Y0' /\ + bounded_by loose_bounds X1' /\ + bounded_by loose_bounds Y1' /\ + bounded_by loose_bounds Z' /\ + let '(R1', R0') := proj1_sig R1R0' in + proj1_sig R0' = (feval X0', feval Y0', feval Z') /\ + proj1_sig R1' = (feval X1', feval Y1', feval Z')). + eapply wp_while. exists nat, lt, inv. ssplit; [eapply lt_wf|..]. + (* Invariant holds at beginning *) + eexists. unfold inv; ssplit; [reflexivity|..]. + exists 2. exists (ltac:(lia): 2 <= 2 <= scalarbitsz). ssplit; [reflexivity|..]. + rewrite DecimalPos.Unsigned.nat_iter_0. ssplit; [reflexivity|..]. + exists loc. ssplit; [reflexivity|..]. + apply Core.map.ext_eq; intros s. + destruct (String.eqb_spec "i" s); [subst s; rewrite map.get_put_same; assumption|rewrite map.get_put_diff by auto]. + destruct (String.eqb_spec "swap" s); [subst s; rewrite map.get_put_same; assumption|rewrite map.get_put_diff by auto]. + reflexivity. do 5 eexists; ssplit; [ecancel_assumption|..]; try solve_bounds. + unfold R1R0. cbn [proj1_sig]. rewrite H12, H13. split; reflexivity. + (* Invariant preservation *) + intros fuel * Hinv. destruct Hinv as (-> & vi & Hvi & -> & Hiter). + pose (iter_res := Nat.iter (Z.to_nat (vi - 2)) (fun s => if test s then body s else s) (R1R0, Z.testbit k 1, 2%Z)). + 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). + eexists ?[b]; ssplit. + eexists; split; [apply map.get_put_same|]. + eapply Core.WeakestPrecondition_dexpr_expr; [|apply ExprCompiler.expr_compile_Z_literal]. + cbn. rewrite <- Core.word.morph_ltu by lia. + reflexivity. + all: pose proof Zlt_cases vi scalarbitsz; + intros Hnz; destruct (vi & -> & ->). + repeat straightline. eexists; split. + repeat straightline. eexists; split. + repeat (rewrite map.get_put_diff by congruence). + apply map.get_put_same. repeat straightline. + eexists; split. apply map.get_put_same. + unfold Core.word.b2w. rewrite <- Core.word.morph_xor. + rewrite Core.Z.lxor_xorb. reflexivity. + repeat straightline. eexists; split. + eexists. split. apply map.get_put_same. + repeat straightline. eexists; split. + unfold l. repeat (rewrite map.get_put_diff by congruence). + rewrite Hloc' by congruence. eassumption. + repeat straightline. eexists; split. + unfold l. repeat (rewrite map.get_put_diff by congruence). + rewrite Hloc' by congruence. eassumption. + repeat straightline. + straightline_call; ssplit. + destruct (xorb _ _); simpl; auto. + rewrite <- Bignum_as_array. unfold FElem in Hmem. + ecancel_assumption. repeat straightline. + eexists. split. repeat straightline. + eexists; split. apply map.get_put_same. + repeat straightline. eexists; split. + unfold l. repeat (rewrite map.get_put_diff by congruence). + rewrite Hloc' by congruence. eassumption. + repeat straightline. eexists; split. + unfold l. repeat (rewrite map.get_put_diff by congruence). + rewrite Hloc' by congruence. eassumption. + repeat straightline. + cbv [dlet.dlet] in H26. + straightline_call; ssplit. + destruct (xorb _ _); auto. + rewrite <- Bignum_as_array. ecancel_assumption. + repeat straightline. + cbv [dlet.dlet] in H27. + assert (Hlen: forall ptr v m R, (FElem ptr v * R)%sep m -> Datatypes.length v = felem_size_in_words). + { unfold FElem. rewrite Bignum_as_array. + intros * XX. apply Arrays.length_of_sizedlistarray_value_R in XX. exact XX. } + repeat rewrite cswap_low_combine_eq in H27 by (repeat erewrite Hlen by ecancel_assumption; reflexivity). + rewrite cswap_combine_eq in H27. + 2: destruct (xorb _ _); cbv; auto. + 2-3: symmetry; eapply Hlen; ecancel_assumption. + rewrite cswap_combine_eq in H27. + 2: destruct (xorb _ _); cbv; auto. + 2-3: symmetry; eapply Hlen; ecancel_assumption. + rewrite <- Bignum_as_array in H27. + repeat rewrite car_cswap, cdr_cswap in H27. + rewrite word.unsigned_eqb, Core.word.unsigned_of_Z_b2z, word.unsigned_of_Z_1 in H27. + assert (XY: forall bb, (Z.b2z bb =? 1) = bb) by (destruct bb; auto). + rewrite XY in H27; clear XY. + eexists; split. + repeat (repeat straightline; eexists; split; [unfold l; repeat rewrite map.get_put_diff by congruence; rewrite Hloc' by congruence; eassumption|]). + repeat straightline. straightline_call; ssplit. + 8: unfold Field.FElem; ecancel_assumption_impl. + instantiate (1 := if xorb (snd (fst iter_res)) (Z.testbit k vi) then R0' else R1'). + destruct (xorb _ _); [exact Hproj0|exact Hproj1]. + instantiate (1 := if xorb (snd (fst iter_res)) (Z.testbit k vi) then R1' else R0'). + destruct (xorb _ _); [exact Hproj1|exact Hproj0]. + 1-4: destruct (xorb _ _); solve_bounds. + solve_bounds. + Unshelve. 3: unfold Jacobian.co_z, Jacobian.z_of; destruct (xorb _ _); rewrite Hproj0, Hproj1; reflexivity. + repeat straightline. + eexists. ssplit. repeat straightline. + eexists. split. unfold l. repeat (rewrite map.get_put_diff by congruence). + apply map.get_put_same. reflexivity. + repeat straightline. + eexists. ssplit. repeat straightline. + eexists. split. unfold l0, l. repeat (rewrite map.get_put_diff by congruence). + apply map.get_put_same. repeat straightline. + repeat straightline. eexists. split. + unfold inv; split; [reflexivity|]. + exists (vi + 1). exists (ltac:(lia): 2 <= vi + 1 <= scalarbitsz). + ssplit; [reflexivity|]. + replace (Z.to_nat (vi + 1 - 2)) with (S (Z.to_nat (vi - 2))) by lia. + rewrite Nat.iter_succ. fold iter_res. + unfold test. rewrite (surjective_pairing iter_res), Hvi'. + replace (vi by lia. + assert (iter_res = Nat.iter (S (Z.to_nat (scalarbitsz - 2))) (fun s : co_z_points * bool * BinNums.Z => if test s then body s else s) (R1R0, Z.testbit k 1, 2)). + { rewrite Nat.iter_succ. fold iter_res. + rewrite (surjective_pairing iter_res) at 2. + rewrite Hvi'. simpl test. + replace (scalarbitsz > coq:(expr.literal 3)) >> (coq:(expr.var "i") & coq:(expr.literal 7)) & coq:(expr.literal 1)) _ _ _ _ => idtac end |straightline]. + eapply spec_of_testbit; try reflexivity; try ecancel_assumption_impl; try lia. + + assert (HPaff: Jacobian.z_of (Jacobian.of_affine P) = F.one) by (apply (ScalarMult.ScalarMult.joye_ladder_obligation_1 P HPnz)). + + repeat straightline. + single_step. + instantiate (3 := Jacobian.of_affine P). + unfold Jacobian.of_affine, WeierstrassCurve.W.coordinates. + cbn [proj1_sig]. rewrite (sig_eta P). rewrite H15. eexists. reflexivity. + 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|] + 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. cancel_seps_at_indices 0%nat 4%nat; [reflexivity|]. + cancel_seps_at_indices 0%nat 3%nat; [reflexivity|]. + cancel_seps_at_indices 0%nat 2%nat; [reflexivity|]. + cancel_seps_at_indices 0%nat 1%nat; [reflexivity|]. + cancel_seps_at_indices 0%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 3%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 3%nat 0%nat; [reflexivity|]. + ecancel. + + repeat straightline. + instantiate (1:=HPaff) in H48. + eapply spec_of_inner_loop; try reflexivity; try ecancel_assumption_impl; try lia. + exact H49. exact H48. + 1-5: solve_bounds. + repeat straightline. + rewrite H18 in H47. + case_eq (Loops.while.while (fun '(_, _, i) => i + (zdau_co_z_points (cswap_co_z_points (xorb swap (Z.testbit k i)) R1R0), Z.testbit k i, Z.succ i)) (Z.to_nat (scalarbitsz - 2)) + (exist (fun '(P, Q) => Jacobian.co_z P Q) (fst (Jacobian.tplu (Jacobian.of_affine P) HPaff), snd (Jacobian.tplu (Jacobian.of_affine P) HPaff)) x4, Z.testbit k 1, 2)); intros [R1R0' vswap] ?i Hloopeq. + rewrite Hloopeq in H47. repeat straightline. + + eexists; ssplit. repeat straightline. + eexists; ssplit; [unfold loc'0; repeat rewrite map.get_put_diff by congruence; apply map.get_put_same|repeat straightline]. + eexists; ssplit; [unfold loc'0; repeat rewrite map.get_put_diff by congruence; rewrite H46|]; repeat straightline. congruence. + eexists; ssplit; [unfold loc'0; repeat rewrite map.get_put_diff by congruence; rewrite H46|]; repeat straightline. congruence. + + single_step. rewrite Core.word.b2w_if; destruct vswap; auto. + rewrite <- Bignum_as_array. unfold FElem in H56. ecancel_assumption. + repeat straightline. red in H64. + assert (Hlen: forall ptr v m R, (FElem ptr v * R)%sep m -> Datatypes.length v = felem_size_in_words). + { unfold FElem. rewrite Bignum_as_array. + intros * XX. apply Arrays.length_of_sizedlistarray_value_R in XX. exact XX. } + rewrite cswap_low_combine_eq in H64 by (repeat erewrite Hlen by ecancel_assumption; reflexivity). + rewrite cswap_combine_eq in H64. + 2: destruct vswap; cbv; auto. + 2-3: symmetry; eapply Hlen; ecancel_assumption. + repeat rewrite car_cswap, cdr_cswap in H64. + rewrite word.unsigned_eqb, Core.word.unsigned_b2w, word.unsigned_of_Z_1 in H64. + assert (XY: forall bb, (Z.b2z bb =? 1) = bb) by (destruct bb; auto). + rewrite XY in H64; clear XY. + rewrite <- Bignum_as_array in H64. + eexists; ssplit. repeat straightline. + eexists; ssplit; [unfold loc'0; repeat rewrite map.get_put_diff by congruence; apply map.get_put_same|repeat straightline]. + eexists; ssplit; [unfold loc'0; repeat rewrite map.get_put_diff by congruence; rewrite H46|]; repeat straightline. congruence. + eexists; ssplit; [unfold loc'0; repeat rewrite map.get_put_diff by congruence; rewrite H46|]; repeat straightline. congruence. + + single_step. rewrite Core.word.b2w_if; destruct vswap; auto. + rewrite <- Bignum_as_array. ecancel_assumption. + repeat straightline. red in H65. + rewrite cswap_low_combine_eq in H65 by (repeat erewrite Hlen by ecancel_assumption; reflexivity). + rewrite cswap_combine_eq in H65. + 2: destruct vswap; cbv; auto. + 2-3: symmetry; eapply Hlen; ecancel_assumption. + repeat rewrite car_cswap, cdr_cswap in H65. + rewrite word.unsigned_eqb, Core.word.unsigned_b2w, word.unsigned_of_Z_1 in H65. + assert (XY: forall bb, (Z.b2z bb =? 1) = bb) by (destruct bb; auto). + rewrite XY in H65; clear XY. + rewrite <- Bignum_as_array in H65. + eexists; ssplit. repeat straightline. + eexists; ssplit. unfold l9. rewrite map.get_put_diff by congruence. + apply map.get_put_same. repeat straightline. + eexists; ssplit; [apply map.get_put_same|]. repeat straightline. + eexists; ssplit. unfold l9, l8, loc'0. + repeat (rewrite map.get_put_diff by congruence). + rewrite H46. repeat straightline. congruence. + repeat straightline. eexists; ssplit. unfold l9, l8, loc'0. + repeat (rewrite map.get_put_diff by congruence). + rewrite H46. repeat straightline. congruence. + repeat straightline. eexists; ssplit. unfold l9, l8, loc'0. + repeat (rewrite map.get_put_diff by congruence). + rewrite H46. repeat straightline. congruence. + repeat straightline. + destruct R1R0' as ((R1'& R0') & HR1R0') eqn:HeqR1R0'. + destruct H62. + single_step. + exists (if vswap then feval x8 else feval x6). + exists (if vswap then feval x9 else feval x7). + instantiate (2:=if vswap then R1' else R0'). + destruct (vswap); [exact H68|exact H62]. + exists 1%F. instantiate (3:=Jacobian.of_affine P). + unfold Jacobian.of_affine, WeierstrassCurve.W.coordinates. + cbv [proj1_sig]. + assert (proj1_sig P = (let (xyi, _) := P in xyi)) as <- by (destruct P; reflexivity). + rewrite H15. reflexivity. + 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|] + 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. cancel_seps_at_indices 0%nat 1%nat; [reflexivity|]. + cancel_seps_at_indices 0%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 6%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 6%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 5%nat 0%nat; [reflexivity|]. + ecancel. + instantiate (1:=HPaff) in H73. + repeat straightline. + + eexists; ssplit. repeat straightline. + eexists; ssplit. apply map.get_put_same. repeat straightline. + eexists; ssplit; [apply map.get_put_same|]; repeat straightline. + single_step. + 2-3: ecancel_assumption_impl. + solve_bounds. + repeat straightline. + eexists; split. unfold l9, l8, loc'0. + repeat (repeat straightline; eexists; ssplit; [repeat (rewrite map.get_put_diff by congruence); rewrite H46; repeat straightline; congruence|]). + repeat straightline. eexists; ssplit. + repeat (rewrite map.get_put_diff by congruence); apply map.get_put_same. + repeat straightline. eexists; ssplit. + repeat (rewrite map.get_put_diff by congruence); apply map.get_put_same. + repeat straightline. eexists; ssplit. + repeat (rewrite map.get_put_diff by congruence); rewrite H46; repeat straightline; congruence. + repeat straightline. + cbv [un_model un_opp] in H79. + + assert (Hzaddu_ob: Jacobian.co_z (if vswap then R1' else R0') (Jacobian.opp (snd (Jacobian.make_co_z (if vswap then R1' else R0') (Jacobian.of_affine P) HPaff)))). + { unfold Jacobian.co_z, Jacobian.z_of, Jacobian.opp. + cbv [proj1_sig] in *. rewrite H75. + destruct vswap; [rewrite H68|rewrite H62]; reflexivity. } + single_step. + instantiate (1:=x10). + instantiate (1:=if vswap then x9 else x7). + instantiate (1:=if vswap then x8 else x6). + instantiate (1:=if vswap then R1' else R0'). + destruct vswap; [exact H68|exact H62]. + instantiate (1:=x13). instantiate (1:=x11). + instantiate (1:=Jacobian.opp (snd (Jacobian.make_co_z (if vswap then R1' else R0') (Jacobian.of_affine P) HPaff))). + unfold Jacobian.opp. + cbv [proj1_sig]. cbv [proj1_sig] in H75. rewrite H75. + unfold JacobianCoZ.frep256k1. unfold frep256k1 in H79. + rewrite H79. reflexivity. + 1-2: destruct vswap; solve_bounds. + 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|] + 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. cancel_seps_at_indices 9%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 9%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 7%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 5%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 0%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 4%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 3%nat 0%nat; [reflexivity|]. + cancel_seps_at_indices 0%nat 0%nat; [reflexivity|]. + ecancel. + instantiate (1:=Hzaddu_ob) in H73. + repeat first [match goal with | |- cmd _ bedrock_func_body:($_ = load1(coq:(expr.var "k") + coq:(expr.var "i") >> coq:(expr.literal 3)) >> (coq:(expr.var "i") & coq:(expr.literal 7)) & coq:(expr.literal 1)) _ _ _ _ => idtac end |straightline]. + eapply spec_of_testbit; try reflexivity; try ecancel_assumption_impl; try lia. + unfold l10, l9, l8, loc'0. repeat (rewrite map.get_put_diff by congruence). + rewrite H46 by congruence. reflexivity. + apply map.get_put_same. lia. lia. + repeat straightline. + + eexists; ssplit. repeat straightline. + eexists; ssplit; [apply map.get_put_same|]. + repeat straightline. eexists; ssplit. + unfold loc'1, l10, l9, l8, loc'0. repeat (rewrite map.get_put_diff by congruence). + rewrite H46 by congruence. reflexivity. + repeat straightline. eexists; ssplit. + unfold loc'1, l10, l9, l8, loc'0. repeat (rewrite map.get_put_diff by congruence). + rewrite H46 by congruence. reflexivity. + repeat straightline. + rewrite H18. + single_step. + rewrite Core.word.b2w_if; destruct (Z.testbit k 0); auto. + rewrite <- Bignum_as_array. + unfold Field.FElem in H89. ecancel_assumption_impl. + repeat straightline. red in H90. + rewrite <- Bignum_as_array in H90. + rewrite cswap_low_combine_eq in H90 by (repeat erewrite Hlen by ecancel_assumption_impl; reflexivity). + rewrite cswap_combine_eq in H90. + 2: destruct (Z.testbit k 0); cbv; auto. + 2-3: symmetry; eapply Hlen; ecancel_assumption_impl. + repeat rewrite car_cswap, cdr_cswap in H90. + rewrite word.unsigned_eqb, Core.word.unsigned_b2w, word.unsigned_of_Z_1 in H90. + assert (XY: forall bb, (Z.b2z bb =? 1) = bb) by (destruct bb; auto). + rewrite XY in H90; clear XY. + eexists; ssplit. repeat straightline. + eexists; ssplit; [apply map.get_put_same|]. + repeat straightline. eexists; ssplit. + unfold loc'1, l10, l9, l8, loc'0. repeat (rewrite map.get_put_diff by congruence). + rewrite H46 by congruence. reflexivity. + repeat straightline. eexists; ssplit. + unfold loc'1, l10, l9, l8, loc'0. repeat (rewrite map.get_put_diff by congruence). + rewrite H46 by congruence. reflexivity. + repeat straightline. + rewrite H18. + single_step. + destruct (Z.testbit k 0); cbv; auto. + rewrite <- Bignum_as_array. + unfold Field.FElem in H90. ecancel_assumption_impl. + repeat straightline. red in H91. + rewrite <- Bignum_as_array in H91. + rewrite cswap_low_combine_eq in H91 by (repeat erewrite Hlen by ecancel_assumption_impl; reflexivity). + rewrite cswap_combine_eq in H91. + 2: destruct (Z.testbit k 0); cbv; auto. + 2-3: symmetry; eapply Hlen; ecancel_assumption_impl. + repeat rewrite car_cswap, cdr_cswap in H91. + rewrite word.unsigned_eqb, Core.word.unsigned_b2w, word.unsigned_of_Z_1 in H91. + assert (XY: forall bb, (Z.b2z bb =? 1) = bb) by (destruct bb; auto). + rewrite XY in H91; clear XY. + + eexists; ssplit. repeat straightline. eexists; ssplit. + unfold loc'1, l10, l9, l8, loc'0. repeat (rewrite map.get_put_diff by congruence). + rewrite H46 by congruence. reflexivity. + repeat straightline. eexists; ssplit. + unfold loc'1, l10, l9, l8, loc'0. repeat (rewrite map.get_put_diff by congruence). + rewrite H46 by congruence. reflexivity. + repeat straightline. + single_step. + 3: unfold Field.FElem; ecancel_assumption_impl. + reflexivity. solve_bounds. + repeat straightline. + eexists; ssplit. repeat straightline. eexists; ssplit. + unfold loc'1, l10, l9, l8, loc'0. repeat (rewrite map.get_put_diff by congruence). + rewrite H46 by congruence. reflexivity. + repeat straightline. eexists; ssplit. + unfold loc'1, l10, l9, l8, loc'0. repeat (rewrite map.get_put_diff by congruence). + rewrite H46 by congruence. reflexivity. + repeat straightline. eexists; ssplit. + unfold loc'1, l10, l9, l8, loc'0. repeat (rewrite map.get_put_diff by congruence). + rewrite H46 by congruence. reflexivity. + repeat straightline. + single_step. + 3-5: unfold FElem; ecancel_assumption_impl. + destruct (Z.testbit k 0); solve_bounds. + solve_bounds. + repeat straightline. + eexists; ssplit. repeat straightline. + repeat (eexists; ssplit; [unfold loc'1, l10, l9, l8, loc'0; repeat (rewrite map.get_put_diff by congruence); rewrite H46 by congruence; reflexivity|]; repeat straightline). + cbv [bin_model bin_mul] in H95. + + single_step. + 3-5: unfold FElem in *; ecancel_assumption_impl. + 1-2: solve_bounds. + repeat straightline. + eexists; ssplit. repeat straightline. + repeat (eexists; ssplit; [unfold loc'1, l10, l9, l8, loc'0; repeat (rewrite map.get_put_diff by congruence); rewrite H46 by congruence; reflexivity|]; repeat straightline). + cbv [bin_model bin_mul] in H98. + + single_step. + 2-3: unfold FElem in *; ecancel_assumption_impl. + destruct (Z.testbit k 0); solve_bounds. + repeat straightline. + eexists; ssplit. repeat straightline. + repeat (eexists; ssplit; [unfold loc'1, l10, l9, l8, loc'0; repeat (rewrite map.get_put_diff by congruence); rewrite H46 by congruence; reflexivity|]; repeat straightline). + cbv [bin_model bin_mul] in H101. + + single_step. + 3-5: unfold FElem in *; ecancel_assumption_impl. + 1-2: solve_bounds. + repeat straightline. + cbv [bin_model bin_mul] in H104. + + cbv [FElem] in *. + replace JacobianCoZ.frep256k1 with frep256k1 in * by reflexivity. + replace Addchain.frep256k1 with frep256k1 in * by reflexivity. + repeat match goal with + | |- context [anybytes ?a _ _] => + match goal with + | H: _ ?a' |- context [map.split ?a' _ _] => + seprewrite_in (@Bignum.Bignum_to_bytes _ _ _ _ _ _ felem_size_in_words a) H + end + end. + extract_ex1_and_emp_in H106. + repeat straightline. + + unfold ScalarMult.joye_ladder. + unfold ScalarMult.joye_ladder_inner. + assert (ScalarMult.tplu_co_z_points (Jacobian.of_affine P) (ScalarMult.ScalarMult.joye_ladder_obligation_1 P HPnz) = exist (fun '(P, Q) => Jacobian.co_z P Q) (fst (Jacobian.tplu (Jacobian.of_affine P) HPaff), snd (Jacobian.tplu (Jacobian.of_affine P) HPaff)) x4) as ->. + { unfold ScalarMult.tplu_co_z_points. + apply eq_sig_hprop. + - intros. destruct x24. + apply Eqdep_dec.UIP_dec; apply F.eq_dec. + - cbv [proj1_sig]. + rewrite <- (surjective_pairing (Jacobian.tplu (Jacobian.of_affine P) HPaff)). + f_equal. apply Eqdep_dec.UIP_dec; apply F.eq_dec. } + assert (Z.to_nat scalarbitsz - 2 = Z.to_nat (scalarbitsz - 2))%nat as -> by lia. + match goal with + | |- context [Loops.while.while ?test ?body ?fuel ?args] => + match type of Hloopeq with + | context [Loops.while.while ?test1 ?body1 ?fuel1 ?args1] => + replace (Loops.while.while test body fuel args) with (Loops.while.while test1 body1 fuel1 args1) by reflexivity + end + end. + rewrite Hloopeq. + rewrite (proj1_sig_cswap_co_z_points vswap). + assert (red_proj1_sig: forall (A : Type) (P : A -> Prop) (x : A) (Px : P x), proj1_sig (exist P x Px) = x) by reflexivity. + rewrite red_proj1_sig. + cbv [fst snd]. + rewrite proj1_sig_cswap_co_z_points, proj1_sig_zaddu_co_z_points. + rewrite <- (surjective_pairing (Jacobian.zaddu _ _ _)). + assert (Jacobian.zaddu + (fst (proj1_sig (make_co_z_points (if vswap then R1' else R0') (Jacobian.opp (Jacobian.of_affine P)) (ScalarMult.opp_of_affine P HPnz)))) + (snd (proj1_sig (make_co_z_points (if vswap then R1' else R0') (Jacobian.opp (Jacobian.of_affine P)) (ScalarMult.opp_of_affine P HPnz)))) + (co_z_conv (make_co_z_points (if vswap then R1' else R0') (Jacobian.opp (Jacobian.of_affine P)) (ScalarMult.opp_of_affine P HPnz))) = + Jacobian.zaddu (if vswap then R1' else R0') + (Jacobian.opp (snd (Jacobian.make_co_z (if vswap then R1' else R0') (Jacobian.of_affine P) HPaff))) Hzaddu_ob) as ->. + { apply zaddu_eq. + - unfold make_co_z_points. rewrite red_proj1_sig. + unfold Jacobian.make_co_z. cbv [fst]. + apply eq_sig_hprop; [|rewrite red_proj1_sig]. + + intros. destruct x24 as ((?X & ?Y) & ?Z). + destruct (dec (Z = 0%F)). destruct p, q; reflexivity. + apply Eqdep_dec.UIP_dec; apply F.eq_dec. + + destruct (Jacobian.of_affine P) as (((?X & ?Y) & ?Z) & ?H). + destruct R1' as (((?X & ?Y) & ?Z) & ?H). + destruct R0' as (((?X & ?Y) & ?Z) & ?H). + destruct vswap; cbv [Jacobian.opp]; repeat rewrite red_proj1_sig; reflexivity. + - unfold make_co_z_points. rewrite red_proj1_sig. + unfold Jacobian.make_co_z. cbv [snd]. + apply eq_sig_hprop; [|rewrite red_proj1_sig]. + + intros. destruct x24 as ((?X & ?Y) & ?Z). + destruct (dec (Z = 0%F)). destruct p, q; reflexivity. + apply Eqdep_dec.UIP_dec; apply F.eq_dec. + + unfold Jacobian.opp; repeat rewrite red_proj1_sig. + destruct (Jacobian.of_affine P) as (((?X & ?Y) & ?Z) & ?H). + destruct R1' as (((?X & ?Y) & ?Z) & ?H). + destruct R0' as (((?X & ?Y) & ?Z) & ?H). + destruct vswap; repeat rewrite red_proj1_sig; f_equal; f_equal; ring. } + unfold Jacobian.to_affine. rewrite red_proj1_sig. + destruct (Z.testbit k 0); [rewrite H83|rewrite H82]; + match goal with + | |- context [if ?test then _ else _] => destruct test + end; do 2 eexists; ssplit; try ecancel_assumption_impl; try solve_bounds; + repeat match goal with + | H : feval ?a = _ |- context [feval ?a] => rewrite H + end. + 1,2,5,6: rewrite F.inv_0; ring. + Add Field Private_field : (Algebra.Field.field_theory_for_stdlib_tactic (T:=F M_pos)). + Import Field_tac. + 1-4: field; exact n. + Qed. + +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)]. *) +(* Compute (ToCString.c_module funcs). *) diff --git a/src/Curves/Weierstrass/Jacobian/ScalarMult.v b/src/Curves/Weierstrass/Jacobian/ScalarMult.v index 2fe2dba939..185e4eb9cb 100644 --- a/src/Curves/Weierstrass/Jacobian/ScalarMult.v +++ b/src/Curves/Weierstrass/Jacobian/ScalarMult.v @@ -206,19 +206,22 @@ Module ScalarMult. Definition joye_ladder_inner (scalarbitsz : Z) (testbit : Z -> bool) (P : point) (HPaff : z_of P = 1) : point := (* Initialization *) - let b := testbit 1%Z in - let R1R0 := cswap_co_z_points b (tplu_co_z_points P HPaff) in + let swap := testbit 1%Z in + let R1R0 := tplu_co_z_points P HPaff in (* loop *) - let '(R1R0, _) := - (@while (co_z_points*Z) (fun '(_, i) => (Z.ltb i scalarbitsz)) - (fun '(R1R0, i) => + let '(R1R0, swap, _) := + (@while (co_z_points*bool*Z) (fun '(_, _, i) => (Z.ltb i scalarbitsz)) + (fun '(R1R0, swap, i) => let b := testbit i in - let R1R0 := cswap_co_z_points b R1R0 in - let R1R0 := cswap_co_z_points b (zdau_co_z_points R1R0) in + let swap := xorb swap b in + let R1R0 := cswap_co_z_points swap R1R0 in + let R1R0 := zdau_co_z_points R1R0 in + let swap := b in let i := Z.succ i in - (R1R0, i)) - (Z.to_nat scalarbitsz) (* bound on loop iterations *) - (R1R0, 2%Z)) in + (R1R0, swap, i)) + (Z.to_nat scalarbitsz - 2) (* bound on loop iterations *) + (R1R0, swap, 2%Z)) in + let R1R0 := cswap_co_z_points swap R1R0 in snd (proj1_sig R1R0). (* Wrapper around joye_ladder_inner for points in affine coordinates, @@ -283,25 +286,28 @@ Module ScalarMult. (joye_ladder_inner bitsz testbit1 P HPaff). Proof. unfold joye_ladder_inner. - rewrite (surjective_pairing (while _ _ _ (cswap_co_z_points (testbit0 _) _, _))). - rewrite (surjective_pairing (while _ _ _ (cswap_co_z_points (testbit1 _) _, _))). + rewrite (surjective_pairing (while _ _ _ (_, testbit0 _, _))). + rewrite (surjective_pairing (while _ _ _ (_, testbit1 _, _))). + rewrite (surjective_pairing (fst (while _ _ _ (_, testbit0 _, _)))). + rewrite (surjective_pairing (fst (while _ _ _ (_, testbit1 _, _)))). rewrite bit0_irr by lia. match goal with - | |- eq (snd (proj1_sig (fst (while ?T0 ?B0 ?F0 ?I0)))) - (snd (proj1_sig (fst (while ?T1 ?B1 ?F1 ?I1)))) => + | |- eq (snd (proj1_sig (cswap_co_z_points (snd (fst (while ?T0 ?B0 ?F0 ?I0))) _))) + (snd (proj1_sig (cswap_co_z_points (snd (fst (while ?T1 ?B1 ?F1 ?I1))) _))) => set (test0 := T0); set (body0 := B0); set (fuel := F0); set (init0 := I0); set (body1 := B1) end. - apply (while.preservation test0 body0 test0 body1 (fun s1 s2 => eq (snd (proj1_sig (fst s1))) (snd (proj1_sig (fst s2))) /\ (s1 = s2 :> (co_z_points * Z)) /\ (2 <= snd s1)%Z)). - - intros s1 s2 (_ & <- & _). reflexivity. - - unfold test0. intros (PQ1 & i1) (PQ2 & i2) _. - cbn [fst snd]. intros (_ & Heq & Hi). inversion Heq; clear Heq. - subst PQ1; subst i1. + eelim (while.preservation test0 body0 test0 body1 (fun s1 s2 => (s1 = s2 :> (co_z_points * bool * Z)) /\ (2 <= snd s1)%Z)). + { intros A B. rewrite A. reflexivity. } + - intros s1 s2 (<- & _). reflexivity. + - unfold test0. intros ((PQ1 & b1) & i1) ((PQ2 & b2) & i2) _. + cbn [fst snd]. intros (Heq & Hi). inversion Heq; clear Heq. + subst PQ1; subst b1; subst i1. unfold body0, body1. rewrite bit0_irr by lia. - split; [reflexivity|split; [reflexivity|simpl; lia] ]. + split; [reflexivity|simpl; lia]. - repeat (split; try reflexivity). Qed. @@ -579,38 +585,37 @@ Module ScalarMult. rewrite (sig_eta (tplu_co_z_points _ _)) in Htplu. apply proj1_sig_eq in Htplu; simpl in Htplu. (* Initialize the ladder state with ([3]P, [1]P) or its symmetric *) - destruct (cswap_co_z_points (testbitn 1) _) as ((A3 & A4) & HA34) eqn:HA1. - rewrite (sig_eta (cswap_co_z_points _ _)) in HA1. - apply proj1_sig_eq in HA1. cbn [proj1_sig cswap_co_z_points] in HA1. - assert (A3 = (if testbitn 1 then A2 else A1) :> point) as HA3 by (destruct (testbitn 1); inversion HA1; auto). - assert (A4 = (if testbitn 1 then A1 else A2) :> point) as HA4 by (destruct (testbitn 1); inversion HA1; auto). - clear HA1. destruct (tplu_scalarmult' Htplu) as (HeqA1 & HeqA2 & _). + destruct (tplu_scalarmult' Htplu) as (HeqA1 & HeqA2 & _). set (inv := - fun '(R1R0, i) => + fun '(R1R0, swap, i) => let '(R1, R0) := proj1_sig (R1R0:co_z_points) in (2 <= i <= scalarbitsz)%Z /\ - (eq R1 (scalarmult' (TT n (Z.to_nat i)) P) - /\ eq R0 (scalarmult' (SS n (Z.to_nat i)) P)) - /\ ((i < scalarbitsz)%Z -> x_of R1 <> x_of R0)). + (eq (if (swap: bool) then R0 else R1) (scalarmult' (TT n (Z.to_nat i)) P) + /\ eq (if swap then R1 else R0) (scalarmult' (SS n (Z.to_nat i)) P)) + /\ ((i < scalarbitsz)%Z -> x_of R1 <> x_of R0) + /\ (swap = testbitn (i - 1) :> bool)). assert (HH : forall (A B : Prop), A -> (A -> B) -> A /\ B) by tauto. - assert (WWinv : inv WW /\ (snd WW = scalarbitsz :> Z)). - { set (measure := fun (state : (co_z_points*Z)) => ((Z.to_nat scalarbitsz) + 2 - (Z.to_nat (snd state)))%nat). - unfold WW. replace (Z.to_nat scalarbitsz) with (measure (exist _ (A3, A4) HA34, 2%Z)) by (unfold measure; simpl; lia). - eapply (while.by_invariant inv measure (fun s => inv s /\ (snd s = scalarbitsz :> Z))). + assert (WWinv : inv WW /\ (snd WW = scalarbitsz :> Z) /\ (snd (fst WW) = testbitn (scalarbitsz - 1) :> bool)). + { set (measure := fun (state : (co_z_points*bool*Z)) => ((Z.to_nat scalarbitsz) - (Z.to_nat (snd state)))%nat). + unfold WW. replace (Z.to_nat scalarbitsz - 2)%nat with (measure (exist _ (A1, A2) HA12, testbitn 1, 2%Z)) by (unfold measure; simpl; lia). + eapply (while.by_invariant inv measure (fun s => inv s /\ (snd s = scalarbitsz :> Z) /\ (snd (fst s) = testbitn (scalarbitsz - 1) :> bool))). - (* Invariant holds at beginning *) unfold inv. cbn [proj1_sig]. split; [lia|]. apply HH. + change (Z.to_nat 2) with 2%nat. - rewrite SS2, TT2, HA3, HA4. + rewrite SS2, TT2. case Z.testbit; auto. - + intros [He1 He2] Hxe. symmetry. - apply (SS_TT_xne 2%Z A4 A3 ltac:(apply co_z_comm; exact HA34) ltac:(lia)); eauto. + + intros [He1 He2]. split. + * intros Hxe. + generalize (SS_TT_xne 2%Z (if testbitn 1 then A1 else A2) (if testbitn 1 then A2 else A1) ltac:(destruct (testbitn 1); [|apply co_z_comm]; exact HA12) ltac:(lia) He2 He1). + case Z.testbit; [|symmetry]; auto. + * reflexivity. - (* Invariant is preserved by the loop, measure decreases, and post-condition i = scalarbitsz. *) - intros s Hs. destruct s as (R1R0 & i). + intros s Hs. destruct s as ((R1R0 & swap) & i). destruct R1R0 as ((R1 & R0) & HCOZ). - destruct Hs as (Hi & (HR1 & HR0) & Hx). + destruct Hs as (Hi & (HR1 & HR0) & Hx & Hswape). destruct (Z.ltb i scalarbitsz) eqn:Hltb. + apply Z.ltb_lt in Hltb. split. @@ -621,54 +626,55 @@ Module ScalarMult. (R1, R0) <- cswap (testbitn i) (R1, R0); *) (* Start by giving names to all intermediate values *) - unfold inv. destruct (cswap_co_z_points (testbitn i) (exist _ _ _)) as ((B1 & B2) & HB12) eqn:Hswap1. + unfold inv. destruct (cswap_co_z_points (xorb swap (testbitn i)) (exist _ _ _)) as ((B1 & B2) & HB12) eqn:Hswap1. rewrite (sig_eta (cswap_co_z_points _ _)) in Hswap1. apply proj1_sig_eq in Hswap1. simpl in Hswap1. - assert (HB1: B1 = (if testbitn i then R0 else R1) :> point) by (destruct (testbitn i); congruence). - assert (HB2: B2 = (if testbitn i then R1 else R0) :> point) by (destruct (testbitn i); congruence). + assert (HB1: B1 = (if xorb swap (testbitn i) then R0 else R1) :> point) by (destruct (xorb swap (testbitn i)); congruence). + assert (HB2: B2 = (if xorb swap (testbitn i) then R1 else R0) :> point) by (destruct (xorb swap (testbitn i)); congruence). clear Hswap1. destruct (zdau_co_z_points _) as ((C1 & C2) & HC12) eqn:HZDAU. rewrite (sig_eta (zdau_co_z_points _)) in HZDAU. apply proj1_sig_eq in HZDAU. simpl in HZDAU. - assert (HBx : x_of B1 <> x_of B2) by (rewrite HB1, HB2; destruct (testbitn i); [symmetry|]; auto). + assert (HBx : x_of B1 <> x_of B2) by (rewrite HB1, HB2; destruct (xorb swap (testbitn i)); [symmetry|]; auto). destruct (zaddu B1 B2 (zdau_co_z_points_obligation_1 (exist (fun '(A, B) => co_z A B) (B1, B2) HB12) B1 B2 eq_refl)) as (Y1 & Y2) eqn:HY. - assert (HYx : x_of Y1 <> x_of Y2) by (eapply zaddu_SS_TT; eauto; lia). + assert (HYx : x_of Y1 <> x_of Y2) by (eapply zaddu_SS_TT; eauto; try lia; destruct swap; destruct (testbitn i); auto). generalize (@Jacobian.zdau_correct_alt F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a b field char_ge_3 Feq_dec char_ge_12 ltac:(unfold id in *; fsatz) B1 B2 (zdau_co_z_points_obligation_1 (exist (fun '(A, B) => co_z A B) (B1, B2) HB12) B1 B2 eq_refl) HBx ltac:(rewrite HY; simpl; apply HYx)). rewrite HZDAU. intros (HC1 & HC2 & _). - destruct (cswap_co_z_points (testbitn i) _) as ((D1 & D2) & HD12) eqn:HD. - rewrite (sig_eta (cswap_co_z_points _ _)) in HD. - apply proj1_sig_eq in HD. cbn [proj1_sig cswap_co_z_points] in HD. - assert (HD1 : D1 = (if testbitn i then C2 else C1) :> point) by (destruct (testbitn i); congruence). - assert (HD2 : D2 = (if testbitn i then C1 else C2) :> point) by (destruct (testbitn i); congruence). - clear HD. simpl. + (* clear HD. *) simpl. (* invariant preservation *) (* counter still within bounds *) - split; [lia|]. rewrite HD1, HD2. apply HH. + split; [lia|]. (* rewrite HD1, HD2. *) apply HH. { (* New values are indeed [SS (i+1)]P and [TT (i+1)]P *) destruct (testbitn i) eqn:Hti; + destruct swap eqn:Hswap; rewrite <- HC1, <- HC2, HB1, HB2; replace (Z.to_nat (Z.succ i)) with (S (Z.to_nat i)) by lia; rewrite SS_succ, TT_succ, Z2Nat.id by lia; rewrite Hti; split; try assumption; rewrite <- Jacobian.add_double; try reflexivity; - rewrite HR0, HR1; + cbv [xorb]; rewrite HR0, HR1; repeat rewrite <- (scalarmult_add_l (groupG:=Pgroup) (mul_is_scalarmult:=scalarmult_ref_is_scalarmult (groupG:=Pgroup))); rewrite <- Z.add_diag; reflexivity. } { (* Make sure we don't hit bad values *) - intros [He1 He2] Hxe. symmetry. eapply (SS_TT_xne (Z.succ i)); eauto. + intros [He1 He2]. + split; [|f_equal; lia]. + intros Hxe He. eapply (SS_TT_xne (Z.succ i) (if testbitn i then C1 else C2) (if testbitn i then C2 else C1)); eauto. - destruct (testbitn i); [|apply co_z_comm]; auto. - - lia. } + - lia. + - destruct (testbitn i); [|symmetry]; auto. + } * (* measure decreases *) apply Z.ltb_lt in Hltb. unfold measure; simpl; lia. + (* Post-condition *) simpl; split; auto. - rewrite Z.ltb_nlt in Hltb. lia. } - destruct WWinv as (Hinv & Hj). - destruct WW as (R1R0 & i). destruct R1R0 as ((R1 & R0) & HCOZ). - simpl in Hj; subst i. destruct Hinv as (_ & (_ & HR0) & _). + rewrite Z.ltb_nlt in Hltb. split; [|rewrite Hswape; f_equal]; try lia. } + destruct WWinv as (Hinv & Hj & Hswap). + destruct WW as ((R1R0 & swap) & i). destruct R1R0 as ((R1 & R0) & HCOZ). + simpl in Hj; subst i. simpl in Hswap; subst swap. + destruct Hinv as (_ & (_ & HR0) & _). rewrite (SSn n scalarbitsz ltac:(lia) ltac:(lia)) in HR0. - exact HR0. + simpl. destruct (testbitn (scalarbitsz - 1)); simpl; exact HR0. Qed. End Inner. From 1369d76d8038e859b265da49dff9032ddc994a71 Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Mon, 27 May 2024 11:15:11 +0200 Subject: [PATCH 10/10] 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). *)