Document grouped expressions and define system equivalence. #3376
Conversation
| A Grouped Expression consists of a constant term, a list of linear terms (a list of pairs of a non-zero coefficient | ||
| and a variable) and a list of quadratic terms (a list of pairs of Grouped Expressions). | ||
|
|
||
| For affine Algebraic Expressions, the Grouped Expression provides a normal form (if sorted by variable). |
There was a problem hiding this comment.
| For affine Algebraic Expressions, the Grouped Expression provides a normal form (if sorted by variable). | |
| For affine algebraic expressions, the Grouped Expression provides a normal form (if sorted by variable). |
Now sure Algebraic Expressions were defined as a type?
There was a problem hiding this comment.
| and a variable) and a list of quadratic terms (a list of pairs of Grouped Expressions). | ||
|
|
||
| For affine Algebraic Expressions, the Grouped Expression provides a normal form (if sorted by variable). | ||
| It even provides a normal form for affine Algebraic Constraints if multiplied by a factor such that |
There was a problem hiding this comment.
Why Algebraic Constraints in capital initials?
There was a problem hiding this comment.
I'm writing all properly defined concepts in capitals, and in italics (using _..._) at the place where they are defined.
| This normal fom makes it easy to compare affine Algebraic Expressions for equality, | ||
| check if they have a constant difference, etc. | ||
|
|
||
| If a map data structure is used for the linear terms, substitution of variables is also quick. |
There was a problem hiding this comment.
At least you do not need to search for the variable.
|
|
||
| We call two Constraint Systems _equivalent_ if every satisfying assignment for one system | ||
| can be extended to a satisfying assignment for the other system and every such extension | ||
| leads to the same payloads and multiplicities for all _stateful_ bus interactions in both systems. |
There was a problem hiding this comment.
And every non-satisfying assignment of the first system must also not satisfy the second
There was a problem hiding this comment.
I meant "if for both of the two systems, every satisfying assignment can be extended to a satisfying system for the other", so it's symmetric. Is that the misunderstanding? If not:
Written like this, we could have a non-satisfying assignment for one system that is non-satisfying since it assigns an invalid value to a variable that does not occur in the other system, then that assignment could still be satisfying for the other system.
But even in the case we have the same variables, I think what you mean is already included:
Suppose we have an assignment A that does not satisfy system 1 but it does satisfy system 2. Then because of equivalence, it must be extensible to a satisfying assignment for system 1, which is a contradiction since the variables are the same but A does not satisfy system 1.
There was a problem hiding this comment.
Right yea, I missed the "one system or the other" being generic, I think it's fine as is
| ``` | ||
| x = 8 | ||
| x + y + z = 12 | ||
| 2 1 [x, y, z] |
There was a problem hiding this comment.
I assume this is a bus interaction, maybe write as a tuple to look more organized?
|
|
||
| Let us assume that the bus with ID 2 is stateful and allows all combinations of values between 0 and 100 (inclusive). | ||
| Note that the variables `y` and `z` are not uniquely determined in either system, so the stateful bus | ||
| acts both as input and output for the system. TODO can that be or do we need one send and one receive? |
There was a problem hiding this comment.
Currently for openvm every stateful interaction has a receive and a send
Co-authored-by: Leo <[email protected]>
Co-authored-by: Leo <[email protected]>
Co-authored-by: Leo <[email protected]>
Co-authored-by: Leo <[email protected]>
|
|
||
| For affine Algebraic Expressions, the Grouped Expression provides a normal form (if sorted by variable). | ||
| It even provides a normal form for affine Algebraic Constraints if multiplied by a factor such that | ||
| the constant term is zero or one. |
There was a problem hiding this comment.
How can this become zero?
It sounds like there would have to be some factor such that (const * factor) mod P = 0, which would mean that either const or factor is zero.
There was a problem hiding this comment.
Ah this is actually more complicated than I thought and also written in a bad way. What about the following:
It even provides a normal form for affine Algebraic Constraints if we require
the coefficient of the first variable (according to some fixed order on the
variables) to be one. Note that an Algebraic Constraint can be multiplied
by a nonzero factor without changing the semantics.
|
Needs a main merge |
Documents grouped expressions and defines the notion of equivalence we are preserving with the optimizer.
Note that our memory optimization uses a less strict version of equivalence that still needs to be defined.