karpal_verify/
signature.rs

1#[cfg(not(feature = "std"))]
2use alloc::{collections::BTreeMap, string::String};
3#[cfg(feature = "std")]
4use std::{collections::BTreeMap, string::String};
5
6use crate::obligation::Sort;
7
8/// A named binary operator in an algebraic signature.
9#[derive(Debug, Clone, PartialEq, Eq)]
10pub struct BinarySymbol {
11    pub name: String,
12}
13
14impl BinarySymbol {
15    pub fn new(name: impl Into<String>) -> Self {
16        Self { name: name.into() }
17    }
18}
19
20/// A named unary operator in an algebraic signature.
21#[derive(Debug, Clone, PartialEq, Eq)]
22pub struct UnarySymbol {
23    pub name: String,
24}
25
26impl UnarySymbol {
27    pub fn new(name: impl Into<String>) -> Self {
28        Self { name: name.into() }
29    }
30}
31
32/// A named constant in an algebraic signature.
33#[derive(Debug, Clone, PartialEq, Eq)]
34pub struct ConstantSymbol {
35    pub name: String,
36}
37
38impl ConstantSymbol {
39    pub fn new(name: impl Into<String>) -> Self {
40        Self { name: name.into() }
41    }
42}
43
44/// Backend-agnostic signature for an algebraic structure.
45///
46/// This lets Phase 12 build proof obligations from a reusable semantic model
47/// instead of ad-hoc raw strings at each export site.
48#[derive(Debug, Clone, PartialEq, Eq)]
49pub struct AlgebraicSignature {
50    pub carrier: Sort,
51    binary: BTreeMap<String, BinarySymbol>,
52    unary: BTreeMap<String, UnarySymbol>,
53    constants: BTreeMap<String, ConstantSymbol>,
54}
55
56impl AlgebraicSignature {
57    pub fn new(carrier: Sort) -> Self {
58        Self {
59            carrier,
60            binary: BTreeMap::new(),
61            unary: BTreeMap::new(),
62            constants: BTreeMap::new(),
63        }
64    }
65
66    pub fn semigroup(carrier: Sort, combine: impl Into<String>) -> Self {
67        Self::new(carrier).with_binary("combine", combine)
68    }
69
70    pub fn monoid(carrier: Sort, combine: impl Into<String>, identity: impl Into<String>) -> Self {
71        Self::semigroup(carrier, combine).with_constant("identity", identity)
72    }
73
74    pub fn group(
75        carrier: Sort,
76        combine: impl Into<String>,
77        identity: impl Into<String>,
78        inverse: impl Into<String>,
79    ) -> Self {
80        Self::monoid(carrier, combine, identity).with_unary("inverse", inverse)
81    }
82
83    pub fn semiring(
84        carrier: Sort,
85        add: impl Into<String>,
86        mul: impl Into<String>,
87        zero: impl Into<String>,
88        one: impl Into<String>,
89    ) -> Self {
90        Self::new(carrier)
91            .with_binary("add", add)
92            .with_binary("mul", mul)
93            .with_constant("zero", zero)
94            .with_constant("one", one)
95    }
96
97    pub fn lattice(carrier: Sort, meet: impl Into<String>, join: impl Into<String>) -> Self {
98        Self::new(carrier)
99            .with_binary("meet", meet)
100            .with_binary("join", join)
101    }
102
103    pub fn with_binary(mut self, role: impl Into<String>, symbol: impl Into<String>) -> Self {
104        self.binary.insert(role.into(), BinarySymbol::new(symbol));
105        self
106    }
107
108    pub fn with_unary(mut self, role: impl Into<String>, symbol: impl Into<String>) -> Self {
109        self.unary.insert(role.into(), UnarySymbol::new(symbol));
110        self
111    }
112
113    pub fn with_constant(mut self, role: impl Into<String>, symbol: impl Into<String>) -> Self {
114        self.constants
115            .insert(role.into(), ConstantSymbol::new(symbol));
116        self
117    }
118
119    pub fn binary(&self, role: &str) -> Option<&str> {
120        self.binary.get(role).map(|symbol| symbol.name.as_str())
121    }
122
123    pub fn unary(&self, role: &str) -> Option<&str> {
124        self.unary.get(role).map(|symbol| symbol.name.as_str())
125    }
126
127    pub fn constant(&self, role: &str) -> Option<&str> {
128        self.constants.get(role).map(|symbol| symbol.name.as_str())
129    }
130
131    pub fn require_binary(&self, role: &str) -> &str {
132        self.binary(role)
133            .unwrap_or_else(|| panic!("missing binary symbol for role `{role}`"))
134    }
135
136    pub fn require_unary(&self, role: &str) -> &str {
137        self.unary(role)
138            .unwrap_or_else(|| panic!("missing unary symbol for role `{role}`"))
139    }
140
141    pub fn require_constant(&self, role: &str) -> &str {
142        self.constant(role)
143            .unwrap_or_else(|| panic!("missing constant symbol for role `{role}`"))
144    }
145}
146
147#[cfg(test)]
148mod tests {
149    use super::*;
150
151    #[test]
152    fn group_signature_registers_expected_roles() {
153        let sig = AlgebraicSignature::group(Sort::Int, "combine", "e", "inv");
154        assert_eq!(sig.require_binary("combine"), "combine");
155        assert_eq!(sig.require_constant("identity"), "e");
156        assert_eq!(sig.require_unary("inverse"), "inv");
157    }
158
159    #[test]
160    fn semiring_signature_registers_expected_roles() {
161        let sig = AlgebraicSignature::semiring(Sort::Int, "add", "mul", "zero", "one");
162        assert_eq!(sig.require_binary("add"), "add");
163        assert_eq!(sig.require_binary("mul"), "mul");
164        assert_eq!(sig.require_constant("zero"), "zero");
165        assert_eq!(sig.require_constant("one"), "one");
166    }
167}
karpal_verify/signature.rs

karpal_verify/
signature.rs
