POST coverage cluster 1/4: ACL accessors (proof-covered, previously untested)
Adds interpreter-level POST coverage for six ACL read accessors (ACL-MODE@/PINNED?/TTL@/ALLOW@/HEAT@/WORD-ID), ACL-INHERIT as an interpreted word (not just its underlying C function, already tested), and ACL-INIT-PRIMITIVES -- all proof-covered per proof/COVERAGE.md but never exercised via vm_interpret() before. Follows acl_words_test.c's existing hand-rolled ACL_ASSERT style, not the WordTestSuite table format the rest of the tree uses. First boot caught a real bug in the new test itself (2/29 assertions failed): ACL-INHERIT's C implementation pops dst before src, the test pushed them backwards. Fixed the test, not the word -- ACL-INHERIT's own dispatch was correct throughout. Re-verified: 29/29 pass, zero build warnings. Both the failing and fixed boot logs kept as evidence. Part of the agreed sequence (code sweeps -> HOL green -> POST coverage, one proof-covered cluster at a time). Three more clusters queued: Q48.16 math primitives, inference-engine accessors, physics freeze/diagnostic words. Full writeup in FABRIC-2.md Section J. 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
e535346504
commit
b2918fd0b2
+37
@@ -1436,3 +1436,40 @@ occurrences of `error`/`fail`/`sorry`/`oops`/`exception`/`abort` anywhere in the
|
||||
log.** This is the real, current, verified state — not inferred from file/`ROOT` consistency
|
||||
as the earlier entry above had to settle for. The 52-theory count itself (vs. `FINDINGS.md`'s
|
||||
stale "53") is confirmed correct by this run too.
|
||||
|
||||
**Third milestone in the same sequence: POST test coverage for proof-covered-but-untested
|
||||
words, in progress, one cluster at a time.** A fork cross-referenced every `register_word()`
|
||||
call in `src/word_source/*.c` (317 words total) against `WordTestSuite` table entries in
|
||||
`src/test_runner/modules/*.c`, then narrowed to the words `proof/COVERAGE.md` actually claims
|
||||
proof coverage for — landing on four small clusters genuinely proof-covered with zero POST
|
||||
exercise: ACL accessors (9 words, `acl_words.c`), Q48.16 math primitives (21 words,
|
||||
`q48_words.c`), inference-engine accessors (8 words, `inference_words.c`), physics freeze/
|
||||
diagnostic (5 words). The much larger raw 170-word gap the fork also found is mostly words
|
||||
`COVERAGE.md` itself already rules out of proof scope entirely (block-window cache,
|
||||
vocabulary chain, hot-words cache, interactive-only words) — not the target here.
|
||||
|
||||
**Cluster 1, ACL accessors — done.** `src/test_runner/modules/acl_words_test.c` doesn't use
|
||||
the `WordTestSuite` table format the rest of the tree does (hand-rolled `ACL_ASSERT` macro,
|
||||
direct `vm_interpret()` calls) — new tests follow its existing style, not the tabular one.
|
||||
Added three new tests: read accessors (`ACL-MODE@`/`ACL-PINNED?`/`ACL-TTL@`/`ACL-ALLOW@`/
|
||||
`ACL-HEAT@`/`ACL-WORD-ID`, 6 assertions — none of these six had ever been pushed-and-
|
||||
interpreted anywhere in this file, only their write-side siblings had), `ACL-INHERIT` as an
|
||||
*interpreted word* rather than only its underlying C function (2 assertions — the existing
|
||||
`test_acl_inherit` proved `acl_inherit_entry()` correct via a direct C call, but never
|
||||
exercised the FORTH-level stack-popping dispatch itself), and `ACL-INIT-PRIMITIVES` (4
|
||||
assertions — unpinned entries reset to permissive defaults, pinned entries left alone).
|
||||
|
||||
**A real bug in the new test itself, caught immediately by running it — worth recording as
|
||||
the caught mistake it is, not silently fixed.** First run: 27 passed, 2 failed (both
|
||||
`ACL-INHERIT`-as-word assertions). Root cause: the C implementation pops `dst` before `src`
|
||||
(`pop_xt(vm)` twice, top of stack first) — the test pushed `dst` then `src`, backwards. Fixed
|
||||
the test's push order (`src` then `dst`, matching what the C code actually expects), not the
|
||||
word itself — `ACL-INHERIT`'s own dispatch was correct throughout; this was a test-authoring
|
||||
mistake, caught by immediately booting and checking rather than assuming a clean compile
|
||||
meant a correct test. Re-run: **29 passed, 0 failed, 0 skipped, 0 errors.** Full amd64 build
|
||||
zero-warning-clean throughout. `logs/20260818-231204/` records the failing run (kept as
|
||||
evidence the bug was real and caught, not hidden), `logs/20260818-231403/` the fixed one.
|
||||
|
||||
Remaining clusters (Q48.16, inference-engine, physics freeze/diagnostic) not yet started —
|
||||
next up, one at a time, same process: read the C implementation, write tests matching that
|
||||
file's existing style, boot and verify before committing.
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
# Capsule Block Manifest — Auto-generated
|
||||
<!-- Generated by mkcapsule --manifest 2026-08-19T02:18:47Z -->
|
||||
<!-- Generated by mkcapsule --manifest 2026-08-19T03:14:02Z -->
|
||||
<!-- DO NOT EDIT — re-run mkcapsule --manifest to refresh. -->
|
||||
<!-- Hand-written justifications and immutability notes live -->
|
||||
<!-- in MANIFEST.md alongside this auto-generated index. -->
|
||||
|
||||
Binary file not shown.
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
@@ -404,6 +404,150 @@ static void test_acl_pin_blocks_shadow(VM *vm)
|
||||
ACL_ASSERT(found == orig, "original pinned entry still found after blocked shadow");
|
||||
}
|
||||
|
||||
/**
|
||||
* @brief Test 9 — ACL-MODE@/ACL-PINNED?/ACL-TTL@/ACL-ALLOW@/ACL-HEAT@/
|
||||
* ACL-WORD-ID read a word's ACL fields via the interpreter.
|
||||
*
|
||||
* Proof-covered field accessors (`proof/StarForth_ACL_*.thy`) that had no
|
||||
* interpreter-level POST coverage before this test — every other ACL test
|
||||
* in this file exercises the write accessors (`ACL-MODE!`/`ACL-TTL!`/
|
||||
* `ACL-ALLOW!`) or calls the underlying C functions directly, but never
|
||||
* pushed an xt and interpreted these six read words.
|
||||
*
|
||||
* Sets each field to a distinctive non-default value directly on a fresh
|
||||
* test word, then pushes its xt and interprets each accessor in turn,
|
||||
* checking the value returned on the stack.
|
||||
*
|
||||
* Expected assertions (6):
|
||||
* - ACL-MODE@ returns @c ACL_MODE_STRICT
|
||||
* - ACL-PINNED? returns -1 (true) for a pinned entry
|
||||
* - ACL-TTL@ returns 4242
|
||||
* - ACL-ALLOW@ returns 0 (false)
|
||||
* - ACL-HEAT@ returns the entry's @c execution_heat
|
||||
* - ACL-WORD-ID returns the entry's @c word_id
|
||||
*
|
||||
* @param vm VM instance.
|
||||
*/
|
||||
static void test_acl_read_accessors(VM *vm)
|
||||
{
|
||||
DictEntry *e = vm_create_word(vm, "__acl_read_test__", 18, NULL);
|
||||
if (!e) { tests_failed++; return; }
|
||||
|
||||
e->acl_mode = ACL_MODE_STRICT;
|
||||
e->acl_pinned = 1;
|
||||
e->acl_ttl = 4242;
|
||||
e->acl_allow = 0;
|
||||
e->execution_heat = 777;
|
||||
|
||||
vm_push(vm, (cell_t)(uintptr_t)e);
|
||||
vm_interpret(vm, "ACL-MODE@");
|
||||
vm->error = 0;
|
||||
ACL_ASSERT(vm_pop(vm) == (cell_t)ACL_MODE_STRICT, "ACL-MODE@ reads acl_mode");
|
||||
|
||||
vm_push(vm, (cell_t)(uintptr_t)e);
|
||||
vm_interpret(vm, "ACL-PINNED?");
|
||||
vm->error = 0;
|
||||
ACL_ASSERT(vm_pop(vm) == -1, "ACL-PINNED? reads acl_pinned as true");
|
||||
|
||||
vm_push(vm, (cell_t)(uintptr_t)e);
|
||||
vm_interpret(vm, "ACL-TTL@");
|
||||
vm->error = 0;
|
||||
ACL_ASSERT(vm_pop(vm) == 4242, "ACL-TTL@ reads acl_ttl");
|
||||
|
||||
vm_push(vm, (cell_t)(uintptr_t)e);
|
||||
vm_interpret(vm, "ACL-ALLOW@");
|
||||
vm->error = 0;
|
||||
ACL_ASSERT(vm_pop(vm) == 0, "ACL-ALLOW@ reads acl_allow as false");
|
||||
|
||||
vm_push(vm, (cell_t)(uintptr_t)e);
|
||||
vm_interpret(vm, "ACL-HEAT@");
|
||||
vm->error = 0;
|
||||
ACL_ASSERT(vm_pop(vm) == (cell_t)e->execution_heat, "ACL-HEAT@ reads execution_heat");
|
||||
|
||||
vm_push(vm, (cell_t)(uintptr_t)e);
|
||||
vm_interpret(vm, "ACL-WORD-ID");
|
||||
vm->error = 0;
|
||||
ACL_ASSERT(vm_pop(vm) == (cell_t)e->word_id, "ACL-WORD-ID reads word_id");
|
||||
}
|
||||
|
||||
/**
|
||||
* @brief Test 10 — ACL-INHERIT, as an interpreted FORTH word (src dst -- ).
|
||||
*
|
||||
* `test_acl_inherit` above already proves the underlying
|
||||
* @c acl_inherit_entry() C function is correct (Isabelle lemma
|
||||
* @c ACL_Inherit_Clears_Pin) by calling it directly. This test instead
|
||||
* exercises the FORTH-level dispatch path itself — pushing two xts and
|
||||
* interpreting "ACL-INHERIT" — which nothing in this file previously did,
|
||||
* so the word's own stack-popping/argument-order code was untested.
|
||||
*
|
||||
* Expected assertions (2):
|
||||
* - @c dst->acl_mode == ACL_MODE_STRICT after interpreting ACL-INHERIT
|
||||
* - @c dst->acl_pinned == 0 after interpreting ACL-INHERIT
|
||||
*
|
||||
* @param vm VM instance.
|
||||
*/
|
||||
static void test_acl_inherit_word_dispatch(VM *vm)
|
||||
{
|
||||
DictEntry *src = vm_create_word(vm, "__acl_inh_src__", 15, NULL);
|
||||
DictEntry *dst = vm_create_word(vm, "__acl_inh_dst__", 15, NULL);
|
||||
if (!src || !dst) { tests_failed++; return; }
|
||||
|
||||
src->acl_mode = ACL_MODE_STRICT;
|
||||
src->acl_pinned = 0;
|
||||
dst->acl_pinned = 1;
|
||||
dst->acl_mode = ACL_MODE_TTL;
|
||||
|
||||
vm_push(vm, (cell_t)(uintptr_t)src);
|
||||
vm_push(vm, (cell_t)(uintptr_t)dst);
|
||||
vm_interpret(vm, "ACL-INHERIT");
|
||||
vm->error = 0;
|
||||
|
||||
ACL_ASSERT(dst->acl_mode == ACL_MODE_STRICT, "ACL-INHERIT (word) copies acl_mode");
|
||||
ACL_ASSERT(dst->acl_pinned == 0, "ACL-INHERIT (word) clears acl_pinned");
|
||||
}
|
||||
|
||||
/**
|
||||
* @brief Test 11 — ACL-INIT-PRIMITIVES resets unpinned words, skips pinned ones.
|
||||
*
|
||||
* Creates two fresh words with non-default ACL state: one left unpinned,
|
||||
* one pinned. Interprets "ACL-INIT-PRIMITIVES" (which walks the entire
|
||||
* dictionary) and verifies the unpinned word was reset to the permissive
|
||||
* defaults (@c acl_ttl=0, @c acl_allow=1, @c acl_mode=ACL_MODE_TTL) while
|
||||
* the pinned word's deliberately-different state was left untouched.
|
||||
*
|
||||
* Expected assertions (4):
|
||||
* - unpinned word's @c acl_ttl reset to 0
|
||||
* - unpinned word's @c acl_allow reset to 1
|
||||
* - unpinned word's @c acl_mode reset to ACL_MODE_TTL
|
||||
* - pinned word's @c acl_ttl is NOT reset (still its original value)
|
||||
*
|
||||
* @param vm VM instance.
|
||||
*/
|
||||
static void test_acl_init_primitives(VM *vm)
|
||||
{
|
||||
DictEntry *unpinned = vm_create_word(vm, "__acl_initp_free__", 19, NULL);
|
||||
DictEntry *pinned = vm_create_word(vm, "__acl_initp_pin__", 18, NULL);
|
||||
if (!unpinned || !pinned) { tests_failed++; return; }
|
||||
|
||||
unpinned->acl_ttl = 555;
|
||||
unpinned->acl_allow = 0;
|
||||
unpinned->acl_mode = ACL_MODE_STRICT;
|
||||
unpinned->acl_pinned = 0;
|
||||
|
||||
pinned->acl_ttl = 555;
|
||||
pinned->acl_allow = 0;
|
||||
pinned->acl_mode = ACL_MODE_STRICT;
|
||||
pinned->acl_pinned = 1;
|
||||
|
||||
vm_interpret(vm, "ACL-INIT-PRIMITIVES");
|
||||
vm->error = 0;
|
||||
|
||||
ACL_ASSERT(unpinned->acl_ttl == 0, "ACL-INIT-PRIMITIVES resets unpinned acl_ttl");
|
||||
ACL_ASSERT(unpinned->acl_allow == 1, "ACL-INIT-PRIMITIVES resets unpinned acl_allow");
|
||||
ACL_ASSERT(unpinned->acl_mode == ACL_MODE_TTL, "ACL-INIT-PRIMITIVES resets unpinned acl_mode");
|
||||
ACL_ASSERT(pinned->acl_ttl == 555, "ACL-INIT-PRIMITIVES leaves pinned entry untouched");
|
||||
}
|
||||
|
||||
/* ------------------------------------------------------------------ */
|
||||
|
||||
/**
|
||||
@@ -411,7 +555,7 @@ static void test_acl_pin_blocks_shadow(VM *vm)
|
||||
*
|
||||
* Saves the current VM state (dsp, rsp, error, mode, emergency_console)
|
||||
* before each sub-test and restores it between tests so failures do not
|
||||
* cascade. Runs eight tests covering:
|
||||
* cascade. Runs eleven tests covering:
|
||||
*
|
||||
* 1. ACL-PIN one-way ratchet (4 assertions)
|
||||
* 2. ACL-INHERIT semantics (4 assertions)
|
||||
@@ -421,6 +565,9 @@ static void test_acl_pin_blocks_shadow(VM *vm)
|
||||
* 6. STRICT mode — TTL stays 0 (1 assertion or conditional skip)
|
||||
* 7. Adaptive TTL via ACL-TTL-COMPUTE (1 assertion or conditional skip)
|
||||
* 8. Pin blocks shadowing (3 assertions)
|
||||
* 9. Read accessors — ACL-MODE@/PINNED?/TTL@/ALLOW@/HEAT@/WORD-ID (6 assertions)
|
||||
* 10. ACL-INHERIT as an interpreted word, not just its C twin (2 assertions)
|
||||
* 11. ACL-INIT-PRIMITIVES resets unpinned, skips pinned (4 assertions)
|
||||
*
|
||||
* Tests that depend on @c ACL.4th being loaded are conditionally skipped
|
||||
* during bare POST (before @c ACL.4th runs) and counted as passes so the
|
||||
@@ -466,6 +613,15 @@ void run_acl_words_tests(VM *vm)
|
||||
test_acl_pin_blocks_shadow(vm);
|
||||
restore_vm_state(vm, saved_dsp, saved_rsp, 0, saved_mode);
|
||||
|
||||
test_acl_read_accessors(vm);
|
||||
restore_vm_state(vm, saved_dsp, saved_rsp, 0, saved_mode);
|
||||
|
||||
test_acl_inherit_word_dispatch(vm);
|
||||
restore_vm_state(vm, saved_dsp, saved_rsp, 0, saved_mode);
|
||||
|
||||
test_acl_init_primitives(vm);
|
||||
restore_vm_state(vm, saved_dsp, saved_rsp, 0, saved_mode);
|
||||
|
||||
vm->emergency_console = saved_ec;
|
||||
|
||||
print_module_summary("ACL Words", tests_passed, tests_failed, 0, 0);
|
||||
|
||||
Reference in New Issue
Block a user