Induction and first-order assertions

intTests/test_univ_assert/README

@@ -0,0 +1,4 @@
+This is a test of the capability to assert first-order statements
+to the solver. Here, we are reasoning abstractly over about
+generic properties of addition and multiplication (essentially,
+some of the ring axioms).

intTests/test_univ_assert/test.saw

@@ -0,0 +1,33 @@
+enable_experimental;
+
+let {{
+  type vec_t = [384]
+  mul : vec_t -> vec_t -> vec_t
+  mul x y = undefined // this would be e.g. multiplication modulo p
+  add : vec_t -> vec_t -> vec_t
+  add x y = undefined
+
+  term1 x y z1 z2 z3 = add (mul (add (mul (add (mul x y) z1) x) z2) x) z3
+  term2 x y z1 z2 z3 = add (mul y (mul x (mul x x))) (add (mul z1 (mul x x)) (add (mul z2 x) z3))
+}};
+
+// Assume some of the ring axioms
+lemmas <- for
+  [ {{ \x y -> mul x y == mul y x }}
+  , {{ \x y -> add x y == add y x }}
+  , {{ \x y z -> mul (mul x y) z == mul x (mul y z) }}
+  , {{ \x y z -> add (add x y) z == add x (add y z) }}
+  , {{ \x y z -> mul (add x y) z == add (mul x z) (mul y z) }}
+  ]
+  (prove_print assume_unsat);
+
+// Use those axioms to prove a nonmtrivial equality
+thm <- prove_print
+  (do {
+    unfolding ["term1","term2"];
+    for lemmas goal_insert;
+    w4_unint_z3 ["mul","add"];
+  })
+  {{ \x y z1 z2 z3 -> term1 x y z1 z2 z3 == term2 x y z1 z2 z3 }};
+
+print thm;

intTests/test_univ_assert/test.sh

@@ -0,0 +1 @@
+$SAW test.saw

saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

@@ -664,8 +664,7 @@ mkUninterpreted k args nm = svUninterpreted k nm' Nothing args
 
 sbvSATQuery :: SharedContext -> Map Ident SPrim -> SATQuery -> IO ([Labeler], [ExtCns Term], Symbolic SBool)
 sbvSATQuery sc addlPrims query =
-  do true <- liftIO (scBool sc True)
-     t <- liftIO (foldM (scAnd sc) true (satAsserts query))
+  do t <- liftIO (satQueryAsTerm sc query)
      let qvars = Map.toList (satVariables query)
      let unintSet = satUninterp query
      let ecVars (ec, fot) = newVars (Text.unpack (toShortName (ecName ec))) fot

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -96,7 +96,7 @@ import Verifier.SAW.TypedAST (FieldName, ModuleMap, toShortName, ctorPrimName, i
 import qualified What4.Expr.Builder as B
 import           What4.Expr.GroundEval
 import           What4.Interface(SymExpr,Pred,SymInteger, IsExpr,
-                                 IsExprBuilder,IsSymExprBuilder)
+                                 IsExprBuilder,IsSymExprBuilder, BoundVar)
 import qualified What4.Interface as W
 import           What4.BaseTypes
 import qualified What4.SWord as SW
@@ -983,17 +983,101 @@ w4Solve :: forall sym.
   sym ->
   SharedContext ->
   SATQuery ->
-  IO ([(ExtCns Term, (Labeler sym, SValue sym))], SBool sym)
+  IO ([(ExtCns Term, (Labeler sym, SValue sym))], [SBool sym])
 w4Solve sym sc satq =
-  do t <- satQueryAsTerm sc satq
-     let varList  = Map.toList (satVariables satq)
+  do let varList  = Map.toList (satVariables satq)
      vars <- evalStateT (traverse (traverse (newVarFOT sym)) varList) 0
      let varMap   = Map.fromList [ (ecVarIndex ec, v) | (ec, (_,v)) <- vars ]
      ref <- newIORef Map.empty
-     bval <- w4SolveBasic sym sc mempty varMap ref (satUninterp satq) t
+
+     bvals <- mapM (w4SolveAssert sym sc varMap ref (satUninterp satq)) (satAsserts satq)
+     return (vars, bvals)
+
+
+w4SolveAssert :: forall sym.
+  IsSymExprBuilder sym =>
+  sym ->
+  SharedContext ->
+  Map VarIndex (SValue sym) {- ^ bindings for ExtCns values -} ->
+  IORef (SymFnCache sym) {- ^ cache for uninterpreted function symbols -} ->
+  Set VarIndex {- ^ variables to hold uninterpreted -} ->
+  SATAssert ->
+  IO (SBool sym)
+w4SolveAssert sym sc varMap ref uninterp (BoolAssert x) =
+  do bval <- w4SolveBasic sym sc mempty varMap ref uninterp x
+     case bval of
+       VBool v -> return v
+       _ -> fail $ "w4SolveAssert: non-boolean result type. " ++ show bval
+
+w4SolveAssert sym sc varMap ref uninterp (UniversalAssert vars hyps concl) =
+  do g <- case hyps of
+            [] -> return concl
+            _  -> do h <- scAndList sc hyps
+                     scImplies sc h concl
+     (svals,bndvars) <- boundFOTs sym vars
+     let varMap' = foldl (\m ((ec,_fot), sval) -> Map.insert (ecVarIndex ec) sval m)
+                         varMap
+                         (zip vars svals)
+     bval <- w4SolveBasic sym sc mempty varMap' ref uninterp g
      case bval of
