diff --git a/design/contracts/0018-check-codegen-boundary.md b/design/contracts/0018-check-codegen-boundary.md
index 6ee98b4..9938b99 100644
--- a/design/contracts/0018-check-codegen-boundary.md
+++ b/design/contracts/0018-check-codegen-boundary.md
@@ -5,7 +5,7 @@
 `check` produces a single elaborated, typed artefact — a
 [`MirWorkspace`](../../crates/ailang-mir/src/lib.rs) — that is **total**
 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
 a field MIR already carries; there is no recompute-or-guess fallback
 path.
@@ -55,6 +55,16 @@ Cross-module name resolution in particular is resolved **once**, in
 (the retraction recorded in [typeclasses](0013-typeclasses.md), §
 "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
 
 A codegen arm that recomputes a fact instead of reading it off MIR is