From 516227777307c260b13098e95f949b0f7958259f Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 27 May 2016 13:49:12 -0400 Subject: before changing SRep from N to F l --- src/Specific/Ed25519.v | 478 +++++++++++++++++++++++++++++++------------------ 1 file changed, 301 insertions(+), 177 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 3b90b5cdf..08f8a6448 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -1,5 +1,5 @@ Require Import Bedrock.Word. -Require Import Crypto.Spec.Ed25519. +Require Import Crypto.Spec.EdDSA. Require Import Crypto.Tactics.VerdiTactics. Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic. Require Import ModularArithmetic.ModularArithmeticTheorems. @@ -10,13 +10,10 @@ Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. 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). -Local Notation " a '[' i ':]' " := (Word.split2 i _ a) (at level 40). -Local Arguments H {_} _. -Local Arguments scalarMultM1 {_} {_} _ _ _. -Local Arguments unifiedAddM1 {_} {_} _ _. +Require Import Coq.Setoids.Setoid. +Require Import Coq.Classes.Morphisms. + +(*TODO: move enerything before the section out of this file *) Local Ltac set_evars := repeat match goal with @@ -27,6 +24,21 @@ Local Ltac subst_evars := | [ e := ?E |- _ ] => is_evar E; subst e 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. + +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. + Lemma funexp_proj {T T'} (proj : T -> T') (f : T -> T) (f' : T' -> T') x n (f_proj : forall a, proj (f a) = f' (proj a)) : proj (funexp f x n) = funexp f' (proj x) n. @@ -59,10 +71,6 @@ Proof. end. } Qed. -Lemma B_proj : proj1_sig B = (fst(proj1_sig B), snd(proj1_sig B)). destruct B as [[]]; reflexivity. Qed. - -Require Import Coq.Setoids.Setoid. -Require Import Coq.Classes.Morphisms. Global Instance option_rect_Proper_nd {A T} : Proper ((pointwise_relation _ eq) ==> eq ==> eq ==> eq) (@option_rect A (fun _ => T)). Proof. @@ -83,74 +91,6 @@ Proof. destruct v; reflexivity. Qed. -Axiom decode_scalar : word b -> option N. -Local Existing Instance Ed25519.FlEncoding. -Axiom decode_scalar_correct : forall x, decode_scalar x = option_map (fun x : F (Z.of_nat Ed25519.l) => Z.to_N x) (dec x). - -Local Infix "==?" := E.point_eqb (at level 70) : E_scope. -Local Infix "==?" := ModularArithmeticTheorems.F_eq_dec (at level 70) : F_scope. - -Lemma solve_for_R_eq : forall A B C, (A = B + C <-> B = A - C)%E. -Proof. - intros; split; intros; subst; unfold E.sub; - rewrite <-E.add_assoc, ?E.add_opp_r, ?E.add_opp_l, E.add_0_r; reflexivity. -Qed. - -Lemma solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E. -Proof. - intros. - repeat match goal with |- context [(?P ==? ?Q)%E] => - let H := fresh "H" in - destruct (E.point_eq_dec P Q) as [H|H]; - (rewrite (E.point_eqb_complete _ _ H) || rewrite (E.point_eqb_neq_complete _ _ H)) - end; rewrite solve_for_R_eq in H; congruence. -Qed. - -Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). -Local Notation "2" := (ZToField 2) : F_scope. - -Local Existing Instance PointEncoding. -Lemma decode_point_eq : forall (P_ Q_ : word (S (b-1))) (P Q:E.point), - dec P_ = Some P -> - dec Q_ = Some Q -> - weqb P_ Q_ = (P ==? Q)%E. -Proof. - intros. - replace P_ with (enc P) in * by (auto using encoding_canonical). - replace Q_ with (enc Q) in * by (auto using encoding_canonical). - rewrite E.point_eqb_correct. - edestruct E.point_eq_dec; (apply weqb_true_iff || apply weqb_false_iff); congruence. -Qed. - -Lemma decode_test_encode_test : forall S_ X, option_rect (fun _ : option E.point => bool) - (fun S : E.point => (S ==? X)%E) false (dec S_) = weqb S_ (enc X). -Proof. - intros. - destruct (dec S_) eqn:H. - { symmetry; eauto using decode_point_eq, encoding_valid. } - { simpl @option_rect. - destruct (weqb S_ (enc X)) eqn:Heqb; trivial. - apply weqb_true_iff in Heqb. subst. rewrite encoding_valid in H; discriminate. } -Qed. - -Definition enc' : F q * F q -> word b. -Proof. - intro x. - let enc' := (eval hnf in (@enc (@E.point curve25519params) _ _)) in - match (eval cbv [proj1_sig] in (fun pf => enc' (exist _ x pf))) with - | (fun _ => ?enc') => exact enc' - end. -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. @@ -169,13 +109,17 @@ Local Ltac commute_option_rect_Let_In := (* pull let binders out side of option_ 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. + +(** 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. 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] ] @@ -184,72 +128,255 @@ Local Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [optio => change (option_rect P S N (Some x)) with (S x); cbv beta end. -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). +Definition COMPILETIME {T} (x:T) : T := x. - 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 (N.to_nat a <= N.to_nat b)%nat. +Proof. + intros. + pose proof (Nomega.Nlt_out a (N.succ b)). + rewrite N2Nat.inj_succ, N.lt_succ_r, <-NPeano.Nat.lt_succ_r in *; auto. +Qed. +Lemma N_size_nat_le_mono : forall a b, (a <= b)%N -> (N.size_nat a <= N.size_nat b)%nat. +Proof. + intros. + destruct (N.eq_dec a 0), (N.eq_dec b 0); try abstract (subst;rewrite ?N.le_0_r in *;subst;simpl;omega). + rewrite !Nsize_nat_equiv, !N.size_log2 by assumption. + edestruct N.succ_le_mono; eauto using N_to_nat_le_mono, N.log2_le_mono. +Qed. - Axiom wire2FRep : word (b-1) -> option FRep. - Axiom wire2FRep_correct : forall x, Fm_dec x = option_map rep2F (wire2FRep x). +Lemma Z_to_N_Z_of_nat : forall n, Z.to_N (Z.of_nat n) = N.of_nat n. +Proof. induction n; auto. Qed. - Axiom FRep2wire : FRep -> word (b-1). - Axiom FRep2wire_correct : forall x, FRep2wire x = @enc _ _ FqEncoding (rep2F x). +Lemma Z_of_nat_nonzero : forall m, m <> 0 -> (0 < Z.of_nat m)%Z. +Proof. intros. destruct m; [congruence|reflexivity]. Qed. +Lemma N_of_nat_modulo : forall n m, m <> 0 -> N.of_nat (n mod m)%nat = (N.of_nat n mod N.of_nat m)%N. +Proof. + intros. + apply Znat.N2Z.inj_iff. + rewrite !Znat.nat_N_Z. + rewrite Zdiv.mod_Zmod by auto. + apply Znat.Z2N.inj_iff. + { apply Z.mod_pos_bound. apply Z_of_nat_nonzero. assumption. } + { apply Znat.N2Z.is_nonneg. } + rewrite Znat.Z2N.inj_mod by (auto using Znat.Nat2Z.is_nonneg, Z_of_nat_nonzero). + rewrite !Z_to_N_Z_of_nat, !Znat.N2Z.id; reflexivity. +Qed. + +Lemma encoding_canonical' {T} {B} {encoding:canonical encoding of T as B} : + forall a b, enc a = enc b -> a = b. +Proof. + intros. + pose proof (f_equal dec H). + pose proof encoding_valid. + pose proof encoding_canonical. + congruence. +Qed. + +Lemma compare_encodings {T} {B} {encoding:canonical encoding of T as B} + (B_eqb:B->B->bool) (B_eqb_iff : forall a b:B, (B_eqb a b = true) <-> a = b) + : forall a b : T, (a = b) <-> (B_eqb (enc a) (enc b) = true). +Proof. + intros. + split; intro H. + { rewrite B_eqb_iff; congruence. } + { apply B_eqb_iff in H; eauto using encoding_canonical'. } +Qed. + +Lemma eqb_eq_dec' {T} (eqb:T->T->bool) (eqb_iff:forall a b, eqb a b = true <-> a = b) : + forall a b, if eqb a b then a = b else a <> b. +Proof. + intros. + case_eq (eqb a b); intros. + { eapply eqb_iff; trivial. } + { specialize (eqb_iff a b). rewrite H in eqb_iff. intuition. } +Qed. + +Definition eqb_eq_dec {T} (eqb:T->T->bool) (eqb_iff:forall a b, eqb a b = true <-> a = b) : + forall a b : T, {a=b}+{a<>b}. +Proof. + intros. + pose proof (eqb_eq_dec' eqb eqb_iff a b). + destruct (eqb a b); eauto. +Qed. + +Definition eqb_eq_dec_and_output {T} (eqb:T->T->bool) (eqb_iff:forall a b, eqb a b = true <-> a = b) : + forall a b : T, {a = b /\ eqb a b = true}+{a<>b /\ eqb a b = false}. +Proof. + intros. + pose proof (eqb_eq_dec' eqb eqb_iff a b). + destruct (eqb a b); eauto. +Qed. + +Lemma eqb_compare_encodings {T} {B} {encoding:canonical encoding of T as B} + (T_eqb:T->T->bool) (T_eqb_iff : forall a b:T, (T_eqb a b = true) <-> a = b) + (B_eqb:B->B->bool) (B_eqb_iff : forall a b:B, (B_eqb a b = true) <-> a = b) + : forall a b : T, T_eqb a b = B_eqb (enc a) (enc b). +Proof. + intros; + destruct (eqb_eq_dec_and_output T_eqb T_eqb_iff a b); + destruct (eqb_eq_dec_and_output B_eqb B_eqb_iff (enc a) (enc b)); + intuition; + try find_copy_apply_lem_hyp B_eqb_iff; + try find_copy_apply_lem_hyp T_eqb_iff; + try congruence. + apply (compare_encodings B_eqb B_eqb_iff) in H2; congruence. +Qed. + +Lemma decode_failed_neq_encoding {T B} (encoding_T_B:canonical encoding of T as B) (X:B) + (dec_failed:dec X = None) (a:T) : X <> enc a. +Proof. pose proof encoding_valid. congruence. Qed. +Lemma compare_without_decoding {T B} (encoding_T_B:canonical encoding of T as B) + (T_eqb:T->T->bool) (T_eqb_iff:forall a b, T_eqb a b = true <-> a = b) + (B_eqb:B->B->bool) (B_eqb_iff:forall a b, B_eqb a b = true <-> a = b) + (P_:B) (Q:T) : + option_rect (fun _ : option T => bool) + (fun P : T => T_eqb P Q) + false + (dec P_) + = B_eqb P_ (enc Q). +Proof. + destruct (dec P_) eqn:Hdec; simpl option_rect. + { apply encoding_canonical in Hdec; subst; auto using eqb_compare_encodings. } + { pose proof encoding_canonical. + pose proof encoding_valid. + pose proof eqb_compare_encodings. + eapply decode_failed_neq_encoding in Hdec. + destruct (B_eqb P_ (enc Q)) eqn:Heq; [rewrite B_eqb_iff in Heq; eauto | trivial]. } +Qed. + +Generalizable All Variables. +Section FSRepOperations. + Context {q:Z} {prime_q:Znumtheory.prime q} {two_lt_q:(2 < q)%Z}. + Context `(rcS:RepConversions N SRep) (rcSOK:RepConversionsOK rcS). + Context `(rcF:RepConversions (F 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). 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). + Definition FSRepPow width x n := iter_op FRepMul (toRep 1%F) SRep_testbit n x width. + Lemma FSRepPow_correct : forall width x n, (N.size_nat (unRep n) <= width)%nat -> (unRep x ^ unRep n)%F = unRep (FSRepPow width 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. + erewrite <-(fun x => iter_op_spec (scalar := SRep) mul F_mul_assoc _ F_mul_1_l _ unRep SRep_testbit_correct n x width) 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. + Definition FRepInv x : FRep := FSRepPow (COMPILETIME (N.size_nat (Z.to_N (q - 2)))) x (COMPILETIME (toRep (Z.to_N (q - 2)))). + Lemma FRepInv_correct : forall x, inv (unRep x)%F = unRep (FRepInv x). + unfold FRepInv, COMPILETIME; 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. + auto using prime_q, two_lt_q. reflexivity. Qed. +End FSRepOperations. + +Section ESRepOperations. + Context {tep:TwistedEdwardsParams} {a_is_minus1:a = opp 1}. + Context `{rcS:RepConversions N SRep} {rcSOK:RepConversionsOK rcS}. + Context {SRep_testbit : SRep -> nat -> bool}. + Context {SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (unRep x0) i}. + Definition scalarMultExtendedSRep (bound:nat) (a:SRep) (P:extendedPoint) := + unExtendedPoint (iter_op (@unifiedAddM1 _ a_is_minus1) (mkExtendedPoint E.zero) SRep_testbit a P bound). + Definition scalarMultExtendedSRep_correct : forall (bound:nat) (a:SRep) (P:extendedPoint) (bound_satisfied:(N.size_nat (unRep a) <= bound)%nat), + scalarMultExtendedSRep bound a P = (N.to_nat (unRep a) * unExtendedPoint P)%E. + Proof. (* derivation result copy-pasted to above to remove preconditions from it *) + intros. + rewrite <-(scalarMultM1_rep a_is_minus1), <-(@iter_op_spec _ extendedPoint_eq _ _ (@unifiedAddM1 _ a_is_minus1) _ (@unifiedAddM1_assoc _ a_is_minus1) _ (@unifiedAddM1_0_l _ a_is_minus1) _ _ SRep_testbit_correct _ _ bound) by assumption. + reflexivity. + Defined. +End ESRepOperations. + +Section EdDSADerivation. + Context `(eddsaprm:EdDSAParams). + Context `(rcS:RepConversions N SRep) (rcSOK:RepConversionsOK rcS). + Context `(rcF:RepConversions (F 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). + Context (FSRepPow:FRep->SRep->FRep) (FSRepPow_correct: forall x n, (N.size_nat (unRep n) <= (N.size_nat (N.of_nat l)))%nat -> (unRep x ^ unRep n)%F = unRep (FSRepPow x n)). + Context (FRepInv:FRep->FRep) (FRepInv_correct:forall x, inv (unRep x)%F = unRep (FRepInv x)). + Context (a_is_minus1:CompleteEdwardsCurve.a = opp 1). + + Local Infix "++" := Word.combine. + Local Infix "==?" := E.point_eqb (at level 70) : E_scope. + Local Infix "==?" := ModularArithmeticTheorems.F_eq_dec (at level 70) : F_scope. + Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40). + Local Notation " a '[' i ':]' " := (Word.split2 i _ a) (at level 40). + Local Arguments H {_ _} _. + Local Arguments unifiedAddM1 {_} {_} _ _. + + (*TODO:move*) + Lemma F_eqb_iff : forall x y : F q, F_eqb x y = true <-> x = y. + Proof. + split; eauto using F_eqb_eq, F_eqb_complete. + Qed. + Lemma E_eqb_iff : forall x y : E.point, E.point_eqb x y = true <-> x = y. + Proof. + split; eauto using E.point_eqb_sound, E.point_eqb_complete. + Qed. + + Lemma B_proj : proj1_sig B = (fst(proj1_sig B), snd(proj1_sig B)). destruct B as [[]]; reflexivity. Qed. + + Lemma solve_for_R_eq : forall A B C, (A = B + C <-> B = A - C)%E. + Proof. + intros; split; intros; subst; unfold E.sub; + rewrite <-E.add_assoc, ?E.add_opp_r, ?E.add_opp_l, E.add_0_r; reflexivity. + Qed. + + Lemma solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E. + Proof. + intros; + rewrite !E.point_eqb_correct; + repeat match goal with |- context[E.point_eq_dec ?x ?y] => destruct (E.point_eq_dec x y) end; + rewrite solve_for_R_eq in *; + congruence. + Qed. + + Axiom decode_scalar : word b -> option N. + Axiom decode_scalar_correct : forall x, decode_scalar x = option_map (fun x : F (Z.of_nat l) => Z.to_N x) (dec x). + + Axiom enc':(F q * F q) -> word b. + Axiom enc'_correct : @enc E.point _ _ = (fun x => enc' (proj1_sig x)). + + Axiom FRepOpp : FRep -> FRep. + Axiom FRepOpp_correct : forall x, opp (unRep x) = unRep (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 option FRep. + Axiom wire2FRep_correct : forall x, Fm_dec x = option_map unRep (wire2FRep x). + + Axiom FRep2wire : FRep -> word (b-1). + Axiom FRep2wire_correct : forall x, FRep2wire x = @enc _ _ FqEncoding (unRep x). + + Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). + Local Notation "2" := (ZToField 2) : F_scope. 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. + match r with (((x, y), z), t) => mkExtended (unRep x) (unRep y) (unRep z) (unRep 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. - Local Ltac Let_In_unRep := + (** TODO: Move me *) + Local Ltac Let_In_app fn := 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 + | [ |- appcontext G[Let_In (fn ?x) ?f] ] + => change (Let_In (fn x) f) with (Let_In x (fun y => f (fn 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. @@ -266,11 +393,12 @@ Section Ed25519Frep. @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. + 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. + 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. @@ -285,7 +413,7 @@ Section Ed25519Frep. { etransitivity; [|replace_let_in_with_Let_In; reflexivity]. repeat ( autorewrite with FRepOperations; - Let_In_unRep; + Let_In_app 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))) @@ -302,7 +430,7 @@ Section Ed25519Frep. 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 rep2T (P:FRep * FRep) := (unRep (fst P), unRep (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. @@ -310,16 +438,15 @@ Section Ed25519Frep. 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. + Lemma Fl_SRep_bound : forall (a:F (Z.of_nat EdDSA.l)), (N.size_nat (unRep (toRep (Z.to_N (FieldToZ a)))) <= N.size_nat (Z.to_N (Z.pred (Z.of_nat EdDSA.l))))%nat. + Proof. + intros. + rewrite rcSOK. + apply N_size_nat_le_mono. + pose proof l_odd. + edestruct (FieldToZ_range a); [omega|]. + apply Znat.Z2N.inj_le; trivial; omega. + Qed. (** TODO: Move me, remove Local *) Definition proj1_sig_unmatched {A P} := @proj1_sig A P. @@ -336,17 +463,14 @@ Section Ed25519Frep. (* [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 unfold_E_sub : forall a b, (a - b = a + E.opp b)%E. Proof. reflexivity. Qed. 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). + : (unRep x, unRep y, unRep z, unRep t) = rep2E (((x, y), z), t). Proof. reflexivity. Qed. Lemma commute_negateExtended'_rep2E x y z t : negateExtended' (rep2E (((x, y), z), t)) @@ -356,7 +480,7 @@ Section Ed25519Frep. : (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). + : (unRep x, unRep y, z, unRep 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). @@ -369,45 +493,51 @@ 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))) @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. + Local Existing Instance FqEncoding. - Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. + Hint Rewrite @F_mul_0_l commute_negateExtended'_rep2E_rrfr fold_rep2E_0fff solve_for_R + (@fold_rep2E_ff1f (fst (proj1_sig B))) + (eqb_compare_encodings F_eqb F_eqb_iff (@weqb (b-1)) (@weqb_true_iff (b-1))) + (eqb_compare_encodings E.point_eqb E_eqb_iff (@weqb b) (@weqb_true_iff b)) + (if_map unRep) unfold_E_sub E.opp_mul + (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 E.point_eqb_correct + : EdDSA_opts. + + Lemma sharper_verify : forall pk l msg sig, { sherper_verify | sherper_verify = verify (n:=l) pk 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]. + eexists; cbv [EdDSA.verify]; intros. - etransitivity. - Focus 2. - { repeat match goal with + 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. + reflexivity. } Unfocus. + + setoid_rewrite <-E.point_eqb_correct. + setoid_rewrite solve_for_R. + setoid_rewrite (compare_without_decoding PointEncoding _ E_eqb_iff _ (@weqb_true_iff _)). + + rewrite_strat bottomup hints EdDSA_opts. + + setoid_rewrite <-(unExtendedPoint_mkExtendedPoint B). + setoid_rewrite <-(fun a => unExtendedPoint_mkExtendedPoint (E.opp a)). + + setoid_rewrite <-Znat.Z_N_nat. + Axiom nonequivalent_optimization_Hmodl : forall n (x:word n) A, (wordToNat (H x) * A = (wordToNat (H x) mod l * A))%E. + setoid_rewrite nonequivalent_optimization_Hmodl. + setoid_rewrite <-(Nat2N.id (_ mod EdDSA.l)). + setoid_rewrite <-rcSOK. + setoid_rewrite <-(scalarMultExtendedSRep_correct _ _ _ (Fl_SRep_bound _)). + + rewrite N_of_nat_modulo by (pose proof l_odd; omega). + + setoid_rewrite (unifiedAddM1_rep a_is_minus1). etransitivity. Focus 2. @@ -424,12 +554,6 @@ Section Ed25519Frep. } 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]. unfold_proj1_sig_exist. @@ -578,4 +702,4 @@ Section Ed25519Frep. reflexivity. } Unfocus. reflexivity. Defined. -End Ed25519Frep. \ No newline at end of file +End EdDSADerivation. \ No newline at end of file -- cgit v1.2.3 From 568ef28e09b11b5404175d70012ec674dd9fb7e5 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 27 May 2016 15:17:38 -0400 Subject: right after scalars to F l --- src/Specific/Ed25519.v | 83 +++++++++++++++++++++++++++++++------------------- 1 file changed, 51 insertions(+), 32 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 08f8a6448..c8a6977d1 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -12,6 +12,7 @@ Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil Crypto.Rep. Require Import Coq.Setoids.Setoid. Require Import Coq.Classes.Morphisms. +Require Import Zdiv. (*TODO: move enerything before the section out of this file *) @@ -247,32 +248,37 @@ Proof. destruct (B_eqb P_ (enc Q)) eqn:Heq; [rewrite B_eqb_iff in Heq; eauto | trivial]. } Qed. +Definition FieldToN {m} (x:F m) := Z.to_N (FieldToZ x). +Lemma FieldToN_correct {m} (x:F m) : FieldToN (m:=m) x = Z.to_N (FieldToZ x). reflexivity. Qed. + Generalizable All Variables. Section FSRepOperations. Context {q:Z} {prime_q:Znumtheory.prime q} {two_lt_q:(2 < q)%Z}. - Context `(rcS:RepConversions N SRep) (rcSOK:RepConversionsOK rcS). + Context {l:Z} {two_lt_l:(2 < l)%Z}. + Context `{rcS:RepConversions (F l) SRep} {rcSOK:RepConversionsOK rcS}. Context `(rcF:RepConversions (F 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). 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. + Axiom SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (unRep x0)) i. Definition FSRepPow width x n := iter_op FRepMul (toRep 1%F) SRep_testbit n x width. - Lemma FSRepPow_correct : forall width x n, (N.size_nat (unRep n) <= width)%nat -> (unRep x ^ unRep n)%F = unRep (FSRepPow width x n). + Lemma FSRepPow_correct : forall width x n, (N.size_nat (FieldToN (unRep n)) <= width)%nat -> (unRep x ^ FieldToN (unRep n))%F = unRep (FSRepPow width 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 F_mul_assoc _ F_mul_1_l _ unRep SRep_testbit_correct n x width) by auto. + erewrite <-(fun x => iter_op_spec (scalar := SRep) mul F_mul_assoc _ F_mul_1_l _ _ SRep_testbit_correct n x width) by auto. rewrite <-(rcFOK 1%F) at 1. erewrite <-iter_op_proj by auto. reflexivity. Qed. - Definition FRepInv x : FRep := FSRepPow (COMPILETIME (N.size_nat (Z.to_N (q - 2)))) x (COMPILETIME (toRep (Z.to_N (q - 2)))). + Context (q_minus_2_lt_l:(q - 2 < l)%Z). + Definition FRepInv x : FRep := FSRepPow (COMPILETIME (N.size_nat (Z.to_N (q - 2)))) x (COMPILETIME (toRep (ZToField (q - 2)))). Lemma FRepInv_correct : forall x, inv (unRep x)%F = unRep (FRepInv x). unfold FRepInv, COMPILETIME; intros. - rewrite <-FSRepPow_correct; rewrite rcSOK; try reflexivity. - pose proof @Fq_inv_fermat_correct as H; unfold inv_fermat in H; rewrite H by + rewrite <-FSRepPow_correct; rewrite FieldToN_correct, rcSOK, FieldToZ_ZToField, Zmod_small by omega; trivial. + pose proof @Fq_inv_fermat_correct as Hf; unfold inv_fermat in Hf; rewrite Hf by auto using prime_q, two_lt_q. reflexivity. Qed. @@ -280,27 +286,39 @@ End FSRepOperations. Section ESRepOperations. Context {tep:TwistedEdwardsParams} {a_is_minus1:a = opp 1}. - Context `{rcS:RepConversions N SRep} {rcSOK:RepConversionsOK rcS}. + Context {l:Z} {two_lt_l:(2 < l)%Z}. + Context `{rcS:RepConversions (F l) SRep} {rcSOK:RepConversionsOK rcS}. Context {SRep_testbit : SRep -> nat -> bool}. - Context {SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (unRep x0) i}. - Definition scalarMultExtendedSRep (bound:nat) (a:SRep) (P:extendedPoint) := - unExtendedPoint (iter_op (@unifiedAddM1 _ a_is_minus1) (mkExtendedPoint E.zero) SRep_testbit a P bound). - Definition scalarMultExtendedSRep_correct : forall (bound:nat) (a:SRep) (P:extendedPoint) (bound_satisfied:(N.size_nat (unRep a) <= bound)%nat), - scalarMultExtendedSRep bound a P = (N.to_nat (unRep a) * unExtendedPoint P)%E. + Context {SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (unRep x0)) i}. + Definition scalarMultExtendedSRep (a:SRep) (P:extendedPoint) := + unExtendedPoint (iter_op (@unifiedAddM1 _ a_is_minus1) (mkExtendedPoint E.zero) SRep_testbit a P (N.size_nat (Z.to_N (Z.pred l)))). + + Lemma bound_satisfied : forall a, (N.size_nat (FieldToN (unRep a)) <= N.size_nat (Z.to_N (Z.pred l)))%nat. + Proof. + intros. + apply N_size_nat_le_mono. + rewrite FieldToN_correct. + destruct (FieldToZ_range (unRep a)); [omega|]. + rewrite <-Z2N.inj_le; omega. + Qed. + + Definition scalarMultExtendedSRep_correct : forall (a:SRep) (P:extendedPoint), + scalarMultExtendedSRep a P = (N.to_nat (FieldToN (unRep a)) * unExtendedPoint P)%E. Proof. (* derivation result copy-pasted to above to remove preconditions from it *) intros. - rewrite <-(scalarMultM1_rep a_is_minus1), <-(@iter_op_spec _ extendedPoint_eq _ _ (@unifiedAddM1 _ a_is_minus1) _ (@unifiedAddM1_assoc _ a_is_minus1) _ (@unifiedAddM1_0_l _ a_is_minus1) _ _ SRep_testbit_correct _ _ bound) by assumption. + rewrite <-(scalarMultM1_rep a_is_minus1), <-(@iter_op_spec _ extendedPoint_eq _ _ (@unifiedAddM1 _ a_is_minus1) _ (@unifiedAddM1_assoc _ a_is_minus1) _ (@unifiedAddM1_0_l _ a_is_minus1) _ _ SRep_testbit_correct _ _ _ (bound_satisfied _)). reflexivity. Defined. End ESRepOperations. Section EdDSADerivation. Context `(eddsaprm:EdDSAParams). - Context `(rcS:RepConversions N SRep) (rcSOK:RepConversionsOK rcS). + Context `(rcS:RepConversions (F (Z.of_nat l)) SRep) (rcSOK:RepConversionsOK rcS). + Context {SRep_testbit : SRep -> nat -> bool}. + Context {SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (unRep x0)) i}. Context `(rcF:RepConversions (F 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). - Context (FSRepPow:FRep->SRep->FRep) (FSRepPow_correct: forall x n, (N.size_nat (unRep n) <= (N.size_nat (N.of_nat l)))%nat -> (unRep x ^ unRep n)%F = unRep (FSRepPow x n)). Context (FRepInv:FRep->FRep) (FRepInv_correct:forall x, inv (unRep x)%F = unRep (FRepInv x)). Context (a_is_minus1:CompleteEdwardsCurve.a = opp 1). @@ -360,6 +378,16 @@ Section EdDSADerivation. Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). Local Notation "2" := (ZToField 2) : F_scope. + Axiom nonequivalent_optimization_Hmodl : forall n (x:word n) A, (wordToNat (H x) * A = (wordToNat (H x) mod l * A))%E. + Lemma two_lt_l : (2 < Z.of_nat l)%Z. + Proof. + pose proof l_odd. omega. + Qed. + Lemma l_nonzero : l <> 0. + Proof. + pose proof l_odd. omega. + 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 := @@ -438,16 +466,6 @@ Section EdDSADerivation. rewrite !unfoldDiv, <-!FRepMul_correct, <-FRepInv_correct. reflexivity. Qed. - Lemma Fl_SRep_bound : forall (a:F (Z.of_nat EdDSA.l)), (N.size_nat (unRep (toRep (Z.to_N (FieldToZ a)))) <= N.size_nat (Z.to_N (Z.pred (Z.of_nat EdDSA.l))))%nat. - Proof. - intros. - rewrite rcSOK. - apply N_size_nat_le_mono. - pose proof l_odd. - edestruct (FieldToZ_range a); [omega|]. - apply Znat.Z2N.inj_le; trivial; omega. - Qed. - (** 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. @@ -528,15 +546,16 @@ Section EdDSADerivation. setoid_rewrite <-(unExtendedPoint_mkExtendedPoint B). setoid_rewrite <-(fun a => unExtendedPoint_mkExtendedPoint (E.opp a)). - setoid_rewrite <-Znat.Z_N_nat. - Axiom nonequivalent_optimization_Hmodl : forall n (x:word n) A, (wordToNat (H x) * A = (wordToNat (H x) mod l * A))%E. setoid_rewrite nonequivalent_optimization_Hmodl. - setoid_rewrite <-(Nat2N.id (_ mod EdDSA.l)). + setoid_rewrite <-(Nat2Z.id (_ mod EdDSA.l)). + setoid_rewrite (mod_Zmod _ _ l_nonzero). + setoid_rewrite <-Znat.Z_N_nat. + setoid_rewrite <-FieldToZ_ZToField. + setoid_rewrite <-FieldToN_correct. setoid_rewrite <-rcSOK. - setoid_rewrite <-(scalarMultExtendedSRep_correct _ _ _ (Fl_SRep_bound _)). - rewrite N_of_nat_modulo by (pose proof l_odd; omega). - + setoid_rewrite <-(scalarMultExtendedSRep_correct (a_is_minus1:=a_is_minus1) (SRep_testbit_correct:=SRep_testbit_correct) (two_lt_l:=two_lt_l)). + setoid_rewrite (unifiedAddM1_rep a_is_minus1). etransitivity. -- cgit v1.2.3 From b292d20ccc48dc0d2f67cb138abcccaeb7c3948b Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 28 May 2016 12:26:52 -0400 Subject: verify derivation: EdDSA layer --- .../CompleteEdwardsCurveTheorems.v | 16 +- src/Specific/Ed25519.v | 372 ++++++++++----------- 2 files changed, 185 insertions(+), 203 deletions(-) (limited to 'src/Specific') diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index f70479c3a..88ae9578c 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -215,23 +215,23 @@ Module E. Qed. - Program Definition opp (P:E.point) : E.point := let '(x, y) := proj1_sig P in (opp x, y). - Next Obligation. Proof. - pose (proj2_sig P) as H; rewrite <-Heq_anonymous in H; simpl in H. - rewrite F_square_opp; trivial. - Qed. + Definition opp' (xy:(F q*F q)) : (F q * F q) := let '(x, y) := xy in (opp x, y). + Definition opp (P:E.point) : E.point. exists (opp' (proj1_sig P)). + Proof. + destruct P as [[]]; simpl; rewrite F_square_opp; trivial. + Defined. Definition sub P Q := (P + opp Q)%E. Lemma opp_zero : opp E.zero = E.zero. Proof. pose proof @F_opp_0. - unfold opp, E.zero; eapply point_eq; congruence. + unfold opp, opp', E.zero; simpl; eapply point_eq; congruence. Qed. Lemma add_opp_r : forall P, (P + opp P = E.zero)%E. Proof. - unfold opp; Edefn; rewrite ?@F_pow_2_r in *; (F_field_simplify_eq; [clear_prm; F_nsatz|..]); + unfold opp, opp'; Edefn; rewrite ?@F_pow_2_r in *; (F_field_simplify_eq; [clear_prm; F_nsatz|..]); rewrite <-?@F_pow_2_r in *; pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP); pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP); @@ -293,7 +293,7 @@ Module E. Lemma opp_mul : forall n P, opp (E.mul n P) = E.mul n (opp P). Proof. pose proof opp_add; pose proof opp_zero. - induction n; simpl; intros; congruence. + induction n; trivial; intros; rewrite !mul_S_l, opp_add; congruence. Qed. End CompleteEdwardsCurveTheorems. End E. diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index c8a6977d1..0273deb63 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -40,6 +40,33 @@ Local Ltac replace_let_in_with_Let_In := => apply Let_In_Proper_nd; [ reflexivity | cbv beta delta [pointwise_relation]; intro ] end. +Local Ltac Let_In_app fn := + match goal with + | [ |- appcontext G[Let_In (fn ?x) ?f] ] + => change (Let_In (fn x) f) with (Let_In x (fun y => f (fn y))); cbv beta + 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. + +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. + Lemma funexp_proj {T T'} (proj : T -> T') (f : T -> T) (f' : T' -> T') x n (f_proj : forall a, proj (f a) = f' (proj a)) : proj (funexp f x n) = funexp f' (proj x) n. @@ -248,9 +275,29 @@ Proof. destruct (B_eqb P_ (enc Q)) eqn:Heq; [rewrite B_eqb_iff in Heq; eauto | trivial]. } Qed. +Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed. + Definition FieldToN {m} (x:F m) := Z.to_N (FieldToZ x). Lemma FieldToN_correct {m} (x:F m) : FieldToN (m:=m) x = Z.to_N (FieldToZ x). reflexivity. Qed. +Definition natToField {m} x : F m := ZToField (Z.of_nat x). +Definition FieldToNat {m} (x:F m) : nat := Z.to_nat (FieldToZ x). +Lemma FieldToNat_natToField {m} : m <> 0 -> forall x, x mod m = FieldToNat (natToField (m:=Z.of_nat m) x). + unfold natToField, FieldToNat; intros. + rewrite (FieldToZ_ZToField), <-mod_Zmod, Nat2Z.id; trivial. +Qed. + +Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y. +Proof. + split; eauto using F_eqb_eq, F_eqb_complete. +Qed. +Lemma E_eqb_iff : forall {prm:TwistedEdwardsParams} (x y : E.point), E.point_eqb x y = true <-> x = y. +Proof. + split; eauto using E.point_eqb_sound, E.point_eqb_complete. +Qed. + +Lemma unfold_E_sub : forall {prm:TwistedEdwardsParams} a b, (a - b = a + E.opp b)%E. Proof. reflexivity. Qed. + Generalizable All Variables. Section FSRepOperations. Context {q:Z} {prime_q:Znumtheory.prime q} {two_lt_q:(2 < q)%Z}. @@ -291,7 +338,7 @@ Section ESRepOperations. Context {SRep_testbit : SRep -> nat -> bool}. Context {SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (unRep x0)) i}. Definition scalarMultExtendedSRep (a:SRep) (P:extendedPoint) := - unExtendedPoint (iter_op (@unifiedAddM1 _ a_is_minus1) (mkExtendedPoint E.zero) SRep_testbit a P (N.size_nat (Z.to_N (Z.pred l)))). + iter_op (@unifiedAddM1 _ a_is_minus1) (mkExtendedPoint E.zero) SRep_testbit a P (COMPILETIME (N.size_nat (Z.to_N (Z.pred l)))). Lemma bound_satisfied : forall a, (N.size_nat (FieldToN (unRep a)) <= N.size_nat (Z.to_N (Z.pred l)))%nat. Proof. @@ -303,132 +350,35 @@ Section ESRepOperations. Qed. Definition scalarMultExtendedSRep_correct : forall (a:SRep) (P:extendedPoint), - scalarMultExtendedSRep a P = (N.to_nat (FieldToN (unRep a)) * unExtendedPoint P)%E. + unExtendedPoint (scalarMultExtendedSRep a P) = (N.to_nat (FieldToN (unRep a)) * unExtendedPoint P)%E. Proof. (* derivation result copy-pasted to above to remove preconditions from it *) intros. rewrite <-(scalarMultM1_rep a_is_minus1), <-(@iter_op_spec _ extendedPoint_eq _ _ (@unifiedAddM1 _ a_is_minus1) _ (@unifiedAddM1_assoc _ a_is_minus1) _ (@unifiedAddM1_0_l _ a_is_minus1) _ _ SRep_testbit_correct _ _ _ (bound_satisfied _)). reflexivity. Defined. -End ESRepOperations. - -Section EdDSADerivation. - Context `(eddsaprm:EdDSAParams). - Context `(rcS:RepConversions (F (Z.of_nat l)) SRep) (rcSOK:RepConversionsOK rcS). - Context {SRep_testbit : SRep -> nat -> bool}. - Context {SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (unRep x0)) i}. - Context `(rcF:RepConversions (F 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). - Context (FRepInv:FRep->FRep) (FRepInv_correct:forall x, inv (unRep x)%F = unRep (FRepInv x)). - Context (a_is_minus1:CompleteEdwardsCurve.a = opp 1). - Local Infix "++" := Word.combine. - Local Infix "==?" := E.point_eqb (at level 70) : E_scope. - Local Infix "==?" := ModularArithmeticTheorems.F_eq_dec (at level 70) : F_scope. - Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40). - Local Notation " a '[' i ':]' " := (Word.split2 i _ a) (at level 40). - Local Arguments H {_ _} _. - Local Arguments unifiedAddM1 {_} {_} _ _. - - (*TODO:move*) - Lemma F_eqb_iff : forall x y : F q, F_eqb x y = true <-> x = y. - Proof. - split; eauto using F_eqb_eq, F_eqb_complete. - Qed. - Lemma E_eqb_iff : forall x y : E.point, E.point_eqb x y = true <-> x = y. - Proof. - split; eauto using E.point_eqb_sound, E.point_eqb_complete. - Qed. - - Lemma B_proj : proj1_sig B = (fst(proj1_sig B), snd(proj1_sig B)). destruct B as [[]]; reflexivity. Qed. - - Lemma solve_for_R_eq : forall A B C, (A = B + C <-> B = A - C)%E. - Proof. - intros; split; intros; subst; unfold E.sub; - rewrite <-E.add_assoc, ?E.add_opp_r, ?E.add_opp_l, E.add_0_r; reflexivity. - Qed. - - Lemma solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E. - Proof. - intros; - rewrite !E.point_eqb_correct; - repeat match goal with |- context[E.point_eq_dec ?x ?y] => destruct (E.point_eq_dec x y) end; - rewrite solve_for_R_eq in *; - congruence. - Qed. - - Axiom decode_scalar : word b -> option N. - Axiom decode_scalar_correct : forall x, decode_scalar x = option_map (fun x : F (Z.of_nat l) => Z.to_N x) (dec x). - - Axiom enc':(F q * F q) -> word b. - Axiom enc'_correct : @enc E.point _ _ = (fun x => enc' (proj1_sig x)). + Context `{rcF:RepConversions (F 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}. + Context {FRepInv:FRep->FRep} {FRepInv_correct:forall x, inv (unRep x)%F = unRep (FRepInv x)}. Axiom FRepOpp : FRep -> FRep. Axiom FRepOpp_correct : forall x, opp (unRep x) = unRep (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 option FRep. - Axiom wire2FRep_correct : forall x, Fm_dec x = option_map unRep (wire2FRep x). - - Axiom FRep2wire : FRep -> word (b-1). - Axiom FRep2wire_correct : forall x, FRep2wire x = @enc _ _ FqEncoding (unRep x). - - Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). - Local Notation "2" := (ZToField 2) : F_scope. - - Axiom nonequivalent_optimization_Hmodl : forall n (x:word n) A, (wordToNat (H x) * A = (wordToNat (H x) mod l * A))%E. - Lemma two_lt_l : (2 < Z.of_nat l)%Z. - Proof. - pose proof l_odd. omega. - Qed. - Lemma l_nonzero : l <> 0. - Proof. - pose proof l_odd. omega. - Qed. + Create HintDb FRepOperations discriminated. + Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct @FRepInv_correct @FSRepPow_correct FRepOpp_correct : FRepOperations. - Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed. + (* + Definition ERep := (FRep * FRep * FRep * FRep)%type. Definition rep2E (r:FRep * FRep * FRep * FRep) : extended := match r with (((x, y), z), t) => mkExtended (unRep x) (unRep y) (unRep z) (unRep 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. - - (** TODO: Move me *) - Local Ltac Let_In_app fn := - match goal with - | [ |- appcontext G[Let_In (fn ?x) ?f] ] - => change (Let_In (fn x) f) with (Let_In x (fun y => f (fn y))); cbv beta - end. - - 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)))). + Lemma fold_rep2E x y z t + : mkExtended (unRep x) (unRep y) (unRep z) (unRep t) = rep2E (((x, y), z), t). 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) }. + Lemma unifiedAddM1Rep_sig : forall a b : ERep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. Proof. destruct a as [[[]]]; destruct b as [[[]]]. eexists. @@ -443,7 +393,7 @@ Section EdDSADerivation. autorewrite with FRepOperations; Let_In_app 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) => + lazymatch goal with |- ?LHS = mkExtended (unRep ?x) (unRep ?y) (unRep ?z) (unRep ?t) => change (LHS = (rep2E (((x, y), z), t))) end. reflexivity. } @@ -465,70 +415,88 @@ Section EdDSADerivation. unfold rep2T, rep2E, erep2trep, extendedToTwisted; destruct P as [[[]]]; simpl. rewrite !unfoldDiv, <-!FRepMul_correct, <-FRepInv_correct. reflexivity. Qed. + *) +End ESRepOperations. - (** 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]. +Section EdDSADerivation. + Context `(eddsaprm:EdDSAParams). + Context `(rcS:RepConversions (F (Z.of_nat l)) SRep) (rcSOK:RepConversionsOK rcS). + Context {SRep_testbit : SRep -> nat -> bool}. + Context {SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (unRep x0)) i}. + Context `(rcF:RepConversions (F 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). + Context (FRepInv:FRep->FRep) (FRepInv_correct:forall x, inv (unRep x)%F = unRep (FRepInv x)). + Context (a_is_minus1:CompleteEdwardsCurve.a = opp 1). - Lemma unfold_E_sub : forall a b, (a - b = a + E.opp b)%E. Proof. reflexivity. Qed. + Context (SRepDec : word b -> option SRep) (SRepDec_correct : forall x, option_map (fun x : F (Z.of_nat l) => toRep x) (dec x) = SRepDec x). + Context (ERep:Type) (E2Rep : E.point -> ERep). + Context (ERepEnc : ERep -> word b) (ERepEnc_correct : forall (P:E.point), enc P = ERepEnc (E2Rep P)). + Context (ERepOpp : ERep -> ERep) (ERepOpp_correct : forall P:E.point, E2Rep (E.opp P) = ERepOpp (E2Rep P)). + Context (ERepAdd : ERep -> ERep -> ERep) (ERepAdd_correct : forall (P Q:E.point), E2Rep (E.add P Q) = ERepAdd (E2Rep P) (E2Rep Q)). + Context (ESRepMul : SRep -> ERep -> ERep) (ESRepMul_correct : forall (n:F (Z.of_nat l)) (Q:E.point), E2Rep (E.mul (Z.to_nat n) Q) = ESRepMul (toRep (ZToField n)) (E2Rep Q)). + Context (ERepDec:word b -> option ERep) (ERepDec_correct:forall P_, option_map E2Rep (dec P_) = ERepDec P_). + Axiom nonequivalent_optimization_Hmodl : forall n (x:word n) A, (wordToNat (H x) * A = (wordToNat (H x) mod l * A))%E. + Axiom (SRepH:forall {n}, word n -> SRep). + Axiom SRepH_correct : forall {n} (x:word n), toRep (natToField (H x)) = SRepH x. - 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 to EdDSAProofs *) + Lemma two_lt_l : (2 < Z.of_nat l)%Z. + Proof. + pose proof l_odd. omega. + Qed. + Lemma l_nonzero : l <> 0. + Proof. + pose proof l_odd. omega. + Qed. - (* TODO: move me *) - Lemma fold_rep2E x y z t - : (unRep x, unRep y, unRep z, unRep 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 - : (unRep x, unRep y, z, unRep 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. - - Local Existing Instance FqEncoding. - - Hint Rewrite @F_mul_0_l commute_negateExtended'_rep2E_rrfr fold_rep2E_0fff solve_for_R - (@fold_rep2E_ff1f (fst (proj1_sig B))) - (eqb_compare_encodings F_eqb F_eqb_iff (@weqb (b-1)) (@weqb_true_iff (b-1))) - (eqb_compare_encodings E.point_eqb E_eqb_iff (@weqb b) (@weqb_true_iff b)) - (if_map unRep) unfold_E_sub E.opp_mul - (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 E.point_eqb_correct - : EdDSA_opts. + Local Infix "++" := Word.combine. + Local Infix "==?" := E.point_eqb (at level 70) : E_scope. + Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40). + Local Notation " a '[' i ':]' " := (Word.split2 i _ a) (at level 40). + Local Arguments H {_ _} _. + Lemma solve_for_R_eq : forall A B C, (A = B + C <-> B = A - C)%E. + Proof. + intros; split; intros; subst; unfold E.sub; + rewrite <-E.add_assoc, ?E.add_opp_r, ?E.add_opp_l, E.add_0_r; reflexivity. + Qed. + + Lemma solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E. + Proof. + intros; + rewrite !E.point_eqb_correct; + repeat match goal with |- context[E.point_eq_dec ?x ?y] => destruct (E.point_eq_dec x y) end; + rewrite solve_for_R_eq in *; + congruence. + Qed. + + Create HintDb toESRep discriminated. + Hint Rewrite <-E.point_eqb_correct : toESRep. + Hint Rewrite + nonequivalent_optimization_Hmodl + (FieldToNat_natToField l_nonzero) + + (fun n => solve_for_R (n * B)%E) + (compare_without_decoding PointEncoding _ E_eqb_iff _ (@weqb_true_iff _)) + + unfold_E_sub + E.opp_mul + + ESRepMul_correct + ERepAdd_correct + ERepEnc_correct + ERepOpp_correct + + @ZToField_FieldToZ + @SRepH_correct : toESRep. + Lemma sharper_verify : forall pk l msg sig, { sherper_verify | sherper_verify = verify (n:=l) pk msg sig}. Proof. eexists; cbv [EdDSA.verify]; intros. - etransitivity. Focus 2. { + etransitivity. Focus 2. { (* match dec .. with -> option_rect *) repeat match goal with | [ |- ?x = ?x ] => reflexivity | _ => replace_option_match_with_option_rect @@ -537,31 +505,17 @@ Section EdDSADerivation. end. reflexivity. } Unfocus. - setoid_rewrite <-E.point_eqb_correct. - setoid_rewrite solve_for_R. - setoid_rewrite (compare_without_decoding PointEncoding _ E_eqb_iff _ (@weqb_true_iff _)). - - rewrite_strat bottomup hints EdDSA_opts. - - setoid_rewrite <-(unExtendedPoint_mkExtendedPoint B). - setoid_rewrite <-(fun a => unExtendedPoint_mkExtendedPoint (E.opp a)). - - setoid_rewrite nonequivalent_optimization_Hmodl. - setoid_rewrite <-(Nat2Z.id (_ mod EdDSA.l)). - setoid_rewrite (mod_Zmod _ _ l_nonzero). - setoid_rewrite <-Znat.Z_N_nat. - setoid_rewrite <-FieldToZ_ZToField. - setoid_rewrite <-FieldToN_correct. - setoid_rewrite <-rcSOK. - - setoid_rewrite <-(scalarMultExtendedSRep_correct (a_is_minus1:=a_is_minus1) (SRep_testbit_correct:=SRep_testbit_correct) (two_lt_l:=two_lt_l)). - - setoid_rewrite (unifiedAddM1_rep a_is_minus1). - + rewrite_strat topdown hints toESRep. + setoid_rewrite ESRepMul_correct. (* TODO: why does [rewrite_strat] not do this? *) + rewrite_strat topdown hints toESRep. + + (* decoding of S : option_rect (F l) -> option_map SRep *) + (* TODO: we want this section to look more like the following: + setoid_rewrite (@option_rect_option_map (F (Z.of_nat EdDSA.l)) _ bool toRep). *) 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 _) => toRep x) _ false dec)] end. eapply option_rect_Proper_nd; [intro|reflexivity..]. match goal with @@ -571,10 +525,36 @@ Section EdDSADerivation. end. reflexivity. } Unfocus. - rewrite <-decode_scalar_correct. + rewrite SRepDec_correct. - rewrite enc'_correct. - cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1]. + (* decoding of A : option_rect E.point -> option_map E2Rep *) + (* TODO: automate *) + 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 E2Rep _ 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 ERepDec_correct. + + reflexivity. + Defined. + + (* + + (** start dropping sigma-types from Extended points **) + + setoid_rewrite point_enc_coordinates_correct. + cbv beta delta [unExtendedPoint unifiedAddM1 negateExtended scalarMultExtendedSRep E.opp]. unfold_proj1_sig_exist. etransitivity. @@ -593,6 +573,8 @@ Section EdDSADerivation. unfold_proj1_sig_exist. rewrite B_proj. + (* decoding of A : option_rect E.point -> option_map (F q * F q) *) + (* TODO: change to (FRep * FRep) instead *) etransitivity. Focus 2. { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). @@ -609,7 +591,7 @@ Section EdDSADerivation. reflexivity. } Unfocus. - cbv [dec PointEncoding point_encoding]. + (* TODO: this is specific to the encoding pattern (but not specific parameters: etransitivity. Focus 2. { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). @@ -673,9 +655,8 @@ Section EdDSADerivation. reflexivity. } Unfocus. - cbv iota beta delta [q d a]. - - rewrite wire2FRep_correct. + setoid_rewrite wire2FRep_correct. + *) etransitivity. Focus 2. { @@ -721,4 +702,5 @@ Section EdDSADerivation. reflexivity. } Unfocus. reflexivity. Defined. -End EdDSADerivation. \ No newline at end of file +End EdDSADerivation. +*) \ No newline at end of file -- cgit v1.2.3 From 60950d64fc35a179348ffb80087360f753ec2779 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 28 May 2016 12:31:38 -0400 Subject: verify derivation, EdDSA layer: remove unused context variables --- src/Specific/Ed25519.v | 7 ------- 1 file changed, 7 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 0273deb63..ecceadcb3 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -421,13 +421,6 @@ End ESRepOperations. Section EdDSADerivation. Context `(eddsaprm:EdDSAParams). Context `(rcS:RepConversions (F (Z.of_nat l)) SRep) (rcSOK:RepConversionsOK rcS). - Context {SRep_testbit : SRep -> nat -> bool}. - Context {SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (unRep x0)) i}. - Context `(rcF:RepConversions (F 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). - Context (FRepInv:FRep->FRep) (FRepInv_correct:forall x, inv (unRep x)%F = unRep (FRepInv x)). - Context (a_is_minus1:CompleteEdwardsCurve.a = opp 1). Context (SRepDec : word b -> option SRep) (SRepDec_correct : forall x, option_map (fun x : F (Z.of_nat l) => toRep x) (dec x) = SRepDec x). Context (ERep:Type) (E2Rep : E.point -> ERep). -- cgit v1.2.3 From 8f9f92c2b31507c9dbe3da40cc19c07f57263890 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 28 May 2016 13:14:15 -0400 Subject: verify derivation, EdDSA layer: allow arbitrary equivalence relation for ERep and SRep --- src/Specific/Ed25519.v | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index ecceadcb3..1803cbd2b 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -358,15 +358,10 @@ Section ESRepOperations. Defined. Context `{rcF:RepConversions (F 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}. - Context {FRepInv:FRep->FRep} {FRepInv_correct:forall x, inv (unRep x)%F = unRep (FRepInv x)}. - - Axiom FRepOpp : FRep -> FRep. - Axiom FRepOpp_correct : forall x, opp (unRep x) = unRep (FRepOpp x). - - Create HintDb FRepOperations discriminated. - Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct @FRepInv_correct @FSRepPow_correct FRepOpp_correct : FRepOperations. + Context {FRepAdd FRepSub FRepMul:FRep->FRep->FRep} {FRepAdd_correct:forall a b, toRep (mul a b) = FRepMul (toRep a) (toRep b)}. + Context {FRepSub_correct:RepBinOpOK rcF sub FRepSub} {FRepMul_correct:forall a b, toRep (mul a b) = FRepMul (toRep a) (toRep b)}. + Context {FRepInv:FRep->FRep} {FRepInv_correct:forall x, toRep (inv x) = FRepInv (toRep x)}. + Context {FRepOpp : FRep -> FRep} {FRepOpp_correct : forall x, toRep (opp x) = FRepOpp (toRep x)}. (* Definition ERep := (FRep * FRep * FRep * FRep)%type. @@ -418,21 +413,26 @@ Section ESRepOperations. *) End ESRepOperations. +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. +Local Open Scope equiv_scope. + Section EdDSADerivation. - Context `(eddsaprm:EdDSAParams). - Context `(rcS:RepConversions (F (Z.of_nat l)) SRep) (rcSOK:RepConversionsOK rcS). + Context `{eddsaprm:EdDSAParams}. + Context `{ERepEquiv_ok:Equivalence ERep ERepEquiv} {E2Rep : E.point -> ERep}. + Context `{SRepEquiv_ok:Equivalence SRep SRepEquiv} {S2Rep : F (Z.of_nat l) -> SRep}. + + Context `{SRepDec_correct : forall x, option_map (fun x : F (Z.of_nat l) => S2Rep x) (dec x) === SRepDec x}. + Context `{ERepDec_correct:forall P_, option_map E2Rep (dec P_) === ERepDec P_}. + Context `{ERepEnc_correct : forall (P:E.point), enc P = ERepEnc (E2Rep P)} {ERepEnc_proper:Proper (ERepEquiv==>eq) ERepEnc}. + + Context `{ERepAdd_correct : forall (P Q:E.point), E2Rep (E.add P Q) = ERepAdd (E2Rep P) (E2Rep Q)} {ERepAdd_proper:Proper (ERepEquiv==>ERepEquiv==>ERepEquiv) ERepAdd}. + Context `{ESRepMul_correct : forall (n:F (Z.of_nat l)) (Q:E.point), E2Rep (E.mul (Z.to_nat n) Q) = ESRepMul (S2Rep (ZToField n)) (E2Rep Q)} {ESRepMul_proper : Proper (eq==>ERepEquiv==>ERepEquiv) ESRepMul}. + Context `{ERepOpp_correct : forall P:E.point, E2Rep (E.opp P) === ERepOpp (E2Rep P)} {ERepOpp_proper:Proper (ERepEquiv==>ERepEquiv) ERepOpp}. - Context (SRepDec : word b -> option SRep) (SRepDec_correct : forall x, option_map (fun x : F (Z.of_nat l) => toRep x) (dec x) = SRepDec x). - Context (ERep:Type) (E2Rep : E.point -> ERep). - Context (ERepEnc : ERep -> word b) (ERepEnc_correct : forall (P:E.point), enc P = ERepEnc (E2Rep P)). - Context (ERepOpp : ERep -> ERep) (ERepOpp_correct : forall P:E.point, E2Rep (E.opp P) = ERepOpp (E2Rep P)). - Context (ERepAdd : ERep -> ERep -> ERep) (ERepAdd_correct : forall (P Q:E.point), E2Rep (E.add P Q) = ERepAdd (E2Rep P) (E2Rep Q)). - Context (ESRepMul : SRep -> ERep -> ERep) (ESRepMul_correct : forall (n:F (Z.of_nat l)) (Q:E.point), E2Rep (E.mul (Z.to_nat n) Q) = ESRepMul (toRep (ZToField n)) (E2Rep Q)). - Context (ERepDec:word b -> option ERep) (ERepDec_correct:forall P_, option_map E2Rep (dec P_) = ERepDec P_). Axiom nonequivalent_optimization_Hmodl : forall n (x:word n) A, (wordToNat (H x) * A = (wordToNat (H x) mod l * A))%E. Axiom (SRepH:forall {n}, word n -> SRep). - Axiom SRepH_correct : forall {n} (x:word n), toRep (natToField (H x)) = SRepH x. + Axiom SRepH_correct : forall {n} (x:word n), S2Rep (natToField (H x)) = SRepH x. (* TODO: move to EdDSAProofs *) Lemma two_lt_l : (2 < Z.of_nat l)%Z. @@ -508,9 +508,9 @@ Section EdDSADerivation. etransitivity. Focus 2. { lazymatch goal with |- _ = option_rect _ _ ?false ?dec => - symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => toRep x) _ false dec)] + symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => S2Rep x) _ false dec)] end. - eapply option_rect_Proper_nd; [intro|reflexivity..]. + 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 -- cgit v1.2.3 From 1b3fef5834ef94c2b24dd1b60eb82a8534529274 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 28 May 2016 13:29:12 -0400 Subject: --amend --- src/Specific/Ed25519.v | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 1803cbd2b..138babfad 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -10,9 +10,9 @@ Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil Crypto.Rep. -Require Import Coq.Setoids.Setoid. -Require Import Coq.Classes.Morphisms. +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. Require Import Zdiv. +Local Open Scope equiv_scope. (*TODO: move enerything before the section out of this file *) @@ -357,11 +357,16 @@ Section ESRepOperations. reflexivity. Defined. - Context `{rcF:RepConversions (F q) FRep} {rcFOK:RepConversionsOK rcF}. - Context {FRepAdd FRepSub FRepMul:FRep->FRep->FRep} {FRepAdd_correct:forall a b, toRep (mul a b) = FRepMul (toRep a) (toRep b)}. - Context {FRepSub_correct:RepBinOpOK rcF sub FRepSub} {FRepMul_correct:forall a b, toRep (mul a b) = FRepMul (toRep a) (toRep b)}. - Context {FRepInv:FRep->FRep} {FRepInv_correct:forall x, toRep (inv x) = FRepInv (toRep x)}. - Context {FRepOpp : FRep -> FRep} {FRepOpp_correct : forall x, toRep (opp x) = FRepOpp (toRep x)}. + Context `{FRepEquiv_ok:Equivalence FRep FRepEquiv} {F2Rep : F q -> FRep}. + Context `{FRepAdd_correct:forall a b, F2Rep (add a b) === FRepAdd (F2Rep a) (F2Rep b)} {FRepAdd_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepAdd}. + Context `{FRepMul_correct:forall a b, F2Rep (mul a b) === FRepMul (F2Rep a) (F2Rep b)} {FRepMul_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepMul}. + Context `{FRepSub_correct:forall a b, F2Rep (sub a b) === FRepSub (F2Rep a) (F2Rep b)} {FRepSub_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepSub}. + Context {FRepInv:FRep->FRep} {FRepInv_correct:forall x, F2Rep (inv x) === FRepInv (F2Rep x)} {FRepInv_proper: Proper (FRepEquiv==>FRepEquiv) FRepInv}. + Context {FRepOpp : FRep -> FRep} {FRepOpp_correct : forall x, F2Rep (opp x) = FRepOpp (F2Rep x)}. + (* + Lemma ERepAdd_correct : forall (P Q:E.point), E2Rep (E.add P Q) = ERepAdd (E2Rep P) (E2Rep Q). + Lemma ERepAdd_proper : Proper (ERepEquiv==>ERepEquiv==>ERepEquiv) ERepAdd. + *) (* Definition ERep := (FRep * FRep * FRep * FRep)%type. @@ -413,26 +418,23 @@ Section ESRepOperations. *) End ESRepOperations. -Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. -Local Open Scope equiv_scope. - Section EdDSADerivation. Context `{eddsaprm:EdDSAParams}. Context `{ERepEquiv_ok:Equivalence ERep ERepEquiv} {E2Rep : E.point -> ERep}. Context `{SRepEquiv_ok:Equivalence SRep SRepEquiv} {S2Rep : F (Z.of_nat l) -> SRep}. - Context `{SRepDec_correct : forall x, option_map (fun x : F (Z.of_nat l) => S2Rep x) (dec x) === SRepDec x}. - Context `{ERepDec_correct:forall P_, option_map E2Rep (dec P_) === ERepDec P_}. Context `{ERepEnc_correct : forall (P:E.point), enc P = ERepEnc (E2Rep P)} {ERepEnc_proper:Proper (ERepEquiv==>eq) ERepEnc}. - Context `{ERepAdd_correct : forall (P Q:E.point), E2Rep (E.add P Q) = ERepAdd (E2Rep P) (E2Rep Q)} {ERepAdd_proper:Proper (ERepEquiv==>ERepEquiv==>ERepEquiv) ERepAdd}. - Context `{ESRepMul_correct : forall (n:F (Z.of_nat l)) (Q:E.point), E2Rep (E.mul (Z.to_nat n) Q) = ESRepMul (S2Rep (ZToField n)) (E2Rep Q)} {ESRepMul_proper : Proper (eq==>ERepEquiv==>ERepEquiv) ESRepMul}. + Context `{ERepAdd_correct : forall (P Q:E.point), E2Rep (E.add P Q) === ERepAdd (E2Rep P) (E2Rep Q)} {ERepAdd_proper:Proper (ERepEquiv==>ERepEquiv==>ERepEquiv) ERepAdd}. + Context `{ESRepMul_correct : forall (n:F (Z.of_nat l)) (Q:E.point), E2Rep (E.mul (Z.to_nat n) Q) === ESRepMul (S2Rep (ZToField n)) (E2Rep Q)} {ESRepMul_proper : Proper (SRepEquiv==>ERepEquiv==>ERepEquiv) ESRepMul}. Context `{ERepOpp_correct : forall P:E.point, E2Rep (E.opp P) === ERepOpp (E2Rep P)} {ERepOpp_proper:Proper (ERepEquiv==>ERepEquiv) ERepOpp}. + Context `{SRepDec_correct : forall x, option_map (fun x : F (Z.of_nat l) => S2Rep x) (dec x) === SRepDec x}. + Context `{ERepDec_correct:forall P_, option_map E2Rep (dec P_) === ERepDec P_}. Axiom nonequivalent_optimization_Hmodl : forall n (x:word n) A, (wordToNat (H x) * A = (wordToNat (H x) mod l * A))%E. Axiom (SRepH:forall {n}, word n -> SRep). - Axiom SRepH_correct : forall {n} (x:word n), S2Rep (natToField (H x)) = SRepH x. + Axiom SRepH_correct : forall {n} (x:word n), S2Rep (natToField (H x)) === SRepH x. (* TODO: move to EdDSAProofs *) Lemma two_lt_l : (2 < Z.of_nat l)%Z. -- cgit v1.2.3 From 7f5ded6a82327e5dc97ecd4ff300379ddd93dba5 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 29 May 2016 17:45:53 -0400 Subject: ERep add --- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 8 ++ src/Specific/Ed25519.v | 145 ++++++++++++++++++------- 2 files changed, 116 insertions(+), 37 deletions(-) (limited to 'src/Specific') diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 96365084c..44033097d 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -181,6 +181,14 @@ Section ExtendedCoordinates. unfold rep in *; intuition. Qed. + Lemma unifiedAddM1_correct : forall P Q, mkExtendedPoint (E.add P Q) === unifiedAddM1 (mkExtendedPoint P) (mkExtendedPoint Q). + Proof. + unfold equiv, extendedPoint_eq; intros; + pose proof unifiedAddM1_rep (mkExtendedPoint P) (mkExtendedPoint Q); + pose proof unExtendedPoint_mkExtendedPoint; + congruence. + Qed. + Global Instance Proper_unifiedAddM1 : Proper (equiv==>equiv==>equiv) unifiedAddM1. Proof. repeat (econstructor || intro). diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 138babfad..12687310a 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -26,19 +26,18 @@ Local Ltac subst_evars := 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)). +Global Instance Let_In_Proper_nd {A P} R {Reflexive_R:@Reflexive P R} + : Proper (eq ==> pointwise_relation _ R ==> R) (@Let_In A (fun _ => P)). Proof. - lazy; intros; congruence. + lazy; intros; try congruence. + subst; auto. Qed. 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. + match goal with + | [ |- context G[let x := ?y in @?z x] ] + => let G' := context G[Let_In y z] in change G' + end. Local Ltac Let_In_app fn := match goal with @@ -332,61 +331,133 @@ Section FSRepOperations. End FSRepOperations. Section ESRepOperations. - Context {tep:TwistedEdwardsParams} {a_is_minus1:a = opp 1}. - Context {l:Z} {two_lt_l:(2 < l)%Z}. - Context `{rcS:RepConversions (F l) SRep} {rcSOK:RepConversionsOK rcS}. + Context {tep:TwistedEdwardsParams} {a_eq_minus1:a = opp 1}. + Context {l:Z} {two_lt_l:(2 < l)%Z} `{rep2S : SRep -> F l}. Context {SRep_testbit : SRep -> nat -> bool}. - Context {SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (unRep x0)) i}. + Context {SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (rep2S x0)) i}. + Definition scalarMultExtendedSRep (a:SRep) (P:extendedPoint) := - iter_op (@unifiedAddM1 _ a_is_minus1) (mkExtendedPoint E.zero) SRep_testbit a P (COMPILETIME (N.size_nat (Z.to_N (Z.pred l)))). + iter_op (@unifiedAddM1 _ a_eq_minus1) (mkExtendedPoint E.zero) SRep_testbit a P (COMPILETIME (N.size_nat (Z.to_N (Z.pred l)))). - Lemma bound_satisfied : forall a, (N.size_nat (FieldToN (unRep a)) <= N.size_nat (Z.to_N (Z.pred l)))%nat. + Lemma bound_satisfied : forall a, (N.size_nat (FieldToN (rep2S a)) <= N.size_nat (Z.to_N (Z.pred l)))%nat. Proof. intros. apply N_size_nat_le_mono. rewrite FieldToN_correct. - destruct (FieldToZ_range (unRep a)); [omega|]. + destruct (FieldToZ_range (rep2S a)); [omega|]. rewrite <-Z2N.inj_le; omega. Qed. Definition scalarMultExtendedSRep_correct : forall (a:SRep) (P:extendedPoint), - unExtendedPoint (scalarMultExtendedSRep a P) = (N.to_nat (FieldToN (unRep a)) * unExtendedPoint P)%E. + unExtendedPoint (scalarMultExtendedSRep a P) = (N.to_nat (FieldToN (rep2S a)) * unExtendedPoint P)%E. Proof. (* derivation result copy-pasted to above to remove preconditions from it *) intros. - rewrite <-(scalarMultM1_rep a_is_minus1), <-(@iter_op_spec _ extendedPoint_eq _ _ (@unifiedAddM1 _ a_is_minus1) _ (@unifiedAddM1_assoc _ a_is_minus1) _ (@unifiedAddM1_0_l _ a_is_minus1) _ _ SRep_testbit_correct _ _ _ (bound_satisfied _)). + rewrite <-(scalarMultM1_rep a_eq_minus1), <-(@iter_op_spec _ extendedPoint_eq _ _ (@unifiedAddM1 _ a_eq_minus1) _ (@unifiedAddM1_assoc _ a_eq_minus1) _ (@unifiedAddM1_0_l _ a_eq_minus1) _ _ SRep_testbit_correct _ _ _ (bound_satisfied _)). reflexivity. Defined. - Context `{FRepEquiv_ok:Equivalence FRep FRepEquiv} {F2Rep : F q -> FRep}. + Context `{FRepEquiv_ok:Equivalence FRep FRepEquiv} {F2Rep : F q -> FRep} {rep2F:FRep -> F q} {rep2F_proper: Proper (FRepEquiv==>eq) rep2F} {rep2F_F2Rep: forall x, rep2F (F2Rep x) = x}. Context `{FRepAdd_correct:forall a b, F2Rep (add a b) === FRepAdd (F2Rep a) (F2Rep b)} {FRepAdd_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepAdd}. Context `{FRepMul_correct:forall a b, F2Rep (mul a b) === FRepMul (F2Rep a) (F2Rep b)} {FRepMul_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepMul}. Context `{FRepSub_correct:forall a b, F2Rep (sub a b) === FRepSub (F2Rep a) (F2Rep b)} {FRepSub_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepSub}. Context {FRepInv:FRep->FRep} {FRepInv_correct:forall x, F2Rep (inv x) === FRepInv (F2Rep x)} {FRepInv_proper: Proper (FRepEquiv==>FRepEquiv) FRepInv}. - Context {FRepOpp : FRep -> FRep} {FRepOpp_correct : forall x, F2Rep (opp x) = FRepOpp (F2Rep x)}. - (* - Lemma ERepAdd_correct : forall (P Q:E.point), E2Rep (E.add P Q) = ERepAdd (E2Rep P) (E2Rep Q). - Lemma ERepAdd_proper : Proper (ERepEquiv==>ERepEquiv==>ERepEquiv) ERepAdd. - *) + Context {FRepOpp : FRep -> FRep} {FRepOpp_correct : forall x, F2Rep (opp x) = FRepOpp (F2Rep x)} {FRepOpp_proper: Proper (FRepEquiv==>FRepEquiv) FRepOpp}. - (* - Definition ERep := (FRep * FRep * FRep * FRep)%type. + Definition extendedRep := (FRep * FRep * FRep * FRep)%type. + + Definition extended2Rep (P:extendedPoint) := + let 'exist (mkExtended X Y Z T) _ := P in + (F2Rep X, F2Rep Y, F2Rep Z, F2Rep T). + + Definition point2ExtendedRep (P:E.point) := extended2Rep (mkExtendedPoint P). + + Definition extendedRep2Extended (P:extendedRep) : extended := + let '(X, Y, Z, T) := P in + mkExtended (rep2F X) (rep2F Y) (rep2F Z) (rep2F T). + + Definition extendedRep2Twisted (P:extendedRep) : (F q * F q) := extendedToTwisted (extendedRep2Extended P). - Definition rep2E (r:FRep * FRep * FRep * FRep) : extended := - match r with (((x, y), z), t) => mkExtended (unRep x) (unRep y) (unRep z) (unRep t) end. + Definition extendedRepEquiv (P Q:extendedRep) := extendedRep2Twisted P = extendedRep2Twisted Q. - Lemma fold_rep2E x y z t - : mkExtended (unRep x) (unRep y) (unRep z) (unRep t) = rep2E (((x, y), z), t). - Proof. reflexivity. Qed. + Global Instance Equivalence_extendedRepEquiv : Equivalence extendedRepEquiv. + Proof. constructor; intros; congruence. Qed. - Lemma unifiedAddM1Rep_sig : forall a b : ERep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. + Lemma extendedRep2Extended_extended2Rep : forall P, (extendedRep2Extended (extended2Rep P)) = proj1_sig P. + Proof. destruct P as [[] ?]; simpl; rewrite !rep2F_F2Rep; reflexivity. Qed. + + Global Instance extended2Rep_Proper : Proper (extendedPoint_eq==>extendedRepEquiv) extended2Rep. + Proof. + repeat intro. + unfold extendedRepEquiv, extendedRep2Twisted. rewrite !extendedRep2Extended_extended2Rep. + lazymatch goal with [H: extendedPoint_eq _ _ |- _ ] => + unfold extendedPoint_eq, unExtendedPoint in H; + injection H; + solve [trivial] + end. + Qed. + + Lemma extendedRepAdd_extendedPoint_sig : { op | forall P Q, extended2Rep (unifiedAddM1 a_eq_minus1 P Q) === op (extended2Rep P) (extended2Rep Q) }. Proof. - destruct a as [[[]]]; destruct b as [[[]]]. eexists. - lazymatch goal with |- ?LHS = ?RHS :> ?T => - evar (e:T); replace LHS with e; [subst e|] + repeat match goal with + | _ => progress intros + | [ P : extendedPoint |- _ ] => destruct P + | [ P : extended |- _ ] => destruct P + | _ => progress cbv iota beta delta [proj1_sig unifiedAddM1 extended2Rep unifiedAddM1'] + | [ H : rep _ _ /\ _ |- _ ] => clear H + end. + + match goal with |- context[?E] => + match E with let '{| extendedX := _; extendedY := _; extendedZ := _; extendedT := _ |} := ?X in _ + => let E' := (eval pattern X in E) in + change E with E'; + match E' with ?f _ => set (proj := f) end + end 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. + repeat ( + etransitivity; [ + replace_let_in_with_Let_In; + rewrite <-pull_Let_In; + eapply Let_In_Proper_nd; + [solve [eauto with typeclass_instances] + |reflexivity| + cbv beta delta [pointwise_relation]; intro] + |reflexivity]). + subst proj. + cbv beta iota. + reflexivity. + Admitted. + + Definition extendRepAdd_extendedPoint : extendedRep -> extendedRep -> extendedRep := proj1_sig (extendedRepAdd_extendedPoint_sig). + Definition extendRepAdd_extendedPoint_correct : forall P Q, extended2Rep (unifiedAddM1 a_eq_minus1 P Q) === extendRepAdd_extendedPoint (extended2Rep P) (extended2Rep Q) := proj2_sig extendedRepAdd_extendedPoint_sig. + + Lemma extendedRepAdd_sig : { op | forall P Q, point2ExtendedRep (E.add P Q) === op (point2ExtendedRep P) (point2ExtendedRep Q) }. + Proof. + eexists; intros. + unfold point2ExtendedRep. + rewrite <-extendRepAdd_extendedPoint_correct. + apply extended2Rep_Proper. + apply unifiedAddM1_correct. + Defined. + + + cbv beta delta [Let_In]. + + rewrite pull_Let_In. + eapply Let_In_Proper_nd; + [solve [eauto with typeclass_instances] + |reflexivity| + cbv beta delta [pointwise_relation]; intro] + |]. + + replace_let_in_with_Let_In. + rewrite <-pull_Let_In. + eapply Let_In_Proper_nd; [eauto with typeclass_instances|reflexivity|cbv beta delta [pointwise_relation]; intro]; + etransitivity. + + { etransitivity; [|replace_let_in_with_Let_In; reflexivity]. repeat ( -- cgit v1.2.3 From 10531c82d1fe98515dcfd985a288570ecabfbf55 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 30 May 2016 13:54:41 -0400 Subject: E impl: proper morphisms are hard to dow without setoids --- src/Specific/Ed25519.v | 45 ++++++++++++++++++++++++++------------------- 1 file changed, 26 insertions(+), 19 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 12687310a..262d817ae 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -365,11 +365,11 @@ Section ESRepOperations. Definition extendedRep := (FRep * FRep * FRep * FRep)%type. - Definition extended2Rep (P:extendedPoint) := - let 'exist (mkExtended X Y Z T) _ := P in + Definition extended2Rep (P:extended) := + let 'mkExtended X Y Z T := P in (F2Rep X, F2Rep Y, F2Rep Z, F2Rep T). - Definition point2ExtendedRep (P:E.point) := extended2Rep (mkExtendedPoint P). + Definition point2ExtendedRep (P:E.point) := extended2Rep (proj1_sig (mkExtendedPoint P)). Definition extendedRep2Extended (P:extendedRep) : extended := let '(X, Y, Z, T) := P in @@ -382,21 +382,19 @@ Section ESRepOperations. Global Instance Equivalence_extendedRepEquiv : Equivalence extendedRepEquiv. Proof. constructor; intros; congruence. Qed. - Lemma extendedRep2Extended_extended2Rep : forall P, (extendedRep2Extended (extended2Rep P)) = proj1_sig P. + Lemma extendedRep2Extended_extended2Rep : forall P, (extendedRep2Extended (extended2Rep P)) = P. Proof. destruct P as [[] ?]; simpl; rewrite !rep2F_F2Rep; reflexivity. Qed. + (* Global Instance extended2Rep_Proper : Proper (extendedPoint_eq==>extendedRepEquiv) extended2Rep. Proof. repeat intro. unfold extendedRepEquiv, extendedRep2Twisted. rewrite !extendedRep2Extended_extended2Rep. - lazymatch goal with [H: extendedPoint_eq _ _ |- _ ] => - unfold extendedPoint_eq, unExtendedPoint in H; - injection H; - solve [trivial] - end. + lazymatch goal with [H: extendedPoint_eq _ _ |- _ ] => injection H; solve [trivial] end. Qed. + *) - Lemma extendedRepAdd_extendedPoint_sig : { op | forall P Q, extended2Rep (unifiedAddM1 a_eq_minus1 P Q) === op (extended2Rep P) (extended2Rep Q) }. + Definition extendedRepAdd_sig : { op | forall P Q, extended2Rep (unifiedAddM1' P Q) === op (extended2Rep P) (extended2Rep Q) }. Proof. eexists. repeat match goal with @@ -430,17 +428,26 @@ Section ESRepOperations. reflexivity. Admitted. - Definition extendRepAdd_extendedPoint : extendedRep -> extendedRep -> extendedRep := proj1_sig (extendedRepAdd_extendedPoint_sig). - Definition extendRepAdd_extendedPoint_correct : forall P Q, extended2Rep (unifiedAddM1 a_eq_minus1 P Q) === extendRepAdd_extendedPoint (extended2Rep P) (extended2Rep Q) := proj2_sig extendedRepAdd_extendedPoint_sig. + Definition extendedRepAdd : extendedRep -> extendedRep -> extendedRep := proj1_sig (extendedRepAdd_sig). + Definition extendedRepAdd_correct' : forall P Q, extended2Rep (unifiedAddM1' P Q) === extendedRepAdd (extended2Rep P) (extended2Rep Q) := proj2_sig extendedRepAdd_sig. - Lemma extendedRepAdd_sig : { op | forall P Q, point2ExtendedRep (E.add P Q) === op (point2ExtendedRep P) (point2ExtendedRep Q) }. + Lemma extendedRepAdd_correct : forall P Q, point2ExtendedRep (E.add P Q) === extendedRepAdd (point2ExtendedRep P) (point2ExtendedRep Q). Proof. - eexists; intros. - unfold point2ExtendedRep. - rewrite <-extendRepAdd_extendedPoint_correct. - apply extended2Rep_Proper. - apply unifiedAddM1_correct. - Defined. + intros; unfold point2ExtendedRep. + rewrite extendedRepAdd_correct'. + SearchAbout unifiedAddM1'. + rewrite unifiedAddM1_correct. + apply extended2Rep_Proper, unifiedAddM1_correct. + Qed. + + Lemma extendedRepAdd_proper : Proper (extendedRepEquiv==>extendedRepEquiv==>extendedRepEquiv) extendedRepAdd. + Proof. + repeat intro. + etransitivity. + etransitivity. + SearchAbout point2ExtendedRep. + 3:apply extendedRepAdd_correct. + pose proof (fun P P' Q Q' => Proper_unifiedAddM1 a_eq_minus1 P P' Q Q'). cbv beta delta [Let_In]. -- cgit v1.2.3 From 5395b601a29ace08b5a349585726ecef34f34fd6 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 1 Jun 2016 14:43:19 -0400 Subject: leibniz equal version of topdown rewriting of sigma types --- src/Specific/Ed25519.v | 223 +++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 197 insertions(+), 26 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 262d817ae..bf23276f9 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -363,50 +363,221 @@ Section ESRepOperations. Context {FRepInv:FRep->FRep} {FRepInv_correct:forall x, F2Rep (inv x) === FRepInv (F2Rep x)} {FRepInv_proper: Proper (FRepEquiv==>FRepEquiv) FRepInv}. Context {FRepOpp : FRep -> FRep} {FRepOpp_correct : forall x, F2Rep (opp x) = FRepOpp (F2Rep x)} {FRepOpp_proper: Proper (FRepEquiv==>FRepEquiv) FRepOpp}. - Definition extendedRep := (FRep * FRep * FRep * FRep)%type. - Definition extended2Rep (P:extended) := let 'mkExtended X Y Z T := P in (F2Rep X, F2Rep Y, F2Rep Z, F2Rep T). - - Definition point2ExtendedRep (P:E.point) := extended2Rep (proj1_sig (mkExtendedPoint P)). - - Definition extendedRep2Extended (P:extendedRep) : extended := + Definition extendedRep2Extended P : extended := let '(X, Y, Z, T) := P in mkExtended (rep2F X) (rep2F Y) (rep2F Z) (rep2F T). + Definition extendedPointInvariant P := rep P (extendedToTwisted P) /\ E.onCurve (extendedToTwisted P). + Definition extendedRep := { XYZT | extendedPointInvariant (extendedRep2Extended XYZT) }. + + Lemma extendedRep2Extended_extended2Rep P : extendedRep2Extended (extended2Rep P) = P. + Proof. destruct P as [? ? ? ?]; simpl; rewrite !rep2F_F2Rep; reflexivity. Qed. + + Definition extendedPoint2ExtendedRep (P:extendedPoint) : extendedRep. exists (extended2Rep (proj1_sig P)). + Proof. abstract (rewrite extendedRep2Extended_extended2Rep; destruct P; eauto). Defined. - Definition extendedRep2Twisted (P:extendedRep) : (F q * F q) := extendedToTwisted (extendedRep2Extended P). + Definition extendedRep2ExtendedPoint (P:extendedRep) : extendedPoint. exists (extendedRep2Extended (proj1_sig P)). + Proof. abstract (destruct P; eauto). Defined. - Definition extendedRepEquiv (P Q:extendedRep) := extendedRep2Twisted P = extendedRep2Twisted Q. + Definition point2ExtendedRep (P:E.point) : extendedRep := (extendedPoint2ExtendedRep (mkExtendedPoint P)). + Definition extendedRep2Point (P:extendedRep) : E.point := unExtendedPoint (extendedRep2ExtendedPoint P). + + Lemma extendedRep2ExtendedPoint_extendedPoint2ExtendedRep_proj1_sig : forall P, + proj1_sig (extendedRep2ExtendedPoint (extendedPoint2ExtendedRep P)) = proj1_sig P. + Proof. destruct P; simpl; rewrite extendedRep2Extended_extended2Rep; reflexivity. Qed. + + Definition extendedRepEquiv (P Q:extendedRep) := extendedRep2Point P = extendedRep2Point Q. + + Lemma extendedRepEquiv_iff_extendedPoint P Q : extendedRepEquiv P Q <-> extendedRep2ExtendedPoint P === extendedRep2ExtendedPoint Q. + Proof. unfold extendedRepEquiv, extendedRep2Point; split; intros; congruence. Qed. Global Instance Equivalence_extendedRepEquiv : Equivalence extendedRepEquiv. Proof. constructor; intros; congruence. Qed. - Lemma extendedRep2Extended_extended2Rep : forall P, (extendedRep2Extended (extended2Rep P)) = P. - Proof. destruct P as [[] ?]; simpl; rewrite !rep2F_F2Rep; reflexivity. Qed. + Global Instance Proper_extendedPoint2ExtendedRep : Proper (extendedPoint_eq==>extendedRepEquiv) extendedPoint2ExtendedRep. + Proof. + repeat intro. apply E.point_eq. + rewrite !extendedRep2ExtendedPoint_extendedPoint2ExtendedRep_proj1_sig. + injection H; trivial. + Qed. - (* - Global Instance extended2Rep_Proper : Proper (extendedPoint_eq==>extendedRepEquiv) extended2Rep. + Global Instance Proper_extendedRep2Point : Proper (extendedRepEquiv==>eq) extendedRep2Point. + Proof. repeat intro. congruence. Qed. + + Lemma unExtendedPoint_extendedRep2ExtendedPoint : forall P, + unExtendedPoint (extendedRep2ExtendedPoint P) = extendedRep2Point P. + Proof. reflexivity. Qed. + + (* TODO: move *) + Lemma extendedToTwisted_twistedToExtended : forall P, extendedToTwisted (twistedToExtended P) = P. Proof. - repeat intro. - unfold extendedRepEquiv, extendedRep2Twisted. rewrite !extendedRep2Extended_extended2Rep. - lazymatch goal with [H: extendedPoint_eq _ _ |- _ ] => injection H; solve [trivial] end. + destruct P; unfold extendedToTwisted, twistedToExtended; simpl; rewrite !@F_div_1_r; auto using prime_q. + Qed. + Lemma mkExtendedPoint_unExtendedPoint : forall P, mkExtendedPoint (unExtendedPoint P) === P. + Proof. + intros. destruct P; cbv [mkExtendedPoint unExtendedPoint proj1_sig extendedPoint_eq equiv]. + apply E.point_eq. rewrite extendedToTwisted_twistedToExtended; reflexivity. + Qed. + + Lemma extendedRep2Point_point2ExtendedRep : forall P, + extendedRep2Point (point2ExtendedRep P) = P. + Proof. + intros. + unfold extendedRep2Point, point2ExtendedRep. + destruct P; apply E.point_eq. + rewrite !extendedRep2ExtendedPoint_extendedPoint2ExtendedRep_proj1_sig. + apply extendedToTwisted_twistedToExtended. Qed. - *) - Definition extendedRepAdd_sig : { op | forall P Q, extended2Rep (unifiedAddM1' P Q) === op (extended2Rep P) (extended2Rep Q) }. + Lemma point2ExtendedRep_unExtendedPoint : forall P, + (point2ExtendedRep (unExtendedPoint P)) === extendedPoint2ExtendedRep P. Proof. - eexists. - repeat match goal with - | _ => progress intros - | [ P : extendedPoint |- _ ] => destruct P - | [ P : extended |- _ ] => destruct P - | _ => progress cbv iota beta delta [proj1_sig unifiedAddM1 extended2Rep unifiedAddM1'] - | [ H : rep _ _ /\ _ |- _ ] => clear H - end. + intros. unfold point2ExtendedRep. f_equiv. apply mkExtendedPoint_unExtendedPoint. + Qed. + + Lemma point2ExtendedRep_extendedRep2Point : forall P, point2ExtendedRep (extendedRep2Point P) === P. + Proof. + intros; unfold equiv, extendedRepEquiv; pose proof extendedRep2Point_point2ExtendedRep; congruence. + Qed. + + Lemma extendedRepEquiv_refl_proj1_sig : forall P Q : extendedRep, proj1_sig P = proj1_sig Q -> P === Q. + Admitted. + + Definition extendedRepAdd_sig : { op | forall P Q rP rQ, rP === point2ExtendedRep P -> rQ === point2ExtendedRep Q -> point2ExtendedRep (E.add P Q) === op rP rQ }. + Proof. + eexists; intros ? ? ? ? HP HQ. + pose proof unifiedAddM1_rep a_eq_minus1 (extendedRep2ExtendedPoint rP) (extendedRep2ExtendedPoint rQ) as H. + setoid_rewrite unExtendedPoint_extendedRep2ExtendedPoint in H. + rewrite HP in H. + rewrite HQ in H. + rewrite !extendedRep2Point_point2ExtendedRep in H. + rewrite H; clear H HP HQ P Q. rename rQ into Q; rename rP into P. + rewrite point2ExtendedRep_unExtendedPoint at 1. + Axiom BAD: forall x y :extendedRep, x === y <-> x = y. + rewrite BAD. + Lemma path_sig {A P} (x y : @sig A P) (pf : proj1_sig x = proj1_sig y) (pf' : + eq_rect _ P (proj2_sig x) _ pf = proj2_sig y) + : x = y. + Proof. destruct x, y; simpl in *; destruct pf, pf'; reflexivity. Defined. + lazymatch goal with + |- ?LHS = _ :> ?T + => lazymatch eval hnf in T with + @sig ?A ?P + => let lem := constr:(fun x y pf => @path_sig A P LHS (exist _ x y) pf) in + pose proof lem as lem'; + cbv [proj2_sig] in lem'; + simpl @proj1_sig in lem'; + specialize (fun x pf y => lem' x y pf); + specialize (fun x pf => lem' x pf _ eq_refl) + end + end. + apply lem'. + + Grab Existential Variables. + repeat match goal with [H : _ |- _] => revert H end ; intros. + reflexivity. + Defined. + + Definition extendedRepAdd : extendedRep -> extendedRep -> extendedRep := proj1_sig extendedRepAdd_sig. + + Lemma extendedRepAdd_correct : forall P Q, + point2ExtendedRep (E.add P Q) === extendedRepAdd (point2ExtendedRep P) (point2ExtendedRep Q). + Proof. + intros. + setoid_rewrite <-(proj2_sig extendedRepAdd_sig P Q (point2ExtendedRep P) (point2ExtendedRep Q)); reflexivity. + Qed. + + Lemma extendedRepAdd_proper : Proper (extendedRepEquiv==>extendedRepEquiv==>extendedRepEquiv) extendedRepAdd. + Proof. + repeat intro. + pose proof point2ExtendedRep_extendedRep2Point. + setoid_rewrite <- (proj2_sig extendedRepAdd_sig (extendedRep2Point x) (extendedRep2Point x0) x x0); + try setoid_rewrite <- (proj2_sig extendedRepAdd_sig (extendedRep2Point y) (extendedRep2Point y0) y y0); + congruence. + Qed. + + + (* + Lemma path_sig {A P} (x y : @sig A P) (pf : proj1_sig x = proj1_sig y) (pf' : + eq_rect _ P (proj2_sig x) _ pf = proj2_sig y) + : x = y. + Proof. destruct x, y; simpl in *; destruct pf, pf'; reflexivity. Defined. + + Axiom BAD_equiv_eq : forall P Q :extendedRep, P === Q <-> P = Q. + rewrite BAD_equiv_eq. + + cbv iota beta delta [proj1_sig extendedRep2Extended extendedRep2ExtendedPoint extendedPoint2ExtendedRep extended2Rep unifiedAddM1 unifiedAddM1']. + + lazymatch goal with + | [ |- ?LHS = ?e ?x ?y ] + => is_evar e; is_var x; is_var y; (* sanity checks *) + revert x y; + lazymatch goal with + | [ |- forall x' y', @?P x' y' = _ ] + => unify P e + end + end; reflexivity. + + + Definition mkSigBinop : forall T (P:T->Prop) (f:T->T->T) (f_ok:forall x y, P x -> P y -> P(f x y)) (x y:sig P), sig P. + Proof. + intros. + exists (f (proj1_sig x) (proj1_sig y)). + abstract (destruct x; destruct y; eauto). + Defined. + instantiate (1:=mkSigBinop _ _ _ _). + unfold mkSigBinop. + reflexivity. + Or perhaps you are looking for this theorem? + + + and then you want something like + ? + + (You might need to run [shelve. Grab Existential Variables.], where [shelve] + is: + + Ltac shelve := + idtac; + let H := fresh in + lazymatch goal with + | [ |- ?G ] => evar (H : G); exact H + end. + ) + +*) + + + + Lemma + + (* + apply extendedRepEquiv_refl_proj1_sig. + unfold extendedPoint2ExtendedRep. + simpl. + reflexivity. + + destruct P as [[[]]]; destruct Q as [[[]]]. + cbv iota beta delta [proj1_sig extendedRep2Extended extendedRep2ExtendedPoint extendedPoint2ExtendedRep extended2Rep unifiedAddM1 unifiedAddM1']. + + rewrite extendedRepEquiv_iff_extendedPoint in *. + + cbv iota beta delta [proj1_sig extendedPoint2ExtendedRep extended2Rep unifiedAddM1 unifiedAddM1']. + *) + reflexivity. + Qed. + + Definition extendedRepAdd_bottomup P Q : { R | extendedRep2Extended R = unifiedAddM1' (extendedRep2Extended P) (extendedRep2Extended Q) }. + Proof. + destruct P as [[[]]]; destruct Q as [[[]]]; eexists. + cbv iota beta delta [proj1_sig extendedRep2Extended unifiedAddM1']. + + SearchAbout FRepAdd. match goal with |- context[?E] => - match E with let '{| extendedX := _; extendedY := _; extendedZ := _; extendedT := _ |} := ?X in _ + match E with let _ := ?X in _ => let E' := (eval pattern X in E) in change E with E'; match E' with ?f _ => set (proj := f) end -- cgit v1.2.3 From 55df05020ac8f8ad5797d0ff4d51c8523b141e6a Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 1 Jun 2016 14:47:48 -0400 Subject: leibniz equal version of topdown rewriting of sigma types: nicer --- src/Specific/Ed25519.v | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index bf23276f9..23346bebd 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -461,20 +461,10 @@ Section ESRepOperations. eq_rect _ P (proj2_sig x) _ pf = proj2_sig y) : x = y. Proof. destruct x, y; simpl in *; destruct pf, pf'; reflexivity. Defined. - lazymatch goal with - |- ?LHS = _ :> ?T - => lazymatch eval hnf in T with - @sig ?A ?P - => let lem := constr:(fun x y pf => @path_sig A P LHS (exist _ x y) pf) in - pose proof lem as lem'; - cbv [proj2_sig] in lem'; - simpl @proj1_sig in lem'; - specialize (fun x pf y => lem' x y pf); - specialize (fun x pf => lem' x pf _ eq_refl) - end - end. - apply lem'. - + Definition path_sig' {A P} (x : @sig A P) (y0:A) (pf : proj1_sig x = y0) + : x = exist _ y0 (eq_rect _ P (proj2_sig x) _ pf). + Proof. eapply path_sig. reflexivity. Qed. + apply path_sig'. Grab Existential Variables. repeat match goal with [H : _ |- _] => revert H end ; intros. reflexivity. -- cgit v1.2.3 From 3d62b9ac5697c4713ee5ffb976e7e054b1c81c93 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 3 Jun 2016 15:44:20 -0400 Subject: Let_In rewriting --- src/Specific/Ed25519.v | 295 ++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 258 insertions(+), 37 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 23346bebd..ac9bba8ec 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -16,23 +16,82 @@ Local Open Scope equiv_scope. (*TODO: move enerything before the section out of this file *) +Fixpoint tuple' n T : Type := + match n with + | O => T + | S n' => (tuple' n' T * T)%type + end. + +Definition tuple n T : Type := + match n with + | O => unit + | S n' => tuple' n' T + end. + +Fixpoint fieldwise' {A B} (n:nat) (R:A->B->Prop) (a:tuple' n A) (b:tuple' n B) {struct n} : Prop. + destruct n; simpl @tuple' in *. + { exact (R a b). } + { exact (R (snd a) (snd b) /\ fieldwise' _ _ n R (fst a) (fst b)). } +Defined. + +Definition fieldwise {A B} (n:nat) (R:A->B->Prop) (a:tuple n A) (b:tuple n B) : Prop. + destruct n; simpl @tuple in *. + { exact True. } + { exact (fieldwise' _ R a b). } +Defined. + +Global Instance Equivalence_fieldwise' {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}: + Equivalence (fieldwise' n R). +Proof. + induction n; [solve [auto]|]. + simpl; constructor; repeat intro; intuition eauto. +Qed. + +Global Instance Equivalence_fieldwise {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}: + Equivalence (fieldwise n R). +Proof. + destruct n; (repeat constructor || apply Equivalence_fieldwise'). +Qed. + +Arguments fieldwise' {A B n} _ _ _. +Arguments fieldwise {A B n} _ _ _. + + Local Ltac set_evars := repeat match goal with | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E) end. + Local Ltac subst_evars := repeat match goal with | [ e := ?E |- _ ] => is_evar E; subst e end. +Definition path_sig {A P} {RA:relation A} {Rsig:relation (@sig A P)} + {HP:Proper (RA==>Basics.impl) P} + (H:forall (x y:A) (px:P x) (py:P y), RA x y -> Rsig (exist _ x px) (exist _ y py)) + (x : @sig A P) (y0:A) (pf : RA (proj1_sig x) y0) +: Rsig x (exist _ y0 (HP _ _ pf (proj2_sig x))). +Proof. destruct x. eapply H. assumption. Defined. + 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} R {Reflexive_R:@Reflexive P R} +Global Instance Let_In_Proper_changebody {A P R} {Reflexive_R:@Reflexive P R} : Proper (eq ==> pointwise_relation _ R ==> R) (@Let_In A (fun _ => P)). Proof. lazy; intros; try congruence. subst; auto. Qed. +Lemma Let_In_Proper_changevalue {A B} RA {RB} (f:A->B) {Proper_f:Proper (RA==>RB) f} + : Proper (RA ==> RB) (fun x => Let_In x f). +Proof. intuition. Qed. + +Ltac fold_identity_lambdas := + repeat match goal with + | [ H: appcontext [fun x => ?f x] |- _ ] => change (fun x => f x) with f in * + | |- appcontext [fun x => ?f x] => change (fun x => f x) with f in * + end. + Local Ltac replace_let_in_with_Let_In := match goal with | [ |- context G[let x := ?y in @?z x] ] @@ -355,14 +414,11 @@ Section ESRepOperations. rewrite <-(scalarMultM1_rep a_eq_minus1), <-(@iter_op_spec _ extendedPoint_eq _ _ (@unifiedAddM1 _ a_eq_minus1) _ (@unifiedAddM1_assoc _ a_eq_minus1) _ (@unifiedAddM1_0_l _ a_eq_minus1) _ _ SRep_testbit_correct _ _ _ (bound_satisfied _)). reflexivity. Defined. +End ESRepOperations. +Section EFRepDefn. + Context {tep:TwistedEdwardsParams} {a_eq_minus1:a = opp 1}. Context `{FRepEquiv_ok:Equivalence FRep FRepEquiv} {F2Rep : F q -> FRep} {rep2F:FRep -> F q} {rep2F_proper: Proper (FRepEquiv==>eq) rep2F} {rep2F_F2Rep: forall x, rep2F (F2Rep x) = x}. - Context `{FRepAdd_correct:forall a b, F2Rep (add a b) === FRepAdd (F2Rep a) (F2Rep b)} {FRepAdd_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepAdd}. - Context `{FRepMul_correct:forall a b, F2Rep (mul a b) === FRepMul (F2Rep a) (F2Rep b)} {FRepMul_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepMul}. - Context `{FRepSub_correct:forall a b, F2Rep (sub a b) === FRepSub (F2Rep a) (F2Rep b)} {FRepSub_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepSub}. - Context {FRepInv:FRep->FRep} {FRepInv_correct:forall x, F2Rep (inv x) === FRepInv (F2Rep x)} {FRepInv_proper: Proper (FRepEquiv==>FRepEquiv) FRepInv}. - Context {FRepOpp : FRep -> FRep} {FRepOpp_correct : forall x, F2Rep (opp x) = FRepOpp (F2Rep x)} {FRepOpp_proper: Proper (FRepEquiv==>FRepEquiv) FRepOpp}. - Definition extended2Rep (P:extended) := let 'mkExtended X Y Z T := P in (F2Rep X, F2Rep Y, F2Rep Z, F2Rep T). @@ -370,13 +426,14 @@ Section ESRepOperations. let '(X, Y, Z, T) := P in mkExtended (rep2F X) (rep2F Y) (rep2F Z) (rep2F T). Definition extendedPointInvariant P := rep P (extendedToTwisted P) /\ E.onCurve (extendedToTwisted P). - Definition extendedRep := { XYZT | extendedPointInvariant (extendedRep2Extended XYZT) }. + Definition extendedRepInvariant XYZT := extendedPointInvariant (extendedRep2Extended XYZT). + Definition extendedRep := { XYZT | extendedRepInvariant XYZT }. Lemma extendedRep2Extended_extended2Rep P : extendedRep2Extended (extended2Rep P) = P. Proof. destruct P as [? ? ? ?]; simpl; rewrite !rep2F_F2Rep; reflexivity. Qed. Definition extendedPoint2ExtendedRep (P:extendedPoint) : extendedRep. exists (extended2Rep (proj1_sig P)). - Proof. abstract (rewrite extendedRep2Extended_extended2Rep; destruct P; eauto). Defined. + Proof. abstract (unfold extendedRepInvariant; rewrite extendedRep2Extended_extended2Rep; destruct P; eauto). Defined. Definition extendedRep2ExtendedPoint (P:extendedRep) : extendedPoint. exists (extendedRep2Extended (proj1_sig P)). Proof. abstract (destruct P; eauto). Defined. @@ -442,47 +499,211 @@ Section ESRepOperations. intros; unfold equiv, extendedRepEquiv; pose proof extendedRep2Point_point2ExtendedRep; congruence. Qed. - Lemma extendedRepEquiv_refl_proj1_sig : forall P Q : extendedRep, proj1_sig P = proj1_sig Q -> P === Q. - Admitted. + Global Instance Proper_extendedRepInvariant : Proper ((fieldwise (n:=4) FRepEquiv) ==> Basics.impl) (extendedRepInvariant). + Proof. + repeat intro; cbv [tuple tuple' fieldwise fieldwise' extendedRepInvariant extendedRep2Extended] in *. + repeat match goal with + | [x : prod _ _ |- _ ] => destruct x + end. + simpl in *; intuition. + repeat match goal with + | [H: FRepEquiv _ _ |- _ ] => rewrite <- H; [] + end; trivial. + Qed. - Definition extendedRepAdd_sig : { op | forall P Q rP rQ, rP === point2ExtendedRep P -> rQ === point2ExtendedRep Q -> point2ExtendedRep (E.add P Q) === op rP rQ }. + Lemma extendedRep_proof_equiv: forall x y px py, fieldwise (n:=4) FRepEquiv x y -> + exist extendedRepInvariant x px === exist extendedRepInvariant y py. Proof. - eexists; intros ? ? ? ? HP HQ. - pose proof unifiedAddM1_rep a_eq_minus1 (extendedRep2ExtendedPoint rP) (extendedRep2ExtendedPoint rQ) as H. - setoid_rewrite unExtendedPoint_extendedRep2ExtendedPoint in H. - rewrite HP in H. - rewrite HQ in H. - rewrite !extendedRep2Point_point2ExtendedRep in H. - rewrite H; clear H HP HQ P Q. rename rQ into Q; rename rP into P. - rewrite point2ExtendedRep_unExtendedPoint at 1. - Axiom BAD: forall x y :extendedRep, x === y <-> x = y. - rewrite BAD. - Lemma path_sig {A P} (x y : @sig A P) (pf : proj1_sig x = proj1_sig y) (pf' : - eq_rect _ P (proj2_sig x) _ pf = proj2_sig y) - : x = y. - Proof. destruct x, y; simpl in *; destruct pf, pf'; reflexivity. Defined. - Definition path_sig' {A P} (x : @sig A P) (y0:A) (pf : proj1_sig x = y0) - : x = exist _ y0 (eq_rect _ P (proj2_sig x) _ pf). - Proof. eapply path_sig. reflexivity. Qed. - apply path_sig'. - Grab Existential Variables. - repeat match goal with [H : _ |- _] => revert H end ; intros. - reflexivity. + destruct x as [[[]]]; destruct y as [[[]]]; simpl in *; intuition. + apply E.point_eq. unfold extendedRep2ExtendedPoint; simpl. + repeat match goal with + | [H: FRepEquiv _ _ |- _ ] => rewrite <- H; [] + end; trivial. + Qed. + + Definition extended2Rep_mkExtended x y z t : + extended2Rep (mkExtended x y z t) = (F2Rep x, F2Rep y, F2Rep z, F2Rep t) := eq_refl. + +End EFRepDefn. +Section EFRepOperations. + Context {tep:TwistedEdwardsParams} {a_eq_minus1:a = opp 1}. + Context `{FRepEquiv_ok:Equivalence FRep FRepEquiv} {F2Rep : F q -> FRep} {rep2F:FRep -> F q} {rep2F_proper: Proper (FRepEquiv==>eq) rep2F} {rep2F_F2Rep: forall x, rep2F (F2Rep x) = x} {F2Rep_rep2F: forall x, F2Rep (rep2F x) === x}. + Existing Instances tep FRepEquiv_ok. + + Context `{FRepAdd_correct:forall a b, F2Rep (add a b) === FRepAdd (F2Rep a) (F2Rep b)} {FRepAdd_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepAdd}. + Context `{FRepMul_correct:forall a b, F2Rep (mul a b) === FRepMul (F2Rep a) (F2Rep b)} {FRepMul_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepMul}. + Context `{FRepSub_correct:forall a b, F2Rep (sub a b) === FRepSub (F2Rep a) (F2Rep b)} {FRepSub_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepSub}. + Context {FRepInv:FRep->FRep} {FRepInv_correct:forall x, F2Rep (inv x) === FRepInv (F2Rep x)} {FRepInv_proper: Proper (FRepEquiv==>FRepEquiv) FRepInv}. + Context {FRepOpp : FRep -> FRep} {FRepOpp_correct : forall x, F2Rep (opp x) = FRepOpp (F2Rep x)} {FRepOpp_proper: Proper (FRepEquiv==>FRepEquiv) FRepOpp}. + + Create HintDb toFRep discriminated. + Hint Rewrite + @unfoldDiv + FRepAdd_correct FRepMul_correct FRepSub_correct FRepInv_correct FRepOpp_correct + F2Rep_rep2F + : toFRep. + + Definition extendedRepAdd_sig : forall P Q, + { x | forall Pref Qref, + P === (point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep)) Pref + -> Q === (point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep)) Qref + -> x === point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep) (E.add Pref Qref)}. + Proof. + destruct P as [[[[]]] ?]; destruct Q as [[[[]]] ?]. + eexists; intros ? ? HP HQ; fold_identity_lambdas. + + match goal with + [ Hx : ?x === point2ExtendedRep ?p, Hy : ?y === point2ExtendedRep ?q |- _ ] + => pose proof unifiedAddM1_rep a_eq_minus1 (extendedRep2ExtendedPoint x) (extendedRep2ExtendedPoint y) as H; + setoid_rewrite unExtendedPoint_extendedRep2ExtendedPoint in H; + rewrite HP, HQ, !extendedRep2Point_point2ExtendedRep in H; + rewrite H; clear H Hx Hy; try clear p q + end. + + rewrite point2ExtendedRep_unExtendedPoint. + + symmetry; + eapply (path_sig (RA:=fieldwise (n:=4) FRepEquiv)); + eapply extendedRep_proof_equiv; assumption. + + Grab Existential Variables. + cbv iota beta delta [proj1_sig extendedRep2Extended extendedRep2ExtendedPoint extendedPoint2ExtendedRep unifiedAddM1 unifiedAddM1']. + + assert (Proper (eq==>fieldwise (n:=4) FRepEquiv) (@extended2Rep tep FRep F2Rep)) as HProper by admit. + etransitivity; [ + eapply HProper; + repeat (replace_let_in_with_Let_In; + eapply Let_In_Proper_changebody; + [reflexivity| + cbv beta delta [pointwise_relation]; intro + ]); + reflexivity|]. + + Lemma Let_app_In' : forall {A B T} {R} {R_equiv:@Equivalence T R} + (g : A -> B) (f : B -> T) (x : A) + f' (f'_ok: forall z, f' z === f (g z)), + Let_In (g x) f === Let_In x f'. + Proof. intros; cbv [Let_In]; rewrite f'_ok; reflexivity. Qed. + Definition unfold_Let_In {A B} x (f:A->B) : Let_In x f = let y := x in f y := eq_refl. + + Local Opaque Let_In. + repeat setoid_rewrite <-(pull_Let_In extended2Rep). setoid_rewrite extended2Rep_mkExtended. + + Ltac pattern_reflexivity := + intros; + try reflexivity; + lazymatch goal with + |- _ ?LHS (?f ?a) => + let t := eval pattern a in LHS in + match t with + ?LHS' ?x => unify LHS' f; reflexivity + end + end. + + Ltac descend := + idtac; ( + lazymatch goal with + |- ?R (Let_In ?x ?f) ?RHS => + let A := type of x in + eapply (@Let_In_Proper_changebody A _ R); + [eauto with typeclass_instances + |reflexivity + |cbv beta delta [pointwise_relation]; intro] + end || fail "goal must be of the form [LetIn _ _ == _]"). + + Ltac inLetInBody' t := + etransitivity; [descend; t; pattern_reflexivity|]. + Tactic Notation "inLetInBody" tactic3(t) := inLetInBody' t. + + Ltac inLetInValue' properTac rewriteTac := + etransitivity; + [eapply (Let_In_Proper_changevalue FRepEquiv); [properTac | rewriteTac; pattern_reflexivity]|]. + Tactic Notation "inLetInValue" tactic3(properTac) tactic3(rewriteTac) := inLetInValue' properTac rewriteTac. + + etransitivity. + + etransitivity. + descend. + etransitivity. + descend. + etransitivity. + descend. + etransitivity. + descend. + etransitivity. + descend. + etransitivity. + descend. + etransitivity. + descend. + etransitivity. + descend. + etransitivity. + descend. + etransitivity. + descend. + etransitivity. + descend. + etransitivity. + descend. + + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; + try (inLetInValue admit (rewrite_strat topdown hints toFRep)); + pattern_reflexivity. + + reflexivity. Defined. - Definition extendedRepAdd : extendedRep -> extendedRep -> extendedRep := proj1_sig extendedRepAdd_sig. + Definition extendedRepAdd (P Q:extendedRep) : extendedRep := + Eval cbv beta delta [proj1_sig extendedRepAdd_sig] in (proj1_sig (extendedRepAdd_sig P Q)). + Definition admit : forall {T}, T. Admitted. + Eval cbv beta delta [proj1_sig extendedRepAdd] in (fun P Q => Lemma extendedRepAdd_correct : forall P Q, - point2ExtendedRep (E.add P Q) === extendedRepAdd (point2ExtendedRep P) (point2ExtendedRep Q). + point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep) (E.add P Q) === extendedRepAdd (point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep) P) (point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep) Q). Proof. intros. - setoid_rewrite <-(proj2_sig extendedRepAdd_sig P Q (point2ExtendedRep P) (point2ExtendedRep Q)); reflexivity. + setoid_rewrite <-(proj2_sig (extendedRepAdd_sig (point2ExtendedRep P) (point2ExtendedRep Q)) P Q); reflexivity. Qed. Lemma extendedRepAdd_proper : Proper (extendedRepEquiv==>extendedRepEquiv==>extendedRepEquiv) extendedRepAdd. Proof. repeat intro. - pose proof point2ExtendedRep_extendedRep2Point. + pose proof (point2ExtendedRep_extendedRep2Point (rep2F_F2Rep:=rep2F_F2Rep)). setoid_rewrite <- (proj2_sig extendedRepAdd_sig (extendedRep2Point x) (extendedRep2Point x0) x x0); try setoid_rewrite <- (proj2_sig extendedRepAdd_sig (extendedRep2Point y) (extendedRep2Point y0) y y0); congruence. -- cgit v1.2.3 From c255dd3d45d9ab3e487ae5db58c14bac3a51c90c Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 4 Jun 2016 00:17:17 -0400 Subject: rewrite in Let_In binder by tactic --- src/Specific/Ed25519.v | 70 +++++++++++++++++++++++++++++++------------------- 1 file changed, 43 insertions(+), 27 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index ac9bba8ec..0d6f91cd7 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -595,7 +595,7 @@ Section EFRepOperations. lazymatch goal with |- _ ?LHS (?f ?a) => let t := eval pattern a in LHS in - match t with + lazymatch t with ?LHS' ?x => unify LHS' f; reflexivity end end. @@ -617,8 +617,10 @@ Section EFRepOperations. Ltac inLetInValue' properTac rewriteTac := etransitivity; - [eapply (Let_In_Proper_changevalue FRepEquiv); [properTac | rewriteTac; pattern_reflexivity]|]. - Tactic Notation "inLetInValue" tactic3(properTac) tactic3(rewriteTac) := inLetInValue' properTac rewriteTac. + [eapply (Let_In_Proper_changevalue equiv); [properTac|rewriteTac; pattern_reflexivity]|]. + Tactic Notation "inLetInValue" tactic3(rewriteTac) := inLetInValue' idtac rewriteTac. + Tactic Notation "inLetInValue" tactic3(rewriteTac) "by" tactic3(properTac) := inLetInValue' properTac rewriteTac. + Ltac prtc := abstract (repeat intro; repeat rewrite unfold_Let_In; simpl; intuition; repeat f_equiv; assumption). etransitivity. @@ -649,41 +651,55 @@ Section EFRepOperations. pattern_reflexivity. erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + pattern_reflexivity. + erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; - try (inLetInValue admit (rewrite_strat topdown hints toFRep)); - pattern_reflexivity. + try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). + pattern_reflexivity. + + rewrite_strat bottomup unfold_Let_In. reflexivity. Defined. -- cgit v1.2.3 From 3c8a22e82b2162bff4d6d7b8ce813430bc859c77 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 6 Jun 2016 18:35:31 -0400 Subject: ed25519: refactor some Proper --- src/Specific/Ed25519.v | 351 +++++++++++++++++++------------------------------ src/Specific/GF25519.v | 11 ++ 2 files changed, 146 insertions(+), 216 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 0d6f91cd7..fbe461a96 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -13,6 +13,8 @@ Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil Crypto.Rep. Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. Require Import Zdiv. Local Open Scope equiv_scope. + +Generalizable All Variables. (*TODO: move enerything before the section out of this file *) @@ -120,41 +122,73 @@ Lemma Let_app_In {A B T} (g:A->B) (f:B->T) (x:A) : @Let_In _ (fun _ => T) x (fun p => f (g x)). Proof. reflexivity. Qed. +Lemma Let_app_In' : forall {A B T} {R} {R_equiv:@Equivalence T R} + (g : A -> B) (f : B -> T) (x : A) + f' (f'_ok: forall z, f' z === f (g z)), + Let_In (g x) f === Let_In x f'. +Proof. intros; cbv [Let_In]; rewrite f'_ok; reflexivity. Qed. +Definition unfold_Let_In {A B} x (f:A->B) : Let_In x f = let y := x in f y := eq_refl. + 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. -Lemma funexp_proj {T T'} (proj : T -> T') (f : T -> T) (f' : T' -> T') x n - (f_proj : forall a, proj (f a) = f' (proj a)) - : proj (funexp f x n) = funexp f' (proj x) n. +Lemma funexp_proj {T T'} `{@Equivalence T' RT'} + (proj : T -> T') + (f : T -> T) + (f' : T' -> T') {Proper_f':Proper (RT'==>RT') f'} + (f_proj : forall a, proj (f a) === f' (proj a)) + x n + : proj (funexp f x n) === funexp f' (proj x) n. +Proof. + revert x; induction n as [|n IHn]; simpl; intros. + - reflexivity. + - rewrite f_proj. rewrite IHn. reflexivity. +Qed. + +Global Instance pair_Equivalence {A B} `{@Equivalence A RA} `{@Equivalence B RB} : @Equivalence (A*B) (fun x y => fst x = fst y /\ snd x === snd y). Proof. - revert x; induction n as [|n IHn]; simpl; congruence. + constructor; repeat intro; intuition; try congruence. + match goal with [H : _ |- _ ] => solve [rewrite H; auto] end. +Qed. + +Global Instance Proper_test_and_op {T scalar} `{Requiv:@Equivalence T RT} + {op:T->T->T} {Proper_op:Proper (RT==>RT==>RT) op} + {testbit:scalar->nat->bool} {s:scalar} {zero:T} : + let R := fun x y => fst x = fst y /\ snd x === snd y in + Proper (R==>R) (test_and_op op testbit s zero). +Proof. + unfold test_and_op; simpl; repeat intro; intuition; + repeat match goal with + | [ |- context[match ?n with _ => _ end] ] => destruct n eqn:?; simpl in *; subst; try discriminate; auto + | [ H: _ |- _ ] => setoid_rewrite H; reflexivity + end. Qed. -Lemma iter_op_proj {T T' S} (proj : T -> T') (op : T -> T -> T) (op' : T' -> T' -> T') x y z +Lemma iter_op_proj {T T' S} `{T'Equiv:@Equivalence T' RT'} + (proj : T -> T') (op : T -> T -> T) (op' : T' -> T' -> T') {Proper_op':Proper (RT' ==> RT' ==> RT') op'} x y z (testbit : S -> nat -> bool) (bound : nat) - (op_proj : forall a b, proj (op a b) = op' (proj a) (proj b)) - : proj (iter_op op x testbit y z bound) = iter_op op' (proj x) testbit y (proj z) bound. + (op_proj : forall a b, proj (op a b) === op' (proj a) (proj b)) + : proj (iter_op op x testbit y z bound) === iter_op op' (proj x) testbit y (proj z) bound. Proof. unfold iter_op. - simpl. lazymatch goal with - | [ |- ?proj (snd (funexp ?f ?x ?n)) = snd (funexp ?f' _ ?n) ] - => pose proof (fun x0 x1 => funexp_proj (fun x => (fst x, proj (snd x))) f f' (x0, x1)) as H' + | [ |- ?proj (snd (funexp ?f ?x ?n)) === snd (funexp ?f' _ ?n) ] + => pose proof (fun pf x0 x1 => @funexp_proj _ _ _ _ (fun x => (fst x, proj (snd x))) f f' (Proper_test_and_op (Requiv:=T'Equiv)) pf (x0, x1)) as H'; + lazymatch type of H' with + | ?H'' -> _ => assert (H'') as pf; [clear H'|edestruct (H' pf); simpl in *; solve [eauto]] + end end. - simpl in H'. - rewrite <- H'. - { reflexivity. } - { intros [??]; simpl. - repeat match goal with - | [ |- context[match ?n with _ => _ end] ] - => destruct n eqn:? - | _ => progress simpl - | _ => progress subst - | _ => reflexivity - | _ => rewrite op_proj - end. } + + intros [??]; simpl. + repeat match goal with + | [ |- context[match ?n with _ => _ end] ] => destruct n eqn:? + | _ => progress (unfold equiv; simpl) + | _ => progress (subst; intuition) + | _ => reflexivity + | _ => rewrite op_proj + end. Qed. Global Instance option_rect_Proper_nd {A T} @@ -216,8 +250,6 @@ Local Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [optio Definition COMPILETIME {T} (x:T) : T := x. - - Lemma N_to_nat_le_mono : forall a b, (a <= b)%N -> (N.to_nat a <= N.to_nat b)%nat. Proof. intros. @@ -356,7 +388,6 @@ Qed. Lemma unfold_E_sub : forall {prm:TwistedEdwardsParams} a b, (a - b = a + E.opp b)%E. Proof. reflexivity. Qed. -Generalizable All Variables. Section FSRepOperations. Context {q:Z} {prime_q:Znumtheory.prime q} {two_lt_q:(2 < q)%Z}. Context {l:Z} {two_lt_l:(2 < l)%Z}. @@ -374,8 +405,10 @@ Section FSRepOperations. erewrite <-pow_nat_iter_op_correct by auto. erewrite <-(fun x => iter_op_spec (scalar := SRep) mul F_mul_assoc _ F_mul_1_l _ _ SRep_testbit_correct n x width) by auto. rewrite <-(rcFOK 1%F) at 1. - erewrite <-iter_op_proj by auto. - reflexivity. + erewrite <-iter_op_proj; + [apply eq_refl + |eauto with typeclass_instances + |symmetry; eapply FRepMul_correct]. Qed. Context (q_minus_2_lt_l:(q - 2 < l)%Z). @@ -524,10 +557,7 @@ Section EFRepDefn. Definition extended2Rep_mkExtended x y z t : extended2Rep (mkExtended x y z t) = (F2Rep x, F2Rep y, F2Rep z, F2Rep t) := eq_refl. -End EFRepDefn. -Section EFRepOperations. - Context {tep:TwistedEdwardsParams} {a_eq_minus1:a = opp 1}. - Context `{FRepEquiv_ok:Equivalence FRep FRepEquiv} {F2Rep : F q -> FRep} {rep2F:FRep -> F q} {rep2F_proper: Proper (FRepEquiv==>eq) rep2F} {rep2F_F2Rep: forall x, rep2F (F2Rep x) = x} {F2Rep_rep2F: forall x, F2Rep (rep2F x) === x}. + Context `{F2Rep_rep2F: forall x, F2Rep (rep2F x) === x}. Existing Instances tep FRepEquiv_ok. Context `{FRepAdd_correct:forall a b, F2Rep (add a b) === FRepAdd (F2Rep a) (F2Rep b)} {FRepAdd_proper: Proper (FRepEquiv==>FRepEquiv==>FRepEquiv) FRepAdd}. @@ -545,9 +575,9 @@ Section EFRepOperations. Definition extendedRepAdd_sig : forall P Q, { x | forall Pref Qref, - P === (point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep)) Pref - -> Q === (point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep)) Qref - -> x === point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep) (E.add Pref Qref)}. + P === point2ExtendedRep Pref + -> Q === point2ExtendedRep Qref + -> x === point2ExtendedRep (E.add Pref Qref)}. Proof. destruct P as [[[[]]] ?]; destruct Q as [[[[]]] ?]. eexists; intros ? ? HP HQ; fold_identity_lambdas. @@ -569,7 +599,7 @@ Section EFRepOperations. Grab Existential Variables. cbv iota beta delta [proj1_sig extendedRep2Extended extendedRep2ExtendedPoint extendedPoint2ExtendedRep unifiedAddM1 unifiedAddM1']. - assert (Proper (eq==>fieldwise (n:=4) FRepEquiv) (@extended2Rep tep FRep F2Rep)) as HProper by admit. + assert (Proper (eq==>fieldwise (n:=4) FRepEquiv) extended2Rep) as HProper by admit. etransitivity; [ eapply HProper; repeat (replace_let_in_with_Let_In; @@ -579,13 +609,6 @@ Section EFRepOperations. ]); reflexivity|]. - Lemma Let_app_In' : forall {A B T} {R} {R_equiv:@Equivalence T R} - (g : A -> B) (f : B -> T) (x : A) - f' (f'_ok: forall z, f' z === f (g z)), - Let_In (g x) f === Let_In x f'. - Proof. intros; cbv [Let_In]; rewrite f'_ok; reflexivity. Qed. - Definition unfold_Let_In {A B} x (f:A->B) : Let_In x f = let y := x in f y := eq_refl. - Local Opaque Let_In. repeat setoid_rewrite <-(pull_Let_In extended2Rep). setoid_rewrite extended2Rep_mkExtended. @@ -652,7 +675,6 @@ Section EFRepOperations. pattern_reflexivity. erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). - pattern_reflexivity. erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; @@ -698,7 +720,7 @@ Section EFRepOperations. erewrite <- Let_app_In' with (g:=F2Rep); [|pattern_reflexivity]; try (inLetInValue (rewrite_strat topdown hints toFRep) by prtc). pattern_reflexivity. - + rewrite_strat bottomup unfold_Let_In. reflexivity. @@ -706,193 +728,86 @@ Section EFRepOperations. Definition extendedRepAdd (P Q:extendedRep) : extendedRep := Eval cbv beta delta [proj1_sig extendedRepAdd_sig] in (proj1_sig (extendedRepAdd_sig P Q)). - Definition admit : forall {T}, T. Admitted. - Eval cbv beta delta [proj1_sig extendedRepAdd] in (fun P Q => Lemma extendedRepAdd_correct : forall P Q, - point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep) (E.add P Q) === extendedRepAdd (point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep) P) (point2ExtendedRep (rep2F_F2Rep:=rep2F_F2Rep) Q). + point2ExtendedRep (E.add P Q) === extendedRepAdd (point2ExtendedRep P) (point2ExtendedRep Q). Proof. intros. - setoid_rewrite <-(proj2_sig (extendedRepAdd_sig (point2ExtendedRep P) (point2ExtendedRep Q)) P Q); reflexivity. + rewrite (proj2_sig (extendedRepAdd_sig (point2ExtendedRep P) (point2ExtendedRep Q)) P Q); reflexivity. Qed. Lemma extendedRepAdd_proper : Proper (extendedRepEquiv==>extendedRepEquiv==>extendedRepEquiv) extendedRepAdd. Proof. repeat intro. - pose proof (point2ExtendedRep_extendedRep2Point (rep2F_F2Rep:=rep2F_F2Rep)). - setoid_rewrite <- (proj2_sig extendedRepAdd_sig (extendedRep2Point x) (extendedRep2Point x0) x x0); - try setoid_rewrite <- (proj2_sig extendedRepAdd_sig (extendedRep2Point y) (extendedRep2Point y0) y y0); - congruence. + pose proof (proj2_sig (extendedRepAdd_sig x x0) (extendedRep2Point x) (extendedRep2Point x0)) as H1. + pose proof (proj2_sig (extendedRepAdd_sig y y0) (extendedRep2Point y) (extendedRep2Point y0)) as H2. + rewrite !point2ExtendedRep_extendedRep2Point in *. + setoid_rewrite H1; try setoid_rewrite H2; congruence. Qed. - - - (* - Lemma path_sig {A P} (x y : @sig A P) (pf : proj1_sig x = proj1_sig y) (pf' : - eq_rect _ P (proj2_sig x) _ pf = proj2_sig y) - : x = y. - Proof. destruct x, y; simpl in *; destruct pf, pf'; reflexivity. Defined. - - Axiom BAD_equiv_eq : forall P Q :extendedRep, P === Q <-> P = Q. - rewrite BAD_equiv_eq. - cbv iota beta delta [proj1_sig extendedRep2Extended extendedRep2ExtendedPoint extendedPoint2ExtendedRep extended2Rep unifiedAddM1 unifiedAddM1']. - - lazymatch goal with - | [ |- ?LHS = ?e ?x ?y ] - => is_evar e; is_var x; is_var y; (* sanity checks *) - revert x y; - lazymatch goal with - | [ |- forall x' y', @?P x' y' = _ ] - => unify P e - end - end; reflexivity. + Context {l:Z} {two_lt_l:(2 < l)%Z} `{S2Rep : F l -> SRep} {rep2S : SRep -> F l}. + Context`{SRepEquiv_ok:Equivalence SRep SRepEquiv} {rep2S_Proper: Proper (SRepEquiv==>eq) rep2S}. + Context {rep2S_S2Rep: forall x, rep2S (S2Rep x) = x}. - - Definition mkSigBinop : forall T (P:T->Prop) (f:T->T->T) (f_ok:forall x y, P x -> P y -> P(f x y)) (x y:sig P), sig P. - Proof. - intros. - exists (f (proj1_sig x) (proj1_sig y)). - abstract (destruct x; destruct y; eauto). - Defined. - instantiate (1:=mkSigBinop _ _ _ _). - unfold mkSigBinop. - reflexivity. - Or perhaps you are looking for this theorem? - - - and then you want something like - ? - - (You might need to run [shelve. Grab Existential Variables.], where [shelve] - is: - - Ltac shelve := - idtac; - let H := fresh in - lazymatch goal with - | [ |- ?G ] => evar (H : G); exact H - end. - ) - -*) - - - - Lemma - - (* - apply extendedRepEquiv_refl_proj1_sig. - unfold extendedPoint2ExtendedRep. - simpl. - reflexivity. - - - destruct P as [[[]]]; destruct Q as [[[]]]. - cbv iota beta delta [proj1_sig extendedRep2Extended extendedRep2ExtendedPoint extendedPoint2ExtendedRep extended2Rep unifiedAddM1 unifiedAddM1']. - - rewrite extendedRepEquiv_iff_extendedPoint in *. + Context {SRep_testbit : SRep -> nat -> bool}. + Context {SRep_testbit_correct : forall (x0 : SRep) (i : nat), SRep_testbit x0 i = N.testbit_nat (FieldToN (rep2S x0)) i}. - cbv iota beta delta [proj1_sig extendedPoint2ExtendedRep extended2Rep unifiedAddM1 unifiedAddM1']. - *) - reflexivity. + Lemma FieldToNat_natToField' {m:Z} (x:nat) : (0 FieldToNat (@natToField m x) = x mod (Z.to_nat m). + intros. symmetry. + pose proof (fun pf => @FieldToNat_natToField (Z.to_nat m) pf x) as Hn. + rewrite Z2Nat.id in Hn by omega. + apply Hn; pose (Z2Nat.inj_le m 0); omega. Qed. - Definition extendedRepAdd_bottomup P Q : { R | extendedRep2Extended R = unifiedAddM1' (extendedRep2Extended P) (extendedRep2Extended Q) }. - Proof. - destruct P as [[[]]]; destruct Q as [[[]]]; eexists. - cbv iota beta delta [proj1_sig extendedRep2Extended unifiedAddM1']. - - SearchAbout FRepAdd. - match goal with |- context[?E] => - match E with let _ := ?X in _ - => let E' := (eval pattern X in E) in - change E with E'; - match E' with ?f _ => set (proj := f) end - end - end. - - etransitivity. - repeat ( - etransitivity; [ - replace_let_in_with_Let_In; - rewrite <-pull_Let_In; - eapply Let_In_Proper_nd; - [solve [eauto with typeclass_instances] - |reflexivity| - cbv beta delta [pointwise_relation]; intro] - |reflexivity]). - subst proj. - cbv beta iota. - reflexivity. - Admitted. - - Definition extendedRepAdd : extendedRep -> extendedRep -> extendedRep := proj1_sig (extendedRepAdd_sig). - Definition extendedRepAdd_correct' : forall P Q, extended2Rep (unifiedAddM1' P Q) === extendedRepAdd (extended2Rep P) (extended2Rep Q) := proj2_sig extendedRepAdd_sig. + Definition N_to_nat_FieldToN {m} (x : F m) : N.to_nat (FieldToN x) = FieldToNat x. + Proof. intros. apply Z_N_nat. Qed. - Lemma extendedRepAdd_correct : forall P Q, point2ExtendedRep (E.add P Q) === extendedRepAdd (point2ExtendedRep P) (point2ExtendedRep Q). + Definition extendedRepMul_sig : forall (n:SRep) (P:extendedRep), + { x | forall (nref:nat) (Pref:E.point), + nref = nref mod Z.to_nat l + -> n === S2Rep (natToField nref) + -> P === point2ExtendedRep Pref + -> x === point2ExtendedRep (E.mul nref Pref)}. Proof. - intros; unfold point2ExtendedRep. - rewrite extendedRepAdd_correct'. - SearchAbout unifiedAddM1'. - rewrite unifiedAddM1_correct. - apply extended2Rep_Proper, unifiedAddM1_correct. - Qed. - - Lemma extendedRepAdd_proper : Proper (extendedRepEquiv==>extendedRepEquiv==>extendedRepEquiv) extendedRepAdd. - Proof. - repeat intro. - etransitivity. + eexists; intros ? ? nred nRep PRep. + + pose proof (@scalarMultExtendedSRep_correct tep a_eq_minus1 l two_lt_l SRep rep2S SRep_testbit SRep_testbit_correct n (extendedRep2ExtendedPoint P)) as H. + rewrite unExtendedPoint_extendedRep2ExtendedPoint in H. + rewrite PRep, extendedRep2Point_point2ExtendedRep in H. + replace (rep2S n) with (@natToField l nref) in H by (rewrite nRep, rep2S_S2Rep; reflexivity). + replace (N.to_nat (FieldToN (natToField nref))) with nref in H + by (rewrite N_to_nat_FieldToN, FieldToNat_natToField', <-nred; intuition omega). + rewrite <-H; clear H nref nred nRep PRep. + + setoid_rewrite point2ExtendedRep_unExtendedPoint. + setoid_rewrite (iter_op_proj _ _ extendedRepAdd). (* FIXME: Finished transaction in 5. secs (5.169999u,0.s) *) + Lemma extendedPoint2ExtendedRep_extendedRep2ExtendedPoint : + forall P, extendedPoint2ExtendedRep (extendedRep2ExtendedPoint P) === P. + Admitted. + Lemma Proper_iter_op : forall {T S} {TR:relation T} {SR:relation S} op zero testbit, + Proper (SR==>TR==>eq==>TR) (@iter_op T S op zero testbit). + Proof. + unfold iter_op; intros. + repeat intro; subst. + Admitted. etransitivity. - SearchAbout point2ExtendedRep. - 3:apply extendedRepAdd_correct. - pose proof (fun P P' Q Q' => Proper_unifiedAddM1 a_eq_minus1 P P' Q Q'). - + 2:eapply Proper_iter_op. + 2:apply eq_refl. + 2:setoid_rewrite extendedPoint2ExtendedRep_extendedRep2ExtendedPoint; reflexivity. + 2:reflexivity. - cbv beta delta [Let_In]. - - rewrite pull_Let_In. - eapply Let_In_Proper_nd; - [solve [eauto with typeclass_instances] - |reflexivity| - cbv beta delta [pointwise_relation]; intro] - |]. - - replace_let_in_with_Let_In. - rewrite <-pull_Let_In. - eapply Let_In_Proper_nd; [eauto with typeclass_instances|reflexivity|cbv beta delta [pointwise_relation]; intro]; - etransitivity. - + Definition extendedPoint2ExtendedRep_mkExtendedPoint P : + (extendedPoint2ExtendedRep (mkExtendedPoint P)) = point2ExtendedRep P := eq_refl. + rewrite extendedPoint2ExtendedRep_mkExtendedPoint. - { etransitivity; [|replace_let_in_with_Let_In; reflexivity]. - repeat ( - autorewrite with FRepOperations; - Let_In_app unRep; - eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [Proper respectful pointwise_relation]; intro]). - lazymatch goal with |- ?LHS = mkExtended (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. + match goal with |- context [?f E.zero] => change (f E.zero) with (COMPILETIME (f E.zero)) end. + 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) := (unRep (fst P), unRep (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. - *) -End ESRepOperations. +End EFRepDefn. Section EdDSADerivation. Context `{eddsaprm:EdDSAParams}. @@ -902,7 +817,7 @@ Section EdDSADerivation. Context `{ERepEnc_correct : forall (P:E.point), enc P = ERepEnc (E2Rep P)} {ERepEnc_proper:Proper (ERepEquiv==>eq) ERepEnc}. Context `{ERepAdd_correct : forall (P Q:E.point), E2Rep (E.add P Q) === ERepAdd (E2Rep P) (E2Rep Q)} {ERepAdd_proper:Proper (ERepEquiv==>ERepEquiv==>ERepEquiv) ERepAdd}. - Context `{ESRepMul_correct : forall (n:F (Z.of_nat l)) (Q:E.point), E2Rep (E.mul (Z.to_nat n) Q) === ESRepMul (S2Rep (ZToField n)) (E2Rep Q)} {ESRepMul_proper : Proper (SRepEquiv==>ERepEquiv==>ERepEquiv) ESRepMul}. + Context `{ESRepMul_correct : forall (n:F (Z.of_nat l)) (Q:E.point), E2Rep (E.mul (FieldToNat n) Q) === ESRepMul (S2Rep (ZToField n)) (E2Rep Q)} {ESRepMul_proper : Proper (SRepEquiv==>ERepEquiv==>ERepEquiv) ESRepMul}. Context `{ERepOpp_correct : forall P:E.point, E2Rep (E.opp P) === ERepOpp (E2Rep P)} {ERepOpp_proper:Proper (ERepEquiv==>ERepEquiv) ERepOpp}. Context `{SRepDec_correct : forall x, option_map (fun x : F (Z.of_nat l) => S2Rep x) (dec x) === SRepDec x}. @@ -962,22 +877,26 @@ Section EdDSADerivation. @ZToField_FieldToZ @SRepH_correct : toESRep. + + Ltac recursive_replace_option_match_with_option_rect := + etransitivity; + [| + repeat match goal with + | [ |- ?x = ?x ] => reflexivity + | _ => replace_option_match_with_option_rect + | [ |- _ = option_rect _ _ _ _ ] + => eapply option_rect_Proper_nd; [ intro | reflexivity.. ] + end; + reflexivity]. Lemma sharper_verify : forall pk l msg sig, { sherper_verify | sherper_verify = verify (n:=l) pk msg sig}. Proof. eexists; cbv [EdDSA.verify]; intros. - etransitivity. Focus 2. { (* match dec .. with -> option_rect *) - repeat match goal with - | [ |- ?x = ?x ] => reflexivity - | _ => replace_option_match_with_option_rect - | [ |- _ = option_rect _ _ _ _ ] - => eapply option_rect_Proper_nd; [ intro | reflexivity.. ] - end. - reflexivity. } Unfocus. + recursive_replace_option_match_with_option_rect. rewrite_strat topdown hints toESRep. - setoid_rewrite ESRepMul_correct. (* TODO: why does [rewrite_strat] not do this? *) + setoid_rewrite ESRepMul_correct. (* TODO: change the spec to use FieldToNat instead of (Z.to_nat (ZToField _))*) rewrite_strat topdown hints toESRep. (* decoding of S : option_rect (F l) -> option_map SRep *) diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 8aaf8caf6..044bf074b 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -51,6 +51,17 @@ Proof. compute_formula. Time Defined. +Local Transparent Let_In. +Infix "<<" := Z.shiftr (at level 50). +Infix "&" := Z.land (at level 50). +Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_mul_reduce_formula Let_In] in + fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 => 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). +Local Opaque Let_In. + + Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula. (* It's easy enough to use extraction to get the proper nice-looking formula. * More Ltac acrobatics will be needed to get out that formula for further use in Coq. -- cgit v1.2.3