Security fix: Ty::kind() propagates affinity through compound types

Critical bypass: generic ADTs containing capabilities (e.g., Smuggler<FsCap>)
were classified as Kind::Unrestricted, allowing capability duplication via
wrapper copying. Ty::kind() now recurses into ADT type args, tuples, and lists.

Found during pre-hardening for issue-011
442 tests, zero warnings.

Author: Strata Core

crates/strata-types/src/checker.rs

@@ -796,8 +796,13 @@ impl TypeChecker {
                 })
                 .collect::<Result<Vec<_>, TypeError>>()?;
 
-            crate::move_check::check_function_body(&param_info, &decl.body, &self.env)
-                .map_err(move_error_to_type_error)?;
+            crate::move_check::check_function_body(
+                &param_info,
+                &decl.body,
+                &self.env,
+                &self.adt_registry,
+            )
+            .map_err(move_error_to_type_error)?;
         }
 
         // NOW generalize: compute env vars excluding this function's own type vars

crates/strata-types/src/infer/ty.rs

@@ -171,9 +171,34 @@ impl Ty {
     /// `Unrestricted`. Unresolved type variables (`Ty::Var`) are treated
     /// as `Unrestricted` — the move checker should only call this on
     /// fully-resolved types after substitution.
+    ///
+    /// RULE: Closures capturing affine values must themselves be affine.
+    /// Currently not enforceable because Ty::Arrow doesn't track captures
+    /// (closures/lambdas are not yet a language feature). The absence of
+    /// closure syntax is the current enforcement mechanism.
+    /// When closures gain capture tracking (post-borrowing), add:
+    ///   Ty::Arrow with captured_env → if captured_env.contains_affine() { return Kind::Affine; }
     pub fn kind(&self) -> Kind {
         match self {
             Ty::Cap(_) => Kind::Affine,
+            // Compound types containing affine components are themselves affine.
+            // This prevents capability laundering through generic ADTs:
+            // e.g. Smuggler<FsCap> must be affine so it can't be copied.
+            Ty::Adt { args, .. } => {
+                if args.iter().any(|arg| arg.kind() == Kind::Affine) {
+                    Kind::Affine
+                } else {
+                    Kind::Unrestricted
+                }
+            }
+            Ty::Tuple(tys) => {
+                if tys.iter().any(|ty| ty.kind() == Kind::Affine) {
+                    Kind::Affine
+                } else {
+                    Kind::Unrestricted
+                }
+            }
+            Ty::List(inner) => inner.kind(),
             _ => Kind::Unrestricted,
         }
     }

crates/strata-types/src/move_check.rs

@@ -8,6 +8,7 @@
 //! bindings need single-use tracking, and resolves polymorphic return types
 //! by manually instantiating callee schemes with known argument types.
 
+use crate::adt::AdtRegistry;
 use crate::infer::ty::{Kind, Scheme, Ty, TypeVarId};
 use std::collections::HashMap;
 use strata_ast::ast::{Block, Expr, Pat, Stmt};
@@ -104,10 +105,12 @@ pub struct MoveChecker<'a> {
     /// The environment with generalized function schemes (for resolving
     /// polymorphic call return types).
     env: &'a HashMap<String, Scheme>,
+    /// ADT registry for resolving generic field types in pattern destructuring.
+    adt_registry: &'a AdtRegistry,
 }
 
 impl<'a> MoveChecker<'a> {
-    fn new(env: &'a HashMap<String, Scheme>) -> Self {
+    fn new(env: &'a HashMap<String, Scheme>, adt_registry: &'a AdtRegistry) -> Self {
         MoveChecker {
             name_to_id: HashMap::new(),
             tracked: HashMap::new(),
@@ -116,6 +119,7 @@ impl<'a> MoveChecker<'a> {
             errors: Vec::new(),
             binding_types: HashMap::new(),
             env,
+            adt_registry,
         }
     }
 
@@ -236,6 +240,106 @@ impl<'a> MoveChecker<'a> {
         }
     }
 
+    // -----------------------------------------------------------------------
+    // ADT field type resolution for pattern destructuring
+    // -----------------------------------------------------------------------
+
+    /// Resolve variant field types by matching the scrutinee type against the
+    /// ADT definition and substituting generic type parameters.
+    ///
+    /// For example, if `Box<T>` has variant `Val(T)` and the scrutinee is
+    /// `Box<FsCap>`, this returns `[FsCap]` for the variant fields.
+    ///
+    /// Returns None if the ADT or variant can't be resolved (fallback to unit).
+    fn resolve_variant_field_types(
+        &self,
+        path: &strata_ast::ast::Path,
+        scrutinee_ty: &Ty,
+    ) -> Option<Vec<Ty>> {
+        // Path for a variant is e.g. ["Box", "Val"] — first segment is ADT name
+        if path.segments.len() < 2 {
+            return None;
+        }
+        let adt_name = &path.segments[0].text;
+        let variant_name = &path.segments[1].text;
+
+        let adt_def = self.adt_registry.get(adt_name)?;
+        let variant = adt_def.find_variant(variant_name)?;
+
+        let raw_field_types = match &variant.fields {
+            crate::adt::VariantFields::Unit => return Some(vec![]),
+            crate::adt::VariantFields::Tuple(tys) => tys,
+        };
+
+        // Build substitution: type_params[i] → scrutinee_args[i]
+        let scrutinee_args = match scrutinee_ty {
+            Ty::Adt { args, .. } => args,
+            _ => return None,
+        };
+
+        if adt_def.type_params.is_empty() || scrutinee_args.is_empty() {
+            // Non-generic ADT — raw field types are already concrete
+            return Some(raw_field_types.clone());
+        }
+
+        // Map type param TypeVarIds to the concrete types from the scrutinee.
+        // ADT type params are registered with TypeVarId(0), TypeVarId(1), etc.
+        let mut mapping: HashMap<TypeVarId, Ty> = HashMap::new();
+        for (i, arg) in scrutinee_args.iter().enumerate() {
+            mapping.insert(TypeVarId(i as u32), arg.clone());
+        }
+
+        Some(
+            raw_field_types
+                .iter()
+                .map(|t| apply_type_mapping(t, &mapping))
+                .collect(),
+        )
+    }
+
+    /// Resolve struct field types by matching the scrutinee type against the
+    /// ADT definition and substituting generic type parameters.
+    ///
+    /// Returns a map from field name to resolved type, or None if unresolvable.
+    fn resolve_struct_field_types(
+        &self,
+        path: &strata_ast::ast::Path,
+        scrutinee_ty: &Ty,
+    ) -> Option<HashMap<String, Ty>> {
+        let adt_name = &path.segments.first()?.text;
+
+        let adt_def = self.adt_registry.get(adt_name)?;
+        let fields = adt_def.fields()?;
+
+        // Build substitution from scrutinee args
+        let scrutinee_args = match scrutinee_ty {
+            Ty::Adt { args, .. } => args,
+            _ => return None,
+        };
+
+        if adt_def.type_params.is_empty() || scrutinee_args.is_empty() {
+            // Non-generic struct — raw field types are already concrete
+            return Some(
+                fields
+                    .iter()
+                    .map(|f| (f.name.clone(), f.ty.clone()))
+                    .collect(),
+            );
+        }
+
+        let mut mapping: HashMap<TypeVarId, Ty> = HashMap::new();
+        for (i, arg) in scrutinee_args.iter().enumerate() {
+            mapping.insert(TypeVarId(i as u32), arg.clone());
+        }
+
+        Some(
+            fields
+                .iter()
+                .map(|f| (f.name.clone(), apply_type_mapping(&f.ty, &mapping)))
+                .collect(),
+        )
+    }
+
     // -----------------------------------------------------------------------
     // Type resolution for function call return types
     // -----------------------------------------------------------------------
@@ -553,15 +657,34 @@ impl<'a> MoveChecker<'a> {
                     }
                 }
             }
