feat: enforce semantics for Write Once Memory (WOM)

[DavePearce]

Summary

The semantics of a "write once memory" are exactly what it says on the tin. You cannot write more than once to the same address in a WOM. Attempting to do this should result in a machine panic. But, currently, the ZkC interpreter does not prevent this and allows invalid executions to continue.

Example

The following ZkC program is invalid and should result in a machine panic:

output out(address:u16) -> (byte:u8)

fn main(){
   out[0] = 1
   out[0] = 2 // <-- INVALID
}

With the following json input file:

{}

Then, currently, running this program gives the following:

> zkc exec test.json test.zkc
out = 0x02

Clearly, this violates the intended semantics of a "write once memory".

Approach

Let's consider two example programs:

Program A:

output out(address:u16) -> (byte:u8)

fn main(){
   out[0] = 1
   out[1] = 2 
}

Program B:

output out(address:u16) -> (byte:u8)

fn main(){
   out[1] = 2
   out[0] = 1 

The implementation for write-only memory lives in pkg/zkc/vm/internal/memory/wom.go. There are two different ways this implementation could be updated to enforce a write-once semantics:

1. (strict) This approach requires every write to an output memory is for the next consecutive address. This would mean that "Program A" above is valid, but "Program B" is not.
2. (non-strict) This approach is more relaxed and simply requires that writes to the same address with different values result are not permitted.

The difference between these two approaches comes down to the complexity of enforcing their semantics. Basically, option (1) is easier to implement than option (2).

Implementation for Option (1)

In this option, its pretty straightforward. Within our implementation of memory.WriteOnce we simply check that the write address matches the current size of the data array and, if not, cause a machine panic.

Implementation for Option (2)

This is harder to implement, but of course gives rise to more flexible implementations for constructing output. Its not clear whether this flexibility is needed or not. The rough idea would be this: alongside the existing data array we additionally maintain an written []bool array of the same size. This identifies addresses which have already been written. Thus, when a write occurs at address, we check whether written[address]==true or not. If it does, we issue a machine panic.

[OlivierBBB]

Question 1. Should several assignments with the same value be legal ?

output out(address:u16) -> (byte:u8)

fn main(){
   out[0] = 1
   out[0] = 1 // <-- Legal or not ?
}

[OlivierBBB]

Question 2. Do we want to allow consulting (i.e. reading) WOM ?

output out(address:u16) -> (byte:u8)

fn main(){
   var read_val :u8
   read_val = out[0]       // <- allowable ?
}

What about consulting WOM before assignment ?

output out(address:u16) -> (byte:u8)

fn main(){
   var before :u8
   before = out[0]      // <- allowable ?

   out[0] = 1           // <- legal assignment

   var after :u8
   after = out[0]       // <- allowable ?
}

And if so, should before hold 0 or 1 ?

[OlivierBBB]

Question 3. Do we care about the size of the output memory ? I.e. do we care to distinguish between an outputs that are

• [a,b,0,d]
• [a,b,0,d,0] ?

Also do we care to handle empty outputs as a supported possibility ?

---

We can imagine that

• one segment S will contain all of the WOM's finalization reads (which are required to balance the WOM logbus equation)
• there will be a traditional lookup which
  • is internal to this segment S containing the final reads
  • identifies the finalized values from the WOM with a public input holding the predicted output values
  • is likely bidirectional

If we don't care about trailing zeros we can

• make the bidirectional lookup conditional on the source value being nonzero
• this way we don't have to initialize / finalize empty cells
• but we have to account for gaps in the address space of the WOM and thus need to prove address increments are >0

If we do care about trailing zeros we

• have to initialize / finalize all cells up to the expected output length (which may become a public input)
• we have to initialize / finalize all cells in the output range
• address increments are just +1

[OlivierBBB]

In order to prevent WOM's to lead multiple parallel lives one may enforce a single finalization to take place per WOM. For instance in the main function of the RV zkVM one could have

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

    if pc == MAX_UINT_64 {
       finalize(wom_1)
       finalize(wom_2)
       ...
       finalize(wom_n)
    } else {
       // should be unreachable ...
       fail "Invalid final program counter %x", pc
    }

Finalize should trigger a lookup from the main module of the zkVM to the relevant wom_k module. If we adopt the POV from below its main point is to impose the presence of a FINL = 1 row, which triggers the finalization phase.

[OlivierBBB]

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.

// columns of a WOM
EXEC
FINL
ADDRESS
TIMESTAMP_READ
TIMESTAMP_WRITE
VALUE
WAS_ALREADY_WRITTEN_TO
IS_WRITE

and one will impose

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

if EXEC = true then
  // timestamp comparisons are only meaningful if associated
  // to actual reads / writes in the execution phase
  TIMESTAMP_READ < TIMESTAMP_WRITE

  // 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_WRITE, 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_WRITE, 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

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

WOM_TRIGGER
WOM_ADDRESS
WOM_TIMESTAMP_WRITE
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

[OlivierBBB]

There are several design possibilities; "across the full lifetime of the execution" is used synonymously with "across all segments".

• Read only memory (ROM) is an immutable form of memory that allows both for arbitrary reads and limited "writes"; memory comes pre-filled and undergoes no changes whatsoever; all reads at a given address recover the same value across the full lifetime of the execution; writes fail (i.e. should be unprovable) unless the data being written coincides with the data already in memory; its main job is to ensure data consistency across all segments;
• Write once memory (WOM) is a mutable form of memory that allows for arbitrary reads and a single potentially mutating write per cell; it provides a slice of initially empty data where every cell may be modified at most once across the full lifetime of the execution; reads at a given address a return 0 until that point in time when a is the target of a write operation and an arbitrary value v is written to that address; v = 0 is allowed; beyond that point reads at that address must return v and writes must fail unless the value being written coincides with the value already in memory; its main job is to ensure data consistency and to track the WAS_ALREADY_WRITTEN_TO status across all segments;
• Random access memory (RAM) is a mutable form of memory that allows unlimited reads and writes for every cell; RAM starts out being empty i.e. reads at addresses yet untouched return 0; it's only job is to guarantee data consistency across the full lifetime of the execution;

Note. Static memory is a form of ROM that is execution independent.