From 6898249c9f9d1ed4706505761303a3884e42b527 Mon Sep 17 00:00:00 2001 From: DavePearce Date: Tue, 29 Oct 2024 17:48:03 +0000 Subject: [PATCH 1/2] Support interleaving constraints in binfile This adds support for parsing interleaving constraints out of the binfile. --- pkg/binfile/computation.go | 159 ++++++++++++++++++++++++------------- 1 file changed, 104 insertions(+), 55 deletions(-) diff --git a/pkg/binfile/computation.go b/pkg/binfile/computation.go index 5e006cf..7ba72a3 100644 --- a/pkg/binfile/computation.go +++ b/pkg/binfile/computation.go @@ -14,7 +14,8 @@ type jsonComputationSet struct { } type jsonComputation struct { - Sorted *jsonSortedComputation + Sorted *jsonSortedComputation + Interleaved *jsonInterleavedComputation } type jsonSortedComputation struct { @@ -23,6 +24,11 @@ type jsonSortedComputation struct { Signs []bool `json:"signs"` } +type jsonInterleavedComputation struct { + Froms []string `json:"froms"` + Target string `json:"target"` +} + // ============================================================================= // Translation // ============================================================================= @@ -38,62 +44,105 @@ 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())) + } - 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())) - } + 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 +} - 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)) +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) + // Finally, add the sorted permutation assignment + schema.AddAssignment(assignment.NewInterleaving(ctx, dst_hnd.column, sources)) + // Update allocation information. + colmap[target_id] = index + // + return index + 1 +} + +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)") + } + + 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 } From 00168e83ae2d0b0ff065fa4511603030cd96a66e Mon Sep 17 00:00:00 2001 From: DavePearce Date: Tue, 29 Oct 2024 18:09:18 +0000 Subject: [PATCH 2/2] Determine type for interleaved columns This determines the least type which includes all the columns being interleaved as the type of the target column. --- pkg/binfile/computation.go | 10 +++++++++- pkg/hir/parser.go | 2 +- pkg/schema/assignment/interleave.go | 4 ++-- pkg/schema/type.go | 17 +++++++++++++++++ 4 files changed, 29 insertions(+), 4 deletions(-) diff --git a/pkg/binfile/computation.go b/pkg/binfile/computation.go index 7ba72a3..4829d79 100644 --- a/pkg/binfile/computation.go +++ b/pkg/binfile/computation.go @@ -94,8 +94,16 @@ func addInterleavedComputation(c *jsonInterleavedComputation, index uint, 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)) + schema.AddAssignment(assignment.NewInterleaving(ctx, dst_hnd.column, sources, dst_type)) // Update allocation information. colmap[target_id] = index // diff --git a/pkg/hir/parser.go b/pkg/hir/parser.go index b84c4df..d9b2fdc 100644 --- a/pkg/hir/parser.go +++ b/pkg/hir/parser.go @@ -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 } diff --git a/pkg/schema/assignment/interleave.go b/pkg/schema/assignment/interleave.go index 2fde428..3fc0f9d 100644 --- a/pkg/schema/assignment/interleave.go +++ b/pkg/schema/assignment/interleave.go @@ -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} } diff --git a/pkg/schema/type.go b/pkg/schema/type.go index 3fb0c2c..7aac5dc 100644 --- a/pkg/schema/type.go +++ b/pkg/schema/type.go @@ -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 +}