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

//! SMT-LIB export hook for formal algebraic-law specs.

use crate::proof::algebra::formal::loader::{load_catalog, FormalSpecError};

/// Dump all formal law specs as an SMT-LIB flavored placeholder document.
#[inline]
pub fn dump_smt() -> Result<String, FormalSpecError> {
    let specs = load_catalog()?;
    let mut out = String::from("; vyre-conform algebraic law SMT-LIB export\n");
    out.push_str(
        "; Status: scaffold. Statements preserve law metadata for a future SMT encoder.\n",
    );
    out.push_str("(set-logic ALL)\n\n");
    for spec in specs {
        out.push_str("; law: ");
        out.push_str(&spec.law);
        out.push('\n');
        out.push_str("; variant: ");
        out.push_str(&spec.variant);
        out.push('\n');
        out.push_str("; statement: ");
        out.push_str(&spec.mathematical_statement);
        out.push('\n');
        out.push_str("; citation: ");
        out.push_str(&spec.citation);
        out.push('\n');
        let symbol = spec.law.replace('-', "_");
        out.push_str("(assert (! true :named law_");
        out.push_str(&symbol);
        out.push_str("))\n\n");
    }
    out.push_str("(check-sat)\n");
    Ok(out)
}