Ceil simplifier

booster/library/Booster/Definition/Base.hs

@@ -74,6 +74,11 @@ data RewriteRule (tag :: k) = RewriteRule
     , attributes :: AxiomAttributes
     , computedAttributes :: ComputedAxiomAttributes
     , existentials :: Set Variable
+    , definednessResidual :: [Either Predicate Term]
+    -- ^ leftover definedness obligations: the rule preserves definedness (may be
+    -- applied) iff this is empty (≡ @#Top@).  A @Left p@ is a residual predicate, a
+    -- @Right t@ an unresolved @#Ceil(t)@.  Computed at load (see
+    -- 'Booster.Syntax.ParsedKore.Internalise' and 'Booster.Definition.Ceil').
     }
     deriving stock (Eq, Ord, Show, GHC.Generic)
     deriving anyclass (NFData)

booster/library/Booster/Definition/Ceil.hs

@@ -76,12 +76,26 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods ComputeCeilSumm
                                 (Set.toList ceils)
                         ]
 
+{- | Which #Ceil formula to use when computing a rule's definedness residual.
+   Each rule kind picks one; changing the per-kind choice in 'computeCeilsDefinition'
+   is how we experiment with the definedness check.
+-}
+data DefinednessFormula
+    = -- | rewrite rules: @#Ceil(rhs)@ minus @#Ceil(lhs)@ minus @#Ceil(requires)@, plus @#Ceil(requires)@
+      Implication
+    | -- | function equations: @#Ceil(args of lhs) ∧ #Ceil(rhs)@ — the LHS *head* (the function
+      -- being defined) is excluded, since requiring its definedness would be circular
+      ConjunctionArgs
+    | -- | simplification rules: @#Ceil(lhs) ∧ #Ceil(rhs)@
+      Conjunction
+    deriving stock (Eq, Show)
+
 computeCeilsDefinition ::
     LoggerMIO io =>
     Maybe LLVM.API ->
     KoreDefinition ->
     io (KoreDefinition, [ComputeCeilSummary])
-computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do
+computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory, functionEquations, simplifications} = do
     (rewriteTheory', ceilSummaries) <-
         runWriterT $
             let ceilComputation r = do
@@ -91,48 +105,103 @@ computeCeilsDefinition mllvm def@KoreDefinition{rewriteTheory} = do
                             tell (Seq.singleton summary)
                             pure $ fromMaybe r newRule
              in mapM (mapM (mapM ceilComputation)) rewriteTheory
-    pure (def{rewriteTheory = rewriteTheory'}, toList ceilSummaries)
+    functionEquations' <-
+        mapM (mapM (mapM (refineRuleResidual mllvm def ConjunctionArgs))) functionEquations
+    simplifications' <- mapM (mapM (mapM (refineRuleResidual mllvm def Conjunction))) simplifications
+    pure
+        ( def
+            { rewriteTheory = rewriteTheory'
+            , functionEquations = functionEquations'
+            , simplifications = simplifications'
+            }
+        , toList ceilSummaries
+        )
+
+-- | Attach a rule's definedness residual (function/simplification rules: no logging summary).
+refineRuleResidual ::
+    LoggerMIO io =>
+    Maybe LLVM.API ->
+    KoreDefinition ->
+    DefinednessFormula ->
+    RewriteRule.RewriteRule tag ->
+    io (RewriteRule.RewriteRule tag)
+refineRuleResidual mllvm def formula r =
+    computeRuleResidual mllvm def formula r >>= \case
+        Nothing -> pure r
+        Just newRule -> pure newRule
 
+-- | Rewrite-rule ceil computation that additionally produces a logging summary.
 computeCeilRule ::
     LoggerMIO io =>
     Maybe LLVM.API ->
     KoreDefinition ->
     RewriteRule.RewriteRule "Rewrite" ->
     io (Maybe ComputeCeilSummary)
-computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attributes, computedAttributes}
+computeCeilRule mllvm def r =
+    computeRuleResidual mllvm def Implication r >>= \case
+        Nothing -> pure Nothing
+        Just newRule ->
+            pure . Just $
+                ComputeCeilSummary
+                    { rule = r
+                    , ceils = Set.fromList (RewriteRule.definednessResidual newRule)
+                    , newRule = Just newRule
+                    }
+
+{- | Compute a rule's definedness residual under the given formula and attach it
+   (replacing 'definednessResidual'). Returns 'Nothing' for rules already known to
+   preserve definedness (empty 'notPreservesDefinednessReasons'), which are left
+   untouched. When the residual discharges to empty, the rule is additionally marked
+   @preserving@. Polymorphic in the rule tag so it serves all three theories.
+-}
+computeRuleResidual ::
+    LoggerMIO io =>
+    Maybe LLVM.API ->
+    KoreDefinition ->
+    DefinednessFormula ->
+    RewriteRule.RewriteRule tag ->
+    io (Maybe (RewriteRule.RewriteRule tag))
+computeRuleResidual mllvm def formula r@RewriteRule.RewriteRule{lhs, requires, rhs, attributes, computedAttributes}
     | null computedAttributes.notPreservesDefinednessReasons = pure Nothing
     | otherwise = do
         ns <- noSolver
         (res, _) <- runEquationT def mllvm ns mempty mempty $ do
-            lhsCeils <- Set.fromList <$> computeCeil lhs
-            requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) requires
-            let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList
-            rhsCeils <- simplifyCeils =<< (subtractLHSAndRequiresCeils <$> computeCeil rhs)
-
-            pure $
-                Just $
-                    ComputeCeilSummary
-                        { rule = r
-                        , ceils = requiresCeils <> rhsCeils
-                        , newRule =
-                            if null requiresCeils && null rhsCeils
-                                then
-                                    Just
-                                        r
-                                            { RewriteRule.attributes = attributes{preserving = Flag True}
-                                            , RewriteRule.computedAttributes = computedAttributes{notPreservesDefinednessReasons = []}
-                                            }
-                                else -- we could add a case when ceils are fully resolved into predicates, which we would then
-                                -- add to the requires clause of a rule
-                                    Nothing
-                        }
+            ceils <- case formula of
+                Implication -> do
+                    lhsCeils <- Set.fromList <$> computeCeil lhs
+                    requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) requires
+                    let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList
+                    rhsCeils <- simplifyCeils =<< (subtractLHSAndRequiresCeils <$> computeCeil rhs)
+                    pure (requiresCeils <> rhsCeils)
+                ConjunctionArgs -> do
+                    argsCeils <- Set.fromList <$> concatMapM computeCeil (functionArgs lhs)
+                    rhsCeils <- Set.fromList <$> computeCeil rhs
+                    simplifyCeils (argsCeils <> rhsCeils)
+                Conjunction -> do
+                    lhsCeils <- Set.fromList <$> computeCeil lhs
+                    rhsCeils <- Set.fromList <$> computeCeil rhs
+                    simplifyCeils (lhsCeils <> rhsCeils)
+            pure . Just $
+                if null ceils
+                    then -- residual discharges to #Top: the rule preserves definedness
 
+                        r
+                            { RewriteRule.attributes = attributes{preserving = Flag True}
+                            , RewriteRule.computedAttributes = computedAttributes{notPreservesDefinednessReasons = []}
+                            , RewriteRule.definednessResidual = []
+                            }
+                    else r{RewriteRule.definednessResidual = Set.toList ceils}
         case res of
             Left err -> do
                 liftIO $ print err
                 pure Nothing
-            Right r' -> pure r'
+            Right newRule -> pure newRule
   where
+    -- arguments of a function-equation LHS, excluding the (function) head symbol
+    functionArgs = \case
+        SymbolApplication _ _ args -> args
+        other -> [other]
+
     simplifyCeils ceils =
         (.llvmApi) <$> getConfig >>= \case
             Nothing -> pure ceils

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -152,6 +152,11 @@ data EquationConfig = EquationConfig
     , maxLocalSteps :: Bound "LocalSteps"
     , logger :: Logger LogMessage
     , prettyModifiers :: ModifiersRep
+    , dischargeDefinedness :: Bool
+    -- ^ when True, a rule blocked by a non-empty static definedness residual gets a
+    -- dynamic discharge attempt (substitute the match, simplify, re-check) before being
+    -- rejected. Set False for the discharge's own nested simplification, so the attempt
+    -- is at most one level deep (no recursive dynamic discharge).
     }
 
 data EquationState = EquationState
