Skip to content
This repository has been archived by the owner on Jul 5, 2024. It is now read-only.

Commit

Permalink
fix: modify assign function of LtChip to take Value<F> input instea…
Browse files Browse the repository at this point in the history
…d of `F` (#1456)

### Description

The PR modifies the assign function of the LtChip to take `Value<F>`
input instead of `F`. According to this discussion [Halo2 -
Discord](https://discord.com/channels/995022112811135148/1113747239534346250/1113854493646397621)
with @therealyingtong and @ed255, it emerged how the current design of
the chip makes its usage prone to bugs.

For example, this is how it is currently used in summa-solvency =>
https://github.com/summa-dev/summa-solvency/blob/a7d0c1f51c7e146bac2686c432c945ff6f3f063f/src/chips/merkle_sum_tree.rs#L338-L354

In order to extract `F` from an assigned cell, I need to create an if
conditional that performs the `assign` function only if a witness value
is Some. This is a problem as the assignment function won't be called
during keygen.

### Type of change

- [x] Bug fix (non-breaking change which fixes an issue)
- [ ] New feature (non-breaking change which adds functionality)
- [ ] Breaking change (fix or feature that would cause existing
functionality to not work as expected)
- [ ] This change requires a documentation update

### How Has This Been Tested?

`cargo test less_than`
  • Loading branch information
enricobottazzi authored Jun 6, 2023
1 parent 7b77f9c commit 06cce9f
Show file tree
Hide file tree
Showing 2 changed files with 36 additions and 15 deletions.
43 changes: 31 additions & 12 deletions gadgets/src/less_than.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@ pub trait LtInstruction<F: Field> {
&self,
region: &mut Region<'_, F>,
offset: usize,
lhs: F,
rhs: F,
lhs: Value<F>,
rhs: Value<F>,
) -> Result<(), Error>;

/// Load the u8 lookup table.
Expand Down Expand Up @@ -114,28 +114,37 @@ impl<F: Field, const N_BYTES: usize> LtInstruction<F> for LtChip<F, N_BYTES> {
&self,
region: &mut Region<'_, F>,
offset: usize,
lhs: F,
rhs: F,
lhs: Value<F>,
rhs: Value<F>,
) -> Result<(), Error> {
let config = self.config();

let lt = lhs < rhs;
let lt = lhs.zip(rhs).map(|(lhs, rhs)| lhs < rhs);

region.assign_advice(
|| "lt chip: lt",
config.lt,
offset,
|| Value::known(F::from(lt as u64)),
|| lt.map(|lt| F::from(lt as u64)),
)?;

let diff = (lhs - rhs) + (if lt { config.range } else { F::ZERO });
let diff_bytes = diff.to_repr();
let diff_bytes = diff_bytes.as_ref();
let diff_bytes = lhs.zip(rhs).map(|(lhs, rhs)| {
let mut diff = lhs - rhs;
let lt = lhs < rhs;
if lt {
diff += config.range;
} else {
diff += F::ZERO;
}
diff.to_repr()
});

for (idx, diff_column) in config.diff.iter().enumerate() {
region.assign_advice(
|| format!("lt chip: diff byte {}", idx),
*diff_column,
offset,
|| Value::known(F::from(diff_bytes[idx] as u64)),
|| diff_bytes.as_ref().map(|bytes| F::from(bytes[idx] as u64)),
)?;
}

Expand Down Expand Up @@ -323,7 +332,12 @@ mod test {
idx + 1,
|| Value::known(*value),
)?;
chip.assign(&mut region, idx + 1, value_prev, *value)?;
chip.assign(
&mut region,
idx + 1,
Value::known(value_prev),
Value::known(*value),
)?;

value_prev = *value;
}
Expand Down Expand Up @@ -448,7 +462,12 @@ mod test {
idx + 1,
|| Value::known(*value_b),
)?;
chip.assign(&mut region, idx + 1, *value_a, *value_b)?;
chip.assign(
&mut region,
idx + 1,
Value::known(*value_a),
Value::known(*value_b),
)?;
}

Ok(())
Expand Down
8 changes: 5 additions & 3 deletions zkevm-circuits/src/copy_circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -503,8 +503,10 @@ impl<F: Field> CopyCircuitConfig<F> {
lt_chip.assign(
region,
*offset,
F::from(copy_event.src_addr + u64::try_from(step_idx).unwrap() / 2u64),
F::from(copy_event.src_addr_end),
Value::known(F::from(
copy_event.src_addr + u64::try_from(step_idx).unwrap() / 2u64,
)),
Value::known(F::from(copy_event.src_addr_end)),
)?;
}

Expand Down Expand Up @@ -683,7 +685,7 @@ impl<F: Field> CopyCircuitConfig<F> {
// tag
tag_chip.assign(region, *offset, &CopyDataType::Padding)?;
// Assign LT gadget
lt_chip.assign(region, *offset, F::ZERO, F::ONE)?;
lt_chip.assign(region, *offset, Value::known(F::ZERO), Value::known(F::ONE))?;

*offset += 1;

Expand Down

0 comments on commit 06cce9f

Please sign in to comment.