<figure><img src="image_1.png" /></figure>

HAL
open science

Mechanizing the proof of a borrow calculus

Alban Reynaud Michez

<figure><img src="image_2.png" /></figure>

Alban Reynaud Michez. Mechanizing the proof of a borrow calculus. 2026. hal-05527340

HAL Id: hal-05527340

https://hal.science/hal-05527340v1

Preprint submitted on 25 Feb 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_3.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
Mechanizing the proof of a borrow calculus

Alban Reynaud Michez¹

¹Université Grenoble Alpes, CNRS, Grenoble INP, Verimag, France

Abstract

In an ICFP'24 article, Ho, Fromherz and Protzenko propose a model of Rust borrow-
checking. They provide a pen-and-paper proof of soundness, featuring original simulation
invariants, defined as transitive closures. However, it also involves huge case analyses that
are sometimes only sketched.

We started the formalization of this proof in the Rocq prover. For mechanizing their reasoning, we introduced conditional rewriting systems and reduced some well-formedness conditions to arithmetic inequalities that we discharge with Rocq linear integer arithmetic procedure. On the way, we found a flaw in the proofs of some of their fundamental lemmas. We repaired their methodology using techniques from rewriting theory. This article presents the current state of our formalization.

# 1 Introduction

The Rust programming language provides high-level abstractions for low-level system programming, with strong memory safety guarantees, making it an ideal replacement for C or C++. For example, it provides algebraic datatypes with pattern matching like ML. It also provides mutable references to the content of algebraic values, like in low-level C programming, while statically ensuring that mutations through such a reference remain safe.

Rust succeeds to reconcile performance by fine-grained memory control and memory safety,
thanks to a type system based on ownership, with references as a safe alternative to pointers.
A place (also called as lvalue) can be temporarily borrowed by a reference; this reference can
be mutable or shared (i.e. read-only); and at any time, a place can be either borrowed by one
mutable borrow, or by several shared borrows, but not both. The borrow discipline is enforced
by a component of the compiler called the borrow-checker.

Originally introduced for the Aeneas verification project [11], LLBC (*low-level borrow calculus*) is a model of safe Rust with a high-level memory centered around borrow. Borrow-checking is performed within a symbolic execution that abstracts LLBC operational semantics. In an ICFP’2024 article [10], Ho, Fromherz and Protzenko prove that their borrow-checking is sound w.r.t. an operational semantics over a standard heap-and-pointers memory model.

The nature of LLBC—briefly presented §2—induced particular challenges, because states are
represented as tree-like terms (reflecting the ownership discipline of Rust). Our first contribution
is to reformulate the semantics rules using operations on terms. These operations are related to
equations that define a conditional rewriting system. We present it §3.

During this formalization, we found missing arguments in the original proof. In two places, the
authors assume that a local commutation diagram was sufficient to prove a global commutation
diagram. We propose §4 and §5.2 a method to fill these gaps based on Newman’s lemma [22]
and some variant. This method requires proving inequalities over a measure on states. We generate these arithmetic inequalities, simplify them using conditional rewriting, and discharge them with the standard Rocq decision procedure.

In §5.3, we formalize a linear [31] (or at least affine) invariant, that rules out some undesirable states during the proofs. We reduce these well-formedness conditions to linear arithmetic inequalities similar to those for measure, which we discharge with the same process. Finally, §6 summarizes the current state of our formalization.

Throughout this paper, we have inserted clickable references to the HTML Rocq documenta-
tion. To use them, you only have to copy this PDF file at the root of the code directory, and
click on the Rocq icons 😄.

2 A flavor of LLBC: a borrow-centric model of Rust

The LLBC language, presented it §2.1, is a model of the MIR, an intermediate representation of
the Rust compiler, where complex expressions are broken down into small rvalues.

Aeneas symbolic execution, originally introduced to produce functional code, performs static borrow-checking. Ho et al. formalize it as an operational semantics called LLBC#†, presented §2.2, which abstracts the LLBC semantics. The borrow-checking soundness is deduced from the forward simulation of LLBC# by LLBC, sketched in §2.3.

Explaining LLBC in details — and why LLBC#† can be considered as a formal model of safe
Rust borrow-checking — is out of the scope of our very brief introduction. See [9] for details.
We only sketch here some representative features of Ho et al. framework, which will then enable
us to explain our contribution: how to formalize and mechanize their proof.

## 2.1 LLBC on a running example

The goal of the semantics of LLBC is to abstract away memory. It is centered around Rust concepts like ownership and borrowing, rather than a lower-level memory model with heap and addresses. As such, the borrow discipline is built-in the operational semantics.

To explain how it works, let us consider the Rust code fragment of Listing 1, where *a*, *b* are integer variables, *c* is a Boolean, and *x* is a mutable borrow over an integer. This program is correct for Rust borrow-checker. However, if line 9 was uncommented, it would be rejected because *x* possibly borrows variable *a* (depending on *c*) while *a* has been modified at line 8. Such a potential data-race is statically forbidden by Rust borrow-checking.

Let us now run this code with LLBC semantics from the initial state Ω₀. At line 2, the reference *x* mutably borrows the variable *a*. As long as this mutable reference is live, it has the unique rights to read and write in *a*. As such, the value in *a* is transferred and *x* is initialized with a mutable borrow value *borrow*<sup>*m*</sup>ℓ 3. The variable *a* is “loaned out” and left with a mutable loan value *loan*<sup>*m*</sup>ℓ. The loan identifier *ℓ* is used to link the borrow in *x* to its lender *a*.<fnref n="1" /> At line 6, the value in *x* is simply updated, leading to state Ω₂.

At line 8, a direct assignment of variable *a* from Ω₂ would fail (actually, result in a stuck
execution), because the variable *a* is borrowed. In LLBC terms, the mutable loan value forbids
any read or write. The LLBC execution can only be successful if *a* gets its resource back. This
is modeled by a reorganization step, that ends the borrow in *x* and returns the updated value to
*a*, leading to state Ω₃. Such a reorganization step is written Ω₂ ↪ → Ω₃. In LLBC semantics, any
(finite) number of such reorganization steps can be non-deterministically inserted before any
statement. Now, we can execute line 8, and obtain the state Ω₄. Finally, because the reference *x*

<footnote n="1">¹The *m* superscript stands for *mutable*. There are also *loan*<sup>*s*</sup>*ℓ*<sup>*v*</sup> (or *borrow*<sup>*s*</sup>*ℓ*) for a *shared* loan (or *borrow*).</footnote>
<caption>Listing 1: A concrete execution of a LLBC program.</caption>

```
0 // Ω₀ = a ↦ 3, b ↦ 4, c ↦ true, x ↦ ⊥
1 if c {
2   x = &mut a; // Ω₁ = a ↦ loan<sup>m</sup> <sub>l</sub>, b ↦ 4, c ↦ true, x ↦ borrow<sup>m</sup> <sub>l</sub> 3
3 } else {
4   x = &mut b;
5 }
// Ω₁
6 *x = 6; // Ω₂ = a ↦ loan<sup>m</sup> <sub>l</sub>, b ↦ 4, c ↦ true, x ↦ borrow<sup>m</sup> <sub>l</sub> 6
7 // Ω₃ = a ↦ 6, b ↦ 4, c ↦ true, x ↦ ⊥
8 a += 1; // Ω₄ = a ↦ 7, b ↦ 4, c ↦ true, x ↦ ⊥
9 // assert!(*x == 7);
```

has been ended, it is not usable at this point. If line 9 was uncommented, the LLBC semantics would go stuck at this point.

Rather than a heap, a LLBC state is a map of variables to values, that are tree-like terms.<fnref n="2" /> As for the operational semantics, it is defined as a big-step semantics judgment written “Ω ⊢ s ↪ (r, Ω’).” It means that on the state Ω, the statement s produces a safe execution, with a result r and output state Ω’: for example “()” for a successful execution.

## 2.2 LLBC#: a semantics for borrow-checking

The example in Listing 1 was only executed on a particular initial state. To ensure that it safely executes on any “well-typed” initial state, we execute it on LLBC#, featuring *symbolic values* and *region abstractions*, allowing for LLBC# states to over-approximate LLBC states. We now introduce a slightly simplified version of LLBC# on the running example.

