From 2a084ba037788702cf9db199d60644abbd534677 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Tue, 22 Sep 2026 19:49:08 -0400 Subject: [PATCH] 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 --- FABRIC-3.6.md | 51 +++++++++++++++++++++++++++++++++----------- Makefile | 2 +- lfs/amd64/starforth | Bin 1544744 -> 1544744 bytes sbom.spdx | 6 +++--- sbom.spdx.json | 2 +- 5 files changed, 44 insertions(+), 17 deletions(-) diff --git a/FABRIC-3.6.md b/FABRIC-3.6.md index 2273e696..96297ca1 100644 --- a/FABRIC-3.6.md +++ b/FABRIC-3.6.md @@ -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 diff --git a/Makefile b/Makefile index 6928cfd9..d3757f86 100644 --- a/Makefile +++ b/Makefile @@ -14,7 +14,7 @@ # CONFIGURATION # ============================================================================== -VERSION ?= 3.1.0 +VERSION ?= 3.2.0 CC = gcc # Isabelle configuration diff --git a/lfs/amd64/starforth b/lfs/amd64/starforth index fcb340435686c3f052579ecd0e3ec6c9a357b894..979d248ba6e7af25351e7d4378e0eefa8a81807b 100755 GIT binary patch delta 176 zcmZ3nByPo$xD7j)M0CG8N_y)j7?GBvBcX;*v02*gZ4 z%nZaVK+FonY(UHo#2i4(3B+7L%nigmK+L;c?G2xPqq>ovfkK6aS-hEvLUBoAUP@w7 zih_}Wk(sW6rLK`th@qvGiG`JkL3>RuKM)H5u^duE008ZQ BKehk> diff --git a/sbom.spdx b/sbom.spdx index 58af421d..17b0eebc 100644 --- a/sbom.spdx +++ b/sbom.spdx @@ -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 diff --git a/sbom.spdx.json b/sbom.spdx.json index a93ba59a..7c8f5198 100644 --- a/sbom.spdx.json +++ b/sbom.spdx.json @@ -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"}]}