diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-10-29 17:54:42 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-10-29 17:54:42 -0400 |
| commit | b34da8a551b3c8aa2086155ff523030126b19f2e (patch) | |
| tree | 765185361d823b85cce3ee7b2ace0fc36844fe7d /src/Experiments | |
| parent | a0bf587c8223ae237a475bb523784502a7a7dd68 (diff) | |
prove Proper_SRepERepMul
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 090644756..3c2c0baf8 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -661,7 +661,17 @@ Qed. Let SRepEnc : SRep -> Word.word b := (fun x => Word.NToWord _ (Z.to_N x)). -Axiom Proper_SRepERepMul : Proper (SC25519.SRepEq ==> ExtendedCoordinates.Extended.eq (field:=GF25519Bounded.field25519) ==> ExtendedCoordinates.Extended.eq (field:=GF25519Bounded.field25519)) SRepERepMul. +Local Instance Proper_SRepERepMul : Proper (SC25519.SRepEq ==> ExtendedCoordinates.Extended.eq (field:=GF25519Bounded.field25519) ==> ExtendedCoordinates.Extended.eq (field:=GF25519Bounded.field25519)) SRepERepMul. + unfold SRepERepMul, SC25519.SRepEq. + repeat intro. + eapply IterAssocOp.Proper_iter_op. + { eapply ExtendedCoordinates.Extended.Proper_add. } + { reflexivity. } + { repeat intro; subst; reflexivity. } + { unfold ERepSel; repeat intro; break_match; solve [ discriminate | eauto ]. } + { reflexivity. } + { assumption. } +Qed. Lemma SRepEnc_correct : forall x : ModularArithmetic.F.F l, Senc x = SRepEnc (S2Rep x). unfold SRepEnc, Senc, Fencode; intros; f_equal. |