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