Content-Type: text/plain;
	charset=gb2312
Mime-Version: 1.0 (1.0)
From: Mark Friedenbach <mark@friedenbach.org>
In-Reply-To: <1689d7c6-7c32-aa78-6626-c344f19923de@mattcorallo.com>
Date: Mon, 30 Oct 2017 15:32:42 -0700
Content-Transfer-Encoding: quoted-printable
Message-Id: <6E10759E-DCEC-4C13-AD23-7DEE1BC20311@friedenbach.org>
References: <CAMZUoK=VNRMda8oRCtxniE6-vLwG-b=je2Hx+sD9sCzS--v9kQ@mail.gmail.com>
	<E63C347E-5321-4F7F-B69C-75747E88AC06@mattcorallo.com>
	<64173F46-551E-4C36-A43A-5FBDBFF761CD@friedenbach.org>
	<1689d7c6-7c32-aa78-6626-c344f19923de@mattcorallo.com>
To: Matt Corallo <lf-lists@mattcorallo.com>
Cc: Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
Subject: Re: [bitcoin-dev] Simplicity: An alternative to Script
Precedence: list

I was just making a factual observation/correction. This is Russell=A1=AFs p=
roject and I don=A1=AFt want to speak for him. Personally I don=A1=AFt think=
 the particulars of bitcoin integration design space have been thoroughly ex=
plored enough to predict the exact approach that will be used.

It is possible to support a standard library of jets that are general purpos=
e enough to allow the validation of new crypto primitives, like reusing sha2=
 to make Lamport signatures. Or use curve-agnostic jets to do Weil pairing v=
alidation. Or string manipulation and serialization jets to implement covena=
nts. So I don=A1=AFt think the situation is as dire as you make it sound.

> On Oct 30, 2017, at 3:14 PM, Matt Corallo <lf-lists@mattcorallo.com> wrote=
:
>=20
> Are you anticipating it will be reasonably possible to execute more
> complicated things in interpreted form even after "jets" are put in
> place? If not its just a soft-fork to add new script operations and
> going through the effort of making them compatible with existing code
> and using a full 32 byte hash to represent them seems wasteful - might
> as well just add a "SHA256 opcode".
>=20
> Either way it sounds like you're assuming a pretty aggressive soft-fork
> cadence? I'm not sure if that's so practical right now (or are you
> thinking it would be more practical if things were
> drop-in-formally-verified-equivalent-replacements?).
>=20
> Matt
>=20
>> On 10/30/17 17:56, Mark Friedenbach wrote:
>> 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.
>>=20
>>> On Oct 30, 2017, at 2:42 PM, Matt Corallo via bitcoin-dev
>>> <bitcoin-dev@lists.linuxfoundation.org
>>> <mailto: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
>>> <mailto:bitcoin-dev@lists.linuxfoundation.org>> wrote:
>>>=20
>>>    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.=20
>>>    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
>>>    - 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.
>>>=20
>>> _______________________________________________
>>> bitcoin-dev mailing list
>>> bitcoin-dev@lists.linuxfoundation.org
>>> <mailto:bitcoin-dev@lists.linuxfoundation.org>
>>> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
>>=20