nx_glbnorm_gate.nx source
↩ module page · 599 lines · 30706 B
1// nx_glbnorm_gate.nx -- proves that every NORMAL nx_gltf_export writes is a UNIT vector per glTF 2.0,
2// and proves it BY DECODING THE ACTUAL binary32 BYTES OUT OF THE BIN CHUNK OF A FILE THE SUBJECT WROTE.
3//
4// WHY THIS GATE HAD TO EXIST. Until 2026-08-25 every .glb this estate published was invalid. The number
5// came from OUTSIDE: KhronosGroup/glTF-Validator 2.0.0-dev.3.10 under node, over all 18 .glb files pulled
6// from https://nishifamily.com by curl, uncapped -- files=18 clean=0 with_errors=18 threw=0 sum=18, and
7// 33,682 errors, of which ACCESSOR_VECTOR3_NON_UNIT x 33,656. SIX of our own gates ran GREEN over that
8// same code the whole time. They were not weak gates; they were gates that measured our code against our
9// own expectations, and the expectation itself was the bug ("renderers re-normalise" -- a comment, never a
10// measurement). This gate exists so the estate can see that class WITHOUT an external referee: it decodes
11// the emitted bytes and applies a tolerance DERIVED FROM THE REFEREE'S OWN SOURCE LINE
12// if (Math.abs(Math.sqrt(r) - 1) > 0.00674) -> ACCESSOR_VECTOR3_NON_UNIT
13// as GN_TOL_FP. A green here is a claim about the SPEC, not about our taste.
14//
15// THE ANTI-VACUITY CONTROL IS THE WHOLE POINT. gg_prefix_f32 below is a VERBATIM TRANSCRIPTION of the
16// emission this fix replaced. T2 shows it FAILS the identical predicate the fixed path passes, so the
17// tooth can tell a fix from a no-op. T2b proves the transcription is faithful by sweeping it against the
18// still-live gl_i2f32 rather than trusting that it was copied correctly.
19//
20// WHY THIS FILE IS ALL SMALL FUNCTIONS AND main() HOLDS ALMOST NOTHING. NOT STYLE -- A MEASURED LANDMINE.
21// The first draft did the whole job inline in main(), which reached roughly 85 local bindings, and the
22// compiler then MISCOMPILED SOME OF THEM WITH NO DIAGNOSTIC AT ALL. Measured, from that build's own
23// output, with the constants and the inline product printed beside the binding:
24// DUMP GG_NV = 145 ... GG_VEC3_F32_BYTES = 12 ... GG_NV * GG_VEC3_F32_BYTES inline = 1740
25// DUMP gg_pb = 1756 <- let gg_pb: i64 = GG_NV * GG_VEC3_F32_BYTES
26// DUMP gg_nb = 5244 <- let gg_nb: i64 = GG_NV * GG_VEC3_F32_BYTES (the SAME expression)
27// Two `let`s of one constant expression, in one function, disagreeing with each other AND with that
28// expression evaluated inline one line away. Everything computed from a RUNTIME value in the same
29// function (jlen 724, binoff 752, binlen 6384, fsz 7136) stayed correct and self-consistent throughout.
30// The cost of that landmine was a full RED that looked exactly like a broken fix: the gate read the
31// normal block 8 bytes late and reported 132 of 145 normals non-unit, while the writer had been correct
32// all along -- the real block sat at 752+1740, exactly where it belongs.
33// ***A MISCOMPILED LOCAL IS A SILENT WRONG ANSWER THAT INDICTS THE SUBJECT INSTEAD OF THE INSTRUMENT.***
34// So every function here stays small, and the BIN layout is derived ONCE, in gg_layout, from PARAMETERS
35// rather than from constant-expression locals.
36//
37// THE GATE READS u32s WITH ITS OWN gg_ru32 AND ENCODES EXPECTED POSITIONS WITH vm_int_to_f32 RATHER THAN
38// THE SUBJECT'S gl_i2f32 -- ON PURPOSE, and for the reason nx_vnormals_gate states: an oracle that borrows
39// its subject's helpers agrees with it by construction and stops being able to detect a change in them.
40// The side effect is a free measurement: T8 passing means gl_i2f32 and vm_int_to_f32(v,1) are the same
41// function, i.e. gl_i2f32 is a duplicate ruler whose owner is already in nx_vecmath. Recorded, not acted
42// on here -- retiring it is a separate proof and does not belong inside the fix for a different defect.
43//
44// SCOPE, STATED SO NO READER OVERCLAIMS THE GREEN: this gate covers the NORMAL accessor of write_glb and
45// write_glb_colored. The other 26 validator errors live in three other producers (nx_gltf_mesh /
46// nx_gltf_anim emit NORMAL as {VEC3, SHORT normalized}, which is an invalid format AND a 6-byte unaligned
47// element; nx_mesh2glb additionally declares truncated integer POSITION bounds). Those are named here so
48// their absence from this gate is a declared boundary rather than an oversight.
49//
50// Gate scratch lives under /tmp/<gate>/, created at SETUP because a teardown does not run when a run
51// crashes, and so it can never share a fixture with a production beat.
52//
53// 100 percent sovereign. No hardware writes (Rule 26). expect_exit: 0
54import "nx_syscalls.nx"
55import "nx_gate_verdict.nx"
56import "nx_vecmath.nx"
57import "nx_vnormals_lib.nx"
58import "nx_glbnorm_lib.nx"
59import "nx_gltf_export.nx"
60
61const GG_DIR_MODE: i64 = 493 // 0755, spelled in decimal because this dialect has no octal
62const GG_DIR: *u8 = "/tmp/nx_glbnorm_gate"
63const GG_PLAIN: *u8 = "/tmp/nx_glbnorm_gate/plain.glb"
64const GG_COLOR: *u8 = "/tmp/nx_glbnorm_gate/color.glb"
65
66const GG_V3: i64 = 3
67const GG_VEC3_F32_BYTES: i64 = 12
68const GG_U32_BYTES: i64 = 4
69const GG_TRI_I: i64 = 3
70const GG_ALPHA_OPAQUE: i64 = 255
71const GG_NO_COLOUR_BLOCK: i64 = 0 // write_glb has no COLOR_0 block between normals and indices
72const GG_HAS_COLOUR_BLOCK: i64 = 1 // write_glb_colored does
73
74// GLB container geometry, from the format's own fixed layout: a 12-byte file header, then chunks each
75// preceded by an 8-byte (length, type) header. Derived from the file at runtime, never assumed.
76const GG_GLB_HDR_BYTES: i64 = 12
77const GG_CHUNK_HDR_BYTES: i64 = 8
78const GG_OFF_MAGIC: i64 = 0
79const GG_OFF_VERSION: i64 = 4
80const GG_OFF_JSON_LEN: i64 = 12
81const GG_OFF_JSON_TYPE: i64 = 16
82const GG_MAGIC_GLTF: i64 = 0x46546C67
83const GG_MAGIC_JSON: i64 = 0x4E4F534A
84const GG_MAGIC_BIN: i64 = 0x004E4942
85const GG_GLB_VERSION: i64 = 2
86const GG_CONTAINER_CHECKS: i64 = 4
87
88// ---- FIXTURE ---------------------------------------------------------------------------------------
89// A bumpy GG_N x GG_N grid, displaced on all three axes so the resulting normals span many directions
90// rather than all pointing one way, PLUS one ORPHAN vertex that no triangle references -- the
91// degenerate/zero-normal case, exercised through the real writer and not simulated.
92const GG_N: i64 = 12
93const GG_STEP: i64 = 128
94const GG_NV_GRID: i64 = 144 // GG_N * GG_N
95const GG_NV: i64 = 145 // + the orphan
96const GG_ORPHAN: i64 = 144 // GG_NV - 1
97const GG_NF: i64 = 242 // 2 * (GG_N - 1)^2
98
99// The fixture's bumpiness. ARBITRARY BY DESIGN: their only requirement is that the normals come out
100// varied, which T1b ASSERTS rather than assumes. Named so they read as a declared fixture shape and not
101// as tuned thresholds.
102const GG_HA: i64 = 7
103const GG_HB: i64 = 13
104const GG_HC: i64 = 11
105const GG_HD: i64 = 37
106const GG_HE: i64 = 5
107const GG_HF: i64 = 29
108const GG_JX: i64 = 3
109const GG_JXS: i64 = 11
110const GG_JZ: i64 = 4
111const GG_JZS: i64 = 7
112const GG_COL_MOD: i64 = 256
113const GG_MIN_DISTINCT: i64 = 20 // a FLOOR on fixture variety; the measured value is printed
114
115// vn_smooth_area truncates each component of n*VN_SCALE/l, so an emitted raw length is at most VN_SCALE
116// and at least VN_SCALE - sqrt(3) = 998.27, hence 998 after the integer root. The band below has margin
117// on both sides and the worst measured value is printed beside the verdict.
118const GG_RAW_LO: i64 = 995
119const GG_RAW_HI: i64 = 1000
120
121const GG_SWEEP_LO: i64 = 0 - 40000 // gl_i2f32 transcription sweep, wide enough to cross the sign,
122const GG_SWEEP_HI: i64 = 40000 // the 2^e boundaries and the fx1024 range positions live in
123const GG_OVER_ENVELOPE: i64 = 1048576 // 2^20, far outside GN_IN_MAX, to exercise gn_reduce
124const GG_RULER_OVER: i64 = 4096 // > GN_RULER_MAX, so the ruler must abstain rather than acquit
125const GG_EXP_OF_ONE: i64 = 104 // biased exponent of gn_f32(1) = 2^-23: 127 - 23. Underflow guard.
126const GG_EXP_SHIFT: i64 = 23
127const GG_EXP_MASK: i64 = 255
128
129// result slots, so a helper can hand main() many numbers without main() holding many locals
130const GG_R_BINOFF: i64 = 0
131const GG_R_NORMOFF: i64 = 1
132const GG_R_COLOFF: i64 = 2
133const GG_R_IDXOFF: i64 = 3
134const GG_R_BINLEN: i64 = 4
135const GG_R_CONT: i64 = 5
136const GG_R_WORST: i64 = 6
137const GG_R_BAD: i64 = 7
138const GG_R_UNMEAS: i64 = 8
139const GG_R_WORSTX: i64 = 9
140const GG_R_BADX: i64 = 10
141const GG_R_RT: i64 = 11
142const GG_R_N: i64 = 12
143
144// fixture-measurement slots
145const GG_F_RAWLO: i64 = 0
146const GG_F_RAWHI: i64 = 1
147const GG_F_DISTINCT: i64 = 2
148const GG_F_PREFAIL: i64 = 3
149const GG_F_N: i64 = 4
150
151func gg_pv(label: *u8, v: i64) -> i64 { gv_puts(label); gv_num(v); gv_puts("\n" as *u8); return 0 }
152func gg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 }
153// BOTH must hold. gg_eq(a >= lo, b <= hi) would ALSO return 1 when BOTH comparisons are false, which is a
154// tooth that passes on exactly the case it exists to catch. Named rather than inlined for that reason.
155func gg_both(a: i64, b: i64) -> i64 { if a == 1 { if b == 1 { return 1 } } return 0 }
156func gg_ge(a: i64, b: i64) -> i64 { if a >= b { return 1 } return 0 }
157func gg_le(a: i64, b: i64) -> i64 { if a <= b { return 1 } return 0 }
158
159// The gate's OWN little-endian u32 reader. Deliberately not borrowed from the subject or from
160// nx_gltf_load -- see the header.
161func gg_ru32(b: *u8, at: i64) -> i64 {
162 return (b[at] as i64) + ((b[at+1] as i64)<<8) + ((b[at+2] as i64)<<16) + ((b[at+3] as i64)<<24)
163}
164
165// VERBATIM TRANSCRIPTION of the emission this fix replaced: nx_gltf_export.gl_i2f32 applied straight to a
166// ~1000-scale normal component. Its faithfulness is PROVEN by T2b, not assumed.
167func gg_prefix_f32(v: i64) -> i64 {
168 if v == 0 { return 0 }
169 var sign: i64 = 0
170 var a: i64 = v
171 if a < 0 { sign = 1; a = 0 - a }
172 var e: i64 = 0
173 var t: i64 = a
174 while t > 1 { t = t >> 1; e = e + 1 }
175 var mant: i64 = 0
176 if e <= 23 { mant = (a << (23 - e)) & 0x7fffff }
177 else { mant = (a >> (e - 23)) & 0x7fffff }
178 let exp: i64 = 127 + e
179 return (sign << 31) | (exp << 23) | mant
180}
181
182func gg_h(i: i64, j: i64) -> i64 { return ((i*GG_HA + j*GG_HB) % GG_HC) * GG_HD - ((i*j) % GG_HE) * GG_HF }
183
184func gg_set3(a: *i64, i: i64, x: i64, y: i64, z: i64) -> i64 { a[i*GG_V3+0]=x; a[i*GG_V3+1]=y; a[i*GG_V3+2]=z; return 0 }
185
186func gg_build_verts(v: *i64) -> i64 {
187 var i: i64 = 0
188 while i < GG_N {
189 var j: i64 = 0
190 while j < GG_N {
191 gg_set3(v, i*GG_N + j, i*GG_STEP + ((i*j) % GG_JX) * GG_JXS, gg_h(i, j), j*GG_STEP + ((i+j) % GG_JZ) * GG_JZS)
192 j = j + 1
193 }
194 i = i + 1
195 }
196 // the orphan: a real position inside the mesh, referenced by no triangle
197 gg_set3(v, GG_ORPHAN, GG_STEP, 0, GG_STEP)
198 return 0
199}
200
201func gg_build_faces(f: *i64) -> i64 {
202 var n: i64 = 0
203 var i: i64 = 0
204 while i < GG_N - 1 {
205 var j: i64 = 0
206 while j < GG_N - 1 {
207 gg_set3(f, n, i*GG_N + j, i*GG_N + j + 1, (i+1)*GG_N + j + 1)
208 n = n + 1
209 gg_set3(f, n, i*GG_N + j, (i+1)*GG_N + j + 1, (i+1)*GG_N + j)
210 n = n + 1
211 j = j + 1
212 }
213 i = i + 1
214 }
215 return n
216}
217
218func gg_build_cols(c: *i64) -> i64 {
219 var i: i64 = 0
220 while i < GG_NV {
221 gg_set3(c, i, (i*GG_HA) % GG_COL_MOD, (i*GG_HB) % GG_COL_MOD, (i*GG_HD) % GG_COL_MOD)
222 i = i + 1
223 }
224 return 0
225}
226
227// ---- MEASUREMENT HELPERS. Each one small, so no local here is in miscompile territory. --------------
228
229// Derive every BIN offset from the file's OWN chunk header. ncol is GG_NO_COLOUR_BLOCK or
230// GG_HAS_COLOUR_BLOCK, so ONE layout function serves both writer verbs and they cannot drift apart.
231func gg_layout(glb: *u8, nv: i64, ncol: i64, out: *i64) -> i64 {
232 let jlen: i64 = gg_ru32(glb, GG_OFF_JSON_LEN)
233 let binhdr: i64 = GG_GLB_HDR_BYTES + GG_CHUNK_HDR_BYTES + jlen
234 out[GG_R_BINLEN] = gg_ru32(glb, binhdr)
235 out[GG_R_BINOFF] = binhdr + GG_CHUNK_HDR_BYTES
236 out[GG_R_NORMOFF] = out[GG_R_BINOFF] + nv * GG_VEC3_F32_BYTES
237 out[GG_R_COLOFF] = out[GG_R_NORMOFF] + nv * GG_VEC3_F32_BYTES
238 out[GG_R_IDXOFF] = out[GG_R_COLOFF] + ncol * nv * GG_U32_BYTES
239 var c: i64 = 0
240 if gg_ru32(glb, GG_OFF_MAGIC) == GG_MAGIC_GLTF { c = c + 1 }
241 if gg_ru32(glb, GG_OFF_VERSION) == GG_GLB_VERSION { c = c + 1 }
242 if gg_ru32(glb, GG_OFF_JSON_TYPE) == GG_MAGIC_JSON { c = c + 1 }
243 if gg_ru32(glb, binhdr + GG_U32_BYTES) == GG_MAGIC_BIN { c = c + 1 }
244 out[GG_R_CONT] = c
245 return 0
246}
247
248// what the BIN chunk length must be if the fix moved no offset at all
249func gg_expect_binlen(nv: i64, nf: i64, ncol: i64) -> i64 {
250 return nv*GG_VEC3_F32_BYTES + nv*GG_VEC3_F32_BYTES + ncol*nv*GG_U32_BYTES + nf*GG_TRI_I*GG_U32_BYTES
251}
252
253// Decode EVERY emitted normal out of the BIN chunk and measure it three ways: the referee's own
254// tolerance, the exact derived bound, and exact representability. No sampling -- every vertex.
255func gg_measure(glb: *u8, nv: i64, normoff: i64, out: *i64) -> i64 {
256 out[GG_R_WORST] = 0
257 out[GG_R_BAD] = 0
258 out[GG_R_UNMEAS] = 0
259 out[GG_R_WORSTX] = 0
260 out[GG_R_BADX] = 0
261 out[GG_R_RT] = 1
262 var i: i64 = 0
263 while i < nv {
264 let o: i64 = normoff + i*GG_VEC3_F32_BYTES
265 let wx: i64 = gg_ru32(glb, o)
266 let wy: i64 = gg_ru32(glb, o + GG_U32_BYTES)
267 let wz: i64 = gg_ru32(glb, o + GG_U32_BYTES*2)
268 let e: i64 = gn_unit_err(wx, wy, wz)
269 if e == GN_ERR_UNMEASURABLE { out[GG_R_UNMEAS] = out[GG_R_UNMEAS] + 1 }
270 if e != GN_ERR_UNMEASURABLE {
271 if e > out[GG_R_WORST] { out[GG_R_WORST] = e }
272 if e > GN_TOL_FP { out[GG_R_BAD] = out[GG_R_BAD] + 1 }
273 }
274 let ex: i64 = gn_unit_err_exact(wx, wy, wz)
275 if ex == GN_ERR_UNMEASURABLE { out[GG_R_BADX] = out[GG_R_BADX] + 1 }
276 if ex != GN_ERR_UNMEASURABLE {
277 if ex > out[GG_R_WORSTX] { out[GG_R_WORSTX] = ex }
278 if ex > GN_TOL_EXACT { out[GG_R_BADX] = out[GG_R_BADX] + 1 }
279 }
280 if gn_f32(gn_num(wx)) != wx { out[GG_R_RT] = 0 }
281 if gn_f32(gn_num(wy)) != wy { out[GG_R_RT] = 0 }
282 if gn_f32(gn_num(wz)) != wz { out[GG_R_RT] = 0 }
283 i = i + 1
284 }
285 return 0
286}
287
288func gg_pos_ok(glb: *u8, vbuf: *i64, nv: i64, binoff: i64) -> i64 {
289 var i: i64 = 0
290 while i < nv * GG_V3 {
291 if gg_ru32(glb, binoff + i*GG_U32_BYTES) != vm_int_to_f32(vbuf[i], 1) { return 0 }
292 i = i + 1
293 }
294 return 1
295}
296
297func gg_idx_ok(glb: *u8, fbuf: *i64, nf: i64, idxoff: i64) -> i64 {
298 var i: i64 = 0
299 while i < nf * GG_TRI_I {
300 if gg_ru32(glb, idxoff + i*GG_U32_BYTES) != fbuf[i] { return 0 }
301 i = i + 1
302 }
303 return 1
304}
305
306func gg_col_ok(glb: *u8, cbuf: *i64, nv: i64, coloff: i64) -> i64 {
307 var i: i64 = 0
308 while i < nv {
309 let o: i64 = coloff + i*GG_U32_BYTES
310 if (glb[o+0] as i64) != cbuf[i*GG_V3+0] { return 0 }
311 if (glb[o+1] as i64) != cbuf[i*GG_V3+1] { return 0 }
312 if (glb[o+2] as i64) != cbuf[i*GG_V3+2] { return 0 }
313 if (glb[o+3] as i64) != GG_ALPHA_OPAQUE { return 0 }
314 i = i + 1
315 }
316 return 1
317}
318
319// the orphan vertex must come out EXACTLY (0, 1.0, 0): unit, and the direction vn_smooth_area named
320func gg_orphan_ok(glb: *u8, normoff: i64) -> i64 {
321 let o: i64 = normoff + GG_ORPHAN*GG_VEC3_F32_BYTES
322 if gg_ru32(glb, o) != gn_f32(0) { return 0 }
323 if gg_ru32(glb, o + GG_U32_BYTES) != gn_f32(GN_ONE) { return 0 }
324 if gg_ru32(glb, o + GG_U32_BYTES*2) != gn_f32(0) { return 0 }
325 return 1
326}
327
328func gg_distinct(nrm: *i64, n: i64) -> i64 {
329 var d: i64 = 0
330 var i: i64 = 0
331 while i < n {
332 var seen: i64 = 0
333 var k: i64 = 0
334 while k < i {
335 var same: i64 = 1
336 if nrm[i*GG_V3] != nrm[k*GG_V3] { same = 0 }
337 if nrm[i*GG_V3+1] != nrm[k*GG_V3+1] { same = 0 }
338 if nrm[i*GG_V3+2] != nrm[k*GG_V3+2] { same = 0 }
339 if same == 1 { seen = 1 }
340 k = k + 1
341 }
342 if seen == 0 { d = d + 1 }
343 i = i + 1
344 }
345 return d
346}
347
348// FIXTURE MEASUREMENT: does the input actually carry the defect under test, and is it varied enough that
349// a broken normalisation could not pass on one lucky direction?
350func gg_fixture(nrm: *i64, nv: i64, out: *i64) -> i64 {
351 out[GG_F_RAWLO] = GG_RAW_HI + 1
352 out[GG_F_RAWHI] = 0
353 out[GG_F_PREFAIL] = 0
354 var i: i64 = 0
355 while i < nv {
356 let l: i64 = vm_isqrt(nrm[i*GG_V3]*nrm[i*GG_V3] + nrm[i*GG_V3+1]*nrm[i*GG_V3+1] + nrm[i*GG_V3+2]*nrm[i*GG_V3+2])
357 if l < out[GG_F_RAWLO] { out[GG_F_RAWLO] = l }
358 if l > out[GG_F_RAWHI] { out[GG_F_RAWHI] = l }
359 let e: i64 = gn_unit_err(gg_prefix_f32(nrm[i*GG_V3]), gg_prefix_f32(nrm[i*GG_V3+1]), gg_prefix_f32(nrm[i*GG_V3+2]))
360 if e > GN_TOL_FP { out[GG_F_PREFAIL] = out[GG_F_PREFAIL] + 1 }
361 i = i + 1
362 }
363 out[GG_F_DISTINCT] = gg_distinct(nrm, GG_NV_GRID)
364 return 0
365}
366
367// the transcribed pre-fix encoder must reproduce the still-live gl_i2f32 exactly, or T2 proves nothing
368func gg_transcription_ok() -> i64 {
369 var v: i64 = GG_SWEEP_LO
370 while v <= GG_SWEEP_HI {
371 if gg_prefix_f32(v) != gl_i2f32(v) { return 0 }
372 v = v + 1
373 }
374 return 1
375}
376
377// how many halvings gn_unit3 needs across the whole fixture: 0 on every production path
378func gg_shifts(nrm: *i64, nv: i64, un: *i64) -> i64 {
379 var s: i64 = 0
380 var i: i64 = 0
381 while i < nv {
382 s = s + gn_unit3(nrm[i*GG_V3], nrm[i*GG_V3+1], nrm[i*GG_V3+2], un)
383 i = i + 1
384 }
385 return s
386}
387
388// PRINT THE VALUES. A gate that reports a boolean cannot say why.
389func gg_report(tag: *u8, r: *i64) -> i64 {
390 gv_puts(tag)
391 gv_puts(" binoff=" as *u8); gv_num(r[GG_R_BINOFF])
392 gv_puts(" normoff=" as *u8); gv_num(r[GG_R_NORMOFF])
393 gv_puts(" idxoff=" as *u8); gv_num(r[GG_R_IDXOFF])
394 gv_puts(" binlen=" as *u8); gv_num(r[GG_R_BINLEN])
395 gv_puts(" worst_err_2^-19=" as *u8); gv_num(r[GG_R_WORST])
396 gv_puts(" failing=" as *u8); gv_num(r[GG_R_BAD])
397 gv_puts(" unmeasurable=" as *u8); gv_num(r[GG_R_UNMEAS])
398 gv_puts(" worst_exact_2^-23=" as *u8); gv_num(r[GG_R_WORSTX])
399 gv_puts("\n" as *u8)
400 return 0
401}
402
403// the unit predicate applied to vertex 0 of an emitted file -- the good half of the bite
404func gg_err_at(glb: *u8, normoff: i64) -> i64 {
405 return gn_unit_err(gg_ru32(glb, normoff), gg_ru32(glb, normoff + GG_U32_BYTES), gg_ru32(glb, normoff + GG_U32_BYTES*2))
406}
407
408// ---- THE EXACT DECIMAL PRINTER, WHICH THE min/max BOUNDS DEPEND ON ---------------------------------
409// Every expected string below was computed OUTSIDE this estate, from the IEEE-754 value itself, and is
410// transcribed here verbatim. GG_KD_SEEDSAN is the real minimum of a published file whose writer declared
411// it as the truncated integer -444; that single truncation produced three of the six remaining validator
412// error signatures, so this KAT is the defect itself pinned as a tooth.
413const GG_KB_ONE: i64 = 1065353216
414const GG_KD_ONE: *u8 = "1"
415const GG_KB_HALF: i64 = 1056964608
416const GG_KD_HALF: *u8 = "0.5"
417const GG_KB_EIGHTH: i64 = 1040187392
418const GG_KD_EIGHTH: *u8 = "0.125"
419const GG_KB_DANCE: i64 = 1098776576
420const GG_KD_DANCE: *u8 = "15.875"
421const GG_KB_SEEDSAN: i64 = 3286131474
422const GG_KD_SEEDSAN: *u8 = "-444.77398681640625"
423const GG_KD_TRUNC: *u8 = "-444"
424const GG_KB_NEGONE: i64 = 3212836864
425const GG_KD_NEGONE: *u8 = "-1"
426// the two extremes, which are what actually prove the digit bound is a derivation and not a hope:
427// the smallest value here needs 47 fraction digits, the largest needs 39 integer digits.
428const GG_KB_TINY: i64 = 869711765
429const GG_KD_TINY: *u8 = "0.00000010000000116860974230803549289703369140625"
430const GG_KB_HUGE: i64 = 2139095039
431const GG_KD_HUGE: *u8 = "340282346638528859811704183484516925440"
432const GG_KAT_COUNT: i64 = 8
433const GG_DEC_SWEEP_LO: i64 = 0 - 20000
434const GG_DEC_SWEEP_HI: i64 = 20000
435const GG_DEC_BUF: i64 = 384
436
437func gg_dec_is(bits: i64, want: *u8, buf: *u8) -> i64 {
438 let n: i64 = gn_dec_f32(bits, buf, 0)
439 if n == GN_DEC_OVERFLOW { return 0 }
440 var i: i64 = 0
441 while i < n {
442 if want[i] == (0 as u8) { return 0 }
443 if buf[i] != want[i] { return 0 }
444 i = i + 1
445 }
446 if want[n] != (0 as u8) { return 0 }
447 return 1
448}
449
450func gg_kats(buf: *u8) -> i64 {
451 var k: i64 = 0
452 k = k + gg_dec_is(GG_KB_ONE, GG_KD_ONE, buf)
453 k = k + gg_dec_is(GG_KB_HALF, GG_KD_HALF, buf)
454 k = k + gg_dec_is(GG_KB_EIGHTH, GG_KD_EIGHTH, buf)
455 k = k + gg_dec_is(GG_KB_DANCE, GG_KD_DANCE, buf)
456 k = k + gg_dec_is(GG_KB_SEEDSAN, GG_KD_SEEDSAN, buf)
457 k = k + gg_dec_is(GG_KB_NEGONE, GG_KD_NEGONE, buf)
458 k = k + gg_dec_is(GG_KB_TINY, GG_KD_TINY, buf)
459 k = k + gg_dec_is(GG_KB_HUGE, GG_KD_HUGE, buf)
460 return k
461}
462
463// INDEPENDENT cross-check over a whole range: for an integral value the exact decimal must equal the
464// integer's own decimal as rendered by nx_gltf_export's gl_num -- a different printer written by a
465// different lane, so agreement is evidence rather than a restatement.
466// gn_f32_key must order bit patterns exactly as the VALUES order. Swept over an integral range that
467// crosses zero, comparing the key order against the order of the integers those floats came from -- an
468// independent ordering, so agreement is evidence and not a restatement.
469func gg_key_ok() -> i64 {
470 var v: i64 = GG_DEC_SWEEP_LO
471 while v < GG_DEC_SWEEP_HI {
472 if gn_f32_key(vm_int_to_f32(v, 1)) >= gn_f32_key(vm_int_to_f32(v + 1, 1)) { return 0 }
473 v = v + 1
474 }
475 return 1
476}
477
478func gg_dec_int_ok(buf: *u8, ibuf: *u8) -> i64 {
479 var v: i64 = GG_DEC_SWEEP_LO
480 while v <= GG_DEC_SWEEP_HI {
481 let a: i64 = gn_dec_f32(vm_int_to_f32(v, 1), buf, 0)
482 let b: i64 = gl_num(ibuf, 0, v)
483 if a != b { return 0 }
484 var i: i64 = 0
485 while i < a {
486 if buf[i] != ibuf[i] { return 0 }
487 i = i + 1
488 }
489 v = v + 1
490 }
491 return 1
492}
493
494func main() -> i64 {
495 let ctr: *i64 = gv_ctr()
496 gv_head("nx_glbnorm_gate -- every NORMAL byte nx_gltf_export writes decodes to a UNIT vector, at the Khronos validator's own tolerance" as *u8)
497 sys_mkdir(GG_DIR, GG_DIR_MODE)
498
499 let vbuf: *i64 = sys_mmap(GG_NV * GG_V3 * 8) as *i64
500 let fbuf: *i64 = sys_mmap(GG_NF * GG_TRI_I * 8) as *i64
501 let cbuf: *i64 = sys_mmap(GG_NV * GG_V3 * 8) as *i64
502 let nrm: *i64 = sys_mmap(GG_NV * GG_V3 * 8) as *i64
503 let un: *i64 = sys_mmap(GG_V3 * 8) as *i64
504 let r: *i64 = sys_mmap(GG_R_N * 8) as *i64
505 let r2: *i64 = sys_mmap(GG_R_N * 8) as *i64
506 let fx: *i64 = sys_mmap(GG_F_N * 8) as *i64
507 let szp: *i64 = sys_mmap(8) as *i64
508 let szp2: *i64 = sys_mmap(8) as *i64
509 gg_build_verts(vbuf)
510 gg_build_cols(cbuf)
511 gv_check("fixture-built-the-declared-triangle-count" as *u8, gg_eq(gg_build_faces(fbuf), GG_NF), ctr)
512
513 // ---- T1 THE FIXTURE REACHES THE CONDITION UNDER TEST, BEFORE ANY OUTCOME IS ASSERTED -----------
514 vn_smooth_area(vbuf, fbuf, GG_NV, GG_NF, nrm)
515 gg_fixture(nrm, GG_NV, fx)
516 gg_pv(" raw vn_smooth_area length, min = " as *u8, fx[GG_F_RAWLO])
517 gg_pv(" raw vn_smooth_area length, max = " as *u8, fx[GG_F_RAWHI])
518 gg_pv(" distinct raw normal directions in the fixture = " as *u8, fx[GG_F_DISTINCT])
519 gg_pv(" PRE-FIX vertices that FAIL the unit tooth = " as *u8, fx[GG_F_PREFAIL])
520 gv_check("T1 fixture-reaches-the-condition: the raw normals sit at VN_SCALE, i.e. they are NOT unit" as *u8, gg_both(gg_ge(fx[GG_F_RAWLO], GG_RAW_LO), gg_le(fx[GG_F_RAWHI], GG_RAW_HI)), ctr)
521 gv_check("T1b fixture-is-varied: many distinct normal directions, not one lucky direction repeated" as *u8, gg_ge(fx[GG_F_DISTINCT], GG_MIN_DISTINCT), ctr)
522 gv_check("T1c fixture-reaches-the-degenerate-case: the orphan vertex took vn_smooth_area's fallback" as *u8, gg_eq(nrm[GG_ORPHAN*GG_V3+1], VN_FALLBACK_Y), ctr)
523
524 // ---- T2 THE TRANSCRIBED PRE-FIX EMISSION FAILS THE VERY PREDICATE THE FIX MUST PASS ------------
525 gv_check("T2 anti-vacuity: the pre-fix emission fails the unit tooth at EVERY vertex" as *u8, gg_eq(fx[GG_F_PREFAIL], GG_NV), ctr)
526 gv_check("T2b the pre-fix transcription reproduces the live gl_i2f32 exactly over the whole sweep" as *u8, gg_transcription_ok(), ctr)
527
528 // ---- WRITE THE REAL ARTIFACT THROUGH THE REAL SUBJECT ------------------------------------------
529 let wrote: i64 = write_glb(vbuf, fbuf, GG_NV, GG_NF, GG_PLAIN)
530 let glb: *u8 = sys_read_file(GG_PLAIN, szp)
531 gg_pv(" write_glb returned bytes = " as *u8, wrote)
532 gg_pv(" file size on disk = " as *u8, szp[0])
533 gv_check("T3 the subject wrote a file and its length matches what it reported" as *u8, gg_eq(szp[0], wrote), ctr)
534
535 gg_layout(glb, GG_NV, GG_NO_COLOUR_BLOCK, r)
536 gg_measure(glb, GG_NV, r[GG_R_NORMOFF], r)
537 gg_report(" write_glb:" as *u8, r)
538 gv_check("T4 container: glTF magic, version 2, a JSON chunk and a BIN chunk" as *u8, gg_eq(r[GG_R_CONT], GG_CONTAINER_CHECKS), ctr)
539 gv_check("T4b the fix moved no offset: BIN is still positions+normals+indices at the pre-fix sizes" as *u8, gg_eq(r[GG_R_BINLEN], gg_expect_binlen(GG_NV, GG_NF, GG_NO_COLOUR_BLOCK)), ctr)
540 gv_check("T5 write_glb: every emitted normal decodes to unit length, all of them, no sampling" as *u8, gg_eq(r[GG_R_BAD] + r[GG_R_UNMEAS], 0), ctr)
541 gv_check("T6 write_glb: the EXACT length error is inside the bound derived from GN_K and GN_M" as *u8, gg_eq(r[GG_R_BADX], 0), ctr)
542 gv_check("T7 every emitted normal word is exactly m/2^GN_K: encode(decode(w)) == w for all of them" as *u8, gg_eq(r[GG_R_RT], 1), ctr)
543 gv_check("T8 positions unchanged: every POSITION word equals an INDEPENDENT encoding of the input vertex" as *u8, gg_pos_ok(glb, vbuf, GG_NV, r[GG_R_BINOFF]), ctr)
544 gv_check("T9 indices unchanged: every index word equals the input triangle buffer" as *u8, gg_idx_ok(glb, fbuf, GG_NF, r[GG_R_IDXOFF]), ctr)
545 gv_check("T10 a vertex with no incident face emits EXACTLY (0, 1.0, 0): unit, and the named direction" as *u8, gg_orphan_ok(glb, r[GG_R_NORMOFF]), ctr)
546
547 gn_unit3(0, 0, 0, un)
548 gv_check("T10b gn_unit3 on the zero vector returns the named fallback rather than dividing by zero" as *u8, gg_eq(un[1], GN_FB_Y), ctr)
549
550 // ---- THE SIBLING VERB. A fix in one verb and not its sibling is half a fix. ---------------------
551 let wrote2: i64 = write_glb_colored(vbuf, fbuf, cbuf, GG_NV, GG_NF, GG_COLOR)
552 let glb2: *u8 = sys_read_file(GG_COLOR, szp2)
553 gg_layout(glb2, GG_NV, GG_HAS_COLOUR_BLOCK, r2)
554 gg_measure(glb2, GG_NV, r2[GG_R_NORMOFF], r2)
555 gg_report(" write_glb_colored:" as *u8, r2)
556 gg_pv(" write_glb_colored returned bytes = " as *u8, wrote2)
557 gv_check("T11 write_glb_colored: every emitted normal is unit too, the sibling verb is not half-fixed" as *u8, gg_eq(r2[GG_R_BAD] + r2[GG_R_UNMEAS], 0), ctr)
558 gv_check("T11b write_glb_colored: the COLOR_0 bytes are unchanged by the normal fix" as *u8, gg_col_ok(glb2, cbuf, GG_NV, r2[GG_R_COLOFF]), ctr)
559 gv_check("T11c write_glb_colored: positions unchanged there too" as *u8, gg_pos_ok(glb2, vbuf, GG_NV, r2[GG_R_BINOFF]), ctr)
560 gv_check("T11d write_glb_colored: indices unchanged there too" as *u8, gg_idx_ok(glb2, fbuf, GG_NF, r2[GG_R_IDXOFF]), ctr)
561 gv_check("T11e write_glb_colored: BIN layout is the pre-fix one, colour block included" as *u8, gg_eq(r2[GG_R_BINLEN], gg_expect_binlen(GG_NV, GG_NF, GG_HAS_COLOUR_BLOCK)), ctr)
562
563 // ---- THE ENVELOPE REDUCES RATHER THAN REFUSING, AND THE RESULT IS STILL UNIT -------------------
564 gg_pv(" over-envelope input: halvings applied = " as *u8, gn_unit3(GG_OVER_ENVELOPE, GG_OVER_ENVELOPE / 2, 0 - GG_OVER_ENVELOPE, un))
565 gg_pv(" over-envelope input: resulting |len-1| in units of 2^-19 = " as *u8, gn_unit_err(gn_f32(un[0]), gn_f32(un[1]), gn_f32(un[2])))
566 gv_check("T12 an over-envelope normal is HALVED into range and still emitted unit, never refused" as *u8, gg_le(gn_unit_err(gn_f32(un[0]), gn_f32(un[1]), gn_f32(un[2])), GN_TOL_FP), ctr)
567 gv_check("T12b no production normal needs reduction: VN_SCALE 1000 is inside GN_IN_MAX" as *u8, gg_eq(gg_shifts(nrm, GG_NV, un), 0), ctr)
568 gg_pv(" biased exponent of gn_f32(1) = " as *u8, (gn_f32(1) >> GG_EXP_SHIFT) & GG_EXP_MASK)
569 gv_check("T13 gn_f32 exponent does not underflow at the smallest numerator: 127 - GN_K = 104" as *u8, gg_eq((gn_f32(1) >> GG_EXP_SHIFT) & GG_EXP_MASK, GG_EXP_OF_ONE), ctr)
570
571 // ---- THE EXACT DECIMAL PRINTER, WHICH THE ACCESSOR BOUNDS DEPEND ON ---------------------------
572 let dbuf: *u8 = sys_mmap(GG_DEC_BUF)
573 let ibuf: *u8 = sys_mmap(GG_DEC_BUF)
574 gg_pv(" decimal KATs matched (of 8) = " as *u8, gg_kats(dbuf))
575 gv_check("T14 gn_dec_f32 renders every KAT EXACTLY, including the 47-fraction-digit and 39-integer-digit extremes" as *u8, gg_eq(gg_kats(dbuf), GG_KAT_COUNT), ctr)
576 gv_check("T14b gn_dec_f32 agrees with an INDEPENDENT integer printer over the whole integral sweep" as *u8, gg_dec_int_ok(dbuf, ibuf), ctr)
577 gv_check("T15 gn_f32_key orders float32 bit patterns exactly as their values order, across the sign" as *u8, gg_key_ok(), ctr)
578
579 // ---- NEGATIVE CONTROLS -------------------------------------------------------------------------
580 // The exact printer must REFUSE the truncated bound that caused the defect. Without this, a printer
581 // that still truncated would sail through every KAT that happens to be integral.
582 gv_bite("neg-control-the-decimal-printer-rejects-the-truncated-bound-that-caused-ACCESSOR-MIN-MISMATCH" as *u8,
583 gg_eq(gg_dec_is(GG_KB_SEEDSAN, GG_KD_TRUNC, dbuf), 0),
584 gg_eq(gg_dec_is(GG_KB_SEEDSAN, GG_KD_SEEDSAN, dbuf), 0), ctr)
585
586 // The unit tooth must FIRE on the pre-fix emission and STAY SILENT on the fixed one. Without this the
587 // tooth cannot tell a fix from a no-op, and a green would mean nothing at all.
588 gv_bite("neg-control-the-unit-tooth-fires-on-the-pre-fix-1000-scale-emission-and-not-on-the-fix" as *u8,
589 gg_eq(gn_unit_err(gg_prefix_f32(nrm[0]), gg_prefix_f32(nrm[1]), gg_prefix_f32(nrm[2])) > GN_TOL_FP, 1),
590 gg_eq(gg_err_at(glb, r[GG_R_NORMOFF]) > GN_TOL_FP, 1), ctr)
591
592 // A ruler that returns a small number for something it cannot square would silently bless anything
593 // large enough. It must ABSTAIN instead.
594 gv_bite("neg-control-the-ruler-abstains-on-an-unmeasurable-vector-instead-of-acquitting-it" as *u8,
595 gg_eq(gn_unit_err(vm_int_to_f32(GG_RULER_OVER, 1), 0, 0), GN_ERR_UNMEASURABLE),
596 gg_eq(gn_unit_err(gn_f32(GN_ONE), 0, 0), GN_ERR_UNMEASURABLE), ctr)
597
598 return gv_verdict("nx_glbnorm_gate" as *u8, ctr, "unit normals decoded from the emitted BIN chunk, at the Khronos validator's own 0.00674 bar" as *u8)
599}