Prover/Global Constraint Boundary Cancellation Explainer (#335)

* minor typo fix
* comments in the test to show bounadary cancellation
This commit is contained in:
Arijit Dutta
2025-01-06 13:40:04 +05:30
committed by GitHub
parent 3805acbffe
commit 9dc4304846
2 changed files with 18 additions and 7 deletions

View File

@@ -70,7 +70,7 @@ func NewGlobalConstraint(id ifaces.QueryID, expr *symbolic.Expression, noBoundCa
}
if len(noBoundCancel) > 0 {
utils.Require(len(noBoundCancel) == 1, "there should be only 2 bound cancel got %v", len(noBoundCancel))
utils.Require(len(noBoundCancel) == 1, "there should be only 1 bound cancel got %v", len(noBoundCancel))
res.NoBoundCancel = noBoundCancel[0]
}

View File

@@ -50,6 +50,7 @@ func fibonacci() (wizard.DefineFunc, wizard.ProverStep) {
n := 1 << 3
P := build.RegisterCommit(P, n) // overshadows P
// X[i-1] + X[i-2] - X[i] = 0
expr := ifaces.ColumnAsVariable(column.Shift(P, -1)).
Add(ifaces.ColumnAsVariable(column.Shift(P, -2))).
Sub(ifaces.ColumnAsVariable(P))
@@ -79,7 +80,7 @@ func pythagoreTriplet() (wizard.DefineFunc, wizard.ProverStep) {
X := build.RegisterCommit(X, n) // overshadows P
Y := build.RegisterCommit(Y, n) // overshadows P
// X[i]^2 + Y[i]^2 - 25 = 0
expr := ifaces.ColumnAsVariable(X).Square().
Add(ifaces.ColumnAsVariable(Y).Square()).
Sub(symbolic.NewConstant(25))
@@ -106,15 +107,25 @@ func testDummyShifted() (wizard.DefineFunc, wizard.ProverStep) {
define := func(build *wizard.Builder) {
A := build.RegisterCommit(X, 4)
B := build.RegisterCommit(Y, 4)
expr := symbolic.Sub(column.Shift(A, 1),
symbolic.Mul(2, column.Shift(B, 1)))
// X[i+2] - 2 * Y[i+2] = 0
expr := symbolic.Sub(column.Shift(A, 2),
symbolic.Mul(2, column.Shift(B, 2)))
build.InsertGlobal(0, "Q", expr)
}
Prover := func(run *wizard.ProverRuntime) {
x := smartvectors.ForTest(2, 8, 4, 0)
y := smartvectors.ForTest(1, 4, 2, 0)
// Note that the first two indices of x and y columns below does not satisfy the
// constraints. The test still passes because the boundary condition cancellation is by default
// set to true for the InsertGlobal() function. The test will fail if we modify the above line
// by build.InsertGlobal(0, "Q", expr, true) and set noBoundCancellation to true. In this case,
// the columns will behave as circular vectors.
// Also to observe that the boundary indices here are 0 and 1 because for i = 0 onwards, the constraint starts
// looking at index 2, 3, and so on i.e. X[2] = 2*Y[2], X[3] = 2*Y[3].
// The boundary indices will be 2 and 3 if we had constraint: X[i-2] - 2 * Y[i-2] = 0, i.e. we could have put
// whatever values in those indices and the constraint would be satisfied.
x := smartvectors.ForTest(2, 8, 4, 2)
y := smartvectors.ForTest(2, 3, 2, 1)
run.AssignColumn(X, x)
run.AssignColumn(Y, y)
}