diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-02-11 16:34:03 -0800 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-02-11 22:22:46 -0800 |
| commit | b06d11d9e12cae00475e8f9a5f69d42cf34ae729 (patch) | |
| tree | 6f13a3f3c6ccaef28fe6884a677719abe3577ca2 /src/Primitives | |
| parent | 974bb6d7ac3a7f007dd3b8655693f38a54154c2a (diff) | |
Add Option.{lift,map,combine}, List.Option.lift
These will be useful for extending the AST with `option` types.
Diffstat (limited to 'src/Primitives')
| -rw-r--r-- | src/Primitives/EdDSARepChange.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Primitives/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v index d867a62df..b7f4acd9b 100644 --- a/src/Primitives/EdDSARepChange.v +++ b/src/Primitives/EdDSARepChange.v @@ -56,7 +56,7 @@ Section EdDSA. Context {Edec:word b-> option E} {eq_enc_E_iff: forall P_ P, Eenc P = P_ <-> option_eq Eeq (Edec P_) (Some P)}. Context {Sdec:word b-> option (F l)} {eq_enc_S_iff: forall n_ n, Senc n = n_ <-> Sdec n_ = Some n}. - Local Infix "++" := combine. + Local Infix "++" := Word.combine. Definition verify'_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)), verify mlen message pk sig = true <-> valid message pk sig }. Proof. @@ -231,7 +231,7 @@ Section EdDSA. dlet r := SRepDecModL (H _ (p ++ msg)) in dlet R := SRepERepMul r ErepB in dlet S := SRepAdd r (SRepMul (SRepDecModL (H _ (ERepEnc R ++ pk ++ msg))) s) in - ERepEnc R ++ SRepEnc S. + ERepEnc R ++ SRepEnc S. Lemma Z_l_nonzero : Z.pos l <> 0%Z. discriminate. Qed. |