feat: sort perspectives for register allocation

pkg/corset/allocation.go

@@ -22,12 +22,12 @@ import (
 type Register struct {
 	// Context (i.e. module + multiplier) of this register.
 	Context tr.Context
-	// Name of this register
-	Name string
 	// Underlying datatype of this register.
 	DataType sc.Type
 	// Source columns of this register
 	Sources []RegisterSource
+	// Cached name
+	cached_name *string
 }
 
 // IsActive determines whether or not this register is "active".  Inactive
@@ -60,21 +60,59 @@ func (r *Register) Merge(other *Register) {
 		panic("cannot merge registers from different context")
 	}
 	//
-	r.Name = fmt.Sprintf("%s_xor_%s", r.Name, other.Name)
 	r.DataType = schema.Join(r.DataType, other.DataType)
 	r.Sources = append(r.Sources, other.Sources...)
+	// Reset the cached name
+	r.cached_name = nil
 	// Deactivate other register
 	other.Deactivate()
 }
 
 // Deactivate marks a given register as no longer being required.  This happens
 // when one register is merged into another.
 func (r *Register) Deactivate() {
-	r.Name = ""
 	r.DataType = nil
 	r.Sources = nil
 }
 
+// Name returns the given name for this register.
+func (r *Register) Name() string {
+	if r.cached_name == nil {
+		// Construct registers name
+		names := make([]string, len(r.Sources))
+		// Sort by perspective name
+		slices.SortFunc(r.Sources, func(l RegisterSource, r RegisterSource) int {
+			return strings.Compare(l.Perspective(), r.Perspective())
+		})
+		//
+		for i, source := range r.Sources {
+			// FIXME: below is used instead of above in order to replicate the original
+			// Corset tool.  Eventually, this behaviour should be deprecated.
+			names[i] = source.name.Tail()
+		}
+		// Construct register name from list of names
+		name := constructRegisterName(names)
+		r.cached_name = &name
+	}
+	//
+	return *r.cached_name
+}
+
+// A simple algorithm for joining names together.
+func constructRegisterName(names []string) string {
+	str := ""
+	// Joing them together
+	for i, n := range names {
+		if i == 0 {
+			str = n
+		} else {
+			str = fmt.Sprintf("%s_xor_%s", str, n)
+		}
+	}
+	//
+	return str
+}
+
 // RegisterSource provides necessary information about source-level columns
 // allocated to a  given register.
 type RegisterSource struct {
@@ -212,10 +250,10 @@ func identicalType(lhs *RegisterGroup, rhs *RegisterGroup) bool {
 // Sort the registers into alphabetical order.
 func sortRegisters(view *RegisterAllocationView) {
 	slices.SortFunc(view.registers, func(l, r uint) int {
-		lhs := view.Register(l)
-		rhs := view.Register(r)
-		// Compare them alphabetically
-		return strings.Compare(lhs.Name, rhs.Name)
+		lhs := view.Register(l).Sources[0].name.String()
+		rhs := view.Register(r).Sources[0].name.String()
+		// Within perspective sort alphabetically by name
+		return strings.Compare(lhs, rhs)
 	})
 }
 
@@ -238,6 +276,8 @@ type RegisterAllocator struct {
 	allocation RegisterAllocation
 	// Maps perspectives to their "allocation slot"
 	perspectives map[string]uint
+	// Maps each slot to its perspective string.
+	slots []string
 	// Allocation matrix, where each innermost array has an entry for each
 	// perspective.  The allocation slot for a perspective determines its index
 	// within this array.  Entries can be "empty" if they are given MaxUint
@@ -252,6 +292,7 @@ func NewRegisterAllocator(allocation RegisterAllocation) *RegisterAllocator {
 	allocator := RegisterAllocator{
 		allocation,
 		make(map[string]uint, 0),
+		make([]string, 0),
 		make([]RegisterGroup, 0),
 	}
 	// Identify all perspectives
@@ -321,6 +362,7 @@ func (p *RegisterAllocator) allocatePerspective(perspective string) {
 	if _, ok := p.perspectives[perspective]; !ok {
 		slot := uint(len(p.perspectives))
 		p.perspectives[perspective] = slot
+		p.slots = append(p.slots, perspective)
 	}
 }
 

pkg/corset/environment.go

@@ -226,16 +226,6 @@ func (p *GlobalEnvironment) allocateArray(col *ColumnBinding, ctx util.Path, pat
 // Allocate a single register.
 func (p *GlobalEnvironment) allocateUnit(column *ColumnBinding, ctx util.Path, path util.Path, datatype sc.Type) {
 	module := ctx.String()
-	// // The name is extracted from the different between the context and the //
-	// // path.  The context must be a prefix of the path and, essentially, //
-	// // identifies the concrete module where this column will eventually live.
-	// name := path.Slice(ctx.Depth()).String()[1:]
-	// // Neaten the name up a bit
-	// name = strings.ReplaceAll(name, "/", "$")
-	//
-	// FIXME: below is used instead of above in order to replicate the original
-	// Corset tool.  Eventually, this behaviour should be deprecated.
-	name := path.Tail()
 	//
 	moduleId := p.modules[module].Id
 	regId := uint(len(p.registers))
@@ -250,9 +240,9 @@ func (p *GlobalEnvironment) allocateUnit(column *ColumnBinding, ctx util.Path, p
 	// Allocate register
 	p.registers = append(p.registers, Register{
 		tr.NewContext(moduleId, column.multiplier),
-		name,
 		datatype,
 		[]RegisterSource{source},
+		nil,
 	})
 	// Map column to register
 	p.columns[path.String()] = regId

pkg/corset/translator.go

@@ -94,7 +94,7 @@ func (t *translator) translateInputColumnsInModule(module string) {
 			panic("inactive register encountered")
 		} else if regInfo.IsInput() {
 			// Declare column at HIR level.
-			cid := t.schema.AddDataColumn(regInfo.Context, regInfo.Name, regInfo.DataType)
+			cid := t.schema.AddDataColumn(regInfo.Context, regInfo.Name(), regInfo.DataType)
 			// Prove underlying types (as necessary)
 			t.translateTypeConstraints(regIndex)
 			// Sanity check
@@ -158,7 +158,7 @@ func (t *translator) translateTypeConstraints(regIndex uint) {
 		}
 		// Add appropriate type constraint
 		bound := regInfo.DataType.AsUint().Bound()
-		t.schema.AddRangeConstraint(regInfo.Name, regInfo.Context, &hir.ColumnAccess{Column: regIndex, Shift: 0}, bound)
+		t.schema.AddRangeConstraint(regInfo.Name(), regInfo.Context, &hir.ColumnAccess{Column: regIndex, Shift: 0}, bound)
 	}
 }
 
@@ -331,7 +331,7 @@ func (t *translator) translateDefInterleaved(decl *DefInterleaved, module util.P
 		sources[i] = t.env.RegisterOf(source.Path())
 	}
 	// Register assignment
-	cid := t.schema.AddAssignment(assignment.NewInterleaving(target.Context, target.Name, sources, target.DataType))
+	cid := t.schema.AddAssignment(assignment.NewInterleaving(target.Context, target.Name(), sources, target.DataType))
 	// Sanity check column identifiers align.
 	if cid != targetId {
 		err := fmt.Sprintf("inconsitent (interleaved) column identifier (%d v %d)", cid, targetId)
@@ -358,7 +358,7 @@ func (t *translator) translateDefPermutation(decl *DefPermutation, module util.P
 		targetId := t.env.RegisterOf(targetPath)
 		target := t.env.Register(targetId)
 		// Construct columns
-		targets[i] = sc.NewColumn(target.Context, target.Name, target.DataType)
+		targets[i] = sc.NewColumn(target.Context, target.Name(), target.DataType)
 		sources[i] = t.env.RegisterOf(decl.Sources[i].Path())
 		signs[i] = decl.Signs[i]
 		// Record first CID

pkg/test/valid_corset_test.go

@@ -909,6 +909,10 @@ func Test_Perspective_28(t *testing.T) {
 	Check(t, false, "perspective_28")
 }
 
+func Test_Perspective_29(t *testing.T) {
+	Check(t, false, "perspective_29")
+}
+
 // ===================================================================
 // Let
 // ===================================================================

testdata/perspective_29.accepts

@@ -0,0 +1,31 @@
+{ "A": [], "P": [], "Q": [], "B_xor_C": [] }
+;;
+{ "A": [0], "P": [0], "Q": [0], "B_xor_C": [0] }
+{ "A": [0], "P": [0], "Q": [0], "B_xor_C": [1] }
+{ "A": [0], "P": [0], "Q": [0], "B_xor_C": [2] }
+{ "A": [0], "P": [0], "Q": [0], "B_xor_C": [3] }
+{ "A": [1], "P": [0], "Q": [0], "B_xor_C": [0] }
+{ "A": [1], "P": [0], "Q": [0], "B_xor_C": [1] }
+{ "A": [1], "P": [0], "Q": [0], "B_xor_C": [2] }
+{ "A": [1], "P": [0], "Q": [0], "B_xor_C": [3] }
+{ "A": [2], "P": [0], "Q": [0], "B_xor_C": [0] }
+{ "A": [2], "P": [0], "Q": [0], "B_xor_C": [1] }
+{ "A": [2], "P": [0], "Q": [0], "B_xor_C": [2] }
+{ "A": [2], "P": [0], "Q": [0], "B_xor_C": [3] }
+{ "A": [3], "P": [0], "Q": [0], "B_xor_C": [0] }
+{ "A": [3], "P": [0], "Q": [0], "B_xor_C": [1] }
+{ "A": [3], "P": [0], "Q": [0], "B_xor_C": [2] }
+{ "A": [3], "P": [0], "Q": [0], "B_xor_C": [3] }
+;; perspective p1
+{ "A": [0], "P": [1], "Q": [0], "B_xor_C": [0] }
+{ "A": [1], "P": [1], "Q": [0], "B_xor_C": [1] }
+{ "A": [2], "P": [1], "Q": [0], "B_xor_C": [2] }
+{ "A": [3], "P": [1], "Q": [0], "B_xor_C": [3] }
+;; perspective p2
+{ "A": [0], "P": [0], "Q": [1], "B_xor_C": [0] }
+{ "A": [0], "P": [0], "Q": [1], "B_xor_C": [1] }
+{ "A": [0], "P": [0], "Q": [1], "B_xor_C": [2] }
+{ "A": [0], "P": [0], "Q": [1], "B_xor_C": [3] }
+{ "A": [1], "P": [0], "Q": [1], "B_xor_C": [0] }
+{ "A": [2], "P": [0], "Q": [1], "B_xor_C": [0] }
+{ "A": [3], "P": [0], "Q": [1], "B_xor_C": [0] }

testdata/perspective_29.lisp

@@ -0,0 +1,17 @@
+(defpurefun ((vanishes! :@loob :force) e0) e0)
+;;
+(defcolumns
+    ;; Column (not in perspective)
+    A
+    ;; Selector column for perspective p1
+    (P :binary@prove)
+    ;; Selector column for perspective p2
+    (Q :binary@prove))
+
+;; Section 2
+(defperspective p2 Q ((C :binary)))
+(defconstraint c2 (:perspective p2) (vanishes! (* A C)))
+
+;; Section 1
+(defperspective p1 P ((B :binary)))
+(defconstraint c1 (:perspective p1) (vanishes! (- A B)))

testdata/perspective_29.rejects

@@ -0,0 +1,21 @@
+{ "A": [0], "P": [1], "Q": [0], "B_xor_C": [1] }
+{ "A": [0], "P": [1], "Q": [0], "B_xor_C": [2] }
+{ "A": [0], "P": [1], "Q": [0], "B_xor_C": [3] }
+{ "A": [1], "P": [1], "Q": [0], "B_xor_C": [2] }
+{ "A": [1], "P": [1], "Q": [0], "B_xor_C": [3] }
+{ "A": [1], "P": [1], "Q": [0], "B_xor_C": [0] }
+{ "A": [2], "P": [1], "Q": [0], "B_xor_C": [0] }
+{ "A": [2], "P": [1], "Q": [0], "B_xor_C": [1] }
+{ "A": [2], "P": [1], "Q": [0], "B_xor_C": [3] }
+{ "A": [3], "P": [1], "Q": [0], "B_xor_C": [0] }
+{ "A": [3], "P": [1], "Q": [0], "B_xor_C": [1] }
+{ "A": [3], "P": [1], "Q": [0], "B_xor_C": [2] }
+{ "A": [1], "P": [0], "Q": [1], "B_xor_C": [1] }
+{ "A": [1], "P": [0], "Q": [1], "B_xor_C": [2] }
+{ "A": [1], "P": [0], "Q": [1], "B_xor_C": [3] }
+{ "A": [2], "P": [0], "Q": [1], "B_xor_C": [1] }
+{ "A": [2], "P": [0], "Q": [1], "B_xor_C": [2] }
+{ "A": [2], "P": [0], "Q": [1], "B_xor_C": [3] }
+{ "A": [3], "P": [0], "Q": [1], "B_xor_C": [1] }
+{ "A": [3], "P": [0], "Q": [1], "B_xor_C": [2] }
+{ "A": [3], "P": [0], "Q": [1], "B_xor_C": [3] }