program_to_be_proven
is nested inside as input to the zkVM
program_to_be_proven
directly as the guest program? However, this level of indirection unlocks powerful capabilities that significantly expand the utility of the zkVM.
Stwo
prover used here is transparent).Enum
of the possible Term
s available: an indexed Var
, a Lambda
function definition, and an Apply
function application, as well as some useful trait implementations for constructing and debugging. In the rest of the library, we’ll define full expressions in the calculus, which amount to programs that are “executed” via reduction.
step
and iterative eval
routines that reduce the statement into a stable form.
In order to make our common library work across both the host and guest, we have a few quick steps we need to handle. First, we need to update the guest crate to depend on serde
, which the library uses for serializing and deserializing the Expr
structs to and from the zkVM:
Expr
is a program in the lambda calculus, we can now implement our (dead simple) interpreter — for simplicity, we omit any hash-based consistency checking: