Static check + diagnostics: program memory footprint must fit the requested pages (no OOM)

[0xGeorgii]

Summary

Add a compile-time check, with meaningful diagnostics, that a program's total static memory footprint fits within the number of linear-memory pages it requests at startup — so the program can never need more memory than it declared, and can never OOM / hit a memory.grow failure at runtime.

Current state

For today's model this guarantee already holds, but only implicitly and via two independent hardcoded constants that merely happen to agree:

• Codegen declares linear memory as exactly 1 page (minimum: 1, maximum: Some(1)), never grows it, and there is no heap / no malloc — the shadow stack is the only consumer of linear memory.
• Analysis rule A036 (StackDepthExceeded) bounds the cumulative shadow-stack usage along the worst-case call chain to STACK_BUDGET_BYTES = 65_536 = exactly that one 64 KiB page.

So a program that passes A036 cannot OOM today. But the budget (65_536) and the declared page count (1) are unrelated constants in different crates; neither is derived from the other.

Proposal

Generalize A036 from a hardcoded, stack-only 64 KiB budget into a holistic, page-derived total-memory bound:

1. Derive the budget from the requested page count (see Compilation parameter: number of linear-memory pages to allocate (Inference.toml + CLI) #210) rather than hardcoding 64 KiB: budget = pages * 64 KiB.
2. Account for every linear-memory consumer, not just the shadow stack: the worst-case shadow stack plus future data sections, globals, and any future heap. Prove Σ(all static allocations) <= budget.
3. Emit a meaningful compile-time diagnostic when the footprint exceeds the requested pages — naming the contributing consumers (e.g. the worst-case call chain, the data-segment total) and the overflow amount, rather than letting the program trap at runtime.

This realizes Power of 10 Rule 3 (no dynamic allocation after initialization): the footprint is fully static, bounded, and checked.

Relationship

• Depends on / pairs with Compilation parameter: number of linear-memory pages to allocate (Inference.toml + CLI) #210 (the requested page count is the budget input).
• Generalizes existing rule A036 — must reuse, not duplicate, its call-graph + frame-size machinery (core/analysis/src/call_graph.rs, estimate_frame_sizes).
• Context: spun out of the array-bounds work in Array Bounds Checking #164 during a design discussion on memory safety.

Future work.