1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
//! Core MIR — executable middle-end (0.24 epic #252).
//!
//! Sits **after** the existing frontend / normalization pipeline and
//! **before** every runtime backend. Same role for execution that
//! [`proof_ir`](crate::ir::proof_ir) plays for proof export: a single
//! canonical IR that every consumer reads instead of re-deriving
//! semantics from `ResolvedExpr` shape.
//!
//! ```text
//! AST → frontend / normalization → Typed Resolved HIR
//! ↓
//! +---------+
//! | MIR | (this module)
//! +---------+
//! ↓
//! VM / Rust / wasm-gc / wasip2
//! ```
//!
//! # Scope (0.24)
//!
//! Phase 1 of #252 (this commit) is **doc-only** — module skeleton,
//! pinned design decisions, and the RFC in `RFC.md` next to this
//! file. No types yet, no lowering, no consumer. Phase 2 lands the
//! data model + dump, Phase 3 lands HIR → MIR lowering in widening
//! waves, Phase 4 wires the VM as the first vertical-slice
//! consumer.
//!
//! # Decisions pinned before any lowering lands
//!
//! - **`Try` stays a node, not desugared.** `let x = step()?` lowers
//! to a `Try` MIR node; backends pick the final shape. Rust will
//! eventually emit `?` native; the VM emits a tag check + early
//! return. This is the concrete fix for the lesson from
//! [stage 8b of #232][shape8b] where the post-pipeline AST had
//! already collapsed `?` to nested match, forcing the
//! `ResultPipelineChain` recognizer to smuggle the step list
//! through a side-channel on `ModulePattern`.
//! - **`match` stays structured.** Flattening to terminator-style
//! basic blocks is a separate later step (Flat MIR / LIR), not
//! Phase 1–4.
//! - **Identity is typed.** MIR refers to user declarations via
//! `FnId` / `TypeId` / `CtorId` / `ModuleId` — never by string.
//! `SymbolTable` is an input.
//! - **ProofIR is separate.** MIR answers "what does this program
//! execute"; ProofIR answers "what does this program prove". They
//! don't merge.
//! - **No flag-day backend rewrite.** Phase 4 migrates the VM only.
//! Other backends consume HIR until their own slice ships in
//! later releases.
//!
//! [shape8b]: https://github.com/jasisz/aver/pull/245
//!
//! # Inputs / outputs (Phase 1 contract)
//!
//! Input: `ResolvedProgramView` + `SymbolTable` produced by the
//! existing pipeline. No new frontend.
//!
//! Output: `MirProgram` keyed by `FnId`. Backends consume via
//! `mir_program.fn_by_id(id)`. Per-fn body shape is documented in
//! `RFC.md` and made concrete in Phase 2.
//!
//! # Out of scope for the 0.24 epic
//!
//! - Phase 5 (Rust / wasm-gc / wasip2 migration) — later releases.
//! - Phase 6 (DCE / inliner / monomorphization / SRoA / effect
//! scheduling) — same.
//! - Moving `interp_lower` / `buffer_build` / `escape` to MIR —
//! only on a per-pass concrete-win basis, not as a 0.24
//! deliverable.
//! - Try-auto proof harness (#222 second half) — independent
//! track.
//!
//! See `RFC.md` next to this file for the full design write-up,
//! open questions, and the per-phase checklist.
pub use crateBuiltinCtor;
pub use ;
pub use ;
pub use ;
pub use bare_i64;
pub use ;
pub use ;
pub use ;