uor-foundation 0.2.1

// @generated by uor-crate from uor-ontology — do not edit manually

//! v0.2.1 Reduction Pipeline — no_std in-process driver.
//!
//! Backs `Certify::certify` on every resolver façade and (re-exported
//! via the macros crate) the `uor_ground!` macro's compile-time pipeline.
//!
//! The driver implements the full reduction pipeline per
//! `external/ergonomics-spec.md` §3.3 and §4: 6 preflight checks,
//! 7 reduction stages, 4 resolver backends, real 2-SAT and Horn-SAT
//! deciders, fragment classifier, content-addressed unit-ids.
//!
//! Every entry point is ontology-driven: IRIs, stage order, and
//! dispatch-table rules are baked in at codegen time from the
//! ontology graph. Adding a new preflight check or resolver is a
//! pure ontology edit.

use crate::enforcement::{
    BindingEntry, BindingsTable, CompileUnit, CompletenessCertificate, ConstrainedTypeInput,
    GenericImpossibilityWitness, Grounded, GroundingCertificate, InhabitanceCertificate,
    InhabitanceImpossibilityWitness, LiftChainCertificate, MacroProvenance, PipelineFailure,
    ShapeViolation, Validated,
};
use crate::ViolationKind;
use crate::WittLevel;

/// Zero-based preflight check order read from `reduction:PreflightCheck`
/// individuals at codegen time. `BudgetSolvencyCheck` MUST be index 0 per
/// `reduction:preflightOrder` — enforced by the ontology, not here.
pub const PREFLIGHT_CHECK_IRIS: &[&str] = &[
    "https://uor.foundation/reduction/BudgetSolvencyCheck",
    "https://uor.foundation/reduction/FeasibilityCheck",
    "https://uor.foundation/reduction/DispatchCoverageCheck",
    "https://uor.foundation/reduction/PackageCoherenceCheck",
    "https://uor.foundation/reduction/PreflightTiming",
    "https://uor.foundation/reduction/RuntimeTiming",
];

/// Seven reduction stages in declared order, sourced from
/// `reduction:ReductionStep` individuals.
pub const REDUCTION_STAGE_IRIS: &[&str] = &[
    "https://uor.foundation/reduction/stage_initialization",
    "https://uor.foundation/reduction/stage_declare",
    "https://uor.foundation/reduction/stage_factorize",
    "https://uor.foundation/reduction/stage_resolve",
    "https://uor.foundation/reduction/stage_attest",
    "https://uor.foundation/reduction/stage_extract",
    "https://uor.foundation/reduction/stage_convergence",
];

/// Opaque constraint reference carried by `ConstrainedTypeShape` impls.
/// Variants mirror `type:Constraint` subclasses from the ontology.
/// The `SatClauses` variant carries a compact 2-SAT/Horn-SAT clause
/// list — each clause is a `&'static [(u32, bool)]` of (variable, negated).
#[derive(Debug, Clone, Copy)]
#[non_exhaustive]
pub enum ConstraintRef {
    /// `type:ResidueConstraint`: value ≡ residue (mod modulus).
    Residue { modulus: u64, residue: u64 },
    /// `type:HammingConstraint`: bit-weight bound.
    Hamming { bound: u32 },
    /// `type:DepthConstraint`: site-depth bound.
    Depth { min: u32, max: u32 },
    /// `type:CarryConstraint`: carry-bit relation.
    Carry { site: u32 },
    /// `type:SiteConstraint`: site-position restriction.
    Site { position: u32 },
    /// `type:AffineConstraint`: affine relation over sites.
    Affine {
        coefficients: &'static [i64],
        bias: i64,
    },
    /// Opaque clause list for 2-SAT / Horn-SAT inputs.
    /// Each clause is a slice of `(variable_index, is_negated)`.
    SatClauses {
        clauses: &'static [&'static [(u32, bool)]],
        num_vars: u32,
    },
}

