Phase 5 corrections: sharpen 5.1's boundary claim, fix hosted Makefile's own stale VERSION
Advisor review of the Phase 5 close-out commit caught two real issues: - Task 5.1's write-up claimed the Isabelle pass "confirms no regression" -- overstated. Nothing in proof/'s scope changed, so the pass isn't regression evidence, it's a build-completeness formality; the boundary argument alone already supports the real conclusion. Sharpened. - sbom.spdx was regenerated before the 5.4 version bump, so it briefly understated the engine version. Root cause: the hosted Makefile carries its own separate hardcoded VERSION (Makefile:17, still 3.1.0), distinct from Makefile.starkernel's copy that 5.4 bumped -- duplication CLAUDE.md's own "two independently tracked version strings" note doesn't document. Bumped to 3.2.0 to match, regenerated (PackageVersion now correct), and rebuilt the hosted starforth binary so lfs/amd64/starforth reflects it. Also recorded why 5.1-5.4 landed as one commit (deviation from this document's per-task-commit discipline) and sharpened the riscv64 log entry so the FAILED run and the accepted retry aren't ambiguous to a future reader grepping logs/. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
co-authored by
Claude Sonnet 5
Claude Sonnet 5
parent
a4ad14aec6
commit
2a084ba037
+39
-12
@@ -1347,6 +1347,13 @@ intermediate states.
|
||||
|
||||
## Phase 5 — Close-out
|
||||
|
||||
**Note on commit granularity:** tasks 5.1–5.4 landed as one commit (`a4ad14a`), a deliberate
|
||||
deviation from the per-task-commit discipline this document has otherwise used since Phase 0.
|
||||
Reason: all four tasks' write-ups accumulated in `FABRIC-3.6.md` across one continuous work
|
||||
pass before any commit was made, so splitting the commit would have meant hand-splitting one
|
||||
file's hunks after the fact rather than committing as each task actually finished — the
|
||||
opposite of what per-task commits are for. Tasks 5.5–5.7 return to one-commit-per-task.
|
||||
|
||||
- [x] **5.1** — Isabelle/HOL pass. **Deliverable is the restated boundary**, explicitly
|
||||
including §XXV.4's coverage loss — *not* a green build (§XXV.3).
|
||||
2026-09-22 · **Closed.** `/home/rajames/CLionProjects/Isabelle2011-1/bin/isabelle build
|
||||
@@ -1362,11 +1369,16 @@ intermediate states.
|
||||
Every file this reshuffle changed lives in `src/starkernel/` (kernel-only C, `kernel_
|
||||
hermes.c`/`.h`, `repl.c`, `capsule_*.c`, `kernel_main.c`) or `capsules/*.4th` (Hera/
|
||||
Artemis/Hestia init capsules, the deleted `messaging.4th`/`hermes/init.4th`) — both
|
||||
entirely outside `proof/`'s own stated boundary from the start. The clean pass above
|
||||
confirms no regression in the covered surface, but it is not evidence the reshuffle's
|
||||
*own* new code (kernel-Hermes's C implementation, the WIREBIND/MINT identity flow, the
|
||||
capsule birth/switch-signal changes) is formally verified — none of that was ever in
|
||||
scope for this suite, and still isn't. The suite's already-documented gaps (block-window
|
||||
entirely outside `proof/`'s own stated boundary from the start. **The clean pass above is
|
||||
not regression evidence — nothing in `proof/`'s scope changed, so there was nothing this
|
||||
reshuffle could have regressed there in the first place**; the 41s runtime is a warm
|
||||
heap-cache replay, not a fresh re-verification, so it shouldn't be read as re-checking
|
||||
anything either. It is included for completeness (task 5.1 asks for the build), not as
|
||||
support for a no-regression claim the boundary argument above already makes on its own.
|
||||
Separately, and for the same reason: none of the reshuffle's *own* new code
|
||||
(kernel-Hermes's C implementation, the WIREBIND/MINT identity flow, the capsule
|
||||
birth/switch-signal changes) is formally verified — none of that was ever in scope for
|
||||
this suite, and still isn't. The suite's already-documented gaps (block-window
|
||||
cache, TIB scan-shape variants beyond `forth_parse_word`, vocabulary-chain file-scope
|
||||
statics, raw-pointer DictEntry navigation, the three divergent L8 mode-selector
|
||||
representations — full list in `proof/COVERAGE.md`'s own "structurally NOT provable"
|
||||
@@ -1431,8 +1443,21 @@ intermediate states.
|
||||
a genuine Makefile bug, not a stale artifact: `Makefile:747` hardcodes `--source-name
|
||||
StarForth` in the `sbom` target. Fixed (`--source-name LithosAnanke`, explicit approval
|
||||
obtained first) and regenerated. Both fields now correct: `DocumentName: LithosAnanke`,
|
||||
`Created: 2026-09-22T23:21:56Z`. `sbom.spdx`/`sbom.spdx.json` and the `Makefile` one-line
|
||||
fix ride this phase's commit.
|
||||
`Created: 2026-09-22T23:21:56Z`.
|
||||
|
||||
**Found and fixed, an ordering bug against 5.4:** this regen ran before the version bump
|
||||
(5.4, below), so `sbom.spdx`'s `PackageVersion` came out `3.1.0` — correct at the moment
|
||||
of generation, but stale the moment 5.4 landed. Root cause is a second, independent
|
||||
finding: the hosted `Makefile` (which `sbom` actually runs from — `Makefile.starkernel`
|
||||
is the kernel build, a separate file) carries its **own** hardcoded `VERSION ?= 3.1.0`
|
||||
at `Makefile:17`, never mentioned by `.claude/CLAUDE.md`'s own "two independently tracked
|
||||
version strings" note, which only documents `Makefile.starkernel`'s pair. Two hardcoded
|
||||
copies of the same semantic value (the embedded StarForth engine version) in two build
|
||||
files is real duplication-drift risk, not intentional independence like `LITHOS_VERSION`/
|
||||
`VERSION`'s documented split. Bumped `Makefile:17` to `3.2.0` to match 5.4's engine-version
|
||||
rule and re-ran `make sbom`: `PackageVersion: 3.2.0`, `Created` refreshed again. `sbom.spdx`/
|
||||
`sbom.spdx.json`, the `Makefile:747` `--source-name` fix, and this `Makefile:17` fix all
|
||||
ride this phase's commit.
|
||||
- [x] **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).
|
||||
2026-09-22 · **Closed.** `Makefile.starkernel`: `LITHOS_VERSION` `2.0.0` → `2.1.0`;
|
||||
@@ -1454,12 +1479,14 @@ intermediate states.
|
||||
change, so it gets the same three-arch boot as any kernel change): amd64
|
||||
(`logs/20260922-192400/amd64/`) and aarch64 (`logs/20260922-192931/aarch64/`) both clean
|
||||
on the first pass — zero `UNKNOWN WORD`, banner correctly reads `LithosAnanke v2.1.0` /
|
||||
`StarForth Version 3.2.0`. riscv64's first pass (`logs/20260922-193504/riscv64/`) hit a
|
||||
`StarForth Version 3.2.0`. **riscv64's first pass, `logs/20260922-193504/riscv64/` —
|
||||
FAILED, committed as the audit record of the failure, not a fourth passing run** — hit a
|
||||
`virtio_blk: vblk_io timed out` during the boot-time Zuse genesis mint (fence marker
|
||||
write failed, not persistent) — reached `[zuse@Hera] ok>` regardless, but flagged rather
|
||||
than accepted on a degraded run. Retried immediately with no code change
|
||||
(`logs/20260922-194020/riscv64/`): clean pass, genesis mint succeeded, zero `UNKNOWN
|
||||
WORD`. Assessed as transient host I/O contention under TCG (single qemu process, no
|
||||
write failed, not persistent); reached `[zuse@Hera] ok>` regardless, but flagged rather
|
||||
than accepted on a degraded run. **riscv64's accepted run is the immediate retry,
|
||||
`logs/20260922-194020/riscv64/`**, no code change in between: clean pass, genesis mint
|
||||
succeeded, zero `UNKNOWN WORD`. Assessed as transient host I/O contention under TCG
|
||||
(single qemu process, no
|
||||
leaked processes, host memory tight but not exhausted at the time) rather than a
|
||||
regression — this change touched only `Makefile.starkernel` version strings/comments and
|
||||
two markdown files, no runtime code — and the clean retry on identical disk state/binary
|
||||
|
||||
@@ -14,7 +14,7 @@
|
||||
# CONFIGURATION
|
||||
# ==============================================================================
|
||||
|
||||
VERSION ?= 3.1.0
|
||||
VERSION ?= 3.2.0
|
||||
CC = gcc
|
||||
|
||||
# Isabelle configuration
|
||||
|
||||
Binary file not shown.
@@ -2,11 +2,11 @@ SPDXVersion: SPDX-2.3
|
||||
DataLicense: CC0-1.0
|
||||
SPDXID: SPDXRef-DOCUMENT
|
||||
DocumentName: LithosAnanke
|
||||
DocumentNamespace: https://anchore.com/syft/dir/LithosAnanke-2eaf09a2-c24c-435e-b628-e0dc58035114
|
||||
DocumentNamespace: https://anchore.com/syft/dir/LithosAnanke-d51dd61a-7347-4290-89f9-8896251d48fc
|
||||
LicenseListVersion: 3.28
|
||||
Creator: Organization: Anchore, Inc
|
||||
Creator: Tool: syft-1.52.0
|
||||
Created: 2026-09-22T23:21:56Z
|
||||
Created: 2026-09-22T23:48:18Z
|
||||
|
||||
##### Unpackaged files
|
||||
|
||||
@@ -42,7 +42,7 @@ FileCopyrightText: NOASSERTION
|
||||
|
||||
PackageName: LithosAnanke
|
||||
SPDXID: SPDXRef-DocumentRoot-Directory-LithosAnanke
|
||||
PackageVersion: 3.1.0
|
||||
PackageVersion: 3.2.0
|
||||
PackageSupplier: NOASSERTION
|
||||
PackageDownloadLocation: NOASSERTION
|
||||
PrimaryPackagePurpose: FILE
|
||||
|
||||
+1
-1
@@ -1 +1 @@
|
||||
{"spdxVersion":"SPDX-2.3","dataLicense":"CC0-1.0","SPDXID":"SPDXRef-DOCUMENT","name":"LithosAnanke","documentNamespace":"https://anchore.com/syft/dir/LithosAnanke-30820106-85cc-4f0a-9a13-02c7ab97774d","creationInfo":{"licenseListVersion":"3.28","creators":["Organization: Anchore, Inc","Tool: syft-1.52.0"],"created":"2026-09-22T23:21:56Z"},"packages":[{"name":"LithosAnanke","SPDXID":"SPDXRef-DocumentRoot-Directory-LithosAnanke","versionInfo":"3.1.0","supplier":"NOASSERTION","downloadLocation":"NOASSERTION","filesAnalyzed":false,"licenseConcluded":"NOASSERTION","licenseDeclared":"NOASSERTION","copyrightText":"NOASSERTION","primaryPackagePurpose":"FILE"}],"files":[{"fileName":"lfs/amd64/starforth","SPDXID":"SPDXRef-File-lfs-amd64-starforth-61e983295223f075","checksums":[{"algorithm":"SHA1","checksumValue":"0000000000000000000000000000000000000000"}],"licenseConcluded":"NOASSERTION","licenseInfoInFiles":["NOASSERTION"],"copyrightText":"NOASSERTION"},{"fileName":"lfs/arm64/starforth","SPDXID":"SPDXRef-File-lfs-arm64-starforth-1b0ce26643de8d76","checksums":[{"algorithm":"SHA1","checksumValue":"0000000000000000000000000000000000000000"}],"licenseConcluded":"NOASSERTION","licenseInfoInFiles":["NOASSERTION"],"copyrightText":"NOASSERTION"},{"fileName":"lfs/raspi/starforth","SPDXID":"SPDXRef-File-lfs-raspi-starforth-6f4f7296d88b0a57","checksums":[{"algorithm":"SHA1","checksumValue":"0000000000000000000000000000000000000000"}],"licenseConcluded":"NOASSERTION","licenseInfoInFiles":["NOASSERTION"],"copyrightText":"NOASSERTION"},{"fileName":"lfs/riscv64/starforth","SPDXID":"SPDXRef-File-lfs-riscv64-starforth-619b07683e31fae9","checksums":[{"algorithm":"SHA1","checksumValue":"0000000000000000000000000000000000000000"}],"licenseConcluded":"NOASSERTION","licenseInfoInFiles":["NOASSERTION"],"copyrightText":"NOASSERTION"}],"relationships":[{"spdxElementId":"SPDXRef-DOCUMENT","relatedSpdxElement":"SPDXRef-DocumentRoot-Directory-LithosAnanke","relationshipType":"DESCRIBES"}]}
|
||||
{"spdxVersion":"SPDX-2.3","dataLicense":"CC0-1.0","SPDXID":"SPDXRef-DOCUMENT","name":"LithosAnanke","documentNamespace":"https://anchore.com/syft/dir/LithosAnanke-a6b94918-a7a0-47b1-bc52-8de896255426","creationInfo":{"licenseListVersion":"3.28","creators":["Organization: Anchore, Inc","Tool: syft-1.52.0"],"created":"2026-09-22T23:48:18Z"},"packages":[{"name":"LithosAnanke","SPDXID":"SPDXRef-DocumentRoot-Directory-LithosAnanke","versionInfo":"3.2.0","supplier":"NOASSERTION","downloadLocation":"NOASSERTION","filesAnalyzed":false,"licenseConcluded":"NOASSERTION","licenseDeclared":"NOASSERTION","copyrightText":"NOASSERTION","primaryPackagePurpose":"FILE"}],"files":[{"fileName":"lfs/amd64/starforth","SPDXID":"SPDXRef-File-lfs-amd64-starforth-61e983295223f075","checksums":[{"algorithm":"SHA1","checksumValue":"0000000000000000000000000000000000000000"}],"licenseConcluded":"NOASSERTION","licenseInfoInFiles":["NOASSERTION"],"copyrightText":"NOASSERTION"},{"fileName":"lfs/arm64/starforth","SPDXID":"SPDXRef-File-lfs-arm64-starforth-1b0ce26643de8d76","checksums":[{"algorithm":"SHA1","checksumValue":"0000000000000000000000000000000000000000"}],"licenseConcluded":"NOASSERTION","licenseInfoInFiles":["NOASSERTION"],"copyrightText":"NOASSERTION"},{"fileName":"lfs/raspi/starforth","SPDXID":"SPDXRef-File-lfs-raspi-starforth-6f4f7296d88b0a57","checksums":[{"algorithm":"SHA1","checksumValue":"0000000000000000000000000000000000000000"}],"licenseConcluded":"NOASSERTION","licenseInfoInFiles":["NOASSERTION"],"copyrightText":"NOASSERTION"},{"fileName":"lfs/riscv64/starforth","SPDXID":"SPDXRef-File-lfs-riscv64-starforth-619b07683e31fae9","checksums":[{"algorithm":"SHA1","checksumValue":"0000000000000000000000000000000000000000"}],"licenseConcluded":"NOASSERTION","licenseInfoInFiles":["NOASSERTION"],"copyrightText":"NOASSERTION"}],"relationships":[{"spdxElementId":"SPDXRef-DOCUMENT","relatedSpdxElement":"SPDXRef-DocumentRoot-Directory-LithosAnanke","relationshipType":"DESCRIBES"}]}
|
||||
|
||||
Reference in New Issue
Block a user