code wiki / _hdl_build / nx_syscalls_gate.nx
nx_syscalls_gate.nx source
↩ module page · 205 lines · 9032 B
1// nx_syscalls_gate.nx -- THE BASE CONTRACT GATE (arch-board w22 queue row #1: nx_syscalls = 13,307
2// importers, ZERO direct gate until now; also the mom-3 "never break userspace" hard version). Every
3// sworn wrapper is proven with a REAL KERNEL ROUND-TRIP -- not presence, BEHAVIOR: bytes written are
4// bytes read, forked children are reaped with their exact code, shared pages cross fork, dirents list
5// planted files, negatives FAIL (a gate that cannot fail is not a gate). Composes (fork+exec, fail-
6// closed) nx_syscall_sanity_kat.elf -- the syscall-NUMBER translation KAT from the RV64/x86 collision
7// fix -- so number-mistranslation and behavior regressions are both caught here. Any edit to
8// nx_syscalls.nx must leave this GREEN; the arch board counts it as the base's paired validator.
9// nx_syscalls_gate -- run the battery; exit 0 GREEN / 1 RED
10// license_tier: ORIGINAL module: nishi-core.examiner.syscalls_gate No hw writes (rule 26).
11import "nx_syscalls.nx"
12
13func sg_p(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
14func sg_pn(v: i64) -> i64 {
15 var m: i64 = v; if m < 0 { sg_p("-" as *u8); m = 0 - m }
16 let t: *u8 = sys_mmap(24); var k: i64 = 0; if m == 0 { t[0] = 48 as u8; k = 1 }
17 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
18 let o: *u8 = sys_mmap(24); var i: i64 = 0; while i < k { o[i] = t[k-1-i]; i = i + 1 } sys_write(1, o, k)
19 sys_munmap(t, 24); sys_munmap(o, 24); return 0
20}
21func sg_row(name: *u8, ok: i64, fails: *i64) -> i64 {
22 if ok == 1 { sg_p(" [PASS] " as *u8) } else { sg_p(" [FAIL] " as *u8); fails[0] = fails[0] + 1 }
23 sg_p(name); sg_p("\n" as *u8)
24 return 0
25}
26
27func main(argc: i64, argv: *i64) -> i64 {
28 sg_p("=== nx_syscalls GATE -- the base contract (behavioral round-trips; sworn interface) ===\n" as *u8)
29 let fails: *i64 = sys_mmap(16) as *i64
30 fails[0] = 0
31
32 // K1 mmap/munmap: write pattern at both ends of an 8KB map, read back, unmap cleanly
33 let m1: *u8 = sys_mmap(8192)
34 var ok: i64 = 0
35 if (m1 as i64) != 0 {
36 m1[0] = 171 as u8
37 m1[8191] = 205 as u8
38 if m1[0] == (171 as u8) { if m1[8191] == (205 as u8) { if sys_munmap(m1, 8192) == 0 { ok = 1 } } }
39 }
40 sg_row("K1 mmap/munmap 8KB pattern round-trip" as *u8, ok, fails)
41
42 // K2 openat_wr -> write -> close -> openat_rd -> read: bytes equal
43 let path_a: *u8 = "/tmp/nxsg_a" as *u8
44 let fd1: i64 = sys_openat_wr(path_a, 420)
45 ok = 0
46 if fd1 >= 0 {
47 sys_write(fd1, "NXSG-CONTRACT" as *u8, 13)
48 sys_close(fd1)
49 let fd2: i64 = sys_openat_rd(path_a)
50 if fd2 >= 0 {
51 let rb: *u8 = sys_mmap(64)
52 let rn: i64 = sys_read(fd2, rb, 63)
53 sys_close(fd2)
54 if rn == 13 {
55 var eq: i64 = 1
56 let want: *u8 = "NXSG-CONTRACT" as *u8
57 var i: i64 = 0
58 while i < 13 { if rb[i] != want[i] { eq = 0 } i = i + 1 }
59 if eq == 1 { ok = 1 }
60 }
61 }
62 }
63 sg_row("K2 file write->read byte-exact round-trip" as *u8, ok, fails)
64
65 // K3 NEGATIVE: opening a path that cannot exist must fail (<0) -- the gate can fail
66 ok = 0
67 if sys_openat_rd("/tmp/nxsg_definitely_absent_9714" as *u8) < 0 { ok = 1 }
68 sg_row("K3 negative-control: open(absent) < 0" as *u8, ok, fails)
69
70 // K4 lseek: seek to offset 5 of the 13-byte file, read from there ("ONTRACT" tail starts 'C' at 5? NXSG-CONTRACT: idx5='C')
71 ok = 0
72 let fd3: i64 = sys_openat_rd(path_a)
73 if fd3 >= 0 {
74 if sys_lseek(fd3, 5, 0) == 5 {
75 let rb2: *u8 = sys_mmap(16)
76 if sys_read(fd3, rb2, 1) == 1 { if rb2[0] == (67 as u8) { ok = 1 } }
77 }
78 sys_close(fd3)
79 }
80 sg_row("K4 lseek(5,SET) reads the exact byte" as *u8, ok, fails)
81
82 // K5 renameat: A->B atomically; A gone, B has the bytes
83 ok = 0
84 let path_b: *u8 = "/tmp/nxsg_b" as *u8
85 if sys_renameat(path_a, path_b) == 0 {
86 if sys_openat_rd(path_a) < 0 {
87 let fd4: i64 = sys_openat_rd(path_b)
88 if fd4 >= 0 { ok = 1; sys_close(fd4) }
89 }
90 }
91 sg_row("K5 renameat: old gone, new readable" as *u8, ok, fails)
92
93 // K6 getdents64: /tmp listing must contain our planted nxsg_b
94 ok = 0
95 let dfd: i64 = sys_openat_rd("/tmp" as *u8)
96 if dfd >= 0 {
97 let db: *u8 = sys_mmap(65536)
98 var found: i64 = 0
99 var nr: i64 = 1
100 while nr > 0 {
101 nr = sys_getdents64(dfd, db, 65536)
102 if nr > 0 {
103 var o: i64 = 0
104 while o < nr {
105 let rl: i64 = (db[o+16] as i64) + ((db[o+17] as i64) * 256)
106 if rl <= 0 { o = nr } else {
107 // name at o+19: compare to "nxsg_b"
108 let want2: *u8 = "nxsg_b" as *u8
109 var eq2: i64 = 1
110 var j: i64 = 0
111 while j < 6 { if db[o+19+j] != want2[j] { eq2 = 0; j = 6 } else { j = j + 1 } }
112 if eq2 == 1 { if db[o+25] == (0 as u8) { found = 1 } }
113 o = o + rl
114 }
115 }
116 }
117 }
118 sys_close(dfd)
119 if found == 1 { ok = 1 }
120 }
121 sg_row("K6 getdents64 lists the planted file" as *u8, ok, fails)
122
123 // K7 fork + wait4: child exits 42, parent captures exactly 42
124 ok = 0
125 let pid: i64 = sys_fork()
126 if pid == 0 { sys_exit(42) }
127 if pid > 0 {
128 let st: *i64 = sys_mmap(16) as *i64
129 if sys_wait4(pid, st, 0) == pid { if ((st[0] / 256) & 255) == 42 { ok = 1 } }
130 }
131 sg_row("K7 fork/wait4 child exit code 42 captured" as *u8, ok, fails)
132
133 // K8 pipe2: bytes written to the write end arrive on the read end. ⚠THE PACKED-INT32 LAW: the kernel
134 // writes TWO int32 fds into ONE i64 slot -- read fd = fds[0] low half, write fd = fds[0] HIGH half.
135 // (fds[1] is never written; the old sanity-KAT read it and false-passed on garbage -- fixed there too.)
136 // HANG-PROOF: never read the pipe unless the 3-byte write actually succeeded.
137 ok = 0
138 let fds: *i64 = sys_mmap(16) as *i64
139 fds[0] = 0 - 1; fds[1] = 0 - 1
140 if sys_pipe2(fds, 0) == 0 {
141 let rfd: i64 = fds[0] & 4294967295
142 let wfd: i64 = (fds[0] / 4294967296) & 4294967295
143 if rfd >= 0 { if wfd >= 0 {
144 if sys_write(wfd, "xyz" as *u8, 3) == 3 {
145 let pb: *u8 = sys_mmap(16)
146 if sys_read(rfd, pb, 3) == 3 { if pb[0] == (120 as u8) { if pb[2] == (122 as u8) { ok = 1 } } }
147 }
148 sys_close(rfd); sys_close(wfd)
149 } }
150 }
151 sg_row("K8 pipe2 write-end -> read-end byte flow (packed-int32 fds)" as *u8, ok, fails)
152
153 // K9 readlinkat /proc/self/exe: non-empty absolute path
154 ok = 0
155 let lb: *u8 = sys_mmap(512)
156 let ll: i64 = sys_readlinkat("/proc/self/exe" as *u8, lb, 511)
157 if ll > 0 { if lb[0] == (47 as u8) { ok = 1 } }
158 sg_row("K9 readlinkat(/proc/self/exe) absolute path" as *u8, ok, fails)
159
160 // K10 mmap_shared crosses fork: child writes 123, parent reads 123 (the /status seqlock substrate)
161 ok = 0
162 let sh: *u8 = sys_mmap_shared(4096)
163 if (sh as i64) != 0 {
164 sh[100] = 0 as u8
165 let pid2: i64 = sys_fork()
166 if pid2 == 0 { sh[100] = 123 as u8; sys_exit(0) }
167 if pid2 > 0 {
168 let st2: *i64 = sys_mmap(16) as *i64
169 sys_wait4(pid2, st2, 0)
170 if sh[100] == (123 as u8) { ok = 1 }
171 }
172 }
173 sg_row("K10 mmap_shared page crosses fork (child write seen by parent)" as *u8, ok, fails)
174
175 // K11 chdir: relative open resolves in the new cwd
176 ok = 0
177 if sys_chdir("/tmp" as *u8) == 0 {
178 let fd5: i64 = sys_openat_rd("nxsg_b" as *u8)
179 if fd5 >= 0 { ok = 1; sys_close(fd5) }
180 }
181 sg_row("K11 chdir + relative open resolves" as *u8, ok, fails)
182
183 // K12 COMPOSED: the syscall-NUMBER translation KAT (RV64/x86 collision class) must be GREEN.
184 // fail-closed: missing ELF or nonzero exit = FAIL (the number-KAT is part of the sworn contract).
185 ok = 0
186 let pid3: i64 = sys_fork()
187 if pid3 == 0 {
188 let av: *i64 = sys_mmap(24) as *i64
189 av[0] = "/volume1/homes/elderwesto/nishihost/nx_syscall_sanity_kat.elf" as *u8 as i64
190 av[1] = 0
191 let ev: *i64 = sys_mmap(16) as *i64
192 ev[0] = 0
193 sys_execve(av[0] as *u8, av, ev)
194 sys_exit(127)
195 }
196 if pid3 > 0 {
197 let st3: *i64 = sys_mmap(16) as *i64
198 if sys_wait4(pid3, st3, 0) == pid3 { if ((st3[0] / 256) & 255) == 0 { ok = 1 } }
199 }
200 sg_row("K12 composed nx_syscall_sanity_kat (number-translation) GREEN" as *u8, ok, fails)
201
202 if fails[0] == 0 { sg_p("=== GATE verdict=GREEN: the base contract holds -- 12/12 behavioral KATs (never break userspace) ===\n" as *u8); return 0 }
203 sg_p("=== GATE RED: " as *u8); sg_pn(fails[0]); sg_p(" contract KAT(s) FAILED -- nx_syscalls may not ship ===\n" as *u8)
204 return 1
205}