ZORP

Proving meaningful computations using the Eden zkVM

09/06/23 | Yaseen Shaikh

Welcome! In this blog post, we’ll be expanding more details on how to use the Eden zkVM and associated tools. We assume you have a working verifier agent already set up, so please take a look at the previous post if you haven’t already.

Proving practical programs

Wouldn’t it be kinda neat if we could prove something slightly cooler than a simple eden formula like [42 [4 0 1]]? Let’s try our hand at writing and proving a real high-level program using Eden.

Luckily, we’ve made the first part easy for you; we’ll be using a pre-written program that has been made available in the repo you had cloned earlier. The program can be found at lib/jet-test.hoon.

We’ve reproduced its source below:

|=  a=@
::  pk from https://github.com/urbit/urbit/blob/d52826e570/tests/sys/zuse/crypto/secp256k1.hoon#L119
=.  a  (div (mul a 2) (neg (neg 1)))
=/  sk=bignum  [%bignum %| 0x3]
=/  pk=bignum  [%bignum %| 0xf930.8a01.9258.c310.4934.4f85.f89d.5229.b531.c845.836f.99b0.8601.f113.bce0.36f9]
=/  msg        [%bignum %| 'hello']
=/  aux        [%bignum %| 0]
=/  sig  (schnorr-sign sk msg aux)
=/  success
  (schnorr-verify pk msg sig)
[success a]

This program represents something way more interesting: signing and verifying a message using Schnorr signatures. For the especially proactive, you’ll have noticed that we make use of arms that don’t seem to exist. The reason this still works is that our code will be compiled automatically against our custom standard library, flib, in the following steps.

To prove a run of this program, we’ll need to introduce a new tool: the -build-eden thread. This thread accepts a path to a file containing a gate to be run inside the Eden zkVM, and a vase of the input to slam it with.

Here’s how we’d compile the code to run the gate with an input of 100:

=jet-test -zkvm!build-eden /=zkvm=/lib/jet-test/hoon !>(100)

And then to prove it, all we have to do is run the following:

=vr -zkvm!prove-eden jet-test

This is a much bigger program, which means more work for the prover, so be sure to give it a minute before checking back.

If all went well, we can inspect the result by typing vr into the dojo like we did last time. Since the code is a lot bigger this time, we’ll instead use an actual equality check rather than visually comparing the formulas.

Here’s a handy snippet to make checking out the proof a bit easier:

valid:(need vr)
=(code:(need vr) jet-test)

If both of those produce %.y then it means everything worked out. Hopefully by now you’ve gotten a flavor of how to work with the system.

Differences between the Nock VM and the Eden zkVM

ZKVMs naturally impart various restrictions and limitations on the computational model that they support in order to make generating proofs possible, such as on program size or on the amount of addressable memory. In the Nock VM and Eden zkVM, the notion of manipulating linear blocks of unstructured memory is replaced with structured tree manipulation, but in a moment see how similar limitations translate to our paradigm.

One key point to note is that even though we are compiling source code that has the .hoon file extension, the compiled code ultimately targets the Eden zkVM and not the Nock VM. This means that our programs have fundamentally different semantics than standard hoon programs, even though they may overlap heavily in their behavior.

Here we outline the key distinctions between the Nock VM and the Eden zkVM:

  • Atoms @ are defined to be field elements—that is, all natural numbers under \(p = 2^{64} - 2^{32} + 1\), our field’s order—rather than arbitrary size integers
  • Increment (Eden %4) is defined in terms of finite field increment, which wraps back to \(0\) when hitting the maximum atom value.
  • Axis lookup (Eden %0) uses atoms and is thus not immune to the size limit, which implies a limit on the maximum depth that can be addressed on a given noun1

Disclaimer

While proof-making can be a lot of fun, we must stress to the reader that the current release of our software suite is in alpha and as such, does not provide any cryptographic guarantees. Don’t go securing your power grid with it just yet. Since this is an early-access release, we expect bugs and prover downtime (planned and unplanned) as we see increased usage and make upgrades to the system.

If something does come up, please feel free to use the issue tracker, and we’ll do our best to help out.

2