Question about witnesses in the main function

SimplicityHL development
1

In the office hours on 11 Aug, @tvolk131 asked about witnesses in the main function. For some background, the current rule is that witness::FIELD cannot appear outside of the main function.
Firstly, this is a SimplicityHL requirement, simplicity itself does not have any notion of functions.
Secondly, I think this is purely a design choice, since the compiler explicitly checks for witnesses outside of main and errors. Unfortunately, the code doesn’t have any reasoning in the comments. SimplicityHL/src/ast.rs at master · BlockstreamResearch/SimplicityHL · GitHub

I don’t think there is any real consequence to allowing witness values to be read later. The elements run time actually only reads the witness input stack as it is needed.

The only rational I can think for this rule is to prevent foot guns. Perhaps someone else has some insight?

If we do change it, I would suggest we keep the restriction that witnesses can only be read in the entry file, to prevent any possible shenanigans of libraries reading witness data they shouldn’t have access to.

2

The reason is a compiler limitation – right now whenever a function is called, we compile it inline. If you call it twice, it gets compiled twice.

This sounds crazy but it kinda makes sense in the Simplicity model – Simplicity itself does not have any loops or gotos; if you want to run a section of code multiple times in a row, it really does get evaluated afresh multiple times in a row. Sharing lets you avoid encoding repeated expressions multiple times, but sharing is essentially just an encoding optimization. It doesn’t affect the “real program” as it is run in the Bit Machine.

However, consider what would happen if there were a witness node in an expression that was evaluated multiple times. Ignoring sharing (which has no semantic effect), this would appear on-chain as multiple witness nodes. If the user put the same witness on every node, they’d be shared and everything would “just work”. But there is no requirement that the user do this. The user could just as well unshare the program, put different witnesses in each instance of an expression, then reshare.

The TL;DR is that if you had a function func that contained witness::WIT, then every time func was called, it could be called with a distinct WIT. But in the SimplicityHL model, every witness name corresponds to a single witness. So the compiled code would not correspond to the model of the code, and this would almost certainly lead to coin-stealing bugs.

3

I’ve been thinking a bit about whether we should introduce a Reader effect into SimplicityHL used for witness and parameter accesses. This is a jargony way of saying that the type signature of functions would indicate which witnesses and parameters they use. We could extend this to module boundaries – modules would also need to declare what parameters and witnesses they access.

This would help us add CMR quoting to the language in a sensible way. In the quotation of an expression, witnesses become constants and parameters become inputs. Making this comprehensible to a reader of the code seems like it’d require some sort of annotation of what witnesses and params are present in the expression.

We could then easily relax the “witnesses only appear in main” rule to “only one function in the full compilation may access each witness”. But relaxing it further would require a sort of preamble in which we composed each witness with pair iden iden (the “duplication operator”) and compiled every access to the witness into one of those iden branches rather than directly compiling them as witness nodes.

4

Sorry to triple-post, but I realize we’ve already implemented logic that does this (or something similar anyway).

The program

fn main() {
    let x: u32 = witness::B;
    assert!(jet::eq_32(x, x));
}

compiles to
(witness & iden); (((((OH & OH); jet_eq_32 ); jet_verify ) & unit); IH)

Because our compiler, for each let binding, implements this as a composition of the let-binding (witness & iden, where witness is the binding and iden carries forward any previous bindings) with the rest of the block, which can then refer to the binding with “selectors” such as OH which you see, which are trees of drops and takes that index into the input value to obtain specific values.

So one way to allow witnesses to appear in multiple functions, we could implement logic which “hoists” any witness accesses above main into a top-level pre-main block which creates let-bindings for each witnes. Then witness references in the functions themselves would compile to selectors into the let-bound values.

If we did this for every witness access, whether it appeared in one function or many, in main or elsewhere, we’d effectively have turned witnesses into implicit function parameters, and then again we might wonder whether we want to add syntax for this (and even whether this syntax should be mandatory, since witness access is a side-effect in SimplicityHL) (even though it’s not in Simplicity). This would have a nontrivial on-chain cost: in cases where witness data was accessed only once, rather than compiling to a single witness node, this access would become (witness & iden); followed by some selector (and every single other selector would need to be enlarged to select around the witness).

But if we didn’t do this, say, we only did this hoisting for witness values that appeared in more than one function, then we have “spooky action at a distance” where functions compile into different programs – and even have different input type signatures – depending on whether they appear alongside a different function that makes the same access. This would have surprising efficiency properties, complicate definition of an ABI and a linker, and undermine covenant logic which often needs to know the exact CMR of particular pieces of code.

Effects, witnesses, parameters and purity