nx_wasm_threads_gate.nx source
↩ module page · 285 lines · 19382 B
1// nx_wasm_threads_gate.nx -- LN33 / LN34 REFEREE (lang.plan): wasm threads from the sovereign compiler, ONE family.
2//
3// THE FAMILY IS THE INCUMBENT'S: the parser builtins __atomic_load_i64 / __atomic_store_i64 / __atomic_cas_i64 /
4// __atomic_faa_i64 / __atomic_fence (nx_atom.nx wraps them) lower to OP_ATOMIC_* in the IR; the x86-64 backend
5// lowers those to LOCK-prefixed instructions, the rv64 backend to AMO and lr/sc (LN34), and the wasm backend to the
6// 0xFE family over a module-declared shared memory -- with __syscall(98 futex, addr, WAIT|WAKE, val) lowering to
7// memory.atomic.wait32 / memory.atomic.notify. Under --nothreads the SAME ops lower to plain single-thread twins.
8// SUBJECTS, forked by their SERVED name first: ./nx_compile_wat.elf (the WAT backend driver over nx_wasm.nx) and
9// ./nx_wat_compiler.elf (WAT -> wasm); the VM twin nx_wasm_vm is composed IN-PROCESS so its 0xFE semantics are
10// measured here rather than trusted.
11// FIXTURES are assembled at RUNTIME under the fixture dir (argv[1], default /tmp/nx_wasm_threads_gate) and use the
12// builtins directly, so no library has to be copied beside them: a shared-declaring module, a plain module (the
13// neutrality control), a shared-without-maximum module (the emitter must refuse by name), a hand-written WAT with a
14// shared memory and no maximum (the WAT compiler must refuse by name), and the --nothreads twin of the shared module.
15// THE BROWSER HALF of the done-rule -- two Workers over ONE shared WebAssembly.Memory behind real cross-origin
16// isolation, the atomic counter exact and the plain-store twin losing updates -- lives on the CDP wire
17// (nishi-ops/ac_cdp.py with AC_CDP_SERVE), because a gate on the NAS has no browser; its numbers are journaled on
18// lang.plan LN33, and this gate proves everything BELOW the browser and says so in its verdict note.
19// nx_wasm_threads_gate [fixture-dir]
20// license_tier: ORIGINAL No hw writes (Rule 26).
21import "nx_syscalls.nx"
22import "nx_gate_verdict.nx"
23import "nx_tool_run.nx"
24import "nx_wasm_vm.nx"
25
26const TG_DIR_DEFAULT: *u8 = "/tmp/nx_wasm_threads_gate"
27const TG_CAP: i64 = 1048576 // diagnostic capture for a forked tool (the WAT itself goes to a file)
28const TG_TMO_MS: i64 = 60000
29const TG_MODE_755: i64 = 493
30const TG_MODE_644: i64 = 420
31const TG_PATH_BYTES: i64 = 1024
32const TG_TICKS: i64 = 1000
33const TG_CELL_A: i64 = 64
34const TG_CELL_B: i64 = 256
35const TG_CELL_C: i64 = 512
36const TG_EXIT_EMIT_REFUSED: i64 = 3
37const TG_EXIT_WATC_REFUSED: i64 = 1
38const TG_PAGE_BYTES: i64 = 65536
39// expected probe values, derived from the fixture arithmetic (see the fixture text below)
40const TG_EXP_CAS: i64 = 1009
41const TG_EXP_FUTEX: i64 = 10
42const TG_EXP_FUTEX_TWIN: i64 = 0
43const TG_EXP_BIG: i64 = 10000000003
44
45const TG_FX_SHARED: *u8 = "static nx_wasm_pages_req: i64 = 1\nstatic nx_wasm_pages_max: i64 = 2\nstatic nx_wasm_shared_req: i64 = 1\nconst MO: i64 = 5\nfunc tick(p: i64, n: i64) -> i64 {\n let c: *i64 = p as *i64\n var i: i64 = 0\n while i < n { __atomic_faa_i64(c, 1, MO); i = i + 1 }\n return __atomic_load_i64(c, MO)\n}\nfunc tick_racy(p: i64, n: i64) -> i64 {\n let q: *i64 = p as *i64\n var i: i64 = 0\n while i < n { q[0] = q[0] + 1; i = i + 1 }\n return q[0]\n}\nfunc probe_cas(p: i64) -> i64 {\n let c: *i64 = p as *i64\n let s: i64 = __atomic_store_i64(c, 7, MO)\n let a: i64 = __atomic_cas_i64(c, 7, 9, MO)\n let b: i64 = __atomic_cas_i64(c, 7, 11, MO)\n let v: i64 = __atomic_load_i64(c, MO)\n return a * 1000 + b * 100 + v + s\n}\nfunc probe_futex(p: i64) -> i64 {\n let c: *i64 = p as *i64\n let s: i64 = __atomic_store_i64(c, 5, MO)\n let w: i64 = __syscall(98, p, 128, 6, 0, 0, 0)\n let nt: i64 = __syscall(98, p, 129, 1, 0, 0, 0)\n let f: i64 = __atomic_fence(MO)\n return w * 10 + nt + s + f\n}\nfunc probe_big(p: i64) -> i64 {\n let c: *i64 = p as *i64\n let s: i64 = __atomic_store_i64(c, 5000000000, MO)\n let old: i64 = __atomic_faa_i64(c, 3, MO)\n return old + __atomic_load_i64(c, MO) + s\n}\n"
46const TG_FX_PLAIN: *u8 = "func plain(a: i64, b: i64) -> i64 { return a + b }\n"
47const TG_FX_NOMAX: *u8 = "static nx_wasm_pages_req: i64 = 1\nstatic nx_wasm_shared_req: i64 = 1\nfunc tick(p: i64, n: i64) -> i64 { return __atomic_faa_i64(p as *i64, n, 5) }\n"
48const TG_WAT_NOMAX: *u8 = "(module\n (memory (export \"memory\") 1 shared)\n (func (export \"f\") (result i64)\n i64.const 1\n )\n)\n"
49
50func tg_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
51func tg_path(dir: *u8, name: *u8) -> *u8 {
52 let p: *u8 = sys_mmap(TG_PATH_BYTES)
53 var o: i64 = gv_cat(p, 0, dir)
54 o = gv_cat(p, o, "/" as *u8)
55 o = gv_cat(p, o, name)
56 p[o] = 0 as u8
57 return p
58}
59func tg_write(path: *u8, s: *u8) -> i64 {
60 let fd: i64 = sys_openat_wr(path, TG_MODE_644)
61 if fd < 0 { return 0 }
62 sys_write(fd, s, tg_slen(s))
63 sys_close(fd)
64 return 1
65}
66func tg_exists(path: *u8) -> i64 {
67 let fd: i64 = sys_openat_rd(path)
68 if fd < 0 { return 0 }
69 sys_close(fd)
70 return 1
71}
72func tg_pick3(a: *u8, b: *u8, c: *u8) -> *u8 {
73 if tg_exists(a) == 1 { return a }
74 if tg_exists(b) == 1 { return b }
75 if tg_exists(c) == 1 { return c }
76 return 0 as *u8
77}
78// substring presence over a byte buffer (needle NUL-terminated); a zero-length needle is never present
79func tg_has(buf: *u8, n: i64, needle: *u8) -> i64 {
80 let m: i64 = tg_slen(needle)
81 if m == 0 { return 0 }
82 if (buf as i64) == 0 { return 0 }
83 var i: i64 = 0
84 while i + m <= n {
85 var k: i64 = 0
86 var ok: i64 = 1
87 while k < m {
88 if buf[i + k] != needle[k] { ok = 0; k = m }
89 k = k + 1
90 }
91 if ok == 1 { return 1 }
92 i = i + 1
93 }
94 return 0
95}
96// byte-triple presence (an opcode prefix, sub-opcode and align byte) over a binary buffer
97func tg_has3(buf: *u8, n: i64, a: i64, b: i64, c: i64) -> i64 {
98 if (buf as i64) == 0 { return 0 }
99 var i: i64 = 0
100 while i + 3 <= n {
101 if buf[i] == (a as u8) { if buf[i + 1] == (b as u8) { if buf[i + 2] == (c as u8) { return 1 } } }
102 i = i + 1
103 }
104 return 0
105}
106// fork <exe> with up to four positional args (a NULL arg ends the vector); merged stdout+stderr -> out
107func tg_run(exe: *u8, a1: *u8, a2: *u8, a3: *u8, a4: *u8, out: *u8, outlen: *i64) -> i64 {
108 return tg_run5(exe, a1, a2, a3, a4, 0 as *u8, out, outlen)
109}
110// five positional args: --shared <req> <max> <src> <out> needs every one of them, and a runner one slot
111// short would have handed the driver a PATH where the maximum belongs -- read as 0 and refused for the
112// wrong reason, which is a green tooth measuring nothing.
113func tg_run5(exe: *u8, a1: *u8, a2: *u8, a3: *u8, a4: *u8, a5: *u8, out: *u8, outlen: *i64) -> i64 {
114 let av: *i64 = sys_mmap(64) as *i64
115 av[0] = exe as i64
116 av[1] = a1 as i64
117 av[2] = a2 as i64
118 av[3] = a3 as i64
119 av[4] = a4 as i64
120 av[5] = a5 as i64
121 av[6] = 0
122 return tr_run_capture_to(exe, av, out, TG_CAP, outlen, TG_TMO_MS)
123}
124// the VM twin: load a .wasm, parse, look up an export and call it with (a, b)
125func tg_vm_call2(bytes: *u8, len: i64, name: *u8, a: i64, b: i64, nargs: i64, ok: *i64) -> i64 {
126 ok[0] = 0
127 if (bytes as i64) == 0 { return 0 }
128 let mod: *WasmMod = wm_new(bytes, len)
129 wm_parse(mod)
130 let fidx: i64 = wm_find_export(mod, name)
131 if fidx < 0 { return 0 }
132 let args: *i64 = sys_mmap(32) as *i64
133 args[0] = a
134 args[1] = b
135 ok[0] = 1
136 return wm_call(mod, fidx, args, nargs)
137}
138
139func main(argc: i64, argv: *i64) -> i64 {
140 let ctr: *i64 = gv_ctr()
141 gv_head("nx_wasm_threads_gate -- LN33/LN34: the IR atomic family on the wasm lane, shared memory, futex, proven below the browser" as *u8)
142 var dir: *u8 = TG_DIR_DEFAULT
143 if argc > 1 { dir = argv[1] as *u8 }
144 sys_mkdir(dir, TG_MODE_755)
145
146 // ---- subjects and preconditions ----------------------------------------------------------
147 let cw: *u8 = tg_pick3("./nx_compile_wat.elf" as *u8, "_build/nx_compile_wat.sov.elf" as *u8, "_offc/nx_compile_wat.elf" as *u8)
148 let wc: *u8 = tg_pick3("./nx_wat_compiler.elf" as *u8, "_build/nx_wat_compiler.sov.elf" as *u8, "_offc/nx_wat_compiler.elf" as *u8)
149 let have_cw: i64 = gv_need("nx_compile_wat binary (served ./nx_compile_wat.elf, else _build, else _offc)" as *u8, (cw as i64) != 0, ctr)
150 let have_wc: i64 = gv_need("nx_wat_compiler binary (served ./nx_wat_compiler.elf, else _build, else _offc)" as *u8, (wc as i64) != 0, ctr)
151 if have_cw * have_wc != 1 {
152 return gv_verdict("wasm_threads_gate" as *u8, ctr, "the subjects are absent on this host" as *u8)
153 }
154 gv_puts(" subjects: " as *u8); gv_puts(cw); gv_puts(" + " as *u8); gv_puts(wc); gv_puts(" fixtures: " as *u8); gv_puts(dir); gv_puts("\n" as *u8)
155
156 // ---- fixtures assembled at runtime --------------------------------------------------------
157 let lenp: *i64 = sys_mmap(16) as *i64
158 let fx_shared: *u8 = tg_path(dir, "fx_shared.nx" as *u8)
159 let fx_plain: *u8 = tg_path(dir, "fx_plain.nx" as *u8)
160 let fx_nomax: *u8 = tg_path(dir, "fx_nomax.nx" as *u8)
161 let wat_nomax: *u8 = tg_path(dir, "nomax.wat" as *u8)
162 tg_write(fx_shared, TG_FX_SHARED)
163 tg_write(fx_plain, TG_FX_PLAIN)
164 tg_write(fx_nomax, TG_FX_NOMAX)
165 tg_write(wat_nomax, TG_WAT_NOMAX)
166 let out: *u8 = sys_mmap(TG_CAP)
167 let outlen: *i64 = sys_mmap(16) as *i64
168
169 // ---- 1. the emitter on the shared module -------------------------------------------------
170 let w_shared: *u8 = tg_path(dir, "fx_shared.wat" as *u8)
171 let rc1: i64 = tg_run(cw, fx_shared, w_shared, 0 as *u8, 0 as *u8, out, outlen)
172 gv_check("emitter-compiles-the-shared-module-rc0" as *u8, rc1 == 0, ctr)
173 let wat: *u8 = sys_read_file(w_shared, lenp)
174 let wat_n: i64 = lenp[0]
175 gv_check("wat-imports-a-shared-memory-with-a-maximum" as *u8, tg_has(wat, wat_n, "(import \"env\" \"memory\" (memory 1 2 shared))" as *u8), ctr)
176 gv_check("wat-exports-the-imported-memory-under-the-old-name" as *u8, tg_has(wat, wat_n, "(export \"memory\" (memory 0))" as *u8), ctr)
177 gv_check("wat-faa-lowers-to-i64-atomic-rmw-add" as *u8, tg_has(wat, wat_n, "i64.atomic.rmw.add" as *u8), ctr)
178 gv_check("wat-cas-lowers-to-i64-atomic-rmw-cmpxchg" as *u8, tg_has(wat, wat_n, "i64.atomic.rmw.cmpxchg" as *u8), ctr)
179 gv_check("wat-atomic-load-and-store-lower-to-the-i64-family" as *u8, tg_has(wat, wat_n, "i64.atomic.load" as *u8) * tg_has(wat, wat_n, "i64.atomic.store" as *u8), ctr)
180 gv_check("wat-futex-syscalls-lower-to-wait32-and-notify" as *u8, tg_has(wat, wat_n, "memory.atomic.wait32" as *u8) * tg_has(wat, wat_n, "memory.atomic.notify" as *u8), ctr)
181 gv_check("wat-fence-lowers-to-atomic-fence" as *u8, tg_has(wat, wat_n, "atomic.fence" as *u8), ctr)
182
183 // ---- 2. the WAT compiler on that WAT ------------------------------------------------------
184 let b_shared: *u8 = tg_path(dir, "fx_shared.wasm" as *u8)
185 let rc2: i64 = tg_run(wc, w_shared, b_shared, 0 as *u8, 0 as *u8, out, outlen)
186 gv_check("wat-compiler-accepts-the-shared-module-rc0" as *u8, rc2 == 0, ctr)
187 let bin: *u8 = sys_read_file(b_shared, lenp)
188 let bin_n: i64 = lenp[0]
189 // import entry: ..."memory" desc=02 flags=03 (shared+max) min=01 max=02
190 var imp_ok: i64 = 0
191 var bi: i64 = 0
192 while bi + 10 <= bin_n {
193 if bin[bi] == (0x6D as u8) { if bin[bi + 1] == (0x65 as u8) { if bin[bi + 5] == (0x79 as u8) {
194 if bin[bi + 6] == (2 as u8) { if bin[bi + 7] == (3 as u8) { if bin[bi + 8] == (1 as u8) { if bin[bi + 9] == (2 as u8) { imp_ok = 1 } } } }
195 } } }
196 bi = bi + 1
197 }
198 gv_check("wasm-import-section-declares-memory-with-limits-flag-3-min-1-max-2" as *u8, imp_ok, ctr)
199 gv_check("wasm-bytes-carry-i64-atomic-rmw-add-FE-1F-align-3" as *u8, tg_has3(bin, bin_n, 0xFE, 0x1F, 3), ctr)
200 gv_check("wasm-bytes-carry-cmpxchg-FE-49-align-3" as *u8, tg_has3(bin, bin_n, 0xFE, 0x49, 3), ctr)
201 gv_check("wasm-bytes-carry-atomic-load-FE-11-and-store-FE-18" as *u8, tg_has3(bin, bin_n, 0xFE, 0x11, 3) * tg_has3(bin, bin_n, 0xFE, 0x18, 3), ctr)
202 gv_check("wasm-bytes-carry-wait32-FE-01-and-notify-FE-00" as *u8, tg_has3(bin, bin_n, 0xFE, 0x01, 2) * tg_has3(bin, bin_n, 0xFE, 0x00, 2), ctr)
203 gv_check("wasm-bytes-carry-the-fence-FE-03-00" as *u8, tg_has3(bin, bin_n, 0xFE, 0x03, 0), ctr)
204
205 // ---- 3. the VM twin executes the 0xFE family with the reference semantics -----------------
206 let ok: *i64 = sys_mmap(16) as *i64
207 let mod: *WasmMod = wm_new(bin, bin_n)
208 wm_parse(mod)
209 gv_check("vm-supplies-the-imported-memory-sized-from-the-import" as *u8, mod.mem_bytes == TG_PAGE_BYTES, ctr)
210 let f_tick: i64 = wm_find_export(mod, "tick" as *u8)
211 gv_check("vm-finds-the-tick-export" as *u8, f_tick >= 0, ctr)
212 let args: *i64 = sys_mmap(32) as *i64
213 args[0] = TG_CELL_A; args[1] = TG_TICKS
214 let t1: i64 = wm_call(mod, f_tick, args, 2)
215 gv_check("vm-tick-1000-atomic-faa-reads-1000" as *u8, t1 == TG_TICKS, ctr)
216 let t2: i64 = wm_call(mod, f_tick, args, 2)
217 gv_check("vm-second-tick-accumulates-to-2000-so-the-memory-persists" as *u8, t2 == TG_TICKS * 2, ctr)
218 let v_cas: i64 = tg_vm_call2(bin, bin_n, "probe_cas" as *u8, TG_CELL_B, 0, 1, ok)
219 gv_check("vm-cas-swaps-once-then-refuses-reads-1009" as *u8, (ok[0] == 1) * (v_cas == TG_EXP_CAS), ctr)
220 let v_fx: i64 = tg_vm_call2(bin, bin_n, "probe_futex" as *u8, TG_CELL_B, 0, 1, ok)
221 gv_check("vm-futex-wait-answers-not-equal-and-wake-wakes-nobody-10" as *u8, (ok[0] == 1) * (v_fx == TG_EXP_FUTEX), ctr)
222 let v_big: i64 = tg_vm_call2(bin, bin_n, "probe_big" as *u8, TG_CELL_C, 0, 1, ok)
223 gv_check("vm-faa-over-a-value-past-32-bits-reads-10000000003" as *u8, (ok[0] == 1) * (v_big == TG_EXP_BIG), ctr)
224
225 // ---- 4. neg-controls: both refusals fire by name -------------------------------------------
226 let w_nomax: *u8 = tg_path(dir, "fx_nomax.wat" as *u8)
227 let rc4: i64 = tg_run(cw, fx_nomax, w_nomax, 0 as *u8, 0 as *u8, out, outlen)
228 gv_check("neg-control-emitter-refuses-shared-without-a-maximum-exit-3-naming-nx_wasm_pages_max" as *u8, (rc4 == TG_EXIT_EMIT_REFUSED) * tg_has(out, outlen[0], "nx_wasm_pages_max" as *u8), ctr)
229 let b_nomax: *u8 = tg_path(dir, "nomax.wasm" as *u8)
230 let rc5: i64 = tg_run(wc, wat_nomax, b_nomax, 0 as *u8, 0 as *u8, out, outlen)
231 gv_check("neg-control-wat-compiler-refuses-shared-without-a-maximum-by-name" as *u8, (rc5 == TG_EXIT_WATC_REFUSED) * tg_has(out, outlen[0], "WATC REFUSED" as *u8), ctr)
232
233 // ---- 5. neutrality: a plain module carries none of this --------------------------------------
234 let w_plain: *u8 = tg_path(dir, "fx_plain.wat" as *u8)
235 let rc6: i64 = tg_run(cw, fx_plain, w_plain, 0 as *u8, 0 as *u8, out, outlen)
236 let pw: *u8 = sys_read_file(w_plain, lenp)
237 let pw_n: i64 = lenp[0]
238 gv_check("plain-module-still-emits-the-default-defined-memory" as *u8, (rc6 == 0) * tg_has(pw, pw_n, "(memory (export \"memory\") 364)" as *u8), ctr)
239 gv_check("plain-module-carries-no-shared-and-no-atomic-token" as *u8, (1 - tg_has(pw, pw_n, "shared" as *u8)) * (1 - tg_has(pw, pw_n, "atomic" as *u8)), ctr)
240
241 // ---- 5b. GE30 THE BUILD-LANE DECLARATION: --shared <req> <max> ------------------------------
242 // A DUAL-TARGET module cannot carry the LN33 statics -- nx_wasm_craft compiles natively as well as to
243 // wasm, and the native lane refuses a non-zero static initializer outright
244 // (G3_NONZERO_INIT_STATIC_UNSUPPORTED_BOTH_LANES) -- and it should not have to: the standing order is
245 // that a target's limit is a declared door on a ladder, never a constant in the source. So the same
246 // declaration is reachable from the BUILD LANE, on a module carrying no statics at all. The subject
247 // here is TG_FX_PLAIN, which is exactly that module.
248 let w_flag: *u8 = tg_path(dir, "fx_flag.wat" as *u8)
249 let rcf: i64 = tg_run5(cw, "--shared" as *u8, "3" as *u8, "8" as *u8, fx_plain, w_flag, out, outlen)
250 let fw: *u8 = sys_read_file(w_flag, lenp)
251 let fw_n: i64 = lenp[0]
252 gv_check("build-flag-declares-a-shared-memory-on-a-module-with-no-statics" as *u8, (rcf == 0) * tg_has(fw, fw_n, "(import \"env\" \"memory\" (memory 3 8 shared))" as *u8), ctr)
253 gv_check("build-flag-re-exports-the-imported-memory-under-the-old-name" as *u8, tg_has(fw, fw_n, "(export \"memory\" (memory 0))" as *u8), ctr)
254 // the scale-down door at the SAME declared size: one source, two artifacts, one shared and one not
255 let w_flagtwin: *u8 = tg_path(dir, "fx_flagtwin.wat" as *u8)
256 let rcft: i64 = tg_run5(cw, "--shared" as *u8, "3" as *u8, "8" as *u8, "--nothreads" as *u8, fx_plain, out, outlen)
257 gv_check("neg-control-nothreads-still-wins-over-the-shared-flag-and-keeps-the-declared-size" as *u8, (rcft == 0) * (1 - tg_has(out, outlen[0], "shared" as *u8)), ctr)
258 // REFUSALS, each by name rather than by a silently wrong size
259 let rcz: i64 = tg_run5(cw, "--shared" as *u8, "0" as *u8, "8" as *u8, fx_plain, w_flag, out, outlen)
260 gv_check("neg-control-a-zero-page-request-is-refused-by-name" as *u8, (rcz != 0) * tg_has(out, outlen[0], "req must be >= 1 page" as *u8), ctr)
261 let rcm: i64 = tg_run5(cw, "--shared" as *u8, "9" as *u8, "4" as *u8, fx_plain, w_flag, out, outlen)
262 gv_check("neg-control-a-maximum-below-the-request-is-refused-by-name" as *u8, (rcm != 0) * tg_has(out, outlen[0], "max must be >= req" as *u8), ctr)
263
264 // ---- 6. scale-down: the --nothreads twin of the shared module ------------------------------
265 let w_twin: *u8 = tg_path(dir, "fx_twin.wat" as *u8)
266 let rc7: i64 = tg_run(cw, "--nothreads" as *u8, fx_shared, w_twin, 0 as *u8, out, outlen)
267 let tw: *u8 = sys_read_file(w_twin, lenp)
268 let tw_n: i64 = lenp[0]
269 gv_check("nothreads-twin-emits-an-unshared-defined-memory-of-the-declared-size" as *u8, (rc7 == 0) * tg_has(tw, tw_n, "(memory (export \"memory\") 1)" as *u8), ctr)
270 gv_check("nothreads-twin-lowers-the-same-ops-to-plain-loads-and-stores" as *u8, (1 - tg_has(tw, tw_n, "atomic" as *u8)) * tg_has(tw, tw_n, "i64.load" as *u8), ctr)
271 let b_twin: *u8 = tg_path(dir, "fx_twin.wasm" as *u8)
272 let rc8: i64 = tg_run(wc, w_twin, b_twin, 0 as *u8, 0 as *u8, out, outlen)
273 let tb: *u8 = sys_read_file(b_twin, lenp)
274 let tb_n: i64 = lenp[0]
275 let tv: i64 = tg_vm_call2(tb, tb_n, "tick" as *u8, TG_CELL_A, TG_TICKS, 2, ok)
276 gv_check("nothreads-twin-compiles-and-ticks-1000-through-the-plain-twins" as *u8, (rc8 == 0) * (ok[0] == 1) * (tv == TG_TICKS), ctr)
277 let tcas: i64 = tg_vm_call2(tb, tb_n, "probe_cas" as *u8, TG_CELL_B, 0, 1, ok)
278 gv_check("nothreads-twin-cas-agrees-with-the-atomic-lowering-1009" as *u8, (ok[0] == 1) * (tcas == TG_EXP_CAS), ctr)
279 let tfx: i64 = tg_vm_call2(tb, tb_n, "probe_futex" as *u8, TG_CELL_B, 0, 1, ok)
280 gv_check("nothreads-twin-futex-is-the-historical-syscall-no-op-0" as *u8, (ok[0] == 1) * (tfx == TG_EXP_FUTEX_TWIN), ctr)
281 let tbig: i64 = tg_vm_call2(tb, tb_n, "probe_big" as *u8, TG_CELL_C, 0, 1, ok)
282 gv_check("nothreads-twin-faa-agrees-with-the-atomic-lowering-10000000003" as *u8, (ok[0] == 1) * (tbig == TG_EXP_BIG), ctr)
283
284 return gv_verdict("wasm_threads_gate" as *u8, ctr, "everything below the browser; the two-Worker shared-counter proof and its lost-update neg-control run on the CDP wire and are journaled on lang.plan LN33" as *u8)
285}