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
81
82
83
84
85
86
87
88
89
90
91
92
93
94

use super::{Certificate, OpOutcome, OpResult};

/// Serialize a certificate to pretty JSON.
#[inline]
pub fn to_json(cert: &Certificate) -> Result<String, String> {
    serde_json::to_string_pretty(cert)
        .map_err(|err| format!("certificate serialization failed: {err}. Fix: report this vyre-conform bug with the certificate shape."))
}

/// Render a certificate as a human-readable report.
#[must_use]
#[inline]
pub fn to_human(cert: &Certificate) -> String {
    let mut lines = Vec::new();
    lines.push("vyre conformance certificate".to_string());
    lines.push(cert.proof_status.clone());
    lines.push(format!(
        "backend: {} {}",
        cert.backend_name, cert.backend_version
    ));
    lines.push(format!("spec version: {}", cert.spec_version));
    lines.push(format!(
        "certificate_hash: {}",
        hex::encode(cert.certificate_hash)
    ));
    lines.push(format!(
        "verification: {:?}, {} u32 witnesses per law",
        cert.strength, cert.witness_count
    ));
    lines.push(format!(
        "levels: integer={:?}, float={:?}, approximate={:?}",
        cert.level.integer, cert.level.float, cert.level.approximate
    ));
    lines.push(format!(
        "coverage: {}/{} supported parity ops, {} unsupported ops, {}/{} laws, {} cases",
        cert.coverage.ops_parity_passed,
        cert.coverage
            .ops_total
            .saturating_sub(cert.coverage.ops_unsupported),
        cert.coverage.ops_unsupported,
        cert.coverage.laws_passed,
        cert.coverage.laws_total,
        cert.coverage.cases_tested
    ));
    lines.push(String::new());
    lines.push("integer operations:".to_string());
    push_ops(&mut lines, &cert.integer_track.ops);
    if let Some(track) = &cert.float_track {
        lines.push(String::new());
        lines.push("float operations:".to_string());
        push_ops(&mut lines, &track.ops);
    }
    if let Some(track) = &cert.approximate_track {
        lines.push(String::new());
        lines.push("approximate operations:".to_string());
        push_ops(&mut lines, &track.ops);
    }
    if cert.engines.is_empty() {
        lines.push(String::new());
        lines.push("engines: not evaluated by op-only certificate run".to_string());
    }
    lines.join("\n")
}

fn push_ops(lines: &mut Vec<String>, ops: &[OpResult]) {
    if ops.is_empty() {
        lines.push("- none".to_string());
        return;
    }
    for op in ops {
        let parity = match op.outcome {
            OpOutcome::Passed => "pass",
            OpOutcome::Failed => "fail",
            OpOutcome::Pending => "pending",
            OpOutcome::Unsupported => "unsupported",
        };
        let law_denom = op.laws_verified.len() + op.laws_failed.len();
        lines.push(format!(
            "- {}: parity={}, laws={}/{}, cases={}, witnesses={}",
            op.id,
            parity,
            op.laws_verified.len(),
            law_denom,
            op.cases_tested,
            op.witness_count
        ));
        for violation in &op.laws_failed {
            lines.push(format!("  law failure: {violation}"));
        }
        for failure in &op.parity_failures {
            lines.push(format!("  parity failure: {failure}"));
        }
    }
}