Mr Solver precondition hints

heapster-saw/examples/arrays.sawcore

@@ -2,3 +2,40 @@
 module arrays where
 
 import Prelude;
+
+-- The helper function for noErrorsContains0
+--
+-- noErrorsContains0H len i v =
+--   orM (exists x. returnM x) (noErrorsContains0H len (i+1) v)
+noErrorsContains0H : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
+                     CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
+noErrorsContains0H len_top i_top v_top =
+  letRecM
+    (LRT_Cons
+     (LRT_Fun (Vec 64 Bool) (\ (len:Vec 64 Bool) ->
+      LRT_Fun (Vec 64 Bool) (\ (_:Vec 64 Bool) ->
+      LRT_Fun (BVVec 64 len (Vec 64 Bool)) (\ (_:BVVec 64 len (Vec 64 Bool)) ->
+      LRT_Ret (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))))
+     LRT_Nil)
+    (BVVec 64 len_top (Vec 64 Bool) * Vec 64 Bool)
+    (\ (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
+             (CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool))
+             (and (bvsle 64 0x0000000000000000 i)
+                  (bvsle 64 i 0x0fffffffffffffff))
+             (orM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
+                  (existsM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
+                           (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)
+                           (returnM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)))
+                  (f len (bvAdd 64 i 0x0000000000000001) v))), ()))
+    (\ (f : (len i:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
+            CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool)) ->
+       f len_top i_top v_top);
+
+-- The specification that contains0 has no errors
+noErrorsContains0 : (len:Vec 64 Bool) -> BVVec 64 len (Vec 64 Bool) ->
+                    CompM (BVVec 64 len (Vec 64 Bool) * Vec 64 Bool);
+noErrorsContains0 len v =
+  noErrorsContains0H len 0x0000000000000000 v;

heapster-saw/examples/arrays_mr_solver.saw

@@ -16,4 +16,8 @@ let run_test name test expected =
 
 // Test that contains0 |= contains0
 contains0 <- parse_core_mod "arrays" "contains0";
-run_test "contains0 |= contains0" (mr_solver contains0 contains0) true;
+// run_test "contains0 |= contains0" (mr_solver contains0 contains0) true;
+
+noErrorsContains0 <- parse_core_mod "arrays" "noErrorsContains0";
+run_test "contains0 |= noErrorsContains0"
+  (mr_solver_debug 0 contains0 noErrorsContains0) true;

saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v

@@ -377,12 +377,12 @@ Definition and_triv2 : forall (x : SAWCoreScaffolding.Bool), SAWCoreScaffolding.
   fun (x : SAWCoreScaffolding.Bool) => let var__0   := SAWCoreScaffolding.not SAWCoreScaffolding.true in
   SAWCoreScaffolding.iteDep (fun (b : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool (SAWCoreScaffolding.and (SAWCoreScaffolding.not b) b) SAWCoreScaffolding.false) x (trans SAWCoreScaffolding.Bool (SAWCoreScaffolding.and var__0 SAWCoreScaffolding.true) var__0 SAWCoreScaffolding.false (and_True2 var__0) not_True) (and_False2 (SAWCoreScaffolding.not SAWCoreScaffolding.false)).
 
-Definition FalseProp : Prop :=
-  SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false.
-
 Definition EqTrue : SAWCoreScaffolding.Bool -> Prop :=
   fun (x : SAWCoreScaffolding.Bool) => SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool x SAWCoreScaffolding.true.
 
+Definition TrueProp : Prop :=
+  EqTrue SAWCoreScaffolding.true.
+
 Definition TrueI : EqTrue SAWCoreScaffolding.true :=
   SAWCoreScaffolding.Refl SAWCoreScaffolding.Bool SAWCoreScaffolding.true.
 
@@ -534,6 +534,9 @@ Axiom head : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), SAWCoreVect
 
 Axiom tail : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), SAWCoreVectorsAsCoqVectors.Vec (SAWCoreScaffolding.Succ n) a -> SAWCoreVectorsAsCoqVectors.Vec n a .
 
+Definition atWithDefault' : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), a -> SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a :=
+  fun (n_top : SAWCoreScaffolding.Nat) (a : Type) (d : a) => Nat__rec (fun (n : SAWCoreScaffolding.Nat) => SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a) (fun (_1 : SAWCoreVectorsAsCoqVectors.Vec 0 a) (_2 : SAWCoreScaffolding.Nat) => d) (fun (n : SAWCoreScaffolding.Nat) (rec_f : SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a) (v : SAWCoreVectorsAsCoqVectors.Vec (SAWCoreScaffolding.Succ n) a) (i : SAWCoreScaffolding.Nat) => Nat_cases a (head n a v) (fun (i_prev : SAWCoreScaffolding.Nat) (_1 : a) => rec_f (tail n a v) i_prev) i) n_top.
+
 (* Prelude.atWithDefault was skipped *)
 
 Definition sawAt : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreScaffolding.Nat -> a :=
@@ -1009,10 +1012,16 @@ Definition genBVVec : forall (n : SAWCoreScaffolding.Nat), forall (len : SAWCore
 Definition genBVVecFromVec : forall (m : SAWCoreScaffolding.Nat), forall (a : Type), SAWCoreVectorsAsCoqVectors.Vec m a -> a -> forall (n : SAWCoreScaffolding.Nat), forall (len : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool), BVVec n len a :=
   fun (m : SAWCoreScaffolding.Nat) (a : Type) (v : SAWCoreVectorsAsCoqVectors.Vec m a) (def : a) (n : SAWCoreScaffolding.Nat) (len : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) => genBVVec n len a (fun (i : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) (_1 : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool (SAWCoreVectorsAsCoqVectors.bvult n i len) SAWCoreScaffolding.true) => SAWCoreVectorsAsCoqVectors.atWithDefault m a def v (SAWCoreVectorsAsCoqVectors.bvToNat n i)).
 
-Definition efq : forall (a : Type), SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false -> a :=
+Definition FalseProp : Prop :=
+  SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false.
+
+Definition efq : forall (a : Type), FalseProp -> a :=
   fun (a : Type) (contra : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false) => let var__0   := if SAWCoreScaffolding.true then unit : Type else a in
   SAWCoreScaffolding.coerce (unit : Type) a (trans Type (unit : Type) var__0 a (sym Type var__0 (unit : Type) (ite_true Type (unit : Type) a)) (trans Type var__0 (if SAWCoreScaffolding.false then unit : Type else a) a (eq_cong SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false contra Type (fun (b : SAWCoreScaffolding.Bool) => if b then unit : Type else a)) (ite_false Type (unit : Type) a))) tt.
 
+Definition efq1 : forall (a : Type), SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false -> a :=
+  fun (a : Type) (contra : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool SAWCoreScaffolding.true SAWCoreScaffolding.false) => SAWCoreScaffolding.Eq__rec Bit Bit1 (fun (b : Bit) (_1 : SAWCoreScaffolding.Eq Bit Bit1 b) => SAWCorePrelude.Bit_rect (fun (_2 : Bit) => Type) (unit : Type) a b) tt Bit0 (efq (SAWCoreScaffolding.Eq Bit Bit1 Bit0) contra).
+
 Definition emptyBVVec : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), BVVec n (SAWCoreVectorsAsCoqVectors.bvNat n 0) a :=
   fun (n : SAWCoreScaffolding.Nat) (a : Type) => genBVVec n (SAWCoreVectorsAsCoqVectors.bvNat n 0) a (fun (i : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) (pf : SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool (SAWCoreVectorsAsCoqVectors.bvult n i (SAWCoreVectorsAsCoqVectors.bvNat n 0)) SAWCoreScaffolding.true) => let var__0   := SAWCoreVectorsAsCoqVectors.bvult n i (SAWCoreVectorsAsCoqVectors.bvNat n 0) in
   efq a (trans SAWCoreScaffolding.Bool SAWCoreScaffolding.true var__0 SAWCoreScaffolding.false (sym SAWCoreScaffolding.Bool var__0 SAWCoreScaffolding.true pf) (not_bvult_zero n i))).
@@ -1130,8 +1139,6 @@ Definition foldIRT : forall (As : ListSort), forall (Ds : IRTSubsts As), forall
 
 (* Prelude.bindM was skipped *)
 
-(* Prelude.existsM was skipped *)
-
 (* Prelude.errorM was skipped *)
 
 Definition fmapM : forall (a : Type), forall (b : Type), (a -> b) -> CompM a -> CompM b :=
