nx_gvmigrate.nx source
↩ module page · 367 lines · 14546 B
1// nx_gvmigrate.nx -- STAGE the gv_check -> gv_check_eq migration (the edit substrate, not the judge).
2//
3// WHY THIS EXISTS. nx_gatelaw_gate's L4 axis measures gates that EMIT their values and reads 2 of 3,422:
4// 666 gates already inherit the base class and print only PASS or FAIL. An arithmetic that cannot see a
5// number can never contradict one, so a PASS-only gate makes an independent SECOND METHOD CLASS
6// structurally impossible -- that is the fleet-level reason PROVEN reads 0/105. gv_check_eq(name, actual,
7// expected, ctr) asserts AND emits in ONE expression, so the number tested and the number published
8// cannot drift apart by construction. The primitive shipped; the TRANSFORMATION was missing.
9//
10// WHAT THIS IS NOT: a second migrator. nx_gate_migrate already owns the dangerous half -- a 4-clause
11// judge-equivalence oracle (exit code, verdict line, PASS/FAIL vector, evidence side-effect) with
12// commit-or-restore never-brick. This organ only writes <src>.migrated, exactly as nx_dedup_migrate
13// stage does, and hands it to that verifier. Composing the proven judge beats re-implementing it, and
14// a second ruler over gate equivalence is precisely the duplicate-ruler defect.
15//
16// SCOPE, MEASURED OVER THE POPULATION, NOT SAMPLED. 901 call sites, corpus_complete=1: 670 carry '==',
17// 147 '>', 44 '>=', 44 '<', 42 ne, 24 '<=', 7 '&&', and 262 sites are MULTI-LINE continuations. An
18// 18-line sample of that same population contained ZERO '==' and would have killed this work; only the
19// full count reversed it. Coarse caveat, stated: those are line-contains counts, so a token inside a
20// tooth NAME inflates them -- this organ re-derives the truth per site by parsing.
21//
22// ONLY the (A == B) as i64 shape is rewritten, because it is the only shape the base class has an
23// emitter for. Every other operator is SKIPPED AND NAMED rather than guessed at: inventing an emitter
24// that does not exist would not compile, and silently dropping a tooth would be far worse than skipping
25// it. The counts printed below form a partition that SUMS to the sites found.
26//
27// license_tier: ORIGINAL
28import "syscalls.nx"
29
30const GM_Q: i64 = 34
31const GM_LP: i64 = 40
32const GM_RP: i64 = 41
33const GM_LB: i64 = 91
34const GM_RB: i64 = 93
35const GM_COMMA: i64 = 44
36const GM_EQ: i64 = 61
37const GM_BSL: i64 = 92
38const GM_SP: i64 = 32
39const GM_TAB: i64 = 9
40const GM_NL: i64 = 10
41const GM_CR: i64 = 13
42const GM_GT: i64 = 62
43const GM_LT: i64 = 60
44const GM_BANG: i64 = 33
45const GM_NEEDLE: i64 = 9
46
47func gm_p(s: *u8) -> i64 {
48 var n: i64 = 0
49 while s[n] != (0 as u8) { n = n + 1 }
50 sys_write(1, s, n)
51 return n
52}
53
54func gm_num(v: i64) -> i64 {
55 let t: *u8 = sys_mmap(32)
56 var m: i64 = v
57 var k: i64 = 0
58 if m == 0 { t[0] = 48 as u8; k = 1 }
59 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
60 var i: i64 = 0
61 while i < k { sys_write(1, (((t as i64) + (k - 1 - i)) as *u8), 1); i = i + 1 }
62 sys_munmap(t, 32)
63 return 0
64}
65
66func gm_isws(c: i64) -> i64 {
67 if c == GM_SP { return 1 }
68 if c == GM_TAB { return 1 }
69 if c == GM_NL { return 1 }
70 if c == GM_CR { return 1 }
71 return 0
72}
73
74// Index of the ')' closing the '(' at `open`, or -1. STRING LITERALS ARE SKIPPED: this dialect permits
75// a literal newline inside a string, so only the closing quote ends one, and a paren or comma inside a
76// tooth NAME would otherwise derail every downstream split.
77func gm_close(buf: *u8, n: i64, open: i64) -> i64 {
78 var i: i64 = open + 1
79 var depth: i64 = 1
80 var instr: i64 = 0
81 while i < n {
82 let c: i64 = buf[i] as i64
83 if instr == 1 {
84 if c == GM_BSL { i = i + 1 } else { if c == GM_Q { instr = 0 } }
85 } else {
86 if c == GM_Q { instr = 1 }
87 else { if c == GM_LP { depth = depth + 1 }
88 else { if c == GM_RP { depth = depth - 1; if depth == 0 { return i } } } }
89 }
90 i = i + 1
91 }
92 return 0 - 1
93}
94
95// Index of the next TOP-LEVEL comma in [start,end), or -1.
96func gm_comma_at(buf: *u8, start: i64, end: i64) -> i64 {
97 var i: i64 = start
98 var depth: i64 = 0
99 var instr: i64 = 0
100 while i < end {
101 let c: i64 = buf[i] as i64
102 if instr == 1 {
103 if c == GM_BSL { i = i + 1 } else { if c == GM_Q { instr = 0 } }
104 } else {
105 if c == GM_Q { instr = 1 }
106 else { if c == GM_LP { depth = depth + 1 }
107 else { if c == GM_RP { depth = depth - 1 }
108 else { if c == GM_LB { depth = depth + 1 }
109 else { if c == GM_RB { depth = depth - 1 }
110 else { if c == GM_COMMA { if depth == 0 { return i } } } } } } }
111 }
112 i = i + 1
113 }
114 return 0 - 1
115}
116
117// Index of a TOP-LEVEL '==' in [start,end), or -1. Rejects >=, <= and ne by inspecting the previous
118// byte, so a relational operator can never be mistaken for equality.
119func gm_eq_at(buf: *u8, start: i64, end: i64) -> i64 {
120 var i: i64 = start
121 var depth: i64 = 0
122 var instr: i64 = 0
123 while i < end - 1 {
124 let c: i64 = buf[i] as i64
125 if instr == 1 {
126 if c == GM_BSL { i = i + 1 } else { if c == GM_Q { instr = 0 } }
127 } else {
128 if c == GM_Q { instr = 1 }
129 else { if c == GM_LP { depth = depth + 1 }
130 else { if c == GM_RP { depth = depth - 1 }
131 else { if c == GM_LB { depth = depth + 1 }
132 else { if c == GM_RB { depth = depth - 1 }
133 else {
134 if depth == 0 { if c == GM_EQ { if (buf[i + 1] as i64) == GM_EQ {
135 let pv: i64 = buf[i - 1] as i64
136 if pv != GM_GT { if pv != GM_LT { if pv != GM_BANG { return i } } }
137 } } }
138 } } } } }
139 }
140 i = i + 1
141 }
142 return 0 - 1
143}
144
145func gm_starts(buf: *u8, at: i64, n: i64, lit: *u8) -> i64 {
146 var i: i64 = 0
147 while lit[i] != (0 as u8) {
148 if at + i >= n { return 0 }
149 if buf[at + i] != lit[i] { return 0 }
150 i = i + 1
151 }
152 return 1
153}
154
155func gm_usage() -> i64 {
156 gm_p("usage: nx_gvmigrate stage <gate-src.nx>\n" as *u8)
157 gm_p(" writes <gate-src.nx>.migrated -- the EDIT SUBSTRATE only. It does NOT judge and does NOT\n" as *u8)
158 gm_p(" install: hand the result to nx_gate_migrate verify <gate> <migrated-src>, which owns the\n" as *u8)
159 gm_p(" 4-clause judge-equivalence oracle and commit-or-restore. This organ never touches the original.\n" as *u8)
160 return 2
161}
162
163func main(argc: i64, argv: *i64) -> i64 {
164 if argc < 3 { return gm_usage() }
165 let verb: *u8 = argv[1] as *u8
166 if gm_starts(verb, 0, 6, "stage" as *u8) == 0 { return gm_usage() }
167 let path: *u8 = argv[2] as *u8
168
169 let lenbox: *i64 = (sys_mmap(8)) as *i64
170 let buf: *u8 = sys_read_file(path, lenbox)
171 let n: i64 = lenbox[0]
172 if n <= 0 {
173 gm_p("nx_gvmigrate: REFUSED unreadable-or-empty source: " as *u8)
174 gm_p(path)
175 gm_p("\n" as *u8)
176 return 3
177 }
178
179 // Growth is bounded: "gv_check" -> "gv_check_eq" adds 3 bytes per site while every rewrite DELETES
180 // the wrapping paren, the " as i64" and the "==" it replaces. 2x input therefore cannot overflow.
181 let out: *u8 = sys_mmap(n * 2 + 4096)
182 var o: i64 = 0
183 var i: i64 = 0
184
185 var sites: i64 = 0
186 var mig: i64 = 0
187 var sk_noteq: i64 = 0
188 var sk_nocast: i64 = 0
189 var sk_arity: i64 = 0
190
191 while i < n {
192 if gm_starts(buf, i, n, "gv_check(" as *u8) == 1 {
193 sites = sites + 1
194 let open: i64 = i + GM_NEEDLE - 1
195 let close: i64 = gm_close(buf, n, open)
196 var handled: i64 = 0
197 if close > 0 {
198 let c1: i64 = gm_comma_at(buf, open + 1, close)
199 var c2: i64 = 0 - 1
200 if c1 > 0 { c2 = gm_comma_at(buf, c1 + 1, close) }
201 if c2 > 0 {
202 let c3: i64 = gm_comma_at(buf, c2 + 1, close)
203 if c3 > 0 {
204 sk_arity = sk_arity + 1
205 handled = 2
206 } else {
207 var a0: i64 = c1 + 1
208 var g1: i64 = 1
209 while g1 == 1 {
210 if a0 < c2 { if gm_isws(buf[a0] as i64) == 1 { a0 = a0 + 1 } else { g1 = 0 } } else { g1 = 0 }
211 }
212 var a1: i64 = c2
213 var g2: i64 = 1
214 while g2 == 1 {
215 if a1 > a0 { if gm_isws(buf[a1 - 1] as i64) == 1 { a1 = a1 - 1 } else { g2 = 0 } } else { g2 = 0 }
216 }
217
218 var ok: i64 = 0
219 var inner0: i64 = 0
220 var inner1: i64 = 0
221 if a1 - a0 > 2 {
222 if (buf[a0] as i64) == GM_LP {
223 let icl: i64 = gm_close(buf, n, a0)
224 if icl > 0 {
225 if icl < a1 {
226 var t: i64 = icl + 1
227 var g3: i64 = 1
228 while g3 == 1 {
229 if t < a1 { if gm_isws(buf[t] as i64) == 1 { t = t + 1 } else { g3 = 0 } } else { g3 = 0 }
230 }
231 if gm_starts(buf, t, n, "as i64" as *u8) == 1 {
232 ok = 1
233 inner0 = a0 + 1
234 inner1 = icl
235 }
236 }
237 }
238 }
239 }
240
241 if ok == 0 {
242 sk_nocast = sk_nocast + 1
243 handled = 2
244 } else {
245 let eqp: i64 = gm_eq_at(buf, inner0, inner1)
246 if eqp < 0 {
247 sk_noteq = sk_noteq + 1
248 handled = 2
249 } else {
250 var k: i64 = 0
251 let lit: *u8 = "gv_check_eq(" as *u8
252 while lit[k] != (0 as u8) { out[o] = lit[k]; o = o + 1; k = k + 1 }
253 var q: i64 = open + 1
254 while q < c1 { out[o] = buf[q]; o = o + 1; q = q + 1 }
255 out[o] = GM_COMMA as u8
256 o = o + 1
257 out[o] = GM_SP as u8
258 o = o + 1
259 var ae: i64 = eqp
260 var g4: i64 = 1
261 while g4 == 1 {
262 if ae > inner0 { if gm_isws(buf[ae - 1] as i64) == 1 { ae = ae - 1 } else { g4 = 0 } } else { g4 = 0 }
263 }
264 q = inner0
265 while q < ae { out[o] = buf[q]; o = o + 1; q = q + 1 }
266 out[o] = GM_COMMA as u8
267 o = o + 1
268 out[o] = GM_SP as u8
269 o = o + 1
270 var bs: i64 = eqp + 2
271 var g5: i64 = 1
272 while g5 == 1 {
273 if bs < inner1 { if gm_isws(buf[bs] as i64) == 1 { bs = bs + 1 } else { g5 = 0 } } else { g5 = 0 }
274 }
275 q = bs
276 while q < inner1 { out[o] = buf[q]; o = o + 1; q = q + 1 }
277 q = c2
278 while q < close { out[o] = buf[q]; o = o + 1; q = q + 1 }
279 out[o] = GM_RP as u8
280 o = o + 1
281 mig = mig + 1
282 i = close + 1
283 handled = 1
284 }
285 }
286 }
287 } else {
288 sk_arity = sk_arity + 1
289 handled = 2
290 }
291 } else {
292 sk_nocast = sk_nocast + 1
293 handled = 2
294 }
295
296 if handled != 1 {
297 // copy verbatim -- a tooth we cannot rewrite is NEVER dropped
298 out[o] = buf[i]
299 o = o + 1
300 i = i + 1
301 }
302 } else {
303 out[o] = buf[i]
304 o = o + 1
305 i = i + 1
306 }
307 }
308
309 let dst: *u8 = sys_mmap(1024)
310 var d: i64 = 0
311 while path[d] != (0 as u8) { dst[d] = path[d]; d = d + 1 }
312 let sfx: *u8 = ".migrated" as *u8
313 var s: i64 = 0
314 while sfx[s] != (0 as u8) { dst[d] = sfx[s]; d = d + 1; s = s + 1 }
315 dst[d] = 0 as u8
316
317 let fd: i64 = sys_openat_wr(dst, 420)
318 if fd < 0 {
319 gm_p("nx_gvmigrate: REFUSED cannot-open-dst " as *u8)
320 gm_p(dst)
321 gm_p("\n" as *u8)
322 return 4
323 }
324 let wr: i64 = sys_write(fd, out, o)
325 sys_close(fd)
326 if wr != o {
327 gm_p("nx_gvmigrate: REFUSED short-write\n" as *u8)
328 return 5
329 }
330
331 gm_p("nx_gvmigrate stage " as *u8)
332 gm_p(path)
333 gm_p("\n wrote " as *u8)
334 gm_p(dst)
335 gm_p(" bytes=" as *u8)
336 gm_num(o)
337 gm_p(" src_bytes=" as *u8)
338 gm_num(n)
339 gm_p("\n sites=" as *u8)
340 gm_num(sites)
341 gm_p(" migrated_eq=" as *u8)
342 gm_num(mig)
343 gm_p(" skip_not_equality=" as *u8)
344 gm_num(sk_noteq)
345 gm_p(" skip_not_cast_shape=" as *u8)
346 gm_num(sk_nocast)
347 gm_p(" skip_arity=" as *u8)
348 gm_num(sk_arity)
349 let sum: i64 = mig + sk_noteq + sk_nocast + sk_arity
350 gm_p("\n partition sums to " as *u8)
351 gm_num(sum)
352 gm_p(" of " as *u8)
353 gm_num(sites)
354 if sum == sites {
355 gm_p(" RECONCILES\n" as *u8)
356 } else {
357 gm_p(" LEAK -- do not trust these counts\n" as *u8)
358 }
359 if mig == 0 {
360 gm_p(" NOTHING REWRITTEN: no (A == B) as i64 tooth here. That is a NAMED absence, not a pass.\n" as *u8)
361 }
362 gm_p(" NEXT: nx_gate_migrate verify <gate> " as *u8)
363 gm_p(dst)
364 gm_p(" -- it judges and commits or restores; this organ did neither.\n" as *u8)
365 if sum != sites { return 6 }
366 return 0
367}