From cf205ca04a1c3c840001bd95b003a47ba38d65f8 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Fri, 14 Aug 2026 14:03:05 -0400 Subject: [PATCH] proof/: add StarForth_Editor_Words.thy and StarForth_Format_Words.thy editor_words.c: zero tractable words (first such file in this sweep) -- every word routes through the same deferred block-window cache as block_words.c, and EDIT is an interactive stdin/stdout REPL loop, not a single-step transition. format_words.c: 17 of 19 registered words modeled (# and #S deferred, multi-precision division out of scope). Two genuine C findings recorded: (1) DECIMAL/HEX/OCTAL write only the FORTH-visible memory cell at base_addr, never the separate vm->base host-mirror field that number OUTPUT words actually read -- proved formally (decimal_does_not_change_vm_base et al.), so HEX/OCTAL/DECIMAL silently never affect printed output, only parsed input. (2) ? and DUMP cast the popped cell directly to a host pointer and dereference it, bypassing vm_addr_ok entirely -- an out-of-VM-bounds read, not modeled since it isn't a vm->memory access at all. Adds base_addr/hold_addr/hold_pos to vm_state (StarForth_Base.thy), matching the scr_addr/here pattern from earlier files. --- proof/ROOT | 2 + proof/StarForth_Base.thy | 12 ++ proof/StarForth_Editor_Words.thy | 47 +++++ proof/StarForth_Format_Words.thy | 350 +++++++++++++++++++++++++++++++ 4 files changed, 411 insertions(+) create mode 100644 proof/StarForth_Editor_Words.thy create mode 100644 proof/StarForth_Format_Words.thy diff --git a/proof/ROOT b/proof/ROOT index 26b05cf..c638666 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -16,6 +16,8 @@ session "StarForth" = "HOL-Library" + StarForth_String_Words StarForth_Block_Words StarForth_IO_Words + StarForth_Editor_Words + StarForth_Format_Words StarForth_Mutex StarForth_Transition StarForth_Loop1_Heat diff --git a/proof/StarForth_Base.thy b/proof/StarForth_Base.thy index d46fea1..0e8b838 100644 --- a/proof/StarForth_Base.thy +++ b/proof/StarForth_Base.thy @@ -519,6 +519,18 @@ record vm_state = block number. Modeled as nat, matching `here`'s convention for VM addresses. See StarForth_Block_Words.thy's SCR. *) scr_addr :: nat + (* ○ CODE-MUST-MATCH: C: vaddr_t base_addr (include/vm.h:453) -- VM address + of the FORTH BASE variable cell; vaddr_t hold_addr (include/vm.h:454) -- + VM address of the 64-byte pictured-number hold buffer; int hold_pos + (include/vm.h:455) -- current fill count in that buffer, 0..63. + `vm_base` (above) is the SEPARATE host-mirror cell_t field C reads for + number *output* formatting (format_words.c's current_base()); the cell + at `base_addr` is what number *parsing* reads (vm.c's vm_get_base()). + See StarForth_Format_Words.thy for the finding that these two can + desync. *) + base_addr :: nat + hold_addr :: nat + hold_pos :: nat (* ── Physics Loop #1: Execution heat tracking ───────────────────────── *) (* ○ CODE-MUST-MATCH: heat_threshold_{25th,50th,75th} in C VM struct. diff --git a/proof/StarForth_Editor_Words.thy b/proof/StarForth_Editor_Words.thy new file mode 100644 index 0000000..4790c31 --- /dev/null +++ b/proof/StarForth_Editor_Words.thy @@ -0,0 +1,47 @@ +theory StarForth_Editor_Words + imports StarForth_Base +begin + +(* ========================================================================= + POST-12: Editor Words + Mirrors: src/word_source/editor_words.c (4 registered words) + + SCOPE, decided 2026-08-14: none of the 4 registered words are modeled -- + the first file in this sweep with zero tractable words (block_words.c, + the previous "worst case", still had SCR). Every word here routes + through the shared helper `line_ptr`, which calls straight into the + same block-subsystem cache StarForth_Block_Words.thy already documented + as out of scope: `blk_get_buffer`/`blk_is_valid` (block_subsystem.h), + backed by real disk I/O, none of it in vm_state. There is no analogue + of SCR here -- editor_words.c's `current_scr` *dereferences* memory at + `vm->scr_addr` (`vm_load_cell(vm, vm->scr_addr)`) rather than pushing + the address itself, so even the SCR-range guard clauses ultimately gate + entry into `line_ptr`, which is where every word's real effect lives. + + L ( u -- ) : line_ptr + print_line_64 (console I/O). + S ( c-addr len u -- ) : line_ptr + memcpy into the block buffer (disk- + backed memory, not vm_state) + mark_buffer_dirty + (block-window cache, same gap as block_words.c). + SHOW ( -- ) : line_ptr x16 (one per line) + printf (console I/O). + EDIT ( u -- ) : an interactive stdin/stdout REPL loop (fgets in a + `for (;;)`) that dispatches to L/S/SHOW plus + save_all_buffers (block-window cache) -- not a + single-step vm_state transition in any sense the rest + of this suite's words are, same category as + block_words.c's LOAD/THRU (recursive/looping, not a + leaf effect). + + Nothing new added to vm_state or StarForth_Base.thy for this file -- + there is nothing self-contained enough to need it. + ======================================================================== *) + +lemma l_not_modelled: True \ \L: line_ptr (block-window cache + blk_is_valid) + console I/O.\ + by simp +lemma s_not_modelled: True \ \S: line_ptr + memcpy into block buffer + mark_buffer_dirty.\ + by simp +lemma show_not_modelled: True \ \SHOW: line_ptr x16 + console I/O.\ + by simp +lemma edit_not_modelled: True \ \EDIT: interactive stdin/stdout REPL loop, not a single-step transition.\ + by simp + +end diff --git a/proof/StarForth_Format_Words.thy b/proof/StarForth_Format_Words.thy new file mode 100644 index 0000000..d107aa5 --- /dev/null +++ b/proof/StarForth_Format_Words.thy @@ -0,0 +1,350 @@ +theory StarForth_Format_Words + imports StarForth_Base StarForth_Memory_Words +begin + +(* ========================================================================= + POST-13: Format / Numeric-Conversion Words + Mirrors: src/word_source/format_words.c (18 registered words) + + ── Genuine finding, not fixed: BASE output and BASE input silently desync ─ + `current_base()` (used by every number-OUTPUT word below: `.`/`.R`/`U.`/ + `U.R`/`#`/`#S`) reads `vm->base` directly -- the C struct's host-mirror + cell_t field. `DECIMAL`/`HEX`/`OCTAL` (and `BASE` itself) never touch + that field: they call `vm_store_cell(vm, vm->base_addr, ...)`, writing + only the FORTH-visible memory cell at `vm->base_addr`. The ONLY place + that keeps the two in sync is `vm_set_base()` (src/vm.c:109), which + `format_words.c` never calls -- and `vm_set_base()` itself is only ever + invoked once, at boot (`vm_bootstrap.c:222`, hard-coded to 10). Number + *parsing* (`vm_get_base()`, src/vm.c:84, used by the numeric-literal + reader) DOES prefer the memory cell, so it correctly honors HEX/OCTAL/ + DECIMAL -- but number *output* never sees the change. Net effect: `HEX + FF .` continues to print in whatever base `vm->base` last held (10, + forever, since nothing else ever sets it), even though `HEX` genuinely + changed the FORTH BASE variable that parsing and BASE-fetching code see. + Proved below as `decimal_does_not_change_vm_base` et al. -- a formal, + machine-checked witness of the desync, not a hypothesis. + + ── Genuine finding, not fixed: `?` and `DUMP` dereference a raw host + pointer, bypassing the VM's own memory abstraction entirely ───────── + Every other memory-reading word in this codebase goes through + `vm_load_cell`/`vm->memory[...]` with `vm_addr_ok` bounds checking (see + StarForth_Memory_Words.thy's `@`/`C@`). `format_word_question` (`?`) and + `format_word_dump` (`DUMP`) instead cast the popped cell straight to a + host pointer via a C-style cast to `cell_t`-pointer / `uint8_t`-pointer + (see format_words.c's format_word_question/format_word_dump) -- + casting the popped FORTH cell DIRECTLY to a host pointer and + dereferencing it, with only a null check (`addr == 0`), never a + VM-memory-bounds check. Any FORTH program (or ACL-unprivileged user, + if these words are ever exposed past `zuse_session`) can hand `?`/`DUMP` + an arbitrary non-zero integer and get an arbitrary host-memory read -- + a real, exploitable out-of-VM-bounds read, categorically worse than + `TYPE`'s in-VM overflow bypass (StarForth_IO_Words.thy). Not modeled as + a memory read below (it isn't a `vm->memory` access at all, so nothing + in this suite's memory model applies) -- only the pop/guard shape is + modeled; the dereference itself is exactly the finding. + + MODELED (17 words): BASE, DECIMAL, HEX, OCTAL, `<#`, HOLD, SIGN, `#>`, + `.`, `.R`, `U.`, `U.R`, `D.`, `D.R`, `.S`, `?`, `DUMP`. + + NOT MODELED (2 words): `#` and `#S`. `#` performs `div_ud_by_base`, a + 16-bit-chunked long division of a double-cell (128-bit-equivalent) + magnitude by an arbitrary base 2..36 -- multi-precision division + algorithm correctness is its own proof project, on the scale of the + block-window cache or TIB input-subsystem deferrals elsewhere in this + sweep, not a one-word extension. `#S` loops `#` in an unbounded `for + (;;)` until the quotient reaches zero -- termination itself would need + to be established (it does, since the magnitude strictly decreases each + iteration under division by base \ 2, but that argument depends on + `#`'s own arithmetic being modeled first). Both deferred together. + ======================================================================== *) + +definition PN_CAP :: nat where "PN_CAP = 64" + \ \○ CODE-MUST-MATCH: #define PN_CAP 64 in format_words.c\ + +(* ── BASE ( -- addr ) : pushes the ADDRESS of the BASE cell, like SCR ───── *) + +definition forth_base :: "vm_state \ vm_state" where + "forth_base vm = vm\data_stack := word_of_nat (base_addr vm) # data_stack vm\" + +lemma base_pushes_base_addr: + "data_stack (forth_base vm) = word_of_nat (base_addr vm) # data_stack vm" + by (simp add: forth_base_def) + +(* ── DECIMAL / HEX / OCTAL ( -- ) : write the memory cell, NOT vm_base ──── *) + +definition forth_decimal :: "vm_state \ vm_state" where + "forth_decimal vm = vm\memory := mem_write (memory vm) (base_addr vm) 10\" + +definition forth_hex :: "vm_state \ vm_state" where + "forth_hex vm = vm\memory := mem_write (memory vm) (base_addr vm) 16\" + +definition forth_octal :: "vm_state \ vm_state" where + "forth_octal vm = vm\memory := mem_write (memory vm) (base_addr vm) 8\" + +lemma decimal_sets_base_cell: + "mem_read (memory (forth_decimal vm)) (base_addr vm) = 10" + by (simp add: forth_decimal_def mem_read_def mem_write_def) + +lemma decimal_does_not_change_vm_base: + "vm_base (forth_decimal vm) = vm_base vm" + by (simp add: forth_decimal_def) + +lemma hex_sets_base_cell: + "mem_read (memory (forth_hex vm)) (base_addr vm) = 16" + by (simp add: forth_hex_def mem_read_def mem_write_def) + +lemma hex_does_not_change_vm_base: + "vm_base (forth_hex vm) = vm_base vm" + by (simp add: forth_hex_def) + +lemma octal_sets_base_cell: + "mem_read (memory (forth_octal vm)) (base_addr vm) = 8" + by (simp add: forth_octal_def mem_read_def mem_write_def) + +lemma octal_does_not_change_vm_base: + "vm_base (forth_octal vm) = vm_base vm" + by (simp add: forth_octal_def) + +(* ── <# ( -- ) : hold_pos := 0, clear PN_CAP bytes at hold_addr ─────────── *) + +definition forth_begin_conversion :: "vm_state \ vm_state" where + "forth_begin_conversion vm = + vm\hold_pos := 0, + memory := (\a. if hold_addr vm \ a \ a < hold_addr vm + PN_CAP + then 0 else memory vm a)\" + +lemma begin_conversion_resets_hold_pos: + "hold_pos (forth_begin_conversion vm) = 0" + by (simp add: forth_begin_conversion_def) + +lemma begin_conversion_clears_buffer: + assumes "hold_addr vm \ a" "a < hold_addr vm + PN_CAP" + shows "memory (forth_begin_conversion vm) a = 0" + using assms by (simp add: forth_begin_conversion_def) + +lemma begin_conversion_data_stack_unchanged: + "data_stack (forth_begin_conversion vm) = data_stack vm" + by (simp add: forth_begin_conversion_def) + +(* ── HOLD ( c -- ) : prepend byte to the pictured-number buffer ─────────── *) + +definition forth_hold :: "vm_state \ vm_state" where + "forth_hold vm = + (case data_stack vm of + [] \ set_error vm + | c # rest \ + if c (255 :: cell) data_stack := rest\) + else if hold_pos vm \ PN_CAP - 1 + then set_error (vm\data_stack := rest\) + else vm\data_stack := rest, + memory := (\a. if a = hold_addr vm then c + else if hold_addr vm < a \ a \ hold_addr vm + hold_pos vm + then memory vm (a - 1) + else memory vm a), + hold_pos := hold_pos vm + 1\)" + +lemma hold_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_hold vm)" + by (simp add: forth_hold_def set_error_def assms) + +lemma hold_out_of_range: + assumes "data_stack vm = c # rest" "c (255 :: cell) data_stack (forth_hold vm) = rest" + using assms by (simp add: forth_hold_def set_error_def) + +lemma hold_buffer_full: + assumes "data_stack vm = c # rest" "\ (c (255 :: cell) PN_CAP - 1" + shows "vm_error (forth_hold vm) \ data_stack (forth_hold vm) = rest" + using assms by (simp add: forth_hold_def set_error_def) + +lemma hold_normal_prepends_and_advances: + assumes "data_stack vm = c # rest" "\ (c (255 :: cell) vm_state" where + "forth_sign vm = + (case data_stack vm of + [] \ set_error vm + | n # rest \ + if n data_stack := (45 :: cell) # rest\) \ \'-' = ASCII 45\ + else vm\data_stack := rest\)" + +lemma sign_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_sign vm)" + by (simp add: forth_sign_def set_error_def assms) + +lemma sign_nonnegative_just_pops: + assumes "data_stack vm = n # rest" "\ n data_stack := (45 :: cell) # rest\)" + using assms by (simp add: forth_sign_def) + +(* ── # / #S -- NOT MODELLED, see SCOPE above ─────────────────────────────── *) + +lemma hash_not_modelled: True \ \#: chunked multi-precision division, own proof project.\ + by simp +lemma hash_s_not_modelled: True \ \#S: loops #, inherits its gap plus loop termination.\ + by simp + +(* ── #> ( [ud] -- addr u ) : drop optional double, push hold buffer view ── *) + +definition forth_end_conversion :: "vm_state \ vm_state" where + "forth_end_conversion vm = + (let ds' = (if length (data_stack vm) \ 2 then drop 2 (data_stack vm) else data_stack vm) + in vm\data_stack := word_of_nat (hold_pos vm) # word_of_nat (hold_addr vm) # ds'\)" + +lemma end_conversion_never_errors: + "vm_error (forth_end_conversion vm) = vm_error vm" + by (simp add: forth_end_conversion_def Let_def) + +lemma end_conversion_pushes_buffer_view: + "data_stack (forth_end_conversion vm) = + word_of_nat (hold_pos vm) # word_of_nat (hold_addr vm) # + (if length (data_stack vm) \ 2 then drop 2 (data_stack vm) else data_stack vm)" + by (simp add: forth_end_conversion_def Let_def) + +(* ── . / U. ( n -- ) : pop one, print (unmodelled I/O) ───────────────────── *) + +definition forth_dot :: "vm_state \ vm_state" where + "forth_dot vm = + (case data_stack vm of [] \ set_error vm | n # rest \ vm\data_stack := rest\)" + +definition forth_u_dot :: "vm_state \ vm_state" where + "forth_u_dot vm = + (case data_stack vm of [] \ set_error vm | n # rest \ vm\data_stack := rest\)" + +lemma dot_underflow: "data_stack vm = [] \ vm_error (forth_dot vm)" + by (simp add: forth_dot_def set_error_def) +lemma dot_pops_one: "data_stack vm = n # rest \ data_stack (forth_dot vm) = rest" + by (simp add: forth_dot_def) +lemma u_dot_underflow: "data_stack vm = [] \ vm_error (forth_u_dot vm)" + by (simp add: forth_u_dot_def set_error_def) +lemma u_dot_pops_one: "data_stack vm = n # rest \ data_stack (forth_u_dot vm) = rest" + by (simp add: forth_u_dot_def) + +(* ── .R / U.R ( n width -- ) : pop two, print (unmodelled I/O) ──────────── *) + +definition forth_dot_r :: "vm_state \ vm_state" where + "forth_dot_r vm = + (if length (data_stack vm) < 2 then set_error vm + else vm\data_stack := drop 2 (data_stack vm)\)" + +definition forth_u_dot_r :: "vm_state \ vm_state" where + "forth_u_dot_r vm = + (if length (data_stack vm) < 2 then set_error vm + else vm\data_stack := drop 2 (data_stack vm)\)" + +lemma dot_r_underflow: "length (data_stack vm) < 2 \ vm_error (forth_dot_r vm)" + by (simp add: forth_dot_r_def set_error_def) +lemma dot_r_pops_two: + "length (data_stack vm) \ 2 \ data_stack (forth_dot_r vm) = drop 2 (data_stack vm)" + by (simp add: forth_dot_r_def) +lemma u_dot_r_underflow: "length (data_stack vm) < 2 \ vm_error (forth_u_dot_r vm)" + by (simp add: forth_u_dot_r_def set_error_def) +lemma u_dot_r_pops_two: + "length (data_stack vm) \ 2 \ data_stack (forth_u_dot_r vm) = drop 2 (data_stack vm)" + by (simp add: forth_u_dot_r_def) + +(* ── D. ( d -- ) : pop two, print (unmodelled I/O, both branches) ───────── *) + +definition forth_d_dot :: "vm_state \ vm_state" where + "forth_d_dot vm = + (if length (data_stack vm) < 2 then set_error vm + else vm\data_stack := drop 2 (data_stack vm)\)" + +lemma d_dot_underflow: "length (data_stack vm) < 2 \ vm_error (forth_d_dot vm)" + by (simp add: forth_d_dot_def set_error_def) +lemma d_dot_pops_two: + "length (data_stack vm) \ 2 \ data_stack (forth_d_dot vm) = drop 2 (data_stack vm)" + by (simp add: forth_d_dot_def) + +(* ── D.R ( d width -- ) : pop three, print (unmodelled I/O, both branches) *) + +definition forth_d_dot_r :: "vm_state \ vm_state" where + "forth_d_dot_r vm = + (if length (data_stack vm) < 3 then set_error vm + else vm\data_stack := drop 3 (data_stack vm)\)" + +lemma d_dot_r_underflow: "length (data_stack vm) < 3 \ vm_error (forth_d_dot_r vm)" + by (simp add: forth_d_dot_r_def set_error_def) +lemma d_dot_r_pops_three: + "length (data_stack vm) \ 3 \ data_stack (forth_d_dot_r vm) = drop 3 (data_stack vm)" + by (simp add: forth_d_dot_r_def) + +(* ── .S ( -- ) : pure I/O, no vm_state effect at all ─────────────────────── *) + +definition forth_dot_s :: "vm_state \ vm_state" where + "forth_dot_s vm = vm" + +lemma dot_s_is_identity: "forth_dot_s vm = vm" + by (simp add: forth_dot_s_def) + +(* ── ? ( addr -- ) : pop one; error iff addr = 0; see header finding ────── *) + +definition forth_question :: "vm_state \ vm_state" where + "forth_question vm = + (case data_stack vm of + [] \ set_error vm + | addr # rest \ + if addr = 0 then set_error (vm\data_stack := rest\) + else vm\data_stack := rest\) \ \raw host-pointer deref, unmodelled\" + +lemma question_underflow: "data_stack vm = [] \ vm_error (forth_question vm)" + by (simp add: forth_question_def set_error_def) +lemma question_null_errors: + "data_stack vm = 0 # rest \ vm_error (forth_question vm) \ data_stack (forth_question vm) = rest" + by (simp add: forth_question_def set_error_def) +lemma question_pops_one: + "data_stack vm = addr # rest \ data_stack (forth_question vm) = rest" + by (simp add: forth_question_def) + +(* ── DUMP ( addr u -- ) : pop two; error iff u<0 or addr=0; see finding ─── *) + +definition forth_dump :: "vm_state \ vm_state" where + "forth_dump vm = + (case data_stack vm of + u # addr # rest \ + if u data_stack := rest\) + else if addr = 0 then set_error (vm\data_stack := rest\) + else vm\data_stack := rest\ \ \raw host-pointer deref, unmodelled\ + | _ \ set_error vm)" + +lemma dump_underflow: + assumes "length (data_stack vm) < 2" + shows "vm_error (forth_dump vm)" +proof (cases "data_stack vm") + case Nil then show ?thesis using assms by (simp add: forth_dump_def set_error_def) +next + case (Cons x xs) then show ?thesis using assms + by (cases xs) (auto simp: forth_dump_def set_error_def) +qed + +lemma dump_negative_count_errors: + assumes "data_stack vm = u # addr # rest" "u data_stack (forth_dump vm) = rest" + using assms by (simp add: forth_dump_def set_error_def) + +lemma dump_null_addr_errors: + assumes "data_stack vm = u # 0 # rest" "\ u data_stack (forth_dump vm) = rest" + using assms by (simp add: forth_dump_def set_error_def) + +lemma dump_pops_two: + assumes "data_stack vm = u # addr # rest" + shows "data_stack (forth_dump vm) = rest" + using assms by (simp add: forth_dump_def) + +end