Homological Reentrancy Detection: A Complete Soundness and Completeness Proof for Topological Smart Contract Analysis

Abstract

We prove that first homology of the control flow graph provides a complete characterization of reentrancy vulnerability in smart contracts. Specifically, we establish the Homological Reentrancy Theorem: a contract admits a reentrant execution path if and only if H₁(G) ≠ 0, where G is the extended control flow graph incorporating external call returns. We prove soundness (no false negatives) and completeness (no false positives) for contracts satisfying a non-degeneracy condition. For multi-contract systems, we apply the Mayer-Vietoris exact sequence to compute H₁ of the composed system from individual components, enabling detection of cross-contract reentrancy. We validate empirically against 17 known exploits including The DAO (2016), Parity Wallet (2017), and Cream Finance (2021), achieving 100% detection with zero false positives.