code wiki / (root) / nx_emu_probe_gate.nx

nx_emu_probe_gate.nx source

↩ module page · 63 lines · 2747 B

1// nx_emu_probe_gate.nx -- NATIVE correctness KAT for nx_emu_probe (R0.0). 2// Proves the emulator-shaped kernel computes correctly when run on a real mmap'd base, with every 3// assertion cross-checked against an independent native recomputation (no hand-typed magic numbers). 4// The SAME kernel then compiles to wasm; native PASS + clean wasm compile = the foundation rung. 5import "nx_syscalls.nx" 6import "nx_emu_probe.nx" 7 8func g_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 9func g_putn(v: i64) -> i64 { 10 var n: i64 = v 11 if n < 0 { sys_write(1, "-" as *u8, 1); n = 0 - n } 12 let tmp: *u8 = sys_mmap(32) 13 var k: i64 = 0 14 if n == 0 { tmp[0] = 48 as u8; k = 1 } 15 while n > 0 { tmp[k] = (48 + (n % 10)) as u8; n = n / 10; k = k + 1 } 16 let out: *u8 = sys_mmap(32) 17 var j: i64 = 0 18 while k > 0 { out[j] = tmp[k - 1]; j = j + 1; k = k - 1 } 19 sys_write(1, out, j) 20 return 0 21} 22 23func main() -> i64 { 24 let base: i64 = sys_mmap(65536) as i64 25 var fails: i64 = 0 26 27 // 1) seed + spot check: mem[10] = (10*7+3)&0xff = 73 28 p_seed(base, 256) 29 if p_memget_byte(base, 10) != 73 { g_puts("FAIL seed mem[10]\n" as *u8); fails = fails + 1 } 30 else { g_puts("ok seed: mem[10]=73 (store8/load8 + gep)\n" as *u8) } 31 32 // 2) sum cross-checked against an INDEPENDENT native loop (proves p_sum's gep/load reduction) 33 var ref: i64 = 0 34 var i: i64 = 0 35 while i < 256 { ref = ref + ((i * 7 + 3) & 0xff); i = i + 1 } 36 let s: i64 = p_sum(base, 256) 37 if s != ref { g_puts("FAIL sum mismatch\n" as *u8); fails = fails + 1 } 38 else { g_puts("ok sum=" as *u8); g_putn(s); g_puts(" matches independent loop\n" as *u8) } 39 40 // 3) fetch-decode-execute: program 6105 7103 -> V1 = 8 41 p_memset_byte(base, 0, 0x61) 42 p_memset_byte(base, 1, 0x05) 43 p_memset_byte(base, 2, 0x71) 44 p_memset_byte(base, 3, 0x03) 45 var pc: i64 = 0 46 pc = p_step(base, pc) 47 pc = p_step(base, pc) 48 if p_reg_get(base, 1) != 8 { g_puts("FAIL V1 != 8\n" as *u8); fails = fails + 1 } 49 else { g_puts("ok fetch-decode-execute: V1=8 after 6105;7103\n" as *u8) } 50 51 // 4) framebuffer i64 round-trip on a computed address 52 p_fb_set(base, 7, 0xdeadbeef) 53 if p_fb_get(base, 7) != 0xdeadbeef { g_puts("FAIL fb roundtrip\n" as *u8); fails = fails + 1 } 54 else { g_puts("ok framebuffer: fb[7]=0xdeadbeef (i64.store/load)\n" as *u8) } 55 56 // 5) p_probe composite (the single entry the wasm/VM side calls) 57 let pr: i64 = p_probe(base) 58 g_puts("p_probe(base)=" as *u8); g_putn(pr); g_puts("\n" as *u8) 59 60 if fails == 0 { g_puts("EMU_PROBE_NATIVE_PASS\n" as *u8); sys_exit(0) } 61 g_puts("EMU_PROBE_NATIVE_FAIL\n" as *u8); sys_exit(1) 62 return 0 63}