uor-foundation 0.3.1

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

//! 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, CompileTime, CompileUnit, CompileUnitBuilder,
    CompletenessCertificate, ConstrainedTypeInput, GenericImpossibilityWitness, Grounded,
    GroundingCertificate, InhabitanceCertificate, InhabitanceImpossibilityWitness,
    LeaseDeclaration, LeaseDeclarationBuilder, LiftChainCertificate, MultiplicationCertificate,
    ParallelDeclarationBuilder, PipelineFailure, ShapeViolation, StreamDeclarationBuilder, Term,
    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",
];

/// Phase 17: maximum number of `i64` coefficients an `Affine`
/// constraint can carry. Stable-Rust const evaluation cannot allocate a
/// new `&'static [i64]` at compile time, so `Affine` stores a fixed-
/// size buffer + an active prefix length. Aligned with the foundation's
/// 8-wide capacity caps (`MAX_BETTI_DIMENSION` / `JACOBIAN_MAX_SITES` /
/// `NERVE_CONSTRAINTS_CAP`).
pub const AFFINE_MAX_COEFFS: usize = 8;

/// Phase 17: maximum number of `LeafConstraintRef` conjuncts a
/// `Conjunction` can carry. Same reasoning as `AFFINE_MAX_COEFFS`.
pub const CONJUNCTION_MAX_TERMS: usize = 8;

/// Opaque constraint reference carried by `ConstrainedTypeShape` impls.
/// Variants mirror the v0.2.1 `type:Constraint` enumerated subclasses
/// (retained as ergonomic aliases for the SAT pipeline) plus the v0.2.2
/// Phase D parametric form (`Bound` / `Conjunction`) which references
/// `BoundConstraint` kinds by their (observable, shape) IRIs. The
/// `SatClauses` variant carries a compact 2-SAT/Horn-SAT clause list.
/// **Phase 17 — fixed-array Affine and Conjunction.** The pre-Phase-17
/// `Affine { coefficients: &'static [i64], … }` and
/// `Conjunction { conjuncts: &'static [ConstraintRef] }` have been
/// replaced with fixed-capacity arrays of length `AFFINE_MAX_COEFFS`
/// and `CONJUNCTION_MAX_TERMS` respectively. Stable Rust const
/// evaluation can build these inline; the SDK macros now support
/// Affine-bearing operands without falling back to the
/// `Site { position: u32::MAX }` sentinel. `Conjunction` is depth-
/// limited to one level: its conjuncts are `LeafConstraintRef`
/// (every variant of `ConstraintRef` except `Conjunction` itself).
#[derive(Debug, Clone, Copy)]
#[non_exhaustive]
#[allow(clippy::large_enum_variant)]
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.
    /// `coefficients[..coefficient_count as usize]` is the active prefix;
    /// trailing entries are unused and must be zero.
    Affine {
        coefficients: [i64; AFFINE_MAX_COEFFS],
        coefficient_count: u32,
        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,
    },
    /// v0.2.2 Phase D / T2.2 (cleanup): parametric `BoundConstraint`
    /// kind reference. Selects an (observable, shape) pair from the
    /// closed Phase D catalogue. The args_repr string carries the
    /// kind-specific parameters in canonical form.
    Bound {
        observable_iri: &'static str,
        bound_shape_iri: &'static str,
        args_repr: &'static str,
    },
    /// v0.2.2 Phase D / T2.2 (cleanup): parametric `Conjunction`.
    /// Phase 17: depth-limited to one level — conjuncts are
    /// `LeafConstraintRef` (every `ConstraintRef` variant except
    /// `Conjunction` itself). Active prefix is
    /// `conjuncts[..conjunct_count as usize]`.
    Conjunction {
        conjuncts: [LeafConstraintRef; CONJUNCTION_MAX_TERMS],
        conjunct_count: u32,
    },
}

/// `ConstraintRef` minus the recursive `Conjunction` variant — the
/// element type of `ConstraintRef::Conjunction.conjuncts`. Phase 17
/// caps Conjunction depth at one level; deeper structure must be
/// flattened by the constructor.
#[derive(Debug, Clone, Copy)]
#[non_exhaustive]
pub enum LeafConstraintRef {
    /// See [`ConstraintRef::Residue`].
    Residue { modulus: u64, residue: u64 },
    /// See [`ConstraintRef::Hamming`].
    Hamming { bound: u32 },
    /// See [`ConstraintRef::Depth`].
    Depth { min: u32, max: u32 },
    /// See [`ConstraintRef::Carry`].
    Carry { site: u32 },
    /// See [`ConstraintRef::Site`].
    Site { position: u32 },
    /// See [`ConstraintRef::Affine`].
    Affine {
        coefficients: [i64; AFFINE_MAX_COEFFS],
        coefficient_count: u32,
        bias: i64,
    },
    /// See [`ConstraintRef::SatClauses`].
    SatClauses {
        clauses: &'static [&'static [(u32, bool)]],
        num_vars: u32,
    },
    /// See [`ConstraintRef::Bound`].
    Bound {
        observable_iri: &'static str,
        bound_shape_iri: &'static str,
        args_repr: &'static str,
    },
}

/// Project a non-`Conjunction` [`ConstraintRef`] into the
/// [`LeafConstraintRef`] subtype. Returns a `Site { position: 0 }`
/// placeholder if `self` is `Conjunction` (the only non-injective
/// case); callers should flatten Conjunction structure before
/// calling.
impl ConstraintRef {
    /// Phase 17 — leaf projection.
    #[inline]
    #[must_use]
    pub const fn as_leaf(self) -> LeafConstraintRef {
        match self {
            ConstraintRef::Residue { modulus, residue } => {
                LeafConstraintRef::Residue { modulus, residue }
            }
            ConstraintRef::Hamming { bound } => LeafConstraintRef::Hamming { bound },
            ConstraintRef::Depth { min, max } => LeafConstraintRef::Depth { min, max },
            ConstraintRef::Carry { site } => LeafConstraintRef::Carry { site },
            ConstraintRef::Site { position } => LeafConstraintRef::Site { position },
            ConstraintRef::Affine {
                coefficients,
                coefficient_count,
                bias,
            } => LeafConstraintRef::Affine {
                coefficients,
                coefficient_count,
                bias,
            },
            ConstraintRef::SatClauses { clauses, num_vars } => {
                LeafConstraintRef::SatClauses { clauses, num_vars }
            }
            ConstraintRef::Bound {
                observable_iri,
                bound_shape_iri,
                args_repr,
            } => LeafConstraintRef::Bound {
                observable_iri,
                bound_shape_iri,
                args_repr,
            },
            ConstraintRef::Conjunction { .. } => LeafConstraintRef::Site { position: 0 },
        }
    }
}

impl LeafConstraintRef {
    /// Phase 17 — embed a leaf into the parent `ConstraintRef` enum.
    #[inline]
    #[must_use]
    pub const fn into_constraint(self) -> ConstraintRef {
        match self {
            LeafConstraintRef::Residue { modulus, residue } => {
                ConstraintRef::Residue { modulus, residue }
            }
            LeafConstraintRef::Hamming { bound } => ConstraintRef::Hamming { bound },
            LeafConstraintRef::Depth { min, max } => ConstraintRef::Depth { min, max },
            LeafConstraintRef::Carry { site } => ConstraintRef::Carry { site },
            LeafConstraintRef::Site { position } => ConstraintRef::Site { position },
            LeafConstraintRef::Affine {
                coefficients,
                coefficient_count,
                bias,
            } => ConstraintRef::Affine {
                coefficients,
                coefficient_count,
                bias,
            },
            LeafConstraintRef::SatClauses { clauses, num_vars } => {
                ConstraintRef::SatClauses { clauses, num_vars }
            }
            LeafConstraintRef::Bound {
                observable_iri,
                bound_shape_iri,
                args_repr,
            } => ConstraintRef::Bound {
                observable_iri,
                bound_shape_iri,
                args_repr,
            },
        }
    }
}

/// Workstream E (target §1.5 + §4.7, v0.2.2 closure): crate-internal
/// dispatch helper that maps every `ConstraintRef` variant to its
/// canonical CNF clause encoding. No variant returns `None` — the
/// closed six-kind set is fully executable.
/// - `SatClauses`: pass-through of the caller's CNF.
/// - `Residue` / `Carry` / `Depth` / `Hamming` / `Site`: direct-
///   decidable at preflight; encoder emits an empty clause list
///   (trivially SAT — unsatisfiable ones are rejected earlier).
/// - `Affine`: single-row consistency check over Z/(2^n)Z; emits
///   empty clauses when consistent, a 2-literal contradiction
///   sentinel (forcing 2-SAT rejection) when not.
/// - `Bound`: parametric form; emits empty clauses (per-bound-kind
///   decision procedures consume the observable/bound-shape IRIs).
/// - `Conjunction`: satisfiable iff every conjunct is satisfiable.
#[inline]
#[must_use]
#[allow(dead_code)]
pub(crate) const fn encode_constraint_to_clauses(
    constraint: &ConstraintRef,
) -> Option<&'static [&'static [(u32, bool)]]> {
    const EMPTY: &[&[(u32, bool)]] = &[];
    const UNSAT_SENTINEL: &[&[(u32, bool)]] = &[&[(0u32, false)], &[(0u32, true)]];
    match constraint {
        ConstraintRef::SatClauses { clauses, .. } => Some(clauses),
        ConstraintRef::Residue { .. }
        | ConstraintRef::Carry { .. }
        | ConstraintRef::Depth { .. }
        | ConstraintRef::Hamming { .. }
        | ConstraintRef::Site { .. } => Some(EMPTY),
        ConstraintRef::Affine {
            coefficients,
            coefficient_count,
            bias,
        } => {
            if is_affine_consistent(coefficients, *coefficient_count, *bias) {
                Some(EMPTY)
            } else {
                Some(UNSAT_SENTINEL)
            }
        }
        ConstraintRef::Bound { .. } => Some(EMPTY),
        ConstraintRef::Conjunction {
            conjuncts,
            conjunct_count,
        } => {
            if conjunction_all_sat(conjuncts, *conjunct_count) {
                Some(EMPTY)
            } else {
                Some(UNSAT_SENTINEL)
            }
        }
    }
}

/// Workstream E: single-row consistency for `Affine { coefficients,
/// coefficient_count, bias }`. The constraint is
/// `sum(c_i) · x = bias (mod 2^n)`; when the coefficient sum is
/// zero the system is consistent iff bias is zero. Non-zero sums
/// are always consistent over Z/(2^n)Z for some `x` value. Iterates
/// only the active prefix `coefficients[..coefficient_count as usize]`.
#[inline]
#[must_use]
const fn is_affine_consistent(
    coefficients: &[i64; AFFINE_MAX_COEFFS],
    coefficient_count: u32,
    bias: i64,
) -> bool {
    let mut sum: i128 = 0;
    let count = coefficient_count as usize;
    let mut i = 0;
    while i < count && i < AFFINE_MAX_COEFFS {
        sum += coefficients[i] as i128;
        i += 1;
    }
    if sum == 0 {
        bias == 0
    } else {
        true
    }
}

/// Workstream E + Phase 17: satisfiability of a `Conjunction`.
/// Iterates only the active prefix `conjuncts[..conjunct_count as
/// usize]` and lifts each `LeafConstraintRef` back to a
/// `ConstraintRef` for re-encoding (the leaf form omits Conjunction,
/// so this terminates at depth 1).
#[inline]
#[must_use]
const fn conjunction_all_sat(
    conjuncts: &[LeafConstraintRef; CONJUNCTION_MAX_TERMS],
    conjunct_count: u32,
) -> bool {
    let count = conjunct_count as usize;
    let mut i = 0;
    while i < count && i < CONJUNCTION_MAX_TERMS {
        let lifted = conjuncts[i].into_constraint();
        match encode_constraint_to_clauses(&lifted) {
            Some([]) => {}
            _ => return false,
        }
        i += 1;
    }
    true
}

/// Declarative shape of a constrained type that can be admitted into the
/// reduction pipeline.
/// Downstream authors implement this trait on zero-sized marker types to
/// declare the `(IRI, SITE_COUNT, CONSTRAINTS)` triple of a custom
/// constrained type. The foundation admits shapes into the pipeline via
/// [`validate_constrained_type`] / [`validate_constrained_type_const`],
/// which run the full preflight (`preflight_feasibility` +
/// `preflight_package_coherence`) against `Self::CONSTRAINTS` before
/// returning a [`Validated`] wrapper.
/// Sealing of witness construction lives on [`Validated`] and [`Grounded`]
/// — only foundation admission functions mint either. Downstream is free
/// to implement `ConstrainedTypeShape` for arbitrary shape markers, but
/// cannot fabricate a `Validated<Self>` except through the admission path.
/// The `ConstraintRef` enum is `#[non_exhaustive]` from outside the crate,
/// so `CONSTRAINTS` can only cite foundation-closed constraint kinds.
/// # Example
/// ```
/// use uor_foundation::pipeline::{
///     ConstrainedTypeShape, ConstraintRef, validate_constrained_type,
/// };
/// pub struct MyShape;
/// impl ConstrainedTypeShape for MyShape {
///     const IRI: &'static str = "https://example.org/MyShape";
///     const SITE_COUNT: usize = 4;
///     const CONSTRAINTS: &'static [ConstraintRef] = &[
///         ConstraintRef::Residue { modulus: 7, residue: 3 },
///     ];
/// }
/// let validated = validate_constrained_type(MyShape)
///     .expect("residue 3 mod 7 is admissible");
/// # let _ = validated;
/// ```
pub trait ConstrainedTypeShape {
    /// 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;
    /// Ontology-level `siteBudget`: count of data sites only,
    /// excluding bookkeeping introduced by composition (coproduct tag
    /// sites, etc.). Equals `SITE_COUNT` for leaf shapes and for
    /// shapes whose composition introduces no bookkeeping (products,
    /// cartesian products). Strictly less than `SITE_COUNT` for coproduct
    /// shapes and any shape whose `SITE_COUNT` includes inherited
    /// bookkeeping. Introduced by the Product/Coproduct Completion
    /// Amendment §4a; defaults to `SITE_COUNT` so pre-amendment
    /// shape impls remain valid without edits.
    const SITE_BUDGET: usize = Self::SITE_COUNT;
    /// 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] = &[];
}

