Merge with public master

12 files changed, 126 insertions, 23 deletions

diff --git a/src/BaseSystem.v b/src/BaseSystem.v
index c07aad759..1985520f0 100644
--- a/src/BaseSystem.v
+++ b/src/BaseSystem.v
@@ -2,6 +2,7 @@ Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
 Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
+Require Import Crypto.Util.Notations.
 Import Nat.
 
 Local Open Scope Z.
@@ -47,7 +48,7 @@ Section BaseSystem.
       | _, nil => us
       | _, _ => vs
     end.
-  Infix ".+" := add (at level 50).
+  Infix ".+" := add.
 
   Hint Extern 1 (@eq Z _ _) => ring.
 
diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v
index 4414877b4..85835aabe 100644
--- a/src/BaseSystemProofs.v
+++ b/src/BaseSystemProofs.v
@@ -3,9 +3,10 @@ Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
 Require Import ZArith.ZArith ZArith.Zdiv.
 Require Import Omega NPeano Arith.
 Require Import Crypto.BaseSystem.
+Require Import Crypto.Util.Notations.
 Local Open Scope Z.
 
-Local Infix ".+" := add (at level 50).
+Local Infix ".+" := add.
 
 Local Hint Extern 1 (@eq Z _ _) => ring.
 
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 683addd5d..476592b36 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -7,6 +7,7 @@ Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.Classes.Morphisms.
 Require Import Relation_Definitions.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Notations.
 
 Module E.
   Import Group Ring Field CompleteEdwardsCurve.E.
@@ -18,7 +19,7 @@ Module E.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
-    Local Notation "x ^2" := (x*x) (at level 30).
+    Local Notation "x ^ 2" := (x*x).
     Local Notation point := (@point F Feq Fone Fadd Fmul a d).
     Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d).
 
@@ -158,7 +159,7 @@ Module E.
     Admitted.
 
     Section PointCompression.
-      Local Notation "x ^2" := (x*x).
+      Local Notation "x ^ 2" := (x*x).
       Definition solve_for_x2 (y : F) := ((y^2 - 1) / (d * (y^2) - a)).
 
       Lemma a_d_y2_nonzero : forall y, d * y^2 - a <> 0.
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 25af83a0a..deeb795b1 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -7,6 +7,7 @@ Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.Classes.Morphisms.
 Require Import Relation_Definitions.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Notations.
 
 Module Extended.
   Section ExtendedCoordinates.
@@ -18,7 +19,7 @@ Module Extended.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
-    Local Notation "x ^2" := (x*x) (at level 30).
+    Local Notation "x ^ 2" := (x*x).
     Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
     Local Notation onCurve := (@Pre.onCurve F Feq Fone Fadd Fmul a d).
 
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index 5314ee37c..be294fb3e 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -1,5 +1,6 @@
 Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
 Require Import Crypto.Algebra Crypto.Tactics.Nsatz.
+Require Import Crypto.Util.Notations.
 
 Generalizable All Variables.
 Section Pre.
@@ -9,7 +10,7 @@ Section Pre.
   Local Notation "0" := zero.  Local Notation "1" := one.
   Local Infix "+" := add. Local Infix "*" := mul.
   Local Infix "-" := sub. Local Infix "/" := div.
-  Local Notation "x '^' 2" := (x*x) (at level 30).
+  Local Notation "x ^ 2" := (x*x).
 
   Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)).
 
@@ -97,4 +98,4 @@ Section RespectsFieldHomomorphism.
       apply conj;
       (rewrite_strat topdown hints field_homomorphism); reflexivity.
   Qed.
-End RespectsFieldHomomorphism.
\ No newline at end of file
+End RespectsFieldHomomorphism.
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index ca8c19d18..08545bdb4 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -7,6 +7,7 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
 Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
 Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Util.Notations.
 Local Open Scope Z_scope.
 
 Section PseudoMersenneBase.
@@ -15,7 +16,7 @@ Section PseudoMersenneBase.
   Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us).
 
   Definition rep (us : digits) (x : F modulus) := (length us = length base)%nat /\ decode us = x.
-  Local Notation "u '~=' x" := (rep u x) (at level 70).
+  Local Notation "u ~= x" := (rep u x).
   Local Hint Unfold rep.
 
   Definition encode (x : F modulus) := encode x ++ BaseSystem.zeros (length base - 1)%nat.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 0462b0f37..6f82a8950 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -6,15 +6,16 @@ Require Import VerdiTactics.
 Require Crypto.BaseSystem.
 Require Import Crypto.ModularArithmetic.ModularBaseSystem Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.BaseSystemProofs Crypto.ModularArithmetic.PseudoMersenneBaseParams Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs Crypto.ModularArithmetic.ExtendedBaseVector.
