How prover convince verifier that it has indeed executed given program in a VM?

[vivekvpandya]

It seems like miden is doing some complex process https://0xpolygonmiden.github.io/miden-vm/design/decoder/main.html
But Risc0 seem to have different approach.

[vivekvpandya]

Since Risc0 uses ELF as input to the VM, it generates a cryptographic hash and verifier needs that hash to begin verification of the seal generated by Risc0 prover.

[vivekvpandya]

More details as per discussion with Risc0 discord

simple_user — Today at 10:22 AM
hello, I am comparing miden to Risc0 in certain aspects and want to clear some doubts. I see that miden is doing https://0xpolygonmiden.github.io/miden-vm/design/decoder/main.html to make sure that prover has indeed executed a given program for them its just taking hash of all Miden assmebly instructions and also doing some traces of decoding too.
however it seems Risc0 id doing something different, specially because it uses ELF format, AFAIU risc0 hashes ELF but it can be case that not all instruction in ELF get executed, also does risc0 also do traces and ZK for decoding of instructions too?
Program decoder - Polygon Miden VM
[10:22 AM]
kindly reply

@simple_user
hello, I am comparing miden to Risc0 in certain aspects and want to clear some doubts. I see that miden is doing https://0xpolygonmiden.github.io/miden-vm/design/decoder/main.html to make sure that prover has indeed executed a given program for them its just taking hash of all Miden assmebly instructions and also doing some traces of decoding too. however it seems Risc0 id doing something different, specially because it uses ELF format, AFAIU risc0 hashes ELF but it can be case that not all instruction in ELF get executed, also does risc0 also do traces and ZK for decoding of instructions too?

Frank Laub [RISC Zero] — Today at 11:14 AM
i will be giving a talk tomorrow about Continuations, and we'll discuss a bit about what the image_id is, which is basically a hash of a merkle tree, where every entry in the tree corresponds to a hash of a page in memory. What we did is verify that the initial image_id is what we expect it to be. When the user performs a verify of a receipt, the user must also specify the expected image_id. we can validate that a particular receipt came from the specified image_id. The initial memory state includes the ELF binary being loaded in, which would include the instructions and any static/constant data values.

simple_user — Today at 11:17 AM
Thanks @frank Laub [RISC Zero] ! So my question is that, it seems like Miden is proving that even decoding of source assembley has been done correctly https://0xpolygonmiden.github.io/miden-vm/design/decoder/main.html#decoder-trace and also I feel some other VM like Ola is also doing it. (I may be wrong )
and its not the case in Risc0 ?
Program decoder - Polygon Miden VM

@simple_user
Thanks @frank Laub [RISC Zero] ! So my question is that, it seems like Miden is proving that even decoding of source assembley has been done correctly https://0xpolygonmiden.github.io/miden-vm/design/decoder/main.html#decoder-trace and also I feel some other VM like Ola is also doing it. (I may be wrong ) and its not the case in Risc0 ?

Frank Laub [RISC Zero] — Today at 11:20 AM
The rv32im circuit that is the source for all of the constraints that go into the proving system includes rules for how to decode and execute a given rv32im instruction. every cycle performs:
fetch
decode
execute
store result(s)

thus we ensure that the entire program is executed properly

simple_user — Today at 11:21 AM
oh okay makes sense now
[11:21 AM]
image_id is separate thing

Frank Laub [RISC Zero] — Today at 11:21 AM
yes, the image_id is about the state of memory, the circuit itself is about the proper execution against that memory
[11:24 AM]
the circuit includes extra memory verification rules that uses plookup and a permutation argument to ensure that a memory access to a given address must follow certain rules. first read must match corresponding image_id, following read/writes must be consistent, and final write produces a new image_id

[vivekvpandya]

Based on this it seems that we also need to generate proof of decoding step at some-point in future.

[matthiasgoergens]

We can avoid that proof, if we disallow self-modifying code. See #107

Then we load the initial memory, decode all the instructions, and produce the hash of the program from that.

A user who wants to verify a proof can take the ELF file the prover claims to have executed, compute the hash with our program, and verify the program hash that the proof comes with against this result.