[MRSolver] Changes to Mr. Solver to get zero_array working

cryptol-saw-core/cryptol-saw-core.cabal

@@ -15,6 +15,7 @@ Description:
 
 extra-source-files:
     saw/Cryptol.sawcore
+    saw/CryptolM.sawcore
 
 library
   build-depends:

cryptol-saw-core/saw/CryptolM.sawcore

@@ -57,16 +57,67 @@ mseq : Num -> sort 0 -> sort 0;
 mseq num a =
   Num_rec (\ (_:Num) -> sort 0) (\ (n:Nat) -> Vec n a) (Stream (CompM a)) num;
 
+bvVecMapInvarBindM : (a b c : isort 0) -> (n : Nat) -> (len : Vec n Bool) ->
+                     (a -> CompM b) -> BVVec n len a ->
+                     Bool -> (BVVec n len b -> CompM c) -> CompM c;
+bvVecMapInvarBindM a b c n len f xs invar cont =
+  existsM (BVVec n len b) c (\ (ys0:BVVec n len b) ->
+    multiArgFixM
+      (LRT_Fun (Vec n Bool) (\ (_:Vec n Bool) ->
+       LRT_Fun (BVVec n len b) (\ (_:BVVec n len b) ->
+       LRT_Ret c)))
+      (\ (rec : Vec n Bool -> BVVec n len b -> CompM c)
+         (i:Vec n Bool) (ys:BVVec n len b) ->
+         invariantHint (CompM c) (and (bvule n i len) invar)
+           (maybe (is_bvult n i len) (CompM c)
+                  (cont ys)
+                  (\ (pf:is_bvult n i len) ->
+                     bindM b c
+                           (f (atBVVec n len a xs i pf))
+                           (\ (y:b) -> rec (bvAdd n i (bvNat n 1))
+                                           (updBVVec n len b ys i y)))
+                  (bvultWithProof n i len)))
+      (bvNat n 0) ys0);
+
+bvVecMapInvarM : (a b : isort 0) -> (n : Nat) -> (len : Vec n Bool) ->
+                 (a -> CompM b) -> BVVec n len a ->
+                 Bool -> CompM (BVVec n len b);
+bvVecMapInvarM a b n len f xs invar =
+  bvVecMapInvarBindM a b (BVVec n len b) n len f xs invar
+                                                    (returnM (BVVec n len b));
+
+bvVecMapM : (a b : isort 0) -> (n : Nat) -> (len : Vec n Bool) ->
+            (a -> CompM b) -> BVVec n len a -> CompM (BVVec n len b);
+bvVecMapM a b n len f xs = bvVecMapInvarM a b n len f xs True;
+
+vecMapInvarBindM : (a b c : isort 0) -> (n : Nat) -> (a -> CompM b) ->
+                   Vec n a -> Bool -> (Vec n b -> CompM c) -> CompM c;
+vecMapInvarBindM a b c n f xs invar cont =
+  existsM (Vec n b) c (\ (ys0:Vec n b) ->
+    multiArgFixM
+      (LRT_Fun Nat (\ (_:Nat) ->
+       LRT_Fun (Vec n b) (\ (_:Vec n b) ->
+       LRT_Ret c)))
+      (\ (rec : Nat -> Vec n b -> CompM c) (i:Nat) (ys:Vec n b) ->
+         invariantHint (CompM c) (and (ltNat i (Succ n)) invar)
+           (maybe (IsLtNat i n) (CompM c)
+                  (cont ys)
+                  (\ (pf:IsLtNat i n) ->
+                     bindM b c
+                           (f (atWithProof n a xs i pf))
+                           (\ (y:b) -> rec (Succ i)
+                                           (updWithProof n b ys i y pf)))
+                  (proveLtNat i n)))
+      0 ys0);
+
+vecMapInvarM : (a b : isort 0) -> (n : Nat) -> (a -> CompM b) -> Vec n a ->
+               Bool -> CompM (Vec n b);
+vecMapInvarM a b n f xs invar =
+  vecMapInvarBindM a b (Vec n b) n f xs invar (returnM (Vec n b));
+
 vecMapM : (a b : isort 0) -> (n : Nat) -> (a -> CompM b) -> Vec n a ->
           CompM (Vec n b);
