Documentation debt sweep: 5 of 6 items resolved, 1 confirmed accurate
- docs/lithosananke/ROADMAP.md + M7.1.md: fixed stale "Branch: lithosananke" (no such branch post-split), M7.1's "Design Complete" status (shipped and live, redirected to FABRIC*.md), the M8/success-criteria self-contradiction (OBSOLETE marking vs. unqualified live criterion), and the stale AHCI/SATA claim for M9 (real implementation is virtio_blk.c) -- also corrected BLOCK/BUFFER/UPDATE/FLUSH and block device abstraction to [x] since both are confirmed live in src/word_source/block_words.c and block_subsystem.c. - Top-level ROADMAP.md: marked OBSOLETE (Captain Bob's call -- more than "stale," the architecture/branch topology/terminology it describes no longer exist), pointing to docs/lithosananke/ROADMAP.md and FABRIC*.md for current status. - docs/03-architecture/word-acl/DESIGN.md: fixed the ACL Phase 7 contradiction -- Phase 7 (LithosAnanke kernel parity) is independently verified complete per .claude/CLAUDE.md, not "remaining"; removed the stale lithosananke-branch-parity framing. - VM-FLEET-ATTRACTOR-DESIGN-20260705.md's doe-campaign.4th "broken" claim: investigated, ran SMOKE-CAMPAIGN live (completes clean, fleet heat conserved) -- initially read as contradicting the claim, corrected directly by Captain Bob: a clean execution trace doesn't disprove the doc's actual argument (no real controlled-experimental-factor mechanism). Confirmed accurate, left untouched. - Isabelle/HOL pipeline-metrics model/C-struct mismatch: confirmed a real proof-modeling gap (pm_last_accuracy_num/den has no analogue in the real PipelineGlobalMetrics struct), not stale prose -- tracked here rather than fixed, matching the .thy file's own scope boundary and this project's standing caution that each Isabelle gap needs its own subsystem model. ACL-RWT DoE overhead re-measurement (the 6th item) intentionally not started -- a full multi-architecture DoE campaign, not a doc-text fix, holding for explicit confirmation given the scale. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CXjAPTEKrgY2Mrk25KoLDn
This commit is contained in:
co-authored by
Claude Sonnet 5
parent
6341b3b3dd
commit
cbe7b49a59
+20
-5
@@ -78,12 +78,27 @@ decisions get added here, not to `FABRIC-2.md`. Follow the same discipline `FABR
|
|||||||
is still "remaining" — direct contradiction with `.claude/CLAUDE.md`, which states Phase 7
|
is still "remaining" — direct contradiction with `.claude/CLAUDE.md`, which states Phase 7
|
||||||
is independently verified complete. Not fixed.
|
is independently verified complete. Not fixed.
|
||||||
|
|
||||||
- [ ] `VM-FLEET-ATTRACTOR-DESIGN-20260705.md` claims `doe-campaign.4th` is "broken and being
|
- [x] Confirmed accurate, not stale (2026-08-26): `VM-FLEET-ATTRACTOR-DESIGN-20260705.md`'s
|
||||||
superseded" — unverified against repeated successful `L8-DOE` runs (a different FORTH entry
|
claim that `doe-campaign.4th` is "broken and being superseded." Live-ran `SMOKE-CAMPAIGN`
|
||||||
point; not confirmed either way).
|
from the current capsule (amd64) — it completes without error and correctly conserves fleet
|
||||||
|
heat (`VM-PHYSICS: conserved=CONSERVED`, `fleet_heat_sum=65536`). Initially read that as
|
||||||
|
contradicting the doc's claim; **Captain Bob corrected this directly — it's broken.**
|
||||||
|
"Doesn't crash" and "runs" are not the same claim: the doc's actual argument is that the
|
||||||
|
capsule has no real controlled-experimental-factor mechanism (no manual heat-injection
|
||||||
|
point under the current design, so it cannot drive the fleet through controlled scenarios
|
||||||
|
the way a DoE campaign needs to), a methodological gap a clean execution trace doesn't
|
||||||
|
surface or disprove. Doc's claim stands; not touched.
|
||||||
|
|
||||||
- [ ] Isabelle/HOL: the pipeline-metrics model/C-struct mismatch this sweep surfaced —
|
- [x] Tracked (2026-08-26) — real proof-modeling gap, not just stale prose, so not fixed
|
||||||
flagged in the `.thy` file itself, not independently tracked elsewhere, not fixed.
|
here. Confirmed by reading `StarForth_Loop4_Pipeline.thy`'s own comment (lines 127–137):
|
||||||
|
`pipeline_metrics_state`'s `pm_last_accuracy_num`/`pm_last_accuracy_den` fraction pair
|
||||||
|
doesn't correspond to anything in the real C struct — `include/vm.h`'s
|
||||||
|
`PipelineGlobalMetrics` has a single `double last_checked_accuracy` field, no num/den pair
|
||||||
|
anywhere. The `.thy` file's own comment already scopes the real fix correctly: "a full
|
||||||
|
field-level pass over `pipeline_metrics_state` is its own separate task" — matches this
|
||||||
|
project's standing caution that each remaining Isabelle gap needs its own subsystem model,
|
||||||
|
not a documentation-sprint patch. The punch-list ask was tracking this outside the buried
|
||||||
|
`.thy` comment, which it now has here — the actual re-model stays unattempted, on purpose.
|
||||||
|
|
||||||
### From FABRIC-2.md §X, Milestone 2 — USB hardware stack
|
### From FABRIC-2.md §X, Milestone 2 — USB hardware stack
|
||||||
|
|
||||||
|
|||||||
@@ -1,5 +1,14 @@
|
|||||||
# StarForth Roadmap: VM → Kernel → OS → FPGA
|
# StarForth Roadmap: VM → Kernel → OS → FPGA
|
||||||
|
|
||||||
|
> **OBSOLETE (flagged 2026-08-26, Captain Bob's call — this is more than "stale," the
|
||||||
|
> architecture, branch topology, and terminology it describes no longer exist).** This is a
|
||||||
|
> StarForth-era plan dated 2025-12-14, written before the repo split, before
|
||||||
|
> Tripod/Stadium/word-level ACL existed, and before "Phase 1 Starting (HAL)" had any of the
|
||||||
|
> meaning it has now. Kept for historical record only. For current status, see
|
||||||
|
> `docs/lithosananke/ROADMAP.md` (repo-specific, LithosAnanke roadmap) and
|
||||||
|
> `FABRIC.md`/`FABRIC-2.md`/`FABRIC-3.md` (design history and current work) — not this
|
||||||
|
> document.
|
||||||
|
|
||||||
**Version**: 1.0
|
**Version**: 1.0
|
||||||
**Date**: 2025-12-14
|
**Date**: 2025-12-14
|
||||||
**Timeline**: 2025-2028 (3.5 years)
|
**Timeline**: 2025-2028 (3.5 years)
|
||||||
|
|||||||
@@ -1,7 +1,11 @@
|
|||||||
# Word-Level ACL System
|
# Word-Level ACL System
|
||||||
|
|
||||||
**Status:** Implemented through Phase 6 — Phase 7 (LithosAnanke parity) remaining
|
**Status:** Implemented through Phase 7 (LithosAnanke kernel parity) — independently verified
|
||||||
**Target branch:** `master` complete; `lithosananke` parity next
|
present in current `master` (`.claude/CLAUDE.md`'s Word-Level ACL System section). Phase 8
|
||||||
|
(PKI/thumbdrive minting) is the current open item.
|
||||||
|
**Target branch:** `master` — post-split, this repo's sole production line; there is no
|
||||||
|
separate `lithosananke` branch to reach parity with (see `.claude/CLAUDE.md`'s "On the branch
|
||||||
|
topology" note)
|
||||||
**Implementation files:** `capsules/ACL.4th`, `capsules/zuse.4th`, `src/word_source/acl_words.c`, `src/test_runner/modules/acl_words_test.c`
|
**Implementation files:** `capsules/ACL.4th`, `capsules/zuse.4th`, `src/word_source/acl_words.c`, `src/test_runner/modules/acl_words_test.c`
|
||||||
|
|
||||||
---
|
---
|
||||||
@@ -368,16 +372,24 @@ Five `.thy` files in `proof/` alongside existing VM proofs:
|
|||||||
- [x] `ACL_No_Escalation.thy` — a child VM cannot produce a pinned entry
|
- [x] `ACL_No_Escalation.thy` — a child VM cannot produce a pinned entry
|
||||||
with higher privilege than its inherited mode
|
with higher privilege than its inherited mode
|
||||||
|
|
||||||
### Phase 7 — LithosAnanke Parity (REMAINING)
|
### Phase 7 — LithosAnanke Parity (COMPLETE — independently verified)
|
||||||
|
|
||||||
- [ ] Merge / port ACL subsystem to `lithosananke` branch
|
There is no separate `lithosananke` branch to merge/port to (post-split, this repo's `master`
|
||||||
- [ ] Verify `ACL.4th` loads cleanly in kernel context (freestanding)
|
is the sole production line) — that framing is stale. Verified present directly in current
|
||||||
- [ ] `ACL-BOOT` runs at kernel boot before first `BIRTH`
|
`master`: `acl_recheck()`/`zuse_session`/`emergency_console` wiring confirmed in
|
||||||
- [ ] `vm->emergency_console` wired to kernel REPL active flag
|
`src/starkernel/vm/vm_core.c`; the per-iteration `emergency_console = zuse_session ? 0 : 1`
|
||||||
- [ ] `vm->zuse_session` wired to kernel Zuse console authentication path
|
assignment confirmed in `src/starkernel/repl.c`; the old `!vm->zuse_session` ACL-check bypass
|
||||||
- [ ] Three-arch acceptance: amd64, aarch64, riscv64 boot to `ok>` with ACL
|
confirmed absent from `src/vm.c`. See `.claude/CLAUDE.md`'s Word-Level ACL System section for
|
||||||
|
the full verification writeup.
|
||||||
|
|
||||||
|
- [x] Verify `ACL.4th` loads cleanly in kernel context (freestanding)
|
||||||
|
- [x] `ACL-BOOT` runs at kernel boot before first `BIRTH`
|
||||||
|
- [x] `vm->emergency_console` wired to kernel REPL active flag
|
||||||
|
- [x] `vm->zuse_session` wired to kernel Zuse console authentication path
|
||||||
|
- [x] Three-arch acceptance: amd64, aarch64, riscv64 boot to `ok>` with ACL
|
||||||
active and no regressions
|
active and no regressions
|
||||||
- [ ] Commit acceptance logs
|
- [x] Acceptance logs — this repo's standing convention commits every acceptance boot's serial
|
||||||
|
log under `logs/`, not a one-time Phase 7 action
|
||||||
|
|
||||||
### Phase 8 — PKI / Thumbdrive Authentication (FUTURE)
|
### Phase 8 — PKI / Thumbdrive Authentication (FUTURE)
|
||||||
|
|
||||||
|
|||||||
@@ -1,7 +1,9 @@
|
|||||||
# M7.1: Init Capsule Architecture
|
# M7.1: Init Capsule Architecture
|
||||||
|
|
||||||
**Status:** Design Complete
|
**Status:** Shipped and live, not just designed — this document predates the actual
|
||||||
**Branch:** lithosananke
|
capsule/Tripod/Stadium work; see `FABRIC.md`/`FABRIC-2.md`/`FABRIC-3.md` for real status
|
||||||
|
(per `.claude/CLAUDE.md`'s standing redirect)
|
||||||
|
**Branch:** `master` (post-split; the old `lithosananke` branch no longer exists in this repo)
|
||||||
**Prerequisite:** M7 (VM Parity Validation)
|
**Prerequisite:** M7 (VM Parity Validation)
|
||||||
|
|
||||||
## The Immutable Law
|
## The Immutable Law
|
||||||
|
|||||||
@@ -1,7 +1,9 @@
|
|||||||
# LithosAnanke Roadmap
|
# LithosAnanke Roadmap
|
||||||
|
|
||||||
**Branch:** `lithosananke`
|
**Branch:** `master` (post-split: this repo's `master` is the sole LithosAnanke production
|
||||||
**Current:** M7 Complete
|
line; the old `lithosananke` branch belonged to the pre-split combined monorepo and no
|
||||||
|
longer exists here — see `.claude/CLAUDE.md`'s "On the branch topology" note)
|
||||||
|
**Current:** M7.1 in progress — see `FABRIC.md`/`FABRIC-2.md`/`FABRIC-3.md` for real status
|
||||||
|
|
||||||
---
|
---
|
||||||
|
|
||||||
@@ -16,7 +18,7 @@ M4 APIC ██████████████████
|
|||||||
M5 Timer ████████████████████ COMPLETE
|
M5 Timer ████████████████████ COMPLETE
|
||||||
M6 Heap ████████████████████ COMPLETE
|
M6 Heap ████████████████████ COMPLETE
|
||||||
M7 VM Parity ████████████████████ COMPLETE
|
M7 VM Parity ████████████████████ COMPLETE
|
||||||
M7.1 Capsules ████████████░░░░░░░░ DESIGN COMPLETE
|
M7.1 Capsules ████████████████░░░░ LIVE — see FABRIC.md/FABRIC-2.md/FABRIC-3.md
|
||||||
M8 REPL ░░░░░░░░░░░░░░░░░░░░ OBSOLETE — see FABRIC.md §25.5 item 4.4
|
M8 REPL ░░░░░░░░░░░░░░░░░░░░ OBSOLETE — see FABRIC.md §25.5 item 4.4
|
||||||
M9 Block I/O ░░░░░░░░░░░░░░░░░░░░ PLANNED
|
M9 Block I/O ░░░░░░░░░░░░░░░░░░░░ PLANNED
|
||||||
M10 Networking ░░░░░░░░░░░░░░░░░░░░ FUTURE
|
M10 Networking ░░░░░░░░░░░░░░░░░░░░ FUTURE
|
||||||
@@ -346,10 +348,14 @@ identically afterward.)
|
|||||||
**Goal:** Read/write blocks to disk
|
**Goal:** Read/write blocks to disk
|
||||||
|
|
||||||
**Deliverables:**
|
**Deliverables:**
|
||||||
- [ ] AHCI driver (SATA)
|
- [x] Block device driver — implemented via `virtio_blk.c` (virtio block device), not the
|
||||||
- [ ] Block device abstraction
|
AHCI/SATA driver originally scoped here; see `.claude/CLAUDE.md`'s M9 note.
|
||||||
- [ ] `BLOCK` / `BUFFER` / `UPDATE` / `FLUSH` words
|
- [x] Block device abstraction — `block_subsystem.c`'s unified LBN address space, backend-agnostic
|
||||||
- [ ] Persistent dictionary
|
across RAM/RAMDRIVE/DISK/USB via the `blkio_dev` vtable.
|
||||||
|
- [x] `BLOCK` / `BUFFER` / `UPDATE` / `FLUSH` words — live, `src/word_source/block_words.c`.
|
||||||
|
- [ ] Persistent dictionary — no evidence found of word definitions surviving reboot; not
|
||||||
|
independently verified as done, left unchecked rather than assumed from the rest of this
|
||||||
|
list being live.
|
||||||
|
|
||||||
---
|
---
|
||||||
|
|
||||||
@@ -406,7 +412,9 @@ LithosAnanke is successful when:
|
|||||||
|
|
||||||
1. **M7 Parity** — VM dictionary hash reproducible across boots
|
1. **M7 Parity** — VM dictionary hash reproducible across boots
|
||||||
2. **M7.1 Capsules** — Birth protocol enforced, provenance logged
|
2. **M7.1 Capsules** — Birth protocol enforced, provenance logged
|
||||||
3. **M8 REPL** — Interactive Forth at bare metal
|
3. ~~**M8 REPL** — Interactive Forth at bare metal~~ — superseded, this criterion is now met
|
||||||
|
via Stadium's Console fabric work (`FABRIC.md` §25.5 item 4.4), not a standalone M8; see
|
||||||
|
the OBSOLETE banner above Phase 4
|
||||||
4. **M9 Persistence** — State survives reboot
|
4. **M9 Persistence** — State survives reboot
|
||||||
|
|
||||||
---
|
---
|
||||||
|
|||||||
Reference in New Issue
Block a user