Implies endpoint in booster (#3846)

Closes #3778 #3601 This PR introduces a simple check implication implementation, which uses the matching algorithm to try to find a substitution or fail to unify the given configurations. If matching the RHS configuration to the LHS succeeds and produces a substitution σ, we filter out any predicates in the consequent which appear in the antecedent and then check if all predicates in σ(filtered_preds) evaluate to true/#top. (Question: do we want to apply σ to the RHS preds before filtering?). With this simple algorithm, we can successfully discharge almost 85% of implication checks in KEVM and 88% in Kontrol. --------- Co-authored-by: github-actions <[email protected]>
runtimeverification · May 8, 2024 · a0ca443 · a0ca443
1 parent 538d079
commit a0ca443
Show file tree

Hide file tree

Showing 20 changed files with 43,502 additions and 43,569 deletions.
diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs
@@ -48,14 +48,20 @@ import Booster.Log
 import Booster.Pattern.ApplyEquations qualified as ApplyEquations
 import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
 import Booster.Pattern.Base qualified as Pattern
+import Booster.Pattern.Bool (pattern TrueBool)
+import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (..), matchTerms)
 import Booster.Pattern.Rewrite (
     RewriteFailed (..),
     RewriteResult (..),
     RewriteTrace (..),
     performRewrite,
  )
