379: Miniscript

[achow101]

No description provided.

[murchandamus]

Was wondering whether @sipa, @apoelstra, @sanket1729, @darosior might want to review this?

[apoelstra]

For the most part this looks great to me. In 3282c75:

• There is trailing whitespace on a couple of lines.
• The definition of "non-canonical" doesn't make sense to me (and I forget what the correct definition is supposed to be :) @sipa do you remember?)
• I think the Type system section (lowercase s) should be moved up and folded into the Type System section (uppercase s).

[sipa]

@apoelstra I think it's roughly right. Non-canonical (dis)satisfactions are ones that are valid by script semantics (and thus need to be taken into account when they're available to malleators, e.g.), but can be proven to never be used by the specified non-malleable satisfaction algorithm.

[achow101]

There is trailing whitespace on a couple of lines.

Fixed

I think the Type system section (lowercase s) should be moved up and folded into the Type System section (uppercase s).

This was a deliberate decision to split the discussion/reasoning/explanation of things away from the specification. The types are explained in the discussion section since an implementor does not need to understand what each type means in order to implement miniscript.

[apoelstra]

@sipa ok, rereading the text, I understand it now, but I think it's worded in a confusing way. The text says "are not necessary to produce correct witnesses", but the surrounding text is not about the satisfaction algorithm and it's not clear who they're "not necessary" to. My read of it was that they weren't necessary to the spec, in which case, why are they listed, and why aren't they necessary.

I think the text in your comment (they are provably unused by the satisfaction algorithm but they are legal according to consensus rules and available to malleators) is much better.

This was a deliberate decision to split the discussion/reasoning/explanation of things away from the specification. The types are explained in the discussion section since an implementor does not need to understand what each type means in order to implement miniscript.

Ok, yeah, that's reasonable. I rescind my request then.

[apoelstra]

ACK d2f8b25 except that I'd still like the first occurrence of "non-canonical" to be changed to have a clearer definition.

[achow101]

I'd still like the first occurrence of "non-canonical" to be changed to have a clearer definition.

Suggest some words please?

[apoelstra]

Some options are not actually necessary to produce correct witnesses, and are called non-canonical options.

should be

Some options are inefficient and provably unnecessary to the satisfaction algorithm described below, but are valid according to Script rules and could be used by a malleator or other non-standard actor. These are called non-canonical options, and are listed for completeness...

[apoelstra]

ACK da4ca97

[sipa]

A few quick comments.

[sipa]

The typing rules for timelock mixing don't seem to be included here.

[achow101]

Hmm, it seems like representing them in the table might be complicated since it depends on the arguments to the older and after fragments.

[sanket1729]

How about adding as a small description as suggested here?

[apoelstra]

ACK c868e9e other than the locktime rule.

I think that, after the correctness table, we should add some text like:

"Additionally there is one global correctness rule: every older fragment within a Miniscript fragment must make the same choice of height- or time-based timelocks. Similarly, every after fragment must make the same choice of height- or time-based timelocks. (It is permissible for the older fragments to differ from the after fragments.)"

I think it makes sense for this to appear outside of the table because all the rules in the table are local, in the sense that once you see a fragmet you know whether it's legal or not. Vs this thing which is a global rule that breaks composability.

Maybe we should recommend people always use height-based timelocks to avoid running afoul of this rule?

[sipa]

@apoelstra That's too strong, I think. It is only groups that get anded/threshed together that cannot conflict in their height vs time constraints. Pure disjunctions can make distinct choices. In that sense it is not a global constraint, but a local one just like the other type properties.

[apoelstra]

Ah, yes, you're right. It's a local constraint on the conjunctions and thresholds I guess.

[sanket1729]

@achow101 @murchandamus I have this on my review list for this weekend.

[sanket1729]

I think it makes sense for this to appear outside of the table because all the rules in the table are local, in the sense that once you see a fragmet you know whether it's legal or not. Vs this thing which is a global rule that breaks composability.

I think adding 5 new type properties in the table will pollute(add too many things in the row) the existing properties and confuse people. For the sake of completeness, we can write a description of how "k" property is computed and link to the source c++ code for details.

How about adding a line after the table:

Property 'k' is determined as follows: Each leaf node inherently possesses property 'k'. A parent node will not have property 'k' if any of its children lack this property. Furthermore, in scenarios involving thresholds (k ≥ 2) or conjunctions, property 'k'—which indicates no-timelock mixing—is absent if the node contains two or more children that require different types of timelock conditions for their satisfaction.

[achow101]

I think adding 5 new type properties in the table will pollute(add too many things in the row) the existing properties and confuse people. For the sake of completeness, we can write a description of how "k" property is computed and link to the source c++ code for details.

I agree

How about adding a line after the table:

