FABRIC-3.5.md §XXV: DoE constraint relaxed; Isabelle/HOL pass closes the sequence

Captain Bob, 2026-09-19. The DoE's invocative paths are slated for
rewrite, so doe_log.c's six Tripod-hardcoded columns stop being the
expensive consequence §XIII.3 named -- the schema change is absorbed
rather than paid, and doe-campaign.4th's five by-name Hermes sites fold
into the same rewrite. Notes what this does not relax: §XXII.3's
strip-safety rule stands on its own footing, since rewriting how the
apparatus is invoked is not discarding the apparatus, and the audit and
patent-support roles are unchanged. Experiment capsules stay
live-by-default during the strip.

A formal re-verification pass runs at the end, giving the sequence a
symmetry -- the surgical strip opens it, Isabelle/HOL closes it.

Corrects CLAUDE.md while scoping it: it claims proof/ holds 23 theory
files, 18 core plus 5 ACL. There are 52, all listed in proof/ROOT, and
COVERAGE.md already says 52. Stale by more than a factor of two; added to
item 20's documentation reconciliation.

Records the standard the pass must meet, which COVERAGE.md already states
in Bob's own framing: a clean pass/fail is not the deliverable, the
boundary between formally verified and not-for-this-reason is. A suite
that still compiles while quietly covering less would satisfy the build
and fail the standard.

States a cost of this reshuffle not previously named anywhere. COVERAGE.md
scopes the suite to words over modelled per-VM state and explicitly flags
implementations that reach outside it via file-scope statics. Messaging
today is FORTH over per-VM dictionary state, inside the model;
kernel-Hermes makes it C with file-scope statics, outside it. So the
reshuffle is likely a net reduction in formal coverage of the messaging
area -- plausibly the right trade given §III.2's circular-dependency
argument, but a real one the pass must name rather than let the boundary
move quietly. Partially offset by the one-way latch being close to the
easiest thing here to prove.

Maps the affected theories, and carries forward the observation that
ACL_No_Escalation.thy already proves no-escalation at word level, making
§VI.1's central safety claim the same theorem one level up. The
reshuffle's most important safety property is already half-proven at a
different granularity.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VkM1zHGvBerLF6aqkHPweP

FABRIC-3.5.md

@@ -2304,3 +2304,117 @@ the three.
   `.claude/CLAUDE.md` (twice) and `ACL.4th`/`kernel_main.c`. Documentation, not code; outside
   this reshuffle.
 - Build sequencing otherwise unchanged (§XXIII.6), with the surgical strip still item 1.
