From 8af19a545b2e558b4e54f10390d951115362eeb3 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Mon, 3 Aug 2026 09:45:05 -0400 Subject: [PATCH] =?UTF-8?q?Add=20FABRIC.md=20=E2=80=94=20Stadium=20design,?= =?UTF-8?q?=20sections=201-18?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Captures the 2026-08-03 design session: collapsing the four independent heat/TTL/pin implementations (blocks, messages, console cells, ACLs) into one bounded Stadium of fixed-size entries, driven by an engine below every VM. Sections 1-15 are the original design argument. Sections 16-18 add: - 16 Substrate findings. No IRQ return path exists on aarch64 or riscv64; riscv64's time base is a hardcoded 1 GHz guess; the dictionary already carries six of the seven entry wires; the engine must stay deterministic. - 17 Patrons. TTL, heat decay and pin are three distinct mechanisms on one tick, not a type field. Reap means leaves the floor, not destroyed. The framebuffer is a utility, not a patron. Dynamic in capacity, static in structure. - 18 The engine (L0). L0 and L8 bookend the gated loops L1-L7, both ungated. Jacquard stays 7-bit/128 states, accounting for L0 by its absence. Dispatch enumerates behaviours, never patron kinds. Determinism traced end to end and confirmed intact: TIME-TRUST is measured and never fed back, inference inputs are wholly execution-derived, decay is tick-based, and the parity hash covers only word name and execution_heat. One pre-existing exception recorded — vm_physics_touch scales fleet heat by wall-clock elapsed time, outside the parity path. Draft. Sections marked DECIDED / LEANING / OPEN throughout. Co-Authored-By: Claude Opus 5 --- FABRIC.md | 925 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 925 insertions(+) create mode 100644 FABRIC.md diff --git a/FABRIC.md b/FABRIC.md new file mode 100644 index 0000000..a214b29 --- /dev/null +++ b/FABRIC.md @@ -0,0 +1,925 @@ +# FABRIC.md — DRAFT + +**Status:** Draft for review. Captures the design session of 3 August 2026. +**Nothing here is committed.** Sections are marked **DECIDED**, **LEANING**, or **OPEN** so +you can argue with it rather than inherit it. + +--- + +## 1. The claim + +StarshipOS currently has four subsystems that each independently implement the same +physics: Artemis heats blocks, Hermes ages messages, Console heats dirty cells, ACLs +carry heat and TTL. Four implementations, one pattern. + +The claim is that this is one mechanism wearing four costumes, and that the dictionary +is already the reference implementation of it. Lift the dictionary one level of +abstraction and every subsystem becomes an instance rather than a special case. + +The argument that decides it: **they already have the same wires.** Blocks felt +different because they are large and live on disk — but size and location are not +properties, they are payload details. Strip those away and a block has exactly what a +message has. + +**DECIDED.** Direction is not optional. The remaining question is effort, not validity. + +--- + +## 2. The arena + +A single region of memory, outside any VM, holding everything currently **live**. + +- Bounded capacity. The bound is real and inescapable, and it is what gives K≡1.0 a + fixed denominator. Without a hard outer wall, K is bookkeeping rather than a + conservation law. +- Allocated at boot, before any VM exists. +- Not part of the heap. + +The critical scoping decision, and the one that keeps this from sprawling: + +> **The arena holds what is live. Not everything that exists.** + +**DECIDED.** + +--- + +## 3. The entry + +One structure. No variants, no type field, no subclassing. + +| Wire | Meaning | +|---|---| +| identity | handle or name | +| heat | current thermal state | +| TTL | remaining lifetime | +| pin | invariance flag (opposite of TTL, not an extension of it) | +| link | index into the arena, not a pointer | +| code field | what to do when this entry is worked | +| payload | inline if small, by reference if large | + +Fixed-size cells. Links are indices, so the arena stays an array — no fragmentation, +and tractable for Isabelle later. + +**The code field is the entire type system.** A block's code field migrates. A message's +delivers. A VM's ticks. The engine never asks what kind of thing it is holding; it +heats, ranks, reaps, and calls the code field. + +> If you find yourself wanting a type field so the engine can branch on entry kind, the +> design has gone wrong. The code field already answers that question. + +**DECIDED**, except payload threshold — see Open Questions. + +--- + +## 4. Heat + +Heat is **conferred by traffic, not intrinsic to the entry.** + +This is the piece that was missing for most of the session. Nothing decides what matters. +An entry is hot because activity is concentrated around it — the way a crowd in front of +one car makes that corner of the hall hot. Density generates heat; nobody computes it. + +Consequences: + +- **Ranking is read, not decided.** There is no scheduler because there is no policy. + The arena is simply already in heat order when you look at it. +- **K constrains the total,** so ordering is forced by conservation rather than by tuned + parameters. There is nothing to tune wrongly. This is the defensible distinction from + a scheduler and it belongs in the write-up. +- **Popularity is self-limiting.** A crowded entry is harder to reach, which throttles + traffic to it, which cools it. The governor is local and emergent — no global damping + constant to pick. + +TTL expiry stays unconditional: entries leave at their own time, unscheduled, nobody's +decision. Pinning remains the separate, opposite mechanism — invariance, not longevity. + +**LEANING.** The causality is right; the density formulation needs a concrete definition. + +--- + +## 5. What is *not* in the arena + +This section exists because forcing everything in is how this design turns into a mess. + +- **Storage is beneath the arena.** The show floor is not the warehouse. Artemis is where + entries live when they are not in play. Blocks migrate onto the floor when hot and back + out when cold — which is heat-driven block migration, already built. Artemis does not + become an arena occupant; it becomes what the arena pages against. +- **Devices are beside the arena.** The framebuffer is the building's lighting, not an + occupant. Console's dirty *events* are arena entries; the pixels are not. + +**DECIDED.** Three sharp edges, nothing forced. + +--- + +## 6. Boot order + +The engine cannot be a VM service, because VMs live inside the thing it manages. + +1. LithosAnanke establishes the arena and starts the engine. +2. Hera becomes the first entry in it. +3. Hera births everything else, sizing each VM as it goes. + +Structurally the same move as minting Zuse's certificate at first boot: a root that +cannot be produced by the mechanism it grounds. + +**LEANING.** Order is right; the allocation mechanism is unspecified. + +--- + +## 7. Hera + +Hera's job becomes arena distribution. This is not a new responsibility — allocating a +VM's share *is* birthing it, and lifecycle is already what Hera is for. + +**OPEN:** whether a VM's share is a hard bound or an elastic one that can grow and shrink +under pressure, with capacity transferring between VMs as a conserved operation Hera +arbitrates. Elastic is more powerful and more work. Under elasticity, birth sizes the +*rest* volume rather than a cap — a more forgiving thing to have to guess right. + +--- + +## 8. The mental model + +An auto show hall. + +Cars and people, in a building with a fixed capacity. People arrive and leave at their +own times. They ask questions and converse — those are the messages. They stand in front +of a car for a while and move on. Occasionally one sits in a car, which is the only +exclusive thing in the room, scoped to a single object, no global lock. + +The hall gets crowded. Crowds get hot. + +**One discipline to hold:** cars and people cannot be two structures. That would be a type +field re-entering through a metaphor. They are one entry shape differing only in TTL and +code field — a car's lifetime is the show, a person's is a visit; a car's code field is +*be attended to*, a person's is *move and attend*. + +--- + +## 9. The admission test + +Before writing code, run this on paper against every candidate entry type. Two questions, +both of which must have a non-forced answer: + +1. **What does heat mean for this thing?** +2. **What is its reap event?** + +| Type | Heat means | Reap is | Verdict | +|---|---|---|---| +| Block | accessed often | migration | passes | +| Message | delivery urgency | delivery | passes | +| VM | runs often | execution / death by cooling | passes | +| ACL | checked often | ? | check | +| Screen cell | ? | redraw, which removes nothing | **suspect** | + +Screen cells are the one to resolve first. A cell never expires — it is a fixed grid +position always present. If cells are permanent arena entries, most of the arena is inert +and permanently pinned. The likely correct read is that the arena entry is the **dirty +event**, not the cell: transient, honest TTL, and the grid stays outside where it belongs. + +Ten minutes on paper. Either it confirms the design or it finds the one case that breaks +it, before any code moves. + +--- + +## 10. Sequencing + +**FABRIC.md first, then Hermes native on the fabric, then measure, then Console, then +Artemis last.** + +Reasoning: + +- Hermes is unfinished, which is lucky. Finishing it the old way and refactoring later + means deliberately writing code already slated for deletion. Build it on the fabric + directly and it carries zero migration debt. +- It becomes the proving ground — the fabric gets tested against a real subsystem before + anything that currently works is touched. +- **It produces the effort number empirically.** What Hermes costs is the multiplier for + everything else. One data point from real work beats any amount of estimating. +- Artemis reads, writes, and persists reliably today. That is banked. It goes last, + because it is the thing you cannot afford to break. + +Existing instrument: the POST suite exercises every dictionary word and was already +earmarked as the regression gate for the shrink-to-colon-definitions pass. Same tool, +second job. + +**Caution:** a green POST suite does not mean K still holds. Those are different claims. +The DoE campaign validated K on the *current* substrate; changing the substrate means +re-running it. Automated, but budget for it. + +--- + +## 11. Where the debt accrues + +- **Dual paths — avoidable, and the big one.** Never two live heat mechanisms at once. + Convert one subsystem completely, prove it, move on. Every shim bridging old and new is + debt, and new code will get written against whichever is convenient. +- **Speculative generality — avoidable.** Only add a wire when a second entry type needs + it. Generality that never pays back is still debt. +- **The exception — not avoidable, so decide it early.** If one subsystem does not fit and + gets special-cased, that special case is permanent and worse than not unifying: you + carry the general machinery *and* the exception, and every future reader learns both. + This is why the admission test comes before code. + +**Early signal:** ARTEMIS.md, HERMES.md, CONSOLE.md and TRIPOD.md each currently describe +their own heat mechanics. After FABRIC.md, each should shrink to roughly three lines — +what an entry is here, what heat means, what the reap event is. If any one of them gets +*longer*, that subsystem is fighting the fabric, and you will know which one before +writing code. + +--- + +## 12. Open questions + +1. Payload threshold — what size goes inline versus by reference. +2. Arena entry header size. Cardinality spans orders of magnitude (dozens of VMs, + thousands of messages, potentially very many screen events). The header must be sized + for the worst case, and that case is the screen. Sizing this constrains everything + else, so settle it early. +3. Screen cells: entry-per-cell or entry-per-dirty-event. (Leaning: event.) +4. Per-VM share — hard bound or elastic under pressure. +5. Loop coupling. Roughly eight feedback loops once Hera and heartbeat depth are counted. + The algorithms are known; the risk is interference. Usual discipline is separation of + timescales — keep nested loop periods an order of magnitude apart. Cheaper to decide + than to debug. +6. Whether the arena is one region for the whole system or nested per VM. Nested implies + K conserved at each level with messages as the only thing crossing a boundary, which + would mean no shared-memory atomicity is ever needed. Single region is simpler but + reintroduces locking — the one mechanism this architecture has otherwise never wanted. + +--- + +## 13. What this does to formal verification + +This may be the largest payoff, and it was not the reason for the change. + +Verifying four subsystems means four state models, four conservation arguments, and — the +expensive part — proofs about how they interact. That last category grows combinatorially +and is where a verification effort usually dies. Unification deletes it outright. + +What the design gives Isabelle/HOL, more or less for free: + +- **One datatype.** The arena entry is a single record. Everything else is payload. You + reason about `entry` once rather than about blocks, messages, VMs and events separately. +- **No pointers.** Fixed-size cells with index links means the arena models as a total + function over a finite index set — no heap model, no separation logic, no aliasing, no + null. This is the single biggest difference between a tractable proof effort and a + research project. +- **Finite state.** Bounded capacity means the state space is finite. Induction over the + arena is straightforward, and model checking becomes available alongside theorem proving. +- **One conservation theorem.** *Every engine operation preserves K.* Proved once against + the engine, it holds for every entry kind — because the engine cannot distinguish them. + Previously this was four proofs plus their interactions. +- **A clean model boundary.** Storage below and devices beside the arena means disk I/O and + framebuffer writes sit outside the model, at the C primitive boundary already drawn. +- **A trivial initial state.** Boot order — kernel, then arena, then engine, then Hera — + gives a base case that is trivially conserving, with everything else following by + induction on operations. + +**One constraint this imposes, and it is not optional.** + +The code field is late-bound behaviour, which is the one part of this that HOL does not +like: an arbitrary function stored in a record is higher-order and can wreck termination +arguments. The fix is a design rule rather than a proof technique: + +> **The set of code-field behaviours must be a closed enumeration, fixed at build time.** + +Model it as a datatype of behaviour tags plus a dispatch function and the whole thing stays +first-order and tractable. Leave the code field open as a general extension point and you +have traded four easy verification problems for one genuinely hard one. + +This is consistent with the existing rule that adding a primitive requires rebuilding from +source rather than doing it from inside a running system. Worth stating explicitly in the +fabric design, because it is the kind of constraint that gets casually violated later by +someone adding "just one" dynamic behaviour. + +--- + +## 14. Formalism + +The thermodynamic analogy holds in places and inverts in one, which matters for the paper +but not for the build. + +- Fixed capacity → closed system. K≡1.0 → conservation. Capacity transfer → work. These + map cleanly. +- **Heat is not entropy.** Heat is closer to energy or temperature. Entropy would measure + how heat is *distributed*: concentrated is low, uniform is high. +- **This matters practically.** K is conserved, so K can never tell you anything — it is + 1.0 by construction, a correctness check rather than a diagnostic. Entropy over the heat + distribution actually varies, and distinguishes idle from productive from thrashing. + That is the real instrument, and the quantity worth driving the LED matrix with. +- **The inversion:** the second law says entropy rises spontaneously. This system does the + opposite — it self-organizes, concentrating heat where work happens. That is not + equilibrium thermodynamics; it is a **driven dissipative system**, order sustained by + throughput. Prigogine, not Carnot. A stronger claim, but only if stated correctly — + writing "thermodynamic system" while entropy decreases unprompted is an easy shot for a + reviewer. + +Phenomenon first, then mathematics. The formalism follows the phenomenon; it does not gate +the build, and it is not finished until it is correct. + +--- + +## 15. The whole thing in five lines + +- The arena holds the live crowd. Storage is the warehouse. Devices are the building. +- One entry shape. The code field is the only difference between kinds. +- Heat is density, conferred by traffic. Nobody decides. +- Departure is unconditional. Pinning is invariance, not longevity. +- The kernel opens the hall. Hera walks in first. + +--- + +## 16. Substrate findings — 2026-08-03 + +Naming: the arena is now called the **Stadium**, because `src/starkernel/vm/arena.c` +already owns "arena" for the PMM-backed VM page allocator — an unrelated concept. Sections +1–15 above still say arena and have not been reconciled. + +Four findings from reading the tree. The first three change what step one costs. The +fourth changes what the engine is allowed to be. + +### 16.1 There is no interrupt return path on two of three ISAs + +The engine has to be driven from outside the VMs (§6), which in a kernel means interrupts. +That mechanism does not currently exist on most of our targets. + +- `apic_timer_start()` is an explicit no-op stub on aarch64 (`arch/aarch64/apic.c:82`) and + riscv64 (`arch/riscv64/apic.c:76`). Both say the driver is deferred. +- `heartbeat_tick()` is defined on all three architectures and *called* from exactly one + site in the tree: `arch/amd64/interrupts.c:337`. On the other two it is dead code. +- Worse: every vector in `arch/aarch64/isr.S` — IRQ included — is a bare branch to a + handler that prints and enters `for(;;) wfe`. `arch/riscv64/isr.S` is the same shape. + There is no register save, no `ERET`, no `SRET`. + +So enabling a timer interrupt today halts the kernel on the first tick. The work is not +"write a timer driver," it is "build the interrupt return path that was never built." + +**Consequence for §12 Q5.** That question assumes a hierarchy of loop periods kept an +order of magnitude apart. Separation of *timescales* presupposes a time base. There is +one real time source, on one architecture; everything else paces off execution count. +Q5 cannot be answered on the current substrate — it is downstream of this work, not +parallel to it. + +### 16.2 riscv64's time base is a guess + +`arch/riscv64/timer.c:46` sets `s_counter_hz = 1000000000ULL` with the comment +`/* assume 1 GHz */`. The file header concedes `rdcycle`'s frequency is not +architecturally discoverable. + +Every heartbeat variance and TIME-TRUST figure riscv64 has produced was computed against +a wrong `expected_delta`. This has to be fixed as part of any timer work, and it means +riscv64 timing numbers before and after that fix are not comparable. + +### 16.3 The dictionary is already a Stadium + +§1 claims the dictionary is the reference implementation. It is stronger than that. +`DictEntry` today carries six of the seven wires in §3: + +| §3 wire | Already in `DictEntry` | +|---|---| +| identity | name / `word_id` | +| heat | `physics.*` (Loop #1) | +| TTL | `acl_ttl` | +| pin | `acl_pinned`, plus `WORD_PINNED` / `WORD_FROZEN` | +| link | dictionary chaining | +| code field | literally a function pointer | + +The dictionary is not *analogous* to a Stadium entry. It is one, already built and already +tested. Everything else is what gets generalized toward it. + +**But run §9's admission test on it before moving it in.** Its reap event is the weak +wire. Blocks migrate, messages deliver, VMs die by cooling — a dictionary word does not +expire. Heat decays to a floor and the word stays; `FORGET` is manual and rare. That is +the same shape §9 already flags as **suspect** for screen cells: hundreds of permanently +resident, largely inert entries. It may well be fine, but the dictionary is too central +to wave through, and it is precisely the case §9 exists to catch. + +**Also:** the dictionary is what `parity.c` hashes. Moving its representation into the +Stadium changes that hash, so every committed baseline in `logs/` shifts. Not a blocker — +but a deliberate re-baseline with a before/after record, not something to discover later. + +### 16.4 The engine must stay deterministic — this is a new constraint + +Nothing in §1–15 says this, and it binds the engine tightly. + +`parity.c` logs a dictionary hash per VM birth. The DoE's 0.000% CV across 90 runs and the +patent support material both rest on the same capsule producing the same heat state on +every run. Today that holds for a reason worth naming: ticking is **execution-driven**. +`vm_tick()` (`vm/vm_runtime.c:114`) is called from execution paths, and its own header +says *"Synchronous (now): Called from main execution loop, every N executions."* Same +instruction sequence, same tick points, same decay events, same hash. + +Wall-clock ticking does not have that property. Under TCG, elapsed time varies run to run +on identical input. + +> **The interrupt may supply pacing, but the engine must fire on tick *count*, never on +> elapsed wall time.** + +Same input → same tick ordinal → same reap and inference events → same hash. This keeps +parity intact while still letting compudynamics be genuinely timer-driven. + +There is a second, narrower version of the same discipline. `heartbeat_tick()` measures +inter-tick deltas to derive variance and TIME-TRUST. If the engine's own work ran inside +that handler, the handler's runtime would become part of the interval it measures — the +instrument would be reporting the cost of running the instrument. So the interrupt does +bookkeeping only; the engine runs outside it. The split already exists in the tree and +works: `adaptive_check_accumulator` / `adaptive_pending` (`include/vm.h:113-114`), set at +`rolling_window_of_truth.c:372-375`, serviced at `:1302-1308`. + +**DECIDED** unless argued — it is a constraint inherited from what the system already +claims, not a new preference. + +### 16.5 What this implies about order + +Whatever step one turns out to be, it now has a floor under it: real timer interrupts and +a real IRQ return path on all three ISAs. §10's sequencing (Hermes first, as the proving +ground) sits above that floor, not below it. + +--- + +## 17. Patrons + +An occupant of the Stadium is a **patron**. Blocks, words, ACLs and messages are all +patrons. The word is doing real work: it names the category without implying a class +hierarchy, and it keeps the metaphor honest — patrons attend, they are not the building. + +**DECIDED.** + +### 17.1 Four patrons die four different ways — and that is not a type field + +The observation that prompted this section is correct: these things do not all end the +same way. A message is consumed. An ACL lapses. A block should never be destroyed. A word +should never be destroyed either. + +The reflex is a decision branch on patron kind. That is the type field §3 forbids, and it +is not needed — but neither is the opposite over-simplification, which an earlier draft of +this section made and which is corrected here. + +**Heat and TTL are not the same mechanism, and neither is a special case of the other.** +§3 lists them as separate wires and they must stay separate. A message carries a countdown. +A block does not — a block leaves the floor because it *cooled*, not because a timer +expired. Collapsing the two forces the design, which is precisely the failure §11 warns +about. + +There are three mechanisms, and each patron uses the ones that genuinely apply: + +| Mechanism | Nature | Patrons | Departure | +|---|---|---|---| +| **TTL** | countdown to a definite event | messages, ACLs | expiry | +| **Heat decay** | continuous, gradual | blocks, words | cooling off the floor | +| **Pin** | invariance — §3's wire | any | never | + +Mapped per patron: + +| Patron | Governed by | Reap event | +|---|---|---| +| Message | TTL | delivery — consumed, gone | +| ACL | TTL | expiry | +| Block | heat decay | **migration back to Artemis** — evicted, not destroyed | +| Word | heat decay | cooling off the floor (see §17.3) | + +#### Two measures, one clock + +This does **not** mean two clocks. Both mechanisms advance off the same tick — the +adaptive heartbeat. TTL decrements on a tick; heat decays on a tick. They are two different +*readings* of one counter, not two independent time sources. + +That is not a tidiness preference, it is forced. §16.4 requires the engine to fire on tick +count so that the same input reproduces the same dictionary hash. Two independent clocks +would be two independent sources of nondeterminism and parity would not survive it. + +> **One tick. Two measures. Three mechanisms.** + +The engine still asks nothing about patron kind. It advances the tick, applies whichever +measures a patron carries, and calls the code field when a patron departs. A pinned patron +never departs. There is no type interrogation — see §18 for how the dispatch works without +one. + +### 17.2 Reaping is not destruction + +The block case is the one that makes this work, and §9 already had it right: a block's +reap event **is migration**. §5 puts storage beneath the Stadium, with blocks coming onto +the floor when hot and going back off when cold. + +So a block is reaped in exactly the sense the engine means — it leaves the floor. Where it +goes afterwards is the code field's business, not the engine's. A message's code field +ends in delivery; a block's ends in a write-back to Artemis. Same event, different +behaviour, no special case. + +This is worth stating plainly because "reap" reads as "free" and here it does not: + +> **Reap means leaves the floor. It does not mean destroyed.** + +**DECIDED.** + +### 17.3 Words: the dictionary is the warehouse, hot words are the patrons + +§16.3 left words as the unresolved patron. Pinning all of them resolves nothing — several +hundred permanently resident, largely inert entries is the §9 screen-cell failure with a +different label, and it wastes the bounded capacity that gives K a fixed denominator. + +The better reading applies §5 unchanged. Storage sits beneath the Stadium. The **full +dictionary sits beneath it too**, and only **hot words are on the floor**. + +This is not speculative — it already exists and is already measured: + +- `src/physics_hotwords_cache.c` maintains the hot-word set +- `cache_hits_delta` is column 4 of the DoE CSV, "hot-words cache hits this tick" +- execution heat (Loop #1) is what promotes a word; linear decay (Loop #3) is what cools it + +So the hot-word population is already a live, moving crowd with an existing promotion rule +and an existing cooling rule. It is the crowd. The dictionary is the warehouse it is drawn +from, exactly as Artemis is the warehouse blocks are drawn from. + +#### The existing cache is only half-aligned — and that is the argument for doing this + +Reading `physics_hotwords_cache.c` closely turns up something that strengthens the case +rather than weakening it. **Heat governs admission to the cache. Nothing governs +departure.** + +`hotwords_cache_promote()` (`:362-383`), when full, writes the new word to +`cache[lru_index]` and advances that index modulo the size. That is round-robin. The field +is named `lru_index`, the inline comment at `:365` says "LRU eviction: remove oldest entry +(round-robin)", and the doc block at `:347` says "round-robin least-recently-used" — which +is a contradiction in terms. Nothing anywhere tracks recency of use. Promotion is gated on +`execution_heat > HOTWORDS_EXECUTION_HEAT_THRESHOLD` (`:283`); eviction consults heat not +at all. + +The consequence is that the hottest word in the cache can be evicted purely because its +slot came up in the rotation. + +That is a direct contradiction of §4: + +> *Ranking is read, not decided. There is no scheduler because there is no policy. The +> arena is simply already in heat order when you look at it.* + +Round-robin eviction is exactly a policy — an arbitrary one, uninformed by the physics the +rest of the system runs on. + +**This is the strongest practical argument for §17.3.** Moving words onto the Stadium is +not a relabeling exercise; it repairs a real defect by deleting the arbitrary half of an +existing mechanism. And it is measurable before and after: `stats.evictions`, +`stats.promotions` and `stats.cache_hits` are already instrumented and already flow into +the DoE CSV. + +Consequences if this holds: + +- Words need no pin exception. Their reap event is cooling off the floor — the same shape + as a block's, one level up. +- §16.3's objection dissolves. The dictionary does not move into the Stadium wholesale; + it stays beneath it and pages against it. +- The parity concern in §16.3 narrows considerably. The dictionary's own representation is + not what changes — what becomes a patron is the hot set, which is already transient. +- Pin stops being a general-purpose escape hatch and goes back to meaning what §3 says: + invariance, for the few things that genuinely must not vary. + +**LEANING.** The mechanism is already built and the fit is clean, but this reframes a +direction stated differently earlier the same day, and it deserves longer than a paragraph. + +### 17.4 Open + +1. **What is a word's TTL, concretely?** Heat decay already cools words, but decay-to-cold + and TTL-expiry are not obviously the same clock. Either they unify or §17.3 needs a + second mechanism, which would be a bad sign. +2. ~~**Is the hot-word set bounded today?**~~ **RESOLVED — yes, hard bounded.** + `DictEntry *cache[HOTWORDS_CACHE_SIZE]` (`include/physics_hotwords_cache.h:168`) is a + fixed array inside the struct, with `HOTWORDS_CACHE_SIZE = 32` (`:84`). Nothing is + allocated — `hotwords_cache_cleanup()` notes there is nothing to free, since the cache + holds borrowed pointers the dictionary owns. It is per-VM (`vm->hotwords_cache`, used + at `dictionary_management.c:320`), not global. This is exactly the inescapable outer + wall §2 requires. + + Two things follow. **First, the bound is 32** out of a 453-word Mama dictionary — a + very tight floor. Whether that is the right Stadium population or an artifact of the + structure having been sized as a lookup cache rather than as a live set is a design + input, not a given. **Second**, the eviction defect in §17.3 above. + + *Reported, not fixed:* in `hotwords_cache_promote()`, if `word` is NULL **and** the + cache is full, the guard at `:363` falls into the inner branch at `:364` and writes + NULL into `cache[lru_index]`. Unreachable today — every caller passes a non-NULL entry + from the bucket search — but the NULL check reads as though it prevents this, and does + not. +3. **ACL reap** — §9 still marks this `?`. ACL entries carry `acl_ttl` in `DictEntry` + already, so this is likely the easiest of the four to close, and it should be closed on + paper alongside the others rather than left dangling. +4. Does a patron ever change what it is? A block that is written becomes a new block by + content-addressing. A word that is redefined is a new word. If nothing mutates in place, + that is worth stating explicitly — it removes a whole class of proof obligation in §13. + +### 17.5 The framebuffer is not a patron — it is a utility + +**DECIDED.** This is §5 and §2 applied rather than a new call, but it was close enough to +becoming an exception that it is worth writing down explicitly. + +#### Outside the Stadium is not the same as an exception + +§11's warning is about a *patron kind that needs special handling inside the engine* — you +end up carrying the general machinery and the carve-out, and every future reader has to +learn both. That is the thing to fear, and the fear is correct. + +But §5 is not a carve-out. It is a taxonomy. The test for whether something is an +exception is: **does the engine change because this thing exists?** For the framebuffer, +nothing changes. The engine never learns about it. That is a boundary, not an exception. + +#### It fails §2's liveness test by definition, not by fiat + +§2's scoping decision is the sharpest line in this document: *the Stadium holds what is +live, not everything that exists.* A patron arrives and departs. The framebuffer does +neither — it is there from init to power-off. It has no arrival event and no reap event, +not because it has been excused from having them, but because it genuinely has none. + +#### Better than "the building's lighting": a utility + +§5 calls the framebuffer the building's lighting, which undersells it — that reads like +part of the structure. It is closer to **the power company**: external infrastructure the +building consumes. Not the Stadium. Not the basement of the Stadium. A third thing. + +That gives three categories, all principled, none of them exceptions: + +| Category | Relation | Example | +|---|---|---| +| Warehouse | beneath | Artemis, the dictionary (§17.3) | +| Stadium | the floor | patrons | +| Utility | beside | framebuffer, and devices generally | + +#### What is live is the dirty event — and it is not a fifth patron kind + +Run §9's two questions on it: + +- **Heat means** — a region written often is hot. A scrolling log, a blinking cursor. A + static border is cold. Traffic confers heat, identically to everything else. +- **Reap is** — redraw. Consumed by being painted. + +Consumed on delivery, carries a TTL, dies on arrival. **A dirty event is a message whose +recipient happens to be the framebuffer.** It does not extend the patron taxonomy; it is +the message patron with a different destination. + +Which yields a symmetry worth keeping: + +| Patron | Code field terminates at | Which lives | +|---|---|---| +| Block | Artemis | beneath | +| Dirty event | framebuffer | beside | + +Both are code fields finishing outside the Stadium. Neither is special. + +**This closes the last `?` in §9.** The screen-cell row resolves to: the event is the +patron, the grid is not. + +#### The sizing argument, independently + +A framebuffer is several megabytes of fixed device memory. Making it a patron means either +blowing the bounded capacity that gives K a fixed denominator (§2), or forcing the +by-reference payload path to exist for exactly one pathological object — which would decide +§12 Q1's payload threshold on the worst possible case. Sizing a design around its single +largest outlier is how the header ends up wrong for the other ten thousand entries. + +#### Not a patron does not mean no physics + +Worth stating so it is not lost: excluding the framebuffer from the Stadium says nothing +about whether compudynamic concepts apply *within* it. A utility can have its own internal +dynamics — heat over regions, decay, adaptive refresh — without being a Stadium +participant. The power company has physics too. + +**OPEN, deferred.** What those dynamics are is a question for when the framebuffer work +actually happens. It does not gate the Stadium, and it should not be designed speculatively +now. + +### 17.6 Sizing and allocation — the Stadium should be dynamic, but not heap-allocated + +§3 says the Stadium stays an array with index links. That is right, but it is stated in a +way that invites the wrong objection, because **"array" and "fixed at compile time" are +not the same thing** — and it is the second one that is genuinely objectionable. + +A hardcoded capacity is arbitrary: `HOTWORDS_CACHE_SIZE = 32` is a number someone picked, +and §17.4 shows exactly how that ages. A contiguous block of fixed-size cells, sized at +boot from the memory budget and addressed by index, is dynamic in every sense that matters +operationally while remaining an array in every sense §3 and §13 depend on. + +Four positions, with what each costs: + +| | What it is | Cost | +|---|---|---| +| a | Capacity fixed at compile time | Arbitrary bound. What the hot-words cache does today. | +| **b** | **Sized at boot, contiguous, index-linked** | **None. Retains every property below.** | +| c | Contiguous but resizable at runtime | K's denominator moves; couples to §7 | +| d | Per-entry allocation, pointer links | Forfeits §13 | + +#### Why (b) is free + +The Stadium is established before any VM exists (§6), so boot is already the moment its +capacity is determined. Deriving that capacity from available memory rather than from a +constant costs nothing and gives up nothing. Cells stay uniform, links stay indices, the +region stays contiguous. + +**LEANING toward (b).** + +#### Why (d) is expensive — by this document's own argument + +§13 is unambiguous: + +> *No pointers. Fixed-size cells with index links means the arena models as a total +> function over a finite index set — no heap model, no separation logic, no aliasing, no +> null. **This is the single biggest difference between a tractable proof effort and a +> research project.*** + +Per-entry heap allocation gives that up and takes several things with it: + +- **The finite state space.** Bounded capacity is what makes induction over the Stadium + straightforward and what puts model checking on the table alongside theorem proving. +- **§2's hard outer wall.** Without an inescapable bound, K is bookkeeping rather than a + conservation law — §2 says this in as many words. +- **The engine's simplicity.** This is a freestanding kernel with `kmalloc.c` / `pmm.c` + and no libc. Allocation in the reap path means the engine can fail to allocate, which + means the engine needs a failure mode, which means it is no longer the thing §3 + describes. An engine that can fail is a different engine. + +Fragmentation is the least of it, though §3 is right that indices avoid that too. + +#### Why (c) is the genuinely open one + +A contiguous region that grows and shrinks *as a whole* keeps index links and keeps the +proof structure — the capacity becomes a parameter rather than a constant, which HOL +handles without difficulty. What it complicates is K, since the denominator moves. + +This is not a new question. §7 already has it open for per-VM shares: *"whether a VM's +share is a hard bound or an elastic one that can grow and shrink under pressure, with +capacity transferring between VMs as a conserved operation Hera arbitrates."* Elasticity at +the Stadium level and elasticity at the per-VM level are the same question asked at two +scales, and they should be answered together rather than separately. + +**OPEN**, and coupled to §7 and to §12 Q6 (one Stadium or nested per VM). Note that if Q6 +resolves to nested-per-VM, (c) becomes considerably more attractive — capacity transfer +between VMs is the whole point of that arrangement, and a fixed per-VM bound would waste it. + +#### The rule this reduces to + +> **Dynamic in capacity. Static in structure.** + +Decide how big the Stadium is at runtime. Do not decide what an entry is, or how entries +are addressed, at runtime. + +--- + +## 18. The engine — L0 + +The engine that holds the patrons is a loop like the others, and it needs a name in the +same scheme. L1–L7 are taken by the existing feedback loops; L8 is the Jacquard mode +selector. The engine sits **beneath** all of them, so: **L0**. + +### 18.1 L0 and L8 bookend the gated loops + +This produces a structure worth drawing, because it explains why two of the ten are +different in kind: + +``` + L8 Jacquard mode selector always on, ungated + ───────────────────────────────────────────────────── + L1 … L7 feedback loops gated by L8 + ───────────────────────────────────────────────────── + L0 the Stadium engine always on, ungated +``` + +L1–L7 are gated: L8 switches them on and off, 128 configurations over seven bits. + +The two bookends are ungated, and for symmetric reasons: + +- **L8 cannot be gated** because something has to decide the gates. A selector that could + deselect itself has no defined behaviour. +- **L0 cannot be gated** because it is what holds the patrons the other loops operate on. + Switch it off and nothing is reaped, the Stadium fills and stays full, and K stops being + conserved. That is not a mode, it is a failure state. + +This is the same argument §6 makes about boot order. The thing that manages existence +cannot be a participant in what it manages — not for VMs, and not for loops. + +**DECIDED.** + +### 18.2 The Jacquard accounting is an exclusion, not an extension + +The obvious reading of "add L0" is that the selector grows a bit: 7 bits becomes 8, +128 configurations become 256. + +**That is the wrong move, and §18.1 is why.** L0 is not gateable, so it has no bit. The +gate word stays seven bits wide and the selector stays at 128 states. + +This is worth stating explicitly because the alternative is expensive: widening the gate +word would invalidate the 128-configuration L8 table, the DoE campaign already run against +it, and the existing results. There is no reason to pay that, and the design does not ask +us to. + +> **L0 is accounted for in Jacquard by being deliberately absent from it.** + +**DECIDED.** + +### 18.3 Dispatch: enumerate behaviours, not kinds + +§13 already requires a closed enumeration: + +> *The set of code-field behaviours must be a closed enumeration, fixed at build time… +> Model it as a datatype of behaviour tags plus a dispatch function and the whole thing +> stays first-order and tractable.* + +So a fixed enum with fixed dispatch is mandatory, not a concession to practicality. But +there are two things one could enumerate, and only one of them preserves §3: + +| | Enumerate | Engine asks | Cost of a fifth patron | +|---|---|---|---| +| ✗ | patron **kinds** — `BLOCK`, `WORD`, `ACL`, `MESSAGE` | "what are you?" | touch the engine | +| ✓ | **behaviours** — `MIGRATE`, `DELIVER`, `EXPIRE`, `COOL` | nothing; calls `dispatch(tag)` | none | + +Both are closed, both are fixed at build time, both are equally provable. Only the second +keeps the engine ignorant of its contents, which is the property §3 exists to protect. Two +patrons may share a tag; a new patron that migrates costs zero engine changes. + +The branching Captain Bob is right to want is real and it is allowed — it lives in the +dispatch function over a closed tag set, not in the engine asking patrons what they are. + +**DECIDED.** + +### 18.4 One tick + +L0 advances on the adaptive heartbeat. Everything derived from time is derived from that +one counter: + +- TTL decrements per tick (messages, ACLs) +- Heat decays per tick (blocks, words) + +Two measures, one clock — see §17.1. §16.4 forces this: the engine must fire on tick count +for the same input to reproduce the same dictionary hash, and two independent time sources +would be two independent sources of drift. + +### 18.5 CLOSED — the adaptive rate does not break determinism, and here is why + +The concern: the heartbeat is *adaptive* — faster, slower, window wider, narrower. If it +adapts off **timing measurements**, the adaptation is machine-dependent and §16.4 fails. +If it adapts off **execution-derived state**, tick ordinals still map deterministically to +work and parity survives. + +Traced end to end on 2026-08-03. **The dictionary-parity chain is clean.** Resolution (1) +— adaptation inputs are execution-derived, TIME-TRUST stays diagnostic — is already the +de-facto design. + +Evidence, in the order it decides the question: + +1. **TIME-TRUST is computed and never consumed.** `heartbeat_trust()` has **zero callers** + in the entire tree. `m5_time_trust` and `m5_variance` (`include/vm.h:315-316`) are + declared and never read or written. The only consumer of `ts->trust` is + `starkernel/doe_log.c:98`, which writes it to a CSV column. It is measured and + reported, never fed back. + +2. **The intent is already documented.** `include/starkernel/timer.h:70` — + *"TIME-TRUST thresholds in Q48.16 (for diagnostics, NOT for gating)."* + +3. **Every inference-engine input is execution-derived.** `vm_runtime.c:626-640` populates + `InferenceInputs` from: the rolling window, `trajectory_length` (from `window_pos` / + `total_executions`), `prefetch_hits` / `prefetch_attempts`, `hot_word_count`, + `stale_word_count`, `total_heat`, `word_count`, and the previous check's baselines. + **No timing input of any kind.** The outputs it applies — `adaptive_window_width` and + `adaptive_decay_slope` — therefore depend only on execution history. + +4. **Decay is tick-based, and deliberately so.** `vm_tick_apply_background_decay()` is + handed `vm_monotonic_ns(vm)` but computes + `elapsed_ticks = tick_count - last_decay_tick` (`vm_runtime.c:375`). The `now_ns` + argument only writes `last_decay_ns`. The comment at `:373-374` says so explicitly: + *"Tick-based, not wall-clock… now_ns is kept only to refresh last_decay_ns for + diagnostics."* Someone already defended this exact boundary. + +5. **The parity hash contains nothing time-derived.** `capsule_dict_hash_hook()` + (`capsule/capsule_vm_hooks.c:60-70`) walks the dictionary hashing exactly two things + per entry: **the word name and `execution_heat`**. Not `last_decay_ns`, not any + timestamp. So even the diagnostic wall-clock field from (4) cannot reach the hash. + +**Conclusion: §16.4 holds today, and holds by construction rather than by luck.** + +#### One real exception, and it is not in the parity path + +`vm_physics_touch()` (`capsule/capsule_vm_physics.c:250-313`) **is** wall-clock dependent: +it computes `elapsed_us = (now_ns - last_active_ns) / 1000` (`:272`) and the header comment +at `:122` confirms the transfer amount scales with elapsed time. So **fleet-level VM heat +is not reproducible run to run** the way dictionary heat is. + +Scope of that, precisely: + +- It touches `node->physics` in the VM registry, **not** `DictEntry.execution_heat`, so it + does not reach the parity hash and does not invalidate the existing claim. +- `vm_physics_tick()` (`:366`) explicitly discards its `now_ns` argument (`(void)now_ns;`), + so only the touch path is affected. +- With Hera alone this is nearly inert. It becomes live again when Hermes and Artemis + return. + +This is a **pre-existing condition, not something the Stadium introduces.** But it is +exactly the pattern L0 must not inherit, and it is worth knowing that fleet K figures and +dictionary parity have different reproducibility guarantees today. + +#### The invariant this should become + +Determinism currently survives on convention plus one good comment. That is too thin for +something load-bearing. L0 should make it explicit: + +> **Anything that influences patron state advances on tick count. Wall-clock time may be +> recorded for diagnostics and must never be an input to a decision.** + +**DECIDED**, and it supersedes the "leaning (1)" in the earlier draft of this section.