snarkify / sirius

A Plonkish folding framework for Incrementally Verifiable Computation (IVC).
MIT License
120 stars 17 forks source link

Add StepCircuit support #12

Closed chaosma closed 8 months ago

chaosma commented 1 year ago

Our goal is to make the integration of existing halo2 circuit easy. The developer still need to some minimal modifications in order to use folding scheme.

To prepare for step circuit integration, the developer has to make necessary modification to existing circuit or design a new circuit that follows conventions: (1) the input and output of step circuit to be the same shape: z_in.len()=z_out.len(). (2) Do not expose z_in, z_out to halo2 instance column. Instead, z_in, z_out are allocated in advice columns and will be hashed into public IO of the IVC circuit. (3) The layout of the IVC circuit looks like StepCircuit IVCAuxCircuit
... ...

In practice, they will share the same cs: ConstraintSystem and each of them have individual halo2 table space.

We follow the similar trait as defined in Nova's library:

/// refer to: halo2_proofs/src/plonk/circuit.rs: Circuit trait
pub trait StepCircuit<F: PrimeField>: Circuit {
  type Config: Clone;  

  /// Return the the number of inputs or outputs of each step
  /// (this method is called only at circuit synthesis time)
  /// `synthesize` and `output` methods are expected to take as
  /// input a vector of size equal to arity and output a vector of size equal to arity
  fn arity(&self) -> usize;

  /// configure the step circuit, it will create necessary fixed columns and advice columns, 
  /// but NO instance column
  fn configure(cs: &mut ConstraintSystem<F>) -> Self::Config;

  /// Sythesize the circuit for a computation step and return variable
  /// that corresponds to the output of the step z_{i+1}
  /// this method will be called when we synthesize the IVC_Circuit
  fn synthesize(
    &self,
    cs: &mut ConstraintSystem<F>,
    z: &[AssignedCell<F, F>],
  ) -> Result<Vec<AssignedCell<F, F>>, SynthesisError>;

  /// return the output of the step when provided with the step's input
  fn output(&self, z: &[F]) -> Vec<F>;
}
drouyang commented 1 year ago

We should invite boarder review since this is an user facing interface

cyphersnake commented 1 year ago
cyphersnake commented 1 year ago

https://github.com/axiom-crypto/halo2-lib/tree/feat/zkevm-sha256/hashes/zkevm/src/sha256