touhou-formal

If operating systems get formal verification, Gensokyo gets an executable specification.

The bullets are already formal. The VM should be, too.

touhou-formal is a formal-methods workbench for Touhou script VMs, starting with the ECL VM family in TH06, TH07, and TH08.

This is not a “write a safer clone of ZUN’s VM” project. The point is sharper: model the original VM, including its oddities, missing checks, historical drift, and crashable edges, closely enough that Lean + SMT/symbolic execution can produce real counterexamples for properties the retail games do not satisfy.

Fuzzing is still useful. But danmaku scripts have tiny weird gates everywhere: time checks, difficulty masks, operand flags, subroutine stacks, selector fallbacks, host-state-dependent operands, and version-specific dispatch. Random mutation can spend a lot of time proving that fairies still shoot bullets. A solver can instead ask: “is there any byte-realizable ECL instruction that passes the VM’s own gates and reaches this exact bad boundary?”

That is the intended loop:

1. recover the original source-backed semantics;
2. encode the shared VM core once;
3. let SMT produce witnesses instead of hand-picking examples;
4. replay the witness through Lean’s executable model;
5. validate high-value counterexamples against retail builds in isolation.

Current slice

The executable model currently covers these source-backed boundaries:

• TH06 raw bytes flow through the shared ECL loader, timeline-prefix decoder, and CallEclSub lookup to reproduce the arg0 = 256 subTable fault.
• TH07 and TH08 reuse the same lookup semantics while preserving their negative-sub-id policy difference.
• Loader and cursor checks expose first missing-byte, zero-size, and before-buffer boundaries as executable theorems.
• Timeline size and raw instruction nextOffset cursor sweeps are generated from shared profile widths, so TH08's unsigned timeline-size delta is recorded without title-local search logic.
• Raw ECL difficulty-mask semantics are modeled as profile policy; TH08's override-mask rule is proven distinct from the TH06/TH07 active-bit intersection rule.
• Shared integer operand resolution covers TH06's always-GetVar behavior and TH07/TH08 operandFlags mask branches, including known selector fallthrough to raw immediates.
• Shared scalar assignment semantics cover SET_INT/SET_FLOAT across TH06/TH07/TH08, including TH06's source-level SetVar type guard and the TH07/TH08 opcode-specific int/float lvalue split.
• Shared integer unary-update semantics cover INC/DEC, including TH06's direct GetVar(..., NULL) pointer write path where unknown outputs update the raw operand cell instead of becoming a SetVar no-op.
• Shared integer binary-op semantics cover ADD/SUB/MUL/DIV/MOD over title-profiled operand layouts, including output lvalue resolution, TH08 in-place arithmetic, resolver-driven zero divisors, and signed INT_MIN / -1 idiv overflow.
• Shared float binary-op semantics cover ADD/SUB/MUL/DIV/MOD dispatch, title-profiled operand layouts, output lvalue resolution, and resolver behavior for TH06/TH07/TH08. Lean records lhs/rhs/result bit patterns; exact IEEE-754/fmod solving is a later SMT boundary, not claimed here.
• Shared float-function semantics cover TH06/TH07 atan2f, TH08 VectorAngle, TH07/TH08 sinf/cosf, and angle normalization. The profile preserves TH06's unusual GetVar-pointer read followed by SetVar, while transcendental result bits remain an explicit host/SMT float-theory boundary.
• Shared special-numeric semantics covers nine self-position, LERP, polar-to-Cartesian, and distance opcodes, preserving repeated resolver reads and two-output write order. A separate shared 8-slot interpolation model covers TH07/TH08 installation, including IEEE signed-zero/NaN matching, no-free-slot suppression, and unchecked 8-entry callback-table indexing.
• Shared bullet command/transform semantics covers TH07's six-entry legacy command table and TH08's 18-entry transform table. The table index is resolved and checked first, so an unchecked out-of-range source write faults before later operands are read; valid writes retain raw 32-bit kind values and title-specific record fields.
• Shared random-value semantics cover integer range/modulo, range-plus-addend, repeated-bound float ranges, and parity-selected sign opcodes. Integer results use explicit 32-bit word arithmetic; float RNG results stay at the host/SMT boundary. TH06 preserves the extra SetVar RHS lookup that can reinterpret generated result bits as an ECL selector, while TH07 opcode 51 preserves both occurrences of its lower-bound resolver read.
• The first gameplay host-effect family covers 24 immediate movement opcodes: position, axis/polar velocity, angular velocity, speed, acceleration, player-relative motion, and movement bounds. Shared effects retain title differences such as TH06's raw player-angle offset/bounds, TH07's derived axis angle, and TH08's forced-zero Z plus timer-reset behavior.
• Timed movement adds 20 more opcode bodies through one consecutive-family semantics: TH06's opcode-selected easing ranges and TH07/TH08's operand-selected direction/position interpolation. The model retains every repeated resolver call, three-bit easing writes, mirror-X sign toggling, position-versus-world-position origins, and the nonpositive-duration fast paths—including exact timer subframe/history resets, TH08's distinct timer policies, opcode 69's player-relative/absolute-angle branch split, and the host-derived angles used by TH08 opcodes 67 and 178 without inventing synthetic bytecode reads.
• Shared orbit semantics adds nine opcode bodies: TH07's full orbit, radius/angle updates, and three movement-timer mode setters; plus TH08's full orbit, orbit-from-current-position, and velocity update. Profiles retain TH08's X/Y-only origin write for opcode 72 and the exact timer reset state.
• Random-direction semantics covers TH06's raw range moves, TH07's two exit angle helpers, and their TH08 counterparts. One profile parameter preserves whether a right-wall reflection subtracts the generated candidate or the enemy's old angle; ordered binary32 guards reject NaNs exactly like the C++ comparisons. TH08 host-derived directions compose directly into the shared timed-movement transition, with a profile-drift check between both stages.
• Shared enemy-state effects cover 24 hitbox, collision/damage flag, death-mode, life, and boss-timer opcodes. The model retains TH06/TH07 bitfield truncation, TH08's inverted replace-mask rules, alignment-effect collision mirroring, the high-opcode presentation-write guard, title-specific life operand resolution/gauge effects, and exact timer-history reset writes.
• Shared enemy-lifecycle effects cover eight spawn/remove opcodes. The model keeps the source spawn packet order, TH06 raw-i16 life/item fields, TH07/TH08 operand-flag resolution, parent-life spawn suppression before operand reads, relative-position host f32 addition as an explicit boundary, context-argument copying policy, i16 sub-id truncation at CallEclSub, i8 item-drop truncation in TH07/TH08, and the three distinct remove-all loop policies.
• Shared item/drop effects cover 10 cross-title opcodes. The model records raw-versus-resolved item counts and item ids, TH06's 144/72 random spread, TH07/TH08's 128/64 spread, the power-under-128 branch that selects power items versus point items, point-only loops, single-item spawns, and TH08's item-drop state fields without simulating the full ItemManager.
• Shared boss/spellcard lifecycle effects cover 21 cross-title opcodes. The model records unchecked bosses[8] slot writes, TH08's u8 bossSlot truncation after the full-int array access, primary-slot-only GUI presence in TH08, legacy TH06/TH07 spellcard start/end state, TH08 StartSpell/EndSpell host calls, boss gauge ratios, life-marker side effects, timeout/survival flags, boss run-interrupt writes, and TH08 spellcard effect/bonus control flags without expanding the full GUI/Spellcard/Catk runtimes.
• Shared host-effect semantics cover 15 sound, particle, tracked-effect, color, and alignment opcodes. Profiles preserve raw versus resolved operands while the executable boundary exposes TH06's 12-slot and TH07/TH08's 24-slot effect-pointer arrays, the two 28-entry color tables, TH07's unchecked specialEffect dereference, and TH08's alignment-effect interrupt policy.
• Shared shooting-control effects cover 18 interval, gate, previous-pattern, and offset opcodes. One rank-scaling function is reused across all titles, while profiles retain TH06's unconditional zero-interval timer reset, TH07/TH08's nonzero guard, TH08's defer-versus-suppress gate meaning, and TH08's forced-zero offset Z.
• Shared time-control effects cover VM-local no-op advance, context-time addition, context wait timers, TH08 secondary-time waits, and global stage-script waits. The wait gate is modeled separately from opcode bodies: TH07 and TH08 decrement the timer and pre-tail context time, then the normal frame tail restores script time, giving a net stall without fusing scheduler and opcode semantics.
• Shared bullet-control effects cover 13 cross-title opcodes: TH06's point conversion, TH07 item/no-item/radius removal, TH08 transition/world-radius/ mode-4 clearing, sound flag toggles and overrides, and bullet-rank influence writes. The model preserves TH06 raw operands, TH07/TH08 operandFlags resolution, repeated primary sound reads before override reads, and signed-i16 count truncation.
• Shared laser-spawn descriptor effects cover the six fixed/aimed laser spawn opcodes. They preserve title-specific descriptor targets, position sources, shifted TH07/TH08 operand flags, 16-bit sprite/color storage, spawn requests, and the unchecked selected-slot pointer write that happens after SpawnLaserPattern.
• Shared laser slot controls cover 29 cross-title opcodes for selected-slot writes, indexed angle/position/start-length/offset/hide updates, active-state tests, stop transitions, and clear-all loops. The model preserves unchecked enemy laser pointer-slot reads, null-pointer guards that suppress later operand reads, TH06's non-normalized angle add, TH07/TH08 stop-width copies, and TH08's inverted in-use test value.
• Shared animation-control effects cover 29 ECL/ANM bridge opcodes: TH06/TH07 primary enemy script selection, cross-title packed move/death animation fields, raw bitfield auto-rotation, primary VM interrupts, TH07/TH08 primary rotation-Z writes, TH08's primary/alternate script-table bank policy, and unchecked secondary VM slot accesses. The model records host ANM calls, table writes, slot clears, secondary interrupts, high-index diagnostics, and negative/high slot faults without executing the ANM VM itself.
• One consecutive-family profile now covers all 27 primary bullet-pattern opcodes (nine aim modes per title). The shared effect preserves packed-i16 type/color reads, shifted resolver bits, i16 count writes, spellcard rank bypass, binary32 zero/minimum-speed tests, and descriptor-versus-spawn ordering. TH08 additionally exposes dead/defer/alignment/distance exits and records its unchecked fixed 0x2c-byte pending-instruction copy boundary.
• Shared callback-configuration effects cover 18 death/life/timer/periodic opcodes. They retain raw-width versus resolved operands, exact timer resets, TH08 presentation suppression, unchecked four-slot life arrays, and repeated index resolution—so an RNG selector can produce a successful threshold write followed by a second-index fault instead of being silently memoized.
• Shared interrupt effects cover each title's table-write, immediate-run, and stack-disable opcodes. They preserve unchecked table accesses, TH08 signed i16 storage, context-advance/save ordering, subTable policy, and the original asymmetry where a disabled save still permits stack-depth increment.
• Shared extension-dispatch semantics covers immediate and per-frame EX instruction opcodes in all three titles. It preserves the 17/24/32-entry callback-table bounds, TH06 raw indices, TH07/TH08 resolver reads, negative callback clearing, repeated condition/table-index reads, and the boundary between callback installation and later scheduler execution.
• TH08 child-ECL block installation models its unchecked four-slot pointer table, old-block release, allocator failure, full 0x24b0 zeroing, repeated sub-id resolution, i16 CallEclSub conversion, partial state before lookup faults, and the exact 0x78-byte variable-region copy. Multi-context frame scheduling remains a separate transition layer.
• One miscellaneous state-control family closes 29 small but nontrivial handlers across the three titles: raw bitfield/u8/i16 stores, ZunTimer assignment, trail-strip division, TH06 stage unpause, TH07 cherry requests, and TH08 background, pause-mode, GUI, minimum-distance, and signed-i8 clock behavior. Partial trail writes survive a zero-stride fault, exactly as in the source.
• TH08 cross-enemy boss dispatch models opcodes 88/89 through the unchecked bosses[8] table, including null behavior, repeated index resolution, mutation of the target boss's active instruction/call stack, i16 subroutine conversion, partial CallEclSub faults, and pending-sub writes.
• TH08 linked-child opcodes 90--92 share one constructor semantics. It records attachment-tail traversal (including a nonterminating chain), parent-state spawn suppression, the 480-slot child request and 0x78 context copy, three distinct player-alignment reads, effect allocation/null behavior, chain links, inherited positions, and the unconditional spawn sound.
• The source-surface audit now maps every named/case-labeled raw ECL opcode to an explicit profile family: TH06 136/136, TH07 159/159, and TH08 184/184. That is complete opcode-handler coverage, not a claim that BulletManager, EnemyManager, GUI, audio, rendering, ANM, or multi-frame scheduling has been reimplemented inside Lean; those remain explicit host boundaries.
• TH07 ECL_GET_BOSS_INT and TH08 low opcode 86 are modeled through one shared boss-indexed integer-read shape, including operand-flag bypass, bosses[8] index bounds, null boss pointers, and host/default selector resolution.
• The control-flow body includes JUMPDEC, integer conditional jumps, TH06 integer/float compare-register producers, and TH07/TH08 direct float conditional jumps. Float ordering explicitly includes IEEE unordered/NaN behavior; the older immediate/raw div/mod check remains as a regression beside the fuller integer-binary model.
• Plain CALL/RET stack behavior is modeled with shared semantics for stack saves/restores, depth guards, subTable lookup, and TH08 child-context RET exits.
• TH06 conditional CALL opcodes are modeled as guard predicates that reuse the same shared CALL stack/subTable body when taken.
• Raw ECL instruction prefixes and ANM entry headers are decoded through shared profile-driven code across TH06/TH07/TH08.

