Adds VERT/EDGE/CUBE to capsules/fabric.4th (blocks 4913-4915). VERT ( n -- x y z ) reads bits 0/1/2 of a corner index as the X/Y/Z sign (+-CS from center), so all 8 cube corners come from one word. EDGE resolves both corners via VERT and calls LINE; CUBE is 12 EDGE calls (4 bottom, 4 top, 4 vertical). First item in the 4.3.3.x sequence with no new bug found -- a small signal that Q.TO-INT, the VARIABLE alignment fix, and the LINE-STUCK? cap were the real gaps rather than something still lurking in LINE/PROJECT/CART-Y. Verified live on amd64: a centered, half-size-100 cube renders correctly -- front/back face squares, back face offset diagonally up-right by exactly the 45-degree cavalier projection's depth term, all 12 edges connecting at the right corners. All three architectures boot clean to ok> with the DoE completing; dict_hash identical across all three and unchanged from 4.3.3a/4.3.3b. FABRIC.md item 4.3.4 marked done. This is the checkpoint -- 4.3.x groundwork stops here for review per this item's own acceptance criterion.
4196 lines
254 KiB
Markdown
4196 lines
254 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) |
|
||
| **contains** | **index of the patron currently held inside this one, or none — containment, not a lock (§8, item 1.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.
|
||
>
|
||
> **Amended again by item 1.1 (§25.2).** `contains` is a ninth wire — an index to the
|
||
> patron currently held inside this one, or none. This does not reopen the two-valued cell
|
||
> union above: the contained patron keeps its own independent header and cells elsewhere in
|
||
> the Stadium, resolved and ranked exactly as any other patron. `contains` is a reference to
|
||
> that residency, not a physical embedding of one patron's cells inside another's. See §8 for
|
||
> what this wire is for and why it replaced a lock.
|
||
>
|
||
> **Amended by item 3.1 (2026-08-04) — the header/continuation discriminator is an
|
||
> external side bitmap, not a header field.** A flat-array scan must tell a header cell
|
||
> from a continuation cell before it knows which shape it is looking at. That rules out
|
||
> folding a tag into either variant's own bytes: a continuation cell has no header fields
|
||
> to place one in, and forcing a common leading tag byte into both shapes would eat into
|
||
> the continuation cell's usable payload, contradicting §23.3's 60-byte figure. Ruled: one
|
||
> bit per cell, in a bitmap kept outside the 64-byte cell array. Item 3.1 declares the
|
||
> bitmap's purpose and indexing; item 3.2 (boot-time allocation) allocates it, since it is
|
||
> Stadium-sized memory decided at boot alongside the cell array itself.
|
||
|
||
**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*.
|
||
|
||
> **RESOLVED by item 1.1 (§25.2), 2026-08-04.** *"Occasionally one sits in a car, which is
|
||
> the only exclusive thing in the room, scoped to a single object, no global lock."* The
|
||
> instinct that this needs an exclusivity primitive was right; the instinct that it needs a
|
||
> **lock** was not. Sitting in a car is not mutual exclusion — it is **containment**. The
|
||
> person-patron does not get barred from the car-patron; it goes **inside** it.
|
||
>
|
||
> **The mechanism is the ninth wire, `contains`** (§3): an index to the patron currently held
|
||
> inside this one, or none. Getting in sets it; getting out clears it. The contained patron
|
||
> keeps its own independent header and residency — it is still ranked, still heats and cools
|
||
> like anything else — `contains` only records the relationship.
|
||
>
|
||
> **Reap is gated, not derived.** A patron with a non-none `contains` link cannot be reaped.
|
||
> This is checked ahead of density ranking, as an absolute rule, not inferred from mass or
|
||
> density — a light, cold container with something inside it must not read as evictable just
|
||
> because the numbers say so. This is what actually answers the use-after-free concern §9
|
||
> raised: the engine cannot select an occupied patron for reaping in the first place.
|
||
>
|
||
> **Containment chains, and unwinding is forced, not chosen.** Because a patron can itself be
|
||
> contained, `contains` links can form a chain — a patron inside a patron inside a patron.
|
||
> If A contains B contains C, A cannot become reapable until B is empty, and B cannot become
|
||
> reapable until C departs. This ordering is **topological, not a policy** — there is no
|
||
> FIFO/LIFO choice to make here; the chain's own shape forces innermost-first.
|
||
>
|
||
> **Bounded, single occupant per level.** Each patron holds at most one `contains` link
|
||
> (single occupant, not a set). Chain depth is capped — **default 5** — enforced by the
|
||
> engine at containment-entry time (refuse to nest past the cap). The cap is a **Kconfig
|
||
> symbol**, not a hardcoded constant, consistent with this project's existing tunable-knob
|
||
> convention (`STARFORTH_ENABLE_VM`, `HOTWORDS_CACHE_SIZE`, etc.) — named at implementation
|
||
> time in item 3.1, default 5, scannable via `menuconfig`.
|
||
>
|
||
> **What this leaves genuinely open, deferred, not blocking:** if multiple independent
|
||
> containment chains are simultaneously blocked and waiting to unwind, whether the engine
|
||
> gives any of them priority over another is a scheduling question, not a header-design one.
|
||
> It does not affect the wire, the reap gate, or the depth cap, and is left for whenever it
|
||
> becomes a real concern.
|
||
>
|
||
> §22.3's earlier remark that separate-region layout gives "physical fault containment" that
|
||
> the single-cell-pool layout gave up is unaffected by this — `contains` is a logical
|
||
> reference within one VM's own Stadium, the same trust boundary that layout decision already
|
||
> accepted.
|
||
|
||
---
|
||
|
||
## 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.**~~ **DECIDED 2026-08-04**, on paper, before item 4.1's code — settled after
|
||
starting that item surfaced this section as its unresolved prerequisite.
|
||
|
||
**The core claim stands, for the reason already given above.** The existing cache is
|
||
self-contradictory as built: heat gates admission, nothing governs departure, and the
|
||
consequence is that the hottest word in the cache can be evicted purely because its slot
|
||
came up in the round-robin rotation. Moving words onto the Stadium repairs a real defect,
|
||
not a relabeling exercise, and `stats.evictions`/`stats.promotions`/`stats.cache_hits` make
|
||
it directly measurable before and after, exactly as this section already argued.
|
||
|
||
**What was actually missing was the hosted/kernel split** — §25.5's own header warns
|
||
"never two live heat mechanisms at once" (§11), but nothing said which way that resolves,
|
||
and the two subsystems involved are not symmetric:
|
||
|
||
- `src/physics_hotwords_cache.c` and `src/dictionary_management.c` are vendored, shared
|
||
source. `dictionary_management.c` calls `hotwords_cache_lookup()` /
|
||
`hotwords_cache_evict_*()` directly in the word-lookup path, **not gated by
|
||
`#ifdef ENABLE_HOTWORDS_CACHE`** at the call sites — the toggle only controls the cache's
|
||
own internal behaviour, not whether these call sites exist. This file must keep compiling
|
||
and working correctly in both the hosted and kernel builds (CLAUDE.md is explicit).
|
||
- The Stadium (`stadium.h`/`stadium.c`) is, and by construction of everything built through
|
||
item 3.7 can only be, kernel-only — every declaration in it is `#ifdef __STARKERNEL__`.
|
||
Nothing in this document has ever proposed a hosted Stadium, and building one is not
|
||
something item 4.1 needs to do.
|
||
- `ENABLE_HOTWORDS_CACHE` already defaults to **off** in both the hosted `Makefile` and
|
||
`Makefile.starkernel` today (`Kconfig.physics`, confirmed against both Makefiles directly
|
||
— a stale comment beside the Makefile default claims the opposite, but the actual default
|
||
is `n`/`0` in both). So "two live mechanisms" is not a live conflict in the default build
|
||
today; it only becomes one once item 4.1's kernel-side migration and the old cache are
|
||
both actually exercised at once.
|
||
|
||
**Resolution: kernel and hosted diverge, and that is the correct shape, not a compromise.**
|
||
|
||
- **Kernel builds:** once item 4.1 lands, the old cache's *effect* is retired under
|
||
`__STARKERNEL__` — word patrons migrate onto the Stadium, and
|
||
`hotwords_cache_lookup()`/`hotwords_cache_evict_*()`'s call sites in
|
||
`dictionary_management.c` are bypassed for the kernel build regardless of the
|
||
`ENABLE_HOTWORDS_CACHE` setting. The shared source can stay compiled as-is (untouched, for
|
||
hosted's sake) while being functionally inert on the kernel side. Item 4.1 decides the
|
||
exact mechanism (a build-time gate, a runtime check, or something else) — not invented
|
||
here.
|
||
- **Hosted builds: unchanged.** No Stadium exists there, none is being built for it, and the
|
||
existing mechanism — including its current off-by-default setting — stays exactly as it
|
||
is. This is what keeps CLAUDE.md's dual-target compileability requirement satisfied
|
||
without inventing a second Stadium implementation nobody asked for.
|
||
|
||
Consequences from above still hold: words need no pin exception (reap event is cooling off
|
||
the floor), §16.3's dictionary-parity concern narrows to the hot set alone, and pin goes
|
||
back to meaning invariance rather than a general-purpose escape hatch.
|
||
|
||
### 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.
|
||
|
||
### 17.7 Word-level heat conservation — DECIDED 2026-08-05, blocks item 4.1 until implemented
|
||
|
||
Item 4.1 (hot words onto the Stadium, §25.5) needs word patrons to carry a Stadium `heat`
|
||
share. The obvious move — `q48_from_u64(execution_heat)`, a pure representation change
|
||
grafted onto `DictEntry.execution_heat`, no real conservation — was proposed and **rejected
|
||
2026-08-04**: Captain Bob wants real conservation for word heat, on the same footing as
|
||
§19.1's fleet-level invariant, not just a unit conversion of the existing counter.
|
||
|
||
**Corrected premise (2026-08-05): this was never a choice between converting
|
||
`execution_heat` or leaving it alone.** `include/starkernel/vm/stadium.h:64` already declares
|
||
the Stadium cell's `heat` field as `Q48.16, conserved share of 1.0 (§19.1)` — written when
|
||
item 3.1 was done, before this section was reopened. Items 3.4 (density = heat ÷ mass) and
|
||
3.5 (admit if denser than the least-dense resident) already consume it as a real, relative,
|
||
conserved quantity. **L0 already has a genuine conservation mechanism; it has just never
|
||
been fed, because nothing has been admitted to the Stadium yet.** `execution_heat` and
|
||
Stadium `heat` are two different fields with two different jobs. Item 4.1's task is to feed
|
||
the second one from word dispatch, not to convert the first one into it. That reframing
|
||
resolves four of the five questions this section left open:
|
||
|
||
1. ~~**The promotion threshold breaks.**~~ **RESOLVED — it doesn't, because nothing replaces
|
||
it.** `HOTWORDS_EXECUTION_HEAT_THRESHOLD` belongs to the old cache mechanism, and §17.3's
|
||
resolution already retires that mechanism's *effect* under `__STARKERNEL__` regardless of
|
||
this question. Item 4.1 admits by item 3.5's rule instead — density relative to the
|
||
least-dense resident — which is already the relative trigger this bullet said conservation
|
||
would require, and it is already built.
|
||
2. ~~**`dict_hash` moves.**~~ **RESOLVED — it doesn't move, because `execution_heat` is not
|
||
touched.** `capsule_dict_hash_hook()` keeps hashing name and `execution_heat` exactly as
|
||
today; the counter keeps incrementing and decaying exactly as today. Stadium `heat` is not
|
||
part of `dict_hash` and item 4.1 does not need to add it there. No baseline discontinuity,
|
||
no "before vs. after" comparison problem — there is nothing to reconcile.
|
||
3. ~~**What transfers, from whom, on every dispatch — and its cost.**~~ **RESOLVED
|
||
2026-08-05 — a reservoir, not a fan-out, keeping the transfer O(1).**
|
||
`vm_physics_touch()`'s proportional pull across every other live VM (`capsule_vm_physics.c
|
||
:281-355`) is O(n) over the fleet and is explicitly justified there only because fleet
|
||
touches are rare — the file's own comment (`:47-49`) contrasts "dozens to low hundreds" of
|
||
fleet touches against word executions "in the millions." Copying that shape for words is
|
||
not viable.
|
||
|
||
Instead, each VM's inner Stadium gets one additional scalar — the **reservoir** — holding
|
||
whatever heat is not currently claimed by a resident patron. All word-heat transfers are
|
||
two-party, against the reservoir, mirroring Hera's structural role at the fleet level (a
|
||
single fixed point that absorbs and donates) rather than the fleet's peer-to-peer fan-out:
|
||
- **Touch** (dispatch of an already-resident word): pull a fixed Q48.16 quantum from the
|
||
reservoir into the word's cell, clamped at what the reservoir holds. O(1).
|
||
- **Cooling** (Loop #3's decay shape, redirected): return heat from the cell to the
|
||
reservoir instead of letting it vanish. O(1) per word, same as today's independent decay.
|
||
- **Eviction:** the cell's *remaining* heat must flow back to the reservoir before the cell
|
||
returns to the free list (item 3.7) — otherwise conservation breaks on every reap.
|
||
- **Quantum size:** a Kconfig constant, not an inferred rate. The fleet needed a
|
||
statistical estimator (`VMFleetWindow`, `vm_physics_tick()`) because its touches are rare
|
||
and irregular; words already have a simpler precedent — `execution_heat`'s existing
|
||
per-dispatch increment is a flat `+1`, not tick-scaled. Mirroring that shape avoids a
|
||
second estimator. Actual tuning is DoE work (item 5.1), not decided here.
|
||
|
||
**Admission is the starter grant, by explicit choice (2026-08-05) — `execution_heat`
|
||
plays no role.** A non-resident word has no cell, so its density is 0 and it can never win
|
||
item 3.5's "denser than the least-dense resident" comparison on its own. Two shapes were
|
||
weighed: (A) gate admission attempts on `execution_heat`'s existing threshold crossing —
|
||
free, since the increment already happens, but makes `execution_heat` the promotion
|
||
governor in kernel builds, directly against the "one governor per build" rule below; or
|
||
(B) every dispatch of a non-resident word requests a fixed starter quantum from the
|
||
reservoir and is admitted iff that quantum's density beats the current least-dense
|
||
resident — `execution_heat` stays fully inert, matching the rule as already committed.
|
||
**Chosen: (B).**
|
||
|
||
**Correction (2026-08-05): the cost below was stated wrong.** An earlier draft of this
|
||
paragraph took item 3.5's own commit note — written before item 3.7 — at face value
|
||
instead of reading `stadium_admit()` as it stands today (`stadium.c:312-381`). The free
|
||
list landed with item 3.7 and **is the primary path**: an O(1) pop, no scan, no
|
||
comparison. The O(N) fallback only runs once a VM's own free list is exhausted, and even
|
||
then it scans only that VM's own resident cells (`stadium_owner[i] != slot`), never the
|
||
global array. Option B is O(1) in the common case — every admission attempt, for as long
|
||
as the touched VM's Stadium floor has free capacity — and only degrades once that VM's
|
||
floor is genuinely full, which is exactly when a real ranking decision (not a workaround)
|
||
is the correct thing to be paying for. Better-justified than the original draft, not
|
||
merely corrected.
|
||
4. ~~**What happens to `dict_hash` and parity comparisons that predate this change.**~~
|
||
**RESOLVED by #2 above** — nothing predates a change that isn't being made to the hashed
|
||
field.
|
||
5. ~~**A new "L9" loop, or composes into an existing one.**~~ **RESOLVED — composes into L0.**
|
||
The Stadium engine (§18) already owns a conserved heat wire per cell; item 4.1 populates
|
||
that existing wire for the word patron kind. It is not a new loop and needs no name.
|
||
|
||
**What sums to what, and admission semantics — settled by code already written, plus the
|
||
reservoir above:** per-VM Stadium, one pool per VM (words, blocks, ACLs, messages together,
|
||
not a word-only sub-pool) — matching §21.4's "K conserved here, independently" and the
|
||
`stadium.h:64` field comment. **Correction to this section's 2026-08-05 earlier wording:**
|
||
the invariant is not "residents sum to `Q48_ONE`" — the reservoir holds whatever residents
|
||
haven't claimed, so the correct invariant is
|
||
|
||
> Σ(resident patron heat) + reservoir == `Q48_ONE`
|
||
|
||
checked the same way `vm_physics_conserved()` checks the fleet sum, epsilon-bounded. No reset
|
||
on admit/evict: the total stays invariant across *any* call, so admission and eviction are
|
||
transfers against the reservoir, never a reset — mirroring `capsule_vm_physics.c`'s VM-birth
|
||
pattern (a new patron starts at 0, topped up by transfer) with the reservoir playing Hera's
|
||
role: at VM-Stadium-quota-grant time, before any word patron is resident, the reservoir holds
|
||
the VM's entire share, exactly as Hera holds the fleet's entire `Q48_ONE` before any other VM
|
||
is born.
|
||
|
||
**One governor per build — states explicitly what closes the §11/§25.5 "never two live heat
|
||
mechanisms" gap:**
|
||
|
||
- **Kernel builds:** `execution_heat` stops being a *decision input* once item 4.1 lands — it
|
||
keeps incrementing, decaying, and getting hashed exactly as today (ENTROPY@, ACL words,
|
||
diagnostics, `dict_hash` all keep working unchanged), but it no longer governs residency.
|
||
Stadium `heat`/density governs Stadium residency instead.
|
||
- **Hosted builds: unchanged**, per §17.3's own resolution — no Stadium exists there,
|
||
`execution_heat` keeps governing the old cache exactly as it does today.
|
||
|
||
This is the same per-build split §17.3 already ruled for the cache itself; word-level heat
|
||
conservation follows it rather than inventing a second shape.
|
||
|
||
**Open, deferred honestly rather than blocking:**
|
||
|
||
- The quantum size (Kconfig constant, §17.7 bullet 3 above) has no value yet — tuning is DoE
|
||
work (item 5.1), not invented here, same treatment as `STADIUM_MEMORY_PERCENT` (item 3.2).
|
||
- Whether `rolling_window_seed_hotwords_cache()`'s POST warm-start
|
||
(`rolling_window_of_truth.c:786`) needs a Stadium-side counterpart to seed word patrons'
|
||
initial `heat` distribution from the reservoir — noted here as the natural seeding site,
|
||
not designed. Item 4.1 may ship without it; POST warm-start of the *old* cache is unaffected
|
||
either way since it writes `execution_heat`, which stays untouched.
|
||
- `stadium_admit()`'s O(N) scans (item 3.5's own recorded debt) are accepted cost for word
|
||
admission under Option B, not re-litigated here. They resolve when the free list (item 3.7)
|
||
supersedes the full-array scan — tracked at item 3.5, not a new item.
|
||
|
||
**This section now authorizes item 4.1 to wire word patrons onto the Stadium using: the
|
||
reservoir-based O(1) touch/cool transfer, Option B's starter-grant admission (no
|
||
`execution_heat` involvement), and the corrected invariant above. `execution_heat`'s current
|
||
increment/decay behaviour and `dict_hash` remain explicitly out of scope — nothing in item
|
||
4.1 touches either.**
|
||
|
||
#### Two rulings made during item 4.1's implementation, 2026-08-05
|
||
|
||
A pre-coding design pass surfaced two problems this section had not accounted for. Both were
|
||
taken to Captain Bob before any file was touched; both are now closed.
|
||
|
||
1. **Cell-0 panic hazard.** `stadium_boot_init()` grants Hera's quota with `free_head = 0` so
|
||
the first-ever admission pops cell 0 — documented as preserving item 3.6's "Hera is
|
||
patron zero." But nothing had ever actually birthed Hera into the Stadium; item 4.1's
|
||
first word dispatch would have made an ordinary, evictable word the accidental occupant
|
||
of cell 0, arming `stadium_evict()`'s hard panic guard for the day something tried to
|
||
reap it. **Ruled: birth Hera for real, as part of item 4.1** (a deliberate scope addition,
|
||
not silently folded in) — `stadium_birth_hera()` admits a pinned, zero-heat, mass-1
|
||
candidate into cell 0 before anything else can reach it. Zero heat means no reservoir
|
||
transfer is needed for her admission; conservation holds trivially at boot.
|
||
2. **Quantum/cool-rate underspecification.** The quantum this section names as
|
||
Kconfig-tunable had no defensible starting value, and the cooling coefficient wasn't
|
||
named as a *fraction of the patron's own current heat per tick* until this pass — the
|
||
naive reading (reusing `execution_heat`'s flat per-tick decay shape directly) can zero a
|
||
cell in one tick, since Q48_ONE (65536) is a much smaller number than it looks at a
|
||
glance. **Ruled: two new Kconfig knobs**, `STADIUM_WORD_HEAT_QUANTUM` (default 2048 =
|
||
Q48_ONE ÷ `HOTWORDS_CACHE_SIZE`, i.e. one "cache slot's worth" of the mechanism this item
|
||
retires) and `STADIUM_WORD_COOL_RATE_Q48` (default 21845, reusing
|
||
`INITIAL_DECAY_SLOPE_Q48`'s numeric value but reinterpreted as a fraction-of-current-heat
|
||
removed per tick, unit-safe for a conserved share — NOT the same quantity as
|
||
`execution_heat`'s decay, just a reasonable starting magnitude borrowed from it). Both
|
||
flagged in their Kconfig help text as untuned placeholders, DoE work for item 5.1, same
|
||
treatment as `STADIUM_MEMORY_PERCENT`.
|
||
|
||
**Noted in passing, not fixed:** Kconfig/`menuconfig` itself has never been exercised
|
||
end-to-end in this repo — every knob added so far, including these two, has only been
|
||
verified via its `Makefile.starkernel` default, never through an actual `menuconfig` →
|
||
`.config` → build round trip. Filed at §25.7.
|
||
|
||
**Also found, reported not fixed (§25.7):** `stadium_admit()` never writes
|
||
`stadium_owner[idx]` on either the free-list-pop or the eviction-fallback path. Harmless
|
||
today — every cell's owner byte is already `0` (Hera) from `stadium_boot_init()`, and Hera is
|
||
the only VM with a quota — but once item 4.2 restores Hermes, a resident's evict-credit would
|
||
flow to the wrong VM's reservoir unless this is fixed first.
|
||
|
||
---
|
||
|
||
## 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 — RESOLVED by item 1.6
|
||
|
||
**RESOLVED 2026-08-04.** What follows was written as a proposal; it is confirmed here rather
|
||
than rewritten, because everything since has already been treating it as decided. §22's
|
||
elasticity mechanism (DECIDED) only means something if a VM's mass is its variable quota —
|
||
"capacity flows down the density gradient" (§22.1) is vacuous if every VM's mass were pinned
|
||
at one cell. §24.3 already states outright that "a VM's mass is elastic by §22." Items 1.2
|
||
through 1.5 (the resting floor, the transfer trigger, the timescale ratio, the outer bound)
|
||
all already read mass-as-quota as given. §20.5 #2's own framing settles it independently:
|
||
the one-cell alternative "throws away the distinction" in the table below, which is the
|
||
entire reason for doing this. **A VM's mass is the capacity share — the quota — Hera
|
||
allocated it**, not a fixed one-cell footprint regardless of size.
|
||
|
||
Decided on paper, not yet built: `VMPhysics` currently holds only `execution_heat_q48`,
|
||
`last_active_ns` and `is_live` (`capsule_vm_physics.c:59-63`). There is no share field yet —
|
||
adding one is implementation work for a later phase, not this item.
|
||
|
||
§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.**~~ **RESOLVED by item 1.5 (§25.2), 2026-08-04.** What is
|
||
the outer Stadium's capacity, and what happens at the bound — birth refused, or coldest
|
||
VM reaped?
|
||
|
||
**Correction first: "coldest reaped, consistent with §19.3" does not survive §20.2.**
|
||
§19.3's admission rule is *admit if denser than the least dense resident*. §20.2 already
|
||
decided every VM but Hera is born at heat zero. A newborn can never be denser than an
|
||
existing warm VM, so applying §19.3 literally at the outer level means births at the
|
||
bound would fail regardless — just silently, via a comparison that can never succeed,
|
||
instead of by an explicit refusal. Treating "coldest reaped" as automatic would also
|
||
require a bespoke, non-density rule that exists for VMs alone, which is exactly the
|
||
per-kind special case §11 warns against.
|
||
|
||
**Resolution: birth is refused at the bound.** Making room is Hera's own deliberate act —
|
||
she already reaps VMs (§20.1) — never an automatic side effect of someone else's birth
|
||
request. This is the explicit, stated behaviour the original text asked for.
|
||
|
||
**The bound itself: 4, Kconfig-tunable, explicitly a placeholder.** 4 matches Tripod's
|
||
own currently-known topology (Hera + two Hermes instances + Artemis) — the smallest
|
||
number that doesn't already contradict what this system is known to need, not a padded
|
||
estimate. It is expected to be too small for real workloads. The right way to find an
|
||
idealized default is empirical — a DoE campaign, the same discipline already used
|
||
elsewhere in this project (`experiments/bare_metal/`) — not a second guess made on paper.
|
||
Tracked as future work, not invented here. The constant is a Kconfig symbol (e.g.
|
||
`STADIUM_MAX_VM_COUNT`, named at implementation time in item 3.1 alongside the other new
|
||
symbols this phase introduces), not hardcoded.
|
||
|
||
**Fixed for the machine's lifetime once set at build** — resolves §22.5 #4 below in the
|
||
same stroke. The outer total does not itself flex at runtime; only per-VM quotas do
|
||
(§22). An outer bound that could grow or shrink live would mean §2's "inescapable wall"
|
||
is not actually inescapable.
|
||
2. ~~**Is a VM's mass its allocated share, or one cell?**~~ **RESOLVED by item 1.6 — the
|
||
allocated share.** See §20.4.
|
||
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?**~~ **RESOLVED by item 1.7 (§25.2), 2026-08-04.**
|
||
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 bounded deliberately, since the boot order in
|
||
§6 does not forbid it.
|
||
|
||
**Not the same question as §8's `contains` chains (item 1.1)** — those are same-Stadium
|
||
patron-holds-patron relationships, bounded to depth 5, and do not create a second
|
||
Stadium. This is specifically about a patron *being* a VM with its own nested Stadium
|
||
underneath it.
|
||
|
||
**Resolution: bounded by a Kconfig-tunable cap, default 2 — not a hard "never."**
|
||
Consistent with how item 1.1 treated its own depth question rather than declaring a
|
||
permanent architectural prohibition. 2 matches what §21 already decided and what already
|
||
exists: the outer Stadium (patrons: VMs) and each VM's own inner Stadium (patrons: words,
|
||
blocks, ACLs, messages). Nothing today drives a third level, so 2 is the honest default,
|
||
not a padded estimate. The cap is enforced explicitly at VM-birth time — birthing a VM
|
||
whose own Stadium would sit at a depth beyond the configured cap is refused, the same
|
||
"explicit refusal over silent/emergent behaviour" discipline item 1.5 used for the outer
|
||
bound — rather than left as an unstated assumption nothing checks.
|
||
|
||
---
|
||
|
||
## 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.
|
||
|
||
**RESOLVED by item 1.4 (§25.2), 2026-08-04 — 1000:1, grounded in an existing precedent, not
|
||
picked from nothing.** `capsule_vm_physics.c:434-441`'s `vm_physics_heartbeat_tick()` already
|
||
runs a fleet-level slow loop at `HEARTBEAT_INFERENCE_FREQUENCY` virtual ticks (default 1000,
|
||
`starforth_config.h:72`) to recalibrate `fleet_transfer_slope_q48` — the rate `vm_physics_touch()`
|
||
uses for heat transfers. Different mechanism (heat-transfer-rate recalibration, not
|
||
capacity/mass transfer), but the identical shape item 1.3's capacity-tick needs: a coarse,
|
||
fleet-level reassessment layered over the fine virtual tick, in the same file, same
|
||
subsystem.
|
||
|
||
The capacity-tick gets its **own** named constant rather than literally sharing
|
||
`HEARTBEAT_INFERENCE_FREQUENCY` — they are conceptually separate concerns (inference-engine
|
||
window/decay tuning versus capacity arbitration), and coupling them would mean retuning one
|
||
silently retunes the other. But its **default is 1000**, matching this precedent rather than
|
||
inventing an unrelated number. 1000:1 against the virtual tick is comfortably past §12 Q5's
|
||
"order of magnitude apart" minimum. Named and made a Kconfig symbol at implementation time
|
||
(item 3.1), same tunable-knob convention as item 1.1's containment-depth cap.
|
||
|
||
### 22.5 Open
|
||
|
||
1. ~~**The resting floor.**~~ **RESOLVED by item 1.2 (§25.2), 2026-08-04.** 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.
|
||
|
||
**Floor = max(mass of pinned patrons, one message-sized cell).** The first term is the
|
||
principled alternative this section already named: derived, not tuned. The second term
|
||
closes a gap the first term leaves open on its own — a VM with zero pinned patrons would
|
||
otherwise get a floor of zero, and a VM with zero quota cannot receive anything, including
|
||
the message that would be the reason for it to wake up and regrow via §22.1's
|
||
density-gradient feedback. That is a deadlock: no capacity to receive, no way to ever
|
||
regain capacity. One message-sized cell is itself derived, from §23.3's cell sizing rule
|
||
("size the cell so a typical message is exactly one cell"), not a second tuned constant —
|
||
so the discipline this section wanted to preserve still holds with both terms in place.
|
||
2. ~~**What arbitrates a transfer, concretely?**~~ **RESOLVED by item 1.3 (§25.2),
|
||
2026-08-04.** §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.
|
||
|
||
**The cadence is the slow part, not a threshold.** Hera evaluates the density gradient
|
||
once per **capacity-tick** — a coarser, derived multiple of the virtual tick (§18.4). The
|
||
exact multiple is item 1.4's job, not fixed here. This is what gives "sustained density"
|
||
(§22.4) its actual meaning: anything shorter-lived than one capacity-tick interval cannot
|
||
trigger a transfer, without needing a magnitude threshold layered on top.
|
||
|
||
**Whether to act, once she looks, is a pure comparison — no tuned threshold.** At each
|
||
capacity-tick, Hera finds the single densest and single least-dense live VM. If they
|
||
differ at all, a transfer is eligible. This is the same shape as §19.3's admission rule
|
||
("denser than the least dense resident") — a comparison of two intrinsic numbers, not a
|
||
policy, so nothing needs inventing here.
|
||
|
||
Both halves satisfy the tick-expressibility constraint item 1.3 states: the cadence is a
|
||
tick multiple, and the decision itself reads only heat and mass, never wall time.
|
||
|
||
**What this does not resolve:** how much capacity moves per eligible transfer. §22.3 only
|
||
says the mechanism is "arithmetic on two integers"; neither this section nor item 1.3
|
||
pins down the amount. Reported rather than invented — it can become its own item if
|
||
warranted, but is out of this item's scope.
|
||
3. ~~**The exact timescale ratio**~~ **RESOLVED by item 1.4 — 1000:1.** See §22.4.
|
||
4. ~~**Does the outer Stadium's own capacity ever change?**~~ **RESOLVED by item 1.5 —
|
||
no.** §22 makes per-VM quotas elastic within a fixed total; the total itself is fixed for
|
||
the machine's lifetime, set once at build via the Kconfig bound §20.5 #1 introduces. See
|
||
§20.5 #1 for the full argument.
|
||
|
||
---
|
||
|
||
## 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 and gives the `contains` wire item
|
||
1.1 resolved to somewhere to live — a 4-byte index, the same width as `link`. (The
|
||
header/continuation discriminator does not compete for this space: item 3.1 ruled it an
|
||
external side bitmap, not a header field — see §3's amendment.) Whether 4 bytes is the
|
||
final byte count item 3.1 settles on for `contains`, or whether it can shrink, is exactly
|
||
the kind of thing item 3.1's real byte count settles, not this section — flagged here
|
||
rather than assumed. 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.
|
||
|
||
#### The continuation cell — RESOLVED by item 1.12, linked
|
||
|
||
**RESOLVED 2026-08-04.** An earlier draft stated a 1024-byte block is "17 cells: 1 header +
|
||
16 payload." That figure assumed continuation cells are contiguous and carry nothing but
|
||
bytes — an assumption this section settles rather than leaves open.
|
||
|
||
**Linked, not contiguous — forced by what §22.3 already decided, not a fresh 50/50 choice.**
|
||
§22.3's per-VM free list (DECIDED) draws cells individually, with no adjacency guarantee.
|
||
Guaranteeing contiguous runs for multi-cell patrons would mean changing that allocator to
|
||
find runs rather than pop a free-list head, which reintroduces exactly the fragmentation §3
|
||
and §13 already ruled out by choosing fixed-size, index-linked cells in the first place. The
|
||
allocator that exists says linked; contiguous would require an allocator that does not.
|
||
|
||
**Consequence for sizing:** each continuation cell carries a 4-byte next-index alongside its
|
||
payload, leaving **60 bytes usable** out of the 64-byte cell. A 1024-byte block needs **18
|
||
continuation cells** at 60 usable bytes each, not 16 at a full 64 — the same figure this
|
||
section's earlier draft flagged as the linked-form cost without yet choosing it. §23.3's
|
||
sizing table is now complete on this row.
|
||
|
||
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?**~~ **RESOLVED by item 1.10
|
||
(§25.2), 2026-08-04 — no, it cannot be elided.** 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.
|
||
|
||
**It cannot be, and the reason is a genuine conflict, not just difficulty.** Two ways to
|
||
elide it, both blocked:
|
||
|
||
- **Elide it only for kinds that don't need it** (messages) while keeping it for kinds
|
||
that do (words, blocks). This is exactly the per-kind branch §18.3 forbids — the
|
||
engine, or something reading the header, would have to know a message's header is
|
||
shaped differently than a word's, which reintroduces the type-field problem §3 exists
|
||
to prevent.
|
||
- **Elide it everywhere, uniformly.** This breaks the kinds that genuinely need it: a
|
||
word is resolved by name, not by Stadium position — `vm_dict_resolve_in_bucket()`
|
||
looks up by name — and a block is resolved by LBN, not by Stadium position either. The
|
||
Stadium index is not a substitute for either; they are different addressing schemes
|
||
serving different lookups.
|
||
|
||
So the saving is not reachable without violating either §18.3's uniformity requirement or
|
||
a lookup mechanism a patron kind already depends on outside the Stadium. `identity` stays
|
||
a fixed, always-present 8-byte header field for every kind, whether or not a given kind's
|
||
own logic makes use of it.
|
||
|
||
**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. (Settled by
|
||
item 1.12 — see §23.4 #4 — reinforcing that identity stays untouched by that encoding.)
|
||
|
||
4. ~~**The continuation-cell encoding.**~~ **RESOLVED by item 1.12 — linked.** See §23.3's
|
||
"The continuation cell" subsection: forced by §22.3's already-decided disjoint free list,
|
||
not a fresh choice. 4-byte next-index, 60 usable bytes per continuation cell, 18
|
||
continuation cells for a 1024-byte block. Item 3.1 is unblocked on this item.
|
||
|
||
---
|
||
|
||
## 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?**~~
|
||
**RESOLVED by item 1.8 (§25.2), 2026-08-04.** 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, and the hand-off is: the new hash is computed **exactly
|
||
once, at the migration boundary**, as part of the block's `MIGRATE` code field —
|
||
consistent with §24.4 (a resident block's identity is its handle/LBN, never its content
|
||
hash) and §17.2 (migration is the block's departure event, not destruction). Nothing
|
||
about a resident block's identity changes mid-residency regardless of how many times its
|
||
content mutates; the hash is a warehouse-side fact computed only when the block actually
|
||
leaves.
|
||
|
||
**Whether the old hash is retained anywhere for audit is out of scope here.** §5 draws
|
||
this boundary already: the warehouse is beneath the Stadium, and the Stadium does not do
|
||
content addressing — the warehouse does. Audit retention is an Artemis-layer policy
|
||
question, not a Stadium one, and inventing an answer for it here would cross that
|
||
boundary rather than respect it.
|
||
2. ~~**Does redefining a word while its old definition is resident leave two patrons?**~~
|
||
**RESOLVED by item 1.9 (§25.2), 2026-08-04 — confirmed, yes.** Not a design choice, a
|
||
factual check: `vm_dict_resolve_in_bucket()` (`dictionary_management.c:257`) walks a
|
||
bucket chain and returns the newest match — "the newest visible definition wins
|
||
(FORTH-79 shadowing)" (`:266`). Nothing in the redefinition path unlinks or frees the
|
||
superseded `DictEntry`; it stays in the bucket, merely shadowed. So if both the old and
|
||
new definitions are hot, both are correctly on the floor, both have mass, both are
|
||
ranked independently. This is the right behaviour, not an artefact to work around — they
|
||
are genuinely two different words with two different execution histories.
|
||
|
||
---
|
||
|
||
# 25. The punch list
|
||
|
||
**This section is authoritative for what is done and what is not.** Sections 1–24 are the
|
||
design. This is the work.
|
||
|
||
---
|
||
|
||
## 25.0 How to implement this punch list
|
||
|
||
**Read this subsection every time before touching an item. Do not skip it because it was
|
||
read earlier in the session.**
|
||
|
||
### The rules
|
||
|
||
1. **One item at a time.** Take the lowest-numbered unchecked item whose prerequisites are
|
||
met. Finish it completely. Do not begin a second item while one is in progress.
|
||
|
||
2. **Do not jump ahead.** Do not start a later item because it seems easy, related, or
|
||
convenient. Do not do "while I'm in here" work. If a later item looks like it should be
|
||
reordered, say so and wait for an answer — do not reorder unilaterally.
|
||
|
||
3. **Do not increase scope.** Do exactly what the item says. If the item says "write the
|
||
trap entry," write the trap entry — not the trap entry plus a refactor of the file it
|
||
lives in. Anything you notice that is not in the item gets **reported**, not fixed.
|
||
This includes obvious bugs. Report them; they get their own item if they warrant one.
|
||
|
||
4. **Do not fabricate, confabulate, or conflate.** If you do not know how something works,
|
||
read it. If you cannot determine it by reading, **stop and say so**. Never invent a
|
||
function, a register name, a constant, a FORTH word, or an API that you have not
|
||
verified exists in this tree or in the relevant hardware manual. Never guess at a value
|
||
and present it as known. Never merge two things that are similar into one thing that is
|
||
neither. A wrong answer stated confidently has cost this project git resets before.
|
||
|
||
5. **When blocked, stop.** Report exactly what is blocking, what was tried, and what is
|
||
needed. Do not work around it silently. Do not substitute a different approach and
|
||
carry on.
|
||
|
||
6. **Acceptance is not optional and not negotiable.** Each item states *Done when*. An item
|
||
is not done until that exact condition is met and observed. Not "should work," not
|
||
"compiles cleanly" unless that is what the item says. If acceptance requires the
|
||
three-architecture QEMU boot, then all three have booted and their logs exist.
|
||
|
||
7. **Report failures honestly.** If a test fails, say it failed and show the output. If a
|
||
step was skipped, say it was skipped and why. Never describe partial work as complete.
|
||
|
||
### The commit discipline
|
||
|
||
Every checked-off item gets **its own commit**, and that commit contains:
|
||
|
||
- the code or document change for that item, and
|
||
- this file, with that item's checkbox changed from `[ ]` to `[x]`.
|
||
|
||
Nothing else. One item, one commit. The punch list and the tree move together, so the
|
||
document is never a claim about work that is not in the branch.
|
||
|
||
Commit message format:
|
||
|
||
```
|
||
<area>: <what the item did> e.g. riscv64: real trap entry with SRET return
|
||
|
||
Punch list §25 item <id> complete.
|
||
<one or two lines on what was actually verified, not what was intended>
|
||
|
||
Co-Authored-By: <the implementing model's attribution line, per its harness>
|
||
```
|
||
|
||
### Standing constraints from `.claude/CLAUDE.md`
|
||
|
||
These override anything convenient:
|
||
|
||
- **Never create a branch without explicit permission.** Work on the branch you are on.
|
||
- **Never stash.** If the tree is dirty, report it and wait.
|
||
- **Never apply a fix that was not requested.** Report it instead.
|
||
- **Acceptance for any kernel change is the three-architecture QEMU boot.** There is no
|
||
other test. The hosted `make` build is compile-sanity only.
|
||
- **One QEMU instance at a time, foreground, `clean` before `qemu`.** Concurrent runs
|
||
corrupt the timing signal.
|
||
- **Read `experiments/bare_metal/README.md` in full before editing any `.4th` file**, and
|
||
verify capsule edits with `mkcapsule --lint` rather than counting bytes by hand.
|
||
|
||
### When an item is genuinely wrong
|
||
|
||
The design is not sacred. If implementing an item shows the design is wrong, **stop, report
|
||
what the code demonstrated, and propose the amendment.** Amend the relevant section of this
|
||
document first, get agreement, then continue. Do not implement something you believe is
|
||
wrong because it is written down, and do not silently implement something different.
|
||
|
||
---
|
||
|
||
## 25.1 Phase 0 — Substrate
|
||
|
||
*Nothing in later phases can start until Phase 0 is complete. The engine has nothing to run
|
||
on until there is a tick on all three architectures (§16.1, §16.5).*
|
||
|
||
- [x] **0.1 — Prune `capsules/init.4th` to Hera alone.**
|
||
**Delete** blocks 2051, 2052, 2053, 2054, 2055, 2056, 2058, 2059 — the readiness
|
||
handshake, broadcast test, TRIPOD-TEST, HERMES-E2E, and fleet-DoE scaffolding.
|
||
**Edit** the three surviving blocks: 2057 (`BOOT-BANNER` — drop the Tripod lines), 2049
|
||
(remove the Artemis and Hermes births with their `CD-INIT` calls and the `common:msg.4th`
|
||
/ `process.4th` loads; keep `lib.4th`; adjust `VM-TREE` / `VM-CHILDREN`), and 2050 (keep
|
||
the `BOOT-BANNER` call; remove the `READINESS-HANDSHAKE` and `BROADCAST-TEST` calls).
|
||
Leave `capsules/hermes/` and `capsules/artemis/` untouched on disk. An earlier draft of
|
||
this item said "remove blocks 2050–2059," which contradicted its own Refs line — 2050
|
||
survives, edited (C1).
|
||
*Done when:* all three architectures boot to the prompt with Hera alone, no Hermes or
|
||
Artemis in the banner, and the three logs exist under `logs/`.
|
||
*Refs:* the surviving blocks are 2057, 2049, 2050. `mkcapsule --lint` before building.
|
||
|
||
- [x] **0.2 — riscv64: real trap entry.**
|
||
Replace the one-way `riscv64_trap_entry` in `arch/riscv64/isr.S` with save / dispatch /
|
||
restore / `sret`. Route `scause` bit 63 + cause 5 to the timer path; everything else keeps
|
||
falling through to the existing fatal handler.
|
||
**FP state is not optional (B2 verified):** the kernel builds `-march=rv64gc -mabi=lp64d`
|
||
(`Makefile.starkernel:162`) — hard-float ABI, and kernel code genuinely uses doubles
|
||
(`hotwords_stats_print`). The trap entry must save the ABI's caller-saved FP registers
|
||
plus `fcsr` alongside the integer set; verify the exact register list against the RISC-V
|
||
psABI, not this document. Do not "fix" this by switching to soft-float — that breaks
|
||
existing code and is a build-system decision nobody has made.
|
||
*Done when:* riscv64 boots to the prompt with no regression, and exceptions still halt
|
||
with the same diagnostic as before. **No trap source exists yet at this item** — the
|
||
timer arms in 0.3, whose tick-advance acceptance is what proves this entry path took and
|
||
returned an interrupt (C2). Do not arm the timer early to manufacture evidence here.
|
||
|
||
- [x] **0.3 — riscv64: SBI timer and real time base.**
|
||
**First, the prerequisite this item silently assumed (B1 verified it absent):** the
|
||
kernel has no DTB access — `BootInfo` (`uefi.h:624-639`) carries no FDT pointer and no
|
||
FDT code exists in the tree. Capture the DTB pointer from the EFI configuration table
|
||
(DTB table GUID) into a new `BootInfo` field in the shared loader. This also serves 0.6.
|
||
Then: arm the timer via the SBI TIME extension, **enable `sie.STIE`**, and **re-arm
|
||
inside the handler on every tick — the SBI timer is one-shot by nature, and a missed
|
||
re-arm stops the heartbeat forever with no error. That is the single most likely silent
|
||
failure of this item (C3).** Switch the time base from `rdcycle` to the `time` CSR and
|
||
take its frequency from the device tree `timebase-frequency`, with a named fallback
|
||
constant — not a bare magic number (§16.2).
|
||
*Done when:* `heartbeat_ticks()` advances on riscv64 and the tick interval matches the
|
||
configured rate within measurement noise. Verify the SBI extension is present before
|
||
relying on it; if it is absent, stop and report rather than falling back silently.
|
||
|
||
- [x] **0.4 — aarch64: determine the exception level at runtime.**
|
||
Read `CurrentEL` once, early, and let it govern **everything EL-dependent**, not just the
|
||
timer (B3): the vector base register (`VBAR_EL1` vs `VBAR_EL2` — today's `isr.S` writes
|
||
`VBAR_EL1` unconditionally, which is never consulted for exceptions taken at EL2), the
|
||
saved-state pair (`ELR_ELx`/`SPSR_ELx`), and the timer register set (`CNTP_*_EL0` vs
|
||
`CNTHP_*_EL2`). Do not hardcode either level anywhere.
|
||
*Done when:* the boot log states which EL was detected, on real QEMU output.
|
||
|
||
- [x] **0.5 — aarch64: IRQ vector split.**
|
||
Split `irq_spx` out of the shared fatal handler in `arch/aarch64/isr.S`: save `x0`–`x30`
|
||
plus the saved-state registers (see B3 note below), call a C handler, restore, `eret`.
|
||
The other fifteen vectors are unchanged. Note the 128-byte slot limit — the save sequence
|
||
will not fit inline and must branch to a trampoline.
|
||
**FP state is not optional (B2 verified):** the kernel builds without
|
||
`-mgeneral-regs-only` (`Makefile.starkernel:146`), so the compiler may use SIMD registers
|
||
anywhere. Save the ABI's caller-saved SIMD set plus `FPSR`/`FPCR` alongside the integer
|
||
set; verify the exact list against the AAPCS64, not this document.
|
||
**EL governs the whole path (B3):** this item previously hardcoded `ELR_EL1`/`SPSR_EL1`,
|
||
while 0.4 refuses to hardcode the EL — and today's `isr.S` installs `VBAR_EL1`, which is
|
||
never consulted for exceptions taken at EL2. The EL detected in 0.4 must select the
|
||
vector base register (`VBAR_ELx`), the saved-state pair (`ELR_ELx`/`SPSR_ELx`), and the
|
||
`eret` target state, not just the timer registers.
|
||
*Done when:* aarch64 boots to the prompt with no regression. **No IRQ source exists yet
|
||
at this item** — the GIC lands in 0.6 and the timer arms in 0.7, whose tick-advance
|
||
acceptance is what proves this path took and returned an IRQ (C2). Do not pull 0.6/0.7
|
||
work forward to manufacture evidence here.
|
||
|
||
- [x] **0.6 — aarch64: minimal GICv2.**
|
||
Enable the distributor and CPU interface, set the priority mask, enable the timer PPI,
|
||
acknowledge via `IAR` / `EOIR`. **Read the base addresses and the PPI INTID from the
|
||
device tree — do not take them from memory or from this document.** The DTB pointer
|
||
comes from the `BootInfo` field added in 0.3 (B1 verified no such field existed). If the
|
||
DTB turns out to be unreachable on aarch64 EDK2, stop and report — deciding between
|
||
loader work and named QEMU-virt constants with a recorded caveat is Captain Bob's call,
|
||
not the implementer's.
|
||
|
||
> **DTB confirmed unreachable (checked live, 2026-08-03) — same finding as riscv64.**
|
||
> `fdt_valid(boot_info->dtb)` fails on this system's aarch64 build too (installed
|
||
> firmware: `qemu-efi-aarch64` 2025.11-3ubuntu7, no alternate available). Ruling: named
|
||
> QEMU-virt constants, verified rather than recalled — `qemu-system-aarch64
|
||
> -machine virt,dumpdtb=...` was used to dump QEMU's own internal devicetree (the one
|
||
> EDK2 fails to forward) and decoded with this tree's own `fdt.c` reader, giving
|
||
> **GICD 0x08000000, GICC 0x08010000** (both confirmed for this exact QEMU 10.2.1
|
||
> build, not assumed stable across versions) and **PPI 30** for the non-secure EL1
|
||
> physical timer (bonus finding: PPI 26 for the EL2 hypervisor timer, for item 0.7's
|
||
> EL2 path). Register *offsets* (GICD_CTLR, GICC_IAR, etc.) are architectural, not
|
||
> board-specific, and were cross-checked against
|
||
> `/usr/src/linux-headers-*/include/linux/irqchip/arm-gic.h` rather than recalled.
|
||
|
||
> **Acceptance corrected — same defect C2 already fixed for items 0.2 and 0.5, missed
|
||
> here.** "The timer interrupt is delivered and acknowledged" cannot be observed within
|
||
> this item's own scope: nothing arms the timer until item 0.7's `apic_timer_start()`.
|
||
> As written this item could never be marked done on its own evidence. Acceptance is
|
||
> now the same shape as 0.2/0.5: GIC initialises without fault, IAR/EOIR path is wired
|
||
> into `aarch64_irq_handler()` and ready, boots with no regression. Item 0.7's
|
||
> tick-advance acceptance is what proves this path actually delivers and acknowledges an
|
||
> interrupt, exactly as 0.5 already defers to 0.7 for the same reason.
|
||
|
||
*Done when:* GIC distributor and CPU interface initialise without fault; the timer PPI
|
||
is enabled; `aarch64_irq_handler()` reads `IAR`, dispatches, and writes `EOIR`; boots to
|
||
the prompt with no regression. Scope is one interrupt; a general GIC driver is out of
|
||
scope and must not be written.
|
||
|
||
- [x] **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.
|
||
|
||
- [x] **0.8 — Converge the three architectures on one tick path, and make the physical
|
||
heartbeat adaptive.**
|
||
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.
|
||
|
||
**Per §26 (ruled):** the physical re-arm period is no longer a fixed 100 Hz constant.
|
||
`heartbeat.c` owns the current adaptive period (`heartbeat_set_adaptive_period_ns()` /
|
||
`heartbeat_next_period_ns()`); Loop #7's existing site in `vm_runtime.c` calls the setter
|
||
with its stable/volatile-derived value, rescaled to the 10 ms kernel base per §26.3 (not
|
||
the 10 µs hosted `HEARTBEAT_TICK_NS`); each architecture's re-arm function reads the
|
||
getter and converts to its own raw counter units instead of using a hardcoded period. No
|
||
new concurrency primitive — single writer (mainline), single reader (ISR), same shape
|
||
§21.1 already found free on one hart.
|
||
*Done when:* all three architectures drive the same TIME-TRUST bottom half; no loop math
|
||
runs in interrupt context; `vm_tick()`'s call sites are unchanged.
|
||
|
||
> **Live variation not directly observed.** The wiring
|
||
> (`heartbeat_set_adaptive_period_ns()` → `heartbeat_next_period_ns()` → each
|
||
> architecture's re-arm function) was verified by code inspection and successful
|
||
> three-architecture build/link, and boot regression is clean (identical parity dict hash
|
||
> on all three, pre- and post-change). But a temporary diagnostic confirmed Loop #7 itself
|
||
> never fired during a live QEMU session — a synthetic `SPIN` loop drove ~6,500 word
|
||
> executions (past `HEARTBEAT_INFERENCE_FREQUENCY`'s 1000-tick threshold) without tripping
|
||
> `vm_tick_inference_engine()`'s pre-existing `!vm->rolling_window.is_warm` gate
|
||
> (`vm_runtime.c:583`). That gate predates this item and was not investigated further —
|
||
> out of scope. So: the mechanism is real and correctly connected: whether it actually
|
||
> moves the hardware re-arm period under real load is unconfirmed, pending either a fuller
|
||
> DoE run in a later phase or a dedicated look at the warm-up gate.
|
||
*Refs:* §16.4 (as ruled), §18.4, §21.2, §26.
|
||
|
||
- [x] **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.
|
||
|
||
- [x] **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.
|
||
|
||
> **Observed 2026-08-04.** All three boot to `ok>`. Tick count at the point just before
|
||
> `sk_repl()` (a bounded wait for 3 real ticks was added at `kernel_main.c` — with none,
|
||
> the count landed on 1 (amd64) and 0 (riscv64) purely from how little wall time elapses
|
||
> between arming the timer and this print, which is not the same claim as "the heartbeat
|
||
> doesn't tick" and would have been a false negative to report as one): amd64 4,
|
||
> riscv64 3, aarch64 3. riscv64: `trust=0x00010000` (exactly `Q48_ONE`), `variance=0x0`.
|
||
> amd64: `dict_hash=0x3d4e1daf289da94f`, identical to the pre-item-0.8 baseline
|
||
> (`logs/20260803-231322`) — unchanged output, as the GAP-A1 control requires. Two
|
||
> consecutive amd64 boots (`logs/20260804-001948`, `logs/20260804-002021`) both produced
|
||
> `dict_hash=0x3d4e1daf289da94f` — reproducible, no wall-clock leakage into patron state.
|
||
> Logs committed: `logs/20260804-001727` (amd64), `logs/20260804-001805` (riscv64),
|
||
> `logs/20260804-001850` (aarch64), `logs/20260804-001948` / `logs/20260804-002021`
|
||
> (amd64 double-boot pair).
|
||
*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.*
|
||
|
||
- [x] **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.
|
||
|
||
> **RESOLVED 2026-08-04 — containment, not a lock.** A ninth wire, `contains` (§3): an
|
||
> index to the patron currently held inside this one, or none. Reap is **gated**, not
|
||
> density-derived — a patron with a non-none `contains` link cannot be reaped, full stop.
|
||
> Chains up to a depth cap, **default 5, exposed as a Kconfig symbol** (named at
|
||
> implementation time in item 3.1) rather than hardcoded — this project's existing
|
||
> tunable-knob convention. Unwinding is innermost-first, forced by the chain's own
|
||
> topology, not a policy choice — no FIFO/LIFO decision exists to make. Single occupant per
|
||
> level. Full argument in §8. **Same-Stadium relationship** — distinct from item 1.7's
|
||
> VM-tree-recursion question (§20.5 #4), which this does not resolve and remains open.
|
||
> Item 3.1 is now unblocked on this item; the ninth wire and the reserved header bytes
|
||
> (§23.3) are the concrete carry-forward.
|
||
|
||
- [x] **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.
|
||
|
||
> **RESOLVED 2026-08-04.** Floor = max(mass of pinned patrons, one message-sized cell).
|
||
> Both terms derived, neither tuned — the second closes a reachability gap the first term
|
||
> leaves open for a VM with nothing pinned (zero quota means it can never receive the
|
||
> message that would let it regrow). Full argument in §22.5 #1.
|
||
|
||
- [x] **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.
|
||
|
||
> **RESOLVED 2026-08-04.** Hera evaluates once per capacity-tick (a coarser, derived
|
||
> multiple of the virtual tick — the multiple itself is item 1.4). At each capacity-tick
|
||
> she finds the single densest and single least-dense live VM; if they differ at all, a
|
||
> transfer is eligible — a pure comparison, no tuned threshold, same shape as §19.3's
|
||
> admission rule. Cadence carries the "sustained density" requirement; the decision itself
|
||
> is a comparison. Both are tick-expressible, never wall-clock. **Not resolved:** how much
|
||
> capacity moves per transfer — reported, not invented, out of this item's scope. Full
|
||
> argument in §22.5 #2.
|
||
|
||
- [x] **1.4 — The heat/capacity timescale ratio.** The ordering is fixed (capacity slower);
|
||
the ratio is not. *Refs:* §22.4, §22.5 #3.
|
||
|
||
> **RESOLVED 2026-08-04 — 1000:1.** The capacity-tick gets its own named constant,
|
||
> defaulted to 1000 virtual ticks, matching the existing precedent at
|
||
> `capsule_vm_physics.c:434-441` (`vm_physics_heartbeat_tick()`'s
|
||
> `HEARTBEAT_INFERENCE_FREQUENCY`-gated fleet recalibration loop) rather than an invented
|
||
> number. Comfortably past §12 Q5's order-of-magnitude minimum. Kconfig-tunable at
|
||
> implementation (item 3.1). Full argument in §22.4.
|
||
|
||
- [x] **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.
|
||
|
||
> **RESOLVED 2026-08-04.** Bound = 4 (matches Tripod's known topology: Hera + 2 Hermes +
|
||
> Artemis), Kconfig-tunable, explicitly a placeholder pending a later DoE campaign to find
|
||
> an idealized default rather than a second guess made on paper. Fixed for the machine's
|
||
> lifetime once set at build. At the bound, **birth is refused** — not coldest-VM-reaped,
|
||
> which the original text called "consistent with §19.3" but which does not survive
|
||
> §20.2's cold-start birth rule (a newborn can never out-density an existing warm VM).
|
||
> Making room stays Hera's own deliberate act. Full argument in §20.5 #1.
|
||
|
||
- [x] **1.6 — A VM's mass: allocated share, or one cell.** *Refs:* §20.4, §20.5 #2.
|
||
|
||
> **RESOLVED 2026-08-04 — allocated share.** Less a fresh choice than a confirmation of
|
||
> what §22's elasticity mechanism and §24.3 already treated as decided, and what items
|
||
> 1.2–1.5 already assumed. The one-cell alternative would make outer-level density
|
||
> collapse to heat alone, discarding the starved-vs-small diagnostic that's the entire
|
||
> point of §20.4. Full argument in §20.4.
|
||
|
||
- [x] **1.7 — Rule out recursion beyond two levels** — deliberately, not by omission.
|
||
*Refs:* §20.5 #4.
|
||
|
||
> **RESOLVED 2026-08-04 — Kconfig-tunable cap, default 2.** Not a hard prohibition:
|
||
> bounded, same treatment as item 1.1's containment depth. 2 matches §21's already-decided
|
||
> two-level structure (outer VM Stadium, per-VM inner Stadium). Enforced explicitly at
|
||
> VM-birth time — a birth that would exceed the configured depth is refused. Full argument
|
||
> in §20.5 #4.
|
||
|
||
- [x] **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.
|
||
|
||
> **RESOLVED 2026-08-04.** New hash computed exactly once, at the migration boundary, as
|
||
> part of the block's `MIGRATE` code field — the resident identity (handle/LBN) never
|
||
> changes mid-residency. Whether the old hash is retained for audit is an Artemis-layer
|
||
> question, out of scope for the Stadium per §5's boundary. Full argument in §24.6 #1.
|
||
|
||
- [x] **1.9 — Redefined words as two resident patrons.** Confirm both may be on the floor.
|
||
*Refs:* §24.6 #2.
|
||
|
||
> **RESOLVED 2026-08-04 — confirmed, yes.** Factual, not a design choice:
|
||
> `vm_dict_resolve_in_bucket()` keeps both entries resident with newest-wins shadowing, no
|
||
> GC on redefinition. Correct behaviour, not an artefact. Full argument in §24.6 #2.
|
||
|
||
- [x] **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.
|
||
|
||
> **RESOLVED 2026-08-04 — closed as no.** Eliding it per-kind reintroduces the type-field
|
||
> branch §18.3 forbids; eliding it uniformly breaks lookups words and blocks already
|
||
> depend on outside the Stadium (name, LBN). Neither path is reachable without violating
|
||
> an existing constraint. `identity` stays a fixed, always-present 8-byte field for every
|
||
> kind. Full argument in §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.
|
||
|
||
- [x] **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.**
|
||
|
||
> **RESOLVED 2026-08-04 — linked.** Forced, not chosen: §22.3's disjoint per-VM free list
|
||
> gives no adjacency guarantee, and guaranteeing contiguity would reintroduce the
|
||
> fragmentation §3/§13 already ruled out. 4-byte next-index, 60 usable bytes per
|
||
> continuation cell, 18 continuation cells for a 1024-byte block. §23.3's sizing table is
|
||
> complete; item 3.1 is unblocked on this item. Full argument in §23.3's "The continuation
|
||
> cell" subsection.
|
||
|
||
---
|
||
|
||
## 25.3 Phase 2 — Prepare the existing physics
|
||
|
||
- [x] **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.
|
||
|
||
> **DONE 2026-08-04.** `vm_physics_touch()` no longer takes a `now_ns` parameter at all —
|
||
> it reads `fleet_heartbeat_tick_count` internally, which `vm_runtime.c:143` confirms is
|
||
> execution-paced (advanced once per `vm_tick()` call), not wall-clock. `VMPhysics.last_active_ns`
|
||
> → `last_active_tick`; `VMFleetTouchSample.elapsed_us` → `elapsed_ticks`; a new explicit
|
||
> `touched` flag replaces the old `> 0` sentinel, which doesn't safely carry over to tick
|
||
> counts (a genuine first touch can land on tick 0). The three call sites (VM-EXEC,
|
||
> VM-CALL, VM-STEP in `mama_forth_words.c`) dropped `vm_monotonic_ns(vm)` accordingly.
|
||
> `vm_physics_heartbeat_tick()`/`vm_physics_tick()`'s own dead `now_ns` parameters were
|
||
> left alone — already unused, already documented as such, out of this item's scope.
|
||
>
|
||
> **Regression: clean.** All three architectures boot to `ok>` with identical
|
||
> `dict_hash=0x3d4e1daf289da94f`, matching the item-0.10 baseline, on amd64 (×2), aarch64,
|
||
> and riscv64. Logs: `logs/20260804-113146`, `logs/20260804-113233` (amd64 pair),
|
||
> `logs/20260804-131020` (aarch64), `logs/20260804-131119` (riscv64). No new compiler
|
||
> warnings in the touched files.
|
||
>
|
||
> **Honest limitation on the fleet-heat-sum acceptance criterion.** With Tripod pruned to
|
||
> Hera alone (item 0.1), `vm_physics_touch()`'s fan-out has no other live VM to pull heat
|
||
> from — `others_total` is always 0, so the fleet heat sum is trivially `Q48_ONE` on every
|
||
> boot regardless of whether the tick logic is correct. The double-boot dict-hash match is
|
||
> a valid regression guard (as the acceptance note above already says), but it does not
|
||
> actually stress-test this item's new code path. A real check needs at least one other
|
||
> live VM to touch, which returns in Phase 4 (Hermes/Artemis) — not fabricated here.
|
||
>
|
||
> **Unresolved, flagged not fixed:** `fleet_transfer_slope_q48`'s seed (65536/3) was
|
||
> calibrated against elapsed wall-clock microseconds; elapsed ticks between touches is a
|
||
> different quantity at a different scale, and the seed has not been re-fit against it.
|
||
> Left as-is per §25.0 rule 4 (no invented numbers) — a real re-tune is DoE work (item
|
||
> 5.1), and can only be meaningfully measured once Phase 4 restores a multi-VM fleet
|
||
> anyway, per the limitation just above.
|
||
|
||
- [x] **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.
|
||
|
||
> **DONE 2026-08-04.** `STADIUM_MAX_VM_COUNT` Kconfig symbol (default 4, per item 1.5),
|
||
> wired through `Makefile.starkernel` and given the missing `starforth_config.h` fallback
|
||
> default (`STARFORTH_CONFIG_STADIUM_MAX_VM_COUNT_DEFAULT`) that the earlier WIP commit
|
||
> omitted — without it the macro was only ever defined when a Kconfig `.config` was active,
|
||
> and this build has none, so the first compile attempt failed with `STADIUM_MAX_VM_COUNT`
|
||
> undeclared. `vm_registry_live_count()` (added in the prior WIP commit, counts only
|
||
> `VM_STATE_LIVE` nodes) is now called in `capsule_birth_baby()`
|
||
> (`src/starkernel/capsule/capsule_birth.c`), between capsule validation and
|
||
> `vm_registry_alloc()`, so a full fleet is refused — returning the new
|
||
> `CAPSULE_RUN_ERR_FLEET_FULL` and logging via `capsule_parity_log_birth_failed()` with
|
||
> `vm_id=0` (no VM is allocated on this path) — before any EMBRYO registry slot is
|
||
> consumed.
|
||
>
|
||
> **Regression: clean.** All three architectures boot to `ok>` with identical
|
||
> `dict_hash=0x3d4e1daf289da94f`, matching the item-0.10/2.1 baseline: amd64
|
||
> (`logs/20260804-134914`), aarch64 (`logs/20260804-134957`), riscv64
|
||
> (`logs/20260804-135102`).
|
||
>
|
||
> **Honest limitation.** With Tripod pruned to Hera alone (item 0.1), the fleet never
|
||
> reaches `STADIUM_MAX_VM_COUNT` during boot, so this run exercises the bound-check code
|
||
> path only in the trivially-not-full case — the actual refusal branch is unexercised until
|
||
> Phase 4 restores a multi-VM fleet. Same caveat item 2.1 already recorded for the same
|
||
> reason.
|
||
|
||
---
|
||
|
||
## 25.4 Phase 3 — Stadium core
|
||
|
||
*Blocked on Phase 0 complete, and on items 1.1–1.7 and 1.12.*
|
||
|
||
- [x] **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.
|
||
|
||
> **DONE 2026-08-04.** `StadiumPatronHeader` and `StadiumContinuationCell` defined in the
|
||
> new `include/starkernel/vm/stadium.h`, unioned as `StadiumCell`; translation unit
|
||
> `src/starkernel/vm/stadium.c` added to `Makefile.starkernel`'s `LOADER_EXTRA_SRCS` /
|
||
> `KERNEL_EXTRA_SRCS` so the header actually gets compiled, not merely included by
|
||
> something that never builds.
|
||
>
|
||
> **Discriminator ruling, made before this item's code was written (Captain Bob's call):**
|
||
> the header/continuation discriminator is an external side bitmap, one bit per cell, kept
|
||
> outside the 64-byte cell array — not a header field. Amended into §3 and §23.3
|
||
> accordingly. Item 3.1 declares the bitmap's purpose and indexing contract in a comment;
|
||
> it does not allocate it — that is item 3.2's scope, since sizing depends on the memory
|
||
> budget item 3.2 works from.
|
||
>
|
||
> **Byte count, both counted for real, both exactly 64 with zero compiler-inserted
|
||
> padding** (verified via three C99-portable negative-array-size assertions, no
|
||
> `_Static_assert` — this project targets C99, not C11):
|
||
> - `StadiumPatronHeader`: `identity` u64(8) + `heat` u64(8) + `ttl` u32(4) + `link` u32(4)
|
||
> + `contains` u32(4) + `mass` u16(2) + `flags` u8(1) + `behaviour` u8(1) +
|
||
> `payload` u8[32] = 64. `pin` lives as bit 0 of `flags`, not its own field, matching
|
||
> §3/§23.3. Fields ordered largest-to-smallest so every offset is already a multiple of
|
||
> its own alignment and the 64-byte total is a multiple of the struct's 8-byte max
|
||
> alignment — no padding, without resorting to a `packed` attribute (a GNU extension,
|
||
> forbidden by CLAUDE.md's strict-ANSI-C99 rule).
|
||
> Because the discriminator moved outside the cell, this matches §23.3's original
|
||
> 32-byte-header / 32-byte-inline-payload proposal exactly — no adjustment needed here,
|
||
> unlike the continuation cell below.
|
||
> - `StadiumContinuationCell`: `next` u32(4) + `payload` u8[60] = 64, unchanged from
|
||
> item 1.12's figure — the discriminator living outside the cell means neither variant's
|
||
> byte budget was disturbed by it.
|
||
>
|
||
> **Assertion proven live, not just present:** temporarily changed the header check's
|
||
> expected size to 63, recompiled `stadium.c` standalone
|
||
> (`cc -std=c99 -Wall -Werror -Wextra -D__STARKERNEL__`), confirmed the build failed with
|
||
> `error: size of array 'stadium_header_size_check' is negative`, then restored it and
|
||
> confirmed a clean compile.
|
||
>
|
||
> **Regression: clean, and `stadium.o` confirmed present.** All three architectures boot to
|
||
> `ok>` with identical `dict_hash=0x3d4e1daf289da94f`, matching the item-2.2 baseline —
|
||
> amd64 (`logs/20260804-145132`), aarch64 (`logs/20260804-145232`), riscv64
|
||
> (`logs/20260804-145329`). `find build/<arch> -iname stadium*` confirmed
|
||
> `obj/loader/vm/stadium.o` and `obj/kernel/vm/stadium.o` both exist post-build, closing
|
||
> the gap the WIP on item 2.2 exposed: a header nothing compiles proves nothing.
|
||
>
|
||
> **Open, deferred honestly:** §23.4 #2 ("does a typical message still fit in one cell")
|
||
> remains unanswered — there is no message patron struct anywhere in this tree yet
|
||
> (messages are undesigned future work), so there is nothing concrete to check the 32-byte
|
||
> inline payload against. Not fabricated a number to close this; left open.
|
||
>
|
||
> **REOPENED 2026-08-04.** While reading context for item 3.2, found that two earlier
|
||
> resolutions had explicitly named *this* item as where their Kconfig symbols would be
|
||
> implemented — item 1.1 (line ~2400, "exposed as a Kconfig symbol, named at implementation
|
||
> time in item 3.1", the `contains`-chain depth cap, default 5) and item 1.4 (§22.4 and its
|
||
> own resolution, "Kconfig-tunable at implementation (item 3.1)", the capacity-tick
|
||
> constant, default 1000). Neither made it into the work above, because 3.1's own stated
|
||
> scope ("cell and header") never mentioned them — the promise lived only in items 1.1 and
|
||
> 1.4's text. Captain Bob ruled: reopen, add both here (Phase 3 is implementation, unlike
|
||
> Phase 1's paper-only items — item 1.7's own nesting-depth Kconfig symbol was correctly
|
||
> left undone at Phase 1, by contrast). Declaration only, matching how
|
||
> `STADIUM_MAX_VM_COUNT` was introduced in item 2.2's WIP commit before its consuming logic
|
||
> existed: `STADIUM_CONTAINS_DEPTH_MAX` (default 5) has no consumer yet — reap-gating on
|
||
> `contains` is item 3.5's scope. `STADIUM_CAPACITY_TICK` (default 1000) has no consumer
|
||
> yet either — capacity arbitration isn't on the punch list at all yet. Not inventing that
|
||
> logic here; only the two symbols.
|
||
>
|
||
> **RE-CLOSED 2026-08-04.** Both symbols added following `STADIUM_MAX_VM_COUNT`'s exact
|
||
> pattern: `Kconfig.kernel` entry, `Makefile.starkernel` `kconfig_int` +
|
||
> `VM_FEATURE_FLAG_VARS` forwarding, `starforth_config.h` fallback default (needed for this
|
||
> no-`.config` build, same gap the original `STADIUM_MAX_VM_COUNT` WIP commit hit and item
|
||
> 2.2 fixed). `stadium.h` now includes `starforth_config.h` and carries two more
|
||
> C99-portable compile-time checks (`> 0`, not byte-count) proving both symbols are defined
|
||
> and sane in the same translation unit as the cell checks. `contains`'s field comment now
|
||
> references `STADIUM_CONTAINS_DEPTH_MAX` by name. Recompiled `stadium.c` standalone
|
||
> (clean) before the full run.
|
||
>
|
||
> **Regression: clean, re-run after reopening.** All three architectures boot to `ok>`
|
||
> with identical `dict_hash=0x3d4e1daf289da94f` -- amd64 (`logs/20260804-151032`), aarch64
|
||
> (`logs/20260804-151115`), riscv64 (`logs/20260804-151222`).
|
||
|
||
- [x] **3.2 — Boot-time allocation.** One global cell array, sized from the memory budget,
|
||
before any VM exists. *Refs:* §6, §17.6, §22.3.
|
||
|
||
> **DONE 2026-08-04.** Sizing ruled by Captain Bob among three options (flat Kconfig
|
||
> constant / runtime PMM-derived / `STADIUM_MAX_VM_COUNT × STADIUM_CELLS_PER_VM`):
|
||
> **runtime PMM-derived**, matching §17.6 position (b) literally rather than position (a),
|
||
> the "arbitrary bound" that section argues against. New `STADIUM_MEMORY_PERCENT` Kconfig
|
||
> symbol (default 1%, ruled by Captain Bob) — `stadium_boot_init()` in `stadium.c` reads
|
||
> `pmm_get_stats().free_bytes` at the point of allocation, takes that percent, rounds down
|
||
> to whole `STADIUM_CELL_BYTES` cells. Both the cell array and the discriminator bitmap
|
||
> item 3.1 declared but did not allocate are `kmalloc`'d here and explicitly zero-filled
|
||
> (`kmalloc` does not zero — checked `kmalloc.c`, no `memset`). Called from
|
||
> `kernel_main.c`, immediately before `sk_vm_bootstrap_parity()` — before any VM exists,
|
||
> per §6. Failure is soft (logs, returns -1, does not halt boot): nothing downstream
|
||
> consumes the Stadium yet, matching the existing precedent one line below it
|
||
> (`sk_vm_bootstrap_parity()`'s own failure path also just logs and continues).
|
||
>
|
||
> **Made observable, by agreement before writing code** (same blind spot the item-3.1
|
||
> uncompiled-header gap exposed): a `Stadium: N cells (M KB)` console line at the
|
||
> allocation site, so the three-arch boot's serial logs are evidence the array was
|
||
> actually allocated at the size intended, not just that the kernel still boots.
|
||
>
|
||
> **Regression: clean, and the boot line confirmed present on all three.** All three
|
||
> architectures boot to `ok>` with identical `dict_hash=0x3d4e1daf289da94f`, matching the
|
||
> item-3.1 baseline. Observed sizes (1% of free memory at the allocation point, this
|
||
> session's QEMU configuration): amd64 74234 cells (4639 KB, `logs/20260804-164332`),
|
||
> aarch64 161329 cells (10083 KB, `logs/20260804-164432`), riscv64 76122 cells (4757 KB,
|
||
> `logs/20260804-164537`). Reported, not evaluated against §23.3's ~4096-cells-per-VM
|
||
> illustrative figure — that figure is itself labeled a proposal to validate, not a target
|
||
> this item is scored against.
|
||
>
|
||
> **Explicitly not built here, reported per §25.0 rule 3:** per-VM free lists (§22.3, "each
|
||
> VM holds its own free-list head index into the global array") — those get granted when
|
||
> Hera assigns a VM its quota, which is not this item's scope.
|
||
- [x] **3.3 — Behaviour enumeration and dispatch.** Closed tag set fixed at build time.
|
||
Enumerate behaviours, never patron kinds. *Refs:* §13, §18.3.
|
||
|
||
> **DONE 2026-08-04.** `StadiumBehaviour` (`stadium.h`) enumerates exactly the four tags
|
||
> §18.3 already names — `MIGRATE`, `DELIVER`, `EXPIRE`, `COOL` — mapped from §17.1's
|
||
> patron table: blocks→MIGRATE, messages→DELIVER, ACLs→EXPIRE, words and VMs both→COOL
|
||
> (§18.3 explicitly: "a VM's behaviour tag is COOL, the same tag a word carries"). Nothing
|
||
> invented — the tag set and mapping were already in the document.
|
||
>
|
||
> `stadium_dispatch(cell_index, behaviour)` (`stadium.c`) dispatches on the tag only —
|
||
> never asks what kind of patron departed, per §3/§18.3. Handlers are stubs (console log
|
||
> only): the real migrate/deliver/expire/cool actions belong to subsystems not yet
|
||
> migrated onto the Stadium (Phase 4, §25.5). Nothing calls `stadium_dispatch()` yet
|
||
> either — item 3.5 is its first consumer.
|
||
>
|
||
> **The closedness requirement is now a compiler-enforced property, not just prose:** the
|
||
> switch in `stadium_dispatch()` is exhaustive with no `default` case. Verified this is
|
||
> real, not decorative — temporarily deleted the `COOL` case, rebuilt, got
|
||
> `error: enumeration value 'STADIUM_BEHAVIOUR_COOL' not handled in switch
|
||
> [-Werror=switch]`, restored it, confirmed clean again. Under this project's
|
||
> `-Wall -Werror`, a fifth behaviour tag added without updating dispatch is now a build
|
||
> failure, not a silent gap — the strongest available reading of §13's "closed enumeration,
|
||
> fixed at build time."
|
||
>
|
||
> The header's `behaviour` field stays `uint8_t`, not the enum type itself: C does not
|
||
> guarantee an enum's underlying type, and that field's offset is load-bearing for the
|
||
> exact 64-byte layout item 3.1 validated. Documented as holding `StadiumBehaviour` values
|
||
> cast to `uint8_t`. No new Kconfig symbol — this is a closed code set, not a tunable
|
||
> number.
|
||
>
|
||
> **Regression: clean.** All three architectures boot to `ok>` with identical
|
||
> `dict_hash=0x3d4e1daf289da94f`, matching the item-3.2 baseline — amd64
|
||
> (`logs/20260804-170226`), aarch64 (`logs/20260804-170309`), riscv64
|
||
> (`logs/20260804-170407`).
|
||
- [x] **3.4 — Density ranking.** Heat ÷ mass, read not computed. *Refs:* §19.2, §19.3.
|
||
|
||
> **DONE 2026-08-04.** `stadium_density(cell_index)` (`stadium.c`) reads a header's `heat`
|
||
> and `mass` and returns `heat / mass` — a division on demand from fields already stored
|
||
> in the cell, matching §19.3's "read, not computed by a scheduler" literally: no
|
||
> background process maintains this value. Stays valid Q48.16 without any special
|
||
> fixed-point routine, since `heat` is already Q48.16 and `mass` is a plain integer
|
||
> divisor.
|
||
>
|
||
> `mass == 0` and an out-of-range `cell_index` both return 0 rather than dividing by zero
|
||
> — an empty or never-admitted slot (everything is zero-initialized by item 3.2's
|
||
> `stadium_boot_init()`, and nothing yet births a patron into the Stadium) has no
|
||
> footprint to be dense within.
|
||
>
|
||
> **Deliberately not built here, per the item's own wording:** finding the densest or
|
||
> least-dense resident (§19.3's admission/eviction comparison) is item 3.5's scope — this
|
||
> function supplies the per-cell value that comparison will read, not the ranking/min-max
|
||
> machinery itself. Nothing calls `stadium_density()` yet either.
|
||
>
|
||
> **Regression: clean.** All three architectures boot to `ok>` with identical
|
||
> `dict_hash=0x3d4e1daf289da94f`, matching the item-3.3 baseline — amd64
|
||
> (`logs/20260804-171332`), aarch64 (`logs/20260804-171414`), riscv64
|
||
> (`logs/20260804-171513`).
|
||
- [x] **3.5 — Admission and eviction.** Admit if denser than the least dense resident.
|
||
*Refs:* §19.3.
|
||
|
||
> **DONE 2026-08-04.** `stadium_admit(candidate)` and `stadium_evict(cell_index)` in
|
||
> `stadium.c`. Admission scans for an unused cell first (bitmap bit clear, `mass == 0`) and
|
||
> places there directly, no comparison needed — §19.3's density rule only governs the full
|
||
> case. Otherwise finds the least-dense resident, skipping pinned patrons (`flags` bit 0,
|
||
> §3) and `contains`-gated ones (item 1.1: a patron holding another cannot be reaped), and
|
||
> evicts it only if the candidate is strictly denser ("denser than," not "at least as dense
|
||
> as," per §19.3's own wording). Eviction dispatches the departing patron's behaviour
|
||
> (§18.3) before clearing its slot, per §17.2 ("reap means leaves the floor, not
|
||
> destroyed").
|
||
>
|
||
> **A real bug caught before this ever ran:** the first draft used `contains == 0` to mean
|
||
> "holds nothing." Cell index 0 is a valid index — Hera, item 3.6's patron zero — so that
|
||
> conflated "contains Hera" with "contains nothing." Fixed with a proper sentinel,
|
||
> `STADIUM_CONTAINS_NONE` (`UINT32_MAX`), distinct from every valid index. Caught by
|
||
> re-reading before compiling, not by any test.
|
||
>
|
||
> **A second-pass review (before the boot run) found one blocking gap, fixed, and two
|
||
> non-blocking ones, recorded rather than fixed:**
|
||
>
|
||
> - **Blocking, fixed:** neither function accounted for `mass`. Admission placed exactly
|
||
> one cell and set exactly one bit regardless of the candidate's stated mass; eviction
|
||
> symmetrically freed one cell and orphaned the rest. For `mass > 1` (§23.3: a 1024-byte
|
||
> block is mass 19) this breaks capacity conservation — cells leak on every eviction of a
|
||
> multi-cell patron, and the "Stadium is full" test becomes wrong since occupancy was
|
||
> never correctly accounted. The fix is refusal, not implementation:
|
||
> **`stadium_admit()` now refuses any candidate with `mass != 1`.** A multi-cell patron
|
||
> needs its continuation chain allocated through the per-VM free lists (§22.3) —
|
||
> item 3.2's own DONE note already deferred those as out of scope, granted only when Hera
|
||
> assigns a VM its quota. This item does not build them; it refuses what it can't yet do
|
||
> correctly rather than doing it wrong.
|
||
> - **Not fixed, documented as a live latent gap:** the discriminator bitmap can only say
|
||
> header-vs-not-header, not free-vs-continuation. The free-cell scan
|
||
> (`!bitmap_get(i) && mass == 0`) reads offsets 28–29 of whatever cell is actually there
|
||
> under the *header* struct layout; for a real continuation cell those offsets are
|
||
> payload bytes, and if they happen to read as zero the scan would treat a live
|
||
> continuation cell as free and overwrite it. Latent, not live: nothing creates
|
||
> continuation cells yet, and the `mass != 1` refusal above keeps this provably latent
|
||
> for as long as that refusal stands. The real fix is the free list itself — a cell is
|
||
> free iff it is on one, no union-punning needed — which supersedes this scan when built.
|
||
> - **Not fixed, minor:** `stadium_admit()`'s two full-array scans are O(N) each, and
|
||
> `candidate_density` duplicates `stadium_density()`'s arithmetic inline because the
|
||
> candidate is not yet in the array to call it on. Both go away with the free list; not
|
||
> worth a workaround for code with no caller yet.
|
||
>
|
||
> **Unexercised at runtime, stated plainly rather than implied by a passing boot:** nothing
|
||
> calls `stadium_admit()` or `stadium_evict()` yet (no real patron kind is wired to the
|
||
> Stadium — Phase 4 migration work). No self-test was added: filling ~74,000+ cells to
|
||
> actually reach the eviction-on-full branch in a boot run was judged impractical for the
|
||
> value it would add, following the same honesty precedent item 2.2 recorded for its own
|
||
> unexercised fleet-full path. The free-cell placement branch, the pin/contains skip
|
||
> logic, and the density-comparison branch have never executed against real data.
|
||
>
|
||
> **Regression: clean.** All three architectures boot to `ok>` with identical
|
||
> `dict_hash=0x3d4e1daf289da94f`, matching the item-3.4 baseline — amd64
|
||
> (`logs/20260804-172516`), aarch64 (`logs/20260804-172556`), riscv64
|
||
> (`logs/20260804-172651`).
|
||
>
|
||
> **Amended by item 3.7, 2026-08-04, same day.** `stadium_admit()`'s signature changed —
|
||
> it now takes a `vm_id` parameter and scopes both free-cell placement and eviction-search
|
||
> to that VM's own quota, per §22.3's per-VM free lists (built in 3.7, not this item). The
|
||
> two full-array O(N) scans this item shipped are gone in the O(1)-free-list-pop common
|
||
> case; the "not fixed, minor" note above about them is superseded. The `mass != 1`
|
||
> refusal and the pin/contains logic described above are otherwise unchanged.
|
||
- [x] **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.
|
||
|
||
> **DONE 2026-08-04.** `STADIUM_HERA_CELL_INDEX` (0) documented as a positional invariant
|
||
> from §6's boot order (Hera is the first patron admitted), not a runtime identity check —
|
||
> nothing births anything yet, Hera included, so the index is never actually occupied
|
||
> today. `stadium_evict()` now panics via `sk_hal_panic()` (already `noreturn`, matching
|
||
> `arena.c`'s existing use) if a *resident* cell 0 is ever selected.
|
||
>
|
||
> **Placement matters and was deliberate:** the assertion runs *before* the pin and
|
||
> `contains` refusal checks, not after. §20.5 #3 asks for a check independent of pin
|
||
> holding — if it ran after the pin check, a wrongly-cleared pin would let the ordinary
|
||
> refusal path quietly return `-1` instead of ever reaching the panic, silently swallowing
|
||
> exactly the failure this item exists to surface.
|
||
>
|
||
> **Per the item's own wording, not implemented as a filter:** `stadium_admit()`'s
|
||
> least-dense search is unchanged — it still relies on the general pin skip (item 3.5) to
|
||
> avoid selecting a pinned Hera in the first place. §20.5 #3 explicitly: "state it as an
|
||
> assertion at the eviction site, not as a filter on the candidate set — filtering hides
|
||
> the bug, asserting reports it." Adding a second, redundant filter in the search loop
|
||
> would have done exactly what that line warns against.
|
||
>
|
||
> **The panic path itself is, and will remain, unexercised by the acceptance mechanism.**
|
||
> `sk_hal_panic()` halts the machine — triggering it deliberately would mean the kernel
|
||
> cannot reach `ok>`, which is incompatible with the three-arch boot being this project's
|
||
> sole acceptance test. Nothing calls `stadium_evict()` yet regardless (same as items 3.4
|
||
> and 3.5), so this boot run does not exercise the check either way. Correctness rests on
|
||
> the placement argument above, not a test.
|
||
>
|
||
> **Regression: clean.** All three architectures boot to `ok>` with identical
|
||
> `dict_hash=0x3d4e1daf289da94f`, matching the item-3.5 baseline — amd64
|
||
> (`logs/20260804-173311`), aarch64 (`logs/20260804-173350`), riscv64
|
||
> (`logs/20260804-173446`).
|
||
>
|
||
> **Correction, 2026-08-04, same day:** the line originally here claimed "Phase 3 core
|
||
> complete" with items 3.1–3.6. That was premature — starting work on item 4.1 surfaced
|
||
> that its own prerequisite (the per-VM free lists §22.3 describes) doesn't exist yet.
|
||
> §25.4 gained a seventh item, 3.7, below. Phase 3 core is not complete until it is.
|
||
|
||
- [x] **3.7 — Per-VM free lists.** Each VM holds its own free-list head index into the
|
||
global array (§22.3); cells are drawn by popping that head, granted by Hera. Added
|
||
2026-08-04 after starting item 4.1 surfaced this as an unbuilt prerequisite — see item
|
||
3.6's correction note above. *Refs:* §22.3.
|
||
|
||
> **DONE 2026-08-04.** `StadiumVMQuota` table (`stadium.c`, size `STADIUM_MAX_VM_COUNT`,
|
||
> linearly searched by `vm_id`): `capsule_birth.c`'s `vm_id` is monotonic and never reused
|
||
> (`next_vm_id` only increments, even across VM death — verified by reading, not assumed),
|
||
> so it cannot index a table directly; a linear scan over 4 entries costs nothing.
|
||
>
|
||
> A new per-cell `stadium_owner` byte array (one byte per cell, same pattern as item 3.1's
|
||
> discriminator bitmap) records which quota slot a cell belongs to — needed because
|
||
> eviction must return a freed cell to the *correct* VM's list, and because eviction's
|
||
> least-dense search must stay scoped to the evicting VM's own residents (quota
|
||
> isolation: one VM's admission can never evict another VM's patron). A compile-time check
|
||
> (`STADIUM_MAX_VM_COUNT <= 255`) confirms the quota-slot index fits the byte.
|
||
>
|
||
> Free-list linkage reuses each cell's own `link` field as a "next free cell" pointer while
|
||
> unresident — `link` is documented only as generic "index into the Stadium, not a
|
||
> pointer," so this is a repurposing of already-permitted, previously-unspecified storage,
|
||
> not a header change. It does **not** answer the separate, still-open question of which
|
||
> field would carry a multi-cell patron's first continuation-cell index — item 3.5's
|
||
> `mass != 1` refusal stands exactly as it was.
|
||
>
|
||
> At `stadium_boot_init()`, every cell is chained into one list in ascending index order
|
||
> and granted in full to `vm_id` 0 (Hera) — the only VM that exists (item 0.1). Ascending
|
||
> order guarantees the first-ever pop returns cell 0, preserving item 3.6's "Hera is patron
|
||
> zero" invariant once real birth-wiring calls `stadium_admit()`.
|
||
>
|
||
> `stadium_admit()`'s signature changed to `stadium_admit(vm_id, candidate)` — a change to
|
||
> code shipped in item 3.5, amended there (see above). Pops the calling VM's free-list
|
||
> head first (O(1)); only falls back to a same-VM-scoped eviction search if that list is
|
||
> empty.
|
||
>
|
||
> **A real bug caught before the boot run, by a second review pass:** the zero-fill that
|
||
> clears a header on eviction (and the initial free-list build) both leave `contains == 0`
|
||
> — but 0 is Hera's valid index (item 3.1's earlier `STADIUM_CONTAINS_NONE` fix was about
|
||
> exactly this collision), so every cell on a free list was silently readable as "contains
|
||
> Hera." Fixed by explicitly setting `contains = STADIUM_CONTAINS_NONE` at both sites
|
||
> (the boot-time chain-build loop, and `stadium_evict()`'s free-list-return step) rather
|
||
> than leaving it to the zero-fill's incidental value.
|
||
>
|
||
> **Explicitly out of scope, reported not invented:**
|
||
> - Granting quota to any VM other than Hera, and transferring capacity between VMs, is
|
||
> capacity *arbitration* — item 1.3 left "how much capacity moves per eligible transfer"
|
||
> explicitly open, so this item does not invent it. Only the boot-time all-to-Hera grant
|
||
> exists; `stadium_owner` is set once at boot and never written again, so
|
||
> `quota_slot_for_vm()` returns refusal for every `vm_id != 0`, permanently, until
|
||
> something else writes to it. Item 4.2 ("Hermes native on the Stadium") will need both
|
||
> the grant path and the owner-array writes — flagging now so it isn't a surprise there.
|
||
> - Multi-cell continuation-chain attachment remains unresolved (see above); item 3.5's
|
||
> refusal is untouched.
|
||
>
|
||
> **Unexercised at runtime,** same as items 3.4–3.6: nothing calls `stadium_admit()` or
|
||
> `stadium_evict()` yet. The free-list pop path, the quota-scoped eviction fallback, and
|
||
> the boot-time chain-build are all unexercised against real data.
|
||
>
|
||
> **Regression: clean.** All three architectures boot to `ok>` with identical
|
||
> `dict_hash=0x3d4e1daf289da94f`, matching the item-3.6 baseline, and the `Stadium: N
|
||
> cells (M KB)` boot line is unaffected in format — amd64 (`logs/20260804-180453`, `74234
|
||
> cells (4639 KB)`), aarch64 (`logs/20260804-180541`), riscv64 (`logs/20260804-180637`).
|
||
>
|
||
> **Correction, 2026-08-04, same day:** starting work on item 4.1 surfaced a further
|
||
> prerequisite — see item 3.8 below. §25.4 gained an eighth item.
|
||
|
||
- [x] **3.8 — VM identifiers as UUID/GUID.** Replaces `capsule_birth.c`'s monotonic
|
||
`uint32_t vm_id` with a wider, RFC-4122-shaped 128-bit identifier. Added 2026-08-04 after
|
||
starting item 4.1 surfaced the need to thread a `vm_id` into `stadium_admit()`'s new
|
||
quota parameter, and Captain Bob ruled UUID/GUID rather than keeping the narrower type.
|
||
*Refs:* §22.3 (item 3.7's quota table), capsule_birth.c's VM registry.
|
||
|
||
> **DONE 2026-08-04.** New `VMUuid` type (`include/starkernel/vm_uuid.h`,
|
||
> `src/starkernel/capsule/vm_uuid.c`): two `uint64_t` halves, formatted
|
||
> RFC-4122-shaped (`xxxxxxxx-xxxx-xxxx-xxxx-xxxxxxxxxxxx`) for logging.
|
||
>
|
||
> **Not real randomness — checked directly, not assumed.** This kernel has no RNG source
|
||
> at all. Verified empirically against QEMU 10.2.1 rather than guessed: amd64's `RDRAND`
|
||
> and riscv64's `Zkr` entropy extension are both real, available CPU features here (QEMU
|
||
> accepts `-cpu qemu64,+rdrand` and `-cpu rv64,zkr=true` without error); aarch64 has
|
||
> **no** RNG/RNDR property on any CPU model including `max` — checked exhaustively via
|
||
> QMP's `query-cpu-model-expansion` against all 23 of `max`'s exposed properties, none
|
||
> RNG-related. Captain Bob ruled a uniform fallback across all three ISAs rather than a
|
||
> per-architecture split (real RNG on two, something else on the third).
|
||
>
|
||
> **The fallback is a deterministic PRNG (splitmix64 — public-domain, minimal), seeded
|
||
> from the Mama capsule's content hash**, pre-filling a 16-entry FIFO pool at boot
|
||
> (`vm_uuid_pool_init()`, called from `capsule_birth_mama()` right after the capsule hash
|
||
> is known), refilled with another batch continuing the same stream when exhausted
|
||
> (`vm_uuid_next()`) — exactly the shape Captain Bob asked for. Same capsule booted twice
|
||
> produces the same id sequence, preserving the run-to-run reproducibility this session's
|
||
> `dict_hash` regression check has relied on for every prior item.
|
||
>
|
||
> **Hera keeps a fixed, reserved id — all-zero — not drawn from the pool.**
|
||
> `capsule_birth.c` uses `vm_id == 0` as a load-bearing sentinel in three places, found by
|
||
> reading before writing any code: "Hera cannot be killed" (`capsule_vm_kill`), the same
|
||
> check in `capsule_vm_kill_all_nonmama`, and the fleet heat-fanout parent-chain
|
||
> terminator (`capsule_run.h`'s `parent_vm_id` comment: "self-referential, `parent_vm_id
|
||
> == vm_id == 0`"). `vm_uuid_hera()` (all-zero) preserves all three with a cheap
|
||
> equality check (`vm_uuid_is_hera()`).
|
||
>
|
||
> **Two real sentinel-collision bugs caught before they shipped, both the same class of
|
||
> mistake `STADIUM_CONTAINS_NONE` was already fixed for once this session:**
|
||
> - `vm_uuid_none()` (all-ones) is deliberately **not** all-zero, since all-zero is now
|
||
> Hera's reserved value — used for "not yet assigned" placeholders
|
||
> (`vm_registry_alloc()`'s embryo `vm_id` before birth completes) and "no VM" logging
|
||
> (item 2.2's `FLEET_FULL` refusal, which happens before any VM is allocated).
|
||
> - `StadiumVMQuota`'s "slot empty" state was already tracked by an `in_use` boolean
|
||
> (item 3.7), not a `vm_id` sentinel value — so no second collision was actually
|
||
> possible there; confirmed by re-reading item 3.7's own code rather than assumed, and
|
||
> the dead, never-referenced `STADIUM_QUOTA_SLOT_EMPTY` macro item 3.7 defined "just in
|
||
> case" was removed as part of this item's cleanup.
|
||
>
|
||
> **Blast radius, larger than first scoped — flagged mid-work rather than silently
|
||
> absorbed:** beyond the originally-flagged `capsule_run.*`/`capsule_birth.*`/`stadium.*`,
|
||
> compiling surfaced that `capsule_vm_physics.c`/`.h` (the fleet heat-transfer layer item
|
||
> 2.1 modified earlier this session) has its own `vm_id`-keyed node table and walks
|
||
> `parent_vm_id` chains via `capsule_vm_registry_get()` — the same identity space, so it
|
||
> had to change too (`vm_physics_init`/`_retire`/`_touch`/`_heat_of`/`_find`/
|
||
> `_find_root_id`), plus its callers in `mama_forth_words.c` and
|
||
> `sk_vm_bootstrap.c`.
|
||
>
|
||
> **One live FORTH word contract changed, by explicit ruling:** `CAPSULE-BIRTH` was
|
||
> `( capsule-id -- vm-id )`, a single cell — can't hold 128 bits. Options were two cells,
|
||
> a silent 64-bit truncation, or a separate small FORTH-only handle; Captain Bob picked
|
||
> two cells ("there is doubles support in the FORTH std word set anyway"). New contract:
|
||
> `( capsule-id -- vm-id-hi vm-id-lo )`, high cell on top, `vm_uuid_none()`'s hi/lo (both
|
||
> all-ones) on any failure path including the early bounds-check return. `MAMA-VM-ID`
|
||
> changed the same way: `( -- 0 0 )`, both cells zero since Hera's id is all-zero.
|
||
>
|
||
> **Regression: clean, across a genuinely large diff.** All three architectures boot to
|
||
> `ok>` with identical `dict_hash=0x3d4e1daf289da94f`, matching the item-3.7 baseline —
|
||
> amd64 (`logs/20260804-194631`), aarch64 (`logs/20260804-194711`), riscv64
|
||
> (`logs/20260804-194810`). A full (not standalone-file) kernel rebuild was used to catch
|
||
> cross-file breakage before the boot run, given the size of this change; it surfaced the
|
||
> `capsule_vm_physics.c` blast radius above that a narrower compile check would have
|
||
> missed.
|
||
>
|
||
> **Phase 3 core complete.** Items 3.1–3.8 close out §25.4.
|
||
|
||
---
|
||
|
||
## 25.5 Phase 4 — Migrate the subsystems
|
||
|
||
*One subsystem at a time, converted completely. Never two live heat mechanisms at once
|
||
(§11).*
|
||
|
||
- [x] **4.1 — Hot words onto the Stadium.** Replaces the round-robin eviction with density
|
||
ranking, via the reservoir mechanism (§17.7) and a kernel-side `word_id → cell_index` map
|
||
(no `DictEntry` change, decided 2026-08-05). *Refs:* §17.3, §17.7.
|
||
|
||
> **Unblocked 2026-08-05 — §17.7 reads DECIDED.** Acceptance restated below now that the
|
||
> mechanism itself changed; the original "measurable via `stats.evictions`/
|
||
> `stats.promotions`" presumed reusing the old cache's `HotwordsStats`, which this item
|
||
> retires on the kernel side rather than extends.
|
||
>
|
||
> **Done, 2026-08-05.** Two rulings made mid-implementation (§17.7's addendum): Hera is now
|
||
> actually birthed into cell 0 (`stadium_birth_hera()`, a deliberate scope addition, not
|
||
> silently folded in) closing the cell-0 panic hazard the original design left open; the
|
||
> quantum/cool-rate got two new Kconfig knobs (`STADIUM_WORD_HEAT_QUANTUM`,
|
||
> `STADIUM_WORD_COOL_RATE_Q48`) with derived-not-fabricated defaults, flagged untuned. A
|
||
> third addition, required for the item's own correctness rather than scope creep: a FORGET
|
||
> coherence hook (`stadium_word_forget()`, called from `vm_dictionary_untrack_entry()`)
|
||
> reclaims a resident word's cell before its `word_id` is recycled, closing an aliasing gap
|
||
> of the same shape as the 2026-08-02 `block_words.c` bug.
|
||
>
|
||
> *Acceptance, verified:*
|
||
> - Kernel builds only: all five `hotwords_cache_*` call sites in `dictionary_management.c`
|
||
> (not just the two originally named) are bypassed under `__STARKERNEL__`.
|
||
> - Word dispatch feeds the Stadium at all three of `vm_core.c`'s
|
||
> `physics_execution_heat_increment()` call sites — an already-resident word gets the
|
||
> reservoir-quantum touch; a non-resident word attempts Option B starter-grant admission.
|
||
> - New Stadium-side promotion/eviction counters (`stadium_words_stats()`) and a
|
||
> conservation check are printed to the boot console
|
||
> (`stadium_words_print_boot_diagnostics()`) before the REPL starts.
|
||
> - Hosted builds unaffected — confirmed via a clean hosted `make`.
|
||
> - All three architectures booted to `ok>` with logs under `logs/20260805-130800/amd64/`,
|
||
> `logs/20260805-130919/aarch64/`, `logs/20260805-131030/riscv64/`. `dict_hash` is
|
||
> identical across all three (`0x3d4e1daf289da94f`) and identical in shape to pre-4.1
|
||
> parity output — untouched, as designed. Stadium diagnostics also identical across all
|
||
> three: `promotions=354 evictions=0`, `resident_sum=65536 reservoir=0 sum=65536
|
||
> (Q48_ONE=65536)` — the conservation invariant closes exactly.
|
||
- [x] **4.1a — Quota granting: Hermes's birth grant.** New prerequisite item, inserted
|
||
2026-08-05 while scoping 4.2 — found that no quota-granting mechanism exists at all.
|
||
`quota_slot_for_vm()` refuses every `vm_id != 0` today, permanently, by design (item 3.5's
|
||
note); `stadium_admit()`'s own doc and item 3.2's DONE note both defer per-VM free lists to
|
||
"when Hera assigns a VM its quota," which nothing builds. Item 1.3 (§25.2) resolved *when*
|
||
Hera arbitrates a capacity *transfer* between VMs that already hold quotas, but explicitly
|
||
left "how much capacity moves" unresolved and out of scope (§22.5 #2) — that is the
|
||
*recurring* mechanism, and stays open; this item is narrower: Hermes's one-time *initial*
|
||
grant at birth, the same shape as Hera's own whole-pool grant at `stadium_boot_init()`, not
|
||
an instance of the still-open recurring loop. *Refs:* §1.3, §22.3, §22.5 #2.
|
||
|
||
> **Ruled, 2026-08-05:**
|
||
> 1. **Reservoir is not part of this.** `stadium.c`'s own comment states the conservation
|
||
> invariant per-VM — `Σ(resident heat) + reservoir == Q48_ONE` for *that VM's own
|
||
> quota* — not a shared pool split across VMs. Hermes gets her own fresh `Q48_ONE`
|
||
> reservoir at birth, the same pattern as Hera's boot grant, not a fraction of Hera's.
|
||
> Only cell count is actually open.
|
||
> 2. **Cell split: even.** At Hermes's birth, half of whatever cells are currently on
|
||
> Hera's free list move to a new quota slot for Hermes. Hera's residents — including
|
||
> pinned cell 0 — are never touched; only her free list is split. No tuned constant: an
|
||
> even split needs no threshold, consistent with §22's "no tuned threshold" elsewhere in
|
||
> this design.
|
||
>
|
||
> *Done, verified 2026-08-05.* `stadium_grant_quota(VMUuid new_vm_id, VMUuid from_vm_id)`
|
||
> (`stadium.c`/`stadium.h`) exists as designed: counts `from_vm_id`'s free list, splits the
|
||
> first half (by list-walk order) into a new quota slot for `new_vm_id` with `stadium_owner`
|
||
> reassigned per moved cell, terminates both lists correctly, and grants a fresh `Q48_ONE`
|
||
> reservoir. Refuses without crashing if `new_vm_id` already holds a quota, `from_vm_id`
|
||
> holds none, the free list has fewer than 2 cells, or no empty quota slot remains. Wired
|
||
> into every baby VM's birth (`capsule_birth.c`, right after `stadium_vm_id` is set, before
|
||
> IDENTITY exec) — failure is non-fatal to birth itself, same as having no quota is today's
|
||
> status quo for every VM.
|
||
>
|
||
> *Verified* via a boot-time self-test (`kernel_main.c`, right after item 4.1's diagnostic
|
||
> print) using a synthetic identity — deliberately not `vm_uuid_next()`'s real birth pool
|
||
> (would perturb the deterministic ID stream) and not a real capsule birth (item 0.1 pruned
|
||
> automatic Hermes birth from `init.4th`; restoring that is item 4.2's job, not this one's).
|
||
> All three architectures booted to `ok>` with logs under `logs/20260805-145714/amd64/`,
|
||
> `logs/20260805-145806/aarch64/`, `logs/20260805-145902/riscv64/`, each printing identically:
|
||
> `Stadium quota grant self-test: OK`, `Hera reservoir=0` (already fully committed to
|
||
> resident words by item 4.1's own self-test, unchanged by this grant — correct, since this
|
||
> item never touches reservoir on the donor side), `test-vm reservoir=65536` (a fresh
|
||
> `Q48_ONE`, as ruled). `dict_hash` identical across all three and unchanged from item 4.1's
|
||
> baseline (`0x3d4e1daf289da94f`), confirming this item added no dictionary word.
|
||
- [x] **4.2 — Hermes native on the Stadium.** The proving ground; produces the effort
|
||
number. *Refs:* §10. **Unblocked 2026-08-05** — item 4.1a closed; `stadium_grant_quota()`
|
||
exists and is wired into every baby VM's birth. **Complete 2026-08-07** — all `Done when`
|
||
bullets satisfied; see the effort number and MBR-scoping ruling below.
|
||
|
||
> **Two rulings taken before work starts, 2026-08-05:**
|
||
> 1. **`stadium_owner[idx]` fix folded into this item's scope**, by explicit Captain Bob
|
||
> authorization (not a §25.0-rule-3 violation — this is the same "required for the
|
||
> item's own correctness" precedent as 4.1's FORGET hook). `stadium_admit()` writes
|
||
> `stadium_owner[idx]` on neither the free-list-pop nor the eviction-fallback path;
|
||
> harmless while Hera is the only VM with a quota, but this item puts a second VM
|
||
> (Hermes) on the Stadium, and without the fix a resident's evict-credit flows to the
|
||
> wrong VM's reservoir. Fix ships as part of this item's commit, called out separately
|
||
> in the acceptance below so it doesn't hide inside the migration diff.
|
||
> 2. **C/FORTH boundary: new thin FORTH-callable primitives**, registered in C exactly
|
||
> like `BIRTH`/`RUN`/`USE` (kernel-only, not shared/vendored), justified under
|
||
> `.claude/CLAUDE.md`'s "raw hardware access, atomics, syscalls, freestanding kernel
|
||
> ops" exception to "compose in FORTH first." Candidate surface — confirmed, not yet
|
||
> implemented:
|
||
> ```
|
||
> STADIUM-ADMIT ( identity heat behaviour -- cell | -1 )
|
||
> STADIUM-EVICT ( cell -- flag )
|
||
> STADIUM-RES@ ( vm-id -- heat )
|
||
> STADIUM-RES-PULL ( vm-id qty -- heat )
|
||
> STADIUM-RES-PUSH ( vm-id heat -- )
|
||
> ```
|
||
> Exact stack signatures and error handling to be finalized during implementation, not
|
||
> invented here. `HERMES.md`'s non-negotiable — all Hermes-side logic in StarForth,
|
||
> zero new C beyond this primitive layer — still applies; these five words are the
|
||
> entire C surface this item may add.
|
||
> 3. **`vm_core.c`'s hardcoded `vm_uuid_hera()` — Option A, add a `VMUuid` field to `VM`.**
|
||
> Found while scoping this item, not a new bug: all three `stadium_word_dispatch()`
|
||
> call sites in `vm_core.c` (item 4.1) hardcode `vm_uuid_hera()`, with an inline
|
||
> comment already naming this as 4.2's job ("Tripod is pruned to Hera alone; revisit
|
||
> at item 4.2"). Fixing it requires a running `VM*` to know its own identity, which
|
||
> nothing today provides — `VMUuid` exists only on `VMRegistryEntry` (`capsule_run.h`),
|
||
> never on `VM` (`include/vm.h`) itself. Ruled: add a `VMUuid` field to `VM`, guarded
|
||
> `#ifdef __STARKERNEL__` in the same block as the existing `VMCallState` lifecycle
|
||
> fields (`include/vm.h` ~line 523) — not Option B (threading vm_id through the call
|
||
> chain without touching the struct). `VM` is shared/vendored, same as `DictEntry`, so
|
||
> the hosted build's layout must stay untouched outside the `__STARKERNEL__` guard.
|
||
> Set once, at VM creation, from the same `VMRegistryEntry.vm_id` the birth path
|
||
> already assigns (`capsule_birth.c`) — not invented at the dispatch call sites.
|
||
> 4. **Primitive surface grows from five to seven.** Found while reading Hermes's actual
|
||
> implementation (`capsules/hermes/init.4th`): `MSG-COOL-ALL`/`CH-COOL-ALL` (blocks
|
||
> 4108/4114) mutate each live node's own heat field in place every `HERMES-TICK`, and
|
||
> `MSG-TOTAL-HEAT`/`CH-TOTAL-HEAT` sum it. None of the original five primitives expose
|
||
> a resident cell's own `heat` field at all — only admission, eviction, and the calling
|
||
> VM's reservoir. Ruled: two more primitives, same implicit-self discipline as the
|
||
> original five (cell must belong to the calling VM's own quota):
|
||
> ```
|
||
> STADIUM-HEAT@ ( cell -- heat )
|
||
> STADIUM-HEAT! ( new-heat cell -- )
|
||
> ```
|
||
> `STADIUM-HEAT!` reconciles the reservoir delta atomically in C — pulls from the
|
||
> calling VM's reservoir if `new-heat` is higher than current (refusing, leaving heat
|
||
> unchanged, if the reservoir can't cover it), pushes back if lower — the same shape as
|
||
> `stadium_word_dispatch()`'s own cooling code. Conservation is never left to FORTH to
|
||
> get right by remembering to call `STADIUM-RES-PULL`/`-PUSH` itself; a single call is
|
||
> both the write and the correct accounting. Serves two callers: a cooling tick
|
||
> (`heat × Q-DECAY`, replacing `MSG-COOL-ONE`'s in-place multiply) and a floor-refresh
|
||
> (`COMMON-INIT`/`HERMES-TICK` reset `COMMON-CH`'s heat to a fixed `Q.1/3` unconditionally,
|
||
> not a decay — needs the same delta-reconciling write, just with a different target
|
||
> value). `STADIUM-HEAT@` alone serves `MSG-TOTAL-HEAT`/`CH-TOTAL-HEAT`'s summation and
|
||
> `MSG-REAP`/`CH-REAP-SAFE`'s heat-reached-zero check. Cooling cadence stays entirely in
|
||
> Hermes's own FORTH `HERMES-TICK` loop (rewritten to call these, not a new C-side
|
||
> per-tick sweep) — matches `HERMES.md`'s language constraint and the fact that
|
||
> `HERMES-TICK` already owns this loop; nothing about moving the heat storage changes
|
||
> who decides when to cool.
|
||
>
|
||
> **Open, surfaced not resolved:** mapping Hermes's message/channel lifecycle onto the
|
||
> closed `STADIUM_BEHAVIOUR_*` set (`MIGRATE`/`DELIVER`/`EXPIRE`/`COOL`) — `DELIVER` and
|
||
> `EXPIRE` currently have dispatch cases in `stadium.c` but no consumer, and were
|
||
> apparently reserved for exactly this. Which tag maps to a message and which (if either)
|
||
> to a channel is implementation work for this item, not decided here. Also open: whether
|
||
> migrating message/channel heat into the Stadium's conserved 1.0 dissolves or changes
|
||
> `HERMES.md`'s G8 note (`HERMES-K`/`K-FLEET` integration deferred pending cross-VM return
|
||
> values) — the reservoir mechanism (`stadium_reservoir_pull`/`push`) already crosses VM
|
||
> boundaries, so this may no longer be blocked the way G8 describes. Raise during
|
||
> implementation; do not resolve by assumption.
|
||
>
|
||
> **Bug found and fixed during implementation, 2026-08-06 — amd64-only dictionary
|
||
> corruption, root cause was a missing `-fno-pic`, not Stadium logic.** While exercising
|
||
> Hermes's migrated words in this item's self-test (`kernel_main.c`), `MSG-COOL-ALL`
|
||
> became unreachable via `vm_find_word()` immediately after `MSG-DELIVER-ALL` ran —
|
||
> amd64 only; aarch64 and riscv64 never showed it. Initial hypotheses (capsule-loader
|
||
> forward-reference retry interaction, GDB-perturbed timing, arena exhaustion, a stray
|
||
> `dict_reorganize_buckets_by_heat()` race) were each tested and ruled out by direct
|
||
> print-based bisection (GDB is unusable on this kernel — see below). Root cause,
|
||
> confirmed by disassembling the actual booted `starkernel_loader.efi`:
|
||
> `dict_find_word_heat_aware()` (`dictionary_heat_optimization.c`) and `vm_find_word()`
|
||
> (`dictionary_management.c`) both reference the same extern globals
|
||
> (`sf_fc_list`/`sf_fc_count`/`sf_fc_cap`, the dictionary's first-character lookup index),
|
||
> but GCC compiled the two files' references differently: `vm_find_word()`, in the same
|
||
> translation unit as the arrays' definition, got direct `lea sym(%rip), %reg` addressing;
|
||
> `dict_find_word_heat_aware()`, a genuine cross-TU extern reference, got GOT-indirect
|
||
> `mov sym@GOTPCREL(%rip), %reg` addressing (`R_X86_64_REX_GOTPCRELX`). The latter requires
|
||
> a populated Global Offset Table slot — normally a dynamic linker's job. This kernel is a
|
||
> freestanding, statically-linked UEFI PE image with no dynamic linker and no `.got`
|
||
> section; the "GOT slot" GCC emitted the reference against is just an ordinary
|
||
> zero-initialized `.bss` cell that nothing ever writes. The load silently returns NULL
|
||
> instead of the array's real address, `vm_find_word()`'s `!bucket || n==0` guard reads it
|
||
> as "empty," and the word reports `UNKNOWN WORD` even though its `DictEntry` is fully
|
||
> intact (verified by a manual `vm->latest`→`link` chain walk). Whether a given reference
|
||
> gets the safe or unsafe addressing mode is a per-call-site GCC codegen heuristic
|
||
> sensitive to surrounding code size — which is why the symptom appeared and disappeared
|
||
> across unrelated one-line changes (even hitting an unrelated symbol, `BIRTH`'s own
|
||
> dictionary entry, once), and why it looked for a long time like a timing-sensitive
|
||
> memory-corruption bug rather than a static codegen/build-flag one.
|
||
>
|
||
> **Fix:** `Makefile.starkernel`'s amd64 `ARCH_CFLAGS` now appends `-fno-pic -fno-pie`,
|
||
> overriding `COMMON_CFLAGS`'s `-fPIC` for amd64 only (GCC takes the last flag on the
|
||
> command line; `ARCH_CFLAGS` is appended after `-fPIC` in `COMMON_CFLAGS`'s definition).
|
||
> amd64 is a fixed-base, statically-linked image with no dynamic-linker use for PIC in the
|
||
> first place, so this is a correctness fix, not a workaround. aarch64/riscv64 keep
|
||
> `-fPIC` — riscv64's loader link step (`ld -shared -Bsymbolic`) genuinely requires it and
|
||
> fails to link without it; aarch64 was never observed to hit this bug (different
|
||
> toolchain, `clang`+`lld-link`, different codegen heuristics). Also removed
|
||
> `-DPLATFORM_TIME_NO_INLINE` from `COMMON_CFLAGS` (and its now-redundant explanatory
|
||
> comment) — a prior one-off workaround for the identical bug class, applied specifically
|
||
> to `sf_monotonic_ns()`'s access to `sf_time_backend`, made unnecessary once amd64 got
|
||
> the real fix. Confirmed no regression on any architecture: all three still boot to
|
||
> `ok>` and pass the full self-test with the flag removed. `shim.c`/
|
||
> `physics_hotwords_cache.c`'s own local `#define PLATFORM_TIME_NO_INLINE` (their concrete,
|
||
> non-inline implementations of `sf_monotonic_ns()` etc.) were left as-is — out of scope
|
||
> for this fix, and harmless either way.
|
||
>
|
||
> **Also fixed as a side effect, kept though not the active bug:** `elf_apply_relocations()`
|
||
> (`src/starkernel/boot/elf_loader.c`) didn't handle `R_X86_64_PC32`/`R_X86_64_PLT32`
|
||
> either, discovered while chasing an earlier (wrong) theory that this was a runtime ELF
|
||
> relocation bug. That code path turned out to be dead for this build — `uefi_loader.c`
|
||
> calls `kernel_main()` as a direct function call under `MONOLITHIC_BUILD` (the default
|
||
> here), never invoking `elf_load_kernel()`/`elf_apply_relocations()` at all; the actual
|
||
> boot image is a standard PE32+ UEFI application, relocated by OVMF's own PE loader, not
|
||
> by this custom ELF loader. The relocation-type gap is real for the non-monolithic
|
||
> split-build path though (`elf_load_kernel()` returns 0 — hard failure — on any
|
||
> unhandled type, and the loop aborts the rest of that RELA section on the first one hit),
|
||
> so the handling was kept as a legitimate robustness fix rather than reverted.
|
||
>
|
||
> **Process note:** GDB+QEMU is confirmed unusable for debugging this kernel — the custom
|
||
> UEFI loader relocates/loads the image such that static-symbol software breakpoints never
|
||
> fire, and a hardware breakpoint (`hbreak`) not only never fired but its mere presence
|
||
> caused a different, more severe corruption (`BIRTH` itself became `UNKNOWN WORD`) before
|
||
> any breakpoint triggered — likely a parity/dict-hash boot-gate reacting to the debugger
|
||
> session, not "timing perturbation" as first guessed. Print-based bisection
|
||
> (`console_puts`/`print_uint`, plus `log_message(LOG_ERROR, ...)` — `LOG_INFO` is below
|
||
> the active log threshold and never appears in the serial log, a separate dead end closed
|
||
> along the way) is the only viable method for this kernel today.
|
||
>
|
||
> **Blocker found 2026-08-06, ruled and fixed 2026-08-07 — item 4.1 and item 4.2 silently
|
||
> share one finite per-VM reservoir, and word-execution admission alone can exhaust it
|
||
> before any application-level allocation runs. This failed the K≡1.0 `Done when` bullet
|
||
> below and was not a code bug to just patch — it was a design question spanning both
|
||
> items, reported for a ruling rather than resolved unilaterally (§25.0 rule 3). Captain
|
||
> Bob ruled option 4 below (reserve a floor); implementation and result are at the end of
|
||
> this note.**
|
||
>
|
||
> After the `Q.SLOT` admission-heat fix (below) closed the original `MSG-SEND`/`CH-ACCEPT`
|
||
> over-admission bug, `HERMES-K` still read `0` instead of `65536`. Three prints in one
|
||
> boot discriminated the cause: `stadium_reservoir_peek(Hermes)` reads `65536` immediately
|
||
> after `BIRTH` (the one-time grant, item 4.1a, is fine) but is already `0` — and
|
||
> `COMMON-CH`'s own heat is already `0` — immediately after `CD-INIT` finishes, before
|
||
> `HERMES-MSG-TEST`/`MSG-DELIVER-ALL`/anything else in the self-test runs. So this is not a
|
||
> Stadium cell getting silently reassigned out from under `COMMON-CH` after the fact
|
||
> (aliasing); `COMMON-INIT`'s own `CH-ALLOC` call, partway through `CD-INIT`, never got
|
||
> funded in the first place.
|
||
>
|
||
> Root cause: `stadium_word_dispatch()` (item 4.1, `stadium_words.c:111`) pulls
|
||
> `STADIUM_WORD_HEAT_QUANTUM` (2048) from the dispatching VM's reservoir on **every single
|
||
> word dispatch**, not just the first time a word is admitted — the "already resident"
|
||
> branch (line 142) does `h->heat += stadium_reservoir_pull(vm_id, STADIUM_WORD_HEAT_QUANTUM)`
|
||
> unconditionally, every call. `CD-INIT`'s own `MSG-INIT-FREE`/`CH-INIT-FREE`/
|
||
> `MBR-INIT-FREE` loops alone dispatch several hundred words (32 + 16 + 64 iterations, each
|
||
> several words deep) before `COMMON-INIT` ever runs. At 2048 per dispatch, a VM's entire
|
||
> 65536 reservoir is exhausted by roughly 32 total word dispatches — trivially reached
|
||
> within `CD-INIT`'s first loop, let alone the rest of Hermes's boot. The boot log's own
|
||
> `promotions=145` figure (Hermes's dict-check diagnostics) makes this arithmetic visible
|
||
> directly: 145 × 2048 = 296,960, about 4.5× her entire conserved share, from
|
||
> word-execution tracking alone. This applies to any VM doing non-trivial work, not
|
||
> something specific to Hermes or to messages/channels — Hera's own reservoir has read `0`
|
||
> in every log this entire session, for the same reason, just never surfaced as a problem
|
||
> because nothing previously tried to spend Hera's reservoir on anything else.
|
||
>
|
||
> Options, no ranking, not decided here:
|
||
> 1. **Separate reservoirs per VM** — one for word-execution tracking (item 4.1), one for
|
||
> application-level use (item 4.2 and whatever comes after it). Most invasive: splits
|
||
> `stadium_quotas[slot].reservoir` or the one-time grant itself, touches item 4.1's
|
||
> already-shipped design and its recorded DoE baseline.
|
||
> 2. **Exempt certain VMs from word-execution admission entirely** — e.g., only Hera (or
|
||
> only VMs with no item-4.2-style application economy) get word-heat tracking. Requires
|
||
> a new per-VM-class distinction that doesn't exist today.
|
||
> 3. **Re-scope `STADIUM_WORD_HEAT_QUANTUM`** — smaller, or charged per-unique-word instead
|
||
> of per-dispatch. Touches a Kconfig default that already feeds item 4.1's recorded DoE
|
||
> measurements; re-tuning it here could invalidate that baseline.
|
||
> 4. **Reserve a floor within the shared reservoir** that word-execution admission cannot
|
||
> dip below, mirroring `COMMON-CH`'s own `Q.1/3` floor pattern but at the reservoir
|
||
> level instead of a single resident. New mechanism, not yet designed.
|
||
>
|
||
> **Ruling, 2026-08-07: option 4.** Implemented as `word_dispatch_pull()`
|
||
> (`stadium_words.c`), a static helper wrapping `stadium_reservoir_pull()` for
|
||
> `stadium_word_dispatch()`'s two call sites only (both the already-resident re-heat pull
|
||
> and the not-yet-resident starter-grant pull) — clamped so a pull never takes the
|
||
> reservoir below `Q48_ONE / 3`, the same "VM-COUNT=3 fair share" figure `COMMON-CH`'s own
|
||
> floor already uses, not a new invented number. Application-level pulls
|
||
> (`stadium_reservoir_pull()` called directly, e.g. via `STADIUM-RES-PULL`) are untouched —
|
||
> only word-execution admission respects the ceiling on its own consumption. Verified: the
|
||
> eviction-credit demo now shows a real transfer (`resident_sum` −1612, `reservoir` +1612,
|
||
> exactly, when `COMMON-CH` is evicted) instead of the prior `0`→`0` no-op, and the
|
||
> Stadium's own conservation line closes exactly on every boot, every architecture:
|
||
> `resident_sum=43691 reservoir=21845 sum=65536`.
|
||
>
|
||
> This alone brought `HERMES-K` from `0` to `43002` — real, but not exact, because
|
||
> `HERMES-K`'s formula (`MSG-TOTAL-HEAT CH-TOTAL-HEAT + STADIUM-RES@ +`) has no term for
|
||
> word-execution residents' heat, which the floor now deliberately leaves nonzero. Second
|
||
> ruling, same date: **add that term.** New accessor `stadium_words_resident_heat(vm_id)`
|
||
> (`stadium_words.c`) sums heat over only a VM's own word-execution residents (walking its
|
||
> `word_slots` map, not `stadium_resident_sum()`'s full ownership scan, which would double-
|
||
> count messages/channels already in `MSG-TOTAL-HEAT`/`CH-TOTAL-HEAT`), exposed as an
|
||
> eighth `STADIUM-*` primitive, `STADIUM-WORD-HEAT ( -- heat )`, same implicit-self
|
||
> discipline as the other seven. `HERMES-K` becomes
|
||
> `MSG-TOTAL-HEAT CH-TOTAL-HEAT + STADIUM-RES@ + STADIUM-WORD-HEAT + ;`. Confirmed on all
|
||
> three architectures: `HERMES-K` prints exactly `65536`, K≡1.0, closing the item's
|
||
> headline invariant.
|
||
>
|
||
> *Done when:*
|
||
> - The eight `STADIUM-*` FORTH primitives exist, are kernel-only (not in the shared/
|
||
> vendored word set), and are exercised by at least one Hermes word each.
|
||
> - `stadium_owner[idx]` is written correctly on both the free-list-pop and
|
||
> eviction-fallback paths in `stadium_admit()`, verified by a resident cell's
|
||
> evict-credit landing in the correct VM's reservoir with two VMs holding quotas
|
||
> (Hera + Hermes) — not just asserted from reading the code.
|
||
> - `VM.stadium_vm_id` (or equivalent name chosen at implementation time) exists under
|
||
> `__STARKERNEL__`, is set correctly at Hermes's birth, and all three `vm_core.c`
|
||
> `stadium_word_dispatch()` call sites pass it instead of the hardcoded
|
||
> `vm_uuid_hera()` — verified by a Hermes-dispatched word's heat landing in Hermes's
|
||
> own reservoir, not Hera's, with both VMs' conservation checks closing independently.
|
||
> - Hermes's message and channel lifecycle (`MSG-ALLOC`/`MSG-FREE-NODE`, `CH-ALLOC`/
|
||
> `CH-FREE-NODE`) run entirely through Stadium admission/eviction — no parallel free
|
||
> list, no parallel heat field. Per §11, this is atomic: `MSG-HEAT@/!`, `MSG-COOL-ONE`,
|
||
> `MSG-COOL-ALL`, `CH-HEAT@/!`, `CH-COOL-ALL`, `CH-TOTAL-HEAT`, `MSG-TOTAL-HEAT` either
|
||
> come out in this same change or are rewritten to read/write the Stadium cell instead
|
||
> of a local field — never both mechanisms live at once. **`MBR-ALLOC`/`MBR-FREE-NODE`
|
||
> ruled out of scope, 2026-08-07 — see below.**
|
||
>
|
||
> **Ruling, 2026-08-07: `MBR-ALLOC`/`MBR-FREE-NODE` stay on their own free list, not
|
||
> migrated onto the Stadium.** This bullet originally named them alongside `MSG-*`/`CH-*`.
|
||
> Checked the actual record layout (`capsules/hermes/init.4th`): an MBR record has exactly
|
||
> two fields, `MBR-NEXT@` (link) and `MBR-VM@` (owning VM id) — a pure channel-membership
|
||
> relationship, no heat field, never had one. The bullet's own stated purpose is "no
|
||
> parallel free list, no parallel heat field" — for MBR, "no parallel heat field" is
|
||
> already true vacuously, since none exists to be parallel to. Forcing MBR records through
|
||
> `stadium_admit()`/`stadium_evict()` would mean inventing a heat/mass/behaviour for
|
||
> something structurally without either, spending Stadium cells and reservoir budget on
|
||
> records the item's actual design goal (a conserved, evictable-under-pressure heat
|
||
> economy) has no reason to govern — "does VM X belong to channel Y" is not a quantity
|
||
> that cools, competes for capacity, or needs eviction pressure. Their original inclusion
|
||
> in this bullet reads as a completeness gesture written before the field layout was
|
||
> checked, not a deliberate requirement. `MBR-ALLOC`/`MBR-FREE-NODE`'s own free list
|
||
> (`capsules/hermes/init.4th`, unchanged this item) is correct as-is.
|
||
> - Blocks 4110–4113 (Artemis) are untouched, per `HERMES.md`'s block-map lock. Any new or
|
||
> changed Hermes block is verified with `mkcapsule --lint` before commit, per
|
||
> `experiments/bare_metal/README.md`.
|
||
> - The POST suite (regression gate per §10) passes.
|
||
> - **The effort number is recorded explicitly** — per §10, "what Hermes costs is the
|
||
> multiplier for everything else." Report at minimum: wall-clock/session time spent,
|
||
> lines changed (FORTH + the eight-primitive C surface, split out), and file count
|
||
> touched, so 4.3/4.4 can be estimated from a real data point rather than guessed.
|
||
> - All three architectures boot to `ok>`/`zuse)ok>` with logs under `logs/`, and
|
||
> Hermes's own conservation check (K≡1.0 across messages + channels + reservoir) closes
|
||
> exactly, reported the same way item 4.1 reported `resident_sum`/`reservoir`/`sum`.
|
||
>
|
||
> **Effort number, reported 2026-08-07:**
|
||
> - **Session time.** This conversation's own boot-log timestamps span roughly 10 hours
|
||
> elapsed (`logs/20260806-153504` through `logs/20260807-013712`), covering: the amd64
|
||
> GOT-indirect-addressing corruption investigation and fix (unrelated to Stadium logic,
|
||
> committed separately as `0a7f144`), the item-4.2 acceptance-status survey against this
|
||
> punch-list entry, the `Q.SLOT` admission-heat fix, the word-execution reservoir-floor
|
||
> fix, and the `STADIUM-WORD-HEAT` addition that closed K≡1.0. This does **not** include
|
||
> whatever time the original seven-primitive implementation and capsule migration
|
||
> (already in place when this session's survey began) cost in an earlier session — no
|
||
> visibility into that, not estimated rather than guessed.
|
||
> - **Lines changed, split FORTH vs. C surface** (`git diff --stat`, this session's
|
||
> contribution only — the pre-existing implementation's own diff is included since it
|
||
> was still uncommitted when measured, but its authorship/timing is the caveat above):
|
||
> - FORTH (`capsules/hermes/init.4th`): +116 / −45 (161 changed), 1 file.
|
||
> - C, the eight-primitive `STADIUM-*` surface + Stadium core (`mama_forth_words.c`,
|
||
> `stadium.c`, `stadium_words.c`, `stadium.h`, `stadium_words.h`, `vm.h`): +511 / −69
|
||
> (580 changed), 6 files.
|
||
> - C, other wiring (`capsule_birth.c`, `sk_vm_bootstrap.c`, `vm_core.c`,
|
||
> `dictionary_management.c`): +13 / −6 (19 changed), 4 files.
|
||
> - Self-test scaffolding (`kernel_main.c`, diagnostic-only, not production code):
|
||
> +119 / −0, 1 file.
|
||
> - **Total: 12 implementation files, +759 / −120 (879 lines changed).**
|
||
> - **File count:** 12 implementation files (13 including this write-up in `FABRIC.md`
|
||
> itself).
|
||
- [ ] **4.3 — Console.** Settles 1.11 as part of the work. *Refs:* §17.5.
|
||
|
||
> **Note, 2026-08-05: Captain Bob wants a discussion before any work starts on this item.**
|
||
> Do not begin 4.3 on an unblock-and-go basis the way 4.1 was — raise it and wait.
|
||
>
|
||
> **Discussion held 2026-08-07.** `.claude/CONSOLE.md` is a rough prior working draft,
|
||
> superseded — not edited further, not treated as authoritative. Console's design lives
|
||
> in this document from here on. First slice broken out below as 4.3.1–4.3.4. Explicitly
|
||
> out of scope for all four: raster image (PNG/JPEG) rendering as fabric backgrounds —
|
||
> real direction, raised 2026-08-07, deliberately deferred past this slice; also fonts,
|
||
> scrolling, cursor/VT100 semantics, the Hermes message protocol, and Console as a fleet
|
||
> VM under Hera's birth protocol — later 4.3.x items, scoped once this slice is reviewed.
|
||
|
||
- [x] **4.3.1 — Framebuffer sanity: draw a test pattern.** Confirm `framebuffer.c` is wired
|
||
to the real UEFI GOP `BootInfo` and draw a simple orientation-revealing test pattern, using
|
||
the existing raw pixel primitives only — no coordinate/Z machinery yet. *Refs:* §27.1.
|
||
|
||
> **Done, 2026-08-07.** `fb_draw_orientation_test()` added to `framebuffer.c`/`.h` — fills
|
||
> the four raster corners RED/GREEN/BLUE/YELLOW via `fb_fill_rect` only. Wired into
|
||
> `kernel_main.c` calling `fb_init()` directly; `console_fb_init()`/`vt100_init()` removed
|
||
> from the boot path per Captain Bob's direction (vt100.c/console.c are obsolete, superseded
|
||
> by the fabric redesign, not to be exercised even incidentally).
|
||
>
|
||
> **Bug found and fixed, not scope creep — the diagnostic did its job.** First screendump
|
||
> (via 4.3.2) showed a clean R↔B channel swap (G correct, R and B corners exchanged) —
|
||
> spatial placement was correct, so this ruled out flip/rotation but caught a real color
|
||
> bug: `framebuffer.c`'s `pack_pixel()` had its `FB_PIXEL_RGBX32`/`FB_PIXEL_BGRX32` branches
|
||
> swapped relative to UEFI GOP's own byte-order naming convention (pre-existing bug, not
|
||
> introduced this item). Fixed by swapping the two `pack_pixel` return bodies to match
|
||
> `framebuffer.h`'s already-correct doc comments; `kernel_main.c`'s GOP-format `switch`
|
||
> needed no change. Re-verified via a second screendump: all four corners render correctly
|
||
> (`fb/qemu-screenshot-20260807-113612.png`).
|
||
>
|
||
> Not addressed, not in scope: the pre-existing UEFI loader boot-log text remains visible
|
||
> behind the corner blocks, since this diagnostic paints four small rectangles and does not
|
||
> clear the framebuffer — expected, not a bug.
|
||
|
||
- [x] **4.3.2 — QEMU screenshot capability.** Add a monitor/QMP socket to the `qemu` targets
|
||
(mirroring the existing serial-socket pattern) so `screendump` can be issued and the 4.3.1
|
||
test pattern actually inspected. None exists today — all three targets currently run with
|
||
`-display none` and no monitor attached. *Refs:* §27.2.
|
||
|
||
> **Done, 2026-08-07 — mechanism already existed, didn't need building.**
|
||
> `scripts/qemu_screenshot.sh` was already a complete, working amd64 screendump path
|
||
> (monitor UNIX socket + `socat` + HMP `screendump`), just not wired into any
|
||
> `Makefile.starkernel` target and not previously exercised this session — 34 prior
|
||
> screenshots already sat in `logs/` from earlier use. Changed: output PNG now goes to a
|
||
> new top-level `fb/` directory (tracked in git, per Captain Bob — not `logs/`, not a
|
||
> gitignored temp dir); added a `python3`+PIL fallback for PPM→PNG conversion since
|
||
> `imagemagick` isn't installed on this machine. Left as a standalone script, not wired into
|
||
> a Makefile target, per direction — run directly for now. aarch64/riscv64 not covered by
|
||
> this script; not needed for 4.3.1's amd64-only diagnostic.
|
||
|
||
- [x] **4.3.3 — Cartesian coordinate machinery.** Origin bottom-left `(0, 0)`, Y-up, plus a
|
||
new Z axis (depth-into-screen, not height) and a fixed orthographic projection as a
|
||
placeholder — not the final projection, no perspective/camera work yet. **Angle settled
|
||
2026-08-07: true 45° cavalier.** New C primitives `PLOT ( x y color -- )`, `FB-WIDTH`,
|
||
`FB-HEIGHT` (raw hardware boundary, no Cartesian awareness); new FORTH capsule
|
||
`capsules/fabric.4th` (blocks 4900+) for `PROJECT`/`CART-Y`/`CART-PLOT`, per the
|
||
compose-in-FORTH-first rule — the transform is policy, not hardware access. *Refs:* §27.3.
|
||
|
||
> **Done, 2026-08-07.** `register_framebuffer_words()` (Module 28) adds `PLOT`/`FB-WIDTH`/
|
||
> `FB-HEIGHT` — kernel-only, no-op on hosted builds, same pattern as every other module.
|
||
> `capsules/fabric.4th` (blocks 4900–4902, lint-clean per `mkcapsule --lint`) defines
|
||
> `COS45`/`Z->DELTA`/`PROJECT`/`CART-Y`/`CART-PLOT`.
|
||
>
|
||
> **A second real bug found and fixed, not scope creep.** Live-tested `CART-PLOT` over the
|
||
> serial socket (same injection technique the DoE machinery uses) and hit a silent `ERROR`
|
||
> on the capsule's own `VARIABLE ZD`, while an identical `VARIABLE` typed live at the REPL
|
||
> worked fine. Traced to `defining_word_variable()` (`defining_words.c:471`): it captures
|
||
> `vm->here` as the variable's address with no alignment call first, and `vm_load_cell`/
|
||
> `vm_store_cell` require 8-byte-aligned addresses. `ZD` landed at `945` (misaligned) purely
|
||
> because of what preceded it in the capsule; `TESTV`/`ZD2` defined live happened to land on
|
||
> aligned addresses by luck. This is a real deviation from FORTH-83/ANS, which specifies
|
||
> `VARIABLE` reserves an *aligned* cell. Fixed with one line (`vm_align(vm)` before capturing
|
||
> `addr`) — `ALIGN` already existed as a word (`dictionary_words.c`) but `VARIABLE` wasn't
|
||
> calling it. Fixes every `VARIABLE` in the system, not just this capsule's — other capsules
|
||
> (`doe.4th`, `init-4.4th`) were landing aligned by luck, not by guarantee. Both hosted and
|
||
> kernel builds recompiled clean after the fix.
|
||
>
|
||
> **Verified end-to-end**, amd64, via the same manual-injection + `screendump` technique:
|
||
> plotted 4 marker points (origin, +100 X, +100 Y, +50 Z; a 3×3 cluster each for visibility)
|
||
> and confirmed all four landed at hand-calculated raster coordinates — including the
|
||
> diagonal up-right shift for the Z-axis point, confirming the 45° cavalier projection math
|
||
> is correct, not just non-crashing. Screenshot: `fb/fabric-test-cart-plot.png`. 4.3.1's
|
||
> corner diagnostic still renders correctly in the same shot — no regression.
|
||
>
|
||
> Not wired into `init.4th`'s boot chain, per plan — Console isn't a fleet VM yet.
|
||
|
||
- [x] **4.3.3a — Q48.16 trigonometry.** `Q.SIN`/`Q.COS` (radian input) added to `q48_16.c`,
|
||
Taylor series after range-reducing into `[-π, π]` — same pattern as this file's existing
|
||
`Q.LOG`/`Q.EXP`/`Q.SQRT`, not a new precedent. Raised 2026-08-07 while scoping 4.3.3: needed
|
||
by 4.3.3b, does not exist anywhere in this codebase today (checked). *Refs:* §27.3.
|
||
|
||
> **Done, 2026-08-07.** `q48_reduce_angle()` (single integer division on the raw Q48.16
|
||
> representations to strip full `2·PI_Q48` turns, then a bounded fix-up loop) plus
|
||
> `q48_sin_approx`/`q48_cos_approx` (Taylor series, terms `n=3,5,7,9,11` / `n=2,4,6,8,10`,
|
||
> early exit below 10). `PI_Q48 = 205887`; `TWO_PI_Q48` is *derived* as `2·PI_Q48` rather
|
||
> than independently rounded, so the ±π reduction boundary has no seam.
|
||
>
|
||
> **A real duplication, not previously flagged:** this codebase has *two* independent
|
||
> Q48.16 implementations — `src/word_source/q48_16_words.c` (vendored/hosted) and
|
||
> `src/starkernel/math/q48_16.c` (kernel-only; the kernel build does not compile the
|
||
> former at all). Found the hard way — the hosted build linked fine, the kernel build
|
||
> failed with `undefined reference to q48_sin_approx` until the same two functions were
|
||
> added to both files (plus both `q48_16.h` headers — `include/q48_16.h` and
|
||
> `include/starkernel/q48_16.h`, which also declare the same functions independently).
|
||
> Not fixed at the root (de-duplicating the two implementations is a much larger change
|
||
> than this item), just navigated correctly — `Q.LOG`/`Q.EXP`/`Q.SQRT` already had this
|
||
> same four-file duplication, unremarked until now.
|
||
>
|
||
> **Verified live on amd64** via serial injection: `sin(0)=0`, `cos(0)=65536` (exact),
|
||
> `sin(π/2)=65536`, `cos(π/2)=0` (exact), `sin(-π/2)=-65536` (exact, confirms the odd-
|
||
> function sign handling), `sin(π)≈-27` (residual from `PI_Q48` rounding, ~0.04%),
|
||
> `cos(π)≈-65656` (Taylor truncation near the interval edge, ~0.18%), and `sin(3π)` reduces
|
||
> to the same `-27` as `sin(π)`, confirming range reduction across multiple turns. Both
|
||
> hosted and kernel (amd64) builds clean.
|
||
|
||
- [x] **4.3.3b — Geometry drawing primitive wordset.** `LINE`, `CIRCLE`, `ARC`, `ELLIPSE` in
|
||
`capsules/fabric.4th`, built on 4.3.3's `PLOT`/`CART-PLOT` and 4.3.3a's `Q.SIN`/`Q.COS`.
|
||
Raised 2026-08-07. Q48.16 throughout; resolution-agnostic (48 integer bits comfortably
|
||
covers 1080p and well beyond — no hardcoded viewport assumptions). *Refs:* §27.3.
|
||
|
||
> **Done, 2026-08-07.** Blocks 4903–4912. `TO-RASTER` factored out of `CART-PLOT` (same
|
||
> behavior, not a change) so `LINE` can project both endpoints once and Bresenham the
|
||
> straight line between them in raster space — valid because the cavalier projection is
|
||
> linear, so projecting endpoints and interpolating is equivalent to projecting every point
|
||
> along the line. `LINE` itself split across three helper words (`LINE-SETUP`,
|
||
> `LINE-DONE?`/`LINE-STUCK?`, `LINE-STEP`) — discovered mid-implementation that colon
|
||
> definitions **cannot span block boundaries** in this capsule loader (verified with a
|
||
> throwaway test capsule: the continuation lands in a `[CAPSULE][DEFER]` path that never
|
||
> resolves and errors out), so anything too long for one 16-line/64-char block has to be
|
||
> factored into separate, block-local word definitions instead. `CIRCLE`/`ELLIPSE` are
|
||
> 36-segment polygon approximations (`LINE` calls between consecutive `Q.SIN`/`Q.COS`
|
||
> points); `ARC` is the same at 18 segments over a caller-supplied `[a0, a1]` radian range.
|
||
>
|
||
> **A fourth real bug, this one serious — found, fixed, verified with the recommended fix
|
||
> applied both times.** `CIRCLE`'s first live test rendered only its first quadrant, then
|
||
> a follow-up test call hung the VM for several minutes before being killed. Root cause:
|
||
> `q48_to_u64()` (`include/q48_16.h` and `include/starkernel/q48_16.h`, backing
|
||
> `Q.TO-INT`) did `q >> 16` as an **unsigned logical shift**. For any negative `q48_16_t` —
|
||
> inevitable once `Q.SIN`/`Q.COS` leave the first quadrant — this produces a huge garbage
|
||
> integer instead of sign-extending. That garbage became a bogus `LINE` target, and
|
||
> `LINE-STEP`'s Bresenham loop had no bound, so it churned for a very long time trying to
|
||
> converge on a point that was effectively unreachable. Fixed by shifting through a signed
|
||
> `int64_t` intermediate (bit-identical output for the non-negative case, which is all the
|
||
> inference engine's own caller ever produces). Independently, added `LINE-STUCK?`
|
||
> (`LSTEPS` counter vs. `FB-WIDTH + FB-HEIGHT`, the true worst case for any on-screen line)
|
||
> as a defense-in-depth cap, so a future bad target degrades to "stops drawing" rather than
|
||
> hanging the VM again.
|
||
>
|
||
> **Verified live on amd64**, fresh boot after both fixes: `-65536 Q.TO-INT .` now prints
|
||
> `-1`. `LINE`, `CIRCLE`, `ARC` (semicircle, 0 to π), and `ELLIPSE` all completed without
|
||
> hanging or erroring, and a combined screendump shows all four rendering correctly and
|
||
> distinctly — full circle, correct upper-half arc, properly proportioned ellipse (wider
|
||
> than tall, matching unequal radii), and the earlier diagonal `LINE` test.
|
||
> `fb/amd64/geom-test-circle-fixed.png`, `fb/amd64/geom-test-full-wordset.png`.
|
||
|
||
- [x] **4.3.4 — Checkpoint: draw a cube.** First real exercise of the 4.3.3/4.3.3a/4.3.3b
|
||
coordinate/projection/geometry machinery — cube edges use `LINE`. Stop and review here
|
||
before scoping the next 4.3.x item — not expected to be fast. *Refs:* §27.4.
|
||
|
||
> **Done, 2026-08-07.** Block 4913–4915. Vertices are bit-coded: `VERT ( n -- x y z )`
|
||
> reads bits 0/1/2 of `n` as the sign of the X/Y/Z offset from center (`±CS`), so all 8
|
||
> corners come from one word instead of 8 hand-written coordinate triples. `EDGE
|
||
> ( n1 n2 color -- )` resolves both corners via `VERT` and calls `LINE`. `CUBE
|
||
> ( cx cy cz s color -- )` is 12 `EDGE` calls — 4 bottom, 4 top, 4 vertical — grouped by
|
||
> face for readability, not because the grouping means anything to the machinery.
|
||
>
|
||
> No new bugs this item — first time in the 4.3.3.x sequence that's been true, which is
|
||
> itself a small signal that `Q.TO-INT`/the `VARIABLE` alignment fix/the `LINE-STUCK?`
|
||
> cap were the real gaps, not something still lurking in `LINE`/`PROJECT`/`CART-Y`.
|
||
>
|
||
> **Verified live on amd64**: `640 400 0 100 16777215 CUBE` (white, half-size 100,
|
||
> centered mid-screen) completed cleanly, no errors, no `LINE-STUCK?` trips. Screendump
|
||
> (`fb/amd64/cube-4.3.4.png`) shows a correct wireframe cube — front face square, back
|
||
> face square offset diagonally up-right by exactly the 45° cavalier projection's
|
||
> depth term, all 12 edges connecting at the right corners, no crossed or broken lines.
|
||
>
|
||
> **This is the checkpoint** — 4.3.x groundwork stops here for review per this item's own
|
||
> acceptance criterion, before scoping whatever comes next.
|
||
|
||
⋯ *(4.3.x is open-ended — more items get appended here as Console work is scoped item by*
|
||
*item, developed on the fly per §25.0. 4.4 below is unaffected by anything added above*
|
||
*this marker.)*
|
||
|
||
- [ ] **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.
|
||
|
||
> **Note to self, flagged by Captain Bob 2026-08-04, before item 5.1.** Currently
|
||
> invisible: with Tripod pruned to Hera alone (item 0.1), `others_total` is always 0, so
|
||
> this path is never exercised — nothing today can trip it. It becomes reachable, and
|
||
> therefore measurable, the moment Phase 4 restores Hermes/Artemis. Check this before
|
||
> trusting item 5.1's DoE re-run as evidence that `VM-CONSERVED?` holds: a clean run on a
|
||
> document this careful about falsifiability elsewhere, sitting on top of an unmeasured,
|
||
> monotonic leak, would be a false negative, not a green light. Still reported-not-
|
||
> scheduled on purpose — becomes its own item only if Captain Bob says so.
|
||
- `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`.
|
||
- **Kconfig/`menuconfig` has never been exercised end-to-end.** Every Kconfig knob added so
|
||
far, including item 4.1's `STADIUM_WORD_HEAT_QUANTUM`/`STADIUM_WORD_COOL_RATE_Q48`, has only
|
||
ever been verified via its `Makefile.starkernel` `kconfig_int`/`kconfig_bool` default. Nobody
|
||
has run `make -f Makefile.starkernel menuconfig`, changed a value, and confirmed it actually
|
||
flows through to a build. Flagged by Captain Bob 2026-08-05.
|
||
- **`stadium_admit()` never writes `stadium_owner[idx]`**, on either the free-list-pop or the
|
||
eviction-fallback path (found during item 4.1's design pass, 2026-08-05). Harmless today —
|
||
every cell's owner byte is `0` (Hera) from `stadium_boot_init()`, and Hera is the only VM
|
||
with a quota — but once item 4.2 restores Hermes, a resident's evict-credit (item 4.1's
|
||
reservoir accounting in `stadium_evict()`) would flow to the wrong VM's reservoir unless
|
||
this is fixed first.
|
||
- **Taxonomy and lexicon.** Raised by Captain Bob 2026-08-04, mid-item-3.1. This document's
|
||
physics-flavored vocabulary (heat, mass, density, patron, Stadium, and the rest) needs a
|
||
glossary that is explicit these are named analogies, not physical claims — and that also
|
||
covers the growing set of Kconfig build knobs (`STADIUM_MAX_VM_COUNT` and its siblings) so
|
||
the terminology in code, Kconfig help text, and this document stays one language instead
|
||
of drifting apart. Not scoped, not placed in a phase. Captain Bob: "I guess that we didn't
|
||
finish out FABRIC.md quite as much as we thought."
|
||
|
||
### 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.
|
||
|
||
---
|
||
|
||
## 26. The hardware heartbeat must itself be adaptive — RULED 2026-08-03
|
||
|
||
Raised mid-0.8: the punch list, as written, makes the hardware tick a fixed-rate
|
||
instrument (100 Hz, unconditionally, on all three architectures — the `apic_timer_init(...,
|
||
100)` calls built across items 0.1–0.7). That is correct for what §18.4/§18.5 require of
|
||
the *engine* — the virtual tick stays execution-paced regardless. But it leaves the
|
||
*physical* heartbeat monotonic, and the physical heartbeat was never supposed to be
|
||
monotonic. Captain Bob: *"the heartbeat is adaptive... it spreads the heartbeat out when
|
||
your heart goes faster when you're running... it's gotta be an adaptive heartbeat, that's
|
||
the whole thing to cage variance."*
|
||
|
||
### 26.1 The finding — an adaptive-rate engine already exists, and it is orphaned
|
||
|
||
`vm_runtime.c:703-752` ("Loop #7 — Adaptive Heartrate") computes a bounded adaptive period,
|
||
`vm->heartbeat.tick_target_ns`, from the same ANOVA-driven stability signal Loop #5 already
|
||
uses: early-exit (stable) slows it down, full-inference (volatile) speeds it up, ±25% per
|
||
step, clamped to `[¼×, 4×]` of a configured base. This is real, executing code, faithful to
|
||
the design in the sibling StarForth repo's own
|
||
`docs/working/architecture/03-architecture/heartbeat-system/architecture.md` (Option A vs.
|
||
Option B). It is not a proposal — it already runs, on every `vm_tick()`.
|
||
|
||
It is orphaned. `tick_target_ns` is written to `vm->heartbeat.worker->tick_ns`
|
||
(`include/vm.h:286,289`), and `worker` is always `NULL` in kernel builds — nothing in
|
||
`src/starkernel/` reads `tick_target_ns` at all. The mechanism that was meant to *consume*
|
||
it, a `pthread_create()`-based background worker (`heartbeat_thread_main()`, vendored into
|
||
`vm_bootstrap.c:310`), is deliberately and redundantly disabled for kernel builds
|
||
(`Makefile.starkernel:293,338`, `HEARTBEAT_THREAD_ENABLED` forced to `0` twice) — correctly:
|
||
this is a bare-metal single-hart kernel, there is no pthread implementation, and the
|
||
mechanism's own history (`segfault-analysis.md` in the StarForth repo) is a real
|
||
concurrent-access bug against `RollingWindowOfTruth`, fixed by a mutex a single hart doesn't
|
||
need and can't cheaply provide (§21.2, item 0.9).
|
||
|
||
So: the *decision logic* is real, tested by inheritance, and currently produces a number
|
||
nothing downstream ever reads. Phase 0 as written would ship a heartbeat that looks adaptive
|
||
in the source tree and is not adaptive on the wire.
|
||
|
||
### 26.2 This does not reopen GAP-A1
|
||
|
||
§18.5 already proved the general shape of this argument for Loop #5 and is directly
|
||
reusable for Loop #7: **adaptation is safe exactly when its inputs are execution-derived**,
|
||
because then the *decision* to change the period is itself a deterministic function of the
|
||
execution stream, not of wall-clock jitter. §18.5 point 3 already establishes that every
|
||
`InferenceInputs` field feeding this ANOVA machinery — rolling window, trajectory length,
|
||
prefetch hit rate, hot/stale word counts, total heat, word count — is execution-derived with
|
||
zero timing input. Loop #7's stable/volatile classification is downstream of that same
|
||
machinery. Nothing new needs proving there.
|
||
|
||
What must not change, and does not under this design:
|
||
|
||
- The **virtual tick stays the engine's clock** (§18.4, unchanged). Adjusting the physical
|
||
re-arm period changes *when TIME-TRUST samples land and how often the idle path wakes* —
|
||
it does not move decay, reap, or inference off the virtual tick onto the hardware one.
|
||
- The hardware tick's **output** still feeds nothing that reaches the parity hash (§18.5
|
||
points 1, 5, unchanged) — only its *input* (the period it's told to re-arm at) becomes
|
||
execution-derived instead of fixed.
|
||
- What was already true and already inert under §18.5 — that wall-clock interrupt *arrival*
|
||
timing is not reproducible run to run — stays true and stays inert. Nothing patron-facing
|
||
ever depended on it; this design doesn't change that.
|
||
|
||
### 26.3 The scale mismatch, and the ruling
|
||
|
||
`tick_target_ns`'s configured base, `HEARTBEAT_TICK_NS` (`include/starforth_config.h:71`),
|
||
is `10000ULL` — 10 microseconds. Its live range under Loop #7's ±25%/`[¼×,4×]` bounds is
|
||
therefore 2.5µs–40µs. The hardware timer configured throughout items 0.1–0.7 runs at 100 Hz
|
||
— 10 milliseconds. That is a three-orders-of-magnitude mismatch: reprogramming the physical
|
||
re-arm to the literal `tick_target_ns` value would fire the timer 25,000–400,000 times a
|
||
second, which on a bare-metal single-hart kernel means the core spends effectively all its
|
||
time in trap entry/exit and the REPL is never reached. `HEARTBEAT_TICK_NS` was tuned for a
|
||
hosted OS thread's sleep granularity, not a bare-metal ISR period.
|
||
|
||
**RULED (Captain Bob, 2026-08-03):** same relationship, kernel-appropriate scale. The
|
||
mechanism must be real and load-bearing — a genuine, measurable effect on the physical
|
||
re-arm period, the same kind of effect the original hosted pthread experiments showed — but
|
||
computed against the 10 ms / 100 Hz base already established for this kernel, not the 10 µs
|
||
hosted base. Loop #7's *decision logic* (stable → slower, volatile → faster, ±25% per step,
|
||
clamped `[¼×, 4×]`) is reused unmodified; only the base it is applied to changes.
|
||
|
||
### 26.4 The mechanism — no thread needed
|
||
|
||
Captain Bob authorized building a kernel-native thread/task if one were required
|
||
("if we gotta run a thread or whatever, it doesn't matter"). One is not required, and adding
|
||
one would need a preemptive scheduler this single-hart kernel does not have (§21.2 already
|
||
rules out real locking for exactly this reason). The existing shape gets there without new
|
||
infrastructure:
|
||
|
||
- `vm_tick()` already calls Loop #7 on the **mainline path** (execution-paced, never in
|
||
interrupt context) and already produces a fresh `tick_target_ns` there.
|
||
- Item 0.8 already introduces a shared `heartbeat.c` owning the top/bottom-half split. That
|
||
file is the natural owner of one new piece of state: the *current adaptive period*, set by
|
||
a new `heartbeat_set_adaptive_period_ns(uint64_t ns)` (called from `vm_runtime.c`'s Loop #7
|
||
site, scaled to the kernel base per §26.3) and read by a new `heartbeat_next_period_ns(void)`.
|
||
- Each architecture's existing re-arm function (`apic_timer_rearm()`, `riscv64_timer_rearm()`,
|
||
the aarch64 equivalent) already runs in interrupt context at the top of every tick (§18.4's
|
||
"one tick" call sites, unchanged). It converts `heartbeat_next_period_ns()` to that
|
||
architecture's raw counter units — a conversion each already does today for its fixed
|
||
period — instead of using a hardcoded constant.
|
||
|
||
No new concurrency: the write happens on the mainline execution path, the read happens in
|
||
interrupt context, and the value read is whatever was last written — the same single-writer/
|
||
single-reader shape every other piece of ISR-read, mainline-written state in this kernel
|
||
already has (§21.1's finding that locking here is already free, because nothing here is
|
||
actually concurrent on one hart). No pthread, no kernel task, no scheduler.
|
||
|
||
### 26.5 Open, deferred
|
||
|
||
- Multi-VM: today Hera is the only VM, so "whose `tick_target_ns` drives the one physical
|
||
timer" has one answer. Not resolved for when Hermes/Artemis return — deferred, not
|
||
applicable yet (consistent with §20.5's other Tripod-return deferrals).
|
||
- `HEARTBEAT_TICK_NS`'s name and its hosted-scale value are unchanged by this ruling — the
|
||
kernel-side base (10 ms) is a **separate** constant, not a redefinition of the hosted one.
|
||
Naming the kernel constant is an implementation detail of the item that builds this, not a
|
||
document-level open question.
|
||
|
||
**RULED.** Item 0.8 is amended below to include this; no new punch-list item is needed —
|
||
this is squarely inside what 0.8 already builds (`heartbeat.c`, the three re-arm call
|
||
sites).
|
||
|
||
## 27. Console — the drawing fabric (groundwork, 4.3.1)
|
||
|
||
**STATUS: design-stage, 2026-08-07.** Supersedes `.claude/CONSOLE.md` as the authoritative
|
||
Console design document. `CONSOLE.md` was a rough prior working draft and is not edited
|
||
further; nothing in it should be treated as decided just because it is written down there.
|
||
This section covers 4.3.1–4.3.4 only — the groundwork slice: verify the hardware boundary
|
||
works and stand up the coordinate machinery. It is explicitly *not* the full Console
|
||
specification (fonts, scrolling-as-a-VM-behavior, message protocol from Hermes, etc.) —
|
||
those are later items under 4.3, scoped once this slice's checkpoint (4.3.4) is reviewed.
|
||
|
||
### 27.1 The hardware boundary already exists (4.3.1)
|
||
|
||
`console_fb_init()` (`hal/console.c:269`) calls `fb_init()` with real UEFI GOP data from
|
||
`boot_info->framebuffer`, but only after POST completes, immediately before the REPL starts
|
||
(`kernel_main.c:800-807`). `include/starkernel/framebuffer.h` already exposes raw pixel
|
||
primitives: `fb_put_pixel`, `fb_fill_rect`, `fb_draw_glyph` (8×16 cells), `fb_scroll_rows`.
|
||
There is nothing to build to get pixels on screen — 4.3.1's task is *verification*, not
|
||
construction: draw a simple, orientation-revealing test pattern with the existing primitives
|
||
and confirm it displays right-side up.
|
||
|
||
### 27.2 No screenshot capability exists today (4.3.2)
|
||
|
||
All three `qemu` targets in `Makefile.starkernel` run with `-display none` and attach only a
|
||
serial chardev socket (for the log) — no monitor, no QMP socket. There is no way today to
|
||
issue QEMU's `screendump` command. 4.3.2 adds a monitor/QMP socket (mirroring the existing
|
||
serial-socket pattern) so the framebuffer can actually be inspected as a `.ppm` after a run.
|
||
|
||
### 27.3 Coordinate system (4.3.3, 4.3.3a, 4.3.3b)
|
||
|
||
- **Origin bottom-left**, `(0, 0)`. Traditional Cartesian, not raster/top-left-Y-down.
|
||
**Reinterpreted 2026-08-07:** §27.3 originally said the Y-flip "must live at the lowest
|
||
primitive layer," written before the language split (below) was decided. `PLOT` is the true
|
||
hardware boundary and is deliberately raster-native with no Cartesian awareness at all —
|
||
same posture as `BLOCK`/`UPDATE` staying dumb about policy. `CART-Y`, in FORTH, is the
|
||
lowest *Cartesian-aware* layer, which satisfies the original intent (nothing above it ever
|
||
thinks about the flip) even though the flip itself lives one level up from the raw pixel
|
||
write.
|
||
- **Z axis, depth-into-screen** (not height-off-ground). Confirmed 2026-08-07: this is
|
||
heading toward real 3D animation over time, not a single static scene — Z is being added
|
||
now because retrofitting it later is more expensive than building it in from the start.
|
||
- **Projection: fixed orthographic, for now.** Explicitly a placeholder — not the final
|
||
projection, no perspective/camera work yet. **Angle settled 2026-08-07: true 45° cavalier**
|
||
(both X and Z axes drawn at 45° off horizontal) — `sx = x + z·cos45`, `sy = y + z·cos45`.
|
||
Ruled out the 2:1 pixel-art isometric convention (~26.57°); no reason recorded beyond
|
||
preference.
|
||
- **Language: FORTH for the transform, C only for the raw pixel write.** Per the project's
|
||
compose-in-FORTH-first rule — `PROJECT`/`CART-Y`/`CART-PLOT` are policy, not hardware
|
||
access, so they belong in `capsules/fabric.4th`, not in C. Only `PLOT`/`FB-WIDTH`/
|
||
`FB-HEIGHT` are C primitives.
|
||
- **Trigonometry (4.3.3a) and geometry primitives (4.3.3b), raised 2026-08-07 while scoping
|
||
this item.** `Q.SIN`/`Q.COS` (Taylor series, radian input) extend `q48_16.c` the same way
|
||
`Q.LOG`/`Q.EXP`/`Q.SQRT` already do — not a new precedent, just more of the same module.
|
||
`LINE`/`CIRCLE`/`ARC`/`ELLIPSE` build on those plus `PLOT`/`CART-PLOT`, entirely in FORTH,
|
||
Q48.16 throughout. Resolution-agnostic by design — 48 integer bits is vastly more range
|
||
than 1920×1080 needs, checked as a sizing sanity check only, not a hardcoded constraint.
|
||
|
||
### 27.4 Checkpoint: a cube (4.3.4)
|
||
|
||
Acceptance for this whole slice is a cube rendered on screen using the 4.3.3 coordinate/
|
||
projection machinery — the first real exercise of that math, expected to take real effort,
|
||
not a quick add. Stop and review here before scoping the next 4.3.x item. Out-of-scope list
|
||
for 4.3.1–4.3.4 is recorded once, at the 4.3 punch-list entry itself (§25.5), not repeated
|
||
per sub-item.
|