Mechanised Hypersafety Proofs about Structured Data
VLADIMIR GLADSHTEIN, National University of Singapore, Singapore
QIYUAN ZHAO, National University of Singapore, Singapore
WILLOW AHRENS, Massachusetts Institute of Technology, USA
SAMAN AMARASINGHE, Massachusetts Institute of Technology, USA
ILYA SERGEY, National University of Singapore, Singapore
Arrays are a fundamental abstraction to represent collections of data. It is often possible to exploit structuralproperties of the data stored in an array (e.g., repetition or sparsity) to develop a specialised representation
optimised for space eﬃciency. 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 speciﬁcations for structured data manipulations can be phrased as hypersafety
properties, i.e., predicates that relate traces of 𝑘 programs. To turn this observation into an eﬀective veriﬁcation
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 speciﬁcations that allow the number 𝑘 of the program components todepend 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-speciﬁctactics that automate computer-aided hypersafety reasoning, resulting in pleasantly short proof scripts thatenjoy a high degree of reuse. We argue for the eﬀectiveness of relational reasoning about structured data
in LGTM by specifying and mechanically proving correctness of 13 case studies including computations oncompressed arrays and eﬃcient operations over multiple kinds of sparse tensors.
CCS Concepts: • Theory of computation → Logic and veriﬁcation; Programming logic; • Software andits engineering → Formal software veriﬁcation.
Additional Key Words and Phrases: sparse data structures, mechanised proofs, relational logic
ACM Reference Format:
Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey. 2024. Mechanised
Hypersafety Proofs about Structured Data. Proc. ACM Program. Lang. 8, PLDI, Article 173 (June 2024), 24 pages.
https://doi.org/10.1145/3656403

1 INTRODUCTION
Arrays are one of the most basic yet most powerful abstractions in computer science, capable ofrepresenting virtually any kind of data. The most common way to encode data is via a dense arraythat stores data in memory contiguously, providing a simple interface to access it via iteration.
Representing data via dense arrays is often not optimal in terms of space eﬃciency. For instance, asparse tensor (i.e., an 𝑛-dimensional matrix with most of its elements being zeros) can be encodedcompactly by storing only its non-zero elements. Without this space optimisation, manipulations
Authors’ addresses: Vladimir Gladshtein, National University of Singapore, Singapore, vgladsht@comp.nus.edu.sg; Qiyuan
Zhao, National University of Singapore, Singapore, qiyuanz@comp.nus.edu.sg; Willow Ahrens, Massachusetts Institute ofTechnology, USA, willow@csail.mit.edu; Saman Amarasinghe, Massachusetts Institute of Technology, USA, saman@csail.
mit.edu; Ilya Sergey, National University of Singapore, Singapore, ilya@nus.edu.sg.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for proﬁt or commercial advantage and that copies bear this notice andthe full citation on the ﬁrst page. Copyrights for third-party components of this work must be honored. For all other uses,
This work
licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.
contact
theisowner/author(s).
© 2024 Copyright held by the owner/author(s).
ACM 2475-1421/2024/6-ART173
https://doi.org/10.1145/3656403
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:2

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

with tensors that contain real-world datasets becomes impossible due to the immense amount ofstorage that would be required by their dense representations.
Sparsity of a dense array is just one of the many structural properties of the array-stored data;
others include symmetry (e.g., an array-encoded matrix is equal to its transpose), repetition (datacontains segments of repeating elements), or length-irregularity (a.k.a. ragged arrays). Realisingsuch data properties allows one to choose a specialised format for representing structured data,
leading to reduced size of the required storage and improved performance by avoiding redundant
computations (e.g., skipping through all zeros when performing summation over a sparse tensor).
Unsurprisingly, computations that involve structured data are typically much more intricate
than simply iterating through a dense array, as they should take the conventions imposed by thedata’s format into account. The problem of automatically generating code, which is specialised forparticular representations of structured data it manipulates with, has received a lot of attention inrecent years. Some of the most prominent works in this direction include the inﬂuential TACO
framework for code generation (Kjolstad et al. 2017) and the Finch compiler (Ahrens et al. 2023).
Problem statement. Given the intricacy of computations on structured data, it is natural to wonder:
Do they produce the same results as their non-specialised counterparts on dense data representations?
This question suggests a veriﬁcation challenge that we focus on in this work.
Existing eﬀorts on verifying computations with structured data either provide high-level domainspeciﬁc languages (DSL) for encoding data formats as well as format-aware computations (Arnold
et al. 2010), or encode data formats as logical predicates in a language of a solver used to verify
reﬁnement w.r.t. operations on the dense representations (Dyer et al. 2019). By oﬀering a limited
set of predeﬁned abstractions, these DSL- or predicate-based approaches do not allow for verifying
formats, whose encoding does not ﬁt into their formalisms. None of these approaches come with aformal soundness proof regarding the executable code they produce. A recent work by Kellison
et al. (2023) presented a mechanised correctness proof of a particular sparse matrix computation ina general-purpose separation logic embedded into Coq (Appel 2011). That veriﬁcation eﬀort relied
on a tailored encoding of the chosen data format and required several format-speciﬁc lemmas,
making it diﬃcult to reuse any of its components for verifying programs over diﬀerent formats.
The goal of this work is to provide a versatile framework for formally specifying and mechanicallyverifying diverse computations with structured data. We aim for an approach that (a) allows fornaturally-looking and easy-to-state speciﬁcations, (b) can accommodate arbitrary programmaticallydeﬁned data formats, and (c) enables a high degree of proof reuse and automation.
In the rest of the paper, we argue that relational program logics are the right tool for this job.
Specifying manipulations with structured data. Let 1 def m_get (mc, i, j) -> val:
# matrix format; body omitted
us immediately dive into computations with struc- 2
tured data. Fig. 1 shows a high-level outline of one 3
such computations in Python-style pseudocode. The 4 def v_get (vc, i) -> val:
# vector format; body omitted
5function mv_prod multiplies a compressed matrix, com- 6
pactly encoded by a data structure mc, by a compressed 7 def mv_prod(mc, vc) -> val[]:let ans = malloc(vc.size)
vector, encoded via vc.1 The two random access func- 8
for mp in partition(mc):tions, m_get and v_get, whose signatures are given, 9inner_prod (mp, vc, ans)
specify the formats used to compress the matrix and 10
the vector, correspondingly. For instance, given a com- Fig. 1. Structured matrix/vector multiplication.
pressed matrix mc and two indices (row and column
1 Compressed tensors, such as mc and vc from Fig. 1, are typically encoded as tuples of 1-dimensional arrays with their sizes,

but might be also represented as linked data structures (Chou and Amarasinghe 2022).
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

Mechanised Hypersafety Proofs about Structured Data

173:3

position), m_get returns a value (of some type val) stored in the “algebraic” (i.e., dense) version of
the matrix at those positions, without fully reconstructing the dense representation.
An eﬃcient implementation mv_prod of a matrix/vector product, therefore, operates directlyon the compressed representations mc and vc provided as its arguments. Such computations are
typically structured by partitioning the representation of the matrix into separate chunks in someformat-speciﬁc way, and storing the results of submatrix/vector products into the (dense) result
vector ans. Functions of this sort, operating on sparse tensors, compressed via multiple diﬀerent
formats, are standard components of popular libraries for tensor computations, such as SciPy(Python), CsMatBase (Rust), and Eigen (C++). While at the time of this writing most of suchfunction implementations are hand-crafted, they can be also automatically generated by domainspeciﬁc compilers, such as Finch (Ahrens et al. 2023), provided the corresponding computation on
dense matrices/vectors and the programmatic format speciﬁcations such as m_get and v_get.
Importantly, the programmatic format deﬁnitions m_get and v_get are not used directly within theimplementation of mv_prod. Instead, they should be considered as speciﬁcations of the compresseddata that mv_prod manipulates with. Given such speciﬁcations, modern domain-speciﬁc compilers
are capable of producing eﬃcient format-speciﬁc implementations from reference implementationsof the operations phrased in terms of dense representations (Ahrens et al. 2023; Sakka et al. 2017).
How do we specify correctness of mv_prod, asserting that its result is the same as a multiplying
an uncompressed version of mc to that of vc? The key observation we make in this work is thatsuch correctness statements can be stated naturally and concisely as Hoare-style triples that relate
executions of the programmatic format speciﬁcations, such as m_get and v_get, to that of theoperation in question. A common way to capture it formally is via a hypersafety judgment—alogical statement that relates results of executions of multiple possibly diﬀerent computations.
Hypersafety properties can be ascribed to a product of independently run programs in a form of(Hoare-style) hyper-triples, whose pre/postconditions constrain collections of pre/post-states of the
programs in question, as well as their results. Therefore, a correctness speciﬁcation for mv_prod canbe phrased as the following hyper-triple relating its result to those of m_get and v_get:
1: mv_prod(mc, vc)   𝑎 ⟨2, 𝑖, 𝑗⟩𝑖 ∈ [0, 𝑀 ) : m_get(mc, 𝑖, 𝑗)  
𝑃mc (·) ∗ 𝑃vc (·)  𝑚𝑗 ∈ [0, 𝑁 ) ⟨3, 𝑗⟩ 𝑗 ∈ [0,𝑁 ) : v_get(vc, 𝑗)
𝑣








∃𝑠, arr(𝑎, 𝑠) ∗Í⌈∀𝑖, 𝑠 [𝑖] = 𝑗 𝑚(𝑖, 𝑗)𝑣 ( 𝑗)⌉ 


(1)



The hypersafety speciﬁcation (1) relates the execution of 1 + 𝑀 × 𝑁 + 𝑁 programs, with 𝑀
and 𝑁 being the number of the rows and the columns in the matrix. For instance, the component⟨2, 𝑖, 𝑗⟩𝑖 ∈ [0,𝑀 ), 𝑗 ∈ [0,𝑁 ) : m_get (𝑚, 𝑖, 𝑗) of the triple represents a collection of independent runs ofm_get indexed by tuples ⟨2, 𝑖, 𝑗⟩, with 𝑖 ranging from 0 to 𝑀 − 1 and 𝑗 from 0 to 𝑁 − 1. In suchcases, we will refer to the set like {⟨2, 𝑖, 𝑗⟩ | 𝑖 ∈ [0, 𝑀), 𝑗 ∈ [0, 𝑁 )} as index sets. The results of those
𝑀 × 𝑁 programs are bound to a sequence (hyper-)variable 𝑚 of size 𝑀 × 𝑁 , whose individualcomponents are retrieved in the postcondition as 𝑚(𝑖, 𝑗). The same intuition applies to the last 𝑁
program components, whose results are bound to 𝑣. The postcondition of the triple, thus, ensuresthat the result of the ﬁrst program component 𝑎, is a base pointer of an array storing a mathematicalsequence 𝑠, which is element-wise equal to the dot-product of the given matrix and vector.
The precondition features two Separation Logic-style predicates, 𝑃mc and 𝑃 vc , that deﬁne thememory shape of the corresponding compressed matrix/vector representations (i.e., state that they
are encoded in memory by array tuples). The deﬁnitions of those predicates are quite unremarkable,
as they do not capture any relations between elements of a compressed encoding and its densecounterpart: that task is left to m_get and v_get. The only noteworthy component of the preconditionis the (·) notation, which indicates distinct copies of the same symbolic state across multiple state
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:4

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

components indexed by elements of {1} ∪ {⟨2, 𝑖, 𝑗⟩ | . . .} ∪ {⟨3, 𝑗⟩ | . . .}, thus, supplying a valid (i.e.,
safe to execute from) precondition to each one of the 1 + 𝑀 × 𝑁 + 𝑁 programs in the hyper-triple.
Key idea. The speciﬁcation (1) of mv_prod owes its brevity to the idea of parametrised hypertriples. Speciﬁcally, parametrisation means that the index sets used in program components canbe expressed as functions of the input state and variables of the programs in question. To wit,
the index sets in (1) are determined by the variables 𝑀 and 𝑁 , which correspond to the “logical”
dimensions of the involved matrix, and are constrained by the predicate 𝑃 mc .2 The beneﬁts ofparametrisation are not limited to relatively concise speciﬁcations. While very simple conceptually,
the ability to vary the number of the components in a hyper-triple depending on logical- andprogram-level variables is surprisingly useful for verifying properties of iterative computations on
non-overlapping data, such as formats for compression or sparsity. As we will show in Sec. 2, theidea of parametrised hyper-triples makes it almost straightforward to decompose proofs of (statedrelationally) correctness of compressed structure-manipulating programs featuring multiple loops.
Towards practical reasoning about parametrised hypersafety. So-called relational program logics
are a well-studied formalism to specify and reason symbolically about hypersafety properties ofprograms, such as information-ﬂow security and correctness of optimisations (Barthe et al. 2011,2012; Benton 2004; Carbin et al. 2012; Nanevski et al. 2011; Yang 2007). Alas, the vast majority ofexisting relational logics are limited to specifying and proving 2-properties only, while our approach,
exempliﬁed by the spec (1), requires proofs about arbitrary-arity parametrised speciﬁcations.
Two relatively new logics, CHL by Sousa and Dillig (2016) and LHC by D’Osualdo et al. (2022),
provide proof rules for arbitrary-arity hypersafety triples. Unfortunately, CHL does not feature
the necessary proof composition principles: it ﬁxes the arity of a hyper-triple for the entire proof,
making it impossible to employ speciﬁcations about subsets of the program components (or Hoarestyle proofs for individual programs) in the context of a larger proof. LHC, on the other hand,allows for combining speciﬁcations of arbitrary constant arity in a single proof, but lacks rules forworking with hyper-triples whose arity depends on program-level variables. This limitation of LHC
turns out to be a show-stopper for constructing proofs about loops within the logic, requiring one
to resort to proofs in terms of semantics. Furthermore, LHC is not a Separation Logic and, therefore,
provides no support for modular reasoning about arrays and heap-based indirection. Finally, LHC
only exists on paper: it is not implemented as a tool, and its soundness has not been mechanised.
In our quest of building a framework for machine-assisted veriﬁcation of structured data manipulations, which is both foundational (i.e., proven sound from ﬁrst principles) and practical (i.e.,requires low annotation overhead), we are taking forward the ideas for compositional hypersafety
reasoning pioneered by LHC (D’Osualdo et al. 2022), enhancing them with three new aspects:(1) adding new rules for decomposing proofs about arbitrary arity-parametric hyper-triples;(2) providing specialised proof rules for loops that take advantage of hyper-triple parametrisation;(3) introducing support for state-local hypersafety proofs in the style of Separation Logic.
The result is the novel logical framework for Hoare-style hypersafety proofs, dubbed Logic forGraceful Tensor Manipulation (LGTM). We implemented LGTM as a Separation Logic (Reynolds
2002) embedded into the Coq proof assistant. The shallow nature of the embedding allowed us to
use Coq’s higher-order logic capabilities for implementing rules for handling parametrised triples
in the form of ordinary Coq lemmas. Furthermore, the careful design of rules for hyper-triple
decomposition and reasoning about loops made it possible to engineer eﬀective proof automation
resulting in very short and conceptually simple machine-assisted veriﬁcation proofs.
2 In our example, we made those variables explicit in the speciﬁcation, omitting the full signature of 𝑃

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

