code wiki / _hdl_build / nx_netsync_gate.nx
nx_netsync_gate.nx source
↩ module page · 490 lines · 20593 B
1// nx_netsync_gate.nx -- CERTIFICATION of nx_netsync (gamebench gap-queue rank 1: networking-multiplayer).
2// The existing nx_lockstep/nx_rollback gates prove netcode mechanisms on a TOY stepper; this gate proves
3// the same laws hold when the simulation is the REAL certified world (nx_worldsim) and the snapshots are
4// REAL save files (nx_gamesave) -- the composition the capability actually demands.
5// T1 LOCKSTEP DETERMINISM -- two peers, same commands, different within-tick arrival order,
6// 200 ticks -> checksums equal EVERY tick and shared state word-exact
7// T2 STALL-NOT-GUESS -- missing one peer's input for a tick freezes the session (no advance, no state
8// change) until it arrives; advancing on partial input is THE lockstep desync bug
9// T3 ARRIVAL-CHAOS IMMUNE -- the full 400-command schedule delivered in a shuffled order with
10// duplicates -> final state EXACTLY equals the in-order run; a conflicting resend is REFUSED
11// T4 DESYNC LOCALIZED -- a 1-unit wealth mint injected into one peer at tick 120 is first visible in
12// the checksum stream AT tick 120 (never earlier, never missed)
13// T5 ROLLBACK ON THE REAL SIM -- speculative head with predicted inputs diverges when the prediction
14// was wrong; discard + resim from the confirmed state converges bit-exact to ground truth; a
15// CORRECT prediction triggers no divergence (no false rollback)
16// T6 LATE-JOIN VIA nx_gamesave -- a peer that loads a mid-session snapshot file into a ZEROED arena
17// tracks the original checksum-for-checksum to the end (GX-9 transparency)
18// T7 BOUNDED + LOUD -- out-of-range tick/peer and conflicting input each refuse with a DISTINCT code
19// and change nothing
20// T8 ANTI-VACUITY -- the session actually traded and grew (a frozen or all-no-op world would pass
21// T1-T3 while proving nothing)
22// T9 ARTIFACT -- the final session round-trips through a real save file and RESUMES identically;
23// knowledge/nx_netsync_session.sav is the board evidence
24// license_tier: ORIGINAL expect_exit: 0
25import "nx_syscalls.nx"
26import "nx_netsync.nx"
27import "nx_gamesave.nx"
28import "nx_net_chan.nx"
29import "nx_gate_verdict.nx"
30const K_MAGIC_25214903917: i64 = 25214903917
31const K_MAGIC_2654435761: i64 = 2654435761
32const K_MAGIC_100000000: i64 = 100000000
33const K_MAGIC_1000000: i64 = 1000000
34const K_MAGIC_4242: i64 = 4242
35const K_MAGIC_20260730: i64 = 20260730
36const K_MAGIC_60621: i64 = 60621
37const K_MAGIC_1785425000: i64 = 1785425000
38const K_MAGIC_9750: i64 = 9750
39const K_MAGIC_60620: i64 = 60620
40const K_MAGIC_38921: i64 = 38921
41const K_MAGIC_31337: i64 = 31337
42
43func pw(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
44func pn(v: i64) -> i64 {
45 if v==0 { sys_write(1,"0" as *u8,1); return 0 }
46 var m: i64=v; if m<0 { sys_write(1,"-" as *u8,1); m=0-m }
47 let t: *u8=sys_mmap(32); var k: i64=0
48 while m>0 { t[k]=(48+(m%10)) as u8; m=m/10; k=k+1 }
49 let o: *u8=sys_mmap(32); var q: i64=k-1; var i: i64=0
50 while q>=0 { o[i]=t[q]; i=i+1; q=q-1 }
51 sys_write(1,o,i); return 0
52}
53func lcg(s: *i64) -> i64 { s[0] = ((s[0]*K_MAGIC_25214903917)+11) & 0x7FFFFFFFFFFF; return s[0] }
54
55// the deterministic command schedule -- a pure function of (tick,peer), so every session in this gate
56// independently derives the same "player decisions". ~3/4 of commands are real trade orders.
57func cmd_for(t: i64, p: i64) -> i64 {
58 var x: i64 = t*31 + p*17 + 7
59 x = (x * K_MAGIC_2654435761) & 0x7FFFFFFFFFFFFFFF
60 if x % 4 == 0 { return 0 }
61 let from: i64 = x % 6
62 var to: i64 = (x / 7) % 6
63 if to == from { to = (to + 1) % 6 }
64 let amt: i64 = 100 + ((x / 49) % 300)
65 return from*K_MAGIC_100000000 + to*K_MAGIC_1000000 + amt
66}
67
68const GMAXT: i64 = 300
69const GNFAC: i64 = 6
70// 2 peers, 300 tick capacity, 6 factions
71func mksess(a: *i64, self_id: i64, seed: i64) -> i64 {
72 ns_init(a, 2, self_id, GMAXT, GNFAC, seed)
73 let w: *i64 = ns_world(a)
74 var i: i64 = 0
75 while i < GNFAC {
76 ws_set_res(w, i, 1000 + i*250)
77 ws_set_pop(w, i, 500 + i*100)
78 ws_set_terr(w, i, 3 + i)
79 i = i + 1
80 }
81 return 0
82}
83
84func main() -> i64 {
85 pw("=== nx_netsync_gate: is multiplayer netcode safe to build on the certified parts? ===\n\n")
86 var pass: i64 = 0
87 var checks: i64 = 0
88 let W: i64 = ns_words(2, GMAXT, GNFAC)
89 let AP: *u8 = "knowledge/nx_netsync_session.sav" as *u8
90 let JP: *u8 = "knowledge/nx_netsync_join.sav" as *u8
91 // start clean -- both artifacts must be REGENERATED by this run
92 sys_unlinkat(AP)
93 sys_unlinkat(JP)
94
95 // ---------- T1 lockstep determinism on the real sim ----------
96 checks = checks + 1
97 let A: *i64 = sys_mmap(W*8) as *i64
98 let B: *i64 = sys_mmap(W*8) as *i64
99 mksess(A, 0, K_MAGIC_4242)
100 mksess(B, 1, K_MAGIC_4242)
101 var ckok: i64 = 1
102 var t: i64 = 0
103 while t < 200 {
104 ns_offer(A, t, 0, cmd_for(t,0)); ns_offer(A, t, 1, cmd_for(t,1))
105 ns_offer(B, t, 1, cmd_for(t,1)); ns_offer(B, t, 0, cmd_for(t,0))
106 ns_step(A, 4); ns_step(B, 4)
107 if ns_checksum(A) != ns_checksum(B) { ckok = 0 }
108 t = t + 1
109 }
110 var t1: i64 = 0
111 if ckok==1 { if ns_shared_eq(A,B)==1 { if ns_tick(A)==200 { t1=1 } } }
112 if t1==1 {
113 pw("T1 GREEN lockstep deterministic: 2 peers, 200 ticks, different arrival order -> checksum equal every tick, shared state word-exact (ck=")
114 pn(ns_checksum(A)); pw(")\n"); pass=pass+1
115 } else { pw("T1 RED peers diverged: ckok="); pn(ckok); pw(" tick="); pn(ns_tick(A)); pw("\n") }
116
117 // ---------- T2 stall-not-guess ----------
118 checks = checks + 1
119 let S: *i64 = sys_mmap(W*8) as *i64
120 mksess(S, 0, 777)
121 t = 0
122 while t < 50 {
123 ns_offer(S, t, 0, cmd_for(t,0)); ns_offer(S, t, 1, cmd_for(t,1))
124 t = t + 1
125 }
126 ns_offer(S, 50, 0, cmd_for(50,0))
127 while ns_step(S, 4)==1 {}
128 let stick: i64 = ns_tick(S)
129 let sck: i64 = ns_checksum(S)
130 let z1: i64 = ns_step(S, 4)
131 let z2: i64 = ns_step(S, 4)
132 var t2: i64 = 0
133 if stick==50 { if z1==0 { if z2==0 { if ns_checksum(S)==sck {
134 ns_offer(S, 50, 1, cmd_for(50,1))
135 if ns_step(S, 4)==1 { if ns_tick(S)==51 { t2=1 } }
136 } } } }
137 if t2==1 {
138 pw("T2 GREEN stalls-not-guesses: missing peer-1 input froze tick at 50 (2 step attempts, state untouched); arrival unfroze to 51\n")
139 pass=pass+1
140 } else { pw("T2 RED advanced on partial input: tick="); pn(stick); pw("\n") }
141
142 // ---------- T3 arrival-chaos immune ----------
143 checks = checks + 1
144 let list: *i64 = sys_mmap(400*8) as *i64
145 var i: i64 = 0
146 while i < 400 { list[i]=i; i=i+1 }
147 let rs: *i64 = sys_mmap(8) as *i64
148 rs[0] = K_MAGIC_20260730
149 i = 399
150 while i > 0 {
151 let j: i64 = lcg(rs) % (i+1)
152 let tmp: i64 = list[i]; list[i]=list[j]; list[j]=tmp
153 i = i - 1
154 }
155 let C: *i64 = sys_mmap(W*8) as *i64
156 mksess(C, 0, K_MAGIC_4242)
157 var acc: i64 = 0
158 var dup: i64 = 0
159 i = 0
160 while i < 400 {
161 let k: i64 = list[i]
162 let kt: i64 = k / 2
163 let kp: i64 = k % 2
164 let rc: i64 = ns_offer(C, kt, kp, cmd_for(kt,kp))
165 if rc==1 { acc = acc + 1 }
166 if i % 8 == 0 {
167 let rc2: i64 = ns_offer(C, kt, kp, cmd_for(kt,kp))
168 if rc2==0 { dup = dup + 1 }
169 }
170 while ns_step(C, 4)==1 {}
171 i = i + 1
172 }
173 let ck3: i64 = ns_checksum(C)
174 let rcx: i64 = ns_offer(C, 10, 0, cmd_for(10,0)+1)
175 var t3: i64 = 0
176 if ns_tick(C)==200 { if ns_shared_eq(C,A)==1 { if acc==400 { if dup==50 {
177 if rcx==NS_E_CONFLICT { if ns_checksum(C)==ck3 { t3=1 } } } } } }
178 if t3==1 {
179 pw("T3 GREEN chaos immune: 400 commands shuffled + 50 duplicates -> identical to in-order run; conflicting resend REFUSED, state untouched\n")
180 pass=pass+1
181 } else {
182 pw("T3 RED chaos diverged: tick="); pn(ns_tick(C)); pw(" eq="); pn(ns_shared_eq(C,A))
183 pw(" acc="); pn(acc); pw(" dup="); pn(dup); pw(" rcx="); pn(rcx); pw("\n")
184 }
185
186 // ---------- T4 desync localized to the exact tick ----------
187 checks = checks + 1
188 let A2: *i64 = sys_mmap(W*8) as *i64
189 let B2: *i64 = sys_mmap(W*8) as *i64
190 mksess(A2, 0, 999)
191 mksess(B2, 1, 999)
192 var first_diff: i64 = 0-1
193 t = 0
194 while t < 200 {
195 if t==120 {
196 let wc: *i64 = ns_world(B2)
197 wc[ws_o_res(wc)+0] = wc[ws_o_res(wc)+0] + 1
198 }
199 ns_offer(A2, t, 0, cmd_for(t,0)); ns_offer(A2, t, 1, cmd_for(t,1))
200 ns_offer(B2, t, 0, cmd_for(t,0)); ns_offer(B2, t, 1, cmd_for(t,1))
201 ns_step(A2, 4); ns_step(B2, 4)
202 if ns_checksum(A2) != ns_checksum(B2) { if first_diff < 0 { first_diff = t } }
203 t = t + 1
204 }
205 let mint: i64 = ws_total_res(ns_world(B2)) - ws_total_res(ns_world(A2))
206 var t4: i64 = 0
207 if first_diff==120 { if mint==1 { t4=1 } }
208 if t4==1 {
209 pw("T4 GREEN desync localized: 1-unit mint at tick 120 first flagged AT tick 120 (0 false positives before), audit shows exactly +"); pn(mint); pw(" phantom unit\n")
210 pass=pass+1
211 } else { pw("T4 RED first_diff="); pn(first_diff); pw(" mint="); pn(mint); pw("\n") }
212
213 // ---------- T5 rollback on the real sim ----------
214 checks = checks + 1
215 var TK: i64 = 250
216 while cmd_for(TK,1)==0 { TK = TK + 1 }
217 let GT: *i64 = sys_mmap(W*8) as *i64
218 mksess(GT, 0, 555)
219 t = 0
220 while t < TK+3 {
221 ns_offer(GT, t, 0, cmd_for(t,0)); ns_offer(GT, t, 1, cmd_for(t,1))
222 ns_step(GT, 4)
223 t = t + 1
224 }
225 let P: *i64 = sys_mmap(W*8) as *i64
226 mksess(P, 0, 555)
227 t = 0
228 while t < TK {
229 ns_offer(P, t, 0, cmd_for(t,0)); ns_offer(P, t, 1, cmd_for(t,1))
230 ns_step(P, 4)
231 t = t + 1
232 }
233 let H: *i64 = sys_mmap(W*8) as *i64
234 ns_copy(H, P, W)
235 t = TK
236 while t < TK+3 {
237 ns_offer(H, t, 0, cmd_for(t,0))
238 ns_offer(H, t, 1, 0)
239 ns_step(H, 4)
240 t = t + 1
241 }
242 var mispred: i64 = 0
243 if cmd_for(TK,1) != 0 { mispred = 1 }
244 var hdiv: i64 = 0
245 if ns_shared_eq(H, GT)==0 { hdiv = 1 }
246 t = TK
247 while t < TK+3 {
248 ns_offer(P, t, 0, cmd_for(t,0)); ns_offer(P, t, 1, cmd_for(t,1))
249 ns_step(P, 4)
250 t = t + 1
251 }
252 let conv: i64 = ns_shared_eq(P, GT)
253 var TK2: i64 = 250
254 while cmd_for(TK2,1)!=0 { TK2 = TK2 + 1 }
255 let G2: *i64 = sys_mmap(W*8) as *i64
256 mksess(G2, 0, 555)
257 t = 0
258 while t < TK2 {
259 ns_offer(G2, t, 0, cmd_for(t,0)); ns_offer(G2, t, 1, cmd_for(t,1))
260 ns_step(G2, 4)
261 t = t + 1
262 }
263 let H2: *i64 = sys_mmap(W*8) as *i64
264 ns_copy(H2, G2, W)
265 ns_offer(H2, TK2, 0, cmd_for(TK2,0)); ns_offer(H2, TK2, 1, 0)
266 ns_step(H2, 4)
267 ns_offer(G2, TK2, 0, cmd_for(TK2,0)); ns_offer(G2, TK2, 1, cmd_for(TK2,1))
268 ns_step(G2, 4)
269 let nofalse: i64 = ns_shared_eq(H2, G2)
270 var t5: i64 = 0
271 if mispred==1 { if hdiv==1 { if conv==1 { if nofalse==1 { t5=1 } } } }
272 if t5==1 {
273 pw("T5 GREEN rollback converges: wrong prediction at tick "); pn(TK)
274 pw(" diverged the speculative head; resim from confirmed state == ground truth bit-exact; correct prediction (tick ")
275 pn(TK2); pw(") rolled nothing back\n"); pass=pass+1
276 } else {
277 pw("T5 RED mispred="); pn(mispred); pw(" hdiv="); pn(hdiv); pw(" conv="); pn(conv)
278 pw(" nofalse="); pn(nofalse); pw("\n")
279 }
280
281 // ---------- T6 late-join via nx_gamesave ----------
282 checks = checks + 1
283 let A3: *i64 = sys_mmap(W*8) as *i64
284 mksess(A3, 0, 888)
285 t = 0
286 while t < 150 {
287 ns_offer(A3, t, 0, cmd_for(t,0)); ns_offer(A3, t, 1, cmd_for(t,1))
288 ns_step(A3, 4)
289 t = t + 1
290 }
291 let jw: i64 = gs_save(JP, K_MAGIC_60621, A3, W, K_MAGIC_1785425000)
292 let C3: *i64 = sys_mmap(W*8) as *i64
293 let jr: i64 = gs_load(JP, C3, W, 0 as *i64)
294 C3[1] = 1
295 var jok: i64 = 1
296 t = 150
297 while t < 200 {
298 ns_offer(A3, t, 0, cmd_for(t,0)); ns_offer(A3, t, 1, cmd_for(t,1))
299 ns_offer(C3, t, 0, cmd_for(t,0)); ns_offer(C3, t, 1, cmd_for(t,1))
300 ns_step(A3, 4); ns_step(C3, 4)
301 if ns_checksum(A3) != ns_checksum(C3) { jok = 0 }
302 t = t + 1
303 }
304 var t6: i64 = 0
305 if jw > 0 { if jr==W { if jok==1 { if ns_shared_eq(A3,C3)==1 { if ns_tick(C3)==200 { t6=1 } } } } }
306 if t6==1 {
307 pw("T6 GREEN late-join: peer loaded the tick-150 snapshot file ("); pn(jw)
308 pw("B) into a ZEROED arena and tracked the host checksum-for-checksum to tick 200\n"); pass=pass+1
309 } else { pw("T6 RED jw="); pn(jw); pw(" jr="); pn(jr); pw(" jok="); pn(jok); pw("\n") }
310
311 // ---------- T7 bounded + loud ----------
312 checks = checks + 1
313 let S7: *i64 = sys_mmap(W*8) as *i64
314 mksess(S7, 0, 111)
315 let ckb: i64 = ns_checksum(S7)
316 let r1: i64 = ns_offer(S7, 0-1, 0, 5)
317 let r2: i64 = ns_offer(S7, GMAXT, 0, 5)
318 let r3: i64 = ns_offer(S7, 5, 2, 5)
319 ns_offer(S7, 5, 0, 7)
320 let r4: i64 = ns_offer(S7, 5, 0, 8)
321 let r5: i64 = ns_offer(S7, 5, 0, 7)
322 var t7: i64 = 0
323 if r1==NS_E_TICK { if r2==NS_E_TICK { if r3==NS_E_PEER { if r4==NS_E_CONFLICT { if r5==NS_DUP {
324 if ns_checksum(S7)==ckb { t7=1 } } } } } }
325 if t7==1 {
326 pw("T7 GREEN bounded+loud: tick/peer/conflict refusals distinct ("); pn(r1); pw("/"); pn(r3)
327 pw("/"); pn(r4); pw("), duplicate idempotent ("); pn(r5); pw("), shared state untouched\n"); pass=pass+1
328 } else {
329 pw("T7 RED codes r1="); pn(r1); pw(" r2="); pn(r2); pw(" r3="); pn(r3)
330 pw(" r4="); pn(r4); pw(" r5="); pn(r5); pw("\n")
331 }
332
333 // ---------- T8 anti-vacuity ----------
334 checks = checks + 1
335 var sched_nz: i64 = 0
336 t = 0
337 while t < 200 {
338 if cmd_for(t,0)!=0 { sched_nz = sched_nz + 1 }
339 if cmd_for(t,1)!=0 { sched_nz = sched_nz + 1 }
340 t = t + 1
341 }
342 let wA: *i64 = ns_world(A)
343 var relmoved: i64 = 0
344 i = 0
345 while i < GNFAC {
346 var jj: i64 = i+1
347 while jj < GNFAC {
348 if ws_rel(wA, i, jj) != 0 { relmoved = 1 }
349 jj = jj + 1
350 }
351 i = i + 1
352 }
353 var t8: i64 = 0
354 if ns_applied(A) >= 50 { if ns_moved(A) > 0 { if ws_total_res(wA) > K_MAGIC_9750 {
355 if relmoved==1 { if sched_nz >= 100 { t8=1 } } } } }
356 if t8==1 {
357 pw("T8 GREEN anti-vacuity: "); pn(ns_applied(A)); pw(" trades moved "); pn(ns_moved(A))
358 pw(" units over "); pn(sched_nz); pw(" real commands; wealth 9750 -> "); pn(ws_total_res(wA))
359 pw("; relations moved -- the session actually simulates\n"); pass=pass+1
360 } else {
361 pw("T8 RED applied="); pn(ns_applied(A)); pw(" moved="); pn(ns_moved(A))
362 pw(" total="); pn(ws_total_res(wA)); pw(" relmoved="); pn(relmoved); pw("\n")
363 }
364
365 // ---------- T9 artifact round-trip + resume ----------
366 checks = checks + 1
367 let aw: i64 = gs_save(AP, K_MAGIC_60620, A, W, K_MAGIC_1785425000)
368 let RD: *i64 = sys_mmap(W*8) as *i64
369 let ar: i64 = gs_load(AP, RD, W, 0 as *i64)
370 var exact: i64 = 1
371 i = 0
372 while i < W { if RD[i]!=A[i] { exact=0 } i=i+1 }
373 var t9: i64 = 0
374 if aw > 0 { if ar==W { if exact==1 {
375 ns_offer(A, 200, 0, cmd_for(200,0)); ns_offer(A, 200, 1, cmd_for(200,1))
376 ns_offer(RD, 200, 0, cmd_for(200,0)); ns_offer(RD, 200, 1, cmd_for(200,1))
377 ns_step(A, 4); ns_step(RD, 4)
378 if ns_shared_eq(A, RD)==1 { t9=1 }
379 } } }
380 if t9==1 {
381 pw("T9 GREEN artifact: "); pn(W); pw("-word session ("); pn(aw)
382 pw("B) round-tripped through knowledge/nx_netsync_session.sav word-exact AND resumed stepping identically\n")
383 pass=pass+1
384 } else { pw("T9 RED aw="); pn(aw); pw(" ar="); pn(ar); pw(" exact="); pn(exact); pw("\n") }
385
386 // ---------- T10 REAL-SOCKET TRANSPORT (closes the declared residual) ----------
387 // Two PROCESSES, one per peer, exchange commands over a REAL loopback TCP socket using the
388 // nx_net_chan 8-byte big-endian frame protocol -- the wire is the kernel's, not a model.
389 // Property: sessions converge tick-for-tick across the socket; final checksums exchanged OVER
390 // THE WIRE must match and the child must exit clean. A bind failure (port squat) FAILS LOUD
391 // rather than skipping -- the throwaway-port lesson: a tooth must verify its own listener.
392 checks = checks + 1
393 var t10: i64 = 0
394 let NSPORT: i64 = K_MAGIC_38921
395 let lfd: i64 = nx_sock_socket(NX_AF_INET, NX_SOCK_STREAM, NX_IPPROTO_TCP)
396 var bok: i64 = 0
397 if lfd >= 0 {
398 nx_sock_reuseaddr(lfd)
399 let sa: *u8 = sys_mmap(16)
400 nx_sock_sin_init(sa, 0x0100007F, NSPORT)
401 if nx_sock_bind(lfd, sa, 16) >= 0 { if nx_sock_listen(lfd, 1) >= 0 { bok = 1 } }
402 }
403 if bok == 0 {
404 pw("T10 RED cannot bind loopback port 38921 (squatter or perm) -- refusing to skip\n")
405 }
406 if bok == 1 {
407 let pid: i64 = sys_fork()
408 if pid == 0 {
409 let cfd: i64 = nx_sock_socket(NX_AF_INET, NX_SOCK_STREAM, NX_IPPROTO_TCP)
410 let ca: *u8 = sys_mmap(16)
411 nx_sock_sin_init(ca, 0x0100007F, NSPORT)
412 if cfd < 0 { sys_exit(9) }
413 if nx_sock_connect(cfd, ca, 16) < 0 { sys_exit(9) }
414 let nc: *NxNetChan = nx_net_chan_from_fd(cfd)
415 let SC: *i64 = sys_mmap(W*8) as *i64
416 mksess(SC, 1, K_MAGIC_31337)
417 let rvp: *i64 = sys_mmap(16) as *i64
418 var tt: i64 = 0
419 var bad: i64 = 0
420 while tt < 120 {
421 if nx_net_chan_send(nc, cmd_for(tt,1)) != 0 { bad = 1 }
422 if bad == 0 { if nx_net_chan_recv(nc, rvp) != 0 { bad = 1 } }
423 if bad == 0 {
424 ns_offer(SC, tt, 1, cmd_for(tt,1))
425 ns_offer(SC, tt, 0, rvp[0])
426 ns_step(SC, 4)
427 }
428 tt = tt + 1
429 }
430 if bad == 1 { sys_exit(8) }
431 let myck: i64 = ns_checksum(SC)
432 if nx_net_chan_send(nc, myck) != 0 { sys_exit(8) }
433 if nx_net_chan_recv(nc, rvp) != 0 { sys_exit(8) }
434 if rvp[0] != myck { sys_exit(7) }
435 sys_exit(0)
436 }
437 let afd: i64 = nx_sock_accept(lfd, 0 as *u8, 0 as *i64)
438 var pok: i64 = 1
439 if afd < 0 { pok = 0 }
440 var pck: i64 = 0
441 var rck: i64 = 0
442 let SP: *i64 = sys_mmap(W*8) as *i64
443 if pok == 1 {
444 let np: *NxNetChan = nx_net_chan_from_fd(afd)
445 mksess(SP, 0, K_MAGIC_31337)
446 let rp: *i64 = sys_mmap(16) as *i64
447 var tp: i64 = 0
448 while tp < 120 {
449 if nx_net_chan_send(np, cmd_for(tp,0)) != 0 { pok = 0 }
450 if pok == 1 { if nx_net_chan_recv(np, rp) != 0 { pok = 0 } }
451 if pok == 1 {
452 ns_offer(SP, tp, 0, cmd_for(tp,0))
453 ns_offer(SP, tp, 1, rp[0])
454 ns_step(SP, 4)
455 }
456 tp = tp + 1
457 }
458 pck = ns_checksum(SP)
459 if pok == 1 { if nx_net_chan_recv(np, rp) != 0 { pok = 0 } }
460 if pok == 1 { rck = rp[0] }
461 nx_net_chan_send(np, pck)
462 }
463 let stp: *i64 = sys_mmap(16) as *i64
464 stp[0] = 0
465 sys_wait4(pid, stp, 0)
466 let cexit: i64 = (stp[0] >> 8) & 255
467 if pok == 1 { if cexit == 0 { if rck == pck { if ns_tick(SP) == 120 { if ns_applied(SP) > 0 {
468 t10 = 1
469 } } } } }
470 if t10 == 1 {
471 pw("T10 GREEN real-socket transport: 2 processes, 120 ticks over loopback TCP (nx_net_chan 8B-BE frames), checksums exchanged OVER THE WIRE match (ck=")
472 pn(pck); pw("), child exit 0 -- the residual is closed by execution, not declaration\n")
473 pass = pass + 1
474 } else {
475 pw("T10 RED socket lockstep failed: pok="); pn(pok); pw(" child-exit="); pn(cexit)
476 pw(" pck="); pn(pck); pw(" rck="); pn(rck); pw(" tick="); pn(ns_tick(SP)); pw("\n")
477 }
478 }
479
480 pw("\n=== nx_netsync_gate "); pn(pass); pw("/"); pn(checks)
481 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
482 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
483 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
484 let ctr__dry: *i64 = gv_ctr()
485 ctr__dry[0] = pass
486 ctr__dry[1] = checks
487 let rc__dry: i64 = gv_verdict("NETSYNC-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
488 sys_exit(rc__dry)
489 return rc__dry
490}