diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-04-17 15:50:46 -0400 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:44:45 -0400 |
| commit | d000eb14f2859e036ea458158ccacf6ef529677e (patch) | |
| tree | 13680cd1f9caf5b6de93d3eb39ff120ec22c8491 /src | |
| parent | ce88dd18c6a6ef6968e165e054930cf6112c14df (diff) | |
ed25519 derivation: down to final encoding
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/Ed25519.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index a1d77705a..50379b8d1 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -498,7 +498,18 @@ Proof. rewrite <-unifiedAddM1Rep_correct. - (* cbv iota beta delta [extendedToTwisted rep2E]. *) + etransitivity. Focus 2. { + apply f_equal. + 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. + rewrite <-erep2trep_correct; cbv beta delta [erep2trep]. + reflexivity. } Unfocus. + reflexivity. } Unfocus. (* cbv beta iota delta |