A data structure to help the calculation of stack size limits.
Conceptually, every SatInfo object corresponds to a (possibly empty) set of script execution traces (sequences of opcodes).
- SatInfo{} corresponds to the empty set.
- SatInfo{n, e} corresponds to a single trace whose net effect is removing n elements from the stack (may be negative for a net increase), and reaches a maximum of e stack elements more than it ends with.
- operator| is the union operation: (a | b) corresponds to the union of the traces in a and the traces in b.
- operator+ is the concatenation operator: (a + b) corresponds to the set of traces formed by concatenating any trace in a with any trace in b.
Its fields are:
- valid is true if the set is non-empty.
- netdiff (if valid) is the largest difference between stack size at the beginning and at the end of the script across all traces in the set.
- exec (if valid) is the largest difference between stack size anywhere during execution and at the end of the script, across all traces in the set (note that this is not necessarily due to the same trace as the one that resulted in the value for netdiff).
This allows us to build up stack size limits for any script efficiently, by starting from the individual opcodes miniscripts correspond to, using concatenation to construct scripts, and using the union operation to choose between execution branches. Since any top-level script satisfaction ends with a single stack element, we know that for a full script:
- netdiff+1 is the maximal initial stack size (relevant for P2WSH stack limits).
- exec+1 is the maximal stack size reached during execution (relevant for P2TR stack limits).
Mathematically, SatInfo forms a semiring:
- operator| is the semiring addition operator, with identity SatInfo{}, and which is commutative and associative.
- operator+ is the semiring multiplication operator, with identity SatInfo{0}, and which is associative.
- operator+ is distributive over operator|, so (a + (b | c)) = (a+b | a+c). This means we do not need to actually materialize all possible full execution traces over the whole script (which may be exponential in the length of the script); instead we can use the union operation at the individual subexpression level, and concatenate the result with subexpressions before and after it.
- It is not a commutative semiring, because a+b can differ from b+a. For example, "OP_1 OP_DROP" has exec=1, while "OP_DROP OP_1" has exec=0.
Definition at line 439 of file miniscript.h.