Anoma meta-app & the Babeloma fish

[cwgoes]

Part 1: The Current Problem Space

I’m going to try to break down the current problem space as I see it (focusing on the next immediate step, not the long-term “Babeloma” vision). In the current problem space, I think that we have three major levels and two major conversions, one of which is automated (compilation) and the other one of which is manual (what the application developer does).

The three levels:

1. The application interface – the high-level specification of what observable behavior an application should have, in terms of inputs, outputs, and behavioral properties (as described above).
2. The application intermediate representation (“Anoma-level”) – an “intermediate-level” definition of what kinds of state, reads, and writes an application consists of, including who should be able to see what (information flow control - type properties).
3. The application low-level implementation – the actual “operating-system-level” logic that implements an application, including resource logics, transaction functions, query logics, etc. (e.g. custom engines, MRDTs, etc. in the future). The low-level implementation also includes details like which resource machine primitives/proofs are used when, and all specific cryptographic choices.

The two conversions:

1. The application developer must write the intermediate representation, given an application interface specification, and reason about whether their intermediate representation correctly implements the application specification (eventually, maybe we can incorporate some automated verification tooling here, but that’s a future project).
2. We must be able to compile the intermediate representation to appropriate low-level implementation code which correctly implements it. This compilation should be fully automated, and need not be altered or understood by the developer (although it can be exposed to experienced developers so that they can control the low-level representation if they want to).

Pictorially, we could visualize this as follows:

What exactly is this intermediate representation? This is a complex design problem, and I think we’d best start with some “boundary constraints”. Let’s first address an elephant in the room: information flow control.

Part 2: Information Flow Control

Application Interface Level IFC

Let’s start at the application interface level. In the application interface, at the most basic level, information flow control means that the interface must specify who can read what outputs under which conditions.

Let’s take the kudos example from above, which had two specified outputs:

1. A user must be able to read their kudo balance.
2. A user must be able to read a history of changes to their kudo balance, and associated data.

I wasn’t clear in the above example, but suppose that we take the default to be non-access, e.g. no outputs should be possible to read other than the ones which the application interface explicitly specifies. Given that default, we can infer from this list of outputs that:

• No user should be able to learn anything about any other user’s kudo balance.
• No user should be able to learn anything about any other user’s kudo balance changes/history.

etc. – nothing should be able to be learned other than these explicit outputs. Of course, users can always choose to disclose any data they would like to, but this is not the primary concern of the application developer. In order to implement this application interface, then, we need a shielded resource machine – and fully private solving, if swapping shouldn’t reveal anything either. Likely this requirement is too strict, and the application designer might choose to alter the definition roughly as follows:

Inputs

• A user must be able to swap X kudos for Y kudos, with specified amounts, where the user selects a set of solvers S to whom they are comfortable revealing X-for-Y.

Outputs

• A solver who a user selects with a swap should be able to see X-for-Y as in their swap and search for solutions.

Given our non-access default, this output implies that no other solvers (or, indeed, nodes) other than the ones selected should be able to see X-for-Y for a particular user input. Implementing this requires a trust assumption – namely, that the solvers which the user selects do not further disclose the “X-for-Y” information – which must be made explicit in the expected output property. To be fully explicit, we we will likely want to specify information flow control properties as relations between outputs and inputs, given assumptions – for this example:

Input	Assumption	Output
Swap(X, Y, S)	\forall s \in S. honest(s)	SwapRequest(X, Y), visible to only s \in S

We’ve now introduced solvers as an actor in this application definition – there is no implied semantics here other than “the node which the user chose in their swap input” – but note how which solver is supposed to be able to read the output depends on the field in the user’s input. Presto, information flow control!

To contrast this: a fully transparent kudos application interface would specify that anyone can read anyone’s kudo balance, transaction history, and swap intents. This application interface would then be fully implementable on a transparent RM.

Note that for now, we’re just focusing on information flow control of state, including in intents, but not including metadata like transaction timing. This is also important to think about, but I think we should figure out the state-level information flow control throughout the whole application programming stack first.

