admin/LithosAnanake
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

proof/: close the data-field (DF) gap for CREATE/VARIABLE/CONSTANT

Browse Source 
Adds de_df :: cell to dict_entry (StarForth_Base.thy) -- the DF cell
modelled as a plain value, closing gap (b) for every word that only
reads/writes it through its OWNING entry. Confirmed by grep this record
has exactly one construction site in the whole 52-theory suite
(dict_insert_entry), so the field addition's blast radius is contained
to StarForth_Defining_Words.thy alone -- full suite still verifies
unchanged elsewhere.

dict_write_df writes an existing entry's DF by word_id. forth_create_full/
forth_variable_full/forth_constant_full now compose the DF write in,
making CREATE/VARIABLE/CONSTANT the first three FULLY modelled words in
this file (guard through parse through insertion through the DF write --
nothing left unmodelled per word except the pin-shadow name-scan guard,
sidestepped the same way as everywhere else in this suite).

Their runtime companions (defining_runtime_create/_variable/_constant --
confirmed byte-identical C bodies) share one new definition,
forth_runtime_read_df, gated on ds_full matching vm_push's real internal
check. Required adding current_executing_word_id to vm_state (mirrors
vm->current_executing_entry, word-id-indexed like latest_id).

DEFER and : remain at their previous closure level: DEFER's DF write was
already implicitly closed (de_df=0 at creation matches its explicit
*df=0), but its own runtime is a fundamentally different DF usage
(dispatch reassignment via a stored pointer, gap c, not a plain value);
: has no vm_state field for vm->compiling_word tracking.

