code wiki / (root) / nx_win_ledger_test.nx

nx_win_ledger_test.nx

buildroot/runtime/nx_win_ledger_test.nx

7690 B126 linesdepth 8pulls 8 transitivereach 0 importersview sourcekind gate/prooftopic win
docsdependenciesstructsconstsfunctions

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

nx_win_ledger.nx nx_win_ledger_test.nx

imports: nx_win_ledger.nx

imported by: nobody (leaf or entry point)

structs

none

consts

none

functions

33func _t_emit(s: *u8) -> i64
40func main() -> i64