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