Hints for existing vars#3761
Conversation
chriseth
force-pushed
the
hints_for_existing_vars
branch
from
8e0d2fb to
6d53ac7
Compare
| } | ||
| } | ||
|
|
||
| fn convert_computation_method<T, U>( |
There was a problem hiding this comment.
I guess if you go for 063d3f1, this should also be a method on ComputationMethod for consistency.
| } | ||
| } | ||
| }; | ||
| if derived_column.is_new { |
There was a problem hiding this comment.
Similar to my other comment, I think it would be better if columns_to_compute didn't even store the hints.
I'd suggest that SymbolicMachine stores them separately (instead of in derived_columns). Then the let columns_to_compute = &apc.machine.derived_columns; line in generate_trace wouldn't even put it into TraceData.
…estions Suggestions to #3761
Co-authored-by: Georg Wiese <georgwiese@gmail.com>
| diff_marker__1_0 (old) = IfEqZero(b__3_0, IfEqZero(b__2_0, IfEqZero(b__1_0, 0, 1), 0), 0) | ||
| diff_marker__2_0 (old) = IfEqZero(b__3_0, IfEqZero(b__2_0, 0, 1), 0) | ||
| diff_marker__3_0 (old) = IfEqZero(b__3_0, 0, 1) | ||
| diff_val_0 (old) = IfEqZero(b__0_0, 1, QuotientOrZero(b__0_0 - 1, 1)) |
There was a problem hiding this comment.
I'm reviewing this again, but I still don't see how this is correct. Still confused about the two comments I made in #3770.
I studied the algebraic constraints of OpenVM's less than chip. This is an annotated excerpt (I already specialized it to the SLTU case):
cmp_result * (cmp_result - 1) = 0
// Diff markers are boolean and at most one is set
diff_marker__3 * (diff_marker__3 - 1) = 0
diff_marker__2 * (diff_marker__2 - 1) = 0
diff_marker__1 * (diff_marker__1 - 1) = 0
diff_marker__0 * (diff_marker__0 - 1) = 0
(0 + diff_marker__3 + diff_marker__2 + diff_marker__1 + diff_marker__0) * (0 + diff_marker__3 + diff_marker__2 + diff_marker__1 + diff_marker__0 - 1) = 0
// If diff_marker__3 is unset, c__3 = b__3 ((2 * cmp_result - 1) is always nonzero?!)
(1 - diff_marker__3) * ((c__3 - b__3) * (2 * cmp_result - 1)) = 0
// If diff_marker__3 is set, diff_val = (c__3 - b__3) * (2 * cmp_result - 1)
// => if cmp_result = 0: diff_val = b__3 - c__3
// => if cmp_result = 1: diff_val = c__3 - b__3
// Note that `diff_val - 1` is byte constrained
// => if diff_marker__3, it has to be that b__3 != c__3 and cmp_result is set correctly!
diff_marker__3 * (diff_val - (c__3 - b__3) * (2 * cmp_result - 1)) = 0
// Same for limb 2
(1 - (0 + diff_marker__3 + diff_marker__2)) * ((c__2 - b__2) * (2 * cmp_result - 1)) = 0
diff_marker__2 * (diff_val - (c__2 - b__2) * (2 * cmp_result - 1)) = 0
// Same for limb 1
(1 - (0 + diff_marker__3 + diff_marker__2 + diff_marker__1)) * ((c__1 - b__1) * (2 * cmp_result - 1)) = 0
diff_marker__1 * (diff_val - (c__1 - b__1) * (2 * cmp_result - 1)) = 0
// Same for limb 0
(1 - (0 + diff_marker__3 + diff_marker__2 + diff_marker__1 + diff_marker__0)) * ((c__0 - b__0) * (2 * cmp_result - 1)) = 0
diff_marker__0 * (diff_val - (c__0 - b__0) * (2 * cmp_result - 1)) = 0
// If no diff marker is set, cmp_result is zero
(1 - (0 + diff_marker__3 + diff_marker__2 + diff_marker__1 + diff_marker__0)) * cmp_result = 0SEQZ is implemented as SLTU with c = 1, i.e. c__1 = c__2 = c__3 = 0 and c__0 = 1. So, I think these would be the correct hints:
diff_marker__0_0 = 1 ↔ b__3_0 = 0 ∧ b__2_0 = 0 ∧ b__1_0 = 0 ∧ b__0_0 ≠ 1
diff_marker__1_0 = 1 ↔ b__3_0 = 0 ∧ b__2_0 = 0 ∧ b__1_0 ≠ 0
diff_marker__2_0 = 1 ↔ b__3_0 = 0 ∧ b__2_0 ≠ 0
diff_marker__3_0 = 1 ↔ b__3_0 ≠ 0
diff_val_0 = if b__3_0 ≠ 0 {
b__3_0 // b__3 - c__3
} else if b__2_0 ≠ 0 {
b__2_0 // b__2 - c__2
} else if b__1_0 ≠ 0 {
b__1_0 // b__1 - c__1
} else if b__0_0 = 0 {
1 // c__0 - b__0
} else b__0_0 = 1 {
// We have b__0_0 = 0 ∧ b__1_0 = 0 ∧ b__2_0 = 0 ∧ b__3_0 = 1 (or: b = c = 1)
// If b = 1, diff_val is unconstrained, except that `diff_val - 1` must be a byte
1
} else {
b__0_0 - 1 // b__0 - c__0
}
There was a problem hiding this comment.
I think the hints here are correct for b = 0 and b = 1, which is probably many (if not all) cases in practice. But I think SEQZ should work for all values of b?
There was a problem hiding this comment.
Sorry, did a few edits, I think the above is correct now. I now believe the existing hints for the diff markers are correct, but not for diff_val_0. It should depend on all limbs of b, like above. Also, right now, b = 1 would yield diff_val_0 = 0, which would fail this constraint in the original chip.
2 participants
This adds a mechanism that allows to provide a way to compute the value of variables that were removed. This is sometimes helpful, especially in complicated cases, to prove semantic equivalence of constraint systems.
We re-use the existing "derived columns" mechanism and add the "removed variables" in the same way, adding a flag that indicates if the variable was added or removed.