Skip to content

Commit

Permalink
Fix failing assertion in witgen (#2120)
Browse files Browse the repository at this point in the history
When writing #2119, I came across another issue in witgen. When running
this file on `main`:

```rs
namespace main(4);

    // Two bit-constrained witness columns
    // In practice, bit1 is always one (but this is not constrained)
    col witness bit1(i) query Query::Hint(1);
    col witness bit2;
    bit1 * (bit1 - 1) = 0;
    bit2 * (bit2 - 1) = 0;

    // Constrain their sum to be binary as well.
    // This ensures that at most one of the two bits is set.
    // Therefore, bit2 is always zero.
    let bit_sum;
    bit_sum = bit1 + bit2;
    bit_sum * (bit_sum - 1) = 0;

    // Some witness that depends on bit2.
    col witness foo;
    foo = bit2 * 42 + (1 - bit2) * 43;
```

I'm getting
```
thread 'main' panicked at /Users/georg/coding/powdr/executor/src/witgen/global_constraints.rs:258:17:
assertion failed: known_constraints.insert(p, RangeConstraint::from_max_bit(0)).is_none()
```

This is because when it sees the binary range constraint `bit_sum *
(bit_sum - 1) = 0`, it already figured out that `bit_sum` can be at most
`1` because of `bit_sum = bit1 + bit2`.

This PR fixes it.
  • Loading branch information
georgwiese authored Nov 20, 2024
1 parent e009331 commit 8b38138
Showing 1 changed file with 14 additions and 11 deletions.
25 changes: 14 additions & 11 deletions executor/src/witgen/global_constraints.rs
Original file line number Diff line number Diff line change
Expand Up @@ -241,6 +241,17 @@ fn process_fixed_column<T: FieldElement>(fixed: &[T]) -> Option<(RangeConstraint
Some((RangeConstraint::from_mask(mask), false))
}

fn add_constraint<T: FieldElement>(
known_constraints: &mut BTreeMap<PolyID, RangeConstraint<T>>,
poly_id: PolyID,
constraint: RangeConstraint<T>,
) {
known_constraints
.entry(poly_id)
.and_modify(|existing| *existing = existing.conjunction(&constraint))
.or_insert(constraint);
}

/// Deduces new range constraints on witness columns from constraints on fixed columns
/// and identities. Note that these constraints hold globally, i.e. for all rows.
/// If the returned flag is true, the identity can be removed, because it contains
Expand All @@ -255,20 +266,15 @@ fn propagate_constraints<T: FieldElement>(
match identity {
Identity::Polynomial(identity) => {
if let Some(p) = is_binary_constraint(intermediate_definitions, &identity.expression) {
assert!(known_constraints
.insert(p, RangeConstraint::from_max_bit(0))
.is_none());
add_constraint(known_constraints, p, RangeConstraint::from_max_bit(0));
true
} else {
for (p, c) in try_transfer_constraints(
intermediate_definitions,
&identity.expression,
known_constraints,
) {
known_constraints
.entry(p)
.and_modify(|existing| *existing = existing.conjunction(&c))
.or_insert(c);
add_constraint(known_constraints, p, c);
}
false
}
Expand All @@ -287,10 +293,7 @@ fn propagate_constraints<T: FieldElement>(
(try_to_simple_poly(left), try_to_simple_poly(right))
{
if let Some(constraint) = known_constraints.get(&right.poly_id).cloned() {
known_constraints
.entry(left.poly_id)
.and_modify(|existing| *existing = existing.conjunction(&constraint))
.or_insert(constraint);
add_constraint(known_constraints, left.poly_id, constraint);
}
}
}
Expand Down

0 comments on commit 8b38138

Please sign in to comment.