LithosAnanake/FABRIC.md

# FABRIC.md — the Stadium

**Status:** Living working document. Started 3 August 2026 and appended to as work proceeds.
Sections are marked **DECIDED**, **LEANING**, or **OPEN** so they can be argued with rather
than inherited.

**How to read it.** §1–15 are the original design argument, written before any code was
examined. §16 onward are findings and decisions made against the actual tree, in the order
they happened. **Where the two disagree, the later section wins** — earlier text is left
standing, with a pointer, because §19.4 and §19.5 quote it directly and because retracing
the reasoning matters more than a tidy read.

**On the name.** The thing described here is the **Stadium**. "The arena" was the working
name until it collided with `src/starkernel/vm/arena.c` — the PMM-backed VM page allocator,
an unrelated structure. The document has been swept; "arena" now survives only inside block
quotes that reproduce an earlier section verbatim, and in §12's preserved question list,
which several sections quote.

**§25 is the punch list.** It is the authoritative statement of what is done and what is
not. Read its instructions before doing any work against this document.

---

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

> **Updated by §20 and §17.5.** There are five patron kinds, not four — VMs are the fifth
> and were already implemented (§20.1). And the Console's patron is the dirty *event*, not
> the cell (§17.5); "Console heats dirty cells" above is the reading that §9 flagged as
> suspect and §17.5 resolved.

---

## 2. The Stadium

A single region of memory, outside any VM, holding everything currently **live**.

- Bounded capacity. The bound is real and inescapable.
- Allocated at boot, before any VM exists.
- Not part of the heap.

> **Corrected after §19.1.** This bullet originally read *"the bound is what gives K≡1.0 a
> fixed denominator. Without a hard outer wall, K is bookkeeping rather than a conservation
> law."* That justification does not survive the definition of K.
>
> §19.1 establishes K as a conserved, normalised **heat share** summing to 1.0. Its
> denominator is 1.0 by definition; capacity does not enter it, and §19.2 says outright that
> mass never enters K. A transfer-based sum is equally conserved at three patrons or three
> hundred — population is not what makes the check meaningful.
>
> The bound is still necessary, for two reasons this section can honestly claim:
>
> - **Finite state (§13).** A bounded population is what makes induction over the Stadium
>   straightforward and puts model checking alongside theorem proving. This is the larger
>   payoff and it does depend on the wall.
> - **Density needs a volume.** §19.2 defines density as heat ÷ mass, and mass is cells
>   occupied. Without a fixed capacity there is nothing for a patron to be dense *within*,
>   and §19.3's admission rule — admit if denser than the least dense resident — has no
>   meaning because nothing is ever full.
>
> What makes conservation falsifiable is the *mechanism*, not the bound: heat that is
> **transferred** can drift and be caught; heat that is **renormalised** cannot. See §20.2.

The critical scoping decision, and the one that keeps this from sprawling:

> **The Stadium 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 — **never a content hash while resident** (§24.4) |
| heat | conserved share of 1.0, moved by traffic (§19.1) |
| TTL | remaining lifetime — messages and ACLs only (§17.1) |
| pin | invariance flag (opposite of TTL, not an extension of it) |
| link | index into the Stadium, not a pointer |
| code field | behaviour tag from a closed enumeration (§18.3) |
| **mass** | **cells this patron occupies — its footprint (§19.2)** |
| payload | carried in the patron's own cells; large patrons are simply heavy (§23.1) |

Fixed-size cells. Links are indices, so the Stadium stays an array — no fragmentation,
and tractable for Isabelle later.

#### A cell is one of exactly two things

The wire table above describes a **patron header**. §23.1 establishes that a large patron is
not held by reference but simply occupies more cells — a 1024-byte block is 17 cells, one
header and sixteen of payload. Those sixteen carry no identity, no heat, no TTL and no code
field.

That is a second cell shape, and this section's opening line — *"One structure. No variants"*
— forbade it without saying so. Declared properly:

> **A cell is either a patron header or a continuation cell owned by exactly one patron.
> The union is closed, two-valued, and fixed at build time.**

This introduces no new principle. It is the same discipline §18.3 applies to behaviours: a
closed enumeration fixed at build time is as tractable in HOL as a single record, and a
two-valued union is the smallest possible instance of one. §13's "one datatype" remains true
in substance — the datatype is now a two-constructor sum rather than a single record, which
costs a case split and nothing else.

What it is **not** is a type field. The engine does not ask a header what kind of patron it
is; the two-valued distinction is structural, tells the engine only whether a cell begins a
patron or continues one, and is exhausted by that. A continuation cell is never ranked,
never reaped and never dispatched — it is floor space, accounted for in its owner's mass.

> **Amended by §19.2 and §23.1.** `mass` is an eighth wire, added when density was
> defined — density is heat ÷ mass, so mass has to live in the entry. And the original
> payload rule ("inline if small, by reference if large") was dissolved rather than
> answered: a large patron occupies more cells, which is what mass already measures.
> By-reference is reserved for things outside the Stadium, which are not patrons.

**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**, including the payload question — dissolved in §23.1.

---

## 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 Stadium 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.

**DECIDED as amended by §19.** The density formulation this section called for is supplied
there. Three specific amendments, and the original wording above is left intact because
§19.4 and §19.5 quote it:

- **"Density generates heat" is backwards** (§19.5). Traffic confers heat; density is
  heat ÷ mass, derived downstream. One word was carrying two meanings.
- **The third bullet is struck, not repaired** (§19.4). "A crowded entry is harder to
  reach" does not translate — a hot entry is *easier* to reach, which is what a cache is
  for. The conclusion survives via the second bullet: heat is zero-sum, so popularity is
  self-limiting by conservation.
- **The first bullet is now true rather than aspirational.** Ranking reads density, which
  §19.2 makes a number.

The line about TTL and pinning is correct but incomplete — §17.1 shows there are three
departure mechanisms, not two: TTL, heat decay, and pin.

---

## 5. What is *not* in the Stadium

This section exists because forcing everything in is how this design turns into a mess.

- **Storage is beneath the Stadium.** 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 a Stadium occupant; it becomes what the Stadium pages against.
- **Devices are beside the Stadium.** The framebuffer is the building's lighting, not an
  occupant. Console's dirty *events* are Stadium entries; the pixels are not.

**DECIDED**, and completed by §17.5, which supplies the third edge this section counted but
did not list, and sharpens the second:

| Category | Relation | Example |
|---|---|---|
| Warehouse | beneath | Artemis, and the dictionary (§17.3) |
| Stadium | the floor | patrons |
| Utility | beside | framebuffer, and devices generally |

"The building's lighting" undersells the framebuffer — it reads as part of the structure.
§17.5 calls it **the power company**: external infrastructure the building consumes. Not
the Stadium, not the basement of the Stadium, a third thing.

---

## 6. Boot order

The engine cannot be a VM service, because VMs live inside the thing it manages.

1. LithosAnanke establishes the Stadium 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.

**DECIDED.** The order was right, and the allocation mechanism this section left unspecified
is now given: one global array of fixed-size cells, sized at boot from the memory budget,
addressed by index (§17.6b, §22.3). Step 1 above allocates that array before any VM exists;
step 2 makes Hera the first patron in it (§20).

---

## 7. Hera

Hera's job becomes Stadium distribution. This is not a new responsibility — allocating a
VM's share *is* birthing it, and lifecycle is already what Hera is for.

~~**OPEN:**~~ **RESOLVED in §22 — elastic.** 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.

§22 takes the elastic option. §19's density definition turns it into a negative feedback
loop that runs itself — capacity flows down the density gradient — so it costs less than
this section anticipated. The layout that makes it cheap is a single global cell pool with
per-VM quotas held as counts (§22.3), and capacity must move on a slower loop than heat
(§22.4).

---

## 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*.

> **OPEN — the one thing in this section the design has not addressed.** *"Occasionally one
> sits in a car, which is the only exclusive thing in the room, scoped to a single object,
> no global lock."* That sentence asserts an exclusivity primitive: per-patron, not global.
> Nothing in §16–24 defines it. §21 addresses ISR-versus-mainline concurrency, which is a
> different question.
>
> It matters because a patron reaped while someone is "sitting in" it is a use-after-free
> under another name, and §22.3 gave up physical fault containment, which raises the stakes
> rather than lowering them. Tracked as a punch-list item in §25.

---

## 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?**

**COMPLETE.** Run against every candidate; all five patron kinds pass, and the two `?` marks
are closed:

| Type | Heat means | Governed by | Reap is | Verdict |
|---|---|---|---|---|
| Block | accessed often | heat decay | migration back to Artemis | passes |
| Message | delivery urgency | TTL | delivery | passes |
| VM | runs often | heat decay | death by cooling | passes (§20) |
| Word | executed often | heat decay | cooling off the floor | passes (§17.3) |
| ACL | checked often | TTL | **expiry** (§17.1) | passes |
| ~~Screen cell~~ | — | — | — | **not a patron** (§17.5) |

Screen cells were the suspect case and the suspicion was correct. A cell never expires — it
is a fixed grid position always present, so cells-as-entries would leave most of the Stadium
inert and permanently pinned. §17.5 confirms the reading anticipated here: **the patron is
the dirty event, not the cell.** The grid stays outside, and the event turns out to be a
message with a different destination rather than a sixth kind.

Words were added to the table by §17.3 — the original list omitted them because §1 treated
the dictionary as the *reference implementation* rather than as a population of patrons.

Ten minutes on paper. It confirmed the design and caught one case, which is what it was for.

---

## 10. Sequencing

**FABRIC.md first, then Hermes native on the fabric, then measure, then Console, then
Artemis last.**

> **Amended by §16.5 and §21.2.** This ordering is still right for the *subsystems*, but it
> is not the first work. A substrate floor sits beneath all of it: Hera alone, real timer
> interrupts and a real IRQ return path on all three ISAs (§16.1), and compudynamics driven
> from that tick. None of the sequencing below can begin until that exists, because the
> engine has nothing to run on. §25 carries the actual order.

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 — five closed, one partial

**Status as of §24.** Five of the six are answered or dissolved; Q5 is partial. The original
text is kept below because several later sections quote it.

| | Question | Outcome | Where |
|---|---|---|---|
| Q1 | Payload threshold | **dissolved** — large patrons are simply heavy | §23.1 |
| Q2 | Entry header size | **sized** — 64-byte cell, ~32-byte header (constants to validate) | §23.3 |
| Q3 | Screen cell or dirty event | **event**; the grid is not a patron | §17.5 |
| Q4 | Per-VM share hard or elastic | **elastic**, via quota over one pool | §22 |
| Q5 | Loop coupling / timescales | **partly** — capacity must move slower than heat | §22.4 |
| Q6 | One region or nested per VM | **nested**, two levels | §21 |

