Sematics of "andor" differs from expected by the reader (no mention that it is satisfaction-dependent)

[dgpv]

miniscript/index.html

Lines 251 to 255 in 027b422

	<tr>
	<td>(<em>X</em> and <em>Y</em>) or <em>Z</em></td>
	<td><code>andor(<em>X</em>,<em>Y</em>,<em>Z</em>)</code></td>
	<td><samp><em>[X]</em> NOTIF <em>[Z]</em> ELSE <em>[Y]</em> ENDIF</samp></td>
	</tr>

For andor(X,Y,Z) the semantics is listed as (X and Y) or Z, while the code [X] NOTIF [Z] ELSE [Y] ENDIF when applied to the truth table for the three variables does not correspond to the truth table that results from (X and Y) or Z expression.

This can be shown with the following script (using python-bitcoinlib):

from bitcoin.core import *
from bitcoin.core.script import *
from bitcoin.core.scripteval import *

print(f'X Y Z | E A')
print(f'-----------')
for X in (0, 1):
    for Y in (0, 1):
        for Z in (0, 1):
            script = CScript([X, OP_NOTIF, Z, OP_ELSE, Y, OP_ENDIF])
            stack=[]
            EvalScript(stack, script, CTransaction(), 0)

            expected = (X and Y) or Z
            actual = int(bool(stack[0]))

            print(f'{X} {Y} {Z} | {expected} {actual}')

the output:

X Y Z | E A
-----------
0 0 0 | 0 0
0 0 1 | 1 1
0 1 0 | 0 0
0 1 1 | 1 1
1 0 0 | 0 0
1 0 1 | 1 0
1 1 0 | 1 1
1 1 1 | 1 1

We can see that for X=1 Y=0 Z=1 the result of (X and Y) or Z does not correspond to the result of evaluating the script.

Either the logical expression in the 'Semantics' column has to be (X or Z) and ((not X) or Y), or the script in the Bitcoin script column has to be changed to have the semantics of (X and Y) or Z

[sipa]

The semantics aren't an exact representation of the script execution; they encode the conditions under which a script can be satisfied.

Say your script is andor(c:A,c:B:c:C) = <A> CHECKSIG NOTIF <C> CHECKSIG ELSE <B> CHECKSIG ENDIF. If the signer(s) have access to the private key of C, they can produce a satisfying witness <sigC> 0. Sure, if they also had access to the private key of A then they could produce a non-satisfying witness 0 <sigA>, but why would they?

Note that the X argument needs to have property d (dissatisfiable); otherwise it may not be possible to force the Z expression to be evaluated, as your example shows (1 does not have the d property).

[dgpv]

I think this should be a footnote or some other clarification in the text so the readers would not be confused.
I wasn't able to come up with good text (not overly long) for such a note at the moment, though. Maybe will get an idea after more reading.

[dgpv]

Would this sentence be correct?

It might be possible to construct a witness such that the script execution will not match the listed semantics; the execution in this case will always result in dissatisfaction, and the spender will always be able to produce a different witness that will result in the execution with expected semantics

I'm not sure if it would be a good explanation text for the table, though, it sounds difficult to process mentally.

[dgpv]

Maybe just add a note

Semantics are defined for canonical satisfaction/dissatisfaction options, and may not be valid for non-canonical options (see "Satisfaction and malleability", "Basic satisfactions" below)