+
+---
+
+## XXV. DoE constraint relaxed; a formal re-verification pass closes the sequence (Captain Bob, 2026-09-19)
+
+**Captain Bob, verbatim:** "Don't worry about the DoE, I'm anticipating a rewrite of its
+invocative paths. AND at the end redo a lot of Isabelle/HOL."
+
+### XXV.1 — RULING: the DoE CSV schema stops being "the expensive consequence"
+
+§XIII.3 named `doe_log.c`'s six Tripod-hardcoded columns as the costly part of changing Tripod
+membership, and §XVII.4/§XIX.6 carried it forward as such. **With the DoE's invocative paths
+slated for rewrite, that cost is absorbed rather than paid.** Two items collapse:
+
+- **Punch item 5** (the CSV schema change) is no longer a constraint on the reshuffle. The
+  columns become `hestia_heat_q48`/`switch_hestia_readiness` as part of the DoE rewrite, not as
+  a reluctant edit to a schema that had to stay comparable.
+- **§XIII.1's sites 9–13** — `doe-campaign.4th`'s five `S" Hermes" VM-EXEC` calls — fold into
+  the same rewrite. They were already classed "not auto-run"; they are now explicitly someone
+  else's problem, in a good way.
+
+**One thing this does *not* relax, stated to avoid over-reading it.** §XXII.3's strip-safety
+rule stands on its own footing: the hazard there was a naive grep deleting `init-l8-*`, the
+workloads and `sdk.4th` **by accident**, passing all three architectures cleanly and surfacing
+months later. Rewriting how the apparatus is *invoked* is not the same as discarding the
+apparatus, and its evidentiary role is unchanged — `.claude/CLAUDE.md` still records the
+`logs/` artifacts as committed audit artifacts and the campaign report as patent support
+material. **Experiment capsules remain live-by-default during the strip.**
+
+### XXV.2 — RULING: Isabelle/HOL re-verification is the closing item
+
+A formal re-proof pass runs **at the end**, after the build work. That gives the sequence a
+deliberate symmetry: **the surgical strip opens it (§XXII.6 item 1), formal re-verification
+closes it.**
+
+**Correction to `.claude/CLAUDE.md` while establishing scope.** It states `proof/` "contains 23
+Isabelle/HOL theory files (same composition as the standalone StarForth repo — 18 core VM/
+word-category theories + 5 ACL theories)." Traced 2026-09-19: there are **52 `.thy` files** —
+5 `ACL_*` and 47 `StarForth_*` — and **all 52 are listed in `proof/ROOT`**, so none is orphaned.
+`proof/COVERAGE.md` says 52 and is correct; CLAUDE.md is stale by more than a factor of two.
+**Added to item 20's documentation reconciliation.** Build invocation is `isabelle build -D
+proof/` directly; neither Makefile defines a target (that part of CLAUDE.md is accurate).
+
+### XXV.3 — The standard this pass must meet is already written, and it is not "the proofs build"
+
+`proof/COVERAGE.md` states the goal in Captain Bob's own framing:
+
+> Prove the StarForth VM system as close to bare metal as possible under Isabelle/HOL, and —
+> just as importantly — **identify precisely what cannot be proven and why. A clean pass/fail
+> isn't the deliverable; the boundary between "formally verified" and "not, for this specific
+> reason" is.**
+
+So the deliverable of the closing pass is **a restated boundary**, not a green build. A suite
+that still compiles while quietly covering less than it did would satisfy the build and fail
+the actual standard.
+
+### XXV.4 — The honest cost: this reshuffle moves messaging *out* of the provable region
+
+**Not previously stated anywhere in this document, and it should be, before it is discovered.**
+`COVERAGE.md` defines what the suite can reach: words "that operate purely on modelled per-VM
+state (stacks, dictionary, and the ~40 scalar fields this suite has added to an abstract
+`vm_state` record)" — and, explicitly, where an implementation "reaches outside that model (raw
+pointers, **file-scope statics**, TIB/stdio, an unmodelled subsystem), the theory says so
+explicitly rather than silently modelling something else."
+
+Today's messaging layer is FORTH over per-VM dictionary state — **inside** the model.
+Kernel-Hermes makes it C with file-scope statics — **outside** it. Likewise the sinking latch
+(§XXIII.2) is by design a kernel-resident scalar.
+
+**So the reshuffle is very likely a net reduction in formal coverage of the messaging area.**
+That may well be the right trade — §III.2's circular-dependency argument for moving it is
+strong — but it is a real cost, and by this project's own standard the pass must *name* it
+rather than let the boundary quietly move.
+
+**Partially offsetting, and cheap:** the one-way latch is close to the easiest thing in this
+design to prove. Single writer, one irreversible transition, both observable values valid
+(§XXIII.3) — and `StarForth_Mutex.thy`, `StarForth_Concurrent.thy` and
+`StarForth_Transition.thy` already exist as the homes for exactly that reasoning.
+
+### XXV.5 — What the pass will actually touch, mapped
+
+| Theory | Why this reshuffle touches it |
+|---|---|
+| **`ACL_No_Escalation.thy`** | **The central one — see below.** |
+| `ACL_Inherit_Clears_Pin.thy` | §XV.1's "almost a clone with its own ACL DNA" *is* inheritance semantics |
+| `ACL_Pin_Monotone.thy` | Same monotonicity shape as the §XXIII.3 latch |
+| `StarForth_System_Words.thy` | `BYE` lives here; §XXIV adds a Hera-only sibling beside it |
+| `StarForth_Framebuffer_Words.thy` | `PLOT`/`FB-WIDTH`/`FB-HEIGHT` registration moves to Hestia (§XVIII.3) |
+| `StarForth_Lifecycle_Words_Hosted.thy` | Birth/lifecycle adjacency |
+| `StarForth_Mutex` / `_Concurrent` / `_Transition` | The sinking latch's safety argument |
+
+**The observation worth carrying into the pass:** `ACL_No_Escalation.thy` already proves a
+no-escalation property at the **word** level. §VI.1's central safety claim — *a VM can never
+birth something with more authority than it itself holds* — is **the same theorem one level
+up**, at VM granularity. And §IX.2's "authority only ever flows down the birth graph, never
+sideways and never up" is a graph invariant of exactly the kind this suite is good at.
+
+**The reshuffle's most important safety property is therefore already half-proven, at a
+different granularity.** Lifting it is a better-defined task than it would be from a standing
+start — and per §VI.1 the property is structural (enforced by inheritance, no gate to bypass),
+which is precisely the kind of claim that survives formalization.
+
+### XXV.6 — Punch list
+
+- ✅ **Item 5 (DoE CSV schema) — RELAXED** (§XXV.1). Absorbed by the DoE invocative-path
+  rewrite; no longer a constraint.
+- ⬜ **Item 21, NEW — the closing Isabelle/HOL pass** (§XXV.2–XXV.5). Runs last. Deliverable is
+  a restated boundary per §XXV.3, explicitly including §XXV.4's coverage loss, not a green
+  build.
+- ⬜ **Item 20 grows** (§XXV.2): CLAUDE.md's "23 theory files" joins the ACL-pinning
+  contradiction in the documentation reconciliation.
+- ⬜ **Item 18** (§XVI.7) — the empty-floor halt. **Still the last undecided design item.**
+- Sequence otherwise unchanged (§XXIII.6): surgical strip first, build, formal re-verification
+  last.