resultWrittenIntoNewlyGrownMemoryIsReadBack
A guest that successfully grows linear memory mid-call and writes its result into the new region gets those exact bytes back.
Why a suite of refusals needs one success
Every other loadable vector either never calls memory.grow or grows past its declared max and traps (growPastDeclaredMaxTraps), so no property here has ever asked an implementation to notice that the bound moved. A suite that only drives refusals is satisfied by an implementation that refuses everything — and more to the point, the failure a legitimate grow provokes is silent corruption, not an exception: a ByteBuffer whose backing store moved on the JVM, a detached ArrayBuffer in the browser, a base pointer from m3_GetMemory that a realloc invalidated on wasm3. All three shipped impls re-fetch after the guest call and each says so in a comment; nothing held them to it.
So this property asserts content, not absence of an exception. A host reading through a stale handle either throws (which reds) or hands back other bytes (which also reds).
How it proves its own rig fired
"A grow happened" is not observable through us.tractat.kuilt.warp.Op — the result is bytes — and a vector that quietly stopped growing would still return something, in bounds, and pass. The kernel therefore writes the result pointer into the first four bytes of its own result, and assertion 3 demands that pointer sit at or above the pre-grow memory end. It is a self-report rather than a claim because the host read those bytes from that address. The kernel also traps on a denied grow instead of falling through, so an engine that refuses the grow reds rather than reverting this vector to a plain in-bounds read.
Four assertions: 1 the result is the size the kernel promises; 2 the marker bytes survive the round trip — the content claim; 3 the result was written at or above the pre-grow memory end — the rig-fired claim; 4 and within the grown memory, so the self-report is a real address rather than an arbitrary number.
Mutation receipts, measured on this branch — each applied alone and reverted. Backends as above.
| Mutation | Reds here | Reds elsewhere |
|---|---|---|
Bound the result against the memory size read before the guest call — ChicoryWasmRuntime.runAbi | RED: window [65536, 65544) outside [0, 65536) escapes invoke | nothing else in jvmTest |
The same on native — Wasm3WasmRuntime.runAbi | RED, same window | nothing else in macosArm64Test |
Cache exports.memory.buffer before warp_run — BrowserWasmRuntime's worker | RED: "Cannot perform Construct on a detached ArrayBuffer" | nothing else in wasmJsBrowserTest |
Cache the linear-memory base pointer before the guest call — Wasm3WasmRuntime.runAbi | green | nothing |
| Fixture: write the result at offset 0 instead of into the new page | assertion 3 only — "0 against 65536" | nothing |
The first three rows are the property earning its place: each is the exact mechanism that backend's own comment says it avoids, and before this vector existed each was held by the comment alone. The browser row is the one to read twice — the detached-ArrayBuffer message is the failure mode named in BrowserWasmRuntime's KDoc, arriving as a real red.
Row 4 is green, and it is the more interesting measurement. Caching wasm3's base pointer across the grow — the stale-base bug Wasm3WasmRuntime.memoryBaseFor's KDoc exists to prevent — changes nothing, because m3 grew a 64 KiB arena to 128 KiB in place and the cached pointer stayed valid. So this property does not pin that half of the contract on that backend, and no property expressible over us.tractat.kuilt.warp.Op could: a base that is still correct is indistinguishable from a base that was re-fetched. It is stated here rather than left for a reader to assume the green row proves something. See GrowThenWriteVector.
Row 5 is the vacuity guard, and the one that matters day to day: it is the fixture edit that turns this back into an ordinary round-trip property, and assertion 3 is the only thing that notices.