mc for brevity.

Mechanised Hypersafety Proofs about Structured Data

173:5
1

x_ind

1

3

5

B

0

C

2
3

x

0

A

0

0

2

x_val

A

m_ind

midx
m_idx

C

2

3

B

1

G
D

4

E

1

B
i\j

0
4

4
3

0

4

6

7

5

4

m_val

A

0

2

1

6

C

(b) Sparse Vector (SV) format

m
0

1

0
0

def sv_get(x_ind, x_val, i):
ind = index(x_ind, i)
if (ind != -1):
return x_val[ind]else:
return 0

2

3

4

5

A

0

0

B

0

1

0

0

0

0

0

2

0

D

0

E

0

0

3

0

0

C

0

0

0

0

0

0

0

G

0

(a) SV and uCSR, pictographically4
5
6

def ucsr_get(m_idx, m_ind, m_val, i, j):
ind = index(m_idx, i)
if (ind != -1):
return sv_get(m_ind[ind], m_val[ind], j)else:
return 0(c) Unordered Compressed Sparse Row (uCSR)

Fig. 2. Sparse Vector and Unordered Compressed Sparse Row formats

Contributions and outline. To summarise, in this work we make the following contributions.
• Our ﬁrst conceptual contribution is an observation that speciﬁcation and veriﬁcation of manipulations with structured data can be phrased in terms of reasoning about hypersafety properties.
• Our second conceptual contribution is an idea of a parametrised hyper-triple, whose arity depends
on attributes of the data under manipulation. We show that parametrisation enables hypersafety
proofs based on the structure of the data rather than the structure of the program (Sec. 2).
• Our main theoretical contribution is the Logic for Graceful Tensor Manipulation (LGTM)—a
Hoare-style relational separation logic for hypersafety properties that provides eﬀective reasoning
principles about array-manipulating programs with loops (Sec. 3). We mechanised the metatheory, the rules, and the soundness proof of LGTM in the Coq proof assistant.
• Our practical contribution is a set of Coq-based automation techniques for mechanised proofs in
LGTM that allow for short and intellectually manageable hypersafety proofs (Sec. 4). We haveevaluated our implementation of LGTM by mechanising proofs for 13 characteristic case studies
that implement computations with sparse and compressed tensors in various formats (Sec. 5).
We show that, in comparison with related foundational eﬀorts, mechanised proofs in LGTM areabout 10 times shorter than those done in a general-purpose non-relational Separation Logic.
2 A TOUR OF LGTM
In this section, we showcase the reasoning principles of LGTM as a logic formalism, postponing
the demonstration of its veriﬁcation capabilities as a tool until Sec. 4 and 5. To do so, we specify
and verify a program that computes a product of a compressed sparse matrix and a sparse vector,
represented via the Unordered Compressed Sparse Row (uCSR) format and a Sparse Vector (SV),correspondingly, storing the result into an uncompressed vector represented by an array.
Fig. 2a graphically depicts the data layout in both SV and uCSR formats. The SV format is astandard representation for sparse vectors. It achieves great rates of compression for sparse (i.e.,
mostly-zero) vectors by storing only their non-zero values in an array x_val together with theirindices at the same positions in an array x_ind. The programmatic encoding of SV is provided by
the sv_get function shown in Fig. 2b. This function “decompresses” a sparse vector encoded by
the pair of arrays (x_val, x_ind) by retrieving the ith value of the dense representation x from its
compressed representation via x_ind and x_val. It does so by ﬁrst ﬁnding the index of the element
corresponding to i in the array x_ind, calling the index function (line 2). The implementation ofProc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:6

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

index simply performs a linear scan through the contents of x_ind, returning a position of its second
argument, if it’s present, and -1 otherwise (remember, sv_get only serves as a format speciﬁcation,
hence its eﬃciency is not important). Depending on the search result stored into ind, the rest of
sv_get’s implementation returns either the corresponding x_val element, or zero (lines 3-6).
The uCSR format for sparse matrices is a modiﬁcation of the popular Compressed Sparse
Row (CSR) format, designed to be more eﬃcient by enabling adaptive tiling (Hong et al. 2019).
uCSR adopts a compression principle similar to that of SV: rather than storing each row of thematrix, its only stores rows that have non-zero elements. To this end, uCSR uses an unordered
array m_idx to store the positions of non-empty rows. Those rows are in turn compressed using SV,
with associated two-dimensional arrays m_ind and m_val storing indices and values of non-empty
cells for each row.3 This intuition is mirrored in the programmatic speciﬁcation of uCSR shownin Fig. 2c, which takes three arrays m_idx, m_ind, and m_val, as well as the dense row/column indicesi and j, and retrieves the corresponding element by calling sv_get on its actual row encoding.
The implementation of the sparse ma- 1 def spmspv(m_idx, m_ind, m_val, x_ind, x_val):trix/vector product is given in Fig. 3; we have 2
ans = malloc(M)for i in range(0, length(m_idx)):
adopted it from the output produced by the 3ans[m_idx[i]] =Finch compiler (Ahrens et al. 2023). The func- 4
5
spvspv(m_ind[i], m_val[i], x_ind, x_val)
tion spmspv takes a sparse matrix 𝑚, encoded
return ans
6
in uCSR format via three arrays: m_idx, m_ind, 7
and m_val, as well as a sparse vector 𝑥, en- 8 def spvspv(y_ind, y_val, x_ind, x_val):s, iY, iX = 0, 0, 0
coded via x_ind and x_val. Its result is a dense 9
while (iY < length(y_ind)) &&array ans, populated element-wise by the com- 10
11(iX < length(x_ind)):ponents of the dot-product 𝑚 · 𝑥. The imple12
if y_ind[iY] = x_ind[iX]:mentation of spmspv, also uses the height M of 13
s += y_val[iY] * x_val[iX]
the matrix, which we assume to be a global 14
iY++; iX++
else if y_ind[iY] < x_ind[iX]:variable. The body of spmspv ﬁrst iterates over 15
iY++
all non-zero rows in the order determined by 16
17else if x_ind[iX] < y_ind[iY]:m_idx (line 3). At each iteration of the for-loop
18
iX++
it calls spvspv, computing the product of two 19
return s
sparse vectors, m_idx[i]th row of the matrix 𝑚
and the vector 𝑥. The while-loop in spvspv Fig. 3. Sparse Matrix/Vector product, SpMSpV (top) and(lines 10-18) co-iterates over a pair of sparse Sparse Vector/Vector product, SpVSpV (bottom).
vectors, visiting only non-zero values of both arrays. It does so by maintaining the positions in thecorresponding vectors via variables iY and iX, advancing them in a way so that the result stored
in s is changed only when indices of non-zero elements in the two vectors coincide (line 12).
To specify the result of spmspv, let us introduce some notation. We will abbreviate all unmodiﬁedarrays that encode the involved data by the following Separation Logic (SL)-style predicates:
Arrsm
Arrsx
Arrs

≜
≜
≜

arr(mind, 𝑚 ind ) ∗ arr(mval, 𝑚 val ) ∗ arr(midx, 𝑚 idx )arr(xind, 𝑥 ind ) ∗ arr(xval, 𝑥 val )Arrsm ∗ Arrsx(2)

That is, for instance, Arrsm combines three arrays responsible for representing a sparse matrix 𝑚,with their base pointers (e.g., mind ) given in monospace font and payloads (e.g., 𝑚 ind ) given in italic.
The disjointness of the arrays is asserted by the SL separating conjunction connective ( ∗ ).
The desired speciﬁcation for spmspv is, therefore, captured by the following hypersafety triple:
3 In a more realistic encoding, an additional dense array m_ptr is used to store locations of the boundaries between rows

in one-dimensional arrays m_val and m_ind. In this section, for simplicity of the presentation, we treat m_ind and m_val as
two-dimensional arrays. In our mechanisation, however, we verify the encoding involving the m_ptr array (cf. Sec. 5).
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

Mechanised Hypersafety Proofs about Structured Data

173:7

SeqU2
 


𝑃 𝜄 : 𝑝 1, 𝑆 : P2 𝑥, 𝑧 𝐻 (𝑧)𝑃 [𝜄 : 𝑝 1 ] 𝑥 𝐻






𝑥 𝑄 (𝑥𝑧)
𝜄 : 𝑝 1′∀𝑧, 𝐻 (𝑧)𝐻
𝜄 : 𝑝 1′ , 𝑆 : P2 𝑥, 𝑧 𝑄 (𝑧)






′
′
𝑃
𝜄
:
𝑝
;
𝑝
𝑥
,
𝑆
:
P
1 1
1 , 𝑥 2 𝑄 (𝑥 1 𝑥 2 )2𝑃𝜄 : 𝑝 1 ; 𝑝 1, 𝑆 : P2 𝑥, 𝑦 𝑄 (𝑥𝑦)
local({𝑃𝑖 , 𝑄𝑖 }, 𝑖)∀𝑖, ⌈𝑖 ∈ 𝑆⌉ ∗ 𝑃𝑖 [𝑖 : P (𝑖)] 𝑥 𝑄𝑖 (𝑥)Productonno𝑃𝑖 [𝑆 : P] 𝑥
𝑄𝑖 (𝑥 (𝑖))SeqU1 

∗

𝑖 ∈𝑆

∗

𝑖 ∈𝑆

