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
95
96
97
98
99
100
101
102
103
104
105
106
107

//! Self-audit rules for conform's own enforcement surface.

pub mod rules {
    //! Reference-trust and layer coverage rules.

    /// Production self-audit checks.
    use std::collections::BTreeSet;

    use crate::enforce::reference_trust;
    use crate::proof::algebra::formal::loader;
    use crate::spec::OpSpec;

    /// One self-audit finding.
    #[derive(Debug, Clone, Default, Eq, PartialEq)]
    pub struct SelfAuditFinding {
        /// Rule identifier.
        pub rule: u8,
        /// Operation id when the finding belongs to one op.
        pub op_id: Option<String>,
        /// Actionable diagnostic.
        pub message: String,
    }

    /// Rule 3: CPU references must survive reference-trust checks.
    #[inline]
    pub fn rule_3_cpu_reference_trust(specs: &[OpSpec]) -> Vec<SelfAuditFinding> {
        specs
            .iter()
            .flat_map(|spec| {
                reference_trust::validate_spec(spec)
                    .into_iter()
                    .map(|finding| SelfAuditFinding {
                        rule: 3,
                        op_id: Some(finding.op_id.clone()),
                        message: format!(
                        "{} Fix: implement real CPU semantics before this op can be registered.",
                        finding.message()
                    ),
                    })
            })
            .collect()
    }

    /// Rule 9: reference-trust must visit every registered op.
    #[inline]
    pub fn rule_9_reference_trust_covers_registry(specs: &[OpSpec]) -> Vec<SelfAuditFinding> {
        let report = reference_trust::enforce_registry(specs);
        let checked: BTreeSet<&str> = report.checked_ops.iter().map(String::as_str).collect();

        specs
        .iter()
        .filter(|spec| !checked.contains(spec.id))
        .map(|spec| SelfAuditFinding {
            rule: 9,
            op_id: Some(spec.id.to_string()),
            message: format!(
                "reference_trust did not visit `{}`. Fix: route every registry op through reference_trust::enforce_registry before admission.",
                spec.id
            ),
        })
        .collect()
    }

    /// Rule 10: every algebraic-law variant must have a formal spec.
    #[inline]
    pub fn rule_10_algebraic_laws_have_formal_specs() -> Vec<SelfAuditFinding> {
        match loader::load_catalog() {
            Ok(_) => Vec::new(),
            Err(error) => vec![SelfAuditFinding {
                rule: 10,
                op_id: None,
                message: format!(
                "{error}. Fix: add or repair the matching conform/src/algebra/formal/*.formal file."
            ),
            }],
        }
    }
}

/// Registry entry for `self_audit` enforcement.
pub struct SelfAuditEnforcer;

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

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

    fn run(&self, ctx: &crate::enforce::EnforceCtx<'_>) -> Vec<crate::enforce::Finding> {
        let mut findings = rules::rule_3_cpu_reference_trust(ctx.specs);
        findings.extend(rules::rule_9_reference_trust_covers_registry(ctx.specs));
        findings.extend(rules::rule_10_algebraic_laws_have_formal_specs());
        crate::enforce::finding_result(
            self.id(),
            findings
                .into_iter()
                .map(|finding| finding.message)
                .collect(),
        )
    }
}

/// Auto-registered `self_audit` enforcer.
pub const REGISTERED: SelfAuditEnforcer = SelfAuditEnforcer;