logicaffeine_kernel/
word_ring.rs

1//! Kernel ring proofs for the word ring ℤ/2ⁿ (`Word8`/`Word16`/`Word32`/`Word64`).
2//!
3//! The [`crate::ring`] procedure proves a polynomial identity by reducing both sides to a
4//! canonical multivariate polynomial over ℤ and comparing. An identity that canonicalizes equal
5//! holds in **every** commutative ring — so it holds in the word ring ℤ/2ⁿ, whose `+`/`*` are
6//! `wrapping_add`/`wrapping_mul` (the quotient of ℤ by 2ⁿℤ; the ring axioms survive the quotient).
7//!
8//! This is the soundness certificate behind every reassociation and product reshaping the
9//! optimizer performs on wrapping arithmetic: associativity, commutativity, distributivity, and
10//! the Karatsuba/gauss product form are all kernel-certified here, at FULL word width with no
11//! bound on the operands. The bit-logic side of the crypto (`xor`, `rotl`) is not polynomial and
12//! is certified separately by `bitblast→CDCL`.
13//!
14//! Each lemma returns `true` iff the kernel certifies it; the tests pin both the positive proofs
15//! and their non-vacuity (a WRONG identity must NOT canonicalize equal).
16
17use crate::ring::Polynomial;
18
19#[inline]
20fn a() -> Polynomial {
21    Polynomial::var(0)
22}
23#[inline]
24fn b() -> Polynomial {
25    Polynomial::var(1)
26}
27#[inline]
28fn c() -> Polynomial {
29    Polynomial::var(2)
30}
31#[inline]
32fn d() -> Polynomial {
33    Polynomial::var(3)
34}
35
36/// `(a + b) + c = a + (b + c)` — additive associativity in ℤ/2ⁿ.
37pub fn add_associative() -> bool {
38    a().add(&b()).add(&c()).canonical_eq(&a().add(&b().add(&c())))
39}
40
41/// `a + b = b + a` — additive commutativity in ℤ/2ⁿ.
42pub fn add_commutative() -> bool {
43    a().add(&b()).canonical_eq(&b().add(&a()))
44}
45
46/// `(a · b) · c = a · (b · c)` — multiplicative associativity in ℤ/2ⁿ.
47pub fn mul_associative() -> bool {
48    a().mul(&b()).mul(&c()).canonical_eq(&a().mul(&b().mul(&c())))
49}
50
51/// `a · b = b · a` — multiplicative commutativity in ℤ/2ⁿ.
52pub fn mul_commutative() -> bool {
53    a().mul(&b()).canonical_eq(&b().mul(&a()))
54}
55
56/// `a · (b + c) = a · b + a · c` — left distributivity in ℤ/2ⁿ.
57pub fn left_distributive() -> bool {
58    a().mul(&b().add(&c())).canonical_eq(&a().mul(&b()).add(&a().mul(&c())))
59}
60
61/// `a + 0 = a` — additive identity in ℤ/2ⁿ.
62pub fn additive_identity() -> bool {
63    a().add(&Polynomial::constant(0)).canonical_eq(&a())
64}
65
66/// `a · 1 = a` — multiplicative identity in ℤ/2ⁿ.
67pub fn multiplicative_identity() -> bool {
68    a().mul(&Polynomial::constant(1)).canonical_eq(&a())
69}
70
71/// `(a + b)(c + d) = ac + ad + bc + bd` — the Karatsuba/gauss product expansion, the identity the
72/// 3-multiply NTT butterfly and complex-multiply reshaping rely on, certified at full word width.
73pub fn karatsuba_expand() -> bool {
74    let lhs = a().add(&b()).mul(&c().add(&d()));
75    let rhs = a()
76        .mul(&c())
77        .add(&a().mul(&d()))
78        .add(&b().mul(&c()))
79        .add(&b().mul(&d()));
80    lhs.canonical_eq(&rhs)
81}
82
83/// Every word-ring law the optimizer leans on, kernel-certified — a single gate.
84pub fn all_word_ring_laws_certified() -> bool {
85    add_associative()
86        && add_commutative()
87        && mul_associative()
88        && mul_commutative()
89        && left_distributive()
90        && additive_identity()
91        && multiplicative_identity()
92        && karatsuba_expand()
93}
94
95#[cfg(test)]
96mod tests {
97    use super::*;
98
99    #[test]
100    fn word_ring_laws_are_kernel_certified() {
101        assert!(add_associative(), "additive associativity in ℤ/2ⁿ");
102        assert!(add_commutative(), "additive commutativity in ℤ/2ⁿ");
103        assert!(mul_associative(), "multiplicative associativity in ℤ/2ⁿ");
104        assert!(mul_commutative(), "multiplicative commutativity in ℤ/2ⁿ");
105        assert!(left_distributive(), "left distributivity in ℤ/2ⁿ");
106        assert!(additive_identity(), "additive identity in ℤ/2ⁿ");
107        assert!(multiplicative_identity(), "multiplicative identity in ℤ/2ⁿ");
108        assert!(karatsuba_expand(), "Karatsuba/gauss expansion in ℤ/2ⁿ");
109        assert!(all_word_ring_laws_certified(), "the combined gate");
110    }
111
112    #[test]
113    fn wrong_word_ring_identities_are_not_certified() {
114        // Non-vacuity: the prover must reject FALSE identities, or the proofs above are worthless.
115        // a + b ≠ a · b
116        assert!(
117            !a().add(&b()).canonical_eq(&a().mul(&b())),
118            "sum must not be certified equal to product"
119        );
120        // a · (b + c) ≠ a · b + c  (a dropped factor on the second term)
121        assert!(
122            !a()
123                .mul(&b().add(&c()))
124                .canonical_eq(&a().mul(&b()).add(&c())),
125            "a broken distributive law must not be certified"
126        );
127        // (a + b)(c + d) ≠ ac + bd  (the cross terms dropped — the classic Karatsuba bug)
128        assert!(
129            !a()
130                .add(&b())
131                .mul(&c().add(&d()))
132                .canonical_eq(&a().mul(&c()).add(&b().mul(&d()))),
133            "dropping the cross terms must not be certified"
134        );
135    }
136}
logicaffeine_kernel/word_ring.rs

logicaffeine_kernel/
word_ring.rs
