Add heterogenous equality to Mr. Solver for SHA512 example (#1670)

* instantiate evars in mrProvable

* fix typo in `ecShiftRM`

* reorganize recognizers in MRSolver, add asNatType to Recognizer.hs

* add fromBVVecUpdateM and mrBvConst, fix atM nat case of normComp

* mark s0,s1 as unused in the args to round_16_80, add rw arg to int64_ptr

* add heterogenous equality on return types in MRSolver

cryptol-saw-core/saw/CryptolM.sawcore

@@ -172,6 +172,17 @@ bvVecUpdateM n len a xs i x =
                                            (updBVVec n len a xs i x))
         (bvultWithProof n i len);
 
+fromBVVecUpdateM : (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) ->
+                   BVVec n len a -> Vec n Bool -> a ->
+                   a -> (m : Nat) -> CompM (Vec m a);
+fromBVVecUpdateM n len a xs i x def m =
+  maybe (is_bvult n i len) (CompM (Vec m a))
+        (errorM (Vec m a) "bvVecUpdateM: invalid sequence index")
+        (\ (_:is_bvult n i len) -> returnM (Vec m a)
+                                           (genFromBVVec n len a
+                                             (updBVVec n len a xs i x) def m))
+        (bvultWithProof n i len);
+
 updateM : (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> a -> CompM (Vec n a);
 updateM n a xs i x =
   maybe (IsLtNat i n) (CompM (Vec n a))
@@ -340,7 +351,7 @@ ecShiftRM : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a ->
 ecShiftRM =
   Num_rec (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a ->
                         mseq m a -> ix -> mseq m a)
-          (\ (m:Nat) -> ecShiftL (TCNum m))
+          (\ (m:Nat) -> ecShiftR (TCNum m))
           (\ (ix a : sort 0) (pix:PIntegral ix) (pa:PZero a) ->
              ecShiftR TCInf ix (CompM a) pix (PZeroCompM a pa));
 

heapster-saw/examples/sha512.cry

@@ -73,14 +73,13 @@ round_00_15_spec i a b c d e f g h T1 =
 
 round_16_80_spec : [w] -> [w] ->
                    [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] -> [w] ->
-                   [16][w] ->
-                   [w] -> [w] -> [w] ->
+                   [16][w] -> [w] ->
                    ([w], [w], [w], [w], [w], [w], [w], [w], [16][w], [w], [w], [w])
-round_16_80_spec i j a b c d e f g h X s0 s1 T1 =
+round_16_80_spec i j a b c d e f g h X T1 =
   (a', b', c', d', e', f', g', h', X', s0', s1', T1'')
   where s0' = sigma_0 (X @ ((j + 1) && 15))
-        s1' = sigma_1 (X @ ((j +  4) && 15))
-        T1' = X @ (j && 15) + s0' + s1' + X @ ((j + 9) && 15)
+        s1' = sigma_1 (X @ ((j + 14) && 15))
+        T1' = (X @ (j && 15)) + s0' + s1' + (X @ ((j + 9) && 15))
         X' = update X (j && 15) T1'
         (a', b', c', d', e', f', g', h', T1'') =
           round_00_15_spec (i + j) a b c d e f g h T1'

heapster-saw/examples/sha512_mr_solver.saw

@@ -7,7 +7,10 @@ heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x)
 heapster_define_perm env "int32" " " "llvmptr 32" "exists x:bv 32.eq(llvmword(x))";
 heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
 
-heapster_define_perm env "int64_ptr" " " "llvmptr 64" "ptr((W,0) |-> int64<>)";
+// FIXME: We always have rw=W, but without the rw arguments below Heapster
+// doesn't realize the perm is not copyable (it needs to unfold named perms).
+heapster_define_perm env "int64_ptr" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> int64<>)";
+heapster_define_perm env "true_ptr" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> true)";
 
 heapster_assume_fun env "CRYPTO_load_u64_be"
   "(). arg0:ptr((R,0) |-> int64<>) -o \
@@ -16,37 +19,37 @@ heapster_assume_fun env "CRYPTO_load_u64_be"
 
 heapster_typecheck_fun env "round_00_15"
  "(). arg0:int64<>, \
-    \ arg1:int64_ptr<>, arg2:int64_ptr<>, arg3:int64_ptr<>, arg4:int64_ptr<>, \
-    \ arg5:int64_ptr<>, arg6:int64_ptr<>, arg7:int64_ptr<>, arg8:int64_ptr<>, \
-    \ arg9:int64_ptr<> -o \
-    \ arg1:int64_ptr<>, arg2:int64_ptr<>, arg3:int64_ptr<>, arg4:int64_ptr<>, \
-    \ arg5:int64_ptr<>, arg6:int64_ptr<>, arg7:int64_ptr<>, arg8:int64_ptr<>, \
-    \ arg9:int64_ptr<>, ret:true";
+    \ arg1:int64_ptr<W>, arg2:int64_ptr<W>, arg3:int64_ptr<W>, arg4:int64_ptr<W>, \
+    \ arg5:int64_ptr<W>, arg6:int64_ptr<W>, arg7:int64_ptr<W>, arg8:int64_ptr<W>, \
+    \ arg9:int64_ptr<W> -o \
+    \ arg1:int64_ptr<W>, arg2:int64_ptr<W>, arg3:int64_ptr<W>, arg4:int64_ptr<W>, \
+    \ arg5:int64_ptr<W>, arg6:int64_ptr<W>, arg7:int64_ptr<W>, arg8:int64_ptr<W>, \
+    \ arg9:int64_ptr<W>, ret:true";
 
 heapster_typecheck_fun env "round_16_80"
  "(). arg0:int64<>, arg1:int64<>, \
-    \ arg2:int64_ptr<>, arg3:int64_ptr<>, arg4:int64_ptr<>, arg5:int64_ptr<>, \
-    \ arg6:int64_ptr<>, arg7:int64_ptr<>, arg8:int64_ptr<>, arg9:int64_ptr<>, \
+    \ arg2:int64_ptr<W>, arg3:int64_ptr<W>, arg4:int64_ptr<W>, arg5:int64_ptr<W>, \
+    \ arg6:int64_ptr<W>, arg7:int64_ptr<W>, arg8:int64_ptr<W>, arg9:int64_ptr<W>, \
     \ arg10:array(W,0,<16,*8,fieldsh(int64<>)), \
-    \ arg11:ptr((W,0) |-> true), arg12:ptr((W,0) |-> true), arg13:int64_ptr<> -o \
-    \ arg2:int64_ptr<>, arg3:int64_ptr<>, arg4:int64_ptr<>, arg5:int64_ptr<>, \
-    \ arg6:int64_ptr<>, arg7:int64_ptr<>, arg8:int64_ptr<>, arg9:int64_ptr<>, \
+    \ arg11:true_ptr<W>, arg12:true_ptr<W>, arg13:int64_ptr<W> -o \
+    \ arg2:int64_ptr<W>, arg3:int64_ptr<W>, arg4:int64_ptr<W>, arg5:int64_ptr<W>, \
+    \ arg6:int64_ptr<W>, arg7:int64_ptr<W>, arg8:int64_ptr<W>, arg9:int64_ptr<W>, \
     \ arg10:array(W,0,<16,*8,fieldsh(int64<>)), \
-    \ arg11:int64_ptr<>, arg12:int64_ptr<>, arg13:int64_ptr<>, ret:true";
+    \ arg11:int64_ptr<W>, arg12:int64_ptr<W>, arg13:int64_ptr<W>, ret:true";
 
 heapster_typecheck_fun env "return_X"
   "(). arg0:array(W,0,<16,*8,fieldsh(int64<>)) -o \
      \ arg0:array(W,0,<16,*8,fieldsh(int64<>))";
 
 heapster_set_translation_checks env false;
 heapster_typecheck_fun env "processBlock"
