Support for exact annex padding

[roconnor-blockstream]

Simplicity programs have a cost associated with them. This cost is computed from a worst case static analysis of the (pruned) Simplicty program prior to execution. This cost is computed in milliWU and must be less than or equal to the provided budget, which is defined to be the WU of the input under consideration.

We expect that most common and simple use cases of Simplicity, the budget computed form the serialized Simplicity program will be more than adequate to cover the cost computed form the static analysis of the program.

However, the due to sub-expression sharing, the cost of Simplicity programs can be exponential in the serialized size of the program, leading to cases where the budget is inadequate to cover the required costs. In particular this can happen when using the higher level for_while construction. The intended solution in this case is to pad the input's annex in order to increase the budget to adequate levels.

However, there is a design flaw with Taproot's annex, an input's signature can only cover it's own annex, and not the annex of other inputs. While most of the time users are incentivized to minimize their transaction's weight, in some circumstances within a multi-party protocol, one party could prefer to sabotage the transaction they are participating in by substituting their input's annex with a very large annex in order to increase the transaction size and decrease the transaction's fee weight. Because inputs only sign their own annex, this substitution can even be done after the transaction is signed by all parties, and one party replaces their own signature with an otherwise identical one signing a heavy annex. This party would then try to quickly broadcast this heavy transaction, and "pinning" the other party's inputs.

With fullRBF on by default, such pinning attacks are perhaps harder to pull off, but I believe it is still a concern.

Currently we have standardness rules that forbid the annex form appearing in transaction, and these standardness rules prevent such attacks from being practical to pull off. However, this standardness rules rule currently forbids padding the annex in cases where it is needed to increase the budget of Simplicity programs.

To this end we want to carve out a minimal standardness rule to allow padding of Simplicity programs, at least until we get other adequate rules regarding allowed annex uses. The obvious minimal standardness rule is an annex consisting of only 0x00 bytes that is adequate to cover the costs of an input's Simplicity program, but no more. The carve out only allows a single possible annex for simplicity programs, one that is adequate for satisfying it's needed budget.

If an annex is needed, then under most circumstances this specification will yield a budget, b, in WU, such that the cost c, in milliWU satifies b-1 < c <= b. However, in rare cases, adding one more 0x00 byte to the annex will increase the budget by 2 or more WU. This is because the varint prefix of the annex counts towards the budget and the varint prefix is itself variable width. Similar considerations also hold from going from no-annex to empty-but-now-existing annex, which adds an entire stack item to the witness stack. Thus the required invariant is l < c <= b where b is the budget, c is the cost and l is "what the budget would be if the annex had one less byte in it or in the case of the empty annex, if the annex didn't exist at all".

Notice that the strictness of the inequalities is important if we are being exact. If the rule were instead l <= c <= b then if it were to happen that c were exactly l down to the the exact milliWU, there would be two annex sizes that would support that cost, which would add a small malleability in the allowed size of the annex.

It is also important to note that this proposed restriction would only be a standardness rule, and would not apply in cases where standardness is not applied. Thus for block validation, or in other cases where standardness is disabled, then the consensus rule, c <= b, would only be applied.

Some changes to the libSimplicity API is needed to support this exact annex padding proposal. We need the ability to reject programs when the l < c constraint is violated after the static analysis is performed.

To this end, the proposal is to add a minCost parameter to simplicity_elements_execSimplicity to complement the existing budget parameter. The code would fail with a new error message if the statically computed costs are not strictly greater than the minCost.

To disable this check, users can pass in 0 to the minCost field. While this technically imposes a new constraint that the statically computed costs must be strictly positive, this constraint happens to already always be satisfied. This is because all Simplicity program must consist of at least one node, and every node has at minimum a cost of 100 milliWU.

[uncomputable]

If the rule were instead l <= c <= b then if it were to happen that c were exactly l down to the the exact milliWU, there would be two annex sizes that would support that cost, which would add a small malleability in the allowed size of the annex.

Trying to wrap my head around this standardness rule, what changes? In rare cases, consensus allows for two possible annex lengths instead of one. Consensus allows for arbitrary annex bytes and there is no upper bound on the annex length.

To summarize the new standardness rule:

1. Enforce 0x00 bytes in the annex
2. Enforce exactly one annex length per cost in milliWU
   1. Enforce a lower bound using minCost
   2. Enforce an upper bound using budget

Is this accurate?

[apoelstra]

Trying to wrap my head around this standardness rule, what changes? In rare cases, consensus allows for two possible annex lengths instead of one.

Consensus allows for any annex length whatsoever as long as the transaction fits in a block. Current standardness rules allow only one length (zero). If we want to use the annex for simplicity padding then we need to relax that, but in doing so, we need to avoid introducing any malleability potential.

To summarize the new standardness rule:

Yes.

[roconnor-blockstream]

1. Enforce 0x00 bytes in the annex

   2. Enforce exactly one annex length per cost in milliWU

      1. Enforce a lower bound using minCost
      2. Enforce an upper bound using budget

1. Enforce 0x00 bytes in the annex

2. Enforce exactly one annex length per cost in milliWU

   1. Set the minCost to what the transaction weight would have been if the annex were one byte smaller (plus some subtlety around going from the "empty annex" to the "no annex") or set minCost to 0 if there is "no annex".
   2. Enforce an upper bound using budget

Consensus allows for any annex length whatsoever as long as the transaction fits in a block. Current standardness rules allow only one length (zero).

Technically standardness requires no annex, which is slightly different from the empty annex (Peter Todd pointed this out to me on the mailing list).