Update to latest sbv.

* We're now back on Levent's sbv (:tada:) * When SBV 8.1 is released we can switch to it to be back on a hackage release * We now add names to all allocations to make debugging much easier * The quantified variables issue that's been haunting us since forever is finally fixed (see LeventErkok/sbv#459) * We now need to add `Ord` constraints in some places due to sbv changes.
kadena-io · Mar 4, 2019 · 2459422 · 2459422
1 parent 0b799ae
commit 2459422
Show file tree

Hide file tree

Showing 9 changed files with 96 additions and 69 deletions.
diff --git a/default.nix b/default.nix
@@ -88,12 +88,12 @@ in
             hlint = self.callHackage "hlint" "2.0.14" {};
             # hoogle = self.callHackage "hoogle" "5.0.15" {};
 
-            # sbv with a patch to disable "unsupported query call" until it's fixed upstream
+            # this is pre-sbv-8.1 (switch when it's released)
             sbv = dontCheck (self.callCabal2nix "sbv" (pkgs.fetchFromGitHub {
-              owner = "joelburget";
+              owner = "LeventErkok";
               repo = "sbv";
-              rev = "25d9357ff8eaac697eb6fde96598d7beb587b4e9";
-              sha256 = "0i0ajrw8j9hc208hizi4rnj5giqhbawjfgdbacswwfvgfqvvb69z";
+              rev = "68375576f87d17a2da759c56f7147f4e559471a2";
+              sha256 = "11qmgc8jnsx1m2hy3x28ihl941ik4wsdpj0bkbsz226zncad13dp";
             }) {});
 
             # need crackNum 2.3

