feat: support interleaving constraints in binfile

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,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
 }

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
 }

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}
 }

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
+}