Mechanised Hypersafety Proofs about Structured Data: Extended Version
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要