uor-foundation-sdk 0.3.4

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

//! UOR Foundation SDK — procedural-macro ergonomics for `uor-foundation`.
//!
//! Emitted by `codegen/src/sdk_macros.rs` from the ontology. Consumers of
//! this crate must also depend on `uor-foundation`; the macros emit
//! absolute-path references (`::uor_foundation::…`) that resolve in the
//! *consumer's* dependency graph.
//!
//! # Macros
//!
//! - [`product_shape!`] — emits a `ConstrainedTypeShape` impl and a
//!   `mint_product_witness` helper for the UOR product type `A × B`
//!   (PT_1 / PT_2a / PT_3 / PT_4).
//! - [`coproduct_shape!`] — emits a `ConstrainedTypeShape` impl and a
//!   `mint_coproduct_witness` helper for the UOR sum type `A + B`
//!   (ST_1 / ST_2 / ST_6 / ST_7 / ST_8 / ST_9 / ST_10).
//! - [`cartesian_product_shape!`] — emits a `ConstrainedTypeShape` impl,
//!   a `CartesianProductShape` marker impl, and a `mint_cartesian_witness`
//!   helper for the UOR Cartesian-partition product `A ⊠ B`
//!   (CPT_1 / CPT_2a / CPT_3 / CPT_4 / CPT_5).
//! - [`prism_model!`] — emits the seal impls (`__sdk_seal::Sealed` for
//!   the model and the route witness), the `FoundationClosed` impl on
//!   the route witness, and the `PrismModel<H, B, A>` impl whose
//!   `forward` body delegates to `pipeline::run_route` (wiki ADR-020 +
//!   ADR-022 D1, D3, D4, D5).
//!
//! # Operand support
//!
//! Operand `CONSTRAINTS` arrays may contain every `ConstraintRef`
//! variant: `Residue`, `Hamming`, `Depth`, `Carry`, `Site`, `Affine`,
//! `SatClauses`, `Bound`, and `Conjunction`. Phase 17 stores
//! `Affine.coefficients` as a fixed-size
//! `[i64; AFFINE_MAX_COEFFS]` array (capacity 8) and limits
//! `Conjunction.conjuncts` to a `[LeafConstraintRef; CONJUNCTION_MAX_TERMS]`
//! depth-1 array; both are stable-Rust const-buildable, so the SDK
//! macros support the full operand catalogue. Inputs exceeding the
//! caps fail `validate_const()` with a typed `ShapeViolation`.

#![deny(
    clippy::unwrap_used,
    clippy::expect_used,
    clippy::panic,
    missing_docs,
    clippy::missing_errors_doc
)]

use proc_macro::TokenStream;
use quote::quote;
use syn::parse::{Parse, ParseStream};
use syn::{parse_macro_input, Ident, Result, Token};

/// Callsite input for `product_shape!(Name, A, B)` — three identifier
/// tokens separated by commas.
struct ShapeArgs {
    name: Ident,
    left: Ident,
    right: Ident,
}

impl Parse for ShapeArgs {
    fn parse(input: ParseStream) -> Result<Self> {
        let name: Ident = input.parse()?;
        input.parse::<Token![,]>()?;
        let left: Ident = input.parse()?;
        input.parse::<Token![,]>()?;
        let right: Ident = input.parse()?;
        // Trailing comma permitted for consistency with Rust style.
        let _ = input.parse::<Token![,]>();
        Ok(Self { name, left, right })
    }
}

/// Product-type shape constructor. See crate-level docs.
///
/// # Example
///
/// ```
/// use uor_foundation::pipeline::{ConstrainedTypeShape, ConstraintRef};
/// use uor_foundation_sdk::product_shape;
///
/// pub struct A;
/// impl ConstrainedTypeShape for A {
///     const IRI: &'static str = "https://example.org/A";
///     const SITE_COUNT: usize = 1;
///     const CONSTRAINTS: &'static [ConstraintRef] = &[
///         ConstraintRef::Residue { modulus: 7, residue: 3 },
///     ];
/// }
///
/// pub struct B;
/// impl ConstrainedTypeShape for B {
///     const IRI: &'static str = "https://example.org/B";
///     const SITE_COUNT: usize = 1;
///     const CONSTRAINTS: &'static [ConstraintRef] = &[
///         ConstraintRef::Hamming { bound: 1 },
///     ];
/// }
///
/// product_shape!(MyProduct, A, B);
///
/// assert!(<MyProduct as ConstrainedTypeShape>::IRI.starts_with("urn:uor:product:"));
/// assert_eq!(<MyProduct as ConstrainedTypeShape>::SITE_COUNT, 2);
/// ```
#[proc_macro]
pub fn product_shape(input: TokenStream) -> TokenStream {
    let ShapeArgs { name, left, right } = parse_macro_input!(input as ShapeArgs);
    let iri = format!(
        "urn:uor:product:{}:{}",
        lexically_earlier(&left, &right),
        lexically_later(&left, &right)
    );
    // Canonicalize operand ordering by stable token spelling so
    // `product_shape!(X, A, B)` and `product_shape!(X, B, A)` emit
    // identical source. Documented as the §4e canonicalization rule the
    // SDK enforces — the runtime content-fingerprint match §4e describes
    // is then checked by consumer tests.
    let (l, r) = canonical_operand_pair(&left, &right);
    let raw_const = format_ident_suffix(&name, "__CONSTRAINTS_RAW");
    let len_const = format_ident_suffix(&name, "__CONSTRAINTS_LEN");

    let expansion = quote! {
        /// UOR ProductType shape, emitted by `product_shape!`.
        pub struct #name;

        const #raw_const:
            [::uor_foundation::pipeline::ConstraintRef;
             2 * ::uor_foundation::enforcement::NERVE_CONSTRAINTS_CAP]
        = ::uor_foundation::pipeline::sdk_concat_product_constraints::<#l, #r>();

        const #len_const: usize =
            ::uor_foundation::pipeline::sdk_product_constraints_len::<#l, #r>();

        impl ::uor_foundation::pipeline::ConstrainedTypeShape for #name {
            const IRI: &'static str = #iri;
            const SITE_BUDGET: usize =
                <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET
                + <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET;
            const SITE_COUNT: usize =
                <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT
                + <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
            const CONSTRAINTS: &'static [::uor_foundation::pipeline::ConstraintRef] = {
                let buf: &'static [::uor_foundation::pipeline::ConstraintRef] = &#raw_const;
                match buf.split_at_checked(#len_const) {
                    Some((head, _tail)) => head,
                    None => &[],
                }
            };
        }

        // Wiki ADR-023 + ADR-027: shape-derived shapes receive the four
        // sealed-trait impls (`__sdk_seal::Sealed`, `IntoBindingValue`,
        // `GroundedShape`, plus the `ConstrainedTypeShape` impl above).
        // The shape struct is a zero-sized type-level marker, so the
        // canonical byte sequence is empty (MAX_BYTES = 0); applications
        // that need to carry runtime input data declare a custom
        // `ConstrainedTypeShape` via the `output_shape!` macro and write a
        // bespoke `IntoBindingValue` impl.
        impl ::uor_foundation::pipeline::__sdk_seal::Sealed for #name {}
        impl ::uor_foundation::pipeline::IntoBindingValue for #name {
            const MAX_BYTES: usize = 0;
            fn into_binding_bytes(
                &self,
                _out: &mut [u8],
            ) -> ::core::result::Result<usize, ::uor_foundation::enforcement::ShapeViolation> {
                Ok(0)
            }
        }
        impl ::uor_foundation::enforcement::GroundedShape for #name {}

        impl #name {
            /// Mint a verified [`PartitionProductWitness`] for this shape's
            /// operand pair. The numeric invariants (Euler characteristics,
            /// entropy, fingerprints) are caller-supplied because they depend
            /// on the resolved constraint configuration; shape-derivable
            /// fields (site budgets / site counts) are read from the
            /// operand `ConstrainedTypeShape` impls.
            ///
            /// # Errors
            ///
            /// Returns a `GenericImpossibilityWitness` citing the specific
            /// failed identity when PT_1, PT_3, PT_4, or the foundation
            /// layout-width invariant fails.
            #[allow(clippy::too_many_arguments)]
            pub fn mint_product_witness(
                witt_bits: u16,
                left_fingerprint: ::uor_foundation::ContentFingerprint,
                right_fingerprint: ::uor_foundation::ContentFingerprint,
                left_euler: i32,
                right_euler: i32,
                left_entropy_nats_bits: u64,
                right_entropy_nats_bits: u64,
                combined_euler: i32,
                combined_entropy_nats_bits: u64,
                combined_fingerprint: ::uor_foundation::ContentFingerprint,
            ) -> ::core::result::Result<
                ::uor_foundation::PartitionProductWitness,
                ::uor_foundation::enforcement::GenericImpossibilityWitness,
            > {
                use ::uor_foundation::pipeline::ConstrainedTypeShape;
                let inputs = ::uor_foundation::PartitionProductMintInputs {
                    witt_bits,
                    left_fingerprint,
                    right_fingerprint,
                    left_site_budget: <#l as ConstrainedTypeShape>::SITE_BUDGET as u16,
                    right_site_budget: <#r as ConstrainedTypeShape>::SITE_BUDGET as u16,
                    left_total_site_count: <#l as ConstrainedTypeShape>::SITE_COUNT as u16,
                    right_total_site_count: <#r as ConstrainedTypeShape>::SITE_COUNT as u16,
                    left_euler,
                    right_euler,
                    left_entropy_nats_bits,
                    right_entropy_nats_bits,
                    combined_site_budget: <#name as ConstrainedTypeShape>::SITE_BUDGET as u16,
                    combined_site_count: <#name as ConstrainedTypeShape>::SITE_COUNT as u16,
                    combined_euler,
                    combined_entropy_nats_bits,
                    combined_fingerprint,
                };
                <::uor_foundation::PartitionProductWitness
                    as ::uor_foundation::VerifiedMint>::mint_verified(inputs)
            }
        }
    };

    expansion.into()
}

/// Coproduct shape constructor. See crate-level docs.
///
/// # Example
///
/// Demonstrates the post-Phase-17 fixed-array `Affine` operand variant.
///
/// ```
/// use uor_foundation::pipeline::{
///     AFFINE_MAX_COEFFS, ConstrainedTypeShape, ConstraintRef,
/// };
/// use uor_foundation_sdk::coproduct_shape;
///
/// const A_COEFFS: [i64; AFFINE_MAX_COEFFS] = {
///     let mut a = [0i64; AFFINE_MAX_COEFFS];
///     a[0] = 1;
///     a
/// };
///
/// pub struct A;
/// impl ConstrainedTypeShape for A {
///     const IRI: &'static str = "https://example.org/A";
///     const SITE_COUNT: usize = 1;
///     const CONSTRAINTS: &'static [ConstraintRef] = &[
///         ConstraintRef::Affine {
///             coefficients: A_COEFFS,
///             coefficient_count: 1,
///             bias: 0,
///         },
///     ];
/// }
///
/// pub struct B;
/// impl ConstrainedTypeShape for B {
///     const IRI: &'static str = "https://example.org/B";
///     const SITE_COUNT: usize = 1;
///     const CONSTRAINTS: &'static [ConstraintRef] = &[];
/// }
///
/// coproduct_shape!(MySum, A, B);
/// assert!(<MySum as ConstrainedTypeShape>::IRI.starts_with("urn:uor:coproduct:"));
/// ```
#[proc_macro]
pub fn coproduct_shape(input: TokenStream) -> TokenStream {
    let ShapeArgs { name, left, right } = parse_macro_input!(input as ShapeArgs);
    let iri = format!(
        "urn:uor:coproduct:{}:{}",
        lexically_earlier(&left, &right),
        lexically_later(&left, &right)
    );
    let (l, r) = canonical_operand_pair(&left, &right);

    // Per amendment §4b' + §4d: coproduct layout is
    //   constraints(A) ∪ {tag-pinner bias=0} ∪ constraints(B) ∪ {tag-pinner bias=-1}
    // with tag_site = max(SITE_COUNT(A), SITE_COUNT(B)). The foundation
    // `sdk_concat_product_constraints` helper handles the A / B splice
    // but the two Affine tag-pinners require construction at macro time,
    // because the tag_site index is a call-site-specific const expression.
    //
    // For a coproduct, the Affine coefficient slices are `&[i64]` with
    // all-zero entries except position tag_site = 1. Since the macro
    // cannot allocate `&'static [i64]` slices of arbitrary length, the
    // emission uses a fixed-size coefficient array that matches
    // `NERVE_CONSTRAINTS_CAP` (the bound on site indices in SDK shapes).
    let raw_const = format_ident_suffix(&name, "__CONSTRAINTS_RAW");
    let len_const = format_ident_suffix(&name, "__CONSTRAINTS_LEN");
    let tag_coeffs_l = format_ident_suffix(&name, "__TAG_COEFFS_L");
    let tag_coeffs_r = format_ident_suffix(&name, "__TAG_COEFFS_R");
    let tag_coeff_count = format_ident_suffix(&name, "__TAG_COEFF_COUNT");

    let expansion = quote! {
        /// UOR SumType shape, emitted by `coproduct_shape!`.
        pub struct #name;

        // Two tag-pinning Affine coefficient arrays, one per variant,
        // each of length 2 * NERVE_CONSTRAINTS_CAP so the single `1` at
        // the tag_site position fits regardless of how wide the
        // operands' SITE_COUNTs are (bounded by NERVE_CONSTRAINTS_CAP
        // each, so tag_site = max(L::SITE_COUNT, R::SITE_COUNT) <
        // Phase 17: tag-pinner coefficient buffer is now a fixed-size
        // `[i64; AFFINE_MAX_COEFFS]` array stored inline in the
        // ConstraintRef::Affine variant. The active prefix runs to
        // `tag_site + 1`. For coproduct shapes whose
        // `max(L::SITE_COUNT, R::SITE_COUNT) + 1` exceeds
        // AFFINE_MAX_COEFFS = 8, the const-eval clamps the tag-pinner
        // to a no-op (count = 0), and `validate_const` rejects the
        // shape at admission time as Affine-unsatisfiable.
        const #tag_coeffs_l: [i64; ::uor_foundation::pipeline::AFFINE_MAX_COEFFS] = {
            let mut out = [0i64; ::uor_foundation::pipeline::AFFINE_MAX_COEFFS];
            let tag_site = {
                let a = <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
                let b = <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
                if a > b { a } else { b }
            };
            if tag_site < ::uor_foundation::pipeline::AFFINE_MAX_COEFFS {
                out[tag_site] = 1;
            }
            out
        };
        const #tag_coeffs_r: [i64; ::uor_foundation::pipeline::AFFINE_MAX_COEFFS] = #tag_coeffs_l;
        const #tag_coeff_count: u32 = {
            let a = <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
            let b = <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
            let tag_site = if a > b { a } else { b };
            (tag_site as u32).saturating_add(1)
        };

        // Full constraint buffer: L constraints + L tag-pinner (bias=0)
        // + R constraints (shifted by L::SITE_COUNT? — per amendment §4d
        // sum types share the data-site space so R's site references are
        // NOT shifted). The foundation helper
        // `sdk_concat_product_constraints` shifts R by A::SITE_COUNT, which
        // is correct for products but wrong for coproducts. Coproducts
        // instead splice R's constraints verbatim since the tag site is
        // the distinguishing bit, not a layout offset.
        //
        // This makes coproduct construction diverge from the helper's
        // assumption, so we emit a per-callsite const fn that does the
        // correct coproduct splice.
        const #raw_const:
            [::uor_foundation::pipeline::ConstraintRef;
             2 * ::uor_foundation::enforcement::NERVE_CONSTRAINTS_CAP + 2]
        = {
            let mut out =
                [::uor_foundation::pipeline::ConstraintRef::Site { position: u32::MAX };
                 2 * ::uor_foundation::enforcement::NERVE_CONSTRAINTS_CAP + 2];
            let left_arr = <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::CONSTRAINTS;
            let right_arr = <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::CONSTRAINTS;
            let mut i = 0;
            while i < left_arr.len() {
                out[i] = left_arr[i];
                i += 1;
            }
            // L's tag-pinner: bias 0.
            out[i] = ::uor_foundation::pipeline::ConstraintRef::Affine {
                coefficients: #tag_coeffs_l,
                coefficient_count: #tag_coeff_count,
                bias: 0,
            };
            let left_boundary = i + 1;
            let mut j = 0;
            while j < right_arr.len() {
                out[left_boundary + j] = right_arr[j];
                j += 1;
            }
            // R's tag-pinner: bias -1.
            out[left_boundary + right_arr.len()] = ::uor_foundation::pipeline::ConstraintRef::Affine {
                coefficients: #tag_coeffs_r,
                coefficient_count: #tag_coeff_count,
                bias: -1,
            };
            out
        };
        const #len_const: usize =
            <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::CONSTRAINTS.len()
            + <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::CONSTRAINTS.len()
            + 2;

        impl ::uor_foundation::pipeline::ConstrainedTypeShape for #name {
            const IRI: &'static str = #iri;
            const SITE_BUDGET: usize = {
                let a = <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET;
                let b = <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET;
                if a > b { a } else { b }
            };
            const SITE_COUNT: usize = {
                let a = <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
                let b = <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
                (if a > b { a } else { b }) + 1
            };
            const CONSTRAINTS: &'static [::uor_foundation::pipeline::ConstraintRef] = {
                let buf: &'static [::uor_foundation::pipeline::ConstraintRef] = &#raw_const;
                match buf.split_at_checked(#len_const) {
                    Some((head, _tail)) => head,
                    None => &[],
                }
            };
        }

        // Wiki ADR-023 + ADR-027: shape-derived shapes receive the four
        // sealed-trait impls so they qualify as both Input
        // (`IntoBindingValue`) and Output (`GroundedShape` +
        // `IntoBindingValue`) for `PrismModel` (zero-sized marker;
        // canonical byte sequence is empty).
        impl ::uor_foundation::pipeline::__sdk_seal::Sealed for #name {}
        impl ::uor_foundation::pipeline::IntoBindingValue for #name {
            const MAX_BYTES: usize = 0;
            fn into_binding_bytes(
                &self,
                _out: &mut [u8],
            ) -> ::core::result::Result<usize, ::uor_foundation::enforcement::ShapeViolation> {
                Ok(0)
            }
        }
        impl ::uor_foundation::enforcement::GroundedShape for #name {}

        impl #name {
            /// Mint a verified [`PartitionCoproductWitness`] for this shape's
            /// operand pair. See `product_shape!`'s `mint_product_witness`
            /// doc comment for the caller-vs-derived field split.
            ///
            /// # Errors
            ///
            /// Returns a `GenericImpossibilityWitness` citing the specific
            /// failed identity when ST_1, ST_2, ST_6, ST_7, ST_8, ST_9,
            /// ST_10, the `CoproductLayoutWidth` layout invariant, or the
            /// `CoproductTagEncoding` byte-pattern invariant fails.
            #[allow(clippy::too_many_arguments)]
            pub fn mint_coproduct_witness(
                witt_bits: u16,
                left_fingerprint: ::uor_foundation::ContentFingerprint,
                right_fingerprint: ::uor_foundation::ContentFingerprint,
                left_euler: i32,
                right_euler: i32,
                left_entropy_nats_bits: u64,
                right_entropy_nats_bits: u64,
                left_betti: [u32; ::uor_foundation::enforcement::MAX_BETTI_DIMENSION],
                right_betti: [u32; ::uor_foundation::enforcement::MAX_BETTI_DIMENSION],
                combined_euler: i32,
                combined_entropy_nats_bits: u64,
                combined_betti: [u32; ::uor_foundation::enforcement::MAX_BETTI_DIMENSION],
                combined_fingerprint: ::uor_foundation::ContentFingerprint,
            ) -> ::core::result::Result<
                ::uor_foundation::PartitionCoproductWitness,
                ::uor_foundation::enforcement::GenericImpossibilityWitness,
            > {
                use ::uor_foundation::pipeline::ConstrainedTypeShape;
                let left_total_site_count = <#l as ConstrainedTypeShape>::SITE_COUNT as u16;
                let right_total_site_count = <#r as ConstrainedTypeShape>::SITE_COUNT as u16;
                let tag_site = if left_total_site_count > right_total_site_count {
                    left_total_site_count
                } else {
                    right_total_site_count
                };
                let left_constraint_count =
                    <#l as ConstrainedTypeShape>::CONSTRAINTS.len() + 1;
                let inputs = ::uor_foundation::PartitionCoproductMintInputs {
                    witt_bits,
                    left_fingerprint,
                    right_fingerprint,
                    left_site_budget: <#l as ConstrainedTypeShape>::SITE_BUDGET as u16,
                    right_site_budget: <#r as ConstrainedTypeShape>::SITE_BUDGET as u16,
                    left_total_site_count,
                    right_total_site_count,
                    left_euler,
                    right_euler,
                    left_entropy_nats_bits,
                    right_entropy_nats_bits,
                    left_betti,
                    right_betti,
                    combined_site_budget: <#name as ConstrainedTypeShape>::SITE_BUDGET as u16,
                    combined_site_count: <#name as ConstrainedTypeShape>::SITE_COUNT as u16,
                    combined_euler,
                    combined_entropy_nats_bits,
                    combined_betti,
                    combined_fingerprint,
                    combined_constraints: <#name as ConstrainedTypeShape>::CONSTRAINTS,
                    left_constraint_count,
                    tag_site,
                };
                <::uor_foundation::PartitionCoproductWitness
                    as ::uor_foundation::VerifiedMint>::mint_verified(inputs)
            }
        }
    };

    expansion.into()
}