So – roughly – information flow control at the application interface level consists of specification in the inputs, outputs, and behavioral properties of who can read which outputs under what conditions. Other than the explicitly specified outputs, and assuming explicitly listed assumptions, no one should learn anything (default “non-access”). This are really information flow policies, in that they are fully declarative and specify who should learn what (and, by exclusion, who should not), but prescribe no specific cryptographic or operational mechanisms. This needs to be worked out in much greater detail and with more examples, but let’s first take this rough concept and see what it means for the intermediate representation.

Intermediate Representation Level IFC

I’m going to take some interpretive jumps here, attempting to synthesize past work here, here, and elsewhere, and make a specific proposal: let’s imagine an intermediate representation with two sub-levels, both with “objects”, which I will call the “high-level declarative object application IR” and “mid-level immutable object application IR”. Both of these levels are total, in the sense that an application can be represented fully at the respective level of abstraction, without any “abstraction leakage” from other levels (and both levels can be understood to have defined semantics, which correct compilation to a lower level must respect).

I think it’s best to start with a diagram:

Roughly:

In the immutable object-level application IR representation:

The state of an application at any given time consists simply of a set of immutable atomic (indivisible) objects. These immutable objects define five methods:

1. holds_always, a predicate which must always return true for this object (and is checked on both creation and consumption), with scope of only the object itself. In a type theoretic formulation, this predicate corresponds to a well-formedness rule, and can be used to implement a “type” of object, colloquially speaking, e.g. int64.
2. holds_on_creation, a predicate which must return true in order for the given immutable object to be created. In a type theoretic formulation, this predicate corresponds to an introduction rule.
3. holds_on_consumption, a predicate which must return true in order for the given immutable object to be consumed. In a type theoretic formulation, this predicate corresponds to an elimination rule.
4. holds_on_transaction, a predicate which must return true in order for the given immutable object to be created or consumed, with scope of the transaction (details TBD, but this would correspond e.g. to the balance check).
5. can_read, a function which (given the object) returns an external identity which should be able to read the object (implying, by exclusion, that any identity not a member of this external identity should not be able to read the object).

These immutable objects can be written by object-level actions – which can query, create, and destroy immutable objects – and read by object-level queries, which can simply read immutable objects (and compute/return some result).

This representation is compiled to a low-level application implementation, with object-level actions roughly corresponding to transaction functions (and other code run in the local domain to generate intents, create proofs, etc.), immutable atomic objects roughly corresponding to resources (although this mapping is not 1-1, it will probably be n-1, where many small objects can be represented by a single resource), and object-level queries roughly corresponding to resource-level queries. The can_read information determines which kinds of proofs are created (when generating proofs / in transaction functions) and who data is encrypted to (and entails that e.g. a shielded RM is used unless all data is totally public).

In the high-level declarative object-level application IR representation:

The high-level declarative object-level application IR representation is currently a grab bag of “nice abstractions that we should be able to compile to immutable objects”, including:

1. Mutable objects (compiled to unique sequences of immutable objects) (this correspondence is described roughly here).
2. Read-only methods on objects which can have different permissions for who is “allowed to call” them (compiled to sets of immutable objects with the appropriate can_read functions).
3. State-level constraints (e.g. kudos total supply is constant) (compiled to holds_on_transaction predicates in immutable objects).
4. Pseudo-objects / views e.g. MyKudosContext, which contains all of my kudos (compiled to object-level actions and object-level queries).
5. Pseudo-methods e.g. MyKudo.send (compiled to object-level actions).
6. Higher-level information flow control properties, e.g. who can call what methods, complex conditions on who should learn what when (compiled to immutable objects / actions / queries).

I imagine that we might want to add more in the future. Many of these transformations are independent and don’t necessarily need to belong in the same “level”, but they all sit between the application interface and the mid-level immutable object IR.

I think the next step here is to try to work out the immutable object-level application IR in detail, but I first want to pause and solicit feedback from folks – particularly @mariari @vveiln – to see if this general approach / structure makes sense.