From 3426d6a4a75302a6fb12d1f3456f9a86c5a23a61 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Fri, 14 Aug 2026 21:33:00 -0400 Subject: [PATCH] proof/: add FINDINGS.md and COVERAGE.md deliverables for the completed word-source sweep Aggregates the sweep's cross-cutting architectural findings (file-scope statics standing in for per-VM state, missing overflow guards, duplicate word registration/shadowing) and gives an executive-summary coverage index across all 34 src/word_source/*.c files, per Bob's original framing for this initiative. Co-Authored-By: Claude Sonnet 5 --- proof/COVERAGE.md | 134 ++++++++++++++++++++++++++++++++ proof/FINDINGS.md | 194 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 328 insertions(+) create mode 100644 proof/COVERAGE.md create mode 100644 proof/FINDINGS.md diff --git a/proof/COVERAGE.md b/proof/COVERAGE.md new file mode 100644 index 0000000..9f32bb8 --- /dev/null +++ b/proof/COVERAGE.md @@ -0,0 +1,134 @@ +# Isabelle/HOL Proof Suite — Coverage & Purpose + +**Status:** 52 theory files under `proof/`, all verify with zero errors +(`isabelle build -D proof/`, ~35–40s full build). Covers all of +`src/word_source/*.c` (34 files) plus the 7 physics feedback loops, the +word-level ACL system, and core VM correctness/concurrency properties. + +## What this proves, in one sentence + +For every word in the FORTH dictionary that operates purely on modelled +per-VM state (stacks, dictionary, and the ~40 scalar fields this suite has +added to an abstract `vm_state` record as it went), the suite has a +machine-checked, literal transcription of the C implementation's stack +effect, guard conditions, and error behavior — and where a word's real +implementation reaches outside that model (raw pointers, file-scope +statics, TIB/stdio, an unmodelled subsystem like the block-window cache), +the theory says so explicitly rather than silently modelling something +else. + +## Why this matters (the goal, per Bob's original 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. That +boundary is what `proof/FINDINGS.md` (the companion architectural write-up) +draws conclusions from. + +## Structure + +``` +proof/ +├── StarForth_Base.thy # the abstract vm_state record + shared +│ # helpers (vm_addr_ok, cell arithmetic, +│ # resolve_span, etc.) every other file builds on +├── StarForth_Correctness.thy # core interpreter properties +├── StarForth_Concurrent.thy, +│ StarForth_Mutex.thy, +│ StarForth_Transition.thy # cross-cutting VM/concurrency properties +│ # (predate this sweep, part of the earlier +│ # FABRIC-2.md item 5.2 toolchain work) +├── StarForth_Loop{1..7}_*.thy # the 7 physics feedback loops +├── StarForth_Q48_16.thy # Q48.16 fixed-point math library +├── ACL_*.thy (5 files) # word-level ACL policy properties +│ # (pin monotonicity, TTL bounds, no-escalation, +│ # inherit-clears-pin, emergency bypass) +└── StarForth_*_Words.thy (34 files) # one per src/word_source/*.c file — the + # word-by-word coverage sweep this document + # is summarizing +``` + +## Word-source coverage, file by file + +Every `.c` file in `src/word_source/` has a matching `StarForth_*_Words.thy`, +except `q48_16_words.c` (deliberately skipped — it's the underlying Q48.16 +math library, not a FORTH words file; its transcendental approximations need +numerical-analysis proofs unlike the rest of this sweep's style, and the +library itself is separately covered by `StarForth_Q48_16.thy`). + +| Source file | Theory | Coverage | +|---|---|---| +| `dictionary_words.c` | `StarForth_Dictionary_Words.thy` | HERE/ALIGN/ALLOT/`,`/`C,`/`2,`/PAD/LATEST modelled; SP@/SP! unmodelled | +| `dictionary_manipulation_words.c` | `StarForth_Dictionary_Manipulation_Words.thy` | mode/flag half modelled; raw-pointer DictEntry navigation half unmodelled | +| `control_words.c` | `StarForth_Control_Words.thy` | runtime half fully modelled (BRANCH/0BRANCH/?DO/DO/LOOP/+LOOP/LEAVE/UNLOOP/I/J/EXIT); compile-time half unmodelled (file-scope statics, see FINDINGS.md §1) | +| `double_words.c` | `StarForth_Double_Words.thy` | all 20 registered words | +| `string_words.c` | `StarForth_String_Words.thy` | 10/25 (TIB/stdio/strtol clusters deferred) | +| `block_words.c` | `StarForth_Block_Words.thy` | 1/12 (SCR only; rest is the disk-backed block-window cache subsystem, its own proof project) | +| `io_words.c` | `StarForth_IO_Words.thy` | 7/9 (KEY, `."` deferred) | +| `editor_words.c` | `StarForth_Editor_Words.thy` | 0 tractable (all route through the block-window cache; EDIT is also an interactive stdin loop) | +| `format_words.c` | `StarForth_Format_Words.thy` | 17/19 (`#`/`#S` multi-precision division deferred) | +| `system_words.c` | `StarForth_System_Words.thy` | 10/16 + `(ABORT")` helper | +| `vocabulary_words.c` | `StarForth_Vocabulary_Words.thy` | 1/7 partial (entire subsystem is file-scope statics, see FINDINGS.md §1) | +| `defining_words.c` | `StarForth_Defining_Words.thy` | 4/19 full + 2 guard-only (`:`/`;`) | +| `acl_words.c` | `StarForth_ACL_Words.thy` | 7/12 (5 already covered by the pre-existing `ACL_*.thy` policy theories) | +| `dictionary_heat_diagnostic_words.c` | `StarForth_Dictionary_Heat_Diagnostic_Words.thy` | 4/6 full + 1 partial | +| `physics_freeze_words.c` | `StarForth_Physics_Freeze_Words.thy` | 6/9 | +| `physics_diagnostic_words.c` | `StarForth_Physics_Diagnostic_Words.thy` | 3/4 | +| `physics_benchmark_words.c` | `StarForth_Physics_Benchmark_Words.thy` | partial (hot-words cache unmodelled subsystem) | +| `physics_pipelining_diagnostic_words.c` | `StarForth_Physics_Pipelining_Diagnostic_Words.thy` | identity-only, explicit model-blind-spot caveat | +| `starforth_words.c` | `StarForth_StarForth_Words.thy` | 5/12 full + partial guards | +| `framebuffer_words.c`, `keyboard_words.c` | `StarForth_Framebuffer_Words.thy`, `StarForth_Keyboard_Words.thy` | hosted-build fallback branches fully modelled | +| `scroll_words.c`, `ttf_words.c` | `StarForth_Scroll_Words.thy`, `StarForth_TTF_Words.thy` | sentinel-only — words don't exist on hosted builds at all | +| `lifecycle_words_hosted.c` | `StarForth_Lifecycle_Words_Hosted.thy` | 100% — zero deferred remainder | +| `defer_words.c` | `StarForth_Defer_Words.thy` | modelled, but words are dead (shadowed, see FINDINGS.md §3) | +| `log_words.c` | `StarForth_Log_Words.thy` | 100% | +| `q48_words.c` | `StarForth_Q48_Words.thy` | 17/23 | +| `inference_words.c` | `StarForth_Inference_Words.thy` | 5 accessors full; rest guard/shape | +| plus: `arithmetic_words.c`, `stack_words.c`, `return_stack_words.c`, `logical_words.c`, `memory_words.c`, `mixed_arithmetic_words.c` | corresponding `StarForth_*_Words.thy` | pre-date this sweep, part of the original 23-theory FABRIC-2.md §5.2 base | + +## What's structurally NOT provable without a bigger modelling project + +These aren't gaps to close incrementally — each is its own subsystem-modelling +effort on the scale of what's already here: + +- **The disk-backed block-window cache** (`block_subsystem.h` + + `blk_vm_lbn`/`blk_vm_cbuf`/`blk_vm_dirty`/`blk_vm_next`) — blocks + `block_words.c` and `editor_words.c` almost entirely. +- **The TIB / interactive input subsystem** — blocks the `(`/`\` comment + words, `KEY`, `."`, `ABORT"`'s compile-time half, `SEE`. +- **Real stdio/file I/O** — `SAVE-SYSTEM`, parts of `string_words.c`. +- **Raw C-string/strtol-backed words** — the rest of `string_words.c`. +- **Raw-pointer DictEntry navigation** (`>BODY`/`>NAME`/CFA-style words) — + the abstract `dict_entry` model is word-id-indexed, not addressed; no + independent `dsp` register exists to model `SP@`/`SP!` against either. +- **Dictionary insertion** (`vm_create_word`, used by `:`, CREATE, VARIABLE, + CONSTANT, DEFER) — every other file only ever *reads* the abstract + dictionary table; no insertion operation has ever been modelled. +- **The vocabulary chain mechanics** (VOCABULARY/DEFINITIONS/CONTEXT/CURRENT/ + FORTH) — file-scope statics, see FINDINGS.md §1, instance #5. +- **The hot-words cache** (`physics_benchmark_words.c`) and **the bucket/ + lookup-table structure** (`REORG-BUCKETS`) — each its own subsystem. +- **Three divergent L8 mode-selector representations** — see FINDINGS.md §4. + +## How to reproduce + +```bash +/home/rajames/CLionProjects/Isabelle2011-1/bin/isabelle build -v -D proof/ +``` + +(The directory is misleadingly named `Isabelle2011-1` — it's actually +Isabelle2025-2.) A clean run (no `FAILED` in the output) means every theory +in the suite verified — Isabelle sessions fail atomically, so partial +success isn't a state that exists. Full build is ~35–40s warm, ~16 minutes +cold (only relevant if the heap cache is cleared with `-c`, which should not +be done routinely — see `.claude/` session memory on this). + +## Companion document + +`proof/FINDINGS.md` — the cross-cutting architectural findings this sweep +surfaced (file-scope statics standing in for per-VM state, missing overflow +guards, duplicate word registration/shadowing, and several one-off findings +including a highest-severity unchecked-pointer-cast in `EXECUTE`). + +*Generated 2026-08-14, commit `346c793`.* diff --git a/proof/FINDINGS.md b/proof/FINDINGS.md new file mode 100644 index 0000000..e5f38c3 --- /dev/null +++ b/proof/FINDINGS.md @@ -0,0 +1,194 @@ +# Isabelle/HOL Word-Source Sweep — Aggregated Architectural Findings + +**Status:** `src/word_source/*.c` coverage sweep complete as of commit `346c793` +(53 theories, all green, ~35–40s full build). This document synthesizes the +cross-cutting findings the sweep surfaced along the way — each was noted in +the relevant `.thy` file's header comment as it was found; this pulls them +together into one place for review, since no single file's header shows the +pattern's full size. + +These are **not** proof gaps (things the sweep declined to model). They are +real properties of the C implementation that the act of formalizing surfaced. +Nothing here has been fixed — per project convention, findings are reported, +not acted on, until you decide what (if anything) to do about them. + +--- + +## 1. File-scope C statics standing in for per-VM state + +**The single biggest finding of the sweep.** A recurring pattern: state that +conceptually belongs to one VM instance (`struct VM`) is instead a C +file-scope `static`, shared by every VM in the process. In the Tripod +multi-VM fleet (Hera/Hermes/Artemis + any future VMs), this means one VM's +actions silently affect every other VM's behavior through hidden shared +state, with no locking or per-VM isolation. + +Confirmed instances, in the order the sweep found them: + +| # | File | Static(s) | What it backs | Severity | +|---|------|-----------|----------------|----------| +| 1 | `control_words.c` | `cf_stack`/`cf_sp`, `cf_last_mode`, `leave_addrs`/`leave_sp`, `endof_addrs`/`endof_sp` | Compile-time control-flow (IF/THEN/BEGIN/DO/CASE/...) nesting state | **High** — two VMs compiling control structures at overlapping times corrupt each other's nesting; a VM whose compile aborts mid-structure leaves stale state for whoever compiles next. The one reset guard (`cf_epoch_sync`) is itself a single global. | +| 2 | `dictionary_manipulation_words.c` | `static cell_t state_variable` | Backed `[`, `]`, `STATE`; also written (inertly) by `INTERPRET` | **Mixed** — `[`/`]`/`STATE` were dead/shadowed and have been **removed** (§3 instance #1). `INTERPRET` is live (not shadowed) and still writes this static on every call, but the write is functionally inert since nothing on any live path reads it anymore; left alone as a live registered word rather than edited under this repair's scope. | +| 3 | `string_words.c` | `static vaddr_t word_scratch_addr` | `WORD`'s scratch buffer | **Medium** — lazily allocated on first call, reused by every VM thereafter. | +| 4 | `system_words.c` | `static int system_running`, `static int forth_79_standard` | `COLD`/`WARM`/`BYE` run-state; `79-STANDARD` mode flag | **Medium** — process-wide instead of per-VM. | +| 5 | `vocabulary_words.c` | `forth_vocab`/`context_vocab`/`current_vocab`, `context_var_addr`/`current_var_addr`, first-char search index, plus `static int initialized` guard | **The entire vocabulary subsystem** | **Highest severity in the sweep** — one VM's `VOCABULARY`/`DEFINITIONS`/`FORTH` silently changes where *every* VM looks up and defines words. The `initialized` guard compounds it: only the first VM to touch any vocabulary word ever seeds the vocabulary roots, seeded from *its own* dictionary. | +| 6 | `starforth_words.c` | `g_prng_state` | `SEED`/`RANDOM` | **Medium** — every VM in the fleet draws from the same RNG stream (also a reproducibility/determinism concern for the DoE campaigns, not just isolation). | +| 7 | `ttf_words.c` | `static int g_ttf_font_ready` | TTF font-load-once gate | **Low–Medium** — one VM's font initialization silently satisfies the "ready" check for every other VM. | + +Seven confirmed live instances, plus one dead-code instance (#2, see §3). +**All were found incidentally** — the sweep wasn't looking for this pattern, +it kept encountering it because `vm_state` (the abstract model) only has a +field when the C genuinely threads it through `struct VM`, so file-scope +statics kept showing up as "this word can't be modelled against per-VM state +the way its siblings can." + +**Recommendation:** #5 (vocabulary) and #1 (control-flow compile state) are +the two that would actually corrupt VM behavior in the live Tripod fleet +today, if two VMs exercise them concurrently. Worth scoping as a real fix +independent of this proof work — moving these into `struct VM` fields. + +--- + +## 2. Missing overflow/capacity guards before stack pushes + +**Corrected after re-checking against the real C, not just the proof +model** (2026-08-14, during the repair pass below). The sweep's `.thy` files +flagged ~15 words across 6 files as pushing with no capacity check. On +inspection, that overstated the real defect count by a lot — the abstract +proof model's `push` helper didn't credit two things the real C already +does: + +- **`vm_push()`** (`src/stack_management.c:75`) bounds-checks internally + (`if (vm->dsp >= STACK_SIZE - 1) { vm->error = 1; return; }`) before every + write. Any word that calls `vm_push()` — `FB-WIDTH`/`FB-HEIGHT`, all four + flagged keyboard words, and all `LOG-*`/`LOG-LEVEL@` words — was already + safe. Not a bug; a proof-model gap (fixed in the theories, no C change + needed). +- **`VM_PUSH`/`VM_POP`** (`include/vm.h:706-719`) is a macro that resolves + to the checked `vm_push`/`vm_pop` in every build **except** one compiled + with `STARFORTH_PERFORMANCE` defined, which switches it to unchecked + `vm_push_fast`/`vm_pop_fast`. Repo-wide grep confirms `STARFORTH_PERFORMANCE` + is **never defined by any Makefile or Kconfig target in this repo** — + only referenced inside `vm.h` itself and `stack_words.c`. So `Q.1`/`Q.0`/ + `Q.SCALE` (`q48_words.c`) and the `INFER-*@`/`WINDOW-DIVERSITY`/`L8-MODE`/ + `BAYES-*` words (`inference_words.c`), which all go through `VM_PUSH`, + are safe under every configuration this repo currently builds. The + exposure is real but dormant — it would only activate if some future + build target defined that macro, which is a build-configuration decision, + not a per-word bug to patch 14 times over. + +**The one real, live, unconditional instance:** `DECAY-RATE@` +(`physics_freeze_words.c`) writes straight to `vm->data_stack[vm->dsp++]` +with no guard at all and no prior pop to make room — unlike its +neighbors in the same file (`FROZEN?`, `HEAT@`) which pop 2 before pushing +1, net-shrinking the stack and therefore can't overflow. **Fixed**: added +the same `if (vm->dsp >= STACK_SIZE) { vm->error = 1; return; }` guard +`LOOKUP-STRATEGY@` (`dictionary_heat_diagnostic_words.c:98`) already uses +for the identical shape. + +--- + +## 3. Duplicate word registration / dead-code shadowing + +Three confirmed instances where two different C files register a +same-named word, and FORTH's newest-registration-wins dictionary lookup +means the earlier registration is permanently dead code: + +1. **`[`, `]`, `STATE`** — `dictionary_manipulation_words.c` (module 13) + registered first, `defining_words.c` (module 17) registered the same + names later and shadowed them. **Repaired 2026-08-14**: removed the + three dead functions (`dictionary_m_word_left_bracket`/ + `right_bracket`/`state`) and their `register_word()` calls from + `dictionary_manipulation_words.c` — confirmed via repo-wide grep they + had no other callers or header declarations. The live + `defining_words.c` versions (`vm->state_addr`) are untouched. + **Correction**: `INTERPRET` is *not* part of this shadow — + `defining_words.c` never registers a word by that name, so + `dictionary_manipulation_words.c`'s `INTERPRET` is the only + registration and is live, reachable code (see §1 instance #1's updated + text). It still writes the dead `state_variable` static on every call, + but that write is functionally inert (nothing on any live path reads + it) and, being a live registered word, was left alone rather than + edited under this repair's "confirmed-dead-registrations-only" scope — + reported, not touched. +2. **`DEFER`, `IS`, `DEFER@`** — `defer_words.c` (module 27) shadows + `defining_words.c` (module 17) in **both** hosted and kernel builds + (`defer_words.c` has no `__STARKERNEL__` guard despite CLAUDE.md + documenting it as a "kernel-only addition"; the hosted Makefile wildcards + it in regardless). **Repaired 2026-08-14**: removed the three dead + functions (`defining_word_defer`/`is`/`defer_fetch`) and the now-orphaned + `defining_runtime_defer` helper (would otherwise trigger an + unused-static-function warning under `-Wall -Werror`) plus their + `register_word()` calls from `defining_words.c`. The live + `defer_words.c` implementation is entirely separate code, untouched. +3. **`starforth_words.c`'s own double-registration** — + `register_starforth_words` registers 10 words into the STARFORTH + vocabulary, then re-registers 12 words (the same 10 plus `ENTROPY@`/ + `ENTROPY!`) into that same vocabulary context. Not yet judged + intentional or not — resolving that needs the vocabulary-chain mechanics, + which are themselves unmodelled (see §1 instance #5). Not touched. + +**Verification for #1/#2's repair:** hosted `make` builds clean with zero +warnings under `-Wall -Werror`; the hosted build's own comprehensive +self-test suite (runs automatically at every startup) passed 965/965 +implemented tests, 0 failures, 0 errors, including the `Defining Words +Tests (Module 13)` block that exercises `DEFER`/`IS`/`DEFER@` end to end +through the live `defer_words.c` path. Three-arch QEMU boot acceptance +(per `.claude/CLAUDE.md`, mandatory for any change touching vendored +kernel word-source) — see this document's closing status line for result. + +--- + +## 4. Notable one-off findings (not patterns, but worth knowing) + +- **`EXECUTE`** (`system_words.c`) casts a popped cell straight to a + `DictEntry` host pointer and calls through it, gated only by a null + check. Same hazard class as `?`/`DUMP` below, but far more consequential + since `EXECUTE` is a core, ubiquitous primitive rather than a diagnostic + word. **Flagged as the highest-severity single-word finding in the + sweep.** +- **`?` and `DUMP`** (`format_words.c`) cast the popped cell straight to a + host pointer and dereference it, bypassing `vm_addr_ok` — an + out-of-VM-bounds read. +- **`TYPE`** (`io_words.c`) has a signed-overflow bypass in its bounds + check (machine-checked witness in the proof). +- **`DECIMAL`/`HEX`/`OCTAL`** (`format_words.c`) write only the memory cell + at `base_addr`, never `vm->base` (the separate host-mirror field number- + *output* words actually read via `current_base()`) — proved as + `decimal_does_not_change_vm_base` et al. Net effect: these words silently + affect number *parsing* but never number *printing*. +- **`LATEST`** (`dictionary_words.c`) has a body identical to `HERE` (both + push `vm->here`) — does not consult `vm->latest` despite its doc comment + claiming otherwise. +- **`ALIGN`** bounds-checks `here` against `DICTIONARY_MEMORY_SIZE` (2MB) + while `ALLOT`/`,`/`C,`/`2,` check against `VM_MEMORY_SIZE` (5MB) instead — + two different ceilings for the same pointer. +- **`INFER-*` (`array_ptr`, `inference_words.c`)** sets `vm->error` *and* + still pushes a placeholder value anyway — violates the "error or push, + never both" shape essentially every other word in the sweep follows. +- **Three different L8 mode-selector representations exist** in the live + system: the 4-mode `ssm_l8` field this suite has modelled since early in + the sweep, a legacy 16-mode `ssm_l8_state_t` that `L8-MODE`/`L8-UPDATE`/ + `L8-APPLY` actually manipulate, and a separate 128-config adaptive table + that `L8-TABLE-FORCE`'s own comment says the heartbeat's bandit actually + drives. Open question for you — not guessed at in the proof. + +--- + +## Where these came from + +Each finding above is documented in full (with the specific line numbers +and the lemma that proves it, where machine-checked) in the header comment +of its `.thy` file under `proof/`. This document is an index and synthesis, +not a replacement — consult the individual file for the exact argument. + +*Generated 2026-08-14 from the completed word-source sweep, commit `346c793`.* + +**Repair-pass acceptance, 2026-08-14:** three-architecture QEMU boot, one at +a time per `.claude/CLAUDE.md`. All three reached `ok>` with an **identical** +dictionary parity hash (`0x24b4279f0670aa3a`) and identical self-test results +(`Total tests run: 1003, Passed: 965, Failed: 0, Errors: 0`) — +`logs/20260814-195128/amd64`, `logs/20260814-201210/aarch64`, +`logs/20260814-202224/riscv64`. Confirms the §2/§3 repairs (the +`DECAY-RATE@` guard and the two dead-registration removals) introduced no +behavioral drift on any architecture.