Skip to content

Commit

Permalink
Merge pull request #372 from Consensys/319-support-interleaving-const…
Browse files Browse the repository at this point in the history 
…raints-in-binfile

feat: support interleaving constraints in binfile
  • Loading branch information
@DavePearce
DavePearce authored Oct 29, 2024
2 parents a386e3f + 00168e8 commit 89596bb
Show file tree
Hide file tree
Showing 4 changed files with 132 additions and 58 deletions.
167 changes: 112 additions & 55 deletions pkg/binfile/computation.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,8 @@ type jsonComputationSet struct {
}

type jsonComputation struct {
Sorted *jsonSortedComputation
Sorted *jsonSortedComputation
Interleaved *jsonInterleavedComputation
}

type jsonSortedComputation struct {
Expand All @@ -23,6 +24,11 @@ type jsonSortedComputation struct {
Signs []bool `json:"signs"`
}

type jsonInterleavedComputation struct {
Froms []string `json:"froms"`
Target string `json:"target"`
}

// =============================================================================
// Translation
// =============================================================================
Expand All @@ -38,62 +44,113 @@ func (e jsonComputationSet) addToSchema(columns []column, colmap map[uint]uint,
//
for _, c := range e.Computations {
if c.Sorted != nil {
targetIDs := asColumns(c.Sorted.Tos)
sourceIDs := asColumns(c.Sorted.Froms)
handle := asHandle(columns[sourceIDs[0]].Handle)
// Resolve enclosing module
mid, ok := schema.Modules().Find(func(m sc.Module) bool {
return m.Name() == handle.module
})
// Sanity check assumptions
if !ok {
panic(fmt.Sprintf("unknown module %s", handle.module))
} else if len(sourceIDs) != len(targetIDs) {
panic("differing number of source / target columns in sorted permutation")
}
// Convert source refs into column indexes
sources := make([]uint, len(sourceIDs))
// Convert target refs into columns
targets := make([]sc.Column, len(targetIDs))
//
ctx := trace.VoidContext()
//
for i, target_id := range targetIDs {
source_id := sourceIDs[i]
// Extract binfile info about target column
dst_col := columns[target_id]
dst_hnd := asHandle(dst_col.Handle)
// Determine schema column index for ith source column.
src_cid, ok := colmap[source_id]
if !ok {
h := asHandle(columns[source_id].Handle)
panic(fmt.Sprintf("unallocated source column %s.%s", h.module, h.column))
}
// Extract schema info about source column
src_col := schema.Columns().Nth(src_cid)
// Sanity check enclosing modules match
if src_col.Context().Module() != mid {
panic("inconsistent enclosing module for sorted permutation (source)")
}
index = addSortedComputation(c.Sorted, index, columns, colmap, schema)
} else if c.Interleaved != nil {
index = addInterleavedComputation(c.Interleaved, index, columns, colmap, schema)
} else {
panic("unknown computation encountered")
}
}
}

func addSortedComputation(sorted *jsonSortedComputation, index uint,
columns []column, colmap map[uint]uint, schema *hir.Schema) uint {
targetIDs := asColumns(sorted.Tos)
// Convert source refs into column indexes
ctx, sources := sourceColumnsFromHandles(sorted.Froms, columns, colmap, schema)
// Sanity checks
if len(sources) != len(targetIDs) {
panic("differing number of source / target columns in sorted permutation")
}
// Convert target refs into columns
targets := make([]sc.Column, len(targetIDs))
//
for i, target_id := range targetIDs {
// Extract binfile info about target column
dst_col := columns[target_id]
dst_hnd := asHandle(dst_col.Handle)
src_col := schema.Columns().Nth(sources[i])
// Sanity check source column type
if src_col.Type().AsUint() == nil {
panic(fmt.Sprintf("source column %s has field type", src_col.Name()))
}

targets[i] = sc.NewColumn(ctx, dst_hnd.column, src_col.Type())
// Update allocation information.
colmap[target_id] = index
index++
}
// Finally, add the sorted permutation assignment
schema.AddAssignment(assignment.NewSortedPermutation(ctx, targets, sorted.Signs, sources))
//
return index
}

func addInterleavedComputation(c *jsonInterleavedComputation, index uint,
columns []column, colmap map[uint]uint, schema *hir.Schema) uint {
// Convert column handles into column indices in the schema
ctx, sources := sourceColumnsFromHandles(c.Froms, columns, colmap, schema)
// Determine column handle
target_id := asColumn(c.Target)
dst_col := columns[target_id]
dst_hnd := asHandle(dst_col.Handle)
// Initially assume bottom type
var dst_type sc.Type = sc.NewUintType(0)
// Ensure each column's types included
for i := range sources {
src_col := schema.Columns().Nth(sources[i])
// Update the column type
dst_type = sc.Join(dst_type, src_col.Type())
}
// Finally, add the sorted permutation assignment
schema.AddAssignment(assignment.NewInterleaving(ctx, dst_hnd.column, sources, dst_type))
// Update allocation information.
colmap[target_id] = index
//
return index + 1
}

ctx = ctx.Join(src_col.Context())
// Sanity check we have a sensible type here.
if src_col.Type().AsUint() == nil {
panic(fmt.Sprintf("source column %s has field type", src_col.Name()))
} else if ctx.IsConflicted() {
panic(fmt.Sprintf("source column %s has conflicted evaluation context", src_col.Name()))
} else if ctx.IsVoid() {
panic(fmt.Sprintf("source column %s has void evaluation context", src_col.Name()))
}
func sourceColumnsFromHandles(handles []string, columns []column,
colmap map[uint]uint, schema *hir.Schema) (trace.Context, []uint) {
sourceIDs := asColumns(handles)
handle := asHandle(columns[sourceIDs[0]].Handle)
// Resolve enclosing module
mid, ok := schema.Modules().Find(func(m sc.Module) bool {
return m.Name() == handle.module
})
// Sanity check assumptions
if !ok {
panic(fmt.Sprintf("unknown module %s", handle.module))
}
// Convert source refs into column indexes
sources := make([]uint, len(sourceIDs))
//
ctx := trace.VoidContext()
//
for i, source_id := range sourceIDs {
// Determine schema column index for ith source column.
src_cid, ok := colmap[source_id]
if !ok {
h := asHandle(columns[source_id].Handle)
panic(fmt.Sprintf("unallocated source column %s.%s", h.module, h.column))
}
// Extract schema info about source column
src_col := schema.Columns().Nth(src_cid)
// Sanity check enclosing modules match
if src_col.Context().Module() != mid {
panic("inconsistent enclosing module for sorted permutation (source)")
}

sources[i] = src_cid
targets[i] = sc.NewColumn(ctx, dst_hnd.column, src_col.Type())
// Update allocation information.
colmap[target_id] = index
index++
}
// Finally, add the sorted permutation assignment
schema.AddAssignment(assignment.NewSortedPermutation(ctx, targets, c.Sorted.Signs, sources))
ctx = ctx.Join(src_col.Context())
// Sanity check we have a sensible type here.
if ctx.IsConflicted() {
panic(fmt.Sprintf("source column %s has conflicted evaluation context", src_col.Name()))
} else if ctx.IsVoid() {
panic(fmt.Sprintf("source column %s has void evaluation context", src_col.Name()))
}

sources[i] = src_cid
}
//
return ctx, sources
}
2 changes: 1 addition & 1 deletion pkg/hir/parser.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -404,7 +404,7 @@ func (p *hirParser) parseInterleavingDeclaration(l *sexp.List) error {
sources[i] = cid
}
// Add assignment
p.env.AddAssignment(assignment.NewInterleaving(ctx, sexpTarget.Value, sources))
p.env.AddAssignment(assignment.NewInterleaving(ctx, sexpTarget.Value, sources, &sc.FieldType{}))
// Done
return nil
}
Expand Down
4 changes: 2 additions & 2 deletions pkg/schema/assignment/interleave.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,11 +19,11 @@ type Interleaving struct {
}

// NewInterleaving constructs a new interleaving assignment.
func NewInterleaving(context tr.Context, name string, sources []uint) *Interleaving {
func NewInterleaving(context tr.Context, name string, sources []uint, datatype sc.Type) *Interleaving {
// Update multiplier
context = context.Multiply(uint(len(sources)))
// Fixme: determine interleaving type
target := sc.NewColumn(context, name, &sc.FieldType{})
target := sc.NewColumn(context, name, datatype)

return &Interleaving{target, sources}
}
Expand Down
17 changes: 17 additions & 0 deletions pkg/schema/type.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,3 +139,20 @@ func (p *FieldType) Accept(val fr.Element) bool {
func (p *FieldType) String() string {
return "𝔽"
}

// Join compute the Least Upper Bound of two types. For example, the lub of u16
// and u128 is u128, etc.
func Join(lhs Type, rhs Type) Type {
if lhs.AsField() != nil || rhs.AsField() != nil {
return &FieldType{}
}
//
uLhs := lhs.AsUint()
uRhs := rhs.AsUint()
//
if uLhs.nbits >= uRhs.nbits {
return uLhs
}
//
return uRhs
}

0 comments on commit 89596bb

Please sign in to comment.