nx_craft_tile_gate.nx source

1// nx_craft_tile_gate.nx -- GE30 REFEREE: the frame cut into row bands is BIT-IDENTICAL to the frame 2// drawn by one thread, and a band writes NOTHING outside the rows it owns. 3// 4// WHY THIS SUBJECT NEEDS ITS OWN GATE. nx_wasm_craft_gate proves the WORLD (raycast ground truth, 5// causal edits, determinism, the input edge contract) and nx_wasm_craft_vm_gate proves the SHIPPED 6// WASM fits and paints inside the memory it declares. Neither can see the defect GE30 introduces: 7// a frame assembled by N workers over ONE shared linear memory is correct only if the band pass 8// writes disjoint pixels and reads no scratch its neighbour writes. The old renderer failed the 9// second half by construction -- five wray outputs lived in ONE shared slot (O_ST 46-50), which is 10// invisible with one thread and a race with two -- so the decomposition is the subject here. 11// 12// THE LOAD-BEARING TOOTH IS A FULL PIXEL COMPARE, NOT A DIGEST. Two fresh arenas, same seed, same 13// camera: arena A drawn by render_impl (one thread, the shipped path), arena B drawn as N bands plus 14// one overlay. Every word of the WRITTEN EXTENT must agree -- rw x rh, the compact buffer the 15// one-pixel-per-ray law made the single owner of, never W*H, because a comparison over unwritten 16// memory is a claim about uninitialised bytes. A tiling defect lives at BAND SEAMS, so the band 17// counts include ones that do NOT divide the row count evenly, and a stride-sampling checksum is 18// deliberately not used anywhere in this file. 19// 20// ANTI-VACUITY, STATED BECAUSE "IDENTICAL" IS THE EASIEST GREEN TO FAKE: two blank frames are also 21// identical. So the gate first proves the frame is VARIED (many distinct colours) and that the 22// overlay pass genuinely CHANGES pixels; only then does agreement mean anything. 23// nx_craft_tile_gate 24// license_tier: ORIGINAL No hw writes (Rule 26). 25import "nx_syscalls.nx" 26import "nx_gate_verdict.nx" 27import "nx_wasm_craft.nx" 28 29const CT_SEED: i64 = 20260728 // craft's shipped identity seed (wc_spec v0) 30const CT_SLACK: i64 = 4096 // arena slack, matching the sibling gates' allocation shape 31const CT_SENTINEL: i64 = 123456789 // a colour word the renderer never writes 32const CT_MIN_DISTINCT: i64 = 40 // the varied-frame floor the world gate already uses 33const CT_BUCKETS: i64 = 4096 34const CT_WARM: i64 = 12 // ticks before measuring: the camera settles onto the ground 35const CT_BANDS_A: i64 = 2 36const CT_BANDS_B: i64 = 3 37const CT_BANDS_C: i64 = 5 38const CT_BANDS_D: i64 = 7 39const CT_BANDS_E: i64 = 16 40 41func ct_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 } 42func ct_n(v: i64) -> i64 { return gv_num(v) } 43 44func ct_arena() -> i64 { 45 let b: i64 = sys_mmap(CRAFT_TOTAL + CT_SLACK) as i64 46 init_impl(b, CT_SEED) 47 var t: i64 = 0 48 while t < CT_WARM { tick_impl(b, 0); t = t + 1 } 49 return b 50} 51// paint every framebuffer word with a value the renderer cannot produce 52// fill the WHOLE framebuffer, not just the written extent: a sentinel past rw*rh is how a write 53// beyond the compact extent gets caught rather than assumed absent. 54func ct_fill(base: i64, v: i64) -> i64 { 55 let f: *i64 = wfb(base) 56 var i: i64 = 0 57 while i < W*H { f[i] = v; i = i + 1 } 58 return 0 59} 60func ct_extent(base: i64) -> i64 { return wc_rw(base) * wc_rh(base) } 61// FULL pixel compare -- returns the count of disagreeing words (0 = bit-identical) 62func ct_diff(a: i64, b: i64) -> i64 { 63 let fa: *i64 = wfb(a) 64 let fb: *i64 = wfb(b) 65 let n: i64 = ct_extent(a) 66 var d: i64 = 0 67 var i: i64 = 0 68 while i < n { if fa[i] != fb[i] { d = d + 1 } i = i + 1 } 69 return d 70} 71// how many framebuffer words still hold the sentinel 72func ct_untouched(base: i64, v: i64) -> i64 { 73 let f: *i64 = wfb(base) 74 let e: i64 = ct_extent(base) 75 var n: i64 = 0 76 var i: i64 = 0 77 while i < e { if f[i] == v { n = n + 1 } i = i + 1 } 78 return n 79} 80// sentinel words PAST the written extent -- all of them must survive any band 81func ct_untouched_past(base: i64, v: i64) -> i64 { 82 let f: *i64 = wfb(base) 83 var n: i64 = 0 84 var i: i64 = ct_extent(base) 85 while i < W*H { if f[i] == v { n = n + 1 } i = i + 1 } 86 return n 87} 88// sentinel words INSIDE a pixel-row range [y0, y1) of the framebuffer 89// COMPACT geometry: ray-row py owns words [py*rw, (py+1)*rw) 90func ct_untouched_rows(base: i64, v: i64, y0: i64, y1: i64) -> i64 { 91 let f: *i64 = wfb(base) 92 let rw: i64 = wc_rw(base) 93 var n: i64 = 0 94 var y: i64 = y0 95 while y < y1 { 96 var x: i64 = 0 97 while x < rw { if f[y*rw + x] == v { n = n + 1 } x = x + 1 } 98 y = y + 1 99 } 100 return n 101} 102func ct_distinct(base: i64) -> i64 { 103 let f: *i64 = wfb(base) 104 let seen: *i64 = sys_mmap(CT_BUCKETS*8) as *i64 105 let e: i64 = ct_extent(base) 106 var q: i64 = 0 107 while q < CT_BUCKETS { seen[q] = 0; q = q + 1 } 108 var d: i64 = 0 109 var i: i64 = 0 110 while i < e { 111 let k: i64 = ((f[i] & 255)/16)*256 + (((f[i] >> 8) & 255)/16)*16 + ((f[i] >> 16) & 255)/16 112 if seen[k % CT_BUCKETS] == 0 { seen[k % CT_BUCKETS] = 1; d = d + 1 } 113 i = i + 1 114 } 115 return d 116} 117// draw one frame as N bands plus the single overlay pass, exactly as N workers would 118func ct_banded(base: i64, nb: i64) -> i64 { 119 let rows: i64 = wc_rh(base) 120 var k: i64 = 0 121 while k < nb { 122 let y0: i64 = rows*k/nb 123 let y1: i64 = rows*(k + 1)/nb 124 render_band_impl(base, y0, y1, k) 125 k = k + 1 126 } 127 render_overlay_impl(base) 128 return 0 129} 130// bit-identity of the one-thread frame and the nb-band frame, on two fresh arenas 131func ct_identical(nb: i64, ctr: *i64, name: *u8) -> i64 { 132 let a: i64 = ct_arena() 133 let b: i64 = ct_arena() 134 render_impl(a) 135 ct_banded(b, nb) 136 let d: i64 = ct_diff(a, b) 137 ct_w(" bands=" as *u8); ct_n(nb); ct_w(" differing_words=" as *u8); ct_n(d); ct_w("\n" as *u8) 138 gv_check(name, d == 0, ctr) 139 return d 140} 141 142func main(argc: i64, argv: *i64) -> i64 { 143 let ctr: *i64 = gv_ctr() 144 gv_head("nx_craft_tile_gate -- GE30: the banded frame is bit-identical to the single-thread frame, and a band owns its rows alone" as *u8) 145 146 // ---- the frame under test is VARIED, or every identity tooth below is vacuous -------------- 147 let a0: i64 = ct_arena() 148 render_impl(a0) 149 let rows: i64 = wc_rh(a0) 150 let q0: i64 = wc_q(a0) 151 let cols: i64 = wc_rw(a0) 152 let dist: i64 = ct_distinct(a0) 153 ct_w(" q=" as *u8); ct_n(q0); ct_w(" ray_rows=" as *u8); ct_n(rows) 154 ct_w(" distinct_colours=" as *u8); ct_n(dist); ct_w(" tile_max=" as *u8); ct_n(TILE_MAX); ct_w("\n" as *u8) 155 gv_check("anti-vacuity-the-single-thread-frame-is-varied-not-blank" as *u8, dist > CT_MIN_DISTINCT, ctr) 156 gv_check("row-door-reports-a-positive-cut-matching-the-adaptive-quality" as *u8, (rows > 0) * (rows == H/q0), ctr) 157 gv_check("the-gate-measures-the-COMPACT-written-extent-not-the-whole-framebuffer" as *u8, (cols == W/q0) * (cols*rows < W*H), ctr) 158 159 // ---- the load-bearing identity, at band counts that do and do not divide evenly ------------- 160 ct_identical(1, ctr, "one-band-equals-the-single-thread-frame-word-for-word" as *u8) 161 ct_identical(CT_BANDS_A, ctr, "two-bands-equal-the-single-thread-frame-word-for-word" as *u8) 162 ct_identical(CT_BANDS_B, ctr, "three-bands-uneven-cut-equal-the-single-thread-frame-word-for-word" as *u8) 163 ct_identical(CT_BANDS_C, ctr, "five-bands-uneven-cut-equal-the-single-thread-frame-word-for-word" as *u8) 164 ct_identical(CT_BANDS_D, ctr, "seven-bands-uneven-cut-equal-the-single-thread-frame-word-for-word" as *u8) 165 ct_identical(CT_BANDS_E, ctr, "sixteen-bands-equal-the-single-thread-frame-word-for-word" as *u8) 166 167 // ---- DISJOINTNESS: one band writes its own pixel rows and not one word beyond --------------- 168 // A band owns ray-rows [y0,y1), which are PIXEL rows [y0*q, y1*q) because each ray paints a qxq 169 // block. Fill with a sentinel, draw the middle band only, and require: every pixel inside the 170 // block was written, and every pixel outside it still holds the sentinel. 171 let b1: i64 = ct_arena() 172 ct_fill(b1, CT_SENTINEL) 173 let y0: i64 = rows/3 174 let y1: i64 = rows*2/3 175 render_band_impl(b1, y0, y1, 0) 176 let inside_left: i64 = ct_untouched_rows(b1, CT_SENTINEL, y0, y1) 177 let above_left: i64 = ct_untouched_rows(b1, CT_SENTINEL, 0, y0) 178 let below_left: i64 = ct_untouched_rows(b1, CT_SENTINEL, y1, rows) 179 let above_total: i64 = y0*cols 180 let below_total: i64 = (rows - y1)*cols 181 ct_w(" band[" as *u8); ct_n(y0); ct_w("," as *u8); ct_n(y1) 182 ct_w(") inside_unwritten=" as *u8); ct_n(inside_left) 183 ct_w(" above_kept=" as *u8); ct_n(above_left); ct_w("/" as *u8); ct_n(above_total) 184 ct_w(" below_kept=" as *u8); ct_n(below_left); ct_w("/" as *u8); ct_n(below_total); ct_w("\n" as *u8) 185 gv_check("the-band-writes-every-pixel-row-it-owns" as *u8, inside_left == 0, ctr) 186 gv_check("the-band-writes-nothing-above-its-first-row" as *u8, (above_left == above_total) * (above_total > 0), ctr) 187 gv_check("the-band-writes-nothing-below-its-last-row" as *u8, (below_left == below_total) * (below_total > 0), ctr) 188 gv_check("the-band-writes-nothing-past-the-compact-extent-into-unwritten-framebuffer" as *u8, ct_untouched_past(b1, CT_SENTINEL) == W*H - ct_extent(b1), ctr) 189 190 // ---- the bands PARTITION the frame: every pixel written exactly once across the whole cut --- 191 let b2: i64 = ct_arena() 192 ct_fill(b2, CT_SENTINEL) 193 var k: i64 = 0 194 while k < CT_BANDS_C { 195 render_band_impl(b2, rows*k/CT_BANDS_C, rows*(k + 1)/CT_BANDS_C, k) 196 k = k + 1 197 } 198 let left2: i64 = ct_untouched(b2, CT_SENTINEL) 199 ct_w(" five bands leave " as *u8); ct_n(left2); ct_w(" of " as *u8); ct_n(ct_extent(b2)); ct_w(" written-extent words unwritten\n" as *u8) 200 gv_check("the-full-cut-covers-the-frame-leaving-no-pixel-unwritten" as *u8, left2 == 0, ctr) 201 202 // ---- CLAMPS: a band past the cut, and an empty band, write nothing rather than past the end -- 203 let b3: i64 = ct_arena() 204 ct_fill(b3, CT_SENTINEL) 205 render_band_impl(b3, rows + 4, rows + 40, 0) 206 gv_check("neg-control-a-band-entirely-past-the-row-count-writes-nothing" as *u8, ct_untouched(b3, CT_SENTINEL) == ct_extent(b3), ctr) 207 render_band_impl(b3, 0, 0, 0) 208 gv_check("neg-control-an-empty-band-writes-nothing" as *u8, ct_untouched(b3, CT_SENTINEL) == ct_extent(b3), ctr) 209 210 // ---- the OVERLAY genuinely draws, so "identical" is a claim about something ------------------ 211 let b4: i64 = ct_arena() 212 let b5: i64 = ct_arena() 213 ct_banded(b4, CT_BANDS_A) // bands + overlay 214 render_band_impl(b5, 0, wc_rh(b5), 0) // bands only, overlay withheld 215 let od: i64 = ct_diff(b4, b5) 216 ct_w(" overlay changes " as *u8); ct_n(od); ct_w(" words\n" as *u8) 217 gv_check("neg-control-the-overlay-pass-changes-pixels-so-identity-is-not-vacuous" as *u8, od > 0, ctr) 218 219 // ---- per-worker scratch is PRIVATE: distinct ids address distinct slots, inside the arena ---- 220 let s0: i64 = O_TILE + 0*TILE_W*8 221 let s1: i64 = O_TILE + 1*TILE_W*8 222 let slast: i64 = O_TILE + (TILE_MAX - 1)*TILE_W*8 + TILE_W*8 223 ct_w(" scratch slot0=" as *u8); ct_n(s0); ct_w(" slot1=" as *u8); ct_n(s1) 224 ct_w(" end=" as *u8); ct_n(slast); ct_w(" arena=" as *u8); ct_n(CRAFT_TOTAL); ct_w("\n" as *u8) 225 gv_check("two-worker-ids-address-two-different-scratch-slots" as *u8, s1 - s0 == TILE_W*8, ctr) 226 gv_check("the-ray-outs-of-one-slot-cannot-reach-the-next-slot" as *u8, TILE_HOUT + 5 <= TILE_W, ctr) 227 gv_check("every-worker-slot-lies-inside-the-declared-arena" as *u8, slast <= CRAFT_TOTAL, ctr) 228 gv_check("the-scratch-region-starts-past-every-other-region-so-no-existing-offset-moved" as *u8, O_TILE >= O_PERF, ctr) 229 // an out-of-range worker id is CLAMPED into the arena rather than trusted 230 let b6: i64 = ct_arena() 231 ct_fill(b6, CT_SENTINEL) 232 render_band_impl(b6, 0, wc_rh(b6), TILE_MAX + 9) 233 gv_check("an-out-of-range-worker-id-is-clamped-and-still-draws-its-band" as *u8, ct_untouched(b6, CT_SENTINEL) == 0, ctr) 234 235 // ---- THE RACE PROOF A SEQUENTIAL GATE CAN ACTUALLY GIVE ------------------------------------ 236 // Bands here run one after another, so a shared scratch produces IDENTICAL bytes and every 237 // identity tooth above stays green while the browser races. Stating that limit and testing 238 // around it: a band must write ITS OWN slot and no other. ⚠The first cut of this tooth ran the 239 // band as worker 0 and asserted worker 1 was clean -- and a planted mutant that funnels EVERY 240 // worker into slot 0 survived it, because a worker-0 band writing slot 0 is what correct code 241 // does too. The tooth only bites when the band runs as a NON-ZERO worker: slot 1 must change, 242 // slot 0 must not. Both halves are required; either alone passes for the wrong reason. 243 let b7: i64 = ct_arena() 244 let sc0: *i64 = (b7 + O_TILE) as *i64 245 let sc1: *i64 = (b7 + O_TILE + 1*TILE_W*8) as *i64 246 var j: i64 = 0 247 while j < TILE_W { sc0[j] = CT_SENTINEL; sc1[j] = CT_SENTINEL; j = j + 1 } 248 render_band_impl(b7, 0, wc_rh(b7), 1) 249 var kept0: i64 = 0 250 var moved1: i64 = 0 251 j = 0 252 while j < TILE_W { 253 if sc0[j] == CT_SENTINEL { kept0 = kept0 + 1 } 254 if sc1[j] != CT_SENTINEL { moved1 = moved1 + 1 } 255 j = j + 1 256 } 257 ct_w(" band as worker 1: slot0 words kept=" as *u8); ct_n(kept0); ct_w("/" as *u8); ct_n(TILE_W) 258 ct_w(" slot1 words written=" as *u8); ct_n(moved1); ct_w("\n" as *u8) 259 gv_check("a-band-drawn-as-worker-1-writes-its-own-scratch-slot" as *u8, moved1 > 0, ctr) 260 gv_check("a-band-drawn-as-worker-1-leaves-every-word-of-worker-0-scratch-untouched" as *u8, kept0 == TILE_W, ctr) 261 262 // ---- the digest door discriminates (a ruler that returns one number for everything is none) -- 263 let d4: i64 = wc_fbdigest(b4) 264 let d4b: i64 = wc_fbdigest(b4) 265 let d5: i64 = wc_fbdigest(b5) 266 ct_w(" digest(with overlay)=" as *u8); ct_n(d4); ct_w(" (without)=" as *u8); ct_n(d5); ct_w("\n" as *u8) 267 gv_check("the-frame-digest-is-stable-on-an-unchanged-frame" as *u8, d4 == d4b, ctr) 268 gv_check("neg-control-the-frame-digest-separates-two-different-frames" as *u8, d4 != d5, ctr) 269 let a1: i64 = ct_arena() 270 let a2: i64 = ct_arena() 271 render_impl(a1) 272 ct_banded(a2, CT_BANDS_D) 273 gv_check("the-digest-agrees-with-the-full-compare-on-the-banded-frame" as *u8, wc_fbdigest(a1) == wc_fbdigest(a2), ctr) 274 275 return gv_verdict("craft_tile_gate" as *u8, ctr, "the decomposition below the browser: bands are disjoint, cover the frame and reproduce the single-thread bytes exactly; the Worker wiring and the shared memory it runs over are GE30's page half" as *u8) 276}