Smart contracts: Turing completeness & reality

The meltdown of “The DAO” and, more recently DDOS attacks on Ethereum have spurred a debate on the wisdom of “Turing completeness” in smart contract languages. , a cryptographic ledger and smart contract platform offers Turing complete smart contracts in a formally specified language (with strong typing and static type checking). We seek to clarify some misconceptions about the relevance of “Turing completeness” in the context of smart contracts. Tezos The theory Alan Turing Turing-completeness is a property indicating that certain (typically, most) programming languages are fully general. According to the (a physics principle with substantial empirical evidence), every computation which can be physically carried out, even in principle, can be expressed and implemented in a Turing-complete language. Church-Turing thesis It does not matter which language. Any Turing-complete language is general enough to emulate all the others (albeit with a potential slowdown), making them equivalent in terms of the computations they can carry out. Turing-complete languages are so pervasive that they even appear in deceptively simple looking systems such as or . cellular automata tiling systems Alonzo Church Unfortunately, with power comes complexity. tells us that, in principle, no procedure (human or mechanical) can decide programs whether they will terminate. In fact, it may not even predict any nontrivial property about their behavior. Rice’s theorem general for all One might be tempted to conclude that since we cannot predict what these programs will do, we should stay clear of such languages. In fact, isn’t this clearly what happened with The DAO? The contract participants weren’t able to predict the behavior of the contract, and catastrophe ensued. This misconception is surprisingly common . Clearly, at least one person, the attacker, was able to predict and understand the contract — better so than its creators in fact. Rice’s theorem asserts that there is no procedure for deciding if the properties about the behavior of a program hold true. These might be properties such as: “does this program halt”, “does it reach an error condition”, “can a certain output ever be produced”. general The theorem implies the existence of programs which terminate, and behave as expected, but not provably so. We cannot really know what they are, but we know they exist through clever mathematical arguments (courtesy of Turing, Church, and Gödel). Importantly, there may be general procedures which can compute the behavior of programs, just not . do do most all Kurt Gödel Some languages forego Turing completeness and their programs be shown always to halt. Such is the case for the Bitcoin script for instance. A folk belief seems to be that the converse of Rice’s theorem is true. Namely, the misconception goes: can “Since the halting problem in Turing complete languages implies that we cannot predict the behavior of programs in general, then, as long as we write our programs in a language that guarantees termination, we’ll be able to predict all the interesting properties we’d like.” This is not true, not in theory, not in practice. There are languages for which programs are guaranteed to halt for all input, but where you may not decide if any given input will cause the program to reach an error condition. (For the theoretically inclined: take for instance the language consisting of a single program f which checks if its input x is a proof of the inconsistency of ZFC. f always halt, but whether or not it ever returns “true” is undecidable in ZFC) The practice In practice, Turing completeness is an idealization. Concretely, computers have a finite amount of memory and will only run for a finite amount of time before being turned off. Tezos (or Ethereum) smart contracts are bounded in time by a limit set per block and per transaction. In some trivial way, they are not quite Turing-complete. Better, since the number of steps in the execution of a contract is bounded, it is theoretically possible to predict the behavior of a given program for any possible input. Since parsing an input takes an amount of time at least commensurate with the length of the input, the cap on the number of steps in the execution bounds the maximal size of any input that the contract may read. The following algorithm can thus decide the behavior of any contract: for(all inputs < max size) {run program for max time;check property;} Of course, this algorithm is astronomically unpractical. If the input size were restricted to a measly kilobyte, there may still not be enough free energy in the universe to carry out the computation. My point here isn’t to show that we can always prove all the true properties of time bounded smart contracts. Quite the opposite, my point is that the existence of a general algorithm and the existence of a algorithm are two very different things. practical Does such an efficient algorithm exist for Bitcoin script? The answer is no as well! Consider the following Bitcoin script scriptPubKey: OP_HASH256 0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef OP_EQUAL This is a hash puzzle, as described on the . Notice that the hash I picked is clearly made up. The script clearly halts for all input, but we might be interested to know if this output is spendable. It all depends if there exists a preimage to the hash I made up, and that is absolutely unclear. We would have to brute force the hash function for billions of years to find out. bitcoin wiki Bitcoin’s script lack of Turing completeness is not a magic bullet. It is of no help in deciding a fundamental property of this very simple script. What really matters As we’ve said before, Rice’s theorem essentially tells us that there exist programs which terminate, and behave as expected, but not provably so. do do However, almost all programs of interest are going to be essentially . Moreover, the proof of their correctness will be relatively straightforward. This is especially true in the context of smart contract on cryptographic ledgers which generally implement simple and straightforward business logic (it is of course less true if you’re dealing with, say, computational algebra). correct provably correct A correctness proof might rely on admitting certain hard to prove conjectures. For instance, we may accept from heuristic arguments that hash functions are indeed hard to invert, and use it as a lemma in our proof, as is generally done in cryptography papers. But overall, whenever a programmer writes a program, they generally keep a vague outline of a proof of correctness in their head. Sometimes that proof is incomplete or wrong — humans are fallible — but it always guides the writing. The programmer constantly reasons about he behavior of their program, to make sure it does what is intended. It just isn’t the case that a programmer sits as their desk and writes, in good faith, a swap contract that destroys all of its pledged collateral if and only if the is true, or is inconsistent. Collatz conjecture ZFC Whether there exists a fully general procedure for deciding if programs written in a given language are correct doesn’t really matter. Rather, what matters is how it is to construct programs which are to reason about. arbitrary straightforward easy In that respect, it generally straightforward to reason about the behavior of Bitcoin scripts. They do not carry much surprise. Is there a preimage t0 0x123… ? Perhaps, perhaps not, but it’s astronomically unlikely that anyone can find out, so for all intent and purposes, the transaction is not spendable. is The tradeoff The efficient frontier, and the new frontier created by automated theorem proving and formal verification Programming languages exist below an expressiveness / ease to reason about frontier. languages make it easy to describe certain desired behavior. While, in principle, all Turing languages can express the same type of computations, in practice, it can be very hard to express certain computations if the language is inadequate. A humorous example is the language. While Malbolge is Turing complete, it is extremely hard to write programs in this language that do what they are intended to do. Expressive Malbolge Like expressiveness, is not a binary variable. Turing completeness has important theoretical and practical implications for the general possibility of reasoning about a language, but as we’ve seen earlier, it does not tell the whole story. ease to reason about Very expressive languages tend to be harder to reason about, while some restricted languages (such as finite state machines) can be very easy to reason about at the cost of expressiveness. There is fortunately a way to push that frontier: formal verification. Formal verification is a rising computer science discipline which produces provably correct programs. You might think of it as creating a machine checkable proof that a program is correct, though, oftentimes, the proof itself a program. Smart contracts have few lines of code, but a lot at stake, making them a perfect candidate for this technique. is In particular, assisted, or even automated, theorem proving lets the programmer specify the properties they want to prove and lets the computer do most of the tedious work of coming up with a formal proof of correctness. This does not affect all languages equally. While it is true that a provably correct program is still provably correct when compiled down to some assembly, it is much harder to derive proofs from the compiled version. This is true for humans, this is true for automated theorem provers. The compilation step throws away vital information about the structure of the program. What we’re doing about it Since Tezos started in the summer of 2014, a core tenet of the project has been that smart-contract languages are a perfect target for formal verification. We wanted a language that would play nicely with theorem provers, but also that could also be easily reasoned about on its own. This led to the following choices: We started with a of the language, to determine precisely and exactly what the program . formal specification meant We made the language strongly typed, with algebraic datatypes and static type checking. Types are a powerful way to reason about the behavior of a program. They can ensure for instance that we do not mistakenly add apples and oranges, but they can be pushed further to enforce certain properties of the contract. We made the language high-level. The contract that participants enter into isn’t some obfuscated assembly, but the language in which the contracts are written. This allows us to introduce useful high level primitives, such as functional maps, and functional sets. Our goal isn’t to build some arbitrary code execution engine, but an engine tailored to the needs of smart-contract writers. All these properties facilitate proving facts about the contracts using automated theorem provers such as the , but they also make it easier to manually check the correctness of the programs. Coq proof assistant Conclusion Turing completeness was framed! There are programs for which properties are easy to understand and prove, and some for which they are difficult. There are programming languages which facilitate such proofs, and some which obscure them. It’s about trade-offs, not about some bright line around the halting problem.