3

Quoted from the whitepaper, one of the design goals of Simplicity is:

Provide formal semantics that facilitate easy reasoning about programs using existing off-the-shelf proof-assistant software.

How does Simplicity achieve being more static-analysis-friendly than script? Is it the read-write order in the bit machine?

4

For this answer, I will mainly focus on static analysis of computation resources such as memory use and time.

In Simplicity, we have a separation between the Simplicity language and the language of the Bit Machine with a formal translation from the Simplicity language to the Bit Machine language (see Figure 2 from the whitepaper). This translation has been formalized in the Coq proof assistant. Only the Simplicity language is exposed at the blockchain's consensus layer with the Bit Machine technically being an implementation detail. This means that only the Simplicity language needs to be analyzed.

Because Simplicity subexpressions can only manipulate their local data (i.e. from the point of view of the Bit Machine implementation, Simplicity subexpressions can only manipulate the top of the read and write stacks), we can write a simple recursive analysis to determine computation costs such as memory use (see Figure 3 and Figure 5 from the whitepaper) and similarly for time resources (not yet implemented). Furthermore, the Simplicity combinators are extraordinarily simple, which makes the static analysis practical. One form of the memory static analysis algorithm is already verified correct with the Coq proof assistant.

On the other hand, Script comes with a few wrinkles that can impede static analysis. In particular DEPTH is non-local (i.e. it isn't a simple function of a fixed number of stack elements), and IFDUP leaves one or two items on the stack depending on the runtime value of the top stack item. Nothing in Script guarantees that when exiting an IF ENDIF block that the number of stack items left would be identical in either case (compared this with Simplicity's case combinator that requires the resulting type of the two branches to be identical). And lastly while ROLL, PICK, and CHECKMULTISIG are usually used with a constant n (and m) parameters, nothing guarantees this is the case.

All this makes static analysis of memory use that much more complicated to do for a generic Script program, though for specific normal Script programs that do not use/abuse the above OP codes, analysis is probably feasible.

The story for time analysis is a bit better since Script just iterates through the code. Though ROLL is problematic since it requires O(n) work. (Recently the implementation of IF was repaired so that it now only requires O(1) work). Simplicity combinators only require constant amount of time each, with the exception of iden, which copies a statically known number of bits when implemented in the Bit Machine. Because the amount of work for iden is known statically, we can incorporate that into our analysis.

Simplicity aims to make static analysis of computation resources easier than for Script while at the same time increasing the practical expressiveness of the language.

For reference, the SCRIPT Analyser that I am aware of makes simplifying assumptions about Script operations (e.g. that values passed to OP_IF are either 0 or 1). On the other hand, the SCRIPT Analyser does a full symbolic analysis rather than time and space resource analysis. Such a symbolic analysis probably isn't practical for Simplicity programs. Instead one is expected to use the formal semantics of Simplicity to directly reason about Simplicity expressions (for example we have a proof of correctness of the SHA-256 implementation in Simplicity).

| improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.