diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-04-16 15:41:28 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-04-16 15:41:28 -0400 |
| commit | 31577de175b0aaae3ec1f4d3e88a91cfffc5376e (patch) | |
| tree | e104016c2b9ff397d21882fdf19d6b8ff5bb84b7 /src | |
| parent | 4ca19f34d4feaa4fc3ba56a7b57048cc0d94f459 (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 |