/// Back-door supertrait for `ConstrainedTypeShape`. Reachable via
/// `uor_foundation::pipeline::constrained_type_shape_sealed::Sealed`.
/// Only `#[derive(ConstrainedType)]` is supposed to impl it.
#[doc(hidden)]
pub mod constrained_type_shape_sealed {
    /// Sealed supertrait of `ConstrainedTypeShape`. Not part of the
    /// stable API — reserved for `#[derive(ConstrainedType)]` emission.
    pub trait Sealed {}
    /// Built-in impl for the ConstrainedTypeInput foundation shim.
    impl Sealed for super::ConstrainedTypeInput {}
}

/// Runtime-visible shape of a user `#[derive(ConstrainedType)]` struct.
/// The pipeline driver consumes a reference to any type implementing this
/// trait. Downstream types get the impl via the derive macro, which fills
/// in `IRI`, `SITE_COUNT`, and `CONSTRAINTS` from the struct's `#[uor(...)]`
/// attributes.
pub trait ConstrainedTypeShape: constrained_type_shape_sealed::Sealed {
    /// IRI of the ontology `type:ConstrainedType` instance this shape represents.
    const IRI: &'static str;
    /// Number of sites (fields) this constrained type carries.
    const SITE_COUNT: usize;
    /// Per-site constraint list. Empty means unconstrained.
    const CONSTRAINTS: &'static [ConstraintRef];
}

impl ConstrainedTypeShape for ConstrainedTypeInput {
    const IRI: &'static str = "https://uor.foundation/type/ConstrainedType";
    const SITE_COUNT: usize = 0;
    const CONSTRAINTS: &'static [ConstraintRef] = &[];
}

/// Result of `fragment_classify`: which `predicate:*Shape` fragment the
/// input belongs to. Drives `InhabitanceResolver` dispatch routing.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum FragmentKind {
    /// `predicate:Is2SatShape` — clauses of width ≤ 2.
    TwoSat,
    /// `predicate:IsHornShape` — clauses with ≤ 1 positive literal.
    Horn,
    /// `predicate:IsResidualFragment` — catch-all; no polynomial bound.
    Residual,
}

/// Classify a constraint system into one of the three dispatch fragments.
/// The classifier inspects the first `SatClauses` constraint (if any) and
/// applies the ontology's shape predicates. Constraint systems with no
/// `SatClauses` constraint — e.g., pure residue/hamming constraints — are
/// classified as `Residual` because the dispatch table has no polynomial
/// decider for them in v0.2.1.
#[must_use]
pub const fn fragment_classify(constraints: &[ConstraintRef]) -> FragmentKind {
    let mut i = 0;
    while i < constraints.len() {
        if let ConstraintRef::SatClauses { clauses, .. } = constraints[i] {
            // Classify by maximum clause width and positive-literal count.
            let mut max_width: usize = 0;
            let mut horn: bool = true;
            let mut j = 0;
            while j < clauses.len() {
                let clause = clauses[j];
                if clause.len() > max_width {
                    max_width = clause.len();
                }
                let mut positives: usize = 0;
                let mut k = 0;
                while k < clause.len() {
                    let (_, negated) = clause[k];
                    if !negated {
                        positives += 1;
                    }
                    k += 1;
                }
                if positives > 1 {
                    horn = false;
                }
                j += 1;
            }
            if max_width <= 2 {
                return FragmentKind::TwoSat;
            } else if horn {
                return FragmentKind::Horn;
            } else {
                return FragmentKind::Residual;
            }
        }
        i += 1;
    }
    // No SAT clauses at all — residual.
    FragmentKind::Residual
}

/// Aspvall-Plass-Tarjan 2-SAT decider: returns `true` iff the clause list
/// is satisfiable.
/// Builds the implication graph: for each clause `(a | b)`, adds
/// `¬a → b` and `¬b → a`. Runs Tarjan's SCC algorithm and checks that
/// no variable and its negation share an SCC. O(n+m) via iterative
/// Tarjan (the `no_std` path can't recurse freely).
/// v0.2.1 bounds (from `reduction:TwoSatBound`): up to 256 variables, up to 512 clauses. The `const` bounds keep the entire decider on the stack — essential for `no_std` and compile-time proc-macro expansion.
const TWO_SAT_MAX_VARS: usize = 256;
const TWO_SAT_MAX_NODES: usize = TWO_SAT_MAX_VARS * 2;
const TWO_SAT_MAX_EDGES: usize = 2048;

