[feat] Enforce semantics for write once memory (wom) by OlivierBBB · Pull Request #1834 · LFDT-Lineth/zkc

OlivierBBB · 2026-06-02T21:52:32Z

No description provided.

Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>

CLAassistant · 2026-06-02T22:01:05Z

All committers have signed the CLA.

…emory-wom

Copilot

Pull request overview

This PR aims to introduce/enforce semantics for write-once memory (WOM) by adding specification docs (RAM/ROM/WOM) and beginning an implementation of memory-related MIR constraints in the ZkC constraints translator, along with a small unit-test fixture.

Changes:

Added markdown specifications for RAM/ROM/WOM constraint semantics and lookup interactions.
Refactored memory translation in pkg/zkc/constraints/translator.go to route ROM/WOM/RAM through a shared translateMemoryCommon() and added initial (partial) constraints.
Added a new unit test fixture and a test entry for it.

Reviewed changes

Copilot reviewed 15 out of 15 changed files in this pull request and generated 13 comments.

Show a summary per file

File	Description
wom.md	New WOM constraint specification (docs) including bus interaction pseudocode and lookup mapping.
rom.md	New ROM constraint specification (docs).
ram.md	New RAM constraint specification (docs) and discussion of finalization.
pkg/zkc/constraints/translator.go	Implements shared memory translation and adds initial flag/timestamp constraints for memories.
pkg/ir/mir/constraint.go	Adds placeholder constructors for send/receive constraints.
pkg/test/zkc_unit_test.go	Adds a new unit test invoking the new `_example` fixture.
testdata/zkc/unit/_example.zkc	New unit test program fixture.
testdata/zkc/unit/_example.accepts	New expected I/O JSON for the `_example` fixture.
testdata/zkc/unit/_example_0.zkc	Additional example fixture (not referenced by the new test entry).
pkg/zkc/compiler/parser/environment.go	Receiver renaming cleanup for Environment methods.
pkg/zkc/compiler/codegen/statement.go	Comment example formatting tweak (documentation-only).
pkg/zkc/compiler/ast/decl/decl.go	Expanded Declaration doc comment.
pkg/schema/constraint/vanishing/constraint.go	Comment punctuation tweak.
pkg/schema/constraint/ranged/constraint.go	Comment punctuation tweak.
pkg/ir/hir/constraint.go	Comment punctuation tweak.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

DavePearce · 2026-06-07T21:42:38Z

+// > var t tmp
+// > tmp = f(...)


Agreed, this is a typo

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


+```rust
+rcv( address, timestamp, is_written, value )
+snd( address, timestamp, is_written, value )
+```


+
+### 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:


