Skip to content

Commit

Permalink
Support constraints with void context
Browse files Browse the repository at this point in the history
This adds partial support for constraints with `void` context.
Specifically, this is only support for constraints being read out of a
binfile, and also the constant evaluation is fairly limited.  If
necessary, it could be improved further down the track.
  • Loading branch information
DavePearce committed Nov 5, 2024
1 parent 452d062 commit 0d43888
Show file tree
Hide file tree
Showing 2 changed files with 74 additions and 2 deletions.
12 changes: 10 additions & 2 deletions pkg/binfile/constraint.go
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
64 changes: 64 additions & 0 deletions pkg/hir/expr.go
Original file line number Diff line number Diff line change
Expand Up @@ -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
}

// ============================================================================
Expand Down Expand Up @@ -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
// ============================================================================
Expand Down Expand Up @@ -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
// ============================================================================
Expand Down Expand Up @@ -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
// ============================================================================
Expand Down Expand Up @@ -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
// ============================================================================
Expand Down Expand Up @@ -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
// ============================================================================
Expand Down Expand Up @@ -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
// ============================================================================
Expand Down Expand Up @@ -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
// ============================================================================
Expand Down Expand Up @@ -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
// ============================================================================
Expand Down Expand Up @@ -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 }

0 comments on commit 0d43888

Please sign in to comment.