path: root/ab/13ff627576c07329f458e8afc1739874cecf6f

Return-Path: <roconnor@blockstream.io>
Received: from smtp1.linuxfoundation.org (smtp1.linux-foundation.org
	[172.17.192.35])
	by mail.linuxfoundation.org (Postfix) with ESMTPS id 697F3CE3
	for <bitcoin-dev@lists.linuxfoundation.org>;
	Tue, 31 Oct 2017 20:38:39 +0000 (UTC)
X-Greylist: whitelisted by SQLgrey-1.7.6
Received: from mail-ua0-f174.google.com (mail-ua0-f174.google.com
	[209.85.217.174])
	by smtp1.linuxfoundation.org (Postfix) with ESMTPS id 50F3A1A0
	for <bitcoin-dev@lists.linuxfoundation.org>;
	Tue, 31 Oct 2017 20:38:38 +0000 (UTC)
Received: by mail-ua0-f174.google.com with SMTP id z4so195858uaz.5
	for <bitcoin-dev@lists.linuxfoundation.org>;
	Tue, 31 Oct 2017 13:38:38 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
	d=blockstream-io.20150623.gappssmtp.com; s=20150623;
	h=mime-version:in-reply-to:references:from:date:message-id:subject:to
	:cc; bh=mEoe+Ot2hAxwF7QbPP12QuRrOOg4CHonKMlJ7hTA4xM=;
	b=iNGo7XfKh3mcC8Me0vJF/j7RfU/AxcpL+mw+ywLcRiokM9SKN5AtCYM03PES1x5mxr
	Rf2bCCWUudY44ryLepJrgO67SHDnjFa8zP6VoNokh912ExCx7OtCfdvnXfDXX8PJmbnl
	/QN1SrjhO9Id7zgOlZZkwDwsQPgprdl7bs5/KEXeS0u/HBiDvxkU9G4oRk+qVXVBackO
	7q2sg3ds68Zlw8QLjv2XGgB2GEH4Prmg6KTp3rqxa1nXsFMNDAey7nOXPmuci+UXhiMo
	iDjm6sjefJcR4z7pPIzH9eYf/jD1sci04ndwslBQIxCt3AvjjZoNgmlSljCi2V1MrxfW
	z9Pw==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
	d=1e100.net; s=20161025;
	h=x-gm-message-state:mime-version:in-reply-to:references:from:date
	:message-id:subject:to:cc;
	bh=mEoe+Ot2hAxwF7QbPP12QuRrOOg4CHonKMlJ7hTA4xM=;
	b=bNfhlgtEmxbWpFqZLb6Kh5vRiwmLs3v5ZDb49WywQNuOwKsqECIb5Mpw3IWqPFk0ID
	e/VXQbA4rwoJwbgjM4V3VVCDdOi1s7sf0LPW11xXtDZGZRif1DNL0CZ+iu+Izemz7BG8
	AR0LpGRwZf+xBx/vhIjE5SJIzIvPJCrbYP1cecBuqRKOufxyaq3lLtnSBHQjhRBX3Wex
	gJ9A3d6pbnKywAxt+ky3Gn9hx0KBxG9jLrf1/7Lr7hmFM7+dXyiUGYA3gRF6qXBtUiR6
	qk71p1lOQX3Dm9eT2a1h99PyoiADvuz9TOIHXb6x3ozT0c91osiH+R+KRvPfClu2rM2F
	g7ew==
X-Gm-Message-State: AMCzsaVQ7beILvblUu4U2/ToraMYGN6zmaoahBV0R2fbhFNgjBhihCBu
	FYG1QIT39E2h4oeavxn7MR3+leviwuo8fFlMYpb0Cg==
X-Google-Smtp-Source: ABhQp+SozBjQR1q6GZStD52kvsgZbst7LxnPt0vQrcAvAie+md2ID1iD+XmEH6hIx+0FYghwpxkVQYcc/fVNGKI3MCY=
X-Received: by 10.176.80.3 with SMTP id b3mr2808429uaa.1.1509482317319; Tue,
	31 Oct 2017 13:38:37 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.176.73.202 with HTTP; Tue, 31 Oct 2017 13:38:16 -0700 (PDT)
