code wiki / _hdl_build / nx_vizsla_budget_gate.nx
`nx_vizsla_budget_gate.nx` source

↩ module page · 324 lines · 13426 B
1// nx_vizsla_budget_gate.nx -- VIZSLA V1 gate: the budget ledger is gate-proven
2// against a HAND-TOTALED fixture month (construction-known sums; the oracle is
3// arithmetic done by hand in this file's comments, not the module under test).
4// Fixture store lives under an epoch-unique /tmp prefix => every run starts on
5// a virgin store AND the module's prefix-derived log keeps fixtures out of the
6// family ledger log (isolation by construction).
7//
8// month1 (segid 1001), hand-totaled:
9//   rent 120000 | groceries 4500+6250+3250=14000 | dining 2200+5800=8000 | fun 999
10//   => total txns=7 spent=142999; env rent=120000 OK(0), groceries=15000 OK(+1000),
11//      dining=7500 OVER(-500); fun UNBUDGETED(-999)
12// month2 (segid 1002): rent 120000 + groceries 5100 + dining 1500 = 126600
13//   => ALL: groceries 19100, txns=10, spent=269599
14//
15// Rows:
16//   1 loud-fail        missing txn file => exit 1
17//   2 load-month1      scanned=7 new=7 committed seg-1001
18//   3 hand-totaled     groceries row exact + TOTAL txns=7 spent=142999
19//   4 envelope-over    dining delta=-500 state=OVER
20//   5 unbudgeted       fun named state=UNBUDGETED (never silently dropped)
21//   6 idempotent       re-load month1 => new=0 dup_instore=7 segment=none (law 10)
22//   7 additive-month2  month2 lands; ALL report groceries=19100 txns=10
23//   8 TIME-TRAVEL      report asof=1001 AFTER month2 == byte-identical pre-month2 report
24//   9 determinism      ALL report twice => byte-identical
25//  10 verify-clean     CID recompute over 10 entries => verdict=CLEAN exit 0
26//  11 TAMPER-EVIDENCE  one flipped byte in seg-1002.docs => verdict=TAMPERED exit 1
27// Evidence: VIZSLA-BUDGET-GATE line -> stdout + knowledge/status/vizsla_gate.log;
28// exit 0 iff 11/11.
29// spec: knowledge/specs/2026-06-10-nishi-vizsla-ladder.md   license_tier: ORIGINAL
30import "nx_syscalls.nx"
31import "nx_gate_verdict.nx"
32
33func bg_slen(s: *u8) -> i64 {
  var n: i64 = 0
  while s[n] != (0 as u8) { n = n + 1 }
  return n
37}
38
39func bg_p(s: *u8) -> i64 {
  sys_write(1, s, bg_slen(s))
  return 0
42}
43
44func bg_cat(dst: *u8, off: i64, s: *u8) -> i64 {
  var i: i64 = 0
  while s[i] != (0 as u8) { dst[off + i] = s[i]; i = i + 1 }
  return off + i
48}
49
50func bg_catn(dst: *u8, off: i64, v: i64) -> i64 {
  var o: i64 = off
  var m: i64 = v
  if m < 0 { dst[o] = 45 as u8; o = o + 1; m = 0 - m }
  let t: *u8 = sys_mmap(28)
  var k: i64 = 0
  if m == 0 { t[0] = 48 as u8; k = 1 }
  while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
  var i: i64 = 0
  while i < k { dst[o + i] = t[k - 1 - i]; i = i + 1 }
  return o + k
61}
62
63func bg_write(path: *u8, content: *u8) -> i64 {
  let fd: i64 = sys_openat_wr(path, 0x1a4)
  if fd < 0 { return 0 - 1 }
  sys_write(fd, content, bg_slen(content))
  sys_close(fd)
  return 0
69}
70
71func bg_readall(path: *u8, szout: *i64) -> *u8 {
  let fd: i64 = sys_openat_rd(path)
  if fd < 0 { szout[0] = 0 - 1; return 0 as *u8 }
  let sz: i64 = sys_lseek(fd, 0, 2)
  sys_lseek(fd, 0, 0)
  let buf: *u8 = sys_mmap(sz + 64)
  var got: i64 = 0
  var n: i64 = 1
  while n > 0 {
      n = sys_read(fd, (buf as i64 + got) as *u8, 65536)
      if n > 0 { got = got + n }
  }
  sys_close(fd)
  szout[0] = got
  return buf
86}
87
88// run elf with up to 4 args, stdout+stderr -> outpath; returns WEXITSTATUS or 128+sig
89func bg_run(elf: *u8, a1: *u8, a2: *u8, a3: *u8, a4: *u8, outpath: *u8) -> i64 {
  let pid: i64 = sys_fork()
  if pid == 0 {
      if (outpath as i64) != 0 {
          let ofd: i64 = sys_openat_wr(outpath, 0x1a4)
          if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) }
      }
      let argv: *i64 = sys_mmap(64) as *i64
      argv[0] = elf as i64
      var i: i64 = 1
      if (a1 as i64) != 0 { argv[i] = a1 as i64; i = i + 1 }
      if (a2 as i64) != 0 { argv[i] = a2 as i64; i = i + 1 }
      if (a3 as i64) != 0 { argv[i] = a3 as i64; i = i + 1 }
      if (a4 as i64) != 0 { argv[i] = a4 as i64; i = i + 1 }
      argv[i] = 0
      let envp: *i64 = sys_mmap(16) as *i64
      envp[0] = 0
      sys_execve(elf, argv, envp)
      sys_exit(127)
  }
  let st: *i64 = sys_mmap(16) as *i64
  sys_wait4(pid, st, 0)
  let sig: i64 = st[0] & 0x7f
  if sig != 0 { return 128 + sig }
  return (st[0] >> 8) & 0xff
