<div dir="auto"><div>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?<div dir="auto"><br></div><div dir="auto">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.</div><br><div class="gmail_extra"><br><div class="gmail_quote">On Oct 31, 2017 15:47, "Mark Friedenbach" <<a href="mailto:mark@friedenbach.org">mark@friedenbach.org</a>> wrote:<br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Nit, but if you go down that specific path I would suggest making just<br>
the jet itself fail-open. That way you are not so limited in requiring<br>
validation of the full contract -- one party can verify simply that<br>
whatever condition they care about holds on reaching that part of the<br>
contract. E.g. maybe their signature is needed at the top level, and<br>
then they don't care what further restrictions are placed.<br>
<br>
On Tue, Oct 31, 2017 at 1:38 PM, Russell O'Connor via bitcoin-dev<br>
<div class="elided-text"><<a href="mailto:bitcoin-dev@lists.linuxfoundation.org">bitcoin-dev@lists.<wbr>linuxfoundation.org</a>> wrote:<br>
> (sorry, I forgot to reply-all earlier)<br>
><br>
> The very short answer to this question is that I plan on using Luke's<br>
> fail-success-on-unknown-<wbr>operation in Simplicity. This is something that<br>
> isn't detailed at all in the paper.<br>
><br>
> The plan is that discounted jets will be explicitly labeled as jets in the<br>
> commitment. If you can provide a Merkle path from the root to a node that<br>
> is an explicit jet, but that jet isn't among the finite number of known<br>
> discounted jets, then the script is automatically successful (making it<br>
> anyone-can-spend). When new jets are wanted they can be soft-forked into<br>
> the protocol (for example if we get a suitable quantum-resistant digital<br>
> signature scheme) and the list of known discounted jets grows. Old nodes<br>
> get a merkle path to the new jet, which they view as an unknown jet, and<br>
> allow the transaction as a anyone-can-spend transaction. New nodes see a<br>
> regular Simplicity redemption. (I haven't worked out the details of how the<br>
> P2P protocol will negotiate with old nodes, but I don't forsee any<br>
> problems.)<br>
><br>
> Note that this implies that you should never participate in any Simplicity<br>
> contract where you don't get access to the entire source code of all<br>
> branches to check that it doesn't have an unknown jet.<br>
><br>
> On Mon, Oct 30, 2017 at 5:42 PM, Matt Corallo <<a href="mailto:lf-lists@mattcorallo.com">lf-lists@mattcorallo.com</a>><br>
> wrote:<br>
>><br>
>> I admittedly haven't had a chance to read the paper in full details, but I<br>
>> was curious how you propose dealing with "jets" in something like Bitcoin.<br>
>> AFAIU, other similar systems are left doing hard-forks to reduce the<br>
>> sigops/weight/fee-cost of transactions every time they want to add useful<br>
>> optimized drop-ins. For obvious reasons, this seems rather impractical and a<br>
>> potentially critical barrier to adoption of such optimized drop-ins, which I<br>
>> imagine would be required to do any new cryptographic algorithms due to the<br>
>> significant fee cost of interpreting such things.<br>
>><br>
>> Is there some insight I'm missing here?<br>
>><br>
>> Matt<br>
>><br>
>><br>
>> On October 30, 2017 11:22:20 AM EDT, Russell O'Connor via bitcoin-dev<br>
>> <<a href="mailto:bitcoin-dev@lists.linuxfoundation.org">bitcoin-dev@lists.<wbr>linuxfoundation.org</a>> wrote:<br>
>>><br>
>>> I've been working on the design and implementation of an alternative to<br>
>>> Bitcoin Script, which I call Simplicity. Today, I am presenting my design<br>
>>> at the PLAS 2017 Workshop on Programming Languages and Analysis for<br>
>>> Security. You find a copy of my Simplicity paper at<br>
>>> <a href="https://blockstream.com/simplicity.pdf" rel="noreferrer" target="_blank">https://blockstream.com/<wbr>simplicity.pdf</a><br>
>>><br>
>>> Simplicity is a low-level, typed, functional, native MAST language where<br>
>>> programs are built from basic combinators. Like Bitcoin Script, Simplicity<br>
>>> is designed to operate at the consensus layer. While one can write<br>
>>> Simplicity by hand, it is expected to be the target of one, or multiple,<br>
>>> front-end languages.<br>
>>><br>
>>> Simplicity comes with formal denotational semantics (i.e. semantics of<br>
>>> what programs compute) and formal operational semantics (i.e. semantics of<br>
>>> how programs compute). These are both formalized in the Coq proof assistant<br>
>>> and proven equivalent.<br>
>>><br>
>>> Formal denotational semantics are of limited value unless one can use<br>
>>> them in practice to reason about programs. I've used Simplicity's formal<br>
>>> semantics to prove correct an implementation of the SHA-256 compression<br>
>>> function written in Simplicity. I have also implemented a variant of ECDSA<br>
>>> signature verification in Simplicity, and plan to formally validate its<br>
>>> correctness along with the associated elliptic curve operations.<br>
>>><br>
>>> Simplicity comes with easy to compute static analyses that can compute<br>
>>> bounds on the space and time resources needed for evaluation. This is<br>
>>> important for both node operators, so that the costs are knows before<br>
>>> evaluation, and for designing Simplicity programs, so that smart-contract<br>
>>> participants can know the costs of their contract before committing to it.<br>
>>><br>
>>> As a native MAST language, unused branches of Simplicity programs are<br>
>>> pruned at redemption time. This enhances privacy, reduces the block weight<br>
>>> used, and can reduce space and time resource costs needed for evaluation.<br>
>>><br>
>>> To make Simplicity practical, jets replace common Simplicity expressions<br>
>>> (identified by their MAST root) and directly implement them with C code. I<br>
>>> anticipate developing a broad set of useful jets covering arithmetic<br>
>>> operations, elliptic curve operations, and cryptographic operations<br>
>>> including hashing and digital signature validation.<br>
>>><br>
>>> The paper I am presenting at PLAS describes only the foundation of the<br>
>>> Simplicity language. The final design includes extensions not covered in<br>
>>> the paper, including<br>
>>><br>
>>> - full convent support, allowing access to all transaction data.<br>
>>> - support for signature aggregation.<br>
>>> - support for delegation.<br>
>>><br>
>>> Simplicity is still in a research and development phase. I'm working to<br>
>>> produce a bare-bones SDK that will include<br>
>>><br>
>>> - the formal semantics and correctness proofs in Coq<br>
>>> - a Haskell implementation for constructing Simplicity programs<br>
>>> - and a C interpreter for Simplicity.<br>
>>><br>
>>> After an SDK is complete the next step will be making Simplicity<br>
>>> available in the Elements project so that anyone can start experimenting<br>
>>> with Simplicity in sidechains. Only after extensive vetting would it be<br>
>>> suitable to consider Simplicity for inclusion in Bitcoin.<br>
>>><br>
>>> Simplicity has a long ways to go still, and this work is not intended to<br>
>>> delay consideration of the various Merkelized Script proposals that are<br>
>>> currently ongoing.<br>
><br>
><br>
><br>
</div><div class="elided-text">> ______________________________<wbr>_________________<br>
> bitcoin-dev mailing list<br>
> <a href="mailto:bitcoin-dev@lists.linuxfoundation.org">bitcoin-dev@lists.<wbr>linuxfoundation.org</a><br>
> <a href="https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev" rel="noreferrer" target="_blank">https://lists.linuxfoundation.<wbr>org/mailman/listinfo/bitcoin-<wbr>dev</a><br>
><br>
</div></blockquote></div><br></div></div></div>