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/pkg/ir/hir/constraint.go b/pkg/ir/hir/constraint.go
index 5203941de..75fedb704 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 5261f4c10..e74072045 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 e15bef107..9e3e3181e 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 ebc76f276..7c75dc5c8 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 4ab9fa23c..d4a83d9a9 100644
--- a/pkg/test/zkc_unit_test.go
+++ b/pkg/test/zkc_unit_test.go
@@ -32,6 +32,14 @@ var DEFAULT_UNIT_CONFIG = util.DEFAULT_CONFIG.
 var DEFAULT_UNITBIG_CONFIG = DEFAULT_UNIT_CONFIG.
 	Words(vm.WORD_UINT128)
 
+// ===================================================================
+// example test
+// ===================================================================
+
+func Test_ZkcUnit_Example(t *testing.T) {
+	checkZkcUnit(t, "zkc/unit/_example", DEFAULT_UNIT_CONFIG.Constraints(true).GoGen(false))
+}
+
 // ===================================================================
 // Basic Tests
 // ===================================================================
diff --git a/pkg/zkc/compiler/ast/decl/decl.go b/pkg/zkc/compiler/ast/decl/decl.go
index 1074cd026..0bd5e69d1 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 ad2de8e95..8f58b6c8c 100644
--- a/pkg/zkc/compiler/codegen/statement.go
+++ b/pkg/zkc/compiler/codegen/statement.go
@@ -88,7 +88,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 6785b3f71..ecdcd322f 100644
--- a/pkg/zkc/constraints/translator.go
+++ b/pkg/zkc/constraints/translator.go
@@ -92,43 +92,233 @@ func translateStaticMemory[F field.Element[F]](_ schema.ModuleId, m vm.Memory[F]
 	return mod
 }
 
-func translateReadOnlyMemory[F field.Element[F]](_ schema.ModuleId, fm vm.Memory[F]) mir.Module[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 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 translateAccessOnceMemory(ctx, fm, name)
+}
+
+func translateReadWriteMemory[F field.Element[F]](
+	ctx 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}
+		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.Memory[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
+
+	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
+		valueWidth   uint
+	)
+
+	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 (
+		addressDelta = register.NewId(memoryModule.Width() + 0)
+	)
+
+	memoryModule.AddRegisters(register.NewComputed("address_delta", 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)
+		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)
+	)
+
+	// ================================================
+	// 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(prevFinl.NotEquals(zero), finl.Equals(one)).AsLogical())
+	flagMonotony2 := mir.NewVanishingConstraint("exec+finl_monotony", ctx, util.None[int](),
+		mirc.If(mirc.Sum([]Expr[F]{prevExec, prevFinl}).NotEquals(zero),
+			mirc.Sum([]Expr[F]{exec, finl}).Equals(one)).AsLogical())
+
+	// 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())
+
+	// // 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})
+
+	addressMonotonyInFinl := mir.NewVanishingConstraint("address_monotony_in_finalization_phase", ctx, util.None[int](),
+		mirc.If(mirc.Product([]Expr[F]{finl, prevFinl}).NotEquals(zero),
+			addr.Equals(prevAddr.Add(addrDelta, one))).AsLogical())
+
+	constraints := []mir.Constraint[F]{
+		flagExclusivity,
+		flagMonotony1,
+		flagMonotony2,
+		timestampMonotony,
+		// rcvExec,
+		// sndExec,
+		addressMonotonyInFinl,
+	}
+	memoryModule.AddConstraints(constraints...)
+
+	return memoryModule
 }
 