+
+// executed at program end
+if pc == MAX_UINT_64 {
+  // finaliztion of ROM's


+snd( address, timestamp, value )
+```
+
+Any zkc module `MOD` that allows one to touch the WOM requires the following columns


DavePearce

Overall, it is good to see that you are getting the hang of how to write MIR constraints within the ZkC compiler. There is some minor misunderstandings around the columns address and valueRead (i.e. since the necessary columns are already added from the memory declaration in ZkC).

However, some things about this PR also confuse me:

(Which Issue?) One of the strange things about this PR is that it does not address issue #1560. It is more like a PR for #1800 but anticipating the use send/receive instead of just lookups (which is what I was expecting).
(Timestamps) It is confusing me why you are adding read/write timestamps for ROM/WOMs. We don't need timestamps for these memory types (and, in fact, we cannot have them under the current design). Timestamps are intended specifically for accessing RAM.

To me, it feels more like you've been writing the constraints for RAM here instead those for ROM/WOM. For example, timestamp_monotony is what I expect to see for RAM not for ROM/WOM.

DavePearce · 2026-06-07T21:41:43Z

 )

+func Test_ZkcUnit_Example(t *testing.T) {
+	checkZkcUnit(t, "zkc/unit/_example", util.DEFAULT_CONFIG)


Why does the test begin with an underscore? That's not consistent with others. Something like basic_XX or ram_XX would be consistent.

DavePearce · 2026-06-07T21:42:38Z

+// > var t tmp
+// > tmp = f(...)


Agreed, this is a typo

DavePearce · 2026-06-07T21:44:15Z

 // 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 {


Not really sure what the motivation for this change is? Did claude suggest this or something? p is for "pointer", and is generally what is used in the code base. Anyway, not an issue ... just not sure where its coming from.

DavePearce · 2026-06-07T22:20:54Z

+	timestampMonotony := mir.NewVanishingConstraint("timestamp_monotony", ctx, util.None[int](),
+		mirc.If(exec.NotEquals(zero), wTime.Equals(rTime.Add(dTime, one))).AsLogical())
+
+	// var isImmutable bool


I'm not sure if this is code you want to keep for later so that it can be enabled again? If so, seems fine since we cannot fully implement this solution without send/receive. But, if its junk, then remove please.

DavePearce · 2026-06-07T22:22:39Z

@@ -0,0 +1,24 @@
+memory RAM(address :u4) -> (value :u4)


This test is not used anywhere ... ?

DavePearce · 2026-06-07T22:25:07Z

@@ -0,0 +1,134 @@
+## RAM module


I guess this is like some working notes. It doesn't belong in the testdata/zkc/unit directory. Maybe put it in docs/ where eventually we merge it into docs/ZKC_ARCHITECTURE_CONSTRAINTS.md.

DavePearce · 2026-06-07T22:26:11Z

@@ -0,0 +1,94 @@
+## ROM module


ditto re location and also for the wom.md file.

DavePearce · 2026-06-07T22:27:43Z


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


Its also strange to me that you would have a timestamp written for a ROM --- this doesn't make sense.

in fact, it doesn't make sense to have timestamps for ROM or WOM at all. Yes for RAM, but no for the others.

…emory-wom

AOM stands for Access Once Memory and is meant to encompass both Read Once Memory and Write Once Memory

…emory-wom Signed-off-by: Olivier Bégassat <38285177+OlivierBBB@users.noreply.github.com>

OlivierBBB linked an issue Jun 2, 2026 that may be closed by this pull request

feat: enforce semantics for Write Once Memory (WOM) #1560

Open

OlivierBBB added 4 commits June 3, 2026 00:00

wip

ea6b692

Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>

ras

6671d63

Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>

feat: unified memory

3721199

Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>

ras: renaming of p to env in environment.go

c0cc361

Signed-off-by: Olivier Bégassat <olivier.begassat.cours@gmail.com>

OlivierBBB force-pushed the 1560-feat-enforce-semantics-for-write-once-memory-wom branch from 5cf507a to 145c864 Compare June 2, 2026 22:00

OlivierBBB force-pushed the 1560-feat-enforce-semantics-for-write-once-memory-wom branch from aaa745a to c0cc361 Compare June 2, 2026 22:12

Merge branch 'main' into 1560-feat-enforce-semantics-for-write-once-m…

0f2959c

…emory-wom

OlivierBBB self-assigned this Jun 2, 2026

OlivierBBB marked this pull request as ready for review June 3, 2026 08:00

Copilot AI review requested due to automatic review settings June 3, 2026 08:00

Copilot started reviewing on behalf of OlivierBBB June 3, 2026 08:00 View session

Copilot AI reviewed Jun 3, 2026

View reviewed changes

OlivierBBB mentioned this pull request Jun 3, 2026

zkc completeness LFDT-Lineth/lineth-monorepo#3223

Open

8 tasks

DavePearce reviewed Jun 7, 2026

View reviewed changes

OlivierBBB and others added 5 commits June 24, 2026 01:12

Merge branch 'main' into 1560-feat-enforce-semantics-for-write-once-m…

544f1da

…emory-wom

ras

d3c68ba

ras: documentation

e587dd4

feat: AOM constraints

dee6fbf

AOM stands for Access Once Memory and is meant to encompass both Read Once Memory and Write Once Memory

Merge branch 'main' into 1560-feat-enforce-semantics-for-write-once-m…

adc023d

…emory-wom Signed-off-by: Olivier Bégassat <38285177+OlivierBBB@users.noreply.github.com>


		### 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:

Uh oh!

Conversation

OlivierBBB commented Jun 2, 2026

Uh oh!

CLAassistant commented Jun 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

DavePearce left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

CLAassistant commented Jun 2, 2026 •

edited

Loading