axon-frontend 1.3.0

//! AXON Type Checker — Phase 1: symbol table, duplicates, references, field validation.
//!
//! Direct port of axon/compiler/type_checker.py (subset).
//!
//! What it checks:
//!   - Duplicate declarations
//!   - Undefined references in `run` (flow, persona, context, anchors)
//!   - Field value validation (tone, depth, memory scope, temperature, confidence, effort)
//!   - Duplicate step names within flows
//!
//! What it does NOT check (deferred to C7+):
//!   - Epistemic lattice / type compatibility
//!   - Cross-node type inference / uncertainty propagation
//!   - Tier 2 construct-specific validation

#![allow(dead_code)]

use std::collections::HashMap;

use crate::ast::*;
use crate::session::SessionType;
use crate::epistemic;

// ── Valid value sets (mirrors Python frozensets) ─────────────────────────────

const VALID_TONES: &[&str] = &[
    "analytical",
    "assertive",
    "casual",
    "diplomatic",
    "empathetic",
    "formal",
    "friendly",
    "precise",
];

const VALID_MEMORY_SCOPES: &[&str] = &["ephemeral", "none", "persistent", "session"];

const VALID_DEPTHS: &[&str] = &["deep", "exhaustive", "shallow", "standard"];

const VALID_EFFORT_LEVELS: &[&str] = &["high", "low", "max", "medium"];

const VALID_VIOLATION_ACTIONS: &[&str] = &["escalate", "fallback", "log", "raise", "warn"];

const VALID_RETRIEVAL_STRATEGIES: &[&str] = &["exact", "hybrid", "semantic"];

// Fase 15.d — reserved primitive / built-in type names that a
// `lambda apply ... -> OutputType` MUST NOT shadow. Mirror of
// axon.compiler.type_checker._RESERVED_OUTPUT_TYPE_NAMES.
const RESERVED_OUTPUT_TYPE_NAMES: &[&str] = &[
    "any", "bool", "boolean", "bytes", "dict", "false", "float",
    "int", "integer", "list", "map", "none", "null", "number",
    "set", "str", "string", "true", "tuple", "void",
];

// §λ-L-E Fase 11.a + 11.c + 11.e — `stream` (mandatory backpressure),
// `trust` (mandatory proof), `sensitive` (data-category jurisdiction
// — open taxonomy), `legal` (mandatory legal basis from the closed
// catalogue in `crate::legal_basis`), `ots` (subkinds `transform:
// <from>:<to>` + `backend:<native|ffmpeg>`) join the catalogue.
// Qualifiers are validated separately below.
const VALID_EFFECTS: &[&str] = &[
    "io",
    "network",
    "pure",
    "random",
    "storage",
    "stream",
    "trust",
    "sensitive",
    "legal",
    "ots",
];

const VALID_EPISTEMIC_LEVELS: &[&str] = &["believe", "doubt", "know", "speculate"];

const VALID_DERIVATIONS: &[&str] = &["aggregated", "derived", "inferred", "raw", "transformed"];

// ── Tier 2 valid-value sets (mirrors Python frozensets) ────────────────────

const VALID_AGENT_STRATEGIES: &[&str] = &["custom", "plan_and_execute", "react", "reflexion"];

const VALID_ON_STUCK_POLICIES: &[&str] = &["escalate", "forge", "hibernate", "retry"];

const VALID_SCAN_CATEGORIES: &[&str] = &[
    "bias",
    "code_injection",
    "data_exfil",
    "hallucination",
    "jailbreak",
    "model_theft",
    "pii_leak",
    "prompt_injection",
    "social_engineering",
    "toxicity",
    "training_poisoning",
];

const VALID_SHIELD_STRATEGIES: &[&str] = &[
    "canary",
    "classifier",
    "dual_llm",
    "ensemble",
    "pattern",
    "perplexity",
];

const VALID_ON_BREACH_POLICIES: &[&str] = &[
    "deflect",
    "escalate",
    "halt",
    "quarantine",
    "sanitize_and_retry",
];

const VALID_SEVERITY_LEVELS: &[&str] = &["critical", "high", "low", "medium"];

const VALID_OTS_HOMOTOPY: &[&str] = &["deep", "shallow", "speculative"];

const VALID_MANDATE_POLICIES: &[&str] = &["coerce", "halt", "retry"];

// §Fase 36.x.b (D2) — `in_memory` is a first-class declarable
// `axonstore` backend. The runtime `StoreRegistry::classify_backend`
// already maps `"in_memory"` → `StoreHandle::InMemory` (the
// key-value path); adding it here makes a source-declared in-memory
// store type-check, so the canonical agent flow (retrieve → step →
// persist) is runnable + testable with ZERO external infrastructure
// — no Postgres, no `DATABASE_URL`. `connection:` is optional for an
// `in_memory` store (it is optional for every backend at the
// type-checker layer — no `connection`-required check exists here).
//
// `mysql` / `sqlite` remain type-check-valid but runtime-absent (a
// documented future fase) — see `docs/fase/fase_36x_mixed_flow_streaming.md` §7.
const VALID_STORE_BACKENDS: &[&str] = &["in_memory", "mysql", "postgresql", "sqlite"];

const VALID_STORE_ISOLATION: &[&str] = &["read_committed", "repeatable_read", "serializable"];

const VALID_STORE_ON_BREACH: &[&str] = &["log", "raise", "rollback"];

const VALID_ENDPOINT_METHODS: &[&str] = &["DELETE", "GET", "PATCH", "POST", "PUT"];

const VALID_INFERENCE_MODES: &[&str] = &["active", "passive"];

fn is_valid(value: &str, set: &[&str]) -> bool {
    set.contains(&value)
}

fn valid_list(set: &[&str]) -> String {
    set.join(", ")
}

// ── Type error ───────────────────────────────────────────────────────────────

#[derive(Debug)]
pub struct TypeError {
    pub message: String,
    pub line: u32,
    pub column: u32,
}

// ── §Fase 38.x.f — Cardinality inference primitive ──────────────────────────

/// §Fase 38.x.f (D1) — A flow-tail / endpoint-output cardinality.
///
/// Distinguishes the four cardinality classes the type-checker reasons
/// about at compile time, plus the disagreement + unknown fallback cases:
///
///  - [`Cardinality::Singular`] — one value of the named type.
///    Examples: `step S { return T }`, `return result[0]`, a bound
///    let-variable that resolved to singular.
///  - [`Cardinality::Plural`] — a `List<T>` materialized at once.
///    Examples: `retrieve … as x`, `for x in xs { … } yield T`,
///    `return [a, b, c]`.
///  - [`Cardinality::StreamCardinality`] — a `Stream<T>` whose chunks
///    arrive over time (SSE wire format). Distinct from
///    [`Cardinality::Plural`] because the runtime handles them
///    differently — `List<T>` ships as a single JSON array; `Stream<T>`
///    ships as a sequence of SSE events.
///  - [`Cardinality::Unit`] — statement-only nodes (`persist`, `mutate`,
///    `purge`) that yield no value. Endpoints declaring `output: Unit`
///    accept this.
///  - [`Cardinality::Disagreed`] — branches (`if`/`else`, `par`)
///    disagree on tail cardinality. Triggers `axon-W003
///    cardinality_disagreement_in_branches`. The special `output: Any`
///    accepts this (degraded type safety).
///  - [`Cardinality::Unknown`] — opaque flow tail (e.g. a `Par` block,
///    a `LambdaDataApply` whose target resolves dynamically). The gate
///    silently passes — the runtime D5 path stays as the final check.
///  - [`Cardinality::Wrapped`] (§Fase 39 D4) — `FlowEnvelope<T>`
///    declares a `transport: json` endpoint whose wire payload is the
///    canonical ψ-vector envelope. The compile-time cardinality of the
///    wrapper IS the cardinality of T; the type-checker reasons through
///    the wrapper transparently. `Wrapped(Box::new(Plural("X")))` for
///    `FlowEnvelope<List<X>>`; `Wrapped(Box::new(Singular("X")))` for
///    `FlowEnvelope<X>`. Nested wraps (`FlowEnvelope<FlowEnvelope<X>>`)
///    are syntactically possible but semantically degenerate and the
///    gate treats them transparently.
#[derive(Debug, Clone, PartialEq)]
pub(crate) enum Cardinality {
    /// A singular value of the named type.
    Singular(String),
    /// A `List<T>` materialized at once.
    Plural(String),
    /// A `Stream<T>` (temporal plural — chunks arrive on SSE).
    StreamCardinality(String),
    /// Statement-only tail (no return value).
    Unit,
    /// Branches disagree on cardinality.
    Disagreed,
    /// Opaque — cannot be inferred at compile time.
    Unknown,
    /// §Fase 39 (D4) — `FlowEnvelope<T>` wrapping. The compile-time
    /// cardinality of the wrapper is the cardinality of T preserved
    /// through the wrap. The wire-shape envelope is always a singular
    /// object; the type-checker reasons through the wrap by unwrapping.
    Wrapped(Box<Cardinality>),
}

/// §Fase 38.x.f (D1) — Compute the cardinality declared by an
/// `axonendpoint`'s `output:` string. Pure + total:
///
///  - `""` → `Unknown` (endpoint didn't declare; gate skips).
///  - `"Unit"` → `Unit`.
///  - `"Any"` → `Disagreed` (degraded acceptance — any tail accepted).
///  - `"List<T>"` → `Plural("T")`.
///  - `"Stream<T>"` → `StreamCardinality("T")`.
///  - `"FlowEnvelope<T>"` (§Fase 39 D4) → `Wrapped(Box::new(declared_cardinality(T)))`,
///    recursive — `"FlowEnvelope<List<X>>"` yields
///    `Wrapped(Box::new(Plural("X")))`.
///  - everything else → `Singular(s)`.
pub(crate) fn declared_cardinality(output_type: &str) -> Cardinality {
    let t = output_type.trim();
    if t.is_empty() {
        return Cardinality::Unknown;
    }
    if t == "Unit" {
        return Cardinality::Unit;
    }
    if t == "Any" {
        return Cardinality::Disagreed;
    }
    // §Fase 39 (D4) — FlowEnvelope<T> wrapping. Recurse on T so nested
    // forms like FlowEnvelope<List<X>> and FlowEnvelope<Stream<X>>
    // are recognized end-to-end. Recursion lands ≥ once and terminates
    // when T is a non-wrapping primitive.
    if let Some(rest) = t.strip_prefix("FlowEnvelope<") {
        if let Some(inner) = rest.strip_suffix('>') {
            let inner_card = declared_cardinality(inner.trim());
            return Cardinality::Wrapped(Box::new(inner_card));
        }
    }
    if let Some(rest) = t.strip_prefix("List<") {
        if let Some(inner) = rest.strip_suffix('>') {
            return Cardinality::Plural(inner.trim().to_string());
        }
    }
    if let Some(rest) = t.strip_prefix("Stream<") {
        if let Some(inner) = rest.strip_suffix('>') {
            return Cardinality::StreamCardinality(inner.trim().to_string());
        }
    }
    Cardinality::Singular(t.to_string())
}

/// §Fase 38.x.f (D1) — Infer the cardinality of a flow's tail
/// expression. Walks the body from tail backwards, returning the
/// first FlowStep whose cardinality is determinable, joining branches
/// on `if`/`else` (and detecting disagreement).
///
/// Pure + total: every flow body produces some [`Cardinality`] value;
/// when no FlowStep's tail is determinable the function returns
/// [`Cardinality::Unknown`] (the gate then silently passes — the
/// runtime D5 path remains the final check).
///
/// The implementation handles the FlowStep variants common to adopter
/// REST patterns:
///
///  - `Step` / `Probe` / `Reason` / `Validate` / `Refine` / `Weave` /
///    `LambdaDataApply` / `ShieldApply` / `OtsApply` / `MandateApply`
///    → declared `output_type` (mapped via [`declared_cardinality`]).
///  - `Return` → infer from the `value_expr` string shape:
///    `[a, b, …]` → Plural, `xs[N]` → Singular, bare identifier or
///    expression → Unknown.
///  - `Retrieve` → always `Plural("StoreRow")`.
///  - `Persist` / `Mutate` / `Purge` → `Unit`.
///  - `If` → join of `then_body` + `else_body` tail cardinalities.
///  - `ForIn` → `Plural` of the body's per-iteration cardinality
///    (a `for x in xs { … }` accumulates one value per iteration).
///  - `Let` → skip (intermediate); recurse to the next-newer step.
///  - `Break` / `Continue` → skip.
///
/// Every other FlowStep variant returns [`Cardinality::Unknown`]
/// (Par, Stream, Hibernate, Deliberate, Consensus, Forge, Focus,
/// Associate, Aggregate, ExploreStep, Ingest, Navigate, Drill, Trail,
/// Corroborate, ComputeApply, UseTool, Remember, Recall, Listen,
/// DaemonStep, Emit, Publish, Discover, Transact, GenericStep).
pub(crate) fn infer_flow_tail_cardinality(flow: &FlowDefinition) -> Cardinality {
    infer_body_tail_cardinality(&flow.body)
}

fn infer_body_tail_cardinality(body: &[FlowStep]) -> Cardinality {
    if body.is_empty() {
        return Cardinality::Unit;
    }
    // Walk from tail backwards; skip intermediate non-returning
    // statements (Let, Break, Continue) until we find the first
    // FlowStep whose tail cardinality is determinable.
    for step in body.iter().rev() {
        match step {
            FlowStep::Step(s) => return declared_cardinality(&s.output_type),
            FlowStep::LambdaDataApply(n) => return declared_cardinality(&n.output_type),
            FlowStep::ShieldApply(n) => return declared_cardinality(&n.output_type),
            FlowStep::OtsApply(n) => return declared_cardinality(&n.output_type),
            FlowStep::MandateApply(n) => return declared_cardinality(&n.output_type),
            FlowStep::If(cond) => {
                let then_card = infer_body_tail_cardinality(&cond.then_body);
                let else_card = infer_body_tail_cardinality(&cond.else_body);
                return join_cardinalities(&then_card, &else_card);
            }
            FlowStep::ForIn(fi) => {
                // The for-loop body's per-iteration cardinality becomes
                // Plural at the loop's tail (N iterations × per-iter
                // value = a list of N elements). When the body is empty
                // or yields Unit, the for-loop yields Plural of Unknown.
                let inner = infer_body_tail_cardinality(&fi.body);
                return match inner {
                    Cardinality::Singular(t) => Cardinality::Plural(t),
                    Cardinality::Plural(t) => Cardinality::Plural(t),
                    Cardinality::StreamCardinality(t) => {
                        // A for-loop accumulating streams flattens to
                        // a list of streams — treat as Plural of the
                        // stream element type for the gate.
                        Cardinality::Plural(t)
                    }
                    Cardinality::Unit => Cardinality::Unknown,
                    other => other,
                };
            }
            FlowStep::Return(r) => return infer_return_cardinality(&r.value_expr),
            FlowStep::Retrieve(_) => {
                return Cardinality::Plural("StoreRow".to_string());
            }
            FlowStep::Persist(_) | FlowStep::Mutate(_) | FlowStep::Purge(_) => {
                return Cardinality::Unit;
            }
            FlowStep::Let(_) | FlowStep::Break(_) | FlowStep::Continue(_) => {
                continue;
            }
            // All other variants opaque for v1.40.0 (honest scope).
            _ => return Cardinality::Unknown,
        }
    }
    Cardinality::Unit
}

fn infer_return_cardinality(expr: &str) -> Cardinality {
    let t = expr.trim();
    if t.is_empty() {
        return Cardinality::Unit;
    }
    // `[a, b, c]` literal list → Plural with unknown element type.
    if t.starts_with('[') && t.ends_with(']') && t.len() >= 2 {
        return Cardinality::Plural(String::new());
    }
    // Indexed projection `name[N]` (e.g. `result[0]`) → Singular.
    // Match: ends with `]`, contains `[`, NOT starting with `[`.
    if t.ends_with(']') && t.contains('[') && !t.starts_with('[') {
        return Cardinality::Singular(String::new());
    }
    // Bare identifier or unknown expression — opaque.
    Cardinality::Unknown
}

fn join_cardinalities(a: &Cardinality, b: &Cardinality) -> Cardinality {
    // Unknown joins as the OTHER cardinality (one branch determines).
    if matches!(a, Cardinality::Unknown) {
        return b.clone();
    }
    if matches!(b, Cardinality::Unknown) {
        return a.clone();
    }
    // Both determined and equal → preserve.
    if a == b {
        return a.clone();
    }
    // Disagreed cases: cardinality kinds differ → Disagreed.
    // (We do NOT compare element types here — Fase 37 D2 / T901 handle
    // type mismatch; we only care about Singular vs Plural vs Stream
    // vs Unit kind disagreement for D6 W003.)
    let kind = |c: &Cardinality| match c {
        Cardinality::Singular(_) => 0,
        Cardinality::Plural(_) => 1,
        Cardinality::StreamCardinality(_) => 2,
        Cardinality::Unit => 3,
        Cardinality::Disagreed => 4,
        Cardinality::Unknown => 5,
        // §Fase 39 (D4) — Wrapped joins by its INNER kind. A
        // `FlowEnvelope<List<X>>` branch joining a bare `List<X>`
        // branch agree on plural cardinality through the wrap.
        Cardinality::Wrapped(_) => 6,
    };
    if kind(a) == kind(b) {
        // Same kind, different element type — preserve a's shape.
        return a.clone();
    }
    Cardinality::Disagreed
}

// ── Symbol table ─────────────────────────────────────────────────────────────

#[derive(Debug, Clone)]
struct Symbol {
    name: String,
    kind: String,
    line: u32,
}

struct SymbolTable {
    symbols: HashMap<String, Symbol>,
}

impl SymbolTable {
    fn new() -> Self {
        SymbolTable {
            symbols: HashMap::new(),
        }
    }

    fn declare(&mut self, name: &str, kind: &str, line: u32) -> Option<String> {
        if let Some(existing) = self.symbols.get(name) {
            return Some(format!(
                "Duplicate declaration: '{}' already defined as {} (first defined at line {})",
                name, existing.kind, existing.line
            ));
        }
        self.symbols.insert(
            name.to_string(),
            Symbol {
                name: name.to_string(),
                kind: kind.to_string(),
                line,
            },
        );
        None
    }

    fn lookup(&self, name: &str) -> Option<&Symbol> {
        self.symbols.get(name)
    }
}

// ── Type checker ─────────────────────────────────────────────────────────────

pub struct TypeChecker<'a> {
    program: &'a Program,
    symbols: SymbolTable,
    errors: Vec<TypeError>,
    /// §λ-L-E Fase 13 D4 — non-fatal diagnostics (deprecation, etc.).
    /// Errors halt compilation; warnings surface in `axon check` output
    /// without failing unless `--strict` is set.  Mirrors the Python
    /// TypeChecker.warnings property.
    warnings: Vec<TypeError>,
    /// §Fase 38.d (D2) — store-name → ColumnSet built from each
    /// `axonstore` declaration's `schema:` declaration form.
    ///
    /// §Fase 38.x.d (D2) extends this to ALL THREE forms when a
    /// `manifest` is supplied via [`TypeChecker::with_manifest`]:
    /// form (a) inline (always populated, no manifest needed),
    /// form (b) manifest_ref (populated from `manifest.lookup(qualified_name)`),
    /// form (c) env_var (populated via first-match heuristic
    /// `<env_var>.<store_name>` then fallback `*.<store_name>`).
    ///
    /// When no manifest is supplied (the v1.38.3 default), forms
    /// (b)/(c) silently skip exactly as they did pre-v1.38.4 (D5
    /// absolute backwards-compat).
    store_inline_column_sets:
        std::collections::HashMap<String, crate::store_column_proof::ColumnSet>,
    /// §Fase 38.d (D2) — the current flow's parameter-name → axon-
    /// language-type-name map, set while `check_flow` runs so
    /// `check_flow_steps` can run the §38.d D2 proof against
    /// `where:` clauses. Cleared between flows so a parameter in one
    /// flow cannot leak into the proof for another.
    current_flow_params: crate::store_column_proof::FlowParamTypes,
    /// §Fase 38.x.d (D2) — optional manifest supplied at construction
    /// for forms (b)/(c) compile-time proof. `None` means form (b)/(c)
    /// silently skip (v1.38.3-compatible default). When `Some`, the
    /// `register_declarations` pass uses it to populate
    /// `store_inline_column_sets` for the non-inline forms.
    manifest: Option<&'a crate::store_schema_manifest::Manifest>,
}

impl<'a> TypeChecker<'a> {
    pub fn new(program: &'a Program) -> Self {
        TypeChecker {
            program,
            symbols: SymbolTable::new(),
            errors: Vec::new(),
            warnings: Vec::new(),
            store_inline_column_sets: std::collections::HashMap::new(),
            current_flow_params: crate::store_column_proof::FlowParamTypes::new(),
            manifest: None,
        }
    }

    /// §Fase 38.x.d (D2) — construct a TypeChecker that consults the
    /// supplied manifest when an `axonstore` declares its schema via
    /// form (b) `manifest_ref` or form (c) `env_var`. Form (a) inline
    /// is unaffected (populated identically with or without manifest).
    ///
    /// Adopters using `axon check --schemas-dir <path>` reach this
    /// constructor via `axon-rs/src/main.rs::cmd_check`. Adopters
    /// embedding the type-checker programmatically pass their own
    /// `Manifest` (e.g. constructed from `load_and_merge_manifests`).
    ///
    /// When `manifest` is None, behavior is byte-identical to
    /// [`Self::new`] (D5 backwards-compat absolute).
    pub fn with_manifest(
        program: &'a Program,
        manifest: &'a crate::store_schema_manifest::Manifest,
    ) -> Self {
        TypeChecker {
            program,
            symbols: SymbolTable::new(),
            errors: Vec::new(),
            warnings: Vec::new(),
            store_inline_column_sets: std::collections::HashMap::new(),
            current_flow_params: crate::store_column_proof::FlowParamTypes::new(),
            manifest: Some(manifest),
        }
    }

    pub fn check(mut self) -> Vec<TypeError> {
        self.register_declarations(&self.program.declarations);
        self.check_declarations(&self.program.declarations);
        self.errors
    }

    /// §λ-L-E Fase 13 D4 — return both errors and warnings.
    /// Callers preferring strict mode promote warnings → errors at the
    /// rendering layer (CLI `--strict` flag).  Mirrors the Python
    /// `(TypeChecker.check(), .warnings)` pair.
    pub fn check_with_warnings(mut self) -> (Vec<TypeError>, Vec<TypeError>) {
        self.register_declarations(&self.program.declarations);
        self.check_declarations(&self.program.declarations);
        (self.errors, self.warnings)
    }

    // ── emit ─────────────────────────────────────────────────────

    fn emit(&mut self, message: String, loc: &Loc) {
        self.errors.push(TypeError {
            message,
            line: loc.line,
            column: loc.column,
        });
    }

    /// §λ-L-E Fase 13 D4 — non-fatal diagnostic.
    fn warn(&mut self, message: String, loc: &Loc) {
        self.warnings.push(TypeError {
            message,
            line: loc.line,
            column: loc.column,
        });
    }

    fn check_range(&mut self, value: f64, lo: f64, hi: f64, field: &str, loc: &Loc) {
        if value < lo || value > hi {
            self.emit(
                format!("{field} must be between {lo:.1} and {hi:.1}, got {value:.1}"),
                loc,
            );
        }
    }

    // ── Phase 1: registration ────────────────────────────────────

