Linear constraint remover #2425
Conversation
Depends on #2426. With this PR, we use the annotations added in #2412 and #2426 to find the columns being generated. This allows us to detect when the folded payload is not persisted as a witness column. The background is that @Schaeff is working on #2425, which would undo persisting the folded payloads in some cases, allowing us to spend fewer witness columns per bus interaction. With this PR, this should be fine: The column type will change from witness to intermediate, which means that the bus witgen will not output any folded columns. It can be tested by changing the `materialize_folded` bool to `false`, e.g. [here](https://github.com/powdr-labs/powdr/blob/e77d3801c1decff039fd0ec6bbeb55ed734357fb/std/protocols/bus.asm#L48) and running: ``` cargo run pil test_data/asm/block_to_block.asm \ -o output -f --linker-mode bus --prove-with mock --field gl ``` This used to fail before this PR.
| // We require `left` to be a single, non-shifted, witness column `w` | ||
| let w = if let AlgebraicExpression::Reference( | ||
| r @ AlgebraicReference { | ||
| poly_id: | ||
| PolyID { | ||
| ptype: PolynomialType::Committed, | ||
| .. | ||
| }, | ||
| next: false, | ||
| .. | ||
| }, | ||
| ) = left.as_ref() | ||
| { | ||
| r | ||
| } else { | ||
| return None; | ||
| }; | ||
|
|
||
| // we require `y` to be a multi-linear expression over non-shifted columns | ||
| if right.contains_next_ref(intermediate_columns) | ||
| || right.degree_with_cache(intermediate_columns, &mut Default::default()) != 1 | ||
| { | ||
| return None; | ||
| } | ||
|
|
||
| // we require `y` not to be a single, non-shifted, witness column, because this case is already covered and does not require an intermediate column | ||
| // TODO: maybe we should avoid this edge case by removing the other optimizer, see xxx | ||
| if matches!( | ||
| right.as_ref(), | ||
| AlgebraicExpression::Reference(AlgebraicReference { | ||
| poly_id: PolyID { | ||
| ptype: PolynomialType::Committed, | ||
| .. | ||
| }, | ||
| next: false, | ||
| .. | ||
| }) | ||
| ) { | ||
| return None; | ||
| } |
There was a problem hiding this comment.
I'm a bit confused by this chunk. It seems that we have opposite requirements for left and right being a single, non-shifted, witness column AND also no requirements for left being a multi-linear expression. In practice, shouldn't we have both left and right be single and non shifted multilinear expression OR witness column?
There was a problem hiding this comment.
The current pattern is:
w = lin
where w is a non shifted witness column and lin is a multilinear expression over non-shifted columns.
Additionally, we require lin NOT to be a single non shifted column, because we already have another optimizer for this case that we don't want to interfere with here.
Are you suggesting that we could also support lin = w with the same requirements?
| ( | ||
| index, | ||
| ( | ||
| (name.clone(), *old_poly_id), |
There was a problem hiding this comment.
Because these are used to substitute polynomials, does it mean that neither name nor poly_id uniquely defines a polynomial and we have to use both? What was the reason we didn't define a unique poly_id initially?
There was a problem hiding this comment.
The reason is legacy code from polygon where the ids are per column type.
| X = one * (X_b1 + X_b2 * 0x100); | ||
| R = one * (R_b1 + R_b2 * 0x100); |
There was a problem hiding this comment.
Is there a way to force materializing a witness column instead of multiplying by one here? If X and R are exposed as an operation here, will they still be optimized away?
There was a problem hiding this comment.
Both having a way to block the optimizer and #2464 seem overkill just to fix a test. In practice the quotient and remainder do turn out to be single witness columns, it's the simplicity of this example which makes it fail due to inlining, so the one trick seems acceptable to me, similar to other tests here.
There was a problem hiding this comment.
Could we add a comment here to explain that we don't want to be optimized away? Otherwise I think this example could be confusing to first time readers.
| .flat_map(|pil| pil.identities.iter()) | ||
| .flat_map(|identity| identity.all_children()) | ||
| .flat_map(|pil| { | ||
| pil.identities | ||
| .iter() | ||
| .flat_map(|identity| identity.all_children()) | ||
| .chain( | ||
| // Note: we iterate on a `HashMap` so the ordering is not guaranteed, but this is ok since we're building another map. | ||
| pil.intermediate_columns | ||
| .values() | ||
| .flat_map(|(_, def)| def.iter().flat_map(|d| d.all_children())), | ||
| ) | ||
| .collect_vec() | ||
| }) |
There was a problem hiding this comment.
Is this edit because we now move some identities to intermediates, so we have to use both as the preimage of challenge derivation, in order to guarantee sufficient randomness?
There was a problem hiding this comment.
No it's simpler than that:
col a = challenge(0, 0); // the challenge is declared in the intermediate definition
a = a * a; // in the identity, the challenge does not appear
Here we simply look through all expressions as opposed to starting with identities and visiting the definitions of the intermediates they access, which is the same assuming that unused intermediates have been optimized away. If not, we may end up introducing challenges which are not needed.
| /// Auxiliary function to collect all references and next references to constant polynomials | ||
| /// References to intermediate values are resolved recursively | ||
| fn get_constant_refs_with_intermediates<T, E: AllChildren<AlgebraicExpression<T>>>( | ||
| e: &E, | ||
| intermediate_definitions: &BTreeMap<AlgebraicReferenceThin, AlgebraicExpression<T>>, | ||
| intermediates_cache: &mut BTreeMap<AlgebraicReferenceThin, BTreeSet<AlgebraicReference>>, | ||
| ) -> BTreeSet<AlgebraicReference> { | ||
| e.all_children() | ||
| .filter_map(|e| { | ||
| if let AlgebraicExpression::Reference(reference) = e { | ||
| Some(reference) | ||
| } else { | ||
| None | ||
| } | ||
| }; | ||
| }); | ||
| constant_with_next_list | ||
| }) | ||
| .map(|reference| match reference.poly_id.ptype { | ||
| PolynomialType::Constant => std::iter::once(reference.clone()).collect(), | ||
| PolynomialType::Intermediate => { | ||
| let reference = reference.to_thin(); | ||
| intermediates_cache | ||
| .get(&reference) | ||
| .cloned() | ||
| .unwrap_or_else(|| { | ||
| let result = get_constant_refs_with_intermediates( | ||
| &intermediate_definitions[&reference], | ||
| intermediate_definitions, | ||
| intermediates_cache, | ||
| ); | ||
| intermediates_cache.insert(reference, result.clone()); | ||
| result | ||
| }) | ||
| } | ||
| PolynomialType::Committed => std::iter::empty().collect(), | ||
| }) | ||
| .fold(BTreeSet::new(), |mut acc, set| { | ||
| acc.extend(set); | ||
| acc | ||
| }) |
There was a problem hiding this comment.
Are these edits needed, because previously intermediates can't contain next references to constants as children but now they can and these intermediates are always prior witness columns downgraded to intermediates by the optimizer?
There was a problem hiding this comment.
So basically no next reference to constants for intermediates is a user interface level requirement but not a hard requirement in lower level?
There was a problem hiding this comment.
This is needed because we need to find all constant columns which are referenced in the current and next row, respectively, and this requires recursively looking at intermediate columns:
col fixed F = ...;
col a = F;
col a_next = F';
col witness b;
b = a_next; // this means that `F'` is accessed, by definition of `a_next`
b = a; // this means that `F` is accessed, by definition of `a`
b = a'; // this means that `F'` is accessed, by definition of `a`
Blocking #2425 , adapted from `arith256.asm`
what
Replace certain multilinear constraints* with intermediate polynomials in pilopt.
*with no next references, not touching public inputs
why
This comment highlights a use-case where materialising a column which is only constrained to a non-shifted multilinear polynomial is wasteful. Fixing this when we create the code is tricky, since we cannot know the degree of the constraint from pil. This is however something pilopt can do, which is what we attempt to do here
unknowns
x = 42andx = ywhich are both multilinear expressions. They do no yield intermediate polynomials, since in that case it is fine to "inline" them. This implementation currently makes sure all three optimizer apply to distinct cases, but maybe it would be better to have a single optimizer which handles all three cases, only introducing intermediate polynomials in the non trivial cases (42andy)