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

proof/: model the TIB name-parse primitive, close it into CONSTANT's full model

Browse Source 
input_buffer/input_length/input_pos (include/vm.h:415-417) turned out to
be plain per-VM array/scalar fields, not host pointers -- unlike almost
every other input-adjacent gap in this suite. vm_parse_word (src/vm.c:
137-160) is a pure whitespace-delimited scan over them, now modelled as
forth_parse_word in StarForth_Base.thy (is_ws + dropWhile/takeWhile,
faithful to the C's skip-then-copy-with-truncation loop, including that
input_pos only advances past a truncated token by what was actually
copied, matching the C's `len < max_len - 1` bound exactly).

dict_insert_entry (added last session) now takes the entry's name as a
parameter instead of hardcoding the empty string. forth_constant_full
composes forth_parse_word with dict_insert_entry end-to-end as a worked
example: CONSTANT's real order (stack-underflow guard -> pop value ->
parse name -> vm_create_word) is modelled in full up to the data-field
write, which remains the one still-open gap. The other four entry-half
definitions (:/CREATE/VARIABLE/DEFER) take the parsed name as a caller
parameter for now rather than repeating the same composition four more
times in one pass.

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-14 22:53:11 -04:00
co-authored by Claude Sonnet 5
parent cc46cf83f1
commit 1aca77d55c
4 changed files with 229 additions and 54 deletions
Download Patch File Download Diff File Expand all files Collapse all files
proof/StarForth_Defining_Words.thy
+101 -42
View File
@@ -139,13 +139,13 @@ definition WORD_SMUDGED :: nat where "WORD_SMUDGED = 0x20"
initializers (acl_ttl=0, acl_allow=True, acl_mode=ACL_MODE_TTL=0,
acl_pinned=False) -- src/dictionary_management.c:427-430. *)
definition dict_insert_entry :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"dict_insert_entry init_flags pinned_conflict vm =
definition dict_insert_entry :: "string \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"dict_insert_entry name init_flags pinned_conflict vm =
(if pinned_conflict
then set_error vm
else
let wid = word_id_next vm;
e = \<lparr>de_name = '''', de_flags = init_flags, de_heat = 0,
e = \<lparr>de_name = name, de_flags = init_flags, de_heat = 0,
de_word_id = wid,
de_physics = \<lparr>dp_temperature_q8 = 0, dp_last_active_ns = 0,
dp_last_decay_ns = 0, dp_mass_bytes = 0,
@@ -158,28 +158,29 @@ definition dict_insert_entry :: "nat \<Rightarrow> bool \<Rightarrow> vm_state \
lemma dict_insert_entry_pinned_conflict_errors:
assumes "pinned_conflict"
shows "vm_error (dict_insert_entry init_flags pinned_conflict vm)"
shows "vm_error (dict_insert_entry name init_flags pinned_conflict vm)"
by (simp add: dict_insert_entry_def set_error_def assms)
lemma dict_insert_entry_assigns_fresh_word_id:
assumes "\<not> pinned_conflict"
shows "latest_id (dict_insert_entry init_flags pinned_conflict vm) = Some (word_id_next vm)"
shows "latest_id (dict_insert_entry name init_flags pinned_conflict vm) = Some (word_id_next vm)"
using assms by (simp add: dict_insert_entry_def Let_def)
lemma dict_insert_entry_populates_dictionary:
assumes "\<not> pinned_conflict"
shows "\<exists>e. dictionary (dict_insert_entry init_flags pinned_conflict vm) (word_id_next vm) = Some e
\<and> de_word_id e = word_id_next vm \<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"
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"
using assms by (simp add: dict_insert_entry_def Let_def)
lemma dict_insert_entry_advances_counter:
assumes "\<not> pinned_conflict"
shows "word_id_next (dict_insert_entry init_flags pinned_conflict vm) = word_id_next vm + 1"
shows "word_id_next (dict_insert_entry name init_flags pinned_conflict vm) = word_id_next vm + 1"
using assms by (simp add: dict_insert_entry_def Let_def)
lemma dict_insert_entry_data_stack_unchanged:
"data_stack (dict_insert_entry init_flags pinned_conflict vm) = data_stack vm"
"data_stack (dict_insert_entry name init_flags pinned_conflict vm) = data_stack vm"
by (simp add: dict_insert_entry_def set_error_def Let_def)
lemma dict_insert_entry_not_full_word_id_next_bound: True
@@ -382,27 +383,30 @@ lemma colon_guard_not_full_colon: True
here), vm_align+HERE capture, and the DF write of the threaded-body
start address (gap b). *)
definition forth_colon_entry_half :: "bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"forth_colon_entry_half pinned_conflict vm =
dict_insert_entry WORD_SMUDGED pinned_conflict (forth_colon_guard vm)"
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)"
lemma colon_entry_half_requires_guard_to_pass:
assumes "vm_mode vm \<noteq> ModeCompile" "\<not> pinned_conflict"
shows "\<exists>e. dictionary (forth_colon_entry_half pinned_conflict vm) (word_id_next (forth_colon_guard vm)) = Some e
\<and> de_flags e = WORD_SMUDGED"
shows "\<exists>e. dictionary (forth_colon_entry_half name pinned_conflict vm) (word_id_next (forth_colon_guard vm)) = Some e
\<and> de_name e = name \<and> de_flags e = WORD_SMUDGED"
using assms by (simp add: forth_colon_entry_half_def forth_colon_guard_def
dict_insert_entry_def Let_def)
lemma colon_entry_half_still_compile_mode:
assumes "vm_mode vm \<noteq> ModeCompile" "\<not> pinned_conflict"
shows "vm_mode (forth_colon_entry_half pinned_conflict vm) = ModeCompile"
shows "vm_mode (forth_colon_entry_half name pinned_conflict vm) = ModeCompile"
using assms by (simp add: forth_colon_entry_half_def forth_colon_guard_def
dict_insert_entry_def Let_def)
lemma colon_entry_half_not_full_colon: True
\<comment> \<open>Still NOT modelled: name parse, 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>
\<comment> \<open>Still NOT modelled: name parse (`name` is a caller-supplied parameter
here, not derived from `forth_parse_word` -- see forth_constant_full
below for the one word in this file where parse IS composed in),
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>
by simp
(* ── ; ( -- ) : compile-mode guard only ──────────────────────────────────── *)
@@ -442,55 +446,110 @@ lemma semicolon_guard_not_full_semicolon: True
`forth_<word>`, to keep the omission visible at the call site the way
`forth_colon_guard` already does for `:`. *)
definition forth_create_entry_half :: "bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"forth_create_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm"
definition forth_create_entry_half :: "string \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"forth_create_entry_half name pinned_conflict vm = dict_insert_entry name 0 pinned_conflict vm"
definition forth_variable_entry_half :: "bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"forth_variable_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm"
definition forth_variable_entry_half :: "string \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"forth_variable_entry_half name pinned_conflict vm = dict_insert_entry name 0 pinned_conflict vm"
definition forth_constant_entry_half :: "bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"forth_constant_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm"
definition forth_constant_entry_half :: "string \<Rightarrow> bool \<Rightarrow> vm_state \<Rightarrow> vm_state" where
"forth_constant_entry_half name pinned_conflict vm = dict_insert_entry name 0 pinned_conflict vm"
lemma create_entry_half_populates_dictionary:
assumes "\<not> pinned_conflict"
shows "\<exists>e. dictionary (forth_create_entry_half pinned_conflict vm) (word_id_next vm) = Some e
\<and> de_flags e = 0"
shows "\<exists>e. dictionary (forth_create_entry_half name pinned_conflict vm) (word_id_next vm) = Some e
\<and> de_name e = name \<and> de_flags e = 0"
using assms by (simp add: forth_create_entry_half_def dict_insert_entry_def Let_def)
lemma variable_entry_half_populates_dictionary:
assumes "\<not> pinned_conflict"
shows "\<exists>e. dictionary (forth_variable_entry_half pinned_conflict vm) (word_id_next vm) = Some e
\<and> de_flags e = 0"
shows "\<exists>e. dictionary (forth_variable_entry_half name pinned_conflict vm) (word_id_next vm) = Some e
\<and> de_name e = name \<and> de_flags e = 0"
using assms by (simp add: forth_variable_entry_half_def dict_insert_entry_def Let_def)
lemma constant_entry_half_populates_dictionary:
assumes "\<not> pinned_conflict"
shows "\<exists>e. dictionary (forth_constant_entry_half pinned_conflict vm) (word_id_next vm) = Some e
\<and> de_flags e = 0"
shows "\<exists>e. dictionary (forth_constant_entry_half name pinned_conflict vm) (word_id_next vm) = Some e
\<and> de_name e = name \<and> de_flags e = 0"
using assms by (simp add: forth_constant_entry_half_def dict_insert_entry_def Let_def)
lemma create_entry_half_pinned_conflict_errors:
assumes "pinned_conflict"
shows "vm_error (forth_create_entry_half pinned_conflict vm)"
shows "vm_error (forth_create_entry_half name pinned_conflict vm)"
using assms by (simp add: forth_create_entry_half_def dict_insert_entry_def set_error_def)
lemma create_entry_half_not_full_create: True
\<comment> \<open>Still NOT modelled beyond entry creation: name parse, vm_align+HERE
capture, and the DF write of the DFA (gap b). See section header.\<close>
\<comment> \<open>Still NOT modelled beyond entry creation: `name` here is a caller-
supplied parameter, not derived from `forth_parse_word` (see
forth_constant_full below for that composition); also vm_align+HERE
capture and the DF write of the DFA (gap b). See section header.\<close>
by simp
lemma variable_entry_half_not_full_variable: True
\<comment> \<open>Still NOT modelled beyond entry creation: name parse, vm_align+HERE
capture, vm_allot of one cell, and the DF write of that cell's
address (gap b). See section header.\<close>
\<comment> \<open>Still NOT modelled beyond entry creation: name parse (see note
above), vm_align+HERE capture, vm_allot of one cell, and the DF write
of that cell's address (gap b). See section header.\<close>
by simp
lemma constant_entry_half_not_full_constant: True
\<comment> \<open>Still NOT modelled beyond entry creation: name parse, the value pop
(this word's one real vm_state-only guard, `vm->dsp < 0`, is itself
also unmodelled here since it gates the parse that must happen
before vm_create_word), and the DF write of the popped value
(gap b). See section header.\<close>
\<comment> \<open>Still NOT modelled beyond entry creation: name parse (see note
above -- though see forth_constant_full below, which DOES compose
the parse and the value-pop guard together) and the DF write of the
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. *)
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>;
(nm, vm2) = forth_parse_word max_len vm1
in if nm = ''''
then set_error vm2
else dict_insert_entry nm 0 pinned_conflict vm2)"
lemma constant_full_underflow:
assumes "data_stack vm = []"
shows "vm_error (forth_constant_full max_len pinned_conflict vm)"
by (simp add: forth_constant_full_def set_error_def assms)
lemma constant_full_success_populates_dictionary:
assumes "data_stack vm \<noteq> []"
assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) \<noteq> []" (is "?s1 \<noteq> []")
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"
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
have input_pos_unaffected: "dropWhile is_ws (drop (input_pos ?vm1) (input_buffer ?vm1)) \<noteq> []"
using assms(2) by simp
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"
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"
using assms(4) by (simp add: dict_insert_entry_def Let_def)
ultimately show ?thesis using nm_nonempty by auto
qed
lemma create_runtime_not_modelled: True \<comment> \<open>defining_runtime_create: reads current_executing_entry's DF cell (gap b).\<close>
by simp
lemma variable_runtime_not_modelled: True \<comment> \<open>defining_runtime_variable: reads current_executing_entry's DF cell (gap b).\<close>