Minimal range rules after head tail split #3511

ShuangWu121 · 2025-12-22T19:47:52Z

solve the constraints that satisfying the following properties

a + b = 0
a >= 0
b >= 0

then : a = 0, b = 0

…iables

…occurrence_variables

…iables

Co-authored-by: ShuangWu121 <[email protected]>

…labs/powdr into single_occurrence_variables

…o head-tail-split

chriseth · 2026-01-05T18:24:16Z

constraint-solver/src/rule_based_optimizer/rules.rs

+    // 3. head is a linear expression coeff * var,
+    // then both head and tail must be zero.
+    // This rule replaces the variable var by zero.
+    struct ExpressionWithZeroMinimalRange(Expr);


We could call it NonNegativeExpression and instead of starting with ExpressionSumHeadTail, we could just use RangeConstraintOnExpression(e, rc) - it will work for all expressions. I also needed that in one of my PRs, so I think it will come in handy.

Oh and we also need rc.range().1 < T::from(-1), otherwise it could also be unrestricted.

Indeed. Done.

chriseth · 2026-01-05T18:26:32Z

constraint-solver/src/rule_based_optimizer/rules.rs

+    struct MinimalRangeZeroDeducible<T: FieldElement>(Expr, Expr,Expr, Var, T);
+    MinimalRangeZeroDeducible(e, head, tail, var, coeff) <-
+      MinimalRangeAlgebraicConstraintCandidate(e),
+      ExpressionSumHeadTail(e, head, tail),


Aren't the following 4 lines already part of MinimalRangeAlgebraicConstraintCandidate?

chriseth

Looks good but I think this can still be simplified.

constraint-solver/src/rule_based_optimizer/rules.rs

chriseth · 2026-01-07T11:24:18Z

constraint-solver/src/rule_based_optimizer/rules.rs

+    // If an algebraic constraint e = 0 has the following properties:
+    // 1. expression e has range constraint [0, a] with a < P,
+    // 2. e = head + tail, and both head, tail >= 0,
+    // 3. head is a linear expression coeff * var,


Please correct me if I'm wrong, but I think we need as a vital component that rc(head) + rc(tail) is non-negative, i.e. does not wrap. I.e. it's not a property of the range constraint of e but rather of how we can combine the range constraints of head and tail.

I am not sure I got it, since e = head + tail, isn't rc(head) + rc(tail) = rc(e)? This is an assumption though.

Do you see any case where
rc(e) < P - 1 holds, but rc_head.combine_sum(rc_tail).range().1 < P - 1 does not hold?

I can think about a case that rc(head) + rc(tail) wrapped but e is not:

rc(head) = [P-5, P-1] rc(tail) = [10, 20] rc(e) =[5, 19]

but the combine_sum function cannot distinguish this case, right?

In this minimal range zero rule, both head and tail has range start from zero, in this case, it seems to me:
rc(e) < P - 1 <=> rc_head.combine_sum(rc_tail).range().1 < P - 1
does this make sense?

I think we have to be more specific with our notation here. The notation rc(head) is convenient but also problematic. Is it "just some range constraint that is compatible with the satisfying assignments to head" or is it "the currently best-known range constraint for head" or is it "the theoretically best range constraint for head"?

It can be that the best-known range constraint for e is "smaller" (i.e. a subset of) than the sum of the best-known range constraints for head and tail.

We could have a constraint X + Y = 0, then we have range constraints on X and Y that are 0..P-8 and then we have another range constrain on X + Y that say that it is either 0 or 1. Note that range constraints for expression can come from bus interactions. In this case, we cannot conclude that X = Y = 0, because another valid solution would be X = -10, Y = 10. I think we cannot work with range constraints for the expression (if it is an algebraic constraint) at all, because in the end, that expression is known to be 0 and only 0.

I see. Thanks for the explanation!
I added the condition rc_head.combine_sum(rc_tail).range().1 < P - 1
now since rc_head.combine_sum(rc_tail).range().1 < P - 1 requires rc_head.range_width() + rc_tail.range_width() < P -1, the case (X + Y = 0, X, Y = [0..P-8], X = -10, Y = 10) should be ruled out, does this sound correct?

chriseth · 2026-01-07T11:24:56Z

constraint-solver/src/rule_based_optimizer/rules.rs

      (coeff != T::zero());

+    //////////////////// RANGE PROPERTIES OF EXPRESSIONS //////////////////////
+    struct NonNegativeExpression(Expr);


I think I suggested the name, but it's not strictly correct. But I also don't know a better name, so maybe it's enough to document the exact semantics?

Added comment.

When you say “not strictly correct”, is that because this works over field elements, where “negative” isn’t really a well-defined concept?

I mean this is also an aspect but usually, when we talk about signed numbers in the field, we say that 0.. P/2 are the non-negative numbers and the rest is the negative numbers. I.e. the range 0..(P-2) would also have negative numbers.

I see. I documented its range, what about calling it NonWrappingExpression though?

chriseth · 2026-01-07T11:25:25Z

constraint-solver/src/rule_based_optimizer/rules.rs

+      (e_rc.range().1 < T::from(-1)),
+      NonNegativeExpression(head),
+      NonNegativeExpression(tail),
+      AlgebraicConstraint(e);


Please check the performance, but I think putting AlgebraicConstraint(e) first should improve the speed.

I tested this on keccak_small_prove_mock, and moving AlgebraicConstraint(e) first is indeed much faster.
Is there a general ordering principle for these facts that can improve performance?

chriseth · 2026-01-07T11:27:24Z

constraint-solver/src/rule_based_optimizer/rules.rs

+    struct MinimalRangeAlgebraicConstraintCandidate(Expr);
+    MinimalRangeAlgebraicConstraintCandidate(e) <-
+      ExpressionSumHeadTail(e, head, tail),
+      RangeConstraintOnExpression(e, e_rc),


