Module-scope constants and a static memory footprint check (A058) by 0xGeorgii · Pull Request #515 · Inferara/inference

0xGeorgii · 2026-10-04T08:29:39Z

Closes #211. This PR also includes the follow-up work: extending the footprint check to data sections. That required a real data producer, so it adds module-scope const.

Why

An Inference program allocates nothing at run time. Its linear memory holds only what is sized before it runs: the shadow stack, plus any data the module carries above it. A036 already proves the deepest call chain fits the stack. Nothing proved that the stack and the data together fit the declared pages, and the one data producer the language wants, module constants, was refused outright by A032. The heap stays out of scope on purpose, because it is hard to verify.

What changes

Language and type checker

Module-scope const (pub or private) can be read from any function, method or spec: bare, through an item import, or by qualified path.
Every initializer is evaluated once at compile time, using the program's own arithmetic:
- checked + - * and negation, plus wrapping(...)
- division and remainder, including the trapping cases
- shifts, which require a count below the type's width
- bitwise and comparison operators, and short-circuit &&/||
- member and index access
- array, repeated-array and struct literals
Two new errors:
- NonConstantInitializer for a call or @.
- ConstEvaluationFailed for an operation that would trap at run time, reported at that operation.
Every compound constant that some body reads is placed in a StaticData region, in source order and at its natural alignment.
A write to an imported constant is now refused. It used to be accepted silently.

Memory layout (inference-compiler-interface)

MemoryLayout::with_static_data places the data region directly above the stack:
- If the build didn't set a stack size, the default 64 KiB stack shrinks by exactly what the data needs (rounded to 16 bytes). A program with constant tables still builds in the default page.
- If the build requested a stack size, it is kept, and it must leave room for the data. Otherwise you get StaticDataError.
request_to_fit computes the smallest layout that holds a given stack and data size.

Analysis

Breaking: AnalysisOptions now takes layout: MemoryLayout instead of stack_budget_bytes. Analysis measures against the same placed layout that codegen emits. The CLI, infs and the language server pass their layout through.
New rule A058 (StaticDataExceedsMemory):
- Fires when the stack plus the data needs more than pages.
- Anchored at the first constant that doesn't fit, and lists the constants largest first.
- Suggests more pages, or a smaller stack when the deepest call chain allows one.
A036 now:
- lists each frame on the chain
- says how many bytes it is over
- says where the stack size came from: requested, the default, or the default minus the data
- names the smallest layout that fits
Together, A036 and A058 prove a program never needs more memory than it declares (Power of 10, Rule 3).
A032 now refuses only a const inside a spec.
A046, A053 and A054 now examine initializers the same way they examine bodies.
A031 accepts a constant as a compound return value.
The range analysis behind A056 reads an integer constant as its value.

Codegen, linker and translation

A scalar constant is emitted as an immediate.
A read of a compound constant is i32.const <address>, so indexing, field access, copies, arguments and sret returns lower unchanged.
One active data segment at i32.const <stack size> holds all the compound constants. No DataCount section is emitted, because SpaceWasm can't decode one. A program without compound constants is byte-identical to before.
The linker now keeps the main module's active data segments instead of refusing them (first commit).
The Rocq translation reads a constant in a spec as its computed value, and the .v carries the segment as MD_active.
Codegen without analysis now reports a frame larger than the stack as an error instead of panicking.
A parenthesized array initializer (let mut b = (a);) is now copied instead of aliased.

Tests

Type checker: evaluation, refusals and layout (tests/src/type_checker/module_consts.rs).
Runtime: 14 tests at both instruction levels (tests/src/codegen/wasm/module_consts.rs), covering:
- scalar and compound reads
- nested and cross-file constants
- sret returns
- data placement
- growable memory
A058: tests that follow each finding's suggested fix and re-analyze to show it clears (rules_a058.rs). The A032/A036 tests and neighbouring rule tests are updated.
Goldens and corpus rows:
- codegen and bulk-memory goldens
- SpaceWasm conformance, panic-free and stock-validity rows
- a Rocq corpus row plus a committed .v golden, with an assertion that at least one corpus module carries MD_active
Stellar: a contract that reads a constant table.
End to end: infc (4 tests), infs (3) and the language server (1 A058 test).