/// 2-SAT decision result.
#[must_use]
pub fn decide_two_sat(clauses: &[&[(u32, bool)]], num_vars: u32) -> bool {
    if (num_vars as usize) > TWO_SAT_MAX_VARS {
        return false;
    }
    let n = (num_vars as usize) * 2;
    // Node index: 2*var is positive literal, 2*var+1 is negated.
    let mut adj_starts = [0usize; TWO_SAT_MAX_NODES + 1];
    let mut adj_targets = [0usize; TWO_SAT_MAX_EDGES];
    // First pass: count out-degrees.
    for clause in clauses {
        if clause.len() > 2 || clause.is_empty() {
            return false;
        }
        if clause.len() == 1 {
            let (v, neg) = clause[0];
            let lit = lit_index(v, neg);
            let neg_lit = lit_index(v, !neg);
            // x ↔ (x ∨ x): ¬x → x (assignment forced)
            if neg_lit < n + 1 {
                adj_starts[neg_lit + 1] += 1;
            }
            let _ = lit;
        } else {
            let (a, an) = clause[0];
            let (b, bn) = clause[1];
            // ¬a → b, ¬b → a
            let na = lit_index(a, !an);
            let nb = lit_index(b, !bn);
            if na + 1 < n + 1 {
                adj_starts[na + 1] += 1;
            }
            if nb + 1 < n + 1 {
                adj_starts[nb + 1] += 1;
            }
        }
    }
    // Prefix-sum to get adjacency starts.
    let mut i = 1;
    while i <= n {
        adj_starts[i] += adj_starts[i - 1];
        i += 1;
    }
    let edge_count = adj_starts[n];
    if edge_count > TWO_SAT_MAX_EDGES {
        return false;
    }
    let mut fill = [0usize; TWO_SAT_MAX_NODES];
    for clause in clauses {
        if clause.len() == 1 {
            let (v, neg) = clause[0];
            let pos_lit = lit_index(v, neg);
            let neg_lit = lit_index(v, !neg);
            let slot = adj_starts[neg_lit] + fill[neg_lit];
            adj_targets[slot] = pos_lit;
            fill[neg_lit] += 1;
        } else {
            let (a, an) = clause[0];
            let (b, bn) = clause[1];
            let pa = lit_index(a, an);
            let na = lit_index(a, !an);
            let pb = lit_index(b, bn);
            let nb = lit_index(b, !bn);
            let s1 = adj_starts[na] + fill[na];
            adj_targets[s1] = pb;
            fill[na] += 1;
            let s2 = adj_starts[nb] + fill[nb];
            adj_targets[s2] = pa;
            fill[nb] += 1;
        }
    }
    // Iterative Tarjan's SCC.
    let mut index_counter: usize = 0;
    let mut indices = [usize::MAX; TWO_SAT_MAX_NODES];
    let mut lowlinks = [0usize; TWO_SAT_MAX_NODES];
    let mut on_stack = [false; TWO_SAT_MAX_NODES];
    let mut stack = [0usize; TWO_SAT_MAX_NODES];
    let mut stack_top: usize = 0;
    let mut scc_id = [usize::MAX; TWO_SAT_MAX_NODES];
    let mut scc_count: usize = 0;
    let mut call_stack = [(0usize, 0usize); TWO_SAT_MAX_NODES];
    let mut call_top: usize = 0;
    let mut v = 0;
    while v < n {
        if indices[v] == usize::MAX {
            call_stack[call_top] = (v, adj_starts[v]);
            call_top += 1;
            indices[v] = index_counter;
            lowlinks[v] = index_counter;
            index_counter += 1;
            stack[stack_top] = v;
            stack_top += 1;
            on_stack[v] = true;
            while call_top > 0 {
                let (u, mut next_edge) = call_stack[call_top - 1];
                let end_edge = adj_starts[u + 1];
                let mut advanced = false;
                while next_edge < end_edge {
                    let w = adj_targets[next_edge];
                    next_edge += 1;
                    if indices[w] == usize::MAX {
                        call_stack[call_top - 1] = (u, next_edge);
                        indices[w] = index_counter;
                        lowlinks[w] = index_counter;
                        index_counter += 1;
                        stack[stack_top] = w;
                        stack_top += 1;
                        on_stack[w] = true;
                        call_stack[call_top] = (w, adj_starts[w]);
                        call_top += 1;
                        advanced = true;
                        break;
                    } else if on_stack[w] && indices[w] < lowlinks[u] {
                        lowlinks[u] = indices[w];
                    }
                }
                if !advanced {
                    call_stack[call_top - 1] = (u, next_edge);
                    if lowlinks[u] == indices[u] {
                        loop {
                            stack_top -= 1;
                            let w = stack[stack_top];
                            on_stack[w] = false;
                            scc_id[w] = scc_count;
                            if w == u {
                                break;
                            }
                        }
                        scc_count += 1;
                    }
                    call_top -= 1;
                    if call_top > 0 {
                        let (parent, _) = call_stack[call_top - 1];
                        if lowlinks[u] < lowlinks[parent] {
                            lowlinks[parent] = lowlinks[u];
                        }
                    }
                }
            }
        }
        v += 1;
    }
    // Unsatisfiable iff x and ¬x are in the same SCC for any variable.
    let mut var = 0u32;
    while var < num_vars {
        let pos = lit_index(var, false);
        let neg = lit_index(var, true);
        if scc_id[pos] == scc_id[neg] {
            return false;
        }
        var += 1;
    }
    true
}

