From 7d73379213af07d6c36e48c91e6337e8b2f5777a Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Thu, 2 May 2024 16:00:33 +0200 Subject: [PATCH] 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. + +