Issue #761: Lowering in phases: collect each file’s facts once, then infer, then check and emit as reads (maintainability and #727)

Open and answer this issue on GitHub.

performance, decision · opened 2026-10-20 · updated 2026-11-03 · 1 comment

What this is about

Lowering a file runs the checker’s walk over the same syntax tree twice, with different settings:

1. The ledger pass (check_for_the_ledger, crates/nikaia/src/contracts/mod.rs) runs before the ledger is finished. Its consumers read only methods and stored_code. Since #727 it skips prove, views, view_changes and the tether check.
2. Then the ledger’s columns are inferred (sync::infer, throws::infer, keep inference, write_result_sources).
3. The file check (project::check) walks again, against the finished ledger. Some of its rules read the finished columns, for example traits::check reads sync.

The emitter then needs facts of that check (propagation, keep plans, bounds). buffer_plans runs twice, against two different ledgers.

Cost today (cold nikaia lower --no-cache crates/rs2nika/convert/src/main.nika, benches/lowering/lower.sh, 3 096 M Ir in all):

Step	Ir
check::walked, both walks	1 111 M
of that, the ledger walk	390 M
infer_package_noted	735 M
keep::buffer_plans, twice	217 M

Why the question arises: maintainability

To get under a third of the cost, #727 added reuse shortcuts that apply only under a condition:

• the emitter takes the check’s facts only when the check asked exactly what propagation_against asks: no modules, no changed contract, the promised ledger equal to program.contracts;
• it takes the check’s keep plans only when the check’s library is std_ledger() alone;
• the trust join reuses the ledger pass only for one group of own files with std alone;
• lower-std passes the facts on only when no described name is also a std name.

Each of these is a quiet coupling between two places. Today the output is byte for byte the same. But a change to one side can make the other differ without any test noticing, and whoever adds a rule has to know which of the two walks sees which state of the ledger. Merging the two walks as they are would make this worse: checking would then run against a half-finished ledger.

Proposal

Split lowering into phases with a clear contract. Each phase only reads what the phases before it wrote, and what it writes is frozen when it ends.

• A. Facts: one walk per file collects what typing needs (resolved calls and methods, stored_code, the types of locals and expressions). It reads no inferred column.
• B. Inference: sync, throws, keeps and result sources are computed as fixpoints over the facts and the call graph, not by walking the tree again.
• C. Judgements and emitting: the check’s rules and the emitter are reads over the facts and the finished ledger. buffer_plans and prove run once.

What this gains for maintainability:

• one walk instead of two;
• the order the steps depend on is in the shape of the program, not hidden behind conditions;
• the reuse shortcuts above go away, because there is only one result left to reuse;
• a new rule is a new read in C and does not touch the walk.

What it gains elsewhere:

• frozen facts can be shared between threads instead of cloned per file;
• reading the interner during a read phase can work without a lock (see the issue on writes during read phases and the interner’s thread safety);
• each phase or file has a lifetime its memory can live in as a block (#490).

Performance (estimated, not measured): the second walk goes, and so do one buffer_plans and the conditional reuses. Probably 15–25 % of today’s cost.

Risks

• The core assumption is not checked yet: that typing (A) reads no inferred column. If it reads, say, throws for ?, that part has to move into B or stay iterative. Step 1 checks this before anything is built.
• Diagnostics have to come out in the same order and with the same text as before.
• It is a large rework of check (Rust and tools/check_*.nika).
• Open question for the owner: the emitter plans buffers against std alone, the check against std plus described crates. With one plan, one of the two has to decide.

To build

1. Inventory. For every read of a ledger column in check::walked and its callees, record whether it is needed for typing (A) or only for a rule (C). Result: the list of reads that stand in A’s way. Decide here whether to go on.
2. Introduce UnitFacts as the result of one walk. The ledger pass reads methods and stored_code from it, and the second walk reads its facts from it. Output byte for byte the same (lower.sh all), all tests green.
3. Make the rules reads in C, over UnitFacts and the finished ledger, and remove the second walk.
4. Run buffer_plans and prove once, after the owner has answered the std-versus-described question.
5. Remove the reuse shortcuts. Until then, a check mode that recomputes every reused result and compares it, on in the tests.
6. Measure with benches/lowering/lower.sh and record the result in #727.

Comments

keywan-ghadami, 2026-11-03

Owner, 2026-11-03: this is the target architecture: collect the facts first, then run every later phase on them. The timing is not decided yet.

Until then, a new design should not add hidden or swapped state that this split would have to undo. Context passes as data, as #1123 decided (D).

Still open before building: step 1’s inventory, and the question of whether buffers are planned against std alone or against std plus the described crates.

---

Generated by Claude Code

Back to Open Issues