nx_srcfmt_gate.nx source
↩ module page · 160 lines · 8609 B
1// nx_srcfmt_gate.nx -- GATE for LN9, the canonical source formatter (lang.plan rung LN9, symbol
2// srcfmt_emit). The done-rule: idempotent over the tokenizer stream, fmt(fmt(x)) == fmt(x); comments
3// and string literals preserved; the formatted corpus builds byte-identical. This gate proves the
4// deterministic half in-process (it IMPORTS nx_srcfmt, so nx_gate_bite mutating nx_srcfmt.nx and
5// rebuilding the gate exercises the real subject) and the build-neutrality half on a hermetic fixture
6// by forking the live compiler; the WHOLE-CORPUS build-neutrality is the lane's sweep (nx_srcfmt runs
7// it over every .nx as a sibling in the tree so imports resolve; a /tmp copy fails expand_imports for
8// a reason unrelated to the formatter -- measured 2026-08-23) and its count is published, not sampled
9// here. The load-bearing non-vacuity tooth is T9: it proves the ORACLE inside the formatter actually
10// distinguishes two different token streams -- the oracle is what makes "a formatter that changes a
11// program is impossible" true, so a vacuous oracle would make every other tooth meaningless.
12// Data captures in /tmp/nxsf/, the one runnable under _build/ (NAS /tmp is noexec).
13// Usage: nx_srcfmt_gate [compiler_elf] (CWD = the tree root, like nx_cc_equiv_gate)
14// license_tier: ORIGINAL No hw writes (Rule 26).
15import "nx_syscalls.nx"
16import "nx_gate_verdict.nx"
17import "nx_srcfmt.nx"
18import "nx_ccgate_lib.nx"
19
20func g_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
21
22// Format an in-memory source; returns length, writes buffer ptr through op. Uses the growing emitter.
23func g_fmt(src: *u8, op: *i64) -> i64 {
24 let n: i64 = g_len(src)
25 let capp: *i64 = sys_mmap(16) as *i64
26 let m: i64 = srcfmt_emit_grow(src, n, op, capp, 0 as *i64)
27 return m
28}
29
30// Does the byte window [0,m) of a contain the NUL-terminated needle?
31func g_has(a: *u8, m: i64, needle: *u8) -> i64 {
32 let nl: i64 = g_len(needle)
33 if nl == 0 { return 0 }
34 var i: i64 = 0
35 while i + nl <= m {
36 var j: i64 = 0
37 var ok: i64 = 1
38 while j < nl { if a[i + j] != needle[j] { ok = 0; j = nl } else { j = j + 1 } }
39 if ok == 1 { return 1 }
40 i = i + 1
41 }
42 return 0
43}
44
45func g_write_file(path: *u8, buf: *u8, n: i64) -> i64 {
46 let fd: i64 = sys_openat_wr(path, CCG_MODE_RW)
47 if fd < 0 { return 0 - 1 }
48 var done: i64 = 0
49 while done < n { let w: i64 = sys_write(fd, ((buf as i64) + done) as *u8, n - done); if w <= 0 { done = n } else { done = done + w } }
50 sys_close(fd)
51 return 0
52}
53
54func g_files_eq(a: *u8, b: *u8) -> i64 {
55 let sa: *i64 = sys_mmap(16) as *i64
56 let sb: *i64 = sys_mmap(16) as *i64
57 let ba: *u8 = sys_read_file(a, sa)
58 let bb: *u8 = sys_read_file(b, sb)
59 if (ba as i64) == 0 { return 0 - 1 }
60 if (bb as i64) == 0 { return 0 - 1 }
61 if sa[0] != sb[0] { return 0 }
62 var i: i64 = 0
63 while i < sa[0] { if ba[i] != bb[i] { return 0 } i = i + 1 }
64 return 1
65}
66
67func main(argc: i64, argv: *i64) -> i64 {
68 var cc: *u8 = "_offc/nx_cc_sovereign.elf\x00"
69 if argc >= 2 { cc = argv[1] as *u8 }
70 ccg_anchor_root()
71 sys_mkdir("/tmp/nxsf\x00" as *u8, CCG_MODE_X)
72 let pid: i64 = ccg_pid()
73 let ctr: *i64 = gv_ctr()
74 gv_head("=== nx_srcfmt_gate -- LN9 canonical formatter: idempotent over the token stream, comments and strings preserved, build byte-identical, and the oracle actually fires ===" as *u8)
75
76 let op: *i64 = sys_mmap(16) as *i64
77 let op2: *i64 = sys_mmap(16) as *i64
78
79 // ---- a messy but valid program (odd spacing, tabs->none, blank runs, split else, ragged struct) ----
80 let messy: *u8 = "// head comment\n\n\nstruct P{\n a:i64,\n bb : i64,\n}\nfunc f(x:i64,y:i64)->i64{\n let z=x+y*2\n if z==0{\n return 0\n }\n else{\n return z\n }\n}\n// tail comment\n\x00"
81
82 let m1: i64 = g_fmt(messy, op)
83 let out1: *u8 = op[0] as *u8
84 gv_check("format-succeeds\x00" as *u8, 1 - (m1 < 0), ctr)
85
86 // T1 idempotent: fmt(fmt(x)) == fmt(x)
87 let m2: i64 = g_fmt(out1, op2)
88 let out2: *u8 = op2[0] as *u8
89 var idem: i64 = 0
90 if m2 == m1 { idem = 1; var i: i64 = 0; while i < m1 { if out1[i] != out2[i] { idem = 0; i = m1 } else { i = i + 1 } } }
91 gv_check("idempotent-fmt-of-fmt-equals-fmt\x00" as *u8, idem, ctr)
92
93 // T3 comments preserved: both the head and tail comment survive
94 var cpres: i64 = 0
95 if g_has(out1, m1, "// head comment\x00" as *u8) == 1 { if g_has(out1, m1, "// tail comment\x00" as *u8) == 1 { cpres = 1 } }
96 gv_check("comments-preserved\x00" as *u8, cpres, ctr)
97
98 // T-struct-align: the struct field type column is aligned -- `a: i64` (a padded to bb's width)
99 gv_check("struct-field-type-column-aligned\x00" as *u8, g_has(out1, m1, " a: i64,\x00" as *u8), ctr)
100 // and the longer field gets exactly one space
101 gv_check("struct-aligned-longest-one-space\x00" as *u8, g_has(out1, m1, " bb: i64,\x00" as *u8), ctr)
102
103 // canonical spacing landed
104 gv_check("else-joined-to-brace\x00" as *u8, g_has(out1, m1, " } else {\x00" as *u8), ctr)
105 gv_check("binary-operator-spaced\x00" as *u8, g_has(out1, m1, "let z = x + y * 2\x00" as *u8), ctr)
106 gv_check("call-and-decl-colon-spacing\x00" as *u8, g_has(out1, m1, "func f(x: i64, y: i64) -> i64 {\x00" as *u8), ctr)
107
108 // T4 neg-control: a mis-indented fixture is NOT already canonical (fmt is not the identity here)
109 let bad: *u8 = "func g()->i64{\n return 1\n}\n\x00"
110 let mb: i64 = g_fmt(bad, op)
111 let outb: *u8 = op[0] as *u8
112 var badn: i64 = g_len(bad)
113 var same_bad: i64 = 0
114 if mb == badn { same_bad = 1; var i2: i64 = 0; while i2 < mb { if outb[i2] != bad[i2] { same_bad = 0; i2 = mb } else { i2 = i2 + 1 } } }
115 gv_check("neg-control-misindent-changes-under-fmt\x00" as *u8, 1 - same_bad, ctr)
116
117 // T5 neg-control: a string literal with odd internal spacing is preserved byte-for-byte
118 let strf: *u8 = "func h()->*u8{\n return \"a b c\\ttab\" as *u8\n}\n\x00"
119 let ms: i64 = g_fmt(strf, op)
120 let outs: *u8 = op[0] as *u8
121 gv_check("neg-control-string-internal-spacing-preserved\x00" as *u8, g_has(outs, ms, "\"a b c\\ttab\"\x00" as *u8), ctr)
122
123 // T9 the ORACLE fires: two DIFFERENT token streams must NOT verify as equal, and identical ones must.
124 // This is the non-vacuity of the whole design: srcfmt_file returns -3 (REFUSED) only because this works.
125 let sa: *u8 = "func k()->i64{ return 1 }\n\x00"
126 let sb: *u8 = "func k()->i64{ return 2 }\n\x00"
127 let van: i64 = srcfmt_verify(sa, g_len(sa), sb, g_len(sb))
128 let vsame: i64 = srcfmt_verify(sa, g_len(sa), sa, g_len(sa))
129 gv_check("oracle-distinguishes-different-token-streams\x00" as *u8, 1 - (van == 0), ctr)
130 gv_check("oracle-accepts-identical-token-streams\x00" as *u8, 1 - (vsame != 0), ctr)
131
132 // T-build: the formatted messy program compiles to BYTE-IDENTICAL asm as the original (hermetic:
133 // the fixture has no imports, so /tmp compiles fine). This is the per-fixture build-neutrality
134 // proof; the WHOLE-CORPUS proof is the lane sweep (sibling-in-tree), whose count is published.
135 let f_orig: *u8 = ccg_path("/tmp/nxsf/orig_\x00" as *u8, pid, ".nx\x00" as *u8)
136 let f_fmt: *u8 = ccg_path("/tmp/nxsf/fmt_\x00" as *u8, pid, ".nx\x00" as *u8)
137 let s_orig: *u8 = ccg_path("/tmp/nxsf/orig_\x00" as *u8, pid, ".s\x00" as *u8)
138 let s_fmt: *u8 = ccg_path("/tmp/nxsf/fmt_\x00" as *u8, pid, ".s\x00" as *u8)
139 // a self-contained program (no imports)
140 let prog: *u8 = "func main(argc:i64,argv:*i64)->i64{\n var s:i64=0\n var i:i64=0\n while i<10{ s=s+i i=i+1 }\n return s\n}\n\x00"
141 let mp: i64 = g_fmt(prog, op)
142 let outp: *u8 = op[0] as *u8
143 g_write_file(f_orig, prog, g_len(prog))
144 g_write_file(f_fmt, outp, mp)
145 let ao: *i64 = sys_mmap(8 * 3) as *i64
146 ao[0] = cc as i64; ao[1] = f_orig as i64; ao[2] = 0
147 let so_fd: i64 = sys_openat_wr(s_orig, CCG_MODE_RW)
148 let bo: i64 = ccg_run(cc, ao, so_fd, 0 - 1)
149 sys_close(so_fd)
150 let af: *i64 = sys_mmap(8 * 3) as *i64
151 af[0] = cc as i64; af[1] = f_fmt as i64; af[2] = 0
152 let sf_fd: i64 = sys_openat_wr(s_fmt, CCG_MODE_RW)
153 let bf: i64 = ccg_run(cc, af, sf_fd, 0 - 1)
154 sys_close(sf_fd)
155 var build_ok: i64 = 0
156 if bo == 0 { if bf == 0 { if g_files_eq(s_orig, s_fmt) == 1 { build_ok = 1 } } }
157 gv_check("formatted-program-compiles-byte-identical-asm\x00" as *u8, build_ok, ctr)
158
159 return gv_verdict("SRCFMT-LN9\x00" as *u8, ctr, "canonical formatter: idempotent, comment/string preserving, build-neutral, oracle-proven\x00" as *u8)
160}