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