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..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 @@ -83,22 +87,39 @@ 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. + +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 @@ -107,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 ``` @@ -367,7 +389,8 @@ 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). | +| 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 460ea33..be75adb 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -15,15 +15,16 @@ 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) 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 @@ -148,8 +149,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 +177,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 @@ -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/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/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 -> diff --git a/src/Telomare/Driver.hs b/src/Telomare/Driver.hs index e6973e2..7f9b9d4 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 @@ -33,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) @@ -78,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 @@ -87,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 = @@ -276,6 +284,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/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 8238895..66be9c3 100644 --- a/telomare.cabal +++ b/telomare.cabal @@ -38,12 +38,15 @@ library , Telomare.Lexical , Telomare.Machine , Telomare.Eval.Meter + , Telomare.Eval.Space , Telomare.Expand , Telomare.Parse , Telomare.PrettyPrint , Telomare.PrettyPrint.Indent , Telomare.Resolve , Telomare.Size + , Telomare.SpaceBound + , Telomare.Space.Static , Telomare.Size.IR , Telomare.TypeCheck , Telomare.Util @@ -186,10 +189,13 @@ test-suite telomare-sizing-test other-modules: ConformanceTests , RunModeTests , SizingTests - build-depends: base + , SpaceTests + build-depends: QuickCheck + , 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/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 cd021ab..a55fa11 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,9 @@ main = hspec $ do sizingSpec runModeSpec conformanceSpec + spaceSpec + sessionParitySpec + boundSpec + boundLawSpec + staticFixtureSpec + staticVsMeasuredSpec diff --git a/test/SpaceTests.hs b/test/SpaceTests.hs new file mode 100644 index 0000000..f7e0d24 --- /dev/null +++ b/test/SpaceTests.hs @@ -0,0 +1,365 @@ +{-# 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 +-- 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 Control.Monad (forM_, unless) +import Data.Char (ord) +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) + +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) +import Telomare.Size (SizingReport (..)) +import Telomare.Space.Static (StaticSpaceFailure (..), StaticSpaceStats (..), + defaultStaticSpaceFuel, evalSpaceStatic') +import Telomare.SpaceBound + +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) + +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 +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 () + +-- |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)