Re: [bitcoin-dev] Simplicity proposal - Jets?

["Adán Sánchez de Pedro Crespo" <adan@stampery.co>]

Hi everyone,

I agree that the paper could use some more details on the rationale
behind "jets". After a couple of reads, I think I can "ELI5 them":

As far as I understand, jets are a smart optimization that makes complex
Simplicity contracts way cheaper to compute (ideally, comparable to
Script or EVM).

For this purpose, jets leverage the most important element of the
Simplicity Bit Machine: the frames stack.

In a Simplicity program, every expression or sub-expression can be
thought of as a pure function that when applied on a certain initial
read frame, results in the active write frame having a different value.
This happens deterministically and without any side effects.

So, if the Simplicity interpreter finds some expression whose result
when applied upon a certain read frame is already known (because it has
already been executed or it was somehow precomputed), it doesn't need to
execute such expression step-by-step once again. Instead, it just need
to write the known result to the active write frame.

The paper suggests that at all times the interpreter knows the result of
applying many common operations on all possible combinations of inputs
in the range of 8 to 256 bits. In other words, the interpreter won't
need to calculate "123 + 321" or compare "456 > 654 because the results
of those expressions will be already known to it. These are stupid
examples, but the savings are real for hash functions internals,
elliptic curve calculations or even validation of signatures.

As said before, this can help making Simplicity programs lighter on CPU
usage, but it has many other benefits too:

+ Jets can replicate the behavior of complex chunks of Simplicity code
with the guarantee that they can't introduce side effects.

+ Interpreter-bundled jets are formally proven. The more a Simplicity
program relies on jets, the more it benefits from their safety. When
proving the soundness of your program, you can just ignore the jets,
assume they are valid and focus on your own logic.

The paper also suggests that different sets of jets could make up
different single purpose dialects, just like domain-specific languages
bring richer vocabulary and semantics to the bare syntax and grammar of
general-purpose languages.

I hope Russel or Mark can correct me if I got something totally wrong. I
must admit I really like this proposal and hereby declare myself a huge
fan of their work :)

-- 
Adán Sánchez de Pedro Crespo
CTO, Stampery Inc.
San Francisco - Madrid