Is it theoretically possible to have a better Operational Semantics than the BitMachine

[ProofOfKeags]

One of the things I keep returning back to is how laughably silly the BitMachine's semantics seem from a silicon efficiency perspective. However, it isn't obvious that it can be done more efficiently that generalizes over all possible type-correct arrangements of the combinators. I am also assuming that since there isn't a better way presented in either the Whitepaper or Tech Report that we don't definitively know of a better way. However, do we know that no better way is possible? Why or why not?

[roconnor-blockstream]

In some sense, the combinators of Simplicity and the Bit Machine were designed hand-in-hand. There are a couple of variations in choices one could make with the combinator language and get an equivalently powerful language. Simplicity's combinator set, in particular with respect to the case combinator, is designed to make the Bit Machine design work out. The Bit Machine's padding sits between the tag and the payload allowing the "associativity" with the case expression's "context type" to transform into the representation of the pair in the branches. The "context type" is the C in (A + B) × C ⊢ D, and the Bit Machine's representation of a value of type (A + B) × C, provides immediate access to the values of either A × C or B × C as needed when evaluating the branches without needing to reformat any data.

The above is maybe incidental to what you are asking about. It is certainly possible that something else could be better for some definition of better. What would qualify as being a better operational semantics?

In a very vague sense, the Bit Machine doesn't operate so differently from how Bitcoin Script does. There are some stacks, items are pushed and popped of stack. The main difference is that the Bit Machine doesn't have byte alignment, and requires somewhat messy bit level access and realignment when marshaling data between the Bit Machine and the native code that implements jets.

