From d59a913e13aefe5e9731d7a0c89744cda514bf9b Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Sat, 15 Aug 2026 05:40:02 -0400 Subject: [PATCH] proof/: close the data-field (DF) gap for CREATE/VARIABLE/CONSTANT 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 --- proof/COVERAGE.md | 40 +++--- proof/StarForth_Base.thy | 20 +++ proof/StarForth_Defining_Words.thy | 203 +++++++++++++++++++++-------- 3 files changed, 195 insertions(+), 68 deletions(-) diff --git a/proof/COVERAGE.md b/proof/COVERAGE.md index 93d0f29..e8ebcc0 100644 --- a/proof/COVERAGE.md +++ b/proof/COVERAGE.md @@ -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` | 4/19 full + `;` guard-only + `:`/CREATE/VARIABLE/CONSTANT full up to the DF write (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 + `:` full except `compiling_word` tracking (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,20 +116,30 @@ 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) — **partially closed 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. All five - words now have a `forth_*_full` definition composing the real parse, - any word-specific guard (CONSTANT's stack-underflow check, `:`'s - nested-definition check), any align/allot step (CREATE's `vm_align`, - VARIABLE's `vm_align` + a new `forth_vm_allot_raw` modelling the raw - `vm_allot` C helper), and the entry insertion itself, all the way up - to — but not including — the data-field write. 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). + CONSTANT, DEFER) — **closed end-to-end for CREATE/VARIABLE/CONSTANT, + 2026-08-14/15**, `:`/DEFER closed up to `vm->compiling_word` tracking. + `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`) + and `dict_write_df` close the data-field (DF) write gap (b) for every + word that treats DF as a plain value. Each of the five words' `forth_ + *_full` definition now composes the real parse, any word-specific guard + (CONSTANT's stack-underflow check, `:`'s nested-definition check), any + align/allot step (CREATE's `vm_align`; VARIABLE's `vm_align` + + `forth_vm_allot_raw`, modelling the raw `vm_allot` C helper distinctly + from the FORTH word ALLOT), the entry insertion, AND the DF write — + CREATE/VARIABLE/CONSTANT are now fully modelled words, the first three + in this entire file. Their runtime companions (`defining_runtime_ + 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). - **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/ diff --git a/proof/StarForth_Base.thy b/proof/StarForth_Base.thy index 838ad09..9089921 100644 --- a/proof/StarForth_Base.thy +++ b/proof/StarForth_Base.thy @@ -300,6 +300,19 @@ record dict_entry = de_acl_allow :: bool \ \acl_allow: cached decision (True=allow, False=deny)\ de_acl_mode :: nat \ \acl_mode: 0=TTL, 1=STRICT\ de_acl_pinned :: bool \ \acl_pinned: one-way ratchet; True = immutable\ + (* ○ CODE-MUST-MATCH, added 2026-08-15: the entry's data-field (DF) cell + -- the storage C's `vm_dictionary_get_data_field(entry)` returns a + pointer into (a single cell_t immediately following the entry's name + in the arena, per vm_create_word's layout, dictionary_management.c: + 406-410). Modelled here as a plain VALUE (`cell`), not an address -- + this closes gap (b) for every word that only ever reads/writes the DF + as a value through its OWNING entry (CREATE/VARIABLE/CONSTANT/DEFER + and their runtimes). It does NOT close >BODY/>NAME-style words in + StarForth_Dictionary_Manipulation_Words.thy, which need the DF's + ADDRESS (so a later, unrelated `@`/`!` could target it generically) + -- this model has no notion of a dict_entry's own address, only its + word_id, so that remains a distinct, still-open gap. *) + de_df :: cell (* ── Word transition metrics ─────────────────────────────────────────────── *) (* ○ CODE-MUST-MATCH: struct WordTransitionMetrics in include/physics_pipelining_metrics.h @@ -501,6 +514,13 @@ record vm_state = dict_fence :: "nat option" \ \FENCE word_id for FORGET\ dict_lock :: lock_state word_id_next :: nat + (* ○ CODE-MUST-MATCH, added 2026-08-15: C `DictEntry* vm-> + current_executing_entry` (include/vm.h:434) -- the entry currently + executing, read by runtime helpers like `defining_runtime_create`/ + `_variable`/`_constant` via `vm->current_executing_entry` rather than + a fresh lookup. Modelled word-id-indexed (`nat option`), matching + `latest_id`'s convention, rather than as a raw pointer. *) + current_executing_word_id :: "nat option" (* ── Execution state ──────────────────────────────────────────────────── *) vm_mode :: vm_mode diff --git a/proof/StarForth_Defining_Words.thy b/proof/StarForth_Defining_Words.thy index 2b66f9d..e686843 100644 --- a/proof/StarForth_Defining_Words.thy +++ b/proof/StarForth_Defining_Words.thy @@ -151,7 +151,7 @@ definition dict_insert_entry :: "string \ nat \ bool \, de_acl_ttl = 0, de_acl_allow = True, de_acl_mode = ACL_MODE_TTL, - de_acl_pinned = False\ + de_acl_pinned = False, de_df = 0\ in vm\dictionary := (dictionary vm)(wid := Some e), latest_id := Some wid, word_id_next := wid + 1\)" @@ -171,7 +171,7 @@ lemma dict_insert_entry_populates_dictionary: 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" + \ \ de_acl_pinned e \ 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.\ 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 \ cell \ vm_state \ vm_state" where + "dict_write_df wid v vm = + (case dictionary vm wid of + None \ vm + | Some e \ vm\dictionary := (dictionary vm)(wid := Some (e\de_df := v\))\)" + +lemma dict_write_df_present: + assumes "dictionary vm wid = Some e" + shows "dictionary (dict_write_df wid v vm) wid = Some (e\de_df := v\)" + 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.\ 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 \ 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)\; + let value = hd (data_stack vm); + 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)" + 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 \ 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" + \ de_name e \ '''' \ de_flags e = 0 \ de_df e = hd (data_stack vm)" 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 @@ -598,26 +623,31 @@ proof - 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" + 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 "\e. dictionary (dict_insert_entry nm 0 pinned_conflict vm2) (word_id_next vm2) = Some e - \ de_name e = nm \ de_flags e = 0" + have "\e. dictionary ?vm3 ?wid = 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 + 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\de_df := hd (data_stack vm)\)" + 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 \ bool \ vm_state \ vm_state" where @@ -625,7 +655,10 @@ definition forth_create_full :: "nat \ bool \ 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 \ ''''" 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 "\e. dictionary (dict_insert_entry nm 0 pinned_conflict vm1) (word_id_next vm1) = Some e - \ de_name e = nm \ 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 "\e. dictionary (dict_insert_entry nm 0 pinned_conflict vm1) ?wid = Some e + \ de_name e = nm \ 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\de_df := word_of_nat (here ?vm2)\)" + 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 \ bool \ vm_state \ 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 \ ''''" 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 "\e. dictionary (dict_insert_entry nm 0 pinned_conflict ?vm3) (word_id_next ?vm3) = Some e - \ de_name e = nm \ 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 "\e. dictionary (dict_insert_entry nm 0 pinned_conflict ?vm3) ?wid = Some e + \ de_name e = nm \ 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\de_df := word_of_nat (here (forth_align vm1))\)" + 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 \ \defining_runtime_create: reads current_executing_entry's DF cell (gap b).\ +(* ── 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 \ vm_state" where + "forth_runtime_read_df vm = + (case current_executing_word_id vm of + None \ set_error vm + | Some wid \ + (case dictionary vm wid of + None \ set_error vm + | Some e \ + if ds_full vm + then set_error vm + else vm\data_stack := de_df e # data_stack vm\))" + +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 "\ 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 \ \defining_runtime_create IS forth_runtime_read_df -- see definition above.\ by simp -lemma variable_runtime_not_modelled: True \ \defining_runtime_variable: reads current_executing_entry's DF cell (gap b).\ +lemma variable_runtime_is_read_df: True \ \defining_runtime_variable IS forth_runtime_read_df -- see definition above.\ by simp -lemma constant_runtime_not_modelled: True \ \defining_runtime_constant: reads current_executing_entry's DF cell (gap b).\ +lemma constant_runtime_is_read_df: True \ \defining_runtime_constant IS forth_runtime_read_df -- see definition above.\ by simp lemma lit_not_modelled: True \ \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.\ by simp