Timelock Jets

[roconnor-blockstream]

Add timelock related jets.

[ProofOfKeags]

I attempted to review the Haskell portion of this code, and while everything looks fine, it revealed to me that I can't quite follow the jet indirection and I feel like I'm missing the overall Jet architecture for the Haskell stuff. IIRC the C code is really how the Jets are going to land in anything that approximates consensus code. Is the purpose of the Haskell implementation to make testing Jet equivalence easier?

[roconnor-blockstream]

The Haskell code is largely there as a reference to compare the C code to. That and the C code doesn't do any encoding; just decoding, similar to how Bitcoin's Script implementation didn't/doesn't let you construct arbitrary Scripts. At the moment Haskell is the only way to generate Simplicity programs. Though Rust-Simplicity should add another venue.

That all said, I've decided that the Jet implementation in Haskell has ended up as a big mess. It was designed to be generic over any possible choice of jets, but the encoding scheme ended up only allowing specific jets and the resulting mismatch has caused all sorts of headaches and this extremely awkward jet-substitution implementation.

Thanks for your review!

[ProofOfKeags]

My understanding of the purpose of jets is that it will encounter specific merkle nodes in the AST and recognize them as being interchangeable with alternate operational semantics than the standard bit machine. That suggests to me that jet code probably doesn't need to be in any sort of compiler, of which the Haskell code seems like it is serving as a compiler front end for simplicity expressions. Since the operational interpreter for simplicity is unlikely to be anything other than C, it perhaps doesn't make sense to actually implement any of the Jets in Haskell.

That said, quickcheck can be a useful tool for checking bit-machine, haskell jet, and c-jet semantics equivalence for testing purposes. So maybe as a form of runnable documentation it can be helpful but I don't anticipate it having much reach beyond that. Though it does occur to me that if certain expressions are equivalent to each other and one of them is jetted you'd want to know which one was jetted and what substitutions were valid in the compiler front end so that you could always select the fastest implementation. I'd liken this to the code-generation step of a compiler.

At the end of the day it seems less important that the Haskell code can actually efficiently implement the jets, but it does seem to need to be able to be aware of the set of available jets if you want efficient compiler output.

[roconnor-blockstream]

Yes, the primary purpose here is to (1) test that the simplicity expressions for jets are behaving the way we want them to (i.e. we aren't jetting the wrong thing) and (2) via the FFI test that the C jets also behave in accordance to the expressions they are jetting.

During testing, Haskell needs to implement evaluation using (other) jets because otherwise testing by evaluating Simplicity is just too slow for things like schnorr signature verification.

[ProofOfKeags]

During testing, Haskell needs to implement evaluation using (other) jets because otherwise testing by evaluating Simplicity is just too slow for things like schnorr signature verification.

This seems like it may work as an inductive step to assert that the jet has the correct semantics, but you would still need to anchor down to base Simplicity in order to guarantee that any of the proofs you draw up on the simplicity expressions extend to their jet counterparts.

Also perhaps this isn't correct place for me to be talking about this, do you have a more appropriate forum to talk more about the general design of Simplicity and the codebase. I don't want to hijack your PR for architectural discussion 😅

[roconnor-blockstream]

There is ##simplicity on the libera.chat IRC network.

[apoelstra]

ACK c0f5aff

(I don't think the comment nit is a blocker, but I'd appreciate a fix.) Interesting notation "distance" and "duration". Did you invent this? I think these terms are pretty clear/unambiguous.

[roconnor-blockstream]

I was unable to find an aeronautic or otherwise term for vertical displacement (other than "vertical separation") so I ended up going with "distance".

[ProofOfKeags]

Altitude? Not that I’m trying to bikeshed this. 😅

…

On Tue, Apr 19, 2022 at 8:53 AM roconnor-blockstream < ***@***.***> wrote: I was unable to find an aeronautic or otherwise term for vertical displacement (other than "vertical separation") so I ended up going with "distance". — Reply to this email directly, view it on GitHub <#83 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA6YY44ISO43ZSQSYWD2WALVF3CG7ANCNFSM5RVSJXQA> . You are receiving this because you commented.Message ID: ***@***.***>

[roconnor-blockstream]

Altitude is usually an "absolute" value rather than "relative" value, either against mean sea level (true altitude) or the terrain (absolute altitude).

[roconnor-blockstream]

What I was looking for was a word that means "difference in height" in the same way that distance (or displacement) means "difference in position", or how duration means "difference in time".

[apoelstra]

ACK 8eccd8d