-  "(). arg0:int64_ptr<>, arg1:int64_ptr<>, arg2:int64_ptr<>, \
-     \ arg3:int64_ptr<>, arg4:int64_ptr<>, arg5:int64_ptr<>, \
-     \ arg6:int64_ptr<>, arg7:int64_ptr<>, \
+  "(). arg0:int64_ptr<W>, arg1:int64_ptr<W>, arg2:int64_ptr<W>, \
+     \ arg3:int64_ptr<W>, arg4:int64_ptr<W>, arg5:int64_ptr<W>, \
+     \ arg6:int64_ptr<W>, arg7:int64_ptr<W>, \
      \ arg8:array(R,0,<16,*8,fieldsh(int64<>)) -o \
-     \ arg0:int64_ptr<>, arg1:int64_ptr<>, arg2:int64_ptr<>, \
-     \ arg3:int64_ptr<>, arg4:int64_ptr<>, arg5:int64_ptr<>, \
-     \ arg6:int64_ptr<>, arg7:int64_ptr<>, \
+     \ arg0:int64_ptr<W>, arg1:int64_ptr<W>, arg2:int64_ptr<W>, \
+     \ arg3:int64_ptr<W>, arg4:int64_ptr<W>, arg5:int64_ptr<W>, \
+     \ arg6:int64_ptr<W>, arg7:int64_ptr<W>, \
      \ arg8:array(R,0,<16,*8,fieldsh(int64<>)), ret:true";
 
 // FIXME: This translation contains errors
