From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from smtp1.linuxfoundation.org (smtp1.linux-foundation.org [172.17.192.35]) by mail.linuxfoundation.org (Postfix) with ESMTPS id E2B1AC18 for ; Mon, 30 Oct 2017 22:32:48 +0000 (UTC) X-Greylist: whitelisted by SQLgrey-1.7.6 Received: from mail-pg0-f43.google.com (mail-pg0-f43.google.com [74.125.83.43]) by smtp1.linuxfoundation.org (Postfix) with ESMTPS id 3F4784CD for ; Mon, 30 Oct 2017 22:32:48 +0000 (UTC) Received: by mail-pg0-f43.google.com with SMTP id g6so12895252pgn.6 for ; Mon, 30 Oct 2017 15:32:48 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=friedenbach-org.20150623.gappssmtp.com; s=20150623; h=mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=cogsPm86Fe/tFu3hataPdhbvUsWYn2YFK5XXQ3FSinE=; b=wA3+MN6WVYxOo16za8bxenrsio7XNfohd82ZQ07UBIHsyShl7jvBKAkPSzN/C2Km4g aF6RoJ95l6/FJuTHbkW2IxdCRTMdD7a+5861nURab5lKecWeyD1ww1vrCR0M0dixguSb TDIpO1ySEFje2xFecTg0tYITgV7CgkIB1QVWhNUzb4yDCpKA9TgSVWOtoiieiCvrQ62b n2uBhTGUZcg01zwG85EsmyWBgjeYLN58IrgtJsSAstsFEOWQrQSK1JKFVBbk7bWTCPUd 6kwcFdT5sUfCSBdNX5tdJ1QSR0G/UKFiYyRSRwZ7jefln2rdTZinfxi4K13yTasE+Smy g15Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=cogsPm86Fe/tFu3hataPdhbvUsWYn2YFK5XXQ3FSinE=; b=Qat08nm0AiVY1nItgrOUkSCyVG9TgVtZl6aJ1F1yPRfiWeydDFU+IB4LTgDe6nVKB1 egRcK1wwBF6kKWAxdFQrgvwB+FgDNVkqG4zPcv9QMhiFwlJba7agoP4jUgER4BnXp6jH 3Twudik7+E1ESw6FCCl2NCSC3Si8pxlDV2r6Il3SmkbL1ptRrI9f/NARhgNJXiMquPZj uKtNc56ijjufvCi4zZxNY61IqYzJfKW4m+aOyIou7e2XirEjbANCyAp2NTkRsIM+35WJ Y9aphIeboRDYbXl7MOQGe44hNoQqnnNJZiSHmGNAGlNZSohCE3+GbTE5a2gyNGjPbdAN j/Nw== X-Gm-Message-State: AMCzsaVYSAF/9+qTEq41boZ45YJxCdBAsAA6OoeygVLIC92jdct/6fvx yuYr0oLyTqnKodWj2VbpJyFm86E/dmc= X-Google-Smtp-Source: ABhQp+T1ZM3U40vWBHpCGIdvd3R7Q0TW6pCvo0tRI+bt9BY5sWTWyAYgWfKwfwCxGoEjRchFZBvY9Q== X-Received: by 10.99.165.25 with SMTP id n25mr9031890pgf.294.1509402767650; Mon, 30 Oct 2017 15:32:47 -0700 (PDT) Received: from ?IPv6:2607:fb90:a45b:cc2c:ddb4:9930:9e3d:3dfb? ([2607:fb90:a45b:cc2c:ddb4:9930:9e3d:3dfb]) by smtp.gmail.com with ESMTPSA id r9sm11102pfd.6.2017.10.30.15.32.44 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 30 Oct 2017 15:32:47 -0700 (PDT) Content-Type: text/plain; charset=gb2312 Mime-Version: 1.0 (1.0) From: Mark Friedenbach X-Mailer: iPhone Mail (15A432) 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: <64173F46-551E-4C36-A43A-5FBDBFF761CD@friedenbach.org> <1689d7c6-7c32-aa78-6626-c344f19923de@mattcorallo.com> To: Matt Corallo X-Spam-Status: No, score=0.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, 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 Cc: Bitcoin Protocol Discussion 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 List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 30 Oct 2017 22:32:49 -0000 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 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 >>> >> > 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 >>> >> > 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 >>> on Programming Languages and >>> Analysis for Security. You 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 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 >>> 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 >>> >>> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev >>=20