From 89d886b7f711036612dd6f05836ce2c4ab0ba7d6 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 19 Sep 2026 14:47:35 +0000 Subject: [PATCH] =?UTF-8?q?CLAUDE.md:=20correct=20four=20stale=20claims,?= =?UTF-8?q?=20add=20reshuffle=20pointer;=20record=20as=20FABRIC-3.5=20?= =?UTF-8?q?=C2=A7XLIV?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Authorized by Captain Bob. Each claim re-verified against source immediately before editing rather than from this session's notes. Theory files: 23 becomes 52, all listed in proof/ROOT, with a pointer to COVERAGE.md's own statement that the deliverable is the verified boundary rather than a green build. LITHOS_VERSION: 2.0.1 becomes 2.0.0, noting §I.2 rolled it back because 2.0.1 names the SER5 hardware-track line and claims progress not yet verified, and that the policy is semantic rather than sequential. ACL pinning carried two mutually inconsistent rules, neither matching the code: policy never in C with no vm_find_word plus field assignment, and separately that kernel-only words should be pinned in a kernel-specific capsule. kernel_main.c:771-782 pins BIRTH and CAPSULE-BIRTH exactly the forbidden way, deliberately, and ACL.4th's block-4005 comment explains why -- so ACL.4th stays host-portable. Now stated as the rule plus its one sanctioned exception. The mkcapsule block rule was described as a 1024-byte budget verified with wc -c. Reading tools/mkcapsule.c shows validate_forth_blocks enforces 64 chars by 16 lines and a block number in [2048,5120). 64 times 16 is 1024, which is where the figure came from, but the enforcement is per-line: eight lines of 128 chars is 1024 bytes and still fails. Note that FABRIC-3 §XXXII.2's own correction of this claim was itself incomplete, fixing the number while missing the line-length rule. Adds a WORK IN PROGRESS pointer directing a fresh session to FABRIC-3.6.md's START HERE, since CLAUDE.md is what auto-loads. It states no reshuffle code exists and that the file's current Tripod descriptions stay correct until the reshuffle lands, deliberately not pre-writing the post-reshuffle state. FABRIC-3.6.md: trap 5 rewritten, since it told a fresh session to distrust four claims that are now fixed; it now names MANIFEST.md and FABRIC-0 §25.7 as the documents that still drift. Also removes a quoted commit id from the handoff that will always be stale. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VkM1zHGvBerLF6aqkHPweP --- .claude/CLAUDE.md | 35 ++++++++++++++++++++++++++++------- FABRIC-3.5.md | 45 +++++++++++++++++++++++++++++++++++++++++++++ FABRIC-3.6.md | 23 +++++++++++++---------- 3 files changed, 86 insertions(+), 17 deletions(-) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 106ee82e..6717c234 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -18,6 +18,14 @@ This file provides guidance to Claude Code (claude.ai/code) when working with co > authority, and do not cite them in place of `FABRIC-0.md`/`FABRIC-1.md`/`FABRIC-2.md`/ > `FABRIC-3.md`. +> **WORK IN PROGRESS — Tripod/kernel reshuffle (2026-09-19).** Hermes moves into the kernel; +> the Tripod becomes **Hera / Artemis / Hestia**. Design is complete and ruled in +> **`FABRIC-3.5.md`** (authoritative); execution is tracked in **`FABRIC-3.6.md`** — **start +> there, at its `START HERE` section.** `FABRIC-3.md` remains open and authoritative for its +> own topic (bare metal boot); nothing in the reshuffle supersedes it. **No reshuffle code has +> been written yet.** The descriptions of the Tripod elsewhere in this file describe the +> *current* fleet (Hera/Hermes/Artemis) and stay correct until the reshuffle lands. + > **Scope:** This repo is LithosAnanke — the bare-metal UEFI kernel that boots StarForth > directly on hardware. StarForth (the hosted FORTH-79 VM) has its own separate repository > now. This repo vendors a full copy of the shared VM source (`src/vm.c`, `src/word_source/`, @@ -57,8 +65,9 @@ about "which line am I on." - **BIRTH, RUN, USE are primitives** — registered in C exactly like DUP, BYE, EXEC. Use `' BIRTH` directly. Never reach for FIND, never add conditionals, never rename them to `CAPSULE-BIRTH` or anything else. - **FIND is a proven, tested, registered word. Never modify it.** The implementation is intentionally non-standard (parses from input stream). It is tested. Leave it alone. - **Never modify a registered, tested word to "fix" it.** If something seems wrong with a word, the problem is almost certainly in the caller, not the word. -- **ACL policy belongs in `ACL.4th`, never in C.** No policy logic in `kernel_main.c`, no `vm_find_word` + field assignment for pinning. Use `' WORD ACL-PIN` in FORTH exactly as IMMEDIATE works. -- **`' BIRTH` in shared capsules breaks the hosted build** — BIRTH is kernel-only. Pin it in a kernel-specific capsule, not in `ACL.4th` which is shared. `capsules/ACL.4th` itself documents this exclusion in a comment (line ~64) — it deliberately omits `BIRTH`/`CAPSULE-BIRTH` even though this IS the kernel repo, because `ACL.4th` is meant to stay portable/shared. +- **ACL policy belongs in `ACL.4th`, never in C — with one sanctioned exception, below.** Use `' WORD ACL-PIN` in FORTH exactly as IMMEDIATE works. +- **The exception: kernel-only words are pinned in C, in `kernel_main.c`, after capsule load.** Corrected 2026-09-19 — this file previously forbade `vm_find_word` + field assignment outright and separately advised pinning such words "in a kernel-specific capsule." Neither matched the code. `kernel_main.c:771-782` pins `BIRTH` and `CAPSULE-BIRTH` exactly that way, deliberately, and `capsules/ACL.4th`'s own block-4005 comment explains why: they are "kernel-only, not in hosted VM. Pinned in C (`kernel_main.c`) after capsule load instead, **so this file stays host-portable**." Follow the code. Do not add C-side pinning for any word that *could* live in `ACL.4th`. +- **`' BIRTH` in shared capsules breaks the hosted build** — BIRTH is kernel-only. `capsules/ACL.4th` itself documents this exclusion in a comment (line ~64) — it deliberately omits `BIRTH`/`CAPSULE-BIRTH` even though this IS the kernel repo, because `ACL.4th` is meant to stay portable/shared. ### On the Embedded VM vs. the Kernel - **`src/vm.c`, `include/vm.h`, `capsules/`, `src/word_source/` are the shared/vendored VM @@ -152,8 +161,13 @@ capsule files — accurate): - `2100–2199` — `doe.4th` only - `3000–3999` — workload capsules - `4000+` — user-defined capsules (`ACL.4th` uses 4000–4015, `zuse.4th` uses 4016–4018) -Each block header line counts against the 1024-byte limit. Any block exceeding 1024 bytes -is truncated silently at load time — verify with `wc -c` before committing. +**Block format, corrected 2026-09-19 against `tools/mkcapsule.c` itself** (this file +previously described a 1024-byte-per-block budget — right by arithmetic, wrong as a rule): +`validate_forth_blocks` enforces a **64-char × 16-line** format — +**line length ≤ 64 chars, ≤ 16 content lines per block** (`mkcapsule.c:344-345`, `:430`) — and +a block number in **`[2048, 5120)`** (`:408-409`). 64 × 16 = 1024, which is where the old +figure came from, but the enforcement is per-line and per-line-count: **8 lines of 128 chars +is 1024 bytes and still fails.** Verify with `mkcapsule --lint capsules/`, not `wc -c`. --- @@ -212,7 +226,11 @@ Output: `build//kernel/starkernel_loader.efi` + `build//kernel/stark Two independently tracked version strings flow into the generated `include/version.h`: `VERSION` (`Makefile.starkernel` — the embedded StarForth engine version, currently `3.1.0`; note this does **not** auto-sync with the standalone StarForth repo's own version) and -`LITHOS_VERSION` (`Makefile.starkernel` — the kernel version, currently `2.0.1`). +`LITHOS_VERSION` (`Makefile.starkernel` — the kernel version, currently **`2.0.0`**; +corrected 2026-09-19 — this file said `2.0.1`, but `FABRIC-3.md` §I.2 rolled it back to +`2.0.0` on 2026-09-04 because `2.0.1` names the SER5 hardware-track line and claims hardware +progress not yet verified. The versioning policy is **semantic, not sequential** — see the +roadmap table in `Makefile.starkernel` before choosing any version). ### Build configuration (Kconfig — real, wired, not vestigial) @@ -436,8 +454,11 @@ replacing hardcoded compudynamics constants with a dynamically-inferred rate. ## Formal Verification -`proof/` contains 23 Isabelle/HOL theory files (same composition as the standalone StarForth -repo — 18 core VM/word-category theories + 5 ACL theories). Run `isabelle build -D proof/` +`proof/` contains **52** Isabelle/HOL theory files — 47 `StarForth_*` + 5 `ACL_*`, all of them +listed in `proof/ROOT` (corrected 2026-09-19; this file said 23, and `proof/COVERAGE.md` has +said 52 all along). **Read `proof/COVERAGE.md` first**: its stated goal is not a green build but +"identify precisely what cannot be proven and why — the boundary between 'formally verified' +and 'not, for this specific reason'." Run `isabelle build -D proof/` directly; neither `Makefile` nor `Makefile.starkernel` in this repo defines an `isabelle-build`/`isabelle-check` target (unlike the standalone StarForth repo, which has a broken one — this repo simply doesn't have the target at all, so there's nothing to diff --git a/FABRIC-3.5.md b/FABRIC-3.5.md index 389e448b..0ff51bac 100644 --- a/FABRIC-3.5.md +++ b/FABRIC-3.5.md @@ -4620,3 +4620,48 @@ lock and no new state. **Phase 3's design blocker is cleared. What remains before it is buildable are two decisions, neither of which requires further investigation:** channels (one membership or negotiation), and the switch-slot ceiling. **The reshuffle has no undesigned mechanism left.** + +--- + +## XLIV. `.claude/CLAUDE.md` corrected (authorized 2026-09-19) + +Item 20's four known-stale claims, plus a discoverability pointer, applied to `.claude/CLAUDE.md` +under explicit authorization. **Each was verified against source immediately before editing, not +from this document's own notes.** + +| Claim | Was | Now | Evidence | +|---|---|---|---| +| Theory files | 23 (18 core + 5 ACL) | **52** (47 `StarForth_*` + 5 `ACL_*`), all in `proof/ROOT` | direct count; `COVERAGE.md` agreed all along | +| `LITHOS_VERSION` | `2.0.1` | **`2.0.0`** | `Makefile.starkernel:83`; §I.2 rolled it back 2026-09-04 | +| ACL pinning | "never in C… no `vm_find_word` + field assignment", *and separately* "pin it in a kernel-specific capsule" | **the rule, plus its one live exception** | `kernel_main.c:771-782` does exactly that, deliberately; `ACL.4th` block 4005 explains why | +| `mkcapsule` blocks | "1024-byte limit… verify with `wc -c`" | **64 chars × 16 lines, range `[2048,5120)`; verify with `--lint`** | `mkcapsule.c:344-345`, `:408-409`, `:430` | + +**Also added:** a `WORK IN PROGRESS` pointer at the top directing a fresh session to +`FABRIC-3.6.md`'s `START HERE`, since `.claude/CLAUDE.md` is what auto-loads and this document +is not. It states explicitly that no reshuffle code exists yet, and that the file's existing +Tripod descriptions remain correct until the reshuffle lands — **deliberately not pre-writing +the post-reshuffle state as though it were current.** + +### XLIV.1 — A finding: §XXXII.2's own correction was incomplete + +`FABRIC-3.md` §XXXII.2 corrected the `mkcapsule` framing to "block range `[2048, 5120)` and a +hard 16-content-line-per-block cap." **Reading the tool directly shows a third constraint it +missed: line length ≤ 64 characters** (`mkcapsule.c:344-345`, `:430` — `validate_forth_blocks` +enforces a "64-char × 16-line block format"). + +**And it explains where the wrong figure came from: 64 × 16 = 1024.** The old "1024-byte limit" +was arithmetically right and operationally wrong — **8 lines of 128 characters is 1024 bytes and +still fails.** A correction that fixes a number while leaving the wrong *kind* of rule in place +is the subtler version of the same error, and §XXXII.2 made it. + +**Recorded rather than propagated:** `FABRIC-3.md` is a living document for another topic and is +not edited from here. `.claude/CLAUDE.md` now carries the full 64×16 rule. + +### XLIV.2 — Punch list + +- ✅ **Item 20 — CLOSED**: all four `.claude/CLAUDE.md` errors corrected, with the pointer added. +- ⬜ **Item 42** (qualify "K"/"conservation", §XXXIX.6) and the `MANIFEST.md` corrections + (§XIII.2) remain — they belong to the files they describe, not to `CLAUDE.md`, and + `MANIFEST.md`'s ride the strip per §XXII.5. +- ⬜ **Item 45, NEW** — carry §XLIV.1's 64-char line limit into the `experiments/bare_metal/README.md` + capsule guidance if it repeats the byte framing. **Not checked; flagged.** diff --git a/FABRIC-3.6.md b/FABRIC-3.6.md index 3a7df13f..29dd2b17 100644 --- a/FABRIC-3.6.md +++ b/FABRIC-3.6.md @@ -12,8 +12,8 @@ > handoff was authored in a container whose default working directory was a *different*, empty > repo on an unrelated remote — if you ever see that, you are in the wrong place.) `master` is > the sole production line. Work on branch **`claude/starshipos-tripod-kernel-reshuffle-itbjns`** -> (head `2032974` at handoff, 34 commits ahead of `master` at `e56974e`, clean fast-forward, -> documentation only — **no code has been written**). +> (a clean fast-forward of `master` at `e56974e`; **documentation only — no reshuffle code has +> been written**. The branch head is the source of truth; do not trust a commit id quoted here). > > **The two documents.** `FABRIC-3.5.md` is the **design record and is authoritative** — every > ruling, with its reasoning and evidence, §I–§XLIII. **This** document is the execution log. @@ -38,11 +38,12 @@ > `1`. **Stage B's evidence is the ledger plus `stadium_conserved()`, never `fleet_conserved`.** > 4. **`dict_hash` *changing* is expected; `dict_hash` *diverging* across architectures is the > stop condition.** §XXXIV.6. Do not "fix" a changed hash. -> 5. **`.claude/CLAUDE.md` has four known-stale claims** (§XXVI.1): 23 theory files (there are -> 52), `LITHOS_VERSION` 2.0.1 (it is 2.0.0), the ACL-pinning rule (contradicted by live code -> at `kernel_main.c:771-782`), and the 1024-byte `mkcapsule` framing (it is block range -> `[2048,5120)` and a 16-content-line cap). **Trust the code over that file where they -> disagree.** +> 5. **Documentation in this repo drifts from the code — trust the code.** `.claude/CLAUDE.md` +> carried four stale claims; **all four were corrected 2026-09-19 (§XLIV) and it is now +> reliable.** Others are not: `capsules/MANIFEST.md` still describes block 4055 as a live +> "immutable ABI" that `FABRIC-2.md:2773` declared stale, and still misdescribes block 2049. +> `FABRIC-0.md` §25.7 lists resolved defects as open. **Where a document and the code +> disagree, the code wins — and record the drift rather than working around it.** > > **Blocked, and not to be worked around:** Phase 3 needs three decisions from Captain Bob — > **B1** channels (one membership or negotiation), **B2** the `SK_SWITCH_MAX_SLOTS` ceiling of @@ -243,9 +244,11 @@ Only after every live type is cut over. **Hermes leaves `is_fleet_foundation` an - [ ] **5.1** — Isabelle/HOL pass. **Deliverable is the restated boundary**, explicitly including §XXV.4's coverage loss — *not* a green build (§XXV.3). -- [ ] **5.2** — Documentation sweep, grepping **by exclusion** (§XXVIII.3): CLAUDE.md's four - errors, `MANIFEST.md`, the `TRIPOD.md`/0.1 contradiction, item 42's K-qualification, - the superseded subsystem docs' update-or-archive call. +- [~] **5.2** — Documentation sweep, grepping **by exclusion** (§XXVIII.3). + **CLAUDE.md's four errors: DONE 2026-09-19 (§XLIV), pointer to this document added.** + Outstanding: `MANIFEST.md` (rides the strip, §XXII.5), the `TRIPOD.md`/0.1 contradiction, + item 42's K-qualification, the superseded subsystem docs' update-or-archive call, and + item 45 (`experiments/bare_metal/README.md` block framing). - [ ] **5.3** — `make sbom`; check `Created:` and `DocumentName` (§XXVI.2). - [ ] **5.4** — `LITHOS_VERSION = 2.1.0`; engine `VERSION` per §XXX.6's rule; roadmap table gains its `2.1.0` line in two live places (§XXVIII.2).