Compile to Halo2 middleware

[alxkzmn]

Switching to a more recent Halo2 version revealed a problem with our lookups - they don't pass a lookup-any-sanity-checks because they are using only the fixed query. This is why I had to disable the default features of all halo2 crates (that include lookup-any-sanity-checks) and only enable the rest. I suppose we can refactor our lookups to use lookup instead of lookup_any.

[leolara]

@alxkzmn something that for me is important is to check that we can use the "mock prover" for the new middleware that @ed255 mentioned. Can you check that we can use that and that we get the information we need to find bugs in circuits.

[alxkzmn]

Sure

[leolara]

I think this could be pub(super) and being called from a method in the result of the plonkish compilation. That method could be added here in a pub trait, so in the future with several packages you don't depend on halo2 if you don't need it.

I think this should return a struct instead of a touple, and to interact with this result calling methods.

[leolara]

Perhaps we can see if k is something we can calculate from the number of rows in the plonkish compilation.

[alxkzmn]

By result of the plonkish compilation do you mean the result of compile() that is currently a tuple of (Circuit,Option<AssignmentGenerator>)?

[leolara]

Yes, is it possible to change the result of plonkish::compile to don't be a tuple?

Then add a trait that has a method that returns the halo2 compilation.

Then the return of the halo2 compilation is a struct with methods instead of a long tuble?

[alxkzmn]

@leolara regarding the debug prover - according to Edu it is already doing the job. Here's the information he provided: the new check_witness function and the example. I'll wait until it's merged into main. I think it's safe to remove the fronted references already. Some of the remaining frontend code is preventing me from refactoring the changes in a better way.

[leolara]

@alxkzmn I know that it is impossible that two people name things the same, but I always use get_ to obtain things that are already calculated as something that is going to be called many times every time I want a value. not for something that is acually running things.

perhaps to_halo2() could be good, a get_preprocessing, just preprocessing. This is not important, really.

[leolara]

@alxkzmn why does setup needs args I thought one of the advantes of this is that we could get the setup without wittness and then pass the witness to the prover

[leolara]

@alxkzmn we have already this rng when we are doing the setup? could this one be different that the one we pass to setup?

Also, why a hashmap of assignments instead of an assignment? For the super circuit? What do you think is the best interface for this?

[leolara]

Perhaps there could be Halo2Setup and Halo2SetupSuperCircuit. with the first one accepting Assignments as witness and the second one accepting the result of doing the mapping?

[alxkzmn]

@leolara ready for review, fixed everything. Regarding inferring the k - there's no information on the number of rows in the plonkish compilation itself or the supercircuit. It only becomes available after we actually generate the witness, implying that we would need the witness for the setup phase. I can try to implement it if it sounds good to you.

[leolara]

@alxkzmn i guess the prints in the library you are going to remove them before merging, right? They are ok in the examples and tests, but a library cannot have prints

[leolara]

@alxkzmn num_rows is available in the compilation of plonkish but not put in the IR, it can be added to the IR trivially

[leolara]

@alxkzmn what you mean by refactor lookups in using lookup instead of lookup_any.

In plonkish IR the lookups are:

pub lookups: Vec<PolyLookup<F>>,

We should ignore 100% how the previous halo2 frontend was used. And create a new backend that goes to the halo2 middleware.

[leolara]

@alxkzmn shouldn't this be a method of the plonkish::ir::SuperCircuit? because how do you get to ChiquitoHalo2SuperCircuit otherwise?

Also, I don't know how can be only one Halo2Setup, as the witness for one is an assigment and for other is a mapping of assignments?

[alxkzmn]

I understand your concern about the extra HashMap creation for a single circuit and I will try to fix it. There will be two separate implementations as you suggested. However, Halo2Setup does not include witness, so I don't see a problem here. I believe that it is nice to encapsulate a few things that Halo2 needs regardless of where they are coming. Specifically, CosntraintSystem, Params, PK and VK can live together in a struct.

[alxkzmn]

Zooming out, I realized that a better approach could be to only expose a new trait for SuperCircuit<F, MappingArgs> - something like SuperCircuitHalo2Prover that has generate_proof(), and a similar trait Halo2Prover for the PlonkishCompilationResult. This way, the witness will stay inside the plonkish::backend::halo2 all the time and the proof generation and verification would look like the following (by the example of or mimc7 circuit):

    let x_in_value = Fr::from_str_vartime("1").expect("expected a number");
    let k_value = Fr::from_str_vartime("2").expect("expected a number");

    let super_circuit = mimc7_super_circuit::<Fr>();
    let rng = BlockRng::new(DummyRng {});
    let (proof, instance, params, vk) = super_circuit.generate_proof(
      10 /*k, maybe unnecessary if possible to take from the num_rows*/,
      rng,
      (x_in_value, k_value) /*mapping_args*/, 
    )
    let result = halo2_verify(proof, params, vk, instance);

