Interleaving proofs ideas

[ecioppettini]

Interleaving proofs guided by communication through IS and FS

NOTE: This is a draft. I'm probably going to change multiple things (especially as
I'm still reading the Coral paper), but feel free to quote and comment.

The TLDR is basically that I think we can verify a Starstream utxo aggregation
trace with just proving memory splicings and concatenations.

Background

Let's assume that we have a zkVM that works with a memory, with a nebula-like
memory argument (e.g. zkEngine).

This means we can generate proofs of the correct computation with the following
inputs and outputs:

input:
(pc = program counter, sp = stack pointer, IS = initial memory, P = a wasm program)

output:
(pc, sp, FS = final memory)

So, let's say we want to prove that 2 + 3 = 5 (who would believe it otherwise).

We could encode the computation as a wasm program, like:

(module
  (memory (export "memory") 1)
  (func (export "add") 
    ;; Load value from address 3
    i32.const 3
    i32.load
    ;; Load value from address 4
    i32.const 4
    i32.load
    ;; Add the two values
    i32.add
    ;; Store the result at address 5
    i32.const 5
    i32.store
  )
)

Then we initialize a memory with

IS: [0, 0, 0, 2, 2, 0]

And we use the zkVM to generate the proof.

The verifier now can check that the proof was generated with the initial memory
it expected (the prover has to commit to it), and then it knows that the result
should be at FS[5].

The rest of the memory could be used for state needed in the computation (a
coroutine frame), or other private information.

Chaining

What about proving a chain of 2 different computations?

We would have:

Proof_0 := F( pc, sp, IS_0, P_0 ) == FS_0
Proof_1 := F( pc, sp, IS_1, P_1 ) == FS_1

Then to verify the chaning we can assert that:

verify(Proof_0, IS_0) && verify(Proof_1, IS_1) && IS_1 == FS_0

But of course this only works if the memory layout is the same.

What if we just want to inject the result, instead of any auxiliary memory or
state used by the computation?

We would need to assert that:

  verify(Proof_0, IS_0) &&
  verify(Proof_1, IS_1) &&
  IS_1 == IS_state_p1[0..j] <> FS_0[i..i+n] <> IS_state_p1[j+n..]

Where IS_state_p1 is the previous state of this program (a previous FS,
for example).

Starstream

In the context of Starstream, the IS_state_p1 would be the current coroutine
frame of a utxo, or a coordination script. And the interleaving operation would
be equivalent to injecting an external slice of memory into it before resuming.

Since we need to do the verification outlined above in a circuit, we need mostly
2 things:

A way to compute FS[i..i+n].

There is a more or less straight-forward way of doing this already. Since the
zkVM needs to compute multiset hashes to IS and FS and commit to them.

Multiset hashes are associative, so we could split them into 3 parts.

H(FS) = H(FS_0) * H(FS_1) * H(FS_2).

Then in our verifier function can assert that

H(IS) = H(IS_1) * H(FS_1) * H(IS_2).

The issue with this is that it doesn't prove that the splices are done at the
right indexes. So most likely we need to compute H(FS_1) in the circuit too,
and prove that the addresses are in the right range (reminder: the IS is a
multiset of pairs (address, value, timestamp)). This shouldn't be a big issue,
since the same kind of computation needs to be done anyway for the mcc, although
whether there is a way of re-using work is still unclear to me.

There may be also another way of doing this check with some other type of
commitment.

TODO: there is something like this mentioned in this paper:

"Coral: Fast Succinct Non-Interactive Zero-Knowledge CFG Proofs"

Quoting:

Persistent memory.
In Appendix D.1 we discuss the construction of Split Witness Relaxed R1CS,
which makes it straightforward to share segmented/incremental memory between
different proofs. Essentially, one can commit to any segment of IS or FS (or
their entirety) separately, and then incrementally and verifiably access that
segment across proofs.