@@ -367,6 +372,7 @@ runEquationT definition llvmApi smtSolver sCache known (EquationT m) = do
                         , maxLocalSteps = globalEquationOptions.maxLocalSteps
                         , logger
                         , prettyModifiers
+                        , dischargeDefinedness = True
                         }
     -- NB the returned cache assumes the known predicates
     pure (res, endState.cache)
@@ -923,6 +929,45 @@ applyEquations theory handler term = do
                     )
                     err
 
+{- | Dynamic ceil discharge. Given the match substitution and a rule's leftover
+   definedness residual, substitute and simplify each obligation and report whether they
+   are now all trivially satisfied: a @#Ceil(t)@ obligation (@Right t@) when the simplified
+   term has no remaining partial sub-terms (the same "trivially defined" check used at load),
+   a predicate obligation (@Left p@) when it simplifies to @true@.
+
+   The nested simplification runs with 'dischargeDefinedness' disabled, so a rule blocked
+   during the discharge is simply not applied rather than triggering a further (recursive)
+   discharge — the attempt is at most one level deep.
+-}
+dischargeDefinednessResidual ::
+    LoggerMIO io =>
+    Substitution ->
+    [Either Predicate Term] ->
+    EquationT io Bool
+dischargeDefinednessResidual subst residual = do
+    cfg <- getConfig
+    st <- getState
+    and <$> mapM (dischargeObligation cfg st) residual
+  where
+    -- run the residual's simplification in an *isolated* equation state (fresh iteration
+    -- state, copied cache/known predicates) so it cannot corrupt the outer evaluation, and
+    -- with dynamic discharge disabled so it does not recurse (at most one level deep)
+    dischargeObligation cfg st obligation =
+        eqState . lift $ do
+            let substituted = substituteInTerm subst (either coerce id obligation)
+            (result, _) <-
+                runEquationT cfg.definition cfg.llvmApi cfg.smtSolver st.cache st.predicates $
+                    withoutDynamicDischarge (evaluateTerm' BottomUp substituted)
+            pure $ case (obligation, result) of
+                -- #Ceil(t): satisfied once the simplified term has no partial sub-terms
+                (Right{}, Right simplified) -> null (collectUndefinedSubterms simplified)
+                -- predicate obligation: satisfied once it simplifies to true
+                (Left{}, Right simplified) -> simplified == TrueBool
+                (_, Left _) -> False
+
+    withoutDynamicDischarge (EquationT m) =
+        EquationT $ withReaderT (\cfg -> cfg{dischargeDefinedness = False}) m
+
 applyEquation ::
     forall io tag.
     LoggerMIO io =>
@@ -941,17 +986,22 @@ applyEquation term rule =
                         logMessage ("Equation with existentials" :: Text)
                     lift . throw . InternalError $
                         "Equation with existentials: " <> Text.pack (show rule)
-                -- immediately cancel if not preserving definedness
-                unless (null rule.computedAttributes.notPreservesDefinednessReasons) $ do
-                    throwE
-                        ( \ctxt ->
-                            ctxt $
-                                logMessage $
-                                    renderOneLineText $
-                                        "Uncertain about definedness of rule due to:"
-                                            <+> hsep (intersperse "," $ map pretty rule.computedAttributes.notPreservesDefinednessReasons)
-                        , RuleNotPreservingDefinedness
-                        )
+                let rejectNotPreservingDefinedness =
+                        throwE
+                            ( \ctxt ->
+                                ctxt $
+                                    logMessage $
+                                        renderOneLineText $
+                                            "Uncertain about definedness of rule due to:"
+                                                <+> hsep (intersperse "," $ map pretty rule.computedAttributes.notPreservesDefinednessReasons)
+                            , RuleNotPreservingDefinedness
+                            )
+                -- A non-empty static definedness residual blocks the rule. When dynamic
+                -- discharge is enabled we defer the decision to after matching (where the
+                -- match substitution is available); otherwise we reject up front.
+                unless (null rule.definednessResidual) $ do
+                    discharge <- (.dischargeDefinedness) <$> lift getConfig
+                    unless discharge rejectNotPreservingDefinedness
                 -- immediately cancel if rule has concrete() flag and term has variables
                 when (allMustBeConcrete rule.attributes.concreteness && not (Set.null (freeVariables term))) $ do
                     throwE
@@ -1006,6 +1056,14 @@ applyEquation term rule =
                                                     Map.toList subst
                                         )
 
