bitcoin-dev

Simplicity: An alternative to Script

Simplicity: An alternative to Script

Original Postby Mark Friedenbach

Posted on: October 31, 2017 20:46 UTC

Russell O'Connor has presented his work on an alternative to Bitcoin Script named Simplicity at the PLAS 2017 Workshop.

Simplicity is a low-level, typed, functional, native MAST language where programs are built from basic combinators and is designed to operate at the consensus layer. The language comes with formal denotational semantics and formal operational semantics that are both formalized in the Coq proof assistant and proven equivalent. A variant of ECDSA signature verification has been implemented in Simplicity and its correctness will be formally validated along with the associated elliptic curve operations. 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 block weight used, and can reduce space and time resource costs needed for evaluation. Jets replace common Simplicity expressions and directly implement them with C code and are expected to cover arithmetic operations, elliptic curve operations, and cryptographic operations including hashing and digital signature validation. In the long term, Simplicity is expected to have full convent support, allowing access to all transaction data, support for signature aggregation and support for delegation. Simplicity is still in a research and development phase. An SDK will be produced that includes the formal semantics and correctness proofs in Coq, a Haskell implementation for constructing Simplicity programs, and a C interpreter for Simplicity. 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.