Punch list §25 item 0.4 complete. Adds aarch64_current_el() in arch.c: reads CurrentEL[3:2] on first call, caches the result (CurrentEL cannot change post-ExitBootServices, so every consumer gets the same answer without repeating the MRS). Called from arch_interrupts_init() in interrupts.c -- the earliest point with both a working console (up since M1) and a genuine first consumer (vector installation is the first EL-dependent operation) -- and the detected level is printed to the boot log there. Declared via extern-in-place in interrupts.c rather than added to the shared arch.h: "exception level" has no amd64/riscv64 equivalent, matching the convention already used for riscv64_timer_rearm() in item 0.3. Verified on real QEMU output: "AArch64: running at EL1", correctly positioned immediately before "IDT installed." in the serial log. Boots clean, dict_hash 0x3d4e1daf289da94f unchanged from the item 0.1-0.3 baseline. Scope: this item establishes the detection and exposes it; it does not yet change VBAR/ELR/SPSR or timer-register selection to use it. arch_interrupts_init() still writes VBAR_EL1 unconditionally, and now says so explicitly in its own doc comment -- if aarch64_current_el() ever reports 2 on real hardware, exceptions taken at EL2 vector through VBAR_EL2, which nothing programs yet. That gap is items 0.5 (vectors/saved-state) and 0.7 (CNTP vs CNTHP) to close, per FABRIC.md's GAP-B3 finding. The boot-log EL2 case prints a note pointing at both. Only aarch64-scoped files touched (arch.c, interrupts.c) -- no shared loader or header changed, so amd64 and riscv64 are provably unaffected; not rebuilt for this item. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
2429 lines
127 KiB
Markdown
2429 lines
127 KiB
Markdown
# 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.
|
||
|
||
- [ ] **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.
|
||
|
||
- [ ] **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.
|
||
*Done when:* the timer interrupt is delivered and acknowledged. 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.
|