diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-11-06 21:03:39 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-11-06 22:39:04 -0500 |
commit | 7ae2244439e0f8e72fcbbbb276aaa5f240509cb9 (patch) | |
tree | 6cd6ec4455418d64ced9e77064dd245e9f7cb569 /src | |
parent | 3dfd82f6493b8b38656b01b33a64921d01e6bdf6 (diff) |
move B_order_l and prime_q
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/Ed25519.v | 9 | ||||
-rw-r--r-- | src/MxDHRepChange.v | 157 | ||||
-rw-r--r-- | src/Spec/Ed25519.v | 6 | ||||
-rw-r--r-- | src/Specific/GF25519.v | 3 |
4 files changed, 165 insertions, 10 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index de6d39202..86c075e19 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -878,7 +878,6 @@ Proof. 2:vm_decide. apply dec_bool. vm_cast_no_check (eq_refl true). -Admitted. (* Time Qed. (* Finished transaction in 1646.167 secs (1645.753u,0.339s) (successful) *) *) Definition sign := @EdDSARepChange.sign E @@ -903,7 +902,7 @@ Definition sign := @EdDSARepChange.sign E (@ModularArithmetic.F.opp q) (@ModularArithmetic.F.add q) (@ModularArithmetic.F.sub q) (@ModularArithmetic.F.mul q) (@ModularArithmetic.F.inv q) (@ModularArithmetic.F.div q) (@PrimeFieldTheorems.F.field_modulo q prime_q) (@ModularArithmeticTheorems.F.eq_dec q) Spec.Ed25519.a - Spec.Ed25519.d curve_params) b H c n l B Eenc Senc (@ed25519 H) Erep ERepEnc SRep SC25519.SRepDecModL + Spec.Ed25519.d curve_params) b H c n l B Eenc Senc (@ed25519 H B_order_l ) Erep ERepEnc SRep SC25519.SRepDecModL SRepERepMul SRepEnc SC25519.SRepAdd SC25519.SRepMul ERepB SC25519.SRepDecModLShort. Let sign_correct : forall pk sk {mlen} (msg:Word.word mlen), sign pk sk _ msg = EdDSA.sign pk sk msg := @@ -922,7 +921,7 @@ Let sign_correct : forall pk sk {mlen} (msg:Word.word mlen), sign pk sk _ msg = (* B := *) B (* Eenc := *) Eenc (* Senc := *) Senc - (* prm := *) ed25519 + (* prm := *) (ed25519 B_order_l) (* Erep := *) Erep (* ErepEq := *) ExtendedCoordinates.Extended.eq (* ErepAdd := *) ErepAdd @@ -1448,7 +1447,7 @@ Let verify_correct : (* B := *) B (* Eenc := *) Eenc (* Senc := *) Senc - (* prm := *) ed25519 + (* prm := *) (ed25519 B_order_l) (* Proper_Eenc := *) (PointEncoding.Proper_encode_point (b:=b-1)) (* Edec := *) Edec (* eq_enc_E_iff := *) eq_enc_E_iff @@ -1480,4 +1479,4 @@ Let verify_correct : (* SRepDec_correct := *) SRepDec_correct . Let both_correct := (@sign_correct, @verify_correct). -Print Assumptions both_correct. +Print Assumptions both_correct.
\ No newline at end of file diff --git a/src/MxDHRepChange.v b/src/MxDHRepChange.v new file mode 100644 index 000000000..1b8427afa --- /dev/null +++ b/src/MxDHRepChange.v @@ -0,0 +1,157 @@ +Require Import Crypto.Spec.MxDH. +Require Import Crypto.Algebra. Import Monoid Group Ring Field. +Require Import Crypto.Util.Tuple. + +Section MxDHRepChange. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {Fcswap:bool->F*F->F*F->(F*F)*(F*F)} {Fa24:F} {tb1:nat->bool}. + Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} {impl_field:@Algebra.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} {Keq_dec:Decidable.DecidableRel Keq} {Kcswap:bool->K*K->K*K->(K*K)*(K*K)} {Ka24:K} {tb2:nat->bool}. + + Context {FtoK} {homom:@Ring.is_homomorphism F Feq Fone Fadd Fmul + K Keq Kone Kadd Kmul FtoK}. + Context {homomorphism_inv_zero:Keq (FtoK (Finv Fzero)) (Kinv Kzero)}. + Context {homomorphism_a24:Keq (FtoK Fa24) Ka24}. + Context {Fcswap_correct:forall b x y, Fcswap b x y = if b then (y,x) else (x,y)}. + Context {Kcswap_correct:forall b x y, Kcswap b x y = if b then (y,x) else (x,y)}. + Context {tb2_correct:forall i, tb2 i = tb1 i}. + + (* TODO: move to algebra *) + Lemma homomorphism_multiplicative_inverse_complete' x : Keq (FtoK (Finv x)) (Kinv (FtoK x)). + Proof. + eapply (homomorphism_multiplicative_inverse_complete). + intro J; rewrite J. rewrite homomorphism_inv_zero, homomorphism_id. + reflexivity. + Qed. + + Ltac t := + repeat ( + rewrite homomorphism_id || + rewrite homomorphism_one || + rewrite homomorphism_a24 || + rewrite homomorphism_sub || + rewrite homomorphism_add || + rewrite homomorphism_mul || + rewrite homomorphism_multiplicative_inverse_complete' || + reflexivity + ). + + Import Crypto.Util.Tactics. + Import List. + Import Coq.Classes.Morphisms. + + Global Instance Proper_ladderstep : + Proper (Keq ==> (fieldwise (n:=2) Keq) ==> fieldwise (n:=2) Keq ==> fieldwise (n:=2) (fieldwise (n:=2) Keq)) (@MxDH.ladderstep K Kadd Ksub Kmul Ka24). + Proof. + cbv [MxDH.ladderstep tuple tuple' fieldwise fieldwise' fst snd]; + repeat intro; destruct_head' prod; destruct_head' and; repeat split; + repeat match goal with [H:Keq ?x ?y |- _ ] => rewrite !H; clear H x end; reflexivity. + Qed. + + Lemma MxLadderstepRepChange u P Q Ku (Ku_correct:Keq (FtoK u) Ku): + fieldwise (n:=2) (fieldwise (n:=2) Keq) + ((Tuple.map (n:=2) (Tuple.map (n:=2) FtoK)) (@MxDH.ladderstep F Fadd Fsub Fmul Fa24 u P Q)) + (@MxDH.ladderstep K Kadd Ksub Kmul Ka24 Ku (Tuple.map (n:=2) FtoK P) (Tuple.map (n:=2) FtoK Q)). + Proof. + destruct P as [? ?], Q as [? ?]; cbv; repeat split; rewrite <-?Ku_correct; t. + Qed. + + Let loopiter_sig F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u : + { loopiter | @MxDH.montladder F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u = + let '(_, _, _) := MxDH.downto _ _ loopiter in _ } := exist _ _ eq_refl. + Let loopiter F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u := + Eval cbv [proj1_sig loopiter_sig] in ( + proj1_sig (loopiter_sig F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb u)). + + Let loopiter_phi s : ((K * K) * (K * K)) * bool := + (Tuple.map (n:=2) (Tuple.map (n:=2) FtoK) (fst s), snd s). + + Let loopiter_eq (a b: (((K * K) * (K * K)) * bool)) := + fieldwise (n:=2) (fieldwise (n:=2) Keq) (fst a) (fst b) /\ snd a = snd b. + + Local Instance Equivalence_loopiter_eq : Equivalence loopiter_eq. + Proof. + unfold loopiter_eq; split; repeat intro; + intuition (reflexivity||symmetry;eauto||etransitivity;symmetry;eauto). + Qed. + + Lemma MxLoopIterRepChange b Fu s i Ku (HKu:Keq (FtoK Fu) Ku) : loopiter_eq + (loopiter_phi (loopiter F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb1 Fu s i)) + (loopiter K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap b tb2 Ku (loopiter_phi s) i). + Proof. + destruct_head' prod; break_match. + simpl. + rewrite !Fcswap_correct, !Kcswap_correct, tb2_correct in *. + break_match; cbv [loopiter_eq loopiter_phi fst snd]; split; try reflexivity; + (etransitivity;[|etransitivity]; [ | eapply (MxLadderstepRepChange _ _ _ _ HKu) | ]; + match goal with Heqp:_ |- _ => rewrite <-Heqp; reflexivity end). + Qed. + + Global Instance Proper_fold_left {A RA B RB} : + Proper ((RA==>RB==>RA) ==> SetoidList.eqlistA RB ==> RA ==> RA) (@fold_left A B). + Proof. + intros ? ? ? ? ? Hl; induction Hl; repeat intro; [assumption|]. + simpl; cbv [Proper respectful] in *; eauto. + Qed. + + Lemma proj_fold_left {A B L} R {Equivalence_R:@Equivalence B R} (proj:A->B) step step' {Proper_step':(R ==> eq ==> R)%signature step' step'} (xs:list L) init init' (H0:R (proj init) init') (Hproj:forall x i, R (proj (step x i)) (step' (proj x) i)) : + R (proj (fold_left step xs init)) (fold_left step' xs init'). + Proof. + generalize dependent init; generalize dependent init'. + induction xs; [solve [eauto]|]. + repeat intro; simpl; rewrite IHxs by eauto. + f_equiv; eapply Proper_step'; eauto. + Qed. + + Global Instance Proper_downto {T R} {Equivalence_R:@Equivalence T R} : + Proper (R ==> Logic.eq ==> (R==>Logic.eq==>R) ==> R) MxDH.downto. + Proof. + intros s0 s0' Hs0 n' n Hn'; subst n'; generalize dependent s0; generalize dependent s0'. + induction n; repeat intro; [assumption|]. + unfold MxDH.downto; simpl. + eapply Proper_fold_left; try eassumption; try reflexivity. + cbv [Proper respectful] in *; eauto. + Qed. + + Global Instance Proper_loopiter a b c : + Proper (loopiter_eq ==> eq ==> loopiter_eq) (loopiter K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap a b c). + Proof. + unfold loopiter; intros [? ?] [? ?] [[[] []] ?] ? ? ?; cbv [fst snd] in * |-; subst. + repeat VerdiTactics.break_match; subst; repeat (VerdiTactics.find_injection; intros; subst). + split; [|reflexivity]. + etransitivity; [|etransitivity]; [ | eapply Proper_ladderstep | ]; + [eapply eq_subrelation; [ exact _ | symmetry; eassumption ] + | reflexivity | | + | eapply eq_subrelation; [exact _ | eassumption ] ]; + rewrite !Kcswap_correct in *; + match goal with [H: (if ?b then _ else _) = _ |- _] => destruct b end; + repeat (VerdiTactics.find_injection; intros; subst); + split; simpl; eauto. + Qed. + + Lemma MxDHRepChange b (x:F) : + Keq + (FtoK (@MxDH.montladder F Fzero Fone Fadd Fsub Fmul Finv Fa24 Fcswap b tb1 x)) + (@MxDH.montladder K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap b tb2 (FtoK x)). + Proof. + cbv [MxDH.montladder]. + repeat break_match. + assert (Hrel:loopiter_eq (loopiter_phi (p, p0, b0)) (p1, p3, b1)). + { + rewrite <-Heqp0; rewrite <-Heqp. + unfold MxDH.downto. + eapply (proj_fold_left (L:=nat) loopiter_eq loopiter_phi). + { eapply @Proper_loopiter. } + { cbv; repeat split; t. } + { intros; eapply MxLoopIterRepChange; reflexivity. } + } + { destruct_head' prod; destruct Hrel as [[[] []] ?]; simpl in *; subst. + rewrite !Fcswap_correct, !Kcswap_correct in *. + match goal with [H: (if ?b then _ else _) = _ |- _] => destruct b end; + repeat (VerdiTactics.find_injection; intros; subst); + repeat match goal with [H: Keq (FtoK ?x) (?kx)|- _ ] => rewrite <- H end; + t. + } + Grab Existential Variables. + exact 0. + exact 0. + Qed. +End MxDHRepChange.
\ No newline at end of file diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index d6873607f..aa904fc7e 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -71,15 +71,13 @@ Section Ed25519. let '(x,y) := E.coordinates P in Fencode (len:=b-1) y ++ bit (sign x). Definition Senc : Fl -> Word.word b := Fencode (len:=b). - (* TODO(andreser): prove this after we have fast scalar multplication *) - Axiom B_order_l : CompleteEdwardsCurveTheorems.E.eq (BinInt.Z.to_nat l * B)%E E.zero. - Require Import Crypto.Util.Decidable. Definition ed25519 : + CompleteEdwardsCurveTheorems.E.eq (BinInt.Z.to_nat l * B)%E E.zero -> (* TODO: prove this earlier than Experiments/Ed25519? *) EdDSA (E:=E) (Eadd:=E.add) (Ezero:=E.zero) (EscalarMult:=E.mul) (B:=B) (Eopp:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.opp) (* TODO: move defn *) (Eeq:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.eq) (* TODO: move defn *) (l:=l) (b:=b) (n:=n) (c:=c) (Eenc:=Eenc) (Senc:=Senc) (H:=H). - Proof. split; try exact _; try exact B_order_l; vm_decide. Qed. + Proof. split; try (assumption || exact _); vm_decide. Qed. End Ed25519.
\ No newline at end of file diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 0a487b1e2..2c0365fd2 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -14,6 +14,7 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Decidable. Require Import Crypto.Algebra. +Require Crypto.Spec.Ed25519. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. Local Open Scope Z. @@ -21,7 +22,7 @@ Local Open Scope Z. (* BEGIN precomputation. *) Definition modulus : Z := Eval compute in 2^255 - 19. -Lemma prime_modulus : prime modulus. Admitted. +Definition prime_modulus : prime modulus := Crypto.Spec.Ed25519.prime_q. Definition int_width := 64%Z. Definition freeze_input_bound := 32%Z. |