Optimizer Documentation: Terminology #3350

chriseth · 2025-10-13T11:13:19Z

No description provided.

autoprecompiles/src/optimizer_documentation.md

Co-authored-by: Thibaut Schaeffer <[email protected]>

Schaeff · 2025-10-14T13:04:53Z

autoprecompiles/src/optimizer_documentation.md

+a superset of the set of allowed values. This means we can only use
+the information if the Range Constraints says that a value is not
+allowed. This also makes sense since we are looking at Algebraic


I find this part a bit vague.

Schaeff · 2025-10-14T13:10:28Z

autoprecompiles/src/optimizer_documentation.md

+A _Wrapping Interval_ is a pair of field elements `min` and `max`.
+If `min <= max` (as seen in the natural numbers), the Wrapping
+Interval allows a value `x` if and only if `min <= x <= max`.
+This is the non-wrapping case.
+If `min > max`, the Wrapping Interval allows a value `x`
+if and only if `x >= min` or `x <= max`. This is the wrapping case.
+
+The reason we allow these wrapping intervals is that we can compute
+the Range Constraint interval of an expression `x + k` for any constant `k`
+from the Range Constraint interval of `x` without losing information.


Do wrapping and non-wrapping intervals ever interact? I see the argument that you can define addition (and multiplication?) on intervals in a unified way, but I'm not sure it's worth it given the non-intuitive aspect of min > max being okay. Would it be possible to use an enum enum Interval { Inside { min, max }, Outside { min, max } and define addition and multiplication on that instead?

Sure, it could be done that way, but then you would need to verify in addition that min <= max is always ensured.

Another way we could do it is just to have first and length, and a value x is in range if it included in the sequence first, first + 1, first + 2, ..., first + length (and if length = 0, we would be able to model the empty range, which we cannot do currently).

Yes, first and length sound good

I just checked and I think it's at least 2-3 days work to change it, if not a week. I'll focus on documenting for now.

Thanks for checking!

autoprecompiles/src/optimizer_documentation.md

Schaeff · 2025-10-14T13:18:18Z

autoprecompiles/src/optimizer_documentation.md

+  lookup tables are not stateful.
+
+- `handle_bus_interaction`: Takes a Bus Interaction where its items are represented
+  by Range Constraints instead of expressions or field elements and returns


What does or apply to here?

I can remove or field elements if it creates confusion instead of clarifying things ;)

yea I guess instead of expressions suffices

Schaeff · 2025-10-14T13:21:10Z

autoprecompiles/src/optimizer_documentation.md

+parts of the system. A simple (and also best possible) implementation of
+`handle_bus_interaction` would be to always return the `0xff`-mask Range Constraint
+for the payload and ignore the input. Even if the input Range Constraint is something
+like `200..=300`, the solver will combine the two Range Constraints and derive
+`200..=255` as the new Range Constraint for the payload.


Why is 0xff the best implementation? Isn't it the one that mixes the input constraint with the bus constraint? Seems like this part mixes the naive implementation and what we do?

I don't really understand what you mean. Of course this document does not say what a "good" implementation is, so we cannot tell if it is the best possible. What implementation would you say is better and why? What do you mean by "naive implementation" and what do we do?

I think he's referring to the beginning of the par which does say (and also best possible)

I mean that the first part of this section talks about one strategy of always returning 0xff, while the second talks about combining range constraints.

Oh maybe the word 'input' is confusing?

Schaeff · 2025-10-14T13:24:07Z

autoprecompiles/src/optimizer_documentation.md

+Since our Range Constraints do not model individual bits well enough, it is sufficient
+to only compute the third item if two of them are fully known.


i don't understand this

I think the "it is sufficient" part here is what sounds a bit odd to me. Sufficient for what? From the text before it sounds like it's rather not sufficient for a full analysis.

Schaeff

really good introduction

Co-authored-by: Thibaut Schaeffer <[email protected]>

leonardoalt

First pass, need to continue from Bus Interaction Abstraction

