From 35f6dc5d1a6f4b69cf9e1f7f8ef53a83bc11757d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 18 May 2016 12:39:51 -0400 Subject: slightly nicer edwards curve extended coordinates addition --- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index e9c0313ab..e91bc084b 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -116,6 +116,8 @@ Section ExtendedCoordinates. repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence. Qed. + Definition twice_d := d + d. + Section TwistMinus1. Context (a_eq_minus1 : a = opp 1). (** Second equation from section 3.1, also and *) @@ -124,8 +126,8 @@ Section ExtendedCoordinates. let '(X2, Y2, Z2, T2) := P2 in let A := (Y1-X1)*(Y2-X2) in let B := (Y1+X1)*(Y2+X2) in - let C := T1*ZToField 2*d*T2 in - let D := Z1*ZToField 2 *Z2 in + let C := T1*twice_d*T2 in + let D := Z1*(Z2+Z2) in let E := B-A in let F := D-C in let G := D+C in @@ -139,13 +141,17 @@ Section ExtendedCoordinates. Local Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q). + Lemma F_mul_2_l : forall x : F q, ZToField 2 * x = x + x. + intros. ring. + Qed. + Lemma unifiedAddM1'_rep: forall P Q rP rQ, E.onCurve rP -> E.onCurve rQ -> P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (E.add' rP rQ). Proof. intros P Q rP rQ HoP HoQ HrP HrQ. pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d). pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d). - unfoldExtended; rewrite a_eq_minus1 in *; simpl in *. + unfoldExtended; unfold twice_d; rewrite a_eq_minus1 in *; simpl in *. repeat rewrite <-F_mul_2_l. repeat split; repeat apply (f_equal2 pair); try F_field; repeat split; auto; repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r, ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; -- cgit v1.2.3 From e935a6ec0f076fb8ea73bd4aa3e178b44e6d259e Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 18 May 2016 15:32:19 -0400 Subject: unifiedAddM1Rep_sig: almost there --- src/Specific/Ed25519.v | 58 ++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 42 insertions(+), 16 deletions(-) diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index fa1c44d08..996aabb21 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -225,25 +225,57 @@ Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. 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. +Create HintDb FRepOperations discriminated. +Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. + 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 unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. +Proof. + destruct a as [[[]]]; destruct b as [[[]]]. + eexists. + lazymatch goal with |- ?LHS = ?RHS :> ?T => + evar (e:T); replace LHS with e; [subst e|] + end. + unfold rep2E. cbv beta delta [unifiedAddM1']. + pose proof (rep2F_F2rep twice_d) as H; rewrite H; clear H. (* XXX: this is a hack -- rewrite misresolves typeclasses? *) + + { etransitivity; [|replace_let_in_with_Let_In; reflexivity]. + repeat ( + autorewrite with FRepOperations; + Let_In_rep2F; + eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [Proper respectful pointwise_relation]; intro]). + lazymatch goal with |- ?LHS = (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) => + change (LHS = (rep2E (((x, y), z), t))) + end. + reflexivity. } + + subst e. + reflexivity. (* FIXME: do not simpl the goal here, we want to keep the Let_In common subexpressions *) +Defined. + +(*Eval simpl in (fun x1 y1 z1 t1 x2 y2 z2 t2 => proj1_sig (unifiedAddM1Rep_sig (((x1, y1), z1), t1) (((x2, y2), z2), t2))). (* TODO: remove after debugging the fixme three lines above *) *) + +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). + +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. + Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. Proof. eexists; intros. @@ -492,21 +524,15 @@ Proof. 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. + reflexivity. } Unfocus. (* cbv beta iota delta [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q]. *) + reflexivity. } Unfocus. reflexivity. Admitted. -- cgit v1.2.3 From 275fd8922e925e55d279569cebcc6f20bcf302ff Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 18 May 2016 17:30:47 -0400 Subject: F: fermat inversion lemma refactor --- src/ModularArithmetic/PrimeFieldTheorems.v | 63 ++++++++++++++++++------------ 1 file changed, 37 insertions(+), 26 deletions(-) diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 8a69a0c54..2bde727c8 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -120,27 +120,6 @@ Section VariousModPrime. eauto using Fq_inv_unique'. Qed. - Let inv_fermat_powmod (x:Z) : Z := powmod q x (Z.to_N (q-2)). - Lemma FieldToZ_inv_efficient : 2 < q -> - forall x : F q, FieldToZ (inv x) = inv_fermat_powmod x. - Proof. - intros. - rewrite (fun pf => Fq_inv_unique (fun x : F q => ZToField (inv_fermat_powmod (FieldToZ x))) pf); - subst inv_fermat_powmod; intuition; rewrite powmod_Zpow_mod; - replace (Z.of_N (Z.to_N (q - 2))) with (q-2)%Z by (rewrite Z2N.id ; omega). - - (* inv in range *) rewrite FieldToZ_ZToField, Zmod_mod; reflexivity. - - (* inv 0 *) replace (FieldToZ 0) with 0%Z by auto. - rewrite Z.pow_0_l by omega. - rewrite Zmod_0_l; trivial. - - (* inv nonzero *) rewrite <- (fermat_inv q _ x0) by - (rewrite mod_FieldToZ; eauto using FieldToZ_nonzero). - rewrite <-(ZToField_FieldToZ x0). - rewrite <-ZToField_mul. - rewrite ZToField_FieldToZ. - apply ZToField_eqmod. - demod; reflexivity. - Qed. - Lemma Fq_mul_zero_why : forall a b : F q, a*b = 0 -> a = 0 \/ b = 0. intros. assert (Z := F_eq_dec a 0); destruct Z. @@ -194,6 +173,43 @@ Section VariousModPrime. + apply IHp; auto. Qed. + Lemma F_inv_0 : inv 0 = (0 : F q). + Proof. + destruct (@F_inv_spec q); auto. + Qed. + + Definition inv_fermat (x:F q) : F q := x ^ Z.to_N (q - 2)%Z. + Lemma Fq_inv_fermat: 2 < q -> forall x : F q, inv x = x ^ Z.to_N (q - 2)%Z. + Proof. + intros. + erewrite (Fq_inv_unique inv_fermat); trivial; split; intros; unfold inv_fermat. + { replace 2%N with (Z.to_N (Z.of_N 2))%N by auto. + rewrite Fq_pow_zero. admit. intro. + assert (Z.of_N (Z.to_N (q-2)) = 0%Z) by (rewrite H0; eauto); rewrite Z2N.id in *; omega. } + { clear x. rename x0 into x. pose proof (fermat_inv _ _ x) as Hf; forward Hf. + { pose proof @ZToField_FieldToZ; pose proof @ZToField_mod; congruence. } + specialize (Hf H1); clear H1. + rewrite <-(ZToField_FieldToZ x). + rewrite ZToField_pow. + replace (Z.of_N (Z.to_N (q - 2))) with (q-2)%Z by (rewrite Z2N.id ; omega). + rewrite <-ZToField_mul. + apply ZToField_eqmod. + rewrite Hf, Zmod_small by omega; reflexivity. + } + Qed. + Lemma Fq_inv_fermat_correct : 2 < q -> forall x : F q, inv_fermat x = inv x. + Proof. + unfold inv_fermat; intros. rewrite Fq_inv_fermat; auto. + Qed. + + Let inv_fermat_powmod (x:Z) : Z := powmod q x (Z.to_N (q-2)). + Lemma FieldToZ_inv_efficient : 2 < q -> + forall x : F q, FieldToZ (inv x) = inv_fermat_powmod x. + Proof. + unfold inv_fermat_powmod; intros. + rewrite Fq_inv_fermat, powmod_Zpow_mod, <-FieldToZ_pow_Zpow_mod; auto. + Qed. + Lemma F_minus_swap : forall x y : F q, x - y = 0 -> y - x = 0. Proof. intros ? ? eq_zero. @@ -249,11 +265,6 @@ Section VariousModPrime. intros; field. (* TODO: Warning: Collision between bound variables ... *) Qed. - Lemma F_inv_0 : inv 0 = (0 : F q). - Proof. - destruct (@F_inv_spec q); auto. - Qed. - Lemma F_div_opp_1 : forall x y : F q, (opp x / y = opp (x / y))%F. Proof. intros; destruct (F_eq_dec y 0); [subst;unfold div;rewrite !F_inv_0|]; field. -- cgit v1.2.3 From 7fcbb62c515ad973f43a43a73f8ea821e63e3ff6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 18 May 2016 17:50:48 -0400 Subject: F: pow_nat_iter_op_correct --- src/ModularArithmetic/ModularArithmeticTheorems.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 8b1ae9f93..dabfcf883 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -6,6 +6,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *) Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. +Require Export Crypto.Util.IterAssocOp. Section ModularArithmeticPreliminaries. Context {m:Z}. @@ -209,6 +210,14 @@ Section FandZ. reflexivity. Qed. + Lemma pow_nat_iter_op_correct: forall (x:F m) n, (nat_iter_op mul 1) (N.to_nat n) x = x^n. + Proof. + induction n using N.peano_ind; + destruct (F_pow_spec x) as [pow_0 pow_succ]; + rewrite ?N2Nat.inj_succ, ?pow_0, <-?N.add_1_l, ?pow_succ; + simpl; congruence. + Qed. + Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m -> b mod m = (- a) mod m. Proof. -- cgit v1.2.3 From de5416133dc67dcd2729d4c7448991ab2672782a Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 24 May 2016 00:32:09 -0400 Subject: F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more broken... --- _CoqProject | 6 +- src/Rep.v | 13 + src/Specific/Ed25519.v | 663 ++++++++++++++++++++++++------------------------- src/Specific/GF25519.v | 98 +++++++- 4 files changed, 444 insertions(+), 336 deletions(-) create mode 100644 src/Rep.v diff --git a/_CoqProject b/_CoqProject index 1046bef3c..416b29176 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,6 +2,8 @@ src/BaseSystem.v src/BaseSystemProofs.v src/EdDSAProofs.v +src/Rep.v +src/Testbit.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v src/CompleteEdwardsCurve/DoubleAndAdd.v src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -10,6 +12,7 @@ src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v src/Encoding/PointEncodingPre.v +src/Encoding/PointEncodingTheorems.v src/ModularArithmetic/ExtendedBaseVector.v src/ModularArithmetic/FField.v src/ModularArithmetic/FNsatz.v @@ -31,10 +34,9 @@ src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v src/Spec/PointEncoding.v src/Specific/Ed25519.v -src/Specific/GF25519.v src/Specific/GF1305.v +src/Specific/GF25519.v src/Tactics/VerdiTactics.v -src/Testbit.v src/Util/CaseUtil.v src/Util/IterAssocOp.v src/Util/ListUtil.v diff --git a/src/Rep.v b/src/Rep.v new file mode 100644 index 000000000..b7e7f10c5 --- /dev/null +++ b/src/Rep.v @@ -0,0 +1,13 @@ +Class RepConversions (T:Type) (RT:Type) : Type := + { + toRep : T -> RT; + unRep : RT -> T + }. + +Definition RepConversionsOK {T RT} (RC:RepConversions T RT) := forall x, unRep (toRep x) = x. + +Definition RepFunOK {T RT} `(RC:RepConversions T RT) (f:T->T) (rf : RT -> RT) := + forall x, f (unRep x) = unRep (rf x). + +Definition RepBinOpOK {T RT} `(RC:RepConversions T RT) (op:T->T->T) (rop : RT -> RT -> RT) := + forall x y, op (unRep x) (unRep y) = unRep (rop x y). diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 996aabb21..3db14f057 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -9,7 +9,7 @@ Require Import Crypto.Encoding.PointEncodingPre. Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.PointEncoding. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil. +Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil Crypto.Rep. Local Infix "++" := Word.combine. Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40). @@ -184,355 +184,352 @@ Definition enc'_correct : @enc (@E.point curve25519params) _ _ = (fun x => enc' => 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 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 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. - -Create HintDb FRepOperations discriminated. -Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. - -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 unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. -Proof. - destruct a as [[[]]]; destruct b as [[[]]]. - eexists. - lazymatch goal with |- ?LHS = ?RHS :> ?T => - evar (e:T); replace LHS with e; [subst e|] - end. - unfold rep2E. cbv beta delta [unifiedAddM1']. - pose proof (rep2F_F2rep twice_d) as H; rewrite H; clear H. (* XXX: this is a hack -- rewrite misresolves typeclasses? *) - - { etransitivity; [|replace_let_in_with_Let_In; reflexivity]. - repeat ( - autorewrite with FRepOperations; - Let_In_rep2F; - eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [Proper respectful pointwise_relation]; intro]). - lazymatch goal with |- ?LHS = (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) => - change (LHS = (rep2E (((x, y), z), t))) - end. - reflexivity. } - - subst e. - reflexivity. (* FIXME: do not simpl the goal here, we want to keep the Let_In common subexpressions *) -Defined. - -(*Eval simpl in (fun x1 y1 z1 t1 x2 y2 z2 t2 => proj1_sig (unifiedAddM1Rep_sig (((x1, y1), z1), t1) (((x2, y2), z2), t2))). (* TODO: remove after debugging the fixme three lines above *) *) +Section Ed25519Frep. + Generalizable All Variables. + Context `(rcS:RepConversions N SRep) (rcSOK:RepConversionsOK rcS). + Context `(rcF:RepConversions (F (Ed25519.q)) FRep) (rcFOK:RepConversionsOK rcF). + Context (FRepAdd FRepSub FRepMul:FRep->FRep->FRep) (FRepAdd_correct:RepBinOpOK rcF add FRepMul). + Context (FRepSub_correct:RepBinOpOK rcF sub FRepSub) (FRepMul_correct:RepBinOpOK rcF mul FRepMul). + Local Notation rep2F := (unRep : FRep -> F (Ed25519.q)). + Local Notation F2Rep := (toRep : F (Ed25519.q) -> FRep). + Local Notation rep2S := (unRep : SRep -> N). + Local Notation S2Rep := (toRep : N -> SRep). + + 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). -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). + Axiom wltu : forall {b}, word b -> word b -> bool. + Axiom wltu_correct : forall {b} (x y:word b), wltu x y = (wordToN x 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. + Axiom compare_enc : forall x y, F_eqb x y = weqb (@enc _ _ FqEncoding x) (@enc _ _ FqEncoding y). -Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. -Proof. - eexists; intros. - cbv [ed25519_verify EdDSA.verify - ed25519params curve25519params - EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H - EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding]. + Axiom wire2FRep : word (b-1) -> option FRep. + Axiom wire2FRep_correct : forall x, Fm_dec x = option_map rep2F (wire2FRep x). - etransitivity. - Focus 2. - { repeat match goal with - | [ |- ?x = ?x ] => reflexivity - | [ |- _ = match ?a with None => ?N | Some x => @?S x end :> ?T ] - => etransitivity; - [ - | refine (_ : option_rect (fun _ => T) _ N a = _); - let S' := match goal with |- option_rect _ ?S' _ _ = _ => S' end in - refine (option_rect (fun a' => option_rect (fun _ => T) S' N a' = match a' with None => N | Some x => S x end) - (fun x => _) _ a); intros; simpl @option_rect ]; - [ reflexivity | .. ] - end. - set_evars. - rewrite<- E.point_eqb_correct. - rewrite solve_for_R; unfold E.sub. - rewrite E.opp_mul. - let p1 := constr:(scalarMultM1_rep eq_refl) in - let p2 := constr:(unifiedAddM1_rep eq_refl) in - repeat match goal with - | |- context [(_ * E.opp ?P)%E] => - rewrite <-(unExtendedPoint_mkExtendedPoint P); - rewrite negateExtended_correct; - rewrite <-p1 - | |- context [(_ * ?P)%E] => - rewrite <-(unExtendedPoint_mkExtendedPoint P); - rewrite <-p1 - | _ => rewrite p2 - end; - rewrite ?Znat.Z_nat_N, <-?Word.wordToN_nat; - subst_evars; - reflexivity. - } Unfocus. - - etransitivity. - Focus 2. - { lazymatch goal with |- _ = option_rect _ _ ?false ?dec => - symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => Z.to_N x) _ false dec)] - end. - eapply option_rect_Proper_nd; [intro|reflexivity..]. + Axiom FRep2wire : FRep -> word (b-1). + Axiom FRep2wire_correct : forall x, FRep2wire 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 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. + + Create HintDb FRepOperations discriminated. + Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. + + Local Ltac Let_In_unRep := match goal with - | [ |- ?RHS = ?e ?v ] - => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in - unify e RHS' + | [ |- appcontext G[Let_In (unRep ?x) ?f] ] + => change (Let_In (unRep x) f) with (Let_In x (fun y => f (unRep y))); cbv beta end. - reflexivity. - } Unfocus. - rewrite <-decode_scalar_correct. - - etransitivity. - Focus 2. - { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). - symmetry; apply decode_test_encode_test. - } Unfocus. - rewrite enc'_correct. - cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1]. - (* 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..]). - set_evars. - repeat match goal with - | [ |- appcontext[@proj1_sig ?A ?P (@iter_op ?T ?f ?neutral ?T' ?testbit ?exp ?base ?bound)] ] - => erewrite (@iter_op_proj T _ _ (@proj1_sig _ _)) by reflexivity - end. - subst_evars. - reflexivity. } - Unfocus. - - cbv [mkExtendedPoint E.zero]. - unfold proj1_sig at 1 2 3 5 6 7 8. - rewrite B_proj. - - etransitivity. - Focus 2. - { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). - set_evars. - lazymatch goal with |- _ = option_rect _ _ ?false ?dec => - symmetry; etransitivity; [|eapply (option_rect_option_map (@proj1_sig _ _) _ false dec)] - end. - eapply option_rect_Proper_nd; [intro|reflexivity..]. - match goal with - | [ |- ?RHS = ?e ?v ] - => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in - unify e RHS' + Lemma unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. + Proof. + destruct a as [[[]]]; destruct b as [[[]]]. + eexists. + lazymatch goal with |- ?LHS = ?RHS :> ?T => + evar (e:T); replace LHS with e; [subst e|] end. - reflexivity. - } Unfocus. - - cbv [dec PointEncoding point_encoding]. - etransitivity. - Focus 2. - { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + unfold rep2E. cbv beta delta [unifiedAddM1']. + pose proof (rcFOK twice_d) as H; rewrite <-H; clear H. (* XXX: this is a hack -- rewrite misresolves typeclasses? *) + + { etransitivity; [|replace_let_in_with_Let_In; reflexivity]. + repeat ( + autorewrite with FRepOperations; + Let_In_unRep; + eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [Proper respectful pointwise_relation]; intro]). + lazymatch goal with |- ?LHS = (unRep ?x, unRep ?y, unRep ?z, unRep ?t) => + change (LHS = (rep2E (((x, y), z), t))) + end. + reflexivity. } + + subst e. + reflexivity. (* FIXME: do not simpl the goal here, we want to keep the Let_In common subexpressions *) + Defined. + + (*Eval simpl in (fun x1 y1 z1 t1 x2 y2 z2 t2 => proj1_sig (unifiedAddM1Rep_sig (((x1, y1), z1), t1) (((x2, y2), z2), t2))). (* TODO: remove after debugging the fixme three lines above *) *) + + 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). + + 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. + + Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. + Proof. + eexists; intros. + cbv [ed25519_verify EdDSA.verify + ed25519params curve25519params + EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H + EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding]. + + etransitivity. + Focus 2. + { repeat match goal with + | [ |- ?x = ?x ] => reflexivity + | [ |- _ = match ?a with None => ?N | Some x => @?S x end :> ?T ] + => etransitivity; + [ + | refine (_ : option_rect (fun _ => T) _ N a = _); + let S' := match goal with |- option_rect _ ?S' _ _ = _ => S' end in + refine (option_rect (fun a' => option_rect (fun _ => T) S' N a' = match a' with None => N | Some x => S x end) + (fun x => _) _ a); intros; simpl @option_rect ]; + [ reflexivity | .. ] + end. + set_evars. + rewrite<- E.point_eqb_correct. + rewrite solve_for_R; unfold E.sub. + rewrite E.opp_mul. + let p1 := constr:(scalarMultM1_rep eq_refl) in + let p2 := constr:(unifiedAddM1_rep eq_refl) in + repeat match goal with + | |- context [(_ * E.opp ?P)%E] => + rewrite <-(unExtendedPoint_mkExtendedPoint P); + rewrite negateExtended_correct; + rewrite <-p1 + | |- context [(_ * ?P)%E] => + rewrite <-(unExtendedPoint_mkExtendedPoint P); + rewrite <-p1 + | _ => rewrite p2 + end; + rewrite ?Znat.Z_nat_N, <-?Word.wordToN_nat; + subst_evars; + reflexivity. + } Unfocus. + + etransitivity. + Focus 2. + { lazymatch goal with |- _ = option_rect _ _ ?false ?dec => + symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => Z.to_N x) _ false dec)] + end. + eapply option_rect_Proper_nd; [intro|reflexivity..]. + match goal with + | [ |- ?RHS = ?e ?v ] + => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in + unify e RHS' + end. + reflexivity. + } Unfocus. + rewrite <-decode_scalar_correct. + + etransitivity. + Focus 2. + { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + symmetry; apply decode_test_encode_test. + } Unfocus. + + rewrite enc'_correct. + cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1]. + (* 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. - { apply f_equal. - symmetry. - apply point_dec_coordinates_correct. } + { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + set_evars. + repeat match goal with + | [ |- appcontext[@proj1_sig ?A ?P (@iter_op ?T ?f ?neutral ?T' ?testbit ?exp ?base ?bound)] ] + => erewrite (@iter_op_proj T _ _ (@proj1_sig _ _)) by reflexivity + end. + subst_evars. + reflexivity. } Unfocus. - reflexivity. } - Unfocus. - - cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. - - etransitivity. - Focus 2. { - do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro. + + cbv [mkExtendedPoint E.zero]. + unfold proj1_sig at 1 2 3 5 6 7 8. + rewrite B_proj. + etransitivity. Focus 2. - { apply f_equal. - lazymatch goal with - | [ |- _ = ?term :> ?T ] - => lazymatch term with (match ?a with None => ?N | Some x => @?S x end) - => let term' := constr:((option_rect (fun _ => T) S N) a) in - replace term with term' by reflexivity - end + { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + set_evars. + lazymatch goal with |- _ = option_rect _ _ ?false ?dec => + symmetry; etransitivity; [|eapply (option_rect_option_map (@proj1_sig _ _) _ false dec)] end. - reflexivity. } Unfocus. reflexivity. } Unfocus. - - etransitivity. - Focus 2. { - 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. - - 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. - } Unfocus. - - cbv iota beta delta [q d a]. - rewrite wire2rep_F_correct. + eapply option_rect_Proper_nd; [intro|reflexivity..]. + match goal with + | [ |- ?RHS = ?e ?v ] + => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in + unify e RHS' + end. + reflexivity. + } Unfocus. + + cbv [dec PointEncoding point_encoding]. + etransitivity. + Focus 2. + { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + etransitivity. + Focus 2. + { apply f_equal. + symmetry. + apply point_dec_coordinates_correct. } + Unfocus. + reflexivity. } + Unfocus. + + cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. + + etransitivity. + Focus 2. { + do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro. + etransitivity. + Focus 2. + { apply f_equal. + lazymatch goal with + | [ |- _ = ?term :> ?T ] + => lazymatch term with (match ?a with None => ?N | Some x => @?S x end) + => let term' := constr:((option_rect (fun _ => T) S N) a) in + replace term with term' by reflexivity + end + end. + reflexivity. } Unfocus. reflexivity. } Unfocus. + + etransitivity. + Focus 2. { + 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. + + 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. + } Unfocus. + + cbv iota beta delta [q d a]. - etransitivity. - Focus 2. { - 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 (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. - 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. + rewrite wire2FRep_correct. + + etransitivity. + Focus 2. { + 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 <-(rcFOK 1%F). + pattern Ed25519.d at 1. rewrite <-(rcFOK Ed25519.d) at 1. + pattern Ed25519.a at 1. rewrite <-(rcFOK Ed25519.a) at 1. + rewrite !FRepMul_correct. + rewrite !FRepSub_correct. + rewrite !unfoldDiv. + rewrite !FRepInv_correct. + rewrite !FRepMul_correct. + Let_In_unRep. + rewrite <-(rcSOK (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]. { + (* TODO: + rewrite <-pow_nat_iter_op_correct. + erewrite <-iter_op_spec. *) + rewrite FSRepPow_correct. + Let_In_unRep. + 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 <-!FRep2wire_correct. + rewrite <-(rcFOK 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. - 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 (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). - match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite (rep2F_F2rep x) end end. - match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite (rep2F_F2rep x) end end. + Let_In_unRep. + eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. + set_evars. + rewrite !F_pow_2_r. 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 + rewrite if_F_eq_dec_if_F_eqb. + rewrite compare_enc. + rewrite <-!FRep2wire_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 (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. - lazymatch goal with |- context [?X] => - lazymatch X with negateExtended' (rep2E ?E) => - replace X with (rep2E (((((FRepOpp (fst (fst (fst E)))), (snd (fst (fst E)))), (snd (fst E))), (FRepOpp (snd E))))) by (simpl; rewrite !FRepOpp_correct; reflexivity) - end 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. - rewrite <-erep2trep_correct; cbv beta delta [erep2trep]. + 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 <-(rcFOK 0%F). + rewrite <-(rcFOK 1%F). + match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite <-(rcFOK x) end end. + match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite <-(rcFOK x) end end. + autorewrite with FRepOperations. (* breaks reflexivity *) + 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 [?X] => + lazymatch X with negateExtended' (rep2E ?E) => + replace X with (rep2E (((((FRepOpp (fst (fst (fst E)))), (snd (fst (fst E)))), (snd (fst E))), (FRepOpp (snd E))))) by (simpl; autorewrite with FRepOperations; reflexivity) + end 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, <-erep2trep_correct; cbv beta delta [erep2trep]. + + (* reflexivity. } Unfocus. - + (* + cbv beta iota delta + [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd + point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q]. + *) reflexivity. } Unfocus. - (* - cbv beta iota delta - [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd - point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q]. - *) - reflexivity. } Unfocus. - reflexivity. -Admitted. + reflexivity. +*) + Admitted. + +End Ed25519Frep. \ No newline at end of file diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index b01e6280e..8aaf8caf6 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -7,6 +7,7 @@ Require Import Coq.Lists.List Crypto.Util.ListUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.BaseSystem. +Require Import Crypto.Rep. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. Local Open Scope Z. @@ -81,4 +82,99 @@ Proof. intros f g Hf Hg. pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg. compute_formula. -Defined. \ No newline at end of file +Defined. + +Definition F25519Rep := (Z * Z * Z * Z * Z * Z * Z * Z * Z * Z)%type. + +Definition F25519toRep (x:F (2^255 - 19)) : F25519Rep := (0, 0, 0, 0, 0, 0, 0, 0, 0, FieldToZ x)%Z. +Definition F25519unRep (rx:F25519Rep) := + let '(x9, x8, x7, x6, x5, x4, x3, x2, x1, x0) := rx in + ModularBaseSystem.decode [x0;x1;x2;x3;x4;x5;x6;x7;x8;x9]. + +Global Instance F25519RepConversions : RepConversions (F (2^255 - 19)) F25519Rep := + { + toRep := F25519toRep; + unRep := F25519unRep + }. + +Lemma F25519RepConversionsOK : RepConversionsOK F25519RepConversions. +Proof. + unfold F25519RepConversions, RepConversionsOK, unRep, toRep, F25519toRep, F25519unRep; intros. + change (ModularBaseSystem.decode (ModularBaseSystem.encode x) = x). + eauto using ModularBaseSystemProofs.rep_decode, ModularBaseSystemProofs.encode_rep. +Qed. + +Definition F25519Rep_mul (f g:F25519Rep) : F25519Rep. + refine ( + let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in + let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _). + (* FIXME: the r should not be present in generated code *) + pose (r := proj1_sig (GF25519Base25Point5_mul_reduce_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9)). + simpl in r. + unfold F25519Rep. + repeat let t' := (eval cbv beta delta [r] in r) in + lazymatch t' with Let_In ?arg ?f => + let x := fresh "x" in + refine (let x := arg in _); + let t'' := (eval cbv beta in (f x)) in + change (Let_In arg f) with t'' in r + end. + let t' := (eval cbv beta delta [r] in r) in + lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] => + clear r; + exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0) + end. +Time Defined. + +Lemma F25519_mul_OK : RepBinOpOK F25519RepConversions ModularArithmetic.mul F25519Rep_mul. + cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_mul toRep unRep F25519toRep F25519unRep]. + destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. + destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. + let E := constr:(GF25519Base25Point5_mul_reduce_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in + transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]]; + destruct E as [? r]; cbv [proj1_sig]. + cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. +Qed. + +Definition F25519Rep_add (f g:F25519Rep) : F25519Rep. + refine ( + let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in + let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _). + let t' := (eval simpl in (proj1_sig (GF25519Base25Point5_add_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9))) in + lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] => + exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0) + end. +Defined. + +Definition F25519Rep_sub (f g:F25519Rep) : F25519Rep. + refine ( + let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in + let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _). + let t' := (eval simpl in (proj1_sig (GF25519Base25Point5_sub_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9))) in + lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] => + exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0) + end. +Defined. + +Lemma F25519_add_OK : RepBinOpOK F25519RepConversions ModularArithmetic.add F25519Rep_add. + cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_add toRep unRep F25519toRep F25519unRep]. + destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. + destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. + let E := constr:(GF25519Base25Point5_add_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in + transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]]; + destruct E as [? r]; cbv [proj1_sig]. + cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. +Qed. + +Lemma F25519_sub_OK : RepBinOpOK F25519RepConversions ModularArithmetic.sub F25519Rep_sub. + cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_sub toRep unRep F25519toRep F25519unRep]. + destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. + destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. + let E := constr:(GF25519Base25Point5_sub_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in + transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]]; + destruct E as [? r]; cbv [proj1_sig]. + cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. +Qed. \ No newline at end of file -- cgit v1.2.3 From 324e99b1b8d057c00eea0b5133057e75adc821e3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 24 May 2016 11:46:01 -0400 Subject: Fix some issues in Ed25519 tactics - Use replace rather than refine to speed up [Defined] and make the tactics easier to read - Use [apply f_equal] in place of [reflexivity] for unknown presumably arcane reasons to satisfy Coq's unifier - Factor out some tactics into tactic scripts - Write a lemma to pull functions out of [Let_In] - Fix autoindentation in emacs by wrapping [Let_In_unRep] in parentheses (probably a ProofGeneral regexp gone wrong) - Write a kludgy tactic to unfold [proj1_sig] only when applied to [exist] (Pair programming with Andres) --- src/Specific/Ed25519.v | 197 ++++++++++++++++++++++++++++--------------------- 1 file changed, 112 insertions(+), 85 deletions(-) diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 3db14f057..6e61d0ae2 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -168,7 +168,7 @@ Definition enc'_correct : @enc (@E.point curve25519params) _ _ = (fun x => enc' clear; abstract (cbv [Let_In]; reflexivity) | ] - end. + end. Local Ltac replace_let_in_with_Let_In := repeat match goal with | [ |- context G[let x := ?y in @?z x] ] @@ -197,10 +197,10 @@ Section Ed25519Frep. 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). @@ -214,26 +214,34 @@ Section Ed25519Frep. Axiom FRep2wire : FRep -> word (b-1). Axiom FRep2wire_correct : forall x, FRep2wire 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 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. - + Create HintDb FRepOperations discriminated. Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. - + Local Ltac Let_In_unRep := match goal with | [ |- appcontext G[Let_In (unRep ?x) ?f] ] => change (Let_In (unRep x) f) with (Let_In x (fun y => f (unRep y))); cbv beta end. - + + + (** TODO: Move me *) + Lemma pull_Let_In {B C} (f : B -> C) A (v : A) (b : A -> B) + : Let_In v (fun v' => f (b v')) = f (Let_In v b). + Proof. + reflexivity. + Qed. + Lemma unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. Proof. destruct a as [[[]]]; destruct b as [[[]]]. @@ -243,7 +251,7 @@ Section Ed25519Frep. end. unfold rep2E. cbv beta delta [unifiedAddM1']. pose proof (rcFOK twice_d) as H; rewrite <-H; clear H. (* XXX: this is a hack -- rewrite misresolves typeclasses? *) - + { etransitivity; [|replace_let_in_with_Let_In; reflexivity]. repeat ( autorewrite with FRepOperations; @@ -253,16 +261,17 @@ Section Ed25519Frep. change (LHS = (rep2E (((x, y), z), t))) end. reflexivity. } - + subst e. - reflexivity. (* FIXME: do not simpl the goal here, we want to keep the Let_In common subexpressions *) + Local Opaque Let_In. + repeat setoid_rewrite (pull_Let_In rep2E). + Local Transparent Let_In. + reflexivity. Defined. - - (*Eval simpl in (fun x1 y1 z1 t1 x2 y2 z2 t2 => proj1_sig (unifiedAddM1Rep_sig (((x1, y1), z1), t1) (((x2, y2), z2), t2))). (* TODO: remove after debugging the fixme three lines above *) *) - + 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). - + 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). @@ -270,7 +279,38 @@ Section Ed25519Frep. unfold rep2T, rep2E, erep2trep, extendedToTwisted; destruct P as [[[]]]; simpl. rewrite !unfoldDiv, <-!FRepMul_correct, <-FRepInv_correct. reflexivity. Qed. - + + (** TODO: possibly move me, remove local *) + Local Ltac replace_option_match_with_option_rect := + idtac; + lazymatch goal with + | [ |- _ = ?RHS :> ?T ] + => lazymatch RHS with + | match ?a with None => ?N | Some x => @?S x end + => replace RHS with (option_rect (fun _ => T) S N a) by (destruct a; reflexivity) + end + end. + + (** TODO: Move me, remove Local *) + Definition proj1_sig_unmatched {A P} := @proj1_sig A P. + Definition proj1_sig_nounfold {A P} := @proj1_sig A P. + Definition proj1_sig_unfold {A P} := Eval cbv [proj1_sig] in @proj1_sig A P. + Local Ltac unfold_proj1_sig_exist := + (** Change the first [proj1_sig] into [proj1_sig_unmatched]; if it's applied to [exist], mark it as unfoldable, otherwise mark it as not unfoldable. Then repeat. Finally, unfold. *) + repeat (change @proj1_sig with @proj1_sig_unmatched at 1; + match goal with + | [ |- context[proj1_sig_unmatched (exist _ _ _)] ] + => change @proj1_sig_unmatched with @proj1_sig_unfold + | _ => change @proj1_sig_unmatched with @proj1_sig_nounfold + end); + (* [proj1_sig_nounfold] is a thin wrapper around [proj1_sig]; unfolding it restores [proj1_sig]. Unfolding [proj1_sig_nounfold] exposes the pattern match, which is reduced by ι. *) + cbv [proj1_sig_nounfold proj1_sig_unfold]. + + (** TODO: possibly move me, remove Local *) + Local Ltac reflexivity_when_unification_is_stupid_about_evars + := repeat first [ reflexivity + | apply f_equal ]. + Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. Proof. eexists; intros. @@ -278,19 +318,14 @@ Section Ed25519Frep. ed25519params curve25519params EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding]. - + etransitivity. Focus 2. { repeat match goal with | [ |- ?x = ?x ] => reflexivity - | [ |- _ = match ?a with None => ?N | Some x => @?S x end :> ?T ] - => etransitivity; - [ - | refine (_ : option_rect (fun _ => T) _ N a = _); - let S' := match goal with |- option_rect _ ?S' _ _ = _ => S' end in - refine (option_rect (fun a' => option_rect (fun _ => T) S' N a' = match a' with None => N | Some x => S x end) - (fun x => _) _ a); intros; simpl @option_rect ]; - [ reflexivity | .. ] + | _ => replace_option_match_with_option_rect + | [ |- _ = option_rect _ _ _ _ ] + => eapply option_rect_Proper_nd; [ intro | reflexivity.. ] end. set_evars. rewrite<- E.point_eqb_correct. @@ -300,63 +335,60 @@ Section Ed25519Frep. let p2 := constr:(unifiedAddM1_rep eq_refl) in repeat match goal with | |- context [(_ * E.opp ?P)%E] => - rewrite <-(unExtendedPoint_mkExtendedPoint P); - rewrite negateExtended_correct; - rewrite <-p1 + rewrite <-(unExtendedPoint_mkExtendedPoint P); + rewrite negateExtended_correct; + rewrite <-p1 | |- context [(_ * ?P)%E] => - rewrite <-(unExtendedPoint_mkExtendedPoint P); - rewrite <-p1 + rewrite <-(unExtendedPoint_mkExtendedPoint P); + rewrite <-p1 | _ => rewrite p2 end; rewrite ?Znat.Z_nat_N, <-?Word.wordToN_nat; subst_evars; reflexivity. - } Unfocus. - + } Unfocus. + etransitivity. Focus 2. { lazymatch goal with |- _ = option_rect _ _ ?false ?dec => - symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => Z.to_N x) _ false dec)] + symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => Z.to_N x) _ false dec)] end. eapply option_rect_Proper_nd; [intro|reflexivity..]. match goal with | [ |- ?RHS = ?e ?v ] => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in - unify e RHS' + unify e RHS' end. reflexivity. } Unfocus. rewrite <-decode_scalar_correct. - + etransitivity. Focus 2. { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). symmetry; apply decode_test_encode_test. } Unfocus. - + rewrite enc'_correct. cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1]. - (* Why does this take too long? - lazymatch goal with |- context [ proj1_sig ?x ] => - fail 5 - end. *) - unfold proj1_sig at 1 2. + unfold_proj1_sig_exist. + etransitivity. Focus 2. { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). set_evars. repeat match goal with | [ |- appcontext[@proj1_sig ?A ?P (@iter_op ?T ?f ?neutral ?T' ?testbit ?exp ?base ?bound)] ] - => erewrite (@iter_op_proj T _ _ (@proj1_sig _ _)) by reflexivity + => erewrite (@iter_op_proj T _ _ (@proj1_sig _ _)) by reflexivity end. subst_evars. reflexivity. } Unfocus. - + cbv [mkExtendedPoint E.zero]. - unfold proj1_sig at 1 2 3 5 6 7 8. + unfold_proj1_sig_exist. rewrite B_proj. - + etransitivity. Focus 2. { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). @@ -368,11 +400,11 @@ Section Ed25519Frep. match goal with | [ |- ?RHS = ?e ?v ] => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in - unify e RHS' + unify e RHS' end. reflexivity. } Unfocus. - + cbv [dec PointEncoding point_encoding]. etransitivity. Focus 2. @@ -385,9 +417,9 @@ Section Ed25519Frep. Unfocus. reflexivity. } Unfocus. - + cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. - + etransitivity. Focus 2. { do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro. @@ -397,12 +429,12 @@ Section Ed25519Frep. lazymatch goal with | [ |- _ = ?term :> ?T ] => lazymatch term with (match ?a with None => ?N | Some x => @?S x end) - => let term' := constr:((option_rect (fun _ => T) S N) a) in - replace term with term' by reflexivity - end + => let term' := constr:((option_rect (fun _ => T) S N) a) in + replace term with term' by reflexivity + end end. - reflexivity. } Unfocus. reflexivity. } Unfocus. - + reflexivity. } Unfocus. reflexivity. } Unfocus. + etransitivity. Focus 2. { do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). @@ -411,7 +443,7 @@ Section Ed25519Frep. replace_let_in_with_Let_In. reflexivity. } Unfocus. - + etransitivity. Focus 2. { do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). @@ -427,8 +459,8 @@ Section Ed25519Frep. => 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 ] + [ + | destruct b; reflexivity ] | [ |- _ = if ?b then ?t else ?f ] => apply (f_equal2 (fun x y => if b then x else y)) | [ |- _ = false ] => reflexivity @@ -436,11 +468,11 @@ Section Ed25519Frep. end. reflexivity. } Unfocus. - + cbv iota beta delta [q d a]. rewrite wire2FRep_correct. - + etransitivity. Focus 2. { eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro. @@ -455,15 +487,15 @@ Section Ed25519Frep. rewrite !unfoldDiv. rewrite !FRepInv_correct. rewrite !FRepMul_correct. - Let_In_unRep. - rewrite <-(rcSOK (Z.to_N (Ed25519.q / 8 + 1))). + (Let_In_unRep). + rewrite <- (rcSOK (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]. { (* TODO: rewrite <-pow_nat_iter_op_correct. erewrite <-iter_op_spec. *) rewrite FSRepPow_correct. - Let_In_unRep. + (Let_In_unRep). etransitivity. Focus 2. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. { set_evars. rewrite !F_pow_2_r. @@ -478,7 +510,7 @@ Section Ed25519Frep. 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_unRep. + (Let_In_unRep). eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. set_evars. rewrite !F_pow_2_r. @@ -488,17 +520,17 @@ Section Ed25519Frep. rewrite <-!FRep2wire_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 (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 + 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. @@ -507,29 +539,24 @@ Section Ed25519Frep. rewrite <-(rcFOK 1%F). match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite <-(rcFOK x) end end. match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite <-(rcFOK x) end end. - autorewrite with FRepOperations. (* breaks reflexivity *) + autorewrite with FRepOperations. (* breaks reflexivity; use [reflexivity_when_unification_is_stupid_about_evars] instead *) + 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. + 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 [?X] => lazymatch X with negateExtended' (rep2E ?E) => - replace X with (rep2E (((((FRepOpp (fst (fst (fst E)))), (snd (fst (fst E)))), (snd (fst E))), (FRepOpp (snd E))))) by (simpl; autorewrite with FRepOperations; reflexivity) - end end; simpl fst; simpl snd. (* we actually only want to simpl in the with clause *) + replace X with (rep2E (((((FRepOpp (fst (fst (fst E)))), (snd (fst (fst E)))), (snd (fst E))), (FRepOpp (snd E))))) by (simpl; autorewrite with FRepOperations; reflexivity) + end 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, <-erep2trep_correct; cbv beta delta [erep2trep]. - (* - reflexivity. } Unfocus. - (* - cbv beta iota delta - [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd - point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q]. - *) + reflexivity_when_unification_is_stupid_about_evars. + } Unfocus. + reflexivity. } Unfocus. reflexivity. -*) - Admitted. - -End Ed25519Frep. \ No newline at end of file + Defined. +End Ed25519Frep. -- cgit v1.2.3 From 1c19d56200c1794a11efaef2d74bb764ed6d52d2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 24 May 2016 12:08:06 -0400 Subject: Remove unfolding, rewrite -> setoid_rewrite Moving the [scalar] argument to the beginning of [iter_op] makes inference of the [Proper] lemmas a bit easier. Making [Reflexive eq] come before [Reflexive Equivalence.equiv] allows [setoid_rewrite] to work; since [setoid_rewrite] does more unfolding than [rewrite], we no longer need to unfold things to make the [rewrite] work. --- src/Specific/Ed25519.v | 8 +++++--- src/Util/IterAssocOp.v | 10 +++++----- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 6e61d0ae2..ebecba606 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -311,6 +311,9 @@ Section Ed25519Frep. := repeat first [ reflexivity | apply f_equal ]. + + Local Existing Instance eq_Reflexive. (* To get some of the [setoid_rewrite]s below to work, we need to infer [Reflexive eq] before [Reflexive Equivalence.equiv] *) + Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. Proof. eexists; intros. @@ -534,9 +537,8 @@ Section Ed25519Frep. 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 <-(rcFOK 0%F). - rewrite <-(rcFOK 1%F). + setoid_rewrite <- (rcFOK 0%F). (* setoid_rewrite, to bypass needing to unfold things *) + setoid_rewrite <-(rcFOK 1%F). match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite <-(rcFOK x) end end. match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite <-(rcFOK x) end end. autorewrite with FRepOperations. (* breaks reflexivity; use [reflexivity_when_unification_is_stupid_about_evars] instead *) diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 5e23bb987..6116312e1 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -5,12 +5,12 @@ Local Open Scope equiv_scope. Generalizable All Variables. Section IterAssocOp. Context `{Equivalence T} + {scalar : Type} (op:T->T->T) {op_proper:Proper (equiv==>equiv==>equiv) op} (assoc: forall a b c, op a (op b c) === op (op a b) c) (neutral:T) (neutral_l : forall a, op neutral a === a) (neutral_r : forall a, op a neutral === a) - {scalar : Type} (testbit : scalar -> nat -> bool) (scToN : scalar -> N) (testbit_spec : forall x i, testbit x i = N.testbit_nat (scToN x) i). @@ -63,7 +63,7 @@ Section IterAssocOp. | S i' => (i', if testbit sc i' then op a acc2 else acc2) end. - Definition iter_op sc a bound : T := + Definition iter_op sc a bound : T := snd (funexp (test_and_op sc a) (bound, neutral) bound). Definition test_and_op_inv sc a (s : nat * T) := @@ -152,8 +152,8 @@ Section IterAssocOp. Lemma iter_op_termination : forall sc a bound, N.size_nat (scToN sc) <= bound -> - test_and_op_inv sc a - (funexp (test_and_op sc a) (bound, neutral) bound) -> + test_and_op_inv sc a + (funexp (test_and_op sc a) (bound, neutral) bound) -> iter_op sc a bound === nat_iter_op (N.to_nat (scToN sc)) a. Proof. unfold test_and_op_inv, iter_op; simpl; intros ? ? ? ? Hinv. @@ -183,7 +183,7 @@ Section IterAssocOp. rewrite Nat2N.id. auto. Qed. - + Lemma iter_op_spec : forall sc a bound, N.size_nat (scToN sc) <= bound -> iter_op sc a bound === nat_iter_op (N.to_nat (scToN sc)) a. Proof. -- cgit v1.2.3 From 6a59acc27e725056587d48e0e8393f0bf9850d74 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 24 May 2016 13:04:25 -0400 Subject: Factor some rewrites into a single [autorewrite] Slightly less [apply f_equal] beforehand, more automation. --- src/Specific/Ed25519.v | 58 ++++++++++++++++++++++++++++++-------------------- 1 file changed, 35 insertions(+), 23 deletions(-) diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index ebecba606..12f31beeb 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -228,6 +228,10 @@ Section Ed25519Frep. Create HintDb FRepOperations discriminated. Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. + Create HintDb EdDSA_opts discriminated. + Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : EdDSA_opts. + + Local Ltac Let_In_unRep := match goal with | [ |- appcontext G[Let_In (unRep ?x) ?f] ] @@ -314,6 +318,34 @@ Section Ed25519Frep. Local Existing Instance eq_Reflexive. (* To get some of the [setoid_rewrite]s below to work, we need to infer [Reflexive eq] before [Reflexive Equivalence.equiv] *) + (* TODO: move me *) + Lemma fold_rep2E x y z t + : (rep2F x, rep2F y, rep2F z, rep2F t) = rep2E (((x, y), z), t). + Proof. reflexivity. Qed. + Lemma commute_negateExtended'_rep2E x y z t + : negateExtended' (rep2E (((x, y), z), t)) + = rep2E (((FRepOpp x, y), z), FRepOpp t). + Proof. simpl; autorewrite with FRepOperations; reflexivity. Qed. + Lemma fold_rep2E_ffff x y z t + : (x, y, z, t) = rep2E (((toRep x, toRep y), toRep z), toRep t). + Proof. simpl; rewrite !rcFOK; reflexivity. Qed. + Lemma fold_rep2E_rrfr x y z t + : (rep2F x, rep2F y, z, rep2F t) = rep2E (((x, y), toRep z), t). + Proof. simpl; rewrite !rcFOK; reflexivity. Qed. + Lemma fold_rep2E_0fff y z t + : (0%F, y, z, t) = rep2E (((toRep 0%F, toRep y), toRep z), toRep t). + Proof. apply fold_rep2E_ffff. Qed. + Lemma fold_rep2E_ff1f x y t + : (x, y, 1%F, t) = rep2E (((toRep x, toRep y), toRep 1%F), toRep t). + Proof. apply fold_rep2E_ffff. Qed. + Lemma commute_negateExtended'_rep2E_rrfr x y z t + : negateExtended' (unRep x, unRep y, z, unRep t) + = rep2E (((FRepOpp x, y), toRep z), FRepOpp t). + Proof. rewrite <- commute_negateExtended'_rep2E; simpl; rewrite !rcFOK; reflexivity. Qed. + + Hint Rewrite @F_mul_0_l commute_negateExtended'_rep2E_rrfr fold_rep2E_0fff (@fold_rep2E_ff1f (fst (proj1_sig B))) : EdDSA_opts. + Hint Rewrite <- unifiedAddM1Rep_correct erep2trep_correct (fun x y z bound => iter_op_proj rep2E unifiedAddM1Rep unifiedAddM1' x y z N.testbit_nat bound unifiedAddM1Rep_correct) : EdDSA_opts. + Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. Proof. eexists; intros. @@ -534,29 +566,9 @@ Section Ed25519Frep. 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. - setoid_rewrite <- (rcFOK 0%F). (* setoid_rewrite, to bypass needing to unfold things *) - setoid_rewrite <-(rcFOK 1%F). - match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite <-(rcFOK x) end end. - match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite <-(rcFOK x) end end. - autorewrite with FRepOperations. (* breaks reflexivity; use [reflexivity_when_unification_is_stupid_about_evars] instead *) - - 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 [?X] => - lazymatch X with negateExtended' (rep2E ?E) => - replace X with (rep2E (((((FRepOpp (fst (fst (fst E)))), (snd (fst (fst E)))), (snd (fst E))), (FRepOpp (snd E))))) by (simpl; autorewrite with FRepOperations; reflexivity) - end 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, <-erep2trep_correct; cbv beta delta [erep2trep]. - - reflexivity_when_unification_is_stupid_about_evars. - } Unfocus. + unfold twistedToExtended. + autorewrite with EdDSA_opts. + progress cbv beta delta [erep2trep]. reflexivity. } Unfocus. reflexivity. -- cgit v1.2.3 From b9e60f74ff9378126a62cbe8f0981fc99c3dfca7 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 24 May 2016 14:09:47 -0400 Subject: PrimeFieldTheorems fermat inverse lemma: prove admit --- src/ModularArithmetic/PrimeFieldTheorems.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 2bde727c8..70a2c4a87 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -184,7 +184,7 @@ Section VariousModPrime. intros. erewrite (Fq_inv_unique inv_fermat); trivial; split; intros; unfold inv_fermat. { replace 2%N with (Z.to_N (Z.of_N 2))%N by auto. - rewrite Fq_pow_zero. admit. intro. + rewrite Fq_pow_zero. reflexivity. intro. assert (Z.of_N (Z.to_N (q-2)) = 0%Z) by (rewrite H0; eauto); rewrite Z2N.id in *; omega. } { clear x. rename x0 into x. pose proof (fermat_inv _ _ x) as Hf; forward Hf. { pose proof @ZToField_FieldToZ; pose proof @ZToField_mod; congruence. } -- cgit v1.2.3 From afcf7b625484c544d081a5a62a165e92598f62d3 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 24 May 2016 15:03:54 -0400 Subject: ed25519: continue refactor --- src/Specific/Ed25519.v | 73 ++++++++++++++++++++++---------------------------- 1 file changed, 32 insertions(+), 41 deletions(-) diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 12f31beeb..d9cfa6f05 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -225,13 +225,6 @@ Section Ed25519Frep. destruct b; trivial. Qed. - Create HintDb FRepOperations discriminated. - Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. - - Create HintDb EdDSA_opts discriminated. - Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : EdDSA_opts. - - Local Ltac Let_In_unRep := match goal with | [ |- appcontext G[Let_In (unRep ?x) ?f] ] @@ -246,6 +239,22 @@ Section Ed25519Frep. reflexivity. Qed. + Lemma Let_app_In {A B T} (g:A->B) (f:B->T) (x:A) : + @Let_In _ (fun _ => T) (g x) f = + @Let_In _ (fun _ => T) x (fun p => f (g x)). + Proof. reflexivity. Qed. + + Lemma Let_app2_In {A B C D T} (g1:A->C) (g2:B->D) (f:C*D->T) (x:A) (y:B) : + @Let_In _ (fun _ => T) (g1 x, g2 y) f = + @Let_In _ (fun _ => T) (x, y) (fun p => f ((g1 (fst p), g2 (snd p)))). + Proof. reflexivity. Qed. + + Create HintDb FRepOperations discriminated. + Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. + + Create HintDb EdDSA_opts discriminated. + Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : EdDSA_opts. + Lemma unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. Proof. destruct a as [[[]]]; destruct b as [[[]]]. @@ -343,8 +352,8 @@ Section Ed25519Frep. = rep2E (((FRepOpp x, y), toRep z), FRepOpp t). Proof. rewrite <- commute_negateExtended'_rep2E; simpl; rewrite !rcFOK; reflexivity. Qed. - Hint Rewrite @F_mul_0_l commute_negateExtended'_rep2E_rrfr fold_rep2E_0fff (@fold_rep2E_ff1f (fst (proj1_sig B))) : EdDSA_opts. - Hint Rewrite <- unifiedAddM1Rep_correct erep2trep_correct (fun x y z bound => iter_op_proj rep2E unifiedAddM1Rep unifiedAddM1' x y z N.testbit_nat bound unifiedAddM1Rep_correct) : EdDSA_opts. + Hint Rewrite @F_mul_0_l commute_negateExtended'_rep2E_rrfr fold_rep2E_0fff (@fold_rep2E_ff1f (fst (proj1_sig B))) @if_F_eq_dec_if_F_eqb compare_enc (if_map unRep) (fun T => Let_app2_In (T := T) unRep unRep) @F_pow_2_r @unfoldDiv : EdDSA_opts. + Hint Rewrite <- unifiedAddM1Rep_correct erep2trep_correct (fun x y z bound => iter_op_proj rep2E unifiedAddM1Rep unifiedAddM1' x y z N.testbit_nat bound unifiedAddM1Rep_correct) FRep2wire_correct: EdDSA_opts. Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. Proof. @@ -513,17 +522,13 @@ Section Ed25519Frep. 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. + autorewrite with EdDSA_opts. rewrite <-(rcFOK 1%F). pattern Ed25519.d at 1. rewrite <-(rcFOK Ed25519.d) at 1. pattern Ed25519.a at 1. rewrite <-(rcFOK Ed25519.a) at 1. - rewrite !FRepMul_correct. - rewrite !FRepSub_correct. - rewrite !unfoldDiv. - rewrite !FRepInv_correct. - rewrite !FRepMul_correct. - (Let_In_unRep). rewrite <- (rcSOK (Z.to_N (Ed25519.q / 8 + 1))). + autorewrite with EdDSA_opts. + (Let_In_unRep). 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]. { (* TODO: @@ -533,44 +538,30 @@ Section Ed25519Frep. (Let_In_unRep). 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 <-!FRep2wire_correct. rewrite <-(rcFOK sqrt_minus1). - rewrite !FRepMul_correct. - rewrite (if_map rep2F). + autorewrite with EdDSA_opts. subst_evars. reflexivity. } Unfocus. - match goal with |- ?e = Let_In ?xval (fun x => rep2F (@?f x)) => change (e = rep2F (Let_In xval f)) end. + rewrite pull_Let_In. reflexivity. } Unfocus. - (Let_In_unRep). - 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 <-!FRep2wire_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]. + (Let_In_unRep). + + subst_evars. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. set_evars. + + autorewrite with EdDSA_opts. - set_evars. - rewrite !FRepOpp_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. + lazymatch goal with |- _ = if ?b then ?t else ?f => apply (f_equal2 (fun x y => if b then x else y)) end; [|reflexivity]. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. + set_evars. unfold twistedToExtended. autorewrite with EdDSA_opts. progress cbv beta delta [erep2trep]. + subst_evars. reflexivity. } Unfocus. reflexivity. Defined. -End Ed25519Frep. +End Ed25519Frep. \ No newline at end of file -- cgit v1.2.3 From d735498028aca964c7b8d7aad74541df6c38fbcf Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 24 May 2016 16:07:32 -0400 Subject: ed25519: integrate FRepPow and FRepInv --- src/Specific/Ed25519.v | 34 ++++++++++++++++++++++++---------- 1 file changed, 24 insertions(+), 10 deletions(-) diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index d9cfa6f05..183ec8c78 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -195,12 +195,6 @@ Section Ed25519Frep. Local Notation rep2S := (unRep : SRep -> N). Local Notation S2Rep := (toRep : N -> SRep). - 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). @@ -215,6 +209,29 @@ Section Ed25519Frep. Axiom FRep2wire : FRep -> word (b-1). Axiom FRep2wire_correct : forall x, FRep2wire x = @enc _ _ FqEncoding (rep2F x). + Axiom SRep_testbit : SRep -> nat -> bool. + Axiom SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (unRep x0) i. + + Definition FSRepPow x n := iter_op FRepMul (toRep 1%F) SRep_testbit n x 255. + Lemma FSRepPow_correct : forall x n, (N.size_nat (unRep n) <= 255)%nat -> (unRep x ^ unRep n)%F = unRep (FSRepPow x n). + Proof. (* this proof derives the required formula, which I copy-pasted above to be able to reference it without the length precondition *) + unfold FSRepPow; intros. + erewrite <-pow_nat_iter_op_correct by auto. + erewrite <-(fun x => iter_op_spec (scalar := SRep) (mul (m:=Ed25519.q)) F_mul_assoc _ F_mul_1_l _ unRep SRep_testbit_correct n x 255%nat) by auto. + rewrite <-(rcFOK 1%F) at 1. + erewrite <-iter_op_proj by auto. + reflexivity. + Qed. + + Definition FRepInv x : FRep := FSRepPow x (S2Rep (Z.to_N (Ed25519.q - 2))). + Lemma FRepInv_correct : forall x, inv (rep2F x)%F = rep2F (FRepInv x). + unfold FRepInv; intros. + rewrite <-FSRepPow_correct; rewrite rcSOK; try reflexivity. + pose proof @Fq_inv_fermat_correct as H; unfold inv_fermat in H; rewrite H by + auto using Ed25519.prime_q, Ed25519.two_lt_q. + reflexivity. + Qed. + 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 := @@ -531,10 +548,7 @@ Section Ed25519Frep. (Let_In_unRep). 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]. { - (* TODO: - rewrite <-pow_nat_iter_op_correct. - erewrite <-iter_op_spec. *) - rewrite FSRepPow_correct. + rewrite FSRepPow_correct by (rewrite rcSOK; cbv; omega). (Let_In_unRep). etransitivity. Focus 2. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. { set_evars. -- cgit v1.2.3 From 29139b8da7c227ea81ab8daaefb81b3f3a5f7ada Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 24 May 2016 16:32:45 -0400 Subject: ed25519: indentation fix --- src/Specific/Ed25519.v | 76 +++++++++++++++++++++++++------------------------- 1 file changed, 38 insertions(+), 38 deletions(-) diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 183ec8c78..3b90b5cdf 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -145,44 +145,44 @@ Defined. Definition enc'_correct : @enc (@E.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. +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. Section Ed25519Frep. Generalizable All Variables. -- cgit v1.2.3