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
|
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 B87E1BAF
for <bitcoin-dev@lists.linuxfoundation.org>;
Mon, 30 Oct 2017 15:22:43 +0000 (UTC)
X-Greylist: whitelisted by SQLgrey-1.7.6
Received: from mail-vk0-f44.google.com (mail-vk0-f44.google.com
[209.85.213.44])
by smtp1.linuxfoundation.org (Postfix) with ESMTPS id 94FB5561
for <bitcoin-dev@lists.linuxfoundation.org>;
Mon, 30 Oct 2017 15:22:42 +0000 (UTC)
Received: by mail-vk0-f44.google.com with SMTP id d12so8333764vkf.1
for <bitcoin-dev@lists.linuxfoundation.org>;
Mon, 30 Oct 2017 08:22:42 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=blockstream-io.20150623.gappssmtp.com; s=20150623;
h=mime-version:from:date:message-id:subject:to;
bh=569p/y7U6gk5EQjjPhEvViEF8IhdPb6ubzpixW3WGt0=;
b=HPhEg1/dKz1TFU/ZzICj8BGVetc6I3fTkxwB/3ZOBPNT3tZ8w72MEhWQRY/ra+LUaD
rcle53d7+/l5D2L9aQTSuIjVreLWWY0pkGsy+C2B+OdQ7mIstXh8RLGyBlX1O1QlsnZO
H1cB/mf6n+ffnfWAasqUOMKu8V/9tTFhn/0uPGKllY4y00gpcmfdSN4CiSwfAN6LIGp9
oy3hhKb3LpkbvXEsqLlkIHkrPHkulVz9CnapIK6OAQYlOW3B7PNEPEIw7Rt7aBafFJUG
WlxSYSczZtWD9Q4f40qq08WQ0XqNNRMnnSXKrBqmJ+iILjCON/DY/CMHeyNwnYM4cbLS
PZGw==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20161025;
h=x-gm-message-state:mime-version:from:date:message-id:subject:to;
bh=569p/y7U6gk5EQjjPhEvViEF8IhdPb6ubzpixW3WGt0=;
b=pxywB8aVFx1pKAiL5U3zthaC+rKgDLH9YlUWBEPfUC7T8ikuEqoia0tBtKfGnc621m
NixoKOPbjaFcpw4nVm90u6Weu+kydimPArOROgSVBD3z1ks4mWKybc29oML6qjd/9AT9
Vc4Rn2DkjeJmp9e9WeKTxjzZOFqnr0Qw+l6feHMM7hHSi4aekQDHVbqaC4bNr7Hcgj3V
CZ0lVmpbVhJv8YEuGaqqqvjLkBP/SiRcQstuwX7ws8Kum3bNZRPeLCYYWCp2GLmYv2U2
UlIEDSwuVMNtMUIlxEyeyqwteUuERI8FauRq3FucD0jrkCsEvl7aOejTab+In5exZNrQ
Nxgw==
X-Gm-Message-State: AMCzsaUJGGEDyYH+TZKuuDm3JLIr5MXmCas2v67ubgXOktqWfRkfT974
QzYjMdNLRKhFkCGYi+00fDtkEJ/z13F+9TA/UwDwIUF47qQ=
X-Google-Smtp-Source: ABhQp+QdrGY0C/GgOJiVG7XedPzvk0cWtrD+x7idOn1zdYyy4uurhQ5IHREObfbWr3SFfomLHxeErecwO4n5L6XRcFE=
X-Received: by 10.31.26.3 with SMTP id a3mr7379504vka.43.1509376961426; Mon,
30 Oct 2017 08:22:41 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.176.73.202 with HTTP; Mon, 30 Oct 2017 08:22:20 -0700 (PDT)
From: "Russell O'Connor" <roconnor@blockstream.io>
Date: Mon, 30 Oct 2017 11:22:20 -0400
Message-ID: <CAMZUoK=VNRMda8oRCtxniE6-vLwG-b=je2Hx+sD9sCzS--v9kQ@mail.gmail.com>
To: Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
Content-Type: multipart/alternative; boundary="001a11425b169e5b5c055cc535f0"
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
Subject: [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:22:43 -0000
--001a11425b169e5b5c055cc535f0
Content-Type: text/plain; charset="UTF-8"
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.
--001a11425b169e5b5c055cc535f0
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
<div dir=3D"ltr"><div>I'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/<wbr>si=
mplicity.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've used Simplicity'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'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>
--001a11425b169e5b5c055cc535f0--
|