+Require Import Crypto.Util.Notations.
 Local Open Scope Z_scope.
 
 Section PseudoMersenneProofs.
   Context `{prm :PseudoMersenneBaseParams}.
 
   Local Hint Unfold decode.
-  Local Notation "u '~=' x" := (rep u x) (at level 70).
-  Local Notation "u '.+' x" := (add u x) (at level 70).
-  Local Notation "u '.*' x" := (ModularBaseSystem.mul u x) (at level 70).
+  Local Notation "u ~= x" := (rep u x).
+  Local Notation "u .+ x" := (add u x).
+  Local Notation "u .* x" := (ModularBaseSystem.mul u x).
   Local Hint Unfold rep.
 
   Lemma rep_decode : forall us x, us ~= x -> decode us = x.
@@ -256,7 +257,7 @@ End PseudoMersenneProofs.
 
 Section CarryProofs.
   Context `{prm : PseudoMersenneBaseParams}.
-  Local Notation "u '~=' x" := (rep u x) (at level 70).
+  Local Notation "u ~= x" := (rep u x).
   Hint Unfold log_cap.
 
   Lemma base_length_lt_pred : (pred (length base) < length base)%nat.
@@ -2086,4 +2087,4 @@ Section CanonicalizationProofs.
     eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption.
   Qed.
 
-End CanonicalizationProofs.
\ No newline at end of file
+End CanonicalizationProofs.
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 06c3f8fdb..f6db1c14f 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -13,7 +13,7 @@ Module E.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
-    Local Notation "x ^2" := (x*x) (at level 30).
+    Local Notation "x ^ 2" := (x*x) (at level 30).
 
     Context {a d: F}.
     Class twisted_edwards_params :=
@@ -50,4 +50,4 @@ End E.
 
 Delimit Scope E_scope with E.
 Infix "+" := E.add : E_scope.
-Infix "*" := E.mul : E_scope.
\ No newline at end of file
+Infix "*" := E.mul : E_scope.
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 1e3e36ff9..c28ff0482 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -4,9 +4,21 @@ Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
 Require Coq.Numbers.Natural.Peano.NPeano.
 Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 
-Local Infix "^" := Nat.pow.
-Local Infix "mod" := Nat.modulo (at level 40, no associativity).
-Local Infix "++" := Word.combine.
+(** In Coq 8.4, we have [NPeano.pow] and [NPeano.modulo].  In Coq 8.5,
+    they are [Nat.pow] and [Nat.modulo].  To allow this file to work
+    with both versions, we create a module where we (locally) import
+    both [NPeano] and [Nat], and define the notations with unqualified
+    names.  By importing the module, we get access to the notations
+    without importing [NPeano] and [Nat] in the top-level of this
+    file. *)
+
+Module Import Notations.
+  Import NPeano Nat.
+  
+  Infix "^" := pow.
+  Infix "mod" := modulo (at level 40, no associativity).
+  Infix "++" := Word.combine.
+End Notations.
 
 Generalizable All Variables.
 Section EdDSA.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 471c1d548..6d7e2c38c 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -9,6 +9,7 @@ Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.BaseSystem.
 Import ListNotations.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Require Import Crypto.Util.Notations.
 Local Open Scope Z.
 
 (* BEGIN PseudoMersenneBaseParams instance construction. *)
