Symbolic Open Games

# Symbolic Open Games This document discusses some potential design choices and possibilities for using SMT solvers to improve the capabilities of the equilibrium checking features in open games. ## Symbolic Equilibrium Checking At a high level the open games equilibrium checker takes: - A game definition - A set of strategies - An initial state - a payoff function for each player The current checking routine does the following: 1. prepares the initial state 1. for each strategy: - hold all other strategies fixed - apply all strategies from previous turns - try every possible move from the current strategy - apply all subsequent strategies against the resulting state - check that the value function is lower for every other move than the one that would have been chosen by the current strategy In the context of small strategies (i.e. where each strategy has a small number of discrete moves), this is sufficient, but in the case where a strategy can choose between many calls to a smart contract, this can quickly explode (e.g. if each possible value of a `uint256` input can be chosen). We can leverage SMT solvers here to cover all possible inputs without having to perform a concrete execution for each possible choice. The approach would look something like this: 1. prepare the initial (concrete) state 1. for each strategy: - hold all other strategies as fixed & concrete - encode the output of the current strategy as a bunch of symbolic variables in SMT - encode the game in question as a set of SMT equations - encode the choices from all previous turns as (concrete) values in SMT - encode all strategies from future turns as functions in SMT - encode the payoff function in SMT - produce an smt term representing the following sequence of actions 1. apply all previous choices to the game 2. apply the current (symbolic) choice to the game 3. apply all future (concrete) strategies against the symbolic state produced by applying the symbolic choice 4. apply the payoff function to the resulting state - ask the solver to find values for the symbolic choice that would produce a higher payoff than that which would have been chosen by the current strategy 3. If all queries return `Unsat` then we know that the current strategy set is in equilibrium ## Checking Infinite Games The above routine checks equilibria for a single round of a given game. We could in theory leverage SMT solvers to check equilibira for games with an infinite number of rounds. This would build upon the routine described above to produce an inductive proof of equilibrium for a given concrete strategy set: 1. Given some initial concrete state, check that equilibrium holds 1. Check equilibrium against some symbolic starting state which is constrained to be already in equilibrium, and check that all possible following states are also in equilibrium We can assert equilibrium by asserting that the payoff function for each player over the prestate could not produce a larger value. **TODO:** does this require quantifiers? (quantifiers in smt are basically unusably slow) ## Implementation Strategies Open games is currently implemented as a DSL in haskell, and games, payoff functions and strategies are all implemented in standard haskell. A full SMT encoding of the haskell language seems infeasible, so there are a few potential implementation routes for a symbolic encoding of open games. There are a few possible options here: ### Write a New DSL A new DSL could be created for strategy / game / payoff definitions. This DSL could be constructed to allow for an easy encoding to SMT. *Advantages* - Language can be customised specifically to allow for easy domain modelling - Users no longer need to learn haskell (intimidating for many) *Disadvantages* - High design & implementation costs - Existing games will need to be translated to the new language ### Use Act as the new DSL Act already has a robust SMT encoding pipeline. Facilities could be added to open games that allow defining strategies / payoffs / games using the act language instead of pure haskell *Advantages* - No need to build a new DSL - Less work? *Disadvantages* - Act may not be the best language for defining payoffs / strategies (it is very focused on function description of smart contracts) - Existing games will need to be translated to make use of the symbolic checker - May be somewhat clunky to mix multiple different DSLs? ### Restrict Definitions to An Easilsy Encodable Subset of Haskell Some minimal subset of haskell could probably be pretty easily encoded into SMT (i.e. functions, simple datatypes, ite expressions, basic arithmetic ops). Pattern matches and ADT's could even be supported, although these features would place some additional load on the solvers compared to the most minimal subset. If all relevant defintions within a game used only this minimal subset of features, template haskell could be utilised to produce an SMT encoding from the haskell AST. Usage of this subset could be enforced via compiile time errors in the existing template haskell parser. *Advantages* - Easiest integration with the current open games infra - Least disruptive change for existing models *Disadvantages* - Would need to write a new SMT encoding (actually fairly easy)