nx_lockstep_gate.nx source

1// nx_lockstep_gate.nx -- proves N-R2 deterministic lockstep + desync detection. Two "clients" run the 2// SAME input stream and must stay checksum-identical every tick (lockstep). A fresh re-run must reproduce 3// the exact final checksum (determinism). NEG-CONTROL: perturb ONE client's input at one tick -> the 4// checksums MUST diverge (desync detected) -- if they didn't, the detector would be useless. GREEN only 5// if all hold. license_tier: ORIGINAL expect_exit: 0 6import "nx_syscalls.nx" 7import "nx_lockstep.nx" 8 9func lw(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 10func ln(v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m;sys_write(1,"-" as *u8,1)} let t: *u8=sys_mmap(28); 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{bb[i]=t[k-1-i];i=i+1} sys_write(1,bb,k); return 0 } 11 12func zero(s: *i64, n: i64) -> i64 { var i: i64=0; while i<n { s[i]=0; i=i+1 } return 0 } 13 14func main() -> i64 { 15 let K: i64 = 4 16 let SN: i64 = 8 // 2*K 17 let NT: i64 = 8 18 let inputs: *i64 = sys_mmap(8 * 8) as *i64 19 inputs[0]=3; inputs[1]=1; inputs[2]=4; inputs[3]=1; inputs[4]=5; inputs[5]=9; inputs[6]=2; inputs[7]=6 20 21 let a: *i64 = sys_mmap(8 * 8) as *i64 22 let b: *i64 = sys_mmap(8 * 8) as *i64 23 zero(a, SN); zero(b, SN) 24 25 var pass: i64 = 0 26 var total: i64 = 0 27 28 // ---- LOCKSTEP: two clients, same inputs, checksum-identical EVERY tick ---- 29 var tickmatch: i64 = 1 30 var t: i64 = 0 31 while t < NT { 32 ls_update(a, K, inputs[t]) 33 ls_update(b, K, inputs[t]) 34 if ls_checksum(a, SN) != ls_checksum(b, SN) { tickmatch = 0 } 35 t = t + 1 36 } 37 total=total+1; if tickmatch==1 { pass=pass+1 } else { lw("L1 FAIL clients diverged under identical inputs\n") } 38 39 // ---- DETERMINISM: a fresh re-run reproduces the exact final checksum ---- 40 let c: *i64 = sys_mmap(8 * 8) as *i64 41 zero(c, SN) 42 let csum: i64 = ls_run(c, K, inputs, NT) 43 total=total+1; if csum == ls_checksum(a, SN) { pass=pass+1 } else { lw("L2 FAIL not reproducible\n") } 44 45 // ---- DESYNC NEG-CONTROL: perturb client B's input at tick 3 -> checksums MUST diverge ---- 46 let d: *i64 = sys_mmap(8 * 8) as *i64 47 let e: *i64 = sys_mmap(8 * 8) as *i64 48 zero(d, SN); zero(e, SN) 49 var t2: i64 = 0 50 while t2 < NT { 51 ls_update(d, K, inputs[t2]) 52 var ein: i64 = inputs[t2] 53 if t2 == 3 { ein = ein + 1 } // ONE different input on client E 54 ls_update(e, K, ein) 55 t2 = t2 + 1 56 } 57 total=total+1; if ls_checksum(d, SN) != ls_checksum(e, SN) { pass=pass+1 } else { lw("L3 FAIL desync NOT detected (detector useless)\n") } 58 59 // ---- and a clean run with the SAME inputs as d must MATCH d (desync only from the perturbation) ---- 60 let f: *i64 = sys_mmap(8 * 8) as *i64 61 zero(f, SN) 62 let fcsum: i64 = ls_run(f, K, inputs, NT) 63 total=total+1; if fcsum == ls_checksum(d, SN) { pass=pass+1 } else { lw("L4 FAIL clean run mismatch\n") } 64 65 lw("LOCKSTEP "); ln(pass); lw("/"); ln(total) 66 lw(" final_checksum="); ln(csum); lw("\n") 67 if pass == total { lw("LOCKSTEP ALL-PASS (lockstep determinism + reproducible + desync detected)\n"); sys_exit(0) } 68 sys_exit(1) 69 return 1 70}