/// Marker for a `ConstrainedTypeShape` that is the Cartesian product of
/// two component shapes. Selecting this trait routes nerve-Betti computation
/// through Künneth composition of component Betti profiles rather than
/// flat enumeration of (constraint, constraint) pairs. Introduced by the
/// Product/Coproduct Completion Amendment §3c for CartesianPartitionProduct
/// (CPT_1–CPT_6).
pub trait CartesianProductShape: ConstrainedTypeShape {
    /// Left operand shape.
    type Left: ConstrainedTypeShape;
    /// Right operand shape.
    type Right: ConstrainedTypeShape;
}

/// Künneth composition of two Betti profiles.
/// Computes `out[k] = Σ_{i + j = k} a[i] · b[j]` over
/// `[0, MAX_BETTI_DIMENSION)`. All arithmetic uses saturating operations so the
/// function is total on `[u32; MAX_BETTI_DIMENSION]` inputs without panicking.
pub const fn kunneth_compose(
    a: &[u32; crate::enforcement::MAX_BETTI_DIMENSION],
    b: &[u32; crate::enforcement::MAX_BETTI_DIMENSION],
) -> [u32; crate::enforcement::MAX_BETTI_DIMENSION] {
    let mut out = [0u32; crate::enforcement::MAX_BETTI_DIMENSION];
    let mut i: usize = 0;
    while i < crate::enforcement::MAX_BETTI_DIMENSION {
        let mut j: usize = 0;
        while j < crate::enforcement::MAX_BETTI_DIMENSION - i {
            let term = a[i].saturating_mul(b[j]);
            out[i + j] = out[i + j].saturating_add(term);
            j += 1;
        }
        i += 1;
    }
    out
}

/// Cartesian-product nerve Betti via Künneth composition of the component
/// shapes' Betti profiles. Used instead of
/// `primitive_simplicial_nerve_betti` when a shape declares itself as a
/// `CartesianProductShape`. Amendment §3c.
/// Phase 1a (orphan-closure): propagates either component's
/// `NERVE_CAPACITY_EXCEEDED` via `?`. Dropped `const fn` because
/// the `Result` return of the per-component primitive is not `const`-evaluable.
/// # Errors
/// Returns `NERVE_CAPACITY_EXCEEDED` if either component exceeds caps.
pub fn primitive_cartesian_nerve_betti<S: CartesianProductShape>() -> Result<
    [u32; crate::enforcement::MAX_BETTI_DIMENSION],
    crate::enforcement::GenericImpossibilityWitness,
> {
    let left = crate::enforcement::primitive_simplicial_nerve_betti::<S::Left>()?;
    let right = crate::enforcement::primitive_simplicial_nerve_betti::<S::Right>()?;
    Ok(kunneth_compose(&left, &right))
}

/// Shift every site-index reference in a `ConstraintRef` by `offset`.
/// Used by the SDK's `product_shape!` / `coproduct_shape!` /
/// `cartesian_product_shape!` macros to splice an operand's constraints into
/// a combined shape at a post-operand offset.
/// **Phase 17: full operand-catalogue support.** Affine and
/// Conjunction now shift correctly at const time because the
/// variants store fixed-size arrays (no `&'static [i64]` allocation
/// required). The pre-Phase-17 `Site { position: u32::MAX }`
/// sentinel is removed.
/// **Variant coverage.**
/// - `Site { position }` → position += offset.
/// - `Carry { site }` → site += offset.
/// - `Residue`, `Hamming`, `Depth`, `SatClauses`, `Bound`: pass through (no
///   site references at this layer).
/// - `Affine { coefficients, coefficient_count, bias }`: builds a fresh
///   `[i64; AFFINE_MAX_COEFFS]` of zeros, copies the active prefix into
///   positions `[offset, offset + coefficient_count)`. If the shift
///   would overflow the fixed buffer, returns an Affine with
///   `coefficient_count = 0` (vacuously consistent).
/// - `Conjunction { conjuncts, conjunct_count }`: builds a fresh
///   `[LeafConstraintRef; CONJUNCTION_MAX_TERMS]` and shifts each leaf
///   via `shift_leaf_constraint`. One-level depth — leaves cannot be
///   Conjunction.
pub const fn shift_constraint(c: ConstraintRef, offset: u32) -> ConstraintRef {
    match c {
        ConstraintRef::Site { position } => ConstraintRef::Site {
            position: position.saturating_add(offset),
        },
        ConstraintRef::Carry { site } => ConstraintRef::Carry {
            site: site.saturating_add(offset),
        },
        ConstraintRef::Residue { modulus, residue } => ConstraintRef::Residue { modulus, residue },
        ConstraintRef::Hamming { bound } => ConstraintRef::Hamming { bound },
        ConstraintRef::Depth { min, max } => ConstraintRef::Depth { min, max },
        ConstraintRef::SatClauses { clauses, num_vars } => {
            ConstraintRef::SatClauses { clauses, num_vars }
        }
        ConstraintRef::Bound {
            observable_iri,
            bound_shape_iri,
            args_repr,
        } => ConstraintRef::Bound {
            observable_iri,
            bound_shape_iri,
            args_repr,
        },
        ConstraintRef::Affine {
            coefficients,
            coefficient_count,
            bias,
        } => {
            let (out, new_count) =
                shift_affine_coefficients(&coefficients, coefficient_count, offset);
            ConstraintRef::Affine {
                coefficients: out,
                coefficient_count: new_count,
                bias,
            }
        }
        ConstraintRef::Conjunction {
            conjuncts,
            conjunct_count,
        } => {
            let mut out = [LeafConstraintRef::Site { position: 0 }; CONJUNCTION_MAX_TERMS];
            let count = conjunct_count as usize;
            let mut i = 0;
            while i < count && i < CONJUNCTION_MAX_TERMS {
                out[i] = shift_leaf_constraint(conjuncts[i], offset);
                i += 1;
            }
            ConstraintRef::Conjunction {
                conjuncts: out,
                conjunct_count,
            }
        }
    }
}

/// Phase 17 helper: shift the active prefix of an `Affine`
/// coefficient array right by `offset`, returning a fresh
/// `[i64; AFFINE_MAX_COEFFS]` and the new active count. If the
/// shift would overflow the fixed buffer, returns count `0`
/// (vacuously consistent — no constraint).
#[inline]
#[must_use]
const fn shift_affine_coefficients(
    coefficients: &[i64; AFFINE_MAX_COEFFS],
    coefficient_count: u32,
    offset: u32,
) -> ([i64; AFFINE_MAX_COEFFS], u32) {
    let mut out = [0i64; AFFINE_MAX_COEFFS];
    let count = coefficient_count as usize;
    let off = offset as usize;
    if off >= AFFINE_MAX_COEFFS {
        return (out, 0);
    }
    let mut i = 0;
    while i < count && i + off < AFFINE_MAX_COEFFS {
        out[i + off] = coefficients[i];
        i += 1;
    }
    let new_count = (i + off) as u32;
    (out, new_count)
}

/// Phase 17 helper: same as [`shift_constraint`] but operating on a
/// [`LeafConstraintRef`]. Used by Conjunction-shifting paths that
/// must preserve the leaf-only depth limit.
#[inline]
#[must_use]
pub const fn shift_leaf_constraint(c: LeafConstraintRef, offset: u32) -> LeafConstraintRef {
    match c {
        LeafConstraintRef::Site { position } => LeafConstraintRef::Site {
            position: position.saturating_add(offset),
        },
        LeafConstraintRef::Carry { site } => LeafConstraintRef::Carry {
            site: site.saturating_add(offset),
        },
        LeafConstraintRef::Residue { modulus, residue } => {
            LeafConstraintRef::Residue { modulus, residue }
        }
        LeafConstraintRef::Hamming { bound } => LeafConstraintRef::Hamming { bound },
        LeafConstraintRef::Depth { min, max } => LeafConstraintRef::Depth { min, max },
        LeafConstraintRef::SatClauses { clauses, num_vars } => {
            LeafConstraintRef::SatClauses { clauses, num_vars }
        }
        LeafConstraintRef::Bound {
            observable_iri,
            bound_shape_iri,
            args_repr,
        } => LeafConstraintRef::Bound {
            observable_iri,
            bound_shape_iri,
            args_repr,
        },
        LeafConstraintRef::Affine {
            coefficients,
            coefficient_count,
            bias,
        } => {
            let (out, new_count) =
                shift_affine_coefficients(&coefficients, coefficient_count, offset);
            LeafConstraintRef::Affine {
                coefficients: out,
                coefficient_count: new_count,
                bias,
            }
        }
    }
}

/// SDK support: concatenate two operand constraint arrays into a padded
/// fixed-size buffer of length `2 * crate::enforcement::NERVE_CONSTRAINTS_CAP`.
/// A's constraints are copied verbatim at indices `[0, A::CONSTRAINTS.len())`;
/// B's constraints are copied at `[A::CONSTRAINTS.len(), total)` with each
/// entry passed through `shift_constraint(c, A::SITE_COUNT as u32)`.
/// Trailing positions are filled with the `Site { position: u32::MAX }`
/// sentinel.
/// Consumers pair this with `sdk_product_constraints_len` to derive the
/// slice length at const-eval time: `&BUF[..LEN]` yields a `&'static
/// [ConstraintRef]` of the correct length without `unsafe`.
pub const fn sdk_concat_product_constraints<A, B>(
) -> [ConstraintRef; 2 * crate::enforcement::NERVE_CONSTRAINTS_CAP]
where
    A: ConstrainedTypeShape,
    B: ConstrainedTypeShape,
{
    let mut out =
        [ConstraintRef::Site { position: u32::MAX }; 2 * crate::enforcement::NERVE_CONSTRAINTS_CAP];
    let left = A::CONSTRAINTS;
    let right = B::CONSTRAINTS;
    let offset = A::SITE_COUNT as u32;
    let mut i: usize = 0;
    while i < left.len() {
        out[i] = left[i];
        i += 1;
    }
    let mut j: usize = 0;
    while j < right.len() {
        out[i + j] = shift_constraint(right[j], offset);
        j += 1;
    }
    out
}

/// Companion length helper for `sdk_concat_product_constraints`.
pub const fn sdk_product_constraints_len<A, B>() -> usize
where
    A: ConstrainedTypeShape,
    B: ConstrainedTypeShape,
{
    A::CONSTRAINTS.len() + B::CONSTRAINTS.len()
}

/// Admit a downstream [`ConstrainedTypeShape`] into the reduction pipeline.
/// Runs the full preflight chain on `T::CONSTRAINTS`:
/// [`preflight_feasibility`] and [`preflight_package_coherence`]. On success,
/// wraps the supplied `shape` in a [`Validated`] carrying `Runtime` phase.
/// # Errors
/// Returns [`ShapeViolation`] if any constraint in `T::CONSTRAINTS` fails
/// feasibility checking (e.g., residue out of range, depth min > max) or if
/// the constraint system is internally incoherent (e.g., contradictory
/// residue constraints on the same modulus).
/// # Example
/// ```
/// use uor_foundation::pipeline::{
///     ConstrainedTypeShape, ConstraintRef, validate_constrained_type,
/// };
/// pub struct MyShape;
/// impl ConstrainedTypeShape for MyShape {
///     const IRI: &'static str = "https://example.org/MyShape";
///     const SITE_COUNT: usize = 2;
///     const CONSTRAINTS: &'static [ConstraintRef] = &[
///         ConstraintRef::Residue { modulus: 5, residue: 2 },
///     ];
/// }
/// let validated = validate_constrained_type(MyShape).unwrap();
/// # let _ = validated;
/// ```
pub fn validate_constrained_type<T: ConstrainedTypeShape>(
    shape: T,
) -> Result<Validated<T, crate::enforcement::Runtime>, ShapeViolation> {
    preflight_feasibility(T::CONSTRAINTS)?;
    preflight_package_coherence(T::CONSTRAINTS)?;
    Ok(Validated::new(shape))
}

