CLAUDE.md: correct four stale claims, add reshuffle pointer; record as FABRIC-3.5 §XLIV
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VkM1zHGvBerLF6aqkHPweP
This commit is contained in:
+28
-7
@@ -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/<arch>/kernel/starkernel_loader.efi` + `build/<arch>/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
|
||||
|
||||
Reference in New Issue
Block a user