bitcoin-dev
Simplicity: An alternative to Script
Posted on: October 30, 2017 22:14 UTC
In a recent Bitcoin-dev mailing list, Mark Friedenbach proposed Script versions as a solution to deal with "jets" in Bitcoin.
He suggested that the script version would encode which jets are optimized and what their optimized cost is, making it no longer a hard-fork. In response to this, Matt Corallo raised concerns that adding new script operations and using a full 32 byte hash to represent them might be wasteful. He also questioned whether an aggressive soft-fork cadence would be practical at the moment. Meanwhile, Russell O'Connor presented Simplicity, an alternative to Bitcoin Script, at the PLAS 2017 Workshop on Programming Languages and Analysis for Security. Simplicity is a low-level, typed, functional, native MAST language designed to operate at the consensus layer like Bitcoin Script. It comes with formal denotational semantics and formal operational semantics formalized in Coq proof assistant and proven equivalent. Simplicity's formal semantics have been used to prove the correctness of an implementation of the SHA-256 compression function written in Simplicity. Simplicity has easy-to-compute static analyses that can compute bounds on the space and time resources needed for evaluation. Unused branches of Simplicity programs are pruned at redemption time, enhancing privacy, reducing block weight, and saving space and time resource costs needed for evaluation. Jets replace common Simplicity expressions and directly implement them with C code, covering arithmetic operations, elliptic curve operations, and cryptographic operations including hashing and digital signature validation. The final design of Simplicity includes extensions not covered in the paper, such as full convent support, support for signature aggregation, and support for delegation. While Simplicity is still in research and development phase, O'Connor is working to produce a bare-bones SDK that includes the formal semantics and correctness proofs in Coq, a Haskell implementation for constructing Simplicity programs, and a C interpreter for Simplicity. After the SDK is complete, the next step will be making Simplicity available in the Elements project for experimentation with Simplicity in sidechains. However, O'Connor stressed that this work is not intended to delay consideration of various Merkelized Script proposals that are currently ongoing.