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.