Does Nova support local statements (public inputs) to step function F?

[featherin]

Hi there, thanks for this awesome project!

I am trying to build a circuit that computes the digest of a long string, which is done via recursively absorbing new data chunks into existing state. That is, $h := H(\cdots H(H(s, x_1), x_2) \cdots, x_n)$, where $x_1, \cdots, x_n$ are supposed to be statements (i.e., public inputs).

However, it seemed that Nova didn't not allow passing local statements to the circuit in each step, as enforced in these lines. I also checked Nova's original paper, where the input to $F$ is solely the output of the previous round. The eprint 2023/969 paper includes auxiliary values in the IVC definition, but these values are secret witnesses if I understand correctly.

Is there any workaround to support my use case, where the step function takes additional local statements? Thanks!

[srinathsetty]

Hi @featherin, thanks for your interest in this project!

Your use-case is certainly supported. Here's how I would go about doing it:

• The arity in the step circuit is 1, to pass the digest of the state thus far to the next step.
• The step circuit allocates variables corresponding to x_i (these are not necessary to be secret, they are just auxiliary variables).
• The step circuit computes z_out as H(z_in, x_i) and return that as the output of the step circuit.

Does this make sense?

[srinathsetty]

Please see this example: https://github.com/microsoft/Nova/blob/main/examples/hashchain.rs

I'll be closing the issue. Please reopen if you have further questions.

[featherin]

Hi @srinathsetty, I appreciate your kind and prompt comments!

Yeah, your mentioned steps were exactly what I attempted to do, and consequently I obtained a circuit similar to the minimal reproducible example below ($H$ is replaced with a simple multiplication for clarity):

#[derive(Clone, Debug)]
struct FakeHashCircuit<G: Group> {
  x: G::Scalar,
}

impl<G: Group> StepCircuit<G::Scalar> for FakeHashCircuit<G> {
  fn arity(&self) -> usize {
    1
  }

  fn synthesize<CS: ConstraintSystem<G::Scalar>>(
    &self,
    cs: &mut CS,
    z: &[AllocatedNum<G::Scalar>],
  ) -> Result<Vec<AllocatedNum<G::Scalar>>, SynthesisError> {
    let z = z[0].clone();
    let x = AllocatedNum::alloc_input(cs.namespace(|| format!("x")), || Ok(self.x))?;

    z.mul(cs.namespace(|| format!("Compute H(z, x) = z * x")), &x)
      .map(|v| vec![v])
  }
}

However, PublicParams::setup will return Err(InvalidStepCircuitIO) on input an instance of FakeHashCircuit, which is due to the alloc_input IMO. Everything will work as expected when changing alloc_input to alloc.

The full example is in my gist, and please correct me if I misunderstood something😊

---Edit---

Wow, thanks a lot for the example! What I did is to call alloc_input in this line instead, but it complained with the aforementioned error :(

The reason I need these x to be public inputs is that in my use case, the long message is known by the verifier who wants to check the correctness of the hash computation (as well as some other subsequent operations) on the message. Sorry for failing to make it clear!

[srinathsetty]

Yes, we cannot use alloc_input within a step circuit.

If we need to make things public, one design pattern is to add everything that needs to be made public on to a hash chain. Then the verifier can get the tail of the hash chain from the Nova proof and then actual content from the prover out of band and check if they are consistent. Does this make sense?

[featherin]

Yeah, after several failing attempts, I think this is the only viable option for now... A huge thanks for your help anyway!