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>
Completes the src/word_source/*.c sweep -- last of the 5 kernel-only
files.
Five INFER-*@ output accessors fully modelled: they read straight from
vm->last_inference_outputs, which is exactly the already-modelled
`last_inference :: inference_outputs_state option` field with matching
per-field names. Q.VARIANCE/INFER-DECAY-SLOPE/INFER-WINDOW-WIDTH get
guard/shape only, capturing a genuine finding: array_ptr sets vm->error
AND the caller still pushes a 0 placeholder regardless, unlike the
"error or push, never both" shape most guarded words in this sweep
follow. L8-UPDATE/L8-TABLE-FORCE get pop-shape only.
Second finding: L8-MODE/L8-UPDATE/L8-APPLY/L8-TABLE-FORCE manipulate
vm->ssm_l8_state (a legacy 16-mode struct) and, per L8-TABLE-FORCE's own
comment, a separate 128-config adaptive table the heartbeat's bandit
actually drives -- NEITHER is the `ssm_l8 :: ssm_l8_state` (4-mode
C0..C3) field this proof suite has modelled since early in the sweep.
Three L8 representations exist in the real system; none of this file's
words touch the one the model tracks. Flagged as an open question, not
guessed at.
WINDOW-DIVERSITY, INFER-RUN, L8-MODE, L8-APPLY, and the six BAYES-*
words deferred (unmodelled subsystems: rolling-window diversity
algorithm, the whole inference-engine run, legacy L8 state, hot-words
cache Bayesian posteriors).
Suite now 53 theories, green.
