<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body dir="auto">So enthused that this is public now! Great work.&nbsp;<br><br><div id="AppleMailSignature">Sent from my iPhone</div><div><br>On Oct 30, 2017, at 8:22 AM, Russell O'Connor via bitcoin-dev &lt;<a href="mailto:bitcoin-dev@lists.linuxfoundation.org">bitcoin-dev@lists.linuxfoundation.org</a>&gt; wrote:<br><br></div><blockquote type="cite"><div><div dir="ltr"><div>I've
 been working on the design and implementation of an alternative to 
Bitcoin Script, which I call Simplicity.&nbsp; Today, I am presenting my 
design at the <a href="http://plas2017.cse.buffalo.edu/" target="_blank">PLAS 2017 Workshop</a> on Programming Languages and Analysis for Security.&nbsp; You find a copy of my Simplicity paper at <a href="https://blockstream.com/simplicity.pdf" target="_blank">https://blockstream.com/<wbr>simplicity.pdf</a><br></div><div><br></div>Simplicity
 is a low-level, typed, functional, native MAST language where programs 
are built from basic combinators.&nbsp; Like Bitcoin Script, Simplicity is 
designed to operate at the consensus layer.&nbsp; While one can write 
Simplicity by hand, it is expected to be the target of one, or multiple,
 front-end languages.<br><div><br></div><div>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.<br><br></div>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.&nbsp; 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.<br><div><br>Simplicity
 comes with easy to compute static analyses that can compute bounds on 
the space and time resources needed for evaluation.&nbsp; 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.</div><div><br></div><div>As a native MAST language, unused branches 
of Simplicity programs are pruned at redemption time.&nbsp; This enhances 
privacy, reduces the block weight used, and can reduce space and time 
resource costs needed for evaluation.</div><div><br></div><div>To make 
Simplicity practical, jets replace common Simplicity expressions 
(identified by their MAST root) and directly implement them with C 
code.&nbsp; I anticipate developing a broad set of useful jets covering 
arithmetic operations, elliptic curve operations, and cryptographic 
operations including hashing and digital signature validation.<br></div><div><br></div><div>The
 paper I am presenting at PLAS describes only the foundation of the 
Simplicity language.&nbsp; The final design includes extensions not covered 
in the paper, including</div><div><br></div><div>- full convent support, allowing access to all transaction data.</div><div>- support for signature aggregation.</div><div>- support for delegation.</div><div><br></div><div>Simplicity is still in a research and development phase.&nbsp; I'm working to produce a bare-bones SDK that will include <br></div><div><br></div><div>- the formal semantics and correctness proofs in Coq</div><div>- a Haskell implementation for constructing Simplicity programs</div><div>- and a C interpreter for Simplicity.<br></div><div><br></div><div>After an SDK is complete the next step will be making Simplicity available in the <a href="https://elementsproject.org/" target="_blank">Elements project</a>
 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.</div><div><br></div>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.</div>
</div></blockquote><blockquote type="cite"><div><span>_______________________________________________</span><br><span>bitcoin-dev mailing list</span><br><span><a href="mailto:bitcoin-dev@lists.linuxfoundation.org">bitcoin-dev@lists.linuxfoundation.org</a></span><br><span><a href="https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev">https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev</a></span><br></div></blockquote></body></html>