diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-04-17 15:50:46 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-04-17 15:50:46 -0400 |
| commit | ccd934fbd94229469a8da90b52be16545d31e191 (patch) | |
| tree | 2be2a577509310ba1689c8aa22ba3d4692d4fc04 /src | |
| parent | 48e1a0a0257853e8b20f63daff043e06015cf135 (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 |