diff options
author | 2016-04-16 16:36:26 -0400 | |
---|---|---|
committer | 2016-06-22 13:44:44 -0400 | |
commit | 9afb046f7ddfe6a70cd70358eab8640d42872b80 (patch) | |
tree | 8f67ef1e5a81c7240b18b26e764d812d248d21bc /src | |
parent | 6eca78ea2c214375c668f6d7cf2a9b3197edda8b (diff) |
ed25519 derivation: wrangle non-unique representations
Diffstat (limited to 'src')
-rw-r--r-- | src/Specific/Ed25519.v | 22 |
1 files changed, 18 insertions, 4 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 3095e6ce5..fc86cb745 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -60,8 +60,9 @@ Qed. Axiom point_eqb : forall {prm : TwistedEdwardsParams}, point -> point -> bool. Axiom point_eqb_correct : forall P Q, point_eqb P Q = if point_eq_dec P Q then true else false. -Axiom Bc : F q * F q. -Axiom B_proj : proj1_sig B = Bc. +Axiom xB : F q. +Axiom yB : F q. +Axiom B_proj : proj1_sig B = (xB, yB). Require Import Coq.Setoids.Setoid. Require Import Coq.Classes.Morphisms. @@ -451,12 +452,25 @@ Proof. 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 at 1 3 4. + unfold twistedToExtended. rewrite F_mul_0_l. unfold curve25519params, q. (* TODO: do we really wanna do it here? *) rewrite (rep2F_F2rep 0%F). rewrite (rep2F_F2rep 1%F). - rewrite FRepMul_correct. + rewrite (rep2F_F2rep xB%F). + rewrite (rep2F_F2rep yB%F). + rewrite !FRepMul_correct. + Definition rep2E (r:FRep * FRep * FRep * FRep) : extended := + match r with (((x, y), z), t) => mkExtended (rep2F x) (rep2F y) (rep2F z) (rep2F t) end. + 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. + erewrite <- (fun op x y z => iter_op_proj rep2E op unifiedAddM1' x y z N.testbit_nat). + erewrite <- (fun op x y z => iter_op_proj rep2E op unifiedAddM1' x y z N.testbit_nat). + 2:exfalso; admit. + 2:exfalso; admit. (* cbv beta iota delta [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd |