code wiki / _hdl_build / _ale_verify_gate.nx
_ale_verify_gate.nx source
↩ module page · 327 lines · 14315 B
1// _ale_verify_gate.nx -- the ALE-R2c gate: sovereign agent-core SELF-VERIFY phase organ.
2// Diff-lane / no-mocks: runs the REAL sovereign planner nx_ale_plan.elf + executor nx_ale_exec.elf
3// (both nx_cc_sovereign->nxasm_x86_main, NO gcc) to PRODUCE a real hello-kv-extract artifact, then
4// runs the REAL self-verify organ nx_ale_verify.elf and the REAL independent grader nx_ale_grade.elf
5// over the SAME (reference, artifact) pair, and asserts:
6// (1) HONEST-SELF-SCORE -- nx_ale_verify's self-score BYTE-EQUALS an independent nx_ale_grade
7// run on the same (reference, artifact); on the GOOD artifact == 1000
8// (2) WRONG-ARTIFACT-<1000 -- a corrupted artifact (one unit| line dropped) self-scores < 1000
9// AND that self-score BYTE-EQUALS the independent grade of the bad art
10// (3) NO-LEAKAGE -- self-score is BYTE-IDENTICAL whether or not a decoy reference.txt is
11// planted in the sandbox (verify resolves the ref ONLY from the spec)
12// (4) DETERMINISTIC -- two nx_ale_verify runs on the same (task, artifact) -> byte-identical
13// milli-score scoreout files
14// (5) TAMPER REJECTED -- a degenerate/empty artifact self-scores 0 (negative control: the
15// self-verify is not vacuously green)
16// Evidence -> knowledge/status/ale_verify.log (ALEVERIFYGATE row; the queue row's ||MARK= reads it).
17// Sovereign orchestration (fork/dup3/execve/wait4 + mkdirat). license_tier: ORIGINAL
18import "nx_syscalls.nx"
19
20func g_p(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
21func g_fp(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 }
22func g_fn(fd: i64, v: i64) -> i64 { let bb: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m }; let t: *u8 = sys_mmap(28); var k: i64 = 0; if m == 0 { t[0] = 48; k = 1 }; while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }; var i: i64 = 0; while i < k { bb[i] = t[k - 1 - i]; i = i + 1 }; sys_write(fd, bb, k); return 0 }
23
24// run nx_ale_plan.elf <task> <planout>; return child exit code
25func g_run_plan(task: *u8, planout: *u8) -> i64 {
26 let pid: i64 = sys_fork()
27 if pid == 0 {
28 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4)
29 if dn >= 0 { sys_dup3(dn, 1, 0); sys_dup3(dn, 2, 0) }
30 let argv: *i64 = sys_mmap(32) as *i64
31 argv[0] = "_offc/nx_ale_plan.elf" as *u8 as i64
32 argv[1] = task as i64
33 argv[2] = planout as i64
34 argv[3] = 0
35 let envp: *i64 = sys_mmap(16) as *i64
36 envp[0] = 0
37 sys_execve("_offc/nx_ale_plan.elf" as *u8, argv, envp)
38 sys_exit(127)
39 }
40 let st: *i64 = sys_mmap(16) as *i64
41 sys_wait4(pid, st, 0)
42 return (st[0] >> 8) & 0xff
43}
44
45// run nx_ale_exec.elf <plan> <task> <sandbox>; return child exit code
46func g_run_exec(plan: *u8, task: *u8, sandbox: *u8) -> i64 {
47 let pid: i64 = sys_fork()
48 if pid == 0 {
49 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4)
50 if dn >= 0 { sys_dup3(dn, 1, 0); sys_dup3(dn, 2, 0) }
51 let argv: *i64 = sys_mmap(48) as *i64
52 argv[0] = "_offc/nx_ale_exec.elf" as *u8 as i64
53 argv[1] = plan as i64
54 argv[2] = task as i64
55 argv[3] = sandbox as i64
56 argv[4] = 0
57 let envp: *i64 = sys_mmap(16) as *i64
58 envp[0] = 0
59 sys_execve("_offc/nx_ale_exec.elf" as *u8, argv, envp)
60 sys_exit(127)
61 }
62 let st: *i64 = sys_mmap(16) as *i64
63 sys_wait4(pid, st, 0)
64 return (st[0] >> 8) & 0xff
65}
66
67// run nx_ale_verify.elf <task> <artifact> <scoreout>; return child exit code
68func g_run_verify(task: *u8, art: *u8, scoreout: *u8) -> i64 {
69 let pid: i64 = sys_fork()
70 if pid == 0 {
71 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4)
72 if dn >= 0 { sys_dup3(dn, 1, 0); sys_dup3(dn, 2, 0) }
73 let argv: *i64 = sys_mmap(48) as *i64
74 argv[0] = "_offc/nx_ale_verify.elf" as *u8 as i64
75 argv[1] = task as i64
76 argv[2] = art as i64
77 argv[3] = scoreout as i64
78 argv[4] = 0
79 let envp: *i64 = sys_mmap(16) as *i64
80 envp[0] = 0
81 sys_execve("_offc/nx_ale_verify.elf" as *u8, argv, envp)
82 sys_exit(127)
83 }
84 let st: *i64 = sys_mmap(16) as *i64
85 sys_wait4(pid, st, 0)
86 return (st[0] >> 8) & 0xff
87}
88
89// run nx_ale_grade.elf <ref> <artifact> <scoreout>; return child exit code
90func g_run_grade(ref: *u8, art: *u8, scoreout: *u8) -> i64 {
91 let pid: i64 = sys_fork()
92 if pid == 0 {
93 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4)
94 if dn >= 0 { sys_dup3(dn, 1, 0); sys_dup3(dn, 2, 0) }
95 let argv: *i64 = sys_mmap(48) as *i64
96 argv[0] = "_offc/nx_ale_grade.elf" as *u8 as i64
97 argv[1] = ref as i64
98 argv[2] = art as i64
99 argv[3] = scoreout as i64
100 argv[4] = 0
101 let envp: *i64 = sys_mmap(16) as *i64
102 envp[0] = 0
103 sys_execve("_offc/nx_ale_grade.elf" as *u8, argv, envp)
104 sys_exit(127)
105 }
106 let st: *i64 = sys_mmap(16) as *i64
107 sys_wait4(pid, st, 0)
108 return (st[0] >> 8) & 0xff
109}
110
111// read whole file into buf (cap), return byte count (0 on open-fail / empty)
112func g_read(path: *u8, buf: *u8, cap: i64) -> i64 {
113 let fd: i64 = sys_openat_rd(path)
114 if fd < 0 { return 0 }
115 var n: i64 = 0
116 var go: i64 = 1
117 while go == 1 {
118 let r: i64 = sys_read(fd, (buf as i64 + n) as *u8, cap - 1 - n)
119 if r <= 0 { go = 0 } else { n = n + r }
120 if n >= cap - 1 { go = 0 }
121 }
122 sys_close(fd)
123 return n
124}
125
126func g_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
127
128// two files byte-identical? 1/0 (both must be non-empty)
129func g_files_eq(pa: *u8, pb: *u8) -> i64 {
130 let ba: *u8 = sys_mmap(262144)
131 let bb: *u8 = sys_mmap(262144)
132 let na: i64 = g_read(pa, ba, 262144)
133 let nb: i64 = g_read(pb, bb, 262144)
134 if na != nb { return 0 }
135 if na == 0 { return 0 }
136 var i: i64 = 0
137 while i < na { if ba[i] != bb[i] { return 0 } i = i + 1 }
138 return 1
139}
140
141// parse leading non-negative decimal score from a file (0 if none/empty)
142func g_score_of(path: *u8) -> i64 {
143 let sb: *u8 = sys_mmap(64)
144 let n: i64 = g_read(path, sb, 64)
145 var v: i64 = 0
146 var i: i64 = 0
147 while i < n {
148 if sb[i] >= (48 as u8) { if sb[i] <= (57 as u8) { v = v * 10 + (sb[i] - 48) } }
149 i = i + 1
150 }
151 return v
152}
153
154// write n bytes from buf to a fresh file at path. 1/0.
155func g_write_file(path: *u8, buf: *u8, n: i64) -> i64 {
156 let fd: i64 = sys_openat_wr(path, 0x1a4)
157 if fd < 0 { return 0 }
158 if n > 0 { sys_write(fd, buf, n) }
159 sys_close(fd)
160 return 1
161}
162
163// copy a complete line of buf into out UNLESS it begins with skippref (drop that one line).
164// Drops exactly the FIRST line whose start matches skippref; copies all other bytes verbatim.
165// Returns the produced byte count.
166func g_drop_line(buf: *u8, n: i64, skippref: *u8, out: *u8) -> i64 {
167 let sp: i64 = g_len(skippref)
168 var o: i64 = 0
169 var i: i64 = 0
170 var dropped: i64 = 0
171 while i < n {
172 var atbol: i64 = 0
173 if i == 0 { atbol = 1 } else { if buf[i - 1] == (10 as u8) { atbol = 1 } }
174 var ismatch: i64 = 0
175 if atbol == 1 {
176 if dropped == 0 {
177 if i + sp <= n {
178 var k: i64 = 0
179 var eq: i64 = 1
180 while k < sp { if buf[i + k] != skippref[k] { eq = 0 } k = k + 1 }
181 if eq == 1 { ismatch = 1 }
182 }
183 }
184 }
185 if ismatch == 1 {
186 // skip this entire line (up to and including its newline)
187 dropped = 1
188 var p: i64 = i
189 var go: i64 = 1
190 while go == 1 {
191 if p >= n { go = 0 } else {
192 if buf[p] == (10 as u8) { p = p + 1; go = 0 } else { p = p + 1 }
193 }
194 }
195 i = p
196 } else {
197 out[o] = buf[i]; o = o + 1; i = i + 1
198 }
199 }
200 return o
201}
202
203func main() -> i64 {
204 let task: *u8 = "knowledge/specs/ale_exec_examples/task_exec.txt" as *u8
205 let reference: *u8 = "knowledge/specs/ale_exec_examples/reference.txt" as *u8
206 let planp: *u8 = "/tmp/_aleverify_g_plan" as *u8
207 let sb1: *u8 = "/tmp/_aleverify_g_sb1" as *u8
208 let sbdec: *u8 = "/tmp/_aleverify_g_sbdecoy" as *u8
209 let art1: *u8 = "/tmp/_aleverify_g_sb1/result.units" as *u8
210 let artdec: *u8 = "/tmp/_aleverify_g_sbdecoy/result.units" as *u8
211 let decoyref: *u8 = "/tmp/_aleverify_g_sbdecoy/reference.txt" as *u8
212 let badart: *u8 = "/tmp/_aleverify_g_badart" as *u8
213 let emptyart: *u8 = "/tmp/_aleverify_g_emptyart" as *u8
214 // scoreout scratch paths (verify-side vs independent-grade-side, kept distinct for byte-compare)
215 let v_self1: *u8 = "/tmp/_aleverify_g_self1" as *u8
216 let v_self2: *u8 = "/tmp/_aleverify_g_self2" as *u8
217 let v_selfdec: *u8 = "/tmp/_aleverify_g_selfdecoy" as *u8
218 let v_selfbad: *u8 = "/tmp/_aleverify_g_selfbad" as *u8
219 let v_selfempty: *u8 = "/tmp/_aleverify_g_selfempty" as *u8
220 let i_good: *u8 = "/tmp/_aleverify_g_indgood" as *u8
221 let i_bad: *u8 = "/tmp/_aleverify_g_indbad" as *u8
222
223 g_p("=== ALE-verify gate (ALE-R2c: sovereign agent-core SELF-VERIFY phase) ===\n" as *u8)
224
225 // fresh sandbox dirs (mkdir idempotent; artifact writes use O_TRUNC inside the executor)
226 sys_mkdir(sb1, 0x1ed)
227 sys_mkdir(sbdec, 0x1ed)
228
229 // PRODUCE the good artifact: REAL planner -> REAL executor over the fixture into sb1.
230 let rcplan: i64 = g_run_plan(task, planp)
231 let rcexec: i64 = g_run_exec(planp, task, sb1)
232 let abuf: *u8 = sys_mmap(262144)
233 let an: i64 = g_read(art1, abuf, 262144)
234
235 // (1) HONEST-SELF-SCORE: self-score (verify) byte-equals independent grade on same pair == 1000.
236 let rcv1: i64 = g_run_verify(task, art1, v_self1)
237 let rcig: i64 = g_run_grade(reference, art1, i_good)
238 let self1: i64 = g_score_of(v_self1)
239 let ind1: i64 = g_score_of(i_good)
240 var c1: i64 = 0
241 if rcv1 == 0 { if rcig == 0 { if g_files_eq(v_self1, i_good) == 1 { if self1 == 1000 { c1 = 1 } } } }
242
243 // (2) WRONG-ARTIFACT-<1000: drop one unit| line -> self-score < 1000 AND == independent grade.
244 let bbuf: *u8 = sys_mmap(262144)
245 let bn: i64 = g_drop_line(abuf, an, "unit|checksum|" as *u8, bbuf)
246 g_write_file(badart, bbuf, bn)
247 let rcv2: i64 = g_run_verify(task, badart, v_selfbad)
248 let rcib: i64 = g_run_grade(reference, badart, i_bad)
249 let selfbad: i64 = g_score_of(v_selfbad)
250 let indbad: i64 = g_score_of(i_bad)
251 var c2: i64 = 0
252 if rcv2 == 0 { if rcib == 0 { if selfbad < 1000 { if g_files_eq(v_selfbad, i_bad) == 1 { c2 = 1 } } } }
253
254 // (3) NO-LEAKAGE: plant a decoy reference.txt in a sandbox and re-run verify against the SAME
255 // good artifact; the reference is resolved ONLY from the task spec -> self-score unchanged.
256 // The decoy is DELIBERATELY a wrong reference (would mis-score if verify ever read it).
257 let decoytxt: *u8 = "unit|row_count|999\nunit|header|XXX\nunit|sorted_by|nope\nunit|checksum|dead\nunit|extra|leak\n" as *u8
258 g_write_file(decoyref, decoytxt, g_len(decoytxt))
259 let rcvd: i64 = g_run_verify(task, art1, v_selfdec)
260 let selfdec: i64 = g_score_of(v_selfdec)
261 var c3: i64 = 0
262 if rcvd == 0 { if g_files_eq(v_selfdec, v_self1) == 1 { if selfdec == self1 { c3 = 1 } } }
263
264 // (4) DETERMINISTIC: a 2nd verify run on the same (task, good artifact) -> byte-identical score.
265 let rcv2b: i64 = g_run_verify(task, art1, v_self2)
266 var c4: i64 = 0
267 if rcv2b == 0 { if g_files_eq(v_self1, v_self2) == 1 { c4 = 1 } }
268
269 // (5) TAMPER REJECTED (negative control): a degenerate/EMPTY artifact self-scores 0 -- proving
270 // the self-verify is not vacuously green (an empty deliverable cannot self-certify).
271 g_write_file(emptyart, "" as *u8, 0)
272 let rcve: i64 = g_run_verify(task, emptyart, v_selfempty)
273 let selfempty: i64 = g_score_of(v_selfempty)
274 var c5: i64 = 0
275 if rcve == 0 { if selfempty == 0 { c5 = 1 } }
276
277 g_p(" rc_plan=" as *u8); g_fn(1, rcplan)
278 g_p(" rc_exec=" as *u8); g_fn(1, rcexec)
279 g_p(" art_bytes=" as *u8); g_fn(1, an)
280 g_p(" self_good=" as *u8); g_fn(1, self1)
281 g_p(" ind_good=" as *u8); g_fn(1, ind1)
282 g_p(" self_bad=" as *u8); g_fn(1, selfbad)
283 g_p(" ind_bad=" as *u8); g_fn(1, indbad)
284 g_p(" self_decoy=" as *u8); g_fn(1, selfdec)
285 g_p(" self_empty=" as *u8); g_fn(1, selfempty)
286 g_p("\n" as *u8)
287 g_p(" c1_honest_self_score=" as *u8); g_fn(1, c1)
288 g_p(" c2_wrong_below_1000=" as *u8); g_fn(1, c2)
289 g_p(" c3_no_leakage=" as *u8); g_fn(1, c3)
290 g_p(" c4_deterministic=" as *u8); g_fn(1, c4)
291 g_p(" c5_tamper_rejected=" as *u8); g_fn(1, c5)
292 g_p("\n" as *u8)
293
294 var allok: i64 = 1
295 if c1 == 0 { allok = 0 }
296 if c2 == 0 { allok = 0 }
297 if c3 == 0 { allok = 0 }
298 if c4 == 0 { allok = 0 }
299 if c5 == 0 { allok = 0 }
300
301 let lfd: i64 = sys_openat_append("knowledge/status/ale_verify.log" as *u8, 0x1a4)
302 if allok == 1 {
303 g_p("ALEVERIFYGATE verdict=GREEN (honest self-score==independent==1000; wrong-artifact<1000==independent; no-leakage decoy-ignored; deterministic; empty-artifact self-scores 0)\n" as *u8)
304 if lfd >= 0 {
305 g_fp(lfd, "ALEVERIFYGATE verdict=GREEN honest_self_score=1 wrong_below_1000=1 no_leakage=1 deterministic=1 tamper_rejected=1 self_good=1000 self_bad=" as *u8)
306 g_fn(lfd, selfbad)
307 g_fp(lfd, " self_empty=0 rung=ALE-R2c epoch=" as *u8)
308 g_fn(lfd, sys_now_realtime_sec())
309 g_fp(lfd, "\n" as *u8)
310 sys_close(lfd)
311 }
312 sys_exit(0)
313 return 0
314 }
315 g_p("ALEVERIFYGATE verdict=RED (a check did not fire)\n" as *u8)
316 if lfd >= 0 {
317 g_fp(lfd, "ALEVERIFYGATE verdict=RED c1=" as *u8); g_fn(lfd, c1)
318 g_fp(lfd, " c2=" as *u8); g_fn(lfd, c2)
319 g_fp(lfd, " c3=" as *u8); g_fn(lfd, c3)
320 g_fp(lfd, " c4=" as *u8); g_fn(lfd, c4)
321 g_fp(lfd, " c5=" as *u8); g_fn(lfd, c5)
322 g_fp(lfd, "\n" as *u8)
323 sys_close(lfd)
324 }
325 sys_exit(1)
326 return 1
327}