Mark Friedenbach [ARCHIVE] on Nostr: đź“… Original date posted:2017-10-30 đź“ť Original message:I was just making a ...
đź“… Original date posted:2017-10-30
📝 Original message: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 at 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 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: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 at 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 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
>>