[bitcoin-dev] Mempool optimized fees, etc. (Scaling Bitcoin)

[Karl Johan Alm via bitcoin-dev]

This is the paper detailing the research behind my talk "Optimizing
fee estimation via the mempool state" (the presentation only covers
part of the paper) at Scaling Stanford (this coming Sunday). Feedback
welcome.

https://bc-2.jp/mempool.pdf
___
bitcoin-dev mailing list
bitcoin-dev@lists.linuxfoundation.org
https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev

Re: [bitcoin-dev] Simplicity: An alternative to Script

[Mark Friedenbach via bitcoin-dev]

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  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"  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
>  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 
> > 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
> >>  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
> >>> 

Re: [bitcoin-dev] Simplicity: An alternative to Script

[Russell O'Connor via bitcoin-dev]

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"  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
 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 
> 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
>>  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 

Re: [bitcoin-dev] Simplicity: An alternative to Script

[Mark Friedenbach via bitcoin-dev]

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
 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 
> 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
>>  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
>>> 

Re: [bitcoin-dev] Simplicity: An alternative to Script

[Russell O'Connor via bitcoin-dev]

(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 
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