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

//! The proof engine — algebraic law verification.
//!
//! This module is the core of vyre-conform's claim to be a proof system.
//! It verifies that a CPU reference function (or GPU backend) satisfies
//! the algebraic laws declared for each operation.
//!
//! Three verification levels:
//! - **Exhaustive:** All inputs in a small domain (u8). Proof within domain.
//! - **Witnessed:** N random inputs from the full domain (u32). Statistical.
//! - **Combined:** Both. Practical proof.

/// Coverage audit: detect missing laws and undeclared properties.
pub mod audit;
/// Law verification engine: exhaustive u8 and witnessed u32.
pub mod checker;
/// Composition theorem proofs for multi-op chains.
pub mod composition;
/// Law coverage matrix — T03/T04/T05 defense.
pub mod coverage;
/// File-backed formal law catalog and export hooks.
pub mod formal;
/// Machine-readable formal algebraic law specifications.
pub mod formal_spec;
/// GPU-side law verification through backend dispatch.
pub mod gpu_checker;
/// Law inference from CPU reference behavior.
pub mod inference;
/// Per-op law dispatch tables.
pub mod laws;
/// Mandatory law inference for registering ops.
pub mod mandatory_inference;
/// Counterexample minimization.
pub mod minimizer;
/// Construction-time proof tokens for chain composition.
pub mod proof_token;

/// Construction-time proof tokens for chain composition.
pub use crate::spec::types::{ConstructionTime, ProofToken, ProofTokenError};
/// Law verification engine entry points and result types.
pub use checker::{verify_laws, verify_laws_witnessed, LawResult, VerificationLevel};
/// Composition theorem types and queries.
pub use composition::{applicable_theorems, theorems, CompositionTheorem};
/// Machine-readable formal specification types.
pub use formal_spec::{AlgebraicLawFormalSpec, Expr, FormalLaw, Predicate};
/// GPU-backed witnessed law verification.
pub use gpu_checker::verify_gpu_laws_witnessed;
/// Law inference entry points and report types.
pub use inference::{
    find_missing_laws, infer_binary_laws, infer_unary_laws, InferenceReport, InferredLaw,
};
/// Cross-operation law inference.
pub use mandatory_inference::infer_cross_op_laws;