Space bounds: measure the live-heap peak, and bound it statically

.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

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 thirteen 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.*`

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.

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,13 +44,15 @@ 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
 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 = 4
 
 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.
 

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 ->

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 "" []

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
 --