-vecMapM a b n_top f =
-  Nat__rec (\ (n:Nat) -> Vec n a -> CompM (Vec n b))
-           (\ (_:Vec 0 a) -> returnM (Vec 0 b) (EmptyVec b))
-           (\ (n:Nat) (rec:Vec n a -> CompM (Vec n b)) (v:Vec (Succ n) a) ->
-              fmapM2 b (Vec n b) (Vec (Succ n) b)
-                       (\ (x:b) (xs:Vec n b) -> ConsVec b x n xs)
-                       (f (head n a v)) (rec (tail n a v)))
-           n_top;
+vecMapM a b n f xs = vecMapInvarM a b n f xs True;
 
 -- Computational version of seqMap
 seqMapM : (a b : sort 0) -> (n : Num) -> (a -> CompM b) -> mseq n a ->
@@ -97,17 +148,36 @@ seqToMseq n_top a =
 --------------------------------------------------------------------------------
 -- Auxiliary functions
 
-atM : (n : Nat) -> (a : sort 0) -> Vec n a -> Nat -> CompM a;
-atM n_top a =
-  Nat__rec
-    (\ (n:Nat) -> Vec n a -> Nat -> CompM a)
-    (\ (_:Vec 0 a) (_:Nat) -> errorM a "atM: index out of bounds")
-    (\ (n:Nat) (rec_f: Vec n a -> Nat -> CompM a) (v:Vec (Succ n) a) (i:Nat) ->
-       Nat_cases (CompM a)
-                 (returnM a (head n a v))
-                 (\ (i_prev:Nat) (_:CompM a) -> rec_f (tail n a v) i_prev) i)
-    n_top;
-
+bvVecAtM : (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) ->
+           BVVec n len a -> Vec n Bool -> CompM a;
+bvVecAtM n len a xs i =
+  maybe (is_bvult n i len) (CompM a)
+        (errorM a "bvVecAtM: invalid sequence index")
+        (\ (pf:is_bvult n i len) -> returnM a (atBVVec n len a xs i pf))
+        (bvultWithProof n i len);
+
+atM : (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> CompM a;
+atM n a xs i =
+  maybe (IsLtNat i n) (CompM a)
+        (errorM a "atM: invalid sequence index")
+        (\ (pf:IsLtNat i n) -> returnM a (atWithProof n a xs i pf))
+        (proveLtNat i n);
+
+bvVecUpdateM : (n : Nat) -> (len : Vec n Bool) -> (a : isort 0) ->
+               BVVec n len a -> Vec n Bool -> a -> CompM (BVVec n len a);
+bvVecUpdateM n len a xs i x =
+  maybe (is_bvult n i len) (CompM (BVVec n len a))
+        (errorM (BVVec n len a) "bvVecUpdateM: invalid sequence index")
+        (\ (_:is_bvult n i len) -> returnM (BVVec n len a)
+                                           (updBVVec n len a xs i x))
+        (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))
+        (errorM (Vec n a) "updateM: invalid sequence index")
+        (\ (pf:IsLtNat i n) -> returnM (Vec n a) (updWithProof n a xs i x pf))
+        (proveLtNat i n);
 
 eListSelM : (a : isort 0) -> (n : Num) -> mseq n a -> Nat -> CompM a;
 eListSelM a =
@@ -347,15 +417,35 @@ primitive
 ecTransposeM : (m n : Num) -> (a : sort 0) -> mseq m (mseq n a) ->
                mseq n (mseq m a);
 
