This post continues the series on the AVM architecture as AVM ISA: What we’re currently building and why at 12/11/25. This entry is related
to the object and introspection instructions of the AVM or better, an example of how to define an object using this model. It mostly explains how
the object model works as introduced in the green paper and how it relates to the current AVM specs.
Be aware that we have abstracted away the details of the object model in the
instruction set. So, in principle, we are not fixing the object model for the
ISA, however, we are proving one model here.
AVM objects are history plus a pure partial function from input histories to
outputs. No mutable variables. No hidden state. Formally, the object behaviour is
a function behaviour: InputSequence → Maybe Output. Given any input history,
the behaviour either returns outputs or is undefined (a “crash”). This sounds
inefficient, but it enables powerful reasoning. This post explains the functional
object model we are using at the moment — the foundation for AVM’s
message-passing semantics.
Objects as vending machines
We before introduced objects as black boxes with API endpoints. Another analogy
could be to think of an object as a vending machine that remembers every
button you’ve pressed. You press “A3” and get chips. You press “B2” and get a
soda. The machine’s current state (how many chips left, how much money
collected) is determined entirely by the sequence of buttons pressed so far.
Traditional programming: The machine has internal variables tracking inventory
and cash. You modify these directly.
How is this following the AVM approach? The machine is a pure function. Given
the history [A3, B2, A3], it computes the current inventory and decides what
to dispense next.
Why? Because you can replace a history with any phi-equivalent history (one that
induces identical future behaviour) — not arbitrary reorderings. The internal
representation doesn’t matter — only observable behaviour matters.
That’s the reason we formalise the notion of object as two things essentially:
a history (part of the ObjectMeta record) and a behaviour function (part of the Object(-type) record).
Three key properties
Objects must satisfy two core rules to be well-formed (this @graphomath
introduced in the green paper)
- Empty word defined: Every object has an initial state. You can call an object
with no prior inputs. - Prefix closure: If an object responds to input sequence
[a, b, c], it must
respond to[a, b]and[a]. Objects cannot suddenly become defined after
being undefined.
These rules ensure objects behave predictably across all input prefixes.
Formal model
Formally, each object exposes a behaviour function with type:
behavior : InputSequence → Maybe Output
The Maybe result captures partiality: for some histories, behaviour may be
undefined (a crash). As objects behave as actors, they can crash or even not
respond at all when the message is not in the object’s domain of definition.
Optional determinism: Objects may be deterministic (same input history always
produces the same output) or nondeterministic (incorporating randomness or external
choices via choose instruction). So, deterministic objects enable replay (applying behaviour to the history) and the verification of received messages. Nondeterministic objects enable intent matching and constraint satisfaction (no examples of this yet, but we want this).
Why history instead of mutable variables?
Three advantages:
Conceptual rollback: Reverting to a prior state corresponds to truncating the
history when it preserves future behaviour. In the current interpreter, rollback
is achieved via transactions: aborts, discards uncommitted writes (overlays), and
there is no instruction to truncate committed history.
Replay is well-defined: Pure functions have no external side effects. For
deterministic objects, identical histories produce identical outputs, enabling
replay and formal verification. For nondeterministic objects, the history
records which choices were made, enabling replay of the specific execution path.
Behavioural equivalence, what?
Behavioural equivalence is well-defined: Two objects are equivalent if they
respond identically to all future inputs, regardless of internal representation.
A counter tracking explicit state is equivalent to one computing the length of the input
history, as long as both produce the same outputs.
So, two histories are behaviorally equivalent, or their objects, if they produce
identical future behaviour. History [inc, inc, inc] and history [inc, inc, inc, inc, dec] both result in count 3. They have identical future behaviour. In
principle, an implementation can replace either history with a compact state
(e.g., count = 3). The current interpreter, however, recomputes from the
recorded history (ObjectMeta.history) and updates metadata; it does not replace
histories with a compact state today. We’ll see the counter example below, and
using Racket, why not!?
Breaking encapsulation: Why unsafe operations exist
Despite the pure functional model, the AVM provides three unsafe operations that
break encapsulation:
-
reflect: Retrieves object metadata (controller assignments, physical location)
without invoking the message-passing interface. Objects cannot control what
information gets exposed. -
scryMeta: Searches the global store for objects matching a predicate. Can force
complete store traversal if the predicate accepts everything. -
scryDeep: Like scryMeta but filters on object internals and metadata. Breaks
parametricity by exposing raw object values.
Example: A counter object
Finally, an example, not surprisingly, it’s the infamous counterexample.
A counter object processes inc and dec messages (inputs) and produces numeric values (outputs). The theory supports objects where input and output types differ - an I-O object for input type I and output type O.
#lang racket
; Counter object type - specification
(define counter-type
(lambda (history)
(foldl (lambda (msg count)
(cond [(eq? msg 'inc) (+ count 1)]
[(eq? msg 'dec) (- count 1)]
[else count]))
0
history)))
Run this in DrRacket:
- initial state: empty history
(counter-type '())
; => 0
- After one input:
(counter-type '(inc))
; => 1
- After three inputs:
(counter-type '(inc inc inc))
; => 3
- Different history, same count:
(counter-type '(inc inc inc inc dec)) ; => 3
Here, the counter doesn’t store a mutable variable. It computes the count by
folding over the input history. First, I tried to remember this, but I failed. So if
you didn’t get it, just try a second read.
Connecting the dots, you see that the two histories (inc inc inc) and (inc inc inc inc dec) are behaviorally equivalent - both produce count 3.
And these histories are also φ-equivalent for this specific counter; this does not imply that arbitrary input reordering is safe for other object types.
The example above shows the specification: objects are functions from
histories to outputs. Again, we’re not preoccupied with efficiency here, just
the model. An optimisation could be to cache the state and avoid recomputation.
Open questions
Three questions for discussion:
Should the AVM support alternative object models? The current functional model
is statless and one can say that itprovides strong reasoning principles but may
incur performance overhead, as you saw in the example. Should implementations
offer explicit state representations as an alternative? In any case, the object
model is a parametric type, so changing the implementation is a matter of instantiating the type with a different model.
How should implementations decide when to garbage collect history? Behavioral
equivalence enables truncating irrelevant history prefixes. Should the VM
provide explicit compaction instructions, or should garbage collection be
automatic and transparent? This is a matter of implementation detail, but it’s
worth discussing.
Last words
The current AVM object model (as in the green paper) supports rollback via transactions, supports formal reasoning through behavioural
equivalence, and allows applications to choose between deterministic and
nondeterministic behaviour. The current design enforces parametricity, ensuring
objects are opaque – programs cannot inspect internals except througha message
passing.
Unsafe reflection operations break these principles but enable essential
system-level tools. I’m unsure of having a scry(meta/Deep) instruction in
reality. Can one really guarantee an AVM implementation will work as expected?
Looking up the whole universe, humm, I don’t think so. The current specs document
the tradeoff explicitly.
History accumulation appears inefficient, but behavioural equivalence enables
optimisation. Implementations may optimise by replacing histories with compact
representations (explicit state, truncated suffixes) as long as observable
behaviour is preserved. However, we need to double-check this with the implementation.
We wrote more on this a couple ago in Sequential Objects - WIP Notes
Promise:
- how to define a kv-store, bank account, a kudos swap.