From ea4ba3a661e517a89e27fc5034e1a16734a876a9 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Sat, 19 Jun 2021 18:55:53 -0400
Subject: [PATCH] Include ecEq in cryptol_simpset

Fixes #1347.
---
 cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs |  1 -
 examples/aes/aes.saw                                 | 10 ++++------
 2 files changed, 4 insertions(+), 7 deletions(-)

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs
index 0a7e3578de..97c4c07e72 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol/Simpset.hs
@@ -50,5 +50,4 @@ excludedNames =
   , "PEq"
   , "PCmp"
   , "PSignedCmp"
-  , "ecEq"
   ]
diff --git a/examples/aes/aes.saw b/examples/aes/aes.saw
index 2c4d01c835..45800f2de4 100644
--- a/examples/aes/aes.saw
+++ b/examples/aes/aes.saw
@@ -69,15 +69,14 @@ dec_enc <-
                         decrypt_lemma]
               (cryptol_ss()));
     unfolding ["AESRound", "AESInvRound", "AESFinalRound", "AESFinalInvRound"];
-    simplify (add_cryptol_defs ["ecEq"]
-             (add_prelude_eqs ["bvEq_refl"]
+    simplify (add_prelude_eqs ["bvEq_refl"]
              (addsimps [msgToState_stateToMsg,
                         AddRoundKey_cancel,
                         InvShiftRows_ShiftRows,
                         InvSubBytes_SubBytes,
                         InvMixColumns_MixColumns,
                         stateToMsg_msgToState]
-              (cryptol_ss()))));
+              (cryptol_ss())));
     trivial;
   }
   {{ \msg key -> aesDecrypt (aesEncrypt (msg, key), key) == msg }});
@@ -116,15 +115,14 @@ enc_dec <-
                         decrypt_lemma]
               (cryptol_ss()));
     unfolding ["AESRound", "AESInvRound", "AESFinalRound", "AESFinalInvRound"];
-    simplify (add_cryptol_defs ["ecEq"]
-             (add_prelude_eqs ["bvEq_refl"]
+    simplify (add_prelude_eqs ["bvEq_refl"]
              (addsimps [msgToState_stateToMsg,
                         AddRoundKey_cancel,
                         ShiftRows_InvShiftRows,
                         SubBytes_InvSubBytes,
                         MixColumns_InvMixColumns,
                         stateToMsg_msgToState]
-              (cryptol_ss()))));
+              (cryptol_ss())));
     trivial;
   }
   {{ \msg key -> aesEncrypt (aesDecrypt (msg, key), key) == msg }});