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 > _______________________________________________ bitcoin-dev mailing list bitcoin-dev@lists.linuxfoundation.org https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
