From 76f320e54cb520cbdc505a47859eb36914c6f152 Mon Sep 17 00:00:00 2001 From: hhefesto Date: Tue, 15 Sep 2026 13:30:56 -0600 Subject: [PATCH 1/3] Measure the live-heap peak and report it from --meter The memory figure Meter.hs deliberately left undone. runMeter defunctionalized into a CEK machine whose values live in an explicit IntMap store: sharing is id-sharing, so the live heap is reachability from the machine's roots (environment, continuation frames, returning value) over distinct cells, and the peak is the maximum along the run. Retention needs no rule: a value a frame still holds is reachable. Steps and built tick exactly where runMeter's counters do, and the conformance suite now asserts that parity tick for tick alongside value agreement -- that is what keeps a third interpreter honest. The sizing suite repeats the check across whole sessions on the corpus inputs, and checks there that the adaptive bracket holds the exact peak. Gate branches stay syntax in their frame, so the unchosen branch is never evaluated, same as the other evaluators. Two sweep policies: every allocation (exact, for tests) and adaptive (amortized, brackets the peak between a reached figure and a never- exceeded one). Sweeps drop unreachable nodes, which is what makes the bracket's upper end valid. The metered loop runs at the adaptive cadence, so a metered session now prints the peak alongside the step and build counts. The hand-computed fixtures pin what "live" means: a literal pair is its three cells; an argument referenced twice is counted once (a tree count of the same result reads 7 for a peak of 5); and a transient the result drops still shows up, growing with its size -- the retention case the sibling project's cost algebra could not see. The README's metered sample is refreshed from a measured run: its step and build counts had drifted. Profiling output joins .gitignore. --- .gitignore | 3 + README.md | 28 +-- app/Main.hs | 12 +- src/Telomare/Driver.hs | 9 + src/Telomare/Eval/Meter.hs | 17 +- src/Telomare/Eval/Space.hs | 354 +++++++++++++++++++++++++++++++++++++ telomare.cabal | 3 + test/ConformanceTests.hs | 20 +++ test/SizingTest.hs | 3 + test/SpaceTests.hs | 104 +++++++++++ 10 files changed, 528 insertions(+), 25 deletions(-) create mode 100644 src/Telomare/Eval/Space.hs create mode 100644 test/SpaceTests.hs diff --git a/.gitignore b/.gitignore index d4bf188..43191ff 100644 --- a/.gitignore +++ b/.gitignore @@ -16,3 +16,6 @@ dev-profile* .direnv/ # compiled programs written next to their sources by `telomare --compile` *.telc +# GHC profiling output (+RTS -p / -h) +*.prof +*.hp diff --git a/README.md b/README.md index 1f60d41..0be2864 100644 --- a/README.md +++ b/README.md @@ -83,22 +83,26 @@ index differently — a count is per instantiation, a nesting row is per `{test, recursion, last}` as written — so they do not line up row by row, and the report says so. -`--meter` runs the program and reports what the run cost — steps taken, and -term nodes built. Those are measurements of one run, not predictions about the -next: +`--meter` runs the program and reports what the run cost — steps taken, term +nodes built, and the live-heap peak. Those are measurements of one run, not +predictions about the next: ```sh $ printf '3 4\n' | cabal run telomare -- --meter simpleplus.tel -steps (measured): 46652 -nodes built (measured): 13660 +steps (measured): 46566 +nodes built (measured): 13577 +live heap peak (measured): 9430..9887 cells ``` -Neither is a memory figure, deliberately. Telomare's evaluator shares -environments rather than copying them, so counting the term it holds as a tree -counts shared structure once per reference — for `tictactoe.tel` that reads -about 1.2TB for a run that fits in a few GB. An honest memory figure needs -reachability over distinct nodes, which is not implemented; use `+RTS -s` for -the real thing. +The peak is a memory figure in the language's own units — a cell is one +value node, not a byte — and the reason it took until now is worth a +sentence: telomare's evaluator shares environments rather than copying them, +so counting the term it holds as a tree counts shared structure once per +reference — for `tictactoe.tel` that reads about 1.2TB for a run that fits in +a few GB. The peak is instead measured on an explicit store, as reachability +over *distinct* nodes from what the machine still holds, and it is printed as +a bracket — a figure the run reached and one it never exceeded — because the +measuring sweep is amortized rather than run at every allocation. When sizing fails, the error names the recursion, where it is, and which of the two failures it is — a budget that was too small, or an input that nothing @@ -367,7 +371,7 @@ pipeline. In pipeline order: | Resolve | `Telomare.Resolve` | resolves typed module imports, scope-checks only `DesugaredSurfaceTerm`, performs de Bruijn conversion and hash folding, and lowers core terms (`splitExpr`: `Term2 -> Term3`). Documents the dual `process`/`processWlet` pipeline. | | Type check | `Telomare.TypeCheck` | unification-based check of `Term3` against the main type. | | Size (totality) | `Telomare.Size`, `Telomare.Size.IR`, `Telomare.Machine` | telomare's distinguishing stage: `sizeTermM` abstractly interprets the program over symbolic input and infers a finite iteration count for every recursion site, then bakes the counts in (`Term3 -> CompiledExpr`). A program that cannot be sized does not compile. `Machine` is the shared step-algebra the sizing pass and the evaluators are assembled from. | -| Evaluate | `Telomare.Eval.Reference`, `Telomare.Eval.Meter`, `Telomare.Fast` | the reference interpreter, the step-counting meter, and the fuel-based fast path (which skips sizing). | +| Evaluate | `Telomare.Eval.Reference`, `Telomare.Eval.Meter`, `Telomare.Eval.Space`, `Telomare.Fast` | the reference interpreter, the step-counting meter, the space machine that also measures the live-heap peak, and the fuel-based fast path (which skips sizing). | | Drive | `Telomare.Driver`, `Telomare.Artifact`, `Telomare.Certificate`, `Telomare.Levels` | orchestration (`compileModules`, `evalLoop`), `.telc` artifacts, and the static report. | The IR vocabulary shared by all stages lives under `Telomare.IR.*` diff --git a/app/Main.hs b/app/Main.hs index 460ea33..fd14d5c 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -15,8 +15,8 @@ import Telomare.Artifact (Artifact (..), isArtifactPath, nodeCount, readArtifact, sourcesHash, telcExtension, writeArtifact) import Telomare.Certificate (renderStaticReport) -import Telomare.Driver (compileModules, evalLoop, evalLoopMetered) -import Telomare.Eval.Meter (renderMeter) +import Telomare.Driver (compileModules, evalLoop, evalLoopSpaceMetered) +import Telomare.Eval.Space (renderSpaceMeter) import Telomare.Fast (compileFast, defaultFastFuel, renderFastMeter, runFastLoop) import Telomare.IR.Loc (locatedNameText) @@ -148,8 +148,8 @@ runArtifact path action mode = do Certificate -> putStr $ artifactCertificate artifact Run -> evalLoop (artifactExpr artifact) Meter -> do - measured <- evalLoopMetered [] (artifactExpr artifact) - reportMeter $ renderMeter measured <> "\n" + measured <- evalLoopSpaceMetered [] (artifactExpr artifact) + reportMeter $ renderSpaceMeter measured <> "\n" -- |An artifact outlives the checkout it came from, so a hash mismatch is worth -- saying and never worth refusing over. @@ -176,8 +176,8 @@ runSized file action = do Run -> evalLoop sized Certificate -> putStr $ staticReport Nothing (Just report) allModules entryModule Meter -> do - measured <- evalLoopMetered [] sized - reportMeter $ renderMeter measured <> "\n" + measured <- evalLoopSpaceMetered [] sized + reportMeter $ renderSpaceMeter measured <> "\n" Compile output -> do let path = fromMaybe (replaceExtension file telcExtension) output certificate = staticReport Nothing (Just report) allModules entryModule diff --git a/src/Telomare/Driver.hs b/src/Telomare/Driver.hs index e6973e2..b68763b 100644 --- a/src/Telomare/Driver.hs +++ b/src/Telomare/Driver.hs @@ -18,6 +18,7 @@ import Telomare.Desugar (desugarTerm) import Telomare.Error import Telomare.Eval.Meter (Meter, evalMeter) import Telomare.Eval.Reference () +import Telomare.Eval.Space (SpaceMeter, SweepPolicy (SweepAdaptive), evalSpace) import Telomare.Expand (expandDefs, expandModule, expandTerm, renderExpansionError, wrapMain) import Telomare.IR.Base @@ -276,6 +277,14 @@ evalLoopWithInput inputList iexpr = snd <$> evalLoopCore plainEval iexpr keepAcc evalLoopMetered :: [String] -> CompiledExpr -> IO Meter evalLoopMetered manualInput expr = fst <$> evalLoopCore evalMeter expr printAccum "" manualInput +-- |`evalLoopMetered` with the space meter: same session, and the measurement +-- carries the live-heap peak alongside the step and build counts. The +-- adaptive sweep keeps the measuring overhead amortized-constant; what it +-- costs in return is a bracketed peak rather than a pinned one. +evalLoopSpaceMetered :: [String] -> CompiledExpr -> IO SpaceMeter +evalLoopSpaceMetered manualInput expr = + fst <$> evalLoopCore (evalSpace SweepAdaptive) expr printAccum "" manualInput + -- |Same as `evalLoop`, but keeping what was displayed. evalLoop_ :: CompiledExpr -> IO String evalLoop_ iexpr = snd <$> evalLoopCore plainEval iexpr keepAccum "" [] diff --git a/src/Telomare/Eval/Meter.hs b/src/Telomare/Eval/Meter.hs index 4527af5..fe6b45a 100644 --- a/src/Telomare/Eval/Meter.hs +++ b/src/Telomare/Eval/Meter.hs @@ -8,7 +8,7 @@ -- iteration counts that the sizing pass already infers -- (`Telomare.Eval.renderSizingCertificate`). -- --- == Why there is no memory figure +-- == Why there is no memory figure here -- -- There was one, and it was wrong, in a way worth recording so it is not -- reintroduced. Telomare evaluates by rewriting a term, so it is tempting to @@ -22,13 +22,16 @@ -- This is the same shape as the dead end recorded in the sibling project's -- @design/SPACE.md@, one level further down. There, a cost algebra could not -- see /retention/; here, a tree metric cannot see /sharing/. A real figure --- needs reachability over distinct nodes — hash-consing, not arithmetic — and --- is deliberately left undone rather than approximated. For actual memory, run --- the binary under @+RTS -s@. +-- needs reachability over distinct nodes, and that is what +-- `Telomare.Eval.Space` now measures: this same interpreter defunctionalized +-- over an explicit store, where sharing is id-sharing and the live heap is +-- what the machine's roots reach. @--meter@ reports its peak. This module +-- stays as it is — the fast mirror whose step and build counts the space +-- machine must match tick for tick, which is what keeps both honest. -- --- `meterBuilt` is what survives of the idea: a count of the nodes the run --- constructs. It is well defined without any sharing analysis, and it still --- shows how much term-building a program does. +-- `meterBuilt` is a count of the nodes the run constructs. It is well defined +-- without any sharing analysis, and it still shows how much term-building a +-- program does. -- -- == Substitution -- diff --git a/src/Telomare/Eval/Space.hs b/src/Telomare/Eval/Space.hs new file mode 100644 index 0000000..12c1f8e --- /dev/null +++ b/src/Telomare/Eval/Space.hs @@ -0,0 +1,354 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE LambdaCase #-} + +-- |The memory figure `Telomare.Eval.Meter` deliberately leaves undone: the +-- live-heap peak of a concrete run, measured over /distinct/ nodes. +-- +-- The evaluator binds one environment that every `EnvSF` in a body refers to, +-- so what a run holds is a graph with heavy sharing, and counting it as a tree +-- overcounts by orders of magnitude (see the Meter module header for the +-- numbers). This module measures instead of counting: it is the same +-- interpreter as `Telomare.Eval.Meter.runMeter`, defunctionalized into a +-- CEK-style machine whose values live in an explicit store keyed by node id. +-- Sharing is id-sharing — an `EnvSF` resolves to the id the environment was +-- allocated under, never to a copy — so "live heap" is reachability from the +-- machine's roots (the environment, the continuation frames, and the value +-- being returned) over distinct ids, and the peak is the maximum live figure +-- along the run. Retention needs no special handling: a value held by a frame +-- while a sibling evaluates is reachable from that frame, so it is counted for +-- exactly as long as something can still use it. +-- +-- The unit is the /cell/: one value node — `ZeroN`, `PairN`, `GateN`, +-- `AbortN`, a `DeferN` (a reference to static code, which itself weighs +-- nothing), or an `AbortedN` at one cell plus its data payload. +-- +-- Being a third interpreter, this can drift. What keeps it honest is that +-- `spSteps` and `spBuilt` tick in exactly the places `runMeter`'s counters do, +-- and `test/ConformanceTests.hs` asserts both the computed value and those two +-- counts agree with the Meter on every corpus program. The lazy gate branches +-- are load-bearing here as they are there: a `KGate` frame holds its branches +-- as syntax and only the chosen one is ever evaluated. +-- +-- Sweeping the store at every allocation makes the peak exact but costs a +-- reachability walk per allocation; `SweepAdaptive` amortizes that away +-- (sweep when the cells allocated since the last sweep exceed half the last +-- live figure) at the price of bracketing the true peak between +-- `spPeakLower` and `spPeakUpper`. Unreachable nodes are dropped at each +-- sweep, which is what makes the upper end of the bracket valid: between +-- sweeps the store only grows, so no intermediate live set can exceed the +-- last live figure plus the cells allocated since. +module Telomare.Eval.Space where + +import Data.Foldable (asum) +import Data.Functor.Foldable (cata, project) +import Data.IntMap.Strict (IntMap) +import qualified Data.IntMap.Strict as IntMap +import qualified Data.IntSet as IntSet +import Numeric.Natural (Natural) + +import Telomare.Eval.Meter (identityFunction) +import Telomare.IR.Base +import Telomare.IR.Core +import Telomare.Machine (doLeft, doRight) + +-- |A key into the store. Distinctness of ids is what makes the live figure a +-- graph measure rather than a tree measure. +type NodeId = Int + +-- |A value in the store. Only values live here; code stays syntax, so a +-- `DeferN` is one cell however large its body is. +data Node + = ZeroN + | PairN !NodeId !NodeId + | DeferN !FunctionIndex CompiledExpr + | GateN + | AbortN + | AbortedN BasicExpr + deriving (Eq, Show) + +-- |What a node holds live, in cells. +cellCost :: Node -> Natural +cellCost = \case + AbortedN payload -> 1 + basicSize payload + _ -> 1 + where + basicSize :: BasicExpr -> Natural + basicSize = cata $ \case + ZeroSF -> 1 + PairSF a b -> 1 + a + b + +-- |The store children a node keeps reachable. +nodeChildren :: Node -> [NodeId] +nodeChildren = \case + PairN a b -> [a, b] + _ -> [] + +-- |When to measure. Exact costs a reachability walk per allocation; adaptive +-- amortizes it and brackets the peak instead of pinning it. +data SweepPolicy = SweepEveryAlloc | SweepAdaptive + deriving (Eq, Show) + +-- |What a run cost, now with a memory figure. +data SpaceMeter = SpaceMeter + { spSteps :: !Natural + -- ^Evaluation steps taken; ticks where `Telomare.Eval.Meter.meterSteps` does. + , spBuilt :: !Natural + -- ^Term nodes constructed; ticks where `Telomare.Eval.Meter.meterBuilt` does. + , spPeakLower :: !Natural + -- ^A live figure the run actually reached. + , spPeakUpper :: !Natural + -- ^A figure the run never exceeded. Equal to `spPeakLower` under + -- `SweepEveryAlloc`. + , spAborts :: !Natural + -- ^How many aborted values the run constructed. Nonzero means some check + -- failed along the way — even when the result is fine, because an aborted + -- value bound eagerly and never used is simply retained and dropped. The + -- static bound covers refinement-valid runs, so this is what tells a + -- harness which runs it may compare. + } + deriving (Eq, Show) + +-- |Across a session the totals accumulate and the peaks are the worst +-- iteration's, since each iteration starts from a fresh store. +instance Semigroup SpaceMeter where + a <> b = SpaceMeter + { spSteps = spSteps a + spSteps b + , spBuilt = spBuilt a + spBuilt b + , spPeakLower = max (spPeakLower a) (spPeakLower b) + , spPeakUpper = max (spPeakUpper a) (spPeakUpper b) + , spAborts = spAborts a + spAborts b + } + +instance Monoid SpaceMeter where + mempty = SpaceMeter 0 0 0 0 0 + +-- |What to print for a measured run. +renderSpaceMeter :: SpaceMeter -> String +renderSpaceMeter m = "steps (measured): " <> show (spSteps m) + <> "\nnodes built (measured): " <> show (spBuilt m) + <> "\nlive heap peak (measured): " <> peak <> " cells" + where + peak = if spPeakLower m == spPeakUpper m + then show (spPeakLower m) + else show (spPeakLower m) <> ".." <> show (spPeakUpper m) + +-- |What the machine still has to do with the value it is returning. +data Frame + = KPairRight CompiledExpr + -- ^The first pair component is coming back; evaluate the second next. + | KPairLeft !NodeId + -- ^The first component, held live while the second evaluates. + | KGate CompiledExpr CompiledExpr + -- ^The scrutinee is coming back. The branches stay syntax so the + -- unchosen one is never evaluated — load-bearing, see the Meter header. + | KLeft + | KRight + | KSetEnv + | KRestoreEnv !(Maybe NodeId) + -- ^A function body is coming back; restore the caller's environment. The + -- saved environment is a root: the caller can still use it. + +frameRoots :: Frame -> [NodeId] +frameRoots = \case + KPairLeft a -> [a] + KRestoreEnv (Just e) -> [e] + _ -> [] + +data MachSt = MachSt + { mStore :: !(IntMap Node) + , mNext :: !NodeId + , mEnv :: !(Maybe NodeId) + , mFrames :: ![Frame] + , mSteps :: !Natural + , mBuilt :: !Natural + , mPeakLow :: !Natural + , mPeakHigh :: !Natural + , mAborts :: !Natural + , mLastLive :: !Natural + -- ^Live cells at the last sweep; the store holds exactly the live nodes + -- then, since sweeps drop the unreachable ones. + , mDebt :: !Natural + -- ^Cells allocated since the last sweep. + } + +emptySt :: MachSt +emptySt = MachSt IntMap.empty 0 Nothing [] 0 0 0 0 0 0 0 + +step :: MachSt -> MachSt +step st = st { mSteps = mSteps st + 1 } + +builtTick :: MachSt -> MachSt +builtTick st = st { mBuilt = mBuilt st + 1 } + +abortTick :: MachSt -> MachSt +abortTick st = st { mAborts = mAborts st + 1 } + +-- |Mark from the roots and take the measure; drop what was not reached. +sweep :: Bool -- ^Exact: the store is measured at every allocation, so the + -- live figure /is/ the bound. + -> [NodeId] -> MachSt -> MachSt +sweep exact extraRoots st = + let roots = extraRoots + <> foldMap pure (mEnv st) + <> concatMap frameRoots (mFrames st) + reachable = mark (mStore st) IntSet.empty roots + live = IntSet.foldr (\i acc -> acc + cellCost (mStore st IntMap.! i)) 0 reachable + upperCandidate = if exact then live else mLastLive st + mDebt st + in st { mStore = IntMap.restrictKeys (mStore st) reachable + , mPeakLow = max (mPeakLow st) live + , mPeakHigh = max (mPeakHigh st) upperCandidate + , mLastLive = live + , mDebt = 0 + } + where + mark _ visited [] = visited + mark store visited (i : rest) + | IntSet.member i visited = mark store visited rest + | otherwise = mark store (IntSet.insert i visited) + (nodeChildren (store IntMap.! i) <> rest) + +-- |Put a node in the store; sweep if the policy says it is time. The fresh id +-- is a root — nothing else holds it yet. +alloc :: SweepPolicy -> Node -> MachSt -> (NodeId, MachSt) +alloc policy node st = + let i = mNext st + st1 = st { mStore = IntMap.insert i node (mStore st) + , mNext = i + 1 + , mDebt = mDebt st + cellCost node + } + due = case policy of + SweepEveryAlloc -> True + SweepAdaptive -> mDebt st1 > max 1024 (mLastLive st1 `div` 2) + in (i, if due then sweep (policy == SweepEveryAlloc) [i] st1 else st1) + +-- |Evaluate, measuring. The machine is `Telomare.Eval.Meter.runMeter` with +-- its continuations made explicit, which is what lets a sweep see its roots. +evalSpace :: SweepPolicy -> CompiledExpr -> (SpaceMeter, Either RunTimeError CompiledExpr) +evalSpace policy expr = + let (finalSt, root) = evalC emptySt expr + -- Fold the remaining debt into the peak before reading the result back. + settledSt = sweep (policy == SweepEveryAlloc) [root] finalSt + result = readback (mStore settledSt) root + measured = SpaceMeter + { spSteps = mSteps settledSt + , spBuilt = mBuilt settledSt + , spPeakLower = mPeakLow settledSt + , spPeakUpper = mPeakHigh settledSt + , spAborts = mAborts settledSt + } + in (measured, case findAborted result of + Just e -> Left $ AbortRunTime e + Nothing -> Right result) + where + look st i = mStore st IntMap.! i + + settle st n = let (i, st') = alloc policy n (step st) in retC st' i + + allocRet st n = let (i, st') = alloc policy n st in retC st' i + + push f st = st { mFrames = f : mFrames st } + + -- The `GateSwitch` case must come before the generic `SetEnvSF` one: a + -- gate switch is a `SetEnv` shape, and taking it apart generically would + -- evaluate both branches. + evalC !st whole = case project whole of + GateSwitch l r s -> evalC (push (KGate l r) st) s + BasicFW ZeroSF -> settle st ZeroN + BasicFW (PairSF a b) -> evalC (push (KPairRight b) st) a + StuckFW (DeferSF fi body) -> settle st (DeferN fi body) + StuckFW GateSF -> settle st GateN + StuckFW (LeftSF x) -> evalC (push KLeft st) x + StuckFW (RightSF x) -> evalC (push KRight st) x + StuckFW (SetEnvSF x) -> evalC (push KSetEnv st) x + StuckFW EnvSF -> case mEnv st of + Just i -> retC (step st) i + Nothing -> unhandled "unapplied environment reference" + AbortFW AbortF -> settle st AbortN + AbortFW (AbortedF e) -> settle (abortTick st) (AbortedN e) + _ -> error "Telomare.Eval.Space.evalSpace: unexpected expression" + + retC !st v = case mFrames st of + [] -> (st, v) + KPairRight b : k -> evalC (st { mFrames = KPairLeft v : k }) b + KPairLeft a : k -> + allocRet (step (builtTick (st { mFrames = k }))) (PairN a v) + KGate l r : k -> + let st1 = step (st { mFrames = k }) + in case look st1 v of + AbortedN _ -> retC st1 v + ZeroN -> evalC (step st1) l + PairN _ _ -> evalC (step st1) r + _ -> unhandled "gate on a non-data scrutinee" + KLeft : k -> projRet (st { mFrames = k }) v $ \case + PairN l _ -> Just l + _ -> Nothing + KRight : k -> projRet (st { mFrames = k }) v $ \case + PairN _ r -> Just r + _ -> Nothing + KSetEnv : k -> + let st1 = st { mFrames = k } + in case look st1 v of + AbortedN _ -> retC (step st1) v + PairN f e -> applyC st1 f e + _ -> unhandled "SetEnv of something that is not a pair" + KRestoreEnv saved : k -> + retC (st { mEnv = saved, mFrames = k }) v + + projRet st v pick = + let st1 = step st + in case look st1 v of + AbortedN _ -> retC st1 v + ZeroN -> retC st1 v + n -> case pick n of + Just i -> retC st1 i + Nothing -> unhandled "projection of something that is not a pair" + + applyC st f e = case (look st f, look st e) of + (AbortedN _, _) -> retC (step st) f + (_, AbortedN _) -> retC (step st) e + -- `assert` on a passing value yields the identity function. + (AbortN, ZeroN) -> allocRet (step st) (deferNode identityFunction) + (AbortN, _) -> + allocRet (abortTick (builtTick (step st))) (AbortedN (truncateData (mStore st) e)) + (GateN, ZeroN) -> allocRet (step st) (deferNode doLeft) + (GateN, PairN _ _) -> allocRet (step st) (deferNode doRight) + -- The body's environment is now `e`; nothing is copied, so every + -- `EnvSF` in the body resolves to this same id. + (DeferN _ body, _) -> + evalC ((step st) { mFrames = KRestoreEnv (mEnv st) : mFrames st + , mEnv = Just e }) body + _ -> unhandled "application of something that is not a function" + + unhandled why = error $ "Telomare.Eval.Space: " <> why + + findAborted = cata $ \case + AbortFW (AbortedF e) -> Just e + x -> asum x + +-- |The store view of a known function value. +deferNode :: CompiledExpr -> Node +deferNode x = case project x of + StuckFW (DeferSF fi body) -> DeferN fi body + _ -> error "Telomare.Eval.Space.deferNode: not a function" + +-- |What an abort keeps of its argument: the data, with anything else read as +-- zero. Mirrors the Meter's @truncateToData@. +truncateData :: IntMap Node -> NodeId -> BasicExpr +truncateData store = go where + go :: NodeId -> BasicExpr + go i = case store IntMap.! i of + PairN a b -> PairB (go a) (go b) + _anything -> ZeroB + +-- |The result as a term again, so the callers of the plain evaluator work +-- unchanged. Shared substructure is materialized per reference, exactly as +-- the tree evaluators would have built it. +readback :: IntMap Node -> NodeId -> CompiledExpr +readback store = go where + go i = case store IntMap.! i of + ZeroN -> ZeroB + PairN a b -> PairB (go a) (go b) + DeferN fi body -> StuckEE (DeferSF fi body) + GateN -> StuckEE GateSF + AbortN -> AbortEE AbortF + AbortedN e -> AbortEE (AbortedF e) diff --git a/telomare.cabal b/telomare.cabal index 8238895..412aeb3 100644 --- a/telomare.cabal +++ b/telomare.cabal @@ -38,6 +38,7 @@ library , Telomare.Lexical , Telomare.Machine , Telomare.Eval.Meter + , Telomare.Eval.Space , Telomare.Expand , Telomare.Parse , Telomare.PrettyPrint @@ -186,10 +187,12 @@ test-suite telomare-sizing-test other-modules: ConformanceTests , RunModeTests , SizingTests + , SpaceTests build-depends: base , bytestring , containers , hspec + , recursion-schemes , telomare , strict ghc-options: -Wall -Wunused-packages -threaded -rtsopts -with-rtsopts=-N diff --git a/test/ConformanceTests.hs b/test/ConformanceTests.hs index 0fb6627..adbe33d 100644 --- a/test/ConformanceTests.hs +++ b/test/ConformanceTests.hs @@ -11,6 +11,7 @@ import Test.Hspec import Telomare.Driver (compileModules, runMainWithInput) import Telomare.Eval.Meter (Meter (..), evalMeter) +import Telomare.Eval.Space (SpaceMeter (..), SweepPolicy (..), evalSpace) import Telomare.Fast (compileFast, runFastWithInput) import Telomare.IR.Base import Telomare.IR.Core @@ -48,3 +49,22 @@ agreeOn (path, name, input) = describe name $ do meterSteps measured `shouldSatisfy` (> 0) -- A run of any length constructs at least one node. meterBuilt measured `shouldSatisfy` (> 0) + + -- The space meter is the meter defunctionalized over an explicit store, so + -- it must agree not just on the value but tick for tick on both counters — + -- that parity is what keeps the machine rewrite honest. + it "the space meter matches the meter tick for tick" $ do + modules <- loadWith path name + case compileModules modules name of + Left err -> expectationFailure $ "failed to compile:\n" <> err + Right (_, sized) -> do + let applied = appB sized ZeroB + (measured, metered) = evalMeter applied + (spaced, result) = evalSpace SweepEveryAlloc applied + fmap show result `shouldBe` fmap show metered + spSteps spaced `shouldBe` meterSteps measured + spBuilt spaced `shouldBe` meterBuilt measured + -- A run of any length holds at least one live cell, and the exact + -- policy pins the peak rather than bracketing it. + spPeakLower spaced `shouldSatisfy` (> 0) + spPeakUpper spaced `shouldBe` spPeakLower spaced diff --git a/test/SizingTest.hs b/test/SizingTest.hs index cd021ab..fd5eb35 100644 --- a/test/SizingTest.hs +++ b/test/SizingTest.hs @@ -3,6 +3,7 @@ module Main where import ConformanceTests import RunModeTests import SizingTests +import SpaceTests import Test.Hspec main :: IO () @@ -10,3 +11,5 @@ main = hspec $ do sizingSpec runModeSpec conformanceSpec + spaceSpec + sessionParitySpec diff --git a/test/SpaceTests.hs b/test/SpaceTests.hs new file mode 100644 index 0000000..df56ffb --- /dev/null +++ b/test/SpaceTests.hs @@ -0,0 +1,104 @@ +-- |Hand-computed live-heap peaks, on terms small enough to trace against the +-- machine by hand. Each figure here was derived on paper from the sweep +-- discipline in `Telomare.Eval.Space` before it was asserted; a change that +-- moves one of them is a change to what "live" means and deserves the same +-- scrutiny as a changed step count. +module SpaceTests where + +import Data.Char (ord) +import Data.Functor.Foldable (project) +import Test.Hspec + +import ConformanceTests (corpus) +import SizingTests (loadWith) + +import Telomare.Driver (compileModules) +import Telomare.Eval.Meter (Meter (..), evalMeter) +import Telomare.Eval.Space (SpaceMeter (..), SweepPolicy (..), evalSpace) +import Telomare.IR.Base +import Telomare.IR.Core (CompiledExpr) +import Telomare.Machine (appB, deferB) + +measure :: SweepPolicy -> CompiledExpr -> SpaceMeter +measure policy = fst . evalSpace policy + +-- |A unary number as data: 2n+1 cells. +unary :: Int -> CompiledExpr +unary 0 = ZeroB +unary n = PairB (unary (n - 1)) ZeroB + +spaceSpec :: Spec +spaceSpec = describe "the live-heap peak" $ do + it "counts a literal pair as its three cells" $ do + let m = measure SweepEveryAlloc (PairB ZeroB ZeroB) + spPeakLower m `shouldBe` 3 + spPeakUpper m `shouldBe` 3 + spSteps m `shouldBe` 3 + spBuilt m `shouldBe` 1 + + it "counts a shared environment once, not once per reference" $ do + -- \x -> (x, x) applied to a three-cell pair. A tree count of the result + -- reads 7 nodes; the run's peak is 5 cells (the argument pair, its two + -- zeros, the function cell, and the application pair), because both + -- references resolve to the argument's one allocation. + let f = deferB (toEnum 1) (PairB EnvB EnvB) + arg = PairB ZeroB ZeroB + m = measure SweepEveryAlloc (SetEnvB (PairB f arg)) + spPeakLower m `shouldBe` 5 + spPeakUpper m `shouldBe` 5 + + it "sees a transient the result does not keep" $ do + -- @right (n, 0)@ returns a single cell, but the run held the number + -- while the projection waited: its 2n+1 cells, the zero, and the pair. + -- The peak growing with n is what a size-of-the-result figure — or a + -- retention-blind cost algebra — would have missed. + let transientPeak n = + spPeakLower (measure SweepEveryAlloc (RightB (PairB (unary n) ZeroB))) + transientPeak 10 `shouldBe` 2 * 10 + 3 + transientPeak 200 - transientPeak 100 `shouldBe` 200 + + it "the adaptive sweep brackets the exact peak" $ do + let expr = RightB (PairB (unary 5000) ZeroB) + exact = measure SweepEveryAlloc expr + adaptive = measure SweepAdaptive expr + -- Same run, different measuring cadence. + spSteps adaptive `shouldBe` spSteps exact + spBuilt adaptive `shouldBe` spBuilt exact + spPeakLower adaptive `shouldSatisfy` (> 0) + spPeakLower adaptive `shouldSatisfy` (<= spPeakLower exact) + spPeakUpper adaptive `shouldSatisfy` (>= spPeakUpper exact) + +-- |The input as the driver builds it, at the compiled type. +str2b :: String -> CompiledExpr +str2b = foldr (PairB . unary . ord) ZeroB + +-- |Tick parity and the adaptive bracket, across a whole session on the real +-- inputs — the conformance suite checks the first, empty-input iteration only. +sessionParitySpec :: Spec +sessionParitySpec = describe "the space meter across a session" $ + mapM_ parityOn corpus + +parityOn :: (FilePath, String, [String]) -> Spec +parityOn (path, name, inputs) = it name $ do + modules <- loadWith path name + case compileModules modules name of + Left err -> expectationFailure $ "failed to compile:\n" <> err + Right (_, sized) -> loop sized ZeroB inputs + where + loop sized st inps = do + let applied = appB sized st + (metered, result) = evalMeter applied + (exact, result') = evalSpace SweepEveryAlloc applied + (adaptive, _) = evalSpace SweepAdaptive applied + fmap show result' `shouldBe` fmap show result + spSteps exact `shouldBe` meterSteps metered + spBuilt exact `shouldBe` meterBuilt metered + -- The bracket holds the pinned peak, on a real program. + spPeakLower adaptive `shouldSatisfy` (<= spPeakLower exact) + spPeakUpper adaptive `shouldSatisfy` (>= spPeakUpper exact) + case result' of + Right v | BasicFW (PairSF _ newState) <- project v + , BasicFW (PairSF _ _) <- project newState + , (i : rest) <- inps + -> loop sized (PairB (str2b i) newState) rest + _ -> pure () From 536069f6d82442d718cb6d3352c036f482ec19b1 Mon Sep 17 00:00:00 2001 From: hhefesto Date: Tue, 15 Sep 2026 13:32:36 -0600 Subject: [PATCH 2/3] Bound the live-heap peak statically, over input sizes The same machine at compile time, over an abstract input. Bounds are maxima of affine expressions in input-part sizes -- sum of c_p * |p| plus a constant -- with dominated alternatives pruned, widening to pointwise-maximum coefficients, and substitution of the sizes a refinement pins. That language is what a static answer has to be: a program's peak depends on how big its input is, so a single number would be either wrong or vacuous. Bounds are accumulated over millions of transitions, so the language is strict all the way down (strict map, strict fields, a canonical form that forces every affine and drops zero coefficients); left lazy, each accumulation retained the machine state it was made from and the walk's memory grew with its history. The walk runs on the sized term, so every recursion is a church tower it unrolls exactly its inferred count of times, and retention is measured on the abstract run by reachability rather than modelled by per-combinator rules -- the dead end the sibling project's design/SPACE.md records. The abstract input mirrors the sizing pass's initialInput: refinement-guaranteed pairs expand, refinement-guaranteed zeroes are concrete, and the rest are symbolic nodes whose cell bound is |p|. A gate on an unknown takes both branches and joins the values in a superposition whose frozen bound is the maximum of its sides' reachable subgraphs. Four things keep that from exploding, and together they are why tictactoe.tel converges -- 2.6M transitions under the default fuel, about eight seconds after sizing: - World-consistency tags, the sizing pass's filterLeft/filterRight discipline: a fork is about something -- an input path, or the id of a widened node being tested -- that commitment is in force while its branch runs, and a repeated test of the same thing dispatches to the committed side instead of re-forking. k tests of one unknown cost two worlds, not 2^k. A pair commitment on a part makes every ancestor a pair, and a zero commitment covers every part below it. - A pointwise pair merge: a superposition of two pairs joins as a pair of superpositions, sound because a maximum of sums never exceeds the sum of maxima. Closure superpositions collapse to one closure over superposed environments, and nesting depth resets at every pair. A join spends fuel like any transition, since the merge recurses through a pair's whole shape. - Widening of deep data superpositions, at supDepthCap = 4, guarded by a per-node has-function flag so a value that must still be applied is never reduced to a bound alone. Board cells touched by k moves stay bounded-depth instead of depth k, which is what keeps whoWon's nested gates from forking over an unbounded frontier. - A join memo, rare store pruning and a pin stack for ids the machine holds mid-transition, which keep the walk near 3.7M transitions a second. The measuring sweep is amortized: fresh one-cell and symbolic-input allocations enter a debt, join-produced nodes measure on the spot, and last live plus debt bounds any intermediate live set because the store only grows between sweeps. The input graph is built straight into the store, never allocated, so the walk sweeps once before its first transition: without that, every upper bound before the first sweep would omit |input|. A sweep credits each input part to the outermost reachable path above it and counts one path once -- |p| already counts everything under p, and however many nodes view one part, it is one part -- and charges the projections of one widened value once, as a family. Dead worlds -- a stuck configuration, which a typechecked, sized program never reaches on its own -- are counted, and the harness asserts none on the corpus. sizeTermM hands back the InputRestrictions it already computes (moved to Telomare.Size.IR so Telomare.Size can name the walk's types without a cycle); the sizing report carries the bound lazily, next to the walk's statistics, so a plain run never forces the walk. The artifact stores the bound and moves to version 3. Paths index the input as 2^depth and a unary character is around a hundred deep, so numbers in a bound are written as length-prefixed big-endian bytes, never through a machine word. The bound covers refinement-valid runs: a run on invalid input constructs and retains the failed check's aborted message, which is outside the restricted abstract input. The space meter now counts constructed aborted values so a harness can tell those runs apart, and the headline test asserts, on every corpus program, that the bound with actual input sizes substituted stands at or above the exactly measured peak of every abort-free iteration, and that at least one such iteration exists. Fixtures pin the walk directly: a fork that joins, a superposition widened past the cap, a widened value it refuses to apply, QuickCheck laws of the max-plus algebra, and a golden for simpleplus's rendered bound. simpleplus comes out at 116 input parts + 4337 cells; tictactoe at a maximum of two affines whose larger constant, 67,762 cells, is about three times the measured peak of a completed game -- loose where a deep superposition is widened to its bound alone, but finite and sound. --- src/Telomare/Artifact.hs | 61 +++- src/Telomare/Driver.hs | 11 +- src/Telomare/Machine.hs | 2 +- src/Telomare/Size.hs | 31 +- src/Telomare/Size/IR.hs | 14 + src/Telomare/Space/Static.hs | 670 +++++++++++++++++++++++++++++++++++ src/Telomare/SpaceBound.hs | 193 ++++++++++ telomare.cabal | 5 +- test/RunModeTests.hs | 14 + test/SizingTest.hs | 4 + test/SpaceTests.hs | 263 +++++++++++++- 11 files changed, 1247 insertions(+), 21 deletions(-) create mode 100644 src/Telomare/Space/Static.hs create mode 100644 src/Telomare/SpaceBound.hs diff --git a/src/Telomare/Artifact.hs b/src/Telomare/Artifact.hs index d78fa86..6bdcfc6 100644 --- a/src/Telomare/Artifact.hs +++ b/src/Telomare/Artifact.hs @@ -33,6 +33,7 @@ module Telomare.Artifact , isArtifactPath ) where +import Control.Monad (replicateM) import Crypto.Hash (Digest, SHA256, hash) import Data.Binary.Get (Get, getInt64le, getLazyByteString, getWord8, runGetOrFail) @@ -43,6 +44,7 @@ import Data.Functor.Foldable (cata, embed, project) import Data.List (sortOn) import Data.Map (Map) import qualified Data.Map as Map +import Numeric.Natural (Natural) import System.FilePath (takeExtension) import Telomare.IR.Base @@ -50,6 +52,7 @@ import Telomare.IR.Core import Telomare.IR.Loc import Telomare.Size (SizingReport (..)) import Telomare.Size.IR (SizedRecursion (..)) +import Telomare.SpaceBound (Affine (..), SpaceBound (..)) -- |A program with its sizing already done. data Artifact = Artifact @@ -71,7 +74,7 @@ artifactMagic = BL.pack [0x54, 0x45, 0x4C, 0x43] -- "TELC" -- |Bumped whenever the encoding changes, which invalidates older files rather -- than misreading them. artifactVersion :: Int -artifactVersion = 2 +artifactVersion = 3 telcExtension :: String telcExtension = ".telc" @@ -227,12 +230,68 @@ putReport r = do putMap putToken (putMaybe putInt') (unSizedRecursion (sizingReportCounts r)) putMap putToken putLocTag (sizingReportLocs r) putInt' (sizingReportBudget r) + putSpace (sizingReportSpace r) getReport :: Get SizingReport getReport = SizingReport . SizedRecursion <$> getMap getToken (getMaybe getInt') <*> getMap getToken getLocTag <*> getInt' + <*> getSpace + <*> pure Nothing -- the walk's statistics are not stored, only its bound + +-- The space bound. Paths grow as 2^depth and a unary character is a hundred +-- deep, so paths, coefficients and constants are written as numbers of any +-- size rather than machine words. + +putSpace :: Either String SpaceBound -> Put +putSpace = \case + Left why -> putWord8 0 >> putString why + Right (SpaceBound affines) -> putWord8 1 >> putMaybe (putList putAffine) affines + +getSpace :: Get (Either String SpaceBound) +getSpace = getWord8 >>= \case + 0 -> Left <$> getString + 1 -> Right . SpaceBound <$> getMaybe (getList getAffine) + n -> fail $ "unknown space bound tag " <> show n + +putAffine :: Affine -> Put +putAffine a = do + putMap putInteger putNatural (affCoeffs a) + putNatural (affConst a) + +getAffine :: Get Affine +getAffine = Affine <$> getMap getInteger getNatural <*> getNatural + +-- |A natural of any size: its big-endian base-256 digits, length-prefixed. +putNatural :: Natural -> Put +putNatural n = do + let bytes = digits n [] + putInt' (length bytes) + mapM_ putWord8 bytes + where + digits 0 acc = acc + digits m acc = digits (m `div` 256) (fromIntegral (m `mod` 256) : acc) + +getNatural :: Get Natural +getNatural = do + n <- getInt' + assemble 0 <$> replicateM n getWord8 + where + assemble acc [] = acc + assemble acc (w : ws) = assemble (acc * 256 + fromIntegral w) ws + +-- |A sign byte, then the magnitude. +putInteger :: Integer -> Put +putInteger i = do + putWord8 (if i < 0 then 1 else 0) + putNatural (fromInteger (abs i)) + +getInteger :: Get Integer +getInteger = do + negative <- (== 1) <$> getWord8 + n <- toInteger <$> getNatural + pure $ if negative then negate n else n -- Terms. diff --git a/src/Telomare/Driver.hs b/src/Telomare/Driver.hs index b68763b..7f9b9d4 100644 --- a/src/Telomare/Driver.hs +++ b/src/Telomare/Driver.hs @@ -34,6 +34,8 @@ import Telomare.Resolve (main2Term3, main2Term3let, process, resolveAllImports) import Telomare.Size (SizingReport (..), SizingSettings (..), buildUnsizedLocMap, evalStaticCheck, locateSizingFailure, sizeTermM, term3ToUnsizedExpr) +import Telomare.Space.Static (StaticSpaceStats (..), defaultStaticSpaceFuel, + evalSpaceStatic', renderStaticSpaceFailure) import Telomare.TypeCheck (typeCheck) import Text.Megaparsec (errorBundlePretty, runParser) @@ -79,7 +81,7 @@ findChurchSizeD so = fmap snd . findChurchSizeReporting so findChurchSizeReporting :: SizingOption -> Term3 -> Either EvalError (SizingReport, CompiledExpr) findChurchSizeReporting so t3 = case so of - NoSizing -> pure (report mempty, convertPT (const reallyBigNum) t3) + NoSizing -> pure (report mempty (Left "the program was not sized") Nothing, convertPT (const reallyBigNum) t3) UnitTestSizing -> sized (SizingSettings reallyBigNum False) MainSizing -> sized (SizingSettings reallyBigNum True) DebugSizing ss -> sized ss @@ -88,7 +90,12 @@ findChurchSizeReporting so t3 = case so of report counts = SizingReport counts locs (sizingBudget so) sized settings = case sizeTermM settings $ term3ToUnsizedExpr t3 of Left failure -> Left . RecursionLimitError $ locateSizingFailure locs failure - Right (counts, t) -> pure (report counts, t) + Right (counts, restrictions, t) -> + -- The space walk stays a thunk in the report until something reads + -- it; the bound and the statistics share that one thunk. + let stats = evalSpaceStatic' defaultStaticSpaceFuel restrictions t + space = first renderStaticSpaceFailure (ssBound <$> stats) + in pure (report counts space (Just stats), t) runStaticChecks :: CompiledExpr -> Either EvalError CompiledExpr runStaticChecks t = diff --git a/src/Telomare/Machine.hs b/src/Telomare/Machine.hs index 06c7957..78075d2 100644 --- a/src/Telomare/Machine.hs +++ b/src/Telomare/Machine.hs @@ -25,7 +25,7 @@ import qualified Data.Set as Set import Debug.Trace import Telomare.IR.Base import Telomare.PrettyPrint -import Telomare.Size.IR +import Telomare.Size.IR hiding (InputRestrictions (..)) debug :: Bool debug = False diff --git a/src/Telomare/Size.hs b/src/Telomare/Size.hs index 339c199..2ed0de6 100644 --- a/src/Telomare/Size.hs +++ b/src/Telomare/Size.hs @@ -25,7 +25,6 @@ import qualified Data.Map.Strict as Map import Control.Exception (Exception) import Control.Exception.Base (throw) import Data.Functor.Identity (Identity, runIdentity) -import Data.Set (Set) import qualified Data.Set as Set import Debug.Trace import Telomare.Error @@ -35,6 +34,8 @@ import Telomare.IR.Loc import Telomare.Machine hiding (debug, debugTrace) import Telomare.PrettyPrint import Telomare.Size.IR +import Telomare.Space.Static (StaticSpaceFailure, StaticSpaceStats) +import Telomare.SpaceBound (SpaceBound) debug :: Bool debug = False @@ -47,15 +48,6 @@ data SizingSettings = SizingSettings , doCap :: Bool } deriving (Eq, Ord, Show) -data InputRestrictions - = InputRestrictions {zeroes :: Set Integer, pairs :: Set Integer} - deriving Show - -instance Semigroup InputRestrictions where - (<>) (InputRestrictions za pa) (InputRestrictions zb pb) = InputRestrictions (za <> zb) (pa <> pb) -instance Monoid InputRestrictions where - mempty = InputRestrictions mempty mempty - extractInputRestrictions :: InputSizingExpr -> InputRestrictions extractInputRestrictions = cleanup . f Nothing where f expected = f' expected . project @@ -156,7 +148,8 @@ initialInput irs = f 0 where -- -- The failure carries no location — `UnsizedExpr` has none. Callers holding -- the `Term3` fill it in (see `Telomare.Eval.locateSizingFailure`). -sizeTermM :: SizingSettings -> UnsizedExpr -> Either SizingFailure (SizedRecursion, CompiledExpr) +sizeTermM :: SizingSettings -> UnsizedExpr + -> Either SizingFailure (SizedRecursion, InputRestrictions, CompiledExpr) sizeTermM sizingSettings x = tidyUp . transformNoDeferM evalStep $ mx where unlocated tok kind = SizingFailure { sizingFailureToken = tok @@ -183,7 +176,7 @@ sizeTermM sizingSettings x = tidyUp . transformNoDeferM evalStep $ mx where Just (OverfueledSR i) -> debugTrace "sizeTermM ran out of budget" Left . unlocated i . FuelExhausted . succ $ maxSizingSize sizingSettings _ -> let sized = setSizes sm cm - in debugTrace "sizeTermM found all sizes" pure . (,) sr . clean $ if doCap sizingSettings + in debugTrace "sizeTermM found all sizes" pure . (,,) sr inputRestrictions . clean $ if doCap sizingSettings then uncap sized else sized where uncap = \case @@ -248,12 +241,20 @@ evalStaticCheck shouldCap t = -- counts are the numbers the compiler already relies on to claim a program is -- total; reporting them asserts nothing new. data SizingReport = SizingReport - { sizingReportCounts :: SizedRecursion + { sizingReportCounts :: SizedRecursion -- ^Per recursion site, the iteration count inferred over every input. - , sizingReportLocs :: Map UnsizedRecursionToken LocTag + , sizingReportLocs :: Map UnsizedRecursionToken LocTag -- ^Where each site is in the source. - , sizingReportBudget :: Int + , sizingReportBudget :: Int -- ^The unrolling budget the search was allowed. + , sizingReportSpace :: Either String SpaceBound + -- ^A bound on the live-heap peak, in cells over input sizes, or why none + -- was found. Deliberately lazy: computing it walks the sized program, and + -- a plain run never asks. + , sizingReportSpaceStats :: Maybe (Either StaticSpaceFailure StaticSpaceStats) + -- ^What the walk did — transitions, allocations, widenings, dead worlds — + -- when it ran in this process. An artifact stores the bound alone, so a + -- report read back from one has none. Lazy, and sharing the bound's thunk. } -- |Every recursion site's source location, recovered from the `Term3` diff --git a/src/Telomare/Size/IR.hs b/src/Telomare/Size/IR.hs index 2a8a363..cdb814e 100644 --- a/src/Telomare/Size/IR.hs +++ b/src/Telomare/Size/IR.hs @@ -15,6 +15,7 @@ import Data.Functor.Classes (Eq1 (..), Show1 (liftShowsPrec)) import Data.Functor.Foldable import Data.Map (Map) import qualified Data.Map as Map +import Data.Set (Set) import Data.Validity (Validity (..), trivialValidation) import GHC.Generics (Generic) @@ -29,6 +30,19 @@ import Telomare.PrettyPrint.Indent (indentWithOneChild', indentWithTwoChildren') debug' :: Bool debug' = False +-- |What the refinements guarantee about the input, by path: the parts known +-- to be zero and the parts known to be pairs. Paths index the input the way +-- `IndexedInputF` does: the whole input is 0, and path n has its left part at +-- 2n+1 and its right part at 2n+2. +data InputRestrictions + = InputRestrictions {zeroes :: Set Integer, pairs :: Set Integer} + deriving Show + +instance Semigroup InputRestrictions where + (<>) (InputRestrictions za pa) (InputRestrictions zb pb) = InputRestrictions (za <> zb) (pa <> pb) +instance Monoid InputRestrictions where + mempty = InputRestrictions mempty mempty + debugTrace' :: String -> a -> a debugTrace' s x = if debug' then trace s x else x diff --git a/src/Telomare/Space/Static.hs b/src/Telomare/Space/Static.hs new file mode 100644 index 0000000..130ab3a --- /dev/null +++ b/src/Telomare/Space/Static.hs @@ -0,0 +1,670 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE LambdaCase #-} + +-- |The static space bound: `Telomare.Eval.Space`'s machine run at compile +-- time, over an abstract input. The program it runs is the /sized/ term, so +-- every recursion is a church tower the walk unrolls exactly its inferred +-- count of times; per-iteration growth and retained accumulators are then +-- measured on the abstract run by reachability, exactly as the concrete meter +-- measures them — not modelled by per-combinator rules, which is the dead end +-- the sibling project's @design/SPACE.md@ records. +-- +-- The abstract input mirrors the sizing pass's `Telomare.Size.initialInput`: +-- refinement-guaranteed pairs are expanded, refinement-guaranteed zeroes are +-- concrete, and everything else is a symbolic node `AInputN p` whose cell +-- bound is the input-size variable @|p|@ of `Telomare.SpaceBound`. A gate on +-- a symbolic value takes both branches and joins their values in a +-- superposition (`ASupN`), the same shape the sizing pass's @superStepM@ +-- uses; the peak simply sees both branches' allocations, which can only +-- overcount. +-- +-- What keeps that from exploding is the discipline the sizing pass carries +-- in its superposition tags: a fork is /about/ something — whether the input +-- part at path p is zero or a pair — and the superposition it joins into +-- remembers it. While a fork's branch runs, that commitment is in force (the +-- world), so a later test of the same part — the same `AInputN`, or a +-- superposition tagged with it — dispatches to the committed side instead of +-- forking again. Without this, k tests of one unknown cost 2^k worlds; with +-- it they cost two. A fork about a widened node — one that kept only its +-- bound — is tagged by that node's id for the same reason: it is one value, +-- however little is known of it. +-- +-- Where the concrete machine's every figure is a number, here it is a +-- `SpaceBound`. A node's bound is fixed at allocation: one cell for concrete +-- constructors, @|p|@ for a symbolic input, and for a superposition the +-- maximum of its sides' reachable subgraphs, frozen — the store is immutable, +-- so the sides never change. A sweep then sums the bounds of the distinct +-- reachable nodes without entering superpositions, crediting every input +-- part to the outermost reachable path above it (@|p|@ already counts all of +-- path p's subtree) and every projection of a widened node to the whole it +-- came from. Sharing that crosses a superposition boundary is counted on +-- both sides; documented looseness, not a soundness hole. +-- +-- Superpositions nest as unknown-driven choices pile up; shallow-equal sides +-- collapse (as the sizing pass's @mergeShallow@ does), and past a nesting +-- depth cap a superposition is widened to an opaque node that keeps only its +-- bound. An opaque value can still be projected (a part is no larger than the +-- whole) and gated on (both branches), but not applied or entered — that +-- reports `SpaceUnsupported` rather than guessing. +module Telomare.Space.Static where + +import Data.Functor.Foldable (cata, project) +import Data.IntMap.Strict (IntMap) +import qualified Data.IntMap.Strict as IntMap +import qualified Data.IntSet as IntSet +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set + +import Telomare.Eval.Meter (identityFunction) +import Telomare.IR.Base +import Telomare.IR.Core +import Telomare.Machine (appB, decendant, doLeft, doRight) +import Telomare.Size.IR (InputRestrictions (..)) +import Telomare.SpaceBound + +-- |Why no bound came out. Neither is a compile failure; the certificate +-- reports the bound as unknown and says why. +data StaticSpaceFailure + = SpaceFuelExhausted + | SpaceUnsupported String + deriving (Eq, Show) + +renderStaticSpaceFailure :: StaticSpaceFailure -> String +renderStaticSpaceFailure = \case + SpaceFuelExhausted -> "the abstract run did not finish in its fuel" + SpaceUnsupported why -> why + +-- |Machine transitions the abstract run is allowed. The run is finite anyway +-- (every recursion is a baked tower); the fuel guards against a pathological +-- superposition blowup taking the compiler with it. +defaultStaticSpaceFuel :: Int +defaultStaticSpaceFuel = 4194304 + +type NodeId = Int + +-- |What a fork is about. A fork on an input part splits on whether the part +-- at that path is zero or a pair; a fork on a widened node — one that kept +-- only its bound — splits that one value, which never changes, so its id is +-- the name. A world commits to one side per tag. +data Tag = TagPath !Integer | TagNode !NodeId + deriving (Eq, Ord, Show) + +-- |Which side of each split the current world has committed to: True for the +-- zero side, False for the pair side. +type World = Map Tag Bool + +-- |An abstract value. The concrete constructors mirror +-- `Telomare.Eval.Space.Node`; the rest is what "abstract" adds. +data ANode + = AZeroN + | APairN !NodeId !NodeId + | ADeferN !FunctionIndex CompiledExpr + | AGateN + | AAbortN + | AAbortedN + -- ^The payload's size is in the stored bound. + | AInputN !Integer + -- ^The input part at a path, unexamined: @|p|@ cells. + | ASupN !Int !(Maybe Tag) !NodeId !NodeId + -- ^Either side, from a fork: nesting depth, what the fork was about (when + -- it was about one thing), the zero-world side, the pair-world side. + | AOpaqueN !NodeId + -- ^A widened superposition: only its bound remains. Carries its family — + -- the id widening produced — because a part projected out of it is a view + -- of the same whole, and a sweep charges the whole once. + | ADeadN + -- ^An impossible world. A typechecked, sized program never gets stuck, so + -- a stuck configuration can only come from an over-approximated fork whose + -- two worlds were crossed; it costs nothing and vanishes from joins. + deriving (Eq, Show) + +-- |Sides of a superposition are alternatives, not parts: a sweep must not +-- walk into them, their cost is the frozen bound. +aChildren :: ANode -> [NodeId] +aChildren = \case + APairN a b -> [a, b] + _ -> [] + +-- |How deep superpositions may nest before widening. +supDepthCap :: Int +supDepthCap = 4 + +-- |What the machine still has to do with the value it is returning. The +-- first seven mirror `Telomare.Eval.Space.Frame`; the last three are how an +-- unknown forks. Forking frames carry the world to come back to, since the +-- branch in front of them runs under a commitment. +data AFrame + = FPairRight CompiledExpr + | FPairLeft !NodeId + | FGate CompiledExpr CompiledExpr + | FLeft + | FRight + | FSetEnv + | FRestoreEnv !(Maybe NodeId) + | FBothRight !(Maybe Tag) !World CompiledExpr + -- ^A gate could not choose: its zero branch's value is coming back, + -- evaluate the pair branch next, under the other commitment. + | FJoinSup !(Maybe Tag) !World !NodeId + -- ^The zero-world value, held while the pair world finishes; restore the + -- world and join into a superposition. + | FOpFork !PendOp !(Maybe Tag) !World !NodeId + -- ^An operation over a superposed operand: the zero side's result is + -- coming back, run the same operation on the held pair side. + +-- |The operation `FOpFork` repeats on the second side. +data PendOp + = OpGate CompiledExpr CompiledExpr + | OpApply !NodeId + -- ^Apply the side, as a function, to this argument. + | OpArgOf !NodeId + -- ^Apply this function to the side. + | OpSetEnv + | OpProj !Bool + -- ^True for the left part. + +aFrameRoots :: AFrame -> [NodeId] +aFrameRoots = \case + FPairLeft a -> [a] + FRestoreEnv (Just e) -> [e] + FJoinSup _ _ a -> [a] + FOpFork op _ _ a -> a : opRoots op + _ -> [] + where + opRoots = \case + OpApply e -> [e] + OpArgOf f -> [f] + _ -> [] + +data AState = AState + { aStore :: !(IntMap (ANode, SpaceBound, Bool)) + -- ^Per node: its shape, its frozen cell bound, and whether a function + -- (defer, gate or abort) is anywhere inside it — what decides if a + -- superposition over it may ever be widened. + , aNext :: !NodeId + , aEnv :: !(Maybe NodeId) + , aFrames :: ![AFrame] + , aWorld :: !World + , aPeak :: !SpaceBound + , aFuel :: !Int + , aLastLive :: !SpaceBound + -- ^The live bound at the last sweep. + , aLiveCount :: !Int + -- ^How many nodes that live set had; what the sweep cadence is scaled by. + , aDebt :: !SpaceBound + -- ^Bounds of the nodes allocated since the last sweep — fresh content + -- only: a join-produced node, whose frozen bound subsumes structure that + -- is already alive, sweeps on the spot instead of entering the debt. The + -- store grows by at most the debt between sweeps, so last live plus debt + -- bounds any intermediate live set — that is what keeps the amortized + -- cadence sound. + , aDebtCount :: !Int + , aLastPrune :: !Int + -- ^`aNext` at the last store prune; pruning is rare so the join memo + -- keeps earning its keep between prunes. + , aPins :: ![NodeId] + -- ^Ids held in machine internals mid-transition (a join's first half, a + -- two-part allocation) that no frame roots yet; sweeps must keep them. + , aJoinMemo :: !(Map (Maybe Tag, NodeId, NodeId) NodeId) + -- ^Joins already made: the store is immutable, so the same two sides + -- under the same tag always join to the same node. Loops re-joining the + -- same alternatives hit this instead of re-walking their subgraphs. + , aWidened :: !Int + -- ^Superpositions widened to their bound alone. + , aDead :: !Int + -- ^Impossible worlds closed. A typechecked, sized program never gets + -- stuck, so on a sound walk this stays zero; a nonzero count means the + -- bound rests on worlds the analysis could not follow. + } + +-- |Bound the peak live heap of the sized program applied to the abstract +-- input, or say why that could not be done. +evalSpaceStatic :: Int -> InputRestrictions -> CompiledExpr + -> Either StaticSpaceFailure SpaceBound +evalSpaceStatic fuel irs prog = ssBound <$> evalSpaceStatic' fuel irs prog + +-- |What the abstract run did, for calibration against the concrete meter and +-- for tests: the bound, the transitions it took, the nodes it allocated, the +-- superpositions it widened, and the impossible worlds it closed. +data StaticSpaceStats = StaticSpaceStats + { ssBound :: SpaceBound + , ssTransitions :: !Int + , ssAllocations :: !Int + , ssWidenings :: !Int + , ssDeadWorlds :: !Int + } + deriving (Eq, Show) + +-- |`evalSpaceStatic` with the run's statistics. +evalSpaceStatic' :: Int -> InputRestrictions -> CompiledExpr + -> Either StaticSpaceFailure StaticSpaceStats +evalSpaceStatic' fuel irs prog = + let (inputId, st0) = buildInput irs + -- Measured before the first transition: the amortized upper bound is + -- "what was live at the last sweep plus what was allocated since", and + -- the input graph was never allocated, so it has to be in that first + -- live figure or every early upper bound would omit it. + st1 = sweep [] (st0 { aEnv = Just inputId }) + settle (st, root) = + let final = sweep [root] st + in StaticSpaceStats + { ssBound = aPeak final + , ssTransitions = fuel - aFuel final + , ssAllocations = aNext final + , ssWidenings = aWidened final + , ssDeadWorlds = aDead final + } + in settle <$> evalC st1 (appB prog EnvB) + where + look st i = let (n, _, _) = aStore st IntMap.! i in n + boundOf st i = let (_, b, _) = aStore st IntMap.! i in b + hasFun st i = let (_, _, h) = aStore st IntMap.! i in h + + -- The input graph, before the run: sweeps reach it through the + -- environment root for as long as the program can still use it. + buildInput irs' = + let go n st + | Set.member n (zeroes irs') = ins AZeroN (sbConst 1) st + | any (`decendant` n) (pairs irs') = + let (l, st1) = go (n * 2 + 1) st + (r, st2) = go (n * 2 + 2) st1 + in ins (APairN l r) (sbConst 1) st2 + | otherwise = ins (AInputN n) (sbInput n) st + ins node b st = + (aNext st, st { aStore = IntMap.insert (aNext st) (node, b, False) (aStore st) + , aNext = aNext st + 1 }) + in go 0 (AState IntMap.empty 0 Nothing [] Map.empty mempty fuel (sbConst 0) 0 (sbConst 0) 0 0 [] Map.empty 0 0) + + -- What the current world already knows about a tag: committed zero, + -- committed pair, or nothing. Input paths carry structure: a zero has + -- only zeroes under it, so an ancestor's zero commitment covers a part, + -- and a part committed to be a pair makes every ancestor a pair. + worldSide st about = case Map.lookup about (aWorld st) of + Just s -> Just s + Nothing -> case about of + TagPath p + | any (\a -> Map.lookup (TagPath a) (aWorld st) == Just True) (ancestors p) -> Just True + | any (\(t, s) -> not s && below t p) (Map.toList (aWorld st)) -> Just False + | otherwise -> Nothing + TagNode _ -> Nothing + where + below (TagPath t) p = t /= p && t `decendant` p + below (TagNode _) _ = False + + -- The paths above a path, nearest first; the whole input is path 0. + ancestors :: Integer -> [Integer] + ancestors 0 = [] + ancestors p = let a = (p - 1) `div` 2 in a : ancestors a + + commitW t s st = case t of + Just p -> st { aWorld = Map.insert p s (aWorld st) } + Nothing -> st + + -- The reachable bound from some roots: distinct nodes, superpositions + -- contributing their frozen bound and not their sides. Concrete cells + -- are counted in one Int; only symbolic nodes pay bound arithmetic. + -- + -- Two kinds of node are views of something rather than cells of their + -- own. An input part is the subtree of the input at its path, so + -- @|p| = 1 + |2p+1| + |2p+2|@: a part whose ancestor is also reachable + -- is already counted, and one path is one part however many nodes were + -- allocated to view it — what remains are disjoint subtrees, exactly the + -- distinct cells the concrete input shares among those views. A widened + -- node's projections are parts of one whole, and the whole's bound + -- covers them together, so a family is charged once. + reachBound st = fst . reachBoundCounted st + + reachBoundCounted st = go IntSet.empty (0 :: Int) Set.empty IntMap.empty [] where + go visited !plain parts families specials = \case + [] -> + let outermost = [ p | p <- Set.toList parts + , not (any (`Set.member` parts) (ancestors p)) ] + symbolic = fmap sbInput outermost <> IntMap.elems families <> specials + in ( foldr sbAdd (sbConst (fromIntegral plain)) symbolic + , IntSet.size visited ) + (i : rest) + | IntSet.member i visited -> go visited plain parts families specials rest + | otherwise -> + let (node, b, _) = aStore st IntMap.! i + visited' = IntSet.insert i visited + next = aChildren node <> rest + in case node of + AZeroN -> go visited' (plain + 1) parts families specials next + APairN _ _ -> go visited' (plain + 1) parts families specials next + ADeferN _ _ -> go visited' (plain + 1) parts families specials next + AGateN -> go visited' (plain + 1) parts families specials next + AAbortN -> go visited' (plain + 1) parts families specials next + AInputN p -> go visited' plain (Set.insert p parts) families specials next + AOpaqueN fam -> go visited' plain parts (IntMap.insert fam b families) specials next + _ -> go visited' plain parts families (b : specials) next + + sweep extra st = + let roots = extra <> aPins st <> foldMap pure (aEnv st) + <> concatMap aFrameRoots (aFrames st) + (live0, liveCount) = reachBoundCounted st roots + -- Forced here and now — bounds are strict all the way down, see + -- `Telomare.SpaceBound` — so the walk's memory tracks its live set + -- rather than every allocation it ever made. + !live = live0 + -- What the store could have held at its worst since the last look. + !upper = sbAdd (aLastLive st) (aDebt st) + !peak = sbMax (sbMax (aPeak st) upper) live + st' = st { aPeak = peak + , aLastLive = live + , aLiveCount = liveCount + , aDebt = sbConst 0 + , aDebtCount = 0 + } + in if aNext st' - aLastPrune st' > 500000 + then pruneStore roots st' + else st' + + -- Now and then, drop what nothing can reach and the memo entries that + -- pointed into it; without this the store and memo grow without bound + -- and garbage-collection pressure grinds a long walk down. Rare, so the + -- memo keeps earning between prunes. The measuring walk stops at + -- superpositions, but a live superposition's sides can still be read, + -- so the keep-walk goes through them. + pruneStore roots st = + let keep = markAll st IntSet.empty roots + keepK i = IntSet.member i keep + in st { aStore = IntMap.restrictKeys (aStore st) keep + , aJoinMemo = Map.filterWithKey + (\(_, a, b) i -> keepK a && keepK b && keepK i) + (aJoinMemo st) + , aLastPrune = aNext st + } + + markAll st visited = \case + [] -> visited + (i : rest) + | IntSet.member i visited -> markAll st visited rest + | otherwise -> + let (node, _, _) = aStore st IntMap.! i + kids = case node of + APairN a b -> [a, b] + ASupN _ _ a b -> [a, b] + _ -> [] + in markAll st (IntSet.insert i visited) (kids <> rest) + + alloc node b0 st = + let i = aNext st + -- Stored bounds are folded at every sweep; keeping each one a + -- single affine (the pointwise maximum of its alternatives) makes + -- that fold one cheap merge per node instead of a cross product. + !b = sbWiden 1 b0 + -- A join-produced node's frozen bound subsumes structure that is + -- mostly already alive; letting it into the debt would double + -- count wildly, so those measure on the spot. A concrete cell or + -- a symbolic input part is genuinely fresh content. + subsuming = case node of + ASupN {} -> True + AOpaqueN {} -> True + AAbortedN -> True + _ -> False + !funInside = case node of + ADeferN _ _ -> True + AGateN -> True + AAbortN -> True + APairN x y -> hasFun st x || hasFun st y + ASupN _ _ x y -> hasFun st x || hasFun st y + _ -> False + !debt = if subsuming then aDebt st else sbAdd (aDebt st) b + st1 = st { aStore = IntMap.insert i (node, b, funInside) (aStore st) + , aNext = i + 1 + , aDebt = debt + , aDebtCount = aDebtCount st + 1 + } + due = subsuming + || aDebtCount st1 > max 256 (aLiveCount st1 `div` 2) + in (i, if due then sweep [i] st1 else st1) + + allocRet st node b = let (i, st') = alloc node b st in retC st' i + + -- Allocate while some loose ids must survive the sweep. + allocPinned pins node b st = + let (i, st') = alloc node b (st { aPins = pins <> aPins st }) + in (i, st' { aPins = drop (length pins) (aPins st') }) + + -- Run a step while some loose ids must survive its sweeps. + pinned pins act st = do + (st1, r) <- act (st { aPins = pins <> aPins st }) + pure (st1 { aPins = drop (length pins) (aPins st1) }, r) + + spend st + | aFuel st <= 0 = Left SpaceFuelExhausted + | otherwise = pure st { aFuel = aFuel st - 1 } + + unsupported why = Left (SpaceUnsupported ("space bound: " <> why)) + + push f st = st { aFrames = f : aFrames st } + + pop st = st { aFrames = drop 1 (aFrames st) } + + aDefer x = case project x of + StuckFW (DeferSF fi body) -> ADeferN fi body + _ -> error "Telomare.Space.Static: expected a function" + + -- As in the concrete machine, the gate-switch shape comes first: taken + -- apart generically it would evaluate both branches even on a known + -- scrutinee. + evalC st0' whole = spend st0' >>= \st -> case project whole of + GateSwitch l r s -> evalC (push (FGate l r) st) s + BasicFW ZeroSF -> allocRet st AZeroN (sbConst 1) + BasicFW (PairSF a b) -> evalC (push (FPairRight b) st) a + StuckFW (DeferSF fi body) -> allocRet st (ADeferN fi body) (sbConst 1) + StuckFW GateSF -> allocRet st AGateN (sbConst 1) + StuckFW (LeftSF x) -> evalC (push FLeft st) x + StuckFW (RightSF x) -> evalC (push FRight st) x + StuckFW (SetEnvSF x) -> evalC (push FSetEnv st) x + StuckFW EnvSF -> case aEnv st of + Just i -> retC st i + Nothing -> unsupported "unapplied environment reference" + AbortFW AbortF -> allocRet st AAbortN (sbConst 1) + AbortFW (AbortedF e) -> + allocRet st AAbortedN (sbConst (1 + basicCells e)) + _ -> unsupported "unexpected expression" + + basicCells = cata $ \case + ZeroSF -> 1 + PairSF a b -> 1 + a + b + + retC st0' v = spend st0' >>= \st -> case aFrames st of + [] -> pure (st, v) + FPairRight b : k + | isDead st v -> retC (st { aFrames = k }) v + | otherwise -> evalC (st { aFrames = FPairLeft v : k }) b + FPairLeft a : k + | isDead st v -> retC (st { aFrames = k }) v + | otherwise -> allocRet (st { aFrames = k }) (APairN a v) (sbConst 1) + FGate l r : _ -> gateD (pop st) l r v + FLeft : _ -> projD (pop st) True v + FRight : _ -> projD (pop st) False v + FSetEnv : _ -> setEnvD (pop st) v + FRestoreEnv saved : k -> + retC (st { aEnv = saved, aFrames = k }) v + FBothRight t w r : k -> + evalC (commitW t False (st { aFrames = FJoinSup t w v : k, aWorld = w })) r + FJoinSup t w a : k -> + joinSup (st { aFrames = k, aWorld = w }) t a v >>= uncurry retC + FOpFork op t w b : k -> + let st1 = commitW t False + (st { aFrames = FJoinSup t w v : k, aWorld = w }) + in case op of + OpGate l r -> gateD st1 l r b + OpApply e -> applyD st1 b e + OpArgOf f -> applyD st1 f b + OpSetEnv -> setEnvD st1 b + OpProj tl -> projD st1 tl b + + -- Run an operation over a superposition's sides — or, when the world + -- has already committed on what the superposition is about, over just + -- the committed side. Dispatch-not-fork is what keeps repeated tests of + -- one unknown from multiplying worlds. + onSup st t a b op perform = case t >>= worldSide st of + Just True -> perform st a + Just False -> perform st b + Nothing -> + perform (commitW t True (push (FOpFork op t (aWorld st) b) st)) a + + -- A gate with its scrutinee: choose, or take both and superpose. A + -- non-data scrutinee cannot happen in a typechecked program, so it marks + -- an impossible fork world. + gateD st l r v = case look st v of + AZeroN -> evalC st l + APairN _ _ -> evalC st r + AAbortedN -> retC st v + ADeadN -> retC st v + AInputN p -> gateOn (TagPath p) + AOpaqueN _ -> gateOn (TagNode v) + ASupN _ t a b -> onSup st t a b (OpGate l r) (\st' side -> gateD st' l r side) + _ -> dead st + where + gateOn t = case worldSide st t of + Just True -> evalC st l + Just False -> evalC st r + Nothing -> forkGate (Just t) + forkGate t = + evalC (commitW t True (push (FBothRight t (aWorld st) r) st)) l + + -- A projection. In a world where the part is committed zero, the part's + -- parts are zero too. + projD st takeLeft v = case look st v of + APairN a b -> retC st (if takeLeft then a else b) + AZeroN -> retC st v + AAbortedN -> retC st v + AInputN p + | worldSide st (TagPath p) == Just True -> allocRet st AZeroN (sbConst 1) + | otherwise -> + let c = if takeLeft then p * 2 + 1 else p * 2 + 2 + in if Set.member c (zeroes irs) + then allocRet st AZeroN (sbConst 1) + else allocRet st (AInputN c) (sbInput c) + ADeadN -> retC st v + AOpaqueN fam -> allocRet st (AOpaqueN fam) (boundOf st v) + ASupN _ t a b -> onSup st t a b (OpProj takeLeft) (`projD` takeLeft) + _ -> dead st + + setEnvD st v = case look st v of + AAbortedN -> retC st v + ADeadN -> retC st v + APairN f e -> applyD st f e + ASupN _ t a b -> onSup st t a b OpSetEnv setEnvD + -- A widened pair has lost its function; that is a real limitation, + -- not an impossible world. + AOpaqueN _ -> unsupported "SetEnv of a widened value" + _ -> dead st + + applyD st f e = case (look st f, look st e) of + (ADeadN, _) -> retC st f + (_, ADeadN) -> retC st e + (AAbortedN, _) -> retC st f + (_, AAbortedN) -> retC st e + (AAbortN, AZeroN) -> allocRet st (aDefer identityFunction) (sbConst 1) + (AAbortN, APairN _ _) -> + allocRet st AAbortedN (sbAdd (sbConst 1) (reachBound st [e])) + -- The assert fires exactly when the part is a pair, so the fork is + -- about the part and carries its tag. + (AAbortN, AInputN p) -> assertOn (TagPath p) + (AAbortN, ASupN _ t a b) -> onSup st t a b (OpArgOf f) (applyTo f) + -- Anything else an assert can see is a widened value: one value, + -- tested here, so the fork is about that node. + (AAbortN, _) -> assertOn (TagNode e) + (AGateN, AZeroN) -> allocRet st (aDefer doLeft) (sbConst 1) + (AGateN, APairN _ _) -> allocRet st (aDefer doRight) (sbConst 1) + -- A gate selector splits on the same zero-or-pair question. + (AGateN, AInputN p) -> selectOn (TagPath p) + (AGateN, ASupN _ t a b) -> onSup st t a b (OpArgOf f) (applyTo f) + (AGateN, _) -> selectOn (TagNode e) + (ADeferN _ body, _) -> + evalC ((push (FRestoreEnv (aEnv st)) st) { aEnv = Just e }) body + (ASupN _ t a b, _) -> onSup st t a b (OpApply e) (\st' side -> applyD st' side e) + -- A widened value may well have held a function; refusing is honest, + -- inventing a body is not. + (AOpaqueN _, _) -> unsupported "application of a widened value" + _ -> dead st + where + applyTo g st' = applyD st' g + + -- `assert` on an unknown: the identity in the zero world, the + -- retained message in the pair world — unless the world already + -- knows which. + assertOn t = case worldSide st t of + Just True -> allocRet st (aDefer identityFunction) (sbConst 1) + Just False -> allocRet st AAbortedN (sbAdd (sbConst 1) (reachBound st [e])) + Nothing -> do + let (i1, st1) = allocPinned [e] (aDefer identityFunction) (sbConst 1) st + (i2, st2) = allocPinned [i1] AAbortedN (sbAdd (sbConst 1) (reachBound st1 [e])) st1 + joinSup st2 (Just t) i1 i2 >>= uncurry retC + + -- A gate selector on an unknown: left in the zero world, right in + -- the pair world. + selectOn t = case worldSide st t of + Just True -> allocRet st (aDefer doLeft) (sbConst 1) + Just False -> allocRet st (aDefer doRight) (sbConst 1) + Nothing -> do + let (i1, st1) = alloc (aDefer doLeft) (sbConst 1) st + (i2, st2) = allocPinned [i1] (aDefer doRight) (sbConst 1) st1 + joinSup st2 (Just t) i1 i2 >>= uncurry retC + + isDead st i = case look st i of + ADeadN -> True + _ -> False + + dead st = allocRet (st { aDead = aDead st + 1 }) ADeadN (sbConst 0) + + -- Join two alternatives: same id or same shallow shape collapse, a dead + -- world vanishes, two pairs join pointwise, past the depth cap only the + -- bound survives. A join spends fuel like any transition: the pointwise + -- merge recurses through a pair's whole shape. + joinSup st0 t a b = spend st0 >>= \st -> joinSup' st t a b + + joinSup' st t a b + | a == b = pure (st, a) + | isDead st a = pure (st, b) + | isDead st b = pure (st, a) + | shallowEqA (look st a) (look st b) = pure (st, a) + -- A remembered join may have been pruned since; verify before using. + | Just i <- Map.lookup (t, a, b) (aJoinMemo st) + , IntMap.member i (aStore st) = + pure (st, i) + -- The pointwise merge: a superposition of two pairs is a pair of + -- superpositions. Sound for a bound, since a maximum of sums is never + -- above the sum of maxima, and structurally decisive: a superposition + -- of closures (code, env) collapses to one closure over superposed + -- environments, function positions meet and cancel, and nesting depth + -- resets at every pair. Under the same tag the selection stays + -- consistent, so no precision is lost to world-crossing where it + -- matters. + | APairN a1 b1 <- look st a, APairN a2 b2 <- look st b = do + (st1, l) <- pinned [a, b] (\s -> joinSup s t a1 a2) st + (st2, r) <- pinned [a, b, l] (\s -> joinSup s t b1 b2) st1 + let (i, st3) = allocPinned [l] (APairN l r) (sbConst 1) st2 + pure (remember st3 i, i) + | otherwise = + let depth = 1 + max (depthOf (look st a)) (depthOf (look st b)) + joined = sbMax (reachBound st [a]) (reachBound st [b]) + -- Widening keeps only the bound, and a bound cannot be + -- applied; data can afford that, functions cannot. + widen = depth > supDepthCap + && not (hasFun st a) && not (hasFun st b) + in if widen + then let (i, st') = alloc (AOpaqueN (aNext st)) joined (st { aWidened = aWidened st + 1 }) + in pure (remember st' i, i) + else let (i, st') = alloc (ASupN depth t a b) joined st in pure (remember st' i, i) + where + remember st' i = st' { aJoinMemo = Map.insert (t, a, b) i (aJoinMemo st') } + + depthOf = \case + ASupN d _ _ _ -> d + _ -> 0 + + shallowEqA a b = case (a, b) of + (AZeroN, AZeroN) -> True + (APairN x y, APairN x' y') -> x == x' && y == y' + (ADeferN i _, ADeferN j _) -> i == j + (AGateN, AGateN) -> True + (AAbortN, AAbortN) -> True + (AInputN n, AInputN m) -> n == m + (AOpaqueN f, AOpaqueN g) -> f == g + _ -> False diff --git a/src/Telomare/SpaceBound.hs b/src/Telomare/SpaceBound.hs new file mode 100644 index 0000000..4f674e9 --- /dev/null +++ b/src/Telomare/SpaceBound.hs @@ -0,0 +1,193 @@ +{-# LANGUAGE LambdaCase #-} + +-- |The language a static space bound is stated in: a maximum over affine +-- expressions in input sizes, measured in cells (see `Telomare.Eval.Space` +-- for the cell). @3·|input.left| + 12@ is one affine; a program whose peak +-- depends on which branch runs gets the maximum of several. +-- +-- The variables are input /paths/, indexed the way the sizing pass indexes +-- its symbolic input (`Telomare.Size.IR.IndexedInputF`): the whole input is +-- path 0, and a node at path n has its left part at 2n+1 and its right part +-- at 2n+2. @|p|@ stands for the size in cells of the input part at path p. +-- +-- Everything here is an upper bound, so the operations are free to lose +-- precision but never to lose soundness: pruning only drops affines another +-- affine dominates pointwise, and widening replaces a set of affines with +-- their pointwise maximum, which bounds each of them. The one non-value is +-- `sbTop`, the bound that says nothing. Nothing in the static pass produces +-- it today — that pass reports what it could not do as a failure instead — +-- but every operation here absorbs it, so a producer may use it. Input +-- dependence never collapses to it: it stays symbolic. +-- +-- Bounds are accumulated over millions of machine transitions, so they are +-- built strict all the way down: strict fields, a strict map, and `norm` +-- forces every affine before wrapping them. Left lazy, each accumulation is a +-- thunk retaining the state it was made from, and a walk's memory grows with +-- its history instead of its live set. +module Telomare.SpaceBound where + +import Data.List (intercalate, sort) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import qualified Data.Set as Set +import Numeric.Natural (Natural) + +-- |One affine expression: Σ coeff_p · |p| + constant. +data Affine = Affine + { affCoeffs :: !(Map Integer Natural) + -- ^Per-path coefficients; a path absent here has coefficient zero, and no + -- path is stored with one — `norm` drops them. + , affConst :: !Natural + } + deriving (Eq, Ord, Show) + +-- |A bound: the maximum of some affines, or `sbTop` when nothing is known. +-- The list is kept free of dominated entries and never empty. +newtype SpaceBound = SpaceBound (Maybe [Affine]) + deriving (Eq, Show) + +-- |A known figure. +sbConst :: Natural -> SpaceBound +sbConst k = SpaceBound (Just [Affine Map.empty k]) + +-- |The size of the input part at a path. +sbInput :: Integer -> SpaceBound +sbInput p = SpaceBound (Just [Affine (Map.singleton p 1) 0]) + +-- |The bound that says nothing. +sbTop :: SpaceBound +sbTop = SpaceBound Nothing + +-- |Whether the second affine is everywhere at least the first. +dominates :: Affine -> Affine -> Bool +dominates (Affine cs k) (Affine cs' k') = + k <= k' && Map.isSubmapOfBy (<=) cs cs' + +-- |Drop every affine another one dominates. Ties keep one copy. +prune :: [Affine] -> [Affine] +prune xs = go xs [] where + go [] kept = reverse kept + go (a : rest) kept + | any (dominates a) rest || any (dominates a) kept = go rest kept + | otherwise = go rest (a : kept) + +-- |How many affines a bound may hold before it is widened. Past this, the +-- pointwise maximum stands in for all of them — looser, still sound. +defaultWidth :: Int +defaultWidth = 16 + +-- |Collapse to the pointwise maximum once the affine set outgrows the cap. +sbWiden :: Int -> SpaceBound -> SpaceBound +sbWiden _ (SpaceBound Nothing) = sbTop +sbWiden cap b@(SpaceBound (Just affs)) + | length affs <= cap = b + | otherwise = SpaceBound (Just [foldr1 pointwiseMax affs]) + where + pointwiseMax (Affine cs k) (Affine cs' k') = + Affine (Map.unionWith max cs cs') (max k k') + +-- |Canonical form: zero coefficients dropped, dominated affines pruned, the +-- rest sorted so that equal bounds compare equal however they were put +-- together, and everything forced (see the module header). An empty list has +-- no maximum; it reads as the bound that holds nothing. +norm :: [Affine] -> SpaceBound +norm [] = sbConst 0 +norm xs = + let affs = sort (prune (fmap tidy xs)) + tidy (Affine cs k) = Affine (Map.filter (/= 0) cs) k + in foldr seq () affs `seq` sbWiden defaultWidth (SpaceBound (Just affs)) + +-- |Both at once: cells held by co-live values sum. +sbAdd :: SpaceBound -> SpaceBound -> SpaceBound +sbAdd (SpaceBound (Just as)) (SpaceBound (Just bs)) = + norm [ Affine (Map.unionWith (+) cs cs') (k + k') + | Affine cs k <- as, Affine cs' k' <- bs ] +sbAdd _ _ = sbTop + +-- |Either alone: peaks of alternative runs take the worse one. +sbMax :: SpaceBound -> SpaceBound -> SpaceBound +sbMax (SpaceBound (Just as)) (SpaceBound (Just bs)) = norm (as <> bs) +sbMax _ _ = sbTop + +-- |A bound taken a concrete number of times over. +sbScale :: Natural -> SpaceBound -> SpaceBound +sbScale _ (SpaceBound Nothing) = sbTop +sbScale n (SpaceBound (Just affs)) = + norm [ Affine (fmap (n *) cs) (n * k) | Affine cs k <- affs ] + +-- |Cells held together sum; the empty sum holds nothing. +instance Semigroup SpaceBound where + (<>) = sbAdd + +instance Monoid SpaceBound where + mempty = sbConst 0 + +-- |Replace the paths whose sizes are known — refinement-pinned inputs, or a +-- test harness's actual input — by those sizes. +sbSubstitute :: Map Integer Natural -> SpaceBound -> SpaceBound +sbSubstitute _ (SpaceBound Nothing) = sbTop +sbSubstitute sizes (SpaceBound (Just affs)) = norm (fmap subst affs) where + subst (Affine cs k) = + let (known, unknown) = Map.partitionWithKey (\p _ -> Map.member p sizes) cs + pinned = sum [ c * (sizes Map.! p) | (p, c) <- Map.toList known ] + in Affine unknown (k + pinned) + +-- |The figure, when no input size remains in it. +sbConcrete :: SpaceBound -> Maybe Natural +sbConcrete (SpaceBound Nothing) = Nothing +sbConcrete (SpaceBound (Just affs)) + | all (Map.null . affCoeffs) affs = Just (maximum (fmap affConst affs)) + | otherwise = Nothing + +-- |Whether the bound, at the given input sizes, stands at or above a +-- measured figure. `sbTop` bounds everything; a bound still symbolic after +-- substitution verifies nothing. +sbAtLeast :: Natural -> Map Integer Natural -> SpaceBound -> Bool +sbAtLeast measured sizes bound = case sbSubstitute sizes bound of + SpaceBound Nothing -> True + b -> maybe False (>= measured) (sbConcrete b) + +-- |Every input path the bound mentions; what a harness must size to check it. +sbPaths :: SpaceBound -> [Integer] +sbPaths (SpaceBound Nothing) = [] +sbPaths (SpaceBound (Just affs)) = Set.toList (foldMap (Map.keysSet . affCoeffs) affs) + +-- |A path as the words a reader would use: @input@, @input.left.right@, … +renderPath :: Integer -> String +renderPath = intercalate "." . ("input" :) . go [] where + go acc 0 = acc + go acc p + | odd p = go ("left" : acc) ((p - 1) `div` 2) + | otherwise = go ("right" : acc) ((p - 2) `div` 2) + +renderAffine :: Affine -> String +renderAffine (Affine cs k) = case terms of + [] -> show k + _ -> intercalate " + " (terms <> [show k | k /= 0]) + where + terms = [ coeff c <> "|" <> renderPath p <> "|" | (p, c) <- Map.toAscList cs ] + coeff 1 = "" + coeff c = show c <> "·" + +-- |What to print for a bound. +renderSpaceBound :: SpaceBound -> String +renderSpaceBound = \case + SpaceBound Nothing -> "unknown" + SpaceBound (Just [a]) -> renderAffine a <> " cells" + SpaceBound (Just affs) -> + "max(" <> intercalate ", " (fmap renderAffine affs) <> ") cells" + +-- |`renderSpaceBound` for a report line: an affine over many input parts is +-- summarized rather than spelled out, deepest path and all. +renderSpaceBoundBrief :: SpaceBound -> String +renderSpaceBoundBrief = \case + SpaceBound Nothing -> "unknown" + SpaceBound (Just [a]) -> brief a <> " cells" + SpaceBound (Just affs) -> + "max(" <> intercalate ", " (fmap brief affs) <> ") cells" + where + brief a@(Affine cs k) + | Map.size cs <= 4 = renderAffine a + | otherwise = + "sizes of " <> show (Map.size cs) <> " input parts (" + <> show (sum (Map.elems cs)) <> " weighted) + " <> show k diff --git a/telomare.cabal b/telomare.cabal index 412aeb3..66be9c3 100644 --- a/telomare.cabal +++ b/telomare.cabal @@ -45,6 +45,8 @@ library , Telomare.PrettyPrint.Indent , Telomare.Resolve , Telomare.Size + , Telomare.SpaceBound + , Telomare.Space.Static , Telomare.Size.IR , Telomare.TypeCheck , Telomare.Util @@ -188,7 +190,8 @@ test-suite telomare-sizing-test , RunModeTests , SizingTests , SpaceTests - build-depends: base + build-depends: QuickCheck + , base , bytestring , containers , hspec diff --git a/test/RunModeTests.hs b/test/RunModeTests.hs index 2a8868d..af7a7c5 100644 --- a/test/RunModeTests.hs +++ b/test/RunModeTests.hs @@ -24,6 +24,7 @@ import Telomare.Levels (LevelsInfo (..), levelsInfo) import Telomare.Machine (appB) import Telomare.Size (SizingReport (..)) import Telomare.Size.IR (SizedRecursion (..)) +import Telomare.SpaceBound (sbAdd, sbConst, sbInput, sbScale) runModeSpec :: Spec runModeSpec = do @@ -54,6 +55,19 @@ runModeSpec = do `shouldBe` unSizedRecursion (sizingReportCounts report) sizingReportLocs (artifactReport back) `shouldBe` sizingReportLocs report sizingReportBudget (artifactReport back) `shouldBe` sizingReportBudget report + -- The space bound too: reporting it from an artifact must not + -- need the abstract walk again. + sizingReportSpace (artifactReport back) `shouldBe` sizingReportSpace report + + it "carries a space bound whose numbers exceed a machine word" $ do + -- Paths grow as 2^depth and a unary character is a hundred deep, so + -- the encoding must not go through an Int. + let deep = sbAdd (sbScale (2 ^ (70 :: Int)) (sbInput (2 ^ (100 :: Int)))) (sbConst 12) + report = SizingReport (SizedRecursion Map.empty) Map.empty 0 (Right deep) Nothing + artifact = Artifact "deep" "hash" report "" ZeroB + case decodeArtifact (encodeArtifact artifact) of + Left err -> expectationFailure $ "failed to decode:\n" <> err + Right back -> sizingReportSpace (artifactReport back) `shouldBe` Right deep it "evaluates to what the program it came from evaluates to" $ do modules <- loadWith "tc_ultra_minimal.tel" "tc_ultra_minimal" diff --git a/test/SizingTest.hs b/test/SizingTest.hs index fd5eb35..a55fa11 100644 --- a/test/SizingTest.hs +++ b/test/SizingTest.hs @@ -13,3 +13,7 @@ main = hspec $ do conformanceSpec spaceSpec sessionParitySpec + boundSpec + boundLawSpec + staticFixtureSpec + staticVsMeasuredSpec diff --git a/test/SpaceTests.hs b/test/SpaceTests.hs index df56ffb..f7e0d24 100644 --- a/test/SpaceTests.hs +++ b/test/SpaceTests.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE LambdaCase #-} + -- |Hand-computed live-heap peaks, on terms small enough to trace against the -- machine by hand. Each figure here was derived on paper from the sweep -- discipline in `Telomare.Eval.Space` before it was asserted; a change that @@ -5,9 +7,16 @@ -- scrutiny as a changed step count. module SpaceTests where +import Control.Monad (forM_, unless) import Data.Char (ord) -import Data.Functor.Foldable (project) +import Data.Functor.Foldable (cata, project) +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Maybe (fromMaybe) +import Numeric.Natural (Natural) import Test.Hspec +import Test.Hspec.QuickCheck (prop) +import Test.QuickCheck import ConformanceTests (corpus) import SizingTests (loadWith) @@ -18,6 +27,10 @@ import Telomare.Eval.Space (SpaceMeter (..), SweepPolicy (..), evalSpace) import Telomare.IR.Base import Telomare.IR.Core (CompiledExpr) import Telomare.Machine (appB, deferB) +import Telomare.Size (SizingReport (..)) +import Telomare.Space.Static (StaticSpaceFailure (..), StaticSpaceStats (..), + defaultStaticSpaceFuel, evalSpaceStatic') +import Telomare.SpaceBound measure :: SweepPolicy -> CompiledExpr -> SpaceMeter measure policy = fst . evalSpace policy @@ -68,10 +81,138 @@ spaceSpec = describe "the live-heap peak" $ do spPeakLower adaptive `shouldSatisfy` (<= spPeakLower exact) spPeakUpper adaptive `shouldSatisfy` (>= spPeakUpper exact) +boundSpec :: Spec +boundSpec = describe "the bound language" $ do + it "adds cell counts and keeps the worse alternative" $ do + let a = sbAdd (sbConst 3) (sbScale 2 (sbInput 0)) + renderSpaceBound a `shouldBe` "2·|input| + 3 cells" + renderSpaceBound (sbMax a (sbConst 100)) `shouldBe` + "max(100, 2·|input| + 3) cells" + + it "prunes an affine another one dominates" $ do + -- 2·|input| + 3 stands above |input| + 1 everywhere, so the maximum + -- forgets the smaller one. + let big = sbAdd (sbScale 2 (sbInput 0)) (sbConst 3) + small = sbAdd (sbInput 0) (sbConst 1) + sbMax big small `shouldBe` big + -- Incomparable affines both stay. + let other = sbAdd (sbScale 3 (sbInput 1)) (sbConst 1) + sbMax big other `shouldSatisfy` \b -> + b /= big && b /= other && b == sbMax other big + + it "substitutes known input sizes and goes concrete" $ do + let b = sbAdd (sbScale 3 (sbInput 1)) (sbConst 12) + sbConcrete b `shouldBe` Nothing + sbConcrete (sbSubstitute (Map.singleton 1 5) b) `shouldBe` Just 27 + + it "widening stands above everything it replaced" $ do + -- Widen a maximum of incomparable affines to width 1, then check the + -- widened bound is at least each original at sample input sizes. + let affs = [ sbAdd (sbScale c (sbInput p)) (sbConst k) + | (c, p, k) <- [(2, 0, 3), (1, 1, 9), (5, 2, 0)] ] + combined = foldr1 sbMax affs + widened = sbWiden 1 combined + sizes = Map.fromList [(0, 4), (1, 7), (2, 1)] + at b = sbConcrete (sbSubstitute sizes b) + at widened `shouldSatisfy` \w -> all (\a -> at a <= w) affs + + it "checks a measured figure against the bound" $ do + let b = sbAdd (sbInput 0) (sbConst 2) + sizes = Map.singleton 0 10 + sbAtLeast 12 sizes b `shouldBe` True + sbAtLeast 13 sizes b `shouldBe` False + -- The bound that says nothing bounds everything. + sbAtLeast 1000000 sizes sbTop `shouldBe` True + -- A bound still symbolic after substitution verifies nothing. + sbAtLeast 0 Map.empty b `shouldBe` False + + it "renders paths as the words a reader would use" $ do + renderSpaceBound (sbInput 0) `shouldBe` "|input| cells" + renderSpaceBound (sbInput 5) `shouldBe` "|input.right.left| cells" + renderSpaceBound sbTop `shouldBe` "unknown" + +-- |The headline invariant: on every corpus program, the static bound with +-- the actual input sizes substituted stands at or above the exactly measured +-- live-heap peak. This is the empirical check of the simulation between the +-- abstract and the concrete machine. +-- +-- The bound covers refinement-valid runs: the abstract input is shaped by +-- the same refinement-derived restrictions the sizing pass uses, so a run +-- whose input fails a check — which constructs and retains the aborted +-- message — is outside it. Such iterations are detected by `spAborts` and +-- not compared; at least one abort-free iteration must remain, or the test +-- would be vacuous. +staticVsMeasuredSpec :: Spec +staticVsMeasuredSpec = describe "the static bound stands above the measured peak" $ + mapM_ checkOn corpus + +checkOn :: (FilePath, String, [String]) -> Spec +checkOn (path, name, inputs) = it name $ do + modules <- loadWith path name + case compileModules modules name of + Left err -> expectationFailure $ "failed to compile:\n" <> err + Right (report, sized) -> case sizingReportSpace report of + Left why -> expectationFailure $ "no static bound: " <> why + Right bound -> do + -- `sbAtLeast` lets the bound that says nothing pass anything, so a + -- walk that produced it would make every comparison below vacuous. + bound `shouldNotBe` sbTop + -- A world the walk closed as impossible is a world it did not + -- follow; a bound over any of those is weaker evidence, so none may + -- occur on the corpus. + case sizingReportSpaceStats report of + Just (Right stats) -> ssDeadWorlds stats `shouldBe` 0 + other -> expectationFailure $ "no walk statistics: " <> show other + checked <- loop sized bound ZeroB inputs 0 + checked `shouldSatisfy` (> 0) + where + loop :: CompiledExpr -> SpaceBound -> CompiledExpr -> [String] -> Int -> IO Int + loop sized bound st inps checked = do + let applied = appB sized st + (m, r) = evalSpace SweepEveryAlloc applied + sizes = Map.fromList [ (p, sizeAtPath st p) | p <- sbPaths bound ] + validRun = spAborts m == 0 + unless (not validRun || sbAtLeast (spPeakUpper m) sizes bound) + . expectationFailure $ + "measured " <> show (spPeakUpper m) <> " cells, bound only " + <> renderSpaceBound (sbSubstitute sizes bound) + let checked' = checked + fromEnum validRun + case r of + Left _ -> pure checked' -- an abort ended the session + Right v -> case project v of + BasicFW (PairSF _ newState) -> case (project newState, inps) of + (BasicFW ZeroSF, _) -> pure checked' + (_, []) -> pure checked' + (_, i : rest) -> loop sized bound (PairB (str2b i) newState) rest checked' + _ -> expectationFailure "unexpected iteration result" >> pure checked' + -- |The input as the driver builds it, at the compiled type. str2b :: String -> CompiledExpr str2b = foldr (PairB . unary . ord) ZeroB +-- |Directions from the root, decoded from a path index. +pathSteps :: Integer -> [Bool] +pathSteps = go [] where + go acc 0 = acc + go acc p + | odd p = go (True : acc) ((p - 1) `div` 2) + | otherwise = go (False : acc) ((p - 2) `div` 2) + +-- |How many cells the input part at a path holds. Projecting past a zero +-- stays zero, as the machine's projections do. +sizeAtPath :: CompiledExpr -> Integer -> Natural +sizeAtPath v p = cells (walk v (pathSteps p)) where + walk :: CompiledExpr -> [Bool] -> CompiledExpr + walk x [] = x + walk x (s : rest) = case project x of + BasicFW (PairSF a b) -> walk (if s then a else b) rest + _ -> x + cells :: CompiledExpr -> Natural + cells = cata $ \case + BasicFW ZeroSF -> 1 + BasicFW (PairSF a b) -> 1 + a + b + _ -> 1 + -- |Tick parity and the adaptive bracket, across a whole session on the real -- inputs — the conformance suite checks the first, empty-input iteration only. sessionParitySpec :: Spec @@ -102,3 +243,123 @@ parityOn (path, name, inputs) = it name $ do , (i : rest) <- inps -> loop sized (PairB (str2b i) newState) rest _ -> pure () + +-- |Programs small enough to reason about, run through the abstract walk. +staticFixtureSpec :: Spec +staticFixtureSpec = describe "the abstract walk" $ do + it "forks on an unknown input, joins, and bounds both sides" $ + case evalSpaceStatic' defaultStaticSpaceFuel mempty oneGate of + Left why -> expectationFailure $ "no bound: " <> show why + Right stats -> do + ssDeadWorlds stats `shouldBe` 0 + ssWidenings stats `shouldBe` 0 + -- The bound is in the whole input and nothing else. + sbPaths (ssBound stats) `shouldBe` [0] + forM_ [ZeroB, PairB ZeroB ZeroB, PairB (unary 3) (unary 2)] $ \input -> do + let (m, _) = evalSpace SweepEveryAlloc (appB oneGate input) + sbAtLeast (spPeakUpper m) (Map.singleton 0 (sizeAtPath input 0)) (ssBound stats) + `shouldBe` True + + it "widens a superposition nested past the cap, and still bounds every run" $ + case evalSpaceStatic' defaultStaticSpaceFuel mempty nestedGates of + Left why -> expectationFailure $ "no bound: " <> show why + Right stats -> do + ssDeadWorlds stats `shouldBe` 0 + ssWidenings stats `shouldSatisfy` (> 0) + forM_ [ZeroB, str2b "ab", str2b "abcdefgh"] $ \input -> do + let (m, _) = evalSpace SweepEveryAlloc (appB nestedGates input) + sizes = Map.fromList [ (p, sizeAtPath input p) | p <- sbPaths (ssBound stats) ] + sbAtLeast (spPeakUpper m) sizes (ssBound stats) `shouldBe` True + + it "refuses to apply a widened value rather than guess" $ + case evalSpaceStatic' defaultStaticSpaceFuel mempty (closure (FillFunctionEE nestedBody ZeroB)) of + Left (SpaceUnsupported _) -> pure () + other -> expectationFailure $ "expected an unsupported report, got " <> show other + + it "keeps simpleplus at its recorded bound" $ do + -- A golden: a change here is a change to the bound's precision, up or + -- down, and deserves the same look as a changed iteration count. + modules <- loadWith "simpleplus.tel" "simpleplus" + case compileModules modules "simpleplus" of + Left err -> expectationFailure $ "failed to compile:\n" <> err + Right (report, _) -> case sizingReportSpace report of + Left why -> expectationFailure $ "no static bound: " <> why + Right bound -> renderSpaceBoundBrief bound + `shouldBe` "sizes of 116 input parts (116 weighted) + 4337 cells" + +-- |A program as the machine applies one: a closure is a pair of code and its +-- captured environment, and once applied the argument is the left part of +-- the environment its body sees. The captured part is a zero here, as the +-- sizing pass leaves a program with nothing to capture. +closure :: CompiledExpr -> CompiledExpr +closure body = PairB (deferB 7 body) ZeroB + +-- |The argument, inside a `closure` body. +arg :: CompiledExpr +arg = LeftB EnvB + +-- |A program that tests its whole input: zero or a pair. +oneGate :: CompiledExpr +oneGate = closure (GateSwitchEE ZeroB (PairB ZeroB ZeroB) arg) + +-- |The head of the k-th element of the input list: @left (right^k input)@. +element :: Int -> CompiledExpr +element k = LeftB (iterate RightB arg !! k) + +-- |Tests on six independent input parts, nested, every leaf a different +-- number: each join is a genuine superposition of the joins below it, so +-- the nesting outgrows the widening cap. +nestedBody :: CompiledExpr +nestedBody = go 0 0 where + go :: Int -> Int -> CompiledExpr + go k acc + | k == 6 = unary acc + | otherwise = GateSwitchEE (go (k + 1) (2 * acc)) (go (k + 1) (2 * acc + 1)) (element k) + +nestedGates :: CompiledExpr +nestedGates = closure nestedBody + +-- |Laws of the bound language, checked at random sizes: the language is a +-- max-plus algebra and widening only ever loosens. +boundLawSpec :: Spec +boundLawSpec = describe "the bound language's laws" $ do + prop "a maximum evaluates to the larger side" $ \(Few a) (Few b) -> + forAll sizes $ \s -> at s (sbMax a b) === max (at s a) (at s b) + prop "a sum evaluates to the sum" $ \(Few a) (Few b) -> + forAll sizes $ \s -> at s (sbAdd a b) === at s a + at s b + prop "addition distributes over the maximum" $ \(Few a) (Few b) (Few c) -> + forAll sizes $ \s -> at s (sbAdd a (sbMax b c)) === at s (sbMax (sbAdd a b) (sbAdd a c)) + prop "the maximum is idempotent and commutative" $ \(Few a) (Few b) -> + sbMax a a === a .&&. sbMax a b === sbMax b a + prop "widening stands above what it replaced" $ \(Few a) (Few b) -> + forAll sizes $ \s -> at s (sbWiden 1 (sbMax a b)) >= max (at s a) (at s b) + prop "substituting in two steps is substituting at once" $ \(Few a) -> + forAll sizes $ \s -> + let (front, back) = Map.partitionWithKey (\p _ -> even p) s + in at back (sbSubstitute front a) === at s a + where + sizes :: Gen (Map Integer Natural) + sizes = Map.fromList <$> mapM (\p -> (,) p . fromIntegral <$> chooseInt (0, 9)) [0 .. 5] + at :: Map Integer Natural -> SpaceBound -> Natural + at s b = fromMaybe (error "still symbolic after substitution") + (sbConcrete (sbSubstitute s b)) + +-- |A bound of a few affines over paths 0..5, so that every law is exercised +-- without widening getting in the way. +newtype Few = Few SpaceBound + deriving Show + +instance Arbitrary Few where + arbitrary = do + n <- chooseInt (1, 3) + Few . foldr1 sbMax <$> vectorOf n affine + where + affine = do + k <- chooseInt (0, 6) + terms <- listOf term + pure $ foldr (\(p, c) b -> sbAdd (sbScale c (sbInput p)) b) + (sbConst (fromIntegral k)) (take 3 terms) + term = do + p <- chooseInt (0, 5) + c <- chooseInt (0, 4) + pure (toInteger p, fromIntegral c :: Natural) From a2b52eb09289fee37a6a36958db66beaace81938 Mon Sep 17 00:00:00 2001 From: hhefesto Date: Tue, 15 Sep 2026 13:36:43 -0600 Subject: [PATCH 3/3] Report the space bound in the certificate and after --compile The certificate gains a space section between sizing and structure: the bound as an expression over input-part sizes, stated for refinement- valid inputs (a run whose input fails a check builds and retains the aborted message, which is outside it), or an honest unknown with the reason it could not be found. --compile's summary line carries the same figure, so the line that says what was written also says what running it will cost. Affines over many input parts are summarized in report lines rather than spelled out path by path. The README's timings are refreshed from measured runs, since two of them had drifted: sizing tictactoe.tel takes about 13 seconds, not the 70 it claimed before the sizing pass got faster, the abstract walk adds some eight more, and the sample certificate's nesting columns are restated from real output. --- README.md | 31 +++++++++++++++++++++++++------ app/Main.hs | 9 +++++++-- src/Telomare/Certificate.hs | 17 ++++++++++++++++- 3 files changed, 48 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index 0be2864..fcc4a79 100644 --- a/README.md +++ b/README.md @@ -67,10 +67,14 @@ recursion sites (iterations, over every input): sizing budget in force: 65536 unrollings +space (static bound, refinement-valid inputs): sizes of 116 input parts (116 weighted) + 4337 cells + |input.path| stands for the size in cells of that input part; + a run whose input fails a refinement is outside this bound. + recursion nesting (structural, approximate): triple function levels - Prelude:11:19 Prelude.d2c 0, 1 - Prelude:44:34 Prelude.foldr.fixed 0, 1 + Prelude:11:17 Prelude.d2c 0, 1 + Prelude:44:32 Prelude.foldr.fixed 0, 1 ``` The counts assert nothing new: they are the numbers already baked into the @@ -104,6 +108,19 @@ over *distinct* nodes from what the machine still holds, and it is printed as a bracket — a figure the run reached and one it never exceeded — because the measuring sweep is amortized rather than run at every allocation. +The certificate's `space` line is the static side of the same figure: the +same machine, written over abstract values, walked at compile time over a +symbolic input and reporting the peak as an expression over input sizes. The +two are tested against each other: on `simpleplus.tel` and +`tc_ultra_minimal.tel`, the bound with the actual input sizes substituted must +stand at or above the exactly measured peak of every refinement-valid +iteration, and small programs built to fork, widen and refuse pin the walk's +behaviour directly. On `tictactoe.tel` the walk converges in about eight +seconds after sizing: the bound is a maximum of two affines whose +constants top out under seventy thousand cells — about three times the +measured peak of a completed game, loose where a deep superposition is +widened to its bound alone, but finite and sound. + When sizing fails, the error names the recursion, where it is, and which of the two failures it is — a budget that was too small, or an input that nothing bounds. Only the first is fixable by raising the budget. See @@ -111,12 +128,13 @@ bounds. Only the first is fixable by raising the budget. See ## Compiling once -Sizing is the slow part — about 70 seconds for `tictactoe.tel` — and it gives -the same answer every time, because it runs the program over a *symbolic* -input. So it need only happen once: +Sizing is the slow part — about 13 seconds for `tictactoe.tel`, with the space +walk above adding some eight more — and it gives the same answer every time, +because it runs the program over a *symbolic* input. So it need only happen +once: ```sh -$ cabal run telomare -- tictactoe.tel --compile # ~70s, writes tictactoe.telc +$ cabal run telomare -- tictactoe.tel --compile # ~23s, writes tictactoe.telc $ cabal run telomare -- tictactoe.telc # starts immediately ``` @@ -372,6 +390,7 @@ pipeline. In pipeline order: | Type check | `Telomare.TypeCheck` | unification-based check of `Term3` against the main type. | | Size (totality) | `Telomare.Size`, `Telomare.Size.IR`, `Telomare.Machine` | telomare's distinguishing stage: `sizeTermM` abstractly interprets the program over symbolic input and infers a finite iteration count for every recursion site, then bakes the counts in (`Term3 -> CompiledExpr`). A program that cannot be sized does not compile. `Machine` is the shared step-algebra the sizing pass and the evaluators are assembled from. | | Evaluate | `Telomare.Eval.Reference`, `Telomare.Eval.Meter`, `Telomare.Eval.Space`, `Telomare.Fast` | the reference interpreter, the step-counting meter, the space machine that also measures the live-heap peak, and the fuel-based fast path (which skips sizing). | +| Bound | `Telomare.SpaceBound`, `Telomare.Space.Static` | the space-bound language (maxima of affines in input sizes) and the compile-time abstract walk that produces one. | | Drive | `Telomare.Driver`, `Telomare.Artifact`, `Telomare.Certificate`, `Telomare.Levels` | orchestration (`compileModules`, `evalLoop`), `.telc` artifacts, and the static report. | The IR vocabulary shared by all stages lives under `Telomare.IR.*` diff --git a/app/Main.hs b/app/Main.hs index fd14d5c..be75adb 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -23,7 +23,8 @@ import Telomare.IR.Loc (locatedNameText) import Telomare.IR.Surface (ImportDecl (parsedImportModule), ModuleItem (..)) import Telomare.Levels (levelsInfo) import Telomare.Parse (runParseModule) -import Telomare.Size (SizingReport) +import Telomare.Size (SizingReport (sizingReportSpace)) +import Telomare.SpaceBound (renderSpaceBoundBrief) -- |What to do with the program. data Action @@ -189,8 +190,12 @@ runSized file action = do , artifactExpr = sized } writeArtifact path artifact + let spaceNote = case sizingReportSpace report of + Left _ -> "" + Right b -> ", space <= " <> renderSpaceBoundBrief b hPutStrLn stderr $ "wrote " <> path <> " (" <> show (nodeCount sized) - <> " nodes, sources " <> take 12 (sourcesHash allModules) <> ")" + <> " nodes" <> spaceNote + <> ", sources " <> take 12 (sourcesHash allModules) <> ")" -- |Without sizing. The program runs on demand under a fuel cap; no iteration -- count exists, so the certificate reports structure only. diff --git a/src/Telomare/Certificate.hs b/src/Telomare/Certificate.hs index 35967d4..e6e4dc9 100644 --- a/src/Telomare/Certificate.hs +++ b/src/Telomare/Certificate.hs @@ -33,6 +33,7 @@ import Telomare.Levels (BindingKey, LevelsInfo (..), SiteKey (..), bangs, renderBinding, renderDef, renderLevels, renderSource) import Telomare.Size (SizingReport (..)) import Telomare.Size.IR (SizedRecursion (..)) +import Telomare.SpaceBound (renderSpaceBoundBrief) import Telomare.Util (padRight, plural) -- |The whole static report. @@ -44,7 +45,7 @@ renderStaticReport :: Maybe String -- ^Source hash, when read from an artifact. -> Either String LevelsInfo -- ^Levels, or why there are none. -> String renderStaticReport sourceHash sizing levels = unlines $ - header <> [""] <> sizingSection <> [""] <> structuralSection <> closing + header <> [""] <> sizingSection <> spaceSection <> [""] <> structuralSection <> closing where header = "static report: what the compiler knows without running the program" @@ -59,6 +60,20 @@ renderStaticReport sourceHash sizing levels = unlines $ <> ["", "sizing budget in force: " <> show (sizingReportBudget report) <> " unrollings"] + -- The space bound rides with sizing: both come from the same abstract + -- walk machinery, and neither exists for an unsized program. + spaceSection = case sizing of + Nothing -> [] + Just report -> case sizingReportSpace report of + Left why -> + ["", "space (static bound): unknown -- " <> why] + Right bound -> + [ "" + , "space (static bound, refinement-valid inputs): " + <> renderSpaceBoundBrief bound + , " |input.path| stands for the size in cells of that input part;" + , " a run whose input fails a refinement is outside this bound." ] + structuralSection = case levels of Left err -> ["recursion nesting: unavailable (" <> err <> ")"] Right info ->