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.

翻译：数组是表示数据集合的基本抽象。通常可以利用存储在数组中数据的结构特性（例如重复性或稀疏性）来开发专门的空间高效表示。对这种结构化数据的操作进行形式化正确性推理具有挑战性，因为这些操作通常由多个带有非平凡不变量的循环组成。在这项工作中，我们观察到结构化数据操作的规范可以表述为超安全性性质，即关联$k$个程序轨迹的谓词。为了将这一观察转化为有效的验证方法论，我们开发了优雅张量操作逻辑（LGTM），这是一种新的霍尔风格关系分离逻辑，用于指定和验证结构化数据上的计算。LGTM的关键创新在于参数化超安全性规范，它允许程序组件的数量$k$依赖于程序变量。我们将LGTM作为基础嵌入实现在Coq中，对其规则、元理论和可靠性证明进行了机械化。此外，我们开发了一个领域特定策略库，用于自动化计算机辅助的超安全性推理，得到了令人愉悦的短证明脚本，并且具有高度的可复用性。我们通过指定并机械证明13个案例研究的正确性（包括压缩数组上的计算和多种稀疏张量的高效操作），论证了LGTM中关系推理关于结构化数据的有效性。