feat: tweak internal representation of lookups

pkg/asm/compiler/mir.go

@@ -19,6 +19,7 @@ import (
 	"github.com/consensys/go-corset/pkg/ir"
 	"github.com/consensys/go-corset/pkg/ir/mir"
 	"github.com/consensys/go-corset/pkg/schema"
+	"github.com/consensys/go-corset/pkg/schema/constraint/lookup"
 	"github.com/consensys/go-corset/pkg/util"
 	"github.com/consensys/go-corset/pkg/util/collection/array"
 )
@@ -75,9 +76,9 @@ func (p MirModule) NewLookup(name string, from []MirExpr, targetMid uint, to []M
 	// Preprend (unused) selectors.  Eventually, we will most likely want to support selectors.
 	sources = array.Prepend(unused, sources)
 	targets = array.Prepend(unused, targets)
-	//
-	target := []ir.Enclosed[[]mir.Term]{ir.Enclose(p.Module.Id(), targets)}
-	source := []ir.Enclosed[[]mir.Term]{ir.Enclose(targetMid, sources)}
+	// FIXME: exploit conditional lookups
+	target := []lookup.Vector[mir.Term]{lookup.UnfilteredVector(p.Module.Id(), targets...)}
+	source := []lookup.Vector[mir.Term]{lookup.UnfilteredVector(targetMid, sources...)}
 	p.Module.AddConstraint(mir.NewLookupConstraint(name, target, source))
 }
 

pkg/binfile/binfile.go