@@ -103,6 +106,4 @@ monadify_term {{ Maj }};
 monadify_term {{ round_00_15_spec }};
 
 run_test "round_00_15 |= round_00_15_spec" (mr_solver round_00_15 {{ round_00_15_spec }}) true;
-
-// FIXME: Need to add heterogenous equality on output types for this to work
-// run_test "round_16_80 |= round_16_80_spec" (mr_solver_debug 0 round_16_80 {{ round_16_80_spec }}) true;
+run_test "round_16_80 |= round_16_80_spec" (mr_solver round_16_80 {{ round_16_80_spec }}) true;

saw-core/src/Verifier/SAW/Recognizer.hs

@@ -60,6 +60,7 @@ module Verifier.SAW.Recognizer
     -- * Prelude recognizers.
   , asBool
   , asBoolType
+  , asNatType
   , asIntegerType
   , asIntModType
   , asBitvectorType
@@ -357,6 +358,11 @@ asBool _ = Nothing
 asBoolType :: Recognizer Term ()
 asBoolType = isGlobalDef "Prelude.Bool"
 
+asNatType :: Recognizer Term ()
+asNatType (asDataType -> Just (o, []))
+  | primName o == preludeNatIdent = return ()
+asNatType _ = Nothing
+
 asIntegerType :: Recognizer Term ()
 asIntegerType = isGlobalDef "Prelude.Integer"
 

src/SAWScript/Prover/MRSolver/Monad.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DerivingStrategies #-}
@@ -22,8 +23,10 @@ monadic combinators for operating on terms.
 
 module SAWScript.Prover.MRSolver.Monad where
 
-import Data.List (find, findIndex)
+import Data.List (find, findIndex, foldl')
 import qualified Data.Text as T
+import Numeric.Natural (Natural)
+import Data.Bits (testBit)
 import System.IO (hPutStrLn, stderr)
 import Control.Monad.Reader
 import Control.Monad.State
@@ -62,7 +65,7 @@ data FailCtx
 
 -- | That's MR. Failure to you
 data MRFailure
-  = TermsNotEq Term Term
+  = TermsNotRel Bool Term Term
   | TypesNotEq Type Type
   | CompsDoNotRefine NormComp NormComp
   | ReturnNotError Term
@@ -84,6 +87,9 @@ data MRFailure
   | MRFailureDisj MRFailure MRFailure
   deriving Show
 
+pattern TermsNotEq :: Term -> Term -> MRFailure
+pattern TermsNotEq t1 t2 = TermsNotRel False t1 t2
+
 -- | Pretty-print an object prefixed with a 'String' that describes it
 ppWithPrefix :: PrettyInCtx a => String -> a -> PPInCtxM SawDoc
 ppWithPrefix str a = (pretty str <>) <$> nest 2 <$> (line <>) <$> prettyInCtx a
@@ -109,8 +115,10 @@ instance PrettyInCtx FailCtx where
                                 prettyInCtx t]
 
 instance PrettyInCtx MRFailure where