+                        -- dynamic ceil discharge: substitute the match into the (non-empty)
+                        -- static residual and try to simplify it to trivially-satisfied before
+                        -- committing to the rule. One level deep: the nested simplification runs
+                        -- with discharge disabled, so it does not itself attempt discharge.
+                        unless (null rule.definednessResidual) $ do
+                            discharged <- lift $ dischargeDefinednessResidual subst rule.definednessResidual
+                            unless discharged rejectNotPreservingDefinedness
+
                         -- check required constraints from lhs.
                         -- Reaction on false/indeterminate varies depending on the equation's type (function/simplification),
                         -- see @handleSimplificationEquation@ and @handleFunctionEquation@

booster/library/Booster/Pattern/Util.hs

@@ -19,6 +19,7 @@ module Booster.Pattern.Util (
     checkTermSymbols,
     isConcrete,
     filterTermSymbols,
+    collectUndefinedSubterms,
     sizeOfTerm,
     termVarStats,
     termSymbolStats,
@@ -268,6 +269,60 @@ filterTermSymbols check = cata $ \case
                 more ->
                     filter check [concatSym, elemSym] <> fromMaybe [] rest <> concat more
 
+{- | Collect the maximal sub-terms rooted at a partial (non-total, non-constructor)
+   symbol — the rule's runtime definedness obligations (each collected term must not
+   evaluate to bottom).  The traversal mirrors @'filterTermSymbols' (not . 'isDefinedSymbol')@
+   case-for-case, so the result is empty exactly when that scan finds no partial symbol;
+   where the scan would report a (partial) collection meta-symbol, the whole collection
+   term is returned as the obligation.
+-}
+collectUndefinedSubterms :: Term -> [Term]
+collectUndefinedSubterms = go
+  where
+    partial = not . isDefinedSymbol
+    go t = case t of
+        SymbolApplication sym _ args
+            | partial sym -> [t]
+            | otherwise -> concatMap go args
+        AndTerm t1 t2 -> go t1 <> go t2
+        DomainValue{} -> []
+        Var{} -> []
+        Injection _ _ inner -> go inner
+        KMap def [] Nothing -> [t | partial (unitSymbol $ KMapMeta def)]
+        KMap def [(k, v)] Nothing -> go k <> go v <> [t | partial (kmapElementSymbol def)]
+        KMap _ [] (Just rest) -> go rest
+        KMap def kvs rest ->
+            [t | partial (concatSymbol $ KMapMeta def) || partial (kmapElementSymbol def)]
+                <> concatMap (\(k, v) -> go k <> go v) kvs
+                <> maybe [] go rest
+        KList def heads Nothing -> case heads of
+            [] -> [t | partial (unitSymbol $ KListMeta def)]
+            [x] -> [t | partial (klistElementSymbol def)] <> go x
+            more ->
+                [t | partial (concatSymbol $ KListMeta def) || partial (klistElementSymbol def)]
+                    <> concatMap go more
+        KList def heads (Just (mid, tails)) ->
+            go mid
+                <> ( let ends = heads <> tails
+                      in if null ends
+                            then []
+                            else
+                                [t | partial (concatSymbol $ KListMeta def) || partial (klistElementSymbol def)]
+                                    <> concatMap go ends
+                   )
+        KSet def elements rest -> case elements of
+            [] -> maybe [t | partial (unitSymbol $ KSetMeta def)] go rest
+            [single] ->
+                go single
+                    <> maybe
+                        [t | partial (klistElementSymbol def)]
+                        (\r -> [t | partial (concatSymbol $ KSetMeta def) || partial (klistElementSymbol def)] <> go r)
+                        rest
+            more ->
+                [t | partial (concatSymbol $ KSetMeta def) || partial (klistElementSymbol def)]
+                    <> maybe [] go rest
+                    <> concatMap go more
+
 -- | Calculate size of a term in bytes
 sizeOfTerm :: Term -> Int
 sizeOfTerm = cata $ \case