Robert Allan JamesandClaude Sonnet 5
6f59e4f27c
Both words' real blockers are vm_find_word (name resolution, still unmodelled everywhere in this suite) and a de->func != defer_runtime identity check (unmodellable -- word_table exposes no per-entry function identity). Sidestepped the same way physics_freeze_words.c's FREEZE-WORD/UNFREEZE-WORD/etc. already do: parameterised over an explicit target_wid_opt :: nat option (whatever vm_find_word would have resolved) and is_defer_word :: bool (the identity check's result). Given both, forth_is_full's DF write and forth_defer_fetch_full's DF read are fully modelled via dict_write_df/de_df, including IS's own real stack-underflow guard and both words' ds_full push guard. defer_runtime itself remains unmodelled -- it's a structurally different DF usage (the DF value is used as a dispatch target via word_table, gap c, not just returned to the caller like the other DF-reading words). Full suite (54 theories) verifies green. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
175 lines
12 KiB
Markdown
175 lines
12 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` | 7/19 fully modelled (original 4 + CREATE/VARIABLE/CONSTANT and their runtimes) + `;` guard-only + `:` full except `compiling_word` tracking (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**, `:`/DEFER closed up to `vm->compiling_word` tracking.
|
||
`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. Still
|
||
open: `:`'s `vm->compiling_word` tracking (no vm_state field, so `:`
|
||
stops just short of full closure); 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`.*
|