From: "Russell O'Connor" <roconnor@blockstream•io>
To: Bitcoin Protocol Discussion <bitcoin-dev@lists•linuxfoundation.org>
Subject: [bitcoin-dev] Simplicity: An alternative to Script
Date: Mon, 30 Oct 2017 11:22:20 -0400 [thread overview]
Message-ID: <CAMZUoK=VNRMda8oRCtxniE6-vLwG-b=je2Hx+sD9sCzS--v9kQ@mail.gmail.com> (raw)
[-- Attachment #1: Type: text/plain, Size: 3285 bytes --]
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.
[-- Attachment #2: Type: text/html, Size: 3858 bytes --]
next reply other threads:[~2017-10-30 15:22 UTC|newest]
Thread overview: 12+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-10-30 15:22 Russell O'Connor [this message]
2017-10-30 15:31 ` Mark Friedenbach
2017-10-30 21:42 ` Matt Corallo
2017-10-30 21:56 ` Mark Friedenbach
2017-10-30 22:14 ` Matt Corallo
2017-10-30 22:32 ` Mark Friedenbach
2017-10-30 22:50 ` Matt Corallo
2017-10-30 23:29 ` Gregory Maxwell
2017-10-31 20:38 ` Russell O'Connor
2017-10-31 20:46 ` Mark Friedenbach
2017-10-31 21:01 ` Russell O'Connor
2017-11-01 1:46 ` Mark Friedenbach
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to='CAMZUoK=VNRMda8oRCtxniE6-vLwG-b=je2Hx+sD9sCzS--v9kQ@mail.gmail.com' \
--to=roconnor@blockstream$(echo .)io \
--cc=bitcoin-dev@lists$(echo .)linuxfoundation.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox