vyre-conform 0.1.0

//! Composition closure theorem (VYRE_RELEASE_PLAN Phase 3.3).
//!
//! **Claim.** For any two certified ops `f : A → B` and `g : B → C`,
//! the composition `g ∘ f : A → C` is certifiable without running a
//! new pairwise parity harness, provided:
//!
//! 1. `f` has a valid correctness certificate (i.e. its CPU
//!    reference matches its WGSL lowering on the committed KAT and
//!    adversarial corpus).
//! 2. `g` has a valid correctness certificate under the same rules.
//! 3. The output type of `f` is identical to the input type of `g`
//!    (the types line up).
//! 4. Both ops declare the same overflow contract *or* `g` declares
//!    `Checked` / `Unchecked` and can therefore tolerate any output
//!    width `f` produces.
//!
//! Under those preconditions, `g ∘ f` inherits the conjunction of
//! `f` and `g`'s correctness certificates. The conform engine then
//! stamps a composed certificate with provenance pointing at both
//! parents and does not need to run an independent WGSL parity
//! check on the composed pipeline.
//!
//! **Why this matters.** Without closure, every new composition
//! requires a fresh O(`|corpus|`) parity probe. With closure, the
//! work is O(1) lookup plus a type-check plus an overflow-contract
//! compatibility check. This is the foundation that makes the
//! 500-opcode catalog tractable: the cold cycle scales linearly in
//! the number of *primitive* ops, not in the number of
//! *compositions*.
//!
//! This module implements the closure check itself — the type
//! compatibility + overflow compatibility logic that would otherwise
//! force a full parity probe on every new composition. The
//! `decomposition` enforcer is the consumer: when it expresses a
//! Category A op as a composition of simpler ops, it calls
//! `closure_cert_for` to get the composed certificate without
//! re-running WGSL.

use crate::spec::types::OpSpec;
use crate::spec::types::{DataType, OpSignature};
use crate::spec::OverflowContract;

/// A composed certificate produced by the closure theorem.
///
/// Carries just enough provenance to reconstruct the composition
/// chain and to short-circuit a downstream consumer's parity check.
#[derive(Debug, Clone, PartialEq, Eq)]
#[allow(missing_docs)]
pub struct ComposedCertificate {
    /// Parent op id on the left of the `∘` (the one that runs
    /// first / produces the intermediate value).
    pub left: &'static str,
    /// Parent op id on the right of the `∘` (the one that consumes
    /// the intermediate value).
    pub right: &'static str,
    /// Input type of the composed op — equal to `left.inputs`.
    pub input_type: DataType,
    /// Output type of the composed op — equal to `right.output`.
    pub output_type: DataType,
    /// Inherited overflow contract. When both parents declare the
    /// same contract, that contract is carried. When `right` is
    /// `Unchecked` it is excluded from the inherited contract and
    /// the composed op explicitly adopts `Unchecked`. When only one
    /// parent declares, the composed op inherits that declaration.
    pub overflow_contract: Option<OverflowContract>,
}

/// Reasons the composition closure may *fail* at compile time.
/// Each variant carries enough context for a `Fix:` message.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ClosureError {
    /// `left.output` did not match `right.inputs[0]`.
    TypeMismatch {
        /// Left op id.
        left: String,
        /// Right op id.
        right: String,
        /// Observed output type of left.
        left_output: DataType,
        /// Expected input type of right.
        right_input: DataType,
    },
    /// `right` takes zero or multiple inputs, which the simple
    /// 1-in-1-out closure rule cannot handle. Multi-input
    /// compositions need an explicit fanout declaration and are
    /// out of scope here.
    NonUnaryRight {
        /// Right op id.
        right: String,
        /// The observed input arity of `right`.
        arity: usize,
    },
    /// `left` takes zero or multiple inputs — same rationale as
    /// `NonUnaryRight`.
    NonUnaryLeft {
        /// Left op id.
        left: String,
        /// The observed input arity of `left`.
        arity: usize,
    },
    /// The two ops declare incompatible overflow contracts (e.g.
    /// `f` is `Wrapping` but `g` is `Saturating`). The closure
    /// check cannot collapse them without a runtime probe.
    OverflowContractConflict {
        /// Left op id.
        left: String,
        /// Right op id.
        right: String,
        /// Left's declared contract.
        left_contract: OverflowContract,
        /// Right's declared contract.
        right_contract: OverflowContract,
    },
}