The Lean model treats the first invalid operation as a Fault. It does not try to predict arbitrary C++ undefined behavior after that point.

Repository layout

• TouhouFormal/Core/: byte/scalar reads, faults, evidence, and bounded transition-system definitions.
• TouhouFormal/ECL/: shared ECL profile, loader, lookup, timeline, and raw instruction-prefix semantics.
• TouhouFormal/ANM/: shared ANM entry profile and entry-header decoding.
• TouhouFormal/TH06/, TouhouFormal/TH07/, TouhouFormal/TH08/: title-specific profile facts, fixtures, and deltas.
• TouhouFormal/Search/: bounded checks and SMT bridges.
• docs/: modeling policy, source evidence, and roadmap notes.
• scripts/: reproducible local checks.

Commands

lake build
lake exe check
lake exe smt th06-sub-oob | z3 -in
lake exe smt th08-negative-noop-unsat | z3 -in
lake exe smt th08-timeline-size-before-buffer-unsat | z3 -in
lake exe smt th08-raw-difficulty-override-delta | z3 -in
lake exe symex list-paths
lake exe symex query th08 jumped-before-buffer 1 0 | z3 -in
lake exe symex query-values th08 jumped-before-buffer 1 0 | z3 -in
lake exe symex list-body-paths
lake exe symex query-body-values th08 int-divisor-zero 1 2 | z3 -in
lake exe symex list-int-resolver-paths
lake exe symex query-int-resolver-values th07 resolved-default-raw 0 | z3 -in
lake exe symex list-int-binary-paths
lake exe symex query-int-binary-values th08 int-binary-divide-overflow-resolved-host 1 0 | z3 -in
lake exe symex list-boss-int-paths
lake exe symex query-boss-int-values th08 boss-int-null-deref 1 0 | z3 -in
lake exe symex list-boss-float-paths
lake exe symex query-boss-float-values th07 boss-float-null-deref 1 0 | z3 -in
lake exe symex list-callret-paths
lake exe symex query-callret-values th08 ret-child-index-before-array 1 0 | z3 -in
lake exe symex list-condcall-paths
lake exe symex query-condcall-values th06 condcall-lookup-fault 1 0 | z3 -in
lake exe symex list-extension-paths
lake exe symex query-extension-values th08 extension-install-index-before-array 1 0 | z3 -in
./scripts/symex_raw_step.sh th08 1 2
./scripts/symex_materialize_raw_step.py th08 jumped-before-buffer 1 0
./scripts/symex_materialize_raw_step.py th06 jumped-before-buffer 8 0 --ecl-file
./scripts/symex_candidate_queue.py --env th06:8:0:retail-lunatic-bit3 --path jumped-before-buffer
./scripts/symex_materialize_body_step.py th08 all 1 2
./scripts/symex_body_candidate_queue.py
./scripts/symex_materialize_int_resolver.py th07 all 0
./scripts/symex_int_resolver_queue.py
./scripts/symex_materialize_int_binary.py th08 all 1 0
./scripts/symex_int_binary_candidate_queue.py
./scripts/symex_materialize_boss_int_read.py th08 all 1 0
./scripts/symex_boss_int_candidate_queue.py
./scripts/symex_materialize_boss_float_read.py th08 all 1 0
./scripts/symex_boss_float_candidate_queue.py
./scripts/symex_materialize_callret_step.py th08 all 1 0
./scripts/symex_callret_candidate_queue.py
./scripts/symex_materialize_condcall_step.py th06 all 1 0
./scripts/symex_condcall_candidate_queue.py
./scripts/symex_materialize_extension_step.py th08 all 1 0
./scripts/symex_extension_candidate_queue.py
python3 scripts/evaluate_symex_effectiveness.py
python3 scripts/run_ce_campaign.py --name local-full-symex-ce
./scripts/check.sh
./scripts/retail_inventory.sh
./scripts/extract_retail_th06.sh
python3 scripts/retail_confirm_th06_arg0_256.py --prepare-only
python3 scripts/retail_confirm_th06_raw_symex.py --symex-path jumped-before-buffer --prepare-only
python3 scripts/retail_confirm_boss_float_read.py th08 --symex-path boss-float-null-guarded-skip --prepare-only
python3 scripts/retail_confirm_ecl_symex.py th08 --family int-binary --symex-path int-binary-divide-overflow-raw-immediate --prepare-only
python3 scripts/retail_confirm_ecl_symex.py th07 --family callret --symex-path ret-stack-read-before-stack --force-next-offset 16 --prepare-only

