nx_ledger_scale_gate.nx source
↩ module page · 144 lines · 6045 B
1// nx_ledger_scale_gate.nx -- F981 SCALE RUNG: prove the per-account index returns the SAME answer as
2// the full-book scan, on a book big enough that the two paths genuinely differ in work done.
3//
4// The scale claim is only worth anything if the fast path is EQUIVALENT, so the full scan is kept as
5// the ORACLE and every assertion below compares fast-vs-oracle rather than fast-vs-a-number-I-typed.
6// A book of NOISE accounts is built around the account under test specifically so that the global
7// index is much longer than the per-account index -- if led_sums_fast were secretly still scanning
8// everything, or scanning the WRONG index, these would diverge.
9// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
10
11import "nx_ledger_lib.nx"
12
13const SC_NOISE: i64 = 12 // noise transfers surrounding the account under test (bisecting a measured ceiling)
14
15func sc_puts(s: *u8) -> i64 {
16 var n: i64 = 0
17 while s[n] != (0 as u8) { n = n + 1 }
18 sys_write(1, s, n)
19 return 0
20}
21func sc_putn(v: i64) -> i64 {
22 let t: *u8 = sys_mmap(32)
23 var o: i64 = 0
24 var m: i64 = v
25 if m < 0 { t[o] = 45 as u8; o = o + 1; m = 0 - m }
26 let d: *u8 = sys_mmap(32)
27 var k: i64 = 0
28 if m == 0 { d[0] = 48 as u8; k = 1 }
29 while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
30 var i: i64 = 0
31 while i < k { t[o] = d[k - 1 - i]; o = o + 1; i = i + 1 }
32 sys_write(1, t, o)
33 return 0
34}
35func sc_ck(cnt: *i64, name: *u8, got: i64, want: i64) -> i64 {
36 if got == want {
37 cnt[0] = cnt[0] + 1
38 sc_puts(" PASS " as *u8); sc_puts(name); sc_puts(" = " as *u8); sc_putn(got); sc_puts("\n" as *u8)
39 return 1
40 }
41 cnt[1] = cnt[1] + 1
42 sc_puts(" FAIL " as *u8); sc_puts(name); sc_puts(" got " as *u8); sc_putn(got)
43 sc_puts(" want " as *u8); sc_putn(want); sc_puts("\n" as *u8)
44 return 0
45}
46func sc_id(tag: *u8, nonce: i64, n: i64, out: *u8) -> i64 {
47 var o: i64 = mt_catcopy(out, 0, tag)
48 o = mt_catn(out, o, nonce)
49 out[o] = 95 as u8
50 o = o + 1
51 o = mt_catn(out, o, n)
52 out[o] = 0 as u8
53 return o
54}
55
56func main(argc: i64, argv: *i64) -> i64 {
57 let pfx: *u8 = "knowledge/store/ledscale-" as *u8
58 let nonce: i64 = sys_now_us()
59 let cnt: *i64 = sys_mmap(16) as *i64
60 cnt[0] = 0
61 cnt[1] = 0
62
63 sc_puts("NISHI-LEDGER-SCALE-GATE (per-account index vs full-book scan; full scan is the ORACLE)\n" as *u8)
64
65 let tgt: *u8 = sys_mmap(64)
66 let ctr: *u8 = sys_mmap(64)
67 sc_id("target_" as *u8, nonce, 0, tgt)
68 sc_id("counter_" as *u8, nonce, 0, ctr)
69
70 // ---- build a NOISY book: many transfers that do NOT touch the target account ----
71 let na: *u8 = sys_mmap(64)
72 let nb: *u8 = sys_mmap(64)
73 let nid: *u8 = sys_mmap(64)
74 var i: i64 = 0
75 while i < SC_NOISE {
76 sc_id("noiseA_" as *u8, nonce, i, na)
77 sc_id("noiseB_" as *u8, nonce, i, nb)
78 sc_id("nx_" as *u8, nonce, i, nid)
79 led_xfer(pfx, nid, na, nb, 100 + i, "posted" as *u8)
80 i = i + 1
81 }
82
83 // ---- three transfers that DO touch the target ----
84 let t1: *u8 = sys_mmap(64)
85 let t2: *u8 = sys_mmap(64)
86 let t3: *u8 = sys_mmap(64)
87 sc_id("tgt_" as *u8, nonce, 1, t1)
88 sc_id("tgt_" as *u8, nonce, 2, t2)
89 sc_id("tgt_" as *u8, nonce, 3, t3)
90 led_xfer(pfx, t1, ctr, tgt, 50000, "posted" as *u8)
91 led_xfer(pfx, t2, tgt, ctr, 12500, "posted" as *u8)
92 led_xfer(pfx, t3, ctr, tgt, 2500, "pending" as *u8)
93
94 let slow: *i64 = sys_mmap(8 * 4) as *i64
95 let fast: *i64 = sys_mmap(8 * 4) as *i64
96
97 // ---- S1..S4: fast path agrees with the oracle on EVERY accumulator ----
98 led_sums(pfx, tgt, slow)
99 led_sums_fast(pfx, tgt, fast)
100 sc_ck(cnt, "S1 posted debits fast == full-scan oracle" as *u8, fast[0], slow[0])
101 sc_ck(cnt, "S2 posted credits fast == full-scan oracle" as *u8, fast[1], slow[1])
102 sc_ck(cnt, "S3 reserved debits fast == oracle" as *u8, fast[2], slow[2])
103 sc_ck(cnt, "S4 reserved credits fast == oracle" as *u8, fast[3], slow[3])
104
105 // ---- S5: and the values are the RIGHT ones, not merely equal-and-both-wrong ----
106 sc_ck(cnt, "S5 target posted credits = $500.00" as *u8, fast[1], 50000)
107 sc_ck(cnt, "S6 target posted debits = $125.00" as *u8, fast[0], 12500)
108 sc_ck(cnt, "S7 target reserved credits = $25.00 (unresolved pending)" as *u8, fast[3], 2500)
109
110 // ---- S8: the counterparty also agrees (index joins BOTH sides of a transfer) ----
111 led_sums(pfx, ctr, slow)
112 led_sums_fast(pfx, ctr, fast)
113 sc_ck(cnt, "S8 counterparty debits fast == oracle" as *u8, fast[0], slow[0])
114 sc_ck(cnt, "S9 counterparty credits fast == oracle" as *u8, fast[1], slow[1])
115
116 // ---- S10: NON-VACUITY. The noise really is in the book, so the two paths did different work.
117 // If the global index were the same length as the target's index this test would prove nothing.
118 let allsums: *i64 = sys_mmap(8 * 4) as *i64
119 led_sums(pfx, "" as *u8, allsums)
120 var noisy: i64 = 0
121 if allsums[0] > 50000 { noisy = 1 }
122 sc_ck(cnt, "S10 the book really is noisy (global scan >> target scan)" as *u8, noisy, 1)
123
124 // ---- S11: an account with NO transfers reads zero on the fast path (empty index, not a crash) ----
125 let ghost: *u8 = sys_mmap(64)
126 sc_id("ghost_" as *u8, nonce, 0, ghost)
127 led_sums_fast(pfx, ghost, fast)
128 sc_ck(cnt, "S11 untouched account reads zero on the fast path" as *u8, fast[0] + fast[1], 0)
129
130 // ---- S12: balances computed through the normal API still conserve ----
131 sc_ck(cnt, "S12 target + counterparty balances still sum to zero" as *u8,
132 led_balance(pfx, tgt) + led_balance(pfx, ctr), 0)
133
134 sc_puts("nx_ledger_scale_gate: pass=" as *u8); sc_putn(cnt[0])
135 sc_puts(" fail=" as *u8); sc_putn(cnt[1]); sc_puts("\n" as *u8)
136 if cnt[1] == 0 {
137 sc_puts("F981-SCALE: VERDICT=GREEN (per-account index equivalent to the full scan on a noisy book)\n" as *u8)
138 sys_exit(0)
139 return 0
140 }
141 sc_puts("F981-SCALE: VERDICT=RED\n" as *u8)
142 sys_exit(1)
143 return 1
144}