proof: close :'s compiling_word_id tracking, the last easily-closeable defining-words gap
Adds compiling_word_id :: nat option to vm_state, modelling vm->compiling_word (include/vm.h:421). forth_colon_entry_half now sets it from latest_id on success and forces it to None on the pinned-conflict failure path, matching the real C's unconditional `vm->compiling_word = de;` before its own NULL check in vm_enter_compile_mode (src/vm.c:232-264). : is now closed through entry creation + compiling_word tracking, same point as CREATE/VARIABLE/CONSTANT. Remaining gap for : is the same DF write (gap b, vm_align+HERE capture) those three already closed but not yet composed in here. All 52 theories verify clean (isabelle build -D proof/, ~48s). Part of the pre-Artemis closeout pass (FABRIC-2.md 5.2). PROOFS included per Captain Bob's 2026-08-14 instruction. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
co-authored by
Claude Sonnet 5
Claude Sonnet 5
parent
b9e8fdc3ae
commit
ee3a2e57aa
+18
-11
@@ -70,7 +70,7 @@ library itself is separately covered by `StarForth_Q48_16.thy`).
|
||||
| `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) |
|
||||
| `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 |
|
||||
@@ -116,8 +116,8 @@ effort on the scale of what's already here:
|
||||
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.
|
||||
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`)
|
||||
@@ -137,14 +137,21 @@ effort on the scale of what's already here:
|
||||
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.
|
||||
`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/
|
||||
|
||||
@@ -522,6 +522,13 @@ record vm_state =
|
||||
`latest_id`'s convention, rather than as a raw pointer. *)
|
||||
current_executing_word_id :: "nat option"
|
||||
|
||||
(* ── Compile-time state ───────────────────────────────────────────────
|
||||
Models `vm->compiling_word` (include/vm.h:421, a DictEntry pointer),
|
||||
the entry currently under construction by `:` until `;` clears it.
|
||||
Word-id-indexed (`nat option`), matching `current_executing_word_id`
|
||||
and `latest_id`'s convention, rather than a raw pointer. *)
|
||||
compiling_word_id :: "nat option"
|
||||
|
||||
(* ── Execution state ──────────────────────────────────────────────────── *)
|
||||
vm_mode :: vm_mode
|
||||
vm_ip :: nat \<comment> \<open>instruction pointer (byte offset)\<close>
|
||||
|
||||
@@ -70,10 +70,10 @@ begin
|
||||
remains unmodelled per word: `vm_create_word` itself parses no
|
||||
input (name arrives pre-parsed, but the parse producing that
|
||||
name is the TIB/input-subsystem gap, present throughout this
|
||||
suite), does not capture the entry into any per-VM
|
||||
`vm->compiling_word`-style tracking field (none exists in
|
||||
vm_state), and callers still mutate the returned `DictEntry*`
|
||||
directly afterward for flags beyond what `dict_insert_entry`'s
|
||||
suite; `:` alone captures the entry into `compiling_word_id`,
|
||||
CLOSED 2026-08-15, see `forth_colon_entry_half` below), and
|
||||
callers still mutate the returned `DictEntry*` directly
|
||||
afterward for flags beyond what `dict_insert_entry`'s
|
||||
`init_flags` parameter already captures. This is still a
|
||||
materially bigger gap than the raw-pointer-navigation gap
|
||||
already flagged in dictionary_manipulation_words.c (which only
|
||||
@@ -398,7 +398,7 @@ lemma colon_guard_not_full_colon: True
|
||||
file header finding (a)/(b). Named so the omission is greppable.\<close>
|
||||
by simp
|
||||
|
||||
(* ── : entry-creation half, gap (a) PARTIALLY CLOSED 2026-08-14 ──────────
|
||||
(* ── : entry-creation half, gap (a) CLOSED 2026-08-15 ─────────────────────
|
||||
`vm_enter_compile_mode` (src/vm.c:232-264) does forth_colon_guard's
|
||||
mode/state effect FIRST, then `vm_create_word(...)`, then
|
||||
`de->flags |= WORD_SMUDGED` on the fresh entry (vm.c:251) -- unlike
|
||||
@@ -407,15 +407,24 @@ lemma colon_guard_not_full_colon: True
|
||||
`dict_insert_entry 0`. Composed after forth_colon_guard: only valid
|
||||
when the nested-`:` guard did not already error (real C: vm_create_word
|
||||
is never reached if `defining_word_colon`'s own nested check fired,
|
||||
since that returns before calling vm_enter_compile_mode at all). Still
|
||||
NOT modelled beyond this: name parse, `vm->compiling_word` tracking
|
||||
(no vm_state counterpart -- would need a new field, not attempted
|
||||
here), vm_align+HERE capture, and the DF write of the threaded-body
|
||||
start address (gap b). *)
|
||||
since that returns before calling vm_enter_compile_mode at all).
|
||||
`vm->compiling_word = de;` (vm.c:245) is unconditional -- it runs
|
||||
BEFORE the `if (!de) { vm->error = 1; return; }` check right after it,
|
||||
so compiling_word is set to the fresh entry on success and to NULL
|
||||
(mirrored here as `None`) on failure, in both cases. Modelled via
|
||||
`compiling_word_id` (StarForth_Base.thy), set from `latest_id vm1`
|
||||
after `dict_insert_entry` (which sets `latest_id := Some wid` only on
|
||||
the non-pinned-conflict path and leaves it untouched on the error
|
||||
path) -- explicitly forced to `None` on the pinned_conflict branch so a
|
||||
stale `latest_id` from an earlier successful definition can never leak
|
||||
through as a false "compiling_word" on this failure. Still NOT modelled:
|
||||
vm_align+HERE capture, and the DF write of the threaded-body start
|
||||
address (gap b). *)
|
||||
|
||||
definition forth_colon_entry_half :: "string \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
||||
"forth_colon_entry_half name pinned_conflict vm =
|
||||
dict_insert_entry name WORD_SMUDGED pinned_conflict (forth_colon_guard vm)"
|
||||
(let vm1 = dict_insert_entry name WORD_SMUDGED pinned_conflict (forth_colon_guard vm)
|
||||
in vm1\<lparr>compiling_word_id := (if pinned_conflict then None else latest_id vm1)\<rparr>)"
|
||||
|
||||
lemma colon_entry_half_requires_guard_to_pass:
|
||||
assumes "vm_mode vm \<noteq> ModeCompile" "\<not> pinned_conflict"
|
||||
@@ -430,24 +439,36 @@ lemma colon_entry_half_still_compile_mode:
|
||||
using assms by (simp add: forth_colon_entry_half_def forth_colon_guard_def
|
||||
dict_insert_entry_def Let_def)
|
||||
|
||||
lemma colon_entry_half_sets_compiling_word:
|
||||
assumes "\<not> pinned_conflict"
|
||||
shows "compiling_word_id (forth_colon_entry_half name pinned_conflict vm) =
|
||||
Some (word_id_next (forth_colon_guard vm))"
|
||||
using assms by (simp add: forth_colon_entry_half_def forth_colon_guard_def
|
||||
dict_insert_entry_def Let_def)
|
||||
|
||||
lemma colon_entry_half_conflict_clears_compiling_word:
|
||||
assumes "pinned_conflict"
|
||||
shows "compiling_word_id (forth_colon_entry_half name pinned_conflict vm) = None"
|
||||
using assms by (simp add: forth_colon_entry_half_def)
|
||||
|
||||
lemma colon_entry_half_not_full_colon: True
|
||||
\<comment> \<open>Still NOT modelled: name parse (`name` is a caller-supplied parameter
|
||||
here, not derived from `forth_parse_word` -- see forth_colon_full
|
||||
below), vm->compiling_word tracking (no vm_state field), vm_align+HERE
|
||||
capture, DF write of the threaded-body start address (gap b). See
|
||||
section header.\<close>
|
||||
below), vm_align+HERE capture, DF write of the threaded-body start
|
||||
address (gap b). See section header.\<close>
|
||||
by simp
|
||||
|
||||
(* ── `:`, full composition, gap (a)+parse CLOSED 2026-08-15 ──────────────
|
||||
(* ── `:`, full composition, gap (a)+parse+compiling_word CLOSED 2026-08-15
|
||||
`defining_word_colon` (defining_words.c:407-426): nested-`:` guard
|
||||
FIRST (checked before any parse -- real C order), THEN parse name, THEN
|
||||
`vm_enter_compile_mode` (mode/state effect + WORD_SMUDGED entry
|
||||
creation, already `forth_colon_entry_half`). `forth_parse_word` never
|
||||
touches `vm_mode`, so checking the guard before parsing and reusing
|
||||
`forth_colon_entry_half` (which re-derives the same guard internally
|
||||
via `forth_colon_guard`) afterward is sound -- the mode it observes is
|
||||
unchanged by the intervening parse. Still NOT modelled: vm->
|
||||
compiling_word tracking, vm_align+HERE capture, DF write (gap b). *)
|
||||
creation + compiling_word_id, already `forth_colon_entry_half`).
|
||||
`forth_parse_word` never touches `vm_mode`, so checking the guard
|
||||
before parsing and reusing `forth_colon_entry_half` (which re-derives
|
||||
the same guard internally via `forth_colon_guard`) afterward is sound
|
||||
-- the mode it observes is unchanged by the intervening parse. Still
|
||||
NOT modelled: vm_align+HERE capture, DF write of the threaded-body
|
||||
start address (gap b) -- this is the last remaining gap for `:`. *)
|
||||
|
||||
definition forth_colon_full :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
||||
"forth_colon_full max_len pinned_conflict vm =
|
||||
@@ -496,6 +517,22 @@ proof -
|
||||
ultimately show ?thesis using nm_nonempty by auto
|
||||
qed
|
||||
|
||||
lemma colon_full_success_sets_compiling_word:
|
||||
assumes "vm_mode vm \<noteq> ModeCompile"
|
||||
assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) \<noteq> []"
|
||||
assumes "max_len \<ge> 2"
|
||||
assumes "\<not> pinned_conflict"
|
||||
shows "compiling_word_id (forth_colon_full max_len pinned_conflict vm) \<noteq> None"
|
||||
proof -
|
||||
obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce
|
||||
hence nm_nonempty: "nm \<noteq> ''''"
|
||||
using forth_parse_word_success_nonempty[OF assms(2) assms(3)] by (metis fstI)
|
||||
have "forth_colon_full max_len pinned_conflict vm = forth_colon_entry_half nm pinned_conflict vm1"
|
||||
using parse_eq nm_nonempty assms(1) by (simp add: forth_colon_full_def)
|
||||
thus ?thesis
|
||||
using colon_entry_half_sets_compiling_word[OF assms(4), of nm vm1] by simp
|
||||
qed
|
||||
|
||||
(* ── ; ( -- ) : compile-mode guard only ──────────────────────────────────── *)
|
||||
(* C: error unless vm->mode == MODE_COMPILE; else calls vm_exit_compile_mode,
|
||||
entirely unmodelled (finds/compiles EXIT, flips WORD_SMUDGED/WORD_COMPILED,
|
||||
|
||||
Reference in New Issue
Block a user