Return-Path: Received: from smtp1.linuxfoundation.org (smtp1.linux-foundation.org [172.17.192.35]) by mail.linuxfoundation.org (Postfix) with ESMTPS id EC442D32 for ; Mon, 30 Oct 2017 21:42:48 +0000 (UTC) X-Greylist: from auto-whitelisted by SQLgrey-1.7.6 Received: from mail.bluematt.me (mail.bluematt.me [192.241.179.72]) by smtp1.linuxfoundation.org (Postfix) with ESMTPS id 21007483 for ; Mon, 30 Oct 2017 21:42:48 +0000 (UTC) Received: from [IPv6:2607:fb90:7d5:dbf8:1ca1:7f3a:59b0:9f4f] (unknown [172.56.34.81]) by mail.bluematt.me (Postfix) with ESMTPSA id 977A5181075; Mon, 30 Oct 2017 21:42:46 +0000 (UTC) Date: Mon, 30 Oct 2017 21:42:44 +0000 In-Reply-To: References: MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----O9A443LRCGB2UN0REF7PPEDVPHED9K" Content-Transfer-Encoding: 7bit To: Russell O'Connor , Bitcoin Protocol Discussion , Russell O'Connor via bitcoin-dev From: Matt Corallo Message-ID: X-Spam-Status: No, score=0.0 required=5.0 tests=HTML_MESSAGE autolearn=disabled version=3.3.1 X-Spam-Checker-Version: SpamAssassin 3.3.1 (2010-03-16) on smtp1.linux-foundation.org Subject: Re: [bitcoin-dev] Simplicity: An alternative to Script X-BeenThere: bitcoin-dev@lists.linuxfoundation.org X-Mailman-Version: 2.1.12 Precedence: list List-Id: Bitcoin Protocol Discussion List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 30 Oct 2017 21:42:49 -0000 ------O9A443LRCGB2UN0REF7PPEDVPHED9K Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable I admittedly haven't had a chance to read the paper in full details, but I = was curious how you propose dealing with "jets" in something like Bitcoin= =2E AFAIU, other similar systems are left doing hard-forks to reduce the si= gops/weight/fee-cost of transactions every time they want to add useful opt= imized drop-ins=2E For obvious reasons, this seems rather impractical and a= potentially critical barrier to adoption of such optimized drop-ins, which= I imagine would be required to do any new cryptographic algorithms due to = the significant fee cost of interpreting such things=2E Is there some insight I'm missing here? Matt On October 30, 2017 11:22:20 AM EDT, Russell O'Connor via bitcoin-dev wrote: >I've been working on the design and implementation of an alternative to >Bitcoin Script, which I call Simplicity=2E Today, I am presenting my >design >at the PLAS 2017 Workshop on >Programming >Languages and Analysis for Security=2E You find a copy of my Simplicity >paper at https://blockstream=2Ecom/simplicity=2Epdf > >Simplicity is a low-level, typed, functional, native MAST language >where >programs are built from basic combinators=2E Like Bitcoin Script, >Simplicity >is designed to operate at the consensus layer=2E While one can write >Simplicity by hand, it is expected to be the target of one, or >multiple, >front-end languages=2E > >Simplicity comes with formal denotational semantics (i=2Ee=2E semantics o= f >what >programs compute) and formal operational semantics (i=2Ee=2E semantics of >how >programs compute)=2E These are both formalized in the Coq proof assistant >and >proven equivalent=2E > >Formal denotational semantics are of limited value unless one can use >them >in practice to reason about programs=2E I've used Simplicity's formal >semantics to prove correct an implementation of the SHA-256 compression >function written in Simplicity=2E 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=2E > >Simplicity comes with easy to compute static analyses that can compute >bounds on the space and time resources needed for evaluation=2E 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=2E > >As a native MAST language, unused branches of Simplicity programs are >pruned at redemption time=2E This enhances privacy, reduces the block >weight >used, and can reduce space and time resource costs needed for >evaluation=2E > >To make Simplicity practical, jets replace common Simplicity >expressions >(identified by their MAST root) and directly implement them with C >code=2E I >anticipate developing a broad set of useful jets covering arithmetic >operations, elliptic curve operations, and cryptographic operations >including hashing and digital signature validation=2E > >The paper I am presenting at PLAS describes only the foundation of the >Simplicity language=2E The final design includes extensions not covered >in >the paper, including > >- full convent support, allowing access to all transaction data=2E >- support for signature aggregation=2E >- support for delegation=2E > >Simplicity is still in a research and development phase=2E 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=2E > >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=2E Only after extensive >vetting would it be suitable to consider Simplicity for inclusion in >Bitcoin=2E > >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=2E ------O9A443LRCGB2UN0REF7PPEDVPHED9K Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable I admittedly haven't had a chance to read the = paper in full details, but I was curious how you propose dealing with "= ;jets" in something like Bitcoin=2E AFAIU, other similar systems are l= eft doing hard-forks to reduce the sigops/weight/fee-cost of transactions e= very time they want to add useful optimized drop-ins=2E For obvious reasons= , this seems rather impractical and a potentially critical barrier to adopt= ion of such optimized drop-ins, which I imagine would be required to do any= new cryptographic algorithms due to the significant fee cost of interpreti= ng such things=2E

