Add diagnostic scan cross-check of the Hermes counters -- FABRIC-3.6.md task 2.8
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Sonnet 5
parent
2a2bf6eb35
commit
feace42397
+18
-1
@@ -712,8 +712,25 @@ Hestia; headless policy intact.
|
|||||||
|
|
||||||
**Phase 2 gate: passed** (2.7 holds on all three arches). Remaining Phase 2 work is 2.8
|
**Phase 2 gate: passed** (2.7 holds on all three arches). Remaining Phase 2 work is 2.8
|
||||||
(diagnostic scan cross-check).
|
(diagnostic scan cross-check).
|
||||||
- [ ] **2.8** — Scan-based cross-check of the counters, diagnostics only, off the hot path
|
- [x] **2.8** — Scan-based cross-check of the counters, diagnostics only, off the hot path
|
||||||
(§XXXVII.4). *Check:* scan agrees with counters.
|
(§XXXVII.4). *Check:* scan agrees with counters.
|
||||||
|
2026-09-21 · `logs/20260921-083638/amd64/`, `logs/20260921-083950/aarch64/`,
|
||||||
|
`logs/20260921-084314/riscv64/` — all print `Scan cross-check (counters vs arena): PASS`
|
||||||
|
with identical `scan_held_before_decay=8192`, `scan_held_after_decay=8148`; Stage B and
|
||||||
|
the main self-test still `PASS`, `audit_failures=0`, zero `UNKNOWN WORD`, `dict_hash`
|
||||||
|
triple unmoved and identical across ISAs.
|
||||||
|
|
||||||
|
Added `sk_hermes_scan_held()` (walks the arena, sums live Stadium-cell heat of in-use
|
||||||
|
messages, reports the live count) and `sk_hermes_scan_check()` (scan == `held`, exact).
|
||||||
|
Called only from the self-test, never from alloc/release/decay. The check runs at rest
|
||||||
|
(0 live), mid-hold (4 live, 4×2048 = 8192), after decay (8148 = 8192 − 4×11) and after
|
||||||
|
release (0), with a vacuity guard (non-zero mid-hold, strictly less after decay).
|
||||||
|
|
||||||
|
Limit, stated: the scan reads the same Stadium cells the counters were derived from, so
|
||||||
|
it verifies the counters against the arena, not the Stadium cells against ground truth;
|
||||||
|
the latter is `stadium_conserved()`'s job (2.7).
|
||||||
|
|
||||||
|
**Phase 2 is complete (2.1–2.8).** Phase 3 remains blocked on B1, B2, B4.
|
||||||
|
|
||||||
## Phase 3 — Cutover — **BLOCKED**
|
## Phase 3 — Cutover — **BLOCKED**
|
||||||
|
|
||||||
|
|||||||
@@ -264,6 +264,21 @@ int sk_hermes_audit_values(uint64_t held, uint64_t pulled, uint64_t returned, ui
|
|||||||
int sk_hermes_audit(void);
|
int sk_hermes_audit(void);
|
||||||
uint64_t sk_hermes_audit_failure_count(void);
|
uint64_t sk_hermes_audit_failure_count(void);
|
||||||
|
|
||||||
|
/*
|
||||||
|
* Task 2.8 (item 28), SXXXVII.4: the scan that verifies the counters
|
||||||
|
* themselves. DIAGNOSTIC ONLY -- O(SK_HERMES_MSG_MAX), never called from
|
||||||
|
* alloc/release/decay.
|
||||||
|
*
|
||||||
|
* sk_hermes_scan_held - walks the message arena and sums the live Stadium
|
||||||
|
* cell heat of every in-use message (the ground truth `held` claims to
|
||||||
|
* track). Sets *live_count (may be NULL) to the messages counted.
|
||||||
|
*
|
||||||
|
* sk_hermes_scan_check - nonzero iff the scan sum equals the `held`
|
||||||
|
* counter exactly.
|
||||||
|
*/
|
||||||
|
uint64_t sk_hermes_scan_held(size_t *live_count);
|
||||||
|
int sk_hermes_scan_check(void);
|
||||||
|
|
||||||
#endif /* __STARKERNEL__ */
|
#endif /* __STARKERNEL__ */
|
||||||
|
|
||||||
#endif /* STARKERNEL_VM_KERNEL_HERMES_H */
|
#endif /* STARKERNEL_VM_KERNEL_HERMES_H */
|
||||||
|
|||||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
@@ -982,6 +982,34 @@ static void kernel_main_deep(BootInfo *boot_info) {
|
|||||||
if (!stadium_conserved(alloc_test_id)) sb = 0; /* after release */
|
if (!stadium_conserved(alloc_test_id)) sb = 0; /* after release */
|
||||||
sk_hermes_ledger(&h, &p_, &r, &c);
|
sk_hermes_ledger(&h, &p_, &r, &c);
|
||||||
if (h != held0 || !sk_hermes_audit_values(h, p_, r, c)) sb = 0;
|
if (h != held0 || !sk_hermes_audit_values(h, p_, r, c)) sb = 0;
|
||||||
|
/* Task 2.8: scan cross-check of the counters -- mid-hold
|
||||||
|
* and after decay it must equal `held` and be non-zero
|
||||||
|
* (vacuity guard); after release it must be zero. The
|
||||||
|
* mid-hold/decay points are re-established here on a
|
||||||
|
* short fresh hold. */
|
||||||
|
{
|
||||||
|
size_t live = 0, live2 = 0;
|
||||||
|
uint64_t s1, s2;
|
||||||
|
int sc = 1;
|
||||||
|
uint64_t k = 0;
|
||||||
|
if (!sk_hermes_scan_check() || sk_hermes_scan_held(&live) != 0 || live != 0) sc = 0;
|
||||||
|
while (k < 4 && sk_hermes_alloc(alloc_test_id, &msg) == 0) msgs[k++] = msg;
|
||||||
|
if (k != 4) sc = 0;
|
||||||
|
s1 = sk_hermes_scan_held(&live);
|
||||||
|
sk_hermes_ledger(&h, &p_, &r, &c);
|
||||||
|
if (s1 == 0 || live != 4 || s1 != h || !sk_hermes_scan_check()) sc = 0;
|
||||||
|
for (i = 0; i < k; i++) if (sk_hermes_decay(msgs[i]) != 0) sc = 0;
|
||||||
|
s2 = sk_hermes_scan_held(&live2);
|
||||||
|
sk_hermes_ledger(&h, &p_, &r, &c);
|
||||||
|
if (s2 >= s1 || s2 != h || live2 != 4 || !sk_hermes_scan_check()) sc = 0;
|
||||||
|
for (i = 0; i < k; i++) if (sk_hermes_release(msgs[i]) != 0) sc = 0;
|
||||||
|
if (sk_hermes_scan_held(&live) != 0 || live != 0 || !sk_hermes_scan_check()) sc = 0;
|
||||||
|
console_puts("Scan cross-check (counters vs arena): ");
|
||||||
|
console_println(sc ? "PASS" : "FAIL");
|
||||||
|
print_uint(" scan_held_before_decay=", s1);
|
||||||
|
print_uint(" scan_held_after_decay=", s2);
|
||||||
|
if (!sc) sb = 0;
|
||||||
|
}
|
||||||
console_puts("Stage B (ledger + stadium_conserved): ");
|
console_puts("Stage B (ledger + stadium_conserved): ");
|
||||||
console_println(sb ? "PASS" : "FAIL");
|
console_println(sb ? "PASS" : "FAIL");
|
||||||
print_uint(" vm_consumed=", stadium_consumed_peek(alloc_test_id));
|
print_uint(" vm_consumed=", stadium_consumed_peek(alloc_test_id));
|
||||||
|
|||||||
@@ -88,6 +88,24 @@ uint64_t sk_hermes_audit_failure_count(void) {
|
|||||||
return sk_hermes_audit_failures;
|
return sk_hermes_audit_failures;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
uint64_t sk_hermes_scan_held(size_t *live_count) {
|
||||||
|
uint64_t sum = 0;
|
||||||
|
size_t n = 0;
|
||||||
|
int i;
|
||||||
|
|
||||||
|
for (i = 0; i < SK_HERMES_MSG_MAX; i++) {
|
||||||
|
if (!sk_hermes_msgs[i].in_use || sk_hermes_msgs[i].stadium_cell < 0) continue;
|
||||||
|
sum += stadium_cells()[sk_hermes_msgs[i].stadium_cell].header.heat;
|
||||||
|
n++;
|
||||||
|
}
|
||||||
|
if (live_count) *live_count = n;
|
||||||
|
return sum;
|
||||||
|
}
|
||||||
|
|
||||||
|
int sk_hermes_scan_check(void) {
|
||||||
|
return sk_hermes_scan_held((size_t *)0) == sk_hermes_held;
|
||||||
|
}
|
||||||
|
|
||||||
static int sk_hermes_find_free_slot(void) {
|
static int sk_hermes_find_free_slot(void) {
|
||||||
int i;
|
int i;
|
||||||
for (i = 0; i < SK_HERMES_MSG_MAX; i++) {
|
for (i = 0; i < SK_HERMES_MSG_MAX; i++) {
|
||||||
|
|||||||
Reference in New Issue
Block a user