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

↩ module page · 272 lines · 15635 B
1// nx_gsplat4d_gate.nx -- GATE for the 4D spatiotemporal Gaussian core.
2//
3// ★★THIS REFEREE CARRIES NO TUNED THRESHOLDS. An earlier revision judged with hand-picked bands -- "the
4// 1-sigma weight is between 140 and 170", "more than 2000 pixels lit", "the arena is under 4 MiB". Every
5// one of those is a number nobody measured, and a referee that judges with them is measuring the number,
6// not the subject. They are all replaced by one of three honest forms:
7//   EXACT IDENTITY   -- the envelope must equal the TABLE ENTRY its index formula names (the index
8//                       arithmetic is the thing that can be wrong; only an exact compare tests it).
9//   A MATHEMATICAL LAW -- symmetry in dt, strict monotonicity, antisymmetry of a signed ramp. These hold
10//                       regardless of table precision, so they need no tolerance at all.
11//   A CONTROL        -- render the SAME time twice and require ZERO changed pixels, then a different time
12//                       and require MORE than that. The control replaces the threshold entirely, and is
13//                       strictly stronger: it proves the difference is caused by TIME, not by noise.
14//
15// The teeth that a plausible-but-wrong implementation FAILS:
16//   T4 TEMPORAL LOCALITY is the anti-vacuity tooth. Two Gaussians carry IDENTICAL motion and differ only
17//      in t_mu. At one instant one must have moved and the other must not. A deformation that ignored
18//      the temporal window -- one that just animated everything -- passes every other tooth and dies here.
19//   T1 REST INVARIANCE is the control: with no motion declared, the 4D bake reproduces the static cloud at
20//      EVERY t. 4D that cannot reduce to 3D is not a superset, it is a different thing.
21//   T9/T10/T11 are deny-guards asked BOTH directions, because A GUARD THAT REFUSES EVERYTHING PASSES
22//      EVERY NEGATIVE TEST.
23// license_tier: ORIGINAL  expect_exit: 0
24import "nx_syscalls.nx"
25import "nx_gsplat.nx"
26import "nx_gsplat4d_lib.nx"
27import "nx_png.nx"
28import "nx_gate_verdict.nx"
29
30// FIXTURE parameters. These are the scene being tested, not policy inside the organ: a referee has to
31// choose a subject, and it says out loud which one it chose.
32const GG_CAP: i64 = 256
33const GG_RING: i64 = 3
34const GG_TMU_A: i64 = 1000
35const GG_SIG: i64 = 400
36const GG_TMU_B: i64 = 5000
37const GG_VX: i64 = 4096
38const GG_WAVE: i64 = 40
39
40// 0=A and 1=B carry identical motion but different windows, 2=C is static (no motion row at all), and
41// 3.. are a travelling wave whose t_mu staggers across x -- the visual subject.
42func gg_scene() -> i64 {
  g4_init(GG_CAP, GG_RING)
  g4_set_rest(0, 0, 0, 0, 0, 0, 0-256, 400, 240, 240, 240, 256)
  g4_set_time(0, GG_TMU_A, GG_SIG)
  g4_set_motion(0, GG_VX, 0, 0, 0, 0, 0, 0)
  g4_set_rest(1, 6000, 0, 0, 0, 0, 0-256, 400, 240, 240, 240, 256)
  g4_set_time(1, GG_TMU_B, GG_SIG)
  g4_set_motion(1, GG_VX, 0, 0, 0, 0, 0, 0)
  g4_set_rest(2, 0-6000, 0, 0, 0, 0, 0-256, 400, 240, 240, 240, 256)
  var i: i64 = 0
  while i < GG_WAVE {
      let gx: i64 = 0 - 9000 + i*460
      g4_set_rest(3+i, gx, 0-2500, 0, 0, 0, 0-256, 520, 90 + i*3, 150, 230 - i*2, 256)
      g4_set_time(3+i, 600 + i*40, 300)
      g4_set_motion(3+i, 0, 5200, 0, 260, 0, 0, 0)
      i = i + 1
  }
  return 0
60}
61
62func gg_cmp(a: *i64, b: *i64, n: i64) -> i64 {
  var i: i64 = 0
  while i < n { if a[i] != b[i] { return 0 } i = i + 1 }
  return 1
66}
67func gg_pixdiff(a: *i64, b: *i64, n: i64) -> i64 {
  var d: i64 = 0
  var i: i64 = 0
  while i < n { if a[i] != b[i] { d = d + 1 } i = i + 1 }
  return d
72}
73
74func main() -> i64 {
  let ctr: *i64 = gv_ctr()
  gv_head("nx_gsplat4d_gate -- the temporal axis: 4D spatiotemporal Gaussians over the proven rasterizer" as *u8)
77
  gg_scene()
  let ng: i64 = g4_n()
  let st: i64 = gs_stride_aniso()
  let f1: *i64 = sys_mmap(GG_CAP*st*8) as *i64
  let f2: *i64 = sys_mmap(GG_CAP*st*8) as *i64
  let f3: *i64 = sys_mmap(GG_CAP*st*8) as *i64
  gv_puts("  scene gaussians=" as *u8); gv_num(ng)
  gv_puts(" arena_bytes=" as *u8); gv_num(g4_bytes())
  gv_puts(" ring_depth=" as *u8); gv_num(g4_ring_depth())
  gv_puts(" tick_unit=" as *u8); gv_num(g4_tscale())
  gv_puts(" lut_horizon_sigma=" as *u8); gv_num(g4_horizon_sigma()); gv_puts("\n" as *u8)
89
  // T1 CONTROL: gaussian 2 declares no motion, so it must sit at its rest position at EVERY t.
  g4_bake(GG_TMU_A, f1)
  g4_bake(GG_TMU_A + 3*GG_SIG, f2)
  g4_bake(0 - 20000, f3)
  var t1: i64 = 0
  if f1[2*st] == 0 - 6000 { if f2[2*st] == 0 - 6000 { if f3[2*st] == 0 - 6000 { t1 = 1 } } }
  gv_puts("  rest-invariance: static gaussian x at three different t = " as *u8)
  gv_num(f1[2*st]); gv_puts("," as *u8); gv_num(f2[2*st]); gv_puts("," as *u8); gv_num(f3[2*st]); gv_puts("\n" as *u8)
  gv_check("T1 rest invariance: a motionless gaussian bakes to its rest position at every t (4D reduces to 3D)" as *u8, t1, ctr)
99
  // T2 the envelope is EXACTLY the table entry its index formula names. u = (dt/sigma)^2, and the index
  // is k = lutu*u, so dt=sigma is k=lutu and dt=2*sigma is k=4*lutu. No band, no tolerance: an exact
  // identity that fails the moment the index arithmetic is wrong.
  let lu: i64 = gs_lutu()
  let e0: i64 = g4_envelope(0, GG_TMU_A)
  let e1: i64 = g4_envelope(0, GG_TMU_A + GG_SIG)
  let e2: i64 = g4_envelope(0, GG_TMU_A + 2*GG_SIG)
  gv_puts("  envelope: w(0)=" as *u8); gv_num(e0); gv_puts(" vs lut[0]=" as *u8); gv_num(g4_lut(0))
  gv_puts(" | w(1sig)=" as *u8); gv_num(e1); gv_puts(" vs lut[lutu]=" as *u8); gv_num(g4_lut(lu))
  gv_puts(" | w(2sig)=" as *u8); gv_num(e2); gv_puts(" vs lut[4*lutu]=" as *u8); gv_num(g4_lut(4*lu)); gv_puts("\n" as *u8)
  var t2: i64 = 0
  if e0 == g4_lut(0) { if e1 == g4_lut(lu) { if e2 == g4_lut(4*lu) { if e0 == g4_wfull() { t2 = 1 } } } }
  gv_check("T2 envelope EXACT: w equals the table entry its index formula names, at three derived indices" as *u8, t2, ctr)
113
  // T2b LAWS that hold at ANY table precision, so they need no tolerance: the envelope is symmetric in
  // dt, strictly decreasing away from t_mu, and exactly zero past the horizon the table itself implies.
  let sym1: i64 = g4_envelope(0, GG_TMU_A + GG_SIG)
  let sym2: i64 = g4_envelope(0, GG_TMU_A - GG_SIG)
  let e3: i64 = g4_envelope(0, GG_TMU_A + 3*GG_SIG)
  let ebeyond: i64 = g4_envelope(0, GG_TMU_A + (g4_horizon_sigma() + 1)*GG_SIG)
  gv_puts("  envelope laws: symmetric " as *u8); gv_num(sym1); gv_puts("==" as *u8); gv_num(sym2)
  gv_puts(" | strictly decreasing " as *u8); gv_num(e0); gv_puts(">" as *u8); gv_num(e1); gv_puts(">" as *u8); gv_num(e2); gv_puts(">" as *u8); gv_num(e3)
  gv_puts(" | past horizon=" as *u8); gv_num(ebeyond); gv_puts("\n" as *u8)
  var t2b: i64 = 0
  if sym1 == sym2 { if e0 > e1 { if e1 > e2 { if e2 > e3 { if ebeyond == 0 { t2b = 1 } } } } }
  gv_check("T2b envelope LAWS: symmetric in dt, strictly decreasing, exactly zero past the derived horizon" as *u8, t2b, ctr)
126
  // T3 the kernel is a SIGNED ramp: equal and opposite displacement either side of t_mu.
  g4_bake(GG_TMU_A + GG_SIG, f1)
  g4_bake(GG_TMU_A - GG_SIG, f2)
  let dpos: i64 = f1[0]
  let dneg: i64 = f2[0]
  gv_puts("  antisymmetry: x(t_mu+sig)=" as *u8); gv_num(dpos)
  gv_puts(" x(t_mu-sig)=" as *u8); gv_num(dneg); gv_puts("\n" as *u8)
  var t3: i64 = 0
  if dpos == 0 - dneg { if dpos != 0 { t3 = 1 } }
  gv_check("T3 signed kernel: displacement either side of t_mu is equal and opposite, and NOT zero" as *u8, t3, ctr)
137
  // T4 ★ANTI-VACUITY -- TEMPORAL LOCALITY.
  g4_bake(GG_TMU_A + GG_SIG, f1)
  let amoved: i64 = f1[0] - 0
  let bmoved: i64 = f1[1*st] - 6000
  gv_puts("  locality at t=" as *u8); gv_num(GG_TMU_A + GG_SIG)
  gv_puts(": A(t_mu=" as *u8); gv_num(GG_TMU_A); gv_puts(") moved " as *u8); gv_num(amoved)
  gv_puts(" | B(t_mu=" as *u8); gv_num(GG_TMU_B); gv_puts(", same motion) moved " as *u8); gv_num(bmoved); gv_puts("\n" as *u8)
  var t4: i64 = 0
  if amoved != 0 { if bmoved == 0 { t4 = 1 } }
  gv_check("T4 anti-vacuity temporal locality: identical motion, different t_mu -- one moves, the other does NOT" as *u8, t4, ctr)
148
  // T5 the 4D state reaches PIXELS, judged by a CONTROL rather than a pixel-count threshold: the same
  // time rendered twice must differ in ZERO pixels, and two different times must differ in MORE. That
  // proves the change is caused by time and not by nondeterminism -- which a threshold cannot show.
  let W: i64 = gs_w()
  let H: i64 = gs_h()
  let npx: i64 = W*H
  let fb1: *i64 = sys_mmap(npx*8) as *i64
  let fb2: *i64 = sys_mmap(npx*8) as *i64
  let fb3: *i64 = sys_mmap(npx*8) as *i64
  let acc: *i64 = sys_mmap(npx*3*8) as *i64
  let trn: *i64 = sys_mmap(npx*8) as *i64
  let dep: *i64 = sys_mmap(GG_CAP*8) as *i64
  let sxb: *i64 = sys_mmap(GG_CAP*8) as *i64
  let syb: *i64 = sys_mmap(GG_CAP*8) as *i64
  let pa: *i64 = sys_mmap(GG_CAP*8) as *i64
  let pb: *i64 = sys_mmap(GG_CAP*8) as *i64
  let pc: *i64 = sys_mmap(GG_CAP*8) as *i64
  let pdt: *i64 = sys_mmap(GG_CAP*8) as *i64
  let ord: *i64 = sys_mmap(GG_CAP*8) as *i64
  let cnt: *i64 = sys_mmap((gs_nb()+2)*8) as *i64
  let elut: *i64 = sys_mmap(gs_expn()*8) as *i64
  gs_build_explut(elut)
  let bg: i64 = 26 + 28*256 + 44*65536
  g4_bake(GG_TMU_A, f1)
  gs_render_aniso(f1, ng, 0, 14, fb1, acc, trn, dep, sxb, syb, pa, pb, pc, pdt, ord, cnt, elut, 26, 28, 44)
  g4_bake(GG_TMU_A, f3)
  gs_render_aniso(f3, ng, 0, 14, fb3, acc, trn, dep, sxb, syb, pa, pb, pc, pdt, ord, cnt, elut, 26, 28, 44)
  g4_bake(GG_TMU_A + GG_SIG, f2)
  gs_render_aniso(f2, ng, 0, 14, fb2, acc, trn, dep, sxb, syb, pa, pb, pc, pdt, ord, cnt, elut, 26, 28, 44)
  let same_time: i64 = gg_pixdiff(fb1, fb3, npx)
  let diff_time: i64 = gg_pixdiff(fb1, fb2, npx)
  var lit: i64 = 0
  var pi: i64 = 0
  while pi < npx { if fb2[pi] != bg { lit = lit + 1 } pi = pi + 1 }
  write_png(fb2, W, H, "knowledge/nx_gsplat4d_wave.png" as *u8)
  gv_puts("  render: lit=" as *u8); gv_num(lit)
  gv_puts(" | CONTROL same-time pixels changed=" as *u8); gv_num(same_time)
  gv_puts(" | different-time pixels changed=" as *u8); gv_num(diff_time)
  gv_puts(" artifact knowledge/nx_gsplat4d_wave.png\n" as *u8)
  var t5: i64 = 0
  if same_time == 0 { if diff_time > same_time { if lit > 0 { t5 = 1 } } }
  gv_check("T5 the temporal state reaches PIXELS: same time changes NOTHING, a different time changes something" as *u8, t5, ctr)
191
  // T6 the frame cache cannot lie: a slot must equal a direct bake at that same t, byte for byte.
  g4_ring_prime(1000, 200)
  g4_bake(1200, f1)
  let slot: i64 = g4_ring_find(1200)
  var t6: i64 = 0
  if slot >= 0 { if gg_cmp(g4_ring_frame(slot), f1, ng*st) == 1 { t6 = 1 } }
  gv_puts("  ring: t=1200 resident in slot " as *u8); gv_num(slot)
  gv_puts(", byte-equal to a direct bake=" as *u8); gv_num(t6); gv_puts("\n" as *u8)
  gv_check("T6 frame cache honesty: a cached frame is byte-identical to baking that time directly" as *u8, t6, ctr)
201
  // T7 the ring is BOUNDED and evicts the oldest.
  let vic: i64 = g4_ring_advance(200)
  var live: i64 = 0
  var s: i64 = 0
  while s < g4_ring_depth() { live = live + g4_ring_valid(s); s = s + 1 }
  let gone: i64 = g4_ring_find(1000)
  let fresh: i64 = g4_ring_find(1600)
  gv_puts("  ring advance: recycled slot " as *u8); gv_num(vic)
  gv_puts(", t=1000 now " as *u8); gv_num(gone)
  gv_puts(" (-1 = evicted), t=1600 in slot " as *u8); gv_num(fresh)
  gv_puts(", live slots=" as *u8); gv_num(live); gv_puts("\n" as *u8)
  var t7: i64 = 0
  if gone == 0 - 1 { if fresh >= 0 { if live == g4_ring_depth() { t7 = 1 } } }
  gv_check("T7 the frame cache is BOUNDED: advancing evicts the oldest and never grows past its declared depth" as *u8, t7, ctr)
216
  // T8 determinism
  g4_bake(1337, f1)
  g4_bake(1337, f2)
  gv_check("T8 deterministic: the same time bakes byte-identical state" as *u8, gg_cmp(f1, f2, ng*st), ctr)
221
  // ★T9/T10/T10b/T11 -- THE DENY-GUARDS, ASKED BOTH DIRECTIONS. A suite that only asks "was it refused?"
  // is blind by construction. ⚠T10b exists because nx_gate_bite SURVIVED a mutant in the diagnostic path:
  // a guard whose message length computes to zero refuses SILENTLY, and every code-only tooth passes.
  let r9bad: i64 = g4_set_time(0, GG_TMU_A, 0)
  let r9good: i64 = g4_set_time(0, GG_TMU_A, GG_SIG)
  let r10bad: i64 = g4_set_rest(GG_CAP + 5, 0, 0, 0, 0, 0, 0-256, 10, 1, 1, 1, 1)
  let r10good: i64 = g4_set_rest(2, 0-6000, 0, 0, 0, 0, 0-256, 400, 240, 240, 240, 256)
  gv_puts("  sigma guard: bad=" as *u8); gv_num(r9bad); gv_puts(" good=" as *u8); gv_num(r9good)
  gv_puts(" | range guard: bad=" as *u8); gv_num(r10bad); gv_puts(" good=" as *u8); gv_num(r10good); gv_puts("\n" as *u8)
  var t9: i64 = 0
  if r9bad == 0 - 3 { if r9good == 0 { t9 = 1 } }
  gv_check("T9 sigma guard NAMES its rule (-3) and has a POSITIVE CONTROL: a valid window is accepted" as *u8, t9, ctr)
  var t10: i64 = 0
  if r10bad == 0 - 5 { if r10good == 0 { t10 = 1 } }
  gv_check("T10 range guard NAMES its rule (-5) and has a POSITIVE CONTROL: an in-range index is accepted" as *u8, t10, ctr)
237
  // T10b the diagnostic path can measure its own message. Asserting the length of a literal against
  // that same literal is the definition of a length function, not a tuned constant.
  var t10b: i64 = 0
  if g4_slen("" as *u8) == 0 { if g4_slen("ab" as *u8) == 2 { t10b = 1 } }
  gv_puts("  diagnostic path: slen(empty)=" as *u8); gv_num(g4_slen("" as *u8))
  gv_puts(" slen(ab)=" as *u8); gv_num(g4_slen("ab" as *u8)); gv_puts("\n" as *u8)
  gv_check("T10b a refusal that cannot measure its own message prints nothing: the length function is correct" as *u8, t10b, ctr)
245
  // T11 the prefetch depth is CHOSEN BY THE CALLER, and the structural floor is enforced both ways: a
  // depth that cannot hold the frame in use plus one ahead is not a prefetch cache.
  let rbad: i64 = g4_init(GG_CAP, g4_ring_min() - 1)
  let rgood: i64 = g4_init(GG_CAP, g4_ring_min())
  gv_puts("  ring-depth guard: below floor=" as *u8); gv_num(rbad)
  gv_puts(" at floor=" as *u8); gv_num(rgood)
  gv_puts(" depth now=" as *u8); gv_num(g4_ring_depth()); gv_puts("\n" as *u8)
  var t11: i64 = 0
  if rbad == 0 - 6 { if rgood == 0 { if g4_ring_depth() == g4_ring_min() { t11 = 1 } } }
  gv_check("T11 prefetch depth is the CALLER'S choice, with a structural floor enforced both ways" as *u8, t11, ctr)
256
  // T12 the arena COUNTS ITSELF. No expected byte total is written here -- writing one would recreate
  // the hand-maintained count this organ was changed to eliminate. What is asserted instead is that the
  // number is real and behaves like a measurement: non-zero, and tracking the capacity it was given.
  g4_init(GG_CAP*4, GG_RING)
  let bbig: i64 = g4_bytes()
  gv_puts("  arena: " as *u8); gv_num(bbig)
  gv_puts(" bytes at capacity " as *u8); gv_num(g4_cap())
  gv_puts(", counted by construction at every allocation\n" as *u8)
  var t12: i64 = 0
  if bbig > 0 { if g4_cap() == GG_CAP*4 { t12 = 1 } }
  gv_check("T12 the arena counts itself: bytes are accumulated at every allocation, never hand-maintained" as *u8, t12, ctr)
268
  let rc: i64 = gv_verdict("GSPLAT4D-GATE" as *u8, ctr, "the temporal axis is real: exact envelope identities, laws instead of tolerances, controls instead of thresholds, refusals that fail closed" as *u8)
  sys_exit(rc)
  return rc
272}
nx_gsplat4d_gate.nx source

`nx_gsplat4d_gate.nx` source
