Skip to main content

hekate_program/
chiplet.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
18//! Independent AIR Chiplet definitions.
19//!
20//! A `ChipletDef` snapshots a chiplet's full AIR
21//! (constraints, layout, bus specs) into an owned struct.
22//! The prover runs an independent ZeroCheck per chiplet.
23//! The bus (GPA) reconnects chiplets to the main trace.
24
25use crate::constraint::{
26    BoundaryConstraint, BoundaryTarget, ConstraintAst, ConstraintExpr, ExprId,
27};
28use crate::expander::VirtualExpander;
29use crate::permutation::PermutationCheckSpec;
30use crate::{Air, FixedColumn, ProgramCell, validate_fixed_columns};
31use alloc::boxed::Box;
32use alloc::string::String;
33use alloc::vec::Vec;
34use hekate_core::errors;
35use hekate_core::poly::PolyVariant;
36use hekate_core::trace::{ColumnTrace, ColumnType, Trace, TraceCompatibleField};
37use hekate_math::{Flat, HardwareField, PackableField, TowerField};
38
39/// Pre-computed chiplet AIR definition.
40pub struct ChipletDef<F: TowerField> {
41    name: String,
42    num_columns: usize,
43    constraint_ast: ConstraintAst<F>,
44    column_layout: Vec<ColumnType>,
45    virtual_column_layout: Vec<ColumnType>,
46    boundary_constraints: Vec<BoundaryConstraint<F>>,
47    fixed_columns: Vec<FixedColumn<F>>,
48    expander: Option<VirtualExpander>,
49    pub permutation_checks: Vec<(String, PermutationCheckSpec)>,
50}
51
52impl<F: TowerField> ChipletDef<F> {
53    /// Snapshot a chiplet's full AIR definition.
54    /// Call once at setup; the source chiplet can be dropped after.
55    pub fn from_air<P: Air<F> + Send + 'static>(p: &P) -> errors::Result<Self>
56    where
57        F: TraceCompatibleField + PackableField + HardwareField + 'static,
58        <F as PackableField>::Packed: Copy + Send + Sync,
59    {
60        let permutation_checks = p.permutation_checks();
61        for (bus_id, spec) in &permutation_checks {
62            spec.validate_clock_stitching(bus_id)?;
63        }
64
65        let constraint_ast = p.constraint_ast();
66        let boundary_constraints = p.boundary_constraints();
67        let fixed_columns = p.fixed_columns();
68
69        validate_paired_bus_mutex(&permutation_checks, &constraint_ast)?;
70        validate_chiplet_boundaries(&boundary_constraints, p.num_columns())?;
71        validate_fixed_columns(&fixed_columns, p.virtual_column_layout(), None)?;
72        validate_expander_coverage(p.virtual_expander(), p.column_layout())?;
73
74        Ok(Self {
75            name: p.name(),
76            num_columns: p.num_columns(),
77            constraint_ast,
78            column_layout: p.column_layout().to_vec(),
79            virtual_column_layout: p.virtual_column_layout().to_vec(),
80            boundary_constraints,
81            fixed_columns,
82            expander: p.virtual_expander().cloned(),
83            permutation_checks,
84        })
85    }
86
87    /// Prefixes internal bus_ids with a namespace.
88    /// Bus_ids listed in `exempt` are left unchanged.
89    pub fn prefix_bus_ids(&mut self, prefix: &str, exempt: &[String]) {
90        for (bus_id, _) in &mut self.permutation_checks {
91            if !exempt.contains(bus_id) {
92                let mut prefixed = String::from(prefix);
93                prefixed.push_str("::");
94                prefixed.push_str(bus_id);
95
96                *bus_id = prefixed;
97            }
98        }
99    }
100
101    /// Expand physical ColumnTrace into virtual PolyVariants.
102    /// Uses embedded expander if present, else 1:1 mapping.
103    pub fn expand_variants<'a>(
104        &self,
105        trace: &'a ColumnTrace,
106    ) -> errors::Result<Vec<PolyVariant<'a, F>>>
107    where
108        F: TraceCompatibleField + 'static,
109    {
110        match &self.expander {
111            Some(e) => e.expand_variants(trace, 0),
112            None => trace.get_poly_variants::<F>(),
113        }
114    }
115
116    /// Reconstruct from deserialized wire data.
117    /// Validates every embedded `PermutationCheckSpec`.
118    #[allow(clippy::too_many_arguments)]
119    pub fn from_wire(
120        name: String,
121        num_columns: usize,
122        constraint_ast: ConstraintAst<F>,
123        column_layout: Vec<ColumnType>,
124        virtual_column_layout: Vec<ColumnType>,
125        boundary_constraints: Vec<BoundaryConstraint<F>>,
126        fixed_columns: Vec<FixedColumn<F>>,
127        expander: Option<VirtualExpander>,
128        permutation_checks: Vec<(String, PermutationCheckSpec)>,
129    ) -> errors::Result<Self> {
130        for (bus_id, spec) in &permutation_checks {
131            spec.validate_clock_stitching(bus_id)?;
132        }
133
134        validate_paired_bus_mutex(&permutation_checks, &constraint_ast)?;
135        validate_chiplet_boundaries(&boundary_constraints, num_columns)?;
136
137        let virt_layout = match &expander {
138            Some(e) => e.virtual_layout(),
139            None => virtual_column_layout.as_slice(),
140        };
141
142        validate_fixed_columns(&fixed_columns, virt_layout, None)?;
143
144        Ok(Self {
145            name,
146            num_columns,
147            constraint_ast,
148            column_layout,
149            virtual_column_layout,
150            boundary_constraints,
151            fixed_columns,
152            expander,
153            permutation_checks,
154        })
155    }
156}
157
158impl<F: TowerField> Clone for ChipletDef<F> {
159    fn clone(&self) -> Self {
160        Self {
161            name: self.name.clone(),
162            num_columns: self.num_columns,
163            constraint_ast: self.constraint_ast.clone(),
164            column_layout: self.column_layout.clone(),
165            virtual_column_layout: self.virtual_column_layout.clone(),
166            boundary_constraints: self.boundary_constraints.clone(),
167            fixed_columns: self.fixed_columns.clone(),
168            expander: self.expander.clone(),
169            permutation_checks: self.permutation_checks.clone(),
170        }
171    }
172}
173
174impl<F: TowerField> Air<F> for ChipletDef<F> {
175    fn name(&self) -> String {
176        self.name.clone()
177    }
178
179    fn num_columns(&self) -> usize {
180        self.num_columns
181    }
182
183    fn boundary_constraints(&self) -> Vec<BoundaryConstraint<F>> {
184        self.boundary_constraints.clone()
185    }
186
187    fn column_layout(&self) -> &[ColumnType] {
188        &self.column_layout
189    }
190
191    fn virtual_column_layout(&self) -> &[ColumnType] {
192        match &self.expander {
193            Some(e) => e.virtual_layout(),
194            None => &self.virtual_column_layout,
195        }
196    }
197
198    fn permutation_checks(&self) -> Vec<(String, PermutationCheckSpec)> {
199        self.permutation_checks.clone()
200    }
201
202    fn fixed_columns(&self) -> Vec<FixedColumn<F>> {
203        self.fixed_columns.clone()
204    }
205
206    fn virtual_expander(&self) -> Option<&VirtualExpander> {
207        self.expander.as_ref()
208    }
209
210    fn parse_virtual_row(&self, bytes: &[u8], res: &mut Vec<Flat<F>>)
211    where
212        F: TraceCompatibleField,
213    {
214        if let Some(e) = &self.expander {
215            res.clear();
216
217            e.parse_row(bytes, res)
218                .expect("committed row byte length must match physical_row_bytes");
219            return;
220        }
221
222        res.clear();
223
224        let mut offset = 0;
225        for col_type in &self.column_layout {
226            let size = col_type.byte_size();
227            if offset + size <= bytes.len() {
228                res.push(col_type.parse_from_bytes(&bytes[offset..offset + size]));
229                offset += size;
230            }
231        }
232    }
233
234    fn constraint_ast(&self) -> ConstraintAst<F> {
235        self.constraint_ast.clone()
236    }
237}
238
239// =================================================================
240// Composite Chiplet Composition
241// =================================================================
242
243/// Factory trait for deterministic ChipletDef construction.
244trait AirFactory<F: TowerField>: Send + Sync {
245    fn build(&self) -> errors::Result<ChipletDef<F>>;
246    fn permutation_checks(&self) -> Vec<(String, PermutationCheckSpec)>;
247    fn clone_box(&self) -> Box<dyn AirFactory<F>>;
248}
249
250impl<F, A> AirFactory<F> for A
251where
252    F: TowerField + TraceCompatibleField + PackableField + HardwareField + 'static,
253    <F as PackableField>::Packed: Copy + Send + Sync,
254    A: Air<F> + Clone + Send + Sync + 'static,
255{
256    fn build(&self) -> errors::Result<ChipletDef<F>> {
257        ChipletDef::from_air(self)
258    }
259
260    fn permutation_checks(&self) -> Vec<(String, PermutationCheckSpec)> {
261        Air::permutation_checks(self)
262    }
263
264    fn clone_box(&self) -> Box<dyn AirFactory<F>> {
265        Box::new(self.clone())
266    }
267}
268
269impl<F: TowerField> Clone for Box<dyn AirFactory<F>> {
270    fn clone(&self) -> Self {
271        self.clone_box()
272    }
273}
274
275struct CompositeEntry<F: TraceCompatibleField> {
276    air: Box<dyn AirFactory<F>>,
277}
278
279impl<F: TraceCompatibleField> Clone for CompositeEntry<F> {
280    fn clone(&self) -> Self {
281        Self {
282            air: self.air.clone_box(),
283        }
284    }
285}
286
287/// Build-time composition of peer
288/// chiplets into a single unit.
289///
290/// Flattens into standard `ChipletDef` entries
291/// for the prover, no protocol-level awareness
292/// of hierarchy. Internal buses are namespaced
293/// with `"{name}::"` to prevent cross-composite
294/// collisions. External buses pass through
295/// unchanged.
296///
297/// All chiplets within a composite are peers, no mandatory root.
298pub struct CompositeChiplet<F: TraceCompatibleField> {
299    name: String,
300    chiplets: Vec<CompositeEntry<F>>,
301    external_bus_ids: Vec<String>,
302    external_buses: Vec<(String, PermutationCheckSpec)>,
303}
304
305impl<F: TraceCompatibleField> Clone for CompositeChiplet<F> {
306    fn clone(&self) -> Self {
307        Self {
308            name: self.name.clone(),
309            chiplets: self.chiplets.clone(),
310            external_bus_ids: self.external_bus_ids.clone(),
311            external_buses: self.external_buses.clone(),
312        }
313    }
314}
315
316impl<F: TraceCompatibleField> CompositeChiplet<F> {
317    /// Start building a composite
318    /// with the given namespace.
319    pub fn builder(name: &str) -> CompositeChipletBuilder<F> {
320        CompositeChipletBuilder {
321            name: String::from(name),
322            chiplets: Vec::new(),
323            external_bus_ids: Vec::new(),
324            external_buses: Vec::new(),
325        }
326    }
327
328    /// Produce fresh ChipletDefs for `Program::chiplet_defs()`.
329    pub fn flatten_defs(&self) -> errors::Result<Vec<ChipletDef<F>>> {
330        let mut out = Vec::with_capacity(self.chiplets.len());
331        for entry in &self.chiplets {
332            let mut def = entry.air.build()?;
333            def.prefix_bus_ids(&self.name, &self.external_bus_ids);
334
335            out.push(def);
336        }
337
338        Ok(out)
339    }
340
341    /// External buses for `Program::permutation_checks()`.
342    ///
343    /// These are main-trace-side specs, column indices
344    /// reference the main trace, not any chiplet trace.
345    pub fn external_buses(&self) -> Vec<(String, PermutationCheckSpec)> {
346        self.external_buses.clone()
347    }
348
349    /// Number of flattened chiplets in this composite.
350    pub fn len(&self) -> usize {
351        self.chiplets.len()
352    }
353
354    /// Returns true if this composite contains no chiplets.
355    pub fn is_empty(&self) -> bool {
356        self.chiplets.is_empty()
357    }
358
359    /// The composite's namespace.
360    pub fn name(&self) -> &str {
361        &self.name
362    }
363}
364
365/// Builder for `CompositeChiplet`.
366pub struct CompositeChipletBuilder<F: TraceCompatibleField> {
367    name: String,
368    chiplets: Vec<CompositeEntry<F>>,
369    external_bus_ids: Vec<String>,
370    external_buses: Vec<(String, PermutationCheckSpec)>,
371}
372
373impl<F: TraceCompatibleField> CompositeChipletBuilder<F> {
374    /// Add a sub-chiplet.
375    pub fn chiplet<A>(mut self, air: A) -> Self
376    where
377        A: Air<F> + Clone + Send + Sync + 'static,
378        F: TraceCompatibleField + PackableField + HardwareField + 'static,
379        <F as PackableField>::Packed: Copy + Send + Sync,
380    {
381        self.chiplets.push(CompositeEntry { air: Box::new(air) });
382
383        self
384    }
385
386    /// Declare an external bus (connects to the main trace).
387    pub fn external_bus(mut self, bus_id: &str, spec: PermutationCheckSpec) -> Self {
388        self.external_bus_ids.push(String::from(bus_id));
389        self.external_buses.push((String::from(bus_id), spec));
390
391        self
392    }
393
394    /// Finalize the composite.
395    ///
396    /// Validates selector orthogonality:
397    /// two specs on different bus_ids must not share a selector column
398    /// index. Same bus_id is exempt for dual-spec intra-table check.
399    pub fn build(self) -> errors::Result<CompositeChiplet<F>> {
400        for (bus_id, spec) in &self.external_buses {
401            spec.validate_clock_stitching(bus_id)?;
402        }
403
404        for entry in &self.chiplets {
405            let checks = entry.air.permutation_checks();
406            for i in 0..checks.len() {
407                for j in (i + 1)..checks.len() {
408                    if checks[i].0 == checks[j].0 {
409                        continue;
410                    }
411
412                    if let (Some(sel_i), Some(sel_j)) = (checks[i].1.selector, checks[j].1.selector)
413                        && sel_i == sel_j
414                    {
415                        return Err(errors::Error::Protocol {
416                            protocol: "composite_chiplet",
417                            message: "different bus_ids share a selector column",
418                        });
419                    }
420                }
421            }
422        }
423
424        Ok(CompositeChiplet {
425            name: self.name,
426            chiplets: self.chiplets,
427            external_bus_ids: self.external_bus_ids,
428            external_buses: self.external_buses,
429        })
430    }
431}
432
433// =================================================================
434// Multi-Composite Helpers
435// =================================================================
436
437/// Flatten multiple composites into a single chiplet def list.
438///
439/// Validates that no two composites share the same name
440/// (would cause bus namespace collisions).
441pub fn compose_chiplet_defs<F: TraceCompatibleField>(
442    composites: &[&CompositeChiplet<F>],
443) -> errors::Result<Vec<ChipletDef<F>>> {
444    for i in 0..composites.len() {
445        for j in (i + 1)..composites.len() {
446            if composites[i].name == composites[j].name {
447                return Err(errors::Error::Protocol {
448                    protocol: "composite_chiplet",
449                    message: "duplicate composite name in compose_chiplet_defs",
450                });
451            }
452        }
453    }
454
455    let mut defs = Vec::new();
456    for composite in composites {
457        defs.extend(composite.flatten_defs()?);
458    }
459
460    let endpoints = defs
461        .iter()
462        .flat_map(|d| d.permutation_checks.iter().map(|(id, s)| (id.as_str(), s)));
463
464    crate::permutation::validate_bus_set(endpoints)?;
465
466    Ok(defs)
467}
468
469/// Collect external buses from multiple composites.
470pub fn compose_external_buses<F: TraceCompatibleField>(
471    composites: &[&CompositeChiplet<F>],
472) -> Vec<(String, PermutationCheckSpec)> {
473    let mut buses = Vec::new();
474    for composite in composites {
475        buses.extend(composite.external_buses());
476    }
477
478    buses
479}
480
481/// Without the mutex root, both selectors high collapse
482/// the bus numerator to zero in char-2; without the
483/// boolean roots, the mutex admits non-zero field-element
484/// selectors that bypass binary on/off semantics.
485pub fn validate_paired_bus_mutex<F: TowerField>(
486    specs: &[(String, PermutationCheckSpec)],
487    ast: &ConstraintAst<F>,
488) -> errors::Result<()> {
489    for (_bus_id, spec) in specs {
490        let (s_send, s_recv) = match (spec.selector, spec.recv_selector) {
491            (Some(send), Some(recv)) => (send, recv),
492            (None, Some(_)) => {
493                return Err(errors::Error::Protocol {
494                    protocol: "logup_bus",
495                    message: "paired bus has recv_selector without send selector",
496                });
497            }
498            _ => continue,
499        };
500
501        if !ast_contains_mutex_root(ast, s_send, s_recv) {
502            return Err(errors::Error::Protocol {
503                protocol: "logup_bus",
504                message: "paired bus requires `s_send · s_recv = 0` mutex root in the AST",
505            });
506        }
507
508        if !ast_contains_boolean_root(ast, s_send) {
509            return Err(errors::Error::Protocol {
510                protocol: "logup_bus",
511                message: "paired bus requires boolean-assertion root for s_send",
512            });
513        }
514
515        if !ast_contains_boolean_root(ast, s_recv) {
516            return Err(errors::Error::Protocol {
517                protocol: "logup_bus",
518                message: "paired bus requires boolean-assertion root for s_recv",
519            });
520        }
521    }
522
523    Ok(())
524}
525
526/// Chiplets carry no `public_inputs`; a `PublicInput`
527/// boundary target is unsatisfiable; reject it at
528/// snapshot time. Also rejects out-of-range `col_idx`.
529fn validate_chiplet_boundaries<F>(
530    boundaries: &[BoundaryConstraint<F>],
531    num_columns: usize,
532) -> errors::Result<()> {
533    for bc in boundaries {
534        if bc.col_idx >= num_columns {
535            return Err(errors::Error::Protocol {
536                protocol: "boundary",
537                message: "chiplet boundary col_idx out of range",
538            });
539        }
540
541        if matches!(bc.target, BoundaryTarget::PublicInput(_)) {
542            return Err(errors::Error::Protocol {
543                protocol: "boundary",
544                message: "chiplet boundaries must use BoundaryTarget::Constant",
545            });
546        }
547    }
548
549    Ok(())
550}
551
552/// Physical columns outside every expansion entry enter
553/// no master fold; nothing binds their committed cells.
554fn validate_expander_coverage(
555    expander: Option<&VirtualExpander>,
556    layout: &[ColumnType],
557) -> errors::Result<()> {
558    let covered = match expander {
559        Some(e) => e.num_physical_columns(),
560        None => layout.len(),
561    };
562
563    if covered != layout.len() {
564        return Err(errors::Error::Protocol {
565            protocol: "chiplet",
566            message: "virtual_expander does not tile column_layout",
567        });
568    }
569
570    Ok(())
571}
572
573/// Non-paired `Bit` selectors with no direct `s·s + s` boolean root,
574/// each tagged with the declaring `bus_id`. Advisory only:
575/// booleanness can hold indirectly (one-hot, disjoint products),
576/// callers warn rather than reject.
577pub fn unconstrained_bit_selectors<'a, F: TowerField>(
578    specs: &'a [(String, PermutationCheckSpec)],
579    ast: &ConstraintAst<F>,
580    virtual_layout: &[ColumnType],
581) -> Vec<(usize, &'a str)> {
582    let mut flagged: Vec<(usize, &str)> = Vec::new();
583    for (bus_id, spec) in specs {
584        if spec.recv_selector.is_some() {
585            continue;
586        }
587
588        let Some(sel) = spec.selector else {
589            continue;
590        };
591
592        if virtual_layout.get(sel) != Some(&ColumnType::Bit) {
593            continue;
594        }
595
596        if !ast_contains_boolean_root(ast, sel) && !flagged.iter().any(|(s, _)| *s == sel) {
597            flagged.push((sel, bus_id.as_str()));
598        }
599    }
600
601    flagged
602}
603
604fn ast_contains_mutex_root<F: TowerField>(
605    ast: &ConstraintAst<F>,
606    s_send: usize,
607    s_recv: usize,
608) -> bool {
609    ast.roots
610        .iter()
611        .any(|root| is_mutex_product(ast, *root, s_send, s_recv))
612}
613
614fn ast_contains_boolean_root<F: TowerField>(ast: &ConstraintAst<F>, col: usize) -> bool {
615    ast.roots
616        .iter()
617        .any(|root| is_boolean_assertion(ast, *root, col))
618}
619
620fn is_boolean_assertion<F: TowerField>(ast: &ConstraintAst<F>, id: ExprId, col: usize) -> bool {
621    let ConstraintExpr::Add(a, b) = ast.arena.get(id) else {
622        return false;
623    };
624
625    matches_boolean_pair(ast, *a, *b, col) || matches_boolean_pair(ast, *b, *a, col)
626}
627
628fn matches_boolean_pair<F: TowerField>(
629    ast: &ConstraintAst<F>,
630    sq_id: ExprId,
631    cell_id: ExprId,
632    col: usize,
633) -> bool {
634    let ConstraintExpr::Mul(x, y) = ast.arena.get(sq_id) else {
635        return false;
636    };
637
638    current_col_idx(ast, *x) == Some(col)
639        && current_col_idx(ast, *y) == Some(col)
640        && current_col_idx(ast, cell_id) == Some(col)
641}
642
643fn is_mutex_product<F: TowerField>(
644    ast: &ConstraintAst<F>,
645    id: ExprId,
646    s_send: usize,
647    s_recv: usize,
648) -> bool {
649    let ConstraintExpr::Mul(a, b) = ast.arena.get(id) else {
650        return false;
651    };
652
653    let lhs = current_col_idx(ast, *a);
654    let rhs = current_col_idx(ast, *b);
655
656    matches!(
657        (lhs, rhs),
658        (Some(x), Some(y)) if (x == s_send && y == s_recv) || (x == s_recv && y == s_send)
659    )
660}
661
662fn current_col_idx<F: TowerField>(ast: &ConstraintAst<F>, id: ExprId) -> Option<usize> {
663    match ast.arena.get(id) {
664        ConstraintExpr::Cell(ProgramCell {
665            col_idx,
666            next_row: false,
667        }) => Some(*col_idx),
668        _ => None,
669    }
670}
671
672#[cfg(test)]
673mod tests {
674    use super::*;
675    use crate::ConstraintAst;
676    use crate::constraint::builder::ConstraintSystem;
677    use crate::define_columns;
678    use crate::permutation::{BusKind, ChallengeLabel, PermutationCheckSpec, Source};
679    use alloc::string::String;
680    use alloc::vec;
681    use hekate_core::trace::ColumnType;
682    use hekate_math::Block128;
683
684    type F = Block128;
685
686    define_columns! {
687        PairedAirCols {
688            KEY: B32,
689            S_SEND: Bit,
690            S_RECV: Bit,
691        }
692    }
693
694    #[derive(Clone)]
695    struct ExpanderAir {
696        expander: VirtualExpander,
697    }
698
699    impl Air<F> for ExpanderAir {
700        fn num_columns(&self) -> usize {
701            self.expander.virtual_layout().len()
702        }
703
704        fn column_layout(&self) -> &[ColumnType] {
705            &[ColumnType::B32, ColumnType::Bit]
706        }
707
708        fn virtual_expander(&self) -> Option<&VirtualExpander> {
709            Some(&self.expander)
710        }
711
712        fn constraint_ast(&self) -> ConstraintAst<F> {
713            ConstraintSystem::<F>::new().build()
714        }
715    }
716
717    #[derive(Clone)]
718    struct OneBusAir {
719        spec: PermutationCheckSpec,
720    }
721
722    impl Air<F> for OneBusAir {
723        fn num_columns(&self) -> usize {
724            2
725        }
726
727        fn column_layout(&self) -> &[ColumnType] {
728            &[ColumnType::B32, ColumnType::Bit]
729        }
730
731        fn permutation_checks(&self) -> Vec<(String, PermutationCheckSpec)> {
732            vec![("test_bus".into(), self.spec.clone())]
733        }
734
735        fn constraint_ast(&self) -> ConstraintAst<F> {
736            ConstraintSystem::<F>::new().build()
737        }
738    }
739
740    #[derive(Clone)]
741    struct PairedAir {
742        with_mutex: bool,
743    }
744
745    impl Air<F> for PairedAir {
746        fn num_columns(&self) -> usize {
747            PairedAirCols::NUM_COLUMNS
748        }
749
750        fn column_layout(&self) -> &[ColumnType] {
751            static LAYOUT: std::sync::OnceLock<Vec<ColumnType>> = std::sync::OnceLock::new();
752            LAYOUT.get_or_init(PairedAirCols::build_layout)
753        }
754
755        fn permutation_checks(&self) -> Vec<(String, PermutationCheckSpec)> {
756            let sources = vec![
757                (Source::Column(PairedAirCols::KEY), b"k_a" as ChallengeLabel),
758                (Source::RowIndexLeBytes(4), b"k_clk" as ChallengeLabel),
759            ];
760
761            vec![(
762                "paired_test_bus".into(),
763                PermutationCheckSpec::new_paired(
764                    sources,
765                    PairedAirCols::S_SEND,
766                    PairedAirCols::S_RECV,
767                    BusKind::Permutation,
768                ),
769            )]
770        }
771
772        fn constraint_ast(&self) -> ConstraintAst<F> {
773            let cs = ConstraintSystem::<F>::new();
774
775            cs.assert_boolean(cs.col(PairedAirCols::S_SEND));
776            cs.assert_boolean(cs.col(PairedAirCols::S_RECV));
777
778            if self.with_mutex {
779                cs.constrain_named(
780                    "paired_bus_mutex",
781                    cs.col(PairedAirCols::S_SEND) * cs.col(PairedAirCols::S_RECV),
782                );
783            }
784
785            cs.build()
786        }
787    }
788
789    #[derive(Clone)]
790    struct PairedNoBoolAir;
791
792    impl Air<F> for PairedNoBoolAir {
793        fn num_columns(&self) -> usize {
794            PairedAirCols::NUM_COLUMNS
795        }
796
797        fn column_layout(&self) -> &[ColumnType] {
798            static LAYOUT: std::sync::OnceLock<Vec<ColumnType>> = std::sync::OnceLock::new();
799            LAYOUT.get_or_init(PairedAirCols::build_layout)
800        }
801
802        fn permutation_checks(&self) -> Vec<(String, PermutationCheckSpec)> {
803            let sources = vec![
804                (Source::Column(PairedAirCols::KEY), b"k_a" as ChallengeLabel),
805                (Source::RowIndexLeBytes(4), b"k_clk" as ChallengeLabel),
806            ];
807
808            vec![(
809                "paired_test_bus".into(),
810                PermutationCheckSpec::new_paired(
811                    sources,
812                    PairedAirCols::S_SEND,
813                    PairedAirCols::S_RECV,
814                    BusKind::Permutation,
815                ),
816            )]
817        }
818
819        fn constraint_ast(&self) -> ConstraintAst<F> {
820            let cs = ConstraintSystem::<F>::new();
821
822            cs.constrain_named(
823                "paired_bus_mutex",
824                cs.col(PairedAirCols::S_SEND) * cs.col(PairedAirCols::S_RECV),
825            );
826
827            cs.build()
828        }
829    }
830
831    fn key_only() -> Vec<(Source, ChallengeLabel)> {
832        vec![(Source::Column(0), b"k_a")]
833    }
834
835    fn key_with_clock() -> Vec<(Source, ChallengeLabel)> {
836        vec![
837            (Source::Column(0), b"k_a"),
838            (Source::RowIndexLeBytes(4), b"k_clk"),
839        ]
840    }
841
842    fn snapshot(spec: PermutationCheckSpec) -> errors::Result<ChipletDef<F>> {
843        ChipletDef::from_air(&OneBusAir { spec })
844    }
845
846    fn assert_logup_bus_err<T>(res: errors::Result<T>) {
847        match res {
848            Err(errors::Error::Protocol { protocol, .. }) => {
849                assert_eq!(protocol, "logup_bus");
850            }
851            Ok(_) => panic!("expected Err(Protocol {{ protocol: \"logup_bus\", .. }})"),
852            Err(other) => panic!("expected Err(Protocol), got {:?}", other),
853        }
854    }
855
856    #[test]
857    fn def_rejects_permutation_without_clock() {
858        let spec = PermutationCheckSpec::new(key_only(), Some(1));
859        assert_logup_bus_err(snapshot(spec));
860    }
861
862    #[test]
863    fn def_rejects_permutation_with_empty_waiver() {
864        let spec = PermutationCheckSpec::new(key_only(), Some(1)).with_clock_waiver("");
865        assert_logup_bus_err(snapshot(spec));
866    }
867
868    #[test]
869    fn def_rejects_permutation_with_clock_and_waiver() {
870        let spec =
871            PermutationCheckSpec::new(key_with_clock(), Some(1)).with_clock_waiver("redundant");
872        assert_logup_bus_err(snapshot(spec));
873    }
874
875    #[test]
876    fn def_rejects_lookup_with_waiver() {
877        let spec = PermutationCheckSpec::new_lookup(key_only(), Some(1)).with_clock_waiver("nope");
878        assert_logup_bus_err(snapshot(spec));
879    }
880
881    #[test]
882    fn def_accepts_permutation_with_row_index() {
883        let spec = PermutationCheckSpec::new(key_with_clock(), Some(1));
884        snapshot(spec).expect("permutation bus with row-index source must accept");
885    }
886
887    #[test]
888    fn def_accepts_permutation_with_clock_waiver() {
889        let spec = PermutationCheckSpec::new(key_only(), Some(1))
890            .with_clock_waiver("see foo.rs:42: structurally unique by AIR body");
891        snapshot(spec).expect("permutation bus with non-empty clock_waiver must accept");
892    }
893
894    #[test]
895    fn def_accepts_lookup_without_clock() {
896        let spec = PermutationCheckSpec::new_lookup(key_only(), Some(1));
897        snapshot(spec).expect("lookup bus without clock must accept");
898    }
899
900    #[test]
901    fn def_rejects_permutation_with_too_short_waiver() {
902        let spec = PermutationCheckSpec::new(key_only(), Some(1)).with_clock_waiver("see x.rs");
903        assert_logup_bus_err(snapshot(spec));
904    }
905
906    #[test]
907    fn def_rejects_permutation_with_missing_see_citation() {
908        let spec = PermutationCheckSpec::new(key_only(), Some(1))
909            .with_clock_waiver("structurally unique by AIR body but no file citation prefix here");
910        assert_logup_bus_err(snapshot(spec));
911    }
912
913    #[test]
914    fn paired_bus_emits_mutex_and_boolean_assertions() {
915        let cs = ConstraintSystem::<F>::new();
916
917        cs.assert_paired_bus_mutex(PairedAirCols::S_SEND, PairedAirCols::S_RECV);
918
919        let ast = cs.build();
920
921        let labels: Vec<_> = ast.labels.iter().filter_map(|l| *l).collect();
922
923        assert_eq!(
924            labels.iter().filter(|l| **l == "boolean").count(),
925            2,
926            "gadget must emit two boolean assertions"
927        );
928        assert_eq!(
929            labels.iter().filter(|l| **l == "paired_bus_mutex").count(),
930            1,
931            "gadget must emit exactly one mutex root"
932        );
933    }
934
935    #[test]
936    fn paired_bus_shares_cell_nodes() {
937        let cs = ConstraintSystem::<F>::new();
938
939        let send_first = cs.col(PairedAirCols::S_SEND);
940        let recv_first = cs.col(PairedAirCols::S_RECV);
941
942        cs.assert_paired_bus_mutex(PairedAirCols::S_SEND, PairedAirCols::S_RECV);
943
944        let send_again = cs.col(PairedAirCols::S_SEND);
945        let recv_again = cs.col(PairedAirCols::S_RECV);
946
947        assert_eq!(send_first.id, send_again.id, "S_SEND must dedup");
948        assert_eq!(recv_first.id, recv_again.id, "S_RECV must dedup");
949    }
950
951    #[test]
952    fn chiplet_def_rejects_paired_spec_without_mutex() {
953        let bad = PairedAir { with_mutex: false };
954        assert_logup_bus_err(ChipletDef::<F>::from_air(&bad));
955    }
956
957    #[test]
958    fn chiplet_def_accepts_paired_spec_with_mutex() {
959        let good = PairedAir { with_mutex: true };
960        ChipletDef::<F>::from_air(&good).expect("paired AIR with mutex must snapshot");
961    }
962
963    #[test]
964    fn chiplet_def_rejects_paired_spec_without_boolean_roots() {
965        assert_logup_bus_err(ChipletDef::<F>::from_air(&PairedNoBoolAir));
966    }
967
968    #[test]
969    fn chiplet_def_requires_expander_to_tile_the_layout() {
970        let tiled = ExpanderAir {
971            expander: VirtualExpander::new()
972                .expand_bits(1, ColumnType::B32)
973                .control_bits(1)
974                .build()
975                .unwrap(),
976        };
977
978        ChipletDef::<F>::from_air(&tiled).expect("tiling expander must snapshot");
979
980        let short = ExpanderAir {
981            expander: VirtualExpander::new()
982                .expand_bits(1, ColumnType::B32)
983                .build()
984                .unwrap(),
985        };
986
987        assert!(ChipletDef::<F>::from_air(&short).is_err());
988    }
989
990    #[test]
991    fn validator_rejects_recv_selector_without_send_selector() {
992        let spec = PermutationCheckSpec {
993            sources: vec![
994                (Source::Column(PairedAirCols::KEY), b"k_a" as ChallengeLabel),
995                (Source::RowIndexLeBytes(4), b"k_clk" as ChallengeLabel),
996            ],
997            selector: None,
998            recv_selector: Some(PairedAirCols::S_RECV),
999            kind: BusKind::Permutation,
1000            clock_waiver: None,
1001        };
1002
1003        let ast = ConstraintSystem::<F>::new().build();
1004
1005        assert_logup_bus_err(validate_paired_bus_mutex(
1006            &[("asym_bus".into(), spec)],
1007            &ast,
1008        ));
1009    }
1010
1011    #[test]
1012    fn flags_bit_selector_without_boolean_root() {
1013        let ast = ConstraintSystem::<F>::new().build();
1014        let layout = vec![ColumnType::B32, ColumnType::Bit];
1015        let specs = vec![(
1016            String::from("bus"),
1017            PermutationCheckSpec::new(vec![(Source::Column(0), b"k" as ChallengeLabel)], Some(1)),
1018        )];
1019
1020        assert_eq!(
1021            unconstrained_bit_selectors(&specs, &ast, &layout),
1022            vec![(1, "bus")]
1023        );
1024    }
1025
1026    #[test]
1027    fn boolean_root_clears_bit_selector() {
1028        let cs = ConstraintSystem::<F>::new();
1029        let sel = cs.col(1);
1030        cs.assert_boolean(sel);
1031        let ast = cs.build();
1032
1033        let layout = vec![ColumnType::B32, ColumnType::Bit];
1034        let specs = vec![(
1035            String::from("bus"),
1036            PermutationCheckSpec::new(vec![(Source::Column(0), b"k" as ChallengeLabel)], Some(1)),
1037        )];
1038
1039        assert!(unconstrained_bit_selectors(&specs, &ast, &layout).is_empty());
1040    }
1041}