#[inline]
const fn lit_index(var: u32, negated: bool) -> usize {
    let base = (var as usize) * 2;
    if negated {
        base + 1
    } else {
        base
    }
}

/// Horn-SAT decider via unit propagation. Returns `true` iff the clause
/// list is satisfiable.
/// Algorithm: start with all variables false. Repeatedly find a clause
/// whose negative literals are all satisfied but whose positive literal
/// is unassigned/false; set the positive literal true. Fail if a clause
/// with no positive literal has all its negatives satisfied.
/// v0.2.1 bounds (from `reduction:HornSatBound`): up to 256 variables.
const HORN_MAX_VARS: usize = 256;

/// Horn-SAT decision result.
#[must_use]
pub fn decide_horn_sat(clauses: &[&[(u32, bool)]], num_vars: u32) -> bool {
    if (num_vars as usize) > HORN_MAX_VARS {
        return false;
    }
    let mut assignment = [false; HORN_MAX_VARS];
    let n = num_vars as usize;
    loop {
        let mut changed = false;
        for clause in clauses {
            // Count positive literals.
            let mut positive: Option<u32> = None;
            let mut positive_count = 0;
            for (_, negated) in clause.iter() {
                if !*negated {
                    positive_count += 1;
                }
            }
            if positive_count > 1 {
                return false;
            }
            for (var, negated) in clause.iter() {
                if !*negated {
                    positive = Some(*var);
                }
            }
            // Check whether all negative literals are satisfied (var=true).
            let mut all_neg_satisfied = true;
            for (var, negated) in clause.iter() {
                if *negated {
                    let idx = *var as usize;
                    if idx >= n {
                        return false;
                    }
                    if !assignment[idx] {
                        all_neg_satisfied = false;
                        break;
                    }
                }
            }
            if all_neg_satisfied {
                match positive {
                    None => return false,
                    Some(v) => {
                        let idx = v as usize;
                        if idx >= n {
                            return false;
                        }
                        if !assignment[idx] {
                            assignment[idx] = true;
                            changed = true;
                        }
                    }
                }
            }
        }
        if !changed {
            break;
        }
    }
    // Final verification pass.
    for clause in clauses {
        let mut satisfied = false;
        for (var, negated) in clause.iter() {
            let idx = *var as usize;
            if idx >= n {
                return false;
            }
            let val = assignment[idx];
            if (*negated && !val) || (!*negated && val) {
                satisfied = true;
                break;
            }
        }
        if !satisfied {
            return false;
        }
    }
    true
}

