code wiki / _hdl_build / nx_math_rung_run.nx
nx_math_rung_run.nx source
↩ module page · 195 lines · 9001 B
1// nx_math_rung_run.nx -- MATH-ARC AUTORUN organ: re-verifies EVERY math rung
2// hands-off from the DATA table knowledge/specs/math_rungs.tsv (rule 11: a new
3// rung = a new row, never new orchestration). Per rung, in order:
4// spec emitter -> kernel emitter (demo) -> invariant test ->
5// oracle self-anchor gate -> live-oracle ULP gate ->
6// TAMPER (nx_tamper_lit on the rung's load-bearing literal) -> ULP gate must
7// go RED -> regenerate via the emitter -> ULP gate must return GREEN.
8// Ends with a scorecard refresh and an AUTORUN evidence row appended to
9// knowledge/status/math_engine.log. Exit = number of failed rungs.
10// Every stage builds+runs through the sovereign lane (nx_sov_build_run): the
11// whole math arc is re-proven from source on every beat -- no stale grades.
12// TSV columns: rung spec demo test ogate ugate kernelfile litskip
13// license_tier: ORIGINAL
14
15import "nx_syscalls.nx"
16import "nx_tamper_lit.nx"
17const K_MAGIC_65536: i64 = 65536
18const K_MAGIC_65535: i64 = 65535
19
20func mrr_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
21func mrr_w(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 mrr_putn(v: i64) -> i64 { let bb: *u8 = sys_mmap(28); var m: i64 = v; if m < 0 { m = 0 - m; sys_write(1, "-" as *u8, 1) }; 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); m = m / 10; k = k + 1 }; var i: i64 = 0; while i < k { bb[i] = t[k-1-i]; i = i + 1 }; sys_write(1, bb, k); return 0 }
23
24// build+run a module through the sovereign lane, silenced; returns wait status
25func mrr_stage(base: *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 lane: *u8 = "./_offc/nx_sov_build_run.elf" as *u8
31 let argv: *i64 = sys_mmap(32) as *i64
32 argv[0] = lane as i64
33 argv[1] = base as i64
34 argv[2] = 0
35 let envp: *i64 = sys_mmap(16) as *i64
36 envp[0] = 0
37 sys_execve(lane, 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]
43}
44
45func mrr_report(name: *u8, rc: i64) -> i64 {
46 mrr_puts(" " as *u8)
47 mrr_puts(name)
48 mrr_puts("=" as *u8)
49 if rc == 0 { mrr_puts("ok" as *u8) } else { mrr_puts("FAIL" as *u8) }
50 return 0
51}
52
53func main() -> i64 {
54 let buf: *u8 = sys_mmap(K_MAGIC_65536)
55 let fd: i64 = sys_openat_rd("knowledge/specs/math_rungs.tsv" as *u8)
56 if fd < 0 { mrr_puts("RUNGRUN-ALL verdict=RED reason=no-table\n" as *u8); sys_exit(101) }
57 var n: i64 = 0
58 var r: i64 = sys_read(fd, buf, K_MAGIC_65535)
59 while r > 0 { n = n + r; r = sys_read(fd, buf + n, K_MAGIC_65535 - n) }
60 sys_close(fd)
61
62 // field buffers (7 strings + litskip)
63 let fb: *i64 = sys_mmap(8 * 8) as *i64
64 var fi: i64 = 0
65 while fi < 7 { fb[fi] = sys_mmap(128) as i64; fi = fi + 1 }
66
67 var rungs: i64 = 0
68 var fails: i64 = 0
69 var tp_ok: i64 = 0
70 // durable per-rung evidence: each rung's verdict is APPENDED to the math log
71 // so the ladder rows (ME2-ERF-001/ME2-GAMMA-001) reconcile against the live
72 // RUNGRUN anchor instead of a stdout line that evaporates (no-float wiring).
73 let lg: i64 = sys_openat_append("knowledge/status/math_engine.log" as *u8, 0x1a4)
74 var i: i64 = 0
75 while i < n {
76 // parse one line into 7 string fields + trailing integer
77 var f: i64 = 0
78 var col: i64 = 0
79 var litskip: i64 = 0
80 while f < 8 {
81 if f < 7 {
82 let dst: *u8 = fb[f] as *u8
83 var k: i64 = 0
84 var go: i64 = 1
85 while go == 1 {
86 if i >= n { go = 0 } else {
87 let ch: i64 = buf[i] as i64
88 if ch == 9 { i = i + 1; go = 0 } else {
89 if ch == 10 { go = 0 } else {
90 if k < 120 { dst[k] = ch as u8; k = k + 1 }
91 i = i + 1
92 }
93 }
94 }
95 }
96 dst[k] = 0 as u8
97 if f == 0 { col = k } // rung-name length
98 } else {
99 litskip = 0
100 var go2: i64 = 1
101 while go2 == 1 {
102 if i >= n { go2 = 0 } else {
103 let ch2: i64 = buf[i] as i64
104 if ch2 == 10 { i = i + 1; go2 = 0 } else {
105 if ch2 >= 48 { if ch2 <= 57 { litskip = litskip * 10 + (ch2 - 48) } }
106 i = i + 1
107 }
108 }
109 }
110 }
111 f = f + 1
112 }
113 if col == 0 { i = n } else {
114 rungs = rungs + 1
115 let rname: *u8 = fb[0] as *u8
116 mrr_puts("RUNGRUN rung=" as *u8)
117 mrr_puts(rname)
118 let rc_spec: i64 = mrr_stage(fb[1] as *u8)
119 mrr_report("spec" as *u8, rc_spec)
120 let rc_demo: i64 = mrr_stage(fb[2] as *u8)
121 mrr_report("demo" as *u8, rc_demo)
122 let rc_test: i64 = mrr_stage(fb[3] as *u8)
123 mrr_report("test" as *u8, rc_test)
124 let rc_og: i64 = mrr_stage(fb[4] as *u8)
125 mrr_report("ogate" as *u8, rc_og)
126 let rc_ug: i64 = mrr_stage(fb[5] as *u8)
127 mrr_report("ugate" as *u8, rc_ug)
128 // mechanical honesty proof: tamper -> RED -> regenerate -> GREEN
129 var tred: i64 = 0
130 var tgrn: i64 = 0
131 if tl_flip(fb[6] as *u8, litskip) == 1 {
132 if mrr_stage(fb[5] as *u8) != 0 { tred = 1 }
133 if mrr_stage(fb[2] as *u8) == 0 {
134 if mrr_stage(fb[5] as *u8) == 0 { tgrn = 1 }
135 }
136 }
137 mrr_puts(" tamper-red=" as *u8); mrr_putn(tred)
138 mrr_puts(" regreen=" as *u8); mrr_putn(tgrn)
139 var ok: i64 = 1
140 if rc_spec != 0 { ok = 0 }
141 if rc_demo != 0 { ok = 0 }
142 if rc_test != 0 { ok = 0 }
143 if rc_og != 0 { ok = 0 }
144 if rc_ug != 0 { ok = 0 }
145 if tred == 0 { ok = 0 }
146 if tgrn == 0 { ok = 0 }
147 if ok == 1 {
148 tp_ok = tp_ok + 1
149 mrr_puts(" verdict=GREEN\n" as *u8)
150 if lg >= 0 { mrr_w(lg, "RUNGRUN rung=" as *u8); mrr_w(lg, rname); mrr_w(lg, " stages=spec,demo,test,ogate,ugate tamper-proofs=mechanical verdict=GREEN lane=nx_sov_build_run\n" as *u8) }
151 } else {
152 fails = fails + 1
153 mrr_puts(" verdict=RED\n" as *u8)
154 if lg >= 0 { mrr_w(lg, "RUNGRUN rung=" as *u8); mrr_w(lg, rname); mrr_w(lg, " verdict=RED lane=nx_sov_build_run\n" as *u8) }
155 }
156 }
157 }
158
159 // evidence-derived scorecard refresh (B0 law: grades from gates, live)
160 let rc_sc: i64 = mrr_stage("nx_math_scorecard" as *u8)
161 // no-float math family-search refresh (every beat re-derives the rebuild DAG +
162 // MATHGENE coherence gate from the fresh per-rung evidence above -- the genealogy
163 // can never stale-rot; a math float surfaces in math_genealogy.log within one beat)
164 let rc_gene: i64 = mrr_stage("nx_math_genealogist" as *u8)
165 // standing extension guardrail: re-prove the off-rung proven extensions (erf full-domain,
166 // gamma reflection, integer incomplete-gamma) FROM SOURCE every beat so they cannot rot;
167 // transparently re-measures the negative-x gamma known gap (regression past it is caught).
168 let rc_ext: i64 = mrr_stage("nx_math_ext_verify" as *u8)
169 mrr_puts("RUNGRUN-ALL rungs=" as *u8); mrr_putn(rungs)
170 mrr_puts(" green=" as *u8); mrr_putn(rungs - fails)
171 mrr_puts(" tamper-proofs=" as *u8); mrr_putn(tp_ok)
172 mrr_puts(" genealogy=" as *u8)
173 if rc_gene == 0 { mrr_puts("no-float" as *u8) } else { mrr_puts("FLOAT-OR-FAIL" as *u8) }
174 mrr_puts(" extensions=" as *u8)
175 if rc_ext == 0 { mrr_puts("verified" as *u8) } else { mrr_puts("REGRESSED" as *u8) }
176 mrr_puts(" scorecard=" as *u8)
177 if rc_sc == 0 { mrr_puts("refreshed" as *u8) } else { mrr_puts("FAIL" as *u8) }
178 if fails == 0 {
179 mrr_puts(" verdict=GREEN\n" as *u8)
180 if lg >= 0 {
181 mrr_w(lg, "AUTORUN epoch=run-2026-06-10 organ=nx_math_rung_run table=knowledge/specs/math_rungs.tsv rungs=" as *u8)
182 let d0: *u8 = sys_mmap(8)
183 d0[0] = (48 + (rungs % 10)) as u8
184 d0[1] = 0 as u8
185 mrr_w(lg, d0)
186 mrr_w(lg, " stages=spec,demo,test,ogate,ugate tamper-proofs=mechanical(nx_tamper_lit) verdict=GREEN lane=nx_sov_build_run\n" as *u8)
187 sys_close(lg)
188 }
189 sys_exit(0)
190 }
191 mrr_puts(" verdict=RED\n" as *u8)
192 if lg >= 0 { sys_close(lg) }
193 sys_exit(fails)
194 return 0
195}