Mirrorshard: Proof by computational reflection with verified hints

We describe a method for building composable and extensible ver-ification procedures within the Coq proof assistant. Unlike tradi-tional methods that rely on run-time generation and checking of proofs, we use verified-correct procedures with Coq soundness proofs. Though they are internalized in Coq’s logic, our provers support sound extension by users with hints over new domains, en-abling automated reasoning about user-defined abstract predicates. We maintain soundness by developing an architecture for modular packaging, construction, and composition of hint databases, which had previously only been implemented in Coq at the level of its dy-namically typed, proof-generating tactic language. Our provers also include rich handling of unification variables, enabling integration with other tactic-based deduction steps within Coq. We have imple-mented our techniques in MirrorShard, an open-source framework for reflective verification. We demonstrate its applicability by in-stantiating it to separation logic in order to reason about imperative program verification. 1