# 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. ```haskell= type Commitment = Commitment -> Strategy ``` - Need randomness, separate payoff, etc. to terminate. ```haskell= 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 ```haskell= 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 ```haskell= 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 ```haskell= data PartialTx = PartialTx { consumed :: Set Resource, created :: Set Resource, extradata :: ByteString } ``` ---- ## Basic structure: validity ```haskell= valid ptx@(PartialTx consumed created _) = all (map (\r -> logic r ptx Consumed) consumed) && all (map (\r -> logic r ptx Created) created) ``` ---- ## Basic structure: balance ```haskell= 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: