|
| 1 | +# Miniscript Analyzer Internals |
| 2 | + |
| 3 | +This document is for contributors who want to understand or extend the |
| 4 | +TypeScript Miniscript analyzer. It focuses on the static type system and how it |
| 5 | +produces `issane` and `issanesublevel`, while keeping the satisfier-based |
| 6 | +derivation flow intact. |
| 7 | + |
| 8 | +## High-level flow |
| 9 | + |
| 10 | +1. Parse the Miniscript expression into a lightweight AST. |
| 11 | +2. Run static analysis on the AST (correctness + malleability + timelocks). |
| 12 | +3. Derive `issane` and `issanesublevel`. |
| 13 | +4. If sane, the satisfier derives satisfactions (witnesses) and classifies them |
| 14 | + as non-malleable or malleable. |
| 15 | + |
| 16 | +Key modules: |
| 17 | + |
| 18 | +- `src/compiler/parse.ts`: parses expressions into an AST. |
| 19 | +- `src/compiler/compile.ts`: compiles the AST into ASM. |
| 20 | +- `src/compiler/correctness.ts`: correctness type rules. |
| 21 | +- `src/compiler/malleability.ts`: malleability type rules. |
| 22 | +- `src/compiler/analyze.ts`: analysis pass that computes sanity flags. |
| 23 | +- `src/compiler/index.ts`: entry point that wires parse + compile + analysis. |
| 24 | + |
| 25 | +## AST model |
| 26 | + |
| 27 | +AST stands for **Abstract Syntax Tree**. It is the tree representation of a |
| 28 | +Miniscript expression where each node corresponds to one fragment or wrapper. |
| 29 | + |
| 30 | +The parser builds a minimal AST that matches Miniscript fragments and wrappers. |
| 31 | +A **node** is a plain object that always contains: |
| 32 | + |
| 33 | +- `type`: the normalized node kind (fragment or wrapper identifier) after |
| 34 | + syntactic sugar expansion (string) |
| 35 | + |
| 36 | +Depending on the fragment, a node may also contain: |
| 37 | + |
| 38 | +- `key`: a key identifier (for `pk_k`, `pk_h`) |
| 39 | +- `value`: a scalar value (for `after`, `older`, hashes) |
| 40 | +- `k`: a numeric threshold (for `thresh`, `multi`, `multi_a`) |
| 41 | +- `keys`: array of keys (for `multi`, `multi_a`) |
| 42 | +- `arg`: a single child node (for unary wrappers `a/s/c/d/v/j/n`) |
| 43 | +- `args`: array of child nodes (for binary/ternary operators like `and_v`, |
| 44 | + `or_b`, `andor`) |
| 45 | +- `subs`: array of child nodes (for `thresh`) |
| 46 | + |
| 47 | +Values are kept as strings during parsing; numeric validation happens in the |
| 48 | +analyzer and compiler. |
| 49 | + |
| 50 | +Example input and shape: |
| 51 | + |
| 52 | +``` |
| 53 | +and_v(v:pk(A),after(10)) |
| 54 | +
|
| 55 | +{ |
| 56 | + type: 'and_v', |
| 57 | + args: [ |
| 58 | + { type: 'v', arg: { type: 'pk_k', key: 'A' } }, |
| 59 | + { type: 'after', value: '10' } |
| 60 | + ] |
| 61 | +} |
| 62 | +``` |
| 63 | + |
| 64 | +Other examples: |
| 65 | + |
| 66 | +- AST shape (summary): |
| 67 | + |
| 68 | +``` |
| 69 | +Node := |
| 70 | + { type, ... } |
| 71 | +
|
| 72 | +type in: |
| 73 | + - "0" | "1" |
| 74 | + - pk_k | pk_h (key) |
| 75 | + - after | older (value) |
| 76 | + - sha256 | hash160 | ... (value) |
| 77 | + - multi | multi_a (k, keys[]) |
| 78 | + - thresh (k, subs[]) |
| 79 | + - and_v/or_b/... (args[2]) |
| 80 | + - andor (args[3]) |
| 81 | + - a/s/c/d/v/j/n (arg) |
| 82 | +``` |
| 83 | + |
| 84 | +- Base nodes: `0`, `1`, `pk_k`, `pk_h`, `multi`, `multi_a`, `sha256`, `after`, |
| 85 | + `older`, `thresh`, `and_v`, `or_b`, `andor`, etc. |
| 86 | +- Wrapper nodes: `a`, `s`, `c`, `d`, `v`, `j`, `n` as unary nodes with `arg`. |
| 87 | +- Syntactic sugar is expanded during parsing: |
| 88 | + - `pk(x)` -> `c:pk_k(x)` |
| 89 | + - `pkh(x)` -> `c:pk_h(x)` |
| 90 | + - `and_n(x,y)` -> `andor(x,y,0)` |
| 91 | + - `t:`/`l:`/`u:` wrappers expand to `and_v`/`or_i` forms (so they never |
| 92 | + appear as `type` values) |
| 93 | + |
| 94 | +The AST is intentionally simple so it can be shared by the compiler and the |
| 95 | +static analyzer. |
| 96 | + |
| 97 | +## Type system overview |
| 98 | + |
| 99 | +The static type system mirrors the Miniscript specification: |
| 100 | + |
| 101 | +- **Correctness**: basic type (B/V/K/W), z/o/n input modifiers, dissatisfiable |
| 102 | + flag and unit output. |
| 103 | +- **Malleability**: signed (`s`), forced (`f`), expressive (`e`), plus derived |
| 104 | + `nonMalleable`. |
| 105 | + |
| 106 | +These rules are encoded in `src/compiler/correctness.ts` and |
| 107 | +`src/compiler/malleability.ts` and are pure functions that take child types and |
| 108 | +return a parent type (or an error). |
| 109 | + |
| 110 | +### Correctness fields |
| 111 | + |
| 112 | +Correctness is tracked as a small record with these fields: |
| 113 | + |
| 114 | +- `basicType`: one of `B`, `V`, `K`, `W` (boolean, verify, key or wrapped output). |
| 115 | +- `zeroArg`: `z` modifier (consumes exactly 0 stack elements). |
| 116 | +- `oneArg`: `o` modifier (consumes exactly 1 stack element). |
| 117 | +- `nonZero`: `n` modifier (top input is never required to be zero). |
| 118 | +- `dissatisfiable`: whether the fragment has a valid dissatisfaction (dsat). |
| 119 | +- `unit`: whether the fragment leaves exactly one stack element (`u`). |
| 120 | + |
| 121 | +These fields are combined by the correctness rules (for example, `or_b` requires |
| 122 | +both children to be dissatisfiable and produces a `B` output). |
| 123 | + |
| 124 | +Context differences: in Tapscript, `d:X` gains the `unit` (`u`) property because |
| 125 | +`SCRIPT_VERIFY_MINIMALIF` enforces exact 0/1 encoding for IF. |
| 126 | + |
| 127 | +### Malleability fields |
| 128 | + |
| 129 | +Malleability uses the Miniscript `s/f/e` properties from the |
| 130 | +"Guaranteeing non-malleability" section of the spec: |
| 131 | + |
| 132 | +- `signed`: every satisfaction requires a signature. |
| 133 | +- `forced`: every dissatisfaction requires a signature (or none exist). |
| 134 | +- `expressive`: a unique unconditional dissatisfaction exists and any |
| 135 | + conditional dissatisfactions require signatures. |
| 136 | +- `nonMalleable`: derived from the spec's "Requires" column to guarantee a |
| 137 | + non-malleable satisfaction exists. |
| 138 | + |
| 139 | +## Correctness vs malleability |
| 140 | + |
| 141 | +Correctness properties answer "is this miniscript well-typed and semantically |
| 142 | +valid?" They ensure fragments are used in the right context (B/V/K/W rules), |
| 143 | +require the right kind of stack input and preserve intended meaning. Without |
| 144 | +correctness, a miniscript may compile to ASM but no longer represent the policy |
| 145 | +it claims (for example, an `or_b` that behaves like `and`). |
| 146 | + |
| 147 | +Malleability properties answer "if it is valid, can it be spent without |
| 148 | +malleable witnesses?" They are only meaningful after correctness passes. |
| 149 | + |
| 150 | +In code, correctness and malleability rules live side-by-side in |
| 151 | +`src/compiler/correctness.ts` and `src/compiler/malleability.ts`. Correctness |
| 152 | +helpers return `{ ok, correctness, error? }` and malleability helpers return |
| 153 | +`signed/forced/expressive` plus `nonMalleable`. Both are applied in |
| 154 | +`src/compiler/analyze.ts` during `analyzeNode`. |
| 155 | + |
| 156 | +## Analysis pass |
| 157 | + |
| 158 | +`src/compiler/analyze.ts` walks the AST and computes: |
| 159 | + |
| 160 | +- **Type information** via the type rules. |
| 161 | +- **Timelock mixing** via `TimelockInfo` and the combine functions. |
| 162 | +- **Duplicate keys** by merging key sets from child nodes. |
| 163 | + |
| 164 | +`analyzeParsedNode` converts those results into: |
| 165 | + |
| 166 | +- `issanesublevel`: requires signature, non-malleable, no timelock mixing, |
| 167 | + and no duplicate keys. |
| 168 | +- `issane`: `issanesublevel` plus top-level `B` type requirement. |
| 169 | + |
| 170 | +The analysis returns a short, human-readable error message (for example, |
| 171 | +`sane: malleable satisfactions possible.`) to help with debugging. |
| 172 | + |
| 173 | +## Timelock mixing |
| 174 | + |
| 175 | +Timelocks are tracked by `TimelockInfo`: |
| 176 | + |
| 177 | +- `after()` sets CLTV height/time flags. |
| 178 | +- `older()` sets CSV height/time flags (via `bip68`). |
| 179 | + |
| 180 | +The combine rules follow the spec: |
| 181 | + |
| 182 | +- For disjunctions (`k=1`), timelock info is unioned. |
| 183 | +- For conjunctions (`k>1`), incompatible height/time combinations set |
| 184 | + `contains_combination` to mark timelock mixing. |
| 185 | + |
| 186 | +## Satisfier integration |
| 187 | + |
| 188 | +The satisfier runs the static analysis first. If `issane` is false, it throws: |
| 189 | + |
| 190 | +``` |
| 191 | +Miniscript <expr> is not sane. |
| 192 | +``` |
| 193 | + |
| 194 | +By default, unknown satisfactions are pruned unless `computeUnknowns` is |
| 195 | +enabled. When `computeUnknowns` is true, the satisfier keeps solutions that |
| 196 | +contain unknown signatures or preimages and surfaces them via `unknownSats`. |
| 197 | +Enumeration is capped by `maxSolutions` (default 1000), which counts every |
| 198 | +derived solution including dsats and intermediate combinations; set |
| 199 | +`maxSolutions: null` to disable the cap. Raw analysis errors are attached to |
| 200 | +`err.cause` for debugging. |
| 201 | + |
| 202 | +## Extending the analyzer |
| 203 | + |
| 204 | +When adding a new fragment, update all four layers: |
| 205 | + |
| 206 | +1. **Parser**: add a case in `parse.ts`. |
| 207 | +2. **Compiler**: add ASM generation in `compile.ts`. |
| 208 | +3. **Type system**: add correctness and malleability rules in |
| 209 | + `src/compiler/correctness.ts` and `src/compiler/malleability.ts`. |
| 210 | +4. **Analyzer**: add a case in `analyze.ts` and merge keys/timelocks. |
| 211 | + |
| 212 | +This keeps compile, analyze and satisfy behavior consistent. |
0 commit comments