Full workspace run: 8298 passed, 3 failed. The 3 failures are the infs permission tests (*_permission_denied, build_fails_on_readonly_output_directory). They fail only because the container runs as root, and pass otherwise.

Notes for review

Rocq: coqc isn't installed in the environment where this was developed, so the new .v golden with a non-empty mod_datas hasn't been elaborated locally. CI's Rocq lane is the first check that ValidModule holds for a module with a data segment.
wasmtime CLI: it isn't installed locally either, so the infs run end-to-end test was skipped here. It runs in CI.
Formatting: the code that changes in the touched files is formatted. Untouched code that rustfmt would already change at main was left as is, to keep the diff readable.

🤖 Generated with Claude Code

https://claude.ai/code/session_01JQx2CSSMvBPmy8TfiHDM2d

Generated by Claude Code

Confidence Score: 5/5

The PR appears safe to merge based on the changes since the previous review; no outstanding findings were identified.

_{Reviews (4) · Last reviewed commit: "test(hassert): pin how constants of each..."}

The compiler is about to place module-scope compound constants in linear memory above the shadow stack, initialized by one active data segment over memory 0 at an `i32.const` offset. The merge rebuilt the main module section by section and emitted no Data section, so it refused any main module carrying a segment rather than drop it; with that refusal in place, a program with module constants could not link an external at all. `ParsedModule` now records each segment in `data_segments` (kind, memory index, a lone-`i32.const` offset or `Unsupported`, owned bytes) beside the existing `data_count`. `Plan::build` admits a main-side segment when it is active, over memory 0, at a lone `i32.const` offset, and refuses a passive segment, a segment over another memory, or any other offset expression with an `UnsupportedConstruct` naming the segment and the problem. `emit` writes the admitted segments in a Data section right after Code, and nothing at all for a data-free module, so that output is byte-identical to before. No DataCount section is ever written: SpaceWasm cannot decode section id 12. Carrying a segment unchanged is correct because no data index moves (the main-body re-encoder now refuses `memory.init`/`data.drop`, which would also demand a DataCount section, and an external closure using either is Tier C), no offset moves (main's memory stays memory 0), and the reconciled memory's minimum only widens from main's. External modules' data segments stay Tier C, unchanged. The provenance and README docs now say the data region above the stack holds module constants, and why a Tier-B external cannot be handed it through a declared path: A047 refuses a compound argument to a `mut` external parameter unless it is rooted at a `mut` binding, which a `const` is not. Tests: the M-2 rejection test becomes a preservation test (offset and bytes survive, no DataCount section, and the linked module reads the constant under wasmtime), joined by an ordering test in a widened memory, a data-free test, and refusals for a passive segment, memory 1, an extended-constant offset, and a main body using `data.drop`. The M-2 probe and fuzz seed are now positive controls, with a passive-segment probe and seed (M-2b) taking over the rejection. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JQx2CSSMvBPmy8TfiHDM2d

An Inference program allocates nothing at run time, so its linear memory holds exactly what is sized before it runs: the shadow stack, and above it whatever data the module carries. A036 proved the deepest call chain fits the stack, but nothing proved the stack and the data together fit the pages the module declares, and the only data producer the language wanted -- module-scope constants -- was refused outright by A032. Module-scope `const` now works. The type checker resolves a constant read anywhere (bare, item-imported, or path-qualified) to its definition, and computes every module constant once under the program's own arithmetic: literals, enum variants, other constants, the arithmetic, bitwise, shift and comparison operators, short-circuit `&&`/`||`, `checked`/`wrapping`, member and index access, and array, repeated-array and struct literals. An initializer that is not a constant expression (a call, `@`) is refused as `NonConstantInitializer`; one whose operation would trap if the program ran it (a checked overflow, a division by zero, `MIN / -1`, a shift by the width or more, an index past the end) as `ConstEvaluationFailed`, at that operation. A write to a constant is refused however it is named; an item-imported constant used to accept one silently. A scalar constant is an immediate at every use. Every array or struct constant some body reads is laid out in source order at its natural alignment (`StaticData`) and written by one active data segment at `i32.const <stack size>`, directly above the stack; a read is `i32.const <address>` where a binding's would be `local.get`, so indexing, field access, copies, arguments and sret returns lower unchanged. No DataCount section is emitted, since SpaceWasm cannot decode one. A program with no compound module constant emits exactly the bytes it did before. `MemoryLayout::with_static_data` places the data: a stack the build did not size keeps 64 KiB when the memory has room and otherwise gives up what the data needs, rounded to 16 bytes, so a program with constant tables builds in the default page; a requested stack is kept and must leave the data its room. `AnalysisOptions` now carries the build's `MemoryLayout` instead of a bare stack budget, so analysis measures the program against the same placed layout code generation emits. New rule A058 (StaticDataExceedsMemory) refuses a stack and data that need more than the pages, anchored at the first constant that does not fit, naming the constants largest first, and offering more pages or, when the deepest chain allows, a smaller stack. A036 now itemizes the chain, says where the stack's size comes from (requested, the default page, or the default less the constant data), and names the smallest layout that holds the chain. Together they prove a program never needs more memory than it declares (Power of 10, Rule 3). A032 narrows to a `const` inside a `spec`; A046/A053/A054 examine initializers as they do bodies; A031 accepts a constant as a compound return value; the range analysis behind A056 reads an integer constant as its value. The proof-mode translation reads a constant in a specification as its computed value, and the .v carries the segment as MD_active. The CLI, infs and the language server pass their layout through. Code generation driven without analysis reports a frame larger than the stack as an error rather than panicking, and a parenthesized array initializer is copied rather than aliased. Tests: type-checker evaluation and layout tests; 14 runtime tests at both instruction levels covering scalar and compound reads, nested and cross-file constants, sret returns and the data placement; A058 tests that follow each finding's help and re-analyze; updated A032/A036 and neighbouring rule tests; codegen and bulk-memory goldens; SpaceWasm conformance, panic-free, stock-validity and Rocq corpus rows plus a committed .v golden; a Stellar contract reading a constant table; and end-to-end tests through infc, infs and the language server. Closes #211. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JQx2CSSMvBPmy8TfiHDM2d

The Static Analysis chapter gains "Static memory footprint", describing A036 and A058 together as the proof that a program never needs more memory than it declares, with an example of each finding, and its rule table counts A058 and the narrowed A032. The Memory Allocation chapter gains "Module Constants and the Static Data Region" and shows the data segment in its layout diagram and section table. The language-server and compilation-targets chapters, the infs manifest reference, and the analysis, codegen, inference and ide READMEs describe module constants, the data region above the stack, and `AnalysisOptions::layout`. The changelog records the feature, the API changes and the fixes under #211. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01JQx2CSSMvBPmy8TfiHDM2d

codecov · 2026-10-04T08:37:33Z

Codecov Report

❌ Patch coverage is 95.02398% with 83 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
core/type-checker/src/module_consts.rs	94.63%	28 Missing ⚠️
core/wasm-codegen/src/compiler.rs	78.00%	22 Missing ⚠️
core/type-checker/src/errors.rs	47.22%	19 Missing ⚠️
core/wasm-codegen/src/hassert/translate.rs	94.54%	6 Missing ⚠️
core/type-checker/src/symbol_table.rs	90.90%	3 Missing ⚠️
core/analysis/src/range.rs	80.00%	2 Missing ⚠️
core/analysis/src/errors.rs	99.64%	1 Missing ⚠️
core/analysis/src/rules/static_data_footprint.rs	97.61%	1 Missing ⚠️
...ysis/src/rules/unsupported_compound_return_expr.rs	93.75%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!

… sweep The bounds-elision sweep meters fuel, and a new store holds none until the first call sets it. Wasmtime writes an active data segment at instantiation with metered code unless the memory is mapped from a copy-on-write image, which it builds from an in-memory module only on Linux. module_consts.inf is the first corpus program with a data segment, so on macOS and Windows instantiating it ran out of fuel and corpus_builds_with_and_without_proven_guards_agree panicked, while the Linux job passed. Running::new now gives the store fuel before it instantiates. The test's engine also turns copy-on-write images off, so a Linux run initializes memory the way the other hosts do and catches this on every runner. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Co-Authored-By: Paperclip <noreply@paperclip.ing>

…t count The module documentation listed a shift count past the width among the operations that would trap at run time. The emitted shift does not trap: it takes its count modulo the width. It is the constant evaluator that refuses a count that is negative or at or past the width, because such a count is always a mistake. The note also sent readers to A043 (reserved export names); the literal shift-count check is A044. The shift test now also pins the negative `>>` count the note describes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Co-Authored-By: Paperclip <noreply@paperclip.ing>

A specification that read one element of a module constant, such as `TABLE[0]`, first expanded the whole constant into a value tree: a `[0; N]` table became N cloned leaves before the access chain picked one. Nothing checked the size. A constant compared whole, or split by a non-constant index, also skipped the 64-leaf budget that aggregate literals are held to. A non-constant index into a million-element table built a million-case definition, which overflowed the stack. An access chain over a module constant now takes its constant steps (constant indices and field names) inside the computed value, so `TABLE[999999]`, `GRID[1][2]` or `HOLDER.xs[3]` reaches its one element without building any other. Whatever is still an array or a struct when it becomes a value tree is counted against the leaf budget first, from a count read off the value (a repeated element is not visited per copy). A constant past the budget is refused with P013 before anything is built. A scalar costs nothing, as it already did in term position. A constant written as an element of a literal is not counted again, since the literal's own introduction already counts its leaves. Tests: one-element reads of three million-leaf constants translate at a full budget; a constant index past the end is P014; a non-constant index into a 65-element constant and a whole-value comparison past the budget are P013; a small constant still splits and compares leafwise; and a constant inside a literal fills the budget exactly once. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Co-Authored-By: Paperclip <noreply@paperclip.ing>

Covers the module-constant paths the previous commit added that no test reached yet: a `bool` and an enum constant read as their values, a struct constant compared whole as one equality per field, and an array constant named where a term is required, which is the aggregate-is-not- a-term P004 an aggregate binding gets. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Co-Authored-By: Paperclip <noreply@paperclip.ing>

claude added 3 commits October 4, 2026 07:57

greptile-apps Bot reviewed Oct 4, 2026

View reviewed changes

Comment thread core/wasm-codegen/src/hassert/translate.rs

Comment thread core/type-checker/src/module_consts.rs

Comment thread core/type-checker/src/module_consts.rs Outdated

0xGeorgii self-assigned this Oct 4, 2026

0xGeorgii added the ci:real-rocq Run the real-library Rocq type-check on this PR (needs a configured wasm-verifier runner) label Oct 4, 2026

0xGeorgii deployed to real-rocq October 4, 2026 09:32 — with GitHub Actions Active

claude and others added 2 commits October 4, 2026 10:41

0xGeorgii deployed to real-rocq October 4, 2026 10:41 — with GitHub Actions Active

0xGeorgii deployed to real-rocq October 4, 2026 10:58 — with GitHub Actions Active

0xGeorgii added codegen Bytecode emitting static analysis Static code analysis memory management Related to how memory is tracked and manipulated labels Oct 10, 2026

0xGeorgii requested a deployment to real-rocq October 10, 2026 23:21 — with GitHub Actions Waiting

Navigation Menu

Repository navigation

Module-scope constants and a static memory footprint check (A058) - #515

Module-scope constants and a static memory footprint check (A058)#515
0xGeorgii wants to merge 7 commits into
mainfrom
claude/stoic-fermat-0przdx

0xGeorgii commented Oct 4, 2026 •

edited by greptile-apps Bot

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

codecov Bot commented Oct 4, 2026 •

edited

Loading

Uh oh!

This branch is waiting to be deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

0xGeorgii commented Oct 4, 2026 • edited by greptile-apps Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Why

What changes

Tests

Notes for review

Confidence Score: 5/5

Uh oh!

Uh oh!

Uh oh!

Uh oh!

codecov Bot commented Oct 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

This branch is waiting to be deployed

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

0xGeorgii commented Oct 4, 2026 •

edited by greptile-apps Bot

Loading

codecov Bot commented Oct 4, 2026 •

edited

Loading