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.

RESOLVED 2026-09-05: both #1 and #5 moved onto struct VM, following the hold_addr/hold_pos precedent already in include/vm.h. vocabulary_words.c's chain heads, VM-cell addresses, first-char index, and initialized guard now live at vm->vocab (a new VocabularyState struct); control_words.c's cf_stack/leave_*/endof_* bookkeeping now lives at vm->cf (a new ControlFlowState struct). Every word function in both files already took VM *vm, so no call sites outside these two files needed to change. #2, #3, #4, #6, #7 remain open — out of scope for this pass.

---

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. RESOLVED 2026-09-05: now validates via the (newly shared) vm_dict_entry_ok() — the same dictionary-walk check ENTROPY@/ENTROPY! already used, promoted out of starforth_words.c into dictionary_management.c so EXECUTE can call it too.
• ? 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. RESOLVED 2026-09-05: both now go through VM_ADDR/vm_addr_ok/ vm_load_cell/vm_ptr, matching @/,/editor_words.c`'s pattern.
• TYPE (io_words.c) has a signed-overflow bypass in its bounds check (machine-checked witness in the proof). RESOLVED 2026-09-05: replaced the manual addr + count > VM_MEMORY_SIZE sum with vm_addr_ok(vm, addr, count), which is written to avoid exactly this overflow.
• 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. RESOLVED 2026-09-05: all three now call the existing vm_set_base() (previously only used at boot init), which updates both base_addr and vm->base; vm_get_base()/vm_set_base() promoted to public declarations in include/vm.h so word-source files can reach them.
• 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. RESOLVED 2026-09-05: the two ceilings disagreeing was real, but ALIGN's 2MB was the correct one, not ALLOT's 5MB — vm_get_block_addr() maps block N directly to vm->memory + N*BLOCK_SIZE for the entire 5MB arena, and USER_BLOCKS_START (block 2048) lines up exactly with DICTIONARY_MEMORY_SIZE, so letting dictionary growth run past 2MB (as ALLOT/,/C,/2, previously allowed) would silently corrupt live block/user data sharing that same memory. Tightened ALLOT/,/C,/2, to DICTIONARY_MEMORY_SIZE to match ALIGN, not the other way around.
• 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.