diff options
author | 2016-04-16 15:41:28 -0400 | |
---|---|---|
committer | 2016-06-22 13:44:44 -0400 | |
commit | 6eca78ea2c214375c668f6d7cf2a9b3197edda8b (patch) | |
tree | fb21978b68a978a0672cefc4c90da74dd8f78559 /src | |
parent | 565ff8ce7d982390aa5f2fb1a50a91e07aed5222 (diff) |
ed25519 derivation: stuck at main loop
Diffstat (limited to 'src')
-rw-r--r-- | src/Specific/Ed25519.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index baad7a184..3095e6ce5 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -450,6 +450,13 @@ Proof. 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 at 1 3 4. + 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. (* cbv beta iota delta [iter_op test_and_op unifiedAddM1' extendedToTwisted twistedToExtended enc' snd |