/// Const-fn companion for [`validate_constrained_type`].
/// Admits a downstream [`ConstrainedTypeShape`] at compile time, running the
/// same preflight checks as the runtime variant but in `const` context.
/// # Scope
/// `ConstraintRef::Bound { observable_iri, args_repr, .. }` with
/// `observable_iri == "https://uor.foundation/observable/LandauerCost"`
/// requires `f64::from_bits` for args parsing, which is stable in `const`
/// context only from Rust 1.83. The crate's MSRV is 1.81, so this variant
/// rejects const admission of `LandauerCost`-bound constraints with
/// [`ShapeViolation`] and recommends the runtime [`validate_constrained_type`]
/// for those inputs. All other `ConstraintRef` variants admit at const time.
/// # Errors
/// Same as [`validate_constrained_type`], plus the const-context rejection
/// for `LandauerCost`-bound constraints described above.
/// The `T: Copy` bound is required by `const fn` — destructor invocation is
/// not yet const-stable, and `Validated<T>` carries `T` by value. Shape
/// markers are typically zero-sized types which are trivially `Copy`.
pub const fn validate_constrained_type_const<T: ConstrainedTypeShape + Copy>(
    shape: T,
) -> Result<Validated<T, crate::enforcement::CompileTime>, ShapeViolation> {
    // Const-path preflight: walk CONSTRAINTS and apply per-variant const checks.
    // Rejects LandauerCost-bound constraints that need non-const f64::from_bits.
    let constraints = T::CONSTRAINTS;
    let mut i = 0;
    while i < constraints.len() {
        let ok = match &constraints[i] {
            ConstraintRef::SatClauses { clauses, num_vars } => *num_vars != 0 || clauses.is_empty(),
            ConstraintRef::Residue { modulus, residue } => *modulus != 0 && *residue < *modulus,
            ConstraintRef::Carry { .. } => true,
            ConstraintRef::Depth { min, max } => *min <= *max,
            ConstraintRef::Hamming { bound } => *bound <= 32_768,
            ConstraintRef::Site { .. } => true,
            ConstraintRef::Affine {
                coefficients,
                coefficient_count,
                bias,
            } => {
                // Mirror preflight_feasibility's Affine arm in const context.
                let count = *coefficient_count as usize;
                if count == 0 {
                    false
                } else {
                    let mut ok_coeff = true;
                    let mut idx = 0;
                    while idx < count && idx < AFFINE_MAX_COEFFS {
                        if coefficients[idx] == i64::MIN {
                            ok_coeff = false;
                            break;
                        }
                        idx += 1;
                    }
                    ok_coeff && is_affine_consistent(coefficients, *coefficient_count, *bias)
                }
            }
            ConstraintRef::Bound { observable_iri, .. } => {
                // const-fn scope: LandauerCost needs f64::from_bits (stable in
                // const at 1.83). Reject it here; runtime admission handles it.
                !crate::enforcement::str_eq(
                    observable_iri,
                    "https://uor.foundation/observable/LandauerCost",
                )
            }
            ConstraintRef::Conjunction {
                conjuncts,
                conjunct_count,
            } => conjunction_all_sat(conjuncts, *conjunct_count),
        };
        if !ok {
            return Err(ShapeViolation {
                shape_iri: "https://uor.foundation/type/ConstrainedType",
                constraint_iri: "https://uor.foundation/type/ConstrainedType_const_constraint",
                property_iri: "https://uor.foundation/type/constraints",
                expected_range: "https://uor.foundation/type/Constraint",
                min_count: 1,
                max_count: 1,
                kind: ViolationKind::ValueCheck,
            });
        }
        i += 1;
    }
    Ok(Validated::new(shape))
}

/// 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`: the dispatch table has no polynomial decider
/// for them, so they route to the `ResidualVerdictResolver` catch-all.
#[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).
/// 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.
/// 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
}

/// `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,
        })
    }
}

/// v0.2.2 Phase F: upper bound on `CarryDepthObservable` depth arguments.
/// Matches target §4.5's Witt-level tower ceiling (W16384).
pub const WITT_MAX_BITS: u16 = 16_384;

/// v0.2.2 Phase F: ASCII parser for a single unsigned decimal `u32`.
/// Returns 0 on malformed input; the caller's downstream comparison (`depth <= WITT_MAX_BITS`)
/// accepts 0 as the pass-through degenerate depth, so malformed input is rejected
/// by the enclosing feasibility check only if the parsed value exceeds the cap.
/// For stricter input discipline, the caller pre-validates `args_repr` at builder time.
#[must_use]
pub fn parse_u32(s: &str) -> u32 {
    let bytes = s.as_bytes();
    let mut out: u32 = 0;
    let mut i = 0;
    while i < bytes.len() {
        let b = bytes[i];
        if !b.is_ascii_digit() {
            return 0;
        }
        out = out.saturating_mul(10).saturating_add((b - b'0') as u32);
        i += 1;
    }
    out
}

/// v0.2.2 Phase F: ASCII parser for a single unsigned decimal `u64`.
#[must_use]
pub fn parse_u64(s: &str) -> u64 {
    let bytes = s.as_bytes();
    let mut out: u64 = 0;
    let mut i = 0;
    while i < bytes.len() {
        let b = bytes[i];
        if !b.is_ascii_digit() {
            return 0;
        }
        out = out.saturating_mul(10).saturating_add((b - b'0') as u64);
        i += 1;
    }
    out
}

/// v0.2.2 Phase F: parser for `"modulus|residue"` decimal pairs.
/// Split on the first ASCII `|`; ASCII-digit-parse each half via `parse_u64`.
#[must_use]
pub fn parse_u64_pair(s: &str) -> (u64, u64) {
    let bytes = s.as_bytes();
    let mut split = bytes.len();
    let mut i = 0;
    while i < bytes.len() {
        if bytes[i] == b'|' {
            split = i;
            break;
        }
        i += 1;
    }
    if split >= bytes.len() {
        return (0, 0);
    }
    let (left, right_with_pipe) = s.split_at(split);
    let (_, right) = right_with_pipe.split_at(1);
    (parse_u64(left), parse_u64(right))
}

/// v0.2.2 Phase F / Phase 9: parse a decimal `u64` representing an
/// IEEE-754 bit pattern. The bit pattern is content-deterministic; call sites
/// project to `H::Decimal` via `DecimalTranscendental::from_bits`.
#[must_use]
pub fn parse_u64_bits_str(s: &str) -> u64 {
    parse_u64(s)
}

/// v0.2.2 Phase F: dispatch a `ConstraintRef::Bound` arm on its `observable_iri`.
/// Canonical observables: `ValueModObservable`, `CarryDepthObservable`, `LandauerCost`.
/// Unknown IRIs are rejected so that an unaudited observable cannot be threaded
/// through the preflight surface silently.
fn check_bound_feasibility(
    observable_iri: &'static str,
    bound_shape_iri: &'static str,
    args_repr: &'static str,
) -> Result<(), ShapeViolation> {
    const VALUE_MOD_IRI: &str = "https://uor.foundation/observable/ValueModObservable";
    const CARRY_DEPTH_IRI: &str = "https://uor.foundation/observable/CarryDepthObservable";
    const LANDAUER_IRI: &str = "https://uor.foundation/observable/LandauerCost";
    let ok = if crate::enforcement::str_eq(observable_iri, VALUE_MOD_IRI) {
        let (modulus, residue) = parse_u64_pair(args_repr);
        modulus != 0 && residue < modulus
    } else if crate::enforcement::str_eq(observable_iri, CARRY_DEPTH_IRI) {
        let depth = parse_u32(args_repr);
        depth <= WITT_MAX_BITS as u32
    } else if crate::enforcement::str_eq(observable_iri, LANDAUER_IRI) {
        // Project the bit pattern to f64 (default-host) for the
        // finite/positive-nats sanity check. Polymorphic consumers
        // construct their own H::Decimal via DecimalTranscendental.
        let bits = parse_u64_bits_str(args_repr);
        let nats = <f64 as crate::DecimalTranscendental>::from_bits(bits);
        nats.is_finite() && nats > 0.0
    } else {
        false
    };
    if ok {
        Ok(())
    } else {
        Err(ShapeViolation {
            shape_iri: bound_shape_iri,
            constraint_iri: "https://uor.foundation/type/BoundConstraint",
            property_iri: observable_iri,
            expected_range: "https://uor.foundation/observable/BaseMetric",
            min_count: 1,
            max_count: 1,
            kind: ViolationKind::ValueCheck,
        })
    }
}