A way to encode a verifier for the auxiliary (wasm) VM as part of the aggregator step function.

If we want a single proof, we need to also verify the wasm VM as part of
this consistency check. This should be doable, since this is how the Nebula
implementation in zkEngine works for example, so the code can be adapted from
that.

Essentially we could just extend the aggregator snark with it's own shared
memory and add the segmentation checks.

A few potential issues:

1. If we need to do other operations, not sure how easy it is to make that
   adaptable to the switchboard approach.

2. If we want to use https://github.com/jkwoods/segmented_circuit_memory then it
   uses a different fork of Nova that doesn't seem to have that code (because they
   implemented nebula with a single layer).

NOTE: I think we probably could also just have 2 circuits if needed.

Transaction processing

To put the above together, the aggregation proof could work like this:

Both utxos and coordination scripts are just wasm programs. The only difference
is that coordination scripts are not persisted after the transaction ends, but
we also need a coroutine frame for them (that gets initialized empty).

First we just run Starstream in non zk mode.

From this we can capture

1. The utxos used as inputs.
2. The new utxos.
3. The utxos that ended.
4. The interleaving order (who yields to who).

This creates the structure of a Transaction.

From this information, we can build a trace of this shape:

utxo = utxo id | wasm program vk | pc | sp | IS | FS = (frame, next_program?) | proof

Each step basically has to run a snark verifier, by using as inputs:

1. The wasm program.
2. An initial memory composed of the previous FS for that utxo, plus whatever is injected as input.

Then we update the current FS for this utxo with a variable in the public
memory.

How do we know which data to inject?

We control the memory layouts of the programs. That means we can just have the
programs decide the flow. And we know it's correct because of the wasm proofs.

If we have a coordinator script as a wasm program, and it calls utxo.resume,
then it has to push the utxo id to the stack as an argument. We just need to
decompose the FS at that position to extract the data.

We can also have it communicate in the same way which memory range we need to
inject into the other program's memory.

We can then keep track of two variables in the linear memory:

1. current_program
2. next_program

In each folding step, we assert that the utxo we are verifying is
next_program. And we compose the new IS with

inject_output(memory[next_program], range_from, memory[current_program], range_to).

Then set current_program = next_program.

Since we can inject one piece of data at a time, we also don't need any control
flow in this machine, that gets decided by what the wasm programs communicate
through it's output (memory).

What about effect handlers?

Effect handlers work similar to utxo resuming. We can pass handler ids down
as inputs, and if a function defines a new handler, it just overrides that
parameter.

Then when yielding, the utxo (or coordinator script) explicitly communicates
what the next program would be, by writing to the stack who should handle the
effect, and with which data.

What about builtin effects?

I think it's the same thing. We can inject the current_program for example, if
a utxo wants to assert that is being called by a specific coordination script.

Ledger-specific data could be also in the initial memory.

What about normal yield?

If a utxo yields, it doesn't yield to a specific utxo.

In that case we set next_program = current_program to continue the
coordination script that resumed that utxo.

We also need to verify that the last witness in the trace is for a coordination
script that just returns nothing.

[SebastienGllmt]

Since we're modeling every utxo as an independent program that may run forever, we have to be careful about mapping the FS of program A as the IS of program B.

The IS of program B is the FS of the previous iteration of B, and the inputs to a function call to B is some external memory we lookup (and the coordination script proves these lookups properly were done correctly)

[ecioppettini]

The IS of program B is the FS of the previous iteration of B, and the inputs to a function call to B is some external memory we lookup (and the coordination script proves these lookups properly were done correctly)

But is there any practical distinction in that?

The utxo vm has to include this external memory in its IS anyway, since it has to read the values and prove that it did that correctly. The only potential difference (in Nebula) is that it doesn't need to compute the multiset hash of that external memory, and can just leave it to the verifier.

So at most we can say that: IS_B_curr = FS_B_prev U IS_external.

