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" 13 14func g_abs(v: i64) -> i64 { if v < 0 { return 0 - v } return v } 15func mkf(f: *i64, x: i64) -> i64 { var i: i64=0; while i<10 { f[i]=0; i=i+1 } f[0]=x; return 0 } 16 17func main() -> i64 { 18 g_puts("nx_interp_ex gate (sovereign dead-reckoning: keep moving during loss, no freeze, bounded)\n" as *u8) 19 var pass: i64 = 0; var total: i64 = 0 20 21 let K: i64 = 16 22 let hist: *i64 = sys_mmap((1 + K*IP_STRIDE) * 8) as *i64 23 ip_init(hist) 24 let f: *i64 = sys_mmap(10*8) as *i64 25 let out: *i64 = sys_mmap(10*8) as *i64 26 27 // steady motion val(t)=t/2, samples 0..500 received; then 600/700/800 LOST (newest = 500) 28 var t: i64 = 0 29 while t <= 500 { mkf(f, t/2); ip_push(hist, K, t, f); t = t + 100 } 30 let MAXEX: i64 = 400 31 32 // 1)+2) during the loss burst rt=600..800: extrapolate vs hold 33 var ex_max: i64 = 0; var hold_max: i64 = 0 34 var rt: i64 = 600 35 while rt <= 800 { 36 ip_sample_ex(hist, rt, MAXEX, out) 37 let ex: i64 = g_abs(out[0] - rt/2); if ex > ex_max { ex_max = ex } 38 ip_sample(hist, rt, out) // NET-R1 (holds last = freeze) 39 let hd: i64 = g_abs(out[0] - rt/2); if hd > hold_max { hold_max = hd } 40 rt = rt + 50 41 } 42 g_puts(" [measure] loss burst rt=600..800: extrap_max_err=" as *u8); g_pn(ex_max) 43 g_puts(" hold(freeze)_max_err=" as *u8); g_pn(hold_max); g_puts("\n" as *u8) 44 pass = pass + g_check("extrapolation tracks truth during loss burst (err ~0)" as *u8, ex_max <= 2); total=total+1 45 pass = pass + g_check("extrap_max_err < hold/freeze_max_err (no freeze)" as *u8, ex_max < hold_max); total=total+1 46 47 // 3) horizon cap (neg): far beyond newest -> HOLD bounded (status 3), not a runaway extrapolation 48 let st_far: i64 = ip_sample_ex(hist, 500 + MAXEX + 300, MAXEX, out) 49 var r3: i64 = 1 50 if st_far != 3 { r3 = 0 } // held, not extrapolated 51 if out[0] != 250 { r3 = 0 } // == last sample value (bounded), not 250+big 52 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) 53 pass = pass + g_check("horizon cap: long loss HOLDS bounded (no runaway)" as *u8, r3); total=total+1 54 55 // 4) interior unchanged (regression): ex delegates to interp for in-bracket rt 56 let stex: i64 = ip_sample_ex(hist, 250, MAXEX, out) 57 let ix: i64 = out[0] 58 let sti: i64 = ip_sample(hist, 250, out) 59 var r4: i64 = 1 60 if stex != 1 { r4 = 0 } 61 if sti != 1 { r4 = 0 } 62 if ix != out[0] { r4 = 0 } // same value as plain interp 63 pass = pass + g_check("interior rt unchanged (delegates to interp)" as *u8, r4); total=total+1 64 65 // 5) no-data neg 66 let he: *i64 = sys_mmap((1 + 4*IP_STRIDE) * 8) as *i64 67 ip_init(he) 68 pass = pass + g_check("empty history -> 0 (no fabrication)" as *u8, ip_sample_ex(he, 999, MAXEX, out) == 0); total=total+1 69 70 g_puts("---- interp_ex gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8) 71 if pass == total { g_puts("verdict=GREEN\n" as *u8); sys_exit(0); return 0 } 72 g_puts("verdict=RED\n" as *u8); sys_exit(1); return 1 73}