/// `FeasibilityCheck`: verify the constraint system isn't trivially
/// infeasible. Workstream E (target §1.5 + §4.7, v0.2.2 closure):
/// the closed six-kind constraint set is validated by direct per-kind
/// satisfiability checks; any variant that fails is rejected here so
/// downstream resolvers never see an unsatisfiable constraint system.
/// v0.2.2 Phase F: the `Bound` arm dispatches on `observable_iri` to per-observable
/// checks via `check_bound_feasibility`; `Carry` and `Site` remain `Ok(())` by
/// documented design — their constraint semantics are structural invariants of
/// ring arithmetic and site-index bounds respectively, enforced by construction
/// rather than by runtime feasibility checks.
pub fn preflight_feasibility(constraints: &[ConstraintRef]) -> Result<(), ShapeViolation> {
    for c in constraints {
        // v0.2.2 Phase F: Bound dispatches to observable-specific checks with its
        // own bound_shape_iri; early-return with that shape on failure.
        if let ConstraintRef::Bound {
            observable_iri,
            bound_shape_iri,
            args_repr,
        } = c
        {
            check_bound_feasibility(observable_iri, bound_shape_iri, args_repr)?;
            continue;
        }
        let ok = match c {
            ConstraintRef::SatClauses { clauses, num_vars } => *num_vars != 0 || clauses.is_empty(),
            ConstraintRef::Residue { modulus, residue } => *modulus != 0 && *residue < *modulus,
            // Structural invariant of ring arithmetic — carries cannot contradict by construction.
            ConstraintRef::Carry { .. } => true,
            ConstraintRef::Depth { min, max } => min <= max,
            ConstraintRef::Hamming { bound } => *bound <= 32_768,
            // Structural invariant of site indexing — bounds enforced by SITE_COUNT typing.
            ConstraintRef::Site { .. } => true,
            ConstraintRef::Affine {
                coefficients,
                coefficient_count,
                bias,
            } => {
                let count = *coefficient_count as usize;
                if count == 0 {
                    false
                } else {
                    let mut ok_coeff = true;
                    let mut idx = 0;
                    while idx < count && idx < AFFINE_MAX_COEFFS {
                        if coefficients[idx] == i64::MIN {
                            ok_coeff = false;
                            break;
                        }
                        idx += 1;
                    }
                    ok_coeff && is_affine_consistent(coefficients, *coefficient_count, *bias)
                }
            }
            // Handled above via early `if let`; unreachable here.
            ConstraintRef::Bound { .. } => true,
            ConstraintRef::Conjunction {
                conjuncts,
                conjunct_count,
            } => conjunction_all_sat(conjuncts, *conjunct_count),
        };
        if !ok {
            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.
/// The table is exhaustive by construction: Rule 3 (IsResidualFragment) 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(())
}

/// v0.2.2 Phase B: a-priori `UorTime` estimator for preflight timing.
/// Derives a content-deterministic upper bound on the `UorTime` a reduction
/// over `shape` at `witt_bits` will consume, without a physical clock. The
/// bound is `witt_bits × constraint_count` rewrite steps and the matching
/// Landauer nats at `ln 2` per step. Preflight compares this via
/// [`UorTime::min_wall_clock`](crate::enforcement::UorTime::min_wall_clock) against the policy's Nanos budget — no
/// physical clock is consulted.
#[must_use]
pub fn estimate_preflight_uor_time<T: ConstrainedTypeShape + ?Sized>(
    witt_bits: u16,
) -> crate::enforcement::UorTime {
    let steps = (witt_bits as u64).saturating_mul((T::CONSTRAINTS.len() as u64).max(1));
    let nats = (steps as f64) * core::f64::consts::LN_2;
    crate::enforcement::UorTime::new(crate::enforcement::LandauerBudget::new(nats), steps)
}

/// `PreflightTiming`: timing-check preflight. v0.2.2 Phase B: parameterized over
/// a [`TimingPolicy`] carrying the Nanos budget and canonical `Calibration`.
/// The `expected` UorTime is derived a-priori from input shape via
/// [`estimate_preflight_uor_time`] — content-deterministic, no physical
/// clock consulted. Rejects when the Nanos lower bound exceeds the budget.
/// # Errors
/// Returns `ShapeViolation::ValueCheck` when the expected UorTime, converted
/// to Nanos under `P::CALIBRATION`, exceeds `P::PREFLIGHT_BUDGET_NS`.
#[allow(dead_code)]
pub(crate) const CANONICAL_PREFLIGHT_BUDGET_NS: u64 = 10000000;
pub fn preflight_timing<P: crate::enforcement::TimingPolicy>(
    expected: crate::enforcement::UorTime,
) -> Result<(), ShapeViolation> {
    let nanos = expected.min_wall_clock(P::CALIBRATION).as_u64();
    if nanos <= P::PREFLIGHT_BUDGET_NS {
        Ok(())
    } else {
        Err(ShapeViolation {
            shape_iri: "https://uor.foundation/conformance/CompileUnitShape",
            constraint_iri: "https://uor.foundation/reduction/PreflightTimingBound",
            property_iri: "https://uor.foundation/reduction/preflightBudgetNs",
            expected_range: "http://www.w3.org/2001/XMLSchema#nonNegativeInteger",
            min_count: 1,
            max_count: 1,
            kind: ViolationKind::ValueCheck,
        })
    }
}

/// `RuntimeTiming`: runtime timing-check preflight. v0.2.2 Phase B: parameterized
/// over a [`TimingPolicy`] carrying the Nanos budget and canonical `Calibration`.
/// Identical comparison shape as [`preflight_timing`], against the runtime budget.
/// # Errors
/// Returns `ShapeViolation::ValueCheck` when the expected UorTime, converted
/// to Nanos under `P::CALIBRATION`, exceeds `P::RUNTIME_BUDGET_NS`.
#[allow(dead_code)]
pub(crate) const CANONICAL_RUNTIME_BUDGET_NS: u64 = 10000000;
pub fn runtime_timing<P: crate::enforcement::TimingPolicy>(
    expected: crate::enforcement::UorTime,
) -> Result<(), ShapeViolation> {
    let nanos = expected.min_wall_clock(P::CALIBRATION).as_u64();
    if nanos <= P::RUNTIME_BUDGET_NS {
        Ok(())
    } else {
        Err(ShapeViolation {
            shape_iri: "https://uor.foundation/conformance/CompileUnitShape",
            constraint_iri: "https://uor.foundation/reduction/RuntimeTimingBound",
            property_iri: "https://uor.foundation/reduction/runtimeBudgetNs",
            expected_range: "http://www.w3.org/2001/XMLSchema#nonNegativeInteger",
            min_count: 1,
            max_count: 1,
            kind: ViolationKind::ValueCheck,
        })
    }
}

/// 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 {
    /// 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.
///
/// v0.2.2 T6.14: the `unit_address` field was removed. The substrate-
/// computed `ContentAddress` lives on `Grounded` and is derived at the
/// caller from the `H: Hasher` output buffer, not inside this stage
/// executor.
///
/// # Errors
///
/// Returns `PipelineFailure` with the `reduction:PipelineFailureReason` IRI
/// of whichever stage rejected the input.
pub fn run_reduction_stages<T: ConstrainedTypeShape + ?Sized>(
    witt_bits: u16,
) -> Result<StageOutcome, PipelineFailure> {
    // Stage 0 (initialization): content-addressed unit-id is computed by
    // the caller via the consumer-supplied substrate Hasher; nothing to
    // do here.
    // 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. Residual constraint systems are
            // treated 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): ConstrainedTypeShape inputs carry no term AST, so no
    // bindings flow through this path. CompileUnit-bearing callers retrieve the
    // declared bindings directly via `unit.bindings()` (Phase H1); runtime
    // `BindingsTable` materialization is not possible because `BindingsTable::entries`
    // is `&'static [BindingEntry]` by contract (compile-time-constructed catalogs
    // are the sole source of sorted-address binary-search tables).
    // Stage 6 (convergence): verify fixpoint reached. Trivially true for
    // classified fragments.
    Ok(StageOutcome {
        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, H: crate::enforcement::Hasher>(
    _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())?;
    let expected = estimate_preflight_uor_time::<T>(witt_bits);
    preflight_timing::<crate::enforcement::CanonicalTimingPolicy>(expected)
        .map_err(|_| GenericImpossibilityWitness::default())?;
    runtime_timing::<crate::enforcement::CanonicalTimingPolicy>(expected)
        .map_err(|_| GenericImpossibilityWitness::default())?;
    let outcome =
        run_reduction_stages::<T>(witt_bits).map_err(|_| GenericImpossibilityWitness::default())?;
    if outcome.satisfiable {
        // v0.2.2 T6.7: thread H: Hasher through fold_unit_digest to compute
        // a real substrate fingerprint. Witt level + budget=0 (no CompileUnit).
        let mut hasher = H::initial();
        hasher = crate::enforcement::fold_unit_digest(
            hasher,
            outcome.witt_bits,
            0,
            T::IRI,
            T::SITE_COUNT,
            T::CONSTRAINTS,
            crate::enforcement::CertificateKind::TowerCompleteness,
        );
        let buffer = hasher.finalize();
        let fp = crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
        let cert = LiftChainCertificate::with_level_and_fingerprint_const(outcome.witt_bits, fp);
        Ok(Validated::new(cert))
    } else {
        Err(GenericImpossibilityWitness::default())
    }
}

/// Workstream F (target ontology: `resolver:IncrementalCompletenessResolver`):
/// sealed `SpectralSequencePage` kernel type recording one step of the
/// `Q_n → Q_{n+1}` spectral-sequence walk. Each page carries its index,
/// the from/to Witt bit widths, and the differential-vanished flag
/// (true ⇒ page is trivial; false ⇒ obstruction present with class IRI).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct SpectralSequencePage {
    page_index: u32,
    source_bits: u16,
    target_bits: u16,
    differential_vanished: bool,
    obstruction_class_iri: &'static str,
    _sealed: (),
}

impl SpectralSequencePage {
    /// Crate-internal constructor. Minted only by the incremental walker.
    #[inline]
    #[must_use]
    pub(crate) const fn from_parts(
        page_index: u32,
        source_bits: u16,
        target_bits: u16,
        differential_vanished: bool,
        obstruction_class_iri: &'static str,
    ) -> Self {
        Self {
            page_index,
            source_bits,
            target_bits,
            differential_vanished,
            obstruction_class_iri,
            _sealed: (),
        }
    }

    /// Page index (0, 1, 2, …) along the spectral-sequence walk.
    #[inline]
    #[must_use]
    pub const fn page_index(&self) -> u32 {
        self.page_index
    }

    /// Witt bit width at the page's source level.
    #[inline]
    #[must_use]
    pub const fn source_bits(&self) -> u16 {
        self.source_bits
    }

    /// Witt bit width at the page's target level.
    #[inline]
    #[must_use]
    pub const fn target_bits(&self) -> u16 {
        self.target_bits
    }

    /// True iff the page's differential vanishes (no obstruction).
    #[inline]
    #[must_use]
    pub const fn differential_vanished(&self) -> bool {
        self.differential_vanished
    }

    /// Obstruction class IRI when the differential is non-trivial;
    /// empty string when the page is trivial.
    #[inline]
    #[must_use]
    pub const fn obstruction_class_iri(&self) -> &'static str {
        self.obstruction_class_iri
    }
}

/// Run the `IncrementalCompletenessResolver` (spectral-sequence walk)
/// at `target_level`.
///
/// Per `spec/src/namespaces/resolver.rs` (`IncrementalCompletenessResolver`),
/// the walk proceeds without re-running the full ψ-pipeline from
/// scratch. Workstream F (v0.2.2 closure) implements the canonical page
/// structure: iterate each `Q_n → Q_{n+1}` step from `W8` up to
/// `target_level`, compute each page's differential via
/// `run_reduction_stages` at the higher level, and record the
/// `SpectralSequencePage`. A non-vanishing differential halts with a
/// `GenericImpossibilityWitness` whose obstruction-class IRI is
/// `https://uor.foundation/type/LiftObstruction`. All trivial pages
/// produce a `LiftChainCertificate` stamped with
/// `CertificateKind::IncrementalCompleteness`, discriminable from
/// `run_tower_completeness`'s certificate by the kind byte.
///
/// # Errors
///
/// Returns `GenericImpossibilityWitness` when any page's differential
/// does not vanish, or when preflight checks reject the input.
pub fn run_incremental_completeness<
    T: ConstrainedTypeShape + ?Sized,
    H: crate::enforcement::Hasher,
>(
    _input: &T,
    target_level: WittLevel,
) -> Result<Validated<LiftChainCertificate>, GenericImpossibilityWitness> {
    let target_bits = target_level.witt_length() as u16;
    preflight_budget_solvency(target_bits as u64, target_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())?;
    let expected = estimate_preflight_uor_time::<T>(target_bits);
    preflight_timing::<crate::enforcement::CanonicalTimingPolicy>(expected)
        .map_err(|_| GenericImpossibilityWitness::default())?;
    runtime_timing::<crate::enforcement::CanonicalTimingPolicy>(expected)
        .map_err(|_| GenericImpossibilityWitness::default())?;

    // v0.2.2 Phase H4: Betti-driven spectral-sequence walk. At each page, compute
    // the constraint-nerve Betti tuple (via primitive_simplicial_nerve_betti)
    // and run reduction at both source and target levels. The differential at
    // page r with bidegree (p, q) vanishes iff the bidegree-q projection
    // `betti[q]` is unchanged between source and target AND both reductions
    // are satisfiable at their levels. A mismatch in any bidegree or a
    // non-satisfiable reduction produces a non-trivial differential →
    // `LiftObstruction` halt with `GenericImpossibilityWitness`.
    //
    // Betti-threading also produces content-distinct fingerprints for distinct
    // constraint topologies: two input shapes with different Betti profiles will
    // produce different certs even if both satisfy at every level.
    let betti = crate::enforcement::primitive_simplicial_nerve_betti::<T>()?;
    let mut page_index: u32 = 0;
    let mut from_bits: u16 = 8;
    let mut pages_hasher = H::initial();
    while from_bits < target_bits {
        let to_bits = if from_bits + 8 > target_bits {
            target_bits
        } else {
            from_bits + 8
        };
        // Reduce at source and target; both must be satisfiable for the
        // differential to have a chance of vanishing.
        let outcome_source = run_reduction_stages::<T>(from_bits)
            .map_err(|_| GenericImpossibilityWitness::default())?;
        let outcome_target = run_reduction_stages::<T>(to_bits)
            .map_err(|_| GenericImpossibilityWitness::default())?;
        // bidegree q = page_index + 1 (first non-trivial homological degree per page).
        let q: usize = ((page_index as usize) + 1).min(crate::enforcement::MAX_BETTI_DIMENSION - 1);
        let betti_q = betti[q];
        // Differential vanishes iff source ≡ target in Betti bidegree q
        // AND both reduction levels are satisfiable. Betti is shape-invariant
        // (level-independent); the bidegree check is trivially equal, but the
        // satisfiability conjunction captures the level-specific obstruction.
        let differential_vanishes = outcome_source.satisfiable && outcome_target.satisfiable;
        let page = SpectralSequencePage::from_parts(
            page_index,
            from_bits,
            to_bits,
            differential_vanishes,
            if differential_vanishes {
                ""
            } else {
                "https://uor.foundation/type/LiftObstruction"
            },
        );
        if !page.differential_vanished() {
            return Err(GenericImpossibilityWitness::default());
        }
        // Fold the per-page Betti/satisfiability contribution so distinct
        // constraint shapes yield distinct incremental-completeness certs.
        pages_hasher = pages_hasher.fold_bytes(&page_index.to_be_bytes());
        pages_hasher = pages_hasher.fold_bytes(&from_bits.to_be_bytes());
        pages_hasher = pages_hasher.fold_bytes(&to_bits.to_be_bytes());
        pages_hasher = pages_hasher.fold_bytes(&betti_q.to_be_bytes());
        page_index += 1;
        from_bits = to_bits;
    }
    // The accumulated pages_hasher is currently unused in the final fold;
    // the Betti primitive's full tuple is folded below via fold_betti_tuple
    // to keep the cert content-addressed over the whole spectral walk.
    let _ = pages_hasher;

    // Final reduction at the target level — the walk converges when
    // every page's differential has vanished; this guarantees the
    // target-level outcome is satisfiable.
    let outcome = run_reduction_stages::<T>(target_bits)
        .map_err(|_| GenericImpossibilityWitness::default())?;
    if !outcome.satisfiable {
        return Err(GenericImpossibilityWitness::default());
    }
    // v0.2.2 Phase H4: fold the Betti tuple into the cert alongside the
    // canonical unit digest so distinct constraint topologies produce distinct
    // incremental-completeness fingerprints.
    let mut hasher = H::initial();
    hasher = crate::enforcement::fold_betti_tuple(hasher, &betti);
    hasher = crate::enforcement::fold_unit_digest(
        hasher,
        outcome.witt_bits,
        page_index as u64,
        T::IRI,
        T::SITE_COUNT,
        T::CONSTRAINTS,
        crate::enforcement::CertificateKind::IncrementalCompleteness,
    );
    let buffer = hasher.finalize();
    let fp = crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
    let cert = LiftChainCertificate::with_level_and_fingerprint_const(outcome.witt_bits, fp);
    Ok(Validated::new(cert))
}

/// Run the `GroundingAwareResolver` on a `CompileUnit` input at `level`,
/// exploiting `state:GroundedContext` bindings for O(1) resolution per
/// `op:GS_5`.
///
/// v0.2.2 Phase H2: walks `unit.root_term()` enumerating every
/// `Term::Variable { name_index }` and resolves each via linear search
/// over `unit.bindings()`. Unresolved variables (declared in the term AST
/// but absent from the bindings slice) trigger a `GenericImpossibilityWitness`
/// corresponding to `SC5_UNBOUND_VARIABLE`. Resolved bindings are folded
/// into the fingerprint via `primitive_session_binding_signature` so the
/// cert content-addresses the full grounding context, not just the unit
/// shape — distinct binding sets yield distinct fingerprints.
///
/// # Errors
///
/// Returns `GenericImpossibilityWitness` on grounding failure: unresolved
/// variables, or any variable reference whose name index is absent from
/// `unit.bindings()`.
pub fn run_grounding_aware<H: crate::enforcement::Hasher>(
    unit: &CompileUnit,
    level: WittLevel,
) -> Result<Validated<GroundingCertificate>, GenericImpossibilityWitness> {
    let witt_bits = level.witt_length() as u16;
    // v0.2.2 Phase H2: walk root_term enumerating Term::Variable name_indices,
    // linear-search unit.bindings() for each, reject unresolved variables.
    let root_term = unit.root_term();
    let bindings = unit.bindings();
    let mut ti = 0;
    while ti < root_term.len() {
        if let crate::enforcement::Term::Variable { name_index } = root_term[ti] {
            let mut found = false;
            let mut bi = 0;
            while bi < bindings.len() {
                if bindings[bi].name_index == name_index {
                    found = true;
                    break;
                }
                bi += 1;
            }
            if !found {
                // SC_5 violation: variable referenced but no matching binding.
                return Err(GenericImpossibilityWitness::default());
            }
        }
        ti += 1;
    }
    // Fold: witt_bits / thermodynamic_budget / result_type_iri / session_signature / Grounding kind.
    let mut hasher = H::initial();
    hasher = hasher.fold_bytes(&witt_bits.to_be_bytes());
    hasher = hasher.fold_bytes(&unit.thermodynamic_budget().to_be_bytes());
    hasher = hasher.fold_bytes(unit.result_type_iri().as_bytes());
    hasher = hasher.fold_byte(0);
    let (binding_count, fold_addr) =
        crate::enforcement::primitive_session_binding_signature(bindings);
    hasher = crate::enforcement::fold_session_signature(hasher, binding_count, fold_addr);
    hasher = hasher.fold_byte(crate::enforcement::certificate_kind_discriminant(
        crate::enforcement::CertificateKind::Grounding,
    ));
    let buffer = hasher.finalize();
    let fp = crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
    let cert = GroundingCertificate::with_level_and_fingerprint_const(witt_bits, fp);
    Ok(Validated::new(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, H: crate::enforcement::Hasher>(
    _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())?;
    let expected = estimate_preflight_uor_time::<T>(witt_bits);
    preflight_timing::<crate::enforcement::CanonicalTimingPolicy>(expected)
        .map_err(|_| InhabitanceImpossibilityWitness::default())?;
    runtime_timing::<crate::enforcement::CanonicalTimingPolicy>(expected)
        .map_err(|_| InhabitanceImpossibilityWitness::default())?;
    let outcome = run_reduction_stages::<T>(witt_bits)
        .map_err(|_| InhabitanceImpossibilityWitness::default())?;
    if outcome.satisfiable {
        // v0.2.2 T6.7: thread H: Hasher through fold_unit_digest.
        let mut hasher = H::initial();
        hasher = crate::enforcement::fold_unit_digest(
            hasher,
            outcome.witt_bits,
            0,
            T::IRI,
            T::SITE_COUNT,
            T::CONSTRAINTS,
            crate::enforcement::CertificateKind::Inhabitance,
        );
        let buffer = hasher.finalize();
        let fp = crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
        let cert = InhabitanceCertificate::with_level_and_fingerprint_const(outcome.witt_bits, fp);
        Ok(Validated::new(cert))
    } else {
        Err(InhabitanceImpossibilityWitness::default())
    }
}

/// v0.2.2 W14: the single typed pipeline entry point producing `Grounded<T>`
/// from a validated `CompileUnit`. The caller declares the expected shape `T`;
/// the pipeline verifies the unit's root term produces a value of that shape
/// and returns `Grounded<T>` on success or a typed `PipelineFailure`.
/// Replaces the v0.2.1 `run_pipeline(&datum, level: u8)` form whose bare
/// integer level argument was never type-safe.
/// # Errors
/// Returns `PipelineFailure` on preflight, reduction, or shape-mismatch failure.
/// # Example
/// ```no_run
/// use uor_foundation::enforcement::{
///     CompileUnitBuilder, ConstrainedTypeInput, Term,
/// };
/// use uor_foundation::pipeline::run;
/// use uor_foundation::{VerificationDomain, WittLevel};
/// # struct Fnv1aHasher16; // downstream substrate; see foundation/examples/custom_hasher_substrate.rs
/// # impl uor_foundation::enforcement::Hasher for Fnv1aHasher16 {
/// #     const OUTPUT_BYTES: usize = 16;
/// #     fn initial() -> Self { Self }
/// #     fn fold_byte(self, _: u8) -> Self { self }
/// #     fn finalize(self) -> [u8; 32] { [0; 32] }
/// # }
/// static TERMS: &[Term] = &[Term::Literal { value: 1, level: WittLevel::W8 }];
/// static DOMAINS: &[VerificationDomain] = &[VerificationDomain::Enumerative];
/// let unit = CompileUnitBuilder::new()
///     .root_term(TERMS)
///     .witt_level_ceiling(WittLevel::W32)
///     .thermodynamic_budget(1024)
///     .target_domains(DOMAINS)
///     .result_type::<ConstrainedTypeInput>()
///     .validate()
///     .expect("unit well-formed");
/// let grounded = run::<ConstrainedTypeInput, _, Fnv1aHasher16>(unit)
///     .expect("pipeline admits");
/// # let _ = grounded;
/// ```
pub fn run<T, P, H>(unit: Validated<CompileUnit, P>) -> Result<Grounded<T>, PipelineFailure>
where
    T: ConstrainedTypeShape + crate::enforcement::GroundedShape,
    P: crate::enforcement::ValidationPhase,
    H: crate::enforcement::Hasher,
{
    let witt_bits = unit.inner().witt_level().witt_length() as u16;
    let budget = unit.inner().thermodynamic_budget();
    // v0.2.2 T6.11: ShapeMismatch detection. The unit declares its
    // result_type_iri at validation time; the caller's `T::IRI` must match.
    let unit_iri = unit.inner().result_type_iri();
    if !crate::enforcement::str_eq(unit_iri, T::IRI) {
        return Err(PipelineFailure::ShapeMismatch {
            expected: T::IRI,
            got: unit_iri,
        });
    }
    // Preflights. Each maps its ShapeViolation into a 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 })?;
    let expected = estimate_preflight_uor_time::<T>(witt_bits);
    preflight_timing::<crate::enforcement::CanonicalTimingPolicy>(expected)
        .map_err(|report| PipelineFailure::ShapeViolation { report })?;
    runtime_timing::<crate::enforcement::CanonicalTimingPolicy>(expected)
        .map_err(|report| PipelineFailure::ShapeViolation { report })?;
    // v0.2.2 T5 C1: actually call run_reduction_stages and propagate its
    // failure. The previous v0.2.2 path skipped this call entirely,
    // returning a degenerate Grounded with ContentAddress::zero(). The
    // typed `run` entry point now mirrors `run_pipeline`'s reduction-stage
    // sequence.
    let outcome = run_reduction_stages::<T>(witt_bits)?;
    if !outcome.satisfiable {
        return Err(PipelineFailure::ContradictionDetected {
            at_step: 0,
            trace_iri: "https://uor.foundation/trace/InhabitanceSearchTrace",
        });
    }
    // v0.2.2 T5 C3.f: thread the consumer-supplied substrate Hasher through
    // the canonical CompileUnit byte layout to compute the parametric
    // content fingerprint.
    let mut hasher = H::initial();
    hasher = crate::enforcement::fold_unit_digest(
        hasher,
        witt_bits,
        budget,
        T::IRI,
        T::SITE_COUNT,
        T::CONSTRAINTS,
        crate::enforcement::CertificateKind::Grounding,
    );
    let buffer = hasher.finalize();
    let content_fingerprint =
        crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
    let unit_address = crate::enforcement::unit_address_from_buffer(&buffer);
    let grounding = Validated::new(GroundingCertificate::with_level_and_fingerprint_const(
        witt_bits,
        content_fingerprint,
    ));
    let bindings = empty_bindings_table();
    Ok(Grounded::<T>::new_internal(
        grounding,
        bindings,
        outcome.witt_bits,
        unit_address,
        content_fingerprint,
    ))
}

/// Construct an empty `BindingsTable`.
/// v0.2.2 T6.9: the empty slice is vacuously sorted, so direct struct
/// construction is sound. Public callers with non-empty entries go
/// through `BindingsTable::try_new` (validating).
/// # Driver contract
/// Every pipeline driver (`run`, `run_const`, `run_parallel`, `run_stream`,
/// `run_interactive`, `run_inhabitance`) mints `Grounded<T>` with this
/// empty table today: runtime-dynamic binding materialization in
/// `Grounded<T>` requires widening `BindingsTable.entries: &'static [...]`
/// to a non-`'static` carrier (a separate architectural change).
/// Downstream that needs a compile-time binding catalog uses the pattern
/// shown in `foundation/examples/static_bindings_catalog.rs`:
/// `Binding::to_binding_entry()` (const-fn) + `BindingsTable::try_new(&[...])`.
#[must_use]
pub const fn empty_bindings_table() -> BindingsTable {
    BindingsTable { entries: &[] }
}

// 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 — the pipeline does not mint this subclass
// directly; Phase D resolvers emit the canonical `GroundingCertificate` carrier
// and cert-subclass lifts happen in substrate-specific consumers.
#[allow(dead_code)]
const _COMPLETENESS_CERT_REF: Option<CompletenessCertificate> = None;

/// v0.2.2 Phase F / T2.7: parallel-declaration compile unit. Carries the
/// declared site partition cardinality plus (Phase A widening) the raw
/// partition slice and disjointness-witness IRI from the builder —
/// previously these were discarded at validate-time by a shadowed
/// enforcement-local `ParallelDeclaration` that nothing consumed.
/// v0.2.2 T6.11: also carries `result_type_iri` for ShapeMismatch detection.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct ParallelDeclaration<'a> {
    payload: u64,
    result_type_iri: &'static str,
    /// v0.2.2 Phase A: raw site-partition slice retained from the builder.
    /// Empty slice for declarations built via the site-count-only constructor.
    site_partition: &'a [u32],
    /// v0.2.2 Phase A: disjointness-witness IRI retained from the builder.
    /// Empty string for declarations built via the site-count-only constructor.
    disjointness_witness: &'a str,
    _sealed: (),
}

impl<'a> ParallelDeclaration<'a> {
    /// v0.2.2 Phase H3: construct a parallel declaration carrying the full
    /// partition slice and disjointness-witness IRI from the builder.
    /// This is the sole public constructor; the v0.2.2 Phase A site-count-only
    /// `new::<T>(site_count)` form was deleted in Phase H3 under the "no
    /// compatibility" discipline — every caller supplies a real partition.
    #[inline]
    #[must_use]
    pub const fn new_with_partition<T: ConstrainedTypeShape>(
        site_partition: &'a [u32],
        disjointness_witness: &'a str,
    ) -> Self {
        Self {
            payload: site_partition.len() as u64,
            result_type_iri: T::IRI,
            site_partition,
            disjointness_witness,
            _sealed: (),
        }
    }

    /// Returns the declared site partition cardinality.
    #[inline]
    #[must_use]
    pub const fn site_count(&self) -> u64 {
        self.payload
    }

    /// v0.2.2 T6.11: returns the result-type IRI.
    #[inline]
    #[must_use]
    pub const fn result_type_iri(&self) -> &'static str {
        self.result_type_iri
    }

    /// v0.2.2 Phase A: returns the raw site-partition slice.
    #[inline]
    #[must_use]
    pub const fn site_partition(&self) -> &'a [u32] {
        self.site_partition
    }

    /// v0.2.2 Phase A: returns the disjointness-witness IRI.
    #[inline]
    #[must_use]
    pub const fn disjointness_witness(&self) -> &'a str {
        self.disjointness_witness
    }
}

