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

use crate::spec::types::OracleKind;
use crate::OpSpec;
use vyre_spec::Category;

use super::error::CoverageError;

pub(super) fn check_oracle(spec: &OpSpec, errors: &mut Vec<CoverageError>) {
    match spec.oracle_override {
        Some(OracleKind::SpecTable) if spec.spec_table.is_empty() => {
            errors.push(CoverageError::InvalidOracle {
                op_id: spec.id.to_string(),
                message: "SpecTable requires at least one SpecRow. Fix: add rows or choose another oracle."
                    .to_string(),
            });
        }
        Some(OracleKind::Law) if spec.laws.is_empty() => {
            errors.push(CoverageError::InvalidOracle {
                op_id: spec.id.to_string(),
                message:
                    "Law oracle requires declared laws. Fix: declare laws or choose another oracle."
                        .to_string(),
            })
        }
        Some(OracleKind::Composition) if !matches!(spec.category, Category::A { .. }) => {
            errors.push(CoverageError::InvalidOracle {
                op_id: spec.id.to_string(),
                message:
                    "Composition oracle requires Category A. Fix: change the oracle or category."
                        .to_string(),
            });
        }
        Some(OracleKind::External)
            if spec
                .external_oracle_url
                .map(|s| s.trim().is_empty())
                .unwrap_or(true) =>
        {
            errors.push(CoverageError::InvalidOracle {
                op_id: spec.id.to_string(),
                message:
                    "External oracle requires external_oracle_url. Fix: set the URL or choose another oracle."
                        .to_string(),
            });
        }
        Some(OracleKind::Property) if spec.property_invariants.is_empty() => {
            errors.push(CoverageError::InvalidOracle {
                op_id: spec.id.to_string(),
                message:
                    "Property oracle requires non-empty property_invariants. Fix: declare invariants or choose another oracle."
                        .to_string(),
            });
        }
        _ => {}
    }
}