# 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` | 7/19 fully modelled (original 4 + CREATE/VARIABLE/CONSTANT and their runtimes) + `;` guard-only + `:` closed through entry-creation + `compiling_word_id` tracking, DF write (gap b) still open (added 2026-08-14/15) |
| `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` | live (see FINDINGS.md §3 correction); DEFER full up to the DF write, IS/DEFER@ full with FIND sidestepped, `defer_runtime` itself still gap (c) (added 2026-08-14/15) |
| `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 — partially closed 2026-08-14/15.**
  `input_buffer`/`input_length`/`input_pos` turned out to be plain per-VM
  array/scalar fields, not host pointers, and `vm_parse_word` (the
  whitespace-delimited name-parse every CREATE/VARIABLE/CONSTANT/`:`/
  DEFER-family word depends on) is a pure scan — now modelled as
  `forth_parse_word` in `StarForth_Base.thy`, composed end-to-end with
  `dict_insert_entry` for all five name-parsing/entry-creating words
  (`forth_colon_full`/`forth_create_full`/`forth_variable_full`/
  `forth_constant_full`/`forth_defer_full`). Still blocked: words needing
  a *different* scan shape over the same buffer — `(`/`\` comment
  (skip-to-delimiter, not whitespace-delimited), `KEY` (single raw
  character, not a parsed token), `."`/`S"` (delimiter-terminated string
  literal), `ABORT"`'s compile-time half, `SEE` (raw pointer walk) — each
  would need its own scan function modelled against the same fields, not
  automatically unlocked by `forth_parse_word`.
- **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) — **closed end-to-end for CREATE/VARIABLE/CONSTANT/`:`,
  2026-08-14/15.**
  `dict_insert_entry` (`StarForth_Defining_Words.thy`) models the
  word_id-assignment/dictionary-table/`latest_id`/`word_id_next`-counter
  portion; `de_df :: cell` (added to `dict_entry` in `StarForth_Base.thy`)
  and `dict_write_df` close the data-field (DF) write gap (b) for every
  word that treats DF as a plain value. Each of the five words' `forth_
  *_full` definition now composes the real parse, any word-specific guard
  (CONSTANT's stack-underflow check, `:`'s nested-definition check), any
  align/allot step (CREATE's `vm_align`; VARIABLE's `vm_align` +
  `forth_vm_allot_raw`, modelling the raw `vm_allot` C helper distinctly
  from the FORTH word ALLOT), the entry insertion, AND the DF write —
  CREATE/VARIABLE/CONSTANT are now fully modelled words, the first three
  in this entire file. Their runtime companions (`defining_runtime_
  create`/`_variable`/`_constant` — byte-identical C bodies) share one
  new definition, `forth_runtime_read_df`, which also required adding
  `current_executing_word_id` to `vm_state` (mirrors `vm->
  current_executing_entry`). IS/DEFER@ (`StarForth_Defer_Words.thy`) are
  also now modelled end to end, with the FIND-family name-resolution gap
  sidestepped via an explicit `target_wid_opt :: nat option` +
  `is_defer_word :: bool` pair, the same technique
  `physics_freeze_words.c`'s FREEZE-WORD/etc. already established. `:`
  closed to the same point as CREATE/VARIABLE/CONSTANT, 2026-08-15:
  `compiling_word_id` added to `vm_state` (mirrors `vm->compiling_word`),
  set by `forth_colon_entry_half` from `latest_id` on success and forced
  to `None` on the pinned-conflict failure path, matching the real C's
  unconditional `vm->compiling_word = de;` before its own null check.
  Still open: `:`'s vm_align+HERE capture and DF write of the
  threaded-body start address (gap b, same as CREATE/VARIABLE/CONSTANT's
  own DF write, just not yet composed in for `:`); DEFER's own runtime
  (dispatch reassignment via a stored pointer — a fundamentally different
  DF usage, still gap (c), NOT the same shape as IS/DEFER@'s plain-value
  DF access); the pin-shadow name-scan guard everywhere (sidestepped via
  an explicit `pinned_conflict :: bool` parameter); and the FIND-family
  lookup itself, which IS/DEFER@'s sidestep still doesn't model, only
  routes around.
- **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`.*