loadRejectsOversizeInitialWhoseDeclaredMaxIsWithinTheCap

The oversize-initial arm, on the only input that can reach it.

Why no spec-valid module can isolate this guard

WebAssembly validates limits with min <= max. So in any valid module initial > cap forces max > cap when a max is declared, and forces the no-max rule when it is not: the initial arm is subsumed by its two neighbours, and every valid fixture that trips it trips one of them too. That is not a fixture-authoring mistake to be corrected — it is arithmetic, and it is why loadRejectsModuleWithNoMaxAndOversizeInitialMemory cannot attribute its rejection however carefully it is written.

So the vector is deliberately spec-invalid, and that is the case the guard is for

WasmKernelFixtures.INITIAL_ABOVE_DECLARED_MAX declares memory 32 16: an explicit max (no-max rule satisfied) sitting exactly at the cap (size-cap max arm satisfied) under an initial of 32. Of the sandbox's three memory rules only the initial one is broken. The whole reason a sandbox re-derives limits from the bytes is that it must not rest on the engine doing so, and this is the input on which those two differ.

The measurement, and why it makes this a tripwire rather than a live guard

No mutation of any shipped runtime reds this property, and that is stated first because an all-green cell read as an absence would be read as a gap. Deleting the initial > cap check from all three impls leaves all four backends green, because each engine refuses this module on its own and by a different mechanism:

• Chicory — Parser.parse throws "size minimum must not be greater than maximum";

• browser — WebAssembly.Module() throws "maximum memory size (16 pages) is less than initial (32 pages)";

• wasm3 — m3_ParseModule accepts min > max, and unmutated it is the sandbox's own guard that speaks ("module initial memory 32 pages exceeds sandbox cap 16 pages"); with the guard deleted, m3_LoadModule then fails to size the memory past the declared max ("runtime ran out of memory"). Two independent refusals, so still green.

So the oversize-initial guard is defence in depth on every engine shipped today: subsumed arithmetically for valid modules, and beaten to the punch by the engine for the one invalid shape that could reach it. What this property holds is the outcome — a spec-invalid limits pair is a terminal WasmLoadException, never a raw engine error escaping the sealed hierarchy, an input class no other vector here covers — and it reds the day a backend both accepts min > max and sizes the initial from it. A future engine is exactly where that is plausible; it is already true of one of the two wasm3 layers.

No message assertion, for the same measurement: the three mechanisms word themselves differently, and asserting "initial" would fail two conforming impls for checking limits earlier than the sandbox does. The three preconditions below say what the vector is, against the config actually used, so a drifted fixture or a changed default cap reds here instead of quietly retargeting the property.

Mutation receipts, measured on this branch — each applied alone and reverted, read out of the results XML, tasks confirmed EXECUTED. Backends: ChicoryWasmRuntimeConformanceTest (jvmTest), Wasm3WasmRuntimeConformanceTest (macosArm64Test and iosSimulatorArm64Test), BrowserWasmRuntimeConformanceTest (wasmJsBrowserTest).

Row 1 is why this KDoc leads with the measurement. Row 2 is the honest limit of the property: an off-by-one that widens the guard is invisible here, and only the boundary-acceptance vector notices — the two together pin the threshold from both sides, and neither does alone.