@@ -200,7 +200,7 @@ func (p *Header) IsCompatible() bool {
 // matter what version, we should always have the ZKBINARY identifier first,
 // followed by a GOB encoding of the header.  What follows after that, however,
 // is determined by the major version.
-const BINFILE_MAJOR_VERSION uint16 = 5
+const BINFILE_MAJOR_VERSION uint16 = 6
 
 // BINFILE_MINOR_VERSION gives the minor version of the binary file format.  The
 // expected interpretation is that older versions are compatible with newer

pkg/cmd/check.go

@@ -26,6 +26,9 @@ import (
 	"github.com/consensys/go-corset/pkg/ir"
 	sc "github.com/consensys/go-corset/pkg/schema"
 	"github.com/consensys/go-corset/pkg/schema/constraint"
+	"github.com/consensys/go-corset/pkg/schema/constraint/lookup"
+	"github.com/consensys/go-corset/pkg/schema/constraint/ranged"
+	"github.com/consensys/go-corset/pkg/schema/constraint/vanishing"
 	"github.com/consensys/go-corset/pkg/trace"
 	tr "github.com/consensys/go-corset/pkg/trace"
 	"github.com/consensys/go-corset/pkg/util"
@@ -221,15 +224,15 @@ func reportFailures(ir string, failures []sc.Failure, trace tr.Trace, cfg checkC
 
 // Print a human-readable report detailing the given failure
 func reportFailure(failure sc.Failure, trace tr.Trace, cfg checkConfig) {
-	if f, ok := failure.(*constraint.VanishingFailure); ok {
+	if f, ok := failure.(*vanishing.Failure); ok {
 		cells := f.RequiredCells(trace)
 		fmt.Printf("failing constraint %s:\n", f.Handle)
 		reportRelevantCells(cells, trace, cfg)
-	} else if f, ok := failure.(*constraint.RangeFailure); ok {
+	} else if f, ok := failure.(*ranged.Failure); ok {
 		cells := f.RequiredCells(trace)
 		fmt.Printf("failing range constraint %s:\n", f.Handle)
 		reportRelevantCells(cells, trace, cfg)
-	} else if f, ok := failure.(*constraint.LookupFailure); ok {
+	} else if f, ok := failure.(*lookup.Failure); ok {
 		cells := f.RequiredCells(trace)
 		fmt.Printf("failing lookup constraint %s:\n", f.Handle)
 		reportRelevantCells(cells, trace, cfg)

pkg/corset/compiler/translator.go

@@ -25,8 +25,8 @@ import (
 	"github.com/consensys/go-corset/pkg/ir/assignment"
 	"github.com/consensys/go-corset/pkg/ir/mir"
 	"github.com/consensys/go-corset/pkg/schema"
+	"github.com/consensys/go-corset/pkg/schema/constraint/lookup"
 	"github.com/consensys/go-corset/pkg/util"
-	"github.com/consensys/go-corset/pkg/util/collection/array"
 	"github.com/consensys/go-corset/pkg/util/source"
 )
 
@@ -357,8 +357,8 @@ func (t *translator) translateDefLookup(decl *ast.DefLookup) []SyntaxError {
 	var (
 		errors  []SyntaxError
 		context ast.Context
-		sources []ir.Enclosed[[]mir.Term]
-		targets []ir.Enclosed[[]mir.Term]
+		sources []lookup.Vector[mir.Term]
+		targets []lookup.Vector[mir.Term]
 	)
 	// Translate sources
 	for i, ith := range decl.Targets {
@@ -387,7 +387,7 @@ func (t *translator) translateDefLookup(decl *ast.DefLookup) []SyntaxError {
 }
 
 func (t *translator) translateDefLookupSources(selector ast.Expr,
-	sources []ast.Expr) (ir.Enclosed[[]mir.Term], ast.Context, []SyntaxError) {
+	sources []ast.Expr) (lookup.Vector[mir.Term], ast.Context, []SyntaxError) {
 	// Determine context of ith set of targets
 	context, j := ast.ContextOfExpressions(sources...)
 	// Include selector (when present)
@@ -397,7 +397,7 @@ func (t *translator) translateDefLookupSources(selector ast.Expr,
 	// Translate target expressions whilst again checking for a conflicting
 	// context.
 	if context.IsConflicted() {
-		return ir.Enclosed[[]mir.Term]{}, context, t.srcmap.SyntaxErrors(sources[j], "conflicting context")
+		return lookup.Vector[mir.Term]{}, context, t.srcmap.SyntaxErrors(sources[j], "conflicting context")
 	}
 	// Determine enclosing module
 	module := t.moduleOf(context)
@@ -407,14 +407,11 @@ func (t *translator) translateDefLookupSources(selector ast.Expr,
 	if selector != nil {
 		s, errs := t.translateExpression(selector, module, 0)
 		errors = append(errors, errs...)
-		terms = array.Prepend(s, terms)
-	} else {
-		// Selector is unused
-		s := ir.NewRegisterAccess[mir.Term](schema.NewUnusedRegisterId(), 0)
-		terms = array.Prepend(s, terms)
+
+		return lookup.FilteredVector(module.Id(), s, terms...), context, errors
 	}
-	// Return enclosed terms
-	return ir.Enclose(module.Id(), terms), context, errors
+	//
+	return lookup.UnfilteredVector(module.Id(), terms...), context, errors
 }
 
 // Translate a "definrange" declaration.

pkg/ir/air/constraint.go

@@ -17,6 +17,11 @@ import (
 	"github.com/consensys/go-corset/pkg/ir"
 	"github.com/consensys/go-corset/pkg/schema"
 	"github.com/consensys/go-corset/pkg/schema/constraint"
+	"github.com/consensys/go-corset/pkg/schema/constraint/interleaving"
+	"github.com/consensys/go-corset/pkg/schema/constraint/lookup"
+	"github.com/consensys/go-corset/pkg/schema/constraint/permutation"
+	"github.com/consensys/go-corset/pkg/schema/constraint/ranged"
+	"github.com/consensys/go-corset/pkg/schema/constraint/vanishing"
 	"github.com/consensys/go-corset/pkg/trace"
 	"github.com/consensys/go-corset/pkg/util"
 	"github.com/consensys/go-corset/pkg/util/collection/bit"
@@ -34,11 +39,11 @@ type ConstraintBound interface {
 	schema.Constraint
 
 	constraint.Assertion[ir.Testable] |
-		constraint.InterleavingConstraint[*ColumnAccess] |
-		constraint.LookupConstraint[*ColumnAccess] |
-		constraint.PermutationConstraint |
-		constraint.RangeConstraint[*ColumnAccess] |
-		constraint.VanishingConstraint[LogicalTerm]
+		interleaving.Constraint[*ColumnAccess] |
+		lookup.Constraint[*ColumnAccess] |
+		permutation.Constraint |
+		ranged.Constraint[*ColumnAccess] |
+		vanishing.Constraint[LogicalTerm]
 }
 
 // Air attempts to encapsulate the notion of a valid constraint at the AIR
@@ -64,32 +69,32 @@ func NewAssertion(handle string, ctx schema.ModuleId, term ir.Testable) Assertio
 // NewInterleavingConstraint creates a new interleaving constraint with a given handle.
 func NewInterleavingConstraint(handle string, targetContext schema.ModuleId,
 	sourceContext schema.ModuleId, target ColumnAccess, sources []*ColumnAccess) Constraint {
-	return newAir(constraint.NewInterleavingConstraint(handle, targetContext, sourceContext, &target, sources))
+	return newAir(interleaving.NewConstraint(handle, targetContext, sourceContext, &target, sources))
 }
 
 // NewLookupConstraint constructs a new AIR lookup constraint
-func NewLookupConstraint(handle string, targets []ir.Enclosed[[]*ColumnAccess],
-	sources []ir.Enclosed[[]*ColumnAccess]) LookupConstraint {
+func NewLookupConstraint(handle string, targets []lookup.Vector[*ColumnAccess],
+	sources []lookup.Vector[*ColumnAccess]) LookupConstraint {
 	//
-	return newAir(constraint.NewLookupConstraint(handle, targets, sources))
+	return newAir(lookup.NewConstraint(handle, targets, sources))
 }
 
 // NewPermutationConstraint creates a new permutation
 func NewPermutationConstraint(handle string, context schema.ModuleId, targets []schema.RegisterId,
 	sources []schema.RegisterId) Constraint {
-	return newAir(constraint.NewPermutationConstraint(handle, context, targets, sources))
+	return newAir(permutation.NewPermutationConstraint(handle, context, targets, sources))
 }
 
 // NewRangeConstraint constructs a new AIR range constraint
 func NewRangeConstraint(handle string, ctx schema.ModuleId, expr ColumnAccess, bitwidth uint) RangeConstraint {
-	return newAir(constraint.NewRangeConstraint(handle, ctx, &expr, bitwidth))
+	return newAir(ranged.NewRangeConstraint(handle, ctx, &expr, bitwidth))
 }
 
 // NewVanishingConstraint constructs a new AIR vanishing constraint
 func NewVanishingConstraint(handle string, ctx schema.ModuleId, domain util.Option[int],
 	term Term) VanishingConstraint {
 	//
-	return newAir(constraint.NewVanishingConstraint(handle, ctx, domain, LogicalTerm{term}))
+	return newAir(vanishing.NewConstraint(handle, ctx, domain, LogicalTerm{term}))
 }
 
 // Air marks the constraint as being valid for the AIR representation.

pkg/ir/air/gadgets/bitwidth.go

@@ -22,6 +22,7 @@ import (
 	"github.com/consensys/go-corset/pkg/ir/assignment"
 	"github.com/consensys/go-corset/pkg/schema"
 	sc "github.com/consensys/go-corset/pkg/schema"
+	"github.com/consensys/go-corset/pkg/schema/constraint/lookup"
 	"github.com/consensys/go-corset/pkg/trace"
 	"github.com/consensys/go-corset/pkg/util"
 	"github.com/consensys/go-corset/pkg/util/field"
@@ -164,20 +165,16 @@ func (p *BitwidthGadget) applyRecursiveBitwidthGadget(ref sc.RegisterRef, bitwid
 	}
 	// Add lookup constraint for register into proof
 	sourceAccesses := []*air.ColumnAccess{
-		// Source Selector (unused)
-		ir.RawRegisterAccess[air.Term](sc.NewUnusedRegisterId(), 0),
 		// Source Value
 		ir.RawRegisterAccess[air.Term](ref.Register(), 0)}
 	// NOTE: 0th column always assumed to hold full value, with others
 	// representing limbs, etc.
 	targetAccesses := []*air.ColumnAccess{
-		// Target Selector (unused)
-		ir.RawRegisterAccess[air.Term](sc.NewUnusedRegisterId(), 0),
 		// Target Value
 		ir.RawRegisterAccess[air.Term](sc.NewRegisterId(0), 0)}
 	//
-	targets := []ir.Enclosed[[]*air.ColumnAccess]{ir.Enclose(mid, targetAccesses)}
-	sources := []ir.Enclosed[[]*air.ColumnAccess]{ir.Enclose(module.Id(), sourceAccesses)}
+	targets := []lookup.Vector[*air.ColumnAccess]{lookup.UnfilteredVector(mid, targetAccesses...)}
+	sources := []lookup.Vector[*air.ColumnAccess]{lookup.UnfilteredVector(module.Id(), sourceAccesses...)}
 	//
 	module.AddConstraint(air.NewLookupConstraint(lookupHandle, targets, sources))
 	// Add column to assignment so its proof is included

pkg/ir/air/schema.go

@@ -17,6 +17,11 @@ import (
 	"github.com/consensys/go-corset/pkg/ir"
 	"github.com/consensys/go-corset/pkg/schema"
 	"github.com/consensys/go-corset/pkg/schema/constraint"
+	"github.com/consensys/go-corset/pkg/schema/constraint/interleaving"
+	"github.com/consensys/go-corset/pkg/schema/constraint/lookup"
+	"github.com/consensys/go-corset/pkg/schema/constraint/permutation"
+	"github.com/consensys/go-corset/pkg/schema/constraint/ranged"
+	"github.com/consensys/go-corset/pkg/schema/constraint/vanishing"
 	"github.com/consensys/go-corset/pkg/trace"
 	"github.com/consensys/go-corset/pkg/util"
 	"github.com/consensys/go-corset/pkg/util/collection/set"
@@ -66,19 +71,19 @@ type (
 	Assertion = Air[constraint.Assertion[ir.Testable]]
 	// InterleavingConstraint captures the essence of an interleaving constraint
 	// at the MIR level.
-	InterleavingConstraint = constraint.InterleavingConstraint[*ColumnAccess]
+	InterleavingConstraint = Air[interleaving.Constraint[*ColumnAccess]]
 	// LookupConstraint captures the essence of a lookup constraint at the AIR
 	// level.  At the AIR level, lookup constraints are only permitted between
 	// columns (i.e. not arbitrary expressions).
-	LookupConstraint = Air[constraint.LookupConstraint[*ColumnAccess]]
+	LookupConstraint = Air[lookup.Constraint[*ColumnAccess]]
 	// PermutationConstraint captures the essence of a permutation constraint at the
 	// AIR level. Specifically, it represents a constraint that one (or more)
 	// columns are a permutation of another.
-	PermutationConstraint = Air[constraint.PermutationConstraint]
+	PermutationConstraint = Air[permutation.Constraint]
 	// RangeConstraint captures the essence of a range constraints at the AIR level.
-	RangeConstraint = Air[constraint.RangeConstraint[*ColumnAccess]]
+	RangeConstraint = Air[ranged.Constraint[*ColumnAccess]]
 	// VanishingConstraint captures the essence of a vanishing constraint at the AIR level.
-	VanishingConstraint = Air[constraint.VanishingConstraint[LogicalTerm]]
+	VanishingConstraint = Air[vanishing.Constraint[LogicalTerm]]
 )
 
 // Following types capture permitted expression forms at the AIR level.

pkg/ir/mir/agnosticity.go

@@ -15,7 +15,7 @@ package mir
 import (
 	"github.com/consensys/go-corset/pkg/ir"
 	"github.com/consensys/go-corset/pkg/schema"
-	"github.com/consensys/go-corset/pkg/schema/constraint"
+	"github.com/consensys/go-corset/pkg/schema/constraint/vanishing"
 )
 
 // Subdivide implementation for the FieldAgnostic interface.
@@ -55,7 +55,7 @@ func subdivideVanishing(p VanishingConstraint, mapping schema.RegisterLimbsMap)
 	// FIXME: this is an insufficient solution because it does not address the
 	// potential issues around bandwidth.  Specifically, where additional carry
 	// lines are needed, etc.
-	return constraint.NewVanishingConstraint(p.Handle, p.Context, p.Domain, c)
+	return vanishing.NewConstraint(p.Handle, p.Context, p.Domain, c)
 }
 
 func splitLogicalTerm(term LogicalTerm, mapping schema.RegisterLimbsMap) LogicalTerm {
@@ -122,14 +122,7 @@ func splitTerm(term Term, mapping schema.RegisterLimbsMap) Term {
 	case *LabelledConst:
 		return t
 	case *RegisterAccess:
-		if t.Register.IsUsed() {
-			return splitRegisterAccess(t, mapping)
-		}
-		// NOTE: this indicates an unused register access.  Currently, this can
-		// only occur for the selector column of a lookup.  This behaviour maybe
-		// deprecated in the future, and that would make this check
-		// unnecessary.
-		return t
+		return splitRegisterAccess(t, mapping)
 	case *Exp:
 		return ir.Exponent(splitTerm(t.Arg, mapping), t.Pow)
 	case *Mul:
@@ -166,6 +159,12 @@ func splitRegisterAccess(term *RegisterAccess, mapping schema.RegisterLimbsMap)
 	for i, limb := range limbs {
 		terms[i] = &ir.RegisterAccess[Term]{Register: limb, Shift: term.Shift}
 	}
+	// Check whether vector required, or not
+	if len(limbs) == 1 {
+		// NOTE: we cannot return the original term directly, as its index may
+		// differ under the limb mapping.
+		return terms[0]
+	}
 	//
 	return ir.NewVectorAccess(terms)
 }

pkg/ir/mir/constraint.go

@@ -14,9 +14,14 @@ package mir
 
 import (
 	"github.com/consensys/gnark-crypto/ecc/bls12-377/fr"
-	"github.com/consensys/go-corset/pkg/ir"
 	"github.com/consensys/go-corset/pkg/schema"
 	"github.com/consensys/go-corset/pkg/schema/constraint"
+	"github.com/consensys/go-corset/pkg/schema/constraint/interleaving"
+	"github.com/consensys/go-corset/pkg/schema/constraint/lookup"
+	"github.com/consensys/go-corset/pkg/schema/constraint/permutation"
+	"github.com/consensys/go-corset/pkg/schema/constraint/ranged"
+	"github.com/consensys/go-corset/pkg/schema/constraint/sorted"
+	"github.com/consensys/go-corset/pkg/schema/constraint/vanishing"
 	"github.com/consensys/go-corset/pkg/trace"
 	"github.com/consensys/go-corset/pkg/util"
 	"github.com/consensys/go-corset/pkg/util/collection/bit"
@@ -41,36 +46,36 @@ func NewAssertion(handle string, ctx schema.ModuleId, term LogicalTerm) Constrai
 func NewVanishingConstraint(handle string, ctx schema.ModuleId, domain util.Option[int],
 	term LogicalTerm) Constraint {
 	//
-	return Constraint{constraint.NewVanishingConstraint(handle, ctx, domain, term)}
+	return Constraint{vanishing.NewConstraint(handle, ctx, domain, term)}
 }
 
 // NewInterleavingConstraint creates a new interleaving constraint with a given handle.
 func NewInterleavingConstraint(handle string, targetContext schema.ModuleId,
 	sourceContext schema.ModuleId, target Term, sources []Term) Constraint {
-	return Constraint{constraint.NewInterleavingConstraint(handle, targetContext, sourceContext, target, sources)}
+	return Constraint{interleaving.NewConstraint(handle, targetContext, sourceContext, target, sources)}
 }
 
 // NewLookupConstraint creates a new lookup constraint with a given handle.
-func NewLookupConstraint(handle string, targets []ir.Enclosed[[]Term], sources []ir.Enclosed[[]Term]) Constraint {
-	return Constraint{constraint.NewLookupConstraint(handle, targets, sources)}
+func NewLookupConstraint(handle string, targets []lookup.Vector[Term], sources []lookup.Vector[Term]) Constraint {
+	return Constraint{lookup.NewConstraint(handle, targets, sources)}
 }
 
 // NewPermutationConstraint creates a new permutation
 func NewPermutationConstraint(handle string, context schema.ModuleId, targets []schema.RegisterId,
 	sources []schema.RegisterId) Constraint {
-	return Constraint{constraint.NewPermutationConstraint(handle, context, targets, sources)}
+	return Constraint{permutation.NewPermutationConstraint(handle, context, targets, sources)}
 }
 
 // NewRangeConstraint constructs a new Range constraint!
 func NewRangeConstraint(handle string, ctx schema.ModuleId, expr Term, bitwidth uint) Constraint {
-	return Constraint{constraint.NewRangeConstraint(handle, ctx, expr, bitwidth)}
+	return Constraint{ranged.NewRangeConstraint(handle, ctx, expr, bitwidth)}
 }
 
 // NewSortedConstraint creates a new Sorted
 func NewSortedConstraint(handle string, context schema.ModuleId, bitwidth uint, selector util.Option[Term],
 	sources []Term, signs []bool, strict bool) Constraint {
 	//
-	return Constraint{constraint.NewSortedConstraint(handle, context, bitwidth, selector, sources, signs, strict)}
+	return Constraint{sorted.NewSortedConstraint(handle, context, bitwidth, selector, sources, signs, strict)}
 }
 
 // Accepts determines whether a given constraint accepts a given trace or