From 1aca77d55ccfc7e09a2b973fdb9bdda0630b560f Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Fri, 14 Aug 2026 22:53:11 -0400 Subject: [PATCH] proof/: model the TIB name-parse primitive, close it into CONSTANT's full model 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 --- proof/COVERAGE.md | 28 ++++-- proof/StarForth_Base.thy | 102 ++++++++++++++++++++ proof/StarForth_Defer_Words.thy | 10 +- proof/StarForth_Defining_Words.thy | 143 ++++++++++++++++++++--------- 4 files changed, 229 insertions(+), 54 deletions(-) diff --git a/proof/COVERAGE.md b/proof/COVERAGE.md index a9df1e6..4f5f381 100644 --- a/proof/COVERAGE.md +++ b/proof/COVERAGE.md @@ -95,8 +95,20 @@ 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** — blocks the `(`/`\` comment - words, `KEY`, `."`, `ABORT"`'s compile-time half, `SEE`. +- **The TIB / interactive input subsystem — partially closed 2026-08-14.** + `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 with + `dict_insert_entry` for CONSTANT in `StarForth_Defining_Words.thy` as a + worked example. 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) — @@ -106,11 +118,13 @@ effort on the scale of what's already here: CONSTANT, DEFER) — **partially closed 2026-08-14.** `dict_insert_entry` (`StarForth_Defining_Words.thy`) now models the word_id-assignment/ dictionary-table/`latest_id`/`word_id_next`-counter portion, reused by - all five words' `forth_*_entry_half` definitions. Still not modelled: - the name parse (TIB gap, same as everywhere else in this suite), - `vm->compiling_word` tracking (no vm_state field), the data-field (DF) - write each of the five words does afterward (still gap (b) below), and - the pin-shadow name-scan guard (sidestepped via an explicit + all five words' `forth_*_entry_half` definitions, which take the parsed + name as a caller-supplied parameter. `forth_constant_full` composes + `forth_parse_word` (the TIB gap above) in directly for CONSTANT, as a + worked example not yet repeated for the other four. Still not modelled + for any of the five: `vm->compiling_word` tracking (no vm_state field), + the data-field (DF) write each word does afterward (still gap (b) + below), and the pin-shadow name-scan guard (sidestepped via an explicit `pinned_conflict :: bool` parameter, same technique as the XT-pop gap elsewhere in this suite). - **The vocabulary chain mechanics** (VOCABULARY/DEFINITIONS/CONTEXT/CURRENT/ diff --git a/proof/StarForth_Base.thy b/proof/StarForth_Base.thy index 28b401d..5a88792 100644 --- a/proof/StarForth_Base.thy +++ b/proof/StarForth_Base.thy @@ -541,6 +541,27 @@ record vm_state = for the correction). *) state_addr :: nat + (* ── Input system (TIB), added 2026-08-14 ───────────────────────────── + ○ CODE-MUST-MATCH: C: char input_buffer[INPUT_BUFFER_SIZE] (=1025), + size_t input_length, size_t input_pos (include/vm.h:415-417). This is + the REAL, live interpreter input buffer -- vm_interpret's dispatch + path for both interactive REPL lines and LOAD'd block content (see + .claude/CLAUDE.md's INPUT_BUFFER_SIZE note) -- distinct from the + separate `tib_buf`/`tib_cap`/`in_var`/`span_var` fields (vm.h:444-448, + the C's own comment marks them "legacy; will migrate to VM addr") and + from `hold_addr`/`hold_pos` above (the pictured-number OUTPUT buffer, + unrelated). Modelled as `input_buffer :: string` holding exactly the + meaningful prefix (not the full fixed 1025-byte physical array, which + has no abstract counterpart -- content past `input_length` in the + real C is stale/undefined and never read), with `input_length` kept + as a separate field even though it always equals `length input_buffer` + here, to mirror the real C's two-field structure precisely. `input_pos` + is FORTH's `>IN` (parse position), advanced by `vm_parse_word` + (src/vm.c:137-160, modelled below as `forth_parse_word`). *) + input_buffer :: string + input_length :: nat + input_pos :: nat + (* ── Physics Loop #1: Execution heat tracking ───────────────────────── *) (* ○ CODE-MUST-MATCH: heat_threshold_{25th,50th,75th} in C VM struct. ⚠ HUMAN-REVIEW: Thresholds are recomputed periodically by the heat bucket @@ -634,6 +655,87 @@ record vm_state = return_stack, memory), never on physics state. *) consts word_table :: "nat \ vm_state \ vm_state" +(* ========================================================================= + Section 4b: TIB parsing (added 2026-08-14) + + Closes, for the first time in this suite, the "name parse" dependency + named as an unmodelled precondition by nearly every name-consuming word + swept so far (CREATE/VARIABLE/CONSTANT/`:`/DEFER/IS/DEFER@/COMPILE/ + [COMPILE]/FIND/WORD and others -- see StarForth_Defining_Words.thy's + file header, StarForth_Defer_Words.thy, etc.). `vm_parse_word` + (src/vm.c:137-160) turns out to be a pure scan over the input_buffer/ + input_length/input_pos fields added above -- no host pointers, no C- + string tricks, unlike almost everything else this suite has deferred. + Individual per-word applications (composing this with e.g. + `dict_insert_entry`) are done in the files that use them, not here -- + this section is only the shared parsing primitive. + ======================================================================== *) + +definition is_ws :: "char \ bool" where + "is_ws c \ c = CHR '' '' \ c = char_of (9::nat) \ c = char_of (10::nat) \ c = char_of (13::nat)" + \ \space, tab, LF, CR -- matches vm_parse_word's `c==' '||c=='\t'||c=='\n'||c=='\r'` exactly\ + +(* C: `vm_parse_word` skips leading whitespace in input_buffer[input_pos.. + input_length), then copies the following run of non-whitespace + (truncated to max_len-1 chars) into the caller's buffer, advancing + input_pos by exactly what was skipped plus what was copied (NOT past + any untruncated remainder of a token longer than max_len-1 -- the C + loop's own `len < max_len - 1` condition stops consuming input_pos at + the same point it stops writing `word`). Returns the parsed token + (empty string signals the C's `return 0`, matching every caller's + `nlen <= 0` failure check) and the updated vm_state. *) +definition forth_parse_word :: "nat \ vm_state \ (string \ vm_state)" where + "forth_parse_word max_len vm = + (let s = drop (input_pos vm) (input_buffer vm); + s1 = dropWhile is_ws s; + skipped = length s - length s1; + pos_ws = input_pos vm + skipped + in if s1 = [] + then ('''', vm\input_pos := pos_ws\) + else + let tok = take (max_len - 1) (takeWhile (\c. \ is_ws c) s1) + in (tok, vm\input_pos := pos_ws + length tok\))" + +lemma forth_parse_word_all_whitespace_yields_empty: + assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) = []" + shows "fst (forth_parse_word max_len vm) = ''''" + using assms by (simp add: forth_parse_word_def Let_def) + +lemma forth_parse_word_success_nonempty: + assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) \ []" + assumes "max_len \ 2" + shows "fst (forth_parse_word max_len vm) \ ''''" +proof - + let ?s1 = "dropWhile is_ws (drop (input_pos vm) (input_buffer vm))" + from assms(1) obtain c cs where s1_eq: "?s1 = c # cs" by (cases ?s1) auto + have "\ is_ws c" using dropWhile_eq_Cons_conv[of is_ws "drop (input_pos vm) (input_buffer vm)" c cs] + using s1_eq by auto + hence "takeWhile (\x. \ is_ws x) ?s1 = c # takeWhile (\x. \ is_ws x) cs" + by (simp add: s1_eq) + hence "take (max_len - 1) (takeWhile (\x. \ is_ws x) ?s1) \ []" + using assms(2) by simp + thus ?thesis + using assms(1) by (simp add: forth_parse_word_def Let_def) +qed + +lemma forth_parse_word_input_pos_monotone: + "input_pos vm \ input_pos (snd (forth_parse_word max_len vm))" + by (simp add: forth_parse_word_def Let_def) + +lemma forth_parse_word_preserves_buffer: + "input_buffer (snd (forth_parse_word max_len vm)) = input_buffer vm" + by (simp add: forth_parse_word_def Let_def) + +lemma forth_parse_word_preserves_data_stack: + "data_stack (snd (forth_parse_word max_len vm)) = data_stack vm" + by (simp add: forth_parse_word_def Let_def) + +lemma forth_parse_word_never_sets_error: True + \ \vm_parse_word's own C body never touches vm->error -- callers check + the returned length themselves and set it. Faithfully NOT set here + either.\ + by simp + (* ========================================================================= Section 5: Well-formedness, error signalling, capacity predicates ======================================================================== *) diff --git a/proof/StarForth_Defer_Words.thy b/proof/StarForth_Defer_Words.thy index dcaac88..094dd16 100644 --- a/proof/StarForth_Defer_Words.thy +++ b/proof/StarForth_Defer_Words.thy @@ -73,18 +73,18 @@ lemma is_guard_rest_not_modelled: True VARIABLE/CONSTANT, reusing `dict_insert_entry 0` directly. NOT modelled: the name parse (TIB gap), and the DF zero-init that follows (gap b). *) -definition forth_defer_entry_half :: "bool \ vm_state \ vm_state" where - "forth_defer_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm" +definition forth_defer_entry_half :: "string \ bool \ vm_state \ vm_state" where + "forth_defer_entry_half name pinned_conflict vm = dict_insert_entry name 0 pinned_conflict vm" lemma defer_entry_half_populates_dictionary: assumes "\ pinned_conflict" - shows "\e. dictionary (forth_defer_entry_half pinned_conflict vm) (word_id_next vm) = Some e - \ de_flags e = 0" + shows "\e. dictionary (forth_defer_entry_half name pinned_conflict vm) (word_id_next vm) = Some e + \ de_name e = name \ de_flags e = 0" using assms by (simp add: forth_defer_entry_half_def dict_insert_entry_def Let_def) lemma defer_entry_half_pinned_conflict_errors: assumes "pinned_conflict" - shows "vm_error (forth_defer_entry_half pinned_conflict vm)" + shows "vm_error (forth_defer_entry_half name pinned_conflict vm)" using assms by (simp add: forth_defer_entry_half_def dict_insert_entry_def set_error_def) lemma defer_not_modelled: True \ \DEFER beyond the entry-creation half: name parse (TIB gap) + DF zero-init (gap b). See forth_defer_entry_half above for what IS now modelled.\ diff --git a/proof/StarForth_Defining_Words.thy b/proof/StarForth_Defining_Words.thy index 11ebedd..b38b6cd 100644 --- a/proof/StarForth_Defining_Words.thy +++ b/proof/StarForth_Defining_Words.thy @@ -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 \ bool \ vm_state \ vm_state" where - "dict_insert_entry init_flags pinned_conflict vm = +definition dict_insert_entry :: "string \ nat \ bool \ vm_state \ 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 = \de_name = '''', de_flags = init_flags, de_heat = 0, + e = \de_name = name, de_flags = init_flags, de_heat = 0, de_word_id = wid, de_physics = \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 \ bool \ 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 "\ 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 "\ pinned_conflict" - shows "\e. dictionary (dict_insert_entry init_flags pinned_conflict vm) (word_id_next vm) = Some e - \ de_word_id e = word_id_next vm \ de_flags e = init_flags \ de_heat e = 0 - \ de_acl_ttl e = 0 \ de_acl_allow e \ de_acl_mode e = ACL_MODE_TTL \ \ de_acl_pinned e" + shows "\e. dictionary (dict_insert_entry name init_flags pinned_conflict vm) (word_id_next vm) = Some e + \ de_word_id e = word_id_next vm \ de_name e = name \ de_flags e = init_flags + \ de_heat e = 0 \ de_acl_ttl e = 0 \ de_acl_allow e \ de_acl_mode e = ACL_MODE_TTL + \ \ de_acl_pinned e" using assms by (simp add: dict_insert_entry_def Let_def) lemma dict_insert_entry_advances_counter: assumes "\ 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 \ vm_state \ 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 \ bool \ vm_state \ 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 \ ModeCompile" "\ pinned_conflict" - shows "\e. dictionary (forth_colon_entry_half pinned_conflict vm) (word_id_next (forth_colon_guard vm)) = Some e - \ de_flags e = WORD_SMUDGED" + shows "\e. dictionary (forth_colon_entry_half name pinned_conflict vm) (word_id_next (forth_colon_guard vm)) = Some e + \ de_name e = name \ 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 \ ModeCompile" "\ 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 - \ \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.\ + \ \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.\ by simp (* ── ; ( -- ) : compile-mode guard only ──────────────────────────────────── *) @@ -442,55 +446,110 @@ lemma semicolon_guard_not_full_semicolon: True `forth_`, to keep the omission visible at the call site the way `forth_colon_guard` already does for `:`. *) -definition forth_create_entry_half :: "bool \ vm_state \ vm_state" where - "forth_create_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm" +definition forth_create_entry_half :: "string \ bool \ vm_state \ 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 \ vm_state \ vm_state" where - "forth_variable_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm" +definition forth_variable_entry_half :: "string \ bool \ vm_state \ 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 \ vm_state \ vm_state" where - "forth_constant_entry_half pinned_conflict vm = dict_insert_entry 0 pinned_conflict vm" +definition forth_constant_entry_half :: "string \ bool \ vm_state \ 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 "\ pinned_conflict" - shows "\e. dictionary (forth_create_entry_half pinned_conflict vm) (word_id_next vm) = Some e - \ de_flags e = 0" + shows "\e. dictionary (forth_create_entry_half name pinned_conflict vm) (word_id_next vm) = Some e + \ de_name e = name \ 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 "\ pinned_conflict" - shows "\e. dictionary (forth_variable_entry_half pinned_conflict vm) (word_id_next vm) = Some e - \ de_flags e = 0" + shows "\e. dictionary (forth_variable_entry_half name pinned_conflict vm) (word_id_next vm) = Some e + \ de_name e = name \ 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 "\ pinned_conflict" - shows "\e. dictionary (forth_constant_entry_half pinned_conflict vm) (word_id_next vm) = Some e - \ de_flags e = 0" + shows "\e. dictionary (forth_constant_entry_half name pinned_conflict vm) (word_id_next vm) = Some e + \ de_name e = name \ 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 - \ \Still NOT modelled beyond entry creation: name parse, vm_align+HERE - capture, and the DF write of the DFA (gap b). See section header.\ + \ \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.\ by simp lemma variable_entry_half_not_full_variable: True - \ \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.\ + \ \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.\ by simp lemma constant_entry_half_not_full_constant: True - \ \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.\ + \ \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.\ 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 \ bool \ vm_state \ vm_state" where + "forth_constant_full max_len pinned_conflict vm = + (if data_stack vm = [] + then set_error vm + else + let vm1 = vm\data_stack := tl (data_stack vm)\; + (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 \ []" + assumes "dropWhile is_ws (drop (input_pos vm) (input_buffer vm)) \ []" (is "?s1 \ []") + assumes "max_len \ 2" + assumes "\ pinned_conflict" + shows "\e wid. dictionary (forth_constant_full max_len pinned_conflict vm) wid = Some e + \ de_name e \ '''' \ de_flags e = 0" +proof - + let ?vm1 = "vm\data_stack := tl (data_stack vm)\" + 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)) \ []" + using assms(2) by simp + hence nm_nonempty: "nm \ ''''" + 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 "\e. dictionary (dict_insert_entry nm 0 pinned_conflict vm2) (word_id_next vm2) = Some e + \ de_name e = nm \ 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 \ \defining_runtime_create: reads current_executing_entry's DF cell (gap b).\ by simp lemma variable_runtime_not_modelled: True \ \defining_runtime_variable: reads current_executing_entry's DF cell (gap b).\