Desiderata for the AVM

Protocol Design
1

Preface

Designing a VM is no small task. A wide variety of different examples and design choices can be found in the literature, but none of them are likely to suit our context exactly – we need to pick and choose the pieces that make sense and assemble them together into a coherent whole. In order to know how to select the correct pieces and connect them together, we must have a clear idea of our boundary constraints: design choices, desired features and properties, and decisions we do and do not want to make. This post is an attempt to assemble a clear list thereof.

Basic context

  • The basic units of state and history in the AVM are objects. Objects can send and receive messages, and each object has a history.
  • Objects do not have mutable state. An object is either a code object or a data object. Data objects can be created exactly once, read any number of times, and destroyed exactly once. Code objects run a program when they are called.
  • At any point in time, execution is taking place within one object. Execution can move between objects with calls.

Distributed execution

The AVM is executed by many machines. At any point in time, execution is taking place on one machine. The AVM must support teleportation, where programs can move the current execution context to another machine.

Objects are controlled, each by a unique machine at any point in the history of the object. Each machine tracks the histories of other machines and synchronizes state, and each AVM execution is tied to a particular historical snapshot. Programs interacting with an object which is locally controlled (controlled by the machine on which the program is executing) are guaranteed to see the latest version of the object, which programs interacting with an object which is not locally controlled may see an out-of-date version.

AVM programs must be able to:

  • read the current (latest) history identifier from the executing machine
  • switch to a target history identifier

Do code objects need to be moved between controllers? Or are data objects (which exist on exactly one controller, since they’re immutable) sufficient?

Pure computation

The AVM must not make decisions about how pure computations (functions) are represented. Instead, the AVM should support an arbitrary set of known functions which can be appended to over time.

Transactionality

The AVM must support transactional semantics, where programs can:

  • begin a transaction (scoped to a specific controller), starting a transaction context which collects pending state changes
  • commit a transaction context (attempting to atomically commit all pending state changes)
  • revert a transaction context (resulting in no state changes)

Preference-directed non-determinism (aka intents)

The AVM must support preference-directed non-determinism, where programs can:

  • request an arbitrary input, given a specified preference distribution over the range
  • constrain it in arbitrary ways (such that the transaction will fail if the constraints are not met)

This should be a sufficient substrate on top of which to implement Prolog-like logic programming.

Multi-party transactions

The AVM must support multi-party transaction constraints, where programs can:

  • create linear constraints which must be satisfied by message sends in the same transaction in order for the transaction to be committed, where a given message send can only be used to satisfy one linear constraint

The combination of preference-directed non-determinism and multi-party transactions must be sufficient to allow programs to implement arbitrary intents.

3 Likes
AVM ISA: What we’re currently building and why at 12/11/25
AVM Instruction Set - Instr₀
AVM Instruction Set - Instr₀
2

Thanks for writing this because it really makes me evaluate where AVM Instruction Set - Instr₀ sits in the actual AVM discussion.

Done, see What’s an object.

The word “mutable” here brings some tension.

In my understanding, objects can “mutate” via messages, resources, no. Objects compile to resources; however, the correspondence is not one-to-one. Every new message the object receives creates a new resource, altering the object’s history.

There are two abstraction levels to consider here:

  • The resource machine level: Each object is an immutable resource. When we “send a message” to an object, it doesn’t mutate. Instead, we create a new object with the updated history.

  • The AVM/logical level: An object is conceptually a function from input sequences to outputs, plus a history. This function is the immutable part—it specifies how the object responds to incoming messages, with no dependency on the history. However, objects mutate/evolve.

At the AVM level, the history is simply the sequence of messages the object has processed so far (in order matters). I prefer to call this sequence the object’s “view”, same ideas as in Tango. These views are subject to synchronisation in a distributed environment. That’s one reason we keep it along with the object’s definition.

The views of an object determine its “state,” which results from applying its function to its history. Note that different histories may produce the same view.

