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

↩ module page · 217 lines · 9225 B
1// nx_seat_drive_gate.nx -- GATE for the S2 seat-protocol driver (6 teeth, 3 negative controls).
2// PREREQ: stage the elfs first (banked /tmp-wipe + fork-budget laws):
3//   nx_sov_build_run nx_seat_drive / nx_fix_ok / nx_fix_fail  -> cp /tmp/<n>.sov.elf _offc/<n>.elf
4// Run from nxc2 root. SELF-EXEC CHAIN (one driver fork per process, counters ride argv --
5// the proven WSL fork-budget pattern): argv = [self] [stage] [pass].
6// Teeth: T1 happy e2e (DONE frame + both artifacts) | T2 NEG work-fail refused | T3 NEG lane-gate
7// RED refused | T4 NEG checkin refused fail-closed (work never ran) | T5 NEG artifact-lie refused
8// (rc0 work without its declared artifact) | T6 journal is append-only across reruns (DONE x2).
9// Verdict: NX-SEAT-DRIVE-GATE pass=N/6 verdict=GREEN|RED (exit 0 iff 6/6).
10// license_tier: ORIGINAL   No hw writes (Rule 26).
11import "nx_seg_store.nx"
12import "nx_deploy_lib.nx"
13import "nx_syscalls.nx"
14
15const SG_JCAP: i64 = 65536
16
17func sg_w(s: *u8) -> i64 {
  var n: i64 = 0
  while s[n] != (0 as u8) { n = n + 1 }
  sys_write(1, s, n)
  return 0
22}
23
24func sg_len(s: *u8) -> i64 {
  var n: i64 = 0
  while s[n] != (0 as u8) { n = n + 1 }
  return n
28}
29
30func sg_atoi(s: *u8) -> i64 {
  var v: i64 = 0
  var i: i64 = 0
  while s[i] != (0 as u8) {
      let c: i64 = s[i] as i64
      if c >= 48 { if c <= 57 { v = v * 10 + (c - 48) } }
      i = i + 1
  }
  return v
39}
40
41func sg_itoa(dst: *u8, v: i64) -> i64 {
  var m: i64 = v
  let t: *u8 = sys_mmap(24)
  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[i] = t[k - 1 - i]; i = i + 1 }
  dst[k] = 0 as u8
  return k
