Skip to content

Commit

Permalink
fix(ecpair): ensure last non-trivial input pair goes to ML+finalexp c…
Browse files Browse the repository at this point in the history 
…ircuit (#524)

* fix: set inputresult only once

* fix: copy only actual inputs going to pairing (no trivial pairs)

* fix: non-exclusive G2 membership or pairing check

* fix: enable index consistency check when interleaved G2 membership

We may interleave in the same rows the G2 membership and pairing check
inputs. Currently when we have interleaved then we disable the index
consisitency check.

* fix: do not project pair IDs and total pairings

* fix: add constraint to check totalpairs correctness

* test: add IS_RESULT column to test cases and uniform reformat

* feat: allow outputting CSV in hex

* feat: add utility method to write the module

* test: check also IS_RESULT in test cases

* test: add test case modules

* test: add regression test case

* feat: add testdata generator for ecpair

* feat: add tests for manual generation of EC edge cases

* fix: accumulator consistency assignment in case of one valid point

* docs: describe assignment

* fix: indexing when non-sequential valid points

* test: run tests on generated data

* feat: generate all cases for 1-5 input pairs

* test: skip long tests

* fix: test imports

* enable ecpair

* perf: parallelize testcase testing

---------

Co-authored-by: gusiri <[email protected]>
  • Loading branch information
@ivokub @gusiri
ivokub and gusiri authored Jan 16, 2025
1 parent 26ba22e commit 05d3ee2
Show file tree
Hide file tree
Showing 17 changed files with 2,805 additions and 810 deletions.
13 changes: 12 additions & 1 deletion prover/utils/csvtraces/csvtraces.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ type cfg struct {
nbRows int
skipPrePaddingZero bool
filterOn ifaces.Column
inHex bool
}

type Option func(*cfg) error
Expand Down Expand Up @@ -47,6 +48,12 @@ func FilterOn(col ifaces.Column) Option {
}
}

// InHex sets the CSV printer to print the values in hexadecimal
func InHex(c *cfg) error {
c.inHex = true
return nil
}

