From 5ccfd463f70eedee24a68b353042f7103aa7a6e6 Mon Sep 17 00:00:00 2001 From: arijitdutta67 Date: Tue, 8 Oct 2024 12:38:20 +0530 Subject: [PATCH 1/2] added constraints --- .../prover/statemanager/accumulator/define.go | 47 +++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/prover/zkevm/prover/statemanager/accumulator/define.go b/prover/zkevm/prover/statemanager/accumulator/define.go index 66b324cc..b718e676 100644 --- a/prover/zkevm/prover/statemanager/accumulator/define.go +++ b/prover/zkevm/prover/statemanager/accumulator/define.go @@ -273,6 +273,10 @@ func (am *Module) define(comp *wizard.CompiledIOP, s Settings) { // INSERT or a DELETE operation respectively. am.checkEmptyLeaf() + // Check the consistency of the HKey, HKeyMinus, and HKeyPlus for INSERT and ReadZero operations. + // i.e., they are consistent with the corresponding leaf opening values + am.checkHKeyConsistency() + // Sandwitch check for INSERT and READ-ZERO operations am.checkSandwitch() @@ -458,6 +462,49 @@ func (am *Module) checkEmptyLeaf() { am.comp.InsertGlobal(am.Round, am.qname("EMPTY_LEAVES_FOR_DELETE"), expr2) } +func (am *Module) checkHKeyConsistency() { + cols := am.Cols + // INSERT: The HKeyMinus in the leaf minus openings is the same as HKeyMinus column i.e., + // IsActiveAccumulator[i] * IsInsert[i] * IsFirst[i] * (HKeyMinus[i] - LeafOpenings.Hkey[i]) + expr1 := symbolic.Mul(cols.IsActiveAccumulator, + cols.IsInsert, + cols.IsFirst, + symbolic.Sub(cols.HKeyMinus, cols.LeafOpenings.HKey)) + am.comp.InsertGlobal(am.Round, am.qname("HKEY_MINUS_CONSISTENCY_INSERT"), expr1) + + // INSERT: The HKey in the inserted leaf openings (in the fourth row) is the same as HKey column i.e., + // IsActiveAccumulator[i] * IsInsert[i] * IsFirst[i] * (HKey[i] - LeafOpenings.Hkey[i+3]) + expr2 := symbolic.Mul(cols.IsActiveAccumulator, + cols.IsInsert, + cols.IsFirst, + symbolic.Sub(cols.HKey, ifaces.ColumnAsVariable(column.Shift(cols.LeafOpenings.HKey, 3)))) + am.comp.InsertGlobal(am.Round, am.qname("HKEY_CONSISTENCY_INSERT"), expr2) + + // INSERT: The HKeyPlus in the plus leaf openings is the same as HKeyPlus column i.e., + // IsActiveAccumulator[i] * IsInsert[i] * IsFirst[i] * (HKeyPlus[i] - LeafOpenings.Hkey[i+4]) + expr3 := symbolic.Mul(cols.IsActiveAccumulator, + cols.IsInsert, + cols.IsFirst, + symbolic.Sub(cols.HKeyPlus, ifaces.ColumnAsVariable(column.Shift(cols.LeafOpenings.HKey, 4)))) + am.comp.InsertGlobal(am.Round, am.qname("HKEY_PLUS_CONSISTENCY_INSERT"), expr3) + + // READ-ZERO: The HKeyMinus in the minus leaf openings is the same as HKeyMinus column i.e., + // IsActiveAccumulator[i] * IsReadZero[i] * IsFirst[i] * (HKeyMinus[i] - LeafOpenings.Hkey[i]) + expr4 := symbolic.Mul(cols.IsActiveAccumulator, + cols.IsReadZero, + cols.IsFirst, + symbolic.Sub(cols.HKeyMinus, cols.LeafOpenings.HKey)) + am.comp.InsertGlobal(am.Round, am.qname("HKEY_MINUS_CONSISTENCY_READ_ZERO"), expr4) + + // READ-ZERO: The HKeyPlus in the plus leaf openings is the same as HKeyPlus column i.e., + // IsActiveAccumulator[i] * IsReadZero[i] * IsFirst[i] * (HKeyPlus[i] - LeafOpenings.Hkey[i+1]) + expr5 := symbolic.Mul(cols.IsActiveAccumulator, + cols.IsReadZero, + cols.IsFirst, + symbolic.Sub(cols.HKeyPlus, ifaces.ColumnAsVariable(column.Shift(cols.LeafOpenings.HKey, 1)))) + am.comp.InsertGlobal(am.Round, am.qname("HKEY_PLUS_CONSISTENCY_READ_ZERO"), expr5) +} + func (am *Module) checkSandwitch() { cols := am.Cols // We want sandwitch check only at row 1 of INSERT and READ-ZERO From 87fe5a72101107e02c4fed374dc03375fe5d4d9e Mon Sep 17 00:00:00 2001 From: arijitdutta67 Date: Wed, 9 Oct 2024 12:26:37 +0530 Subject: [PATCH 2/2] added the constraints in the sandwitch check --- .../prover/statemanager/accumulator/define.go | 27 ++++++++----------- 1 file changed, 11 insertions(+), 16 deletions(-) diff --git a/prover/zkevm/prover/statemanager/accumulator/define.go b/prover/zkevm/prover/statemanager/accumulator/define.go index b718e676..b1804265 100644 --- a/prover/zkevm/prover/statemanager/accumulator/define.go +++ b/prover/zkevm/prover/statemanager/accumulator/define.go @@ -273,11 +273,9 @@ func (am *Module) define(comp *wizard.CompiledIOP, s Settings) { // INSERT or a DELETE operation respectively. am.checkEmptyLeaf() - // Check the consistency of the HKey, HKeyMinus, and HKeyPlus for INSERT and ReadZero operations. - // i.e., they are consistent with the corresponding leaf opening values - am.checkHKeyConsistency() - // Sandwitch check for INSERT and READ-ZERO operations + // We also check the consistency of the HKey, HKeyMinus, and HKeyPlus for INSERT and ReadZero operations. + // i.e., they are consistent with the corresponding leaf opening values am.checkSandwitch() // Pointer check for INSERT, READ-ZERO, and DELETE operations @@ -462,8 +460,13 @@ func (am *Module) checkEmptyLeaf() { am.comp.InsertGlobal(am.Round, am.qname("EMPTY_LEAVES_FOR_DELETE"), expr2) } -func (am *Module) checkHKeyConsistency() { +func (am *Module) checkSandwitch() { cols := am.Cols + // We want sandwitch check only at row 1 of INSERT and READ-ZERO + activeRow := symbolic.Add(symbolic.Mul(cols.IsFirst, cols.IsInsert), symbolic.Mul(cols.IsFirst, cols.IsReadZero)) + byte32cmp.Bytes32Cmp(am.comp, 16, 16, string(am.qname("CMP_HKEY_HKEY_MINUS")), am.Cols.HKey, am.Cols.HKeyMinus, activeRow) + byte32cmp.Bytes32Cmp(am.comp, 16, 16, string(am.qname("CMP_HKEY_PLUS_HKEY")), am.Cols.HKeyPlus, am.Cols.HKey, activeRow) + // INSERT: The HKeyMinus in the leaf minus openings is the same as HKeyMinus column i.e., // IsActiveAccumulator[i] * IsInsert[i] * IsFirst[i] * (HKeyMinus[i] - LeafOpenings.Hkey[i]) expr1 := symbolic.Mul(cols.IsActiveAccumulator, @@ -477,7 +480,7 @@ func (am *Module) checkHKeyConsistency() { expr2 := symbolic.Mul(cols.IsActiveAccumulator, cols.IsInsert, cols.IsFirst, - symbolic.Sub(cols.HKey, ifaces.ColumnAsVariable(column.Shift(cols.LeafOpenings.HKey, 3)))) + symbolic.Sub(cols.HKey, column.Shift(cols.LeafOpenings.HKey, 3))) am.comp.InsertGlobal(am.Round, am.qname("HKEY_CONSISTENCY_INSERT"), expr2) // INSERT: The HKeyPlus in the plus leaf openings is the same as HKeyPlus column i.e., @@ -485,7 +488,7 @@ func (am *Module) checkHKeyConsistency() { expr3 := symbolic.Mul(cols.IsActiveAccumulator, cols.IsInsert, cols.IsFirst, - symbolic.Sub(cols.HKeyPlus, ifaces.ColumnAsVariable(column.Shift(cols.LeafOpenings.HKey, 4)))) + symbolic.Sub(cols.HKeyPlus, column.Shift(cols.LeafOpenings.HKey, 4))) am.comp.InsertGlobal(am.Round, am.qname("HKEY_PLUS_CONSISTENCY_INSERT"), expr3) // READ-ZERO: The HKeyMinus in the minus leaf openings is the same as HKeyMinus column i.e., @@ -501,18 +504,10 @@ func (am *Module) checkHKeyConsistency() { expr5 := symbolic.Mul(cols.IsActiveAccumulator, cols.IsReadZero, cols.IsFirst, - symbolic.Sub(cols.HKeyPlus, ifaces.ColumnAsVariable(column.Shift(cols.LeafOpenings.HKey, 1)))) + symbolic.Sub(cols.HKeyPlus, column.Shift(cols.LeafOpenings.HKey, 1))) am.comp.InsertGlobal(am.Round, am.qname("HKEY_PLUS_CONSISTENCY_READ_ZERO"), expr5) } -func (am *Module) checkSandwitch() { - cols := am.Cols - // We want sandwitch check only at row 1 of INSERT and READ-ZERO - activeRow := symbolic.Add(symbolic.Mul(cols.IsFirst, cols.IsInsert), symbolic.Mul(cols.IsFirst, cols.IsReadZero)) - byte32cmp.Bytes32Cmp(am.comp, 16, 16, string(am.qname("CMP_HKEY_HKEY_MINUS")), am.Cols.HKey, am.Cols.HKeyMinus, activeRow) - byte32cmp.Bytes32Cmp(am.comp, 16, 16, string(am.qname("CMP_HKEY_PLUS_HKEY")), am.Cols.HKeyPlus, am.Cols.HKey, activeRow) -} - func (am *Module) checkPointer() { cols := am.Cols // Check #1 for INSERT: IsFirst[i] * IsInsert[i] * (LeafMinusNext[i] - LeafPlusIndex[i])