omena-smt 0.2.0

SMT-encoded cascade verification contracts for Omena CSS
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

use omena_refinement_trait::RefinementVerdictV0;
use serde::Serialize;

use crate::{
    CanonicalSmtInputV0, SMT_FEATURE_GATE_V0, SMT_LAYER_MARKER_V0, SMT_SCHEMA_VERSION_V0,
    SmtBackendCheckV0, SmtBackendKindV0, SmtBackendSatResultV0, SmtBackendV0,
};

pub(crate) const CASCADE_SMT_SPEC_MATERIAL_V0: &str = "\
schema=0\n\
theory=cascade-smt-theory-v0\n\
encoding=canonical-smt-input-v0\n\
default-backend=stub-propositional\n\
opt-in-backend=smt-z3-qf-lia-layer-inversion\n\
obligations=box-shorthand-combination,scope-flatten-candidate,layer-flatten-candidate,static-supports-condition\n\
";

#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub enum SmtVerdictV0 {
    Accepted,
    Rejected,
    Unknown,
}

#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct CascadeSMTProofV0 {
    pub schema_version: &'static str,
    pub product: &'static str,
    pub layer_marker: &'static str,
    pub feature_gate: &'static str,
    pub obligation_id: String,
    pub backend: SmtBackendKindV0,
    pub verdict: SmtVerdictV0,
    pub l1_primitive: &'static str,
    pub l1_accepted: Option<bool>,
    pub canonical_input: CanonicalSmtInputV0,
    pub solver_check: SmtBackendCheckV0,
    pub refinement_verdict: Option<RefinementVerdictV0>,
    pub cascade_spec_digest: [u8; 32],
}

#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct CascadeSMTProofAuditLogV0 {
    pub schema_version: &'static str,
    pub product: &'static str,
    pub layer_marker: &'static str,
    pub feature_gate: &'static str,
    pub obligation_id: String,
    pub backend: SmtBackendKindV0,
    pub solver_latency_us: Option<u64>,
    pub unsat_core_labels: Vec<String>,
}

pub(crate) fn cascade_smt_proof_v0<B: SmtBackendV0>(
    canonical_input: CanonicalSmtInputV0,
    backend: &B,
    l1_primitive: &'static str,
    l1_accepted: Option<bool>,
) -> CascadeSMTProofV0 {
    let solver_check = backend.check_canonical_input_v0(&canonical_input);
    CascadeSMTProofV0 {
        schema_version: SMT_SCHEMA_VERSION_V0,
        product: "omena-smt.cascade-proof",
        layer_marker: SMT_LAYER_MARKER_V0,
        feature_gate: SMT_FEATURE_GATE_V0,
        obligation_id: canonical_input.obligation_id.clone(),
        backend: backend.backend_kind(),
        verdict: smt_verdict_from_backend_check_v0(solver_check.sat_result),
        l1_primitive,
        l1_accepted,
        canonical_input,
        solver_check,
        refinement_verdict: None,
        cascade_spec_digest: cascade_spec_digest_v0(),
    }
}

fn smt_verdict_from_backend_check_v0(sat_result: SmtBackendSatResultV0) -> SmtVerdictV0 {
    match sat_result {
        SmtBackendSatResultV0::Sat => SmtVerdictV0::Accepted,
        SmtBackendSatResultV0::Unsat => SmtVerdictV0::Rejected,
        SmtBackendSatResultV0::Unknown => SmtVerdictV0::Unknown,
    }
}

pub fn cascade_spec_digest_v0() -> [u8; 32] {
    *blake3::hash(CASCADE_SMT_SPEC_MATERIAL_V0.as_bytes()).as_bytes()
}