diff --git a/crates/rue-air/src/inst.rs b/crates/rue-air/src/inst.rs
index 5d4ebf79c..eb0132266 100644
--- a/crates/rue-air/src/inst.rs
+++ b/crates/rue-air/src/inst.rs
@@ -32,6 +32,21 @@ use rue_span::Span;
 #[cfg(any(test, feature = "fuzz-support"))]
 mod payload_support;
 
+/// The published ceiling on AIR instructions in **one function body**
+/// (spec Appendix C.6:1).
+///
+/// Unlike the RIR instruction ceiling, which counts one shared per-program
+/// array, every function body owns a private AIR instruction array addressed by
+/// its own [`AirRef`] — a `u32`. The array's length is narrowed to `u32` at the
+/// payload-staging boundary (`Air::reserve_instruction`), so a body holds at
+/// most this many instructions and the last `u32` index is left unused rather
+/// than making the count itself unrepresentable.
+///
+/// Exceeding the ceiling is a diagnosable compile-time failure (spec C.1:2),
+/// surfaced as `E1401` at the semantic AIR boundary ([`Air::finish`]) — never a
+/// truncated `AirRef` that aliases instruction 0 onto instruction 2^32.
+pub const MAX_AIR_INSTRUCTIONS_PER_BODY: u32 = u32::MAX;
+
 /// Structured failure returned by checked AIR payload decoding.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub struct AirPayloadError {
@@ -137,17 +152,51 @@ impl From<AirBuildError> for rue_error::CompileError {
     }
 }
 
+/// Why an AIR owner was refused at its publication boundary.
+///
+/// The boundary reports two unrelated things. A structural inconsistency is a
+/// producer bug and stays an internal compiler error; running past a published
+/// implementation limit is a diagnosable compile-time failure that must name
+/// the limit (spec C.1:2), so it needs its own typed channel out of
+/// [`Air::finish`] rather than collapsing into `E9000`.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum AirValidationErrorKind {
+    /// The owner does not satisfy AIR's structural invariants (`E9000`).
+    Structural,
+    /// Construction ran past a published implementation limit
+    /// (spec Appendix C.6:1). Reported as `E1401` naming the limit.
+    ResourceLimit,
+}
+
 #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct AirValidationError {
     pub instruction: Option<usize>,
     pub reason: String,
+    pub kind: AirValidationErrorKind,
+}
+
+impl AirValidationError {
+    /// Whether this rejection is an implementation-limit failure (spec C.1:2)
+    /// rather than a producer bug. Consumers use it to pick `E1401` over an
+    /// internal-error code.
+    pub fn is_resource_limit(&self) -> bool {
+        matches!(self.kind, AirValidationErrorKind::ResourceLimit)
+    }
 }
 
 impl fmt::Display for AirValidationError {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        match self.instruction {
-            Some(index) => write!(f, "invalid AIR instruction {index}: {}", self.reason),
-            None => write!(f, "invalid AIR: {}", self.reason),
+        // A limit rejection already reads as a user-facing sentence naming the
+        // exceeded ceiling; the "invalid AIR" prefix belongs only to the
+        // structural (compiler-bug) channel.
+        match (self.kind, self.instruction) {
+            (AirValidationErrorKind::ResourceLimit, _) => f.write_str(&self.reason),
+            (AirValidationErrorKind::Structural, Some(index)) => {
+                write!(f, "invalid AIR instruction {index}: {}", self.reason)
+            }
+            (AirValidationErrorKind::Structural, None) => {
+                write!(f, "invalid AIR: {}", self.reason)
+            }
         }
     }
 }
@@ -156,9 +205,15 @@ impl std::error::Error for AirValidationError {}
 
 impl From<AirValidationError> for rue_error::CompileError {
     fn from(error: AirValidationError) -> Self {
-        rue_error::CompileError::without_span(rue_error::ErrorKind::InternalError(
-            error.to_string(),
-        ))
+        let kind = match error.kind {
+            AirValidationErrorKind::ResourceLimit => {
+                rue_error::ErrorKind::CompilerResourceLimit(error.to_string())
+            }
+            AirValidationErrorKind::Structural => {
+                rue_error::ErrorKind::InternalError(error.to_string())
+            }
+        };
+        rue_error::CompileError::without_span(kind)
     }
 }
 
@@ -1019,6 +1074,17 @@ pub struct Air {
     /// so the binder aliases an element the collection still owns and drops —
     /// dropping the binder too would double-free (RUE-259).
     borrow_slots: Vec<u32>,
+    /// Set once [`Air::push_inst`] was asked for an instruction beyond the
+    /// published per-body ceiling ([`MAX_AIR_INSTRUCTIONS_PER_BODY`],
+    /// spec Appendix C.6:1).
+    ///
+    /// `push_inst` runs from every non-payload lowering site in semantic
+    /// analysis and returns a bare `AirRef`, so the ceiling cannot be reported
+    /// by threading a `Result` back through all of them. The owner records the
+    /// rejection here, stops growing, and [`Air::finish`] converts the record
+    /// into the `E1401` diagnostic spec C.1:2 requires instead of handing back
+    /// an index truncated by `len() as u32`.
+    instruction_limit_exceeded: bool,
     #[cfg(test)]
     place_reserve_failure: Option<PlaceReserveFailure>,
 }
