From 6d0fb6795cf3670d410c81688afdaaa5c4201b0d Mon Sep 17 00:00:00 2001 From: arijitdutta67 Date: Wed, 9 Oct 2024 13:24:32 +0530 Subject: [PATCH] changes as suggested by Alex --- .../zkevm/prover/statemanager/accumulator/define.go | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/prover/zkevm/prover/statemanager/accumulator/define.go b/prover/zkevm/prover/statemanager/accumulator/define.go index db7e7432c..47afc723e 100644 --- a/prover/zkevm/prover/statemanager/accumulator/define.go +++ b/prover/zkevm/prover/statemanager/accumulator/define.go @@ -542,13 +542,12 @@ func (am *Module) checkNextFreeNode() { symbolic.Sub(cols.NextFreeNode, cols.InsertionPath, symbolic.NewConstant(1))) am.comp.InsertGlobal(am.Round, am.qname("NEXT_FREE_NODE_CONSISTENCY_2"), expr4) - // If it is an empty leaf for the INSERT operation, then it must be at row 3 - // and IsInsertRow3 is true i.e., - // IsActive[i] * IsInsert[i] * IsEmptyLeaf[i] * (1-IsInsertRow3[i]) + // IsInsertRow3 is true if and only if it is row 3 for INSERT operation, i.e., + // IsActiveAccumulator[i] * (IsInsert[i] * IsEmptyLeaf[i] - IsInsertRow3[i]). The constraint that + // IsEmptyLeaf is 1 if and only if it is row 3 for INSERT (and row 4 of DELETE) is imposed already. expr5 := symbolic.Mul(cols.IsActiveAccumulator, - cols.IsInsert, - cols.IsEmptyLeaf, - symbolic.Sub(1, cols.IsInsertRow3)) + symbolic.Sub(symbolic.Mul(cols.IsInsert, cols.IsEmptyLeaf), + cols.IsInsertRow3)) am.comp.InsertGlobal(am.Round, am.qname("IS_INSERT_ROW3_CONSISTENCY"), expr5) }