proof/: model IS and DEFER@ with the FIND-family gap sidestepped
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>
This commit is contained in:
Robert Allan James
co-authored by
Claude Sonnet 5
Claude Sonnet 5
parent
133f4060aa
commit
6f59e4f27c
+13
-8
@@ -81,7 +81,7 @@ library itself is separately covered by `StarForth_Q48_16.thy`).
|
||||
| `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 (added 2026-08-14/15) |
|
||||
| `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 |
|
||||
@@ -133,13 +133,18 @@ effort on the scale of what's already here:
|
||||
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`). 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)); IS/DEFER@ (need the
|
||||
FIND-family name-resolution gap first); and the pin-shadow name-scan
|
||||
guard everywhere (sidestepped via an explicit `pinned_conflict :: bool`
|
||||
parameter, same technique as the XT-pop gap elsewhere in this suite).
|
||||
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/
|
||||
|
||||
@@ -60,12 +60,88 @@ lemma is_underflow:
|
||||
by (simp add: forth_is_guard_def set_error_def assms)
|
||||
|
||||
lemma is_guard_rest_not_modelled: True
|
||||
\<comment> \<open>Beyond the underflow guard: name parse (unmodelled TIB dependency),
|
||||
vm_find_word (FIND-family gap), the `func != defer_runtime` identity
|
||||
check (unmodellable -- word_table has no per-entry function-identity
|
||||
query in this model), and the DF store (gap b). See file header.\<close>
|
||||
\<comment> \<open>Superseded by forth_is_full below (name parse and DF store are now
|
||||
modelled; only the FIND lookup and identity check are sidestepped,
|
||||
not left as a blank "not modelled"). Kept for its accurate
|
||||
description of the OLD state, not deleted.\<close>
|
||||
by simp
|
||||
|
||||
(* ── IS, full composition (FIND sidestepped), gap (a)+(b) CLOSED where
|
||||
reachable, 2026-08-15 ───────────────────────────────────────────────────
|
||||
`word_is` (defer_words.c:112-154): underflow guard -> pop xt -> parse
|
||||
name -> vm_find_word -> `de->func != defer_runtime` identity check ->
|
||||
DF store. `vm_find_word` and the identity check are both unmodellable
|
||||
in this suite (FIND-family name-resolution gap; `word_table` exposes
|
||||
no per-entry function-identity query) -- sidestepped the same way
|
||||
`physics_freeze_words.c`'s FREEZE-WORD/UNFREEZE-WORD/etc. already
|
||||
sidestep the identical shape: parameterised over an explicit
|
||||
`target_wid_opt :: nat option` (standing in for whatever vm_find_word
|
||||
would have resolved) and `is_defer_word :: bool` (standing in for the
|
||||
identity check's result). Given both, the DF store itself is fully
|
||||
modelled via `dict_write_df`. *)
|
||||
|
||||
definition forth_is_full :: "nat \<Rightarrow> nat option \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
||||
"forth_is_full max_len target_wid_opt is_defer_word vm =
|
||||
(if data_stack vm = []
|
||||
then set_error vm
|
||||
else
|
||||
let xt = hd (data_stack vm);
|
||||
vm1 = vm\<lparr>data_stack := tl (data_stack vm)\<rparr>;
|
||||
(nm, vm2) = forth_parse_word max_len vm1
|
||||
in if nm = ''''
|
||||
then set_error vm2
|
||||
else case target_wid_opt of
|
||||
None \<Rightarrow> set_error vm2
|
||||
| Some wid \<Rightarrow>
|
||||
if \<not> is_defer_word
|
||||
then set_error vm2
|
||||
else dict_write_df wid xt vm2)"
|
||||
|
||||
lemma is_full_underflow:
|
||||
assumes "data_stack vm = []"
|
||||
shows "vm_error (forth_is_full max_len target_wid_opt is_defer_word vm)"
|
||||
by (simp add: forth_is_full_def set_error_def assms)
|
||||
|
||||
lemma is_full_not_found_errors:
|
||||
assumes "data_stack vm \<noteq> []"
|
||||
assumes "fst (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>)) \<noteq> ''''"
|
||||
assumes "target_wid_opt = None"
|
||||
shows "vm_error (forth_is_full max_len target_wid_opt is_defer_word vm)"
|
||||
proof -
|
||||
obtain nm vm2 where parse_eq: "forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>) = (nm, vm2)"
|
||||
by fastforce
|
||||
hence "nm \<noteq> ''''" using assms(2) by simp
|
||||
thus ?thesis using assms(1) assms(3) parse_eq by (simp add: forth_is_full_def set_error_def)
|
||||
qed
|
||||
|
||||
lemma is_full_not_defer_word_errors:
|
||||
assumes "data_stack vm \<noteq> []"
|
||||
assumes "fst (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>)) \<noteq> ''''"
|
||||
assumes "target_wid_opt = Some wid" "\<not> is_defer_word"
|
||||
shows "vm_error (forth_is_full max_len target_wid_opt is_defer_word vm)"
|
||||
proof -
|
||||
obtain nm vm2 where parse_eq: "forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>) = (nm, vm2)"
|
||||
by fastforce
|
||||
hence "nm \<noteq> ''''" using assms(2) by simp
|
||||
thus ?thesis using assms(1) assms(3) assms(4) parse_eq by (simp add: forth_is_full_def set_error_def)
|
||||
qed
|
||||
|
||||
lemma is_full_success_writes_df:
|
||||
assumes "data_stack vm \<noteq> []"
|
||||
assumes "fst (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>)) \<noteq> ''''"
|
||||
assumes "target_wid_opt = Some wid" "is_defer_word"
|
||||
assumes "dictionary (snd (forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>))) wid = Some e"
|
||||
shows "dictionary (forth_is_full max_len target_wid_opt is_defer_word vm) wid = Some (e\<lparr>de_df := hd (data_stack vm)\<rparr>)"
|
||||
proof -
|
||||
obtain nm vm2 where parse_eq: "forth_parse_word max_len (vm\<lparr>data_stack := tl (data_stack vm)\<rparr>) = (nm, vm2)"
|
||||
by fastforce
|
||||
hence "nm \<noteq> ''''" using assms(2) by simp
|
||||
moreover have "dictionary vm2 wid = Some e" using assms(5) parse_eq by simp
|
||||
ultimately show ?thesis
|
||||
using assms(1) assms(3) assms(4) parse_eq dict_write_df_present
|
||||
by (simp add: forth_is_full_def)
|
||||
qed
|
||||
|
||||
(* ── DEFER: entry-creation half, gap (a) PARTIALLY CLOSED 2026-08-14 ─────
|
||||
`word_defer` (src/word_source/defer_words.c:73-101) calls
|
||||
`vm_create_word(vm, name, len, defer_runtime)` with no extra flags set
|
||||
@@ -129,9 +205,59 @@ proof -
|
||||
using assms(3) by (simp add: dict_insert_entry_def Let_def)
|
||||
ultimately show ?thesis using nm_nonempty by auto
|
||||
qed
|
||||
lemma defer_runtime_not_modelled: True \<comment> \<open>defer_runtime: DF read (gap b) + call-through (gap c).\<close>
|
||||
lemma defer_runtime_not_modelled: True \<comment> \<open>defer_runtime: DF read (gap b) + call-through (gap c) -- structurally different from forth_runtime_read_df, since the DF value here is USED as a dispatch target, not just returned. Genuinely still not modelled, not superseded.\<close>
|
||||
by simp
|
||||
lemma defer_fetch_not_modelled: True \<comment> \<open>DEFER@: FIND (name-resolution gap) + DF read (gap b).\<close>
|
||||
lemma defer_fetch_not_modelled: True \<comment> \<open>Superseded by forth_defer_fetch_full below, same as is_guard_rest_not_modelled above.\<close>
|
||||
by simp
|
||||
|
||||
(* ── DEFER@, full composition (FIND sidestepped), gap (a)+(b) CLOSED where
|
||||
reachable, 2026-08-15 ───────────────────────────────────────────────────
|
||||
`word_defer_fetch` (defer_words.c:161-198): parse name -> vm_find_word
|
||||
-> identity check -> DF read + push. Same sidestep as forth_is_full;
|
||||
the DF read itself is fully modelled via `de_df`, with the same
|
||||
`ds_full` guard `forth_runtime_read_df` already established for the
|
||||
equivalent vm_push() call. *)
|
||||
|
||||
definition forth_defer_fetch_full :: "nat \<Rightarrow> nat option \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
||||
"forth_defer_fetch_full max_len target_wid_opt is_defer_word vm =
|
||||
(let (nm, vm1) = forth_parse_word max_len vm
|
||||
in if nm = ''''
|
||||
then set_error vm1
|
||||
else case target_wid_opt of
|
||||
None \<Rightarrow> set_error vm1
|
||||
| Some wid \<Rightarrow>
|
||||
if \<not> is_defer_word
|
||||
then set_error vm1
|
||||
else case dictionary vm1 wid of
|
||||
None \<Rightarrow> set_error vm1
|
||||
| Some e \<Rightarrow>
|
||||
if ds_full vm1
|
||||
then set_error vm1
|
||||
else vm1\<lparr>data_stack := de_df e # data_stack vm1\<rparr>)"
|
||||
|
||||
lemma defer_fetch_full_empty_parse_errors:
|
||||
assumes "fst (forth_parse_word max_len vm) = ''''"
|
||||
shows "vm_error (forth_defer_fetch_full max_len target_wid_opt is_defer_word vm)"
|
||||
proof -
|
||||
obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce
|
||||
hence "nm = ''''" using assms by simp
|
||||
thus ?thesis using parse_eq by (simp add: forth_defer_fetch_full_def set_error_def)
|
||||
qed
|
||||
|
||||
lemma defer_fetch_full_success_pushes_df:
|
||||
assumes "fst (forth_parse_word max_len vm) \<noteq> ''''"
|
||||
assumes "target_wid_opt = Some wid" "is_defer_word"
|
||||
assumes "dictionary (snd (forth_parse_word max_len vm)) wid = Some e"
|
||||
assumes "\<not> ds_full (snd (forth_parse_word max_len vm))"
|
||||
shows "data_stack (forth_defer_fetch_full max_len target_wid_opt is_defer_word vm)
|
||||
= de_df e # data_stack (snd (forth_parse_word max_len vm))"
|
||||
proof -
|
||||
obtain nm vm1 where parse_eq: "forth_parse_word max_len vm = (nm, vm1)" by fastforce
|
||||
hence nm_nonempty: "nm \<noteq> ''''" using assms(1) by simp
|
||||
have "dictionary vm1 wid = Some e" using assms(4) parse_eq by simp
|
||||
thus ?thesis
|
||||
using parse_eq nm_nonempty assms(2) assms(3) assms(5)
|
||||
by (simp add: forth_defer_fetch_full_def)
|
||||
qed
|
||||
|
||||
end
|
||||
|
||||
Reference in New Issue
Block a user