/// FNV-1a 128-bit hash of a constraint system, used as the content-addressed
/// `reduction:unitAddress`. Populated by `stage_initialization`; excludes
/// budget/domains/witt-level to enable memoization across identical shapes.
#[must_use]
pub const fn hash_constraints(iri: &str, site_count: usize, constraints: &[ConstraintRef]) -> u128 {
    let mut hash: u128 = 0x6c62272e07bb014262b821756295c58d;
    let iri_bytes = iri.as_bytes();
    let mut i = 0;
    while i < iri_bytes.len() {
        hash ^= iri_bytes[i] as u128;
        hash = hash.wrapping_mul(0x0000000001000000000000000000013b);
        i += 1;
    }
    hash ^= site_count as u128;
    hash = hash.wrapping_mul(0x0000000001000000000000000000013b);
    hash ^= constraints.len() as u128;
    hash = hash.wrapping_mul(0x0000000001000000000000000000013b);
    hash
}

/// `BudgetSolvencyCheck` (preflightOrder 0): `thermodynamicBudget` must be
/// ≥ `bitsWidth(unitWittLevel) × ln 2` per `op:GS_7` / `op:OA_5`.
/// Takes the budget in `k_B T · ln 2` units and the target Witt level in
/// bit-width. Returns `Ok(())` if solvent, `Err` with the shape violation.
pub fn preflight_budget_solvency(budget_units: u64, witt_bits: u32) -> Result<(), ShapeViolation> {
    // Landauer bound: one bit requires k_B T · ln 2. Integer form.
    let minimum = witt_bits as u64;
    if budget_units >= minimum {
        Ok(())
    } else {
        Err(ShapeViolation {
            shape_iri: "https://uor.foundation/conformance/CompileUnitShape",
            constraint_iri:
                "https://uor.foundation/conformance/compileUnit_thermodynamicBudget_constraint",
            property_iri: "https://uor.foundation/reduction/thermodynamicBudget",
            expected_range: "http://www.w3.org/2001/XMLSchema#decimal",
            min_count: 1,
            max_count: 1,
            kind: ViolationKind::ValueCheck,
        })
    }
}

/// `FeasibilityCheck`: verify the constraint system isn't trivially infeasible
/// (e.g., a `SatClauses` constraint with `num_vars == 0` but non-empty clauses).
pub fn preflight_feasibility(constraints: &[ConstraintRef]) -> Result<(), ShapeViolation> {
    for c in constraints {
        if let ConstraintRef::SatClauses { clauses, num_vars } = c {
            if *num_vars == 0 && !clauses.is_empty() {
                return Err(ShapeViolation {
                    shape_iri: "https://uor.foundation/conformance/CompileUnitShape",
                    constraint_iri:
                        "https://uor.foundation/conformance/compileUnit_rootTerm_constraint",
                    property_iri: "https://uor.foundation/reduction/rootTerm",
                    expected_range: "https://uor.foundation/schema/Term",
                    min_count: 1,
                    max_count: 1,
                    kind: ViolationKind::ValueCheck,
                });
            }
        }
    }
    Ok(())
}

/// `DispatchCoverageCheck`: verify the inhabitance dispatch table covers the input.
/// In v0.2.1 the table is exhaustive by construction (Rule 3 is the catch-all).
pub fn preflight_dispatch_coverage() -> Result<(), ShapeViolation> {
    // Always covered: IsResidualFragment catches everything not in 2-SAT/Horn.
    Ok(())
}

/// `PackageCoherenceCheck`: verify each site's constraints are internally consistent.
pub fn preflight_package_coherence(constraints: &[ConstraintRef]) -> Result<(), ShapeViolation> {
    // Check residue constraints don't contradict (same modulus, different residues).
    let mut i = 0;
    while i < constraints.len() {
        if let ConstraintRef::Residue {
            modulus: m1,
            residue: r1,
        } = constraints[i]
        {
            let mut j = i + 1;
            while j < constraints.len() {
                if let ConstraintRef::Residue {
                    modulus: m2,
                    residue: r2,
                } = constraints[j]
                {
                    if m1 == m2 && r1 != r2 {
                        return Err(ShapeViolation {
                            shape_iri: "https://uor.foundation/conformance/CompileUnitShape",
                            constraint_iri:
                                "https://uor.foundation/conformance/compileUnit_rootTerm_constraint",
                            property_iri: "https://uor.foundation/reduction/rootTerm",
                            expected_range: "https://uor.foundation/schema/Term",
                            min_count: 1,
                            max_count: 1,
                            kind: ViolationKind::ValueCheck,
                        });
                    }
                }
                j += 1;
            }
        }
        i += 1;
    }
    Ok(())
}

