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

//! Pipeline proof-token validation before composition dispatch.

use super::chain_version;
use crate::spec::types::{ChainSpec, ParityFailure, ProofToken};

#[inline]
pub(crate) fn validate_chain(chain: &ChainSpec) -> Result<(), Box<ParityFailure>> {
    let expected = match ProofToken::from_specs(&chain.specs, chain.proof_token.computed_at) {
        Ok(t) => t,
        Err(err) => {
            return Err(Box::new(ParityFailure {
                op_id: chain.id.clone(),
                generator: "composition-proof".to_string(),
                input_label: "construction-token".to_string(),
                input: Vec::new(),
                gpu_output: Vec::new(),
                cpu_output: Vec::new(),
                message: format!(
                    "composition proof token recomputation failed for {}: {err}. \
                     Fix: verify that all component ops satisfy their declared laws.",
                    chain.id
                ),
                spec_version: chain_version(chain),
                workgroup_size: 0,
            }));
        }
    };
    if chain.proof_token.theorem_claims_match(&expected) {
        return Ok(());
    }

    Err(Box::new(ParityFailure {
        op_id: chain.id.clone(),
        generator: "composition-proof".to_string(),
        input_label: "construction-token".to_string(),
        input: Vec::new(),
        gpu_output: Vec::new(),
        cpu_output: Vec::new(),
        message: format!(
            "composition proof token mismatch for {}: claimed preserved=[{}], broken=[{}], \
             theorems=[{}]; expected preserved=[{}], broken=[{}], theorems=[{}]. \
             Fix: build ChainSpec through a composer or recompute ProofToken::from_specs \
             before dispatch.",
            chain.id,
            law_names(&chain.proof_token.preserved_laws),
            law_names(&chain.proof_token.broken_laws),
            chain.proof_token.theorem_chain.join(","),
            law_names(&expected.preserved_laws),
            law_names(&expected.broken_laws),
            expected.theorem_chain.join(","),
        ),
        spec_version: chain_version(chain),
        workgroup_size: 0,
    }))
}

fn law_names(laws: &[crate::spec::law::AlgebraicLaw]) -> String {
    laws.iter()
        .map(crate::spec::law::AlgebraicLaw::name)
        .collect::<Vec<_>>()
        .join(",")
}