From d0a25364ab7fe1b4f9f3cb5720f6022e146228bd Mon Sep 17 00:00:00 2001 From: Azam Soleimanian <49027816+Soleimani193@users.noreply.github.com> Date: Mon, 23 Sep 2024 09:50:31 +0200 Subject: [PATCH] Prover: stitching compiler (#39) * scanning the compiler trace for the eligible column * committing to the eligible columns * replacing the eligible subcolumns with their stitching * local opening constraints * eligible expression for the compilation * ignoring the queries over the eligible columns * local constraints *global constraints * supporting the verifier col in the expression * expanding the verifier columns per expression * adding the verifier's checks for the very small columns --------- Signed-off-by: Leo Jeong Co-authored-by: Leo Jeong --- .../common/smartvectors/arithmetic_test.go | 3 +- .../column/verifiercol/expand_verifcol.go | 90 ++++++ .../column/verifiercol/from_accessors.go | 2 +- .../compiler/splitter/splitter/common.go | 121 +++++++ .../splitter/splitter/stitcher/constraints.go | 233 ++++++++++++++ .../splitter/splitter/stitcher/stitcher.go | 301 ++++++++++++++++++ .../splitter/stitcher/stitcher_test.go | 296 +++++++++++++++++ prover/protocol/query/local.go | 5 +- 8 files changed, 1047 insertions(+), 4 deletions(-) create mode 100644 prover/protocol/column/verifiercol/expand_verifcol.go create mode 100644 prover/protocol/compiler/splitter/splitter/common.go create mode 100644 prover/protocol/compiler/splitter/splitter/stitcher/constraints.go create mode 100644 prover/protocol/compiler/splitter/splitter/stitcher/stitcher.go create mode 100644 prover/protocol/compiler/splitter/splitter/stitcher/stitcher_test.go diff --git a/prover/maths/common/smartvectors/arithmetic_test.go b/prover/maths/common/smartvectors/arithmetic_test.go index 063659303..4d9b24a9e 100644 --- a/prover/maths/common/smartvectors/arithmetic_test.go +++ b/prover/maths/common/smartvectors/arithmetic_test.go @@ -237,7 +237,8 @@ func TestOpBasicEdgeCases(t *testing.T) { t.Run(fmt.Sprintf("case-%v", i), func(t *testing.T) { t.Logf("test-case details: %v", testCase.explainer) res := testCase.fn(testCase.inputs...).(*Pooled) - require.Equal(t, testCase.expectedRes, &res.Regular, "expectedRes=%v\nres=%v", testCase.expectedRes.Pretty(), res.Pretty()) + actual := NewRegular(res.Regular) + require.Equal(t, testCase.expectedRes, actual, "expectedRes=%v\nres=%v", testCase.expectedRes.Pretty(), res.Pretty()) }) } } diff --git a/prover/protocol/column/verifiercol/expand_verifcol.go b/prover/protocol/column/verifiercol/expand_verifcol.go new file mode 100644 index 000000000..b984cc3e5 --- /dev/null +++ b/prover/protocol/column/verifiercol/expand_verifcol.go @@ -0,0 +1,90 @@ +package verifiercol + +import ( + "github.com/consensys/gnark/frontend" + "github.com/consensys/linea-monorepo/prover/maths/common/smartvectors" + "github.com/consensys/linea-monorepo/prover/maths/common/vector" + "github.com/consensys/linea-monorepo/prover/maths/field" + "github.com/consensys/linea-monorepo/prover/protocol/ifaces" + "github.com/consensys/linea-monorepo/prover/protocol/wizard" +) + +// compile check to enforce the struct to belong to the corresponding interface +var _ VerifierCol = ExpandedVerifCol{} + +type ExpandedVerifCol struct { + Verifiercol VerifierCol + Expansion int +} + +// Round returns the round ID of the column and implements the [ifaces.Column] +// interface. +func (ex ExpandedVerifCol) Round() int { + return ex.Verifiercol.Round() +} + +// GetColID returns the column ID +func (ex ExpandedVerifCol) GetColID() ifaces.ColID { + return ifaces.ColIDf("Expanded_%v", ex.Verifiercol.GetColID()) +} + +// MustExists implements the [ifaces.Column] interface and always returns true. +func (ex ExpandedVerifCol) MustExists() { + ex.Verifiercol.MustExists() +} + +// Size returns the size of the colum and implements the [ifaces.Column] +// interface. +func (ex ExpandedVerifCol) Size() int { + return ex.Verifiercol.Size() * ex.Expansion +} + +// GetColAssignment returns the assignment of the current column +func (ex ExpandedVerifCol) GetColAssignment(run ifaces.Runtime) ifaces.ColAssignment { + assi := ex.Verifiercol.GetColAssignment(run) + values := make([][]field.Element, ex.Expansion) + for j := range values { + values[j] = smartvectors.IntoRegVec(assi) + } + res := vector.Interleave(values...) + return smartvectors.NewRegular(res) +} + +// GetColAssignment returns a gnark assignment of the current column +func (ex ExpandedVerifCol) GetColAssignmentGnark(run ifaces.GnarkRuntime) []frontend.Variable { + + assi := ex.Verifiercol.GetColAssignmentGnark(run) + res := make([]frontend.Variable, ex.Size()) + for i := 0; i < len(assi); i++ { + for j := 0; j < ex.Expansion; j++ { + res[j+i*ex.Expansion] = assi[i] + } + } + return res +} + +// GetColAssignmentAt returns a particular position of the column +func (ex ExpandedVerifCol) GetColAssignmentAt(run ifaces.Runtime, pos int) field.Element { + return ex.Verifiercol.GetColAssignmentAt(run, pos/ex.Expansion) +} + +// GetColAssignmentGnarkAt returns a particular position of the column in a gnark circuit +func (ex ExpandedVerifCol) GetColAssignmentGnarkAt(run ifaces.GnarkRuntime, pos int) frontend.Variable { + + return ex.GetColAssignmentGnarkAt(run, pos/ex.Expansion) +} + +// IsComposite implements the [ifaces.Column] interface +func (ex ExpandedVerifCol) IsComposite() bool { + return ex.Verifiercol.IsComposite() +} + +// String implements the [symbolic.Metadata] interface +func (ex ExpandedVerifCol) String() string { + return ex.Verifiercol.String() +} + +// Split implements the [VerifierCol] interface +func (ex ExpandedVerifCol) Split(_ *wizard.CompiledIOP, from, to int) ifaces.Column { + return ex.Verifiercol +} diff --git a/prover/protocol/column/verifiercol/from_accessors.go b/prover/protocol/column/verifiercol/from_accessors.go index 2eea330c7..2f2d8172a 100644 --- a/prover/protocol/column/verifiercol/from_accessors.go +++ b/prover/protocol/column/verifiercol/from_accessors.go @@ -123,7 +123,7 @@ func (f FromAccessors) IsComposite() bool { return false } -// IsComposite implements the [symbolic.Metadata] interface +// String implements the [symbolic.Metadata] interface func (f FromAccessors) String() string { return string(f.GetColID()) } diff --git a/prover/protocol/compiler/splitter/splitter/common.go b/prover/protocol/compiler/splitter/splitter/common.go new file mode 100644 index 000000000..ba23ede5a --- /dev/null +++ b/prover/protocol/compiler/splitter/splitter/common.go @@ -0,0 +1,121 @@ +package alliance + +import ( + "github.com/consensys/linea-monorepo/prover/protocol/column" + "github.com/consensys/linea-monorepo/prover/protocol/ifaces" + "github.com/consensys/linea-monorepo/prover/symbolic" +) + +// It stores the information regarding an alliance between a BigCol and a set of SubColumns. +// The subject of alliance can be either stitching or splitting. +type Alliance struct { + // the bigCol in the alliance; + // - for stitching, it is the result of stitching of the subColumns. + // - for splitting, it is split to the sub Columns. + BigCol ifaces.Column + // sub columns allied with the bigCol + SubCols []ifaces.Column + // the Round in which the alliance is created. + Round int + // Status of the sub columns + // the only valid Status for the eligible sub columns are; + // committed, Precomputed, VerifierDefined + Status column.Status +} + +// It summarizes the information about all the alliances in a single round of PIOP. +type SummerizedAlliances struct { + // associate a group of the sub columns to their splitting + ByBigCol map[ifaces.ColID][]ifaces.Column + // for a sub column, it indicates its splitting column and its position in the splitting. + BySubCol map[ifaces.ColID]struct { + NameBigCol ifaces.ColID + PosInBigCol int + } +} + +// The summary of all the alliances round-by-round. +type MultiSummary []SummerizedAlliances + +// It inserts the new alliance into the summary. +func (summary MultiSummary) InsertNew(s Alliance) { + // Initialize the bySubCol if necessary + if summary[s.Round].BySubCol == nil { + summary[s.Round].BySubCol = map[ifaces.ColID]struct { + NameBigCol ifaces.ColID + PosInBigCol int + }{} + } + + // Populate the bySubCol + for posInNew, c := range s.SubCols { + summary[s.Round].BySubCol[c.GetColID()] = struct { + NameBigCol ifaces.ColID + PosInBigCol int + }{ + NameBigCol: s.BigCol.GetColID(), + PosInBigCol: posInNew, + } + } + + // Initialize ByBigCol if necessary + if summary[s.Round].ByBigCol == nil { + summary[s.Round].ByBigCol = make(map[ifaces.ColID][]ifaces.Column) + } + // populate ByBigCol + summary[s.Round].ByBigCol[s.BigCol.GetColID()] = s.SubCols +} + +// It checks if the expression is over a set of the columns eligible to the stitching. +// Namely, it contains columns of proper size with status Precomputed, Committed, or Verifiercol. +// It panics if the expression includes a mixture of eligible columns and columns with status Proof/VerifiyingKey/Ignored. +// +// If all the columns are verifierCol the expression is not eligible to the compilation. +// This is an expected behavior, since the verifier checks such expression by itself. +func IsExprEligible( + isColEligible func(MultiSummary, ifaces.Column) bool, + stitchings MultiSummary, + board symbolic.ExpressionBoard, +) bool { + metadata := board.ListVariableMetadata() + hasAtLeastOneEligible := false + allAreEligible := true + allAreVeriferCol := true + for i := range metadata { + switch m := metadata[i].(type) { + // reminder: [verifiercol.VerifierCol] , [column.Natural] and [column.Shifted] + // all implement [ifaces.Column] + case ifaces.Column: // it is a Committed, Precomputed or verifierCol + natural := column.RootParents(m)[0] + switch natural.(type) { + case column.Natural: // then it is not a verifiercol + allAreVeriferCol = false + b := isColEligible(stitchings, m) + + hasAtLeastOneEligible = hasAtLeastOneEligible || b + allAreEligible = allAreEligible && b + if m.Size() == 0 { + panic("found no columns in the expression") + } + } + + } + + } + + if hasAtLeastOneEligible && !allAreEligible { + // 1. we expect no expression including Proof columns + // 2. we expect no expression over ignored columns + // 3. we expect no VerifiyingKey withing the stitching range. + panic("the expression is not valid, it is mixed with invalid columns of status Proof/Ingnored/verifierKey") + } + if allAreVeriferCol { + // 4. we expect no expression involving only and only the verifierCols. + // We expect that this case wont happen. + // Otherwise should be handled in the [github.com/consensys/linea-monorepo/prover/protocol/query] package. + // Namely, Local/Global queries should be checked directly by the verifer. + panic("all the columns in the expression are verifierCols, unsupported by the compiler") + } + + return hasAtLeastOneEligible +} diff --git a/prover/protocol/compiler/splitter/splitter/stitcher/constraints.go b/prover/protocol/compiler/splitter/splitter/stitcher/constraints.go new file mode 100644 index 000000000..41e032be3 --- /dev/null +++ b/prover/protocol/compiler/splitter/splitter/stitcher/constraints.go @@ -0,0 +1,233 @@ +package stitcher + +import ( + "github.com/consensys/gnark/frontend" + "github.com/consensys/linea-monorepo/prover/protocol/coin" + "github.com/consensys/linea-monorepo/prover/protocol/column" + "github.com/consensys/linea-monorepo/prover/protocol/column/verifiercol" + alliance "github.com/consensys/linea-monorepo/prover/protocol/compiler/splitter/splitter" + "github.com/consensys/linea-monorepo/prover/protocol/ifaces" + "github.com/consensys/linea-monorepo/prover/protocol/query" + "github.com/consensys/linea-monorepo/prover/protocol/variables" + "github.com/consensys/linea-monorepo/prover/protocol/wizard" + "github.com/consensys/linea-monorepo/prover/symbolic" + "github.com/consensys/linea-monorepo/prover/utils" + "github.com/consensys/linea-monorepo/prover/utils/collection" +) + +func (ctx stitchingContext) constraints() { + ctx.LocalOpening() + ctx.LocalGlobalConstraints() +} + +func (ctx stitchingContext) LocalOpening() { + + // Ignore the LocalOpening queries over the subColumns. + for _, qName := range ctx.comp.QueriesParams.AllUnignoredKeys() { + // Filters out only the LocalOpening + q, ok := ctx.comp.QueriesParams.Data(qName).(query.LocalOpening) + if !ok { + utils.Panic("got an uncompilable query %v", qName) + } + + round := ctx.comp.QueriesParams.Round(q.ID) + + if q.Pol.Size() < ctx.MinSize { + //sanity-check: column should be public + verifiercol.AssertIsPublicCol(ctx.comp, q.Pol) + // Ask the verifier to directly check the query + insertVerifier(ctx.comp, q, round) + // mark the query as ignored + ctx.comp.QueriesParams.MarkAsIgnored(q.ID) + + // And skip the rest of the compilation : we are done + continue + } + + if !isColEligible(ctx.Stitchings, q.Pol) { + continue + } + // mark the query as ignored + ctx.comp.QueriesParams.MarkAsIgnored(qName) + + // get the stitching column associated with the sub column q.Poly. + stitchingCol := getStitchingCol(ctx, q.Pol) + + newQ := ctx.comp.InsertLocalOpening(round, queryName(q.ID), stitchingCol) + + // Registers the prover's step responsible for assigning the new query + ctx.comp.SubProvers.AppendToInner(round, func(run *wizard.ProverRuntime) { + y := run.QueriesParams.MustGet(q.ID).(query.LocalOpeningParams).Y + run.AssignLocalPoint(newQ.ID, y) + }) + } + +} + +func (ctx stitchingContext) LocalGlobalConstraints() { + for _, qName := range ctx.comp.QueriesNoParams.AllUnignoredKeys() { + + q := ctx.comp.QueriesNoParams.Data(qName) + // round of definition of the query to compile + round := ctx.comp.QueriesNoParams.Round(qName) + + var board symbolic.ExpressionBoard + + switch q := q.(type) { + case query.LocalConstraint: + board = q.Board() + if q.DomainSize < ctx.MinSize { + // Sanity-check : at this point all the parameters of the query + // should have a public status. Indeed, prior to compiling the + // constraints to work + metadatas := board.ListVariableMetadata() + for _, metadata := range metadatas { + if h, ok := metadata.(ifaces.Column); ok { + verifiercol.AssertIsPublicCol(ctx.comp, h) + } + } + insertVerifier(ctx.comp, q, round) + // mark the query as ignored + ctx.comp.QueriesNoParams.MarkAsIgnored(qName) + continue + } + // detect if the expression is eligible; + // i.e., it contains columns of proper size with status Precomputed, committed, or verifiercol. + if !alliance.IsExprEligible(isColEligible, ctx.Stitchings, board) { + continue + } + + // if the associated expression is eligible to the stitching, mark the query, over the sub columns, as ignored. + ctx.comp.QueriesNoParams.MarkAsIgnored(qName) + + // adjust the query over the stitching columns + ctx.comp.InsertLocal(round, queryName(qName), ctx.adjustExpression(q.Expression, false)) + + case query.GlobalConstraint: + board = q.Board() + if q.DomainSize < ctx.MinSize { + + // Sanity-check : at this point all the parameters of the query + // should have a public status. Indeed, prior to compiling the + // constraints to work + metadatas := board.ListVariableMetadata() + for _, metadata := range metadatas { + if h, ok := metadata.(ifaces.Column); ok { + verifiercol.AssertIsPublicCol(ctx.comp, h) + } + } + insertVerifier(ctx.comp, q, round) + // mark the query as ignored + ctx.comp.QueriesNoParams.MarkAsIgnored(qName) + continue + } + // detect if the expression is over the eligible columns. + if !alliance.IsExprEligible(isColEligible, ctx.Stitchings, board) { + continue + } + + // if the associated expression is eligible to the stitching, mark the query, over the sub columns, as ignored. + ctx.comp.QueriesNoParams.MarkAsIgnored(qName) + + // adjust the query over the stitching columns + ctx.comp.InsertGlobal(round, queryName(qName), + ctx.adjustExpression(q.Expression, true), + q.NoBoundCancel) + + default: + utils.Panic("got an uncompilable query %++v", qName) + } + } +} + +// Takes a sub column and returns the stitching column. +// the stitching column is shifted such that the first row agrees with the first row of the sub column. +// more detailed, such stitching column agrees with the the sub column up to a subsampling with offset zero. +func getStitchingCol(ctx stitchingContext, col ifaces.Column) ifaces.Column { + + switch m := col.(type) { + case verifiercol.VerifierCol: + scaling := ctx.MaxSize / col.Size() + return verifiercol.ExpandedVerifCol{ + Verifiercol: m, + Expansion: scaling, + } + } + + // Extract the assumedly single col + natural := column.RootParents(col)[0] + + round := col.Round() + subColInfo := ctx.Stitchings[round].BySubCol[natural.GetColID()] + stitchingCol := ctx.comp.Columns.GetHandle(subColInfo.NameBigCol) + + // Shift the stitching column by the right position + position := column.StackOffsets(col) + + scaling := stitchingCol.Size() / natural.Size() + newPosition := scaling*position + subColInfo.PosInBigCol + + return column.Shift(stitchingCol, newPosition) +} + +func queryName(oldQ ifaces.QueryID) ifaces.QueryID { + return ifaces.QueryIDf("%v_STITCHER", oldQ) +} + +// it adjusts the expression, that is among sub columns, by replacing the sub columns with their stitching columns. +// for the verfiercol instead of stitching, they are expanded to reach the proper size. +// This is due to the fact that the verifiercols are not tracked by the compiler and can not be stitched +// via [scanAndClassifyEligibleColumns]. +func (ctx *stitchingContext) adjustExpression( + expr *symbolic.Expression, + isGlobalConstraint bool, +) ( + newExpr *symbolic.Expression, +) { + + board := expr.Board() + metadata := board.ListVariableMetadata() + replaceMap := collection.NewMapping[string, *symbolic.Expression]() + domainSize := 0 + + for i := range metadata { + switch m := metadata[i].(type) { + case ifaces.Column: + // it's always a compiled column + domainSize = m.Size() + stitchingCol := getStitchingCol(*ctx, m) + replaceMap.InsertNew(m.String(), ifaces.ColumnAsVariable(stitchingCol)) + case coin.Info, ifaces.Accessor: + replaceMap.InsertNew(m.String(), symbolic.NewVariable(m)) + case variables.X: + panic("unsupported, the value of `x` in the unsplit query and the split would be different") + case variables.PeriodicSample: + // there, we need to inflate the period and the offset + scaling := ctx.MaxSize / domainSize + replaceMap.InsertNew(m.String(), variables.NewPeriodicSample(m.T*scaling, m.Offset*scaling)) + } + } + + newExpr = expr.Replay(replaceMap) + if isGlobalConstraint { + // for the global constraints, check the constraint only over the subSampeling of the columns. + newExpr = symbolic.Mul(newExpr, variables.NewPeriodicSample(ctx.MaxSize/domainSize, 0)) + } + + return newExpr +} + +func insertVerifier( + comp *wizard.CompiledIOP, + q ifaces.Query, + round int, +) { + + // Requires the verifier to verify the query itself + comp.InsertVerifier(round, func(vr *wizard.VerifierRuntime) error { + return q.Check(vr) + }, func(api frontend.API, wvc *wizard.WizardVerifierCircuit) { + q.CheckGnark(api, wvc) + }) + +} diff --git a/prover/protocol/compiler/splitter/splitter/stitcher/stitcher.go b/prover/protocol/compiler/splitter/splitter/stitcher/stitcher.go new file mode 100644 index 000000000..982474f25 --- /dev/null +++ b/prover/protocol/compiler/splitter/splitter/stitcher/stitcher.go @@ -0,0 +1,301 @@ +package stitcher + +import ( + "strings" + + "github.com/consensys/linea-monorepo/prover/maths/common/smartvectors" + "github.com/consensys/linea-monorepo/prover/maths/common/vector" + "github.com/consensys/linea-monorepo/prover/maths/field" + "github.com/consensys/linea-monorepo/prover/protocol/column" + "github.com/consensys/linea-monorepo/prover/protocol/column/verifiercol" + alliance "github.com/consensys/linea-monorepo/prover/protocol/compiler/splitter/splitter" + "github.com/consensys/linea-monorepo/prover/protocol/ifaces" + "github.com/consensys/linea-monorepo/prover/protocol/wizard" + "github.com/consensys/linea-monorepo/prover/utils" + "github.com/consensys/linea-monorepo/prover/utils/profiling" +) + +type stitchingContext struct { + // The compiled IOP + comp *wizard.CompiledIOP + // All columns under the minSize are ignored. + // No stitching goes beyond MaxSize. + MinSize, MaxSize int + + // It collects the information about subColumns and their stitchings. + // The index of Stitchings is over the rounds. + Stitchings []alliance.SummerizedAlliances +} + +// Stitcher applies the stitching over the eligible sub columns and adjusts the constraints accordingly. +func Stitcher(minSize, maxSize int) func(comp *wizard.CompiledIOP) { + + return func(comp *wizard.CompiledIOP) { + // it creates stitchings from the eligible columns and commits to the them. + ctx := newStitcher(comp, minSize, maxSize) + + // adjust the constraints accordingly over the stitchings of the sub columns. + ctx.constraints() + + // it assigns the stitching columns and delete the assignment of the sub columns. + comp.SubProvers.AppendToInner(comp.NumRounds()-1, func(run *wizard.ProverRuntime) { + for round := range comp.NumRounds() { + for subCol := range ctx.Stitchings[round].BySubCol { + run.Columns.TryDel(subCol) + } + } + }) + } +} + +// it commits to the stitchings of the eligible sub columns. +func newStitcher(comp *wizard.CompiledIOP, minSize, maxSize int) stitchingContext { + numRounds := comp.NumRounds() + res := stitchingContext{ + comp: comp, + MinSize: minSize, + MaxSize: maxSize, + // initialize the stitichings + Stitchings: make([]alliance.SummerizedAlliances, numRounds), + } + // it scans the compiler trace for the eligible columns, creates stitchings from the sub columns and commits to the them. + res.ScanStitchCommit() + return res +} + +// ScanStitchCommit scans compiler trace and classifies the sub columns eligible to the stitching. +// It then stitches the sub columns, commits to them and update stitchingContext. +// It also forces the compiler to set the status of the sub columns to 'ignored'. +// since the sub columns are technically replaced with their stitching. +func (ctx *stitchingContext) ScanStitchCommit() { + for round := 0; round < ctx.comp.NumRounds(); round++ { + + // scan the compiler trace to find the eligible columns for stitching + columnsBySize := scanAndClassifyEligibleColumns(*ctx, round) + + for size, cols := range columnsBySize { + + var ( + precomputedCols = make([]ifaces.Column, 0, len(cols)) + committedCols = make([]ifaces.Column, 0, len(cols)) + ) + + // collect the the columns with valid status; Precomputed, committed + // verifierDefined is valid but is not present in the compiler trace we handle it directly during the constraints. + for _, col := range cols { + status := ctx.comp.Columns.Status(col.GetColID()) + switch status { + case column.Precomputed: + precomputedCols = append(precomputedCols, col) + case column.Committed: + committedCols = append(committedCols, col) + + default: + // note that status of verifercol/ veriferDefined is not available via compiler trace. + utils.Panic("found the column %v with the invalid status %v for stitching", col.GetColID(), status.String()) + } + + // Mark it as ignored, so that it is no longer considered as + // queryable (since we are replacing it with its stitching). + ctx.comp.Columns.MarkAsIgnored(col.GetColID()) + } + + if len(precomputedCols) != 0 { + // classify the columns to the groups, each of size ctx.MaxSize + preComputedGroups := groupCols(precomputedCols, ctx.MaxSize/size) + + for _, group := range preComputedGroups { + // prepare a group for stitching + stitching := alliance.Alliance{ + SubCols: group, + Round: round, + Status: column.Precomputed, + } + // stitch the group + ctx.stitchGroup(stitching) + } + } + + if len(committedCols) != 0 { + committedGroups := groupCols(committedCols, ctx.MaxSize/size) + + for _, group := range committedGroups { + stitching := alliance.Alliance{ + SubCols: group, + Round: round, + Status: column.Committed, + } + ctx.stitchGroup(stitching) + + } + } + + } + // @Azam Precomputed ones are double assigned by this? + ctx.comp.SubProvers.AppendToInner(round, func(run *wizard.ProverRuntime) { + stopTimer := profiling.LogTimer("stitching compiler") + defer stopTimer() + for idBigCol, subColumns := range ctx.Stitchings[round].ByBigCol { + + // Sanity-check + sizeBigCol := ctx.comp.Columns.GetHandle(idBigCol).Size() + if sizeBigCol != ctx.MaxSize { + utils.Panic("Unexpected size %v != %v", sizeBigCol, ctx.MaxSize) + } + + // If the column is precomputed, it is already assigned + if ctx.comp.Precomputed.Exists(idBigCol) { + continue + } + + // get the assignment of the subColumns and interleave them + witnesses := make([]smartvectors.SmartVector, len(subColumns)) + for i := range witnesses { + witnesses[i] = subColumns[i].GetColAssignment(run) + } + assignement := smartvectors. + AllocateRegular(len(subColumns) * witnesses[0].Len()).(*smartvectors.Regular) + for i := range subColumns { + for j := 0; j < witnesses[0].Len(); j++ { + (*assignement)[i+j*len(subColumns)] = witnesses[i].Get(j) + } + } + run.AssignColumn(idBigCol, assignement) + } + }) + } +} + +// It scan the compiler trace for a given round and classifies the columns eligible to the stitching, by their size. +func scanAndClassifyEligibleColumns(ctx stitchingContext, round int) map[int][]ifaces.Column { + columnsBySize := map[int][]ifaces.Column{} + + for _, colName := range ctx.comp.Columns.AllKeysAt(round) { + + status := ctx.comp.Columns.Status(colName) + col := ctx.comp.Columns.GetHandle(colName) + + // 1. we expect no constraint over a mix of eligible columns and proof, thus ignore Proof columns + // 2. we expect no verifingKey column to fall withing the stitching interval (ctx.MinSize, ctx.MaxSize) + // 3. we expect no query over the ignored columns. + if status == column.Ignored || status == column.Proof || status == column.VerifyingKey { + continue + } + + // If the column is too big, the stitcher does not manipulate the column. + if col.Size() >= ctx.MaxSize { + continue + } + + // If the column is very small, make it public. + if col.Size() < ctx.MinSize { + if status.IsPublic() { + // Nothing to do : the column is already public and we will ask the + // verifier to perform the operation itself. + continue + } + ctx.makeColumnPublic(col, status) + continue + } + // Initialization clause of `sizes` + if _, ok := columnsBySize[col.Size()]; !ok { + columnsBySize[col.Size()] = []ifaces.Column{} + } + + columnsBySize[col.Size()] = append(columnsBySize[col.Size()], col) + } + return columnsBySize +} + +// group the cols with the same size +func groupCols(cols []ifaces.Column, numToStitch int) (groups [][]ifaces.Column) { + + numGroups := utils.DivCeil(len(cols), numToStitch) + groups = make([][]ifaces.Column, numGroups) + + size := cols[0].Size() + + for i, col := range cols { + if col.Size() != size { + utils.Panic( + "column %v of size %v has been grouped with %v of size %v", + col.GetColID(), col.Size(), cols[0].GetColID(), cols[0].Size(), + ) + } + groups[i/numToStitch] = append(groups[i/numToStitch], col) + } + + lastGroup := &groups[len(groups)-1] + zeroCol := verifiercol.NewConstantCol(field.Zero(), size) + + for i := len(*lastGroup); i < numToStitch; i++ { + *lastGroup = append(*lastGroup, zeroCol) + } + + return groups +} + +func groupedName(group []ifaces.Column) ifaces.ColID { + fmtted := make([]string, len(group)) + for i := range fmtted { + fmtted[i] = group[i].String() + } + return ifaces.ColIDf("STITCHER_%v", strings.Join(fmtted, "_")) +} + +// for a group of sub columns it creates their stitching. +func (ctx *stitchingContext) stitchGroup(s alliance.Alliance) { + var ( + group = s.SubCols + stitchingCol ifaces.Column + status = s.Status + ) + // Declare the new columns + switch status { + case column.Precomputed: + values := make([][]field.Element, len(group)) + for j := range values { + values[j] = smartvectors.IntoRegVec(ctx.comp.Precomputed.MustGet(group[j].GetColID())) + } + assignement := vector.Interleave(values...) + stitchingCol = ctx.comp.InsertPrecomputed( + groupedName(group), + smartvectors.NewRegular(assignement), + ) + case column.Committed: + stitchingCol = ctx.comp.InsertCommit( + s.Round, + groupedName(s.SubCols), + ctx.MaxSize, + ) + + default: + panic("The status is not valid for the stitching") + + } + + s.BigCol = stitchingCol + (alliance.MultiSummary)(ctx.Stitchings).InsertNew(s) +} + +// it checks if the column belongs to a stitching. +func isColEligible(stitchings alliance.MultiSummary, col ifaces.Column) bool { + natural := column.RootParents(col)[0] + _, found := stitchings[col.Round()].BySubCol[natural.GetColID()] + return found +} + +// It makes the given colum public. +// If the colum is Precomputed it becomes the VerifierKey, otherwise it becomes Proof. +func (ctx stitchingContext) makeColumnPublic(col ifaces.Column, status column.Status) { + switch status { + case column.Precomputed: + // send it to the verifier directly as part of the verifying key + ctx.comp.Columns.SetStatus(col.GetColID(), column.VerifyingKey) + case column.Committed: + // send it to the verifier directly as part of the proof + ctx.comp.Columns.SetStatus(col.GetColID(), column.Proof) + default: + utils.Panic("Unknown status : %v", status.String()) + } +} diff --git a/prover/protocol/compiler/splitter/splitter/stitcher/stitcher_test.go b/prover/protocol/compiler/splitter/splitter/stitcher/stitcher_test.go new file mode 100644 index 000000000..e0534173e --- /dev/null +++ b/prover/protocol/compiler/splitter/splitter/stitcher/stitcher_test.go @@ -0,0 +1,296 @@ +package stitcher_test + +import ( + "testing" + + "github.com/consensys/linea-monorepo/prover/maths/common/smartvectors" + "github.com/consensys/linea-monorepo/prover/maths/field" + "github.com/consensys/linea-monorepo/prover/protocol/accessors" + "github.com/consensys/linea-monorepo/prover/protocol/coin" + "github.com/consensys/linea-monorepo/prover/protocol/column" + "github.com/consensys/linea-monorepo/prover/protocol/column/verifiercol" + "github.com/consensys/linea-monorepo/prover/protocol/compiler/dummy" + "github.com/consensys/linea-monorepo/prover/protocol/compiler/splitter/splitter/stitcher" + "github.com/consensys/linea-monorepo/prover/protocol/ifaces" + "github.com/consensys/linea-monorepo/prover/protocol/query" + "github.com/consensys/linea-monorepo/prover/protocol/wizard" + "github.com/consensys/linea-monorepo/prover/symbolic" + "github.com/stretchr/testify/assert" + "github.com/stretchr/testify/require" +) + +func TestLocalEval(t *testing.T) { + + var a, b, c, d ifaces.Column + var q1, q2, q3, q4, q5, q6, q7, q8, q9, q10, q11, q12 query.LocalOpening + + define := func(builder *wizard.Builder) { + // declare columns of different sizes + a = builder.RegisterCommit("A", 2) + b = builder.RegisterCommit("B", 4) + c = builder.RegisterCommit("C", 8) + d = builder.RegisterCommit("D", 16) + + // Local opening at zero + q1 = builder.LocalOpening("Q00", a) + q2 = builder.LocalOpening("Q01", b) + q3 = builder.LocalOpening("Q02", c) + q4 = builder.LocalOpening("Q03", d) + + // Local opening at but shifted by one + q5 = builder.LocalOpening("Q10", column.Shift(a, 1)) + q6 = builder.LocalOpening("Q11", column.Shift(b, 1)) + q7 = builder.LocalOpening("Q12", column.Shift(c, 1)) + q8 = builder.LocalOpening("Q13", column.Shift(d, 1)) + + // Local opening at but shifted by one + q9 = builder.LocalOpening("Q20", column.Shift(a, -1)) + q10 = builder.LocalOpening("Q21", column.Shift(b, -1)) + q11 = builder.LocalOpening("Q22", column.Shift(c, -1)) + q12 = builder.LocalOpening("Q23", column.Shift(d, -1)) + } + + comp := wizard.Compile(define, stitcher.Stitcher(4, 8)) + + //after stitcing-compilation we expect that the eligible columns and their relevant queries be ignored + assert.Equal(t, column.Proof.String(), comp.Columns.Status("A").String()) + assert.Equal(t, column.Ignored.String(), comp.Columns.Status("B").String()) + assert.Equal(t, column.Committed.String(), comp.Columns.Status("C").String()) + assert.Equal(t, column.Committed.String(), comp.Columns.Status("D").String()) + + assert.Equal(t, true, comp.QueriesParams.IsIgnored(q1.ID)) + assert.Equal(t, true, comp.QueriesParams.IsIgnored(q2.ID)) + assert.Equal(t, false, comp.QueriesParams.IsIgnored(q3.ID)) + assert.Equal(t, false, comp.QueriesParams.IsIgnored(q4.ID)) + assert.Equal(t, true, comp.QueriesParams.IsIgnored(q5.ID)) + assert.Equal(t, true, comp.QueriesParams.IsIgnored(q6.ID)) + assert.Equal(t, false, comp.QueriesParams.IsIgnored(q7.ID)) + assert.Equal(t, false, comp.QueriesParams.IsIgnored(q8.ID)) + assert.Equal(t, true, comp.QueriesParams.IsIgnored(q9.ID)) + assert.Equal(t, true, comp.QueriesParams.IsIgnored(q10.ID)) + assert.Equal(t, false, comp.QueriesParams.IsIgnored(q11.ID)) + assert.Equal(t, false, comp.QueriesParams.IsIgnored(q12.ID)) + + // manually compiles the comp + dummy.Compile(comp) + + proof := wizard.Prove(comp, func(assi *wizard.ProverRuntime) { + // Assigns all the columns + assi.AssignColumn(a.GetColID(), smartvectors.ForTest(0, 1)) + assi.AssignColumn(b.GetColID(), smartvectors.ForTest(2, 3, 4, 5)) + assi.AssignColumn(c.GetColID(), smartvectors.ForTest(6, 7, 8, 9, 10, 11, 12, 13)) + assi.AssignColumn(d.GetColID(), smartvectors.ForTest(15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30)) + + // And the alleged results + assi.AssignLocalPoint("Q00", field.NewElement(0)) + assi.AssignLocalPoint("Q01", field.NewElement(2)) + assi.AssignLocalPoint("Q02", field.NewElement(6)) + assi.AssignLocalPoint("Q03", field.NewElement(15)) + assi.AssignLocalPoint("Q10", field.NewElement(1)) + assi.AssignLocalPoint("Q11", field.NewElement(3)) + assi.AssignLocalPoint("Q12", field.NewElement(7)) + assi.AssignLocalPoint("Q13", field.NewElement(16)) + assi.AssignLocalPoint("Q20", field.NewElement(1)) + assi.AssignLocalPoint("Q21", field.NewElement(5)) + assi.AssignLocalPoint("Q22", field.NewElement(13)) + assi.AssignLocalPoint("Q23", field.NewElement(30)) + }) + + err := wizard.Verify(comp, proof) + require.NoError(t, err) + +} + +func TestGlobalConstraintFibonacci(t *testing.T) { + + var a, b, c ifaces.Column + var q1, q2, q3 query.GlobalConstraint + + define := func(builder *wizard.Builder) { + // declare columns of different sizes + a = builder.RegisterCommit("B", 4) + // a = verifiercol.NewConstantCol(field.One(), 4) + b = builder.RegisterCommit("C", 8) + c = builder.RegisterCommit("D", 16) + + fibo := func(col ifaces.Column) *symbolic.Expression { + col_ := ifaces.ColumnAsVariable(col) + colNext := ifaces.ColumnAsVariable(column.Shift(col, 1)) + colNextNext := ifaces.ColumnAsVariable(column.Shift(col, 2)) + return colNextNext.Sub(colNext).Sub(col_) + } + + q1 = builder.GlobalConstraint("Q0", fibo(a)) + q2 = builder.GlobalConstraint("Q1", fibo(b)) + q3 = builder.GlobalConstraint("Q2", fibo(c)) + } + + comp := wizard.Compile(define, stitcher.Stitcher(8, 16)) + + //after stitcing-compilation we expect that the eligible columns and their relevant queries be ignored + assert.Equal(t, true, comp.QueriesNoParams.IsIgnored(q1.ID), "q1 should be ignored") + assert.Equal(t, true, comp.QueriesNoParams.IsIgnored(q2.ID), "q2 should not be ignored") + assert.Equal(t, false, comp.QueriesNoParams.IsIgnored(q3.ID), "q3 should not be ignored") + + // manually compiles the comp + dummy.Compile(comp) + + proof := wizard.Prove(comp, func(assi *wizard.ProverRuntime) { + // Assigns all the columns + assi.AssignColumn(a.GetColID(), smartvectors.ForTest(1, 1, 2, 3)) + assi.AssignColumn(b.GetColID(), smartvectors.ForTest(1, 1, 2, 3, 5, 8, 13, 21)) + assi.AssignColumn(c.GetColID(), smartvectors.ForTest(1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987)) + }) + + err := wizard.Verify(comp, proof) + require.NoError(t, err) + +} + +func TestLocalConstraintFibonacci(t *testing.T) { + + var a, b, c ifaces.Column + var q1, q2, q3 query.LocalConstraint + + define := func(builder *wizard.Builder) { + // declare columns of different sizes + a = builder.RegisterCommit("B", 4) + b = builder.RegisterCommit("C", 8) + c = builder.RegisterCommit("D", 16) + + fibo := func(col ifaces.Column) *symbolic.Expression { + col_ := ifaces.ColumnAsVariable(col) + colNext := ifaces.ColumnAsVariable(column.Shift(col, 1)) + colNextNext := ifaces.ColumnAsVariable(column.Shift(col, 2)) + return colNextNext.Sub(colNext).Sub(col_) + } + + q1 = builder.LocalConstraint("Q0", fibo(a)) + q2 = builder.LocalConstraint("Q1", fibo(b)) + q3 = builder.LocalConstraint("Q2", fibo(c)) + } + + comp := wizard.Compile(define, stitcher.Stitcher(8, 16)) + + //after stitcing-compilation we expect that the eligible columns and their relevant queries be ignored + assert.Equal(t, true, comp.QueriesNoParams.IsIgnored(q1.ID), "q1 should be ignored") + assert.Equal(t, true, comp.QueriesNoParams.IsIgnored(q2.ID), "q2 should not be ignored") + assert.Equal(t, false, comp.QueriesNoParams.IsIgnored(q3.ID), "q3 should not be ignored") + + // manually compiles the comp + dummy.Compile(comp) + + proof := wizard.Prove(comp, func(assi *wizard.ProverRuntime) { + // Assigns all the columns + // Todo: Arbitrary changes of col values do not make the test failing + assi.AssignColumn(a.GetColID(), smartvectors.ForTest(1, 1, 2, 3)) + assi.AssignColumn(b.GetColID(), smartvectors.ForTest(1, 1, 2, 3, 5, 8, 13, 21)) + assi.AssignColumn(c.GetColID(), smartvectors.ForTest(1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987)) + }) + + err := wizard.Verify(comp, proof) + require.NoError(t, err) + +} + +func TestGlobalMixedRounds(t *testing.T) { + + var a0, a1, a2, b0, b1, b2 ifaces.Column + var q0, q1, q2 query.LocalConstraint + + define := func(builder *wizard.Builder) { + // declare columns of different sizes + a0 = builder.RegisterCommit("A0", 4) + a1 = builder.RegisterCommit("A1", 4) + a2 = builder.RegisterCommit("A2", 4) + _ = builder.RegisterRandomCoin("COIN", coin.Field) + b0 = builder.RegisterCommit("B0", 4) + b1 = builder.RegisterCommit("B1", 4) + b2 = builder.RegisterCommit("B2", 4) + + q0 = builder.LocalConstraint("Q0", ifaces.ColumnAsVariable(a0).Sub(ifaces.ColumnAsVariable(b0))) + q1 = builder.LocalConstraint("Q1", ifaces.ColumnAsVariable(a1).Sub(ifaces.ColumnAsVariable(b1))) + q2 = builder.LocalConstraint("Q2", ifaces.ColumnAsVariable(a2).Sub(ifaces.ColumnAsVariable(b2))) + } + + comp := wizard.Compile(define, stitcher.Stitcher(4, 8)) + + //after stitcing-compilation we expect that the eligible columns and their relevant queries be ignored + assert.Equal(t, true, comp.QueriesNoParams.IsIgnored(q0.ID), "q0 should be ignored") + assert.Equal(t, true, comp.QueriesNoParams.IsIgnored(q1.ID), "q1 should be ignored") + assert.Equal(t, true, comp.QueriesNoParams.IsIgnored(q2.ID), "q2 should be ignored") + + // manually compiles the comp + dummy.Compile(comp) + + proof := wizard.Prove(comp, func(assi *wizard.ProverRuntime) { + // Assigns all the columns + assi.AssignColumn(a0.GetColID(), smartvectors.ForTest(1, 1, 2, 3)) + assi.AssignColumn(a1.GetColID(), smartvectors.ForTest(1, 1, 2, 3)) + assi.AssignColumn(a2.GetColID(), smartvectors.ForTest(1, 1, 2, 3)) + _ = assi.GetRandomCoinField("COIN") // triggers going to the next round + assi.AssignColumn(b0.GetColID(), smartvectors.ForTest(1, 1, 2, 3)) + assi.AssignColumn(b1.GetColID(), smartvectors.ForTest(1, 1, 2, 3)) + assi.AssignColumn(b2.GetColID(), smartvectors.ForTest(1, 1, 2, 3)) + }) + + err := wizard.Verify(comp, proof) + require.NoError(t, err) +} + +func TestWithVerifCol(t *testing.T) { + var a, b, c, verifcol1, verifcol2 ifaces.Column + var q1, q2 query.GlobalConstraint + var q3 query.LocalConstraint + + define := func(builder *wizard.Builder) { + // declare columns of different sizes + a = builder.RegisterCommit("B", 4) + b = builder.RegisterCommit("C", 4) + // a new round + _ = builder.RegisterRandomCoin("COIN", coin.Field) + c = builder.RegisterCommit("D", 4) + // verifiercols + verifcol1 = verifiercol.NewConstantCol(field.NewElement(3), 4) + accessors := genAccessors([]int{1, 7, 5, 3}) + verifcol2 = verifiercol.NewFromAccessors(accessors, field.Zero(), 4) + + expr := symbolic.Sub(symbolic.Mul(a, verifcol1), b) + q1 = builder.GlobalConstraint("Q0", expr) + + expr = symbolic.Sub(symbolic.Add(a, verifcol2), c) + q2 = builder.GlobalConstraint("Q1", expr) + + q3 = builder.LocalConstraint("Q2", expr) + } + + comp := wizard.Compile(define, stitcher.Stitcher(4, 16)) + + //after stitcing-compilation we expect that the eligible columns and their relevant queries be ignored + assert.Equal(t, true, comp.QueriesNoParams.IsIgnored(q1.ID), "q1 should be ignored") + assert.Equal(t, true, comp.QueriesNoParams.IsIgnored(q2.ID), "q2 should be ignored") + assert.Equal(t, true, comp.QueriesNoParams.IsIgnored(q3.ID), "q2 should be ignored") + + // manually compiles the comp + dummy.Compile(comp) + + proof := wizard.Prove(comp, func(assi *wizard.ProverRuntime) { + // Assigns all the columns + assi.AssignColumn(a.GetColID(), smartvectors.ForTest(1, 1, 2, 3)) + assi.AssignColumn(b.GetColID(), smartvectors.ForTest(3, 3, 6, 9)) + _ = assi.GetRandomCoinField("COIN") // triggers going to the next round + assi.AssignColumn(c.GetColID(), smartvectors.ForTest(2, 8, 7, 6)) + }) + + err := wizard.Verify(comp, proof) + require.NoError(t, err) + +} + +func genAccessors(a []int) (res []ifaces.Accessor) { + for i := range a { + t := accessors.NewConstant(field.NewElement(uint64(a[i]))) + res = append(res, t) + } + return res +} diff --git a/prover/protocol/query/local.go b/prover/protocol/query/local.go index 14e5c9eec..09d3fe148 100644 --- a/prover/protocol/query/local.go +++ b/prover/protocol/query/local.go @@ -21,7 +21,8 @@ import ( // and the constraint applied after type LocalConstraint struct { *symbolic.Expression - ID ifaces.QueryID + ID ifaces.QueryID + DomainSize int } // Construct a new local constraint @@ -62,7 +63,7 @@ func NewLocalConstraint(id ifaces.QueryID, expr *symbolic.Expression) LocalConst utils.Panic("All commitment given had a length of zero") } - res := LocalConstraint{Expression: expr, ID: id} + res := LocalConstraint{Expression: expr, ID: id, DomainSize: domainSize} return res }