omena_refinement_trait/
lib.rs

1//! Interface-only refinement predicate contracts.
2//!
3//! This crate intentionally has no dependency on cascade or SMT crates. It is
4//! the cycle breaker shared by `omena-cascade`, `omena-refinement`, and
5//! `omena-smt`.
6
7use serde::Serialize;
8
9pub const REFINEMENT_SCHEMA_VERSION_V0: &str = "0";
10pub const REFINEMENT_LAYER_MARKER_V0: &str = "refinement-cascade";
11pub const REFINEMENT_FEATURE_GATE_V0: &str = "refinement-type-system";
12
13pub trait PropertyIndexV0 {
14    const PROPERTY_NAME: &'static str;
15}
16
17pub trait RefinementPredicateV0 {
18    const PREDICATE_ID: &'static str;
19}
20
21#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
22#[serde(rename_all = "camelCase")]
23pub enum RefinementVerdictV0 {
24    SatisfiedAll,
25    SatisfiedSome,
26    Unsatisfiable,
27    Unknown,
28}
29
30#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
31#[serde(rename_all = "camelCase")]
32pub struct RefinementProvenanceV0 {
33    pub schema_version: &'static str,
34    pub product: &'static str,
35    pub layer_marker: &'static str,
36    pub feature_gate: &'static str,
37    pub source: &'static str,
38    pub legacy_proof_primitive: Option<&'static str>,
39}
40
41#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
42#[serde(rename_all = "camelCase")]
43pub struct RefinementWitnessV0 {
44    pub schema_version: &'static str,
45    pub product: &'static str,
46    pub layer_marker: &'static str,
47    pub feature_gate: &'static str,
48    pub predicate_id: &'static str,
49    pub verdict: RefinementVerdictV0,
50    pub provenance: Vec<RefinementProvenanceV0>,
51    pub legacy_proofs_byte_untouched: bool,
52}
53
54pub fn refinement_provenance_v0(
55    source: &'static str,
56    legacy_proof_primitive: Option<&'static str>,
57) -> RefinementProvenanceV0 {
58    RefinementProvenanceV0 {
59        schema_version: REFINEMENT_SCHEMA_VERSION_V0,
60        product: "omena-refinement-trait.provenance",
61        layer_marker: REFINEMENT_LAYER_MARKER_V0,
62        feature_gate: REFINEMENT_FEATURE_GATE_V0,
63        source,
64        legacy_proof_primitive,
65    }
66}
67
68pub fn refinement_witness_v0(
69    predicate_id: &'static str,
70    verdict: RefinementVerdictV0,
71    provenance: Vec<RefinementProvenanceV0>,
72) -> RefinementWitnessV0 {
73    RefinementWitnessV0 {
74        schema_version: REFINEMENT_SCHEMA_VERSION_V0,
75        product: "omena-refinement-trait.witness",
76        layer_marker: REFINEMENT_LAYER_MARKER_V0,
77        feature_gate: REFINEMENT_FEATURE_GATE_V0,
78        predicate_id,
79        verdict,
80        provenance,
81        legacy_proofs_byte_untouched: true,
82    }
83}
84
85#[cfg(test)]
86mod tests {
87    use super::*;
88
89    #[test]
90    fn interface_contracts_keep_schema_zero() {
91        let witness = refinement_witness_v0(
92            "top",
93            RefinementVerdictV0::SatisfiedAll,
94            vec![refinement_provenance_v0(
95                "cascade-refinement",
96                Some("evaluate_static_supports_condition"),
97            )],
98        );
99        assert_eq!(witness.schema_version, "0");
100        assert_eq!(witness.layer_marker, "refinement-cascade");
101        assert!(witness.legacy_proofs_byte_untouched);
102    }
103}
omena_refinement_trait/lib.rs

omena_refinement_trait/
lib.rs