Fig. 4. Rules for sequential composition and independent programs.

)
1: spmspv(midx, mind, mval, xind, xval )  𝑠) ∗ 𝑎 ∃𝑠, arr(𝑎(1),



Í



 ⟨2, 𝑖, 𝑗⟩𝑖 ∈ [0, 𝑀 ) : ucsr_get(midx, mind, mval,𝑖, 𝑗)
Arrs(·)  𝑚 ⌈∀𝑖, 𝑠 [𝑖] = 𝑗 𝑚(𝑖, 𝑗)𝑥 ( 𝑗)⌉ ∗ (3)𝑗 ∈ [0, 𝑁 ) 𝑥 Arrs(·)
 ⟨3, 𝑗⟩ 𝑗 ∈ [0,𝑁 ) : sv_get(xind, xval,𝑗)The spec assumes that the width 𝑁 of the matrix 𝑚 is a global variable. It makes use of the (·)
notation that “replicates” a SL across all state components in the pre/postcondition. The ⌈·⌉ notation
stands for pure assertions that constrain values and do not depend on the shape of the heaps. Notice
that, unlike Arrs(·), the spatial part arr(𝑎 (1), 𝑠) is only present in the ﬁrst component’s post-state.
(

What’s next? In the rest of this section, we will verify the validity of the speciﬁcation (3) via therules of LGTM. We will start by focusing on the for-loop from the spmspv’s body, “peeling away”
all calls to ucsr_get that do not correspond to any of the loop’s iterations (Sec. 2.1 – Sec. 2.2). We
will then split the remaining calls into groups (one group per non-zero row) and relate the resultof each one to one iteration of the for-loop (Sec. 2.3). We will then show how the obtained goal
can be proven compositionally by using an independently veriﬁed speciﬁcation of spvspv (Sec. 2.4).
Finally, we will sketch the proof of spvspv, showcasing LGTM’s rule for while-loops (Sec. 2.5).
2.1

Proofs about Sequential Composition and Independent Programs

To begin with the proof of (3), we unfold the deﬁnition of spmspv in the ﬁrst component, and omit
ranges of variables 𝑖 and 𝑗, obtaining the following goal to prove:()  1 : ans = malloc(M); . . .


𝑠) ∗


 𝑎 ∃𝑠, arr(𝑎(1),




Í


⟨2,
𝑖,
𝑗⟩
:
ucsr_get(m
,
m
,
m
,𝑖,
𝑗)
Arrs(·)
𝑚
⌈∀𝑖,
𝑠
[𝑖]
=
𝑚(𝑖,
𝑗)𝑥
(
𝑗)⌉
(4)
idx
ind
val
𝑗




 ⟨3, 𝑗⟩ : sv_get(xind, xval,𝑗)𝑥∗Arrs(·)

Notice that the for-loop at lines 3-5 of Fig. 3 only “visits” rows of 𝑚 that correspond to m_idx[i] forsome i. In this subsection, we will show how to reduce the veriﬁcation goal (4) to the one that only
mentions those ucsr_get-components whose (row) argument 𝑖 is present as an element in m_idx.
2.1.1 Rules for Sequential Composition. Our ﬁrst step is to get to the for-loop in the ﬁrst componentof the goal (4), which will require us to symbolically step through the malloc statement, while“focusing” on the corresponding component. This focusing capability is achieved by the SeqU1
shown in Fig. 4, which allows one to split the index set of a hyper-triple into two disjoint subsets,{𝜄} and 𝑆, symbolically executing the ﬁrst component 𝑝 1 of the sequential composition 𝑝 1 ; 𝑝 1′ that
corresponds to the 𝜄-indexed component of the entire hyper-triple.4 Applying SeqU1 with 𝜄 = 1 tothe goal (4) allows us to execute the malloc statement using the proof rule for allocation, which isrelatively standard for Separation Logic-style formalisms, so we postpone its presentation until
4 To avoid clutter, the rules assume that execution of the “projected” components, such as 𝜄 : 𝑝

1 in SeqU1, are implicitly
framed with the corresponding hyper-heap footprint of the 𝑆-indexed component, which it keeps unmodiﬁed.

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:8Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

Sec. 3. The ﬁrst premise of SeqU1, thus, takes the form of the following goal, where we use 0 to
denote a 0-ﬁlled vector of a suitable size, evident from the context:{Arrs(·)} 1 : ans = malloc(M) {Arrs(·) ∗ arr(ans(1), 0)}Here the (1) syntax in arr(ans(1), 0) means that ans is a pointer allocated in the 1-indexed
component of the symbolic state (i.e., the heap where the ﬁrst component runs). Abbreviating thefor-loop as 𝑓 we obtain the following triple as the result of the second obligation of SeqU1:

 𝑎 ∃𝑠, arr(𝑎(1), 𝑠) ∗  1 : 𝑓 ; return ans






 ⟨2, 𝑖, 𝑗⟩ : ucsr_get(midx, mind, mval,𝑖, 𝑗)  𝑚 ⌈∀𝑖, 𝑠 [𝑖] = Í 𝑗 𝑚(𝑖, 𝑗)𝑥 ( 𝑗)⌉
(5)




𝑥
 ⟨3, 𝑗⟩ : sv_get(xind, xval,𝑗)∗Arrs(·)The goal is further simpliﬁed by stripping oﬀ the return statement via the SeqU2 and unfolding𝑀arr(ans(1), 0) into an iterated separating conjunction 𝑖=0 ans(1) + 𝑖 ↦→ 0 over a set of points-to
heaplets (i.e., symbolic heap entries), indexed by their oﬀsets 𝑖 from the base array address ans(1):arr(ans(1), 0)∗ Arrs(·)∗



1 : for 𝑖 in range(0, |𝑚 |) {𝑝 (𝑖)}  −∃𝑠, ∗ ans(1) + 𝑖 ↦→ 𝑠 [𝑖] ∗ Í+ 𝑖 ↦→ 0  ⟨2, 𝑖, 𝑗⟩ : ucsr_get(m , m , m ,𝑖, 𝑗)  
∗ ans(1)
𝑚
⌈∀𝑖,
𝑠
[𝑖]
=
𝑚(𝑖,
𝑗)𝑥
(
𝑗)⌉




∗ Arrs(·)
𝑀
𝑖=0



idx

idx

ind

val

𝑀
𝑖=0



𝑗

𝑥


 ⟨3, 𝑗⟩ : sv_get(xind, xval,𝑗)






∗ Arrs(·)

Finally, we abbreviate the loop’s body as 𝑝 (𝑖), and simplify the postcondition by substituting eachvalue of the ans’ payload sequence 𝑠 [𝑖] with the correspondent sum expression:  1 : for 𝑖 in range(0, |𝑚 |) {𝑝 (𝑖)}  + 𝑖 ↦→ − ∗ ans(1)Í+ 𝑖 ↦→ 0 ∗ ans(1)

𝑚(𝑖,
𝑗)𝑥
(
𝑗)
⟨2,
𝑖,
𝑗⟩
:
ucsr_get(m
,
m
,
m
,𝑖,
𝑗)
𝑚
(6)


∗ Arrs(·)

idx

𝑖

idx

ind

 ⟨3, 𝑗⟩ : sv_get(xind, xval,𝑗)


𝑖

𝑗

val

𝑥


∗ Arrs(·)



2.1.2 Reasoning with Component-Local Assertions. Remember that array midx contains indicesof non-zero rows of the matrix 𝑚, so that the for-loop from the ﬁrst component will iterate only oversuch indices. This suggests us to ﬁrst get rid of all the components with ucsr_get(midx, mind, mval, 𝑖, 𝑗)
for 𝑖 ∉ 𝑚 idx , and try to relate the rest of those with each iteration of the for-loop. To implement the former, we note that for each index 𝑖 outside of the payload 𝑚 idx the result of
ucsr_get(midx, mind, mval, 𝑖, 𝑗) will be 0 for any 𝑗. This fact can be stated as the following triple:ih⌈∀𝑖 ∉ 𝑚 idx ∀𝑗, 𝑚(𝑖, 𝑗) = 0⌉
: ucsr_get(midx, mind, mval,𝑖, 𝑗)𝑚Arrs(·) ⟨2, 𝑖, 𝑗⟩𝑖 ∉ 𝑚idx
(7)𝑗 ∈ [0, 𝑁 )∗ Arrs(·)

To see how to deal with such triples, let us consider the following simple veriﬁcation goal:𝑠 (·) ↦→ 𝑦 [𝑖 0≤𝑖<𝑁 : s += 𝑖] _ 𝑠 (·) ↦→ 𝑦 + 𝑖

Intuitively, proving this triple is equivalent to proving 𝑁 independent 1-safety triples of the form
𝑠 (𝑖) ↦→ 𝑦 [𝑖 : s += 𝑖] _ 𝑠 (𝑖) ↦→ 𝑦 + 𝑖

To capture this intuition LGTM features the rule Product (cf. Fig. 4) that allows one to divide
the state assertions in the pre-/postcondition (indexed by a set 𝑆) into |𝑆 | disjoint assertions, eachbeing local to a particular index. The idea of locality comes from the LGTM memory model, sothat its state assertions constrain not just the shapes of the heap but also the component in which
they reside, so that, e.g., 𝑥 (1) ↦→ 0 and 𝑥 (2) ↦→ 0 are not satisﬁed by the same heap. Postponing amore formal treatment of LGTM state till Sec. 3, here we say that an LGTM assertion is local toan index 𝜄 if it can only be satisﬁed by states that belong to the 𝜄 component. With the Productrule, the assumed locality of the individual speciﬁcations and independence of the program runs, it
suﬃces to prove the correspondent triple for each individual program 𝑝 from a hyper-triple.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

Mechanised Hypersafety Proofs about Structured Data

173:9

The postcondition of the speciﬁcation (7) can be rewritten using the following equivalence:⌈∀𝑖 ∉ 𝑚 idx ∀𝑗, 𝑚(𝑖, 𝑗) = 0⌉ ⇐⇒∗ ⌈𝑚(𝑖, 𝑗) = 0⌉𝑖∉𝑚 idx ,𝑗With the right-hand side of the equivalence above, we can apply the Product rule, reducing (7) to⌈𝑖 ∉ 𝑚 idx ∧ 𝑗 ∈ [0, 𝑁 )⌉ ∗⌈𝑚 = 0⌉ ∗[⟨2, 𝑖, 𝑗⟩ : ucsr_get(midx, mind, mval,𝑖, 𝑗)] 𝑚(8)Arrs(·)

Arrs(·)

This
is a 1-safety property, which is stated in terms of a traditional Hoare-style triple of the form
𝑃 [𝜄 : 𝑝] 𝑥 𝑄 (𝑥) for a program 𝑝. To discharge such obligations, LGTM provides thestandard set of Separation Logic rules. We omit this proof, which relies on an independently provenspeciﬁcation of index(midx,𝑖); it can be found in our Coq development (Gladshtein et al. 2024a).
2.2 Focusing and Framing
At this point, one can think of LGTM as of a “Separation Logic going hyper”, with the heaps being
replicated over index sets. An astute reader could have noticed that the rule Product exploits the(hyper-)locality of spatial triples to provide a version of SL’s frame rule that combines multiple
independent unary triples into a single hyper-triple. In our next steps, we will keep taking advantageof the SL nature of LGTM that enables principles of modular reasoning about hypersafety.
Using (7), we can remove all runs of ucsr_get for 𝑚’s Focus
𝑆 = 𝑆1 ⊎ 𝑆2zero-only rows of 𝑚 from the goal (6). To do so, we willmake use the Focus rule, shown in Fig. 5. Applying it,
𝑃 [𝑆 1 : P1 ] 𝑥 𝐻 (𝑥)followed by the framing-out of some no longer useful∀𝑥, 𝐻 (𝑥) [𝑆 2 : P2 ] 𝑦 𝑄 (𝑥𝑦)
pre-/postconditions components (via standard SL fram𝑃 [𝑆 : P1 ⊎ P2 ] 𝑧 𝑄 (𝑧)ing rules), will make us ready to handle the for-loop in
Fig. 5. Focus rulethe ﬁrst component. The Focus rules allows us to advance executions of the programs within 𝑆 1 (a subset of the whole index set 𝑆 = 𝑆 1 ⊎𝑆 2 ), keeping therest of the state unchanged. The notation P1 ⊎ P2 stands for the disjoint union of two sets of indexed
programs. Notice that the range of the result vector 𝑦 of 𝑆 2 : P would be 𝑆 2 , so we will extend it to
the whole 𝑆 by appending with the result of 𝑆 1 : P, vector 𝑥 of range 𝑆 1 . We apply the Focus ruleto the goal (6) by taking 𝑆 1 = {⟨2, 𝑖, 𝑗⟩ | 𝑖 ∉ 𝑚 idx } and 𝑆 2 = {1} ∪ {⟨2, 𝑖, 𝑗⟩ | 𝑖 ∈ 𝑚 idx } ∪ {⟨3, 𝑗⟩ | . . .}.
Using the spec (7) on the 𝑆 1 -indexed part earns us the conjunct ⌈∀𝑖 ∉ 𝑚 idx ∀𝑗, 𝑚(𝑖, 𝑗) = 0⌉ in theprecondition of the following goal, which corresponds to the second premise of the Focus:

∗

∗
∗

∗
∗

∗


ans(1) + 𝑖 ↦→ 






𝑖 ∈𝑚 idx Í
1: for 𝑖 in range(0, |𝑚 idx |) {𝑝 (𝑖)}  
−





𝑗 𝑚(𝑖, 𝑗)𝑥 ( 𝑗) ans(1) + 𝑖 ↦→ 0 


⟨2,
:
ucsr_get(m
,
m
,
m
,𝑖,
𝑗)
𝑖,
𝑗⟩
𝑚
𝑖
idx
ind
val
𝑖
∈𝑚
idx


ans(1)
+
𝑖
→
↦
0


∗ Arrs(·)
 ⟨3, 𝑗⟩𝑖∉𝑚 idx𝑥: sv_get(xind, xval,𝑗)






∗
Arrs(·)

Now, we can once again exploit the Separation Logic capabilities of LGTM, framing out the part𝑖∉𝑚 idx ans(1) + 𝑖 ↦→ 0 from both pre- and postconditions, obtaining the following goal:
)
(

−
1
: for 𝑖 in range(0, |𝑚 idx |) {𝑝 (𝑖)} 
ans(1) + 𝑖 ↦→ ans(1) + 𝑖 ↦→ 0  ⟨2, 𝑖, 𝑗⟩𝑖 ∈𝑚 : ucsr_get(midx, mind, mval,𝑖, 𝑗)  𝑚 𝑖 ∈𝑚idx Í 𝑗 𝑚(𝑖, 𝑗)𝑥 ( 𝑗) (9)𝑖 ∈𝑚 idx
idx∗ Arrs(·)
 ⟨3, 𝑗⟩: sv_get(xind, xval,𝑗)  𝑥 ∗ Arrs(·)
The triple (9) is an examplary case of a parametrised hypersafety speciﬁcation: its arity is determinedby the data 𝑚 idx that serves as a selector for the ucsr_get programs. Phrasing it this way allowed us
to bring the iterations of spmspv’s for-loop in line with the indexing structure of the speciﬁcation
components, so we could handle the remaining proof using a dedicated LGTM rule for loops.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:10

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

𝑆=

𝑁Ø
−1

𝑆𝑖

local(𝑅𝑖 , 𝑆𝑖 )

𝑖=0

(

𝑁 −1

𝐼 (0, ∅) ∗

∗𝑅
𝑖=0

𝑖

∀𝑥, 𝑖 < 𝑁 ,)

𝐼 (𝑖, 𝑥) ∗ 𝑅𝑖



𝜄 : 𝑝, 𝑆𝑖 : P𝑖𝑧, 𝑦 𝐼 (𝑖 + 1, 𝑥𝑦)For𝜄 : for 𝑖 in range(0, 𝑁 ) {𝑝} , 𝑆 : P 𝑧, 𝑦 𝐼 (𝑁 , 𝑦)Fig. 6. A rule for for-iteration.

2.3

Iteration and Array Splitting

To prove the goal (9), we observe that the 𝑖 th iteration of the for-loop in the ﬁrst component
computes the dot product of the vector 𝑥 and the 𝑖 th row of the matrix 𝑚. This suggest partitioining
the veriﬁcation task by aligning (i.e., relating the result of) each 𝑖 th iteration of that loop with asequence of runs of sv_get(xind, xval,𝑗) and ucsr_get(midx, mind, mval,𝑖, 𝑗) for all 𝑗, 0 ≤ 𝑗 < 𝑁 , asthose runs compute values of 𝑥 and the 𝑖 th row of 𝑚. This pattern of splitting a set of independentruns into “batches” to align with individual loop iterations in the “main” program is so common in
structured data computations that LGTM introduces a dedicated rule For to handle it (Fig. 6).
Ð𝑁 −1
To understand how the rule works, ﬁrst notice its premise 𝑆 = 𝑖=0
𝑆𝑖 that splits the index set
𝑆 into 𝑁 parts 𝑆𝑖 . Each part corresponding to a program “batch” to be aligned with one iteration𝑁 −1of the for-loop. The precondition of the conclusion features an assertion 𝑖=0 𝑅𝑖 that describes
a matching split of the pre-state required to run each of those batches (hence the locality side
condition). The most interesting aspect of the rule is the loop invariant 𝐼 , which is an assertion
parametrised by (𝑖) an integer that corresponds to the next value of the loop counter and (𝑖𝑖) a
hyper-value that collects the results of all program batches that have been already aligned with the“preﬁx” of the loop. That is, in the conclusion of the rule, it is assumed that the assertion 𝐼 (0, ∅)holds initially: which corresponds to zero iterations and no aligned batches executed so far (∅ is anempty hyper-value). At the end, 𝐼 (𝑁 , 𝑦) means that the loop has been fully executed and all of thealigned programs’ results are bound by 𝑦. The inductive step of the rule, i.e., the premise deﬁning
the goal for the body of the loop 𝑝, assumes that the invariant initially holds for some 𝑖 < 𝑁 and a
hyper-value 𝑥 (of size 𝑖, which we omit from the rule for brevity), and asserts in the postcondition
that at the end the invariant holds on the next index 𝑖 + 1 and the combined hyper-value 𝑥𝑦.5
To proceed with our proof of (9) using the For rule, we ﬁrst split the set of its indices as follows:∗⟨2, 𝑖, 𝑗⟩𝑖 ∈𝑚idx ,𝑗 ∈ [0,𝑁 ) ∪ ⟨3, 𝑗⟩ 𝑗 ∈ [0,𝑁 ) =|𝑚Ø
idx | −1

𝑆𝑖 =

𝑖 ∈0

Next, we deﬁne the loop invariant as follows:
𝐼 for (𝑖, 𝑚𝑥)≜|𝑚Øidx | −1 

⟨2, 𝑚 idx [𝑖], 𝑗⟩ 𝑗 ∈ [0,𝑁 ) ∪ ⟨3, 𝑗⟩ 𝑗 ∈ [0,𝑁 )𝑖 ∈0∗ ans(1) + 𝑗 ↦→ Í 𝑚( 𝑗, 𝑘)𝑥 (𝑘) ∗ ∗
𝑖 −1
𝑗=0

𝑁
𝑘=0

|𝑚 idx | −1
ans(1) + 𝑗 ↦→ 0
𝑗=𝑖



(10)

(11)

The invariant states that (a) a 𝑗 th element from the preﬁx of the array ans(1), is already ﬁlled withthe dot product of 𝑥 and 𝑗 th row of 𝑚 (i.e., the dot-product of results of ucsr_get and sv_get), for
0 ≤ 𝑗 < 𝑖 and (b) that the suﬃx of the array is ﬁlled with zeros. After applying For and advancing
the code of spmspv (Fig. 3) up to the line 5, we obtain the following goal, for some 𝑖 ∈ [0, |𝑚 idx |):



1
: ans[midx [i]] = spvspv(. . . )


−


ans(1) + 
𝑚 idx [𝑖] ↦→ 0  ⟨2, 𝑖, 𝑗⟩ 𝑗 ∈ [0,𝑁 ) : ucsr_get(midx, mind, mval,𝑚 idx [𝑖], 𝑗)  𝑚  ⟨3, 𝑗⟩ ∗ Arrs(·)
𝑥𝑗 ∈ [0,𝑁 ) : sv_get(xind , xval ,𝑗)





ans(1) + 𝑚 idx [𝑖] ↦→ 


Í
𝑚(𝑖,
𝑗)𝑥
(
𝑗)
𝑗


∗ Arrs(·)


5 As a curiosity, this means that 𝐼 has a dependent type: the value of its ﬁrst parameter determines the arity of the second.

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

Mechanised Hypersafety Proofs about Structured Data

173:11

Now we can advance lines 2 and 3 in uscr_get (Fig. 2c): index (midx, 𝑚 idx [𝑖]) evaluates to 𝑖, triggering
then-branch of the if-statement (line 4), leaving us with the following goal:




1
: ans[midx [i]] = spvspv(. . . )  + 𝑚 idx [𝑖] ↦→ 
 ans(1)+ − ans(1)Í




𝑚 idx [𝑖] ↦→ 0  ⟨2, 𝑖, 𝑗⟩ 𝑗 ∈ [0,𝑁 ) : sv_get(mind [i], mval [i],𝑗)  𝑚
𝑚(𝑖,
𝑗)𝑥
(
𝑗)
(12)
𝑗





 ∗ Arrs(·)
  ⟨3, 𝑗⟩𝑥∗
Arrs(·):
sv_get(x
,
x
,𝑗)
ind
val
𝑗
∈
[0,𝑁
)




We can further reduce the goal using SeqU1 and omitted symbolic execution rules for unary triples:()
1: spvspv(mind [i], mval [i], xind, xval )  
Í


 𝑠



⌈𝑠 = 𝑗 𝑚(𝑖, 𝑗)𝑥 ( 𝑗)⌉ Arrs(·)  ⟨2, 𝑖, 𝑗⟩ 𝑗 ∈ [0,𝑁 ) : sv_get(mind [i], mval [i],𝑗)
𝑚
(13)


∗
Arrs(·)
𝑥 ⟨3, 𝑗⟩:sv_get(x
,
x
,𝑗)
ind
val
𝑗
∈
[0,𝑁
)



2.4 Domain Substitution and Specification Composition
At this point, we have almost reduced the veriﬁcation of the spmspv speciﬁcation to verifying
the correctness of its auxiliary function spvspv w.r.t. the respective format deﬁnition sv_get: ourremaining goal (13) looks pretty much like a speciﬁcation of a sparse vector/vector dot-product.
The actual desired speciﬁcation of spvspv is captured via the following hyper-triple:
1: spvspv(yind, yval, xind, xval )  




𝑠


 𝑦 ⌈𝑠 = Í 𝑗 𝑦 ( 𝑗)𝑥 ( 𝑗)⌉ ⟨2, 𝑗⟩ 𝑗 ∈ [0,𝑁 ) : sv_get(yind, yval,𝑗)
(14)






 ⟨3, 𝑗⟩𝑗 ∈ [0,𝑁 ) : sv_get(xind , xval ,𝑗) 𝑥The predicate Arrsy (·) abbreviates arr(yind (·), 𝑦𝑖𝑛𝑑 ) ∗ arr(yval (·), 𝑦 𝑣𝑎𝑙 ) , similarly for Arrsx (·). To
see how can we get (13) out of (14) recall that in (13), the implicitly universally quantiﬁed (outside ofthe entire hyper-triple) variable 𝑖 ranges from 0 up to |𝑚 ind | − 1. Since 𝑖 is ﬁxed across all programsin the second component, we get rid of it via domain substitution.
A simpliﬁed version of the substitution rule Subst
Subst is presented in Fig. 7. Its key component
𝜙 : 𝑆 → 𝑆 ′ is injective ∀𝑖, P ′ (𝑖) = P (𝜙 (𝑖))is an injective mapping 𝜙 from the index set 𝑆 to a{𝜙 [𝑃]} 𝜙 [𝑆] : P ′ {𝜙 [𝑄]}′set 𝑆 , which embodies the reindexing in question.
{𝑃 } [𝑆 : P] {𝑄 }This rule applies 𝜙 to the index set of the triple 𝑆.
It also changes P to P ′ , which is a reindexed P
Fig. 7. Domain substitution rule
w.r.t. to 𝜙. Finally, it re-indexes the components ofboth pre- and postcondition by applying 𝜙 (denoted, e.g., 𝜙 [𝑃]), transforming, in particular, spatialassertions of the kind 𝑥 (𝜄) ↦→ 𝑣 into 𝑥 (𝜙 (𝜄)) ↦→ 𝑣. For composite assertions, containing separation conjunction, and big separation conjunction, 𝜙 just iteratively distributes over their logicalconnectives. This transformation does not aﬀect the validity of the assertions, since 𝜙 is injective.
We apply Subst to (13), taking 𝑆 to be the index set of (13), and 𝜙 to be a function removing
the second element 𝑖 from all tuples from the second component of 𝑆. Note that this 𝜙 is going to
injective as 𝑖 is ﬁxed across all the programs in the second component. The obtained triple is:Arrsy (·) ∗Arrsx (·)


1
: spvspv(mind [i], mval [i], xind, xval )  




 𝑠


 𝑚 ⌈𝑠 = Í 𝑗 𝑚( 𝑗)𝑥 ( 𝑗)⌉ ⟨2, 𝑗⟩ 𝑗 ∈ [0,𝑁 ) : sv_get(mind [i], mval [i],𝑗)




𝑥
 ⟨3, 𝑗⟩𝑗 ∈ [0,𝑁 ) : sv_get(xind , xval ,𝑗)Now, substituting mind [i] for y in (14), we get a hyper-triple that immediately implies (15).


Arrs(·)(15)

2.5 A Rule for While-Loops
What is left now is to verify correctness of spvspv stated as a hyper-triple (14). Below, we sketch its
proof, primarily focusing on how to deal with the while-loop in the body of spvspv.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:12

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

While
𝑁Ø
−1
𝑆𝑖
𝑆=
𝑖=0




𝜄 :𝑐
𝑏 ⌈𝑏 = false⌉∀𝑥, 𝐼 (𝑁 , 𝑥)
local(𝑅𝑖 , 𝑆𝑖 )
𝜄 : if 𝑐 then 𝑝, 𝑆𝑖 : P𝑖 𝑧, 𝑦 𝐼 (𝑖 + 1, 𝑥𝑦)∀𝑥, 𝑖 < 𝑁 , 𝐼 (𝑖, 𝑥) ∗ 𝑅𝑖
(
)
𝑁 −1


𝜄 : while (𝑐) {𝑝} , 𝑆 : P 𝑧, 𝑦 𝐼 (𝑁 , 𝑦)
𝐼 (0, ∅) ∗
𝑅𝑖

∗

𝑖=0

Fig. 9. A rule for while-iteration.

0
1
2
3
4
5
6
7
The proof is enabled by an important fact: the while-loop
0
1
0
7
0
1
0
2
in spvspv processes only non-zero values of input vectors. An yillustration of how spvspv works is depicted in Fig. 8. Given
the vectors 𝑦 and 𝑥, the algorithm visits all positions where x 0 0 2 3 0 0 0 9
at least one vector has a non-zero value (1, 2, 3, 5, and 7 inthis example). For each such position, spvspv will increase the s
0 + 0 + 0 +21+ 0 + 0 + 0 +18
value of s only if both positions are non-zero (such situations
Fig. 8. SpVSpV pictographicallyare depicted with solid black lines in Fig. 8). Getting backto (14), this suggests us to align each iteration of the while-loop with the corresponding elementfrom the sequence of non-zero indexes in payloads of either of the two vectors 𝑦ind ∪ 𝑥 ind . For
all other indices 𝑗, results of both sv_get
functions, 𝑦 ( 𝑗) and 𝑥 ( 𝑗) will be zero, hence they can beÍsafely elided from the summation 𝑗 𝑦 ( 𝑗)𝑥 ( 𝑗). This can be captured by the following triple:

Arrsy (·) ∗Arrsx (·)

⟨2, 𝑗⟩ 𝑗∉𝑦ind ∪𝑥 ind : sv_get(yind, yval,𝑗)⟨3, 𝑗⟩ 𝑗∉𝑦ind ∪𝑥 ind : sv_get(xind, xval,𝑗)



𝑦
𝑥

⌈∀𝑗 ∉ 𝑦ind ∪ 𝑥 ind , 𝑦 ( 𝑗) = 0⌉ ∗⌈∀𝑗 ∉ 𝑦ind ∪ 𝑥 ind , 𝑥 ( 𝑗) = 0⌉



(16)

The hyper-triple (16) can proven in a way similar to the speciﬁcation (7) of ucsr_get. First, using
the Product rule we reduce it to a set of unary triples, and then, noticing that the index functionin the body of sv_get will return -1 for any 𝑗 that is not an element of the set 𝑥 ind ∪ 𝑦ind . Now
applying the Focus rule, and taking ind ≜ 𝑦ind ∪ 𝑥 ind , we reduce (14) to the following goal:Arrsy (·) ∗Arrsx (·)

1
: spvspv(yind, yval, xind, xval )  

𝑠


 ⟨2, 𝑗⟩ 𝑗 ∈ind : sv_get(yind, yval,𝑗) 𝑦 ⟨3, 𝑗⟩ 𝑥𝑗 ∈ind : sv_get(xind , xval ,𝑗)



⌈𝑠 =

Í

𝑗 ∈ind𝑦 ( 𝑗)𝑥 ( 𝑗)⌉









(17)

Finally, we are ready to align each iteration of the while-loop with the corresponding element of
ind by applying the While rule shown on Fig. 9. While is (predictably) similar to the For rule.
The intuition for this rule comes from the fact that each loop while (𝑐) {𝑝} that terminates after
no more than 𝑁 steps is equivalent to just 𝑁 iterations of if 𝑐 then 𝑝. Therefore, if we divide ourindex set into 𝑁 batches, we can align each batch with one execution of if 𝑐 then 𝑝. Note that
this will also handle the case when the loop terminates after 𝐾 < 𝑁 steps: in that case all runs ofif 𝑐 then 𝑝 will become idle, starting from the 𝐾 th step. A new premise on the top right corner
will ensure that the loop will terminate once we have exhausted all batches.6 To proceed with theproof of (17) by making use of the While rule, we divide our index set as follows:⟨2, 𝑗⟩ 𝑗 ∈ind ∪ ⟨3, 𝑗⟩ 𝑗 ∈ind =

|ind
| −1
Ø

{⟨2, ind [ 𝑗]⟩ , ⟨3, ind [ 𝑗]⟩}𝑗=0

6 LGTM is implemented as logic for total correctness, yet the While rule does not require an explicit termination measure.
The termination will follow from the fact that, each iteration is aligned with its own batch from a ﬁnite set of index batches.

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

Mechanised Hypersafety Proofs about Structured Data

173:13

Locations 𝑥, 𝑦, . . . alpha-numeric strings
Constants𝑛
unbounded integer literals
Expressions 𝑒 ::= 𝑛 | true | false | 𝑥 | 𝑒 = 𝑒 | 𝑒 < 𝑒 | 𝑒 ∧ 𝑒 | ¬𝑒 | 𝑒 ⊕ 𝑒Command𝑐 ::= !𝑥 | 𝑥 [𝑑 ] | 𝑥 := 𝑒 | 𝑥 [𝑒 ] := 𝑒 | for 𝑥 in range(𝑒, 𝑒 ) {𝑐 } | while (𝑒 ) 𝑐 | if (𝑒 ) {𝑐 } else{𝑐 } |let 𝑥 := 𝑐 in 𝑐 | alloc(𝑛) | malloc(𝑛) | free(𝑥 ) | mfree(𝑥 ) | length(𝑒 ) | return 𝑒

Fig. 10. LGTM programming language

Here, to reference to the 𝑗 th component of ind we treat as an sorted sequence without duplicates.
Let us show the most important part of the loop invariant and sketch the rest of the prove:
𝐼 while ( 𝑗, 𝑦𝑥) ≜ ∃iy , ix , iY ↦→ iy ∗ iX ↦→ ix ∗Í𝑠 ↦→ 𝑘< 𝑗 𝑦 (ind [𝑘]) 𝑥 (ind [𝑘]) ∗⌈min(𝑥 ind [ix ], 𝑦ind [iy ]) = ind [ 𝑗]⌉ ∗ . . .

(18)

The ﬁrst line of the invariant simply gives names to the values stored in the vector counters(iy and ix ). The second line captures the fact that 𝑠 stores the accumulated intermediate result of thedot product. The third line is the most subtle: it states that at each iteration, the current positionin the ind sequence, is equal to a minimum of the current positions in both vectors (𝑦ind [iy ] and𝑥 ind [ix ]). If 𝑦ind [iy ] and 𝑥 ind [ix ] are same, then they are both equal to ind [𝑘]. Hence line 6 of spvspv
will increase the sum by 𝑦 (ind [ 𝑗]) 𝑥 (ind [ 𝑗]), preserving the second line of 𝐼 while . In other cases,
using the third line of the invariant, we will be able to show one of 𝑦ind [iy ] or 𝑥 ind [ix ] to be zero,so the sum will indeed remain unchanged, matching the code on lines 8-9 and 10-11 of Fig. 3.
2.6 Putting It All Together
And that concludes our tour of LGTM! As a quick recap, the right side of Fig. 13 summarises themain milestones of our proof of spmspv’s speciﬁcation (3) (with pre-/posts elided), showing thecorresponding sections and changes in the proof goals. Once again, we emphasise the key LGTM
aspects that enabled the proof: separation for modular reasoning (Sec. 2.1.2), parametrisation fordeconstructing loops (Sec. 2.3 and 2.5), and compositionality for proof reuse (Sec. 2.4). We next
brieﬂy outline LGTM’s soundness argument, postponing the presentation of its implementation asa veriﬁcation tool till Sec. 4, in which we will show the Coq mechanisation of our spmspv example.
3 LGTM, FORMALLY
The programming language of LGTM (Fig. 10) is chosen to be generic enough to model tensor
computations in C, Python, and Julia. Its commands include location and array access (!𝑥 and𝑥 [𝑒]), allocation/deallocation for both individual memory locations (via alloc/free) and arrays (viamalloc/mfree). The let-expressions are also used to chain sequences of commands, thus encoding asequential composition. For the sake of the presentation, we assume that all the considered programs
are well-typed, integers are unbounded, and division is not present amongst the operations.
3.1 Semantics
We adopt a standard big-step semantics for our language. Let 𝑐 be a command and 𝑠 be a state, i.e.,
a ﬁnite mapping from locations Loc to values Val. The evaluation relation ⟨𝑐, 𝑠⟩ ⇓ ⟨𝑣, 𝑠 ′ ⟩ is deﬁned
inductively on the structure of 𝑐. It means that a command 𝑐 starting from input store 𝑠 terminateswith the return value 𝑣 ∈ Val, and store 𝑠 ′ .7 In this work, we only focus on deterministic program
executions, i.e., such that allocation does not exercise randomness. For a ﬁxed index set 𝑆, given
two hyper-heaps ℎ and ℎ ′ deﬁned as mappings from Loc × 𝑆 to values, a hyper-value 𝑣 and an
7We only consider terminating programs, and require termination measure given for programs with while-loops.

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:14

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

𝑆-indexed program product P, the semantics of a product execution is deﬁned as follows:⟨P, ℎ⟩ ⇓𝑆 ⟨𝑣, ℎ ′ ⟩ ≜ ∀𝜄 ∈ 𝑆, ⟨P (𝜄), ℎ|𝜄 ⟩ ⇓ ⟨𝑣 (𝜄), ℎ ′ |𝜄 ⟩That is, for every 𝜄 ∈ 𝑆 and individual program P (𝜄) executed on the corresponding projection ℎ|𝜄
of the initial hyper-heap (deﬁned as ℎ|𝜄 ≜ 𝜆𝑙 ∈ Loc. ℎ(𝑙, 𝜄)), its execution results in a new state ℎ ′ |𝜄and a value 𝑣 (𝜄). Similarly to the ordinary (unary) programs, we assume all programs in a productto be deterministic and terminate (the latter is guaranteed for all programs that verify in LGTM).
The details of the semantics can be found in our Coq mechanisation (Gladshtein et al. 2024a).
Hyper-safety triples in LGTM are deﬁned in terms of the weakest precondition predicate:
wp [𝑆 : P] {𝑄 } ≜ 𝜆ℎ, ∃ℎ ′ 𝑣, ⟨P, ℎ⟩ ⇓𝑆 ⟨𝑣, ℎ ′ ⟩ ∧ 𝑄 (𝑣)(ℎ ′ )(19)The weakest preconditions are relative to a provided postcondition (i.e., a predicate on hyperheaps) 𝑄 and are deﬁned as predicates on input heaps ℎ, where 𝑄 is a function from hyper-value
to hyper-heap assertions. We next deﬁne a hyper-triple {𝑃 } [𝑆 : P] {𝑄 } as a notation for 𝑃 ⊢wp [𝑆 : P] {𝑄 }. In plain language, this means that an assertion 𝑃 (ℎ) implies wp [𝑆 : P] {𝑄 }(ℎ)
for any hyper-heap ℎ. We will use the expanded version of the postcondition whenever we want toemphasise its assertion 𝑄 to be a function of the result hyper-value: {𝐻 } [𝑆 : P] {𝑣 | 𝑄 (𝑣) } andwe will omit the index set 𝑆 whenever it is clear from the context. Note that, due to the termination
requirement on the programs in products, all triples in LGTM ensure total correctness by deﬁnition.
3.2

Support for Reasoning with Parametrisation and Separation

Many essential rules of LGTM take their origins in the Logic for Hyper-triple Composition (LHC)by D’Osualdo et al. (2022). LGTM’s structural and lockstep rules directly adjust those of LHC to workwith parametrised triples that use Separation Logic (SL) connectives and predicates. Below, weoutline the key LGTM’s enhancements on top of LHC, supporting parametrisation and separation.
3.2.1 Parametrisation. One example of an LGTM rule idx(𝑄 1 ) ⊆ supp(𝑡 1 ) idx(𝑄 2 ) ⊆ supp(𝑡 2 )that is not derivable in LHC is the Product rule (Fig. 4).
wp P1 {𝑄 1 } ∧ wp P2 {𝑄 2 }Wp-Conj
Product takes inspiration from LHC WpConj rule,
wp (P1 + P2 ) {𝑄 1 ∧ 𝑄 2 }depicted on Fig. 11. LHC triples do not feature the index
Fig. 11. WpConj rule from LHC
set explicitly, as all programs in LHC triples can only
be indexed with natural numbers. This rule allows one to conjoin speciﬁcations of two program
products P1 and P2 with possibly overlapping components, yielding P1 + P2 , if P1 and P2 agree
on the overlapping part. Even though LHC’s rules are phrased in terms of triples with an arbitrary
number of programs, this number must be ﬁxed prior the proof. This is not a problem in LHC: forprogram products of a ﬁxed known size 𝑛, one would have to apply this rule 𝑛 times.
Things become problematic with parametrised triples: to get the eﬀect of LGTM’s Productrule, one would have to apply Wp-Conj the size of 𝑆 number of times. To support cases when |𝑆 |depends, e.g., on a program parameter, this would require LHC support a “constant-space” iterated
rule application (as in R𝑛 () instead of R (R (. . . )) - repeated explicitly 𝑛 times) of Wp-Conj. Thisability does, indeed, come “for free” for an embedding into a higher-order logic such as one of Coq(hence the importance of Coq formalisation in our work). It is, however, missing from LHC, but is
explicitly captured in LGTM rules. The same idea applies to For and While rules (Sec. 2.3–2.5). In
both those rules we divide the index set 𝑆 into 𝑛 batches, where 𝑛 is a parameter coming from thespeciﬁcation, so that one iteration of the for-/while-loop handles only one such batch.
3.2.2 Separation. LGTM extends LHC’s lockstep inference
rules with Separation Logic speciﬁc-rules (e.g., for pointerand array allocation). Adding required adjusting a unary{emp} [𝑆 : alloc(𝑣)] 𝑥∗ 𝑥 (𝑖) ↦→ 𝑣

𝑖 ∈𝑆

Fig. 12. LGTM rule for allocation

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

Mechanised Hypersafety Proofs about Structured Data

173:15

SL proof system to work with hyper-heaps, as, for instance, is exempliﬁed by Alloc rule presented
on Fig. 12. Alloc states that the results of a family of pointer allocations are these pointers 𝑥,
pointing to the assigned value. Other LGTM lockstep rules follow the same intuition and areavailable in the appendix of the extended version of the paper (Gladshtein et al. 2024b).
3.3 Soundness and Mechanisation
We say that LGTM triple {𝑃 } [𝑆 : P] {𝑄 } is derivable and write ⊢LGTM {𝑃 } [𝑆 : P] {𝑄 } if this triple
can be obtained using the rules of the logic. We say that the triple {𝑃 } [𝑆 : P] {𝑄 } is semanticallyvalid and write |= {𝑃 } [𝑆 : P] {𝑄 } if and only if∀ℎ, 𝑃 (ℎ) ⇒ ∃ℎ ′ 𝑣, ⟨P, ℎ⟩ ⇓𝑆 ⟨ℎ ′, 𝑣⟩ ∧ 𝑄 (𝑣)(ℎ ′ )That is, we ask that for every hyper-heap ℎ satisfying the precondition, if we run P on it, it
terminates, and the resulting hyper-heap and hyper-value satisfy 𝑄. The derivability of a logic
triple in LGTM is connected to its semantic validity by the following standard soundness result:
Theorem 3.1 (Soundness). For all hyper-heap assertions 𝑃, functions from hyper-value to hyperheap assertions 𝑄, and program products P indexed by a set 𝑆,⊢LGTM {𝑃 } [𝑆 : P] {𝑄 } ⇒ |= {𝑃 } [𝑆 : P] {𝑄 }We have mechanised the meta-theory of LGTM and its semantics in the logic of Coq proof
assistant. In our mechanisation, we deﬁned the Hoare triples semantically in terms of the weakest
precondition predicates, which, by their deﬁnition (19) encode semantic validity. We then deﬁned
each LGTM rule as a lemma and proved that it holds, thus establishing the result of Theorem 3.1.
Our mechanisation of LGTM is built by extending CFML (Charguéraud 2011, 2020)—a mechanised
sequential Separation Logic. Our changes to the original CFML including the theory of hyper-heaps,
the wp-calculus for program products, LGTM rules, and automation, are totalling at 20kLOC.
4 LGTM AS A VERIFICATION TOOL
Let us now showcase LGTM as a veriﬁcation framework by walking through a mechanisation of
the spmspv case study from Sec. 2 and explaining its most essential proof automation components.
4.1

Structuring Mechanised Proofs

Fig. 13 presents a mechanised proof of spmspv (left) next to the informal outline of the proof
derivation from Sec. 2 (right), with gray rectangles depicting the transformations of the proof goals.
One noticeable technical diﬀerence between the two proofs is the representation of index sets inthe mechanisation. In the Coq speciﬁcation (lines 1-7), each component of the program product has
an explicit tag, separate from the rest of the index set deﬁnition. For example, the tag of uscr_get
is 2. We tried several designs for LGTM triples and found the “tagged union” of index sets to be themost user-friendly when it comes to the local per-component reasoning via focusing (Sec. 2.2).8
The proof immediately makes use of the index set tags: the xin tactical (i.e., a higher-order tactic)
at line 9 takes the tag 1 as its argument, thus applying a version of the SeqU1 rule (Sec. 2.1.1). Using
xin, one can advance the proof of a composite hyper-triple by symbolically executing instructions in
its sub-components in a lockstep manner by passing a sequence of tactics implementing sequential(or, in general, lockstep) rules after the : separator. In this case, we pass two tactics to the xin
tactical. The ﬁrst one, xmalloc, symbolically executes the malloc instruction in the ﬁrst component.
The second, xret, strips oﬀ the last return statement in the body of spmspv.
8 The tag-based encoding does not aﬀect expressivity, since index sets can be arbitrarily mapped using Subst (Fig. 7).

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:16

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

1 Lemma spec_spmspv (midx mind mval xind xval : loc) :2 {{ Arrs }} [{[1| _ ∈ {0}⇒ spmspv midx mind mval xind xval ];[2| ij ∈ [0,M) x [0,N) ⇒ uscr_get midx mind mval ij.1 ij.2];

3
4

5[3| j ∈ [0,N)⇒ sv_get xind xval j];
1 }}6 }] {{ a m x, arr(a, fun i ⇒ \sum_(j ∈ [0, N)) m(i,j) * x(j)) \* Arrs
7 Proof. xstart. (* proof start *)
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

2
:
11
: spmspv(midx , mind , mval , xind , xval )6
6 h2, i, ji i 2 [0, M ) : ucsr_get(midx, mind, mval,i, j)
6j 2 [0, N )66 h3, ji j 2[0,N ) : sv_get(xind, xval,j)4: spmspv
1. .i)
get(.val!: for i in range(0, |midx |) {p(i)} §2.1.1<latexit sha1_base64="oZWxhmklKBgXkjk1W8vawWyUHUU=">AAAB8HicbVBNS8NAEJ3Ur1q/qh69LBbBU0mkqMeiF48V7Ie0oWw2m3bpbjbsboQS+iu8eFDEqz/Hm//GTZuDtj4YeLw3w8y8IOFMG9f9dkpr6xubW+Xtys7u3v5B9fCoo2WqCG0TyaXqBVhTzmLaNsxw2ksUxSLgtBtMbnO/+0SVZjJ+MNOE+gKPYhYxgo2VHgec4lAbWRlWa27dnQOtEq8gNSjQGla/BqEkqaCxIRxr3ffcxPgZVoYRTmeVQappgskEj2jf0hgLqv1sfvAMnVklRJFUtmKD5urviQwLracisJ0Cm7Fe9nLxP6+fmujaz1icpIbGZLEoSjkyEuXfo5ApSgyfWoKJYvZWRMZYYWJsRnkI3vLLq6RzUfcu6437Rq15U8RRhhM4hXPw4AqacActaAMBAc/wCm+Ocl6cd+dj0Vpyiplj+APn8wdxmJAv</latexit>

2
1: for i in range(0, |m idx |) {p(i)}(* § 2.1.1 *)6
6 h2, i, ji i 2 [0, M ) : ucsr_get(midx, mind, mval,i, j)
xin 1 : xmalloc p⇒ //; xret.
6
j
2
[0,
N
)
6
(* § 2.2 *)6 h3, ji j 2[0,N ) : sv_get(xind, xval,j)4xfocus 2 (indom (midx x [0, N) )).
ji i < midx
ji i 2 midx ji i 2 [0,6M )6ji i 2 [0, M )(* § 2.1.2 *)4 §2.2j 2 [0, N ) §2.1.2
j 2 [0,4N )j 2 [0, N )j 2 [0, N )xapp spec_ucsr_get.
h- case⇒ ??; indomE; tauto.
2: i in range(0, |m idx |) {p(i)} h2, i, ji i < m : ucsr_get(. . .i, j)
11
: for
6
idx
xclean_unused. (* clean up unused assertions *)j 2 [0, N )6 h2, i, ji i 2 m : ucsr_get(midx, mind, mval,i, j)
idx
6(* frame out unused part of ans array *)j 2 [0, N )66 h3, ji j 2[0,N ) : sv_get(x , x ,j)
xframe_array p midx .
ind val4- move⇒ *; erewrite <-Sum0s at 1; apply/SumEq⇒ ?.
1: spvspv(mind [i], mval [i], xind, xval )1: for i in range(0, |m idx |) {p(i)}by indomE⇒ /=; case_if.
§2.3: ucsr_get(midx, mind, mval,i, j): sv_get(mind [i], mval [i],j)(* partition index set into Si to apply For-rule *)have E: [0,M)x[0,N) ∩ midx x[0,N) = midx x[0,N)2
1: spvspv(mind [i], mval [i], xind, xval )- rewrite prod_intr_list; f_equal; exact/intr_list.
6
6 h2, i, ji j 2[0,N ) : sv_get(mind [i], mval [i],j)
rewrite E fset_of_list_nodup prod_Union_distr.
6
6 h3, jirewrite -(Union_same |midx | [0, N)).
j 2[0,N ) : sv_get(xind , xval ,j)422(* § 2.3 *)6#6
6 h2, ji
§2.4 6 h2, i, ji
xfor with Inv := Ifor .
66
66- xin 2: xapp spec_index; xstep; xif⇒ [?|]; xgo.
2
1
: spvspv(mind [i], mval [i], xind, xval )6#
xin 1: xgo.
6 h2, ji j 2[0,N ) : sv_get(mind [i], mval [i],j)6
rewrite index_nodup //; try math. (* simplify goal *)6 h3, ji
j 2[0,N ) : sv_get(xind , xval ,j)4(* § 2.4 *)xsubst (fun (2,i,j) ⇒ (2,j)).
(yind, yval
§2.5 (mind [i], mval [i](* § 2.5 *)42
1: spvspv(yind, yval, xind, xval )xapp spec_spvspv.
6
6 h2, ji j 2[0,N ) : sv_get(yind, yval,j)
xsimpl⇒->; xstep; xsimpl*. (* store result of spvspv *)6(* solve arithmetic to adjust big summations in precondition *) 6 h3, ji
j 2[0,N ) : sv_get(xind , xval ,j)4
Qed.
<latexit sha1_base64="oZWxhmklKBgXkjk1W8vawWyUHUU=">AAAB8HicbVBNS8NAEJ3Ur1q/qh69LBbBU0mkqMeiF48V7Ie0oWw2m3bpbjbsboQS+iu8eFDEqz/Hm//GTZuDtj4YeLw3w8y8IOFMG9f9dkpr6xubW+Xtys7u3v5B9fCoo2WqCG0TyaXqBVhTzmLaNsxw2ksUxSLgtBtMbnO/+0SVZjJ+MNOE+gKPYhYxgo2VHgec4lAbWRlWa27dnQOtEq8gNSjQGla/BqEkqaCxIRxr3ffcxPgZVoYRTmeVQappgskEj2jf0hgLqv1sfvAMnVklRJFUtmKD5urviQwLracisJ0Cm7Fe9nLxP6+fmujaz1icpIbGZLEoSjkyEuXfo5ApSgyfWoKJYvZWRMZYYWJsRnkI3vLLq6RzUfcu6437Rq15U8RRhhM4hXPw4AqacActaAMBAc/wCm+Ocl6cd+dj0Vpyiplj+APn8wdxmJAv</latexit>!

<latexit sha1_base64="oZWxhmklKBgXkjk1W8vawWyUHUU=">AAAB8HicbVBNS8NAEJ3Ur1q/qh69LBbBU0mkqMeiF48V7Ie0oWw2m3bpbjbsboQS+iu8eFDEqz/Hm//GTZuDtj4YeLw3w8y8IOFMG9f9dkpr6xubW+Xtys7u3v5B9fCoo2WqCG0TyaXqBVhTzmLaNsxw2ksUxSLgtBtMbnO/+0SVZjJ+MNOE+gKPYhYxgo2VHgec4lAbWRlWa27dnQOtEq8gNSjQGla/BqEkqaCxIRxr3ffcxPgZVoYRTmeVQappgskEj2jf0hgLqv1sfvAMnVklRJFUtmKD5urviQwLracisJ0Cm7Fe9nLxP6+fmujaz1icpIbGZLEoSjkyEuXfo5ApSgyfWoKJYvZWRMZYYWJsRnkI3vLLq6RzUfcu6437Rq15U8RRhhM4hXPw4AqacActaAMBAc/wCm+Ocl6cd+dj0Vpyiplj+APn8wdxmJAv</latexit>!

<latexit sha1_base64="oZWxhmklKBgXkjk1W8vawWyUHUU=">AAAB8HicbVBNS8NAEJ3Ur1q/qh69LBbBU0mkqMeiF48V7Ie0oWw2m3bpbjbsboQS+iu8eFDEqz/Hm//GTZuDtj4YeLw3w8y8IOFMG9f9dkpr6xubW+Xtys7u3v5B9fCoo2WqCG0TyaXqBVhTzmLaNsxw2ksUxSLgtBtMbnO/+0SVZjJ+MNOE+gKPYhYxgo2VHgec4lAbWRlWa27dnQOtEq8gNSjQGla/BqEkqaCxIRxr3ffcxPgZVoYRTmeVQappgskEj2jf0hgLqv1sfvAMnVklRJFUtmKD5urviQwLracisJ0Cm7Fe9nLxP6+fmujaz1icpIbGZLEoSjkyEuXfo5ApSgyfWoKJYvZWRMZYYWJsRnkI3vLLq6RzUfcu6437Rq15U8RRhhM4hXPw4AqacActaAMBAc/wCm+Ocl6cd+dj0Vpyiplj+APn8wdxmJAv</latexit>!

<latexit sha1_base64="oZWxhmklKBgXkjk1W8vawWyUHUU=">AAAB8HicbVBNS8NAEJ3Ur1q/qh69LBbBU0mkqMeiF48V7Ie0oWw2m3bpbjbsboQS+iu8eFDEqz/Hm//GTZuDtj4YeLw3w8y8IOFMG9f9dkpr6xubW+Xtys7u3v5B9fCoo2WqCG0TyaXqBVhTzmLaNsxw2ksUxSLgtBtMbnO/+0SVZjJ+MNOE+gKPYhYxgo2VHgec4lAbWRlWa27dnQOtEq8gNSjQGla/BqEkqaCxIRxr3ffcxPgZVoYRTmeVQappgskEj2jf0hgLqv1sfvAMnVklRJFUtmKD5urviQwLracisJ0Cm7Fe9nLxP6+fmujaz1icpIbGZLEoSjkyEuXfo5ApSgyfWoKJYvZWRMZYYWJsRnkI3vLLq6RzUfcu6437Rq15U8RRhhM4hXPw4AqacActaAMBAc/wCm+Ocl6cd+dj0Vpyiplj+APn8wdxmJAv</latexit>

26
27
28
29
30
31
32
33
34
42

!

<latexit sha1_base64="oZWxhmklKBgXkjk1W8vawWyUHUU=">AAAB8HicbVBNS8NAEJ3Ur1q/qh69LBbBU0mkqMeiF48V7Ie0oWw2m3bpbjbsboQS+iu8eFDEqz/Hm//GTZuDtj4YeLw3w8y8IOFMG9f9dkpr6xubW+Xtys7u3v5B9fCoo2WqCG0TyaXqBVhTzmLaNsxw2ksUxSLgtBtMbnO/+0SVZjJ+MNOE+gKPYhYxgo2VHgec4lAbWRlWa27dnQOtEq8gNSjQGla/BqEkqaCxIRxr3ffcxPgZVoYRTmeVQappgskEj2jf0hgLqv1sfvAMnVklRJFUtmKD5urviQwLracisJ0Cm7Fe9nLxP6+fmujaz1icpIbGZLEoSjkyEuXfo5ApSgyfWoKJYvZWRMZYYWJsRnkI3vLLq6RzUfcu6437Rq15U8RRhhM4hXPw4AqacActaAMBAc/wCm+Ocl6cd+dj0Vpyiplj+APn8wdxmJAv</latexit>!

Fig. 13. Mechanised LGTM proof of spmspv (left) and the corresponding paper-and-pencil derivation (right).

Moving on with the proof, we achieve the eﬀect of the Focus rule from Sec. 2.2 by calling xfocus
tactic at line 11. As the result, the index set of the second component will be divided into twogroups, as per the tactic’s second argument: inside 𝑚 idx × [0, 𝑁 ) and outside of it. Subsequently, thelines 12-13 verify the runs of uscr_get outside of 𝑚 idx × [0, 𝑁 ), using the speciﬁcation of uscr_get
via xapp tactic. In the rest of the proof, we ﬁrst divide the index set into a union of |𝑚 idx | batches,
to apply the For rule (lines 21-24). Next, at line 26 we apply the xfor tactic, replicating the steps
from Sec. 2.3, followed by an application of the xsubst, which performs the domain substitution
from Sec. 2.4. We conclude the proof by using an independently veriﬁed speciﬁcation of spvspv(line 33), discharging the residual obligations about index set manipulations (lines 34-42).
4.2

Proof Automation for Separation and Parametrisation

The two enabling features of LGTM, modularity via separation and parametrisation, come withadditional obligations in rules that exercise them. Those obligations have to do with (a) proving
assertion locality (Sec. 2.1.2) when reducing triple arity and (b) changing indices within assertions
when performing domain substitution with arbitrary index sets (Sec. 2.4). Below, we describe two
proof automation techniques that eliminate the proof burden associated with those obligations.
4.2.1 Discharging Locality Obligations. Tactics that generate proof obligations for locality of hyperheap assertions include xprod (which implements the Product rule) and xfor (which implements
For). For instance, the application of xfor at line 26 of Fig. 13 generates a number of subgoals
requiring one to establish locality of the assertions 𝑅𝑖 used as preconditions for programs in therespective components (cf. Fig. 6). Even a subgoal for the third component looks a bit intimidating:Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

Mechanised Hypersafety Proofs about Structured Data

𝑁 −1

𝑁 −1

local

173:17!

∗ arr(x ⟨3, 𝑖⟩ , 𝑥 ) ∗ ∗ arr(x ⟨3, 𝑖⟩ , 𝑥 ) , {⟨3, 𝑖⟩ : 𝑖 ∈ [0, 𝑁 )}
𝑖=0

ind

ind

𝑖=0

val

val

!

To dispatch such goals, we provide the xlocal tactic 1 Ltac xlocal := intros;
shown Fig. 15. In a nutshell, this tactic, structurally decom- 2 match goal with
(P1 \* P2) _ ⇒poses the hyper-heap assertion in a goal, reducing locality 34 | |- local
apply local_conj; xlocal
of a composite assertion to locality of its parts. For instance, 5 | |- local (\*_(i ∈ s) Pi) _ ⇒apply local_big_conj; xlocal
lines 3-4 of the tactic reduce locality of 𝑃1 ∗ 𝑃 2 to local- 6(arr(p(i), l)) s ⇒ity of both 𝑃1 and 𝑃 2 , calling xlocal recursively on those 78 | |- local
apply local_array; indomE
subgoals. Lines 5-6 we reduce locality of 𝑖 ∈𝑆 𝐻𝑖 to the lo- 9 ...
cality of 𝑃𝑖 for each 𝑖 ∈ 𝑆. Finally, whenever xlocal reaches 10 end
terminal goals such as local ( arr (𝑝 (𝑖), 𝑙), 𝑆), it applies theFig. 14. xlocal tactic
local_array lemma, resulting in the obligation 𝑖 ∈ 𝑆, provenby the indomE membership solver from the MathComp library (Mahboubi and Tassi 2022).

∗

4.2.2 Automating Index Set Substitution. The need for proof automation in the presence of parametrisation manifests whenever we want to perform reindexing involving arbitrary index sets via the
Subst rule. As Subst applies a substitution function 𝜙 to both pre- and postcondition, 𝜙 must be
distributed over the connectives of the LGTM including, separation conjunction and its iterated
version (big- ). One naïve approachto implement
such distribution automatically would involve
proving a lemma of the form 𝜙,𝑖 ∈𝑆 𝐻𝑖 =𝑖 ∈𝑆 𝜙 [𝐻𝑖 ] for distributing the substitution overand use it for repeated rewriting in the assertions. Unfortunately, this solution does not combine
well with the shallow embedding of “big” operators into Coq, that implement indexing over 𝑖
via Coq’s lambda-functions. As the inner assertions 𝐻𝑖 of 𝑖 ∈𝑆 𝐻𝑖 might depend on the lambdabound 𝑖, rewriting them would require independently instantiating the equality lemmas such as∀𝑃, 𝑄. 𝜙 [𝑃 ∗ 𝑄] = 𝜙 [𝑃] ∗ 𝜙 [𝑄] with assertions that depend on 𝑖 and are not well-formed outsideof the lambda. Therefore, after we rewrite an assertion involving
using the above equality once,
the application of 𝜙 will occur in the scope of the binder 𝑖, preventing its further rewrites.
We overcome this hurdle with the following trick. 1 Ltac xsubst := match goal with
When performing domain substitution via 𝜙, we start 2 | |- 𝜙 [P1 \* P2] = ?H ⇒rewrite subst_conj;
with replacing the precondition 𝜙 [P] (resp. 𝜙 [Q]) with a 34
apply conj_eq; xsubst
fresh existential variable ?H, adding a subgoal 𝜙 [P] = ?H 5 | |- 𝜙 [\*_(i ∈ s) Pi] = ?H ⇒rewrite subst_big_conj;
to the set of proof obligations. This subgoal will be re- 6
big_conj_eq; intros; xsubst
peatedly transformed as we gradually propagate 𝜙 inside 78 | |- 𝜙apply[arr(p(i), l)] = ?H ⇒P, elaborating ?H as we go. This idea is implemented by 9
rewrite subst_array; reflexivity
xsubst tactic shown in Fig. 15. To understand its eﬀect 10 ...
on the proof, consider the lines 6-8 of its deﬁnition that 11 end
Fig. 15. xsubst tactic
deal with the big- operator. The tactic implementation
ﬁrst propagates 𝜙 under the big-star by performing the rewrite via the subst_big_conj lemma, followed by application of the big_conj_eq lemma of type (∀𝑖, 𝐻𝑖 = 𝑃𝑖 ) ⇒ 𝑖 ∈𝑆 𝐻𝑖 = 𝑖 ∈𝑆 𝑃𝑖 , whichis essentially a specialised version of the functional extensionality axiom. Applying this lemma
instantiates the existential variable ?H with 𝑖=0 (?Hi 𝑖), producing a subgoal ∀𝑖, (𝜙 [𝑃𝑖 ] = ?Hi 𝑖),
which will require further elaboration of ?Hi. The tactic subsequently ﬁxes the binder 𝑖 by moving
it to the proof context using intros, followed by a recursive call of xsubst.
When xsubst reaches primitive heap assertions such as arr (𝑝 (𝑖), 𝑙), it rewrites them using suitablelemmas (e.g., turning arr (𝑝 (𝑖), 𝑙) into arr (𝑝 (𝜙 (𝑖)), 𝑙) via subst_array), dispatching the residual goalby using Coq’s standard reflexivity tactic that instantiates the remaining existential variable.

∗

∗

∗

∗

∗

∗

∗

∗

∗

∗

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:18

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

Table 1. Statistics for the verified programs. For each program, we specify its operation in Einstein notation,
the formats of the involved operands (D is for dense), and the return type, followed by the size of the codeand of the mechanised LGTM proof, along with the proof/code ratio. We also indicate the characteristic rulesof LGTM the auxiliary specifications used by the proof, as well the time it takes Coq to check it.
#
1
2
3
4
5
6
7
8
9
10
11
12
13

Operation
Í
𝑥
Í𝑖 𝑖
𝑥𝑦
Í𝑖 𝑖 𝑖𝑥𝑦
Í𝑖 𝑖 𝑖
𝐴𝑖,𝑗
Í𝑖,𝑗
𝐴𝑖,𝑗
𝑖,𝑗
Í
𝐴𝑖,𝑗 𝑥 𝑗𝑗Í𝐴 𝑥Í𝑗 𝑖,𝑗 𝑗
𝐴𝑖,𝑗
𝑖,𝑗
Í
𝐴
𝑥𝑗
𝑖,𝑗
Í𝑗
𝑗Í𝐴𝑖,𝑗 𝑥 𝑗𝑥
Í 𝑖 𝑖
𝛼𝑥𝑖 + 𝛽𝑦𝑖𝑖Í𝑗 𝐴𝑖,𝑗 𝑥 𝑗Formats(Operands)

ReturnType

Size (LOC)
Code Proof

Ratio

SV (𝑥)1,2
SV (𝑥), D (𝑦)1,2
SV (𝑥), SV (𝑦)1,2
COO (𝐴)
CSR (𝐴)1,2
CSR (𝐴), D (𝑥)1,2
CSR (𝐴), SV (𝑥)1,2
uCSR (𝐴)uCSR (𝐴), D (𝑥)3uCSR (𝐴), SV (𝑥)3
RL (𝑥)2
RL (𝑥), RL (𝑦)2
CSR (𝐴), D (𝑥)4

int
int
int
int
int
int[]
int[]
int
int[]
int[]
int
int
double[]

9
12
31
7
10
10
10
10
11
11
16
64
19

2.4
1.8
7.6
3.6
1.1
1.2
1.6
2.9
3.0
2.7
1.1
2.2
1.9

1 From (Kjolstad et al. 2017)

2 From (Ahrens et al. 2023)

22
22
237
25
11
12
16
29
33
30
18
143
36

For

Prominent rules
While Focus Subst

✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓

✓
✓
✓
✓

✓
✓
✓

✓
✓
✓
✓
✓
✓

✓

✓

✓
✓

3 From (Hong et al. 2019)

Uses

#1
#2
#3
#1
#2
#3

Time
(sec)
5.42
6.96
20.73
5.40
7.91
8.99
11.02
12.62
18.69
20.05
5.90
41.66
31.76

4 From (Kellison et al. 2023)

5 LGTM UNDER THE SPOTLIGHT: EMPIRICAL EVALUATION
We conducted an empirical evaluation of LGTM to answer the following research questions:• RQ1: Is LGTM expressive enough to reason about real-world computations on structured data?
• RQ2: How LGTM proofs are inﬂuenced by the involved formats and kinds of computations?
• RQ3: How does LGTM fare against state-of-the-art approaches not based on relational logic?
Benchmarks. We have assembled our benchmark suite by adopting case studies from diﬀerent
sources, including programs produced by the TACO (Kjolstad et al. 2017) and Finch (Ahrens et al.
2023) compilers, notable benchmarks from the Sparse Suite collection (Hong et al. 2019), and an
example from a recent eﬀort on verifying sparse matrix/vector multiplication (Kellison et al. 2023).
The conversion of the selected programs from their implementation languages, C and Julia, to thelanguage of LGTM (Fig. 10) has been done manually, but could be easily automated.
The resulting collection of 13 programs is summarised in Tab. 1. The programs were selectedto feature diverse range of data formats and operations. The considered formats can be broadlyclassiﬁed into three groups: (1) primitive sparse tensor formats, such by SV and Coordinate List
(COO) (Popoola et al. 2023), (2) composite sparse tensor data formats, CSR and uCSR, that incorporate
primitive formats as their parts, and (3) a data format for non-sparse structured data, represented by
Run-Length Encoding (RL) (Donenfeld et al. 2022). For each such format group, we considered themost common operations with the respective data implemented in real-world kernels: dot-productand alpha-blending for vector formats, and matrix/vector multiplication for matrix formats. All theveriﬁed programs listed in Tab. 1 are parametrised with arbitrary sizes of matrices/vectors.
5.1 RQ1: Expressivity of the Logic
We answer RQ1 by providing quantitative evidence of LGTM’s eﬀectiveness and eﬃciency whenverifying characteristic programs manipulating with structured data listed in Tab. 1.
A quick glance at the table’s ﬁfth and sixth column should convey that LGTM’s proofs are
relatively compact, especially for an extrinsic veriﬁer, such as Coq, with the average proof/code
ratio (in LOC) being 2.5. One notable outlier in this aspect is a dot-product of two sparse vectors (#3),
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

Mechanised Hypersafety Proofs about Structured Data

173:19whose proof we will discuss in Sec. 5.2. The last column of Tab. 1 reports the proof checking times(averaging at 15.2s), obtained via Coq 8.18 on a 3.2 GHz Apple M1 MacBook Air with 16GB RAM.
The time it takes Coq to check LGTM proofs is directly inﬂuenced by the number of uses of tactics
that implement domain-speciﬁc automation, such as xsubst and xlocal (cf. Sec. 4.2.2).
5.2 RQ2: Verification Trends
Besides quantitative characteristics of LGTM, such as proof sizes and proof checking time, we arealso interested in veriﬁcation trends. For instance, what rules one should expect to use when dealing
with a particular format or a kind of structured data computation?
To answer this question, we start by considering the programs #1-#4 involving primitive formats
SV and COO for sparse vectors and matrices, which are used as “building blocks” by other formats
The veriﬁcation trends for these programs are summarised in the seventh column of Tab. 1, featuring(1) the Focus rule, required to focus only on non-zero elements of the input tensor and (2) the For
or While rules, depending on the type of the loop in the code, required to group remaining nonzero elements with correspondent loop iterations. Next, we focus on the case studies #5-#10 withcomposite formats, CSR and uCSR, which are obtained as combinations of a dense representation,
SV (for exploiting sparsity), and COO (for featuring random permutation of the components). The
key proof principle of LGTM that shows up prominently in those proofs is Subst. This should notcome as a surprise: because of the composite nature of the formats, one should expect to makeuse of the speciﬁcations that involve their sub-formats (e.g., SV is a part of CSR). Using Subst
allows one to adjust intermediate subgoals within the proof to match speciﬁcations of “auxiliary”
operations (most of which are represented by case studies #1-#4) so they could be used in the
proof in a compositional manner. As the penultimate column of Tab. 1 indicates, the case studies#5-#10 that involve composite data formats, reuse a proof of some case study #1-#3, involving
only primitive formats. Finally, we consider the case studies #11-#12, in which we have veriﬁed
operations on RL encoding that manipulate with compressed arrays containing repeated data. In
those proofs, we made use only of LGTM’s loops rules, as the RL format is primitive (so we don’t
need Subst) and is not sparse (so we don’t need to focus on non-zero elements via Focus).
We conclude this subsection with an observation about the only example from our collection thathas a relatively large proof/code ratio (7.6): a dot-product of two SV vectors (#3). This ﬁgure canbe explained by the fact that the textbook implementation of SV/SV product is heavily optimisedby skipping as many unnecessary computations (involving zeros) as possible. Hence the main
complexity in the proof is because of the need to justify the absence of code, rather than its presence.
5.3

RQ3: Comparison with Non-Relational Proofs

The landscape of tools for veriﬁed computations on structured data is somewhat scarce, with theprior work mostly focusing on veriﬁed compilers for sparse tensors (Arnold et al. 2010; Dyer et al.
2019; Kovach et al. 2023). Those tools, which we discuss in detail in Sec. 6, can only produce a
subset of computations that can be veriﬁed in LGTM, and they are not guaranteed to produce themost performant format-speciﬁc code. The various existing logics for 𝑘-safety either do not oﬀer
means to work with array computations (Dardinier and Müller 2024; Sousa and Dillig 2016), or are
not even mechanised (D’Osualdo et al. 2022), thus making it impossible to conduct a meaningfulcomparison with them as tools. Therefore, we only compare veriﬁcation in LGTM with formal
reasoning about structured data in a mechanises general-purpose non-relational Separation Logic.
Recent work by Kellison et al. (2023) presented a mechanised proof of a sparse matrix/dense vector
product function implemented in C, taking a sparse matrix in the CSR format. The C implementationis speciﬁed and veriﬁed using the Veriﬁed Software Toolchain (VST) (Appel 2011), a Separation
Logic framework embedded into Coq. Kellison et al.’s proofs follows a relatively conventional
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:20

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

1 Inductive crs_row_rep {t} : ∀ cols (vals:list
2 (ftype t)) col_ind (v:list (ftype t)), Prop :=1 Definition crs_rep_aux {t} (mval : matrix t) cols
2 (vals: list (ftype t)) col_ind row_ptr: Prop :=3 | crs_row_rep_nil: crs_row_rep 0%Z nil nil nil
4 | crs_row_rep_zero: ∀ cols vals col_ind v,
5
crs_row_rep (cols-1) vals (map pred col_ind) v ->3 (* propositions about sortedness and lengths *) ∧4 ∀ j, 0 <= j < Zlength mval ->5 crs_row_rep cols (sublist (Znth j row_ptr)

6
crs_row_rep cols vals col_ind (Zconst t 0 :: v)
7 | crs_row_rep_val: ∀ cols x vals col_ind v,

6(Znth (j+1) row_ptr) vals)
7 (sublist (Znth j row_ptr) (Znth (j+1) row_ptr)
8
col_ind) (Znth j mval ).

89

crs_row_rep (cols-1) vals (map pred col_ind) v ->crs_row_rep cols (x::vals) (0::col_ind) (x::v).

(a) Inductive predicate for relating a vector v withlength cols and its corresponding sparse vector
represented by col_ind and vals.

(b) Predicate for relating a dense matrix mval
modelled as a list and a sparse matrix in CSR,
represented by row_ptr, col_ind, and vals.

Fig. 17. Encoding of CSR format in VST by Kellison et al. (2023); ftype t is a type for floating point numbers.

two-layer paradigm for verifying imperative code (Appel 2022): ﬁrst a functional model of sparse
matrices is deﬁned, along with its operations (e.g., computing the dot-product of a matrix row anda dense vector); next, the C function is ascribed a speciﬁcation in terms of a functional model, andthe veriﬁcation amounts to proving that the imperative function reﬁnes the functional operation.
Fig. 16 presents a slightly simpliﬁed CSR sparse 1 def spmv(m_idx, m_ind, m_val, v):
matrix/dense vector product implementation ver- 2 for i in range(0, length(m_idx)):
iﬁed in Kellison et al.’s LAProof framework. The 3
for j in range(m_idx[i], m_idx[i+1]):
ans[i] += m_val[j] * v[m_ind[j]]outer loop iterates through the rows of a compressed 4
CSR matrix m and the inner loop sums up all nonFig. 16. CSR matrix/dense vector productzero m elements in each row, multiplied by the respective values of a dense vector v. The functional model of CSR is deﬁned using a family of
inductive predicates. First, the inductive predicate crs_row_rep (Fig. 17a) relates the contents of adense vector and its sparse representation, capturing the shape of the SV format. Next, crs_rep_aux(Fig. 17b) uses crs_row_rep to express the relation between a dense matrix and the corresponding
CSR matrix. Finally, an SL representation predicate crs_rep (omitted for brevity) relates a dense
matrix to its sparse counterpart (constrained by crs_rep_aux) stored as a C struct in the memory.
The predicate crs_rep is used in the pre/postconditions of the speciﬁcation, and the postcondition
states that the returned vector is exactly the result of multiplying the input dense matrix and adense vector. The LAproof veriﬁcation proceeds as follows:(1) Prove that the inner loop accumulates into ans[i] all values in the array m_val corresponding
to the 𝑖 th row, multiplied by respective values of v using the invariant𝑗Õ
𝐼 ( 𝑗) ≜ ans[𝑖] =mval [𝑘] · 𝑣 [mind [𝑘]]𝑘=midx [𝑖 ](2) For any 𝑖 at the end of the loop, replace the sum at the right hand side of the equality in theinvariant with the product of the corresponding rows of the logical “dense” matrix m and thevector v. This rewrite requires leveraging the properties of the representation predicate csr_rep,
connecting the contents of m_idx, m_ind, and m_val with the elements of the logical matrix m(including zeros), via a set of predicate-speciﬁc lemmas.
(3) Verify the outer loop using an invariant stating that at 𝑖 th iteration, for each 𝑘 < 𝑖, ans [𝑘] =m [𝑘] · v, where m[k] is an 𝑘 th row of the logical matrix m.
The most laborious part of this proof is its second step. It requires a whole separate ﬁle with 350
LOC of Coq code to prove a number of bespoke facts about csr_rep. Those facts are needed to“align” the representation predicate, which necessarily describes the entire contents of the matrix m,with the logic of the inner loop of the code above, which only operates on m’s non-zero values.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

Mechanised Hypersafety Proofs about Structured Data

173:21

In contrast, our approach does not require one to design such tailored functional model for eachnew sparse format. Instead, with LGTM, one can use access functions (e.g., sv_get) for interpretingthe formats, relating their results to that of the main function being speciﬁed. Those access functions
can be executed “on demand” in lockstep with the respective parts of the operation’s implementationand veriﬁed with a comparatively low proof overhead. This highlights a conceptual advantage of
our approach: it liberates the user from the burden associated with (𝑖) designing functional format
deﬁnitions and (𝑖𝑖) proving their properties that are typically required in reﬁnement proofs.
To further demonstrate how our approach facilitates proofs about sparse matrices, we conducted
the veriﬁcation task from Kellison et al.’s work in LGTM, which is marked as the case study #13
in Tab. 1. In the interest of fair comparison, the program #13 diﬀers from a similar implementation #6
in the following aspects: (a) it works on the domain of IEEE 64-bit ﬂoating point numbers insteadof integers, and (b) it does not call sub-functions (e.g., #2) to keep the full resemblance to the C
program by Kellison et al., which does not depend on sub-procedures that operate with sparse
vectors. To verify the inner loop of smpv in Fig. 16 in LGTM, we ﬁrst replace the manipulations withthe matrix contents via m_ind and m_val by manipulations directly with the contents of its logicalrow m [𝑖], so that the remaining goal is conceptually reduced to a vector/vector product. And thenalign each 𝑖 th iteration of the inner loop with a matching access function call for the 𝑖 th non-zeroelement of the matrix’s row m [𝑖], and prove that the “logical” iterations corresponding to zeros canbe ignored. Veriﬁcation of the outer loop is similar to the one presented in Sec. 2.
To summarise, we note that, instead of inventing a data representation predicate and proving
lemmas about it, LGTM proof is mostly about “aligning” calls to access functions with the code
being veriﬁed. That is why, from Tab. 1, our proof, even without composition, is only 36 LOC.
In Kellison et al.’s work, the proofs about CSR-speciﬁc properties alone take 210 LOC, and thereﬁnement proof takes additional 204 LOC, making our proof less than a tenth of their total length.
6 RELATED WORK
Our work connects several lines of research on (a) program logics for relational safety properties,(b) compilers for structured data, and (c) veriﬁcation of structured data manipulations.
Relational program logics. Benton’s seminal work (2004) introduced Relational Hoare Logic (RHL)
to capture safety properties of pairs of programs and prove them using lockstep rules. RHL’s
extension to Separation Logic (Yang 2007) has been used to specify and verify complex relational
properties of heap-manipulating programs, such as equivalence of heap-based graph-marking
algorithms. Barthe et al. (2011) proposed a method to encode reasoning about 2-safety properties inunary Hoare logic by considering product programs that simulate the execution steps of both theirconstituents. More recently, Sousa and Dillig (2016) introduced Cartesian Hoare Logic (CHL) thatallows one to express and prove 𝑘-safety properties of imperative programs for arbitrary but ﬁxed 𝑘.
CHL comes with the automated veriﬁer Descartes that proves hypersafety speciﬁcations by
reducing them to unary Hoare triples. None of these approaches support reasoning about familiesof programs indexed by elements of an arbitrary ﬁnite set that can change within the proof.
A recent work by Dardinier and Müller (2024) introduced Hyper Hoare Logic (HHL)—a framework
to reason about 𝑘-safety properties of arbitrary (even inﬁnite) arity 𝑘. Unlike LGTM, HHL only
allows for 𝑘-safety speciﬁcations constraining multiple runs of the same program. Similarly to
LGTM, in HHL the arity of a judgement can change during the proof, for instance in its Cons
rule. This feature is, however, not exploited by HHL, which does not provide specialised rules
for reasoning about loops, such as LGTM’s For and While. The closest to our work is Logic forHyper-triple Composition (LHC) by D’Osualdo et al. (2022). We provided a detailed discussion on
the improvements LGTM makes over LHC in terms of expressivity in Sec. 3.2.
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:22

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

Compilers for structured data manipulations. Sparsity is a well-studied example of structured data,with wide-ranging applications from machine learning to scientiﬁc computing. A popular strategy
for sparse tensor compilation is to generate low-level code directly from high-level abstractions(Kjolstad et al. 2019). The TACO tensor compiler is emblematic of the approach, deﬁning sparsetensor formats through an iterator interface for non-zero elements (Chou et al. 2018, 2020), generating an implementation of an operation for the sparse representations from the same operation
on dense arrays. Later works generalised TACO’s format abstraction to capture dynamic data
structures (Chou and Amarasinghe 2022), multiple simultaneous formats (Ye et al. 2023), repetition (Donenfeld et al. 2022), or ragged-style irregularity (Fegade et al. 2022). Many such approaches
were uniﬁed and generalised by the Finch compiler (Ahrens et al. 2023), which goes beyond sparsity
and allows one to deﬁne arbitrary iteration strategies for producing eﬃcient looping code.
Veriﬁed computations with structured data. Arnold et al. (2010) proposed a high-level functional
language LL for expressing computations with sparse tensors that facilitates automation of correctness proofs about matrix manipulations in Isabelle/HOL. The approach by Arnold et al. is, however,
only limited to sparse formats that can be encoded in LL. Furthermore, it assumes correctness ofthe compilation from the LL encoding to the C representation (Arnold 2011). That is, the correctness
guarantees provided by the approach only apply to LL programs, but not to their C counterparts.
Dyer et al. (2019) suggested to encode sparse formats and computation as Alloy predicates,
phrasing veriﬁcation of sparse tensor computations as a search for counterexamples. Such veriﬁcation is unsound, in the sense that Alloy tries to ﬁnd only small counterexamples up to a certain
bound. Moreover the way to encode stateful programs in Alloy proposed by Dyer et al. is only
capable to capture programs with nested for-loops and could not express, e.g., spmspv from Sec. 2.
Liu et al. (2022) developed a Coq library for certiﬁed optimisations of tensor-manipulating program via veriﬁed rewrites. Those rewrites do not exploit the structure of speciﬁc data formats,and, hence, are not guaranteed to produce optimised implementations. Finally Kovach et al. (2023)
presented Etch, a veriﬁed (in Lean) compiler for sparse data computations. Etch is limited tooperations on structures that are expressible as mappings over indexed streams, so its optimisations
can be expressed as stream fusion, hierarchical iterations, and control over interaction order (Kiselyov et al. 2017). This restricts the range of operations Etch can synthesise: for instance, it cannot
generate computations on data with unordered layers, such as COO and uCSR formats.
Unlike the listed above eﬀorts, LGTM is not a compiler, but is a veriﬁcation framework: it does
not synthesise computations, but oﬀers means to mechanically verify the results produced by highly
ﬁne-tuned unveriﬁed synthesisers, such as TACO. This makes it a suitable veriﬁcation back-end
for certifying sparse data compilers, which are yet to be developed. Furthermore, the applicationsof LGTM are not limited to just sparse data: for example, our case studies #11-12 from Tab. 1 areabout the run-length encoding for arrays with repeated values.
7 CONCLUSION AND FUTURE WORKIn this work we presented LGTM: a program logic for hypersafety properties, built around the idea
of parametrised 𝑘-safety speciﬁcations. We argued that parametrisation enables intuitive safety
proofs about intricate computations over structured data (e.g., sparse tensors), and substantiatedthis claim by mechanically verifying thirteen case studies using LGTM embedding into Coq.
In our immediate future work, we are planning to automate common reasoning patterns of LGTM
to facilitate push-the-button construction of machine-assisted proofs for parametrised hypersafety
speciﬁcations. As our long-term agenda, we are aiming to use LGTM as a foundation for building
a certifying compiler for structured data manipulations similar to Finch (Ahrens et al. 2023) byadopting the ideas of proof-producing program synthesis (Watanabe et al. 2021).
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

Mechanised Hypersafety Proofs about Structured Data

173:23

ACKNOWLEDGMENTS
We thank Andrew Appel, Kiran Gopinathan, Yunjeong Lee, Peter Müller, and George Pîrlea for their
feedback on drafts of this paper. We also thank the anonymous PLDI’24 PC and AEC reviewers
for their constructive and insightful comments. This work was partially supported by a Singapore
Ministry of Education (MoE) Tier 3 grant “Automated Program Repair” MOE-MOET32021-0001
and MoE Tier 1 grant T1 251RES2108 “Automated Proof Evolution for Veriﬁed Software Systems”.
DATA AVAILABILITY
The software artefact accompanying this paper is available online (Gladshtein et al. 2024a). The
artefact contains the source code and build scripts for the Coq mechanisation of LGTM, as well as
the collection of case studies that can be used to reproduce the results described in Sec. 5.
REFERENCES
Willow Ahrens, Daniel Donenfeld, Fredrik Kjolstad, and Saman P. Amarasinghe. 2023. Looplets: A Language for Structured
Coiteration. In CGO. ACM, 41–54. https://doi.org/10.1145/3579990.3580020
Andrew W. Appel. 2011. Veriﬁed Software Toolchain - (Invited Talk). In ESOP (LNCS, Vol. 6602). Springer, 1–17. https://doi.org/10.1007/978-3-642-19718-5_1
Andrew W. Appel. 2022. Coq’s vibrant ecosystem for veriﬁcation engineering (invited talk). In CPP. ACM, 2–11. https://doi.org/10.1145/3497775.3503951
Gilad Arnold. 2011. Data-Parallel Language for Correct and Eﬃcient Sparse Matrix Codes. Ph. D. Dissertation. University ofCalifornia, Berkeley, USA. http://www.escholarship.org/uc/item/2pw6165p
Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík, and Mooly Sagiv. 2010. Specifying and verifying sparse
matrix codes. In ICFP. ACM, 249–260. https://doi.org/10.1145/1863543.1863581
Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011. Relational Veriﬁcation Using Product Programs. In FM (LNCS,
Vol. 6664). Springer, 200–214. https://doi.org/10.1007/978-3-642-21437-0_17
Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. 2012. Probabilistic relational reasoning fordiﬀerential privacy. In POPL. ACM, 97–110. https://doi.org/10.1145/2103656.2103670
Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations. In POPL. ACM,
14–25. https://doi.org/10.1145/964001.964003
Michael Carbin, Deokhwan Kim, Sasa Misailovic, and Martin C. Rinard. 2012. Proving acceptability properties of relaxednondeterministic approximate programs. In PLDI. ACM, 169–180. https://doi.org/10.1145/2254064.2254086
Arthur Charguéraud. 2011. Characteristic Formulae for the Veriﬁcation of Imperative Programs. In ICFP. ACM, 418–430.
https://doi.org/10.1145/2034773.2034828
Arthur Charguéraud. 2020. Separation Logic for Sequential Programs (Functional Pearl). Proc. ACM Program. Lang. 4, ICFP
(2020), 116:1–116:34. https://doi.org/10.1145/3408998
Stephen Chou and Saman P. Amarasinghe. 2022. Compilation of dynamic sparse tensor algebra. Proc. ACM Program. Lang.
6, OOPSLA2 (2022), 1408–1437. https://doi.org/10.1145/3563338
Stephen Chou, Fredrik Kjolstad, and Saman P. Amarasinghe. 2018. Format abstraction for sparse tensor algebra compilers.
Proc. ACM Program. Lang. 2, OOPSLA (2018), 123:1–123:30. https://doi.org/10.1145/3276493
Stephen Chou, Fredrik Kjolstad, and Saman P. Amarasinghe. 2020. Automatic generation of eﬃcient sparse tensor format
conversion routines. In PLDI. ACM, 823–838. https://doi.org/10.1145/3385412.3385963
Thibault Dardinier and Peter Müller. 2024. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties. Proc. ACM Program.
Lang. 8, PLDI (2024), 207:1–207:24. https://doi.org/10.1145/3656437
Daniel Donenfeld, Stephen Chou, and Saman P. Amarasinghe. 2022. Uniﬁed Compilation for Lossless Compression andSparse Computing. In CGO. IEEE, 205–216. https://doi.org/10.1109/CGO53902.2022.9741282
Emanuele D’Osualdo, Azadeh Farzan, and Derek Dreyer. 2022. Proving hypersafety compositionally. Proc. ACM Program.
Lang. 6, OOPSLA2 (2022), 289–314. https://doi.org/10.1145/3563298
Tristan Dyer, Alper Altuntas, and John W. Baugh Jr. 2019. Bounded Veriﬁcation of Sparse Matrix Computations. In
2019 IEEE/ACM 3rd International Workshop on Software Correctness for HPC Applications (Correctness). IEEE, 36–43.
https://doi.org/10.1109/Correctness49594.2019.00010
Pratik Fegade, Tianqi Chen, Phillip B. Gibbons, and Todd C. Mowry. 2022. The CoRa Tensor Compiler: Compilation
for Ragged Tensors with Minimal Padding. In MLSys. mlsys.org. https://proceedings.mlsys.org/paper/2022/hash/d3d9446802a44259755d38e6d163e820-Abstract.html
Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.

173:24

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey. 2024a. LGTM: the Logic forGraceful Tensor Manipulation. https://doi.org/10.5281/zenodo.10951930
Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey. 2024b. Mechanised Hypersafety
Proofs about Structured Data: Extended Version. CoRR abs/2404.06477 (2024). https://doi.org/10.48550/ARXIV.2404.06477
Changwan Hong, Aravind Sukumaran Rajam, Israt Nisa, Kunal Singh, and Ponnuswamy Sadayappan. 2019. Adaptive sparsetiling for sparse matrix multiplication. In PPoPP. ACM, 300–314. https://doi.org/10.1145/3293883.3295712
Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, and David Bindel. 2023. LAProof: A Library of Formal Proofs ofAccuracy and Correctness for Linear Algebra Programs. In ARITH. IEEE Computer Society, 36–43. https://doi.org/10.
1109/ARITH58626.2023.00021
Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, and Yannis Smaragdakis. 2017. Stream fusion, to completeness. In POPL.
ACM, 285–299. https://doi.org/10.1145/3009837.3009880
Fredrik Kjolstad, Willow Ahrens, Shoaib Kamil, and Saman Amarasinghe. 2019. Tensor Algebra Compilation with Workspaces.
In CGO. 180–192. https://doi.org/10.1109/CGO.2019.8661185
Fredrik Kjolstad, Shoaib Kamil, Stephen Chou, David Lugato, and Saman P. Amarasinghe. 2017. The tensor algebra compiler.
Proc. ACM Program. Lang. 1, OOPSLA (2017), 77:1–77:29. https://doi.org/10.1145/3133901
Scott Kovach, Praneeth Kolichala, Tiancheng Gu, and Fredrik Kjolstad. 2023. Indexed Streams: A Formal Intermediate
Representation for Fused Contraction Programs. Proc. ACM Program. Lang. 7, PLDI, Article 154 (2023). https://doi.org/
10.1145/3591268
Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, and Jonathan Ragan-Kelley. 2022. Veriﬁed tensor-program optimization
via high-level scheduling rewrites. Proc. ACM Program. Lang. 6, POPL (2022), 1–28. https://doi.org/10.1145/3498717
Assia Mahboubi and Enrico Tassi. 2022. Mathematical Components. https://doi.org/10.5281/zenodo.7118596
Aleksandar Nanevski, Anindya Banerjee, and Deepak Garg. 2011. Veriﬁcation of Information Flow and Access Control
Policies with Dependent Types. In 32nd IEEE Symposium on Security and Privacy. IEEE Computer Society, 165–179.
https://doi.org/10.1109/SP.2011.12
Tobi Popoola, Tuowen Zhao, Aaron St. George, Kalyan Bhetwal, Michelle Mills Strout, Mary Hall, and Catherine
Olschanowsky. 2023. Code Synthesis for Sparse Tensor Format Conversion and Optimization. In CGO. ACM, 28–40.
https://doi.org/10.1145/3579990.3580021
John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. IEEE Computer Society,55–74. https://doi.org/10.1109/LICS.2002.1029817
Laith Sakka, Kirshanthan Sundararajah, and Milind Kulkarni. 2017. TreeFuser: a framework for analyzing and fusing generalrecursive tree traversals. Proc. ACM Program. Lang. 1, OOPSLA (2017), 76:1–76:30. https://doi.org/10.1145/3133900
Marcelo Sousa and Isil Dillig. 2016. Cartesian Hoare Logic for Verifying k-Safety Properties. In PLDI. ACM, 57–69.
https://doi.org/10.1145/2908080.2908092
Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, and Ilya Sergey. 2021. Certifying the Synthesis of
Heap-Manipulating Programs. Proc. ACM Program. Lang. 5, ICFP (2021), 1–29. https://doi.org/10.1145/3473589
Hongseok Yang. 2007. Relational separation logic. Theor. Comput. Sci. 375, 1-3 (2007), 308–334. https://doi.org/10.1016/j.tcs.
2006.12.036
Zihao Ye, Ruihang Lai, Junru Shao, Tianqi Chen, and Luis Ceze. 2023. SparseTIR: Composable Abstractions for Sparse
Compilation in Deep Learning. In ASPLOS. ACM, 660–678. https://doi.org/10.1145/3582016.3582047

Received 2023-11-16; accepted 2024-03-31

Proc. ACM Program. Lang., Vol. 8, No. PLDI, Article 173. Publication date: June 2024.