resultWindowPastMemoryEndIsBounded
A result window that is in range and past the end — an ordinary positive pointer addressing real linear memory, whose ptr + len leaves it — is bounds-rejected.
Why the three vectors above do not already cover this
They all fail the same way: bit 31 set. An implementation whose entire guard is if (word < 0) reject passes every one of them, and then reads 94 bytes past the end of linear memory on (resPtr = 65530, resLen = 100) — a benign-looking pair no fixture in WasmKernelFixtures could produce before this one. A bounds-check suite in which every out-of-bounds vector happens to set the sign bit cannot tell a real bounds check from a sign check, and this is a sandbox boundary: it is the thing that stops code another peer sent you from reaching memory it should not.
The in-range-past-end case is covered one layer down, by WarpAbiResultTest over requireInBounds in :kuilt-warp. That proves the shared decoder is correct; it does not prove any given runtime routes through it, which is precisely what every impl's KDoc promises ("never a hand-rolled unpack") with nothing behind it.
Three preconditions, then the claim. 1 neither ABI word has bit 31 set, so a sign-only guard cannot be what rejects this; 2 the pointer itself addresses real memory, so a guard that only clamps the pointer cannot be either; 3 the window really does leave memory. They run first, and a failure among them ends the test before the claim, because a claim about the wrong vector is not evidence. Then 4: the impl surfaces WasmExecutionException — a guest runtime fault, never an OOB host access and never a raw error escaping the sealed hierarchy.
1–3 are the fixture's own preconditions, restated here so a reader of the property can see what makes it different from its siblings; InRangePastEndVector makes a fixture that fails them unconstructible, and cross-checks all three against the module bytes.
Mutation receipts, measured on this branch — each applied alone, reverted, and read out of the results XML. Three backends: ChicoryWasmRuntimeConformanceTest (jvmTest), Wasm3WasmRuntimeConformanceTest (macosArm64Test), BrowserWasmRuntimeConformanceTest (wasmJsBrowserTest).
| Mutation | Reds here | Reds elsewhere |
|---|---|---|
The hand-rolled signed unpack every impl's KDoc forbids: requireInBounds narrows to Int and checks only the sign — :kuilt-warp | native RED; JVM green; browser unreachable | 1 of 9 WarpAbiResultTest. All three high-bit siblings stay green, on every backend |
The same defect in the browser's JS mirror — asUintN → asIntN, a sign check, and a clamping slice in place of the bounded view | browser RED | nothing: 19 of 20 green, siblings included |
Drop the range arm but keep the words unsigned (ptr < 0 \|\| len < 0) | native: the test binary crashed | 4 of 9 WarpAbiResultTest; crashed the native runner on allocPointerWithHighBitSetIsBounded |
Fixture: resultPointer back into the high-bit region | precondition, at construction | nothing |
Fixture: resultLength shrunk until the window fits | precondition, at construction | nothing |
Fixture: resultLength off by one from the module's own i64.const | the artefact cross-check, at construction | nothing |
Rows 1 and 2 are the finding, and together they are #2314 demonstrated rather than argued: on two of the three backends, an implementation that keeps a sign check and loses the range check passes every pre-existing out-of-bounds vector in this suite and reds only this one. On wasm3 the decode ends in raw pointer arithmetic (base[ptr + i] over m3_GetMemory), so InRangePastEndVector's window is read straight out of host memory and handed back; in the browser the clamping slice silently returns a short array where the bounded Uint8Array(buffer, ptr, len) view would have thrown.
The JVM cell is green, and that is worth saying out loud rather than leaving as an absence. Chicory's Memory API re-checks the narrowed index natively and throws, which ChicoryWasmRuntime wraps — so the guard is layered there and no mutation of the shared decoder alone reds this property on that backend. What it holds on the JVM is the contract term (the fault surfaces as WasmExecutionException, not a hang or a raw engine error); what it holds for the next implementation is everything, because a new backend inherits wasm3's shape — a raw memory view with no second opinion — far more often than Chicory's.
Row 3 is the clumsy neighbour of row 1 and is reported because its shape is the argument: dropping the range check while leaving the words unsigned lets a 0x8000_0000 alloc pointer through as a positive Long, and wasm3 writes there — the native test binary died rather than failing. It is not the mutation this property exists for, because it reds a sibling too; row 1 is the discriminating one.
The last three rows are the vacuity guards — the edits a fixture author commits by accident. All three fail at InRangePastEndVector's construction, before any assertion, and each names the relation it broke. The last of them is the one no relational check could catch: every number in the descriptor stays mutually consistent, and only the cross-check against the module's own constant notices that it is describing a vector nobody is running.