path: root/2c/5b3489f3a3b6d6116d4f59756b802296ed04d7

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 AACD99F0
	for <bitcoin-dev@lists.linuxfoundation.org>;
	Wed,  1 Nov 2017 01:46:59 +0000 (UTC)
X-Greylist: whitelisted by SQLgrey-1.7.6
Received: from mail-pf0-f175.google.com (mail-pf0-f175.google.com
	[209.85.192.175])
	by smtp1.linuxfoundation.org (Postfix) with ESMTPS id 8A1331CE
	for <bitcoin-dev@lists.linuxfoundation.org>;
	Wed,  1 Nov 2017 01:46:57 +0000 (UTC)
Received: by mail-pf0-f175.google.com with SMTP id e64so713444pfk.9
	for <bitcoin-dev@lists.linuxfoundation.org>;
	Tue, 31 Oct 2017 18:46:57 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
	d=friedenbach-org.20150623.gappssmtp.com; s=20150623;
	h=mime-version:subject:from:in-reply-to:date:cc
	:content-transfer-encoding:message-id:references:to;
	bh=yzqKd7hL0IX/WuEbt8IDCnK/jzqm5Xn1+BJrnwAAnk0=;
	b=rR71lkITB+GubnTMLm6NjGbUI5rrOLKMMxw6IhkxWwAtNk1U+DWKrgQCwTBVZ0u2vY
	22L7wB7KFJcBYl0ThgVy2IN1AzH1cSPKk3o7NAFeXNIrQhZHQILJOyDBfo+bHfklcPQZ
	bJSM5AQdiGV9ioBQ8mGofzVhUQYPRtSXl6jHzzkxBcViFT7vs4eGN0b20sNYimfD+zOe
	rbxbkdc4fN8/nABQ72ENV+fSgAgJmOI4KOfa/G8L5LmGTawL+qW/wVIyTJl/oG/1adzu
	YkqNkZvNf+KFh4OAYZGoJTOwf1izE7ortAGKrsVOm0Wssr9DcxZrwd0JqHEjITlIvY+3
	JAzg==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
	d=1e100.net; s=20161025;
	h=x-gm-message-state:mime-version:subject:from:in-reply-to:date:cc
	:content-transfer-encoding:message-id:references:to;
	bh=yzqKd7hL0IX/WuEbt8IDCnK/jzqm5Xn1+BJrnwAAnk0=;
	b=NjZE7zH+zq8fYLRP9QOb0skYxiiWU/u9eMC9ph+EUhYaETeQ+QVZfIEgqASJg90DAP
	o5uBAkXDEVIWxHCuOZTysytTHsf+Q7ImtXE70ExLdr42/hiRNI8GXKsJaJxrD/IEdjjx
	s/rTz4yYVL3o7j7rGOKiihUN00BOhpFBqFjJ79m/9Hd1zKcs6bFlQ3Y/Jjv3+xd1cYrZ
	r9O9CJ8pzYyAtloHdRwF1q4g6RkLzwQJbBiuSJ/H+vdYK+CqtL+8fnthxAZ6bcMgTLyq
	EEdq41djSxDW/gT5v1PLI0q92kP3QFEJbXyjMBIM+/WRARyJ4WwmU+mR/XEiNr6t2cF9
	tafw==
X-Gm-Message-State: AMCzsaVAcjy2jnvmteUw//gQiUZq8+pfxFMwiNHZckN/7V1wAfrkfYlD
	w+XESg5RDabFB9YiSyZae9Z874EFBqM=
X-Google-Smtp-Source: ABhQp+SWPfnzec0tAAn3mZcgHwv58YRMDD6ivL8TDaBID70gkvSiPipDprJ6X/Gdo+L4R2ADCbPATQ==
X-Received: by 10.98.64.75 with SMTP id n72mr4307123pfa.317.1509500817064;
	Tue, 31 Oct 2017 18:46:57 -0700 (PDT)
