Re: [bitcoin-dev] Simplicity: An alternative to Script

[Matt Corallo <lf-lists@mattcorallo.com>]

OK, fair enough, just wanted to make sure we were on the same page.
"Thorny issues there and there hasn't been a ton of effort put into what
Bitcoin integration and maintainability looks like" is a perfectly fair
response :)

Matt

On 10/30/17 18:32, Mark Friedenbach wrote:
> I was just making a factual observation/correction. This is Russell’s project and I don’t want to speak for him. Personally I don’t think the particulars of bitcoin integration design space have been thoroughly explored enough to predict the exact approach that will be used.
> 
> It is possible to support a standard library of jets that are general purpose 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 validation. Or string manipulation and serialization jets to implement covenants. So I don’t 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:
>>
>> 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".
>>
>> 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?).
>>
>> Matt
>>
>>> 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.
>>>
>>>> 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:
>>>>
>>>> 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.
>>>>
>>>> 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
>>>> <mailto: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>
>>>>
>>>>    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.
>>>>
>>>> _______________________________________________
>>>> bitcoin-dev mailing list
>>>> bitcoin-dev@lists.linuxfoundation.org
>>>> <mailto:bitcoin-dev@lists.linuxfoundation.org>
>>>> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
>>>