From 0d43888c7bde3e6e9971431ab3468553454077a6 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Wed, 6 Nov 2024 10:22:59 +1300 Subject: [PATCH] Support constraints with `void` context 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. --- pkg/binfile/constraint.go | 12 ++++++-- pkg/hir/expr.go | 64 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 74 insertions(+), 2 deletions(-) diff --git a/pkg/binfile/constraint.go b/pkg/binfile/constraint.go index ff797ad..959b2ea 100644 --- a/pkg/binfile/constraint.go +++ b/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) diff --git a/pkg/hir/expr.go b/pkg/hir/expr.go index 25fc8e5..279ac93 100644 --- a/pkg/hir/expr.go +++ b/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 }