Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

docs(design): name the fn-value resolution carve-out in 0018

Browse Source 
Audit follow-up (typed-MIR milestone-close drift review, clean). The
boundary contract said codegen does "no callee resolution"; that is true
for App callees — the only thing `Callee` totality claims over — but
`resolve_top_level_fn` still resolves a dotted fn used as a *value* via
`import_map` (the in-corpus-unreachable type-home residue the spec
blessed at mir.2), and ctor/const resolution stay codegen-side. Tighten
the prose to "no App-callee resolution" and name the value-position
carve-out, so the contract is precise and a future drift review does not
read the blanket claim as violated. Prose-only; no code, no test change.
This commit is contained in:
Brummel
2026-06-01 01:39:30 +02:00
parent a378dad0aa
commit bd62f2b9d0
1 changed files with 11 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
design/contracts/0018-check-codegen-boundary.md
+11 -1
View File
@@ -5,7 +5,7 @@
`check` produces a single elaborated, typed artefact — a `check` produces a single elaborated, typed artefact — a
[`MirWorkspace`](../../crates/ailang-mir/src/lib.rs) — that is **total** [`MirWorkspace`](../../crates/ailang-mir/src/lib.rs) — that is **total**
over every fact codegen needs. Codegen consumes that artefact and over every fact codegen needs. Codegen consumes that artefact and
**re-derives nothing**: it performs no type synthesis, no callee **re-derives nothing**: it performs no type synthesis, no App-callee
resolution, no uniqueness inference. Every decision codegen makes reads resolution, no uniqueness inference. Every decision codegen makes reads
a field MIR already carries; there is no recompute-or-guess fallback a field MIR already carries; there is no recompute-or-guess fallback
path. path.
@@ -55,6 +55,16 @@ Cross-module name resolution in particular is resolved **once**, in
(the retraction recorded in [typeclasses](0013-typeclasses.md), § (the retraction recorded in [typeclasses](0013-typeclasses.md), §
"Cross-module references in synthesised bodies", invariant 2). "Cross-module references in synthesised bodies", invariant 2).
The totality claim is over **`App` callees**: every `App` carries a
resolved `Callee`, so codegen never walks a callee ladder to find a call
target. One value-position residue remains and is deliberately not MIR's
job — `resolve_top_level_fn` resolves a dotted fn used as a *value* (not
an `App` callee) through the module's `import_map`. That path is
unreachable for type-scoped names in the current corpus (the type-home
residue blessed in `docs/specs/0060-typed-mir.md`, mir.2 refinement);
ctor and const resolution likewise stay codegen-side. None of these is
callee resolution, so `Callee` totality is intact.
### Failure mode this contract names ### Failure mode this contract names
A codegen arm that recomputes a fact instead of reading it off MIR is A codegen arm that recomputes a fact instead of reading it off MIR is