Additionally, halo2_verify(proof, params, vk, instance) can all be wrapped into a Halo2Verifier struct:

    let x_in_value = Fr::from_str_vartime("1").expect("expected a number");
    let k_value = Fr::from_str_vartime("2").expect("expected a number");

    let super_circuit = mimc7_super_circuit::<Fr>();
    let rng = BlockRng::new(DummyRng {});
    let halo2_verifier = super_circuit.generate_proof(
      10 /*k, maybe unnecessary if possible to take from the num_rows*/,
      rng,
      (x_in_value, k_value) /*mapping_args*/, 
    )
    let result = halo2_verifier.verify();

Does this look good to you?

[leolara]

We should talk about this. For example, you should not need to generate a proof to verify one.

[leolara]

Also, the args cannot be passed to the prover because you might want to generate a evil witness.

[alxkzmn]

In this case the witness could be calculated outside, and the verifier could always be constructed from scratch (not by the prover):

    let x_in_value = Fr::from_str_vartime("1").expect("expected a number");
    let k_value = Fr::from_str_vartime("2").expect("expected a number");

    let super_circuit = mimc7_super_circuit::<Fr>();
    let rng = BlockRng::new(DummyRng {});
    let witness = super_circuit.get_mapping().generate((x_in_value, k_value));
    let (proof, instance, params, vk) = super_circuit.generate_proof(
      10 /*k, maybe unnecessary if possible to take from the num_rows*/,
      rng,
      witness, 
    )
    //-----on the verifier side-------
    let verifier = Halo2Verifier::new(proof, instance, params, vk))
    let result = verifier.verify();

[alxkzmn]

Alternatively, if evil witness is only necessary for testing, we could expose a method to test-prove with evil witness:

    let x_in_value = Fr::from_str_vartime("1").expect("expected a number");
    let k_value = Fr::from_str_vartime("2").expect("expected a number");

    let super_circuit = mimc7_super_circuit::<Fr>();
    let rng = BlockRng::new(DummyRng {});
    let (proof, instance, params, vk) = super_circuit.generate_proof(
      10 /*k, maybe unnecessary if possible to take from the num_rows*/,
      rng,
    ).unwrap();

    let evil_witness = create_evil_witness();
    let failed_proof = super_circuit.test_evil_witness(
      10 /*k, maybe unnecessary if possible to take from the num_rows*/,
      rng,
      evil_witness
    );
    assert!(failed_proof.is_err());

    //-----on the verifier side-------
    let verifier = Halo2Verifier::new(proof, instance, params, vk))
    let result = verifier.verify();

[leolara]

@alxkzmn So let me sumarize my thoughts about the interface:

In the no super circuit scenario:

1. We start with a SBPIR object
2. it should have method to return a plonkish IR thing. I cannot have a method that do halo2 stuff directly because we need to give plonkish config at this step.
3. From the plonkishIR thing we should be able to compile to a halo2 thing, this step cannot be inside another one because we might need to give configuration to the halo2 compilation. This step does not require witness, and the result should have the proving and verifiying keys.
4. The halo2 thing, should have a method to generate a proof, to which we pass plonkish::Assignment. We cannot run the witness generation inside this because we might want to pass an evil witness.

With the Supercircuit in mind, we follow the same process starting with the plonkish::ir::SuperCircuit, and the "things" in the middle can be the same or different type. But the proving method in the halo2 thing should accept a plonkish:SuperAssignments object.

The verification it is correct how it is now, as we shouldn't need to compile anything or generate witness to verify a proof.

I think it is trivial to add num_rows to plonkish IR. Then if you can use that to automatically calculate the halo2 k that would be great.

Also the halo2 thingy needs accessors for the proving key, the verifying key, k, etc..

The previous halo2 backend is legacy code now, so feel free to refactor it, or throw it all away.

I think if there are more things, to avoid more cycles perhaps we should jump in a call.

[leolara]

I think this P should have trait, that in the end the only unbounded type is what is passed as witness. This way we could also create provers that take the args in the future.

trait Halo2Prover<W> {
    fn generate_proof(&self, W)
}

I think I mentioned this, but I don't think it is necessary to pass rng again to generate the proof when it is already passed for the compilation. Is there a reason?

Also, could you answer about the automatic k generation? isn't it log2 of nun_rows? perhaps @ed255 knows this.

[alxkzmn]

Please check this regarding the K: #263 (comment)
I think it will be relatively easy to implement as a log2 taking into account the ConstraintSystem.minimum_rows(), but this is out of scope of this refactoring as it could be done independently before. I'd like to keep the scope of this PR as small as possible and merge it ASAP.

[leolara]

ok, for another task is ok, sorry I didn't see that

[alxkzmn]

K could be derived from the number of rows before this refactoring, so I created a separate issue for that: #266
Also created a separate issue for the lookup refactoring: #267

[leolara]

@alxkzmn I am not sure why you are not using the SuperAssignments type, but it is approved, don't worry about it