§H.12 step 4: Hera registers as session zero; punch list to checkboxes
Rewired stadium_birth_hera() to admit unpinned then register through session_register()/session_set_pinned() instead of setting STADIUM_FLAG_PIN directly on the candidate header. Self-referential parent (vm_uuid_hera(), vm_uuid_hera()), matching capsule_run.h's parent_vm_id == vm_id root convention. Soft-fail, non-fatal, if session_register() fails -- Hera's actual Stadium admission is what the patron-zero invariant is about. Wired session_boot_init() into kernel_main.c right after stadium_boot_init(), before stadium_birth_hera(). Also converted §H.12's punch list from bold "DONE" markers to this document's established - [ ]/- [x] checkbox convention (already used throughout §A), for consistency. Verified 3-arch boot to ok> (amd64/aarch64/riscv64), no soft-fail message on any arch, Hermes/Artemis births unaffected. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Opus 5
parent
a621131ef6
commit
67793ea4a1
+72
-62
@@ -3941,80 +3941,90 @@ identity work lands") — wiring real identities into them is part of this refac
|
|||||||
work, not new invention.
|
work, not new invention.
|
||||||
|
|
||||||
**Phase 1 — Session struct + pin-authority choke point**
|
**Phase 1 — Session struct + pin-authority choke point**
|
||||||
1. **DONE 2026-09-03.** `include/starkernel/session.h`: `Session{vm_id (VMUuid), pinned (int),
|
- [x] **1. DONE 2026-09-03.** `include/starkernel/session.h`: `Session{vm_id (VMUuid), pinned
|
||||||
parent (VMUuid), name (fixed buffer, `SESSION_NAME_BUF`=64), identity (VMIdentity,
|
(int), parent (VMUuid), name (fixed buffer, `SESSION_NAME_BUF`=64), identity (VMIdentity,
|
||||||
embedded)}`. Type only, no logic. No callers yet, so this acceptance run only confirms the
|
embedded)}`. Type only, no logic. No callers yet, so this acceptance run only confirms the
|
||||||
header itself is syntactically clean and doesn't break the build. Verified 3-arch boot to
|
header itself is syntactically clean and doesn't break the build. Verified 3-arch boot to
|
||||||
`ok>` (amd64/aarch64/riscv64).
|
`ok>` (amd64/aarch64/riscv64).
|
||||||
2. **DONE 2026-09-03, one deviation from the original wording.** `src/starkernel/vm/session.c`
|
- [x] **2. DONE 2026-09-03, one deviation from the original wording.**
|
||||||
+ `session_boot_init()`/`session_find(VMUuid)`/`session_register(...)`. Not a fixed-size
|
`src/starkernel/vm/session.c` + `session_boot_init()`/`session_find(VMUuid)`/
|
||||||
array as originally written here — found `stadium.c`'s own `StadiumVMQuota` table had
|
`session_register(...)`. Not a fixed-size array as originally written here — found
|
||||||
already been moved off a fixed array to a `kmalloc`'d-at-boot, budget-sized one (same
|
`stadium.c`'s own `StadiumVMQuota` table had already been moved off a fixed array to a
|
||||||
"population isn't knowable in advance" reasoning), so `session.c` mirrors that current
|
`kmalloc`'d-at-boot, budget-sized one (same "population isn't knowable in advance"
|
||||||
precedent instead: `session_boot_init()` sizes the slot table from `stadium_max_vm_count()`,
|
reasoning), so `session.c` mirrors that current precedent instead: `session_boot_init()`
|
||||||
must run after `stadium_boot_init()`. Added `session.c` to `Makefile.starkernel`'s explicit
|
sizes the slot table from `stadium_max_vm_count()`, must run after `stadium_boot_init()`.
|
||||||
`LOADER_EXTRA_SRCS`/`KERNEL_EXTRA_SRCS` list (not a wildcard build). No callers yet.
|
Added `session.c` to `Makefile.starkernel`'s explicit `LOADER_EXTRA_SRCS`/
|
||||||
Verified 3-arch boot to `ok>`.
|
`KERNEL_EXTRA_SRCS` list (not a wildcard build). No callers yet. Verified 3-arch boot to
|
||||||
3. **DONE 2026-09-03, one addition found necessary.** `session_set_pinned()`/
|
`ok>`.
|
||||||
`session_is_pinned()` implemented — the pin-authority choke point (H.2/H.10).
|
- [x] **3. DONE 2026-09-03, one addition found necessary.** `session_set_pinned()`/
|
||||||
`session_is_pinned()` answers from `Session.pinned` directly (the authoritative copy, no
|
`session_is_pinned()` implemented — the pin-authority choke point (H.2/H.10).
|
||||||
Stadium re-derivation); `session_set_pinned()` writes both `Session.pinned` and the
|
`session_is_pinned()` answers from `Session.pinned` directly (the authoritative copy, no
|
||||||
mirrored `STADIUM_FLAG_PIN` bit on the session's own patron header, so Stadium's own
|
Stadium re-derivation); `session_set_pinned()` writes both `Session.pinned` and the
|
||||||
internal eviction/admission logic (which must stay self-contained, no call back into
|
mirrored `STADIUM_FLAG_PIN` bit on the session's own patron header, so Stadium's own
|
||||||
session.c) keeps seeing a correct bit. **Addition**: `Session` needed a `stadium_cell`
|
internal eviction/admission logic (which must stay self-contained, no call back into
|
||||||
field (index into `stadium_cells()`) that wasn't in the original §H.2 field list — the
|
session.c) keeps seeing a correct bit. **Addition**: `Session` needed a `stadium_cell`
|
||||||
choke point can't reach the right patron header without it. Necessary plumbing, not a new
|
field (index into `stadium_cells()`) that wasn't in the original §H.2 field list — the
|
||||||
session-level concept, so not treated as reopening §H.2's design. Also moved
|
choke point can't reach the right patron header without it. Necessary plumbing, not a new
|
||||||
`STADIUM_FLAG_PIN`'s `#define` from a `stadium.c`-private constant to `stadium.h` (public)
|
session-level concept, so not treated as reopening §H.2's design. Also moved
|
||||||
so `session.c` can reference it without duplicating the definition. Verified 3-arch boot to
|
`STADIUM_FLAG_PIN`'s `#define` from a `stadium.c`-private constant to `stadium.h` (public)
|
||||||
`ok>`.
|
so `session.c` can reference it without duplicating the definition. Verified 3-arch boot to
|
||||||
4. Rewire `stadium_birth_hera()` to register through `session_register()`/
|
`ok>`.
|
||||||
`session_set_pinned()` instead of setting `STADIUM_FLAG_PIN` directly — Hera becomes
|
- [x] **4. DONE 2026-09-03.** Rewired `stadium_birth_hera()` to admit unpinned then register
|
||||||
session zero.
|
through `session_register(vm_uuid_hera(), vm_uuid_hera(), "Hera")` (self-referential
|
||||||
|
parent, matching `capsule_run.h`'s `parent_vm_id == vm_id` root convention) +
|
||||||
|
`session_set_pinned(vm_uuid_hera(), 1)` — Hera is session zero. `stadium_admit()` confirmed
|
||||||
|
to have no admission-time-special pin handling (just copies the candidate header), so
|
||||||
|
admit-unpinned-then-pin-after is safe. Soft-fail (logged, non-fatal) if `session_register()`
|
||||||
|
fails — Hera's actual Stadium admission already succeeded and is what the patron-zero
|
||||||
|
invariant is about. Wired `session_boot_init()` into `kernel_main.c` right after
|
||||||
|
`stadium_boot_init()`, before `stadium_birth_hera()`. Verified 3-arch boot to `ok>`, no
|
||||||
|
soft-fail message logged on any arch (registration succeeded), Hermes/Artemis births
|
||||||
|
unaffected.
|
||||||
|
|
||||||
**Phase 2 — Pin Hermes/Artemis (Correction 1 above)**
|
**Phase 2 — Pin Hermes/Artemis (Correction 1 above)**
|
||||||
5. In `capsule_birth.c`'s existing generic admission block, add a name check ("Hera"/
|
- [ ] **5.** In `capsule_birth.c`'s existing generic admission block, add a name check
|
||||||
"Hermes"/"Artemis" → pinned, everything else → unpinned) routed through
|
("Hera"/"Hermes"/"Artemis" → pinned, everything else → unpinned) routed through
|
||||||
`session_register()`/`session_set_pinned()`.
|
`session_register()`/`session_set_pinned()`.
|
||||||
6. Confirm (boot-log/diagnostic) Hermes and Artemis now admit pinned; ordinary births still
|
- [ ] **6.** Confirm (boot-log/diagnostic) Hermes and Artemis now admit pinned; ordinary
|
||||||
admit unpinned.
|
births still admit unpinned.
|
||||||
|
|
||||||
**Phase 3 — Session fields wired at birth**
|
**Phase 3 — Session fields wired at birth**
|
||||||
7. Populate `Session.parent` from the birthing VM's `stadium_vm_id`.
|
- [ ] **7.** Populate `Session.parent` from the birthing VM's `stadium_vm_id`.
|
||||||
8. Populate `Session.name` from the capsule's own name string (already available at this
|
- [ ] **8.** Populate `Session.name` from the capsule's own name string (already available at
|
||||||
point in `capsule_birth.c`).
|
this point in `capsule_birth.c`).
|
||||||
9. Confirm `Session.identity` defaults to `installed=0` correctly (no behavior change
|
- [ ] **9.** Confirm `Session.identity` defaults to `installed=0` correctly (no behavior
|
||||||
expected yet).
|
change expected yet).
|
||||||
|
|
||||||
**Phase 4 — Creator-ceiling enforcement (H.3, birth-time snapshot)**
|
**Phase 4 — Creator-ceiling enforcement (H.3, birth-time snapshot)**
|
||||||
10. `dictionary_snapshot_acl_from_parent(child, parent)`: for each word also present in the
|
- [ ] **10.** `dictionary_snapshot_acl_from_parent(child, parent)`: for each word also present
|
||||||
parent's dictionary, copy `acl_allow`/`acl_mode`/`acl_pinned`/`acl_ttl` into the child's
|
in the parent's dictionary, copy `acl_allow`/`acl_mode`/`acl_pinned`/`acl_ttl` into the
|
||||||
matching entry.
|
child's matching entry.
|
||||||
11. Call it once, right after a child's dictionary finishes loading in `capsule_birth.c`.
|
- [ ] **11.** Call it once, right after a child's dictionary finishes loading in
|
||||||
|
`capsule_birth.c`.
|
||||||
|
|
||||||
**Phase 5 — `BMAPFMT` (§F.4/§H.6, independent, can run any time)**
|
**Phase 5 — `BMAPFMT` (§F.4/§H.6, independent, can run any time)**
|
||||||
12. Edit `blk_meta_t` in `include/block_subsystem.h`: replace the old 4 ownership fields with
|
- [ ] **12.** Edit `blk_meta_t` in `include/block_subsystem.h`: replace the old 4 ownership
|
||||||
`owner_fp[8]`/`acl_allow`/`acl_ttl` (u32)/`acl_reserved[3]`/`reserved_future`. Verify
|
fields with `owner_fp[8]`/`acl_allow`/`acl_ttl` (u32)/`acl_reserved[3]`/`reserved_future`.
|
||||||
size/offsets with `offsetof`/`sizeof`, not by hand (see the `blk_volume_meta_t` padding-bug
|
Verify size/offsets with `offsetof`/`sizeof`, not by hand (see the `blk_volume_meta_t`
|
||||||
lesson, [[project_phase8_milestone6_complete]]).
|
padding-bug lesson, [[project_phase8_milestone6_complete]]).
|
||||||
13. Define the three `flags` bit constants (`CLAIMED`=0/`MIGRATING`=1/`STALE`=2).
|
- [ ] **13.** Define the three `flags` bit constants (`CLAIMED`=0/`MIGRATING`=1/`STALE`=2).
|
||||||
14. Add C get/set accessors for the new fields in `block_subsystem.c`.
|
- [ ] **14.** Add C get/set accessors for the new fields in `block_subsystem.c`.
|
||||||
15. Add FORTH wrappers (`BLK-ACL-ALLOW@`/`!`, `BLK-ACL-TTL@`/`!`, `BLK-OWNER@`).
|
- [ ] **15.** Add FORTH wrappers (`BLK-ACL-ALLOW@`/`!`, `BLK-ACL-TTL@`/`!`, `BLK-OWNER@`).
|
||||||
16. Add a new policy capsule (mirroring `ACL.4th`) with a real fast-deny check on top — no
|
- [ ] **16.** Add a new policy capsule (mirroring `ACL.4th`) with a real fast-deny check on
|
||||||
stub, per this project's standing "no stubs or TODOs, ever" rule (§C).
|
top — no stub, per this project's standing "no stubs or TODOs, ever" rule (§C).
|
||||||
|
|
||||||
**Phase 6 — Zuse eligibility list (H.5)**
|
**Phase 6 — Zuse eligibility list (H.5)**
|
||||||
17. Extend the metadata-fence record format with a new growable `owner_pubkey[32]`-list
|
- [ ] **17.** Extend the metadata-fence record format with a new growable
|
||||||
record type.
|
`owner_pubkey[32]`-list record type.
|
||||||
18. Implement read/add/membership-check functions in C.
|
- [ ] **18.** Implement read/add/membership-check functions in C.
|
||||||
19. Add a Zuse-only FORTH word to add an entry, gated by `zuse_session`.
|
- [ ] **19.** Add a Zuse-only FORTH word to add an entry, gated by `zuse_session`.
|
||||||
|
|
||||||
**Phase 7 — Message card gate + `ELEVATE-REQUEST` (H.8)**
|
**Phase 7 — Message card gate + `ELEVATE-REQUEST` (H.8)**
|
||||||
20. Add the initiator-only ACL gate at `CH-REQUEST`'s entry point (default-permissive
|
- [ ] **20.** Add the initiator-only ACL gate at `CH-REQUEST`'s entry point
|
||||||
baseline, real hook point established).
|
(default-permissive baseline, real hook point established).
|
||||||
21. Define `ELEVATE-REQUEST` and a minimal real handler checking the eligibility list,
|
- [ ] **21.** Define `ELEVATE-REQUEST` and a minimal real handler checking the eligibility
|
||||||
granting via `ACL-ALLOW!`/`ACL-TTL!` on match.
|
list, granting via `ACL-ALLOW!`/`ACL-TTL!` on match.
|
||||||
22. Add the FORTH entrypoint a session actually calls to send one.
|
- [ ] **22.** Add the FORTH entrypoint a session actually calls to send one.
|
||||||
|
|
||||||
**Excluded, per H.11's deferred items 10–11**: VM card multi-owner support, live-console
|
**Excluded, per H.11's deferred items 10–11**: VM card multi-owner support, live-console
|
||||||
`sudo`-style elevation, pre-signed capability tickets.
|
`sudo`-style elevation, pre-signed capability tickets.
|
||||||
|
|||||||
@@ -1,5 +1,5 @@
|
|||||||
# Capsule Block Manifest — Auto-generated
|
# Capsule Block Manifest — Auto-generated
|
||||||
<!-- Generated by mkcapsule --manifest 2026-09-03T10:08:29Z -->
|
<!-- Generated by mkcapsule --manifest 2026-09-03T10:14:23Z -->
|
||||||
<!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. -->
|
<!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. -->
|
||||||
<!-- Hand-written justifications and immutability notes live -->
|
<!-- Hand-written justifications and immutability notes live -->
|
||||||
<!-- in MANIFEST.md alongside this auto-generated index. -->
|
<!-- in MANIFEST.md alongside this auto-generated index. -->
|
||||||
|
|||||||
Binary file not shown.
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
@@ -58,6 +58,7 @@ EFI_RUNTIME_SERVICES *g_sk_runtime_services = NULL;
|
|||||||
#include "starkernel/vm/stadium.h"
|
#include "starkernel/vm/stadium.h"
|
||||||
#include "starkernel/vm/stadium_words.h"
|
#include "starkernel/vm/stadium_words.h"
|
||||||
#include "starkernel/vm/stadium_blocks.h"
|
#include "starkernel/vm/stadium_blocks.h"
|
||||||
|
#include "starkernel/session.h"
|
||||||
#include "starkernel/capsule_generated.h"
|
#include "starkernel/capsule_generated.h"
|
||||||
#include "starkernel/capsule_loader.h"
|
#include "starkernel/capsule_loader.h"
|
||||||
#include "starkernel/capsule_birth.h" /* capsule_birth_mama, capsule_find_mama_init */
|
#include "starkernel/capsule_birth.h" /* capsule_birth_mama, capsule_find_mama_init */
|
||||||
@@ -512,6 +513,14 @@ static void kernel_main_deep(BootInfo *boot_info) {
|
|||||||
* yet, so a failed allocation logs and boot continues. */
|
* yet, so a failed allocation logs and boot continues. */
|
||||||
(void)stadium_boot_init();
|
(void)stadium_boot_init();
|
||||||
|
|
||||||
|
/* Session: boot-time allocation (FABRIC-3.md §H.12 step 4), sized from
|
||||||
|
* stadium_max_vm_count() so it must run after stadium_boot_init() above
|
||||||
|
* and before the first session is registered (stadium_birth_hera()
|
||||||
|
* below registers Hera as session zero). Soft failure, same reasoning
|
||||||
|
* as stadium_boot_init() -- stadium_birth_hera() itself soft-fails a
|
||||||
|
* failed session_register() rather than treating it as fatal. */
|
||||||
|
(void)session_boot_init();
|
||||||
|
|
||||||
/* item 4.1, FABRIC.md item 3.6/§17.7: actually enforce "Hera is patron
|
/* item 4.1, FABRIC.md item 3.6/§17.7: actually enforce "Hera is patron
|
||||||
* zero" before anything else can land on cell 0 via the free list, then
|
* zero" before anything else can land on cell 0 via the free list, then
|
||||||
* bring up the word layer's map. Both must happen before the first word
|
* bring up the word layer's map. Both must happen before the first word
|
||||||
|
|||||||
@@ -41,6 +41,7 @@
|
|||||||
#include "starkernel/q48_16.h" /* Q48_ONE -- item 4.1's reservoir starts each VM's quota at 1.0 */
|
#include "starkernel/q48_16.h" /* Q48_ONE -- item 4.1's reservoir starts each VM's quota at 1.0 */
|
||||||
#include "vm.h" /* VM_MEMORY_SIZE -- the per-VM footprint stadium_max_vm_count() budgets against */
|
#include "vm.h" /* VM_MEMORY_SIZE -- the per-VM footprint stadium_max_vm_count() budgets against */
|
||||||
#include "block_subsystem.h" /* blk_flush() -- STADIUM_BEHAVIOUR_MIGRATE's real write-back action */
|
#include "block_subsystem.h" /* blk_flush() -- STADIUM_BEHAVIOUR_MIGRATE's real write-back action */
|
||||||
|
#include "starkernel/session.h" /* session_register()/session_set_pinned() -- FABRIC-3.md §H.12 step 4 */
|
||||||
|
|
||||||
static StadiumCell *stadium_cell_array = (StadiumCell *)0;
|
static StadiumCell *stadium_cell_array = (StadiumCell *)0;
|
||||||
static uint8_t *stadium_bitmap = (uint8_t *)0;
|
static uint8_t *stadium_bitmap = (uint8_t *)0;
|
||||||
@@ -637,6 +638,17 @@ uint64_t stadium_resident_sum(VMUuid vm_id) {
|
|||||||
* item-3.1 discriminator bitmap -- if cell 0 already reads as resident,
|
* item-3.1 discriminator bitmap -- if cell 0 already reads as resident,
|
||||||
* something already birthed her (or, if it isn't actually Hera, something
|
* something already birthed her (or, if it isn't actually Hera, something
|
||||||
* else already claimed cell 0 -- either way this must not clobber it).
|
* else already claimed cell 0 -- either way this must not clobber it).
|
||||||
|
*
|
||||||
|
* FABRIC-3.md §H.12 step 4: pinning no longer happens by setting
|
||||||
|
* STADIUM_FLAG_PIN on the candidate before admission -- session.c's
|
||||||
|
* session_set_pinned() is now the sole choke point for that bit (§H.10).
|
||||||
|
* Hera is admitted unpinned, then registered as session zero
|
||||||
|
* (self-referential parent, matching capsule_run.h's parent_vm_id ==
|
||||||
|
* vm_id convention for the root) and pinned through the session layer.
|
||||||
|
* Session registration/pinning is soft-fail (logged, not fatal) -- Hera's
|
||||||
|
* actual Stadium admission above already succeeded and is what the
|
||||||
|
* patron-zero invariant is about; session.c not yet being initialized
|
||||||
|
* must not break that.
|
||||||
*/
|
*/
|
||||||
int stadium_birth_hera(void) {
|
int stadium_birth_hera(void) {
|
||||||
StadiumPatronHeader candidate;
|
StadiumPatronHeader candidate;
|
||||||
@@ -656,7 +668,7 @@ int stadium_birth_hera(void) {
|
|||||||
candidate.link = STADIUM_LINK_NONE;
|
candidate.link = STADIUM_LINK_NONE;
|
||||||
candidate.contains = STADIUM_CONTAINS_NONE;
|
candidate.contains = STADIUM_CONTAINS_NONE;
|
||||||
candidate.mass = 1;
|
candidate.mass = 1;
|
||||||
candidate.flags = STADIUM_FLAG_PIN;
|
candidate.flags = 0;
|
||||||
candidate.behaviour = (uint8_t)STADIUM_BEHAVIOUR_COOL;
|
candidate.behaviour = (uint8_t)STADIUM_BEHAVIOUR_COOL;
|
||||||
|
|
||||||
idx = stadium_admit(vm_uuid_hera(), &candidate);
|
idx = stadium_admit(vm_uuid_hera(), &candidate);
|
||||||
@@ -664,6 +676,17 @@ int stadium_birth_hera(void) {
|
|||||||
if (idx != STADIUM_HERA_CELL_INDEX) {
|
if (idx != STADIUM_HERA_CELL_INDEX) {
|
||||||
sk_hal_panic("Stadium: birth_hera did not land on cell 0 -- patron-zero invariant broken");
|
sk_hal_panic("Stadium: birth_hera did not land on cell 0 -- patron-zero invariant broken");
|
||||||
}
|
}
|
||||||
|
|
||||||
|
{
|
||||||
|
Session *s = session_register(vm_uuid_hera(), vm_uuid_hera(), "Hera");
|
||||||
|
if (s) {
|
||||||
|
s->stadium_cell = idx;
|
||||||
|
session_set_pinned(vm_uuid_hera(), 1);
|
||||||
|
} else {
|
||||||
|
console_println("Stadium: session_register failed for Hera (session.c not yet initialized?)");
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user