Standalone circuit tools

[CeciliaZ030]

Make Circuit-tools a standalone repo that has components & APIs to support Halo2 development.

The current Halo2 APIs apply constraints within Gate which defines expression across polynomial columns, and assign circuit with Region which are independent areas that resembles integrated chip design. However, these features are not fine-grained enough for zkevm development which requires controls over specific cells. In addition, the two-phase process are separated from each other, and no current tools exists to leverage constraints defined in configuration phase to speed up the assignment phase.

Thus we came up with a bucket of toolkits to fill in the blank as we work on the #39 MPT circuit. The toolkits mimics RAM and ROM assess with Cell and Lookup, aiming to exploit the full expressive power of PLONKish arithemetization. The Circuit-tools include:

CellManager

• allow user to specify usage of columns such as cell_type, num_columns, phase, and permutable, then init the section according to CellConfig<C: CellType>.
• allow user to query cells based on their usage, for example obtaining a cell for a phase2, or N cells for byte range check.
• dynamically select the context with the maximum cells being used, with branching scenario like ifx! and matchx!.

circuit! macros

• captures meta: &mut VirtualCells<F> and cb: ConstraintBuilder<F, T> for inner code to call Halo2 APIs,
• query Fixed, Advice, and Any Column from meta captured (f!, a!, and x!).
• provide branching logic by pushing conditions into the constraint builder (ifx!, elsex!, and matchx! ), incorporates CellManager's context to optimize cell allocation.
• require! can enforce equality between $lhs and $rhs, constrain a value to be boolean, or even perform lookups with intuitive syntax sugar (require!((a, b) => @KECCAK).

MemoryBank

• the declaration of a MemoryBank basically initiate Advice lookups into itself to encode R/W logic as part of the proof. It also contains a columns to enforce R/W operations happen at expected place.
• during configuration, store(values: &[Expression<F>]) puts lookup table tuples into cb (resembling memory write), while load(values: &[Expression<F>]) should use the exact same tuples as lookup data (resembling memory read). Proving that stored expressions exist in loaded expression at expected rows would prove R/W correctness.
• during assignment, witness_store(offset: usize, values: &[F]) in fact cached the witness tuple in MemoryBank (instead of assigning it to Cells) and record the stored row index, then witness_load(offset: usize, values: &[F]) takes out those previously cached values and finally assign them to satisfy the self-lookup constraints.
• the assign() function of 'MemoryBank' itself should be call at the end stage of entire circuit assignment, this will write down the recorded row index at Read time into Bank's Advice column.

CachedRegion

• at assignment, it keeps a duplicate of managed Region with Vec<Vec<T>> so when user put for instance Value::known(3) in Cell A and Value::known(7) in Cell B with constraint A + BB = C, then we can get 3 and 7 out from the CachedRegion and evaluate the stored constraint as 3 + 7*7 = 52 to assign Cell C.
• the stored constraint is called StoreExpression at config time. It's mostly used for lookups in the evm_circuit, because the evm_circuit first combine lookup tuple into rlc corresponding to table values that are also combined as rlc, so that we only has one CellType::Lookup to lookup SomeTable.

[Arrefamm]

circuit tools #123

[psix1219king]

This code provides a basic structure and methods for managing cells, memory, and cached regions within the Circuit-tools project. Actual implementation will depend on specific project requirements and architecture.

// Example structure for managing cells
struct CellManager {
// Implementation of the structure
}

impl CellManager {
/// Initializes a section according to cell configuration.
fn init_section(&mut self, cell_type: CellType, num_columns: usize, phase: Phase, permutable: bool) {
// Implementation of the method
}

/// Queries cells based on their usage.
fn query_cells(&self, usage: Usage, count: usize) -> Vec<Cell> {
    // Implementation of the method
}

/// Dynamically selects context and optimizes cell allocation.
fn select_context(&self) {
    // Implementation of the method
}

}

// Example circuit! macros for providing branching logic and optimizing cell allocation
macro_rules! circuit {
// Implementation of the macros
}

// Example structure MemoryBank for memory management
struct MemoryBank {
// Implementation of the structure
}

impl MemoryBank {
/// Stores values in memory.
fn store(&mut self, values: &[Expression]) {
// Implementation of the method
}

/// Loads values from memory.
fn load(&mut self, values: &[Expression<F>]) {
    // Implementation of the method
}

/// Witnesses values in memory.
fn witness(&mut self, offset: usize, values: &[F]) {
    // Implementation of the method
}

}

// Example structure CachedRegion for caching region data
struct CachedRegion {
// Implementation of the structure
}

impl CachedRegion {
/// Caches region data.
fn cache(&mut self, region: Region) {
// Implementation of the method
}

/// Evaluates cached constraint.
fn evaluate_cached_constraint(&self, cell_a: Cell, cell_b: Cell, cell_c: Cell) -> ConstraintResult {
    // Implementation of the method
}

}