Add POST coverage for physics-freeze words (Module 27), fix two real bugs found in the process
Cluster 4 of the POST-coverage sweep: physics_freeze_words_test.c covers the 6 words proof/StarForth_Physics_Freeze_Words.thy actually gives real lemmas for (FREEZE-WORD, UNFREEZE-WORD, FROZEN?, HEAT!, HEAT@, DECAY-RATE@), correcting an earlier fork summary's wrong "5 words" scope. Writing the tests surfaced two independent, pre-existing bugs in physics_freeze_words.c, both now fixed: - Every address-taking word cast the VM's caddr directly to a host pointer instead of resolving it through vm_ptr() -- caddr is an offset into vm->memory, not a host pointer. Fixed in all 9 call sites (the 5 in-scope words plus SHOW-HEAT, which shares the identical pattern). - Every underflow check used dsp < N (item count) instead of dsp < N-1, since this VM's dsp is a 0-indexed top-of-stack pointer. Fixed in all 6 checks. Together these meant every word in this file taking a stack-supplied name has been broken for any real caller since the file was written. Verified zero build warnings and a clean three-arch QEMU boot (amd64/aarch64/riscv64), 1009 passed / 0 failed / 0 errors identically on all three, dict_hash matching across arches. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
co-authored by
Claude Sonnet 5
Claude Sonnet 5
parent
825ab078f1
commit
abb858a300
+69
@@ -1542,3 +1542,72 @@ was meant to avoid, not just silenced a check.
|
||||
|
||||
One cluster left: physics freeze/diagnostic (5 words: `FREEZE-WORD`, `FREEZE-CRITICAL`,
|
||||
`UNFREEZE-WORD`, `FROZEN?`, `DECAY-RATE@`).
|
||||
|
||||
**Cluster 4, physics freeze/diagnostic — done, and this one caught two real pre-existing bugs
|
||||
in production code, not just test-authoring mistakes.** First correction, before any code was
|
||||
written: the scope quoted above (5 words, including `FREEZE-CRITICAL`) came from the fork's
|
||||
secondhand summary and was wrong. Reading `proof/StarForth_Physics_Freeze_Words.thy` directly
|
||||
(`grep -n "^lemma|^theorem"`) shows real, non-`True`-placeholder lemmas for **6** words —
|
||||
`FREEZE-WORD`, `UNFREEZE-WORD`, `FROZEN?`, `HEAT!`, `HEAT@`, `DECAY-RATE@` — while
|
||||
`FREEZE-CRITICAL` (plus `SHOW-HEAT`/`ALL-HEATS`, neither ever in scope) carries only a trivial
|
||||
`freeze_critical_per_word_effect_is_freeze_word: True` placeholder. This matches
|
||||
`proof/COVERAGE.md`'s own "6/9" figure; the fork's "5" was simply wrong, missing `HEAT!`/
|
||||
`HEAT@` and wrongly including `FREEZE-CRITICAL`. New file `physics_freeze_words_test.c`
|
||||
(Module 27) covers exactly the verified 6, tabular `WordTestSuite` format, using `S"` +
|
||||
scratch colon-definitions (`: __freeze_test_word__ ; S" __freeze_test_word__" ...`) as targets
|
||||
so tests don't disturb any real dictionary word's freeze/heat state. Used plain
|
||||
`run_test_suite` (no contract), matching `defining_words_tests.c`'s precedent — these cases
|
||||
define dictionary words, and `check_physics_transparent`'s own header comment documents that
|
||||
it does not snapshot/restore dictionary state around its re-run, so `CONTRACT_PHYSICS_
|
||||
TRANSPARENT`/`CONTRACT_NONE` selection wasn't even the right question here.
|
||||
|
||||
**Bug 1 — wrong-typed pointer cast, in production code, all 6 in-scope words plus `SHOW-HEAT`
|
||||
(9 total call sites across the file).** First boot: 6 failures, 5 of the 6 target words
|
||||
erroring, only `DECAY-RATE@` (the one word taking no address argument) passing. Every
|
||||
address-taking word did `const char *name = (const char *)(uintptr_t)caddr;` — treating the
|
||||
VM's `caddr` as a raw host pointer. But per `include/vm.h:834`'s `vm_ptr()` and this project's
|
||||
own convention (this file's own CLAUDE.md: "Stack values are VM offsets (`vaddr_t`), not C
|
||||
pointers — use `VM_ADDR()`"), `caddr` is an *offset into `vm->memory`* (`vm->memory +
|
||||
(size_t)addr`), not a host pointer — confirmed by reading `vm_ptr()`'s actual body, not just
|
||||
its declaration. The correct idiom, used correctly elsewhere in the same tree (`physics_
|
||||
pipelining_diagnostic_words.c:85`: `vm_ptr(vm, (vaddr_t)(uint64_t)addr)`), was simply never
|
||||
applied here. Fixed all 9 occurrences (`FREEZE-WORD`, `UNFREEZE-WORD`, `FROZEN?`, `HEAT!`,
|
||||
`HEAT@`, and `SHOW-HEAT` — the last isn't proof-covered and isn't in this cluster's test scope,
|
||||
but shares the identical bug pattern in the identical file, so fixing it alongside the other 5
|
||||
is the coherent minimal fix, not scope creep).
|
||||
|
||||
**Bug 2 — off-by-one in every underflow check in the same file, masked until Bug 1 was fixed
|
||||
enough to actually reach it.** Even after Bug 1's fix, the same 6 failures persisted. Traced
|
||||
with a temporary `fprintf` probe (written, used, reverted per this session's established
|
||||
probe-capture-revert convention — never landed in the commit) through `S"`'s runtime push and
|
||||
each word's entry: this VM's `dsp` is a **0-indexed top-of-stack pointer**, not an item count —
|
||||
confirmed via `stack_management.c`'s own `vm_pop()` underflow check (`if (vm->dsp < 0)`, i.e.
|
||||
empty-stack `dsp == -1`) and cross-checked against a working sibling
|
||||
(`physics_pipelining_diagnostic_words.c:145`'s `dsp < 1` guard for its own 2-item pop). Every
|
||||
`( caddr u -- )`/`( heat caddr u -- )` underflow check in `physics_freeze_words.c` used
|
||||
`dsp < N` (item count) instead of `dsp < N-1` (top-of-stack index) — `FREEZE-WORD`/`UNFREEZE-
|
||||
WORD`/`FROZEN?`/`HEAT@`/`SHOW-HEAT` all checked `dsp < 2` (should be `dsp < 1`), `HEAT!`
|
||||
checked `dsp < 3` (should be `dsp < 2`). This means **every one of these words has been broken
|
||||
for any real caller supplying a stack-based name**, for as long as the file has existed —
|
||||
Bug 1 alone wasn't sufficient to explain the failures, this second, independent bug was always
|
||||
there underneath it. Fixed all 6 occurrences with an inline comment explaining the convention,
|
||||
so it doesn't get re-introduced.
|
||||
|
||||
Verified: zero build warnings hosted and on all three kernel architectures. Isolated hosted-
|
||||
binary reproduction first (faster iteration than QEMU) — `DBGPROBE` trace confirmed `dsp=1`
|
||||
immediately after `S"` pushed 2 cells, which is *correct* under the top-of-stack-index
|
||||
convention (proving Bug 2, not a third bug), then hosted rebuild after both fixes: all 7 test-
|
||||
suite entries pass (1009 total passed vs. the pre-fix run, 0 failed, 0 errors). Full three-arch
|
||||
kernel boot: amd64/aarch64/riscv64 all show `Physics Freeze Words Summary` running cleanly,
|
||||
`FINAL TEST SUMMARY` **1009 passed / 0 failed / 0 errors identically on all three**, and
|
||||
`dict_hash` matches exactly across all three arches (`0xa4e77b13fbe0049e` MAMA_INIT,
|
||||
`0x87e7b27b0405b2b3` Hermes birth) — cross-arch determinism intact after both fixes.
|
||||
|
||||
This closes the fourth and final cluster of the POST-coverage milestone — all four (ACL,
|
||||
Q48.16, inference-engine, physics freeze/diagnostic) are now done, and along the way this
|
||||
sequence caught one real bug in the test suite's own restore-state helper (`restore_vm_state()`,
|
||||
recorded above), one test-authoring mistake (`ACL-INHERIT` push order, Cluster 1), and now two
|
||||
independent, previously-undetected production bugs in `physics_freeze_words.c` that predate
|
||||
this session entirely. Per the user's own sequencing ("code sweeps → HOL green → POST
|
||||
coverage"), this closes that sequence; LOGO/turtle demo + HOWTOs + SDK beginnings are next,
|
||||
pending explicit go-ahead.
|
||||
|
||||
Reference in New Issue
Block a user