Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

initial framework for lookup #428

Draft
wants to merge 12 commits into
base: prover/limitless-top-level
Choose a base branch
from
73 changes: 73 additions & 0 deletions prover/protocol/column/column.go
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,11 @@ package column
import (
"reflect"

"github.com/consensys/linea-monorepo/prover/maths/common/smartvectors"
"github.com/consensys/linea-monorepo/prover/protocol/coin"
"github.com/consensys/linea-monorepo/prover/protocol/ifaces"
"github.com/consensys/linea-monorepo/prover/protocol/variables"
"github.com/consensys/linea-monorepo/prover/symbolic"
"github.com/consensys/linea-monorepo/prover/utils"
)

Expand Down Expand Up @@ -91,3 +95,72 @@ func NbLeaves(h ifaces.Column) int {
}
panic("unreachable")
}

func EvalExprColumn(run ifaces.Runtime, board symbolic.ExpressionBoard) smartvectors.SmartVector {

var (
metadata = board.ListVariableMetadata()
inputs = make([]smartvectors.SmartVector, len(metadata))
length = ExprIsOnSameLengthHandles(&board)
)

// Attempt to recover the size of the
for i := range inputs {
switch m := metadata[i].(type) {
case ifaces.Column:
inputs[i] = m.GetColAssignment(run)
case coin.Info:
v := run.GetRandomCoinField(m.Name)
inputs[i] = smartvectors.NewConstant(v, length)
case ifaces.Accessor:
v := m.GetVal(run)
inputs[i] = smartvectors.NewConstant(v, length)
case variables.PeriodicSample:
v := m.EvalCoset(length, 0, 1, false)
inputs[i] = v
case variables.X:
v := m.EvalCoset(length, 0, 1, false)
inputs[i] = v
}
}

return board.Evaluate(inputs)
}