In-Reply-To: <E63C347E-5321-4F7F-B69C-75747E88AC06@mattcorallo.com>
References: <CAMZUoK=VNRMda8oRCtxniE6-vLwG-b=je2Hx+sD9sCzS--v9kQ@mail.gmail.com>
	<E63C347E-5321-4F7F-B69C-75747E88AC06@mattcorallo.com>
From: "Russell O'Connor" <roconnor@blockstream.io>
Date: Tue, 31 Oct 2017 16:38:16 -0400
Message-ID: <CAMZUoKmos5BMkFNsmNnTJhryfho_0fGhSKDQ82D6SPjPBhvd0A@mail.gmail.com>
To: Matt Corallo <lf-lists@mattcorallo.com>
Content-Type: multipart/alternative; boundary="94eb2c18ee3e51a8c0055cddbd3f"
X-Spam-Status: No, score=0.5 required=5.0 tests=DKIM_SIGNED,DKIM_VALID,
	HTML_MESSAGE,RCVD_IN_DNSWL_NONE,RCVD_IN_SORBS_SPAM autolearn=disabled
	version=3.3.1
X-Spam-Checker-Version: SpamAssassin 3.3.1 (2010-03-16) on
	smtp1.linux-foundation.org
Cc: Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.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: Tue, 31 Oct 2017 20:38:39 -0000

--94eb2c18ee3e51a8c0055cddbd3f
Content-Type: text/plain; charset="UTF-8"

(sorry, I forgot to reply-all earlier)

The very short answer to this question is that I plan on using Luke's
fail-success-on-unknown-operation in Simplicity.  This is something that
isn't detailed at all in the paper.

The plan is that discounted jets will be explicitly labeled as jets in the
commitment.  If you can provide a Merkle path from the root to a node that
is an explicit jet, but that jet isn't among the finite number of known
discounted jets, then the script is automatically successful (making it
anyone-can-spend).  When new jets are wanted they can be soft-forked into
the protocol (for example if we get a suitable quantum-resistant digital
signature scheme) and the list of known discounted jets grows.  Old nodes
get a merkle path to the new jet, which they view as an unknown jet, and
allow the transaction as a anyone-can-spend transaction.  New nodes see a
regular Simplicity redemption.  (I haven't worked out the details of how
the P2P protocol will negotiate with old nodes, but I don't forsee any
problems.)

Note that this implies that you should never participate in any Simplicity
contract where you don't get access to the entire source code of all
branches to check that it doesn't have an unknown jet.

On Mon, Oct 30, 2017 at 5:42 PM, Matt Corallo <lf-lists@mattcorallo.com>
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
>> 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.
>>
>

--94eb2c18ee3e51a8c0055cddbd3f
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>(sorry, I forgot to reply-all earlier)<br></div><div>=
<br></div><div>The very short answer to this question is that I plan on usi=
ng Luke&#39;s fail-success-on-unknown-<wbr>operation in Simplicity.=C2=A0 T=
his is something that isn&#39;t detailed at all in the paper.</div><div><br=
></div><div>The
 plan is that discounted jets will be explicitly labeled as jets in the=20