leonardoalt · 2025-10-15T09:15:18Z

autoprecompiles/src/optimizer_documentation.md

+The task of the optimizer is hugely simplified by the concept of
+_Range Constraints_. In an abstract way, a _Range Constraint_ is
+the set of possible values for a specific algebraic expression.
+The solver can derive new Range Constraints from Algebraic Constraints


This is the first time solver is used, it'd be good to refer to something or define it.

Changed it to optimizer

leonardoalt · 2025-10-15T09:16:08Z

autoprecompiles/src/optimizer_documentation.md

+
+In our concrete implementation, we do not represent the exact set
+of allowed values. Instead, we use an under-approximation, i.e.
+a superset of the set of allowed values. This means we can only use


That would be an overapproximation, no?

leonardoalt · 2025-10-15T09:17:38Z

autoprecompiles/src/optimizer_documentation.md

+In our concrete implementation, we do not represent the exact set
+of allowed values. Instead, we use an under-approximation, i.e.
+a superset of the set of allowed values. This means we can only use
+the information if the Range Constraints says that a value is not


I think I do understand this part, but what's unclear here is "use for what"?

leonardoalt · 2025-10-15T09:24:36Z

autoprecompiles/src/optimizer_documentation.md

+We use `RC(x)` to denote the Range Constraint of an algebraic
+expression `x`.
+
+TODO It is not clear if this is the currently best-known range constraint,


TODO as in for this PR or the future?

leonardoalt · 2025-10-15T09:26:21Z

autoprecompiles/src/optimizer_documentation.md

+semantics of a bus interaction depends on the environment, i.e. the
+zkVM we are operating inside and the chips it has.
+
+A _Bus Interaction_ consists of a _Bus ID_, a _Multiplicity_ and


Maybe it makes sense to introduce it as a relation or predicate here? I think that could help abstract it

Can you give an example?

leonardoalt

Done now.

autoprecompiles/src/optimizer_documentation.md

leonardoalt · 2025-10-15T09:38:27Z

autoprecompiles/src/optimizer_documentation.md

+  lookup tables are not stateful.
+
+- `handle_bus_interaction`: Takes a Bus Interaction where its items are represented
+  by Range Constraints instead of expressions or field elements and returns


yea I guess instead of expressions suffices

leonardoalt · 2025-10-15T09:39:57Z

autoprecompiles/src/optimizer_documentation.md

+
+As an example, let us assume we are modeling a bus that implements a byte range
+constraint, i.e. a bus that takes a single payload item and enforces that it is
+in the range `0..=255`. The bus is not stateful since it does not depend on any


Suggested change

in the range `0..=255`. The bus is not stateful since it does not depend on any

in the range `0..=255`. The bus is not stateful since it does not depend on nor affects any

leonardoalt · 2025-10-15T09:40:34Z

autoprecompiles/src/optimizer_documentation.md

+parts of the system. A simple (and also best possible) implementation of
+`handle_bus_interaction` would be to always return the `0xff`-mask Range Constraint
+for the payload and ignore the input. Even if the input Range Constraint is something
+like `200..=300`, the solver will combine the two Range Constraints and derive


solver also undefined up to here

leonardoalt · 2025-10-15T09:41:16Z

autoprecompiles/src/optimizer_documentation.md

+parts of the system. A simple (and also best possible) implementation of
+`handle_bus_interaction` would be to always return the `0xff`-mask Range Constraint
+for the payload and ignore the input. Even if the input Range Constraint is something
+like `200..=300`, the solver will combine the two Range Constraints and derive
+`200..=255` as the new Range Constraint for the payload.


I think he's referring to the beginning of the par which does say (and also best possible)

leonardoalt · 2025-10-15T09:41:38Z

autoprecompiles/src/optimizer_documentation.md

+Another example would be an XOR-bus that takes three payload items `a, b, c`
+and ensures that all of them are bytes and `a ^ b = c`. This bus is also not stateful.
+Here, one would implement `handle_bus_interaction` by returning the three byte constraints
+for the payload items if the input has no restrictiens. But if the value of the same bit


