nx_x86_gate.nx source
↩ module page · 88 lines · 4858 B
1// nx_x86_gate.nx -- NATIVE correctness gate for nx_x86 (R1.0a). Three hand-assembled 16-bit programs:
2// A: MOV/ADD/INC then CMP AX,8 ; JZ taken -> AX stays 8 (proves the equal/taken branch + flags)
3// B: same but CMP AX,7 ; JZ NOT taken -> MOV AX,0xFFFF runs (proves the not-equal/not-taken branch)
4// C: DEC CX / JNZ countdown loop summing AX -> AX=6, CX=0 (proves the loop + DEC flags)
5import "nx_syscalls.nx"
6import "nx_x86.nx"
7import "nx_gate_verdict.nx"
8
9func 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 }
10func g_pn(v: i64) -> i64 {
11 let b: *u8 = sys_mmap(28)
12 var x: i64 = v
13 if x < 0 { b[0] = 45 as u8; sys_write(1, b, 1); x = 0 - x }
14 if x == 0 { b[0] = 48 as u8; sys_write(1, b, 1); return 0 }
15 var d: i64 = 0
16 var y: i64 = x
17 while y > 0 { d = d + 1; y = y / 10 }
18 var i: i64 = d - 1
19 y = x
20 while i >= 0 { b[i] = (48 + (y % 10)) as u8; y = y / 10; i = i - 1 }
21 sys_write(1, b, d)
22 return 0
23}
24func g_check(name: *u8, cond: i64) -> i64 {
25 if cond == 1 { g_puts(" PASS " as *u8) } else { g_puts(" FAIL " as *u8) }
26 g_puts(name); g_puts("\n" as *u8)
27 return cond
28}
29
30// load the shared A/B prologue (MOV AX,0; ADD AX,3; ADD AX,3; INC AX; INC AX) + the CMP/JZ/MOV/HLT tail.
31// cmpval = the immediate compared against AX (8 -> equal/taken ; 7 -> not-equal/not-taken).
32func load_ab(base: i64, cmpval: i64) -> i64 {
33 x86_load(base, 256, 184); x86_load(base, 257, 0); x86_load(base, 258, 0) // MOV AX,0
34 x86_load(base, 259, 5); x86_load(base, 260, 3); x86_load(base, 261, 0) // ADD AX,3
35 x86_load(base, 262, 5); x86_load(base, 263, 3); x86_load(base, 264, 0) // ADD AX,3
36 x86_load(base, 265, 64) // INC AX
37 x86_load(base, 266, 64) // INC AX
38 x86_load(base, 267, 61); x86_load(base, 268, cmpval); x86_load(base, 269, 0) // CMP AX,cmpval
39 x86_load(base, 270, 116); x86_load(base, 271, 3) // JZ +3
40 x86_load(base, 272, 184); x86_load(base, 273, 255); x86_load(base, 274, 255) // MOV AX,0xFFFF
41 x86_load(base, 275, 244) // HLT
42 return 0
43}
44
45func main() -> i64 {
46 g_puts("nx_x86 native gate (16-bit real-mode skeleton: MOV/ADD/INC/DEC/CMP/JZ/JNZ/HLT)\n" as *u8)
47 var pass: i64 = 0
48 var total: i64 = 0
49
50 let base: i64 = sys_mmap(131072) as i64
51
52 // ---- Program A: CMP AX,8 -> ZF=1 -> JZ taken -> AX stays 8 ----
53 x86_reset(base)
54 load_ab(base, 8)
55 x86_run(base, 100)
56 pass = pass + g_check("A: AX == 8 (JZ taken skipped MOV AX,FFFF)" as *u8, x86_reg(base, 0) == 8); total = total + 1
57 pass = pass + g_check("A: ZF == 1 (CMP AX,8 equal)" as *u8, x86_zf(base) == 1); total = total + 1
58
59 // ---- Program B: CMP AX,7 -> ZF=0 -> JZ not taken -> MOV AX,0xFFFF runs ----
60 x86_reset(base)
61 load_ab(base, 7)
62 x86_run(base, 100)
63 pass = pass + g_check("B: AX == 0xFFFF (JZ not taken, MOV ran)" as *u8, x86_reg(base, 0) == 65535); total = total + 1
64 pass = pass + g_check("B: ZF == 0 (CMP AX,7 not equal)" as *u8, x86_zf(base) == 0); total = total + 1
65
66 // ---- Program C: countdown loop (MOV CX,3; MOV AX,0; loop: ADD AX,2; DEC CX; JNZ loop; HLT) ----
67 x86_reset(base)
68 x86_load(base, 256, 185); x86_load(base, 257, 3); x86_load(base, 258, 0) // MOV CX,3
69 x86_load(base, 259, 184); x86_load(base, 260, 0); x86_load(base, 261, 0) // MOV AX,0
70 x86_load(base, 262, 5); x86_load(base, 263, 2); x86_load(base, 264, 0) // ADD AX,2
71 x86_load(base, 265, 73) // DEC CX
72 x86_load(base, 266, 117); x86_load(base, 267, 250) // JNZ -6
73 x86_load(base, 268, 244) // HLT
74 x86_run(base, 100)
75 pass = pass + g_check("C: AX == 6 (loop summed 2 three times)" as *u8, x86_reg(base, 0) == 6); total = total + 1
76 pass = pass + g_check("C: CX == 0 (loop counter drained)" as *u8, x86_reg(base, 1) == 0); total = total + 1
77
78 g_puts("---- x86 native gate: passed " as *u8); g_pn(pass); g_puts(" / " as *u8); g_pn(total); g_puts(" ----\n" as *u8)
79 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
80 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
81 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
82 let ctr__dry: *i64 = gv_ctr()
83 ctr__dry[0] = pass
84 ctr__dry[1] = total
85 let rc__dry: i64 = gv_verdict("X86-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
86 sys_exit(rc__dry)
87 return rc__dry
88}