Robert Allan JamesandClaude Sonnet 5
dfdabcc2d7
DECAY-RATE@ (physics_freeze_words.c) pushed to the data stack with no capacity check and no prior pop to make room, unlike its neighbors in the same file -- the one live, unconditional missing-guard bug the Isabelle sweep's ~15 candidate findings reduced to once checked against vm_push()'s real internal bounds check (see proof/FINDINGS.md SS2). Removed dictionary_manipulation_words.c's [ ] STATE and defining_words.c's DEFER IS DEFER@ (plus the now-orphaned defining_runtime_defer helper) -- all confirmed permanently shadowed by later dictionary registrations (defining_words.c and defer_words.c respectively), per FORTH's newest-first lookup. No behavior change: the removed code was already unreachable. Verified: hosted `make` builds clean under -Wall -Werror; the hosted self-test suite passes 965/965 implemented tests with no regressions. Three-architecture QEMU acceptance boot, all clean to ok> with an identical dict_hash=0x24b4279f0670aa3a across amd64/aarch64/riscv64 and identical 1003/965/0/0 test totals -- logs attached. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
101 lines
4.6 KiB
Plaintext
101 lines
4.6 KiB
Plaintext
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.
|
|
|
|
── CORRECTED finding: FB-WIDTH/FB-HEIGHT are NOT missing a guard ───────
|
|
Both push via C's `vm_push()` (src/stack_management.c:75), which bounds-
|
|
checks internally (`if (vm->dsp >= STACK_SIZE - 1) ...`) before every
|
|
write -- this file's earlier claim that neither checks capacity was a
|
|
gap in this theory's abstract push model, not a real defect in the C.
|
|
Re-verified 2026-08-14 during the sweep's repair pass; see
|
|
proof/FINDINGS.md §2 for the full correction across all files this
|
|
pattern was raised against.
|
|
======================================================================== *)
|
|
|
|
(* ── 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 via vm_push(), which bounds-checks internally
|
|
(see corrected header finding above) -- the abstract push below still
|
|
models an unconditional push since this theory's stack has no depth
|
|
bound to violate, but the real C is guarded. *)
|
|
|
|
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
|