DeclaredLimitsVector

A complete, well-behaved warp kernel whose declared linear-memory limits are the whole point of the vector: nothing else about it can trip a load guard, so a property over it is reasoning about initialPages and maxPages alone.

What is checked here, and what is deliberately left to the property

The two page counts are claims about a byte literal, and a regenerated literal with a stale descriptor beside it is the defect one level up — so init reads the module's memory section and requires it to declare exactly these limits, with an explicit max (the encoder emits the limits flag 0x01, so a fixture that quietly lost its max is not a value this constructor can be handed, and the no-max rule is ruled out structurally rather than by assertion).

What is not checked here is every relation involving the sandbox cap — whether the initial is over it, whether the max is under it, whether either sits exactly on it. The cap is a us.tractat.kuilt.warp.WasmSandboxConfig value, not a property of the module, and a descriptor that hardcoded one would answer a question the property is supposed to ask of the config it actually runs under. Each property therefore asserts its own cap relations against the config it hands WasmRuntimeConformanceSuite.newRuntime, which is also what makes a change to the default cap red the affected properties instead of silently retargeting them.

Properties

Link copied to clipboard
Link copied to clipboard

the module's declared initial linear memory, in pages.

Link copied to clipboard

the module's declared max, in pages — always explicit.