/// Cartesian-product shape constructor. See crate-level docs.
///
/// # Example
///
/// ```
/// use uor_foundation::pipeline::{
///     CartesianProductShape, ConstrainedTypeShape, ConstraintRef,
/// };
/// use uor_foundation_sdk::cartesian_product_shape;
///
/// pub struct A;
/// impl ConstrainedTypeShape for A {
///     const IRI: &'static str = "https://example.org/A";
///     const SITE_COUNT: usize = 1;
///     const CONSTRAINTS: &'static [ConstraintRef] = &[];
/// }
/// pub struct B;
/// impl ConstrainedTypeShape for B {
///     const IRI: &'static str = "https://example.org/B";
///     const SITE_COUNT: usize = 1;
///     const CONSTRAINTS: &'static [ConstraintRef] = &[];
/// }
///
/// cartesian_product_shape!(MyCartesian, A, B);
///
/// fn assert_marker<T: CartesianProductShape>() {}
/// assert_marker::<MyCartesian>();
/// ```
#[proc_macro]
pub fn cartesian_product_shape(input: TokenStream) -> TokenStream {
    let ShapeArgs { name, left, right } = parse_macro_input!(input as ShapeArgs);
    let iri = format!(
        "urn:uor:cartesian:{}:{}",
        lexically_earlier(&left, &right),
        lexically_later(&left, &right)
    );
    let (l, r) = canonical_operand_pair(&left, &right);
    let raw_const = format_ident_suffix(&name, "__CONSTRAINTS_RAW");
    let len_const = format_ident_suffix(&name, "__CONSTRAINTS_LEN");

    // CartesianProduct emission mirrors product_shape!'s layout but
    // additionally implements `CartesianProductShape` so the nerve-Betti
    // pipeline uses `primitive_cartesian_nerve_betti` (Künneth) instead of
    // the flat simplicial primitive.
    let expansion = quote! {
        /// UOR CartesianPartitionProduct shape, emitted by
        /// `cartesian_product_shape!`.
        pub struct #name;

        const #raw_const:
            [::uor_foundation::pipeline::ConstraintRef;
             2 * ::uor_foundation::enforcement::NERVE_CONSTRAINTS_CAP]
        = ::uor_foundation::pipeline::sdk_concat_product_constraints::<#l, #r>();

        const #len_const: usize =
            ::uor_foundation::pipeline::sdk_product_constraints_len::<#l, #r>();

        impl ::uor_foundation::pipeline::ConstrainedTypeShape for #name {
            const IRI: &'static str = #iri;
            const SITE_BUDGET: usize =
                <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET
                + <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET;
            const SITE_COUNT: usize =
                <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT
                + <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
            const CONSTRAINTS: &'static [::uor_foundation::pipeline::ConstraintRef] = {
                let buf: &'static [::uor_foundation::pipeline::ConstraintRef] = &#raw_const;
                match buf.split_at_checked(#len_const) {
                    Some((head, _tail)) => head,
                    None => &[],
                }
            };
        }

        impl ::uor_foundation::pipeline::CartesianProductShape for #name {
            type Left = #l;
            type Right = #r;
        }

        // Wiki ADR-023 + ADR-027: shape-derived shapes receive the four
        // sealed-trait impls so they qualify as both Input
        // (`IntoBindingValue`) and Output (`GroundedShape` +
        // `IntoBindingValue`) for `PrismModel` (zero-sized marker;
        // canonical byte sequence is empty).
        impl ::uor_foundation::pipeline::__sdk_seal::Sealed for #name {}
        impl ::uor_foundation::pipeline::IntoBindingValue for #name {
            const MAX_BYTES: usize = 0;
            fn into_binding_bytes(
                &self,
                _out: &mut [u8],
            ) -> ::core::result::Result<usize, ::uor_foundation::enforcement::ShapeViolation> {
                Ok(0)
            }
        }
        impl ::uor_foundation::enforcement::GroundedShape for #name {}

        impl #name {
            /// Mint a verified [`CartesianProductWitness`] for this shape's
            /// operand pair.
            ///
            /// # Errors
            ///
            /// Returns a `GenericImpossibilityWitness` citing the specific
            /// failed identity when CPT_1, CPT_3, CPT_4, CPT_5, or the
            /// `CartesianLayoutWidth` layout invariant fails.
            #[allow(clippy::too_many_arguments)]
            pub fn mint_cartesian_witness(
                witt_bits: u16,
                left_fingerprint: ::uor_foundation::ContentFingerprint,
                right_fingerprint: ::uor_foundation::ContentFingerprint,
                left_euler: i32,
                right_euler: i32,
                left_betti: [u32; ::uor_foundation::enforcement::MAX_BETTI_DIMENSION],
                right_betti: [u32; ::uor_foundation::enforcement::MAX_BETTI_DIMENSION],
                left_entropy_nats_bits: u64,
                right_entropy_nats_bits: u64,
                combined_euler: i32,
                combined_betti: [u32; ::uor_foundation::enforcement::MAX_BETTI_DIMENSION],
                combined_entropy_nats_bits: u64,
                combined_fingerprint: ::uor_foundation::ContentFingerprint,
            ) -> ::core::result::Result<
                ::uor_foundation::CartesianProductWitness,
                ::uor_foundation::enforcement::GenericImpossibilityWitness,
            > {
                use ::uor_foundation::pipeline::ConstrainedTypeShape;
                let inputs = ::uor_foundation::CartesianProductMintInputs {
                    witt_bits,
                    left_fingerprint,
                    right_fingerprint,
                    left_site_budget: <#l as ConstrainedTypeShape>::SITE_BUDGET as u16,
                    right_site_budget: <#r as ConstrainedTypeShape>::SITE_BUDGET as u16,
                    left_total_site_count: <#l as ConstrainedTypeShape>::SITE_COUNT as u16,
                    right_total_site_count: <#r as ConstrainedTypeShape>::SITE_COUNT as u16,
                    left_euler,
                    right_euler,
                    left_betti,
                    right_betti,
                    left_entropy_nats_bits,
                    right_entropy_nats_bits,
                    combined_site_budget: <#name as ConstrainedTypeShape>::SITE_BUDGET as u16,
                    combined_site_count: <#name as ConstrainedTypeShape>::SITE_COUNT as u16,
                    combined_euler,
                    combined_betti,
                    combined_entropy_nats_bits,
                    combined_fingerprint,
                };
                <::uor_foundation::CartesianProductWitness
                    as ::uor_foundation::VerifiedMint>::mint_verified(inputs)
            }
        }
    };

    expansion.into()
}

// =====================================================================
// `partition_product!` and `partition_coproduct!` — wiki ADR-026 G17 + G18.
//
// ADR-026 specifies these as type-level operators recognised in
// `type Input` / `type Output` positions as variadic forms
// `partition_product!(<A>, <B>, …)`. On stable Rust 1.83 the in-position
// variadic form requires `generic_const_exprs` (unstable) to compute
// `IRI`/`CONSTRAINTS` from operand type-parameters at the trait level;
// the architecturally-equivalent stable-Rust surface is the same macros
// at item position with a name argument followed by the operand list:
//
//   `partition_product!(<Name>, <A>, <B>, [<C>, …]);`
//   `partition_coproduct!(<Name>, <A>, <B>, [<C>, …]);`
//
// Three or more operands fold left-associatively: `partition_product!(N, A, B, C)`
// emits the chain `((A × B) × C)` via repeated PT_3 composition. The
// emitted `ConstrainedTypeShape` impl carries the canonically-joined
// `CONSTRAINTS` per ADR-025's PT_3 rule and the IRI per ADR-017's
// content-deterministic naming.

/// Variadic input: `partition_product!(Name, A, B, [C, …])`.
struct VariadicShapeArgs {
    name: Ident,
    operands: Vec<Ident>,
}

impl Parse for VariadicShapeArgs {
    fn parse(input: ParseStream) -> Result<Self> {
        let name: Ident = input.parse()?;
        input.parse::<Token![,]>()?;
        let mut operands: Vec<Ident> = Vec::new();
        operands.push(input.parse()?);
        while input.peek(Token![,]) {
            input.parse::<Token![,]>()?;
            if input.is_empty() {
                break;
            }
            operands.push(input.parse()?);
        }
        if operands.len() < 2 {
            return Err(syn::Error::new(
                name.span(),
                "partition_product!/partition_coproduct! require at least two operands",
            ));
        }
        Ok(Self { name, operands })
    }
}

/// `partition_product!` — wiki ADR-026 G17 type-level shape constructor.
/// Emits a `ConstrainedTypeShape` impl whose `CONSTRAINTS` carry the
/// canonically-joined PT_3 form (algebraic-product per ADR-025), with
/// `SITE_COUNT = Σ operands' SITE_COUNT`.
#[proc_macro]
pub fn partition_product(input: TokenStream) -> TokenStream {
    let parsed = parse_macro_input!(input as VariadicShapeArgs);
    expand_partition_product(parsed.name, &parsed.operands)
}

fn expand_partition_product(name: Ident, operands: &[Ident]) -> TokenStream {
    if operands.len() == 2 {
        // Binary form — delegate to the existing product_shape! semantics
        // by emitting the same ConstrainedTypeShape impl pattern with the
        // PT_3 canonical-join `CONSTRAINTS`.
        let l = &operands[0];
        let r = &operands[1];
        let iri = format!(
            "urn:uor:product:{}:{}",
            lexically_earlier(l, r),
            lexically_later(l, r),
        );
        let (l, r) = canonical_operand_pair(l, r);
        let raw_const = format_ident_suffix(&name, "__CONSTRAINTS_RAW");
        let len_const = format_ident_suffix(&name, "__CONSTRAINTS_LEN");
        let expansion = quote! {
            /// UOR ADR-026 G17 partition-product shape (binary form).
            pub struct #name;

            const #raw_const:
                [::uor_foundation::pipeline::ConstraintRef;
                 2 * ::uor_foundation::enforcement::NERVE_CONSTRAINTS_CAP]
            = ::uor_foundation::pipeline::sdk_concat_product_constraints::<#l, #r>();

            const #len_const: usize =
                ::uor_foundation::pipeline::sdk_product_constraints_len::<#l, #r>();

            impl ::uor_foundation::pipeline::ConstrainedTypeShape for #name {
                const IRI: &'static str = #iri;
                const SITE_BUDGET: usize =
                    <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET
                    + <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET;
                const SITE_COUNT: usize =
                    <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT
                    + <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
                const CONSTRAINTS: &'static [::uor_foundation::pipeline::ConstraintRef] = {
                    let buf: &'static [::uor_foundation::pipeline::ConstraintRef] = &#raw_const;
                    match buf.split_at_checked(#len_const) {
                        Some((head, _tail)) => head,
                        None => &[],
                    }
                };
            }

            impl ::uor_foundation::pipeline::__sdk_seal::Sealed for #name {}
            impl ::uor_foundation::pipeline::IntoBindingValue for #name {
                const MAX_BYTES: usize = 0;
                fn into_binding_bytes(
                    &self,
                    _out: &mut [u8],
                ) -> ::core::result::Result<usize, ::uor_foundation::enforcement::ShapeViolation> {
                    Ok(0)
                }
            }
            impl ::uor_foundation::enforcement::GroundedShape for #name {}
        };
        expansion.into()
    } else {
        // Variadic form: fold left-associatively. `partition_product!(N, A, B, C)`
        // synthesizes intermediate names `N__pp_step_<i>` for each binary
        // composition and chains them, ending at `N`.
        let mut intermediate_names: Vec<Ident> = Vec::with_capacity(operands.len() - 1);
        for i in 0..operands.len() - 2 {
            intermediate_names.push(Ident::new(&format!("{}PpStep{}", name, i), name.span()));
        }
        let mut chain: Vec<proc_macro2::TokenStream> = Vec::with_capacity(operands.len() - 1);
        // First step: A × B → PpStep0
        let mut prev = if operands.len() > 2 {
            intermediate_names[0].clone()
        } else {
            name.clone()
        };
        let first_a = &operands[0];
        let first_b = &operands[1];
        let first_step_call = expand_partition_product_helper(prev.clone(), first_a, first_b);
        chain.push(first_step_call);
        // Each subsequent step: prev × operand[i+1] → next
        for i in 2..operands.len() {
            let next = if i == operands.len() - 1 {
                name.clone()
            } else {
                intermediate_names[i - 1].clone()
            };
            let next_call = expand_partition_product_helper(next.clone(), &prev, &operands[i]);
            chain.push(next_call);
            prev = next;
        }
        let combined = quote! { #( #chain )* };
        combined.into()
    }
}

