path: root/97/e68faa74a0673df0c786f8d4352bcc1eb7a3e9

Return-Path: <mark@friedenbach.org>
Received: from smtp1.linuxfoundation.org (smtp1.linux-foundation.org
	[172.17.192.35])
	by mail.linuxfoundation.org (Postfix) with ESMTPS id D6D85D30
	for <bitcoin-dev@lists.linuxfoundation.org>;
	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 <bitcoin-dev@lists.linuxfoundation.org>;
	Mon, 30 Oct 2017 21:56:02 +0000 (UTC)
Received: by mail-pf0-f182.google.com with SMTP id d28so12088887pfe.2
	for <bitcoin-dev@lists.linuxfoundation.org>;
	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 <mark@friedenbach.org>
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: <CAMZUoK=VNRMda8oRCtxniE6-vLwG-b=je2Hx+sD9sCzS--v9kQ@mail.gmail.com>
	<E63C347E-5321-4F7F-B69C-75747E88AC06@mattcorallo.com>
To: Matt Corallo <lf-lists@mattcorallo.com>,
	Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
In-Reply-To: <E63C347E-5321-4F7F-B69C-75747E88AC06@mattcorallo.com>
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 <bitcoin-dev.lists.linuxfoundation.org>
List-Unsubscribe: <https://lists.linuxfoundation.org/mailman/options/bitcoin-dev>,
	<mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=unsubscribe>
List-Archive: <http://lists.linuxfoundation.org/pipermail/bitcoin-dev/>
List-Post: <mailto:bitcoin-dev@lists.linuxfoundation.org>
List-Help: <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=help>
List-Subscribe: <https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev>,
	<mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=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 =
<bitcoin-dev@lists.linuxfoundation.org> 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 =
<bitcoin-dev@lists.linuxfoundation.org> 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 <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 =
<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 <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.
>=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

<html><head><meta http-equiv=3D"Content-Type" content=3D"text/html; =
charset=3Dus-ascii"></head><body style=3D"word-wrap: break-word; =
-webkit-nbsp-mode: space; line-break: after-white-space;" =
class=3D"">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.<br class=3D""><div><br =
class=3D""><blockquote type=3D"cite" class=3D""><div class=3D"">On Oct =
30, 2017, at 2:42 PM, Matt Corallo via bitcoin-dev &lt;<a =
href=3D"mailto:bitcoin-dev@lists.linuxfoundation.org" =
class=3D"">bitcoin-dev@lists.linuxfoundation.org</a>&gt; wrote:</div><br =
class=3D"Apple-interchange-newline"><div class=3D""><div class=3D"">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.<br class=3D"">
<br class=3D"">
Is there some insight I'm missing here?<br class=3D"">
<br class=3D"">
Matt<br class=3D""><br class=3D""><div class=3D"gmail_quote">On October =
30, 2017 11:22:20 AM EDT, Russell O'Connor via bitcoin-dev &lt;<a =
href=3D"mailto:bitcoin-dev@lists.linuxfoundation.org" =
class=3D"">bitcoin-dev@lists.linuxfoundation.org</a>&gt; =
wrote:<blockquote class=3D"gmail_quote" style=3D"margin: 0pt 0pt 0pt =
0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">
<div dir=3D"ltr" class=3D""><div class=3D"">I've
 been working on the design and implementation of an alternative to=20
Bitcoin Script, which I call Simplicity.&nbsp; Today, I am presenting my=20=

design at the <a href=3D"http://plas2017.cse.buffalo.edu/" =
target=3D"_blank" class=3D"">PLAS 2017 Workshop</a> on Programming =
Languages and Analysis for Security.&nbsp; You find a copy of my =
Simplicity paper at <a href=3D"https://blockstream.com/simplicity.pdf" =
target=3D"_blank" class=3D"">https://blockstream.com/<wbr =
class=3D"">simplicity.pdf</a><br class=3D""></div><div class=3D""><br =
class=3D""></div>Simplicity
 is a low-level, typed, functional, native MAST language where programs=20=

are built from basic combinators.&nbsp; Like Bitcoin Script, Simplicity =
is=20
designed to operate at the consensus layer.&nbsp; While one can write=20
Simplicity by hand, it is expected to be the target of one, or multiple,
 front-end languages.<br class=3D""><div class=3D""><br =
class=3D""></div><div class=3D"">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.<br class=3D""><br class=3D""></div>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.&nbsp; 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.<br =
class=3D""><div class=3D""><br class=3D"">Simplicity
 comes with easy to compute static analyses that can compute bounds on=20=

the space and time resources needed for evaluation.&nbsp; 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.</div><div class=3D""><br class=3D""></div><div class=3D"">As a =
native MAST language, unused branches=20
of Simplicity programs are pruned at redemption time.&nbsp; This =
enhances=20
privacy, reduces the block weight used, and can reduce space and time=20
resource costs needed for evaluation.</div><div class=3D""><br =
class=3D""></div><div class=3D"">To make=20
Simplicity practical, jets replace common Simplicity expressions=20
(identified by their MAST root) and directly implement them with C=20
code.&nbsp; 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.<br =
class=3D""></div><div class=3D""><br class=3D""></div><div class=3D"">The
 paper I am presenting at PLAS describes only the foundation of the=20
Simplicity language.&nbsp; The final design includes extensions not =
covered=20
in the paper, including</div><div class=3D""><br class=3D""></div><div =
class=3D"">- full convent support, allowing access to all transaction =
data.</div><div class=3D"">- support for signature =
aggregation.</div><div class=3D"">- support for delegation.</div><div =
class=3D""><br class=3D""></div><div class=3D"">Simplicity is still in a =
research and development phase.&nbsp; I'm working to produce a =
bare-bones SDK that will include <br class=3D""></div><div class=3D""><br =
class=3D""></div><div class=3D"">- the formal semantics and correctness =
proofs in Coq</div><div class=3D"">- a Haskell implementation for =
constructing Simplicity programs</div><div class=3D"">- and a C =
interpreter for Simplicity.<br class=3D""></div><div class=3D""><br =
class=3D""></div><div class=3D"">After an SDK is complete the next step =
will be making Simplicity available in the <a =
href=3D"https://elementsproject.org/" target=3D"_blank" =
class=3D"">Elements project</a>
 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.</div><div class=3D""><br =
class=3D""></div>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.</div>
=
</blockquote></div></div>_______________________________________________<b=
r class=3D"">bitcoin-dev mailing list<br class=3D""><a =
href=3D"mailto:bitcoin-dev@lists.linuxfoundation.org" =
class=3D"">bitcoin-dev@lists.linuxfoundation.org</a><br =
class=3D"">https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev<=
br class=3D""></div></blockquote></div><br class=3D""></body></html>=

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