Remove the eq saw-core primitive and the related rewriteEqs

operation.  This requires some minor fixups to the ECDSA proof.

examples/ecdsa/ecdsa.saw

@@ -301,11 +301,8 @@ let ss1 = add_prelude_eqs
   , "ite_bit"
   , "ite_bit_false_1"
   , "ite_bit_true_1"
-  , "ite_eq_cong_1"
-  , "ite_eq_cong_2"
   , "ite_split_cong"
   , "ite_join_cong"
-  , "eq_refl"
   , "at_single"
   , "and_True1", "and_True2", "and_False1", "and_False2", "and_idem"
   , "or_True1", "or_True2", "or_False1", "or_False2"
@@ -349,7 +346,11 @@ ite24 <- prove_rule {{
   else [y0,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16,y17,y18,y19,y20,y21,y22,y23])
   }};
 
-at12 <- prove_core abc "(x : Vec 12 (Vec 32 Bool)) -> EqTrue (eq (Vec 12 (Vec 32 Bool)) [at 12 (Vec 32 Bool) x 0, at 12 (Vec 32 Bool) x 1, at 12 (Vec 32 Bool) x 2, at 12 (Vec 32 Bool) x 3, at 12 (Vec 32 Bool) x 4, at 12 (Vec 32 Bool) x 5, at 12 (Vec 32 Bool) x 6, at 12 (Vec 32 Bool) x 7, at 12 (Vec 32 Bool) x 8, at 12 (Vec 32 Bool) x 9, at 12 (Vec 32 Bool) x 10, at 12 (Vec 32 Bool) x 11] x)";
+at12 <- prove_rule {{
+  \(x:[12][32]) ->
+  [ x @ 0x00, x @ 0x01, x @ 0x02, x @ 0x03, x @ 0x04, x @ 0x05
+  , x @ 0x06, x @ 0x07, x @ 0x08, x @ 0x09, x @ 0x0a, x @ 0x0b
+  ] == x }};
 
 at24 <- prove_rule {{
   \(x:[24][32]) ->

s2nTests/docker/blst.dockerfile

@@ -5,7 +5,7 @@ RUN pip3 install wllvm
 
 RUN git clone https://github.com/GaloisInc/blst-verification.git /workdir && \
     cd /workdir && \
-    git checkout c2c9c8bc07c50eec29250a4b8d03b17b9a3c1f3b && \
+    git checkout 05d29b0e9d826053185e5bdba287045aab0b4669 && \
     git config --file=.gitmodules submodule.blst.url https://github.com/supranational/blst && \
     git submodule sync && \
     git submodule update --init

s2nTests/docker/s2n.dockerfile

@@ -19,7 +19,9 @@ RUN mkdir -p /saw-script && \
     git clone https://github.com/GaloisInc/s2n.git && \
     mkdir -p s2n/test-deps/saw/bin && \
     cd s2n && \
-    git checkout 90b8913a01c6421444d19aaab798d413872cf6f0
+    git checkout 6586f1ad3b35efcd2287ab98a4be124449dcb780
+
+
 
 COPY scripts/s2n-entrypoint.sh /entrypoint.sh
 ENTRYPOINT [ "/entrypoint.sh" ]

src/SAWScript/Builtins.hs

@@ -128,7 +128,6 @@ import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork)
 
 import SAWScript.Prover.Util(checkBooleanSchema,liftCexBB)
 import SAWScript.Prover.SolverStats
-import SAWScript.Prover.Rewrite(rewriteEqs)
 import qualified SAWScript.Prover.SBV as Prover
 import qualified SAWScript.Prover.RME as Prover
 import qualified SAWScript.Prover.ABC as Prover
@@ -687,8 +686,7 @@ satExternal doCNF execName args = withFirstGoal $ \g -> do
   sc <- SV.getSharedContext
   SV.AIGProxy proxy <- SV.getProxy
   io $ do
-  t0 <- propToPredicate sc (goalProp g)
-  t <- rewriteEqs sc t0
+  t <- propToPredicate sc (goalProp g)
   let cnfName = goalType g ++ show (goalNum g) ++ ".cnf"
   (path, fh) <- openTempFile "." cnfName
   hClose fh -- Yuck. TODO: allow writeCNF et al. to work on handles.

src/SAWScript/Prover/ABC.hs

@@ -9,7 +9,6 @@ import qualified Verifier.SAW.Simulator.BitBlast as BBSim
 
 import SAWScript.Proof(Prop, propToPredicate)
 import SAWScript.Prover.SolverStats (SolverStats, solverStats)
-import SAWScript.Prover.Rewrite(rewriteEqs)
 import SAWScript.Prover.Util
          (liftCexBB, bindAllExts)
 
@@ -22,7 +21,7 @@ proveABC ::
   IO (Maybe [(String, FirstOrderValue)], SolverStats)
 proveABC proxy sc goal =
   do t0 <- propToPredicate sc goal
-     t <- bindAllExts sc t0 >>= rewriteEqs sc
+     t <- bindAllExts sc t0
      BBSim.withBitBlastedPred proxy sc mempty t $
       \be lit0 shapes ->
          do let lit = AIG.not lit0

src/SAWScript/Prover/Exporter.hs

@@ -71,7 +71,6 @@ import qualified Verifier.SAW.UntypedAST as Un
 import SAWScript.Crucible.Common
 import SAWScript.Proof (Prop(..), predicateToProp, Quantification(..), propToPredicate)
 import SAWScript.Prover.SolverStats
-import SAWScript.Prover.Rewrite
 import SAWScript.Prover.Util
 import SAWScript.Prover.What4
 import SAWScript.Prover.SBV (prepNegatedSBV)
@@ -110,7 +109,6 @@ adaptExporter exporter sc path (Prop goal) =
      t <- io $ scLambdaList sc args p'
      exporter sc path t
 
-
 --------------------------------------------------------------------------------
 
 -- | Write a @Term@ representing a theorem or an arbitrary
@@ -381,12 +379,11 @@ writeCoqCryptolPrimitivesForSAWCore outputFile notations skips = do
 -- | Tranlsate a SAWCore term into an AIG
 bitblastPrim :: (AIG.IsAIG l g) => AIG.Proxy l g -> SharedContext -> Term -> IO (AIG.Network l g)
 bitblastPrim proxy sc t = do
-  t' <- rewriteEqs sc t
 {-
   let s = ttSchema t'
   case s of
     C.Forall [] [] _ -> return ()
     _ -> fail $ "Attempting to bitblast a term with a polymorphic type: " ++ pretty s
 -}
-  BBSim.withBitBlastedTerm proxy sc mempty t' $ \be ls -> do
+  BBSim.withBitBlastedTerm proxy sc mempty t $ \be ls -> do
     return (AIG.Network be (toList ls))

src/SAWScript/Prover/RME.hs

@@ -12,7 +12,6 @@ import qualified Verifier.SAW.Simulator.RME as RME
 import Verifier.SAW.Recognizer(asPiList)
 
 import SAWScript.Proof(Prop, propToPredicate)
-import SAWScript.Prover.Rewrite(rewriteEqs)
 import SAWScript.Prover.SolverStats
 import SAWScript.Prover.Util
 
@@ -23,7 +22,7 @@ proveRME ::
   IO (Maybe [(String, FirstOrderValue)], SolverStats)
 proveRME sc goal =
   do t0 <- propToPredicate sc goal
-     t <- bindAllExts sc t0 >>= rewriteEqs sc
+     t <- bindAllExts sc t0
      tp <- scWhnf sc =<< scTypeOf sc t
      let (args, _) = asPiList tp
          argNames = map (Text.unpack . fst) args

src/SAWScript/Prover/Rewrite.hs

@@ -9,23 +9,12 @@ module SAWScript.Prover.Rewrite where
 
 import Verifier.SAW.Rewriter
          ( Simpset, emptySimpset, addRules, RewriteRule
-         , rewriteSharedTerm
          , scEqsRewriteRules, scDefRewriteRules
          , addConvs
          )
 import Verifier.SAW.Term.Functor(preludeName, mkIdent, Ident, mkModuleName)
 import Verifier.SAW.Conversion
-import Verifier.SAW.SharedTerm(Term,SharedContext,scFindDef)
-
-rewriteEqs :: SharedContext -> Term -> IO Term
-rewriteEqs sc t =
-  do let eqs = map (mkIdent preludeName)
-                [ "eq_Bool", "eq_Nat", "eq_bitvector", "eq_VecBool"
-                , "eq_VecVec" ]
-     rs <- scEqsRewriteRules sc eqs
-     ss <- addRules rs <$> basic_ss sc
-     t' <- rewriteSharedTerm sc ss t
-     return t'
+import Verifier.SAW.SharedTerm(SharedContext,scFindDef)
 
 basic_ss :: SharedContext -> IO Simpset
 basic_ss sc =
@@ -65,7 +54,6 @@ basic_ss sc =
          , "and_triv1"
          , "or_triv2"
          , "and_triv2"
-         , "eq_refl"
          , "bvAddZeroL"
          , "bvAddZeroR"
          , "bveq_sameL"

src/SAWScript/Prover/SBV.hs

@@ -26,7 +26,6 @@ import Verifier.SAW.Recognizer(asPi, asPiList)
 
 import SAWScript.Proof(Prop, propToPredicate)
 import SAWScript.Prover.SolverStats
-import SAWScript.Prover.Rewrite(rewriteEqs)
 
 
 -- | Bit-blast a proposition and check its validity using SBV.
@@ -92,7 +91,7 @@ prepNegatedSBV sc unintSet goal =
      let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e))
      exts <- filterM nonFun (getAllExts t0)
 
-     t' <- scAbstractExts sc exts t0 >>= rewriteEqs sc
+     t' <- scAbstractExts sc exts t0
 
      (labels, lit) <- SBVSim.sbvSolve sc mempty unintSet t'
      let lit' = liftM SBV.svNot lit

src/SAWScript/Prover/What4.hs

@@ -18,7 +18,6 @@ import Verifier.SAW.FiniteValue
 import Verifier.SAW.Recognizer(asPi)
 
 import           SAWScript.Proof(Prop, propToPredicate)
-import           SAWScript.Prover.Rewrite(rewriteEqs)
 import           SAWScript.Prover.SolverStats
 
 import Data.Parameterized.Nonce
@@ -179,7 +178,7 @@ prepWhat4 sym sc unintSet t0 = do
   let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e))
   exts <- filterM nonFun (getAllExts t0)
 
-  t' <- scAbstractExts sc exts t0 >>= rewriteEqs sc
+  t' <- scAbstractExts sc exts t0
 
   (argNames, lit) <- W.w4Solve sym sc mempty unintSet t'
   return (t', argNames, lit)