Translate Cryptol (==) using the class dictionary, avoiding `Prelude.…

…eq`.

NOTE: The cryptol simpset avoids unfolding the definition of `ecEq`,
to make it easier to recognize equational theorems as such.
The axiom `ecEq_refl` can be used to rewrite goals involving `ecEq`.

saw/Cryptol.sawcore

@@ -970,7 +970,7 @@ ecSLt : (a : sort 0) -> PSignedCmp a -> a -> a -> Bool;
 ecSLt a pa x y = pa.scmp x y False;
 
 ecEq : (a : sort 0) -> PCmp a -> a -> a -> Bool;
-ecEq a _ = eq a;
+ecEq a pa = pa.eq;
 
 ecNotEq : (a : sort 0) -> PCmp a -> a -> a -> Bool;
 ecNotEq a pa x y = not (ecEq a pa x y);
@@ -1363,6 +1363,8 @@ ecSle =
 --------------------------------------------------------------------------------
 -- Rewrite rules
 
+axiom ecEq_refl : (a : sort 0) -> (pa : PCmp a) -> (x : a) -> Eq Bool (ecEq a pa x x) True;
+
 axiom replicate_False : (n : Nat) -> Eq (bitvector n) (replicate n Bool False) (bvNat n 0);
 
 axiom subNat_0 : (n : Nat) -> Eq Nat (subNat n 0) n;

src/Verifier/SAW/Cryptol/Simpset.hs

@@ -47,4 +47,5 @@ excludedNames =
   , "PLiteral"
   , "PLogic"
   , "PSignedCmp"
+  , "ecEq"
   ]