Merge pull request #375 from Consensys/373-parse-range-constraints-fr…

…om-binfile

feat: parse range constraints from binfile

pkg/air/gadgets/bits.go

@@ -51,7 +51,7 @@ func ApplyBitwidthGadget(col uint, nbits uint, schema *air.Schema) {
 		// Create Column + Constraint
 		es[i] = air.NewColumnAccess(index+i, 0).Mul(air.NewConst(coefficient))
 
-		schema.AddRangeConstraint(index+i, &fr256)
+		schema.AddRangeConstraint(index+i, fr256)
 		// Update coefficient
 		coefficient.Mul(&coefficient, &fr256)
 	}

pkg/air/schema.go

@@ -22,6 +22,9 @@ type LookupConstraint = *constraint.LookupConstraint[*ColumnAccess]
 // VanishingConstraint captures the essence of a vanishing constraint at the AIR level.
 type VanishingConstraint = *constraint.VanishingConstraint[constraint.ZeroTest[Expr]]
 
+// RangeConstraint captures the essence of a range constraints at the AIR level.
+type RangeConstraint = *constraint.RangeConstraint[*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.
 type PermutationConstraint = *constraint.PermutationConstraint
@@ -150,8 +153,11 @@ func (p *Schema) AddVanishingConstraint(handle string, context trace.Context, do
 }
 
 // AddRangeConstraint appends a new range constraint.
-func (p *Schema) AddRangeConstraint(column uint, bound *fr.Element) {
-	p.constraints = append(p.constraints, constraint.NewRangeConstraint(column, bound))
+func (p *Schema) AddRangeConstraint(column uint, bound fr.Element) {
+	col := p.Columns().Nth(column)
+	handle := col.QualifiedName(p)
+	tc := constraint.NewRangeConstraint[*ColumnAccess](handle, col.Context(), NewColumnAccess(column, 0), bound)
+	p.constraints = append(p.constraints, tc)
 }
 
 // ============================================================================

pkg/binfile/constraint.go

@@ -13,6 +13,7 @@ type jsonConstraint struct {
 	Vanishes    *jsonVanishingConstraint
 	Permutation *jsonPermutationConstraint
 	Lookup      *jsonLookupConstraint
+	InRange     *jsonRangeConstraint
 }
 
 type jsonDomain struct {
@@ -38,6 +39,12 @@ type jsonLookupConstraint struct {
 	To     []jsonTypedExpr `json:"including"`
 }
 
+type jsonRangeConstraint struct {
+	Handle string        `json:"handle"`
+	Expr   jsonTypedExpr `json:"exp"`
+	Max    jsonExprConst `json:"max"`
+}
+
 // =============================================================================
 // Translation
 // =============================================================================
@@ -70,6 +77,16 @@ func (e jsonConstraint) addToSchema(colmap map[uint]uint, schema *hir.Schema) {
 		}
 		// Add constraint
 		schema.AddLookupConstraint(e.Lookup.Handle, sourceCtx, targetCtx, sources, targets)
+	} else if e.InRange != nil {
+		// Translate the vanishing expression
+		expr := e.InRange.Expr.ToHir(colmap, schema)
+		// Determine enclosing module
+		ctx := expr.Context(schema)
+		// Convert bound into max
+		bound := e.InRange.Max.ToField()
+		handle := expr.Lisp(schema).String(true)
+		// Construct the vanishing constraint
+		schema.AddRangeConstraint(handle, ctx, expr, bound)
 	} else if e.Permutation == nil {
 		// Catch all
 		panic("Unknown JSON constraint encountered")

pkg/binfile/constraint_set.go

@@ -174,8 +174,9 @@ func allocateRegisters(cs *constraintSet, schema *hir.Schema) map[uint]uint {
 			// Add column for this
 			cid := schema.AddDataColumn(ctx, handle.column, col_type)
 			// Check whether a type constraint required or not.
-			if c.MustProve {
-				schema.AddTypeConstraint(cid, col_type)
+			if c.MustProve && col_type.AsUint() != nil {
+				bound := col_type.AsUint().Bound()
+				schema.AddRangeConstraint(c.Handle, ctx, &hir.ColumnAccess{Column: cid, Shift: 0}, *bound)
 			}
 		}
 	}

pkg/binfile/expr.go

@@ -76,6 +76,20 @@ func (e *jsonTypedExpr) ToHir(colmap map[uint]uint, schema *hir.Schema) hir.Expr
 // ToHir converts a big integer represented as a sequence of unsigned 32bit
 // words into HIR constant expression.
 func (e *jsonExprConst) ToHir(schema *hir.Schema) hir.Expr {
+	return &hir.Constant{Val: e.ToField()}
+}
+
+func (e *jsonExprConst) ToField() fr.Element {
+	var num fr.Element
+	//
+	val := e.ToBigInt()
+	// Construct Field Value
+	num.SetBigInt(val)
+	//
+	return num
+}
+
+func (e *jsonExprConst) ToBigInt() *big.Int {
 	sign := int(e.BigInt[0].(float64))
 	words := e.BigInt[1].([]any)
 	// Begin
@@ -100,12 +114,8 @@ func (e *jsonExprConst) ToHir(schema *hir.Schema) hir.Expr {
 	} else {
 		panic(fmt.Sprintf("Unknown BigInt sign: %d", sign))
 	}
-	// Construct Field Value
-	var num fr.Element
-
-	num.SetBigInt(val)
-	// Done!
-	return &hir.Constant{Val: num}
+	// Done
+	return val
 }
 
 func (e *jsonExprColumn) ToHir(colmap map[uint]uint, schema *hir.Schema) hir.Expr {

pkg/hir/lower.go

@@ -6,7 +6,6 @@ import (
 	"github.com/consensys/gnark-crypto/ecc/bls12-377/fr"
 	"github.com/consensys/go-corset/pkg/mir"
 	sc "github.com/consensys/go-corset/pkg/schema"
-	"github.com/consensys/go-corset/pkg/schema/constraint"
 )
 
 // LowerToMir lowers (or refines) an HIR table into an MIR schema.  That means
@@ -53,8 +52,12 @@ func lowerConstraintToMir(c sc.Constraint, schema *mir.Schema) {
 		for _, mir_expr := range mir_exprs {
 			schema.AddVanishingConstraint(v.Handle(), v.Context(), v.Domain(), mir_expr)
 		}
-	} else if v, ok := c.(*constraint.TypeConstraint); ok {
-		schema.AddTypeConstraint(v.Target(), v.Type())
+	} else if v, ok := c.(RangeConstraint); ok {
+		mir_exprs := v.Target().LowerTo(schema)
+		// Add individual constraints arising
+		for _, mir_expr := range mir_exprs {
+			schema.AddRangeConstraint(v.Handle(), v.Context(), mir_expr, v.Bound())
+		}
 	} else {
 		// Should be unreachable as no other constraint types can be added to a
 		// schema.

pkg/hir/parser.go

@@ -102,6 +102,8 @@ func (p *hirParser) parseDeclaration(s sexp.SExp) error {
 			return p.parseLookupDeclaration(e)
 		} else if e.Len() == 3 && e.MatchSymbols(1, "definterleaved") {
 			return p.parseInterleavingDeclaration(e)
+		} else if e.Len() == 3 && e.MatchSymbols(1, "definrange") {
+			return p.parseRangeDeclaration(e)
 		}
 	}
 	// Error
@@ -176,7 +178,11 @@ func (p *hirParser) parseColumnDeclaration(e sexp.SExp) error {
 	}
 	// Register column
 	cid := p.env.AddDataColumn(p.module, columnName, columnType)
-	p.env.schema.AddTypeConstraint(cid, columnType)
+	// Apply type constraint (if applicable)
+	if columnType.AsUint() != nil {
+		bound := columnType.AsUint().Bound()
+		p.env.schema.AddRangeConstraint(columnName, p.module, &ColumnAccess{cid, 0}, *bound)
+	}
 	//
 	return nil
 }
@@ -409,6 +415,37 @@ func (p *hirParser) parseInterleavingDeclaration(l *sexp.List) error {
 	return nil
 }
 
+// Parse a range constraint
+func (p *hirParser) parseRangeDeclaration(l *sexp.List) error {
+	var bound fr.Element
+	// Check bound
+	if l.Get(2).AsSymbol() == nil {
+		return p.translator.SyntaxError(l.Get(2), "malformed bound")
+	}
+	// Parse bound
+	if _, err := bound.SetString(l.Get(2).AsSymbol().Value); err != nil {
+		return p.translator.SyntaxError(l.Get(2), "malformed bound")
+	}
+	// Parse expression
+	expr, err := p.translator.Translate(l.Get(1))
+	if err != nil {
+		return err
+	}
+	// Determine evaluation context of expression.
+	ctx := expr.Context(p.env.schema)
+	// Sanity check we have a sensible context here.
+	if ctx.IsConflicted() {
+		return p.translator.SyntaxError(l.Get(1), "conflicting evaluation context")
+	} else if ctx.IsVoid() {
+		return p.translator.SyntaxError(l.Get(1), "empty evaluation context")
+	}
+	//
+	handle := l.Get(1).String(true)
+	p.env.schema.AddRangeConstraint(handle, ctx, expr, bound)
+	//
+	return nil
+}
+
 // Parse a property assertion
 func (p *hirParser) parseAssertionDeclaration(elements []sexp.SExp) error {
 	handle := elements[1].AsSymbol().Value

pkg/hir/schema.go

@@ -3,6 +3,7 @@ package hir
 import (
 	"fmt"
 
+	"github.com/consensys/gnark-crypto/ecc/bls12-377/fr"
 	"github.com/consensys/go-corset/pkg/schema"
 	sc "github.com/consensys/go-corset/pkg/schema"
 	"github.com/consensys/go-corset/pkg/schema/assignment"
@@ -24,6 +25,9 @@ type VanishingConstraint = *constraint.VanishingConstraint[ZeroArrayTest]
 // certain expression forms cannot be permitted (e.g. the use of lists).
 type LookupConstraint = *constraint.LookupConstraint[UnitExpr]
 
+// RangeConstraint captures the essence of a range constraints at the HIR level.
+type RangeConstraint = *constraint.RangeConstraint[MaxExpr]
+
 // PropertyAssertion captures the notion of an arbitrary property which should
 // hold for all acceptable traces.  However, such a property is not enforced by
 // the prover.
@@ -127,12 +131,11 @@ func (p *Schema) AddVanishingConstraint(handle string, context trace.Context, do
 		constraint.NewVanishingConstraint(handle, context, domain, ZeroArrayTest{expr}))
 }
 
-// AddTypeConstraint appends a new range constraint.
-func (p *Schema) AddTypeConstraint(target uint, t sc.Type) {
+// AddRangeConstraint appends a new range constraint with a raw bound.
+func (p *Schema) AddRangeConstraint(handle string, context trace.Context, expr Expr, bound fr.Element) {
 	// Check whether is a field type, as these can actually be ignored.
-	if t.AsField() == nil {
-		p.constraints = append(p.constraints, constraint.NewTypeConstraint(target, t))
-	}
+	maxExpr := MaxExpr{expr}
+	p.constraints = append(p.constraints, constraint.NewRangeConstraint[MaxExpr](handle, context, maxExpr, bound))
 }
 
 // AddPropertyAssertion appends a new property assertion.

pkg/hir/util.go

@@ -2,6 +2,7 @@ package hir
 
 import (
 	"github.com/consensys/gnark-crypto/ecc/bls12-377/fr"
+	"github.com/consensys/go-corset/pkg/mir"
 	sc "github.com/consensys/go-corset/pkg/schema"
 	"github.com/consensys/go-corset/pkg/sexp"
 	tr "github.com/consensys/go-corset/pkg/trace"
@@ -133,3 +134,80 @@ func (e UnitExpr) RequiredCells(row int, trace tr.Trace) *util.AnySortedSet[tr.C
 func (e UnitExpr) Lisp(schema sc.Schema) sexp.SExp {
 	return e.expr.Lisp(schema)
 }
+
+// ============================================================================
+// MaxExpr
+// ============================================================================
+
+// MaxExpr is an adaptor for a general expression which can be used in
+// situations where an Evaluable expression is required.  This performs a
+// similar function to the ZeroArrayTest, but actually produces a value.
+// Specifically, the value produced is always the maximum of all values
+// produced.  This is only useful in specific situations (e.g. checking range
+// constraints).
+type MaxExpr struct {
+	//
+	expr Expr
+}
+
+// NewMaxExpr constructs a unit wrapper around an HIR expression.  In essence,
+// this introduces a runtime check that the given expression only every reduces
+// to a single value.  Evaluation of this expression will panic if that
+// condition does not hold.  The intention is that this error is checked for
+// upstream (e.g. as part of the compiler front end).
+func NewMaxExpr(expr Expr) MaxExpr {
+	return MaxExpr{expr}
+}
+
+// EvalAt evaluates a column access at a given row in a trace, which returns the
+// value at that row of the column in question or nil is that row is
+// out-of-bounds.
+func (e MaxExpr) EvalAt(k int, trace tr.Trace) fr.Element {
+	vals := e.expr.EvalAllAt(k, trace)
+	//
+	max := fr.NewElement(0)
+	//
+	for _, v := range vals {
+		if max.Cmp(&v) < 0 {
+			max = v
+		}
+	}
+	//
+	return max
+}
+
+// Bounds returns max shift in either the negative (left) or positive
+// direction (right).
+func (e MaxExpr) Bounds() util.Bounds {
+	return e.expr.Bounds()
+}
+
+// Context determines the evaluation context (i.e. enclosing module) for this
+// expression.
+func (e MaxExpr) Context(schema sc.Schema) tr.Context {
+	return e.expr.Context(schema)
+}
+
+// RequiredColumns returns the set of columns on which this term depends.
+// That is, columns whose values may be accessed when evaluating this term
+// on a given trace.
+func (e MaxExpr) RequiredColumns() *util.SortedSet[uint] {
+	return e.expr.RequiredColumns()
+}
+
+// RequiredCells returns the set of trace cells on which this term depends.
+// In this case, that is the empty set.
+func (e MaxExpr) RequiredCells(row int, trace tr.Trace) *util.AnySortedSet[tr.CellRef] {
+	return e.expr.RequiredCells(row, trace)
+}
+
+// LowerTo lowers a max expressions down to one or more expressions at the MIR level.
+func (e MaxExpr) LowerTo(schema *mir.Schema) []mir.Expr {
+	return e.expr.LowerTo(schema)
+}
+
+// Lisp converts this schema element into a simple S-Expression, for example
+// so it can be printed.
+func (e MaxExpr) Lisp(schema sc.Schema) sexp.SExp {
+	return e.expr.Lisp(schema)
+}