Clarify satisfaction connection of "K" and "c:"

[dgpv]

[sipa]

This may be a matter of semantics, but I'm not sure I agree with "K expressions cannot be satisfied or dissatisfied by themselves". Operationally, in terms of script execution, the checksig happens later. But as far as the miniscript specification is concerned, that doesn't matter, and you can think of the K expression doing the validation itself, and the c: wrapper just being a conversion to another type.

[dgpv]

you can think of the K expression doing the validation itself

Validation - yes, but I understand (dis)satisfaction as "outcome that has an effect on the overall spendability of the script" (if the script is not overcomplete). In that sense, if an expression itself does not result in something that influences the spendability, we cannot say that it is satisfied or not. If the wrapper is needed to determine spendability, then only wrapped expression can be (dis)satisfied, but not the bare expression.

My understanding might be incorrect, but this is what I got out of reading of the spec (particularly the "Correctness properties" that define the satisfiability for each of the basic type separately). For the "K" type this does not have clear definition, though, it seems like "delayed satisfiability": "signature is still required to satisfy the expression". I interpreted this as "as of itself, it is not satisfiable or dissatisfiable".

[sipa]

I admit the existing text is confusing, and this change is probably an improvement.

But part of the confusion is due to the fact that miniscript can be interpreted in two ways, and the document probably mixes them:

• In terms of the operational semantics of its corresponding Bitcoin Script.
• As an abstract independent language whose semantics are defined entirely by its satisfaction rules.

In the first interpretation, clearly "pk(A)" (which just pushes A on the stack) cannot be "dissatisfied" or "satisfied", it doesn't "do" anything. But in the second, if we treat Miniscript as its own language, it does - you can think of "pk(A)" as consuming a signature, and the "c:" as just a type modifier with no semantic effect. This is actually how the satisfier is implemented: when trying to sign for "c:pk(A)", it just recurses into the satisfier for "pk(A)" which constructs a signature with the specified key.

[dgpv]

The descriptions for "B", "V" and "W" describe (dis)satisfactions in terms of effects on the stack ("push" or "do not push" something on the stack). It is natural to expect that "K" type description would also hold the same principle of describing on therms of stack effects.

The "how the satisfier is implemented" might be seen as just that - an implementation detail. For example, pk(A) might construct a 'satisfaction obligation' that have to be realized with c: somewhere up the expression tree.

[dgpv]

pk(A) can still be thought of as consuming the signature. I think we can say that "K"-type expression cannot be (dis)satisfied by itself, but bears "satisfaction obligation". This obligation is converted into (dis)satisfaction when "K" is converted to "B". This way the operational and abstract-language semantics will not be out of sync, and the fact that the satisfier "satisfies" pk(A) rather than produces a closure with satisfaction action would be just an implementation detail.

[dgpv]

It is natural to expect that "K" type description would also hold the same principle of describing on therms of stack effects.

Can we maybe say that pk_k(A) and pk_h(A) can't be dissatisfied (only aborted for pk_h), and when satisfied, they leave a pubkey on the stack ?

This way we describe the operational semantics.

We can say that pk_k takes a signature as a parameter (and pk_h takes a sig and a pubkey), but it has to come through a c wrapper, which will also determine (dis)satisfaction of the whole wrapped expression (which might be a tree rather than single pk)

This way we describe the abstract semantics.

[dgpv]

I pushed an update that rephrases the text in accordance to my previous message.

[darosior]

I have no opinion on the changes but for what it's worth it confused me too when reading the satisfier and refering to the specs.

[ProofOfKeags]

I too just ran into this. I was reimplementing MiniScript in Haskell over here and couldn't square some of the stuff I was seeing.