Repository navigation
Sematics of "andor" differs from expected by the reader (no mention that it is satisfaction-dependent) #42
Description
Lines 251 to 255 in 027b422
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
Reacted by James
Activity
sipa commentedon Nov 1, 2020
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 ofC, they can produce a satisfying witness<sigC> 0. Sure, if they also had access to the private key ofAthen they could produce a non-satisfying witness0 <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 (1does not have thedproperty).[-]Sematics of "andor" specified in the Translation table does not correspond to actual script behavior [/-][+]Sematics of "andor" differs from expected by the reader (no mention that it is satisfaction-dependent)[/+]dgpv commentedon Nov 1, 2020
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 commentedon Nov 2, 2020
Would this sentence be correct?
I'm not sure if it would be a good explanation text for the table, though, it sounds difficult to process mentally.
dgpv commentedon Nov 3, 2020
Maybe just add a note
Add note: Semantics defined only for canonical sat/dsat
Add note: Semantics defined only for canonical sat/dsat
Add note: Semantics defined only for canonical sat/dsat