nx_interp_ex_gate.nx source

1// nx_interp_ex_gate.nx -- proves + MEASURES sovereign dead-reckoning extrapolation (nx_interp ip_sample_ex): 2// during a LOSS BURST (rt runs past the newest snapshot) the peer keeps MOVING from estimated velocity 3// instead of freezing, capped at a safe horizon so long loss holds (bounded) rather than diverging. 4// 1) extrapolation tracks truth during a loss burst (measured err ~0 on steady motion) 5// 2) EXCEED vs hold (neg-control = NET-R1 freeze): extrap_max_err << hold_max_err (measured) 6// 3) horizon cap (neg): beyond max_extrap_ms it HOLDS (status 3, bounded) -- no runaway divergence 7// 4) interior unchanged: ip_sample_ex delegates to ip_sample for in-bracket rt (regression) 8// 5) no-data (neg): empty history -> 0 9// Built nx_cc_sovereign -> nxasm_x86 (no gcc, no .sh). license_tier: ORIGINAL 10import "nx_syscalls.nx" 11import "nx_gate_emit_lib.nx" 12import "nx_interp.nx" 13import "nx_gate_verdict.nx" 14 15func g_abs(v: i64) -> i64 { if v < 0 { return 0 - v } return v } 16func mkf(f: *i64, x: i64) -> i64 { var i: i64=0; while i<10 { f[i]=0; i=i+1 } f[0]=x; return 0 } 17 18func main() -> i64 { 19 g_puts("nx_interp_ex gate (sovereign dead-reckoning: keep moving during loss, no freeze, bounded)\n" as *u8) 20 var pass: i64 = 0; var total: i64 = 0 21 22 let K: i64 = 16 23 let hist: *i64 = sys_mmap((1 + K*IP_STRIDE) * 8) as *i64 24 ip_init(hist) 25 let f: *i64 = sys_mmap(10*8) as *i64 26 let out: *i64 = sys_mmap(10*8) as *i64 27 28 // steady motion val(t)=t/2, samples 0..500 received; then 600/700/800 LOST (newest = 500) 29 var t: i64 = 0 30 while t <= 500 { mkf(f, t/2); ip_push(hist, K, t, f); t = t + 100 } 31 let MAXEX: i64 = 400 32 33 // 1)+2) during the loss burst rt=600..800: extrapolate vs hold 34 var ex_max: i64 = 0; var hold_max: i64 = 0 35 var rt: i64 = 600 36 while rt <= 800 { 37 ip_sample_ex(hist, rt, MAXEX, out) 38 let ex: i64 = g_abs(out[0] - rt/2); if ex > ex_max { ex_max = ex } 39 ip_sample(hist, rt, out) // NET-R1 (holds last = freeze) 40 let hd: i64 = g_abs(out[0] - rt/2); if hd > hold_max { hold_max = hd } 41 rt = rt + 50 42 } 43 g_puts(" [measure] loss burst rt=600..800: extrap_max_err=" as *u8); g_pn(ex_max) 44 g_puts(" hold(freeze)_max_err=" as *u8); g_pn(hold_max); g_puts("\n" as *u8) 45 pass = pass + g_check("extrapolation tracks truth during loss burst (err ~0)" as *u8, ex_max <= 2); total=total+1 46 pass = pass + g_check("extrap_max_err < hold/freeze_max_err (no freeze)" as *u8, ex_max < hold_max); total=total+1 47 48 // 3) horizon cap (neg): far beyond newest -> HOLD bounded (status 3), not a runaway extrapolation 49 let st_far: i64 = ip_sample_ex(hist, 500 + MAXEX + 300, MAXEX, out) 50 var r3: i64 = 1 51 if st_far != 3 { r3 = 0 } // held, not extrapolated 52 if out[0] != 250 { r3 = 0 } // == last sample value (bounded), not 250+big 53 g_puts(" [measure] beyond horizon (dt=700>cap400): status=" as *u8); g_pn(st_far); g_puts(" held x=" as *u8); g_pn(out[0]); g_puts("\n" as *u8) 54 pass = pass + g_check("horizon cap: long loss HOLDS bounded (no runaway)" as *u8, r3); total=total+1 55 56 // 4) interior unchanged (regression): ex delegates to interp for in-bracket rt 57 let stex: i64 = ip_sample_ex(hist, 250, MAXEX, out) 58 let ix: i64 = out[0] 59 let sti: i64 = ip_sample(hist, 250, out) 60 var r4: i64 = 1 61 if stex != 1 { r4 = 0 } 62 if sti != 1 { r4 = 0 } 63 if ix != out[0] { r4 = 0 } // same value as plain interp 64 pass = pass + g_check("interior rt unchanged (delegates to interp)" as *u8, r4); total=total+1 65 66 // 5) no-data neg 67 let he: *i64 = sys_mmap((1 + 4*IP_STRIDE) * 8) as *i64 68 ip_init(he) 69 pass = pass + g_check("empty history -> 0 (no fabrication)" as *u8, ip_sample_ex(he, 999, MAXEX, out) == 0); total=total+1 70 71 g_puts("---- interp_ex gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8) 72 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 73 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 74 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 75 let ctr__dry: *i64 = gv_ctr() 76 ctr__dry[0] = pass 77 ctr__dry[1] = total 78 let rc__dry: i64 = gv_verdict("INTERP-EX-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 79 sys_exit(rc__dry) 80 return rc__dry 81}