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 <dreamerty@postech.ac.kr>
Co-authored-by: Leo Jeong <dreamerty@postech.ac.kr>

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())
 		})
 	}
 }

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
+}

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())
 }

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
+}