* [bitcoin-dev] Simplicity: An alternative to Script
@ 2017-10-30 15:22 Russell O'Connor
2017-10-30 15:31 ` Mark Friedenbach
2017-10-30 21:42 ` Matt Corallo
0 siblings, 2 replies; 12+ messages in thread
From: Russell O'Connor @ 2017-10-30 15:22 UTC (permalink / raw)
To: Bitcoin Protocol Discussion
[-- Attachment #1: Type: text/plain, Size: 3285 bytes --]
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
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.
[-- Attachment #2: Type: text/html, Size: 3858 bytes --]
^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [bitcoin-dev] Simplicity: An alternative to Script
2017-10-30 15:22 [bitcoin-dev] Simplicity: An alternative to Script Russell O'Connor
@ 2017-10-30 15:31 ` Mark Friedenbach
2017-10-30 21:42 ` Matt Corallo
1 sibling, 0 replies; 12+ messages in thread
From: Mark Friedenbach @ 2017-10-30 15:31 UTC (permalink / raw)
To: Russell O'Connor, Bitcoin Protocol Discussion
[-- Attachment #1: Type: text/plain, Size: 3687 bytes --]
So enthused that this is public now! Great work.
Sent from my iPhone
> On Oct 30, 2017, at 8:22 AM, Russell O'Connor via bitcoin-dev <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 on Programming Languages and Analysis for Security. You find a copy of my Simplicity paper at 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 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
> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
[-- Attachment #2: Type: text/html, Size: 4739 bytes --]
^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [bitcoin-dev] Simplicity: An alternative to Script
2017-10-30 15:22 [bitcoin-dev] Simplicity: An alternative to Script Russell O'Connor
2017-10-30 15:31 ` Mark Friedenbach
@ 2017-10-30 21:42 ` Matt Corallo
2017-10-30 21:56 ` Mark Friedenbach
` (2 more replies)
1 sibling, 3 replies; 12+ messages in thread
From: Matt Corallo @ 2017-10-30 21:42 UTC (permalink / raw)
To: Russell O'Connor, Bitcoin Protocol Discussion,
Russell O'Connor via bitcoin-dev
[-- Attachment #1: Type: text/plain, Size: 4200 bytes --]
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> 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
>
>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.
[-- Attachment #2: Type: text/html, Size: 4927 bytes --]
^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [bitcoin-dev] Simplicity: An alternative to Script
2017-10-30 21:42 ` Matt Corallo
@ 2017-10-30 21:56 ` Mark Friedenbach
2017-10-30 22:14 ` Matt Corallo
2017-10-30 23:29 ` Gregory Maxwell
2017-10-31 20:38 ` Russell O'Connor
2 siblings, 1 reply; 12+ messages in thread
From: Mark Friedenbach @ 2017-10-30 21:56 UTC (permalink / raw)
To: Matt Corallo, Bitcoin Protocol Discussion
[-- Attachment #1: Type: text/plain, Size: 4635 bytes --]
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> 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> 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
> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
[-- Attachment #2: Type: text/html, Size: 6406 bytes --]
^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [bitcoin-dev] Simplicity: An alternative to Script
2017-10-30 21:56 ` Mark Friedenbach
@ 2017-10-30 22:14 ` Matt Corallo
2017-10-30 22:32 ` Mark Friedenbach
0 siblings, 1 reply; 12+ messages in thread
From: Matt Corallo @ 2017-10-30 22:14 UTC (permalink / raw)
To: Mark Friedenbach, Bitcoin Protocol Discussion
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
>
^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [bitcoin-dev] Simplicity: An alternative to Script
2017-10-30 22:14 ` Matt Corallo
@ 2017-10-30 22:32 ` Mark Friedenbach
2017-10-30 22:50 ` Matt Corallo
0 siblings, 1 reply; 12+ messages in thread
From: Mark Friedenbach @ 2017-10-30 22:32 UTC (permalink / raw)
To: Matt Corallo; +Cc: Bitcoin Protocol Discussion
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@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@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
>>
^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [bitcoin-dev] Simplicity: An alternative to Script
2017-10-30 22:32 ` Mark Friedenbach
@ 2017-10-30 22:50 ` Matt Corallo
0 siblings, 0 replies; 12+ messages in thread
From: Matt Corallo @ 2017-10-30 22:50 UTC (permalink / raw)
To: Mark Friedenbach; +Cc: Bitcoin Protocol Discussion
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@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@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
>>>
^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [bitcoin-dev] Simplicity: An alternative to Script
2017-10-30 21:42 ` Matt Corallo
2017-10-30 21:56 ` Mark Friedenbach
@ 2017-10-30 23:29 ` Gregory Maxwell
2017-10-31 20:38 ` Russell O'Connor
2 siblings, 0 replies; 12+ messages in thread
From: Gregory Maxwell @ 2017-10-30 23:29 UTC (permalink / raw)
To: Matt Corallo, Bitcoin Protocol Discussion
On Mon, Oct 30, 2017 at 9:42 PM, Matt Corallo via bitcoin-dev
<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.
For some framing-- I think we're still a long way off from proposing
something like this in Bitcoin, and _how_ it's ultimately proposed is
an open question.
There are many ways to use simplicity, for an extreme example: one
could define a collection of high level operations and combinators at
the level of things in Bitcoin Script (op_sha256, op_equal, op_cat,
etc.) and make an interpreter that implements these operations as
discounted jets and ONLY these operations at all.
At that point you have a system which is functionally like Bitcoin
Script-- with the same performance characteristics-- but with a pretty
much perfectly rigorous formal specification and which is highly
amenable to the formal analysis of smart contracts written in it.
At the other extreme, you expose a full on Bitmachine and allow
arbitrary simplicity-- But this is probably slow enough to not be
very useful. Simplicity itself is so simple that it doesn't natively
have a concept of a _bit_, library code programs the concept of a bit,
then the concept of a half adder ... and so on. As a result a
completely unjetted implementation is slow (actually remarkably fast
considering that it's effectively interpreting a circuit constructed
from pure logic).
The most useful way of using it would probably be in-between: a good
collection of high level functions, and mid-level functions (e.g.
arithmetic and string operations) making a wide space of useful but
general software both possible and high performance. But to get there
we need enough experience with it to know what the requisite
collection of operations would be.
One challenge is that I don't think we have a clear mental model for
how nominal validation costs are allowed to be before there is a
negative impact. It's probably safe to assume 'pretty darn nominal'
is a requirement, but there is still a lot that can be done within
that envelope.
As far as consensus discounted jets goes:
From my perspective there are three related ideas around this:
Is a particular script-root jetted or not in an implementation?
-- In and of itself this is not of consensus consequence; esp.
because a major design feature of simplicity is that it should be
possible using to prove that an optimized C implementation of a
simplicity program is complete and correct (using VST+COQ).
Is a particular script-root 'standard and known' in the P2P network:
-- This means that you can skip communicating it when sending
witnesses to peers; but this is something that could be negotiated on
a peer by peer basis-- like compressing transactions, and isn't at all
consensus normative.
Is a particular jet discounted and what are the discounts:
-- This is inherently a consensus question; as the bitmachine costing
for a program is consensus normative (assuming that you allow
arbitrary simplicity code at all).
A script-versioning like mechanism can provide for a straight-forward
way to upgrade discounted cost tables in a compatible way-- if you're
running old software that doesn't have the required jets to justify a
particular discount collection -- well that's okay, you won't validate
those scripts at all. (so they'll be super fast for you!)
Another potential tool is the idea of sunsetting cost limits that
sunset; e.g. after N years, the limits go away with an assumption that
updated limits have been softforked in that ativate at that time and
themselves expire in N years. Old software would become slower
validating due to newly discounted code they lack jets for... but
would continue validating (at least until they run out of performance
headroom).
This is theoretically attractive in a number of regards, but
unfortunately I think our industry hasn't shown sufficient maturity
about engineering tradeoffs to make this a politically viable choice
in the mid-term-- I known I'm personally uncomfortable with the
outspokenness of parties that hold positions which I think can fairly
be summarized "We should remove all limits and if the system crashes
and burns as a result, we'll just make a new one! YOLO.". But it's
interesting to think about in the long term.
There are also hybrid approaches where you can imagine this decision
being made by node operators, e.g. continuing to validate code that
exceeds your effort limits on probabilistic and best effort basis;
even more attractive if there were a protocol for efficiently showing
others that an operation had an invalid witness. Though there is a lot
to explore about the brittleness to partitioning that comes from any
expectation that you'd learn about invalid updates by exception.
In any case, these are all options that exist completely independently
of simplicity. I think we should think of simplicity as a rigorous
base which we could _potentially_ use to build whatever future
direction of script we like out of... by itself it doesn't mandate a
particular depth or level of adoption.
And for the moment it's still also mostly just a base-- I don't
anticipate typical smart contracting end users programming directly w/
simplicity even if Bitcoin did support arbitrary simplicity-- I
expect they'd program in user friendly domain specific languages which
are formally tied to their implementations in simplicity that allow-
but do not force- closed loop formal reasoning about their contracts
all the way from their high level business rules straight through to
the machine code implementing the interpreter(s) that run in the
network.
But to get there we'll have to prove in practice that this is actually
workable. We have some evidence that it is, e.g. Roconnor's SHA2
implementation in simplicity is proven to implement the same function
that a C implementation implements (via the compcert formalization of
C). but there will need to be more.
^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [bitcoin-dev] Simplicity: An alternative to Script
2017-10-30 21:42 ` Matt Corallo
2017-10-30 21:56 ` Mark Friedenbach
2017-10-30 23:29 ` Gregory Maxwell
@ 2017-10-31 20:38 ` Russell O'Connor
2017-10-31 20:46 ` Mark Friedenbach
2 siblings, 1 reply; 12+ messages in thread
From: Russell O'Connor @ 2017-10-31 20:38 UTC (permalink / raw)
To: Matt Corallo; +Cc: Bitcoin Protocol Discussion
[-- Attachment #1: Type: text/plain, Size: 5560 bytes --]
(sorry, I forgot to reply-all earlier)
The very short answer to this question is that I plan on using Luke's
fail-success-on-unknown-operation in Simplicity. This is something that
isn't detailed at all in the paper.
The plan is that discounted jets will be explicitly labeled as jets in the
commitment. If you can provide a Merkle path from the root to a node that
is an explicit jet, but that jet isn't among the finite number of known
discounted jets, then the script is automatically successful (making it
anyone-can-spend). When new jets are wanted they can be soft-forked into
the protocol (for example if we get a suitable quantum-resistant digital
signature scheme) and the list of known discounted jets grows. Old nodes
get a merkle path to the new jet, which they view as an unknown jet, and
allow the transaction as a anyone-can-spend transaction. New nodes see a
regular Simplicity redemption. (I haven't worked out the details of how
the P2P protocol will negotiate with old nodes, but I don't forsee any
problems.)
Note that this implies that you should never participate in any Simplicity
contract where you don't get access to the entire source code of all
branches to check that it doesn't have an unknown jet.
On Mon, Oct 30, 2017 at 5:42 PM, Matt Corallo <lf-lists@mattcorallo•com>
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> 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
>>
>> 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.
>>
>
[-- Attachment #2: Type: text/html, Size: 6771 bytes --]
^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [bitcoin-dev] Simplicity: An alternative to Script
2017-10-31 20:38 ` Russell O'Connor
@ 2017-10-31 20:46 ` Mark Friedenbach
2017-10-31 21:01 ` Russell O'Connor
0 siblings, 1 reply; 12+ messages in thread
From: Mark Friedenbach @ 2017-10-31 20:46 UTC (permalink / raw)
To: Russell O'Connor, Bitcoin Protocol Discussion
Nit, but if you go down that specific path I would suggest making just
the jet itself fail-open. That way you are not so limited in requiring
validation of the full contract -- one party can verify simply that
whatever condition they care about holds on reaching that part of the
contract. E.g. maybe their signature is needed at the top level, and
then they don't care what further restrictions are placed.
On Tue, Oct 31, 2017 at 1:38 PM, Russell O'Connor via bitcoin-dev
<bitcoin-dev@lists•linuxfoundation.org> wrote:
> (sorry, I forgot to reply-all earlier)
>
> The very short answer to this question is that I plan on using Luke's
> fail-success-on-unknown-operation in Simplicity. This is something that
> isn't detailed at all in the paper.
>
> The plan is that discounted jets will be explicitly labeled as jets in the
> commitment. If you can provide a Merkle path from the root to a node that
> is an explicit jet, but that jet isn't among the finite number of known
> discounted jets, then the script is automatically successful (making it
> anyone-can-spend). When new jets are wanted they can be soft-forked into
> the protocol (for example if we get a suitable quantum-resistant digital
> signature scheme) and the list of known discounted jets grows. Old nodes
> get a merkle path to the new jet, which they view as an unknown jet, and
> allow the transaction as a anyone-can-spend transaction. New nodes see a
> regular Simplicity redemption. (I haven't worked out the details of how the
> P2P protocol will negotiate with old nodes, but I don't forsee any
> problems.)
>
> Note that this implies that you should never participate in any Simplicity
> contract where you don't get access to the entire source code of all
> branches to check that it doesn't have an unknown jet.
>
> On Mon, Oct 30, 2017 at 5:42 PM, Matt Corallo <lf-lists@mattcorallo•com>
> 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> 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 on Programming Languages and Analysis for
>>> Security. You find a copy of my Simplicity paper at
>>> 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 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
> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
>
^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [bitcoin-dev] Simplicity: An alternative to Script
2017-10-31 20:46 ` Mark Friedenbach
@ 2017-10-31 21:01 ` Russell O'Connor
2017-11-01 1:46 ` Mark Friedenbach
0 siblings, 1 reply; 12+ messages in thread
From: Russell O'Connor @ 2017-10-31 21:01 UTC (permalink / raw)
To: Mark Friedenbach; +Cc: Bitcoin Protocol Discussion
[-- Attachment #1: Type: text/plain, Size: 6989 bytes --]
That approach is worth considering. However there is a wrinkle that
Simplicity's denotational semantics doesn't imply an order of operations.
For example, if one half of a pair contains a assertion failure
(fail-closed), and the other half contains a unknown jet (fail-open), then
does the program succeed or fail?
This could be solved by providing an order of operations; however I fear
that will complicate formal reasoning about Simplicity expressions. Formal
reasoning is hard enough as is and I hesitate to complicate the semantics
in ways that make formal reasoning harder still.
On Oct 31, 2017 15:47, "Mark Friedenbach" <mark@friedenbach•org> wrote:
Nit, but if you go down that specific path I would suggest making just
the jet itself fail-open. That way you are not so limited in requiring
validation of the full contract -- one party can verify simply that
whatever condition they care about holds on reaching that part of the
contract. E.g. maybe their signature is needed at the top level, and
then they don't care what further restrictions are placed.
On Tue, Oct 31, 2017 at 1:38 PM, Russell O'Connor via bitcoin-dev
<bitcoin-dev@lists•linuxfoundation.org> wrote:
> (sorry, I forgot to reply-all earlier)
>
> The very short answer to this question is that I plan on using Luke's
> fail-success-on-unknown-operation in Simplicity. This is something that
> isn't detailed at all in the paper.
>
> The plan is that discounted jets will be explicitly labeled as jets in the
> commitment. If you can provide a Merkle path from the root to a node that
> is an explicit jet, but that jet isn't among the finite number of known
> discounted jets, then the script is automatically successful (making it
> anyone-can-spend). When new jets are wanted they can be soft-forked into
> the protocol (for example if we get a suitable quantum-resistant digital
> signature scheme) and the list of known discounted jets grows. Old nodes
> get a merkle path to the new jet, which they view as an unknown jet, and
> allow the transaction as a anyone-can-spend transaction. New nodes see a
> regular Simplicity redemption. (I haven't worked out the details of how
the
> P2P protocol will negotiate with old nodes, but I don't forsee any
> problems.)
>
> Note that this implies that you should never participate in any Simplicity
> contract where you don't get access to the entire source code of all
> branches to check that it doesn't have an unknown jet.
>
> On Mon, Oct 30, 2017 at 5:42 PM, Matt Corallo <lf-lists@mattcorallo•com>
> 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> 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 on Programming Languages and Analysis for
>>> Security. You find a copy of my Simplicity paper at
>>> 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 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
> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
>
[-- Attachment #2: Type: text/html, Size: 9362 bytes --]
^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [bitcoin-dev] Simplicity: An alternative to Script
2017-10-31 21:01 ` Russell O'Connor
@ 2017-11-01 1:46 ` Mark Friedenbach
0 siblings, 0 replies; 12+ messages in thread
From: Mark Friedenbach @ 2017-11-01 1:46 UTC (permalink / raw)
To: Russell O'Connor; +Cc: Bitcoin Protocol Discussion
[-- Attachment #1: Type: text/plain, Size: 7756 bytes --]
I don’t think you need to set an order of operations, just treat the jet as TRUE, but don’t stop validation. Order of operations doesn’t matter. Either way it’ll execute both branches and terminate of the understood conditions don’t hold.
But maybe I’m missing something here.
> On Oct 31, 2017, at 2:01 PM, Russell O'Connor <roconnor@blockstream•io> wrote:
>
> That approach is worth considering. However there is a wrinkle that Simplicity's denotational semantics doesn't imply an order of operations. For example, if one half of a pair contains a assertion failure (fail-closed), and the other half contains a unknown jet (fail-open), then does the program succeed or fail?
>
> This could be solved by providing an order of operations; however I fear that will complicate formal reasoning about Simplicity expressions. Formal reasoning is hard enough as is and I hesitate to complicate the semantics in ways that make formal reasoning harder still.
>
>
> On Oct 31, 2017 15:47, "Mark Friedenbach" <mark@friedenbach•org> wrote:
> Nit, but if you go down that specific path I would suggest making just
> the jet itself fail-open. That way you are not so limited in requiring
> validation of the full contract -- one party can verify simply that
> whatever condition they care about holds on reaching that part of the
> contract. E.g. maybe their signature is needed at the top level, and
> then they don't care what further restrictions are placed.
>
> On Tue, Oct 31, 2017 at 1:38 PM, Russell O'Connor via bitcoin-dev
> <bitcoin-dev@lists•linuxfoundation.org> wrote:
> > (sorry, I forgot to reply-all earlier)
> >
> > The very short answer to this question is that I plan on using Luke's
> > fail-success-on-unknown-operation in Simplicity. This is something that
> > isn't detailed at all in the paper.
> >
> > The plan is that discounted jets will be explicitly labeled as jets in the
> > commitment. If you can provide a Merkle path from the root to a node that
> > is an explicit jet, but that jet isn't among the finite number of known
> > discounted jets, then the script is automatically successful (making it
> > anyone-can-spend). When new jets are wanted they can be soft-forked into
> > the protocol (for example if we get a suitable quantum-resistant digital
> > signature scheme) and the list of known discounted jets grows. Old nodes
> > get a merkle path to the new jet, which they view as an unknown jet, and
> > allow the transaction as a anyone-can-spend transaction. New nodes see a
> > regular Simplicity redemption. (I haven't worked out the details of how the
> > P2P protocol will negotiate with old nodes, but I don't forsee any
> > problems.)
> >
> > Note that this implies that you should never participate in any Simplicity
> > contract where you don't get access to the entire source code of all
> > branches to check that it doesn't have an unknown jet.
> >
> > On Mon, Oct 30, 2017 at 5:42 PM, Matt Corallo <lf-lists@mattcorallo•com>
> > 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> 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 on Programming Languages and Analysis for
> >>> Security. You find a copy of my Simplicity paper at
> >>> 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 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
> > https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
> >
>
[-- Attachment #2: Type: text/html, Size: 9975 bytes --]
^ permalink raw reply [flat|nested] 12+ messages in thread
end of thread, other threads:[~2017-11-01 1:46 UTC | newest]
Thread overview: 12+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-10-30 15:22 [bitcoin-dev] Simplicity: An alternative to Script Russell O'Connor
2017-10-30 15:31 ` Mark Friedenbach
2017-10-30 21:42 ` Matt Corallo
2017-10-30 21:56 ` Mark Friedenbach
2017-10-30 22:14 ` Matt Corallo
2017-10-30 22:32 ` Mark Friedenbach
2017-10-30 22:50 ` Matt Corallo
2017-10-30 23:29 ` Gregory Maxwell
2017-10-31 20:38 ` Russell O'Connor
2017-10-31 20:46 ` Mark Friedenbach
2017-10-31 21:01 ` Russell O'Connor
2017-11-01 1:46 ` Mark Friedenbach
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox