code wiki / _hdl_build / _ale_grade_gate.nx
_ale_grade_gate.nx source
↩ module page · 205 lines · 9931 B
1// _ale_grade_gate.nx -- the ALE-R1a gate: sovereign DETERMINISTIC grader-runner core.
2// Diff-lane / no-mocks: runs the REAL sovereign grader nx_ale_grade.elf (built by
3// nx_cc_sovereign->nxasm_x86_main, NO gcc) over REAL fixtures and asserts ALL of:
4// (1) SCORE-EXACT -- artifact byte-identical to the reference grading-units -> 1000
5// (2) SCORE-ZERO -- wholly-wrong artifact (no unit matches) -> 0
6// (3) SCORE-PARTIAL -- subset match (2 of 4 units) -> strict (0,1000), == 500 = (2*1000)/4 data-driven
7// (4) BOUNDED -- every emitted score lies in [0,1000] inclusive (all four runs)
8// (5) DETERMINISTIC -- two consecutive runs on the SAME triple+artifact+reference emit the IDENTICAL score
9// (6) NO-LEAKAGE -- grading art_exact against the reference STAGED INTO A DISTINCT PATH
10// (staged_after/ref.txt, which the artifact phase never saw) emits the
11// IDENTICAL 1000 as grading against ref.txt -> score is a pure function of
12// (reference, artifact), independent of when/where the reference existed
13// TAMPER -- a NON-DETERMINISTIC grader stub (clock-derived score) is REJECTED:
14// two runs on the same inputs emit DIFFERENT scores (determinism BITES)
15// The score is read back from a scratch FILE the grader writes (decimal 0..1000), dodging the
16// 0..255 process-exit-code ceiling. The grader's purity (no clock/rand) IS the oracle -- a pure
17// code-grader needs no external oracle, exactly as ALE-R0a established; the tamper fixture is the
18// negative control. Evidence -> knowledge/status/ale_grade.log (ALEGRADEGATE row; the queue row's
19// ||MARK= reads it). license_tier: ORIGINAL
20import "nx_syscalls.nx"
21
22func 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 }
23func 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 }
24func 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 }
25
26// read whole file into buf (cap), return byte count (0 on open-fail / empty)
27func g_read(path: *u8, buf: *u8, cap: i64) -> i64 {
28 let fd: i64 = sys_openat_rd(path)
29 if fd < 0 { return 0 }
30 var n: i64 = 0
31 var go: i64 = 1
32 while go == 1 {
33 let r: i64 = sys_read(fd, (buf as i64 + n) as *u8, cap - 1 - n)
34 if r <= 0 { go = 0 } else { n = n + r }
35 if n >= cap - 1 { go = 0 }
36 }
37 sys_close(fd)
38 return n
39}
40
41// parse the leading non-negative decimal integer out of buf[0..n); -1 if no digit.
42// Scans digits; stops at the first non-digit AFTER seeing a digit (so a stale tail past
43// the child's "<score>\n" -- left by openat_wr having no O_TRUNC -- is ignored).
44func g_parse_int(buf: *u8, n: i64) -> i64 {
45 var seen: i64 = 0
46 var v: i64 = 0
47 var j: i64 = 0
48 while j < n {
49 let c: i64 = buf[j] as i64
50 if c >= 48 { if c <= 57 { v = (v * 10) + (c - 48); seen = 1 } else { j = n } } else { if seen == 1 { j = n } }
51 j = j + 1
52 }
53 if seen == 0 { return 0 - 1 }
54 return v
55}
56
57// run a grader ELF: execve <elf> <ref> <art> <out>; child writes score to <out>; we read it back.
58// returns the parsed milli-score, or -1 on failure.
59func g_run(elf: *u8, ref: *u8, art: *u8, out: *u8) -> i64 {
60 // openat_wr has no O_TRUNC: blank the scratch file first by removing length ambiguity --
61 // we read exactly what the child wrote because the child writes a fresh short line; to be
62 // safe we read and parse only the leading integer, so any stale tail is ignored.
63 let pid: i64 = sys_fork()
64 if pid == 0 {
65 let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4)
66 if dn >= 0 { sys_dup3(dn, 1, 0); sys_dup3(dn, 2, 0) }
67 let argv: *i64 = sys_mmap(48) as *i64
68 argv[0] = elf as i64
69 argv[1] = ref as i64
70 argv[2] = art as i64
71 argv[3] = out as i64
72 argv[4] = 0
73 let envp: *i64 = sys_mmap(16) as *i64
74 envp[0] = 0
75 sys_execve(elf, argv, envp)
76 sys_exit(127)
77 }
78 let st: *i64 = sys_mmap(16) as *i64
79 sys_wait4(pid, st, 0)
80 let sbuf: *u8 = sys_mmap(64)
81 let sn: i64 = g_read(out, sbuf, 64)
82 if sn <= 0 { return 0 - 1 }
83 return g_parse_int(sbuf, sn)
84}
85
86func main() -> i64 {
87 let elf: *u8 = "_offc/nx_ale_grade.elf" as *u8
88 let nondet: *u8 = "_offc/nx_ale_grade_nondet_stub.elf" as *u8
89 let ref: *u8 = "knowledge/specs/ale_grade_examples/ref.txt" as *u8
90 let refstaged: *u8 = "knowledge/specs/ale_grade_examples/staged_after/ref.txt" as *u8
91 let a_exact: *u8 = "knowledge/specs/ale_grade_examples/art_exact.txt" as *u8
92 let a_zero: *u8 = "knowledge/specs/ale_grade_examples/art_zero.txt" as *u8
93 let a_partial: *u8 = "knowledge/specs/ale_grade_examples/art_partial.txt" as *u8
94 let o1: *u8 = "/tmp/_alegr_o1" as *u8
95 let o2: *u8 = "/tmp/_alegr_o2" as *u8
96 let on: *u8 = "/tmp/_alegr_nd1" as *u8
97 let on2: *u8 = "/tmp/_alegr_nd2" as *u8
98 let on3: *u8 = "/tmp/_alegr_nd3" as *u8
99 let on4: *u8 = "/tmp/_alegr_nd4" as *u8
100 g_p("=== ALE-grade gate (ALE-R1a: sovereign deterministic grader-runner core) ===\n" as *u8)
101
102 // (1) SCORE-EXACT: artifact == reference grading-units -> 1000
103 let s_exact: i64 = g_run(elf, ref, a_exact, o1)
104 var c1: i64 = 0
105 if s_exact == 1000 { c1 = 1 }
106
107 // (2) SCORE-ZERO: wholly-wrong artifact -> 0
108 let s_zero: i64 = g_run(elf, ref, a_zero, o1)
109 var c2: i64 = 0
110 if s_zero == 0 { c2 = 1 }
111
112 // (3) SCORE-PARTIAL: subset (2 of 4) -> strict (0,1000); data-driven == 500
113 let s_part: i64 = g_run(elf, ref, a_partial, o1)
114 var c3: i64 = 0
115 if s_part > 0 { if s_part < 1000 { if s_part == 500 { c3 = 1 } } }
116
117 // (4) BOUNDED: every score above lies within [0,1000] inclusive
118 var c4: i64 = 1
119 if s_exact < 0 { c4 = 0 }
120 if s_exact > 1000 { c4 = 0 }
121 if s_zero < 0 { c4 = 0 }
122 if s_zero > 1000 { c4 = 0 }
123 if s_part < 0 { c4 = 0 }
124 if s_part > 1000 { c4 = 0 }
125
126 // (5) DETERMINISTIC: two consecutive runs on the SAME triple emit the IDENTICAL score
127 let d1: i64 = g_run(elf, ref, a_partial, o1)
128 let d2: i64 = g_run(elf, ref, a_partial, o2)
129 var c5: i64 = 0
130 if d1 == d2 { if d1 >= 0 { c5 = 1 } }
131
132 // (6) NO-LEAKAGE: grade art_exact against the reference STAGED INTO A DISTINCT PATH
133 // (the artifact phase never saw it) -> IDENTICAL 1000 = pure function of (ref, art)
134 let s_staged: i64 = g_run(elf, refstaged, a_exact, o1)
135 var c6: i64 = 0
136 if s_staged == s_exact { if s_staged == 1000 { c6 = 1 } }
137
138 // TAMPER: a NON-DETERMINISTIC grader stub must be REJECTED. Sample it FOUR times on the
139 // SAME inputs; a deterministic grader would emit one constant value, so if ANY two of the
140 // four scores DIFFER the stub is proven non-deterministic and REJECTED (gate RED if it
141 // slips, i.e. all four happened to be equal). Four samples make a single unlucky us-bucket
142 // collision irrelevant -- the determinism contract bites on the variation, not one pair.
143 let t1: i64 = g_run(nondet, ref, a_exact, on)
144 let t2: i64 = g_run(nondet, ref, a_exact, on2)
145 let t3: i64 = g_run(nondet, ref, a_exact, on3)
146 let t4: i64 = g_run(nondet, ref, a_exact, on4)
147 var tamper_rejected: i64 = 0
148 if t1 != t2 { tamper_rejected = 1 }
149 if t1 != t3 { tamper_rejected = 1 }
150 if t1 != t4 { tamper_rejected = 1 }
151 if t2 != t3 { tamper_rejected = 1 }
152 if t2 != t4 { tamper_rejected = 1 }
153 if t3 != t4 { tamper_rejected = 1 }
154
155 g_p(" exact=" as *u8); g_fn(1, s_exact)
156 g_p(" zero=" as *u8); g_fn(1, s_zero)
157 g_p(" partial=" as *u8); g_fn(1, s_part)
158 g_p(" det(" as *u8); g_fn(1, d1); g_p("==" as *u8); g_fn(1, d2); g_p(")" as *u8)
159 g_p(" staged=" as *u8); g_fn(1, s_staged)
160 g_p(" nondet(" as *u8); g_fn(1, t1); g_p("!=" as *u8); g_fn(1, t2); g_p(")\n" as *u8)
161 g_p(" c1_exact=" as *u8); g_fn(1, c1)
162 g_p(" c2_zero=" as *u8); g_fn(1, c2)
163 g_p(" c3_partial=" as *u8); g_fn(1, c3)
164 g_p(" c4_bounded=" as *u8); g_fn(1, c4)
165 g_p(" c5_determ=" as *u8); g_fn(1, c5)
166 g_p(" c6_noleak=" as *u8); g_fn(1, c6)
167 g_p(" tamper_rejected=" as *u8); g_fn(1, tamper_rejected)
168 g_p("\n" as *u8)
169
170 var allok: i64 = 1
171 if c1 == 0 { allok = 0 }
172 if c2 == 0 { allok = 0 }
173 if c3 == 0 { allok = 0 }
174 if c4 == 0 { allok = 0 }
175 if c5 == 0 { allok = 0 }
176 if c6 == 0 { allok = 0 }
177 if tamper_rejected == 0 { allok = 0 }
178
179 let lfd: i64 = sys_openat_append("knowledge/status/ale_grade.log" as *u8, 0x1a4)
180 if allok == 1 {
181 g_p("ALEGRADEGATE verdict=GREEN (exact=1000 zero=0 partial=500 bounded det no-leakage; nondet tamper REJECTED)\n" as *u8)
182 if lfd >= 0 {
183 g_fp(lfd, "ALEGRADEGATE verdict=GREEN exact=1000 zero=0 partial=500 bounded=1 det=1 noleak=1 tamper_rejected=1 rung=ALE-R1a epoch=" as *u8)
184 g_fn(lfd, sys_now_realtime_sec())
185 g_fp(lfd, "\n" as *u8)
186 sys_close(lfd)
187 }
188 sys_exit(0)
189 return 0
190 }
191 g_p("ALEGRADEGATE verdict=RED (a check did not fire)\n" as *u8)
192 if lfd >= 0 {
193 g_fp(lfd, "ALEGRADEGATE verdict=RED c1=" as *u8); g_fn(lfd, c1)
194 g_fp(lfd, " c2=" as *u8); g_fn(lfd, c2)
195 g_fp(lfd, " c3=" as *u8); g_fn(lfd, c3)
196 g_fp(lfd, " c4=" as *u8); g_fn(lfd, c4)
197 g_fp(lfd, " c5=" as *u8); g_fn(lfd, c5)
198 g_fp(lfd, " c6=" as *u8); g_fn(lfd, c6)
199 g_fp(lfd, " tamper_rejected=" as *u8); g_fn(lfd, tamper_rejected)
200 g_fp(lfd, "\n" as *u8)
201 sys_close(lfd)
202 }
203 sys_exit(1)
204 return 1
205}