1use 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
39pub 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 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 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 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 #[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
239trait 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
287pub 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 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 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 pub fn external_buses(&self) -> Vec<(String, PermutationCheckSpec)> {
346 self.external_buses.clone()
347 }
348
349 pub fn len(&self) -> usize {
351 self.chiplets.len()
352 }
353
354 pub fn is_empty(&self) -> bool {
356 self.chiplets.is_empty()
357 }
358
359 pub fn name(&self) -> &str {
361 &self.name
362 }
363}
364
365pub 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 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 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 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
433pub 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
469pub 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
481pub 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
526fn 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
552fn 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
573pub 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}