nx_wgsl_compute_gate.nx source
↩ module page · 170 lines · 10042 B
1// nx_wgsl_compute_gate.nx -- GE43 REFEREE: the compute stage of the ONE NishiLang shader backend
2// emits EXACTLY the WGSL the kernel contract names, and the GLSL side REFUSES it BY NAME.
3//
4// SUBJECT: the DEPLOYED nx_wgsl.elf (end-to-end -- this gate forks the artifact a browser page
5// would be built from, not the library). `nx_wgsl compute` prints the depth-min kernel through both
6// backends; every tooth below is a KAT over those bytes. A KAT is the right shape here: a shader
7// backend that drifts by one character produces a program that compiles and draws the wrong
8// picture, so "contains the right idea" is not a bar -- the bytes are.
9//
10// WHY THE GLSL REFUSAL IS LOAD-BEARING: WebGL2 has no compute stage, no storage buffers and no
11// atomics. A backend that silently dropped the storage declarations would emit a fragment program
12// that compiles, links, runs and draws nothing forever. Two teeth pin the refusal (the STAGE refusal
13// on a compute emit, the DECLARATION refusal when the same kernel is asked for as a fragment stage),
14// so the refusal cannot degrade into a later accident and still read GREEN.
15//
16// CONTROLS: the rung-1 contract (fullscreen triangle, trace_equal=1, uncovered_rc=-1) must still
17// hold on the same binary -- a compute edit that broke rung 1 must read RED here, not on some other
18// board weeks later. neg-control-* teeth assert refusals and absences.
19//
20// nx_wgsl_compute_gate [subject-elf] default ./nx_wgsl.elf, then _offc/nx_wgsl.elf
21// license_tier: ORIGINAL No hw writes (Rule 26).
22import "nx_syscalls.nx"
23import "nx_gate_verdict.nx"
24import "nx_tool_run.nx"
25
26const WCG_CAP: i64 = 65536
27const WCG_TMO_MS: i64 = 20000
28const WCG_ARGV: i64 = 4
29const WCG_SUBJECT: *u8 = "./nx_wgsl.elf"
30const WCG_SUBJECT_OFFC: *u8 = "_offc/nx_wgsl.elf"
31// THE CONTRACT BYTES. One line each, exactly as wgsl_emit_module lays them out for shsrc_depth_min.
32const WCG_L_DEPTH: *u8 = "@group(0)@binding(1)var<storage,read_write> depth:array<atomic<u32>>;\n"
33const WCG_L_ZIN: *u8 = "@group(0)@binding(2)var<storage,read> zin:array<u32>;\n"
34const WCG_L_ENTRY: *u8 = "@compute @workgroup_size(64) fn main(@builtin(global_invocation_id) gid:vec3u){\n"
35const WCG_L_GID: *u8 = "var i:u32=gid.x;\n"
36const WCG_L_ATOMIC: *u8 = "atomicMin(&depth[i],zin[i]);\n"
37const WCG_L_CLOSE: *u8 = "}\n"
38const WCG_GL_RC: *u8 = "glsl_compute_rc=-1"
39const WCG_GL_NAMED: *u8 = "glsl_compute_named=glsl: compute stage"
40const WCG_GL_FRAG_RC: *u8 = "glsl_fragment_of_kernel_rc=-1"
41const WCG_GL_FRAG_NAMED: *u8 = "glsl_fragment_of_kernel_named=glsl: storage buffer declaration"
42const WCG_WG_CLEAN: *u8 = "wgsl_refused=NONE"
43const WCG_R1_TRACE: *u8 = "trace_equal=1"
44const WCG_R1_UNCOV: *u8 = "uncovered_rc=-1"
45const WCG_LEAK_GL: *u8 = "gl_"
46const WCG_LEAK_VERSION: *u8 = "version 300"
47// The whole WGSL body, in order: the six lines above concatenated. Asserting the WHOLE text and not
48// only each line catches a reordering (a storage decl emitted after the entry is a compile error in
49// WGSL) that six independent contains-checks would wave through. The contract LENGTH is DERIVED from
50// the six literals at run time (wcg_contract_len) -- the first cut hand-counted it beside the strings,
51// was wrong by nine bytes on the first run, and that is exactly the second-copy-of-a-literal's-shape
52// defect the magic-number law names: bind the string once, derive the number.
53
54func wcg_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
55func wcg_exists(path: *u8) -> i64 { let fd: i64 = sys_openat_rd(path); if fd < 0 { return 0 } sys_close(fd); return 1 }
56
57// first offset of needle in buf[0..n), or -1
58func wcg_find(buf: *u8, n: i64, needle: *u8) -> i64 {
59 let ml: i64 = wcg_slen(needle)
60 if ml == 0 { return 0 - 1 }
61 var i: i64 = 0
62 while i + ml <= n {
63 var k: i64 = 0
64 var hit: i64 = 1
65 while k < ml { if buf[i + k] != needle[k] { hit = 0; k = ml } else { k = k + 1 } }
66 if hit == 1 { return i }
67 i = i + 1
68 }
69 return 0 - 1
70}
71func wcg_has(buf: *u8, n: i64, needle: *u8) -> i64 { if wcg_find(buf, n, needle) >= 0 { return 1 } return 0 }
72func wcg_contract_len() -> i64 {
73 return wcg_slen(WCG_L_DEPTH) + wcg_slen(WCG_L_ZIN) + wcg_slen(WCG_L_ENTRY) + wcg_slen(WCG_L_GID) + wcg_slen(WCG_L_ATOMIC) + wcg_slen(WCG_L_CLOSE)
74}
75
76// run the subject with one optional verb; returns rc, fills out/ol (NUL-terminated inside cap)
77func wcg_run(subject: *u8, verb: *u8, out: *u8, ol: *i64) -> i64 {
78 let av: *i64 = sys_mmap(8 * WCG_ARGV) as *i64
79 var n: i64 = 0
80 av[n] = subject as i64; n = n + 1
81 if (verb as i64) != 0 { av[n] = verb as i64; n = n + 1 }
82 av[n] = 0
83 ol[0] = 0
84 let rc: i64 = tr_run_capture_to(subject, av, out, WCG_CAP, ol, WCG_TMO_MS)
85 var term: i64 = ol[0]
86 if term < 0 { term = 0 }
87 if term >= WCG_CAP { term = WCG_CAP - 1 }
88 out[term] = 0 as u8
89 return rc
90}
91
92func main(argc: i64, argv: *i64) -> i64 {
93 let ctr: *i64 = gv_ctr()
94 gv_head("nx_wgsl_compute_gate -- GE43: the compute stage emits the kernel contract bytes exactly; GLSL refuses by name" as *u8)
95 var subject: *u8 = WCG_SUBJECT
96 if argc > 1 { subject = argv[1] as *u8 }
97 if wcg_exists(subject) == 0 { if argc <= 1 { subject = WCG_SUBJECT_OFFC } }
98 let present: i64 = wcg_exists(subject)
99 gv_puts("subject=" as *u8); gv_puts(subject); gv_puts("\n" as *u8)
100 if gv_need("subject-nx_wgsl.elf-present" as *u8, present, ctr) == 0 {
101 return gv_verdict("nx_wgsl_compute_gate" as *u8, ctr, "SKIP: the subject binary is absent -- nothing was measured" as *u8)
102 }
103
104 // ---- the compute emit ----
105 let out: *u8 = sys_mmap(WCG_CAP)
106 let ol: *i64 = sys_mmap(16) as *i64
107 let rc: i64 = wcg_run(subject, "compute" as *u8, out, ol)
108 let n: i64 = ol[0]
109 gv_puts("compute_rc=" as *u8); gv_num(rc); gv_puts(" bytes=" as *u8); gv_num(n); gv_puts("\n" as *u8)
110 gv_check("compute-verb-exits-0" as *u8, rc == 0, ctr)
111 gv_check("compute-verb-produced-output" as *u8, n > 0, ctr)
112 gv_check("wgsl-storage-depth-atomic-read_write-binding1" as *u8, wcg_has(out, n, WCG_L_DEPTH), ctr)
113 gv_check("wgsl-storage-zin-read-binding2" as *u8, wcg_has(out, n, WCG_L_ZIN), ctr)
114 gv_check("wgsl-compute-entry-workgroup64-global_invocation_id" as *u8, wcg_has(out, n, WCG_L_ENTRY), ctr)
115 gv_check("wgsl-gid-x-into-u32-local" as *u8, wcg_has(out, n, WCG_L_GID), ctr)
116 gv_check("wgsl-atomicMin-takes-address-of-target" as *u8, wcg_has(out, n, WCG_L_ATOMIC), ctr)
117 // ORDER: decl, decl, entry, body, body, close -- each must follow the previous
118 let o1: i64 = wcg_find(out, n, WCG_L_DEPTH)
119 let o2: i64 = wcg_find(out, n, WCG_L_ZIN)
120 let o3: i64 = wcg_find(out, n, WCG_L_ENTRY)
121 let o4: i64 = wcg_find(out, n, WCG_L_GID)
122 let o5: i64 = wcg_find(out, n, WCG_L_ATOMIC)
123 var ordered: i64 = 0
124 if o1 >= 0 { if o2 > o1 { if o3 > o2 { if o4 > o3 { if o5 > o4 { ordered = 1 } } } } }
125 gv_check("wgsl-lines-in-contract-order-decls-before-entry-before-body" as *u8, ordered, ctr)
126 // WHOLE-TEXT: the body is exactly the concatenation (adjacent, nothing between the lines)
127 var contiguous: i64 = 0
128 if ordered == 1 {
129 if o2 == o1 + wcg_slen(WCG_L_DEPTH) { if o3 == o2 + wcg_slen(WCG_L_ZIN) { if o4 == o3 + wcg_slen(WCG_L_ENTRY) { if o5 == o4 + wcg_slen(WCG_L_GID) { contiguous = 1 } } } }
130 }
131 gv_check("wgsl-body-is-exactly-the-six-contract-lines-nothing-between" as *u8, contiguous, ctr)
132 // byte count announced by the subject equals the derived contract length
133 let bpos: i64 = wcg_find(out, n, "wgsl_bytes=" as *u8)
134 var announced: i64 = 0 - 1
135 if bpos >= 0 {
136 var q: i64 = bpos + 11
137 announced = 0
138 while q < n { let c: i64 = out[q] as i64; if c >= 48 { if c <= 57 { announced = announced*10 + (c - 48); q = q + 1 } else { q = n } } else { q = n } }
139 }
140 let clen: i64 = wcg_contract_len()
141 gv_puts("announced_wgsl_bytes=" as *u8); gv_num(announced); gv_puts(" contract_bytes=" as *u8); gv_num(clen); gv_puts("\n" as *u8)
142 gv_check("wgsl-announced-byte-count-equals-derived-contract-length" as *u8, announced == clen, ctr)
143 gv_check("wgsl-backend-did-not-refuse" as *u8, wcg_has(out, n, WCG_WG_CLEAN), ctr)
144 // ---- the GLSL refusals ----
145 gv_check("neg-control-glsl-compute-stage-refuses-rc-minus-1" as *u8, wcg_has(out, n, WCG_GL_RC), ctr)
146 gv_check("neg-control-glsl-refusal-names-the-compute-stage" as *u8, wcg_has(out, n, WCG_GL_NAMED), ctr)
147 gv_check("neg-control-glsl-fragment-of-kernel-refuses-rc-minus-1" as *u8, wcg_has(out, n, WCG_GL_FRAG_RC), ctr)
148 gv_check("neg-control-glsl-fragment-refusal-names-the-storage-declaration" as *u8, wcg_has(out, n, WCG_GL_FRAG_NAMED), ctr)
149 // ---- dialect leaks: the WGSL text must carry no GLSL spelling ----
150 var leak: i64 = 0
151 if o1 >= 0 { if o5 >= 0 {
152 let body_end: i64 = o5 + wcg_slen(WCG_L_ATOMIC) + wcg_slen(WCG_L_CLOSE)
153 let bodyp: *u8 = ((out as i64) + o1) as *u8
154 if wcg_has(bodyp, body_end - o1, WCG_LEAK_GL) == 1 { leak = 1 }
155 if wcg_has(bodyp, body_end - o1, WCG_LEAK_VERSION) == 1 { leak = 1 }
156 } }
157 gv_check("neg-control-no-glsl-spelling-leaks-into-the-wgsl-body" as *u8, leak == 0, ctr)
158
159 // ---- rung-1 control on the SAME binary ----
160 let out1: *u8 = sys_mmap(WCG_CAP)
161 let ol1: *i64 = sys_mmap(16) as *i64
162 let rc1: i64 = wcg_run(subject, 0 as *u8, out1, ol1)
163 let n1: i64 = ol1[0]
164 gv_puts("rung1_rc=" as *u8); gv_num(rc1); gv_puts(" bytes=" as *u8); gv_num(n1); gv_puts("\n" as *u8)
165 gv_check("control-rung1-fullscreen-triangle-still-emits-rc-0" as *u8, rc1 == 0, ctr)
166 gv_check("control-rung1-trace-identity-still-holds" as *u8, wcg_has(out1, n1, WCG_R1_TRACE), ctr)
167 gv_check("neg-control-rung1-uncovered-construct-still-refuses" as *u8, wcg_has(out1, n1, WCG_R1_UNCOV), ctr)
168
169 return gv_verdict("nx_wgsl_compute_gate" as *u8, ctr, "GE43 compute stage: the deployed nx_wgsl.elf emits the depth-min kernel bytes exactly and GLSL refuses it by name" as *u8)
170}