Include ecEq in cryptol_simpset

Fixes #1347.
GaloisInc · Jun 22, 2021 · ea4ba3a · ea4ba3a
1 parent e870373
commit ea4ba3a
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 7 deletions.
diff --git 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
@@ -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 }});