---
title: Realizing intents with a resource model
tags: presentation
type: slide
slideOptions:
theme: solarized
transition: 'fade'
---

# Realizing intents with a resource model

_Christopher Goes
Research Day 2023_

---

## Introduction

----

## Inspiration


*(thanks Andrew Miller!)*

----

## Inspiration part deux


*(thanks Xyn from Flashbots!)*

----

## What this talk is not about

- VMs, but...
- Not your grandma's von Neumann VM.

----

## von Neumann architecture

- Processing unit (CPU)
- Instruction set
- Registers, stack
- Volatile memory
- Non-volatile storage
- Designed to _execute programs sequentially_

----


----

## EVM


*Bonus credit 1: where is this from?*

----

## EVM is a ... von Neumann machine

- Instruction set
- Volatile memory (stack, first 16 = registers)
- Non-volatile storage
- Designed to _execute programs sequentially_

----

## What is a VM, anyways?

- von Neumman VMs are designed to _execute programs sequentially_
- Intent-centric VMs (this talk) are designed to _match conditional commitments atomically_
- Commitments probably involve programs!
- **We'll come back to message-passing and sequential scheduling later

----

## But... Turing-completenesssssssss!


*Bonus credit 2: where is this from?*

---

## Research literature review


----

## A Non-cooperative Equilibrium for Supergames [Friedman 1971]


- Supergame = infinitely repeated game
- Repeated interaction can result in any feasible, individually rational payoff

----

## Program equilibria [Tennenholtz 2004]



----

## What if we just sent around commitments?

- Commitments are functions
- Published to blockchain (somewhere)
- Blockchain (somehow) calculates equilibrium

----

## Four challenges

- Termination / fix-point finding
- Function introspection
- Nominal/structural identities
- Unclear information flow

----

## Termination / fix-point finding

- Higher-order commitments are mutually codependent.

type Commitment = Commitment -> Strategy

- Need randomness, separate payoff, etc. to terminate.

commitment =
    if rand() < 0.01 then Cooperate else
        if other(me) = Cooperate then Cooperate else Defect

- Randomness is possible, but annoying, slow to terminate, adds security assumption.
- Separate payoff creates (arguably unnecessary) MEV.

----

## Function introspection

- Program equilibria use equality checks, but this doesn't work for complex preferences.
- Would need to check arbitrary properties of other's commitment, need e.g. full dependent types.
- Possible, but heavyweight, practical challenges.

----

## Nominal vs. structural identity


- Players (& sometimes commitment devices) are nominally identified (indexed).
- In the typical distributed context, the set of players is open, and we want to identify them _structurally_, by capability.
- e.g. owing a token, ability to make some external move
- We need to explicitly include all actions that matter.

----

## Unclear information flow

- Magic commitment-executing computer
- Has to take all the commitments at once
- Unclear how to compose
- Information flow control (programmable privacy) would require TEE-like embedding

---

## Resource logic to the rescue!

----

## Sequential commitment execution


----

## One weird trick: speculative execution

type Commitment = Set Strategy -> Bool

commitment (Defect, Defect) = True
commitment (Cooperate, Cooperate) = True
commitment _ = False

----

## No one cared about the path anyways


----

## Basic structure: resource

data Change = Created | Consumed

data ResourceLogic = ResourceLogic {
    predicate :: PartialTx -> Change -> Bool,
    arguments :: ByteString
}

data Resource = Resource {
    logic :: ResourceLogic,
    prefix :: ByteString,
    suffix :: Nonce,
    quantity :: Integer,
    value :: ByteString
}

----

## Basic structure: partial transaction

data PartialTx = PartialTx {
    consumed :: Set Resource,
    created :: Set Resource,
    extradata :: ByteString
}

----

## Basic structure: validity

valid ptx@(PartialTx consumed created _) =
    all (map (\r -> logic r ptx Consumed) consumed) &&
    all (map (\r -> logic r ptx Created) created)

----

## Basic structure: balance

type Balance = [(ByteString, Integer)]

denomination :: Resource -> ByteString
denomination (Resource logic prefix _ _ _) =
    hash (logic, prefix)

delta :: Resource -> Balance
delta r = [(denomination r, quantity r)]

balanced :: PartialTx -> Bool
balanced ptx@(PartialTx consumed created _) =
    sum (map delta created) - sum (map delta consumed) = 0

----

## Properties

- Partial transactions compose
- Join consumed and created resources
- If `a` is valid and `b` is valid, `compose(a, b)` is also valid.
- A "transaction" is just a balanced partial transaction

----

## Example: prisonner's dilemma

- Create a resource that says that you cooperate
- Consume a resource that says that your counterparty cooperates
- Symmetric partial transactions will balance

----

## Example: token swap

- Consume the tokens that you already have (& want to pay)
- Create a resource of new tokens assigned to you
- Symmetric partial transactions will balance (maybe with slack)

----

## Addressing termination & introspection

- Separation of computation from verification
- Discontinuous jumps in configuration space

----

## Addressing nominal vs. structural identities

- Interactions are specified on the basis of resources
- Resources connote the ability to do something
- Inclusion of other players is explicit (checked by the predicate in the `PartialTx`, or by balance)

----

## Addressing information flow

- Separation of validity conditions from balance check
- Once you have a valid partial transaction, this can be ZKP'ed (even if still unbalanced)
- Validity constraints "forwarded".

----

## Spicy take

- This resource structure is pretty much inevitable.
- You can still use EVM for program execution if you want.
- But this "virtualised atomic resource logic" will live on top, and programs will be dependent on it.
- EVM's sequential message-passing execution is neither suitable nor necessary for conditional commitments because it is _path-dependent_.

---

## Towards a substrate for information flow control

----

### Viaduct [Recto 2009]


----

### Language vs runtime

- Information flow control language specifies (declaratively)
- Constraints on desired information flow
- Trust assumptions
- Cryptographic assumptions
- etc.
- Compiler selects organisation of primitives
- Runtime executes primitives in correct sequence with real data
- "Least powerful primitive" rule

----

### Example: solver selection

- Users send their partial transactions to known solvers
- Maybe ones they're willing to trust to enforce information flow control policies
- Partial transactions produced by those solvers _compose_

----

### Example: batching ("Penumbra-on-Anoma")

- Consume tokens to create (threshold-encrypted) resources
- Those resources are threshold-decrypted next round
- Those resources can only be consumed in a batch
- Checks fairness condition (optimal arbitrage)

----

### Example: threshold FHE (aggregate statistics)

- Each token spend, increment a threshold encrypted counter
- Validators have instructions to periodically decrypt counter

----

### The case for the resource model

- Clear atomic units of data & logic packaged together
- Information flow control policies can apply to these
- Explicit state inclusion (instead of implicit global state)
- No path-dependence
- Information flow also doesn't care about this, once you know `x`, you can know any `f(x)`

---

## Conclusion and future directions

----

### Three points

1. Intent-centric VM design is not a von Neumman problem.
2. Speculative execution + atomicity is a powerful tool. Users care about equilibria, not paths.
3. The resource model is probably inevitable.

----

### Open questions

- Better formal languages for information flow control
- Particularly ones amenable to conditional disclosure
- Most suitable abstract intermediate representation for programs
- Solver privacy improvements
- (see open questions page)

----

### Thanks!

Find me:
- @cwgoes (while Twitter lasts)
- here :smiley: