Mechanised Hypersafety Proofs about Structured Data
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 m...
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery
2024
|
| Online Access: | https://hdl.handle.net/1721.1/155467 |
| _version_ | 1824458221402718208 |
|---|---|
| author | Gladshtein, Vladimir Zhao, Qiyuan Ahrens, Willow Amarasinghe, Saman Sergey, Ilya |
| author2 | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
| author_facet | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Gladshtein, Vladimir Zhao, Qiyuan Ahrens, Willow Amarasinghe, Saman Sergey, Ilya |
| author_sort | Gladshtein, Vladimir |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T13:20:57Z |
| format | Article |
| id | mit-1721.1/155467 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2025-02-19T04:22:27Z |
| publishDate | 2024 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | mit-1721.1/1554672025-01-05T04:42:43Z Mechanised Hypersafety Proofs about Structured Data Gladshtein, Vladimir Zhao, Qiyuan Ahrens, Willow Amarasinghe, Saman Sergey, Ilya Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science 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. 2024-07-08T18:53:15Z 2024-07-08T18:53:15Z 2024-06-20 2024-07-01T07:58:38Z Article http://purl.org/eprint/type/JournalArticle 2475-1421 https://hdl.handle.net/1721.1/155467 Gladshtein, Vladimir, Zhao, Qiyuan, Ahrens, Willow, Amarasinghe, Saman and Sergey, Ilya. 2024. "Mechanised Hypersafety Proofs about Structured Data." Proceedings of the ACM on Programming Languages, 8 (PLDI). PUBLISHER_CC en 10.1145/3656403 Proceedings of the ACM on Programming Languages Creative Commons Attribution-ShareAlike https://creativecommons.org/licenses/by-sa/4.0/ The author(s) application/pdf Association for Computing Machinery Association for Computing Machinery |
| spellingShingle | Gladshtein, Vladimir Zhao, Qiyuan Ahrens, Willow Amarasinghe, Saman Sergey, Ilya Mechanised Hypersafety Proofs about Structured Data |
| title | Mechanised Hypersafety Proofs about Structured Data |
| title_full | Mechanised Hypersafety Proofs about Structured Data |
| title_fullStr | Mechanised Hypersafety Proofs about Structured Data |
| title_full_unstemmed | Mechanised Hypersafety Proofs about Structured Data |
| title_short | Mechanised Hypersafety Proofs about Structured Data |
| title_sort | mechanised hypersafety proofs about structured data |
| url | https://hdl.handle.net/1721.1/155467 |
| work_keys_str_mv | AT gladshteinvladimir mechanisedhypersafetyproofsaboutstructureddata AT zhaoqiyuan mechanisedhypersafetyproofsaboutstructureddata AT ahrenswillow mechanisedhypersafetyproofsaboutstructureddata AT amarasinghesaman mechanisedhypersafetyproofsaboutstructureddata AT sergeyilya mechanisedhypersafetyproofsaboutstructureddata |