Robert Allan JamesandClaude Sonnet 5
3426d6a4a7
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 <noreply@anthropic.com>
195 lines
12 KiB
Markdown
195 lines
12 KiB
Markdown
# 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.
|