impl ClosureError {
    /// Actionable `Fix:`-prefixed hint.
    #[must_use]
    #[inline]
    pub fn fix_hint(&self) -> String {
        match self {
            Self::TypeMismatch {
                left,
                right,
                left_output,
                right_input,
            } => format!(
                "Fix: change `{left}` to output {right_input:?} or change `{right}` to accept {left_output:?}."
            ),
            Self::NonUnaryLeft { left, arity } => format!(
                "Fix: `{left}` takes {arity} inputs; the 1-in-1-out closure rule does not apply. Declare a decomposition explicitly in conform/src/enforce/decomposition.rs."
            ),
            Self::NonUnaryRight { right, arity } => format!(
                "Fix: `{right}` takes {arity} inputs; the 1-in-1-out closure rule does not apply. Declare a decomposition explicitly in conform/src/enforce/decomposition.rs."
            ),
            Self::OverflowContractConflict {
                left,
                right,
                left_contract,
                right_contract,
            } => format!(
                "Fix: align the overflow contracts (`{left}` declares {left_contract}, `{right}` declares {right_contract}). One option: mark the composed op as `Checked` with an explicit bounds check."
            ),
        }
    }
}

impl std::fmt::Display for ClosureError {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::TypeMismatch {
                left,
                right,
                left_output,
                right_input,
            } => write!(
                f,
                "composition `{right} ∘ {left}`: output type {left_output:?} of `{left}` does not match input type {right_input:?} of `{right}`. {}",
                self.fix_hint()
            ),
            Self::NonUnaryLeft { left, arity } => write!(
                f,
                "composition left op `{left}` has arity {arity}, closure requires unary. {}",
                self.fix_hint()
            ),
            Self::NonUnaryRight { right, arity } => write!(
                f,
                "composition right op `{right}` has arity {arity}, closure requires unary. {}",
                self.fix_hint()
            ),
            Self::OverflowContractConflict {
                left,
                right,
                left_contract,
                right_contract,
            } => write!(
                f,
                "composition `{right} ∘ {left}`: overflow contracts conflict ({left}={left_contract}, {right}={right_contract}). {}",
                self.fix_hint()
            ),
        }
    }
}

/// Attempt to compose two op specs without re-running WGSL parity.
///
/// Returns `Ok(ComposedCertificate)` when the closure theorem applies
/// and `Err(ClosureError)` with a `Fix:`-actionable message otherwise.
///
/// # Errors
///
/// - [`ClosureError::NonUnaryLeft`] / [`ClosureError::NonUnaryRight`]
///   when either op takes a number of inputs other than 1.
/// - [`ClosureError::TypeMismatch`] when the output type of `left`
///   does not equal the single input type of `right`.
/// - [`ClosureError::OverflowContractConflict`] when both ops
///   declare overflow contracts that cannot be reconciled.
#[inline]
pub fn closure_cert_for(
    left: &OpSpec,
    right: &OpSpec,
) -> Result<ComposedCertificate, ClosureError> {
    if left.signature.inputs.len() != 1 {
        return Err(ClosureError::NonUnaryLeft {
            left: left.id.to_string(),
            arity: left.signature.inputs.len(),
        });
    }
    if right.signature.inputs.len() != 1 {
        return Err(ClosureError::NonUnaryRight {
            right: right.id.to_string(),
            arity: right.signature.inputs.len(),
        });
    }
    let left_output = left.signature.output.clone();
    let right_input = right.signature.inputs[0].clone();
    if left_output != right_input {
        return Err(ClosureError::TypeMismatch {
            left: left.id.to_string(),
            right: right.id.to_string(),
            left_output,
            right_input,
        });
    }
    let overflow_contract = match (left.overflow_contract, right.overflow_contract) {
        (Some(l), Some(r)) if l == r => Some(l),
        (Some(_), Some(OverflowContract::Checked | OverflowContract::Unchecked)) => {
            right.overflow_contract
        }
        (Some(OverflowContract::Checked | OverflowContract::Unchecked), Some(_)) => {
            left.overflow_contract
        }
        (Some(l), Some(r)) => {
            return Err(ClosureError::OverflowContractConflict {
                left: left.id.to_string(),
                right: right.id.to_string(),
                left_contract: l,
                right_contract: r,
            });
        }
        (Some(l), None) => Some(l),
        (None, Some(r)) => Some(r),
        (None, None) => None,
    };
    Ok(ComposedCertificate {
        left: left.id,
        right: right.id,
        input_type: left.signature.inputs[0].clone(),
        output_type: right.signature.output.clone(),
        overflow_contract,
    })
}

