From ea6b692c29ce462fe019d05aea525c701d253df0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 26 May 2026 15:37:01 +0200 Subject: [PATCH 1/7] wip MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Olivier Bégassat --- pkg/ir/hir/constraint.go | 2 +- pkg/ir/mir/constraint.go | 16 ++- pkg/schema/constraint/ranged/constraint.go | 2 +- pkg/schema/constraint/vanishing/constraint.go | 2 +- pkg/test/zkc_unit_test.go | 4 + pkg/zkc/compiler/ast/decl/decl.go | 8 +- pkg/zkc/compiler/codegen/statement.go | 3 +- pkg/zkc/constraints/translator.go | 90 +++++++++++- ram.md | 134 ++++++++++++++++++ rom.md | 94 ++++++++++++ testdata/zkc/unit/_example.accepts | 1 + testdata/zkc/unit/_example.zkc | 15 ++ testdata/zkc/unit/_example_0.zkc | 23 +++ wom.md | 112 +++++++++++++++ 14 files changed, 493 insertions(+), 13 deletions(-) create mode 100644 ram.md create mode 100644 rom.md create mode 100644 testdata/zkc/unit/_example.accepts create mode 100644 testdata/zkc/unit/_example.zkc create mode 100644 testdata/zkc/unit/_example_0.zkc create mode 100644 wom.md diff --git a/pkg/ir/hir/constraint.go b/pkg/ir/hir/constraint.go index 95b665887..9f29996d9 100644 --- a/pkg/ir/hir/constraint.go +++ b/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 { // diff --git a/pkg/ir/mir/constraint.go b/pkg/ir/mir/constraint.go index 2a34b665a..f8539372b 100644 --- a/pkg/ir/mir/constraint.go +++ b/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] { // diff --git a/pkg/schema/constraint/ranged/constraint.go b/pkg/schema/constraint/ranged/constraint.go index 65dcb48d9..231679bde 100644 --- a/pkg/schema/constraint/ranged/constraint.go +++ b/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} diff --git a/pkg/schema/constraint/vanishing/constraint.go b/pkg/schema/constraint/vanishing/constraint.go index 00b170742..9d2c68abe 100644 --- a/pkg/schema/constraint/vanishing/constraint.go +++ b/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} diff --git a/pkg/test/zkc_unit_test.go b/pkg/test/zkc_unit_test.go index d568311b7..4e3f1d0e9 100644 --- a/pkg/test/zkc_unit_test.go +++ b/pkg/test/zkc_unit_test.go @@ -18,6 +18,10 @@ import ( "github.com/consensys/go-corset/pkg/test/util" ) +func Test_ZkcUnit_Example(t *testing.T) { + checkZkcUnit(t, "zkc/unit/_example", util.DEFAULT_CONFIG) +} + // =================================================================== // Basic Tests // =================================================================== diff --git a/pkg/zkc/compiler/ast/decl/decl.go b/pkg/zkc/compiler/ast/decl/decl.go index d70835b46..0374cbdcd 100644 --- a/pkg/zkc/compiler/ast/decl/decl.go +++ b/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) diff --git a/pkg/zkc/compiler/codegen/statement.go b/pkg/zkc/compiler/codegen/statement.go index 0053fb936..dba1425bb 100644 --- a/pkg/zkc/compiler/codegen/statement.go +++ b/pkg/zkc/compiler/codegen/statement.go @@ -77,7 +77,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: // diff --git a/pkg/zkc/constraints/translator.go b/pkg/zkc/constraints/translator.go index bdd8c08f0..01ea9e7bd 100644 --- a/pkg/zkc/constraints/translator.go +++ b/pkg/zkc/constraints/translator.go @@ -92,17 +92,95 @@ 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 ( - mod *schema.Table[F, mir.Constraint[F]] - name = trace.ModuleName{Name: fm.Name(), Multiplier: 1} + romModule *schema.Table[F, mir.Constraint[F]] + name = trace.ModuleName{Name: fm.Name(), Multiplier: 1} + padding big.Int + timestampWidth = uint(32) ) + // Initialise module - mod = mod.Init(name, false, true, false, fm.IsNative(), false, 0) + romModule = romModule.Init(name, false, true, false, fm.IsNative(), false, 0) // Add all registers - mod.AddRegisters(fm.Registers()...) + romModule.AddRegisters(fm.Registers()...) + + // mod.AddRegisters(register.NewComputed(io.PC_NAME, pcWidth, padding)) + var ( + timestampRead = register.NewId(romModule.Width() + 0) + timestampWritten = register.NewId(romModule.Width() + 1) + timestampDelta = register.NewId(romModule.Width() + 2) + ) + + romModule.AddRegisters(register.NewComputed("timestamp_read", timestampWidth, padding)) + romModule.AddRegisters(register.NewComputed("timestamp_write", timestampWidth, padding)) + romModule.AddRegisters(register.NewComputed("timestamp_delta", timestampWidth, padding)) + + var ( + addressWidth uint + valueWidth uint + ) + + for i, l := range fm.Registers() { + if uint(i) < fm.Geometry().AddressLines() { + addressWidth += l.Width() + } else { + valueWidth += l.Width() + } + } + + // var address = register.NewId(romModule.Width() + 0) + // var value = register.NewId(romModule.Width() + 1) + romModule.AddRegisters(register.NewComputed("address", addressWidth, padding)) + romModule.AddRegisters(register.NewComputed("value", valueWidth, padding)) + + var ( + executionPhase = register.NewId(romModule.Width() + 0) + finalizationPhase = register.NewId(romModule.Width() + 1) + ) + + romModule.AddRegisters(register.NewComputed("exec", 1, padding)) + romModule.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]](executionPhase, 1, -1) + finlPrev = mirc.Variable[register.Id, Expr[F]](finalizationPhase, 1, -1) + exec = mirc.Variable[register.Id, Expr[F]](executionPhase, 1, 0) + finl = mirc.Variable[register.Id, Expr[F]](finalizationPhase, 1, 0) + zero = mirc.Number[register.Id, Expr[F]](0) + one = mirc.Number[register.Id, Expr[F]](1) + ) + + // constraints + flagExclusivity := mir.NewVanishingConstraint("flag_exclusivity", ctx, util.None[int](), + mirc.Product([]Expr[F]{exec, finl}).Equals(zero).AsLogical()) + 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()) + // rcvExec := mir.NewReceiveConstraint[F]("reading_in_execution_phase", + // []register.Id{address, timestampRead, value}) + // sndExec := mir.NewSendConstraint[F]("writing_in_execution_phase", + // []register.Id{address, timestampWritten, value}) + // first := mir.NewVanishingConstraint("first", ctx, util.Some(0), + // mirc.If(pc_i.NotEquals(zero), pc_i.Equals(one)).AsLogical()) + // + constraints := []mir.Constraint[F]{flagExclusivity, flagMonotony1, + flagMonotony2, timestampMonotony} // , rcvExec, sndExec} + romModule.AddConstraints(constraints...) + // TODO: implement ROM constraints - return mod + return romModule } func translateWriteOnceMemory[F field.Element[F]](_ schema.ModuleId, fm vm.InputOutputMemory[F]) mir.Module[F] { diff --git a/ram.md b/ram.md new file mode 100644 index 000000000..e91322989 --- /dev/null +++ b/ram.md @@ -0,0 +1,134 @@ +## RAM module + +Here's one set of constraints for a random access memory (RAM) module. We make the following assumptions: + +- the RAM may be read from arbitrarily +- before an address has been written to for the first time it holds the value 0 +- we must guarantee consistency across segments + +### Triggering the finalization phase + +To avoid ROM, WOM, and RAM all share the same issue wrt the logUpBus: if initialization/finalization isn't tightly constrained a memory cell can end up living many parallel lives. One constraint that removes this issue is to impose that these memory-types perform a single initialiazation/finalization event per address. Here's one way of doing this in our RISCV zkVM/zkc interpreter: + +```rust +// We interpret pc == MAX_UINT_64 as the stop signal, which is set by the ecall instruction +while pc != MAX_UINT_64 { + instruction = read_32(pc) as Instruction + pc = interpreter(instruction, pc) +} + +// executed at program end +if pc == MAX_UINT_64 { + // finaliztion of ROM's + finalize(rom_1) + finalize(rom_2) + ... + finalize(rom_m) + + // finalization of WOM's + finalize(wom_1) + finalize(wom_2) + ... + finalize(wom_n) + + // finalization of RAM + finalize(ram) +} else { + // should be unreachable ... + fail "Invalid final program counter %x", pc +} +``` + +```rust +// columns of RAM +EXEC +FINL +ADDRESS +TIMESTAMP_READ +TIMESTAMP_WRITTEN +VALUE_READ +VALUE_WRITTEN +IS_WRITE +``` + +and one will impose + +```rust +// binary columns +EXEC +FINL +IS_WRITE +EXEC + FINL + +// monotonous expressions (nondecreasing expressions) +FINL +EXEC + FINL +``` + +Furthermore one wants + +### The "constrain the full range output range" case + +Note. The "constrain the nontrivial part of the output range" alternative has issues if the output is empty. + +```rust +if EXEC = true then + // timestamp comparisons are only meaningful if associated + // to actual reads / writes in the execution phase + TIMESTAMP_READ < TIMESTAMP_WRITTEN + + // value read and value written behave as expected + TIMESTAMP_READ, VALUE_READ = hint(ram, ADDRESS) + rcv( ADDRESS, TIMESTAMP_READ, VALUE_READ ) + snd( ADDRESS, TIMESTAMP_WRITTEN, VALUE_WRITTEN ) + + if IS_WRITE = false then + VALUE_READ = VALUE_WRITTEN + +// the finalization phase does both initializations and finalizations +if FINL = true then + // address starts at 0 and increments by 1 + if prev FINL = false then + ADDRESS = 0 + if prev FINL = true then + ADDRESS = 1 + prev(ADDRESS) + + // initialization and finalization + TIMESTAMP_READ, VALUE_READ = hint(ram, ADDRESS) + snd( ADDRESS, 0, 0 ) // init + rcv( ADDRESS, TIMESTAMP_READ, VALUE_READ ) // finl +``` + +where + +```rust +rcv( address, timestamp, value ) +snd( address, timestamp, value ) +``` + +Any zkc module `MOD` that allows one to touch the WOM requires the following columns + +```rust +WOM_TRIGGER +WOM_ADDRESS +WOM_TIMESTAMP_WRITTEN +WOM_IS_WRITE +WOM_VALUE +``` + +and we require bilateral conditional lookups + +| MOD | WOM | Notes | +| --------------- | ------------------- | ----------- | +| RAM_TRIGGER | EXEC | condition | +| --------------- | ------------------- | ----------- | +| RAM_ADDRESS | ADDRESS | | +| RAM_TIMESTAMP | TIMESTAMP_WRITTEN | | +| RAM_IS_WRITE | IS_WRITE | | +| RAM_VALUE | VALUE_WRITTEN | | + +### Lanes + +There is an issue wrt _input lanes_: if the `ADDRESS` is a tuple then you need some canonical way to enumerate/list its items. Under the hood one can imagine that all components would still end up being `uX`'s for some `X`. The `VALUES_XXX` are tuples there shouldn't be much of an issue conceptually. + +There is the question of emptyness: what to do if we have a "you only pay the initialization / finalization prize for those cells that you touched approach" and no operations were done in the various ROM/WOM/RAM's ? One simple approach to this would be to force a single interaction with every memory component. diff --git a/rom.md b/rom.md new file mode 100644 index 000000000..a0f6461e6 --- /dev/null +++ b/rom.md @@ -0,0 +1,94 @@ +## ROM module + +Here's one set of constraints for a write-once-memory (ROM) module. We make the following assumptions: + +- a ROM is an immutable table: reads always return the same value across the full lifetime of the execution + +### Triggering the finalization phase + +To avoid ROM living parallel lives, there should be a single ROM finalization event. +This will force a single initialization event and a single timeline for a given address in the ROM. + +```rust +// columns of a ROM +EXEC +FINL +ADDRESS // a multitude of columns, potentially +VALUE // a multitude of columns, potentially +TIMESTAMP_READ +TIMESTAMP_WRITTEN +``` + +and one will impose + +```rust +// binary columns +EXEC +FINL +EXEC + FINL // EXEC ∙ FINL ≡ 0 + +// monotonous expressions (nondecreasing expressions) +FINL +EXEC + FINL +``` + +Furthermore one wants + +### The "constrain the full range output range" case + +Note. The "constrain the nontrivial part of the output range" alternative has issues if the output is empty. + +```rust +if EXEC = true then + // timestamp comparisons are only meaningful if associated + // to actual reads / writes in the execution phase + TIMESTAMP_READ < TIMESTAMP_WRITTEN + + // bus interactions + // this ROM address may have already been touched, but it wasn't written to yet + // this ROM address was previously written to + rcv( ADDRESS, TIMESTAMP_READ, VALUE ) + snd( ADDRESS, TIMESTAMP_WRITTEN, VALUE ) + +// the finalization phase does both initializations and finalizations +if FINL = true then + // below we assume for simplicity that addresses are described by a single int + // address starts at 0 and increments by 1 + if prev FINL = false then + ADDRESS = 0 + if prev FINL = true then + ADDRESS = 1 + prev(ADDRESS) + + // bus interactions + if WAS_ALREADY_WRITTEN_TO = true then + // address of ROM was written to at some point + snd( ADDRESS, 0, VALUE ) // initialization + rcv( ADDRESS, TIMESTAMP_READ, VALUE ) // finalization +``` + +where + +```rust +rcv( address, timestamp, is_written, value ) +snd( address, timestamp, is_written, value ) +``` + +Any zkc module `MOD` that allows one to touch the ROM requires the following columns + +```rust +ROM_TRIGGER +ROM_ADDRESS +ROM_TIMESTAMP_WRITTEN +ROM_IS_WRITE +ROM_VALUE +``` + +and we require bilateral conditional lookups + +| MOD | ROM | Notes | +| ------------- | --------- | --------- | +| ROM_TRIGGER | EXEC | condition | +| ROM_ADDRESS | ADDRESS | | +| ROM_TIMESTAMP | TIMESTAMP | | +| ROM_IS_WRITE | IS_WRITE | | +| ROM_VALUE | VALUE | | diff --git a/testdata/zkc/unit/_example.accepts b/testdata/zkc/unit/_example.accepts new file mode 100644 index 000000000..eafd4c77b --- /dev/null +++ b/testdata/zkc/unit/_example.accepts @@ -0,0 +1 @@ +{ "ROM": "0xf_1_0_4" } diff --git a/testdata/zkc/unit/_example.zkc b/testdata/zkc/unit/_example.zkc new file mode 100644 index 000000000..9b4ec3f78 --- /dev/null +++ b/testdata/zkc/unit/_example.zkc @@ -0,0 +1,15 @@ +memory RAM(address :u4) -> (value :u4) + +fn main() { + var r :u4 + RAM[1] = f(7) +} + +fn f(x:u4) -> (r:u4) { + + r = x + RAM[0] + if r == 12 { + r = r + 1 + } + return +} diff --git a/testdata/zkc/unit/_example_0.zkc b/testdata/zkc/unit/_example_0.zkc new file mode 100644 index 000000000..0bfe04c43 --- /dev/null +++ b/testdata/zkc/unit/_example_0.zkc @@ -0,0 +1,23 @@ +memory RAM(address :u4) -> (value :u4) +input ROM(address :u4, bis :u8) -> (value :u4) +output WOM(address :u4) -> (value :u4) + +fn main() { + var r :u4 + r = f(7) + + // WOM[0] = ROM[0, 0] + // + // if ROM[1,1] != 0xf { fail } +} + +fn f(x:u4) -> (r:u4) { + + r = x + RAM[0] + if r == 12 { + r = r + 1 + // } else { + // r = r + 3 + } + return +} diff --git a/wom.md b/wom.md new file mode 100644 index 000000000..6654793aa --- /dev/null +++ b/wom.md @@ -0,0 +1,112 @@ +## WOM module + +Here's one set of constraints for a write-once-memory (WOM) module. We make the following assumptions: + +- the WOM may be read from arbitrarily: before it's been written to reads should return 0 +- multiple writes at a given address are allowed unless they overwrite a previously written value + +By definition in a WOM, once a memory cell with address `a` has been written to, the value in memory may never change from here on out: every subsequent read, including the finalization read, returns that value. A WOM module will have the following columns. + +### Triggering the finalization phase + +To avoid WOM living parallel lives, there should be a single WOM finalization event. This will force a single initialization event and a single timeline for a given address in the WOM. + +```rust +// columns of a WOM +EXEC +FINL +ADDRESS +TIMESTAMP_READ +TIMESTAMP_WRITTEN +VALUE +WAS_ALREADY_WRITTEN_TO +IS_WRITE +``` + +and one will impose + +```rust +// binary columns +EXEC +FINL +WAS_ALREADY_WRITTEN_TO +IS_WRITE +EXEC + FINL + +// monotonous expressions (nondecreasing expressions) +FINL +EXEC + FINL +``` + +Furthermore one wants + +### The "constrain the full range output range" case + +Note. The "constrain the nontrivial part of the output range" alternative has issues if the output is empty. + +```rust +if EXEC = true then + // timestamp comparisons are only meaningful if associated + // to actual reads / writes in the execution phase + TIMESTAMP_READ < TIMESTAMP_WRITTEN + + // bus interactions + // this WOM address may have already been touched, but it wasn't written to yet + if WAS_ALREADY_WRITTEN_TO = false then + rcv( ADDRESS, TIMESTAMP_READ, false, 0 ) + snd( ADDRESS, TIMESTAMP_WRITTEN, IS_WRITE, VALUE ) + if IS_WRITE = false then VALUE = 0 + + // this WOM address was previously written to + if WAS_ALREADY_WRITTEN_TO = true then + rcv( ADDRESS, TIMESTAMP_READ, true, VALUE ) + snd( ADDRESS, TIMESTAMP_WRITTEN, true, VALUE ) + +// the finalization phase does both initializations and finalizations +if FINL = true then + // address starts at 0 and increments by 1 + if prev FINL = false then + ADDRESS = 0 + if prev FINL = true then + ADDRESS = 1 + prev(ADDRESS) + + // no writes take place in the finalization phase + IS_WRITE = false + + // bus interactions + if WAS_ALREADY_WRITTEN_TO = false then + // address of WOM was never written to + snd( ADDRESS, 0, false, 0 ) // initialization + rcv( ADDRESS, TIMESTAMP_READ, false, 0 ) // finalization + if WAS_ALREADY_WRITTEN_TO = true then + // address of WOM was written to at some point + snd( ADDRESS, 0, false, 0 ) // initialization + rcv( ADDRESS, TIMESTAMP_READ, true, VALUE ) // finalization +``` + +where + +```rust +rcv( address, timestamp, is_written, value ) +snd( address, timestamp, is_written, value ) +``` + +Any zkc module `MOD` that allows one to touch the WOM requires the following columns + +```rust +WOM_TRIGGER +WOM_ADDRESS +WOM_TIMESTAMP_WRITTEN +WOM_IS_WRITE +WOM_VALUE +``` + +and we require bilateral conditional lookups + +| MOD | WOM | Notes | +| ------------- | --------- | --------- | +| WOM_TRIGGER | EXEC | condition | +| WOM_ADDRESS | ADDRESS | | +| WOM_TIMESTAMP | TIMESTAMP | | +| WOM_IS_WRITE | IS_WRITE | | +| WOM_VALUE | VALUE | | From 6671d632359bdd7cd5d7893cb499be76337afd38 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 2 Jun 2026 11:02:33 +0200 Subject: [PATCH 2/7] ras MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Olivier Bégassat --- testdata/zkc/unit/_example_0.zkc | 1 + 1 file changed, 1 insertion(+) diff --git a/testdata/zkc/unit/_example_0.zkc b/testdata/zkc/unit/_example_0.zkc index 0bfe04c43..8c4054ee6 100644 --- a/testdata/zkc/unit/_example_0.zkc +++ b/testdata/zkc/unit/_example_0.zkc @@ -5,6 +5,7 @@ output WOM(address :u4) -> (value :u4) fn main() { var r :u4 r = f(7) + WOM[0] = 12 // WOM[0] = ROM[0, 0] // From 3721199062ae805600fb86e89c62b51b74abafbc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 2 Jun 2026 23:16:52 +0200 Subject: [PATCH 3/7] feat: unified memory MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Olivier Bégassat --- pkg/zkc/constraints/translator.go | 145 +++++++++++++++++------------- 1 file changed, 84 insertions(+), 61 deletions(-) diff --git a/pkg/zkc/constraints/translator.go b/pkg/zkc/constraints/translator.go index 01ea9e7bd..5333fa3d4 100644 --- a/pkg/zkc/constraints/translator.go +++ b/pkg/zkc/constraints/translator.go @@ -92,29 +92,46 @@ func translateStaticMemory[F field.Element[F]](_ schema.ModuleId, m vm.InputOutp return mod } -func translateReadOnlyMemory[F field.Element[F]](ctx 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 ( - romModule *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 - romModule = romModule.Init(name, false, true, false, fm.IsNative(), false, 0) - // Add all registers - romModule.AddRegisters(fm.Registers()...) + // Initialise module and add all registers + memoryModule = memoryModule.Init(name, false, true, false, fm.IsNative(), false, 0) + memoryModule.AddRegisters(fm.Registers()...) - // mod.AddRegisters(register.NewComputed(io.PC_NAME, pcWidth, padding)) var ( - timestampRead = register.NewId(romModule.Width() + 0) - timestampWritten = register.NewId(romModule.Width() + 1) - timestampDelta = register.NewId(romModule.Width() + 2) + timestampRead = register.NewId(memoryModule.Width() + 0) + timestampWritten = register.NewId(memoryModule.Width() + 1) + timestampDelta = register.NewId(memoryModule.Width() + 2) ) - romModule.AddRegisters(register.NewComputed("timestamp_read", timestampWidth, padding)) - romModule.AddRegisters(register.NewComputed("timestamp_write", timestampWidth, padding)) - romModule.AddRegisters(register.NewComputed("timestamp_delta", timestampWidth, padding)) + 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 ( addressWidth uint @@ -124,23 +141,23 @@ func translateReadOnlyMemory[F field.Element[F]](ctx schema.ModuleId, fm vm.Inpu for i, l := range fm.Registers() { if uint(i) < fm.Geometry().AddressLines() { addressWidth += l.Width() - } else { + } else if uint(i) < fm.Geometry().AddressLines()+fm.Geometry().DataLines() { valueWidth += l.Width() } } - // var address = register.NewId(romModule.Width() + 0) - // var value = register.NewId(romModule.Width() + 1) - romModule.AddRegisters(register.NewComputed("address", addressWidth, padding)) - romModule.AddRegisters(register.NewComputed("value", valueWidth, padding)) + // 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 ( - executionPhase = register.NewId(romModule.Width() + 0) - finalizationPhase = register.NewId(romModule.Width() + 1) + execPhase = register.NewId(memoryModule.Width() + 0) + finlPhase = register.NewId(memoryModule.Width() + 1) ) - romModule.AddRegisters(register.NewComputed("exec", 1, padding)) - romModule.AddRegisters(register.NewComputed("finl", 1, padding)) + 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) @@ -148,65 +165,71 @@ func translateReadOnlyMemory[F field.Element[F]](ctx schema.ModuleId, fm vm.Inpu 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]](executionPhase, 1, -1) - finlPrev = mirc.Variable[register.Id, Expr[F]](finalizationPhase, 1, -1) - exec = mirc.Variable[register.Id, Expr[F]](executionPhase, 1, 0) - finl = mirc.Variable[register.Id, Expr[F]](finalizationPhase, 1, 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, value}) + // []register.Id{address, timestampRead, valueRead}) // sndExec := mir.NewSendConstraint[F]("writing_in_execution_phase", - // []register.Id{address, timestampWritten, value}) - // first := mir.NewVanishingConstraint("first", ctx, util.Some(0), - // mirc.If(pc_i.NotEquals(zero), pc_i.Equals(one)).AsLogical()) - // + // []register.Id{address, timestampWritten, valueWritten}) + constraints := []mir.Constraint[F]{flagExclusivity, flagMonotony1, flagMonotony2, timestampMonotony} // , rcvExec, sndExec} - romModule.AddConstraints(constraints...) + memoryModule.AddConstraints(constraints...) - // TODO: implement ROM constraints - return romModule -} - -func translateWriteOnceMemory[F field.Element[F]](_ schema.ModuleId, fm vm.InputOutputMemory[F]) mir.Module[F] { - var ( - mod *schema.Table[F, mir.Constraint[F]] - name = trace.ModuleName{Name: fm.Name(), Multiplier: 1} - ) - // 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] { - var ( - mod *schema.Table[F, mir.Constraint[F]] - name = trace.ModuleName{Name: fm.Name(), Multiplier: 1} - ) - // 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 + return memoryModule } func translateFunction[F field.Element[F]](ctx schema.ModuleId, fm vm.FieldFunction) mir.Module[F] { From c0cc3614e4bfc20d1aadf5a0cf9be90f79e47305 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 2 Jun 2026 23:17:30 +0200 Subject: [PATCH 4/7] ras: renaming of p to env in environment.go MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Olivier Bégassat --- pkg/zkc/compiler/parser/environment.go | 52 +++++++++++++------------- 1 file changed, 26 insertions(+), 26 deletions(-) diff --git a/pkg/zkc/compiler/parser/environment.go b/pkg/zkc/compiler/parser/environment.go index 4b946d284..0ad8704fe 100644 --- a/pkg/zkc/compiler/parser/environment.go +++ b/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 } } From d3c68ba7c62a718246e0ec7bc626e2cc4d8eea0c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 24 Jun 2026 01:31:03 +0200 Subject: [PATCH 5/7] ras --- rom (read once memory).md | 70 +++++++++++++++++++++++++++++ rom (read only memory).md | 94 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 164 insertions(+) create mode 100644 rom (read once memory).md create mode 100644 rom (read only memory).md diff --git a/rom (read once memory).md b/rom (read once memory).md new file mode 100644 index 000000000..568c3d8b6 --- /dev/null +++ b/rom (read once memory).md @@ -0,0 +1,70 @@ +# ROM (read ONCE memory) module + +Here's one set of constraints for a read-once-memory (ROM) module. +We make the following assumptions: + +- a ROM is an immutable table +- addresses are consecutive, start at 0 and there are no gaps +- the full contents of that memory will be read start to finish at one specific point in time +- the ROM is never read from again + +**Note.** The fact that this data is read **once** must be assured by the zkc program itself. +The ROM has no control over it. If the ROM were to enforce this we would have to add a source +time stamp column, that predicts the source module's time stamp. + +The reason for these assumptions are + +- they correspond to real use-cases + - ROM for sections from the compiled guest program + - ROM for inputs to the guest program + - both get loaded in full at the start of execution and are never touched again after that +- there is no need to ensure coherence over time and over segments since there will be a single read of any cell + +## ROM (once variant) vs WOM + +There will be no difference between the two + +## Constraints / columns side + +The entire thing can be arranged as a single lookup + +```rust +// columns of the source +ACCESS // determines padding (ACCESS ≡ 0) and non padding rows (ACCESS ≡ 1) +ADDRESS // a multitude of columns, potentially +VALUE // a multitude of columns, potentially + +// binary constraint +ACCESS +``` + +and one will impose + +```rust +ACCESS[0] = False +if ACCESS = False: + ADDRESS = 0 + +if ACCESS = True: + next( ACCESS ) = True + ADDRESS = 1 + prev( ADDRESS ) +``` + +## Requirements for sources adding to the bus + +Any zkc module `MOD` that may read a ROM requires the following columns + +```rust +ROM_ACCESS +ROM_ADDRESS +ROM_VALUE +``` + +and we require bilateral conditional lookups + +| MOD | ROM | Notes | +| ------------- | --------- | ----------- | +| ROM_ACCESS | ACCESS | condition | +| ------------- | --------- | ----------- | +| ROM_ADDRESS | ADDRESS | | +| ROM_VALUE | VALUE | | diff --git a/rom (read only memory).md b/rom (read only memory).md new file mode 100644 index 000000000..b7364ccc8 --- /dev/null +++ b/rom (read only memory).md @@ -0,0 +1,94 @@ +# ROM (read ONLY memory) module + +Here's one set of constraints for a write-once-memory (ROM) module. We make the following assumptions: + +- a ROM is an immutable table: reads always return the same value across the full lifetime of the execution + +### Triggering the finalization phase + +To avoid ROM living parallel lives, there should be a single ROM finalization event. +This will force a single initialization event and a single timeline for a given address in the ROM. + +```rust +// columns of a ROM +EXEC +FINL +ADDRESS // a multitude of columns, potentially +VALUE // a multitude of columns, potentially +TIMESTAMP_READ +TIMESTAMP_WRITTEN +``` + +and one will impose + +```rust +// binary columns +EXEC +FINL +EXEC + FINL // EXEC ∙ FINL ≡ 0 + +// monotonous expressions (nondecreasing expressions) +FINL +EXEC + FINL +``` + +Furthermore one wants + +### The "constrain the full range output range" case + +Note. The "constrain the nontrivial part of the output range" alternative has issues if the output is empty. + +```rust +if EXEC = true then + // timestamp comparisons are only meaningful if associated + // to actual reads / writes in the execution phase + TIMESTAMP_READ < TIMESTAMP_WRITTEN + + // bus interactions + // this ROM address may have already been touched, but it wasn't written to yet + // this ROM address was previously written to + rcv( ADDRESS, TIMESTAMP_READ, VALUE ) + snd( ADDRESS, TIMESTAMP_WRITTEN, VALUE ) + +// the finalization phase does both initializations and finalizations +if FINL = true then + // below we assume for simplicity that addresses are described by a single int + // address starts at 0 and increments by 1 + if prev FINL = false then + ADDRESS = 0 + if prev FINL = true then + ADDRESS = 1 + prev(ADDRESS) + + // bus interactions + if WAS_ALREADY_WRITTEN_TO = true then + // address of ROM was written to at some point + snd( ADDRESS, 0, VALUE ) // initialization + rcv( ADDRESS, TIMESTAMP_READ, VALUE ) // finalization +``` + +where + +```rust +rcv( address, timestamp, is_written, value ) +snd( address, timestamp, is_written, value ) +``` + +Any zkc module `MOD` that allows one to touch the ROM requires the following columns + +```rust +ROM_TRIGGER +ROM_ADDRESS +ROM_TIMESTAMP_WRITTEN +ROM_IS_WRITE +ROM_VALUE +``` + +and we require bilateral conditional lookups + +| MOD | ROM | Notes | +| ------------- | --------- | --------- | +| ROM_TRIGGER | EXEC | condition | +| ROM_ADDRESS | ADDRESS | | +| ROM_TIMESTAMP | TIMESTAMP | | +| ROM_IS_WRITE | IS_WRITE | | +| ROM_VALUE | VALUE | | From e587dd489dd5d8d32251a7867ad25762b624c73e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Wed, 24 Jun 2026 22:53:31 +0200 Subject: [PATCH 6/7] ras: documentation --- memory design space.md | 73 +++++++++++++++++++ ram.md | 147 ++++++++++++++++++++++---------------- rom (read once memory).md | 30 ++++---- rom (read only memory).md | 32 ++++----- rom.md | 94 ------------------------ wom.md | 66 ++++++++++------- 6 files changed, 233 insertions(+), 209 deletions(-) create mode 100644 memory design space.md delete mode 100644 rom.md diff --git a/memory design space.md b/memory design space.md new file mode 100644 index 000000000..814393e4e --- /dev/null +++ b/memory design space.md @@ -0,0 +1,73 @@ +# Memory design space + +Designing a memory module `m` requires at a minimum categorizing it along the following dimensions: + +- **ACCESS**: how do other modules communicate with it ? +- **COHERENCE**: is a coherence argument (i.e. memory consistency argument) required ? +- **MUTABILITY**: is that memory mutable or immutable ? +- **ADDRESS SPACE**: is data stored in a contiguous fashion or can it be sparse ? +- **SEGMENTATION**: is the memory accessible across several trace segments or not ? + +We provide constraints for memories below: + +## RAM: Random Access Memory + +- **ACCESS**: logUpBus based +- **COHERENCE**: logUpBus-based `Σ ≡ 0` coherence argument involving timestamps +- **MUTABILITY**: unrestricted reads and writes +- **ADDRESS SPACE**: sparse +- **SEGMENTATION**: multi-segment + +Use case: standard computer memory + +## AOM: Access Once Memory + +**AOM**'s provide an immutable memory that gets read start to finish in a single segment. + +**Note.** I suggest using **AOM** as a replacement for **ROM** / **WOM**: these two notions are functionally identical and differ, AFAICT, only in their intended use cases. Both are meant to hold immutable data that's avaiable from the start of tracing, and either seen as _providing_ inputs or _receiving_ output. In any case, they are functionally identical. + +- **ACCESS**: lookup based +- **COHERENCE**: none required +- **MUTABILITY**: immutable +- **ADDRESS SPACE**: contiguous +- **SEGMENTATION**: all accesses concentrated in one segment + +Use case: provide inputs or extract outputs in one go, +e.g. read `m` start to finish in one trace segment. + +## WOM: Write Once Memory + +**WOM**'s provide an initially empty memory where every cell may be read from and written to, but the initial write is definitive. + +- **ACCESS**: logUpBus based +- **COHERENCE**: logUpBus-based `Σ ≡ 0` coherence argument involving timestamps +- **MUTABILITY**: + - arbitrary reads + - first write sets value in stone (subsequent writes mustn't modify the current value) + - first write marks an address as `WAS_ALREADY_WRITTEN_TO` +- **ADDRESS SPACE**: contiguous +- **SEGMENTATION**: multi-segment + +Use case: extract definitive outputs that may be read by other processes + +- is `m` single access ? + - there are concrete cases (e.g. guest program ELF sections, guest program input) + - can it be assumed that the accesses land in a single trace segment ? if so one doesn't have to care about inter segment coherence +- is `m` + - immutable ? + - set once ? + - arbitrarily modifiable ? + - the answer to that question dictates whether one requires whether access must be tracked or not + - e.g. for WRITE ONCE MEMORY one should track +- is memory access confined to a single segment ? + - the answer to that question dictates whether + - memory consistency can be handled in module (and without permutation) or should be handled using a bus argument + - whether timestamps are required to order accesses or not +- does the memory permit writes ? + - if so, does it permit more than one write per address ? +- does the memory permit reads ? +- are accesses sequential and confined to a single segment or can they occur at any point in the execution ? + - one can talk of the ONE TIME ACCESS property +- are accesses sequential and confined to a single segment or can they occur at any point in the execution ? +- does the touched address space have gaps ? + - CONTIGUOUS memory allows potential initialization / finalization phases to increment addresses via `addr.next() = addr + 1` diff --git a/ram.md b/ram.md index e91322989..bcb11ef88 100644 --- a/ram.md +++ b/ram.md @@ -1,57 +1,75 @@ -## RAM module +# RAM module -Here's one set of constraints for a random access memory (RAM) module. We make the following assumptions: +We document the constraints for random access memory (RAM) modules. +We make the following assumptions: - the RAM may be read from arbitrarily - before an address has been written to for the first time it holds the value 0 -- we must guarantee consistency across segments - -### Triggering the finalization phase - -To avoid ROM, WOM, and RAM all share the same issue wrt the logUpBus: if initialization/finalization isn't tightly constrained a memory cell can end up living many parallel lives. One constraint that removes this issue is to impose that these memory-types perform a single initialiazation/finalization event per address. Here's one way of doing this in our RISCV zkVM/zkc interpreter: +- the RAM module must guarantee consistency across segments + +## Triggering the initialization/finalization phase `FINL ≡ true` + +If RAM initialization/finalization isn't tightly constrained a memory cell can +end up living parallel and wholly unrelated lives. One constraint that removes +this issue is to impose that these memory-types perform a single initialiazation +and finalization event per address. And here there are two options: go over a +contiguous chunk of addresses (with address increments of 1) or only initialize/ +finalize active addresses. The first option is valid when address space is small +and can be expected to be filled contiguously. RV's RAM isn't in that category +given the way the linker script allocates swathes of memory in the order of mega +bytes to the program itself, inputs and the stack ... The alternative and likely +most useful option is to only initialize/finalize active addresses, which requires +proving address monotony in the initialization/finalization phase. + +One option (to ensure unique init/finl) is to have the RISCV zkVM/zkc interpreter +make these init/finl calls itself at specific points in time, e.g. after the +program is done executing. For instance one could have ```rust -// We interpret pc == MAX_UINT_64 as the stop signal, which is set by the ecall instruction +// We interpret pc == MAX_UINT_64 as the stop signal while pc != MAX_UINT_64 { instruction = read_32(pc) as Instruction pc = interpreter(instruction, pc) } -// executed at program end +// Program execution has ended, perform finalization if pc == MAX_UINT_64 { - // finaliztion of ROM's - finalize(rom_1) - finalize(rom_2) - ... - finalize(rom_m) - - // finalization of WOM's - finalize(wom_1) - finalize(wom_2) - ... - finalize(wom_n) - // finalization of RAM - finalize(ram) + // would require passing ram's as arguments in one way or another + finalize(ram_1) + finalize(ram_2) + ... + finalize(ram_m) } else { // should be unreachable ... fail "Invalid final program counter %x", pc } ``` +## Ram module columns + ```rust // columns of RAM EXEC FINL -ADDRESS -TIMESTAMP_READ + +// slices of address columns +[]ADDRESS +[]ADDRESS_DELTA + +// slices of value columns +[]VALUE_READ +[]VALUE_WRITTEN + +// timestamp columns TIMESTAMP_WRITTEN -VALUE_READ -VALUE_WRITTEN +TIMESTAMP_READ +TIMESTAMP_DELTA + IS_WRITE ``` -and one will impose +## General constraints ```rust // binary columns @@ -65,70 +83,79 @@ FINL EXEC + FINL ``` -Furthermore one wants +We differentiate between memory accesses stemming from the execution of the +guest program (`EXEC ≡ true`) and memory accesses stemming from the init/finl +phase (`FINL ≡ true`). -### The "constrain the full range output range" case +## Execution phase constraints -Note. The "constrain the nontrivial part of the output range" alternative has issues if the output is empty. +We impose the following 'execution-phase' constraints: ```rust if EXEC = true then // timestamp comparisons are only meaningful if associated // to actual reads / writes in the execution phase TIMESTAMP_READ < TIMESTAMP_WRITTEN + // Note: the constraint will be enforced with a TIMESTAMP_DELTA column via + // TIMESTAMP_WRITTEN = TIMESTAMP_READ + 1 + TIMESTAMP_DELTA // value read and value written behave as expected - TIMESTAMP_READ, VALUE_READ = hint(ram, ADDRESS) - rcv( ADDRESS, TIMESTAMP_READ, VALUE_READ ) - snd( ADDRESS, TIMESTAMP_WRITTEN, VALUE_WRITTEN ) + TIMESTAMP_READ, []VALUE_READ = hint(ram, []ADDRESS) + rcv( []ADDRESS, []VALUE_READ, TIMESTAMP_READ, ) + snd( []ADDRESS, []VALUE_WRITTEN, TIMESTAMP_WRITTEN, ) if IS_WRITE = false then - VALUE_READ = VALUE_WRITTEN + []VALUE_READ = []VALUE_WRITTEN + +``` + +## Finalization phase constraints +We impose the following 'finalization-phase' constraints: + +```rust // the finalization phase does both initializations and finalizations if FINL = true then // address starts at 0 and increments by 1 if prev FINL = false then - ADDRESS = 0 + []ADDRESS = []0 if prev FINL = true then - ADDRESS = 1 + prev(ADDRESS) + // using []ADDRESS_DELTA + []ADDRESS > prev( []ADDRESS ) - // initialization and finalization - TIMESTAMP_READ, VALUE_READ = hint(ram, ADDRESS) - snd( ADDRESS, 0, 0 ) // init - rcv( ADDRESS, TIMESTAMP_READ, VALUE_READ ) // finl + // initialization and finalization + TIMESTAMP_READ, []VALUE_READ = hint(ram, []ADDRESS) + snd( []ADDRESS, []0, 0, ) // init + rcv( []ADDRESS, []VALUE_READ, TIMESTAMP_READ, ) // finl ``` where -```rust -rcv( address, timestamp, value ) -snd( address, timestamp, value ) -``` - Any zkc module `MOD` that allows one to touch the WOM requires the following columns ```rust -WOM_TRIGGER -WOM_ADDRESS -WOM_TIMESTAMP_WRITTEN -WOM_IS_WRITE -WOM_VALUE +RAM_TRIGGER +[]RAM_ADDRESS +[]RAM_VALUE // the value retrieved by +RAM_TIMESTAMP_WRITTEN +RAM_IS_WRITE ``` and we require bilateral conditional lookups -| MOD | WOM | Notes | -| --------------- | ------------------- | ----------- | -| RAM_TRIGGER | EXEC | condition | -| --------------- | ------------------- | ----------- | -| RAM_ADDRESS | ADDRESS | | -| RAM_TIMESTAMP | TIMESTAMP_WRITTEN | | -| RAM_IS_WRITE | IS_WRITE | | -| RAM_VALUE | VALUE_WRITTEN | | +| MOD | WOM | Notes | +| --------------------- | ----------------- | --------- | +| RAM_TRIGGER | EXEC | condition | +| []RAM_ADDRESS | []ADDRESS | | +| []RAM_VALUE | []VALUE_WRITTEN | | +| RAM_TIMESTAMP_WRITTEN | TIMESTAMP_WRITTEN | | +| RAM_IS_WRITE | IS_WRITE | | ### Lanes -There is an issue wrt _input lanes_: if the `ADDRESS` is a tuple then you need some canonical way to enumerate/list its items. Under the hood one can imagine that all components would still end up being `uX`'s for some `X`. The `VALUES_XXX` are tuples there shouldn't be much of an issue conceptually. +There is an issue wrt _input lanes_: if the `[]ADDRESS` is a tuple then you need some canonical way to enumerate/list its items. Under the hood one can imagine that all components would still end up being `uX`'s for some `X`. The `VALUES_XXX` are tuples there shouldn't be much of an issue conceptually. -There is the question of emptyness: what to do if we have a "you only pay the initialization / finalization prize for those cells that you touched approach" and no operations were done in the various ROM/WOM/RAM's ? One simple approach to this would be to force a single interaction with every memory component. +What to do in case of empty RAM ? It shouldn't be an issue in our RV-interpreter. +In the "you only initialize / finalize those cells that you touched" approach +you can force an interaction with address `[]0`, for instance +what diff --git a/rom (read once memory).md b/rom (read once memory).md index 568c3d8b6..b8d06a5db 100644 --- a/rom (read once memory).md +++ b/rom (read once memory).md @@ -4,9 +4,9 @@ Here's one set of constraints for a read-once-memory (ROM) module. We make the following assumptions: - a ROM is an immutable table -- addresses are consecutive, start at 0 and there are no gaps +- addresses are consecutive, start at 0; there are no gaps - the full contents of that memory will be read start to finish at one specific point in time -- the ROM is never read from again +- the ROM is never touched again **Note.** The fact that this data is read **once** must be assured by the zkc program itself. The ROM has no control over it. If the ROM were to enforce this we would have to add a source @@ -30,9 +30,9 @@ The entire thing can be arranged as a single lookup ```rust // columns of the source -ACCESS // determines padding (ACCESS ≡ 0) and non padding rows (ACCESS ≡ 1) -ADDRESS // a multitude of columns, potentially -VALUE // a multitude of columns, potentially +ACCESS // determines padding (ACCESS ≡ 0) and non padding rows (ACCESS ≡ 1) +[]ADDRESS // slice of columns that define the address space +[]VALUE // slice of columns that define the value space // binary constraint ACCESS @@ -43,11 +43,11 @@ and one will impose ```rust ACCESS[0] = False if ACCESS = False: - ADDRESS = 0 + []ADDRESS = 0 if ACCESS = True: next( ACCESS ) = True - ADDRESS = 1 + prev( ADDRESS ) + []ADDRESS = 1 + prev( []ADDRESS ) ``` ## Requirements for sources adding to the bus @@ -56,15 +56,15 @@ Any zkc module `MOD` that may read a ROM requires the following columns ```rust ROM_ACCESS -ROM_ADDRESS -ROM_VALUE +[]ROM_ADDRESS +[]ROM_VALUE ``` and we require bilateral conditional lookups -| MOD | ROM | Notes | -| ------------- | --------- | ----------- | -| ROM_ACCESS | ACCESS | condition | -| ------------- | --------- | ----------- | -| ROM_ADDRESS | ADDRESS | | -| ROM_VALUE | VALUE | | +| MOD | ROM | Notes | +| --------------- | ----------- | ----------- | +| ROM_ACCESS | ACCESS | condition | +| --------------- | ----------- | ----------- | +| []ROM_ADDRESS | []ADDRESS | | +| []ROM_VALUE | []VALUE | | diff --git a/rom (read only memory).md b/rom (read only memory).md index b7364ccc8..2dbbdbf04 100644 --- a/rom (read only memory).md +++ b/rom (read only memory).md @@ -4,7 +4,7 @@ Here's one set of constraints for a write-once-memory (ROM) module. We make the - a ROM is an immutable table: reads always return the same value across the full lifetime of the execution -### Triggering the finalization phase +## Triggering the finalization phase To avoid ROM living parallel lives, there should be a single ROM finalization event. This will force a single initialization event and a single timeline for a given address in the ROM. @@ -13,8 +13,8 @@ This will force a single initialization event and a single timeline for a given // columns of a ROM EXEC FINL -ADDRESS // a multitude of columns, potentially -VALUE // a multitude of columns, potentially +[]ADDRESS // a multitude of columns, potentially +[]VALUE // a multitude of columns, potentially TIMESTAMP_READ TIMESTAMP_WRITTEN ``` @@ -34,7 +34,7 @@ EXEC + FINL Furthermore one wants -### The "constrain the full range output range" case +## The "constrain the full range output range" case Note. The "constrain the nontrivial part of the output range" alternative has issues if the output is empty. @@ -47,40 +47,40 @@ if EXEC = true then // bus interactions // this ROM address may have already been touched, but it wasn't written to yet // this ROM address was previously written to - rcv( ADDRESS, TIMESTAMP_READ, VALUE ) - snd( ADDRESS, TIMESTAMP_WRITTEN, VALUE ) + rcv( []ADDRESS, []VALUE, TIMESTAMP_READ, ) + snd( []ADDRESS, []VALUE, TIMESTAMP_WRITTEN, ) // the finalization phase does both initializations and finalizations if FINL = true then // below we assume for simplicity that addresses are described by a single int // address starts at 0 and increments by 1 if prev FINL = false then - ADDRESS = 0 + []ADDRESS = 0 if prev FINL = true then - ADDRESS = 1 + prev(ADDRESS) + []ADDRESS = 1 + []prev(ADDRESS) // bus interactions if WAS_ALREADY_WRITTEN_TO = true then // address of ROM was written to at some point - snd( ADDRESS, 0, VALUE ) // initialization - rcv( ADDRESS, TIMESTAMP_READ, VALUE ) // finalization + snd( []ADDRESS, []VALUE, 0, ) // initialization + rcv( []ADDRESS, []VALUE, TIMESTAMP_READ, ) // finalization ``` where ```rust -rcv( address, timestamp, is_written, value ) -snd( address, timestamp, is_written, value ) +rcv( address, value, timestamp, is_written, ) +snd( address, value, timestamp, is_written, ) ``` Any zkc module `MOD` that allows one to touch the ROM requires the following columns ```rust ROM_TRIGGER -ROM_ADDRESS +[]ROM_ADDRESS +[]ROM_VALUE ROM_TIMESTAMP_WRITTEN ROM_IS_WRITE -ROM_VALUE ``` and we require bilateral conditional lookups @@ -88,7 +88,7 @@ and we require bilateral conditional lookups | MOD | ROM | Notes | | ------------- | --------- | --------- | | ROM_TRIGGER | EXEC | condition | -| ROM_ADDRESS | ADDRESS | | +| []ROM_ADDRESS | []ADDRESS | | +| []ROM_VALUE | []VALUE | | | ROM_TIMESTAMP | TIMESTAMP | | | ROM_IS_WRITE | IS_WRITE | | -| ROM_VALUE | VALUE | | diff --git a/rom.md b/rom.md deleted file mode 100644 index a0f6461e6..000000000 --- a/rom.md +++ /dev/null @@ -1,94 +0,0 @@ -## ROM module - -Here's one set of constraints for a write-once-memory (ROM) module. We make the following assumptions: - -- a ROM is an immutable table: reads always return the same value across the full lifetime of the execution - -### Triggering the finalization phase - -To avoid ROM living parallel lives, there should be a single ROM finalization event. -This will force a single initialization event and a single timeline for a given address in the ROM. - -```rust -// columns of a ROM -EXEC -FINL -ADDRESS // a multitude of columns, potentially -VALUE // a multitude of columns, potentially -TIMESTAMP_READ -TIMESTAMP_WRITTEN -``` - -and one will impose - -```rust -// binary columns -EXEC -FINL -EXEC + FINL // EXEC ∙ FINL ≡ 0 - -// monotonous expressions (nondecreasing expressions) -FINL -EXEC + FINL -``` - -Furthermore one wants - -### The "constrain the full range output range" case - -Note. The "constrain the nontrivial part of the output range" alternative has issues if the output is empty. - -```rust -if EXEC = true then - // timestamp comparisons are only meaningful if associated - // to actual reads / writes in the execution phase - TIMESTAMP_READ < TIMESTAMP_WRITTEN - - // bus interactions - // this ROM address may have already been touched, but it wasn't written to yet - // this ROM address was previously written to - rcv( ADDRESS, TIMESTAMP_READ, VALUE ) - snd( ADDRESS, TIMESTAMP_WRITTEN, VALUE ) - -// the finalization phase does both initializations and finalizations -if FINL = true then - // below we assume for simplicity that addresses are described by a single int - // address starts at 0 and increments by 1 - if prev FINL = false then - ADDRESS = 0 - if prev FINL = true then - ADDRESS = 1 + prev(ADDRESS) - - // bus interactions - if WAS_ALREADY_WRITTEN_TO = true then - // address of ROM was written to at some point - snd( ADDRESS, 0, VALUE ) // initialization - rcv( ADDRESS, TIMESTAMP_READ, VALUE ) // finalization -``` - -where - -```rust -rcv( address, timestamp, is_written, value ) -snd( address, timestamp, is_written, value ) -``` - -Any zkc module `MOD` that allows one to touch the ROM requires the following columns - -```rust -ROM_TRIGGER -ROM_ADDRESS -ROM_TIMESTAMP_WRITTEN -ROM_IS_WRITE -ROM_VALUE -``` - -and we require bilateral conditional lookups - -| MOD | ROM | Notes | -| ------------- | --------- | --------- | -| ROM_TRIGGER | EXEC | condition | -| ROM_ADDRESS | ADDRESS | | -| ROM_TIMESTAMP | TIMESTAMP | | -| ROM_IS_WRITE | IS_WRITE | | -| ROM_VALUE | VALUE | | diff --git a/wom.md b/wom.md index 6654793aa..fa62c3c0a 100644 --- a/wom.md +++ b/wom.md @@ -1,11 +1,19 @@ ## WOM module -Here's one set of constraints for a write-once-memory (WOM) module. We make the following assumptions: +We present constraints for a write-once-memory (WOM) module with the following features: -- the WOM may be read from arbitrarily: before it's been written to reads should return 0 -- multiple writes at a given address are allowed unless they overwrite a previously written value +- the WOM may be read from and written to arbitrarily subject to the following rules: + - a read (`IS_WRITE ≡ false`) to an address that hasn't been written to (`WAS_ALREADY_WRITTEN_TO ≡ false`) returns 0 + - a write (`IS_WRITE ≡ true`) to an address that hasn't been written to (`WAS_ALREADY_WRITTEN_TO ≡ false`) flips `WAS_ALREADY_WRITTEN_TO` to `true` + - reads and writes to an address that has already been written to (`WAS_ALREADY_WRITTEN_TO ≡ true`) reproduce the same value in the snd / rcv requests +- note that the `WAS_ALREADY_WRITTEN_TO` bit is a _prediction_ +- the WOM may be written to (at a given address) once; further writes are allowed unless they overwrite a previously written value +- reads / writes may ocurr in all segments of the trace +- regardless, the WOM must ensure its own consistency -By definition in a WOM, once a memory cell with address `a` has been written to, the value in memory may never change from here on out: every subsequent read, including the finalization read, returns that value. A WOM module will have the following columns. +By definition in a WOM, once a memory cell with address `a` has been written to, +the value in memory may never change from here on out: every subsequent read, +including the finalization read, returns that value. ### Triggering the finalization phase @@ -15,10 +23,17 @@ To avoid WOM living parallel lives, there should be a single WOM finalization ev // columns of a WOM EXEC FINL -ADDRESS + +// address columns for the address lanes +[]ADDRESS + +// value columns for the value lanes +[]VALUE + TIMESTAMP_READ TIMESTAMP_WRITTEN -VALUE +TIMESTAMP_DELTA + WAS_ALREADY_WRITTEN_TO IS_WRITE ``` @@ -31,7 +46,9 @@ EXEC FINL WAS_ALREADY_WRITTEN_TO IS_WRITE -EXEC + FINL + +// exclusivity +EXEC ∙ FINL ≡ 0 // monotonous expressions (nondecreasing expressions) FINL @@ -49,26 +66,27 @@ if EXEC = true then // timestamp comparisons are only meaningful if associated // to actual reads / writes in the execution phase TIMESTAMP_READ < TIMESTAMP_WRITTEN + // the constraint is enforced via TIMESTAMP_WRITTEN = TIMESTAMP_READ + 1 + TIMESTAMP_DELTA // bus interactions // this WOM address may have already been touched, but it wasn't written to yet if WAS_ALREADY_WRITTEN_TO = false then - rcv( ADDRESS, TIMESTAMP_READ, false, 0 ) - snd( ADDRESS, TIMESTAMP_WRITTEN, IS_WRITE, VALUE ) - if IS_WRITE = false then VALUE = 0 + rcv( []ADDRESS, []0, TIMESTAMP_READ, false, ) // read + snd( []ADDRESS, []VALUE, TIMESTAMP_WRITTEN, IS_WRITE, ) // write (maybe) + if IS_WRITE = false then []VALUE = []0 // this WOM address was previously written to if WAS_ALREADY_WRITTEN_TO = true then - rcv( ADDRESS, TIMESTAMP_READ, true, VALUE ) - snd( ADDRESS, TIMESTAMP_WRITTEN, true, VALUE ) + rcv( []ADDRESS, []VALUE, TIMESTAMP_READ, true, ) // read + snd( []ADDRESS, []VALUE, TIMESTAMP_WRITTEN, true, ) // write (the same value) // the finalization phase does both initializations and finalizations if FINL = true then // address starts at 0 and increments by 1 if prev FINL = false then - ADDRESS = 0 + []ADDRESS = []0 if prev FINL = true then - ADDRESS = 1 + prev(ADDRESS) + []ADDRESS = 1 + prev( []ADDRESS ) // no writes take place in the finalization phase IS_WRITE = false @@ -76,29 +94,29 @@ if FINL = true then // bus interactions if WAS_ALREADY_WRITTEN_TO = false then // address of WOM was never written to - snd( ADDRESS, 0, false, 0 ) // initialization - rcv( ADDRESS, TIMESTAMP_READ, false, 0 ) // finalization + snd( []ADDRESS, []0, 0, false, ) // initialization, set initial value to 0 + rcv( []ADDRESS, []0, TIMESTAMP_READ, false, ) // finalization, read final value for what it is, 0 if WAS_ALREADY_WRITTEN_TO = true then // address of WOM was written to at some point - snd( ADDRESS, 0, false, 0 ) // initialization - rcv( ADDRESS, TIMESTAMP_READ, true, VALUE ) // finalization + snd( []ADDRESS, []0, 0, false, ) // initialization, set initial value to 0 + rcv( []ADDRESS, []VALUE, TIMESTAMP_READ, true, ) // finalization, read final value for what it is ``` where ```rust -rcv( address, timestamp, is_written, value ) -snd( address, timestamp, is_written, value ) +rcv( []address, []value, timestamp, has_been_written_to, ) +snd( []address, []value, timestamp, has_been_written_to, ) ``` Any zkc module `MOD` that allows one to touch the WOM requires the following columns ```rust WOM_TRIGGER -WOM_ADDRESS +[]WOM_ADDRESS +[]WOM_VALUE WOM_TIMESTAMP_WRITTEN WOM_IS_WRITE -WOM_VALUE ``` and we require bilateral conditional lookups @@ -106,7 +124,7 @@ and we require bilateral conditional lookups | MOD | WOM | Notes | | ------------- | --------- | --------- | | WOM_TRIGGER | EXEC | condition | -| WOM_ADDRESS | ADDRESS | | +| []WOM_ADDRESS | []ADDRESS | | +| []WOM_VALUE | []VALUE | | | WOM_TIMESTAMP | TIMESTAMP | | | WOM_IS_WRITE | IS_WRITE | | -| WOM_VALUE | VALUE | | From dee6fbf03aaccebcf2072605a8a7f794926b8066 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 25 Jun 2026 09:24:53 +0200 Subject: [PATCH 7/7] feat: AOM constraints AOM stands for Access Once Memory and is meant to encompass both Read Once Memory and Write Once Memory --- pkg/zkc/constraints/translator.go | 134 ++++++++++++++++++++++++----- testdata/zkc/unit/_example_aom.zkc | 12 +++ 2 files changed, 124 insertions(+), 22 deletions(-) create mode 100644 testdata/zkc/unit/_example_aom.zkc diff --git a/pkg/zkc/constraints/translator.go b/pkg/zkc/constraints/translator.go index 0c1c9a93b..ecdcd322f 100644 --- a/pkg/zkc/constraints/translator.go +++ b/pkg/zkc/constraints/translator.go @@ -95,14 +95,14 @@ func translateStaticMemory[F field.Element[F]](_ schema.ModuleId, m vm.Memory[F] func translateReadOnlyMemory[F field.Element[F]]( ctx schema.ModuleId, fm vm.Memory[F]) mir.Module[F] { var name = trace.ModuleName{Name: fm.Name(), Multiplier: 1} - return translateSingleAccessMemory(ctx, fm, name) + return translateAccessOnceMemory(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.Memory[F]) mir.Module[F] { var name = trace.ModuleName{Name: fm.Name(), Multiplier: 1} - return translateSingleAccessMemory(ctx, fm, name) + return translateAccessOnceMemory(ctx, fm, name) } func translateReadWriteMemory[F field.Element[F]]( @@ -141,9 +141,10 @@ func translateReadWriteMemory[F field.Element[F]]( } } - // var address = register.NewId(memoryModule.Width() + 0) - // var valueRead = register.NewId(memoryModule.Width() + 1) - memoryModule.AddRegisters(register.NewComputed("address", addressWidth, padding)) + var ( + addressDelta = register.NewId(memoryModule.Width() + 0) + ) + memoryModule.AddRegisters(register.NewComputed("address_delta", addressWidth, padding)) memoryModule.AddRegisters(register.NewComputed("valueRead", valueWidth, padding)) @@ -156,17 +157,20 @@ func translateReadWriteMemory[F field.Element[F]]( 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) - prevExec = mirc.Variable[register.Id, Expr[F]](execPhase, 1, -1) - prevFinl = 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) + 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) + addrRegs = fm.Geometry().AddressRegisters() + addrRegOffset = uint(0) + prevAddr = concatenateRegisters[F](addrRegs, addrRegOffset, -1) + addr = concatenateRegisters[F](addrRegs, addrRegOffset, 0) + addrDelta = mirc.Variable[register.Id, Expr[F]](addressDelta, 1, 0) + prevExec = mirc.Variable[register.Id, Expr[F]](execPhase, 1, -1) + prevFinl = 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) ) // ================================================ @@ -195,8 +199,8 @@ func translateReadWriteMemory[F field.Element[F]]( mirc.If(mirc.Sum([]Expr[F]{prevExec, prevFinl}).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 + // we want WT > RT which we prove via WT = RT + (1 + ΔT) + // which works given that ΔT is ≥ 0 timestampMonotony := mir.NewVanishingConstraint("timestamp_monotony", ctx, util.None[int](), mirc.If(exec.NotEquals(zero), wTime.Equals(rTime.Add(dTime, one))).AsLogical()) @@ -207,7 +211,8 @@ func translateReadWriteMemory[F field.Element[F]]( // []register.Id{address, timestampWritten, valueWritten}) addressMonotonyInFinl := mir.NewVanishingConstraint("address_monotony_in_finalization_phase", ctx, util.None[int](), - mirc.If(mirc.Product([]Expr[F]{finl, prevFinl}).NotEquals(zero), wTime.Equals(rTime.Add(dTime, one))).AsLogical()) + mirc.If(mirc.Product([]Expr[F]{finl, prevFinl}).NotEquals(zero), + addr.Equals(prevAddr.Add(addrDelta, one))).AsLogical()) constraints := []mir.Constraint[F]{ flagExclusivity, @@ -223,12 +228,97 @@ func translateReadWriteMemory[F field.Element[F]]( return memoryModule } -// translateSingleAccessMemory handles both +// translateAccessOnceMemory handles both // - read once memory // - write once memory -func translateSingleAccessMemory[F field.Element[F]]( +func translateAccessOnceMemory[F field.Element[F]]( ctx schema.ModuleId, fm vm.Memory[F], name trace.ModuleName) (mod mir.Module[F]) { - return + var ( + memoryModule *schema.Table[F, mir.Constraint[F]] + padding big.Int + ) + + // Initialise module and add all registers + memoryModule = memoryModule.Init(name, false, true, false, fm.IsNative(), false, 0) + memoryModule.AddRegisters(fm.Registers()...) + + var ( + access = register.NewId(memoryModule.Width() + 0) + ) + + memoryModule.AddRegisters(register.NewComputed("access", 1, padding)) + + var ( + addrRegs = fm.Geometry().AddressRegisters() + addrRegOffset = uint(0) + addr = concatenateRegisters[F](addrRegs, addrRegOffset, 0) + nextAddr = concatenateRegisters[F](addrRegs, addrRegOffset, 1) + acc = mirc.Variable[register.Id, Expr[F]](access, 1, 0) + nextAcc = mirc.Variable[register.Id, Expr[F]](access, 1, 1) + zero = mirc.Number[register.Id, Expr[F]](0) + one = mirc.Number[register.Id, Expr[F]](1) + ) + + // ================================================ + // constraints + // ================================================ + + // ================================================ + // ACCESS bit constraints + // ================================================ + + // ACCESS[0] = 0 + accessBitVanishesInPadding := mir.NewVanishingConstraint("access_bit_vanishes_in_padding", ctx, util.Some[int](0), + acc.Equals(zero).AsLogical()) + // ACCESS[i] = 1 => ACCESS[i + 1] = 1 + accessBitMonotony := mir.NewVanishingConstraint("access_bit_monotony", ctx, util.None[int](), + mirc.If(acc.Equals(one), nextAcc.Equals(one)).AsLogical()) + + // ================================================ + // []ADDRESS constraints + // ================================================ + + // If ACCESS[i] = 0 Then ADDRESS[i] = 0 + addressesVanishInPadding := mir.NewVanishingConstraint("addresses_vanish_in_padding", ctx, util.None[int](), + mirc.If(acc.Equals(zero), addr.Equals(zero)).AsLogical()) + // If ACCESS[i] = 0 ∧ ACCESS[i + 1] = 1 Then ADDRESS[i + 1] = 0 + firstNonpaddingAddressIsZero := mir.NewVanishingConstraint("first_nontrivial_address_is_zero", ctx, util.None[int](), + mirc.If(acc.Equals(zero), + mirc.If(nextAcc.NotEquals(zero), + nextAddr.Equals(zero))).AsLogical()) + // If ACCESS[i] = 1 Then ADDRESS[i + 1] = 1 + ADDRESS[i] + addressMonotony := mir.NewVanishingConstraint("address_monotony", ctx, util.None[int](), + mirc.If(acc.NotEquals(zero), nextAddr.Equals(addr.Add(one))).AsLogical()) + + constraints := []mir.Constraint[F]{ + accessBitVanishesInPadding, + accessBitMonotony, + addressesVanishInPadding, + firstNonpaddingAddressIsZero, + addressMonotony, + } + memoryModule.AddConstraints(constraints...) + + return memoryModule +} + +// concatenateRegisters concatenates registers in 'big endian order', e.g. +// [a, b, c] should correspond to a :: b :: c. It assumes that register ids +// are contiguous (and start at id = base). +func concatenateRegisters[F field.Element[F]](registers []register.Register, base uint, shift int) Expr[F] { + terms := make([]Expr[F], len(registers)) + // cumulative width of registers + tail := uint(0) + // + for j := len(registers) - 1; j >= 0; j-- { + w := registers[j].Width() + v := mirc.Variable[register.Id, Expr[F]](register.NewId(base+uint(j)), w, shift) + weight := new(big.Int).Lsh(big.NewInt(1), tail) // 2^tail + terms[j] = v.Multiply(mirc.BigNumber[register.Id, Expr[F]](weight)) + tail += w + } + // + return mirc.Sum(terms) } func translateFunction[F field.Element[F]](ctx schema.ModuleId, fm vm.FieldFunction) mir.Module[F] { diff --git a/testdata/zkc/unit/_example_aom.zkc b/testdata/zkc/unit/_example_aom.zkc new file mode 100644 index 000000000..29d91c568 --- /dev/null +++ b/testdata/zkc/unit/_example_aom.zkc @@ -0,0 +1,12 @@ +// access once memory +output AOM(address_1 :u4, address_2 :u16) -> (value :u4) + +fn main<>() { + var r :u4 = 7 + AOM[1, 1] = f(r) +} + +fn f<>(x:u4) -> (r:u4) { + r = x + 1 + return +}