p3_sumcheck/ring_switch/bits/
transcript.rs

1//! Fiat-Shamir transcript of one bit-alphabet ring-switching reduction.
2//!
3//! ```text
4//!     evaluation point   ->  one element per coordinate
5//!     tensor rows        ->  one element per row of the bit matrix
6//!     carry rows         ->  the same, only when the shape has successor rows
7//!     last rows          ->  the same, only when the shape has successor rows
8//!     batching point     ->  one element per absorbed coordinate, drawn
9//!     tensor batching    ->  one element, drawn, only when the shape has successor rows
10//!     sumcheck           ->  a bracket around a delegated run
11//!     surviving claim    ->  one element
12//! ```
13//!
14//! # What the order settles
15//!
16//! The batching draws come after every element's rows, and nothing else does.
17//! That is the ordering the reduction's soundness rests on, so it lives here.
18//!
19//! A bit matrix solving two `F_2`-linear systems moves the claim with the sum held.
20//! Drawing the challenge first would let a prover pick such a matrix.
21//!
22//! # What the shape binds
23//!
24//! A fingerprint of the description enters the sponge before any step runs.
25//! The coordinate count moves the first width, the level fixes the other two.
26//!
27//! The successor row count is bound as an instance label.
28//! It moves no width, yet it decides which successor the column check reads.
29//!
30//! No grinding step is described, so every challenge here is resampleable.
31
32use alloc::vec;
33use alloc::vec::Vec;
34use core::marker::PhantomData;
35
36use p3_binary_field::TowerLevel;
37use p3_challenger::fs::{
38    DomainSeparator, FieldToFieldCodec, FieldUnit, Hierarchy, Interaction, InteractionPattern,
39    Kind, Length, ProverState, TranscriptBound, TranscriptField, VerifierState,
40};
41use p3_challenger::{CanObserve, CanSample};
42use p3_multilinear_util::point::Point;
43
44use super::basis::Coefficients;
45use super::reduction::BitRingSwitch;
46
47/// Version byte bound into the seed, separating two revisions of this protocol.
48const VERSION: u8 = 1;
49
50/// Protocol name bound into the seed, distinct from the general reduction's.
51pub(crate) const NAME: &[u8] = b"p3-sumcheck-bit-ring-switch";
52
53/// Step label of the point the incoming evaluation claim is stated at.
54const EVALUATION_POINT: &str = "evaluation_point";
55
56/// Step label of the rows of the shared tensor element.
57const TENSOR_ROWS: &str = "tensor_rows";
58
59/// Step label of the rows of the element carrying the successor into the next element.
60const CARRY_ROWS: &str = "carry_rows";
61
62/// Step label of the rows of the element holding the repeating last row.
63const LAST_ROWS: &str = "last_rows";
64
65/// Step label of the challenges that collapse the row claims into one.
66const BATCHING_POINT: &str = "batching_point";
67
68/// Step label of the challenge that batches the successor elements with the tensor.
69const TENSOR_BATCHING: &str = "tensor_batching";
70
71/// Elements a successor view adds to the statement when its rows outrun one element.
72const SUCCESSOR_ELEMENTS: usize = 2;
73
74/// Step label of the bracket around the delegated sumcheck.
75const BATCHED_SUMCHECK: &str = "batched_sumcheck";
76
77/// Step label of the value the surviving claim carries.
78const SURVIVING_CLAIM: &str = "surviving_claim";
79
80/// Sponge alphabet of a challenger that speaks the level natively.
81type Alphabet<EF> = FieldUnit<EF>;
82
83/// Type-level name of the sub-protocol the reduction delegates its rounds to.
84struct BatchedSumcheck;
85
86/// Numbers that fix the transcript of one bit-alphabet reduction.
87///
88/// Both sides build this from their own configuration, never from a proof.
89#[derive(Clone, Copy, Debug, PartialEq, Eq)]
90pub struct BitRingSwitchShape {
91    /// Coordinates the incoming evaluation point names.
92    pub num_variables: usize,
93    /// Row coordinates of a successor view whose rows outrun one element.
94    ///
95    /// Set only when the reduction sends the two successor elements.
96    /// A successor view inside one element is a column reading, and plays the plain run.
97    pub successor_rows: Option<usize>,
98}
99
100impl BitRingSwitchShape {
101    /// Describe a reduction of a claim at a point of this width.
102    #[must_use]
103    pub const fn new(num_variables: usize) -> Self {
104        Self {
105            num_variables,
106            successor_rows: None,
107        }
108    }
109
110    /// Describe a reduction that also sends the two successor elements.
111    ///
112    /// For a successor view stepping within the trailing `row_variables` coordinates.
113    /// Only a view with more row coordinates than one element absorbs sends them.
114    #[must_use]
115    pub const fn with_successor_rows(num_variables: usize, row_variables: usize) -> Self {
116        Self {
117            num_variables,
118            successor_rows: Some(row_variables),
119        }
120    }
121
122    /// Maximum delegated rounds for this point width.
123    ///
124    /// A Boolean prefix of length `p` leaves `l' - p` rounds from this maximum `l'`.
125    ///
126    /// # Panics
127    ///
128    /// Panics when the point is narrower than one element.
129    #[must_use]
130    pub fn sumcheck_rounds<EF: TowerLevel>(&self) -> usize {
131        let absorbed = BitRingSwitch::<EF>::ABSORBED;
132        assert!(
133            self.num_variables >= absorbed,
134            "the evaluation point must name at least the {absorbed} absorbed coordinates"
135        );
136        self.num_variables - absorbed
137    }
138
139    /// Describe every step of one reduction, which one matched bracket always validates.
140    #[must_use]
141    pub fn pattern<EF: TranscriptField + TowerLevel>(&self) -> InteractionPattern {
142        let rows = |label| {
143            Interaction::algebra::<EF, EF>(
144                Hierarchy::Atomic,
145                Kind::Message,
146                label,
147                Length::Fixed(Coefficients::<EF>::DIMENSION),
148            )
149        };
150        let successor = self.successor_rows.is_some();
151
152        let mut steps = vec![
153            // The point comes first, so no later draw is chosen before the claim is placed.
154            Interaction::algebra::<EF, EF>(
155                Hierarchy::Atomic,
156                Kind::Message,
157                EVALUATION_POINT,
158                Length::Fixed(self.num_variables),
159            ),
160            // The rows are the whole element, one bit per entry.
161            // Binding them therefore binds both readings of it.
162            rows(TENSOR_ROWS),
163        ];
164        // The successor elements are bound beside the tensor, before any draw.
165        if successor {
166            steps.extend([rows(CARRY_ROWS), rows(LAST_ROWS)]);
167        }
168        // One challenge per absorbed coordinate collapses the rows into a single claim.
169        steps.push(Interaction::algebra::<EF, EF>(
170            Hierarchy::Atomic,
171            Kind::Challenge,
172            BATCHING_POINT,
173            Length::Fixed(BitRingSwitch::<EF>::ABSORBED),
174        ));
175        // One more challenge collapses the three elements' batched rows into one sum.
176        if successor {
177            steps.push(Interaction::algebra::<EF, EF>(
178                Hierarchy::Atomic,
179                Kind::Challenge,
180                TENSOR_BATCHING,
181                Length::Scalar,
182            ));
183        }
184        steps.extend([
185            // The bracket records that a sub-protocol runs here, under its own seed.
186            Interaction::marker::<BatchedSumcheck>(
187                Hierarchy::Begin,
188                Kind::Protocol,
189                BATCHED_SUMCHECK,
190            ),
191            Interaction::marker::<BatchedSumcheck>(
192                Hierarchy::End,
193                Kind::Protocol,
194                BATCHED_SUMCHECK,
195            ),
196            // The value left behind is bound before the sponge goes back.
197            // That is what ties whatever discharges it to this run.
198            Interaction::algebra::<EF, EF>(
199                Hierarchy::Atomic,
200                Kind::Message,
201                SURVIVING_CLAIM,
202                Length::Scalar,
203            ),
204        ]);
205
206        InteractionPattern::new(steps).expect("one matched bracket is always well formed")
207    }
208
209    /// Bind the protocol identity and this shape into a seed.
210    ///
211    /// The successor row count, when there is one, is an instance label.
212    /// A plain shape adds none, so its seed is the protocol's and the pattern's alone.
213    #[must_use]
214    pub fn domain_separator<EF: TranscriptField + TowerLevel>(
215        &self,
216    ) -> DomainSeparator<Alphabet<EF>> {
217        let mut separator = DomainSeparator::new(VERSION, NAME, self.pattern::<EF>());
218        if let Some(rows) = self.successor_rows {
219            separator.instance(&(rows as u64).to_be_bytes());
220        }
221        separator
222    }
223}
224
225/// Prover-side transcript of one bit-alphabet reduction.
226///
227/// The challenger is borrowed, because a reduction always runs inside something larger.
228pub struct BitRingSwitchProverTranscript<'a, C, EF: TranscriptField> {
229    /// Driver walking the description and holding the borrowed sponge.
230    state: ProverState<&'a mut C, Alphabet<EF>>,
231    /// The numbers this run was described with.
232    shape: BitRingSwitchShape,
233}
234
235impl<'a, C, EF> BitRingSwitchProverTranscript<'a, C, EF>
236where
237    EF: TranscriptField + TowerLevel,
238    C: CanObserve<EF> + CanSample<EF>,
239{
240    /// Seed the transcript from the shape, folding its fingerprint into the sponge.
241    pub fn new(challenger: &'a mut C, shape: BitRingSwitchShape) -> Self {
242        Self {
243            state: ProverState::new(challenger, &shape.domain_separator::<EF>()),
244            shape,
245        }
246    }
247
248    /// Bind the claim's point and every element's rows, then draw the batching challenges.
249    ///
250    /// # Arguments
251    ///
252    /// - The evaluation point of the claim.
253    /// - The rows of the tensor element.
254    /// - The rows of the carry and last elements, when the shape has successor rows.
255    ///
256    /// # Returns
257    ///
258    /// - The batching point, one challenge per absorbed coordinate.
259    /// - The challenge batching the three elements, when the shape has successor rows.
260    ///
261    /// # Panics
262    ///
263    /// - When the presence of the successor rows disagrees with the shape.
264    /// - When a list is not the width the run was described with.
265    pub fn statement(
266        &mut self,
267        point: &Point<EF>,
268        rows: &[EF],
269        successor: Option<(&[EF], &[EF])>,
270    ) -> (Point<EF>, Option<EF>) {
271        assert_eq!(
272            successor.is_some(),
273            self.shape.successor_rows.is_some(),
274            "the successor elements are sent exactly when the shape describes them",
275        );
276
277        // The point is bound first, so the element cannot be chosen to suit it.
278        self.state
279            .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(
280                EVALUATION_POINT,
281                point.as_slice(),
282            );
283        self.state
284            .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(TENSOR_ROWS, rows);
285        if let Some((carry, last)) = successor {
286            self.state
287                .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(CARRY_ROWS, carry);
288            self.state
289                .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(LAST_ROWS, last);
290        }
291
292        // Only now are the batching challenges drawn, so no message above them knew them.
293        let batching_point = Point::new(
294            self.state
295                .challenge_extensions::<EF, EF, FieldToFieldCodec<EF>>(
296                    BATCHING_POINT,
297                    BitRingSwitch::<EF>::ABSORBED,
298                )
299                .into_iter()
300                .map(TranscriptBound::into_inner)
301                .collect(),
302        );
303        let alpha = successor.map(|_| {
304            self.state
305                .challenge_extension::<EF, EF, FieldToFieldCodec<EF>>(TENSOR_BATCHING)
306                .into_inner()
307        });
308        (batching_point, alpha)
309    }
310
311    /// Hand the sponge to the delegated sumcheck rounds.
312    pub fn batched_sumcheck<R>(&mut self, run: impl FnOnce(&mut C) -> R) -> R {
313        self.state
314            .begin_protocol::<BatchedSumcheck>(BATCHED_SUMCHECK);
315        let output = run(self.state.challenger_mut());
316        self.state.end_protocol::<BatchedSumcheck>(BATCHED_SUMCHECK);
317        output
318    }
319
320    /// Bind the value the surviving claim carries.
321    pub fn surviving_claim(&mut self, value: EF) {
322        self.state
323            .observe_extension::<EF, EF, FieldToFieldCodec<EF>>(SURVIVING_CLAIM, &value);
324    }
325
326    /// Close the transcript, panicking unless every described step was played.
327    pub fn finish(self) {
328        assert!(
329            self.state.finalize().is_empty(),
330            "a bit-alphabet reduction carries every value in its own proof",
331        );
332    }
333}
334
335/// Verifier-side transcript of one bit-alphabet reduction.
336///
337/// Mirrors the prover side call for call, over the same description.
338pub struct BitRingSwitchVerifierTranscript<'a, C, EF: TranscriptField> {
339    /// Driver walking the description and holding the borrowed sponge.
340    state: VerifierState<'static, &'a mut C, Alphabet<EF>>,
341    /// The numbers this run was described with.
342    shape: BitRingSwitchShape,
343    /// Marker keeping the level out of the driver's own signature.
344    _level: PhantomData<EF>,
345}
346
347impl<'a, C, EF> BitRingSwitchVerifierTranscript<'a, C, EF>
348where
349    EF: TranscriptField + TowerLevel,
350    C: CanObserve<EF> + CanSample<EF>,
351{
352    /// Seed the transcript from the shape.
353    pub fn new(challenger: &'a mut C, shape: BitRingSwitchShape) -> Self {
354        Self {
355            state: VerifierState::new(challenger, &shape.domain_separator::<EF>(), &[]),
356            shape,
357            _level: PhantomData,
358        }
359    }
360
361    /// Replay the statement, then redraw the batching challenges.
362    ///
363    /// Takes the same arguments as the prover side and returns the same draws.
364    ///
365    /// # Errors
366    ///
367    /// Returns an error, releasing the driver, before anything is absorbed:
368    ///
369    /// - when the point or a row list is not the described width
370    /// - when the presence of the successor rows disagrees with the shape
371    pub fn statement(
372        &mut self,
373        point: &Point<EF>,
374        rows: &[EF],
375        successor: Option<(&[EF], &[EF])>,
376    ) -> Result<(Point<EF>, Option<EF>), TranscriptWidth> {
377        if let Err(error) = self.check_widths(point, rows, successor) {
378            self.state.abort();
379            return Err(error);
380        }
381
382        let _ = self
383            .state
384            .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(
385                EVALUATION_POINT,
386                point.as_slice(),
387            );
388        let _ = self
389            .state
390            .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(TENSOR_ROWS, rows);
391        if let Some((carry, last)) = successor {
392            let _ = self
393                .state
394                .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(CARRY_ROWS, carry);
395            let _ = self
396                .state
397                .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(LAST_ROWS, last);
398        }
399
400        let batching_point = Point::new(
401            self.state
402                .challenge_extensions::<EF, EF, FieldToFieldCodec<EF>>(
403                    BATCHING_POINT,
404                    BitRingSwitch::<EF>::ABSORBED,
405                )
406                .into_iter()
407                .map(TranscriptBound::into_inner)
408                .collect(),
409        );
410        let alpha = successor.map(|_| {
411            self.state
412                .challenge_extension::<EF, EF, FieldToFieldCodec<EF>>(TENSOR_BATCHING)
413                .into_inner()
414        });
415        Ok((batching_point, alpha))
416    }
417
418    /// Check every list of the statement against the description, absorbing nothing.
419    fn check_widths(
420        &self,
421        point: &Point<EF>,
422        rows: &[EF],
423        successor: Option<(&[EF], &[EF])>,
424    ) -> Result<(), TranscriptWidth> {
425        check_statement_widths(&self.shape, point, rows, successor)
426    }
427
428    /// Hand the sponge to the delegated sumcheck replay.
429    pub fn batched_sumcheck<R>(&mut self, run: impl FnOnce(&mut C) -> R) -> R {
430        self.state
431            .begin_protocol::<BatchedSumcheck>(BATCHED_SUMCHECK);
432        let output = run(self.state.challenger_mut());
433        self.state.end_protocol::<BatchedSumcheck>(BATCHED_SUMCHECK);
434        output
435    }
436
437    /// Replay the value the surviving claim carries.
438    pub fn surviving_claim(&mut self, value: EF) {
439        self.state
440            .observe_extension::<EF, EF, FieldToFieldCodec<EF>>(SURVIVING_CLAIM, &value);
441    }
442
443    /// Release the completeness check because the proof is being rejected.
444    pub fn abort(&mut self) {
445        self.state.abort();
446    }
447
448    /// Close the transcript, panicking unless every described step was replayed.
449    pub fn finish(self) {
450        self.state
451            .finalize()
452            .expect("a bit-alphabet reduction reads an empty wire");
453    }
454}
455
456/// Check one claim's statement against the shape it was described with, absorbing nothing.
457fn check_statement_widths<EF: TowerLevel>(
458    shape: &BitRingSwitchShape,
459    point: &Point<EF>,
460    rows: &[EF],
461    successor: Option<(&[EF], &[EF])>,
462) -> Result<(), TranscriptWidth> {
463    if point.num_variables() != shape.num_variables {
464        return Err(TranscriptWidth::Point {
465            expected: shape.num_variables,
466            actual: point.num_variables(),
467        });
468    }
469    // Every element is a square bit matrix, so every row list has the level's dimension.
470    let successor_rows = successor
471        .into_iter()
472        .flat_map(|(carry, last)| [carry, last]);
473    if let Some(malformed) = core::iter::once(rows)
474        .chain(successor_rows)
475        .find(|rows| rows.len() != Coefficients::<EF>::DIMENSION)
476    {
477        return Err(TranscriptWidth::TensorRows {
478            expected: Coefficients::<EF>::DIMENSION,
479            actual: malformed.len(),
480        });
481    }
482
483    let expected = shape.successor_rows.is_some();
484    if successor.is_some() == expected {
485        Ok(())
486    } else {
487        Err(TranscriptWidth::successor_elements(
488            expected,
489            successor.is_some(),
490        ))
491    }
492}
493
494/// Protocol name of a batch of claims, distinct from the one-claim run's.
495pub(crate) const CLAIMS_NAME: &[u8] = b"p3-sumcheck-bit-ring-switch-claims";
496
497/// Step label of the challenge that folds the claims' batched rows into one sum.
498const CLAIM_BATCHING: &str = "claim_batching";
499
500/// What one claim of a batch binds before any batching draw.
501#[derive(Clone, Copy, Debug)]
502pub struct ClaimStatement<'a, EF> {
503    /// The evaluation point of the claim.
504    pub point: &'a Point<EF>,
505    /// The rows of its tensor element.
506    pub rows: &'a [EF],
507    /// The rows of its carry and last elements, when its shape has successor rows.
508    pub successor: Option<(&'a [EF], &'a [EF])>,
509}
510
511/// The challenges a batch of claims draws once every claim is bound.
512#[derive(Clone, Debug, PartialEq, Eq)]
513pub struct ClaimsDraws<EF> {
514    /// One challenge per absorbed coordinate, shared by every claim.
515    pub batching_point: Point<EF>,
516    /// The challenge batching successor elements, when some claim sends them.
517    pub alpha: Option<EF>,
518    /// The challenge whose powers weigh the claims, claim `i` by `lambda^i`.
519    pub lambda: EF,
520}
521
522/// Numbers that fix the transcript of a batch of at least two bit-alphabet claims.
523///
524/// ```text
525///     per claim        point, tensor rows [, carry rows, last rows]
526///     then, once       batching point, [tensor batching,] claim batching
527///     then, once       sumcheck bracket, surviving claim
528/// ```
529///
530/// Both sides build this from their own configuration, never from a proof.
531#[derive(Clone, Debug, PartialEq, Eq)]
532pub struct BitRingSwitchClaimsShape {
533    /// The shape of each claim, in the order the claims are bound.
534    pub claims: Vec<BitRingSwitchShape>,
535}
536
537impl BitRingSwitchClaimsShape {
538    /// Whether some claim sends successor elements, so the shared `alpha` is drawn.
539    #[must_use]
540    pub fn sends_successor(&self) -> bool {
541        self.claims
542            .iter()
543            .any(|claim| claim.successor_rows.is_some())
544    }
545
546    /// Describe every step of one batched run, which one matched bracket always validates.
547    #[must_use]
548    pub fn pattern<EF: TranscriptField + TowerLevel>(&self) -> InteractionPattern {
549        let rows = |label| {
550            Interaction::algebra::<EF, EF>(
551                Hierarchy::Atomic,
552                Kind::Message,
553                label,
554                Length::Fixed(Coefficients::<EF>::DIMENSION),
555            )
556        };
557        let scalar_challenge = |label| {
558            Interaction::algebra::<EF, EF>(
559                Hierarchy::Atomic,
560                Kind::Challenge,
561                label,
562                Length::Scalar,
563            )
564        };
565
566        let mut steps = Vec::new();
567        // Every claim is bound whole before any draw, which is what the batching bound needs.
568        for claim in &self.claims {
569            steps.push(Interaction::algebra::<EF, EF>(
570                Hierarchy::Atomic,
571                Kind::Message,
572                EVALUATION_POINT,
573                Length::Fixed(claim.num_variables),
574            ));
575            steps.push(rows(TENSOR_ROWS));
576            if claim.successor_rows.is_some() {
577                steps.extend([rows(CARRY_ROWS), rows(LAST_ROWS)]);
578            }
579        }
580        // One batching point shared by every claim collapses each claim's rows.
581        steps.push(Interaction::algebra::<EF, EF>(
582            Hierarchy::Atomic,
583            Kind::Challenge,
584            BATCHING_POINT,
585            Length::Fixed(BitRingSwitch::<EF>::ABSORBED),
586        ));
587        if self.sends_successor() {
588            steps.push(scalar_challenge(TENSOR_BATCHING));
589        }
590        // Powers of one more challenge fold the claims' sums into the one the rounds prove.
591        steps.push(scalar_challenge(CLAIM_BATCHING));
592        steps.extend([
593            Interaction::marker::<BatchedSumcheck>(
594                Hierarchy::Begin,
595                Kind::Protocol,
596                BATCHED_SUMCHECK,
597            ),
598            Interaction::marker::<BatchedSumcheck>(
599                Hierarchy::End,
600                Kind::Protocol,
601                BATCHED_SUMCHECK,
602            ),
603            Interaction::algebra::<EF, EF>(
604                Hierarchy::Atomic,
605                Kind::Message,
606                SURVIVING_CLAIM,
607                Length::Scalar,
608            ),
609        ]);
610
611        InteractionPattern::new(steps).expect("one matched bracket is always well formed")
612    }
613
614    /// Bind the protocol identity and this shape into a seed.
615    ///
616    /// Each claim's successor row count is an instance label, as in the one-claim run.
617    /// An empty label marks a claim without successor rows, so no two shapes share a seed.
618    #[must_use]
619    pub fn domain_separator<EF: TranscriptField + TowerLevel>(
620        &self,
621    ) -> DomainSeparator<Alphabet<EF>> {
622        let mut separator = DomainSeparator::new(VERSION, CLAIMS_NAME, self.pattern::<EF>());
623        separator.instance(&(self.claims.len() as u64).to_be_bytes());
624        for claim in &self.claims {
625            match claim.successor_rows {
626                Some(rows) => separator.instance(&(rows as u64).to_be_bytes()),
627                None => separator.instance(&[]),
628            };
629        }
630        separator
631    }
632}
633
634/// Prover-side transcript of a batch of bit-alphabet claims.
635pub struct BitRingSwitchClaimsProverTranscript<'a, C, EF: TranscriptField> {
636    /// Driver walking the description and holding the borrowed sponge.
637    state: ProverState<&'a mut C, Alphabet<EF>>,
638    /// The numbers this run was described with.
639    shape: BitRingSwitchClaimsShape,
640}
641
642impl<'a, C, EF> BitRingSwitchClaimsProverTranscript<'a, C, EF>
643where
644    EF: TranscriptField + TowerLevel,
645    C: CanObserve<EF> + CanSample<EF>,
646{
647    /// Seed the transcript from the shape, folding its fingerprint into the sponge.
648    pub fn new(challenger: &'a mut C, shape: BitRingSwitchClaimsShape) -> Self {
649        Self {
650            state: ProverState::new(challenger, &shape.domain_separator::<EF>()),
651            shape,
652        }
653    }
654
655    /// Bind every claim's point and elements, then draw the batching challenges.
656    ///
657    /// # Panics
658    ///
659    /// - When the claim count or a claim's successor rows disagree with the shape.
660    /// - When a list is not the width the run was described with.
661    pub fn statement(&mut self, claims: &[ClaimStatement<'_, EF>]) -> ClaimsDraws<EF> {
662        assert_eq!(
663            claims.len(),
664            self.shape.claims.len(),
665            "one statement per claim the shape describes"
666        );
667        for (claim, shape) in claims.iter().zip(&self.shape.claims) {
668            assert_eq!(
669                claim.successor.is_some(),
670                shape.successor_rows.is_some(),
671                "the successor elements are sent exactly when the shape describes them",
672            );
673            self.state
674                .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(
675                    EVALUATION_POINT,
676                    claim.point.as_slice(),
677                );
678            self.state
679                .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(TENSOR_ROWS, claim.rows);
680            if let Some((carry, last)) = claim.successor {
681                self.state
682                    .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(CARRY_ROWS, carry);
683                self.state
684                    .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(LAST_ROWS, last);
685            }
686        }
687        // Only now are the batching challenges drawn, so no message above them knew them.
688        let batching_point = Point::new(
689            self.state
690                .challenge_extensions::<EF, EF, FieldToFieldCodec<EF>>(
691                    BATCHING_POINT,
692                    BitRingSwitch::<EF>::ABSORBED,
693                )
694                .into_iter()
695                .map(TranscriptBound::into_inner)
696                .collect(),
697        );
698        let alpha = self.shape.sends_successor().then(|| {
699            self.state
700                .challenge_extension::<EF, EF, FieldToFieldCodec<EF>>(TENSOR_BATCHING)
701                .into_inner()
702        });
703        let lambda = self
704            .state
705            .challenge_extension::<EF, EF, FieldToFieldCodec<EF>>(CLAIM_BATCHING)
706            .into_inner();
707        ClaimsDraws {
708            batching_point,
709            alpha,
710            lambda,
711        }
712    }
713
714    /// Hand the sponge to the delegated sumcheck rounds.
715    pub fn batched_sumcheck<R>(&mut self, run: impl FnOnce(&mut C) -> R) -> R {
716        self.state
717            .begin_protocol::<BatchedSumcheck>(BATCHED_SUMCHECK);
718        let output = run(self.state.challenger_mut());
719        self.state.end_protocol::<BatchedSumcheck>(BATCHED_SUMCHECK);
720        output
721    }
722
723    /// Bind the value the surviving claim carries.
724    pub fn surviving_claim(&mut self, value: EF) {
725        self.state
726            .observe_extension::<EF, EF, FieldToFieldCodec<EF>>(SURVIVING_CLAIM, &value);
727    }
728
729    /// Close the transcript, panicking unless every described step was played.
730    pub fn finish(self) {
731        assert!(
732            self.state.finalize().is_empty(),
733            "a batch of bit-alphabet claims carries every value in its own proof",
734        );
735    }
736}
737
738/// Verifier-side transcript of a batch of bit-alphabet claims.
739///
740/// Mirrors the prover side call for call, over the same description.
741pub struct BitRingSwitchClaimsVerifierTranscript<'a, C, EF: TranscriptField> {
742    /// Driver walking the description and holding the borrowed sponge.
743    state: VerifierState<'static, &'a mut C, Alphabet<EF>>,
744    /// The numbers this run was described with.
745    shape: BitRingSwitchClaimsShape,
746}
747
748impl<'a, C, EF> BitRingSwitchClaimsVerifierTranscript<'a, C, EF>
749where
750    EF: TranscriptField + TowerLevel,
751    C: CanObserve<EF> + CanSample<EF>,
752{
753    /// Seed the transcript from the shape.
754    pub fn new(challenger: &'a mut C, shape: BitRingSwitchClaimsShape) -> Self {
755        Self {
756            state: VerifierState::new(challenger, &shape.domain_separator::<EF>(), &[]),
757            shape,
758        }
759    }
760
761    /// Replay every claim's statement, then redraw the batching challenges.
762    ///
763    /// # Errors
764    ///
765    /// Returns an error, releasing the driver, before anything is absorbed:
766    ///
767    /// - when the claim count disagrees with the shape
768    /// - when a point or a row list is not the described width
769    /// - when a claim's successor rows disagree with its shape
770    pub fn statement(
771        &mut self,
772        claims: &[ClaimStatement<'_, EF>],
773    ) -> Result<ClaimsDraws<EF>, TranscriptWidth> {
774        let checked = if claims.len() == self.shape.claims.len() {
775            claims
776                .iter()
777                .zip(&self.shape.claims)
778                .try_for_each(|(claim, shape)| {
779                    check_statement_widths(shape, claim.point, claim.rows, claim.successor)
780                })
781        } else {
782            Err(TranscriptWidth::Claims {
783                expected: self.shape.claims.len(),
784                actual: claims.len(),
785            })
786        };
787        if let Err(error) = checked {
788            self.state.abort();
789            return Err(error);
790        }
791
792        for claim in claims {
793            let _ = self
794                .state
795                .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(
796                    EVALUATION_POINT,
797                    claim.point.as_slice(),
798                );
799            let _ = self
800                .state
801                .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(TENSOR_ROWS, claim.rows);
802            if let Some((carry, last)) = claim.successor {
803                let _ = self
804                    .state
805                    .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(CARRY_ROWS, carry);
806                let _ = self
807                    .state
808                    .observe_extensions::<EF, EF, FieldToFieldCodec<EF>>(LAST_ROWS, last);
809            }
810        }
811        // Only now are the batching challenges drawn, so no message above them knew them.
812        let batching_point = Point::new(
813            self.state
814                .challenge_extensions::<EF, EF, FieldToFieldCodec<EF>>(
815                    BATCHING_POINT,
816                    BitRingSwitch::<EF>::ABSORBED,
817                )
818                .into_iter()
819                .map(TranscriptBound::into_inner)
820                .collect(),
821        );
822        let alpha = self.shape.sends_successor().then(|| {
823            self.state
824                .challenge_extension::<EF, EF, FieldToFieldCodec<EF>>(TENSOR_BATCHING)
825                .into_inner()
826        });
827        let lambda = self
828            .state
829            .challenge_extension::<EF, EF, FieldToFieldCodec<EF>>(CLAIM_BATCHING)
830            .into_inner();
831        Ok(ClaimsDraws {
832            batching_point,
833            alpha,
834            lambda,
835        })
836    }
837
838    /// Hand the sponge to the delegated sumcheck replay.
839    pub fn batched_sumcheck<R>(&mut self, run: impl FnOnce(&mut C) -> R) -> R {
840        self.state
841            .begin_protocol::<BatchedSumcheck>(BATCHED_SUMCHECK);
842        let output = run(self.state.challenger_mut());
843        self.state.end_protocol::<BatchedSumcheck>(BATCHED_SUMCHECK);
844        output
845    }
846
847    /// Replay the value the surviving claim carries.
848    pub fn surviving_claim(&mut self, value: EF) {
849        self.state
850            .observe_extension::<EF, EF, FieldToFieldCodec<EF>>(SURVIVING_CLAIM, &value);
851    }
852
853    /// Release the completeness check because the proof is being rejected.
854    pub fn abort(&mut self) {
855        self.state.abort();
856    }
857
858    /// Close the transcript, panicking unless every described step was replayed.
859    pub fn finish(self) {
860        self.state
861            .finalize()
862            .expect("a batch of bit-alphabet claims reads an empty wire");
863    }
864}
865
866/// A list whose width does not match the one the run was described with.
867#[derive(Clone, Copy, Debug, thiserror::Error, PartialEq, Eq)]
868#[non_exhaustive]
869pub enum TranscriptWidth {
870    /// The evaluation point names the wrong number of coordinates.
871    #[error("the evaluation point names {actual} coordinates, expected {expected}")]
872    Point {
873        /// Coordinates the description fixes.
874        expected: usize,
875        /// Coordinates supplied.
876        actual: usize,
877    },
878    /// A tensor element carries the wrong number of rows.
879    #[error("the tensor element carries {actual} rows, expected {expected}")]
880    TensorRows {
881        /// Rows the level's dimension fixes.
882        expected: usize,
883        /// Rows supplied.
884        actual: usize,
885    },
886    /// A batch binds a different number of claims than its description.
887    #[error("the batch binds {actual} claims, expected {expected}")]
888    Claims {
889        /// Claims the description fixes.
890        expected: usize,
891        /// Claims supplied.
892        actual: usize,
893    },
894    /// The presence of the successor elements disagrees with the description.
895    ///
896    /// The count is zero or two, one carry element and one last element.
897    #[error("the statement carries {actual} successor elements, expected {expected}")]
898    SuccessorElements {
899        /// Elements the description fixes.
900        expected: usize,
901        /// Elements supplied.
902        actual: usize,
903    },
904}
905
906impl TranscriptWidth {
907    /// The successor-element mismatch, from whether each side has the elements.
908    #[must_use]
909    pub(crate) const fn successor_elements(expected: bool, actual: bool) -> Self {
910        const fn count(present: bool) -> usize {
911            if present { SUCCESSOR_ELEMENTS } else { 0 }
912        }
913        Self::SuccessorElements {
914            expected: count(expected),
915            actual: count(actual),
916        }
917    }
918}
919
920#[cfg(test)]
921mod tests {
922    use alloc::vec::Vec;
923
924    use p3_binary_field::{BinaryChallenger, BinaryField16};
925    use p3_challenger::HashChallenger;
926    use p3_challenger::testing::{
927        SeedDigest, assert_seeds_pairwise_distinct, pow_difficulties, seed_digest,
928    };
929    use p3_field::PrimeCharacteristicRing;
930    use p3_keccak::Keccak256Hash;
931
932    use super::*;
933
934    type EF = BinaryField16;
935    type Chal = BinaryChallenger<EF, HashChallenger<u8, Keccak256Hash, 32>>;
936
937    /// Coordinate count every run below is described with.
938    ///
939    /// A 16-bit level absorbs four of them, leaving four sumcheck rounds.
940    const NUM_VARIABLES: usize = 8;
941
942    /// Rows a 16-bit level's tensor element carries, one per basis coordinate.
943    const NUM_ROWS: usize = 16;
944
945    fn fresh_challenger() -> Chal {
946        // A fresh sponge, so two runs differ only where the transcript makes them differ.
947        Chal::from_hasher(Vec::new(), Keccak256Hash)
948    }
949
950    /// Row coordinates of the successor shape, two more than one element absorbs.
951    const SUCCESSOR_ROWS: usize = 6;
952
953    /// Baseline shape every mutation below is measured against.
954    const fn base_shape() -> BitRingSwitchShape {
955        BitRingSwitchShape::new(NUM_VARIABLES)
956    }
957
958    /// A shape whose reduction sends the two successor elements.
959    const fn successor_shape() -> BitRingSwitchShape {
960        BitRingSwitchShape::with_successor_rows(NUM_VARIABLES, SUCCESSOR_ROWS)
961    }
962
963    /// The digest of the byte stream a shape seeds its sponge with.
964    ///
965    /// Comparing seed streams keeps the sponge out of the separation claim.
966    fn seed_of(shape: BitRingSwitchShape) -> SeedDigest {
967        seed_digest(&shape.domain_separator::<EF>())
968    }
969
970    /// Every field of the shape, each moved one step away from the baseline.
971    ///
972    /// A field added to the shape stops the destructuring below from compiling.
973    fn one_step_from_base() -> Vec<(&'static str, BitRingSwitchShape)> {
974        // Exhaustiveness check: every field named, none elided by a rest pattern.
975        let BitRingSwitchShape {
976            num_variables: _,
977            successor_rows: _,
978        } = base_shape();
979
980        // One more coordinate widens the step that binds the point.
981        let mut wider = base_shape();
982        wider.num_variables += 1;
983
984        // Two successor shapes differing only in the row count.
985        // The pattern is the same for both, so only the instance binding can part them.
986        alloc::vec![
987            ("num_variables", wider),
988            ("successor_rows", successor_shape()),
989            (
990                "successor_rows_count",
991                BitRingSwitchShape::with_successor_rows(NUM_VARIABLES, SUCCESSOR_ROWS + 1),
992            ),
993        ]
994    }
995
996    /// A point whose coordinates are distinct and seed-dependent.
997    fn point_of(num_variables: usize, seed: u32) -> Point<EF> {
998        Point::new(
999            (0..num_variables)
1000                .map(|i| EF::from_u32(seed * 31 + i as u32 + 1))
1001                .collect(),
1002        )
1003    }
1004
1005    /// A full-width row list whose entries are distinct and seed-dependent.
1006    fn rows_of(seed: u32) -> Vec<EF> {
1007        (0..NUM_ROWS)
1008            .map(|i| EF::from_u32(seed * 17 + i as u32 + 1))
1009            .collect()
1010    }
1011
1012    /// Everything one run produces, in the order the description fixes.
1013    ///
1014    /// The batching point comes first, so a test can read it on its own.
1015    /// The second draw batches the successor elements, when the shape sends them.
1016    type Draws = (Point<EF>, Option<EF>, EF);
1017
1018    /// The carry and last rows a statement binds, when its shape has successor rows.
1019    type SuccessorRows<'a> = Option<(&'a [EF], &'a [EF])>;
1020
1021    /// Drive a full prover-side run and hand back the draws it produced.
1022    ///
1023    /// The delegated sumcheck is stood in for by a single draw.
1024    /// That keeps the bracket on the path a real delegation takes.
1025    fn drive_prover(
1026        challenger: &mut Chal,
1027        shape: BitRingSwitchShape,
1028        point: &Point<EF>,
1029        rows: &[EF],
1030        successor: SuccessorRows<'_>,
1031        claim: EF,
1032    ) -> Draws {
1033        let mut transcript = BitRingSwitchProverTranscript::<Chal, EF>::new(challenger, shape);
1034        let (batching_point, alpha) = transcript.statement(point, rows, successor);
1035        let delegated = transcript.batched_sumcheck(<Chal as CanSample<EF>>::sample);
1036        transcript.surviving_claim(claim);
1037        transcript.finish();
1038        (batching_point, alpha, delegated)
1039    }
1040
1041    /// Replay a full verifier-side run against recorded values.
1042    fn drive_verifier(
1043        challenger: &mut Chal,
1044        shape: BitRingSwitchShape,
1045        point: &Point<EF>,
1046        rows: &[EF],
1047        successor: SuccessorRows<'_>,
1048        claim: EF,
1049    ) -> Result<Draws, TranscriptWidth> {
1050        let mut transcript = BitRingSwitchVerifierTranscript::<Chal, EF>::new(challenger, shape);
1051        let (batching_point, alpha) = transcript.statement(point, rows, successor)?;
1052        let delegated = transcript.batched_sumcheck(<Chal as CanSample<EF>>::sample);
1053        transcript.surviving_claim(claim);
1054        transcript.finish();
1055        Ok((batching_point, alpha, delegated))
1056    }
1057
1058    /// Everything a verifier redraws from one recorded run, plus the state it hands back.
1059    ///
1060    /// The trailing draw is taken after the run closes.
1061    /// It exposes a value bound with nothing left inside the description to move.
1062    fn replay(point: &Point<EF>, rows: &[EF], claim: EF) -> (Draws, EF) {
1063        replay_in(
1064            BitRingSwitchShape::new(point.num_variables()),
1065            point,
1066            rows,
1067            None,
1068            claim,
1069        )
1070    }
1071
1072    /// The same replay, over a shape and successor elements of the caller's choosing.
1073    fn replay_in(
1074        shape: BitRingSwitchShape,
1075        point: &Point<EF>,
1076        rows: &[EF],
1077        successor: SuccessorRows<'_>,
1078        claim: EF,
1079    ) -> (Draws, EF) {
1080        let mut challenger = fresh_challenger();
1081        let draws = drive_verifier(&mut challenger, shape, point, rows, successor, claim)
1082            .expect("a well-shaped run always replays");
1083        (draws, CanSample::<EF>::sample(&mut challenger))
1084    }
1085
1086    #[test]
1087    fn the_same_shape_seeds_the_same_stream_twice() {
1088        // Completeness: the seed is a pure function of the shape.
1089        assert_eq!(seed_of(base_shape()), seed_of(base_shape()));
1090    }
1091
1092    #[test]
1093    fn no_two_configurations_of_the_shape_share_a_seed() {
1094        // Invariant: the knobs are separated from each other, not merely from a baseline.
1095        //
1096        //     baseline in the set    ->  every knob has to reach the seed
1097        //     pairwise over the set  ->  no two knobs may land on one seed
1098        let mut seeds = alloc::vec![("base", seed_of(base_shape()))];
1099        seeds.extend(
1100            one_step_from_base()
1101                .into_iter()
1102                .map(|(field, shape)| (field, seed_of(shape))),
1103        );
1104
1105        assert_seeds_pairwise_distinct(&seeds);
1106    }
1107
1108    #[test]
1109    fn the_description_asks_for_no_grinding() {
1110        // Invariant: this reduction grinds nowhere.
1111        //
1112        // A step appearing here would be a cost neither side accounts for.
1113        assert!(pow_difficulties(&base_shape().pattern::<EF>()).is_empty());
1114    }
1115
1116    #[test]
1117    fn the_two_derived_widths_come_from_the_level() {
1118        // Fixture state: a 16-bit level over F_2.
1119        //
1120        //     - absorbed coordinates  ->  log2(16) = 4
1121        //     - tensor rows           ->  16
1122        //     - sumcheck rounds       ->  8 - 4   = 4
1123        assert_eq!(BitRingSwitch::<EF>::ABSORBED, 4);
1124        assert_eq!(Coefficients::<EF>::DIMENSION, NUM_ROWS);
1125        assert_eq!(base_shape().sumcheck_rounds::<EF>(), 4);
1126    }
1127
1128    #[test]
1129    fn both_sides_of_a_run_draw_the_same_stream() {
1130        // Completeness: the two drivers walk one description and land on one stream.
1131        //
1132        // Fixture state: 8 coordinates, 16 rows, one delegated draw.
1133        let point = point_of(NUM_VARIABLES, 3);
1134        let rows = rows_of(5);
1135
1136        let mut prover_challenger = fresh_challenger();
1137        let proved = drive_prover(
1138            &mut prover_challenger,
1139            base_shape(),
1140            &point,
1141            &rows,
1142            None,
1143            EF::ONE,
1144        );
1145
1146        let mut verifier_challenger = fresh_challenger();
1147        let replayed = drive_verifier(
1148            &mut verifier_challenger,
1149            base_shape(),
1150            &point,
1151            &rows,
1152            None,
1153            EF::ONE,
1154        )
1155        .expect("the honest run must replay");
1156
1157        assert_eq!(proved, replayed);
1158
1159        // The sponge is handed back in one state, so the surrounding protocol stays in step.
1160        assert_eq!(
1161            CanSample::<EF>::sample(&mut prover_challenger),
1162            CanSample::<EF>::sample(&mut verifier_challenger),
1163        );
1164    }
1165
1166    #[test]
1167    fn a_perturbed_point_coordinate_moves_every_later_draw() {
1168        // Invariant: the point is bound before anything is drawn against it.
1169        //
1170        // Without it one proof would replay at every point sharing its absorbed tail.
1171        //
1172        // Mutation: bump one coordinate by one, once per position.
1173        //
1174        //     honest:    [c_0, ..., c_i,     ..., c_7]
1175        //     tampered:  [c_0, ..., c_i + 1, ..., c_7]
1176        let honest = point_of(NUM_VARIABLES, 3);
1177        let rows = rows_of(5);
1178        let baseline = replay(&honest, &rows, EF::ONE);
1179
1180        for position in 0..NUM_VARIABLES {
1181            let mut moved = honest.as_slice().to_vec();
1182            moved[position] += EF::ONE;
1183            assert_ne!(
1184                baseline,
1185                replay(&Point::new(moved), &rows, EF::ONE),
1186                "tampering with coordinate {position} left the stream where it was",
1187            );
1188        }
1189    }
1190
1191    #[test]
1192    fn a_perturbed_tensor_row_moves_every_later_draw() {
1193        // Invariant: the rows that cross the wire are what enters the sponge.
1194        //
1195        // The rows are the whole element, so binding them binds both of its readings.
1196        // Binding one derived reading instead would leave the other unbound.
1197        //
1198        // Mutation: bump one row by one, at both ends and in the middle.
1199        //
1200        //     16 rows  ->  positions 0, 8 and 15
1201        let point = point_of(NUM_VARIABLES, 3);
1202        let honest = rows_of(5);
1203        let baseline = replay(&point, &honest, EF::ONE);
1204
1205        for position in [0, NUM_ROWS / 2, NUM_ROWS - 1] {
1206            let mut tampered = honest.clone();
1207            tampered[position] += EF::ONE;
1208            assert_ne!(
1209                baseline,
1210                replay(&point, &tampered, EF::ONE),
1211                "tampering with row {position} left the stream where it was",
1212            );
1213        }
1214    }
1215
1216    #[test]
1217    fn the_batching_draw_is_the_first_challenge_and_answers_to_the_rows() {
1218        // Invariant: the batching challenge is drawn after the element is bound.
1219        //
1220        // This is the ordering the reduction's soundness rests on.
1221        //
1222        // A bit matrix solving two F_2-linear systems moves the claim with the sum held.
1223        // A prover who knew the challenge first could search for such a matrix.
1224        //
1225        // Two things are pinned below.
1226        // Either one alone can be satisfied while the order is still wrong.
1227        //
1228        // First, where the steps sit in the description:
1229        //
1230        //     ... evaluation_point | tensor_rows | batching_point ...
1231        //                                ^             ^
1232        //                                |             the first challenge of the run
1233        //                                bound before it
1234        let pattern = base_shape().pattern::<EF>();
1235        let labels: Vec<&str> = pattern
1236            .interactions()
1237            .iter()
1238            .map(Interaction::label)
1239            .collect();
1240
1241        let point_at = labels
1242            .iter()
1243            .position(|&label| label == EVALUATION_POINT)
1244            .expect("the description binds the evaluation point");
1245        let rows_at = labels
1246            .iter()
1247            .position(|&label| label == TENSOR_ROWS)
1248            .expect("the description binds the tensor rows");
1249        let first_challenge = pattern
1250            .interactions()
1251            .iter()
1252            .position(|interaction| interaction.kind() == Kind::Challenge)
1253            .expect("the description draws a challenge");
1254
1255        assert_eq!(labels[first_challenge], BATCHING_POINT);
1256        assert!(
1257            point_at < first_challenge,
1258            "the evaluation point is bound at step {point_at}, the first challenge is step \
1259             {first_challenge}",
1260        );
1261        assert!(
1262            rows_at < first_challenge,
1263            "the rows are bound at step {rows_at}, the first challenge is step \
1264             {first_challenge}",
1265        );
1266
1267        // Second, that the draw answers to the rows rather than merely following them.
1268        //
1269        // A run binding the rows after the draw would still move every later draw.
1270        // Only the batching point itself discriminates here.
1271        //
1272        // Mutation: bump one row by one, once per position.
1273        let point = point_of(NUM_VARIABLES, 3);
1274        let honest = rows_of(5);
1275        let (baseline, _) = replay(&point, &honest, EF::ONE);
1276
1277        for position in 0..NUM_ROWS {
1278            let mut tampered = honest.clone();
1279            tampered[position] += EF::ONE;
1280            let (moved, _) = replay(&point, &tampered, EF::ONE);
1281            assert_ne!(
1282                baseline.0, moved.0,
1283                "row {position} left the batching point where it was",
1284            );
1285        }
1286    }
1287
1288    #[test]
1289    fn a_perturbed_surviving_claim_moves_the_state_the_sponge_is_handed_back_in() {
1290        // Invariant: the surviving claim is bound before the sponge goes back.
1291        //
1292        // Nothing inside this description is drawn after it.
1293        // The effect therefore shows up outside.
1294        //
1295        // Mutation: bump the claim by one and compare the draw taken past the run's end.
1296        let point = point_of(NUM_VARIABLES, 3);
1297        let rows = rows_of(5);
1298
1299        assert_ne!(
1300            replay(&point, &rows, EF::ONE),
1301            replay(&point, &rows, EF::TWO),
1302        );
1303    }
1304
1305    // The two tests below drive the verifier transcript the way a downstream crate would.
1306    //
1307    // Values go in straight from proof fields, with no shape pre-check in front.
1308    // A panic here would compound with the driver's own drop check and abort.
1309
1310    #[test]
1311    fn a_tensor_element_of_the_wrong_width_is_rejected() {
1312        // Described run: 16 rows, fixed by the level alone.
1313        //
1314        //     described:    16
1315        //     proof holds:  1   -> rejected before anything is absorbed
1316        let mut challenger = fresh_challenger();
1317        let mut transcript =
1318            BitRingSwitchVerifierTranscript::<Chal, EF>::new(&mut challenger, base_shape());
1319
1320        let err = transcript
1321            .statement(&point_of(NUM_VARIABLES, 3), &[EF::ONE], None)
1322            .expect_err("a tensor element outside the described width must error");
1323
1324        assert_eq!(
1325            err,
1326            TranscriptWidth::TensorRows {
1327                expected: NUM_ROWS,
1328                actual: 1,
1329            },
1330        );
1331
1332        // The rejection leaves the run part-played, with later steps still described.
1333        // Absorbing the width error is what releases the completeness check.
1334        drop(transcript);
1335    }
1336
1337    #[test]
1338    fn an_evaluation_point_of_the_wrong_width_is_rejected() {
1339        // Described run: 8 coordinates, taken from the replaying side's configuration.
1340        //
1341        //     described:    8
1342        //     handed over:  3  -> rejected before anything is absorbed
1343        let mut challenger = fresh_challenger();
1344        let mut transcript =
1345            BitRingSwitchVerifierTranscript::<Chal, EF>::new(&mut challenger, base_shape());
1346
1347        let err = transcript
1348            .statement(&point_of(3, 3), &rows_of(5), None)
1349            .expect_err("a point outside the described width must error");
1350
1351        assert_eq!(
1352            err,
1353            TranscriptWidth::Point {
1354                expected: NUM_VARIABLES,
1355                actual: 3,
1356            },
1357        );
1358
1359        drop(transcript);
1360    }
1361
1362    #[test]
1363    fn a_successor_element_list_outside_the_description_is_rejected() {
1364        // Described run: the shape alone fixes whether two successor elements follow the rows.
1365        //
1366        //     shape       proof holds        -> rejected before anything is absorbed
1367        //     plain       two elements       -> 0 expected, 2 supplied
1368        //     successor   none               -> 2 expected, 0 supplied
1369        //     successor   a one-row carry    -> a malformed element, like a short tensor
1370        let point = point_of(NUM_VARIABLES, 3);
1371        let rows = rows_of(5);
1372        let (carry, last) = (rows_of(7), rows_of(11));
1373        let cases: [(BitRingSwitchShape, SuccessorRows<'_>, TranscriptWidth); 3] = [
1374            (
1375                base_shape(),
1376                Some((&carry, &last)),
1377                TranscriptWidth::SuccessorElements {
1378                    expected: 0,
1379                    actual: 2,
1380                },
1381            ),
1382            (
1383                successor_shape(),
1384                None,
1385                TranscriptWidth::SuccessorElements {
1386                    expected: 2,
1387                    actual: 0,
1388                },
1389            ),
1390            (
1391                successor_shape(),
1392                Some((&[EF::ONE], &last)),
1393                TranscriptWidth::TensorRows {
1394                    expected: NUM_ROWS,
1395                    actual: 1,
1396                },
1397            ),
1398        ];
1399
1400        for (shape, successor, expected) in cases {
1401            let mut challenger = fresh_challenger();
1402            let mut transcript =
1403                BitRingSwitchVerifierTranscript::<Chal, EF>::new(&mut challenger, shape);
1404
1405            let err = transcript
1406                .statement(&point, &rows, successor)
1407                .expect_err("a successor list outside the description must error");
1408
1409            assert_eq!(err, expected);
1410            drop(transcript);
1411        }
1412    }
1413
1414    #[test]
1415    fn both_sides_of_a_successor_run_draw_the_same_stream() {
1416        // Completeness: the successor steps are walked the same way on both sides.
1417        //
1418        // Fixture state: the base run plus two successor elements and one scalar draw.
1419        let point = point_of(NUM_VARIABLES, 3);
1420        let rows = rows_of(5);
1421        let (carry, last) = (rows_of(7), rows_of(11));
1422        let successor = Some((carry.as_slice(), last.as_slice()));
1423
1424        let mut prover_challenger = fresh_challenger();
1425        let proved = drive_prover(
1426            &mut prover_challenger,
1427            successor_shape(),
1428            &point,
1429            &rows,
1430            successor,
1431            EF::ONE,
1432        );
1433
1434        let mut verifier_challenger = fresh_challenger();
1435        let replayed = drive_verifier(
1436            &mut verifier_challenger,
1437            successor_shape(),
1438            &point,
1439            &rows,
1440            successor,
1441            EF::ONE,
1442        )
1443        .expect("the honest run must replay");
1444
1445        assert_eq!(proved, replayed);
1446        assert!(
1447            proved.1.is_some(),
1448            "a successor shape draws the element batching"
1449        );
1450        assert_eq!(
1451            CanSample::<EF>::sample(&mut prover_challenger),
1452            CanSample::<EF>::sample(&mut verifier_challenger),
1453        );
1454    }
1455
1456    #[test]
1457    fn the_batching_draws_answer_to_the_successor_rows() {
1458        // Invariant: both batching draws come after every element is bound.
1459        //
1460        // A successor element formed after r'' or alpha is the tensor's forgery again.
1461        //
1462        // First, where the steps sit in the description:
1463        //
1464        //     ... tensor_rows | carry_rows | last_rows | batching_point | tensor_batching ...
1465        //                                       ^             ^
1466        //                                       |             the first challenge of the run
1467        //                                       bound before it
1468        let pattern = successor_shape().pattern::<EF>();
1469        let labels: Vec<&str> = pattern
1470            .interactions()
1471            .iter()
1472            .map(Interaction::label)
1473            .collect();
1474
1475        let position = |wanted: &str| {
1476            labels
1477                .iter()
1478                .position(|&label| label == wanted)
1479                .expect("the successor description holds every step")
1480        };
1481        let first_challenge = pattern
1482            .interactions()
1483            .iter()
1484            .position(|interaction| interaction.kind() == Kind::Challenge)
1485            .expect("the description draws a challenge");
1486
1487        assert_eq!(labels[first_challenge], BATCHING_POINT);
1488        assert!(position(TENSOR_ROWS) < position(CARRY_ROWS));
1489        assert!(position(CARRY_ROWS) < position(LAST_ROWS));
1490        assert!(
1491            position(LAST_ROWS) < first_challenge,
1492            "the last rows are bound at step {}, the first challenge is step {first_challenge}",
1493            position(LAST_ROWS),
1494        );
1495        assert_eq!(position(TENSOR_BATCHING), first_challenge + 1);
1496
1497        // Second, that both draws answer to the successor rows rather than merely following them.
1498        //
1499        // Mutation: bump one carry row by one, then one last row.
1500        let point = point_of(NUM_VARIABLES, 3);
1501        let rows = rows_of(5);
1502        let (carry, last) = (rows_of(7), rows_of(11));
1503        let replay_with = |carry: &[EF], last: &[EF]| {
1504            replay_in(
1505                successor_shape(),
1506                &point,
1507                &rows,
1508                Some((carry, last)),
1509                EF::ONE,
1510            )
1511            .0
1512        };
1513        let baseline = replay_with(&carry, &last);
1514
1515        let mut bumped_carry = carry.clone();
1516        bumped_carry[NUM_ROWS / 2] += EF::ONE;
1517        let mut bumped_last = last.clone();
1518        bumped_last[NUM_ROWS - 1] += EF::ONE;
1519
1520        for (element, moved) in [
1521            ("carry", replay_with(&bumped_carry, &last)),
1522            ("last", replay_with(&carry, &bumped_last)),
1523        ] {
1524            assert_ne!(
1525                baseline.0, moved.0,
1526                "a {element} row left the batching point where it was",
1527            );
1528            assert_ne!(
1529                baseline.1, moved.1,
1530                "a {element} row left the element batching where it was",
1531            );
1532        }
1533    }
1534
1535    #[test]
1536    #[should_panic(expected = "the evaluation point must name at least the 4 absorbed")]
1537    fn a_point_shorter_than_the_absorbed_tail_has_no_round_count() {
1538        // Boundary: three coordinates cannot host the four an element absorbs.
1539        //
1540        // The split that separates the absorbed tail from the rest is undefined below four.
1541        let _ = BitRingSwitchShape::new(3).sumcheck_rounds::<EF>();
1542    }
1543
1544    #[test]
1545    fn every_batch_of_claims_seeds_its_own_stream() {
1546        // Invariant: the claim count and each claim's successor rows reach the seed.
1547        //
1548        //     count        two plain claims  vs  three
1549        //     order        plain then successor  vs  successor then plain
1550        //     row count    the same claims, one successor row count apart
1551        //     one claim    a batch of two never shares the one-claim run's seed
1552        let plain = base_shape();
1553        let successor = successor_shape();
1554        let wider = BitRingSwitchShape::with_successor_rows(NUM_VARIABLES, SUCCESSOR_ROWS + 1);
1555        let batch = |claims: &[BitRingSwitchShape]| {
1556            seed_digest(
1557                &BitRingSwitchClaimsShape {
1558                    claims: claims.to_vec(),
1559                }
1560                .domain_separator::<EF>(),
1561            )
1562        };
1563        let seeds = [
1564            ("two plain", batch(&[plain, plain])),
1565            ("three plain", batch(&[plain, plain, plain])),
1566            ("plain, successor", batch(&[plain, successor])),
1567            ("successor, plain", batch(&[successor, plain])),
1568            ("plain, wider successor", batch(&[plain, wider])),
1569            ("one-claim run", seed_of(plain)),
1570        ];
1571        assert_seeds_pairwise_distinct(&seeds);
1572
1573        // Nothing in a batch grinds either.
1574        assert!(
1575            pow_difficulties(
1576                &BitRingSwitchClaimsShape {
1577                    claims: vec![plain, successor]
1578                }
1579                .pattern::<EF>()
1580            )
1581            .is_empty()
1582        );
1583    }
1584
1585    #[test]
1586    fn a_batch_statement_of_the_wrong_count_is_refused_before_absorbing() {
1587        // The verifier checks every claim's widths before the sponge moves.
1588        let shape = BitRingSwitchClaimsShape {
1589            claims: vec![base_shape(), base_shape()],
1590        };
1591        let point = point_of(NUM_VARIABLES, 1);
1592        let rows = rows_of(1);
1593        let claim = ClaimStatement {
1594            point: &point,
1595            rows: &rows,
1596            successor: None,
1597        };
1598        let mut challenger = fresh_challenger();
1599        let mut transcript =
1600            BitRingSwitchClaimsVerifierTranscript::<Chal, EF>::new(&mut challenger, shape);
1601        assert_eq!(
1602            transcript.statement(&[claim]).unwrap_err(),
1603            TranscriptWidth::Claims {
1604                expected: 2,
1605                actual: 1
1606            }
1607        );
1608    }
1609}
p3_sumcheck/ring_switch/bits/transcript.rs

p3_sumcheck/ring_switch/bits/
transcript.rs