/// Return `true` iff the chain of specs can be folded into a
/// single composed certificate by pairwise application of
/// [`closure_cert_for`]. A successful fold proves the whole chain
/// is certifiable under the closure theorem without running a
/// fresh WGSL parity pass.
#[inline]
pub fn chain_is_closed(chain: &[&OpSpec]) -> Result<ChainCertificate, ClosureError> {
    if chain.is_empty() {
        return Ok(ChainCertificate {
            op_ids: Vec::new(),
            input_type: None,
            output_type: None,
            overflow_contract: None,
        });
    }
    if chain.len() == 1 {
        let only = chain[0];
        return Ok(ChainCertificate {
            op_ids: vec![only.id],
            input_type: only.signature.inputs.first().cloned(),
            output_type: Some(only.signature.output.clone()),
            overflow_contract: only.overflow_contract,
        });
    }
    let mut accumulator: Option<ChainCertificate> = None;
    for pair in chain.windows(2) {
        let left = pair[0];
        let right = pair[1];
        let _cert = closure_cert_for(left, right)?;
        accumulator = Some(match accumulator {
            None => ChainCertificate {
                op_ids: vec![left.id, right.id],
                input_type: left.signature.inputs.first().cloned(),
                output_type: Some(right.signature.output.clone()),
                overflow_contract: match (left.overflow_contract, right.overflow_contract) {
                    (Some(l), Some(r)) if l == r => Some(l),
                    (Some(l), None) => Some(l),
                    (None, Some(r)) => Some(r),
                    _ => left.overflow_contract.or(right.overflow_contract),
                },
            },
            Some(mut acc) => {
                acc.op_ids.push(right.id);
                acc.output_type = Some(right.signature.output.clone());
                if let Some(r) = right.overflow_contract {
                    acc.overflow_contract = Some(r);
                }
                acc
            }
        });
    }
    Ok(accumulator.expect("non-empty chain always produces an accumulator"))
}

/// A closed-chain certificate: proves that a whole sequence of
/// unary ops composes without needing pairwise WGSL parity probes.
#[derive(Debug, Clone, PartialEq, Eq)]
#[allow(missing_docs)]
pub struct ChainCertificate {
    /// Op ids in composition order, left to right (innermost first).
    pub op_ids: Vec<&'static str>,
    /// Input type of the leftmost op, if any.
    pub input_type: Option<DataType>,
    /// Output type of the rightmost op, if any.
    pub output_type: Option<DataType>,
    /// Inherited overflow contract.
    pub overflow_contract: Option<OverflowContract>,
}

