vyre-conform 0.1.0

Conformance suite for vyre backends — proves byte-identical output to CPU reference
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

//! H10 — composition proof harness.
//!
//! Wraps `crate::proof::algebra::composition` and `crate::proof::algebra::proof_token`.
//! Given an ordered slice of operation specs (a composition chain), returns
//! the proof token if the composition is theorem-supported, or a list of
/// broken laws otherwise.
use crate::spec::types::{ConstructionTime, OpSpec, ProofToken, ProofTokenError};

/// Result of a composition proof check.
///
/// Captures the structured outcome of validating algebraic properties across operation
/// chains so upstream logic can gracefully handle missing or partial proofs.
///
/// # Examples
///
/// Inspect a failed composition result:
///
/// ```rust
/// use vyre_conform::verify::harnesses::composition_proof::CompositionProofResult;
///
/// let result = CompositionProofResult::Failed(vec!["Associativity".to_string()]);
/// assert!(matches!(result, CompositionProofResult::Failed(failures) if failures.len() == 1));
/// ```
#[derive(Debug, Clone, PartialEq)]
pub enum CompositionProofResult {
    /// The composition has a valid proof token.
    Ok(ProofToken),
    /// At least one theorem applied, but one or more component laws remain
    /// unproven. Callers must not treat this as a full composition proof.
    Partial(ProofToken),
    /// One or more component laws are not proven to survive this composition.
    Failed(Vec<String>),
    /// Verification of component laws or theorems failed.
    VerificationFailed(String),
}

/// Check composition theorems for an ordered chain of operations.
///
/// `specs` is the ordered list of operations in the chain. The function
/// computes a [`ProofToken`] using the existing composition theorem engine.
/// If any laws are broken after some theorem application, it returns
/// [`CompositionProofResult::Partial`] so downstream gates must explicitly
/// handle the incomplete proof. If no theorem applies and laws are broken, it
/// returns [`CompositionProofResult::Failed`] with the broken law names.
///
/// Provides a unified entry point to assess whether a given operation sequence
/// preserves necessary mathematical laws.
///
/// # Examples
///
/// Verify composition constraints on an empty chain:
///
/// ```rust
/// use vyre_conform::verify::harnesses::composition_proof::{composition_proof_check, CompositionProofResult};
///
/// let specs = &[];
/// let result = composition_proof_check(specs);
/// assert!(matches!(result, CompositionProofResult::Ok(_)));
/// ```
#[inline]
pub fn composition_proof_check(specs: &[OpSpec]) -> CompositionProofResult {
    let token = match ProofToken::from_specs(specs, ConstructionTime::Manual) {
        Ok(t) => t,
        Err(ProofTokenError::VerificationFailed(msg)) => {
            return CompositionProofResult::VerificationFailed(msg);
        }
    };
    if token.broken_laws.is_empty() {
        CompositionProofResult::Ok(token)
    } else if !token.theorem_chain.is_empty() {
        CompositionProofResult::Partial(token)
    } else {
        let failures = token
            .broken_laws
            .iter()
            .map(|law| law.name().to_string())
            .collect();
        CompositionProofResult::Failed(failures)
    }
}