powdr-labs / powdr

A modular stack for zkVMs, with a focus on productivity, security and performance.
Apache License 2.0
329 stars 65 forks source link

Witgen: Range constraints not transferred for machine-to-machine call #1382

Closed georgwiese closed 3 days ago

georgwiese commented 2 weeks ago

Currently, our Machine trait defines this function:

    fn process_plookup<'b, Q: QueryCallback<T>>(
        &mut self,
        mutable_state: &'b mut MutableState<'a, 'b, T, Q>,
        identity_id: u64,
        args: &[AffineExpression<&'a AlgebraicReference, T>],
    ) -> EvalResult<'a, T>;

where args includes actual arguments, but also where to write the results are written to.

If you have a call like this: {a1 + 256 * a2, b1 + 256 * b2, c1 + 256 * c2} is { XOR.a, XOR.b, XOR.c } assuming all columns on the LHS are range-constrained to be bytes, the solve_with_range_constraints() function can figure out the values of c1 and c2. This already works, if c1 and c2 are globally range constrained (e.g. there is a constraint {c1} in BYTES).

But the range constraints are not global (e.g. because we do some fancy tricks to save lookups), these range constraints are not passed to the called machine.

georgwiese commented 2 weeks ago

This is fixed by b1a07bd9a708e37deed42efe1be188d1682a84c2. Still need to open a (separate) PR.