code wiki / _hdl_build / nx_wasm_fitfixture.nx

nx_wasm_fitfixture.nx source

↩ module page · 50 lines · 2925 B

1// nx_wasm_fitfixture.nx -- A DELIBERATELY BROKEN WASM MODULE. It exists to be REFUSED. 2// 3// WHY THIS FILE EXISTS. nx_wasm_vm_verify decides whether a shipped module's framebuffer lies inside 4// the linear memory it declares. On 2026-08-14 that verifier had a defect of its own: gv_verdict 5// tests ctr[2] (preconditions missing) BEFORE it compares passed-vs-run and returns 3/SKIP, so a 6// module that FAILED the fit check and then hit the frame-affordability abstention was reported as 7// "I could not look" instead of "this is broken". The one failure the tool was built to catch was the 8// one failure it could not report. A census reading exit codes would have scored it as an honest 9// abstention and gone green. 10// 11// A GREEN THAT NEVER HAD A CORRESPONDING RED IS UNVERIFIED, so the fix ships with the input that 12// must produce the RED. This module triggers BOTH conditions AT ONCE -- that simultaneity IS the 13// test, because either one alone is handled correctly even by the defective version: 14// * its framebuffer ends beyond the declared linear memory -> the fit check must FAIL 15// * its frame is far larger than the interpreter budget -> the abstention would otherwise fire 16// A verifier that reports SKIP on this file has the bug. A verifier that reports RED does not. 17// 18// ★THE OVERRUN IS DERIVED, NOT CHOSEN. FIX_OFF is computed so the framebuffer ends exactly ONE PIXEL 19// past the end of memory. A hand-picked "obviously too big" offset would prove only that a gross 20// violation is caught; the tightest possible violation is the one that says the boundary arithmetic 21// itself is right. It also means this fixture cannot silently stop being a violation if the page 22// count changes -- the relationship is expressed, not the number. 23// license_tier: ORIGINAL 24 25const FIX_PAGE_BYTES: i64 = 65536 26const FIX_PAGES: i64 = 192 27const FIX_MEM_BYTES: i64 = FIX_PAGES * FIX_PAGE_BYTES 28 29// A frame far above nx_wasm_vm_verify's interpreter budget, so the affordability abstention is 30// guaranteed to be reachable. These match craft's shipping geometry on purpose: the fixture should 31// look like the real thing it is standing in for. 32const FIX_W: i64 = 1200 33const FIX_H: i64 = 750 34const FIX_FB_BYTES: i64 = FIX_W * FIX_H * 8 35 36// One pixel (8 bytes) past the last byte that would fit. 37const FIX_OVERRUN_BYTES: i64 = 8 38const FIX_OFF: i64 = FIX_MEM_BYTES - FIX_FB_BYTES + FIX_OVERRUN_BYTES 39 40func ww() -> i64 { return FIX_W } 41func hh() -> i64 { return FIX_H } 42func fb_off() -> i64 { return FIX_OFF } 43 44// Never actually called by the verifier on this fixture -- the module is refuted before any frame is 45// attempted. It exists so the module presents a complete framebuffer surface (ww/hh/fb_off/render) 46// and is therefore JUDGED rather than skipped as NOT-A-RENDERER. A fixture that gets abstained on for 47// the wrong reason is not a test. 48func render() -> i64 { return 0 } 49 50func main() -> i64 { return 0 }