From b06d11d9e12cae00475e8f9a5f69d42cf34ae729 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 11 Feb 2019 16:34:03 -0800 Subject: Add Option.{lift,map,combine}, List.Option.lift These will be useful for extending the AST with `option` types. --- src/Primitives/EdDSARepChange.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Primitives') 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. -- cgit v1.2.3