Proof of Code Execution

Putting it altogether, code is rules and queries, while the compiler (being essentially an autoprover) follows the rules and their consequences and outputs answers (while performing any side-effects). This is a closed loop, the code is retrieved from tau-chain upon a new block, using, obviously, some tau client. So we accept and execute block T by executing the code that appeared at block T-1, while block 0 is the genesis block.

The code of the client should allow users run other tau code according to their preferences. It can be thought as the Appstore/Play application itself, while the network contain many other applications.

Tau does not only provide a decentralized appstore, but delivers additional and essentially more powerful technologies. We mentioned several times the decidability of the code itself and its consequences. Now we’d like to discuss an independent feature which brings more power to tau applications (or the root chain itself).

The autoprover is equipped with mechanism of hashing the proof search tree. The prover basically performs a breadth-first search that begins from the query and takes valid steps (according to the rules in the code), and tries to find facts along the search, and by this finishing a proof (a chain of valid moves from facts to the query).

This tree can be hashed like a Merkle tree. Eventually, the hash of the tree’s root is a proof that the whole computation was followed, since one can replay the computation and verify the hash. There are much more efficient methods than replaying the whole tree, as in lambda-auth which presents the algorithm we intend to implement.

By that, one can prove and verify a local execution of code. Exogenic information (like IO) is treated as Monads, IO is a monad and is not an Auth type. For more information about monads please refer to functional programming literature, but note that this weakness of IO isn’t always a trouble, when a user A knows they’re connecting to server B, they can trust B’s proof of flow that originates from the requests A initiated locally.

How this can elevate crowd computing, and the performance issues arising at this scope, will be a discussion from some other time. Let’s mention some more specific applications for now. One example would be an exchange. The exchange can reveal its own code, and constantly provide proofs that that very code was executed. Another example would be a casino, proving that the whole game indeed followed the rules, including, say, a certain hash computation for random number generation. Also, serving as a DHT or even vanilla Bitcoin client can be proved.

A derived feature is the ability to verify participation on the network itself, one can prove that they ran a tau client, and designers of voting schemes may rely on this ability. It is also possible to automatically award coins given a proof of execution (over say Agoras, but not over non-tau coins like BTC), just like it is possible to set any rules to any proof.
I guess that would be enough to ignite the imagination. The 21st advancements of decentralization, cryptography, provability and verifiable computing, open frontiers to a new kind of networking abilities and experience.