karpal_verify/
signature.rs

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

karpal_verify/
signature.rs
