diff options
Diffstat (limited to 'src/Specific/Ed25519.v')
| -rw-r--r-- | src/Specific/Ed25519.v | 369 |
1 files changed, 265 insertions, 104 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index f98bf2d12..50379b8d1 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -60,8 +60,9 @@ Qed. Axiom point_eqb : forall {prm : TwistedEdwardsParams}, point -> point -> bool. Axiom point_eqb_correct : forall P Q, point_eqb P Q = if point_eq_dec P Q then true else false. -Axiom Bc : F q * F q. -Axiom B_proj : proj1_sig B = Bc. +Axiom xB : F q. +Axiom yB : F q. +Axiom B_proj : proj1_sig B = (xB, yB). Require Import Coq.Setoids.Setoid. Require Import Coq.Classes.Morphisms. @@ -92,18 +93,36 @@ Axiom decode_scalar_correct : forall x, decode_scalar x = option_map (fun x : F Local Infix "==?" := point_eqb (at level 70) : E_scope. Local Infix "==?" := ModularArithmeticTheorems.F_eq_dec (at level 70) : F_scope. -Axiom negate : point -> point. +Axiom square_opp : forall (x:F q), (opp x ^ 2 = x ^ 2)%F. + +Program Definition negate (P:point) : point := let '(x, y) := proj1_sig P in (opp x, y). +Next Obligation. +Proof. + pose (proj2_sig P) as H; rewrite <-Heq_anonymous in H; simpl in H. + rewrite square_opp; trivial. +Qed. + Definition point_sub P Q := (P + negate Q)%E. Infix "-" := point_sub : E_scope. Axiom solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E. -Axiom negateExtendedc : extended -> extended. -Definition negateExtended : extendedPoint -> extendedPoint. +Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). +Local Notation "2" := (ZToField 2) : F_scope. + +Lemma mul_opp_1 : forall x y : F q, (opp x * y = opp (x * y))%F. +Admitted. + +Lemma div_opp_1 : forall x y : F q, (opp x / y = opp (x / y))%F. +Admitted. + +Definition negateExtended' P := let '(X, Y, Z, T) := P in (opp X, Y, Z, opp T). +Program Definition negateExtended (P:extendedPoint) : extendedPoint := negateExtended' (proj1_sig P). +Next Obligation. Proof. - intro x. - exists (negateExtendedc (proj1_sig x)). - admit. -Defined. + unfold negateExtended', rep; destruct P as [[X Y Z T] H]; simpl. destruct H as [[[] []] ?]; subst. + repeat rewrite ?div_opp_1, ?mul_opp_1, ?square_opp; repeat split; trivial. +Qed. + Axiom negateExtended_correct : forall P, negate (unExtendedPoint P) = unExtendedPoint (negateExtended P). Local Existing Instance PointEncoding. @@ -132,6 +151,105 @@ Defined. Definition enc'_correct : @enc (@point curve25519params) _ _ = (fun x => enc' (proj1_sig x)) := eq_refl. + Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. + Global Instance Let_In_Proper_nd {A P} + : Proper (eq ==> pointwise_relation _ eq ==> eq) (@Let_In A (fun _ => P)). + Proof. + lazy; intros; congruence. + Qed. + Lemma option_rect_function {A B C S' N' v} f + : f (option_rect (fun _ : option A => option B) S' N' v) + = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v. + Proof. destruct v; reflexivity. Qed. + Local Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect pattern matching *) + idtac; + lazymatch goal with + | [ |- ?LHS = option_rect ?P ?S ?N (Let_In ?x ?f) ] + => (* we want to just do a [change] here, but unification is stupid, so we have to tell it what to unfold in what order *) + cut (LHS = Let_In x (fun y => option_rect P S N (f y))); cbv beta; + [ set_evars; + let H := fresh in + intro H; + rewrite H; + clear; + abstract (cbv [Let_In]; reflexivity) + | ] + end. + Local Ltac replace_let_in_with_Let_In := + repeat match goal with + | [ |- context G[let x := ?y in @?z x] ] + => let G' := context G[Let_In y z] in change G' + | [ |- _ = Let_In _ _ ] + => apply Let_In_Proper_nd; [ reflexivity | cbv beta delta [pointwise_relation]; intro ] + end. + Local Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect _ _ _ (Some _)] *) + repeat match goal with + | [ |- context[option_rect ?P ?S ?N None] ] + => change (option_rect P S N None) with N + | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ] + => change (option_rect P S N (Some x)) with (S x); cbv beta + end. + +Axiom SRep : Type. +Axiom S2rep : N -> SRep. +Axiom rep2S : SRep -> N. +Axiom rep2S_S2rep : forall x, x = rep2S (S2rep x). + +Axiom FRep : Type. +Axiom F2rep : F Ed25519.q -> FRep. +Axiom rep2F : FRep -> F Ed25519.q. +Axiom rep2F_F2rep : forall x, x = rep2F (F2rep x). +Axiom wire2rep_F : word (b-1) -> option FRep. +Axiom wire2rep_F_correct : forall x, Fm_dec x = option_map rep2F (wire2rep_F x). + +Axiom FRepMul : FRep -> FRep -> FRep. +Axiom FRepMul_correct : forall x y, (rep2F x * rep2F y)%F = rep2F (FRepMul x y). + +Axiom FRepAdd : FRep -> FRep -> FRep. +Axiom FRepAdd_correct : forall x y, (rep2F x + rep2F y)%F = rep2F (FRepAdd x y). + +Axiom FRepSub : FRep -> FRep -> FRep. +Axiom FRepSub_correct : forall x y, (rep2F x - rep2F y)%F = rep2F (FRepSub x y). + +Axiom FRepInv : FRep -> FRep. +Axiom FRepInv_correct : forall x, inv (rep2F x)%F = rep2F (FRepInv x). + +Axiom FSRepPow : FRep -> SRep -> FRep. +Axiom FSRepPow_correct : forall x n, (rep2F x ^ rep2S n)%F = rep2F (FSRepPow x n). + +Axiom FRepOpp : FRep -> FRep. +Axiom FRepOpp_correct : forall x, opp (rep2F x) = rep2F (FRepOpp x). +Axiom wltu : forall {b}, word b -> word b -> bool. + +Axiom wltu_correct : forall {b} (x y:word b), wltu x y = (wordToN x <? wordToN y)%N. +Axiom compare_enc : forall x y, F_eqb x y = weqb (@enc _ _ FqEncoding x) (@enc _ _ FqEncoding y). +Axiom enc_rep2F : FRep -> word (b-1). +Axiom enc_rep2F_correct : forall x, enc_rep2F x = @enc _ _ FqEncoding (rep2F x). + +Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed. + +Definition rep2E (r:FRep * FRep * FRep * FRep) : extended := + match r with (((x, y), z), t) => mkExtended (rep2F x) (rep2F y) (rep2F z) (rep2F t) end. + +Lemma unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. +Proof. + unfold rep2E. cbv beta delta [unifiedAddM1']. + eexists; instantiate (1 := (((_,_), _), _)). +Admitted. +Definition unifiedAddM1Rep (a b:FRep * FRep * FRep * FRep) : FRep * FRep * FRep * FRep := Eval hnf in proj1_sig (unifiedAddM1Rep_sig a b). +Definition unifiedAddM1Rep_correct a b : rep2E (unifiedAddM1Rep a b) = unifiedAddM1' (rep2E a) (rep2E b) := Eval hnf in proj2_sig (unifiedAddM1Rep_sig a b). + +Lemma if_map : forall {T U} (f:T->U) (b:bool) (x y:T), (if b then f x else f y) = f (if b then x else y). +Proof. + destruct b; trivial. +Qed. + +Local Ltac Let_In_rep2F := + match goal with + | [ |- appcontext G[Let_In (rep2F ?x) ?f] ] + => change (Let_In (rep2F x) f) with (Let_In x (fun y => f (rep2F y))); cbv beta + end. + Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. Proof. eexists; intros. @@ -155,17 +273,20 @@ Proof. end. set_evars. rewrite<- point_eqb_correct. - rename x0 into R. rename x1 into S. rename x into A. - rewrite solve_for_R. + rewrite solve_for_R; unfold point_sub. + Axiom negate_scalarMult : forall n P, negate (scalarMult n P) = scalarMult n (negate P). + rewrite negate_scalarMult. let p1 := constr:(scalarMultM1_rep eq_refl) in let p2 := constr:(unifiedAddM1_rep eq_refl) in repeat match goal with + | |- context [(_ * negate ?P)%E] => + rewrite <-(unExtendedPoint_mkExtendedPoint P); + rewrite negateExtended_correct; + rewrite <-p1 | |- context [(_ * ?P)%E] => rewrite <-(unExtendedPoint_mkExtendedPoint P); - rewrite <-p1 - | |- context [(?P + unExtendedPoint _)%E] => - rewrite <-(unExtendedPoint_mkExtendedPoint P); - rewrite p2 + rewrite <-p1 + | _ => rewrite p2 end; rewrite ?Znat.Z_nat_N, <-?Word.wordToN_nat; subst_evars; @@ -193,17 +314,13 @@ Proof. symmetry; apply decode_test_encode_test. } Unfocus. - etransitivity. - Focus 2. - { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). - unfold point_sub. rewrite negateExtended_correct. - let p := constr:(unifiedAddM1_rep eq_refl) in rewrite p. - reflexivity. - } Unfocus. - rewrite enc'_correct. cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1]. - unfold proj1_sig at 1 2 5 6. + (* Why does this take too long? + lazymatch goal with |- context [ proj1_sig ?x ] => + fail 5 + end. *) + unfold proj1_sig at 1 2. etransitivity. Focus 2. { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). @@ -217,7 +334,7 @@ Proof. Unfocus. cbv [mkExtendedPoint zero mkPoint]. - unfold proj1_sig at 1 2 3 5 6 7. + unfold proj1_sig at 1 2 3 5 6 7 8. rewrite B_proj. etransitivity. @@ -249,20 +366,8 @@ Proof. reflexivity. } Unfocus. - Set Printing Depth 1000000. - Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). - Local Notation "2" := (ZToField 2) : F_scope. - cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding CompleteEdwardsCurveTheorems.solve_for_x2 sqrt_mod_q]. - Axiom FRep : Type. - Axiom F2rep : F Ed25519.q -> FRep. - Axiom rep2F : FRep -> F Ed25519.q. - Axiom rep2F_F2rep : forall x, x = rep2F (F2rep x). - Axiom wire2rep_F : word (b-1) -> option FRep. - Axiom wire2rep_F_correct : forall x, Fm_dec x = option_map rep2F (wire2rep_F x). - rewrite wire2rep_F_correct. - etransitivity. Focus 2. { do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro. @@ -277,83 +382,139 @@ Proof. end end. reflexivity. } Unfocus. reflexivity. } Unfocus. - rewrite <-!(option_rect_option_map rep2F). etransitivity. Focus 2. { - do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro. + do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). + do 1 (eapply option_rect_Proper_nd; [ intro; reflexivity | reflexivity | ]). + eapply option_rect_Proper_nd; [ cbv beta delta [pointwise_relation]; intro | reflexivity.. ]. + replace_let_in_with_Let_In. + reflexivity. + } Unfocus. - unfold option_rect at 1. - cbv beta iota delta [q d CompleteEdwardsCurve.a enc]. - let RHS' := constr:( - @option_rect FRep (fun _ : option FRep => bool) - (fun x : FRep => - let x2 := ((rep2F x ^ 2 - 1) / (Ed25519.d * rep2F x ^ 2 - Ed25519.a))%F in - let x0 := - let b := (x2 ^ Z.to_N (Ed25519.q / 8 + 1))%F in - if (b ^ 2 ==? x2)%F then b else (@sqrt_minus1 Ed25519.q * b)%F in - if (x0 ^ 2 ==? x2)%F - then - let p := - (if Bool.eqb (@whd (b - 1) pk) - (@wordToN (b - 1) (@Fm_enc Ed25519.q (b - 1) (@opp Ed25519.q x0)) <? - @wordToN (b - 1) (@Fm_enc Ed25519.q (b - 1) x0))%N - then x0 - else @opp Ed25519.q x0, rep2F x) in - @weqb (S (b - 1)) (sig [:b]) - (enc' - (@extendedToTwisted curve25519params - (@unifiedAddM1' curve25519params - (@iter_op (@extended curve25519params) - (@unifiedAddM1' curve25519params) - (@twistedToExtended curve25519params (0%F, 1%F)) - N N.testbit_nat - a - (@twistedToExtended curve25519params Bc) (N.size_nat a)) - (negateExtendedc - (@iter_op (@extended curve25519params) - (@unifiedAddM1' curve25519params) - (@twistedToExtended curve25519params (0%F, 1%F)) - N N.testbit_nat - (@wordToN (b + b) (@H (b + (b + l)) (sig [:b] ++ pk ++ msg))) - (twistedToExtended p) (N.size_nat (@wordToN (b + b) (@H (b + (b + l)) (sig [:b] ++ pk ++ msg))))))))) - else false) false - (wire2rep_F (@wtl (b - 1) pk)) - ) - in match goal with [ |- _ = ?RHS] => replace RHS with RHS' end. + etransitivity. + Focus 2. { + do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). + set_evars. + rewrite option_rect_function. (* turn the two option_rects into one *) + subst_evars. + simpl_option_rect. + do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). + (* push the [option_rect] inside until it hits a [Some] or a [None] *) + repeat match goal with + | _ => commute_option_rect_Let_In + | [ |- _ = Let_In _ _ ] + => apply Let_In_Proper_nd; [ reflexivity | cbv beta delta [pointwise_relation]; intro ] + | [ |- ?LHS = option_rect ?P ?S ?N (if ?b then ?t else ?f) ] + => transitivity (if b then option_rect P S N t else option_rect P S N f); + [ + | destruct b; reflexivity ] + | [ |- _ = if ?b then ?t else ?f ] + => apply (f_equal2 (fun x y => if b then x else y)) + | [ |- _ = false ] => reflexivity + | _ => progress simpl_option_rect + end. reflexivity. - { - unfold option_rect. - repeat progress match goal with [ |- context [match ?x with _ => _ end] ] => destruct x; trivial end. - } } Unfocus. - - Axiom FRepMul : FRep -> FRep -> FRep. - Axiom FRepMul_correct : forall x y, (rep2F x * rep2F y)%F = rep2F (FRepMul x y). - - Axiom FRepAdd : FRep -> FRep -> FRep. - Axiom FRepAdd_correct : forall x y, (rep2F x + rep2F y)%F = rep2F (FRepAdd x y). - - Axiom FRepSub : FRep -> FRep -> FRep. - Axiom FRepSub_correct : forall x y, (rep2F x - rep2F y)%F = rep2F (FRepSub x y). - - Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed. + + cbv iota beta delta [q d a]. + rewrite wire2rep_F_correct. etransitivity. Focus 2. { - do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro. - do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro. + eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro. + rewrite <-!(option_rect_option_map rep2F). + eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro. rewrite !F_pow_2_r. - rewrite !unfoldDiv. - rewrite (rep2F_F2rep Ed25519.d), (rep2F_F2rep Ed25519.a), (rep2F_F2rep 1%F). + rewrite (rep2F_F2rep 1%F). + pattern Ed25519.d at 1. rewrite (rep2F_F2rep Ed25519.d) at 1. + pattern Ed25519.a at 1. rewrite (rep2F_F2rep Ed25519.a) at 1. rewrite !FRepMul_correct. rewrite !FRepSub_correct. - cbv zeta. - rewrite F_pow_2_r. - - cbv beta delta [twistedToExtended]. - - cbv beta iota delta + rewrite !unfoldDiv. + rewrite !FRepInv_correct. + rewrite !FRepMul_correct. + Let_In_rep2F. + rewrite (rep2S_S2rep (Z.to_N (Ed25519.q / 8 + 1))). + eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. + etransitivity. Focus 2. eapply Let_In_Proper_nd; [|cbv beta delta [pointwise_relation]; intro;reflexivity]. { + rewrite FSRepPow_correct. + Let_In_rep2F. + etransitivity. Focus 2. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. { + set_evars. + rewrite !F_pow_2_r. + rewrite !FRepMul_correct. + rewrite if_F_eq_dec_if_F_eqb. + rewrite compare_enc. + rewrite <-!enc_rep2F_correct. + rewrite (rep2F_F2rep sqrt_minus1). + rewrite !FRepMul_correct. + rewrite (if_map rep2F). + subst_evars. + reflexivity. } Unfocus. + match goal with |- ?e = Let_In ?xval (fun x => rep2F (@?f x)) => change (e = rep2F (Let_In xval f)) end. + reflexivity. } Unfocus. + Let_In_rep2F. + eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. + set_evars. + rewrite !F_pow_2_r. + rewrite !FRepMul_correct. + rewrite if_F_eq_dec_if_F_eqb. + rewrite compare_enc. + rewrite <-!enc_rep2F_correct. + subst_evars. + lazymatch goal with |- _ = if ?b then ?t else ?f => apply (f_equal2 (fun x y => if b then x else y)) end; [|reflexivity]. + + set_evars. + rewrite !FRepOpp_correct. + rewrite <-!enc_rep2F_correct. + rewrite <-wltu_correct. + rewrite (if_map rep2F). + lazymatch goal with + |- ?e = Let_In (rep2F ?x, rep2F ?y) (fun p => @?r p) => + change (e = Let_In (x, y) (fun p => r (rep2F (fst p), rep2F (snd p)))); cbv beta zeta + end. + subst_evars. + eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. + + set_evars; erewrite (f_equal2 (@weqb b)); subst_evars; [|reflexivity|symmetry]. Focus 2. { + unfold twistedToExtended. + rewrite F_mul_0_l. + unfold curve25519params, q. (* TODO: do we really wanna do it here? *) + rewrite (rep2F_F2rep 0%F). + rewrite (rep2F_F2rep 1%F). + rewrite (rep2F_F2rep xB%F). + rewrite (rep2F_F2rep yB%F). + rewrite !FRepMul_correct. + repeat match goal with |- appcontext [ ?E ] => + match E with (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) => + change E with (rep2E (((x, y), z), t)) + end + end. + lazymatch goal with |- context [negateExtended' (rep2E ?E)] => + replace (negateExtended' (rep2E E)) with (rep2E (((((FRepOpp (fst (fst (fst E)))), (snd (fst (fst E)))), (snd (fst E))), (FRepOpp (snd E))))) by (simpl; rewrite !FRepOpp_correct; reflexivity) + end; simpl fst; simpl snd. (* we actually only want to simpl in the with clause *) + do 2 erewrite <- (fun x y z => iter_op_proj rep2E unifiedAddM1Rep unifiedAddM1' x y z N.testbit_nat) by apply unifiedAddM1Rep_correct. + rewrite <-unifiedAddM1Rep_correct. + + + etransitivity. Focus 2. { + apply f_equal. + Definition rep2T (P:FRep * FRep) := (rep2F (fst P), rep2F (snd P)). + Definition erep2trep (P:FRep * FRep * FRep * FRep) := Let_In P (fun P => Let_In (FRepInv (snd (fst P))) (fun iZ => (FRepMul (fst (fst (fst P))) iZ, FRepMul (snd (fst (fst P))) iZ))). + Lemma erep2trep_correct : forall P, rep2T (erep2trep P) = extendedToTwisted (rep2E P). + Proof. + unfold rep2T, rep2E, erep2trep, extendedToTwisted; destruct P as [[[]]]; simpl. + rewrite !unfoldDiv, <-!FRepMul_correct, <-FRepInv_correct. reflexivity. + Qed. + rewrite <-erep2trep_correct; cbv beta delta [erep2trep]. + reflexivity. } Unfocus. + + reflexivity. } Unfocus. + (* + cbv beta iota delta [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd - point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q ]. -Admitted. + point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q]. + *) + reflexivity. +Admitted.
\ No newline at end of file |