GrowThenWriteVector

A kernel that successfully grows linear memory mid-call and writes its result into the page that did not exist before the grow.

The payload is self-reporting, so the property can prove its own rig fired

"A grow happened" is not observable through us.tractat.kuilt.warp.Op — the result is bytes. So the kernel writes the result pointer into the result: the first four bytes are that pointer as a little-endian i32 (reportedPointer), followed by marker. The property asserts the reported pointer sits at or above memoryEndBeforeGrow, which is the difference between "this read came from newly-grown memory" and "this read happened to succeed" — and it is an honest self-report rather than a claim, because the host read those very bytes from that address.

The kernel also traps on a denied grow rather than falling through, so an engine that refuses the grow reds loudly instead of quietly reverting the vector to a plain in-bounds read.

What it cannot detect

It cannot distinguish an impl that re-fetches its memory handle from one that never cached a stale handle to begin with — both simply pass. This is a property about the observable contract, and "you must re-fetch" is an implementation strategy, not a contract term.

Nor can it tell whether a host re-read a correct size but a stale base that happened to still be valid, and that is measured rather than supposed: caching Wasm3WasmRuntime's base pointer across the grow leaves this property green, because m3 grew a 64 KiB arena to 128 KiB in place. A base that is still correct is indistinguishable from one that was re-fetched, so no property over us.tractat.kuilt.warp.Op closes it. What the vector does reach is every impl where the handle really is invalidated — a stale memory size on any of the three, and a detached ArrayBuffer in the browser — and each of those is a measured red.

Parameters