nx_win_ledger_test.nx
buildroot/runtime/nx_win_ledger_test.nx
about
nx_win_ledger_test.nx -- PROVES the win-ledger is LOAD-BEARING.
The net before the trapeze: a re-verify that has not been proven to FLIP a
real win to REFUTED on a deliberately-wrong expected is not a verifier at
all. So this gate exercises BOTH directions on a REAL recorded win:
PROOF #1 (HOLDS): seed the real triangulated 64x64->128 multiplier win
-- repro = nx_mul_wide_test, expected "50006 50006"
(the gate's own known answer: ok==total==50006) --
re-verify MUST return HOLDS (the gate really re-runs
on the pinned compiler and emits the expected answer).
PROOF #2 (REFUTED): seed the SAME real gate but with a deliberately-WRONG
expected ("99999 99999"). The gate still self-asserts
PASS (exit 0), but the ledger's stdout-match must FAIL
LOUD and flip the status to REFUTED. This proves the
ledger catches a wrong claim even when the underlying
gate is green.
PROOF #3 (assumptions): record the egg-race / honest-latency superopt win
WITH its explicit, FALSIFIABLE assumptions[] -- including
"latency weights model real silicon" -- and assert the
assumptions round-trip out of the record. A bad
assumption must be catchable because it is written down.
PROOF #4 (additive history): the ledger journaled both wins additively over
the hash-chained log AND the chain still verifies intact.
Self-asserts; exit 0 = PROVEN. license_tier: ORIGINAL
dependencies 1 imports · 0 importers
imports: nx_win_ledger.nx
imported by: nobody (leaf or entry point)
call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown
structs
| none |
consts
| none |
functions
| 33 | func _t_emit(s: *u8) -> i64 called by 1: main |
| 40 | func main() -> i64 |