Suggested change

for the payload items if the input has no restrictiens. But if the value of the same bit

for the payload items if the input has no restrictions. But if the value of the same bit

leonardoalt · 2025-10-15T09:43:27Z

autoprecompiles/src/optimizer_documentation.md

+Since our Range Constraints do not model individual bits well enough, it is sufficient
+to only compute the third item if two of them are fully known.


I think the "it is sufficient" part here is what sounds a bit odd to me. Sufficient for what? From the text before it sounds like it's rather not sufficient for a full analysis.

leonardoalt · 2025-10-15T09:46:04Z

autoprecompiles/src/optimizer_documentation.md

+- exhaustive search
+- equal zero check
+
+### Constraint System Solver


Maybe this section could be moved to the top to clarify what the instances of solver above mean.

…/powdr into optimizer_documentation

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

…/powdr into optimizer_documentation

Terminology

8c84adc

chriseth changed the title ~~Terminology~~ Optimizer Documentation: Terminology Oct 13, 2025

Skeleton of the rest of the document.

e78c051

Schaeff reviewed Oct 13, 2025

View reviewed changes

autoprecompiles/src/optimizer_documentation.md Outdated Show resolved Hide resolved

Update autoprecompiles/src/optimizer_documentation.md

25a058c

Co-authored-by: Thibaut Schaeffer <[email protected]>

Schaeff reviewed Oct 14, 2025

View reviewed changes

autoprecompiles/src/optimizer_documentation.md Outdated Show resolved Hide resolved

Schaeff reviewed Oct 14, 2025

View reviewed changes

autoprecompiles/src/optimizer_documentation.md Outdated Show resolved Hide resolved

Schaeff reviewed Oct 14, 2025

View reviewed changes

autoprecompiles/src/optimizer_documentation.md Outdated Show resolved Hide resolved

Schaeff reviewed Oct 14, 2025

View reviewed changes

chriseth and others added 4 commits October 14, 2025 16:22

Apply suggestion from @Schaeff

771634d

Co-authored-by: Thibaut Schaeffer <[email protected]>

Apply suggestion from @Schaeff

f4f2e9e

Co-authored-by: Thibaut Schaeffer <[email protected]>

Apply suggestion from @Schaeff

60c7682

Co-authored-by: Thibaut Schaeffer <[email protected]>

Another pass.

1cfa4b6

leonardoalt reviewed Oct 15, 2025

View reviewed changes

chriseth and others added 6 commits October 15, 2025 10:14

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

af35555

…/powdr into optimizer_documentation

Update byte range constraint part.

bade7e6

Update autoprecompiles/src/optimizer_documentation.md

900c75b

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

Fix under/over-approximation.

92515b5

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

31c6d06

…/powdr into optimizer_documentation

Rewrite Range Constraint section.

2a8fad0

Schaeff mentioned this pull request Oct 16, 2025

Some cleanup for range constraints. #3336

Open

		Since our Range Constraints do not model individual bits well enough, it is sufficient
		to only compute the third item if two of them are fully known.

	in the range `0..=255`. The bus is not stateful since it does not depend on any
	in the range `0..=255`. The bus is not stateful since it does not depend on nor affects any

	for the payload items if the input has no restrictiens. But if the value of the same bit
	for the payload items if the input has no restrictions. But if the value of the same bit

Optimizer Documentation: Terminology #3350

Are you sure you want to change the base?

Optimizer Documentation: Terminology #3350

Uh oh!

Conversation

chriseth commented Oct 13, 2025

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Schaeff Oct 14, 2025 • 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!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chriseth Oct 14, 2025 • 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!

Schaeff left a comment

Choose a reason for hiding this comment

Uh oh!

leonardoalt left a comment

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!

leonardoalt left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Schaeff Oct 14, 2025 •

edited

Loading

chriseth Oct 14, 2025 •

edited

Loading