commitment.=C2=A0 If you can provide a Merkle path from the root to a node=
=20
that is an explicit jet, but that jet isn&#39;t among the finite number of=
=20
known discounted jets, then the script is automatically successful=20
(making it anyone-can-spend).=C2=A0 When new jets are wanted they can be=20
soft-forked into the protocol (for example if we get a suitable=20
quantum-resistant digital signature scheme) and the list of known=20
discounted jets grows.=C2=A0 Old nodes get a merkle path to the new jet,=20
which they view as an unknown jet, and allow the transaction as a=20
anyone-can-spend transaction.=C2=A0 New nodes see a regular Simplicity=20
redemption.=C2=A0 (I haven&#39;t worked out the details of how the P2P prot=
ocol=20
will negotiate with old nodes, but I don&#39;t forsee any problems.)</div><=
div><br></div><div>Note
 that this implies that you should never participate in any Simplicity=20
contract where you don&#39;t get access to the entire source code of all=20
branches to check that it doesn&#39;t have an unknown jet.</div></div><div =
class=3D"gmail_extra"><br><div class=3D"gmail_quote">On Mon, Oct 30, 2017 a=
t 5:42 PM, Matt Corallo <span dir=3D"ltr">&lt;<a href=3D"mailto:lf-lists@ma=
ttcorallo.com" target=3D"_blank">lf-lists@mattcorallo.com</a>&gt;</span> wr=
ote:<br><blockquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border=
-left:1px #ccc solid;padding-left:1ex"><div>I admittedly haven&#39;t had a =
chance to read the paper in full details, but I was curious how you propose=
 dealing with &quot;jets&quot; in something like Bitcoin. AFAIU, other simi=
lar 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 b=
arrier to adoption of such optimized drop-ins, which I imagine would be req=
uired to do any new cryptographic algorithms due to the significant fee cos=
t of interpreting such things.<br>
<br>
Is there some insight I&#39;m missing here?<span class=3D"HOEnZb"><font col=
or=3D"#888888"><br>
<br>
Matt</font></span><div><div class=3D"h5"><br><br><div class=3D"gmail_quote"=
>On October 30, 2017 11:22:20 AM EDT, Russell O&#39;Connor via bitcoin-dev =
&lt;<a href=3D"mailto:bitcoin-dev@lists.linuxfoundation.org" target=3D"_bla=
nk">bitcoin-dev@lists.<wbr>linuxfoundation.org</a>&gt; wrote:<blockquote cl=
ass=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"><div>I&#39;ve
 been working on the design and implementation of an alternative to=20
Bitcoin Script, which I call Simplicity.=C2=A0 Today, I am presenting my=20
design at the <a href=3D"http://plas2017.cse.buffalo.edu/" target=3D"_blank=
">PLAS 2017 Workshop</a> on Programming Languages and Analysis for Security=
.=C2=A0 You find a copy of my Simplicity paper at <a href=3D"https://blocks=
tream.com/simplicity.pdf" target=3D"_blank">https://blockstream.com/simpli<=
wbr>city.pdf</a><br></div><div><br></div>Simplicity
 is a low-level, typed, functional, native MAST language where programs=20
are built from basic combinators.=C2=A0 Like Bitcoin Script, Simplicity is=
=20
designed to operate at the consensus layer.=C2=A0 While one can write=20
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=20
compute). These are both formalized in the Coq proof assistant and=20
proven equivalent.<br><br></div>Formal denotational semantics are of=20
limited value unless one can use them in practice to reason about=20
programs. I&#39;ve used Simplicity&#39;s formal semantics to prove correct =
an=20
implementation of the SHA-256 compression function written in=20
Simplicity.=C2=A0 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><div><b=
r>Simplicity
 comes with easy to compute static analyses that can compute bounds on=20
the space and time resources needed for evaluation.=C2=A0 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><br></div><div>As a native MAST language, unused branches=20
of Simplicity programs are pruned at redemption time.=C2=A0 This enhances=
=20
privacy, reduces the block weight used, and can reduce space and time=20
resource costs needed for evaluation.</div><div><br></div><div>To make=20
Simplicity practical, jets replace common Simplicity expressions=20
(identified by their MAST root) and directly implement them with C=20
code.=C2=A0 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></div><di=
v><br></div><div>The
 paper I am presenting at PLAS describes only the foundation of the=20
Simplicity language.=C2=A0 The final design includes extensions not covered=
=20
in the paper, including</div><div><br></div><div>- full convent support, al=
lowing access to all transaction data.</div><div>- support for signature ag=
gregation.</div><div>- support for delegation.</div><div><br></div><div>Sim=
plicity is still in a research and development phase.=C2=A0 I&#39;m working=
 to produce a bare-bones SDK that will include <br></div><div><br></div><di=
v>- the formal semantics and correctness proofs in Coq</div><div>- a Haskel=
l implementation for constructing Simplicity programs</div><div>- and a C i=
nterpreter for Simplicity.<br></div><div><br></div><div>After an SDK is com=
plete the next step will be making Simplicity available in the <a href=3D"h=
ttps://elementsproject.org/" target=3D"_blank">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><br></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></div></div></blockquote></div><br></div>

--94eb2c18ee3e51a8c0055cddbd3f--