Property 'k' is determined as follows: Each leaf node inherently possesses property 'k'. A parent node will not have property 'k' if any of its children lack this property. Furthermore, in scenarios involving thresholds (k ≥ 2) or conjunctions, property 'k'—which indicates no-timelock mixing—is absent if the node contains two or more children that require different types of timelock conditions for their satisfaction.

I've added a line similar to this, with slightly different wording.

[apoelstra]

For parent nodes with multiple children (thresholds and conjunctions),

should be changed to Sanket's original For thresholds with k >= 2 and conjunctions,. The existing wording is confusing because it's not obvious what the rule for disjunctions or k=1 thresholds are.

[achow101]

should be changed to Sanket's original For thresholds with k >= 2 and conjunctions,. The existing wording is confusing because it's not obvious what the rule for disjunctions or k=1 thresholds are.

I find it confusing that the type is k, but for thresholds, we're also going to mentioning a k that means something completely different.

---

Updated the sentence.

[sipa]

If we're not going to include "k" as a property in the tables, then I don't think it needs a letter. It can just be described.

It's not the only type property that doesn't have a letter: "validity" and "nonmalleability" also fall in that category.

[achow101]

I've removed the k property and wrote a subsection that describes the timelock mixing constraints. The wording is a little bit awkward though.

[apoelstra]

I would suggest this wording:

"

Timelock Type Mixing

There is one additional correctness property that Miniscript programs must satisfy: the four timelock types (absolute time-based, absolute height-based, relative time-based and relative height-based) must not be mixed in an incompatible way. Specifically, within the and combinator and the thresh combinator where k >= 2, it is illegal for both absolute height-based and time-based locktimes to appear, or for both relative height-based and time-based locktimes to appear.

Outside of these combinators, it is legal to mix height-based and time-based timelocks, and it is always legal to mix absolute and relative timelocks (even if one is height-based and the other is time-based).
"

I think trying to split height/time and absolute/relative into "types" and "categories" is too hard to describe clearly and that it's easier to exhaustively list all four possibilities and how the can be mixed.

[sipa]

In the Bitcoin Core implementation malleability and timelock mixing (as well as resource limit checks) are not part of "validity", but of "sanity". The distinction being that valid-but-insane miniscripts can be parsed, and the satisfaction algorithm can be run for it, and if it succeeds the result can be a valid transaction. Sanity additionally guarantees that the resulting policy of the actually emitted script will match the apparent policy. The idea is that when designing scripts you probably only want sane ones, but if somehow you're confronted with an insane but valid one after the fact (e.g., it already holds funds), the code shouldn't fail at the parsing stage preventing you from attempting to sign it anyway.

Do we want to make that distinction clear in the BIP?

[apoelstra]

Similar in rust-miniscript -- though we've generalized things a bit so that the caller can (if they want to use the annoying form of the API) individually toggle all of the "sanity" checks. The exact definition of "sane" feels ad-hoc and hard to remember and usually I need to check the source code of the default rust-miniscript parser to see which flags it has set/unset.

IMHO we shouldn't bother making this distinction in the BIP, and just consider insane parsers to be "extensions" or nonstandard. Though maybe we could add a sentence saying it's possible to do this.

[sipa]

@apoelstra I'm not sure. The sanity checks are arguably more complicated (or at least similarly complicated) to all the validity checks combined. If we want to only treat sane scripts as BIP-valid-miniscript, then I think it should be fully specified in the BIP (including e.g. stack limit analysis).

[achow101]

it is legal to mix height-based and time-based timelocks

I presume you meant to say illegal?

Nvm, misunderstood that sentence

[achow101]

Updated the timelock mixing text

[jonatack]

Looks like this needs a BIP assignment.

A few optional minor suggestions follow.

BIP 388 contains many references to Miniscript and may need verification of cross-references and updating.

[jonatack]

Assigned BIP 379.

[achow101]

BIP 388 contains many references to Miniscript and may need verification of cross-references and updating.

I'll let @bigspider do that in a separate pr.

[apoelstra]

ACK 4b321d7

@sipa yeah, agreed. It does seem like the sanity checks are a big deal and should be specified. I don't know if they belong here (though it is weird that we have included timelock mixing and put it under "correctness" but not included any other discussion of sanity).

On the other hand, because of the complexity and lack of written specification of the sanity rules (and also I'm not thrilled with the names "sane"/"insane" which were kinda funny when we came up with them, but are awkward to use because "insane" has the wrong connotations when we really mean something like "contains branches that are not verified to be sane"), I don't want to hold up this PR/BIP for it. Nor do I want to have a big discussion on Github which really sucks for long discussions.

I wonder if we should accept this BIP as-is and then move to the ML to propose an extension to it (which would be strictly additive and could be folded into the same BIP) for the sanity rules.

The only question is what to do with the current timelock-mixing text, which IMHO looks good to me other than possibly it shouldn't be labelled "correctness".

[jonatack]

Format looks complete. @sipa @darosior @sanket1729 sign-off?

[jonatack]

Rebased for #1540 and merged manually.