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)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main nx_win_ledger_new sys_mmap nx_blob_store_new sys_mmap ↻ nx_journal_log_new sys_mmap ↻ nx_win_ledger_is_valid nx_blob_store_is_valid nx_journal_log_is_valid _t_emit nx_win_record_new sys_mmap ↻ nx_win_record_add_assumpti nx_win_record_is_valid nx_win_ledger_record_and_v nx_win_ledger_is_valid ↻ nx_win_record_is_valid ↻ nx_win_ledger_record nx_win_ledger_is_valid ↻ nx_win_record_is_valid ↻ _wl_strlen nx_journal_log_append nx_journal_log_is_valid ↻ nx_blob_hash_new sys_mmap ↻ nx_blob_store_put nx_blob_store_is_valid ↻ _hash_bytes_to_struct sys_mmap ↻ sha256_digest _load_i64_le _find_entry_idx _entry_hash_eq _alloc_entry sys_mmap ↻ sys_mmap ↻ _journal_entry_hash sys_mmap ↻ _journal_canonicalize

structs

none

consts

none

functions

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