BIP-379: note that the type properties assume their requirements #2267

The "s", "f" and "e" descriptions in the Security section read as guarantees for every expression, but they only hold for expressions that meet the malleability requirements of the type system.

thresh is the clearest case: its rule is e=all are s, so thresh(2,or_i(pk(A),pk(B)),a:or_i(pk(C),pk(D))) is "e" even though each or_i child has two unconditional dissatisfactions, giving the threshold four; the opposite of the "unique unconditional dissatisfaction" the description promises. (Confirmed by spending or_d(thresh(...),pk(E)) through its second branch: all four witnesses, differing only in the two branch-selector bytes, are accepted by the script engine.)

Nothing is wrong with the rule. Such a threshold fails the "e" requirement that the malleability table imposes for non-malleability, and non-malleability is conjunctive, so the expression and everything containing it is malleable either way; the property value is a don't-care there. This just says so, so that implementations agreeing on those values are not read as contradicting the descriptions.

Prompted by bitcoin/bitcoin#36028 and the BIP 379 test vector PR, where the type of a malleable expression has to be agreed on as well.

I'm going to create a PR soon that updates rust-bitcoin to align with this change and bitcoin/bitcoin#36028 (and https://github.com/btcsuite/btcd/pull/2592 is updated as well).

cc @sipa, @apoelstra

The same is true for the correctness properties. They're all written assuming the Requirements condition already holds.

The same is true for the correctness properties. They're all written assuming the Requirements condition already holds.

Hmm, I see... Thanks for taking a look. Are you suggesting to formulate the caveat more broadly to also include the correctness properties? Or are you saying that this change is not necessary at all as it should already be clear to a reader of the BIP that the requirements conditions need to hold first?

The same is true for the correctness properties

I don't think this is true. At the very least, I think this is a bit more subtle than "you need to be non-malleable to guarantee correctness". If we said that the implication is that you cannot construct malleable Miniscripts or else your coins might be locked.

If the correctness properties are conditional at all (I spent several minutes checking and could not find an instance where they were), the conditionality will be limited to e.g. n's claim about "no satisfaciton needs 0" needing to be amended to "no nonmalleable satisfaction needs 0".

Oh, @sipa did you mean to say:

• the security properties all assume correctness holds (definitely true); or
• the correctness properties all assume that nonmalleability holds (what I initially read you as saying)

Okay, rereading the PR and assuming sipa meant "security requires correctness", I think we should instead change the text to say something like:

"While the s property matches its description for all correct Miniscripts, regardless of malleability, f and e may fail to match their descriptions in malleable scripts. That is, a malleable f expression may be dissatisfiable without a signature, and a malleable e expression may have multiple unconditional satisfactions and/or conditional satisfactions that can be produced without a signature.

"In other words, once an expression is determined to be malleable, any expression containing that expression is malleable. These three type properties can recursively preserve malleability, but they cannot recover it once it is lost.

"If the correctness properties are not met, none of these properties are meaningful and this BIP says nothing at all about the script.

IIIRC:

• The correctness-related type properties in the BIP/website are all written with the assumption that the correctness-Requirement condition on the same fragment holds.
• The malleability-related type properties in the BIP/website are all written with the assumption that the nonmalleability-Requirement condition on the same fragment holds.

I'm in favor of clarifying this in the BIP, as it's pretty non-obvious.

An alternative approach that we could pursue (but makes it a more substantial BIP change) is to define all correctness properties as "Valid AND x", for example make "z" mean "Valid AND zero arguments consumer", and the same with the malleability type properties, making "e" mean "Nonmalleable AND uniquely dissatisfiable".

This would remove all implementation-specific freedom in typing of invalid/nonmalleable things. It also wouldn't really change the test vector implementations, because they could be written as "check that validity matches, and if valid, check that the validity type properties match. If so, also check that malleability matches, and if nonmalleable, check that the malleability type properties match".

@guggero why can't we just fix the thresh rule in the BIP to say that e requires the children to be e? Are there other cases where the f/e/s rules fail to match their descriptions?

Okay, I like sipa's framing here. The tables give the requirements for correctness/nonmalleability, and once you fail to meet the requirements, it's game over and the table stops providing meaningful information. Agree we should make this explicit in the BIP. @sipa ok, great, agreed on all counts. (And I don't think we should attempt the invasive "valid AND" change, which feels like it'd add a ton of noise, for as you say, no benefit.)

What about doing this implicitly?

Add a sentence above/below both tables that says "The type properties all implicitly require the condition under Requirement. Their only purpose is helping reason about correctness/malleability, so they are useful in expressions that already invalid/malleability."

The actual logic implementing this can be pushed to the tests, so no internal code changes are needed, but the tests vectors would drop z/o/n/d/u from invalid cases, and drop s/f/e from malleable cases.

the tests vectors would drop z/o/n/d/u from invalid cases, and drop s/f/e from malleable cases

I like this idea, and proposed the same change in rust-miniscript here https://github.com/rust-bitcoin/rust-miniscript/pull/1032#issuecomment-5380985927. It would also clarify the situation for rust-miniscript users (if they fail correctness the Miniscript won't parse, but if they fail malleability they will get a usable expression that might have s/f/e properties but for which these properties are meaningless).

It's just a question of whether it's worth updating all the test vectors, which might require some mildly annoying sed work. Or a few cents of LLM tokens.

Great, thank you both for the feedback and suggestions!

Add a sentence above/below both tables that says "The type properties all implicitly require the condition under Requirement. Their only purpose is helping reason about correctness/malleability, so they are useful in expressions that already invalid/malleability."

I like that too! I'll change this PR to add that sentence instead, sounds to me like there's agreement on that so far.

the tests vectors would drop z/o/n/d/u from invalid cases, and drop s/f/e from malleable cases

No problem, I'm happy to do that. Shouldn't be too big of a lift.

I'm going to create a new PR for the suggested approach in https://github.com/rust-bitcoin/rust-miniscript/pull/1032#issuecomment-5380985927, then I can rebase my "test vector extraction" branch on that, which should prevent quite a bit of manual work already.

I've updated the wording to match your suggestions. And a proposal for implementing the suggested property erasure on malleable expressions can be found in https://github.com/rust-bitcoin/rust-miniscript/pull/1037.

Concept ACK https://github.com/rust-bitcoin/rust-miniscript/pull/1037 which sets s/f/e to false for all nonmalleable scripts and updates the test vectors accordingly.

ACK a320fe8d7e3f37388fe1c57f026471237c3167ac.

But I would suggest adding one more paragraph Implementors of APIs which unconditionally return values for these properties should always return false for malleable expressions.

ACK a320fe8.

But I would suggest adding one more paragraph Implementors of APIs which unconditionally return values for these properties should always return false for malleable expressions.

Thank you, added that paragraph below the malleability properties table.

ACK acbc7b000bf8655ecf6ef03359ba291b9e9b891f

LGTM