Mechanised Hypersafety Proofs about Structured Data: Extended Version

TL;DR

This paper introduces LGTM, a Logic for Graceful Tensor Manipulation, a Hoare-style relational separation logic for hypersafety properties over structured data such as compressed and sparse tensor formats. LGTM supports parametrised hypersafety specifications whose arity can depend on program variables, enabling modular proofs of complex, loop-driven data-format manipulations; it is embedded in Coq with mechanised meta-theory and automated proof techniques. The authors demonstrate LGTM on 13 case studies, showing that relational proofs can be considerably shorter and more reusable than non-relational approaches, and provide empirical evidence of expressivity and automation benefits. The work offers a foundation for certifying domain-specific compilers for structured data and paves the way for automated, proof-producing verification of advanced data-format libraries.

Abstract

Arrays are a fundamental abstraction to represent collections of data. It is often possible to exploit structural properties of the data stored in an array (e.g., repetition or sparsity) to develop a specialised representation optimised for space efficiency. Formally reasoning about correctness of manipulations with such structured data is challenging, as they are often composed of multiple loops with non-trivial invariants. In this work, we observe that specifications for structured data manipulations can be phrased as hypersafety properties, i.e., predicates that relate traces of $k$ programs. To turn this observation into an effective verification methodology, we developed the Logic for Graceful Tensor Manipulation (LGTM), a new Hoare-style relational separation logic for specifying and verifying computations over structured data. The key enabling idea of LGTM is that of parametrised hypersafety specifications that allow the number $k$ of the program components to depend on the program variables. We implemented LGTM as a foundational embedding into Coq, mechanising its rules, meta-theory, and the proof of soundness. Furthermore, we developed a library of domain-specific tactics that automate computer-aided hypersafety reasoning, resulting in pleasantly short proof scripts that enjoy a high degree of reuse. We argue for the effectiveness of relational reasoning about structured data in LGTM by specifying and mechanically proving correctness of 13 case studies including computations on compressed arrays and efficient operations over multiple kinds of sparse tensors.

Figures (20)

• Figure 1: Structured matrix/vector multiplication.
• Figure 2: Sparse Vector and Unordered Compressed Sparse Row formats
• Figure 3: Sparse Matrix/Vector product, SpMSpV (top) and Sparse Vector/Vector product, SpVSpV (bottom).
• Figure 4: Rules for sequential composition and independent programs.
• Figure 5: Focus rule

Theorems & Definitions (1)

• theorem 1: Soundness