51}
52
53func sg_count(buf: *u8, n: i64, needle: *u8) -> i64 {
  var cnt: i64 = 0
  var p: i64 = 0
  while p < n {
      var ki: i64 = 0
      var hit: i64 = 1
      var scanning: i64 = 1
      while scanning == 1 {
          let kc: i64 = needle[ki] as i64
          if kc == 0 { scanning = 0 } else {
              var bc: i64 = 0
              if p + ki < n { bc = buf[p + ki] as i64 }
              if bc == kc { ki = ki + 1 } else { hit = 0; scanning = 0 }
          }
      }
      if hit == 1 { cnt = cnt + 1 }
      p = p + 1
  }
  return cnt
72}
73
74// journal-frame count: reads path fresh each call, one fixed callee chain
75func sg_jcount(path: *u8, needle: *u8) -> i64 {
  let buf: *u8 = sys_mmap(SG_JCAP)
  let n: i64 = dp_read(path, buf, SG_JCAP)
  return sg_count(buf, n, needle)
79}
80
81// non-empty file probe (artifact-truth): 1 iff path exists with >0 bytes
82func sg_nonempty(path: *u8) -> i64 {
  let buf: *u8 = sys_mmap(64)
  let n: i64 = dp_read(path, buf, 32)
  if n > 0 { return 1 }
  return 0
87}
88
89// run the driver on a lane file; returns driver exit code (-1 on signal death)
90func sg_drive(lanep: *u8, outp: *u8) -> i64 {
  let av: *i64 = sys_mmap(32) as *i64
  av[0] = lanep as i64
  return dep_run_capture("_offc/nx_seat_drive.elf" as *u8, av, 1, outp)
94}
95
96func main(argc: i64, argv: *i64) -> i64 {
  var stage: i64 = 1
  var pass: i64 = 0
  if argc >= 2 { let ss: *u8 = argv[1] as *u8; stage = sg_atoi(ss) }
  if argc >= 3 { let ps: *u8 = argv[2] as *u8; pass = sg_atoi(ps) }
  if stage < 1 { stage = 1 }
102
  if stage == 1 {
      sys_unlinkat("/tmp/sdg_t1.jrnl" as *u8)
      sys_unlinkat("/tmp/sdg_t1.marker" as *u8)
      sys_unlinkat("/tmp/sdg_t1.gmarker" as *u8)
      let lane: *u8 = "ws=sdg-t1\nactor=gatefix\njournal=/tmp/sdg_t1.jrnl\nworkelf=_offc/nx_fix_ok.elf\nworkarg1=/tmp/sdg_t1.marker\nworkartifact=/tmp/sdg_t1.marker\ngateelf=_offc/nx_fix_ok.elf\ngatearg1=/tmp/sdg_t1.gmarker\n" as *u8
      ss_writefile("/tmp/sdg_t1.lane" as *u8, lane, sg_len(lane))
      let rc: i64 = sg_drive("/tmp/sdg_t1.lane" as *u8, "/tmp/sdg_t1.out" as *u8)
      let done: i64 = sg_jcount("/tmp/sdg_t1.jrnl" as *u8, "DONE" as *u8)
      let ma: i64 = sg_nonempty("/tmp/sdg_t1.marker" as *u8)
      let ga: i64 = sg_nonempty("/tmp/sdg_t1.gmarker" as *u8)
      var ok: i64 = 1
      if rc != 0 { ok = 0 }
      if done != 1 { ok = 0 }
      if ma != 1 { ok = 0 }
      if ga != 1 { ok = 0 }
      if ok == 1 { sg_w("T1 happy-e2e PASS\n" as *u8); pass = pass + 1 } else { sg_w("T1 happy-e2e FAIL\n" as *u8) }
  }
  if stage == 2 {
      sys_unlinkat("/tmp/sdg_t2.jrnl" as *u8)
      sys_unlinkat("/tmp/sdg_t2.marker" as *u8)
      let lane: *u8 = "ws=sdg-t2\nactor=gatefix\njournal=/tmp/sdg_t2.jrnl\nworkelf=_offc/nx_fix_fail.elf\nworkarg1=/tmp/sdg_t2.marker\nworkartifact=/tmp/sdg_t2.marker\ngateelf=_offc/nx_fix_ok.elf\n" as *u8
      ss_writefile("/tmp/sdg_t2.lane" as *u8, lane, sg_len(lane))
      let rc: i64 = sg_drive("/tmp/sdg_t2.lane" as *u8, "/tmp/sdg_t2.out" as *u8)
      let wf: i64 = sg_jcount("/tmp/sdg_t2.jrnl" as *u8, "WORKFAIL" as *u8)
      let done: i64 = sg_jcount("/tmp/sdg_t2.jrnl" as *u8, "DONE" as *u8)
      var ok: i64 = 1
      if rc != 4 { ok = 0 }
      if wf != 1 { ok = 0 }
      if done != 0 { ok = 0 }
      if ok == 1 { sg_w("T2 neg-workfail PASS\n" as *u8); pass = pass + 1 } else { sg_w("T2 neg-workfail FAIL\n" as *u8) }
  }
  if stage == 3 {
      sys_unlinkat("/tmp/sdg_t3.jrnl" as *u8)
      sys_unlinkat("/tmp/sdg_t3.marker" as *u8)
      let lane: *u8 = "ws=sdg-t3\nactor=gatefix\njournal=/tmp/sdg_t3.jrnl\nworkelf=_offc/nx_fix_ok.elf\nworkarg1=/tmp/sdg_t3.marker\nworkartifact=/tmp/sdg_t3.marker\ngateelf=_offc/nx_fix_fail.elf\n" as *u8
      ss_writefile("/tmp/sdg_t3.lane" as *u8, lane, sg_len(lane))
      let rc: i64 = sg_drive("/tmp/sdg_t3.lane" as *u8, "/tmp/sdg_t3.out" as *u8)
      let gr: i64 = sg_jcount("/tmp/sdg_t3.jrnl" as *u8, "GATERED" as *u8)
      let done: i64 = sg_jcount("/tmp/sdg_t3.jrnl" as *u8, "DONE" as *u8)
      var ok: i64 = 1
      if rc != 5 { ok = 0 }
      if gr != 1 { ok = 0 }
      if done != 0 { ok = 0 }
      if ok == 1 { sg_w("T3 neg-gatered PASS\n" as *u8); pass = pass + 1 } else { sg_w("T3 neg-gatered FAIL\n" as *u8) }
  }
  if stage == 4 {
      sys_unlinkat("/tmp/sdg_t4.jrnl" as *u8)
      sys_unlinkat("/tmp/sdg_t4.marker" as *u8)
      let lane: *u8 = "ws=sdg-t4\nactor=gatefix\njournal=/tmp/sdg_t4.jrnl\nworkelf=_offc/nx_fix_ok.elf\nworkarg1=/tmp/sdg_t4.marker\nworkartifact=/tmp/sdg_t4.marker\ngateelf=_offc/nx_fix_ok.elf\ncheckinelf=_offc/nx_fix_fail.elf\n" as *u8
      ss_writefile("/tmp/sdg_t4.lane" as *u8, lane, sg_len(lane))
      let rc: i64 = sg_drive("/tmp/sdg_t4.lane" as *u8, "/tmp/sdg_t4.out" as *u8)
      let cr: i64 = sg_jcount("/tmp/sdg_t4.jrnl" as *u8, "CHECKIN-REFUSED" as *u8)
      let ma: i64 = sg_nonempty("/tmp/sdg_t4.marker" as *u8)
      var ok: i64 = 1
      if rc != 3 { ok = 0 }
      if cr != 1 { ok = 0 }
      if ma != 0 { ok = 0 }
      if ok == 1 { sg_w("T4 neg-checkin-failclosed PASS\n" as *u8); pass = pass + 1 } else { sg_w("T4 neg-checkin-failclosed FAIL\n" as *u8) }
  }
  if stage == 5 {
      sys_unlinkat("/tmp/sdg_t5.jrnl" as *u8)
      sys_unlinkat("/tmp/sdg_t5.marker" as *u8)
      sys_unlinkat("/tmp/sdg_t5.other" as *u8)
      let lane: *u8 = "ws=sdg-t5\nactor=gatefix\njournal=/tmp/sdg_t5.jrnl\nworkelf=_offc/nx_fix_ok.elf\nworkarg1=/tmp/sdg_t5.other\nworkartifact=/tmp/sdg_t5.marker\ngateelf=_offc/nx_fix_ok.elf\n" as *u8
      ss_writefile("/tmp/sdg_t5.lane" as *u8, lane, sg_len(lane))
      let rc: i64 = sg_drive("/tmp/sdg_t5.lane" as *u8, "/tmp/sdg_t5.out" as *u8)
      let na: i64 = sg_jcount("/tmp/sdg_t5.jrnl" as *u8, "NOARTIFACT" as *u8)
      var ok: i64 = 1
      if rc != 6 { ok = 0 }
      if na != 1 { ok = 0 }
      if ok == 1 { sg_w("T5 neg-artifact-lie PASS\n" as *u8); pass = pass + 1 } else { sg_w("T5 neg-artifact-lie FAIL\n" as *u8) }
  }
  if stage == 6 {
      // NO cleanup -- T6 proves the journal is append-only across reruns of the T1 lane
      let rc: i64 = sg_drive("/tmp/sdg_t1.lane" as *u8, "/tmp/sdg_t6.out" as *u8)
      let done: i64 = sg_jcount("/tmp/sdg_t1.jrnl" as *u8, "DONE" as *u8)
      var ok: i64 = 1
      if rc != 0 { ok = 0 }
      if done != 2 { ok = 0 }
      if ok == 1 { sg_w("T6 journal-append-only PASS\n" as *u8); pass = pass + 1 } else { sg_w("T6 journal-append-only FAIL\n" as *u8) }
  }
184
  if stage >= 6 {
      sg_w("NX-SEAT-DRIVE-GATE pass=" as *u8)
      let pb: *u8 = sys_mmap(24)
      sg_itoa(pb, pass)
      sg_w(pb)
      if pass == 6 {
          sg_w("/6 verdict=GREEN\n" as *u8)
          sys_exit(0)
          return 0
      }
      sg_w("/6 verdict=RED\n" as *u8)
      sys_exit(1)
      return 1
  }
199
  // SELF-EXEC CHAIN: one driver fork per process; counters ride argv
  let self: *u8 = argv[0] as *u8
  let sb: *u8 = sys_mmap(24)
  sg_itoa(sb, stage + 1)
  let pb2: *u8 = sys_mmap(24)
  sg_itoa(pb2, pass)
  let nav: *i64 = sys_mmap(40) as *i64
  nav[0] = self as i64
  nav[1] = sb as i64
  nav[2] = pb2 as i64
  nav[3] = 0
  let envp: *i64 = sys_mmap(16) as *i64
  envp[0] = 0
  sys_execve(self, nav, envp)
  sg_w("SDG-EXEC-FAIL\n" as *u8)
  sys_exit(1)
  return 1
217}
nx_seat_drive_gate.nx source

`nx_seat_drive_gate.nx` source
