Robert Allan JamesandClaude Sonnet 5
8717416d36
LITHOS_VERSION 2.0.1 was premature: per this project's own versioning policy, 2.0.1 claims SER5 hardware-track progress (RDRAND backend + thumbdrive image) that was never actually verified on real hardware -- that verification is FABRIC-3.md's own open topic. Reset to 2.0.0 (still a QEMU-only release, correctly). Verified 3-arch boot shows "LithosAnanke v2.0.0" in each serial log directly, not assumed from the Makefile edit alone. Also closes a real gap found in today's earlier FABRIC-series rename: Makefile.starkernel, Kconfig.kernel, scripts/bleach_zuse_img.sh, four proof/*.thy files, and isr.S were never swept -- the original file list only matched *.md/*.c/*.h/*.4th, silently skipping every other extension. Fixed with the same safe placeholder substitution. .claude/settings.local.json's historical permission-grant log and ClaudeEXPORT/'s frozen export were deliberately left untouched. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019YcT3H2PQeyujrzjqS3Var
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-0.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
|