    fn register_declarations(&mut self, decls: &[Declaration]) {
        // Collect registrations first to avoid borrow conflict
        let mut registrations: Vec<(String, String, u32, Loc)> = Vec::new();

        for decl in decls {
            match decl {
                Declaration::Persona(n) => {
                    registrations.push((
                        n.name.clone(),
                        "persona".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Context(n) => {
                    registrations.push((
                        n.name.clone(),
                        "context".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Anchor(n) => {
                    registrations.push((
                        n.name.clone(),
                        "anchor".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Memory(n) => {
                    registrations.push((
                        n.name.clone(),
                        "memory".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Tool(n) => {
                    registrations.push((n.name.clone(), "tool".into(), n.loc.line, n.loc.clone()));
                }
                Declaration::Type(n) => {
                    registrations.push((n.name.clone(), "type".into(), n.loc.line, n.loc.clone()));
                }
                Declaration::Flow(n) => {
                    registrations.push((n.name.clone(), "flow".into(), n.loc.line, n.loc.clone()));
                }
                Declaration::Intent(n) => {
                    registrations.push((
                        n.name.clone(),
                        "intent".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::LambdaData(n) => {
                    registrations.push((
                        n.name.clone(),
                        "lambda_data".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Agent(n) => {
                    registrations.push((n.name.clone(), "agent".into(), n.loc.line, n.loc.clone()));
                }
                Declaration::Shield(n) => {
                    registrations.push((
                        n.name.clone(),
                        "shield".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Pix(n) => {
                    registrations.push((n.name.clone(), "pix".into(), n.loc.line, n.loc.clone()));
                }
                Declaration::Psyche(n) => {
                    registrations.push((
                        n.name.clone(),
                        "psyche".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Corpus(n) => {
                    registrations.push((
                        n.name.clone(),
                        "corpus".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Dataspace(n) => {
                    registrations.push((
                        n.name.clone(),
                        "dataspace".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Ots(n) => {
                    registrations.push((n.name.clone(), "ots".into(), n.loc.line, n.loc.clone()));
                }
                Declaration::Mandate(n) => {
                    registrations.push((
                        n.name.clone(),
                        "mandate".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Compute(n) => {
                    registrations.push((
                        n.name.clone(),
                        "compute".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Daemon(n) => {
                    registrations.push((
                        n.name.clone(),
                        "daemon".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::AxonStore(n) => {
                    registrations.push((
                        n.name.clone(),
                        "axonstore".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                    // §Fase 38.d (D2) — when this axonstore carries an
                    // INLINE `schema: { … }` block, build its ColumnSet
                    // now so `check_flow_steps` can prove `where:`
                    // clauses against it.
                    //
                    // §Fase 38.x.d (D2, D4) — when this axonstore uses
                    // form (b) `manifest_ref` OR form (c) `env_var`
                    // AND `self.manifest` is set (the adopter passed
                    // `--schemas-dir <path>` to `axon check`), resolve
                    // the manifest entry NOW and populate the same
                    // `store_inline_column_sets` HashMap. The
                    // downstream proof paths (T801-T805 + T803) read
                    // from the HashMap uniformly — no code-path
                    // divergence between inline and manifest-loaded
                    // forms.
                    //
                    // Without `--schemas-dir`, `self.manifest` is None
                    // and forms (b)/(c) silently skip exactly as they
                    // did in v1.38.3 (D5 backwards-compat absolute).
                    if let Some(schema) = &n.column_schema {
                        match schema {
                            crate::store_schema::StoreColumnSchema::Inline { .. } => {
                                if let Some(cs) =
                                    crate::store_column_proof::ColumnSet::from_inline_schema(
                                        schema,
                                    )
                                {
                                    self.store_inline_column_sets
                                        .insert(n.name.clone(), cs);
                                }
                            }
                            crate::store_schema::StoreColumnSchema::ManifestRef {
                                qualified_name,
                                ..
                            } => {
                                if let Some(manifest) = self.manifest {
                                    if let Some(ms) = manifest.lookup(qualified_name) {
                                        let cs =
                                            crate::store_column_proof::ColumnSet::from_manifest_store(
                                                ms,
                                            );
                                        self.store_inline_column_sets
                                            .insert(n.name.clone(), cs);
                                    }
                                }
                            }
                            crate::store_schema::StoreColumnSchema::EnvVar {
                                var_name,
                                ..
                            } => {
                                if let Some(manifest) = self.manifest {
                                    // First-match heuristic mirrors
                                    // §Fase 38.d's `load_columns_for_schema`
                                    // + §Fase 38.f's `declared_columns_for`:
                                    // try exact `<var_name>.<store_name>`
                                    // first, then fall back to any
                                    // `*.<store_name>` (the manifest
                                    // ships the same shape for every
                                    // per-tenant namespace).
                                    let exact_key = format!("{}.{}", var_name, n.name);
                                    let resolved = manifest
                                        .lookup(&exact_key)
                                        .or_else(|| {
                                            // Suffix scan — find any
                                            // store ending in `.<n.name>`.
                                            let suffix = format!(".{}", n.name);
                                            for (key, store) in &manifest.stores {
                                                if key.ends_with(&suffix) {
                                                    return Some(store);
                                                }
                                            }
                                            None
                                        });
                                    if let Some(ms) = resolved {
                                        let cs =
                                            crate::store_column_proof::ColumnSet::from_manifest_store(
                                                ms,
                                            );
                                        self.store_inline_column_sets
                                            .insert(n.name.clone(), cs);
                                    }
                                }
                            }
                        }
                    }
                }
                Declaration::AxonEndpoint(n) => {
                    registrations.push((
                        n.name.clone(),
                        "axonendpoint".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Resource(n) => {
                    registrations.push((
                        n.name.clone(),
                        "resource".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Fabric(n) => {
                    registrations.push((
                        n.name.clone(),
                        "fabric".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Manifest(n) => {
                    registrations.push((
                        n.name.clone(),
                        "manifest".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Observe(n) => {
                    registrations.push((
                        n.name.clone(),
                        "observe".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Reconcile(n) => {
                    registrations.push((
                        n.name.clone(),
                        "reconcile".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Lease(n) => {
                    registrations.push((n.name.clone(), "lease".into(), n.loc.line, n.loc.clone()));
                }
                Declaration::Ensemble(n) => {
                    registrations.push((
                        n.name.clone(),
                        "ensemble".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Session(n) => {
                    registrations.push((
                        n.name.clone(),
                        "session".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Topology(n) => {
                    registrations.push((
                        n.name.clone(),
                        "topology".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Immune(n) => {
                    registrations.push((
                        n.name.clone(),
                        "immune".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Reflex(n) => {
                    registrations.push((
                        n.name.clone(),
                        "reflex".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Heal(n) => {
                    registrations.push((n.name.clone(), "heal".into(), n.loc.line, n.loc.clone()));
                }
                Declaration::Component(n) => {
                    registrations.push((
                        n.name.clone(),
                        "component".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::View(n) => {
                    registrations.push((n.name.clone(), "view".into(), n.loc.line, n.loc.clone()));
                }
                Declaration::Channel(n) => {
                    registrations.push((
                        n.name.clone(),
                        "channel".into(),
                        n.loc.line,
                        n.loc.clone(),
                    ));
                }
                Declaration::Socket(n) => {
                    registrations.push((n.name.clone(), "socket".into(), n.loc.line, n.loc.clone()));
                }
                Declaration::Generic(n) => {
                    if !n.name.is_empty() {
                        registrations.push((
                            n.name.clone(),
                            n.keyword.clone(),
                            n.loc.line,
                            n.loc.clone(),
                        ));
                    }
                }
                Declaration::Epistemic(_) => {
                    // Recursion handled below
                }
                Declaration::Import(_) | Declaration::Run(_) | Declaration::Let(_) => {}
            }
        }

        for (name, kind, line, loc) in registrations {
            if let Some(err) = self.symbols.declare(&name, &kind, line) {
                self.emit(err, &loc);
            }
        }

        // Recurse into epistemic blocks
        for decl in decls {
            if let Declaration::Epistemic(eb) = decl {
                self.register_declarations(&eb.body);
            }
        }
    }

    // ── Phase 2: validation ──────────────────────────────────────

    fn check_declarations(&mut self, decls: &[Declaration]) {
        for decl in decls {
            match decl {
                Declaration::Persona(n) => self.check_persona(n),
                Declaration::Context(n) => self.check_context(n),
                Declaration::Anchor(n) => self.check_anchor(n),
                Declaration::Memory(n) => self.check_memory(n),
                Declaration::Tool(n) => self.check_tool(n),
                Declaration::Flow(n) => self.check_flow(n),
                Declaration::Intent(n) => self.check_intent(n),
                Declaration::Run(n) => self.check_run(n),
                Declaration::Epistemic(eb) => {
                    self.check_epistemic_mode(&eb.mode, &eb.loc);
                    self.check_declarations(&eb.body);
                }
                Declaration::LambdaData(n) => self.check_lambda_data(n),
                Declaration::Agent(n) => self.check_agent(n),
                Declaration::Shield(n) => self.check_shield(n),
                Declaration::Pix(n) => self.check_pix(n),
                Declaration::Psyche(n) => self.check_psyche(n),
                Declaration::Corpus(n) => self.check_corpus(n),
                Declaration::Dataspace(_) => {} // name-only, no field validation
                Declaration::Ots(n) => self.check_ots(n),
                Declaration::Mandate(n) => self.check_mandate(n),
                Declaration::Compute(_) => {} // no Python validation exists
                Declaration::Daemon(n) => self.check_daemon(n),
                Declaration::AxonStore(n) => self.check_axonstore(n),
                Declaration::AxonEndpoint(n) => self.check_axonendpoint(n),
                Declaration::Resource(n) => self.check_resource(n),
                Declaration::Fabric(n) => self.check_fabric(n),
                Declaration::Manifest(n) => self.check_manifest(n),
                Declaration::Observe(n) => self.check_observe(n),
                Declaration::Reconcile(n) => self.check_reconcile(n),
                Declaration::Lease(n) => self.check_lease(n),
                Declaration::Ensemble(n) => self.check_ensemble(n),
                Declaration::Session(n) => self.check_session(n),
                Declaration::Topology(n) => self.check_topology(n),
                Declaration::Socket(n) => self.check_socket(n),
                Declaration::Immune(n) => self.check_immune(n),
                Declaration::Reflex(n) => self.check_reflex(n),
                Declaration::Heal(n) => self.check_heal(n),
                Declaration::Component(n) => self.check_component(n),
                Declaration::View(n) => self.check_view(n),
                Declaration::Channel(n) => self.check_channel(n),
                Declaration::Import(_)
                | Declaration::Type(_)
                | Declaration::Let(_)
                | Declaration::Generic(_) => {}
            }
        }
    }

    // ── Per-construct checks ─────────────────────────────────────

    fn check_persona(&mut self, node: &PersonaDefinition) {
        if !node.tone.is_empty() && !is_valid(&node.tone, VALID_TONES) {
            self.emit(
                format!(
                    "Unknown tone '{}' for persona '{}'. Valid tones: {}",
                    node.tone,
                    node.name,
                    valid_list(VALID_TONES)
                ),
                &node.loc,
            );
        }
        if let Some(v) = node.confidence_threshold {
            self.check_range(v, 0.0, 1.0, "confidence_threshold", &node.loc);
        }
    }

    fn check_context(&mut self, node: &ContextDefinition) {
        if !node.memory_scope.is_empty() && !is_valid(&node.memory_scope, VALID_MEMORY_SCOPES) {
            self.emit(
                format!(
                    "Unknown memory scope '{}' in context '{}'. Valid: {}",
                    node.memory_scope,
                    node.name,
                    valid_list(VALID_MEMORY_SCOPES)
                ),
                &node.loc,
            );
        }
        if !node.depth.is_empty() && !is_valid(&node.depth, VALID_DEPTHS) {
            self.emit(
                format!(
                    "Unknown depth '{}' in context '{}'. Valid: {}",
                    node.depth,
                    node.name,
                    valid_list(VALID_DEPTHS)
                ),
                &node.loc,
            );
        }
        if let Some(v) = node.temperature {
            self.check_range(v, 0.0, 2.0, "temperature", &node.loc);
        }
        if let Some(v) = node.max_tokens {
            if v <= 0 {
                self.emit(
                    format!(
                        "max_tokens must be positive, got {} in context '{}'",
                        v, node.name
                    ),
                    &node.loc,
                );
            }
        }
    }

    fn check_anchor(&mut self, node: &AnchorConstraint) {
        if let Some(v) = node.confidence_floor {
            self.check_range(v, 0.0, 1.0, "confidence_floor", &node.loc);
        }
        if !node.on_violation.is_empty() && !is_valid(&node.on_violation, VALID_VIOLATION_ACTIONS) {
            self.emit(
                format!(
                    "Unknown on_violation action '{}' in anchor '{}'. Valid: {}",
                    node.on_violation,
                    node.name,
                    valid_list(VALID_VIOLATION_ACTIONS)
                ),
                &node.loc,
            );
        }
        if node.on_violation == "raise" && node.on_violation_target.is_empty() {
            self.emit(
                format!(
                    "Anchor '{}' uses 'raise' but no error type specified",
                    node.name
                ),
                &node.loc,
            );
        }
    }

    fn check_memory(&mut self, node: &MemoryDefinition) {
        if !node.store.is_empty() && !is_valid(&node.store, VALID_MEMORY_SCOPES) {
            self.emit(
                format!(
                    "Unknown store type '{}' in memory '{}'. Valid: {}",
                    node.store,
                    node.name,
                    valid_list(VALID_MEMORY_SCOPES)
                ),
                &node.loc,
            );
        }
        if !node.retrieval.is_empty() && !is_valid(&node.retrieval, VALID_RETRIEVAL_STRATEGIES) {
            self.emit(
                format!(
                    "Unknown retrieval strategy '{}' in memory '{}'. Valid: {}",
                    node.retrieval,
                    node.name,
                    valid_list(VALID_RETRIEVAL_STRATEGIES)
                ),
                &node.loc,
            );
        }
    }

    fn check_tool(&mut self, node: &ToolDefinition) {
        if let Some(v) = node.max_results {
            if v <= 0 {
                self.emit(
                    format!(
                        "max_results must be positive, got {} in tool '{}'",
                        v, node.name
                    ),
                    &node.loc,
                );
            }
        }
        if let Some(ref eff) = node.effects {
            for e in &eff.effects {
                // Handle composite effects like "name:qualifier"
                let (base, qualifier) = match e.split_once(':') {
                    Some((b, q)) => (b, Some(q)),
                    None => (e.as_str(), None),
                };
                if !is_valid(base, VALID_EFFECTS) {
                    self.emit(
                        format!(
                            "Unknown effect '{}' in tool '{}'. Valid: {}",
                            e,
                            node.name,
                            valid_list(VALID_EFFECTS)
                        ),
                        &node.loc,
                    );
                    continue;
                }
                // §λ-L-E Fase 11.a — qualifier enforcement for the
                // stream + trust effects. Both REQUIRE a qualifier
                // from their closed catalogue. Missing or unknown
                // qualifiers are compile errors.
                match base {
                    "stream" => match qualifier {
                        None => self.emit(
                            format!(
                                "Effect 'stream' in tool '{}' requires a \
                                 backpressure policy qualifier \
                                 'stream:<policy>'. Valid policies: {}",
                                node.name,
                                valid_list(crate::stream_effect::BACKPRESSURE_CATALOG)
                            ),
                            &node.loc,
                        ),
                        Some(q) => {
                            if !is_valid(q, crate::stream_effect::BACKPRESSURE_CATALOG) {
                                self.emit(
                                    format!(
                                        "Unknown backpressure policy '{}' in tool '{}'. \
                                         Valid: {}",
                                        q,
                                        node.name,
                                        valid_list(crate::stream_effect::BACKPRESSURE_CATALOG)
                                    ),
                                    &node.loc,
                                );
                            }
                        }
                    },
                    "trust" => match qualifier {
                        None => self.emit(
                            format!(
                                "Effect 'trust' in tool '{}' requires a proof \
                                 qualifier 'trust:<proof>'. Valid proofs: {}",
                                node.name,
                                valid_list(crate::refinement::TRUST_CATALOG)
                            ),
                            &node.loc,
                        ),
                        Some(q) => {
                            if !is_valid(q, crate::refinement::TRUST_CATALOG) {
                                self.emit(
                                    format!(
                                        "Unknown trust proof '{}' in tool '{}'. \
                                         Valid: {}",
                                        q,
                                        node.name,
                                        valid_list(crate::refinement::TRUST_CATALOG)
                                    ),
                                    &node.loc,
                                );
                            }
                        }
                    },
                    // §λ-L-E Fase 11.c — `sensitive:<category>` tags
                    // effects that touch regulated data. The category
                    // is an open taxonomy (adopters write
                    // `sensitive:health_data`, `sensitive:financial_txn`
                    // etc). The qualifier presence is REQUIRED — a
                    // bare `sensitive` is ambiguous and rejected.
                    "sensitive" => {
                        if qualifier.is_none() {
                            self.emit(
                                format!(
                                    "Effect 'sensitive' in tool '{}' \
                                     requires a jurisdiction qualifier \
                                     'sensitive:<category>' (e.g. \
                                     'sensitive:health_data'). The \
                                     category is adopter-defined; the \
                                     legal basis covering it must also \
                                     be declared via 'legal:<basis>' on \
                                     the same tool.",
                                    node.name,
                                ),
                                &node.loc,
                            );
                        }
                    }
                    // §λ-L-E Fase 11.c — `legal:<basis>` declares the
                    // legal basis authorising a sensitive effect. The
                    // basis catalogue is CLOSED.
                    "legal" => match qualifier {
                        None => self.emit(
                            format!(
                                "Effect 'legal' in tool '{}' requires a \
                                 basis qualifier 'legal:<basis>'. Valid \
                                 bases: {}",
                                node.name,
                                valid_list(crate::legal_basis::LEGAL_BASIS_CATALOG)
                            ),
                            &node.loc,
                        ),
                        Some(q) => {
                            if !is_valid(q, crate::legal_basis::LEGAL_BASIS_CATALOG) {
                                self.emit(
                                    format!(
                                        "Unknown legal basis '{}' in tool \
                                         '{}'. Valid: {}",
                                        q,
                                        node.name,
                                        valid_list(crate::legal_basis::LEGAL_BASIS_CATALOG)
                                    ),
                                    &node.loc,
                                );
                            }
                        }
                    },
                    // §λ-L-E Fase 11.e — OTS subkinds:
                    //   ots:transform:<from>:<to>  → kind-pair
                    //   ots:backend:<native|ffmpeg> → closed backend catalogue
                    "ots" => match qualifier {
                        None => self.emit(
                            format!(
                                "Effect 'ots' in tool '{}' requires a \
                                 subkind. Expected 'ots:transform:<from>:<to>' \
                                 or 'ots:backend:<native|ffmpeg>'.",
                                node.name
                            ),
                            &node.loc,
                        ),
                        Some(inner) => {
                            let (subkind, rest) = match inner.split_once(':') {
                                Some((a, b)) => (a, Some(b)),
                                None => (inner, None),
                            };
                            match subkind {
                                "transform" => {
                                    let valid = rest
                                        .and_then(|r| r.split_once(':'))
                                        .map(|(f, t)| !f.is_empty() && !t.is_empty())
                                        .unwrap_or(false);
                                    if !valid {
                                        self.emit(
                                            format!(
                                                "Effect 'ots:transform' in tool \
                                                 '{}' requires '<from>:<to>' \
                                                 qualifier (e.g. \
                                                 'ots:transform:mulaw8:pcm16').",
                                                node.name
                                            ),
                                            &node.loc,
                                        );
                                    }
                                }
                                "backend" => {
                                    let qual = rest.unwrap_or("");
                                    if !is_valid(qual, crate::ots_catalog::OTS_BACKEND_CATALOG) {
                                        self.emit(
                                            format!(
                                                "Unknown OTS backend '{}' in tool '{}'. \
                                                 Valid: {}",
                                                qual,
                                                node.name,
                                                valid_list(crate::ots_catalog::OTS_BACKEND_CATALOG)
                                            ),
                                            &node.loc,
                                        );
                                    }
                                }
                                other => self.emit(
                                    format!(
                                        "Unknown 'ots' subkind '{}' in tool '{}'. \
                                         Expected 'transform' or 'backend'.",
                                        other, node.name
                                    ),
                                    &node.loc,
                                ),
                            }
                        }
                    },
                    _ => {}
                }
            }
            if !eff.epistemic_level.is_empty()
                && !is_valid(&eff.epistemic_level, VALID_EPISTEMIC_LEVELS)
            {
                self.emit(
                    format!(
                        "Unknown epistemic level '{}' in tool '{}'. Valid: {}",
                        eff.epistemic_level,
                        node.name,
                        valid_list(VALID_EPISTEMIC_LEVELS)
                    ),
                    &node.loc,
                );
            }
        }

        // §λ-L-E Fase 11.a — tool output/input trust coherence.
        // When a tool's declared effects announce a trust proof, we
        // don't (yet) propagate it into the return-type refinement
        // since tools don't carry explicit return TypeExprs in this
        // AST tier. Tool-level trust claims are consumed by
        // `check_flow`'s refinement pass below.

        // Mirror for stream: if a tool declares stream:<policy>, the
        // flows that use it inherit the obligation — enforced in
        // `check_flow`.

        // §λ-L-E Fase 11.c — tool-level sensitive/legal coherence.
        // A tool declaring `sensitive:<category>` MUST also declare
        // at least one `legal:<basis>` from the closed catalogue.
        // Declaring `legal:<basis>` without a `sensitive:<category>`
        // is tolerated (some tools are authorised broadly without
        // processing regulated data).
        if let Some(ref eff) = node.effects {
            let mut sensitive_categories: Vec<&str> = Vec::new();
            let mut has_legal_basis = false;
            let mut legal_bases_hipaa: Vec<&str> = Vec::new();
            let mut has_ffmpeg_backend = false;
            for e in &eff.effects {
                let (base, qual) = match e.split_once(':') {
                    Some((b, q)) => (b, Some(q)),
                    None => (e.as_str(), None),
                };
                if base == "sensitive" {
                    if let Some(q) = qual {
                        sensitive_categories.push(q);
                    }
                }
                if base == "legal" {
                    if let Some(q) = qual {
                        if is_valid(q, crate::legal_basis::LEGAL_BASIS_CATALOG) {
                            has_legal_basis = true;
                            if q.starts_with("HIPAA.") {
                                legal_bases_hipaa.push(q);
                            }
                        }
                    }
                }
                if base == "ots" {
                    if let Some(inner) = qual {
                        if let Some(("backend", backend)) = inner.split_once(':') {
                            if backend == "ffmpeg" {
                                has_ffmpeg_backend = true;
                            }
                        }
                    }
                }
            }
            if !sensitive_categories.is_empty() && !has_legal_basis {
                self.emit(
                    format!(
                        "Tool '{}' declares sensitive effect(s) [{}] but \
                         carries no 'legal:<basis>' effect. Regulated \
                         processing requires an explicit legal basis: {}.",
                        node.name,
                        sensitive_categories.join(", "),
                        valid_list(crate::legal_basis::LEGAL_BASIS_CATALOG)
                    ),
                    &node.loc,
                );
            }

            // §λ-L-E Fase 11.e — HIPAA processing MUST stay in-process.
            // Spawning ffmpeg crosses a process boundary the auditor
            // cannot observe; the ePHI disclosure the BAA doesn't
            // cover. Rejected at compile time, per the same closed
            // posture as 11.a trust proofs and 11.c legal bases.
            if !legal_bases_hipaa.is_empty() && has_ffmpeg_backend {
                self.emit(
                    format!(
                        "Tool '{}' combines HIPAA legal basis ({}) with \
                         'ots:backend:ffmpeg'. ePHI MUST NOT cross the \
                         process boundary to a subprocess outside the \
                         auditable runtime. Use 'ots:backend:native' or \
                         register a native transformer that covers the \
                         required pipeline.",
                        node.name,
                        legal_bases_hipaa.join(", "),
                    ),
                    &node.loc,
                );
            }
        }
    }

    fn check_flow(&mut self, node: &FlowDefinition) {
        // §Fase 38.d (D2) — capture the flow's parameter-name → type
        // map for the duration of this flow's body check. Cleared
        // before/after so one flow's params can't leak into another's
        // §38.d proof.
        self.current_flow_params = crate::store_column_proof::FlowParamTypes::new();
        for param in &node.parameters {
            self.current_flow_params
                .insert(param.name.clone(), param.type_expr.name.clone());
        }

        // Validate parameter types
        for param in &node.parameters {
            self.check_type_reference(&param.type_expr.name, &param.loc);
        }
        // Validate return type
        if let Some(ref rt) = node.return_type {
            self.check_type_reference(&rt.name, &rt.loc);
        }

        let mut step_names: Vec<String> = Vec::new();
        for step in &node.body {
            if let FlowStep::Step(s) = step {
                if step_names.contains(&s.name) {
                    self.emit(
                        format!("Duplicate step name '{}' in flow '{}'", s.name, node.name),
                        &s.loc,
                    );
                } else {
                    step_names.push(s.name.clone());
                }
                if let Some(v) = s.confidence_floor {
                    self.check_range(v, 0.0, 1.0, "confidence_floor", &s.loc);
                }
            }
        }

        // Tier 2 flow step reference checks
        self.check_flow_steps(&node.body, &node.name);

        // §λ-L-E Fase 11.a — Temporal Algebraic Effects + Trust
        // Types. Enforce two contracts at the flow level:
        //
        //   1. Stream<T> in parameter/return obliges the flow's body
        //      to reach a tool that carries a `stream:<policy>` effect.
        //      Without it, we cannot guarantee the stream has a
        //      backpressure handler — compile error.
        //
        //   2. Untrusted<T> in parameter obliges the flow's body to
        //      reach a tool that carries a `trust:<proof>` effect —
        //      otherwise the untrusted payload is being consumed
        //      without verification.
        self.check_refinement_and_stream_contracts(node);
    }

    // ── §λ-L-E Fase 11.a — refinement + stream flow-level checks ─

    fn check_refinement_and_stream_contracts(&mut self, flow: &FlowDefinition) {
        // Scan flow signature for the refinement / stream markers.
        // `Trusted<T>` in a parameter imposes no new obligation on
        // this flow (the upstream already proved trust). `Untrusted<T>`
        // in a parameter obliges the flow body to refine it.
        let mut uses_stream = false;
        let mut uses_untrusted = false;

        for param in &flow.parameters {
            if crate::stream_effect::is_stream_type(&param.type_expr.name) {
                uses_stream = true;
            }
            if crate::refinement::is_untrusted_type(&param.type_expr.name) {
                uses_untrusted = true;
            }
        }
        if let Some(ref rt) = flow.return_type {
            if crate::stream_effect::is_stream_type(&rt.name) {
                uses_stream = true;
            }
            // Returning `Untrusted<T>` is legal (the flow is a pure
            // acceptor / pass-through) — the downstream consumer
            // carries the refinement obligation.
        }

        if !uses_stream && !uses_untrusted {
            return;
        }

        // Build {tool_name → Vec<effect_string>} by scanning the
        // program's declarations. Owned strings sidestep lifetime
        // gymnastics; the program-wide walk is O(N_tools) and the
        // strings are short slugs, so the allocation cost is negligible
        // for this checker pass.
        let mut tool_effects: std::collections::HashMap<String, Vec<String>> =
            std::collections::HashMap::new();
        self.collect_tool_effects(&self.program.declarations, &mut tool_effects);

        // Walk the flow body and see which tools each step reaches
        // via `apply_ref` / `navigate_ref`. Record the effects we
        // witness.
        let mut observed_backpressure = false;
        let mut observed_trust_proof = false;
        self.walk_flow_steps_for_effects(
            &flow.body,
            &tool_effects,
            &mut observed_backpressure,
            &mut observed_trust_proof,
        );

        if uses_stream && !observed_backpressure {
            self.emit(
                format!(
                    "Flow '{}' uses 'Stream<T>' in its signature but no \
                     reachable tool declares a 'stream:<policy>' effect. \
                     Every Stream<T> needs a backpressure policy: {}. \
                     Declare the policy on the tool that produces or \
                     consumes the stream (e.g. `effects: [stream:drop_oldest]`).",
                    flow.name,
                    valid_list(crate::stream_effect::BACKPRESSURE_CATALOG)
                ),
                &flow.loc,
            );
        }
        if uses_untrusted && !observed_trust_proof {
            self.emit(
                format!(
                    "Flow '{}' accepts 'Untrusted<T>' in its signature but \
                     no reachable tool declares a 'trust:<proof>' effect. \
                     Untrusted payloads MUST be refined via one of the \
                     catalogue verifiers: {}. Add the appropriate effect \
                     to the verifier tool (e.g. `effects: [trust:hmac]`).",
                    flow.name,
                    valid_list(crate::refinement::TRUST_CATALOG)
                ),
                &flow.loc,
            );
        }
    }

    fn collect_tool_effects(
        &self,
        decls: &[Declaration],
        out: &mut std::collections::HashMap<String, Vec<String>>,
    ) {
        for d in decls {
            match d {
                Declaration::Tool(t) => {
                    if let Some(ref eff) = t.effects {
                        out.insert(t.name.clone(), eff.effects.clone());
                    }
                }
                Declaration::Epistemic(eb) => {
                    self.collect_tool_effects(&eb.body, out);
                }
                _ => {}
            }
        }
    }

    fn walk_flow_steps_for_effects(
        &self,
        steps: &[FlowStep],
        tool_effects: &std::collections::HashMap<String, Vec<String>>,
        observed_backpressure: &mut bool,
        observed_trust_proof: &mut bool,
    ) {
        for step in steps {
            match step {
                FlowStep::Step(s) => {
                    for tool_ref in [&s.apply_ref, &s.navigate_ref] {
                        if tool_ref.is_empty() {
                            continue;
                        }
                        if let Some(effs) = tool_effects.get(tool_ref) {
                            for e in effs {
                                let (base, qual) = match e.split_once(':') {
                                    Some((b, q)) => (b, Some(q)),
                                    None => (e.as_str(), None),
                                };
                                if base == "stream" {
                                    if let Some(q) = qual {
                                        if is_valid(q, crate::stream_effect::BACKPRESSURE_CATALOG) {
                                            *observed_backpressure = true;
                                        }
                                    }
                                }
                                if base == "trust" {
                                    if let Some(q) = qual {
                                        if is_valid(q, crate::refinement::TRUST_CATALOG) {
                                            *observed_trust_proof = true;
                                        }
                                    }
                                }
                            }
                        }
                    }
                }
                FlowStep::If(c) => {
                    self.walk_flow_steps_for_effects(
                        &c.then_body,
                        tool_effects,
                        observed_backpressure,
                        observed_trust_proof,
                    );
                    self.walk_flow_steps_for_effects(
                        &c.else_body,
                        tool_effects,
                        observed_backpressure,
                        observed_trust_proof,
                    );
                }
                FlowStep::ForIn(f) => {
                    self.walk_flow_steps_for_effects(
                        &f.body,
                        tool_effects,
                        observed_backpressure,
                        observed_trust_proof,
                    );
                }
                _ => {}
            }
        }
    }

    fn check_intent(&mut self, node: &IntentNode) {
        if node.ask.is_empty() {
            self.emit(
                format!(
                    "Intent '{}' is missing required 'ask' field — every intent must express a question",
                    node.name
                ),
                &node.loc,
            );
        }
        if let Some(v) = node.confidence_floor {
            self.check_range(v, 0.0, 1.0, "confidence_floor", &node.loc);
        }
    }

    fn check_run(&mut self, node: &RunStatement) {
        // Flow must exist and be a flow
        if !node.flow_name.is_empty() {
            match self.symbols.lookup(&node.flow_name) {
                None => self.emit(
                    format!("Undefined flow '{}' in run statement", node.flow_name),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "flow" => self.emit(
                    format!(
                        "'{}' is a {}, not a flow — only flows can be run",
                        node.flow_name, sym.kind
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }

        // Persona must exist
        if !node.persona.is_empty() {
            match self.symbols.lookup(&node.persona) {
                None => self.emit(format!("Undefined persona '{}'", node.persona), &node.loc),
                Some(sym) if sym.kind != "persona" => self.emit(
                    format!("'{}' is a {}, not a persona", node.persona, sym.kind),
                    &node.loc,
                ),
                _ => {}
            }
        }

        // Context must exist
        if !node.context.is_empty() {
            match self.symbols.lookup(&node.context) {
                None => self.emit(format!("Undefined context '{}'", node.context), &node.loc),
                Some(sym) if sym.kind != "context" => self.emit(
                    format!("'{}' is a {}, not a context", node.context, sym.kind),
                    &node.loc,
                ),
                _ => {}
            }
        }

        // Anchors must exist
        for anchor_name in &node.anchors {
            match self.symbols.lookup(anchor_name) {
                None => self.emit(format!("Undefined anchor '{}'", anchor_name), &node.loc),
                Some(sym) if sym.kind != "anchor" => self.emit(
                    format!("'{}' is a {}, not an anchor", anchor_name, sym.kind),
                    &node.loc,
                ),
                _ => {}
            }
        }

        // Effort validation
        if !node.effort.is_empty() && !is_valid(&node.effort, VALID_EFFORT_LEVELS) {
            self.emit(
                format!(
                    "Unknown effort level '{}'. Valid: {}",
                    node.effort,
                    valid_list(VALID_EFFORT_LEVELS)
                ),
                &node.loc,
            );
        }
    }

    // ── Lambda Data (ΛD) — 4 Invariants + Epistemic Degradation ──

    fn check_lambda_data(&mut self, node: &LambdaDataDefinition) {
        // Invariant 1 — Ontological Rigidity: ontology field is mandatory
        if node.ontology.is_empty() {
            self.emit(
                format!(
                    "lambda '{}' requires an 'ontology' field \
                     (Ontological Rigidity: O must classify the data domain)",
                    node.name
                ),
                &node.loc,
            );
        }

        // Invariant 4 — Epistemic Bounding: certainty ∈ [0, 1]
        if node.certainty < 0.0 || node.certainty > 1.0 {
            self.emit(
                format!(
                    "certainty coefficient must be in [0, 1], got {} \
                     (lambda '{}', Epistemic Bounding)",
                    node.certainty, node.name
                ),
                &node.loc,
            );
        }

        // Derivation validity: δ ∈ Δ
        if !node.derivation.is_empty() && !is_valid(&node.derivation, VALID_DERIVATIONS) {
            self.emit(
                format!(
                    "Unknown derivation '{}' for lambda '{}'. Valid: {}",
                    node.derivation,
                    node.name,
                    valid_list(VALID_DERIVATIONS)
                ),
                &node.loc,
            );
        }

        // Theorem 5.1 — Epistemic Degradation: only 'raw' may carry c = 1.0
        if node.certainty == 1.0 && !node.derivation.is_empty() && node.derivation != "raw" {
            self.emit(
                format!(
                    "Epistemic Degradation Theorem violation: lambda '{}' \
                     has certainty=1.0 with derivation='{}'. \
                     Only 'raw' data may carry absolute certainty (c=1.0). \
                     Derived/inferred/aggregated data must have c < 1.0 \
                     (\u{2200}\u{039b}D\u{2081}\u{2218}\u{039b}D\u{2082}: c_composed \u{2264} min(c\u{2081}, c\u{2082}))",
                    node.name, node.derivation
                ),
                &node.loc,
            );
        }
    }

    // ── Tier 2 declaration checks ───────────────────────────────────

    fn check_agent(&mut self, node: &AgentDefinition) {
        // BDI requirement: every agent must declare a goal
        if node.goal.is_empty() {
            self.emit(
                format!("Agent '{}' requires a 'goal' field (BDI: every agent must declare a desired objective)", node.name),
                &node.loc,
            );
        }

        // Tool references must exist
        for tool_name in &node.tools {
            match self.symbols.lookup(tool_name) {
                None => self.emit(
                    format!("Undefined tool '{}' in agent '{}'", tool_name, node.name),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "tool" => self.emit(
                    format!(
                        "'{}' is a {}, not a tool (referenced in agent '{}')",
                        tool_name, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }

        // Strategy enum
        if !node.strategy.is_empty() && !is_valid(&node.strategy, VALID_AGENT_STRATEGIES) {
            self.emit(
                format!(
                    "Unknown strategy '{}' in agent '{}'. Valid: {}",
                    node.strategy,
                    node.name,
                    valid_list(VALID_AGENT_STRATEGIES)
                ),
                &node.loc,
            );
        }

        // on_stuck policy enum
        if !node.on_stuck.is_empty() && !is_valid(&node.on_stuck, VALID_ON_STUCK_POLICIES) {
            self.emit(
                format!(
                    "Unknown on_stuck policy '{}' in agent '{}'. Valid: {}",
                    node.on_stuck,
                    node.name,
                    valid_list(VALID_ON_STUCK_POLICIES)
                ),
                &node.loc,
            );
        }

        // Memory reference
        if !node.memory_ref.is_empty() {
            match self.symbols.lookup(&node.memory_ref) {
                None => self.emit(
                    format!(
                        "Undefined memory '{}' in agent '{}'",
                        node.memory_ref, node.name
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "memory" => self.emit(
                    format!(
                        "'{}' is a {}, not a memory (referenced in agent '{}')",
                        node.memory_ref, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }

        // Shield reference
        if !node.shield_ref.is_empty() {
            match self.symbols.lookup(&node.shield_ref) {
                None => self.emit(
                    format!(
                        "Undefined shield '{}' in agent '{}'",
                        node.shield_ref, node.name
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "shield" => self.emit(
                    format!(
                        "'{}' is a {}, not a shield (referenced in agent '{}')",
                        node.shield_ref, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }

        // Budget constraints (linear logic: resources must be positive)
        if let Some(v) = node.max_iterations {
            if v < 1 {
                self.emit(
                    format!(
                        "max_iterations must be >= 1, got {} in agent '{}'",
                        v, node.name
                    ),
                    &node.loc,
                );
            }
        }
        if let Some(v) = node.max_tokens {
            if v < 0 {
                self.emit(
                    format!(
                        "max_tokens must be >= 0, got {} in agent '{}'",
                        v, node.name
                    ),
                    &node.loc,
                );
            }
        }
        if let Some(v) = node.max_cost {
            if v < 0.0 {
                self.emit(
                    format!("max_cost must be >= 0, got {} in agent '{}'", v, node.name),
                    &node.loc,
                );
            }
        }
    }

    fn check_shield(&mut self, node: &ShieldDefinition) {
        // Scan categories
        for cat in &node.scan {
            if !is_valid(cat, VALID_SCAN_CATEGORIES) {
                self.emit(
                    format!(
                        "Unknown scan category '{}' in shield '{}'. Valid: {}",
                        cat,
                        node.name,
                        valid_list(VALID_SCAN_CATEGORIES)
                    ),
                    &node.loc,
                );
            }
        }

        // Strategy enum
        if !node.strategy.is_empty() && !is_valid(&node.strategy, VALID_SHIELD_STRATEGIES) {
            self.emit(
                format!(
                    "Unknown strategy '{}' in shield '{}'. Valid: {}",
                    node.strategy,
                    node.name,
                    valid_list(VALID_SHIELD_STRATEGIES)
                ),
                &node.loc,
            );
        }

        // on_breach policy
        if !node.on_breach.is_empty() && !is_valid(&node.on_breach, VALID_ON_BREACH_POLICIES) {
            self.emit(
                format!(
                    "Unknown on_breach policy '{}' in shield '{}'. Valid: {}",
                    node.on_breach,
                    node.name,
                    valid_list(VALID_ON_BREACH_POLICIES)
                ),
                &node.loc,
            );
        }

        // Severity level
        if !node.severity.is_empty() && !is_valid(&node.severity, VALID_SEVERITY_LEVELS) {
            self.emit(
                format!(
                    "Unknown severity '{}' in shield '{}'. Valid: {}",
                    node.severity,
                    node.name,
                    valid_list(VALID_SEVERITY_LEVELS)
                ),
                &node.loc,
            );
        }

        // max_retries >= 0
        if let Some(v) = node.max_retries {
            if v < 0 {
                self.emit(
                    format!(
                        "max_retries must be >= 0, got {} in shield '{}'",
                        v, node.name
                    ),
                    &node.loc,
                );
            }
        }

        // confidence_threshold range
        if let Some(v) = node.confidence_threshold {
            self.check_range(v, 0.0, 1.0, "confidence_threshold", &node.loc);
        }

        // allow/deny overlap
        for tool in &node.allow_tools {
            if node.deny_tools.contains(tool) {
                self.emit(
                    format!(
                        "Tool '{}' appears in both allow_tools and deny_tools in shield '{}'",
                        tool, node.name
                    ),
                    &node.loc,
                );
            }
        }
    }

    fn check_pix(&mut self, node: &PixDefinition) {
        // Source presence
        if node.source.is_empty() {
            self.emit(
                format!("Pix '{}' requires a 'source' field", node.name),
                &node.loc,
            );
        }

        // Depth range 1..=8
        if let Some(v) = node.depth {
            if v < 1 || v > 8 {
                self.emit(
                    format!(
                        "depth must be between 1 and 8, got {} in pix '{}'",
                        v, node.name
                    ),
                    &node.loc,
                );
            }
        }

        // Branching range 1..=10
        if let Some(v) = node.branching {
            if v < 1 || v > 10 {
                self.emit(
                    format!(
                        "branching must be between 1 and 10, got {} in pix '{}'",
                        v, node.name
                    ),
                    &node.loc,
                );
            }
        }
    }

    fn check_psyche(&mut self, node: &PsycheDefinition) {
        // §1: ψ ∈ M requires dim(M) ≥ 1
        if node.dimensions.is_empty() {
            self.emit(
                format!(
                    "Psyche '{}' requires at least one dimension (manifold dim ≥ 1)",
                    node.name
                ),
                &node.loc,
            );
        }

        // Duplicate dimension detection
        let mut seen: Vec<String> = Vec::new();
        for dim in &node.dimensions {
            if seen.contains(dim) {
                self.emit(
                    format!("Duplicate dimension '{}' in psyche '{}'", dim, node.name),
                    &node.loc,
                );
            } else {
                seen.push(dim.clone());
            }
        }

        // Manifold noise σ ∈ (0, 1]
        if let Some(v) = node.manifold_noise {
            if v <= 0.0 || v > 1.0 {
                self.emit(
                    format!(
                        "manifold_noise must be in (0.0, 1.0], got {} in psyche '{}'",
                        v, node.name
                    ),
                    &node.loc,
                );
            }
        }

        // Manifold momentum β ∈ [0, 1]
        if let Some(v) = node.manifold_momentum {
            self.check_range(v, 0.0, 1.0, "manifold_momentum", &node.loc);
        }

        // Safety constraints non-empty
        if node.safety_constraints.is_empty() {
            self.emit(
                format!(
                    "Psyche '{}' requires at least one safety_constraint",
                    node.name
                ),
                &node.loc,
            );
        } else if !node
            .safety_constraints
            .iter()
            .any(|c| c == "non_diagnostic")
        {
            // §4: non_diagnostic is mandatory
            self.emit(
                format!("Psyche '{}' must include 'non_diagnostic' in safety_constraints (dependent type safety §4)", node.name),
                &node.loc,
            );
        }

        // Inference mode enum
        if !node.inference_mode.is_empty() && !is_valid(&node.inference_mode, VALID_INFERENCE_MODES)
        {
            self.emit(
                format!(
                    "Unknown inference_mode '{}' in psyche '{}'. Valid: {}",
                    node.inference_mode,
                    node.name,
                    valid_list(VALID_INFERENCE_MODES)
                ),
                &node.loc,
            );
        }
    }

    fn check_corpus(&mut self, node: &CorpusDefinition) {
        // Invariant G1: D ≠ ∅ — at least one document
        if node.documents.is_empty() && node.mcp_server.is_empty() {
            self.emit(
                format!(
                    "Corpus '{}' requires at least one document or an mcp_server (G1: D ≠ ∅)",
                    node.name
                ),
                &node.loc,
            );
        }
    }

    fn check_ots(&mut self, node: &OtsDefinition) {
        // Teleology presence (goal required)
        if node.teleology.is_empty() {
            self.emit(
                format!(
                    "OTS '{}' requires a 'teleology' field (goal required)",
                    node.name
                ),
                &node.loc,
            );
        }

        // Homotopy search enum
        if !node.homotopy_search.is_empty() && !is_valid(&node.homotopy_search, VALID_OTS_HOMOTOPY)
        {
            self.emit(
                format!(
                    "Unknown homotopy_search '{}' in OTS '{}'. Valid: {}",
                    node.homotopy_search,
                    node.name,
                    valid_list(VALID_OTS_HOMOTOPY)
                ),
                &node.loc,
            );
        }
    }

    fn check_mandate(&mut self, node: &MandateDefinition) {
        // Constraint presence (refinement type T_M)
        if node.constraint.is_empty() {
            self.emit(
                format!("Mandate '{}' requires a 'constraint' field (refinement type T_M = {{x ∈ Σ* | M(x) ⊢ ⊤}})", node.name),
                &node.loc,
            );
        }

        // PID gains
        if let Some(v) = node.kp {
            if v <= 0.0 {
                self.emit(
                    format!("kp must be > 0.0, got {} in mandate '{}'", v, node.name),
                    &node.loc,
                );
            }
        }
        if let Some(v) = node.ki {
            if v < 0.0 {
                self.emit(
                    format!("ki must be >= 0.0, got {} in mandate '{}'", v, node.name),
                    &node.loc,
                );
            }
        }
        if let Some(v) = node.kd {
            if v < 0.0 {
                self.emit(
                    format!("kd must be >= 0.0, got {} in mandate '{}'", v, node.name),
                    &node.loc,
                );
            }
        }

        // Tolerance ε ∈ (0, 1]
        if let Some(v) = node.tolerance {
            if v <= 0.0 || v > 1.0 {
                self.emit(
                    format!(
                        "tolerance must be in (0.0, 1.0], got {} in mandate '{}'",
                        v, node.name
                    ),
                    &node.loc,
                );
            }
        }

        // max_steps >= 1
        if let Some(v) = node.max_steps {
            if v < 1 {
                self.emit(
                    format!(
                        "max_steps must be >= 1, got {} in mandate '{}'",
                        v, node.name
                    ),
                    &node.loc,
                );
            }
        }

        // on_violation policy
        if !node.on_violation.is_empty() && !is_valid(&node.on_violation, VALID_MANDATE_POLICIES) {
            self.emit(
                format!(
                    "Unknown on_violation '{}' in mandate '{}'. Valid: {}",
                    node.on_violation,
                    node.name,
                    valid_list(VALID_MANDATE_POLICIES)
                ),
                &node.loc,
            );
        }
    }

    fn check_axonstore(&mut self, node: &AxonStoreDefinition) {
        // Backend enum
        if !node.backend.is_empty() && !is_valid(&node.backend, VALID_STORE_BACKENDS) {
            self.emit(
                format!(
                    "Unknown backend '{}' in axonstore '{}'. Valid: {}",
                    node.backend,
                    node.name,
                    valid_list(VALID_STORE_BACKENDS)
                ),
                &node.loc,
            );
        }

        // Isolation level enum
        if !node.isolation.is_empty() && !is_valid(&node.isolation, VALID_STORE_ISOLATION) {
            self.emit(
                format!(
                    "Unknown isolation '{}' in axonstore '{}'. Valid: {}",
                    node.isolation,
                    node.name,
                    valid_list(VALID_STORE_ISOLATION)
                ),
                &node.loc,
            );
        }

        // on_breach policy
        if !node.on_breach.is_empty() && !is_valid(&node.on_breach, VALID_STORE_ON_BREACH) {
            self.emit(
                format!(
                    "Unknown on_breach '{}' in axonstore '{}'. Valid: {}",
                    node.on_breach,
                    node.name,
                    valid_list(VALID_STORE_ON_BREACH)
                ),
                &node.loc,
            );
        }

        // confidence_floor range
        if let Some(v) = node.confidence_floor {
            self.check_range(v, 0.0, 1.0, "confidence_floor", &node.loc);
        }
    }

    /// §λ-L-E Fase 1 — Resource validation.
    ///
    /// Enforces: (a) lifetime ∈ {linear | affine | persistent}; (b) certainty_floor
    /// ∈ [0.0, 1.0] when present; (c) shield_ref, if non-empty, is a declared shield.
    fn check_resource(&mut self, node: &ResourceDefinition) {
        if !node.lifetime.is_empty()
            && !matches!(node.lifetime.as_str(), "linear" | "affine" | "persistent")
        {
            self.emit(
                format!(
                    "Invalid lifetime '{}' for resource '{}' — \
                     expected linear | affine | persistent",
                    node.lifetime, node.name
                ),
                &node.loc,
            );
        }
        if let Some(c) = node.certainty_floor {
            if !(0.0..=1.0).contains(&c) {
                self.emit(
                    format!(
                        "certainty_floor {c} for resource '{}' is out of range [0.0, 1.0]",
                        node.name
                    ),
                    &node.loc,
                );
            }
        }
        if !node.shield_ref.is_empty() {
            match self.symbols.lookup(&node.shield_ref) {
                None => self.emit(
                    format!(
                        "Undefined shield '{}' in resource '{}'",
                        node.shield_ref, node.name
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "shield" => self.emit(
                    format!(
                        "'{}' is a {}, not a shield (referenced in resource '{}')",
                        node.shield_ref, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
    }

    /// §λ-L-E Fase 1 — Fabric validation.
    ///
    /// Enforces: (a) zones ≥ 1 when present; (b) shield_ref, if non-empty,
    /// is a declared shield.
    fn check_fabric(&mut self, node: &FabricDefinition) {
        if let Some(z) = node.zones {
            if z < 1 {
                self.emit(
                    format!(
                        "Fabric '{}' has invalid zones {z} — must be >= 1",
                        node.name
                    ),
                    &node.loc,
                );
            }
        }
        if !node.shield_ref.is_empty() {
            match self.symbols.lookup(&node.shield_ref) {
                None => self.emit(
                    format!(
                        "Undefined shield '{}' in fabric '{}'",
                        node.shield_ref, node.name
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "shield" => self.emit(
                    format!(
                        "'{}' is a {}, not a shield (referenced in fabric '{}')",
                        node.shield_ref, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
    }

    /// §λ-L-E Fase 1 — Manifest validation.
    ///
    /// Enforces: (a) every name in `resources` refers to a declared resource;
    /// (b) `fabric_ref`, if non-empty, is a declared fabric; (c) no duplicate
    /// resource names within a single manifest (Separation Logic `*` disjointness
    /// within-manifest — cross-manifest aliasing is a separate check).
    fn check_manifest(&mut self, node: &ManifestDefinition) {
        // (a) resource references must resolve
        let mut seen: std::collections::HashSet<&String> = std::collections::HashSet::new();
        for res_name in &node.resources {
            if !seen.insert(res_name) {
                self.emit(
                    format!(
                        "Manifest '{}' lists resource '{}' more than once \
                         (Linear/Separation Logic disjointness)",
                        node.name, res_name
                    ),
                    &node.loc,
                );
                continue;
            }
            match self.symbols.lookup(res_name) {
                None => self.emit(
                    format!(
                        "Manifest '{}' references undefined resource '{}'",
                        node.name, res_name
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "resource" => self.emit(
                    format!(
                        "'{}' is a {}, not a resource (referenced in manifest '{}')",
                        res_name, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        // (b) fabric reference
        if !node.fabric_ref.is_empty() {
            match self.symbols.lookup(&node.fabric_ref) {
                None => self.emit(
                    format!(
                        "Manifest '{}' references undefined fabric '{}'",
                        node.name, node.fabric_ref
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "fabric" => self.emit(
                    format!(
                        "'{}' is a {}, not a fabric (referenced in manifest '{}')",
                        node.fabric_ref, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        if let Some(z) = node.zones {
            if z < 1 {
                self.emit(
                    format!(
                        "Manifest '{}' has invalid zones {z} — must be >= 1",
                        node.name
                    ),
                    &node.loc,
                );
            }
        }
    }

    /// §λ-L-E Fase 1 — Observe validation.
    ///
    /// Enforces: (a) `target` refers to a declared manifest; (b) certainty_floor
    /// ∈ [0.0, 1.0] when present; (c) quorum ≥ 1 when present; (d) on_partition
    /// ∈ {fail, shield_quarantine}; (e) `sources` is non-empty.
    fn check_observe(&mut self, node: &ObserveDefinition) {
        // (a) target manifest
        if node.target.is_empty() {
            self.emit(
                format!(
                    "Observe '{}' is missing 'from <Manifest>' target",
                    node.name
                ),
                &node.loc,
            );
        } else {
            match self.symbols.lookup(&node.target) {
                None => self.emit(
                    format!(
                        "Observe '{}' targets undefined manifest '{}'",
                        node.name, node.target
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "manifest" => self.emit(
                    format!(
                        "'{}' is a {}, not a manifest (observed by '{}')",
                        node.target, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        // (b) certainty floor range
        if let Some(c) = node.certainty_floor {
            if !(0.0..=1.0).contains(&c) {
                self.emit(
                    format!(
                        "certainty_floor {c} for observe '{}' is out of range [0.0, 1.0]",
                        node.name
                    ),
                    &node.loc,
                );
            }
        }
        // (c) quorum
        if let Some(q) = node.quorum {
            if q < 1 {
                self.emit(
                    format!(
                        "Observe '{}' has invalid quorum {q} — must be >= 1",
                        node.name
                    ),
                    &node.loc,
                );
            }
        }
        // (d) on_partition enum
        if !node.on_partition.is_empty()
            && !matches!(node.on_partition.as_str(), "fail" | "shield_quarantine")
        {
            self.emit(
                format!(
                    "Invalid on_partition '{}' for observe '{}' — \
                     expected fail | shield_quarantine",
                    node.on_partition, node.name
                ),
                &node.loc,
            );
        }
        // (e) sources must be non-empty
        if node.sources.is_empty() {
            self.emit(
                format!("Observe '{}' has empty sources: list", node.name),
                &node.loc,
            );
        }
    }

    /// §λ-L-E Fase 3 — Reconcile validation.
    ///
    /// Enforces: (a) observe_ref refers to a declared observe; (b) threshold
    /// and tolerance ∈ [0.0, 1.0]; (c) shield_ref / mandate_ref (if present)
    /// resolve to correct kinds; (d) max_retries ≥ 0.
    fn check_reconcile(&mut self, node: &ReconcileDefinition) {
        if node.observe_ref.is_empty() {
            self.emit(
                format!("Reconcile '{}' is missing 'observe:' target", node.name),
                &node.loc,
            );
        } else {
            match self.symbols.lookup(&node.observe_ref) {
                None => self.emit(
                    format!(
                        "Reconcile '{}' references undefined observe '{}'",
                        node.name, node.observe_ref
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "observe" => self.emit(
                    format!(
                        "'{}' is a {}, not an observe (referenced in reconcile '{}')",
                        node.observe_ref, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        if let Some(t) = node.threshold {
            if !(0.0..=1.0).contains(&t) {
                self.emit(
                    format!(
                        "threshold {t} for reconcile '{}' is out of range [0.0, 1.0]",
                        node.name
                    ),
                    &node.loc,
                );
            }
        }
        if let Some(t) = node.tolerance {
            if !(0.0..=1.0).contains(&t) {
                self.emit(
                    format!(
                        "tolerance {t} for reconcile '{}' is out of range [0.0, 1.0]",
                        node.name
                    ),
                    &node.loc,
                );
            }
        }
        if node.max_retries < 0 {
            self.emit(
                format!(
                    "Reconcile '{}' has invalid max_retries {} — must be >= 0",
                    node.name, node.max_retries
                ),
                &node.loc,
            );
        }
        if !node.shield_ref.is_empty() {
            match self.symbols.lookup(&node.shield_ref) {
                None => self.emit(
                    format!(
                        "Undefined shield '{}' in reconcile '{}'",
                        node.shield_ref, node.name
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "shield" => self.emit(
                    format!(
                        "'{}' is a {}, not a shield (referenced in reconcile '{}')",
                        node.shield_ref, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        if !node.mandate_ref.is_empty() {
            match self.symbols.lookup(&node.mandate_ref) {
                None => self.emit(
                    format!(
                        "Undefined mandate '{}' in reconcile '{}'",
                        node.mandate_ref, node.name
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "mandate" => self.emit(
                    format!(
                        "'{}' is a {}, not a mandate (referenced in reconcile '{}')",
                        node.mandate_ref, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
    }

    /// §λ-L-E Fase 3 — Lease validation.
    ///
    /// Enforces: (a) resource_ref resolves to a declared resource; (b) duration
    /// is non-empty; (c) acquire / on_expire enums are already validated at
    /// parse time but we re-check symbolically for defence-in-depth.
    fn check_lease(&mut self, node: &LeaseDefinition) {
        if node.resource_ref.is_empty() {
            self.emit(
                format!("Lease '{}' is missing 'resource:' target", node.name),
                &node.loc,
            );
        } else {
            match self.symbols.lookup(&node.resource_ref) {
                None => self.emit(
                    format!(
                        "Lease '{}' references undefined resource '{}'",
                        node.name, node.resource_ref
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "resource" => self.emit(
                    format!(
                        "'{}' is a {}, not a resource (leased by '{}')",
                        node.resource_ref, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        if node.duration.is_empty() {
            self.emit(
                format!("Lease '{}' is missing 'duration:' field", node.name),
                &node.loc,
            );
        }
    }

    /// §λ-L-E Fase 3 — Ensemble validation.
    ///
    /// Enforces: (a) each observation name refers to a declared observe;
    /// (b) quorum ≥ 1 and ≤ len(observations); (c) at least 2 observations
    /// are required for a meaningful Byzantine ensemble.
    fn check_ensemble(&mut self, node: &EnsembleDefinition) {
        if node.observations.is_empty() {
            self.emit(
                format!("Ensemble '{}' has empty observations: list", node.name),
                &node.loc,
            );
            return;
        }
        if node.observations.len() < 2 {
            self.emit(
                format!(
                    "Ensemble '{}' has {} observation(s); Byzantine quorum requires >= 2",
                    node.name,
                    node.observations.len()
                ),
                &node.loc,
            );
        }
        let mut seen: std::collections::HashSet<&String> = std::collections::HashSet::new();
        for obs_name in &node.observations {
            if !seen.insert(obs_name) {
                self.emit(
                    format!(
                        "Ensemble '{}' lists observation '{}' more than once",
                        node.name, obs_name
                    ),
                    &node.loc,
                );
                continue;
            }
            match self.symbols.lookup(obs_name) {
                None => self.emit(
                    format!(
                        "Ensemble '{}' references undefined observation '{}'",
                        node.name, obs_name
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "observe" => self.emit(
                    format!(
                        "'{}' is a {}, not an observe (referenced in ensemble '{}')",
                        obs_name, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        if let Some(q) = node.quorum {
            if q < 1 {
                self.emit(
                    format!(
                        "Ensemble '{}' has invalid quorum {q} — must be >= 1",
                        node.name
                    ),
                    &node.loc,
                );
            } else if (q as usize) > node.observations.len() {
                self.emit(
                    format!(
                        "Ensemble '{}' quorum {q} exceeds available observations ({})",
                        node.name,
                        node.observations.len()
                    ),
                    &node.loc,
                );
            }
        }
    }

    // ── §λ-L-E Fase 4 — Topology + π-calculus binary sessions ──────

    /// §λ-L-E Fase 4 — Session validation.
    ///
    /// Enforces: (a) exactly 2 roles; (b) role names are distinct; (c) every
    /// step has a valid op and — for send/receive — a non-empty message type;
    /// (d) Honda-Vasconcelos duality between the two roles.
    fn check_session(&mut self, node: &SessionDefinition) {
        if node.roles.len() != 2 {
            self.emit(
                format!(
                    "Session '{}' must declare exactly 2 roles (binary session); got {}",
                    node.name,
                    node.roles.len()
                ),
                &node.loc,
            );
        } else if node.roles[0].name == node.roles[1].name {
            self.emit(
                format!(
                    "Session '{}' has duplicate role name '{}'",
                    node.name, node.roles[0].name
                ),
                &node.loc,
            );
        }
        for role in &node.roles {
            self.check_session_role(&node.name, role);
        }
        if node.roles.len() == 2 {
            self.check_session_duality(node);
        }
    }

    fn check_session_role(&mut self, session_name: &str, role: &SessionRole) {
        self.check_session_steps(session_name, &role.name, &role.steps);
    }

    /// §Fase 41.b — validate a step sequence, recursing into `select`/`branch`
    /// arms: `send`/`receive` need a message type; a choice needs ≥ 1 branch
    /// with unique labels; each branch's sub-protocol is validated recursively.
    fn check_session_steps(&mut self, session_name: &str, role_name: &str, steps: &[SessionStep]) {
        for (idx, step) in steps.iter().enumerate() {
            match step.op.as_str() {
                "send" | "receive" => {
                    if step.message_type.is_empty() {
                        self.emit(
                            format!(
                                "Session '{session_name}' role '{role_name}' step #{idx} '{}' \
                                 requires a message type",
                                step.op
                            ),
                            &step.loc,
                        );
                    }
                }
                "loop" | "end" => {}
                "select" | "branch" => {
                    if step.branches.is_empty() {
                        self.emit(
                            format!(
                                "Session '{session_name}' role '{role_name}' step #{idx} '{}' must \
                                 have at least one branch",
                                step.op
                            ),
                            &step.loc,
                        );
                    }
                    let mut seen: std::collections::HashSet<&str> = std::collections::HashSet::new();
                    for b in &step.branches {
                        if !seen.insert(b.label.as_str()) {
                            self.emit(
                                format!(
                                    "Session '{session_name}' role '{role_name}' choice has \
                                     duplicate branch label '{}'",
                                    b.label
                                ),
                                &b.loc,
                            );
                        }
                        self.check_session_steps(session_name, role_name, &b.steps);
                    }
                }
                other => {
                    self.emit(
                        format!("Session '{session_name}' role '{role_name}' step #{idx} has invalid op '{other}'"),
                        &step.loc,
                    );
                }
            }
        }
    }

    /// §Fase 41.b — duality is now decided by the **session-type algebra**
    /// (`crate::session`): each role is lowered to a [`SessionType`] (with
    /// `loop` becoming an equirecursive `μ`), and the two are checked under the
    /// **connection law** `T₂ ≡ T₁⊥` via regular-coinductive duality. This
    /// supersedes the old positional, equal-length, step-by-step check — which
    /// could not reason about `loop` as a recursion point — and grounds the
    /// language's binary-session duality in linear logic (Caires–Pfenning).
    fn check_session_duality(&mut self, node: &SessionDefinition) {
        let t1 = lower_session_role(&node.roles[0]);
        let t2 = lower_session_role(&node.roles[1]);
        if !t1.is_dual_to(&t2) {
            self.emit(
                format!(
                    "Session '{}' duality violation: role '{}' has the session type `{}`, \
                     whose dual is `{}`, but role '{}' has `{}` (expected the dual)",
                    node.name,
                    node.roles[0].name,
                    t1,
                    t1.dual(),
                    node.roles[1].name,
                    t2,
                ),
                &node.loc,
            );
        }
    }

    /// §Fase 41.b/c — `socket` validation (the typed-WS transport binding).
    /// Enforces, in order:
    ///   (a) `protocol` references a **declared `session`** (whose two roles
    ///       are duality-checked via the §41.a algebra, so the dialogue
    ///       carried over the connection is conformant by construction);
    ///   (b) the backpressure credit window, if given, is **positive** — a
    ///       0-credit window cannot type a send (§4.2: no rule at n=0);
    ///   (c) §Fase 41.c — the **Presburger discharge**: lower each role into
    ///       the §41.a algebra, stamp with the socket's `credit(k)`, and run
    ///       [`SessionType::credit_analyse`] — surfaces send-at-zero, burst
    ///       overflow (the protocol demands a send-burst > k), and loop
    ///       unsustainability (`Δ = #send − #recv > 0` per recurring path).
    fn check_socket(&mut self, node: &SocketDefinition) {
        // (a) protocol shape.
        let session = if node.protocol.is_empty() {
            self.emit(
                format!("Socket '{}' has no `protocol:` — it must reference a declared session", node.name),
                &node.loc,
            );
            None
        } else {
            match find_session_by_name(self.program, &node.protocol) {
                Some(s) => Some(s),
                None => {
                    self.emit(
                        format!(
                            "Socket '{}' protocol '{}' is not a declared session (the protocol must be a `session`)",
                            node.name, node.protocol
                        ),
                        &node.loc,
                    );
                    None
                }
            }
        };
        // (b) credit window must be positive — the static face of the n=0 axiom.
        let budget: Option<u64> = match node.backpressure_credit {
            Some(n) if n >= 1 => Some(n as u64),
            Some(n) => {
                self.emit(
                    format!(
                        "Socket '{}' backpressure credit must be ≥ 1 (got {n}); a 0-credit window \
                         cannot type a send (§Fase 41 §4.2)",
                        node.name
                    ),
                    &node.loc,
                );
                None
            }
            None => None, // unbounded fragment — no credit constraints to discharge
        };
        // (c) Presburger discharge — only runs when (a) + (b) succeeded.
        if let (Some(session), Some(budget)) = (session, budget) {
            for role in &session.roles {
                let lowered = lower_session_role(role).with_credit(budget);
                if let Err(e) = lowered.credit_analyse(budget) {
                    self.emit(
                        format!(
                            "Socket '{}' violates the credit-refined backpressure type of \
                             session '{}' role '{}': {} (D2)",
                            node.name, node.protocol, role.name, e
                        ),
                        &node.loc,
                    );
                }
            }
        }
    }

    /// §λ-L-E Fase 4 — Topology validation.
    ///
    /// Enforces: (a) each node name is unique + resolves to a valid kind;
    /// (b) each edge's source/target appear in `nodes`; (c) no self-loops;
    /// (d) each `session_ref` is a declared session;
    /// (e) Honda liveness — no cycle where every edge is receive-first.
    fn check_topology(&mut self, node: &TopologyDefinition) {
        const NODE_KINDS: &[&str] = &[
            "resource",
            "fabric",
            "manifest",
            "observe",
            "axonendpoint",
            "axonstore",
            "daemon",
            "agent",
            "shield",
        ];
        let mut seen_nodes: std::collections::HashSet<&String> = std::collections::HashSet::new();
        for n in &node.nodes {
            if !seen_nodes.insert(n) {
                self.emit(
                    format!("Topology '{}' lists node '{}' more than once", node.name, n),
                    &node.loc,
                );
                continue;
            }
            match self.symbols.lookup(n) {
                None => self.emit(
                    format!("Topology '{}' references undefined node '{}'", node.name, n),
                    &node.loc,
                ),
                Some(sym) if !NODE_KINDS.contains(&sym.kind.as_str()) => self.emit(
                    format!(
                        "Topology '{}' node '{}' is a {} — not a valid topology entity. \
                         Valid kinds: {}",
                        node.name,
                        n,
                        sym.kind,
                        NODE_KINDS.join(", ")
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        for edge in &node.edges {
            self.check_topology_edge(&node.name, edge, &seen_nodes);
        }
        self.check_topology_liveness(node);
    }

    fn check_topology_edge(
        &mut self,
        topology_name: &str,
        edge: &TopologyEdge,
        declared_nodes: &std::collections::HashSet<&String>,
    ) {
        if !declared_nodes.contains(&edge.source) {
            self.emit(
                format!(
                    "Topology '{topology_name}' edge source '{}' is not in the nodes list",
                    edge.source
                ),
                &edge.loc,
            );
        }
        if !declared_nodes.contains(&edge.target) {
            self.emit(
                format!(
                    "Topology '{topology_name}' edge target '{}' is not in the nodes list",
                    edge.target
                ),
                &edge.loc,
            );
        }
        if edge.source == edge.target {
            self.emit(
                format!(
                    "Topology '{topology_name}' has self-loop edge on '{}' — \
                     π-calculus binary sessions require two distinct endpoints",
                    edge.source
                ),
                &edge.loc,
            );
        }
        if edge.session_ref.is_empty() {
            self.emit(
                format!(
                    "Topology '{topology_name}' edge {}->{} has no session reference",
                    edge.source, edge.target
                ),
                &edge.loc,
            );
            return;
        }
        match self.symbols.lookup(&edge.session_ref) {
            None => self.emit(
                format!(
                    "Topology '{topology_name}' edge {}->{} references undefined session '{}'",
                    edge.source, edge.target, edge.session_ref
                ),
                &edge.loc,
            ),
            Some(sym) if sym.kind != "session" => self.emit(
                format!(
                    "Topology '{topology_name}' edge {}->{} session ref '{}' is a {}, not a session",
                    edge.source, edge.target, edge.session_ref, sym.kind
                ),
                &edge.loc,
            ),
            _ => {}
        }
    }

    /// Honda-liveness: detect cycles whose every edge starts with `receive`
    /// on the source role. Such a cycle has no progress — static deadlock.
    fn check_topology_liveness(&mut self, node: &TopologyDefinition) {
        let mut adjacency: std::collections::HashMap<String, Vec<String>> =
            std::collections::HashMap::new();
        for edge in &node.edges {
            if !edge.source.is_empty() && !edge.target.is_empty() {
                adjacency
                    .entry(edge.source.clone())
                    .or_default()
                    .push(edge.target.clone());
            }
        }
        let cycles = find_cycles(&adjacency);
        if cycles.is_empty() {
            return;
        }
        for cycle in cycles {
            let cycle_edges = cycle_to_edges(&cycle, &node.edges);
            // Only flag if (a) we found every edge in the cycle (sanity) and
            // (b) every one of them is receive-first on the source side.
            if cycle_edges.len() == cycle.len()
                && cycle_edges.iter().all(|e| self.edge_is_receive_first(e))
            {
                let mut tour: Vec<String> = cycle.clone();
                if let Some(first) = cycle.first() {
                    tour.push(first.clone());
                }
                self.emit(
                    format!(
                        "Topology '{}' has a static deadlock: cycle [{}] where every \
                         edge waits on receive — no progress is possible (Honda liveness violation)",
                        node.name, tour.join(" -> ")
                    ),
                    &node.loc,
                );
            }
        }
    }

    /// Look up the session AST for an edge and check whether the FIRST
    /// role's first step is `receive`. Source plays the first role (fixed
    /// convention per AST docstring).
    fn edge_is_receive_first(&self, edge: &TopologyEdge) -> bool {
        let session = match find_session_by_name(self.program, &edge.session_ref) {
            Some(s) => s,
            None => return false,
        };
        let first_role = match session.roles.first() {
            Some(r) => r,
            None => return false,
        };
        first_role
            .steps
            .first()
            .map(|s| s.op == "receive")
            .unwrap_or(false)
    }

    // ── §λ-L-E Fase 5 — Cognitive immune system (paper_immune_v2.md) ───

    /// §λ-L-E Fase 5 — Immune validation.
    ///
    /// Enforces paper §8.2 mandatory scope + watch non-empty + sensitivity
    /// ∈ [0.0, 1.0] + window ≥ 1 + decay enum.
    fn check_immune(&mut self, node: &ImmuneDefinition) {
        if node.scope.is_empty() {
            self.emit(
                format!(
                    "immune '{}' requires an explicit 'scope' (tenant | flow | global). \
                     No implicit default exists — blast radius must be declared (paper §8.2)",
                    node.name
                ),
                &node.loc,
            );
        } else if !matches!(node.scope.as_str(), "tenant" | "flow" | "global") {
            self.emit(
                format!(
                    "immune '{}' has invalid scope '{}'. Valid: tenant | flow | global",
                    node.name, node.scope
                ),
                &node.loc,
            );
        }
        if node.watch.is_empty() {
            self.emit(
                format!(
                    "immune '{}' requires a non-empty 'watch' list (observables to monitor)",
                    node.name
                ),
                &node.loc,
            );
        }
        if let Some(s) = node.sensitivity {
            if !(0.0..=1.0).contains(&s) {
                self.emit(
                    format!(
                        "immune '{}' sensitivity must be in [0.0, 1.0], got {s}",
                        node.name
                    ),
                    &node.loc,
                );
            }
        }
        if node.window < 1 {
            self.emit(
                format!(
                    "immune '{}' window must be >= 1, got {}",
                    node.name, node.window
                ),
                &node.loc,
            );
        }
        if !matches!(node.decay.as_str(), "exponential" | "linear" | "none") {
            self.emit(
                format!(
                    "immune '{}' has invalid decay '{}'. Valid: exponential | linear | none",
                    node.name, node.decay
                ),
                &node.loc,
            );
        }
    }

    /// §λ-L-E Fase 5 — Reflex validation.
    ///
    /// Enforces mandatory scope + valid scope/on_level/action enums + trigger
    /// resolves to an `immune` (one-way dependency per paper §4).
    fn check_reflex(&mut self, node: &ReflexDefinition) {
        if node.scope.is_empty() {
            self.emit(
                format!(
                    "reflex '{}' requires an explicit 'scope' (tenant | flow | global) — paper §8.2",
                    node.name
                ),
                &node.loc,
            );
        } else if !matches!(node.scope.as_str(), "tenant" | "flow" | "global") {
            self.emit(
                format!("reflex '{}' has invalid scope '{}'", node.name, node.scope),
                &node.loc,
            );
        }
        if node.trigger.is_empty() {
            self.emit(
                format!("reflex '{}' requires a 'trigger: <ImmuneName>'", node.name),
                &node.loc,
            );
        } else {
            match self.symbols.lookup(&node.trigger) {
                None => self.emit(
                    format!(
                        "reflex '{}' references undefined trigger '{}' (expected an immune)",
                        node.name, node.trigger
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "immune" => self.emit(
                    format!(
                        "reflex '{}' trigger '{}' is a {}, not an immune",
                        node.name, node.trigger, sym.kind
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        if !matches!(
            node.on_level.as_str(),
            "know" | "believe" | "speculate" | "doubt"
        ) {
            self.emit(
                format!(
                    "reflex '{}' invalid on_level '{}'. Valid: know | believe | speculate | doubt",
                    node.name, node.on_level
                ),
                &node.loc,
            );
        }
        if node.action.is_empty() {
            self.emit(
                format!(
                    "reflex '{}' requires an 'action' (drop | revoke | emit | redact | \
                     quarantine | terminate | alert)",
                    node.name
                ),
                &node.loc,
            );
        } else if !matches!(
            node.action.as_str(),
            "drop" | "revoke" | "emit" | "redact" | "quarantine" | "terminate" | "alert"
        ) {
            self.emit(
                format!("reflex '{}' invalid action '{}'", node.name, node.action),
                &node.loc,
            );
        }
    }

    /// §λ-L-E Fase 5 — Heal validation.
    ///
    /// Enforces mandatory scope + source is an immune + on_level/mode enums +
    /// **paper §7.3: mode='adversarial' requires a shield gate** + shield_ref
    /// (if present) resolves to a shield + max_patches ≥ 1.
    fn check_heal(&mut self, node: &HealDefinition) {
        if node.scope.is_empty() {
            self.emit(
                format!(
                    "heal '{}' requires an explicit 'scope' (tenant | flow | global) — paper §8.2",
                    node.name
                ),
                &node.loc,
            );
        } else if !matches!(node.scope.as_str(), "tenant" | "flow" | "global") {
            self.emit(
                format!("heal '{}' has invalid scope '{}'", node.name, node.scope),
                &node.loc,
            );
        }
        if node.source.is_empty() {
            self.emit(
                format!("heal '{}' requires a 'source: <ImmuneName>'", node.name),
                &node.loc,
            );
        } else {
            match self.symbols.lookup(&node.source) {
                None => self.emit(
                    format!(
                        "heal '{}' references undefined source '{}' (expected an immune)",
                        node.name, node.source
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "immune" => self.emit(
                    format!(
                        "heal '{}' source '{}' is a {}, not an immune",
                        node.name, node.source, sym.kind
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        if !matches!(
            node.on_level.as_str(),
            "know" | "believe" | "speculate" | "doubt"
        ) {
            self.emit(
                format!("heal '{}' invalid on_level '{}'", node.name, node.on_level),
                &node.loc,
            );
        }
        if !matches!(
            node.mode.as_str(),
            "audit_only" | "human_in_loop" | "adversarial"
        ) {
            self.emit(
                format!(
                    "heal '{}' invalid mode '{}'. Valid: audit_only | human_in_loop | \
                     adversarial (paper §7)",
                    node.name, node.mode
                ),
                &node.loc,
            );
        }
        // Paper §7.3 — adversarial mode requires an explicit shield gate.
        if node.mode == "adversarial" && node.shield_ref.is_empty() {
            self.emit(
                format!(
                    "heal '{}' mode='adversarial' requires a 'shield' gate \
                     (no LLM-generated patch ships without review). \
                     Paper §7.3: adversarial mode needs explicit Risk Acceptance",
                    node.name
                ),
                &node.loc,
            );
        }
        if !node.shield_ref.is_empty() {
            match self.symbols.lookup(&node.shield_ref) {
                None => self.emit(
                    format!(
                        "heal '{}' references undefined shield '{}'",
                        node.name, node.shield_ref
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "shield" => self.emit(
                    format!(
                        "heal '{}' shield ref '{}' is a {}, not a shield",
                        node.name, node.shield_ref, sym.kind
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        if node.max_patches < 1 {
            self.emit(
                format!(
                    "heal '{}' max_patches must be >= 1, got {}",
                    node.name, node.max_patches
                ),
                &node.loc,
            );
        }
    }

    // ── §λ-L-E Fase 9 — UI cognitiva (component / view) ────────────
    //
    // Compile-time invariants enforced below:
    //   1. `renders` references a declared `type`.
    //   2. `on_interact` (if present) is a declared `flow` whose first
    //      parameter type matches `renders`.
    //   3. If `renders` carries κ (regulatory class), `via_shield` is
    //      MANDATORY and its `compliance` must cover every κ of the
    //      rendered type. Fase 9.5 compile-time contract.
    //   4. `via_shield` (if present) must name a declared `shield`.
    //   5. Every component listed in a `view.components` must resolve
    //      to a declared `component`.

    fn check_component(&mut self, node: &ComponentDefinition) {
        // (1) renders must resolve to a type
        let rendered_type = if node.renders.is_empty() {
            self.emit(
                format!("component '{}' requires 'renders: <TypeName>'", node.name),
                &node.loc,
            );
            None
        } else {
            match self.symbols.lookup(&node.renders) {
                None => {
                    self.emit(
                        format!(
                            "component '{}' references undefined type '{}'",
                            node.name, node.renders
                        ),
                        &node.loc,
                    );
                    None
                }
                Some(sym) if sym.kind != "type" => {
                    self.emit(
                        format!(
                            "component '{}' renders '{}' which is a {}, not a type",
                            node.name, node.renders, sym.kind
                        ),
                        &node.loc,
                    );
                    None
                }
                Some(_) => find_type_by_name(self.program, &node.renders),
            }
        };

        // (4) shield ref
        let shield_node = if node.via_shield.is_empty() {
            None
        } else {
            match self.symbols.lookup(&node.via_shield) {
                None => {
                    self.emit(
                        format!(
                            "component '{}' references undefined shield '{}'",
                            node.name, node.via_shield
                        ),
                        &node.loc,
                    );
                    None
                }
                Some(sym) if sym.kind != "shield" => {
                    self.emit(
                        format!(
                            "component '{}' via_shield '{}' is a {}, not a shield",
                            node.name, node.via_shield, sym.kind
                        ),
                        &node.loc,
                    );
                    None
                }
                Some(_) => find_shield_by_name(self.program, &node.via_shield),
            }
        };

        // (3) regulated-render rule — Fase 9.5
        if let Some(t) = rendered_type {
            let type_kappa: std::collections::HashSet<&str> =
                t.compliance.iter().map(|s| s.as_str()).collect();
            if !type_kappa.is_empty() {
                match shield_node {
                    None => self.emit(
                        format!(
                            "component '{}' renders regulated type '{}' \
                             (kappa = {{{}}}) but declares no 'via_shield'. \
                             Regulated renders require a shield that covers \
                             the type's kappa — Fase 9.5.",
                            node.name,
                            node.renders,
                            {
                                let mut v: Vec<&str> = type_kappa.iter().copied().collect();
                                v.sort();
                                v.join(", ")
                            }
                        ),
                        &node.loc,
                    ),
                    Some(s) => {
                        let shield_kappa: std::collections::HashSet<&str> =
                            s.compliance.iter().map(|s| s.as_str()).collect();
                        let mut missing: Vec<&str> =
                            type_kappa.difference(&shield_kappa).copied().collect();
                        missing.sort();
                        if !missing.is_empty() {
                            self.emit(
                                format!(
                                    "component '{}' via_shield '{}' does not cover \
                                     kappa = {{{}}} of type '{}'. Add these classes \
                                     to the shield's 'compliance' list or pick a \
                                     shield that already covers them.",
                                    node.name,
                                    node.via_shield,
                                    missing.join(", "),
                                    node.renders,
                                ),
                                &node.loc,
                            );
                        }
                    }
                }
            }
        }

        // (2) on_interact must resolve to a flow with compatible signature
        if !node.on_interact.is_empty() {
            match self.symbols.lookup(&node.on_interact) {
                None => self.emit(
                    format!(
                        "component '{}' references undefined flow '{}'",
                        node.name, node.on_interact
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "flow" => self.emit(
                    format!(
                        "component '{}' on_interact '{}' is a {}, not a flow",
                        node.name, node.on_interact, sym.kind
                    ),
                    &node.loc,
                ),
                Some(_) => {
                    if let Some(flow) = find_flow_by_name(self.program, &node.on_interact) {
                        if !rendered_type.is_none() {
                            if let Some(first_param) = flow.parameters.first() {
                                let pt = first_param.type_expr.name.as_str();
                                if !pt.is_empty() && pt != node.renders {
                                    self.emit(
                                        format!(
                                            "component '{}' on_interact flow '{}' \
                                             expects first parameter of type '{}', \
                                             but component renders '{}'. Signatures \
                                             must match — Fase 9.2 rule 2.",
                                            node.name, node.on_interact, pt, node.renders
                                        ),
                                        &node.loc,
                                    );
                                }
                            }
                        }
                    }
                }
            }
        }
    }

    fn check_view(&mut self, node: &ViewDefinition) {
        if node.components.is_empty() {
            self.emit(
                format!(
                    "view '{}' has empty components list — a view must \
                     compose at least one component",
                    node.name
                ),
                &node.loc,
            );
            return;
        }
        let mut seen: std::collections::HashSet<&String> = std::collections::HashSet::new();
        for comp_name in &node.components {
            if !seen.insert(comp_name) {
                self.emit(
                    format!(
                        "view '{}' lists component '{}' more than once",
                        node.name, comp_name
                    ),
                    &node.loc,
                );
                continue;
            }
            match self.symbols.lookup(comp_name) {
                None => self.emit(
                    format!(
                        "view '{}' references undefined component '{}'",
                        node.name, comp_name
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "component" => self.emit(
                    format!(
                        "view '{}' component ref '{}' is a {}, not a component",
                        node.name, comp_name, sym.kind
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
    }

    fn check_axonendpoint(&mut self, node: &AxonEndpointDefinition) {
        // HTTP method enum
        if !node.method.is_empty() {
            let upper = node.method.to_uppercase();
            if !is_valid(&upper, VALID_ENDPOINT_METHODS) {
                self.emit(
                    format!(
                        "Unknown HTTP method '{}' in axonendpoint '{}'. Valid: {}",
                        node.method,
                        node.name,
                        valid_list(VALID_ENDPOINT_METHODS)
                    ),
                    &node.loc,
                );
            }
        }

        // §Fase 36.d (D2) — declared execution backend, closed catalog.
        // The parser already rejects an unknown backend with a smart-
        // suggest hint; this re-check defends ASTs built outside the
        // parser (LSP synthesis, programmatic construction) so an
        // impossible backend is a compile error on every path.
        if !node.backend.is_empty()
            && !is_valid(&node.backend, crate::parser::AXONENDPOINT_BACKEND_VALUES)
        {
            self.emit(
                format!(
                    "Unknown backend '{}' in axonendpoint '{}'. Valid: {}",
                    node.backend,
                    node.name,
                    valid_list(crate::parser::AXONENDPOINT_BACKEND_VALUES)
                ),
                &node.loc,
            );
        }

        // §Fase 36.k (D10) — `axon-W003`: an axonendpoint that declares
        // no `backend:` relies on the Fase 36 ladder for resolution.
        // An explicit `backend: auto` is the adopter's deliberate
        // opt-in to ladder resolution — it carries no warning. An
        // omitted field does: the adopter learns at compile time, not
        // at the first production 503.
        if node.backend.is_empty() {
            self.warn(build_w003_message(&node.name), &node.loc);
        }

        // Path must start with /
        if !node.path.is_empty() && !node.path.starts_with('/') {
            self.emit(
                format!(
                    "Path must start with '/' in axonendpoint '{}', got '{}'",
                    node.name, node.path
                ),
                &node.loc,
            );
        }

        // execute_flow reference
        if !node.execute_flow.is_empty() {
            match self.symbols.lookup(&node.execute_flow) {
                None => self.emit(
                    format!(
                        "Undefined flow '{}' in axonendpoint '{}'",
                        node.execute_flow, node.name
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "flow" => self.emit(
                    format!(
                        "'{}' is a {}, not a flow (referenced in axonendpoint '{}')",
                        node.execute_flow, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }

        // Shield reference
        if !node.shield_ref.is_empty() {
            match self.symbols.lookup(&node.shield_ref) {
                None => self.emit(
                    format!(
                        "Undefined shield '{}' in axonendpoint '{}'",
                        node.shield_ref, node.name
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "shield" => self.emit(
                    format!(
                        "'{}' is a {}, not a shield (referenced in axonendpoint '{}')",
                        node.shield_ref, sym.kind, node.name
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }

        // Retries >= 0
        if let Some(v) = node.retries {
            if v < 0 {
                self.emit(
                    format!(
                        "retries must be >= 0, got {} in axonendpoint '{}'",
                        v, node.name
                    ),
                    &node.loc,
                );
            }
        }

        // §Fase 35.j (D11) — Pillar IV: capability-typed store access.
        // The endpoint must GRANT (in `requires:`) every capability a
        // capability-gated store accessed by its flow declares — data
        // isolation as a language guarantee, enforced statically.
        // Nested store ops (inside `for`/`par` bodies) are caught by
        // the runtime re-check (35.j `store::capability`), not this
        // top-level walk.
        if !node.execute_flow.is_empty() {
            if let Some(flow) = self.find_flow(&node.execute_flow) {
                for step in &flow.body {
                    let store_name = match step {
                        FlowStep::Persist(s) => &s.store_name,
                        FlowStep::Retrieve(s) => &s.store_name,
                        FlowStep::Mutate(s) => &s.store_name,
                        FlowStep::Purge(s) => &s.store_name,
                        _ => continue,
                    };
                    let Some(store) = self.find_store(store_name) else {
                        continue;
                    };
                    if store.capability.is_empty()
                        || node.requires_capabilities.contains(&store.capability)
                    {
                        continue;
                    }
                    self.emit(
                        format!(
                            "axonendpoint '{}' executes flow '{}' which accesses \
                             axonstore '{}' requiring capability '{}', but '{}' \
                             does not grant it — add '{}' to the endpoint's \
                             `requires:` list (Fase 35.j Pillar IV).",
                            node.name,
                            node.execute_flow,
                            store_name,
                            store.capability,
                            node.name,
                            store.capability,
                        ),
                        &node.loc,
                    );
                }
            }
        }

        // §Fase 39.e (D12 α RATIFIED) — Wire-shape mandate gate
        // (`axon-E039`). On `transport: json` endpoints, every
        // declared `output: T` MUST be `FlowEnvelope<T>` (or `Any` /
        // `Unit` / `<empty>`). Bare `output: T` / `output: List<T>` /
        // `output: Stream<T>` declarations are now COMPILE ERRORS —
        // the v1.x bridge is closed, the v2.0.0 wire contract is
        // structural.
        //
        // This gate runs BEFORE the 38.x.f cardinality gate. When
        // E039 fires, the cardinality gate is SUPPRESSED so the
        // adopter sees ONE canonical diagnostic with the right
        // answer (FlowEnvelope<tail_T> based on the actual flow
        // cardinality + sse migration alternative). When E039 does
        // NOT fire (declaration IS FlowEnvelope<T> or sse transport
        // or no output declared), the cardinality gate runs
        // normally and unwraps the FlowEnvelope per 39.a.
        let e039_fired = if !node.execute_flow.is_empty()
            && !node.output_type.is_empty()
        {
            self.emit_e039_wire_packaging_gate(node)
        } else {
            false
        };

        // §Fase 38.x.f (D1–D6) — Cardinality Coverage gate.
        //
        // Runs BEFORE the 37.c totality block because the latter does
        // an early `return` when no binding sources are declared
        // (endpoint with `output:` + `execute:` only, no `body:` /
        // `path` / `query`). The cardinality gate is independent of
        // binding-source declarations — it only needs the endpoint's
        // `output:` + the flow's body tail — so it must run first or
        // it never fires on the no-source case (e.g. the Stream
        // mismatch §6 in the anchor test).
        //
        // §39.e — When E039 fires above, we SKIP the cardinality
        // gate (the E039 diagnostic already names the canonical
        // FlowEnvelope<...> answer; double-emitting T9XX would be
        // noisy).
        if !e039_fired
            && !node.execute_flow.is_empty()
            && !node.output_type.is_empty()
        {
            if let Some(flow) = self.find_flow(&node.execute_flow) {
                let declared = declared_cardinality(&node.output_type);
                let tail = infer_flow_tail_cardinality(flow);
                self.emit_cardinality_gate(node, &declared, &tail);
            }
        }

        // §Fase 37.c (D2) — The Request Binding Contract totality check.
        //
        // When the endpoint declares `body: T`, the type-checker
        // proves every REQUIRED parameter of `execute: F` is covered
        // by a field of T — by name, type-compatible. An uncovered
        // required parameter is a compile error: otherwise the flow
        // reaches production and fails at REQUEST time for a missing
        // argument (the exact v1.35.0 defect Fase 37 closes). The
        // failure moves from production to `axon check`. Sibling of
        // the Fase 35.j Pillar IV endpoint→flow→store-capability check.
        //
        // The check runs only when `body: T` resolves to a declared
        // struct type. A primitive `body:` (or a `body:` naming an
        // undeclared type) has no fields to cover parameters — the
        // runtime binding is then untyped/best-effort and outside the
        // D2 theorem (honest scope). An OPTIONAL parameter need not be
        // covered. Type-compatibility is exact: same type name + same
        // generic parameter.
        //
        // §Fase 37.y (D3) — D2 totality UNION over three binding sources:
        // path_params (typed `Text` by HTTP convention), query_params
        // (declared type from the closed catalog), body type fields
        // (existing v1.36.0 surface). Each required flow param must be
        // covered by EXACTLY ONE source — zero coverage emits the
        // legacy missing-binding error (extended to mention all three
        // sources); multi-source coverage emits the new `axon-T901`
        // collision error (D4).
        //
        // The gate now runs when `execute_flow` is set AND at least
        // one binding source is declared. An endpoint with NO sources
        // and NO required flow params is a no-op for the contract
        // (matches v1.36.0 honest-scope behavior).
        if !node.execute_flow.is_empty() {
            let has_any_source = !node.body_type.is_empty()
                || !node.path_params.is_empty()
                || !node.query_params.is_empty();
            if !has_any_source {
                // No declared binding sources — honest scope. The
                // runtime binder will deliver an empty map; the flow
                // must accept that (any required param would fail at
                // request time, which is the v1.36.0 behavior).
                return;
            }
            let body_opt = if node.body_type.is_empty() {
                None
            } else {
                find_type_by_name(self.program, &node.body_type)
            };
            if let Some(flow) = self.find_flow(&node.execute_flow) {
                for param in &flow.parameters {
                    if param.type_expr.optional {
                        continue; // an optional parameter need not bind.
                    }
                    // — Resolve binding sources for this param name. —
                    let path_hit =
                        node.path_params.iter().any(|p| p == &param.name);
                    let query_hit = node
                        .query_params
                        .iter()
                        .find(|f| f.name == param.name);
                    let body_hit = body_opt
                        .and_then(|b| b.fields.iter().find(|f| f.name == param.name));
                    let source_count = (path_hit as usize)
                        + (query_hit.is_some() as usize)
                        + (body_hit.is_some() as usize);

                    if source_count == 0 {
                        // ── D3 (extended) — no coverage. The hint
                        // now names ALL THREE candidate sources so the
                        // adopter knows where to add the field.
                        let body_clause = if node.body_type.is_empty() {
                            "(declare a body type via `body: T` or)".to_string()
                        } else {
                            format!(
                                "add a field '{}: {}' to '{}', or",
                                param.name,
                                fmt_type_expr(&param.type_expr),
                                node.body_type,
                            )
                        };
                        self.emit(
                            format!(
                                "axonendpoint '{}' executes flow '{}' whose \
                                 required parameter '{}: {}' has no matching \
                                 binding source. The Request Binding Contract \
                                 (Fase 37 + 37.y D3) binds a flow parameter \
                                 from a same-named path placeholder \
                                 (`{{{}}}` in the `path:` string), query \
                                 param (`query: {{ {}: {} }}`), or body \
                                 field. Either {} add a `{{{}}}` placeholder \
                                 to the path, or declare `{}: {}` in the \
                                 `query: {{ … }}` block — or make the \
                                 parameter optional (Fase 37.y D3).",
                                node.name,
                                node.execute_flow,
                                param.name,
                                fmt_type_expr(&param.type_expr),
                                param.name,
                                param.name,
                                fmt_type_expr(&param.type_expr),
                                body_clause,
                                param.name,
                                param.name,
                                fmt_type_expr(&param.type_expr),
                            ),
                            &node.loc,
                        );
                        continue;
                    }

                    if source_count > 1 {
                        // ── D4 — collision. The new `axon-T901`
                        // error: an adopter who declares the same
                        // name in two+ sources MUST disambiguate
                        // before the build can pass. The runtime
                        // merge order would otherwise mask which
                        // source the value came from.
                        let mut sources: Vec<&str> = Vec::new();
                        if path_hit {
                            sources.push("path");
                        }
                        if query_hit.is_some() {
                            sources.push("query");
                        }
                        if body_hit.is_some() {
                            sources.push("body");
                        }
                        let where_phrase = if sources.len() == 2 {
                            format!("{} and {}", sources[0], sources[1])
                        } else {
                            format!(
                                "{}, {}, and {}",
                                sources[0], sources[1], sources[2]
                            )
                        };
                        self.emit(
                            format!(
                                "axon-T901 axonendpoint '{}' parameter '{}' \
                                 is declared in MORE than one binding source \
                                 ({where_phrase}). The Request Binding Contract \
                                 forbids a name in multiple sources to keep \
                                 the runtime binding unambiguous. Remove the \
                                 declaration from {} of the sources so '{}' \
                                 resolves uniquely. (Fase 37.y D4)",
                                node.name,
                                param.name,
                                sources.len() - 1,
                                param.name,
                            ),
                            &node.loc,
                        );
                        continue;
                    }

                    // ── source_count == 1: type-compatibility check. —
                    if path_hit {
                        // Path params bind as `Text` (HTTP convention).
                        // The flow param must be `Text` (with no generic).
                        if param.type_expr.name != "Text"
                            || !param.type_expr.generic_param.is_empty()
                        {
                            self.emit(
                                format!(
                                    "axonendpoint '{}' parameter '{}' is bound \
                                     from path placeholder `{{{}}}` (HTTP path \
                                     segments are `Text` by convention), but \
                                     the flow declares '{}: {}'. Either change \
                                     the flow parameter to `{}: Text` and \
                                     parse/validate inside the flow, or move \
                                     the binding to `query: {{ {}: {} }}` if \
                                     the type matters at the wire (Fase 37.y D3).",
                                    node.name,
                                    param.name,
                                    param.name,
                                    param.name,
                                    fmt_type_expr(&param.type_expr),
                                    param.name,
                                    param.name,
                                    fmt_type_expr(&param.type_expr),
                                ),
                                &node.loc,
                            );
                        }
                    } else if let Some(qf) = query_hit {
                        // Query param: exact-match type check (same as
                        // the body branch — uniform contract).
                        if qf.type_expr.name != param.type_expr.name
                            || qf.type_expr.generic_param
                                != param.type_expr.generic_param
                        {
                            self.emit(
                                format!(
                                    "axonendpoint '{}' executes flow '{}' \
                                     whose parameter '{}' is '{}', but the \
                                     `query: {{ … }}` block declares '{}' as \
                                     '{}' — the types must match for the \
                                     Request Binding Contract to bind it \
                                     (Fase 37.y D3).",
                                    node.name,
                                    node.execute_flow,
                                    param.name,
                                    fmt_type_expr(&param.type_expr),
                                    qf.name,
                                    fmt_type_expr(&qf.type_expr),
                                ),
                                &node.loc,
                            );
                        }
                    } else if let Some(field) = body_hit {
                        // Body field — preserved v1.36.0 logic verbatim.
                        if field.type_expr.name != param.type_expr.name
                            || field.type_expr.generic_param
                                != param.type_expr.generic_param
                        {
                            self.emit(
                                format!(
                                    "axonendpoint '{}' executes flow '{}' whose \
                                     parameter '{}' is '{}', but body type '{}' \
                                     declares field '{}' as '{}' — the types \
                                     must match for the Request Binding \
                                     Contract to bind it (Fase 37 D2).",
                                    node.name,
                                    node.execute_flow,
                                    param.name,
                                    fmt_type_expr(&param.type_expr),
                                    node.body_type,
                                    field.name,
                                    fmt_type_expr(&field.type_expr),
                                ),
                                &node.loc,
                            );
                        }
                    }
                }
            }
        }

        // §Fase 38.x.f cardinality gate runs ABOVE this block (before
        // the 37.c early-return on no-source endpoints). See the
        // comment block at the top of check_axonendpoint for the
        // load-bearing rationale.
    }

    /// §Fase 39.e (D12 α RATIFIED) — Wire-shape mandate gate.
    ///
    /// On `transport: json` endpoints (effective wire = json), every
    /// declared `output: T` MUST be one of:
    ///   - `FlowEnvelope<X>` (the canonical v2.0.0 wire shape)
    ///   - `Any` (universal accept — degraded surface)
    ///   - `Unit` (no body)
    ///   - `<empty>` (no declaration — D9 backwards-compat skip)
    ///
    /// Any other declaration — `T` (singular bare), `List<X>`,
    /// `Stream<X>` — is a COMPILE ERROR `axon-E039`. The error
    /// message includes the canonical FlowEnvelope wrapping suggestion
    /// (computed from the flow tail's actual cardinality) PLUS the
    /// sse transport alternative.
    ///
    /// On `transport: sse` / `transport: ndjson` endpoints, this gate
    /// does NOT fire — the SSE wire has its own event family per
    /// Fase 39 D9 (`axon.token` / `axon.complete` / etc.), so adopters
    /// can declare any cardinality output without the wrapping
    /// mandate.
    ///
    /// Returns `true` when E039 fires (the caller suppresses the
    /// downstream cardinality gate to keep the diagnostic noise low);
    /// `false` when E039 does NOT fire.
    fn emit_e039_wire_packaging_gate(
        &mut self,
        node: &AxonEndpointDefinition,
    ) -> bool {
        // ── §1 — Resolve effective transport ────────────────────────
        // Mirrors the runtime's three-way resolution:
        //   explicit (parser captured `transport:`) →
        //     use `node.transport`
        //   not explicit + `implicit_transport` computed (Fase 31) →
        //     use `node.implicit_transport`
        //   neither → default "json"
        let effective_transport = if node.transport_explicit {
            node.transport.as_str()
        } else if !node.implicit_transport.is_empty() {
            node.implicit_transport.as_str()
        } else {
            "json"
        };
        // Only json wire bears the mandate per D2 + D9. SSE / ndjson
        // have their own event families and are exempt.
        if effective_transport != "json" {
            return false;
        }

        // ── §2 — Classify the declared output ──────────────────────
        let declared = node.output_type.trim();
        // Empty: D9 backwards-compat skip (no validation gate runs
        // on the wire either).
        if declared.is_empty() {
            return false;
        }
        // `Any`: universal accept — documented degraded surface.
        if declared == "Any" {
            return false;
        }
        // `Unit`: no body to validate — explicit "I produce no
        // wire payload" contract.
        if declared == "Unit" {
            return false;
        }
        // `FlowEnvelope<...>`: the canonical wrapping. Compile-clean
        // even if the inner T is itself a generic (List<X>,
        // Stream<X>) — the 39.a Cardinality::Wrapped variant carries
        // the inner cardinality through transparently.
        if declared.starts_with("FlowEnvelope<") && declared.ends_with('>') {
            return false;
        }

        // ── §3 — E039 fires: compute the canonical suggestion ──────
        // The suggestion is the SAME inner T the adopter declared,
        // just wrapped: `output: T` → suggest `FlowEnvelope<T>`. When
        // the flow's actual tail cardinality differs from the
        // declared bare type, we additionally name the tail shape
        // so the adopter sees the right wrapping for the data.
        let tail_form = if let Some(flow) = self.find_flow(&node.execute_flow) {
            let tail = infer_flow_tail_cardinality(flow);
            match tail {
                Cardinality::Singular(t) if !t.is_empty() => t,
                Cardinality::Plural(t) if !t.is_empty() => {
                    format!("List<{t}>")
                }
                Cardinality::StreamCardinality(t) if !t.is_empty() => {
                    format!("Stream<{t}>")
                }
                Cardinality::Wrapped(_) => {
                    // Defensive: tail being Wrapped is degenerate
                    // (flows don't produce FlowEnvelope<T> directly —
                    // the converter wraps them at the wire). Fall
                    // back to the declared shape.
                    declared.to_string()
                }
                _ => declared.to_string(),
            }
        } else {
            declared.to_string()
        };

        let suggested_envelope = format!("FlowEnvelope<{tail_form}>");

        // ── §4 — Emit the canonical diagnostic ─────────────────────
        self.emit(
            format!(
                "axon-E039 axonendpoint '{}' declares `output: {}` with \
                 `transport: json` (effective), but the v2.0.0 wire \
                 contract requires `FlowEnvelope<T>` wrapping for every \
                 JSON-transport response (D12 α). The wire payload IS \
                 the ψ-vector envelope `⟨ontological_type, result, \
                 certainty, provenance_chain, …⟩`; a bare `{}` cannot \
                 satisfy that contract. Flow '{}' produces a `{}` tail. \
                 Either: \
                 (a) wrap the output type — `output: {}` is the \
                     canonical v2.0.0 declaration (the inner T is \
                     validated against the envelope's `result` slot \
                     by the D5 runtime gate); OR \
                 (b) change the transport — `transport: sse(axon)` \
                     surfaces a streaming wire (per-chunk axon.token \
                     events + axon.complete envelope) where bare \
                     `Stream<T>` / `List<T>` declarations are valid. \
                 See https://axon-lang.io/docs/wire-envelope for the \
                 ψ-vector contract. \
                 (Fase 39 D2 + D12 — Pure Silicon Cognition)",
                node.name,
                node.output_type,
                node.output_type,
                node.execute_flow,
                tail_form,
                suggested_envelope,
            ),
            &node.loc,
        );
        true
    }

    /// §Fase 38.x.f (D1–D6) — Emit the cardinality-mismatch diagnostic
    /// for the `(declared, tail)` disjoint pair. Pure: depends only on
    /// the endpoint's `output:` declaration and the flow tail's
    /// inferred cardinality.
    fn emit_cardinality_gate(
        &mut self,
        node: &AxonEndpointDefinition,
        declared: &Cardinality,
        tail: &Cardinality,
    ) {
        // §Fase 39 (D4) — Wrapped(inner) unwraps transparently for the
        // cardinality gate. The wire shape of `FlowEnvelope<T>` is
        // always a singular object, but the COMPILE-TIME cardinality
        // the type-checker reasons about IS T's cardinality. The
        // unwrap is recursive (covers `FlowEnvelope<FlowEnvelope<X>>`
        // degenerate forms too). The full axon-E039 wire-shape
        // mandate enforcement lands in sub-fase 39.e; here in 39.a we
        // only establish that Wrapped participates in the cardinality
        // truth table by unwrapping its inner.
        if let Cardinality::Wrapped(inner) = declared {
            return self.emit_cardinality_gate(node, inner.as_ref(), tail);
        }
        if let Cardinality::Wrapped(inner) = tail {
            return self.emit_cardinality_gate(node, declared, inner.as_ref());
        }
        match (declared, tail) {
            // — Agreed shapes → silent pass.
            (Cardinality::Unit, Cardinality::Unit) => {}
            (Cardinality::Singular(d), Cardinality::Singular(_)) => {
                // Type-level mismatch is the existing Fase 37 D2
                // contract; cardinality agrees.
                let _ = d;
            }
            (Cardinality::Plural(_), Cardinality::Plural(_)) => {}
            (Cardinality::StreamCardinality(_), Cardinality::StreamCardinality(_)) => {}

            // — Unknown / Disagreed-acceptance → silent pass.
            (_, Cardinality::Unknown) => {}
            (Cardinality::Disagreed, _) => {
                // `output: Any` accepts every cardinality (degraded
                // surface; documented adopter choice — Fase 38.x.f D6).
            }
            (Cardinality::Unknown, _) => {}

            // — D3 bilateral: declared Plural vs tail Singular.
            (Cardinality::Plural(decl_t), Cardinality::Singular(_)) => {
                self.emit(
                    format!(
                        "axon-T9XX axonendpoint '{}' declares `output: {}` \
                         (plural — `List<{}>`), but flow '{}' produces a \
                         `{}` (singular) tail. The runtime would either \
                         wrap the singular in an array implicitly OR fail \
                         the D5 output-schema gate (Fase 32.d) depending \
                         on path. To make the contract explicit: \
                         (a) change the endpoint to `output: {}` if it \
                             returns a single resource (REST \
                             `GET /api/{{resource}}/{{id}}`-style); OR \
                         (b) wrap the tail in a list — `return [result]` \
                             or `for x in [result] {{ x }}` at the flow \
                             tail. \
                         (Fase 38.x.f D3 bilateral)",
                        node.name,
                        node.output_type,
                        decl_t,
                        node.execute_flow,
                        decl_t,
                        decl_t,
                    ),
                    &node.loc,
                );
            }

            // — D1 v1.39.0 retained: declared Singular vs tail Plural
            //   (this is the canonical kivi-shape that 38.x.e shipped).
            (Cardinality::Singular(decl_t), Cardinality::Plural(_)) => {
                self.emit(
                    format!(
                        "axon-T9XX axonendpoint '{}' declares `output: {}` \
                         (singular), but flow '{}' produces a `List<{}>` \
                         tail expression — the flow ends with a step or \
                         construct that produces a list (e.g. `retrieve` \
                         step, `for x in xs {{ … }}` loop, or `return \
                         [a, b, c]`). The runtime D5 output-schema gate \
                         (Fase 32.d) would reject the response as a \
                         shape mismatch. \
                         Either: \
                         (a) change the endpoint to `output: List<{}>` if \
                             it is intentionally returning a collection \
                             (REST `GET /api/{{resource}}`-style); OR \
                         (b) collapse the tail to a singular element — \
                             e.g. add `step Project {{ return result[0] }}` \
                             (or any step that emits the singular shape) \
                             BEFORE the implicit tail, OR add an explicit \
                             `return result[0]` at the end of the flow if \
                             the iteration is guaranteed to yield exactly \
                             one element. \
                         (Fase 38.x.f D1 — v1.39.0 narrow case preserved)",
                        node.name,
                        node.output_type,
                        node.execute_flow,
                        decl_t,
                        decl_t,
                    ),
                    &node.loc,
                );
            }

            // — D5 Stream mismatches (any direction crossing Stream
            //   with non-Stream).
            (Cardinality::StreamCardinality(decl_t), Cardinality::Singular(_))
            | (Cardinality::StreamCardinality(decl_t), Cardinality::Plural(_)) => {
                self.emit(
                    format!(
                        "axon-T9YY axonendpoint '{}' declares `output: \
                         Stream<{}>` (temporal — chunks arrive over time \
                         on SSE), but flow '{}' produces a non-stream \
                         tail. These are distinct cardinality primitives: \
                         (a) change the endpoint to `output: {}` (or \
                             `List<{}>`) if you want JSON delivery at \
                             once, OR \
                         (b) change the flow tail to a step with \
                             `output: Stream<{}>` (e.g. `step Generate \
                             {{ ask: \"...\" output: Stream<{}> }}`) if \
                             you want SSE chunked delivery. \
                         (Fase 38.x.f D5 stream_cardinality_mismatch)",
                        node.name,
                        decl_t,
                        node.execute_flow,
                        decl_t,
                        decl_t,
                        decl_t,
                        decl_t,
                    ),
                    &node.loc,
                );
            }
            (Cardinality::Singular(_), Cardinality::StreamCardinality(strm_t))
            | (Cardinality::Plural(_), Cardinality::StreamCardinality(strm_t)) => {
                self.emit(
                    format!(
                        "axon-T9YY axonendpoint '{}' declares `output: {}` \
                         (spatial — materialized at once), but flow '{}' \
                         produces a `Stream<{}>` tail (temporal — chunks \
                         arrive over time). These are distinct \
                         cardinality primitives: \
                         (a) change the endpoint to `output: Stream<{}>` \
                             if you want SSE chunked delivery, OR \
                         (b) change the flow tail to a non-streaming step \
                             returning `{}` if you want JSON delivery. \
                         (Fase 38.x.f D5 stream_cardinality_mismatch)",
                        node.name,
                        node.output_type,
                        node.execute_flow,
                        strm_t,
                        strm_t,
                        node.output_type,
                    ),
                    &node.loc,
                );
            }

            // — D6 W003: tail-Disagreed against non-Any output.
            (_, Cardinality::Disagreed) => {
                self.emit(
                    format!(
                        "axon-W003 axonendpoint '{}' executes flow '{}' \
                         whose tail is an `if`/`else` (or `par`) where \
                         the branches disagree on cardinality — one \
                         branch returns a singular value while another \
                         returns a list (or stream). The endpoint's \
                         `output: {}` cannot satisfy both shapes \
                         simultaneously. Either: \
                         (a) align the branches — return the same \
                             cardinality from both; OR \
                         (b) declare `output: Any` to accept either \
                             shape (degraded type safety; the runtime \
                             D5 gate will not protect this endpoint); \
                             OR \
                         (c) split into two endpoints, one per branch's \
                             shape. \
                         (Fase 38.x.f D6 cardinality_disagreement_in_branches)",
                        node.name,
                        node.execute_flow,
                        node.output_type,
                    ),
                    &node.loc,
                );
            }

            // — Type-mismatch only (cardinality agrees, types differ).
            //   The existing Fase 37 D2 contract handles this.
            (Cardinality::Unit, _) | (_, Cardinality::Unit) => {
                // Unit + anything else is intentionally silent here —
                // the runtime treats Unit-output as "no response body"
                // and the existing output-schema gate doesn't apply.
            }

            // §Fase 39 (D4) — Wrapped arms are statically unreachable
            // because the early-return at the top of this fn unwraps
            // any Wrapped operand before entering the match. The arms
            // here exist solely to satisfy Rust's exhaustiveness
            // checker. If reached, it indicates a bug in the unwrap
            // shortcut.
            (Cardinality::Wrapped(_), _) | (_, Cardinality::Wrapped(_)) => {
                unreachable!(
                    "§Fase 39 D4 invariant — Wrapped is unwrapped by the \
                     early-return shortcut at the top of emit_cardinality_gate; \
                     this match arm should be unreachable."
                );
            }
        }
    }

    /// §Fase 35.j — Resolve a flow declaration by name.
    fn find_flow(&self, name: &str) -> Option<&'a FlowDefinition> {
        self.program.declarations.iter().find_map(|d| match d {
            Declaration::Flow(f) if f.name == name => Some(f),
            _ => None,
        })
    }

    /// §Fase 35.j — Resolve an axonstore declaration by name.
    fn find_store(&self, name: &str) -> Option<&'a AxonStoreDefinition> {
        self.program.declarations.iter().find_map(|d| match d {
            Declaration::AxonStore(s) if s.name == name => Some(s),
            _ => None,
        })
    }

    // ── Flow-level reference checks ─────────────────────────────────

    fn check_flow_steps(&mut self, steps: &[FlowStep], flow_name: &str) {
        for step in steps {
            match step {
                FlowStep::ShieldApply(n) => {
                    if !n.shield_name.is_empty() {
                        match self.symbols.lookup(&n.shield_name) {
                            None => self.emit(
                                format!(
                                    "Undefined shield '{}' in flow '{}'",
                                    n.shield_name, flow_name
                                ),
                                &n.loc,
                            ),
                            Some(sym) if sym.kind != "shield" => self.emit(
                                format!("'{}' is a {}, not a shield", n.shield_name, sym.kind),
                                &n.loc,
                            ),
                            _ => {}
                        }
                    }
                }
                FlowStep::OtsApply(n) => {
                    if !n.ots_name.is_empty() {
                        match self.symbols.lookup(&n.ots_name) {
                            None => self.emit(
                                format!("Undefined OTS '{}' in flow '{}'", n.ots_name, flow_name),
                                &n.loc,
                            ),
                            Some(sym) if sym.kind != "ots" => self.emit(
                                format!("'{}' is a {}, not an OTS", n.ots_name, sym.kind),
                                &n.loc,
                            ),
                            _ => {}
                        }
                    }
                }
                FlowStep::MandateApply(n) => {
                    if !n.mandate_name.is_empty() {
                        match self.symbols.lookup(&n.mandate_name) {
                            None => self.emit(
                                format!(
                                    "Undefined mandate '{}' in flow '{}'",
                                    n.mandate_name, flow_name
                                ),
                                &n.loc,
                            ),
                            Some(sym) if sym.kind != "mandate" => self.emit(
                                format!("'{}' is a {}, not a mandate", n.mandate_name, sym.kind),
                                &n.loc,
                            ),
                            _ => {}
                        }
                    }
                }
                FlowStep::LambdaDataApply(n) => {
                    if !n.lambda_data_name.is_empty() {
                        match self.symbols.lookup(&n.lambda_data_name) {
                            None => self.emit(
                                format!(
                                    "Undefined lambda '{}' in flow '{}'",
                                    n.lambda_data_name, flow_name
                                ),
                                &n.loc,
                            ),
                            Some(sym) if sym.kind != "lambda_data" => self.emit(
                                format!(
                                    "'{}' is a {}, not a lambda_data",
                                    n.lambda_data_name, sym.kind
                                ),
                                &n.loc,
                            ),
                            _ => {}
                        }
                    }
                    // Fase 15.d — output_type must not shadow primitive type names.
                    // Mirror of axon.compiler.type_checker._RESERVED_OUTPUT_TYPE_NAMES;
                    // drift is detected by tests/test_lambda_data_runtime.py::
                    // test_derivation_vocab_parity_with_compiler (sibling concept).
                    if !n.output_type.is_empty()
                        && RESERVED_OUTPUT_TYPE_NAMES
                            .contains(&n.output_type.to_ascii_lowercase().as_str())
                    {
                        self.emit(
                            format!(
                                "lambda apply output_type '{}' shadows a reserved \
                                 primitive / built-in type name — choose a distinct \
                                 name for the bound envelope",
                                n.output_type
                            ),
                            &n.loc,
                        );
                    }
                }
                FlowStep::Let(n) => {
                    // Fase 17.d — type-checker hardening for `let` bindings.
                    // Mirror of axon/compiler/type_checker.py::_check_let.
                    if n.identifier.is_empty() {
                        self.emit(
                            "let binding requires an identifier".to_string(),
                            &n.loc,
                        );
                    } else {
                        // Reserved primitive type name shadowing.
                        if RESERVED_OUTPUT_TYPE_NAMES
                            .contains(&n.identifier.to_ascii_lowercase().as_str())
                        {
                            self.emit(
                                format!(
                                    "let binding '{}' shadows a reserved primitive / \
                                     built-in type name — choose a distinct identifier",
                                    n.identifier
                                ),
                                &n.loc,
                            );
                        }
                        // Self-reference: `let X = X` or `let X = X.something`.
                        if n.value_kind == "reference" && !n.value_expr.is_empty() {
                            let head = n.value_expr.split('.').next().unwrap_or("");
                            if head == n.identifier {
                                self.emit(
                                    format!(
                                        "let binding '{}' is self-referential \
                                         (value '{}' starts with the binding name itself) — \
                                         cannot resolve at runtime",
                                        n.identifier, n.value_expr
                                    ),
                                    &n.loc,
                                );
                            }
                        }
                    }
                }
                FlowStep::Navigate(n) => {
                    if !n.pix_name.is_empty() {
                        match self.symbols.lookup(&n.pix_name) {
                            None => self.emit(
                                format!("Undefined pix '{}' in navigate step", n.pix_name),
                                &n.loc,
                            ),
                            Some(sym) if sym.kind != "pix" => self.emit(
                                format!("'{}' is a {}, not a pix", n.pix_name, sym.kind),
                                &n.loc,
                            ),
                            _ => {}
                        }
                    }
                    if n.query_expr.is_empty() {
                        self.emit(
                            "Navigate step requires a query expression".to_string(),
                            &n.loc,
                        );
                    }
                }
                FlowStep::Drill(n) => {
                    if !n.pix_name.is_empty() {
                        match self.symbols.lookup(&n.pix_name) {
                            None => self.emit(
                                format!("Undefined pix '{}' in drill step", n.pix_name),
                                &n.loc,
                            ),
                            Some(sym) if sym.kind != "pix" => self.emit(
                                format!("'{}' is a {}, not a pix", n.pix_name, sym.kind),
                                &n.loc,
                            ),
                            _ => {}
                        }
                    }
                    if n.subtree_path.is_empty() {
                        self.emit("Drill step requires a subtree_path".to_string(), &n.loc);
                    }
                    if n.query_expr.is_empty() {
                        self.emit("Drill step requires a query expression".to_string(), &n.loc);
                    }
                }
                FlowStep::Trail(n) => {
                    if n.navigate_ref.is_empty() {
                        self.emit("Trail step requires a navigate_ref".to_string(), &n.loc);
                    }
                }
                FlowStep::Corroborate(n) => {
                    if n.navigate_ref.is_empty() {
                        self.emit(
                            "Corroborate step requires a navigate_ref".to_string(),
                            &n.loc,
                        );
                    }
                }
                FlowStep::DaemonStep(n) => {
                    if !n.daemon_ref.is_empty() {
                        match self.symbols.lookup(&n.daemon_ref) {
                            None => self.emit(
                                format!(
                                    "Undefined daemon '{}' in flow '{}'",
                                    n.daemon_ref, flow_name
                                ),
                                &n.loc,
                            ),
                            Some(sym) if sym.kind != "daemon" => self.emit(
                                format!("'{}' is a {}, not a daemon", n.daemon_ref, sym.kind),
                                &n.loc,
                            ),
                            _ => {}
                        }
                    }
                }
                FlowStep::Persist(n) => {
                    self.check_store_ref(&n.store_name, flow_name, &n.loc);
                    // §Fase 38.e — D2 second half: persist field-block
                    // proof (axon-T803 NOT-NULL omission + axon-T804
                    // unknown field + axon-T802 value-type mismatch).
                    self.run_38e_persist_proof(&n.store_name, &n.fields, &n.loc);
                }
                FlowStep::Retrieve(n) => {
                    self.check_store_ref(&n.store_name, flow_name, &n.loc);
                    self.run_38d_where_proof(&n.store_name, &n.where_expr, &n.loc);
                }
                FlowStep::Mutate(n) => {
                    self.check_store_ref(&n.store_name, flow_name, &n.loc);
                    self.run_38d_where_proof(&n.store_name, &n.where_expr, &n.loc);
                    // §Fase 38.e — D2 second half: mutate SET-block
                    // proof (axon-T804 unknown field + axon-T802
                    // value-type mismatch). NOT-NULL omission (T803)
                    // does NOT apply to mutate (UPDATE preserves
                    // existing values for omitted columns).
                    self.run_38e_mutate_proof(&n.store_name, &n.fields, &n.loc);
                }
                FlowStep::Purge(n) => {
                    self.check_store_ref(&n.store_name, flow_name, &n.loc);
                    self.run_38d_where_proof(&n.store_name, &n.where_expr, &n.loc);
                }
                FlowStep::ComputeApply(n) => {
                    if !n.compute_name.is_empty() {
                        match self.symbols.lookup(&n.compute_name) {
                            None => self.emit(
                                format!(
                                    "Undefined compute '{}' in flow '{}'",
                                    n.compute_name, flow_name
                                ),
                                &n.loc,
                            ),
                            Some(sym) if sym.kind != "compute" => self.emit(
                                format!("'{}' is a {}, not a compute", n.compute_name, sym.kind),
                                &n.loc,
                            ),
                            _ => {}
                        }
                    }
                }
                // Recurse into control flow bodies
                FlowStep::If(n) => {
                    self.check_flow_steps(&n.then_body, flow_name);
                    self.check_flow_steps(&n.else_body, flow_name);
                }
                FlowStep::ForIn(n) => {
                    self.check_flow_steps(&n.body, flow_name);
                }
                // §λ-L-E Fase 13 — Mobile typed channel reductions
                FlowStep::Emit(n) => self.check_emit(n),
                FlowStep::Publish(n) => self.check_publish(n),
                FlowStep::Discover(n) => self.check_discover(n),
                // All other steps: no cross-reference checks needed
                _ => {}
            }
        }
    }

    fn check_store_ref(&mut self, store_name: &str, flow_name: &str, loc: &Loc) {
        if !store_name.is_empty() {
            match self.symbols.lookup(store_name) {
                None => self.emit(
                    format!(
                        "Undefined axonstore '{}' in flow '{}'",
                        store_name, flow_name
                    ),
                    loc,
                ),
                Some(sym) if sym.kind != "axonstore" => self.emit(
                    format!("'{}' is a {}, not an axonstore", store_name, sym.kind),
                    loc,
                ),
                _ => {}
            }
        }
    }

    /// §Fase 38.d (D2) — run the `where:` column-type proof against
    /// the store's declared INLINE schema (form a). Forms (b)/(c)
    /// silently skip at this layer (they're proven at deploy time —
    /// D8, in 38.f — when filesystem context for manifest discovery
    /// exists). Every proof failure is converted to a `TypeError`
    /// anchored at the store-op's source location.
    fn run_38d_where_proof(&mut self, store_name: &str, where_expr: &str, loc: &Loc) {
        if store_name.is_empty() || where_expr.trim().is_empty() {
            return;
        }
        let cs = match self.store_inline_column_sets.get(store_name) {
            Some(cs) => cs.clone(),
            None => return, // no inline schema declared → 38.d silently skips
        };
        let errors = crate::store_column_proof::check_filter(
            where_expr,
            &cs,
            &self.current_flow_params,
            (loc.line, loc.column),
        );
        for err in errors {
            self.emit(err.message, loc);
        }
    }

    /// §Fase 38.e (D2 — second half) — run the `persist` field-block
    /// proof: axon-T803 NOT-NULL omission + axon-T804 unknown field +
    /// axon-T802 value-type mismatch. An empty fields block (the
    /// v1.30.0 blockless `persist <store>` form that writes user
    /// bindings) is silently skipped per D5 absolute.
    fn run_38e_persist_proof(
        &mut self,
        store_name: &str,
        fields: &[(String, String)],
        loc: &Loc,
    ) {
        if store_name.is_empty() || fields.is_empty() {
            return;
        }
        let cs = match self.store_inline_column_sets.get(store_name) {
            Some(cs) => cs.clone(),
            None => return,
        };
        let errors = crate::store_column_proof::check_persist_fields(
            fields,
            &cs,
            &self.current_flow_params,
            (loc.line, loc.column),
        );
        for err in errors {
            self.emit(err.message, loc);
        }
    }

    /// §Fase 38.e (D2 — second half) — run the `mutate` SET-block
    /// proof: axon-T804 unknown field + axon-T802 value-type mismatch.
    /// NOT-NULL omission (T803) does NOT apply to mutate (UPDATE
    /// preserves existing values for omitted columns).
    fn run_38e_mutate_proof(
        &mut self,
        store_name: &str,
        fields: &[(String, String)],
        loc: &Loc,
    ) {
        if store_name.is_empty() || fields.is_empty() {
            return;
        }
        let cs = match self.store_inline_column_sets.get(store_name) {
            Some(cs) => cs.clone(),
            None => return,
        };
        let errors = crate::store_column_proof::check_mutate_fields(
            fields,
            &cs,
            &self.current_flow_params,
            (loc.line, loc.column),
        );
        for err in errors {
            self.emit(err.message, loc);
        }
    }

    // ── Type reference validation (epistemic lattice) ──────────────

    /// Verify that a type name is either built-in or user-defined.
    /// Soft check: unknown types are silently accepted (may come from imports).
    fn check_type_reference(&self, type_name: &str, _loc: &Loc) -> bool {
        if type_name.is_empty() {
            return true;
        }
        let builtin = epistemic::builtin_types();
        if builtin.contains(type_name) {
            return true;
        }
        if self
            .symbols
            .lookup(type_name)
            .map_or(false, |s| s.kind == "type")
        {
            return true;
        }
        // Soft: unknown types accepted silently (may be from imports)
        true
    }

    // ── Epistemic mode validation ──────────────────────────────────

    fn check_epistemic_mode(&mut self, mode: &str, loc: &Loc) {
        const VALID_EPISTEMIC_MODES: &[&str] = &["believe", "doubt", "know", "speculate"];
        if !mode.is_empty() && !is_valid(mode, VALID_EPISTEMIC_MODES) {
            self.emit(
                format!(
                    "Unknown epistemic mode '{}'. Valid: {}",
                    mode,
                    valid_list(VALID_EPISTEMIC_MODES)
                ),
                loc,
            );
        }
    }

    // ──────────────────────────────────────────────────────────────────
    //  §λ-L-E Fase 13 — Mobile Typed Channels validation
    //  (paper_mobile_channels.md §3 + Fase 13.b parity port)
    // ──────────────────────────────────────────────────────────────────

    /// Validate `channel Name { … }` (paper §3.1 + §3.4 shield prereq).
    fn check_channel(&mut self, node: &ChannelDefinition) {
        if node.name.is_empty() {
            self.emit("channel requires a name".to_string(), &node.loc);
        }
        // Resolve the message schema; supports nested `Channel<…<T>>`.
        if node.message.is_empty() {
            self.emit(
                "channel requires a `message:` schema type".to_string(),
                &node.loc,
            );
        } else {
            self.validate_channel_message_type(&node.message, &node.loc);
        }
        // Optional shield reference must resolve when set (D8 prereq).
        if !node.shield_ref.is_empty() {
            match self.symbols.lookup(&node.shield_ref) {
                None => self.emit(
                    format!(
                        "channel '{}' references undefined shield '{}'",
                        node.name, node.shield_ref
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "shield" => self.emit(
                    format!(
                        "channel '{}' shield '{}' is a {}, not a shield",
                        node.name, node.shield_ref, sym.kind
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
    }

    /// Recursively validate a `message:` spelling.  `Channel<T>` peels
    /// one layer; the leaf must be a builtin / user type / channel name.
    /// Soft-resolve unknown leaves (consistent with resource conventions).
    fn validate_channel_message_type(&mut self, spelling: &str, _loc: &Loc) {
        let s = spelling.trim();
        if s.starts_with("Channel<") && s.ends_with('>') {
            let inner = &s["Channel<".len()..s.len() - 1];
            self.validate_channel_message_type(inner, _loc);
            return;
        }
        // Plain type name — silently accepted whether builtin, user-typed,
        // or a registered channel.  Type references are intentionally soft
        // here (matches resource/manifest convention).
    }

    /// Validate `daemon` body — listeners + delegated flow-step checks.
    /// Pre-Fase 13 the Rust checker skipped daemons entirely; we now
    /// walk listeners so emit/publish/discover/listen receive the same
    /// validation they do inside flows.
    fn check_daemon(&mut self, node: &DaemonDefinition) {
        if !node.shield_ref.is_empty() {
            match self.symbols.lookup(&node.shield_ref) {
                None => self.emit(
                    format!(
                        "daemon '{}' references undefined shield '{}'",
                        node.name, node.shield_ref
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "shield" => self.emit(
                    format!(
                        "daemon '{}' shield '{}' is a {}, not a shield",
                        node.name, node.shield_ref, sym.kind
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        }
        for listener in &node.listeners {
            self.check_listen(listener, &node.name);
        }
    }

    /// Validate a listen block (Fase 13 D4 dual-mode).
    fn check_listen(&mut self, node: &ListenStep, daemon_name: &str) {
        if node.channel_is_ref {
            match self.symbols.lookup(&node.channel) {
                None => self.emit(
                    format!(
                        "daemon '{}' listens on undefined channel '{}'",
                        daemon_name, node.channel
                    ),
                    &node.loc,
                ),
                Some(sym) if sym.kind != "channel" => self.emit(
                    format!(
                        "daemon '{}' listen target '{}' is a {}, not a channel",
                        daemon_name, node.channel, sym.kind
                    ),
                    &node.loc,
                ),
                _ => {}
            }
        } else {
            // Legacy string topic — D4 deprecation warning.
            self.warn(
                format!(
                    "daemon '{}' uses string topic '{}' which is deprecated since \
                     Fase 13 (v1.4.x). Migrate to a typed `channel` declaration; \
                     string topics will be removed in v2.0 (D4).",
                    daemon_name, node.channel
                ),
                &node.loc,
            );
        }
    }

    /// Validate an emit step (Chan-Output / Chan-Mobility, paper §3.1, §3.2).
    fn check_emit(&mut self, node: &EmitStatement) {
        if node.channel_ref.is_empty() {
            self.emit("emit requires a channel reference".to_string(), &node.loc);
            return;
        }
        let kind = match self.symbols.lookup(&node.channel_ref) {
            None => {
                self.emit(
                    format!("emit references undefined channel '{}'", node.channel_ref),
                    &node.loc,
                );
                return;
            }
            Some(sym) => sym.kind.clone(),
        };
        if kind != "channel" {
            self.emit(
                format!(
                    "emit target '{}' is a {}, not a channel",
                    node.channel_ref, kind
                ),
                &node.loc,
            );
            return;
        }
        if node.value_ref.is_empty() {
            self.emit(
                format!("emit on channel '{}' requires a value", node.channel_ref),
                &node.loc,
            );
            return;
        }
        // Fase 13.i — a dotted-access value_ref ("Step.output" or deeper)
        // references a prior step's result and is always scalar at the
        // type-check layer. The runtime resolves it via the executor's
        // ContextManager. Mobility (paper §3.2) is by definition a
        // bare-identifier case (a declared channel name), so the
        // second-order check below intentionally skips dotted paths.
        if node.value_ref.contains('.') {
            return;
        }
        // Second-order schema check (paper §3.2 Chan-Mobility): if the
        // outer channel carries `Channel<U>`, the value must resolve to
        // a channel whose own message equals U.  Lookup channel
        // definition by walking the AST so we don't need a separate
        // channel registry.
        let outer_msg = self.find_channel_message(&node.channel_ref);
        if let Some(outer) = outer_msg {
            if outer.starts_with("Channel<") && outer.ends_with('>') {
                let inner = &outer["Channel<".len()..outer.len() - 1];
                let value_kind = self
                    .symbols
                    .lookup(&node.value_ref)
                    .map(|s| s.kind.clone())
                    .unwrap_or_default();
                if value_kind != "channel" {
                    self.emit(
                        format!(
                            "emit on '{}' carries '{}' but value '{}' is not a \
                             channel handle (mobility violation, Chan-Mobility paper §3.2)",
                            node.channel_ref, outer, node.value_ref
                        ),
                        &node.loc,
                    );
                    return;
                }
                let value_msg = self
                    .find_channel_message(&node.value_ref)
                    .unwrap_or_default();
                if value_msg != inner {
                    self.emit(
                        format!(
                            "emit on '{}' expects Channel<{}> but '{}' carries \
                             Channel<{}> (second-order schema mismatch)",
                            node.channel_ref, inner, node.value_ref, value_msg
                        ),
                        &node.loc,
                    );
                }
            }
        }
    }

    /// Validate a publish step — D8 capability extrusion gate.
    fn check_publish(&mut self, node: &PublishStatement) {
        if node.channel_ref.is_empty() {
            self.emit(
                "publish requires a channel reference".to_string(),
                &node.loc,
            );
            return;
        }
        if node.shield_ref.is_empty() {
            self.emit(
                format!(
                    "publish '{}' requires a shield gate (D8 — capability \
                     extrusion is shield-mediated)",
                    node.channel_ref
                ),
                &node.loc,
            );
            return;
        }
        let ch_kind = match self.symbols.lookup(&node.channel_ref) {
            None => {
                self.emit(
                    format!(
                        "publish references undefined channel '{}'",
                        node.channel_ref
                    ),
                    &node.loc,
                );
                return;
            }
            Some(sym) => sym.kind.clone(),
        };
        if ch_kind != "channel" {
            self.emit(
                format!(
                    "publish target '{}' is a {}, not a channel",
                    node.channel_ref, ch_kind
                ),
                &node.loc,
            );
            return;
        }
        let sh_kind = match self.symbols.lookup(&node.shield_ref) {
            None => {
                self.emit(
                    format!(
                        "publish '{}' references undefined shield '{}'",
                        node.channel_ref, node.shield_ref
                    ),
                    &node.loc,
                );
                return;
            }
            Some(sym) => sym.kind.clone(),
        };
        if sh_kind != "shield" {
            self.emit(
                format!(
                    "publish gate '{}' is a {}, not a shield",
                    node.shield_ref, sh_kind
                ),
                &node.loc,
            );
        }
        // κ-coverage compliance enforcement is deferred to a follow-up
        // pass that walks TypeDefinition.compliance — the Rust checker
        // currently does not aggregate type compliance metadata, so this
        // mirrors the soft-resolve behaviour of resource/manifest checks.
    }

    /// Validate a discover step — capability_ref must be publishable.
    fn check_discover(&mut self, node: &DiscoverStatement) {
        if node.capability_ref.is_empty() {
            self.emit(
                "discover requires a channel reference".to_string(),
                &node.loc,
            );
            return;
        }
        if node.alias.is_empty() {
            self.emit(
                "discover requires an `as <alias>` binding".to_string(),
                &node.loc,
            );
            return;
        }
        let kind = match self.symbols.lookup(&node.capability_ref) {
            None => {
                self.emit(
                    format!(
                        "discover references undefined channel '{}'",
                        node.capability_ref
                    ),
                    &node.loc,
                );
                return;
            }
            Some(sym) => sym.kind.clone(),
        };
        if kind != "channel" {
            self.emit(
                format!(
                    "discover target '{}' is a {}, not a channel",
                    node.capability_ref, kind
                ),
                &node.loc,
            );
            return;
        }
        // Verify publishability: the channel must declare a shield_ref.
        let shield = self.find_channel_shield(&node.capability_ref);
        if shield.as_deref().unwrap_or("").is_empty() {
            self.emit(
                format!(
                    "discover '{}' is not publishable: its channel definition \
                     declares no shield (D8 — only shield-gated channels can \
                     be discovered)",
                    node.capability_ref
                ),
                &node.loc,
            );
        }
    }

    /// Find the `message:` field of a registered channel by name.
    fn find_channel_message(&self, name: &str) -> Option<String> {
        for decl in &self.program.declarations {
            if let Declaration::Channel(c) = decl {
                if c.name == name {
                    return Some(c.message.clone());
                }
            }
        }
        None
    }

    /// Find the `shield:` field of a registered channel by name.
    fn find_channel_shield(&self, name: &str) -> Option<String> {
        for decl in &self.program.declarations {
            if let Declaration::Channel(c) = decl {
                if c.name == name {
                    return Some(c.shield_ref.clone());
                }
            }
        }
        None
    }
}

// ── §λ-L-E Fase 4 — Honda-Vasconcelos helpers (free fns) ────────────────────

/// Honda-Vasconcelos duality on a single step pair:
/// `send T ↔ receive T`, `loop ↔ loop`, `end ↔ end`.
/// §Fase 41.b — lower a Fase 4 [`SessionRole`] (a flat `send`/`receive`/`loop`/
/// `end` step list) into the [`SessionType`] algebra of `crate::session`:
/// `send T` ↦ `!T.·`, `receive T` ↦ `?T.·`, a terminal `end` ↦ `end`, and a
/// terminal `loop` ↦ a `μ`-recursion back to the role's start
/// (`[send T, loop]` ↦ `μX. !T.X`). Prefix `end`/`loop` (malformed; caught by
/// `check_session_role`) are treated as the tail.
fn lower_session_role(role: &SessionRole) -> SessionType {
    let body = lower_session_steps(&role.steps);
    // A single role-level `μX` is the loop-back point: any `loop` (at the top
    // level or inside a branch) recurses to the role's start.
    if steps_contain_loop(&role.steps) {
        SessionType::rec("X", body)
    } else {
        body
    }
}

/// Lower a step sequence into a [`SessionType`] (§Fase 41.b). `send`/`receive`
/// prefix the continuation; `end`↦`end`, `loop`↦`X` (the role-level recursion
/// var); `select`/`branch` are terminal choices whose labelled branches each
/// lower recursively (their own sub-protocol).
fn lower_session_steps(steps: &[SessionStep]) -> SessionType {
    let Some((first, rest)) = steps.split_first() else {
        return SessionType::End;
    };
    match first.op.as_str() {
        "send" => SessionType::send(first.message_type.clone(), lower_session_steps(rest)),
        "receive" => SessionType::recv(first.message_type.clone(), lower_session_steps(rest)),
        "loop" => SessionType::var("X"),
        "end" => SessionType::End,
        "select" => SessionType::select(branch_types(&first.branches)),
        "branch" => SessionType::branch(branch_types(&first.branches)),
        // Malformed mid-sequence op; `check_session_role` flags it. Skip so
        // duality diagnostics stay focused on the real shape.
        _ => lower_session_steps(rest),
    }
}

fn branch_types(branches: &[SessionBranch]) -> impl Iterator<Item = (String, SessionType)> + '_ {
    branches.iter().map(|b| (b.label.clone(), lower_session_steps(&b.steps)))
}

/// True if any step (top-level or inside a `select`/`branch`) is a `loop` — the
/// role then carries a single `μX` whose `X` every `loop` recurses to.
fn steps_contain_loop(steps: &[SessionStep]) -> bool {
    steps.iter().any(|s| {
        s.op == "loop"
            || (matches!(s.op.as_str(), "select" | "branch") && s.branches.iter().any(|b| steps_contain_loop(&b.steps)))
    })
}

/// Directed-graph cycle detector (DFS with gray/black colouring). Returns
/// one representative ordering per strongly-connected cycle found.
fn find_cycles(adjacency: &std::collections::HashMap<String, Vec<String>>) -> Vec<Vec<String>> {
    let mut color: std::collections::HashMap<String, &'static str> =
        std::collections::HashMap::new();
    let mut stack: Vec<String> = Vec::new();
    let mut cycles: Vec<Vec<String>> = Vec::new();

    fn visit(
        n: &str,
        adjacency: &std::collections::HashMap<String, Vec<String>>,
        color: &mut std::collections::HashMap<String, &'static str>,
        stack: &mut Vec<String>,
        cycles: &mut Vec<Vec<String>>,
    ) {
        color.insert(n.to_string(), "gray");
        stack.push(n.to_string());
        let targets = adjacency.get(n).cloned().unwrap_or_default();
        for tgt in targets {
            match color.get(&tgt).copied() {
                Some("gray") => {
                    if let Some(idx) = stack.iter().position(|s| s == &tgt) {
                        cycles.push(stack[idx..].to_vec());
                    }
                }
                None => visit(&tgt, adjacency, color, stack, cycles),
                _ => {}
            }
        }
        stack.pop();
        color.insert(n.to_string(), "black");
    }

    let keys: Vec<String> = adjacency.keys().cloned().collect();
    for src in keys {
        if !color.contains_key(&src) {
            visit(&src, adjacency, &mut color, &mut stack, &mut cycles);
        }
    }
    cycles
}

fn cycle_to_edges<'a>(cycle: &[String], edges: &'a [TopologyEdge]) -> Vec<&'a TopologyEdge> {
    let n = cycle.len();
    let mut result = Vec::with_capacity(n);
    for i in 0..n {
        let src = &cycle[i];
        let tgt = &cycle[(i + 1) % n];
        if let Some(e) = edges.iter().find(|e| &e.source == src && &e.target == tgt) {
            result.push(e);
        }
    }
    result
}

/// Locate a session by name in the program's declarations (flat scan).
fn find_session_by_name<'a>(program: &'a Program, name: &str) -> Option<&'a SessionDefinition> {
    for decl in &program.declarations {
        if let Declaration::Session(s) = decl {
            if s.name == name {
                return Some(s);
            }
        }
    }
    None
}

/// §Fase 37.c — Render a `TypeExpr` for a diagnostic message:
/// `String`, `List<String>`, `String?` (optional marker appended).
fn fmt_type_expr(t: &TypeExpr) -> String {
    let mut s = t.name.clone();
    if !t.generic_param.is_empty() {
        s.push('<');
        s.push_str(&t.generic_param);
        s.push('>');
    }
    if t.optional {
        s.push('?');
    }
    s
}

fn find_type_by_name<'a>(program: &'a Program, name: &str) -> Option<&'a TypeDefinition> {
    for decl in &program.declarations {
        if let Declaration::Type(t) = decl {
            if t.name == name {
                return Some(t);
            }
        }
    }
    None
}

fn find_shield_by_name<'a>(program: &'a Program, name: &str) -> Option<&'a ShieldDefinition> {
    for decl in &program.declarations {
        if let Declaration::Shield(s) = decl {
            if s.name == name {
                return Some(s);
            }
        }
    }
    None
}

fn find_flow_by_name<'a>(program: &'a Program, name: &str) -> Option<&'a FlowDefinition> {
    for decl in &program.declarations {
        if let Declaration::Flow(f) = decl {
            if f.name == name {
                return Some(f);
            }
        }
    }
    None
}

// ═══════════════════════════════════════════════════════════════════
//  §FASE 31.b — TYPE-DRIVEN WIRE INFERENCE (D1, D7, D10)
// ═══════════════════════════════════════════════════════════════════
//
// Cross-stack mirror of Python `axon/compiler/type_checker.py`
// (`_implicit_transport` + `_compute_implicit_transports`). D7
// ratifies byte-identical inference across both stacks; the
// `tests/fixtures/fase31_implicit_transport/corpus.json` drift gate
// locks parity in CI.
//
// The inference rule (D1):
//
//   implicit_transport(F, E) =
//     declared_transport(E)          if transport_explicit
//     "sse"                           if produces_stream(F) ∧ ¬explicit
//     "json"                          otherwise
//
// `produces_stream(F)` is the 3-disjunct predicate from Fase 30.c
// (Rust port shipping here as part of 31.b — Fase 30.c was
// Python-only, with the Rust port deferred to 30.c.2; 31.b
// supersedes that deferral by shipping the predicate now, since
// the inference REQUIRES it cross-stack).
//
// Pillar trace:
//   MATHEMATICS — function on (Flow, AxonEndpoint, Program).
//   LOGIC       — disjunction of three formal predicates.
//   PHILOSOPHY  — the language is the wire's source of truth.
//   COMPUTING   — pure function; no side effects beyond AST mutation
//                  in `compute_implicit_transports`.
// ═══════════════════════════════════════════════════════════════════

/// Disjunct (b) helper: does the named tool declare a
/// `stream:<policy>` effect? Returns `false` for unresolved names.
fn tool_has_stream_effect(program: &Program, tool_name: &str) -> bool {
    if tool_name.is_empty() {
        return false;
    }
    for decl in &program.declarations {
        if let Declaration::Tool(t) = decl {
            if t.name == tool_name {
                if let Some(ref effects) = t.effects {
                    return effects.effects.iter().any(|e| e.starts_with("stream:"));
                }
                return false;
            }
        }
    }
    false
}

/// Disjunct (a): does any step in the flow have `output: Stream<T>`?
fn flow_has_stream_output(flow: &FlowDefinition) -> bool {
    for step in &flow.body {
        if let FlowStep::Step(s) = step {
            let out = s.output_type.trim();
            if out.starts_with("Stream<") && out.ends_with('>') {
                return true;
            }
        }
    }
    false
}

/// Look up the `tool_name` field on a `UseToolStep`. The exact field
/// name is `tool_name` for the Rust AST (mirrors Python's `UseToolNode`).
fn use_tool_step_name(u: &UseToolStep) -> &str {
    &u.tool_name
}

/// Disjunct (b): does the flow reach a tool with `effects:
/// <stream:<policy>>`? Walks both `FlowStep::UseTool` (top-level
/// flow-step) AND `FlowStep::Step(s)` where `s.apply_ref` resolves
/// to a tool — the latter is the Kivi-shape pattern (Fase 31.b
/// extension of the Fase 30.c predicate; see Python mirror for
/// the rationale).
pub fn flow_uses_streaming_tool(flow: &FlowDefinition, program: &Program) -> bool {
    let mut seen: std::collections::HashSet<String> = std::collections::HashSet::new();
    for step in &flow.body {
        match step {
            FlowStep::UseTool(u) => {
                let tn = use_tool_step_name(u);
                if !tn.is_empty()
                    && seen.insert(tn.to_string())
                    && tool_has_stream_effect(program, tn)
                {
                    return true;
                }
            }
            FlowStep::Step(s) => {
                // §Fase 31.b — `apply: <name>` inside a step body is
                // the canonical adopter pattern (Kivi 2026-05-11).
                if !s.apply_ref.is_empty()
                    && seen.insert(s.apply_ref.clone())
                    && tool_has_stream_effect(program, &s.apply_ref)
                {
                    return true;
                }
            }
            _ => {}
        }
    }
    false
}

/// Master predicate: disjunction of the formal layers from
/// Fase 30.c. Disjunct (c) `perform Stream.Yield(...)` is not
/// surfaced at this layer because the Rust AST does not currently
/// expose step-body perform expressions through `FlowStep` — that
/// path is the Rust frontend completion gap from Fase 30.e and is
/// covered by the runtime source-text fallback in
/// `axon-rs/src/axon_server.rs::classify_negotiation_via_source_text`.
/// Disjuncts (a) and (b) cover every adopter-observable in-AST
/// pattern (the Kivi case + every Fase 30.c-tested source).
pub fn produces_stream(flow: &FlowDefinition, program: &Program) -> bool {
    flow_has_stream_output(flow) || flow_uses_streaming_tool(flow, program)
}

/// Compute the inferred transport for one axonendpoint per D1.
///
/// Returns one of:
///   * `"sse"`  — explicit `transport: sse|ndjson` declared (D2 ndjson
///                inferred as sse for wire-format purposes today;
///                ndjson namespace remains reserved per Fase 30 D2),
///              OR `transport_explicit == false` AND `produces_stream`
///                evaluates true (D1 inference fires).
///   * `"json"` — explicit `transport: json` declared (D3 opt-out),
///              OR `transport_explicit == false` AND flow does not
///                produce a stream.
///
/// `flow` may be `None` when the endpoint's `execute_flow` does not
/// resolve to any flow in scope (a separate type-error reported
/// elsewhere); we conservatively default to declared-or-json.
///
/// NEVER panics. Total + deterministic over every input shape.
pub fn implicit_transport(
    endpoint: &AxonEndpointDefinition,
    flow: Option<&FlowDefinition>,
    program: &Program,
) -> String {
    if endpoint.transport_explicit {
        return match endpoint.transport.as_str() {
            // D2 — ndjson namespace reserved; semantically streaming.
            "ndjson" => "sse".to_string(),
            "sse" | "json" => endpoint.transport.clone(),
            // Unknown explicit value; parser would normally reject.
            // Defensive: default json.
            _ => "json".to_string(),
        };
    }
    // No explicit declaration; D1 inference path.
    match flow {
        Some(f) if produces_stream(f, program) => "sse".to_string(),
        _ => "json".to_string(),
    }
}

// ═══════════════════════════════════════════════════════════════════
//  §Fase 33.z.k.c (v1.28.0) — Effective dialect resolver
// ═══════════════════════════════════════════════════════════════════
//
// The dialect resolver answers the question "WHICH SSE dialect does
// this route emit?". It is orthogonal to `classify_dynamic_route_wire`
// which answers "IS the wire SSE?". The two compose:
//
//   1. classify_dynamic_route_wire → DynamicRouteWire::{Sse, Json}
//   2. If Sse:  resolve_effective_dialect → "axon" | "openai" | "anthropic"
//      If Json: dialect is "" (irrelevant)
//
// # Q1 algebraic-effect-driven default
//
// When the source omits the explicit `transport: sse(<dialect>)`
// parametrization, the resolver applies the founder-ratified default:
//   - openai: when the flow declares an algebraic effect (the tool
//             carries `effects: <stream:<policy>>`). The LLM-streaming
//             ecosystem expects OpenAI-style on the wire.
//   - axon:   when the flow uses type-annotation only
//             (`output: Stream<T>` without a tool effect). W3C
//             named-events stays the structural-commitment baseline.
//
// # D3 precedence preserved
//
// Adopter-explicit `transport: sse(<dialect>)` always wins. Adopter-
// explicit `transport: json` short-circuits before the resolver
// runs (the wire is JSON; no dialect applies).
//
// # Pure function discipline (D10)
//
// `resolve_effective_dialect` is total over its 2-input domain.
// Returns `""` only when called with an inconsistent state (no
// algebraic signal AND no explicit dialect AND no type-annotation
// stream — i.e., the caller violated the precondition that the
// wire IS SSE). Defensive: returns "axon" in that case rather than
// panic.
//
// Pillar trace:
//   MATHEMATICS — pure 2-input function with total domain.
//   LOGIC       — closed catalog of 3 outputs + defensive fallback.
//   PHILOSOPHY  — algebraic effects on tools drive openai default
//                 because that's where LLM-streaming adopters
//                 already live; type-annotation stays axon-baseline.
//   COMPUTING   — adopters' SDKs see the wire format their
//                 ecosystem documents; no client-side adapter
//                 work required.

/// Resolve which SSE dialect the runtime should emit for a route.
///
/// Precondition: caller already determined the wire IS SSE (via
/// `classify_dynamic_route_wire`). Calling this on a JSON-wire
/// route is meaningless but never panics.
///
/// Closed-catalog output: always one of `"axon"`, `"openai"`, or
/// `"anthropic"`. Never returns an empty string under valid input.
///
/// # Resolution rules (Q1 ratified)
///
/// 1. **Explicit dialect wins.** When `transport_dialect != ""`,
///    return it verbatim. (The parser already validated it
///    against `AXONENDPOINT_TRANSPORT_DIALECTS` so it's one of
///    `axon`/`openai`/`anthropic`.)
/// 2. **Algebraic-effect → openai.** Tool with declared stream
///    effect → adopters consume LLM-style streams → openai default.
/// 3. **Type-annotation only → axon.** No tool effect; W3C named
///    events stay the structural-commitment baseline.
pub fn resolve_effective_dialect(
    transport_dialect: &str,
    has_algebraic_stream_effect: bool,
) -> String {
    // Rule 1 — explicit dialect wins (D3-style precedence for the
    // dialect choice).
    if !transport_dialect.is_empty() {
        return transport_dialect.to_string();
    }
    // Rule 2 — algebraic effect (disjunct b) → openai default.
    if has_algebraic_stream_effect {
        return "openai".to_string();
    }
    // Rule 3 — type-annotation only (disjunct a) → axon default.
    "axon".to_string()
}

// ═══════════════════════════════════════════════════════════════════
//  §FASE 31.c — COMPILE-TIME WARNING `axon-W001` (D4, D10)
// ═══════════════════════════════════════════════════════════════════
//
// Rust mirror of Python `_emit_implicit_transport_warnings`. Same
// emission conditions, same message shape, same warning code
// `axon-W001`. D7 cross-stack contract: both stacks render
// byte-identical warning text for byte-identical input.

/// Warning code namespace per D4 — first entry in the warning
/// namespace `axon-Wnnn`. Errors keep their `axon-Ennn` namespace
/// from Fase 28 + Fase 30.
pub const W001_CODE: &str = "axon-W001";

/// §Fase 36.k (D10) — warning code for an `axonendpoint` that
/// declares no `backend:`.
///
/// `axon-W002` is held by the runtime warning catalog
/// (`axon::runtime_warnings` — `streaming-not-supported`, Fase
/// 33.x.g); the `axon-Wnnn` namespace is shared across the frontend
/// and the runtime, so the next free slot is `axon-W003`.
pub const W003_CODE: &str = "axon-W003";

/// §Fase 36.k (D10) — build the canonical `axon-W003` message: an
/// `axonendpoint` that declares no `backend:` relies on ladder
/// resolution. Emitted by `check_axonendpoint`, surfaced by
/// `axon check` (and promoted to an error under `--strict`).
fn build_w003_message(endpoint_name: &str) -> String {
    format!(
        "warning[{W003_CODE}]: axonendpoint '{endpoint_name}' declares \
         no `backend:` — its execution backend is resolved at request \
         time down the Fase 36 precedence ladder (server default → \
         environment-available providers). If none resolves the \
         endpoint fails with a structured HTTP 503; it never silently \
         runs the no-op `stub`. Declare `backend: <provider>` to pin \
         the model, or `backend: auto` to make the reliance on ladder \
         resolution explicit and silence this warning."
    )
}

/// Find the most informative description of WHY the flow produces
/// a stream — mirror of Python `_describe_stream_origin`. Used by
/// the W001 warning builder to make the diagnostic paste-actionable.
fn describe_stream_origin(flow: &FlowDefinition, program: &Program) -> String {
    // Disjunct (a) — step with `output: Stream<T>`.
    for step in &flow.body {
        if let FlowStep::Step(s) = step {
            let out = s.output_type.trim();
            if out.starts_with("Stream<") && out.ends_with('>') {
                return format!("step '{}' has `output: {}`", s.name, s.output_type);
            }
        }
    }
    // Disjunct (b) — find the first stream-effect tool reference.
    let mut seen: std::collections::HashSet<String> = std::collections::HashSet::new();
    for step in &flow.body {
        match step {
            FlowStep::Step(s) => {
                if !s.apply_ref.is_empty() && seen.insert(s.apply_ref.clone()) {
                    if let Some(policy) = tool_stream_policy(program, &s.apply_ref) {
                        return format!(
                            "step '{}' applies tool '{}' with effects `<{}>`",
                            s.name, s.apply_ref, policy
                        );
                    }
                }
            }
            FlowStep::UseTool(u) => {
                let tn = use_tool_step_name(u);
                if !tn.is_empty() && seen.insert(tn.to_string()) {
                    if let Some(policy) = tool_stream_policy(program, tn) {
                        return format!(
                            "tool '{}' is used directly with effects `<{}>`",
                            tn, policy
                        );
                    }
                }
            }
            _ => {}
        }
    }
    "its declared algebraic effects".to_string()
}

/// Resolve a tool by name and return the first `stream:<policy>`
/// effect, or `None` if the tool doesn't exist / has no stream effect.
fn tool_stream_policy(program: &Program, tool_name: &str) -> Option<String> {
    for decl in &program.declarations {
        if let Declaration::Tool(t) = decl {
            if t.name == tool_name {
                if let Some(ref effects) = t.effects {
                    for e in &effects.effects {
                        if e.starts_with("stream:") {
                            return Some(e.clone());
                        }
                    }
                }
                return None;
            }
        }
    }
    None
}

/// Build the canonical W001 message text per D4. Mirrors Python
/// `_build_w001_message` byte-identically.
fn build_w001_message(endpoint: &AxonEndpointDefinition, flow: &FlowDefinition, program: &Program) -> String {
    let origin = describe_stream_origin(flow, program);
    format!(
        "warning[{}]: implicit `transport: sse` inferred from stream \
         effects on axonendpoint '{}' (flow '{}' produces a stream \
         via {}). Declare `transport: sse` to silence this warning \
         and lock in SSE behavior, or `transport: json` to opt out \
         and keep the legacy JSON wire format. When \
         `strict_type_driven_transport: true`, this endpoint emits \
         SSE on /v1/execute by default.",
        W001_CODE, endpoint.name, endpoint.execute_flow, origin
    )
}

/// Walk every `AxonEndpointDefinition` and emit one `axon-W001`
/// warning per implicit-sse site (D4). Returns the list of new
/// `TypeError` warnings — caller appends to whatever warning
/// collection it manages (e.g. `TypeChecker.warnings` or a
/// CLI-rendering buffer).
///
/// Emission conditions (all must hold):
///   1. `endpoint.transport_explicit == false`
///   2. `endpoint.implicit_transport == "sse"`
///   3. The endpoint's `execute_flow` resolves to a flow in scope
///      (orphan endpoints emit no W001 — their separate error is
///      unrelated; a W001 attached would be noise).
///
/// Rate-limited per axonendpoint by construction. Safe to call
/// repeatedly (each call rebuilds the warning list — idempotent).
pub fn compute_implicit_transport_warnings(program: &Program) -> Vec<TypeError> {
    let mut warnings: Vec<TypeError> = Vec::new();
    let mut flow_indices: HashMap<String, usize> = HashMap::new();
    for (i, decl) in program.declarations.iter().enumerate() {
        if let Declaration::Flow(f) = decl {
            flow_indices.insert(f.name.clone(), i);
        }
    }
    for decl in &program.declarations {
        let ae = match decl {
            Declaration::AxonEndpoint(ae) => ae,
            _ => continue,
        };
        if ae.transport_explicit {
            continue;
        }
        if ae.implicit_transport != "sse" {
            continue;
        }
        let flow = match flow_indices.get(&ae.execute_flow) {
            Some(&fi) => match &program.declarations[fi] {
                Declaration::Flow(f) => f,
                _ => continue,
            },
            None => continue,
        };
        warnings.push(TypeError {
            message: build_w001_message(ae, flow, program),
            line: ae.loc.line,
            column: ae.loc.column,
        });
    }
    warnings
}

/// Walk every `AxonEndpointDefinition` in the program and attach
/// its computed `implicit_transport` per D1. Mutates the AST in
/// place. Idempotent + safe to re-run.
///
/// Mirrors Python `_compute_implicit_transports` byte-identically
/// (D7 cross-stack contract — locked in CI by the drift-gate
/// corpus at `tests/fixtures/fase31_implicit_transport/corpus.json`).
pub fn compute_implicit_transports(program: &mut Program) {
    // First pass: index every FlowDefinition by name. We must clone
    // the necessary references because subsequent mutation of
    // program.declarations needs &mut access; we cannot hold a
    // shared borrow simultaneously. Index uses indices into the
    // declarations Vec so we can resolve flows by name without
    // re-walking the whole Vec for each endpoint.
    let mut flow_indices: HashMap<String, usize> = HashMap::new();
    for (i, decl) in program.declarations.iter().enumerate() {
        if let Declaration::Flow(f) = decl {
            flow_indices.insert(f.name.clone(), i);
        }
    }

    // Second pass: walk endpoints. For each, look up the flow by
    // name (immutable borrow of program.declarations via index) and
    // compute the inference; then re-borrow mutably to assign the
    // result. Because Rust's borrow checker forbids simultaneous
    // immutable + mutable borrow of the same Vec, we precompute the
    // (endpoint_index, inferred_transport) pairs first, then apply
    // them all in a second mutating loop.
    // §Fase 33.z.k.1 (v1.27.1) — compute BOTH `implicit_transport`
    // (Fase 31 D1 inference) AND the new `has_algebraic_stream_effect`
    // predicate (algebraic-effect override). Both are read by the
    // runtime classifier; the algebraic-effect predicate carries
    // strictly more information (it isolates disjunct (b) of
    // `produces_stream` — the tool-effect signal — from disjunct (a)
    // — the type-annotation signal). The runtime promotes the route
    // to SSE unconditionally when the algebraic predicate is true
    // (D3 `transport: json` opt-out still wins).
    let mut updates: Vec<(usize, String, bool)> = Vec::new();
    for (i, decl) in program.declarations.iter().enumerate() {
        if let Declaration::AxonEndpoint(ae) = decl {
            let flow = flow_indices.get(&ae.execute_flow).and_then(|&fi| {
                if let Declaration::Flow(f) = &program.declarations[fi] {
                    Some(f)
                } else {
                    None
                }
            });
            let transport_result = implicit_transport(ae, flow, program);
            let algebraic_result = match flow {
                Some(f) => flow_uses_streaming_tool(f, program),
                None => false,
            };
            updates.push((i, transport_result, algebraic_result));
        }
    }
    for (i, transport_result, algebraic_result) in updates {
        if let Declaration::AxonEndpoint(ae) = &mut program.declarations[i] {
            ae.implicit_transport = transport_result;
            ae.has_algebraic_stream_effect = algebraic_result;
        }
    }
}

// ── §λ-L-E Fase 13 — Mobile Typed Channels type-checker tests ────────────────

#[cfg(test)]
mod fase13_typecheck_tests {
    use super::*;
    use crate::lexer::Lexer;
    use crate::parser::Parser;

    fn check_with_warnings(src: &str) -> (Vec<TypeError>, Vec<TypeError>) {
        let tokens = Lexer::new(src, "<test>").tokenize().expect("lex");
        let prog = Parser::new(tokens).parse().expect("parse");
        TypeChecker::new(&prog).check_with_warnings()
    }

    fn check_errors(src: &str) -> Vec<TypeError> {
        check_with_warnings(src).0
    }

    #[test]
    fn channel_with_valid_shield_clean() {
        let src = r#"
            type Order { id: String }
            shield Gate { scan: [pii_leak] }
            channel C { message: Order shield: Gate }
        "#;
        assert!(check_errors(src).is_empty());
    }

    #[test]
    fn channel_undefined_shield_rejected() {
        let src = "channel C { message: Order shield: NotDefined }";
        let errs = check_errors(src);
        assert!(
            errs.iter()
                .any(|e| e.message.contains("undefined shield 'NotDefined'")),
            "got: {:?}",
            errs
        );
    }

    #[test]
    fn channel_shield_wrong_kind_rejected() {
        let src = r#"
            type NotAShield { x: String }
            channel C { message: Order shield: NotAShield }
        "#;
        let errs = check_errors(src);
        assert!(
            errs.iter().any(|e| e.message.contains("not a shield")),
            "got: {:?}",
            errs
        );
    }

    #[test]
    fn emit_undefined_channel_rejected() {
        let src = "flow f() -> O { emit Bogus(payload) }";
        let errs = check_errors(src);
        assert!(
            errs.iter()
                .any(|e| e.message.contains("undefined channel 'Bogus'")),
            "got: {:?}",
            errs
        );
    }

    #[test]
    fn emit_target_wrong_kind_rejected() {
        let src = r#"
            type Order { id: String }
            flow f() -> O { emit Order(payload) }
        "#;
        let errs = check_errors(src);
        assert!(
            errs.iter().any(|e| e.message.contains("not a channel")),
            "got: {:?}",
            errs
        );
    }

    #[test]
    fn emit_mobility_schema_mismatch_rejected() {
        let src = r#"
            type Order { id: String }
            type Other { y: String }
            channel Wrong { message: Other }
            channel Outer { message: Channel<Order> }
            flow f() -> O { emit Outer(Wrong) }
        "#;
        let errs = check_errors(src);
        assert!(
            errs.iter()
                .any(|e| e.message.contains("second-order schema mismatch")),
            "got: {:?}",
            errs
        );
    }

    #[test]
    fn publish_undefined_shield_rejected() {
        let src = r#"
            channel C { message: Order }
            flow f() -> Cap { publish C within MissingShield }
        "#;
        let errs = check_errors(src);
        assert!(
            errs.iter()
                .any(|e| e.message.contains("undefined shield 'MissingShield'")),
            "got: {:?}",
            errs
        );
    }

    #[test]
    fn discover_unpublishable_channel_rejected() {
        let src = r#"
            type Order { id: String }
            channel C { message: Order }
            flow f() -> O { discover C as ch }
        "#;
        let errs = check_errors(src);
        assert!(
            errs.iter().any(|e| e.message.contains("not publishable")),
            "got: {:?}",
            errs
        );
    }

    #[test]
    fn listen_typed_channel_clean() {
        let src = r#"
            type Order { id: String }
            channel C { message: Order }
            daemon D() {
                goal: "x"
                listen C as ev { }
            }
        "#;
        let (errs, warns) = check_with_warnings(src);
        assert!(errs.is_empty(), "errors: {:?}", errs);
        assert!(warns.is_empty(), "no warnings expected: {:?}", warns);
    }

    #[test]
    fn listen_typed_undefined_rejected() {
        let src = r#"
            daemon D() {
                goal: "x"
                listen NoSuchChannel as ev { }
            }
        "#;
        let errs = check_errors(src);
        assert!(
            errs.iter().any(|e| e.message.contains("undefined channel")),
            "got: {:?}",
            errs
        );
    }

    #[test]
    fn listen_string_topic_emits_d4_warning() {
        let src = r#"
            daemon D() {
                goal: "x"
                listen "orders.created" as ev { }
            }
        "#;
        let (errs, warns) = check_with_warnings(src);
        assert!(errs.is_empty(), "no errors expected: {:?}", errs);
        assert_eq!(warns.len(), 1);
        assert!(warns[0].message.contains("deprecated since Fase 13"));
        assert!(warns[0].message.contains("orders.created"));
    }

    #[test]
    fn listen_dual_mode_only_legacy_warns() {
        let src = r#"
            type Order { id: String }
            channel C { message: Order }
            daemon Mixed() {
                goal: "x"
                listen C as canonical { }
                listen "legacy" as legacy_ev { }
            }
        "#;
        let (errs, warns) = check_with_warnings(src);
        assert!(errs.is_empty(), "no errors expected: {:?}", errs);
        assert_eq!(warns.len(), 1, "only legacy emits a warning");
        assert!(warns[0].message.contains("legacy"));
    }

    // ── Fase 13.i — type checker tolerates dotted-access value_ref ──

    #[test]
    fn emit_dotted_value_ref_does_not_trip_mobility_check() {
        // Previously, a second-order channel with a dotted-access value
        // would falsely error as "not a channel handle". With 13.i the
        // mobility check must skip when value_ref contains '.'.
        let src = r#"
            channel Inner { message: Bytes qos: at_least_once }
            channel Outer { message: Channel<Bytes> qos: at_least_once }
            flow f() -> Out {
                emit Outer(Build.handle)
            }
        "#;
        let errs = check_errors(src);
        let mobility = errs
            .iter()
            .filter(|e| {
                e.message.contains("second-order schema mismatch")
                    || e.message.contains("not a channel handle")
            })
            .count();
        assert_eq!(
            mobility, 0,
            "dotted access must not trip mobility check; got: {:?}",
            errs
        );
    }

    #[test]
    fn emit_bare_identifier_mobility_check_still_runs() {
        // Regression guard — non-dotted refs still get the second-order
        // check applied, so a wrong handle is still rejected.
        let src = r#"
            channel Inner { message: Bytes qos: at_least_once }
            channel Wrong { message: Integer qos: at_least_once }
            channel Outer { message: Channel<Bytes> qos: at_least_once }
            flow f() -> Out {
                emit Outer(Wrong)
            }
        "#;
        let errs = check_errors(src);
        assert!(
            errs.iter()
                .any(|e| e.message.contains("second-order schema mismatch")),
            "expected mobility violation for bare-id ref, got: {:?}",
            errs
        );
    }
}

// ── §Fase 35.j — Pillar IV: capability-typed store access ───────────

#[cfg(test)]
mod fase35j_capability_tests {
    use super::*;
    use crate::lexer::Lexer;
    use crate::parser::Parser;

    fn check_errors(src: &str) -> Vec<TypeError> {
        let tokens = Lexer::new(src, "<test>").tokenize().expect("lex");
        let prog = Parser::new(tokens).parse().expect("parse");
        TypeChecker::new(&prog).check()
    }

    fn mentions_capability(errs: &[TypeError]) -> bool {
        errs.iter().any(|e| e.message.contains("requiring capability"))
    }

    #[test]
    fn endpoint_must_grant_a_gated_store_capability() {
        // The flow accesses a `capability: "tenant.read"` store, but
        // the endpoint executing it grants nothing → a type error.
        let src = r#"
            axonstore tenants {
                backend: postgresql
                connection: "env:DB"
                capability: "tenant.read"
            }
            flow GetTenants() -> Unit {
                retrieve tenants { where: "id = 1" }
            }
            axonendpoint Ep { method: GET path: "/t" execute: GetTenants }
        "#;
        assert!(
            mentions_capability(&check_errors(src)),
            "an endpoint that does not grant the store's capability \
             must fail the compositional check"
        );
    }

    #[test]
    fn endpoint_granting_the_capability_type_checks_clean() {
        let src = r#"
            axonstore tenants {
                backend: postgresql
                connection: "env:DB"
                capability: "tenant.read"
            }
            flow GetTenants() -> Unit {
                retrieve tenants { where: "id = 1" }
            }
            axonendpoint Ep {
                method: GET path: "/t" execute: GetTenants
                requires: [tenant.read]
            }
        "#;
        assert!(
            !mentions_capability(&check_errors(src)),
            "an endpoint that grants the capability must type-check clean"
        );
    }

    #[test]
    fn ungated_store_needs_no_endpoint_grant() {
        let src = r#"
            axonstore cache { backend: postgresql connection: "env:DB" }
            flow Fetch() -> Unit {
                retrieve cache { where: "k = 1" }
            }
            axonendpoint Ep { method: GET path: "/c" execute: Fetch }
        "#;
        assert!(
            !mentions_capability(&check_errors(src)),
            "a store with no `capability:` requires no endpoint grant"
        );
    }

    #[test]
    fn malformed_capability_slug_is_a_parse_error() {
        // The closed slug grammar is enforced at parse time.
        let src = r#"axonstore s { backend: postgresql connection: "env:DB" capability: "Tenant.Read" }"#;
        let tokens = Lexer::new(src, "<test>").tokenize().expect("lex");
        assert!(
            Parser::new(tokens).parse().is_err(),
            "an uppercase capability slug must be rejected at parse time"
        );
    }
}

// ════════════════════════════════════════════════════════════════════
//  §Fase 37.y.4 — D3 union-coverage + D4 T901 collision rejection
// ════════════════════════════════════════════════════════════════════

#[cfg(test)]
mod fase37y_d3_d4_tests {
    use super::*;
    use crate::lexer::Lexer;
    use crate::parser::Parser;

    fn check_errors(src: &str) -> Vec<TypeError> {
        let tokens = Lexer::new(src, "<test>").tokenize().expect("lex");
        let prog = Parser::new(tokens).parse().expect("parse");
        TypeChecker::new(&prog).check()
    }

    #[test]
    fn d3_path_only_param_passes_d2_totality() {
        let src = r#"
            type SecretWriteRequest { value: Text }
            type WriteResult { ok: Bool }
            axonendpoint write_secret {
                method: POST
                path: "/api/tenants/{tenant_id}/secrets/{secret_name}"
                body: SecretWriteRequest
                execute: WriteSecret
            }
            flow WriteSecret(tenant_id: Text, secret_name: Text, value: Text) -> WriteResult {
                step Echo { reason: "ok" output: WriteResult }
            }
        "#;
        let errs = check_errors(src);
        let binding_errs: Vec<&TypeError> = errs
            .iter()
            .filter(|e| {
                e.message.contains("tenant_id")
                    || e.message.contains("secret_name")
                    || e.message.contains("Request Binding")
            })
            .collect();
        assert!(
            binding_errs.is_empty(),
            "D3 — path-only params must satisfy D2 totality. Got: {binding_errs:#?}"
        );
    }

    #[test]
    fn d3_query_only_param_passes_d2_totality() {
        let src = r#"
            type UserList { count: Int }
            axonendpoint list_users {
                method: GET
                path: "/api/users"
                query: { status: Text }
                execute: ListUsers
            }
            flow ListUsers(status: Text) -> UserList {
                step Build { reason: "list" output: UserList }
            }
        "#;
        let errs = check_errors(src);
        let binding_errs: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("status") || e.message.contains("Request Binding"))
            .collect();
        assert!(
            binding_errs.is_empty(),
            "D3 — query-only params must satisfy D2 totality. Got: {binding_errs:#?}"
        );
    }

    #[test]
    fn d3_mixed_path_query_body_coverage_passes() {
        let src = r#"
            type CreateRequest { content: Text }
            type CreateResult { id: Uuid }
            axonendpoint create_item {
                method: POST
                path: "/api/orgs/{org_id}/items"
                query: { dry_run: Bool? }
                body: CreateRequest
                execute: CreateItem
            }
            flow CreateItem(org_id: Text, dry_run: Bool?, content: Text) -> CreateResult {
                step Build { reason: "create" output: CreateResult }
            }
        "#;
        let errs = check_errors(src);
        let binding_errs: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("Request Binding") || e.message.contains("axon-T901"))
            .collect();
        assert!(
            binding_errs.is_empty(),
            "D3 — mixed coverage must satisfy D2. Got: {binding_errs:#?}"
        );
    }

    #[test]
    fn d3_missing_param_extended_hint_names_all_three_sources() {
        let src = r#"
            type Empty { ok: Bool }
            axonendpoint x {
                method: POST
                path: "/api/x"
                body: Empty
                execute: X
            }
            flow X(missing: Text) -> Empty {
                step S { reason: "x" output: Empty }
            }
        "#;
        let errs = check_errors(src);
        let hint = errs.iter().find(|e| e.message.contains("missing")).expect(
            "missing-binding error must surface",
        );
        assert!(hint.message.contains("path placeholder"), "hint names path: {}", hint.message);
        assert!(hint.message.contains("query"), "hint names query: {}", hint.message);
        assert!(hint.message.contains("body"), "hint names body: {}", hint.message);
    }

    #[test]
    fn d4_t901_collision_path_and_body() {
        let src = r#"
            type SecretWriteRequest { tenant_id: Text, value: Text }
            type WriteResult { ok: Bool }
            axonendpoint write {
                method: POST
                path: "/api/tenants/{tenant_id}"
                body: SecretWriteRequest
                execute: Write
            }
            flow Write(tenant_id: Text, value: Text) -> WriteResult {
                step S { reason: "x" output: WriteResult }
            }
        "#;
        let errs = check_errors(src);
        let t901 = errs.iter().find(|e| e.message.contains("axon-T901"));
        assert!(
            t901.is_some(),
            "D4 — path+body collision must emit axon-T901. Errors: {errs:#?}"
        );
        let msg = &t901.unwrap().message;
        assert!(msg.contains("path and body"), "names both sources: {msg}");
        assert!(msg.contains("tenant_id"), "names the colliding param: {msg}");
    }

    #[test]
    fn d4_t901_collision_path_and_query() {
        let src = r#"
            type Empty { ok: Bool }
            axonendpoint x {
                method: GET
                path: "/api/users/{id}"
                query: { id: Text }
                execute: X
            }
            flow X(id: Text) -> Empty {
                step S { reason: "x" output: Empty }
            }
        "#;
        let errs = check_errors(src);
        let t901 = errs.iter().find(|e| e.message.contains("axon-T901"));
        assert!(t901.is_some(), "D4 — path+query collision. Errs: {errs:#?}");
        assert!(
            t901.unwrap().message.contains("path and query"),
            "names path AND query"
        );
    }

    #[test]
    fn d4_t901_collision_query_and_body() {
        let src = r#"
            type Req { status: Text }
            type Empty { ok: Bool }
            axonendpoint x {
                method: POST
                path: "/api/x"
                query: { status: Text }
                body: Req
                execute: X
            }
            flow X(status: Text) -> Empty {
                step S { reason: "x" output: Empty }
            }
        "#;
        let errs = check_errors(src);
        let t901 = errs.iter().find(|e| e.message.contains("axon-T901"));
        assert!(t901.is_some(), "D4 — query+body collision. Errs: {errs:#?}");
        assert!(
            t901.unwrap().message.contains("query and body"),
            "names query AND body"
        );
    }

    #[test]
    fn d4_t901_collision_triple_source() {
        let src = r#"
            type Req { id: Text }
            type Empty { ok: Bool }
            axonendpoint x {
                method: POST
                path: "/api/{id}"
                query: { id: Text }
                body: Req
                execute: X
            }
            flow X(id: Text) -> Empty {
                step S { reason: "x" output: Empty }
            }
        "#;
        let errs = check_errors(src);
        let t901 = errs.iter().find(|e| e.message.contains("axon-T901"));
        assert!(t901.is_some(), "D4 — triple collision. Errs: {errs:#?}");
        let msg = &t901.unwrap().message;
        assert!(
            msg.contains("path, query, and body"),
            "names all three sources with Oxford comma: {msg}"
        );
        assert!(
            msg.contains("Remove the declaration from 2 of the sources"),
            "explicit count of removals needed: {msg}"
        );
    }

    #[test]
    fn d3_path_param_typed_non_text_emits_error() {
        let src = r#"
            type Empty { ok: Bool }
            axonendpoint x {
                method: GET
                path: "/api/users/{id}"
                execute: X
            }
            flow X(id: Uuid) -> Empty {
                step S { reason: "x" output: Empty }
            }
        "#;
        let errs = check_errors(src);
        let type_err = errs.iter().find(|e| {
            e.message.contains("path placeholder") && e.message.contains("Text")
        });
        assert!(
            type_err.is_some(),
            "path-binding type mismatch must surface. Errs: {errs:#?}"
        );
    }

    #[test]
    fn d3_query_param_type_mismatch_emits_error() {
        let src = r#"
            type Empty { ok: Bool }
            axonendpoint x {
                method: GET
                path: "/api/x"
                query: { limit: Int }
                execute: X
            }
            flow X(limit: Text) -> Empty {
                step S { reason: "x" output: Empty }
            }
        "#;
        let errs = check_errors(src);
        let type_err = errs.iter().find(|e| {
            e.message.contains("query: {") && e.message.contains("Int")
        });
        assert!(
            type_err.is_some(),
            "query-binding type mismatch must surface. Errs: {errs:#?}"
        );
    }

    #[test]
    fn d5_body_only_endpoint_legacy_behavior_intact() {
        let src_passes = r#"
            type Req { value: Text }
            type Empty { ok: Bool }
            axonendpoint x {
                method: POST
                path: "/api/x"
                body: Req
                execute: X
            }
            flow X(value: Text) -> Empty {
                step S { reason: "x" output: Empty }
            }
        "#;
        let errs = check_errors(src_passes);
        assert!(
            errs.iter().all(|e| !e.message.contains("Request Binding")

                && !e.message.contains("axon-T901")),
            "D5 — body-only happy path passes unchanged. Errs: {errs:#?}"
        );
    }

    #[test]
    fn d3_kivi_secret_write_passes_post_37y() {
        // The exact kivi adopter case — pre-37.y this was the
        // blocking bug. Post-37.y the build is green.
        let src = r#"
            type SecretWriteRequest { value: Text }
            type WriteResult { ok: Bool }
            axonendpoint write_secret {
                method: POST
                path: "/api/tenants/{tenant_id}/secrets/{secret_name}"
                query: { dry_run: Bool?, overwrite: Bool? }
                body: SecretWriteRequest
                execute: WriteSecret
            }
            flow WriteSecret(
                tenant_id: Text,
                secret_name: Text,
                dry_run: Bool?,
                overwrite: Bool?,
                value: Text
            ) -> WriteResult {
                step S { reason: "x" output: WriteResult }
            }
        "#;
        let errs = check_errors(src);
        let binding_errs: Vec<&TypeError> = errs
            .iter()
            .filter(|e| {
                e.message.contains("Request Binding") || e.message.contains("axon-T901")
            })
            .collect();
        assert!(
            binding_errs.is_empty(),
            "Kivi corpus must pass post-37.y. Got: {binding_errs:#?}"
        );
    }
}

// ════════════════════════════════════════════════════════════════════
//  §Fase 38.x.e — Retrieve Cardinality vs Output Singularity Gate
// ════════════════════════════════════════════════════════════════════

#[cfg(test)]
mod fase38xe_cardinality_tests {
    use super::*;
    use crate::lexer::Lexer;
    use crate::parser::Parser;

    fn check_errors(src: &str) -> Vec<TypeError> {
        let tokens = Lexer::new(src, "<test>").tokenize().expect("lex");
        let prog = Parser::new(tokens).parse().expect("parse");
        TypeChecker::new(&prog).check()
    }

    #[test]
    fn retrieve_tail_with_singular_output_emits_t9xx() {
        // §Fase 39.e UPDATE — the kivi-shape regression: endpoint
        // declares `output: T` (bare singular) on default
        // `transport: json` with a retrieve-tail flow producing
        // `List<T>`.
        //
        // - Pre-38.x.e (v1.x): passed `axon check` silently, failed
        //   at runtime with the opaque D5 `internal_validation_error`.
        // - 38.x.e (v1.39.0): fired `axon-T9XX retrieve_cardinality_mismatch`
        //   at compile time hinting `change to output: List<T>`.
        // - v1.40.0+: same hint but ALSO failed at D5 because the
        //   wire was the v1.x flat envelope (not a List).
        // - **39.e (v2.0.0)**: fires `axon-E039` at compile time
        //   with the canonical FlowEnvelope wrapping suggestion +
        //   sse migration alternative. This is the STRUCTURAL
        //   closure of the adopter-reported gap. T9XX is suppressed
        //   under E039 (single canonical diagnostic).
        let src = r#"
            type TenantRecord { id: Text }
            axonstore tenants { backend: in_memory }
            axonendpoint get_tenant {
                method: GET
                path: "/api/tenants/{tenant_id}"
                output: TenantRecord
                execute: GetTenant
            }
            flow GetTenant(tenant_id: Text) -> TenantRecord {
                retrieve tenants { where: "id = ${tenant_id}" as: result }
            }
        "#;
        let errs = check_errors(src);
        let e039: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-E039"))
            .collect();
        assert!(
            !e039.is_empty(),
            "§Fase 39.e (D12 α) — a bare-singular `output: T` on a \
             `transport: json` endpoint with retrieve-tail MUST emit \
             `axon-E039`. All errors: {errs:#?}"
        );
        let err = e039[0];
        // The retrieve-tail's inferred cardinality is plural of
        // `StoreRow` (the IR-level row type — the flow's declared
        // return type `TenantRecord` doesn't currently propagate
        // through the retrieve-step taxonomy). The diagnostic
        // honestly reflects what the inference sees; adopters map
        // `StoreRow` to their declared row type mentally. A future
        // sub-fase can refine the inference to use the flow's
        // declared return type when available.
        assert!(
            err.message.contains("FlowEnvelope<List<StoreRow>>")
                || err.message.contains("FlowEnvelope<List<TenantRecord>>"),
            "§39.e — the E039 hint MUST suggest a canonical \
             FlowEnvelope wrapping around the inferred tail \
             cardinality (List<StoreRow> from the IR retrieve-step \
             taxonomy today; List<TenantRecord> if inference is \
             refined). Got: {}",
            err.message
        );
        assert!(
            err.message.contains("transport: sse"),
            "§39.e — the E039 hint MUST also name the sse migration \
             alternative. Got: {}",
            err.message
        );
        // T9XX is suppressed under E039 — single canonical diagnostic.
        let t9xx: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-T9XX"))
            .collect();
        assert!(
            t9xx.is_empty(),
            "§39.e — when E039 fires, T9XX MUST be suppressed (single \
             canonical diagnostic with the right answer). Got: {t9xx:#?}"
        );
    }

    #[test]
    fn retrieve_tail_with_list_output_passes() {
        // D5 — the symmetric well-formed case: retrieve-tail flow
        // with `output: List<T>` endpoint. No T9XX fires.
        let src = r#"
            type TenantRecord { id: Text }
            axonstore tenants { backend: in_memory }
            axonendpoint list_tenants {
                method: GET
                path: "/api/tenants"
                output: List<TenantRecord>
                execute: ListTenants
            }
            flow ListTenants() -> List<TenantRecord> {
                retrieve tenants { where: "1 = 1" as: result }
            }
        "#;
        let errs = check_errors(src);
        let t9xx: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-T9XX"))
            .collect();
        assert!(
            t9xx.is_empty(),
            "§Fase 38.x.e D1 — a retrieve-tail flow with `output: \
             List<T>` is the well-formed case. No T9XX should fire. \
             Got: {t9xx:#?}"
        );
    }

    #[test]
    fn step_tail_with_singular_output_passes() {
        // The other well-formed case: flow's tail is a `step` returning
        // a singular type, matching the endpoint's singular output. No
        // T9XX fires (the step's return shape is the contract).
        let src = r#"
            type WriteResult { ok: Bool }
            axonendpoint write_secret {
                method: POST
                path: "/api/secrets"
                output: WriteResult
                execute: WriteSecret
            }
            flow WriteSecret() -> WriteResult {
                step Echo { reason: "ok" output: WriteResult }
            }
        "#;
        let errs = check_errors(src);
        let t9xx: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-T9XX"))
            .collect();
        assert!(
            t9xx.is_empty(),
            "§Fase 38.x.e D1 — a step-tail flow with matching singular \
             output is well-formed; no cardinality mismatch. Got: \
             {t9xx:#?}"
        );
    }

    #[test]
    fn no_output_declared_skips_gate() {
        // D1 honest scope — when the endpoint omits `output:` entirely
        // (empty string), the gate cannot determine the expected
        // cardinality and silently passes. Adopters who don't declare
        // output are NOT protected by this gate; the runtime path is
        // their only check. Documented as future Fase 38.x.f scope.
        let src = r#"
            type TenantRecord { id: Text }
            axonstore tenants { backend: in_memory }
            axonendpoint get_tenant_loose {
                method: GET
                path: "/api/tenants/{tenant_id}"
                execute: GetTenantLoose
            }
            flow GetTenantLoose(tenant_id: Text) -> Unit {
                retrieve tenants { where: "id = ${tenant_id}" as: result }
            }
        "#;
        let errs = check_errors(src);
        let t9xx: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-T9XX"))
            .collect();
        assert!(
            t9xx.is_empty(),
            "§Fase 38.x.e D1 — endpoint with no `output:` declared \
             skips the cardinality gate (honest scope). Got: {t9xx:#?}"
        );
    }

    #[test]
    fn stream_output_skips_gate() {
        // Stream<T> is its own cardinality concept (Plural<T> over
        // time, not a List). The v1.39.0 gate doesn't reason about
        // Stream — honestly deferred to Fase 38.x.f. Endpoints
        // declaring `output: Stream<T>` are NOT compared against the
        // flow tail.
        let src = r#"
            type Token { text: Text }
            axonendpoint stream_chat {
                method: POST
                path: "/api/stream"
                output: Stream<Token>
                execute: StreamChat
            }
            flow StreamChat() -> Stream<Token> {
                step Generate { ask: "stream" output: Stream<Token> }
            }
        "#;
        let errs = check_errors(src);
        let t9xx: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-T9XX"))
            .collect();
        assert!(
            t9xx.is_empty(),
            "§Fase 38.x.e D1 — Stream<T> output skips the gate \
             (v1.39.0 honest scope). Got: {t9xx:#?}"
        );
    }
}

// ════════════════════════════════════════════════════════════════════
// §Fase 39.a — FlowEnvelope<T> built-in primitive (Rust-canonical)
// ════════════════════════════════════════════════════════════════════
//
// Anchor §-assertions for sub-fase 39.a per the plan vivo
// `docs/fase/fase_39_pure_silicon_cognition.md`. Acceptance criterion:
//   declared_cardinality("FlowEnvelope<List<X>>") == Wrapped(Plural("X"))
// + transparent unwrap behavior at the gate
// + nested generic parser support (parse_type_expr recurses)
// + existing T9XX warnings preserved unchanged for non-wrapped declarations
// + zero regressions in the 447-lib + 38.x.e + 38.x.f anchor tests
//
// The full axon-E039 mandate enforcement (D12 α ratified — singular too
// requires FlowEnvelope wrapping for transport: json) lands in 39.e
// once the runtime wire envelope is in place (39.b). 39.a establishes
// the type-system FOUNDATION; behavior gate fires in 39.e.

#[cfg(test)]
mod fase39a_flow_envelope_tests {
    use super::*;
    use crate::lexer::Lexer;
    use crate::parser::Parser;

    fn check_errors(src: &str) -> Vec<TypeError> {
        let tokens = Lexer::new(src, "<test>").tokenize().expect("lex");
        let prog = Parser::new(tokens).parse().expect("parse");
        TypeChecker::new(&prog).check()
    }

    // ── §1 — declared_cardinality(FlowEnvelope<T>) recognition ──

    #[test]
    fn fase39a_flow_envelope_of_singular_is_wrapped_singular() {
        // §Fase 39.a §1 — `FlowEnvelope<TenantRecord>` recognized as
        // Wrapped(Singular("TenantRecord")). The wrapper preserves
        // inner cardinality through unwrap-recurse.
        let card = declared_cardinality("FlowEnvelope<TenantRecord>");
        match card {
            Cardinality::Wrapped(inner) => {
                assert_eq!(
                    *inner,
                    Cardinality::Singular("TenantRecord".to_string()),
                    "§39.a §1 — inner must be Singular(\"TenantRecord\")"
                );
            }
            other => panic!(
                "§39.a §1 — FlowEnvelope<TenantRecord> must yield \
                 Wrapped(Singular(...)). Got: {other:?}"
            ),
        }
    }

    #[test]
    fn fase39a_flow_envelope_of_list_is_wrapped_plural() {
        // §Fase 39.a §1 — the acceptance criterion verbatim:
        // declared_cardinality("FlowEnvelope<List<X>>") == Wrapped(Plural("X"))
        let card = declared_cardinality("FlowEnvelope<List<TenantRecord>>");
        match card {
            Cardinality::Wrapped(inner) => {
                assert_eq!(
                    *inner,
                    Cardinality::Plural("TenantRecord".to_string()),
                    "§39.a §1 acceptance — inner must be Plural(\"TenantRecord\") \
                     (the canonical retrieve-tail shape Kivi reported)"
                );
            }
            other => panic!(
                "§39.a §1 acceptance — FlowEnvelope<List<TenantRecord>> must \
                 yield Wrapped(Plural(\"TenantRecord\")). Got: {other:?}"
            ),
        }
    }

    #[test]
    fn fase39a_flow_envelope_of_stream_is_wrapped_stream() {
        // §Fase 39.a §1 — Stream<T> wrapped through FlowEnvelope.
        // Note: per D9 SSE wire keeps its own event family; this
        // shape is here for type-system completeness, not for runtime
        // SSE dispatch.
        let card = declared_cardinality("FlowEnvelope<Stream<Token>>");
        match card {
            Cardinality::Wrapped(inner) => {
                assert_eq!(
                    *inner,
                    Cardinality::StreamCardinality("Token".to_string()),
                    "§39.a §1 — inner must be StreamCardinality(\"Token\")"
                );
            }
            other => panic!(
                "§39.a §1 — FlowEnvelope<Stream<Token>> must yield \
                 Wrapped(StreamCardinality(...)). Got: {other:?}"
            ),
        }
    }

    #[test]
    fn fase39a_flow_envelope_of_any_is_wrapped_disagreed() {
        // §Fase 39.a §1 — `FlowEnvelope<Any>` is a degenerate but
        // valid wrap; the Any (Disagreed) propagates through.
        let card = declared_cardinality("FlowEnvelope<Any>");
        match card {
            Cardinality::Wrapped(inner) => {
                assert_eq!(
                    *inner,
                    Cardinality::Disagreed,
                    "§39.a §1 — FlowEnvelope<Any> inner must be Disagreed"
                );
            }
            other => panic!("§39.a §1 — got: {other:?}"),
        }
    }

    #[test]
    fn fase39a_nested_flow_envelope_is_doubly_wrapped() {
        // §Fase 39.a §1 — degenerate `FlowEnvelope<FlowEnvelope<X>>`
        // is syntactically valid (parser recursion) and semantically
        // double-wrapped. The unwrap-recurse at the gate handles
        // arbitrary depth transparently.
        let card = declared_cardinality("FlowEnvelope<FlowEnvelope<TenantRecord>>");
        match card {
            Cardinality::Wrapped(outer_inner) => match outer_inner.as_ref() {
                Cardinality::Wrapped(inner_inner) => {
                    assert_eq!(
                        **inner_inner,
                        Cardinality::Singular("TenantRecord".to_string()),
                        "§39.a §1 — nested wrap inner must be Singular"
                    );
                }
                other => panic!(
                    "§39.a §1 — nested wrap outer.inner must be Wrapped. \
                     Got: {other:?}"
                ),
            },
            other => panic!("§39.a §1 — got: {other:?}"),
        }
    }

    // ── §2 — non-FlowEnvelope declarations preserve v1.x semantics ──

    #[test]
    fn fase39a_list_without_envelope_still_plural() {
        // §Fase 39.a §2 — pre-Fase 39 declarations stay backwards-compat
        // at the cardinality level. `List<T>` is still Plural; the
        // axon-E039 mandate that promotes it to a compile error
        // when paired with `transport: json` lands in 39.e, not 39.a.
        let card = declared_cardinality("List<TenantRecord>");
        assert_eq!(
            card,
            Cardinality::Plural("TenantRecord".to_string()),
            "§39.a §2 — List<T> backwards-compat: still Plural"
        );
    }

    #[test]
    fn fase39a_stream_without_envelope_still_stream() {
        let card = declared_cardinality("Stream<Token>");
        assert_eq!(
            card,
            Cardinality::StreamCardinality("Token".to_string()),
            "§39.a §2 — Stream<T> backwards-compat: still StreamCardinality"
        );
    }

    #[test]
    fn fase39a_bare_type_still_singular() {
        let card = declared_cardinality("TenantRecord");
        assert_eq!(
            card,
            Cardinality::Singular("TenantRecord".to_string()),
            "§39.a §2 — bare type backwards-compat: still Singular"
        );
    }

    // ── §3 — Parser supports nested generics post-39.a ──

    #[test]
    fn fase39a_parser_accepts_flow_envelope_of_list() {
        // §Fase 39.a §3 — pre-39.a `parse_type_expr` only consumed
        // one Identifier inside `<...>`, so `FlowEnvelope<List<X>>`
        // failed to parse with a syntax error. Post-39.a the parser
        // recurses on the inner type expression and accepts
        // arbitrary depth. This test compiles end-to-end via the
        // existing check_errors harness (lexer + parser + checker).
        let src = r#"
            type TenantRecord { id: Text }
            axonstore tenants { backend: in_memory }
            axonendpoint get_all {
                method: GET
                path: "/api/tenants"
                output: FlowEnvelope<List<TenantRecord>>
                execute: GetAll
            }
            flow GetAll() -> Unit {
                retrieve tenants { where: "" as: result }
            }
        "#;
        let errs = check_errors(src);
        // The flow is intentionally Unit-tailed so the cardinality
        // gate doesn't emit T9XX/T9YY here — we're checking the
        // parser+type-checker accept the wrapping syntax end-to-end.
        let parse_errs: Vec<&TypeError> = errs
            .iter()
            .filter(|e| {
                e.message.contains("Expected")
                    || e.message.contains("Unexpected token")
                    || e.message.contains("syntax")
            })
            .collect();
        assert!(
            parse_errs.is_empty(),
            "§39.a §3 — FlowEnvelope<List<TenantRecord>> MUST parse cleanly. \
             Got parse-class errors: {parse_errs:#?}"
        );
    }

    // ── §4 — Gate unwraps Wrapped transparently ──

    #[test]
    fn fase39a_wrapped_plural_matches_plural_tail_silent() {
        // §Fase 39.a §4 — when declared is Wrapped(Plural(X)) and the
        // flow tail is Plural(X), the gate silently passes (the
        // canonical Kivi-shape after migration). axon-E039 in 39.e
        // will additionally check the wire-shape mandate (transport
        // json + Wrapped required), but at 39.a's cardinality layer
        // the truth-table agrees.
        let src = r#"
            type TenantRecord { id: Text }
            axonstore tenants { backend: in_memory }
            axonendpoint get_all {
                method: GET
                path: "/api/tenants"
                output: FlowEnvelope<List<TenantRecord>>
                execute: GetAll
            }
            flow GetAll() -> List<TenantRecord> {
                retrieve tenants { where: "" as: result }
            }
        "#;
        let errs = check_errors(src);
        // Filter out unrelated errors that may pre-exist on the
        // canonical adopter shape; we only care that NO T9XX/T9YY
        // fires on the wrap+tail agreement.
        let cardinality_errs: Vec<&TypeError> = errs
            .iter()
            .filter(|e| {
                e.message.contains("axon-T9XX")
                    || e.message.contains("axon-T9YY")
                    || e.message.contains("axon-W003")
            })
            .collect();
        assert!(
            cardinality_errs.is_empty(),
            "§39.a §4 — FlowEnvelope<List<T>> declared against Plural \
             tail MUST silent-pass the cardinality gate (the wrap \
             unwraps transparently). Got: {cardinality_errs:#?}"
        );
    }

    // ── §Fase 39.e — axon-E039 wire-shape mandate (D12 α) ────────

    #[test]
    fn fase39e_bare_singular_with_json_transport_emits_e039() {
        // §39.e §1 — the canonical kivi-shape: bare `output: T` on
        // default `transport: json` is now a COMPILE ERROR.
        let src = r#"
            type TenantRecord { id: Text }
            axonstore tenants { backend: in_memory }
            axonendpoint get_tenant {
                method: GET
                path: "/api/tenants/{id}"
                output: TenantRecord
                execute: GetTenant
            }
            flow GetTenant(id: Text) -> TenantRecord {
                step Echo { reason: "x" output: TenantRecord }
            }
        "#;
        let errs = check_errors(src);
        let e039: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-E039"))
            .collect();
        assert!(!e039.is_empty(), "§39.e §1 — bare T MUST fire E039. Got: {errs:#?}");
        assert!(
            e039[0].message.contains("`output: TenantRecord`"),
            "§39.e §1 — diagnostic MUST name the declared bare type. Got: {}",
            e039[0].message
        );
        assert!(
            e039[0].message.contains("FlowEnvelope<"),
            "§39.e §1 — diagnostic MUST suggest FlowEnvelope wrapping. \
             Got: {}",
            e039[0].message
        );
        assert!(
            e039[0].message.contains("transport: sse"),
            "§39.e §1 — diagnostic MUST mention sse migration alternative. \
             Got: {}",
            e039[0].message
        );
        assert!(
            e039[0].message.contains("D12"),
            "§39.e §1 — diagnostic MUST reference the D12 α \
             ratification anchor. Got: {}",
            e039[0].message
        );
    }

    #[test]
    fn fase39e_bare_list_with_json_transport_emits_e039() {
        // §39.e §2 — bare `List<T>` (the original adopter shape
        // that v1.40.0-v1.40.3 tried to bridge) is now a COMPILE
        // ERROR. The canonical answer is `FlowEnvelope<List<T>>`.
        let src = r#"
            type TenantRecord { id: Text }
            axonstore tenants { backend: in_memory }
            axonendpoint list_tenants {
                method: GET
                path: "/api/tenants"
                output: List<TenantRecord>
                execute: ListTenants
            }
            flow ListTenants() -> List<TenantRecord> {
                retrieve tenants { where: "1=1" as: result }
            }
        "#;
        let errs = check_errors(src);
        let e039: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-E039"))
            .collect();
        assert!(
            !e039.is_empty(),
            "§39.e §2 — bare `List<T>` MUST fire E039. Got: {errs:#?}"
        );
        assert!(
            e039[0].message.contains("`output: List<TenantRecord>`"),
            "§39.e §2 — diagnostic MUST name the declared bare List<T>. \
             Got: {}",
            e039[0].message
        );
        assert!(
            e039[0].message.contains("FlowEnvelope<List<"),
            "§39.e §2 — diagnostic MUST suggest FlowEnvelope<List<...>>. \
             Got: {}",
            e039[0].message
        );
    }

    #[test]
    fn fase39e_bare_stream_with_json_transport_emits_e039() {
        // §39.e §3 — bare `Stream<T>` with default `transport: json`
        // is a COMPILE ERROR. The diagnostic suggests both FlowEnvelope
        // wrapping AND (more idiomatically) sse transport migration.
        let src = r#"
            type Token { text: Text }
            axonendpoint stream_chat {
                method: POST
                path: "/api/stream"
                output: Stream<Token>
                execute: StreamChat
            }
            flow StreamChat() -> Stream<Token> {
                step Generate { ask: "stream" output: Stream<Token> }
            }
        "#;
        let errs = check_errors(src);
        // Note: implicit_transport inference (Fase 31) might set this
        // endpoint to "sse" implicitly because the flow produces Stream<T>.
        // In that case E039 would NOT fire — the wire is correctly sse.
        // The test accepts EITHER outcome since both are correct under
        // D2 + D9: bare Stream<T> with json fires E039; bare Stream<T>
        // with sse-inferred is acceptable.
        let e039_or_silent =
            errs.iter().filter(|e| e.message.contains("axon-E039")).count();
        // No T9YY should leak when the wire matches.
        let t9yy: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-T9YY"))
            .collect();
        assert!(
            e039_or_silent <= 1,
            "§39.e §3 — Stream<T> bare emits at most ONE diagnostic \
             (E039 or silent if implicit_transport=sse). Got count: \
             {e039_or_silent}, t9yy: {t9yy:#?}, all: {errs:#?}"
        );
    }

    #[test]
    fn fase39e_flow_envelope_singular_passes_clean() {
        // §39.e §4 — the canonical v2.0.0 happy path: `output:
        // FlowEnvelope<T>` on a flow producing a matching tail. No
        // E039, no T9XX, no T9YY.
        let src = r#"
            type WriteResult { ok: Bool }
            axonendpoint write_secret {
                method: POST
                path: "/api/secrets"
                output: FlowEnvelope<WriteResult>
                execute: WriteSecret
            }
            flow WriteSecret() -> WriteResult {
                step Echo { reason: "ok" output: WriteResult }
            }
        "#;
        let errs = check_errors(src);
        let wire_errs: Vec<&TypeError> = errs
            .iter()
            .filter(|e| {
                e.message.contains("axon-E039")
                    || e.message.contains("axon-T9XX")
                    || e.message.contains("axon-T9YY")
            })
            .collect();
        assert!(
            wire_errs.is_empty(),
            "§39.e §4 — FlowEnvelope<T> singular happy path MUST be \
             clean. Got: {wire_errs:#?}"
        );
    }

    #[test]
    fn fase39e_flow_envelope_list_passes_clean() {
        // §39.e §5 — the canonical migration target: `output:
        // FlowEnvelope<List<T>>` on a retrieve-tail flow. No errors.
        let src = r#"
            type TenantRecord { id: Text }
            axonstore tenants { backend: in_memory }
            axonendpoint list_tenants {
                method: GET
                path: "/api/tenants"
                output: FlowEnvelope<List<TenantRecord>>
                execute: ListTenants
            }
            flow ListTenants() -> List<TenantRecord> {
                retrieve tenants { where: "1=1" as: result }
            }
        "#;
        let errs = check_errors(src);
        let wire_errs: Vec<&TypeError> = errs
            .iter()
            .filter(|e| {
                e.message.contains("axon-E039")
                    || e.message.contains("axon-T9XX")
                    || e.message.contains("axon-T9YY")
            })
            .collect();
        assert!(
            wire_errs.is_empty(),
            "§39.e §5 — FlowEnvelope<List<T>> over a List<T>-tail flow \
             is the canonical migration. Got: {wire_errs:#?}"
        );
    }

    #[test]
    fn fase39e_flow_envelope_any_passes_clean() {
        // §39.e §6 — `output: Any` is the universal-accept escape
        // hatch (documented degraded surface). No E039 fires; T9XX/T9YY
        // also silent per Cardinality::Disagreed semantics.
        let src = r#"
            type X { f: Text }
            axonendpoint p {
                method: POST
                path: "/api/p"
                output: Any
                execute: F
            }
            flow F() -> X {
                step S { reason: "x" output: X }
            }
        "#;
        let errs = check_errors(src);
        let wire_errs: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-E039"))
            .collect();
        assert!(
            wire_errs.is_empty(),
            "§39.e §6 — `output: Any` is the universal-accept escape \
             hatch; E039 MUST NOT fire. Got: {wire_errs:#?}"
        );
    }

    #[test]
    fn fase39e_sse_transport_exempts_from_e039() {
        // §39.e §7 — explicit `transport: sse` exempts the endpoint
        // from the wrapping mandate (D9 — SSE has its own event
        // family). Bare `Stream<T>` declarations are valid on sse.
        let src = r#"
            type Token { text: Text }
            axonendpoint stream_chat {
                method: POST
                path: "/api/stream"
                transport: sse
                output: Stream<Token>
                execute: StreamChat
            }
            flow StreamChat() -> Stream<Token> {
                step Generate { ask: "stream" output: Stream<Token> }
            }
        "#;
        let errs = check_errors(src);
        let e039: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-E039"))
            .collect();
        assert!(
            e039.is_empty(),
            "§39.e §7 — explicit `transport: sse` MUST exempt the \
             endpoint from E039 (the SSE wire has its own event \
             family per D9). Got: {e039:#?}"
        );
    }

    #[test]
    fn fase39e_no_output_declared_skips_e039() {
        // §39.e §8 — D9 backwards-compat: empty `output:` declaration
        // (no `output:` line) skips both E039 and the cardinality
        // gate. Honest scope — adopters can opt out of strict
        // wire-shape contracts by simply not declaring.
        let src = r#"
            type TenantRecord { id: Text }
            axonstore tenants { backend: in_memory }
            axonendpoint loose {
                method: GET
                path: "/api/loose"
                execute: GetLoose
            }
            flow GetLoose() -> Unit {
                retrieve tenants { where: "1=1" as: result }
            }
        "#;
        let errs = check_errors(src);
        let wire_errs: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-E039"))
            .collect();
        assert!(
            wire_errs.is_empty(),
            "§39.e §8 — empty `output:` MUST skip E039 (D9 \
             backwards-compat). Got: {wire_errs:#?}"
        );
    }

    #[test]
    fn fase39e_unit_output_skips_e039() {
        // §39.e §9 — `output: Unit` is explicit "no wire body" —
        // exempt from the wrapping mandate.
        let src = r#"
            type X { f: Text }
            axonendpoint noop {
                method: POST
                path: "/api/noop"
                output: Unit
                execute: F
            }
            flow F() -> Unit {
                step S { reason: "x" output: Unit }
            }
        "#;
        let errs = check_errors(src);
        let e039: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-E039"))
            .collect();
        assert!(
            e039.is_empty(),
            "§39.e §9 — `output: Unit` MUST be exempt from E039. \
             Got: {e039:#?}"
        );
    }

    #[test]
    fn fase39e_nested_flow_envelope_passes_clean() {
        // §39.e §10 — defensive: degenerate nested
        // `FlowEnvelope<FlowEnvelope<T>>` is syntactically valid
        // (per 39.a parser nested-generic support) and is treated
        // as a FlowEnvelope wrap (E039 doesn't fire). It's
        // semantically weird (double wrap) but not a compile error.
        let src = r#"
            type X { f: Text }
            axonendpoint p {
                method: POST
                path: "/api/p"
                output: FlowEnvelope<FlowEnvelope<X>>
                execute: F
            }
            flow F() -> X {
                step S { reason: "x" output: X }
            }
        "#;
        let errs = check_errors(src);
        let e039: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-E039"))
            .collect();
        assert!(
            e039.is_empty(),
            "§39.e §10 — nested FlowEnvelope<FlowEnvelope<X>> is \
             semantically degenerate but NOT an E039 (any \
             `FlowEnvelope<...>` declaration passes the wrapping \
             mandate). Got: {e039:#?}"
        );
    }

    #[test]
    fn fase39a_wrapped_singular_vs_plural_tail_still_warns() {
        // §Fase 39.a §4 — when declared is Wrapped(Singular(X)) but
        // the flow tail is Plural, the gate still surfaces the
        // T9XX mismatch (unwrap shows the inner Singular vs Plural
        // shape disagreement). The hint message still references the
        // existing T9XX format; the axon-E039 promotion happens in 39.e.
        let src = r#"
            type TenantRecord { id: Text }
            axonstore tenants { backend: in_memory }
            axonendpoint get_one {
                method: GET
                path: "/api/tenants/{id}"
                output: FlowEnvelope<TenantRecord>
                execute: GetOne
            }
            flow GetOne(id: Text) -> TenantRecord {
                retrieve tenants { where: "id = ${id}" as: result }
            }
        "#;
        let errs = check_errors(src);
        let t9xx: Vec<&TypeError> = errs
            .iter()
            .filter(|e| e.message.contains("axon-T9XX"))
            .collect();
        assert!(
            !t9xx.is_empty(),
            "§39.a §4 — Wrapped(Singular) against Plural tail MUST \
             surface axon-T9XX through the unwrap (the wrap is \
             transparent to the cardinality contract). Errors: {errs:#?}"
        );
    }
}

#[cfg(test)]
mod fase41b_session_lowering_tests {
    //! §Fase 41.b — the Fase 4 `session` surface lowered into the §41.a
    //! session-type algebra, with duality decided by the connection law
    //! (regular-coinductive `is_dual_to`) rather than the old positional check.
    use super::*;

    fn step(op: &str, ty: &str) -> SessionStep {
        SessionStep { op: op.into(), message_type: ty.into(), ..Default::default() }
    }
    fn role(name: &str, steps: Vec<SessionStep>) -> SessionRole {
        SessionRole { name: name.into(), steps, ..Default::default() }
    }

    #[test]
    fn lowers_send_receive_end_to_session_type() {
        let r = role("client", vec![step("send", "T"), step("receive", "U"), step("end", "")]);
        assert_eq!(lower_session_role(&r), SessionType::send("T", SessionType::recv("U", SessionType::End)));
    }

    #[test]
    fn lowers_terminal_loop_to_mu_recursion() {
        // `[send T, loop]` ↦ `μX. !T.X` — the loop is a recursion point, not a token.
        let r = role("p", vec![step("send", "T"), step("loop", "")]);
        assert_eq!(lower_session_role(&r), SessionType::rec("X", SessionType::send("T", SessionType::var("X"))));
    }

    #[test]
    fn dual_recursive_roles_satisfy_the_connection_law() {
        // The case the old positional check could not reason about as recursion:
        // client loops sending T; server loops receiving T — genuinely dual.
        let client = lower_session_role(&role("c", vec![step("send", "T"), step("loop", "")]));
        let server = lower_session_role(&role("s", vec![step("receive", "T"), step("loop", "")]));
        assert!(client.is_dual_to(&server));
        assert!(server.is_dual_to(&client)); // symmetric up to involutivity
    }

    #[test]
    fn non_dual_roles_are_rejected() {
        let a = lower_session_role(&role("a", vec![step("send", "T"), step("end", "")]));
        // Same direction → not dual.
        let same = lower_session_role(&role("b", vec![step("send", "T"), step("end", "")]));
        assert!(!a.is_dual_to(&same));
        // Dual direction but mismatched payload → not dual.
        let wrong = lower_session_role(&role("c", vec![step("receive", "WRONG"), step("end", "")]));
        assert!(!a.is_dual_to(&wrong));
    }
}

#[cfg(test)]
mod fase41b_socket_tests {
    //! §Fase 41.b — the `socket` declaration: parse + check (protocol must
    //! reference a declared `session`; backpressure credit must be positive).
    use super::*;
    use crate::lexer::Lexer;
    use crate::parser::Parser;

    // A well-formed (dual) binary session the socket can reference.
    const SESSION: &str =
        "session Chat { client: [send Msg, receive Token, end] server: [receive Msg, send Token, end] }";

    fn parse_prog(src: &str) -> Program {
        let toks = Lexer::new(src, "<t>").tokenize().expect("lex");
        Parser::new(toks).parse().expect("parse")
    }
    fn errors(src: &str) -> Vec<TypeError> {
        TypeChecker::new(&parse_prog(src)).check()
    }

    #[test]
    fn socket_parses_into_ast_fields() {
        let prog = parse_prog(&format!(
            "{SESSION}\nsocket ChatWS {{ protocol: Chat, backpressure: credit(64), reconnect: cognitive_state, legal_basis: legitimate_interest }}"
        ));
        let sock = prog
            .declarations
            .iter()
            .find_map(|d| if let Declaration::Socket(s) = d { Some(s) } else { None })
            .expect("socket parsed");
        assert_eq!(sock.name, "ChatWS");
        assert_eq!(sock.protocol, "Chat");
        assert_eq!(sock.backpressure_credit, Some(64));
        assert!(sock.reconnect);
        assert_eq!(sock.legal_basis.as_deref(), Some("legitimate_interest"));
    }

    #[test]
    fn socket_referencing_a_declared_session_has_no_socket_error() {
        let errs = errors(&format!("{SESSION}\nsocket ChatWS {{ protocol: Chat, backpressure: credit(64) }}"));
        assert!(!errs.iter().any(|e| e.message.contains("Socket")), "unexpected socket error: {errs:?}");
    }

    #[test]
    fn socket_with_undeclared_protocol_is_rejected() {
        let errs = errors("socket ChatWS { protocol: DoesNotExist }");
        assert!(errs.iter().any(|e| e.message.contains("not a declared session")), "{errs:?}");
    }

    #[test]
    fn socket_with_zero_credit_window_is_rejected() {
        let errs = errors(&format!("{SESSION}\nsocket ChatWS {{ protocol: Chat, backpressure: credit(0) }}"));
        assert!(errs.iter().any(|e| e.message.contains("credit must be")), "{errs:?}");
    }
}

#[cfg(test)]
mod fase41b_choice_tests {
    //! §Fase 41.b — `select`/`branch` choice steps (⊕ / &): nested sub-protocols
    //! that lower into `SessionType::Select`/`Branch`, with duality decided by
    //! the connection law (`select` is dual to `branch` arm-for-arm).
    use super::*;
    use crate::lexer::Lexer;
    use crate::parser::Parser;
    use std::collections::BTreeMap;

    fn parse_prog(src: &str) -> Program {
        let toks = Lexer::new(src, "<t>").tokenize().expect("lex");
        Parser::new(toks).parse().expect("parse")
    }
    fn session<'a>(p: &'a Program, name: &str) -> &'a SessionDefinition {
        p.declarations
            .iter()
            .find_map(|d| match d {
                Declaration::Session(s) if s.name == name => Some(s),
                _ => None,
            })
            .expect("session declared")
    }
    fn role_of<'a>(s: &'a SessionDefinition, name: &str) -> &'a SessionRole {
        s.roles.iter().find(|r| r.name == name).expect("role")
    }

    // A session whose two roles disagree only by direction inside each arm:
    // client offers a choice (⊕), server accepts it (&) — genuinely dual.
    const CHOICE: &str = "session Negotiate {\n\
        client: [select { ask: [send Query, receive Answer, end], quit: [end] }]\n\
        server: [branch { ask: [receive Query, send Answer, end], quit: [end] }]\n\
    }";

    #[test]
    fn select_branch_steps_parse_with_nested_arms() {
        let p = parse_prog(CHOICE);
        let s = session(&p, "Negotiate");
        let client = role_of(s, "client");
        assert_eq!(client.steps.len(), 1);
        assert_eq!(client.steps[0].op, "select");
        let labels: Vec<_> = client.steps[0].branches.iter().map(|b| b.label.as_str()).collect();
        assert_eq!(labels, vec!["ask", "quit"]);
        // The `ask` arm carries its own ordered sub-protocol.
        let ask = &client.steps[0].branches[0];
        assert_eq!(ask.steps.iter().map(|s| s.op.as_str()).collect::<Vec<_>>(), vec!["send", "receive", "end"]);
    }

    #[test]
    fn select_lowers_to_session_type_select() {
        let p = parse_prog(CHOICE);
        let client = lower_session_role(role_of(session(&p, "Negotiate"), "client"));
        let mut arms = BTreeMap::new();
        arms.insert("ask".to_string(), SessionType::send("Query", SessionType::recv("Answer", SessionType::End)));
        arms.insert("quit".to_string(), SessionType::End);
        assert_eq!(client, SessionType::Select(arms));
    }

    #[test]
    fn select_is_dual_to_matching_branch() {
        // The connection law for choice: ⊕{ℓ:Sℓ} ⊥ &{ℓ:S̄ℓ} arm-for-arm.
        let p = parse_prog(CHOICE);
        let s = session(&p, "Negotiate");
        let client = lower_session_role(role_of(s, "client"));
        let server = lower_session_role(role_of(s, "server"));
        assert!(client.is_dual_to(&server));
        assert!(server.is_dual_to(&client));
    }

    #[test]
    fn choice_session_typechecks_clean() {
        let errs = TypeChecker::new(&parse_prog(CHOICE)).check();
        assert!(
            !errs.iter().any(|e| e.message.contains("not dual") || e.message.contains("Session")),
            "unexpected session error: {errs:?}"
        );
    }

    #[test]
    fn choice_with_duplicate_labels_is_rejected() {
        let src = "session Bad {\n\
            client: [select { ask: [end], ask: [end] }]\n\
            server: [branch { ask: [end] }]\n\
        }";
        let errs = TypeChecker::new(&parse_prog(src)).check();
        assert!(errs.iter().any(|e| e.message.contains("duplicate") || e.message.contains("label")), "{errs:?}");
    }

    #[test]
    fn empty_choice_is_rejected() {
        let src = "session Bad {\n\
            client: [select {  }]\n\
            server: [branch {  }]\n\
        }";
        let errs = TypeChecker::new(&parse_prog(src)).check();
        assert!(errs.iter().any(|e| e.message.contains("at least one") || e.message.contains("branch")), "{errs:?}");
    }
}

#[cfg(test)]
mod fase41c_credit_tests {
    //! §Fase 41.c — the Presburger discharge wired into `check_socket`.
    //! The bare session + dual is duality-checked (41.a/b); when a `socket`
    //! binds `backpressure: credit(k)`, both roles are lowered, stamped with
    //! `k`, and run through [`SessionType::credit_analyse`] — surfacing
    //! send-at-zero, burst overflow and loop unsustainability as type errors.
    use super::*;
    use crate::lexer::Lexer;
    use crate::parser::Parser;

    fn parse_prog(src: &str) -> Program {
        let toks = Lexer::new(src, "<t>").tokenize().expect("lex");
        Parser::new(toks).parse().expect("parse")
    }
    fn errors(src: &str) -> Vec<TypeError> {
        TypeChecker::new(&parse_prog(src)).check()
    }
    fn has(errs: &[TypeError], needle: &str) -> bool {
        errs.iter().any(|e| e.message.contains(needle))
    }

    // A 2-send burst protocol — the client wants to put two messages on the
    // wire back-to-back; under `credit(1)` the second send hits n=0.
    const BURST_SESSION: &str =
        "session Burst { client: [send A, send B, end] server: [receive A, receive B, end] }";

    #[test]
    fn credit_window_within_budget_is_accepted() {
        let errs = errors(&format!(
            "{BURST_SESSION}\nsocket S {{ protocol: Burst, backpressure: credit(2) }}"
        ));
        assert!(!has(&errs, "credit-refined"), "unexpected credit error: {errs:?}");
        assert!(!has(&errs, "violates"), "{errs:?}");
    }

    #[test]
    fn burst_overflow_is_rejected() {
        let errs = errors(&format!(
            "{BURST_SESSION}\nsocket S {{ protocol: Burst, backpressure: credit(1) }}"
        ));
        // The client role demands a 2-send burst; budget=1 cannot absorb it.
        assert!(has(&errs, "credit-window overflow"), "expected burst overflow, got: {errs:?}");
        assert!(has(&errs, "send-burst of 2"), "expected burst=2 detail, got: {errs:?}");
        assert!(has(&errs, "credit(1)"), "expected budget=1 detail, got: {errs:?}");
        // The dual `server` role is purely receives → no error attributed to it.
        let server_errs: Vec<_> = errs
            .iter()
            .filter(|e| e.message.contains("role 'server'") && e.message.contains("credit-refined"))
            .collect();
        assert!(server_errs.is_empty(), "server role should be clean: {server_errs:?}");
    }

    #[test]
    fn unsustainable_loop_is_rejected_at_any_budget() {
        // rec X. !A.!B.?Ack.X — Δ = 2-1 = 1 > 0 per recurring iteration.
        // No finite k is sufficient; even credit(100) is rejected statically.
        let src = "session Drain {\n\
            client: [send A, send B, receive Ack, loop]\n\
            server: [receive A, receive B, send Ack, loop]\n\
        }\nsocket S { protocol: Drain, backpressure: credit(100) }";
        let errs = errors(src);
        assert!(has(&errs, "unsustainable"), "expected loop unsustainability, got: {errs:?}");
        assert!(has(&errs, "2 - 1 > 0"), "expected Δ detail, got: {errs:?}");
    }

    #[test]
    fn balanced_loop_is_accepted_at_minimal_budget() {
        // rec X. !A.?Ack.X — Δ = 1-1 = 0 ⇒ sustainable; budget=1 is enough.
        let src = "session Pingpong {\n\
            client: [send A, receive Ack, loop]\n\
            server: [receive A, send Ack, loop]\n\
        }\nsocket S { protocol: Pingpong, backpressure: credit(1) }";
        let errs = errors(src);
        assert!(!has(&errs, "credit-refined"), "{errs:?}");
        assert!(!has(&errs, "unsustainable"), "{errs:?}");
    }

    #[test]
    fn choice_arms_are_each_checked_under_budget() {
        // The `ask` arm needs a 2-send burst; the `quit` arm terminates.
        let src = "session Choice {\n\
            client: [select { ask: [send Q, send R, end], quit: [end] }]\n\
            server: [branch { ask: [receive Q, receive R, end], quit: [end] }]\n\
        }\nsocket S { protocol: Choice, backpressure: credit(1) }";
        let errs = errors(src);
        assert!(has(&errs, "credit-window overflow"), "ask arm must overflow: {errs:?}");
        // Same protocol under sufficient credit is clean.
        let src_ok = src.replace("credit(1)", "credit(2)");
        assert!(!has(&errors(&src_ok), "credit-refined"), "credit(2) should fit");
    }

    #[test]
    fn no_backpressure_annotation_skips_credit_analysis() {
        // Omitting `backpressure` leaves the protocol in the unbounded
        // fragment (`!∞A.S`); the burst session typechecks clean.
        let errs = errors(&format!(
            "{BURST_SESSION}\nsocket S {{ protocol: Burst }}"
        ));
        assert!(!has(&errs, "credit-refined"), "{errs:?}");
        assert!(!has(&errs, "violates"), "{errs:?}");
    }

    #[test]
    fn zero_credit_still_caught_as_a_separate_diagnostic() {
        // `credit(0)` was already rejected by 41.b's `≥ 1` check; 41.c does
        // not silently swallow it — the earlier diagnostic still fires and
        // the credit-analysis is skipped (no budget to discharge against).
        let errs = errors(&format!(
            "{BURST_SESSION}\nsocket S {{ protocol: Burst, backpressure: credit(0) }}"
        ));
        assert!(has(&errs, "credit must be"), "41.b ≥ 1 check still fires: {errs:?}");
        assert!(!has(&errs, "credit-window overflow"), "no overflow-walking on bad budget: {errs:?}");
    }
}