LithosAnanake/proof/FINDINGS.md

# 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.