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>
135 lines
8.5 KiB
Markdown
135 lines
8.5 KiB
Markdown
# 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`.*
|