code wiki / _hdl_build / nx_simd_avx2_kat_gate.nx
nx_simd_avx2_kat_gate.nx source
↩ module page · 113 lines · 4592 B
1// nx_simd_avx2_kat_gate.nx -- SOVEREIGN 256-bit AVX2 vector run-KAT (the VEX rung): proves the
2// sovereign encoder/assembler emit working VEX-encoded ymm load/compute/store on REAL x86 silicon
3// (host has avx2), NO gcc/qemu/binutils. AUTHOR=ORGAN, no-false-green.
4//
5// 8x u32 lanes: vecA lane0=10, vecB lane0=32.
6// POS: vmovdqu ymm load x2; vpaddd ymm -> lane0=42; vmovdqu ymm store; reload -> exit(42).
7// NEG: + vpxor %ymm0,%ymm0,%ymm0 (self-xor zero) -> exit(0).
8// GREEN iff pos==42 AND neg==0 AND pos!=neg. Run-proves the 3-byte VEX encoder (x86_vex_rrr /
9// x86_vex_rm), ymm register parsing, and the 3-operand AT&T form -- the foundation every AVX2
10// capability (and, with EVEX, AVX-512) reuses. Appends knowledge/status/simd_vec_kat.log.
11// license_tier: ORIGINAL
12import "nx_syscalls.nx"
13
14const ASM_TOOL: *u8 = "_offc/nxasm_x86_main.elf"
15const SV_LOG: *u8 = "knowledge/status/simd_vec_kat.log"
16
17func gw(fd: i64, s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(fd, s, n); return 0 }
18func gwn(fd: i64, v: i64) -> i64 {
19 let bb: *u8 = sys_mmap(28); var m: i64 = v
20 if m < 0 { m = 0 - m; sys_write(fd, "-" as *u8, 1) }
21 let t: *u8 = sys_mmap(28); var k: i64 = 0
22 if m == 0 { t[0] = 48; k = 1 }
23 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
24 var i: i64 = 0
25 while i < k { bb[i] = t[k - 1 - i]; i = i + 1 }
26 sys_write(fd, bb, k); return 0
27}
28
29func g_run(path: *u8, argv: *i64) -> i64 {
30 let envp: *i64 = sys_mmap(8 * 4) as *i64
31 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64
32 envp[1] = 0
33 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4)
34 let pid: i64 = sys_fork()
35 if pid == 0 {
36 if dn >= 0 { sys_dup3(dn, 1, 0) }
37 if dn >= 0 { sys_dup3(dn, 2, 0) }
38 sys_execve(path, argv, envp)
39 sys_exit(127)
40 }
41 let st: *i64 = sys_mmap(16) as *i64
42 sys_wait4(pid, st, 0)
43 if dn >= 0 { sys_close(dn) }
44 let sig: i64 = st[0] & 0x7f
45 if sig != 0 { return 128 + sig }
46 return (st[0] >> 8) & 0xff
47}
48
49func asm_and_run(spath: *u8, elfpath: *u8) -> i64 {
50 let aa: *i64 = sys_mmap(8 * 4) as *i64
51 aa[0] = ASM_TOOL as i64
52 aa[1] = spath as i64
53 aa[2] = elfpath as i64
54 aa[3] = 0
55 let rc_a: i64 = g_run(ASM_TOOL, aa)
56 if rc_a != 0 { return 0 - 200 - rc_a }
57 let rr: *i64 = sys_mmap(8 * 4) as *i64
58 rr[0] = elfpath as i64
59 rr[1] = 0
60 return g_run(elfpath, rr)
61}
62
63func write_avx2_s(path: *u8, zero: i64) -> i64 {
64 let fd: i64 = sys_openat_wr(path, 0x1a4)
65 if fd < 0 { return 0 - 1 }
66 gw(fd, ".text\n" as *u8)
67 gw(fd, "_start:\n" as *u8)
68 gw(fd, "leaq vecA(%rip), %rdi\n" as *u8)
69 gw(fd, "vmovdqu (%rdi), %ymm0\n" as *u8)
70 gw(fd, "leaq vecB(%rip), %rsi\n" as *u8)
71 gw(fd, "vmovdqu (%rsi), %ymm1\n" as *u8)
72 gw(fd, "vpaddd %ymm1, %ymm0, %ymm0\n" as *u8)
73 if zero == 1 { gw(fd, "vpxor %ymm0, %ymm0, %ymm0\n" as *u8) }
74 gw(fd, "leaq outbuf(%rip), %rdx\n" as *u8)
75 gw(fd, "vmovdqu %ymm0, (%rdx)\n" as *u8)
76 gw(fd, "movl (%rdx), %edi\n" as *u8)
77 gw(fd, "movabsq $60, %rax\n" as *u8)
78 gw(fd, "syscall\n" as *u8)
79 gw(fd, ".section .rodata\n" as *u8)
80 gw(fd, "vecA:\n" as *u8)
81 gw(fd, ".byte 10,0,0,0,1,0,0,0,2,0,0,0,3,0,0,0,4,0,0,0,5,0,0,0,6,0,0,0,7,0,0,0\n" as *u8)
82 gw(fd, "vecB:\n" as *u8)
83 gw(fd, ".byte 32,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0\n" as *u8)
84 gw(fd, ".lcomm outbuf, 32\n" as *u8)
85 sys_close(fd)
86 return 0
87}
88
89func g_emit(fd: i64, pos: i64, neg: i64, ok: i64) -> i64 {
90 gw(fd, "SIMD_VEC_KAT rung=R4-avx2-256 authored=organ width=256 reg=ymm forms=vmovdqu+vpaddd+vpxor(VEX-3byte) sovereign(nx_cc->nxasm_x86,no-gcc/qemu/binutils) silicon=real-avx2 pos42=" as *u8); gwn(fd, pos)
91 gw(fd, " neg0=" as *u8); gwn(fd, neg)
92 gw(fd, " distinct=" as *u8); if pos != neg { gwn(fd, 1) } else { gwn(fd, 0) }
93 if ok == 1 { gw(fd, " verdict=GREEN\n" as *u8) } else { gw(fd, " verdict=RED reason=exit-mismatch-or-vex-gap\n" as *u8) }
94 return 0
95}
96
97func main() -> i64 {
98 write_avx2_s("/tmp/_avx2_pos.s" as *u8, 0)
99 let pos: i64 = asm_and_run("/tmp/_avx2_pos.s" as *u8, "/tmp/_avx2_pos.elf" as *u8)
100 write_avx2_s("/tmp/_avx2_neg.s" as *u8, 1)
101 let neg: i64 = asm_and_run("/tmp/_avx2_neg.s" as *u8, "/tmp/_avx2_neg.elf" as *u8)
102
103 var ok: i64 = 1
104 if pos != 42 { ok = 0 }
105 if neg != 0 { ok = 0 }
106 if pos == neg { ok = 0 }
107
108 g_emit(1, pos, neg, ok)
109 let lf: i64 = sys_openat_append(SV_LOG, 420)
110 if lf >= 0 { g_emit(lf, pos, neg, ok); sys_close(lf) }
111 if ok == 1 { return 0 }
112 return 1
113}