Virtual machine¶

A virtual machine is a specific way to represent functions, uniquely defined by three functions encode, decode, and evaluate. The protocol uses virtual machines in several places:

• wherever we need canonical commitments to and evaluatable representations of functions, such as external identities
• in the resource machine, for resource logics
• in the resource machine, for transaction functions
• in application definitions, for projection functions

In general, the protocol does not require the same virtual machine to be used in all of these places, or even a specific virtual machine to be used in a specific place. However, agents who wish to interoperate must agree on the definitions of the virtual machines which they are using, and different virtual machines may have different performance characteristics in different contexts. In order to facilitate interoperability, the protocol standardizes a multiformat of virtual machines, where each virtual machine is associated with a unique natural number. We will refer to the virtual machine associated with \(n\) as \(VM_n\), and associated functions as \(encode_n\), \(decode_n\), and \(evaluate_n\). Each virtual machine, in the implementation language, also comes with an opaque internal representation type \(VM_n.t\).

Decoding¶

The decoding function \(decode_n\) attempts to decode a DataValue into an internal representation \(VM_n.t\). Decoding which encounters a FunctionV associated with a different virtual machine will simply represent that as data (instead of code) in the internal representation type.

type Decode = DataValue -> Maybe VM_n.t

Encoding¶

The encoding function \(encode_n\) encodes an internal representation of a function and/or data into a DataValue. Functions in the internal representation will be serialized in some fashion and paired with the natural number associated with the virtual machine in a FunctionV.

type Encode = VM_n.t -> DataValue

Properties¶

The encoding and decoding functions must be inverses of each other, in that:

• decoding an encoded value will result in Just <that value>
• encoding a decoded value will result in the original internal representation

Evaluation¶

The evaluation function \(evaluate_n\) calls a function (in the internal representation) on the provided list of arguments (in the original representation). Evaluation must be deterministic. Evaluation must also meter gas, a measure of compute and memory resource expenditure. Different virtual machines will have different gas scales. Evaluation takes a gas limit. During VM internal execution, gas must be tracked, and evaluation must terminate if the gas limit is exceeded. Should execution complete successfully within the gas limit, the VM must return the gas actually used.

type Evaluate =
  VM_n.t ->
  [VM_n.t] ->
  Natural ->
  (Maybe VM_n.t, Natural)

Provable virtual machines¶

A provable virtual machine is a virtual machine with a proof type \(P_n\) and two additional functions parameterized over \(P_n\), \(prove_n\) and \(verify_n\).

Proving¶

The proving function \(prove_n\) generates a proof for a given program (logical relation), public input, and private input.

type Prove =
  VM_n.t (T0 -> T1 -> boolean) ->
  VM_n.t (T0) ->
  VM_n.t (T1) ->
  P_n

Verification¶

The verification function \(verify_n\) verifies a proof for a given program and public input.

type Verify =
  VM_n.t (T0 -> T1 -> boolean) ->
  VM_n.t (T1) ->
  P_n ->
  boolean

Properties¶

These functions must be sound and complete, in that:

• valid proofs can only be created for valid inputs (soundness), and a valid proof can be created for any valid input (completeness)
• i.e. verify f public proof = true if and only if proof = prove f public' private' where public = public' and evaluate f [public', private'] g = (true, _) for some sufficient gas limit g (we could probably split evaluation into gassy and gassless versions)

Should P_n not reveal any information about VM_n.t (T0), the provable virtual machine can be said to be zero-knowledge.