From 22978d3b5e5b508d0fe6a6bbc6e2d402e1a7021a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jun 2026 13:33:56 +0000 Subject: [PATCH 1/7] booster/Pattern/ApplyEquations, {GlobalState,CLOptions}, unit-tests/Pattern/ApplyEquations: local-fixpoint evaluation behind --equation-local-fixpoint MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit iterateEquations restarts the full term traversal whenever any node changes, and within a pass a successful application's RHS is not re-evaluated at its position. Each firing therefore triggers a whole-term sweep in which every ancestor of the changed node is a novel term and parents match against unevaluated RHS redexes — a sweep multiplier on equation attempts that grows with the length of causal rewrite chains. Behind the new --equation-local-fixpoint flag (default off, for A/B measurement), the BottomUp equation pass wraps its evaluation hook: when a node is rewritten, run the LLVM pass on the result (preserving the LLVM-before-equations ordering of the global loop) and re-enter the cached recursion on it, normalizing the new subtree in place. Ancestors then see children in final form and the global loop converges in 1-2 passes instead of one per causal chain step. Whole-term snapshots no longer catch node-level oscillations, so the chain of local rewrites along the current path is tracked in a path-scoped localSteps stack (saved/restored around each local recursion, reset for nested predicate evaluation) and checked per step, throwing EquationLoop; maxIterations keeps counting global passes only, so TooManyIterations semantics and its partial result are unchanged. traverseTerm itself is untouched (it is shared with the LLVM and path-condition passes). Validation: with the flag on, a causal chain of depth 101 that exceeds the global-pass limit today normalizes in a single pass, the loopDef oscillation is still detected as EquationLoop, and standard scenarios give identical results. The flag-window test is sequenced after the iteration-limit test it would otherwise race with (the test binary runs tests in parallel). Full unit suite passes; test-retain-condition-cache passes with byte-identical output with --equation-local-fixpoint enabled. Co-Authored-By: Claude Fable 5 --- booster/library/Booster/CLOptions.hs | 6 +++ booster/library/Booster/GlobalState.hs | 9 +++- .../library/Booster/Pattern/ApplyEquations.hs | 50 +++++++++++++++++-- .../Test/Booster/Pattern/ApplyEquations.hs | 45 +++++++++++++++++ 4 files changed, 105 insertions(+), 5 deletions(-) diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs index 122dfaabab..72a1a7cd7a 100644 --- a/booster/library/Booster/CLOptions.hs +++ b/booster/library/Booster/CLOptions.hs @@ -417,6 +417,12 @@ parseEquationOptions = <> value defaultMaxRecursion <> showDefault ) + <*> switch + ( long "equation-local-fixpoint" + <> help + "Normalize rewritten subterms in place instead of restarting \ + \the term traversal from the top after every change" + ) where defaultMaxIterations = 100 defaultMaxRecursion = 5 diff --git a/booster/library/Booster/GlobalState.hs b/booster/library/Booster/GlobalState.hs index b40dc4026e..4214ff0036 100644 --- a/booster/library/Booster/GlobalState.hs +++ b/booster/library/Booster/GlobalState.hs @@ -13,6 +13,9 @@ import Booster.Util (Bound (..)) data EquationOptions = EquationOptions { maxIterations :: Bound "Iterations" , maxRecursion :: Bound "Recursion" + , localFixpoint :: Bool + -- ^ normalize rewritten subterms in place instead of restarting + -- the traversal from the top after every change } deriving stock (Show, Eq) @@ -20,7 +23,11 @@ data EquationOptions = EquationOptions globalEquationOptions :: IORef EquationOptions globalEquationOptions = unsafePerformIO . newIORef $ - EquationOptions{maxIterations = 100, maxRecursion = 5} + EquationOptions + { maxIterations = 100 + , maxRecursion = 5 + , localFixpoint = False + } readGlobalEquationOptions :: IO EquationOptions readGlobalEquationOptions = readIORef globalEquationOptions diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index dd4a573185..9995c4e1ae 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -149,6 +149,7 @@ data EquationConfig = EquationConfig , smtSolver :: SMT.SMTContext , maxRecursion :: Bound "Recursion" , maxIterations :: Bound "Iterations" + , localFixpoint :: Bool , logger :: Logger LogMessage , prettyModifiers :: ModifiersRep } @@ -156,6 +157,10 @@ data EquationConfig = EquationConfig data EquationState = EquationState { termStack :: Seq Term , recursionStack :: [Term] + , localSteps :: [Term] + -- ^ chain of locally-rewritten node values on the current + -- traversal path, for loop detection in local-fixpoint mode + -- (path-scoped: saved and restored around each local recursion) , changed :: Bool , predicates :: Set Predicate , cache :: SimplifierCache @@ -193,6 +198,7 @@ startState cache known = EquationState { termStack = mempty , recursionStack = [] + , localSteps = [] , changed = False , predicates = known , -- replacements from predicates are rebuilt from the path conditions every time @@ -353,6 +359,7 @@ runEquationT definition llvmApi smtSolver sCache known (EquationT m) = do , smtSolver , maxIterations = globalEquationOptions.maxIterations , maxRecursion = globalEquationOptions.maxRecursion + , localFixpoint = globalEquationOptions.localFixpoint , logger , prettyModifiers } @@ -406,13 +413,47 @@ iterateEquations direction preference startTerm = do in simp llvmResult -- evaluate functions and simplify (recursively at each level) newTerm <- - let simp = cached Equations $ traverseTerm direction simp (applyHooksAndEquations preference) + let onEval + | config.localFixpoint && direction == BottomUp = localFixpointEval simp + | otherwise = applyHooksAndEquations preference + simp = cached Equations $ traverseTerm direction simp onEval in simp replacedTerm changeFlag <- getChanged if changeFlag then checkForLoop newTerm >> resetChanged >> go newTerm else pure llvmResult + {- Local-fixpoint evaluation (only in BottomUp mode, behind + --equation-local-fixpoint): when a node was rewritten, run the + LLVM pass on the result (preserving the LLVM-before-equations + ordering the global loop provides) and re-enter the cached + recursion on it, normalizing the new subtree in place instead + of restarting the whole-term traversal. Ancestors then see + children in final form and the global loop converges in 1-2 + passes instead of one per causal chain step. + + The whole-term snapshots on the term stack no longer catch + node-level oscillations (a -> b -> a), so the chain of local + rewrites along the current path is tracked in 'localSteps' and + checked per step. The stack is path-scoped by save/restore; + 'maxIterations' keeps counting global passes only. + -} + localFixpointEval :: LoggerMIO io => (Term -> EquationT io Term) -> Term -> EquationT io Term + localFixpointEval recurse t = do + t' <- applyHooksAndEquations preference t + if t' == t + then pure t + else do + priorSteps <- (.localSteps) <$> getState + when (t' `elem` priorSteps) $ do + withContext CtxAbort $ do + logWarn "Equation loop detected (local fixpoint)." + throw . EquationLoop . reverse $ t' : priorSteps + eqState . modify $ \s -> s{localSteps = t' : s.localSteps} + result <- llvmSimplify t' >>= recurse + eqState . modify $ \s -> s{localSteps = priorSteps} + pure result + llvmSimplify :: forall io. LoggerMIO io => Term -> EquationT io Term llvmSimplify term = do config <- getConfig @@ -1201,9 +1242,10 @@ simplifyConstraint' recurseIntoEvalBool = \case evalBool :: LoggerMIO io => Term -> EquationT io Term evalBool t = withTermContext t $ do prior <- getState -- save prior state so we can revert - eqState $ put prior{termStack = mempty, changed = False} + eqState $ put prior{termStack = mempty, changed = False, localSteps = []} result <- iterateEquations BottomUp PreferFunctions t - -- reset change flag and term stack to prior values + -- reset change flag, term stack, and local steps to prior values -- (keep the updated cache and added predicates, if any) - eqState $ modify $ \s -> s{changed = prior.changed, termStack = prior.termStack} + eqState $ modify $ \s -> + s{changed = prior.changed, termStack = prior.termStack, localSteps = prior.localSteps} pure result diff --git a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index b2353bae83..0ff3b1a425 100644 --- a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -12,9 +12,11 @@ module Test.Booster.Pattern.ApplyEquations ( test_simplify, test_simplifyPattern, test_simplifyConstraint, + test_localFixpoint, test_errors, ) where +import Control.Exception (finally) import Control.Monad.Logger (runNoLoggingT) import Data.ByteString (ByteString) import Data.Map (Map) @@ -25,6 +27,11 @@ import Test.Tasty.HUnit import Booster.Definition.Attributes.Base import Booster.Definition.Base +import Booster.GlobalState ( + EquationOptions (..), + readGlobalEquationOptions, + writeGlobalEquationOptions, + ) import Booster.Pattern.ApplyEquations import Booster.Pattern.Base import Booster.Pattern.Bool @@ -226,6 +233,44 @@ test_simplifyConstraint = ns <- noSolver runNoLoggingT $ fst <$> simplifyConstraint testDefinition Nothing ns mempty mempty t +test_localFixpoint :: TestTree +test_localFixpoint = + -- must run after the iteration-limit test ("Recursive evaluation"), + -- whose outcome the temporary flag window below would change if the + -- two ran concurrently (the test binary runs tests in parallel) + after AllFinish "Recursive evaluation" $ + testCase "Local fixpoint mode normalizes causal chains in one pass" $ do + defaults <- readGlobalEquationOptions + writeGlobalEquationOptions defaults{localFixpoint = True} + runChecks `finally` writeGlobalEquationOptions defaults + where + runChecks = do + -- standard scenarios give identical results + evalWith funDef [trm| f1{}(con2{}(A:SomeSort{})) |] + >>= (@?= Right [trm| con2{}(A:SomeSort{}) |]) + evalWith simplDef (app con1 [app con2 [app f2 [a]]]) + >>= (@?= Right (app con2 [app f2 [a]])) + -- a causal chain of depth 101 exceeds the global-pass limit + -- without local fixpoints (one whole-term pass per chain + -- step, see "Recursive evaluation"), but normalizes in a + -- single pass here + let subj depth = app f1 [iterate (apply con1) start !! depth] + start = app con2 [a] + n `times` f = foldr (.) id (replicate n $ apply f) + evalWith funDef (subj 101) >>= (@?= Right (101 `times` con2 $ start)) + -- node-level oscillation is detected per local step + isLoop =<< evalWith loopDef (app f1 [app con1 [a]]) + + a = var "A" someSort + apply f = app f . (: []) + + isLoop (Left (EquationLoop _)) = pure () + isLoop other = assertFailure $ "Expected an equation loop, got " <> show other + + evalWith def t = do + ns <- noSolver + runNoLoggingT $ fst <$> evaluateTerm BottomUp def Nothing ns mempty mempty t + test_errors :: TestTree test_errors = testGroup From 6c4a88077bf492508b17076c90026f007b289d0a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jun 2026 18:35:41 +0000 Subject: [PATCH 2/7] booster/Pattern/ApplyEquations, {GlobalState,CLOptions}, unit-tests/Pattern/ApplyEquations: replace the local-fixpoint flag with a per-pass budget, on by default (--equation-max-local-steps) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Bool flag forked evaluation into two strategies and left the in-place recursion unbounded (a single pass could apply arbitrarily many equations, with loop detection as the only brake). Replace it with a budget: at most maxLocalSteps in-place rewrites per traversal pass (--equation-max-local-steps, default 20, chosen on the expectation that a few applications normalize a side condition to its final truth value). On exhaustion, rewritten nodes are returned without recursion — exactly the restart-only strategy — and the global loop picks them up on the next pass. Restart-only evaluation is therefore the budget-0 special case of a single code path rather than a separate mode, the new strategy is the default, and total work is again bounded by maxIterations passes times (budget plus one application per node), with TooManyIterations and its partial result reached as before. Loop detection becomes two-layered: the path-scoped per-step check catches oscillations shorter than the budget immediately, and cycles that survive a pass boundary recur in the existing whole-term snapshots within at most one cycle period of passes (a period dividing the budget repeats the snapshot on the very next pass). Validation: bottom-up chains beyond the old one-application-per-pass limit complete with defaults; a lowered pass limit with the default budget still aborts an over-long chain with a partial result; budget 0 reproduces the old depth-100/101 success/abort boundary exactly; oscillations are detected per local step with the budget on and by whole-term snapshots with it off. Full unit suite passes; test-retain-condition-cache produces byte-identical output with the default budget. Co-Authored-By: Claude Fable 5 --- booster/library/Booster/CLOptions.hs | 16 +++- booster/library/Booster/GlobalState.hs | 9 +- .../library/Booster/Pattern/ApplyEquations.hs | 91 +++++++++++++------ .../Test/Booster/Pattern/ApplyEquations.hs | 50 ++++++---- 4 files changed, 109 insertions(+), 57 deletions(-) diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs index 72a1a7cd7a..ee73cb9f27 100644 --- a/booster/library/Booster/CLOptions.hs +++ b/booster/library/Booster/CLOptions.hs @@ -400,7 +400,7 @@ parseSMTOptions = parseEquationOptions :: Parser EquationOptions parseEquationOptions = - (\x y -> EquationOptions (Bound x) (Bound y)) + (\x y z -> EquationOptions (Bound x) (Bound y) (Bound z)) <$> option nonnegativeInt ( metavar "ITERATION_LIMIT" @@ -417,15 +417,21 @@ parseEquationOptions = <> value defaultMaxRecursion <> showDefault ) - <*> switch - ( long "equation-local-fixpoint" + <*> option + nonnegativeInt + ( metavar "LOCAL_STEP_LIMIT" + <> long "equation-max-local-steps" <> help - "Normalize rewritten subterms in place instead of restarting \ - \the term traversal from the top after every change" + "Number of equations applied in place at rewritten subterms \ + \per traversal pass before restarting the traversal from the \ + \top (0 restores restart-only evaluation)" + <> value defaultMaxLocalSteps + <> showDefault ) where defaultMaxIterations = 100 defaultMaxRecursion = 5 + defaultMaxLocalSteps = 20 parseRewriteOptions :: Parser RewriteOptions parseRewriteOptions = diff --git a/booster/library/Booster/GlobalState.hs b/booster/library/Booster/GlobalState.hs index 4214ff0036..b7213f1a8c 100644 --- a/booster/library/Booster/GlobalState.hs +++ b/booster/library/Booster/GlobalState.hs @@ -13,9 +13,10 @@ import Booster.Util (Bound (..)) data EquationOptions = EquationOptions { maxIterations :: Bound "Iterations" , maxRecursion :: Bound "Recursion" - , localFixpoint :: Bool - -- ^ normalize rewritten subterms in place instead of restarting - -- the traversal from the top after every change + , maxLocalSteps :: Bound "LocalSteps" + -- ^ how many equations may be applied in place at rewritten + -- subterms per traversal pass before falling back to restarting + -- the traversal from the top (0 restores restart-only evaluation) } deriving stock (Show, Eq) @@ -26,7 +27,7 @@ globalEquationOptions = EquationOptions { maxIterations = 100 , maxRecursion = 5 - , localFixpoint = False + , maxLocalSteps = 20 } readGlobalEquationOptions :: IO EquationOptions diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index 9995c4e1ae..a8e6d08071 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -149,7 +149,7 @@ data EquationConfig = EquationConfig , smtSolver :: SMT.SMTContext , maxRecursion :: Bound "Recursion" , maxIterations :: Bound "Iterations" - , localFixpoint :: Bool + , maxLocalSteps :: Bound "LocalSteps" , logger :: Logger LogMessage , prettyModifiers :: ModifiersRep } @@ -159,8 +159,11 @@ data EquationState = EquationState , recursionStack :: [Term] , localSteps :: [Term] -- ^ chain of locally-rewritten node values on the current - -- traversal path, for loop detection in local-fixpoint mode + -- traversal path, for loop detection of in-place rewriting -- (path-scoped: saved and restored around each local recursion) + , localStepCount :: Int + -- ^ in-place rewrites taken in the current traversal pass, + -- bounded by 'maxLocalSteps' (reset at the start of each pass) , changed :: Bool , predicates :: Set Predicate , cache :: SimplifierCache @@ -199,6 +202,7 @@ startState cache known = { termStack = mempty , recursionStack = [] , localSteps = [] + , localStepCount = 0 , changed = False , predicates = known , -- replacements from predicates are rebuilt from the path conditions every time @@ -359,7 +363,7 @@ runEquationT definition llvmApi smtSolver sCache known (EquationT m) = do , smtSolver , maxIterations = globalEquationOptions.maxIterations , maxRecursion = globalEquationOptions.maxRecursion - , localFixpoint = globalEquationOptions.localFixpoint + , maxLocalSteps = globalEquationOptions.maxLocalSteps , logger , prettyModifiers } @@ -402,6 +406,8 @@ iterateEquations direction preference startTerm = do throw $ TooManyIterations currentCount startTerm currentTerm pushTerm currentTerm + -- each pass gets a fresh in-place rewriting budget + eqState . modify $ \s -> s{localStepCount = 0} -- simplify the term using the LLVM backend first llvmResult <- llvmSimplify currentTerm -- NB llvmSimplify is idempotent. No need to iterate if @@ -414,7 +420,7 @@ iterateEquations direction preference startTerm = do -- evaluate functions and simplify (recursively at each level) newTerm <- let onEval - | config.localFixpoint && direction == BottomUp = localFixpointEval simp + | direction == BottomUp = localFixpointEval simp | otherwise = applyHooksAndEquations preference simp = cached Equations $ traverseTerm direction simp onEval in simp replacedTerm @@ -423,20 +429,34 @@ iterateEquations direction preference startTerm = do then checkForLoop newTerm >> resetChanged >> go newTerm else pure llvmResult - {- Local-fixpoint evaluation (only in BottomUp mode, behind - --equation-local-fixpoint): when a node was rewritten, run the - LLVM pass on the result (preserving the LLVM-before-equations - ordering the global loop provides) and re-enter the cached - recursion on it, normalizing the new subtree in place instead - of restarting the whole-term traversal. Ancestors then see - children in final form and the global loop converges in 1-2 - passes instead of one per causal chain step. - - The whole-term snapshots on the term stack no longer catch - node-level oscillations (a -> b -> a), so the chain of local - rewrites along the current path is tracked in 'localSteps' and - checked per step. The stack is path-scoped by save/restore; - 'maxIterations' keeps counting global passes only. + {- Local-fixpoint evaluation (BottomUp mode): when a node was + rewritten, run the LLVM pass on the result (preserving the + LLVM-before-equations ordering the global loop provides) and + re-enter the cached recursion on it, normalizing the new + subtree in place instead of restarting the whole-term + traversal. Ancestors then see children in final form and the + global loop converges in a few passes instead of one per + causal chain step. + + The in-place rewriting effort is bounded: at most + 'maxLocalSteps' rewrites per traversal pass; once the budget + is exhausted, rewritten nodes are returned without recursion, + which is exactly the restart-only strategy (the changed flag + is already set, so the global loop picks the node up on the + next pass). Total work per evaluation therefore stays bounded + by 'maxIterations' passes times ('maxLocalSteps' plus one + application per node), and 'TooManyIterations' with its + partial result is reached as before. A budget of 0 restores + the restart-only strategy entirely. + + Loop detection is two-layered: the chain of in-place rewrites + along the current path is tracked in 'localSteps' (path-scoped + by save/restore) and checked per step, catching oscillations + shorter than the budget immediately; cycles that survive a + pass boundary recur in the whole-term snapshots within at most + one cycle period of passes and are caught by 'checkForLoop' + (a cycle period dividing the budget repeats the snapshot on + the very next pass). -} localFixpointEval :: LoggerMIO io => (Term -> EquationT io Term) -> Term -> EquationT io Term localFixpointEval recurse t = do @@ -444,15 +464,23 @@ iterateEquations direction preference startTerm = do if t' == t then pure t else do - priorSteps <- (.localSteps) <$> getState - when (t' `elem` priorSteps) $ do - withContext CtxAbort $ do - logWarn "Equation loop detected (local fixpoint)." - throw . EquationLoop . reverse $ t' : priorSteps - eqState . modify $ \s -> s{localSteps = t' : s.localSteps} - result <- llvmSimplify t' >>= recurse - eqState . modify $ \s -> s{localSteps = priorSteps} - pure result + config <- getConfig + st <- getState + if coerce st.localStepCount >= config.maxLocalSteps + then pure t' -- budget exhausted: defer to the global loop + else do + when (t' `elem` st.localSteps) $ do + withContext CtxAbort $ do + logWarn "Equation loop detected (local fixpoint)." + throw . EquationLoop . reverse $ t' : st.localSteps + eqState . modify $ \s -> + s + { localSteps = t' : s.localSteps + , localStepCount = s.localStepCount + 1 + } + result <- llvmSimplify t' >>= recurse + eqState . modify $ \s -> s{localSteps = st.localSteps} + pure result llvmSimplify :: forall io. LoggerMIO io => Term -> EquationT io Term llvmSimplify term = do @@ -1242,10 +1270,15 @@ simplifyConstraint' recurseIntoEvalBool = \case evalBool :: LoggerMIO io => Term -> EquationT io Term evalBool t = withTermContext t $ do prior <- getState -- save prior state so we can revert - eqState $ put prior{termStack = mempty, changed = False, localSteps = []} + eqState $ put prior{termStack = mempty, changed = False, localSteps = [], localStepCount = 0} result <- iterateEquations BottomUp PreferFunctions t -- reset change flag, term stack, and local steps to prior values -- (keep the updated cache and added predicates, if any) eqState $ modify $ \s -> - s{changed = prior.changed, termStack = prior.termStack, localSteps = prior.localSteps} + s + { changed = prior.changed + , termStack = prior.termStack + , localSteps = prior.localSteps + , localStepCount = prior.localStepCount + } pure result diff --git a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index 0ff3b1a425..c86d3fadee 100644 --- a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -76,9 +76,11 @@ test_evaluateFunction = n `times` f = foldr (.) id (replicate n $ apply f) -- top-down evaluation: a single iteration is enough eval TopDown (subj 101) @?>>= Right (101 `times` con2 $ a) - -- bottom-up evaluation: `depth` many iterations + -- bottom-up evaluation: each pass advances the chain by + -- the in-place rewriting budget, so depths beyond the old + -- one-application-per-pass limit complete now eval BottomUp (subj 100) @?>>= Right (100 `times` con2 $ a) - isTooManyIterations =<< eval BottomUp (subj 101) + eval BottomUp (subj 101) @?>>= Right (101 `times` con2 $ a) , -- con3(f1(con2(a)), f1(con1(con2(b)))) => con3(con2(a), con2(con2(b))) testCase "Several function calls inside a constructor" $ do eval TopDown [trm| con3{}(f1{}(con2{}(A:SomeSort{})), f1{}(con1{}(con2{}(B:SomeSort{})))) |] @@ -236,30 +238,37 @@ test_simplifyConstraint = test_localFixpoint :: TestTree test_localFixpoint = -- must run after the iteration-limit test ("Recursive evaluation"), - -- whose outcome the temporary flag window below would change if the - -- two ran concurrently (the test binary runs tests in parallel) + -- whose outcome the temporary budget-0 window below would change + -- if the two ran concurrently (the test binary runs tests in + -- parallel) after AllFinish "Recursive evaluation" $ - testCase "Local fixpoint mode normalizes causal chains in one pass" $ do + testCase "In-place rewriting: loop detection, and budget 0 restores restart-only evaluation" $ do + -- with the default budget, node-level oscillation is + -- detected per local step (cycle shorter than the budget) + isLoop =<< evalWith loopDef (app f1 [app con1 [a]]) + -- with a budget of 0, evaluation degrades to the + -- restart-only strategy: one application per pass, so the + -- depth-101 chain exceeds the pass limit again defaults <- readGlobalEquationOptions - writeGlobalEquationOptions defaults{localFixpoint = True} - runChecks `finally` writeGlobalEquationOptions defaults + writeGlobalEquationOptions defaults{maxLocalSteps = 0} + legacyChecks `finally` writeGlobalEquationOptions defaults where - runChecks = do - -- standard scenarios give identical results - evalWith funDef [trm| f1{}(con2{}(A:SomeSort{})) |] - >>= (@?= Right [trm| con2{}(A:SomeSort{}) |]) - evalWith simplDef (app con1 [app con2 [app f2 [a]]]) - >>= (@?= Right (app con2 [app f2 [a]])) - -- a causal chain of depth 101 exceeds the global-pass limit - -- without local fixpoints (one whole-term pass per chain - -- step, see "Recursive evaluation"), but normalizes in a - -- single pass here + legacyChecks = do let subj depth = app f1 [iterate (apply con1) start !! depth] start = app con2 [a] n `times` f = foldr (.) id (replicate n $ apply f) - evalWith funDef (subj 101) >>= (@?= Right (101 `times` con2 $ start)) - -- node-level oscillation is detected per local step + evalWith funDef (subj 100) >>= (@?= Right (100 `times` con2 $ start)) + isTooMany =<< evalWith funDef (subj 101) + -- oscillations are still caught, by the whole-term snapshots isLoop =<< evalWith loopDef (app f1 [app con1 [a]]) + -- the combined bound (passes times per-pass budget plus one + -- application per node) still terminates evaluation with a + -- partial result: with 10 passes and the default budget of 20, + -- a chain of depth 300 cannot finish + defaults <- readGlobalEquationOptions + writeGlobalEquationOptions defaults{maxIterations = 10, maxLocalSteps = 20} + (isTooMany =<< evalWith funDef (subj 300)) + `finally` writeGlobalEquationOptions defaults a = var "A" someSort apply f = app f . (: []) @@ -267,6 +276,9 @@ test_localFixpoint = isLoop (Left (EquationLoop _)) = pure () isLoop other = assertFailure $ "Expected an equation loop, got " <> show other + isTooMany (Left (TooManyIterations _ _ _)) = pure () + isTooMany other = assertFailure $ "Expected an iteration-limit abort, got " <> show other + evalWith def t = do ns <- noSolver runNoLoggingT $ fst <$> evaluateTerm BottomUp def Nothing ns mempty mempty t From 8ec10df6f3bfb6ccd01c866a3787e98a7527c800 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jun 2026 22:57:47 +0000 Subject: [PATCH 3/7] booster/unit-tests/Pattern/ApplyEquations: fix pedantic build (unused binding, ambiguous record updates) The --pedantic CI build (-Werror) rejected the leftover isTooManyIterations helper, unused since the iteration-limit test moved into the budget-0 window, and the EquationOptions record updates, which are ambiguous under DuplicateRecordFields because the field names are shared with EquationConfig. Construct the options explicitly instead. Co-Authored-By: Claude Fable 5 --- .../Test/Booster/Pattern/ApplyEquations.hs | 21 +++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index c86d3fadee..27e708f214 100644 --- a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -109,10 +109,6 @@ test_evaluateFunction = ns <- noSolver runNoLoggingT $ fst <$> evaluateTerm direction funDef Nothing ns mempty mempty t - isTooManyIterations (Left (TooManyIterations _n _ _)) = pure () - isTooManyIterations (Left err) = assertFailure $ "Unexpected error " <> show err - isTooManyIterations (Right r) = assertFailure $ "Unexpected result" <> show r - test_simplify :: TestTree test_simplify = testGroup @@ -249,8 +245,16 @@ test_localFixpoint = -- with a budget of 0, evaluation degrades to the -- restart-only strategy: one application per pass, so the -- depth-101 chain exceeds the pass limit again + -- explicit construction instead of record update: the + -- field names are shared with EquationConfig, making an + -- update ambiguous under DuplicateRecordFields defaults <- readGlobalEquationOptions - writeGlobalEquationOptions defaults{maxLocalSteps = 0} + writeGlobalEquationOptions + EquationOptions + { maxIterations = defaults.maxIterations + , maxRecursion = defaults.maxRecursion + , maxLocalSteps = 0 + } legacyChecks `finally` writeGlobalEquationOptions defaults where legacyChecks = do @@ -266,7 +270,12 @@ test_localFixpoint = -- partial result: with 10 passes and the default budget of 20, -- a chain of depth 300 cannot finish defaults <- readGlobalEquationOptions - writeGlobalEquationOptions defaults{maxIterations = 10, maxLocalSteps = 20} + writeGlobalEquationOptions + EquationOptions + { maxIterations = 10 + , maxRecursion = defaults.maxRecursion + , maxLocalSteps = 20 + } (isTooMany =<< evalWith funDef (subj 300)) `finally` writeGlobalEquationOptions defaults From 7e136282bbcbecfeb4b5a02d6b9a6f10ee0d9418 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jun 2026 22:57:56 +0000 Subject: [PATCH 4/7] booster/test/rpc-integration/test-log-simplify-json: update simplify-log golden for in-place evaluation In-place evaluation attempts the INT.lt hook directly at the rewritten constraint subterm (logged failure on the symbolic argument) and the later simplify pass no longer re-attempts it (cache hit). Log-trace changes only; all RPC responses are unchanged. Co-Authored-By: Claude Fable 5 --- .../test-log-simplify-json/simplify-log.txt.golden | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden index 7eb8a46402..f5a58da3ca 100644 --- a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden +++ b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden @@ -48,10 +48,10 @@ {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]]}} {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"success",{"term":"8f1e2b8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}}} +{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"fd81940"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} -{"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},"simplify",{"term":"50120f3"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} From 9b9557658f0cf963945bd692d3c3e0aa37e19748 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jun 2026 23:27:01 +0000 Subject: [PATCH 5/7] booster/{GlobalState,CLOptions}, unit-tests/Pattern/ApplyEquations: default --equation-max-local-steps to 0 (restart-only) Make the in-place budget opt-in so the default behavior is identical to the existing restart-only evaluation strategy. The unit tests now pin the legacy iteration-limit boundary at the default and exercise the in-place behaviors (deeper chains, per-step loop detection, combined bound) in an explicit budget-20 window. The test-log-simplify-json golden reverts to the upstream trace, guarding that the default changes nothing. Co-Authored-By: Claude Fable 5 --- booster/library/Booster/CLOptions.hs | 4 +- booster/library/Booster/GlobalState.hs | 5 +- .../simplify-log.txt.golden | 2 +- .../Test/Booster/Pattern/ApplyEquations.hs | 48 ++++++++++--------- 4 files changed, 32 insertions(+), 27 deletions(-) diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs index ee73cb9f27..106b3126bb 100644 --- a/booster/library/Booster/CLOptions.hs +++ b/booster/library/Booster/CLOptions.hs @@ -424,14 +424,14 @@ parseEquationOptions = <> help "Number of equations applied in place at rewritten subterms \ \per traversal pass before restarting the traversal from the \ - \top (0 restores restart-only evaluation)" + \top (0, the default, is restart-only evaluation)" <> value defaultMaxLocalSteps <> showDefault ) where defaultMaxIterations = 100 defaultMaxRecursion = 5 - defaultMaxLocalSteps = 20 + defaultMaxLocalSteps = 0 parseRewriteOptions :: Parser RewriteOptions parseRewriteOptions = diff --git a/booster/library/Booster/GlobalState.hs b/booster/library/Booster/GlobalState.hs index b7213f1a8c..e9a8c72a0b 100644 --- a/booster/library/Booster/GlobalState.hs +++ b/booster/library/Booster/GlobalState.hs @@ -16,7 +16,8 @@ data EquationOptions = EquationOptions , maxLocalSteps :: Bound "LocalSteps" -- ^ how many equations may be applied in place at rewritten -- subterms per traversal pass before falling back to restarting - -- the traversal from the top (0 restores restart-only evaluation) + -- the traversal from the top (0, the default, is restart-only + -- evaluation) } deriving stock (Show, Eq) @@ -27,7 +28,7 @@ globalEquationOptions = EquationOptions { maxIterations = 100 , maxRecursion = 5 - , maxLocalSteps = 20 + , maxLocalSteps = 0 } readGlobalEquationOptions :: IO EquationOptions diff --git a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden index f5a58da3ca..7eb8a46402 100644 --- a/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden +++ b/booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden @@ -48,10 +48,10 @@ {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"},"match","failure","break"],"message":{"remainder":[[{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"},{"tag":"App","name":"Lbl'Unds-LT-Eqls'Int'Unds'","sorts":[],"args":[{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}},{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"}]}]]}} {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"detail"],"message":"...include/imp-semantics/imp-verification.k : (24, 10)"} {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"simplification":"2499eab08be5a893dde1183881ad2aee18a0aab6fc53deb2c78f94c6466e3e15"},"success",{"term":"8f1e2b8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"App","name":"Lbl'Unds-LT-'Int'Unds'","sorts":[],"args":[{"tag":"DV","sort":{"tag":"SortApp","name":"SortInt","args":[]},"value":"0"},{"tag":"EVar","name":"VarN","sort":{"tag":"SortApp","name":"SortInt","args":[]}}]}}} -{"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"473c428"},{"rewrite":"029649977a189d0740b894b184f10ed8b77b043ff935d356dca9fa87ffbffc58"},"constraint",{"term":"fbb3d17"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"fd81940"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} +{"context":[{"request":"4"},"booster","execute",{"term":"d3dc513"},"simplify",{"term":"50120f3"},{"hook":"INT.lt"},"failure"],"message":"Hook returned no result"} {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"detail"],"message":"UNKNOWN"} {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"function":"f4c2469bcff9527515b6d36f16040307917bda61067d10b85fb531e142483bee"},"success",{"term":"98b0892"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"true"}}} {"context":[{"request":"4"},"booster","execute",{"term":"ee3511f"},{"rewrite":"2821768ca76231d9d23da884f160f8a8a67b03f3575f41bd4fc76649c39a94fb"},"constraint",{"term":"d2e9706"},{"hook":"BOOL.not"},"success",{"term":"9eb81e8"},"kore-term"],"message":{"format":"KORE","version":1,"term":{"tag":"DV","sort":{"tag":"SortApp","name":"SortBool","args":[]},"value":"false"}}} diff --git a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index 27e708f214..3c14409a41 100644 --- a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -76,11 +76,11 @@ test_evaluateFunction = n `times` f = foldr (.) id (replicate n $ apply f) -- top-down evaluation: a single iteration is enough eval TopDown (subj 101) @?>>= Right (101 `times` con2 $ a) - -- bottom-up evaluation: each pass advances the chain by - -- the in-place rewriting budget, so depths beyond the old - -- one-application-per-pass limit complete now + -- bottom-up evaluation: with the default in-place budget + -- of 0, each pass advances the chain by one application, + -- so the iteration limit caps the chain depth eval BottomUp (subj 100) @?>>= Right (100 `times` con2 $ a) - eval BottomUp (subj 101) @?>>= Right (101 `times` con2 $ a) + isTooManyIterations =<< eval BottomUp (subj 101) , -- con3(f1(con2(a)), f1(con1(con2(b)))) => con3(con2(a), con2(con2(b))) testCase "Several function calls inside a constructor" $ do eval TopDown [trm| con3{}(f1{}(con2{}(A:SomeSort{})), f1{}(con1{}(con2{}(B:SomeSort{})))) |] @@ -109,6 +109,10 @@ test_evaluateFunction = ns <- noSolver runNoLoggingT $ fst <$> evaluateTerm direction funDef Nothing ns mempty mempty t + isTooManyIterations (Left (TooManyIterations _n _ _)) = pure () + isTooManyIterations (Left err) = assertFailure $ "Unexpected error " <> show err + isTooManyIterations (Right r) = assertFailure $ "Unexpected result" <> show r + test_simplify :: TestTree test_simplify = testGroup @@ -234,17 +238,15 @@ test_simplifyConstraint = test_localFixpoint :: TestTree test_localFixpoint = -- must run after the iteration-limit test ("Recursive evaluation"), - -- whose outcome the temporary budget-0 window below would change + -- whose outcome the temporary budget window below would change -- if the two ran concurrently (the test binary runs tests in -- parallel) after AllFinish "Recursive evaluation" $ - testCase "In-place rewriting: loop detection, and budget 0 restores restart-only evaluation" $ do - -- with the default budget, node-level oscillation is - -- detected per local step (cycle shorter than the budget) + testCase "In-place rewriting: deeper chains, loop detection, and bounded effort" $ do + -- at the default budget of 0 (restart-only evaluation), + -- node-level oscillation is detected by the whole-term + -- snapshots of the global passes isLoop =<< evalWith loopDef (app f1 [app con1 [a]]) - -- with a budget of 0, evaluation degrades to the - -- restart-only strategy: one application per pass, so the - -- depth-101 chain exceeds the pass limit again -- explicit construction instead of record update: the -- field names are shared with EquationConfig, making an -- update ambiguous under DuplicateRecordFields @@ -253,31 +255,33 @@ test_localFixpoint = EquationOptions { maxIterations = defaults.maxIterations , maxRecursion = defaults.maxRecursion - , maxLocalSteps = 0 + , maxLocalSteps = 20 } - legacyChecks `finally` writeGlobalEquationOptions defaults + budgetChecks defaults `finally` writeGlobalEquationOptions defaults where - legacyChecks = do + budgetChecks :: EquationOptions -> IO () + budgetChecks defaults = do let subj depth = app f1 [iterate (apply con1) start !! depth] start = app con2 [a] n `times` f = foldr (.) id (replicate n $ apply f) - evalWith funDef (subj 100) >>= (@?= Right (100 `times` con2 $ start)) - isTooMany =<< evalWith funDef (subj 101) - -- oscillations are still caught, by the whole-term snapshots + -- each pass advances a chain by the budget plus one + -- application, so depths beyond the restart-only limit of + -- maxIterations complete now + evalWith funDef (subj 101) >>= (@?= Right (101 `times` con2 $ start)) + -- node-level oscillation is detected per local step (cycle + -- shorter than the budget) isLoop =<< evalWith loopDef (app f1 [app con1 [a]]) -- the combined bound (passes times per-pass budget plus one -- application per node) still terminates evaluation with a - -- partial result: with 10 passes and the default budget of 20, - -- a chain of depth 300 cannot finish - defaults <- readGlobalEquationOptions + -- partial result: with 10 passes and a budget of 20, a chain + -- of depth 300 cannot finish writeGlobalEquationOptions EquationOptions { maxIterations = 10 , maxRecursion = defaults.maxRecursion , maxLocalSteps = 20 } - (isTooMany =<< evalWith funDef (subj 300)) - `finally` writeGlobalEquationOptions defaults + isTooMany =<< evalWith funDef (subj 300) a = var "A" someSort apply f = app f . (: []) From 2cebb60e9212d52005c36d586ef7ae2783429095 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jun 2026 23:49:55 +0000 Subject: [PATCH 6/7] docs/2024-10-18-booster-description, CLAUDE.md: document the pass-restart loop and the --equation-max-local-steps budget The booster description's equation section now explains the restart-from-top pass structure that was previously implicit (and described as hard-coded), and how the in-place budget generalises it. Also fixes a typo (traverser) in the strategy bullets. Co-Authored-By: Claude Fable 5 --- CLAUDE.md | 4 ++++ docs/2024-10-18-booster-description.md | 6 ++++-- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index a6ecda6464..801433a187 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -172,6 +172,10 @@ CLI flags for these fields are defined in `booster/tools/booster/Server.hs` in - Traverses bottom-up, applies function/simplification equations. - Concrete sub-terms are sent to the LLVM backend for evaluation (top-down first to maximise batch size). +- Passes restart from the top until a fixed point (bounded by + `--equation-max-iterations`); `--equation-max-local-steps N` additionally + re-simplifies rewritten sub-terms in place, up to N equation applications + per pass (default 0 = restart-only). **Term representation** (`Booster/Pattern/Base.hs`): - `Term` is a tagged union with a `TermAttributes` field tracking `isConstructorLike`, diff --git a/docs/2024-10-18-booster-description.md b/docs/2024-10-18-booster-description.md index c49a9794f1..1f50f7b500 100644 --- a/docs/2024-10-18-booster-description.md +++ b/docs/2024-10-18-booster-description.md @@ -229,11 +229,13 @@ The simplification code path is used at two different points of the execution, a Concrete function evaluation is handled by the LLVM backend and thus requires the semantics to be written in such a way, so as to be able to build both the kore definition used by the haskell backend, as well as the LLVM kore definition. The booster relies on the LLVM version of a semantics, compiled as a dynamic library, which is loaded when the server starts. During simplification, the term is traversed bottom up and any concrete sub-terms are sent to he LLVM backend to be evaluated. -The symbolic parts of a term are handled directly by the booster. Similarly to rewrite rules, function rules may also have side conditions. As a result, the simplifier may have to recurse into evaluating whether the side-condition of a function/simplification rule evaluates to true/false before successfully rewriting the term. At the moment, the evaluation strategy is hard-coded in the booster, and it is generally is the following: +The symbolic parts of a term are handled directly by the booster. Similarly to rewrite rules, function rules may also have side conditions. As a result, the simplifier may have to recurse into evaluating whether the side-condition of a function/simplification rule evaluates to true/false before successfully rewriting the term. The evaluation strategy is generally the following: - traverse the term top-down once and apply LLVM simplifications to the concrete sub-terms. It is essential to discover the concrete terms top-down and thus track the concreteness of sub-terms with attributes. By doing that, we make sure that we send a few big terms to the LLVM backend and not many small terms, thus minimising the overhead. -- traverser the term bottom-up, applying equations at every level until we make progress with at least one equation; +- traverse the term bottom-up, applying equations at every level until we make progress with at least one equation; - when applying equations, prefer functions, and only apply simplifications when function do not produce a result anymore, i.e. no functions apply. +These traversal passes restart from the top of the term after every pass that changed it, until a fixed point is reached or the pass limit (`--equation-max-iterations`, default 100) aborts evaluation. By default, a rewrite chain at a single position therefore advances by one equation application per pass. The `--equation-max-local-steps N` option generalises this: when an equation rewrites a sub-term, the result is re-simplified in place (LLVM evaluation plus re-entering the bottom-up traversal) for up to `N` equation applications per pass before deferring back to the restart loop, so chains of side-condition evaluations can complete at the sub-term where they arise instead of paying one global pass per step. `N = 0` (the default) is exactly the restart-only behaviour. Total effort remains bounded by the pass limit times the per-pass budget, and equation loops are detected both per local step (cycles shorter than the budget) and by whole-term snapshots across passes (cycles longer than the budget). + **TODO**: discuss the abort conditions of function vs. simplifications. In short, simplifications are optional, and functions are mandatory, i.e. we abort if a function equation produces an indeterminate match or a function condition is indeterminate. **TODO**: discuss the process of applying a single equation. **TODO**: discuss caching and how it's implemented in Booster. From 3def8ed7490e059c15ae16e72afde1ae55ce833e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 11 Jun 2026 13:11:53 +0000 Subject: [PATCH 7/7] booster/Pattern/ApplyEquations, {GlobalState,CLOptions}, docs: path-scope the in-place budget (localStepCount == length localSteps) Per review: restore the counter together with the chain around the recursion, making the budget bound each in-place chain's depth rather than the total per pass, with localStepCount == length localSteps as a state invariant (the counter exists only to avoid computing the length per step). The per-pass reset in the global loop becomes redundant and is removed. Also use put on the captured state with a pre-forced counter instead of modify, and align the option help and docs with the per-chain budget semantics. The in-place recursion deliberately re-enters the full bottom-up traversal of the rewritten result (rather than re-applying at the rewritten node only): the rewrite builds a new subterm from the rule's RHS whose arguments need full evaluation, and the equation cache cuts the descent short at already-normal substituted subject parts. Co-Authored-By: Claude Fable 5 --- CLAUDE.md | 4 +- booster/library/Booster/CLOptions.hs | 7 +- booster/library/Booster/GlobalState.hs | 8 +-- .../library/Booster/Pattern/ApplyEquations.hs | 66 +++++++++++-------- .../Test/Booster/Pattern/ApplyEquations.hs | 18 ++--- docs/2024-10-18-booster-description.md | 2 +- 6 files changed, 59 insertions(+), 46 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index 801433a187..7dfeb2baa4 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -174,8 +174,8 @@ CLI flags for these fields are defined in `booster/tools/booster/Server.hs` in to maximise batch size). - Passes restart from the top until a fixed point (bounded by `--equation-max-iterations`); `--equation-max-local-steps N` additionally - re-simplifies rewritten sub-terms in place, up to N equation applications - per pass (default 0 = restart-only). + re-simplifies rewritten sub-terms in place, up to N chained equation + applications (default 0 = restart-only). **Term representation** (`Booster/Pattern/Base.hs`): - `Term` is a tagged union with a `TermAttributes` field tracking `isConstructorLike`, diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs index 106b3126bb..9cdd1ecb72 100644 --- a/booster/library/Booster/CLOptions.hs +++ b/booster/library/Booster/CLOptions.hs @@ -422,9 +422,10 @@ parseEquationOptions = ( metavar "LOCAL_STEP_LIMIT" <> long "equation-max-local-steps" <> help - "Number of equations applied in place at rewritten subterms \ - \per traversal pass before restarting the traversal from the \ - \top (0, the default, is restart-only evaluation)" + "Number of equations applied in place at a rewritten subterm \ + \(per chain of in-place rewrites) before restarting the \ + \traversal from the top (0, the default, is restart-only \ + \evaluation)" <> value defaultMaxLocalSteps <> showDefault ) diff --git a/booster/library/Booster/GlobalState.hs b/booster/library/Booster/GlobalState.hs index e9a8c72a0b..1a95ecf349 100644 --- a/booster/library/Booster/GlobalState.hs +++ b/booster/library/Booster/GlobalState.hs @@ -14,10 +14,10 @@ data EquationOptions = EquationOptions { maxIterations :: Bound "Iterations" , maxRecursion :: Bound "Recursion" , maxLocalSteps :: Bound "LocalSteps" - -- ^ how many equations may be applied in place at rewritten - -- subterms per traversal pass before falling back to restarting - -- the traversal from the top (0, the default, is restart-only - -- evaluation) + -- ^ how many equations may be applied in place at a rewritten + -- subterm (per chain of in-place rewrites) before falling back + -- to restarting the traversal from the top (0, the default, is + -- restart-only evaluation) } deriving stock (Show, Eq) diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index a8e6d08071..928c941afe 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/booster/library/Booster/Pattern/ApplyEquations.hs @@ -162,8 +162,9 @@ data EquationState = EquationState -- traversal path, for loop detection of in-place rewriting -- (path-scoped: saved and restored around each local recursion) , localStepCount :: Int - -- ^ in-place rewrites taken in the current traversal pass, - -- bounded by 'maxLocalSteps' (reset at the start of each pass) + -- ^ length of 'localSteps' (path-scoped like the chain itself), + -- kept separately to bound in-place rewriting by 'maxLocalSteps' + -- without computing the length on every step , changed :: Bool , predicates :: Set Predicate , cache :: SimplifierCache @@ -406,8 +407,6 @@ iterateEquations direction preference startTerm = do throw $ TooManyIterations currentCount startTerm currentTerm pushTerm currentTerm - -- each pass gets a fresh in-place rewriting budget - eqState . modify $ \s -> s{localStepCount = 0} -- simplify the term using the LLVM backend first llvmResult <- llvmSimplify currentTerm -- NB llvmSimplify is idempotent. No need to iterate if @@ -432,26 +431,32 @@ iterateEquations direction preference startTerm = do {- Local-fixpoint evaluation (BottomUp mode): when a node was rewritten, run the LLVM pass on the result (preserving the LLVM-before-equations ordering the global loop provides) and - re-enter the cached recursion on it, normalizing the new - subtree in place instead of restarting the whole-term - traversal. Ancestors then see children in final form and the - global loop converges in a few passes instead of one per - causal chain step. - - The in-place rewriting effort is bounded: at most - 'maxLocalSteps' rewrites per traversal pass; once the budget - is exhausted, rewritten nodes are returned without recursion, - which is exactly the restart-only strategy (the changed flag - is already set, so the global loop picks the node up on the - next pass). Total work per evaluation therefore stays bounded - by 'maxIterations' passes times ('maxLocalSteps' plus one - application per node), and 'TooManyIterations' with its - partial result is reached as before. A budget of 0 restores - the restart-only strategy entirely. - - Loop detection is two-layered: the chain of in-place rewrites - along the current path is tracked in 'localSteps' (path-scoped - by save/restore) and checked per step, catching oscillations + re-enter the cached bottom-up traversal on it, normalizing + everything the rewrite produced in place instead of restarting + the whole-term traversal (the rewrite builds a new subterm + from the rule's RHS, which needs full evaluation in all its + arguments; the cache cuts the descent short at substituted + subject parts that are already normal). Ancestors then see + children in final form and the global loop converges in a few + passes instead of one per causal chain step. + + The in-place rewriting effort is bounded: both 'localSteps' + and 'localStepCount' are path-scoped (saved and restored + around the recursion, maintaining the invariant + localStepCount == length localSteps), so each chain of + in-place rewrites is at most 'maxLocalSteps' deep. Once the + budget is exhausted, rewritten nodes are returned without + recursion, which is exactly the restart-only strategy (the + changed flag is already set, so the global loop picks the + node up on the next pass). Each chain therefore advances by + at most 'maxLocalSteps' plus one application per pass, total + work stays bounded by 'maxIterations' passes, and + 'TooManyIterations' with its partial result is reached as + before. A budget of 0 restores the restart-only strategy + entirely. + + Loop detection is two-layered: the in-place rewrite chain in + 'localSteps' is checked per step, catching oscillations shorter than the budget immediately; cycles that survive a pass boundary recur in the whole-term snapshots within at most one cycle period of passes and are caught by 'checkForLoop' @@ -473,13 +478,18 @@ iterateEquations direction preference startTerm = do withContext CtxAbort $ do logWarn "Equation loop detected (local fixpoint)." throw . EquationLoop . reverse $ t' : st.localSteps + let !newCount = st.localStepCount + 1 + eqState . put $ + st + { localSteps = t' : st.localSteps + , localStepCount = newCount + } + result <- llvmSimplify t' >>= recurse eqState . modify $ \s -> s - { localSteps = t' : s.localSteps - , localStepCount = s.localStepCount + 1 + { localSteps = st.localSteps + , localStepCount = st.localStepCount } - result <- llvmSimplify t' >>= recurse - eqState . modify $ \s -> s{localSteps = st.localSteps} pure result llvmSimplify :: forall io. LoggerMIO io => Term -> EquationT io Term diff --git a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs index 3c14409a41..d8cb3ed9b2 100644 --- a/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs +++ b/booster/unit-tests/Test/Booster/Pattern/ApplyEquations.hs @@ -261,20 +261,18 @@ test_localFixpoint = where budgetChecks :: EquationOptions -> IO () budgetChecks defaults = do - let subj depth = app f1 [iterate (apply con1) start !! depth] - start = app con2 [a] - n `times` f = foldr (.) id (replicate n $ apply f) -- each pass advances a chain by the budget plus one -- application, so depths beyond the restart-only limit of - -- maxIterations complete now + -- maxIterations complete now (the chain rule produces its + -- redex inside the RHS, which the in-place recursion follows) evalWith funDef (subj 101) >>= (@?= Right (101 `times` con2 $ start)) -- node-level oscillation is detected per local step (cycle -- shorter than the budget) isLoop =<< evalWith loopDef (app f1 [app con1 [a]]) - -- the combined bound (passes times per-pass budget plus one - -- application per node) still terminates evaluation with a - -- partial result: with 10 passes and a budget of 20, a chain - -- of depth 300 cannot finish + -- the combined bound (passes times the per-chain budget plus + -- one application) still terminates evaluation with a partial + -- result: with 10 passes and a budget of 20, a chain of depth + -- 300 cannot finish writeGlobalEquationOptions EquationOptions { maxIterations = 10 @@ -283,6 +281,10 @@ test_localFixpoint = } isTooMany =<< evalWith funDef (subj 300) + subj depth = app f1 [iterate (apply con1) start !! depth] + start = app con2 [a] + n `times` f = foldr (.) id (replicate n $ apply f) + a = var "A" someSort apply f = app f . (: []) diff --git a/docs/2024-10-18-booster-description.md b/docs/2024-10-18-booster-description.md index 1f50f7b500..d6d8e33ac7 100644 --- a/docs/2024-10-18-booster-description.md +++ b/docs/2024-10-18-booster-description.md @@ -234,7 +234,7 @@ The symbolic parts of a term are handled directly by the booster. Similarly to r - traverse the term bottom-up, applying equations at every level until we make progress with at least one equation; - when applying equations, prefer functions, and only apply simplifications when function do not produce a result anymore, i.e. no functions apply. -These traversal passes restart from the top of the term after every pass that changed it, until a fixed point is reached or the pass limit (`--equation-max-iterations`, default 100) aborts evaluation. By default, a rewrite chain at a single position therefore advances by one equation application per pass. The `--equation-max-local-steps N` option generalises this: when an equation rewrites a sub-term, the result is re-simplified in place (LLVM evaluation plus re-entering the bottom-up traversal) for up to `N` equation applications per pass before deferring back to the restart loop, so chains of side-condition evaluations can complete at the sub-term where they arise instead of paying one global pass per step. `N = 0` (the default) is exactly the restart-only behaviour. Total effort remains bounded by the pass limit times the per-pass budget, and equation loops are detected both per local step (cycles shorter than the budget) and by whole-term snapshots across passes (cycles longer than the budget). +These traversal passes restart from the top of the term after every pass that changed it, until a fixed point is reached or the pass limit (`--equation-max-iterations`, default 100) aborts evaluation. By default, a rewrite chain at a single position therefore advances by one equation application per pass. The `--equation-max-local-steps N` option generalises this: when an equation rewrites a sub-term, the result is re-simplified in place for up to `N` chained equation applications before deferring back to the restart loop, so chains of side-condition evaluations can complete at the sub-term where they arise instead of paying one global pass per step. `N = 0` (the default) is exactly the restart-only behaviour. The in-place step re-enters the bottom-up traversal of the rewritten result, fully evaluating the new subterm the rule's RHS produced (the descent stops early at sub-terms that are already cached as evaluated). Total effort remains bounded by the pass limit times the per-chain budget, and equation loops are detected both per local step (cycles shorter than the budget) and by whole-term snapshots across passes (cycles longer than the budget). **TODO**: discuss the abort conditions of function vs. simplifications. In short, simplifications are optional, and functions are mandatory, i.e. we abort if a function equation produces an indeterminate match or a function condition is indeterminate. **TODO**: discuss the process of applying a single equation.