nx_linux_guest_gate.nx source
↩ module page · 248 lines · 10144 B
1// nx_linux_guest_gate.nx -- F103c "Linux guest lane" (os lane, critical path; deps F103a=D F103b=D 2026-07-21).
2// THE CLAIM: the Linux ABI exists in NishiOS ONLY as a LABELED interop GUEST LANE (contract C09,
3// backend linux-host-syscalls) and that lane WORKS end-to-end as a real process substrate: guest
4// spawn (fork+dup3+execve+wait4) with exit-code propagation, byte-exact stdout capture, stderr on
5// the same capture, envp delivery, determinism -- while the NATIVE lane REFUSES Linux guests BY
6// CONSTRUCTION (host paths unresolvable in the block-VFS; planted ELF bytes rejected by
7// verify-before-execute with NO output fabricated). D001: emits the nx_gate_verdict contract.
8// REFUTATION: argv[1]=negctl corrupts ONE byte of the expected stdout capture -> the byte-exact
9// capture tooth (C03) MUST go RED alone; registered sibling nx_linux_guest_negtest pins that arg.
10// license_tier: ORIGINAL expect_exit: 0 No hw writes (Rule 26): guests are user-space children.
11import "nx_pabi.nx"
12import "nx_gate_verdict.nx"
13
14const LG_BUF: i64 = 4096
15const LG_EXECN: i64 = 5
16
17// deterministic exit-code sweep table (incl 200 to prove full 0..255 byte range rides wait4)
18func lg_code(i: i64) -> i64 {
19 if i == 0 { return 0 }
20 if i == 1 { return 1 }
21 if i == 2 { return 7 }
22 if i == 3 { return 42 }
23 return 200
24}
25
26func lg_script(i: i64) -> *u8 {
27 if i == 0 { return "exit 0" as *u8 }
28 if i == 1 { return "exit 1" as *u8 }
29 if i == 2 { return "exit 7" as *u8 }
30 if i == 3 { return "exit 42" as *u8 }
31 return "exit 200" as *u8
32}
33
34// spawn ONE guest: /bin/sh -c <script> through the labeled guest lane, stdout+stderr -> outpath.
35// envp is EXPLICIT (only F103C_GUEST) so the env tooth proves delivery, not host leakage.
36func lg_run(script: *u8, outpath: *u8) -> i64 {
37 let av: *i64 = sys_mmap(64) as *i64
38 let s0: *u8 = "/bin/sh" as *u8
39 let s1: *u8 = "-c" as *u8
40 av[0] = s0 as i64
41 av[1] = s1 as i64
42 av[2] = script as i64
43 av[3] = 0
44 let ev: *i64 = sys_mmap(32) as *i64
45 let e0: *u8 = "F103C_GUEST=sovereign" as *u8
46 ev[0] = e0 as i64
47 ev[1] = 0
48 return pabi_spawn(PABI_LINUX, 0 as *u8, av, ev, outpath)
49}
50
51// spawn a bare program path (no shell) -- the absent-binary labeled-failure tooth.
52func lg_runx(prog: *u8, outpath: *u8) -> i64 {
53 let av: *i64 = sys_mmap(32) as *i64
54 av[0] = prog as i64
55 av[1] = 0
56 let ev: *i64 = sys_mmap(16) as *i64
57 ev[0] = 0
58 return pabi_spawn(PABI_LINUX, 0 as *u8, av, ev, outpath)
59}
60
61// byte compare with lengths: 1 equal / 0 mismatch (negctl proves this comparator non-vacuous)
62func lg_cmp(got: *u8, gn: i64, want: *u8, wn: i64) -> i64 {
63 if gn != wn { return 0 }
64 var i: i64 = 0
65 while i < gn {
66 if got[i] != want[i] { return 0 }
67 i = i + 1
68 }
69 return 1
70}
71
72func lg_slen(s: *u8) -> i64 {
73 var n: i64 = 0
74 while s[n] != (0 as u8) { n = n + 1 }
75 return n
76}
77
78// order-sensitive rolling fold (vb_sum family): a swapped pair changes it; length folded too
79func lg_fold(ck: i64, buf: *u8, n: i64) -> i64 {
80 var s: i64 = ck
81 var k: i64 = 0
82 while k < n { s = s * 131 + (buf[k] as i64); k = k + 1 }
83 s = s * 1000003 + n
84 return s
85}
86
87func main(argc: i64, argv: *i64) -> i64 {
88 var neg: i64 = 0
89 if argc >= 2 {
90 let a1v: i64 = argv[1]
91 let a1: *u8 = a1v as *u8
92 if a1[0] == (110 as u8) { if a1[1] == (101 as u8) { if a1[2] == (103 as u8) { neg = 1 } } }
93 }
94 let ctr: *i64 = gv_ctr()
95 gv_head("LINUX-GUEST-LANE (F103c) -- Linux ABI as the LABELED interop guest lane only: spawn/exit/stdio/env proven end-to-end; the native lane REFUSES Linux guests by construction" as *u8)
96 if neg == 1 { gv_puts(" [negctl] ONE byte of the expected stdout capture corrupted -- the byte-exact capture tooth MUST go RED\n" as *u8) }
97 var errs: i64 = 0
98 var tot: i64 = 0
99 var okx: i64 = 0
100 var a: i64 = 0
101 while a < LG_EXECN {
102 let sc: *u8 = lg_script(a)
103 let want: i64 = lg_code(a)
104 let rc1: i64 = lg_run(sc, "/tmp/f103c_x" as *u8)
105 if rc1 < 0 { errs = errs + 1 }
106 if rc1 == want { okx = okx + 1 }
107 a = a + 1
108 }
109 let re: i64 = lg_run("echo guest lane alive" as *u8, "/tmp/f103c_e" as *u8)
110 if re != 0 { errs = errs + 1 }
111 let eb: *u8 = sys_mmap(LG_BUF) as *u8
112 let en: i64 = pabi_read(PABI_LINUX, 0 as *u8, "/tmp/f103c_e" as *u8, eb, LG_BUF)
113 if en < 0 { errs = errs + 1 }
114 tot = tot + en
115 let xb: *u8 = sys_mmap(64) as *u8
116 let xs: *u8 = "guest lane alive\n" as *u8
117 let xn: i64 = lg_slen(xs)
118 var q: i64 = 0
119 while q < xn { xb[q] = xs[q]; q = q + 1 }
120 if neg == 1 { let ov: i64 = xb[0] as i64; xb[0] = (ov ^ 1) as u8 }
121 let c03: i64 = lg_cmp(eb, en, xb, xn)
122 let rv: i64 = lg_run("echo $F103C_GUEST" as *u8, "/tmp/f103c_v" as *u8)
123 if rv != 0 { errs = errs + 1 }
124 let vb2: *u8 = sys_mmap(LG_BUF) as *u8
125 let vn: i64 = pabi_read(PABI_LINUX, 0 as *u8, "/tmp/f103c_v" as *u8, vb2, LG_BUF)
126 let vs: *u8 = "sovereign\n" as *u8
127 let vsl: i64 = lg_slen(vs)
128 let c04: i64 = lg_cmp(vb2, vn, vs, vsl)
129 tot = tot + vn
130 let rs: i64 = lg_run("echo failbytes 1>&2" as *u8, "/tmp/f103c_s" as *u8)
131 if rs != 0 { errs = errs + 1 }
132 let sb: *u8 = sys_mmap(LG_BUF) as *u8
133 let sn: i64 = pabi_read(PABI_LINUX, 0 as *u8, "/tmp/f103c_s" as *u8, sb, LG_BUF)
134 let ss: *u8 = "failbytes\n" as *u8
135 let ssl: i64 = lg_slen(ss)
136 let c05: i64 = lg_cmp(sb, sn, ss, ssl)
137 tot = tot + sn
138 let rda: i64 = lg_run("echo guest lane alive" as *u8, "/tmp/f103c_da" as *u8)
139 let rdb: i64 = lg_run("echo guest lane alive" as *u8, "/tmp/f103c_db" as *u8)
140 if rda != 0 { errs = errs + 1 }
141 if rdb != 0 { errs = errs + 1 }
142 let da: *u8 = sys_mmap(LG_BUF) as *u8
143 let db2: *u8 = sys_mmap(LG_BUF) as *u8
144 let dan: i64 = pabi_read(PABI_LINUX, 0 as *u8, "/tmp/f103c_da" as *u8, da, LG_BUF)
145 let dbn: i64 = pabi_read(PABI_LINUX, 0 as *u8, "/tmp/f103c_db" as *u8, db2, LG_BUF)
146 var cka: i64 = 7
147 var ckb: i64 = 7
148 cka = lg_fold(cka, da, dan)
149 ckb = lg_fold(ckb, db2, dbn)
150 tot = tot + dan
151 tot = tot + dbn
152 var c06: i64 = 0
153 if cka == ckb { if dan > 0 { c06 = 1 } }
154 let r7: i64 = lg_runx("/bin/no_such_f103c_guest_zz" as *u8, "/tmp/f103c_a" as *u8)
155 let ln: *u8 = pabi_backend_name(PABI_LINUX)
156 let lnl: i64 = lg_slen(ln)
157 let lw: *u8 = "linux-host-syscalls" as *u8
158 let lwl: i64 = lg_slen(lw)
159 let c08: i64 = lg_cmp(ln, lnl, lw, lwl)
160 let nn: *u8 = pabi_backend_name(PABI_NISHIOS)
161 let nnl: i64 = lg_slen(nn)
162 let nw: *u8 = "nishios-block-vfs" as *u8
163 let nwl: i64 = lg_slen(nw)
164 let c09: i64 = lg_cmp(nn, nnl, nw, nwl)
165 let img9: *u8 = pabi_nishios_new()
166 let av9: *i64 = sys_mmap(32) as *i64
167 let sp9: *u8 = "/bin/sh" as *u8
168 av9[0] = sp9 as i64
169 av9[1] = 0
170 let r9: i64 = pabi_spawn(PABI_NISHIOS, img9, av9, av9, "/gout9" as *u8)
171 let img10: *u8 = pabi_nishios_new()
172 let ebuf: *u8 = sys_mmap(32) as *u8
173 ebuf[0] = 0x7F as u8
174 ebuf[1] = 69 as u8
175 ebuf[2] = 76 as u8
176 ebuf[3] = 70 as u8
177 ebuf[4] = 2 as u8
178 ebuf[5] = 1 as u8
179 ebuf[6] = 1 as u8
180 var z: i64 = 7
181 while z < 16 { ebuf[z] = 0 as u8; z = z + 1 }
182 let we: i64 = pabi_write(PABI_NISHIOS, img10, "/guest_elf" as *u8, ebuf, 16)
183 let av10: *i64 = sys_mmap(32) as *i64
184 let gp: *u8 = "/guest_elf" as *u8
185 av10[0] = gp as i64
186 av10[1] = 0
187 let r10: i64 = pabi_spawn(PABI_NISHIOS, img10, av10, av10, "/gout10" as *u8)
188 let f10: i64 = pabi_exists(PABI_NISHIOS, img10, "/gout10" as *u8)
189 var r9neg: i64 = 0
190 if r9 < 0 { r9neg = 1 }
191 var r10neg: i64 = 0
192 if r10 < 0 { r10neg = 1 }
193 gv_puts(" evidence: okx=" as *u8)
194 gv_num(okx)
195 gv_puts(" en=" as *u8)
196 gv_num(en)
197 gv_puts(" vn=" as *u8)
198 gv_num(vn)
199 gv_puts(" sn=" as *u8)
200 gv_num(sn)
201 gv_puts(" cka=" as *u8)
202 gv_num(cka)
203 gv_puts(" ckb=" as *u8)
204 gv_num(ckb)
205 gv_puts(" r7=" as *u8)
206 gv_num(r7)
207 gv_puts(" r9neg=" as *u8)
208 gv_num(r9neg)
209 gv_puts(" r10neg=" as *u8)
210 gv_num(r10neg)
211 gv_puts(" tot=" as *u8)
212 gv_num(tot)
213 gv_puts(" errs=" as *u8)
214 gv_num(errs)
215 gv_puts("\n" as *u8)
216 var t: i64 = 0
217 if errs == 0 { t = 1 }
218 gv_check("C01 guest workload completed: all spawns+captures errs==0" as *u8, t, ctr)
219 t = 0
220 if okx == LG_EXECN { t = 1 }
221 gv_check("C02 exit-code sweep 5/5: guest rc propagated exactly via wait4 (0 1 7 42 200)" as *u8, t, ctr)
222 gv_check("C03 stdout capture BYTE-EXACT vs expected through the guest lane" as *u8, c03, ctr)
223 gv_check("C04 envp delivered: guest reads F103C_GUEST=sovereign (explicit env, no host leakage)" as *u8, c04, ctr)
224 gv_check("C05 stderr rides the same capture (dup3 fd2 -> outfile)" as *u8, c05, ctr)
225 gv_check("C06 determinism: identical guest run twice -> capture folds EQUAL" as *u8, c06, ctr)
226 t = 0
227 if r7 == 127 { t = 1 }
228 gv_check("C07 absent guest binary -> labeled failure 127 (nothing fabricated)" as *u8, t, ctr)
229 gv_check("C08 guest lane LABELED linux-host-syscalls (contract C09 needle grounded in behavior)" as *u8, c08, ctr)
230 gv_check("C09 native lane labeled nishios-block-vfs -- lanes never conflated" as *u8, c09, ctr)
231 t = 0
232 if r9 < 0 { t = 1 }
233 gv_check("C10 native lane REFUSES a host path (no VFS entry -> no silent fallback to Linux)" as *u8, t, ctr)
234 t = 0
235 if we == 0 { if r10 < 0 { if f10 == 0 { t = 1 } } }
236 gv_check("C11 native lane REFUSES planted ELF bytes: verify-before-execute, no output fabricated" as *u8, t, ctr)
237 t = 0
238 if tot > 30 { if cka != 7 { t = 1 } }
239 gv_check("C12 non-vacuous: captured bytes folded and above floor" as *u8, t, ctr)
240 let ws2: *u8 = "guest-lane-alive\n" as *u8
241 let cw: i64 = lg_cmp(eb, en, ws2, 17)
242 t = 0
243 if cw == 0 { t = 1 }
244 gv_check("C13 comparator cheat-proof: same-length wrong-expected returns MISMATCH" as *u8, t, ctr)
245 let rc: i64 = gv_verdict("LINUX-GUEST" as *u8, ctr, "F103c linux guest lane: labeled interop guest proven; native refuses guests by construction" as *u8)
246 sys_exit(rc)
247 return rc
248}