Proper abstraction of instruction sets / virtual machines

The objective of this topic is to discuss how to properly abstract specific virtual machines such as Nock, Cairo, and RISC0 in the Anoma specification. At the moment, a virtual machine, which we will take here as simply a way to represent arbitrary classically-computable functions, is required in a few places:

• in the protocol where 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, we do not need to use the same virtual machine in all of these places, or even a specific virtual machine for a specific place - we can support interoperability between multiple representations; we just need a way to demarcate what representation is in use so we can interpret data as the correct code.

In certain cases, however - such as external identities - we do need a way to understand when two representations are equal, i.e. extensional function equality - and to compute a canonical succinct commitment upon the basis of which equality will be judged, we do need a canonical representation for the preimage. It may be possible to work with a weaker notion (`commit a = commit b` entails `a = b`, but `a = b` does not necessarily entail `commit a = commit b`), and use runtime equality judgements (a la “signs for” and “reads for”, which we need anyways), I’m not sure yet.

First, however, what exactly is a virtual machine? Let’s try to capture a definition in math:

1. A virtual machine is an encoding of arbitrary classically-computable functions defined by two (type-parameterized) functions:
• `deserialise : bytes -> Maybe (Repr T)` which attempts to deserialise a bytestring into an internal representation of a function of type `T`.
• `serialise : Repr T -> bytes` which serialises an internal representation of a function of a type `T` into a bytestring.
• These functions must be inverses, i.e. `deserialise . serialise = Just . id`. and `fmap serialise . deserialise = id`.
2. An evaluatable virtual machine is a virtual machine with an additional function `evaluate : (Repr (T0 -> T1)) -> Repr T0 -> Repr T1`, which simply calls a function on the provided argument (in an internal representation). `evaluate` is required to be deterministic.
3. A provable virtual machine is a virtual machine with two additional functions parameterized over a proof type `P`:
• `prove : Repr (T0 -> T1 -> T2 -> boolean) -> Repr T0 -> Repr T1 -> P` generates a proof, where `Repr T0` is understood as the private input, and `Repr T1` as the public input.
• `verify : Repr (T0 -> T1 -> T2) -> Repr T1 -> P -> boolean` verifies a proof for a given program and public input.
• Should `P` not reveal any information about `Repr T0`, the provable virtual machine can be said to be zero-knowledge.

I think these definitions should be (roughly) sufficient for our purposes. They do not answer, for now, the question of how to convert between representations in a semantics-preserving way (i.e., compilation), which may be useful to introduce into the protocol structure in the future, but I think we do not need it yet.

Following this route, in the specs we would then define how each of Nock, Cairo, and RISC0 instantiate these types. Before doing that, I wanted to write this up and seek input from @vveiln @jonathan @degregat @mariari @Moonchild @ray .

1 Like

seems fine generally. mainly i think types is ‘the’ problem and other than that there is not much that can go wrong

presumably missing a ‘-> bool’ at the end?

not sure if an intentional omission but we should ideally have a way to limit gas/execution time

1 Like

Ah yes - fixed.

True, I will include this as well.

Are T2 and P here the same thing?

The definition is broad, but should it also require correctness and soundness properties for a provable vm (not necessarily zk vm)? It feels odd to talk about zero-knowledge without correctness and soundness implied

2 Likes

Ah, I miswrote the type, there should be a boolean - fixed.

Yes, the definition should include correctness and soundness properties.

2 Likes

This sounds like it falls into the domain of GEB, so once these problems are solved there, we should use GEB, or port over the needed formalism/approaches from it.

3 Likes

That is also my hope - cc @terence would you want to chime in here?

1 Like

Yes, that’s exactly right – indeed, one of the things which Geb will automatically provide is, given two specifications, a specification of what it means to translate between them in a semantics-preserving way: a universal-property-preserving functor between theories (where theories are defined as the universal properties they exhibit).

(It should also automatically provide executable specifications in the form of continuations – anything that you don’t implement is “implemented” in terms of a continuation which effectively means “what would/could happen if you implemented and executed this”.)

2 Likes

Thinking about this some more I realize that I’ve been assuming that virtual machines can typecheck their internal representations, which is not necessarily always going to be the case … - however, we need some way to encode how inputs are supposed to be passed to functions - `eval` should also be able to handle multiple inputs. Maybe some virtual machines will need the ability to fail if they return the wrong type. Also, we need to introduce the concept of “gas”.

Additional aspects to standardise here in evaluate:

• errors (out-of-gas, type-mismatch, etc…)
• logs (standard data representations)

Multiencode/multidecode:

Multiencode takes a value in internal representation and a set of preferences, and tries to encode it in a bytestring according to those preferences. To convert between virtual machine representations, this will require compilation (which will not be supported in all cases). Multiformat codes will be included to indicate which formats are in use.

Multidecode takes a value in bytestring representation and tries to decode it into internal representation, according to the multiformat information and the data encoding and virtual machine formats known by the decoding party. Attempting to decode unknown formats will result in an error.

In general, canonical commitments to data and code are made over the output of `multiencode`. `multiencode` is also used before storing data or sending it over the network. Any party should be able to take any piece of stored or sent data and a type and attempt to deserialise it with `multidecode`.

Open questions:

• Implicit FFI with multi-virtual-machine functions? Can we have a `multievaluate` ?
• Can VMs be passed functions from the environment? How will this work?
• Do we need both proof systems and provable virtual machines?

I think some additional “multi”-functions may make sense:

Multievaluation evaluates the application of a function to a value, where the function itself may return another application (perhaps with different virtual machine) to be further applied.

edit: it probably makes more sense for `multievaluate` to pass … a pointer to `multievaluate` to the VM, so that the VM can call `multievaluate` within itself, receive the response, and continue execution - more straightforward than CPS.

(we should think carefully about the types here…)

Multicompilation attempts to compile functions represented in a data value based on a set of preferences. Compilation will fail if unknown VM conversions are attempted.

We should also talk about the guarantees provided, e.g.:

• multiencode a = multiencode b → a = b
• multiencode a /= multiencode b does not imply a != b
• separate “evidence” type that a = b, which can include:
• multicompile (some preferences) a = b

This evidence type should carry a `Proof` (in the proof system sense), which could be of varying practical forms:

• replicating `multicompile` oneself
• trusting another’s run of `multicompile`
• succinct proof of computation correctness

The latter implies the ability to express compilation of one VM to another in terms of a “base” VM, which we (= everyone) knows how to verify proofs for.

I think actually all these types (`BasicValue`, `BasicType`, `Proof`, etc.) probably need to be defined with mutual recursion.

Notes to self:

• move the natural number multiformat basics to Basic Abstractions (but keep the specific lookup tables in Concrete Implementation)

A related question: how can virtual machines execute queries? I think we could build a sort of generic interface where VMs are passed a `query` function that implements this kind of functional namespace. That should be sufficient for pretty much everything. Queries will only make sense in certain contexts - e.g. in transaction functions, but not in resource logics - so we shouldn’t pass this function all the time, only in those contexts which make sense.

With `multievaluate`, we can have a version of this function that acts similarly to parts of the identity machine, and uses available evidence + preferences to use certain known-to-be-equivalent versions of functions (e.g. compiled versions) instead of others. Then “JIT” compilation can happen e.g. asychronously once certain statistical thresholds are met.

Optionally, this “smart multievaluate” can also use known proofs of the results of certain evaluations (instead of repeating the evaluations). If we want, we could even build a version that ships off some evaluations to a compute service provider (although this would usually be too-high-latency as opposed to some pre-coordination of the compute work split).