Models of computation: selection criteria and candidates

Protocol Design
1

Although it is not required for architectural correctness, or, in principle, protocol adherence, Anoma needs to select a model of computation to standardize on for pragmatic purposes.

Basic assumptions

  • We assume that differences in “physical” computational primitives and costs thereof can be modeled as a set of different finite fields, each with bounded constant costs for operations in the field.
  • We assume a boundable, known, monotonically increasing cost of nonlocality of reference (ref).

Requirements

This model of computation will be used for, at minimum, transaction execution:

  • Post-ordering computation performed by validators to compute final transactions
  • Local computation performed by the interaction engine to compose partial transactions

Both of these computations are of type PTX \to PTX (see here).

These uses impose some requirements; in particular:

  • Individual, metered operations (~ instructions, rewrite rules, etc.) must be bounded-constant-cost in space and time (otherwise the cost accounting itself becomes too complex and computationally expensive).
  • The model must be sufficiently expressive to handle runtime reflection and evaluation.

Additional possible uses

  • Could be used for known solver algorithms for which bleeding-edge efficiency (which will never be possible with metered computation) is not critical.
  • With the appropriate VM, could be used as an actual computational substrate for Typhon in the future, if conducive.

Bonus properties

Execution segment transformation

Ideally, the model would have an efficient bidirectional transformation to and from execution segments for verification.

Concurrency

Ideally, the model would be able to represent concurrent computations, parts of which could be evaluated in parallel. This should be reflect in the cost model (perhaps by partitioning a program into parallel segments in a DAG, which seems like a similar problem to execution segmentation).

Candidates

(WIP)

  • “NockFF” (Nock with finite fields)
  • “NockDAG” (Nock with DAGs instead of binary trees)
  • “PolyObject” (Prototype-based object systems with internal polynomial logic, probably has a stack)
1 Like
2

Additionally, the computational model must be deterministic. This renders concurrent models rather tricky, at least without proofs of equivalence of different orderings of execution, as we would have to enforce a specific, a priori execution order amongst the parallel processors, which I imagine would come with very high overhead costs (it’s basically running consensus). For this reason, I’m tempted to save such complexity for later, especially as the existing concurrency provided by Typhon’s execution environment already provides most of the benefits.

Operations which need to be available to the term in partial transactions:

  • RESOURCES_BY_INDEX { index_function }
    Reads resources in the history at execution time by the specified index function. Typically, the index functions allowed will be very restricted, e.g. current unspent resources of a particular kind. (this is used e.g. to increment counters post-ordering without conflicts)
  • READ_STORAGE { content_address }
    Reads the global content-addressed storage at the specified address. Storage not accessible to the machine accessing will be treated as non-existent.
  • WRITE_STORAGE { data } { deletion_criterion }
    Writes the content-addressed storage locally, on whatever machine is executing. The deletion criterion is a predicate that describes when the data can be deleted - e.g. after a certain period of time (local clock), after a signature by another party, etc. Typically, the deletion functions allowed will be very restricted, e.g. within a certain time bound only.
  • CONSUME_RESOURCE { resource_address }
    Consumes the resource at the specified address, adding it to the input resource nullifier set.
  • CREATE_RESOURCE { resource_data }
    Creates a new resource with the provided data, adding it to the output resource commitment set.

@mariari has also convinced me that the stack machine should probably have memory, since otherwise location-independent addressing is not possible. Probably memory would look something like:

  • READ_MEMORY { address }
  • WRITE_MEMORY { address } { value }
  • ALLOC_MEMORY { size }

As far as I can figure, post-ordering execution should not need to read any extradata, since any extradata which would have been read can just be inlined in the term anyways. Extradata only exists to make data available that resource logics might need to check (e.g. signatures) and could probably be understood as equivalent to transaction-time-local storage.

3