Q5 is marked *partly* deliberately: §22.4 fixes the one ordering that matters (capacity
slower than heat) but the full eight-loop interference analysis has not been done, and
§16.1 notes it cannot be until a real time base exists on all three ISAs.

---

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 Stadium entry is a single record. Everything else is payload. You
  reason about `entry` once rather than about blocks, messages, VMs and events separately.
  *(Amended by §3: a cell is a two-constructor sum — patron header or continuation cell —
  not a bare record. That costs one case split and nothing else; the point stands.)*
- **No pointers.** Fixed-size cells with index links means the Stadium 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
  Stadium 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 Stadium 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 Stadium, 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 Stadium holds the live crowd. Storage is the warehouse. Devices are the utility.
- One entry shape. The code field is the only difference between kinds.
- Traffic confers heat. Heat is conserved at 1.0. Density is heat per cell. Ranking reads
  density.
- Departure is TTL, or cooling, or never. Pinning is invariance, not longevity.
- The kernel opens the hall. Hera walks in first, and cannot be asked to leave.

*(Amended from the original five by §17.5, §19.5, §17.1 and §20.5 #3. The earlier third
line — "heat is density, conferred by traffic" — conflated two quantities; the earlier
fourth — "departure is unconditional" — knew only one mechanism.)*

---

## 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. The
document has since been swept to the new name, and §1–15's *substance* reconciled against
§16–24 with each superseded claim marked in place.

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 — but not
as strong as an earlier draft of this subsection claimed. Read against `DictEntry`
(`include/vm.h:335-351`):

| §3 wire | In `DictEntry` | Form |
|---|---|---|
| identity | `word_id` + `name[]` | correct |
| heat | `execution_heat` + `physics` | correct |
| TTL | `acl_ttl` | correct |
| pin | `acl_pinned`, plus `WORD_PINNED` / `WORD_FROZEN` | correct |
| link | `struct DictEntry *link` | **a pointer, not an index** |
| code field | `word_func_t func` | **a raw function pointer, not an enumerated tag** |
| mass | — | absent |
| payload | — (definition body lives outside the entry) | absent |

**Four wires present in correct form, two present in the wrong form, two absent.** An
earlier draft said "six of eight" and named the missing two as mass and a behaviour tag,
which double-counted the code field and omitted payload.

The wrong-form pair is the interesting part. `link` being a pointer is precisely what §13
identifies as *"the single biggest difference between a tractable proof effort and a research
project,"* and the raw function pointer is what §18.3 requires to become a closed tag.

So the honest claim is weaker than "the dictionary *is* a Stadium entry" and still strong
enough to carry §1: **the dictionary already has the concepts, and two of the eight need to
change form.** Everything else is what gets generalised 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.

#### Corrected by the GAP-A1 ruling — the tick is virtual

The rule above ("fire on tick count, never on elapsed wall time") was necessary but not
sufficient, and its inference — *same tick ordinal → same hash* — was unsound. The hash
covers `execution_heat`, which is co-written by **two streams**: word executions and engine
ticks. A hardware timer makes the *interleaving* of those streams wall-clock-dependent
under TCG, so same-per-tick actions do not compose into the same hash. See §25.7.1 GAP-A1
for the full argument.

**RULED 2026-08-03:**

> **The engine's tick is a virtual tick — a pure, deterministic function of the execution
> stream.** This is what exists today (`vm_tick()` paced every N executions) and it is why
> parity holds today. The hardware heartbeat is the TIME-TRUST instrument, the idle wake
> source, and the driver of **nothing that feeds patron state.** When the system is idle,
> the REPL poll loop pumps virtual ticks so TTLs still expire in real time — a context in
> which parity was never claimed.

Phase 0's timer bring-up remains fully justified: it makes the instrument real on three
ISAs instead of one, and it is the substrate SMP will eventually need. What it does not do
is drive the engine.

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, messages **and VMs** 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.

VMs were omitted when this section was written and added by §20, which found they were
already implemented as the outer level. **Five kinds, not four** — the counts elsewhere in
§17 predate that and should be read accordingly.

**DECIDED.**

