InRangePastEndVector

A kernel whose warp_run returns a result window that is in range and past the end: both ABI words are ordinary small positive numbers, the pointer addresses real linear memory, and only ptr + len crosses the memory end.

Why this takes the geometry rather than a boolean

The claim "this window is past the end" is a relation between three numbers — the pointer, the length and the live memory size — and a fixture carrying it as an answer can be handed the wrong one. So the descriptor takes the inputs (declaredPages, resultPointer, resultLength) and derives the relation in init; a vector that has drifted into the siblings' high-bit region, or whose window no longer leaves memory, is not a value this constructor can be handed.

What is checked against the artefact, and what is not

The three numbers are claims about a byte literal, and a regenerated literal with a stale descriptor beside it is the same defect one level up. init therefore also reads the module: it requires the memory section to declare exactly declaredPages as both min and max, and the i64.const the kernel returns to be exactly (resultPointer shl 32) or resultLength.

What that still cannot see is whether warp_run returns that constant rather than merely containing it — a kernel could push it and drop it. Nothing short of executing the module settles that, and executing it is what the property does: an impl that rejects the window proves the constant reached the host decoder.

Parameters