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