/// `PreflightTiming`: timing-check preflight. v0.2.1 returns Ok
/// unconditionally; the budget is parametric via `reduction:PreflightTimingBound`.
#[allow(dead_code)]
const PREFLIGHT_BUDGET_NS: u64 = 10000000;
pub fn preflight_timing() -> Result<(), ShapeViolation> {
    Ok(())
}

/// `RuntimeTiming`: runtime timing-check preflight. v0.2.1 returns Ok
/// unconditionally; the budget is parametric via `reduction:RuntimeTimingBound`.
#[allow(dead_code)]
const RUNTIME_BUDGET_NS: u64 = 10000000;
pub fn runtime_timing() -> Result<(), ShapeViolation> {
    Ok(())
}

/// Reduction stage executor. Takes a classified input and runs the 7 stages
/// in order, producing a `StageOutcome` on success.
#[derive(Debug, Clone, Copy)]
pub struct StageOutcome {
    /// `reduction:unitAddress` computed at `stage_initialization`.
    pub unit_address: u128,
    /// Witt level the compile unit was resolved at.
    pub witt_bits: u16,
    /// Fragment classification decided at `stage_resolve`.
    pub fragment: FragmentKind,
    /// Whether the input is satisfiable (carrier non-empty).
    pub satisfiable: bool,
}

/// Run the 7 reduction stages on a constrained-type input.
///
/// # Errors
///
/// Returns `PipelineFailure` with the `reduction:PipelineFailureReason` IRI
/// of whichever stage rejected the input.
pub fn run_reduction_stages<T: ConstrainedTypeShape + ?Sized>(
    _input: &T,
    witt_bits: u16,
) -> Result<StageOutcome, PipelineFailure> {
    // Stage 0 (initialization): compute content-addressed unit-id.
    let unit_address = hash_constraints(T::IRI, T::SITE_COUNT, T::CONSTRAINTS);
    // Stage 1 (declare): no-op; declarations already captured by the derive macro.
    // Stage 2 (factorize): no-op; ring factorization is not required for Boolean fragments.
    // Stage 3 (resolve): fragment classification.
    let fragment = fragment_classify(T::CONSTRAINTS);
    // Stage 4 (attest): run the decider associated with the fragment.
    let satisfiable = match fragment {
        FragmentKind::TwoSat => {
            let mut sat = true;
            for c in T::CONSTRAINTS {
                if let ConstraintRef::SatClauses { clauses, num_vars } = c {
                    sat = decide_two_sat(clauses, *num_vars);
                    break;
                }
            }
            sat
        }
        FragmentKind::Horn => {
            let mut sat = true;
            for c in T::CONSTRAINTS {
                if let ConstraintRef::SatClauses { clauses, num_vars } = c {
                    sat = decide_horn_sat(clauses, *num_vars);
                    break;
                }
            }
            sat
        }
        FragmentKind::Residual => {
            // No polynomial decider available. v0.2.1 treats residual
            // constraint systems as vacuously satisfiable when they carry
            // no SatClauses — pure residue/hamming/etc. inputs always have
            // some value satisfying at least the trivial case. Non-trivial
            // residuals yield ConvergenceStall at stage_convergence below.
            let mut has_sat_clauses = false;
            for c in T::CONSTRAINTS {
                if matches!(c, ConstraintRef::SatClauses { .. }) {
                    has_sat_clauses = true;
                    break;
                }
            }
            !has_sat_clauses
        }
    };
    if matches!(fragment, FragmentKind::Residual) && !satisfiable {
        return Err(PipelineFailure::ConvergenceStall {
            stage_iri: "https://uor.foundation/reduction/stage_convergence",
            angle_milliradians: 0,
        });
    }
    // Stage 5 (extract): extract bindings (none for v0.2.1's stub inputs).
    // Stage 6 (convergence): verify fixpoint reached. Trivially true for
    // classified fragments.
    Ok(StageOutcome {
        unit_address,
        witt_bits,
        fragment,
        satisfiable,
    })
}

