Skip to content

Commit

Permalink
Merge pull request #209 from Consensys/208-support-lookup-constraints…
Browse files Browse the repository at this point in the history
…-in-binfile

Support for Lookups in binfile
  • Loading branch information
DavePearce authored Jul 4, 2024
2 parents 4f5dd3e + 75cffae commit b2d1668
Show file tree
Hide file tree
Showing 3 changed files with 38 additions and 0 deletions.
20 changes: 20 additions & 0 deletions pkg/binfile/constraint.go
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ import (
type jsonConstraint struct {
Vanishes *jsonVanishingConstraint
Permutation *jsonPermutationConstraint
Lookup *jsonLookupConstraint
}

type jsonDomain struct {
Expand All @@ -29,6 +30,12 @@ type jsonPermutationConstraint struct {
To []string `json:"to"`
}

type jsonLookupConstraint struct {
Handle string `json:"handle"`
From []jsonTypedExpr `json:"included"`
To []jsonTypedExpr `json:"including"`
}

// =============================================================================
// Translation
// =============================================================================
Expand All @@ -48,6 +55,19 @@ func (e jsonConstraint) addToSchema(schema *hir.Schema) {
module, multiplier := sc.DetermineEnclosingModuleOfExpression(expr, schema)
// Construct the vanishing constraint
schema.AddVanishingConstraint(e.Vanishes.Handle, module, multiplier, domain, expr)
} else if e.Lookup != nil {
sources := jsonExprsToHirUnit(e.Lookup.From, schema)
targets := jsonExprsToHirUnit(e.Lookup.To, schema)
source, source_multiplier, err1 := sc.DetermineEnclosingModuleOfExpressions(sources, schema)
target, target_multiplier, err2 := sc.DetermineEnclosingModuleOfExpressions(targets, schema)
// Error check
if err1 != nil {
panic(err1.Error)
} else if err2 != nil {
panic(err2.Error)
}
// Add constraint
schema.AddLookupConstraint(e.Lookup.Handle, source, source_multiplier, target, target_multiplier, sources, targets)
} else if e.Permutation == nil {
// Catch all
panic("Unknown JSON constraint encountered")
Expand Down
9 changes: 9 additions & 0 deletions pkg/binfile/expr.go
Original file line number Diff line number Diff line change
Expand Up @@ -164,3 +164,12 @@ func jsonListToHir(Args []jsonTypedExpr, schema *hir.Schema) hir.Expr {

return &hir.List{Args: args}
}

func jsonExprsToHirUnit(Args []jsonTypedExpr, schema *hir.Schema) []hir.UnitExpr {
args := make([]hir.UnitExpr, len(Args))
for i := 0; i < len(Args); i++ {
args[i] = hir.NewUnitExpr(Args[i].ToHir(schema))
}

return args
}
9 changes: 9 additions & 0 deletions pkg/hir/util.go
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,15 @@ type UnitExpr struct {
expr Expr
}

// NewUnitExpr 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 NewUnitExpr(expr Expr) UnitExpr {
return UnitExpr{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.
Expand Down

0 comments on commit b2d1668

Please sign in to comment.