Russell O'Connor via bitcoin-dev

2017-10-30 15:22:20 UTC

I've been working on the design and implementation of an alternative to

Bitcoin Script, which I call Simplicity. Today, I am presenting my design

at the PLAS 2017 Workshop <http://plas2017.cse.buffalo.edu/> on Programming

Languages and Analysis for Security. You find a copy of my Simplicity

paper at https://blockstream.com/simplicity.pdf

Simplicity is a low-level, typed, functional, native MAST language where

programs are built from basic combinators. Like Bitcoin Script, Simplicity

is designed to operate at the consensus layer. While one can write

Simplicity by hand, it is expected to be the target of one, or multiple,

front-end languages.

Simplicity comes with formal denotational semantics (i.e. semantics of what

programs compute) and formal operational semantics (i.e. semantics of how

programs compute). These are both formalized in the Coq proof assistant and

proven equivalent.

Formal denotational semantics are of limited value unless one can use them

in practice to reason about programs. I've used Simplicity's formal

semantics to prove correct an implementation of the SHA-256 compression

function written in Simplicity. I have also implemented a variant of ECDSA

signature verification in Simplicity, and plan to formally validate its

correctness 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. This is

important for both node operators, so that the costs are knows before

evaluation, and for designing Simplicity programs, so that smart-contract

participants can know the costs of their contract before committing to it.

As a native MAST language, unused branches of Simplicity programs are

pruned at redemption time. This enhances privacy, reduces the block weight

used, and can reduce space and time resource costs needed for evaluation.

To make Simplicity practical, jets replace common Simplicity expressions

(identified by their MAST root) and directly implement them with C code. I

anticipate developing a broad set of useful jets covering arithmetic

operations, elliptic curve operations, and cryptographic operations

including hashing and digital signature validation.

The paper I am presenting at PLAS describes only the foundation of the

Simplicity language. The final design includes extensions not covered in

the paper, including

- full convent support, allowing access to all transaction data.

- support for signature aggregation.

- support for delegation.

Simplicity is still in a research and development phase. I'm working to

produce a bare-bones SDK that will include

- 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 <https://elementsproject.org/> 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.

Simplicity has a long ways to go still, and this work is not intended to

delay consideration of the various Merkelized Script proposals that are

currently ongoing.

Bitcoin Script, which I call Simplicity. Today, I am presenting my design

at the PLAS 2017 Workshop <http://plas2017.cse.buffalo.edu/> on Programming

Languages and Analysis for Security. You find a copy of my Simplicity

paper at https://blockstream.com/simplicity.pdf

Simplicity is a low-level, typed, functional, native MAST language where

programs are built from basic combinators. Like Bitcoin Script, Simplicity

is designed to operate at the consensus layer. While one can write

Simplicity by hand, it is expected to be the target of one, or multiple,

front-end languages.

Simplicity comes with formal denotational semantics (i.e. semantics of what

programs compute) and formal operational semantics (i.e. semantics of how

programs compute). These are both formalized in the Coq proof assistant and

proven equivalent.

Formal denotational semantics are of limited value unless one can use them

in practice to reason about programs. I've used Simplicity's formal

semantics to prove correct an implementation of the SHA-256 compression

function written in Simplicity. I have also implemented a variant of ECDSA

signature verification in Simplicity, and plan to formally validate its

correctness 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. This is

important for both node operators, so that the costs are knows before

evaluation, and for designing Simplicity programs, so that smart-contract

participants can know the costs of their contract before committing to it.

As a native MAST language, unused branches of Simplicity programs are

pruned at redemption time. This enhances privacy, reduces the block weight

used, and can reduce space and time resource costs needed for evaluation.

To make Simplicity practical, jets replace common Simplicity expressions

(identified by their MAST root) and directly implement them with C code. I

anticipate developing a broad set of useful jets covering arithmetic

operations, elliptic curve operations, and cryptographic operations

including hashing and digital signature validation.

The paper I am presenting at PLAS describes only the foundation of the

Simplicity language. The final design includes extensions not covered in

the paper, including

- full convent support, allowing access to all transaction data.

- support for signature aggregation.

- support for delegation.

Simplicity is still in a research and development phase. I'm working to

produce a bare-bones SDK that will include

- 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 <https://elementsproject.org/> 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.

Simplicity has a long ways to go still, and this work is not intended to

delay consideration of the various Merkelized Script proposals that are

currently ongoing.