Add stadium_conserved() -- FABRIC-3.6.md task 0.7, item 41
Boolean analogue of vm_physics_conserved(), for the Stadium per-VM
quota invariant rather than fleet-wide execution heat
(FABRIC-3.5.md SXXXIX.4). int stadium_conserved(VMUuid vm_id), in
src/starkernel/vm/stadium.c alongside stadium_resident_sum()/
stadium_reservoir_peek() that it's built from, declared in
include/starkernel/vm/stadium.h.
Implements the two-term form -- resident_sum(vm_id) +
reservoir_peek(vm_id) == Q48_ONE -- not the three-term form SXL.4
rules for the eventual system. That ruling's `consumed` term is a
Phase 2 kernel-Hermes ledger deliverable that doesn't exist yet:
nothing draws on any VM's Stadium quota today (task 2.2 is literally
where that wiring gets built), so consumed is honestly zero right now.
Folding it in as a placeholder would be inventing Phase 2 state ahead
of it existing -- the doc comment says so explicitly, so whoever
builds Phase 2's ledger extends this function rather than working
around it.
Wired into the existing per-VM boot diagnostic
(stadium_words_print_boot_diagnostics(), kernel_main.c:810, Hera
only -- the sole existing call site) rather than adding a new one,
printing CONSERVED/DRIFTED the same shape vm_physics_status() already
uses.
Three-arch boot clean: amd64/aarch64/riscv64 all reach [zuse@Hera] ok>,
zero UNKNOWN WORD, all print "Stadium conservation: CONSERVED" with
identical resident_sum=47641 reservoir=17895 sum=65536=Q48_ONE. No
compiler warnings on either edited file (forced recompile checked).
Authorized by Captain Bob ("Yes.").
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Sonnet 5
parent
9886ad5315
commit
380f0a09c9
+16
-1
@@ -259,8 +259,23 @@ it has simply not been attempted.)*
|
||||
touched, so no 3-arch boot run for this task. All of Phase 0's strips and documentation
|
||||
corrections (0.1–0.6) are now done; `stadium_conserved()` (0.7) and the `PLOT`/`FB-WIDTH`/
|
||||
`FB-HEIGHT` registration audit (0.8) remain before Phase 0's gate is fully met.
|
||||
- [ ] **0.7** — Add `stadium_conserved()`: `Σ patron + reservoir + consumed == Q48_ONE`,
|
||||
- [x] **0.7** — Add `stadium_conserved()`: `Σ patron + reservoir + consumed == Q48_ONE`,
|
||||
**epsilon zero** (§XL.4, item 41). *Check:* true on a clean boot, all three arches.
|
||||
2026-09-19 · `logs/20260919-135137/amd64/`, `logs/20260919-135240/aarch64/`,
|
||||
`logs/20260919-135417/riscv64/` — all three reach `[zuse@Hera] ok>`, zero `UNKNOWN WORD`,
|
||||
and print `Stadium conservation: CONSERVED` (all identical: resident_sum=47641
|
||||
reservoir=17895 sum=65536=`Q48_ONE`). Implemented `int stadium_conserved(VMUuid vm_id)` in
|
||||
`src/starkernel/vm/stadium.c` (declared `include/starkernel/vm/stadium.h`) as
|
||||
`stadium_resident_sum(vm_id) + stadium_reservoir_peek(vm_id) == Q48_ONE` — the **two-term**
|
||||
form, not three. §XL.4's `consumed` term is a Phase 2 kernel-Hermes ledger deliverable that
|
||||
doesn't exist yet; nothing draws on any VM's Stadium quota today (Phase 2 task 2.2 is
|
||||
literally where that wiring gets built), so `consumed` is honestly zero right now and
|
||||
folding it in would be inventing Phase 2 state ahead of it existing. Doc comment on the
|
||||
function says exactly this, so whoever builds Phase 2's ledger extends this function rather
|
||||
than working around it. Wired into the existing per-VM boot diagnostic
|
||||
(`stadium_words_print_boot_diagnostics()`, `kernel_main.c:810`, Hera only — the sole
|
||||
existing call site) rather than adding a new one. No compiler warnings on either edited
|
||||
file (checked with a forced recompile).
|
||||
- [ ] **0.8** — Audit that `PLOT`/`FB-WIDTH`/`FB-HEIGHT` are registered **nowhere** but the
|
||||
table Hestia will own (item 33). *Check:* read-only; a second site is a defect to report.
|
||||
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
# Capsule Block Manifest — Auto-generated
|
||||
<!-- Generated by mkcapsule --manifest 2026-09-19T17:44:11Z -->
|
||||
<!-- Generated by mkcapsule --manifest 2026-09-19T17:54:15Z -->
|
||||
<!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. -->
|
||||
<!-- Hand-written justifications and immutability notes live -->
|
||||
<!-- in MANIFEST.md alongside this auto-generated index. -->
|
||||
|
||||
@@ -368,6 +368,28 @@ int stadium_quota_slot_for_vm(VMUuid vm_id);
|
||||
*/
|
||||
uint64_t stadium_resident_sum(VMUuid vm_id);
|
||||
|
||||
/*
|
||||
* stadium_conserved - Boolean analogue of vm_physics_conserved(), for the
|
||||
* Stadium per-VM quota invariant rather than fleet-wide execution heat
|
||||
* (FABRIC-3.5.md §XXXIX.4, item 41). Checks, epsilon zero:
|
||||
*
|
||||
* stadium_resident_sum(vm_id) + stadium_reservoir_peek(vm_id) == Q48_ONE
|
||||
*
|
||||
* FABRIC-3.5.md §XL.4 rules that the full invariant also adds a `consumed`
|
||||
* term once kernel-Hermes exists and ledgers what its allocator consumes
|
||||
* (Phase 2) -- until then nothing draws on a VM's Stadium quota, so the
|
||||
* two-term form above is exact, not an approximation of the eventual one.
|
||||
* A future caller adding the `consumed` term does so here, not by working
|
||||
* around this function.
|
||||
*
|
||||
* Returns 0 (not conserved) for an unknown vm_id, same convention as
|
||||
* stadium_reservoir_peek()/stadium_resident_sum() returning 0 for one.
|
||||
*
|
||||
* @param vm_id VM to check.
|
||||
* @return Non-zero if vm_id's Stadium quota is exactly conserved, 0 otherwise.
|
||||
*/
|
||||
int stadium_conserved(VMUuid vm_id);
|
||||
|
||||
/*
|
||||
* stadium_evict - Reap the patron header at cell_index (FABRIC-0.md §17.2:
|
||||
* "reap means leaves the floor, not destroyed"). Dispatches its behaviour
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
@@ -764,6 +764,10 @@ uint64_t stadium_resident_sum(VMUuid vm_id) {
|
||||
return sum;
|
||||
}
|
||||
|
||||
int stadium_conserved(VMUuid vm_id) {
|
||||
return (stadium_resident_sum(vm_id) + stadium_reservoir_peek(vm_id)) == (uint64_t)Q48_ONE;
|
||||
}
|
||||
|
||||
/*
|
||||
* FABRIC-0.md item 3.6 / item 4.1: see stadium.h's doc. Idempotent via the
|
||||
* item-3.1 discriminator bitmap -- if cell 0 already reads as resident,
|
||||
|
||||
@@ -334,6 +334,9 @@ void stadium_words_print_boot_diagnostics(VMUuid vm_id) {
|
||||
console_puts(" (Q48_ONE=");
|
||||
console_put_u64((uint64_t)Q48_ONE);
|
||||
console_println(")");
|
||||
|
||||
console_puts("Stadium conservation: ");
|
||||
console_println(stadium_conserved(vm_id) ? "CONSERVED" : "DRIFTED");
|
||||
}
|
||||
|
||||
#endif /* __STARKERNEL__ */
|
||||
Reference in New Issue
Block a user