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

<p>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 <a href="https://blockstream.com/simplicity.pdf" rel="noreferrer">whitepaper</a>).  This <a href="https://github.com/ElementsProject/simplicity/blob/23626323d19d6b996a16c4d9e01c6cbc5610aef7/Coq/Simplicity/Translate.v#L74-L84" rel="noreferrer">translation</a> 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.</p>

<p>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 <a href="https://blockstream.com/simplicity.pdf" rel="noreferrer">whitepaper</a>) 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 <a href="https://github.com/ElementsProject/simplicity/blob/23626323d19d6b996a16c4d9e01c6cbc5610aef7/Coq/Simplicity/StaticAnalysis.v#L403-L411" rel="noreferrer">memory static analysis algorithm is already verified correct</a> with the Coq proof assistant.</p>

<p>On the other hand, Script comes with a few wrinkles that can impede static analysis.  In particular <code>DEPTH</code> is non-local (i.e. it isn't a simple function of a fixed number of stack elements), and <code>IFDUP</code> 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 <code>IF</code> <code>ENDIF</code> block that the number of stack items left would be identical in either case (compared this with Simplicity's <code>case</code> combinator that requires the resulting type of the two branches to be identical).  And lastly while <code>ROLL</code>, <code>PICK</code>, and <code>CHECKMULTISIG</code> are usually used with a constant <code>n</code> (and <code>m</code>) parameters, nothing guarantees this is the case.</p>

<p>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.</p>

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

<p>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.</p>

<p>For reference, the <a href="https://vm100.cs.stir.ac.uk/~rkl/home.html" rel="noreferrer">SCRIPT Analyser</a> 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 <a href="https://vm100.cs.stir.ac.uk/~rkl/home.html" rel="noreferrer">SCRIPT Analyser</a> 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 href="https://github.com/ElementsProject/simplicity/blob/23626323d19d6b996a16c4d9e01c6cbc5610aef7/Coq/Simplicity/SHA256.v#L232-L233" rel="noreferrer">a proof of correctness of the SHA-256 implementation in Simplicity</a>).</p>

CC BY-SA 4.0
2020-04-17T20:23:37.603Z
2020-04-17T20:34:57.797Z
2020-04-17T20:34:57.797Z
Russell O'Connor
<p>Quoted from the <a href="https://blockstream.com/simplicity.pdf" rel="noreferrer">whitepaper</a>, one of the design goals of Simplicity is:</p>

<blockquote>
  <p>Provide  formal  semantics  that  facilitate  easy  reasoning  about  programs using existing off-the-shelf proof-assistant software.</p>
</blockquote>

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

<script><simplicity>
How is Simplicity better suited for static analysis compared to script?
MCCCS
# How is Simplicity better suited for static analysis compared to script?

(Asked by: username_0 on 2020-04-17)

Quoted from the [whitepaper](https://blockstream.com/simplicity.pdf), 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?

**Tags:** script, simplicity


---

## 1 answers

### Answer by username_1 on 2020-04-17. Score: 6 | Accepted answer

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](https://blockstream.com/simplicity.pdf)). This [translation](https://github.com/ElementsProject/simplicity/blob/23626323d19d6b996a16c4d9e01c6cbc5610aef7/Coq/Simplicity/Translate.v#L74-L84) 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](https://blockstream.com/simplicity.pdf)) 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](https://github.com/ElementsProject/simplicity/blob/23626323d19d6b996a16c4d9e01c6cbc5610aef7/Coq/Simplicity/StaticAnalysis.v#L403-L411) 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](https://github.com/bitcoin/bitcoin/pull/16902)). 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](https://vm100.cs.stir.ac.uk/~rkl/home.html) 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](https://vm100.cs.stir.ac.uk/~rkl/home.html) 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](https://github.com/ElementsProject/simplicity/blob/23626323d19d6b996a16c4d9e01c6cbc5610aef7/Coq/Simplicity/SHA256.v#L232-L233)).


---