@@ -1147,6 +1154,21 @@ Definition fmapM2 : forall (a : Type), forall (b : Type), forall (c : Type), (a
 Definition fmapM3 : forall (a : Type), forall (b : Type), forall (c : Type), forall (d : Type), (a -> b -> c -> d) -> CompM a -> CompM b -> CompM c -> CompM d :=
   fun (a : Type) (b : Type) (c : Type) (d : Type) (f : a -> b -> c -> d) (m1 : CompM a) (m2 : CompM b) (m3 : CompM c) => applyM c d (fmapM2 a b (c -> d) f m1 m2) m3.
 
+Definition bindM2 : forall (a : Type), forall (b : Type), forall (c : Type), CompM a -> CompM b -> (a -> b -> CompM c) -> CompM c :=
+  fun (a : Type) (b : Type) (c : Type) (m1 : CompM a) (m2 : CompM b) (f : a -> b -> CompM c) => @bindM CompM _ a c m1 (fun (x : a) => @bindM CompM _ b c m2 (f x)).
+
+Definition bindM3 : forall (a : Type), forall (b : Type), forall (c : Type), forall (d : Type), CompM a -> CompM b -> CompM c -> (a -> b -> c -> CompM d) -> CompM d :=
+  fun (a : Type) (b : Type) (c : Type) (d : Type) (m1 : CompM a) (m2 : CompM b) (m3 : CompM c) (f : a -> b -> c -> CompM d) => @bindM CompM _ a d m1 (fun (x : a) => bindM2 b c d m2 m3 (f x)).
+
+Definition bindApplyM : forall (a : Type), forall (b : Type), (a -> CompM b) -> CompM a -> CompM b :=
+  fun (a : Type) (b : Type) (f : a -> CompM b) (m : CompM a) => @bindM CompM _ a b m f.
+
+Definition bindApplyM2 : forall (a : Type), forall (b : Type), forall (c : Type), (a -> b -> CompM c) -> CompM a -> CompM b -> CompM c :=
+  fun (a : Type) (b : Type) (c : Type) (f : a -> b -> CompM c) (m1 : CompM a) (m2 : CompM b) => @bindM CompM _ a c m1 (fun (x : a) => @bindM CompM _ b c m2 (f x)).
+
+Definition bindApplyM3 : forall (a : Type), forall (b : Type), forall (c : Type), forall (d : Type), (a -> b -> c -> CompM d) -> CompM a -> CompM b -> CompM c -> CompM d :=
+  fun (a : Type) (b : Type) (c : Type) (d : Type) (f : a -> b -> c -> CompM d) (m1 : CompM a) (m2 : CompM b) (m3 : CompM c) => bindM3 a b c d m1 m2 m3 f.
+
 Definition composeM : forall (a : Type), forall (b : Type), forall (c : Type), (a -> CompM b) -> (b -> CompM c) -> a -> CompM c :=
   fun (a : Type) (b : Type) (c : Type) (f : a -> CompM b) (g : b -> CompM c) (x : a) => @bindM CompM _ b c (f x) g.
 
@@ -1171,7 +1193,15 @@ Definition appendCastBVVecM : forall (n : SAWCoreScaffolding.Nat), forall (len1
   let var__5   := BVVec n len3 a in
   @returnM CompM _ var__5 (SAWCoreScaffolding.coerce (BVVec n var__4 a) var__5 (eq_cong var__3 var__4 len3 pf Type (fun (l : var__3) => BVVec n l a)) (appendBVVec n len1 len2 a v1 v2))) (bvEqWithProof n var__0 len3).
 
-(* Prelude.fixM was skipped *)
+(* Prelude.existsM was skipped *)
+
+Definition orM : forall (a : Type), CompM a -> CompM a -> CompM a :=
+  fun (a : Type) (m1 : CompM a) (m2 : CompM a) => @CompM.existsM SAWCoreScaffolding.Bool a (fun (b : SAWCoreScaffolding.Bool) => if b then m1 else m2).
+
+(* Prelude.forallM was skipped *)
+
+Definition precondHint : forall (a : Type), SAWCoreScaffolding.Bool -> a -> a :=
+  fun (_1 : Type) (_2 : SAWCoreScaffolding.Bool) (a : _1) => a.
 
 (* Prelude.LetRecType was skipped *)
 
@@ -1183,14 +1213,19 @@ Definition appendCastBVVecM : forall (n : SAWCoreScaffolding.Nat), forall (len1
 
 (* Prelude.lrtTupleType was skipped *)
 
-(* Prelude.multiFixM was skipped *)
-
 (* Prelude.letRecM was skipped *)
 
 Definition letRecM1 : forall (a : Type), forall (b : Type), forall (c : Type), ((a -> CompM b) -> a -> CompM b) -> ((a -> CompM b) -> CompM c) -> CompM c :=
   fun (a : Type) (b : Type) (c : Type) (fn : (a -> CompM b) -> a -> CompM b) (body : (a -> CompM b) -> CompM c) => let var__0   := a -> CompM b in
   @CompM.letRecM (CompM.LRT_Cons (CompM.LRT_Fun a (fun (_1 : a) => CompM.LRT_Ret b)) CompM.LRT_Nil) c (fun (f : var__0) => pair (fn f) tt) (fun (f : var__0) => body f).
 
+(* Prelude.fixM was skipped *)
+
+(* Prelude.multiFixM was skipped *)
+
+Definition multiArgFixM : forall (lrt : CompM.LetRecType), (CompM.lrtToType lrt -> CompM.lrtToType lrt) -> CompM.lrtToType lrt :=
+  fun (lrt : CompM.LetRecType) (F : CompM.LetRecType_rect (fun (lrt1 : CompM.LetRecType) => Type) (fun (b : Type) => CompM b) (fun (a : Type) (_1 : a -> CompM.LetRecType) (b : a -> Type) => forall (x : a), b x) lrt -> CompM.LetRecType_rect (fun (lrt1 : CompM.LetRecType) => Type) (fun (b : Type) => CompM b) (fun (a : Type) (_2 : a -> CompM.LetRecType) (b : a -> Type) => forall (x : a), b x) lrt) => SAWCoreScaffolding.fst (@CompM.multiFixM (CompM.LRT_Cons lrt CompM.LRT_Nil) (fun (f : CompM.LetRecType_rect (fun (lrt1 : CompM.LetRecType) => Type) (fun (b : Type) => CompM b) (fun (a : Type) (_1 : a -> CompM.LetRecType) (b : a -> Type) => forall (x : a), b x) lrt) => pair (F f) tt)).
+
 (* Prelude.test_fun0 was skipped *)
 
 (* Prelude.test_fun1 was skipped *)

saw-core/prelude/Prelude.sawcore

@@ -1718,9 +1718,9 @@ efq a contra =
 -- Ex Falso Quodlibet at sort 1
 efq1 : (a : sort 1) -> Eq Bool True False -> a;
 efq1 a contra =
-  Eq#rec Bit Bit1
-         (\ (b:Bit) (_:Eq Bit Bit1 b) -> Bit#rec (\ (_:Bit) -> sort 1) #() a b)
-         () Bit0 (efq (Eq Bit Bit1 Bit0) contra);
+  Eq__rec Bit Bit1
+          (\ (b:Bit) (_:Eq Bit Bit1 b) -> Bit#rec (\ (_:Bit) -> sort 1) #() a b)
+          () Bit0 (efq (Eq Bit Bit1 Bit0) contra);
 
 -- Generate an empty BVVec
 emptyBVVec : (n : Nat) -> (a : sort 0) -> BVVec n (bvNat n 0) a;
@@ -2158,6 +2158,10 @@ orM a m1 m2 = existsM Bool a (\ (b:Bool) -> ite (CompM a) b m1 m2);
 -- those computations diverge from each other.
 primitive forallM : (a b:sort 0) -> (a -> CompM b) -> CompM b;
 
+-- A hint to Mr Solver that a recursive function has the given precondition
+precondHint : (a : sort 0) -> Bool -> a -> a;
+precondHint _ _ a = a;
+
 -- NOTE: for the simplicity and efficiency of MR solver, we define all
 -- fixed-point computations in CompM via a primitive multiFixM, defined below.
 -- Thus, even though fixM is really the primitive operation, we write this file
@@ -2262,27 +2266,6 @@ lrtPi lrts b =
   (\ (lrt:LetRecType) (_:LetRecTypes) (rest:sort 0) -> lrtToType lrt -> rest)
   lrts;
 
--- Apply a function the the body of a multi-arity lrtPi function
-lrtPiMap : (a b : sort 0) -> (f : a -> b) -> (lrts : LetRecTypes) ->
-           lrtPi lrts a -> lrtPi lrts b;
-lrtPiMap a b f lrts_top =
-  LetRecTypes#rec
-  (\ (lrts:LetRecTypes) -> lrtPi lrts a -> lrtPi lrts b)
-  (\ (x:a) -> f x)
-  (\ (lrt:LetRecType) (lrts:LetRecTypes) (rec:lrtPi lrts a -> lrtPi lrts b)
-     (f:lrtToType lrt -> lrtPi lrts a) (g:lrtToType lrt) ->
-     rec (f g))
-  lrts_top;
-
--- Convert a multi-arity lrtPi that returns a pair to a pair of lrtPi functions
--- that return the individual arguments
-lrtPiPair : (a b:sort 0) -> (lrts : LetRecTypes) -> lrtPi lrts #(a,b) ->
-            #(lrtPi lrts a, lrtPi lrts b);
-lrtPiPair a b lrts f =
-  (lrtPiMap #(a,b) a (\ (tup:#(a,b)) -> tup.(1)) lrts f,
-   lrtPiMap #(a,b) b (\ (tup:#(a,b)) -> tup.(2)) lrts f);
-
-
 -- Build the product type (lrtToType lrt1, ..., lrtToType lrtn) from the
 -- LetRecTypes list [lrt1, ..., lrtn]
 lrtTupleType : LetRecTypes -> sort 0;
@@ -2387,6 +2370,32 @@ fixM a b f x =
           (\ (g: (y:a) -> CompM (b y)) -> (f g, ()))
           (\ (g: (y:a) -> CompM (b y)) -> g x);
 
+
+-- The following commented block allows multiFixM to be defined in terms of and
+-- to reduce to letRecM, which is useful if we want to define all our automated
+-- reasoning in terms of letRecM instead of multiFixM
+
+-- Apply a function the the body of a multi-arity lrtPi function
+{-
+lrtPiMap : (a b : sort 0) -> (f : a -> b) -> (lrts : LetRecTypes) ->
+           lrtPi lrts a -> lrtPi lrts b;
+lrtPiMap a b f lrts_top =
+  LetRecTypes#rec
+  (\ (lrts:LetRecTypes) -> lrtPi lrts a -> lrtPi lrts b)
+  (\ (x:a) -> f x)
+  (\ (lrt:LetRecType) (lrts:LetRecTypes) (rec:lrtPi lrts a -> lrtPi lrts b)
+     (f:lrtToType lrt -> lrtPi lrts a) (g:lrtToType lrt) ->
+     rec (f g))
+  lrts_top;
+
+-- Convert a multi-arity lrtPi that returns a pair to a pair of lrtPi functions
+-- that return the individual arguments
+lrtPiPair : (a b:sort 0) -> (lrts : LetRecTypes) -> lrtPi lrts #(a,b) ->
+            #(lrtPi lrts a, lrtPi lrts b);
+lrtPiPair a b lrts f =
+  (lrtPiMap #(a,b) a (\ (tup:#(a,b)) -> tup.(1)) lrts f,
+   lrtPiMap #(a,b) b (\ (tup:#(a,b)) -> tup.(2)) lrts f);
+
 -- Build a monadic function that takes in its arguments and then calls letRecM.
 -- That is, build a function
 --
@@ -2439,6 +2448,21 @@ multiFixM lrts_top F_top =
       rec (lrtPiPair (lrtToType lrt) (lrtTupleType lrts) lrts_top F).(2)))
   lrts_top
   F_top;
+-}
+
+-- Construct a fixed-point for a tuple of mutually-recursive functions
+--
+-- NOTE: Currently, Mr Solver actually works better with a primitive multiFixM,
+-- so that's what we are going to do for now...
+primitive
+multiFixM : (lrts:LetRecTypes) -> lrtPi lrts (lrtTupleType lrts) ->
+            lrtTupleType lrts;
+
+-- Build a multi-argument fixed-point of type A1 -> ... -> An -> CompM B
+multiArgFixM : (lrt:LetRecType) -> (lrtToType lrt -> lrtToType lrt) ->
+               lrtToType lrt;
+multiArgFixM lrt F =
+  (multiFixM (LRT_Cons lrt LRT_Nil) (\ (f:lrtToType lrt) -> (F f, ()))).(1);
 
 
 -- Test computations

saw-core/src/Verifier/SAW/Term/Functor.hs

@@ -58,6 +58,7 @@ module Verifier.SAW.Term.Functor
     -- * Sets of free variables
   , BitSet, emptyBitSet, inBitSet, unionBitSets, intersectBitSets
   , decrBitSet, multiDecrBitSet, completeBitSet, singletonBitSet, bitSetElems
+  , smallestBitSetElem
   , looseVars, smallestFreeVar
   ) where
 
@@ -485,7 +486,7 @@ bitSetElems = go 0 where
   go shft bs = case smallestBitSetElem bs of
     Nothing -> []
     Just i ->
-      shft + i : go (shft + i + 1) (multiDecrBitSet (shft + i + 1) bs)
+      shft + i : go (shft + i + 1) (multiDecrBitSet (i + 1) bs)
 
 -- | Compute the free variables of a term given free variables for its immediate
 -- subterms

saw-remote-api/src/SAWServer.hs

@@ -59,6 +59,7 @@ import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
 import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm)
 import qualified Cryptol.Utils.Ident as Cryptol
 import Verifier.SAW.Cryptol.Monadify (defaultMonEnv)
+import SAWScript.Prover.MRSolver (emptyMREnv)
 
 import qualified Argo
 --import qualified CryptolServer (validateServerState, ServerState(..))
@@ -219,6 +220,7 @@ initialState readFileFn =
                 , rwDocs = mempty
                 , rwCryptol = cenv
                 , rwMonadify = defaultMonEnv
+                , rwMRSolverEnv = emptyMREnv
                 , rwPPOpts = defaultPPOpts
                 , rwJVMTrans = jvmTrans
                 , rwPrimsAvail = mempty

src/SAWScript/Builtins.hs

@@ -1560,14 +1560,18 @@ ensureMonadicTerm sc t
       False -> monadifyTypedTerm sc t
 ensureMonadicTerm sc t = monadifyTypedTerm sc t
 
+-- | Run Mr Solver with the given debug level to prove that the first term
+-- refines the second
 mrSolver :: SharedContext -> Int -> TypedTerm -> TypedTerm -> TopLevel Bool
 mrSolver sc dlvl t1 t2 =
-  do m1 <- ttTerm <$> ensureMonadicTerm sc t1
+  do rw <- get
+     m1 <- ttTerm <$> ensureMonadicTerm sc t1
      m2 <- ttTerm <$> ensureMonadicTerm sc t2
-     res <- liftIO $ Prover.askMRSolver sc dlvl Nothing m1 m2
+     let env = rwMRSolverEnv rw
+     res <- liftIO $ Prover.askMRSolver sc dlvl env Nothing m1 m2
      case res of
-       Just err -> io (putStrLn $ Prover.showMRFailure err) >> return False
-       Nothing -> return True
+       Left err -> io (putStrLn $ Prover.showMRFailure err) >> return False
+       Right env' -> put (rw { rwMRSolverEnv = env' }) >> return True
 
 setMonadification :: SharedContext -> String -> String -> TopLevel ()
 setMonadification sc cry_str saw_str =

src/SAWScript/Interpreter.hs

@@ -67,6 +67,7 @@ import SAWScript.Value
 import SAWScript.Proof (newTheoremDB)
 import SAWScript.Prover.Rewrite(basic_ss)
 import SAWScript.Prover.Exporter
+import SAWScript.Prover.MRSolver (emptyMREnv)
 import Verifier.SAW.Conversion
 --import Verifier.SAW.PrettySExp
 import Verifier.SAW.Prim (rethrowEvalError)
@@ -474,6 +475,7 @@ buildTopLevelEnv proxy opts =
                    , rwDocs       = primDocEnv primsAvail
                    , rwCryptol    = ce0
                    , rwMonadify   = Monadify.defaultMonEnv
+                   , rwMRSolverEnv = emptyMREnv
                    , rwProofs     = []
                    , rwPPOpts     = SAWScript.Value.defaultPPOpts
                    , rwJVMTrans   = jvmTrans