nx_win_ledger_test.nx source
↩ module page · 126 lines · 7690 B
1// nx_win_ledger_test.nx -- PROVES the win-ledger is LOAD-BEARING.
2//
3// The net before the trapeze: a re-verify that has not been proven to FLIP a
4// real win to REFUTED on a deliberately-wrong expected is not a verifier at
5// all. So this gate exercises BOTH directions on a REAL recorded win:
6//
7// PROOF #1 (HOLDS): seed the real triangulated 64x64->128 multiplier win
8// -- repro = nx_mul_wide_test, expected "50006 50006"
9// (the gate's own known answer: ok==total==50006) --
10// re-verify MUST return HOLDS (the gate really re-runs
11// on the pinned compiler and emits the expected answer).
12//
13// PROOF #2 (REFUTED): seed the SAME real gate but with a deliberately-WRONG
14// expected ("99999 99999"). The gate still self-asserts
15// PASS (exit 0), but the ledger's stdout-match must FAIL
16// LOUD and flip the status to REFUTED. This proves the
17// ledger catches a wrong claim even when the underlying
18// gate is green.
19//
20// PROOF #3 (assumptions): record the egg-race / honest-latency superopt win
21// WITH its explicit, FALSIFIABLE assumptions[] -- including
22// "latency weights model real silicon" -- and assert the
23// assumptions round-trip out of the record. A bad
24// assumption must be catchable because it is written down.
25//
26// PROOF #4 (additive history): the ledger journaled both wins additively over
27// the hash-chained log AND the chain still verifies intact.
28//
29// Self-asserts; exit 0 = PROVEN. license_tier: ORIGINAL
30
31import "nx_win_ledger.nx"
32
33func _t_emit(s: *u8) -> i64 {
34 var n: i64 = 0
35 while s[n] != 0 as u8 { n = n + 1 }
36 sys_write(1, s, n)
37 return 0
38}
39
40func main() -> i64 {
41 let L: *NxWinLedger = nx_win_ledger_new()
42 if nx_win_ledger_is_valid(L) != 1 { _t_emit("FAIL: ledger invalid\n"); sys_exit(11); return 11 }
43
44 // ----- PROOF #1: real win re-verifies HOLDS -----------------------------
45 let win_mul: *NxWinRecord = nx_win_record_new(
46 "triangulated 64x64->128 multiplier: 3 independent legs agree on 50006 cases" as *u8,
47 "correctness (meet): gate-net vs 128-bit shift-add ref vs Freivalds mod-p" as *u8,
48 "why: a single bug would have to fool 3 independent algorithms; cited source_id=cardinal_2026-06-02_triangulation + nx_mul_wide.nx" as *u8,
49 "/mnt/c/Users/elder/nishi-core/nxc2/runtime/_hdl_build/nx_mul_wide_test.nx" as *u8,
50 "50006 50006" as *u8)
51 nx_win_record_add_assumption(win_mul,
52 "ASSUMPTION (falsifiable): the LCG-driven 50000 random pairs adequately sample the 64x64 input space" as *u8)
53
54 let st1: i64 = nx_win_ledger_record_and_verify(L, win_mul)
55 if st1 != WL_STATUS_HOLDS {
56 _t_emit("FAIL: real multiplier win did NOT re-verify HOLDS (re-gate or stdout-match broke)\n")
57 sys_exit(21); return 21
58 }
59 if win_mul.status != WL_STATUS_HOLDS { _t_emit("FAIL: record status not HOLDS after verify\n"); sys_exit(22); return 22 }
60 _t_emit("PROOF#1 OK: real multiplier win re-verified -> HOLDS (expected '50006 50006' found in re-run stdout)\n")
61
62 // ----- PROOF #2: deliberately-wrong expected FLIPS to REFUTED -----------
63 // Same real, green gate; only the expected known-answer is wrong on purpose.
64 let win_bad: *NxWinRecord = nx_win_record_new(
65 "SAME multiplier gate but a DELIBERATELY-WRONG claimed answer" as *u8,
66 "correctness (meet) -- but the recorded expected is a lie" as *u8,
67 "why: negative control -- proves the ledger catches a wrong claim even on a green gate" as *u8,
68 "/mnt/c/Users/elder/nishi-core/nxc2/runtime/_hdl_build/nx_mul_wide_test.nx" as *u8,
69 "99999 99999" as *u8)
70
71 let st2: i64 = nx_win_ledger_record_and_verify(L, win_bad)
72 if st2 != WL_STATUS_REFUTED {
73 _t_emit("FAIL: deliberately-wrong expected did NOT flip to REFUTED (re-verify is not load-bearing!)\n")
74 sys_exit(31); return 31
75 }
76 if win_bad.status != WL_STATUS_REFUTED { _t_emit("FAIL: bad record status not REFUTED\n"); sys_exit(32); return 32 }
77 _t_emit("PROOF#2 OK: deliberately-wrong expected '99999 99999' FAILED LOUD -> REFUTED (gate green, claim false)\n")
78
79 // ----- PROOF #3: egg-race win records its falsifiable assumptions[] ------
80 let win_egg: *NxWinRecord = nx_win_record_new(
81 "egg-race superopt: (mul x 2^k)->(shl x k) lowers the honest critical-path latency" as *u8,
82 "speed: fewer/cheaper gates on the critical path (honest latency metric)" as *u8,
83 "why: strength-reduction is sound (proven by nx_rule_soundness); cited source_id=cardinal_2026-06-02_invention_engine" as *u8,
84 "/mnt/c/Users/elder/nishi-core/nxc2/runtime/_hdl_build/nx_latency_metric_test.nx" as *u8,
85 "" as *u8)
86 // THE falsifiable assumption the operator named explicitly:
87 let a_idx1: i64 = nx_win_record_add_assumption(win_egg,
88 "ASSUMPTION (falsifiable): the latency weights model real silicon -- if a fab's gate delays differ, the 'win' may not hold on metal" as *u8)
89 let a_idx2: i64 = nx_win_record_add_assumption(win_egg,
90 "ASSUMPTION (falsifiable): the shift unit is not itself the critical path at this width" as *u8)
91 let a_idx3: i64 = nx_win_record_add_assumption(win_egg,
92 "ASSUMPTION (falsifiable): k is a compile-time constant power of two (else the rewrite does not apply)" as *u8)
93 if a_idx1 != 1 { _t_emit("FAIL: assumption #1 not stored at idx 1\n"); sys_exit(41); return 41 }
94 if a_idx3 != 3 { _t_emit("FAIL: assumption count wrong after 3 adds\n"); sys_exit(42); return 42 }
95 if win_egg.n_assumptions != 3 { _t_emit("FAIL: n_assumptions != 3\n"); sys_exit(43); return 43 }
96
97 // Round-trip: the falsifiable silicon assumption must be retrievable + intact.
98 let got: *u8 = nx_win_record_assumption(win_egg, 0)
99 if (got as i64) == 0 { _t_emit("FAIL: could not read back assumption 0\n"); sys_exit(44); return 44 }
100 if _wl_contains(got, "latency weights model real silicon" as *u8) != 1 {
101 _t_emit("FAIL: the falsifiable silicon assumption was not recorded verbatim\n")
102 sys_exit(45); return 45
103 }
104 // Record it additively (the assumptions ride along in the record; the win
105 // itself we leave UNVERIFIED-via-stdout here since its known answer is not
106 // asserted -- the POINT of #3 is the falsifiable assumptions list, and an
107 // empty expected must not masquerade as a HOLDS).
108 let seq_egg: i64 = nx_win_ledger_record(L, win_egg)
109 if seq_egg < 0 { _t_emit("FAIL: egg-race win did not record\n"); sys_exit(46); return 46 }
110 _t_emit("PROOF#3 OK: egg-race win recorded WITH 3 falsifiable assumptions (incl 'latency weights model real silicon')\n")
111
112 // ----- PROOF #4: additive hash-chained history is intact -----------------
113 // record_and_verify appended 2 entries each for win_mul + win_bad (record +
114 // verdict) = 4, plus 1 for win_egg = 5 total.
115 let cnt: i64 = nx_win_ledger_count(L)
116 if cnt != 5 { _t_emit("FAIL: journal entry count != 5\n"); sys_exit(51); return 51 }
117 // -1 = chain intact (no broken link).
118 if nx_journal_log_verify_chain(L.log) != -1 {
119 _t_emit("FAIL: win-ledger hash-chain is BROKEN\n"); sys_exit(52); return 52
120 }
121 _t_emit("PROOF#4 OK: 5 win records appended additively; hash-chain verifies intact\n")
122
123 _t_emit("ALL PROOFS PASS: win-ledger is LOAD-BEARING (HOLDS true wins, REFUTES false ones, records falsifiable assumptions)\n")
124 sys_exit(0)
125 return 0
126}