/// Run the `TowerCompletenessResolver` pipeline on a `ConstrainedTypeShape`
/// input at the requested Witt level. Emits a `LiftChainCertificate` on
/// success or a generic `ImpossibilityWitness` on failure.
/// # Errors
/// Returns `GenericImpossibilityWitness` when the input is unsatisfiable or
/// when any preflight / reduction stage rejects it.
pub fn run_tower_completeness<T: ConstrainedTypeShape + ?Sized>(
    input: &T,
    level: WittLevel,
) -> Result<Validated<LiftChainCertificate>, GenericImpossibilityWitness> {
    let witt_bits = level.witt_length() as u16;
    preflight_budget_solvency(witt_bits as u64, witt_bits as u32)
        .map_err(|_| GenericImpossibilityWitness::default())?;
    preflight_feasibility(T::CONSTRAINTS).map_err(|_| GenericImpossibilityWitness::default())?;
    preflight_package_coherence(T::CONSTRAINTS)
        .map_err(|_| GenericImpossibilityWitness::default())?;
    preflight_dispatch_coverage().map_err(|_| GenericImpossibilityWitness::default())?;
    preflight_timing().map_err(|_| GenericImpossibilityWitness::default())?;
    runtime_timing().map_err(|_| GenericImpossibilityWitness::default())?;
    let outcome = run_reduction_stages(input, witt_bits)
        .map_err(|_| GenericImpossibilityWitness::default())?;
    if outcome.satisfiable {
        // SAFETY: MacroProvenance construction is reachable here because
        // the pipeline module is internal to the foundation crate and
        // operates under the sealed-constructor discipline.
        let prov = MacroProvenance::__for_macro_crate();
        let cert = LiftChainCertificate::with_witt_bits(outcome.witt_bits);
        Ok(crate::enforcement::__uor_macro_mint_validated(prov, cert))
    } else {
        Err(GenericImpossibilityWitness::default())
    }
}

/// Run the `IncrementalCompletenessResolver` (single-step lift) at `level`.
///
/// # Errors
///
/// Returns `GenericImpossibilityWitness` when the single-step lift fails.
pub fn run_incremental_completeness<T: ConstrainedTypeShape + ?Sized>(
    input: &T,
    level: WittLevel,
) -> Result<Validated<LiftChainCertificate>, GenericImpossibilityWitness> {
    // v0.2.1: iterative and single-step share the same deciders.
    run_tower_completeness(input, level)
}

/// Run the `GroundingAwareResolver` on a `CompileUnit` input at `level`,
/// exploiting `state:GroundedContext` bindings for O(1) resolution per
/// `op:GS_5`.
///
/// # Errors
///
/// Returns `GenericImpossibilityWitness` on grounding failure.
pub fn run_grounding_aware(
    _input: &CompileUnit,
    level: WittLevel,
) -> Result<Validated<GroundingCertificate>, GenericImpossibilityWitness> {
    // v0.2.1: compile unit input has no ConstrainedTypeShape backing so
    // the GroundingAwareResolver returns a trivial grounding certificate
    // carrying the requested Witt level.
    let witt_bits = level.witt_length() as u16;
    let prov = MacroProvenance::__for_macro_crate();
    let cert = GroundingCertificate::with_witt_bits(witt_bits);
    Ok(crate::enforcement::__uor_macro_mint_validated(prov, cert))
}