114}
115
116func bg_has(path: *u8, needle: *u8) -> i64 {
  let szp: *i64 = sys_mmap(16) as *i64
  let b: *u8 = bg_readall(path, szp)
  let sz: i64 = szp[0]
  let n: i64 = bg_slen(needle)
  if sz < n { return 0 }
  var i: i64 = 0
  while i + n <= sz {
      var ok: i64 = 1
      var j: i64 = 0
      while j < n {
          if b[i + j] != needle[j] { ok = 0; j = n } else { j = j + 1 }
      }
      if ok == 1 { return 1 }
      i = i + 1
  }
  return 0
133}
134
135func bg_fileeq(p1: *u8, p2: *u8) -> i64 {
  let s1: *i64 = sys_mmap(16) as *i64
  let s2: *i64 = sys_mmap(16) as *i64
  let b1: *u8 = bg_readall(p1, s1)
  let b2: *u8 = bg_readall(p2, s2)
  if s1[0] != s2[0] { return 0 }
  if s1[0] <= 0 { return 0 }
  var i: i64 = 0
  while i < s1[0] {
      if b1[i] != b2[i] { return 0 }
      i = i + 1
  }
  return 1
148}
149
150// flip one byte `fromend` before EOF (tamper injection; same size => same layout)
151func bg_flip(path: *u8, fromend: i64) -> i64 {
  let szp: *i64 = sys_mmap(16) as *i64
  let b: *u8 = bg_readall(path, szp)
  let sz: i64 = szp[0]
  if sz <= fromend { return 0 - 1 }
  let off: i64 = sz - fromend
  b[off] = (b[off] as i64 ^ 0x41) as u8
  let fd: i64 = sys_openat_wr(path, 0x1a4)
  if fd < 0 { return 0 - 1 }
  sys_write(fd, b, sz)
  sys_close(fd)
  return 0
163}
164
165func bg_row(name: *u8, pass: i64) -> i64 {
  bg_p("ROW " as *u8)
  bg_p(name)
  if pass == 1 { bg_p(" PASS\n" as *u8) } else { bg_p(" FAIL\n" as *u8) }
  return pass
170}
171
172func main(argc: i64, argv: *i64) -> i64 {
  bg_p("=== VIZSLA BUDGET GATE: hand-totaled ledger KATs on a virgin fixture store ===\n" as *u8)
  var bud: *u8 = "buildroot/_build/nx_vizsla_budget.sov.elf" as *u8
  if argc > 1 { bud = argv[1] as *u8 }
  // self-heal: rebuild the instrument via the durable runner if /tmp was wiped
  let pr: i64 = sys_openat_rd(bud)
  if pr >= 0 { sys_close(pr) }
  else {
      bg_p(" instrument missing -> rebuilding via durable runner\n" as *u8)
      bg_run("_offc/nx_sov_build_run.elf" as *u8, "nx_vizsla_budget" as *u8, 0 as *u8, 0 as *u8, 0 as *u8, "/tmp/vzb_rebuild.out" as *u8)
  }
183
  // epoch-unique virgin store prefix: /tmp/vzbG<epoch>-
  let pfx: *u8 = sys_mmap(128)
  var po: i64 = 0
  po = bg_cat(pfx, po, "/tmp/vzbG" as *u8)
  po = bg_catn(pfx, po, sys_now_us())
  po = bg_cat(pfx, po, "-" as *u8)
  pfx[po] = 0 as u8
191
  // hand-totaled fixtures (sums in the header comment ARE the oracle)
  let m1: *u8 = "TXN 2026-05-01 120000 rent may-rent\nTXN 2026-05-03 4500 groceries heb\nTXN 2026-05-05 2200 dining tacos\nTXN 2026-05-10 6250 groceries costco\nTXN 2026-05-17 3250 groceries heb\nTXN 2026-05-19 5800 dining anniversary\nTXN 2026-05-21 999 fun arcade\n" as *u8
  bg_write("/tmp/vzb_m1.txt" as *u8, m1)
  let m2: *u8 = "TXN 2026-06-02 120000 rent june-rent\nTXN 2026-06-04 5100 groceries heb\nTXN 2026-06-08 1500 dining pizza\n" as *u8
  bg_write("/tmp/vzb_m2.txt" as *u8, m2)
  let env: *u8 = "ENV rent 120000\nENV groceries 15000\nENV dining 7500\n" as *u8
  bg_write("/tmp/vzb_env.txt" as *u8, env)
199
  let fenv: *u8 = "/tmp/vzb_env.txt" as *u8
  var pass: i64 = 0
  var r: i64 = 0
203
  // row 1: loud-fail on missing txn file
  let rc1: i64 = bg_run(bud, "load" as *u8, "/tmp/vzb_m1_NOPE.txt" as *u8, pfx, 0 as *u8, "/tmp/vzb_out1.txt" as *u8)
  r = 0
  if rc1 == 1 { r = 1 }
  pass = pass + bg_row("loud-fail-missing-txnfile" as *u8, r)
209
  // row 2: load month1 into seg-1001
  let rc2: i64 = bg_run(bud, "load" as *u8, "/tmp/vzb_m1.txt" as *u8, pfx, "1001" as *u8, "/tmp/vzb_out2.txt" as *u8)
  r = 0
  if rc2 == 0 {
      if bg_has("/tmp/vzb_out2.txt" as *u8, "VIZSLA-LEDGER-LOAD scanned=7 new=7 dup_infile=0 dup_instore=0 segment=seg-1001" as *u8) == 1 { r = 1 }
  }
  pass = pass + bg_row("load-month1-seg1001" as *u8, r)
217
  // row 3: hand-totaled month (asof=1001 view; this exact file is row 8's oracle)
  let rc3: i64 = bg_run(bud, "report" as *u8, pfx, fenv, "1001" as *u8, "/tmp/vzb_out3.txt" as *u8)
  r = 0
  if rc3 == 0 {
      if bg_has("/tmp/vzb_out3.txt" as *u8, "VIZSLA-LEDGER category=groceries spent=14000 budget=15000 delta=1000 state=OK" as *u8) == 1 {
          if bg_has("/tmp/vzb_out3.txt" as *u8, "VIZSLA-LEDGER-TOTAL txns=7 spent=142999" as *u8) == 1 { r = 1 }
      }
  }
  pass = pass + bg_row("hand-totaled-month" as *u8, r)
227
  // row 4: envelope over-spend named with exact delta
  r = bg_has("/tmp/vzb_out3.txt" as *u8, "VIZSLA-LEDGER category=dining spent=8000 budget=7500 delta=-500 state=OVER" as *u8)
  pass = pass + bg_row("envelope-over-delta" as *u8, r)
231
  // row 5: unbudgeted category is NAMED, never silently dropped
  r = bg_has("/tmp/vzb_out3.txt" as *u8, "VIZSLA-LEDGER category=fun spent=999 budget=0 delta=-999 state=UNBUDGETED" as *u8)
  pass = pass + bg_row("unbudgeted-named" as *u8, r)
235
  // row 6: idempotent re-load (law 10): all 7 dedup vs store, nothing committed
  let rc6: i64 = bg_run(bud, "load" as *u8, "/tmp/vzb_m1.txt" as *u8, pfx, "1009" as *u8, "/tmp/vzb_out6.txt" as *u8)
  r = 0
  if rc6 == 0 {
      if bg_has("/tmp/vzb_out6.txt" as *u8, "VIZSLA-LEDGER-LOAD scanned=7 new=0 dup_infile=0 dup_instore=7 segment=none" as *u8) == 1 { r = 1 }
  }
  pass = pass + bg_row("idempotent-reload" as *u8, r)
243
  // row 7: month2 is additive; ALL view shows combined hand totals
  let rc7: i64 = bg_run(bud, "load" as *u8, "/tmp/vzb_m2.txt" as *u8, pfx, "1002" as *u8, "/tmp/vzb_out7.txt" as *u8)
  var rc7b: i64 = 1
  rc7b = bg_run(bud, "report" as *u8, pfx, fenv, 0 as *u8, "/tmp/vzb_out7b.txt" as *u8)
  r = 0
  if rc7 == 0 { if rc7b == 0 {
      if bg_has("/tmp/vzb_out7.txt" as *u8, " new=3 " as *u8) == 1 {
          if bg_has("/tmp/vzb_out7b.txt" as *u8, "VIZSLA-LEDGER-TOTAL txns=10 spent=269599" as *u8) == 1 { r = 1 }
      }
  } }
  pass = pass + bg_row("additive-month2" as *u8, r)
255
  // row 8: TIME TRAVEL -- asof=1001 AFTER month2 == the pre-month2 report, byte-identical
  bg_run(bud, "report" as *u8, pfx, fenv, "1001" as *u8, "/tmp/vzb_out8.txt" as *u8)
  r = bg_fileeq("/tmp/vzb_out3.txt" as *u8, "/tmp/vzb_out8.txt" as *u8)
  pass = pass + bg_row("time-travel-asof" as *u8, r)
260
  // row 9: determinism -- ALL report twice, byte-identical
  bg_run(bud, "report" as *u8, pfx, fenv, 0 as *u8, "/tmp/vzb_out9.txt" as *u8)
  r = bg_fileeq("/tmp/vzb_out7b.txt" as *u8, "/tmp/vzb_out9.txt" as *u8)
  pass = pass + bg_row("determinism-byte-identical" as *u8, r)
265
  // row 10: tamper-evidence baseline -- untouched store verifies CLEAN
  let rc10: i64 = bg_run(bud, "verify" as *u8, pfx, 0 as *u8, 0 as *u8, "/tmp/vzb_out10.txt" as *u8)
  r = 0
  if rc10 == 0 {
      if bg_has("/tmp/vzb_out10.txt" as *u8, "VIZSLA-LEDGER-VERIFY entries=10 bad=0 verdict=CLEAN" as *u8) == 1 { r = 1 }
  }
  pass = pass + bg_row("verify-clean" as *u8, r)
273
  // row 11: TAMPER-EVIDENCE -- flip one byte inside seg-1002's last value
  let tpath: *u8 = sys_mmap(256)
  var to: i64 = 0
  to = bg_cat(tpath, to, pfx)
  to = bg_cat(tpath, to, "seg-1002.docs" as *u8)
  tpath[to] = 0 as u8
  bg_flip(tpath, 3)
  let rc11: i64 = bg_run(bud, "verify" as *u8, pfx, 0 as *u8, 0 as *u8, "/tmp/vzb_out11.txt" as *u8)
  r = 0
  if rc11 == 1 {
      if bg_has("/tmp/vzb_out11.txt" as *u8, "verdict=TAMPERED" as *u8) == 1 {
          if bg_has("/tmp/vzb_out11.txt" as *u8, "VIZSLA-LEDGER-TAMPER segment=seg-1002" as *u8) == 1 { r = 1 }
      }
  }
  pass = pass + bg_row("tamper-evidence-flipped-byte" as *u8, r)
289
  let permil: i64 = (pass * 1000) / 11
  let logfd: i64 = sys_openat_append("knowledge/status/vizsla_gate.log" as *u8, 0x1a4)
  var fdi: i64 = 0
  while fdi < 2 {
      var fd: i64 = 1
      if fdi == 1 { fd = logfd }
      if fd > 0 {
          let line: *u8 = sys_mmap(256)
          var o: i64 = 0
          o = bg_cat(line, o, "VIZSLA-BUDGET-GATE epoch=" as *u8)
          o = bg_catn(line, o, sys_now_realtime_sec())
          o = bg_cat(line, o, " rows=11 pass=" as *u8)
          o = bg_catn(line, o, pass)
          o = bg_cat(line, o, " permil=" as *u8)
          o = bg_catn(line, o, permil)
          if pass == 11 {
              o = bg_cat(line, o, " verdict=GREEN\n" as *u8)
          } else {
              o = bg_cat(line, o, " verdict=RED\n" as *u8)
          }
          sys_write(fd, line, o)
      }
      fdi = fdi + 1
  }
  if logfd > 0 { sys_close(logfd) }
  // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
  // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
  // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
  let ctr__dry: *i64 = gv_ctr()
  ctr__dry[0] = pass
  ctr__dry[1] = 11
  let rc__dry: i64 = gv_verdict("VIZSLA-BUDGET-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
  sys_exit(rc__dry)
  return rc__dry
324}
nx_vizsla_budget_gate.nx source

`nx_vizsla_budget_gate.nx` source