“The behavioural state of an object ⟨ī, φ⟩ is the equivalence class [ī]_φ of all input sequences that produce the same future behaviour.”

Why bring this distinction? Code is just data, in my opinion. An object may behave as a constant function—like a program that doesn’t care about inputs, just returning some value—in which case we can call it “data”. Or it may behave differently, actually doing something, in which case we call it “code”.

I don’t follow the “created exactly once” constraint. I work assuming that the object lifecycle is dictated by the following instructions:

createObj : Input → Instr₀ Safe ObjectId   -- Create object from input
destroyObj : ObjectId → Instr₀ Safe ⊤      -- Remove object from store

The semantics for createObj states that a new object is created with the given input (which defines its behavior). There is no comparison point to say “there is an object with this input that was already created”. How do we compare such a thing?

Regarding destroyObj, we could modify it to enforce that “an object is destroyed exactly once”. However, again, I need to introduce knowledge about what’s being destroyed, an additional index (as part of the State).

If os, instead of using ⊤ in the return type of destroyObj, we can return a result of two possible natures: either an error (the object was already destroyed/doesn’t exist/isn’t available) or a successful deletion. That is, we use type Either AVMError ⊤, where

data AVMError  : Set where
    ObjectAlreadyDestroyed : AVMError
    ...

Any attempt to destroy an already-destroyed object returns an ObjectAlreadyDestroyed term.

This is compatible with Ctx, which puts in the AVM instance’s state the object id of the current object in execution. You can also find the input used.

record Ctx : Set where
  constructor ctx
  field
    self : ObjectId
    input : Input
    traceMode : Bool

in State:

record State : Set where
  constructor st
  field
    store : Store      -- Persistent store of committed objects
    ...
    y : Ctx            -- Execution context, it includes the current object and input

What do you really mean here? What do you move with the execution?

This is a fundamental requirement for the design of the AVM, and I believe adding this “later” would create difficulties, such as object history synchronisation, object availability, and different semantics for the call instruction.

So, be aware, this is something completely abstracted way, or better put, ignored, in Goose and also in State of the AVM: The Execution Environment. Both works are developed under the assumption there is only one node, which you call controller.

That’s for the basic context section of yours.

3 Likes
3

At a higher level of abstraction, I agree with you – data objects are an attempt to include the immutable state level (resources) in the VM directly. Perhaps we don’t need them, I’m not sure yet, but there could be advantages to enforcing this kind of strict separation: code objects could always be “compiled away” or flattened (de-nested) in a straightforward manner since they don’t themselves have any state (only message calls). Putting data objects (resources) in the VM allows programmers to have control over the low-level state representation when they want, while still allowing it to be abstracted away most of the time (as Goose does).

I just mean the flow of program execution (if you think about it operationally).

4

Okay, I can work with this. But, do you have something in mind on how to control the low-level state representation?

5

Refinement of desiderata for constraint programming, non-determinism, and multi-party transactions:

Simple constraint programming and non-determinism

Programs should be able to:

  • Request an arbitrary input from a specified domain (which may be very large). This corresponds to choose from the current draft.
  • Check constraints on arbitrary values (such that the current transaction will fail if the constraints are not met). This corresponds to require from the current draft.

The AVM runtime should be able to symbolically execute a program in order to extract free variables (from choose) and constraints (from require), and extract the resulting constraint satisfaction program to a suitable intermediate representation such that existing SAT solvers or similar could be used.

Intents and multi-party transactions

Multi-party transactions at the most basic level entail composing multiple program executions (or transactional parts of those executions scoped by beginTx / commitTx) into a single transaction.

Program/transaction composition requirements:

  • It should be possible to compose the transactional parts of multiple non-conflicting program executions into a single transaction, where that transaction executes the combined state changes from all of the individual transactions atomically.
  • It should be possible to compose the transactional parts of multiple sequentially dependent program executions (e.g. A and B where reads performed by B should reflect writes performed by A) into a single transaction, where that transaction executes the combined state changes from all of the individual transactions atomically, as if they were executed in order (A, then B, in this example).

