loadAcceptsInitialMemoryExactlyAtTheCap
The size-cap rule's boundary, from below: a module declaring memory 16 16 under a 16-page cap is entirely legal and must load and run.
Why the happy path does not already cover this
WasmKernelFixtures.REVERSE declares 1 16. Its max sits on the boundary, so an impl that wrote max >= cap reds every happy-path property here — but its initial is 1, sixteen pages clear of the edge, so initial >= cap is invisible to the entire suite. The two arms of one rule are not symmetric in what the existing vectors pin, and this is the missing half: the only vector whose initial touches the cap.
It asserts a completed round trip rather than merely that load did not throw. On the browser the guest is instantiated lazily in a worker at first invoke, so a property that stopped at load would never allocate the 16 pages it is nominally about; the kernel's warp_run returns a zero-length window, so the round trip is the smallest thing that proves the module was really stood up at the cap.
What it cannot detect: anything about rejection. A backend that deleted the initial guard outright passes this happily — that direction belongs to loadRejectsOversizeInitialWhoseDeclaredMaxIsWithinTheCap, and the two together are what pin the threshold from both sides.
Mutation receipts, backends as above.
| Mutation | Reds here | Reds elsewhere |
|---|---|---|
initial > cap → initial >= cap — all three runtimes | RED on all four backends, and the red is the escaping "module initial memory 16 pages exceeds sandbox cap 16 pages" — the guard naming itself and both numbers | nothing: the sole failure of 22, 22, 22 and 41 |
Drop initial > cap entirely — all three | green, correctly — this property is about over-rejection | see the sibling's table |
Fixture: vector regenerated at 1 16 | precondition 1, before the claim | nothing |
Row 2 is green on purpose and is the reason the pair exists: this property cannot see a guard that has been deleted, and its sibling cannot see one that has been widened.