-ecAtM : (n : Num) -> (a ix: sort 0) -> PIntegral ix -> mseq n a -> ix -> CompM a;
+ecAtM : (n : Num) -> (a : isort 0) -> (ix : sort 0) -> PIntegral ix ->
+        mseq n a -> ix -> CompM a;
 ecAtM n_top a ix pix =
   Num_rec
     (\ (n:Num) -> mseq n a -> ix -> CompM a)
     (\ (n:Nat) (v:Vec n a) ->
-       pix.posNegCases (CompM a) (atM n a v) (\ (_:Nat) -> atM n a v 0))
+       pix.posNegCases (CompM a) (atM n a v)
+                       (\ (_:Nat) -> errorM a "ecAtM: invalid sequence index"))
     (\ (s:Stream (CompM a)) ->
        pix.posNegCases (CompM a) (streamGet (CompM a) s)
-                       (\ (_:Nat) -> (streamGet (CompM a) s) 0))
+                       (\ (_:Nat) -> errorM a "ecAtM: invalid sequence index"))
+    n_top;
+
+ecUpdateM : (n : Num) -> (a : isort 0) -> (ix : sort 0) -> PIntegral ix ->
+            mseq n a -> ix -> a -> CompM (mseq n a);
+ecUpdateM n_top a ix pix =
+  Num_rec
+    (\ (n:Num) -> mseq n a -> ix -> a -> CompM (mseq n a))
+    (\ (n:Nat) (v:Vec n a) (i:ix) (x:a) ->
+       pix.posNegCases (CompM (Vec n a))
+                       (\ (i:Nat) -> updateM n a v i x)
+                       (\ (_:Nat) -> errorM (Vec n a)
+                                       "ecUpdateM: invalid sequence index") i)
+    (\ (s:Stream (CompM a)) (i:ix) (x:a) ->
+       pix.posNegCases (CompM (Stream (CompM a)))
+                       (\ (i:Nat) -> returnM (Stream (CompM a))
+                                       (streamUpd (CompM a) s i (returnM a x)))
+                       (\ (_:Nat) -> errorM (Stream (CompM a))
+                                       "ecUpdateM: invalid sequence index") i)
     n_top;
 
 -- FIXME

cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs

@@ -1015,6 +1015,41 @@ eitherMacro = MonMacro 3 $ \_ args ->
                             (MTyArrow (MTyArrow mtp_b mtp_c)
                              (MTyArrow (mkMonType0 tp_eith) mtp_c))) eith_app
 
+-- | The macro for invariantHint, which converts @invariantHint a cond m@
+-- to @invariantHint (CompM a) cond m@ and which contains any binds in the body
+-- to the body
+invariantHintMacro :: MonMacro
+invariantHintMacro = MonMacro 3 $ \_ args ->
+  do let (tp, cond, m) =
+           case args of
+             [t1, t2, t3] -> (t1, t2, t3)
+             _ -> error "invariantHintMacro: wrong number of arguments!"
+     atrm_cond <- monadifyArg (Just boolMonType) cond
+     mtp <- monadifyTypeM tp
+     mtrm <- resetMonadifyM (toArgType mtp) $ monadifyTerm (Just mtp) m
+     return $ fromCompTerm mtp $
+       applyOpenTermMulti (globalOpenTerm "Prelude.invariantHint")
+       [toCompType mtp, toArgTerm atrm_cond, toCompTerm mtrm]
+
+-- | The macro for @asserting@ or @assuming@, which converts @asserting@ to
+-- @assertingM@ or @assuming@ to @assumingM@ (depending on whether the given
+-- 'Bool' is true or false, respectively) and which contains any binds in the
+-- body to the body
+assertingOrAssumingMacro :: Bool -> MonMacro
+assertingOrAssumingMacro doAsserting = MonMacro 3 $ \_ args ->
+  do let (tp, cond, m) =
+           case args of
+             [t1, t2, t3] -> (t1, t2, t3)
+             _ -> error "assertingOrAssumingMacro: wrong number of arguments!"
+     atrm_cond <- monadifyArg (Just boolMonType) cond
+     mtp <- monadifyTypeM tp
+     mtrm <- resetMonadifyM (toArgType mtp) $ monadifyTerm (Just mtp) m
+     let ident = if doAsserting then "Prelude.assertingM"
+                                else "Prelude.assumingM"
+     return $ fromCompTerm mtp $
+       applyOpenTermMulti (globalOpenTerm ident)
+       [toArgType mtp, toArgTerm atrm_cond, toCompTerm mtrm]
+
 -- | Make a 'MonMacro' that maps a named global whose first argument is @n:Num@
 -- to a global of semi-pure type that takes an additional argument of type
 -- @isFinite n@
@@ -1050,7 +1085,6 @@ lrtFromMonType (MTyArrow mtp1 mtp2) =
 lrtFromMonType mtp =
   ctorOpenTerm "Prelude.LRT_Ret" [toArgType mtp]
 
-
 -- | The macro for fix
 --
 -- FIXME: does not yet handle mutual recursion