/// Emit the `ConstrainedTypeShape` + supporting impl-block for a
/// binary partition-product step. Used by `expand_partition_product`'s
/// left-associative variadic chain.
fn expand_partition_product_helper(
    name: Ident,
    left: &Ident,
    right: &Ident,
) -> proc_macro2::TokenStream {
    let iri = format!(
        "urn:uor:product:{}:{}",
        lexically_earlier(left, right),
        lexically_later(left, right),
    );
    let (l, r) = canonical_operand_pair(left, right);
    let raw_const = format_ident_suffix(&name, "__CONSTRAINTS_RAW");
    let len_const = format_ident_suffix(&name, "__CONSTRAINTS_LEN");
    quote! {
        /// UOR ADR-026 G17 partition-product step.
        pub struct #name;

        const #raw_const:
            [::uor_foundation::pipeline::ConstraintRef;
             2 * ::uor_foundation::enforcement::NERVE_CONSTRAINTS_CAP]
        = ::uor_foundation::pipeline::sdk_concat_product_constraints::<#l, #r>();

        const #len_const: usize =
            ::uor_foundation::pipeline::sdk_product_constraints_len::<#l, #r>();

        impl ::uor_foundation::pipeline::ConstrainedTypeShape for #name {
            const IRI: &'static str = #iri;
            const SITE_BUDGET: usize =
                <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET
                + <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET;
            const SITE_COUNT: usize =
                <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT
                + <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
            const CONSTRAINTS: &'static [::uor_foundation::pipeline::ConstraintRef] = {
                let buf: &'static [::uor_foundation::pipeline::ConstraintRef] = &#raw_const;
                match buf.split_at_checked(#len_const) {
                    Some((head, _tail)) => head,
                    None => &[],
                }
            };
        }

        impl ::uor_foundation::pipeline::__sdk_seal::Sealed for #name {}
        impl ::uor_foundation::pipeline::IntoBindingValue for #name {
            const MAX_BYTES: usize = 0;
            fn into_binding_bytes(
                &self,
                _out: &mut [u8],
            ) -> ::core::result::Result<usize, ::uor_foundation::enforcement::ShapeViolation> {
                Ok(0)
            }
        }
        impl ::uor_foundation::enforcement::GroundedShape for #name {}
    }
}

/// `partition_coproduct!` — wiki ADR-026 G18 type-level shape constructor.
/// Variadic named form. Folds left-associatively into binary
/// coproducts. Each binary step emits the same shape `coproduct_shape!`
/// produces (ST_10 canonical structure).
#[proc_macro]
pub fn partition_coproduct(input: TokenStream) -> TokenStream {
    let parsed = parse_macro_input!(input as VariadicShapeArgs);
    expand_partition_coproduct(parsed.name, &parsed.operands)
}

fn expand_partition_coproduct(name: Ident, operands: &[Ident]) -> TokenStream {
    if operands.len() == 2 {
        let combined = expand_partition_coproduct_helper(name, &operands[0], &operands[1]);
        return combined.into();
    }
    let mut intermediate_names: Vec<Ident> = Vec::with_capacity(operands.len() - 1);
    for i in 0..operands.len() - 2 {
        intermediate_names.push(Ident::new(&format!("{}PcStep{}", name, i), name.span()));
    }
    let mut chain: Vec<proc_macro2::TokenStream> = Vec::with_capacity(operands.len() - 1);
    let mut prev = if operands.len() > 2 {
        intermediate_names[0].clone()
    } else {
        name.clone()
    };
    let first_step = expand_partition_coproduct_helper(prev.clone(), &operands[0], &operands[1]);
    chain.push(first_step);
    for i in 2..operands.len() {
        let next = if i == operands.len() - 1 {
            name.clone()
        } else {
            intermediate_names[i - 1].clone()
        };
        let step = expand_partition_coproduct_helper(next.clone(), &prev, &operands[i]);
        chain.push(step);
        prev = next;
    }
    let combined = quote! { #( #chain )* };
    combined.into()
}

fn expand_partition_coproduct_helper(
    name: Ident,
    left: &Ident,
    right: &Ident,
) -> proc_macro2::TokenStream {
    let iri = format!(
        "urn:uor:coproduct:{}:{}",
        lexically_earlier(left, right),
        lexically_later(left, right),
    );
    let (l, r) = canonical_operand_pair(left, right);
    let raw_const = format_ident_suffix(&name, "__CONSTRAINTS_RAW");
    let len_const = format_ident_suffix(&name, "__CONSTRAINTS_LEN");
    let tag_coeffs_l = format_ident_suffix(&name, "__TAG_COEFFS_L");
    let tag_coeffs_r = format_ident_suffix(&name, "__TAG_COEFFS_R");
    let tag_coeff_count = format_ident_suffix(&name, "__TAG_COEFF_COUNT");
    quote! {
        /// UOR ADR-026 G18 partition-coproduct step.
        pub struct #name;

        const #tag_coeffs_l: [i64; ::uor_foundation::pipeline::AFFINE_MAX_COEFFS] = {
            let mut out = [0i64; ::uor_foundation::pipeline::AFFINE_MAX_COEFFS];
            let tag_site = {
                let a = <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
                let b = <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
                if a > b { a } else { b }
            };
            if tag_site < ::uor_foundation::pipeline::AFFINE_MAX_COEFFS {
                out[tag_site] = 1;
            }
            out
        };
        const #tag_coeffs_r: [i64; ::uor_foundation::pipeline::AFFINE_MAX_COEFFS] = #tag_coeffs_l;
        const #tag_coeff_count: u32 = {
            let a = <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
            let b = <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
            let tag_site = if a > b { a } else { b };
            (tag_site as u32).saturating_add(1)
        };

        const #raw_const:
            [::uor_foundation::pipeline::ConstraintRef;
             2 * ::uor_foundation::enforcement::NERVE_CONSTRAINTS_CAP + 2]
        = {
            let mut out =
                [::uor_foundation::pipeline::ConstraintRef::Site { position: u32::MAX };
                 2 * ::uor_foundation::enforcement::NERVE_CONSTRAINTS_CAP + 2];
            let left_arr = <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::CONSTRAINTS;
            let right_arr = <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::CONSTRAINTS;
            let mut i = 0;
            while i < left_arr.len() {
                out[i] = left_arr[i];
                i += 1;
            }
            out[i] = ::uor_foundation::pipeline::ConstraintRef::Affine {
                coefficients: #tag_coeffs_l,
                coefficient_count: #tag_coeff_count,
                bias: 0,
            };
            i += 1;
            let mut j = 0;
            while j < right_arr.len() {
                out[i] = right_arr[j];
                i += 1;
                j += 1;
            }
            out[i] = ::uor_foundation::pipeline::ConstraintRef::Affine {
                coefficients: #tag_coeffs_r,
                coefficient_count: #tag_coeff_count,
                bias: -1,
            };
            out
        };
        const #len_const: usize =
            <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::CONSTRAINTS.len()
            + <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::CONSTRAINTS.len()
            + 2;

        impl ::uor_foundation::pipeline::ConstrainedTypeShape for #name {
            const IRI: &'static str = #iri;
            const SITE_BUDGET: usize = {
                let a = <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET;
                let b = <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_BUDGET;
                if a > b { a } else { b }
            };
            const SITE_COUNT: usize = {
                let a = <#l as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
                let b = <#r as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
                (if a > b { a } else { b }) + 1
            };
            const CONSTRAINTS: &'static [::uor_foundation::pipeline::ConstraintRef] = {
                let buf: &'static [::uor_foundation::pipeline::ConstraintRef] = &#raw_const;
                match buf.split_at_checked(#len_const) {
                    Some((head, _tail)) => head,
                    None => &[],
                }
            };
        }

        impl ::uor_foundation::pipeline::__sdk_seal::Sealed for #name {}
        impl ::uor_foundation::pipeline::IntoBindingValue for #name {
            const MAX_BYTES: usize = 0;
            fn into_binding_bytes(
                &self,
                _out: &mut [u8],
            ) -> ::core::result::Result<usize, ::uor_foundation::enforcement::ShapeViolation> {
                Ok(0)
            }
        }
        impl ::uor_foundation::enforcement::GroundedShape for #name {}
    }
}

// =====================================================================
// `prism_model!` — wiki ADR-020 + ADR-022 D3.
//
// The macro accepts the closure-bodied form the wiki specifies as the
// maximally-Rust-native syntax for declaring a Prism model:
//
// ```text
// prism_model! {
//     pub struct MyModel;
//     pub struct MyRoute;
//     impl PrismModel<HType, BType, AType> for MyModel {
//         type Input  = InputShape;
//         type Output = OutputShape;
//         type Route  = MyRoute;
//         fn route(input: Self::Input) -> Self::Output {
//             // closure body — Rust expression syntax parsed by the macro
//             // into a Term tree at expansion time. The body never executes
//             // as Rust at runtime; it is consumed at macro time, mapped to
//             // the term-tree representation, and the macro emits both the
//             // term tree (as a `&'static [Term]` slice) and the
//             // closure-checked `FoundationClosed` impl.
//             //
//             // Recognised foundation-vocabulary forms:
//             //   - integer literals          → Term::Literal
//             //   - identifier `input`        → Term::Variable
//             //   - lowercase PrimitiveOp     → Term::Application
//             //     names: add, sub, mul, xor, and, or
//             //           neg, bnot, succ, pred
//             // Anything else fails to compile, pointing at the offending
//             // call site (a closure violation per ADR-020).
//         }
//     }
// }
// ```
//
// Emissions (per ADR-022):
//   D1: `impl __sdk_seal::Sealed for MyModel`,
//       `impl __sdk_seal::Sealed for MyRoute`
//   D2: `const ROUTE_TERMS_<MODEL>: &'static [Term] = &[…]` (fully const
//       — `TermArena::from_slice(ROUTE_TERMS_<MODEL>)` is a `const fn`)
//   D5: `impl FoundationClosed for MyRoute { arena_slice() → ROUTE_TERMS_<MODEL> }`
//   D4: `impl PrismModel<H,B,A> for MyModel { …; fn forward(input) { run_route::<H,B,A,Self>(input) } }`

/// Parsed shape of the macro input — a struct declaration for the model,
/// optionally one for the route witness, and an `impl PrismModel<…> for
/// <Model>` block carrying the three associated types and the closure-bodied
/// `route` function.
struct PrismModelInput {
    model_vis: syn::Visibility,
    model_name: Ident,
    route_vis: syn::Visibility,
    route_name: Ident,
    h_ty: syn::Type,
    b_ty: syn::Type,
    a_ty: syn::Type,
    input_ty: syn::Type,
    output_ty: syn::Type,
    route_input_ident: Ident,
    route_body: syn::Block,
}

impl Parse for PrismModelInput {
    fn parse(input: ParseStream) -> Result<Self> {
        // Model struct: `pub struct ModelName;`
        let model_vis: syn::Visibility = input.parse()?;
        input.parse::<Token![struct]>()?;
        let model_name: Ident = input.parse()?;
        input.parse::<Token![;]>()?;

        // Route witness struct: `pub struct RouteName;`
        let route_vis: syn::Visibility = input.parse()?;
        input.parse::<Token![struct]>()?;
        let route_name: Ident = input.parse()?;
        input.parse::<Token![;]>()?;

        // `impl PrismModel<H, B, A> for ModelName`
        input.parse::<Token![impl]>()?;
        let trait_ident: Ident = input.parse()?;
        if trait_ident != "PrismModel" {
            return Err(syn::Error::new(
                trait_ident.span(),
                "prism_model! expects an `impl PrismModel<H, B, A> for <Model>` block",
            ));
        }
        input.parse::<Token![<]>()?;
        let h_ty: syn::Type = input.parse()?;
        input.parse::<Token![,]>()?;
        let b_ty: syn::Type = input.parse()?;
        input.parse::<Token![,]>()?;
        let a_ty: syn::Type = input.parse()?;
        input.parse::<Token![>]>()?;
        input.parse::<Token![for]>()?;
        let impl_target: Ident = input.parse()?;
        if impl_target != model_name {
            return Err(syn::Error::new(
                impl_target.span(),
                "prism_model!'s `impl PrismModel<…> for <Model>` target must match the declared model struct",
            ));
        }

        // Body of the impl block: `{ type Input = …; type Output = …; type Route = …; fn route(…) { … } }`
        let body;
        syn::braced!(body in input);

        // type Input = …;
        body.parse::<Token![type]>()?;
        let input_kw: Ident = body.parse()?;
        if input_kw != "Input" {
            return Err(syn::Error::new(
                input_kw.span(),
                "expected `type Input = …;`",
            ));
        }
        body.parse::<Token![=]>()?;
        let input_ty: syn::Type = body.parse()?;
        body.parse::<Token![;]>()?;

        // type Output = …;
        body.parse::<Token![type]>()?;
        let output_kw: Ident = body.parse()?;
        if output_kw != "Output" {
            return Err(syn::Error::new(
                output_kw.span(),
                "expected `type Output = …;`",
            ));
        }
        body.parse::<Token![=]>()?;
        let output_ty: syn::Type = body.parse()?;
        body.parse::<Token![;]>()?;

        // type Route = …;
        body.parse::<Token![type]>()?;
        let route_kw: Ident = body.parse()?;
        if route_kw != "Route" {
            return Err(syn::Error::new(
                route_kw.span(),
                "expected `type Route = …;`",
            ));
        }
        body.parse::<Token![=]>()?;
        let route_ty_ident: Ident = body.parse()?;
        if route_ty_ident != route_name {
            return Err(syn::Error::new(
                route_ty_ident.span(),
                "prism_model!'s `type Route = <RouteName>;` must match the declared route struct",
            ));
        }
        body.parse::<Token![;]>()?;

        // fn route(input: Self::Input) -> Self::Output { … }
        body.parse::<Token![fn]>()?;
        let fn_kw: Ident = body.parse()?;
        if fn_kw != "route" {
            return Err(syn::Error::new(
                fn_kw.span(),
                "expected `fn route(input: Self::Input) -> Self::Output { … }`",
            ));
        }
        let params;
        syn::parenthesized!(params in body);
        let route_input_ident: Ident = params.parse()?;
        params.parse::<Token![:]>()?;
        let _input_param_ty: syn::Type = params.parse()?;
        // Discard return-type position — we already know it from `type Output`.
        body.parse::<Token![->]>()?;
        let _output_param_ty: syn::Type = body.parse()?;
        let route_body: syn::Block = body.parse()?;

        Ok(Self {
            model_vis,
            model_name,
            route_vis,
            route_name,
            h_ty,
            b_ty,
            a_ty,
            input_ty,
            output_ty,
            route_input_ident,
            route_body,
        })
    }
}