These operations correspond to the transaction composition in the resource machine, just at the AVM level of abstraction.

In order to allow multi-party intents we need to additionally allow programs to check constraints on the state changes performed by other programs which we compose them with. There are many different ways to represent this – I know @graphomath is working on a clearer formalism in the AVM green paper, which will hopefully provide some better guidance here, but in the meantime I suggest something like:

  • The AVM runtime should keep a record of messages sent during the course of program execution (effectively, a record of the message sequence chart of the program execution).
  • AVM programs should be able to check constraints on other parts of the message sequence chart generated by other programs whose execution became part of the same transaction (as described above).
  • These constraints should be able to be both non-linear (leaving the MSC record untouched) and linear (once part of the stored MSC record has been used to satisfy a linear constraint, that part of the MSC record is removed, so that it can satisfy no further constraints). The latter is necessary to implement e.g. simple token swaps – cases where the intent author wants to guarantee that they’re offering some state change A in exchange for some other state change B, and that this exchange is separable from anything else that might be happening in the transaction.

We should also be able to perform some kind of speculative composition and symbolic execution of multiple programs in order to extract the resulting CSP to an intermediate representation suitable for use with SAT solvers, but there are a lot of details here which I haven’t thought about yet.

1 Like
6

I think, I finally may have understood where you are going with this after spending some time answering to this message. I will now present some of my writing (in reverse chronological order).

TL;DR

