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>
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).
