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
46 lines
2.1 KiB
Plaintext
46 lines
2.1 KiB
Plaintext
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-0.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
|