Additional notes:

  • For determinism, the requirement of execution halting as soon as the gas limit has been exceeded can be relaxed a little bit - it merely needs to be the case that execution fails if the gas limit is exceeded in the end - local processing could exceed the gas limit for awhile if it’s cheaper to overshoot slightly than to synchronize all of the time. I don’t think this helps too much, since the primary problem with concurrent execution is potential non-determinism, but it’s worth noting.
  • We’ll need PACK / UNPACK operations for all pairs of finite field types.
  • Would be nice to choose bytecode assignments with some canonical ordering of the set of all finite fields.
    • This could be prime, then power, then operation.
  • A subset of this VM should be equivalent to the “JoeVM” (Sketch of a possible VampIR VM - #15), where segments correspond to sequences of stack operations in between control flow instructions.
4

Additional instructions we should probably have:

  • EXECUTING_IDENTITY - returns the external identity of the executing party
  • GAS_REMAINING
5

OK; after some consideration, I propose - for now - “NockFF+”. NockFF+ (name TBD) is, roughly:

  • Nock, with
  • Primitive operations for arbitrary finite fields, some subset of which may be supported by any particular interpreter, and
  • Additional opcodes for storage and resource I/O

Finite field operations and indexing

Take the set of all finite fields F. Each finite field F_n, with n the order, has:

  • Additive identity: 0_{F_n}, with type F_n
  • Addition: +_{F_n}, with type F_n \to F_n \to F_n
  • Additive inverse: -_{F_n}, with type F_n \to F_n
  • Multiplicative identity: 1_{F_n}, with type F_n
  • Multiplication: *_{F_n}, with type F_n \to F_n \to F_n
  • Equality: =_{F_n}, with type F_n \to F_n \to F_2.

We also assume a family of conversion functions conv_{i, j}:

  • conv_{i, j} with type F_i \to F_j if i \le j
  • conv_{i, j} with type F_i \to (F_j, F_2) if i \gt j, where the bit in the return value indicates whether or not the conversion overflowed

In general, F_n is the finite field of order n. For example:

  • F_2 is the smallest finite field, with only two elements. (binary field, 1-bit).
  • F_{2^{32}} is the finite field with 2^{32} elements, i.e. uint32.
  • F_{2^{256}} is the finite field with 2^{256} elements, i.e. uint256 as used in Ethereum.

As actually indexing finite fields by their orders would not be space efficient, we instead index by prime, followed by power (e.g. (2, 1), (2, 32), (2, 256) for the examples above).

We then index the operations as above from 0 through 5, resulting in a final table as following:

1 2 3 4 OP
p k 0 0 0_{F_{p^k}}
p k 0 1 +_{F_{p^k}}
p k 0 2 -_{F_{p^k}}
p k 0 3 1_{F_{p^k}}
p k 0 4 *_{F_{p^k}}
p k 0 5 =_{F_{p^k}}
p_1 k_1 p_2 k_2 conv_{{p_1}^{k_1}, {p_2}^{k^2}}

As the space of potential primes p and powers k is infinite, we then map this to a known finite field F_h with a hash function hash, and use e.g. hash(p, k, 0, 0) as the opcode.

Storage and resource I/O operations

  • RESOURCES_BY_INDEX { index_function }
    Reads resources in the history at execution time by the specified index function. Typically, the index functions allowed will be very restricted, e.g. current unspent resources of a particular kind. (this is used e.g. to increment counters post-ordering without conflicts)
  • READ_STORAGE { content_address of type F_h }
    Reads the global content-addressed storage at the specified address. Storage not accessible to the machine accessing will be treated as non-existent.
  • WRITE_STORAGE { data } { deletion_criterion }
    Writes the content-addressed storage locally, on whatever machine is executing. The deletion criterion is a predicate that describes when the data can be deleted - e.g. after a certain period of time (local clock), after a signature by another party, etc. Typically, the deletion functions allowed will be very restricted, e.g. within a certain time bound only.
  • CONSUME_RESOURCE { resource_address }
    Consumes the resource at the specified address, adding it to the input resource nullifier set.
  • CREATE_RESOURCE { resource_data }
    Creates a new resource with the provided data, adding it to the output resource commitment set.

Cost functions

  • Finite field operations have specific fixed costs set per field
  • Simple Nock opcodes have fixed costs
  • Tree indexing and modification have costs proportional to the number of branch traversals in the tree access
  • Memory copying (including evaluation) - ?

My primary question right now is around the cost semantics for memory copying, which happens exclusively (?) with 2, Nock’s evaluation instruction. It would certainly be safe to charge proportional to the size of the noun copied. I wonder if this would be wildly impractical, though, since it seems like using Nock will require e.g. basically copying around the standard library into everything. @ray @mariari curious for your thoughts here - this is the main concern I have remaining about using Nock in this way.

6

Notes from discussions with @ray @terence:

  • Asssume copy-on-write memory model
  • Charge for each cons (allocation)
  • Charge for memory modifications (# operator), as this induces a copy
  • Rings, not just finite fields
    • Operations polymorphic in n (integers mod n) or the order (finite fields)
      e.g.
op {0 | 1 indicating integers mod n or finite field of order n} n [operands ... ]
  • I/O should probably be opcodes (in a separate section) since they take/return values.