First, for each type *T*, LLBC# introduces a symbolic—or abstract<fnref n="3" />—value $\sigma_T$: it represents the set of all possible concrete values of type *T*. Uninitialized borrows are set to $\perp$. Hence, initial state $\Omega_0^#$ assigns variables to the symbolic values of their type.

$$ \Omega_0^# = a \mapsto \sigma_{\text{int}}, b \mapsto \sigma_{\text{int}}, c \mapsto \sigma_{\text{bool}}, x \mapsto \perp $$

At line 1, because Boolean *c* is abstract, both branch of the conditional are executed leading to the respective states:

$$ \Omega_{\text{if}}^{\#} = a \mapsto \text{loan}^{m} \text{\textit{l}}, \quad b \mapsto \sigma_{\text{int}}, \quad c \mapsto \text{true}, x \mapsto \text{borrow}^{m} \text{\textit{l}} \sigma_{\text{int}} $$

$$ \Omega_{\text{else}}^{\#} = a \mapsto \sigma_{\text{int}}, \quad b \mapsto \text{loan}^{m} \text{\textit{l}}, \quad c \mapsto \text{false}, x \mapsto \text{borrow}^{m} \text{\textit{l}} \sigma_{\text{int}} $$

In order to continue, we have to exhibit a join state. In this state, the value of the Boolean variable *c* is once again $\sigma_{\text{bool}}$. The value of the reference *x* is the mutable loan $\text{borrow}^m \text{\textit{l}} \sigma_{\text{int}}$.

<footnote n="2">²There are also anonymous bindings _i_ ↦ v storing values overwritten at assignment, as they may contain borrows or loans that have not been ended. We eluded them on this example.</footnote>

<footnote n="3">³Symbolic execution [17, 26] represents the output state of an imperative program as a function of its input state. As such, Aeneas symbolic execution computes a pure function representing a Rust program. Because we omit this generation of functional code, we formalize a slightly simpler variant of LLBC# that does not distinguish between symbolic values of the same type. Thus, in our version, LLBC# is a kind of abstract semantics [5] of LLBC. The underlying abstract domain is relational, because it tracks relations between loans and borrows through loan identifiers. Its concretization relation corresponds to the simulation invariant that we could write $\ge$ in Figure 1a.</footnote>
However, we do not know if it borrows the variable a or b. We cannot place the corresponding loan $loan^m \ell$ in either of these variables.

To approximate this borrow graph, we introduce a region abstraction A between x on one side, and a and b on the other side. It is the region A, a multiset, that contains the loan $loan^m \ell$. The variables a and b are declared as borrowed, with respective loan identifiers $\ell_a$ and $\ell_b$, and corresponding borrows in the region A. The join state is:

$$ \Omega_{\text{join}}^{\#} = \begin{array}{l} a \mapsto \text{loan}^m \ell_a, b \mapsto \text{loan}^m \ell_b, c \mapsto \sigma_{\text{bool}}, x \mapsto \text{borrow}^m \ell \sigma_{\text{int}}, \\ A\{\text{borrow}^m \ell_a \sigma_{\text{int}}, \text{borrow}^m \ell_b \sigma_{\text{int}}, \text{loan}^m \ell\} \end{array} \qquad (1) $$

The region A acts as a barrier preventing any access to a and b when the borrow in x is live. Thus, on line 8, in order to give access back to the variable a, we must successively end the borrow in x, then end the abstraction A, and finally end the borrow of loan $\ell_a$.

## 2.3 Simulation by local transformations

Because the borrow checking of LLBC is defined as an operational semantics, its proof of soundness is a comparison of semantics. For that, Ho et al. define an abstraction relation $\Omega \le \Omega^\#$ between a LLBC state $\Omega$ and a LLBC$^\#$ state $\Omega^\#$. They prove that this relation is a forward simulation [18]. That means that for any states $\Omega_0 \le \Omega_0^\#$, for any successful LLBC$^\#$ executions $\Omega_0^\# \vdash^\# s \rightsquigarrow (r, \Omega_1^\#)$, there exists an execution in LLBC such that the final states are related. In particular, this means that a LLBC$^\#$ execution guarantees the existence of a safe LLBC execution,<fnref n="4" /> so that LLBC$^\#$ is a sound semantics for borrow-checking. This is pictured on the diagram in Figure 1a.

In an original way, the simulation invariant $\le$ is not defined as a global relation (e.g. like in [18]), but as a sequence of local transformations written $<$. Relation $<$ thus relates states that are intermediate between LLBC and LLBC$^\#$ states. Such intermediate states belong to an intermediate semantics called LLBC$^+$ [10], which our paper mostly eludes. For the sake of brevity, we consider that $\le$ is defined as $<^*$, the reflexive-transitive closure of $<$.<fnref n="5" />

For example, we abstract step by step the LLBC state $\Omega_1$ obtained at the end of the conditional line 6 of Listing 1, into the LLBC$^\#$ state $\Omega_{\text{join}}^\#$ (equation 1), by

* abstracting integer and Boolean values into symbolic values:
$$ \Omega'_1 = a \mapsto \text{loan}^m \ell, b \mapsto \sigma_{\text{int}}, c \mapsto \sigma_{\text{bool}}, x \mapsto \text{borrow}^m \ell \sigma_{\text{int}} $$

* declaring the variable b as borrowed in a region B, introducing a fresh loan $\ell_b$ in b:
$$ \Omega'_2 = a \mapsto \text{loan}^m \ell, b \mapsto \text{loan}^m \ell_b, c \mapsto \sigma_{\text{bool}}, x \mapsto \text{borrow}^m \ell \sigma_{\text{int}}, \\ B\{\text{borrow}^m \ell_b \sigma_{\text{int}}\} $$

* reborrowing the borrow between a and x in a region A, introducing a fresh loan $\ell_a$ in a:
$$ \Omega'_3 = a \mapsto \text{loan}^m \ell_a, b \mapsto \text{loan}^m \ell_b, c \mapsto \sigma_{\text{bool}}, x \mapsto \text{borrow}^m \ell \sigma_{\text{int}}, \\ A\{\text{borrow}^m \ell_a \sigma_{\text{int}}, \text{loan}^m \ell\}, B\{\text{borrow}^m \ell_b \sigma_{\text{int}}\} $$

* finally, just merging regions A and B to complete the following chain<fnref n="6" />
$$ \Omega_1 <^* \Omega'_1 <^* \Omega'_2 <^* \Omega'_3 < \Omega_{\text{join}}^\# $$

<footnote n="4">⁴This over-simplified presentation is generalized with fuel [10, §3.4] for enabling non-termination.</footnote>

<footnote n="5">⁵In our formalization, $\le$ is actually the composition of $<^*$ and syntactic equality modulo renaming of anonymous values and loan identifiers.</footnote>

<footnote n="6">⁶Most of the relations in this example are not single abstraction steps as indicated by $<^*$. For example, we need three steps to turn two integers and a Boolean into symbolic values between $\Omega'_1$ and $\Omega'_2$.</footnote>
<figure><img src="image_4.png" /><figcaption>(a) Forward simulation</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>(b) A simpler diagram</figcaption></figure>

<caption>Figure 1: Diagrams within simulation proofs</caption>

The proof of simulation represented in Figure 1a is conducted for every judgment, for example for rvalue evaluation, or for reorganizations. Because the simulation invariant is a reflexive-transitive closure, proofs are generally conducted by an induction, which reduces to the commutation diagram in Figure 1b for every rule of relation < and the judgment.

## 3 A reformulation of the semantics using a rewriting system

In the work of Ho et al., both the semantic judgments and the rules of the relation < are defined using states with holes. A state with one hole $\Omega[-]$ can be filled with any value to obtain a state $\Omega[v]$. A state can also contain two (disjoint) holes $(\Omega[-, -])$ or more. Here are some two selected rules defined with this notion.

$$ \begin{array}{c} \text{LEQ-TO SYMBOLIC} \\ v : T \\ \Omega[v] < \Omega[\sigma_T] \end{array} \quad \begin{array}{c} \text{REORG-END-MUTBORROW} \\ \text{hole of } \Omega[\text{loan}^m \ell, -] \text{ not inside a borrow} \\ \qquad \text{loan} \notin v \\ \Omega[\text{loan}^m \ell, \text{borrow}^m \ell v] \leftrightarrow \Omega[v, \perp] \end{array} $$

When Ho et al. prove that the relation <\* is a simulation for sequences reorganizations, they must study the combination of every rule of the relation < and every reorganization rule. In particular, they must prove the diagram in Figure 1b when the judgment is $\leftrightarrow$. For the two aforementioned rules, they study the case where there exists states with holes $\Omega_0[-]$ and $\Omega_1[-, -]$ such that $\Omega_h = \Omega_0[\sigma_T] = \Omega_1[\text{loan}^m \ell, \text{borrow}^m \ell v]$. It then becomes a problem of finding a unifier with two or three holes, depending on the position in $\Omega_1$ of the hole in $\Omega_0$.

Unifying two states with one hole is feasible. If we have $\Omega_l[v] = \Omega_r[w]$, then:

1. either $\Omega_l[-] = \Omega_r[-]$ and $v = w$;

2. or there exists a value with a hole $V[-]$ such that $\Omega_l[-] = \Omega_r[V[-]]$ and $V[v] = w$;

3. or there exists a value with a hole $V[-]$ such that $\Omega_l[V[-]] = \Omega_r[-]$ and $v = V[w]$;

4. or there exists a two-holed state $\Omega[-, -]$ such that $\Omega_l[-] = \Omega[-, w]$ and $\Omega_l[-] = \Omega[v, -]$.

However, unifying states with more holes proved to be unmanageable. It required giving names to holes, ensuring that each name hole was unique, managing the set of hole names, and even renaming holes.
The value $v = (\text{loan}^m \ell_0, \text{borrow}^m \ell_1 1986)$ is represented as the tree on the right-hand side. Each child of a given node is indexed with an integer (starting from 0 and increasing from left to right). Then, every subtree is uniquely described by the list of indices selecting its successive descendants, starting from the root and going down the tree. Such a list is called a value path (⊠). The value at path $1 \cdot 0$, written $v[1 \cdot 0]$, is 1986.

<figure><img src="image_6.png" /><figcaption>Figure 2: Example of a value path</figcaption></figure>

## 3.1 An algebra of terms

In order to make the proof feasible, we rephrased their semantic rules. Our first step was to notice that a hole describes a position in a state, and to move from this implicit notion to an explicit notion that we call “value paths” (or simply path when there is no ambiguity). We introduce this notion on the example in Figure 2. Such a notion of path is standard in the literature, for example it is called “occurrence” in [13].

**Notation.** We use the notation $x_0 \cdots x_{n-1}$ for a path (i.e. list) of n elements. The operation $p \cdot q$ is also used for concatenation of two paths p and q.

We call the operation $v[\pi]$, introduced in Figure 2, the “read at path $\pi$” on $v(\text{⊠})$. We may also (over)write a value at a path $\pi$, e.g. $v[1 \cdot 0 \leftarrow 1998] = (\text{loan}^m \ell_0, \text{borrow}^m \ell_1 1998) (\text{⊠})$. Given a value, all the lists of integers that correspond to a subvalue (or node) in the tree are called the valid paths (⊠). For $v$, the valid paths are $\varepsilon$, 0, 1 and $1 \cdot 0$. We formalize reading and writing at a path as total operations (using a default value). However, the validity condition is required to prove any property about these operations.

When working with values or states with holes, it was necessary to make a disjunction on whether a hole was contained in another one. The properties about whether a hole contains another one are naturally reformulated as comparisons between paths.

**Definition 1 (Comparison between paths).** Given two paths $\pi_0$ and $\pi_1$, the path $\pi_0$ is a prefix of $\pi_1$ when there exists $\pi'$ such that $\pi_1 = \pi_0 \cdot \pi'$. If $\pi' \neq \varepsilon$ then $\pi_0$ is a strict prefix of $\pi_1$. Two paths $\pi_0$ and $\pi_1$ are disjoint if neither one is a prefix of the other.

And the four-case disjunction when unifying two terms with hole corresponds to:

**Proposition 2 (⊠).** Given two paths $\pi_0$ and $\pi_1$, or $\pi_0$ is a strict prefix of $\pi_1$, or $\pi_1$ is a strict prefix of $\pi_0$, or $\pi_0$ and $\pi_1$ are disjoint.

Finally, there are equations governing consecutive applications of read and write operations on valid paths, depending on their comparison. For example:

$$v[\pi_0 \leftarrow w][\pi_0 \cdot \pi_1] = w[\pi_1] \qquad (2)$$

$$v[\pi_0 \cdot \pi_1 \leftarrow w][\pi_0] = v[\pi_0][\pi_1 \leftarrow w] \qquad (3)$$

$$v[\pi_0 \leftarrow w][\pi_1] = v[\pi_1] \qquad \text{if } \pi_0 \text{ and } \pi_1 \text{ are disjoint} \qquad (4)$$

In order to manipulate these values, we introduce the type of value nodes, and an operation `node(v)` to access the root of a value $v$. For example:

$$\text{node}(\text{borrow}^m \ell v) = \text{borrow}^m \ell -$$
Operations on nodes often come with simpler equations than with values:

$$ \mathbf{node}(v[\pi \leftarrow w]) = \mathbf{node}(v) \quad \text{if } \pi \neq \varepsilon \qquad (5) $$

$$ \mathbf{node}(v[\pi_0 \leftarrow w][\pi_1]) = \mathbf{node}(v[\pi_1]) \quad \text{if } \pi_0 \text{ is not a prefix of } \pi_1 \qquad (6) $$

All of these equations are proved in a generic manner, using a typeclass called **Value** (V**). This typeclass can be instantiated on any (supposedly inductive) type. In particular, the user has to provide the type of nodes, the function **node**, a function returning the list of children of any value, and to prove some axioms. This is necessary to avoid duplication, as several types of values are manipulated across the simulation proofs.

## 3.2 Operations on states

Finally, we generalize these constructions to states. To introduce that, let us use the abstract state $\Omega_{\text{join}}^{\#}$ defined in equation 1. We need to describe each value of the state. However, the abstraction regions we have used so far are multisets. Let us turn them to maps by associating each region elements to an arbitrary index $k$:

$$ \Omega_{\text{join}}^{\#} = \begin{cases} a \mapsto \text{loan}^m \ell_a, b \mapsto \text{loan}^m \ell_b, c \mapsto \sigma_{\text{bool}}, x \mapsto \text{borrow}^m \ell \sigma_{\text{int}}, \\ A\{1 \mapsto \text{borrow}^m \ell_a \sigma_{\text{int}}, 2 \mapsto \text{borrow}^m \ell_b \sigma_{\text{int}}, 3 \mapsto \text{loan}^m \ell\} \end{cases} $$

Each value contained in this region can be uniquely described by an accessor. For abstract states, accessors are either variables, anonymous bindings or pairs $(A, k)$ with $A$ a region and $k$ an index in the region.

$$ acc ::= x \mid \_i \mid (A, k) $$

For example, we have $\Omega_{\text{join}}^{\#}[b] = \text{loan}^m \ell_b$ and $\Omega_{\text{join}}^{\#}[(A, 1)] = \text{borrow}^m \ell_a \sigma_{\text{int}}$.

A “state path” is a pair written $acc \cdot \pi$ of an accessor $acc$ and a value path $\pi$, and the read operation on states generalizes with state paths. We have $\Omega_{\text{join}}^{\#}[x] = \text{borrow}^m \ell \sigma_{\text{int}}$ and $\Omega_{\text{join}}^{\#}[x \cdot 0] = \sigma_{\text{int}}$ for example.

We abusively write $\pi$ for state paths, like for value paths. And we extend path concatenation to state path expressions “$\pi_0 \cdot \pi_1$” where $\pi_0$ is a state path and $\pi_1$ a value path. Then, the notions of (strict) prefixness and disjointness (Definition 1) also apply to state paths. We also extend the write operations for states. The write operation for states $\Omega[\pi \leftarrow v]$ overwrites a value at a given state path.

Like for value, the operations around states are defined in a generic manner with a typeclass called **State** («). To be instantiated, the user must provide several operations —the main one being a translation of a state to a map from accessors to values— and verify axioms. Using this typeclass, we prove lemmas on states, including equations to simplify sequences of reads and writes on states (that are similar to those for values).

$$ \Omega[\pi \leftarrow w][\pi] = w \qquad (7) $$

$$ \Omega[\pi_0][\pi_1] = \Omega[\pi_0 \cdot \pi_1] \qquad (8) $$

$$ \Omega[\pi_0 \leftarrow w][\pi_0 \cdot \pi_1] = w[\pi_1] \qquad (9) $$

$$ \Omega[\pi_0 \cdot \pi_1 \leftarrow w][\pi_0] = \Omega[\pi_0][\pi_1 \leftarrow w] \qquad (10) $$

$$ \Omega[\pi_0 \leftarrow w][\pi_1] = \Omega[\pi_1] \qquad \text{if } \pi_0 \text{ and } \pi_1 \text{ are disjoint} \qquad (11) $$

$$ \Omega[\pi_0 \cdot \pi_1 \leftarrow v][\pi_0 \leftarrow w] = \Omega[\pi_0 \leftarrow w] \qquad (12) $$

$$ \Omega[\pi_0 \leftarrow v][\pi_0 \cdot \pi_1 \leftarrow w] = \Omega[\pi_0 \leftarrow v[\pi_1 \leftarrow w]] \qquad (13) $$

$$ \mathbf{node}(\Omega[\pi_0 \leftarrow w][\pi_1]) = \mathbf{node}(\Omega[\pi_1]) \quad \text{if } \pi_0 \text{ is not a prefix of } \pi_1 \qquad (14) $$
All these equations define a conditional term rewriting system, where variables are Ω, π, w, etc. Our Rocq proof includes them into a dedicated database of the autorewrite tactic for normalization ( autorewrite ). There is another equation, that allows us to commute two substitutions on disjoint paths π₀ and π₁. It is not included in the rewrite database as it is not oriented.

$$
\Omega[\pi_0 \leftarrow v][\pi_1 \leftarrow w] = \Omega[\pi_1 \leftarrow w][\pi_0 \leftarrow v] \quad \text{if } \pi_0 \text{ and } \pi_1 \text{ are disjoint} \quad (15)
$$

The rewrite system contains other equations about the manipulation of other state operations, like the addition of anonymous value or abstractions regions. For example:

$$
(\Omega, A)[(A, k) \cdot \pi'] = v[\pi'] \quad \text{if } A[k] = v \qquad (16)
$$

$$
(\Omega, A)[\pi] = \Omega[\pi] \quad \text{if } \neg\exists k \pi', \pi = (A, k) \cdot \pi' \quad (17)
$$

The conditions of the rewriting rules and the premises of the semantic judgments produce goals, that include comparisons between paths, validity of a path in a state, proving that a value does not contain some kind of nodes (⊥, loan or borrow), proving that a loan identifier is fresh, proving that a path is not contained in a borrow or a region, etc. To solve these conditions, we use a combination of automatic resolution with the tactic eauto and a base of hints, and specialized tactics.

3.3 Example of a simulation case 👋

Let us see how proofs are conducted within this framework. First, we reformulate below the semantic rules given in introduction of §3 using operations over state paths:

$$
\begin{array}{c}
\text{LEQ-TOSYMBOLIC} \quad \text{ Lemmas 3.1 and 3.2} \\
\Omega[\pi] : T \quad \text{borrow, loan } \notin \Omega[\pi] \\
\hline
\Omega < \Omega[\pi \leftarrow \sigma_T]
\end{array}
$$

$$
\begin{array}{c}
\text{REORG-END-MUT-BORROW} \\
\text{node}(\Omega[\pi_0]) = \text{loan}^m \ell \\
\pi_0, \pi_1 \text{ disjoint} \\
\hline
\Omega \hookrightarrow \Omega[\pi_0 \leftarrow \Omega[\pi_1 \cdot 0]] [\pi_1 \leftarrow \perp]
\end{array}
\quad
\begin{array}{c}
\text{node}(\Omega[\pi_1]) = \text{borrow}^m \ell - \\
\pi_1 \text{ not in a borrow or a loan}
\end{array}
$$

For the rule REORG-END-MUT-BORROW, instead of the hypothesis Ω[ π₁ ] = borrow m ℓ v , the condition is more conveniently reformulated as node (Ω[ π₁ ]) = borrow m ℓ − . In particular, variable v is no more needed, since we have Ω[ π₁ · 0] = Ω[ π₁ ][0] = (borrow m ℓ v ) [0] = v . We are now going to prove that these two rules commute for the diagram in Figure 3.

$$
\begin{array}{c}
\Omega < \\
\left| \\
\left. \leftarrow \right| \\
\exists \Omega'_t - \dots - \Omega'_h < \\
\left| \\
\left. \leftarrow \right| \\
\Omega_h
\end{array}
$$

The states Ωₕ and Ω'ₕ that are shorthands for:

$$
\begin{align*}
\Omega_h &= \Omega[\pi \leftarrow \sigma] \\
\Omega'_h &= \Omega_h[\pi_0 \leftarrow \Omega_h[\pi_1 \cdot 0]] [\pi_1 \leftarrow \perp] \\
&= \Omega[\pi \leftarrow \sigma] [\pi_0 \leftarrow \Omega_h[\pi_1 \cdot 0]] [\pi_1 \leftarrow \perp]
\end{align*}
$$

<caption>Figure 3: Commutation of LEQ-TOSYMBOLIC with REORG-END-MUT-BORROW</caption>

The proof involves three paths: the path π where the value v is abstracted, the path π₀ that contains the ended loan, and the path π₁ that contains the ended borrow. Here are the known relations between these paths:

• The paths π₀ and π₁ are disjoint, by hypothesis.

• The path π is not a prefix of π₀ and π₁, because Ωₕ[ π ] is a symbolic value, and it does not contain any mutable loan or borrow.
• More precisely, the paths $\pi$ and $\pi_0$ are disjoint. Indeed, the path $\Omega_h[\pi_0]$ is a mutable loan, it cannot a symbolic value. Thus, $\pi_0$ is not a prefix of $\pi$, so these paths are disjoint.

This is all we can deduce. Thus, for the precise relation between $\pi$ and $\pi_1$:

1. either $\pi_1$ is a prefix of $\pi$ (meaning that the value abstracted as $\sigma_T$ is in the ended borrow);

2. or $\pi_1$ and $\pi$ are disjoint.

**Case 1:** $\pi_1$ is a prefix of $\pi$. Because $\Omega_h[\pi] \neq \Omega_h[\pi_1]$ (a mutable borrow is not a symbolic value), we have $\pi \neq \pi_1$. The path $\pi$ is a strict prefix of $\pi_1$, and more precisely, the path $\pi_1 \cdot 0$ is a prefix of $\pi$, because $\pi$ is a valid path designating a mutable borrow at $\pi$, which has a unique child indexed by 0. Hence, there exists a path $q$ such that $\pi = \pi_0 \cdot 0 \cdot q$.

Now, let us prove that we can apply the reorganization rule REORG-END-MUT-BORROW on $\Omega$. We start with simplifications, using equation 14:

$$ 
\begin{aligned}
\text{node}(\Omega_h[\pi_0]) &= \text{node}(\Omega[\pi_1 \cdot 0 \cdot q \leftarrow \sigma_T][\pi_0]) = \text{node}(\Omega[\pi_0]) \\
\text{node}(\Omega_h[\pi_1]) &= \text{node}(\Omega[\pi_1 \cdot 0 \cdot q \leftarrow \sigma_T][\pi_1]) = \text{node}(\Omega[\pi_1])
\end{aligned}
$$

Thus, $\text{node}(\Omega[\pi_0]) = \text{loan}^m \ell$ and $\text{node}(\Omega[\pi_1]) = \text{borrow}^m \ell$, so we have $\Omega \hookrightarrow \Omega'_l$ with $\Omega'_l = \Omega[\pi_0 \leftarrow \Omega[\pi_1 \cdot 0]]$ $[\pi_1 \leftarrow \perp]$.

Let us then apply the rule LEQ-TOSYMBOLIC to $\Omega'_l$. Because the value abstracted as $\sigma_T$ was contained in the borrow in $\pi_1$, ending this borrow move its value to $\pi_0 \cdot q$ in $\Omega'_l$. Formally, we successively apply equations 11, 9 and 8.

$$ 
\begin{aligned}
\Omega'_l[\pi_0 \cdot q] &= \Omega[\pi_0 \leftarrow \Omega[\pi_1 \cdot 0]] [\pi_1 \leftarrow \perp] [\pi_0 \cdot q] \\
&= \Omega[\pi_0 \leftarrow \Omega[\pi_1 \cdot 0]] [\pi_0 \cdot q] \\
&= \Omega[\pi_1 \cdot 0][q] \\
&= \Omega[\pi_1 \cdot 0 \cdot q]
\end{aligned}
$$

Because $\Omega[\pi_1 \cdot 0 \cdot q] = \Omega[\pi]$ is of type $T$, by applying LEQ-TOSYMBOLIC, we have $\Omega'_l < \Omega''_h$ with $\Omega''_h = \Omega'_l[\pi_0 \cdot q \leftarrow \sigma_T]$. However, because we applied the rules in a different order, state $\Omega''_h$ is not syntactically equal to $\Omega'_h$. To conclude, we must show that these two states are equal. For that, we simplify these states according to the process in Figure 4. On the left-hand side, $\Omega'_h$ is simplified by successively applying equations 10, 15 and 12. On the right-hand side, $\Omega''_h$ is simplified by successively applying equations 15 and 13.

$$ 
\begin{array}{l@{\qquad}l}
\Omega'_h & \Omega''_h \\
\Omega[\pi_1 \cdot 0 \cdot q \leftarrow \sigma_T] [\pi_0 \leftarrow \Omega[\pi_1 \cdot 0 \cdot q \leftarrow \sigma_T][\pi_1 \cdot 0]] [\pi_1 \leftarrow \perp] & \Omega[\pi_0 \leftarrow \Omega[\pi_1 \cdot 0]] [\pi_1 \leftarrow \perp] [\pi_0 \cdot q \leftarrow \sigma_T] \\
\Omega[\pi_1 \cdot 0 \cdot q \leftarrow \sigma_T] [\pi_0 \leftarrow \Omega[\pi_1 \cdot 0][q \leftarrow \sigma_T]] [\pi_1 \leftarrow \perp] & \Omega[\pi_0 \leftarrow \Omega[\pi_1 \cdot 0]] [\pi_0 \cdot q \leftarrow \sigma_T] [\pi_1 \leftarrow \perp] \\
\Omega[\pi_0 \leftarrow \Omega[\pi_1 \cdot 0][q \leftarrow \sigma_T]] [\pi_1 \cdot 0 \cdot q \leftarrow \sigma_T] [\pi_1 \leftarrow \perp] & \Omega[\pi_0 \leftarrow \Omega[\pi_1 \cdot 0][q \leftarrow \sigma_T]] [\pi_1 \leftarrow \perp] \\
\Omega[\pi_0 \leftarrow \Omega[\pi_1 \cdot 0][q \leftarrow \sigma_T]] [\pi_1 \leftarrow \perp] & \Omega[\pi_0 \leftarrow \Omega[\pi_1 \cdot 0][q \leftarrow \sigma_T]] [\pi_1 \leftarrow \perp]
\end{array}
$$

<caption>Figure 4: Proving $\Omega'_h = \Omega''_h$ by simplifications with the rewriting rules</caption>

It would be very tedious to apply these computations manually. The autorewrite tactic fully automates it. When proving the equality between the states $\Omega'_h$ and $\Omega''_h$, we must also reorder substitutions using equation 15. We use a tactic called `states_eq`, that introduces these commutations at selected places on top of automatic rewriting.
As such, when proving this case, human intelligence was only required to decide to apply the rule REORG-END-MUT-BORROW at paths $π_0$ and $π_1$, and to apply the rule LEQ-TO-SYMBOLIC at path $π_0 \cdot q$. The remainder is automated.

**Case 2:** $π_1$ and $π$ are disjoint. Here, the paths $π$, $π_0$ and $π_1$ are mutually disjoint, so read and writes in these paths are mostly independent. We do not detail this case, as it is similar.

## 3.4 Evaluation of places

A nice consequence of the reformulation of the semantics is that it simplifies evaluation of places. As a reminder, a place (or lvalue) is composed by a variable $x$ and a list of projections, including dereferences and field access. It denotes a memory location.

Ho et al. define two different judgments, one to read from a place [9, Fig. 9.3 p. 161] and the other to write in a place [9, Fig. 9.4 p. 162]. Each read rule has a redundant write rule, and the write judgment is convoluted. But in our framework, it suffices to evaluate a place to a state path, that naturally describes an “address” in a state.

We present the single judgment $\Omega \vdash p \Rightarrow^k \pi$ meaning that place $p$ evaluates to $\pi$ in state $\Omega$. Parameter $k$ is a mode in {mov, mut, imm} and prevents illegal operations, such as moving a value out of a reference, or mutating a shared reference. See selected rules on Figure 5.

<figure><img src="image_7.png" /><figcaption>Figure 5: Evaluation of and places in LLBC, selected rules (EVAL-DEREF-MUTBORROW (EVAL-SHRLOAN)).</figcaption></figure>

Similarly to the original work, the evaluation of places is then incorporated into other judgments. See selected rules of our reformulation in Figure 6, involving the judgment $\Omega \vdash rv \downarrow$ ($v, \Omega'$) that denotes the evaluation of rvalue $rv$ into value $v$ with output state $\Omega'$.

# 4 The issue with commutation of reorganizations and concretization

During our formalization, we found a missing argument the proof of Ho et al. When proving that the relation $<^*$ is a simulation for chains of reorganizations $\leftrightarrow^*$, they only prove a local commutation property (Figure 7b) and wrongly$^7$ assume that it is sufficient to prove global commutation (Figure 7a). This flaw and the subsequent methodology to fix it were communicated and acknowledged by Ho et al.

<footnote>$^7$There are counter-examples of local confluence without global confluence [22, 12].</footnote>
<figure><img src="image_8.png" /><figcaption>Figure 6: Selected LLBC rules.</figcaption></figure>

As first attempt, we tried to prove global commutation from the standard Newman’s lemma [22], and more precisely, the generalization for commutation [6].

**Theorem 3** (Newman’s lemma for commutation). *Suppose that there exists a well-founded order (*E*, <) and a measure |Ω| such that:*

1. For all states $\Omega_h$ and $\Omega_l$ such that $\Omega_h > \Omega_l$, we have $|\Omega_h| > |\Omega_l|$.

2. For all states $\Omega$ and $\Omega'$ such that $\Omega \leftrightarrow \Omega'$, we have $|\Omega| > |\Omega'|$.

3. The relations > and ↔ commute locally (Figure 7b).

Then the relations > and ↔ commute globally (Figure 7a).

<figure><img src="image_9.png" /><figcaption>Figure 7: Commutations of concretization > steps and reorganization ↔ steps</figcaption></figure>

Traditionally, the condition states that the union of the relations (>) ∪ (↔) is terminating (i.e. no infinite chain). We preferred the equivalent condition that there exists a measure in a well-founded order *E* that decreases along > and ↔.

However, between LLBC# and LLBC, Newman’s lemma seems insufficient. Indeed, the relation <*> can be used to finitely abstract data structures of arbitrary size. This is necessary to provide an invariant state for execution of loops or recursive function calls. For example, in LLBC, it is possible to define a type *List* of linked lists of integers, using sum types, tuples and boxes. Let $\pi$ a place containing a list of $n$ elements $\Omega[\pi] = \text{Cons}(x_0, \text{Cons}(\dots, \text{Cons}(x_{n-1}, \text{Nil})))$ [9, §12.2.2]. Using the rule LEQ-TOSYMBOLIC, this concrete value can be abstracted through $\Omega < \Omega[\pi \leftarrow \sigma_{\text{List}}]$. We can even build an increasing chain for < of size $n$ between $\Omega$ and $\Omega[\pi \leftarrow \sigma_{\text{List}}]$. Thus, we cannot have $|\Omega| < |\Omega[\pi \leftarrow \sigma_{\text{List}}]|$ in general, otherwise the latter would be greater than any natural $n$.
<figure><img src="image_10.png" /><figcaption>(a) Global commutation of $>k$ and $\leftrightarrow$.</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>(b) Local commutation of $>k$ and $\leftrightarrow$.</figcaption></figure>

<caption>Figure 8: Diagrams for global and local commutation with the measured relation $>k$.</caption>

## 4.1 Generalized Newman's lemma with measured commutation

We fix this issue by extending the abstraction relation. Because rules like LEQ-TOSYMBOLIC can “hide” elements, we make their size visible, where the size $|\cdot|$ of a state or value is the number of nodes it contains. We extend the abstraction relation as $<_k$, with $k$ a parameter called the “size of hidden elements”. We simply ensure the relaxed condition $|\Omega_h| + k > |\Omega_l|$.

For example, here is the updated rule ($\mathbf{\Phi}$):

$$ \frac{\Omega[\pi] : T \quad \text{borrow, loan } \notin \Omega[\pi]}{\Omega <_{|\Omega[v]|} \Omega[\pi \leftarrow \sigma_T]} $$

We now adapt the definitions for the reflexive-transitive closure and for commutation to take the measure of hidden elements into account.<fnref n="8" />

**Definition 4** (Measured closure of a relation $\mathbf{\Phi}$). We say that $\Omega_l <_K^* \Omega_h$ if there exists a chain of relation $\Omega_l <_{k_0} \Omega_1 <_{k_1} \Omega_2 <_{k_2} \dots <_{k_{n-1}} \Omega_h$ such that $K \ge k_0 + \dots + k_{n-1}$.

**Definition 5** (Measured commutation). Relations $>k$ and $\leftrightarrow$ globally (resp. locally) commute if for every $\Omega_h$, $\Omega_l$, $k$ and $\Omega'_h$ such that $\Omega_h >_k^* \Omega_l$ and $\Omega_h \leftrightarrow^* \Omega'_h$ (resp. $\Omega_h >_k \Omega_l$ and $\Omega_h \leftrightarrow \Omega'_h$), there exists $\Omega'_h$ such that $\Omega_l \leftrightarrow^* \Omega'_l$ and $\Omega'_h >_k^* \Omega'_l$. See Figure 8a (resp. 8b).

It is interesting to note that in the measured closure $\Omega_l <_k^* \Omega_h$, the parameter $k$ is an upper-bound of the sum of the measure of hidden elements between $\Omega_l$ and $\Omega_h$. Hence, when we prove local commutation, we do not need to hide elements with the same measure $k$ between the states $\Omega'_l$ and $\Omega'_h$, a lower number is sufficient.

Relation $<_k$ is defined such that for every $\Omega_l$ and $\Omega_h$, $\Omega_l < \Omega_h \iff \exists k, \Omega_l <_k^* \Omega_h$. It directly follows that $\Omega_l <^* \Omega_h \iff \exists k, \Omega_l <_k^* \Omega_h$, and so it suffices to prove global commutation between $>k$ and $\leftrightarrow$ to have global commutation between $>$ and $\leftrightarrow$. Here is our variant of Newman's lemma on relations indexed by the size of hidden elements:

**Theorem 6** (Φ). Suppose that the following conditions hold:

1. For all states $\Omega_h$ and $\Omega_l$ such that $\Omega_h >_k \Omega_l$, we have $|\Omega_h| + k > |\Omega_l|$.

2. For all states $\Omega$ and $\Omega'$ such that $\Omega \leftrightarrow \Omega'$, we have $|\Omega| > |\Omega'|$.

3. The relations $>k$ and $\leftrightarrow$ locally commute (Figure 8b).

Then the relations $>k$ and $\leftrightarrow$ globally commute (Figure 8a).

<footnote n="8">⁸We sometimes use the symmetric relation $>k$ instead of $<_k$ in order to stay consistent with the definitions of commutation in Newman's lemma (Theorem 3).</footnote>
This theorem only takes into account the “hidden elements” of the concretization relation. This is sufficient in the current state of our formalization of LLBC, which only handles scalar values (integer, Booleans and borrows). Dealing with aggregates such as tuples might require some additional measure for reorganizations. We are however confident that our approach can be generalized to handle this extension.

## 4.2 Formalization and automation of measure decrease

In order to formalize our reasoning about sizes, we introduce a more general notion of weighted sum. Given a weight function $f$ mapping each node to a natural number, we sum the weight on each node of a value $v$ (respectively a state $\Omega$) to obtain the weighted sum $|v|_f$ (respectively $|\Omega|_f$). Size is simply the weighted sum with $f(n) = 1$ for any node $n$.

Proofs of inequality are first simplified with automatic rewriting, and discharged by the standard Rocq solver for integer linear inequalities. Here are some of the equations describing the weighted sum of common operations, that are included in our rewriting database:

$$|\text{borrow}^m \ell v|_f = f(\text{borrow}^m \ell -) + |v|_f$$

$$|\Omega[\pi \leftarrow v]|_f = |\Omega|_f - |\Omega[\pi]|_f + |v|_f$$

$$|\Omega, A|_f = |\Omega|_f + \sum_{(k \mapsto v) \in A} |v|_f$$

# 5 Borrow-checking soundness w.r.t. a low-level pointer semantics

Until here, our presentation focused on the most technical parts of Ho et al. proof, but eluded some of its crucial parts. §5.1 sketches how they extend their forward simulation of LLBC# by LLBC into a soundness proof of LLBC# w.r.t. a low-level pointer semantics. §5.2 and §5.3 present our contributions for mechanizing this part of their proof.

## 5.1 Overview of Ho et al. proof from the simulation of LLBC# by LLBC

In order to prove the soundness of their borrow checker against a more standard memory model, Ho et al. introduce a language called PL (pointer language) over a flat memory model à la CompCert [19]. As for LLBC#, PL is defined over the same syntax as LLBC, but with another operational semantics. There, the memory state is a collection of blocks that contain arrays of words. Pointers use addresses written $(b, i)$, with $b$ a block identifier and $i$ an offset. Moreover, the semantics is deterministic.

For example, for $\Omega_1^{pl}$ in Figure 9—the PL state for $\Omega_1$—the variables $a, b, c$ and $x$ are respectively allocated on blocks $b_a, b_b, b_c$ and $b_x$. The borrow $x$ on $a$ does not contain the value of $a$ but simply a reference to the borrowed address.

$$\Omega_1^{pl} = b_a \mapsto [3], b_b \mapsto [4], b_c \mapsto [\text{true}], b_x \mapsto [\text{ptr}(b_a, 0)]$$

$$\Omega_1^{hlpl} = a \mapsto \text{loc} \ell 3, b \mapsto 4, c \mapsto \text{true}, x \mapsto \text{ptr} \ell$$

<caption>Figure 9: Low-level states corresponding to $\Omega_1$ in Listing 1</caption>

It is not straightforward to prove a simulation between LLBC and PL. Because mutable borrows of LLBC carry values, one may have to follow an arbitrarily long chain of borrows to find the value of a given place. In order to bridge the gap between LLBC and PL, Ho et
al. introduce an intermediary language called HLPL (high-level pointer language). Like LLBC, states are maps to tree-like values. However, the notion of references and loans substituted by pointer and location values that are more akin to PL, see $\Omega_1^{hlpl}$ in Figure 9.

The proof of simulation is split in half. To prove a forward simulation from LLBC to HLPL, Ho et al. apply the same methodology as in §2.3, relating LLBC to HLPL states by gradually turning borrows and loans to pointers and locations. For example:

$$ \frac{\substack{\text{LE-MUTBORROW-To-PTR} \\ \text{node}(\Omega[\pi_0]) = \text{loan}^m \ell \\ \text{node}(\Omega[\pi_1]) = \text{borrow}^m \ell - \\ \Omega[\pi_0 \leftarrow \text{loc} \ell (\Omega[\pi_1 \cdot 0])] [\pi_1 \leftarrow \text{ptr} \ell] < \Omega}}{\text{node}(\Omega[\pi_1]) = \text{borrow}^m \ell - \text{node}(\Omega[\pi_0]) = \text{loan}^m \ell} $$

The forward simulation between HLPL and PL is proven in a more standard way, by defining a global map that associates to each variable a block, and to each HLPL location a PL address. Finally, composing all the forward simulation proofs together gives a forward simulation of LLBC# by PL. Because PL is deterministic, this ensures that if a program admits some valid LLBC# execution, then its PL execution cannot go stuck. Hence, LLBC# borrow-checking is sound w.r.t. PL execution. See [9] for details.

## 5.2 Proving global commutation from local commutation within HLPL⁺

Similarly to §4, Ho et al. deduce the forward simulation of LLBC by HLPL from local commutations between concretization (of LLBC to HLPL) and reorganization. This proof thus takes place in HLPL⁺ which is for LLBC/HLPL what LLBC⁺ is for LLBC#/LLBC: an intermediate semantics dealing with partially transformed states. Again, they deduce without justification global from local confluence. Here, we simply fixed the proof by a direct instance of Newman's lemma (Theorem 3). For the measure of HLPL⁺ states, we used a weighted sum (as in §4.2) with carefully selected weights ⚙️.

Interestingly, we also used this weighted sum to prove a useful well-formedness property over states, which we introduce in the next section.

## 5.3 Well-formedness of HLPL⁺ states from arithmetic inequalities

Contrary to the relation between LLBC# and LLBC, the relation between LLBC and HLPL actually transforms loans and borrows into other values. Because of that, there are some states where the commutation between reorganization and the relation > cannot be proven.

For example, given:

$$ \Omega_h = x \mapsto \text{loan}^m \ell, \quad y \mapsto \text{borrow}^m \ell 3, \quad z \mapsto \text{borrow}^m \ell 4 $$

$$ \Omega'_h = x \mapsto 3, \quad y \mapsto \perp, \quad z \mapsto \text{borrow}^m \ell 4 $$

$$ \Omega_l = x \mapsto \text{loc} \ell 4, \quad y \mapsto \text{borrow}^m \ell 3, \quad z \mapsto \text{ptr} \ell $$

Starting from $\Omega_h$, we have $\Omega_h \leftrightarrow \Omega'_h$ by ending the borrow in $y$, and by turning the borrow in $z$ into a pointer, we have $\Omega_l < \Omega_h$. Yet, it is impossible to complete this commutation diagram. Indeed, in $\Omega_l$, the borrow in $y$ cannot be ended because there is no mutable loan of identifier $\ell$ anymore. Similarly, in $\Omega'_h$, the borrow in $z$ cannot be turned into a pointer.

However, $\Omega_h$ cannot be obtained by any LLBC (or more generally HLPL⁺) execution starting from an empty initial state. A mutable borrow is always introduced with a fresh loan identifier $\ell$, and cannot be duplicated. To rule out such states, we introduce a well-formedness predicate, which excludes $\Omega_h$.

**Definition 7 ($\mathbf{\color{red}{\color{blue}{\color{red}{\color{blue}}}}$).** A HLPL⁺ state $\Omega$ is well-formed if for any loan identifier $\ell$:
* Ω contains at most one loan^m^l, at most one location of l, and at most one mutable borrow of l.

* If Ω contains a loan^m^l, then Ω neither contains locations nor pointers of l.

Remark that this well-formedness property expresses some linear [31] or more accurately affine conditions on the loan/borrow/location/pointer structure of HLPL^+ states. This suggests a link between HLPL^+ and separation logic [25].

An initial state with no borrow or loan is clearly well-formed; what remains to be proved is that this predicate is preserved during execution. As we have to check every judgment, this represents dozens of cases. The trick to automate this proof is that these properties can be reformulated as linear inequalities.

**Definition 8** (Number of occurrence of a node in a state ⚙️). The number of occurrences of the node c in state Ω is |Ω|<sub>f</sub>, where f is the indicator function such that f(c) = 1, and for any node d ≠ c, f(d) = 0. It is denoted by #[n ∈ Ω].

**Proposition 9** (). A state Ω is well-formed if and only if for any loan identifier l:

$$
\left\{
\begin{array}{l}
\#[\text{borrow}^m l - \Omega] \le 1 \\
\#[\text{loan}^m l \in \Omega] + \#[\text{loc} l - \Omega] \le 1 \\
\#[\text{loan}^m l \in \Omega] = 0 \lor \#[\text{ptr} l \in \Omega] = 0
\end{array}
\right.
$$

By reusing the codebase about weighted sums and inequalities, proving well-formedness was nearly effortless.

**Note.** The well-formedness predicate and the subsequent proof of invariance are not part of the original work by Ho et al. [10]. Their strategy here is to locally ensure well-formedness by adding a condition on the rule LE-MUTBORROW-TO-PTR. Like other conditions, the preservation of this local well-formedness property was verified for each commutation case involving this rule and a judgment. The purpose of the well-formedness predicate is to isolate and make this execution invariant explicit. The isolation of this property incidentally made the proof easier to automate.

# 6 State of the proof and Future Works

We formalized in the Rocq prover a small fragment of LLBC, that only contains integers, Booleans and mutable reference. On this fragment, we formally proved two key lemmas: concretization relations in LLBC^+ is a forward simulation (), and so is it in HLPL^+ ( ). Our next goal is to prove the simulation relations between LLBC^#, LLBC and HLPL with LLBC^+ and HLPL^+ to have complete simulation from LLBC^# to HLPL.

Because our fragment is restricted, we are working on extending it with if-then-else construc-
tions and loops. We are also working on proving the forward simulation between HLPL and PL,
and to formally prove a translation from PL to C#minor, an intermediate representation of
CompCert, as to have a formally verified Rust compiler. This compiler would be limited to safe
Rust, like Aeneas at the moment, making it only a proof of concept.

After that, several additions are possible. One would be to include functions calls and
recursivity. The other would be to extend our fragments with tuples, enumerations and boxes.
This would enable borrow-checking over complex data-structures, like linked lists.
# 7 Conclusion and Related Works

**Type soundness proofs** While single-hole contexts are standard in syntactic approaches of type soundness [32] and their formalization in proof assistants [7, §4.1], multi-holes contexts seem an original concept of [10]. While this concept is intuitive on paper, it is cumbersome in formalized proofs, at least when context unification is required. Our formalization shows that the standard notion of path (or occurrence) in a term [13] provides a convenient reformulation.

Another original technique of [10] is to model Rust borrow-checking as a kind of abstract operational semantics, and to prove its soundness from operational semantics simulations. Our formalization repaired a flaw in their methodology.

**Semantics of Rust and borrow-checking** The current borrow-checker is NLL (non-lexical lifetimes) [20]. Each reference is parameterized with a lifetime. The algorithm computes the value of each lifetime, that is the set of control points it covers. This information is used to compute at which control points places are borrowed, represented by objects called loans. The proposed successor for NLL is Polonius [23]. It is a more precise algorithm that introduces a concept shift from lifetimes to regions, that are set of loans. The symbolic execution of Aeneas shares similarities with Polonius, with a focus on regions. Some programs that are rejected by NLL are accepted by Polonius and Aeneas [10, §6]. However, studying the formal links between LLBC# and the current borrow-checkers is out of our scope.

Another dynamic semantics for borrows is Tree Borrows [30], a refinement of Stacked Borrows [14]. They both provide an aliasing model for Rust, that could justify optimizations even in the presence of unsafe code. Both are dynamic models that complement the heap with ghost information. Each pointer is decorated with a tag, and each memory cell stores the permissions and tags of the pointers that can access in a tree or a stack. Both are implemented in the Miri interpreter [21]. Finally, the soundness of several optimizations w.r.t. Tree Borrows is formally proven within the Simuliris framework [8].

The LLBC# model shares similarities, but the aim is different. The borrow-centric semantics of LLBC only allows the representation of safe executions. This is used to formalize a borrow-checking. In contrast, Tree Borrows complements a more complete and lower-level model of unsafe Rust with a ghost state, and the focus is on optimization. There is not yet a proof that borrow-checked programs are safe w.r.t. Tree Borrows (it is still empirically verified). Their proofs of optimizations assume that source programs do not have undefined behaviors (w.r.t. Tree Borrows).

For models of Rust and its type system, the seminal work is RustBelt [15], a formal model in the Iris separation logic [16]. It enables proving that functions in the standard library that manipulate unsafe code can be safely called and composed. Among other things, the authors present a model of safe Rust called $\lambda_{Rust}$. They prove that well-typed $\lambda_{Rust}$ programs are safe by interpreting types as separation logic predicates [28].

In the formalization of LLBC, the required techniques (forward simulations, block-based pointer model) are close to those used in the correctness proof of CompCert, whereas the $\lambda_{Rust}$ model seems to us less close to an existing formally verified compiler. However, RustBelt provides a relatively complete model of safe Rust, whereas LLBC# and Aeneas are currently limited to fragments of safe Rust.

**Term rewriting within interactive proofs** Our formalization applies rewriting techniques to automate proofs of semantic preservation. We mainly used the autorewrite tactic of Rocq. This tactic is convenient because it enables us to build our rewriting system incrementally. But it has also limitations. For example, it does not cope with non-oriented equations such
as commutativity. Tools such as CoLoR [1] and CiME3 [4] help mechanize the treatment of user-defined rewriting systems — but it is unclear if they support conditional rewriting rules like ours. An alternative would be to design a reflexive tactic, such as `ring` [2] or KAT [24, §3]. However, it seems complex to design a reflexive tactic on a user-defined term algebra under construction. The Rewriting Type Theory of [3], which embeds user-defined rules in the reduction engine of the host logic, would be an appealing framework, even if some of our rules might be rejected by the static verifier.

We proved a commutation theorem that generalizes confluence theorems of rewriting theory, from a variant of Newman's lemma. They are other complex confluence theorems in Rocq, particularly in Meta-Rocq [27, 3]. These proofs are based on the Tait-Martin Löf method, based on a notion of parallel reduction. It is not clear whether this method can be adapted to our commutation over two distinct rewriting systems. Previously, van Oostrom [29] stated a theorem that generalizes several commutation results, including Newman's lemma. It is based on a general property called "decreasing diagrams", with a multiset order. We are studying whether theorem 6 could be an instance of van Oostrom's theorem, or another theorem in the literature.

# 8 Acknowledgement

We thank Son Ho and Aymeric Fromherz for their precious comments and advice throughout this work.

This work is partially supported by the French National Research Agency in the framework of the "Investissements d'avenir" program (ANR-15- IDEX-02) and the SECUREVAL project funded by the "France 2030" government investment plan managed by the French National Research Agency, under the reference ANR-22-PECY-0005.

# References

[1] Frédécic Blanqui and Adam Koprowski. CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. *Mathematical Structures in Computer Science*, 21(4):827-859, 2011. doi:10.1017/S0960129511000120.

[2] Samuel Boutin. Using reflection to build efficient and certified decision procedures. In Martín Abadi and Takayasu Ito, editors, *Theoretical Aspects of Computer Software, Third International Symposium, TACS '97, Sendai, Japan, September 23-26, 1997, Proceedings*, volume 1281 of *Lecture Notes in Computer Science*, pages 515-529. Springer, 1997. URL: https://doi.org/10.1007/BFb0014565, doi:10.1007/BFB0014565.

[3] Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter. The taming of the rew: a type theory with computational assumptions. *Proc. ACM Program. Lang.*, 5(POPL), January 2021. doi:10.1145/3434341.

[4] Evelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. Automated Certified Proofs with CiME3. In Manfred Schmidt-Schauß, editor, *Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, Novi Sad, Serbia, May 30 - June 1, 2011*, volume 10 of *LIPICS*, pages 21-30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. doi:10.4230/LIPICS.RTA.2011.21.

[5] Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In *Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming*
*Languages*, POPL '79, page 269–282, New York, NY, USA, 1979. Association for Computing Machinery. doi:10.1145/567752.567778.

[6] Henk Doornbos, Roland Backhouse, and Jaap Van Der Woude. A calculational approach to mathematical induction. *Theoretical Computer Science*, 179(1-2):103–135, June 1997. doi:10.1016/S0304-3975(96)00154-5.

[7] Catherine Dubois. Proving ML Type Soundness Within Coq. In *Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics*, TPHOLs '00, page 126–144, Berlin, Heidelberg, 2000. Springer-Verlag.

[8] Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. Simuliris: A separation logic framework for verifying concurrent program optimizations. *Proceedings of the ACM on Programming Languages*, 6(POPL):1–31, January 2022. doi:10.1145/3498689.

[9] Son Ho. *Formal Verification of Rust Programs by Functional Translation*. PhD thesis, Université PSL (Paris Sciences & Lettres), December 2024. https://theses.hal.science/tel-05004605.

[10] Son Ho, Aymeric Fromherz, and Jonathan Protzenko. Sound Borrow-Checking for Rust via Symbolic Semantics. *Proceedings of the ACM on Programming Languages*, 8(ICFP):251:426–251:454, August 2024. doi:10.1145/3674640.

[11] Son Ho and Jonathan Protzenko. Aeneas: Rust Verification by Functional Translation. *Proceedings of the ACM on Programming Languages*, 6(ICFP):711–741, August 2022. arXiv:2206.07185, doi:10.1145/3547647.

[12] Gérard Huet. Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems. *Journal of the ACM*, 27(4):797–821, October 1980. doi:10.1145/322217.322230.

[13] Gérard Huet and Derek C. Oppen. Equations and Rewrite Rules: A Survey. In *Formal Language Theory*, pages 349–405. Academic Press, 1980. doi:10.1016/B978-0-12-115350-2.50017-8.

[14] Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer. Stacked borrows: An aliasing model for Rust. *Proceedings of the ACM on Programming Languages*, 4(POPL):1–32, January 2020. doi:10.1145/3371109.

[15] Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt: Securing the foundations of the Rust programming language. *Proceedings of the ACM on Programming Languages*, 2(POPL):66:1–66:34, December 2017. doi:10.1145/3158154.

[16] Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. *Journal of Functional Programming*, 28:e20, 2018. doi:10.1017/S0956796818000151.

[17] James C. King. Symbolic execution and program testing. *Commun. ACM*, 19(7):385–394, 1976. doi:10.1145/360248.360252.

[18] Xavier Leroy. A Formally Verified Compiler Back-end. *Journal of Automated Reasoning*, 43(4):363, November 2009. doi:10.1007/s10817-009-9155-4.
[19] Xavier Leroy and Sandrine Blazy. Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. *Journal of Automated Reasoning*, 41(1):1-31, July 2008. doi:10.1007/s10817-008-9099-0.

[20] Nicholas Matsakis. The Rust RFC Book: NLL. https://rust-lang.github.io/rfcs/2094-nll.html, August 2017.

[21] Miri team. Miri: An interpreter for Rust's mid-level intermediate representation. https://github.com/rust-lang/miri, 2015.

[22] M. H. A. Newman. On Theories with a Combinatorial Definition of "Equivalence". *Annals of Mathematics*, 43(2):223-243, 1942. arXiv:1968867, doi:10.2307/1968867.

[23] The Polonius Working Group. The Polonius Book. https://rust-lang.github.io/polonius/, 2021.

[24] Damien Pous. *Automata for relation algebra and formal proofs*. Accreditation to supervise research, ENS Lyon, September 2016. URL: https://hal.science/tel-01445821.

[25] John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In *Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science*, LICS '02, page 55-74, USA, 2002. IEEE Computer Society.

[26] Hanan Samet. Compiler testing via symbolic interpretation. In John A. Gosden and Olin G. Johnson, editors, *Proceedings of the 1976 Annual Conference, Houston, Texas, USA, October 20-22, 1976*, pages 492-497. ACM, 1976. doi:10.1145/800191.805648.

[27] Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Nielsen, Nicolas Tabareau, and Théo Winterhalter. Correct and complete type checking and certified erasure for Coq, in Coq. *J. ACM*, 72(1), January 2025. doi:10.1145/3706056.

[28] Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. A logical approach to type soundness. *Journal of the ACM*, 71(6):1-75, 2024. doi:10.1145/3676954.

[29] Vincent van Oostrom. Confluence by Decreasing Diagrams - Converted. In Andrei Voronkov, editor, *Rewriting Techniques and Applications*, pages 306-320, Berlin, Heidelberg, 2008. Springer. doi:10.1007/978-3-540-70590-1_21.

[30] Neven Villani, Johannes Hostert, Derek Dreyer, and Ralf Jung. Tree Borrows. *Proceedings of the ACM on Programming Languages*, 9(PLDI):188:1019-188:1042, June 2025. doi:10.1145/3735592.

[31] Philip Wadler. Linear types can change the world! In *Programming concepts and methods*, volume 3, page 5. Citeseer, 1990. Issue: 4.

[32] A.K. Wright and M. Felleisen. A Syntactic Approach to Type Soundness. *Information and Computation*, 115(1):38-94, 1994. URL: https://www.sciencedirect.com/science/article/pii/S0890540184710935, doi:10.1006/inco.1994.1093.