-  prettyInCtx (TermsNotEq t1 t2) =
+  prettyInCtx (TermsNotRel False t1 t2) =
     ppWithPrefixSep "Could not prove terms equal:" t1 "and" t2
+  prettyInCtx (TermsNotRel True t1 t2) =
+    ppWithPrefixSep "Could not prove terms heterogeneously related:" t1 "and" t2
   prettyInCtx (TypesNotEq tp1 tp2) =
     ppWithPrefixSep "Types not equal:" tp1 "and" tp2
   prettyInCtx (CompsDoNotRefine m1 m2) =
@@ -245,27 +253,6 @@ instance PrettyInCtx DataTypeAssump where
   prettyInCtx (IsNum   x) = prettyInCtx x >>= ppWithPrefix "TCNum"
   prettyInCtx IsInf = return "TCInf"
 
--- | Recognize a term as a @Left@ or @Right@
-asEither :: Recognizer Term (Either Term Term)
-asEither (asCtor -> Just (c, [_, _, x]))
-  | primName c == "Prelude.Left"  = return $ Left x
-  | primName c == "Prelude.Right" = return $ Right x
-asEither _ = Nothing
-
--- | Recognize a term as a @TCNum n@ or @TCInf@
-asNum :: Recognizer Term (Either Term ())
-asNum (asCtor -> Just (c, [n]))
-  | primName c == "Cryptol.TCNum"  = return $ Left n
-asNum (asCtor -> Just (c, []))
-  | primName c == "Cryptol.TCInf"  = return $ Right ()
-asNum _ = Nothing
-
--- | Recognize a term as being of the form @isFinite n@
-asIsFinite :: Recognizer Term Term
-asIsFinite (asApp -> Just (isGlobalDef "CryptolM.isFinite" -> Just (), n)) =
-  Just n
-asIsFinite _ = Nothing
-
 -- | Create a term representing the type @IsFinite n@
 mrIsFinite :: Term -> MRM Term
 mrIsFinite n = liftSC2 scGlobalApply "CryptolM.isFinite" [n]
@@ -481,6 +468,22 @@ funNameType (GlobalName gd projs) =
 mrApplyAll :: Term -> [Term] -> MRM Term
 mrApplyAll f args = liftSC2 scApplyAllBeta f args
 
+-- | Like 'scBvNat', but if given a bitvector literal it is converted to a
+-- natural number literal
+mrBvToNat :: Term -> Term -> MRM Term
+mrBvToNat _ (asArrayValue -> Just (asBoolType -> Just _,
+                                   mapM asBool -> Just bits)) =
+  liftSC1 scNat $ foldl' (\n bit -> if bit then 2*n+1 else 2*n) 0 bits
+mrBvToNat n len = liftSC2 scBvNat n len
+
+-- | Like 'scBvConst', but returns a bitvector literal
+mrBvConst :: Natural -> Integer -> MRM Term
+mrBvConst n x =
+  do bool_tp <- liftSC0 scBoolType
+     bits <- mapM (liftSC1 scBool . testBit x)
+                  [(fromIntegral n - 1), (fromIntegral n - 2) .. 0]
+     liftSC2 scVector bool_tp bits
+
 -- | Get the current context of uvars as a list of variable names and their
 -- types as SAW core 'Term's, with the least recently bound uvar first, i.e., in
 -- the order as seen "from the outside"