Is there some insight I'm missing here?

Matt

On October 30, 2017 11:22:20 AM EDT= , Russell O'Connor via bitcoin-dev <bitcoin-dev@lists=2Elinuxfoundat= ion=2Eorg> wrote:
I've been working on the design and implementation of an alternative to=20 Bitcoin Script, which I call Simplicity=2E  Today, I am presenting my= =20 design at the PLAS 2017 Workshop on Programming Languages and Analysis for S= ecurity=2E  You find a copy of my Simplicity paper at https://blockstrea= m=2Ecom/simplicity=2Epdf

Simplicity is a low-level, typed, functional, native MAST language where programs=20 are built from basic combinators=2E  Like Bitcoin Script, Simplicity = is=20 designed to operate at the consensus layer=2E  While one can write=20 Simplicity by hand, it is expected to be the target of one, or multiple, front-end languages=2E

Simplicity comes with formal denotational semantics (i=2Ee=2E semantics of what programs comput= e) and formal operational semantics (i=2Ee=2E semantics of how programs=20 compute)=2E These are both formalized in the Coq proof assistant and=20 proven equivalent=2E

Formal denotational semantics are of= =20 limited value unless one can use them in practice to reason about=20 programs=2E I've used Simplicity's formal semantics to prove correct an=20 implementation of the SHA-256 compression function written in=20 Simplicity=2E  I have also implemented a variant of ECDSA signature= =20 verification in Simplicity, and plan to formally validate its=20 correctness along with the associated elliptic curve operations=2E

Simplicity comes with easy to compute static analyses that can compute bounds on=20 the space and time resources needed for evaluation=2E  This is import= ant=20 for both node operators, so that the costs are knows before evaluation,=20 and for designing Simplicity programs, so that smart-contract=20 participants can know the costs of their contract before committing to=20 it=2E

As a native MAST language, unused branche= s=20 of Simplicity programs are pruned at redemption time=2E  This enhance= s=20 privacy, reduces the block weight used, and can reduce space and time=20 resource costs needed for evaluation=2E

To make= =20 Simplicity practical, jets replace common Simplicity expressions=20 (identified by their MAST root) and directly implement them with C=20 code=2E  I anticipate developing a broad set of useful jets covering= =20 arithmetic operations, elliptic curve operations, and cryptographic=20 operations including hashing and digital signature validation=2E

The paper I am presenting at PLAS describes only the foundation of the=20 Simplicity language=2E  The final design includes extensions not cove= red=20 in the paper, including

- full convent support,= allowing access to all transaction data=2E
- support for signatu= re aggregation=2E
- support for delegation=2E

Simplicity is still in a research and development phase=2E  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=2E

= After an SDK is complete the next step will be making Simplicity available = in the Element= s project so that anyone can start experimenting with Simplicity in sidechains=2E= =20 Only after extensive vetting would it be suitable to consider Simplicity for inclusion in Bitcoin=2E

Simplicity has a=20 long ways to go still, and this work is not intended to delay=20 consideration of the various Merkelized Script proposals that are=20 currently ongoing=2E
------O9A443LRCGB2UN0REF7PPEDVPHED9K--