The aim of this post is to describe a “minimum viable abstract VM” which does everything that we require. This could also be understood as an abstract interface specification for Taiga.
Basics
Fix a finite field F, with:
- Multiplication: *_F, with type F \to F \to F
- Addition: +_F, with type F \to F \to F
- Additive identity: 0_F, with type F
- Multiplicative identity: 1_F, with type F
- Additive inverse: -_F, with type F \to F
- Equality: =_F, with type F \to F \to {0 | 1}
Fix an abstract (possibly infinite) program field P, with:
- Multiplication: *_P, with type P \to P \to P
- Addition: +_P, with type P \to P \to P
- Additive identity: 0_P, with type P
- Multiplicative identity: 1_P, with type P
- Additive inverse: -_P, with type P \to P
- Comparison: <_P (less than, exclusive), with type P \to P \to {0 | 1}
Fix an abstract proving system with two functions:
- Prove(C, x, w) ⟶ π
- Verify(C, x, π) ⟶ { 0 | 1}
We say that this proving system is zero-knowledge if from π the verifier learns nothing of w.
(we will omit preprocessing for the sake of simplicity)
Fix a hash function H, with type P \to F, such that:
- H is non-invertible, in that a computationally bounded adversary cannot compute the preimage from the output
- H is collision-resistant, in that a computationally bounded adversary cannot feasibly find two preimages with the same output
Programs
Now, we will define programs.
Programs PROG are extended multivariate polynomials over a_0 ... a_n \in P in canonical form, with designated variable b, for example:
We extend these polynomials with control flow and reflection.
First, let’s introduce the control flow primitives: comparison and branching.
Comparison is lt(a, b), where:
- lt(a, b) = 0 if a <_P b
- lt(a, b) = 1 otherwise
Branching is branch(a, b, c), with type P \to P \to P \to P, where:
- branch(0_P, b, \_) = b
- branch(1_P, \_, c) = c
- branch(\_, \_, \_) = undefined
Thus, for example,
is a valid program.
Assuming that a \in {0, 1}, branch(a, b, c) is semantically equivalent to ((1 - a) *_P b) + (a *_P c), so we aren’t changing the expressive power here, just adding explicit information about control flow.
Second, let’s introduce reflection:
- reflect_P, with type P \to PROG
- repr_P, with type PROG \to P
- eval_P, with type PROG \to P {...} \to P, where the arity depends on PROG
Argument order corresponds to numbering of a_0 ... a_n.
Thus, for example,
is a valid program, and so is
The behavior of applying eval_P with the wrong number of arguments is undefined.
Note, in particular, that we can freely swap a subprogram PROG with eval_P(reflect_P(repr_P(PROG))), where repr_P(PROG) can be calculated at compile-time, and thus “defer compilation”.
Circuit transformation
Programs may be transformed to a circuit, by:
- factoring the polynomial
- ordering the factors in canonical form
- transforming to a circuit DAG
Stack machine compilation
The circuit DAG may then be compiled to a sequential stack machine in the standard manner. For example, define the stack machine state as (pc, ins, data), with:
- pc the program counter
- ins the instruction sequence
- data the data stack
Stack machine operations:
- PUSH a
- NEG
- ADD
- MUL
- COMPARE
- BRANCH pc_1 pc_2
- REPR
- REFLECT
- EVAL
TODO: Figure out any stack consistency issues on branching.
Resources
Define a resource R as a seven-tuple (PROG, P, F, P, F, F, 0 | 1) with fields named as follows:
- R_{logic} of type PROG
- R_{label} of type P
- R_{quantity} of type F
- R_{value} of type P
- R_{nonce} of type F
- R_{nc} of type F (“nullifier commitment”)
- R_{ephemerality} of type { 0_P | 1_P }
Resources with R_{ephemerality} = 0_P are known as ephemeral, while resources with R_{ephemerality} = 1_P are known as persistent.
TODO: Same as the commitment for now.
Define the commitment of a resource R_{commitment} as hash(R).
Define the address of a resource R_{address} as R_{commitment}.
Define the nullifier of a resource R_{nullifier} as n such that hash(n) = R_{nc}.
Define the type of a resource R_{type} as hash(R_{logic}, R_{label}).
Define the delta of a resource R_{delta} as the two-tuple (R_{type}, R_{quantity}).
Partial transactions
Define a partial transaction PTX as a six-tuple (Set\ F, Set\ F, Set\ π, D, Set\ P, PROG) with fields named as follows:
- PTX_{created} of type Set\ F (commitments to newly created resources)
- PTX_{consumed} of type Set\ F (nullifiers for consumed resources)
- PTX_{proofs} of type Set\ π (proofs for consumed and created resources)
- PTX_{delta} of type Set (F, F) (as resource delta above)
- PTX_{extradata} of type Set\ P (extradata possibly used as input by proofs)
- PTX_{executable} of type PROG (possibly empty)
A partial transaction is valid w.r.t. a past commitment set CS if and only if:
- For each commitment c in PTX_{created}, a valid proof π is included in PTX_{proofs} such that, for some resource R with R_{commitment} = c,
- Verify(R_{logic}, (in, out, extradata, 1), π) = 1, with in \subset PTX_{consumed}, out \subset PTX_{created}, extradata \subset PTX_{extradata}.
- For each nullifier n in PTX_{consumed}, a valid proof π is included in PTX_{proofs} such that, for some resource R with R_{nullifier} = n and R_{commitment} \in CS.
- Verify(R_{logic}, (in, out, extradata, 0), π) = 1, with in \subset PTX_{consumed}, out \subset PTX_{created}, extradata \subset PTX_{extradata}.
- PTX_{delta} = \sum_{R \in PTX_{consumed}} R_{delta} - \sum_{R \in PTX_{created}} R_{delta}
A partial transaction is balanced if and only if PTX_{delta} = 0.
A partial transaction may be executed by running PROG, which may additionally:
- read resources by R_{address}
- read from and add to PTX_{extradata}
- add to PTX_{created} (altering PTX_{delta})
- add to PTX_{consumed} (altering PTX_{delta})
Partial transactions may be composed either sequentially or concurrently, where sequential composition uses the output commitment set as input to the next transaction, and concurrent composition does not. In both cases, nullifier sets may not conflict.
Recursion
Abstractly, recursion may be achieved as follows: define a resource R with:
- R_{label} set to the consensus provider identity
- R_{quantity} set to 1
- R_{value} set to the commitment and nullifier trees
- R_{nonce} an incrementing counter
- R_{nc} = hash(0_F)
- R_{ephemerality} = 1
- R_{logic} = verify\_partial\_tx\ \&\&\ verify\_signature where the partial tx is checked with respect to the input and output commitment and nullifier sets in R_{value} and the signature is checked with respect to the consensus provider identity in R_{label}.