/// One spec entry in the term arena being built. Maps to a `Term::*`
/// variant token stream at emission time.
enum TermSpec {
    /// `Term::Literal { value, level: WittLevel::W8 }`
    Literal(u64),
    /// `Term::Variable { name_index: 0 }` (the macro recognises `input`
    /// as the sole bound name; future iterations support `let` bindings).
    Variable,
    /// `Term::Application { operator, args: TermList { start, len } }`
    Application {
        operator: proc_macro2::TokenStream,
        args_start: u32,
        args_len: u32,
    },
    /// `Term::HasherProjection { input_index }` — wiki ADR-026 G19.
    /// The input subtree's root is at `input_index`.
    HasherProjection { input_index: u32 },
    /// Compile-time verb splice — wiki ADR-024.
    ///
    /// Inlines the verb's `&'static [Term]` fragment into the host
    /// arena at expansion time via `inline_verb_fragment` (with each
    /// internal arena index shifted by the host's current length) plus
    /// substitution: every `Term::Variable { name_index: 0 }` in the
    /// fragment is replaced by the host arena's term at `arg_root_idx`.
    /// The substitution makes the verb's `input` parameter bind to the
    /// caller's argument expression.
    ///
    /// `arg_root_idx` is the TermSpec arena index whose result position
    /// the verb's input substitutes to. The render layer translates
    /// TermSpec indices to dynamic host positions via per-spec
    /// `pos_<N>` const-let bindings emitted in the arena builder.
    VerbSplice {
        arg_root_idx: u32,
        fragment_path: proc_macro2::TokenStream,
    },
    /// `Term::Lift { operand_index, target }` — wiki ADR-022 D3 G4.
    /// Canonical injection from the operand's Witt level to a strictly
    /// higher target level (lossless zero-extension).
    Lift {
        operand_index: u32,
        target_witt: proc_macro2::TokenStream,
    },
    /// `Term::Project { operand_index, target }` — wiki ADR-022 D3 G5.
    /// Canonical surjection from the operand's Witt level to a strictly
    /// lower target level (lossy truncation).
    Project {
        operand_index: u32,
        target_witt: proc_macro2::TokenStream,
    },
    /// `Term::Try { body_index, handler_index: u32::MAX }` — wiki
    /// ADR-022 D3 G9. The postfix `?` operator on a sub-expression.
    /// Foundation's catamorphism interprets the `u32::MAX` sentinel as
    /// "propagate the failure unchanged through `PipelineFailure`".
    Try { body_index: u32 },
    /// `Term::Recurse { measure_index, base_index, step_index }` — wiki
    /// ADR-022 D3 G7. Bounded recursion guarded by a descent measure.
    Recurse {
        measure_index: u32,
        base_index: u32,
        step_index: u32,
    },
    /// `Term::Unfold { seed_index, step_index }` — wiki ADR-022 D3 G8.
    /// Anamorphism step.
    Unfold { seed_index: u32, step_index: u32 },
    /// `Term::Match { scrutinee_index, arms }` — wiki ADR-022 D3 G6.
    /// Arms alternate (pattern, body) per the convention foundation's
    /// catamorphism reads to dispatch.
    Match {
        scrutinee_index: u32,
        arms_start: u32,
        arms_len: u32,
    },
    /// Wildcard pattern sentinel — wiki ADR-022 D3 G6 (and G9 default
    /// handler). Lowers to `Term::Variable { name_index: u32::MAX }`.
    WildcardSentinel,
}

/// Per-scope binding table the closure-body parser maintains. Maps a
/// `let`-introduced identifier to the arena index where that binding's
/// value-tree's root lives, so identifier references inside the
/// `let`'s scope resolve to that root. Per wiki ADR-022 D3 G10 the
/// macro builds this incrementally as it descends through `let`
/// statements; the route's input parameter is its own special case
/// (`Term::Variable { name_index: 0 }`) and lives outside this table.
#[derive(Default, Clone)]
struct BindingScope {
    bindings: Vec<(Ident, usize)>,
}

impl BindingScope {
    fn lookup(&self, ident: &Ident) -> Option<usize> {
        // Iterate in reverse so inner shadowing (G10 forbids it but the
        // lookup works either way) finds the latest declaration.
        self.bindings
            .iter()
            .rev()
            .find(|(name, _)| name == ident)
            .map(|(_, idx)| *idx)
    }

    fn shadow_check(&self, ident: &Ident) -> Result<()> {
        if self.bindings.iter().any(|(name, _)| name == ident) {
            return Err(syn::Error::new(
                ident.span(),
                format!(
                    "closure violation: shadowing `{ident}` (ADR-022 D3 G10 forbids declaring two `let`s with the same identifier in the same scope)"
                ),
            ));
        }
        Ok(())
    }

    fn push(&mut self, ident: Ident, root_idx: usize) {
        self.bindings.push((ident, root_idx));
    }
}

/// Recursively walk a Rust expression and append the terms that compute
/// it to `arena`, returning the index where this expression's *root*
/// term lands. `route_input` is the name of the route's bound input
/// parameter (mapped to `Term::Variable { name_index: 0 }`); `scope`
/// carries `let`-introduced bindings (G10) the parser has accumulated.
fn emit_term_for_expr(
    expr: &syn::Expr,
    route_input: &Ident,
    arena: &mut Vec<TermSpec>,
    scope: &mut BindingScope,
) -> Result<usize> {
    match expr {
        syn::Expr::Lit(syn::ExprLit { lit: syn::Lit::Int(int_lit), .. }) => {
            let value: u64 = int_lit.base10_parse().map_err(|e| {
                syn::Error::new(int_lit.span(), format!("integer literal out of u64 range: {e}"))
            })?;
            let idx = arena.len();
            arena.push(TermSpec::Literal(value));
            Ok(idx)
        }
        syn::Expr::Path(path_expr) if path_expr.path.get_ident() == Some(route_input) => {
            let idx = arena.len();
            arena.push(TermSpec::Variable);
            Ok(idx)
        }
        syn::Expr::Path(path_expr) => {
            // ADR-022 D3 G10: a bare identifier may be a `let`-introduced
            // binding from the surrounding scope. The macro splices the
            // binding's value-tree root by emitting a duplicate path that
            // shares the same arena root index — semantically identical
            // because Term values are content-determined.
            if let Some(name) = path_expr.path.get_ident() {
                if let Some(root) = scope.lookup(name) {
                    return Ok(root);
                }
            }
            Err(syn::Error::new_spanned(
                path_expr,
                "closure violation: identifier is not a foundation-vocabulary name (only the route's `input` parameter, `let`-introduced bindings, and reserved macro-vocabulary identifiers are recognised)",
            ))
        }
        syn::Expr::Call(call_expr) => emit_term_for_call(call_expr, route_input, arena, scope),
        syn::Expr::Block(block_expr) => emit_term_for_block(&block_expr.block, route_input, arena, scope),
        syn::Expr::Paren(paren_expr) => {
            emit_term_for_expr(&paren_expr.expr, route_input, arena, scope)
        }
        // ADR-022 D3 G9: postfix `?` operator. Emits Term::Try with the
        // default-propagation handler (`u32::MAX`) — the catamorphism
        // propagates the body's failure unchanged through PipelineFailure.
        syn::Expr::Try(try_expr) => {
            let body_root = emit_term_for_expr(&try_expr.expr, route_input, arena, scope)?;
            let idx = arena.len();
            arena.push(TermSpec::Try { body_index: body_root as u32 });
            Ok(idx)
        }
        // ADR-022 D3 G6: `match <scrutinee> { <pat> => <arm>, …, _ => <default> }`.
        syn::Expr::Match(match_expr) => emit_term_for_match(match_expr, route_input, arena, scope),
        other => Err(syn::Error::new_spanned(
            other,
            "closure violation: expression form is not in foundation vocabulary (recognised forms: integer literals, the route's `input` parameter, `let`-introduced bindings, postfix `?`, `match`, and macro-vocabulary function calls — PrimitiveOps, hash, lift, project, recurse, unfold, plus implementation verbs)",
        )),
    }
}

/// Handle `match <scrutinee> { <lit_pat> => <body>, …, _ => <default> }`
/// per wiki ADR-022 D3 G6. Each arm's pattern is an atomic term
/// (Literal or WildcardSentinel); each arm's body is an arbitrary
/// expression whose sub-tree lives in the arena. The wiki specifies the
/// arms span as a contiguous block of `2 * num_arms` terms alternating
/// (pattern, body); the body in that span is a *copy of the body's root
/// term* so the catamorphism's evaluator can dispatch by reading
/// `arena[start + 2k]` (pattern) and `arena[start + 2k + 1]` (body
/// root). The body's sub-tree lives at lower indices.
fn emit_term_for_match(
    match_expr: &syn::ExprMatch,
    route_input: &Ident,
    arena: &mut Vec<TermSpec>,
    scope: &mut BindingScope,
) -> Result<usize> {
    let scrutinee_root = emit_term_for_expr(&match_expr.expr, route_input, arena, scope)?;
    if match_expr.arms.is_empty() {
        return Err(syn::Error::new_spanned(
            match_expr,
            "closure violation: `match` (G6) must have at least one arm; non-exhaustive matches are closure violations",
        ));
    }
    let last_arm = &match_expr.arms[match_expr.arms.len() - 1];
    let last_is_wildcard = matches!(last_arm.pat, syn::Pat::Wild(_));
    if !last_is_wildcard {
        return Err(syn::Error::new_spanned(
            &last_arm.pat,
            "closure violation: `match` (G6) MUST end with a wildcard arm `_ => <default>`; non-exhaustive matches are closure violations",
        ));
    }

    // First pass: emit each arm's body sub-tree, recording the pattern
    // spec and body-root arena index. The pattern is atomic so we
    // construct the spec inline rather than reserving an arena slot.
    let mut arm_pairs: Vec<(TermSpec, usize)> = Vec::with_capacity(match_expr.arms.len());
    for arm in &match_expr.arms {
        if arm.guard.is_some() {
            return Err(syn::Error::new_spanned(
                arm,
                "closure violation: match arm guards are not in the closure-body grammar (G6)",
            ));
        }
        let pattern_spec = match &arm.pat {
            syn::Pat::Lit(lit_pat) => {
                if let syn::Lit::Int(int_lit) = &lit_pat.lit {
                    let value: u64 = int_lit.base10_parse().map_err(|e| {
                        syn::Error::new(
                            int_lit.span(),
                            format!("integer literal out of u64 range: {e}"),
                        )
                    })?;
                    TermSpec::Literal(value)
                } else {
                    return Err(syn::Error::new_spanned(
                        lit_pat,
                        "closure violation: match patterns must be integer literals or `_` (G6)",
                    ));
                }
            }
            syn::Pat::Wild(_) => TermSpec::WildcardSentinel,
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: match patterns must be integer literals or `_` (G6)",
                ));
            }
        };
        let body_root = emit_term_for_expr(&arm.body, route_input, arena, scope)?;
        arm_pairs.push((pattern_spec, body_root));
    }

    // Second pass: emit the contiguous arms span with alternating
    // (pattern, body_root_copy). The body_root_copy duplicates the
    // TermSpec at the body's root so the arms span is exactly
    // `2 * num_arms` terms — the layout the catamorphism's evaluator
    // expects per ADR-029's `Term::Match` fold rule.
    let arms_start = arena.len();
    for (pattern_spec, body_root_idx) in arm_pairs {
        arena.push(pattern_spec);
        let body_copy = clone_term_spec(&arena[body_root_idx]);
        arena.push(body_copy);
    }
    let arms_len = arena.len() - arms_start;
    let idx = arena.len();
    arena.push(TermSpec::Match {
        scrutinee_index: scrutinee_root as u32,
        arms_start: arms_start as u32,
        arms_len: arms_len as u32,
    });
    Ok(idx)
}

/// Duplicate a `TermSpec`. Used when emitting `match` arm-spans where
/// the body's root term must be copied into the arms range alongside
/// its pattern.
fn clone_term_spec(spec: &TermSpec) -> TermSpec {
    match spec {
        TermSpec::Literal(v) => TermSpec::Literal(*v),
        TermSpec::Variable => TermSpec::Variable,
        TermSpec::Application {
            operator,
            args_start,
            args_len,
        } => TermSpec::Application {
            operator: operator.clone(),
            args_start: *args_start,
            args_len: *args_len,
        },
        TermSpec::HasherProjection { input_index } => TermSpec::HasherProjection {
            input_index: *input_index,
        },
        TermSpec::VerbSplice {
            arg_root_idx,
            fragment_path,
        } => TermSpec::VerbSplice {
            arg_root_idx: *arg_root_idx,
            fragment_path: fragment_path.clone(),
        },
        TermSpec::Lift {
            operand_index,
            target_witt,
        } => TermSpec::Lift {
            operand_index: *operand_index,
            target_witt: target_witt.clone(),
        },
        TermSpec::Project {
            operand_index,
            target_witt,
        } => TermSpec::Project {
            operand_index: *operand_index,
            target_witt: target_witt.clone(),
        },
        TermSpec::Try { body_index } => TermSpec::Try {
            body_index: *body_index,
        },
        TermSpec::Recurse {
            measure_index,
            base_index,
            step_index,
        } => TermSpec::Recurse {
            measure_index: *measure_index,
            base_index: *base_index,
            step_index: *step_index,
        },
        TermSpec::Unfold {
            seed_index,
            step_index,
        } => TermSpec::Unfold {
            seed_index: *seed_index,
            step_index: *step_index,
        },
        TermSpec::Match {
            scrutinee_index,
            arms_start,
            arms_len,
        } => TermSpec::Match {
            scrutinee_index: *scrutinee_index,
            arms_start: *arms_start,
            arms_len: *arms_len,
        },
        TermSpec::WildcardSentinel => TermSpec::WildcardSentinel,
    }
}

/// Handle a `{ <stmts>; <tail_expr> }` block — wiki ADR-022 D3 G10 + G11.
/// `let` statements bind identifiers to the `let`'s value-tree root; the
/// final expression is the block's value.
fn emit_term_for_block(
    block: &syn::Block,
    route_input: &Ident,
    arena: &mut Vec<TermSpec>,
    scope: &mut BindingScope,
) -> Result<usize> {
    if block.stmts.is_empty() {
        return Err(syn::Error::new_spanned(
            block,
            "closure violation: block expressions must contain at least one statement (G11) — empty blocks are unreachable in the closure-body grammar",
        ));
    }
    let mut local_scope = scope.clone();
    let last = block.stmts.len() - 1;
    for (i, stmt) in block.stmts.iter().enumerate() {
        match stmt {
            syn::Stmt::Local(local) => {
                if i == last {
                    return Err(syn::Error::new_spanned(
                        stmt,
                        "closure violation: block must end with an expression statement (G11), not a `let` binding",
                    ));
                }
                let ident = match &local.pat {
                    syn::Pat::Ident(pat_ident) => {
                        if pat_ident.by_ref.is_some() || pat_ident.mutability.is_some() {
                            return Err(syn::Error::new_spanned(
                                pat_ident,
                                "closure violation: `let` binding patterns must be plain identifiers (no `ref`, no `mut`) per ADR-022 D3 G10",
                            ));
                        }
                        if pat_ident.subpat.is_some() {
                            return Err(syn::Error::new_spanned(
                                pat_ident,
                                "closure violation: `let` binding patterns must be plain identifiers per ADR-022 D3 G10",
                            ));
                        }
                        pat_ident.ident.clone()
                    }
                    other => {
                        return Err(syn::Error::new_spanned(
                            other,
                            "closure violation: `let` binding patterns must be plain identifiers per ADR-022 D3 G10",
                        ));
                    }
                };
                local_scope.shadow_check(&ident)?;
                let init = local.init.as_ref().ok_or_else(|| {
                    syn::Error::new_spanned(
                        local,
                        "closure violation: `let` bindings must have an initializer (`let <name> = <expr>;`)",
                    )
                })?;
                if init.diverge.is_some() {
                    return Err(syn::Error::new_spanned(
                        local,
                        "closure violation: `let ... else` is not in the closure-body grammar (G10)",
                    ));
                }
                let value_root =
                    emit_term_for_expr(&init.expr, route_input, arena, &mut local_scope)?;
                local_scope.push(ident, value_root);
            }
            syn::Stmt::Expr(inner, semi) => {
                if i == last {
                    if semi.is_some() {
                        return Err(syn::Error::new_spanned(
                            stmt,
                            "closure violation: block must end with a tail expression (G11), no trailing `;`",
                        ));
                    }
                    return emit_term_for_expr(inner, route_input, arena, &mut local_scope);
                }
                return Err(syn::Error::new_spanned(
                    stmt,
                    "closure violation: only `let` statements may precede the block's tail expression (G10/G11)",
                ));
            }
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: block statement is not in the closure-body grammar (G10/G11 admits only `let` and a final expression)",
                ));
            }
        }
    }
    // Unreachable in well-typed flow — the loop always returns or errors.
    Err(syn::Error::new_spanned(
        block,
        "closure violation: block lacks a tail expression (G11)",
    ))
}

