nx_determinism_test.nx source
↩ module page · 80 lines · 3105 B
1// nx_determinism_test.nx -- 1:1 KAT for the rollback sync-test harness
2// (nx_determinism.nx). Proves: (a) the deterministic integer sim survives
3// per-frame rollback with ZERO divergence, and (b) -- the load-bearing
4// negative control -- the harness DETECTS non-determinism (a sim with
5// hidden state outside the snapshot), so the gate is real, not a rubber
6// stamp.
7//
8// expect_exit: 0
9// license_tier: ORIGINAL
10
11import "nx_determinism.nx"
12
13// hidden state OUTSIDE any snapshot -> the #1 rollback desync cause.
14static g_hidden: i64
15
16func det_sim_step_buggy(state: *i64, nwords: i64, input: i64) -> i64 {
17 g_hidden = g_hidden + 1 // not captured by det_copy snapshots
18 var i: i64 = 0
19 while i < nwords {
20 state[i] = state[i] + input + g_hidden
21 i = i + 1
22 }
23 return 0
24}
25// same GGPO loop as det_rollback_verify but driving the BUGGY sim.
26func det_buggy_verify(t: *i64, state0: *i64, nwords: i64, inputs: *i64, nframes: i64) -> i64 {
27 let live: *i64 = sys_mmap(nwords * 8 + 16) as *i64
28 let save: *i64 = sys_mmap(nwords * 8 + 16) as *i64
29 let alt: *i64 = sys_mmap(nwords * 8 + 16) as *i64
30 var mism: i64 = 0
31 det_copy(live, state0, nwords)
32 var f: i64 = 0
33 while f < nframes {
34 det_copy(save, live, nwords)
35 det_sim_step_buggy(live, nwords, inputs[f])
36 det_copy(alt, save, nwords)
37 det_sim_step_buggy(alt, nwords, inputs[f])
38 let ck_live: i64 = det_state_checksum(t, live, nwords)
39 let ck_alt: i64 = det_state_checksum(t, alt, nwords)
40 if ck_alt != ck_live { mism = mism + 1 }
41 f = f + 1
42 }
43 return mism
44}
45
46func main() -> i64 {
47 let t: *i64 = crc32c_build_table()
48 let NW: i64 = 8
49 let NF: i64 = 20
50 let state0: *i64 = sys_mmap(NW * 8) as *i64
51 let inputs: *i64 = sys_mmap(NF * 8) as *i64
52 var i: i64 = 0
53 while i < NW { state0[i] = (i * 1000 + 7); i = i + 1 }
54 i = 0
55 while i < NF { inputs[i] = ((i * 13 + 5) & 0xff); i = i + 1 }
56
57 // ---- T1: deterministic sim survives per-frame rollback -> 0 divergence ----
58 if det_rollback_verify(t, state0, NW, inputs, NF) != 0 { return 1 }
59
60 // ---- T2: holds for a different input stream too ----
61 i = 0
62 while i < NF { inputs[i] = ((i * 31 + 17) & 0x1ff); i = i + 1 }
63 if det_rollback_verify(t, state0, NW, inputs, NF) != 0 { return 2 }
64
65 // ---- T3 (negative control): the harness DETECTS non-determinism ----
66 g_hidden = 0
67 let caught: i64 = det_buggy_verify(t, state0, NW, inputs, NF)
68 if caught <= 0 { return 3 } // MUST flag the hidden-state desync
69
70 sys_write(1, "DETERMINISM KAT PASS (deterministic sim: 0 rollback divergence; harness CATCHES hidden-state desync: ", 100)
71 // print how many frames the buggy sim was caught on
72 let d: *u8 = sys_mmap(8)
73 var m: i64 = caught
74 var k: i64 = 0
75 while m > 0 { d[k] = (0x30 + (m % 10)) as u8; m = m / 10; k = k + 1 }
76 var j: i64 = k - 1
77 while j >= 0 { let one: *u8 = sys_mmap(1); one[0] = d[j]; sys_write(1, one, 1); j = j - 1 }
78 sys_write(1, "/20 frames)\n", 12)
79 return 0
80}