Circuit is satisfied but plonk proof verification fails

[Schaeff]

Hi! I have the following test using the current tip of dev (09474a):

  #[test]
  fn setup_prove_verify() {
      // the program `def main(public field a) -> field { return a }`
      let program: Prog<Bn128Field> = Prog {
          arguments: vec![Parameter::public(Variable::new(0))],
          return_count: 1,
          statements: vec![Statement::constraint(Variable::new(0), Variable::public(0))],
      };

      // generate a dummy universal setup of size 2**10
      let crs: Crs<<Bn128Field as BellmanFieldExtensions>::BellmanEngine, CrsForMonomialForm> =
      Crs::<<Bn128Field as BellmanFieldExtensions>::BellmanEngine, CrsForMonomialForm>::dummy_crs(2usize.pow(10) as usize);

      // transpile
      let hints = transpile(Computation::without_witness(program.clone())).unwrap();

      // run a circuit specific (transparent) setup
      let pols = setup(Computation::without_witness(program.clone()), &hints).unwrap();

      // generate a verification key from the circuit specific setup and the crs
      let vk = make_verification_key(&pols, &crs).unwrap();

      // run the program
      let interpreter = Interpreter::default();

      // extract the witness
      let witness = interpreter
          .execute(program.clone(), &[Bn128Field::from(42)])
          .unwrap();

      // bundle the program and the witness together
      let computation = Computation::with_witness(program.clone(), witness);
      // transpile
      let hints = transpile(Computation::without_witness(program.clone())).unwrap();

      // check that the circuit is satisfied
      assert!(is_satisfied(computation.clone(), &hints).is_ok());

      // generate a proof with no setup precomputations and no init params for the transcript, using Blake2s
      let proof: BellmanProof<<Bn128Field as BellmanFieldExtensions>::BellmanEngine, PlonkCsWidth4WithNextStepParams> =
              prove_by_steps::<_, _, Blake2sTranscript<_>>(
                  computation,
                  &hints,
                  &pols,
                  None,
                  &crs,
                  None,
              )
              .unwrap();

      // verify the proof using Blake2s
      let ans = verify::<_, Blake2sTranscript<_>>(&proof, &vk).unwrap();

      // check that the proof is verified
      assert!(ans);
  }

I would have expected the proof to be verified correctly because the circuit is satisfied, but this test fails. I checked and it fails in the last check in verification.

Is there something I am doing wrong here? Thanks!

[shamatar]

As far as I remember "is_satisfied" doesn't verify that gate that is tied to public input allocation. In any case you can just put a breakpoint inside a "is_satisfied" function and see a gate number or relation that fails. You can also do the same in verification function and check whether polynomial equality on random point fails (which I would guess), or something more exotic

[Schaeff]

I see, I don't have time to dig into it now so here are some other programs I tried which fail:

// fails in `log2_floor`
def main() { 
   return; 
}

// fails in `z_2.add_assign_scaled` inside `second_step_from_first_step`
def main(private field a, private field b) { 
   assert(a == b);
   return; 
}

// fails in `z_2.add_assign_scaled` inside `second_step_from_first_step`
def main(private field a, private field b) { 
   assert(a * a == b);
   return; 
}

// proof generated but not verified
def main(private field a, private field b) { 
   assert(a * a == b);
   assert(a * a == b);
   return; 
}

I am not using any public variable except ~one in any of these.

[georgwiese]

Debugging the program, all I can see is that the very last verification check fails, not sure how to go from there.

@shamatar Could you point me to a minimal working example going from a Circuit to a verified Plonk proof? Then I'd take it from there.

[shamatar]

Hey George.

There is a test, cargo test --release -- --nocapture test_prove_trivial_circuit that passes on my machine. I can see potential problems as:

• you are using better_cs subfolder implementation that is legacy and is more about the time when we transitioned form R1CS into Plonk arithmetization using transpiler. It works well in zkSync1 (actually using beta branch), but it's anyway legacy
• if you are using non-multithreaded implementation then it may contain problems by itself. Such case was never interesting for us, and while implementations are written such they should not depend on number of worker cores, it was never a focus point

I'm neglecting any trivial cases like if you used different trusted setups for VK and proving. The test above generates trusted setup as powers of 42, but it's not important for that test