/// Map a function-call expression to a `Term::Application` (G3),
/// `Term::Lift` (G4), `Term::Project` (G5), `Term::HasherProjection`
/// (G19), `Term::Recurse` (G7), `Term::Unfold` (G8), or — for
/// non-reserved identifiers — a `TermSpec::VerbSplice` that the
/// `prism_model!` const-fn arena builder inlines at compile time per
/// ADR-024. Rejects anything else as a closure violation.
fn emit_term_for_call(
    call: &syn::ExprCall,
    route_input: &Ident,
    arena: &mut Vec<TermSpec>,
    scope: &mut BindingScope,
) -> Result<usize> {
    // ADR-022 D3 G4 / G5: `lift::<W{n}>(operand)` and `project::<W{n}>(operand)`
    // — the call target is a path with a generic Witt-level argument.
    if let syn::Expr::Path(path_expr) = call.func.as_ref() {
        let segments = &path_expr.path.segments;
        if segments.len() == 1 {
            let segment = &segments[0];
            let last_ident = &segment.ident;
            if last_ident == "lift" || last_ident == "project" {
                let target_witt = match &segment.arguments {
                    syn::PathArguments::AngleBracketed(args) if args.args.len() == 1 => {
                        match &args.args[0] {
                            syn::GenericArgument::Type(syn::Type::Path(tp)) => tp.path.clone(),
                            other => {
                                return Err(syn::Error::new_spanned(
                                    other,
                                    "closure violation: lift/project's generic argument must be a Witt-level type (e.g., `WittLevel::W32`)",
                                ));
                            }
                        }
                    }
                    _ => {
                        return Err(syn::Error::new_spanned(
                            segment,
                            format!(
                                "closure violation: `{last_ident}` requires a generic Witt-level argument: `{last_ident}::<WittLevel::W{{n}}>(operand)`"
                            ),
                        ));
                    }
                };
                if call.args.len() != 1 {
                    return Err(syn::Error::new(
                        last_ident.span(),
                        format!(
                            "closure violation: `{last_ident}` (G4/G5) expects 1 argument, got {}",
                            call.args.len()
                        ),
                    ));
                }
                let operand_root = emit_term_for_expr(&call.args[0], route_input, arena, scope)?;
                let target_witt_ts = quote! { #target_witt };
                let idx = arena.len();
                let spec = if last_ident == "lift" {
                    TermSpec::Lift {
                        operand_index: operand_root as u32,
                        target_witt: target_witt_ts,
                    }
                } else {
                    TermSpec::Project {
                        operand_index: operand_root as u32,
                        target_witt: target_witt_ts,
                    }
                };
                arena.push(spec);
                return Ok(idx);
            }
        }
    }

    // All other call shapes require a bare identifier callee.
    let func_ident = match call.func.as_ref() {
        syn::Expr::Path(p) => p.path.get_ident().cloned().ok_or_else(|| {
            syn::Error::new_spanned(
                &call.func,
                "closure violation: call target must be a bare identifier matching a PrimitiveOp name, the `hash` verb form, or a declared verb identifier",
            )
        })?,
        other => {
            return Err(syn::Error::new_spanned(
                other,
                "closure violation: call target must be a bare identifier",
            ));
        }
    };

    // ADR-024 verb invocation: any non-reserved, non-PrimitiveOp
    // identifier in call position is treated as a verb call. The macro
    // records a `TermSpec::VerbSplice` referencing `VERB_TERMS_<NAME>`;
    // when the route emits its arena, `render_const_fn_arena_builder`
    // inlines the verb's fragment at compile time via foundation's
    // `inline_verb_fragment` const-fn helper. Rust's name resolution
    // surfaces "cannot find value" at the verb-call span if the
    // referenced const isn't in scope.
    let verb_resolution = match func_ident.to_string().as_str() {
        // Exclude all reserved + PrimitiveOp identifiers from verb
        // resolution; these have dedicated handling below.
        "add" | "sub" | "mul" | "xor" | "and" | "or" | "neg" | "bnot" | "succ" | "pred"
        | "hash" | "parallel" | "fold_n" | "tree_fold" | "first_admit" | "recurse" | "unfold" => {
            false
        }
        _ => true,
    };
    if verb_resolution {
        if call.args.len() != 1 {
            return Err(syn::Error::new(
                func_ident.span(),
                format!(
                    "verb invocation `{}` expects 1 argument (the verb's input value), got {}",
                    func_ident,
                    call.args.len()
                ),
            ));
        }
        let arg_root = emit_term_for_expr(&call.args[0], route_input, arena, scope)?;
        let const_name = Ident::new(
            &format!("VERB_TERMS_{}", to_screaming_snake(&func_ident.to_string())),
            func_ident.span(),
        );
        let fragment_path = quote! { #const_name };
        let idx = arena.len();
        arena.push(TermSpec::VerbSplice {
            arg_root_idx: arg_root as u32,
            fragment_path,
        });
        return Ok(idx);
    }

    // ADR-026 G14: `fold_n(n, init, |state, idx| step)`. Lowers to an
    // unrolled `Term::Application`-style chain when `n` is a const
    // literal at or below `pipeline::FOLD_UNROLL_THRESHOLD`; lowers to
    // `Term::Recurse` otherwise.
    if func_ident == "fold_n" {
        if call.args.len() != 3 {
            return Err(syn::Error::new(
                func_ident.span(),
                format!(
                    "closure violation: `fold_n` (G14) expects 3 arguments (count, init, step closure), got {}",
                    call.args.len()
                ),
            ));
        }
        // The count must be a const expression. The macro recognises
        // const integer literals (the unroll path) and any other
        // expression (the Term::Recurse path, with the count's tree as
        // the descent measure).
        let count_lit: Option<u64> = match &call.args[0] {
            syn::Expr::Lit(syn::ExprLit {
                lit: syn::Lit::Int(int_lit),
                ..
            }) => int_lit.base10_parse::<u64>().ok(),
            _ => None,
        };
        let init_root = emit_term_for_expr(&call.args[1], route_input, arena, scope)?;
        let step_closure = match &call.args[2] {
            syn::Expr::Closure(c) => c,
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `fold_n`'s third argument must be a closure `|state, idx| <step_expr>` (G14)",
                ));
            }
        };
        if step_closure.inputs.len() != 2 {
            return Err(syn::Error::new_spanned(
                step_closure,
                "closure violation: `fold_n`'s step closure expects exactly 2 parameters (state, idx) per G14",
            ));
        }
        let state_ident = match &step_closure.inputs[0] {
            syn::Pat::Ident(p) => p.ident.clone(),
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `fold_n`'s state parameter must be a plain identifier (G14)",
                ));
            }
        };
        let idx_ident = match &step_closure.inputs[1] {
            syn::Pat::Ident(p) => p.ident.clone(),
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `fold_n`'s idx parameter must be a plain identifier (G14)",
                ));
            }
        };
        // Unroll path: const literal at or below threshold.
        const FOLD_UNROLL_THRESHOLD: u64 = 8;
        if let Some(n) = count_lit {
            if n <= FOLD_UNROLL_THRESHOLD {
                let mut state_root = init_root;
                for i in 0..n {
                    let idx_root = arena.len();
                    arena.push(TermSpec::Literal(i));
                    let mut iter_scope = scope.clone();
                    iter_scope.shadow_check(&state_ident)?;
                    iter_scope.shadow_check(&idx_ident)?;
                    iter_scope.push(state_ident.clone(), state_root);
                    iter_scope.push(idx_ident.clone(), idx_root);
                    state_root = emit_term_for_expr(
                        &step_closure.body,
                        route_input,
                        arena,
                        &mut iter_scope,
                    )?;
                }
                return Ok(state_root);
            }
        }
        // Recurse path: count is parametric or exceeds the threshold.
        // Lower to Term::Recurse with the count's tree as descent measure,
        // init as base, and the step body as the step subtree.
        let measure_root = emit_term_for_expr(&call.args[0], route_input, arena, scope)?;
        let mut step_scope = scope.clone();
        step_scope.shadow_check(&state_ident)?;
        step_scope.shadow_check(&idx_ident)?;
        // Bind state to the recursive-call placeholder (the Recurse node
        // we're about to push); idx binds to the measure.
        let recurse_idx_placeholder = arena.len() + 1; // body emits before Recurse
        step_scope.push(state_ident, recurse_idx_placeholder);
        step_scope.push(idx_ident, measure_root);
        let step_root =
            emit_term_for_expr(&step_closure.body, route_input, arena, &mut step_scope)?;
        let idx = arena.len();
        arena.push(TermSpec::Recurse {
            measure_index: measure_root as u32,
            base_index: init_root as u32,
            step_index: step_root as u32,
        });
        return Ok(idx);
    }

    // ADR-022 D3 G7: `recurse(measure, base, |self_ident| step)`.
    if func_ident == "recurse" {
        if call.args.len() != 3 {
            return Err(syn::Error::new(
                func_ident.span(),
                format!(
                    "closure violation: `recurse` (G7) expects 3 arguments (measure, base, step closure), got {}",
                    call.args.len()
                ),
            ));
        }
        let measure_root = emit_term_for_expr(&call.args[0], route_input, arena, scope)?;
        let base_root = emit_term_for_expr(&call.args[1], route_input, arena, scope)?;
        // Third arg is a closure `|self_ident| step`.
        let step_closure = match &call.args[2] {
            syn::Expr::Closure(c) => c,
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `recurse`'s third argument must be a closure `|self_ident| <step_expr>` (G7)",
                ));
            }
        };
        if step_closure.inputs.len() != 1 {
            return Err(syn::Error::new_spanned(
                step_closure,
                "closure violation: `recurse`'s step closure expects exactly 1 parameter (the recursive-call placeholder, G7)",
            ));
        }
        let self_ident = match &step_closure.inputs[0] {
            syn::Pat::Ident(p) => p.ident.clone(),
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `recurse`'s step parameter must be a plain identifier (G7)",
                ));
            }
        };
        // The step body resolves `self_ident` references through the
        // binding scope; we register a fresh binding pointing at the
        // current arena position (which will be the Recurse node) so
        // self-references emit Variable lookups that the catamorphism
        // interprets as recursive calls per ADR-029 Recurse fold rule.
        let mut step_scope = scope.clone();
        step_scope.shadow_check(&self_ident)?;
        let recurse_idx_placeholder = arena.len() + 1; // body emits before the Recurse node
        step_scope.push(self_ident, recurse_idx_placeholder);
        let step_root =
            emit_term_for_expr(&step_closure.body, route_input, arena, &mut step_scope)?;
        let idx = arena.len();
        arena.push(TermSpec::Recurse {
            measure_index: measure_root as u32,
            base_index: base_root as u32,
            step_index: step_root as u32,
        });
        return Ok(idx);
    }

    // ADR-022 D3 G8: `unfold(seed, |state_ident| step)`.
    if func_ident == "unfold" {
        if call.args.len() != 2 {
            return Err(syn::Error::new(
                func_ident.span(),
                format!(
                    "closure violation: `unfold` (G8) expects 2 arguments (seed, step closure), got {}",
                    call.args.len()
                ),
            ));
        }
        let seed_root = emit_term_for_expr(&call.args[0], route_input, arena, scope)?;
        let step_closure = match &call.args[1] {
            syn::Expr::Closure(c) => c,
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `unfold`'s second argument must be a closure `|state_ident| <step_expr>` (G8)",
                ));
            }
        };
        if step_closure.inputs.len() != 1 {
            return Err(syn::Error::new_spanned(
                step_closure,
                "closure violation: `unfold`'s step closure expects exactly 1 parameter (the state placeholder, G8)",
            ));
        }
        let state_ident = match &step_closure.inputs[0] {
            syn::Pat::Ident(p) => p.ident.clone(),
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `unfold`'s step parameter must be a plain identifier (G8)",
                ));
            }
        };
        let mut step_scope = scope.clone();
        step_scope.shadow_check(&state_ident)?;
        step_scope.push(state_ident, seed_root);
        let step_root =
            emit_term_for_expr(&step_closure.body, route_input, arena, &mut step_scope)?;
        let idx = arena.len();
        arena.push(TermSpec::Unfold {
            seed_index: seed_root as u32,
            step_index: step_root as u32,
        });
        return Ok(idx);
    }

    // ADR-026 G13: `parallel(f, g)` produces the parallel-composed
    // route. The result's term tree is the partition-product of f's
    // and g's term trees: each operand's subtree is emitted, and the
    // composite is realised as a binary `Term::Application` whose
    // operator is the structural-combine `Or` (the foundation-default
    // partition-product byte combiner per the ten-Term-variant
    // commitment of ADR-029; implementations override the runtime per
    // ADR-024's three-way split if they need parallel-execution
    // semantics). The macro recognises `parallel(f, g)` so the verb-
    // closure check + the operator set's closure both hold.
    if func_ident == "parallel" {
        if call.args.len() != 2 {
            return Err(syn::Error::new(
                func_ident.span(),
                format!(
                    "closure violation: `parallel` (G13) expects 2 routes (left, right), got {}",
                    call.args.len()
                ),
            ));
        }
        let lhs_root = emit_term_for_expr(&call.args[0], route_input, arena, scope)?;
        let rhs_root = emit_term_for_expr(&call.args[1], route_input, arena, scope)?;
        // The args block must be contiguous in the arena per ADR-022 D2.
        // Build a contiguous duplicate block at the end if the operands
        // aren't already adjacent.
        let already_contiguous = rhs_root == lhs_root + 1;
        let (args_start, args_len) = if already_contiguous {
            (lhs_root as u32, 2u32)
        } else {
            let start = arena.len();
            let lhs_dup = clone_term_spec(&arena[lhs_root]);
            arena.push(lhs_dup);
            let rhs_dup = clone_term_spec(&arena[rhs_root]);
            arena.push(rhs_dup);
            (start as u32, 2u32)
        };
        let idx = arena.len();
        arena.push(TermSpec::Application {
            operator: quote! { ::uor_foundation::PrimitiveOp::Or },
            args_start,
            args_len,
        });
        return Ok(idx);
    }

    // ADR-026 G15: `tree_fold(reducer, [a, b, c, …])` lowers to a
    // pairwise reduction chain — at each level, the reducer is applied
    // to adjacent operand pairs, halving the count. For a power-of-two
    // count `n`, the output is a balanced tree of depth `log2(n)`. For
    // odd levels, the unpaired leaf is carried forward. The reducer is
    // a binary identifier (PrimitiveOp or verb).
    if func_ident == "tree_fold" {
        if call.args.len() != 2 {
            return Err(syn::Error::new(
                func_ident.span(),
                format!(
                    "closure violation: `tree_fold` (G15) expects 2 arguments (reducer, leaves array), got {}",
                    call.args.len()
                ),
            ));
        }
        // The reducer is an identifier (PrimitiveOp like `add` or a verb).
        let reducer_ident = match &call.args[0] {
            syn::Expr::Path(p) => p.path.get_ident().cloned().ok_or_else(|| {
                syn::Error::new_spanned(
                    &call.args[0],
                    "closure violation: `tree_fold`'s reducer must be a bare identifier (PrimitiveOp or verb)",
                )
            })?,
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `tree_fold`'s reducer must be a bare identifier",
                ));
            }
        };
        // The leaves are an array literal `[expr, expr, …]`.
        let leaves_array = match &call.args[1] {
            syn::Expr::Array(a) => a,
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `tree_fold`'s leaves must be an array literal `[a, b, c, …]`",
                ));
            }
        };
        if leaves_array.elems.is_empty() {
            return Err(syn::Error::new_spanned(
                leaves_array,
                "closure violation: `tree_fold`'s leaves array must be non-empty (G15)",
            ));
        }
        // Emit each leaf's subtree, recording its root index.
        let mut current_level: Vec<usize> = Vec::with_capacity(leaves_array.elems.len());
        for leaf_expr in &leaves_array.elems {
            current_level.push(emit_term_for_expr(leaf_expr, route_input, arena, scope)?);
        }
        // The reducer is rendered via emit_term_for_call's path (via a
        // synthesized two-arg call) so the same identifier-resolution
        // applies (PrimitiveOp / verb / closure violation).
        let reducer_op_or_verb = match reducer_ident.to_string().as_str() {
            "add" => Some(quote! { ::uor_foundation::PrimitiveOp::Add }),
            "sub" => Some(quote! { ::uor_foundation::PrimitiveOp::Sub }),
            "mul" => Some(quote! { ::uor_foundation::PrimitiveOp::Mul }),
            "xor" => Some(quote! { ::uor_foundation::PrimitiveOp::Xor }),
            "and" => Some(quote! { ::uor_foundation::PrimitiveOp::And }),
            "or" => Some(quote! { ::uor_foundation::PrimitiveOp::Or }),
            _ => None,
        };
        // Pairwise reduction: at each level, fold adjacent pairs.
        while current_level.len() > 1 {
            let mut next_level: Vec<usize> = Vec::with_capacity(current_level.len().div_ceil(2));
            let mut i = 0;
            while i + 1 < current_level.len() {
                let l_idx = current_level[i];
                let r_idx = current_level[i + 1];
                // Build the reducer application; args must be contiguous.
                let already_contiguous = r_idx == l_idx + 1;
                let (args_start, args_len) = if already_contiguous {
                    (l_idx as u32, 2u32)
                } else {
                    let start = arena.len();
                    let l_dup = clone_term_spec(&arena[l_idx]);
                    arena.push(l_dup);
                    let r_dup = clone_term_spec(&arena[r_idx]);
                    arena.push(r_dup);
                    (start as u32, 2u32)
                };
                let app_idx = arena.len();
                if let Some(op) = &reducer_op_or_verb {
                    arena.push(TermSpec::Application {
                        operator: op.clone(),
                        args_start,
                        args_len,
                    });
                } else {
                    // Verb-style reducer: emit a VerbSplice. The verb's
                    // term-tree fragment will be inlined at compile time.
                    // The verb call takes the LEFT operand as its arg per
                    // ADR-024's substitution semantics; the right operand
                    // is fed via a wrapping Application (Or as combine).
                    // For tree_fold over verbs, the verb must be unary; if
                    // used here as binary, we wrap via Or.
                    let const_name = Ident::new(
                        &format!(
                            "VERB_TERMS_{}",
                            to_screaming_snake(&reducer_ident.to_string())
                        ),
                        reducer_ident.span(),
                    );
                    let fragment_path = quote! { #const_name };
                    arena.push(TermSpec::VerbSplice {
                        arg_root_idx: l_idx as u32,
                        fragment_path,
                    });
                    let _ = (args_start, args_len, r_idx);
                }
                next_level.push(app_idx);
                i += 2;
            }
            // Carry an unpaired final leaf to the next level.
            if i < current_level.len() {
                next_level.push(current_level[i]);
            }
            current_level = next_level;
        }
        return Ok(current_level[0]);
    }

    // ADR-026 G16: `first_admit(<domain_type>, |i| pred)` lowers to a
    // structural declaration over the domain's successor structure.
    // Foundation emits `Term::Recurse { measure, base, step }` where:
    //   - measure: a Literal carrying the domain's cardinality (foundation
    //     reads the type-level `<DomainTy as ConstrainedTypeShape>::SITE_COUNT`
    //     when available; otherwise uses W8's 256 as a default ceiling)
    //   - base: a Literal(0) sentinel (zero meaning "not found", matching
    //     Term::Recurse's measure-zero termination semantics)
    //   - step: the predicate's term tree, evaluated at the recursive call
    //     placeholder bound to the iteration index
    // Implementations override the runtime per ADR-024 to provide actual
    // search; foundation's catamorphism walks the declaration.
    if func_ident == "first_admit" {
        if call.args.len() != 2 {
            return Err(syn::Error::new(
                func_ident.span(),
                format!(
                    "closure violation: `first_admit` (G16) expects 2 arguments (domain, predicate closure), got {}",
                    call.args.len()
                ),
            ));
        }
        let _domain_ty = match &call.args[0] {
            syn::Expr::Path(_) => &call.args[0],
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `first_admit`'s first argument must be a domain type path (e.g., `WittLevel::W8`)",
                ));
            }
        };
        let pred_closure = match &call.args[1] {
            syn::Expr::Closure(c) => c,
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `first_admit`'s second argument must be a closure `|i| <predicate_body>` (G16)",
                ));
            }
        };
        if pred_closure.inputs.len() != 1 {
            return Err(syn::Error::new_spanned(
                pred_closure,
                "closure violation: `first_admit`'s predicate closure expects exactly 1 parameter (the iteration index, G16)",
            ));
        }
        let idx_ident = match &pred_closure.inputs[0] {
            syn::Pat::Ident(p) => p.ident.clone(),
            other => {
                return Err(syn::Error::new_spanned(
                    other,
                    "closure violation: `first_admit`'s index parameter must be a plain identifier (G16)",
                ));
            }
        };
        // Emit the descent measure as a Literal carrying the domain's
        // cardinality. Foundation uses 256 as the W8 default; the macro
        // doesn't introspect <DomainTy as ConstrainedTypeShape> at proc-
        // macro time, so we encode 256 as the ceiling and let
        // implementations override per ADR-024.
        let measure_root = arena.len();
        arena.push(TermSpec::Literal(256));
        // Base case: Literal(0) — "no admitting index found" sentinel.
        let base_root = arena.len();
        arena.push(TermSpec::Literal(0));
        // Step: the predicate's term tree, with idx_ident bound to the
        // current iteration via the binding scope (Variable lookup).
        let mut step_scope = scope.clone();
        step_scope.shadow_check(&idx_ident)?;
        // The recursive-call placeholder for first_admit IS the next
        // iteration index (which the implementation runtime increments).
        // Foundation binds idx_ident to the measure root for now; the
        // structural declaration is what matters per ADR-024.
        step_scope.push(idx_ident, measure_root);
        let step_root =
            emit_term_for_expr(&pred_closure.body, route_input, arena, &mut step_scope)?;
        let idx = arena.len();
        arena.push(TermSpec::Recurse {
            measure_index: measure_root as u32,
            base_index: base_root as u32,
            step_index: step_root as u32,
        });
        return Ok(idx);
    }

    // ADR-026 G19: `hash(input)` lowers to `Term::HasherProjection`.
    if func_ident == "hash" {
        if call.args.len() != 1 {
            return Err(syn::Error::new(
                func_ident.span(),
                format!(
                    "closure violation: `hash` (ADR-026 G19) expects 1 argument, got {}",
                    call.args.len()
                ),
            ));
        }
        let input_root = emit_term_for_expr(&call.args[0], route_input, arena, scope)?;
        let idx = arena.len();
        arena.push(TermSpec::HasherProjection {
            input_index: input_root as u32,
        });
        return Ok(idx);
    }

    let (operator, expected_arity) = match func_ident.to_string().as_str() {
        "add" => (quote! { ::uor_foundation::PrimitiveOp::Add }, 2usize),
        "sub" => (quote! { ::uor_foundation::PrimitiveOp::Sub }, 2),
        "mul" => (quote! { ::uor_foundation::PrimitiveOp::Mul }, 2),
        "xor" => (quote! { ::uor_foundation::PrimitiveOp::Xor }, 2),
        "and" => (quote! { ::uor_foundation::PrimitiveOp::And }, 2),
        "or" => (quote! { ::uor_foundation::PrimitiveOp::Or }, 2),
        "neg" => (quote! { ::uor_foundation::PrimitiveOp::Neg }, 1),
        "bnot" => (quote! { ::uor_foundation::PrimitiveOp::Bnot }, 1),
        "succ" => (quote! { ::uor_foundation::PrimitiveOp::Succ }, 1),
        "pred" => (quote! { ::uor_foundation::PrimitiveOp::Pred }, 1),
        // ADR-026 reserved macro-vocabulary identifiers (G13–G18). The
        // closure-body lowering for these forms is specified
        // architecturally; the substrate-level macro recognises them so
        // they never fall through to the closure-violation branch as
        // unknown identifiers, but the structural lowering is owned by
        // the implementation (per ADR-024's three-way responsibility split
        // between substrate, prism, and implementation). Implementations
        // that need these forms supply their own SDK macros that desugar
        // into the substrate primitives; the substrate macro reserves the
        // identifiers so they cannot be re-used as `verb!` names.
        "partition_product" | "partition_coproduct" => {
            return Err(syn::Error::new(
                func_ident.span(),
                format!(
                    "closure violation: `{}` (ADR-026 G17/G18) is a type-level shape constructor — invoke it at item position via the named SDK form `partition_product!(<Name>, <A>, <B>)` or `partition_coproduct!(<Name>, <A>, <B>)`, then reference `<Name>` in `type Input` / `type Output`",
                    func_ident
                ),
            ));
        }
        other => {
            return Err(syn::Error::new(
                func_ident.span(),
                format!(
                    "closure violation: `{other}` is not a foundation PrimitiveOp (recognised: add, sub, mul, xor, and, or, neg, bnot, succ, pred), nor an ADR-026 macro-vocabulary identifier (hash/parallel/fold_n/tree_fold/first_admit/recurse/unfold), nor a declared verb"
                ),
            ));
        }
    };

    if call.args.len() != expected_arity {
        return Err(syn::Error::new(
            func_ident.span(),
            format!(
                "PrimitiveOp `{}` expects {} argument(s), got {}",
                func_ident,
                expected_arity,
                call.args.len()
            ),
        ));
    }

    // Emit each arg's subtree and record its root index.
    let mut arg_root_indices: Vec<usize> = Vec::with_capacity(call.args.len());
    for arg in call.args.iter() {
        arg_root_indices.push(emit_term_for_expr(arg, route_input, arena, scope)?);
    }

    // ADR-022 D2: the args block must be CONTIGUOUS in the arena. If
    // the arg roots already are (the common case for leaf args or for
    // the canonical post-order layout), use them directly. Otherwise
    // duplicate each arg's root term into a fresh contiguous block —
    // a duplicate carries the same `Term` value (same operator + same
    // args.start), so it is semantically identical.
    let already_contiguous = arg_root_indices.windows(2).all(|w| w[1] == w[0] + 1);

    let (args_start, args_len) = if already_contiguous && !arg_root_indices.is_empty() {
        let len = arg_root_indices.len();
        let start = arg_root_indices[0];
        (start as u32, len as u32)
    } else {
        // Build a contiguous duplicate block at the end of the arena.
        let start = arena.len();
        for &idx in &arg_root_indices {
            // Clone the spec at idx into a new slot. Since TermSpec is
            // not Clone, hand-build a fresh entry referring to the same
            // contents. (Operators are token streams; clone via .clone()
            // on the field.)
            let dup = match &arena[idx] {
                TermSpec::Literal(v) => TermSpec::Literal(*v),
                TermSpec::Variable => TermSpec::Variable,
                TermSpec::Application {
                    operator,
                    args_start,
                    args_len,
                } => TermSpec::Application {
                    operator: operator.clone(),
                    args_start: *args_start,
                    args_len: *args_len,
                },
                TermSpec::HasherProjection { input_index } => TermSpec::HasherProjection {
                    input_index: *input_index,
                },
                TermSpec::VerbSplice {
                    arg_root_idx,
                    fragment_path,
                } => TermSpec::VerbSplice {
                    arg_root_idx: *arg_root_idx,
                    fragment_path: fragment_path.clone(),
                },
                TermSpec::Lift {
                    operand_index,
                    target_witt,
                } => TermSpec::Lift {
                    operand_index: *operand_index,
                    target_witt: target_witt.clone(),
                },
                TermSpec::Project {
                    operand_index,
                    target_witt,
                } => TermSpec::Project {
                    operand_index: *operand_index,
                    target_witt: target_witt.clone(),
                },
                TermSpec::Try { body_index } => TermSpec::Try {
                    body_index: *body_index,
                },
                TermSpec::Recurse {
                    measure_index,
                    base_index,
                    step_index,
                } => TermSpec::Recurse {
                    measure_index: *measure_index,
                    base_index: *base_index,
                    step_index: *step_index,
                },
                TermSpec::Unfold {
                    seed_index,
                    step_index,
                } => TermSpec::Unfold {
                    seed_index: *seed_index,
                    step_index: *step_index,
                },
                TermSpec::Match {
                    scrutinee_index,
                    arms_start,
                    arms_len,
                } => TermSpec::Match {
                    scrutinee_index: *scrutinee_index,
                    arms_start: *arms_start,
                    arms_len: *arms_len,
                },
                TermSpec::WildcardSentinel => TermSpec::WildcardSentinel,
            };
            arena.push(dup);
        }
        (start as u32, arg_root_indices.len() as u32)
    };

    let app_idx = arena.len();
    arena.push(TermSpec::Application {
        operator,
        args_start,
        args_len,
    });
    Ok(app_idx)
}

