Merge pull request #1689 from GaloisInc/rwd/goal-sequents

Goal sequents

CHANGES.md

@@ -64,6 +64,28 @@
   of them, or if different tactics are needed for different subgoals.
   Currently, this option only applies to LLVM verifications.
 
+* Experimental interactive features. Using the new `subshell`
+  and `proof_subshell` commands, a user can regain a command-line
+  interface in the middle of a running script for experimentation
+  and exploration purposes. In addition `callcc` and `checkpoint`
+  allow the user to have more flexibility with restoring prior states
+  and executing the remaining context of a proof in such an
+  interactive session.
+
+* A significant overhaul of the SAW proof and tactics system.  Under
+  the hood, tactics now manipulate _sequents_ instead of just
+  propositions. This allows more the user to specify more precise goal
+  rearrangements, and provides a much nicer interface for proof
+  exploration (especially with the new `proof_subshell`). There are a
+  variety of new tactics that provide the user with control over proof
+  steps that is similar to that found in an interactive theorem prover.
+  Proofs that do not make use of the new experimental tactics should
+  see no substantive changes, so this is expected to be a highly
+  backward-compatible change.
+
+* The experimental and rarely-used `goal_assume` tactic has been
+  removed. The use case it was targeting is better solved via sequents.
+
 # Version 0.9
 
 ## New Features

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-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v

@@ -172,6 +172,22 @@ Instance Inhabited_nat : Inhabited nat :=
 Global Hint Resolve (0%nat : nat) : inh.
 Global Hint Resolve (0%nat : Nat) : inh.
 
+Definition IsLeNat := @le.
+Definition IsLeNat_base (n:Nat) : IsLeNat n n := le_n n.
+Definition IsLeNat_succ (n m:Nat) : IsLeNat n m -> IsLeNat n (S m) := le_S n m.
+
+Definition IsLeNat__rec
+  (n : Nat)
+  (p : forall (x : Nat), IsLeNat n x -> Prop)
+  (Hbase : p n (IsLeNat_base n))
+  (Hstep : forall (x : Nat) (H : IsLeNat n x), p x H -> p (S x) (IsLeNat_succ n x H))
+  : forall (m : Nat) (Hm : IsLeNat n m), p m Hm :=
+  fix rec (m:Nat) (Hm : IsLeNat n m) {struct Hm} : p m Hm :=
+            match Hm as Hm' in le _ m' return p m' Hm' with
+            | le_n _ => Hbase
+            | le_S _ m H => Hstep m H (rec m H)
+            end.
+
 (* Definition minNat := Nat.min. *)
 
 Definition uncurry (a b c : Type) (f : a -> b -> c) (p : a * (b * unit)) : c  :=

saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs

@@ -302,6 +302,14 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("Refl",    mapsTo sawDefinitionsModule "Refl")
   ]
 
+  -- Nat le
+  ++
+  [ ("IsLeNat"     , mapsTo sawDefinitionsModule "IsLeNat")
+  , ("IsLeNat__rec", mapsTo sawDefinitionsModule "IsLeNat__rec")
+  , ("IsLeNat_base", mapsTo sawDefinitionsModule "IsLeNat_base")
+  , ("IsLeNat_succ", mapsTo sawDefinitionsModule "IsLeNat_succ")
+  ]
+
   -- Strings
   ++
   [ ("String", mapsTo sawDefinitionsModule "String")

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,117 @@ 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 (vars, v)
-       _ -> fail $ "w4Solve: non-boolean result type. " ++ show bval
+       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) -- NB, boundFOTs will construct these lists to be the same length
+     bval <- w4SolveBasic sym sc mempty varMap' ref uninterp g
+     case bval of
+       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
+
+-- | Given a list of external constants with first-order types,
+--   descend in to the structure of those types (as needed) and construct
+--   corresponding What4 bound variables so we can bind them using
+--   a forall quantifier. At the same time construct @SValue@s containing
+--   those variables suitable for passing to the term evaluator as substituions
+--   for the given @ExtCns@ values. The length of the @SValue@ list returned
+--   will match the list of the input @ExtCns@ list, but the list of What4
+--   @BoundVar@s might not.
+--
+--   This procedure it capable of handling most first-order types, execpt
+--   that Array types must have base types as index and result types rather
+--   than more general first-order types. (TODO? should we actually restrict the
+--   @FirstOrderType@ in the same way?)
+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 n FOTBit ->
+         case somePosNat n of
+           Nothing -> -- n == 0
+             return (VWord ZBV)
+           Just (Some (PosNat nr)) ->
+             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)
+
+         | otherwise -> 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
 
@@ -1947,6 +2027,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