-func translateReadWriteMemory[F field.Element[F]](_ schema.ModuleId, fm vm.Memory[F]) mir.Module[F] {
+// translateAccessOnceMemory handles both
+//   - read once memory
+//   - write once memory
+func translateAccessOnceMemory[F field.Element[F]](
+	ctx schema.ModuleId, fm vm.Memory[F], name trace.ModuleName) (mod 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
 	)
-	// 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
+
+	// 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/ram.md b/ram.md
new file mode 100644
index 000000000..bcb11ef88
--- /dev/null
+++ b/ram.md
@@ -0,0 +1,161 @@
+# RAM module
+
+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
+- 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
+while pc != MAX_UINT_64 {
+    instruction = read_32(pc) as Instruction
+    pc = interpreter(instruction, pc)
+}
+
+// Program execution has ended, perform finalization
+if pc == MAX_UINT_64 {
+  // finalization of 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
+
+// slices of address columns
+[]ADDRESS
+[]ADDRESS_DELTA
+
+// slices of value columns
+[]VALUE_READ
+[]VALUE_WRITTEN
+
+// timestamp columns
+TIMESTAMP_WRITTEN
+TIMESTAMP_READ
+TIMESTAMP_DELTA
+
+IS_WRITE
+```
+
+## General constraints
+
+```rust
+// binary columns
+EXEC
+FINL
+IS_WRITE
+EXEC + FINL
+
+// monotonous expressions (nondecreasing expressions)
+FINL
+EXEC + FINL
+```
+
+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`).
+
+## Execution phase constraints
+
+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, []VALUE_READ,    TIMESTAMP_READ,    )
+  snd( []ADDRESS, []VALUE_WRITTEN, TIMESTAMP_WRITTEN, )
+
+  if IS_WRITE = false then
+    []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
+  if prev FINL = true then
+    // using []ADDRESS_DELTA
+    []ADDRESS > prev( []ADDRESS )
+
+    // initialization and finalization
+  TIMESTAMP_READ, []VALUE_READ = hint(ram, []ADDRESS)
+  snd( []ADDRESS, []0,          0,              ) // init
+  rcv( []ADDRESS, []VALUE_READ, TIMESTAMP_READ, ) // finl
+```
+
+where
+
+Any zkc module `MOD` that allows one to touch the WOM requires the following columns
+
+```rust
+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_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.
+
+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
new file mode 100644
index 000000000..b8d06a5db
--- /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; 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 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
+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 // slice of columns that define the address space
+[]VALUE   // slice of columns that define the value space
+
+// 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..2dbbdbf04
--- /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, []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
+  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, []VALUE, 0,              ) // initialization
+    rcv( []ADDRESS, []VALUE, TIMESTAMP_READ, ) // finalization
+```
+
+where
+
+```rust
+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_VALUE
+ROM_TIMESTAMP_WRITTEN
+ROM_IS_WRITE
+```
+
+and we require bilateral conditional lookups
+
+| MOD           | ROM       | Notes     |
+| ------------- | --------- | --------- |
+| ROM_TRIGGER   | EXEC      | condition |
+| []ROM_ADDRESS | []ADDRESS |           |
+| []ROM_VALUE   | []VALUE   |           |
+| ROM_TIMESTAMP | TIMESTAMP |           |
+| ROM_IS_WRITE  | IS_WRITE  |           |
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<RAM>() {
+    var r :u4
+    RAM[1] = f(7)
+}
+
+fn f<RAM>(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..8c4054ee6
--- /dev/null
+++ b/testdata/zkc/unit/_example_0.zkc
@@ -0,0 +1,24 @@
+memory RAM(address :u4) -> (value :u4)
+input  ROM(address :u4, bis :u8) -> (value :u4)
+output WOM(address :u4) -> (value :u4)
+
+fn main<RAM>() {
+    var r :u4
+    r = f(7)
+    WOM[0] = 12
+
+    // WOM[0] = ROM[0, 0]
+    //
+    // if ROM[1,1] != 0xf { fail }
+}
+
+fn f<RAM>(x:u4) -> (r:u4) {
+
+    r = x + RAM[0]
+    if r == 12 {
+        r = r + 1
+    // } else {
+    //     r = r + 3
+    }
+    return
+}
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
+}
diff --git a/wom.md b/wom.md
new file mode 100644
index 000000000..fa62c3c0a
--- /dev/null
+++ b/wom.md
@@ -0,0 +1,130 @@
+## WOM module
+
+We present constraints for a write-once-memory (WOM) module with the following features:
+
+- 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.
+
+### 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 columns for the address lanes
+[]ADDRESS
+
+// value columns for the value lanes
+[]VALUE
+
+TIMESTAMP_READ
+TIMESTAMP_WRITTEN
+TIMESTAMP_DELTA
+
+WAS_ALREADY_WRITTEN_TO
+IS_WRITE
+```
+
+and one will impose
+
+```rust
+// binary columns
+EXEC
+FINL
+WAS_ALREADY_WRITTEN_TO
+IS_WRITE
+
+// exclusivity
+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
+  // 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, []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, []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
+  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, 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,     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, []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_VALUE
+WOM_TIMESTAMP_WRITTEN
+WOM_IS_WRITE
+```
+
+and we require bilateral conditional lookups
+
+| MOD           | WOM       | Notes     |
+| ------------- | --------- | --------- |
+| WOM_TRIGGER   | EXEC      | condition |
+| []WOM_ADDRESS | []ADDRESS |           |
+| []WOM_VALUE   | []VALUE   |           |
+| WOM_TIMESTAMP | TIMESTAMP |           |
+| WOM_IS_WRITE  | IS_WRITE  |           |