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 ring(
98        carrier: Sort,
99        add: impl Into<String>,
100        mul: impl Into<String>,
101        zero: impl Into<String>,
102        one: impl Into<String>,
103        neg: impl Into<String>,
104    ) -> Self {
105        Self::semiring(carrier, add, mul, zero, one).with_unary("neg", neg)
106    }
107
108    pub fn lattice(carrier: Sort, meet: impl Into<String>, join: impl Into<String>) -> Self {
109        Self::new(carrier)
110            .with_binary("meet", meet)
111            .with_binary("join", join)
112    }
113
114    pub fn with_binary(mut self, role: impl Into<String>, symbol: impl Into<String>) -> Self {
115        self.binary.insert(role.into(), BinarySymbol::new(symbol));
116        self
117    }
118
119    pub fn with_unary(mut self, role: impl Into<String>, symbol: impl Into<String>) -> Self {
120        self.unary.insert(role.into(), UnarySymbol::new(symbol));
121        self
122    }
123
124    pub fn with_constant(mut self, role: impl Into<String>, symbol: impl Into<String>) -> Self {
125        self.constants
126            .insert(role.into(), ConstantSymbol::new(symbol));
127        self
128    }
129
130    pub fn binary(&self, role: &str) -> Option<&str> {
131        self.binary.get(role).map(|symbol| symbol.name.as_str())
132    }
133
134    pub fn unary(&self, role: &str) -> Option<&str> {
135        self.unary.get(role).map(|symbol| symbol.name.as_str())
136    }
137
138    pub fn constant(&self, role: &str) -> Option<&str> {
139        self.constants.get(role).map(|symbol| symbol.name.as_str())
140    }
141
142    pub fn require_binary(&self, role: &str) -> &str {
143        self.binary(role)
144            .unwrap_or_else(|| panic!("missing binary symbol for role `{role}`"))
145    }
146
147    pub fn require_unary(&self, role: &str) -> &str {
148        self.unary(role)
149            .unwrap_or_else(|| panic!("missing unary symbol for role `{role}`"))
150    }
151
152    pub fn require_constant(&self, role: &str) -> &str {
153        self.constant(role)
154            .unwrap_or_else(|| panic!("missing constant symbol for role `{role}`"))
155    }
156}
157
158#[cfg(test)]
159mod tests {
160    use super::*;
161
162    #[test]
163    fn group_signature_registers_expected_roles() {
164        let sig = AlgebraicSignature::group(Sort::Int, "combine", "e", "inv");
165        assert_eq!(sig.require_binary("combine"), "combine");
166        assert_eq!(sig.require_constant("identity"), "e");
167        assert_eq!(sig.require_unary("inverse"), "inv");
168    }
169
170    #[test]
171    fn semiring_signature_registers_expected_roles() {
172        let sig = AlgebraicSignature::semiring(Sort::Int, "add", "mul", "zero", "one");
173        assert_eq!(sig.require_binary("add"), "add");
174        assert_eq!(sig.require_binary("mul"), "mul");
175        assert_eq!(sig.require_constant("zero"), "zero");
176        assert_eq!(sig.require_constant("one"), "one");
177    }
178}
karpal_verify/signature.rs

karpal_verify/
signature.rs
