From de5416133dc67dcd2729d4c7448991ab2672782a Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 24 May 2016 00:32:09 -0400 Subject: F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more broken... --- src/Specific/Ed25519.v | 663 ++++++++++++++++++++++++------------------------- src/Specific/GF25519.v | 98 +++++++- 2 files changed, 427 insertions(+), 334 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 996aabb21..3db14f057 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -9,7 +9,7 @@ Require Import Crypto.Encoding.PointEncodingPre. Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.PointEncoding. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil. +Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil Crypto.Rep. Local Infix "++" := Word.combine. Local Notation " a '[:' i ']' " := (Word.split1 i _ a) (at level 40). @@ -184,355 +184,352 @@ Definition enc'_correct : @enc (@E.point curve25519params) _ _ = (fun x => enc' => change (option_rect P S N (Some x)) with (S x); cbv beta end. -Axiom SRep : Type. -Axiom S2rep : N -> SRep. -Axiom rep2S : SRep -> N. -Axiom rep2S_S2rep : forall x, x = rep2S (S2rep x). - -Axiom FRep : Type. -Axiom F2rep : F Ed25519.q -> FRep. -Axiom rep2F : FRep -> F Ed25519.q. -Axiom rep2F_F2rep : forall x, x = rep2F (F2rep x). -Axiom wire2rep_F : word (b-1) -> option FRep. -Axiom wire2rep_F_correct : forall x, Fm_dec x = option_map rep2F (wire2rep_F x). - -Axiom FRepMul : FRep -> FRep -> FRep. -Axiom FRepMul_correct : forall x y, (rep2F x * rep2F y)%F = rep2F (FRepMul x y). - -Axiom FRepAdd : FRep -> FRep -> FRep. -Axiom FRepAdd_correct : forall x y, (rep2F x + rep2F y)%F = rep2F (FRepAdd x y). - -Axiom FRepSub : FRep -> FRep -> FRep. -Axiom FRepSub_correct : forall x y, (rep2F x - rep2F y)%F = rep2F (FRepSub x y). - -Axiom FRepInv : FRep -> FRep. -Axiom FRepInv_correct : forall x, inv (rep2F x)%F = rep2F (FRepInv x). - -Axiom FSRepPow : FRep -> SRep -> FRep. -Axiom FSRepPow_correct : forall x n, (rep2F x ^ rep2S n)%F = rep2F (FSRepPow x n). - -Axiom FRepOpp : FRep -> FRep. -Axiom FRepOpp_correct : forall x, opp (rep2F x) = rep2F (FRepOpp x). -Axiom wltu : forall {b}, word b -> word b -> bool. - -Axiom wltu_correct : forall {b} (x y:word b), wltu x y = (wordToN x word (b-1). -Axiom enc_rep2F_correct : forall x, enc_rep2F x = @enc _ _ FqEncoding (rep2F x). - -Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed. - -Definition rep2E (r:FRep * FRep * FRep * FRep) : extended := - match r with (((x, y), z), t) => mkExtended (rep2F x) (rep2F y) (rep2F z) (rep2F t) end. - -Lemma if_map : forall {T U} (f:T->U) (b:bool) (x y:T), (if b then f x else f y) = f (if b then x else y). -Proof. - destruct b; trivial. -Qed. - -Create HintDb FRepOperations discriminated. -Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. - -Local Ltac Let_In_rep2F := - match goal with - | [ |- appcontext G[Let_In (rep2F ?x) ?f] ] - => change (Let_In (rep2F x) f) with (Let_In x (fun y => f (rep2F y))); cbv beta - end. - -Lemma unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. -Proof. - destruct a as [[[]]]; destruct b as [[[]]]. - eexists. - lazymatch goal with |- ?LHS = ?RHS :> ?T => - evar (e:T); replace LHS with e; [subst e|] - end. - unfold rep2E. cbv beta delta [unifiedAddM1']. - pose proof (rep2F_F2rep twice_d) as H; rewrite H; clear H. (* XXX: this is a hack -- rewrite misresolves typeclasses? *) - - { etransitivity; [|replace_let_in_with_Let_In; reflexivity]. - repeat ( - autorewrite with FRepOperations; - Let_In_rep2F; - eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [Proper respectful pointwise_relation]; intro]). - lazymatch goal with |- ?LHS = (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) => - change (LHS = (rep2E (((x, y), z), t))) - end. - reflexivity. } - - subst e. - reflexivity. (* FIXME: do not simpl the goal here, we want to keep the Let_In common subexpressions *) -Defined. - -(*Eval simpl in (fun x1 y1 z1 t1 x2 y2 z2 t2 => proj1_sig (unifiedAddM1Rep_sig (((x1, y1), z1), t1) (((x2, y2), z2), t2))). (* TODO: remove after debugging the fixme three lines above *) *) +Section Ed25519Frep. + Generalizable All Variables. + Context `(rcS:RepConversions N SRep) (rcSOK:RepConversionsOK rcS). + Context `(rcF:RepConversions (F (Ed25519.q)) FRep) (rcFOK:RepConversionsOK rcF). + Context (FRepAdd FRepSub FRepMul:FRep->FRep->FRep) (FRepAdd_correct:RepBinOpOK rcF add FRepMul). + Context (FRepSub_correct:RepBinOpOK rcF sub FRepSub) (FRepMul_correct:RepBinOpOK rcF mul FRepMul). + Local Notation rep2F := (unRep : FRep -> F (Ed25519.q)). + Local Notation F2Rep := (toRep : F (Ed25519.q) -> FRep). + Local Notation rep2S := (unRep : SRep -> N). + Local Notation S2Rep := (toRep : N -> SRep). + + Axiom FRepInv : FRep -> FRep. + Axiom FRepInv_correct : forall x, inv (rep2F x)%F = rep2F (FRepInv x). + + Axiom FSRepPow : FRep -> SRep -> FRep. + Axiom FSRepPow_correct : forall x n, (rep2F x ^ rep2S n)%F = rep2F (FSRepPow x n). + + Axiom FRepOpp : FRep -> FRep. + Axiom FRepOpp_correct : forall x, opp (rep2F x) = rep2F (FRepOpp x). -Definition unifiedAddM1Rep (a b:FRep * FRep * FRep * FRep) : FRep * FRep * FRep * FRep := Eval hnf in proj1_sig (unifiedAddM1Rep_sig a b). -Definition unifiedAddM1Rep_correct a b : rep2E (unifiedAddM1Rep a b) = unifiedAddM1' (rep2E a) (rep2E b) := Eval hnf in proj2_sig (unifiedAddM1Rep_sig a b). + Axiom wltu : forall {b}, word b -> word b -> bool. + Axiom wltu_correct : forall {b} (x y:word b), wltu x y = (wordToN x Let_In (FRepInv (snd (fst P))) (fun iZ => (FRepMul (fst (fst (fst P))) iZ, FRepMul (snd (fst (fst P))) iZ))). -Lemma erep2trep_correct : forall P, rep2T (erep2trep P) = extendedToTwisted (rep2E P). -Proof. - unfold rep2T, rep2E, erep2trep, extendedToTwisted; destruct P as [[[]]]; simpl. - rewrite !unfoldDiv, <-!FRepMul_correct, <-FRepInv_correct. reflexivity. -Qed. + Axiom compare_enc : forall x y, F_eqb x y = weqb (@enc _ _ FqEncoding x) (@enc _ _ FqEncoding y). -Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. -Proof. - eexists; intros. - cbv [ed25519_verify EdDSA.verify - ed25519params curve25519params - EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H - EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding]. + Axiom wire2FRep : word (b-1) -> option FRep. + Axiom wire2FRep_correct : forall x, Fm_dec x = option_map rep2F (wire2FRep x). - etransitivity. - Focus 2. - { repeat match goal with - | [ |- ?x = ?x ] => reflexivity - | [ |- _ = match ?a with None => ?N | Some x => @?S x end :> ?T ] - => etransitivity; - [ - | refine (_ : option_rect (fun _ => T) _ N a = _); - let S' := match goal with |- option_rect _ ?S' _ _ = _ => S' end in - refine (option_rect (fun a' => option_rect (fun _ => T) S' N a' = match a' with None => N | Some x => S x end) - (fun x => _) _ a); intros; simpl @option_rect ]; - [ reflexivity | .. ] - end. - set_evars. - rewrite<- E.point_eqb_correct. - rewrite solve_for_R; unfold E.sub. - rewrite E.opp_mul. - let p1 := constr:(scalarMultM1_rep eq_refl) in - let p2 := constr:(unifiedAddM1_rep eq_refl) in - repeat match goal with - | |- context [(_ * E.opp ?P)%E] => - rewrite <-(unExtendedPoint_mkExtendedPoint P); - rewrite negateExtended_correct; - rewrite <-p1 - | |- context [(_ * ?P)%E] => - rewrite <-(unExtendedPoint_mkExtendedPoint P); - rewrite <-p1 - | _ => rewrite p2 - end; - rewrite ?Znat.Z_nat_N, <-?Word.wordToN_nat; - subst_evars; - reflexivity. - } Unfocus. - - etransitivity. - Focus 2. - { lazymatch goal with |- _ = option_rect _ _ ?false ?dec => - symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => Z.to_N x) _ false dec)] - end. - eapply option_rect_Proper_nd; [intro|reflexivity..]. + Axiom FRep2wire : FRep -> word (b-1). + Axiom FRep2wire_correct : forall x, FRep2wire x = @enc _ _ FqEncoding (rep2F x). + + Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div. congruence. Qed. + + Definition rep2E (r:FRep * FRep * FRep * FRep) : extended := + match r with (((x, y), z), t) => mkExtended (rep2F x) (rep2F y) (rep2F z) (rep2F t) end. + + Lemma if_map : forall {T U} (f:T->U) (b:bool) (x y:T), (if b then f x else f y) = f (if b then x else y). + Proof. + destruct b; trivial. + Qed. + + Create HintDb FRepOperations discriminated. + Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. + + Local Ltac Let_In_unRep := match goal with - | [ |- ?RHS = ?e ?v ] - => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in - unify e RHS' + | [ |- appcontext G[Let_In (unRep ?x) ?f] ] + => change (Let_In (unRep x) f) with (Let_In x (fun y => f (unRep y))); cbv beta end. - reflexivity. - } Unfocus. - rewrite <-decode_scalar_correct. - - etransitivity. - Focus 2. - { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). - symmetry; apply decode_test_encode_test. - } Unfocus. - rewrite enc'_correct. - cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1]. - (* Why does this take too long? - lazymatch goal with |- context [ proj1_sig ?x ] => - fail 5 - end. *) - unfold proj1_sig at 1 2. - etransitivity. - Focus 2. - { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). - set_evars. - repeat match goal with - | [ |- appcontext[@proj1_sig ?A ?P (@iter_op ?T ?f ?neutral ?T' ?testbit ?exp ?base ?bound)] ] - => erewrite (@iter_op_proj T _ _ (@proj1_sig _ _)) by reflexivity - end. - subst_evars. - reflexivity. } - Unfocus. - - cbv [mkExtendedPoint E.zero]. - unfold proj1_sig at 1 2 3 5 6 7 8. - rewrite B_proj. - - etransitivity. - Focus 2. - { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). - set_evars. - lazymatch goal with |- _ = option_rect _ _ ?false ?dec => - symmetry; etransitivity; [|eapply (option_rect_option_map (@proj1_sig _ _) _ false dec)] - end. - eapply option_rect_Proper_nd; [intro|reflexivity..]. - match goal with - | [ |- ?RHS = ?e ?v ] - => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in - unify e RHS' + Lemma unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. + Proof. + destruct a as [[[]]]; destruct b as [[[]]]. + eexists. + lazymatch goal with |- ?LHS = ?RHS :> ?T => + evar (e:T); replace LHS with e; [subst e|] end. - reflexivity. - } Unfocus. - - cbv [dec PointEncoding point_encoding]. - etransitivity. - Focus 2. - { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + unfold rep2E. cbv beta delta [unifiedAddM1']. + pose proof (rcFOK twice_d) as H; rewrite <-H; clear H. (* XXX: this is a hack -- rewrite misresolves typeclasses? *) + + { etransitivity; [|replace_let_in_with_Let_In; reflexivity]. + repeat ( + autorewrite with FRepOperations; + Let_In_unRep; + eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [Proper respectful pointwise_relation]; intro]). + lazymatch goal with |- ?LHS = (unRep ?x, unRep ?y, unRep ?z, unRep ?t) => + change (LHS = (rep2E (((x, y), z), t))) + end. + reflexivity. } + + subst e. + reflexivity. (* FIXME: do not simpl the goal here, we want to keep the Let_In common subexpressions *) + Defined. + + (*Eval simpl in (fun x1 y1 z1 t1 x2 y2 z2 t2 => proj1_sig (unifiedAddM1Rep_sig (((x1, y1), z1), t1) (((x2, y2), z2), t2))). (* TODO: remove after debugging the fixme three lines above *) *) + + Definition unifiedAddM1Rep (a b:FRep * FRep * FRep * FRep) : FRep * FRep * FRep * FRep := Eval hnf in proj1_sig (unifiedAddM1Rep_sig a b). + Definition unifiedAddM1Rep_correct a b : rep2E (unifiedAddM1Rep a b) = unifiedAddM1' (rep2E a) (rep2E b) := Eval hnf in proj2_sig (unifiedAddM1Rep_sig a b). + + Definition rep2T (P:FRep * FRep) := (rep2F (fst P), rep2F (snd P)). + Definition erep2trep (P:FRep * FRep * FRep * FRep) := Let_In P (fun P => Let_In (FRepInv (snd (fst P))) (fun iZ => (FRepMul (fst (fst (fst P))) iZ, FRepMul (snd (fst (fst P))) iZ))). + Lemma erep2trep_correct : forall P, rep2T (erep2trep P) = extendedToTwisted (rep2E P). + Proof. + unfold rep2T, rep2E, erep2trep, extendedToTwisted; destruct P as [[[]]]; simpl. + rewrite !unfoldDiv, <-!FRepMul_correct, <-FRepInv_correct. reflexivity. + Qed. + + Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. + Proof. + eexists; intros. + cbv [ed25519_verify EdDSA.verify + ed25519params curve25519params + EdDSA.E EdDSA.B EdDSA.b EdDSA.l EdDSA.H + EdDSA.PointEncoding EdDSA.FlEncoding EdDSA.FqEncoding]. + + etransitivity. + Focus 2. + { repeat match goal with + | [ |- ?x = ?x ] => reflexivity + | [ |- _ = match ?a with None => ?N | Some x => @?S x end :> ?T ] + => etransitivity; + [ + | refine (_ : option_rect (fun _ => T) _ N a = _); + let S' := match goal with |- option_rect _ ?S' _ _ = _ => S' end in + refine (option_rect (fun a' => option_rect (fun _ => T) S' N a' = match a' with None => N | Some x => S x end) + (fun x => _) _ a); intros; simpl @option_rect ]; + [ reflexivity | .. ] + end. + set_evars. + rewrite<- E.point_eqb_correct. + rewrite solve_for_R; unfold E.sub. + rewrite E.opp_mul. + let p1 := constr:(scalarMultM1_rep eq_refl) in + let p2 := constr:(unifiedAddM1_rep eq_refl) in + repeat match goal with + | |- context [(_ * E.opp ?P)%E] => + rewrite <-(unExtendedPoint_mkExtendedPoint P); + rewrite negateExtended_correct; + rewrite <-p1 + | |- context [(_ * ?P)%E] => + rewrite <-(unExtendedPoint_mkExtendedPoint P); + rewrite <-p1 + | _ => rewrite p2 + end; + rewrite ?Znat.Z_nat_N, <-?Word.wordToN_nat; + subst_evars; + reflexivity. + } Unfocus. + + etransitivity. + Focus 2. + { lazymatch goal with |- _ = option_rect _ _ ?false ?dec => + symmetry; etransitivity; [|eapply (option_rect_option_map (fun (x:F _) => Z.to_N x) _ false dec)] + end. + eapply option_rect_Proper_nd; [intro|reflexivity..]. + match goal with + | [ |- ?RHS = ?e ?v ] + => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in + unify e RHS' + end. + reflexivity. + } Unfocus. + rewrite <-decode_scalar_correct. + + etransitivity. + Focus 2. + { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + symmetry; apply decode_test_encode_test. + } Unfocus. + + rewrite enc'_correct. + cbv [unExtendedPoint unifiedAddM1 negateExtended scalarMultM1]. + (* Why does this take too long? + lazymatch goal with |- context [ proj1_sig ?x ] => + fail 5 + end. *) + unfold proj1_sig at 1 2. etransitivity. Focus 2. - { apply f_equal. - symmetry. - apply point_dec_coordinates_correct. } + { do 2 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + set_evars. + repeat match goal with + | [ |- appcontext[@proj1_sig ?A ?P (@iter_op ?T ?f ?neutral ?T' ?testbit ?exp ?base ?bound)] ] + => erewrite (@iter_op_proj T _ _ (@proj1_sig _ _)) by reflexivity + end. + subst_evars. + reflexivity. } Unfocus. - reflexivity. } - Unfocus. - - cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. - - etransitivity. - Focus 2. { - do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro. + + cbv [mkExtendedPoint E.zero]. + unfold proj1_sig at 1 2 3 5 6 7 8. + rewrite B_proj. + etransitivity. Focus 2. - { apply f_equal. - lazymatch goal with - | [ |- _ = ?term :> ?T ] - => lazymatch term with (match ?a with None => ?N | Some x => @?S x end) - => let term' := constr:((option_rect (fun _ => T) S N) a) in - replace term with term' by reflexivity - end + { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + set_evars. + lazymatch goal with |- _ = option_rect _ _ ?false ?dec => + symmetry; etransitivity; [|eapply (option_rect_option_map (@proj1_sig _ _) _ false dec)] end. - reflexivity. } Unfocus. reflexivity. } Unfocus. - - etransitivity. - Focus 2. { - do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). - do 1 (eapply option_rect_Proper_nd; [ intro; reflexivity | reflexivity | ]). - eapply option_rect_Proper_nd; [ cbv beta delta [pointwise_relation]; intro | reflexivity.. ]. - replace_let_in_with_Let_In. - reflexivity. - } Unfocus. - - etransitivity. - Focus 2. { - do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). - set_evars. - rewrite option_rect_function. (* turn the two option_rects into one *) - subst_evars. - simpl_option_rect. - do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). - (* push the [option_rect] inside until it hits a [Some] or a [None] *) - repeat match goal with - | _ => commute_option_rect_Let_In - | [ |- _ = Let_In _ _ ] - => apply Let_In_Proper_nd; [ reflexivity | cbv beta delta [pointwise_relation]; intro ] - | [ |- ?LHS = option_rect ?P ?S ?N (if ?b then ?t else ?f) ] - => transitivity (if b then option_rect P S N t else option_rect P S N f); - [ - | destruct b; reflexivity ] - | [ |- _ = if ?b then ?t else ?f ] - => apply (f_equal2 (fun x y => if b then x else y)) - | [ |- _ = false ] => reflexivity - | _ => progress simpl_option_rect - end. - reflexivity. - } Unfocus. - - cbv iota beta delta [q d a]. - rewrite wire2rep_F_correct. + eapply option_rect_Proper_nd; [intro|reflexivity..]. + match goal with + | [ |- ?RHS = ?e ?v ] + => let RHS' := (match eval pattern v in RHS with ?RHS' _ => RHS' end) in + unify e RHS' + end. + reflexivity. + } Unfocus. + + cbv [dec PointEncoding point_encoding]. + etransitivity. + Focus 2. + { do 1 (eapply option_rect_Proper_nd; [intro|reflexivity..]). + etransitivity. + Focus 2. + { apply f_equal. + symmetry. + apply point_dec_coordinates_correct. } + Unfocus. + reflexivity. } + Unfocus. + + cbv iota beta delta [point_dec_coordinates sign_bit dec FqEncoding modular_word_encoding E.solve_for_x2 sqrt_mod_q]. + + etransitivity. + Focus 2. { + do 1 (eapply option_rect_Proper_nd; [|reflexivity..]). cbv beta delta [pointwise_relation]. intro. + etransitivity. + Focus 2. + { apply f_equal. + lazymatch goal with + | [ |- _ = ?term :> ?T ] + => lazymatch term with (match ?a with None => ?N | Some x => @?S x end) + => let term' := constr:((option_rect (fun _ => T) S N) a) in + replace term with term' by reflexivity + end + end. + reflexivity. } Unfocus. reflexivity. } Unfocus. + + etransitivity. + Focus 2. { + do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). + do 1 (eapply option_rect_Proper_nd; [ intro; reflexivity | reflexivity | ]). + eapply option_rect_Proper_nd; [ cbv beta delta [pointwise_relation]; intro | reflexivity.. ]. + replace_let_in_with_Let_In. + reflexivity. + } Unfocus. + + etransitivity. + Focus 2. { + do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). + set_evars. + rewrite option_rect_function. (* turn the two option_rects into one *) + subst_evars. + simpl_option_rect. + do 1 (eapply option_rect_Proper_nd; [cbv beta delta [pointwise_relation]; intro|reflexivity..]). + (* push the [option_rect] inside until it hits a [Some] or a [None] *) + repeat match goal with + | _ => commute_option_rect_Let_In + | [ |- _ = Let_In _ _ ] + => apply Let_In_Proper_nd; [ reflexivity | cbv beta delta [pointwise_relation]; intro ] + | [ |- ?LHS = option_rect ?P ?S ?N (if ?b then ?t else ?f) ] + => transitivity (if b then option_rect P S N t else option_rect P S N f); + [ + | destruct b; reflexivity ] + | [ |- _ = if ?b then ?t else ?f ] + => apply (f_equal2 (fun x y => if b then x else y)) + | [ |- _ = false ] => reflexivity + | _ => progress simpl_option_rect + end. + reflexivity. + } Unfocus. + + cbv iota beta delta [q d a]. - etransitivity. - Focus 2. { - eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro. - rewrite <-!(option_rect_option_map rep2F). - eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro. - rewrite !F_pow_2_r. - rewrite (rep2F_F2rep 1%F). - pattern Ed25519.d at 1. rewrite (rep2F_F2rep Ed25519.d) at 1. - pattern Ed25519.a at 1. rewrite (rep2F_F2rep Ed25519.a) at 1. - rewrite !FRepMul_correct. - rewrite !FRepSub_correct. - rewrite !unfoldDiv. - rewrite !FRepInv_correct. - rewrite !FRepMul_correct. - Let_In_rep2F. - rewrite (rep2S_S2rep (Z.to_N (Ed25519.q / 8 + 1))). - eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. - etransitivity. Focus 2. eapply Let_In_Proper_nd; [|cbv beta delta [pointwise_relation]; intro;reflexivity]. { - rewrite FSRepPow_correct. - Let_In_rep2F. - etransitivity. Focus 2. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. { - set_evars. - rewrite !F_pow_2_r. - rewrite !FRepMul_correct. - rewrite if_F_eq_dec_if_F_eqb. - rewrite compare_enc. - rewrite <-!enc_rep2F_correct. - rewrite (rep2F_F2rep sqrt_minus1). - rewrite !FRepMul_correct. - rewrite (if_map rep2F). - subst_evars. + rewrite wire2FRep_correct. + + etransitivity. + Focus 2. { + eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro. + rewrite <-!(option_rect_option_map rep2F). + eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro. + rewrite !F_pow_2_r. + rewrite <-(rcFOK 1%F). + pattern Ed25519.d at 1. rewrite <-(rcFOK Ed25519.d) at 1. + pattern Ed25519.a at 1. rewrite <-(rcFOK Ed25519.a) at 1. + rewrite !FRepMul_correct. + rewrite !FRepSub_correct. + rewrite !unfoldDiv. + rewrite !FRepInv_correct. + rewrite !FRepMul_correct. + Let_In_unRep. + rewrite <-(rcSOK (Z.to_N (Ed25519.q / 8 + 1))). + eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. + etransitivity. Focus 2. eapply Let_In_Proper_nd; [|cbv beta delta [pointwise_relation]; intro;reflexivity]. { + (* TODO: + rewrite <-pow_nat_iter_op_correct. + erewrite <-iter_op_spec. *) + rewrite FSRepPow_correct. + Let_In_unRep. + etransitivity. Focus 2. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. { + set_evars. + rewrite !F_pow_2_r. + rewrite !FRepMul_correct. + rewrite if_F_eq_dec_if_F_eqb. + rewrite compare_enc. + rewrite <-!FRep2wire_correct. + rewrite <-(rcFOK sqrt_minus1). + rewrite !FRepMul_correct. + rewrite (if_map rep2F). + subst_evars. + reflexivity. } Unfocus. + match goal with |- ?e = Let_In ?xval (fun x => rep2F (@?f x)) => change (e = rep2F (Let_In xval f)) end. reflexivity. } Unfocus. - match goal with |- ?e = Let_In ?xval (fun x => rep2F (@?f x)) => change (e = rep2F (Let_In xval f)) end. - reflexivity. } Unfocus. - Let_In_rep2F. - eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. - set_evars. - rewrite !F_pow_2_r. - rewrite !FRepMul_correct. - rewrite if_F_eq_dec_if_F_eqb. - rewrite compare_enc. - rewrite <-!enc_rep2F_correct. - subst_evars. - lazymatch goal with |- _ = if ?b then ?t else ?f => apply (f_equal2 (fun x y => if b then x else y)) end; [|reflexivity]. - - set_evars. - rewrite !FRepOpp_correct. - rewrite (if_map rep2F). - lazymatch goal with - |- ?e = Let_In (rep2F ?x, rep2F ?y) (fun p => @?r p) => - change (e = Let_In (x, y) (fun p => r (rep2F (fst p), rep2F (snd p)))); cbv beta zeta - end. - subst_evars. - eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. - - set_evars; erewrite (f_equal2 (@weqb b)); subst_evars; [|reflexivity|symmetry]. Focus 2. { - unfold twistedToExtended. - rewrite F_mul_0_l. - unfold curve25519params, q. (* TODO: do we really wanna do it here? *) - rewrite (rep2F_F2rep 0%F). - rewrite (rep2F_F2rep 1%F). - match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite (rep2F_F2rep x) end end. - match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite (rep2F_F2rep x) end end. + Let_In_unRep. + eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. + set_evars. + rewrite !F_pow_2_r. rewrite !FRepMul_correct. - repeat match goal with |- appcontext [ ?E ] => - match E with (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) => - change E with (rep2E (((x, y), z), t)) - end + rewrite if_F_eq_dec_if_F_eqb. + rewrite compare_enc. + rewrite <-!FRep2wire_correct. + subst_evars. + lazymatch goal with |- _ = if ?b then ?t else ?f => apply (f_equal2 (fun x y => if b then x else y)) end; [|reflexivity]. + + set_evars. + rewrite !FRepOpp_correct. + rewrite (if_map rep2F). + lazymatch goal with + |- ?e = Let_In (rep2F ?x, rep2F ?y) (fun p => @?r p) => + change (e = Let_In (x, y) (fun p => r (rep2F (fst p), rep2F (snd p)))); cbv beta zeta end. - lazymatch goal with |- context [?X] => - lazymatch X with negateExtended' (rep2E ?E) => - replace X with (rep2E (((((FRepOpp (fst (fst (fst E)))), (snd (fst (fst E)))), (snd (fst E))), (FRepOpp (snd E))))) by (simpl; rewrite !FRepOpp_correct; reflexivity) - end end; simpl fst; simpl snd. (* we actually only want to simpl in the with clause *) - do 2 erewrite <- (fun x y z => iter_op_proj rep2E unifiedAddM1Rep unifiedAddM1' x y z N.testbit_nat) by apply unifiedAddM1Rep_correct. - rewrite <-unifiedAddM1Rep_correct. - - - etransitivity. Focus 2. { - apply f_equal. - rewrite <-erep2trep_correct; cbv beta delta [erep2trep]. + subst_evars. + eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. + + set_evars; erewrite (f_equal2 (@weqb b)); subst_evars; [|reflexivity|symmetry]. Focus 2. { + unfold twistedToExtended. + rewrite F_mul_0_l. + unfold curve25519params, q. (* TODO: do we really wanna do it here? *) + rewrite <-(rcFOK 0%F). + rewrite <-(rcFOK 1%F). + match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite <-(rcFOK x) end end. + match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite <-(rcFOK x) end end. + autorewrite with FRepOperations. (* breaks reflexivity *) + repeat match goal with |- appcontext [ ?E ] => + match E with (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) => + change E with (rep2E (((x, y), z), t)) + end + end. + lazymatch goal with |- context [?X] => + lazymatch X with negateExtended' (rep2E ?E) => + replace X with (rep2E (((((FRepOpp (fst (fst (fst E)))), (snd (fst (fst E)))), (snd (fst E))), (FRepOpp (snd E))))) by (simpl; autorewrite with FRepOperations; reflexivity) + end end; simpl fst; simpl snd. (* we actually only want to simpl in the with clause *) + do 2 erewrite <- (fun x y z => iter_op_proj rep2E unifiedAddM1Rep unifiedAddM1' x y z N.testbit_nat) by apply unifiedAddM1Rep_correct. + rewrite <-unifiedAddM1Rep_correct, <-erep2trep_correct; cbv beta delta [erep2trep]. + + (* reflexivity. } Unfocus. - + (* + cbv beta iota delta + [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd + point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q]. + *) reflexivity. } Unfocus. - (* - cbv beta iota delta - [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd - point_dec_coordinates PrimeFieldTheorems.sqrt_mod_q]. - *) - reflexivity. } Unfocus. - reflexivity. -Admitted. + reflexivity. +*) + Admitted. + +End Ed25519Frep. \ No newline at end of file diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index b01e6280e..8aaf8caf6 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -7,6 +7,7 @@ Require Import Coq.Lists.List Crypto.Util.ListUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.BaseSystem. +Require Import Crypto.Rep. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. Local Open Scope Z. @@ -81,4 +82,99 @@ Proof. intros f g Hf Hg. pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg. compute_formula. -Defined. \ No newline at end of file +Defined. + +Definition F25519Rep := (Z * Z * Z * Z * Z * Z * Z * Z * Z * Z)%type. + +Definition F25519toRep (x:F (2^255 - 19)) : F25519Rep := (0, 0, 0, 0, 0, 0, 0, 0, 0, FieldToZ x)%Z. +Definition F25519unRep (rx:F25519Rep) := + let '(x9, x8, x7, x6, x5, x4, x3, x2, x1, x0) := rx in + ModularBaseSystem.decode [x0;x1;x2;x3;x4;x5;x6;x7;x8;x9]. + +Global Instance F25519RepConversions : RepConversions (F (2^255 - 19)) F25519Rep := + { + toRep := F25519toRep; + unRep := F25519unRep + }. + +Lemma F25519RepConversionsOK : RepConversionsOK F25519RepConversions. +Proof. + unfold F25519RepConversions, RepConversionsOK, unRep, toRep, F25519toRep, F25519unRep; intros. + change (ModularBaseSystem.decode (ModularBaseSystem.encode x) = x). + eauto using ModularBaseSystemProofs.rep_decode, ModularBaseSystemProofs.encode_rep. +Qed. + +Definition F25519Rep_mul (f g:F25519Rep) : F25519Rep. + refine ( + let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in + let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _). + (* FIXME: the r should not be present in generated code *) + pose (r := proj1_sig (GF25519Base25Point5_mul_reduce_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9)). + simpl in r. + unfold F25519Rep. + repeat let t' := (eval cbv beta delta [r] in r) in + lazymatch t' with Let_In ?arg ?f => + let x := fresh "x" in + refine (let x := arg in _); + let t'' := (eval cbv beta in (f x)) in + change (Let_In arg f) with t'' in r + end. + let t' := (eval cbv beta delta [r] in r) in + lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] => + clear r; + exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0) + end. +Time Defined. + +Lemma F25519_mul_OK : RepBinOpOK F25519RepConversions ModularArithmetic.mul F25519Rep_mul. + cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_mul toRep unRep F25519toRep F25519unRep]. + destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. + destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. + let E := constr:(GF25519Base25Point5_mul_reduce_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in + transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]]; + destruct E as [? r]; cbv [proj1_sig]. + cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. +Qed. + +Definition F25519Rep_add (f g:F25519Rep) : F25519Rep. + refine ( + let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in + let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _). + let t' := (eval simpl in (proj1_sig (GF25519Base25Point5_add_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9))) in + lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] => + exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0) + end. +Defined. + +Definition F25519Rep_sub (f g:F25519Rep) : F25519Rep. + refine ( + let '(f9, f8, f7, f6, f5, f4, f3, f2, f1, f0) := f in + let '(g9, g8, g7, g6, g5, g4, g3, g2, g1, g0) := g in _). + let t' := (eval simpl in (proj1_sig (GF25519Base25Point5_sub_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9))) in + lazymatch t' with [?r0;?r1;?r2;?r3;?r4;?r5;?r6;?r7;?r8;?r9] => + exact (r9, r8, r7, r6, r5, r4, r3, r2, r1, r0) + end. +Defined. + +Lemma F25519_add_OK : RepBinOpOK F25519RepConversions ModularArithmetic.add F25519Rep_add. + cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_add toRep unRep F25519toRep F25519unRep]. + destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. + destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. + let E := constr:(GF25519Base25Point5_add_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in + transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]]; + destruct E as [? r]; cbv [proj1_sig]. + cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. +Qed. + +Lemma F25519_sub_OK : RepBinOpOK F25519RepConversions ModularArithmetic.sub F25519Rep_sub. + cbv iota beta delta [RepBinOpOK F25519RepConversions F25519Rep_sub toRep unRep F25519toRep F25519unRep]. + destruct x as [[[[[[[[[x9 x8] x7] x6] x5] x4] x3] x2] x1] x0]. + destruct y as [[[[[[[[[y9 y8] y7] y6] y5] y4] y3] y2] y1] y0]. + let E := constr:(GF25519Base25Point5_sub_formula x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 y0 y1 y2 y3 y4 y5 y6 y7 y8 y9) in + transitivity (ModularBaseSystem.decode (proj1_sig E)); [|solve[simpl;f_equal]]; + destruct E as [? r]; cbv [proj1_sig]. + cbv [rep ModularBaseSystem.rep PseudoMersenneBase modulus] in r; edestruct r; eauto. +Qed. \ No newline at end of file -- cgit v1.2.3