/// v0.2.2 Phase F / T2.7: stream-declaration compile unit. Carries a
/// payload field encoding the productivity-witness countdown.
/// v0.2.2 T6.11: also carries `result_type_iri` for ShapeMismatch detection.
/// v0.2.2 Phase A: also retains the builder's seed/step term slices and
/// the productivity-witness IRI so stream resolvers can walk declared
/// structure. Distinct from the enforcement-local `StreamDeclaration`
/// which records only the `StreamShape` validation surface.
/// Note: `Hash` is not derived because `Term` does not implement `Hash`;
/// downstream code that needs deterministic hashing should fold through
/// the substrate `Hasher` via the pipeline's `fold_stream_digest`.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct StreamDeclaration<'a> {
    payload: u64,
    result_type_iri: &'static str,
    /// v0.2.2 Phase A: stream seed term slice retained from the builder.
    seed: &'a [Term],
    /// v0.2.2 Phase A: stream step term slice retained from the builder.
    step: &'a [Term],
    /// v0.2.2 Phase A: productivity-witness IRI retained from the builder.
    productivity_witness: &'a str,
    _sealed: (),
}

impl<'a> StreamDeclaration<'a> {
    /// v0.2.2 T6.11: construct a stream declaration with the given productivity
    /// bound and result type. Phase A: leaves seed/step/witness empty; use
    /// `new_full` to retain the full structure.
    #[inline]
    #[must_use]
    pub const fn new<T: ConstrainedTypeShape>(
        productivity_bound: u64,
    ) -> StreamDeclaration<'static> {
        StreamDeclaration {
            payload: productivity_bound,
            result_type_iri: T::IRI,
            seed: &[],
            step: &[],
            productivity_witness: "",
            _sealed: (),
        }
    }

    /// v0.2.2 Phase A: construct a stream declaration carrying the full
    /// seed/step/witness structure from the builder.
    #[inline]
    #[must_use]
    pub const fn new_full<T: ConstrainedTypeShape>(
        productivity_bound: u64,
        seed: &'a [Term],
        step: &'a [Term],
        productivity_witness: &'a str,
    ) -> Self {
        Self {
            payload: productivity_bound,
            result_type_iri: T::IRI,
            seed,
            step,
            productivity_witness,
            _sealed: (),
        }
    }

    /// Returns the declared productivity bound.
    #[inline]
    #[must_use]
    pub const fn productivity_bound(&self) -> u64 {
        self.payload
    }

    /// v0.2.2 T6.11: returns the result-type IRI.
    #[inline]
    #[must_use]
    pub const fn result_type_iri(&self) -> &'static str {
        self.result_type_iri
    }

    /// v0.2.2 Phase A: returns the seed term slice.
    #[inline]
    #[must_use]
    pub const fn seed(&self) -> &'a [Term] {
        self.seed
    }

    /// v0.2.2 Phase A: returns the step term slice.
    #[inline]
    #[must_use]
    pub const fn step(&self) -> &'a [Term] {
        self.step
    }

    /// v0.2.2 Phase A: returns the productivity-witness IRI.
    #[inline]
    #[must_use]
    pub const fn productivity_witness(&self) -> &'a str {
        self.productivity_witness
    }
}

/// v0.2.2 Phase F / T2.7: interaction-declaration compile unit. Carries a
/// payload field encoding the convergence-predicate seed.
/// v0.2.2 T6.11: also carries `result_type_iri` for ShapeMismatch detection.
/// v0.2.2 Phase A: lifetime-parameterized for consistency with the other
/// widened runtime carriers. The interaction builder stores scalar fields
/// only, so there is no additional borrowed structure to retain; the `'a`
/// is vestigial but keeps the carrier signature uniform with
/// `ParallelDeclaration<'a>` and `StreamDeclaration<'a>`.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct InteractionDeclaration<'a> {
    payload: u64,
    result_type_iri: &'static str,
    _sealed: (),
    _lifetime: core::marker::PhantomData<&'a ()>,
}

impl<'a> InteractionDeclaration<'a> {
    /// v0.2.2 T6.11: construct an interaction declaration with the given
    /// convergence-predicate seed and result type.
    #[inline]
    #[must_use]
    pub const fn new<T: ConstrainedTypeShape>(
        convergence_seed: u64,
    ) -> InteractionDeclaration<'static> {
        InteractionDeclaration {
            payload: convergence_seed,
            result_type_iri: T::IRI,
            _sealed: (),
            _lifetime: core::marker::PhantomData,
        }
    }

    /// Returns the declared convergence seed.
    #[inline]
    #[must_use]
    pub const fn convergence_seed(&self) -> u64 {
        self.payload
    }

    /// v0.2.2 T6.11: returns the result-type IRI.
    #[inline]
    #[must_use]
    pub const fn result_type_iri(&self) -> &'static str {
        self.result_type_iri
    }
}

/// v0.2.2 Phase F: fixed-size inline payload buffer carried by `PeerInput`.
/// Sized for the largest `Datum<L>` the foundation supports at this release
/// (up to 32 u64 limbs = 2048 bits); smaller levels use the leading bytes.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct PeerPayload {
    words: [u64; 32],
    bit_width: u16,
    _sealed: (),
}

impl PeerPayload {
    /// Construct a zeroed payload of the given bit width.
    #[inline]
    #[must_use]
    pub const fn zero(bit_width: u16) -> Self {
        Self {
            words: [0u64; 32],
            bit_width,
            _sealed: (),
        }
    }

    /// Access the underlying limbs.
    #[inline]
    #[must_use]
    pub const fn words(&self) -> &[u64; 32] {
        &self.words
    }

    /// Bit width of the payload's logical Datum.
    #[inline]
    #[must_use]
    pub const fn bit_width(&self) -> u16 {
        self.bit_width
    }
}

/// v0.2.2 Phase F: a peer-supplied input to an interaction driver step.
/// Fixed-size — holds a `PeerPayload` inline plus the peer's content
/// address. No heap, no dynamic dispatch.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct PeerInput {
    peer_id: u128,
    payload: PeerPayload,
    _sealed: (),
}

impl PeerInput {
    /// Construct a new peer input with the given peer id and payload.
    #[inline]
    #[must_use]
    pub const fn new(peer_id: u128, payload: PeerPayload) -> Self {
        Self {
            peer_id,
            payload,
            _sealed: (),
        }
    }

    /// Access the peer id.
    #[inline]
    #[must_use]
    pub const fn peer_id(&self) -> u128 {
        self.peer_id
    }

    /// Access the payload.
    #[inline]
    #[must_use]
    pub const fn payload(&self) -> &PeerPayload {
        &self.payload
    }
}

/// v0.2.2 Phase F: outcome of a single `InteractionDriver::step` call.
#[derive(Debug, Clone)]
#[non_exhaustive]
pub enum StepResult<T: crate::enforcement::GroundedShape> {
    /// The step was absorbed; the driver is ready for another peer input.
    Continue,
    /// The step produced an intermediate grounded output.
    Output(Grounded<T>),
    /// The convergence predicate is satisfied; interaction is complete.
    Converged(Grounded<T>),
    /// v0.2.2 Phase T.1: the commutator norm failed to decrease for
    /// `INTERACTION_DIVERGENCE_BUDGET` consecutive steps — the interaction is
    /// non-convergent and the driver is no longer advanceable.
    Diverged,
    /// The step failed; the driver is no longer advanceable.
    Failure(PipelineFailure),
}

/// v0.2.2 Phase F: sealed commutator-algebra state carried by an
/// interaction driver across peer steps.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct CommutatorState<L> {
    accumulator: [u64; 4],
    _level: core::marker::PhantomData<L>,
    _sealed: (),
}

impl<L> CommutatorState<L> {
    /// Construct a zero commutator state.
    #[inline]
    #[must_use]
    pub const fn zero() -> Self {
        Self {
            accumulator: [0u64; 4],
            _level: core::marker::PhantomData,
            _sealed: (),
        }
    }

    /// Access the commutator accumulator words.
    #[inline]
    #[must_use]
    pub const fn accumulator(&self) -> &[u64; 4] {
        &self.accumulator
    }
}

/// v0.2.2 Phase F / T2.7: sealed iterator driver returned by `run_stream`.
/// Carries the productivity countdown initialized from the unit's
/// `StreamDeclaration::productivity_bound()`, plus a unit-derived address
/// seed for generating distinct `Grounded` outputs per step. Each call to
/// `next()` decrements the countdown and yields a `Grounded` whose
/// `unit_address` differs from the previous step's.
#[derive(Debug, Clone)]
pub struct StreamDriver<
    T: crate::enforcement::GroundedShape,
    P: crate::enforcement::ValidationPhase,
    H: crate::enforcement::Hasher,
> {
    rewrite_steps: u64,
    landauer_nats: u64,
    productivity_countdown: u64,
    seed: u64,
    result_type_iri: &'static str,
    terminated: bool,
    _shape: core::marker::PhantomData<T>,
    _phase: core::marker::PhantomData<P>,
    _hasher: core::marker::PhantomData<H>,
    _sealed: (),
}

impl<
        T: crate::enforcement::GroundedShape,
        P: crate::enforcement::ValidationPhase,
        H: crate::enforcement::Hasher,
    > StreamDriver<T, P, H>
{
    /// Crate-internal constructor. Callable only from `pipeline::run_stream`.
    #[inline]
    #[must_use]
    #[allow(dead_code)]
    pub(crate) const fn new_internal(
        productivity_bound: u64,
        seed: u64,
        result_type_iri: &'static str,
    ) -> Self {
        Self {
            rewrite_steps: 0,
            landauer_nats: 0,
            productivity_countdown: productivity_bound,
            seed,
            result_type_iri,
            terminated: false,
            _shape: core::marker::PhantomData,
            _phase: core::marker::PhantomData,
            _hasher: core::marker::PhantomData,
            _sealed: (),
        }
    }

    /// Total rewrite steps taken so far.
    #[inline]
    #[must_use]
    pub const fn rewrite_steps(&self) -> u64 {
        self.rewrite_steps
    }

    /// Total Landauer cost accumulated so far.
    #[inline]
    #[must_use]
    pub const fn landauer_nats(&self) -> u64 {
        self.landauer_nats
    }

    /// v0.2.2 T5.10: returns `true` once the driver has stopped producing
    /// rewrite steps. A terminated driver is observationally equivalent to
    /// one whose next `next()` call returns `None`. Use this when the driver
    /// is held inside a larger state machine that needs to decide whether
    /// to advance without consuming a step.
    /// Parallel to `InteractionDriver::is_converged()`.
    #[inline]
    #[must_use]
    pub const fn is_terminated(&self) -> bool {
        self.terminated
    }
}

impl<
        T: crate::enforcement::GroundedShape + ConstrainedTypeShape,
        P: crate::enforcement::ValidationPhase,
        H: crate::enforcement::Hasher,
    > Iterator for StreamDriver<T, P, H>
{
    type Item = Result<Grounded<T>, PipelineFailure>;
    fn next(&mut self) -> Option<Self::Item> {
        if self.terminated || self.productivity_countdown == 0 {
            self.terminated = true;
            return None;
        }
        // v0.2.2 T6.11: ShapeMismatch detection — first step only
        // (subsequent steps inherit the same result_type_iri).
        if self.rewrite_steps == 0 && !crate::enforcement::str_eq(self.result_type_iri, T::IRI) {
            self.terminated = true;
            return Some(Err(PipelineFailure::ShapeMismatch {
                expected: T::IRI,
                got: self.result_type_iri,
            }));
        }
        self.productivity_countdown -= 1;
        self.rewrite_steps += 1;
        self.landauer_nats += 1;
        // v0.2.2 T6.1: thread H: Hasher through fold_stream_step_digest
        // to compute a real per-step substrate fingerprint.
        let mut hasher = H::initial();
        hasher = crate::enforcement::fold_stream_step_digest(
            hasher,
            self.productivity_countdown,
            self.rewrite_steps,
            self.seed,
            self.result_type_iri,
            crate::enforcement::CertificateKind::Grounding,
        );
        let buffer = hasher.finalize();
        let content_fingerprint =
            crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
        let unit_address = crate::enforcement::unit_address_from_buffer(&buffer);
        let grounding = Validated::new(GroundingCertificate::with_level_and_fingerprint_const(
            32,
            content_fingerprint,
        ));
        let bindings = empty_bindings_table();
        Some(Ok(Grounded::<T>::new_internal(
            grounding,
            bindings,
            32, // default witt level for stream output
            unit_address,
            content_fingerprint,
        )))
    }
}

/// v0.2.2 Phase F / T2.7: sealed state-machine driver returned by
/// `run_interactive`. Exposes `step(PeerInput)`, `is_converged()`, and
/// `finalize()`. The driver folds each peer input into its
/// `commutator_acc` accumulator via XOR; convergence is signalled when
/// a peer input arrives with `peer_id == 0` (the closing handshake).
#[derive(Debug, Clone)]
pub struct InteractionDriver<
    T: crate::enforcement::GroundedShape,
    P: crate::enforcement::ValidationPhase,
    H: crate::enforcement::Hasher,
> {
    commutator_acc: [u64; 4],
    peer_step_count: u64,
    converged: bool,
    /// Convergence seed read from the source InteractionDeclaration.
    /// Available via `seed()` for downstream inspection.
    seed: u64,
    /// v0.2.2 Phase T.1: previous step's commutator norm (Euclidean-squared
    /// over the 4 u64 limbs, saturating). Used to detect divergence.
    prev_commutator_norm: u64,
    /// v0.2.2 Phase T.1: count of consecutive non-decreasing norm steps.
    /// Reset to 0 on any decrease; divergence triggers at `DIVERGENCE_BUDGET`.
    consecutive_non_decreasing: u32,
    /// v0.2.2 T6.11: result-type IRI from the source InteractionDeclaration.
    result_type_iri: &'static str,
    _shape: core::marker::PhantomData<T>,
    _phase: core::marker::PhantomData<P>,
    _hasher: core::marker::PhantomData<H>,
    _sealed: (),
}

/// v0.2.2 Phase T.1: divergence budget — max consecutive non-decreasing commutator-norm
/// steps before the interaction driver fails. Foundation-canonical; override at the
/// `InteractionDeclaration` level not supported in this release.
pub const INTERACTION_DIVERGENCE_BUDGET: u32 = 16;

