nx_uefi_fence_gate.nx source
↩ module page · 331 lines · 13094 B
1// nx_uefi_fence_gate.nx -- F948 "never-brick FENCE gate for UEFI-on-metal" (os lane; deps F103c=D; 2026-07-21).
2// THE CLAIM (rule 26, proven MECHANICALLY not asserted): the autonomous UEFI lane is FILE+EMULATOR-only.
3// Every lane source in knowledge/uefi_lane_manifest.conf is scanned against the data-driven deny list
4// knowledge/uefi_fence_deny.conf: build-class organs (F949 EFI app / F950 ESP builder / F951 boot-proof)
5// may carry ZERO firmware/NVRAM/raw-device write primitives; metal-class organs (F952) must additionally
6// declare NX-OPERATOR-CONFIRM + NX-REMOVABLE-ONLY and still carry ZERO firmware-write primitives -- the
7// only device class they may name is the operator-confirmed removable target. Scanner completeness is
8// proven against a poison fixture that trips EVERY all-class pattern (C09), marker falsifiability against
9// the same (C10), fail-closed on missing files (C03/C11), deterministic (C12), non-vacuous (C13).
10// D001: emits the nx_gate_verdict contract.
11// REFUTATION: argv[1]=negctl injects the poison fixture into the BUILD-class scan set -> the fence tooth
12// (C04) MUST go RED alone; registered sibling nx_uefi_fence_negtest pins that arg.
13// license_tier: ORIGINAL expect_exit: 0 No hw writes (Rule 26): this gate only READS files.
14import "nx_syscalls.nx"
15import "nx_gate_verdict.nx"
16
17const UF_BUF: i64 = 65536
18const UF_TBL: i64 = 512
19const UF_ARENA: i64 = 8192
20const UF_MAXE: i64 = 64
21const UF_FOLD0: i64 = 7
22
23func uf_slen(s: *u8) -> i64 {
24 var n: i64 = 0
25 while s[n] != (0 as u8) { n = n + 1 }
26 return n
27}
28
29// whole-file read: >=0 bytes on success, -1 open-fail (callers treat <0 as ERROR, never as clean)
30func uf_read_all(path: *u8, buf: *u8, cap: i64) -> i64 {
31 let fd: i64 = sys_openat_rd(path)
32 if fd < 0 { return -1 }
33 var tot: i64 = 0
34 var going: i64 = 1
35 while going == 1 {
36 if tot >= cap { going = 0 } else {
37 let r: i64 = sys_read(fd, (buf as i64 + tot) as *u8, cap - tot)
38 if r <= 0 { going = 0 } else { tot = tot + r }
39 }
40 }
41 sys_close(fd)
42 return tot
43}
44
45// naive substring: 1 found / 0 absent
46func uf_find(hay: *u8, hn: i64, pat: *u8, pn: i64) -> i64 {
47 if pn <= 0 { return 0 }
48 if hn < pn { return 0 }
49 var i: i64 = 0
50 while i <= hn - pn {
51 var j: i64 = 0
52 var ok: i64 = 1
53 while j < pn {
54 if hay[i + j] != pat[j] { ok = 0; j = pn } else { j = j + 1 }
55 }
56 if ok == 1 { return 1 }
57 i = i + 1
58 }
59 return 0
60}
61
62// order-sensitive rolling fold (vb_sum family): a swapped pair changes it; length folded too
63func uf_fold(ck: i64, buf: *u8, n: i64) -> i64 {
64 var s: i64 = ck
65 var k: i64 = 0
66 while k < n { s = s * 131 + (buf[k] as i64); k = k + 1 }
67 s = s * 1000003 + n
68 return s
69}
70
71// parse "<class> <token>" rows (# comments + blanks skipped); class a=0 b=1 m=2 other=9.
72// tokens are copied NUL-terminated into arena; returns row count.
73func uf_parse(cbuf: *u8, cn: i64, cls: *i64, sp: *i64, sl: *i64, arena: *u8, abox: *i64, maxe: i64) -> i64 {
74 var n: i64 = 0
75 var i: i64 = 0
76 while i < cn {
77 var le: i64 = i
78 var scanning: i64 = 1
79 while scanning == 1 {
80 if le >= cn { scanning = 0 } else {
81 if cbuf[le] == (10 as u8) { scanning = 0 } else { le = le + 1 }
82 }
83 }
84 if le > i {
85 if cbuf[i] != (35 as u8) {
86 var spx: i64 = i
87 var s2: i64 = 1
88 while s2 == 1 {
89 if spx >= le { s2 = 0 } else {
90 if cbuf[spx] == (32 as u8) { s2 = 0 } else { spx = spx + 1 }
91 }
92 }
93 if spx < le {
94 if n < maxe {
95 let ts: i64 = spx + 1
96 var te: i64 = le
97 var t2: i64 = 1
98 while t2 == 1 {
99 if te <= ts { t2 = 0 } else {
100 let lb: i64 = cbuf[te - 1] as i64
101 if lb == 13 { te = te - 1 } else {
102 if lb == 32 { te = te - 1 } else { t2 = 0 }
103 }
104 }
105 }
106 if te > ts {
107 let c0: i64 = cbuf[i] as i64
108 var cv: i64 = 9
109 if c0 == 97 { cv = 0 }
110 if c0 == 98 { cv = 1 }
111 if c0 == 109 { cv = 2 }
112 cls[n] = cv
113 let ap: i64 = abox[0]
114 let dst: *u8 = (arena as i64 + ap) as *u8
115 let tl: i64 = te - ts
116 var q: i64 = 0
117 while q < tl { dst[q] = cbuf[ts + q]; q = q + 1 }
118 dst[tl] = 0 as u8
119 sp[n] = dst as i64
120 sl[n] = tl
121 abox[0] = ap + tl + 1
122 n = n + 1
123 }
124 }
125 }
126 }
127 }
128 i = le + 1
129 }
130 return n
131}
132
133// scan the manifest set (+ poison injected as build-class when neg=1); res:
134// [0]=readable [1]=bytes [2]=buildHits [3]=metalAllHits [4]=metalBuildHits [5]=confirmAll [6]=removAll [7]=fold [8]=files
135func uf_runset(manC: *i64, manP: *i64, manN: i64, dC: *i64, dP: *i64, dL: *i64, dN: i64, neg: i64, res: *i64) -> i64 {
136 let fbuf: *u8 = sys_mmap(UF_BUF)
137 res[0] = 0
138 res[1] = 0
139 res[2] = 0
140 res[3] = 0
141 res[4] = 0
142 res[5] = 1
143 res[6] = 1
144 res[7] = UF_FOLD0
145 res[8] = 0
146 let m1s: *u8 = "NX-OPERATOR-CONFIRM" as *u8
147 let m2s: *u8 = "NX-REMOVABLE-ONLY" as *u8
148 let pois: *u8 = "knowledge/uefi_fence_fixture_poison.txt" as *u8
149 let total: i64 = manN + neg
150 var k: i64 = 0
151 while k < total {
152 var cls: i64 = 1
153 var pathv: i64 = pois as i64
154 if k < manN {
155 cls = manC[k]
156 pathv = manP[k]
157 }
158 let path: *u8 = pathv as *u8
159 let fn2: i64 = uf_read_all(path, fbuf, UF_BUF)
160 var fl: i64 = fn2
161 if fl < 0 { fl = 0 }
162 if fn2 >= 0 { res[0] = res[0] + 1 }
163 res[1] = res[1] + fl
164 res[8] = res[8] + 1
165 res[7] = uf_fold(res[7], fbuf, fl)
166 var d: i64 = 0
167 while d < dN {
168 let pp: i64 = dP[d]
169 let hit: i64 = uf_find(fbuf, fl, pp as *u8, dL[d])
170 if hit == 1 {
171 let pc: i64 = dC[d]
172 if cls == 1 {
173 if pc <= 1 { res[2] = res[2] + 1 }
174 }
175 if cls == 2 {
176 if pc == 0 { res[3] = res[3] + 1 }
177 if pc == 1 { res[4] = res[4] + 1 }
178 }
179 }
180 d = d + 1
181 }
182 if cls == 2 {
183 let f1: i64 = uf_find(fbuf, fl, m1s, uf_slen(m1s))
184 let f2: i64 = uf_find(fbuf, fl, m2s, uf_slen(m2s))
185 if f1 == 0 { res[5] = 0 }
186 if f2 == 0 { res[6] = 0 }
187 }
188 k = k + 1
189 }
190 sys_munmap(fbuf, UF_BUF)
191 return 0
192}
193
194func main(argc: i64, argv: *i64) -> i64 {
195 var neg: i64 = 0
196 if argc >= 2 {
197 let a1v: i64 = argv[1]
198 let a1: *u8 = a1v as *u8
199 if a1[0] == (110 as u8) { if a1[1] == (101 as u8) { if a1[2] == (103 as u8) { neg = 1 } } }
200 }
201 let ctr: *i64 = gv_ctr()
202 gv_head("UEFI-NEVER-BRICK-FENCE (F948) -- the autonomous UEFI lane is FILE+EMULATOR-only BY CONSTRUCTION: lane sources carry zero firmware/NVRAM/raw-device write primitives; metal is operator-gated removable-only (rule 26, proven mechanically)" as *u8)
203 if neg == 1 { gv_puts(" [negctl] poison fixture injected into the BUILD-class scan set -- the fence tooth C04 MUST go RED\n" as *u8) }
204 let cbuf: *u8 = sys_mmap(UF_BUF)
205 let dC: *i64 = sys_mmap(UF_TBL) as *i64
206 let dP: *i64 = sys_mmap(UF_TBL) as *i64
207 let dL: *i64 = sys_mmap(UF_TBL) as *i64
208 let dAr: *u8 = sys_mmap(UF_ARENA)
209 let dbox: *i64 = sys_mmap(16) as *i64
210 dbox[0] = 0
211 let dn: i64 = uf_read_all("knowledge/uefi_fence_deny.conf" as *u8, cbuf, UF_BUF)
212 var dguard: i64 = dn
213 if dguard < 0 { dguard = 0 }
214 var dnum: i64 = 0
215 if dguard > 0 { dnum = uf_parse(cbuf, dguard, dC, dP, dL, dAr, dbox, UF_MAXE) }
216 var allN: i64 = 0
217 var bldN: i64 = 0
218 var d: i64 = 0
219 while d < dnum {
220 if dC[d] == 0 { allN = allN + 1 }
221 if dC[d] == 1 { bldN = bldN + 1 }
222 d = d + 1
223 }
224 var c01: i64 = 0
225 if allN >= 8 { if bldN >= 2 { c01 = 1 } }
226 gv_check("C01 deny-list loads fail-closed (data-driven; all>=8 build>=2)" as *u8, c01, ctr)
227 let mC: *i64 = sys_mmap(UF_TBL) as *i64
228 let mP: *i64 = sys_mmap(UF_TBL) as *i64
229 let mL: *i64 = sys_mmap(UF_TBL) as *i64
230 let mAr: *u8 = sys_mmap(UF_ARENA)
231 let mbox: *i64 = sys_mmap(16) as *i64
232 mbox[0] = 0
233 let mn: i64 = uf_read_all("knowledge/uefi_lane_manifest.conf" as *u8, cbuf, UF_BUF)
234 var mguard: i64 = mn
235 if mguard < 0 { mguard = 0 }
236 var mnum: i64 = 0
237 if mguard > 0 { mnum = uf_parse(cbuf, mguard, mC, mP, mL, mAr, mbox, UF_MAXE) }
238 var mBld: i64 = 0
239 var mMet: i64 = 0
240 d = 0
241 while d < mnum {
242 if mC[d] == 1 { mBld = mBld + 1 }
243 if mC[d] == 2 { mMet = mMet + 1 }
244 d = d + 1
245 }
246 var c02: i64 = 0
247 if mnum >= 2 { if mBld >= 1 { if mMet >= 1 { c02 = 1 } } }
248 gv_check("C02 lane manifest non-vacuous (>=1 build organ, >=1 metal organ)" as *u8, c02, ctr)
249 let r1: *i64 = sys_mmap(128) as *i64
250 let r2: *i64 = sys_mmap(128) as *i64
251 uf_runset(mC, mP, mnum, dC, dP, dL, dnum, neg, r1)
252 uf_runset(mC, mP, mnum, dC, dP, dL, dnum, neg, r2)
253 let expect: i64 = mnum + neg
254 var c03: i64 = 0
255 if r1[0] == expect { if expect >= 2 { c03 = 1 } }
256 gv_check("C03 every scanned lane file exists+readable (fail-closed)" as *u8, c03, ctr)
257 var c04: i64 = 0
258 if r1[2] == 0 { c04 = 1 }
259 gv_check("C04 THE FENCE: build-class lane carries ZERO firmware/raw-device write primitives" as *u8, c04, ctr)
260 var c05: i64 = 0
261 if r1[3] == 0 { c05 = 1 }
262 gv_check("C05 metal-class organs carry ZERO firmware-write primitives (rule 26 holds even under the operator gate)" as *u8, c05, ctr)
263 var c06: i64 = 0
264 if r1[5] == 1 { c06 = 1 }
265 gv_check("C06 metal-class organs declare NX-OPERATOR-CONFIRM" as *u8, c06, ctr)
266 var c07: i64 = 0
267 if r1[6] == 1 { c07 = 1 }
268 gv_check("C07 metal-class organs declare NX-REMOVABLE-ONLY" as *u8, c07, ctr)
269 var c08: i64 = 0
270 if r1[4] >= 1 { c08 = 1 }
271 gv_check("C08 class fence is REAL: metal fixture trips the build-class raw-device deny (not scanner blindness)" as *u8, c08, ctr)
272 let pn2: i64 = uf_read_all("knowledge/uefi_fence_fixture_poison.txt" as *u8, cbuf, UF_BUF)
273 var pl: i64 = pn2
274 if pl < 0 { pl = 0 }
275 var pAll: i64 = 0
276 d = 0
277 while d < dnum {
278 if dC[d] == 0 {
279 let pp2: i64 = dP[d]
280 let ph: i64 = uf_find(cbuf, pl, pp2 as *u8, dL[d])
281 if ph == 1 { pAll = pAll + 1 }
282 }
283 d = d + 1
284 }
285 var c09: i64 = 0
286 if allN > 0 { if pAll == allN { c09 = 1 } }
287 gv_check("C09 scanner completeness: poison fixture trips EVERY all-class deny pattern" as *u8, c09, ctr)
288 let m1s2: *u8 = "NX-OPERATOR-CONFIRM" as *u8
289 let m2s2: *u8 = "NX-REMOVABLE-ONLY" as *u8
290 let pm1: i64 = uf_find(cbuf, pl, m1s2, uf_slen(m1s2))
291 let pm2: i64 = uf_find(cbuf, pl, m2s2, uf_slen(m2s2))
292 var c10: i64 = 0
293 if pm1 == 0 { if pm2 == 0 { c10 = 1 } }
294 gv_check("C10 marker check falsifiable: poison carries NEITHER operator marker" as *u8, c10, ctr)
295 let bad: i64 = uf_read_all("knowledge/uefi_fence_no_such_zz.conf" as *u8, cbuf, UF_BUF)
296 var c11: i64 = 0
297 if bad < 0 { c11 = 1 }
298 gv_check("C11 fail-closed: a missing file reads as ERROR, never as a clean pass" as *u8, c11, ctr)
299 var c12: i64 = 0
300 if r1[7] == r2[7] { if r1[1] > 0 { c12 = 1 } }
301 gv_check("C12 determinism: two full lane scans fold IDENTICAL" as *u8, c12, ctr)
302 var c13: i64 = 0
303 if r1[1] > 0 { if r1[8] >= 2 { if pn2 > 0 { c13 = 1 } } }
304 gv_check("C13 non-vacuity: real bytes scanned across the set + poison" as *u8, c13, ctr)
305 gv_puts(" evidence: deny_all=" as *u8)
306 gv_num(allN)
307 gv_puts(" deny_build=" as *u8)
308 gv_num(bldN)
309 gv_puts(" man=" as *u8)
310 gv_num(mnum)
311 gv_puts(" bfiles=" as *u8)
312 gv_num(mBld)
313 gv_puts(" mfiles=" as *u8)
314 gv_num(mMet)
315 gv_puts(" bhits=" as *u8)
316 gv_num(r1[2])
317 gv_puts(" mahits=" as *u8)
318 gv_num(r1[3])
319 gv_puts(" mbhits=" as *u8)
320 gv_num(r1[4])
321 gv_puts(" phits=" as *u8)
322 gv_num(pAll)
323 gv_puts(" bytes=" as *u8)
324 gv_num(r1[1])
325 gv_puts(" fold=" as *u8)
326 gv_num(r1[7])
327 gv_puts("\n" as *u8)
328 let rc: i64 = gv_verdict("UEFI-FENCE" as *u8, ctr, "autonomous UEFI path FILE+EMULATOR-only; metal operator-gated removable-only" as *u8)
329 sys_exit(rc)
330 return rc
331}