Merge pull request #379 from Consensys/378-permit-constraints-with-vo…

…id-context

feat: support constraints with `void` context

pkg/binfile/constraint.go

@@ -62,8 +62,16 @@ func (e jsonConstraint) addToSchema(colmap map[uint]uint, schema *hir.Schema) {
 		domain := e.Vanishes.Domain.toHir()
 		// Determine enclosing module
 		ctx := expr.Context(schema)
-		// Construct the vanishing constraint
-		schema.AddVanishingConstraint(e.Vanishes.Handle, ctx, domain, expr)
+		// Check for vacuous constraint (i.e. one which evaluates to a constant)
+		if constant := expr.AsConstant(); constant != nil {
+			// Constraint outcome known at compile time.
+			if !constant.IsZero() {
+				panic(fmt.Sprintf("constraint %s always fails (i.e. evaluates to constant value %s)", e.Vanishes.Handle, constant))
+			}
+		} else {
+			// Construct the vanishing constraint
+			schema.AddVanishingConstraint(e.Vanishes.Handle, ctx, domain, expr)
+		}
 	} else if e.Lookup != nil {
 		sources := jsonExprsToHirUnit(e.Lookup.From, colmap, schema)
 		targets := jsonExprsToHirUnit(e.Lookup.To, colmap, schema)

pkg/hir/expr.go

@@ -31,6 +31,11 @@ type Expr interface {
 	// row which does not exist (e.g. at index -1); secondly, if
 	// it accesses a column which does not exist.
 	EvalAllAt(int, trace.Trace) []fr.Element
+
+	// AsConstant determines whether or not this is a constant expression.  If
+	// so, the constant is returned; otherwise, nil is returned.  NOTE: this
+	// does not perform any form of simplification to determine this.
+	AsConstant() *fr.Element
 }
 
 // ============================================================================
@@ -68,6 +73,11 @@ func (p *Add) RequiredCells(row int, tr trace.Trace) *util.AnySortedSet[trace.Ce
 	})
 }
 
+// AsConstant determines whether or not this is a constant expression.  If
+// so, the constant is returned; otherwise, nil is returned.  NOTE: this
+// does not perform any form of simplification to determine this.
+func (p *Add) AsConstant() *fr.Element { return nil }
+
 // ============================================================================
 // Subtraction
 // ============================================================================
@@ -103,6 +113,11 @@ func (p *Sub) RequiredCells(row int, tr trace.Trace) *util.AnySortedSet[trace.Ce
 	})
 }
 
+// AsConstant determines whether or not this is a constant expression.  If
+// so, the constant is returned; otherwise, nil is returned.  NOTE: this
+// does not perform any form of simplification to determine this.
+func (p *Sub) AsConstant() *fr.Element { return nil }
+
 // ============================================================================
 // Multiplication
 // ============================================================================
@@ -138,6 +153,11 @@ func (p *Mul) RequiredCells(row int, tr trace.Trace) *util.AnySortedSet[trace.Ce
 	})
 }
 
+// AsConstant determines whether or not this is a constant expression.  If
+// so, the constant is returned; otherwise, nil is returned.  NOTE: this
+// does not perform any form of simplification to determine this.
+func (p *Mul) AsConstant() *fr.Element { return nil }
+
 // ============================================================================
 // Exponentiation
 // ============================================================================
@@ -172,6 +192,11 @@ func (p *Exp) RequiredCells(row int, tr trace.Trace) *util.AnySortedSet[trace.Ce
 	return p.Arg.RequiredCells(row, tr)
 }
 
+// AsConstant determines whether or not this is a constant expression.  If
+// so, the constant is returned; otherwise, nil is returned.  NOTE: this
+// does not perform any form of simplification to determine this.
+func (p *Exp) AsConstant() *fr.Element { return nil }
+
 // ============================================================================
 // List
 // ============================================================================
@@ -207,6 +232,25 @@ func (p *List) RequiredCells(row int, tr trace.Trace) *util.AnySortedSet[trace.C
 	})
 }
 
+// AsConstant determines whether or not this is a constant expression.  If
+// so, the constant is returned; otherwise, nil is returned.  NOTE: this
+// does not perform any form of simplification to determine this.
+func (p *List) AsConstant() *fr.Element {
+	var constant *fr.Element = nil
+	// Check each expression in this list, one at a time.
+	for _, e := range p.Args {
+		c := e.AsConstant()
+		if c == nil || (constant != nil && constant.Cmp(c) != 0) {
+			// Either missing or mismatched constants
+			return nil
+		}
+		//
+		constant = c
+	}
+	// Done
+	return constant
+}
+
 // ============================================================================
 // Constant
 // ============================================================================
@@ -238,6 +282,11 @@ func (p *Constant) RequiredCells(row int, tr trace.Trace) *util.AnySortedSet[tra
 	return util.NewAnySortedSet[trace.CellRef]()
 }
 
+// AsConstant determines whether or not this is a constant expression.  If
+// so, the constant is returned; otherwise, nil is returned.  NOTE: this
+// does not perform any form of simplification to determine this.
+func (p *Constant) AsConstant() *fr.Element { return &p.Val }
+
 // ============================================================================
 // IfZero
 // ============================================================================
@@ -322,6 +371,11 @@ func (p *IfZero) RequiredCells(row int, tr trace.Trace) *util.AnySortedSet[trace
 	return set
 }
 
+// AsConstant determines whether or not this is a constant expression.  If
+// so, the constant is returned; otherwise, nil is returned.  NOTE: this
+// does not perform any form of simplification to determine this.
+func (p *IfZero) AsConstant() *fr.Element { return nil }
+
 // ============================================================================
 // Normalise
 // ============================================================================
@@ -356,6 +410,11 @@ func (p *Normalise) RequiredCells(row int, tr trace.Trace) *util.AnySortedSet[tr
 	return p.Arg.RequiredCells(row, tr)
 }
 
+// AsConstant determines whether or not this is a constant expression.  If
+// so, the constant is returned; otherwise, nil is returned.  NOTE: this
+// does not perform any form of simplification to determine this.
+func (p *Normalise) AsConstant() *fr.Element { return nil }
+
 // ============================================================================
 // ColumnAccess
 // ============================================================================
@@ -407,3 +466,8 @@ func (p *ColumnAccess) RequiredCells(row int, tr trace.Trace) *util.AnySortedSet
 
 	return set
 }
+
+// AsConstant determines whether or not this is a constant expression.  If
+// so, the constant is returned; otherwise, nil is returned.  NOTE: this
+// does not perform any form of simplification to determine this.
+func (p *ColumnAccess) AsConstant() *fr.Element { return nil }