3 Commits

Include renames

Author	SHA1	Message	Date
Robert Allan JamesandClaude Sonnet 5	8717416d36	FABRIC-3.md: version correction -- LITHOS_VERSION back to 2.0.0, plus a rename-gap fix ... 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	2026-09-04 11:53:44 -04:00
Robert Allan JamesandClaude Sonnet 5	dfdabcc2d7	word_source: repair DECAY-RATE@ overflow guard and remove dead shadowed registrations ... 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>	2026-08-14 21:33:17 -04:00
Robert Allan James	1e76ebea97	proof/: add console-fabric word coverage (framebuffer/keyboard/scroll/ttf) ... 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).	2026-08-14 16:15:27 -04:00