-       VBool v -> return (vars, v)
-       _ -> fail $ "w4Solve: non-boolean result type. " ++ show bval
+       VBool v ->
+         do final <- foldM (\p (Some bndvar) -> W.forallPred sym bndvar p) v bndvars
+            return final
+
+       _ -> fail $ "w4SolveAssert: non-boolean result type. " ++ show bval
+
+boundFOTs :: forall sym.
+  IsSymExprBuilder sym =>
+  sym ->
+  [(ExtCns Term, FirstOrderType)] ->
+  IO ([SValue sym], [Some (BoundVar sym)])
+boundFOTs sym vars =
+  do (svals,(bndvars,_)) <- runStateT (mapM (uncurry handleVar) vars) ([], 0)
+     return (svals, bndvars)
+
+ where
+   freshBnd :: ExtCns Term -> W.BaseTypeRepr tp -> StateT ([Some (BoundVar sym)],Integer) IO (SymExpr sym tp)
+   freshBnd ec tpr =
+     do (vs,n) <- get
+        let nm = Text.unpack (toShortName (ecName ec)) ++ "." ++ show n
+        bvar <- lift (W.freshBoundVar sym (W.safeSymbol nm) tpr)
+        put (Some bvar : vs, n+1)
+        return (W.varExpr sym bvar)
+
+   handleVar :: ExtCns Term -> FirstOrderType -> StateT ([Some (BoundVar sym)], Integer) IO (SValue sym)
+   handleVar ec fot =
+     case fot of
+       FOTBit -> VBool <$> freshBnd ec BaseBoolRepr
+       FOTInt -> VInt  <$> freshBnd ec BaseIntegerRepr
+       FOTIntMod m -> VIntMod m <$> freshBnd ec BaseIntegerRepr
+       FOTVec 0 FOTBit -> return (VWord ZBV)
+       FOTVec n FOTBit
+         | Just (Some (PosNat nr)) <- somePosNat n ->
+         VWord . DBV <$> freshBnd ec (BaseBVRepr nr)
+
+       FOTVec n tp -> -- NB, not Bit
+         do vs  <- V.replicateM (fromIntegral n) (handleVar ec tp)
+            vs' <- traverse (return . ready) vs
+            return (VVector vs')
+
+       FOTRec tm ->
+         do vs  <- traverse (handleVar ec) tm
+            vs' <- traverse (return . ready) vs
+            return (vRecord vs')
+
+       FOTTuple ts ->
+         do vs  <- traverse (handleVar ec) ts
+            vs' <- traverse (return . ready) vs
+            return (vTuple vs')
+
+       FOTArray idx res
+         | Just (Some idx_repr) <- fotToBaseType idx
+         , Just (Some res_repr) <- fotToBaseType res
+
+         -> VArray . SArray <$> freshBnd ec (BaseArrayRepr (Ctx.Empty Ctx.:> idx_repr) res_repr)
+
+       _ -> fail ("boundFOTs: cannot handle " ++ show fot)
+
 
 --
 -- Pull out argument types until bottoming out at a non-Pi type

saw-core/prelude/Prelude.sawcore

@@ -797,6 +797,15 @@ data IsLeNat (n:Nat) : Nat -> Prop where {
 IsLtNat : Nat -> Nat -> Prop;
 IsLtNat m n = IsLeNat (Succ m) n;
 
+-- | Restate the recursor on IsLeNat
+IsLeNat__rec :
+  (n  : Nat) ->
+  (p  : (x : Nat) -> IsLeNat n x -> Prop) ->
+  (Hbase : p n (IsLeNat_base n)) ->
+  (Hstep : (x : Nat) -> (H : IsLeNat n x) -> p x H -> p (Succ x) (IsLeNat_succ n x H)) ->
+  (m : Nat) -> (Hm : IsLeNat n m) -> p m Hm;
+IsLeNat__rec n p Hbase Hstep m Hm = IsLeNat#rec n p Hbase Hstep m Hm;
+
 -- | Test if m < n or n <= m
 -- FIXME: implement this!
 primitive natCompareLe : (m n : Nat) -> Either (IsLtNat m n) (IsLeNat n m);
@@ -936,6 +945,77 @@ if0Nat a n x y = natCase (\ (_:Nat) -> a) x (\ (_:Nat) -> y) n;
 -- and the number of times to multiply.
 primitive expByNat : (a:sort 0) -> a -> (a -> a -> a) -> a -> Nat -> a;
 
+
+-- | LeNat is transitive
+IsLeNat_transitive :
+  (n m o:Nat) ->
+  IsLeNat n m ->
+  IsLeNat m o ->
+  IsLeNat n o;
+IsLeNat_transitive n m o Hnm Hmo =
+  IsLeNat__rec m
+    (\ (x:Nat) -> \(H:IsLeNat m x) -> IsLeNat n x)
+    Hnm
+    (\ (x:Nat) -> \ (H1:IsLeNat m x) -> \ (H2:IsLeNat n x) -> IsLeNat_succ n x H2)
+  o Hmo;
+
+-- No Nat is strictly less than zero
+IsLtNat_Zero_absurd :
+  (p:Prop) ->
+  (m:Nat) ->
+  IsLtNat m Zero ->
+  p;
+IsLtNat_Zero_absurd p m HSmZ =
+  IsLeNat__rec (Succ m)
+    ( \ (x : Nat) -> \ (H:IsLeNat (Succ m) x) -> if0Nat Prop x p TrueProp)
+    TrueI
+    ( \ (x : Nat) -> \ (H1:IsLeNat (Succ m) x) -> \ (H2 : if0Nat Prop x p TrueProp) -> TrueI)
+    Zero HSmZ;
+
+IsLeNat_SuccSucc :
+  (n m:Nat) ->
+  IsLeNat (Succ n) (Succ m) ->
+  IsLeNat n m;
+IsLeNat_SuccSucc n m HSS =
+  IsLeNat__rec (Succ n)
+    ( \ (x : Nat) -> \ (H:IsLeNat (Succ n) x) -> IsLeNat n (pred x))
+    (IsLeNat_base n)
+    (Nat__rec
+      ( \ (x : Nat) -> IsLeNat (Succ n) x -> IsLeNat n (pred x) -> IsLeNat n x)
+      ( \ (H1 : IsLeNat (Succ n) Zero) -> \ (H2 : IsLeNat n (pred Zero)) -> H2)
+      ( \ (x : Nat) ->
+        \ (Hind : IsLeNat (Succ n) x -> IsLeNat n (pred x) -> IsLeNat n x) ->
+        \ (H1 : IsLeNat (Succ n) (Succ x)) ->
+	\ (H2 : IsLeNat n (pred (Succ x))) ->
+	IsLeNat_succ n x H2)
+    )
+  (Succ m) HSS;
+
+-- | The complete induction principle on natural numbers
+Nat_complete_induction :
+  (p : Nat -> Prop) ->
+  ((n : Nat) -> ((m : Nat) -> IsLtNat m n -> p m) -> p n) ->
+  (n : Nat) -> p n;
+
+Nat_complete_induction p f n0 =
+  Nat__rec ( \ (n:Nat) -> (m:Nat) -> IsLeNat m n -> p m)
+    (\ (n:Nat) ->
+     \ (Hn:IsLeNat n 0) ->
+     f n (\ (m:Nat) -> \ (Hm : IsLeNat (Succ m) n) ->
+            IsLtNat_Zero_absurd (p m) m (IsLeNat_transitive (Succ m) n 0 Hm Hn))
+    )
+   (\ (n:Nat) ->
+     \ (Hind : (m:Nat) -> IsLeNat m n -> p m) ->
+     \ (r:Nat) ->
+     \ (Hr:IsLeNat r (Succ n)) ->
+       f r (\ (m:Nat) -> \ (Hm: IsLeNat (Succ m) r) ->
+             Hind m (IsLeNat_SuccSucc m n (IsLeNat_transitive (Succ m) r (Succ n) Hm Hr)))
+    )
+    n0 n0 (IsLeNat_base n0);
+
+
+
+
 --------------------------------------------------------------------------------
 -- Operations on string values
 
@@ -1764,7 +1844,6 @@ primitive updSliceWithProof : (a : sort 0) -> (n off len : Nat) ->
                               IsLeNat (addNat off len) n ->
                               Vec n a -> Vec len a -> Vec n a;
 
-
 --------------------------------------------------------------------------------
 -- Vectors indexed by bitvectors
 
@@ -1947,6 +2026,29 @@ appendBVVec n len1 len2 a v1 v2 =
          (Refl Bool (bvult n i len1)));
 
 
+-- | The complete induction principle on bitvectors
+BV_complete_induction :
+  (w: Nat) ->
+  (p: Vec w Bool -> Prop) ->
+  ((x : Vec w Bool) -> ((y: Vec w Bool) -> is_bvult w y x -> p y) -> p x) ->
+  (x : Vec w Bool) -> p x;
+BV_complete_induction w p f x0 =
+  Nat_complete_induction
+    (\ (n:Nat) -> (x:Vec w Bool) -> IsLeNat (bvToNat w x) n -> p x)
+    (\ (n:Nat) ->
+     \ (Hind : (m : Nat) -> (Hm : IsLtNat m n) -> (y : Vec w Bool) ->
+               (Hy : IsLeNat (bvToNat w y) m) -> p y) ->
+     \ (x : Vec w Bool) ->
+     \ (Hx : IsLeNat (bvToNat w x) n) ->
+       f x (\ (y:Vec w Bool) -> \ (Hult : is_bvult w y x) ->
+              Hind (bvToNat w y)
+	        (IsLeNat_transitive (Succ (bvToNat w y)) (bvToNat w x) n (bvultToIsLtNat w y x Hult) Hx)
+	        y (IsLeNat_base (bvToNat w y))
+	   )
+    )
+    (bvToNat w x0) x0 (IsLeNat_base (bvToNat w x0));
+
+
 --------------------------------------------------------------------------------
 -- Iso-recursive types
 

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

@@ -1,10 +1,10 @@
 module Verifier.SAW.SATQuery
 ( SATQuery(..)
 , SATResult(..)
+, SATAssert(..)
 , satQueryAsTerm
 ) where
 
-import Control.Monad (foldM)
 import Data.Map (Map)
 import Data.Set (Set)
 
@@ -42,13 +42,19 @@ data SATQuery =
       --   the solver. Models will not report values
       --   for uninterpreted values.
 
-  , satAsserts   :: [Term]
+  , satAsserts   :: [SATAssert]
       -- ^ A collection of assertions.  These should
       --   all be terms of type @Bool@.  The overall
       --   query should be understood as the conjunction
       --   of these terms.
   }
--- TODO, allow first-order propositions in addition to Boolean terms.
+
+data SATAssert
+   = BoolAssert Term -- ^ A boolean term to be asserted
+   | UniversalAssert [(ExtCns Term, FirstOrderType)] [Term] Term
+          -- ^ A univesally-quantified assertion, consisting of a
+          --   collection of first-order variables, a sequence
+          --   of boolean hypotheses, and a boolean conclusion
 
 -- | The result of a sat query.  In the event a model is found,
 --   return a mapping from the @ExtCns@ variables to values.
@@ -59,10 +65,20 @@ data SATResult
 
 -- | Compute the conjunction of all the assertions
 --   in this SAT query as a single term of type Bool.
+--
+--   This method of reducing a sat query to a boolean
+--   cannot be used for univerally-quantified assertions.
 satQueryAsTerm :: SharedContext -> SATQuery -> IO Term
 satQueryAsTerm sc satq =
   case satAsserts satq of
          [] -> scBool sc True
-         (x:xs) -> foldM (scAnd sc) x xs
--- TODO, we may have to rethink this function
---  once we allow first-order statements.
+         (BoolAssert x:xs) -> loop x xs
+         (UniversalAssert{} : _) -> univFail
+ where
+   univFail = fail "satQueryAsTerm : Solver backend cannot handle universally-quantifed assertions"
+
+   loop x [] = return x
+   loop x (BoolAssert y:xs) = 
+     do x' <- scAnd sc x y
+        loop x' xs
+   loop _ (UniversalAssert{} : _) = univFail

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

@@ -168,6 +168,8 @@ module Verifier.SAW.SharedTerm
   , scXor
   , scBoolEq
   , scIte
+  , scAndList
+  , scOrList
   -- *** Natural numbers
   , scNat
   , scNatType
@@ -1702,6 +1704,25 @@ scIte :: SharedContext -> Term -> Term ->
          Term -> Term -> IO Term
 scIte sc t b x y = scGlobalApply sc "Prelude.ite" [t, b, x, y]
 
+-- | Build a conjunction from a list of boolean terms.
+scAndList :: SharedContext -> [Term] -> IO Term
+scAndList sc = conj . filter nontrivial
+  where
+    nontrivial x = asBool x /= Just True
+    conj [] = scBool sc True
+    conj [x] = return x
+    conj (x : xs) = foldM (scAnd sc) x xs
+
+-- | Build a conjunction from a list of boolean terms.
+scOrList :: SharedContext -> [Term] -> IO Term
+scOrList sc = disj . filter nontrivial
+  where
+    nontrivial x = asBool x /= Just False
+    disj [] = scBool sc False
+    disj [x] = return x
+    disj (x : xs) = foldM (scOr sc) x xs
+
+
 -- | Create a term applying @Prelude.append@ to two vectors.
 --
 -- > append : (m n : Nat) -> (e : sort 0) -> Vec m e -> Vec n e -> Vec (addNat m n) e;