@@ -60,8 +61,8 @@ Proof.
 
 (* Uncomment this to see a pretty-printed mulmod
 Local Transparent Let_In.
-Infix "<<" := Z.shiftr (at level 50).
-Infix "&" := Z.land (at level 50).
+Infix "<<" := Z.shiftr.
+Infix "&" := Z.land.
 Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_mul_reduce_formula Let_In] in
   fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9
     g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 => proj1_sig (
@@ -122,9 +123,9 @@ Defined.
 (*
 Set Printing Depth 1000.
 Local Transparent Let_In.
-Infix "<<" := Z.shiftr (at level 50).
-Infix "&" := Z.land (at level 50).
+Infix "<<" := Z.shiftr.
+Infix "&" := Z.land.
 Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_freeze_formula Let_In] in
   fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 => proj1_sig (
     GF25519Base25Point5_freeze_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9).
-*)
\ No newline at end of file
+*)
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
new file mode 100644
index 000000000..726b52b6b
--- /dev/null
+++ b/src/Util/Decidable.v
@@ -0,0 +1,61 @@
+(** Typeclass for decidable propositions *)
+
+Require Import Coq.Logic.Eqdep_dec.
+
+Local Open Scope type_scope.
+
+Class Decidable (P : Prop) := dec : {P} + {~P}.
+
+Notation DecidableRel R := (forall x y, Decidable (R x y)).
+
+Ltac destruct_decidable_step :=
+  match goal with
+  | [ H : Decidable _ |- _ ] => destruct H
+  end.
+Ltac destruct_decidable := repeat destruct_decidable_step.
+
+Local Ltac pre_decide :=
+  repeat (intros
+          || destruct_decidable
+          || subst
+          || split
+          || unfold Decidable in *
+          || hnf ).
+
+Local Ltac solve_decidable_transparent_with tac :=
+  pre_decide;
+  try solve [ left; abstract tac
+            | right; abstract tac
+            | decide equality; eauto with nocore ].
+
+Local Ltac solve_decidable_transparent := solve_decidable_transparent_with firstorder.
+
+Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances.
+
+Global Instance dec_True : Decidable True := left I.
+Global Instance dec_False : Decidable False := right (fun x => x).
+Global Instance dec_or {A B} `{Decidable A, Decidable B} : Decidable (A \/ B). exact _. Defined.
+Global Instance dec_and {A B} `{Decidable A, Decidable B} : Decidable (A /\ B). exact _. Defined.
+Global Instance dec_impl {A B} `{Decidable (B \/ ~A)} : Decidable (A -> B) | 3. exact _. Defined.
+Global Instance dec_impl_simple {A B} `{Decidable A, Decidable B} : Decidable (A -> B). exact _. Defined.
+Global Instance dec_iff {A B} `{Decidable A, Decidable B} : Decidable (A <-> B). exact _. Defined.
+Lemma dec_not {A} `{Decidable A} : Decidable (~A).
+Proof. solve_decidable_transparent. Defined.
+(** Disallow infinite loops of dec_not *)
+Hint Extern 0 (Decidable (~?A)) => apply (@dec_not A) : typeclass_instances.
+
+Global Instance dec_eq_unit : DecidableRel (@eq unit). exact _. Defined.
+Global Instance dec_eq_bool : DecidableRel (@eq bool). exact _. Defined.
+Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set). exact _. Defined.
+Global Instance dec_eq_nat : DecidableRel (@eq nat). exact _. Defined.
+Global Instance dec_eq_prod {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A * B)). exact _. Defined.
+Global Instance dec_eq_sum {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A + B)). exact _. Defined.
+
+Lemma Decidable_respects_iff A B (H : A <-> B) : (Decidable A -> Decidable B) * (Decidable B -> Decidable A).
+Proof. solve_decidable_transparent. Defined.
+
+Lemma Decidable_iff_to_impl A B (H : A <-> B) : Decidable A -> Decidable B.
+Proof. solve_decidable_transparent. Defined.
+
+Lemma Decidable_iff_to_flip_impl A B (H : A <-> B) : Decidable B -> Decidable A.
+Proof. solve_decidable_transparent. Defined.
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
new file mode 100644
index 000000000..bbeb50092
--- /dev/null
+++ b/src/Util/Notations.v
@@ -0,0 +1,22 @@
+(** * Reserved Notations *)
+
+(** Putting them all together in one file prevents conflicts.  Coq's
+    parser (camlpX) is really bad at conflicting notation levels and
+    is sometimes really bad at backtracking, too.  Not having level
+    declarations in other files makes it harder for us to confuse
+    Coq's parser. *)
+
+Reserved Infix "=?" (at level 70, no associativity).
+Reserved Infix "?=" (at level 70, no associativity).
+Reserved Infix "?<" (at level 70, no associativity).
+Reserved Infix ".+" (at level 50).
+Reserved Infix ".*" (at level 50).
+Reserved Notation "x ^ 2" (at level 30, format "x ^ 2").
+Reserved Notation "x ^ 3" (at level 30, format "x ^ 3").
+Reserved Infix "mod" (at level 40, no associativity).
+Reserved Notation "'canonical' 'encoding' 'of' T 'as' B" (at level 50).
+Reserved Infix "<<" (at level 50).
+Reserved Infix "&" (at level 50).
+Reserved Infix "<<" (at level 50).
+Reserved Infix "&" (at level 50).
+Reserved Infix "~=" (at level 70).