[feat] Enforce semantics for write once memory (wom)

pkg/ir/hir/constraint.go

@@ -84,7 +84,7 @@ func NewPermutationConstraint(handle string, context schema.ModuleId, targets []
 	return Constraint{permutation.NewConstraint[word.BigEndian](handle, context, targets, sources)}
 }
 
-// NewRangeConstraint constructs a new Range constraint!
+// NewRangeConstraint constructs a new Range constraint
 func NewRangeConstraint(handle string, ctx schema.ModuleId, expr Term,
 	bitwidth uint) Constraint {
 	//

pkg/ir/mir/constraint.go

@@ -64,13 +64,27 @@ func NewLookupConstraint[F field.Element[F]](handle string, targets []LookupVect
 	return Constraint[F]{lookup.NewConstraint(handle, targets, sources)}
 }
 
+// NewSendConstraint creates a new "send to logUpBus" constraint; it doesn't take into account
+// the potential Id of the logup bus, which would for instance determine what shared randomness to use.
+func NewSendConstraint[F field.Element[F]](handle string, sources []register.Id) Constraint[F] {
+	// TODO
+	return Constraint[F]{}
+}
+
+// NewReceiveConstraint creates a new "receive from logUpBus" constraint; it doesn't take into account
+// the potential Id of the logup bus, which would for instance determine what shared randomness to use.
+func NewReceiveConstraint[F field.Element[F]](handle string, sources []register.Id) Constraint[F] {
+	// TODO
+	return Constraint[F]{}
+}
+
 // NewPermutationConstraint creates a new permutation
 func NewPermutationConstraint[F field.Element[F]](handle string, context schema.ModuleId, targets []register.Id,
 	sources []register.Id) Constraint[F] {
 	return Constraint[F]{permutation.NewConstraint[F](handle, context, targets, sources)}
 }
 
-// NewRangeConstraint constructs a new Range constraint!
+// NewRangeConstraint constructs a new Range constraint
 func NewRangeConstraint[F field.Element[F]](handle string, ctx schema.ModuleId, registers []*RegisterAccess[F],
 	bitwidths []uint) Constraint[F] {
 	//

pkg/schema/constraint/ranged/constraint.go

@@ -43,7 +43,7 @@ type Constraint[F field.Element[F], E term.Evaluable[F]] struct {
 	Bitwidths []uint
 }
 
-// NewConstraint constructs a new Range constraint!
+// NewConstraint constructs a new Range constraint
 func NewConstraint[F field.Element[F], E term.Evaluable[F]](handle string, context schema.ModuleId,
 	exprs []E, bitwidths []uint) Constraint[F, E] {
 	return Constraint[F, E]{handle, context, exprs, bitwidths}

pkg/schema/constraint/vanishing/constraint.go

@@ -47,7 +47,7 @@ type Constraint[F field.Element[F], T term.Testable[F]] struct {
 	Constraint T
 }
 
-// NewConstraint constructs a new vanishing constraint!
+// NewConstraint constructs a new vanishing constraint
 func NewConstraint[F field.Element[F], T term.Testable[F]](handle string, context schema.ModuleId,
 	domain util.Option[int], constraint T) Constraint[F, T] {
 	return Constraint[F, T]{handle, context, domain, constraint}

pkg/test/zkc_unit_test.go

@@ -20,6 +20,10 @@ import (
 	"github.com/consensys/go-corset/pkg/zkc/vm"
 )
 
+func Test_ZkcUnit_Example(t *testing.T) {
+	checkZkcUnit(t, "zkc/unit/_example", util.DEFAULT_CONFIG)
+}
+
 // ===================================================================
 // Basic Tests
 // ===================================================================

pkg/zkc/compiler/ast/decl/decl.go

@@ -25,8 +25,12 @@ type Resolved = Declaration[symbol.Resolved]
 // reference to an external component (e.g. function, RAM, ROM, etc).
 type Unresolved = Declaration[symbol.Unresolved]
 
-// Declaration represents something declared within a source file, such as a
-// function or constant, etc.
+// Declaration represents something declared within a source file, in particular
+// - includes
+// - constants
+// - input / output / memory / static "memories"
+// - functions
+// - type aliases
 type Declaration[S any] interface {
 	// Arity returns the number of inputs/outputs for this declaration.
 	Arity() (inputs uint, outputs uint)

pkg/zkc/compiler/codegen/statement.go

@@ -83,7 +83,8 @@ func (p *StmtCompiler) compileStatement(pc uint, mapping []uint, s Stmt) VectorI
 //
 // > struct tmp { x u32, y u32 }
 // > ...
-// > var t tmp > tmp = f(...)
+// > var t tmp
+// > tmp = f(...)
 //
 // In this case, we want to "compile out" the struct, so we end up with this:
 //

pkg/zkc/compiler/parser/environment.go

@@ -50,76 +50,76 @@ func EmptyEnvironment() Environment {
 // Clone constructs a clone of this environment, such that variables declared in
 // the clone will not clash with those declared elsewhere.  The inLoop parameter
 // indicates whether the cloned environment is inside a loop.
-func (p *Environment) Clone(inLoop bool) Environment {
+func (env *Environment) Clone(inLoop bool) Environment {
 	var local localEnvironment
 	// Clone local variables
-	local.visible = p.local.visible.Clone()
+	local.visible = env.local.visible.Clone()
 	local.inLoop = inLoop
 	// Otherwise, keep global as is
-	return Environment{global: p.global, local: &local}
+	return Environment{global: env.global, local: &local}
 }
 
 // InLoop returns whether the current environment is inside a loop body.
-func (p *Environment) InLoop() bool {
-	return p.local.inLoop
+func (env *Environment) InLoop() bool {
+	return env.local.inLoop
 }
 
 // Effects returns the set of memory effects declared globally
-func (p *Environment) Effects() []*symbol.Unresolved {
-	return p.global.effects
+func (env *Environment) Effects() []*symbol.Unresolved {
+	return env.global.effects
 }
 
 // Variables returns the set of variables declared globally
-func (p *Environment) Variables() []VariableDescriptor {
-	return p.global.variables
+func (env *Environment) Variables() []VariableDescriptor {
+	return env.global.variables
 }
 
 // DeclareEffect declares a new effect.  If an effect with the same name
 // already exists, this panics.
-func (p *Environment) DeclareEffect(effect *symbol.Unresolved) {
+func (env *Environment) DeclareEffect(effect *symbol.Unresolved) {
 	//
-	if p.IsDeclared(effect.Name) {
+	if env.IsDeclared(effect.Name) {
 		panic(fmt.Sprintf("effect %s already declared", effect.Name))
 	}
 	//
-	p.global.effects = append(p.global.effects, effect)
+	env.global.effects = append(env.global.effects, effect)
 }
 
 // DeclareVariable declares a new register with the given name and bitwidth.  If
 // a register with the same name already exists, this panics.
-func (p *Environment) DeclareVariable(kind variable.Kind, name string, datatype Type) {
+func (env *Environment) DeclareVariable(kind variable.Kind, name string, datatype Type) {
 	// Determine global index of this variable
-	var index = uint(len(p.global.variables))
+	var index = uint(len(env.global.variables))
 	// Check whether it clashes with another variable in the same (local) environment
-	if p.IsDeclared(name) {
+	if env.IsDeclared(name) {
 		panic(fmt.Sprintf("variable %s already declared", name))
 	}
 	// Update global environment
-	p.global.variables = append(p.global.variables, variable.New(kind, name, datatype))
+	env.global.variables = append(env.global.variables, variable.New(kind, name, datatype))
 	// Update local environment
-	p.local.visible.Insert(index)
+	env.local.visible.Insert(index)
 }
 
 // IsDeclared checks whether or not a given name is already declared (either as
 // an effect or a variable).
-func (p *Environment) IsDeclared(name string) bool {
+func (env *Environment) IsDeclared(name string) bool {
 	// check effects
-	for _, effect := range p.global.effects {
+	for _, effect := range env.global.effects {
 		if effect.Name == name {
 			return true
 		}
 	}
 	// check local variables
-	return p.IsDeclaredVariable(name)
+	return env.IsDeclaredVariable(name)
 }
 
 // IsDeclaredVariable checks whether or not a given name is already declared as
 // a variable.
-func (p *Environment) IsDeclaredVariable(name string) bool {
+func (env *Environment) IsDeclaredVariable(name string) bool {
 	// check local variables
-	for iter := p.local.visible.Iter(); iter.HasNext(); {
+	for iter := env.local.visible.Iter(); iter.HasNext(); {
 		var index = iter.Next()
-		if p.global.variables[index].Name == name {
+		if env.global.variables[index].Name == name {
 			return true
 		}
 	}
@@ -128,11 +128,11 @@ func (p *Environment) IsDeclaredVariable(name string) bool {
 }
 
 // LookupVariable looks up the index for a given register.
-func (p *Environment) LookupVariable(name string) variable.Id {
+func (env *Environment) LookupVariable(name string) variable.Id {
 	// check local variables
-	for iter := p.local.visible.Iter(); iter.HasNext(); {
+	for iter := env.local.visible.Iter(); iter.HasNext(); {
 		var index = iter.Next()
-		if p.global.variables[index].Name == name {
+		if env.global.variables[index].Name == name {
 			return index
 		}
 	}

pkg/zkc/constraints/translator.go

@@ -92,43 +92,144 @@ func translateStaticMemory[F field.Element[F]](_ schema.ModuleId, m vm.InputOutp
 	return mod
 }
 
-func translateReadOnlyMemory[F field.Element[F]](_ schema.ModuleId, fm vm.InputOutputMemory[F]) mir.Module[F] {
+func translateReadOnlyMemory[F field.Element[F]](
+	ctx schema.ModuleId, fm vm.InputOutputMemory[F]) mir.Module[F] {
+	var name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
+	return translateMemoryCommon(ctx, fm, name)
+}
+
+// Write once memory and read only memory are equivalent on the constraints level
+func translateWriteOnceMemory[F field.Element[F]](
+	ctx schema.ModuleId, fm vm.InputOutputMemory[F]) mir.Module[F] {
+	var name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
+	return translateMemoryCommon(ctx, fm, name)
+}
+
+func translateReadWriteMemory[F field.Element[F]](
+	ctx schema.ModuleId, fm vm.Memory[F]) mir.Module[F] {
+	var name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
+	return translateMemoryCommon(ctx, fm, name)
+}
+
+func translateMemoryCommon[F field.Element[F]](
+	ctx schema.ModuleId, fm vm.Memory[F], name trace.ModuleName) mir.Module[F] {
 	var (
-		mod  *schema.Table[F, mir.Constraint[F]]
-		name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
+		memoryModule   *schema.Table[F, mir.Constraint[F]]
+		padding        big.Int
+		timestampWidth = uint(32)
 	)
-	// Initialise module
-	mod = mod.Init(name, false, true, false, fm.IsNative(), false, 0)
-	// Add all registers
-	mod.AddRegisters(fm.Registers()...)
-	// TODO: implement ROM constraints
-	return mod
-}
 
-func translateWriteOnceMemory[F field.Element[F]](_ schema.ModuleId, fm vm.InputOutputMemory[F]) mir.Module[F] {
+	// Initialise module and add all registers
+	memoryModule = memoryModule.Init(name, false, true, false, fm.IsNative(), false, 0)
+	memoryModule.AddRegisters(fm.Registers()...)
+
 	var (
-		mod  *schema.Table[F, mir.Constraint[F]]
-		name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
+		timestampRead    = register.NewId(memoryModule.Width() + 0)
+		timestampWritten = register.NewId(memoryModule.Width() + 1)
+		timestampDelta   = register.NewId(memoryModule.Width() + 2)
 	)
-	// Initialise module
-	mod = mod.Init(name, false, true, false, fm.IsNative(), false, 0)
-	// Add all registers
-	mod.AddRegisters(fm.Registers()...)
-	// TODO: implement WOM constraints
-	return mod
-}
 
-func translateReadWriteMemory[F field.Element[F]](_ schema.ModuleId, fm vm.Memory[F]) mir.Module[F] {
+	memoryModule.AddRegisters(register.NewComputed("timestamp_read", timestampWidth, padding))
+	memoryModule.AddRegisters(register.NewComputed("timestamp_write", timestampWidth, padding))
+	memoryModule.AddRegisters(register.NewComputed("timestamp_delta", timestampWidth, padding))
+
 	var (
-		mod  *schema.Table[F, mir.Constraint[F]]
-		name = trace.ModuleName{Name: fm.Name(), Multiplier: 1}
+		addressWidth uint
+		valueWidth   uint
 	)
-	// Initialise module
-	mod = mod.Init(name, false, true, false, fm.IsNative(), false, 0)
-	// Add all registers
-	mod.AddRegisters(fm.Registers()...)
-	// TODO: implement WOM constraints
-	return mod
+
+	for i, l := range fm.Registers() {
+		if uint(i) < fm.Geometry().AddressLines() {
+			addressWidth += l.Width()
+		} else if uint(i) < fm.Geometry().AddressLines()+fm.Geometry().DataLines() {
+			valueWidth += l.Width()
+		}
+	}
+
+	// var address = register.NewId(memoryModule.Width() + 0)
+	// var valueRead   = register.NewId(memoryModule.Width() + 1)
+	memoryModule.AddRegisters(register.NewComputed("address", addressWidth, padding))
+	memoryModule.AddRegisters(register.NewComputed("valueRead", valueWidth, padding))
+
+	var (
+		execPhase = register.NewId(memoryModule.Width() + 0)
+		finlPhase = register.NewId(memoryModule.Width() + 1)
+	)
+
+	memoryModule.AddRegisters(register.NewComputed("exec", 1, padding))
+	memoryModule.AddRegisters(register.NewComputed("finl", 1, padding))
+
+	var (
+		rTime = mirc.Variable[register.Id, Expr[F]](timestampRead, timestampWidth, 0)
+		wTime = mirc.Variable[register.Id, Expr[F]](timestampWritten, timestampWidth, 0)
+		dTime = mirc.Variable[register.Id, Expr[F]](timestampDelta, timestampWidth, 0)
+		// addr     = mirc.Variable[register.Id, Expr[F]](address,           addressWidth,   0)
+		// val      = mirc.Variable[register.Id, Expr[F]](value,             valueWidth,     0)
+		execPrev = mirc.Variable[register.Id, Expr[F]](execPhase, 1, -1)
+		finlPrev = mirc.Variable[register.Id, Expr[F]](finlPhase, 1, -1)
+		exec     = mirc.Variable[register.Id, Expr[F]](execPhase, 1, 0)
+		finl     = mirc.Variable[register.Id, Expr[F]](finlPhase, 1, 0)
+		zero     = mirc.Number[register.Id, Expr[F]](0)
+		one      = mirc.Number[register.Id, Expr[F]](1)
+	)
+
+	// ================================================
+	// constraints
+	// ================================================
+
+	// (non padding) rows are either created during standard execution (exec ≡ true)
+	// or during the finalization phase (finl ≡ true)
+	flagExclusivity := mir.NewVanishingConstraint("flag_exclusivity", ctx, util.None[int](),
+		mirc.Product([]Expr[F]{exec, finl}).Equals(zero).AsLogical())
+
+	// both exec and (exec + finl) should, on any trace segment, look like one of these :
+	//
+	//  ¹ ┼       ┌─────         ¹ ┼
+	//    │       │                │
+	//  ⁰ ┴  ─────┘        or    ⁰ ┴  ───────────
+	//
+	// exec may not be nondecreasing; the (exec, finl) pair may look like so :
+	//
+	//  ¹ ┼       ┌─────┐∙∙∙∙∙∙   ( ∙ ≡ finl)
+	//    │       │     │
+	//  ⁰ ┴  ─────┘∙∙∙∙∙└──────   ( ─ ≡ exec)
+	flagMonotony1 := mir.NewVanishingConstraint("finl_monotony", ctx, util.None[int](),
+		mirc.If(finlPrev.NotEquals(zero), finl.Equals(one)).AsLogical())
+	flagMonotony2 := mir.NewVanishingConstraint("exec+finl_monotony", ctx, util.None[int](),
+		mirc.If(mirc.Sum([]Expr[F]{execPrev, finlPrev}).NotEquals(zero),
+			mirc.Sum([]Expr[F]{exec, finl}).Equals(one)).AsLogical())
+
+	// we want to prove WT - RT = 1 + ΔT (which forces WT > RT given that ΔT is ≥ 0)
+	// instead we prove WT = RT + 1 + ΔT
+	timestampMonotony := mir.NewVanishingConstraint("timestamp_monotony", ctx, util.None[int](),
+		mirc.If(exec.NotEquals(zero), wTime.Equals(rTime.Add(dTime, one))).AsLogical())
+
+	// var isImmutable bool
+	// switch fm.(type) {
+	// case vm.InputOutputMemory[F]: isImmutable = true
+	// case vm.Memory[F]: isImmutable = false
+	// default: panic("unknown memory type")
+	// }
+	//
+	// var valueWritten = register.Id
+	// if isImmutable {
+	// 	valueWritten = valueRead
+	// } else {
+	// 	valueWritten   = register.NewId(memoryModule.Width() + 0)
+	// 	memoryModule.AddRegisters(register.NewComputed("valueWritten", valueWidth, padding))
+	// }
+	//
+	// // we impose value constancy by enforcing that the received value be the same as the sent value
+	// rcvExec := mir.NewReceiveConstraint[F]("reading_in_execution_phase",
+	// []register.Id{address, timestampRead, valueRead})
+	// sndExec := mir.NewSendConstraint[F]("writing_in_execution_phase",
+	// []register.Id{address, timestampWritten, valueWritten})
+
+	constraints := []mir.Constraint[F]{flagExclusivity, flagMonotony1,
+		flagMonotony2, timestampMonotony} // , rcvExec, sndExec}
+	memoryModule.AddConstraints(constraints...)
+
+	return memoryModule
 }
 
 func translateFunction[F field.Element[F]](ctx schema.ModuleId, fm vm.FieldFunction) mir.Module[F] {