Assuming that the vm that we are using supports that kind of segmented memory of course.

Or was this comment just an extra clarification? Because I just don't see how you would have inputs that are not part of the IS in some way or another.

[ecioppettini]

Implementation plan/proposal

What follows is a more concrete task breakdown from the original message. It
also maybe addresses the comment above about the external memory.

Utxo VM

Setup

We have a wasm-based zkVM that we use for each utxo, and also for the
coordination script.

That zkVM supports host calls, which in wasm are just imported functions. The vm
obviously can't prove anything about the result of the host call, but it should
be able to constrain the memory that gets modified as a result.

The most basic constraint is the (wasm) stack constraint, since wasm functions
are statically typed. But we could also have an extra memory (multi-memory) that
gets used for the results if necessary.

** NOTE: ** The above is not a necessarily a hard requirement, but it's simpler
conceptually since we already decided on using wasm as the api.

Core idea

On top of the above primitive, we have the proof output (open) an incremental
commitment to the contents of each host call, both inputs and outputs, and which
function it is.

Ideally this can be implemented as part of the VM, but if needed it could also
be a part of the program opcodes, although that may require precompiles for the
cryptography needed for the commitment-scheme that we use.

For example, let's say we have the following contract:

utxo SomeUtxo {
  main {
    let x = yield 10; // previous 'output'

    let x = yield 15;
  }
}

script {
  fn main(utxo: SomeUtxo) {
    let y = utxo.output();    

    assert(y == 10);

    let x = utxo.resume((3, 4));

    assert(x == 15);
  }
}

We first run the program to get the transcripts. When we do that, we start by
running the coordination script.

To perform the resume operation, the program calls an imported function:
starstream_resume. This requires pushing the arguments to the stack, and then
calling the function.

NOTE: We don't necessarily need to care about the name of the imported
function, or its order, we could use an argument to id the operation.

When we fold the instructions required for that, we could compute a commitment
to: STARSTREAM_RESUME || utxo_id=42 || inputs=[(2, 3)] || outputs=[15].
For the commitment we can just use a hash chain, since we'll only open it in the
same order.

For simplicify, we can split yield into 2 functions. One that has inputs and
no outputs, and another one with no inputs and only outputs.

When a utxo yields at the end of a transaction, it calls the first one. Then on
resume it uses the next one to get the resume argument.

This way functions always are atomic per proof (since the machine state doesn't
change in the middle of the host call witnesses). There is most likely a way of
removing this limitation if needed.

After running both programs, and generating both proofs (1 per program), we can
export the interleaved version of the host call transcript.

STARSTREAM_UTXO_GET     || utxo_id || inputs=[]        || outputs=[10]
STARSTREAM_RESUME       || utxo_id || inputs=[(2, 3)]  || outputs=[15]
STARSTREAM_YIELD_RESUME            || inputs=[]        || outputs=[(2, 3)] 
STARSTREAM_YIELD_PUT               || inputs=[15]      || outputs=[] 

Then we can fold over these new witnesses to produce the interleaving proof.

The step function/circuit should work like this:

1. We have a memory with one variable per utxo in the transaction. We use that
   to re-compute the commitments.
2. We keep current_program and next_program variables. current_program
   starts with the coordination script id.
3. If we see a resume(program_id), then we set the next_program to that
   program's id.
4. If we see a yield, then we set next_program to the current coordination
   script. Since we use current_program to decide which commitment to increment,
   the yield has to be from the right program, or the commits won't match.

To fold STARSTREAM_RESUME: We just store the values into the coordination
script's input and output variables.

To fold STARSTREAM_YIELD_RESUME we need to match the output with the last
STARSTREAM_RESUME input.

To fold STARSTREAM_YIELD_PUT we match the input with the last
STARSTREAM_RESUME output. We also store the input as the output in a
continuation table (we can keep only one row per utxo).