### 17.1 Patrons die several 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) |
| VM | heat decay | death by cooling (see §20); Hera is pinned (§20.5 #3) |

#### Two measures, one clock

This does **not** mean two clocks. Both mechanisms advance off the same tick — **the
virtual tick of §16.4 as ruled**, a deterministic function of the execution stream, not the
hardware 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 — twice over. §16.4 requires the engine to
fire deterministically so the same input reproduces the same dictionary hash. And the
mechanisms cannot be split across clocks: TTL expiry has side effects on the instruction
stream (a message expiring versus delivered changes what runs next), so a wall-clock TTL
would corrupt heat downstream even if heat itself stayed execution-paced. One virtual
clock for everything that touches patron state; the hardware heartbeat observes and wakes,
never drives.

> **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 density needs as its volume
(§19.2; this sentence originally cited the K-denominator justification that §2's
correction removed — D1).

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
> Stadium 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?**~~ **DISSOLVED — a word has no TTL.** The premise
   was wrong. §17.1 (as corrected) establishes TTL and heat decay as two distinct
   mechanisms, not one clock read two ways: words are governed by **heat decay**, and only
   messages and ACLs carry a TTL. Nothing needed unifying and no second mechanism was
   required.
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**~~ **RESOLVED — TTL expiry.** ACL entries already carry `acl_ttl` in
   `DictEntry`, so they fall under the TTL mechanism in §17.1 alongside messages. §9's `?`
   is closed.
4. ~~Does a patron ever change what it is?~~ **RESOLVED in §24 — and the question was
   slightly wrong.** Full immutability is not available: FORTH blocks mutate in place by
   definition (`BLOCK` / `UPDATE` / `FLUSH`), while words already behave the opposite way,
   redefinition creating a new entry. The kinds genuinely disagree.

   What actually mattered was never payload but **mass and identity**. §24.2 states the
   invariant: identity never changes during a residency; mass never changes as a side effect
   of use; header fields mutate freely; payload contents may mutate provided size and
   identity do not. That gives §13 the enumerable mass function it needed without demanding
   immutability nothing could deliver.

### 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 new patron kind

*(Written when the taxonomy had four kinds; §20 has since added VMs as the fifth. The point
stands unchanged — the dirty event adds nothing to the taxonomy at all.)*

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
swamping the bounded capacity (§2) — as mass, it would dwarf every other patron and make
density comparisons meaningless — or forcing a by-reference payload path to exist for
exactly one pathological object, which §23.1 has since abolished for patrons entirely.
Sizing a design around its single largest outlier is how the header ends up wrong for the
other ten thousand entries. *(This paragraph originally leaned on the K-denominator
justification removed from §2 and on the pre-§23.1 payload framing; the conclusion is
unchanged — D1.)*

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

**SUPERSEDED by §22.3 — the answer is (b) with a refinement.** The Stadium is one global
array of cells sized at boot, and per-VM shares are **quotas held as counts** rather than
separate regions. That keeps (b)'s properties while making (c)'s elasticity trivial, so the
two are no longer alternatives.

#### Why (d) is expensive — by this document's own argument

§13 is unambiguous:

> *No pointers. Fixed-size cells with index links means the Stadium 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.** The bound is what gives density a volume to be dense within
  (§19.2) and §13 its finite index set. *(This bullet originally read "Without an
  inescapable bound, K is bookkeeping — §2 says this in as many words"; §2 no longer says
  that, and §20.2 established conservation is falsifiable regardless of the bound — D1.)*
- **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**~~ **RESOLVED — and the prediction here was right.** Q6 did resolve to nested
(§21), and (c) did become the attractive option (§22). But §22.3 found a cheaper route to
it than resizing a contiguous region: with quotas held as counts over one shared cell pool,
elasticity costs arithmetic on two integers and the denominator never moves at the level
that matters. The total stays fixed; only the partition shifts.

#### 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 new patron kind |
|---|---|---|---|
| ✗ | patron **kinds** — `BLOCK`, `WORD`, `ACL`, `MESSAGE`, `VM` | "what are you?" | touch the engine |
| ✓ | **behaviours** — `MIGRATE`, `DELIVER`, `EXPIRE`, `COOL` | nothing; calls `dispatch(tag)` | none |

This was not hypothetical. VMs were added as a patron kind by §20 *after* this section was
written, and cost the engine nothing — a VM's behaviour tag is `COOL`, the same tag a word
carries. Under the rejected column it would have been an engine change.

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 virtual tick** — a deterministic function of the execution stream, per
the §16.4 ruling. 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 as ruled forces this: patron state must advance
deterministically for the same input to reproduce the same dictionary hash, and the
hardware heartbeat cannot supply that, because its interleaving with the instruction
stream is wall-clock-dependent. The heartbeat's roles are the TIME-TRUST instrument and
the idle wake source; when the system idles, the REPL poll loop pumps the virtual tick.

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

---

## 19. Mass, density, and what K actually is

§4 is marked LEANING with the note that *"the density formulation needs a concrete
definition."* This section supplies it. It is the keystone: §4 claims ranking is **read**
rather than decided, and that claim is empty until the thing being read is a number.

The objection that forced this section is the right one. Density is *quantity per unit
volume*, so it implies a mass and a volume. Neither had been named.

### 19.1 K is already defined, and it is not an occupancy ratio

This has to come first, because the obvious definition of K contradicts working code.

`vm_physics_conserved()` (`capsule/capsule_vm_physics.c:456-461`) sums
`execution_heat_q48` across live VMs and tests that total against `Q48_ONE`:

```c
uint64_t sum  = vm_physics_fleet_heat_sum();
uint64_t diff = (sum > Q48_ONE) ? (sum - Q48_ONE) : (Q48_ONE - sum);
return diff < VM_PHYSICS_EPSILON_Q48;
```

So:

> **K is a conserved, normalised heat *share*. Total heat is always 1.0. Traffic transfers
> heat to a patron from the others; it does not create it.**

K is **not** occupancy, and defining it as `Σmass / capacity` would contradict an
implemented, tested mechanism. It stays exactly as it is.

### 19.2 Three quantities, not one

| Quantity | What it is | Range | Status |
|---|---|---|---|
| **Heat** | conserved share, moved by traffic | Σ = 1.0 always | already implemented |
| **Mass** | cells the patron occupies — its footprint | integer ≥ 1 | new |
| **Density** | **heat ÷ mass** — heat per cell | derived | new |

Heat is the conserved quantity. Mass is an independent axis and never enters K. Density is
the ratio, and it is density in the literal sense at last: quantity per unit volume, where
the volume is a patron's own footprint inside the bounded capacity §2 requires.

A patron holding a large share of the fleet's heat in a single cell is dense. A patron
squatting on four cells with a negligible share is sparse, and belongs back in the
warehouse.

**DECIDED.**

### 19.3 Everything else reads off it

The point of §4 is that no policy exists. With density defined, none is needed:

- **Ranking** — order by density. Read, not computed by a scheduler. §4's first bullet is
  now true rather than aspirational.
- **Admission when full** — admit the newcomer if it is denser than the least dense
  resident, and evict that one. This is a comparison of two intrinsic numbers, not a
  policy, and it closes the "what happens when the Stadium is full" gap.
- **Hysteresis** — falls out unpaid-for. A heavy patron needs a proportionally larger heat
  share to hold its floor space, so a block sitting near the threshold does not oscillate
  on and off. No damping constant to pick, which is what §4 wanted and could not previously
  deliver.
- **Migration cost is not a separate quantity.** An earlier draft of this reasoning treated
  cost-to-move as its own axis. It is not needed: footprint and cost correlate, because a
  patron is expensive to move precisely because it is large. Deriving cost from mass avoids
  introducing a second tunable, which §11 would rightly call speculative generality.

### 19.4 Correction to §4 — the self-limiting claim has the wrong mechanism

§4's third bullet states:

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

**The conclusion is right and the mechanism is wrong.** In a hall, a crowd physically
blocks access to the car. In a computer the inverse is true — a hot entry is *easier* to
reach, since that is the entire purpose of a cache. The metaphor does not survive
translation, and no mechanism in this design reproduces the blocking effect because the
effect is not real in this substrate.

The real governor is **conservation**. Heat is zero-sum: total heat is 1.0, so a patron
heating up necessarily cools every other patron, and nothing can exceed the ceiling.
Popularity is self-limiting because there is a fixed amount of popularity to go around.

This is §4's *second* bullet — *"K constrains the total, so ordering is forced by
conservation rather than by tuned parameters"* — which was the correct answer already. The
third bullet should be struck, not repaired. Designing a mechanism to make the crowd
metaphor come true would be fitting the system to the analogy, which §14 already warns
against in the other direction.

**DECIDED.** §4's third bullet is superseded by this section.

### 19.5 Correction to §4 — "density generates heat" reverses the causality

§4 says *"Density generates heat; nobody computes it."* Under §19.2 that is backwards, and
the confusion is that one word was carrying two meanings:

- **Traffic** generates heat — activity concentrated on a patron transfers heat share to
  it. §4's causality is correct with this word substituted.
- **Density** is heat per cell — *derived* from heat, downstream of it, and it is the
  quantity that gets read when ranking.

The corrected statement:

> **Traffic confers heat. Heat is conserved at 1.0. Density is heat per cell. Ranking reads
> density.**

Nobody decides what matters at any step in that chain. §4's spirit is intact; only the
noun was overloaded.

### 19.6 Open

1. ~~**What is mass, exactly, for each patron?**~~ **RESOLVED by §23.1** — the by-reference
   loophole is closed: if the payload is in the Stadium it counts toward mass, and what is
   not in the Stadium is not resident. The one residue — whether continuation cells are
   contiguous or linked, which shifts every large patron's mass — is §23.4 #4, scheduled as
   item 1.12. (D2)
2. ~~**Is mass constant for a patron's lifetime?**~~ **RESOLVED by §24.3** — mass changes
   only through an arbitrated transfer, never through traffic, so density is stable between
   transfers and §13 gets a mass function that changes at enumerable points. (D2)
3. **How does traffic transfer heat between patrons, concretely?** `vm_physics_touch()`
   does this today for VMs, but it scales the transfer by wall-clock elapsed time
   (`capsule_vm_physics.c:272`), which §18.5 forbids for anything influencing patron state.
   **The transfer rule must be restated on tick count before L0 can use it.** This is the
   single most concrete piece of work this section implies.

---

## 20. VMs are patrons

§17 named four patrons: blocks, words, ACLs, messages. That list is incomplete, and the
omission matters because the missing kind is the only one already implemented.

§9's admission table has always included VM — heat means *runs often*, reap is *death by
cooling* — and §6 states it directly: *"Hera becomes the first entry in it."* Those cannot
be reconciled with a four-patron taxonomy. **VMs are patrons.** Chronologically they are
the first ones.

**DECIDED.**

### 20.1 This is a finding, not a proposal

The outer Stadium already exists in working code:

- `vm_physics_fleet_heat_sum()` sums `execution_heat_q48` **across live VMs**, and
  `vm_physics_conserved()` tests that total against `Q48_ONE`
  (`capsule/capsule_vm_physics.c:456-461`).
- That is a Stadium's K, computed over VM patrons. §19.1's definition of K was derived
  from it.
- Hera already reaps VMs; `TRIPOD.md` makes governing existence her defining contract.

So the mechanism §19 describes is not novel at the VM level. It is running now.

### 20.2 The outer level is unbounded — but fleet K is a real conservation law

**This subsection previously claimed fleet K was "bookkeeping" that could not fail. That was
wrong, and it was wrong on a point of fact rather than of interpretation.** It is replaced
here rather than annotated. The error: it asserted heat is *renormalised* after population
changes, without reading the paths where renormalisation would have to occur.

#### Heat is transferred, not renormalised

Read end to end in `capsule/capsule_vm_physics.c`:

- **The primitive** (`:147-154`). `vm_physics_transfer()` subtracts from one patron and adds
  the same amount to another, clamped at zero. Its own comment: *"The one conservative
  primitive everything else is a special case of… Nothing is created or destroyed:
  sum(execution_heat for all LIVE VMs) is invariant across any call."*
- **Birth** (`:156-185`). Hera (`vm_id 0`) is seeded with `Q48_ONE`; **every other VM starts
  at zero**, described as *"cold mass added to a closed system."* Population growth rescales
  nothing.
- **Death** (`:225-247`). The dying VM's entire heat is *transferred* to the root it chains
  up to before being zeroed.
- **Touch** (`:250-311`). Pulls from other live VMs proportionally, clamped to what they
  actually hold so it *"can never manufacture heat."*

There is no renormalisation anywhere. `vm_physics_conserved()` tests a genuine invariant.

#### It is therefore falsifiable — and there are two ways it can drift

1. **A documented leak** (`:240-244`). If a dying VM is itself the root, or its parent chain
   is broken, there is nowhere conservation-preserving to send the remainder and it is
   dropped. Both cases are guarded and described as "shouldn't happen," but the path exists.
2. **Truncation** (`:304-305`). The proportional fan-out computes
   `(moved_total * heat) / others_total` per VM in integer arithmetic. The shares sum to
   *less than* `moved_total`. **Every multi-VM touch loses a little heat**, so the sum drifts
   downward monotonically. `VM_PHYSICS_EPSILON_Q48` is 3277 — 5% of `Q48_ONE` — so given
   enough touches this would eventually trip.

#### What this means for the bound, and for the campaign

**Bounding the VM population does not make conservation falsifiable — it already is.** The
two are unrelated, and §2 has been corrected accordingly. The bound is still needed, for
finite state (§13) and because density requires a capacity to be dense within (§19.2).

It also changes the reading of the Artemis campaign's K-invariance arm. That arm was not
measuring an identity. It was measuring a quantity that genuinely could drift, and which did
not drift far enough to trip a 5% epsilon over the run. That is a real result about the
system, not an artefact of the check.

**Reported, not scheduled:** the truncation leak at `:304-305` is a live defect in a
conservation law the project makes claims about. It is small per touch and may be entirely
tolerable, but it is monotonic, and nobody has measured how far it drifts over a long run.

### 20.3 Nesting — §12 Q6 is less open than it looks

If VMs are patrons, the structure follows without further invention:

```
  Outer Stadium        patrons: VMs                  ← exists today (unbounded)
    └── per-VM Stadium patrons: words, blocks,
                                ACLs, messages       ← to be built
```

K conserved at each level, with messages as the only thing crossing a boundary. That is
precisely §12 Q6's *nested* option — *"K conserved at each level with messages as the only
thing crossing a boundary, which would mean no shared-memory atomicity is ever needed"* —
and the outer level is already there.

This does not close Q6 by itself, but it changes the question. The choice is no longer
between two greenfield designs; it is whether to formalise a nesting that is already half
built, or to collapse it into a single region and discard the level that works.

~~**LEANING nested.**~~ **DECIDED nested in §21**, written immediately after this section
(D3). See §20.5 for what still had to be settled.

### 20.4 A VM's mass is the capacity share Hera allocated it — PROPOSAL

Marked as proposal, not finding: `VMPhysics` currently holds only `execution_heat_q48`,
`last_active_ns` and `is_live` (`capsule_vm_physics.c:59-63`). There is no share field.

§7 says Hera's job is Stadium distribution, and that *allocating a VM's share is birthing
it*. If that share is the VM's mass, §19's density definition applies unchanged at the
outer level, and §7 stops being abstract.

The payoff is that Hera gets a strictly better lifecycle signal than heat alone:

| VM | Heat | Mass | Density | Reading |
|---|---|---|---|---|
| small, quiet | low | low | moderate | healthy — dense enough, merely small |
| big, idle | low | high | **low** | **sparse — reap or shrink** |
| small, busy | high | low | **high** | dense — a candidate to grow |

Heat alone cannot distinguish *starved* from *small*. Density can. `TRIPOD.md` states that
Hera uses the fleet K view for exactly this question — *"Is a child VM healthy? Is a child
VM starved?"* — and density is the quantity that actually answers it.

Note this stays within `TRIPOD.md`'s constraint that fleet K is **lifecycle telemetry, not
a dispatch mechanism**. Density informs whether a VM should exist or change size. It never
decides where work goes; that remains capability-based routing.

### 20.5 Open

1. **Bounding the VM population.** What is the outer Stadium's capacity, and what happens
   at the bound — birth refused, or coldest VM reaped? The latter is consistent with §19.3
   but means a VM can die because a new one was born, which needs to be an explicit,
   stated behaviour rather than an emergent surprise.
2. **Is a VM's mass its allocated share, or one cell?** §20.4 proposes the share. The
   alternative — every VM is one entry regardless of size — is simpler but throws away the
   distinction in the table above, which is the reason to do this at all.
3. ~~**What is Hera's own mass?**~~ **RESOLVED — Hera is pinned, and her eviction is a
   panic.**

   She is the first patron and she governs the rest, so she is subject to §3's pin wire:
   invariance, not longevity. That is the correct use of pin rather than an exception to
   the rules.

   But pinning alone is a silent guarantee, and a silent guarantee that fails under load is
   worse than none. **If the engine ever selects Hera for eviction, that is a kernel
   panic**, not a skipped iteration and not a logged warning. The condition is
   unreachable by construction; reaching it means the invariant is already broken and
   continuing would run the system without a governor.

   State it as an assertion at the eviction site, not as a filter on the candidate set —
   filtering hides the bug, asserting reports it.

   Her mass is still whatever §20.4 resolves for VMs generally. Pinning governs whether she
   can depart, not how much room she takes.
4. **Does the nesting recurse further?** A VM's Stadium holds patrons; if one of those
   patrons were itself a VM, the structure is a tree rather than two levels. Nothing
   currently requires this, and §11 would call it speculative generality — but it should be
   ruled out deliberately, since the boot order in §6 does not forbid it.

---

## 21. §12 Q6 resolved — nested

> *Q6: 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.*

**Resolved: nested.** The conclusion Q6 leaned toward is right; the reason it gives is not.

**DECIDED.**

### 21.1 The locking premise is false — locking is already free

Every mutex in the kernel build is a no-op. `src/starkernel/vm/host/shim.c:415`:

```c
void sf_mutex_lock(sf_mutex_t *mutex) {
    (void)mutex;
}
```

`dict_lock` and `tuning_lock` (`include/vm.h:410,507`) are real `pthread_mutex_t` in the
hosted build (`platform_lock.h:58-63`), but the kernel compiles with
`-DSTARFORTH_MINIMAL=1` (`Makefile.starkernel:253`) and the shim stubs them out. The stated
rationale is accurate: *"Single-threaded kernel: no contention is possible at the VM
level."*

So the cost Q6 weighs against the single-region option is currently **zero**. The
architecture has not avoided locking; it has locking, inert. Q6 cannot be decided on this
basis.

### 21.2 Step one introduces real concurrency — and locks are the wrong answer for it

This belongs in §16's substrate work, not here, but it surfaced while resolving Q6 and it
lands sooner than anything the Stadium needs.

Once the timer interrupt fires on all three ISAs (§16.1), **the ISR preempts the
mainline.** That is genuine concurrency between two contexts sharing state on a single
hart. It does not exist today, which is precisely why the no-op stub is currently safe.

Making the mutexes real would not fix it and would actively break it: on a single hart, an
ISR spinning on a lock the mainline holds **deadlocks outright**, because the mainline can
never run to release it. This is a well-known failure and it is easy to introduce by
reflex.

The correct answer is already in the design — §18.4's top-half / bottom-half split:

- **ISR (top half)** touches only a word-sized counter and a flag. Single writer.
- **Mainline (bottom half)** is the only context that mutates Stadium structure.

No lock, no deadlock, and no reliance on atomicity beyond aligned word access. This is a
constraint on the L0 implementation, not a preference.

> **Nothing in interrupt context may mutate Stadium structure. Ever.**

### 21.3 What actually decides Q6

With locking removed from the argument, six discriminators remain:

| | Nested | Single region |
|---|---|---|
| Matches what exists | `hotwords_cache`, `rolling_window`, dictionary are already per-VM; the physics registry is already outer | collapses a working two-level structure into one |
| Fault containment | a VM cannot corrupt another's Stadium | one bad patron reaches everything |
| Capacity transfer (§7) | meaningful — VMs have shares to trade | no per-VM share exists to transfer |
| K semantics | conserved per level; existing fleet K survives unchanged | fleet K needs re-deriving |
| Verification (§13) | prove the engine once, instantiate at both levels — demonstrates genericity | one region, marginally simpler |
| **If SMP ever happens** | **messages are the only boundary-crossers → no shared memory, still no locks** | **needs real locks, and the no-op stubs become a live correctness hole** |

The last row is the strongest, and it is what Q6 was reaching for. Nested does not avoid
locking *today* — nothing needs locking today. Nested avoids locking **permanently**,
including in a multi-hart future where the current stubs would silently stop being correct.

The first row is the most practical: §20.1 established that the outer level already exists
and works. Single-region means discarding a working structure to build a simpler one, which
is a poor trade at this stage.

### 21.4 The shape this fixes

```
  Outer Stadium          patrons: VMs
    │                    K conserved here
    │                    bounded — see §20.5 #1
    │
    ├── Hera's Stadium   patrons: words, blocks, ACLs, messages
    │                    K conserved here, independently
    │
    └── (future VMs)     same shape, no special cases
```

Messages are the only patrons that cross a boundary. Everything else is confined to the
level it was born on.

### 21.5 Consequences and open items

1. **The no-op mutexes are now load-bearing in a way they were not before.** They are
   correct today and correct under nesting, but only while the top/bottom discipline in
   §21.2 holds. That discipline should be stated in the code at the stub site, so the next
   reader does not "fix" the no-op into a spinlock and deadlock the kernel.
2. **Two capacities to size, not one.** §20.5 #1 (outer bound) and §17.6 (per-VM bound) are
   now distinct questions with distinct answers.
3. **§12 Q4 / §7 / §17.6(c) elasticity becomes the live question.** Nesting is what makes
   capacity transfer between VMs meaningful, so the hard-versus-elastic decision can no
   longer be deferred as an abstraction — it is the next real fork.
4. **§20.5 #4 remains open.** Nesting is two levels here. Whether a patron may itself
   contain a Stadium — a tree rather than two tiers — is still deliberately unruled.
   Nothing requires it; it should be excluded on purpose rather than by omission.

---

## 22. Elasticity resolved — elastic, via quota over a single cell pool

§7, §12 Q4 and §17.6(c) are one question asked at three scales: is a VM's share of capacity
a hard bound, or elastic under pressure with transfer arbitrated by Hera?

**Resolved: elastic.** And the layout that makes it cheap is a single global cell pool with
per-VM quotas, not separate physical regions.

**DECIDED.**

### 22.1 Why elastic — §19 turns it into a feedback loop

Under §19's definition, elasticity stops being a feature to implement and becomes a
negative feedback loop that runs itself:

```
  VM gets busy  →  heat share rises  →  density rises
                →  capacity flows toward it  →  mass rises
                →  density falls back
```

Capacity flows **down the density gradient** — from sparse VMs toward dense ones. That is
diffusion. There is no threshold to choose, no damping constant, and nothing decides: it is
§4's *read, not decided* applied one level up.

A hard bound offers none of this. It offers a number that had to be guessed correctly at
birth and stays wrong.

§7's own argument is the practical half, and it holds:

> *Under elasticity, birth sizes the rest volume rather than a cap — a more forgiving thing
> to have to guess right.*

Predicting a VM's resting size is far easier than predicting its peak, and being wrong
self-corrects instead of persisting.

### 22.2 The connection to §14

Heat concentrates where work happens — §14's driven-dissipative inversion, order sustained
by throughput. Capacity then follows heat. So the two distributions move in opposite
directions: **heat concentrates while density equalises.**

That makes the flatness of the density distribution a real, measurable signal of a settled
system, distinct from the heat distribution's entropy that §14 already identifies as the
instrument worth having. Two signals, not one, and they say different things.

### 22.3 The layout decision, which matters more than hard-versus-elastic

Framing this as hard-versus-elastic obscures the real choice. Elastic is cheap or expensive
entirely according to how the Stadium is laid out, and §21's nesting decision does not
settle that.

| Layout | Elastic cost | Isolation | §13 verification |
|---|---|---|---|
| Separate physical regions | expensive — transferring capacity means moving memory, and regions fragment against each other | physical | two index spaces |
| **One cell pool, per-VM quota** | **trivial — arithmetic on two integers** | logical (disjoint index sets) | **one index space, one total function** |
| Separate regions, hard bounds | n/a | physical | two index spaces |

**Chosen: one global array of cells, one global index space.** Nesting becomes a
*partition* of that index set rather than separate allocations. A VM's quota is a **count,
not a contiguous range**, so there is no adjacency requirement, no fragmentation, and index
links keep working because indices are global.

#### Free lists are per-VM, not shared

An earlier draft of this section said cells are drawn from a **shared free list**. That was
wrong, and it quietly undercut the argument that decided §21.

§21.3's decisive discriminator is the SMP row: *messages are the only boundary-crossers, so
no shared memory and still no locks.* A shared free list is shared mutable state, touched by
every VM on every admission and every reap. Under SMP it would need a lock or atomics —
exactly what that row claims nesting avoids permanently. The defence offered there, that
"VMs never touch each other's cells," does not reach it: **the free list is nobody's cell,
and allocation touches it.**

The fix costs essentially nothing:

> **Each VM holds its own free-list head index into the global array.** Hera hands a VM its
> cells when she grants quota; the VM allocates and frees only within what it holds.

One head index per VM instead of one global head. One index space is preserved, one datatype
is preserved, §13 is unaffected — and disjointness becomes **total** rather than nearly
total. No mutable structure is shared between VMs at all, which is what §21.3 actually
promised.

Transfer of capacity is then Hera moving cells from one VM's free list to another's, which
is still arithmetic plus a list splice, and still arbitrated at a known point (§22.5 #2).

Two reasons this is the right trade:

- **§13 gets simpler rather than harder.** One array, one datatype, one total function over
  one finite index set. A partition of a finite set is trivial in HOL. Separate regions
  would mean two of everything and a cross-region invariant to maintain.
- **§21's reasoning survives intact.** Its argument for nesting was K conserved per level
  with messages as the only boundary-crossers — both preserved. SMP-safety also survives:
  what matters is that VMs never touch each other's cells, and disjoint index sets give
  that provided quota changes are arbitrated by Hera, which §7 already requires.

What is given up is *physical* fault containment — a corrupt index could reach another VM's
patrons where separate regions would fault instead. That was one of §21.3's six
discriminators and not the decisive one. It is a real cost, recorded here rather than
glossed.

### 22.4 Capacity moves slower than heat — required, not preferred

Two conserved quantities in motion can oscillate. Heat moves on traffic; capacity moves on
density. At comparable rates they chase each other and the ratio never settles.

> **Heat responds tick by tick. Capacity responds to sustained density across many ticks.**

This is §12 Q5's separation-of-timescales discipline — *"keep nested loop periods an order
of magnitude apart"* — arriving as a concrete instance rather than general advice, and it
partly answers Q5.

The exact ratio is a tuning question, but the *ordering* is not: capacity must be the
slower loop. Getting this backwards produces a system that thrashes while every individual
rule looks correct.

### 22.5 Open

1. **The resting floor.** A VM that goes quiet loses capacity; if it wakes it may not
   regain it fast enough. The obvious guard is a floor below which a quota cannot fall —
   but that is a tuned number, which this design otherwise avoids. Decide it deliberately.
   A principled alternative: floor a VM's quota at the mass of its pinned patrons, which is
   not a tuned constant but a derived one.
2. **What arbitrates a transfer, concretely?** §7 says Hera. Under §22.3 a transfer is
   arithmetic on two integers, so the mechanism is trivial — but *when* she does it, and on
   what signal, is not yet stated. It should read off the density gradient (§22.1) rather
   than a schedule.
3. **The exact timescale ratio** in §22.4.
4. **Does the outer Stadium's own capacity ever change?** §22 makes per-VM quotas elastic
   within a fixed total. Whether that total is itself fixed for the machine's lifetime is
   §20.5 #1, still open — and it should stay fixed, or §2's inescapable wall is not
   inescapable.

---

## 23. §12 Q1 dissolved, §12 Q2 sized

### 23.1 Q1 — the inline/by-reference threshold should not exist

> *Q1: Payload threshold — what size goes inline versus by reference.*

§3's motivation is sound: a cell sized for a 1024-byte block would be grotesque for a
patron that carries twelve bytes. But §19 supplies a better answer than a threshold.

If cells are small and uniform, a large patron **occupies more of them, chained by index**.
That is exactly what mass already means. A block is not "by reference" — a block is
**heavy**.

This closes the loophole recorded in §19.6 #1 without introducing a rule:

> **If the payload is in the Stadium, it counts toward mass. If it is not in the Stadium,
> the patron is not resident — it is a handle to the warehouse.**

A 1 MB block cannot occupy one cell and read as dense, because its bytes are on the floor
and the floor is what mass measures.

This is also what gives §19's hysteresis its teeth. Blocks *should* be expensive to keep
resident — that is the entire reason migration back to Artemis is their reap event (§17.2).
A threshold that let big patrons masquerade as light ones would have quietly disabled the
mechanism.

Nothing in §3 is violated: cells stay fixed-size, links stay indices, the Stadium stays an
array. Multi-cell patrons are consistent with all of it. **By-reference is reserved for
things genuinely outside the Stadium**, and those are not patrons.

**DECIDED — Q1 is dissolved rather than answered.**

### 23.2 Q2's premise moved, and an unsettled question sits under it

> *Q2: Arena entry header size… The header must be sized for the worst case, and that case
> is the screen.*

§17.5 removed the screen grid from the Stadium, so that premise no longer holds. What
replaces it depends on something §17.5 established only halfway: it decided the **dirty
event** is the patron, but not what one event *covers*.

| Granularity | 80×25 full redraw | Consequence |
|---|---|---|
| per cell | 2,000 simultaneous patrons | floods the Stadium; starves every other patron |
| **per line span / region** | **~25 patrons** | negligible |

A two-order-of-magnitude swing, currently undefined.

**Recommend region-based.** Framebuffer updates are naturally regional — a scroll dirties
everything, a print dirties one span — overlapping regions coalesce for free, and per-cell
events would make the console the numerically dominant patron kind in the entire system.
That is absurd for something §17.5 correctly classified as a *utility* rather than an
occupant.

**LEANING region-based.** It is a console-design decision as much as a Stadium one, so it
should be confirmed when the console work happens rather than fixed here.

With that settled, the worst case for cardinality becomes **messages** — numerous,
individually small. Which yields the sizing rule:

> **Size the cell so that a typical message is exactly one cell.**

### 23.3 Concrete sizing — proposal, to be validated

These are numbers to check against a real build, not derived truths.

| | Value | Reasoning |
|---|---|---|
| Cell size | **64 bytes** | one cache line; keeps density-ranking scans cache-friendly |
| Header — used | **28 bytes** | identity 8, heat 8, TTL 4, link 4, mass 2, flags + behaviour tag 2 |
| Header — reserved | **4 bytes** | deliberate slack; see below |
| Header — total | **32 bytes** | |
| Inline payload | **32 bytes** | a small message fits in one cell — mass 1 |
| Per-VM Stadium | ~4096 cells = 256 KB | hundreds of hot words and blocks, ACLs, messages in flight |
| Continuation cell | **undetermined** | see below — depends on an unsettled encoding |

The four reserved bytes are deliberate rather than a rounding artefact. The fields above sum
to 28; padding to 32 keeps the header a clean half-cell, leaves room for the
header/continuation discriminator §3 now requires, and gives the exclusivity primitive of
§8 somewhere to live if item 1.1 resolves to a holder index. Reserved space in a header that
is expected to grow is cheaper than repacking one later.

256 KB per VM is comfortable against QEMU's `-m 1024`, and the outer Stadium's capacity
(§20.5 #1) then follows from how many VMs the machine is willing to host.

#### Why the continuation cell cannot be sized yet

An earlier draft stated a 1024-byte block is "17 cells: 1 header + 16 payload." **That figure
assumes continuation cells are contiguous and carry nothing but bytes.** Neither is
established:

- §22.3 allocates cells from a per-VM free list, so a patron's cells are **not necessarily
  adjacent**. If they are not, each continuation cell needs a link to the next — which is
  4 bytes off its payload, making it 60 usable, and a 1024-byte block 18 continuation cells
  rather than 16.
- Alternatively, allocation could guarantee contiguous runs for multi-cell patrons, keeping
  continuation cells pure payload at the cost of reintroducing the fragmentation §3 avoids.

These are different designs with different costs, and the choice determines both the mass of
every large patron and whether §22.3's free list stays a simple list. **OPEN — settle before
item 3.1.** The "17 cells" figure should not be relied on until it is.

Firmness of each figure:

- **Heat at 8 bytes is fixed**, not chosen — Q48.16 in a `uint64_t`, matching
  `execution_heat_q48` in the existing implementation.
- **Link at 4 bytes** caps the Stadium at ~4 billion cells, far past anything plausible. It
  could shrink to 3 or even 2 bytes if the header gets tight.
- **TTL at 4 bytes** gives ~4 billion ticks — over a year at 100 Hz. Almost certainly
  oversized; 2 bytes may do.
- **Cell size 64** is the one to validate first, because everything else is expressed
  relative to it.

**LEANING.** The structure is decided; the constants are not.

### 23.4 Open

1. **Dirty-event granularity** (§23.2) — confirm region-based when console work begins.
2. **Cell size validation.** Build the header for real, count the bytes, and check that a
   typical message still fits in one cell with the behaviour tag and flags included.
3. **Is `identity` needed at all for every patron kind?** For a word it is a name; for a
   block a handle (§24.4); for a message possibly nothing — its identity could be its index.
   If identity can be elided for some kinds, 8 bytes of a 32-byte header is a large saving.
   This must not become a per-kind branch (§18.3), so it is only worth doing if it can be
   expressed uniformly.

   **Larger than it first appeared.** §3 now declares cells a closed two-valued union —
   header or continuation. Whatever distinguishes the two occupies header space and
   interacts directly with any identity elision: a scheme that reuses the identity field as
   the discriminator, for instance, would couple the two decisions. Settle the
   header/continuation encoding first; identity elision is downstream of it.

4. **The continuation-cell encoding.** Whether a multi-cell patron's cells are contiguous
   (continuation cells are pure payload; allocation must find runs, reintroducing
   fragmentation) or linked (continuation cells carry a next-index, costing 4 bytes of
   payload each and changing every large patron's mass). §22.3's per-VM free list does not
   currently guarantee adjacency, so the linked form is the default unless allocation
   changes. **This gates item 3.1** — the cell structure cannot be built without it, and
   §23.3's sizing table cannot be completed without it either.

---

## 24. Mutation, identity, and mass stability

§17.4 #4 and §19.6 #2 ask whether patrons mutate in place. The question as posed does not
survive contact with the patron kinds, and the version that does is cheaper.

### 24.1 Full immutability is not available

FORTH-79 blocks are mutable by definition: `BLOCK` returns a buffer, writes go into it,
`UPDATE` marks it dirty, `FLUSH` writes it back. In a block editor that is a mutation per
keystroke. A rule that every write produces a new patron would mean a new patron per
keystroke.

Words already behave the opposite way. Redefinition creates a **new** dictionary entry
rather than editing the existing one — which is why `vm_dict_resolve_in_bucket()` resolves
in reverse-insertion order, newest visible definition winning.

The kinds genuinely disagree. Forcing them to agree would be §11's exception trap approached
from the other side.

### 24.2 The concern was never payload — it was mass and identity

§19.6 #2 asks this for density stability: if mass changes underfoot, density changes and
ranking is meaningless. §13 asks it because in-place mutation is what makes proofs
expensive.

Neither concern is about payload bytes. A block's contents can change entirely and it is
still 1024 bytes at the same handle.

So the invariant is narrower than immutability and costs almost nothing:

| Tier | Rule |
|---|---|
| **Identity** | never changes for the life of the residency |
| **Mass** | never changes *as a side effect of use* |
| **Header** — heat, TTL, flags, link | mutates freely; this is the engine's work |
| **Payload contents** | may mutate in place, provided size and identity do not |

**DECIDED.**

### 24.3 VMs appear to violate the mass rule, and do not

A VM's mass is elastic by §22 — that is the point of elasticity. But it changes only through
Hera's arbitrated transfer, on the slow loop of §22.4. So the rule is not that mass is
constant:

> **Mass changes only through an arbitrated transfer, never through traffic.**

Traffic moves heat and nothing else. Density is therefore stable between transfers, which is
what ranking requires, and §13 gets a mass function that changes at known, enumerable points
rather than continuously.

### 24.4 A resident patron's identity is its handle, not its content hash

This follows from tier 1 and is worth stating because it is easy to get backwards.

A block's identity while resident is its **handle** — its LBN. Its content hash is computed
at **migration**, for the warehouse. If identity were the content hash, editing a resident
block would change its identity mid-residency and break tier 1 immediately.

§3 already permits this: identity is *"handle or name"*. It never said hash.

Content-addressing therefore stays where it belongs — at the warehouse boundary, which is
already how Artemis and the capsule model behave. The Stadium does not do content
addressing; the warehouse does.

### 24.5 The rule this reduces to

> **No patron may grow or shrink while resident. If it needs to be a different size, it is
> a different patron.**

No per-kind branching, no exception, and it holds for all five patron kinds.

### 24.6 Open

1. **What happens to a resident block whose content changes, at migration time?** Its new
   content hash differs from the one it arrived with. The warehouse sees a new block; the
   Stadium saw one continuous residency. That is coherent, but the hand-off needs stating —
   particularly whether the old hash is retained anywhere for audit.
2. **Does redefining a word while its old definition is resident leave two patrons?** The
   dictionary keeps both entries by design. If both are hot, both are on the floor, both
   have mass. That is probably correct — they are genuinely two different words — but it
   should be confirmed rather than discovered.

---

# 25. The punch list

**This section is authoritative for what is done and what is not.** Sections 1–24 are the
design. This is the work.

---

## 25.0 How to implement this punch list

**Read this subsection every time before touching an item. Do not skip it because it was
read earlier in the session.**

### The rules

1. **One item at a time.** Take the lowest-numbered unchecked item whose prerequisites are
   met. Finish it completely. Do not begin a second item while one is in progress.

2. **Do not jump ahead.** Do not start a later item because it seems easy, related, or
   convenient. Do not do "while I'm in here" work. If a later item looks like it should be
   reordered, say so and wait for an answer — do not reorder unilaterally.

3. **Do not increase scope.** Do exactly what the item says. If the item says "write the
   trap entry," write the trap entry — not the trap entry plus a refactor of the file it
   lives in. Anything you notice that is not in the item gets **reported**, not fixed.
   This includes obvious bugs. Report them; they get their own item if they warrant one.

4. **Do not fabricate, confabulate, or conflate.** If you do not know how something works,
   read it. If you cannot determine it by reading, **stop and say so**. Never invent a
   function, a register name, a constant, a FORTH word, or an API that you have not
   verified exists in this tree or in the relevant hardware manual. Never guess at a value
   and present it as known. Never merge two things that are similar into one thing that is
   neither. A wrong answer stated confidently has cost this project git resets before.

5. **When blocked, stop.** Report exactly what is blocking, what was tried, and what is
   needed. Do not work around it silently. Do not substitute a different approach and
   carry on.

6. **Acceptance is not optional and not negotiable.** Each item states *Done when*. An item
   is not done until that exact condition is met and observed. Not "should work," not
   "compiles cleanly" unless that is what the item says. If acceptance requires the
   three-architecture QEMU boot, then all three have booted and their logs exist.

7. **Report failures honestly.** If a test fails, say it failed and show the output. If a
   step was skipped, say it was skipped and why. Never describe partial work as complete.

### The commit discipline

Every checked-off item gets **its own commit**, and that commit contains:

- the code or document change for that item, and
- this file, with that item's checkbox changed from `[ ]` to `[x]`.

Nothing else. One item, one commit. The punch list and the tree move together, so the
document is never a claim about work that is not in the branch.

Commit message format:

```
<area>: <what the item did>            e.g.  riscv64: real trap entry with SRET return

Punch list §25 item <id> complete.
<one or two lines on what was actually verified, not what was intended>

Co-Authored-By: <the implementing model's attribution line, per its harness>
```

### Standing constraints from `.claude/CLAUDE.md`

These override anything convenient:

- **Never create a branch without explicit permission.** Work on the branch you are on.
- **Never stash.** If the tree is dirty, report it and wait.
- **Never apply a fix that was not requested.** Report it instead.
- **Acceptance for any kernel change is the three-architecture QEMU boot.** There is no
  other test. The hosted `make` build is compile-sanity only.
- **One QEMU instance at a time, foreground, `clean` before `qemu`.** Concurrent runs
  corrupt the timing signal.
- **Read `experiments/bare_metal/README.md` in full before editing any `.4th` file**, and
  verify capsule edits with `mkcapsule --lint` rather than counting bytes by hand.

### When an item is genuinely wrong

The design is not sacred. If implementing an item shows the design is wrong, **stop, report
what the code demonstrated, and propose the amendment.** Amend the relevant section of this
document first, get agreement, then continue. Do not implement something you believe is
wrong because it is written down, and do not silently implement something different.

---

## 25.1 Phase 0 — Substrate

*Nothing in later phases can start until Phase 0 is complete. The engine has nothing to run
on until there is a tick on all three architectures (§16.1, §16.5).*

- [x] **0.1 — Prune `capsules/init.4th` to Hera alone.**
  **Delete** blocks 2051, 2052, 2053, 2054, 2055, 2056, 2058, 2059 — the readiness
  handshake, broadcast test, TRIPOD-TEST, HERMES-E2E, and fleet-DoE scaffolding.
  **Edit** the three surviving blocks: 2057 (`BOOT-BANNER` — drop the Tripod lines), 2049
  (remove the Artemis and Hermes births with their `CD-INIT` calls and the `common:msg.4th`
  / `process.4th` loads; keep `lib.4th`; adjust `VM-TREE` / `VM-CHILDREN`), and 2050 (keep
  the `BOOT-BANNER` call; remove the `READINESS-HANDSHAKE` and `BROADCAST-TEST` calls).
  Leave `capsules/hermes/` and `capsules/artemis/` untouched on disk. An earlier draft of
  this item said "remove blocks 2050–2059," which contradicted its own Refs line — 2050
  survives, edited (C1).
  *Done when:* all three architectures boot to the prompt with Hera alone, no Hermes or
  Artemis in the banner, and the three logs exist under `logs/`.
  *Refs:* the surviving blocks are 2057, 2049, 2050. `mkcapsule --lint` before building.

- [x] **0.2 — riscv64: real trap entry.**
  Replace the one-way `riscv64_trap_entry` in `arch/riscv64/isr.S` with save / dispatch /
  restore / `sret`. Route `scause` bit 63 + cause 5 to the timer path; everything else keeps
  falling through to the existing fatal handler.
  **FP state is not optional (B2 verified):** the kernel builds `-march=rv64gc -mabi=lp64d`
  (`Makefile.starkernel:162`) — hard-float ABI, and kernel code genuinely uses doubles
  (`hotwords_stats_print`). The trap entry must save the ABI's caller-saved FP registers
  plus `fcsr` alongside the integer set; verify the exact register list against the RISC-V
  psABI, not this document. Do not "fix" this by switching to soft-float — that breaks
  existing code and is a build-system decision nobody has made.
  *Done when:* riscv64 boots to the prompt with no regression, and exceptions still halt
  with the same diagnostic as before. **No trap source exists yet at this item** — the
  timer arms in 0.3, whose tick-advance acceptance is what proves this entry path took and
  returned an interrupt (C2). Do not arm the timer early to manufacture evidence here.

- [x] **0.3 — riscv64: SBI timer and real time base.**
  **First, the prerequisite this item silently assumed (B1 verified it absent):** the
  kernel has no DTB access — `BootInfo` (`uefi.h:624-639`) carries no FDT pointer and no
  FDT code exists in the tree. Capture the DTB pointer from the EFI configuration table
  (DTB table GUID) into a new `BootInfo` field in the shared loader. This also serves 0.6.
  Then: arm the timer via the SBI TIME extension, **enable `sie.STIE`**, and **re-arm
  inside the handler on every tick — the SBI timer is one-shot by nature, and a missed
  re-arm stops the heartbeat forever with no error. That is the single most likely silent
  failure of this item (C3).** Switch the time base from `rdcycle` to the `time` CSR and
  take its frequency from the device tree `timebase-frequency`, with a named fallback
  constant — not a bare magic number (§16.2).
  *Done when:* `heartbeat_ticks()` advances on riscv64 and the tick interval matches the
  configured rate within measurement noise. Verify the SBI extension is present before
  relying on it; if it is absent, stop and report rather than falling back silently.

- [x] **0.4 — aarch64: determine the exception level at runtime.**
  Read `CurrentEL` once, early, and let it govern **everything EL-dependent**, not just the
  timer (B3): the vector base register (`VBAR_EL1` vs `VBAR_EL2` — today's `isr.S` writes
  `VBAR_EL1` unconditionally, which is never consulted for exceptions taken at EL2), the
  saved-state pair (`ELR_ELx`/`SPSR_ELx`), and the timer register set (`CNTP_*_EL0` vs
  `CNTHP_*_EL2`). Do not hardcode either level anywhere.
  *Done when:* the boot log states which EL was detected, on real QEMU output.

- [x] **0.5 — aarch64: IRQ vector split.**
  Split `irq_spx` out of the shared fatal handler in `arch/aarch64/isr.S`: save `x0`–`x30`
  plus the saved-state registers (see B3 note below), call a C handler, restore, `eret`.
  The other fifteen vectors are unchanged. Note the 128-byte slot limit — the save sequence
  will not fit inline and must branch to a trampoline.
  **FP state is not optional (B2 verified):** the kernel builds without
  `-mgeneral-regs-only` (`Makefile.starkernel:146`), so the compiler may use SIMD registers
  anywhere. Save the ABI's caller-saved SIMD set plus `FPSR`/`FPCR` alongside the integer
  set; verify the exact list against the AAPCS64, not this document.
  **EL governs the whole path (B3):** this item previously hardcoded `ELR_EL1`/`SPSR_EL1`,
  while 0.4 refuses to hardcode the EL — and today's `isr.S` installs `VBAR_EL1`, which is
  never consulted for exceptions taken at EL2. The EL detected in 0.4 must select the
  vector base register (`VBAR_ELx`), the saved-state pair (`ELR_ELx`/`SPSR_ELx`), and the
  `eret` target state, not just the timer registers.
  *Done when:* aarch64 boots to the prompt with no regression. **No IRQ source exists yet
  at this item** — the GIC lands in 0.6 and the timer arms in 0.7, whose tick-advance
  acceptance is what proves this path took and returned an IRQ (C2). Do not pull 0.6/0.7
  work forward to manufacture evidence here.

- [x] **0.6 — aarch64: minimal GICv2.**
  Enable the distributor and CPU interface, set the priority mask, enable the timer PPI,
  acknowledge via `IAR` / `EOIR`. **Read the base addresses and the PPI INTID from the
  device tree — do not take them from memory or from this document.** The DTB pointer
  comes from the `BootInfo` field added in 0.3 (B1 verified no such field existed). If the
  DTB turns out to be unreachable on aarch64 EDK2, stop and report — deciding between
  loader work and named QEMU-virt constants with a recorded caveat is Captain Bob's call,
  not the implementer's.

  > **DTB confirmed unreachable (checked live, 2026-08-03) — same finding as riscv64.**
  > `fdt_valid(boot_info->dtb)` fails on this system's aarch64 build too (installed
  > firmware: `qemu-efi-aarch64` 2025.11-3ubuntu7, no alternate available). Ruling: named
  > QEMU-virt constants, verified rather than recalled — `qemu-system-aarch64
  > -machine virt,dumpdtb=...` was used to dump QEMU's own internal devicetree (the one
  > EDK2 fails to forward) and decoded with this tree's own `fdt.c` reader, giving
  > **GICD 0x08000000, GICC 0x08010000** (both confirmed for this exact QEMU 10.2.1
  > build, not assumed stable across versions) and **PPI 30** for the non-secure EL1
  > physical timer (bonus finding: PPI 26 for the EL2 hypervisor timer, for item 0.7's
  > EL2 path). Register *offsets* (GICD_CTLR, GICC_IAR, etc.) are architectural, not
  > board-specific, and were cross-checked against
  > `/usr/src/linux-headers-*/include/linux/irqchip/arm-gic.h` rather than recalled.

  > **Acceptance corrected — same defect C2 already fixed for items 0.2 and 0.5, missed
  > here.** "The timer interrupt is delivered and acknowledged" cannot be observed within
  > this item's own scope: nothing arms the timer until item 0.7's `apic_timer_start()`.
  > As written this item could never be marked done on its own evidence. Acceptance is
  > now the same shape as 0.2/0.5: GIC initialises without fault, IAR/EOIR path is wired
  > into `aarch64_irq_handler()` and ready, boots with no regression. Item 0.7's
  > tick-advance acceptance is what proves this path actually delivers and acknowledges an
  > interrupt, exactly as 0.5 already defers to 0.7 for the same reason.

  *Done when:* GIC distributor and CPU interface initialise without fault; the timer PPI
  is enabled; `aarch64_irq_handler()` reads `IAR`, dispatches, and writes `EOIR`; boots to
  the prompt with no regression. Scope is one interrupt; a general GIC driver is out of
  scope and must not be written.

- [ ] **0.7 — aarch64: arm the generic timer.**
  `apic_timer_start()` / `apic_timer_stop()` using the register set chosen in 0.4, re-armed
  each tick.
  *Done when:* `heartbeat_ticks()` advances on aarch64 at the configured rate.

- [ ] **0.8 — Converge the three architectures on one tick path.**
  One `heartbeat_tick()` call site per architecture; the ISR does counter, timestamp and
  flag only. **Per the GAP-A1 ruling, the hardware tick drives instrumentation only:** the
  bottom half services TIME-TRUST bookkeeping, and the engine (`vm_tick()`, decay,
  inference) stays on the virtual tick — execution-paced, exactly as today. Nothing that
  feeds patron state reads the hardware counter.
  *Done when:* all three architectures drive the same TIME-TRUST bottom half; no loop math
  runs in interrupt context; and `vm_tick()`'s call sites are unchanged.
  *Refs:* §16.4 (as ruled), §18.4, §21.2.

- [ ] **0.9 — Write the concurrency constraint at the mutex stub.**
  Add a comment at `src/starkernel/vm/host/shim.c:415` stating that the no-op is correct
  only while nothing in interrupt context mutates shared structure, and that making it a
  real spinlock would deadlock a single hart.
  *Done when:* the comment is in place. This is a documentation item; no behaviour changes.
  *Refs:* §21.2, §21.5 #1.

- [ ] **0.10 — Phase 0 acceptance.**
  Full three-architecture QEMU run. Confirm: boots to prompt on all three; tick count
  non-zero on all three; on riscv64 after 0.3, trust near `Q48_ONE` and variance small
  relative to the new `expected_delta` — not merely "sane", which is unfalsifiable (C6);
  amd64 output unchanged from its pre-branch behaviour (a valid control under the GAP-A1
  ruling, since 0.8 no longer touches engine plumbing).
  **Then boot one architecture twice and confirm the parity dict hash is identical across
  runs.** If it drifts, something is firing on wall time and Phase 0 is not complete.
  *Done when:* all of the above observed, logs committed.
  *Refs:* §16.4, §18.5.

---

## 25.2 Phase 1 — Design questions to settle on paper

*These need answers, not code. Each one is settled by amending the relevant section of this
document and committing that amendment as its own item.*

- [ ] **1.1 — Exclusive access ("sitting in a car").** §8 asserts a per-patron exclusivity
  primitive that is not a global lock. Nothing defines it. Decide what it is, what it
  blocks, and what happens if a patron is selected for reaping while held.
  *Refs:* §8. **This is the largest unresolved design question.**

  > **Hard prerequisite of item 3.1, and its outcome may amend §3.** This item is filed in
  > Phase 1 alongside questions that have no structural effect, and it is not in that class.
  > A per-patron exclusivity primitive plausibly needs a held flag or a holder index — a
  > **ninth wire** in §3's table, in the header item 3.1 builds. Resolve 1.1 after 3.1 and
  > the cell header gets rebuilt.
  >
  > §25.4 already blocks Phase 3 on items 1.1–1.7, so the ordering is right. What was
  > missing is *why 1.1 specifically* — which is the kind of omission that gets an item
  > quietly reordered later by someone who does not know what it was holding up. §23.3
  > reserves 4 header bytes partly against this outcome.

- [ ] **1.2 — The resting floor.** Whether a VM's quota has a floor, and whether it is the
  mass of its pinned patrons (derived) or a constant (tuned). *Refs:* §22.5 #1.

- [ ] **1.3 — What triggers a capacity transfer.** Hera arbitrates; on what signal, and how
  often. Should read the density gradient, not a schedule.
  **Constraint, not optional:** arbitration mutates patron mass, so §18.5's invariant binds
  it directly — *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.* Pacing
  arbitration off a wall-clock interval would reintroduce exactly the defect item 2.1
  exists to remove, in a new place. Whatever 1.3 decides must be expressible in ticks.
  *Refs:* §22.5 #2, **§18.5**, §22.4.

- [ ] **1.4 — The heat/capacity timescale ratio.** The ordering is fixed (capacity slower);
  the ratio is not. *Refs:* §22.4, §22.5 #3.

- [ ] **1.5 — The outer bound.** The outer Stadium's capacity, and the behaviour at the
  bound: birth refused, or coldest VM reaped. *Refs:* §20.5 #1, §22.5 #4.

- [ ] **1.6 — A VM's mass: allocated share, or one cell.** *Refs:* §20.4, §20.5 #2.

- [ ] **1.7 — Rule out recursion beyond two levels** — deliberately, not by omission.
  *Refs:* §20.5 #4.

- [ ] **1.8 — Block content change at migration.** A resident block whose content changed
  has a different hash on the way out. State the hand-off. *Refs:* §24.6 #1.

- [ ] **1.9 — Redefined words as two resident patrons.** Confirm both may be on the floor.
  *Refs:* §24.6 #2.

- [ ] **1.10 — Identity elision.** Whether identity can be dropped for some kinds without a
  per-kind branch. Optimisation; may be closed as "no". *Refs:* §23.4 #3.

- [ ] **1.11 — Dirty-event granularity.** Leaning region-based. **Blocked on item 4.3** —
  it is settled as part of the console migration, not speculatively before it (C5).
  *Refs:* §17.5, §23.2, §23.4 #1.

- [ ] **1.12 — The continuation-cell encoding.** Contiguous (continuation cells are pure
  payload; allocation must find runs, reintroducing fragmentation) or linked (each
  continuation cell carries a next-index, costing 4 bytes of payload and changing every
  large patron's mass). §22.3's per-VM free list guarantees no adjacency, so linked is the
  default unless allocation changes. This was §23.4 #4 — a stated blocker of item 3.1 that
  was never a schedulable item until now (C4). Settling it completes §23.3's sizing table.
  *Refs:* §23.4 #4, §23.3, §22.3. **Prerequisite of 3.1.**

---

## 25.3 Phase 2 — Prepare the existing physics

- [ ] **2.1 — Restate heat transfer on the virtual tick.**
  `vm_physics_touch()` scales transfers by wall-clock elapsed time
  (`capsule_vm_physics.c:272`). Restate it on **the virtual tick** — the execution-derived
  counter of §16.4 as ruled, not the hardware heartbeat, whose interleaving with execution
  is wall-clock-dependent and would leave the acceptance below unachievable (§25.7.1
  GAP-A1).
  *Done when:* no wall-clock value influences heat, **and the same capsule booted twice
  produces an identical fleet heat sum across the two runs** — achievable now that both
  the touch points and the elapsed-tick values are deterministic functions of execution.
  *Refs:* §16.4 (as ruled), §18.5, §19.6 #3.

  > **Acceptance corrected.** This item previously accepted on the dictionary-hash
  > double-boot check from 0.10. That cannot detect this work: §18.5 establishes that
  > `vm_physics_touch()` writes `node->physics`, **not** `DictEntry.execution_heat`, and
  > therefore never reaches the parity hash. The dict hash would be identical whether 2.1
  > succeeded, failed, or was skipped. Fleet heat is the quantity this item changes, so
  > fleet heat is what has to be compared. Run 0.10's dict-hash check as well, as a
  > regression guard — but it is not evidence for 2.1.

- [ ] **2.2 — Bound the VM registry.**
  The registry is a `kmalloc`-backed unbounded list (`capsule_vm_physics.c:71-72`). Give it
  the hard bound decided in 1.5.
  *Done when:* the population is bounded, birth at the bound behaves as 1.5 specifies, and
  the three-architecture boot is unaffected.
  *Refs:* §2, §13, §19.2, §20.2.

  > **Justification corrected.** This item previously read that the registry "makes fleet K
  > an identity that cannot fail" and accepted on `VM-CONSERVED?` becoming able to fail.
  > Both were wrong, and the reason is now in §20.2: heat is **transferred**, not
  > renormalised, so conservation is already a real invariant and already falsifiable —
  > by the dropped-remainder path at `:240-244` and by integer truncation at `:304-305`.
  > Bounding the population changes neither.
  >
  > The bound is still needed, on the two grounds §2 now states: **finite state** for §13's
  > induction and model checking, and **density requires a capacity to be dense within**
  > (§19.2), without which §19.3's admission rule has nothing to compare against. Those are
  > the honest justifications and this item now rests on them.
  >
  > Making conservation *more* falsifiable is a different and larger piece of work — fixing
  > the truncation leak — and is recorded in §25.7 rather than folded in here.

---

## 25.4 Phase 3 — Stadium core

*Blocked on Phase 0 complete, and on items 1.1–1.7 and 1.12.*

- [ ] **3.1 — Cell and header.** Define the entry with all eight wires (§3) — **nine if
  item 1.1 resolves to a holder index.** Define both members of §3's closed two-valued
  union: patron header and continuation cell. Validate the 64-byte cell by counting real
  bytes; adjust and record if it does not fit.
  **Blocked on:** item 1.1 (may add a wire) and item 1.12 (the continuation-cell encoding —
  contiguous or linked — which sets the mass of every large patron and cannot be guessed).
  *Refs:* §3, §23.3, §23.4 #4.
- [ ] **3.2 — Boot-time allocation.** One global cell array, sized from the memory budget,
  before any VM exists. *Refs:* §6, §17.6, §22.3.
- [ ] **3.3 — Behaviour enumeration and dispatch.** Closed tag set fixed at build time.
  Enumerate behaviours, never patron kinds. *Refs:* §13, §18.3.
- [ ] **3.4 — Density ranking.** Heat ÷ mass, read not computed. *Refs:* §19.2, §19.3.
- [ ] **3.5 — Admission and eviction.** Admit if denser than the least dense resident.
  *Refs:* §19.3.
- [ ] **3.6 — Hera as patron zero, pinned.** Assert at the eviction site; selecting Hera is
  a panic, not a filtered candidate. *Refs:* §20.5 #3.

---

## 25.5 Phase 4 — Migrate the subsystems

*One subsystem at a time, converted completely. Never two live heat mechanisms at once
(§11).*

- [ ] **4.1 — Hot words onto the Stadium.** Replaces the round-robin eviction with density
  ranking. Measurable before and after via `stats.evictions` / `stats.promotions`.
  *Refs:* §17.3.
- [ ] **4.2 — Hermes native on the Stadium.** The proving ground; produces the effort
  number. *Refs:* §10.
- [ ] **4.3 — Console.** Settles 1.11 as part of the work. *Refs:* §17.5.
- [ ] **4.4 — Artemis last.** It works today; it is the thing that cannot be broken.
  *Refs:* §10.

---

## 25.6 Phase 5 — Verification and measurement

- [ ] **5.1 — Re-run the DoE on the new substrate.** A green POST suite is not evidence that
  K holds; those are different claims. *Refs:* §10.
- [ ] **5.2 — Isabelle/HOL.** One datatype, one index space, one conservation theorem.
  *Refs:* §13, §22.3.
- [ ] **5.3 — Shrink the subsystem documents.** `ARTEMIS.md`, `HERMES.md`, `CONSOLE.md`,
  `TRIPOD.md` should each reduce to roughly three lines. Any that grows is fighting the
  design. `TRIPOD.md` also needs its Immediate Goal rewritten — it currently requires Hera
  to spawn Hermes and Artemis at boot, which 0.1 undoes. *Refs:* §11.

---

## 25.7 Reported, not scheduled

*Found while reading. Not fixed, not assigned. They become items only if Captain Bob says
so.*

- **Fleet heat leaks on every multi-VM touch.** `vm_physics_touch()` fans out
  `(moved_total * heat) / others_total` per VM in integer arithmetic
  (`capsule_vm_physics.c:304-305`); the shares sum to less than `moved_total`, so total
  fleet heat drifts downward monotonically. `VM_PHYSICS_EPSILON_Q48` is 5% of `Q48_ONE`, so
  a long enough run would trip `VM-CONSERVED?`. Nobody has measured the rate. This is a
  live defect in a conservation law the project makes claims about — see §20.2.
- `hotwords_cache_promote()` writes NULL into the ring if `word` is NULL and the cache is
  full (`physics_hotwords_cache.c:363-364`). Unreachable today.
- `heartbeat_trust()` is exported and has zero callers.
- `m5_time_trust` and `m5_variance` (`include/vm.h:315-316`) are declared and never used.
- `src/*.c.bak` files are tracked in git at the `src/` top level.
- The `bump-z` / `bump-y` targets in the hosted `Makefile` reference version macros that do
  not exist in the generated `include/version.h`.

### 25.7.1 Second review pass — 2026-08-03, pre-coding. Awaiting rulings.

*A full re-read of this document as it stood after the first review's corrections, looking
for what would break a lower-capability model working the punch list.*

**Status: all fourteen findings closed, 2026-08-03.** A1 ruled (virtual tick) and applied
to §16.4/§17.1/§18.4 and items 0.8/2.1. B1 verified (no DTB access; fixed into 0.3/0.6),
B2 verified (no FP restriction on any arch; fixed into 0.2/0.5), B3 applied (EL governs
the vector path; 0.4/0.5). C1–C7 applied to their items; D1–D3 swept. The findings below
are preserved as the record of what was found and why.

#### GAP-A1 — §16.4's central inference is unsound. ~~NEEDS RULING~~ **RULED 2026-08-03: virtual tick.**

> **Applied.** The recommended resolution below was adopted by Captain Bob. §16.4, §17.1
> and §18.4 now carry the ruling; items 0.8 and 2.1 were reworded to it. Item 0.10 needed
> no change: with the engine staying execution-paced, its double-boot dict-hash check is a
> valid regression guard and the amd64-as-control framing is accurate again, since 0.8 no
> longer touches engine plumbing on any architecture. The argument below is preserved as
> the record of why.

§16.4 claims: *"same input → same tick ordinal → same reap and inference events → same
hash."* The last arrow is invalid. The hash covers `execution_heat`, which is co-written by
**two streams** — word executions (increments) and engine ticks (decay). Once ticks come
from a hardware timer, *where tick N lands relative to the instruction stream* is
wall-clock-dependent: under TCG, run A takes tick 42 after word #1000, run B after word
#1017. Decay interleaves differently, heat trajectories diverge, hashes differ. Firing on
tick count fixes the engine's *schedule*; the hash measures the *composition* of the two
streams, and that is not fixed.

Blast radius:

- **Item 0.8 is ambiguous between two different kernels.** Reading (i): the bottom half
  services only TIME-TRUST bookkeeping — safe, parity holds, but "compudynamics on the
  tick" did not actually happen. Reading (ii): the bottom half drives the engine/decay from
  the hardware tick — parity breaks *by construction*, not by implementation error.
- **Item 0.10's double-boot dict-hash check** then fails under reading (ii), and no
  implementation effort can fix it.
- **Item 2.1's corrected acceptance** (identical fleet heat *sum* across runs) is *still*
  unachievable under a hardware tick: touch amounts scale with elapsed ticks between fixed
  execution points, elapsed ticks vary run to run, so truncation losses vary, so the sum
  varies. The first review's amendment did not go far enough.
- **The tempting split does not survive either.** "Hash-covered state on execution ticks,
  TTLs on hardware ticks" fails because TTL expiry has side effects on the instruction
  stream — a message expiring versus being delivered changes what runs, which corrupts heat
  downstream. §17.1's "one tick" instinct was right; it picked the wrong clock.

**Recommended resolution (not decided):** the engine's tick is a **virtual tick — a pure
function of the execution stream**, which is exactly what exists today and why parity holds
today. The hardware heartbeat becomes: the TIME-TRUST instrument (now real on three ISAs
instead of one), the idle wake source, and the driver of nothing that feeds patron state.
Scripted/parity runs stay bit-identical; interactive idling pumps virtual ticks from the
REPL poll loop so TTLs still expire in real time, in a context where parity was never
claimed. Phase 0's timer work remains fully justified as instrument and substrate. Under
this ruling §16.4, §17.1, §18.4 and items 0.8, 0.10, 2.1 all need rewording. The
alternative — re-baselining the parity claim itself — touches the patent support material
and is not recommended.

#### GAP-B — unverified prerequisites (each is a short read; none has been done)

- **B1 — Device tree reachability.** Items 0.3 and 0.6 instruct "read from the device tree"
  (0.6 forbids alternatives). Whether the loader captures the DTB from the EFI
  configuration table into `BootInfo` is unverified. If it does not, 0.3 and 0.6 silently
  require loader plumbing that has no punch item. Read `uefi_loader.c` / `BootInfo` first.
- **B2 — FP/SIMD in the ISR path.** Items 0.2 and 0.5 save integer state only. If the
  kernel is not built with `-mgeneral-regs-only` (aarch64) / soft-float (riscv64), a C
  interrupt handler may clobber FP registers the interrupted mainline was using. One grep
  of `Makefile.starkernel` settles it; the items should carry the check.
- **B3 — 0.4's EL detection does not govern the vector path.** 0.4 refuses to hardcode the
  EL for timer registers, but 0.5 hardcodes `ELR_EL1`/`SPSR_EL1`/`eret`, and today's
  `isr.S` installs `VBAR_EL1`. If EDK2 leaves the kernel at EL2, exceptions vector through
  `VBAR_EL2` and 0.5's entire edit targets a table that is never consulted. EL
  determination must govern VBAR, the saved-state register forms, *and* the timer set.

#### GAP-C — defects in punch items a literal implementer will hit

- **C1 — Item 0.1 contradicts itself.** Body says remove "blocks 2050–2059"; Refs says
  block 2050 *survives*. The delete set is 2051–2056 + 2058–2059; 2050 is edited (banner
  call kept, handshake/broadcast calls removed). A literal reading deletes the banner.
- **C2 — Items 0.2 and 0.5 have unsatisfiable acceptance.** Both require having "taken and
  returned from at least one trap/IRQ," but at 0.2 no timer is armed (0.3) and at 0.5 there
  is no GIC (0.6) and no armed timer (0.7). No interrupt source exists at those stages.
  Fix: 0.2/0.5 accept on "boots unchanged, no regression"; the took-and-returned evidence
  moves to 0.3/0.7.
- **C3 — Item 0.3 lost the two silent-failure modes.** The SBI timer is one-shot: a missed
  re-arm stops the heartbeat forever with no error. `sie.STIE` is also unmentioned. 0.7
  says "re-armed each tick"; 0.3 must too.
- **C4 — §23.4 #4 blocks item 3.1 but is not a punch item.** The continuation-cell
  encoding gates 3.1 by 3.1's own text, but rule 1 walks numbered items and nothing ever
  schedules it. It should become item 1.12.
- **C5 — Item 1.11's deferral is not a formal prerequisite.** It says "do not settle
  speculatively" but states no blocker, so rule 1 would schedule it. Add "(blocked on
  4.3)."
- **C6 — Item 0.10 misc.** "amd64 output unchanged" treats amd64 as a control, but 0.8
  changes amd64's engine plumbing by design — stale framing. "TIME-TRUST and variance
  sane" is soft; sharpen to trust near `Q48_ONE`, variance small relative to the new
  `expected_delta`.
- **C7 — The commit template hardcodes "Claude Opus 5."** Whichever model implements will
  either violate the template or misattribute. Genericize.

#### GAP-D — inconsistencies left by the layered amendments

- **D1 — Three passages still argue from the K-justification the first review removed.**
  §17.3 ("wastes the bounded capacity that gives K a fixed denominator"), §17.5's sizing
  argument (same phrase), and §17.6(d) — the worst, since it cites §2 for a claim §2 now
  explicitly disavows ("Without an inescapable bound, K is bookkeeping — §2 says this in as
  many words").
- **D2 — §19.6 #1 and #2 read as open but are resolved** (#1 by §23.1 with the residue in
  §23.4 #4; #2 by §24.3). §17.4 got strike-through treatment; §19.6 did not.
- **D3 — §20.3 still says "LEANING nested"** one section before §21 decides it. One
  forward pointer fixes it.

#### What held up under this pass

The patron taxonomy, behaviours-not-kinds dispatch, the three quantities, the two-valued
cell union, the nested-elastic-quota layout, the identity/mass invariant, Hera's
pin-and-panic, and §25.0's rules themselves. None of them moved.

**Triage order when this is picked up:** rule on A1 first — it decides what item 0.8 even
means. B1/B2 are ten-minute reads. C and D are mechanical once A1 is ruled. Nothing should
go to a coding model before C1, C2 and C3 are fixed at minimum — those are the ones it
will hit in its first hour.