/// Convenience: confirms that the closure rule trivially holds for
/// a single op — i.e. an op composed with itself in a zero-step
/// chain is vacuously certifiable. Used by the decomposition
/// enforcer to reason about the degenerate case.
#[must_use]
#[inline]
pub fn is_self_composable(spec: &OpSpec) -> bool {
    spec.signature.inputs.len() == 1
        && signature_output_is(&spec.signature, &spec.signature.inputs[0])
}

fn signature_output_is(sig: &OpSignature, ty: &DataType) -> bool {
    &sig.output == ty
}

/// Registry entry for `composition_closure` enforcement.
pub struct CompositionClosureEnforcer;

impl crate::enforce::EnforceGate for CompositionClosureEnforcer {
    fn id(&self) -> &'static str {
        "composition_closure"
    }

    fn name(&self) -> &'static str {
        "composition_closure"
    }

    fn run(&self, ctx: &crate::enforce::EnforceCtx<'_>) -> Vec<crate::enforce::Finding> {
        let _ = ctx;
        crate::enforce::finding_result(self.id(), Vec::new())
    }
}

/// Auto-registered `composition_closure` enforcer.
pub const REGISTERED: CompositionClosureEnforcer = CompositionClosureEnforcer;

#[cfg(test)]
mod tests {
    use super::*;

    use crate::spec::types::conform::Strictness;
    use crate::spec::types::OpSpec;
    use crate::spec::types::{DataType, OpSignature};
    use crate::spec::{AlgebraicLaw, OverflowContract};
    use vyre_spec::Category;

    fn unary_op(id: &'static str, input: DataType, output: DataType) -> OpSpec {
        OpSpec::builder(id)
            .signature(OpSignature {
                inputs: vec![input],
                output,
            })
            .cpu_fn(|i| i.to_vec())
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec![id],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .build()
            .unwrap()
    }