scripts/check.sh runs the Lean build, executable counterexample check, Z3 controls, and the current raw-ECL symbolic witness materializer. The materializer solves a path, asks Lean to encode the witness into bytes from the shared title profile, decodes it again, and checks that the concrete step lands back in the requested path class. The body materializer does the same for the first opcode-body layer: JUMPDEC, integer conditional jumps, and immediate/raw integer div/mod zero-divisor faults. The resolver materializer covers integer rvalue operandFlags branches separately from opcode-body effects. The integer-binary materializer covers title-specific ADD/SUB/MUL/DIV/MOD layouts, output lvalue resolution, resolver-driven divisor faults, and signed idiv overflow. Scalar assignment, integer unary updates, float binary arithmetic, float functions, random-value opcodes, compare-register producers, direct float conditional jumps, immediate and timed movement effects, enemy-state effects, enemy-lifecycle effects, item/drop effects, boss/spellcard lifecycle effects, shooting-control effects, time-control effects, bullet-control effects, laser slot controls, laser-spawn descriptor effects, animation-control effects, bullet-pattern effects, callback-configuration effects, interrupt effects, miscellaneous state controls, cross-enemy boss dispatch, and linked-child construction currently have Lean executable controls for profile coverage and shared-step execution, but no dedicated solver/materializer lane yet. The extension-dispatch materializer covers TH06/TH07/TH08 immediate and per-frame EX callback-table reads, including TH07/TH08 repeated resolver-read install faults and negative-index callback clears. The boss integer-read materializer covers TH07/TH08 g_EnemyManager.bosses[index] reads, including solver-generated out-of-bounds and null-dereference counterexamples. The boss float-read materializer reuses that host boundary with float selector bit-pattern ranges and the TH07/TH08 null-policy split. The CALL/RET materializer covers stack write/read faults, subTable lookup faults, and TH08 child-context RET exits. The conditional-CALL materializer covers TH06 guard-false fallthrough and guard-true reuse of the same CALL stack/subTable body. scripts/evaluate_symex_effectiveness.py reruns the symbolic candidate queues and reports which modeled branches have solver/materializer coverage alongside the automatically derived source-opcode profile coverage. The current retained full campaign is formal_results/ce_campaigns/2026-09-02-extension-symex/summary.json: 328/328 candidates are satisfiable and replay-matched, with 209 high-priority counterexamples and 44 medium-priority semantic surprises. docs/symbolic-execution-roadmap.md records the current solver boundary and the next lane order. scripts/retail_inventory.sh is read-only and records archive hashes plus executable/data CRCs before any Wine validation. Retail validation scripts operate on isolated copies under /home/yann/yann/touhou/formal/retail_extract and the repository's ignored-by-default retail_validation/ tree. Small result.json and report.json evidence files in that tree are committed; retail game files, Wine prefixes, screenshots, and mutated payloads are not.

Current retained results are summarized in docs/formal-results.md. The current formal-vs-fuzz coverage assessment is in docs/effectiveness.md.