Please correct me if I'm wrong, but I think we need a statement that rc_head.combine_sum(rc_tail).range().1 < P - 1

Co-authored-by: chriseth <[email protected]>

…fter-head-tail

chriseth · 2026-01-14T14:55:16Z

constraint-solver/src/rule_based_optimizer/rules.rs

+    RangeConstraintOnExpression(tail, rc_tail),
+    (rc_head.range().0 == T::from(0)),
+    (rc_tail.range().0 == T::from(0)),
+    (rc_head.combine_sum(&rc_tail).range().1 < T::from(-1));


If you use combine_sum here, then (following good practice and not assuming anything about the inner workings of combine_sum), it could still be that rc_head and rc_tail are unconstrained, even though all three of the conditions are met (since it could be -1..-2). Because of that, I think it would be better to use rc_head.range().1.to_arbitrary_integer() + ... - it should also be faster.

constraint-solver/src/rule_based_optimizer/rules.rs

ShuangWu121 · 2026-01-14T15:32:08Z

performance check (rule system enabled before solver):

chriseth · 2026-01-14T16:36:22Z

Does it reduce the overall timing?

Co-authored-by: chriseth <[email protected]>

ShuangWu121 · 2026-01-16T09:51:46Z

Does it reduce the overall timing?

No, it actually make the performance worse. I measured the execution time of the optimizer, got

solver runs first: 14s
rule based system without this PR: 25s
rule based system with this PR: 42s
I will check what causes this result.

chriseth and others added 30 commits December 12, 2025 10:37

Rules for single-occurrence variables.

af02f34

Fix single occurrence.

b2d5b5a

Compute range constraints on expressions.

00ec4d6

update expectations.

9b627ae

Rename rules.

65c090c

Merge remote-tracking branch 'origin/main' into single_occurrence_var…

2da3d78

…iables

Do not replace.

39c6a5b

Update expectations.

6fd7d61

Do not execute replacements in the rule system.

060e60b

clippy

b9df4cc

Merge remote-tracking branch 'origin/fix_reth_benchmark' into single_…

8338ef4

…occurrence_variables

Update expectations.

0153958

Merge remote-tracking branch 'origin/main' into single_occurrence_var…

b18a804

…iables

rules for head tail split

bb71b51

undo comment

6e00e00

fix

0f55dcf

update copy_byte change

fe88f66

update tests

1386f54

refine rules

08e90b1

Apply suggestion from @ShuangWu121

fcbccbd

Co-authored-by: ShuangWu121 <[email protected]>

Apply suggestion from @ShuangWu121

fd441c5

Co-authored-by: ShuangWu121 <[email protected]>

Add comment.

e7c2c00

fix comments

42a8e5b

clean up

88f7cdb

clean up more

0723dd4

Merge branch 'single_occurrence_variables' of ssh://github.com/powdr-…

a624322

…labs/powdr into single_occurrence_variables

Merge remote-tracking branch 'origin/single_occurrence_variables' int…

7ff18a2

…o head-tail-split

fix comments

93b6b33

remove algebraicConstraint, it cause performance slow down

0a1e412

add comments

db6330e

ShuangWu121 added 2 commits January 5, 2026 15:33

change version of crepe

d279500

update comments

fbe90a7

ShuangWu121 marked this pull request as ready for review January 5, 2026 16:03

chriseth reviewed Jan 5, 2026

View reviewed changes

chriseth requested changes Jan 5, 2026

View reviewed changes

ShuangWu121 added 2 commits January 5, 2026 23:37

simplified

f3f432e

relocate nonnegativeexpression

7021bd4

chriseth reviewed Jan 7, 2026

View reviewed changes

constraint-solver/src/rule_based_optimizer/rules.rs Outdated Show resolved Hide resolved

chriseth reviewed Jan 7, 2026

View reviewed changes

ShuangWu121 and others added 8 commits January 7, 2026 13:41

Update constraint-solver/src/rule_based_optimizer/rules.rs

b95a3e5

Co-authored-by: chriseth <[email protected]>

add comment

fca5b14

change order of the facts

c167566

Merge remote-tracking branch 'origin/main' into minimal-range-rules-a…

2f9024c

…fter-head-tail

add more restriction

252438e

add more comment

bcea4b1

refactor

d15e5ab

change name

b5dacc4

chriseth reviewed Jan 14, 2026

View reviewed changes

constraint-solver/src/rule_based_optimizer/rules.rs Outdated Show resolved Hide resolved

chriseth reviewed Jan 14, 2026

View reviewed changes

constraint-solver/src/rule_based_optimizer/rules.rs Outdated Show resolved Hide resolved

ShuangWu121 and others added 2 commits January 16, 2026 09:36

Update constraint-solver/src/rule_based_optimizer/rules.rs

61e4b5b

Co-authored-by: chriseth <[email protected]>

Update constraint-solver/src/rule_based_optimizer/rules.rs

ab0d7f4

Co-authored-by: chriseth <[email protected]>

change how the addition is done

27cbbec

Minimal range rules after head tail split #3511

Are you sure you want to change the base?

Minimal range rules after head tail split #3511

Uh oh!

Conversation

ShuangWu121 commented Dec 22, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chriseth left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ShuangWu121 Jan 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chriseth Jan 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

ShuangWu121 commented Jan 14, 2026

Uh oh!

chriseth commented Jan 14, 2026

Uh oh!

ShuangWu121 commented Jan 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

ShuangWu121 Jan 7, 2026 •

edited

Loading

chriseth Jan 14, 2026 •

edited

Loading

ShuangWu121 commented Jan 16, 2026 •

edited

Loading