diff --git a/src/Pact/Analyze/Alloc.hs b/src/Pact/Analyze/Alloc.hs
@@ -33,33 +33,33 @@ import           Pact.Analyze.Types          (Concrete, S, SingI (sing), SingTy,
 -- is permitted.
 class Monad m => MonadAlloc m where
 
-  singForAll :: SingTy a -> m (S (Concrete a)) -- ^ universally quantified
-  singExists :: SingTy a -> m (S (Concrete a)) -- ^ existentially quantified
-  singFree   :: SingTy a -> m (S (Concrete a)) -- ^ quantified per the context of sat vs prove
+  singForAll :: String -> SingTy a -> m (S (Concrete a)) -- ^ universally quantified
+  singExists :: String -> SingTy a -> m (S (Concrete a)) -- ^ existentially quantified
+  singFree   :: String -> SingTy a -> m (S (Concrete a)) -- ^ quantified per the context of sat vs prove
 
   default singForAll
     :: (MonadTrans t, MonadAlloc m', m ~ t m')
-    => SingTy a -> m (S (Concrete a))
-  singForAll ty = lift (singForAll ty)
+    => String -> SingTy a -> m (S (Concrete a))
+  singForAll name ty = lift (singForAll name ty)
 
   default singExists
     :: (MonadTrans t, MonadAlloc m', m ~ t m')
-    => SingTy a -> m (S (Concrete a))
-  singExists ty = lift (singExists ty)
+    => String -> SingTy a -> m (S (Concrete a))
+  singExists name ty = lift (singExists name ty)
 
   default singFree
     :: (MonadTrans t, MonadAlloc m', m ~ t m')
-    => SingTy a -> m (S (Concrete a))
-  singFree   = lift . singFree
+    => String -> SingTy a -> m (S (Concrete a))
+  singFree name  = lift . singFree name
 
-forAll :: forall a m. (MonadAlloc m, SingI a) => m (S (Concrete a))
-forAll = singForAll (sing @a)
+forAll :: forall a m. (MonadAlloc m, SingI a) => String -> m (S (Concrete a))
+forAll name = singForAll name (sing @a)
 
-exists :: forall a m. (MonadAlloc m, SingI a) => m (S (Concrete a))
-exists = singExists (sing @a)
+exists :: forall a m. (MonadAlloc m, SingI a) => String -> m (S (Concrete a))
+exists name = singExists name (sing @a)
 
-free :: forall a m. (MonadAlloc m, SingI a) => m (S (Concrete a))
-free = singFree (sing @a)
+free :: forall a m. (MonadAlloc m, SingI a) => String -> m (S (Concrete a))
+free name = singFree name (sing @a)
 
 instance MonadAlloc m             => MonadAlloc (ExceptT e m)
 instance MonadAlloc m             => MonadAlloc (MaybeT m)
@@ -78,6 +78,6 @@ newtype Alloc a = Alloc { runAlloc :: Symbolic a }
   deriving (Functor, Applicative, Monad)
 
 instance MonadAlloc Alloc where
-  singForAll ty = Alloc $ withSymVal ty $ sansProv <$> SBV.forall_
-  singExists ty = Alloc $ withSymVal ty $ sansProv <$> SBV.exists_
-  singFree   ty = Alloc $ withSymVal ty $ sansProv <$> SBV.free_
+  singForAll name ty = Alloc $ withSymVal ty $ sansProv <$> SBV.forall name
+  singExists name ty = Alloc $ withSymVal ty $ sansProv <$> SBV.exists name
+  singFree   name ty = Alloc $ withSymVal ty $ sansProv <$> SBV.free   name
diff --git a/src/Pact/Analyze/Check.hs b/src/Pact/Analyze/Check.hs
@@ -302,7 +302,7 @@ verifyFunctionInvariants' modName funName funInfo tables caps pactArgs body = ru
     ExceptT $ catchingExceptions $ runSymbolic $ runExceptT $ do
       lift $ SBV.setTimeOut 1000 -- one second
       modelArgs' <- lift $ runAlloc $ allocArgs args
-      tags <- lift $ runAlloc $ allocModelTags modelArgs' (Located funInfo tm) graph
+      tags       <- lift $ runAlloc $ allocModelTags modelArgs' (Located funInfo tm) graph
       let rootPath = _egRootPath graph
       resultsTable <- withExceptT analyzeToCheckFailure $
         runInvariantAnalysis modName tables caps (analysisArgs modelArgs') tm
@@ -333,7 +333,7 @@ verifyFunctionInvariants' modName funName funInfo tables caps pactArgs body = ru
     goal = Validation
 
     config :: SBV.SMTConfig
-    config = SBV.z3 -- { SBVI.verbose = True }
+    config = SBV.z3 { SBVI.allowQuantifiedQueries = True } -- , SBVI.verbose = True }
 
     -- Discharges impure 'SBVException's from sbv.
     catchingExceptions
@@ -363,33 +363,35 @@ verifyFunctionProperty modName funName funInfo tables caps pactArgs body (Locate
     ExceptT $ catchingExceptions $ runSymbolic $ runExceptT $ do
       lift $ SBV.setTimeOut 1000 -- one second
       modelArgs' <- lift $ runAlloc $ allocArgs args
-      tags <- lift $ runAlloc $ allocModelTags modelArgs' (Located funInfo tm) graph
+      tags       <- lift $ runAlloc $ allocModelTags modelArgs' (Located funInfo tm) graph
       let rootPath = _egRootPath graph
       AnalysisResult _querySucceeds prop ksProvs
         <- withExceptT analyzeToCheckFailure $
           runPropertyAnalysis modName check tables caps
             (analysisArgs modelArgs') tm rootPath tags funInfo
 
+      let model = Model modelArgs' tags ksProvs graph
+
       -- TODO: bring back the query success check when we've resolved the SBV
       -- query / quantified variables issue:
       -- https://github.com/LeventErkok/sbv/issues/407
       --
       -- _ <- hoist SBV.query $ do
-      --   void $ lift $ SBV.constrain $ SBV.bnot $ successBool querySucceeds
-      --   withExceptT (smtToQueryFailure (getInfo check)) $
+      --   void $ lift $ SBV.constrain $ SBV.sNot $ successBool querySucceeds
+      --   withExceptT (smtToQueryFailure propInfo) $
       --     resultQuery Validation model
 
       void $ lift $ SBV.output prop
       hoist SBV.query $
         withExceptT (smtToCheckFailure propInfo) $
-          resultQuery goal $ Model modelArgs' tags ksProvs graph
+          resultQuery goal model
 
   where
     goal :: Goal
     goal = checkGoal check
 
     config :: SBV.SMTConfig
-    config = SBV.z3 -- { SBVI.verbose = True }
+    config = SBV.z3 { SBVI.allowQuantifiedQueries = True } -- , SBVI.verbose = True }
 
     -- Discharges impure 'SBVException's from sbv.
     catchingExceptions
@@ -400,7 +402,7 @@ verifyFunctionProperty modName funName funInfo tables caps pactArgs body (Locate
 
     runSymbolic :: Symbolic a -> IO a
     runSymbolic = fmap fst .
-      SBVI.runSymbolic (SBVI.SMTMode SBVI.ISetup (goal == Satisfaction) config)
+      SBVI.runSymbolic (SBVI.SMTMode SBVI.QueryExternal SBVI.ISetup (goal == Satisfaction) config)
 
 moduleTables
   :: HM.HashMap ModuleName ModuleData -- ^ all loaded modules
@@ -855,5 +857,6 @@ verifyCheck moduleData funName check = do
   tables <- withExceptT ModuleParseFailure $ moduleTables modules moduleData
   case moduleFun moduleData funName of
     Just funRef -> ExceptT $
-      Right . head <$> verifyFunctionProps moduleName tables caps funRef funName [Located info check]
+      Right . head <$> verifyFunctionProps moduleName tables caps funRef funName
+        [Located info check]
     Nothing -> pure $ Left $ CheckFailure info $ NotAFunction funName
diff --git a/src/Pact/Analyze/Eval/Core.hs b/src/Pact/Analyze/Eval/Core.hs
@@ -99,7 +99,7 @@ evalComparisonOp
   -> TermOf m a
   -> TermOf m a
   -> m (S Bool)
-evalComparisonOp ty op xT yT = do
+evalComparisonOp ty op xT yT = withOrd ty $ do
   x <- withSing ty $ eval xT
   y <- withSing ty $ eval yT
   let f :: SymVal (Concrete a) => SBV Bool
@@ -254,7 +254,7 @@ evalCore (ListConcat ty p1 p2) = withSymVal ty $ withSing ty $ do
 evalCore (ListReverse ty l) = withSymVal ty $ withSing ty $ do
   S prov l' <- eval l
   pure $ S prov $ breverse listBound l'
-evalCore (ListSort ty l) = withSymVal ty $ withSing ty $ do
+evalCore (ListSort ty l) = withSymVal ty $ withSing ty $ withOrd ty $ do
   S prov l' <- eval l
   pure $ S prov $ bsort listBound l'
 evalCore (MakeList ty i a) = withSymVal ty $ withSing ty $ do

diff --git a/src/Pact/Analyze/Eval/Prop.hs b/src/Pact/Analyze/Eval/Prop.hs
@@ -115,8 +115,8 @@ evalPropSpecific :: PropSpecific a -> Query (S (Concrete a))
 evalPropSpecific Success = view $ qeAnalyzeState.succeeds
 evalPropSpecific Abort   = sNot <$> evalPropSpecific Success
 evalPropSpecific Result  = aval (pure ... mkS) =<< view qeAnalyzeResult
-evalPropSpecific (Forall vid _name (EType (ty :: Types.SingTy ty)) p) = do
-  var <- singForAll ty
+evalPropSpecific (Forall vid name (EType (ty :: Types.SingTy ty)) p) = do
+  var <- singForAll ("forall_" ++ T.unpack name) ty
   local (scope.at vid ?~ mkAVal var) $ evalProp p
 evalPropSpecific (Forall vid _name QTable prop) = do
   TableMap tables <- view (analyzeEnv . invariants)
@@ -129,8 +129,8 @@ evalPropSpecific (Forall vid _name (QColumnOf tabName) prop) = do
     let colName' = ColumnName $ T.unpack colName
     in local (qeColumnScope . at vid ?~ colName') (evalProp prop)
   pure $ foldr (.&&) sTrue bools
-evalPropSpecific (Exists vid _name (EType (ty :: Types.SingTy ty)) p) = do
-  var <- singExists ty
+evalPropSpecific (Exists vid name (EType (ty :: Types.SingTy ty)) p) = do
+  var <- singExists ("exists_" ++ T.unpack name) ty
   local (scope.at vid ?~ mkAVal var) $ evalProp p
 evalPropSpecific (Exists vid _name QTable prop) = do
   TableMap tables <- view (analyzeEnv . invariants)

diff --git a/src/Pact/Analyze/Model/Tags.hs b/src/Pact/Analyze/Model/Tags.hs
@@ -30,7 +30,7 @@ import           Data.SBV             (SBV, SymVal)
 import qualified Data.SBV             as SBV
 import qualified Data.SBV.Control     as SBV
 import qualified Data.SBV.Internals   as SBVI
-import           Data.Text            (pack)
+import           Data.Text            (pack, unpack)
 import           Data.Traversable     (for)
 import           GHC.TypeLits         (symbolVal)
 
@@ -39,32 +39,36 @@ import qualified Pact.Types.Typecheck as TC
 import           Pact.Analyze.Alloc   (Alloc, free, singFree)
 import           Pact.Analyze.Types
 
-allocS :: forall a. SingI a => Alloc (S (Concrete a))
-allocS = free @a
+allocS :: forall a. SingI a => String -> Alloc (S (Concrete a))
+allocS name = free @a ("tag_" ++ name)
 
-allocSbv :: forall a. SingI a => Alloc (SBV (Concrete a))
-allocSbv = _sSbv <$> allocS @a
+allocSbv :: forall a. SingI a => String -> Alloc (SBV (Concrete a))
+allocSbv name = _sSbv <$> allocS @a name
 
 allocSchema :: SingList schema -> Alloc UObject
 allocSchema = fmap UObject . allocSchema' where
   allocSchema' = foldrSingList (pure Map.empty) $ \k ty m -> do
-    let ety = EType ty
-    val <- allocAVal ety
-    Map.insert (pack (symbolVal k)) (ety, val) <$> m
+    let ety  = EType ty
+        name = symbolVal k
+    val <- allocAVal name ety
+    Map.insert (pack name) (ety, val) <$> m
 
-allocAVal :: EType -> Alloc AVal
-allocAVal (EType ty) = mkAVal <$> singFree ty
+allocAVal :: String -> EType -> Alloc AVal
+allocAVal name (EType ty) = mkAVal <$> singFree name ty
 
-allocTVal :: EType -> Alloc TVal
-allocTVal ety = (ety,) <$> allocAVal ety
+allocTVal :: String -> EType -> Alloc TVal
+allocTVal name ety = (ety,) <$> allocAVal name ety
 
-allocForETerm :: ETerm -> Alloc TVal
-allocForETerm (existentialType -> ety) = allocTVal ety
+allocForETerm :: String -> ETerm -> Alloc TVal
+allocForETerm name (existentialType -> ety) = allocTVal name ety
+
+unmungedStr :: Unmunged -> String
+unmungedStr (Unmunged name) = unpack name
 
 allocArgs :: [Arg] -> Alloc (Map VarId (Located (Unmunged, TVal)))
 allocArgs args = fmap Map.fromList $ for args $ \(Arg nm vid node ety) -> do
   let info = node ^. TC.aId . TC.tiInfo
-  av <- allocAVal ety <&> _AVal._1 ?~ FromInput nm
+  av <- allocAVal (unmungedStr nm) ety <&> _AVal._1 ?~ FromInput nm
   pure (vid, Located info (nm, (ety, av)))
 
 allocModelTags
@@ -98,7 +102,8 @@ allocModelTags argsMap locatedTm graph = ModelTags
       for (toListOf (traverse._TracePushScope._3.traverse) events) $
         \(Located info (Binding vid nm _ ety)) ->
           case Map.lookup vid argsMap of
-            Nothing  -> allocTVal ety <&> \tv -> (vid, Located info (nm, tv))
+            Nothing  -> allocTVal ("binding_" ++ unmungedStr nm) ety <&>
+              \tv -> (vid, Located info (nm, tv))
             Just arg -> pure (vid, arg)
 
     allocAccesses
@@ -107,9 +112,9 @@ allocModelTags argsMap locatedTm graph = ModelTags
     allocAccesses p = fmap Map.fromList $
       for (toListOf (traverse.p) events) $
         \(ESchema schema, Located info tid) -> do
-          srk <- allocS @TyRowKey
+          srk <- allocS @TyRowKey "row_key"
           obj <- allocSchema schema
-          suc <- allocSbv @'TyBool
+          suc <- allocSbv @'TyBool "access_success"
           pure (tid, Located info (Access srk obj suc))
 
     allocReads :: Alloc (Map TagId (Located Access))
@@ -127,18 +132,20 @@ allocModelTags argsMap locatedTm graph = ModelTags
     allocAsserts :: Alloc (Map TagId (Located (SBV Bool)))
     allocAsserts = fmap Map.fromList $
       for (toListOf (traverse._TraceAssert._2) events) $ \(Located info tid) ->
-        (tid,) . Located info <$> allocSbv @'TyBool
+        (tid,) . Located info <$> allocSbv @'TyBool "assert"
 
     allocGEs :: Alloc (Map TagId (Located GuardEnforcement))
     allocGEs = fmap Map.fromList $
       for (toListOf (traverse._TraceGuard._2) events) $ \(Located info tid) ->
         (tid,) . Located info <$>
-          (GuardEnforcement <$> allocS @'TyGuard <*> allocSbv @'TyBool)
+          (GuardEnforcement
+            <$> allocS @'TyGuard "guard"
+            <*> allocSbv @'TyBool "guard_success")
 
     allocResult :: Alloc (TagId, Located TVal)
     allocResult = do
       let tid :: TagId = last $ toListOf (traverse._TracePopScope._3) events
-      fmap (tid,) $ sequence $ allocForETerm <$> locatedTm
+      fmap (tid,) $ sequence $ allocForETerm "result" <$> locatedTm
 
     -- NOTE: the root path we manually set to true. translation only emits the
     -- start of "subpaths" on either side of a conditional. the root path is
@@ -148,12 +155,12 @@ allocModelTags argsMap locatedTm graph = ModelTags
     allocPaths = do
       let rootPath = _egRootPath graph
           paths    = rootPath : toListOf (traverse._TraceSubpathStart) events
-      Map.fromList <$> for paths (\p -> (p,) <$> allocSbv @'TyBool)
+      Map.fromList <$> for paths (\p -> (p,) <$> allocSbv @'TyBool "path")
 
     allocReturns :: Alloc (Map TagId TVal)
     allocReturns = fmap Map.fromList $
       for (toListOf (traverse._TracePopScope) events) $ \(_, _, tid, ety) ->
-        (tid,) <$> allocTVal ety
+        (tid,) <$> allocTVal "trace_pop_scope" ety
 
 -- | Builds a new 'Model' by querying the SMT model to concretize the provided
 -- symbolic 'Model'.

diff --git a/src/Pact/Analyze/PrenexNormalize.hs b/src/Pact/Analyze/PrenexNormalize.hs
@@ -126,7 +126,7 @@ singFloat ty p = case p of
 
   -- - logical
   CoreProp (Logical AndOp [a, b]) -> PAnd <$> float a <*> float b
-  CoreProp (Logical OrOp [a, b]) -> POr  <$> float a <*> float b
+  CoreProp (Logical OrOp  [a, b]) -> POr  <$> float a <*> float b
   CoreProp (Logical NotOp [a]) -> bimap (fmap flipQuantifier) PNot (float a)
   CoreProp (Logical _ _) -> error ("ill-defined logical op: " ++ showTm p)
   CoreProp (AndQ ty' f g a) -> CoreProp <$>

diff --git a/src/Pact/Analyze/Types/Shared.hs b/src/Pact/Analyze/Types/Shared.hs
@@ -361,7 +361,7 @@ instance (SymVal a) => Mergeable (S a) where
 instance EqSymbolic (S a) where
   S _ x .== S _ y = x .== y
 
-instance SymVal a => OrdSymbolic (S a) where
+instance (Ord a, SymVal a) => OrdSymbolic (S a) where
   S _ x .< S _ y = x .< y
 
 instance Boolean (S Bool) where
@@ -400,7 +400,7 @@ instance {-# OVERLAPPING #-} Num (S Decimal) where
   fromInteger i  = sansProv $ fromInteger i
   negate (S _ x) = sansProv $ negate x
 
-instance (Num a, SymVal a) => Num (S a) where
+instance (Num a, Ord a, SymVal a) => Num (S a) where
   S _ x + S _ y  = sansProv $ x + y
   S _ x * S _ y  = sansProv $ x * y
   abs (S _ x)    = sansProv $ abs x
@@ -414,7 +414,7 @@ instance {-# OVERLAPPING #-} Fractional (S Decimal) where
   fromRational  = literalS . fromRational
   S _ x / S _ y = sansProv $ x / y
 
-instance (Fractional a, SymVal a) => Fractional (S a) where
+instance (Fractional a, Ord a, SymVal a) => Fractional (S a) where
   fromRational = literalS . fromRational
   S _ x / S _ y = sansProv $ x / y
 
@@ -636,7 +636,7 @@ fromIntegralS
   -> S b
 fromIntegralS = over s2Sbv sFromIntegral
 
-oneIfS :: (Num a, SymVal a) => S Bool -> S a
+oneIfS :: (Num a, Ord a, SymVal a) => S Bool -> S a
 oneIfS = over s2Sbv oneIf
 
 isConcreteS :: SymVal a => S a -> Bool
@@ -870,6 +870,24 @@ withEq = withDict . singMkEq
       SObjectUnsafe (SCons' _ ty' tys)
         -> withEq ty' $ withDict (singMkEq (SObjectUnsafe tys)) Dict
 
+withOrd :: SingTy a -> (Ord (Concrete a) => b) -> b
+withOrd = withDict . singMkOrd
+  where
+
+    singMkOrd :: SingTy a -> Dict (Ord (Concrete a))
+    singMkOrd = \case
+      SInteger     -> Dict
+      SBool        -> Dict
+      SStr         -> Dict
+      STime        -> Dict
+      SDecimal     -> Dict
+      SGuard       -> Dict
+      SAny         -> Dict
+      SList ty'    -> withOrd ty' Dict
+      SObjectUnsafe SNil'   -> Dict
+      SObjectUnsafe (SCons' _ ty' tys)
+        -> withOrd ty' $ withDict (singMkOrd (SObjectUnsafe tys)) Dict
+
 withShow :: SingTy a -> (Show (Concrete a) => b) -> b
 withShow = withDict . singMkShow
   where

diff --git a/stack.yaml b/stack.yaml
@@ -16,7 +16,6 @@ extra-deps:
   - git: https://github.com/kadena-io/thyme.git
     commit: 6ee9fcb026ebdb49b810802a981d166680d867c9
   - constraints-extras-0.2.0.0
-  # temporarily using a patched fork of sbv to disable "unsupported query call"
-  # until it's fixed upstream
-  - git: https://github.com/joelburget/sbv.git
-    commit: 8d13e26255178c5ee5b5b3fad97873ff214d7470
+  # this is pre-sbv-8.1 (switch when it's released)
+  - git: https://github.com/LeventErkok/sbv.git
+    commit: 68375576f87d17a2da759c56f7147f4e559471a2