omena_abstract_value/
semiring.rs

1use serde::Serialize;
2use std::fmt::Debug;
3
4pub trait ProvenanceSemiringV0: Default + Clone + PartialEq + Eq + Serialize {
5    const IDENTIFIER: &'static str;
6    type Element: Clone + Debug + PartialEq + Eq + Serialize;
7
8    fn semiring_identifier(&self) -> &'static str {
9        Self::IDENTIFIER
10    }
11
12    fn zero(&self) -> Self::Element;
13    fn one(&self) -> Self::Element;
14    fn add(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element;
15    fn multiply(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element;
16    fn idempotent_addition(&self) -> bool;
17}
18
19#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
20#[serde(rename_all = "camelCase")]
21pub struct ProvenanceSemiringLawReportV0 {
22    pub schema_version: &'static str,
23    pub product: &'static str,
24    pub layer_marker: &'static str,
25    pub feature_gate: &'static str,
26    pub semiring_identifier: &'static str,
27    pub fixture_count: usize,
28    pub additive_identity_holds: bool,
29    pub multiplicative_identity_holds: bool,
30    pub zero_is_absorbing: bool,
31    pub addition_associative: bool,
32    pub multiplication_associative: bool,
33    pub multiplication_distributes_over_addition: bool,
34    pub additive_idempotence_matches_descriptor: bool,
35    pub all_fixture_laws_hold: bool,
36}
37
38pub fn verify_provenance_semiring_laws_on_fixtures<K: ProvenanceSemiringV0>(
39    semiring: &K,
40    fixtures: &[K::Element],
41) -> ProvenanceSemiringLawReportV0 {
42    let zero = semiring.zero();
43    let one = semiring.one();
44    let additive_identity_holds = fixtures
45        .iter()
46        .all(|value| semiring.add(value, &zero) == *value && semiring.add(&zero, value) == *value);
47    let multiplicative_identity_holds = fixtures.iter().all(|value| {
48        semiring.multiply(value, &one) == *value && semiring.multiply(&one, value) == *value
49    });
50    let zero_is_absorbing = fixtures.iter().all(|value| {
51        semiring.multiply(value, &zero) == zero && semiring.multiply(&zero, value) == zero
52    });
53    let addition_associative = fixtures.iter().all(|lhs| {
54        fixtures.iter().all(|mid| {
55            fixtures.iter().all(|rhs| {
56                semiring.add(&semiring.add(lhs, mid), rhs)
57                    == semiring.add(lhs, &semiring.add(mid, rhs))
58            })
59        })
60    });
61    let multiplication_associative = fixtures.iter().all(|lhs| {
62        fixtures.iter().all(|mid| {
63            fixtures.iter().all(|rhs| {
64                semiring.multiply(&semiring.multiply(lhs, mid), rhs)
65                    == semiring.multiply(lhs, &semiring.multiply(mid, rhs))
66            })
67        })
68    });
69    let multiplication_distributes_over_addition = fixtures.iter().all(|lhs| {
70        fixtures.iter().all(|mid| {
71            fixtures.iter().all(|rhs| {
72                semiring.multiply(lhs, &semiring.add(mid, rhs))
73                    == semiring.add(&semiring.multiply(lhs, mid), &semiring.multiply(lhs, rhs))
74                    && semiring.multiply(&semiring.add(mid, rhs), lhs)
75                        == semiring.add(&semiring.multiply(mid, lhs), &semiring.multiply(rhs, lhs))
76            })
77        })
78    });
79    let additive_idempotence_matches_descriptor = if semiring.idempotent_addition() {
80        fixtures
81            .iter()
82            .all(|value| semiring.add(value, value) == *value)
83    } else {
84        fixtures
85            .iter()
86            .any(|value| semiring.add(value, value) != *value)
87    };
88    let all_fixture_laws_hold = additive_identity_holds
89        && multiplicative_identity_holds
90        && zero_is_absorbing
91        && addition_associative
92        && multiplication_associative
93        && multiplication_distributes_over_addition
94        && additive_idempotence_matches_descriptor;
95
96    ProvenanceSemiringLawReportV0 {
97        schema_version: "0",
98        product: "omena-abstract-value.provenance-semiring-law-report",
99        layer_marker: "qtt-graded",
100        feature_gate: "qtt-provenance",
101        semiring_identifier: semiring.semiring_identifier(),
102        fixture_count: fixtures.len(),
103        additive_identity_holds,
104        multiplicative_identity_holds,
105        zero_is_absorbing,
106        addition_associative,
107        multiplication_associative,
108        multiplication_distributes_over_addition,
109        additive_idempotence_matches_descriptor,
110        all_fixture_laws_hold,
111    }
112}
113
114#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
115#[serde(rename_all = "camelCase")]
116pub struct Lin01ProvenanceSemiringV0 {
117    pub zero: &'static str,
118    pub one: &'static str,
119    pub addition: &'static str,
120    pub multiplication: &'static str,
121    pub idempotent_addition: bool,
122}
123
124impl Lin01ProvenanceSemiringV0 {
125    pub const fn new() -> Self {
126        Self {
127            zero: "0",
128            one: "1",
129            addition: "or",
130            multiplication: "andThen",
131            idempotent_addition: true,
132        }
133    }
134}
135
136impl Default for Lin01ProvenanceSemiringV0 {
137    fn default() -> Self {
138        Self::new()
139    }
140}
141
142impl ProvenanceSemiringV0 for Lin01ProvenanceSemiringV0 {
143    const IDENTIFIER: &'static str = "lin01";
144    type Element = bool;
145
146    fn zero(&self) -> Self::Element {
147        false
148    }
149
150    fn one(&self) -> Self::Element {
151        true
152    }
153
154    fn add(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element {
155        *lhs || *rhs
156    }
157
158    fn multiply(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element {
159        *lhs && *rhs
160    }
161
162    fn idempotent_addition(&self) -> bool {
163        self.idempotent_addition
164    }
165}
166
167#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
168#[serde(rename_all = "camelCase")]
169pub struct NaturalCountProvenanceSemiringV0 {
170    pub zero: u8,
171    pub one: u8,
172    pub addition: &'static str,
173    pub multiplication: &'static str,
174    pub idempotent_addition: bool,
175}
176
177impl NaturalCountProvenanceSemiringV0 {
178    pub const fn new() -> Self {
179        Self {
180            zero: 0,
181            one: 1,
182            addition: "plus",
183            multiplication: "times",
184            idempotent_addition: false,
185        }
186    }
187}
188
189impl Default for NaturalCountProvenanceSemiringV0 {
190    fn default() -> Self {
191        Self::new()
192    }
193}
194
195impl ProvenanceSemiringV0 for NaturalCountProvenanceSemiringV0 {
196    const IDENTIFIER: &'static str = "naturalCount";
197    type Element = u16;
198
199    fn zero(&self) -> Self::Element {
200        self.zero.into()
201    }
202
203    fn one(&self) -> Self::Element {
204        self.one.into()
205    }
206
207    fn add(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element {
208        lhs.saturating_add(*rhs)
209    }
210
211    fn multiply(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element {
212        lhs.saturating_mul(*rhs)
213    }
214
215    fn idempotent_addition(&self) -> bool {
216        self.idempotent_addition
217    }
218}
219
220#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize)]
221#[serde(rename_all = "camelCase")]
222pub enum TropicalCostV0 {
223    Finite(u16),
224    Infinity,
225}
226
227#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
228#[serde(rename_all = "camelCase")]
229pub struct TropicalProvenanceSemiringV0 {
230    pub zero: &'static str,
231    pub one: u8,
232    pub addition: &'static str,
233    pub multiplication: &'static str,
234    pub idempotent_addition: bool,
235}
236
237impl TropicalProvenanceSemiringV0 {
238    pub const fn new() -> Self {
239        Self {
240            zero: "infinity",
241            one: 0,
242            addition: "min",
243            multiplication: "plus",
244            idempotent_addition: true,
245        }
246    }
247}
248
249impl Default for TropicalProvenanceSemiringV0 {
250    fn default() -> Self {
251        Self::new()
252    }
253}
254
255impl ProvenanceSemiringV0 for TropicalProvenanceSemiringV0 {
256    const IDENTIFIER: &'static str = "tropical";
257    type Element = TropicalCostV0;
258
259    fn zero(&self) -> Self::Element {
260        TropicalCostV0::Infinity
261    }
262
263    fn one(&self) -> Self::Element {
264        TropicalCostV0::Finite(self.one.into())
265    }
266
267    fn add(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element {
268        (*lhs).min(*rhs)
269    }
270
271    fn multiply(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element {
272        match (lhs, rhs) {
273            (TropicalCostV0::Finite(lhs), TropicalCostV0::Finite(rhs)) => {
274                TropicalCostV0::Finite(lhs.saturating_add(*rhs))
275            }
276            _ => TropicalCostV0::Infinity,
277        }
278    }
279
280    fn idempotent_addition(&self) -> bool {
281        self.idempotent_addition
282    }
283}
284
285#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
286#[serde(rename_all = "camelCase")]
287pub struct ViterbiProvenanceSemiringV0 {
288    pub zero: u8,
289    pub one: u8,
290    pub addition: &'static str,
291    pub multiplication: &'static str,
292    pub idempotent_addition: bool,
293}
294
295impl ViterbiProvenanceSemiringV0 {
296    pub const fn new() -> Self {
297        Self {
298            zero: 0,
299            one: 1,
300            addition: "max",
301            multiplication: "times",
302            idempotent_addition: true,
303        }
304    }
305}
306
307impl Default for ViterbiProvenanceSemiringV0 {
308    fn default() -> Self {
309        Self::new()
310    }
311}
312
313impl ProvenanceSemiringV0 for ViterbiProvenanceSemiringV0 {
314    const IDENTIFIER: &'static str = "viterbi";
315    type Element = u8;
316
317    fn zero(&self) -> Self::Element {
318        self.zero
319    }
320
321    fn one(&self) -> Self::Element {
322        self.one
323    }
324
325    fn add(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element {
326        (*lhs).max(*rhs)
327    }
328
329    fn multiply(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element {
330        lhs.saturating_mul(*rhs)
331    }
332
333    fn idempotent_addition(&self) -> bool {
334        self.idempotent_addition
335    }
336}
337
338#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize)]
339#[serde(rename_all = "camelCase")]
340pub enum SecurityLabelV0 {
341    Public,
342    Trusted,
343}
344
345#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
346#[serde(rename_all = "camelCase")]
347pub struct SecurityLabelProvenanceSemiringV0 {
348    pub zero: &'static str,
349    pub one: &'static str,
350    pub addition: &'static str,
351    pub multiplication: &'static str,
352    pub idempotent_addition: bool,
353}
354
355impl SecurityLabelProvenanceSemiringV0 {
356    pub const fn new() -> Self {
357        Self {
358            zero: "public",
359            one: "trusted",
360            addition: "leastUpperBound",
361            multiplication: "flowThen",
362            idempotent_addition: true,
363        }
364    }
365}
366
367impl Default for SecurityLabelProvenanceSemiringV0 {
368    fn default() -> Self {
369        Self::new()
370    }
371}
372
373impl ProvenanceSemiringV0 for SecurityLabelProvenanceSemiringV0 {
374    const IDENTIFIER: &'static str = "securityLabel";
375    type Element = SecurityLabelV0;
376
377    fn zero(&self) -> Self::Element {
378        SecurityLabelV0::Public
379    }
380
381    fn one(&self) -> Self::Element {
382        SecurityLabelV0::Trusted
383    }
384
385    fn add(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element {
386        (*lhs).max(*rhs)
387    }
388
389    fn multiply(&self, lhs: &Self::Element, rhs: &Self::Element) -> Self::Element {
390        (*lhs).min(*rhs)
391    }
392
393    fn idempotent_addition(&self) -> bool {
394        self.idempotent_addition
395    }
396}
397
398pub fn m4_alpha_provenance_semiring_law_reports_v0() -> Vec<ProvenanceSemiringLawReportV0> {
399    vec![
400        verify_provenance_semiring_laws_on_fixtures(
401            &Lin01ProvenanceSemiringV0::new(),
402            &[false, true],
403        ),
404        verify_provenance_semiring_laws_on_fixtures(
405            &NaturalCountProvenanceSemiringV0::new(),
406            &[0, 1, 2, 3],
407        ),
408        verify_provenance_semiring_laws_on_fixtures(
409            &TropicalProvenanceSemiringV0::new(),
410            &[
411                TropicalCostV0::Finite(0),
412                TropicalCostV0::Finite(1),
413                TropicalCostV0::Finite(3),
414                TropicalCostV0::Infinity,
415            ],
416        ),
417        verify_provenance_semiring_laws_on_fixtures(&ViterbiProvenanceSemiringV0::new(), &[0, 1]),
418        verify_provenance_semiring_laws_on_fixtures(
419            &SecurityLabelProvenanceSemiringV0::new(),
420            &[SecurityLabelV0::Public, SecurityLabelV0::Trusted],
421        ),
422    ]
423}
omena_abstract_value/semiring.rs

omena_abstract_value/
semiring.rs