/// Run the `InhabitanceResolver` dispatch on a `ConstrainedTypeShape`
/// input at `level`.
///
/// Routes to the 2-SAT / Horn-SAT / residual decider via
/// `predicate:InhabitanceDispatchTable` rules (ordered by priority).
///
/// # Errors
///
/// Returns `InhabitanceImpossibilityWitness` when the input is unsatisfiable.
pub fn run_inhabitance<T: ConstrainedTypeShape + ?Sized>(
    input: &T,
    level: WittLevel,
) -> Result<Validated<InhabitanceCertificate>, InhabitanceImpossibilityWitness> {
    let witt_bits = level.witt_length() as u16;
    preflight_budget_solvency(witt_bits as u64, witt_bits as u32)
        .map_err(|_| InhabitanceImpossibilityWitness::default())?;
    preflight_feasibility(T::CONSTRAINTS)
        .map_err(|_| InhabitanceImpossibilityWitness::default())?;
    preflight_package_coherence(T::CONSTRAINTS)
        .map_err(|_| InhabitanceImpossibilityWitness::default())?;
    preflight_dispatch_coverage().map_err(|_| InhabitanceImpossibilityWitness::default())?;
    preflight_timing().map_err(|_| InhabitanceImpossibilityWitness::default())?;
    runtime_timing().map_err(|_| InhabitanceImpossibilityWitness::default())?;
    let outcome = run_reduction_stages(input, witt_bits)
        .map_err(|_| InhabitanceImpossibilityWitness::default())?;
    if outcome.satisfiable {
        let prov = MacroProvenance::__for_macro_crate();
        let cert = InhabitanceCertificate::with_witt_bits(outcome.witt_bits);
        Ok(crate::enforcement::__uor_macro_mint_validated(prov, cert))
    } else {
        Err(InhabitanceImpossibilityWitness::default())
    }
}

/// Run the full pipeline for `uor_ground!` macro expansion. Produces a
/// `Grounded<T>` value on `reduction:PipelineSuccess`.
/// # Errors
/// Returns `PipelineFailure` on preflight or stage failure.
pub fn run_pipeline<T: ConstrainedTypeShape + crate::enforcement::GroundedShape>(
    input: &T,
    witt_bits: u16,
) -> Result<Grounded<T>, PipelineFailure> {
    preflight_budget_solvency(witt_bits as u64, witt_bits as u32)
        .map_err(|report| PipelineFailure::ShapeViolation { report })?;
    preflight_feasibility(T::CONSTRAINTS)
        .map_err(|report| PipelineFailure::ShapeViolation { report })?;
    preflight_package_coherence(T::CONSTRAINTS)
        .map_err(|report| PipelineFailure::ShapeViolation { report })?;
    preflight_dispatch_coverage().map_err(|report| PipelineFailure::ShapeViolation { report })?;
    preflight_timing().map_err(|report| PipelineFailure::ShapeViolation { report })?;
    runtime_timing().map_err(|report| PipelineFailure::ShapeViolation { report })?;
    let outcome = run_reduction_stages(input, witt_bits)?;
    if !outcome.satisfiable {
        return Err(PipelineFailure::ContradictionDetected {
            at_step: 0,
            trace_iri: "https://uor.foundation/trace/InhabitanceSearchTrace",
        });
    }
    let prov = MacroProvenance::__for_macro_crate();
    let grounding =
        crate::enforcement::__uor_macro_mint_validated(prov, GroundingCertificate::default());
    let bindings = empty_bindings_table();
    Ok(crate::enforcement::__uor_macro_mint_grounded::<T>(
        MacroProvenance::__for_macro_crate(),
        grounding,
        bindings,
        outcome.witt_bits,
        outcome.unit_address,
    ))
}

/// Construct an empty `BindingsTable` for v0.2.1 stub inputs.
#[must_use]
pub const fn empty_bindings_table() -> BindingsTable {
    BindingsTable::new(&[])
}

// Suppress warning: BindingEntry is re-exported via use but not used in
// this module directly; it's part of the public pipeline surface.
#[allow(dead_code)]
const _BINDING_ENTRY_REF: Option<BindingEntry> = None;
// Same for CompletenessCertificate — v0.2.1 pipeline does not yet mint
// these directly; they're consumed by the macros crate.
#[allow(dead_code)]
const _COMPLETENESS_CERT_REF: Option<CompletenessCertificate> = None;