public inbox for bitcoindev@googlegroups.com
 help / color / mirror / Atom feed
From: Matt Corallo <lf-lists@mattcorallo•com>
To: Russell O'Connor <roconnor@blockstream•io>,
	Bitcoin Protocol Discussion
	<bitcoin-dev@lists•linuxfoundation.org>,
	Russell O'Connor via bitcoin-dev
	<bitcoin-dev@lists•linuxfoundation.org>
Subject: Re: [bitcoin-dev] Simplicity: An alternative to Script
Date: Mon, 30 Oct 2017 21:42:44 +0000	[thread overview]
Message-ID: <E63C347E-5321-4F7F-B69C-75747E88AC06@mattcorallo.com> (raw)
In-Reply-To: <CAMZUoK=VNRMda8oRCtxniE6-vLwG-b=je2Hx+sD9sCzS--v9kQ@mail.gmail.com>

[-- Attachment #1: Type: text/plain, Size: 4200 bytes --]

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> 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
>
>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.

[-- Attachment #2: Type: text/html, Size: 4927 bytes --]

  parent reply	other threads:[~2017-10-30 21:42 UTC|newest]

Thread overview: 12+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2017-10-30 15:22 Russell O'Connor
2017-10-30 15:31 ` Mark Friedenbach
2017-10-30 21:42 ` Matt Corallo [this message]
2017-10-30 21:56   ` Mark Friedenbach
2017-10-30 22:14     ` Matt Corallo
2017-10-30 22:32       ` Mark Friedenbach
2017-10-30 22:50         ` Matt Corallo
2017-10-30 23:29   ` Gregory Maxwell
2017-10-31 20:38   ` Russell O'Connor
2017-10-31 20:46     ` Mark Friedenbach
2017-10-31 21:01       ` Russell O'Connor
2017-11-01  1:46         ` Mark Friedenbach

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=E63C347E-5321-4F7F-B69C-75747E88AC06@mattcorallo.com \
    --to=lf-lists@mattcorallo$(echo .)com \
    --cc=bitcoin-dev@lists$(echo .)linuxfoundation.org \
    --cc=roconnor@blockstream$(echo .)io \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox