Integrate ecc ops and databus into check_circuit #842
Assignees
Comments
|
From discussion with @ledwards2225 makes sense to do this when work on databus has been completed since there might be changes to the current structure (e.g. we might have multiple calldata columns) so moving to Next Up |
ledwards2225
added a commit
to AztecProtocol/aztec-packages
that referenced
this issue
Apr 9, 2024
Introduces a `stdlib::DataBus` class to facilitate calldata/return_data
reads/writes. The work also includes:
- Circuit checker functionality for checking the validity of databus
read gates (simply checks whether the {idx, value} pair in the gate
corresponds to data in the corresponding bus vector). Closes
AztecProtocol/barretenberg#842
- Tests for the stdlib DataBus (including failure tests and
demonstration of check circuit)
- Minor updates to the builder notion of DataBus; now an array of
`BusVector`s to improve interface from stdlib
AztecBot
pushed a commit
that referenced
this issue
Apr 10, 2024
Introduces a `stdlib::DataBus` class to facilitate calldata/return_data
reads/writes. The work also includes:
- Circuit checker functionality for checking the validity of databus
read gates (simply checks whether the {idx, value} pair in the gate
corresponds to data in the corresponding bus vector). Closes
#842
- Tests for the stdlib DataBus (including failure tests and
demonstration of check circuit)
- Minor updates to the builder notion of DataBus; now an array of
`BusVector`s to improve interface from stdlib
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
check_circuit()is incomplete for the UltraGoblinCircuitBuilder because it does not check the goblin ecc op gates or the databus lookup gates. For this reason, various tests utilizing the UG arithmetization must construct and verify full proofs to be complete.Note: Its not clear what this should look like for goblin ecc ops since UGH only checks two things here: that the ecc op wire columns match the wire values at the start of the exec trace, and also that the ecc op wires are zero outside of that block. Neither of these checks really make sense at the builder stage since this structure doesn't arise until the Composer stage. Still, there may be some basic sanity checks to be performed.
Edit: expanding on my previous comments above:
For Goblin ecc ops: There's nothing to check here. The only structure imposed by the UGH proof is that introduced in the "composer" stage, i.e. the duplication of the ecc op wires across columns. Checking the correctness of the underlying ops would be misleading since invalid ops would not cause verification of the UGH proof to fail.
For databus lookups: We cant check the actual databus lookup relation since it depends on polynomials computed by the prover (similar to the conventional lookup relation). We currently check conventional lookups in CircuitChecker by simply ensuring that the lookup gates are present in the set of tables used in the circuit. (See e.g.
LookupHashTable). We could do something similar for the databus: check that the "read" gates contain data present in the databus columns.The text was updated successfully, but these errors were encountered: