summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMark Friedenbach <mark@friedenbach.org>2017-10-31 18:46:54 -0700
committerbitcoindev <bitcoindev@gnusha.org>2017-11-01 01:46:59 +0000
commitcbc95834e685c771479dc89e6617467a91769940 (patch)
treeb701e2a1b272e37cba2e41e2406b98dd1763e5b2
parentf3b8af9212768fccd87c4e8f04a1760c414c4fde (diff)
downloadpi-bitcoindev-cbc95834e685c771479dc89e6617467a91769940.tar.gz
pi-bitcoindev-cbc95834e685c771479dc89e6617467a91769940.zip
Re: [bitcoin-dev] Simplicity: An alternative to Script
-rw-r--r--2c/5b3489f3a3b6d6116d4f59756b802296ed04d7505
1 files changed, 505 insertions, 0 deletions
diff --git a/2c/5b3489f3a3b6d6116d4f59756b802296ed04d7 b/2c/5b3489f3a3b6d6116d4f59756b802296ed04d7
new file mode 100644
index 000000000..bbf407660
--- /dev/null
+++ b/2c/5b3489f3a3b6d6116d4f59756b802296ed04d7
@@ -0,0 +1,505 @@
+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--
+