# Claims and caveats

All empirical statements below are about the retained specimens, tool builds, flags, models and budgets. PASS is not universal correctness. Every row supplies evidence; the prohibited phrasing deliberately illustrates an overclaim.

| Safe formulation | DO NOT SAY | Evidence / qualification |
| --- | --- | --- |
| The 68 planned showcase matrix conditions linked as x64 PE and passed their canonical run checks. | All programs produced by these obfuscators are correct. | [Matrix scope and commands](assets/reports/showcase_matrix_v1.md). BinProtect and backend/MIR were not part of these 68 conditions. |
| Annotation-only SUB pilots for the tested OLLVM/Hikari compilers compiled without transforming the target; retained builds used global flags. | Hikari's retained matrix used validated function-local annotations. | [Selective targeting result](assets/reports/showcase_matrix_v1.md). Hikari flags: `-enable-subobf`, `-enable-bcfobf`, `-enable-cffobf`, `-enable-splitobf`, each via `-mllvm`. This does not prove annotation support is impossible in every Hikari build. |
| All 24 intended OLLVM SUB O0 sites expanded in retained IR, but native XOR/SUB operations were already recognizable; higher optimization recovered all 24 intended native operations. | IR expansion guarantees difficult machine code, or msynth recovered operations already simplified before it ran. | [Arithmetic study](assets/reports/msynth_validation.md), [optimization](assets/reports/optimization_survival.md). Coverage, template diversity and persistence are separate. |
| The exact Polaris MBA O0 target grows from 115 to 678 native instructions. | Polaris is universally stronger than every other obfuscator. | [Metric definitions](assets/tables/research/selected_metrics.md). Named target and matched compiler baseline; not whole-PE size or a hardness proof. |
| The extended isolated-site synthesis probe accepted 10/12 recoveries after SMT checks; two were UNKNOWN. | Synthesis solved the corpus, or UNKNOWN means equivalent. | [Synthesis expansion](assets/evidence/complex_arithmetic_v1_summaries/synthesis_expansion.json). Keep this separate from complete-function tests. |
| No complete recovery occurred among 20 extracted obfuscated complex-return expressions in the tested AST/SiMBA paths; useful partial reductions occurred. | Composed MBA is impossible to simplify. | [Complex arithmetic](assets/reports/complex_arithmetic_deobfuscation.md), [family results](assets/evidence/complex_arithmetic_v1_summaries/family_results.json). Four Polaris MBA extractions hit a flag-AST guard; these are extraction limits, not failed SMT equivalence queries. |
| Hikari O0 BCF injected conditional gates were folded before native predicate analysis; the four surviving Jccs were genuine. | Triton removed Hikari's injected O0 gates. | [Triton study](assets/reports/opaque_predicate_triton.md). Source/IR provenance separates injected versus genuine conditions. Hikari's exact BCF IR text also has legacy mixed-pointer syntax; direct compilation worked, reparsing did not. |
| All 22 tested OLLVM O0 and 16 Polaris O0 injected gates were proved one-sided by the retained generic Triton workflow. | Triton can remove all opaque predicates. | [Triton report](assets/reports/opaque_predicate_triton.md), [summary](assets/evidence/triton_summaries/family_results.json), [one frozen proof](assets/evidence/s03_ollvm_bcf/first_gate_proof/result.json). Bounded exploration, supported memory semantics and recorded prefix coverage matter. |
| Under path prefix P, UNSAT for P ∧ not-C rules out that branch direction for states covered by P and the model. | One path-local UNSAT result establishes a global invariant for every program execution. | [Proof methodology](assets/reports/opaque_predicate_triton.md). Require feasible/reachable context and coverage of relevant prefixes. SAT gives a model; TIMEOUT/UNKNOWN is not proof. |
| Tigress O0's three injected gates became provable after importing one captured initialized state while x/y remained symbolic. | Tigress predicates are universally opaque for arbitrary global state. | [Generic result](assets/evidence/support_tigress_opaque/o0/result.json), [initialized result](assets/evidence/support_tigress_opaque/o0_initialized/result.json), [state](assets/evidence/support_tigress_opaque/o0_initialized/initialized_state.json). Generic yield 0/3; initialized 3/3. Allocation, entropy, heap layout and subsequent mutations are not universally quantified by this model. |
| A separate proof consumer rewrote the 22/16 gates as JMP plus padding; all retained canonical and 9,189 native differential triples matched. | Triton's proof automatically produces a fully deobfuscated PE, or tests prove all inputs. | [OLLVM validation](assets/evidence/s03_ollvm_bcf/validation.json), [Polaris validation](assets/evidence/s07_polaris_bcf/validation.json), [rewrite report](assets/reports/opaque_predicate_rewrite.md). Analysis and rewriting are distinct steps. |
| Audited entry-reachable BCF blocks fall 70→37 for OLLVM and 54→30 for Polaris; physical bytes and predicate arithmetic remain. | All dead code was deleted, or an unchanged file size means no deobfuscation happened. | [OLLVM projection notes](assets/evidence/s03_ollvm_bcf/projection_notes.json), [Polaris notes](assets/evidence/s07_polaris_bcf/projection_notes.json). These CFGs do not split calls; Miasm's FLA counts do. |
| Stock ollvm-unflattener produced working canonical rewritten PEs for the selected OLLVM-16 O0 and Hikari O0 specimens. | Stock ollvm-unflattener generically supports all OLLVM-family flattening. | [OLLVM result](assets/evidence/s04_ollvm_fla/stock_result.json), [Hikari result](assets/evidence/support_hikari_fla/stock_result.json). 25/25 and 28/28 successor pairs; graph-pair scores do not prove branch polarity or every runtime behavior. O2 results differ. |
| Polaris's stock O0 FLA rewrite is WRONG despite a smaller 10-block graph. | Polaris FLA was successfully deobfuscated. | [Stock result](assets/evidence/s05_polaris_fla_wrong/stock_result.json), [wrong output](assets/evidence/s05_polaris_fla_wrong/output_runtime_stdout.txt): F9CD8332 instead of DBEFFCE7; exit 1. Legitimate switch alternatives become sequential operations. Static negative example only. |
| Stock Tigress Flatten discovery saw 6 blocks where the jump-table-aware reference has 38; no successful rewrite followed. | Tigress was reduced to six blocks, or the SMT solver failed to understand its semantics. | [Discovery result](assets/evidence/s08_tigress_flatten/stock_result.json), [verified table](assets/evidence/s08_tigress_flatten/verified_jump_table.json). Failure occurred before useful symbolic successor recovery. |
| RPISEC's SSA def/use approach was inspected as an alternative methodology. | RPISEC was executed successfully on this corpus, or would fix Polaris automatically. | [Methodology section](assets/reports/unflattening_validation.md). No Binary Ninja plugin run is claimed. |
| Mergen emitted verifier-valid, recompilable LLVM IR for all 17 selected cases at four retained stages (68 modules). | Verifier-valid lifted IR is semantically correct. | [Mergen study](assets/reports/mergen_validation.md), [totals](assets/evidence/mergen_summaries/totals.json). Thirteen cases had passing runtime outcomes under their contracts; two BCF lifts were not run and BinProtect stayed static-only. |
| Mergen's lift of the valid native OLLVM SUB specimen is SEMANTIC FAILURE in all four stages. | OLLVM SUB's original executable is wrong, or ordinary LLVM O2 introduced the lifting bug. | [Mismatch record](assets/evidence/s01_ollvm_sub/mergen/semantic_result.json): 3,917/4,118 mismatches per stage; raw lift already wrong; x=0 expects 0x08083808 but gives 0. |
| The retained Polaris MBA lift passes 4,118 vectors per stage yet retains substantial MBA (359 M2 IR instructions). | Mergen recovered clean source or rewrote the original PE. | [Semantic result](assets/evidence/s02_polaris_mba/mergen/semantic_result.json), [IR metrics](assets/evidence/s02_polaris_mba/mergen/ir_metrics.json). R→R2 and R→M→M2 are alternative paths, not one four-stage chain. |
| All eight tested BinProtect protected outputs failed runtime validation by crash or hang. | BinProtect provides a working runnable course lane, or its static expansion proves superior protection. | [BinProtect report](assets/reports/binprotect_validation.md). No protected BinProtect PE included. Virtualization was intentionally not tested. |
| Original PDB identifiers can survive rewriting while instruction mappings become stale. | Matching RSDS GUID/age proves original PDB mappings remain correct inside rewritten functions. | [Rewrite metadata audit](assets/evidence/s03_ollvm_bcf/metadata_audit.json), [unflattening report](assets/reports/unflattening_validation.md). No PDBs are included; use exports/RVAs and distinguish ordinary execution from unwind guarantees. |
| Optimization level changes both treatment survival and recovery-tool behavior. | Every O0 result transfers to O2, or cross-compiler counts form a fair leaderboard. | [Optimization](assets/reports/optimization_survival.md), [boundary correction](assets/reports/obfuscator_comparison_summary.md). Historical next-export measurements can overrun target boundaries; Tigress /Ox clean is 106 instructions, not the older O2 overcount. |
| Some retained seeded probes repeated identically; Polaris MBA/MIR and whole Tigress generated files did not reliably reconstruct from seed alone. | A seed is a complete reconstruction key for all passes. | [Polaris validation](assets/reports/polaris_validation.md), [Tigress validation](assets/reports/tigress_validation.md). Preserve exact artifacts and hashes. |
| Screenshots illustrate the graph/instruction views actually visible, with two explicitly held identity mismatches. | Filename, diff colour or visual similarity proves binary identity or semantic equivalence. | [Visual index](VISUAL_INDEX.md). Exact screenshot capture tool version/database hashes were not supplied. |

## Scope checklist for every future page

Name the specimen and optimization level; identify representation and metric convention; link retained evidence; state relevant input/state assumptions; distinguish SAT, UNSAT and UNKNOWN; identify whether a PE was actually produced and validated. Do not imply external paper results were reproduced here. Keep future virtualization/devirtualization discussion brief and clearly outside the measured corpus.