Skip to main content

vela_protocol/
provenance_poly.rs

1//! Provenance polynomials in the semiring N[X].
2//!
3//! Implements the algebraic provenance type defined in
4//! `docs/THEORY.md` Sections 2.2, 6, and Theorem 2.
5//!
6//! Each derived object carries a polynomial `p in N[X]` where `X`
7//! is the set of source and event identifiers. The semiring
8//! operations are:
9//!
10//! - **Multiplication.** Joint dependence: `p1 * d3` means a
11//!   derivation needed both p1 and d3.
12//! - **Addition.** Alternative derivation paths: `p1 * d3 + r7 * e2`
13//!   means either path supports the derived object.
14//! - **Coefficients.** Natural-number coefficients count distinct
15//!   derivation events. `2 * p1 * d3` means the substrate observed
16//!   two distinct derivations through the same source combination.
17//!   Idempotent collapse is not assumed.
18//!
19//! ## Retraction
20//!
21//! For a set `Y` of retracted variables, the retraction
22//! homomorphism `rho_Y` maps `x -> 0` for `x in Y` and `x -> x`
23//! otherwise, extended homomorphically over `+` and `*`.
24//!
25//! Retraction is the load-bearing operation behind Theorem 2
26//! (provenance retraction monotonicity): the support set of
27//! `rho_Y(p)` is always a subset of `supp(p)`.
28//!
29//! ## What this module does NOT do
30//!
31//! This module is the abstract algebraic type and its operations.
32//! It does NOT:
33//!
34//! - Wire into Carina event payloads (target v0.85+).
35//! - Compute provenance from the event log (target v0.85+).
36//! - Track support vs refute polynomials per claim-context pair
37//!   (target v0.85+ via a separate `StatusProvenance` type).
38//!
39//! Those wirings ride on top of this primitive in later substrate
40//! cycles.
41
42use std::collections::{BTreeMap, BTreeSet};
43use std::fmt;
44use std::ops::{Add, AddAssign, Mul, MulAssign};
45
46use serde::{Deserialize, Deserializer, Serialize, Serializer};
47
48/// A monomial is a finite multiset of variables (each variable
49/// optionally raised to a positive exponent). Stored as a sorted
50/// map so equality and ordering are deterministic and `serde` is
51/// stable.
52///
53/// The empty monomial represents `1`.
54#[derive(Debug, Clone, Default, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
55pub struct Monomial {
56    factors: BTreeMap<String, u32>,
57}
58
59impl Monomial {
60    /// The empty monomial, representing the multiplicative identity `1`.
61    #[must_use]
62    pub fn one() -> Self {
63        Self::default()
64    }
65
66    /// A single variable with exponent 1.
67    pub fn singleton(var: impl Into<String>) -> Self {
68        let mut m = Self::default();
69        m.factors.insert(var.into(), 1);
70        m
71    }
72
73    /// Build from `(variable, exponent)` pairs. Exponents must be
74    /// strictly positive; pairs with exponent 0 are dropped.
75    pub fn from_factors(factors: impl IntoIterator<Item = (impl Into<String>, u32)>) -> Self {
76        let mut m = Self::default();
77        for (var, exp) in factors {
78            if exp > 0 {
79                let entry = m.factors.entry(var.into()).or_insert(0);
80                *entry = entry.saturating_add(exp);
81            }
82        }
83        m
84    }
85
86    /// Variables appearing in this monomial (with exponents).
87    pub fn factors(&self) -> &BTreeMap<String, u32> {
88        &self.factors
89    }
90
91    /// Set of variable names appearing in this monomial.
92    pub fn variables(&self) -> BTreeSet<String> {
93        self.factors.keys().cloned().collect()
94    }
95
96    /// Whether `var` appears in this monomial with positive exponent.
97    pub fn contains(&self, var: &str) -> bool {
98        self.factors.contains_key(var)
99    }
100
101    /// Whether this is the empty (identity) monomial.
102    #[must_use]
103    pub fn is_one(&self) -> bool {
104        self.factors.is_empty()
105    }
106
107    /// Multiply two monomials by adding exponents.
108    pub fn mul(&self, other: &Self) -> Self {
109        let mut result = self.clone();
110        for (var, exp) in &other.factors {
111            let entry = result.factors.entry(var.clone()).or_insert(0);
112            *entry = entry.saturating_add(*exp);
113        }
114        result
115    }
116}
117
118impl fmt::Display for Monomial {
119    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
120        if self.factors.is_empty() {
121            return write!(f, "1");
122        }
123        let mut first = true;
124        for (var, exp) in &self.factors {
125            if !first {
126                write!(f, "*")?;
127            }
128            first = false;
129            if *exp == 1 {
130                write!(f, "{var}")?;
131            } else {
132                write!(f, "{var}^{exp}")?;
133            }
134        }
135        Ok(())
136    }
137}
138
139/// A provenance polynomial: a finite sum of monomials with
140/// natural-number coefficients.
141///
142/// Stored in normal form: monomials with zero coefficient are
143/// dropped; like terms are merged.
144///
145/// The empty polynomial is `0` (additive identity). The polynomial
146/// `{Monomial::one() -> 1}` is the multiplicative identity `1`.
147///
148/// Custom serde: serialized as a sorted array of
149/// `{"monomial": ..., "coefficient": n}` entries, since JSON
150/// objects require string keys.
151#[derive(Debug, Clone, Default, PartialEq, Eq)]
152pub struct ProvenancePoly {
153    /// Map from monomial to its (positive) natural-number coefficient.
154    /// Entries with zero coefficient are removed eagerly.
155    terms: BTreeMap<Monomial, u64>,
156}
157
158#[derive(Serialize, Deserialize)]
159struct PolyTerm {
160    monomial: Monomial,
161    coefficient: u64,
162}
163
164impl Serialize for ProvenancePoly {
165    fn serialize<S: Serializer>(&self, serializer: S) -> Result<S::Ok, S::Error> {
166        let entries: Vec<PolyTerm> = self
167            .terms
168            .iter()
169            .map(|(m, c)| PolyTerm {
170                monomial: m.clone(),
171                coefficient: *c,
172            })
173            .collect();
174        entries.serialize(serializer)
175    }
176}
177
178impl<'de> Deserialize<'de> for ProvenancePoly {
179    fn deserialize<D: Deserializer<'de>>(deserializer: D) -> Result<Self, D::Error> {
180        let entries: Vec<PolyTerm> = Vec::deserialize(deserializer)?;
181        let mut poly = Self::default();
182        for entry in entries {
183            poly.insert_term(entry.monomial, entry.coefficient);
184        }
185        Ok(poly)
186    }
187}
188
189impl ProvenancePoly {
190    /// Additive identity: the polynomial `0`.
191    #[must_use]
192    pub fn zero() -> Self {
193        Self::default()
194    }
195
196    /// Multiplicative identity: the polynomial `1`.
197    #[must_use]
198    pub fn one() -> Self {
199        let mut p = Self::default();
200        p.terms.insert(Monomial::one(), 1);
201        p
202    }
203
204    /// Polynomial consisting of a single variable with coefficient 1.
205    pub fn singleton(var: impl Into<String>) -> Self {
206        let mut p = Self::default();
207        p.terms.insert(Monomial::singleton(var), 1);
208        p
209    }
210
211    /// Polynomial consisting of a single monomial with the given
212    /// coefficient. If the coefficient is 0, returns `zero()`.
213    pub fn from_monomial(monomial: Monomial, coefficient: u64) -> Self {
214        let mut p = Self::default();
215        if coefficient > 0 {
216            p.terms.insert(monomial, coefficient);
217        }
218        p
219    }
220
221    /// Iterate `(monomial, coefficient)` in monomial-sorted order.
222    pub fn terms(&self) -> impl Iterator<Item = (&Monomial, &u64)> {
223        self.terms.iter()
224    }
225
226    /// Number of distinct monomials with positive coefficient.
227    pub fn term_count(&self) -> usize {
228        self.terms.len()
229    }
230
231    /// Whether this is the additive identity.
232    #[must_use]
233    pub fn is_zero(&self) -> bool {
234        self.terms.is_empty()
235    }
236
237    /// Coefficient of a specific monomial, or 0 if not present.
238    pub fn coefficient(&self, monomial: &Monomial) -> u64 {
239        self.terms.get(monomial).copied().unwrap_or(0)
240    }
241
242    /// Support: the set of variables appearing in any monomial with
243    /// positive coefficient.
244    ///
245    /// This is what Theorem 2 bounds under retraction: for any
246    /// retracted set `Y`, `support(retract(p, Y))` is a subset of
247    /// `support(p)`.
248    pub fn support(&self) -> BTreeSet<String> {
249        let mut result = BTreeSet::new();
250        for monomial in self.terms.keys() {
251            for var in monomial.factors.keys() {
252                result.insert(var.clone());
253            }
254        }
255        result
256    }
257
258    /// Add a single term in place, merging like monomials.
259    pub fn insert_term(&mut self, monomial: Monomial, coefficient: u64) {
260        if coefficient == 0 {
261            return;
262        }
263        let entry = self.terms.entry(monomial).or_insert(0);
264        *entry = entry.saturating_add(coefficient);
265    }
266
267    /// Retract every variable in `retracted` by the substitution
268    /// `x -> 0`. This is the homomorphism `rho_Y` from
269    /// `docs/THEORY.md` Section 6.
270    ///
271    /// Operationally: any monomial containing a retracted variable
272    /// is dropped. Monomials with no retracted variables are kept
273    /// with their coefficients unchanged.
274    pub fn retract<S: AsRef<str>>(&self, retracted: &BTreeSet<S>) -> Self {
275        let retracted_set: BTreeSet<&str> = retracted.iter().map(AsRef::as_ref).collect();
276        let mut result = Self::default();
277        for (monomial, coefficient) in &self.terms {
278            let touches_retracted = monomial
279                .factors
280                .keys()
281                .any(|v| retracted_set.contains(v.as_str()));
282            if !touches_retracted {
283                result.terms.insert(monomial.clone(), *coefficient);
284            }
285        }
286        result
287    }
288}
289
290impl fmt::Display for ProvenancePoly {
291    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
292        if self.terms.is_empty() {
293            return write!(f, "0");
294        }
295        let mut first = true;
296        for (monomial, coefficient) in &self.terms {
297            if !first {
298                write!(f, " + ")?;
299            }
300            first = false;
301            if *coefficient == 1 {
302                write!(f, "{monomial}")?;
303            } else if monomial.is_one() {
304                write!(f, "{coefficient}")?;
305            } else {
306                write!(f, "{coefficient}*{monomial}")?;
307            }
308        }
309        Ok(())
310    }
311}
312
313// Operator overloads for ergonomics. Owned versions take ownership;
314// reference versions are used in tests and examples.
315
316impl Add<&ProvenancePoly> for &ProvenancePoly {
317    type Output = ProvenancePoly;
318
319    fn add(self, other: &ProvenancePoly) -> ProvenancePoly {
320        let mut result = self.clone();
321        for (monomial, coefficient) in &other.terms {
322            result.insert_term(monomial.clone(), *coefficient);
323        }
324        result
325    }
326}
327
328impl Add for ProvenancePoly {
329    type Output = ProvenancePoly;
330
331    fn add(self, other: ProvenancePoly) -> ProvenancePoly {
332        &self + &other
333    }
334}
335
336impl AddAssign<&ProvenancePoly> for ProvenancePoly {
337    fn add_assign(&mut self, other: &ProvenancePoly) {
338        for (monomial, coefficient) in &other.terms {
339            self.insert_term(monomial.clone(), *coefficient);
340        }
341    }
342}
343
344impl Mul<&ProvenancePoly> for &ProvenancePoly {
345    type Output = ProvenancePoly;
346
347    fn mul(self, other: &ProvenancePoly) -> ProvenancePoly {
348        let mut result = ProvenancePoly::zero();
349        for (m1, c1) in &self.terms {
350            for (m2, c2) in &other.terms {
351                let product_monomial = m1.mul(m2);
352                let product_coefficient = c1.saturating_mul(*c2);
353                result.insert_term(product_monomial, product_coefficient);
354            }
355        }
356        result
357    }
358}
359
360impl Mul for ProvenancePoly {
361    type Output = ProvenancePoly;
362
363    fn mul(self, other: ProvenancePoly) -> ProvenancePoly {
364        &self * &other
365    }
366}
367
368impl MulAssign<&ProvenancePoly> for ProvenancePoly {
369    fn mul_assign(&mut self, other: &ProvenancePoly) {
370        *self = &*self * other;
371    }
372}
373
374#[cfg(test)]
375mod tests {
376    use super::*;
377
378    fn vars(names: &[&str]) -> BTreeSet<String> {
379        names.iter().map(|s| (*s).to_string()).collect()
380    }
381
382    #[test]
383    fn zero_is_additive_identity() {
384        let p = ProvenancePoly::singleton("p1");
385        let zero = ProvenancePoly::zero();
386        assert_eq!(&p + &zero, p);
387        assert_eq!(&zero + &p, p);
388    }
389
390    #[test]
391    fn one_is_multiplicative_identity() {
392        let p = ProvenancePoly::singleton("p1");
393        let one = ProvenancePoly::one();
394        assert_eq!(&p * &one, p);
395        assert_eq!(&one * &p, p);
396    }
397
398    #[test]
399    fn multiplication_combines_factors() {
400        let p1 = ProvenancePoly::singleton("p1");
401        let d3 = ProvenancePoly::singleton("d3");
402        let product = &p1 * &d3;
403        // p1 * d3 is a single monomial with coefficient 1
404        assert_eq!(product.term_count(), 1);
405        assert_eq!(product.support(), vars(&["d3", "p1"]));
406        assert_eq!(format!("{product}"), "d3*p1");
407    }
408
409    #[test]
410    fn addition_records_alternative_paths() {
411        // p1*d3 + r7*e2
412        let path1 = &ProvenancePoly::singleton("p1") * &ProvenancePoly::singleton("d3");
413        let path2 = &ProvenancePoly::singleton("r7") * &ProvenancePoly::singleton("e2");
414        let combined = &path1 + &path2;
415        assert_eq!(combined.term_count(), 2);
416        assert_eq!(combined.support(), vars(&["d3", "e2", "p1", "r7"]));
417    }
418
419    #[test]
420    fn coefficient_counts_distinct_derivations() {
421        // Two reviewers independently derive the same finding through p1*d3.
422        let derivation = &ProvenancePoly::singleton("p1") * &ProvenancePoly::singleton("d3");
423        let combined = &derivation + &derivation;
424        assert_eq!(combined.term_count(), 1);
425        let key = Monomial::from_factors([("d3", 1u32), ("p1", 1)]);
426        assert_eq!(combined.coefficient(&key), 2);
427        // Idempotent collapse is NOT assumed: p + p != p.
428        assert_ne!(combined, derivation);
429    }
430
431    #[test]
432    fn theorem_2_retraction_support_is_subset() {
433        // p = p1*d3 + r7*e2
434        let p = &(&ProvenancePoly::singleton("p1") * &ProvenancePoly::singleton("d3"))
435            + &(&ProvenancePoly::singleton("r7") * &ProvenancePoly::singleton("e2"));
436
437        let original_support = p.support();
438        // Retract p1
439        let retracted = p.retract(&vars(&["p1"]));
440        let retracted_support = retracted.support();
441        // Theorem 2: supp(rho_Y(p)) is a subset of supp(p)
442        assert!(retracted_support.is_subset(&original_support));
443    }
444
445    #[test]
446    fn theorem_2_monomials_with_retracted_var_are_deleted() {
447        let p = &(&ProvenancePoly::singleton("p1") * &ProvenancePoly::singleton("d3"))
448            + &(&ProvenancePoly::singleton("r7") * &ProvenancePoly::singleton("e2"));
449
450        let retracted = p.retract(&vars(&["p1"]));
451        // The p1*d3 monomial should be gone; r7*e2 remains.
452        assert_eq!(retracted.term_count(), 1);
453        assert_eq!(retracted.support(), vars(&["e2", "r7"]));
454        // The p1*d3 monomial coefficient is now 0.
455        let p1d3 = Monomial::from_factors([("d3", 1u32), ("p1", 1)]);
456        assert_eq!(retracted.coefficient(&p1d3), 0);
457        // The r7*e2 monomial coefficient is unchanged.
458        let r7e2 = Monomial::from_factors([("e2", 1u32), ("r7", 1)]);
459        assert_eq!(retracted.coefficient(&r7e2), 1);
460    }
461
462    #[test]
463    fn theorem_2_monomials_without_retracted_var_are_unchanged() {
464        // p = 2*p1*d3 + r7
465        let mut p = ProvenancePoly::zero();
466        p.insert_term(Monomial::from_factors([("p1", 1u32), ("d3", 1)]), 2);
467        p.insert_term(Monomial::singleton("r7"), 1);
468
469        let retracted = p.retract(&vars(&["p1"]));
470        // The 2*p1*d3 monomial is dropped; r7 remains with coefficient 1.
471        assert_eq!(retracted.term_count(), 1);
472        assert_eq!(retracted.coefficient(&Monomial::singleton("r7")), 1);
473    }
474
475    #[test]
476    fn theorem_2_no_new_monomials_after_retraction() {
477        // Build a complex polynomial: 3*p1*d3 + 2*p1*d3*e2 + r7
478        let mut p = ProvenancePoly::zero();
479        p.insert_term(Monomial::from_factors([("p1", 1u32), ("d3", 1)]), 3);
480        p.insert_term(
481            Monomial::from_factors([("p1", 1u32), ("d3", 1), ("e2", 1)]),
482            2,
483        );
484        p.insert_term(Monomial::singleton("r7"), 1);
485
486        let original_monomials: BTreeSet<Monomial> = p.terms.keys().cloned().collect();
487        let retracted = p.retract(&vars(&["p1"]));
488        let retracted_monomials: BTreeSet<Monomial> = retracted.terms.keys().cloned().collect();
489
490        // Every retracted monomial must already be in the original
491        // (no new monomials introduced by substitution).
492        assert!(retracted_monomials.is_subset(&original_monomials));
493    }
494
495    #[test]
496    fn retract_empty_set_is_identity() {
497        let p = &(&ProvenancePoly::singleton("p1") * &ProvenancePoly::singleton("d3"))
498            + &(&ProvenancePoly::singleton("r7") * &ProvenancePoly::singleton("e2"));
499        let retracted = p.retract(&BTreeSet::<String>::new());
500        assert_eq!(retracted, p);
501    }
502
503    #[test]
504    fn retract_all_support_yields_zero() {
505        let p = &(&ProvenancePoly::singleton("p1") * &ProvenancePoly::singleton("d3"))
506            + &(&ProvenancePoly::singleton("r7") * &ProvenancePoly::singleton("e2"));
507        let retracted = p.retract(&vars(&["d3", "e2", "p1", "r7"]));
508        assert!(retracted.is_zero());
509    }
510
511    #[test]
512    fn retract_is_idempotent() {
513        let p = &(&ProvenancePoly::singleton("p1") * &ProvenancePoly::singleton("d3"))
514            + &(&ProvenancePoly::singleton("r7") * &ProvenancePoly::singleton("e2"));
515        let once = p.retract(&vars(&["p1"]));
516        let twice = once.retract(&vars(&["p1"]));
517        assert_eq!(once, twice);
518    }
519
520    #[test]
521    fn retract_is_homomorphism_over_addition() {
522        // rho(p + q) == rho(p) + rho(q)
523        let p = &ProvenancePoly::singleton("p1") * &ProvenancePoly::singleton("d3");
524        let q = &ProvenancePoly::singleton("p1") * &ProvenancePoly::singleton("e2");
525        let retracted_combined = (&p + &q).retract(&vars(&["p1"]));
526        let combined_retracted = &p.retract(&vars(&["p1"])) + &q.retract(&vars(&["p1"]));
527        assert_eq!(retracted_combined, combined_retracted);
528    }
529
530    #[test]
531    fn retract_is_homomorphism_over_multiplication() {
532        // rho(p * q) == rho(p) * rho(q)
533        let p = ProvenancePoly::singleton("p1");
534        let q = ProvenancePoly::singleton("d3");
535        let retracted_product = (&p * &q).retract(&vars(&["p1"]));
536        let product_retracted = &p.retract(&vars(&["p1"])) * &q.retract(&vars(&["p1"]));
537        assert_eq!(retracted_product, product_retracted);
538    }
539
540    #[test]
541    fn display_renders_canonical_form() {
542        // 2*p1*d3 + r7
543        let mut p = ProvenancePoly::zero();
544        p.insert_term(Monomial::from_factors([("p1", 1u32), ("d3", 1)]), 2);
545        p.insert_term(Monomial::singleton("r7"), 1);
546        // Monomials are sorted alphabetically by their first variable name:
547        // d3*p1 (sorts before r7), then r7.
548        assert_eq!(format!("{p}"), "2*d3*p1 + r7");
549    }
550
551    #[test]
552    fn distributivity_holds() {
553        // p * (q + r) = p*q + p*r
554        let p = ProvenancePoly::singleton("p1");
555        let q = ProvenancePoly::singleton("d3");
556        let r = ProvenancePoly::singleton("e2");
557        let lhs = &p * &(&q + &r);
558        let rhs = &(&p * &q) + &(&p * &r);
559        assert_eq!(lhs, rhs);
560    }
561
562    #[test]
563    fn associativity_of_addition() {
564        let p = ProvenancePoly::singleton("p1");
565        let q = ProvenancePoly::singleton("d3");
566        let r = ProvenancePoly::singleton("e2");
567        assert_eq!(&(&p + &q) + &r, &p + &(&q + &r));
568    }
569
570    #[test]
571    fn commutativity_of_addition() {
572        let p = ProvenancePoly::singleton("p1");
573        let q = ProvenancePoly::singleton("d3");
574        assert_eq!(&p + &q, &q + &p);
575    }
576
577    #[test]
578    fn associativity_of_multiplication() {
579        let p = ProvenancePoly::singleton("p1");
580        let q = ProvenancePoly::singleton("d3");
581        let r = ProvenancePoly::singleton("e2");
582        assert_eq!(&(&p * &q) * &r, &p * &(&q * &r));
583    }
584
585    #[test]
586    fn commutativity_of_multiplication() {
587        let p = ProvenancePoly::singleton("p1");
588        let q = ProvenancePoly::singleton("d3");
589        assert_eq!(&p * &q, &q * &p);
590    }
591
592    #[test]
593    fn serde_round_trip() {
594        let p = &(&ProvenancePoly::singleton("p1") * &ProvenancePoly::singleton("d3"))
595            + &(&ProvenancePoly::singleton("r7") * &ProvenancePoly::singleton("e2"));
596        let json = serde_json::to_string(&p).expect("serialize");
597        let restored: ProvenancePoly = serde_json::from_str(&json).expect("deserialize");
598        assert_eq!(restored, p);
599    }
600}