Having a nice CSP representation for solvers certainly helps in figuring out examples, getting an idea whether this all is practicable, and helps the prospective end user (cf. “upward”). Also, I actually appreciate that there seems a large sub-space of what you’re describing that includes the possibility of spiffy illustrations that feature message sequence charts. Now, long story short, in view of getting out a first prototypical picture of the AVM, “this” is not only fun, but “it” also ties in with best practices (as per my slide 5/13 from the last Anoma day or the software practices taught in the course of this slide. So, what is “this” and “it”

blueprint.pdf (692.1 KB)

double checking by tentatively narrowing down

Let me see if I have understood the direction of your proposal, choosing one particular path, which may go in roughly the right direction.

  1. So, it seems that we likely can figure out how each (execution of a) program (on some object[s]) can be mapped to an MSC (potentially injectively, by suitable annotations etc.)[1]
  2. We then could define an AVM-intent format as something consisting of a set of (sub-)MSCs with variables and constraints.[2]
  3. Solving would amount to puzzling together the sub-MSCs to a fully specified MSC, which corresponds to a program (as per injectivity in item 1. ), satisfying all other constraints.[3]

Would this be a specialization of what you’ve had in mind when writing the above, @cwgoes?

The following may look like a digression. I think it is very simple and almost obvious. However, let me repeat the argument that may be buried in Appendix A of the AVM green paper

PS / last but not least …

I have no specific formalism in mind in particular concerning the syntactic nature of intents. I merely have a simple definition of program enabling that should be polymorphic in the intent type and the program type, namely each intent is associated with a set of programs that it enables.

program enabling

In the context of the intent-machine report, we can define that an intent i is enabling a program p when there is

  • a batch b that contains the intent i and
    • a state s such that
    1. program p can be executed on s in the context of b and
    2. this is not the case w/o the intent i, i.e., p cannot be executed on s in the context of b ∖ \{ i \}

In the concrete case of intents as unbalanced actions and programs as transactions, a transaction is enabled by an intent if there there are other intents such that combining them together with the intent we obtain a transaction that can be executed on some state.

program extension ≔ set of enabled programs

Now, we can look at the set of programs that are enabled by an intent. Maybe this is now all completely uncontroversial and the only thing that may have been suboptimal was the proposal to identify intent with its program extension.[4]

  1. There are questions concerning whether method calls are transferring control to another machine, or we simply pull the code and keep execution locally; both options are valid, I think, and only the application context will tell us which one is the more suitable approach (moving code or moving data). ↩︎

  2. I am leaving out on purpose of whether or not we need/want linearity/quantitativity/etc. ↩︎

  3. Here, in particular the constraints from choose-instructions and the postulated require-commands. ↩︎

  4. There is a fundamental problem with all this, in that we may accidentally included “spurious” intents, because an intent with vacuous extension (by which I mean the empty set), is not committing the issue to anything. Thus, if we understand intents as commitments with additional qualities, then, well, we have a problem insofar as we now have intents that do not commit to potentially anything? But let us now come back to the actual thing, how this all relates to CSP. ↩︎

1 Like
7

Cross-roads in object histories and why single object histories are only part of the story

This post is addressing the observation that there are events—in the sense of the source—that

may involve multiple objects of possibly different types.[1]

Now, if we look at the desideratum that

and we have two or more objects o_1, o_2, ... interact with each other as part of a program, we would have to pack them up (temporally) into the sum \sum_i o_i of the previous objects o_1,o_2,... to give the execution of the program a place to be “located”, namely the sum object \sum_i o_i. E.g., for n=2, this would involve first deleting o_1 and o_2, then creating the sum (o_1 + o_2), running the program on the sum, and finally splitting the next version of (o_1 + o_2) into new objects o_1' and o_2'.

[☜ here is some background material concerning object history, object versions, and (im)mutability---click the triangle to unfold this material]

For the post, it may be helpful to recall that an

object can be thought of as a sequence of versions, the states that the object has assumed and will assume as the result of the computations that are applied to it. We will call this sequence the object history. It is a completely static picture of the object’s behavior. Since the entire object history is not known until the system has finished execution, this is clearly a logical concept, rather than something that has a counterpart in the real system. Nonetheless […], imagine that a program does execute in an environment where all the histories of all shared objects are known.[2]

The typical situation is a swap of assets, or concretely our typical kind of example.[3]

sequenceDiagram
    participant Alice
    participant John
    Note over Alice,John: begin swap
    
    par
    Alice ->> John: have an apple
    John ->> Alice: have an orange
end
   Note over Alice,John: end swap

We can use plain flat transactions (potentially shielded) to achieve the above synchronization pattern for a pair of objects—to be precise, two potentially concurrent versions of objects. Moreover, as part of the desiderata, we have the begin transaction-end transaction-blocks, which seem to be exactly for this kind of interaction between objects—as illustrated above.

TL;DR

  • some transactions (on a controller) commit the effect of program executions involving several appends to histories of several objects
  • while each of the extended histories is consistent in the context of the respective object, only the extension of all the object histories is the intended state change of the transaction

A potential solution would be the (temporary) grouping of objects for some purpose. In fact, grouping of objects may be useful also for moving objects together.[4] This grouping is de facto necessary to collect all necessary data for creating the proofs of a (shielded) transaction.

How does it related to the title and what else?

Object histories naturally evolve jointly. Forcing several objects to become one is maybe too drastic, in particular if it is only in the context of a certain common “task,” which could be any of a session, transaction.[5] A notion of object group is not a new idea.[6]

  1. Object-Centric Process Mining: An Introduction Wil M.P. van der Aalst ↩︎

  2. page 64 of Naming and synchronization in a decentralized computer system. Massachusetts Institute of Technology, Cambridge, MA, USA, 1978, emphasis in the original ↩︎

  3. Let us leave aside even the complications of objects that are controlled by different controllers. Image the single controller case and all relevant (resource represented) objects are controlled by a single controller. ↩︎

  4. In fact, this idea is described in the context of Emerald. ↩︎

  5. In short, not all interaction is naturally asynchronous in the following sense: The most general form of a rewrite rule for the modeling of object-oriented systems is the following:

    image
    image362×278 18.4 KB
    ↩︎

  6. In fact, merging of rule sets and facts also makes sense in the context of a logical approach, e.g., in PROLOG. ↩︎