feat: splitting property assertions (#1321)

* enable previously broken tests

This enables several tests which were previously broken due to the lack
of splitting for property assertions.

* support splitting property assertions

Splitting property assertions is more challenging than expected since we
want to maintain the notion that a property is an execution computation,
rather than a term which can be reduced to an arithmetic expression.

* simplify Assertion type and tidy up

This simplifies the assertion type to take only a single generic
parameter F.

Author: DavePearce

pkg/corset/compiler/translator.go

@@ -645,8 +645,9 @@ func (t *translator) translateDefProperty(decl *ast.DefProperty) []SyntaxError {
 	assertion, errors := t.translateLogical(decl.Assertion, module, 0)
 	//
 	if len(errors) == 0 {
+		comp := term.NewLogicalComputation[word.BigEndian, hir.LogicalTerm, hir.Term](assertion)
 		// Add translated constraint
-		module.AddConstraint(hir.NewAssertion(decl.Handle, module.Id(), decl.Domain, assertion))
+		module.AddConstraint(hir.NewAssertion(decl.Handle, module.Id(), decl.Domain, comp))
 	}
 	// Done
 	return errors

pkg/ir/air/constraint.go

@@ -13,7 +13,6 @@
 package air
 
 import (
-	"github.com/consensys/go-corset/pkg/ir/term"
 	"github.com/consensys/go-corset/pkg/schema"
 	"github.com/consensys/go-corset/pkg/schema/constraint"
 	"github.com/consensys/go-corset/pkg/schema/constraint/interleaving"
@@ -39,7 +38,7 @@ import (
 type ConstraintBound[F field.Element[F]] interface {
 	schema.Constraint[F]
 
-	constraint.Assertion[F, term.Testable[F]] |
+	constraint.Assertion[F] |
 		interleaving.Constraint[F, *ColumnAccess[F]] |
 		lookup.Constraint[F, *ColumnAccess[F]] |
 		permutation.Constraint[F] |
@@ -63,9 +62,9 @@ func newAir[F field.Element[F], C ConstraintBound[F]](constraint C) Air[F, C] {
 
 // NewAssertion constructs a new AIR assertion
 func NewAssertion[F field.Element[F]](handle string, ctx schema.ModuleId, domain util.Option[int],
-	term term.Testable[F]) Assertion[F] {
+	term constraint.Property) Assertion[F] {
 	//
-	return newAir(constraint.NewAssertion(handle, ctx, domain, term))
+	return newAir(constraint.NewAssertion[F](handle, ctx, domain, term))
 }
 
 // NewInterleavingConstraint creates a new interleaving constraint with a given handle.

pkg/ir/air/schema.go

@@ -71,7 +71,7 @@ type (
 	// Assertion captures the notion of an arbitrary property which should hold for
 	// all acceptable traces.  However, such a property is not enforced by the
 	// prover.
-	Assertion[F field.Element[F]] = Air[F, constraint.Assertion[F, term.Testable[F]]]
+	Assertion[F field.Element[F]] = Air[F, constraint.Assertion[F]]
 	// InterleavingConstraint captures the essence of an interleaving constraint
 	// at the MIR level.
 	InterleavingConstraint[F field.Element[F]] = Air[F, interleaving.Constraint[F, *ColumnAccess[F]]]

pkg/ir/hir/constraint.go

@@ -38,10 +38,10 @@ type Constraint struct {
 }
 
 // NewAssertion constructs a new assertion
-func NewAssertion(handle string, ctx schema.ModuleId, domain util.Option[int], term LogicalTerm,
+func NewAssertion(handle string, ctx schema.ModuleId, domain util.Option[int], term constraint.Property,
 ) Constraint {
 	//
-	return Constraint{constraint.NewAssertion(handle, ctx, domain, term)}
+	return Constraint{constraint.NewAssertion[word.BigEndian](handle, ctx, domain, term)}
 }
 
 // NewVanishingConstraint constructs a new vanishing constraint