Preamble
Recently, I’ve been investigating what it might mean to model applications as object systems. This involves many aspects, some of which are “essential” (in the sense that they must be considered holistically), and some of which are “inessential” (in the sense that they would be little more than syntactic sugar compiled to a simpler representation) – and it’s not always clear which is which. This post is an aim to construct some critical components – basic definitions, transactionality, determinism/non-determinism, information flow control, and compilation to resources – in a step-by-step way which carefully teases apart what they mean individually and thereby allows us to see clearly how they might relate to each other.
This post will define important terms in bold.
Basic definitions
What are applications?
The SGS ART report will discuss applications from first principles, but here I will just adopt a working definition: an application is a subset of Anoma network state and associated functionality which provides a user-facing interface surface oriented towards a particular purpose, such as credit tracking (kudos), social organization (multichat), or deciding where to go for lunch (LunchBot). An application is singular (unified) in virtue of this purpose: if it’s unrelated to lunch decision-making, it isn’t part of the LunchBot application.
What are objects?
For our purposes, an object is anything which you can send messages to and get responses from. This is a purely behavioral definition – an object is as an object does – and it is both necessary and sufficient: if you can’t send messages to (specifically) it, or can’t get responses from (specifically) it (eventually), it isn’t an object.
From this basic definition we can derive some corollaries:
- An object is fundamentally relational: an object is an object to whomever can send messages to it and receive responses from it (perhaps, but not necessarily, everyone). It’s entirely possible that something may be an object to me but not to thee.
- In order to send messages to one object as opposed to another, I must be able to distinguish between them. Therefore, an object must have some sort of name from the perspective of whoever is able to send messages to it. For the remainder of this post, we will use numbers to indicate this name – e.g. O_1, O_2, etc. – but this is just convention, names need not be anything in particular.
- From the perspective of whoever is sending messages to it and receiving responses, an object has a history: the sequence of messages sent and received. We will also call that sequence of messages a trace.
How can we characterize objects?
So far, we haven’t talked about how objects behave – we’ve just said that you can send messages to them and get responses. However, in modeling applications as objects, we will be constructing objects, and when we construct objects, we can specify how they (ought to) behave. Let’s dive into what that might look like.
A basic first step in characterizing the behavior of an object – which we will call the object type – is to specify what kinds of messages you can send to it and what kinds of responses you might get back. This entails two types. Let’s call the first type the input and the second type the output. In the simplest sense, then, an object type is simply a pair of two types (the input type and the output type).
type SimpleObjectType I O = (I, O)
We will use the word “type” somewhat loosely – it can be understood as a synonym for “set”.
This simple object type tells us what kinds of messages we can send to the object and what kinds of responses we might get back, but it doesn’t say anything about when we would get certain responses. How might we characterize that? Remember that objects have a history – outputs aren’t necessarily a pure function of inputs. The most basic thing we could know about what kinds of responses we might get back is then a property of all potential histories, which we will call a trace invariant:
type TraceInvariant I O = [(I, O)] -> Boolean
Histories where the trace invariant holds are histories we might observe. Histories where it does not we will definitely not observe. What history we actually observe, of course, depends on which messages are actually sent to the object in question.
With a trace invariant, then, an object type consists of an input type, an output type, and the trace invariant:
type ObjectType I O = (I, O, [(I, O)] -> Boolean)
Note: we are assuming here that messages are totally ordered. We may revisit this assumption later but will take it as granted for now.
Now, this trace invariant is just an invariant: it specifies what histories may be observed, but does not necessarily allow us to compute what the response of an object would be given a particular history of inputs (since there might be many possible responses). If we want to specify the ability to compute that, we are specifying a deterministic object with a characteristic response function, as:
type DeterministicObjectType I O = (I, O, [(I, O)] -> I -> O)
Note that from a characteristic response function we can compute a trace invariant: the trace invariant is true for the output determined by the characteristic response function, and false otherwise.
One possible way to implement a deterministic object is for the object to keep a state which keeps (and typically compresses) whatever information about the history of interaction is needed in order to compute the response to the next input. From the perspective of the external interface, though, this is just one possible implementation – an external observer doesn’t know anything about the “state” of an object or lack thereof, only its observable behavior.
For the remainder of this exploration, we will work mostly with the standard (not necessarily deterministic) object type.
What would it mean to model an application as an object? Let’s take a very simple version of kudos, specified as follows:
- A party A (parties are identified by public keys) should start with 100 kudos.
- Any party should be able to transfer kudos to another party (authorized with a signature) and read their balance.
- After a transfer of amount X from source S to destination D, the balance of S should decrease by X and the balance of D should increase by X. If S’s balance would become negative, the transfer fails (and has no effect).
Let’s model this simple kudos application as an object. To start, the input and output messages:
Now, what should the trace invariant be? In this case, we can describe it recursively:
calculateBalance [] a = if a == A then 100 else 0
calculateBalance (x : xs) a = calculateBalance xs a + case x of
(Transfer source dest amount, OK) = if
| a == source -> -amount
| a == dest -> amount
| 0
_ -> 0
traceInvariant xs : [ (getBalance a, balance amount) ] = amount == calculateBalance xs a
traceInvariant xs : [ (transfer s d a sig, result) ] =
result == validSig sig (s, d, a) and a >= calculateBalance xs s
traceInvariant [] = True
If an object behaves like this, it is a valid implementation of this kudos application as we have defined it. Now, how might we implement an object which behaves like this? We could, of course, create a specific object with a state (balances of different users) and a transition function, but this would mean that we have to place that object somewhere in our distributed system, and notably that reads and writes to that particular object would be more ordered than they need to be: independent transfers do not need to be ordered with respect to each other in order to satisfy this invariant. Instead, therefore, we will attempt something else: to decompose this object (type) into a system of smaller object (types) which, taken together, provide the same external behavior.
We will call this problem the problem of object decomposition: to take a description of a higher-level object type and craft a system of lower-level objects and messages between them that, taken as a system, behave as if they were a higher-level object without a need for an actual, named higher-level object anywhere in particular.
Transactional object systems
Let’s now investigate object systems: collections of objects interacting with each other in a shared context. Remember: we want these object systems to behave as if they were one higher-level object. That higher-level object either receives a message and responds or does nothing at all – messages are atomic, there is no “partial receipt”. This means that our object system must be transactional: even though multiple messages may be involved internally, each transition initiated from the outside must either fully complete or have no effect at all. Let’s draw this:
The basic execution flow would always be as follows:
- An incoming message comes into the system (as would be sent to the higher-level object).
- Internal message-passing happens between objects in the system.
- A response goes back out (as would be sent by the higher-level object).
How should these external messages trigger internal messages? A start is simply to model this relationship as the implementation of the higher-level object, which has no state and must handle incoming messages by making calls to the lower-level objects. These calls must all happen within a transaction, which either completes successfully or has no effect. As a diagram:
What would this object system look like for our kudos app example from earlier? A simple option is to keep a “balance” object for each public key, which we subtract from or add to on a transfer and read on a balance query:
Note here that implicit in this description is a balance object associated to each public key, which starts with a balance of 0 – and the high-level “SimpleKudos” object must be able to look up these balance objects somehow.
Let’s write this out as an internal transaction invariant scoped over the message sent to and response sent from the higher-level object and the messages & responses to and from the lower-level objects, where nameOf captures this nominal relation described above:
transactionInvariant (Transfer s d a sig, OK)
[(s_o, Subtract a, OK), (d_o, Add a, OK)] =
nameOf s_o == s &&
nameOf d_o == d &&
verifySig sig (s, d, a)
transactionInvariant (Transfer s d a _, Failure)
[(s_o, Subtract a, Failure)] =
nameOf s_o == s
transactionInvariant (getBalance a, balance a)
[(a_o, Read, ReadResult a')] =
nameOf a_o == a **
a == a'
transactionInvariant _ = False
So far, so straightforward. Now for the sleight of hand: nowhere in this transacation invariant is the higher-level object actually referenced. Thus, we can erase it: as long as this invariant is checked in any transaction involving the lower-level objects, the observable behavior of the system will be identical to the desired behavior of the higher-level object (as we intend).
This invariant, however, is still singular, and we must decide how to trigger it. Let’s proceed as follows: for each lower-level object, encode a check for the subset of the invariant which mentions that object, which gets triggered whenever that object is modified.
General process of compilation
- Take a system described by a higher-level object and express it in terms of a transactional system of lower-level objects, described by a transaction invariant (as in the above example).
- Partially evaluate the transaction invariant on each lower-level object in order to obtain the invariant which should be enforced by that specific object.
- Transaction environment must include (a) external inputs + outputs [messages to/from the higher-level object] and (b) messages between the objects at this level.
This can be repeated recursively by carrying constraints through the recursive passes, which will typically reference intermediate messages that can then be simplified out (into more complex constraints). I haven’t worked out all the exact details yet, there’s a stab here.
To illuminate roughly how this can work, let’s run through the full example for kudos, where we implement the balance objects in terms of immutable objects which simply store a certain amount assigned to a particular public key, and can only be created or destroyed. In a diagram, the application now looks like:
Let’s examine the balance object transaction invariant:
transactionInvariant (balanceFor a) (Subtract amt, OK) objs
= all (ownedBy a objs) and
sum (consumed - created objs) = amt
transactionInvariant (balanceFor a) (Add amt, OK) [(NewImmutableObject a' amt')]
= a == a' and amt == amt'
transactionInvariant (balanceFor a) (Read, ReadResult amt) objs
= sum (map amount objs) == amt
transactionInvariant _ _ = false
I’m eliding some detail here concerning how we ensure that all relevant immutable objects are looked up in the balance query, but let’s leave that for a future, more refined version – it’s inessential to the essence of the proposal here.
We can now erase these intermediary balance objects by combining the transaction invariants as described above, and voila: a kudos application compiled down from a higher-level object representation to constraints on immutable objects!
This process needs to be worked out in full detail, but I wanted to share this direction for feedback first. Note a few particularities of this flavor of object system:
- Objects do not have state, except for the final level of immutable objects. Higher-level objects can only create, destroy, and send messages to lower-level objects.
- A hierarchy is implicit: we can think of the lower-level objects, in some sense, as within the higher-level objects. Lower-level objects within a higher-level object cannot be referenced elsewhere (so this is also a nominal scope).
Brief notes for self on future topics to explore in this area:
Intents in object systems
Let’s extend the kudos example with a “swap” input. This will require two changes:
- We’ll need to extend the application to be able to refer to multiple denominations (A-kudos, B-kudos, etc.).
- We’ll need to add an input “Swap(denomA, amountA, denomB, amountB)” which allows the user to swap amountA of denomA kudos for amountB of denomB kudos (if a counterparty can be found).
Let’s first extend the existing application with different denominations, which is straightforward:
Now, let’s add “Swap”. At a high level, the inputs and outputs should look like this:
where either the swap completes successfully, and the swapping user’s balance increases by amountB of denomB and decreases by amountA of denomA, or the swap does not complete, and no balance changes happen.
Now, how might we implement this? The user in the swap example wants to find a counterparty, so let’s invent a magic “counterparty discovery” object, which will either find them a counterparty (who wants to swap in the opposite direction) or fail (if no counterparty is found). If a counterparty is found, simply execute the transfers – if not, do nothing. In a diagram:
This is the basic pattern: represent counterparty discovery as an object, which either returns a suitable counterparty or fails, and perform subsequent state changes accordingly.
TODO: Figure out the compilation here, it should result in two opposite swaps being able to be matched because “counterparty” is a free variable. Also figure out the difference between one counterparty and multiple counterparties.
Information flow control
The basic thing we want to do here is add annotations to specific messages (methods) which specify who is allowed to send (call) them. As a first pass, we can limit the scope of these annotations to data in the method itself (so annotations cannot depend on any state). This is sufficient, for example, to specify that only the owner should be able to read their kudos balance:
Now, this metadata, described as a constraint, must be passed through compilation and eventually operationalized (e.g. by verifiable encryption). In order to do this, we need to track the decomposition of messages (e.g. whatever getBalance is implemented in terms of) and pass through the constraint (only A should be able to send those methods), where the constraint can be operationally realized at the final level by mechanisms such as verifiable encryption (which must be tracked holistically, since e.g. someone transferring kudos must now encrypt the outputs). Some combinations will not be possible to compile, e.g. an input that is only allowed to be sent by A and another only allowed to be sent by B, where both translate to reads of the same object (a smart compiler could show an indicative error message in this case, and the user could perhaps change the annotation to make it work).
This should already be sufficient to make a lot of basic things work. More complex iterations could allow for history-dependent annotations (e.g. as in a messaging app - should be able to read messages sent to me), and this would ultimately need to be incorporated into the trace invariant (which would then be additionally scoped to “who is calling” beyond just the inputs and outputs).
- Similar to Viaduct, we should be able to search for cryptographic primitives to implement the desired IFC properties (but modeled in this object-system-way).
- Analyze many more examples.
cool video though!
