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

↩ module page · 223 lines · 10246 B
1// nx_game_actor_gate.nx -- proves the character<->environment interaction floor (ws=game-interact).
2// Teeth follow the lane law: every equality carries a NON-VACUITY guard; the flagship tooth (T2/T5
3// occupancy) is designed so the mutation "ac_step skips the occupancy check" turns it RED while the
4// anti-vacuity tooth stays GREEN. license_tier: ORIGINAL
5import "nx_syscalls.nx"
6import "nx_game_actor.nx"
7import "nx_pathfind.nx"
8import "nx_gamesave.nx"
9
10func p(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
11func pn(v: i64) -> i64 {
  let t: *u8 = sys_mmap(32) as *u8
  var m: i64 = v
  var w: i64 = 0
  if m < 0 { t[w] = 45 as u8; w = w + 1; m = 0 - m }
  if m == 0 { t[w] = 48 as u8; sys_write(1, t, w + 1); return 0 }
  let d: *u8 = sys_mmap(32) as *u8
  var k: i64 = 0
  while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
  var j: i64 = 0
  while j < k { t[w] = d[k - 1 - j]; w = w + 1; j = j + 1 }
  sys_write(1, t, w)
  return 0
24}
25func nl() -> i64 { p("\n" as *u8); return 0 }
26
27const GW2: i64 = 16
28const GH2: i64 = 12
29
30// deterministic scripted walk: fold a seed into a move dir each step
31func dir_dx(d: i64) -> i64 { if d == 0 { return 1 } if d == 1 { return 0-1 } return 0 }
32func dir_dy(d: i64) -> i64 { if d == 2 { return 1 } if d == 3 { return 0-1 } return 0 }
33
34func main() -> i64 {
  p("=== nx_game_actor_gate (character<->environment interaction floor) ===\n" as *u8)
  var pass: i64 = 0
  let checks: i64 = 7
38
  let wd: *i64 = sys_mmap(wd_bytes(GW2, GH2)) as *i64
  wd_init(wd, GW2, GH2)
  // border walls + one interior pillar
  var i: i64 = 0
  while i < GW2 { wd_set_wall(wd, i, 0, 1); wd_set_wall(wd, i, GH2 - 1, 1); i = i + 1 }
  var j: i64 = 0
  while j < GH2 { wd_set_wall(wd, 0, j, 1); wd_set_wall(wd, GW2 - 1, j, 1); j = j + 1 }
  wd_set_wall(wd, 8, 5, 1)
47
  let ar: *i64 = sys_mmap(en_bytes(64, AC_NC)) as *i64
  en_init(ar, 64, AC_NC)
  let out: *i64 = sys_mmap(64) as *i64
51
  // T1 wall + oob collision, with the anti-vacuity half (an open move MUST succeed)
  let hp2: i64 = ac_spawn(wd, ar, 7, 5, 0, 30, 0, 1, 12345)
  var t1: i64 = 0
  if ac_step(wd, ar, hp2, 1, 0, out) == AC_WALL {              // into the pillar at (8,5)
      if en_get(ar, hp2, A_X) == 7 {                            // position unchanged
          if ac_step(wd, ar, hp2, 0, 1, out) == AC_MOVED {      // open move works (non-vacuous)
              if en_get(ar, hp2, A_Y) == 6 { t1 = 1 }
          }
      }
  }
  if t1 == 1 { pass = pass + 1; p("T1 GREEN wall stops, open passes: pillar blocked pos held, open cell entered\n" as *u8) }
  if t1 == 0 { p("T1 RED wall/open\n" as *u8) }
64
  // T2 entity collision = BUMP with the right handle, nobody moves (the interaction primitive)
  let he: i64 = ac_spawn(wd, ar, 7, 7, 1, 20, 1, 1, 777)
  var t2: i64 = 0
  let rc2: i64 = ac_step(wd, ar, hp2, 0, 1, out)               // player at (7,6) -> into enemy (7,7)
  if rc2 == AC_BUMP {
      if out[0] == he {
          if en_get(ar, hp2, A_Y) == 6 {
              if en_get(ar, he, A_Y) == 7 { t2 = 1 }
          }
      }
  }
  if t2 == 1 { pass = pass + 1; p("T2 GREEN bump-to-interact: moving into an occupied cell returns the occupant, positions held\n" as *u8) }
  if t2 == 0 { p("T2 RED bump\n" as *u8) }
78
  // T3 oob refused (walls are the border here, so drive to a corner via a fresh open-map world)
  let wd3: *i64 = sys_mmap(wd_bytes(4, 4)) as *i64
  wd_init(wd3, 4, 4)
  let ar3: *i64 = sys_mmap(en_bytes(8, AC_NC)) as *i64
  en_init(ar3, 8, AC_NC)
  let h3: i64 = ac_spawn(wd3, ar3, 0, 0, 0, 10, 0, 1, 1)
  var t3: i64 = 0
  if ac_step(wd3, ar3, h3, 0-1, 0, out) == AC_OOB {
      if ac_step(wd3, ar3, h3, 1, 0, out) == AC_MOVED { t3 = 1 }
  }
  if t3 == 1 { pass = pass + 1; p("T3 GREEN oob refused at the true edge, in-bounds move fine\n" as *u8) }
  if t3 == 0 { p("T3 RED oob\n" as *u8) }
91
  // T4 determinism: 400-step scripted walk replayed twice -> identical ck; non-vacuity: ck must MOVE
  var rep: i64 = 0
  var ck1: i64 = 0
  var ck2: i64 = 0
  var moved_total: i64 = 0
  while rep < 2 {
      let wdr: *i64 = sys_mmap(wd_bytes(GW2, GH2)) as *i64
      wd_init(wdr, GW2, GH2)
      var bi: i64 = 0
      while bi < GW2 { wd_set_wall(wdr, bi, 0, 1); wd_set_wall(wdr, bi, GH2 - 1, 1); bi = bi + 1 }
      var bj: i64 = 0
      while bj < GH2 { wd_set_wall(wdr, 0, bj, 1); wd_set_wall(wdr, GW2 - 1, bj, 1); bj = bj + 1 }
      wd_set_wall(wdr, 8, 5, 1)
      let arr: *i64 = sys_mmap(en_bytes(64, AC_NC)) as *i64
      en_init(arr, 64, AC_NC)
      let ha: i64 = ac_spawn(wdr, arr, 3, 3, 0, 30, 0, 1, 5)
      let hb: i64 = ac_spawn(wdr, arr, 12, 8, 1, 20, 1, 1, 9)
      let ck0: i64 = ac_ck(wdr, arr)
      var s: i64 = 424242
      var st: i64 = 0
      while st < 400 {
          s = s * 1103515245 + 12345
          var d: i64 = (s >> 16) & 3
          if d < 0 { d = 0 - d }
          let rc: i64 = ac_step(wdr, arr, ha, dir_dx(d), dir_dy(d), out)
          if rc == AC_MOVED { moved_total = moved_total + 1 }
          s = s * 1103515245 + 12345
          var d2: i64 = (s >> 16) & 3
          if d2 < 0 { d2 = 0 - d2 }
          ac_step(wdr, arr, hb, dir_dx(d2), dir_dy(d2), out)
          st = st + 1
      }
      var ckf: i64 = ac_ck(wdr, arr)
      if ckf == ck0 { ckf = 0 }                                 // frozen world would be vacuous
      if rep == 0 { ck1 = ckf }
      if rep == 1 { ck2 = ckf }
      rep = rep + 1
  }
  var t4: i64 = 0
  if ck1 == ck2 { if ck1 != 0 { if moved_total > 100 { t4 = 1 } } }
  if t4 == 1 { pass = pass + 1; p("T4 GREEN deterministic: 2x400-step replay ck identical ck=" as *u8); pn(ck1); p(" moved=" as *u8); pn(moved_total); nl() }
  if t4 == 0 { p("T4 RED determinism ck1=" as *u8); pn(ck1); p(" ck2=" as *u8); pn(ck2); nl() }
134
  // T5 occupancy invariant under churn: spawn/walk/remove cycles, then the invariant walker
  var t5: i64 = 0
  var churn_moves: i64 = 0
  var s5: i64 = 31337
  var c: i64 = 0
  while c < 30 {
      s5 = s5 * 1103515245 + 12345
      var px: i64 = ((s5 >> 16) & 32767) % (GW2 - 2) + 1
      s5 = s5 * 1103515245 + 12345
      var py: i64 = ((s5 >> 16) & 32767) % (GH2 - 2) + 1
      let hn: i64 = ac_spawn(wd, ar, px, py, 1, 10, 2, 1, s5)
      if hn > 0 {
          var mv: i64 = 0
          while mv < 12 {
              s5 = s5 * 1103515245 + 12345
              var dd: i64 = (s5 >> 16) & 3
              if dd < 0 { dd = 0 - dd }
              if ac_step(wd, ar, hn, dir_dx(dd), dir_dy(dd), out) == AC_MOVED { churn_moves = churn_moves + 1 }
              mv = mv + 1
          }
          if (c % 3) == 0 { ac_remove(wd, ar, hn) }
      }
      c = c + 1
  }
  if ac_occ_check(wd, ar) == 0 { if churn_moves > 20 { if en_count(ar) > 2 { t5 = 1 } } }
  if t5 == 1 { pass = pass + 1; p("T5 GREEN occupancy invariant held through churn: moves=" as *u8); pn(churn_moves); p(" actors=" as *u8); pn(en_count(ar)); nl() }
  if t5 == 0 { p("T5 RED occupancy violations=" as *u8); pn(ac_occ_check(wd, ar)); nl() }
162
  // T6 the shared grid REALLY drives pf_astar: path around the pillar exists and every path cell is open
  var t6: i64 = 0
  let n6: i64 = GW2 * GH2
  let g6: *i64 = sys_mmap(n6 * 8) as *i64
  let f6: *i64 = sys_mmap(n6 * 8) as *i64
  let cm6: *i64 = sys_mmap(n6 * 8) as *i64
  let of6: *i64 = sys_mmap(n6 * 8) as *i64
  let cl6: *i64 = sys_mmap(n6 * 8) as *i64
  let pa6: *i64 = sys_mmap(n6 * 8) as *i64
  let plen: i64 = pf_astar(wd_grid(wd), GW2, GH2, 1, 5, 14, 5, g6, f6, cm6, of6, cl6, pa6)
  if plen > 0 {
      var okcells: i64 = 1
      var pi: i64 = 0
      while pi < plen {
          let cell: i64 = pa6[pi]
          if wd_wall(wd, cell % GW2, cell / GW2) != 0 { okcells = 0 }
          pi = pi + 1
      }
      if okcells == 1 { if plen >= 13 { t6 = 1 } }              // straight line is 13; pillar may force more
  }
  if t6 == 1 { pass = pass + 1; p("T6 GREEN pf_astar consumes the live world grid: path len=" as *u8); pn(plen); p(" all cells open\n" as *u8) }
  if t6 == 0 { p("T6 RED astar-on-world plen=" as *u8); pn(plen); nl() }
185
  // T7 gamesave transparency (GX-9): save world+actors, load into ZEROED arenas, ck equal + non-vacuous
  var t7: i64 = 0
  let wn: i64 = wd_words(GW2, GH2)
  let an: i64 = en_words(64, AC_NC)
  let S: *i64 = sys_mmap((wn + an) * 8) as *i64
  var si: i64 = 0
  while si < wn { S[si] = wd[si]; si = si + 1 }
  var sj: i64 = 0
  while sj < an { S[wn + sj] = ar[sj]; sj = sj + 1 }
  let ckpre: i64 = ac_ck(wd, ar)
  let rcs: i64 = gs_save("knowledge/nx_actor_t7.sav" as *u8, 9101, S, wn + an, 1000)
  let L: *i64 = sys_mmap((wn + an) * 8) as *i64
  let meta: *i64 = sys_mmap(64) as *i64
  let rcl: i64 = gs_load("knowledge/nx_actor_t7.sav" as *u8, L, wn + an, meta)
  if rcs > 0 { if rcl >= 0 {
      let wd7: *i64 = sys_mmap(wn * 8) as *i64
      let ar7: *i64 = sys_mmap(an * 8) as *i64
      var li: i64 = 0
      while li < wn { wd7[li] = L[li]; li = li + 1 }
      var lj: i64 = 0
      while lj < an { ar7[lj] = L[wn + lj]; lj = lj + 1 }
      let ckpost: i64 = ac_ck(wd7, ar7)
      if ckpost == ckpre { if en_count(ar7) > 2 { if churn_moves > 0 {
          // resumed world must CONTINUE identically: same scripted step on both
          ac_step(wd, ar, hp2, 0, 0-1, out)
          let hp7: i64 = hp2                                     // same handle value is valid in the copy
          ac_step(wd7, ar7, hp7, 0, 0-1, out)
          if ac_ck(wd, ar) == ac_ck(wd7, ar7) { t7 = 1 }
      } } }
  } }
  if t7 == 1 { pass = pass + 1; p("T7 GREEN save/load transparent: ck equal pre/post + resumed step identical (non-vacuous world)\n" as *u8) }
  if t7 == 0 { p("T7 RED save/load rcs=" as *u8); pn(rcs); p(" rcl=" as *u8); pn(rcl); nl() }
218
  p("nx_game_actor_gate: " as *u8); pn(pass); p("/" as *u8); pn(checks); nl()
  if pass == checks { p("VERDICT GREEN\n" as *u8); return 0 }
  p("VERDICT RED\n" as *u8)
  return 1
223}
nx_game_actor_gate.nx source

`nx_game_actor_gate.nx` source
