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
|
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 16B49C07
for <bitcoin-dev@lists.linuxfoundation.org>;
Mon, 30 Oct 2017 15:31:26 +0000 (UTC)
X-Greylist: whitelisted by SQLgrey-1.7.6
Received: from mail-pg0-f53.google.com (mail-pg0-f53.google.com [74.125.83.53])
by smtp1.linuxfoundation.org (Postfix) with ESMTPS id 000B616A
for <bitcoin-dev@lists.linuxfoundation.org>;
Mon, 30 Oct 2017 15:31:24 +0000 (UTC)
Received: by mail-pg0-f53.google.com with SMTP id a192so11902159pge.9
for <bitcoin-dev@lists.linuxfoundation.org>;
Mon, 30 Oct 2017 08:31:24 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=friedenbach-org.20150623.gappssmtp.com; s=20150623;
h=from:content-transfer-encoding:mime-version:date:subject:message-id
:references:in-reply-to:to;
bh=CXnHB1J4MnYaPoEG45b/BI2cI6UuqKpeWHYvhaiaIac=;
b=nvxVkPfMhooo2Yk+mV29kz4UhqZnO2oFhNmDlijxNH4/SbPiPBhrL/a3Q9xBIIPzXJ
fiD/i38VExdPGzlqDhTJMYp18fV2Op8LEYqEqOuX3898qttWaYR9KYhLx1l+YhvvmKGH
DwNvZ0qvm8wyIkp1bqYjIoHJbjn1WZkAB1GJauIF85+RsgrqTxOryAhWHmwJOHV88BGQ
x6Ul+dtwX2+Ub6r7EWTvcZYLAQog+DMM4pq7aaWBf8603P5zsyK6CoesAcwPwHNQeJ9K
mR2CDxGp03XEWNkanzOGgOOiUCi84DFJuVKJChtGjXt1yJuiM3Fpnljr93d+0o9qgUAg
tT3g==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20161025;
h=x-gm-message-state:from:content-transfer-encoding:mime-version:date
:subject:message-id:references:in-reply-to:to;
bh=CXnHB1J4MnYaPoEG45b/BI2cI6UuqKpeWHYvhaiaIac=;
b=oNzBHvazI4+2csNz/8zKAQR2mqgMsVrUUE8rZpsElERtkfLWdqdDQ56LV5a7MCDKTK
8MKyWOm7JDebRYlFdc4H16vgF2lj97vGyZTyckbbNMviwf5RVtPAcF4kVMnZKCh85BRd
JMxKYrTzqIFDoxBqzASIyRgXaBZp8oVDTdqGi9EWN/n3a0poHyeYzkCDtzMFzY/QMF8K
agAeSAE7ARUYE5QcJVrFcyVN1OX/Tx6k49LOFnPEJoqcbAaMU8Ie6pkWt4hwiqHX5Rpb
XyYJ51akcNL5WkQsu48ygjU7iIG2cA5eA1ikur03EY68owDeIHgiv/plmcpf++yJgjlq
VXsw==
X-Gm-Message-State: AMCzsaUZDKxN7DX0XH/pU1+dLFNZr4S2FitRNu/M96MMeIORcO7BfKS6
yT6816Djihlh5TxnpftwOjPWmZhZTdg=
X-Google-Smtp-Source: ABhQp+QnZ2a9tG39scwJA/7+0/PVYMC95FSGPfX+k3tZgtNE47/8Hbxe63yirrD0eonBZ90+AUSD1Q==
X-Received: by 10.98.89.208 with SMTP id k77mr9356288pfj.164.1509377484407;
Mon, 30 Oct 2017 08:31:24 -0700 (PDT)
Received: from ?IPv6:2607:fb90:a45b:cc2c:3426:1dfc:f5e3:2061?
([2607:fb90:a45b:cc2c:3426:1dfc:f5e3:2061])
by smtp.gmail.com with ESMTPSA id
e24sm33037389pfl.43.2017.10.30.08.31.23
(version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
Mon, 30 Oct 2017 08:31:23 -0700 (PDT)
From: Mark Friedenbach <mark@friedenbach.org>
Content-Type: multipart/alternative;
boundary=Apple-Mail-12649DF9-94A7-4B6A-B657-BB5B3F8D6FF0
Content-Transfer-Encoding: 7bit
Mime-Version: 1.0 (1.0)
Date: Mon, 30 Oct 2017 08:31:22 -0700
Message-Id: <E5CEEE3C-C557-43FC-82C8-9E203EAB0266@friedenbach.org>
References: <CAMZUoK=VNRMda8oRCtxniE6-vLwG-b=je2Hx+sD9sCzS--v9kQ@mail.gmail.com>
In-Reply-To: <CAMZUoK=VNRMda8oRCtxniE6-vLwG-b=je2Hx+sD9sCzS--v9kQ@mail.gmail.com>
To: Russell O'Connor <roconnor@blockstream.io>,
Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
X-Mailer: iPhone Mail (15A432)
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
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 15:31:26 -0000
--Apple-Mail-12649DF9-94A7-4B6A-B657-BB5B3F8D6FF0
Content-Type: text/plain;
charset=us-ascii
Content-Transfer-Encoding: quoted-printable
So enthused that this is public now! Great work.=20
Sent from my iPhone
> On Oct 30, 2017, at 8:22 AM, Russell O'Connor via bitcoin-dev <bitcoin-dev=
@lists.linuxfoundation.org> wrote:
>=20
> I've been working on the design and implementation of an alternative to Bi=
tcoin Script, which I call Simplicity. Today, I am presenting my design at t=
he PLAS 2017 Workshop on Programming Languages and Analysis for Security. Y=
ou find a copy of my Simplicity paper at https://blockstream.com/simplicity.=
pdf
>=20
> Simplicity is a low-level, typed, functional, native MAST language where p=
rograms are built from basic combinators. Like Bitcoin Script, Simplicity i=
s designed to operate at the consensus layer. While one can write Simplicit=
y by hand, it is expected to be the target of one, or multiple, front-end la=
nguages.
>=20
> Simplicity comes with formal denotational semantics (i.e. semantics of wha=
t programs compute) and formal operational semantics (i.e. semantics of how p=
rograms compute). These are both formalized in the Coq proof assistant and p=
roven 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 semanti=
cs to prove correct an implementation of the SHA-256 compression function wr=
itten in Simplicity. I have also implemented a variant of ECDSA signature v=
erification in Simplicity, and plan to formally validate its correctness alo=
ng with the associated elliptic curve operations.
>=20
> Simplicity comes with easy to compute static analyses that can compute bou=
nds on the space and time resources needed for evaluation. This is importa=
nt for both node operators, so that the costs are knows before evaluation, a=
nd for designing Simplicity programs, so that smart-contract participants c=
an know the costs of their contract before committing to it.
>=20
> As a native MAST language, unused branches of Simplicity programs are prun=
ed 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 a=
nticipate developing a broad set of useful jets covering arithmetic operatio=
ns, elliptic curve operations, and cryptographic operations including hashin=
g and digital signature validation.
>=20
> The paper I am presenting at PLAS describes only the foundation of the Sim=
plicity language. The final design includes extensions not covered in the p=
aper, 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 p=
roduce 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 so that anyone can start experimenting with Simplic=
ity in sidechains. Only after extensive vetting would it be suitable to cons=
ider Simplicity for inclusion in Bitcoin.
>=20
> Simplicity has a long ways to go still, and this work is not intended to d=
elay consideration of the various Merkelized Script proposals that are curre=
ntly ongoing.
> _______________________________________________
> bitcoin-dev mailing list
> bitcoin-dev@lists.linuxfoundation.org
> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
--Apple-Mail-12649DF9-94A7-4B6A-B657-BB5B3F8D6FF0
Content-Type: text/html;
charset=utf-8
Content-Transfer-Encoding: 7bit
<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body dir="auto">So enthused that this is public now! Great work. <br><br><div id="AppleMailSignature">Sent from my iPhone</div><div><br>On Oct 30, 2017, at 8:22 AM, Russell O'Connor via bitcoin-dev <<a href="mailto:bitcoin-dev@lists.linuxfoundation.org">bitcoin-dev@lists.linuxfoundation.org</a>> wrote:<br><br></div><blockquote type="cite"><div><div dir="ltr"><div>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 <a href="http://plas2017.cse.buffalo.edu/" target="_blank">PLAS 2017 Workshop</a> on Programming Languages and Analysis for Security. You find a copy of my Simplicity paper at <a href="https://blockstream.com/simplicity.pdf" target="_blank">https://blockstream.com/<wbr>simplicity.pdf</a><br></div><div><br></div>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.<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
compute). These are both formalized in the Coq proof assistant and
proven equivalent.<br><br></div>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.<br><div><br>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.</div><div><br></div><div>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.</div><div><br></div><div>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.<br></div><div><br></div><div>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</div><div><br></div><div>- full convent support, allowing access to all transaction data.</div><div>- support for signature aggregation.</div><div>- support for delegation.</div><div><br></div><div>Simplicity is still in a research and development phase. I'm working to produce a bare-bones SDK that will include <br></div><div><br></div><div>- the formal semantics and correctness proofs in Coq</div><div>- a Haskell implementation for constructing Simplicity programs</div><div>- and a C interpreter for Simplicity.<br></div><div><br></div><div>After an SDK is complete the next step will be making Simplicity available in the <a href="https://elementsproject.org/" target="_blank">Elements project</a>
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.</div><div><br></div>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.</div>
</div></blockquote><blockquote type="cite"><div><span>_______________________________________________</span><br><span>bitcoin-dev mailing list</span><br><span><a href="mailto:bitcoin-dev@lists.linuxfoundation.org">bitcoin-dev@lists.linuxfoundation.org</a></span><br><span><a href="https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev">https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev</a></span><br></div></blockquote></body></html>
--Apple-Mail-12649DF9-94A7-4B6A-B657-BB5B3F8D6FF0--
|
