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

//! Filesystem-registered proof oracles.

use crate::pipeline::certify::Violation;
use crate::spec::types::OpSpec;
use crate::spec::types::OracleKind;

/// Context supplied to an oracle verification pass.
pub struct VerifyCtx<'a> {
    /// Operation specification being verified.
    pub op: &'a OpSpec,
    /// Backend identifier whose output is under verification.
    pub backend_id: &'a str,
    /// Input bytes for the verification case.
    pub input: &'a [u8],
    /// CPU reference bytes for the verification case.
    pub reference_output: &'a [u8],
    /// Backend output bytes for the verification case.
    pub backend_output: &'a [u8],
}

/// Result of an oracle verification pass.
pub type VerifyResult = Result<(), Violation>;

/// Independent proof source for expected conformance output.
pub trait Oracle: Send + Sync {
    /// Stable oracle identifier.
    fn id(&self) -> &'static str;

    /// Oracle hierarchy kind.
    fn kind(&self) -> OracleKind;

    /// Whether this oracle can verify the supplied operation.
    fn applicable_to(&self, op: &OpSpec) -> bool;

    /// Verify a backend output against this oracle.
    fn verify(&self, ctx: &VerifyCtx<'_>) -> VerifyResult;
}

automod::dir!(pub(crate) "src/proof/oracles");

include!(concat!(env!("OUT_DIR"), "/oracles_registry.rs"));