type CsvTrace struct {
mapped map[string][]field.Element

Expand Down Expand Up @@ -110,7 +117,11 @@ func FmtCsv(w io.Writer, run *wizard.ProverRuntime, cols []ifaces.Column, option
}

if assignment[c][r].IsUint64() {
fmtVals = append(fmtVals, assignment[c][r].String())
if cfg.inHex {
fmtVals = append(fmtVals, "0x"+assignment[c][r].Text(16))
} else {
fmtVals = append(fmtVals, assignment[c][r].String())
}
continue
}

Expand Down
5 changes: 4 additions & 1 deletion prover/zkevm/prover/ecpair/ecpair.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,11 +108,12 @@ func newECPair(comp *wizard.CompiledIOP, limits *Limits, ecSource *ECPairSource)
res.csInstanceIDChangeWhenNewInstance(comp)
res.csAccumulatorInit(comp)
res.csAccumulatorConsistency(comp)
res.csTotalPairs(comp)
res.csLastPairToFinalExp(comp)
res.csIndexConsistency(comp)
res.csAccumulatorMask(comp)
// only Unaligned Pairing data or G2 membership data is active at a time
res.csExclusiveUnalignedDatas(comp)
res.csPairingDataOrMembershipActive(comp)
// only to Miller loop or to FinalExp
res.csExclusivePairingCircuitMasks(comp)

Expand Down Expand Up @@ -241,6 +242,7 @@ type UnalignedPairingData struct {
ToMillerLoopCircuitMask ifaces.Column
ToFinalExpCircuitMask ifaces.Column

IsResultOfInstance ifaces.Column
IsFirstLineOfInstance ifaces.Column
IsFirstLineOfPrevAccumulator ifaces.Column
IsFirstLineOfCurrAccumulator ifaces.Column
Expand All @@ -263,6 +265,7 @@ func newUnalignedPairingData(comp *wizard.CompiledIOP, limits *Limits) *Unaligne
IsFirstLineOfInstance: createCol("IS_FIRST_LINE_OF_INSTANCE"),
IsFirstLineOfPrevAccumulator: createCol("IS_FIRST_LINE_OF_PREV_ACC"),
IsFirstLineOfCurrAccumulator: createCol("IS_FIRST_LINE_OF_CURR_ACC"),
IsResultOfInstance: createCol("IS_RESULT"),
IsAccumulatorPrev: createCol("IS_ACCUMULATOR_PREV"),
IsAccumulatorCurr: createCol("IS_ACCUMULATOR_CURR"),
IsAccumulatorInit: createCol("IS_ACCUMULATOR_INIT"),
Expand Down
109 changes: 91 additions & 18 deletions prover/zkevm/prover/ecpair/ecpair_assignment.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,10 +88,18 @@ func (ec *ECPair) assignPairingData(run *wizard.ProverRuntime) {
dstIndex = common.NewVectorBuilder(ec.UnalignedPairingData.Index)
dstIsFirstPrev = common.NewVectorBuilder(ec.UnalignedPairingData.IsFirstLineOfPrevAccumulator)
dstIsFirstCurr = common.NewVectorBuilder(ec.UnalignedPairingData.IsFirstLineOfCurrAccumulator)
dstIsResult = common.NewVectorBuilder(ec.UnalignedPairingData.IsResultOfInstance)
)

for currPos := 0; currPos < len(srcLimbs); {
// we need to check if the current position is a pairing or not. If not, then skip it.
// we need to check if the current position is a pairing or not. If not,
// then skip it.
//
// this also skips inputs to the current pairing instance which do not
// require passing to the pairing circuit (full-trivial or half-trivial
// inputs). But this is fine as it doesn't change the result as trivial
// result ML is 1. Only non-trivial input pairs affect the pairing check
// result.
if srcIsPairing[currPos].IsZero() {
currPos++
continue
Expand All @@ -100,28 +108,42 @@ func (ec *ECPair) assignPairingData(run *wizard.ProverRuntime) {
// input data. We iterate over the data to get the number of pairing
// inputs.
nbInputs := 1 // we start with 1 because we always have at least one pairing input
// we may have trivial input pairs in-between the non-trivial ones. We
// mark which inputs we are interested in.
actualInputs := []int{0} // we started when isPairing is 1, this means that we have non-trivial input.
for {
if srcIsRes[currPos+nbInputs*(nbG1Limbs+nbG2Limbs)].IsOne() {
break
}
if srcIsPairing[currPos+nbInputs*(nbG1Limbs+nbG2Limbs)].IsOne() {
actualInputs = append(actualInputs, nbInputs)
}
nbInputs++
}
nbActualTotalPairs := len(actualInputs)
// now, we have continous chunk of data that is for the pairing. Prepare it for processing.
pairingInG1 = make([][nbG1Limbs]field.Element, nbInputs)
pairingInG2 = make([][nbG2Limbs]field.Element, nbInputs)
for i := 0; i < nbInputs; i++ {
pairingInG1 = make([][nbG1Limbs]field.Element, nbActualTotalPairs)
pairingInG2 = make([][nbG2Limbs]field.Element, nbActualTotalPairs)
for ii, i := range actualInputs {
for j := 0; j < nbG1Limbs; j++ {
pairingInG1[i][j] = srcLimbs[currPos+i*(nbG1Limbs+nbG2Limbs)+j]
pairingInG1[ii][j] = srcLimbs[currPos+i*(nbG1Limbs+nbG2Limbs)+j]
}
for j := 0; j < nbG2Limbs; j++ {
pairingInG2[i][j] = srcLimbs[currPos+i*(nbG1Limbs+nbG2Limbs)+nbG1Limbs+j]
pairingInG2[ii][j] = srcLimbs[currPos+i*(nbG1Limbs+nbG2Limbs)+nbG1Limbs+j]
}
inputResult[0] = srcLimbs[currPos+(i+1)*(nbG1Limbs+nbG2Limbs)]
inputResult[1] = srcLimbs[currPos+(i+1)*(nbG1Limbs+nbG2Limbs)+1]
}
inputResult[0] = srcLimbs[currPos+nbInputs*(nbG1Limbs+nbG2Limbs)]
inputResult[1] = srcLimbs[currPos+nbInputs*(nbG1Limbs+nbG2Limbs)+1]
limbs := processPairingData(pairingInG1, pairingInG2, inputResult)
instanceId := srcID[currPos]
// processed data has the input limbs, but we have entered the intermediate Gt accumulator values

// generic assignment. We push the static values for the current instance:
// - the limbs (interleaved with accumulator values)
// - indicator for the first row of the whole pairingcheck instance
// - the instance id
// - the index of the current limb
// - activeness of the submodule
for i := 0; i < len(limbs); i++ {
dstLimb.PushField(limbs[i])
if i == 0 {
Expand All @@ -133,15 +155,24 @@ func (ec *ECPair) assignPairingData(run *wizard.ProverRuntime) {
dstIndex.PushInt(i)
dstIsActive.PushOne()
}
for i := 0; i < nbInputs-1; i++ {
// now we push the dynamic values per Miller loop. We send all valid
// pairs except the last to Miller loop (not Miller loop + finalexp!)
// circuit. Keep in mind if there is only a single valid pair then this
// loop is skipped.
for ii := range actualInputs[:len(actualInputs)-1] {
// first we indicate for the accumulator if it is the first one, previous or current
for j := 0; j < nbGtLimbs; j++ {
dstIsComputed.PushOne()
dstIsPulling.PushZero()
if i == 0 {
if ii == 0 {
// we handle first accumulator separately to be able to
// constrain that the initial accumulator value is correct.
dstIsAccInit.PushOne()
dstIsAccPrev.PushZero()
dstIsFirstPrev.PushZero()
} else {
// we're not in the first pair of points, so we indicate
// that the accumulator consistency needs to be checked.
dstIsAccInit.PushZero()
if j == 0 {
dstIsFirstPrev.PushOne()
Expand All @@ -153,6 +184,8 @@ func (ec *ECPair) assignPairingData(run *wizard.ProverRuntime) {
dstIsAccCurr.PushZero()
dstIsFirstCurr.PushZero()
}
// now we push the dynamic values for the actual inputs to the pairing check circuit (coming from the arithmetization).
// essentially we only mark that this limb came directly from arithmetization.
for j := nbGtLimbs; j < nbGtLimbs+nbG1Limbs+nbG2Limbs; j++ {
dstIsPulling.PushOne()
dstIsComputed.PushZero()
Expand All @@ -162,6 +195,7 @@ func (ec *ECPair) assignPairingData(run *wizard.ProverRuntime) {
dstIsFirstPrev.PushZero()
dstIsFirstCurr.PushZero()
}
// finally, we need to indicate that the next limbs are for the current accumulator
for j := nbGtLimbs + nbG1Limbs + nbG2Limbs; j < 2*nbGtLimbs+nbG1Limbs+nbG2Limbs; j++ {
dstIsComputed.PushOne()
dstIsPulling.PushZero()
Expand All @@ -175,54 +209,92 @@ func (ec *ECPair) assignPairingData(run *wizard.ProverRuntime) {
}
dstIsAccCurr.PushOne()
}
// we also set the static values for all limbs in this pairs of points. These are:
// - true mark for miller loop circuit
// - false mark for the ML+finalexp circuit
// - the pair ID
// - the total number of pairs
// - false mark that current limb is for the result
for j := 0; j < nbG1Limbs+nbG2Limbs+2*nbGtLimbs; j++ {
dstToMillerLoop.PushOne()
dstToFinalExp.PushZero()
dstPairId.PushInt(i + 1)
dstTotalPairs.PushInt(nbInputs)
dstPairId.PushInt(ii + 1)
dstTotalPairs.PushInt(nbActualTotalPairs)
dstIsResult.PushZero()
}
}
// we need to handle the final pair of points separately. The
// ML+finalexp circuit does not take the current accumulator as an
// input, but rather the expected pairing check result.
//
// first we set the masks for the accumulator limbs.
for j := 0; j < nbGtLimbs; j++ {
dstIsComputed.PushOne()
dstIsPulling.PushZero()
dstPairId.PushInt(nbInputs)
dstIsAccInit.PushZero()
dstIsAccPrev.PushOne()
dstPairId.PushInt(nbActualTotalPairs)
// handle separately the case when there is only one valid input
// pair. In this case, the first valid pair also includes the
// accumulator initialization.
if nbActualTotalPairs == 1 {
dstIsAccInit.PushOne()
dstIsAccPrev.PushZero()
} else {
dstIsAccInit.PushZero()
dstIsAccPrev.PushOne()
}
dstIsAccCurr.PushZero()
if j == 0 {
dstIsFirstPrev.PushOne()
// handle separately the case when there is only one valid
// input. In this case we don't have the previous accumulator.
if nbActualTotalPairs == 1 {
dstIsFirstPrev.PushZero()
} else {
dstIsFirstPrev.PushOne()
}
} else {
dstIsFirstPrev.PushZero()
}
dstIsFirstCurr.PushZero()
dstIsResult.PushZero()
}
// similarly for the final pair of points, we need to indicate that the
// G1/G2 points come directly from the arithmetization.
for j := nbGtLimbs; j < nbGtLimbs+nbG1Limbs+nbG2Limbs; j++ {
dstIsPulling.PushOne()
dstIsComputed.PushZero()
dstPairId.PushInt(nbInputs)
dstPairId.PushInt(nbActualTotalPairs)
dstIsAccInit.PushZero()
dstIsAccPrev.PushZero()
dstIsAccCurr.PushZero()
dstIsFirstPrev.PushZero()
dstIsFirstCurr.PushZero()
dstIsResult.PushZero()
}
// finally, we need to indicate that the result of the pairing check
// comes directly from the arithmetization. this is a bit explicit loop,
// but it's easier to understand.
for j := nbGtLimbs + nbG1Limbs + nbG2Limbs; j < nbGtLimbs+nbG1Limbs+nbG2Limbs+2; j++ {
dstIsPulling.PushOne()
dstIsComputed.PushZero()
// NB! for the result the Pair ID is 0. This is important to keep in
// mind as we set some constraints based on this.
dstPairId.PushZero()
dstIsAccInit.PushZero()
dstIsAccPrev.PushZero()
dstIsAccCurr.PushZero()
dstIsFirstPrev.PushZero()
dstIsFirstCurr.PushZero()
dstIsResult.PushOne()
}
// finally we set the static masks for the final pair of points.
for j := 0; j < nbG1Limbs+nbG2Limbs+nbGtLimbs+2; j++ {
dstToFinalExp.PushOne()
dstToMillerLoop.PushZero()
dstTotalPairs.PushInt(nbInputs)
dstTotalPairs.PushInt(nbActualTotalPairs)
}
currPos += nbInputs*(nbG1Limbs+nbG2Limbs) + 2
}
// Finally, we pad and assign the assigned data.
dstIsActive.PadAndAssign(run, field.Zero())
dstLimb.PadAndAssign(run, field.Zero())
dstPairId.PadAndAssign(run, field.Zero())
Expand All @@ -239,6 +311,7 @@ func (ec *ECPair) assignPairingData(run *wizard.ProverRuntime) {
dstIndex.PadAndAssign(run, field.Zero())
dstIsFirstPrev.PadAndAssign(run, field.Zero())
dstIsFirstCurr.PadAndAssign(run, field.Zero())
dstIsResult.PadAndAssign(run, field.Zero())
}

func processPairingData(pairingInG1 [][nbG1Limbs]field.Element, pairingInG2 [][nbG2Limbs]field.Element, inputResult [2]field.Element) []field.Element {
Expand Down
40 changes: 32 additions & 8 deletions prover/zkevm/prover/ecpair/ecpair_constraints.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,8 @@ func (ec *ECPair) csProjections(comp *wizard.CompiledIOP) {
// we project data from the arithmetization correctly to the unaligned part of the circuit
projection.InsertProjection(
comp, ifaces.QueryIDf("%v_PROJECTION_PAIRING", nameECPair),
[]ifaces.Column{ec.ECPairSource.Limb, ec.ECPairSource.AccPairings, ec.ECPairSource.TotalPairings, ec.ECPairSource.ID},
[]ifaces.Column{ec.UnalignedPairingData.Limb, ec.UnalignedPairingData.PairID, ec.UnalignedPairingData.TotalPairs, ec.UnalignedPairingData.InstanceID},
[]ifaces.Column{ec.ECPairSource.Limb, ec.ECPairSource.ID, ec.ECPairSource.IsEcPairingResult},
[]ifaces.Column{ec.UnalignedPairingData.Limb, ec.UnalignedPairingData.InstanceID, ec.UnalignedPairingData.IsResultOfInstance},
ec.ECPairSource.CsEcpairing,
ec.UnalignedPairingData.IsPulling,
)
Expand Down Expand Up @@ -159,6 +159,23 @@ func (ec *ECPair) csAccumulatorConsistency(comp *wizard.CompiledIOP) {
)
}

func (ec *ECPair) csTotalPairs(comp *wizard.CompiledIOP) {
// total pairs corresponds to the number of pairs in the instance. for this
// we check that when the limb corresponds to the result, then the PairID of
// the shifted by two corresponds to the total pairs. the limb corresponds
// to the result when its PairID is 0 (for input pairs the indexing starts
// from 1).
comp.InsertGlobal(
roundNr,
ifaces.QueryIDf("%v_TOTAL_PAIRS", nameECPair),
sym.Mul(
ec.UnalignedPairingData.IsActive,
ec.UnalignedPairingData.IsResultOfInstance,
sym.Sub(ec.UnalignedPairingData.TotalPairs, column.Shift(ec.UnalignedPairingData.PairID, -2)), // we have two limbs for the result, shift by two gets to the input
),
)
}

func (ec *ECPair) csLastPairToFinalExp(comp *wizard.CompiledIOP) {
// if the last pair then the final exp circuit should be active

Expand Down Expand Up @@ -191,7 +208,6 @@ func (ec *ECPair) csIndexConsistency(comp *wizard.CompiledIOP) {
ifaces.QueryIDf("%v_INDEX_INCREMENT", nameECPair),
sym.Mul(
ec.UnalignedPairingData.IsActive,
sym.Sub(1, ec.UnalignedG2MembershipData.IsPulling, ec.UnalignedG2MembershipData.IsComputed), // we dont use index in the G2 membership check
sym.Sub(1, ec.UnalignedPairingData.IsFirstLineOfInstance),
sym.Sub(ec.UnalignedPairingData.Index, column.Shift(ec.UnalignedPairingData.Index, -1), 1),
),
Expand Down Expand Up @@ -276,11 +292,19 @@ func (ec *ECPair) csAccumulatorMask(comp *wizard.CompiledIOP) {
)
}

func (ec *ECPair) csExclusiveUnalignedDatas(comp *wizard.CompiledIOP) {
common.MustBeMutuallyExclusiveBinaryFlags(comp, ec.IsActive, []ifaces.Column{
ec.UnalignedG2MembershipData.ToG2MembershipCircuitMask,
ec.UnalignedPairingData.IsActive,
})
func (ec *ECPair) csPairingDataOrMembershipActive(comp *wizard.CompiledIOP) {
// when module is active, then either pairing data or membership data is
// active. Can also be both.
comp.InsertGlobal(
roundNr,
ifaces.QueryIDf("%v_PAIRING_OR_MEMBERSHIP_ACTIVE", nameECPair),
sym.Add(
ec.IsActive,
sym.Neg(ec.UnalignedPairingData.IsActive),
sym.Neg(ec.UnalignedG2MembershipData.ToG2MembershipCircuitMask),
sym.Mul(ec.UnalignedPairingData.IsActive, ec.UnalignedG2MembershipData.ToG2MembershipCircuitMask),
),
)
}

func (ec *ECPair) csExclusivePairingCircuitMasks(comp *wizard.CompiledIOP) {
Expand Down
Loading

0 comments on commit 05d3ee2

Please sign in to comment.