The Round as a Formula: Fair, transparent, real-time multiplayer games with the Tau language

Abstract

This paper is about games in which several parties move at the same time and one step decides the round: a lottery, a pot shared by its players, a bet against a bank, a hand of cards, a move on a board. Such a round is usually a program run by an operator. The method disclosed here makes the round a formula. The round function (inputs, previous state) ↦ (outputs, next state) is written in the temporal logic of the Tau language, created by Ohad Asor [2] and developed by IDNI AG, and the engine evaluates that text step by step; no separately written program states an outcome of the round in the execution. Properties of the round are put to the same engine as queries on the executed lines, each with its expected verdict and, wherever one exists, a negative control; a round is checked by evaluating it again from its recorded inputs and the state before it; the inputs of every party are bound by commitments before any opening, and what follows from a missing opening is a line of the formula. The method is stated for every game whose round can be written as a block of guarded definitions over the inputs of the round and the previous state; that it carries over beyond the games run is a conjecture (§5.7). No single ingredient is new; what is disclosed is their combination and the kind of evidence aimed at. What has been run, on one machine, is this. Nine small programs — dice in several constructions, a lottery, a pot that rolls over, the order in which the parties contribute — put 64 queries to the engine, all answered as expected on the public development branch, two of them with an external synthesis tool. A four-player race game was played 16 times to a win, every printed output equal to that of a reference model by the same author; 42 queries on one to five of its executed lines and seven queries on all lines of a whole round, with four and with eight players, were answered as expected, the queries on the four-player round also on the public branch. Single steps were checked from a recorded state. The same rules ran from 16 to 96 blocks of lines; a lottery with up to 64 tickets, a wheel, the smallest form of a card game, and the smallest forms of two of seven newer designs ran with every value equal to a reference computation. A probe put to the engine shows that an equation between amounts kept in bytes is answered as valid where the amounts are not conserved; the method therefore counts a statement about a payout as decided only as an equation together with the bounds that keep every sum inside the byte. The whole round of the race game was executed only on a build that carries the author's engine changes, which are not merged; there it opens in seconds. On the public branch the run of the same round with 16 blocks did not open under a memory cap of 7.5 GB, while the seven queries on its lines were decided there. One round of the four-player game took a median of 63–81 ms through an in-process host, the evaluation alone. Designed and not run are the binding of the inputs, the signed records, the marks and the settlement in the lines of the whole round, the network execution, and most classes of games. What remains trusted is the operator, who is the only channel, opens last, sets the marks, and can bias the draw, take moves and abort a game; the engine build; and the agreement of the formula with the rule in words (§7).