[WIP] recursive_verifier::transcript: Introduce Transcript gadget

halo2/Cargo.toml

@@ -19,7 +19,11 @@ all-features = true
 rustdoc-args = ["--cfg", "docsrs", "--html-in-header", "katex-header.html"]
 
 [dependencies]
+halo2_gadgets = { version = "0.2", path = "../halo2_gadgets" }
 halo2_proofs = { version = "0.2", path = "../halo2_proofs" }
 
+[dev-dependencies]
+rand_core = { version = "0.6", default-features = false, features = ["getrandom"] }
+
 [lib]
 bench = false

halo2/src/lib.rs

@@ -5,3 +5,5 @@
 #![deny(missing_debug_implementations)]
 #![deny(missing_docs)]
 #![deny(unsafe_code)]
+
+mod recursive_verifier;

halo2/src/recursive_verifier.rs

@@ -0,0 +1,2 @@
+//! Gadget that verifies a recursive proof.
+pub mod transcript;

halo2/src/recursive_verifier/transcript.rs

@@ -0,0 +1,104 @@
+use std::marker::PhantomData;
+
+use halo2_gadgets::{
+    ecc::{EccInstructions, Point, ScalarVar},
+    utilities::{bitstring::BitstringInstructions, RangeConstrained},
+};
+use halo2_proofs::{
+    arithmetic::{CurveAffine, FieldExt},
+    circuit::{AssignedCell, Layouter, Value},
+    plonk::Error,
+};
+
+pub trait DuplexInstructions<F: FieldExt> {
+    fn absorb(
+        &mut self,
+        layouter: impl Layouter<F>,
+        value: AssignedCell<F, F>,
+    ) -> Result<(), Error>;
+    fn squeeze(&mut self, layouter: impl Layouter<F>) -> Result<AssignedCell<F, F>, Error>;
+}
+
+pub trait TranscriptInstructions<C: CurveAffine>:
+    BitstringInstructions<C::Base> + DuplexInstructions<C::Base> + EccInstructions<C>
+{
+}
+
+/// A Transcript gadget
+pub struct Transcript<C, TranscriptChip>
+where
+    C: CurveAffine,
+    TranscriptChip: TranscriptInstructions<C>,
+{
+    transcript_chip: TranscriptChip,
+    _marker: PhantomData<C>,
+}
+
+impl<C, TranscriptChip> Transcript<C, TranscriptChip>
+where
+    C: CurveAffine,
+    TranscriptChip: TranscriptInstructions<C>,
+{
+    pub fn new(transcript_chip: TranscriptChip) -> Self {
+        Self {
+            transcript_chip,
+            _marker: PhantomData,
+        }
+    }
+
+    /// Hashes a point into the transcript.
+    pub fn common_point(
+        &mut self,
+        mut layouter: impl Layouter<C::Base>,
+        point: Value<C>,
+    ) -> Result<Point<C, TranscriptChip>, Error> {
+        // Witness point
+        let point = Point::new(
+            self.transcript_chip.clone(),
+            layouter.namespace(|| "witness points"),
+            point,
+        )?;
+
+        // TODO: absorb POSEIDON_PREFIX_POINT
+        self.transcript_chip
+            .absorb(layouter.namespace(|| "x-coordinate"), point.x())?;
+        self.transcript_chip
+            .absorb(layouter.namespace(|| "y-coordinate"), point.y())?;
+
+        Ok(point)
+    }
+
+    /// Reads a scalar field element from the transcript.
+    ///
+    /// This instruction does the following steps:
+    /// - Constrains the next sequence of proof bits to be the representation of a scalar
+    ///   field element.
+    /// - Assigns the scalar field element into the circuit.
+    /// - Updates the transcript's internal state with this scalar field element.
+    /// - Returns the assigned scalar field element.
+    pub fn common_scalar(
+        &mut self,
+        mut layouter: impl Layouter<C::Base>,
+        scalar: Value<C::Scalar>,
+    ) -> Result<ScalarVar<C, TranscriptChip>, Error> {
+        // TODO: absorb POSEIDON_PREFIX_SCALAR
+        // TODO: absorb scalar
+
+        todo!()
+    }
+
+    /// Squeezes a `LENGTH`-bit challenge from the transcript.
+    pub fn squeeze_challenge<const LENGTH: usize>(
+        &mut self,
+        mut layouter: impl Layouter<C::Base>,
+    ) -> Result<RangeConstrained<C::Base, AssignedCell<C::Base, C::Base>>, Error> {
+        let challenge = self
+            .transcript_chip
+            .squeeze(layouter.namespace(|| "squeeze"))?;
+        self.transcript_chip.extract_bitrange(
+            layouter.namespace(|| "extract bitrange"),
+            &challenge,
+            0..LENGTH,
+        )
+    }
+}

halo2_gadgets/src/ecc.rs

@@ -4,7 +4,7 @@ use std::fmt::Debug;
 
 use halo2_proofs::{
     arithmetic::CurveAffine,
-    circuit::{Chip, Layouter, Value},
+    circuit::{AssignedCell, Chip, Layouter, Value},
     plonk::Error,
 };
 
@@ -407,6 +407,16 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> Point<C,
         point.map(|inner| Point { chip, inner })
     }
 
+    /// Returns `x`-coordinate of point
+    pub fn x(&self) -> AssignedCell<C::Base, C::Base> {
+        todo!()
+    }
+
+    /// Returns `y`-coordinate of point
+    pub fn y(&self) -> AssignedCell<C::Base, C::Base> {
+        todo!()
+    }
+
     /// Constrains this point to be equal in value to another point.
     pub fn constrain_equal<Other: Into<Point<C, EccChip>> + Clone>(
         &self,

halo2_gadgets/src/endoscale.rs

@@ -20,7 +20,7 @@ where
     /// A bitstring up to `MAX_BITSTRING_LENGTH` bits.
     type Bitstring: Clone + Debug;
     /// Enumeration of fixed bases used in endoscaling.
-    type FixedBases;
+    type FixedBases: Clone + Debug;
     /// The maximum number of bits that can be represented by [`Self::Bitstring`].
     /// When endoscaling with a base, each unique base can only support up to
     /// `MAX_BITSTRING_LENGTH` bits.

halo2_proofs/src/plonk.rs

@@ -107,6 +107,16 @@ impl<C: CurveAffine> VerifyingKey<C> {
             cs: self.cs.pinned(),
         }
     }
+
+    /// Returns the ConstraintSystem.
+    pub fn cs(&self) -> &ConstraintSystem<C::Scalar> {
+        &self.cs
+    }
+
+    /// Returns the transcript_repr
+    pub fn transcript_repr(&self) -> C::Scalar {
+        self.transcript_repr
+    }
 }
 
 /// Minimal representation of a verification key that can be used to identify

halo2_proofs/src/plonk/circuit.rs

@@ -1469,6 +1469,26 @@ impl<F: Field> ConstraintSystem<F> {
                 // and the interstitial values.)
             + 1 // for at least one row
     }
+
+    /// Returns num_fixed_columns
+    pub fn num_fixed_columns(&self) -> usize {
+        self.num_fixed_columns
+    }
+
+    /// Returns num_advice_columns
+    pub fn num_advice_columns(&self) -> usize {
+        self.num_advice_columns
+    }
+
+    /// Returns num_instance_columns
+    pub fn num_instance_columns(&self) -> usize {
+        self.num_instance_columns
+    }
+
+    /// Returns num_selectors
+    pub fn num_selectors(&self) -> usize {
+        self.num_selectors
+    }
 }
 
 /// Exposes the "virtual cells" that can be queried while creating a custom gate or lookup