code wiki / _hdl_build / _ale_format_gate.nx
_ale_format_gate.nx source
↩ module page · 162 lines · 7664 B
1// _ale_format_gate.nx -- the ALE-FORMAT gate (rungs ALE-R0a/R0b, sovereign schema).
2// Diff-lane / no-mocks: runs the REAL sovereign validator nx_ale_format_validate.elf
3// (built by nx_cc_sovereign->nxasm_x86_main, NO gcc) over REAL fixtures and asserts:
4// ACCEPT-1 -- validator EXIT 0 on the golden valid triple (good_triple.txt)
5// ACCEPT-2 -- validator EXIT 0 on the FIRST EXTERNAL fixture ale_real_task01.txt
6// (demo/hello from rdi-berkeley/agents-last-exam@6b7f1b98, real provenance)
7// REJECT-1 -- validator NONZERO on bad_missing.txt (missing required field)
8// REJECT-2 -- validator NONZERO on bad_range.txt (score out of [0,1])
9// REJECT-3 -- validator NONZERO on bad_nondet.txt (grader non-deterministic)
10// REJECT-4 -- validator NONZERO on bad_leak.txt (staged_reference_after=no LEAKAGE)
11// REJECT-5 -- validator NONZERO on bad_humanjudge.txt (code_graded=no HUMAN JUDGE)
12// SPEC -- ale_format.spec carries the three contract names + PROVENANCE + RECONCILED
13// The "diff" here = the sovereign ACCEPT lane vs the REFUSAL lane disagreeing on
14// valid-vs-tampered input (the validator's own exit code is the gating signal). The
15// REAL Berkeley repo is the external oracle: ale_real_task01 is extracted from the
16// actual cloned code, so the spec is no longer self-authored-only. Evidence ->
17// knowledge/status/ale_format.log (ALEFMTGATE row; the queue row's ||MARK= reads
18// it). license_tier: ORIGINAL
19import "nx_syscalls.nx"
20
21func 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 }
22func 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 }
23func 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 }
24
25// run nx_ale_format_validate.elf <triple>; return child exit code (decoded from wait status)
26func g_run_val(triple: *u8) -> i64 {
27 let pid: i64 = sys_fork()
28 if pid == 0 {
29 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4)
30 if dn >= 0 { sys_dup3(dn, 1, 0); sys_dup3(dn, 2, 0) }
31 let argv: *i64 = sys_mmap(32) as *i64
32 argv[0] = "_offc/nx_ale_format_validate.elf" as *u8 as i64
33 argv[1] = triple as i64
34 argv[2] = 0
35 let envp: *i64 = sys_mmap(16) as *i64
36 envp[0] = 0
37 sys_execve("_offc/nx_ale_format_validate.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// does the file at path contain pat (substring, anywhere)? 1/0
46func g_file_has(path: *u8, pat: *u8) -> i64 {
47 let buf: *u8 = sys_mmap(262144)
48 let fd: i64 = sys_openat_rd(path)
49 if fd < 0 { return 0 }
50 var n: i64 = 0
51 var go: i64 = 1
52 while go == 1 {
53 let r: i64 = sys_read(fd, (buf as i64 + n) as *u8, 262143 - n)
54 if r <= 0 { go = 0 } else { n = n + r }
55 if n >= 262143 { go = 0 }
56 }
57 sys_close(fd)
58 var pl: i64 = 0
59 while pat[pl] != (0 as u8) { pl = pl + 1 }
60 var i: i64 = 0
61 while i + pl <= n {
62 var k: i64 = 0
63 var hit: i64 = 1
64 while k < pl { if buf[i + k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } }
65 if hit == 1 { return 1 }
66 i = i + 1
67 }
68 return 0
69}
70
71func main() -> i64 {
72 let spec: *u8 = "knowledge/specs/ale_format.spec" as *u8
73 let good: *u8 = "knowledge/specs/ale_examples/good_triple.txt" as *u8
74 let real1: *u8 = "knowledge/specs/ale_examples/ale_real_task01.txt" as *u8
75 let bmiss: *u8 = "knowledge/specs/ale_examples/bad_missing.txt" as *u8
76 let brange: *u8 = "knowledge/specs/ale_examples/bad_range.txt" as *u8
77 let bnondet: *u8 = "knowledge/specs/ale_examples/bad_nondet.txt" as *u8
78 let bleak: *u8 = "knowledge/specs/ale_examples/bad_leak.txt" as *u8
79 let bhuman: *u8 = "knowledge/specs/ale_examples/bad_humanjudge.txt" as *u8
80 g_p("=== ALE-format gate (ALE-R0b: real-repo-grounded validator + tamper refusal) ===\n" as *u8)
81
82 // PRIMARY accept lane -- 2 goldens (synthetic + REAL external fixture) MUST pass
83 let rc_good: i64 = g_run_val(good)
84 var accept_good: i64 = 0
85 if rc_good == 0 { accept_good = 1 }
86 let rc_real: i64 = g_run_val(real1)
87 var accept_real: i64 = 0
88 if rc_real == 0 { accept_real = 1 }
89
90 // refusal lane -- each tamper MUST be rejected (nonzero)
91 let rc_miss: i64 = g_run_val(bmiss)
92 let rc_range: i64 = g_run_val(brange)
93 let rc_nondet: i64 = g_run_val(bnondet)
94 let rc_leak: i64 = g_run_val(bleak)
95 let rc_human: i64 = g_run_val(bhuman)
96 var rej_miss: i64 = 0
97 if rc_miss != 0 { rej_miss = 1 }
98 var rej_range: i64 = 0
99 if rc_range != 0 { rej_range = 1 }
100 var rej_nondet: i64 = 0
101 if rc_nondet != 0 { rej_nondet = 1 }
102 var rej_leak: i64 = 0
103 if rc_leak != 0 { rej_leak = 1 }
104 var rej_human: i64 = 0
105 if rc_human != 0 { rej_human = 1 }
106
107 // spec carries the three contract names + a PROVENANCE + a RECONCILED line
108 var spec_ok: i64 = 1
109 if g_file_has(spec, "task|" as *u8) == 0 { spec_ok = 0 }
110 if g_file_has(spec, "grader|" as *u8) == 0 { spec_ok = 0 }
111 if g_file_has(spec, "deployer|" as *u8) == 0 { spec_ok = 0 }
112 if g_file_has(spec, "PROVENANCE|" as *u8) == 0 { spec_ok = 0 }
113 if g_file_has(spec, "RECONCILED|" as *u8) == 0 { spec_ok = 0 }
114
115 g_p(" accept(good)=" as *u8); g_fn(1, accept_good)
116 g_p(" accept(real)=" as *u8); g_fn(1, accept_real)
117 g_p(" reject(missing)=" as *u8); g_fn(1, rej_miss)
118 g_p(" reject(range)=" as *u8); g_fn(1, rej_range)
119 g_p(" reject(nondet)=" as *u8); g_fn(1, rej_nondet)
120 g_p(" reject(leak)=" as *u8); g_fn(1, rej_leak)
121 g_p(" reject(human)=" as *u8); g_fn(1, rej_human)
122 g_p(" spec_ok=" as *u8); g_fn(1, spec_ok)
123 g_p("\n" as *u8)
124
125 var allok: i64 = 1
126 if accept_good == 0 { allok = 0 }
127 if accept_real == 0 { allok = 0 }
128 if rej_miss == 0 { allok = 0 }
129 if rej_range == 0 { allok = 0 }
130 if rej_nondet == 0 { allok = 0 }
131 if rej_leak == 0 { allok = 0 }
132 if rej_human == 0 { allok = 0 }
133 if spec_ok == 0 { allok = 0 }
134
135 let lfd: i64 = sys_openat_append("knowledge/status/ale_format.log" as *u8, 0x1a4)
136 if allok == 1 {
137 g_p("ALEFMTGATE verdict=GREEN (validator ACCEPTS 2 goldens + REJECTS 5 tampers; real-repo grounded)\n" as *u8)
138 if lfd >= 0 {
139 g_fp(lfd, "ALEFMTGATE verdict=GREEN accept=2 reject=5 spec=ok ext_fixture=ale_real_task01 repo=rdi-berkeley/agents-last-exam@6b7f1b98 rung=ALE-R0b epoch=" as *u8)
140 g_fn(lfd, sys_now_realtime_sec())
141 g_fp(lfd, "\n" as *u8)
142 sys_close(lfd)
143 }
144 sys_exit(0)
145 return 0
146 }
147 g_p("ALEFMTGATE verdict=RED (a check did not fire)\n" as *u8)
148 if lfd >= 0 {
149 g_fp(lfd, "ALEFMTGATE verdict=RED accept_good=" as *u8); g_fn(lfd, accept_good)
150 g_fp(lfd, " accept_real=" as *u8); g_fn(lfd, accept_real)
151 g_fp(lfd, " rej_miss=" as *u8); g_fn(lfd, rej_miss)
152 g_fp(lfd, " rej_range=" as *u8); g_fn(lfd, rej_range)
153 g_fp(lfd, " rej_nondet=" as *u8); g_fn(lfd, rej_nondet)
154 g_fp(lfd, " rej_leak=" as *u8); g_fn(lfd, rej_leak)
155 g_fp(lfd, " rej_human=" as *u8); g_fn(lfd, rej_human)
156 g_fp(lfd, " spec_ok=" as *u8); g_fn(lfd, spec_ok)
157 g_fp(lfd, "\n" as *u8)
158 sys_close(lfd)
159 }
160 sys_exit(1)
161 return 1
162}