(At least Simplicity isn't using ternary machine like IOTA uses. So things could always get funnier :)

[ProofOfKeags]

I suppose that we need to define "better", yes. I think my intuition is telling me that what I find comical about the operational semantics is that it seems to operate on individual bits at a time, far more low level than any typical language. Some of that seems to be a consequence of the design (we represent bits with unit types injected into a general sum). So things that would hypothetically operate on a byte may have to operate on each individual bit separately. Yes, jets can be used to address this, and I'm sure that will be fine in practice, but I was trying to assess whether it would be possible to improve the operational semantics in general or whether they are essentially a necessary consequence of Simplicity's very bare design.

[apoelstra]

I suspect that a byte-aligned or even word-aligned machine could be defined without too much trouble, with only a small constant-multiple hit to memory requirements.

@ProofOfKeags regarding "laughably silly", do you have any resources that we non-silicon people could read to try to understand some rules of thumb we could use? Alternately, do you know anybody who has experience in this area who'd be willing to chat with us for a few hours to get a shared understanding of Simplicity's semantics?

[ProofOfKeags]

To be clear, I'm not trying to actually criticize the design. I'm not actually qualified to judge that, that's actually the motivation for asking this here. I'm mostly just pointing out that doing things at the bit level seems really inefficient. Normally I don't care about it but I was curious about whether or not the design was just the minimal thing we could get working over all Simplicity programs or if we have an argument for why it actually can't be better. The byte-aligned one seems like it would be capable of using certain optimizations but I am not a hardware engineer by any stretch. I'm more of a math person like y'all are.

[ProofOfKeags]

Alternately, do you know anybody who has experience in this area who'd be willing to chat with us for a few hours to get a shared understanding of Simplicity's semantics?

I wish. I don't believe that I am any better resourced in this respect than anyone y'all might know.

[roconnor-blockstream]

From the outside it looks like Simplicity's design looks like took a bunch of trivial, very low level combinators and, through ridiculous effort, uses those combinators to program anything we want from them. We argue that these combinators are simple and, through that enormous effort, adequate in a technical sense that requires jets to order to overcome it's ridiculous primitiveness.

But let me offer you a different perspective which may help assuage concerns about the ridiculously primitive nature of Simplicity's combinators.

When designing a Blockchain programing language we will have a set of basic functionality that we will want to build programs out of. Basic functionality like adding, multiplying and dividing numbers, computing signature hashes, checking BIP-0340 schnorr signatures, etc. Eventually this basic functionality will be realized as jets in Simplicity's design, but for now let's just say we want a language that comes with some expressive set of basic functionality.

These basic functions all come with some sort of interface, that determine what inputs are acceptable and what outputs they produce on those inputs. In order to program we need ways of compose all these basic functions together to get new functionality from the parts. There is lots of different ways we can choose to enable this composition. Bitcoin Script uses stacks for this composition, where inputs and output values are places on these stacks, and these stacks come with operations to manipulate them them in such a way that the basic functions can have their inputs and outputs combined together allowing new computations that go beyond just the basic functions themselves.

From a type-theory perspective, there are just a handful of fundamental ways of combining functions together. The most basic way is by function composition, that is using the output of one function as the input to another function, but there are other ways. Another way is parallel composition, where two functions are both evaluated logically in parallel with each other (not necessarily operationally concurrent), producing two outputs. Another important way is by making a choice between evaluating one of two functions, the heart of the "if" expression. The type theory way says to create combinators to enable function composition, parallel composition, and choice composition of basic functions to derive new functions, and to recursively use those combinators again to derive further new function from those new derivations.

Type theory gives other operations for manipulating these combinations. take and drop are (one way) of accessing the two results of parallel composition. Left injection injl and right injection injr are ways to create bits (as in the digital notion of a bit) needed for the choice composition to use to make its choice. As you may have already noticed, we pick comp, pair and case as our methods of implementing function composition, parallel composition, and choice composition.

Bitcoin Script also enables these forms of composition. Function composition doesn't have have an explicit operation to enable it, just sequencing two basic functions one after the other is all you need to do this in a "concatinative" language. The dup and swap operations are fundamental to enabling parallel composition. The "if" blocks enable choice composition, and various other stack operations are needed to plumb complex "circuits" of basic functions together.

My point here is, that Simplicity's combinator design emerges before we even get to something low level. We would want Simplicity's combinators anyways, even if we were building a high-level language. The choice composition more or less requires a notion of a bit in order to make its choice. That's what "if" expressions operate on in almost every language design. So no matter what, we are going to need all this stuff.

In particular, if we want to formally reason about this language, we will need to give formal semantics to this choice of combinators, in addition to the formal semantics of each of the basic functions. From here we note that we can "complete" our combinator language by adding unit and iden and we get something that "technically" could implement any function we want. We choose to leverage this technicality as a way of specifying the formal semantics of the basic functions. Since people need to reason about the combinators anyways, and the combinators form a complete set, we can specify the basic functionality in terms of these combinators. Thus, what we have been calling basic functions, are transformed into what we now call "jets", by the act of attaching formal semantics to them by defining their semantics in terms of the combinators of the rest of the language.

Ultimately I expect Simplicity programs to mostly consist of jets, with a few uses of pair, case and comp thrown in to glue these jets together in interesting ways. The Bit Machine is a just way of interpreting this glue in order to run these jets. The glue layer necessarily has a primitive notion of bits in order to manage the case combinator, as is needed for managing any "if"-type expression. I'm not too worried about the bit alignment. After all the GIF file format's Huffman decoder also manipulates strings of unaligned bits, and AFAIK, there are not too many gripes about that. The use of Simplicity as a formal method of specifying the jets may or may not be a good idea, but it doesn't have an impact on the operation of those jets (i.e. basic functions).

P.S. Type theory does give us even more ways of combining functions. For example the, trace combinator uses recursion to find fixed points of functions. There is an abstraction combinator for applying partial input to create a suspended function (which can then be copied). However, we've excluded other combinators in Simplicity in order to restrict ourselves to a set of combinators whose complexity can be effectively analyzed and bounded.

[roconnor-blockstream]

As it stands, jets are monomorphic, so we cannot write such a thing as a jet. Also that version of assoc would have the operational semantics of iden which involves copying from the read frame to the write frame.

What I'd more likely do is

 f :: (A × B) × C ⊢ D
--------------------
assocR f :: A × (B × C) ⊢ D

and

 f :: A × (B × C) ⊢ D
--------------------
assocL f :: (A × B) × C ⊢ D

which would truly be noops in the Bit Machine.

This is really useful for getting the correct associativity needed to apply case.

Another tack would be to generalize case to look for the first sum on the left, allowing it to operate on anything of the form (...((A + B) × C1) × ... ) × Cn. But that might upset the complexity of type inference, which is currently (quasi-)linear time.

[ProofOfKeags]

Is this simply because we are exploiting the associativity of bit concatenation per frame? and so we can coerce any associative grouping into any other without needing to change the contents of the stacks?

[roconnor-blockstream]

That's correct.

[np]

During compilation to the bit machine language, could we replace compositions such as comp X Y by Y (where X is just a complex identity term such as assocs)?

I would prefer not to add new combinators and rather try to make the compiler smarter.

What do you think?

[roconnor-blockstream]

As it stands the current implementation doesn't compile into bit machine instructions, rather the simplicity combinators are interpreted: https://github.com/ElementsProject/simplicity/blob/07d3ebd68b7ed1102e6247b6d8989602acff207d/C/eval.c#L366-L559

Also the precomputed costs of evaluation are computed from the Simplicity expressions, so optimizations would either be invisible to the cost calculations, or the understanding that there is an optimization would have to be baked into the cost calculations. These costs calculations are consensus critical, so I'd like to avoid them getting more complicated than necessary. (The tail composition optimization already makes the calculation a little bit complicated: https://github.com/ElementsProject/simplicity/blob/07d3ebd68b7ed1102e6247b6d8989602acff207d/C/eval.c#L601-L683)

I suspect that having new combinators is the simplest way do add this feature. The cost calculations becomes easy to interpret because the cost of these new combinators would be trivial since they are implemented as a no-op.

[np]

Personally I've been truly amazed by this hand in hand codesign of the two languages.
First ,the high-level language of combinators is fundamental (based on sequent calculus).
Second, the translation to the low-level language shows how orthogonal each combinator is to each other:

• comp is the only combinator which allocates memory. This means that we can track memory footprint improvement through semantics preserving transformations which uses "less" comp.
• injl/injr are the pure write operations.
• unit, take, pair are only sequencing.
• case is the pure read operation which also acts on the data being read (branch on the bit value).
• iden is mostly a short-cut to avoid useless read this and write it back.

Of course bit alignments of injl, injr, case and drop are the necessary greases to make things work and they tend to clutter the otherwise nice machinery.