/// Emit the macro-time-built term arena as a sequence of `Term::*`
/// constructor expressions, ready to splice into a `&'static [Term]`
/// const-array literal.
fn render_arena(arena: &[TermSpec]) -> Vec<proc_macro2::TokenStream> {
    arena
        .iter()
        .map(|spec| match spec {
            TermSpec::Literal(value) => quote! {
                ::uor_foundation::enforcement::Term::Literal {
                    value: #value,
                    level: ::uor_foundation::WittLevel::W8,
                }
            },
            TermSpec::Variable => quote! {
                ::uor_foundation::enforcement::Term::Variable { name_index: 0u32 }
            },
            TermSpec::Application {
                operator,
                args_start,
                args_len,
            } => {
                let s = *args_start;
                let l = *args_len;
                quote! {
                    ::uor_foundation::enforcement::Term::Application {
                        operator: #operator,
                        args: ::uor_foundation::enforcement::TermList {
                            start: #s,
                            len: #l,
                        },
                    }
                }
            }
            TermSpec::HasherProjection { input_index } => {
                let i = *input_index;
                quote! {
                    ::uor_foundation::enforcement::Term::HasherProjection {
                        input_index: #i,
                    }
                }
            }
            TermSpec::VerbSplice { .. } => {
                // VerbSplice never reaches the slice-literal renderer:
                // when an arena contains a VerbSplice the caller falls
                // back to `render_const_fn_arena_builder` which inlines
                // the verb fragment via foundation's const-fn helper
                // `inline_verb_fragment` at const-eval time per
                // ADR-024. Reaching this branch indicates a logic bug
                // in the macro's emission selection.
                quote! {
                    compile_error!(
                        "internal error: VerbSplice reached the slice-literal renderer; \
                         render_const_fn_arena_builder should have been chosen"
                    )
                }
            }
            TermSpec::Lift {
                operand_index,
                target_witt,
            } => {
                let i = *operand_index;
                quote! {
                    ::uor_foundation::enforcement::Term::Lift {
                        operand_index: #i,
                        target: #target_witt,
                    }
                }
            }
            TermSpec::Project {
                operand_index,
                target_witt,
            } => {
                let i = *operand_index;
                quote! {
                    ::uor_foundation::enforcement::Term::Project {
                        operand_index: #i,
                        target: #target_witt,
                    }
                }
            }
            TermSpec::Try { body_index } => {
                let i = *body_index;
                quote! {
                    ::uor_foundation::enforcement::Term::Try {
                        body_index: #i,
                        handler_index: u32::MAX,
                    }
                }
            }
            TermSpec::Recurse {
                measure_index,
                base_index,
                step_index,
            } => {
                let m = *measure_index;
                let b = *base_index;
                let s = *step_index;
                quote! {
                    ::uor_foundation::enforcement::Term::Recurse {
                        measure_index: #m,
                        base_index: #b,
                        step_index: #s,
                    }
                }
            }
            TermSpec::Unfold {
                seed_index,
                step_index,
            } => {
                let s = *seed_index;
                let st = *step_index;
                quote! {
                    ::uor_foundation::enforcement::Term::Unfold {
                        seed_index: #s,
                        step_index: #st,
                    }
                }
            }
            TermSpec::Match {
                scrutinee_index,
                arms_start,
                arms_len,
            } => {
                let s = *scrutinee_index;
                let st = *arms_start;
                let l = *arms_len;
                quote! {
                    ::uor_foundation::enforcement::Term::Match {
                        scrutinee_index: #s,
                        arms: ::uor_foundation::enforcement::TermList {
                            start: #st,
                            len: #l,
                        },
                    }
                }
            }
            TermSpec::WildcardSentinel => quote! {
                ::uor_foundation::enforcement::Term::Variable {
                    name_index: u32::MAX,
                }
            },
        })
        .collect()
}

