nx_verify_ingest.nx source
↩ module page · 209 lines · 7334 B
1// nx_verify_ingest.nx -- verify the ingested-primitive JSONL artifact.
2//
3// Reads specs/ingested_metamath_1m.jsonl (or any *_ingest_*.jsonl)
4// and reports:
5// - total rows
6// - rows with well-formed `"label":"..."` field
7// - unique labels (via FNV-1a hashing into a fixed-cap bitset)
8// - duplicate-label count (collision detection)
9// - kind distribution
10//
11// Per user directive 2026-05-13: confirm the algorithms came in
12// properly, were deduped, and are well-formed enough for NishiLang
13// to reference.
14
15// nx_safety_envelope:
16// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
17// sil_target: SIL1
18// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
19// verdict: NOT_YET_EVALUATED
20
21import "nx_syscalls.nx"
22import "nx_runtime.nx"
23import "nx_clock.nx"
24import "nx_hash.nx"
25import "nx_tier.nx"
26
27const STDOUT: i64 = 1
28
29// Find " in a line starting at offset; return -1 if not found.
30func find_quote(buf: *u8, start: nx_idx, end: nx_idx) -> nx_idx {
31 var p: nx_idx = start
32 while p < end {
33 if buf[p] == 34 { return p }
34 p = p + 1
35 }
36 return -1
37}
38
39// Find substring `needle` in [start..end), return offset or -1.
40func find_substr(buf: *u8, start: nx_idx, end: nx_idx, needle: *u8) -> nx_idx {
41 let nlen: nx_size = strlen(needle)
42 if nlen == 0 { return start }
43 var p: nx_idx = start
44 while p + nlen <= end {
45 var j: nx_idx = 0
46 var hit: nx_int = 1
47 while j < nlen {
48 if buf[p + j] != needle[j] { hit = 0; j = nlen }
49 j = j + 1
50 }
51 if hit == 1 { return p }
52 p = p + 1
53 }
54 return -1
55}
56
57func main() -> i64 {
58 let path: *u8 = "nxc2/specs/ingested_metamath_1m.jsonl" as *u8
59 let out_len: *i64 = (sys_mmap(8)) as *i64
60 out_len[0] = 0
61 let buf: *u8 = sys_read_file(path, out_len)
62 if (buf as i64) == 0 {
63 let err: *u8 = "error: cannot read ingested artifact\n" as *u8
64 sys_write(STDOUT, err, strlen(err))
65 return 1
66 }
67 let total: nx_size = out_len[0]
68
69 let m1: *u8 = "Verifying ingested-primitive artifact:\n file: " as *u8
70 sys_write(STDOUT, m1, strlen(m1))
71 sys_write(STDOUT, path, strlen(path))
72 let m1b: *u8 = "\n bytes: " as *u8
73 sys_write(STDOUT, m1b, strlen(m1b))
74 print_i64(total)
75 let nl: *u8 = "\n\n" as *u8
76 sys_write(STDOUT, nl, 2)
77
78 // Open-addressing hash table sized 4 million slots (covers 250k
79 // entries at <10% load factor for fast lookup; mmap-on-demand
80 // means we only pay for buckets we actually touch).
81 let t: *NxHash = nx_hash_new(22) // 2^22 = 4M slots. Type was NxHashTable, which is
82 // declared NOWHERE -- nx_hash.nx:86 returns *NxHash.
83
84 let t0: i64 = nx_clock_monotonic_ns()
85 var pos: nx_idx = 0
86 var n_rows: nx_int = 0
87 var n_with_label: nx_int = 0
88 var n_unique: nx_int = 0
89 var n_dup: nx_int = 0
90 var n_kind1: nx_int = 0
91 var n_kind2: nx_int = 0
92 var n_kind3: nx_int = 0
93 var n_other_kind: nx_int = 0
94
95 let label_key: *u8 = "\"label\":\"" as *u8
96 let kind_key: *u8 = "\"kind\":" as *u8
97
98 while pos < total {
99 // Find end of line.
100 var eol: nx_idx = pos
101 var done: nx_int = 0
102 while done == 0 {
103 if eol >= total { done = 1 }
104 if done == 0 {
105 if buf[eol] == 10 { done = 1 }
106 if done == 0 { eol = eol + 1 }
107 }
108 }
109 if eol > pos {
110 n_rows = n_rows + 1
111
112 // Extract label between "label":" and "
113 let label_start: nx_idx = find_substr(buf, pos, eol, label_key)
114 if label_start >= 0 {
115 let label_value_start: nx_idx = label_start + strlen(label_key)
116 let label_end: nx_idx = find_quote(buf, label_value_start, eol)
117 if label_end > label_value_start {
118 n_with_label = n_with_label + 1
119 let lp: *u8 = ((buf as i64) + label_value_start) as *u8
120 let llen: nx_size = label_end - label_value_start
121 let h: i64 = nx_hash_fnv1a_bytes(lp, llen)
122 if nx_hash_has(t, h) == 1 {
123 n_dup = n_dup + 1
124 }
125 if nx_hash_has(t, h) == 0 {
126 nx_hash_put(t, h, 1)
127 n_unique = n_unique + 1
128 }
129 }
130 }
131
132 // Extract kind (single digit after "kind":)
133 let kind_start: nx_idx = find_substr(buf, pos, eol, kind_key)
134 if kind_start >= 0 {
135 let kv: nx_idx = kind_start + strlen(kind_key)
136 if kv < eol {
137 let c: nx_int = buf[kv] as nx_int
138 if c == 49 { n_kind1 = n_kind1 + 1 }
139 if c == 50 { n_kind2 = n_kind2 + 1 }
140 if c == 51 { n_kind3 = n_kind3 + 1 }
141 if c < 49 { n_other_kind = n_other_kind + 1 }
142 if c > 51 { n_other_kind = n_other_kind + 1 }
143 }
144 }
145 }
146 pos = eol + 1
147 }
148 let t1: i64 = nx_clock_monotonic_ns()
149
150 let m2: *u8 = "Verification results:\n total rows: " as *u8
151 sys_write(STDOUT, m2, strlen(m2))
152 print_i64(n_rows)
153 let nl1: *u8 = "\n" as *u8
154 sys_write(STDOUT, nl1, 1)
155 let m3: *u8 = " rows w/ label: " as *u8
156 sys_write(STDOUT, m3, strlen(m3))
157 print_i64(n_with_label)
158 sys_write(STDOUT, nl1, 1)
159 let m4: *u8 = " unique labels: " as *u8
160 sys_write(STDOUT, m4, strlen(m4))
161 print_i64(n_unique)
162 sys_write(STDOUT, nl1, 1)
163 let m5: *u8 = " duplicate labels: " as *u8
164 sys_write(STDOUT, m5, strlen(m5))
165 print_i64(n_dup)
166 sys_write(STDOUT, nl1, 1)
167
168 let m6: *u8 = "\nKind distribution:\n kind 1 (axiom): " as *u8
169 sys_write(STDOUT, m6, strlen(m6))
170 print_i64(n_kind1)
171 sys_write(STDOUT, nl1, 1)
172 let m7: *u8 = " kind 2 ($a): " as *u8
173 sys_write(STDOUT, m7, strlen(m7))
174 print_i64(n_kind2)
175 sys_write(STDOUT, nl1, 1)
176 let m8: *u8 = " kind 3 ($p): " as *u8
177 sys_write(STDOUT, m8, strlen(m8))
178 print_i64(n_kind3)
179 sys_write(STDOUT, nl1, 1)
180 let m9: *u8 = " other: " as *u8
181 sys_write(STDOUT, m9, strlen(m9))
182 print_i64(n_other_kind)
183 sys_write(STDOUT, nl1, 1)
184
185 let m10: *u8 = "\nElapsed ns: " as *u8
186 sys_write(STDOUT, m10, strlen(m10))
187 print_i64(t1 - t0)
188 sys_write(STDOUT, nl1, 1)
189
190 // Verdict
191 if n_rows > 0 {
192 if n_with_label == n_rows {
193 if n_dup == 0 {
194 let v1: *u8 = "\nVERDICT: PASS\n every row well-formed (label present)\n every label unique (FNV-1a collision-free)\n kind field populated\n" as *u8
195 sys_write(STDOUT, v1, strlen(v1))
196 return 0
197 }
198 let v2: *u8 = "\nVERDICT: WARN -- duplicates present\n" as *u8
199 sys_write(STDOUT, v2, strlen(v2))
200 return 2
201 }
202 let v3: *u8 = "\nVERDICT: FAIL -- some rows missing label\n" as *u8
203 sys_write(STDOUT, v3, strlen(v3))
204 return 3
205 }
206 let v4: *u8 = "\nVERDICT: FAIL -- zero rows\n" as *u8
207 sys_write(STDOUT, v4, strlen(v4))
208 return 4
209}