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
  Image Not Showing Possible Reasons

  • The image file may be corrupted
  • The server hosting the image is unavailable
  • The image path is incorrect
  • The image format is not supported

  Learn More →