Skip to main content

hekate_program/
linearized.rs

1// SPDX-FileCopyrightText: 2026 Andrei Kochergin <andrei@oumuamua.dev>
2// SPDX-FileCopyrightText: 2026 Oumuamua Labs <info@oumuamua.dev>
3// SPDX-License-Identifier: AGPL-3.0-only
4
5//! F₂-linear maps on GF(2^128) as linearized polynomials
6//! `Σ_j μ_j x^{2^j}`, and the outer-statement gadget that
7//! proves `Σ_c a_c φ(h_c)` on committed pad entries with
8//! a Frobenius-Horner chain of 127 squarings.
9
10use crate::predicate::{AffineRow, Unknown, WireRole};
11use alloc::vec;
12use alloc::vec::Vec;
13use hekate_math::{Block128, Flat, HardwareField, TowerField};
14
15pub const BITS: usize = 128;
16
17const DUAL_KERNEL: [u8; 8] = [0x29, 0xb0, 0x58, 0x05, 0xa6, 0x53, 0xa4, 0x52];
18
19/// `Δ = Σ_c a_c φ(h_c)` over the pad entries `(pad, a_c)`
20/// as the chain `X_127 = T'_127`, `X_j = T'_j + X_{j+1}²`,
21/// `T'_j = Σ_c σ^{-j}(μ_j a_c) h_c`, on squaring wires
22/// `first_wire + j - 1` for `j = 1..128`; `Δ = X_0`.
23pub struct RingGadget<F> {
24    pub ring: Vec<(u32, Flat<F>)>,
25    pub mu: Vec<Flat<F>>,
26    pub first_wire: u32,
27
28    /// Statement row of `Lhs_1`; the chain
29    /// occupies `2 · (BITS - 1)` rows from there.
30    pub first_row: usize,
31}
32
33impl<F: HardwareField> RingGadget<F> {
34    pub fn new(ring: Vec<(u32, Flat<F>)>, mu: Vec<Flat<F>>, first_wire: u32) -> Self {
35        Self {
36            ring,
37            mu,
38            first_wire,
39            first_row: 0,
40        }
41    }
42
43    fn wire(&self, j: usize) -> u32 {
44        self.first_wire + j as u32 - 1
45    }
46
47    /// Statement row of `Lhs_j`; `Rhs_j` follows it.
48    pub fn row_of(&self, j: usize) -> usize {
49        self.first_row + 2 * (j - 1)
50    }
51
52    /// `f(j, tie_j)` for `j = 127` down to `1`,
53    /// `tie_j[c] = σ^{-j}(μ_j a_c)`; the coefficients
54    /// of row `Lhs_j` on the pad entries.
55    pub fn for_each_tie_row(&self, mut f: impl FnMut(usize, &[Flat<F>])) {
56        let mut conj: Vec<Flat<F>> = self.ring.iter().map(|&(_, a)| a).collect();
57        let mut tie = vec![Flat::from_raw(F::ZERO); conj.len()];
58
59        for j in (1..BITS).rev() {
60            for a in conj.iter_mut() {
61                *a = *a * *a;
62            }
63
64            let mu_conj = frobenius(self.mu[j], BITS - j);
65            for (t, &a) in tie.iter_mut().zip(&conj) {
66                *t = a * mu_conj;
67            }
68
69            f(j, &tie);
70        }
71    }
72
73    /// Wire terms of the chain rows, in [`row_of`] order:
74    /// `Lhs_j + Product_{j+1}` and `Rhs_j + Lhs_j`.
75    pub fn wire_rows(&self) -> Vec<AffineRow<F>> {
76        let one = Flat::from_raw(F::ONE);
77        let zero = Flat::from_raw(F::ZERO);
78
79        let mut rows = Vec::with_capacity(2 * (BITS - 1));
80        for j in 1..BITS {
81            let mut unknowns = vec![(
82                Unknown::Wire {
83                    mul: self.wire(j),
84                    role: WireRole::Lhs,
85                },
86                one,
87            )];
88
89            if j + 1 < BITS {
90                unknowns.push((
91                    Unknown::Wire {
92                        mul: self.wire(j + 1),
93                        role: WireRole::Product,
94                    },
95                    one,
96                ));
97            }
98
99            rows.push(AffineRow {
100                unknowns,
101                claims: Vec::new(),
102                constant: zero,
103            });
104
105            rows.push(AffineRow {
106                unknowns: vec![
107                    (
108                        Unknown::Wire {
109                            mul: self.wire(j),
110                            role: WireRole::Rhs,
111                        },
112                        one,
113                    ),
114                    (
115                        Unknown::Wire {
116                            mul: self.wire(j),
117                            role: WireRole::Lhs,
118                        },
119                        one,
120                    ),
121                ],
122                claims: Vec::new(),
123                constant: zero,
124            });
125        }
126
127        rows
128    }
129
130    /// `Δ` over the pad entries and the wire `Product_1`.
131    pub fn delta_form(&self) -> Vec<(Unknown, Flat<F>)> {
132        let mut form: Vec<(Unknown, Flat<F>)> = self
133            .ring
134            .iter()
135            .map(|&(pad, a)| (Unknown::Pad(pad), a * self.mu[0]))
136            .collect();
137
138        form.push((
139            Unknown::Wire {
140                mul: self.wire(1),
141                role: WireRole::Product,
142            },
143            Flat::from_raw(F::ONE),
144        ));
145
146        form
147    }
148
149    /// Honest `[X_j, X_j, X_j²]` for `j = 1..128`
150    /// from the pad values, indexed by wire.
151    pub fn wires(&self, pad_values: &[Flat<F>]) -> Vec<[Flat<F>; 3]> {
152        let mut wires = vec![[Flat::from_raw(F::ZERO); 3]; BITS - 1];
153        let mut x = Flat::from_raw(F::ZERO);
154
155        self.for_each_tie_row(|j, tie| {
156            x = dot(pad_values, tie) + x * x;
157            wires[j - 1] = [x, x, x * x];
158        });
159
160        wires
161    }
162
163    /// `Δ = Σ_c a_c φ(h_c)` on plaintext pad values.
164    pub fn delta(&self, pad_values: &[Flat<F>]) -> Flat<F> {
165        let mut x = Flat::from_raw(F::ZERO);
166        self.for_each_tie_row(|_, tie| x = dot(pad_values, tie) + x * x);
167
168        let mut t0 = Flat::from_raw(F::ZERO);
169        for (&h, &(_, a)) in pad_values.iter().zip(&self.ring) {
170            t0 += a * self.mu[0] * h;
171        }
172
173        t0 + x * x
174    }
175}
176
177/// Trace-dual of the tower basis:
178/// `Tr(dual_basis(u) · 2^w) = [u == w]`.
179pub fn dual_basis(u: usize) -> Block128 {
180    let byte = DUAL_KERNEL[u & 7] as u128;
181    let select = u >> 3;
182
183    let mut acc = 0u128;
184    for p in 0..16 {
185        if p & select == 0 {
186            acc |= byte << (8 * p);
187        }
188    }
189
190    Block128(acc)
191}
192
193/// `μ_j` with `Σ_u eq(r'',u)·bit_u(x) = Σ_j μ_j x^{2^j}`
194/// for every `x`, bits in the tower basis.
195pub fn linearized_coeffs(eq_mix: &[Block128]) -> Vec<Flat<Block128>> {
196    let eq: Vec<Flat<Block128>> = eq_mix.iter().map(|m| m.to_hardware()).collect();
197
198    let mut gamma: Vec<Flat<Block128>> = (0..BITS).map(|u| dual_basis(u).to_hardware()).collect();
199    let mut mu = Vec::with_capacity(BITS);
200
201    for _ in 0..BITS {
202        let mut acc = Flat::from_raw(Block128::ZERO);
203        for (g, m) in gamma.iter().zip(&eq) {
204            acc += *g * *m;
205        }
206
207        mu.push(acc);
208
209        for g in gamma.iter_mut() {
210            *g = *g * *g;
211        }
212    }
213
214    mu
215}
216
217fn dot<F: HardwareField>(a: &[Flat<F>], b: &[Flat<F>]) -> Flat<F> {
218    let mut acc = Flat::from_raw(F::ZERO);
219    for (&x, &y) in a.iter().zip(b) {
220        acc += x * y;
221    }
222
223    acc
224}
225
226fn frobenius<F: HardwareField>(x: Flat<F>, k: usize) -> Flat<F> {
227    let mut acc = x;
228    for _ in 0..k {
229        acc = acc * acc;
230    }
231
232    acc
233}
234
235#[cfg(test)]
236mod tests {
237    use super::*;
238    use crate::expander::{eq_tensor_b, ring_batch_b};
239    use hekate_math::BinaryFieldExtras;
240
241    fn next(state: &mut u128) -> Block128 {
242        *state ^= *state << 13;
243        *state ^= *state >> 7;
244        *state ^= *state << 17;
245
246        Block128(*state)
247    }
248
249    /// Every chain row on the given values: wire terms
250    /// from `wire_rows()`, tie terms streamed onto `row_of(j)`.
251    fn chain_rows(
252        gadget: &RingGadget<Block128>,
253        pad: &[Flat<Block128>],
254        wires: &[[Flat<Block128>; 3]],
255    ) -> Vec<Flat<Block128>> {
256        let value = |u: Unknown| -> Flat<Block128> {
257            match u {
258                Unknown::Pad(i) => pad[i as usize],
259                Unknown::Wire { mul, role } => wires[mul as usize][role as usize],
260            }
261        };
262
263        let mut acc: Vec<Flat<Block128>> = gadget
264            .wire_rows()
265            .iter()
266            .map(|row| {
267                let mut acc = row.constant;
268                for &(u, coeff) in &row.unknowns {
269                    acc += coeff * value(u);
270                }
271
272                acc
273            })
274            .collect();
275
276        gadget.for_each_tie_row(|j, tie| {
277            for (&(pad_idx, _), &t) in gadget.ring.iter().zip(tie) {
278                acc[gadget.row_of(j)] += t * value(Unknown::Pad(pad_idx));
279            }
280        });
281
282        acc
283    }
284
285    #[test]
286    fn dual_basis_is_trace_dual() {
287        for u in 0..BITS {
288            for w in 0..BITS {
289                let tr = (dual_basis(u) * Block128(1u128 << w)).trace().get();
290                assert_eq!(tr == 1, u == w, "u={u} w={w}");
291            }
292        }
293    }
294
295    #[test]
296    fn coefficients_reproduce_bit_transposition() {
297        let mut state = 0x0f0f_1234_5678_9abc_def0_1122_3344_5566u128;
298
299        let r_mix: Vec<Block128> = (0..7).map(|_| next(&mut state)).collect();
300        let eq_mix = eq_tensor_b(&r_mix);
301        let mu = linearized_coeffs(&eq_mix);
302
303        for _ in 0..8 {
304            let x = next(&mut state);
305
306            let mut lin = Flat::from_raw(Block128::ZERO);
307            let mut power = x.to_hardware();
308
309            for m in &mu {
310                lin += *m * power;
311                power = power * power;
312            }
313
314            assert_eq!(lin.to_tower(), ring_batch_b(&[x], &eq_mix));
315        }
316    }
317
318    #[test]
319    fn wires_and_rows_evaluate_to_delta() {
320        let mut state = 0x7777_8888_9999_aaaa_bbbb_cccc_dddd_eeeeu128;
321
322        let r_mix: Vec<Block128> = (0..7).map(|_| next(&mut state)).collect();
323        let eq_mix = eq_tensor_b(&r_mix);
324        let mu = linearized_coeffs(&eq_mix);
325
326        let ring: Vec<(u32, Flat<Block128>)> = (0..5u32)
327            .map(|c| (c, next(&mut state).to_hardware()))
328            .collect();
329        let pad: Vec<Flat<Block128>> = (0..5).map(|_| next(&mut state).to_hardware()).collect();
330
331        let mut direct = Flat::from_raw(Block128::ZERO);
332        for (&(_, a), &h) in ring.iter().zip(&pad) {
333            direct += a * ring_batch_b(&[h.to_tower()], &eq_mix).to_hardware();
334        }
335
336        let gadget = RingGadget::new(ring, mu, 0);
337        assert_eq!(gadget.delta(&pad), direct);
338
339        let wires = gadget.wires(&pad);
340
341        for (i, v) in chain_rows(&gadget, &pad, &wires).iter().enumerate() {
342            assert_eq!(*v, Flat::from_raw(Block128::ZERO), "row {i}");
343        }
344
345        for wire in &wires {
346            assert_eq!(wire[0], wire[1]);
347            assert_eq!(wire[0] * wire[1], wire[2]);
348        }
349
350        let mut delta = Flat::from_raw(Block128::ZERO);
351        for &(u, coeff) in &gadget.delta_form() {
352            delta += coeff
353                * match u {
354                    Unknown::Pad(i) => pad[i as usize],
355                    Unknown::Wire { mul, role } => wires[mul as usize][role as usize],
356                };
357        }
358
359        assert_eq!(delta, direct);
360    }
361
362    /// A floating wire would let a prover pick its value freely;
363    /// every wire must be pinned by a row or a Hadamard triple.
364    #[test]
365    fn chain_is_rigid_under_single_wire_perturbation() {
366        let mut state = 0xdead_beef_0bad_f00d_1357_9bdf_2468_ace0u128;
367
368        let r_mix: Vec<Block128> = (0..7).map(|_| next(&mut state)).collect();
369        let mu = linearized_coeffs(&eq_tensor_b(&r_mix));
370
371        let ring: Vec<(u32, Flat<Block128>)> = (0..7u32)
372            .map(|c| (c, next(&mut state).to_hardware()))
373            .collect();
374        let pad: Vec<Flat<Block128>> = (0..7).map(|_| next(&mut state).to_hardware()).collect();
375
376        let gadget = RingGadget::new(ring, mu, 0);
377        let honest = gadget.wires(&pad);
378        let delta = next(&mut state).to_hardware();
379
380        let zero = Flat::from_raw(Block128::ZERO);
381
382        for target in 0..honest.len() {
383            for role in 0..3 {
384                let mut wires = honest.clone();
385                wires[target][role] += delta;
386
387                let row_broken = chain_rows(&gadget, &pad, &wires)
388                    .iter()
389                    .any(|acc| *acc != zero);
390                let hadamard_broken = wires.iter().any(|w| w[0] * w[1] != w[2]);
391
392                assert!(
393                    row_broken || hadamard_broken,
394                    "wire {target} role {role} perturbation went undetected"
395                );
396            }
397        }
398    }
399}