nx_ledger_gate.nx source
↩ module page · 176 lines · 7937 B
1// nx_ledger_gate.nx -- F981 INDEPENDENT GATE for the sovereign double-entry ledger.
2// Imports the lib and proves its contract by BEHAVIOUR on a live seg-store plane.
3//
4// ★NON-VACUITY NOTE (stated plainly rather than dressed up): conservation is STRUCTURAL here --
5// one record carries BOTH legs (dr and cr), so a one-sided entry is INEXPRESSIBLE and a global
6// "drift == 0" assertion would be a TAUTOLOGY. Asserting it alone would be fake rigor. So the
7// measured tests are the ones that CAN fail:
8// * per-account balances summed across every account must total 0 -- this cross-checks the
9// per-account FILTER against global conservation; a broken match would break it.
10// * exact expected deltas (not merely non-zero) -- a sign flip or a wrong field would fail.
11// * every refusal path must refuse AND leave ZERO state change.
12// All assertions are DELTAS against a pre-read baseline, so the gate is re-runnable on a plane
13// that already holds history (append-only = prior runs persist by design).
14// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
15
16import "nx_ledger_lib.nx"
17
18const LG_PFX: i64 = 0
19
20func lg_puts(s: *u8) -> i64 {
21 var n: i64 = 0
22 while s[n] != (0 as u8) { n = n + 1 }
23 sys_write(1, s, n)
24 return 0
25}
26func lg_putn(v: i64) -> i64 {
27 let t: *u8 = sys_mmap(32)
28 var o: i64 = 0
29 var m: i64 = v
30 if m < 0 { t[o] = 45 as u8; o = o + 1; m = 0 - m }
31 let d: *u8 = sys_mmap(32)
32 var k: i64 = 0
33 if m == 0 { d[0] = 48 as u8; k = 1 }
34 while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
35 var i: i64 = 0
36 while i < k { t[o] = d[k - 1 - i]; o = o + 1; i = i + 1 }
37 sys_write(1, t, o)
38 return 0
39}
40// cnt[0]=pass cnt[1]=fail -- counters live in an mmap'd slot (no module-level mutable globals)
41func lg_ck(cnt: *i64, name: *u8, got: i64, want: i64) -> i64 {
42 if got == want {
43 cnt[0] = cnt[0] + 1
44 lg_puts(" PASS " as *u8); lg_puts(name); lg_puts(" = " as *u8); lg_putn(got); lg_puts("\n" as *u8)
45 return 1
46 }
47 cnt[1] = cnt[1] + 1
48 lg_puts(" FAIL " as *u8); lg_puts(name); lg_puts(" got " as *u8); lg_putn(got)
49 lg_puts(" want " as *u8); lg_putn(want); lg_puts("\n" as *u8)
50 return 0
51}
52
53// build a run-unique id: <tag><nonce>
54func lg_id(tag: *u8, nonce: i64, out: *u8) -> i64 {
55 var o: i64 = mt_catcopy(out, 0, tag)
56 o = mt_catn(out, o, nonce)
57 out[o] = 0 as u8
58 return o
59}
60
61func main(argc: i64, argv: *i64) -> i64 {
62 let pfx: *u8 = "knowledge/store/ledgergate-" as *u8
63 let nonce: i64 = sys_now_us()
64 let cnt: *i64 = sys_mmap(16) as *i64
65 cnt[0] = 0
66 cnt[1] = 0
67
68 // run-unique account names so deltas are clean even though the plane is append-only
69 let A: *u8 = sys_mmap(64)
70 let B: *u8 = sys_mmap(64)
71 let C: *u8 = sys_mmap(64)
72 lg_id("acctA" as *u8, nonce, A)
73 lg_id("acctB" as *u8, nonce, B)
74 lg_id("acctC" as *u8, nonce, C)
75
76 let i1: *u8 = sys_mmap(64)
77 let i2: *u8 = sys_mmap(64)
78 let i3: *u8 = sys_mmap(64)
79 let i4: *u8 = sys_mmap(64)
80 let i5: *u8 = sys_mmap(64)
81 lg_id("t1_" as *u8, nonce, i1)
82 lg_id("t2_" as *u8, nonce, i2)
83 lg_id("t3_" as *u8, nonce, i3)
84 lg_id("t4_" as *u8, nonce, i4)
85 lg_id("t5_" as *u8, nonce, i5)
86
87 lg_puts("NISHI-LEDGER-GATE (F981 double-entry, integer minor units)\n" as *u8)
88
89 // ---- T1/T2: a posted transfer moves EXACTLY the amount, both directions ----
90 led_xfer(pfx, i1, A, B, 10000, "posted" as *u8)
91 lg_ck(cnt, "T1 debit side bal(A) after A->B $100.00" as *u8, led_balance(pfx, A), 0 - 10000)
92 lg_ck(cnt, "T2 credit side bal(B) after A->B $100.00" as *u8, led_balance(pfx, B), 10000)
93
94 // ---- T3: second transfer, exact cumulative deltas (a sign flip or wrong field fails here) ----
95 led_xfer(pfx, i2, B, C, 2500, "posted" as *u8)
96 lg_ck(cnt, "T3 bal(B) after B->C $25.00" as *u8, led_balance(pfx, B), 7500)
97
98 // ---- T4: THE CROSS-CHECK -- per-account balances must sum to ZERO ----
99 // NOT structural: this validates the per-account filter against global conservation.
100 let sum3: i64 = led_balance(pfx, A) + led_balance(pfx, B) + led_balance(pfx, C)
101 lg_ck(cnt, "T4 sum of per-account balances (conservation)" as *u8, sum3, 0)
102
103 // ---- T5/T6: refusals must refuse AND write nothing ----
104 let bA: i64 = led_balance(pfx, A)
105 lg_ck(cnt, "T5 negative amount REFUSED" as *u8, led_xfer(pfx, i3, A, B, 0 - 500, "posted" as *u8), 0 - 1)
106 lg_ck(cnt, "T5b refusal left bal(A) untouched" as *u8, led_balance(pfx, A), bA)
107 lg_ck(cnt, "T6 self-transfer REFUSED" as *u8, led_xfer(pfx, i3, A, A, 500, "posted" as *u8), 0 - 2)
108 lg_ck(cnt, "T6b refusal left bal(A) untouched" as *u8, led_balance(pfx, A), bA)
109
110 // ---- T7/T8: two-phase pending reserves without moving posted money ----
111 let bB: i64 = led_balance(pfx, B)
112 let avB: i64 = led_available(pfx, B)
113 led_xfer(pfx, i3, B, C, 1000, "pending" as *u8)
114 lg_ck(cnt, "T7 pending does NOT move posted bal(B)" as *u8, led_balance(pfx, B), bB)
115 lg_ck(cnt, "T8 pending DOES reduce available(B) by $10.00" as *u8, led_available(pfx, B), avB - 1000)
116
117 // ---- T9: post the pending -> money moves, available unchanged from the reserved state ----
118 led_resolve(pfx, i3, "post" as *u8)
119 lg_ck(cnt, "T9 after post, bal(B) moved by the pending amount" as *u8, led_balance(pfx, B), bB - 1000)
120
121 // ---- T10/T11: a VOIDED pending must restore available and never touch posted ----
122 let bB2: i64 = led_balance(pfx, B)
123 let avB2: i64 = led_available(pfx, B)
124 led_xfer(pfx, i4, B, C, 3000, "pending" as *u8)
125 led_resolve(pfx, i4, "void" as *u8)
126 lg_ck(cnt, "T10 voided pending left posted bal(B) unchanged" as *u8, led_balance(pfx, B), bB2)
127 lg_ck(cnt, "T11 voided pending RESTORED available(B)" as *u8, led_available(pfx, B), avB2)
128
129 // ---- T12/T13: linked chain atomicity -- underfunded chain writes NOTHING ----
130 let ids: *i64 = sys_mmap(8 * 2) as *i64
131 let drs: *i64 = sys_mmap(8 * 2) as *i64
132 let crs: *i64 = sys_mmap(8 * 2) as *i64
133 let amts: *i64 = sys_mmap(8 * 2) as *i64
134 let c1: *u8 = sys_mmap(64)
135 let c2: *u8 = sys_mmap(64)
136 lg_id("c1_" as *u8, nonce, c1)
137 lg_id("c2_" as *u8, nonce, c2)
138 ids[0] = c1 as i64
139 ids[1] = c2 as i64
140 drs[0] = C as i64
141 drs[1] = C as i64
142 crs[0] = A as i64
143 crs[1] = B as i64
144 amts[0] = 500000
145 amts[1] = 500000
146 let bC: i64 = led_balance(pfx, C)
147 let bA2: i64 = led_balance(pfx, A)
148 lg_ck(cnt, "T12 underfunded chain REFUSED" as *u8, led_chain(pfx, ids, drs, crs, amts, 2, C), 0 - 3)
149 lg_ck(cnt, "T12b refused chain left bal(C) untouched (zero partial state)" as *u8, led_balance(pfx, C), bC)
150 lg_ck(cnt, "T12c refused chain left bal(A) untouched" as *u8, led_balance(pfx, A), bA2)
151
152 // ---- T13: a funded chain commits EVERY leg, conservation still holds ----
153 amts[0] = 100
154 amts[1] = 100
155 lg_ck(cnt, "T13 funded chain committed both legs" as *u8, led_chain(pfx, ids, drs, crs, amts, 2, "" as *u8), 2)
156 let sum4: i64 = led_balance(pfx, A) + led_balance(pfx, B) + led_balance(pfx, C)
157 lg_ck(cnt, "T13b conservation holds after the chain" as *u8, sum4, 0)
158
159 // ---- T14: chain leg validation refuses the WHOLE chain on one bad leg ----
160 amts[0] = 100
161 amts[1] = 0 - 5
162 let bC2: i64 = led_balance(pfx, C)
163 lg_ck(cnt, "T14 one bad leg REFUSES the whole chain" as *u8, led_chain(pfx, ids, drs, crs, amts, 2, "" as *u8), 0 - 1)
164 lg_ck(cnt, "T14b bad-leg refusal wrote NOTHING" as *u8, led_balance(pfx, C), bC2)
165
166 lg_puts("nx_ledger_gate: pass=" as *u8); lg_putn(cnt[0])
167 lg_puts(" fail=" as *u8); lg_putn(cnt[1]); lg_puts("\n" as *u8)
168 if cnt[1] == 0 {
169 lg_puts("F981 nx_ledger: VERDICT=GREEN (conservation cross-checked, refusals leave zero state)\n" as *u8)
170 sys_exit(0)
171 return 0
172 }
173 lg_puts("F981 nx_ledger: VERDICT=RED\n" as *u8)
174 sys_exit(1)
175 return 1
176}