proof/: add console-fabric word coverage (framebuffer/keyboard/scroll/ttf)
Stadium console fabric words (FABRIC.md items 4.3.3/4.3.5/4.3.7e/4.4q/ 4.4v/4.4y). All four files gate their real hardware-touching bodies behind __STARKERNEL__ (and, for keyboard, architecture too): - StarForth_Framebuffer_Words.thy: PLOT/FB-WIDTH/FB-HEIGHT fully modelled for the hosted-build fallback (deterministic, no hardware dependency); kernel bodies (fb_put_pixel/fb_width/fb_height) deferred. Finding: FB-WIDTH/FB-HEIGHT have no overflow guard before pushing -- second instance of this class of bug after DECAY-RATE@. - StarForth_Keyboard_Words.thy: all 6 words' non-kernel-or-wrong-arch fallback modelled (fixed constant pushes / no-op); third and fourth missing-overflow-guard instances. Real hardware polling (i8042/virtio-input) deferred. - StarForth_Scroll_Words.thy / StarForth_TTF_Words.thy: both files gate registration itself behind __STARKERNEL__, so their words don't exist at all in a hosted build -- no fallback to model, sentinel-only. Suite now 48 theories, confirmed green via a full clean rebuild (HOL- Library cold-built in 15m18s after an accidental heap clear, StarForth itself 33s).
This commit is contained in:
Robert Allan James
@@ -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
|
||||
|
||||
@@ -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 \<Rightarrow> vm_state" where
|
||||
"forth_plot_hosted vm =
|
||||
(case data_stack vm of
|
||||
color # y # x # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>
|
||||
| _ \<Rightarrow> 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\<lparr>data_stack := xs\<rparr>"
|
||||
by (simp add: forth_plot_hosted_def assms)
|
||||
|
||||
lemma plot_kernel_not_modelled: True
|
||||
\<comment> \<open>Kernel build: fb_put_pixel((uint32_t)x, (uint32_t)y, (uint32_t)color)
|
||||
-- raw hardware framebuffer write, no vm_state counterpart.\<close>
|
||||
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 \<Rightarrow> vm_state" where
|
||||
"forth_fb_width_hosted vm = vm\<lparr>data_stack := 0 # data_stack vm\<rparr>"
|
||||
|
||||
definition forth_fb_height_hosted :: "vm_state \<Rightarrow> vm_state" where
|
||||
"forth_fb_height_hosted vm = vm\<lparr>data_stack := 0 # data_stack vm\<rparr>"
|
||||
|
||||
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
|
||||
\<comment> \<open>See file header finding -- unconditional push, no ds_full check,
|
||||
modelled faithfully.\<close>
|
||||
by simp
|
||||
|
||||
lemma fb_dimensions_kernel_not_modelled: True
|
||||
\<comment> \<open>Kernel build: fb_width()/fb_height() query real hardware/firmware
|
||||
framebuffer geometry -- no vm_state counterpart.\<close>
|
||||
by simp
|
||||
|
||||
end
|
||||
@@ -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 \<Rightarrow> vm_state" where
|
||||
"forth_kbd_scan_fallback vm = vm\<lparr>data_stack := 0 # data_stack vm\<rparr>"
|
||||
|
||||
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 \<Rightarrow> vm_state" where
|
||||
"forth_kbd_debug_fallback vm = vm\<lparr>data_stack := 0 # 0 # data_stack vm\<rparr>"
|
||||
|
||||
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 \<Rightarrow> vm_state" where
|
||||
"forth_vkbd_event_fallback vm = vm\<lparr>data_stack := 0 # data_stack vm\<rparr>"
|
||||
|
||||
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 \<Rightarrow> vm_state" where
|
||||
"forth_vkbd_debug_fallback vm = vm\<lparr>data_stack := 0 # data_stack vm\<rparr>"
|
||||
|
||||
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 \<Rightarrow> vm_state" where
|
||||
"forth_key_event_fallback vm = vm\<lparr>data_stack := 0 # data_stack vm\<rparr>"
|
||||
|
||||
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 \<Rightarrow> 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
|
||||
\<comment> \<open>Kernel build: console_fb_toggle_graphics() -- console/framebuffer
|
||||
mode-toggle state, no vm_state counterpart.\<close>
|
||||
by simp
|
||||
|
||||
lemma keyboard_kernel_bodies_not_modelled: True
|
||||
\<comment> \<open>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.\<close>
|
||||
by simp
|
||||
|
||||
end
|
||||
@@ -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
|
||||
\<comment> \<open>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).\<close>
|
||||
by simp
|
||||
|
||||
lemma scroll_back_not_modelled: True
|
||||
\<comment> \<open>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.\<close>
|
||||
by simp
|
||||
|
||||
lemma scroll_fwd_not_modelled: True
|
||||
\<comment> \<open>Same shape as SCROLL-BACK, console_fb_scroll_fwd(n).\<close>
|
||||
by simp
|
||||
|
||||
end
|
||||
@@ -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
|
||||
\<comment> \<open>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.\<close>
|
||||
by simp
|
||||
|
||||
lemma ttf_text_guard_only_not_mechanised: True
|
||||
\<comment> \<open>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.\<close>
|
||||
by simp
|
||||
|
||||
lemma ttf_text_body_not_modelled: True
|
||||
\<comment> \<open>Font-capsule loading, UTF-8 decoding of VM memory, and raster-cache/
|
||||
framebuffer blitting -- see file header for the full breakdown.\<close>
|
||||
by simp
|
||||
|
||||
end
|
||||
Reference in New Issue
Block a user