đź“… Original date posted:2017-10-30
đź“ť Original message:OK, fair enough, just wanted to make sure we were on the same page.
"Thorny issues there and there hasn't been a ton of effort put into what
Bitcoin integration and maintainability looks like" is a perfectly fair
response :)
Matt
On 10/30/17 18:32, Mark Friedenbach wrote:
> 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
>>>
Matt Corallo [ARCHIVE] /
npub1e4…jxmcu
2023-06-07 18:07:18
in reply to nevent1q…g8tc
Author Public Key
npub1e46n428mcyfwznl7nlsf6d3s7rhlwm9x3cmkuqzt3emmdpadmkaqqjxmcuPublished at
2023-06-07 18:07:18Event JSON
{
"id": "b6fd99a1d51a2c1061d08cae6fc39160978748d11fef7f52d894430b8a6cb4db",
"pubkey": "cd753aa8fbc112e14ffe9fe09d3630f0eff76ca68e376e004b8e77b687adddba",
"created_at": 1686161238,
"kind": 1,
"tags": [
[
"e",
"d15fafc39a5d3749653ccc48eff7d462b7549fee81626c4c9fcaabb10820ea69",
"",
"root"
],
[
"e",
"a9c211c02fd2dc0cdbcd516f08c5ee7e8fd9c77bbbba64d4ab2387296d3d3e35",
"",
"reply"
],
[
"p",
"1c61d995949cbfaf14f767784e166bde865c7b8783d7aa3bf0a1d014b70c0069"
]
],
"content": "📅 Original date posted:2017-10-30\n📝 Original message:OK, fair enough, just wanted to make sure we were on the same page.\n\"Thorny issues there and there hasn't been a ton of effort put into what\nBitcoin integration and maintainability looks like\" is a perfectly fair\nresponse :)\n\nMatt\n\nOn 10/30/17 18:32, Mark Friedenbach wrote:\n\u003e 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.\n\u003e \n\u003e 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.\n\u003e \n\u003e\u003e On Oct 30, 2017, at 3:14 PM, Matt Corallo \u003clf-lists at mattcorallo.com\u003e wrote:\n\u003e\u003e\n\u003e\u003e Are you anticipating it will be reasonably possible to execute more\n\u003e\u003e complicated things in interpreted form even after \"jets\" are put in\n\u003e\u003e place? If not its just a soft-fork to add new script operations and\n\u003e\u003e going through the effort of making them compatible with existing code\n\u003e\u003e and using a full 32 byte hash to represent them seems wasteful - might\n\u003e\u003e as well just add a \"SHA256 opcode\".\n\u003e\u003e\n\u003e\u003e Either way it sounds like you're assuming a pretty aggressive soft-fork\n\u003e\u003e cadence? I'm not sure if that's so practical right now (or are you\n\u003e\u003e thinking it would be more practical if things were\n\u003e\u003e drop-in-formally-verified-equivalent-replacements?).\n\u003e\u003e\n\u003e\u003e Matt\n\u003e\u003e\n\u003e\u003e\u003e On 10/30/17 17:56, Mark Friedenbach wrote:\n\u003e\u003e\u003e Script versions makes this no longer a hard-fork to do. The script\n\u003e\u003e\u003e version would implicitly encode which jets are optimized, and what their\n\u003e\u003e\u003e optimized cost is.\n\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e On Oct 30, 2017, at 2:42 PM, Matt Corallo via bitcoin-dev\n\u003e\u003e\u003e\u003e \u003cbitcoin-dev at lists.linuxfoundation.org\n\u003e\u003e\u003e\u003e \u003cmailto:bitcoin-dev at lists.linuxfoundation.org\u003e\u003e wrote:\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e I admittedly haven't had a chance to read the paper in full details,\n\u003e\u003e\u003e\u003e but I was curious how you propose dealing with \"jets\" in something\n\u003e\u003e\u003e\u003e like Bitcoin. AFAIU, other similar systems are left doing hard-forks\n\u003e\u003e\u003e\u003e to reduce the sigops/weight/fee-cost of transactions every time they\n\u003e\u003e\u003e\u003e want to add useful optimized drop-ins. For obvious reasons, this seems\n\u003e\u003e\u003e\u003e rather impractical and a potentially critical barrier to adoption of\n\u003e\u003e\u003e\u003e such optimized drop-ins, which I imagine would be required to do any\n\u003e\u003e\u003e\u003e new cryptographic algorithms due to the significant fee cost of\n\u003e\u003e\u003e\u003e interpreting such things.\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e Is there some insight I'm missing here?\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e Matt\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e On October 30, 2017 11:22:20 AM EDT, Russell O'Connor via bitcoin-dev\n\u003e\u003e\u003e\u003e \u003cbitcoin-dev at lists.linuxfoundation.org\n\u003e\u003e\u003e\u003e \u003cmailto:bitcoin-dev at lists.linuxfoundation.org\u003e\u003e wrote:\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e I've been working on the design and implementation of an\n\u003e\u003e\u003e\u003e alternative to Bitcoin Script, which I call Simplicity. Today, I\n\u003e\u003e\u003e\u003e am presenting my design at the PLAS 2017 Workshop\n\u003e\u003e\u003e\u003e \u003chttp://plas2017.cse.buffalo.edu/\u003e on Programming Languages and\n\u003e\u003e\u003e\u003e Analysis for Security. You find a copy of my Simplicity paper at\n\u003e\u003e\u003e\u003e https://blockstream.com/simplicity.pdf\n\u003e\u003e\u003e\u003e \u003chttps://blockstream.com/simplicity.pdf\u003e\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e Simplicity is a low-level, typed, functional, native MAST language\n\u003e\u003e\u003e\u003e where programs are built from basic combinators. Like Bitcoin\n\u003e\u003e\u003e\u003e Script, Simplicity is designed to operate at the consensus layer. \n\u003e\u003e\u003e\u003e While one can write Simplicity by hand, it is expected to be the\n\u003e\u003e\u003e\u003e target of one, or multiple, front-end languages.\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e Simplicity comes with formal denotational semantics (i.e.\n\u003e\u003e\u003e\u003e semantics of what programs compute) and formal operational\n\u003e\u003e\u003e\u003e semantics (i.e. semantics of how programs compute). These are both\n\u003e\u003e\u003e\u003e formalized in the Coq proof assistant and proven equivalent.\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e Formal denotational semantics are of limited value unless one can\n\u003e\u003e\u003e\u003e use them in practice to reason about programs. I've used\n\u003e\u003e\u003e\u003e Simplicity's formal semantics to prove correct an implementation\n\u003e\u003e\u003e\u003e of the SHA-256 compression function written in Simplicity. I have\n\u003e\u003e\u003e\u003e also implemented a variant of ECDSA signature verification in\n\u003e\u003e\u003e\u003e Simplicity, and plan to formally validate its correctness along\n\u003e\u003e\u003e\u003e with the associated elliptic curve operations.\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e Simplicity comes with easy to compute static analyses that can\n\u003e\u003e\u003e\u003e compute bounds on the space and time resources needed for\n\u003e\u003e\u003e\u003e evaluation. This is important for both node operators, so that\n\u003e\u003e\u003e\u003e the costs are knows before evaluation, and for designing\n\u003e\u003e\u003e\u003e Simplicity programs, so that smart-contract participants can know\n\u003e\u003e\u003e\u003e the costs of their contract before committing to it.\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e As a native MAST language, unused branches of Simplicity programs\n\u003e\u003e\u003e\u003e are pruned at redemption time. This enhances privacy, reduces the\n\u003e\u003e\u003e\u003e block weight used, and can reduce space and time resource costs\n\u003e\u003e\u003e\u003e needed for evaluation.\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e To make Simplicity practical, jets replace common Simplicity\n\u003e\u003e\u003e\u003e expressions (identified by their MAST root) and directly implement\n\u003e\u003e\u003e\u003e them with C code. I anticipate developing a broad set of useful\n\u003e\u003e\u003e\u003e jets covering arithmetic operations, elliptic curve operations,\n\u003e\u003e\u003e\u003e and cryptographic operations including hashing and digital\n\u003e\u003e\u003e\u003e signature validation.\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e The paper I am presenting at PLAS describes only the foundation of\n\u003e\u003e\u003e\u003e the Simplicity language. The final design includes extensions not\n\u003e\u003e\u003e\u003e covered in the paper, including\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e - full convent support, allowing access to all transaction data.\n\u003e\u003e\u003e\u003e - support for signature aggregation.\n\u003e\u003e\u003e\u003e - support for delegation.\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e Simplicity is still in a research and development phase. I'm\n\u003e\u003e\u003e\u003e working to produce a bare-bones SDK that will include\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e - the formal semantics and correctness proofs in Coq\n\u003e\u003e\u003e\u003e - a Haskell implementation for constructing Simplicity programs\n\u003e\u003e\u003e\u003e - and a C interpreter for Simplicity.\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e After an SDK is complete the next step will be making Simplicity\n\u003e\u003e\u003e\u003e available in the Elements project \u003chttps://elementsproject.org/\u003e\n\u003e\u003e\u003e\u003e so that anyone can start experimenting with Simplicity in\n\u003e\u003e\u003e\u003e sidechains. Only after extensive vetting would it be suitable to\n\u003e\u003e\u003e\u003e consider Simplicity for inclusion in Bitcoin.\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e Simplicity has a long ways to go still, and this work is not\n\u003e\u003e\u003e\u003e intended to delay consideration of the various Merkelized Script\n\u003e\u003e\u003e\u003e proposals that are currently ongoing.\n\u003e\u003e\u003e\u003e\n\u003e\u003e\u003e\u003e _______________________________________________\n\u003e\u003e\u003e\u003e bitcoin-dev mailing list\n\u003e\u003e\u003e\u003e bitcoin-dev at lists.linuxfoundation.org\n\u003e\u003e\u003e\u003e \u003cmailto:bitcoin-dev at lists.linuxfoundation.org\u003e\n\u003e\u003e\u003e\u003e https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev\n\u003e\u003e\u003e",
"sig": "ac7ebba63728257a1b35315556ac3fe04acd10a566f4f8b42e7e7e62bcb6e91982519f0d618a7c41d2a43c16a41d06fe83fab54102f27c488959e44d98f406f7"
}