Encoding a program's execution

[terse timber]

Hey friends, first off, I'm not sure if I'm asking the right question so please clarify if i'm off base, but what would be an efficient way to encode a program's execution into a zkApp/zkProgram? For example, let's say we have a program that compiles down to assembly and has 10 instructions, how would I go about putting that into a smart contract?

Currently working on zkBUIDL Bounties: https://github.com/Devtonite/onchain-zkbuidl

Oh, also, this question is assuming there's another way to do this without building the entire compiler with o1js

Of course, doing that, we'd be able to prove any computation, but i'm more looking for a way to verify a user correctly ran a solution against a unit test and did not just make up a result for during their run

[late mantle]

Hello @terse timber. If I have understood your question correctly, you are trying to verify a ZkProgram's execution result inside a smart contract method. Am I right? If this is the case, you can put the proof of your ZKProgram as an argument to your smart contract. Then, inside your smart contract you can verify the proof (by simply calling .verify() and use publicOutput's of the ZKProgram to perform your computation. ZKPrograms can also have recursion (actually that is the most important reason why we have them), so you can have any off chain computation on your client side, and then just send the final proof of execution to the smart contract to use computation results inside your smart contract trustlessly. Please see this link for more information: https://docs.minaprotocol.com/zkapps/o1js/recursion. I hope this solves your issue. If you meant something completely different, please let me know so I can help you 🙂

[terse timber]

@late mantle thank you. Yes I was initially looking at Zkprogram as well, I believe that's what I'll be using. But my question was something in the lines of "is there a way to prove some execution of a program in a different language (rust/solidity) without modeling the entire language's semantics in an o1js circuit"?

Basically, i'm building a zkapp that let's one submit a unit test with a token bounty, which can then be redeemed if you submit a proof of a correct solution to the unit test. In this scenario, what would be the most straightforward way to prove a user ran the unit test with the code solution correctly?

[stiff plover]

You don't want to model the semantics of a language, but the VM in which the compiled assembly runs in. Still you probably don't want to go into that in o1js.

[candid ether]

I know only about one project that can, in theory, do it - RISC ZERO. In practice, it will be veeeery slow or impossible.

If your program is an assembler with 10 instructions, there are a lot of xor, shift, etc. operations in o1js, so it would be easier to rewrite specific programs using o1js. Don't think that it is possible with rust/solidity.

[terse timber]

haha yeah that is indeed what i'm trying to avoid, so I was asking if there would/could be an alternative that achieves a similar result without doing all that

[terse timber]

yes, I was also considering using this if there isn't any other option. If i go with risc0, i would have to have a separate verifier program built on risc0 which would then interact with my o1js contracts. It's definitely AN approach...

[terse timber]

thoughts on encoding some of the characteristics of a foundry result into the zkprogram instead? for example, you can get a JSON file that represents how a test ran in foundry. would using some of the keys from that JSON and putting them into the zkprogram help with trying to prove a computation outside of o1js ran correctly?

[terse timber]

yeah, so basically a MINAxEVM type of thing lol. That would probably have to be it's own dedicated project.

[candid ether]

I think that it is a wise approach. You can ask the user to run the program with inputs that you provide or random inputs and give the result with inputs to o1js ZkProgram to prove that the result is correct. You should have, in this case, two equivalent programs, one in rust/solidity and the other in o1js TypeScript.

Basically, we are going with this design to one of the methods of the formal verifications of the program. There was a good review of those methods in ZK bootcamp - see page 23: