4059 ensures substitution (#4060)

Fixes #4059

This PR improves Booster's handling of substitutions.

## Summary

Substitutions are special predicates: equations where the LHS is a
variable, for example `VAR ==Int TERM`. See
`Booster.Syntax.Json.Internalise.mbSubstitution` for the exact
specification of what is considered to be a substitution.

This PR changes the `Pattern` type to explicitly carry these special
substitution predicates:

```diff
+type Substitution = Map Variable Term
+
 -- | A term (configuration) constrained by a number of predicates.
 data Pattern = Pattern
     { term :: Term
     , constraints :: !(Set Predicate)
+    , substitution :: Substitution
     , ceilConditions :: ![Ceil]
     }
     deriving stock (Eq, Ord, Show, Generic, Data)
```

Substitution may appear out of three places:
- sent in the request body
- ensured as a post condition of a rewrite rule
- **NOT IMPLEMENTED** learned from the branching condition --- this is
something that will be added as part of #4058

The first source is handled by the pattern internalisation code. The
second and third sources are different, as the pattern has already been
internalised. All this sources can also produce generic (i.e.
non-substitution) constrains that should be added into the `constrains`
set of a `Pattern`. Substitutions, when produces, should be applied to
the `term` of the `Pattern` and added to the `substitution` field. This
PR makes sure we use the same code path for separating substitutions
from generic predicates everywhere. We use
`Booster.Syntax.Json.Internalise.mbSubstitution.mkSubstitution` to take
care of cyclic, which are broken up, and duplicate bindings, which are
treated as constraints.

With these changes, we can harmonize many (but not all) specialisations
of the integrations test responses, i.e. we do not need many of the
`*.booster-dev` and `*.kore-rpc-dev` response files.

## Changes to pattern simplification code

As the `Pattern` type has changed, we must adapt the
`ApplyEquations.evaluatePattern` and `ApplyEquations.evaluatePattern'`
functions to:
- consider `substitutions` as known truth together with all other
constraints (that's what we did before)
- simplify the substitution

We achieve that by doing the following:
- convert the substitution into equalities and assume it as know truth
- when constructing the new, simplified pattern, use the same code as
when internalising a pattern to partition predicates into the
substitution and non-substitution ones

## Changes to rewrite rule application code

The `Pattern.Rewrite.applyRule` function has been changed to:
- consider `substiontion` as known truth together with all other
constraints (that's what we did before) when checking requires/ensures
- extract the substitution from the ensured conditions and add it to the
rewritten pattern

---------

Co-authored-by: github-actions <[email protected]>

Author: geo2a

booster/library/Booster/JsonRpc.hs

@@ -44,7 +44,7 @@ import Booster.Definition.Base qualified as Definition (RewriteRule (..))
 import Booster.LLVM as LLVM (API)
 import Booster.Log
 import Booster.Pattern.ApplyEquations qualified as ApplyEquations
-import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
+import Booster.Pattern.Base (Pattern (..), Sort (SortApp))
 import Booster.Pattern.Base qualified as Pattern
 import Booster.Pattern.Implies (runImplies)
 import Booster.Pattern.Pretty
@@ -55,12 +55,11 @@ import Booster.Pattern.Rewrite (
     RewriteTrace (..),
     performRewrite,
  )
+import Booster.Pattern.Substitution qualified as Substitution
 import Booster.Pattern.Util (
     freeVariables,
     sortOfPattern,
     sortOfTerm,
-    substituteInPredicate,
-    substituteInTerm,
  )
 import Booster.Prettyprinter (renderText)
 import Booster.SMT.Interface qualified as SMT
@@ -69,6 +68,7 @@ import Booster.Syntax.Json.Externalise
 import Booster.Syntax.Json.Internalise (
     InternalisedPredicates (..),
     TermOrPredicates (..),
+    extractSubstitution,
     internalisePattern,
     internaliseTermOrPredicate,
     logPatternError,
@@ -131,12 +131,14 @@ respond stateVar request =
                                         [ req.logSuccessfulRewrites
                                         , req.logFailedRewrites
                                         ]
-                        -- apply the given substitution before doing anything else
+                        -- apply the given substitution before doing anything else,
+                        -- as internalisePattern does not substitute
                         let substPat =
                                 Pattern
-                                    { term = substituteInTerm substitution term
-                                    , constraints = Set.fromList $ map (substituteInPredicate substitution) preds
+                                    { term = Substitution.substituteInTerm substitution term
+                                    , constraints = Set.fromList $ map (Substitution.substituteInPredicate substitution) preds
                                     , ceilConditions = ceils
+                                    , substitution
                                     }
                             -- remember all variables used in the substitutions
                             substVars =
@@ -166,7 +168,7 @@ respond stateVar request =
                         result <-
                             performRewrite rewriteConfig substPat
                         SMT.finaliseSolver solver
-                        pure $ execResponse req result substitution unsupported
+                        pure $ execResponse req result unsupported
             RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do
                 -- block other request executions while modifying the server state
                 state <- liftIO $ takeMVar stateVar
@@ -244,20 +246,14 @@ respond stateVar request =
                                     RpcError.CouldNotVerifyPattern $
                                         map patternErrorToRpcError patternErrors
                     -- term and predicate (pattern)
-                    Right (TermAndPredicates pat substitution unsupported) -> do
+                    -- NOTE: the input substitution will have already been applied by internaliseTermOrPredicate
+                    Right (TermAndPredicates pat unsupported) -> do
                         unless (null unsupported) $ do
                             withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do
                                 logMessage ("ignoring unsupported predicate parts" :: Text)
-                        -- apply the given substitution before doing anything else
-                        let substPat =
-                                Pattern
-                                    { term = substituteInTerm substitution pat.term
-                                    , constraints = Set.map (substituteInPredicate substitution) pat.constraints
-                                    , ceilConditions = pat.ceilConditions
-                                    }
-                        ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case
+                        ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty pat >>= \case
                             (Right newPattern, _) -> do
-                                let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
+                                let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
                                     tSort = externaliseSort (sortOfPattern newPattern)
                                     result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
                                         [] -> term
@@ -281,23 +277,24 @@ respond stateVar request =
                                 withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
                                     logMessage ("ignoring unsupported predicate parts" :: Text)
                             -- apply the given substitution before doing anything else
-                            let predicates = map (substituteInPredicate ps.substitution) ps.boolPredicates
+                            let predicates = map (Substitution.substituteInPredicate ps.substitution) ps.boolPredicates
                             withContext CtxConstraint $
                                 ApplyEquations.simplifyConstraints
                                     def
                                     mLlvmLibrary
                                     solver
                                     mempty
-                                    predicates
+                                    (predicates <> Substitution.asEquations ps.substitution)
                                     >>= \case
-                                        (Right newPreds, _) -> do
+                                        (Right simplified, _) -> do
                                             let predicateSort =
                                                     fromMaybe (error "not a predicate") $
                                                         sortOfJson req.state.term
+                                                (simplifiedSubstitution, simplifiedPredicates) = extractSubstitution simplified
                                                 result =
-                                                    map (externalisePredicate predicateSort) newPreds
+                                                    map (externalisePredicate predicateSort) (Set.toList simplifiedPredicates)
                                                         <> map (externaliseCeil predicateSort) ps.ceilPredicates
-                                                        <> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
+                                                        <> map (uncurry $ externaliseSubstitution predicateSort) (Map.assocs simplifiedSubstitution)
                                                         <> ps.unsupported
 
                                             pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)
@@ -332,7 +329,7 @@ respond stateVar request =
                             -- term and predicates were sent. Only work on predicates
                             (boolPs, suppliedSubst) <-
                                 case things of
-                                    TermAndPredicates pat substitution unsupported -> do
+                                    TermAndPredicates pat unsupported -> do
                                         withContext CtxGetModel $
                                             logMessage' ("ignoring supplied terms and only checking predicates" :: Text)
 
@@ -341,7 +338,7 @@ respond stateVar request =
                                                 logMessage' ("ignoring unsupported predicates" :: Text)
                                                 withContext CtxDetail $
                                                     logMessage (Text.unwords $ map prettyPattern unsupported)
-                                        pure (Set.toList pat.constraints, substitution)
+                                        pure (Set.toList pat.constraints, pat.substitution)
                                     Predicates ps -> do
                                         unless (null ps.ceilPredicates && null ps.unsupported) $ do
                                             withContext CtxGetModel $ do
@@ -472,21 +469,20 @@ execStateToKoreJson RpcTypes.ExecuteState{term = t, substitution, predicate} =
 execResponse ::
     RpcTypes.ExecuteRequest ->
     (Natural, Seq (RewriteTrace ()), RewriteResult Pattern) ->
-    Map Variable Term ->
     [Syntax.KorePattern] ->
     Either ErrorObj (RpcTypes.API 'RpcTypes.Res)
-execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
+execResponse req (d, traces, rr) unsupported = case rr of
     RewriteBranch p nexts ->
         Right $
             RpcTypes.Execute
                 RpcTypes.ExecuteResult
                     { reason = RpcTypes.Branching
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates =
                         Just $
-                            map (\(_, muid, p') -> toExecState p' originalSubstitution unsupported (Just muid)) $
+                            map (\(_, muid, p') -> toExecState p' unsupported (Just muid)) $
                                 toList nexts
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -498,7 +494,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.Stuck
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -510,7 +506,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.Vacuous
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -522,8 +518,8 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.CutPointRule
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
-                    , nextStates = Just [toExecState next originalSubstitution unsupported Nothing]
+                    , state = toExecState p unsupported Nothing
+                    , nextStates = Just [toExecState next unsupported Nothing]
                     , rule = Just lbl
                     , unknownPredicate = Nothing
                     }
@@ -534,7 +530,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.TerminalRule
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates = Nothing
                     , rule = Just lbl
                     , unknownPredicate = Nothing
@@ -546,7 +542,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.DepthBound
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -563,7 +559,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                                     (logSuccessfulRewrites, logFailedRewrites)
                                     (RewriteStepFailed failure)
                          in logs <|> abortRewriteLog
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -586,8 +582,8 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                 xs@(_ : _) -> Just xs
 
 toExecState ::
-    Pattern -> Map Variable Term -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
-toExecState pat sub unsupported muid =
+    Pattern -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
+toExecState pat unsupported muid =
     RpcTypes.ExecuteState
         { term = addHeader t
         , predicate = addHeader <$> addUnsupported p
@@ -597,7 +593,7 @@ toExecState pat sub unsupported muid =
         , ruleId = getUniqueId <$> muid
         }
   where
-    (t, p, s) = externalisePattern pat sub
+    (t, p, s) = externalisePattern pat
     termSort = externaliseSort $ sortOfPattern pat
     allUnsupported = Syntax.KJAnd termSort unsupported
     addUnsupported

booster/library/Booster/JsonRpc/Utils.hs

@@ -279,18 +279,9 @@ diffBy def pat1 pat2 =
             <> if null ps.unsupported
                 then ""
                 else BS.unlines ("Unsupported parts:" : map Json.encode ps.unsupported)
-    renderBS (TermAndPredicates p m u) =
+    renderBS (TermAndPredicates p u) =
         ( BS.pack . renderDefault $
             pretty (PrettyWithModifiers @['Decoded, 'Truncated] p)
-                <+> vsep
-                    ( map
-                        ( \(k, v) ->
-                            pretty (PrettyWithModifiers @['Decoded, 'Truncated] k)
-                                <+> "="
-                                <+> pretty (PrettyWithModifiers @['Decoded, 'Truncated] v)
-                        )
-                        (Map.toList m)
-                    )
         )
             <> if null u then "" else BS.unlines ("Unsupported parts: " : map Json.encode u)
     internalise =

booster/library/Booster/Log.hs

@@ -69,6 +69,7 @@ import Booster.Pattern.Base (
     pattern AndTerm,
  )
 import Booster.Pattern.Pretty
+import Booster.Pattern.Substitution (asEquations)
 import Booster.Prettyprinter (renderOneLineText)
 import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern)
 import Booster.Syntax.Json.Externalise (externaliseTerm)
@@ -185,8 +186,8 @@ withTermContext t@(Term attrs _) m =
         m
 
 withPatternContext :: LoggerMIO m => Pattern -> m a -> m a
-withPatternContext Pattern{term, constraints} m =
-    let t' = foldl' AndTerm term $ Set.toList $ Set.map coerce constraints -- FIXME
+withPatternContext Pattern{term, constraints, substitution} m =
+    let t' = foldl' AndTerm term . map coerce $ Set.toList constraints <> asEquations substitution
      in withTermContext t' m
 
 instance ToLogFormat KorePattern where

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -66,10 +66,12 @@ import Booster.Pattern.Bool
 import Booster.Pattern.Index qualified as Idx
 import Booster.Pattern.Match
 import Booster.Pattern.Pretty
+import Booster.Pattern.Substitution
 import Booster.Pattern.Util
 import Booster.Prettyprinter (renderOneLineText)
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.Json.Externalise (externaliseTerm)
+import Booster.Syntax.Json.Internalise (extractSubstitution)
 import Booster.Util (Bound (..))
 import Kore.JsonRpc.Types.ContextLog (CLContext (CLWithId), IdContext (CtxCached))
 import Kore.Util (showHashHex)
@@ -455,7 +457,15 @@ evaluatePattern ::
     Pattern ->
     io (Either EquationFailure Pattern, SimplifierCache)
 evaluatePattern def mLlvmLibrary smtSolver cache pat =
-    runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat
+    runEquationT
+        def
+        mLlvmLibrary
+        smtSolver
+        cache
+        -- interpret substitution as additional known constraints
+        (pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
+        . evaluatePattern'
+        $ pat
 
 -- version for internal nested evaluation
 evaluatePattern' ::
@@ -469,7 +479,20 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
     traverse_ simplifyAssumedPredicate . predicates =<< getState
     -- this may yield additional new constraints, left unevaluated
     evaluatedConstraints <- predicates <$> getState
-    pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions}
+    -- The interface-level evaluatePattern puts pat.substitution together with pat.constraints
+    -- into the simplifier state as known truth. Here the substitution will bubble-up as part of
+    -- evaluatedConstraints. To avoid duplicating constraints (i.e. having equivalent entities
+    -- in pat.predicate and pat.substitution), we discard the old substitution here
+    -- and extract a possible simplified one from evaluatedConstraints.
+    let (simplifiedSubsitution, simplifiedConstraints) = extractSubstitution (Set.toList evaluatedConstraints)
+
+    pure
+        Pattern
+            { constraints = simplifiedConstraints
+            , term = newTerm
+            , ceilConditions
+            , substitution = simplifiedSubsitution
+            }
   where
     -- when TooManyIterations exception occurred while evaluating the top-level term,
     -- i.e. not in a recursive evaluation of a side-condition,

booster/library/Booster/Pattern/Base.hs

@@ -36,6 +36,7 @@ import Data.Functor.Foldable
 import Data.Hashable (Hashable)
 import Data.Hashable qualified as Hashable
 import Data.List as List (foldl', foldl1', sort)
+import Data.Map.Strict (Map)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import GHC.Generics (Generic)
@@ -761,19 +762,22 @@ pattern KSeq sort a =
 
 --------------------
 
+type Substitution = Map Variable Term
+
 -- | A term (configuration) constrained by a number of predicates.
 data Pattern = Pattern
     { term :: Term
     , constraints :: !(Set Predicate)
+    , substitution :: Substitution
     , ceilConditions :: ![Ceil]
     }
     deriving stock (Eq, Ord, Show, Generic, Data)
     deriving anyclass (NFData)
 
 pattern Pattern_ :: Term -> Pattern
-pattern Pattern_ t <- Pattern t _ _
+pattern Pattern_ t <- Pattern t _ _ _
     where
-        Pattern_ t = Pattern t mempty mempty
+        Pattern_ t = Pattern t mempty mempty mempty
 
 pattern ConsApplication :: Symbol -> [Sort] -> [Term] -> Term
 pattern ConsApplication sym sorts args <-

booster/library/Booster/Pattern/Binary.hs

@@ -564,7 +564,7 @@ decodePattern mDef = do
                 preds <- forM preds' $ \case
                     BPredicate pIdx -> Predicate <$> getTerm pIdx
                     _ -> fail "Expecting a predicate"
-                pure $ Pattern trm (Set.fromList preds) mempty
+                pure $ Pattern trm (Set.fromList preds) mempty mempty
             _ -> fail "Expecting a term on the top of the stack"
 
 encodeMagicHeaderAndVersion :: Version -> Put

booster/library/Booster/Pattern/Bool.hs

@@ -36,11 +36,10 @@ import Booster.Definition.Attributes.Base (
     pattern IsNotMacroOrAlias,
  )
 import Booster.Pattern.Base (
-    Pattern,
+    Pattern (..),
     Predicate (..),
     Symbol (Symbol),
     Term,
-    constraints,
     pattern DomainValue,
     pattern SortBool,
     pattern SortInt,