code wiki / (root) / nx_vnormals_gate.nx

nx_vnormals_gate.nx source

↩ module page · 345 lines · 19535 B

1// nx_vnormals_gate.nx -- proves the vertex-normal consolidation, and proves the NON-consolidation. 2// 3// TWO SEPARATE CLAIMS, EACH MEASURED: 4// 5// (1) THE RETIREMENT LOST NOTHING. gl_vnormals (nx_gltf_export) and the block that was INLINE inside 6// write_obj (nx_obj_export) both now call vn_smooth_area (nx_vnormals_lib). This gate carries a 7// VERBATIM TRANSCRIPTION OF EACH ORIGINAL BODY as a reference oracle and asserts the owner reproduces 8// both, word for word over every output word, on every fixture. That is the same differential-probe 9// discipline nx_retire_onto applies before it writes; it is done by hand here because that organ 10// retires a named private FUNCTION onto an owner and the obj copy was not a function at all. 11// 12// (2) THE THIRD COPY IS NOT THE SAME COMPUTATION AND WAS CORRECTLY LEFT ALONE. sc_vertex_normals 13// (nx_shellclose) normalises each face normal BEFORE accumulating it, so faces contribute EQUALLY 14// regardless of area. This gate runs the REAL shipped sc_vertex_normals -- not a paraphrase of it -- 15// on the same geometry and shows the two answers are not even PARALLEL. 16// 17// AND THE TOOTH THAT MAKES (2) MEAN SOMETHING IS T12, NOT T10. "These two functions disagree" is a weak 18// claim: two functions can disagree because one of them is simply broken. T12 runs both on a fixture whose 19// two incident triangles have EQUAL area and shows they then agree exactly in direction. So the divergence 20// in T10 is caused BY THE AREA RATIO and by nothing else, which is the actual mechanism, and it is the 21// reason merging them would have silently changed shipped geometry rather than merely changed code. 22// 23// THE REFERENCE ORACLES BELOW CONTAIN BARE 3s AND 1000s ON PURPOSE. They are transcriptions of code that 24// has been deleted, and their whole value is being INDEPENDENT of the owner. Rewriting them in terms of 25// the owner's VN_V3 and VN_SCALE would make them agree with it by construction and they would stop being 26// able to detect a change in those constants -- an oracle that imports its subject's constants is not an 27// oracle. Named here so the next reader sees a decision rather than an oversight. 28// 29// 100 percent sovereign. No hardware writes (Rule 26). expect_exit: 0 30import "nx_syscalls.nx" 31import "nx_gate_verdict.nx" 32import "nx_vecmath.nx" 33import "nx_vnormals_lib.nx" 34import "nx_gltf_export.nx" 35import "nx_obj_export.nx" 36import "nx_shellclose.nx" 37 38// Gate scratch lives under /tmp/<gate>/ so it can never share a fixture with a production beat, and it is 39// created at SETUP because a teardown does not run when a run crashes. 40const VNG_DIR_MODE: i64 = 493 // 0755, spelled in decimal because this dialect has no octal 41const VNG_V3: i64 = 3 42 43// FIXTURE A -- two triangles meeting at vertex 0 whose cross-product magnitudes are 1000000 and 10000, 44// a 100:1 area ratio, plus vertex 5 which NO triangle uses (the degenerate-vertex case). 45const VNG_A_NV: i64 = 6 46const VNG_A_NF: i64 = 2 47// Hand-derived expectation for vertex 0 under AREA weighting, so the KAT cannot drift with the code: 48// face 0 cross = (0, 0, 1000000); face 1 cross = (0, 10000, 0); sum = (0, 10000, 1000000) 49// len = isqrt(10000^2 + 1000000^2) = isqrt(1000100000000) = 1000049 50// out = (0, 10000*1000/1000049, 1000000*1000/1000049) = (0, 9, 999) 51const VNG_A_KAT_X: i64 = 0 52const VNG_A_KAT_Y: i64 = 9 53const VNG_A_KAT_Z: i64 = 999 54 55// FIXTURE B -- the SAME shape of construction with the two cross-product magnitudes made EQUAL (1000000 56// each), which is the only difference between it and fixture A. 57const VNG_B_NV: i64 = 5 58const VNG_B_NF: i64 = 2 59 60func vng_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 61func vng_ne(a: i64, b: i64) -> i64 { if a != b { return 1 } return 0 } 62func vng_pv(label: *u8, v: i64) -> i64 { gv_puts(label); gv_num(v); gv_puts("\n" as *u8); return 0 } 63 64func vng_p3(label: *u8, a: *i64, vi: i64) -> i64 { 65 gv_puts(label); gv_num(a[vi*VNG_V3+0]); gv_puts(" " as *u8); gv_num(a[vi*VNG_V3+1]); gv_puts(" " as *u8); gv_num(a[vi*VNG_V3+2]); gv_puts("\n" as *u8) 66 return 0 67} 68 69// every word equal, over the whole output -- not a spot check 70func vng_same(a: *i64, b: *i64, n: i64) -> i64 { 71 var i: i64 = 0 72 var ok: i64 = 1 73 while i < n { if a[i] != b[i] { ok = 0 } i = i + 1 } 74 return ok 75} 76 77// SCALE-FREE non-parallelism test on the (y,z) projection. The two computations emit at DIFFERENT scales 78// (1000 versus SC_Q = 256), so comparing components directly would confuse a scale difference with a 79// direction difference. A cross product is zero exactly when the two vectors are parallel, whatever their 80// lengths, so this asks the only question that matters: do they point the same way. 81func vng_cross_yz(a: *i64, b: *i64, vi: i64) -> i64 { 82 return a[vi*VNG_V3+1]*b[vi*VNG_V3+2] - a[vi*VNG_V3+2]*b[vi*VNG_V3+1] 83} 84 85func vng_find(hay: *u8, hlen: i64, needle: *u8) -> i64 { 86 var nlen: i64 = 0 87 while needle[nlen] != (0 as u8) { nlen = nlen + 1 } 88 if nlen <= 0 { return 0 - 1 } 89 var i: i64 = 0 90 while i + nlen <= hlen { 91 var j: i64 = 0 92 var ok: i64 = 1 93 while j < nlen { 94 if hay[i+j] != needle[j] { ok = 0 } 95 j = j + 1 96 } 97 if ok == 1 { return i } 98 i = i + 1 99 } 100 return 0 - 1 101} 102 103func vng_m3_build(base: i64, verts: *i64, nv: i64, tris: *i64, nf: i64) -> i64 { 104 m3_init(base) 105 var i: i64 = 0 106 while i < nv { m3_add_vert(base, verts[i*VNG_V3+0], verts[i*VNG_V3+1], verts[i*VNG_V3+2]); i = i + 1 } 107 var t: i64 = 0 108 while t < nf { m3_add_tri(base, tris[t*VNG_V3+0], tris[t*VNG_V3+1], tris[t*VNG_V3+2]); t = t + 1 } 109 return 0 110} 111 112// ---- REFERENCE ORACLE 1: the former body of nx_gltf_export.gl_vnormals, transcribed verbatim ---- 113func vnref_gl_original(vbuf: *i64, fbuf: *i64, nv: i64, nf: i64, nrm: *i64) -> i64 { 114 var i: i64 = 0 115 while i < nv * 3 { nrm[i] = 0; i = i + 1 } 116 var t: i64 = 0 117 while t < nf { 118 let a: i64 = fbuf[t*3]; let b: i64 = fbuf[t*3+1]; let c: i64 = fbuf[t*3+2] 119 let e1x: i64 = vbuf[b*3]-vbuf[a*3]; let e1y: i64 = vbuf[b*3+1]-vbuf[a*3+1]; let e1z: i64 = vbuf[b*3+2]-vbuf[a*3+2] 120 let e2x: i64 = vbuf[c*3]-vbuf[a*3]; let e2y: i64 = vbuf[c*3+1]-vbuf[a*3+1]; let e2z: i64 = vbuf[c*3+2]-vbuf[a*3+2] 121 let fnx: i64 = e1y*e2z - e1z*e2y; let fny: i64 = e1z*e2x - e1x*e2z; let fnz: i64 = e1x*e2y - e1y*e2x 122 nrm[a*3]=nrm[a*3]+fnx; nrm[a*3+1]=nrm[a*3+1]+fny; nrm[a*3+2]=nrm[a*3+2]+fnz 123 nrm[b*3]=nrm[b*3]+fnx; nrm[b*3+1]=nrm[b*3+1]+fny; nrm[b*3+2]=nrm[b*3+2]+fnz 124 nrm[c*3]=nrm[c*3]+fnx; nrm[c*3+1]=nrm[c*3+1]+fny; nrm[c*3+2]=nrm[c*3+2]+fnz 125 t = t + 1 126 } 127 i = 0 128 while i < nv { 129 let l: i64 = vm_isqrt(nrm[i*3]*nrm[i*3] + nrm[i*3+1]*nrm[i*3+1] + nrm[i*3+2]*nrm[i*3+2]) 130 if l < 1 { nrm[i*3]=0; nrm[i*3+1]=1000; nrm[i*3+2]=0 } 131 else { nrm[i*3]=nrm[i*3]*1000/l; nrm[i*3+1]=nrm[i*3+1]*1000/l; nrm[i*3+2]=nrm[i*3+2]*1000/l } 132 i = i + 1 133 } 134 return 0 135} 136 137// ---- REFERENCE ORACLE 2: the block formerly INLINE in nx_obj_export.write_obj, transcribed verbatim. 138// It hoisted ax/ay/az where oracle 1 re-indexed; that is the ONLY textual difference between the two 139// originals, and transcribing both independently is how this gate proves they were the same computation 140// rather than assuming it. ---- 141func vnref_obj_original(vbuf: *i64, fbuf: *i64, nv: i64, nf: i64, nrm: *i64) -> i64 { 142 var z: i64 = 0 143 while z < nv * 3 { nrm[z] = 0; z = z + 1 } 144 var t: i64 = 0 145 while t < nf { 146 let a: i64 = fbuf[t*3]; let b: i64 = fbuf[t*3+1]; let c: i64 = fbuf[t*3+2] 147 let ax: i64 = vbuf[a*3]; let ay: i64 = vbuf[a*3+1]; let az: i64 = vbuf[a*3+2] 148 let e1x: i64 = vbuf[b*3]-ax; let e1y: i64 = vbuf[b*3+1]-ay; let e1z: i64 = vbuf[b*3+2]-az 149 let e2x: i64 = vbuf[c*3]-ax; let e2y: i64 = vbuf[c*3+1]-ay; let e2z: i64 = vbuf[c*3+2]-az 150 let fnx: i64 = e1y*e2z - e1z*e2y 151 let fny: i64 = e1z*e2x - e1x*e2z 152 let fnz: i64 = e1x*e2y - e1y*e2x 153 nrm[a*3]=nrm[a*3]+fnx; nrm[a*3+1]=nrm[a*3+1]+fny; nrm[a*3+2]=nrm[a*3+2]+fnz 154 nrm[b*3]=nrm[b*3]+fnx; nrm[b*3+1]=nrm[b*3+1]+fny; nrm[b*3+2]=nrm[b*3+2]+fnz 155 nrm[c*3]=nrm[c*3]+fnx; nrm[c*3+1]=nrm[c*3+1]+fny; nrm[c*3+2]=nrm[c*3+2]+fnz 156 t = t + 1 157 } 158 var i: i64 = 0 159 while i < nv { 160 var qx: i64 = nrm[i*3]; var qy: i64 = nrm[i*3+1]; var qz: i64 = nrm[i*3+2] 161 let l: i64 = vm_isqrt(qx*qx + qy*qy + qz*qz) 162 if l < 1 { qx = 0; qy = 1000; qz = 0 } else { qx = qx*1000/l; qy = qy*1000/l; qz = qz*1000/l } 163 nrm[i*3] = qx; nrm[i*3+1] = qy; nrm[i*3+2] = qz 164 i = i + 1 165 } 166 return 0 167} 168 169func vng_streq(a: *u8, b: *u8) -> i64 { 170 var i: i64 = 0 171 while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 } 172 if b[i] != (0 as u8) { return 0 } 173 return 1 174} 175 176func vng_set3(a: *i64, i: i64, x: i64, y: i64, z: i64) -> i64 { a[i*3+0]=x; a[i*3+1]=y; a[i*3+2]=z; return 0 } 177 178func main() -> i64 { 179 let ctr: *i64 = gv_ctr() 180 gv_head("nx_vnormals_gate -- one owner for area-weighted vertex normals, and the copy that is NOT the same computation" as *u8) 181 182 sys_mkdir("/tmp/nx_vnormals_gate" as *u8, VNG_DIR_MODE) 183 184 // ---------------- FIXTURE A: 100:1 area ratio, plus an orphan vertex ---------------- 185 let av: *i64 = sys_mmap(VNG_A_NV * VNG_V3 * 8) as *i64 186 let af: *i64 = sys_mmap(VNG_A_NF * VNG_V3 * 8) as *i64 187 vng_set3(av, 0, 0, 0, 0) 188 vng_set3(av, 1, 1000, 0, 0) 189 vng_set3(av, 2, 0, 1000, 0) 190 vng_set3(av, 3, 0, 0, 100) 191 vng_set3(av, 4, 100, 0, 0) 192 vng_set3(av, 5, 0, 0, 0) 193 vng_set3(af, 0, 0, 1, 2) 194 vng_set3(af, 1, 0, 3, 4) 195 196 // FIXTURE-REACHED: the two faces really do differ in area by 100:1. Asserted arithmetically from the 197 // fixture itself, before any outcome is asserted, so a fixture edit cannot silently make T10 vacuous. 198 let big: i64 = 1000*1000 - 0*0 199 let small: i64 = 100*100 - 0*0 200 vng_pv("A face0 cross magnitude = " as *u8, big); vng_pv("A face1 cross magnitude = " as *u8, small) 201 gv_check("T1 FIXTURE REACHED: the two faces at vertex 0 differ in area by exactly 100:1" as *u8, 202 vng_eq(big, 1000000)*vng_eq(small, 10000)*vng_eq(big, small*100), ctr) 203 204 let n_own: *i64 = sys_mmap(VNG_A_NV * VNG_V3 * 8) as *i64 205 let n_gl: *i64 = sys_mmap(VNG_A_NV * VNG_V3 * 8) as *i64 206 let n_obj: *i64 = sys_mmap(VNG_A_NV * VNG_V3 * 8) as *i64 207 let n_shp: *i64 = sys_mmap(VNG_A_NV * VNG_V3 * 8) as *i64 208 209 let rc_own: i64 = vn_smooth_area(av, af, VNG_A_NV, VNG_A_NF, n_own) 210 vnref_gl_original(av, af, VNG_A_NV, VNG_A_NF, n_gl) 211 vnref_obj_original(av, af, VNG_A_NV, VNG_A_NF, n_obj) 212 gl_vnormals(av, af, VNG_A_NV, VNG_A_NF, n_shp) 213 214 vng_p3("A owner v0 = " as *u8, n_own, 0) 215 vng_p3("A gl-orig v0 = " as *u8, n_gl, 0) 216 vng_p3("A obj-orig v0 = " as *u8, n_obj, 0) 217 vng_p3("A shipped-gl_vnormals v0 = " as *u8, n_shp, 0) 218 219 gv_check("T2 the owner reproduces the RETIRED gl_vnormals body EXACTLY, every output word" as *u8, 220 vng_eq(rc_own, VN_OK)*vng_same(n_own, n_gl, VNG_A_NV * VNG_V3), ctr) 221 gv_check("T3 the owner reproduces the RETIRED write_obj inline block EXACTLY, every output word" as *u8, 222 vng_same(n_own, n_obj, VNG_A_NV * VNG_V3), ctr) 223 gv_check("T4 the two retired copies were the SAME computation as each other, transcribed independently" as *u8, 224 vng_same(n_gl, n_obj, VNG_A_NV * VNG_V3), ctr) 225 gv_check("T5 the SHIPPED gl_vnormals now returns the owner's answer -- the delegation is WIRED, not merely written" as *u8, 226 vng_same(n_shp, n_own, VNG_A_NV * VNG_V3), ctr) 227 gv_check("T6 KAT: vertex 0 is exactly (0, 9, 999), hand-derived in this file from the fixture" as *u8, 228 vng_eq(n_own[0], VNG_A_KAT_X)*vng_eq(n_own[1], VNG_A_KAT_Y)*vng_eq(n_own[2], VNG_A_KAT_Z), ctr) 229 230 vng_p3("A owner orphan v5 = " as *u8, n_own, 5) 231 gv_check("T7 a vertex NO face touches gets the named +Y fallback, not a zero vector" as *u8, 232 vng_eq(n_own[5*3+0], VN_FALLBACK_X)*vng_eq(n_own[5*3+1], VN_FALLBACK_Y)*vng_eq(n_own[5*3+2], VN_FALLBACK_Z), ctr) 233 234 // ---------------- write_obj END-TO-END: prove the inline block was really replaced by the call ------- 235 // Arithmetic equivalence alone cannot prove the patch APPLIED -- the old code was self-contained, so a 236 // file where the edit never landed still compiles and still emits correct normals. This tooth reads the 237 // bytes write_obj actually wrote. 238 let ob: i64 = write_obj(av, af, VNG_A_NV, VNG_A_NF, "/tmp/nx_vnormals_gate/t.obj" as *u8) 239 let flen: *i64 = sys_mmap(8) as *i64 240 flen[0] = 0 241 let fbytes: *u8 = sys_read_file("/tmp/nx_vnormals_gate/t.obj" as *u8, flen) 242 var have_file: i64 = 0 243 if ob > 0 { if flen[0] > 0 { have_file = 1 } } 244 var saw_vn: i64 = 0 245 if have_file == 1 { if vng_find(fbytes, flen[0], "vn " as *u8) >= 0 { saw_vn = 1 } } 246 vng_pv("E write_obj returned = " as *u8, ob); vng_pv("E file bytes = " as *u8, flen[0]); vng_pv("E file has a vn line = " as *u8, saw_vn) 247 gv_check("T8 FIXTURE REACHED: write_obj wrote a non-empty file and it contains at least one vn line" as *u8, 248 have_file*saw_vn, ctr) 249 250 // Build the expected line with write_obj's OWN formatter, so the comparison cannot drift from the wire 251 // format, and search the emitted bytes for it. 252 let exp: *u8 = sys_mmap(64) 253 var eo: i64 = oe_cat(exp, 0, "vn " as *u8) 254 eo = oe_num(exp, eo, n_own[0]); exp[eo]=32 as u8; eo=eo+1 255 eo = oe_num(exp, eo, n_own[1]); exp[eo]=32 as u8; eo=eo+1 256 eo = oe_num(exp, eo, n_own[2]); exp[eo]=10 as u8; eo=eo+1 257 exp[eo] = 0 as u8 258 var found: i64 = 0 - 1 259 if have_file == 1 { found = vng_find(fbytes, flen[0], exp) } 260 gv_puts("E expected line = " as *u8); gv_puts(exp); vng_pv("E found at offset = " as *u8, found) 261 gv_check("T9 END TO END: the vn line write_obj emitted for vertex 0 is exactly the owner's answer" as *u8, 262 vng_eq(have_file,1)*vng_ne(found, 0 - 1), ctr) 263 264 // ---------------- THE NON-MERGE FINDING, measured against the REAL sc_vertex_normals ---------------- 265 let ma: i64 = sys_mmap(m3_bytes()) as i64 266 vng_m3_build(ma, av, VNG_A_NV, af, VNG_A_NF) 267 sc_vertex_normals(ma, n_shp) 268 vng_p3("A sc_vertex_normals v0 = " as *u8, n_shp, 0) 269 let cross_a: i64 = vng_cross_yz(n_own, n_shp, 0) 270 vng_pv("A owner-vs-sc (y,z) cross = " as *u8, cross_a) 271 gv_check("T10 sc_vertex_normals is NOT the same computation: on a 100:1 area ratio its answer is not even PARALLEL to the area-weighted one" as *u8, 272 vng_ne(cross_a, 0), ctr) 273 274 vng_pv("A sc v0 y = " as *u8, n_shp[1]); vng_pv("A sc v0 z = " as *u8, n_shp[2]) 275 vng_pv("A owner v0 y = " as *u8, n_own[1]); vng_pv("A owner v0 z = " as *u8, n_own[2]) 276 gv_check("T11 THE MECHANISM: sc weights the two faces EQUALLY so its y equals its z, while area weighting tilts toward the larger face so its y does not" as *u8, 277 vng_eq(n_shp[1], n_shp[2])*vng_ne(n_own[1], n_own[2]), ctr) 278 279 vng_p3("A sc orphan v5 = " as *u8, n_shp, 5) 280 gv_check("T12 and they disagree about an untouched vertex too: sc leaves the ZERO vector where the owner returns the +Y fallback" as *u8, 281 vng_eq(n_shp[5*3+0],0)*vng_eq(n_shp[5*3+1],0)*vng_eq(n_shp[5*3+2],0), ctr) 282 283 // ---------------- FIXTURE B: the SAME construction with EQUAL areas. This is what makes T10 mean 284 // something: with the area ratio removed the two computations agree in direction exactly, so the 285 // divergence above is caused by the WEIGHTING and not by one of them being broken. ---------------- 286 let bv: *i64 = sys_mmap(VNG_B_NV * VNG_V3 * 8) as *i64 287 let bf: *i64 = sys_mmap(VNG_B_NF * VNG_V3 * 8) as *i64 288 vng_set3(bv, 0, 0, 0, 0) 289 vng_set3(bv, 1, 1000, 0, 0) 290 vng_set3(bv, 2, 0, 1000, 0) 291 vng_set3(bv, 3, 0, 0, 1000) 292 vng_set3(bv, 4, 1000, 0, 0) 293 vng_set3(bf, 0, 0, 1, 2) 294 vng_set3(bf, 1, 0, 3, 4) 295 let bbig: i64 = 1000*1000 296 let bsmall: i64 = 1000*1000 297 gv_check("T13 FIXTURE REACHED: fixture B differs from fixture A in exactly one respect -- its two faces have EQUAL area" as *u8, 298 vng_eq(bbig, bsmall)*vng_eq(bbig, 1000000), ctr) 299 300 let nb_own: *i64 = sys_mmap(VNG_B_NV * VNG_V3 * 8) as *i64 301 let nb_sc: *i64 = sys_mmap(VNG_B_NV * VNG_V3 * 8) as *i64 302 vn_smooth_area(bv, bf, VNG_B_NV, VNG_B_NF, nb_own) 303 let mb: i64 = sys_mmap(m3_bytes()) as i64 304 vng_m3_build(mb, bv, VNG_B_NV, bf, VNG_B_NF) 305 sc_vertex_normals(mb, nb_sc) 306 vng_p3("B owner v0 = " as *u8, nb_own, 0) 307 vng_p3("B sc v0 = " as *u8, nb_sc, 0) 308 let cross_b: i64 = vng_cross_yz(nb_own, nb_sc, 0) 309 vng_pv("B owner-vs-sc (y,z) cross = " as *u8, cross_b) 310 gv_check("T14 THE CONTROL THAT MAKES T10 MEAN SOMETHING: with the area ratio removed the SAME two functions become exactly PARALLEL, so the weighting is the whole cause" as *u8, 311 vng_eq(cross_b, 0)*vng_ne(nb_own[1], 0)*vng_ne(nb_sc[1], 0), ctr) 312 313 // ---------------- negative controls ---------------- 314 let scratch: *i64 = sys_mmap(VNG_A_NV * VNG_V3 * 8) as *i64 315 let bad_nv: i64 = vn_smooth_area(av, af, 0, VNG_A_NF, scratch) 316 let good_nv: i64 = vn_smooth_area(av, af, VNG_A_NV, VNG_A_NF, scratch) 317 vng_pv("N nv=0 rc = " as *u8, bad_nv); vng_pv("N nv=6 rc = " as *u8, good_nv) 318 gv_bite("neg-control-a-non-positive-vertex-count-REFUSES-instead-of-looping-on-a-nonsense-bound" as *u8, 319 vng_eq(bad_nv, VN_E_ARGS), vng_ne(good_nv, VN_OK), ctr) 320 321 let bad_nf: i64 = vn_smooth_area(av, af, VNG_A_NV, 0 - 1, scratch) 322 let good_nf: i64 = vn_smooth_area(av, af, VNG_A_NV, 0, scratch) 323 let zero_face_ok: i64 = vng_eq(scratch[0], VN_FALLBACK_X)*vng_eq(scratch[1], VN_FALLBACK_Y)*vng_eq(scratch[2], VN_FALLBACK_Z) 324 vng_pv("N nf=-1 rc = " as *u8, bad_nf); vng_pv("N nf=0 rc = " as *u8, good_nf); vng_pv("N nf=0 gave the fallback = " as *u8, zero_face_ok) 325 gv_bite("neg-control-a-negative-face-count-REFUSES-while-zero-faces-is-ADMITTED-a-point-cloud-is-legal" as *u8, 326 vng_eq(bad_nf, VN_E_ARGS), vng_ne(good_nf, VN_OK), ctr) 327 gv_check("T15 POSITIVE CONTROL: zero faces is not an error -- every vertex correctly comes back as the named fallback" as *u8, 328 vng_eq(good_nf, VN_OK)*zero_face_ok, ctr) 329 330 // ---- T16: the refusal-naming contract. This tooth exists because nx_gate_bite reported vn_code_name's 331 // two comparisons as NOT-REACHED -- the mutants produced a BYTE-IDENTICAL artifact, which is the 332 // compiler telling you the function is dead code because nothing calls it. A refusal-name table that 333 // nothing exercises is a contract nobody checks, so it gets a tooth rather than a deletion. 334 let nm_ok: i64 = vng_streq(vn_code_name(VN_OK), "OK" as *u8) 335 let nm_args: i64 = vng_streq(vn_code_name(VN_E_ARGS), "REFUSED-BAD-ARGUMENTS" as *u8) 336 let nm_unk: i64 = vng_streq(vn_code_name(0 - 999), "REFUSED-UNCLASSIFIED" as *u8) 337 gv_puts("N name(VN_OK) = " as *u8); gv_puts(vn_code_name(VN_OK)); gv_puts("\n" as *u8) 338 gv_puts("N name(VN_E_ARGS) = " as *u8); gv_puts(vn_code_name(VN_E_ARGS)); gv_puts("\n" as *u8) 339 gv_puts("N name(unknown) = " as *u8); gv_puts(vn_code_name(0 - 999)); gv_puts("\n" as *u8) 340 gv_check("T16 EVERY REFUSAL IS NAMED: each code maps to its own token, and an UNKNOWN code is not laundered into a known one" as *u8, 341 nm_ok*nm_args*nm_unk, ctr) 342 343 return gv_verdict("nx_vnormals_gate" as *u8, ctr, 344 "one owner for area-weighted vertex normals, proven against both retired originals and separated from the uniform-weighted one" as *u8) 345}