Full suite (54 theories) verifies green.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
2026-08-15 05:40:02 -04:00
co-authored by Claude Sonnet 5
parent d3d66fb608
commit d59a913e13
3 changed files with 195 additions and 68 deletions
Download Patch File Download Diff File Expand all files Collapse all files
proof/StarForth_Defining_Words.thy
+150 -53
View File
@@ -151,7 +151,7 @@ definition dict_insert_entry :: "string \<Rightarrow> nat \<Rightarrow> bool \<R
dp_last_decay_ns = 0, dp_mass_bytes = 0,
dp_avg_latency_ns = 0, dp_state_flags = 0\<rparr>,
de_acl_ttl = 0, de_acl_allow = True, de_acl_mode = ACL_MODE_TTL,
de_acl_pinned = False\<rparr>
de_acl_pinned = False, de_df = 0\<rparr>
in vm\<lparr>dictionary := (dictionary vm)(wid := Some e),
latest_id := Some wid,
word_id_next := wid + 1\<rparr>)"
@@ -171,7 +171,7 @@ lemma dict_insert_entry_populates_dictionary:
shows "\<exists>e. dictionary (dict_insert_entry name init_flags pinned_conflict vm) (word_id_next vm) = Some e
\<and> de_word_id e = word_id_next vm \<and> de_name e = name \<and> de_flags e = init_flags
\<and> de_heat e = 0 \<and> de_acl_ttl e = 0 \<and> de_acl_allow e \<and> de_acl_mode e = ACL_MODE_TTL
\<and> \<not> de_acl_pinned e"
\<and> \<not> de_acl_pinned e \<and> de_df e = 0"
using assms by (simp add: dict_insert_entry_def Let_def)
lemma dict_insert_entry_advances_counter:
@@ -193,6 +193,36 @@ lemma dict_insert_entry_not_full_word_id_next_bound: True
than DICTIONARY_SIZE words), not claimed to be handled.\<close>
by simp
(* ── Data-field (DF) write, gap (b) PARTIALLY CLOSED 2026-08-15 ──────────
`de_df` (StarForth_Base.thy) models the DF cell as a plain value.
`dict_write_df` writes it into an EXISTING entry by word_id -- the
shared mechanism CREATE/VARIABLE/CONSTANT's own DF write (after
`vm_create_word` already returned) all reduce to. No-op if the word_id
doesn't resolve (mirrors a defensive NULL check that never actually
fires on any real caller in this suite, all of which write DF
immediately after a successful `dict_insert_entry` at a word_id they
just observed being created). *)
definition dict_write_df :: "nat \<Rightarrow> cell \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"dict_write_df wid v vm =
(case dictionary vm wid of
None \<Rightarrow> vm
| Some e \<Rightarrow> vm\<lparr>dictionary := (dictionary vm)(wid := Some (e\<lparr>de_df := v\<rparr>))\<rparr>)"
lemma dict_write_df_present:
assumes "dictionary vm wid = Some e"
shows "dictionary (dict_write_df wid v vm) wid = Some (e\<lparr>de_df := v\<rparr>)"
using assms by (simp add: dict_write_df_def)
lemma dict_write_df_absent_noop:
assumes "dictionary vm wid = None"
shows "dict_write_df wid v vm = vm"
using assms by (simp add: dict_write_df_def)
lemma dict_write_df_data_stack_unchanged:
"data_stack (dict_write_df wid v vm) = data_stack vm"
by (simp add: dict_write_df_def split: option.split)
(* ── [ ( -- ) : interpret mode, LIVE version (see file header) ──────────── *)
(* C: vm_store_cell(vm, vm->state_addr, 0); vm->mode = MODE_INTERPRET. *)
@@ -553,30 +583,25 @@ lemma constant_entry_half_not_full_constant: True
popped value (gap b). See section header.\<close>
by simp
(* ── CONSTANT, full composition, gap (a)+parse CLOSED for this one word
2026-08-14 ─────────────────────────────────────────────────────────────
Demonstrates end-to-end what StarForth_Base.thy's `forth_parse_word`
(added this session, closing the TIB/name-parse gap named as an
unmodelled precondition throughout this suite) unlocks when composed
with `dict_insert_entry`: CONSTANT's real C order is guard (dsp<0) ->
pop value -> parse name -> vm_create_word. Modelled here exactly in
that order, chosen as the flagship composition because it is this
file's simplest word with a real stack guard (unlike CREATE/VARIABLE,
which have no stack precondition at all). Still NOT modelled: the DF
write of the popped value into the new entry (gap b) -- `value` is
computed and discarded here, faithfully matching everything up to
that point but no further. *)
(* ── CONSTANT, full composition, gap (a)+parse+DF CLOSED 2026-08-14/15 ───
CONSTANT's real C order: guard (dsp<0) -> pop value -> parse name ->
vm_create_word -> DF write of the popped value. Now modelled completely
-- the first fully-closed word in this file, and the flagship
composition of `forth_parse_word` (TIB), `dict_insert_entry` (gap a),
and `dict_write_df` (gap b), all added this session. *)
definition forth_constant_full :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"forth_constant_full max_len pinned_conflict vm =
(if data_stack vm = []
then set_error vm
else
let vm1 = vm\<lparr>data_stack := tl (data_stack vm)\<rparr>;
let value = 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 dict_insert_entry nm 0 pinned_conflict vm2)"
else let wid = word_id_next vm2
in dict_write_df wid value (dict_insert_entry nm 0 pinned_conflict vm2))"
lemma constant_full_underflow:
assumes "data_stack vm = []"
@@ -589,7 +614,7 @@ lemma constant_full_success_populates_dictionary:
assumes "max_len \<ge> 2"
assumes "\<not> pinned_conflict"
shows "\<exists>e wid. dictionary (forth_constant_full max_len pinned_conflict vm) wid = Some e
\<and> de_name e \<noteq> '''' \<and> de_flags e = 0"
\<and> de_name e \<noteq> '''' \<and> de_flags e = 0 \<and> de_df e = hd (data_stack vm)"
proof -
let ?vm1 = "vm\<lparr>data_stack := tl (data_stack vm)\<rparr>"
obtain nm vm2 where parse_eq: "forth_parse_word max_len ?vm1 = (nm, vm2)" by fastforce
@@ -598,26 +623,31 @@ proof -
hence nm_nonempty: "nm \<noteq> ''''"
using forth_parse_word_success_nonempty[OF input_pos_unaffected assms(3)] parse_eq
by (metis fstI)
have "forth_constant_full max_len pinned_conflict vm
= dict_insert_entry nm 0 pinned_conflict vm2"
let ?wid = "word_id_next vm2"
let ?vm3 = "dict_insert_entry nm 0 pinned_conflict vm2"
have full_eq: "forth_constant_full max_len pinned_conflict vm = dict_write_df ?wid (hd (data_stack vm)) ?vm3"
using assms(1) parse_eq nm_nonempty by (simp add: forth_constant_full_def)
moreover have "\<exists>e. dictionary (dict_insert_entry nm 0 pinned_conflict vm2) (word_id_next vm2) = Some e
\<and> de_name e = nm \<and> de_flags e = 0"
have "\<exists>e. dictionary ?vm3 ?wid = Some e \<and> de_name e = nm \<and> de_flags e = 0"
using assms(4) by (simp add: dict_insert_entry_def Let_def)
ultimately show ?thesis using nm_nonempty by auto
then obtain e where e_eq: "dictionary ?vm3 ?wid = Some e" "de_name e = nm" "de_flags e = 0" by blast
have "dictionary (dict_write_df ?wid (hd (data_stack vm)) ?vm3) ?wid = Some (e\<lparr>de_df := hd (data_stack vm)\<rparr>)"
using dict_write_df_present[OF e_eq(1)] by simp
thus ?thesis using full_eq e_eq nm_nonempty by auto
qed
(* ── CREATE, full composition, gap (a)+parse CLOSED for this word
2026-08-15 ─────────────────────────────────────────────────────────────
(* ── CREATE, full composition, gap (a)+parse+DF CLOSED 2026-08-15 ────────
CREATE's real C order: parse name -> vm_create_word -> vm_align(vm) ->
capture dfa = here (fed to the still-unmodelled DF write, gap b). No
stack precondition at all (unlike CONSTANT). `forth_align`
(StarForth_Dictionary_Words.thy) is reused directly -- it is exactly
what `vm_align` already models, word-for-word. Composed unconditionally
over `dict_insert_entry`'s result the same way `forth_colon_entry_half`
already does: when `pinned_conflict` holds, the real C returns before
ever calling vm_align, so `forth_align` running anyway on the
already-errored state is a known, minor divergence, not claimed
capture dfa = here -> DF write of dfa. No stack precondition at all
(unlike CONSTANT). `forth_align` (StarForth_Dictionary_Words.thy) is
reused directly -- it is exactly what `vm_align` already models,
word-for-word. The word_id is captured BEFORE `dict_insert_entry`
advances `word_id_next`, then used to target the DF write after
`forth_align` has run (align only touches `here`, never `dictionary`,
so this ordering is safe regardless of which happens first). When
`pinned_conflict` holds, the real C returns before ever calling
vm_align; `forth_align`/`dict_write_df` running anyway on the
already-errored state (a no-op for dict_write_df, since no entry
exists at that word_id) is a known, minor divergence, not claimed
otherwise -- see forth_colon_entry_half's identical precedent. *)
definition forth_create_full :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
@@ -625,7 +655,10 @@ definition forth_create_full :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \
(let (nm, vm1) = forth_parse_word max_len vm
in if nm = ''''
then set_error vm1
else forth_align (dict_insert_entry nm 0 pinned_conflict vm1))"
else
let wid = word_id_next vm1;
vm2 = forth_align (dict_insert_entry nm 0 pinned_conflict vm1)
in dict_write_df wid (word_of_nat (here vm2)) vm2)"
lemma create_full_empty_parse_errors:
assumes "fst (forth_parse_word max_len vm) = ''''"
@@ -646,15 +679,20 @@ 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(1) assms(2)] by (metis fstI)
have "forth_create_full max_len pinned_conflict vm
= forth_align (dict_insert_entry nm 0 pinned_conflict vm1)"
using parse_eq nm_nonempty by (simp add: forth_create_full_def)
moreover have "\<exists>e. dictionary (dict_insert_entry nm 0 pinned_conflict vm1) (word_id_next vm1) = Some e
\<and> de_name e = nm \<and> de_flags e = 0"
using assms(3) by (simp add: dict_insert_entry_def Let_def)
moreover have "dictionary (forth_align vm2) = dictionary vm2" for vm2
let ?wid = "word_id_next vm1"
let ?vm2 = "forth_align (dict_insert_entry nm 0 pinned_conflict vm1)"
have full_eq: "forth_create_full max_len pinned_conflict vm = dict_write_df ?wid (word_of_nat (here ?vm2)) ?vm2"
using parse_eq nm_nonempty by (simp add: forth_create_full_def Let_def)
have dict_eq: "dictionary ?vm2 = dictionary (dict_insert_entry nm 0 pinned_conflict vm1)"
by (simp add: forth_align_def set_error_def Let_def)
ultimately show ?thesis using nm_nonempty by metis
have "\<exists>e. dictionary (dict_insert_entry nm 0 pinned_conflict vm1) ?wid = Some e
\<and> de_name e = nm \<and> de_flags e = 0"
using assms(3) by (simp add: dict_insert_entry_def Let_def)
then obtain e where e_eq: "dictionary ?vm2 ?wid = Some e" "de_name e = nm" "de_flags e = 0"
using dict_eq by auto
have "dictionary (forth_create_full max_len pinned_conflict vm) ?wid = Some (e\<lparr>de_df := word_of_nat (here ?vm2)\<rparr>)"
using full_eq dict_write_df_present[OF e_eq(1)] by simp
thus ?thesis using e_eq(2) e_eq(3) nm_nonempty by fastforce
qed
(* ── VARIABLE, full composition, gap (a)+parse CLOSED for this word
@@ -689,13 +727,21 @@ lemma vm_allot_raw_dictionary_unchanged:
"dictionary (forth_vm_allot_raw bytes vm) = dictionary vm"
by (simp add: forth_vm_allot_raw_def set_error_def)
(* Real C order: parse -> vm_align -> capture addr=here -> vm_allot(cell)
-> vm_create_word -> DF write of addr. `addr` is captured right after
align, BEFORE allot advances `here` again -- gap (b) now closed too. *)
definition forth_variable_full :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"forth_variable_full max_len pinned_conflict vm =
(let (nm, vm1) = forth_parse_word max_len vm
in if nm = ''''
then set_error vm1
else dict_insert_entry nm 0 pinned_conflict
(forth_vm_allot_raw CELL_BYTES (forth_align vm1)))"
else
let vm2 = forth_align vm1;
addr = here vm2;
vm3 = forth_vm_allot_raw CELL_BYTES vm2;
wid = word_id_next vm3
in dict_write_df wid (word_of_nat addr) (dict_insert_entry nm 0 pinned_conflict vm3))"
lemma variable_full_empty_parse_errors:
assumes "fst (forth_parse_word max_len vm) = ''''"
@@ -717,20 +763,71 @@ proof -
hence nm_nonempty: "nm \<noteq> ''''"
using forth_parse_word_success_nonempty[OF assms(1) assms(2)] by (metis fstI)
let ?vm3 = "forth_vm_allot_raw CELL_BYTES (forth_align vm1)"
have "forth_variable_full max_len pinned_conflict vm
= dict_insert_entry nm 0 pinned_conflict ?vm3"
using parse_eq nm_nonempty by (simp add: forth_variable_full_def)
moreover have "\<exists>e. dictionary (dict_insert_entry nm 0 pinned_conflict ?vm3) (word_id_next ?vm3) = Some e
\<and> de_name e = nm \<and> de_flags e = 0"
let ?wid = "word_id_next ?vm3"
have full_eq: "forth_variable_full max_len pinned_conflict vm
= dict_write_df ?wid (word_of_nat (here (forth_align vm1))) (dict_insert_entry nm 0 pinned_conflict ?vm3)"
using parse_eq nm_nonempty by (simp add: forth_variable_full_def Let_def)
have "\<exists>e. dictionary (dict_insert_entry nm 0 pinned_conflict ?vm3) ?wid = Some e
\<and> de_name e = nm \<and> de_flags e = 0"
using assms(3) by (simp add: dict_insert_entry_def Let_def)
ultimately show ?thesis using nm_nonempty by auto
then obtain e where e_eq: "dictionary (dict_insert_entry nm 0 pinned_conflict ?vm3) ?wid = Some e"
"de_name e = nm" "de_flags e = 0" by blast
have "dictionary (forth_variable_full max_len pinned_conflict vm) ?wid = Some (e\<lparr>de_df := word_of_nat (here (forth_align vm1))\<rparr>)"
using full_eq dict_write_df_present[OF e_eq(1)] by simp
thus ?thesis using e_eq(2) e_eq(3) nm_nonempty by fastforce
qed
lemma create_runtime_not_modelled: True \<comment> \<open>defining_runtime_create: reads current_executing_entry's DF cell (gap b).\<close>
(* ── defining_runtime_create / _variable / _constant: gap (b) CLOSED
2026-08-15 ───────────────────────────────────────────────────────────
All three C bodies are byte-identical in shape (defining_words.c:91-160):
guard `current_executing_entry` present, guard its DF cell present,
push the DF value. One shared definition suffices; the real C's
distinction is only which name gets logged, with no vm_state-visible
difference. `current_executing_word_id` (StarForth_Base.thy) models
`vm->current_executing_entry`; the second guard (DF cell present) is
always true here since a live word_id always has an entry with a
`de_df` field in this model -- included anyway via the `None` dictionary
case for defensive symmetry with the C's own two-guard shape, even
though it is unreachable from any real entry point in this suite. A
`ds_full` check is added before the push, matching every other
guarded-push word in this suite that goes through `vm_push`. *)
definition forth_runtime_read_df :: "vm_state \<Rightarrow> vm_state" where
"forth_runtime_read_df vm =
(case current_executing_word_id vm of
None \<Rightarrow> set_error vm
| Some wid \<Rightarrow>
(case dictionary vm wid of
None \<Rightarrow> set_error vm
| Some e \<Rightarrow>
if ds_full vm
then set_error vm
else vm\<lparr>data_stack := de_df e # data_stack vm\<rparr>))"
lemma runtime_read_df_no_executing_entry:
assumes "current_executing_word_id vm = None"
shows "vm_error (forth_runtime_read_df vm)"
using assms by (simp add: forth_runtime_read_df_def set_error_def)
lemma runtime_read_df_pushes_value:
assumes "current_executing_word_id vm = Some wid"
assumes "dictionary vm wid = Some e"
assumes "\<not> ds_full vm"
shows "data_stack (forth_runtime_read_df vm) = de_df e # data_stack vm"
using assms by (simp add: forth_runtime_read_df_def)
lemma runtime_read_df_overflow:
assumes "current_executing_word_id vm = Some wid"
assumes "dictionary vm wid = Some e"
assumes "ds_full vm"
shows "vm_error (forth_runtime_read_df vm)"
using assms by (simp add: forth_runtime_read_df_def set_error_def)
lemma create_runtime_is_read_df: True \<comment> \<open>defining_runtime_create IS forth_runtime_read_df -- see definition above.\<close>
by simp
lemma variable_runtime_not_modelled: True \<comment> \<open>defining_runtime_variable: reads current_executing_entry's DF cell (gap b).\<close>
lemma variable_runtime_is_read_df: True \<comment> \<open>defining_runtime_variable IS forth_runtime_read_df -- see definition above.\<close>
by simp
lemma constant_runtime_not_modelled: True \<comment> \<open>defining_runtime_constant: reads current_executing_entry's DF cell (gap b).\<close>
lemma constant_runtime_is_read_df: True \<comment> \<open>defining_runtime_constant IS forth_runtime_read_df -- see definition above.\<close>
by simp
lemma lit_not_modelled: True \<comment> \<open>LIT: reads/advances the return-stack top as a raw C cell_t* threaded-code IP -- see file header, distinct from control_words.c's already-resolved IP-as-vaddr usage.\<close>
by simp