@@ -1328,9 +1394,17 @@ impl ValidatedAir {
 
 impl Air {
     fn finish(self, context: AirValidationContext<'_>) -> Result<ValidatedAir, AirValidationError> {
+        // Report the published per-body instruction ceiling first: a latched
+        // owner holds a truncated reference graph, so every structural finding
+        // downstream would be a consequence of the limit rather than a producer
+        // bug, and spec C.1:2 wants the limit named (E1401), not an E9000.
+        if let Some(error) = self.latched_capacity_error() {
+            return Err(error);
+        }
         let fail = |instruction, reason| AirValidationError {
             instruction,
             reason,
+            kind: AirValidationErrorKind::Structural,
         };
         let type_cache = std::cell::RefCell::new(([Type::UNIT; 64], 0usize));
         let validate_type = |ty| -> Result<(), String> {
@@ -2294,6 +2368,7 @@ impl Air {
             places: Vec::new(),
             param_drops: Vec::new(),
             borrow_slots: Vec::new(),
+            instruction_limit_exceeded: false,
             #[cfg(test)]
             place_reserve_failure: None,
         }
@@ -2332,13 +2407,26 @@ impl Air {
         self.push_inst(inst)
     }
 
+    /// Preflight one instruction slot for a payload-bearing owner builder.
+    ///
+    /// Payload builders are already fallible, so they reject the published
+    /// per-body ceiling directly instead of relying on `push_inst`'s latch. The
+    /// admissible indices are `0..MAX_AIR_INSTRUCTIONS_PER_BODY`, which is
+    /// exactly the range `push_inst` will accept.
     fn reserve_instruction(&mut self, family: &'static str) -> Result<(), AirBuildError> {
-        u32::try_from(self.instructions.len()).map_err(|_| AirBuildError {
-            phase: "AIR",
-            family,
-            operation: "insert instruction",
-            kind: AirBuildErrorKind::ResourceLimit,
-        })?;
+        let over_limit = match u32::try_from(self.instructions.len()) {
+            Ok(index) => index == MAX_AIR_INSTRUCTIONS_PER_BODY,
+            Err(_) => true,
+        };
+        if over_limit {
+            self.instruction_limit_exceeded = true;
+            return Err(AirBuildError {
+                phase: "AIR",
+                family,
+                operation: "insert instruction",
+                kind: AirBuildErrorKind::ResourceLimit,
+            });
+        }
         self.instructions.try_reserve(1).map_err(|_| AirBuildError {
             phase: "AIR",
             family,
@@ -2368,12 +2456,46 @@ impl Air {
         Ok(())
     }
 
+    /// Append an instruction and return its reference.
+    ///
+    /// An `AirRef` is a `u32` index into this body's instruction array, so a
+    /// body holds at most [`MAX_AIR_INSTRUCTIONS_PER_BODY`] instructions.
+    /// Beyond that the reference is not representable: `len() as u32` would
+    /// wrap instruction 2^32 onto instruction 0 and silently alias two
+    /// distinct values, which spec C.1:2 forbids. This method has no fallible
+    /// callers, so it latches [`Air::instruction_limit_exceeded`] and hands
+    /// back an already-valid reference; [`Air::finish`] turns the latch into an
+    /// `E1401` diagnostic before the body is published.
     fn push_inst(&mut self, inst: AirInst) -> AirRef {
+        let over_limit = match u32::try_from(self.instructions.len()) {
+            Ok(index) => index == MAX_AIR_INSTRUCTIONS_PER_BODY,
+            Err(_) => true,
+        };
+        if over_limit {
+            self.instruction_limit_exceeded = true;
+            // The array is full, so index 0 is always a live instruction.
+            return AirRef::from_raw(0);
+        }
         let index = self.instructions.len() as u32;
         self.instructions.push(inst);
         AirRef::from_raw(index)
     }
 
+    /// The implementation-limit rejection latched during construction, if this
+    /// body ran past the published per-body instruction ceiling. Checked at the
+    /// publication boundary ([`Air::finish`]).
+    fn latched_capacity_error(&self) -> Option<AirValidationError> {
+        self.instruction_limit_exceeded.then(|| AirValidationError {
+            instruction: None,
+            reason: format!(
+                "this function body has more AIR instructions than the implementation limit \
+                     of {MAX_AIR_INSTRUCTIONS_PER_BODY} per body — an AIR instruction reference \
+                     is a u32 index into one body's instruction array (spec Appendix C.6:1)"
+            ),
+            kind: AirValidationErrorKind::ResourceLimit,
+        })
+    }
+
     /// Get an instruction by reference.
     #[inline]
     pub fn get(&self, inst_ref: AirRef) -> &AirInst {
@@ -3814,6 +3936,76 @@ impl Air {
     }
 }
 
+#[cfg(test)]
+mod resource_limit_tests {
+    use super::*;
+
+    #[test]
+    fn published_air_body_ceiling_matches_the_addressable_reference_space() {
+        // Spec Appendix C.6:1: an `AirRef` is a u32 index into one body's own
+        // instruction array, and the array length is narrowed to u32 at the
+        // payload-staging boundary, so the count itself stays representable.
+        assert_eq!(MAX_AIR_INSTRUCTIONS_PER_BODY, u32::MAX);
+        assert_eq!(u64::from(MAX_AIR_INSTRUCTIONS_PER_BODY), 4_294_967_295);
+    }
+
+    #[test]
+    fn ordinary_air_owner_never_latches_the_body_ceiling() {
+        let pool = TypeInternPool::new().freeze();
+        let mut editor = AirEditor::new(Type::UNIT);
+        editor.add_unit(Span::new(0, 0));
+        assert!(editor.air.latched_capacity_error().is_none());
+        assert!(
+            editor
+                .finish(AirValidationContext::Canonical(&pool))
+                .is_ok()
+        );
+    }
+
+    #[test]
+    fn a_latched_body_is_refused_with_a_diagnostic_naming_the_limit() {
+        // RUE-1226 / spec C.1:2: `push_inst` is infallible, so the per-body
+        // ceiling is latched during lowering and reported here, naming the
+        // limit, rather than truncating `len() as u32` onto instruction 0.
+        let pool = TypeInternPool::new().freeze();
+        let mut editor = AirEditor::new(Type::UNIT);
+        editor.add_unit(Span::new(0, 0));
+        editor.air.instruction_limit_exceeded = true;
+
+        let error = editor
+            .finish(AirValidationContext::Canonical(&pool))
+            .unwrap_err();
+        assert!(error.is_resource_limit());
+        assert!(error.to_string().contains("4294967295"));
+        assert!(error.to_string().contains("spec Appendix C.6:1"));
+        assert!(!error.to_string().contains("invalid AIR"));
+    }
+
+    #[test]
+    fn air_boundary_failures_are_classified_apart_from_internal_errors() {
+        let limit = AirValidationError {
+            instruction: None,
+            reason: "over the ceiling".to_string(),
+            kind: AirValidationErrorKind::ResourceLimit,
+        };
+        let structural = AirValidationError {
+            instruction: Some(3),
+            reason: "bad operand".to_string(),
+            kind: AirValidationErrorKind::Structural,
+        };
+        assert!(limit.is_resource_limit());
+        assert!(!structural.is_resource_limit());
+        assert_eq!(
+            rue_error::CompileError::from(limit).kind.code(),
+            rue_error::ErrorCode::COMPILER_RESOURCE_LIMIT
+        );
+        assert_eq!(
+            rue_error::CompileError::from(structural).kind.code(),
+            rue_error::ErrorCode::INTERNAL_ERROR
+        );
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use std::sync::Arc;
diff --git a/crates/rue-air/src/intern_pool.rs b/crates/rue-air/src/intern_pool.rs
index bb27a20cc..08656fded 100644
--- a/crates/rue-air/src/intern_pool.rs
+++ b/crates/rue-air/src/intern_pool.rs
@@ -28,7 +28,7 @@
 
 use std::collections::{HashMap, HashSet};
 use std::ops::Deref;
-use std::sync::{Arc, PoisonError, RwLock};
+use std::sync::{Arc, LazyLock, PoisonError, RwLock};
 
 use lasso::Spur;
 use rue_span::FileId;
@@ -610,11 +610,60 @@ struct TypeInternPoolInner {
 /// 8-bit kind tag and a 24-bit type-pool index (spec Appendix C.6:1).
 pub const MAX_COMPOSITE_TYPES: u32 = type_encoding::MAX_PAYLOAD + 1;
 
+/// The user-facing text for a compilation refused by the composite-type
+/// ceiling (spec Appendix C.6:1, under the C.1:2 policy).
+///
+/// Shared so that the declaration-binding boundary — which stops the
+/// compilation as soon as the latch is visible — and the per-body CFG boundary
+/// that backstops it name the same limit in the same words.
+pub fn composite_type_limit_message() -> String {
+    format!(
+        "this compilation defines more distinct composite types (structs, enums, arrays, \
+         pointers, modules) than the implementation limit of {MAX_COMPOSITE_TYPES} — a live type \
+         handle is a u32 holding an 8-bit kind tag and a 24-bit type-pool index (spec Appendix \
+         C.6:1)"
+    )
+}
+
 fn checked_pool_index(index: usize) -> Option<u32> {
     let index = u32::try_from(index).ok()?;
     (index <= type_encoding::MAX_PAYLOAD).then_some(index)
 }
 
+/// The struct definition read back for a handle that the composite-type
+/// capacity latch aliased onto an entry of a different kind, and only for such
+/// a handle (see [`TypeInternPoolInner::next_pool_index`]).
+///
+/// The compilation this pool belongs to is already failing with `E1401` and
+/// nothing built from the pool will be published, so the read only has to be
+/// answerable without aborting (spec C.1:2). A field-less, drop-less,
+/// non-linear struct is the answer that keeps every dependent walk — ABI slot
+/// counting, containment, layout — finite and free of further aliased reads.
+static ALIASED_STRUCT_DEF: LazyLock<StructDefEntry> = LazyLock::new(|| {
+    StructDefEntry::new(StructDef {
+        name: Arc::from("<type-pool capacity exceeded>"),
+        fields: Vec::new(),
+        is_copy: false,
+        is_linear: false,
+        destructor: None,
+        is_builtin: false,
+        is_pub: false,
+        file_id: FileId::DEFAULT,
+    })
+});
+
+/// The enum counterpart of [`ALIASED_STRUCT_DEF`]. A variant-less enum has no
+/// payload to walk and no discriminant to widen.
+static ALIASED_ENUM_DEF: LazyLock<EnumDefEntry> = LazyLock::new(|| {
+    EnumDefEntry::new(EnumDef {
+        name: Arc::from("<type-pool capacity exceeded>"),
+        variants: Arc::from([] as [Arc<str>; 0]),
+        variant_payloads: Vec::new(),
+        is_pub: false,
+        file_id: FileId::DEFAULT,
+    })
+});
+
 /// Round `offset` up to the next multiple of `align` (a power of two, always at
 /// least 1). Saturating so an already-oversized aggregate cannot wrap; the slot
 /// budget guard (`MAX_TYPE_SLOTS`) rejects genuinely oversized types earlier.
@@ -935,6 +984,23 @@ impl TypeInternPoolInner {
     /// pool read in range; the public accessors additionally re-check the kind
     /// tag against the entry, so an aliased handle degrades to `None` rather
     /// than to a mistyped entry.
+    ///
+    /// # The latch window
+    ///
+    /// The latch is set inside declaration collection, type resolution, or
+    /// specialization, and the diagnostic is reported at the declaration-binding
+    /// boundary (with the per-body CFG query as a backstop for a universe that
+    /// latches later). Registration continues in between (spec C.1:2 forbids an
+    /// abort), so aliased handles are *read* inside that window — most
+    /// immediately by `incremental_facts`, which walks the field types of the
+    /// very entry being registered, and then by every layout, ABI, and
+    /// containment query the remaining declarations trigger. An aliased handle
+    /// carries the kind tag its registration asked for while the entry it names
+    /// keeps the kind it was created with, so the `&`-returning definition
+    /// accessors below cannot assert the two agree; inside the window they
+    /// degrade to an empty definition of the requested kind
+    /// ([`ALIASED_STRUCT_DEF`], [`ALIASED_ENUM_DEF`]) instead of panicking. A
+    /// kind mismatch with no latch is still a producer bug and still panics.
     fn next_pool_index(&mut self) -> u32 {
         match checked_pool_index(self.entry_count()) {
             Some(index) => index,
@@ -1275,8 +1341,14 @@ impl TypeInternPoolInner {
     }
 
     fn struct_def(&self, id: StructId) -> &StructDefEntry {
-        self.try_struct_def(id)
-            .unwrap_or_else(|| panic!("Expected struct at pool index {}", id.0))
+        match self.try_struct_def(id) {
+            Some(def) => def,
+            // Only a capacity-latched pool can hand out a struct handle that
+            // names a non-struct entry; see `next_pool_index`. Anywhere else a
+            // kind mismatch is a producer bug and must stay loud.
+            None if self.capacity_exceeded() => &ALIASED_STRUCT_DEF,
+            None => panic!("Expected struct at pool index {}", id.0),
+        }
     }
 
     fn struct_def_mut(&mut self, id: StructId) -> &mut StructDef {
@@ -1328,13 +1400,22 @@ impl TypeInternPoolInner {
     }
 
     fn enum_def(&self, id: EnumId) -> &EnumDefEntry {
-        self.try_enum_def(id)
-            .unwrap_or_else(|| panic!("Expected enum at pool index {}", id.0))
+        match self.try_enum_def(id) {
+            Some(def) => def,
+            // See `struct_def`: an aliased handle is only possible inside the
+            // capacity-latch window.
+            None if self.capacity_exceeded() => &ALIASED_ENUM_DEF,
+            None => panic!("Expected enum at pool index {}", id.0),
+        }
     }
 
     fn array_def(&self, id: ArrayTypeId) -> (Type, u64) {
         match self.data(id.0) {
             TypeData::Array { element, len } => (*element, *len),
+            // See `struct_def`: inside the capacity-latch window an array
+            // handle can name an entry of another kind. A zero-length array of
+            // the error type terminates every dependent walk.
+            _ if self.capacity_exceeded() => (Type::ERROR, 0),
             other => panic!("Expected array at pool index {}, got {:?}", id.0, other),
         }
     }
@@ -1349,6 +1430,9 @@ impl TypeInternPoolInner {
     fn ptr_const_def(&self, id: PtrConstTypeId) -> Type {
         match self.data(id.pool_index()) {
             TypeData::PtrConst { pointee } => *pointee,
+            // See `struct_def`: aliasing is confined to the capacity-latch
+            // window, and the error type terminates the pointee walk.
+            _ if self.capacity_exceeded() => Type::ERROR,
             other => panic!(
                 "Expected ptr const at pool index {}, got {:?}",
                 id.pool_index(),
@@ -1360,6 +1444,8 @@ impl TypeInternPoolInner {
     fn ptr_mut_def(&self, id: PtrMutTypeId) -> Type {
         match self.data(id.pool_index()) {
             TypeData::PtrMut { pointee } => *pointee,
+            // See `ptr_const_def`.
+            _ if self.capacity_exceeded() => Type::ERROR,
             other => panic!(
                 "Expected ptr mut at pool index {}, got {:?}",
                 id.pool_index(),
@@ -2763,12 +2849,16 @@ impl TypeInternPool {
     ///
     /// # Panics
     ///
-    /// Panics if the StructId doesn't correspond to a struct in the pool.
+    /// Panics if the StructId doesn't correspond to a struct in the pool —
+    /// unless the composite-type capacity latch has aliased handles onto the
+    /// final entry, in which case the read degrades to an empty definition
+    /// while the compilation fails with `E1401` (spec C.1:2).
     #[track_caller]
     pub fn struct_def(&self, struct_id: StructId) -> Arc<StructDefEntry> {
         let inner = self.inner.read().unwrap_or_else(PoisonError::into_inner);
         match inner.try_struct_def_arc(struct_id) {
             Some(def) => Arc::clone(def),
+            None if inner.capacity_exceeded() => Arc::new(ALIASED_STRUCT_DEF.clone()),
             None => panic!("Expected complete struct at pool index {}", struct_id.0),
         }
     }
@@ -2894,12 +2984,14 @@ impl TypeInternPool {
     ///
     /// # Panics
     ///
-    /// Panics if the EnumId doesn't correspond to an enum in the pool.
+    /// Panics if the EnumId doesn't correspond to an enum in the pool — with
+    /// the same capacity-latch exemption as [`Self::struct_def`].
     #[track_caller]
     pub fn enum_def(&self, enum_id: EnumId) -> Arc<EnumDefEntry> {
         let inner = self.inner.read().unwrap_or_else(PoisonError::into_inner);
         match inner.try_enum_def_arc(enum_id) {
             Some(def) => Arc::clone(def),
+            None if inner.capacity_exceeded() => Arc::new(ALIASED_ENUM_DEF.clone()),
             None => panic!("Expected complete enum at pool index {}", enum_id.0),
         }
     }
@@ -2995,6 +3087,14 @@ impl TypeInternPool {
             "destructor symbol must end with .__drop"
         );
         let mut inner = self.inner.write().unwrap_or_else(PoisonError::into_inner);
+        // A capacity-latched pool aliases later registrations onto the final
+        // entry, so `struct_id` need not name a complete struct and the
+        // assertions below would be checking someone else's definition. The
+        // compilation is already failing with `E1401`; skip the metadata
+        // finalization instead of aborting (spec C.1:2).
+        if inner.capacity_exceeded() {
+            return;
+        }
         let def = inner.struct_def_mut(struct_id);
         assert!(!def.is_copy, "a copy struct cannot acquire a destructor");
         assert!(
@@ -3016,6 +3116,11 @@ impl TypeInternPool {
             "destructor symbol must end with .__drop"
         );
         let mut inner = self.inner.write().unwrap_or_else(PoisonError::into_inner);
+        // See `set_struct_destructor`: inside the capacity-latch window the
+        // handle need not name the struct this call means.
+        if inner.capacity_exceeded() {
+            return;
+        }
         let destructor = inner
             .struct_def_mut(struct_id)
             .destructor
@@ -3757,6 +3862,98 @@ mod tests {
         assert!(!pool.freeze().capacity_exceeded());
     }
 
+    /// Drive the pool into the state `next_pool_index` reaches once the
+    /// composite-type ceiling is exhausted, without materializing 2^24 entries.
+    fn latch_composite_type_ceiling(pool: &TypeInternPool) {
+        pool.inner
+            .write()
+            .unwrap_or_else(PoisonError::into_inner)
+            .capacity_exceeded = true;
+    }
+
+    #[test]
+    fn latched_pool_degrades_wrong_kind_definition_reads_instead_of_aborting() {
+        // RUE-1226 / spec C.1:2: between the capacity latch and the boundary
+        // that reports E1401, registrations alias the final entry, so a handle
+        // can carry a kind tag the entry it names does not have. Reading one
+        // must not abort the compiler.
+        let interner = ThreadedRodeo::default();
+        let pool = TypeInternPool::new();
+        let (struct_id, _) = pool.register_struct(
+            interner.get_or_intern("Owner"),
+            struct_def(
+                "Owner",
+                vec![StructField {
+                    name: "value".into(),
+                    ty: Type::I32,
+                }],
+            ),
+        );
+        latch_composite_type_ceiling(&pool);
+
+        let aliased_enum = EnumId::from_pool_index(struct_id.pool_index());
+        assert_eq!(pool.enum_def(aliased_enum).variant_count(), 0);
+
+        let frozen = pool.freeze();
+        assert!(frozen.capacity_exceeded());
+        assert_eq!(frozen.enum_def(aliased_enum).variant_count(), 0);
+        assert_eq!(frozen.struct_def(struct_id).fields.len(), 1);
+        // Every other `&`-returning definition accessor degrades the same way,
+        // so a containment or ABI walk that meets an aliased handle terminates.
+        assert_eq!(
+            frozen.array_def(ArrayTypeId::from_pool_index(struct_id.pool_index())),
+            (Type::ERROR, 0)
+        );
+        assert_eq!(
+            frozen.ptr_const_def(PtrConstTypeId::from_pool_index(struct_id.pool_index())),
+            Type::ERROR
+        );
+        assert_eq!(
+            frozen.ptr_mut_def(PtrMutTypeId::from_pool_index(struct_id.pool_index())),
+            Type::ERROR
+        );
+        // The aliased enum is walkable: no payload, no further aliased reads,
+        // so an ABI or containment walk that meets it terminates rather than
+        // recursing into a mistyped entry.
+        assert_eq!(frozen.inner.abi_slot_count(Type::new_enum(aliased_enum)), 1);
+        // The validating, backend-facing entry points still refuse the aliased
+        // handle. They are not reached in a latched compilation: declaration
+        // binding stops it, and the per-body CFG query backstops that before it
+        // projects domains or queries layouts.
+        assert_eq!(
+            frozen
+                .inner
+                .validate_complete_type(Type::new_enum(aliased_enum)),
+            Err(TypeValidationError::KindMismatch)
+        );
+    }
+
+    #[test]
+    #[should_panic(expected = "Expected complete enum at pool index")]
+    fn a_wrong_kind_handle_without_the_latch_is_still_a_producer_bug() {
+        // The degradation above is scoped to the latch window; a kind mismatch
+        // in a healthy pool stays loud, so the ICE surface does not grow.
+        let interner = ThreadedRodeo::default();
+        let pool = TypeInternPool::new();
+        let (struct_id, _) =
+            pool.register_struct(interner.get_or_intern("Owner"), struct_def("Owner", vec![]));
+        let _ = pool.enum_def(EnumId::from_pool_index(struct_id.pool_index()));
+    }
+
+    #[test]
+    fn latched_pool_skips_destructor_metadata_finalization() {
+        // `set_struct_destructor` asserts against the definition it finds, but
+        // inside the latch window the handle need not name it. The compilation
+        // is already failing with E1401; the finalization is skipped instead.
+        let interner = ThreadedRodeo::default();
+        let pool = TypeInternPool::new();
+        let (struct_id, _) =
+            pool.register_struct(interner.get_or_intern("Owner"), struct_def("Owner", vec![]));
+        latch_composite_type_ceiling(&pool);
+        pool.set_struct_destructor(struct_id, "Owner.__drop".to_string());
+        assert!(pool.struct_def(struct_id).destructor.is_none());
+    }
+
     #[test]
     fn checked_pool_index_enforces_type_payload_capacity() {
         let maximum = type_encoding::MAX_PAYLOAD as usize;
diff --git a/crates/rue-air/src/lib.rs b/crates/rue-air/src/lib.rs
index b331563dd..66849a51b 100644
--- a/crates/rue-air/src/lib.rs
+++ b/crates/rue-air/src/lib.rs
@@ -58,11 +58,12 @@ pub use inst::{
     AirEnumPayload, AirInst, AirInstData, AirIntrinsicArgs, AirMatchArms, AirParamMode, AirPattern,
     AirPayloadError, AirPayloadStorageStats, AirPlace, AirPlaceBase, AirPlaceRef, AirProjection,
     AirRef, AirSourceOrder, AirStructFields, AirTypeArgs, AirValidationContext, AirValidationError,
-    ValidatedAir,
+    AirValidationErrorKind, MAX_AIR_INSTRUCTIONS_PER_BODY, ValidatedAir,
 };
 pub use intern_pool::{
     EnumData, EnumDefEntry, FrozenTypeInternPool, MAX_COMPOSITE_TYPES, StructData, StructDefEntry,
     TypeData, TypeInternPool, TypeInternPoolStats, TypeValidationError,
+    composite_type_limit_message,
 };
 pub use layout::{Layout, LayoutKind, PaddingRange, SLOT_BYTES};
 pub use module_registry::ModuleRegistry;
diff --git a/crates/rue-cfg/src/build.rs b/crates/rue-cfg/src/build.rs
index 8ab72ad4b..58b678c46 100644
--- a/crates/rue-cfg/src/build.rs
+++ b/crates/rue-cfg/src/build.rs
@@ -616,14 +616,27 @@ impl<'a> CfgBuilder<'a> {
         let source_param_abi = derive_source_param_abi(&builder);
         builder.cfg.set_source_param_abi(source_param_abi);
 
-        let cfg = match builder.cfg.finish(builder.type_pool) {
-            Ok(cfg) => Some(cfg),
-            Err(error) => {
-                builder.errors.push(CompileError::new(
-                    ErrorKind::InternalError(error.to_string()),
-                    rue_span::Span::default(),
-                ));
-                None
+        // Report the published per-function block/value ceiling before
+        // verification: a latched graph holds identities that were handed back
+        // instead of allocated, so every structural finding downstream is a
+        // consequence of the limit rather than a producer bug. Spec C.1:2 wants
+        // the limit named (E1401), not the E9000 the verifier would raise.
+        let cfg = if let Some(error) = builder.cfg.latched_capacity_error() {
+            builder.errors.push(CompileError::new(
+                error.error_kind("CFG construction failed"),
+                rue_span::Span::default(),
+            ));
+            None
+        } else {
+            match builder.cfg.finish(builder.type_pool) {
+                Ok(cfg) => Some(cfg),
+                Err(error) => {
+                    builder.errors.push(CompileError::new(
+                        ErrorKind::InternalError(error.to_string()),
+                        rue_span::Span::default(),
+                    ));
+                    None
+                }
             }
         };
         CfgOutput {
diff --git a/crates/rue-cfg/src/inst.rs b/crates/rue-cfg/src/inst.rs
index 95981f1ee..b9d7c4244 100644
--- a/crates/rue-cfg/src/inst.rs
+++ b/crates/rue-cfg/src/inst.rs
@@ -747,6 +747,16 @@ pub struct Cfg {
     /// the AIR keeps a durable/imported body — which rebuilds its CFG from the
     /// same AIR — identical to its freshly analyzed counterpart.
     source_param_abi: Vec<rue_air::SourceParamAbi>,
+    /// The family ("basic blocks" / "values") whose per-function ceiling
+    /// ([`MAX_CFG_ENTITIES_PER_FUNCTION`], spec Appendix C.6:1) a
+    /// [`Cfg::new_block`] or [`Cfg::add_inst`] call ran past, if any.
+    ///
+    /// Both owner-index allocators are infallible and are called from hundreds
+    /// of construction and optimization sites, so the ceiling is recorded here
+    /// and reported once at the construction and optimization boundaries rather
+    /// than wrapping `len() as u32` onto an existing identity. Spec C.1:2
+    /// requires a diagnostic (`E1401`), not a wrapped index.
+    capacity_exceeded: Option<&'static str>,
 }
 
 #[derive(Debug, Clone, Copy, Default, PartialEq, Eq)]
@@ -780,6 +790,9 @@ pub enum CfgEditError {
     },
     /// A payload cannot be represented by the compact `u32` range format.
     ResourceLimitExceeded { family: &'static str },
+    /// One function's block or value arena ran past the published per-function
+    /// ceiling, so its next `u32` identity is not representable.
+    OwnerLimitExceeded { family: &'static str },
     /// Reserving storage failed without changing the CFG.
     CapacityFailure { family: &'static str },
 }
@@ -789,6 +802,32 @@ pub enum CfgEditError {
 /// holds at most this many CFG payload words (spec Appendix C.6:1).
 pub const MAX_CFG_PAYLOAD_WORDS_PER_PROGRAM: u32 = u32::MAX;
 
+/// The published per-function ceiling on CFG basic blocks and CFG values
+/// (spec Appendix C.6:1).
+///
+/// A [`BlockId`] and a [`CfgValue`] are `u32` indices into the arenas of **one**
+/// function's graph, and both arena lengths are narrowed to `u32` by graph
+/// traversal and domain projection, so a function holds at most this many of
+/// each. Exceeding either is a diagnosable compile-time failure (spec C.1:2),
+/// surfaced as `E1401` at the CFG construction and optimization boundaries.
+///
+/// This ceiling is *checked*, not argued unreachable: CFG entities are not a
+/// small constant multiple of the RIR instructions that produce them. Drop
+/// elaboration re-emits one drop (and, for a path-dependent move, a flag-guard
+/// block) per live slot at **every** exit, so a body with `N` droppable
+/// bindings and `M` `return` statements lowers to on the order of `N * M`
+/// values and blocks — quadratic, from a body that is linear in its source. See
+/// spec C.6:5 for the arithmetic that disproves the unreachability hypothesis.
+pub const MAX_CFG_ENTITIES_PER_FUNCTION: u32 = u32::MAX;
+
+/// The `u32` identity the next block or value in a per-function arena of
+/// `length` entries will take, or `None` once the published per-function
+/// ceiling leaves no representable identity.
+fn checked_owner_index(length: usize) -> Option<u32> {
+    let index = u32::try_from(length).ok()?;
+    (index < MAX_CFG_ENTITIES_PER_FUNCTION).then_some(index)
+}
+
 impl fmt::Display for CfgEditError {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
@@ -801,6 +840,11 @@ impl fmt::Display for CfgEditError {
                  {MAX_CFG_PAYLOAD_WORDS_PER_PROGRAM} payload words per program \
                  (spec Appendix C.6:1)"
             ),
+            Self::OwnerLimitExceeded { family } => write!(
+                f,
+                "this function's CFG has more {family} than the implementation limit of \
+                 {MAX_CFG_ENTITIES_PER_FUNCTION} per function (spec Appendix C.6:1)"
+            ),
             Self::CapacityFailure { family } => {
                 write!(f, "could not reserve storage for CFG {family} payload")
             }
@@ -821,7 +865,7 @@ impl CfgEditError {
     /// `E1402`; only a malformed builder request remains an ICE.
     pub fn error_kind(&self, context: &str) -> rue_error::ErrorKind {
         match self {
-            Self::ResourceLimitExceeded { .. } => {
+            Self::ResourceLimitExceeded { .. } | Self::OwnerLimitExceeded { .. } => {
                 rue_error::ErrorKind::CompilerResourceLimit(self.to_string())
             }
             Self::CapacityFailure { .. } => {
@@ -954,6 +998,7 @@ impl Clone for Cfg {
             address_taken_slots: self.address_taken_slots.clone(),
             address_taken_params: self.address_taken_params.clone(),
             source_param_abi: self.source_param_abi.clone(),
+            capacity_exceeded: self.capacity_exceeded,
         }
     }
 }
@@ -1260,6 +1305,7 @@ impl Cfg {
             address_taken_slots: std::collections::HashSet::new(),
             address_taken_params: std::collections::HashSet::new(),
             source_param_abi: Vec::new(),
+            capacity_exceeded: None,
         }
     }
 
@@ -1399,12 +1445,33 @@ impl Cfg {
     }
 
     /// Create a new basic block and return its ID.
+    ///
+    /// A `BlockId` is a `u32` index into this function's block arena, so one
+    /// function holds at most [`MAX_CFG_ENTITIES_PER_FUNCTION`] blocks. Past
+    /// that, `len() as u32` would wrap block 2^32 onto the entry block and
+    /// silently reroute control flow. This allocator has no fallible callers,
+    /// so it latches [`Cfg::capacity_exceeded`] and hands back an existing
+    /// block; the construction and optimization boundaries turn the latch into
+    /// an `E1401` diagnostic before the graph is published (spec C.1:2).
     pub fn new_block(&mut self) -> BlockId {
-        let id = BlockId(self.blocks.len() as u32);
+        let Some(index) = checked_owner_index(self.blocks.len()) else {
+            self.capacity_exceeded.get_or_insert("basic blocks");
+            // The arena is full, so the entry block always exists.
+            return BlockId(0);
+        };
+        let id = BlockId(index);
         self.blocks.push(BasicBlock::new(id));
         id
     }
 
+    /// The implementation-limit rejection latched by an infallible
+    /// [`Self::new_block`] or [`Self::add_inst`] that ran past the published
+    /// per-function ceiling, if any (spec Appendix C.6:1).
+    pub(crate) fn latched_capacity_error(&self) -> Option<CfgEditError> {
+        self.capacity_exceeded
+            .map(|family| CfgEditError::OwnerLimitExceeded { family })
+    }
+
     /// Get a block by ID.
     #[inline]
     pub fn get_block(&self, id: BlockId) -> &BasicBlock {
@@ -1418,8 +1485,17 @@ impl Cfg {
     }
 
     /// Add an instruction and return its value reference.
+    ///
+    /// A `CfgValue` is a `u32` index into this function's value arena, so one
+    /// function holds at most [`MAX_CFG_ENTITIES_PER_FUNCTION`] values. See
+    /// [`Self::new_block`] for why the ceiling is latched rather than returned.
     pub(crate) fn add_inst(&mut self, inst: CfgInst) -> CfgValue {
-        let value = CfgValue::from_raw(self.values.len() as u32);
+        let Some(index) = checked_owner_index(self.values.len()) else {
+            self.capacity_exceeded.get_or_insert("values");
+            // The arena is full, so value 0 always exists.
+            return CfgValue::from_raw(0);
+        };
+        let value = CfgValue::from_raw(index);
         self.values.push(inst);
         value
     }
@@ -3133,6 +3209,76 @@ mod tests {
         );
     }
 
+    #[test]
+    fn cfg_owner_limit_message_names_the_published_per_function_ceiling() {
+        // RUE-1226 / spec C.1:2: the per-function block and value arenas are a
+        // separate ceiling from the per-program payload word store, and its
+        // diagnostic has to name the one actually exceeded.
+        let error = CfgEditError::OwnerLimitExceeded {
+            family: "basic blocks",
+        };
+        assert_eq!(
+            error.to_string(),
+            "this function's CFG has more basic blocks than the implementation limit of \
+             4294967295 per function (spec Appendix C.6:1)"
+        );
+        assert_eq!(
+            error.error_kind("CFG construction failed").code(),
+            rue_error::ErrorCode::COMPILER_RESOURCE_LIMIT
+        );
+        assert_eq!(MAX_CFG_ENTITIES_PER_FUNCTION, u32::MAX);
+    }
+
+    #[test]
+    fn owner_index_allocation_stops_at_the_published_ceiling() {
+        assert_eq!(checked_owner_index(0), Some(0));
+        assert_eq!(
+            checked_owner_index(MAX_CFG_ENTITIES_PER_FUNCTION as usize - 1),
+            Some(MAX_CFG_ENTITIES_PER_FUNCTION - 1)
+        );
+        // The final u32 identity is not allocated: `len() as u32` would then
+        // wrap the next entity onto identity 0.
+        assert_eq!(
+            checked_owner_index(MAX_CFG_ENTITIES_PER_FUNCTION as usize),
+            None
+        );
+    }
+
+    #[test]
+    fn an_ordinary_graph_never_latches_the_per_function_ceiling() {
+        let mut cfg = Cfg::new(Type::I32, 0, 0, "f".into(), Vec::<bool>::new());
+        let block = cfg.new_block();
+        assert_eq!(block, BlockId(0));
+        assert!(cfg.new_block() != block);
+        cfg.add_inst(CfgInst {
+            data: CfgInstData::Const(7),
+            ty: Type::I32,
+            span: Span::new(0, 1),
+        });
+        assert!(cfg.latched_capacity_error().is_none());
+    }
+
+    #[test]
+    fn a_latched_graph_reports_the_family_that_ran_out() {
+        // Reaching the ceiling needs 2^32 entities, so the latch itself is set
+        // here; `new_block`/`add_inst` set it the same way and then hand back an
+        // existing identity rather than a wrapped one.
+        let mut cfg = Cfg::new(Type::I32, 0, 0, "f".into(), Vec::<bool>::new());
+        cfg.new_block();
+        cfg.capacity_exceeded = Some("values");
+        let error = cfg.latched_capacity_error().expect("latched");
+        assert!(matches!(
+            error,
+            CfgEditError::OwnerLimitExceeded { family: "values" }
+        ));
+        assert_eq!(
+            error.error_kind("CFG construction failed").code(),
+            rue_error::ErrorCode::COMPILER_RESOURCE_LIMIT
+        );
+        // The latch survives the clone every optimization transaction takes.
+        assert!(cfg.clone().latched_capacity_error().is_some());
+    }
+
     #[test]
     fn test_block_id_size() {
         assert_eq!(std::mem::size_of::<BlockId>(), 4);
diff --git a/crates/rue-cfg/src/lib.rs b/crates/rue-cfg/src/lib.rs
index 3d2acf0d7..11d3bf021 100644
--- a/crates/rue-cfg/src/lib.rs
+++ b/crates/rue-cfg/src/lib.rs
@@ -33,8 +33,8 @@ pub use inline::{CfgInlineError, inline_call};
 pub use inst::{
     BasicBlock, BlockId, Cfg, CfgArgMode, CfgCallArg, CfgDisplay, CfgEditError,
     CfgEditTransactionError, CfgEditor, CfgInst, CfgInstData, CfgPayloadStorageStats,
-    CfgRemapError, CfgValue, MAX_CFG_PAYLOAD_WORDS_PER_PROGRAM, Place, PlaceBase, Projection,
-    Terminator, ValidatedCfg,
+    CfgRemapError, CfgValue, MAX_CFG_ENTITIES_PER_FUNCTION, MAX_CFG_PAYLOAD_WORDS_PER_PROGRAM,
+    Place, PlaceBase, Projection, Terminator, ValidatedCfg,
 };
 pub use opt::OptLevel;
 #[doc(hidden)]
diff --git a/crates/rue-cfg/src/opt/mod.rs b/crates/rue-cfg/src/opt/mod.rs
index a6390ad47..9a7766136 100644
--- a/crates/rue-cfg/src/opt/mod.rs
+++ b/crates/rue-cfg/src/opt/mod.rs
@@ -283,6 +283,13 @@ fn publish_optimization(
     type_pool: &FrozenTypeInternPool,
 ) -> Result<ValidatedCfg, CfgOptimizationError> {
     pass_result?;
+    // A pass that allocated past the published per-function block/value ceiling
+    // (spec Appendix C.6:1) latched instead of wrapping an identity; report the
+    // limit here rather than letting verification raise an E9000 about the
+    // aliased identity it handed back.
+    if let Some(error) = cfg.latched_capacity_error() {
+        return Err(error.into());
+    }
     // Recheck the graph handed to codegen. DCE deliberately leaves detached
     // dead values in the arena, so attachment completeness was established by
     // the strict pre-pass check above; all live attachments and uses are still
diff --git a/crates/rue-compiler/src/canonical_semantic.rs b/crates/rue-compiler/src/canonical_semantic.rs
index bcbd077b5..1f9249eff 100644
--- a/crates/rue-compiler/src/canonical_semantic.rs
+++ b/crates/rue-compiler/src/canonical_semantic.rs
@@ -809,6 +809,29 @@ pub(crate) fn analyze_prepared_canonical_program_reusing_declarations(
                 ),
             )
         })?;
+    // The declaration-binding boundary is the earliest point at which the
+    // composite-type ceiling can be reported (spec Appendix C.6:1, C.1:2).
+    // Interning is infallible, so a compilation past the ceiling latches and
+    // keeps handing later registrations the final pool entry; every handle
+    // issued after the latch carries a kind tag the entry it names need not
+    // have. Stopping here means no body is analyzed, no layout or drop fact is
+    // queried, and no CFG is built against that aliased universe — the reads
+    // those stages perform assume a well-kinded graph.
+    if bound.with_type_pool(rue_air::TypeInternPool::capacity_exceeded) {
+        return Err(CanonicalSemanticFailure::declaration(
+            crate::CompileErrors::from(crate::CompileError::without_span(
+                rue_error::ErrorKind::CompilerResourceLimit(rue_air::composite_type_limit_message()),
+            )),
+            declaration_stage_work(
+                declaration_index,
+                DeclarationBindingWork::default(),
+                SemanticBindingManifestWork::default(),
+                BodyOwnerTokenWork::default(),
+                BodyAnalysisWork::default(),
+                reuse,
+            ),
+        ));
+    }
     let dependency_file = |key: &crate::StableDefinitionKey| {
         definitions
             .definition_by_key(key)
diff --git a/crates/rue-compiler/src/cfg_query.rs b/crates/rue-compiler/src/cfg_query.rs
index 8fd2283ec..69e1b7210 100644
--- a/crates/rue-compiler/src/cfg_query.rs
+++ b/crates/rue-compiler/src/cfg_query.rs
@@ -719,6 +719,17 @@ fn materialize_and_build_cfg(
     };
     context.record_work(rue_query::WorkItem::new("cfg.materialize.successes", 1));
 
+    // Backstop for the composite-type ceiling, checked before this body's type
+    // graph is projected or its layouts, drop facts, and drop glues are
+    // queried. A latched universe aliases later registrations onto the final
+    // pool entry, and those backend-facing reads require a well-kinded graph,
+    // so the check has to precede them rather than guard only `build_cfg`.
+    // Declaration binding normally reports the limit first (spec C.1:2); this
+    // covers a universe that latched after binding completed.
+    if materialized.type_pool.capacity_exceeded() {
+        return Ok(composite_type_limit_failure(materialized.body_span));
+    }
+
     let domains = match crate::durable_cfg::CfgDomainProjection::from_local_body(
         &materialized,
         body,
@@ -770,9 +781,6 @@ fn materialize_and_build_cfg(
         context.query_registered(type_facts, dependency.clone())?;
         context.query_registered(drop_glues, dependency)?;
     }
-    if materialized.type_pool.capacity_exceeded() {
-        return Ok(composite_type_limit_failure(materialized.body_span));
-    }
     build_cfg(context, call_abis, key, materialized, domains)
 }
 
@@ -786,12 +794,7 @@ fn materialize_and_build_cfg(
 fn composite_type_limit_failure(body_span: Span) -> CfgValue {
     CfgValue::Failure {
         errors: crate::CompileError::new(
-            rue_error::ErrorKind::CompilerResourceLimit(format!(
-                "this compilation defines more distinct composite types (structs, enums, arrays, \
-                 pointers, modules) than the implementation limit of {} — a live type handle is a \
-                 u32 holding an 8-bit kind tag and a 24-bit type-pool index (spec Appendix C.6:1)",
-                rue_air::MAX_COMPOSITE_TYPES
-            )),
+            rue_error::ErrorKind::CompilerResourceLimit(rue_air::composite_type_limit_message()),
             body_span,
         )
         .into(),
diff --git a/docs/spec/src/appendices/C-implementation-limits.md b/docs/spec/src/appendices/C-implementation-limits.md
index c54aeefab..c1a69f808 100644
--- a/docs/spec/src/appendices/C-implementation-limits.md
+++ b/docs/spec/src/appendices/C-implementation-limits.md
@@ -90,6 +90,9 @@ The compiler stores syntax, untyped IR, and typed IR in compact index-based form
 | Distinct identifiers and string literals | 4,294,967,295 | non-zero `u32` interner keys | E1401, when a token is interned |
 | IR instructions in one program | 4,294,967,295 | `u32` instruction reference, `u32::MAX` reserved as the null payload | E1401, at RIR publication |
 | IR payload words in one program | 4,294,967,295 words (16 GiB) | `u32` payload `start`/`extent` into one word store | E1401, at RIR/CFG payload staging |
+| Typed-IR instructions in one function body | 4,294,967,295 | `u32` instruction reference into that body's own array | E1401, at the semantic AIR boundary |
+| CFG basic blocks in one function | 4,294,967,295 | `u32` block identifier into that function's own graph | E1401, at CFG construction and optimization |
+| CFG values in one function | 4,294,967,295 | `u32` value reference into that function's own graph | E1401, at CFG construction and optimization |
 | Parameters of one function | 613,566,756 | 7 payload words per parameter | E1401, via the shared word store |
 | Fields of one struct | 2,147,483,647 | 2 payload words per field | E1401, via the shared word store |
 | Arguments of one call | 2,147,483,647 | 2 payload words per argument | E1401, via the shared word store |
@@ -104,12 +107,22 @@ The compiler stores syntax, untyped IR, and typed IR in compact index-based form
 
 The ceilings are not independent: parameters, fields, variants, arguments, and array elements all draw on the same per-program word store, so the sum of every payload in a program cannot exceed 4,294,967,295 words even when no individual construct does. That shared store is also what diagnoses them — a payload range that no longer fits `(start: u32, extent: u32)` is rejected when it is staged, whichever construct requested it.
 
-The "Diagnosed by" column names where each check runs, because the compact stores are filled by construction paths that cannot themselves fail. Instructions and composite types are the two such paths: `add_inst` and type interning are called from hundreds of infallible sites, so instead of returning an error at each one, the owner records that its ceiling was reached, stops growing, and the next construction or semantic boundary converts that record into the E1401 diagnostic. No index is ever wrapped, no entry is ever silently dropped in a compilation that goes on to be published, and no artifact built past a ceiling reaches code generation.
+The "Diagnosed by" column names where each check runs, because the compact stores are filled by construction paths that cannot themselves fail. Instructions, composite types, and the per-function CFG arenas are such paths: `add_inst`, `new_block`, and type interning are called from hundreds of infallible sites, so instead of returning an error at each one, the owner records that its ceiling was reached, stops growing, and the next construction, semantic, or optimization boundary converts that record into the E1401 diagnostic. No index is ever wrapped, no entry is ever silently dropped in a compilation that goes on to be published, and no artifact built past a ceiling reaches code generation.
 
 {{ rule(id="C.6:3", cat="normative") }}
 
 Syntactic nesting depth — the depth to which expressions, types, and blocks may be nested within one another — is bounded. A conforming implementation **MUST** support a nesting depth of at least 256 levels, and **MUST** diagnose input that exceeds its supported maximum with a clear error rather than exhausting the stack or otherwise failing catastrophically. The reference implementation rejects over-deep input with error `E0482` and a fixed maximum of 256 levels. This bound applies uniformly to every recursive syntactic construct, including parenthesised and operator-chained expressions (`((…))`, `a + a + …`), field and method chains (`a.b.c…`), nested types (`[[…]]`, `ptr const ptr const …`), and `else if` chains.
 
+{{ rule(id="C.6:4") }}
+
+The rows differ in what they count, and the "Construct" column says which. A per-program row names a store the whole compilation shares, so every construct in the program draws on the same budget. A per-function row — the typed-IR instruction array, the CFG block arena, the CFG value arena, and the frame budget of C.4:3 — names storage that belongs to one function and is indexed only by that function's own identifiers. A per-function ceiling binds independently of program size: a program of any legal size may hold any number of functions that each stay inside it, and one function that exceeds it is rejected even in an otherwise tiny program. The per-construct rows (parameters, fields, arguments, variants, array elements) are neither: they are consequences of the shared per-program word store, as C.6:2 states.
+
+{{ rule(id="C.6:5") }}
+
+A per-function CFG ceiling is checked rather than argued unreachable, because the number of CFG entities a function produces is not a small constant multiple of the typed-IR instructions it was lowered from. Drop elaboration re-emits the pending drops at *every* exit: a `return` emits one drop for each live binding still owning a value, plus a guard block for each binding whose move is path-dependent. A body with `N` droppable bindings and `M` `return` statements therefore lowers to on the order of `N * M` CFG values and blocks, from a body whose own instruction count is on the order of `N + M`.
+
+That expansion is quadratic, so no linear bound on CFG size follows from the ceilings above. Taking `N = M = 65,536` gives 2^32 drop values — past the `u32` value space — from roughly 65,536 bindings of about 32 source bytes each and 65,536 returns of about 16 bytes each: about 3 MiB of source, three orders of magnitude inside the file ceiling of C.3:1, and a typed-IR body four orders of magnitude inside the per-program instruction ceiling. The compiler checks these two ceilings for that reason, and reports E1401 naming the exceeded one.
+
 ## Stack and Memory Considerations
 
 {{ rule(id="C.7:1") }}