From 16435a42298233efec773781eb858ef4a9c7f8c2 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Fri, 14 Aug 2026 13:55:09 -0400 Subject: [PATCH] proof/: add StarForth_IO_Words.thy (io_words.c coverage) 7 of 9 registered words modeled (EMIT/CR/?TERMINAL/TYPE/SPACE/SPACES/ (do-string)); KEY and ." deferred (real external input / TIB-adjacent input-buffer dependency, same categories as earlier deferrals in this sweep). Two genuine C findings recorded: ?TERMINAL is a permanent stub always returning false, and TYPE's bounds check has a signed-integer- overflow bypass (addr+count wraps negative for large addr/count, defeating the VM_MEMORY_SIZE guard) with a machine-checked witness. --- proof/ROOT | 1 + proof/StarForth_IO_Words.thy | 237 +++++++++++++++++++++++++++++++++++ 2 files changed, 238 insertions(+) create mode 100644 proof/StarForth_IO_Words.thy diff --git a/proof/ROOT b/proof/ROOT index 1367c27..26b05cf 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -15,6 +15,7 @@ session "StarForth" = "HOL-Library" + StarForth_Control_Words StarForth_String_Words StarForth_Block_Words + StarForth_IO_Words StarForth_Mutex StarForth_Transition StarForth_Loop1_Heat diff --git a/proof/StarForth_IO_Words.thy b/proof/StarForth_IO_Words.thy new file mode 100644 index 0000000..5629adc --- /dev/null +++ b/proof/StarForth_IO_Words.thy @@ -0,0 +1,237 @@ +theory StarForth_IO_Words + imports StarForth_Base StarForth_Dictionary_Words +begin + +(* ========================================================================= + POST-11: I/O & Terminal Words + Mirrors: src/word_source/io_words.c (9 registered words) + + SCOPE, decided 2026-08-14: unlike block_words.c (the previous file), + this one turned out NOT to need a near-total deferral -- worth recording + since the previous resume-point note predicted "expect this to look + like block_words.c" and that prediction was itself worth re-checking, + not trusting (same discipline as the stale-blocker lesson from earlier + in this sweep). Every word here has a real console I/O side effect + (putchar/getchar/fflush), which is never modeled anywhere in this + suite -- but MOST of them also have a fully deterministic, precisely + specifiable effect on data_stack/return_stack/memory independent of + that I/O, and that part is what gets modeled below, with the I/O + itself simply noted as an unmodelled side channel each time. + + MODELED (7 words): EMIT, CR, ?TERMINAL, TYPE, SPACE, SPACES, + (do-string). + + NOT MODELED (2 words), for two different reasons: + - KEY: pushes `(cell_t) getchar()` -- unlike every other word here, + this one's result VALUE depends on real external input, not just an + unmodelled side effect of an otherwise-determined transition. Same + category as string_words.c's EXPECT/QUERY (deferred there for + exactly this reason), even though KEY's own overflow guard alone is + trivial. + - ." (dot_quote): the compile-time immediate word depends on + vm->input_buffer/input_pos/input_length, the same unmodelled + TIB-adjacent input state string_words.c's S" was deferred for. + (do-string) -- ."'s RUNTIME companion -- is NOT in this category and + IS modeled below, using the same return-stack-held-address-into- + memory technique already established for control_words.c's branch + words and string_words.c's deferred (s") sibling. + + ── Genuine finding, not fixed: ?TERMINAL is a permanent stub ────────── + `io_word_question_terminal`'s own comment admits it: "Simple + implementation - always return false for now." It is registered, + callable, and returns a well-formed flag -- but that flag NEVER + reflects real terminal state, unconditionally. Modeled faithfully as + the constant `forth_false`, not "fixed" to poll anything. + + ── Genuine finding, not fixed: TYPE's bounds check has an integer- + overflow bypass, a real out-of-bounds read ────────────────────────── + `io_word_type`'s guard is `addr < 0 || count < 0 || (addr+count) > + VM_MEMORY_SIZE`, evaluated in signed cell_t arithmetic. If addr and + count are both large-but-individually-positive (e.g. both 2^62), their + sum overflows the signed 64-bit range and wraps to a NEGATIVE value + (two's complement, matching this codebase's established wraparound + semantics elsewhere, e.g. the ALLOT finding earlier in this sweep) -- + which then compares as LESS than VM_MEMORY_SIZE, so the check reports + "in bounds" for a request that is wildly out of bounds. Unlike the + ALLOT case (re-analyzed earlier in this sweep and found to be actually + safe), this one is a genuine, exploitable bypass: the subsequent loop + reads `vm->memory[addr+i]` for i up to a huge count, a real + out-of-bounds heap read. `type_overflow_witness_passes_check` and + `type_overflow_witness_is_actually_oob` below give a concrete, + machine-checked witness (addr = count = 2^62). Transcribed faithfully, + not fixed -- report, don't silently patch, per standing instruction. + ======================================================================== *) + +(* ── EMIT ( c -- ) ─────────────────────────────────────────────────────── *) + +definition forth_emit :: "vm_state \ vm_state" where + "forth_emit vm = + (case data_stack vm of + [] \ set_error vm + | c # rest \ vm\data_stack := rest\)" + +lemma emit_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_emit vm)" + by (simp add: forth_emit_def set_error_def assms) + +lemma emit_pops_one: + assumes "data_stack vm = c # rest" + shows "data_stack (forth_emit vm) = rest" + by (simp add: forth_emit_def assms) + +(* ── CR ( -- ) : pure I/O, no vm_state effect at all ─────────────────────── *) + +definition forth_cr :: "vm_state \ vm_state" where + "forth_cr vm = vm" + +lemma cr_is_identity: + "forth_cr vm = vm" + by (simp add: forth_cr_def) + +(* ── ?TERMINAL ( -- flag ) : permanent stub, see header finding ─────────── *) + +definition forth_question_terminal :: "vm_state \ vm_state" where + "forth_question_terminal vm = + (if ds_full vm then set_error vm else vm\data_stack := forth_false # data_stack vm\)" + +lemma question_terminal_overflow: + assumes "ds_full vm" + shows "vm_error (forth_question_terminal vm)" + by (simp add: forth_question_terminal_def set_error_def assms) + +lemma question_terminal_always_false: + assumes "\ ds_full vm" + shows "data_stack (forth_question_terminal vm) = forth_false # data_stack vm" + by (simp add: forth_question_terminal_def assms) + +(* ── TYPE ( addr u -- ) : see header finding on the overflow bypass ─────── *) + +definition forth_type :: "vm_state \ vm_state" where + "forth_type vm = + (case data_stack vm of + count # addr # rest \ + if addr count word_of_nat VM_MEMORY_SIZE data_stack := rest\) + else vm\data_stack := rest\ \ \printing is the only further effect, unmodelled\ + | _ \ set_error vm)" + +lemma type_underflow: + assumes "length (data_stack vm) < 2" + shows "vm_error (forth_type vm)" +proof (cases "data_stack vm") + case Nil then show ?thesis using assms by (simp add: forth_type_def set_error_def) +next + case (Cons x xs) then show ?thesis using assms + by (cases xs) (auto simp: forth_type_def set_error_def) +qed + +lemma type_normal: + assumes "data_stack vm = count # addr # rest" + assumes "\ (addr count word_of_nat VM_MEMORY_SIZE ((2 ^ 62 :: cell) (2 ^ 62 :: cell) + word_of_nat VM_MEMORY_SIZE VM_MEMORY_SIZE" + \ \NOT `by eval`: `eval` on `unat` forces the code generator to represent + the resulting nat in unary Peano form (no `Code_Target_Nat` import in + this session's HOL-Library setup), so evaluating `unat` of a word as + large as 2^62 tries to build ~4.6e18 `Suc` constructors -- this is what + hung the build for 15+ minutes and drove free memory toward zero + (2026-08-14). `unat_numeral` sidesteps code generation entirely: it's a + symbolic simp lemma (`unat (numeral b) = numeral b mod 2^LENGTH('a)`), + so the numeral arithmetic stays in `simp`'s fast binary-numeral engine, + never touching `eval`.\ + by (simp add: unat_numeral VM_MEMORY_SIZE_def) + +(* ── SPACE ( -- ) : pure I/O, no vm_state effect at all ──────────────────── *) + +definition forth_space :: "vm_state \ vm_state" where + "forth_space vm = vm" + +lemma space_is_identity: + "forth_space vm = vm" + by (simp add: forth_space_def) + +(* ── SPACES ( n -- ) : always pops, regardless of n's sign ──────────────── *) +(* C: negative n silently skips the print loop via an early `return` -- + NOT an error path, and the pop of n already happened unconditionally + before that check. So the vm_state effect is identical for every n. *) + +definition forth_spaces :: "vm_state \ vm_state" where + "forth_spaces vm = + (case data_stack vm of + [] \ set_error vm + | n # rest \ vm\data_stack := rest\)" + +lemma spaces_underflow: + assumes "data_stack vm = []" + shows "vm_error (forth_spaces vm)" + by (simp add: forth_spaces_def set_error_def assms) + +lemma spaces_pops_one_regardless_of_sign: + assumes "data_stack vm = n # rest" + shows "data_stack (forth_spaces vm) = rest" + by (simp add: forth_spaces_def assms) + +(* ── (do-string) ( -- ) : runtime companion of ." ──────────────────────── + Same return-stack-held-address-into-memory technique as + StarForth_Control_Words.thy's (BRANCH)/(0BRANCH) and + StarForth_String_Words.thy's deferred (s") sibling. Printing the string + itself is the unmodelled side effect; the IP-advance is fully + deterministic and modeled precisely, including the C's exact + cell-alignment padding formula (reusing CELL_BYTES from + StarForth_Dictionary_Words.thy). *) + +definition forth_do_string :: "vm_state \ vm_state" where + "forth_do_string vm = + (case return_stack vm of + [] \ set_error vm + | ip # rst \ + let n = unat (mem_read (memory vm) (unat ip) AND 0xFF); + skip = 1 + n; + m = skip mod CELL_BYTES; + padded = (if m = 0 then skip else skip + (CELL_BYTES - m)) + in vm\return_stack := (ip + word_of_nat padded) # rst\)" + +lemma do_string_underflow: + assumes "return_stack vm = []" + shows "vm_error (forth_do_string vm)" + by (simp add: forth_do_string_def set_error_def assms) + +lemma do_string_data_stack_unchanged: + "data_stack (forth_do_string vm) = data_stack vm" + by (auto simp: forth_do_string_def set_error_def Let_def split: list.split) + +lemma do_string_advances_ip_past_aligned_block: + assumes "return_stack vm = ip # rst" + assumes "n = unat (mem_read (memory vm) (unat ip) AND 0xFF)" + assumes "(1 + n) mod CELL_BYTES = 0" + shows "return_stack (forth_do_string vm) = (ip + word_of_nat (1 + n)) # rst" + using assms by (simp add: forth_do_string_def Let_def) + +(* ── ." -- NOT MODELLED, see SCOPE above ─────────────────────────────────── *) + +lemma dot_quote_not_modelled: True + \ \Compile-time half of S"'s io_words.c sibling: depends on + vm->input_buffer/input_pos/input_length, the TIB-adjacent input + state deferred throughout string_words.c (WORD/SPAN/TIB/etc). See + StarForth_String_Words.thy's header for the full argument.\ + by simp + +(* ── KEY -- NOT MODELLED, see SCOPE above ────────────────────────────────── *) + +lemma key_not_modelled: True + \ \KEY's pushed VALUE is `(cell_t) getchar()` -- real external input, + not determined by vm_state alone (unlike every other word in this + file, where I/O is a side effect of an otherwise fully-determined + transition). Same category as string_words.c's EXPECT/QUERY.\ + by simp + +end