-
Notifications
You must be signed in to change notification settings - Fork 47
/
Copy pathindex.html
685 lines (613 loc) · 48.2 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
<!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>
function htmlEscape(str) {
return String(str)
.replace(/&/g, '&')
.replace(/"/g, '"')
.replace(/'/g, ''')
.replace(/</g, '<')
.replace(/>/g, '>');
}
em_miniscript_compile = Module.cwrap('miniscript_compile', 'none', ['string', 'number', 'number', 'number', 'number', 'number', 'number']);
em_miniscript_analyze = Module.cwrap('miniscript_analyze', 'none', ['string', 'number', 'number', 'number', 'number']);
function miniscript_compile() {
document.getElementById("out").innerHTML = "Compiling...";
window.setTimeout(function() {
src = document.getElementById("source").value;
var msout = Module._malloc(10000);
var costout = Module._malloc(500);
var asmout = Module._malloc(100000);
em_miniscript_compile(src, msout, 10000, costout, 500, asmout, 100000);
document.getElementById("analyze_ms").value = Module.UTF8ToString(msout);
document.getElementById("analyze_out").innerHTML = "";
document.getElementById("out").innerHTML =
"<p><p><b>Miniscript output:</b><p><code>" + htmlEscape(Module.UTF8ToString(msout)) + "</code>" +
"<p><b>Spending cost analysis</b><p>" + Module.UTF8ToString(costout) + "" +
"<p><b>Resulting script structure</b><p><samp><pre>" + htmlEscape(Module.UTF8ToString(asmout)) + "</pre></samp>";
Module._free(msout)
Module._free(costout)
Module._free(asmout)
});
}
function load_policy(pol) {
document.getElementById("source").value = pol;
miniscript_compile();
}
function miniscript_analyze() {
document.getElementById("analyze_out").innerHTML = "Analyzing...";
window.setTimeout(function() {
src = document.getElementById("analyze_ms").value;
var analyze_out = Module._malloc(50000);
var asmout = Module._malloc(100000);
em_miniscript_analyze(src, analyze_out, 50000, asmout, 100000);
document.getElementById("analyze_out").innerHTML =
"<p><p><b>Analysis</b><p>" + Module.UTF8ToString(analyze_out) + "<p><small>Hover over the tree elements for more details</small>" +
"<p><b>Resulting script structure</b><p><samp><pre>" + htmlEscape(Module.UTF8ToString(asmout)) + "</pre></samp>";
Module._free(analyze_out)
Module._free(asmout)
});
}
</script>
<div class="container" style="margin-top:50px">
<div class="card mb-3 text-left">
<h3 class="card-header">Introduction</h3>
<div class="card-block">
<p>
<em>Miniscript</em> is a language for writing (a subset of) Bitcoin Scripts in a structured way, enabling analysis, composition, generic signing and more.
<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>
<li>Given a combination of spending conditions, finding the most economical script to implement it.</li>
<li>Given 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>
<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 particular resource limitations like the ops limit might be hit when spending.</li>
</ul>
<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 below). Finally, compatible scripts can easily be converted to Miniscript form - avoiding the need for additional metadata for e.g. signing devices that support it.
<p>
Miniscript is designed for (P2SH-)P2WSH and Tapscript (as defined in BIP342) embedded scripts. Most of its constructions
work 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.
<p>
Miniscript was designed and implemented by Pieter Wuille, Andrew Poelstra, and Sanket Kanjalkar at Blockstream Research, but is the result of discussions with several other people.
<p>
Links:<ul>
<li>This <a href="http://bitcoin.sipa.be/miniscript">website</a> and C++ compiler: <a href="https://github.com/sipa/miniscript">[code]</a></li>
<li>Bitcoin Core compatible C++ implementation: <a href="https://github.com/sipa/miniscript/tree/master/bitcoin/script">[code]</a></li>
<li>Rust-miniscript implementation: <a href="https://github.com/apoelstra/rust-miniscript">[code]</a></li>
<li>Talk about (an early version of) Miniscript at <a href="https://cyber.stanford.edu/sbc19">SBC'19</a>: <a href="https://www.youtube.com/watch?v=XM1lzN4Zfks">[video]</a> <a href="http://diyhpl.us/wiki/transcripts/stanford-blockchain-conference/2019/miniscript/">[transcript]</a> <a href="https://prezi.com/view/KH7AXjnse7glXNoqCxPH/">[slides]</a></li>
</ul>
</div>
</div>
<div class="card mb-3 text-left">
<h3 class="card-header">Policy to Miniscript compiler</h3>
<div class="card-block">
<p>Here you can see a demonstration of the P2WSH Miniscript compiler. Write a spending policy according to the instructions below, and observe how it affects the constructed Miniscript.
<form>
<div class="form-group">
<label for="source">Policy</label>
<textarea class="form-control" id="source" rows="1">and(pk(A),or(pk(B),or(9@pk(C),older(1000))))</textarea>
<div class="small form-text test-muted">Supported policies:
<ul>
<li><samp>pk(<em>NAME</em>)</samp>: Require public key named <em>NAME</em> to sign. <em>NAME</em> can be any string up to 16 characters.</li>
<li><samp>after(<em>NUM</em>)</samp>, <samp>older(<em>NUM</em>)</samp>: Require that the <samp>nLockTime</samp>/<samp>nSequence</samp> value is at least <em>NUM</em>. <em>NUM</em> cannot be 0.</li>
<li><samp>sha256(<em>HEX</em>)</samp>, <samp>hash256(<em>HEX</em>)</samp>: Require that the preimage of 64-character <em>HEX</em> is revealed. The special value <samp>H</samp> can be used as <em>HEX</em>.</li>
<li><samp>ripemd160(<em>HEX</em>)</samp>, <samp>hash160(<em>HEX</em>)</samp>: Require that the preimage of 40-character <em>HEX</em> is revealed. The special value <samp>H</samp> can be used as <em>HEX</em>.</li>
<li><samp>and(<em>POL</em>,<em>POL</em>)</samp>: Require that both subpolicies are satisfied.</li>
<li><samp>or([<em>N</em>@]<em>POL</em>,[<em>N</em>@]<em>POL</em>)</samp>: Require that one of the subpolicies is satisfied. The numbers N indicate the relative probability of each of the subexpressions (so <samp>9@</samp> is 9 times more likely than the default).</li>
<li><samp>thresh(<em>NUM</em>,<em>POL</em>,<em>POL</em>,...)</samp>: Require that NUM out of the following subpolicies are met (all combinations are assumed to be equally likely).</li>
</ul></div>
Fill field with:
<ul>
<li><a class="demo_link" href='javascript:load_policy("pk(key_1)")'>A single key</a>
<li><a class="demo_link" href='javascript:load_policy("or(pk(key_1),pk(key_2))")'>One of two keys (equally likely)</a>
<li><a class="demo_link" href='javascript:load_policy("or(99@pk(key_likely),pk(key_unlikely))")'>One of two keys (one likely, one unlikely)</a>
<li><a class="demo_link" href='javascript:load_policy("and(pk(key_user),or(99@pk(key_service),older(12960)))")'>A user and a 2FA service need to sign off, but after 90 days the user alone is enough</a>
<li><a class="demo_link" href='javascript:load_policy("thresh(3,pk(key_1),pk(key_2),pk(key_3),older(12960))")'>A 3-of-3 that turns into a 2-of-3 after 90 days</a>
<li><a class="demo_link" href='javascript:load_policy("or(pk(key_revocation),and(pk(key_local),older(1008)))")'>The BOLT #3 to_local policy</a>
<li><a class="demo_link" href='javascript:load_policy("or(pk(key_revocation),and(pk(key_remote),or(pk(key_local),hash160(H))))")'>The BOLT #3 offered HTLC policy</a>
<li><a class="demo_link" href='javascript:load_policy("or(pk(key_revocation),and(pk(key_remote),or(and(pk(key_local),hash160(H)),older(1008))))")'>The BOLT #3 received HTLC policy</a>
</ul>
</div>
<button type="button" class="btn btn-primary" onclick="miniscript_compile();">Compile</button>
</form>
<div id="out"></div>
</div>
</div>
<div class="card text-left mb-3">
<h3 class="card-header">Analyze a Miniscript</h3>
<div class="card-block">
<p>Here you can analyze the structure of a Miniscript expression and more.
<form>
<div class="form-group">
<label for="analyze_ms">Miniscript</label>
<textarea class="form-control" id="analyze_ms" rows="1">and_v(v:pk(K),pk(A))</textarea>
<small class="form-text test-muted">Provide a well-typed miniscript expression of type "B".</small>
</div>
<button type="button" class="btn btn-primary" onclick="miniscript_analyze();">Analyze</button>
</form>
<div id="analyze_out"></div>
</div>
</div>
<div class="card mb-3 text-left">
<h3 class="card-header">Miniscript reference</h3>
<div class="card-block">
<h4>P2WSH or Tapscript?</h4>
<p>
The Miniscript specifications vary only slightly between P2WSH and Tapscript embedded scripts. Differences are pointed
inline. If no information specific to the context is given you can assume it is valid for both P2WSH and Tapscript.
</p>
<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>dv:older(144)</code> is the <code>d:</code>
wrapper applied to the <code>v:</code> wrapper applied to the <code>older</code> fragment for 144 blocks. Note how
<samp>key</samp> expressions in this table and the followings are implicitly 32 bytes "x-only" public key in Tapscript
and 33 bytes compressed public keys in P2WSH.
<div class="table-responsive">
<table class="table table-sm">
<thead class="thead-light">
<tr><th scope="col">Semantics</th><th scope="col">Miniscript fragment</th><th scope="col">Bitcoin Script</th></tr></thead>
<tbody>
<tr>
<td>false</td>
<td><code>0</code></td>
<td><samp>0</samp></td>
</tr>
<tr>
<td>true</td>
<td><code>1</code></td>
<td><samp>1</samp></td>
</tr>
<tr>
<td rowspan="4">check(key)</td>
<td><code>pk_k(key)</code></td>
<td><samp><key></samp></td>
</tr>
<tr>
<td><code>pk_h(key)</code></td>
<td><samp>DUP HASH160 <HASH160(key)> EQUALVERIFY</samp></td>
</tr>
<tr>
<td><code>pk(key) = c:pk_k(key)</code></td>
<td><samp><key> CHECKSIG</samp></td>
</tr>
<tr>
<td><code>pkh(key) = c:pk_h(key)</code></td>
<td><samp>DUP HASH160 <HASH160(key)> EQUALVERIFY CHECKSIG</samp></td>
</tr>
<tr>
<td>nSequence ≥ n (and compatible)</td>
<td><code>older(n)</code></td>
<td><samp><n> CHECKSEQUENCEVERIFY</samp></td>
</tr>
<tr>
<td>nLockTime ≥ n (and compatible)</td>
<td><code>after(n)</code></td>
<td><samp><n> CHECKLOCKTIMEVERIFY</samp></td>
</tr>
<tr>
<td>len(x) = 32 and SHA256(x) = h</td>
<td><code>sha256(h)</code></td>
<td><samp>SIZE <20> EQUALVERIFY SHA256 <h> EQUAL</samp></td>
</tr>
<tr>
<td>len(x) = 32 and HASH256(x) = h</td>
<td><code>hash256(h)</code></td>
<td><samp>SIZE <20> EQUALVERIFY HASH256 <h> EQUAL</samp></td>
</tr>
<tr>
<td>len(x) = 32 and RIPEMD160(x) = h</td>
<td><code>ripemd160(h)</code></td>
<td><samp>SIZE <20> EQUALVERIFY RIPEMD160 <h> EQUAL</samp></td>
</tr>
<tr>
<td>len(x) = 32 and HASH160(x) = h</td>
<td><code>hash160(h)</code></td>
<td><samp>SIZE <20> EQUALVERIFY HASH160 <h> EQUAL</samp></td>
<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>
<tr>
<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>
</tr>
<tr>
<td><code>and_b(<em>X</em>,<em>Y</em>)</code></td>
<td><samp><em>[X]</em> <em>[Y]</em> BOOLAND</samp></td>
</tr>
<tr>
<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> NOTIF 0 ELSE <em>[Y]</em> ENDIF</samp></td>
</tr>
<tr>
<td rowspan="4"><em>X</em> or <em>Z</em></td>
<td><code>or_b(<em>X</em>,<em>Z</em>)</code></td>
<td><samp><em>[X]</em> <em>[Z]</em> BOOLOR</samp></td>
</tr>
<tr>
<td><code>or_c(<em>X</em>,<em>Z</em>)</code></td>
<td><samp><em>[X]</em> NOTIF <em>[Z]</em> ENDIF</samp></td>
</tr>
<tr>
<td><code>or_d(<em>X</em>,<em>Z</em>)</code></td>
<td><samp><em>[X]</em> IFDUP NOTIF <em>[Z]</em> ENDIF</samp></td>
</tr>
<tr>
<td><code>or_i(<em>X</em>,<em>Z</em>)</code></td>
<td><samp>IF <em>[X]</em> ELSE <em>[Z]</em> ENDIF</samp></td>
</tr>
<tr>
<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> ADD ... <em>[X<sub>n</sub>]</em> ADD ... <k> EQUAL</samp></td>
</tr>
<tr>
<td>check(key<sub>1</sub>) + ... + check(key<sub>n</sub>) = k <small><em>(P2WSH only)</em></small></td>
<td><code>multi(k,key<sub>1</sub>,...,key<sub>n</sub>)</code></td>
<td><samp><k> <key<sub>1</sub>> ... <key<sub>n</sub>> <n> CHECKMULTISIG</samp></td>
</tr>
<tr>
<td>check(key<sub>1</sub>) + ... + check(key<sub>n</sub>) = k <small><em>(Tapscript only)</em></small></td>
<td><code>multi_a(k,key<sub>1</sub>,...,key<sub>n</sub>)</code></td>
<td>
<samp><key<sub>1</sub>> CHECKSIG <key<sub>2</sub>> CHECKSIGADD ... <key<sub>n</sub>> CHECKSIGADD <k> NUMEQUAL</samp>
</td>
</tr>
<tr>
<td rowspan="10"><em>X</em> (identities)</td>
<td><code>a:<em>X</em></code></td>
<td><samp>TOALTSTACK <em>[X]</em> FROMALTSTACK</samp></td>
</tr>
<tr>
<td><code>s:<em>X</em></code></td>
<td><samp>SWAP <em>[X]</em></samp></td>
</tr>
<tr>
<td><code>c:<em>X</em></code></td>
<td><samp><em>[X]</em> CHECKSIG</samp></td>
</tr>
<tr>
<td><code>t:<em>X</em></code> = <code>and_v(<em>X</em>,1)</code></td>
<td><samp><em>[X]</em> 1</samp></td>
<tr>
<td><code>d:<em>X</em></code></td>
<td><samp>DUP IF <em>[X]</em> ENDIF</samp></td>
</tr>
<tr>
<td><code>v:<em>X</em></code></td>
<td><samp><em>[X]</em> VERIFY</samp> (or <samp>VERIFY</samp> version of last opcode in <samp><em>[X]</em></samp>)</td>
</tr>
<tr>
<td><code>j:<em>X</em></code></td>
<td><samp>SIZE 0NOTEQUAL IF <em>[X]</em> ENDIF</samp></td>
</tr>
<tr>
<td><code>n:<em>X</em></code></td>
<td><samp><em>[X]</em> 0NOTEQUAL</samp></td>
</tr>
<tr>
<td><code>l:<em>X</em></code> = <code>or_i(0,<em>X</em>)</code></td>
<td><samp>IF 0 ELSE <em>[X]</em> ENDIF</samp></td>
</tr>
<tr>
<td><code>u:<em>X</em></code> = <code>or_i(<em>X</em>,0)</code></td>
<td><samp>IF <em>[X]</em> ELSE 0 ENDIF</samp></td>
</tr>
</tbody>
</table>
</div>
The <code>pk</code>, <code>pkh</code>, and <code>and_n</code> fragments 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.
<p>
<p>
Hash preimages are constrained to 32 bytes to disallow various forms of griefing, including making non-standard(un-relayable) transactions,
consensus-invalid swaps across blockchains, as well as ensure that satisfaction cost can be accurately calculated. Finally, note that <code><20></code>
are in hex representation in this document.
<p>
<h4>Correctness properties</h4>
<p>
Not every Miniscript expression can be composed with every other. Some return their result by putting true or false on the stack; others can only abort or continue.
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>
Every miniscript expression has one of four basic types:<ul>
<li><b>"B"</b> Base expressions. These take their inputs from the top of the stack. When satisfied, they push a nonzero value of up to 4 bytes onto the stack.
When dissatisfied, they push an exact 0 onto the stack (if dissatisfaction without aborting is possible at all).
This type is used for most expressions, and required for the top level expression. An example is <code>older(n)</code> = <samp><n> CHECKSEQUENCEVERIFY</samp>.</li>
<li><b>"V"</b> Verify expressions. Like "B", these take their inputs from the top of the stack. Upon satisfaction however, they continue without pushing anything. They cannot be
dissatisfied (will abort instead). 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>.
An example is <code>v:pk(key)</code> = <samp><key> CHECKSIGVERIFY</samp>.</li>
<li><b>"K"</b> Key expressions. They again take their inputs from the top of the stack, but instead of verifying a condition directly they always push a public key onto the stack, for
which a signature is still required to satisfy the expression. A "K" can be converted into a "B" using the <code>c:</code> wrapper (<samp>CHECKSIG</samp>).
An example is <code>pk_h(key)</code> = <samp>DUP HASH160 <Hash160(key)> EQUALVERIFY</samp></li>
<li><b>"W"</b> Wrapped expressions. They take their inputs from one below the top of the stack, and push a nonzero (in case of satisfaction) or zero (in case of dissatisfaction)
either on top of the stack, or one below. So for example a 3-input "W" would take the stack "A B C D E F" and turn it into "A B F 0" or "A B 0 F" in case of dissatisfaction, and
"A B F n" or "A B n F" in case of satisfaction (with n a nonzero value). Every "W" is either <code>s:B</code> (<samp>SWAP B</samp>) or <code>a:B</code> (<samp>TOALTSTACK B FROMALTSTACK</samp>).
An example is <code>s:pk(key)</code> = <samp>SWAP <key> CHECKSIG</samp>.</li>
</ul>
<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: this expression always consumes at least 1 stack element, no satisfaction for this expression requires the top input stack element to be zero.</li>
<li><b>"d"</b> Dissatisfiable: a dissatisfaction for this expression can unconditionally be constructed. This implies the dissatisfaction cannot include any signature or hash preimage, and cannot rely on timelocks being satisfied.</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>
This tables lists the correctness requirements for each of the Miniscript expressions, and its type properties in function of those of their subexpressions:
<div class="table-responsive">
<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>
<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_k(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 ≤ n < 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>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>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>Z</sub> or z<sub>Z</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>thresh(k,<em>X<sub>1</sub></em>,...,<em>X<sub>n</sub></em>)</code></td><td>1 ≤ k ≤ 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>multi(k,key<sub>1</sub>,...,key<sub>n</sub>)</code></td><td>1 ≤ k ≤ n</td><td>B</td><td>n; d; u</td></tr>
<tr><td><code>multi_a(k,key<sub>1</sub>,...,key<sub>n</sub>)</code></td><td>1 ≤ k ≤ n</td><td>B</td><td>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; n; d; <small>(Tapscript only)</small> u</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>
</tbody>
</table>
</div>
<h4>Detecting timelock mixing</h4>
<p>
The <samp>nSequence</samp> field in a transaction input, or the <samp>nLockTime</samp> field in transaction can be specified either as a time or height but not both.
Therefore it is not possible to spend scripts that require satisfaction of both, height based timelock and time based timelock of the same type.
<ul>
<li><b>"k"</b> No timelock mixing. This expression does not contain a mix of heightlock and timelock of the same type. If the miniscript does not have the "k" property, the miniscript template will not match the user expectation of the corresponding spending policy.</li>
</ul>
<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). In Tapscript scripts are only implicitly bounded by the maximum standard transaction size (of 100k virtual bytes), which makes the maximum script size a bit less than 400000 bytes.</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>multi</code>s, is above 201, are invalid by consensus (bare, P2SH, P2WSH, P2SH-P2WSH).</li>
<li>Anything but <code>pk(key)</code> (P2PK), <code>pkh(key)</code> (P2PKH), and <code>multi(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>
<li>Script satisfactions that make the stack exceed 1000 elements during or before script execution are invalid by consensus (bare, P2SH, P2WSH, P2SH-P2WSH, Tapscript).</li>
</ul>
For P2WSH, a Miniscript whose script is larger than 3600 bytes is invalid.
For all the other limits, Miniscript makes it easy to verify they don't impact the ability to satisfy a script. Note that this is different from verifying whether the limits are never
reachable at all (which is also possible). Consider for example an <code>or_b(<em>X</em>,<em>Y</em>)</code> where both <em>X</em> and <em>Y</em> require a number of large <code>multi</code>s
to be executed to satisfy. It may be the case that satisfying just one of <em>X</em> or <em>Y</em> does not exceed the ops limit, while satisfying both does. As it's never required to
satisfy both, the limit does not prevent satisfaction.
<p>
<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 and there is no timelock mixing, for every set of met conditions that are permitted by the semantics, 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>
<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.
The soundness can be reasoned about by considering all possible execution paths through each of the fragments' scripts.
<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.
</div>
</div>
<div class="card text-left">
<h3 class="card-header">Satisfactions and malleability</h3>
<div class="card-block">
<h4>Basic satisfactions</h4>
<p>
The following table shows all valid satisfactions and dissatisfactions for every Miniscript, using satisfactions and dissatisfactions of its subexpressions.
Multiple possibilities are separated by semicolons. Some options are not actually necessary to produce correct witnesses, and are called <em>non-canonical</em> options. They
are listed for completeness, but marked in <span class="text-muted">[grey]</span> below.
<div class="table-responsive">
<table class="table table-sm">
<thead class="thead-light"><tr><th scope="col">Miniscript</th><th scope="col">Dissatisfactions (dsat)</th><th scope="col">Satisfactions (sat)</th></thead>
<tbody>
<tr><td><code>0</code></td><td></td><td>-</td></tr>
<tr><td><code>1</code></td><td>-</td><td></td></tr>
<tr><td><code>pk_k(key)</code></td><td>0</td><td>sig</td></tr>
<tr><td><code>pk_h(key)</code></td><td>0 key</td><td>sig key</td></tr>
<tr><td><code>older(n)</code></td><td>-</td><td></td></tr>
<tr><td><code>after(n)</code></td><td>-</td><td></td></tr>
<tr><td><code>sha256(h)</code></td><td>any 32-byte vector except the preimage</td><td>preimage</td></tr>
<tr><td><code>ripemd160(h)</code></td><td>any 32-byte vector except the preimage</td><td>preimage</td></tr>
<tr><td><code>hash256(h)</code></td><td>any 32-byte vector except the preimage</td><td>preimage</td></tr>
<tr><td><code>hash160(h)</code></td><td>any 32-byte vector except the preimage</td><td>preimage</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>); <span class="text-muted">[dsat(<em>Y</em>) sat(<em>X</em>)]</span></td><td>sat(<em>Y</em>) sat(<em>X</em>); sat(<em>Z</em>) dsat(<em>X</em>)</td></tr>
<tr><td><code>and_v(<em>X</em>,<em>Y</em>)</code></td><td><span class="text-muted">[dsat(<em>Y</em>) sat(<em>X</em>)]</span></td><td>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>); <span class="text-muted">[sat(<em>Y</em>) dsat(<em>X</em>)]</span>; <span class="text-muted">[dsat(<em>Y</em>) sat(<em>X</em>)]</span></td><td>sat(<em>Y</em>) sat(<em>X</em>)</td></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>); sat(<em>Z</em>) dsat(<em>X</em>); <span class="text-muted">[sat(<em>Z</em>) sat(<em>X</em>)]</span></td></tr>
<tr><td><code>or_c(<em>X</em>,<em>Z</em>)</code></td><td>-</td><td>sat(<em>X</em>); 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>); 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; dsat(<em>Z</em>) 0</td><td>sat(<em>X</em>) 1; sat(<em>Z</em>) 0</td></tr>
<tr><td><code>thresh(k,<em>X<sub>1</sub></em>,...,<em>X<sub>n</sub></em>)</code></td><td>All dsats <span class="text-muted">[Sats/dsats with 1 ≤ #(sats) ≠ k]</span></td><td>Sats/dsats with #(sats) = k</td></tr>
<tr><td><code>multi(k,key<sub>1</sub>,...,key<sub>n</sub>)</code></td><td>0 0 ... 0 (k+1 times)</td><td>0 sig ... sig</td></tr>
<tr><td><code>multi_a(k,key<sub>1</sub>,...,key<sub>n</sub>)</code></td><td>0 ... 0 (n times)</td><td>sig/0 with #(sig) = k and #(sigs/0) = n </td></tr>
<tr><td><code>a:<em>X</em></code></td><td>dsat(<em>X</em>)</td><td>sat(<em>X</em>)</td></tr>
<tr><td><code>s:<em>X</em></code></td><td>dsat(<em>X</em>)</td><td>sat(<em>X</em>)</td></tr>
<tr><td><code>c:<em>X</em></code></td><td>dsat(<em>X</em>)</td><td>sat(<em>X</em>)</td></tr>
<tr><td><code>d:<em>X</em></code></td><td>0</td><td>sat(<em>X</em>) 1</td></tr>
<tr><td><code>v:<em>X</em></code></td><td>-</td><td>sat(<em>X</em>)</td></tr>
<tr><td><code>j:<em>X</em></code></td><td>0; <span class="text-muted">[dsat(<em>X</em>) (if nonzero top stack)]</span></td><td>sat(<em>X</em>)</td></tr>
<tr><td><code>n:<em>X</em></code></td><td>dsat(<em>X</em>)</td><td>sat(<em>X</em>)</td></tr>
</tbody>
</table>
</div>
<p>
The correctness properties in the previous section are based on the availability of satisfactions and dissatisfactions listed above. The requirements include a "d" for every
subexpression whose dissatisfaction may be needed in building a satisfaction for the parent expression. The "d" properties themselves rely on the "d" properties of subexpressions.
An interesting property is that in a well-typed Miniscript, dissatisfying a non-"d" subexpression always causes the overall script to fail, propagating
the failure upwards to a point where it either causes the script to abort, or reach the top level.
<p>
A conservative simplification is made here, ignoring the existence of always-true expressions like <code>1</code>. This makes the typing rules incorrect in the following cases:<ul>
<li><code>or_b(<em>X</em>,1)</code> and <code>or_b(1,<em>X</em>)</code> are complete when <em>X</em> is dissatisfiable ("d"). In that case, the condition is equivalent to 1 and is always met, and a satisfaction of the form "dsat(<em>X</em>)" exists.
<li><code>or_b(1,1)</code> is complete, as it is equivalent to 1 and "" is a valid satisfaction.</li>
<li><code>and_b(<em>X</em>,1)</code> and <code>and_b(1,<em>X</em>)</code> are dissatisfiable ("d") when <em>X</em> is.
<li><code>andor(1,1,<em>Z</em>)</code> is complete, as it is equivalent to 1 and "" is a valid satisfaction.</li>
<li><code>andor(1,<em>Y</em>,0)</code> is complete when <em>Y</em> is; it also has the same type as <em>Y</em>, despite <code>0</code> always being a "B". This is also dissatisfiable when <em>Y</em> is.
<li>The <code>1</code>s items listed above can be replaced with any other always-true expression.
</ul>
Since all these cases of inaccurate typing involve always-true expressions that can be avoided
using strictly simpler/smaller Miniscripts, we don't consider this to be a serious restriction. For Miniscripts excluding always-true expressions (except in the <code>and_v(<em>X</em>,1)</code> code), the typing rules match the definitions above.
<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>
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. Finally, malleability may interfere with the usage of hash locks as a mechanism for publishing preimages.
<p>
Because of these reasons, Miniscript is actually designed to permit non-malleable signing. As this guarantee is restricted in non-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. Participants with private keys inherently have the ability to produce different satisfactions by creating multiple signatures. While it is also interesting to study the impact rogue participants can have, we treat it as a distinct problem.</li>
<li>The attacker only has access to hash preimages that honest users have access to as well. This is a reasonable assumption because hash preimages are revealed once globally, and then available to everyone. On the other hand, making the assumption that attackers may have access to more preimages than honest users makes a large portion of scripts impossible to satisfy in a non-malleable way.</li>
<li>The attacker gets to see exactly one satisfying witness of any transaction. If he sees multiple, it becomes possible for the attacker to mix and match different satisfactions. This is very hard to reason about.</li>
<li>We restrict this analysis to scripts where no public key is repeated. If signatures constructed for one part of the script can be bound to other checks in the same script, a variant of the mixing from the previous point becomes available that is equally hard to reason about. Furthermore this situation can be avoided by using separate keys.</li>
</ul>
<p>
Malleable satisfactions or dissatisfactions appear whenever options are available to attackers distinct from the one taken by honest users. This can happen for multiple reasons:<ol>
<li>Two or more options for a satisfaction or dissatisfaction are listed in the table above which are both available to attackers directly. Regardless of which option is used in the honest solution, the attacker can change the solution to the other one.</li>
<li>Two or more options for a satisfaction or dissatisfaction are listed in the table above, only one of which is available to attackers, but the honest solution uses another one. In that case, the attacker can modify the solution to pick the one available to him.</li>
<li>The honest users pick a solution that contains a satisfaction which can be turned into a dissatisfaction without invalidating the overall witness. Those are called overcomplete solutions.</li>
</ol>
<h4>Non-malleable satisfaction algorithm</h4>
<p>
Because we assume attackers never have access to private keys, we can treat any solution that includes a signature as one that is unavailable to attackers.
For others, the worst case is that the attacker has access to every solution the honest users have, but no others: for preimages this is an explicit assumption, while timelock availability is determined
by the <samp>nLockTime</samp> and <samp>nSequence</samp> fields in the transaction. As long as the overall satisfaction includes at least one signature, those values are fixed, and timelock availability is identical for attackers and honest users.
<p>
In order to produce non-malleable satisfactions we make use of a function that returns the optimal satisfaction and dissatisfaction for a given expression (if any exist), or a special DONTUSE value, together with an optional HASSIG marker that tracks whether the solution contains at least one signature. To implement the function: <ul>
<li>Invoke the function recursively for all subexpressions, obtaining all their satisfactions/dissatisfactions.</li>
<li>Iterate over all the valid satisfactions/dissatisfactions in the table above (including the non-canonical ones), taking into account:<ul>
<li>The dissatisfactions for <code>sha256</code>, <code>ripemd160</code>, <code>hash256</code>, and <code>hash160</code> are always malleable (reason 1), so instead use DONTUSE there.</li>
<li>The non-canonical options for <code>and_b</code>, <code>or_b</code>, and <code>thresh</code> are always overcomplete (reason 3), so instead use DONTUSE there as well (with HASSIG flag if the original non-canonical solution had one).
<li>The satisfactions for <code>pk_k</code>, <code>pk_h</code>, and <code>multi</code> can be marked HASSIG.</li>
<li>When constructing solutions by combining results for subexpressions, the result is DONTUSE if any of the constituent results is DONTUSE. Furthermore, the result gets the HASSIG tag if any of the constituents do.</li>
</ul></li>
<li>If among all valid solutions (including DONTUSE ones) more than one does not have the HASSIG marker, return DONTUSE, as this is malleable because of reason 1.</li>
<li>If instead exactly one does not have the HASSIG marker, return that solution because of reason 2.</li>
<li>If all valid solutions have the HASSIG marker, but all of them are DONTUSE, return DONTUSE-HASSIG. The HASSIG marker is important because while this represents a choice between multiple options that would cause malleability if used, they are not available to the attacker, and we may be able to avoid them entirely still.
<li>Otherwise, all not-DONTUSE options are valid, so return the smallest one (in terms of witness size).
</ul>
To produce an overall satisfaction, invoke the function on the toplevel expression. If no valid satisfaction is returned, or it is DONTUSE, fail. Otherwise, if any timelocking is used in the script but the result does not have the HASSIG flag, also fail, as this represents a situation where an attacker could change the <samp>nLockTime</samp> or <samp>nSequence</samp> values to meet additional timelock conditions. Not to mention that solutions without signatures are generally insecure. If the satisfaction is both not DONTUSE and HASSIG, return it.
<p>
The above can be used to show that no non-canonical solutions listed in the satisfaction table can occur inside non-malleable satisfactions.<ul>
<li>Some of the non-canonical options (the <code>or_b</code>, <code>and_b</code>, and <code>thresh</code> ones) are overcomplete, and thus can clearly not appear in non-malleable satisfactions.</li>
<li>The fact that non-"d" expressions cannot be dissatisfied in valid witnesses rules out the usage of the non-canonical <code>and_v</code> dissatisfaction.</li>
<li>"d" expressions are defined to be unconditionally dissatisfiable, which implies that for those a non-HASSIG dissatisfaction must exist. Non-HASSIG solutions
must be preferred over HASSIG ones (reason 2), and when multiple non-HASSIG ones exist, none can be used (reason 1). This lets us rule out the other non-canonical options in the table:<ul>
<li><code>j:X</code> is always "d", its non-HASSIG dissatisfaction "0" always exists, and thus rules out any usage of "dsat(<em>X</em>)".
<li>If <code>andor(<em>X</em>,<em>Y</em>,<em>Z</em>)</code> is "d", a non-HASSIG dissatisfaction "dsat(<em>Z</em>) dsat(<em>X</em>)" must exist, and thus rules out any usage of "dsat(<em>Y</em>) sat(<em>X</em>)".</li>
<li>If <code>and_b(<em>X</em>,<em>Y</em>)</code> is "d", a non-HASSIG dissatisfaction "dsat(<em>Y</em>) dsat(<em>X</em>)" must exist, and thus rules out any usage of "dsat(<em>Y</em>) sat(<em>X</em>)" and "sat(<em>Y</em>) dsat(<em>X</em>)". Those are also overcomplete. </li>
<li><code>thresh(k,...)</code> is always "d", a non-HASSIG dissatisfaction with just dissatisfactions must exist due to typing rules, and thus rules out usage of the other dissatisfactions. They are also overcomplete.</li>
</ul>
</ul>
<h4>Guaranteeing non-malleability</h4>
<p>
Now we have an algorithm that can find the optimal non-malleable satisfaction for any Miniscript, if it exists. But can we statically prove that such a solution always exists?
In order to do that, we add additional properties to the type system:<ul>
<li><b>"s"</b> Signed: satisfying this expression always requires a signature (predicting whether all satisfactions will be HASSIG).</li>
<li><b>"f"</b> Forced: dissatisfying this expression always requires a signature (predicting whether all dissatisfactions will be HASSIG). </li>
<li><b>"e"</b> Expressive: this requires a unique unconditional dissatisfaction to exist, and forces all conditional dissatisfactions (if any) to require a signature.
</ul>
<p>
The following table lists these additional properties, and the requirements for non-malleability.
<div class="table-respnsive">
<table class="table table-sm">
<thead class="thead-light"><tr><th scope="col">Miniscript</th><th scope="col">Requires</th><th scope="col">Properties</th></tr></thead>
<tbody>
<tr><td><code>0</code></td><td></td><td>s, e</td></tr>
<tr><td><code>1</code></td><td></td><td>f</td></tr>
<tr><td><code>pk_k(key)</code></td><td></td><td>s, e</td></tr>
<tr><td><code>pk_h(key)</code></td><td></td><td>s, e</td></tr>
<tr><td><code>older(n)</code></td><td></td><td>f</td></tr>
<tr><td><code>after(n)</code></td><td></td><td>f</td></tr>
<tr><td><code>sha256(h)</code></td><td></td><td></td></tr>
<tr><td><code>ripemd160(h)</code></td><td></td><td></td></tr>
<tr><td><code>hash256(h)</code></td><td></td><td></td></tr>
<tr><td><code>hash160(h)</code></td><td></td><td></td></tr>
<tr><td><code>andor(<em>X</em>,<em>Y</em>,<em>Z</em>)</code></td><td>e<sub>X</sub> and (s<sub>X</sub> or s<sub>Y</sub> or s<sub>Z</sub>)</td><td>s=s<sub>Z</sub> and (s<sub>X</sub> or s<sub>Y</sub>); f=f<sub>Z</sub> and (s<sub>X</sub> or f<sub>Y</sub>); e=e<sub>Z</sub> and (s<sub>X</sub> or f<sub>Y</sub>)</td></tr>
<tr><td><code>and_v(<em>X</em>,<em>Y</em>)</code></td><td></td><td>s=s<sub>X</sub> or s<sub>Y</sub>; f=s<sub>X</sub> or f<sub>Y</sub></td></tr>
<tr><td><code>and_b(<em>X</em>,<em>Y</em>)</code></td><td></td><td>s=s<sub>X</sub> or s<sub>Y</sub>; f=f<sub>X</sub>f<sub>Y</sub> or s<sub>X</sub>f<sub>X</sub> or s<sub>Y</sub>f<sub>Y</sub>; e=e<sub>X</sub>e<sub>Y</sub>s<sub>X</sub>s<sub>Y</sub></td></tr>
<tr><td><code>or_b(<em>X</em>,<em>Z</em>)</code></td><td>e<sub>X</sub>e<sub>Z</sub> and (s<sub>X</sub> or s<sub>Z</sub>)</td><td>s=s<sub>X</sub>s<sub>Z</sub>; e</td></tr>
<tr><td><code>or_c(<em>X</em>,<em>Z</em>)</code></td><td>e<sub>X</sub> and (s<sub>X</sub> or s<sub>Z</sub>)</td><td>s=s<sub>X</sub>s<sub>Z</sub>; f</td></tr>
<tr><td><code>or_d(<em>X</em>,<em>Z</em>)</code></td><td>e<sub>X</sub> and (s<sub>X</sub> or s<sub>Z</sub>)</td><td>s=s<sub>X</sub>s<sub>Z</sub>; f=f<sub>Z</sub>; e=e<sub>Z</sub></td></tr>
<tr><td><code>or_i(<em>X</em>,<em>Z</em>)</code></td><td>s<sub>X</sub> or s<sub>Z</sub></td><td>s=s<sub>X</sub>s<sub>Z</sub>; f=f<sub>X</sub>f<sub>Z</sub>; e=e<sub>X</sub>f<sub>Z</sub> or e<sub>Z</sub>f<sub>X</sub></td></tr>
<tr><td><code>thresh(k,<em>X<sub>1</sub></em>,...,<em>X<sub>n</sub></em>)</code></td><td>all are e; at most k are non-s</td><td>s=at most k-1 are non-s; e=all are s</td></tr>
<tr><td><code>multi(k,key<sub>1</sub>,...,key<sub>n</sub>)</code></td><td></td><td>s; e</td></tr>
<tr><td><code>multi_a(k,key<sub>1</sub>,...,key<sub>n</sub>)</code></td><td></td><td>s; e</td></tr>
<tr><td><code>a:<em>X</em></code></td><td></td><td>s=s<sub>X</sub>; f=f<sub>X</sub>; e=e<sub>X</sub></td></tr>
<tr><td><code>s:<em>X</em></code></td><td></td><td>s=s<sub>X</sub>; f=f<sub>X</sub>; e=e<sub>X</sub></td></tr>
<tr><td><code>c:<em>X</em></code></td><td></td><td>s; f=f<sub>X</sub>; e=e<sub>X</sub></td></tr>
<tr><td><code>d:<em>X</em></code></td><td></td><td>s=s<sub>X</sub>; e</td></tr>
<tr><td><code>v:<em>X</em></code></td><td></td><td>s=s<sub>X</sub>; f</td></tr>
<tr><td><code>j:<em>X</em></code></td><td></td><td>s=s<sub>X</sub>; e=f<sub>X</sub></td></tr>
<tr><td><code>n:<em>X</em></code></td><td></td><td>s=s<sub>X</sub>; f=f<sub>X</sub>; e=e<sub>X</sub></td></tr>
</tbody>
</table>
</div>
<p>
Using the malleability type properties it is possible to determine statically whether a script can be nonmalleably satisfied under all circumstances.
In many cases it is reasonable to only accept such guaranteed-nonmalleable scripts, as unexpected behavior can occur when using other scripts.
<p>
For example, when running the non-malleable satisfaction algorithm above, adding available preimages, or increasing the <samp>nLockTime</samp>/<samp>nSequence</samp> values
actually may make it fail where it succeeded before. This is because a larger set of met conditions may mean an existing satisfaction goes from nonmalleable to malleable.
Restricting things to scripts that are guaranteed to be satisfiable in a non-malleable way avoids this problem.
<p>
When analysing Miniscripts for resource limits, restricting yourself to just non-malleable solutions (or even non-malleable scripts) also leads to tighter bounds,
as all non-canonical satisfactions and dissatisfactions can be left out of consideration.
</div>
</div>
</div>
</body>
</html>