update usage sections to last interfaces

This commit is contained in:
arnaucube
2024-05-08 13:34:59 +02:00
parent 3114a3a152
commit d328ae7d16
4 changed files with 64 additions and 38 deletions

View File

@@ -30,7 +30,8 @@ let mut folding_scheme = NOVA::init(&prover_params, F_circuit, initial_state.clo
// compute a step of the IVC
for i in 0..num_steps {
let start = Instant::now();
folding_scheme.prove_step().unwrap();
// here we pass an empty vec since it does not use external_inputs
folding_scheme.prove_step(vec![]).unwrap();
println!("Nova::prove_step {}: {:?}", i, start.elapsed());
}

View File

@@ -22,7 +22,10 @@ impl<F: PrimeField> FCircuit<F> for CubicFCircuit<F> {
fn state_len(&self) -> usize {
1
}
fn step_native(&self, _i: usize, z_i: Vec<F>) -> Result<Vec<F>, Error> {
fn external_inputs_len(&self) -> usize {
0
}
fn step_native(&self, _i: usize, z_i: Vec<F>, _external_inputs: Vec<F>) -> Result<Vec<F>, Error> {
Ok(vec![z_i[0] * z_i[0] * z_i[0] + z_i[0] + F::from(5_u32)])
}
fn generate_step_constraints(
@@ -30,6 +33,7 @@ impl<F: PrimeField> FCircuit<F> for CubicFCircuit<F> {
cs: ConstraintSystemRef<F>,
_i: usize,
z_i: Vec<FpVar<F>>,
_external_inputs: Vec<FpVar<F>>,
) -> Result<Vec<FpVar<F>>, SynthesisError> {
let five = FpVar::<F>::new_constant(cs.clone(), F::from(5u32))?;
let z_i = z_i[0].clone();
@@ -70,10 +74,13 @@ impl<F: PrimeField> FCircuit<F> for MultiInputsFCircuit<F> {
fn state_len(&self) -> usize {
5 // This circuit has 5 inputs
}
fn external_inputs_len(&self) -> usize {
0
}
// Computes the next state values in place, assigning z_{i+1} into z_i, and computing the new z_{i+1}
// We want the `step_native` method to implement the same logic as the `generate_step_constraints` method
fn step_native(&self, _i: usize, z_i: Vec<F>) -> Result<Vec<F>, Error> {
fn step_native(&self, _i: usize, z_i: Vec<F>, _external_inputs: Vec<F>) -> Result<Vec<F>, Error> {
let a = z_i[0] + F::from(4_u32);
let b = z_i[1] + F::from(40_u32);
let c = z_i[2] * F::from(4_u32);
@@ -89,6 +96,7 @@ impl<F: PrimeField> FCircuit<F> for MultiInputsFCircuit<F> {
cs: ConstraintSystemRef<F>,
_i: usize,
z_i: Vec<FpVar<F>>,
_external_inputs: Vec<FpVar<F>>,
) -> Result<Vec<FpVar<F>>, SynthesisError> {
// Implementing the circuit constraints
let four = FpVar::<F>::new_constant(cs.clone(), F::from(4u32))?;
@@ -129,10 +137,13 @@ impl<F: PrimeField> FCircuit<F> for Sha256FCircuit<F> {
fn state_len(&self) -> usize {
1
}
fn external_inputs_len(&self) -> usize {
0
}
/// Computes the next state values in place, assigning z_{i+1} into z_i, and computing the new
/// z_{i+1}
fn step_native(&self, _i: usize, z_i: Vec<F>) -> Result<Vec<F>, Error> {
fn step_native(&self, _i: usize, z_i: Vec<F>, _external_inputs: Vec<F>) -> Result<Vec<F>, Error> {
let out_bytes = Sha256::evaluate(&(), z_i[0].into_bigint().to_bytes_le()).unwrap();
let out: Vec<F> = out_bytes.to_field_elements().unwrap();
@@ -145,6 +156,7 @@ impl<F: PrimeField> FCircuit<F> for Sha256FCircuit<F> {
_cs: ConstraintSystemRef<F>,
_i: usize,
z_i: Vec<FpVar<F>>,
_external_inputs: Vec<FpVar<F>>,
) -> Result<Vec<FpVar<F>>, SynthesisError> {
let unit_var = UnitVar::default();
let out_bytes = Sha256Gadget::evaluate(&unit_var, &z_i[0].to_bytes()?)?;
@@ -172,22 +184,20 @@ This is useful for example if we want to fold multiple verifications of signatur
where each F is:
w_i
│ ┌────────────────────┐
│ │FCircuit │
│ │ │
└────►│ h =Hash(z_i[0],w_i)│
│ │ =Hash(v, w_i) │
────────►│ │ ├───────►
z_i=[v,0] │ └──►z_{i+1}=[h, 0] │ z_{i+1}=[h,0]
│ │
└────────────────────┘
w_i
│ ┌────────────────────┐
│ │FCircuit │
│ │ │
└────►│ h =Hash(z_i[0],w_i)│
────────►│ │ ├───────►
z_i │ └──►z_{i+1}=[h] z_{i+1}
│ │
└────────────────────┘
```
where each $w_i$ value is set at the `external_inputs` array.
The last state $z_i$ is used together with the external input w_i as inputs to compute the new state $z_{i+1}$.
The function F will output the new state in an array of two elements, where the second element is a 0. In other words, $z_{i+1} = [F([z_i, w_i]), 0]$, and the 0 will be replaced by $w_{i+1}$ in the next iteration, so $z_{i+2} = [F([z_{i+1}, w_{i+1}]), 0]$.
```rust
#[derive(Clone, Debug)]
@@ -197,47 +207,48 @@ where
{
_f: PhantomData<F>,
poseidon_config: PoseidonConfig<F>,
external_inputs: Vec<F>,
}
impl<F: PrimeField> FCircuit<F> for ExternalInputsCircuits<F>
where
F: Absorb,
{
type Params = (PoseidonConfig<F>, Vec<F>); // where Vec<F> contains the external inputs
type Params = (PoseidonConfig<F>);
fn new(params: Self::Params) -> Self {
Self {
_f: PhantomData,
poseidon_config: params.0,
external_inputs: params.1,
}
}
fn state_len(&self) -> usize {
2
1
}
fn external_inputs_len(&self) -> usize {
1
}
/// computes the next state values in place, assigning z_{i+1} into z_i, and computing the new
/// computes the next state value for the step of F for the given z_i and external_inputs
/// z_{i+1}
fn step_native(&self, i: usize, z_i: Vec<F>) -> Result<Vec<F>, Error> {
let input: [F; 2] = [z_i[0], self.external_inputs[i]];
let h = CRH::<F>::evaluate(&self.poseidon_config, input).unwrap();
Ok(vec![h, F::zero()])
fn step_native(&self, i: usize, z_i: Vec<F>, external_inputs: Vec<F>) -> Result<Vec<F>, Error> {
let hash_input: [F; 2] = [z_i[0], external_inputs[0]];
let h = CRH::<F>::evaluate(&self.poseidon_config, hash_input).unwrap();
Ok(vec![h])
}
/// generates the constraints for the step of F for the given z_i
/// generates the constraints and returns the next state value for the step of F for the given
/// z_i and external_inputs
fn generate_step_constraints(
&self,
cs: ConstraintSystemRef<F>,
i: usize,
z_i: Vec<FpVar<F>>,
external_inputs: Vec<FpVar<F>>,
) -> Result<Vec<FpVar<F>>, SynthesisError> {
let crh_params =
CRHParametersVar::<F>::new_constant(cs.clone(), self.poseidon_config.clone())?;
let external_inputVar =
FpVar::<F>::new_witness(cs.clone(), || Ok(self.external_inputs[i])).unwrap();
let input: [FpVar<F>; 2] = [z_i[0].clone(), external_inputVar.clone()];
let h = CRHGadget::<F>::evaluate(&crh_params, &input)?;
Ok(vec![h, FpVar::<F>::zero()])
let hash_input: [FpVar<F>; 2] = [z_i[0].clone(), external_inputs[0].clone()];
let h = CRHGadget::<F>::evaluate(&crh_params, &hash_input)?;
Ok(vec![h])
}
}
```

View File

@@ -5,8 +5,11 @@ We can define the circuit to be folded in Circom. The only interface that we nee
```c
template FCircuit() {
signal input ivc_input[1];
signal output ivc_output[1];
signal input ivc_input[1]; // IVC state
signal input external_inputs[2]; // not state
signal output ivc_output[1]; // next IVC state
// [...]
}
component main {public [ivc_input]} = Example();
@@ -14,18 +17,23 @@ component main {public [ivc_input]} = Example();
The `ivc_input` is the array that defines the initial state, and the `ivc_output` is the array that defines the output state after the step.
So for example, the following circuit does the traditional example at each step, which proves knowledge of $x$ such that $y==x^3 + x + 5$ for a known $y$:
So for example, the following circuit does the traditional example at each step, which proves knowledge of $x$ such that $y==x^3 + x + e_0 + e_1$ for a known $y$ ($e_i$ are the `external_inputs[i]`):
```c
pragma circom 2.0.3;
template Example () {
signal input ivc_input[1];
signal output ivc_output[1];
signal temp;
signal input ivc_input[1]; // IVC state
signal input external_inputs[2]; // not state
signal output ivc_output[1]; // next IVC state
signal temp1;
signal temp2;
temp <== ivc_input[0] * ivc_input[0];
ivc_output[0] <== temp * ivc_input[0] + ivc_input[0] + 5;
temp1 <== ivc_input[0] * ivc_input[0];
temp2 <== ivc_input[0] * external_inputs[0];
ivc_output[0] <== temp1 * ivc_input[0] + temp2 + external_inputs[1];
}
component main {public [ivc_input]} = Example();

View File

@@ -20,6 +20,10 @@ pub trait FCircuit<F: PrimeField>: Clone + Debug {
/// Returns the number of elements in the state of the FCircuit, which corresponds to the
/// FCircuit inputs.
fn state_len(&self) -> usize;
/// returns the number of elements in the external inputs used by the FCircuit. External inputs
/// are optional, and in case no external inputs are used, this method should return 0.
fn external_inputs_len(&self) -> usize;
/// Computes the next state values in place, assigning z_{i+1} into z_i, and computing the new
/// z_{i+1}
@@ -29,6 +33,7 @@ pub trait FCircuit<F: PrimeField>: Clone + Debug {
&self,
i: usize,
z_i: Vec<F>,
external_inputs: Vec<F>, // inputs that are not part of the state
) -> Result<Vec<F>, Error>;
/// Generates the constraints for the step of F for the given z_i
@@ -39,6 +44,7 @@ pub trait FCircuit<F: PrimeField>: Clone + Debug {
cs: ConstraintSystemRef<F>,
i: usize,
z_i: Vec<FpVar<F>>,
external_inputs: Vec<FpVar<F>>, // inputs that are not part of the state
) -> Result<Vec<FpVar<F>>, SynthesisError>;
}
```