code wiki / (root) / nx_ledger_gate.nx
`nx_ledger_gate.nx` source

↩ module page · 186 lines · 8862 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 {
  var n: i64 = 0
  while s[n] != (0 as u8) { n = n + 1 }
  sys_write(1, s, n)
  return 0
25}
26func lg_putn(v: i64) -> i64 {
  let t: *u8 = sys_mmap(32)
  var o: i64 = 0
  var m: i64 = v
  if m < 0 { t[o] = 45 as u8; o = o + 1; m = 0 - m }
  let d: *u8 = sys_mmap(32)
  var k: i64 = 0
  if m == 0 { d[0] = 48 as u8; k = 1 }
  while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
  var i: i64 = 0
  while i < k { t[o] = d[k - 1 - i]; o = o + 1; i = i + 1 }
  sys_write(1, t, o)
  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 {
  if got == want {
      cnt[0] = cnt[0] + 1
      lg_puts("  PASS " as *u8); lg_puts(name); lg_puts(" = " as *u8); lg_putn(got); lg_puts("\n" as *u8)
      return 1
  }
  cnt[1] = cnt[1] + 1
  lg_puts("  FAIL " as *u8); lg_puts(name); lg_puts(" got " as *u8); lg_putn(got)
  lg_puts(" want " as *u8); lg_putn(want); lg_puts("\n" as *u8)
  return 0
51}
52
53// build a run-unique id: <tag><nonce>
54func lg_id(tag: *u8, nonce: i64, out: *u8) -> i64 {
  var o: i64 = mt_catcopy(out, 0, tag)
  o = mt_catn(out, o, nonce)
  out[o] = 0 as u8
  return o
59}
60
61func main(argc: i64, argv: *i64) -> i64 {
  // FIXTURE MOVED OUT OF THE SWEPT STORE (2026-08-07). knowledge/store/ is walked every 600s by the
  // nx_segguard beat, which has folded THIS gate's fixture 17 times -- more than any other gate in
  // the corpus. A fold landing mid-run rewrites the manifest under the code being measured, so a RED
  // here could not be attributed to the ledger logic at all. Proven on the sibling defect: the SAME
  // code went RED on a knowledge/store fixture and GREEN 24/24 on a /tmp one.
  // The run-unique account names below were the earlier mitigation -- they keep the DELTAS clean but
  // leave the plane accumulating in production, which is precisely what let it grow past the fold
  // threshold. ★MAKING THE DATA UNIQUE IS NOT THE SAME AS MAKING THE LOCATION ISOLATED.
  // Created at SETUP, not teardown: a teardown does not run when a run crashes.
  sys_mkdir("/tmp/ledgergate\x00" as *u8, 0x1ed)
  let pfx: *u8 = "/tmp/ledgergate/ledgergate-" as *u8
  let nonce: i64 = sys_now_us()
  let cnt: *i64 = sys_mmap(16) as *i64
  cnt[0] = 0
  cnt[1] = 0
77
  // run-unique account names so deltas are clean even though the plane is append-only
  let A: *u8 = sys_mmap(64)
  let B: *u8 = sys_mmap(64)
  let C: *u8 = sys_mmap(64)
  lg_id("acctA" as *u8, nonce, A)
  lg_id("acctB" as *u8, nonce, B)
  lg_id("acctC" as *u8, nonce, C)
85
  let i1: *u8 = sys_mmap(64)
  let i2: *u8 = sys_mmap(64)
  let i3: *u8 = sys_mmap(64)
  let i4: *u8 = sys_mmap(64)
  let i5: *u8 = sys_mmap(64)
  lg_id("t1_" as *u8, nonce, i1)
  lg_id("t2_" as *u8, nonce, i2)
  lg_id("t3_" as *u8, nonce, i3)
  lg_id("t4_" as *u8, nonce, i4)
  lg_id("t5_" as *u8, nonce, i5)
96
  lg_puts("NISHI-LEDGER-GATE (F981 double-entry, integer minor units)\n" as *u8)
98
  // ---- T1/T2: a posted transfer moves EXACTLY the amount, both directions ----
  led_xfer(pfx, i1, A, B, 10000, "posted" as *u8)
  lg_ck(cnt, "T1 debit side  bal(A) after A->B $100.00" as *u8, led_balance(pfx, A), 0 - 10000)
  lg_ck(cnt, "T2 credit side bal(B) after A->B $100.00" as *u8, led_balance(pfx, B), 10000)
103
  // ---- T3: second transfer, exact cumulative deltas (a sign flip or wrong field fails here) ----
  led_xfer(pfx, i2, B, C, 2500, "posted" as *u8)
  lg_ck(cnt, "T3 bal(B) after B->C $25.00" as *u8, led_balance(pfx, B), 7500)
107
  // ---- T4: THE CROSS-CHECK -- per-account balances must sum to ZERO ----
  // NOT structural: this validates the per-account filter against global conservation.
  let sum3: i64 = led_balance(pfx, A) + led_balance(pfx, B) + led_balance(pfx, C)
  lg_ck(cnt, "T4 sum of per-account balances (conservation)" as *u8, sum3, 0)
112
  // ---- T5/T6: refusals must refuse AND write nothing ----
  let bA: i64 = led_balance(pfx, A)
  lg_ck(cnt, "T5 negative amount REFUSED" as *u8, led_xfer(pfx, i3, A, B, 0 - 500, "posted" as *u8), 0 - 1)
  lg_ck(cnt, "T5b refusal left bal(A) untouched" as *u8, led_balance(pfx, A), bA)
  lg_ck(cnt, "T6 self-transfer REFUSED" as *u8, led_xfer(pfx, i3, A, A, 500, "posted" as *u8), 0 - 2)
  lg_ck(cnt, "T6b refusal left bal(A) untouched" as *u8, led_balance(pfx, A), bA)
119
  // ---- T7/T8: two-phase pending reserves without moving posted money ----
  let bB: i64 = led_balance(pfx, B)
  let avB: i64 = led_available(pfx, B)
  led_xfer(pfx, i3, B, C, 1000, "pending" as *u8)
  lg_ck(cnt, "T7 pending does NOT move posted bal(B)" as *u8, led_balance(pfx, B), bB)
  lg_ck(cnt, "T8 pending DOES reduce available(B) by $10.00" as *u8, led_available(pfx, B), avB - 1000)
126
  // ---- T9: post the pending -> money moves, available unchanged from the reserved state ----
  led_resolve(pfx, i3, "post" as *u8)
  lg_ck(cnt, "T9 after post, bal(B) moved by the pending amount" as *u8, led_balance(pfx, B), bB - 1000)
130
  // ---- T10/T11: a VOIDED pending must restore available and never touch posted ----
  let bB2: i64 = led_balance(pfx, B)
  let avB2: i64 = led_available(pfx, B)
  led_xfer(pfx, i4, B, C, 3000, "pending" as *u8)
  led_resolve(pfx, i4, "void" as *u8)
  lg_ck(cnt, "T10 voided pending left posted bal(B) unchanged" as *u8, led_balance(pfx, B), bB2)
  lg_ck(cnt, "T11 voided pending RESTORED available(B)" as *u8, led_available(pfx, B), avB2)
138
  // ---- T12/T13: linked chain atomicity -- underfunded chain writes NOTHING ----
  let ids: *i64 = sys_mmap(8 * 2) as *i64
  let drs: *i64 = sys_mmap(8 * 2) as *i64
  let crs: *i64 = sys_mmap(8 * 2) as *i64
  let amts: *i64 = sys_mmap(8 * 2) as *i64
  let c1: *u8 = sys_mmap(64)
  let c2: *u8 = sys_mmap(64)
  lg_id("c1_" as *u8, nonce, c1)
  lg_id("c2_" as *u8, nonce, c2)
  ids[0] = c1 as i64
  ids[1] = c2 as i64
  drs[0] = C as i64
  drs[1] = C as i64
  crs[0] = A as i64
  crs[1] = B as i64
  amts[0] = 500000
  amts[1] = 500000
  let bC: i64 = led_balance(pfx, C)
  let bA2: i64 = led_balance(pfx, A)
  lg_ck(cnt, "T12 underfunded chain REFUSED" as *u8, led_chain(pfx, ids, drs, crs, amts, 2, C), 0 - 3)
  lg_ck(cnt, "T12b refused chain left bal(C) untouched (zero partial state)" as *u8, led_balance(pfx, C), bC)
  lg_ck(cnt, "T12c refused chain left bal(A) untouched" as *u8, led_balance(pfx, A), bA2)
161
  // ---- T13: a funded chain commits EVERY leg, conservation still holds ----
  amts[0] = 100
  amts[1] = 100
  lg_ck(cnt, "T13 funded chain committed both legs" as *u8, led_chain(pfx, ids, drs, crs, amts, 2, "" as *u8), 2)
  let sum4: i64 = led_balance(pfx, A) + led_balance(pfx, B) + led_balance(pfx, C)
  lg_ck(cnt, "T13b conservation holds after the chain" as *u8, sum4, 0)
168
  // ---- T14: chain leg validation refuses the WHOLE chain on one bad leg ----
  amts[0] = 100
  amts[1] = 0 - 5
  let bC2: i64 = led_balance(pfx, C)
  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)
  lg_ck(cnt, "T14b bad-leg refusal wrote NOTHING" as *u8, led_balance(pfx, C), bC2)
175
  lg_puts("nx_ledger_gate: pass=" as *u8); lg_putn(cnt[0])
  lg_puts(" fail=" as *u8); lg_putn(cnt[1]); lg_puts("\n" as *u8)
  if cnt[1] == 0 {
      lg_puts("F981 nx_ledger: VERDICT=GREEN (conservation cross-checked, refusals leave zero state)\n" as *u8)
      sys_exit(0)
      return 0
  }
  lg_puts("F981 nx_ledger: VERDICT=RED\n" as *u8)
  sys_exit(1)
  return 1
186}
nx_ledger_gate.nx source

`nx_ledger_gate.nx` source
