You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

950 lines
42 KiB

5 years ago
<!DOCTYPE html>
<html lang="en">
<head>
<!-- Required meta tags -->
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
<title>Miniscript</title>
<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/4.0.0-alpha.6/css/bootstrap.min.css" integrity="sha384-rwoIResjU2yc3z8GV/NPeZWAv56rSmLldC3R/AZzGRnGxQQKnKkoFVhFQhNUwEyJ" crossorigin="anonymous">
<!-- Optional theme -->
<link rel="stylesheet" href="style.css">
<style>
.monospace {
font-family: Consolas,Monaco,Lucida Console,Liberation Mono,DejaVu Sans Mono,Bitstream Vera Sans Mono,Courier New, monospace;
}
a.demo_link {
text-decoration-style: dashed;
text-underline-position: under;
}
</style>
</head>
<body>
<script src="miniscript.js"></script>
<script>
em_miniscript_compile = Module.cwrap('miniscript_compile', 'none', ['string', 'number', 'number', 'number', 'number']);
em_miniscript_analyze = Module.cwrap('miniscript_analyze', 'none', ['string', 'number', 'number']);
function miniscript_compile() {
document.getElementById("descout").value = "Compiling...";
document.getElementById("spendout").innerHTML = "Compiling...";
window.setTimeout(function() {
src = document.getElementById("source").value;
var descout = Module._malloc(1000);
var spendout = Module._malloc(50000);
em_miniscript_compile(src, descout, 1000, spendout, 50000);
document.getElementById("descout").value = Module.UTF8ToString(descout);
document.getElementById("spendout").innerHTML = Module.UTF8ToString(spendout);
Module._free(descout)
Module._free(spendout)
});
}
function miniscript_analyze() {
document.getElementById("spendout").innerHTML = "Analyzing...";
window.setTimeout(function() {
src = document.getElementById("descout").value;
var spendout = Module._malloc(50000);
em_miniscript_analyze(src, spendout, 50000);
document.getElementById("spendout").innerHTML = Module.UTF8ToString(spendout);
Module._free(spendout)
});
}
</script>
<div class="container" style="margin-top:50px">
<div class="card mb-3 text-left">
5 years ago
<h3 class="card-header">Introduction</h3>
5 years ago
<div class="card-block">
<p>
5 years ago
<em>Miniscript</em> is a language for writing (a subset of) Bitcoin Scripts in a structured way, enabling analysis, composition, generic signing and more.
5 years ago
</p>
5 years ago
<p>
Bitcoin Script is an unusual stack-based language with many edge cases, designed for implementing spending conditions consisting of various combinations of
signatures, hash locks, and time locks. Yet despite being limited in functionality it is still highly nontrivial to:<ul>
5 years ago
<li>Given a combination of spending conditions, finding the most economical script to implement it.</li>
5 years ago
<li>Given a two scripts, construct a script that implements a composition of their spending conditions (e.g. a multisig where one of the "keys" is another multisig).</li>
5 years ago
<li>Given a script, find out what spending conditions it permits.</li>
<li>Given a script and access to a sufficient set of private keys, construct a general satisfying witness for it.</li>
<li>Given a script, be able to predict the cost of spending an output.</li>
<li>Given a script, know whether any code path requires violating particular resource limitations like the ops limit.</li>
5 years ago
</ul>
</p>
<p>
Miniscript functions as a representation for scripts that makes these sort of operations possible. It has a structure that allows composition. It is very easy to
statically analyze for various properties (spending conditions, correctness, security properties, malleability, ...). It can be targeted by spending policy compilers
(see further). Finally, compatible scripts easily can be converted to miniscript - avoiding the need for additional metadata for e.g. signing devices that support it.
</p>
5 years ago
<p>
For now, Miniscript is really only designed for P2WSH and P2SH-P2WSH embedded scripts. Most of its constructions works fine in P2SH as well, but some of the (optional) security properties
rely on Segwit-specific rules. Furthermore, the implemented policy compilers assume a Segwit-specific cost model.
5 years ago
</p>
5 years ago
</div>
</div>
<div class="card mb-3 text-left">
<h3 class="card-header">Miniscript reference</h3>
<div class="card-block">
5 years ago
<h4>Translation table</h4>
<p>
This table shows all Miniscript <em>fragments</em> and their associated semantics and Bitcoin Script.
Fragments that do not change the semantics of their subexpressions are called <em>wrappers</em>. Normal fragments use
a "fragment(arguments,...)" notation, while wrappers are written using prefixes separated from other fragments
by a colon. The colon is dropped between subsequent wrappers; e.g. <code>vc:pk(key)</code> is the <code>v:</code>
wrapper applied to the <code>c:</code> wrapper applied to the <code>pk</code> fragment for a given key.
5 years ago
<table class="table table-sm">
<thead class="thead-light">
5 years ago
<tr><th scope="col">Semantics</th><th scope="col">Miniscript fragment</th><th scope="col">Bitcoin Script</th></tr></thead>
5 years ago
<tbody>
<tr>
<td>true</td>
5 years ago
<td><code>1</code></td>
<td><samp>OP_1</samp></td>
5 years ago
</tr>
<tr>
<td>false</td>
5 years ago
<td><code>0</code></td>
<td><samp>OP_0</samp></td>
5 years ago
</tr>
<tr>
<td rowspan="2">check(key)</td>
5 years ago
<td><code>pk(key)</code></td>
<td><samp>&lt;key&gt;</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>pk_h(key)</code></td>
<td><samp>OP_DUP OP_HASH160 &lt;HASH160(key)&gt; OP_EQUALVERFIFY</samp></td>
5 years ago
</tr>
<tr>
<td>nSequence &ge; n (and compatible)</td>
5 years ago
<td><code>older(n)</code></td>
<td><samp>&lt;n&gt; OP_CHECKSEQUENCEVERIFY</samp></td>
5 years ago
</tr>
<tr>
<td>nLockTime &ge; n (and compaitlbe)</td>
5 years ago
<td><code>after(n)</code></td>
<td><samp>&lt;n&gt; OP_CHECKLOCKTIMEVERIFY</samp></td>
5 years ago
</tr>
<tr>
<td>len(x) = 32 and SHA256(x) = h</td>
5 years ago
<td><code>sha256(h)</code></td>
<td><samp>OP_SIZE &lt;32&gt; OP_EQUALVERIFY OP_SHA256 &lt;h&gt; OP_EQUAL</samp></td>
5 years ago
</tr>
<tr>
<td>len(x) = 32 and HASH256(x) = h</td>
5 years ago
<td><code>hash256(h)</code></td>
<td><samp>OP_SIZE &lt;32&gt; OP_EQUALVERIFY OP_HASH256 &lt;h&gt; OP_EQUAL</samp></td>
5 years ago
</tr>
<tr>
<td>len(x) = 32 and RIPEMD160(x) = h</td>
5 years ago
<td><code>ripemd160(h)</code></td>
<td><samp>OP_SIZE &lt;32&gt; OP_EQUALVERIFY OP_RIPEMD160 &lt;h&gt; OP_EQUAL</samp></td>
5 years ago
</tr>
<tr>
<td>len(x) = 32 and HASH160(x) = h</td>
5 years ago
<td><code>hash160(h)</code></td>
<td><samp>OP_SIZE &lt;32&gt; OP_EQUALVERIFY OP_HASH160 &lt;h&gt; OP_EQUAL</samp></td>
5 years ago
<tr>
5 years ago
<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> OP_NOTIF <em>[Z]</em> OP_ELSE <em>[Y]</em> OP_ENDIF</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td rowspan="3"><em>X</em> and <em>Y</em></td>
<td><code>and_v(<em>X</em>,<em>Y</em>)</code></td>
<td><samp><em>[X]</em> <em>[Y]</em></samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>and_b(<em>X</em>,<em>Y</em>)</code></td>
<td><samp><em>[X]</em> <em>[Y]</em> OP_BOOLAND</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>and_n(<em>X</em>,<em>Y</em>)</code> = <code>andor(<em>X</em>,<em>Y</em>,0)</code></td>
<td><samp><em>[X]</em> OP_NOTIF OP_0 OP_ELSE <em>[Y]</em> OP_ENDIF</samp></td>
5 years ago
</tr>
<tr>
<td rowspan="4"><em>X</em> or <em>Z</em></td>
5 years ago
<td><code>or_b(<em>X</em>,<em>Z</em>)</code></td>
<td><samp><em>[X]</em> <em>[Z]</em> OP_BOOLOR</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>or_d(<em>X</em>,<em>Z</em>)</code></td>
<td><samp><em>[X]</em> OP_IFDUP OP_NOTIF <em>[Z]</em> OP_ENDIF</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>or_c(<em>X</em>,<em>Z</em>)</code></td>
<td><samp><em>[X]</em> OP_NOTIF <em>[Z]</em> OP_ENDIF</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>or_i(<em>X</em>,<em>Z</em>)</code></td>
<td><samp>OP_IF <em>[X]</em> OP_ELSE <em>[Z]</em> OP_ENDIF</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><em>X<sub>1</sub></em> + ... + <em>X<sub>n</sub></em> = k</td>
<td><code>thresh(k,<em>X<sub>1</sub></em>,...,<em>X<sub>n</sub></em>)</code></td>
<td><samp><em>[X<sub>1</sub>]</em> <em>[X<sub>2</sub>]</em> OP_ADD ... <em>[X<sub>n</sub>]</em> OP_ADD ... &lt;k&gt; OP_EQUAL</samp></td>
5 years ago
</tr>
<tr>
<td>check(key<sub>1</sub>) + ... + check(key<sub>n</sub>) = k</td>
5 years ago
<td><code>thresh_m(k,key<sub>1</sub>,...,key<sub>n</sub>)</code></td>
<td><samp>&lt;k&gt; &lt;key<sub>1</sub>&gt; ... &lt;key<sub>n</sub>&gt; &lt;n&gt; OP_CHECKMULTISIG</samp></td>
5 years ago
</tr>
<tr>
<td rowspan="10"><em>X</em> (identities)</td>
5 years ago
<td><code>a:<em>X</em></code></td>
<td><samp>OP_TOALTSTACK <em>[X]</em> OP_FROMALTSTACK</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>s:<em>X</em></code></td>
<td><samp>OP_SWAP <em>[X]</em></samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>c:<em>X</em></code></td>
<td><samp><em>[X]</em> OP_CHECKSIG</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>t:<em>X</em></code> = <code>and_v(<em>X</em>,1)</code></td>
<td><samp><em>[X]</em> OP_1</samp></td>
5 years ago
<tr>
5 years ago
<td><code>d:<em>X</em></code></td>
<td><samp>OP_DUP OP_IF <em>[X]</em> OP_ENDIF</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>v:<em>X</em></code></td>
<td><samp><em>[X]</em> OP_VERIFY</samp> (or <samp>VERIFY</samp> version of last opcode in <samp><em>[X]</em></samp>)</td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>j:<em>X</em></code></td>
<td><samp>OP_SIZE OP_0NOTEQUAL OP_IF <em>[X]</em> OP_ENDIF</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>n:<em>X</em></code></td>
<td><samp><em>[X]</em> OP_0NOTEQUAL</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>l:<em>X</em></code> = <code>or_i(0,<em>X</em>)</code></td>
<td><samp>OP_IF OP_0 OP_ELSE <em>[X]</em> OP_ENDIF</samp></td>
5 years ago
</tr>
<tr>
5 years ago
<td><code>u:<em>X</em></code> = <code>or_i(<em>X</em>,0)</code></td>
<td><samp>OP_IF <em>[X]</em> OP_ELSE 0 OP_ENDIF</samp></td>
5 years ago
</tr>
</tbody>
</table>
The <code>and_n</code> fragment and <code>t:</code>, <code>l:</code>, and <code>u:</code> wrappers are syntactic sugar for other Miniscripts, as listed in the table above.
In what follows, they will not be included anymore, as their properties can be derived by looking at their expansion.
5 years ago
</p>
5 years ago
<h4>Correctness properties</h4>
<p>
Not every Miniscript expression can be composed with every other. Some return their result by putting zero or false on the stack; others distinguish by aborting or continuing.
Some require subexpressions that consume an exactly known number of arguments, while others need a subexpression that has a nonzero top stack element to satisfy. To model all
these properties, we define a correctness type system for Miniscript.
</p>
<p>
Every miniscript expression has one of four basic types:<ul>
<li><b>"B"</b> Base expressions:<ul>
<li>Takes its inputs from the top of the stack.</li>
<li>When satisfied, pushes a nonzero value of up to 4 bytes onto the stack.</li>
<li>When dissatisfied, pushes a 0 onto the stack.</li>
<li>This is used for most expressions, and required for the top level one.</li>
5 years ago
<li>For example: <code>older(n)</code> = <samp>&lt;n&gt; OP_CHECKSEQUENCEVERIFY</samp>.</li>
5 years ago
</ul></li>
<li><b>"V"</b> Verify expressions:<ul>
<li>Takes its inputs from the top of the stack.</li>
<li>When satisfactied, pushes nothing.</li>
<li>Cannot be dissatisfied (aborts execution instead).</li>
5 years ago
<li>A "V" can be obtained using the <code>v:</code> wrapper on a "B" expression, or by combining other "V" expressions using <code>and_v</code>, <code>or_i</code>, <code>or_c</code>, or <code>andor</code>.</li>
5 years ago
<li>For example <code>vc:pk(key)</code> = <samp>&lt;key&gt; OP_CHECKSIGVERIFY</samp>.</li>
5 years ago
</ul></li>
<li><b>"K"</b> Key expressions:<ul>
<li>Takes its inputs from the top of the stack.</li>
<li>Always pushes a public key onto the stack, for which a signature is to be provided to satisfy the expression.</li>
5 years ago
<li>Can be converted into a "B" using the <code>c:</code> wrapper (<samp>OP_CHECKSIG</samp>).</li>
5 years ago
<li>For example <code>pk_h(key)</code> = <samp>OP_DUP OP_HASH160 &lt;Hash160(key)&gt; OP_EQUALVERIFY</samp></li>
5 years ago
</ul></li>
<li><b>"W"</b> Wrapped expressions:<ul>
<li>Takes its input from one below the top of the stack.</li>
<li>When satisfied, pushes a nonzero value (like B) on top of the stack, or one below the top.</li>
<li>When dissatisfied, pushes 0 op top of the stack or one below the top.</li>
5 years ago
<li>Every "W" is either <code>s:B</code> (<samp>OP_SWAP B</samp>) or <code>a:B</code> (<samp>OP_TOALTSTACK B OP_FROMALTSTACK</code>).</li>
5 years ago
<li>For example <code>sc:pk(key)</code> = <samp>OP_SWAP &lt;key&gt; OP_CHECKSIG</samp>.</li>
5 years ago
</ul></li>
</ul>
</p>
<p>
Then there are 5 type modifiers, which guarantee additional properties:<ul>
<li><b>"z"</b> Zero-arg: this expression always consumes exactly 0 stack elements.</li>
<li><b>"o"</b> One-arg: this expression always consumes exactly 1 stack element.</li>
<li><b>"n"</b> Nonzero: no satisfaction for this expression requires a top stack element that is zero.</li>
<li><b>"d"</b> Dissatisfiable: this expression can be dissatisfied by anyone.</li>
<li><b>"u"</b> Unit: when satisfied, this expression will put an exact 1 on the stack (as opposed to any nonzero value).</li>
</ul>
</p>
<p>
This tables lists the correctness requirements for each of the Miniscript expressions, and its type properties in function of those of their subexpressions:
<table class="table table-sm">
<thead class="thead-light"><tr><th scope="col">Miniscript</th><th scope="col">Requires</th><th scope="col">Type</th><th scope="col">Properties</th></tr></thead>
<tbody>
5 years ago
<tr><td><code>0</code></td><td></td><td>B</td><td>z; u; d</td></tr>
<tr><td><code>1</code></td><td></td><td>B</td><td>z; u</td></tr>
<tr><td><code>pk(key)</code></td><td></td><td>K</td><td>o; n; d; u</td></tr>
<tr><td><code>pk_h(key)</code></td><td></td><td>K</td><td>n; d; u</td></tr>
<tr><td><code>older(n)</code>, <code>after(n)</code></td><td>1 &le; n &lt; 2<sup>31</sup></td><td>B</td><td>z</td></tr>
<tr><td><code>sha256(h)</code></td><td></td><td>B</td><td>o; n; d; u</td></tr>
<tr><td><code>ripemd160(h)</code></td><td></td><td>B</td><td>o; n; d; u</td></tr>
<tr><td><code>hash256(h)</code></td><td></td><td>B</td><td>o; n; d; u</td></tr>
<tr><td><code>hash160(h)</code></td><td></td><td>B</td><td>o; n; d; u</td></tr>
<tr><td><code>and_v(<em>X</em>,<em>Y</em>)</code></td><td><em>X</em> is V; <em>Y</em> is B, K, or V</td><td>same as <em>Y</em></td><td>z=z<sub>X</sub>z<sub>Y</sub>; o=z<sub>X</sub>o<sub>Y</sub> or z<sub>Y</sub>o<sub>X</sub>; n=n<sub>X</sub> or z<sub>X</sub>n<sub>Y</sub>; u=u<sub>Y</sub></td></tr>
<tr><td><code>and_b(<em>X</em>,<em>Y</em>)</code></td><td><em>X</em> is B; <em>Y</em> is W</td><td>B</td><td>z=z<sub>X</sub>z<sub>Y</sub>; o=z<sub>X</sub>o<sub>Y</sub> or z<sub>Y</sub>o<sub>X</sub>; n=n<sub>X</sub> or z<sub>X</sub>n<sub>Y</sub>; d=d<sub>X</sub>d<sub>Y</sub>; u</td></tr>
<tr><td><code>or_b(<em>X</em>,<em>Z</em>)</code></td><td><em>X</em> is Bd; <em>Z</em> is Wd</td><td>B</td><td>z=z<sub>X</sub>z<sub>Z</sub>; o=z<sub>X</sub>o<sub>Y</sub> or z<sub>Y</sub>o<sub>X</sub>; d; u</td></tr>
<tr><td><code>or_c(<em>X</em>,<em>Z</em>)</code></td><td><em>X</em> is Bdu; <em>Z</em> is V</td><td>V</td><td>z=z<sub>X</sub>z<sub>Z</sub>; o=o<sub>X</sub>z<sub>Z</sub></td></tr>
<tr><td><code>or_d(<em>X</em>,<em>Z</em>)</code></td><td><em>X</em> is Bdu; <em>Z</em> is B</td><td>B</td><td>z=z<sub>X</sub>z<sub>Z</sub>; o=o<sub>X</sub>z<sub>Z</sub>; d=d<sub>Z</sub>; u=u<sub>Z</sub></td></tr>
<tr><td><code>or_i(<em>X</em>,<em>Z</em>)</code></td><td>both are B, K, or V</td><td>same as X/Z</td><td>o=z<sub>X</sub>z<sub>Z</sub>; u=u<sub>X</sub>u<sub>Z</sub>; d=d<sub>X</sub> or d<sub>Z</sub></td></tr>
<tr><td><code>andor(<em>X</em>,<em>Y</em>,<em>Z</em>)</code></td><td><em>X</em> is Bdu; <em>Y</em> and <em>Z</em> are both B, K, or V</td><td>same as Y/Z</td><td>z=z<sub>X</sub>z<sub>Y</sub>z<sub>Z</sub>; o=z<sub>X</sub>o<sub>Y</sub>o<sub>Z</sub> or o<sub>X</sub>z<sub>Y</sub>z<sub>Z</sub>; u=u<sub>Y</sub>u<sub>Z</sub>; d=d<sub>Z</sub></td></tr>
<tr><td><code>thresh(k,<em>X<sub>1</sub><em>,...,<em>X<sub>n</sub></em>)</code></td><td>1 &lt; k &lt; n; <em>X<sub>1</sub></em> is Bdu; others are Wdu</td><td>B</td><td>z=all are z; o=all are z except one is o; d; u</td></tr>
<tr><td><code>thresh_m(k,key<sub>1</sub>,...,key<sub>n</sub>)</code></td><td>1 &le; k &le; n</td><td>B</td><td>n; d; u</td></tr>
<tr><td><code>a:X</code></td><td><em>X</em> is B</td><td>W</td><td>d=d<sub>X</sub>; u=u<sub>X</sub></td></tr>
<tr><td><code>s:X</code></td><td><em>X</em> is Bo</td><td>W</td><td>d=d<sub>X</sub>; u=u<sub>X</sub></td></tr>
<tr><td><code>c:X</code></td><td><em>X</em> is K</td><td>B</td><td>o=o<sub>X</sub>; n=n<sub>X</sub>; d=d<sub>X</sub>; u</td></tr>
<tr><td><code>d:X</code></td><td><em>X</em> is Vz</td><td>B</td><td>o=z<sub>X</sub>; n; u; d</td></tr>
<tr><td><code>v:X</code></td><td><em>X</em> is B</td><td>V</td><td>z=z<sub>X</sub>; o=o<sub>X</sub>; n=n<sub>X</sub></td></tr>
<tr><td><code>j:X</code></td><td><em>X</em> is Bn</td><td>B</td><td>o=o<sub>X</sub>; n; d; u=u<sub>X</sub></td></tr>
<tr><td><code>n:X</code></td><td><em>X</em> is B</td><td>B</td><td>z=z<sub>X</sub>; o=o<sub>X</sub>; n=n<sub>X</sub>; d=d<sub>X</sub>; u</td></tr>
5 years ago
</tbody>
</table>
</p>
<h4>Resource limitations</h4>
<p>
Various types of Bitcoin Scripts have different resource limitations, either through consensus or standardness. Some of them affect otherwise valid Miniscripts: <ul>
<li>Scripts over 10000 bytes are invalid by consensus (bare, P2SH, P2WSH, P2SH-P2WSH).</li>
<li>Scripts over 520 bytes are invalid by consensus (P2SH).</li>
<li>Script satisfactions where the total number of non-push opcodes plus the number of keys participating in all executed <code>thresh_m</code>s, is above 201, are invalid by consensus (bare, P2SH, P2WSH, P2SH-P2WSH).</li>
<li>Anything but <code>c:pk(key)</code> (P2PK), <code>c:pk_h(key)</code> (P2PKH), and <code>thresh_m(k,...)</code> up to n=3 is invalid by standardness (bare).</li>
<li>Scripts over 3600 bytes are invalid by standardness (P2WSH, P2SH-P2WSH).</li>
<li>Script satisfactions with a serialized <samp>scriptSig</samp> over 1650 bytes are invalid by standardness (P2SH).</li>
<li>Script satisfactions with a witness consisting of over 100 stack elements (excluding the script itself) are invalid by standardness (P2WSH, P2SH-P2WSH).</li>
</ul>
Miniscript makes it easy to verify these properties statically for all possible execution paths.
</p>
5 years ago
<h4>Security properties</h4>
<p>
The type system above guarantees that the corresponding Bitcoin Scripts are:<ul>
<li><b>consensus and standardness complete</b>: Assuming the resource limits listed in the previous section are not violated, for every way that the spending conditions associated with the Miniscript can be met, a witness can be constructed that passes Bitcoin's consensus rules and common standardness rules.</li>
<li><b>consensus sound</b>: It is not possible to construct a witness that is consensus valid for a Script unless the spending conditions are met. Since standardness rules permit only a subset of consensus-valid satisfactions (by definition), this property also implies <b>standardness soundness</b>.
</ul>
5 years ago
</p>
<p>
The completeness property has been extensively tested for P2WSH by verifying large numbers of random satisfactions for random Miniscript expressions against Bitcoin Core's consensus and standardness implementation.
5 years ago
<p>
<p>In order for these properties to not just apply to script, but to an entire transaction, it's important that the witness commits to all data relevant for verification. In practice
this means that scripts whose conditions can be met without any digital signature are insecure. For example, if an output can be spent by simply passing a certain <samp>nLockTime</samp>
(an <code>after(n)</code> fragment in Miniscript) but without any digital signatures, an attacker can modify the <samp>nLockTime</samp> field in the spending transaction.
</p>
5 years ago
</div>
</div>
<div class="card mb-3 text-left">
<h3 class="card-header">Satisfactions and malleability</h3>
<div class="card-block">
<h4>Basic satisfactions</h4>
<p>
The following table shows how to construct valid satisfactions and dissatisfactions for every Miniscript, using satisfactions and dissatisfactions of its subexpressions.
<table class="table table-sm">
<thead class="thead-light"><tr><th scope="col">Miniscript</th><th scope="col">Dissatisfaction (dsat)</th><th scope="col" colspan="2">Satisfaction (sat)</th></thead>
<tbody>
<tr><td><code>0</code></td><td></td><td colspan="2">-</td></tr>
<tr><td><code>1</code></td><td>-</td><td colspan="2"></td></tr>
<tr><td><code>pk(key)</code></td><td>0</td><td colspan="2">sig</td></tr>
<tr><td><code>pk_h(key)</code></td><td>0</td><td colspan="2">sig key</td></tr>
<tr><td><code>older(n)</code></td><td>-</td><td colspan="2"></td></tr>
<tr><td><code>after(n)</code></td><td>-</td><td colspan="2"></td></tr>
<tr><td><code>sha256(h)</code></td><td>any 32-byte vector</td><td colspan="2">preimage</td></tr>
<tr><td><code>ripemd160(h)</code></td><td>any 32-byte vector</td><td colspan="2">preimage</td></tr>
<tr><td><code>hash256(h)</code></td><td>any 32-byte vector</td><td colspan="2">preimage</td></tr>
<tr><td><code>hash160(h)</code></td><td>any 32-byte vector</td><td colspan="2">preimage</td></tr>
<tr><td><code>thresh_m(k,key<sub>1</sub>,...,key<sub>n</sub>)</code></td><td>0 0 ... 0 (n+1 times)</td><td colspan="2">0 sig ... sig</td></tr>
<tr><td><code>a:<em>X</em></code></td><td>dsat(<em>X</em>)</td><td colspan="2">sat(<em>X</em>)</td></tr>
<tr><td><code>s:<em>X</em></code></td><td>dsat(<em>X</em>)</td><td colspan="2">sat(<em>X</em>)</td></tr>
<tr><td><code>c:<em>X</em></code></td><td>dsat(<em>X</em>)</td><td colspan="2">sat(<em>X</em>)</td></tr>
<tr><td><code>n:<em>X</em></code></td><td>dsat(<em>X</em>)</td><td colspan="2">sat(<em>X</em>)</td></tr>
<tr><td><code>v:<em>X</em></code></td><td>-</td><td colspan="2">sat(<em>X</em>)</td></tr>
<tr><td><code>d:<em>X</em></code></td><td>0</td><td colspan="2">sat(<em>X</em>) 1</td></tr>
<tr><td><code>j:<em>X</em></code></td><td>0</td><td colspan="2">sat(<em>X</em>)</td></tr>
<tr><td><code>and_v(<em>X</em>,<em>Y</em>)</code></td><td>-</td><td colspan="2">sat(<em>Y</em>) sat(<em>X</em>)</td></tr>
<tr><td><code>and_b(<em>X</em>,<em>Y</em>)</code></td><td>dsat(<em>Y</em>) dsat(<em>X</em>)</td><td colspan="2">sat(<em>Y</em>) sat(<em>X</em>)</td></tr>
<tr><td><code>thresh(k,<em>X<sub>1</sub></em>,...,<em>X<sub>n</sub></em>)</code></td><td>dsat(<em>X<sub>n</sub></em>) ... dsat(<em>X<sub>1</sub></em>)</td><td colspan="2">[d]sat(<em>X<sub>n</sub></em>) ... [d]sat(<em>X<sub>1</sub></em>) (with k sats and n-k dsats)</td></tr>
<thead class="thead-light"><tr><th scope="col"></th><th scope="col"></th><th scope="col">Left</th><th scope="col">Right</th></tr>
<tr><td><code>or_b(<em>X</em>,<em>Z</em>)</code></td><td>dsat(<em>Z</em>) dsat(<em>X</em>)</td><td>dsat(<em>Z</em>) sat(<em>X</em>)</td><td>sat(<em>Z</em>) dsat(<em>X</em>)</td></tr>
<tr><td><code>or_c(<em>X</em>,<em>Z</em>)</code></td><td>-</td><td>sat(<em>X</em>)</td><td>sat(<em>Z</em>) dsat(<em>X</em>)</td></tr>
<tr><td><code>or_d(<em>X</em>,<em>Z</em>)</code></td><td>dsat(<em>Z</em>) dsat(<em>X</em>)</td><td>sat(<em>X</em>)</td><td>sat(<em>Z</em>) dsat(<em>X</em>)</td></tr>
<tr><td><code>or_i(<em>X</em>,<em>Z</em>)</code></td><td>dsat(<em>X</em>) 1 or dsat(<em>Z</em>) 0</td><td>sat(<em>X</em>) 1</td><td>sat(<em>Z</em>) 0</td></tr>
<tr><td><code>andor(<em>X</em>,<em>Y</em>,<em>Z</em>)</code></td><td>dsat(<em>Z</em>) dsat(<em>X</em>)</td><td>sat(<em>Y</em>) sat(<em>X</em>)</td><td>sat(<em>Z</em>) dsat(<em>X</em>)</td></tr>
</tbody>
</table>
</p>
<h4>Malleability</h4>
<p>
While following the table above to construct satisfactions is sufficient for meeting the completeness and soundness properties, it does not guarantee non-malleability.
</p>
<p>
Malleability is the ability for a third party (<em>not</em> a participant in the script) to modify an existing satisfaction into another valid satisfaction.
Since Segwit, malleating a transaction no longer breaks the validity of unconfirmed descendant transactions. However, unintentional malleability may still have a number of
much weaker undesirable effects. If a witness can be stuffed with additional data, the transaction's feerate will go down, potentially to the point where its ability to
propagate and get confirmed is impacted. Additionally, malleability can be exploited to add roundtrips to BIP152 block propagation, by trying to get different miners to mine different versions
of the same transaction.
</p>
<p>
Because of these reasons, Miniscript is actually designed to permit non-malleable signing. As this guarantee is restricted in nob-obvious ways, let's first state the assumptions:<ul>
<li>The attacker does not have access to any of the private keys of public keys that participate in the Script. Limiting the impact a rogue participant can have is a distinct attack model.</li>
<li>The attacker gets to see exactly one satisfying witness of the script. If he sees multiple, the protections defined here are not necessarily valid anymore.</li>
<li>No public keys appear more than once in the script.</li>
<li>We want something that works even when the attacker has access to all the hash preimages the honest participants have access to (even if the honest participants choose a satisfaction that does not reveal that preimage).</li>
</lu>
</p>
<p>
Several ways to introduce malleability under the assumptions above exist:<ul>
<li>Dissatisfactions for <code>sha256(h)</code> and other hash locks are always malleable, as any 32-byte input suffices. An attacker can modify any such dissatisfaction into another one. Because of this, inside a non-malleable satisfaction, a hash lock can never be directly dissatisfied. Instead if must be protected by an <samp>OP_IF</samp> (e.g. <code>u:</code>) that skip execution of the hash lock check entirely when its satsifaction is not required.</li>
<li>For certain conjunctions (<code>and_b</code>, <code>andor</code>, and <code>thresh</code>) a dissatisfaction could be constructed that involves subexpressions that are actually satisfied. To prevent this, we must require that satisfying those subexpressions requires a digital signature. In that case, a malleability attacker cannot construct a satisfaction as we assume he has no access to private keys.</li>
<li>For <code>or_i</code> two possible ways for dissatisfying the expression exist: one involving the left subexpression and one involving the right one. To prevent the dissatisfaction from being malleable, we must make sure that at most one of the two is dissatisfiable.</code>
<li>For disjunctions (<code>or_*</code>, <code>andor</code>, and <code>thresh</code>) multiple ways of satisfaction exist. We must prevent malleability attackers from changing a satsifaction from one branch to another. Whenever a satisfaction exists for an expression that does not involve any signatures, we must take it. Otherwise the attacker could change the satisfaction to the non-signature requiring one. Whenever multiple ways exist that all require no signature, the result is inevitably malleable.</li>
</ul>
</p>
</div>
</div>
5 years ago
<div class="card mb-3 text-left">
<h3 class="card-header">Compiler demo</h3>
<div class="card-block">
<textarea rows="1" cols="100" id="source">
and(pk(C),or(pk(C),or(9@pk(C),older(1000))))
</textarea><br/>
<button type="button" onclick="miniscript_compile();">Compile</button>
Supported elements:
<ul>
<li><b>pk(HEX)</b>: Require public key HEX to sign.</li>
<li><b>time(NUMBER)</b>: Require that a relative time NUMBER has passed since creating the output.</li>
<li><b>hash(HEX)</b>: Require that the SHA256 preimage of HEX is revealed.</li>
<li><b>and(EXPR,EXPR)</b>: Require that both subexpressions are satisfied.</li>
<li><b>or([N@]EXPR,[N@]EXPR)</b>: Require that one of the subexpressions is satisfied. The numbers N indicate the relative probability of each of the subexpressions.</li>
<li><b>thresh(NUM,EXPR,EXPR,...)</b>: Require that NUM out of the following subexpressions are satisfied.</li>
</ul>
Shorthands:
<ul>
<li><b>C</b>: A dummy compressed public key (usable as argument to pk or multi)</li>
<li><b>U</b>: A dummy uncompressed public key (usable as argument to pk or multi)</li>
<li><b>H</b>: A dummy hash (usable as argument to hash)</li>
</ul>
<hr/>
<b>Miniscript output</b><br/>
<textarea rows="4" cols="100" id="descout"></textarea>
<button type="button" onclick="miniscript_analyze();">Analyze</button>
<hr/>
<b>Analysis</b><br/>
<a id="spendout"></a>
</div>
</div>
<div class="card text-left">
<h3 class="card-header">Miniscript reference</h3>
<div class="card-block">
<table border="1">
<tr><th>Type</th><th>Shorthand</th><th>Behavior under honest inputs</th><th>Behavior under adverserial inputs</th></tr>
<tr><td>Base</td><td>B</td><td>Takes its inputs from the top of the stack. Pushes a nonzero value of up to 4 bytes if the condition is satisfied, exactly zero otherwise.</td><td>Pushes zero onto the stack, or aborts.</td></tr>
<tr><td>Key</td><td>K</td><td>Takes its inputs from the top of the stack. Pushes a public key with which a checksig is to be done onto the stack.</td><td>Aborts.</td></tr>
<tr><td>Verify</td><td>V</td><td>Takes its inputs from the top of the stack, which must satisfy the condition. Does not push anything onto the stack.</td><td>Aborts.</td></tr>
<tr><td>Wrapped</td><td>W</td><td>Takes from the stack its inputs + element X at the top. If the inputs satisfy the condition, [t X] or [X t] is pushed, where t is a nonzero value of up to 4 bytes. If not, [0 X] or [X 0] is pushed.</td><td>Pushes [0 X] or [X 0] onto the stack, or aborts.</td></tr>
</table>
In addition, every expression can have zero or more of the following properties used for reasoning about correctness:<ul>
<li><b>z</b> "zero": Known to consume exactly zero stack elements. Conflicts with "o".</li>
<li><b>o</b> "one": Known to consume exactly one stack element. Conflicts with "z".</li>
<li><b>n</b> "nonzero": Known to consume at least one stack element, and the top element is never required to be 0 to satisfy the condition. Conflicts with "z". Impossible for W.</li>
<li><b>d</b> "dissatisfiable": There is a guaranteed way to this dissatisfy the expression. Impossible for V.</li>
<li><b>u</b> "unit": Satisfaction always results in an exact 1 on the stack (as opposed to arbitrary nonzero value). Impossible for V. Implied by K</li>
</ul>
There are also four more properties that let us reason about nonmalleability:<ul>
<li><b>e</b> "expr": A unique way to dissatisfy this expression exists which cannot be modified into another dissatisfaction by an attacker. Conflicts with "f". Implies "d". Impossible for V.</li>
<li><b>f</b> "forced": There is no way to dissatisfy the expression, either under honest or malicious input. Conflicts with "d" and "e". Implied by V.</li>
<li><b>s</b> "safe": Satisfying this expression requires at least one signature. This means a dissatisfaction cannot be converted into a satisfaction for this expression. Implied by K.</li>
<li><b>m</b> "nonmalleable": For every way the condition can be met, a unique satisfaction exists which cannot be modified into another satisfaction by an attacker. Implied by Z.</li>
</ul>
<h3>Legend</h3>
<table border="1">
<tr>
<th>Semantics</th>
<th>Node</th>
<th>Script</th>
<th>nsat</th>
<th>sat (X,Y)</th>
<th>sat Z</th>
<th>Types</th>
<th>Req.</th>
<th>Corr. prop.</th>
<th>Mall. prop.</th>
</tr>
<tr>
<td rowspan="2">check(key)</td>
<td>pk(key)</td>
<td>key</td>
<td>0</td>
<td>sig</td>
<td>-</td>
<td>K</td>
<td></td>
<td>o, n, u, d</td>
<td>e, m, s</td>
</tr>
<tr>
<td>pk_h(keyhash)</td>
<td>DUP HASH160 keyhash EQUALVERFIFY</td>
<td>0 key</td>
<td>sig key</td>
<td>-</td>
<td>K</td>
<td></td>
<td>n, u, d</td>
<td>e, m, s</td>
</tr>
<tr>
<td>nSequence &ge; n (and compatible)</td>
<td>older(n)</td>
<td>n CHECKSEQUENCEVERIFY</td>
<td>-</td>
<td>[]</td>
<td>-</td>
<td>B</td>
<td>n &ge; 1</td>
<td>z</td>
<td>f, m</td>
</tr>
<tr>
<td>nLockTime &ge; n (and compaitlbe)</td>
<td>after(n)</td>
<td>n CHECKLOCKTIMEVERIFY</td>
<td>-</td>
<td>[]</td>
<td>-</td>
<td>B</td>
<td>2<sup>31</sup> > n &ge; 1</td>
<td>z</td>
<td>f, m</td>
</tr>
<tr>
<td>len(x) = 32 and SHA256(x) = h</td>
<td>sha256(h)</td>
<td>SIZE 32 EQUALVERIFY SHA256 h EQUAL</td>
<td>000...</td>
<td>x</td>
<td>-</td>
<td>B</td>
<td></td>
<td>o, n, u, d</td>
<td>m</td>
</tr>
<tr>
<td>len(x) = 32 and HASH256(x) = h</td>
<td>hash256(h)</td>
<td>SIZE 32 EQUALVERIFY HASH256 h EQUAL</td>
<td>000...</td>
<td>x</td>
<td>-</td>
<td>B</td>
<td></td>
<td>o, n, u, d</td>
<td>m</td>
</tr>
<tr>
<td>len(x) = 32 and RIPEMD160(x) = h</td>
<td>ripemd160(h)</td>
<td>SIZE 32 EQUALVERIFY RIPEMD160 h EQUAL</td>
<td>000...</td>
<td>x</td>
<td>-</td>
<td>B</td>
<td></td>
<td>o, n, u, d</td>
<td>m</td>
</tr>
<tr>
<td>len(x) = 32 and HASH160(x) = h</td>
<td>hash160(h)</td>
<td>SIZE 32 EQUALVERIFY HASH160 h EQUAL</td>
<td>000...</td>
<td>x</td>
<td>-</td>
<td>B</td>
<td></td>
<td>o, n, u, d</td>
<td>m</td>
</tr>
<tr>
<td rowspan="3">X and Y</td>
<td>and_v(X,Y)</td>
<td>[X] [Y]</td>
<td>-</td>
<td>sat<sub>Y</sub> sat<sub>X</sub></td>
<td>-</td>
<td>B=V<sub>X</sub>B<sub>Y</sub><br />K=V<sub>X</sub>K<sub>Y</sub><br />V=V<sub>X</sub>V<sub>Y</sub></td>
<td></td>
<td>
u=u<sub>Y</sub><br />
n=n<sub>X</sub>+z<sub>X</sub>n<sub>Y</sub><br />
z=z<sub>X</sub>z<sub>Y</sub><br />
o=z<sub>X</sub>o<sub>Y</sub>+o<sub>X</sub>z<sub>Y</sub>
</td>
<td>
f=f<sub>X</sub>f<sub>Y</sub>[=f<sub>Y</sub>]<br />
m=m<sub>X</sub>m<sub>Y</sub><br />
s=s<sub>X</sub>+s<sub>Y</sub>
</td>
</tr>
<tr>
<td>and_b(X,Y)</td>
<td>[X] [Y] BOOLAND</td>
<td>nsat<sub>Y</sub> nsat<sub>X</sub></td>
<td>sat<sub>Y</sub> sat<sub>X</sub></td>
<td>-</td>
<td>B=B<sub>X</sub>W<sub>Y</sub></td>
<td></td>
<td>
z=z<sub>X</sub>z<sub>Y</sub><br />
o=z<sub>X</sub>o<sub>Y</sub>+o<sub>X</sub>z<sub>Y</sub><br />
n=n<sub>X</sub>+z<sub>X</sub>n<sub>Y</sub><br />
d=d<sub>X</sub>d<sub>Y</sub><br />
u
</td>
<td>
f=f<sub>X</sub>f<sub>Y</sub><br />
e=e<sub>X</sub>e<sub>Y</sub>s<sub>X</sub>s<sub>Y</sub><br />
m=m<sub>X</sub>m<sub>Y</sub><br />
s=s<sub>X</sub>+s<sub>Y</sub>
</td>
</tr>
<tr>
<td>and_n(X,Y)</td>
<td>[X] NOTIF 0 ELSE [Y] ENDIF (=andor(X,Y,0))</td>
<td>nsat<sub>X</sub></td>
<td>sat<sub>Y</sub> sat<sub>X</sub></td>
<td>-</td>
<td>B=B<sub>X</sub>B<sub>Y</sub></td>
<td>d<sub>X</sub>u<sub>X</sub></td>
<td>
z=z<sub>X</sub>z<sub>Y</sub><br />
o=o<sub>X</sub>z<sub>Y</sub><br />
u=u<sub>Y</sub><br />
d=d<sub>X</sub>[=1]
</td>
<td>
f=f<sub>Y</sub>f<sub>X</sub>[=0]<br />
e=e<sub>X</sub>(s<sub>X</sub>+f<sub>Y</sub>)<br />
m=m<sub>X</sub>m<sub>Y</sub>e<sub>X</sub><br />
s=s<sub>X</sub>+s<sub>Y</sub>
</td>
</tr>
<tr>
<td rowspan="4">X or Z</td>
<td>or_b(X,Z)</td>
<td>[X] [Z] BOOLOR</td>
<td>nsat<sub>Z</sub> nsat<sub>X</sub></td>
<td>nsat<sub>Z</sub> sat<sub>X</sub></td>
<td>sat<sub>Z</sub> nsat<sub>X</sub></td>
<td>B=B<sub>X</sub>W<sub>Z</sub></td>
<td>d<sub>X</sub>d<sub>Z</sub></td>
<td>
z=z<sub>X</sub>z<sub>Z</sub><br />
o=z<sub>X</sub>o<sub>Z</sub>+o<sub>X</sub>z<sub>Z</sub><br />
d=d<sub>X</sub>d<sub>Z</sub>[=1]<br />
u
</td>
<td>
f=f<sub>X</sub>+f<sub>Z</sub>[=0]<br />
e=e<sub>X</sub>e<sub>Z</sub><br />
m=m<sub>X</sub>m<sub>Z</sub>e<sub>X</sub>e<sub>Z</sub>(s<sub>X</sub>+s<sub>Z</sub>)<br />
s=s<sub>X</sub>s<sub>Z</sub>
</td>
</tr>
<tr>
<td>or_d(X,Z)</td>
<td>[X] IFDUP NOTIF [Z] ENDIF</td>
<td>nsat<sub>Z</sub> nsat<sub>X</sub></td>
<td>sat<sub>X</sub></td>
<td>sat<sub>Z</sub> nsat<sub>X</sub></td>
<td>B=B<sub>X</sub>B<sub>Z</sub></td>
<td>d<sub>X</sub>u<sub>X</sub></td>
<td>
z=z<sub>X</sub>z<sub>Z</sub><br />
o=o<sub>X</sub>z<sub>Z</sub><br />
u=u<sub>X</sub>(f<sub>X</sub>+u<sub>Z</sub>)[=u<sub>Z</sub>]<br />
d=d<sub>X</sub>d<sub>Z</sub>[=d<sub>Z</sub>]
</td>
<td>
f=f<sub>X</sub>+f<sub>Z</sub>[=f<sub>Z</sub>]<br />
e=e<sub>X</sub>e<sub>Z</sub><br />
m=m<sub>X</sub>m<sub>Z</sub>e<sub>X</sub>(s<sub>X</sub>+s<sub>Z</sub>)<br />
s=s<sub>X</sub>s<sub>Z</sub>
</td>
</tr>
<tr>
<td>or_c(X,Z)</td>
<td>[X] NOTIF [Z] ENDIF</td>
<td>-</td>
<td>sat<sub>X</sub></td>
<td>sat<sub>Z</sub> nsat<sub>X</sub></td>
<td>V=B<sub>X</sub>V<sub>Z</sub></td>
<td>d<sub>X</sub>u<sub>X</sub></td>
<td>
z=z<sub>X</sub>z<sub>Z</sub><br />
o=o<sub>X</sub>z<sub>Z</sub>
</td>
<td>
f=f<sub>X</sub>+f<sub>Z</sub>[=1]<br />
m=m<sub>X</sub>m<sub>Z</sub>e<sub>X</sub>(s<sub>X</sub>+s<sub>Z</sub>)<br />
s=s<sub>X</sub>s<sub>Z</sub>
</td>
</tr>
<tr>
<td>or_i(X,Z)</td>
<td>IF [X] ELSE [Z] ENDIF</td>
<td>nsat<sub>X</sub> 1<br />nsat<sub>Z</sub> 0</td>
<td>sat<sub>X</sub> 1</td>
<td>sat<sub>Z</sub> 0</td>
<td>V=V<sub>X</sub>V<sub>Z</sub><br />B=B<sub>X</sub>B<sub>Z</sub><br />K=K<sub>X</sub>K<sub>Z</sub></td>
<td></td>
<td>
o=z<sub>X</sub>z<sub>Z</sub><br />
u=u<sub>X</sub>u<sub>Z</sub><br />
d=d<sub>X</sub>+d<sub>Z</sub>
</td>
<td>
f=f<sub>X</sub>f<sub>Z</sub><br />
e=e<sub>X</sub>f<sub>Z</sub>+e<sub>Z</sub>f<sub>X</sub><br />
m=m<sub>X</sub>m<sub>Z</sub>(s<sub>X</sub>+s<sub>Z</sub>)<br />
s=s<sub>X</sub>s<sub>Z</sub>
</td>
</tr>
<tr>
<td>(X and Y) or Z</td>
<td>andor(X,Y,Z)</td>
<td>[X] NOTIF [Z] ELSE [Y] ENDIF</td>
<td>nsat<sub>Z</sub> nsat<sub>X</sub></td>
<td>sat<sub>Y</sub> sat<sub>X</sub></td>
<td>sat<sub>Z</sub> nsat<sub>X</sub></td>
<td>B=B<sub>X</sub>B<sub>Y</sub>B<sub>Z</sub><br />K=B<sub>X</sub>K<sub>Y</sub>K<sub>Z</sub><br />V=B<sub>X</sub>V<sub>Y</sub>V<sub>Z</sub></td>
<td>d<sub>X</sub>u<sub>X</sub></td>
<td>
z=z<sub>X</sub>z<sub>Y</sub>z<sub>Z</sub><br />
o=z<sub>X</sub>o<sub>Y</sub>o<sub>Z</sub>+o<sub>X</sub>z<sub>Y</sub>z<sub>Z</sub><br />
u=u<sub>Y</sub>u<sub>Z</sub><br />
d=d<sub>X</sub>d<sub>Z</sub>[=d<sub>Z</sub>]
</td>
<td>
f=f<sub>Y</sub>(f<sub>X</sub>+f<sub>Z</sub>)[=f<sub>Y</sub>f<sub>Z</sub>]<br />
e=e<sub>X</sub>e<sub>Z</sub>(s<sub>X</sub>+f<sub>Y</sub>)<br />
m=m<sub>X</sub>m<sub>Y</sub>m<sub>Z</sub>e<sub>X</sub>(s<sub>X</sub>+s<sub>Y</sub>+s<sub>Z</sub>)<br />
s=s<sub>Z</sub>(s<sub>X</sub>+s<sub>Y</sub>)
</td>
</tr>
<tr>
<td>X<sub>1</sub> + ... + X<sub>n</sub> = k</td>
<td>thresh(k,...)</td>
<td>[X<sub>1</sub>] ([X<sub>i</sub> ADD)*(n-1) k EQUAL</td>
<td>nsat...</td>
<td>(sat|nsat)...</td>
<td>-</td>
<td>B=X<sub>1</sub> is B<br />others are W</td>
<td>n > k > 1<br />all are d and u</td>
<td>
z=all are z<br />
o=all are z, except one is o<br />
d<br />
u
</td>
<td>
e=all are e and s<br />
m=all are e and m, &ge;(n-k) are s<br />
s=&ge;(n-k+1) are s
</td>
</tr>
<tr>
<td>check(key_1) + ... = k</td>
<td>thresh_m(k,...)</td>
<td>k key_1 ... key_n n CHECKMULTISIG</td>
<td>0 0 ... 0</td>
<td>0 sig...</td>
<td>-</td>
<td>B</td>
<td>n &ge; k &ge; 1</td>
<td>n, u, d</td>
<td>e, m, s</td>
</tr>
<tr>
<td rowspan="10">X</td>
<td>a:X</td>
<td>TOALTSTACK [X] FROMALTSTACK</td>
<td>nsat<sub>X</sub></td>
<td>sat<sub>X</sub></td>
<td>-</td>
<td>W=B<sub>X</sub></td>
<td></td>
<td>u=u<sub>X</sub>, d=d<sub>X</sub></td>
<td>f=f<sub>X</sub>, e=e<sub>X</sub>, m=m<sub>X</sub>, s=s<sub>X</sub></td>
</tr>
<tr>
<td>s:X</td>
<td>SWAP [X]</td>
<td>nsat<sub>X</sub></td>
<td>sat<sub>X</sub></td>
<td>o<sub>X</sub></td>
<td>W=B<sub>X</sub></td>
<td></td>
<td>u=u<sub>x</sub>, d=d<sub>X</sub></td>
<td>f=f<sub>X</sub>, e=e<sub>X</sub>, m=m<sub>X</sub>, s=s<sub>X</sub></td>
</tr>
<tr>
<td>c:X</td>
<td>[X] CHECKSIG</td>
<td>nsat<sub>X</sub></td>
<td>sat<sub>X</sub></td>
<td>-</td>
<td>B=K<sub>X</sub></td>
<td></td>
<td>o=o<sub>X</sub>, n=n<sub>X</sub>, u, d=d<sub>X</sub></td>
<td>e=e<sub>X</sub>, m=m<sub>X</sub>, s=s<sub>X</sub>[=1]</td>
</tr>
<tr>
<td>t:X</td>
<td>[X] 1 (=and_v(X,1))</td>
<td>-</td>
<td>sat<sub>X</sub></td>
<td>-</td>
<td>B=V<sub>X</sub></td>
<td></td>
<td>u, n=n<sub>X</sub>, z=z<sub>X</sub>, o=o<sub>X</sub></td>
<td>f, m=m<sub>X</sub>, s=s<sub>X</sub></td>
<tr>
<td>d:X</td>
<td>DUP IF [X] ENDIF</td>
<td>0</td>
<td>sat<sub>X</sub> 1</td>
<td>-</td>
<td>B=V<sub>X</sub></td>
<td>z<sub>X</sub></td>
<td>o=z<sub>X</sub>, n, u, d</td>
<td>e=f<sub>X</sub>, m=m<sub>X</sub>, s=s<sub>X</sub></td>
</tr>
<tr>
<td>v:X</td>
<td>[X] VERIFY</td>
<td>-</td>
<td>sat<sub>X</sub></td>
<td>-</td>
<td>V=B<sub>X</sub></td>
<td></td>
<td>z=z<sub>X</sub>, o=o<sub>X</sub>, n=n<sub>X</sub></td>
<td>f, m=m<sub>X</sub>, s=s<sub>X</sub></td>
</tr>
<tr>
<td>j:X</td>
<td>SIZE 0NOTEQUAL IF [X] ENDIF</td>
<td>0</td>
<td>sat<sub>X</sub></td>
<td>-</td>
<td>B=B<sub>X</sub></td>
<td>n<sub>X</sub></td>
<td>o=o<sub>X</sub>, n, u=u<sub>X</sub>, d</td>
<td>e=f<sub>X</sub>, m=m<sub>X</sub>, s=s<sub>X</sub></td>
</tr>
<tr>
<td>n:X</td>
<td>[X] 0NOTEQUAL</td>
<td>nsat<sub>X</sub></td>
<td>sat<sub>X</sub></td>
<td>-</td>
<td>B=B<sub>X</sub></td>
<td></td>
<td>z=z<sub>X</sub>, o=o<sub>X</sub>, n=n<sub>X</sub>, u, d=d<sub>X</sub></td>
<td>f=f<sub>X</sub>, e=e<sub>X</sub>, m=m<sub>X</sub>, s=s<sub>X</sub></td>
</tr>
<tr>
<td>l:X</td>
<td>IF 0 ELSE [X] ENDIF (=or_i(0,X))</td>
<td>1</td>
<td>sat<sub>X</sub> 0</td>
<td>-</td>
<td>B=B<sub>X</sub></td>
<td></td>
<td>o=z<sub>X</sub>, u=u<sub>X</sub>, d</td>
<td>e=f<sub>X</sub>, m=m<sub>X</sub>, s=s<sub>X</sub></td>
</tr>
<tr>
<td>u:X</td>
<td>IF [X] ELSE 0 ENDIF (=or_i(X,0))</td>
<td>0</td>
<td>sat<sub>X</sub> 1</td>
<td>-</td>
<td>B=B<sub>X</sub></td>
<td></td>
<td>o=z<sub>X</sub>, u=u<sub>X</sub>, d</td>
<td>e=f<sub>X</sub>, m=m<sub>X</sub>, s=s<sub>X</sub></td>
</tr>
<tr>
<td>true</td>
<td>1</td>
<td>1</td>
<td>-</td>
<td>[]</td>
<td>-</td>
<td>B</td>
<td></td>
<td>z, u</td>
<td>f, m</td>
</tr>
<tr>
<td>false</td>
<td>0</td>
<td>0</td>
<td>[]</td>
<td>-</td>
<td>-</td>
<td>B</td>
<td></td>
<td>z, u, d</td>
<td>e, m, s</td>
</tr>
</table>
</div>
</div>
</div>
</body>
</html>