ethan-000/halo2_backend

halo2_backend's Issues

refactor code to four crates

dynamic configuration

Ideally, we want to configure the circuit based on the opcodes required.

For example, if the circuit doesn't use ecdsa opcode there's no need to configure ecdsa.

currently the configure function of the Circuit trait in halo2 doesn't take self, so it doesn't have access to the fields of the struct (NoirHalo2Translator). I'm wondering if theres a way around this.

Adding table for readme

Problem

Want to add table for feature-list. Easier and more space efficient to look at.

Happy Case

Written using markdown (example for reference).

features	halo2-pse	halo2-axiom
feature X	supported	supported
feature Y	supported	not supported
feature Z	not supported	supported

Alternatives Considered

No response

Additional Context

No response

Would you like to submit a PR for this Issue?

Yes

Support Needs

No response

Axiom Equality Constraints

Given requirements for interoperating between axiom gate chips and standard halo2 chips (given with example of keccak rather than StandardPlonk, but same process):

• Do halo2-lib computations, make calls to KeccakChip to have keccak do witness generation, return all witness cells to be assigned in keccak part of the arithmetization
• Actually assign keccak part in vanilla halo2, returning AssignedCells: https://github.com/axiom-crypto/axiom-eth/blob/6d2a4acf559a8716b867a715f3acfab745fbad3f/src/keccak/mod.rs#LL751C35-L751C35
• Need to do some tricks to convert AssignedCells to AssignedValues (basically just some way to make copy constraints between halo2-lib and keccak cells): https://github.com/axiom-crypto/axiom-eth/blob/6d2a4acf559a8716b867a715f3acfab745fbad3f/src/keccak/mod.rs#L423
• Now assign halo2-lib AssignedValues into vanilla halo2, where it already has access to the assigned keccak cells, so it can do copy constraints appropriately: https://github.com/axiom-crypto/axiom-eth/blob/6d2a4acf559a8716b867a715f3acfab745fbad3f/src/keccak/mod.rs#LL778C18-L778C18

Likely requires a custom thread builder!

MockProver Tests

It would be ideal to verify the authenticity of Halo2 circuits natively. We should run MockProver against generated circuits to verify their outputs. One issue is that the witness solver will fail to generate values that cause the circuit to fail. Therefore, to fully ensure that circuits behave in the expected case for each of the examples/ tests, we will need to have custom witness maps that will cause the halo2 prover to fail.

change transcript path

#2 (review)

keccak

noir-lang/acvm#315

Map Witnesses to Assigned Cells (for instance values & permutations)

BTreeMap of Witness to a vector of AssignedCell structs.

For public IO:
If noir circuit has public inputs and/or return values add a single instance column. At end of proof synthesis iterate through public inputs/ outputs and constrain values to be instance values. Use index of public inputs (then num public inputs + index of public output) to determine row of instance column to assign

For equality constraints:
Idea WIP - when assigning advice, check if witness already has cell assignment. If assignments >= 1 constrain current assignment to be equal to previously assigned cell instead of assigning witness from OpCode

ecdsa

issue with rust-toolchain. can only run on rust 2022-10-28. not compatible with noir front end rust 1.66

Axiom Arithmetic Constraints not working

I tried randomly assigning the witnesses for arithmetic constraints in Axiom and the proof verifies always.

but PSE seems to constrain correctly (incorrectly setting a/b/c will cause verification to fail)

This already needs to be refactored slightly to use Axiom's contexts in order to support QuantumCells across all witnesses which is needed for equality constraints, will update with more diagnostics/ solution