bitcoin-dev
Simplicity: An alternative to Script
Posted on: October 30, 2017 15:31 UTC
Russell O'Connor has designed and implemented an alternative to Bitcoin Script called Simplicity.
This is a low-level, typed, functional, native MAST language that operates at the consensus layer and can be written by hand or be the target of one or multiple front-end languages. Simplicity comes with formal denotational semantics and formal operational semantics, both formalized in the Coq proof assistant and proven equivalent. O'Connor has used Simplicity's formal semantics to prove correct an implementation of the SHA-256 compression function written in Simplicity and has also implemented a variant of ECDSA signature verification in Simplicity. Simplicity comes with easy-to-compute static analyses that can compute bounds on the space and time resources needed for evaluation. As a native MAST language, unused branches of Simplicity programs are pruned at redemption time, enhancing privacy, reducing the block weight used, and reducing space and time resource costs needed for evaluation. Jets replace common Simplicity expressions and directly implement them with C code. There will be a broad set of useful jets covering arithmetic operations, elliptic curve operations, and cryptographic operations including hashing and digital signature validation.The paper presented at PLAS describes only the foundation of the Simplicity language. The final design includes extensions not covered in the paper, including full convent support, support for signature aggregation, and support for delegation. Simplicity is still in the research and development phase. After an SDK is complete, the next step will be making Simplicity available in the Elements project so that anyone can start experimenting with Simplicity in sidechains. Only after extensive vetting would it be suitable to consider Simplicity for inclusion in Bitcoin.