From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from smtp1.linuxfoundation.org (smtp1.linux-foundation.org [172.17.192.35]) by mail.linuxfoundation.org (Postfix) with ESMTPS id D6D85D30 for ; Mon, 30 Oct 2017 21:56:04 +0000 (UTC) X-Greylist: whitelisted by SQLgrey-1.7.6 Received: from mail-pf0-f182.google.com (mail-pf0-f182.google.com [209.85.192.182]) by smtp1.linuxfoundation.org (Postfix) with ESMTPS id F1E5B483 for ; Mon, 30 Oct 2017 21:56:02 +0000 (UTC) Received: by mail-pf0-f182.google.com with SMTP id d28so12088887pfe.2 for ; Mon, 30 Oct 2017 14:56:02 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=friedenbach-org.20150623.gappssmtp.com; s=20150623; h=from:mime-version:subject:date:references:to:in-reply-to:message-id; bh=S5/kNsY6nCwXuRb0pdmCAomMja+yBr1FkB71cu+2MOU=; b=qZJlu/gUrF+3rA2iNQ+XDYKFpLUNn5jQpNftGYFjU5B5EoP57/CQ34ZZ/iJtyV1Drn B2JANYUpsIYCdjX9z4UsSP1SUtpXp6tNREDH11IrvOFZp2kR8dMN85iak8YV8oZALRtq 33L4BUSEqmlGvq4Uh1mOTltvtI5BwUmu+qrnR3eyUUBZ7AGqqfzUe8032xRygGW87ywP wTFUtUzgeKDIZXQ2wV0MnBNf1qz03ZyR7b+eEXXThWE3+Tpwc6MrwZvDv8Dh4Te6wjwy 99uBr+b6fnh77zW/GSD7gJgXk5fAgZX0Dld3LwLMUQdxKQNn9V+1TIAHAdE0qEKsIEBu X3Mg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:mime-version:subject:date:references:to :in-reply-to:message-id; bh=S5/kNsY6nCwXuRb0pdmCAomMja+yBr1FkB71cu+2MOU=; b=LPLmzfxUGrRV6Zh6FQAO1UUO1YOd0YWXemrrxcBITWN8j/2i0UmUH7T05bUKwugu8c a6h2+LLa9MZJCJZ+XecLiHjPwm/80H9i/FuaN5tCyhOldttHX9ZHs4g5CoyRnOrOQDzo +BrE8JX+IDM+IT/zxRNvxAVjs1ouygJhfgaIv0AuAvq+aX8SxN1TpLdjvpnlHZm9uAYv 3D6ZlISIfh1thpa3tGkdLi7Ic8kA8F0WiWujPWlXZIK2A5hmZ3YmZbRiIds4DxMgXQng qnL1HnBBG84D88L+uQYyzNqrmkI1YG/lCYfNT6oJUIUZf7JS/6+dMAa3J2qDf8hBAATk 6Azw== X-Gm-Message-State: AMCzsaUG/PoX4tPgHUJrtMZ0dKkBMnVUbo64q88gMHht/uWa5ScUYfq+ qXBSsadrSh/WalHsBJivPk+CD/oBDQY= X-Google-Smtp-Source: ABhQp+Q4NFj/cQs/1Z4x3YoN6SOeY5hZnZkxfMDdXbYeXQ8IUXWdRSL+iY0L4wn+BX4emHnXpH5qAg== X-Received: by 10.99.111.65 with SMTP id k62mr8775609pgc.56.1509400562408; Mon, 30 Oct 2017 14:56:02 -0700 (PDT) Received: from [10.1.10.181] (c-73-189-35-88.hsd1.ca.comcast.net. [73.189.35.88]) by smtp.gmail.com with ESMTPSA id c83sm31609343pfk.114.2017.10.30.14.56.01 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 30 Oct 2017 14:56:01 -0700 (PDT) From: Mark Friedenbach Content-Type: multipart/alternative; boundary="Apple-Mail=_27CDD05E-AFE9-4E97-8F62-01E02DAE8157" Mime-Version: 1.0 (Mac OS X Mail 11.0 \(3445.1.7\)) Date: Mon, 30 Oct 2017 14:56:00 -0700 References: To: Matt Corallo , Bitcoin Protocol Discussion In-Reply-To: Message-Id: <64173F46-551E-4C36-A43A-5FBDBFF761CD@friedenbach.org> X-Mailer: Apple Mail (2.3445.1.7) X-Spam-Status: No, score=0.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, HTML_MESSAGE,RCVD_IN_DNSWL_NONE 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:56:04 -0000 --Apple-Mail=_27CDD05E-AFE9-4E97-8F62-01E02DAE8157 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii Script versions makes this no longer a hard-fork to do. The script = version would implicitly encode which jets are optimized, and what their = optimized cost is. > On Oct 30, 2017, at 2:42 PM, Matt Corallo via bitcoin-dev = wrote: >=20 > 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. AFAIU, other similar systems are left doing hard-forks to = reduce the sigops/weight/fee-cost of transactions every time they want = to add useful optimized drop-ins. 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. >=20 > Is there some insight I'm missing here? >=20 > Matt >=20 > 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. Today, I am presenting my = design at the PLAS 2017 Workshop on = Programming Languages and Analysis for Security. You find a copy of my = Simplicity paper at https://blockstream.com/simplicity.pdf = >=20 > 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. >=20 > 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. >=20 > 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. >=20 > 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. >=20 > 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. >=20 > 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. >=20 > 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 >=20 > - full convent support, allowing access to all transaction data. > - support for signature aggregation. > - support for delegation. >=20 > Simplicity is still in a research and development phase. I'm working = to produce a bare-bones SDK that will include=20 >=20 > - the formal semantics and correctness proofs in Coq > - a Haskell implementation for constructing Simplicity programs > - and a C interpreter for Simplicity. >=20 > 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. Only after = extensive vetting would it be suitable to consider Simplicity for = inclusion in Bitcoin. >=20 > 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-dev mailing list > bitcoin-dev@lists.linuxfoundation.org > https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev --Apple-Mail=_27CDD05E-AFE9-4E97-8F62-01E02DAE8157 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=us-ascii Script versions makes this no longer a hard-fork to do. The = script version would implicitly encode which jets are optimized, and = what their optimized cost is.

