How can we formalize a game where each player is a program having access to opponent's code?

Question

How can we define in a proof assistant (eg., Coq) a notion of a 2-player game, where each player is a program that has access to the opponent's source code?

Background: In Open Source Game Theory, we think about bots that reason about each other (prove theorems), knowing the other's source code. I would like implement such bots in a proof assistant, if possible. (https://arxiv.org/pdf/2208.07006.pdf, Open Problem 4)

What I have in mind would looks like this:

Inductive outcome := Cooperate | Defect.
(*  Dupoc is short for Defect Unless Proof of Cooperation   *)
Definition Dupoc (n:N) (bot2 : N -> bot -> outcome) : N -> bot -> outcome :=
    'try for n steps to find a proof that bot2 n self = Cooperate, if found':
        return Cooperate
    else
        return Defect.

The point is that we want to run the agents together with each other as input:

Definition game n1 bot1 n2 bot2 := (bot1 n1 bot2, bo2 n2 bo1).

Of course, the type bot does not exist as I have written it. Is there a way to actually make this happen?

The other problem is that the bot's function is trying to find a proof and returning a bool that reflects the success. Is this possible in some proof assistant? The proof assistant would have to have access to its own inner workings somehow, which seems hard.

I think I could solve the problem by having a Coq implementation in Coq.

Then I could have, like in the paper:

Inductive CoqTokens := ...
Definition BotExpression := ... (* A valid expression for a Bot *)
Class Bot := {
    play : BotExpression -> outcome,
    source : BotExpression (* This should be the source code for 'play' in our Coq-in-Coq implementation *)
}.
Definition game bot1 bot2 := (bot1.play bot2.source, bot2.play bot1.source).

But this seems very much work if it is possible. The Coq implementation in Coq still needs to contain everything about proofing. And I am not sure if it actually solves the problem.

Answer 1

As you found out, the usual technique to solve this kind of difficulty is to introduce a notion of "code" (what you called BotExpression), which expresses the behaviour of your bot. Once you are happy with your codes, you can in a second time define a "decoding" function, something which takes in a code and spits out the expression, but this time as an actual Coq function. Taking the notations from your question, this means that you should be able to define a function that takes in source and outputs play. Note that to do this you do not have to reify all the syntax of Coq. Indeed, the actions available for your bots can probably be defined with a set of primitives smaller than full-fledged Coq. This lets you avoid the problem of using some form of self-description of the meta-language (which are very complicated beasts).

Similarly, you might also want to have such an encoding for proofs, again because your bots need to manipulate "concrete" data rather than meta-proofs in the ambient theory. Regarding formalization of logic, and also to give you ideas on the general code/decoding setting, you might want to give a look at eg. this library formalizing first-order logic.

Finally, there is a second issue you might stumble upon, either in the definition of your decoding function, or that of a play, which is related to the definition of functions in Coq. Indeed, as Coq lets you only define total/terminating functions, quite a lot of things with a "self-recursive" flavour are not definable as functions, as they would lead to non-terminating behaviour. In such a case, a standard solution is to replace the type A -> B by the type A -> B -> Prop, ie. replace an actual function by its graph. This avoids termination issues, and also determinism: since you do not encode a game as a function, you can have multiple choices to move on. Moreover, if you define your relation as an inductive one, you can reason by induction on it, which is probably the kind of reasoning principles you will be after.

Answer 2

Here is a theoretical way you could do this in Lean 4. The key is that you can prove stuff about pure code in Lean. Lean's Declaration and Expr datatypes are pure code I believe, so a lot of work is done for you. Type checking, however, while implemented in Lean 4, is not pure (or I don't think it is), so you would have to write a pure type checker. Automation would also be a lot of work.

import Lean

inductive Outcome
| Cooperate
| Defect

-- A bot is a pure Lean fuction which takes in it's
-- own declaration and that of its opponent to produce an Outcome.
def Bot := Lean.Declaration -> Lean.Declaration -> Outcome

-- Pure code to run the game
def runGame (bot1 bot2 : Bot) (bot1Decl bot2Decl : Lean.Declaration) : Outcome × Outcome :=
  (bot1 bot1Decl bot2Decl, bot2 bot2Decl bot1Decl)

-- -----------------
-- Code needed to build the bots

-- Pure code for checking that a proof expr has the desired type expression.
-- Since type checking in Lean is undecidable, we add a timeout.
-- This code doesn't currently exist in this pure form but it could.
-- Just rewrite enough of the Lean kernel code using pure code and a timeout.
def checkProof (proof : Expr) (expectedType : Expr) (timeout : Nat) : Bool := sorry

-- Pure code for generating the expression
-- `selfBot selfDecl otherDecl = Outcome.Cooperate`
--I don't think this would be hard to write in a pure form.
def cooperateExpr (selfBotDecl otherDecl : Lean.Declaration) : Expr := sorry

-- My cooperate bot
def coorperateBot (selfBotDecl otherDecl : Lean.Declaration) : Outcome := Outcome.Cooperate

-- My bot which sees if the opponent is a simple coorperate bot
def checkIfOpponentIsCooperateBot (selfBotDecl otherBotDecl : Lean.Declaration) : Outcome :=
  -- the thing I'm trying to prove, namely `otherBot otherBotDecl selfBotDecl = Outcome.Cooperate`
  let oppCoopExpr : Lean.Expr := cooperateExpr otherBotDecl selfBotDecl
  -- try the simplest proof, namely `rfl`
  let proof : Lean.Expr := Lean.reflExpr oppCoorExpr  -- not correct code but this can be done
  -- check if proof is valid
  if checkProof proof oppCoopExpr 100 then
    Outcome.Cooperate
  else
    Outcome.Defect

-- Build more complicated bots by extending the logic for
-- `let proof : Expr := ...`
-- one could even implement search procedures
-- however almost all of Lean's automation isn't pure code,
-- so one would have to rewrite it to be pure I believe


-- --------
-- Running the game with the IO monad

-- Unpure meta code to look up the bots declarations and run the game
def runGameIO (bot1 bot2 : Bot) (bot1Name bot2Name : String) : IO (Outcome × Outcome) := do
  let bot1Decl <- Lean.get_decl bot1Name  -- not correct code but this can be done
  let bot2Decl <- Lean.get_decl bot2Name  -- not correct code but this can be done
  return (runGame bot1 bot2 bot1Decl bot2Decl)

def Outcome.repr : Outcome -> String
| Cooperate => "Cooperate"
| Defect => "Defect"

def main : IO Unit := do
  -- run game
  let result <- runGameIO
    coorperateBot checkIfOpponentIsCooperateBot
    "coorperateBot" "checkIfOpponentIsCooperateBot"
  -- print result
  IO.println result.1.repr
  IO.println result.2.repr
```