Skip to main content

hekate_program/
permutation.rs

1// SPDX-License-Identifier: Apache-2.0
2// This file is part of the hekate project.
3// Copyright (C) 2026 Andrei Kochergin <andrei@oumuamua.dev>
4// Copyright (C) 2026 Oumuamua Labs <info@oumuamua.dev>. All rights reserved.
5//
6// Licensed under the Apache License, Version 2.0 (the "License");
7// you may not use this file except in compliance with the License.
8// You may obtain a copy of the License at
9//
10//     http://www.apache.org/licenses/LICENSE-2.0
11//
12// Unless required by applicable law or agreed to in writing, software
13// distributed under the License is distributed on an "AS IS" BASIS,
14// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15// See the License for the specific language governing permissions and
16// limitations under the License.
17
18use alloc::collections::BTreeMap;
19use alloc::string::String;
20use alloc::vec::Vec;
21use hekate_core::errors;
22
23/// Challenge label for Fiat-Shamir transcript.
24pub type ChallengeLabel = &'static [u8];
25
26/// Shared label for the `request_idx` clock
27/// source on stateless-service buses; same
28/// label on both endpoints is load-bearing
29/// for `β`-mix alignment.
30pub const REQUEST_IDX_LABEL: ChallengeLabel = b"kappa_request_idx";
31
32/// LogUp bus semantics.
33///
34/// Cross-bus check sums `claimed_sum` over all
35/// endpoints sharing a `bus_id` and rejects if
36/// the total is non-zero in `GF(2^128)`.
37#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
38pub enum BusKind {
39    #[default]
40    Permutation,
41    Lookup,
42}
43
44/// Byte source for the LogUp
45/// key `Σ β^j · source_j(i)`.
46#[derive(Clone, Debug, PartialEq, Eq)]
47pub enum Source {
48    /// Single byte column from the trace.
49    Column(usize),
50
51    /// Multiple byte columns stitched into one
52    /// key segment via the global `β` schedule.
53    Columns(Vec<usize>),
54
55    /// Virtual clock derived from the row index;
56    /// `num_bytes` controls the byte width.
57    /// Required for `Permutation`-kind buses to
58    /// pin per-row uniqueness and prevent char-2
59    /// even-multiplicity parity collapse.
60    RowIndexLeBytes(usize),
61
62    /// Constant byte for cross-table
63    /// domain separation.
64    Const(u128),
65
66    /// Virtual single byte `k` of the row index.
67    RowIndexByte(usize),
68}
69
70/// One endpoint of a LogUp bus.
71///
72/// Per row `i`:
73/// `h(i) = s(i) / (γ + Σ β^j · source_j(i))`.
74/// The endpoint contributes `claimed_sum = Σ_i h(i)`
75/// (Permutation) or `Σ_i Eq(r_bus, i) · h(i)` (Lookup)
76/// to the cross-bus check.
77///
78/// # Security
79/// `Permutation` kind cancels in char-2 by
80/// multiset parity, so endpoints with even
81/// per-key multiplicity collapse silently.
82/// Use `Source::RowIndexLeBytes` in the key
83/// to force per-row uniqueness, or switch to
84/// `BusKind::Lookup` for positional binding.
85#[derive(Clone, Debug)]
86pub struct PermutationCheckSpec {
87    pub kind: BusKind,
88
89    /// Key sources stitched via the global
90    /// `β` schedule using each label.
91    pub sources: Vec<(Source, ChallengeLabel)>,
92
93    /// Selector column gating the row's `h`.
94    /// `None` means the row is unconditionally active.
95    pub selector: Option<usize>,
96
97    /// Receive-side selector for paired buses.
98    /// AIR must enforce `s_send · s_recv = 0` (char-2 mutex).
99    pub recv_selector: Option<usize>,
100
101    /// Audited carve-out citation for `Permutation`
102    /// specs that intentionally omit a row-index source.
103    pub clock_waiver: Option<String>,
104}
105
106impl PermutationCheckSpec {
107    pub fn new(sources: Vec<(Source, ChallengeLabel)>, selector: Option<usize>) -> Self {
108        Self {
109            sources,
110            selector,
111            recv_selector: None,
112            kind: BusKind::Permutation,
113            clock_waiver: None,
114        }
115    }
116
117    /// Endpoints on a `Lookup` bus must be
118    /// pointwise-equal on the padded hypercube;
119    /// use only when positional binding holds.
120    pub fn new_lookup(sources: Vec<(Source, ChallengeLabel)>, selector: Option<usize>) -> Self {
121        Self {
122            sources,
123            selector,
124            recv_selector: None,
125            kind: BusKind::Lookup,
126            clock_waiver: None,
127        }
128    }
129
130    /// Caller must enforce `s_send · s_recv = 0` in the AIR;
131    /// without it, rows with both selectors high collapse to
132    /// zero in char-2 and slip past cross-bus cancellation.
133    pub fn new_paired(
134        sources: Vec<(Source, ChallengeLabel)>,
135        s_send: usize,
136        s_recv: usize,
137        kind: BusKind,
138    ) -> Self {
139        Self {
140            sources,
141            selector: Some(s_send),
142            recv_selector: Some(s_recv),
143            kind,
144            clock_waiver: None,
145        }
146    }
147
148    /// Audited escape hatch. `reason` must start
149    /// with `"see "` and cite the load-bearing AIR
150    /// constraint (`see <path>:<line>: <argument>`).
151    pub fn with_clock_waiver(mut self, reason: impl Into<String>) -> Self {
152        self.clock_waiver = Some(reason.into());
153        self
154    }
155
156    pub fn num_sources(&self) -> usize {
157        self.sources.len()
158    }
159
160    pub fn has_selector(&self) -> bool {
161        self.selector.is_some()
162    }
163
164    pub fn has_paired(&self) -> bool {
165        self.recv_selector.is_some()
166    }
167
168    /// Reindexes column references when the
169    /// chiplet is embedded into a wider trace.
170    pub fn shift_column_indices(&mut self, offset: usize) {
171        for (source, _) in &mut self.sources {
172            match source {
173                Source::Column(idx) => *idx += offset,
174                Source::Columns(indices) => {
175                    for idx in indices {
176                        *idx += offset;
177                    }
178                }
179                _ => {}
180            }
181        }
182
183        if let Some(sel_idx) = &mut self.selector {
184            *sel_idx += offset;
185        }
186
187        if let Some(sel_idx) = &mut self.recv_selector {
188            *sel_idx += offset;
189        }
190    }
191
192    /// Only structural guarantor of per-row uniqueness;
193    /// label-only stitching is forgeable.
194    pub fn has_real_clock_source(&self) -> bool {
195        self.sources
196            .iter()
197            .any(|(src, _)| matches!(src, Source::RowIndexLeBytes(_) | Source::RowIndexByte(_)))
198    }
199
200    pub fn has_request_idx_column(&self) -> bool {
201        self.sources
202            .iter()
203            .any(|(src, label)| matches!(src, Source::Column(_)) && *label == REQUEST_IDX_LABEL)
204    }
205
206    /// Per-spec only. `validate_bus_set` runs the
207    /// cross-endpoint check that closes label spoofing.
208    pub fn validate_clock_stitching(&self, _bus_id: &str) -> errors::Result<()> {
209        let waiver_status = self.clock_waiver.as_deref().map(WaiverStatus::classify);
210
211        let has_clock_marker = self.has_real_clock_source() || self.has_request_idx_column();
212
213        match (self.kind, has_clock_marker, waiver_status) {
214            (BusKind::Lookup, _, Some(_)) => Err(errors::Error::Protocol {
215                protocol: "logup_bus",
216                message: "lookup bus carries a clock_waiver; waivers only apply \
217                          to Permutation kind, drop the .with_clock_waiver(...) call",
218            }),
219            (BusKind::Permutation, true, Some(_)) => Err(errors::Error::Protocol {
220                protocol: "logup_bus",
221                message: "permutation bus carries both a clock source and a \
222                          clock_waiver; pick one shape",
223            }),
224            (BusKind::Permutation, false, Some(WaiverStatus::Empty)) => {
225                Err(errors::Error::Protocol {
226                    protocol: "logup_bus",
227                    message: "permutation bus has an empty clock_waiver; provide a \
228                              non-empty reason citing the load-bearing AIR constraint",
229                })
230            }
231            (BusKind::Permutation, false, Some(WaiverStatus::TooShort)) => {
232                Err(errors::Error::Protocol {
233                    protocol: "logup_bus",
234                    message: "permutation bus has an under-specified clock_waiver; \
235                              the reason must be at least 32 chars and cite a file/line \
236                              of the load-bearing AIR constraint",
237                })
238            }
239            (BusKind::Permutation, false, Some(WaiverStatus::MissingCitation)) => {
240                Err(errors::Error::Protocol {
241                    protocol: "logup_bus",
242                    message: "permutation bus clock_waiver lacks a 'see <path>' citation; \
243                              waiver text must start with 'see ' followed by the file path \
244                              of the load-bearing AIR constraint",
245                })
246            }
247            (BusKind::Permutation, false, None) => Err(errors::Error::Protocol {
248                protocol: "logup_bus",
249                message: "permutation bus lacks per-row clock stitching; add \
250                          Source::RowIndexLeBytes, pair both endpoints with a \
251                          committed B32 column labelled REQUEST_IDX_LABEL whose \
252                          value matches the partner row index, switch to \
253                          BusKind::Lookup via new_lookup, or document the \
254                          carve-out via .with_clock_waiver(reason)",
255            }),
256            _ => Ok(()),
257        }
258    }
259}
260
261#[derive(Clone, Copy, Debug, PartialEq, Eq)]
262enum WaiverStatus {
263    Empty,
264    TooShort,
265    MissingCitation,
266    Ok,
267}
268
269impl WaiverStatus {
270    const MIN_WAIVER_LEN: usize = 32;
271    const REQUIRED_PREFIX: &'static str = "see ";
272
273    fn classify(s: &str) -> Self {
274        if s.is_empty() {
275            Self::Empty
276        } else if s.len() < Self::MIN_WAIVER_LEN {
277            Self::TooShort
278        } else if !s.starts_with(Self::REQUIRED_PREFIX) {
279            Self::MissingCitation
280        } else {
281            Self::Ok
282        }
283    }
284}
285
286/// Every multi-endpoint `Permutation` `bus_id`
287/// must have at least one endpoint owning a real
288/// `RowIndexLeBytes`/`RowIndexByte` clock;
289/// otherwise label-only stitching admits
290/// char-2 parity collapse.
291pub fn validate_bus_set<'a, I>(endpoints: I) -> errors::Result<()>
292where
293    I: IntoIterator<Item = (&'a str, &'a PermutationCheckSpec)>,
294{
295    let mut by_bus: BTreeMap<&'a str, Vec<&'a PermutationCheckSpec>> = BTreeMap::new();
296
297    for (bus_id, spec) in endpoints {
298        by_bus.entry(bus_id).or_default().push(spec);
299    }
300
301    for (bus_id, specs) in &by_bus {
302        let any_lookup = specs.iter().any(|s| s.kind == BusKind::Lookup);
303        let any_perm = specs.iter().any(|s| s.kind == BusKind::Permutation);
304
305        if any_lookup && any_perm {
306            return Err(errors::Error::Protocol {
307                protocol: "logup_bus",
308                message: "bus_id has mixed BusKind across endpoints; \
309                          all endpoints must agree on Permutation or Lookup",
310            });
311        }
312
313        if any_lookup {
314            continue;
315        }
316
317        if specs.len() < 2 {
318            continue;
319        }
320
321        let any_real_clock = specs.iter().any(|s| s.has_real_clock_source());
322        let all_waivered = specs.iter().all(|s| s.clock_waiver.is_some());
323
324        if !any_real_clock && !all_waivered {
325            let _ = bus_id;
326            return Err(errors::Error::Protocol {
327                protocol: "logup_bus",
328                message: "permutation bus_id has no endpoint owning a real \
329                          Source::RowIndexLeBytes/RowIndexByte clock and not all \
330                          endpoints declare a clock_waiver; label-only stitching \
331                          is forgeable and admits char-2 parity collapse",
332            });
333        }
334    }
335
336    Ok(())
337}
338
339/// Folds `table_rows` into `heights` for each
340/// `Lookup`-kind spec, taking the running max.
341/// Used to derive the per-bus `N_max` absorbed
342/// into the transcript before `r_bus` is drawn.
343pub fn accumulate_lookup_heights(
344    specs: &[(String, PermutationCheckSpec)],
345    table_rows: u64,
346    heights: &mut BTreeMap<String, u64>,
347) {
348    for (bus_id, spec) in specs {
349        if spec.kind == BusKind::Lookup {
350            let entry = heights.entry(bus_id.clone()).or_insert(0);
351            *entry = (*entry).max(table_rows);
352        }
353    }
354}
355
356#[cfg(test)]
357mod tests {
358    use super::*;
359
360    #[test]
361    fn permutation_spec_creation() {
362        let sources = vec![
363            (Source::Column(0), b"kappa_0" as ChallengeLabel),
364            (Source::Column(1), b"kappa_1" as ChallengeLabel),
365            (Source::RowIndexLeBytes(4), b"kappa_clk" as ChallengeLabel),
366        ];
367
368        let spec = PermutationCheckSpec::new(sources, Some(2));
369
370        assert_eq!(spec.num_sources(), 3);
371        assert!(spec.has_selector());
372        assert_eq!(spec.selector, Some(2));
373    }
374
375    #[test]
376    fn source_variants() {
377        let col = Source::Column(5);
378        let cols = Source::Columns(vec![0, 1, 2, 3]);
379        let clock = Source::RowIndexLeBytes(4);
380        let constant = Source::Const(0x01);
381
382        assert_eq!(col, Source::Column(5));
383        assert_eq!(cols, Source::Columns(vec![0, 1, 2, 3]));
384        assert_eq!(clock, Source::RowIndexLeBytes(4));
385        assert_eq!(constant, Source::Const(0x01));
386    }
387
388    #[test]
389    fn new_paired_populates_both_selectors() {
390        let spec = PermutationCheckSpec::new_paired(
391            vec![(Source::Column(0), b"k_a" as ChallengeLabel)],
392            3,
393            5,
394            BusKind::Permutation,
395        );
396
397        assert!(spec.has_selector());
398        assert!(spec.has_paired());
399        assert_eq!(spec.selector, Some(3));
400        assert_eq!(spec.recv_selector, Some(5));
401        assert_eq!(spec.kind, BusKind::Permutation);
402    }
403
404    #[test]
405    fn new_defaults_recv_selector_none() {
406        let spec =
407            PermutationCheckSpec::new(vec![(Source::Column(0), b"k_a" as ChallengeLabel)], Some(1));
408
409        assert!(!spec.has_paired());
410        assert_eq!(spec.recv_selector, None);
411    }
412
413    #[test]
414    fn new_lookup_defaults_recv_selector_none() {
415        let spec = PermutationCheckSpec::new_lookup(
416            vec![(Source::Column(0), b"k_a" as ChallengeLabel)],
417            Some(1),
418        );
419
420        assert!(!spec.has_paired());
421        assert_eq!(spec.recv_selector, None);
422    }
423
424    #[test]
425    fn shift_column_indices_covers_recv_selector() {
426        let mut spec = PermutationCheckSpec::new_paired(
427            vec![
428                (Source::Column(0), b"k_a" as ChallengeLabel),
429                (Source::Columns(vec![1, 2]), b"k_b" as ChallengeLabel),
430            ],
431            3,
432            5,
433            BusKind::Lookup,
434        );
435
436        spec.shift_column_indices(10);
437
438        assert_eq!(spec.selector, Some(13));
439        assert_eq!(spec.recv_selector, Some(15));
440
441        match &spec.sources[0].0 {
442            Source::Column(idx) => assert_eq!(*idx, 10),
443            other => panic!("expected Column, got {other:?}"),
444        }
445
446        match &spec.sources[1].0 {
447            Source::Columns(idxs) => assert_eq!(idxs, &vec![11, 12]),
448            other => panic!("expected Columns, got {other:?}"),
449        }
450    }
451}