MirrorShard: Proof by Computational Reflection with Verified Hints

TL;DR

MirrorShard introduces a verified, extensible framework within Coq for automated reasoning about user-defined predicates, enhancing proof automation with sound extension capabilities and modular hint management.

Contribution

It presents a novel architecture for verified, composable proof procedures in Coq, supporting user-defined hints and integration with tactic-based deduction.

Findings

Implemented in MirrorShard, an open-source framework.

Successfully applied to separation logic for imperative program verification.

Supports sound extension and rich unification handling.

Abstract

We describe a method for building composable and extensible verification procedures within the Coq proof assistant. Unlike traditional 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, enabling 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 dynamically 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 implemented our techniques in MirrorShard, an open-source framework for reflective verification. We demonstrate its applicability by instantiating it to separation logic in order to reason about imperative program verification.