code wiki / (root) / nx_ledger_trust_equiv_gate.nx

nx_ledger_trust_equiv_gate.nx source

↩ module page · 161 lines · 7180 B

1// nx_ledger_trust_equiv_gate.nx -- F997 STEP 1: BEHAVIOUR-EQUIVALENCE PROOF, nx_ledger vs nx_trust. 2// 3// F997 wants nx_trust (IOLTA, RPC 1.15, LIVE and gate-proven 7/7) re-based onto the new nx_ledger 4// primitive. Rewriting a working compliance organ on faith is exactly how you break a bar-audit 5// surface. So this gate does the SAFE half first: it drives the SAME scenario through BOTH 6// implementations and asserts they agree, value for value. nx_trust is NOT modified. 7// 8// If every assertion holds, the re-base is proven safe and F997's real edit becomes mechanical. 9// If any fails, we have found a genuine semantic gap in the primitive BEFORE trusting money to it. 10// (This is the D001 organ-dedup behaviour-equivalence discipline applied to money.) 11// 12// MAPPING (trust semantics -> double-entry): 13// deposit $X for client C == transfer bank -> client:C (credits C) 14// disburse $X for client C == transfer client:C -> operating (debits C) 15// client balance == led_balance(client) = credits - debits (same custodial sense) 16// RPC 1.15 no-overdraw == led_can_fund(client, X) 17// three-way reconciliation == sum(per-client balances) == trust account total 18// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0 19 20import "nx_trust_lib.nx" 21import "nx_ledger_lib.nx" 22 23func eq_puts(s: *u8) -> i64 { 24 var n: i64 = 0 25 while s[n] != (0 as u8) { n = n + 1 } 26 sys_write(1, s, n) 27 return 0 28} 29func eq_putn(v: i64) -> i64 { 30 let t: *u8 = sys_mmap(32) 31 var o: i64 = 0 32 var m: i64 = v 33 if m < 0 { t[o] = 45 as u8; o = o + 1; m = 0 - m } 34 let d: *u8 = sys_mmap(32) 35 var k: i64 = 0 36 if m == 0 { d[0] = 48 as u8; k = 1 } 37 while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 } 38 var i: i64 = 0 39 while i < k { t[o] = d[k - 1 - i]; o = o + 1; i = i + 1 } 40 sys_write(1, t, o) 41 return 0 42} 43// assert the TWO implementations agree, and that they agree on the EXPECTED value 44func eq_ck(cnt: *i64, name: *u8, trust_v: i64, ledger_v: i64, want: i64) -> i64 { 45 if trust_v == ledger_v { 46 if trust_v == want { 47 cnt[0] = cnt[0] + 1 48 eq_puts(" PASS " as *u8); eq_puts(name) 49 eq_puts(" -- trust==ledger==" as *u8); eq_putn(trust_v); eq_puts("\n" as *u8) 50 return 1 51 } 52 } 53 cnt[1] = cnt[1] + 1 54 eq_puts(" FAIL " as *u8); eq_puts(name) 55 eq_puts(" trust=" as *u8); eq_putn(trust_v) 56 eq_puts(" ledger=" as *u8); eq_putn(ledger_v) 57 eq_puts(" want=" as *u8); eq_putn(want); eq_puts("\n" as *u8) 58 return 0 59} 60func eq_id(tag: *u8, nonce: i64, out: *u8) -> i64 { 61 var o: i64 = mt_catcopy(out, 0, tag) 62 o = mt_catn(out, o, nonce) 63 out[o] = 0 as u8 64 return o 65} 66 67func main(argc: i64, argv: *i64) -> i64 { 68 let tp: *u8 = "knowledge/store/equivtrust-" as *u8 69 let lp: *u8 = "knowledge/store/equivledg-" as *u8 70 let nonce: i64 = sys_now_us() 71 let cnt: *i64 = sys_mmap(16) as *i64 72 cnt[0] = 0 73 cnt[1] = 0 74 75 let ca: *u8 = sys_mmap(64) 76 let cb: *u8 = sys_mmap(64) 77 let bank: *u8 = sys_mmap(64) 78 let oper: *u8 = sys_mmap(64) 79 eq_id("ClientA" as *u8, nonce, ca) 80 eq_id("ClientB" as *u8, nonce, cb) 81 eq_id("bank" as *u8, nonce, bank) 82 eq_id("operating" as *u8, nonce, oper) 83 84 let x1: *u8 = sys_mmap(64) 85 let x2: *u8 = sys_mmap(64) 86 let x3: *u8 = sys_mmap(64) 87 eq_id("dep_a_" as *u8, nonce, x1) 88 eq_id("dep_b_" as *u8, nonce, x2) 89 eq_id("dis_a_" as *u8, nonce, x3) 90 91 let m: *u8 = "M-EQUIV" as *u8 92 93 eq_puts("NISHI-LEDGER-TRUST-EQUIV (F997 step 1: is the primitive faithful to the live IOLTA organ?)\n" as *u8) 94 95 // ---- deposit $700.00 for ClientA in BOTH ---- 96 trust_put(tp, ca, 1, m, "deposit" as *u8, 70000) 97 led_xfer(lp, x1, bank, ca, 70000, "posted" as *u8) 98 eq_ck(cnt, "E1 ClientA balance after $700.00 deposit" as *u8, 99 trust_balance(tp, ca), led_balance(lp, ca), 70000) 100 101 // ---- deposit $500.00 for ClientB in BOTH ---- 102 trust_put(tp, cb, 1, m, "deposit" as *u8, 50000) 103 led_xfer(lp, x2, bank, cb, 50000, "posted" as *u8) 104 eq_ck(cnt, "E2 ClientB balance after $500.00 deposit" as *u8, 105 trust_balance(tp, cb), led_balance(lp, cb), 50000) 106 107 // ---- E3 three-way leg: sum of client ledgers == account total ($1200.00) ---- 108 let t_total: i64 = trust_balance(tp, ca) + trust_balance(tp, cb) 109 let l_total: i64 = led_balance(lp, ca) + led_balance(lp, cb) 110 eq_ck(cnt, "E3 trust ACCOUNT TOTAL (sum of client ledgers)" as *u8, t_total, l_total, 120000) 111 112 // ---- E4 RPC 1.15 NO-OVERDRAW: $2000.00 against a $700.00 balance must be refused by BOTH ---- 113 eq_ck(cnt, "E4 overdraw $2000.00 REFUSED (0=refused)" as *u8, 114 trust_disburse_ok(tp, ca, 200000), led_can_fund(lp, ca, 200000), 0) 115 116 // ---- E5 a legitimate disbursement is permitted by BOTH ---- 117 eq_ck(cnt, "E5 legitimate $500.00 disbursement ALLOWED (1=ok)" as *u8, 118 trust_disburse_ok(tp, ca, 50000), led_can_fund(lp, ca, 50000), 1) 119 120 // ---- E6 actually disburse $300.00 from ClientA in BOTH ---- 121 trust_put(tp, ca, 2, m, "disburse" as *u8, 30000) 122 led_xfer(lp, x3, ca, oper, 30000, "posted" as *u8) 123 eq_ck(cnt, "E6 ClientA balance after $300.00 disbursement" as *u8, 124 trust_balance(tp, ca), led_balance(lp, ca), 40000) 125 126 // ---- E7 NO-COMMINGLING: ClientB is untouched by ClientA activity, in BOTH ---- 127 eq_ck(cnt, "E7 no-commingling: ClientB untouched" as *u8, 128 trust_balance(tp, cb), led_balance(lp, cb), 50000) 129 130 // ---- E8 three-way holds after the disbursement ($900.00) ---- 131 let t2: i64 = trust_balance(tp, ca) + trust_balance(tp, cb) 132 let l2: i64 = led_balance(lp, ca) + led_balance(lp, cb) 133 eq_ck(cnt, "E8 three-way reconciliation after disbursement" as *u8, t2, l2, 90000) 134 135 // ---- E9 the overdraw line MOVED with the balance (refuse what was allowed at E5) ---- 136 eq_ck(cnt, "E9 $500.00 now REFUSED (balance fell to $400.00)" as *u8, 137 trust_disburse_ok(tp, ca, 50000), led_can_fund(lp, ca, 50000), 0) 138 139 // ---- E10 LEDGER-ONLY SUPERIORITY: the ledger also conserves globally; trust cannot see this. 140 // bank was debited 1200.00, clients hold 900.00, operating holds 300.00 -> sums to zero. 141 let conserve: i64 = led_balance(lp, bank) + led_balance(lp, ca) + led_balance(lp, cb) + led_balance(lp, oper) 142 if conserve == 0 { 143 cnt[0] = cnt[0] + 1 144 eq_puts(" PASS E10 ledger conserves across bank+clients+operating = 0 (trust has no such check)\n" as *u8) 145 } 146 if conserve != 0 { 147 cnt[1] = cnt[1] + 1 148 eq_puts(" FAIL E10 conservation drift = " as *u8); eq_putn(conserve); eq_puts("\n" as *u8) 149 } 150 151 eq_puts("nx_ledger_trust_equiv_gate: pass=" as *u8); eq_putn(cnt[0]) 152 eq_puts(" fail=" as *u8); eq_putn(cnt[1]); eq_puts("\n" as *u8) 153 if cnt[1] == 0 { 154 eq_puts("F997-STEP1: VERDICT=GREEN -- nx_ledger is BEHAVIOUR-EQUIVALENT to the live IOLTA organ; re-base is proven safe\n" as *u8) 155 sys_exit(0) 156 return 0 157 } 158 eq_puts("F997-STEP1: VERDICT=RED -- do NOT re-base; the primitive diverges from the compliance organ\n" as *u8) 159 sys_exit(1) 160 return 1 161}