On Oct = 30, 2017, at 2:42 PM, Matt Corallo via bitcoin-dev <bitcoin-dev@lists.linuxfoundation.org> wrote:

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. AFAIU, other similar systems are left doing hard-forks to = reduce the sigops/weight/fee-cost of transactions every time they want = to add useful optimized drop-ins. 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.

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.linuxfoundation.org> = wrote:
I've been working on the design and implementation of an alternative to=20 Bitcoin Script, which I call Simplicity.  Today, I am presenting my=20= design at the PLAS 2017 Workshop 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=20= are built from basic combinators.  Like Bitcoin Script, Simplicity = is=20 designed to operate at the consensus layer.  While one can write=20 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=20 compute). These are both formalized in the Coq proof assistant and=20 proven equivalent.

Formal = denotational semantics are of=20 limited value unless one can use them in practice to reason about=20 programs. I've used Simplicity's formal semantics to prove correct an=20 implementation of the SHA-256 compression function written in=20 Simplicity.  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.

Simplicity comes with easy to compute static analyses that can compute bounds on=20= the space and time resources needed for evaluation.  This is = important=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.

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

To make=20 Simplicity practical, jets replace common Simplicity expressions=20 (identified by their MAST root) and directly implement them with C=20 code.  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.

The paper I am presenting at PLAS describes only the foundation of the=20 Simplicity language.  The final design includes extensions not = covered=20 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 so that anyone can start experimenting with Simplicity in sidechains.=20= Only after extensive vetting would it be suitable to consider Simplicity for inclusion in Bitcoin.

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.
=
_______________________________________________bitcoin-dev mailing list
bitcoin-dev@lists.linuxfoundation.org
https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev<= br class=3D"">

= --Apple-Mail=_27CDD05E-AFE9-4E97-8F62-01E02DAE8157--