droidsaw-lean

Lean 4 proofs of decompiler invariants for droidsaw. The Rust side carries the type-system lints, fuzz targets, and Kani harnesses; Lean carries the statements that require quantifying over all possible inputs or all possible CFG shapes — territory bounded model checking can't reach.

20 proved theorems. No sorry, no axiom, no executable code.

This is a Lake workspace (lakefile.lean); it is not in the Rust dependency graph and not loaded by any sibling crate at build time.

What's proved

20 theorems across 6 source files. Per-file counts reproducible via grep -cE '^(theorem|lemma)' Droidsaw/**/*.lean (see "Verify locally" section below).

A seventh file, Droidsaw/Common/Graph/Spec.lean, holds the relational definitions every graph theorem is stated over (CFG, CFG.acyclic, Dominates, PostDom, Path) and declares no theorems itself.

File	Theorems	What it proves
Droidsaw/Apk/AXML.lean	3	axml_parse_terminates, axml_total, axml_rejects_escher. Chunk-walk terminates; parser returns ok or err on any byte list; parse result is acyclic (no element is its own descendant). Backs droidsaw_apk::binary_xml::BinaryXml::decode.
Droidsaw/Common/Graph/Path.lean	6	Path.vertices_nonempty, Path.vertices_head, Path.endpoint_mem, Path.source_mem, Path.append_vertices, Path.split_vertices_sub. Path-structure lemmas used by the dominator and post-dominator proofs.
Droidsaw/Common/Graph/Dominators.lean	6	Dominates.refl, Dominates.entry, Dominates.trans, Dominates.antisymm, Dominates.total, immediate_dom_unique. The dominator relation is a partial order; immediate dominators are unique. Backs dominators_with_rpo in droidsaw-common. CHK algorithm soundness is checked in debug builds by debug_assert!(rpo[0] == entry) and in both build modes by fuzz and naive-oracle differential testing, not by a theorem here.
Droidsaw/Common/Graph/PostDom.lean	3	PostDominates.refl, PostDominates.antisymm, immediate_postdom_unique. The inductive PostDom.node / PostDom.exit type in Spec.lean replaces the Rust implementation's u32::MAX sentinel by construction. Backs post_dominators_with_virtual_exit in droidsaw-common.
Droidsaw/Common/Lattice.lean	1	propagation_monotonic. A monotone operator iterated from ⊥ produces an ascending chain. Backs resolve_consts in droidsaw-dex and the Hermes SSA taint tracker.
Droidsaw/Hermes/CatchRPO.lean	1	catch_after_try. The catch handler appears after the try-region blocks in any RPO that satisfies IsRPO. Backs the exception-edge ordering in droidsaw-hermes cfg.rs.

Lean ↔ Rust correspondence

The Lean side establishes that the algorithm has the property. The Rust side establishes that the implementation is the algorithm — verified independently by #![deny(clippy::unwrap_used, ...)], fuzz targets, fixture ratchets, and Kani. Each .lean file names the Rust function it backs in a header comment (look for RUST: lines). Correspondences are maintained by hand; when a Rust invariant changes, the relevant .lean file is updated.

Lean ↔ Kani migration

When a statement here fits Kani's bounded reach, the Lean file is retired and the obligation moves to a Kani harness in the consuming Rust crate. Past migrations include signing-block constants and MUTF-8 / SSA codec roundtrips.

A second retirement path applies to theorems that turn out to be tautologies over placeholder models — proofs over empty-list stand-ins, sorry-stubbed obligations, statements of type True := trivial. Those are deleted outright; the invariant stays on the Rust side, enforced by the type system, the call graph, or a runtime gauge.

Verify locally

cd droidsaw-lean
lake build                                      # build every theorem
lake build Droidsaw.Common.Graph.Dominators     # one module

Cold build downloads Mathlib (~800 compilation jobs); subsequent builds are incremental.

Per-file theorem count, reproducible:

for f in Droidsaw/**/*.lean; do
  echo "$f $(grep -cE '^(theorem|lemma)' "$f")"
done

Toolchain

Pinned at leanprover/lean4:v4.29.0 (lean-toolchain). Mathlib pinned to the matching v4.29.0 tag in lakefile.lean. Both pins move together or not at all.

Layout

droidsaw-lean/
├── lakefile.lean                 Lake package + Mathlib v4.29.0 pin
├── lean-toolchain                leanprover/lean4:v4.29.0
├── Droidsaw.lean                 root index — imports every module below
└── Droidsaw/
    ├── Apk/
    │   └── AXML.lean
    ├── Common/
    │   ├── Graph/
    │   │   ├── Spec.lean          relational definitions
    │   │   ├── Path.lean
    │   │   ├── Dominators.lean
    │   │   └── PostDom.lean
    │   └── Lattice.lean
    └── Hermes/
        └── CatchRPO.lean

License

BSD-3-Clause.