diff --git a/proof/ROOT b/proof/ROOT index b3817ac..8c5c0ae 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -29,6 +29,10 @@ session "StarForth" = "HOL-Library" + StarForth_Physics_Benchmark_Words StarForth_Physics_Pipelining_Diagnostic_Words StarForth_StarForth_Words + StarForth_Framebuffer_Words + StarForth_Keyboard_Words + StarForth_Scroll_Words + StarForth_TTF_Words StarForth_Loop1_Heat StarForth_Loop2_Window StarForth_Loop3_Decay diff --git a/proof/StarForth_Framebuffer_Words.thy b/proof/StarForth_Framebuffer_Words.thy new file mode 100644 index 0000000..813bb4e --- /dev/null +++ b/proof/StarForth_Framebuffer_Words.thy @@ -0,0 +1,96 @@ +theory StarForth_Framebuffer_Words + imports StarForth_Base +begin + +(* ========================================================================= + Mirrors: src/word_source/framebuffer_words.c + Registers: PLOT FB-WIDTH FB-HEIGHT + + Part of the Stadium console fabric work (FABRIC.md item 4.3.3). All + three words are registered UNCONDITIONALLY in both hosted and kernel + builds, but their bodies are `#ifdef __STARKERNEL__`-gated: the kernel + branch calls real framebuffer hardware functions (fb_put_pixel/ + fb_width/fb_height), the hosted branch is a fixed fallback with no + hardware dependency at all. + + ── Scope ───────────────────────────────────────────────────────────── + The HOSTED build's behaviour is fully modelled -- it is deterministic + and has no hardware dependency (this repo's `make` still produces a + plain hosted binary per CLAUDE.md, so this is a real, reachable build + configuration, not a hypothetical). The KERNEL build's behaviour is not + modelled: fb_put_pixel/fb_width/fb_height are raw hardware framebuffer + accessors with no vm_state counterpart, the same class of gap as every + other hardware-boundary word in this console-fabric group. + + ── Finding: FB-WIDTH/FB-HEIGHT have no overflow guard ────────────────── + Neither checks `ds_full` (or any capacity condition) before pushing -- + same hazard class as physics_freeze_words.c's DECAY-RATE@, the first + instance of this sweep finding a missing overflow guard. Second + instance now, both in diagnostic/hardware-boundary words that read as + "just returns a number" and evidently didn't get the same underflow- + guard-writing discipline as stack-manipulation words. + ======================================================================== *) + +(* ── PLOT ( x y color -- ) : hosted build ─────────────────────────────── *) +(* C: guard `vm->dsp < 2` (need 3 elements); hosted branch discards all + three popped values with no further effect. *) + +definition forth_plot_hosted :: "vm_state \ vm_state" where + "forth_plot_hosted vm = + (case data_stack vm of + color # y # x # xs \ vm\data_stack := xs\ + | _ \ set_error vm)" + +lemma plot_hosted_underflow_nil: + assumes "data_stack vm = []" + shows "vm_error (forth_plot_hosted vm)" + by (simp add: forth_plot_hosted_def set_error_def assms) + +lemma plot_hosted_underflow_one: + assumes "data_stack vm = [a]" + shows "vm_error (forth_plot_hosted vm)" + by (simp add: forth_plot_hosted_def set_error_def assms) + +lemma plot_hosted_underflow_two: + assumes "data_stack vm = [a, b]" + shows "vm_error (forth_plot_hosted vm)" + by (simp add: forth_plot_hosted_def set_error_def assms) + +lemma plot_hosted_normal: + assumes "data_stack vm = color # y # x # xs" + shows "forth_plot_hosted vm = vm\data_stack := xs\" + by (simp add: forth_plot_hosted_def assms) + +lemma plot_kernel_not_modelled: True + \ \Kernel build: fb_put_pixel((uint32_t)x, (uint32_t)y, (uint32_t)color) + -- raw hardware framebuffer write, no vm_state counterpart.\ + by simp + +(* ── FB-WIDTH / FB-HEIGHT ( -- n ) : hosted build ─────────────────────── *) +(* C: hosted branch pushes 0 unconditionally, no capacity guard at all. *) + +definition forth_fb_width_hosted :: "vm_state \ vm_state" where + "forth_fb_width_hosted vm = vm\data_stack := 0 # data_stack vm\" + +definition forth_fb_height_hosted :: "vm_state \ vm_state" where + "forth_fb_height_hosted vm = vm\data_stack := 0 # data_stack vm\" + +lemma fb_width_hosted_pushes_zero: + "data_stack (forth_fb_width_hosted vm) = 0 # data_stack vm" + by (simp add: forth_fb_width_hosted_def) + +lemma fb_height_hosted_pushes_zero: + "data_stack (forth_fb_height_hosted vm) = 0 # data_stack vm" + by (simp add: forth_fb_height_hosted_def) + +lemma fb_width_hosted_no_overflow_guard: True + \ \See file header finding -- unconditional push, no ds_full check, + modelled faithfully.\ + by simp + +lemma fb_dimensions_kernel_not_modelled: True + \ \Kernel build: fb_width()/fb_height() query real hardware/firmware + framebuffer geometry -- no vm_state counterpart.\ + by simp + +end diff --git a/proof/StarForth_Keyboard_Words.thy b/proof/StarForth_Keyboard_Words.thy new file mode 100644 index 0000000..c7231eb --- /dev/null +++ b/proof/StarForth_Keyboard_Words.thy @@ -0,0 +1,105 @@ +theory StarForth_Keyboard_Words + imports StarForth_Base +begin + +(* ========================================================================= + Mirrors: src/word_source/keyboard_words.c + Registers: KBD-SCAN KBD-DEBUG VKBD-EVENT VKBD-DEBUG KEY-EVENT ALT+TAB + + Part of the Stadium console fabric work (FABRIC.md items 4.3.5/4.4v/ + 4.4y). All six words are registered UNCONDITIONALLY regardless of + build/arch, but every body is gated on `__STARKERNEL__` (and, for the + amd64-specific/riscv64-aarch64-specific pairs, the target architecture + too). Outside the matching kernel+arch combination, every one of these + six falls through to a fixed, hardware-independent fallback -- + identically to framebuffer_words.c, and reachable the same way (a + plain hosted `make` build). + + ── Scope ───────────────────────────────────────────────────────────── + The fallback (non-kernel-or-wrong-arch) behaviour of all six words is + fully modelled: every one reduces to a fixed constant push (or, for + ALT+TAB, a true no-op) with NO capacity guard before pushing -- the + third and fourth instances of the missing-overflow-guard finding first + raised in physics_freeze_words.c's DECAY-RATE@ (KBD-SCAN/VKBD-EVENT/ + VKBD-DEBUG/KEY-EVENT push 1-2 cells unconditionally; KBD-DEBUG pushes + 2). The real (matching kernel+arch) hardware-polling bodies are NOT + modelled: i8042_pop_scancode/virtio_input_pop_event/ + console_fb_toggle_graphics are all raw hardware/interrupt-state reads + with no vm_state counterpart, the same class of gap as every other + hardware-boundary word in this console-fabric group. `sk_key_event_poll` + is a small pure function (bit 7 of an XT scancode byte / a virtio-input + value field, both external to vm_state either way) -- its fallback + branch (`return 0`) is what's modelled here as part of KEY-EVENT's + fallback; its two hardware branches are not. + ======================================================================== *) + +(* ── KBD-SCAN ( -- c -1 | 0 ) : fallback pushes 0 ────────────────────────── *) + +definition forth_kbd_scan_fallback :: "vm_state \ vm_state" where + "forth_kbd_scan_fallback vm = vm\data_stack := 0 # data_stack vm\" + +lemma kbd_scan_fallback_pushes_zero: + "data_stack (forth_kbd_scan_fallback vm) = 0 # data_stack vm" + by (simp add: forth_kbd_scan_fallback_def) + +(* ── KBD-DEBUG ( -- isr_count spurious_count ) : fallback pushes 0 0 ─────── *) + +definition forth_kbd_debug_fallback :: "vm_state \ vm_state" where + "forth_kbd_debug_fallback vm = vm\data_stack := 0 # 0 # data_stack vm\" + +lemma kbd_debug_fallback_pushes_zeros: + "data_stack (forth_kbd_debug_fallback vm) = 0 # 0 # data_stack vm" + by (simp add: forth_kbd_debug_fallback_def) + +(* ── VKBD-EVENT ( -- code value -1 | 0 ) : fallback pushes 0 ────────────── *) + +definition forth_vkbd_event_fallback :: "vm_state \ vm_state" where + "forth_vkbd_event_fallback vm = vm\data_stack := 0 # data_stack vm\" + +lemma vkbd_event_fallback_pushes_zero: + "data_stack (forth_vkbd_event_fallback vm) = 0 # data_stack vm" + by (simp add: forth_vkbd_event_fallback_def) + +(* ── VKBD-DEBUG ( -- isr_count ) : fallback pushes 0 ─────────────────────── *) + +definition forth_vkbd_debug_fallback :: "vm_state \ vm_state" where + "forth_vkbd_debug_fallback vm = vm\data_stack := 0 # data_stack vm\" + +lemma vkbd_debug_fallback_pushes_zero: + "data_stack (forth_vkbd_debug_fallback vm) = 0 # data_stack vm" + by (simp add: forth_vkbd_debug_fallback_def) + +(* ── KEY-EVENT ( -- keycode pressed -1 | 0 ) : fallback pushes 0 ────────── *) +(* sk_key_event_poll's fallback branch (neither ARCH_AMD64 nor riscv64/ + aarch64 under __STARKERNEL__) returns 0 without touching its out-params; + kbw_key_event's `else` branch then pushes a single 0. *) + +definition forth_key_event_fallback :: "vm_state \ vm_state" where + "forth_key_event_fallback vm = vm\data_stack := 0 # data_stack vm\" + +lemma key_event_fallback_pushes_zero: + "data_stack (forth_key_event_fallback vm) = 0 # data_stack vm" + by (simp add: forth_key_event_fallback_def) + +(* ── ALT+TAB ( -- ) : fallback is a true no-op ───────────────────────────── *) + +definition forth_alt_tab_fallback :: "vm_state \ vm_state" where + "forth_alt_tab_fallback vm = vm" + +lemma alt_tab_fallback_identity: "forth_alt_tab_fallback vm = vm" + by (simp add: forth_alt_tab_fallback_def) + +lemma alt_tab_kernel_not_modelled: True + \ \Kernel build: console_fb_toggle_graphics() -- console/framebuffer + mode-toggle state, no vm_state counterpart.\ + by simp + +lemma keyboard_kernel_bodies_not_modelled: True + \ \All five hardware-polling words' real (kernel+matching-arch) bodies + -- i8042_pop_scancode/virtio_input_pop_event and their associated ISR + counters (g_i8042_isr_count/g_spurious_count/g_virtio_input_isr_count, + themselves file-scope C statics/externs) -- are not modelled. Same + class of gap as every hardware-boundary word in this group.\ + by simp + +end diff --git a/proof/StarForth_Scroll_Words.thy b/proof/StarForth_Scroll_Words.thy new file mode 100644 index 0000000..5a33a96 --- /dev/null +++ b/proof/StarForth_Scroll_Words.thy @@ -0,0 +1,45 @@ +theory StarForth_Scroll_Words + imports StarForth_Base +begin + +(* ========================================================================= + Mirrors: src/word_source/scroll_words.c + Registers (kernel-only -- see below): SCROLL-BACK SCROLL-FWD + + Part of the Stadium console fabric work (FABRIC.md item 4.4q). Unlike + framebuffer_words.c/keyboard_words.c, this file's word BODIES and its + `register_word` calls are BOTH inside `#ifdef __STARKERNEL__` -- + `register_scroll_words` registers nothing at all on a hosted build + (the `#else` branch is just `(void) vm;`). SCROLL-BACK/SCROLL-FWD + therefore do not exist as words in the hosted build this suite's other + console-fabric theories could otherwise fall back to modelling. + + Kernel build: both words pop one cell (via `vm_pop`'s own underflow + guard, per the file's own comment explaining why no separate `dsp` + precheck is used -- deferring to whichever convention `vm_pop` itself + follows rather than risking a mismatch against this codebase's more + than one historical `dsp` convention), clamp negative values to 0, then + call `console_fb_scroll_back`/`console_fb_scroll_fwd` -- raw console + scrollback-view state with no vm_state counterpart. Not modelled: there + is no hosted-build fallback to fall back to, and the kernel body is a + hardware/console-state mutation like the rest of this group. *) + +lemma scroll_words_not_registered_on_hosted_build: True + \ \register_scroll_words's hosted-build `#else` branch does nothing -- + SCROLL-BACK/SCROLL-FWD are absent from the dictionary entirely + outside a kernel build, unlike every other console-fabric file in + this sweep (which all register unconditionally with a fallback + body).\ + by simp + +lemma scroll_back_not_modelled: True + \ \Kernel build: pop (vm_pop's own guard) + clamp negative-to-0 + call + console_fb_scroll_back(n) -- console scrollback state, no vm_state + counterpart.\ + by simp + +lemma scroll_fwd_not_modelled: True + \ \Same shape as SCROLL-BACK, console_fb_scroll_fwd(n).\ + by simp + +end diff --git a/proof/StarForth_TTF_Words.thy b/proof/StarForth_TTF_Words.thy new file mode 100644 index 0000000..e8efd50 --- /dev/null +++ b/proof/StarForth_TTF_Words.thy @@ -0,0 +1,51 @@ +theory StarForth_TTF_Words + imports StarForth_Base +begin + +(* ========================================================================= + Mirrors: src/word_source/ttf_words.c + Registers (kernel-only -- see below): TTF-TEXT + + Part of the Stadium console fabric work (FABRIC.md item 4.3.7e). Same + shape as scroll_words.c: the word body AND its `register_word` call are + both inside `#ifdef __STARKERNEL__`; TTF-TEXT does not exist as a word + at all on a hosted build. + + Kernel build: guard `vm->dsp < 5` (needs 6 elements: c-addr u x y size + color), pops all six, then depends entirely on the TTF subsystem -- + font-capsule loading (`ttf_words_ensure_font`, itself guarded by a + file-scope `static int g_ttf_font_ready` -- another instance of the + file-scope-static-instead-of-per-VM pattern this sweep keeps finding, + though here arguably correct/intentional: a loaded font glyph cache is + process-wide resource sharing, not per-VM interpreter state, and there + is exactly one font asset regardless of how many VMs are in the Tripod + fleet), a hand-rolled UTF-8 decoder reading VM memory via `vm_load_u8`/ + `vm_addr_ok` (tractable in principle -- StarForth_Base.thy's `memory` + field could back it -- but not attempted here given nothing else in + this word is modellable, so a UTF-8-decode-only partial model would + have no consumer), and raster/blit calls into the framebuffer + + raster-cache subsystem. None of TTF-TEXT's effect is modelled beyond + the guard shape. *) + +lemma ttf_text_not_registered_on_hosted_build: True + \ \Same absent-on-hosted shape as SCROLL-BACK/SCROLL-FWD (see + StarForth_Scroll_Words.thy) -- register_ttf_words's `#else` branch is + `(void) vm;`, nothing registered.\ + by simp + +lemma ttf_text_guard_only_not_mechanised: True + \ \Kernel build: `vm->dsp < 5` guards a 6-cell pop (c-addr u x y size + color). The guard SHAPE follows the same pattern as every other + multi-pop word in this sweep, but is not mechanised here since + nothing downstream of it is modellable (see file header) -- a bare + guard lemma with no consumer would be dead weight, unlike + framebuffer_words.c/keyboard_words.c where the fallback body gives + the guard somewhere to lead.\ + by simp + +lemma ttf_text_body_not_modelled: True + \ \Font-capsule loading, UTF-8 decoding of VM memory, and raster-cache/ + framebuffer blitting -- see file header for the full breakdown.\ + by simp + +end