Received: from ?IPv6:2601:647:4600:9c66:6d98:5b00:7f2d:b007?
	([2601:647:4600:9c66:6d98:5b00:7f2d:b007])
	by smtp.gmail.com with ESMTPSA id
	n72sm4580728pfg.109.2017.10.31.18.46.55
	(version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
	Tue, 31 Oct 2017 18:46:56 -0700 (PDT)
Content-Type: multipart/alternative;
	boundary=Apple-Mail-153FE09F-10A7-4DDA-8DA3-C203951615D5
Mime-Version: 1.0 (1.0)
From: Mark Friedenbach <mark@friedenbach.org>
X-Mailer: iPhone Mail (15A432)
In-Reply-To: <CAMZUoKmNEaTEoHV6cWOdLR=G9XiqTQ9AmHhyxegVEEmXVhU+7w@mail.gmail.com>
Date: Tue, 31 Oct 2017 18:46:54 -0700
Content-Transfer-Encoding: 7bit
Message-Id: <5E7A6643-C478-44EC-BC54-404D86D1D151@friedenbach.org>
References: <CAMZUoK=VNRMda8oRCtxniE6-vLwG-b=je2Hx+sD9sCzS--v9kQ@mail.gmail.com>
	<E63C347E-5321-4F7F-B69C-75747E88AC06@mattcorallo.com>
	<CAMZUoKmos5BMkFNsmNnTJhryfho_0fGhSKDQ82D6SPjPBhvd0A@mail.gmail.com>
	<CAOG=w-vsTCTNW9x5TCHChN6_13pAabWjDQ30Eoo4xQduJ01fdQ@mail.gmail.com>
	<CAMZUoKmNEaTEoHV6cWOdLR=G9XiqTQ9AmHhyxegVEEmXVhU+7w@mail.gmail.com>
To: Russell O'Connor <roconnor@blockstream.io>
X-Spam-Status: No, score=0.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID,
	HTML_MESSAGE,MIME_QP_LONG_LINE,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
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: Wed, 01 Nov 2017 01:46:59 -0000


--Apple-Mail-153FE09F-10A7-4DDA-8DA3-C203951615D5
Content-Type: text/plain;
	charset=gb2312
Content-Transfer-Encoding: quoted-printable

I don=A1=AFt think you need to set an order of operations, just treat the je=
t as TRUE, but don=A1=AFt stop validation. Order of operations doesn=A1=AFt m=
atter. Either way it=A1=AFll execute both branches and terminate of the unde=
rstood conditions don=A1=AFt hold.

But maybe I=A1=AFm missing something here.=20

> On Oct 31, 2017, at 2:01 PM, Russell O'Connor <roconnor@blockstream.io> wr=
ote:
>=20
> That approach is worth considering.  However there is a wrinkle that Simpl=
icity's denotational semantics doesn't imply an order of operations.  For ex=
ample, if one half of a pair contains a assertion failure (fail-closed), and=
 the other half contains a unknown jet (fail-open), then does the program su=
cceed or fail?
>=20
> This could be solved by providing an order of operations; however I fear t=
hat will complicate formal reasoning about Simplicity expressions.  Formal r=
easoning is hard enough as is and I hesitate to complicate the semantics in w=
ays that make formal reasoning harder still.
>=20
>=20
> On Oct 31, 2017 15:47, "Mark Friedenbach" <mark@friedenbach.org> wrote:
> Nit, but if you go down that specific path I would suggest making just
> the jet itself fail-open. That way you are not so limited in requiring
> validation of the full contract -- one party can verify simply that
> whatever condition they care about holds on reaching that part of the
> contract. E.g. maybe their signature is needed at the top level, and
> then they don't care what further restrictions are placed.
>=20
> On Tue, Oct 31, 2017 at 1:38 PM, Russell O'Connor via bitcoin-dev
> <bitcoin-dev@lists.linuxfoundation.org> wrote:
> > (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 t=
he
> > commitment.  If you can provide a Merkle path from the root to a node th=
at
> > 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 int=
o
> > the protocol (for example if we get a suitable quantum-resistant digital=

> > signature scheme) and the list of known discounted jets grows.  Old node=
s
> > 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 Simplici=
ty
> > 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, bu=
t I
> >> was curious how you propose dealing with "jets" in something like Bitco=
in.
> >> AFAIU, other similar systems are left doing hard-forks to reduce the
> >> sigops/weight/fee-cost of transactions every time they want to add usef=
ul
> >> optimized drop-ins. For obvious reasons, this seems rather impractical a=
nd a
> >> potentially critical barrier to adoption of such optimized drop-ins, wh=
ich 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 t=
o
> >>> Bitcoin Script, which I call Simplicity.  Today, I am presenting my de=
sign
> >>> 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 whe=
re
> >>> programs are built from basic combinators.  Like Bitcoin Script, Simpl=
icity
> >>> 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 multipl=
e,
> >>> front-end languages.
> >>>
> >>> Simplicity comes with formal denotational semantics (i.e. semantics of=

> >>> what programs compute) and formal operational semantics (i.e. semantic=
s of
> >>> how programs compute). These are both formalized in the Coq proof assi=
stant
> >>> 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 form=
al
> >>> semantics to prove correct an implementation of the SHA-256 compressio=
n
> >>> function written in Simplicity.  I have also implemented a variant of E=
CDSA
> >>> signature verification in Simplicity, and plan to formally validate it=
s
> >>> 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-contr=
act
> >>> 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 w=
eight
> >>> used, and can reduce space and time resource costs needed for evaluati=
on.
> >>>
> >>> To make Simplicity practical, jets replace common Simplicity expressio=
ns
> >>> (identified by their MAST root) and directly implement them with C cod=
e.  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 t=
o
> >>> 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 experimenti=
ng
> >>> with Simplicity in sidechains. Only after extensive vetting would it b=
e
> >>> suitable to consider Simplicity for inclusion in Bitcoin.
> >>>
> >>> Simplicity has a long ways to go still, and this work is not intended t=
o
> >>> delay consideration of the various Merkelized Script proposals that ar=
e
> >>> currently ongoing.
> >
> >
> >
> > _______________________________________________
> > bitcoin-dev mailing list
> > bitcoin-dev@lists.linuxfoundation.org
> > https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
> >
>=20

--Apple-Mail-153FE09F-10A7-4DDA-8DA3-C203951615D5
Content-Type: text/html;
	charset=utf-8
Content-Transfer-Encoding: quoted-printable

<html><head><meta http-equiv=3D"content-type" content=3D"text/html; charset=3D=
utf-8"></head><body dir=3D"auto">I don=E2=80=99t think you need to set an or=
der of operations, just treat the jet as TRUE, but don=E2=80=99t stop valida=
tion. Order of operations doesn=E2=80=99t matter. Either way it=E2=80=99ll e=
xecute both branches and terminate of the understood conditions don=E2=80=99=
t hold.<br><br><div>But maybe I=E2=80=99m missing something here.&nbsp;</div=
><div><br>On Oct 31, 2017, at 2:01 PM, Russell O'Connor &lt;<a href=3D"mailt=
o:roconnor@blockstream.io">roconnor@blockstream.io</a>&gt; wrote:<br><br></d=
iv><blockquote type=3D"cite"><div><div dir=3D"auto"><div>That approach is wo=
rth considering.&nbsp; However there is a wrinkle that Simplicity's denotati=
onal semantics doesn't imply an order of operations.&nbsp; For example, if o=
ne half of a pair contains a assertion failure (fail-closed), and the other h=
alf contains a unknown jet (fail-open), then does the program succeed or fai=
l?<div dir=3D"auto"><br></div><div dir=3D"auto">This could be solved by prov=
iding an order of operations; however I fear that will complicate formal rea=
soning about Simplicity expressions.&nbsp; Formal reasoning is hard enough a=
s is and I hesitate to complicate the semantics in ways that make formal rea=
soning harder still.</div><br><div class=3D"gmail_extra"><br><div class=3D"g=
mail_quote">On Oct 31, 2017 15:47, "Mark Friedenbach" &lt;<a href=3D"mailto:=
mark@friedenbach.org">mark@friedenbach.org</a>&gt; wrote:<br type=3D"attribu=
tion"><blockquote class=3D"quote" style=3D"margin:0 0 0 .8ex;border-left:1px=
 #ccc solid;padding-left:1ex">Nit, but if you go down that specific path I w=
ould suggest making just<br>
the jet itself fail-open. That way you are not so limited in requiring<br>
validation of the full contract -- one party can verify simply that<br>
whatever condition they care about holds on reaching that part of the<br>
contract. E.g. maybe their signature is needed at the top level, and<br>
then they don't care what further restrictions are placed.<br>
<br>
On Tue, Oct 31, 2017 at 1:38 PM, Russell O'Connor via bitcoin-dev<br>
<div class=3D"elided-text">&lt;<a href=3D"mailto:bitcoin-dev@lists.linuxfoun=
dation.org">bitcoin-dev@lists.<wbr>linuxfoundation.org</a>&gt; wrote:<br>
&gt; (sorry, I forgot to reply-all earlier)<br>
&gt;<br>
&gt; The very short answer to this question is that I plan on using Luke's<b=
r>
&gt; fail-success-on-unknown-<wbr>operation in Simplicity.&nbsp; This is som=
ething that<br>
&gt; isn't detailed at all in the paper.<br>
&gt;<br>
&gt; The plan is that discounted jets will be explicitly labeled as jets in t=
he<br>
&gt; commitment.&nbsp; If you can provide a Merkle path from the root to a n=
ode that<br>
&gt; is an explicit jet, but that jet isn't among the finite number of known=
<br>
&gt; discounted jets, then the script is automatically successful (making it=
<br>
&gt; anyone-can-spend).&nbsp; When new jets are wanted they can be soft-fork=
ed into<br>
&gt; the protocol (for example if we get a suitable quantum-resistant digita=
l<br>
&gt; signature scheme) and the list of known discounted jets grows.&nbsp; Ol=
d nodes<br>
&gt; get a merkle path to the new jet, which they view as an unknown jet, an=
d<br>
&gt; allow the transaction as a anyone-can-spend transaction.&nbsp; New node=
s see a<br>
&gt; regular Simplicity redemption.&nbsp; (I haven't worked out the details o=
f how the<br>
&gt; P2P protocol will negotiate with old nodes, but I don't forsee any<br>
&gt; problems.)<br>
&gt;<br>
&gt; Note that this implies that you should never participate in any Simplic=
ity<br>
&gt; contract where you don't get access to the entire source code of all<br=
>
&gt; branches to check that it doesn't have an unknown jet.<br>
&gt;<br>
&gt; On Mon, Oct 30, 2017 at 5:42 PM, Matt Corallo &lt;<a href=3D"mailto:lf-=
lists@mattcorallo.com">lf-lists@mattcorallo.com</a>&gt;<br>
&gt; wrote:<br>
&gt;&gt;<br>
&gt;&gt; I admittedly haven't had a chance to read the paper in full details=
, but I<br>
&gt;&gt; was curious how you propose dealing with "jets" in something like B=
itcoin.<br>
&gt;&gt; AFAIU, other similar systems are left doing hard-forks to reduce th=
e<br>
&gt;&gt; sigops/weight/fee-cost of transactions every time they want to add u=
seful<br>
&gt;&gt; optimized drop-ins. For obvious reasons, this seems rather impracti=
cal and a<br>
&gt;&gt; potentially critical barrier to adoption of such optimized drop-ins=
, which I<br>
&gt;&gt; imagine would be required to do any new cryptographic algorithms du=
e to the<br>
&gt;&gt; significant fee cost of interpreting such things.<br>
&gt;&gt;<br>
&gt;&gt; Is there some insight I'm missing here?<br>
&gt;&gt;<br>
&gt;&gt; Matt<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; On October 30, 2017 11:22:20 AM EDT, Russell O'Connor via bitcoin-d=
ev<br>
&gt;&gt; &lt;<a href=3D"mailto:bitcoin-dev@lists.linuxfoundation.org">bitcoi=
n-dev@lists.<wbr>linuxfoundation.org</a>&gt; wrote:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; I've been working on the design and implementation of an altern=
ative to<br>
&gt;&gt;&gt; Bitcoin Script, which I call Simplicity.&nbsp; Today, I am pres=
enting my design<br>
&gt;&gt;&gt; at the PLAS 2017 Workshop on Programming Languages and Analysis=
 for<br>
&gt;&gt;&gt; Security.&nbsp; You find a copy of my Simplicity paper at<br>
&gt;&gt;&gt; <a href=3D"https://blockstream.com/simplicity.pdf" rel=3D"noref=
errer" target=3D"_blank">https://blockstream.com/<wbr>simplicity.pdf</a><br>=

&gt;&gt;&gt;<br>
&gt;&gt;&gt; Simplicity is a low-level, typed, functional, native MAST langu=
age where<br>
&gt;&gt;&gt; programs are built from basic combinators.&nbsp; Like Bitcoin S=
cript, Simplicity<br>
&gt;&gt;&gt; is designed to operate at the consensus layer.&nbsp; While one c=
an write<br>
&gt;&gt;&gt; Simplicity by hand, it is expected to be the target of one, or m=
ultiple,<br>
&gt;&gt;&gt; front-end languages.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Simplicity comes with formal denotational semantics (i.e. seman=
tics of<br>
&gt;&gt;&gt; what programs compute) and formal operational semantics (i.e. s=
emantics of<br>
&gt;&gt;&gt; how programs compute). These are both formalized in the Coq pro=
of assistant<br>
&gt;&gt;&gt; and proven equivalent.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Formal denotational semantics are of limited value unless one c=
an use<br>
&gt;&gt;&gt; them in practice to reason about programs. I've used Simplicity=
's formal<br>
&gt;&gt;&gt; semantics to prove correct an implementation of the SHA-256 com=
pression<br>
&gt;&gt;&gt; function written in Simplicity.&nbsp; I have also implemented a=
 variant of ECDSA<br>
&gt;&gt;&gt; signature verification in Simplicity, and plan to formally vali=
date its<br>
&gt;&gt;&gt; correctness along with the associated elliptic curve operations=
.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Simplicity comes with easy to compute static analyses that can c=
ompute<br>
&gt;&gt;&gt; bounds on the space and time resources needed for evaluation.&n=
bsp; This is<br>
&gt;&gt;&gt; important for both node operators, so that the costs are knows b=
efore<br>
&gt;&gt;&gt; evaluation, and for designing Simplicity programs, so that smar=
t-contract<br>
&gt;&gt;&gt; participants can know the costs of their contract before commit=
ting to it.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; As a native MAST language, unused branches of Simplicity progra=
ms are<br>
&gt;&gt;&gt; pruned at redemption time.&nbsp; This enhances privacy, reduces=
 the block weight<br>
&gt;&gt;&gt; used, and can reduce space and time resource costs needed for e=
valuation.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; To make Simplicity practical, jets replace common Simplicity ex=
pressions<br>
&gt;&gt;&gt; (identified by their MAST root) and directly implement them wit=
h C code.&nbsp; I<br>
&gt;&gt;&gt; anticipate developing a broad set of useful jets covering arith=
metic<br>
&gt;&gt;&gt; operations, elliptic curve operations, and cryptographic operat=
ions<br>
&gt;&gt;&gt; including hashing and digital signature validation.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; The paper I am presenting at PLAS describes only the foundation=
 of the<br>
&gt;&gt;&gt; Simplicity language.&nbsp; The final design includes extensions=
 not covered in<br>
&gt;&gt;&gt; the paper, including<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; - full convent support, allowing access to all transaction data=
.<br>
&gt;&gt;&gt; - support for signature aggregation.<br>
&gt;&gt;&gt; - support for delegation.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Simplicity is still in a research and development phase.&nbsp; I=
'm working to<br>
&gt;&gt;&gt; produce a bare-bones SDK that will include<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; - the formal semantics and correctness proofs in Coq<br>
&gt;&gt;&gt; - a Haskell implementation for constructing Simplicity programs=
<br>
&gt;&gt;&gt; - and a C interpreter for Simplicity.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; After an SDK is complete the next step will be making Simplicit=
y<br>
&gt;&gt;&gt; available in the Elements project so that anyone can start expe=
rimenting<br>
&gt;&gt;&gt; with Simplicity in sidechains. Only after extensive vetting wou=
ld it be<br>
&gt;&gt;&gt; suitable to consider Simplicity for inclusion in Bitcoin.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Simplicity has a long ways to go still, and this work is not in=
tended to<br>
&gt;&gt;&gt; delay consideration of the various Merkelized Script proposals t=
hat are<br>
&gt;&gt;&gt; currently ongoing.<br>
&gt;<br>
&gt;<br>
&gt;<br>
</div><div class=3D"elided-text">&gt; ______________________________<wbr>___=
______________<br>
&gt; bitcoin-dev mailing list<br>
&gt; <a href=3D"mailto:bitcoin-dev@lists.linuxfoundation.org">bitcoin-dev@li=
sts.<wbr>linuxfoundation.org</a><br>
&gt; <a href=3D"https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-d=
ev" rel=3D"noreferrer" target=3D"_blank">https://lists.linuxfoundation.<wbr>=
org/mailman/listinfo/bitcoin-<wbr>dev</a><br>
&gt;<br>
</div></blockquote></div><br></div></div></div>
</div></blockquote></body></html>=

--Apple-Mail-153FE09F-10A7-4DDA-8DA3-C203951615D5--