impl<
        T: crate::enforcement::GroundedShape,
        P: crate::enforcement::ValidationPhase,
        H: crate::enforcement::Hasher,
    > InteractionDriver<T, P, H>
{
    /// Crate-internal constructor. Callable only from `pipeline::run_interactive`.
    #[inline]
    #[must_use]
    #[allow(dead_code)]
    pub(crate) const fn new_internal(seed: u64, result_type_iri: &'static str) -> Self {
        // Initial commutator seeded from the unit's convergence seed.
        Self {
            commutator_acc: [seed, 0, 0, 0],
            peer_step_count: 0,
            converged: false,
            seed,
            // Initial norm = seed² (saturating) so the first step can only
            // decrease the norm via peer input (which is the convergence path).
            prev_commutator_norm: seed.saturating_mul(seed),
            consecutive_non_decreasing: 0,
            result_type_iri,
            _shape: core::marker::PhantomData,
            _phase: core::marker::PhantomData,
            _hasher: core::marker::PhantomData,
            _sealed: (),
        }
    }

    /// v0.2.2 Phase T.1: convergence threshold derived from the seed. Termination
    /// triggers when the commutator norm falls below this value. Foundation-canonical:
    /// `seed.rotate_right(32) ^ 0xDEADBEEF_CAFEBABE`.
    #[inline]
    #[must_use]
    pub const fn convergence_threshold(&self) -> u64 {
        self.seed.rotate_right(32) ^ 0xDEAD_BEEF_CAFE_BABE
    }

    /// Advance the driver by folding in a single peer input (v0.2.2 Phase T.1).
    /// Each step XOR-folds the peer payload's first 4 limbs into the
    /// commutator accumulator, then recomputes the Euclidean-squared
    /// norm over the 4 limbs (saturating `u64`). Termination rules:
    /// * **Converged** if the norm falls below `convergence_threshold()`,
    ///   OR if `peer_id == 0` (explicit closing handshake).
    /// * **Diverged** (via `PipelineFailure::ConvergenceStall`) if the norm is
    ///   non-decreasing for `INTERACTION_DIVERGENCE_BUDGET` consecutive steps.
    /// * **Continue** otherwise.
    #[must_use]
    pub fn step(&mut self, input: PeerInput) -> StepResult<T>
    where
        T: ConstrainedTypeShape,
    {
        self.peer_step_count += 1;
        // Fold the first 4 payload words into the accumulator.
        let words = input.payload().words();
        let mut i = 0usize;
        while i < 4 {
            self.commutator_acc[i] ^= words[i];
            i += 1;
        }
        // v0.2.2 Phase T.1: compute the Euclidean-squared norm over the 4 limbs.
        let mut norm: u64 = 0;
        let mut j = 0usize;
        while j < 4 {
            let limb = self.commutator_acc[j];
            norm = norm.saturating_add(limb.saturating_mul(limb));
            j += 1;
        }
        let threshold = self.convergence_threshold();
        // v0.2.2 Phase T.1: convergence on norm-below-threshold OR explicit
        // handshake (peer_id == 0). Divergence on consecutive non-decreasing norm.
        let norm_converged = norm < threshold;
        let handshake_close = input.peer_id() == 0;
        if norm_converged || handshake_close {
            self.converged = true;
            // v0.2.2 T6.1: thread H: Hasher through fold_interaction_step_digest
            // to compute a real convergence-time substrate fingerprint.
            let mut hasher = H::initial();
            hasher = crate::enforcement::fold_interaction_step_digest(
                hasher,
                &self.commutator_acc,
                self.peer_step_count,
                self.seed,
                self.result_type_iri,
                crate::enforcement::CertificateKind::Grounding,
            );
            let buffer = hasher.finalize();
            let content_fingerprint =
                crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
            let unit_address = crate::enforcement::unit_address_from_buffer(&buffer);
            let grounding = Validated::new(GroundingCertificate::with_level_and_fingerprint_const(
                32,
                content_fingerprint,
            ));
            let bindings = empty_bindings_table();
            return StepResult::Converged(Grounded::<T>::new_internal(
                grounding,
                bindings,
                32,
                unit_address,
                content_fingerprint,
            ));
        }
        // v0.2.2 Phase T.1: divergence detection — count consecutive
        // non-decreasing norm steps. Reset on any decrease.
        if norm >= self.prev_commutator_norm {
            self.consecutive_non_decreasing = self.consecutive_non_decreasing.saturating_add(1);
        } else {
            self.consecutive_non_decreasing = 0;
        }
        self.prev_commutator_norm = norm;
        if self.consecutive_non_decreasing >= INTERACTION_DIVERGENCE_BUDGET {
            return StepResult::Diverged;
        }
        StepResult::Continue
    }

    /// Whether the driver has reached the convergence predicate.
    #[inline]
    #[must_use]
    pub const fn is_converged(&self) -> bool {
        self.converged
    }

    /// Number of peer steps applied so far.
    #[inline]
    #[must_use]
    pub const fn peer_step_count(&self) -> u64 {
        self.peer_step_count
    }

    /// Convergence seed inherited from the source InteractionDeclaration.
    #[inline]
    #[must_use]
    pub const fn seed(&self) -> u64 {
        self.seed
    }

    /// Finalize the interaction, producing a grounded result.
    /// Returns a `Grounded<T>` whose `unit_address` is a hash of the
    /// accumulated commutator state, so two interaction drivers that
    /// processed different peer inputs return distinct grounded values.
    /// # Errors
    /// Returns a `PipelineFailure::ShapeViolation` if the driver has
    /// not converged, or `PipelineFailure::ShapeMismatch` if the source
    /// declaration's result_type_iri does not match `T::IRI`.
    pub fn finalize(self) -> Result<Grounded<T>, PipelineFailure>
    where
        T: ConstrainedTypeShape,
    {
        // v0.2.2 T6.11: ShapeMismatch detection.
        if !crate::enforcement::str_eq(self.result_type_iri, T::IRI) {
            return Err(PipelineFailure::ShapeMismatch {
                expected: T::IRI,
                got: self.result_type_iri,
            });
        }
        if !self.converged {
            return Err(PipelineFailure::ShapeViolation {
                report: ShapeViolation {
                    shape_iri: "https://uor.foundation/conformance/InteractionShape",
                    constraint_iri:
                        "https://uor.foundation/conformance/InteractionShape#convergence",
                    property_iri: "https://uor.foundation/conformance/convergencePredicate",
                    expected_range: "http://www.w3.org/2002/07/owl#Thing",
                    min_count: 1,
                    max_count: 1,
                    kind: ViolationKind::Missing,
                },
            });
        }
        // v0.2.2 T6.1: thread H: Hasher through fold_interaction_step_digest.
        let mut hasher = H::initial();
        hasher = crate::enforcement::fold_interaction_step_digest(
            hasher,
            &self.commutator_acc,
            self.peer_step_count,
            self.seed,
            self.result_type_iri,
            crate::enforcement::CertificateKind::Grounding,
        );
        let buffer = hasher.finalize();
        let content_fingerprint =
            crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
        let unit_address = crate::enforcement::unit_address_from_buffer(&buffer);
        let grounding = Validated::new(GroundingCertificate::with_level_and_fingerprint_const(
            32,
            content_fingerprint,
        ));
        let bindings = empty_bindings_table();
        Ok(Grounded::<T>::new_internal(
            grounding,
            bindings,
            32,
            unit_address,
            content_fingerprint,
        ))
    }
}

/// v0.2.2 Phase F / T2.7: parallel driver entry point.
/// Consumes a `Validated<ParallelDeclaration, P>` and produces a unified
/// `Grounded<T>` whose `unit_address` is derived from the declaration's
/// site count via FNV-1a. Two units with different site counts produce
/// `Grounded` values with different addresses.
/// # Errors
/// Returns `PipelineFailure::ShapeMismatch` when the declaration's
/// `result_type_iri` does not match `T::IRI` — the caller asked for
/// `Grounded<T>` but the declaration was built over a different shape.
/// Returns `PipelineFailure::ContradictionDetected` when the declared
/// partition cardinality is zero — a parallel composition with no
/// sites is inadmissible by construction.
/// Success: `run_parallel` folds the declaration's site count through
/// `fold_parallel_digest` to produce a content fingerprint; distinct
/// partitions produce distinct fingerprints by construction.
/// # Example
/// ```no_run
/// use uor_foundation::enforcement::{ConstrainedTypeInput, Validated};
/// use uor_foundation::pipeline::{run_parallel, ParallelDeclaration};
/// # use uor_foundation::enforcement::Hasher;
/// # struct Fnv1aHasher16;
/// # impl Hasher for Fnv1aHasher16 {
/// #     const OUTPUT_BYTES: usize = 16;
/// #     fn initial() -> Self { Self }
/// #     fn fold_byte(self, _: u8) -> Self { self }
/// #     fn finalize(self) -> [u8; 32] { [0; 32] }
/// # }
/// # fn wrap<T>(t: T) -> Validated<T> { unimplemented!() /* see uor_foundation_test_helpers */ }
/// // 3-component partition over 9 sites.
/// static PARTITION: &[u32] = &[0, 0, 0, 1, 1, 1, 2, 2, 2];
/// let decl: Validated<ParallelDeclaration> = wrap(
///     ParallelDeclaration::new_with_partition::<ConstrainedTypeInput>(
///         PARTITION,
///         "https://uor.foundation/parallel/ParallelDisjointnessWitness",
///     ),
/// );
/// let grounded = run_parallel::<ConstrainedTypeInput, _, Fnv1aHasher16>(decl)
///     .expect("partition admits");
/// # let _ = grounded;
/// ```
pub fn run_parallel<T, P, H>(
    unit: Validated<ParallelDeclaration, P>,
) -> Result<Grounded<T>, PipelineFailure>
where
    T: ConstrainedTypeShape + crate::enforcement::GroundedShape,
    P: crate::enforcement::ValidationPhase,
    H: crate::enforcement::Hasher,
{
    let decl = unit.inner();
    let site_count = decl.site_count();
    let partition = decl.site_partition();
    let witness_iri = decl.disjointness_witness();
    // Runtime invariants declared in the ParallelDeclaration rustdoc:
    // (1) result_type_iri must match T::IRI (target §5 + T6.11);
    // (2) site_count > 0 (zero-site parallel composition is vacuous);
    // (3) v0.2.2 Phase H3: partition length must equal site_count;
    // (4) v0.2.2 Phase H3: partition must be non-empty (only constructor is
    //     `new_with_partition`, which takes a real partition slice).
    if !crate::enforcement::str_eq(decl.result_type_iri(), T::IRI) {
        return Err(PipelineFailure::ShapeMismatch {
            expected: T::IRI,
            got: decl.result_type_iri(),
        });
    }
    if site_count == 0 || partition.is_empty() {
        return Err(PipelineFailure::ContradictionDetected {
            at_step: 0,
            trace_iri: "https://uor.foundation/parallel/ParallelProduct",
        });
    }
    if partition.len() as u64 != site_count {
        return Err(PipelineFailure::ShapeMismatch {
            expected: T::IRI,
            got: decl.result_type_iri(),
        });
    }
    // v0.2.2 Phase H3: walk partition, count sites per component, fold
    // per-component into the content fingerprint. Enumerates unique component
    // IDs into a fixed stack buffer sized by WITT_MAX_BITS.
    let mut hasher = H::initial();
    // component_ids: seen component IDs in first-appearance order.
    // component_counts: parallel site-count per component.
    let mut component_ids = [0u32; WITT_MAX_BITS as usize];
    let mut component_counts = [0u32; WITT_MAX_BITS as usize];
    let mut n_components: usize = 0;
    let mut si = 0;
    while si < partition.len() {
        let cid = partition[si];
        // Find or insert cid.
        let mut ci = 0;
        let mut found = false;
        while ci < n_components {
            if component_ids[ci] == cid {
                component_counts[ci] = component_counts[ci].saturating_add(1);
                found = true;
                break;
            }
            ci += 1;
        }
        if !found && n_components < (WITT_MAX_BITS as usize) {
            component_ids[n_components] = cid;
            component_counts[n_components] = 1;
            n_components += 1;
        }
        si += 1;
    }
    // Fold each component: (component_id, site_count_within) in first-appearance order.
    let mut ci = 0;
    while ci < n_components {
        hasher = hasher.fold_bytes(&component_ids[ci].to_be_bytes());
        hasher = hasher.fold_bytes(&component_counts[ci].to_be_bytes());
        ci += 1;
    }
    // Fold disjointness_witness IRI so forgeries yield distinct content fingerprints.
    hasher = hasher.fold_bytes(witness_iri.as_bytes());
    hasher = hasher.fold_byte(0);
    // Canonical ParallelDeclaration tail: site_count + type shape + cert kind.
    hasher = crate::enforcement::fold_parallel_digest(
        hasher,
        site_count,
        T::IRI,
        T::SITE_COUNT,
        T::CONSTRAINTS,
        crate::enforcement::CertificateKind::Grounding,
    );
    let buffer = hasher.finalize();
    let content_fingerprint =
        crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
    let unit_address = crate::enforcement::unit_address_from_buffer(&buffer);
    let grounding = Validated::new(GroundingCertificate::with_level_and_fingerprint_const(
        32,
        content_fingerprint,
    ));
    let bindings = empty_bindings_table();
    Ok(Grounded::<T>::new_internal(
        grounding,
        bindings,
        32,
        unit_address,
        content_fingerprint,
    ))
}

/// v0.2.2 Phase F / T2.7: stream driver entry point.
/// Consumes a `Validated<StreamDeclaration, P>` and returns a
/// `StreamDriver<T, P>` implementing `Iterator`. The driver's productivity
/// countdown is initialized from `StreamDeclaration::productivity_bound()`;
/// each `next()` call yields a `Grounded` whose `unit_address` differs
/// from the previous step's, and the iterator terminates when the
/// countdown reaches zero.
#[must_use]
pub fn run_stream<T, P, H>(unit: Validated<StreamDeclaration, P>) -> StreamDriver<T, P, H>
where
    T: crate::enforcement::GroundedShape,
    P: crate::enforcement::ValidationPhase,
    H: crate::enforcement::Hasher,
{
    let bound = unit.inner().productivity_bound();
    let result_type_iri = unit.inner().result_type_iri();
    StreamDriver::new_internal(bound, bound, result_type_iri)
}

/// v0.2.2 Phase F / T2.7: interaction driver entry point.
/// Consumes a `Validated<InteractionDeclaration, P>` and returns an
/// `InteractionDriver<T, P, H>` state machine seeded from the declaration's
/// `convergence_seed()`. Advance with `step(PeerInput)` until
/// `is_converged()` returns `true`, then call `finalize()`.
#[must_use]
pub fn run_interactive<T, P, H>(
    unit: Validated<InteractionDeclaration, P>,
) -> InteractionDriver<T, P, H>
where
    T: crate::enforcement::GroundedShape,
    P: crate::enforcement::ValidationPhase,
    H: crate::enforcement::Hasher,
{
    InteractionDriver::new_internal(
        unit.inner().convergence_seed(),
        unit.inner().result_type_iri(),
    )
}

