summaryrefslogtreecommitdiff
path: root/97/e68faa74a0673df0c786f8d4352bcc1eb7a3e9
blob: 86195e9e09338fb05b89124d1697b1b89d681eea (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
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--