@@ -1104,6 +1138,9 @@ defaultMonEnv =
   , mmCustom "Prelude.ite" iteMacro
   , mmCustom "Prelude.fix" fixMacro
   , mmCustom "Prelude.either" eitherMacro
+  , mmCustom "Prelude.invariantHint" invariantHintMacro
+  , mmCustom "Prelude.asserting" (assertingOrAssumingMacro True)
+  , mmCustom "Prelude.assuming" (assertingOrAssumingMacro False)
 
     -- Top-level sequence functions
   , mmArg "Cryptol.seqMap" "CryptolM.seqMapM"
@@ -1176,6 +1213,7 @@ defaultMonEnv =
   , mmSemiPureFin1 "Cryptol.ecReverse" "CryptolM.ecReverseM"
   , mmSemiPure "Cryptol.ecTranspose" "CryptolM.ecTransposeM"
   , mmArg "Cryptol.ecAt" "CryptolM.ecAtM"
+  , mmArg "Cryptol.ecUpdate" "CryptolM.ecUpdateM"
   -- , mmArgFin1 "Cryptol.ecAtBack" "CryptolM.ecAtBackM"
   -- , mmSemiPureFin2 "Cryptol.ecFromTo" "CryptolM.ecFromToM"
   , mmSemiPureFin1 "Cryptol.ecFromToLessThan" "CryptolM.ecFromToLessThanM"

heapster-saw/examples/SpecPrims.cry

@@ -0,0 +1,37 @@
+module SpecPrims where
+
+/* Specification primitives */
+
+// The specification that holds for f x for some input x
+exists : {a, b} (a -> b) -> b
+exists f = error "Cannot run exists"
+
+// The specification that holds for f x for all inputs x
+forall : {a, b} (a -> b) -> b
+forall f = error "Cannot run forall"
+
+// The specification that a computation returns some value with no errors
+returnsSpec : {a} a
+returnsSpec = exists (\x -> x)
+
+// The specification that matches any computation. This calls exists at the
+// function type () -> a, which is monadified to () -> CompM a. This means that
+// the exists does not just quantify over all values of type a like noErrors,
+// but it quantifies over all computations of type a, including those that
+// contain errors.
+anySpec : {a} a
+anySpec = exists (\f -> f ())
+
+// The specification which asserts that the first argument is True and then
+// returns the second argument
+asserting : {a} Bit -> a -> a
+asserting b x = if b then x else error "Assertion failed"
+
+// The specification which assumes that the first argument is True and then
+// returns the second argument
+assuming : {a} Bit -> a -> a
+assuming b x = if b then x else anySpec
+
+// A hint to Mr Solver that a recursive function has the given loop invariant
+invariantHint : {a} Bit -> a -> a
+invariantHint b x = x

heapster-saw/examples/arrays.cry

@@ -0,0 +1,15 @@
+
+module Arrays where
+
+import SpecPrims
+
+zero_array_loop_spec : {n} Literal n [64] => [n][64] -> [n][64]
+zero_array_loop_spec ys = loop 0 ys
+  where loop : [64] -> [n][64] -> [n][64]
+        loop i xs = invariantHint (i <= 0x0fffffffffffffff)
+                                  (if i < `n then loop (i+1) (update xs i 0)
+                                             else xs)
+
+zero_array_spec : {n} Literal n [64] => [n][64] -> [n][64]
+zero_array_spec xs = assuming (`n <= 0x0fffffffffffffff)
+                              [ 0 | _ <- xs ]

heapster-saw/examples/arrays.sawcore