// ExprIsOnSameLengthHandles checks that all the variables of the expression
// that are [ifaces.Column] have the same size (and panics if it does not), then
// returns the match.
func ExprIsOnSameLengthHandles(board *symbolic.ExpressionBoard) int {

var (
metadatas = board.ListVariableMetadata()
length = 0
)

for _, m := range metadatas {
switch metadata := m.(type) {
case ifaces.Column:
// Initialize the length with the first commitment
if length == 0 {
length = metadata.Size()
}

// Sanity-check the vector should all have the same length
if length != metadata.Size() {
utils.Panic("Inconsistent length for %v (has size %v, but expected %v)", metadata.GetColID(), metadata.Size(), length)
}
// The expression can involve random coins
case coin.Info, variables.X, variables.PeriodicSample, ifaces.Accessor:
// Do nothing
default:
utils.Panic("unknown type %T", metadata)
}
}

// No commitment were found in the metadata, thus this call is broken
if length == 0 {
utils.Panic("declared a handle from an expression which does not contains any handle")
}

return length
}
4 changes: 2 additions & 2 deletions prover/protocol/compiler/globalcs/merging.go
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,11 @@ import (
"github.com/consensys/linea-monorepo/prover/maths/fft"
"github.com/consensys/linea-monorepo/prover/maths/field"
"github.com/consensys/linea-monorepo/prover/protocol/coin"
"github.com/consensys/linea-monorepo/prover/protocol/column"
"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/protocol/wizardutils"
"github.com/consensys/linea-monorepo/prover/symbolic"
"github.com/consensys/linea-monorepo/prover/utils"
)
Expand Down Expand Up @@ -178,7 +178,7 @@ func getBoundCancelledExpression(cs query.GlobalConstraint) *symbolic.Expression
func getExprRatio(expr *symbolic.Expression) int {
var (
board = expr.Board()
domainSize = wizardutils.ExprIsOnSameLengthHandles(&board)
domainSize = column.ExprIsOnSameLengthHandles(&board)
exprDegree = board.Degree(GetDegree(domainSize))
quotientSize = exprDegree - domainSize + 1
ratio = utils.DivCeil(quotientSize, domainSize)
Expand Down
4 changes: 2 additions & 2 deletions prover/protocol/compiler/innerproduct/prover.go
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ import (

"github.com/consensys/linea-monorepo/prover/maths/common/smartvectors"
"github.com/consensys/linea-monorepo/prover/maths/field"
"github.com/consensys/linea-monorepo/prover/protocol/column"
"github.com/consensys/linea-monorepo/prover/protocol/wizard"
"github.com/consensys/linea-monorepo/prover/protocol/wizardutils"
)

// proverTask implements the [wizard.ProverAction] interface and as such
Expand Down Expand Up @@ -39,7 +39,7 @@ func (ctx *contextForSize) run(run *wizard.ProverRuntime) {

var (
size = ctx.Summation.Size()
collapsed = wizardutils.EvalExprColumn(run, ctx.CollapsedBoard).IntoRegVecSaveAlloc()
collapsed = column.EvalExprColumn(run, ctx.CollapsedBoard).IntoRegVecSaveAlloc()
summation = make([]field.Element, size)
)

Expand Down
78 changes: 39 additions & 39 deletions prover/protocol/compiler/lookup/compiler.go
Original file line number Diff line number Diff line change
Expand Up @@ -27,39 +27,39 @@ type table = []ifaces.Column
func CompileLogDerivative(comp *wizard.CompiledIOP) {

var (
mainLookupCtx = captureLookupTables(comp)
mainLookupCtx = CaptureLookupTables(comp)
lastRound = comp.NumRounds() - 1
proverActions = make([]proverTaskAtRound, comp.NumRounds()+1)
// zCatalog stores a mapping (round, size) into ZCtx and helps finding
// which Z context should be used to handle a part of a given permutation
// query.
zCatalog = map[[2]int]*zCtx{}
zCatalog = map[[2]int]*ZCtx{}
zEntries = [][2]int{}
// verifier actions
va = finalEvaluationCheck{}
)

// Skip the compilation phase if no lookup constraint is being used. Otherwise
// it will register a verifier action that is not required and will be bugged.
if len(mainLookupCtx.lookupTables) == 0 {
if len(mainLookupCtx.LookupTables) == 0 {
return
}

// Step 1. construct the "per table" contexts and pack the Sigma's into
// zCatalog.
for _, lookupTable := range mainLookupCtx.lookupTables {
for _, lookupTable := range mainLookupCtx.LookupTables {

var (
// get checkedTables, rounds, Filters by lookupTableName
lookupTableName = nameTable(lookupTable)
checkTable = mainLookupCtx.checkedTables[lookupTableName]
round = mainLookupCtx.rounds[lookupTableName]
includedFilters = mainLookupCtx.includedFilters[lookupTableName]
tableCtx = compileLookupTable(comp, round, lookupTable, checkTable, includedFilters)
lookupTableName = NameTable(lookupTable)
checkTable = mainLookupCtx.CheckedTables[lookupTableName]
round = mainLookupCtx.Rounds[lookupTableName]
includedFilters = mainLookupCtx.IncludedFilters[lookupTableName]
tableCtx = CompileLookupTable(comp, round, lookupTable, checkTable, includedFilters)
)

// push to zCatalog
tableCtx.pushToZCatalog(zCatalog)
tableCtx.PushToZCatalog(zCatalog)

proverActions[round].pushMAssignment(
mAssignmentTask{
Expand Down Expand Up @@ -119,7 +119,7 @@ func CompileLogDerivative(comp *wizard.CompiledIOP) {
comp.RegisterVerifierAction(lastRound, &va)
}

// captureLookupTables inspects comp and look for Inclusion queries that are not
// CaptureLookupTables inspects comp and look for Inclusion queries that are not
// marked as ignored yet. All the queries matched queries are grouped by look-up
// table (e.g. all the queries that use the same lookup table). All the matched
// queries are marked as ignored. The function returns the thereby-initialized
Expand All @@ -131,13 +131,13 @@ func CompileLogDerivative(comp *wizard.CompiledIOP) {
// The function also implictly reduces the conditionals over the Including table
// be appending a "one" column on the included side and the filter on the
// including side.
func captureLookupTables(comp *wizard.CompiledIOP) mainLookupCtx {
func CaptureLookupTables(comp *wizard.CompiledIOP) mainLookupCtx {

ctx := mainLookupCtx{
lookupTables: [][]table{},
checkedTables: map[string][]table{},
includedFilters: map[string][]ifaces.Column{},
rounds: map[string]int{},
LookupTables: [][]table{},
CheckedTables: map[string][]table{},
IncludedFilters: map[string][]ifaces.Column{},
Rounds: map[string]int{},
}

// Collect all the lookup queries into "lookups"
Expand All @@ -157,8 +157,8 @@ func captureLookupTables(comp *wizard.CompiledIOP) mainLookupCtx {
var (
// checkedTable corresponds to the "included" table and lookupTable
// corresponds to the including table.
checkedTable, lookupTable = getTableCanonicalOrder(lookup)
tableName = nameTable(lookupTable)
checkedTable, lookupTable = GetTableCanonicalOrder(lookup)
tableName = NameTable(lookupTable)
// includedFilters stores the query.IncludedFilter parameter. If the
// query has no includedFilters on the Included side. Then this is
// left as nil.
Expand All @@ -176,7 +176,7 @@ func captureLookupTables(comp *wizard.CompiledIOP) mainLookupCtx {
lookupTable[frag] = append([]ifaces.Column{lookup.IncludingFilter[frag]}, lookupTable[frag]...)
}

tableName = nameTable(lookupTable)
tableName = NameTable(lookupTable)
}

if lookup.IsFilteredOnIncluded() {
Expand All @@ -185,16 +185,16 @@ func captureLookupTables(comp *wizard.CompiledIOP) mainLookupCtx {

// In case this is the first iteration where we encounter the lookupTable
// we need to add entries in the registering maps.
if _, ok := ctx.checkedTables[tableName]; !ok {
ctx.includedFilters[tableName] = []ifaces.Column{}
ctx.checkedTables[tableName] = []table{}
ctx.lookupTables = append(ctx.lookupTables, lookupTable)
ctx.rounds[tableName] = 0
if _, ok := ctx.CheckedTables[tableName]; !ok {
ctx.IncludedFilters[tableName] = []ifaces.Column{}
ctx.CheckedTables[tableName] = []table{}
ctx.LookupTables = append(ctx.LookupTables, lookupTable)
ctx.Rounds[tableName] = 0
}

ctx.includedFilters[tableName] = append(ctx.includedFilters[tableName], includedFilter)
ctx.checkedTables[tableName] = append(ctx.checkedTables[tableName], checkedTable)
ctx.rounds[tableName] = max(ctx.rounds[tableName], comp.QueriesNoParams.Round(lookup.ID))
ctx.IncludedFilters[tableName] = append(ctx.IncludedFilters[tableName], includedFilter)
ctx.CheckedTables[tableName] = append(ctx.CheckedTables[tableName], checkedTable)
ctx.Rounds[tableName] = max(ctx.Rounds[tableName], comp.QueriesNoParams.Round(lookup.ID))

}

Expand All @@ -213,16 +213,16 @@ func captureLookupTables(comp *wizard.CompiledIOP) mainLookupCtx {
// - (5) The verier makes a `Global` query : $\left((\Sigma_T)[i] - (\Sigma_T)[i-1]\right)(T_i + \gamma) = M_i$

// here we are looking up set of columns S in a single column T
func compileLookupTable(
func CompileLookupTable(
comp *wizard.CompiledIOP,
round int,
lookupTable []table,
checkedTables []table,
includedFilters []ifaces.Column,
) (ctx singleTableCtx) {
) (ctx SingleTableCtx) {

ctx = singleTableCtx{
TableName: nameTable(lookupTable),
ctx = SingleTableCtx{
TableName: NameTable(lookupTable),
S: make([]*symbolic.Expression, len(checkedTables)),
SFilters: includedFilters,
T: make([]*symbolic.Expression, len(lookupTable)),
Expand All @@ -240,7 +240,7 @@ func compileLookupTable(
ctx.T[frag] = symbolic.NewVariable(lookupTable[frag][0])
ctx.M[frag] = comp.InsertCommit(
round,
deriveTableNameWithIndex[ifaces.ColID](logDerivativePrefix, lookupTable, frag, "M"),
DeriveTableNameWithIndex[ifaces.ColID](LogDerivativePrefix, lookupTable, frag, "M"),
lookupTable[frag][0].Size(),
)

Expand All @@ -257,15 +257,15 @@ func compileLookupTable(
// columns of T and S when they are (both) multi-columns.
alpha := comp.InsertCoin(
round+1,
deriveTableName[coin.Name](logDerivativePrefix, lookupTable, "ALPHA"),
DeriveTableName[coin.Name](LogDerivativePrefix, lookupTable, "ALPHA"),
coin.Field,
)

for frag := range ctx.T {
ctx.T[frag] = wizardutils.RandLinCombColSymbolic(alpha, lookupTable[frag])
ctx.M[frag] = comp.InsertCommit(
round,
deriveTableNameWithIndex[ifaces.ColID](logDerivativePrefix, lookupTable, frag, "M"),
DeriveTableNameWithIndex[ifaces.ColID](LogDerivativePrefix, lookupTable, frag, "M"),
lookupTable[frag][0].Size(),
)
}
Expand All @@ -277,16 +277,16 @@ func compileLookupTable(

ctx.Gamma = comp.InsertCoin(
round+1,
deriveTableName[coin.Name](logDerivativePrefix, lookupTable, "GAMMA"),
DeriveTableName[coin.Name](LogDerivativePrefix, lookupTable, "GAMMA"),
coin.Field,
)

return ctx
}

// pushToZCatalog constructs the numerators and denominators for S and T of the
// PushToZCatalog constructs the numerators and denominators for S and T of the
// stc into zCatalog for their corresponding rounds and size.
func (stc *singleTableCtx) pushToZCatalog(zCatalog map[[2]int]*zCtx) {
func (stc *SingleTableCtx) PushToZCatalog(zCatalog map[[2]int]*ZCtx) {

var (
round = stc.Gamma.Round
Expand All @@ -299,7 +299,7 @@ func (stc *singleTableCtx) pushToZCatalog(zCatalog map[[2]int]*zCtx) {

key := [2]int{round, size}
if zCatalog[key] == nil {
zCatalog[key] = &zCtx{
zCatalog[key] = &ZCtx{
Size: size,
Round: round,
Name: stc.TableName,
Expand All @@ -324,7 +324,7 @@ func (stc *singleTableCtx) pushToZCatalog(zCatalog map[[2]int]*zCtx) {

key := [2]int{round, size}
if zCatalog[key] == nil {
zCatalog[key] = &zCtx{
zCatalog[key] = &ZCtx{
Size: size,
Round: round,
Name: stc.TableName,
Expand Down
26 changes: 13 additions & 13 deletions prover/protocol/compiler/lookup/context.go
Original file line number Diff line number Diff line change
Expand Up @@ -10,41 +10,41 @@ import (
// altogether.
type mainLookupCtx struct {

// lookupTables stores all the lookup table the compiler encounters. They are
// LookupTables stores all the lookup table the compiler encounters. They are
// sorted in canonical order. This used to derive a determistic ordering
// of the lookup lookupTables. (We want to ensure the compiler yields always
// of the lookup LookupTables. (We want to ensure the compiler yields always
// exactly the same result for replicability).
//
// To illustrates its structure, the following sub-statement
//
// table[numTable][frag]
//
// refers to to the fragment #frag of the the table #numTable.
lookupTables [][]table
LookupTables [][]table

// checkedTables stores all the checked column by lookup table. The key is
// CheckedTables stores all the checked column by lookup table. The key is
// obtained as nameTable(lookupTable) where lookup is sorted in
// canonical order.
checkedTables map[string][]table
CheckedTables map[string][]table

// includedFilters stores all the filters for the checked columns and `nil`
// IncludedFilters stores all the filters for the checked columns and `nil`
// if no filter is applied. As for [checkedTables] they are stored by
// lookup table name and in the same order for each key.
includedFilters map[string][]ifaces.Column
IncludedFilters map[string][]ifaces.Column

// rounds stores the interaction round assigned to each lookupTable. The
// round is obtained by taking the max of the declaration rounds of the
// Rounds stores the interaction round assigned to each lookupTable. The
// round is obtained by taking the max of the declaration Rounds of the
// Inclusion queries using the corresponding lookup table.
rounds map[string]int
Rounds map[string]int
}

// singleTableCtx stores the compilation context for a single lookup query
// SingleTableCtx stores the compilation context for a single lookup query
// when it is compiled using the log-derivative lookup technique.
//
// A singleTableCtx relates to a lookup table rather than a lookup query. This
// A SingleTableCtx relates to a lookup table rather than a lookup query. This
// means that multiple lookup queries that are related to the same table will be
// grouped into the same context. This allows optimizing the
type singleTableCtx struct {
type SingleTableCtx struct {

// TableName reflects the name of the lookup table being compiled.
TableName string
Expand Down
Loading
Loading