From 8926b3e0039b2d9e175b7ace36d496dd94228256 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 25 Jun 2016 16:16:43 -0400 Subject: Fix for Coq 8.4 --- src/Experiments/EdDSARefinement.v | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'src/Experiments') diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v index e3a1a6ad2..7f2f3f8f3 100644 --- a/src/Experiments/EdDSARefinement.v +++ b/src/Experiments/EdDSARefinement.v @@ -2,6 +2,11 @@ Require Import Crypto.Spec.EdDSA Bedrock.Word. Require Import Coq.Classes.Morphisms. Require Import Util.Decidable Util.Option Util.Tactics. +Module Import NotationsFor8485. + Import NPeano Nat. + Notation modulo := modulo. +End NotationsFor8485. + Section EdDSA. Context `{prm:EdDSA}. Context {eq_dec:DecidableRel Eeq}. @@ -29,17 +34,17 @@ Section EdDSA. intros; split; intro Heq; rewrite Heq; clear Heq. Admitted. - + Definition verify {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool := option_rect (fun _ => bool) (fun S : nat => option_rect (fun _ => bool) (fun A : E => weqb (split1 b b sig) - (Eenc (S * B - PeanoNat.Nat.modulo (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ pk ++ message))) l * A)) + (Eenc (S * B - modulo (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ pk ++ message))) l * A)) ) false (decE pk) ) false (decS (split2 b b sig)) . - + Lemma verify_correct mlen (message:word mlen) (pk:word b) (sig:word (b+b)) : verify message pk sig = true <-> valid message pk sig. Proof. @@ -75,7 +80,7 @@ Section EdDSA. } Qed. - Lemma scalarMult_mod_order : forall l x B, l * B == Ezero -> (Nat.modulo x l) * B == x * B. Admitted. + Lemma scalarMult_mod_order : forall l x B, l * B == Ezero -> (modulo x l) * B == x * B. Admitted. Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M). Proof. @@ -83,9 +88,9 @@ Section EdDSA. intros. subst. constructor. Local Arguments H {_} _. Local Notation "'$' x" := (wordToNat x) (at level 1). - Local Infix "mod" := Nat.modulo (at level 50). + Local Infix "mod" := modulo (at level 50). set (HRAM := H (Eenc ($ (H (prngKey sk ++ M)) * B) ++ Eenc (curveKey sk * B) ++ M)). set (r := H (prngKey sk ++ M)). repeat rewrite scalarMult_mod_order by eapply EdDSA_l_order_B. Admitted. -End EdDSA. \ No newline at end of file +End EdDSA. -- cgit v1.2.3