@@ -21,7 +21,7 @@ noErrorsContains0H len_top i_top v_top =
     (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
             CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
        ((\ (len:Vec 64 Bool) (i:Vec 64 Bool) (v:BVVec 64 len (Vec 64 Bool)) ->
-           precondHint
+           invariantHint
              (CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))
              (and (bvsle 64 0x0000000000000000 i)
                   (bvsle 64 i 0x0fffffffffffffff))

heapster-saw/examples/arrays_mr_solver.saw

@@ -21,3 +21,11 @@ contains0 <- parse_core_mod "arrays" "contains0";
 noErrorsContains0 <- parse_core_mod "arrays" "noErrorsContains0";
 run_test "contains0 |= noErrorsContains0"
   (mr_solver_debug 0 contains0 noErrorsContains0) true;
+
+include "specPrims.saw";
+import "arrays.cry";
+
+zero_array <- parse_core_mod "arrays" "zero_array";
+run_test "zero_array |= zero_array_spec"
+//  (mr_solver_debug 0 zero_array {{ zero_array_loop_spec }}) true;
+  (mr_solver_debug 0 zero_array {{ zero_array_spec }}) true;

heapster-saw/examples/exp_explosion.cry

@@ -0,0 +1,23 @@
+
+module ExpExplosion where
+
+op : [64] -> [64] -> [64]
+op x y = x ^ (y << (1 : [6]))
+
+exp_explosion_spec : [64] -> [64]
+exp_explosion_spec x0 = x15
+  where x1 = op x0 x0
+        x2 = op x1 x1
+        x3 = op x2 x2
+        x4 = op x3 x3
+        x5 = op x4 x4
+        x6 = op x5 x5
+        x7 = op x6 x6
+        x8 = op x7 x7
+        x9 = op x8 x8
+        x10 = op x9 x9
+        x11 = op x10 x10
+        x12 = op x11 x11
+        x13 = op x12 x12
+        x14 = op x13 x13
+        x15 = op x14 x14

heapster-saw/examples/exp_explosion.saw

@@ -4,6 +4,6 @@ env <- heapster_init_env "exp_explosion" "exp_explosion.bc";
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
 heapster_typecheck_fun env "exp_explosion"
-  "(). arg0:int64<> -o arg0:int64<>, ret:int64<>";
+  "(). arg0:int64<> -o ret:int64<>";
 
 heapster_export_coq env "exp_explosion_gen.v";

heapster-saw/examples/exp_explosion_mr_solver.saw

@@ -0,0 +1,23 @@
+include "exp_explosion.saw";
+
+let eq_bool b1 b2 =
+  if b1 then
+    if b2 then true else false
+  else
+    if b2 then false else true;
+
+let fail = do { print "Test failed"; exit 1; };
+let run_test name test expected =
+  do { if expected then print (str_concat "Test: " name) else
+         print (str_concat (str_concat "Test: " name) " (expecting failure)");
+       actual <- test;
+       if eq_bool actual expected then print "Success\n" else
+         do { print "Test failed\n"; exit 1; }; };
+
+
+
+import "exp_explosion.cry";
+monadify_term {{ op }};
+
+exp_explosion <- parse_core_mod "exp_explosion" "exp_explosion";
+run_test "exp_explosion |= exp_explosion_spec" (mr_solver exp_explosion {{ exp_explosion_spec }}) true;

heapster-saw/examples/linked_list_mr_solver.saw

@@ -51,5 +51,19 @@ run_test "is_head |= is_head" (mr_solver is_head is_head) true;
 */
 
 is_elem <- parse_core_mod "linked_list" "is_elem";
-run_test "is_elem |= is_elem_spec" (mr_solver_debug 2 is_elem {{ is_elem_spec }}) true;
-//run_test "is_elem |= is_elem" (mr_solver_debug 1 is_elem is_elem) true;
+// run_test "is_elem |= is_elem" (mr_solver_debug 0 is_elem is_elem) true;
+
+/*
+is_elem_noErrorsSpec <- parse_core
+  "\\ (x:Vec 64 Bool) (y:List (Vec 64 Bool)) -> \
+    \ fixM (Vec 64 Bool * List (Vec 64 Bool)) \
+    \      (\\ (pr : Vec 64 Bool * List (Vec 64 Bool)) -> Vec 64 Bool) \
+    \      (\\ (rec : (x : Vec 64 Bool * List (Vec 64 Bool)) -> CompM (Vec 64 Bool)) \
+    \          (x : Vec 64 Bool * List (Vec 64 Bool)) -> \
+    \          orM (Vec 64 Bool) \
+    \              (existsM (Vec 64 Bool) (Vec 64 Bool) (returnM (Vec 64 Bool))) \
+    \              (rec x)) (x, y)";
+run_test "is_elem |= noErrorsSpec" (mr_solver is_elem is_elem_noErrorsSpec) true;
+*/
+
+run_test "is_elem |= is_elem_spec" (mr_solver is_elem {{ is_elem_spec }}) true;