Matt Corallo [ARCHIVE] on Nostr: 📅 Original date posted:2017-10-30 📝 Original message:Are you anticipating it ...
📅 Original date posted:2017-10-30
📝 Original message: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 at lists.linuxfoundation.org
>> <mailto:bitcoin-dev at 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 at lists.linuxfoundation.org
>> <mailto:bitcoin-dev at 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 at lists.linuxfoundation.org
>> <mailto:bitcoin-dev at lists.linuxfoundation.org>
>> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
>
📝 Original message: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 at lists.linuxfoundation.org
>> <mailto:bitcoin-dev at 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 at lists.linuxfoundation.org
>> <mailto:bitcoin-dev at 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 at lists.linuxfoundation.org
>> <mailto:bitcoin-dev at lists.linuxfoundation.org>
>> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
>