diff options
| -rw-r--r-- | _CoqProject | 6 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 12 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 9 | ||||
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 63 | ||||
| -rw-r--r-- | src/Rep.v | 13 | ||||
| -rw-r--r-- | src/Specific/Ed25519.v | 747 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 98 | ||||
| -rw-r--r-- | src/Util/IterAssocOp.v | 10 |
8 files changed, 582 insertions, 376 deletions
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/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 <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *) @@ -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; 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. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 8a69a0c54..70a2c4a87 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. 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. } + 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. 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 fa1c44d08..3b90b5cdf 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). @@ -145,368 +145,437 @@ 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. -Axiom SRep : Type. -Axiom S2rep : N -> SRep. -Axiom rep2S : SRep -> N. -Axiom rep2S_S2rep : forall x, x = rep2S (S2rep x). +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 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 wire2FRep : word (b-1) -> option FRep. + Axiom wire2FRep_correct : forall x, Fm_dec x = option_map rep2F (wire2FRep x). + + 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. -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). + Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed. -Axiom FRepMul : FRep -> FRep -> FRep. -Axiom FRepMul_correct : forall x y, (rep2F x * rep2F y)%F = rep2F (FRepMul x y). + 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. -Axiom FRepAdd : FRep -> FRep -> FRep. -Axiom FRepAdd_correct : forall x y, (rep2F x + rep2F y)%F = rep2F (FRepAdd x y). + 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. -Axiom FRepSub : FRep -> FRep -> FRep. -Axiom FRepSub_correct : forall x y, (rep2F x - rep2F y)%F = rep2F (FRepSub x y). + 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. -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). + (** 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 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 [[[]]]. + 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 (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. + Local Opaque Let_In. + repeat setoid_rewrite (pull_Let_In rep2E). + Local Transparent Let_In. + reflexivity. + Defined. + + 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. + + (** 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. -Axiom FRepOpp : FRep -> FRep. -Axiom FRepOpp_correct : forall x, opp (rep2F x) = rep2F (FRepOpp x). -Axiom wltu : forall {b}, word b -> word b -> bool. + (** 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 ]. + + + 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))) @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. + 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 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). + etransitivity. + Focus 2. + { repeat match goal with + | [ |- ?x = ?x ] => reflexivity + | _ => replace_option_match_with_option_rect + | [ |- _ = option_rect _ _ _ _ ] + => eapply option_rect_Proper_nd; [ intro | 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. -Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed. + 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. -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. + etransitivity. + Focus 2. + { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + symmetry; apply decode_test_encode_test. + } Unfocus. -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). + rewrite enc'_correct. + cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1]. + unfold_proj1_sig_exist. -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. + 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. -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. + cbv [mkExtendedPoint E.zero]. + unfold_proj1_sig_exist. + rewrite B_proj. -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; + 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' + end. 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. - { 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' - end. - reflexivity. - } Unfocus. - - cbv [dec PointEncoding point_encoding]. - etransitivity. - Focus 2. - { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + cbv [dec PointEncoding point_encoding]. etransitivity. Focus 2. - { apply f_equal. - symmetry. - apply point_dec_coordinates_correct. } + { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + etransitivity. + Focus 2. + { apply f_equal. + symmetry. + apply point_dec_coordinates_correct. } + Unfocus. + 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]. + 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]. - rewrite wire2rep_F_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 (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. + 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]. + + 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. + 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 <- (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]. { + 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. + rewrite <-(rcFOK sqrt_minus1). + autorewrite with EdDSA_opts. + subst_evars. + reflexivity. } Unfocus. + rewrite pull_Let_In. 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. + (Let_In_unRep). + + subst_evars. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. set_evars. + + autorewrite with EdDSA_opts. + + 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. - 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. - 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 [?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. - 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]. - *) - reflexivity. -Admitted. + autorewrite with EdDSA_opts. + progress cbv beta delta [erep2trep]. + + subst_evars. + reflexivity. } Unfocus. + reflexivity. + Defined. +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 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. |