Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix some typos in README #2

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Fix some typos in README #2

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 9 additions & 9 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
# circuit-tools
A lightweit SDK for Halo2 frontend circuit.
A lightweight SDK for Halo2 frontend circuit.
## Features
### Logic: Constraint Builder
Leverage Rust's macro to construct conditional constraints based on execution branching. Build all constraints in on step with Halo2's gate.
Expand All @@ -10,9 +10,9 @@ meta.create_gate("Test", |meta| {
circuit!([meta, cb], {
ifx!(f!(q_enable) => {
ifx!{a!(a) => {
require!(a!(res) => a!(b) + f!(c));
require!(a!(res) => a!(b) + f!(c));
} elsex {
require!(a!(res) => a!(b) + c!(r));
require!(a!(res) => a!(b) + c!(r));
}};
});
});
Expand All @@ -38,7 +38,7 @@ require!((a.expr(), b.expr()) =>> @TestCellType::Lookup);

```
### Memory: Dynamic Lookup
Abstraction over using dynamic lookup to prove RW access in RAM. Stores to dynamic table to resemble WRITE and add lookups to represent READ. Lookup operation `(idx, r0, r1) => (rdx, w0, w1)` returns true if and only if the prover access the writen data at anticipated position correctly.
Abstraction over using dynamic lookup to prove RW access in RAM. Stores to dynamic table to resemble WRITE and add lookups to represent READ. Lookup operation `(idx, r0, r1) => (rdx, w0, w1)` returns true if and only if the prover access the written data at anticipated position correctly.
```
let mut memory = Memory::new();
memory.add_rw(meta, &mut cb.base, &mut state_cm, MyCellType::Mem1, 1);
Expand All @@ -56,11 +56,11 @@ register1.load(cb, &[a0, b1]);

```
### Assignment: Cached Region
Used to backtrack the intermediate cells queried in by Constrinat Builder during degree reduction. After `a * b * (c + d)` being split into `x = a * b` and `y = c + d`, the system need to account for the assignment of intermediate cells `x` and `y` while the prover only need to assign `a, b, c, d` based on the execution trace. Hence, Cached Region iterates over all stored expressions and recursively find the prover's assignment to calculate the intermediate values.
Used to backtrack the intermediate cells queried in by Constraint Builder during degree reduction. After `a * b * (c + d)` being split into `x = a * b` and `y = c + d`, the system need to account for the assignment of intermediate cells `x` and `y` while the prover only need to assign `a, b, c, d` based on the execution trace. Hence, Cached Region iterates over all stored expressions and recursively find the prover's assignment to calculate the intermediate values.
```
layouter.get_challenge(self.rand).map(|r| r1 = r);
layouter.assign_region(
|| "Test",
|| "Test",
|mut region| {
let mut region = CachedRegion::new(&mut region, 0.scalar());
region.push_region(0, 0);
Expand All @@ -76,7 +76,7 @@ layouter.assign_region(
)
```
## Workflow
Must specify cell type that implement trait `CellType` to satisfy the generic argument of `ConstraintBuilder<F, C: CellType>`. Can also declear a `TableType` to tag corresponding table for column-to-table lookups.
Must specify cell type that implement trait `CellType` to satisfy the generic argument of `ConstraintBuilder<F, C: CellType>`. Can also declare a `TableType` to tag corresponding table for column-to-table lookups.
```
pub enum TableTag {
Fixed,
Expand Down Expand Up @@ -108,7 +108,7 @@ impl Default for TestCellType {
fn default() -> Self {Self::StoragePhase1}
}
```
Initialize the Constraint Builder and Cell Manager with optional challenge that's used in RLC to conbime multi-columns lookups. The Cell Manager needs a max height and this is usually the height of your Halo2 gate; a offset is also needed to query cell from columns. Offset should be set to 0 in usual case. Load fixed table in to Constraint Builder with corresponding tag and initialized columns with the cell manager with `(cell_type: MyCellType, phase: u8, permuation: bool, num: usize)`.
Initialize the Constraint Builder and Cell Manager with optional challenge that's used in RLC to combine multi-columns lookups. The Cell Manager needs a max height and this is usually the height of your Halo2 gate; a offset is also needed to query cell from columns. Offset should be set to 0 in usual case. Load fixed table in to Constraint Builder with corresponding tag and initialized columns with the cell manager with `(cell_type: MyCellType, phase: u8, permuation: bool, num: usize)`.
```
let mut cm = CellManager::new(5, 0);
let mut cb: ConstraintBuilder<F, TestCellType> = ConstraintBuilder::new(4, Some(cm), Some(challenge));
Expand All @@ -126,4 +126,4 @@ meta.create_gate("Test", |meta| {
});
cb.build_lookups(meta);
```
Finally in assingment, initialize `CachedRegion` as demonstrated above and use it to assign values.
Finally in assignment, initialize `CachedRegion` as demonstrated above and use it to assign values.