We then use this table to fold STARSTREAM_UTXO_GET, which just reads this
value. (do we want this to be read only once?).

Verification

When we finish folding the previous scheme, we end up with:

1. A single interleaving proof.
2. One proof per utxo. *NOTE: * This way we can do offline memory checking only
   once per utxo, per tx, instead of having to initialize and finalize once per
   yield.

A verifier would need to:

a) Verify all the utxo proofs. Extracting the communication transcript
commitments. We also need to check that the IS matches what's in the
continuation table, and the FS too. NOTE: If using Nebula with public-coin
multiset hashing, the IS and FS are different for each proof, the verifier would
have to compute these each time.
b) Verify the interleaving proof. And check that the commitments match.

If we want to end up with a single proof, the above has to be implemented
as another operation in the step function above. We can use the switchboard
construction for this. Then at the end of the transcript we have one
verification step per utxo used in the transaction.

The hard part here is mostly implementing this verifier.

Folding multiple transactions

The main issue with folding multiple transactions is that offline memory
checking requires finalizing (and initializing?) all the memory per proof. This
is fine for the utxo set used in the transaction, but for the entire ledger's
utxo set it may not scale.

A potential solution is a hybrid schema, where we use some online memory
argument (merkle trees/verkle trees?) to ininitialize a small operational
memory. Basically we just open commitments to the utxos that we need, and put
those in some RAM abstraction.

Otherwise the rest would be the same.

Effect handlers

The current implementation of algebraic effect handlers is built on top of
closures. The problem with this scheme is that there is not really a notion of
shared memory.

There are generally two ways we can implement effect handlers then:

---

1. We have some operation to create shared memory. Something like
   STARSTREAM_SHARE. This returns a handle to some object that should only live
   for the current transaction. Then a handler could access the variables it needs
   by calling some STARSTREAM_GET and STARSTREAM_PUT.

This approach doesn't work for utxos though, since they will want to keep the
memory shared across transactions.

Although in that case we can make the utxo storage shared. This has some
overhead but it may work.

---

2. We resume with a tag. This works better for utxos, since there is only one
   point where we can resume, and they have a unique address.

The problem is that with coordination scripts we can't just resume to the point
where the handler was defined.

We'd need to either: resume to the last call, and then unwind the stack until
the handler is found. Probably by keeping track of a continuation to resume.

Or by using stackless coroutines to rewind stack again.

---

We can also use both options. One for utxos and the other for coordination
script handlers. Which do have some differences anyway.

Channels

Channels follow quite naturally, since this scheme is basically describing
channels anyway, with a pair of channels per utxo (one for input and one for
output).

The only thing that would potentially change is the order of the interleaving.

Tokens

For tokens we need:

• STARSTREAM_MINT
• STARSTREAM_BIND
• STARSTREAM_UNBIND
• STARSTREAM_BURN

Mint allocates a new token descriptor. The token descriptor is bound to the
programs for bind and unbind.

When a utxo calls STARSTREAM_BIND or STARSTREAM_UNBIND, we know what's the
next_program from the token descriptor.

The only extra thing we need to keep track is the utxo's program, so that we can
resume it afterwards.

Task breakdown

1. - Implement the interleaving proof machine with an untrusted communication
   transcript, and by using some zk memory abstraction. Do yield and resume first.
2. - Either make zkEngine generate the host call commitments, or use a custom
   VM. Whatever is quicker.
3. - Use the above for a sandbox demo of resuming something like
   PayToPublicKeyHash. This would be 3 proofs (1 utxo, 1 coordination script,
   interleaving proof).
4. - Implement the operations for utxo's effect handlers. This would maybe
   require changes in the compiler.
5. - Implement the folding verifier for the utxo zkvm. And integrate it with
   the interleaving circuit to get a single proof.
6. - Implement the effect handlers in coordination scripts (some form of
   shared memory).
7. - Implement the token operations.
8. - Folding multiple transactions.