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 <***@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" <***@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
> <email@example.com> 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 <firstname.lastname@example.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
> >> <email@example.com> 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
> > firstname.lastname@example.org
> > https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev