Add exact-equality Hermes ledger self-audit -- FABRIC-3.6.md task 2.6
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Sonnet 5
parent
d11eb2e5db
commit
313ffc89e6
+17
-1
@@ -665,8 +665,24 @@ Hestia; headless policy intact.
|
||||
`disk/artemis.img` and `disk/thumbdrives/zuse-thumb-ident.img` were restored via
|
||||
`git checkout --` before each ISA per the task 0.0 finding. That discarded a pre-existing
|
||||
uncommitted modification to `disk/artemis.img` that was present at session start.
|
||||
- [ ] **2.6** — Self-audit: `held == pulled − returned − consumed`, **epsilon zero**. *Check:*
|
||||
- [x] **2.6** — Self-audit: `held == pulled − returned − consumed`, **epsilon zero**. *Check:*
|
||||
holds across the cycle; **deliberately corrupt a counter → audit fires on the first unit**.
|
||||
2026-09-20 · `logs/20260920-204658/amd64/`, `logs/20260920-205410/aarch64/`,
|
||||
`logs/20260920-205834/riscv64/` — all reach `[zuse@Hera] ok>`, zero `UNKNOWN WORD`,
|
||||
`dict_hash` triple unmoved and identical across ISAs; all print `PASS`,
|
||||
`audit_failures=0`, `decay_consumed=352`.
|
||||
|
||||
Added `sk_hermes_audit_values()` (pure exact-equality predicate, no tolerance),
|
||||
`sk_hermes_audit()` (live ledger, O(1), prints and counts a failure) and
|
||||
`sk_hermes_audit_failure_count()`. The live audit runs at the end of every successful
|
||||
alloc, release and decay (§XXXVII.4: no cadence decision needed). Corruption is tested
|
||||
on a *copy* of the ledger, +1 unit on each of the four counters in turn, so live state is
|
||||
never corrupted; each is caught by the predicate while the uncorrupted values pass. The
|
||||
live audit stayed silent through both alloc/decay/release cycles.
|
||||
|
||||
Limit, stated: the corruption proof exercises the predicate, not the wiring of the live
|
||||
audit's failure branch (that branch never executed). Task 2.8's scan cross-check is the
|
||||
independent check on the counters themselves.
|
||||
- [ ] **2.7** — **Stage B proof** (§XXXIV.3 as corrected by §XXXIX.4): alloc/free cycle
|
||||
verifying **(a)** the ledger and **(b)** `stadium_conserved()` before and after.
|
||||
*Check:* both true, all three arches. **`fleet_conserved` is not evidence here** — it
|
||||
|
||||
@@ -244,6 +244,25 @@ void sk_hermes_ledger(uint64_t *held, uint64_t *pulled, uint64_t *returned, uint
|
||||
*/
|
||||
int sk_hermes_decay(SkHermesMessage *msg);
|
||||
|
||||
/*
|
||||
* Task 2.6 (item 28): the self-audit, epsilon zero (SXXXVII.3).
|
||||
*
|
||||
* sk_hermes_audit_values - pure predicate: nonzero iff
|
||||
* held == pulled - returned - consumed exactly. Separate from the live
|
||||
* ledger so the check can be exercised with deliberately corrupted values
|
||||
* without mutating real state.
|
||||
*
|
||||
* sk_hermes_audit - checks the live ledger (O(1), SXXXVII.4); on failure
|
||||
* prints a console line and bumps a failure count. Called at the end of
|
||||
* every successful mutation: alloc, release, decay.
|
||||
*
|
||||
* sk_hermes_audit_failure_count - cumulative failures seen by the live
|
||||
* audit; must be 0 in a healthy kernel.
|
||||
*/
|
||||
int sk_hermes_audit_values(uint64_t held, uint64_t pulled, uint64_t returned, uint64_t consumed);
|
||||
int sk_hermes_audit(void);
|
||||
uint64_t sk_hermes_audit_failure_count(void);
|
||||
|
||||
#endif /* __STARKERNEL__ */
|
||||
|
||||
#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
@@ -951,7 +951,20 @@ static void kernel_main_deep(BootInfo *boot_info) {
|
||||
if (held4 != pulled4 - returned4 - consumed4) ok = 0;
|
||||
if (stadium_reservoir_peek(alloc_test_id) != reservoir0 - decay_expected) ok = 0;
|
||||
|
||||
/* Task 2.6: the live audit never fired across both cycles,
|
||||
* and a ONE-unit corruption of each counter in turn (on a
|
||||
* copy -- live state untouched) is caught by the pure
|
||||
* predicate, while the uncorrupted values pass it. */
|
||||
if (sk_hermes_audit_failure_count() != 0) ok = 0;
|
||||
if (!sk_hermes_audit()) ok = 0;
|
||||
if (!sk_hermes_audit_values(held4, pulled4, returned4, consumed4)) ok = 0;
|
||||
if (sk_hermes_audit_values(held4 + 1, pulled4, returned4, consumed4)) ok = 0;
|
||||
if (sk_hermes_audit_values(held4, pulled4 + 1, returned4, consumed4)) ok = 0;
|
||||
if (sk_hermes_audit_values(held4, pulled4, returned4 + 1, consumed4)) ok = 0;
|
||||
if (sk_hermes_audit_values(held4, pulled4, returned4, consumed4 + 1)) ok = 0;
|
||||
|
||||
console_println(ok ? "PASS" : "FAIL");
|
||||
print_uint(" audit_failures=", sk_hermes_audit_failure_count());
|
||||
print_uint(" decay_consumed=", decay_expected);
|
||||
print_uint(" reservoir0=", reservoir0);
|
||||
print_uint(" Q_SLOT=", SK_HERMES_Q_SLOT);
|
||||
|
||||
@@ -48,6 +48,7 @@
|
||||
#include "starkernel/vm/kernel_hermes.h"
|
||||
#include "starkernel/vm/stadium.h"
|
||||
#include "starkernel/q48_16.h"
|
||||
#include "console.h"
|
||||
|
||||
static SkHermesMessage sk_hermes_msgs[SK_HERMES_MSG_MAX];
|
||||
|
||||
@@ -66,6 +67,27 @@ void sk_hermes_ledger(uint64_t *held, uint64_t *pulled, uint64_t *returned, uint
|
||||
if (consumed) *consumed = sk_hermes_consumed;
|
||||
}
|
||||
|
||||
int sk_hermes_audit_values(uint64_t held, uint64_t pulled, uint64_t returned, uint64_t consumed) {
|
||||
/* Epsilon zero (SXXXVII.3): exact integer equality, no tolerance. */
|
||||
return held == pulled - returned - consumed;
|
||||
}
|
||||
|
||||
static uint64_t sk_hermes_audit_failures = 0;
|
||||
|
||||
int sk_hermes_audit(void) {
|
||||
int ok = sk_hermes_audit_values(sk_hermes_held, sk_hermes_pulled,
|
||||
sk_hermes_returned, sk_hermes_consumed);
|
||||
if (!ok) {
|
||||
sk_hermes_audit_failures++;
|
||||
console_println("Kernel-Hermes AUDIT FAILURE: held != pulled - returned - consumed");
|
||||
}
|
||||
return ok;
|
||||
}
|
||||
|
||||
uint64_t sk_hermes_audit_failure_count(void) {
|
||||
return sk_hermes_audit_failures;
|
||||
}
|
||||
|
||||
static int sk_hermes_find_free_slot(void) {
|
||||
int i;
|
||||
for (i = 0; i < SK_HERMES_MSG_MAX; i++) {
|
||||
@@ -135,6 +157,7 @@ int sk_hermes_alloc(VMUuid vm_id, SkHermesMessage **out_msg) {
|
||||
* once every refusal path above has already returned. */
|
||||
sk_hermes_held += pulled;
|
||||
sk_hermes_pulled += pulled;
|
||||
sk_hermes_audit();
|
||||
|
||||
return 0;
|
||||
}
|
||||
@@ -176,6 +199,7 @@ int sk_hermes_release(SkHermesMessage *msg) {
|
||||
if (rc == 0) {
|
||||
sk_hermes_held -= remaining;
|
||||
sk_hermes_returned += remaining;
|
||||
sk_hermes_audit();
|
||||
}
|
||||
|
||||
memset(msg, 0, sizeof(*msg));
|
||||
@@ -198,6 +222,7 @@ int sk_hermes_decay(SkHermesMessage *msg) {
|
||||
* pays for it). SXXXVII.3: decay's delta is exact and in hand here. */
|
||||
sk_hermes_consumed += before - after;
|
||||
sk_hermes_held -= before - after;
|
||||
sk_hermes_audit();
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user