fix(prover-ray): permutation/lookup bug involving shifts cancellation from vanishing calls - #3793
fix(prover-ray): permutation/lookup bug involving shifts cancellation from vanishing calls#3793bogdanbear wants to merge 1 commit into
Conversation
… cancelling due to the wrong vanishing call Signed-off-by: Bogdan Ursu <bogdanursuoffice@gmail.com>
|
Should we ban all together lookups over shifted: because that seems to be a nest for bugs? Sam, maybe we could ban the shifts that are bigger than one or minus one. |
|
I am still wrapping my head around whether this issue is actually an issue or not:
Then, clearly the first row of this table is ill-defined and it should not even be matched by the lookup. So the contribution of this row in the grand-product or log-derivative sum should be void. What this PR highlight is that, on top of being non-natural to prove, this also causes an interruption in the running sum/product constraints which is an additional problem. Which is solved by this PR. I think this is a good thing. But there are still problems around that:
Then, the 7 first rows of T are now ill-defined and must be excluded from the lookup. But with your PR, the expression offset is forced to 1; and the rows [[1; 6]] are "re-added" in the sum/product. The consequence is that it makes the entire notion of lookup/permutation. In fact, even with an offset of 1 there is a problem because the initiating/terminating local constraints are using the garbage row instead of the global one. You can keep the fix, but the API should reject tables with offsets as this is not well-defined in our framework. This will also prevent an entire class of wierd bug that result from that. |
buildZin grandproduct and logderivativesum registered the running-product/sum recurrence withNewVanishing, which infers cancelled rows from every shift in the tree — including shifts inside the caller's factor/fraction expressions — so a+k-shifted column cancelled the last k rows on top of row 0, leaving the openedZFinalrow unconstrained and letting a prover forge the endpoint (reachable in production viazkcdriver'sRelativeShifton lookup views).Both now use
NewVanishingManual(..., 0)to cancel row 0 only — preserving the dynamicn=1vacuity — plus a warning onNewVanishingabout inference over spliced-in subexpressions, and a regression test per compiler pinningCancelledPositions == {0}.Checklist