3956 branching on complete conditions in Booster (#4058)

Part of #3956
Partially subsumes
#3960

This PR makes the rewrite rule application algorithm of Booster more
powerful by allowing branching on *complete conditions*.

The rewriting algorithm is modified:
- when checking the `requires` clause of a rule, we compute the
remainder condition `RULE_REM` of that attempted, which is the
semantically-checked subset of the required conjuncts `P` which
*unclear* after checking its entailment form the pattern's constrains
`PC`, meaning that (PC /\ P, PC /\ not P) is (SAT, SAT) or any of the
two queries were UNKNOWN
- if that remainder is not empty, we return it's *negation* together
with the result
- when we are finished attempting a *priority group* of rules, we
collect the negated remainder conditions `not RULE_REM_i` and conjunct
them. This the groups remainder condition `GROUP_REM == not RULE_REM_1
/\ not RULE_REM_2 /\ ... /\ not RULE_REM_n`
- At that point, we need to check `GROUP_REM` for satisfiablity.
- **If the `GROUP_REM` condition is UNSAT, it means that this group of
rules is *complete***, meaning that no other rule can possibly apply,
and we do not need to even attempt applying rules of lower priority.
This behaviour is the **primary contribution of this PR**.
- Otherwise, if it is SAT or solver said UNKNOWN, it means that this
group of rules is not complete, i.e. it does not cover the whole space
of logical possibility, and we need to construct a remainder
configuration, and continue attempting to apply other rules to it. If no
rules remain, it means that we are stuck and the semantics is
incomplete. This PR does not implement the process of descending into
the remainder branch. **Booster with this PR will abort on a SAT
remainder**.

This behaviour is active by default in `booster-dev` and can be enabled
in `kore-rpc-booster` with the flag `--fallback-on Aborted,Stuck` (the
default is `Aborted,Stuck,Branching`). Note that with the default
reasons, the behaviour of `kore-rpc-booster` is functionally the same,
but operationally slightly different: In `Proxy.hs`, Booster may not
return `Branching`, and the fallback logic will confirm that Kore
returns `Branching` as well, flagging any differences in the `[proxy]`
logs (see
[Proxy.hs#L391](https://github.com/runtimeverification/haskell-backend/blob/3956-booster-rewrite-rule-remainders/booster/tools/booster/Proxy.hs#L391)).

TODO: we need a better flag to enabled branching in Booster, as giving a
`--fallback-on Aborted,Stuck` is really non-intuitive.

Note:
a naive algorithm to compute the remainder conditions would be: after
applying a group of rules, take their substituted requires clauses,
disjunct and negate. However, this yields a non-minimal predicate that
was not simplified and syntactically filtered, potentially making it
harder for the SMT solver to solve. The algorithm described above and
implemented in this PR re-uses the indeterminate results obtained while
applying individual rules and simplifying/checking their individual
requires clauses. This logic has been originally proposed by Sam in
#3960.

See
[remainder-predicates.k](https://github.com/runtimeverification/haskell-backend/blob/3956-booster-rewrite-rule-remainders/booster/test/rpc-integration/resources/remainder-predicates.k)
and
[test-remainder-predicates](https://github.com/runtimeverification/haskell-backend/blob/3956-booster-rewrite-rule-remainders/booster/test/rpc-integration/test-remainder-predicates)
for a series of integrations tests that cover the behaviour of
`booster-dev` and `kore-rpc-booster`.

Author: geo2a

booster/library/Booster/JsonRpc.hs

@@ -22,7 +22,7 @@ import Control.Monad
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
 import Crypto.Hash (SHA256 (..), hashWith)
-import Data.Bifunctor (second)
+import Data.Bifunctor (first, second)
 import Data.Foldable
 import Data.List (singleton)
 import Data.Map.Strict (Map)
@@ -38,7 +38,7 @@ import GHC.Records
 import Numeric.Natural
 
 import Booster.CLOptions (RewriteOptions (..))
-import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId)
+import Booster.Definition.Attributes.Base (getUniqueId, uniqueId)
 import Booster.Definition.Base (KoreDefinition (..))
 import Booster.Definition.Base qualified as Definition (RewriteRule (..))
 import Booster.LLVM as LLVM (API)
@@ -49,6 +49,7 @@ import Booster.Pattern.Base qualified as Pattern
 import Booster.Pattern.Implies (runImplies)
 import Booster.Pattern.Pretty
 import Booster.Pattern.Rewrite (
+    AppliedRuleMetadata (..),
     RewriteConfig (..),
     RewriteFailed (..),
     RewriteResult (..),
@@ -57,7 +58,9 @@ import Booster.Pattern.Rewrite (
  )
 import Booster.Pattern.Substitution qualified as Substitution
 import Booster.Pattern.Util (
+    externaliseRuleMarker,
     freeVariables,
+    modifyVarName,
     sortOfPattern,
     sortOfTerm,
  )
@@ -479,11 +482,13 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.Branching
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p Nothing unsupported
                     , nextStates =
-                        Just $
-                            map (\(_, muid, p') -> toExecState p' unsupported (Just muid)) $
-                                toList nexts
+                        Just
+                            $ map
+                                ( \(rewritten, ruleMetadata) -> toExecState rewritten (Just ruleMetadata) unsupported
+                                )
+                            $ toList nexts
                     , rule = Nothing
                     , unknownPredicate = Nothing
                     }
@@ -494,7 +499,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.Stuck
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p Nothing unsupported
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -506,7 +511,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.Vacuous
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p Nothing unsupported
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -518,8 +523,8 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.CutPointRule
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
-                    , nextStates = Just [toExecState next unsupported Nothing]
+                    , state = toExecState p Nothing unsupported
+                    , nextStates = Just [toExecState next Nothing unsupported]
                     , rule = Just lbl
                     , unknownPredicate = Nothing
                     }
@@ -530,7 +535,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.TerminalRule
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p Nothing unsupported
                     , nextStates = Nothing
                     , rule = Just lbl
                     , unknownPredicate = Nothing
@@ -542,7 +547,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.DepthBound
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p Nothing unsupported
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -559,7 +564,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
                                     (logSuccessfulRewrites, logFailedRewrites)
                                     (RewriteStepFailed failure)
                          in logs <|> abortRewriteLog
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p Nothing unsupported
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -582,23 +587,37 @@ execResponse req (d, traces, rr) unsupported = case rr of
                 xs@(_ : _) -> Just xs
 
 toExecState ::
-    Pattern -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
-toExecState pat unsupported muid =
+    Pattern ->
+    Maybe AppliedRuleMetadata ->
+    [Syntax.KorePattern] ->
     RpcTypes.ExecuteState
-        { term = addHeader t
-        , predicate = addHeader <$> addUnsupported p
-        , substitution = addHeader <$> s
-        , ruleSubstitution = Nothing
-        , rulePredicate = Nothing
-        , ruleId = getUniqueId <$> muid
-        }
-  where
-    (t, p, s) = externalisePattern pat
-    termSort = externaliseSort $ sortOfPattern pat
-    allUnsupported = Syntax.KJAnd termSort unsupported
-    addUnsupported
-        | null unsupported = id
-        | otherwise = maybe (Just allUnsupported) (Just . Syntax.KJAnd termSort . (: unsupported))
+toExecState
+    pat
+    mRuleMetadata
+    unsupported =
+        RpcTypes.ExecuteState
+            { term = addHeader t
+            , predicate = addHeader <$> addUnsupported p
+            , substitution = addHeader <$> s
+            , ruleSubstitution = addHeader <$> mruleSubstExt
+            , rulePredicate = addHeader <$> mrulePredExt
+            , ruleId = getUniqueId . ruleUniqueId <$> mRuleMetadata
+            }
+      where
+        mrulePredExt = externalisePredicate termSort . rulePredicate <$> mRuleMetadata
+        mruleSubstExt =
+            Syntax.KJAnd termSort
+                . map
+                    (uncurry (externaliseSubstitution termSort) . first (modifyVarName externaliseRuleMarker))
+                . Map.toList
+                . ruleSubstitution
+                <$> mRuleMetadata
+        (t, p, s) = externalisePattern pat
+        termSort = externaliseSort $ sortOfPattern pat
+        allUnsupported = Syntax.KJAnd termSort unsupported
+        addUnsupported
+            | null unsupported = id
+            | otherwise = maybe (Just allUnsupported) (Just . Syntax.KJAnd termSort . (: unsupported))
 
 mkLogRewriteTrace ::
     (Bool, Bool) ->
@@ -639,6 +658,11 @@ mkLogRewriteTrace
                                             { reason = "Uncertain about a condition in rule"
                                             , _ruleId = Just $ getUniqueId (uniqueId $ Definition.attributes r)
                                             }
+                                    RewriteRemainderPredicate rs _ _ ->
+                                        Failure
+                                            { reason = "Uncertain about the remainder after applying a rule"
+                                            , _ruleId = Just $ getUniqueId (uniqueId $ Definition.attributes (head rs))
+                                            }
                                     DefinednessUnclear r _ undefReasons ->
                                         Failure
                                             { reason = "Uncertain about definedness of rule because of: " <> pack (show undefReasons)

booster/library/Booster/Pattern/Bool.hs

@@ -7,9 +7,11 @@ License     : BSD-3-Clause
 module Booster.Pattern.Bool (
     foldAndBool,
     isBottom,
+    isFalse,
     negateBool,
     splitBoolPredicates,
     splitAndBools,
+    collapseAndBools,
     -- patterns
     pattern TrueBool,
     pattern FalseBool,
@@ -188,6 +190,11 @@ foldAndBool (x : xs) = AndBool x $ foldAndBool xs
 isBottom :: Pattern -> Bool
 isBottom = (Predicate FalseBool `elem`) . constraints
 
+isFalse :: Predicate -> Bool
+isFalse = \case
+    (Predicate FalseBool) -> True
+    _ -> False
+
 {- | We want to break apart predicates of type `Y1 andBool ... Yn` apart, in case some of the `Y`s are abstract
 which prevents the original expression from being fed to the LLVM simplifyBool function
 -}
@@ -205,3 +212,7 @@ splitAndBools :: Predicate -> [Predicate]
 splitAndBools p@(Predicate t)
     | AndBool l r <- t = concatMap (splitAndBools . Predicate) [l, r]
     | otherwise = [p]
+
+-- | Inverse of splitAndBools
+collapseAndBools :: [Predicate] -> Predicate
+collapseAndBools = Predicate . foldAndBool . map (\(Predicate p) -> p)