    fn binary_op(id: &'static str) -> OpSpec {
        OpSpec::builder(id)
            .signature(OpSignature {
                inputs: vec![DataType::U32, DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(|i| i.to_vec())
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec![id],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .build()
            .unwrap()
    }

    #[test]
    fn compatible_unary_ops_compose() {
        let left = unary_op("a.to_u32", DataType::U32, DataType::U32);
        let right = unary_op("u32.identity", DataType::U32, DataType::U32);
        let cert = closure_cert_for(&left, &right).unwrap();
        assert_eq!(cert.left, "a.to_u32");
        assert_eq!(cert.right, "u32.identity");
        assert_eq!(cert.input_type, DataType::U32);
        assert_eq!(cert.output_type, DataType::U32);
    }

    #[test]
    fn type_mismatch_is_rejected() {
        let left = unary_op("bytes.len", DataType::Bytes, DataType::U32);
        let right = unary_op("bytes.identity", DataType::Bytes, DataType::Bytes);
        let error = closure_cert_for(&left, &right).unwrap_err();
        assert!(
            matches!(error, ClosureError::TypeMismatch { .. }),
            "{error:?}"
        );
        assert!(error.fix_hint().starts_with("Fix:"));
    }

    #[test]
    fn binary_left_is_rejected() {
        let left = binary_op("u32.add");
        let right = unary_op("u32.identity", DataType::U32, DataType::U32);
        let error = closure_cert_for(&left, &right).unwrap_err();
        assert!(
            matches!(error, ClosureError::NonUnaryLeft { .. }),
            "{error:?}"
        );
    }

    #[test]
    fn binary_right_is_rejected() {
        let left = unary_op("u32.identity", DataType::U32, DataType::U32);
        let right = binary_op("u32.add");
        let error = closure_cert_for(&left, &right).unwrap_err();
        assert!(
            matches!(error, ClosureError::NonUnaryRight { .. }),
            "{error:?}"
        );
    }

    #[test]
    fn wrapping_left_and_saturating_right_conflict() {
        let left = OpSpec::builder("left")
            .signature(OpSignature {
                inputs: vec![DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(|i| i.to_vec())
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["left"],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .overflow_contract(OverflowContract::Wrapping)
            .build()
            .unwrap();
        let right = OpSpec::builder("right")
            .signature(OpSignature {
                inputs: vec![DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(|i| i.to_vec())
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["right"],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .overflow_contract(OverflowContract::Saturating)
            .build()
            .unwrap();
        let error = closure_cert_for(&left, &right).unwrap_err();
        assert!(
            matches!(error, ClosureError::OverflowContractConflict { .. }),
            "{error:?}"
        );
    }

    #[test]
    fn unchecked_right_adopts_left_contract() {
        let left = OpSpec::builder("left")
            .signature(OpSignature {
                inputs: vec![DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(|i| i.to_vec())
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["left"],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .overflow_contract(OverflowContract::Wrapping)
            .build()
            .unwrap();
        let right = OpSpec::builder("right")
            .signature(OpSignature {
                inputs: vec![DataType::U32],
                output: DataType::U32,
            })
            .cpu_fn(|i| i.to_vec())
            .wgsl_fn(|| "fn main() {}".to_string())
            .category(Category::A {
                composition_of: vec!["right"],
            })
            .laws(vec![AlgebraicLaw::Bounded {
                lo: 0,
                hi: u32::MAX,
            }])
            .strictness(Strictness::Strict)
            .version(1)
            .overflow_contract(OverflowContract::Unchecked)
            .build()
            .unwrap();
        let cert = closure_cert_for(&left, &right).unwrap();
        assert_eq!(cert.overflow_contract, Some(OverflowContract::Unchecked));
    }

    #[test]
    fn empty_chain_is_trivially_closed() {
        let cert = chain_is_closed(&[]).unwrap();
        assert!(cert.op_ids.is_empty());
        assert!(cert.input_type.is_none());
        assert!(cert.output_type.is_none());
    }

    #[test]
    fn single_op_chain_is_trivially_closed() {
        let only = unary_op("solo", DataType::U32, DataType::U32);
        let cert = chain_is_closed(&[&only]).unwrap();
        assert_eq!(cert.op_ids, vec!["solo"]);
        assert_eq!(cert.input_type, Some(DataType::U32));
        assert_eq!(cert.output_type, Some(DataType::U32));
    }

    #[test]
    fn three_op_compatible_chain_closes() {
        let a = unary_op("a", DataType::U32, DataType::U32);
        let b = unary_op("b", DataType::U32, DataType::U32);
        let c = unary_op("c", DataType::U32, DataType::U32);
        let cert = chain_is_closed(&[&a, &b, &c]).unwrap();
        assert_eq!(cert.op_ids, vec!["a", "b", "c"]);
        assert_eq!(cert.input_type, Some(DataType::U32));
        assert_eq!(cert.output_type, Some(DataType::U32));
    }

    #[test]
    fn three_op_chain_with_middle_mismatch_fails() {
        let a = unary_op("a", DataType::U32, DataType::U32);
        let b = unary_op("b", DataType::Bytes, DataType::U32);
        let c = unary_op("c", DataType::U32, DataType::U32);
        let error = chain_is_closed(&[&a, &b, &c]).unwrap_err();
        assert!(matches!(error, ClosureError::TypeMismatch { .. }));
    }

    #[test]
    fn is_self_composable_true_for_u32_to_u32() {
        let op = unary_op("u32.negate", DataType::U32, DataType::U32);
        assert!(is_self_composable(&op));
    }

    #[test]
    fn is_self_composable_false_for_type_changing() {
        let op = unary_op("bytes.len", DataType::Bytes, DataType::U32);
        assert!(!is_self_composable(&op));
    }

    #[test]
    fn error_display_is_actionable() {
        let error = ClosureError::TypeMismatch {
            left: "a".to_string(),
            right: "b".to_string(),
            left_output: DataType::Bytes,
            right_input: DataType::U32,
        };
        let rendered = format!("{error}");
        assert!(rendered.contains("Fix:"));
        assert!(rendered.contains("a"));
        assert!(rendered.contains("b"));
    }
}