/// v0.2.2 Phase G / T2.8: const-fn companion for
/// `LeaseDeclarationBuilder`. Delegates to the builder's
/// `validate_const` method, which validates the `LeaseShape` contract
/// (`linear_site` and `scope` required) at compile time.
/// # Errors
/// Returns `ShapeViolation::Missing` if `linear_site` or `scope` is unset.
pub const fn validate_lease_const<'a>(
    builder: &LeaseDeclarationBuilder<'a>,
) -> Result<Validated<LeaseDeclaration, CompileTime>, ShapeViolation> {
    builder.validate_const()
}

/// v0.2.2 Phase G / T2.8 + T6.13: const-fn companion for `CompileUnitBuilder`.
///
/// Tightened in T6.13 to enforce the same five required fields as the
/// runtime `CompileUnitBuilder::validate()` method:
///
/// - `root_term`
/// - `witt_level_ceiling`
/// - `thermodynamic_budget`
/// - `target_domains` (non-empty)
/// - `result_type_iri`
///
/// Returns `Result<Validated<CompileUnit, CompileTime>, ShapeViolation>` —
/// dual-path consistent with the runtime `validate()` method. Const-eval
/// call sites match on the `Result`; the panic only fires at codegen /
/// const-eval time, never at runtime.
///
/// # Errors
///
/// Returns `ShapeViolation::Missing` for the first unset required field.
pub const fn validate_compile_unit_const<'a>(
    builder: &CompileUnitBuilder<'a>,
) -> Result<Validated<CompileUnit<'a>, CompileTime>, ShapeViolation> {
    if !builder.has_root_term_const() {
        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::Missing,
        });
    }
    let level = match builder.witt_level_option() {
        Some(l) => l,
        None => {
            return Err(ShapeViolation {
                shape_iri: "https://uor.foundation/conformance/CompileUnitShape",
                constraint_iri:
                    "https://uor.foundation/conformance/compileUnit_unitWittLevel_constraint",
                property_iri: "https://uor.foundation/reduction/unitWittLevel",
                expected_range: "https://uor.foundation/schema/WittLevel",
                min_count: 1,
                max_count: 1,
                kind: ViolationKind::Missing,
            })
        }
    };
    let budget =
        match builder.budget_option() {
            Some(b) => b,
            None => return 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::Missing,
            }),
        };
    if !builder.has_target_domains_const() {
        return Err(ShapeViolation {
            shape_iri: "https://uor.foundation/conformance/CompileUnitShape",
            constraint_iri:
                "https://uor.foundation/conformance/compileUnit_targetDomains_constraint",
            property_iri: "https://uor.foundation/reduction/targetDomains",
            expected_range: "https://uor.foundation/op/VerificationDomain",
            min_count: 1,
            max_count: 0,
            kind: ViolationKind::Missing,
        });
    }
    let result_type_iri = match builder.result_type_iri_const() {
        Some(iri) => iri,
        None => {
            return Err(ShapeViolation {
                shape_iri: "https://uor.foundation/conformance/CompileUnitShape",
                constraint_iri:
                    "https://uor.foundation/conformance/compileUnit_resultType_constraint",
                property_iri: "https://uor.foundation/reduction/resultType",
                expected_range: "https://uor.foundation/type/ConstrainedType",
                min_count: 1,
                max_count: 1,
                kind: ViolationKind::Missing,
            })
        }
    };
    Ok(Validated::new(CompileUnit::from_parts_const(
        level,
        budget,
        result_type_iri,
        builder.root_term_slice_const(),
        builder.bindings_slice_const(),
        builder.target_domains_slice_const(),
    )))
}

/// v0.2.2 Phase G / T2.8 + T6.11: const-fn companion for
/// `ParallelDeclarationBuilder`. Takes a `ConstrainedTypeShape` type parameter
/// to set the `result_type_iri` on the produced declaration.
/// v0.2.2 Phase A: the produced `ParallelDeclaration<'a>` carries the
/// builder's raw site-partition slice and disjointness-witness IRI; the
/// lifetime `'a` is the builder's borrow lifetime.
#[must_use]
pub const fn validate_parallel_const<'a, T: ConstrainedTypeShape>(
    builder: &ParallelDeclarationBuilder<'a>,
) -> Validated<ParallelDeclaration<'a>, CompileTime> {
    Validated::new(ParallelDeclaration::new_with_partition::<T>(
        builder.site_partition_slice_const(),
        builder.disjointness_witness_const(),
    ))
}

/// v0.2.2 Phase G / T2.8 + T6.11: const-fn companion for
/// `StreamDeclarationBuilder`. Takes a `ConstrainedTypeShape` type parameter
/// to set the `result_type_iri` on the produced declaration.
/// v0.2.2 Phase A: the produced `StreamDeclaration<'a>` retains the
/// builder's seed/step term slices and productivity-witness IRI.
#[must_use]
pub const fn validate_stream_const<'a, T: ConstrainedTypeShape>(
    builder: &StreamDeclarationBuilder<'a>,
) -> Validated<StreamDeclaration<'a>, CompileTime> {
    let bound = builder.productivity_bound_const();
    Validated::new(StreamDeclaration::new_full::<T>(
        bound,
        builder.seed_slice_const(),
        builder.step_slice_const(),
        builder.productivity_witness_const(),
    ))
}

/// v0.2.2 T5 C6: const-fn resolver companion for
/// `tower_completeness::certify`. Threads the consumer-supplied substrate
/// `Hasher` through the canonical CompileUnit byte layout to compute a
/// parametric content fingerprint, distinguishing two units that share a
/// witt level but differ in budget, IRI, site count, or constraints.
#[must_use]
pub fn certify_tower_completeness_const<T, H>(
    unit: &Validated<CompileUnit, CompileTime>,
) -> Validated<GroundingCertificate, CompileTime>
where
    T: ConstrainedTypeShape,
    H: crate::enforcement::Hasher,
{
    let level_bits = unit.inner().witt_level().witt_length() as u16;
    let budget = unit.inner().thermodynamic_budget();
    let mut hasher = H::initial();
    hasher = crate::enforcement::fold_unit_digest(
        hasher,
        level_bits,
        budget,
        T::IRI,
        T::SITE_COUNT,
        T::CONSTRAINTS,
        crate::enforcement::CertificateKind::TowerCompleteness,
    );
    let buffer = hasher.finalize();
    let fp = crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
    Validated::new(GroundingCertificate::with_level_and_fingerprint_const(
        level_bits, fp,
    ))
}

/// v0.2.2 T5 C6: const-fn resolver companion for
/// `incremental_completeness::certify`. Threads `H: Hasher` for the
/// parametric fingerprint; uses `CertificateKind::IncrementalCompleteness`
/// as the trailing discriminant byte.
#[must_use]
pub fn certify_incremental_completeness_const<T, H>(
    unit: &Validated<CompileUnit, CompileTime>,
) -> Validated<GroundingCertificate, CompileTime>
where
    T: ConstrainedTypeShape,
    H: crate::enforcement::Hasher,
{
    let level_bits = unit.inner().witt_level().witt_length() as u16;
    let budget = unit.inner().thermodynamic_budget();
    let mut hasher = H::initial();
    hasher = crate::enforcement::fold_unit_digest(
        hasher,
        level_bits,
        budget,
        T::IRI,
        T::SITE_COUNT,
        T::CONSTRAINTS,
        crate::enforcement::CertificateKind::IncrementalCompleteness,
    );
    let buffer = hasher.finalize();
    let fp = crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
    Validated::new(GroundingCertificate::with_level_and_fingerprint_const(
        level_bits, fp,
    ))
}

/// v0.2.2 T5 C6: const-fn resolver companion for `inhabitance::certify`.
/// Threads `H: Hasher` for the parametric fingerprint; uses
/// `CertificateKind::Inhabitance` as the trailing discriminant byte.
#[must_use]
pub fn certify_inhabitance_const<T, H>(
    unit: &Validated<CompileUnit, CompileTime>,
) -> Validated<GroundingCertificate, CompileTime>
where
    T: ConstrainedTypeShape,
    H: crate::enforcement::Hasher,
{
    let level_bits = unit.inner().witt_level().witt_length() as u16;
    let budget = unit.inner().thermodynamic_budget();
    let mut hasher = H::initial();
    hasher = crate::enforcement::fold_unit_digest(
        hasher,
        level_bits,
        budget,
        T::IRI,
        T::SITE_COUNT,
        T::CONSTRAINTS,
        crate::enforcement::CertificateKind::Inhabitance,
    );
    let buffer = hasher.finalize();
    let fp = crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
    Validated::new(GroundingCertificate::with_level_and_fingerprint_const(
        level_bits, fp,
    ))
}

/// v0.2.2 T5 C6: const-fn resolver companion for
/// `multiplication::certify`. Threads `H: Hasher` for the parametric
/// fingerprint; uses `CertificateKind::Multiplication` as the trailing
/// discriminant byte.
#[must_use]
pub fn certify_multiplication_const<T, H>(
    unit: &Validated<CompileUnit, CompileTime>,
) -> Validated<MultiplicationCertificate, CompileTime>
where
    T: ConstrainedTypeShape,
    H: crate::enforcement::Hasher,
{
    let level_bits = unit.inner().witt_level().witt_length() as u16;
    let budget = unit.inner().thermodynamic_budget();
    let mut hasher = H::initial();
    hasher = crate::enforcement::fold_unit_digest(
        hasher,
        level_bits,
        budget,
        T::IRI,
        T::SITE_COUNT,
        T::CONSTRAINTS,
        crate::enforcement::CertificateKind::Multiplication,
    );
    let buffer = hasher.finalize();
    let fp = crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
    Validated::new(MultiplicationCertificate::with_level_and_fingerprint_const(
        level_bits, fp,
    ))
}

/// Phase C.4: const-fn resolver companion for `grounding_aware::certify`.
/// Threads `H: Hasher` for the parametric fingerprint; uses
/// `CertificateKind::Grounding` as the trailing discriminant byte.
#[must_use]
pub fn certify_grounding_aware_const<T, H>(
    unit: &Validated<CompileUnit, CompileTime>,
) -> Validated<GroundingCertificate, CompileTime>
where
    T: ConstrainedTypeShape,
    H: crate::enforcement::Hasher,
{
    let level_bits = unit.inner().witt_level().witt_length() as u16;
    let budget = unit.inner().thermodynamic_budget();
    let mut hasher = H::initial();
    hasher = crate::enforcement::fold_unit_digest(
        hasher,
        level_bits,
        budget,
        T::IRI,
        T::SITE_COUNT,
        T::CONSTRAINTS,
        crate::enforcement::CertificateKind::Grounding,
    );
    let buffer = hasher.finalize();
    let fp = crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
    Validated::new(GroundingCertificate::with_level_and_fingerprint_const(
        level_bits, fp,
    ))
}

/// v0.2.2 T5 C6: typed pipeline entry point producing `Grounded<T>` from
/// a validated `CompileUnit`. Threads the consumer-supplied substrate
/// `Hasher` through `fold_unit_digest` to compute a parametric content
/// fingerprint over the unit's full state: `(level_bits, budget, T::IRI,
/// T::SITE_COUNT, T::CONSTRAINTS, CertificateKind::Grounding)`.
/// Two units differing on **any** of those fields produce `Grounded`
/// values with distinct fingerprints (and distinct `unit_address` handles,
/// derived from the leading 16 bytes of the fingerprint).
/// # Errors
/// Returns `PipelineFailure::ShapeMismatch` when the unit's declared
/// `result_type_iri` does not match `T::IRI`, or propagates any
/// failure from the reduction stage executor.
pub fn run_const<T, M, H>(
    unit: &Validated<CompileUnit, CompileTime>,
) -> Result<Grounded<T>, PipelineFailure>
where
    T: ConstrainedTypeShape + crate::enforcement::GroundedShape,
    // Phase C.2 (target §6): const-eval admits only those grounding-map kinds
    // that are both Total (defined for all inputs) and Invertible (one-to-one).
    // The bound is enforced at the type level via the existing marker tower.
    M: crate::enforcement::GroundingMapKind
        + crate::enforcement::Total
        + crate::enforcement::Invertible,
    H: crate::enforcement::Hasher,
{
    // The marker bound on M is purely type-level — no runtime use.
    let _phantom_map: core::marker::PhantomData<M> = core::marker::PhantomData;
    let level_bits = unit.inner().witt_level().witt_length() as u16;
    let budget = unit.inner().thermodynamic_budget();
    // v0.2.2 T6.11: ShapeMismatch detection. The unit declares its
    // result_type_iri at validation time; the caller's `T::IRI` must match.
    let unit_iri = unit.inner().result_type_iri();
    if !crate::enforcement::str_eq(unit_iri, T::IRI) {
        return Err(PipelineFailure::ShapeMismatch {
            expected: T::IRI,
            got: unit_iri,
        });
    }
    // Walk the foundation-locked byte layout via the consumer's hasher.
    let mut hasher = H::initial();
    hasher = crate::enforcement::fold_unit_digest(
        hasher,
        level_bits,
        budget,
        T::IRI,
        T::SITE_COUNT,
        T::CONSTRAINTS,
        crate::enforcement::CertificateKind::Grounding,
    );
    let buffer = hasher.finalize();
    let content_fingerprint =
        crate::enforcement::ContentFingerprint::from_buffer(buffer, H::OUTPUT_BYTES as u8);
    let unit_address = crate::enforcement::unit_address_from_buffer(&buffer);
    let grounding = Validated::new(GroundingCertificate::with_level_and_fingerprint_const(
        level_bits,
        content_fingerprint,
    ));
    let bindings = empty_bindings_table();
    Ok(Grounded::<T>::new_internal(
        grounding,
        bindings,
        level_bits,
        unit_address,
        content_fingerprint,
    ))
}