/// Render a single non-VerbSplice TermSpec as a `Term::*` constructor
/// expression that uses the dynamic `len` variable for index fields
/// when those fields reference the spec at the given TermSpec index.
/// `spec_pos[i]` is the TokenStream for spec `i`'s result-position
/// const-let (e.g., `pos_3` for atomic specs, `len - 1` for verb
/// splices' last term).
fn render_atomic_term_in_builder(
    spec: &TermSpec,
    spec_pos: &[proc_macro2::TokenStream],
) -> proc_macro2::TokenStream {
    let pos_at = |idx: u32| -> proc_macro2::TokenStream {
        let i = idx as usize;
        if i < spec_pos.len() {
            spec_pos[i].clone()
        } else {
            // Out-of-bounds index — emit u32::MAX so const-eval surfaces a
            // recognizable arena-bounds error.
            quote! { u32::MAX }
        }
    };
    match spec {
        TermSpec::Literal(value) => {
            let v = *value;
            quote! {
                ::uor_foundation::enforcement::Term::Literal {
                    value: #v,
                    level: ::uor_foundation::WittLevel::W8,
                }
            }
        }
        TermSpec::Variable => quote! {
            ::uor_foundation::enforcement::Term::Variable { name_index: 0u32 }
        },
        TermSpec::Application {
            operator,
            args_start,
            args_len,
        } => {
            let s = pos_at(*args_start);
            let l = *args_len;
            quote! {
                ::uor_foundation::enforcement::Term::Application {
                    operator: #operator,
                    args: ::uor_foundation::enforcement::TermList {
                        start: (#s) as u32,
                        len: #l,
                    },
                }
            }
        }
        TermSpec::HasherProjection { input_index } => {
            let i = pos_at(*input_index);
            quote! {
                ::uor_foundation::enforcement::Term::HasherProjection {
                    input_index: (#i) as u32,
                }
            }
        }
        TermSpec::Lift {
            operand_index,
            target_witt,
        } => {
            let i = pos_at(*operand_index);
            quote! {
                ::uor_foundation::enforcement::Term::Lift {
                    operand_index: (#i) as u32,
                    target: #target_witt,
                }
            }
        }
        TermSpec::Project {
            operand_index,
            target_witt,
        } => {
            let i = pos_at(*operand_index);
            quote! {
                ::uor_foundation::enforcement::Term::Project {
                    operand_index: (#i) as u32,
                    target: #target_witt,
                }
            }
        }
        TermSpec::Try { body_index } => {
            let i = pos_at(*body_index);
            quote! {
                ::uor_foundation::enforcement::Term::Try {
                    body_index: (#i) as u32,
                    handler_index: u32::MAX,
                }
            }
        }
        TermSpec::Recurse {
            measure_index,
            base_index,
            step_index,
        } => {
            let m = pos_at(*measure_index);
            let b = pos_at(*base_index);
            let s = pos_at(*step_index);
            quote! {
                ::uor_foundation::enforcement::Term::Recurse {
                    measure_index: (#m) as u32,
                    base_index: (#b) as u32,
                    step_index: (#s) as u32,
                }
            }
        }
        TermSpec::Unfold {
            seed_index,
            step_index,
        } => {
            let s = pos_at(*seed_index);
            let st = pos_at(*step_index);
            quote! {
                ::uor_foundation::enforcement::Term::Unfold {
                    seed_index: (#s) as u32,
                    step_index: (#st) as u32,
                }
            }
        }
        TermSpec::Match {
            scrutinee_index,
            arms_start,
            arms_len,
        } => {
            let sc = pos_at(*scrutinee_index);
            let st = *arms_start;
            let l = *arms_len;
            // For Match, arms are emitted as a contiguous span at fixed
            // positional offsets (the macro emits them sequentially in
            // the host arena); arms.start references the first such
            // position which lives at the static spec-index `st`.
            let st_pos = if (st as usize) < spec_pos.len() {
                spec_pos[st as usize].clone()
            } else {
                quote! { u32::MAX }
            };
            quote! {
                ::uor_foundation::enforcement::Term::Match {
                    scrutinee_index: (#sc) as u32,
                    arms: ::uor_foundation::enforcement::TermList {
                        start: (#st_pos) as u32,
                        len: #l,
                    },
                }
            }
        }
        TermSpec::WildcardSentinel => quote! {
            ::uor_foundation::enforcement::Term::Variable { name_index: u32::MAX }
        },
        TermSpec::VerbSplice { .. } => quote! {
            compile_error!("VerbSplice handled separately in render_const_fn_arena_builder")
        },
    }
}

/// Render the TermSpec arena as a const-fn arena builder when the arena
/// contains verb splices (wiki ADR-024). The builder emits a sequence
/// of statements in a const block that:
///
///   - allocates a fixed-capacity `[Term; CAP]` buffer
///   - emits each TermSpec as either a direct `buf[len] = Term::...; len += 1;`
///     (for atomic specs) or a `inline_verb_fragment` call (for verb splices)
///   - tracks each spec's result position via `pos_<N>` const-let bindings
///     so subsequent specs reference verb-spliced positions correctly
///   - returns `(buf, len)` and exposes `&buf[..len]` as the route's
///     `&'static [Term]` slice
fn render_const_fn_arena_builder(arena: &[TermSpec]) -> proc_macro2::TokenStream {
    // Step 1: compute each spec's result-position TokenStream. For
    // atomic specs, the position is a fresh `pos_<N>` const-let. For
    // VerbSplice specs, the position is `len - 1` evaluated AFTER the
    // splice (the last term of the spliced fragment is the verb's
    // result root per ADR-024).
    let spec_pos: Vec<proc_macro2::TokenStream> = (0..arena.len())
        .map(|i| {
            let id = Ident::new(&format!("pos_{}", i), proc_macro2::Span::call_site());
            quote! { #id }
        })
        .collect();

    // Step 2: emit the build-step statements per spec.
    let mut stmts: Vec<proc_macro2::TokenStream> = Vec::with_capacity(arena.len());
    for (i, spec) in arena.iter().enumerate() {
        let pos_id = &spec_pos[i];
        match spec {
            TermSpec::VerbSplice {
                arg_root_idx,
                fragment_path,
            } => {
                // The caller's argument expression's root position is
                // captured in `pos_<arg_root_idx>`. inline_verb_fragment
                // substitutes Variable(0) in the verb's body with a copy
                // of `buf[arg_pos]` and shifts non-Variable(0) terms by
                // the host's current length per ADR-024.
                let arg_pos = &spec_pos[*arg_root_idx as usize];
                stmts.push(quote! {
                    let __spliced = ::uor_foundation::enforcement::inline_verb_fragment(
                        buf,
                        len,
                        #fragment_path,
                        (#arg_pos) as u32,
                    );
                    buf = __spliced.0;
                    len = __spliced.1;
                    let #pos_id: usize = len - 1;
                });
            }
            other => {
                let term_expr = render_atomic_term_in_builder(other, &spec_pos);
                stmts.push(quote! {
                    buf[len] = #term_expr;
                    let #pos_id: usize = len;
                    len += 1;
                });
            }
        }
    }

    // Step 3: assemble the const-fn block. Cap the arena at a generous
    // foundation default; const-eval will reject overflows.
    quote! {
        {
            const ROUTE_ARENA_CAP: usize = 256;
            const fn __build_arena() -> ([::uor_foundation::enforcement::Term; ROUTE_ARENA_CAP], usize) {
                let mut buf: [::uor_foundation::enforcement::Term; ROUTE_ARENA_CAP] =
                    [::uor_foundation::enforcement::Term::Variable { name_index: 0u32 }; ROUTE_ARENA_CAP];
                let mut len: usize = 0;
                #( #stmts )*
                (buf, len)
            }
            const ROUTE_BUILT: ([::uor_foundation::enforcement::Term; ROUTE_ARENA_CAP], usize) =
                __build_arena();
            const ROUTE_LEN: usize = ROUTE_BUILT.1;
            // Slice the active prefix; const split_at_checked is stable on Rust 1.83.
            match ROUTE_BUILT.0.split_at_checked(ROUTE_LEN) {
                Some((head, _)) => head,
                None => &[],
            }
        }
    }
}

/// `prism_model!` — wiki ADR-020 + ADR-022 D3 closure-bodied form.
///
/// Parses the model declaration (struct, route witness struct, impl block
/// with `Input` / `Output` / `Route` associated types and a closure-bodied
/// `route` function), maps the closure body to a foundation-vocabulary
/// term tree at expansion time, and emits:
///
/// - `pub struct <Model>;` and `pub struct <Route>;` (re-emitted from input)
/// - `const ROUTE_TERMS_<MODEL>: &'static [Term] = &[…];` (the term tree)
/// - `impl __sdk_seal::Sealed for <Model>` and `for <Route>` (D1)
/// - `impl FoundationClosed for <Route> { arena_slice() → ROUTE_TERMS_<MODEL> }` (D5)
/// - `impl PrismModel<H, B, A> for <Model>` with `forward` body delegating
///   to `pipeline::run_route::<H, B, A, Self>(input)` (D4 + D5)
///
/// A function call to a name not in the foundation PrimitiveOp catalogue
/// (add, sub, mul, xor, and, or, neg, bnot, succ, pred) fails to compile,
/// pointing at the offending span — the wiki's closure-violation
/// enforcement (ADR-020).
#[proc_macro]
pub fn prism_model(input: TokenStream) -> TokenStream {
    let parsed = parse_macro_input!(input as PrismModelInput);
    let PrismModelInput {
        model_vis,
        model_name,
        route_vis,
        route_name,
        h_ty,
        b_ty,
        a_ty,
        input_ty,
        output_ty,
        route_input_ident,
        route_body,
    } = parsed;

    // Walk the closure body — the macro-time mapping that ADR-020 / D3
    // names. The body is processed via the block handler so `let`
    // bindings (G10) and the trailing tail expression (G11) are both
    // recognised.
    let mut arena: Vec<TermSpec> = Vec::new();
    let mut scope = BindingScope::default();
    if let Err(e) = emit_term_for_block(&route_body, &route_input_ident, &mut arena, &mut scope) {
        return e.to_compile_error().into();
    }

    // Per wiki ADR-024, verb fragments are inlined into the route's
    // arena at compile time via the const-fn arena builder when any
    // verb invocation is present. Pure (verb-free) routes use the
    // simple slice-literal form.
    let route_has_verb_splices = arena
        .iter()
        .any(|s| matches!(s, TermSpec::VerbSplice { .. }));
    let route_arena_expr = if route_has_verb_splices {
        render_const_fn_arena_builder(&arena)
    } else {
        let term_specs = render_arena(&arena);
        quote! { &[ #( #term_specs ),* ] }
    };

    // Synthesize a unique const name from the model's identifier so two
    // models in the same module don't clash on `ROUTE_TERMS`.
    let route_terms_const = Ident::new(
        &format!(
            "ROUTE_TERMS_FOR_{}",
            to_screaming_snake(&model_name.to_string())
        ),
        model_name.span(),
    );

    let expansion = quote! {
        // Re-emit the model + route witness structs from the input.
        #model_vis struct #model_name;
        #route_vis struct #route_name;

        // ADR-022 D2 + ADR-024: const term-tree slice. Macro-time-built,
        // with verb fragments inlined at compile time per ADR-024 (the
        // catamorphism walks a flat arena over the ten Term variants —
        // no runtime depth guard). `pipeline::run_route` reads the
        // slice via `FoundationClosed::arena_slice`.
        #[allow(non_upper_case_globals, dead_code)]
        const #route_terms_const: &[::uor_foundation::enforcement::Term] =
            #route_arena_expr;

        // ADR-022 D1: seal impls. Foundation-internal macro is the
        // only sanctioned producer outside foundation itself.
        impl ::uor_foundation::pipeline::__sdk_seal::Sealed for #model_name {}
        impl ::uor_foundation::pipeline::__sdk_seal::Sealed for #route_name {}

        // ADR-022 D5: FoundationClosed impl returning the parsed term-tree.
        impl ::uor_foundation::pipeline::FoundationClosed for #route_name {
            fn arena_slice() -> &'static [::uor_foundation::enforcement::Term] {
                #route_terms_const
            }
        }

        // ADR-020 + ADR-022 D4: PrismModel impl.
        impl ::uor_foundation::pipeline::PrismModel<#h_ty, #b_ty, #a_ty> for #model_name {
            type Input = #input_ty;
            type Output = #output_ty;
            type Route = #route_name;

            fn forward(
                input: <Self as ::uor_foundation::pipeline::PrismModel<#h_ty, #b_ty, #a_ty>>::Input,
            ) -> ::core::result::Result<
                ::uor_foundation::enforcement::Grounded<
                    <Self as ::uor_foundation::pipeline::PrismModel<#h_ty, #b_ty, #a_ty>>::Output,
                >,
                ::uor_foundation::PipelineFailure,
            > {
                ::uor_foundation::pipeline::run_route::<#h_ty, #b_ty, #a_ty, Self>(input)
            }
        }
    };

    expansion.into()
}

// =====================================================================
// `output_shape!` — wiki ADR-027.
//
// Generalizes `GroundedShape`'s seal: the foundation source seals the
// trait via `__sdk_seal::Sealed`, and the `output_shape!` SDK macro
// emits — alongside the application's `ConstrainedTypeShape` impl — the
// `__sdk_seal::Sealed`, `GroundedShape`, and `IntoBindingValue` impls
// gated on the seal. This widens the path applications can declare a
// custom Output shape without lifting the seal entirely.
//
// Macro form:
//
// ```text
// output_shape! {
//     pub struct OutputHash;
//     impl ConstrainedTypeShape for OutputHash {
//         const IRI: &'static str = "https://prism.btc/shape/OutputHash";
//         const SITE_COUNT: usize = 32;
//         const CONSTRAINTS: &'static [ConstraintRef] = &[];
//     }
// }
// ```
//
// Emissions (per ADR-027):
//   - `pub struct <Name>;` (re-emitted)
//   - `impl ConstrainedTypeShape for <Name>` (re-emitted)
//   - `impl __sdk_seal::Sealed for <Name>`
//   - `impl GroundedShape for <Name>`
//   - `impl IntoBindingValue for <Name>` with MAX_BYTES = SITE_COUNT
//     (byte-level granularity default; shapes whose Witt level is
//     greater than 8 bits use a wider per-site multiplier the
//     application sets via a custom `IntoBindingValue` impl).

/// Parsed shape of the macro input.
struct OutputShapeInput {
    struct_vis: syn::Visibility,
    struct_name: Ident,
    impl_iri: syn::LitStr,
    impl_site_count: syn::Expr,
    impl_constraints: syn::Expr,
}

impl Parse for OutputShapeInput {
    fn parse(input: ParseStream) -> Result<Self> {
        // `pub struct OutputHash;`
        let struct_vis: syn::Visibility = input.parse()?;
        input.parse::<Token![struct]>()?;
        let struct_name: Ident = input.parse()?;
        input.parse::<Token![;]>()?;

        // `impl ConstrainedTypeShape for OutputHash { ... }`
        input.parse::<Token![impl]>()?;
        let trait_ident: Ident = input.parse()?;
        if trait_ident != "ConstrainedTypeShape" {
            return Err(syn::Error::new(
                trait_ident.span(),
                "output_shape! expects `impl ConstrainedTypeShape for <Name>`",
            ));
        }
        input.parse::<Token![for]>()?;
        let target: Ident = input.parse()?;
        if target != struct_name {
            return Err(syn::Error::new(
                target.span(),
                "output_shape!'s `impl ConstrainedTypeShape for <Name>` target must match the declared struct",
            ));
        }

        let body;
        syn::braced!(body in input);

        // `const IRI: &'static str = "...";`
        body.parse::<Token![const]>()?;
        let kw_iri: Ident = body.parse()?;
        if kw_iri != "IRI" {
            return Err(syn::Error::new(
                kw_iri.span(),
                "expected `const IRI: &'static str = ...`",
            ));
        }
        body.parse::<Token![:]>()?;
        let _ty: syn::Type = body.parse()?;
        body.parse::<Token![=]>()?;
        let impl_iri: syn::LitStr = body.parse()?;
        body.parse::<Token![;]>()?;

        // `const SITE_COUNT: usize = ...;`
        body.parse::<Token![const]>()?;
        let kw_sc: Ident = body.parse()?;
        if kw_sc != "SITE_COUNT" {
            return Err(syn::Error::new(
                kw_sc.span(),
                "expected `const SITE_COUNT: usize = ...`",
            ));
        }
        body.parse::<Token![:]>()?;
        let _ty: syn::Type = body.parse()?;
        body.parse::<Token![=]>()?;
        let impl_site_count: syn::Expr = body.parse()?;
        body.parse::<Token![;]>()?;

        // `const CONSTRAINTS: &'static [ConstraintRef] = ...;`
        body.parse::<Token![const]>()?;
        let kw_cn: Ident = body.parse()?;
        if kw_cn != "CONSTRAINTS" {
            return Err(syn::Error::new(
                kw_cn.span(),
                "expected `const CONSTRAINTS: &'static [ConstraintRef] = ...`",
            ));
        }
        body.parse::<Token![:]>()?;
        let _ty: syn::Type = body.parse()?;
        body.parse::<Token![=]>()?;
        let impl_constraints: syn::Expr = body.parse()?;
        body.parse::<Token![;]>()?;

        Ok(Self {
            struct_vis,
            struct_name,
            impl_iri,
            impl_site_count,
            impl_constraints,
        })
    }
}

/// `output_shape!` — wiki ADR-027 custom Output shape declaration.
///
/// Emits the application-named struct, the `ConstrainedTypeShape` impl
/// (re-emitted from the user's body), and the additional impls
/// `__sdk_seal::Sealed`, `GroundedShape`, and `IntoBindingValue` so the
/// shape qualifies as a `PrismModel::Output`.
#[proc_macro]
pub fn output_shape(input: TokenStream) -> TokenStream {
    let parsed = parse_macro_input!(input as OutputShapeInput);
    let OutputShapeInput {
        struct_vis,
        struct_name,
        impl_iri,
        impl_site_count,
        impl_constraints,
    } = parsed;

    let expansion = quote! {
        // Re-emit the user's struct and ConstrainedTypeShape impl.
        #struct_vis struct #struct_name;

        impl ::uor_foundation::pipeline::ConstrainedTypeShape for #struct_name {
            const IRI: &'static str = #impl_iri;
            const SITE_COUNT: usize = #impl_site_count;
            const CONSTRAINTS: &'static [::uor_foundation::pipeline::ConstraintRef] =
                #impl_constraints;
        }

        // ADR-027 emissions: the four sealed-trait impls.
        impl ::uor_foundation::pipeline::__sdk_seal::Sealed for #struct_name {}
        impl ::uor_foundation::enforcement::GroundedShape for #struct_name {}
        impl ::uor_foundation::pipeline::IntoBindingValue for #struct_name {
            const MAX_BYTES: usize =
                <#struct_name as ::uor_foundation::pipeline::ConstrainedTypeShape>::SITE_COUNT;
            fn into_binding_bytes(
                &self,
                _out: &mut [u8],
            ) -> ::core::result::Result<usize, ::uor_foundation::enforcement::ShapeViolation> {
                // The output shape carries the catamorphism's evaluation result, not a
                // user-supplied input, so the input-side serialization is trivial.
                // Applications that re-use the output shape as a downstream model's
                // Input write a bespoke `IntoBindingValue` impl reflecting the bytes
                // they emit at runtime.
                Ok(0)
            }
        }
    };

    expansion.into()
}

// =====================================================================
// `verb!` — wiki ADR-024 Layer-3 implementation closure.
//
// An implementation declares a named, reusable composition of prism
// operators applied to substrate primitives. The macro:
//
//   - parses a closure-bodied function declaration
//     (`pub fn name(input: T) -> U { … }`)
//   - emits a `&'static [Term]` slice carrying the verb's term-tree
//     fragment (built via the same G1–G19 closure-body grammar as
//     `prism_model!`)
//   - emits a `pub fn name_term_arena() -> &'static [Term]` accessor
//     so `prism_model!` can reference the verb by name during
//     route-closure expansion
//
// Form:
//
// ```text
// verb! {
//     pub fn sha256_compression(input: BlockInput) -> CompressionState {
//         // closure body — same G1–G19 grammar as prism_model!
//         hash(input)
//     }
// }
// ```
//
// Per ADR-024's three-way responsibility split, the verb's runtime
// is implementation-owned: the term-tree fragment is the structural
// declaration; how an implementation evaluates it (sequential,
// parallel, optimised) is the implementation's choice. Foundation's
// `pipeline::run_route` evaluates verb-reachable Term trees per the
// per-variant fold-rules (ADR-029).

/// Parsed shape of the `verb!` macro input.
struct VerbInput {
    fn_vis: syn::Visibility,
    fn_name: Ident,
    input_param: Ident,
    input_ty: syn::Type,
    output_ty: syn::Type,
    body: syn::Block,
}

impl Parse for VerbInput {
    fn parse(input: ParseStream) -> Result<Self> {
        let fn_vis: syn::Visibility = input.parse()?;
        input.parse::<Token![fn]>()?;
        let fn_name: Ident = input.parse()?;
        let params;
        syn::parenthesized!(params in input);
        let input_param: Ident = params.parse()?;
        params.parse::<Token![:]>()?;
        let input_ty: syn::Type = params.parse()?;
        input.parse::<Token![->]>()?;
        let output_ty: syn::Type = input.parse()?;
        let body: syn::Block = input.parse()?;
        Ok(Self {
            fn_vis,
            fn_name,
            input_param,
            input_ty,
            output_ty,
            body,
        })
    }
}

/// `verb!` — wiki ADR-024 Layer-3 verb declaration. Emits a const
/// term-tree fragment and a public accessor.
#[proc_macro]
pub fn verb(input: TokenStream) -> TokenStream {
    let parsed = parse_macro_input!(input as VerbInput);
    let VerbInput {
        fn_vis,
        fn_name,
        input_param,
        input_ty,
        output_ty,
        body,
    } = parsed;

    let mut arena: Vec<TermSpec> = Vec::new();
    let mut scope = BindingScope::default();
    if let Err(e) = emit_term_for_block(&body, &input_param, &mut arena, &mut scope) {
        return e.to_compile_error().into();
    }

    // Wiki ADR-024 verb-closure check: a verb's body must not directly
    // reference itself. Self-recursion is the local cycle the macro can
    // detect at expansion time; cross-verb cycles surface at the
    // application's compile time during const-eval of the splicing
    // const-fn calls (Rust's const-eval rejects infinite recursion via
    // its const-step ceiling).
    let self_const_name = format!("VERB_TERMS_{}", to_screaming_snake(&fn_name.to_string()));
    for spec in &arena {
        if let TermSpec::VerbSplice { fragment_path, .. } = spec {
            if fragment_path.to_string().trim() == self_const_name {
                return syn::Error::new(
                    fn_name.span(),
                    format!(
                        "verb-closure violation (ADR-024): `{}`'s body references itself directly; the verb-reference graph through non-`recurse` operators must be acyclic. Lift the recursion through `recurse(...)` (G7) instead.",
                        fn_name
                    ),
                )
                .to_compile_error()
                .into();
            }
        }
    }

    // Determine the term-tree fragment representation: if the verb
    // body contains nested verb splices, we must emit a const-fn
    // builder that resolves the splices at const-eval time. For pure
    // (no nested splices) bodies, the simple slice literal works.
    let body_has_verb_splices = arena
        .iter()
        .any(|s| matches!(s, TermSpec::VerbSplice { .. }));
    let verb_fragment_expr = if body_has_verb_splices {
        render_const_fn_arena_builder(&arena)
    } else {
        let term_specs = render_arena(&arena);
        quote! { &[ #( #term_specs ),* ] }
    };

    let const_name = Ident::new(
        &format!("VERB_TERMS_{}", to_screaming_snake(&fn_name.to_string())),
        fn_name.span(),
    );
    let accessor_name = Ident::new(&format!("{}_term_arena", fn_name), fn_name.span());

    let expansion = quote! {
        // Const term-tree fragment, fully-const, ready for the verb's
        // accessor or for `prism_model!` to splice into a route arena
        // at compile time per wiki ADR-024. The const is `pub` so
        // `prism_model!` invocations in downstream crates (after
        // `use_verbs!` re-export) can name it when emitting calls to
        // foundation's `inline_verb_fragment` const-fn helper.
        #[allow(non_upper_case_globals, dead_code)]
        #fn_vis const #const_name: &[::uor_foundation::enforcement::Term] =
            #verb_fragment_expr;

        // Public accessor for the verb's term-tree fragment. Per
        // ADR-024, the verb is a structural declaration — its
        // runtime is implementation-owned.
        #fn_vis fn #accessor_name() -> &'static [::uor_foundation::enforcement::Term] {
            #const_name
        }

        // Marker `pub fn name(_: InputTy) -> OutputTy` so the verb
        // appears at the consumer's name-resolution surface. The body
        // never executes as Rust at runtime; foundation's catamorphism
        // walks the term-tree fragment per ADR-029.
        #[allow(unused_variables, unreachable_code)]
        #fn_vis fn #fn_name(#input_param: #input_ty) -> #output_ty {
            // Verb bodies are catamorphism-evaluated; the Rust function
            // form exists for name-resolution and macro-time reference.
            // Implementations that invoke a verb directly use foundation's
            // `evaluate_term_tree` against the verb's term-tree slice.
            let _ = #input_param;
            unimplemented!(
                "verb `{}` body is catamorphism-evaluated by foundation's pipeline; \
                 callers reach it through the term-tree accessor `{}_term_arena()`, \
                 not by direct Rust invocation",
                stringify!(#fn_name),
                stringify!(#fn_name),
            )
        }
    };

    expansion.into()
}

// =====================================================================
// `use_verbs!` — wiki ADR-024 cross-implementation verb imports.
//
// Re-exports verbs from another crate's `verb!` emissions. The
// importing implementation's verb-closure check treats imported
// verbs as opaque atoms; the imported crate's own `verb!` macro
// performed that crate's closure check.
//
// Form:
//
// ```text
// use_verbs! {
//     from other_implementation_crate {
//         verb_name_a,
//         verb_name_b,
//     };
// }
// ```

/// Parsed shape of the `use_verbs!` macro input.
struct UseVerbsInput {
    crate_path: syn::Path,
    verb_names: Vec<Ident>,
}

impl Parse for UseVerbsInput {
    fn parse(input: ParseStream) -> Result<Self> {
        // `from <crate_path>`
        let from_kw: Ident = input.parse()?;
        if from_kw != "from" {
            return Err(syn::Error::new(
                from_kw.span(),
                "expected `from <crate_path>`",
            ));
        }
        let crate_path: syn::Path = input.parse()?;

        // `{ verb_a, verb_b, ... }`
        let body;
        syn::braced!(body in input);
        let mut verb_names: Vec<Ident> = Vec::new();
        while !body.is_empty() {
            verb_names.push(body.parse()?);
            if body.peek(Token![,]) {
                body.parse::<Token![,]>()?;
            }
        }

        // Optional trailing semicolon.
        let _ = input.parse::<Token![;]>();

        Ok(Self {
            crate_path,
            verb_names,
        })
    }
}

/// `use_verbs!` — wiki ADR-024 cross-implementation verb imports.
#[proc_macro]
pub fn use_verbs(input: TokenStream) -> TokenStream {
    let parsed = parse_macro_input!(input as UseVerbsInput);
    let UseVerbsInput {
        crate_path,
        verb_names,
    } = parsed;

    let mut imports: Vec<proc_macro2::TokenStream> = Vec::with_capacity(verb_names.len() * 3);
    for name in &verb_names {
        let arena_name = Ident::new(&format!("{}_term_arena", name), name.span());
        let const_name = Ident::new(
            &format!("VERB_TERMS_{}", to_screaming_snake(&name.to_string())),
            name.span(),
        );
        imports.push(quote! { pub use #crate_path::#name; });
        imports.push(quote! { pub use #crate_path::#arena_name; });
        imports.push(quote! { pub use #crate_path::#const_name; });
    }

    let expansion = quote! {
        #( #imports )*
    };

    expansion.into()
}

// Helpers — canonical operand ordering and suffix-identifier construction.

/// Returns the lexically-earlier identifier of two — stable string compare.
/// Used to canonicalize operand ordering in emitted IRIs so
/// `product_shape!(X, A, B)` and `product_shape!(X, B, A)` produce the
/// same `IRI` constant.
fn lexically_earlier(a: &Ident, b: &Ident) -> String {
    let a_s = a.to_string();
    let b_s = b.to_string();
    if a_s.as_str() <= b_s.as_str() {
        a_s
    } else {
        b_s
    }
}

fn lexically_later(a: &Ident, b: &Ident) -> String {
    let a_s = a.to_string();
    let b_s = b.to_string();
    if a_s.as_str() > b_s.as_str() {
        a_s
    } else {
        b_s
    }
}

/// Returns the operand pair in canonical order. The caller's original
/// (left, right) is reordered so the lexically-earlier identifier is
/// returned first. Amendment §4e canonicalization — token-string-based
/// proxy for the runtime content fingerprint, documented in the plan.
fn canonical_operand_pair(a: &Ident, b: &Ident) -> (Ident, Ident) {
    let a_s = a.to_string();
    let b_s = b.to_string();
    if a_s.as_str() <= b_s.as_str() {
        (a.clone(), b.clone())
    } else {
        (b.clone(), a.clone())
    }
}

/// Build a new identifier for a `const` declaration. Converts the base
/// name to SCREAMING_SNAKE_CASE (so a PascalCase shape name like
/// `LeafA_Times_LeafB` becomes `LEAF_A_TIMES_LEAF_B`) and appends the
/// suffix, preserving the original's call-site span for error reporting.
/// This satisfies Rust's `non_upper_case_globals` lint uniformly
/// regardless of the casing style the caller uses for shape names.
fn format_ident_suffix(base: &Ident, suffix: &str) -> Ident {
    let upper_base = to_screaming_snake(&base.to_string());
    let joined = format!("{upper_base}{suffix}");
    Ident::new(&joined, base.span())
}

/// Converts a PascalCase / camelCase / snake_case string to
/// SCREAMING_SNAKE_CASE. Handles runs of uppercase letters, interior
/// underscores, and digit boundaries so the result is idiomatic
/// SCREAMING_SNAKE.
fn to_screaming_snake(s: &str) -> String {
    let mut out = String::with_capacity(s.len() + 4);
    let chars: Vec<char> = s.chars().collect();
    for (i, ch) in chars.iter().enumerate() {
        if *ch == '_' {
            if !out.ends_with('_') && !out.is_empty() {
                out.push('_');
            }
            continue;
        }
        if ch.is_ascii_uppercase() {
            // Insert a separator before an uppercase letter when:
            //  (a) previous char was lowercase or digit
            //  (b) previous was uppercase but next is lowercase (end of a
            //      run like `HTTPServer` → `HTTP_Server`).
            let prev_lower_or_digit = i > 0
                && chars[i - 1] != '_'
                && (chars[i - 1].is_ascii_lowercase() || chars[i - 1].is_ascii_digit());
            let run_ending = i > 0
                && chars[i - 1].is_ascii_uppercase()
                && i + 1 < chars.len()
                && chars[i + 1].is_ascii_lowercase();
            if (prev_lower_or_digit || run_ending) && !out.ends_with('_') && !out.is_empty() {
                out.push('_');
            }
            out.push(*ch);
        } else {
            out.push(ch.to_ascii_uppercase());
        }
    }
    out
}