nx_rollback_gate.nx source

1// nx_rollback_gate.nx -- proves N-R4 rollback. Ground-truth inputs R; PREDICTED inputs P are wrong at 2// tick 3 (P[3]=R[3]+1). Without rollback, the predicted run DIVERGES from truth. Rollback restores the 3// confirmed snapshot (state after the correct ticks 0-2) and re-sims with REAL inputs -> must reach the 4// EXACT ground-truth state. GREEN only if: misprediction detected, naive run != truth (error was real), 5// rollback-corrected == truth (recovered), and no false rollback on a correct tick. license_tier: ORIGINAL expect_exit: 0 6import "nx_syscalls.nx" 7import "nx_lockstep.nx" 8import "nx_rollback.nx" 9 10func rw(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 11func rn(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 } 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 N: i64 = 8 // ticks 18 let CONF: i64 = 3 // confirmed through tick 2; tick 3 was mispredicted 19 20 let R: *i64 = sys_mmap(8 * 8) as *i64 21 let P: *i64 = sys_mmap(8 * 8) as *i64 22 R[0]=3; R[1]=1; R[2]=4; R[3]=1; R[4]=5; R[5]=9; R[6]=2; R[7]=6 23 var i: i64 = 0 24 while i < N { P[i] = R[i]; i = i + 1 } 25 P[3] = R[3] + 1 // misprediction at tick 3 26 27 var pass: i64 = 0 28 var total: i64 = 0 29 30 // ground truth 31 let truth: *i64 = sys_mmap(8 * 8) as *i64 32 zero(truth, SN); rb_advance(truth, K, R, 0, N) 33 let truth_c: i64 = ls_checksum(truth, SN) 34 35 // naive predicted run (no rollback) 36 let naive: *i64 = sys_mmap(8 * 8) as *i64 37 zero(naive, SN); rb_advance(naive, K, P, 0, N) 38 let naive_c: i64 = ls_checksum(naive, SN) 39 40 // misprediction detected at tick 3; no false detection at tick 2 (correct) 41 total=total+1; if rb_mispredict(P, R, 3) == 1 { pass=pass+1 } else { rw("R1 FAIL misprediction not detected\n") } 42 total=total+1; if rb_mispredict(P, R, 2) == 0 { pass=pass+1 } else { rw("R2 FAIL false rollback on correct tick\n") } 43 44 // without rollback, the predicted state is WRONG (neg-control: the error is real) 45 total=total+1; if naive_c != truth_c { pass=pass+1 } else { rw("R3 FAIL naive matched truth (no error to fix?)\n") } 46 47 // ROLLBACK: snapshot = state after confirmed ticks 0..CONF, then re-sim with REAL inputs CONF..N 48 let snap: *i64 = sys_mmap(8 * 8) as *i64 49 zero(snap, SN); rb_advance(snap, K, R, 0, CONF) 50 let corrected: *i64 = sys_mmap(8 * 8) as *i64 51 rb_resim(corrected, snap, K, R, CONF, N) 52 let corrected_c: i64 = ls_checksum(corrected, SN) 53 total=total+1; if corrected_c == truth_c { pass=pass+1 } else { rw("R4 FAIL rollback did NOT recover truth\n") } 54 55 rw("=== ROLLBACK (mispredict @tick3, confirm@"); rn(CONF); rw(") ===\n") 56 rw(" truth_cksum="); rn(truth_c); rw("\n") 57 rw(" naive_cksum="); rn(naive_c); rw(" (diverged: "); if naive_c!=truth_c { rw("YES") } else { rw("no") } rw(")\n") 58 rw(" corrected_cksum="); rn(corrected_c); rw(" (recovered truth: "); if corrected_c==truth_c { rw("YES") } else { rw("no") } rw(")\n") 59 rw("ROLLBACK "); rn(pass); rw("/"); rn(total); rw("\n") 60 if pass == total { rw("ROLLBACK ALL-PASS (mispredict detected + naive wrong + rollback recovers ground truth)\n"); sys_exit(0) } 61 sys_exit(1) 62 return 1 63}