-import Booster.Pattern.Util (sortOfPattern, substituteInPredicate, substituteInTerm)
-import Booster.Prettyprinter (renderText)
+import Booster.Pattern.Util (
+    sortOfPattern,
+    substituteInPredicate,
+    substituteInTerm,
+ )
+import Booster.Prettyprinter (renderDefault, renderText)
 import Booster.SMT.Base qualified as SMT
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.Json (KoreJson (..), addHeader, prettyPattern, sortOfJson)
@@ -73,7 +79,11 @@ import Booster.Syntax.Json.Internalise (
 import Booster.Syntax.ParsedKore (parseKoreModule)
 import Booster.Syntax.ParsedKore.Base hiding (ParsedModule)
 import Booster.Syntax.ParsedKore.Base qualified as ParsedModule (ParsedModule (..))
-import Booster.Syntax.ParsedKore.Internalise (addToDefinitions, definitionErrorToRpcError)
+import Booster.Syntax.ParsedKore.Internalise (
+    addToDefinitions,
+    definitionErrorToRpcError,
+    extractExistentials,
+ )
 import Booster.Util (Flag (..), constructorName)
 import Kore.JsonRpc.Error qualified as RpcError
 import Kore.JsonRpc.Server (ErrorObj (..), JsonRpcHandler (..), Respond)
@@ -455,11 +465,87 @@ respond stateVar =
                                         { satisfiable = RpcTypes.Sat
                                         , substitution
                                         }
+        RpcTypes.Implies req -> withModule req._module $ \(def, mLlvmLibrary, mSMTOptions) -> Booster.Log.withContext "implies" $ do
+            -- internalise given constrained term
+            let internalised =
+                    runExcept . internalisePattern DisallowAlias CheckSubsorts Nothing def . fst . extractExistentials
+
+            case (internalised req.antecedent.term, internalised req.consequent.term) of
+                (Left patternError, _) -> do
+                    Log.logDebug $ "Error internalising antecedent" <> Text.pack (show patternError)
+                    pure $
+                        Left $
+                            RpcError.backendError $
+                                RpcError.CouldNotVerifyPattern
+                                    [ patternErrorToRpcError patternError
+                                    ]
+                (_, Left patternError) -> do
+                    Log.logDebug $ "Error internalising consequent" <> Text.pack (show patternError)
+                    pure $
+                        Left $
+                            RpcError.backendError $
+                                RpcError.CouldNotVerifyPattern
+                                    [ patternErrorToRpcError patternError
+                                    ]
+                (Right (patL, substitutionL, unsupportedL), Right (patR, substitutionR, unsupportedR)) -> do
+                    unless (null unsupportedL && null unsupportedR) $ do
+                        Log.logWarnNS
+                            "booster"
+                            "Implies: aborting due to unsupported predicate parts"
+                        unless (null unsupportedL) $
+                            Log.logOtherNS
+                                "booster"
+                                (Log.LevelOther "ErrorDetails")
+                                (Text.unlines $ map prettyPattern unsupportedL)
+                        unless (null unsupportedR) $
+                            Log.logOtherNS
+                                "booster"
+                                (Log.LevelOther "ErrorDetails")
+                                (Text.unlines $ map prettyPattern unsupportedR)
+                    let
+                        -- apply the given substitution before doing anything else
+                        substPatL =
+                            Pattern
+                                { term = substituteInTerm substitutionL patL.term
+                                , constraints = Set.map (substituteInPredicate substitutionL) patL.constraints
+                                , ceilConditions = patL.ceilConditions
+                                }
+                        substPatR =
+                            Pattern
+                                { term = substituteInTerm substitutionR patR.term
+                                , constraints = Set.map (substituteInPredicate substitutionR) patR.constraints
+                                , ceilConditions = patR.ceilConditions
+                                }
+
+                    case matchTerms Booster.Pattern.Match.Implies def substPatR.term substPatL.term of
+                        MatchFailed (SubsortingError sortError) ->
+                            pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
+                                show sortError
+                        MatchFailed{} ->
+                            doesNotImply (sortOfPattern substPatL) req.antecedent.term req.consequent.term
+                        MatchIndeterminate remainder ->
+                            pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
+                                "match remainder: "
+                                    <> renderDefault (pretty remainder)
+                        MatchSuccess subst -> do
+                            let filteredConsequentPreds =
+                                    Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
+                                doTracing = Flag False
+                            solver <- traverse (SMT.initSolver def) mSMTOptions
+
+                            if null filteredConsequentPreds
+                                then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
+                                else
+                                    ApplyEquations.evaluateConstraints doTracing def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case
+                                        (Right newPreds, _) ->
+                                            if all (== Pattern.Predicate TrueBool) newPreds
+                                                then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
+                                                else pure . Left . RpcError.backendError $ RpcError.Aborted "unknown constrains"
+                                        (Left other, _) ->
+                                            pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
 
         -- this case is only reachable if the cancel appeared as part of a batch request
         RpcTypes.Cancel -> pure $ Left RpcError.cancelUnsupportedInBatchMode
-        -- using "Method does not exist" error code
-        _ -> pure $ Left RpcError.notImplemented
   where
     withModule ::
         Maybe Text ->
@@ -474,6 +560,39 @@ respond stateVar =
             Nothing -> pure $ Left $ RpcError.backendError $ RpcError.CouldNotFindModule mainName
             Just d -> action (d, state.mLlvmLibrary, state.mSMTOptions)
 
+    doesNotImply s l r =
+        pure $
+            Right $
+                RpcTypes.Implies
+                    RpcTypes.ImpliesResult
+                        { implication = addHeader $ Syntax.KJImplies (externaliseSort s) l r
+                        , valid = False
+                        , condition = Nothing
+                        , logs = Nothing
+                        }
+
+    implies s' l r subst =
+        let s = externaliseSort s'
+         in pure $
+                Right $
+                    RpcTypes.Implies
+                        RpcTypes.ImpliesResult
+                            { implication = addHeader $ Syntax.KJImplies s l r
+                            , valid = True
+                            , condition =
+                                Just
+                                    RpcTypes.Condition
+                                        { predicate = addHeader $ Syntax.KJTop s
+                                        , substitution =
+                                            addHeader
+                                                $ (\xs -> if null xs then Syntax.KJTop s else Syntax.KJAnd s xs)
+                                                    . map (uncurry $ externaliseSubstitution s)
+                                                    . Map.toList
+                                                $ subst
+                                        }
+                            , logs = Nothing
+                            }
+
 handleSmtError :: JsonRpcHandler
 handleSmtError = JsonRpcHandler $ \case
     SMT.GeneralSMTError err -> runtimeError "problem" err
@@ -764,7 +883,7 @@ mkLogRewriteTrace
                 | logSuccessfulRewrites ->
                     Just $
                         singleton $
-                            Rewrite
+                            Kore.JsonRpc.Types.Log.Rewrite
                                 { result =
                                     Success
                                         { rewrittenTerm = Nothing
@@ -778,7 +897,7 @@ mkLogRewriteTrace
                 | logFailedRewrites ->
                     Just $
                         singleton $
-                            Rewrite
+                            Kore.JsonRpc.Types.Log.Rewrite
                                 { result = case reason of
                                     NoApplicableRules{} -> Failure{reason = "No applicable rules found", _ruleId = Nothing}
                                     TermIndexIsNone{} -> Failure{reason = "Term index is None for term", _ruleId = Nothing}

diff --git a/booster/library/Booster/JsonRpc/Utils.hs b/booster/library/Booster/JsonRpc/Utils.hs
@@ -13,6 +13,7 @@ module Booster.JsonRpc.Utils (
     rpcTypeOf,
     typeString,
     diffBy,
+    methodOfRpcCall,
 ) where
 
 import Control.Applicative ((<|>))
@@ -200,20 +201,21 @@ typeString = BS.pack . show
 
 rpcTypeOf :: KoreRpcJson -> KoreRpcType
 rpcTypeOf = \case
-    RpcRequest req -> RpcReq $ methodOf req
-    RpcResponse r -> RpcResp $ methodOf r
+    RpcRequest req -> RpcReq $ methodOfRpcCall req
+    RpcResponse r -> RpcResp $ methodOfRpcCall r
     RpcError{} -> RpcErr
     RpcKoreJson{} -> RpcKore
     RpcJson{} -> RpcJs
     NotRpcJson{} -> NotRpcJs
-  where
-    methodOf = \case
-        Execute _ -> ExecuteM
-        Implies _ -> ImpliesM
-        Simplify _ -> SimplifyM
-        AddModule _ -> AddModuleM
-        GetModel _ -> GetModelM
-        Cancel -> error "Cancel"
+
+methodOfRpcCall :: API r -> APIMethod
+methodOfRpcCall = \case
+    Execute _ -> ExecuteM
+    Implies _ -> ImpliesM
+    Simplify _ -> SimplifyM
+    AddModule _ -> AddModuleM
+    GetModel _ -> GetModelM
+    Cancel -> error "Cancel"
 
 -------------------------------------------------------------------
 -- doing the actual diff when output is requested

diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -29,6 +29,7 @@ module Booster.Pattern.ApplyEquations (
     simplifyConstraint,
     simplifyConstraints,
     SimplifierCache,
+    evaluateConstraints,
 ) where
 
 import Control.Applicative (Alternative (..))
@@ -568,7 +569,7 @@ evaluatePattern doTracing def mLlvmLibrary smtSolver cache =
 
 -- version for internal nested evaluation
 evaluatePattern' ::
-    MonadLoggerIO io =>
+    LoggerMIO io =>
     Pattern ->
     EquationT io Pattern
 evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do
@@ -580,14 +581,38 @@ evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternCon
     -- this may yield additional new constraints, left unevaluated
     evaluatedConstraints <- predicates <$> getState
     pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions}
-  where
-    -- evaluate the given predicate assuming all others
-    simplifyAssumedPredicate p = withContext "constraint" $ do
-        allPs <- predicates <$> getState
-        let otherPs = Set.delete p allPs
-        eqState $ modify $ \s -> s{predicates = otherPs}
-        newP <- simplifyConstraint' True $ coerce p
-        pushConstraints $ Set.singleton $ coerce newP
+
+-- evaluate the given predicate assuming all others
+simplifyAssumedPredicate :: LoggerMIO io => Predicate -> EquationT io ()
+simplifyAssumedPredicate p = do
+    allPs <- predicates <$> getState
+    let otherPs = Set.delete p allPs
+    eqState $ modify $ \s -> s{predicates = otherPs}
+    newP <- simplifyConstraint' True $ coerce p
+    pushConstraints $ Set.singleton $ coerce newP
+
+evaluateConstraints ::
+    LoggerMIO io =>
+    Flag "CollectEquationTraces" ->
+    KoreDefinition ->
+    Maybe LLVM.API ->
+    Maybe SMT.SMTContext ->
+    SimplifierCache ->
+    Set Predicate ->
+    io (Either EquationFailure (Set Predicate), SimplifierCache)
+evaluateConstraints doTracing def mLlvmLibrary smtSolver cache =
+    runEquationT doTracing def mLlvmLibrary smtSolver cache . evaluateConstraints'
+
+evaluateConstraints' ::
+    LoggerMIO io =>
+    Set Predicate ->
+    EquationT io (Set Predicate)
+evaluateConstraints' constraints = do
+    pushConstraints constraints
+    -- evaluate all existing constraints, once
+    traverse_ simplifyAssumedPredicate . predicates =<< getState
+    -- this may yield additional new constraints, left unevaluated
+    predicates <$> getState
 
 ----------------------------------------