-            Pat::Variant { fields, .. } => {
-                // Caps in ADT fields are banned, so variant fields are unrestricted
-                for p in fields {
-                    self.introduce_pattern_bindings(p, &Ty::unit());
+            Pat::Variant { path, fields, .. } => {
+                // DEFENSE-IN-DEPTH: When the caps-in-ADTs ban is lifted (post-linear
+                // types), this substitution ensures generic variant fields are properly
+                // resolved so capability bindings are tracked as affine.
+                // Currently the ban prevents caps from reaching ADT fields, so all
+                // field types resolve to unrestricted. But when the ban is lifted,
+                // e.g. Box<FsCap> matched as Box::Val(inner), inner must be FsCap.
+                let field_types = self.resolve_variant_field_types(path, ty);
+                let unit = Ty::unit();
+                for (i, p) in fields.iter().enumerate() {
+                    let field_ty = field_types
+                        .as_ref()
+                        .and_then(|tys| tys.get(i))
+                        .unwrap_or(&unit);
+                    self.introduce_pattern_bindings(p, field_ty);
                 }
             }
-            Pat::Struct { fields, .. } => {
+            Pat::Struct { path, fields, .. } => {
+                // DEFENSE-IN-DEPTH: Same as variant — resolve struct field types
+                // through the generic substitution when possible.
+                let field_types = self.resolve_struct_field_types(path, ty);
+                let unit = Ty::unit();
                 for f in fields {
-                    self.introduce_pattern_bindings(&f.pat, &Ty::unit());
+                    let field_ty = field_types
+                        .as_ref()
+                        .and_then(|m| m.get(&f.name.text))
+                        .unwrap_or(&unit);
+                    self.introduce_pattern_bindings(&f.pat, field_ty);
                 }
             }
         }
@@ -657,8 +780,9 @@ pub fn check_function_body(
     params: &[(String, Ty, Span)],
     body: &Block,
     env: &HashMap<String, Scheme>,
+    adt_registry: &AdtRegistry,
 ) -> Result<(), MoveError> {
-    let mut checker = MoveChecker::new(env);
+    let mut checker = MoveChecker::new(env, adt_registry);
 
     // Introduce function parameters as alive bindings
     for (name, ty, span) in params {

crates/strata-types/tests/capabilities.rs

@@ -382,6 +382,69 @@ fn multiple_cap_params_same_kind() {
     );
 }
 
+// ============================================================================
+// CAPS-IN-ADT BAN REGRESSION TESTS (Defense-in-Depth for Generic ADTs)
+//
+// These tests verify the caps-in-ADT ban covers generic ADT instantiation
+// with capability types. When the ban is eventually lifted (post-linear types),
+// the move checker's generic field resolution must correctly track affinity.
+// ============================================================================
+
+#[test]
+fn caps_in_direct_adt_field_banned() {
+    // Direct capability type in an ADT field is rejected at registration time.
+    // This is the existing enforcement mechanism.
+    let err = check_err(
+        r#"
+        enum Wrapper { Hold(FsCap) }
+    "#,
+    );
+    assert!(
+        err.contains("capability") || err.contains("FsCap"),
+        "Expected error about capability in ADT field, got: {err}"
+    );
+}
+
+#[test]
+fn generic_adt_with_cap_single_use_ok() {
+    // Generic ADTs instantiated with caps are NOT caught by the caps-in-ADT
+    // registration ban (ban checks field types at definition time where fields
+    // are type variables). However, Ty::kind() propagates affinity through ADT
+    // type args, so MyOption<FsCap> is Kind::Affine. This means:
+    // - Single use (constructing and returning) is fine
+    // - Duplication (let a = x; let b = x;) is caught by the move checker
+    check_ok(
+        r#"
+        enum MyOption<T> { Some(T), None }
+        fn wraps_cap(fs: FsCap) -> MyOption<FsCap> & {} {
+            MyOption::Some(fs)
+        }
+    "#,
+    );
+}
+
+#[test]
+fn generic_adt_cap_field_double_use_after_extract() {
+    // When a cap is extracted from a generic ADT via pattern match,
+    // the extracted binding must be affine. Double use is rejected.
+    let err = check_err(
+        r#"
+        enum Box<T> { Val(T) }
+        extern fn use_fs(fs: FsCap) -> () & {Fs};
+        fn bad(fs: FsCap) -> () & {Fs} {
+            let b = Box::Val(fs);
+            match b {
+                Box::Val(inner) => { use_fs(inner); use_fs(inner) },
+            }
+        }
+    "#,
+    );
+    assert!(
+        err.contains("already been used"),
+        "Expected double-use error on cap extracted from generic ADT, got: {err}"
+    );
+}
+
 // ============================================================================
 // ADT NAME SHADOWING TESTS
 // ============================================================================