# An Intermediate Representation to Propagate Semantic Information During Compilation

Benjamin Bonneau

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

## To cite this version:

Benjamin Bonneau. An Intermediate Representation to Propagate Semantic Information During Compilation. 2025. hal-05483672

HAL Id: hal-05483672

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

Preprint submitted on 29 Jan 2026

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# An Intermediate Representation to Propagate Semantic Information During Compilation

Benjamin Bonneau

## Abstract

The soundness of some transformations performed by compilers relies on semantic properties of the programs. In particular, aliasing information is needed to reason on memory accesses. Some properties can be established using analysis on low-level representations of programs, but an alternative is to propagate information available at higher levels. This latter approach involves a representation of information which is both exploited and maintained by the successive compilation passes. Justifying the correctness of the transformations then requires not only a precise semantics of the intermediate representations, but also a formalisation of the representation of information. We propose an intermediate representation that retains high-level information through expressive but statically checked dependent types. We encode non-aliasing information using memory fragments, whose implementation with a global memory is justified by a linearity criterion. We formalize in Rocq the intermediate representation, its semantics and some compilation passes. We also formalize for this purpose a generic functional SSA representation, which enables the definition of effectful languages.

## 1 Introduction

Compilation pipelines involve Intermediate Representations (IRs), which are languages distinct from the source and target languages. Compilers perform transformations, including translations and optimisations, between and within the representations. Hence, IRs are not only designed to express the semantics of the programs, but also to facilitate those transformations. Some transformations, in particular optimisations, are correct only under semantic conditions. For instance in Figure 1, the speculation of a division above a branch requires that the divisor is not zero when the condition is false. A particularly important kind of information is non-aliasing between memory accesses. Indeed, because of the indirection provided by pointers, syntactically distinct addresses may alias, that is refer to overlapping memory location. Non-aliasing information is thus necessary to commute writes with other accesses (Figure 1) or to propagate the values stored in the memory [12].

**Propagation of Information.** A way of obtaining information is to perform analyses on the program. However, those analyses are not always precise enough and may miss

CPP, Rennes, France
2026.

<figure><img src="image_3.png" /><figcaption>**Figure 1.** Semantic Pre-Conditions of Transformations</figcaption></figure>

assumptions such as function pre- and post-conditions. Because of the cost of some analyses, it is also desirable to perform them only once during the compilation pipeline. Moreover, information needed to perform transformations on a low level representation may be easily available at a higher level, yet difficult to reconstruct from the low level representation [27]. In some cases, precise information can be obtained for free, without performing additional analyses:

* In a compilation pipeline, translation passes implement high level abstractions using lower level operations. The structure of those translations may provide precise information.

* Programmers rely on invariants to justify the correctness of their programs. Those invariants are sometimes formally represented, and even checked, using static systems (such as the borrow checker of Rust), source level analyses or user-directed proofs.

It is thus useful to propagate semantic information during compilation.

**Formalizing Semantic Information.** In a verified compilation pipeline, the meaning of semantic information need to be formally defined in order to use it to justify program transformations. For instance, several optimisations of CompCert [21] rely on data flow analyses [4, 30]. The result of those analyses is a map which describes information known at each program point and a correctness theorem ensures that the inferred properties are true during any execution of the program. However the results of analyses are only used for a single pass and discarded immediately after since they may become invalid on the transformed program. Propagating information would thus require explicit manipulation by the passes and formal justifications. Instead we explore ways of encoding semantic information directly in the intermediate representation of the program. This approach requires

56

57

58

59

60

61

62

63

64

65

66

67

68

69

70

71

72

73

74

75

76

77

78

79

80

81

82

83

84

85

86

87

88

89

90

91

92

93

94

95

96

97

98

99

100

101

102

103

104

105

106

107

108

109

110
<figure><img src="image_4.png" /><figcaption>**Figure 2.** A Transformation Invalid if Overflow Is UB</figcaption></figure>

instrumenting the syntax and semantics but avoids updating external data-structures during transformations.

**Undefined Behaviors.** A possible way of encoding the fact that a property hold at a program point is to raise an *Undefined Behavior* (UB) [19] when a program reaches the point without satisfying the property. UBs semantically define guarantees given by the producer of a program, compilers can then recover information from the assumption that programs never raise UB. For instance the C standard consider overflows of signed integers as UB, enabling compilers to obtain bounds on the values and to perform transformations [19]. However, since UBs are defined semantically, they implicitly depend on the whole execution that lead to them, in particular on the control flow. For instance in Figure 2, if one choose to consider integer overflow as UB, then the absence of UB in program (a) ensures that the addition does not overflow, but only if the condition c is true. If we transform (a) by moving the addition above the conditional, we obtain a program (b) where the absence of UB implies the absence of overflow independently of the value of c. Hence the transformation is invalid, unless more information is available on the program. The reverse transformation is valid, but cannot be reverted. This example illustrate not only that UBs introduce dependencies that are not reflected by the syntax, but also that they can prevent transformations. For this reason, intermediate representation designed for optimisations avoid assigning UB to instructions that are implemented with total operations in the target language. For instance, the addition of two integers is always defined in the RTL representation of CompCert, but information that was ensured by the absence of overflow in the C source is lost at this level. A compromise between retaining information and speculation is the use of deferred undefined behaviors with a poison value [19]. However this approach requires the extension of the set of values and may break some reasoning properties. For instance a division by $2 * n + 1$ becomes a partial operation since it is not defined if n is a poison value.

**Contributions.** We designed Frag IR, an intermediate representation which encodes semantic information along with the semantics of the program. The IR, its semantics and typing are formally defined in Rocq.

<table><caption>**Figure 3.** Types, values and memories of Frag IR and Flat IR. In heaplet and memory, a permission to deallocate a range $[p; p + sz)$ is represented by setting the component of type option nat at address p to sz.</caption><tbody><tr><td>scalar><sub>ty</sub></td><td>:=</td><td>unit | bool | int | ptr</td><td>166</td></tr><tr><td>perm</td><td>:=</td><td>Empty | Writable</td><td>167</td></tr><tr><td>type, ty_expr</td><td>:=</td><td>variable | scalar><sub>ty</sub><br/>- propositions<br/>| ty_expr = ty_expr ...<br/>| prop&lt;?id&gt; (list ty_expr)<br/>- memory fragments<br/>| cell&lt;scalar><sub>ty</sub&gt; ty_expr<br/>| malloc ty_expr ty_expr<br/>| mrange ty_expr ty_expr ...<br/>| mem&lt;?id&gt; (list ty_expr)</td><td>168<br/>169<br/>170<br/>171<br/>172<br/>173<br/>174<br/>175<br/>176</td></tr><tr><td>value</td><td>:=</td><td>Vunit | Vbool bool | Vint int | Vptr ptr<br/>| Vmem heaplet<br/>| Vcell ptr scalar><sub>ty</sub> (list byte)</td><td>177<br/>178<br/>179</td></tr><tr><td>heaplet</td><td>:=</td><td>⊥ | ptr → (option byte × option nat)</td><td>180</td></tr><tr><td>mem</td><td>:=</td><td>ptr → (byte × perm × option nat)</td><td>181</td></tr></tbody></table>

* We show that information can be represented without implicit dependencies on the control flow using a type-based system (§2).

* We define a memory model based on memory fragment which encodes non-aliasing properties and validity of accesses (§3).

* We formalized in Rocq a generic functional SSA representation (§4). We define formally verified passes on this representation and obtain Frag IR as an instance.

* We also instantiated our generic representation with a lower level memory model and implemented a verified compilation pipeline from Frag IR to this representation, called Flat IR (§5).

## 2 Dependent Types

This section and the next one present the encoding of semantic information in Frag IR. The types and values of the IR are reproduced Figure 3 and described in the next sections. The syntax and semantics of programs are defined formally in §4, but in the first sections, the examples can be read as if they were written in a typed functional language where operators and function calls are applied to types and variables and may return several values.

### 2.1 Proposition Types

Examples such as Figure 2 motivate us to search for a representation of information which specify the hypotheses under which it is valid. In particular, we avoid a purely semantic approach based on UBs in order to avoid implicit dependencies on the control flow. Instead, we rely on a static approach which uses ad hoc dependent types. The types of
add(n: int, m: int)
: (r: int, post: r = n + m)
div(n: int, d: int, pre: d ≠ 0)
: (r: int, post: r = n / d)

<caption>Figure 4. Signatures of Two Operators of Frag IR</caption>

fn foo(n: int, pre: n > 0)
: (m: int, post: m > 0) {...}
fn bar(n: int, H0: n > 1) : (m: int) {
(* fcall foo(n, H0) is ill-typed *)
let H1: n > 0 = lemma {
(n': int, H0': n' > 1) : (H1': n' > 0)
}(n, H0);
let m, _ = fcall foo(n, H1);
return (m)
}

<caption>Figure 5. Implication Between Pre-Conditions with lemma</caption>

variables can thus contain variables, and the semantics of a type T depends on values ρ for its free variables. We note ρ ⊢ v ∈ T the typing judgement for a value v and ρ ⊢ v ∈ T the typing judgment between corresponding elements of a list of values v and a list of types T. In order to represent information, our set of types for the variables includes so-called proposition types which are inhabited if and only if the proposition they represent is satisfied. If it exists the unique inhabitant is Vunit. We are thus not interested in the values of variables of proposition types and do not have to reason on those values during proofs of transformations, but having such variables in the context provides information about the values of the other variables they depend on. They can thus be used instead of UBs. For instance our division operator (Figure 4) takes an additional argument pre with a proposition type which ensures that the divisor m is not zero. Thanks to this argument, the division becomes a total operator, but is still never performed with a zero divisor. In order to reflect in the type system information about the results of computations, operations return an additional result post with a proposition type. For the same reason, a branch on a guard b introduces a variable (Hb in Figure 6) with type b = true in the then branch and b = false in the else branch.

Despite this particular usage of proposition types, the variables with those types are treated exactly like standard variables in the syntax, typing and semantics. In particular they can appear as arguments or results of functions (e.g. foo in Figure 5). They then act as pre- and post-conditions and propagate inter-procedural information.

## 2.2 Lemma Operations on Propositions

fn foo(b: bool, n: int, H0: prop<?P> b n) : () {
  if b Hb then {
    let H1: n < 9 = lemma{...}(b, n, H0);
    let H2: n > 0 = lemma{...}(b, n, H0, Hb);
    ... }
  }
}

<caption>Figure 6. Combination of lemma instructions and abstract prop types (introduced in §2.2). The dependencies of the lemmas reflect that $n < 9$ is true regardless of the value of b whereas $n > 0$ may depend on hypothesis $Hb : b = true$.</caption>

Typing judgements for programs in Frag IR do not take into account the semantics of propositions, like all types propositions are compared using syntactical equality. For instance, in Figure 5 the proposition $H0 : n > 1$ cannot be given as argument to the function foo which expect a precondition $n > 0$. Instead we provide an operation lemma, which derives new propositions from existing ones. A lemma is described by a closed signature, which defines the type of its formal arguments ($n'$ and $H0'$ in Figure 5) and of its formal results ($H1'$). It is applied to variables defined in the context ($n$ and $H0$) and whose types match the types of the formal arguments. Its actual results ($H1$) add derived information to the context. For a lemma to be sound, the propositions corresponding to its results must be satisfied whenever the propositions taken as arguments are. This property is expressed using the typing judgement:

**Definition 2.1 (Soundness of lemmas, first version).** A lemma with arguments types arg and result types res is sound if:

$$ \forall \text{varg. } (\text{varg} \vdash \text{varg} \in \text{arg}) \Rightarrow \\ \exists \text{vres. } (\text{varg}, \text{vres} \vdash \text{vres} \in \text{res}) $$

Since lemmas have closed signatures, their soundness are independent of the context where they are used and of the semantics of the program. The soundness of all lemmas is a well-formedness property of programs and we maintain it as a formal invariant of the compilation pipeline. That is, the producer of a program must ensure that all lemmas are sound and transformations assume and preserve this property.

Isolating with lemmas the derivation of information has several benefits:

* Since lemmas can only use the propositions taken as arguments, the dependencies of information are explicit. In particular, lemmas do not depend implicitly on the control flow. For instance in Figure 6, a compiler could move the first lemma above the branch to obtain the information $n < 9$ earlier.

* The undecidable implications between propositions are captured with the soundness condition on lemmas. The typing judgments rely only on syntactical equality. This allowed us to implement a type-checker.

276

277

278

279

280

281

282

283

284

285

286

287

288

289

290

291

292

293

294

295

296

297

298

299

300

301

302

303

304

305

306

307

308

309

310

311

312

313

314

315

316

317

318

319

320

321

322

323

324

325

326

327

329

221

222

223

224

225

226

227

228

229

230

231

232

233

234

235

236

237

238

239

240

241

242

243

244

245

246

247

248

249

250

251

252

253

254

255

256

257

258

259

260

261

262

263

264

265

266

267

268

269

270

271

272

273
```
let H: d ≠ 0 = assert<d ≠ 0>();
let r: int, _ = div(n, d, H)
if c _ then fcall f(r)
  ↓
let H: d ≠ 0 = assert<d ≠ 0>();
if c _ then {
  let r: int, _ = div(n, d, H);
  fcall f(r) }
```

<caption>**Figure 7.** Reversible Move of a Division Below a Branch</caption>

Producers of programs can call it instead of proving that the programs they generate are well-typed.

Since type checking does not depend on the semantics of propositions, we increase their expressivity by allowing abstract propositions, whose semantics is not expressed with the syntax of our types and unknown to the compiler. Those abstract proposition are syntactically represented as prop<?P> args where P is by a predicate identifier and args are type expressions. Formally, the semantics of those predicates are chosen by the producer of the program, as functions of the evaluations of their arguments (which are either values or types). The soundness of the lemmas must be justified with respect to the chosen semantics of the predicates.

## 2.3 Assert Operation

In some cases, one may want to justify information semantically instead of deriving it statically using lemmas. Either because it is too complex to express the necessary invariants or because one only has access to a semantic justification, for instance when compiling a language with UBs. For this purpose, Frag IR includes an operation `assert`. Given a proposition P, `assert<P>()` returns the value `Vunit` inhabiting P if P is satisfied and raises an UB otherwise. Like in some verification tools [20], `assert` is not a dynamic check and instead requires the producer of the program to prove that P always hold at the program point. In particular, the compiler can remove assertions if their result is not used, although this erases information.

Figure 7 illustrates the encoding of a partial division operation using `assert`. The point where the information is obtained with `assert` is separated from its use by `div`. As a consequence, the division operation can be commuted with branches in a reversible way.

# 3 Memory Fragments

We now focus on information useful to transform memory accesses. Two kinds of information are relevant:

* Because programs are only allowed to access parts of the memory that they allocated, most memory operations are partial. Speculating them thus require information about the validity of accesses.

* Because of the indirection provided by pointers, non-aliasing information is needed to reason on memory operations and to transform them.

Information about memory accesses are particularly valuable because they often rely on inter-procedural invariants and can only partially be found by alias analyses.

Aliasing information is challenging to encode because it relates many dynamic addresses. Steensgaard [31] showed that it could be encoded by fragmenting the memory using functional stores. Following this approach, programs in Frag IR operate over multiple fragments which are explicitly represented with variables instead of a single global memory. We describe the main ideas of this encoding on an example (§3.1) before formalizing the semantics of the fragments and of operations on them.

## 3.1 Usage of Memory Fragments

Figure 8 describes a function which increments the values stored at two non-aliasing memory locations. The function takes as arguments not only pointers to the locations but also cells representing the fragments of the memory where the integers are stored. Memory fragments, such as cells, store values for a subset of the memory. Instead of accessing a global state, all memory operations take as argument or return memory fragments. Memory fragments are immutable, hence the write operation `Frag.write` creates a new cell storing the value given as argument and the function `incr2` returns the cells containing the updated values.

**Linearity.** Memory fragments are ultimately implemented with a global memory in §5 and we need to add restrictions to Frag IR to ensure that it is possible. Indeed, the translation requires a linear usage of memory fragments [33]. In particular, the fragments given as arguments to `Frag.write` are considered as "consumed" and must not be used after. Note that this condition is respected for `c0a` and `c1a` in Figure 8.

**Non-Aliasing.** A key property of Frag IR is that, thanks to the absence of a global state, memory operations have explicit dependencies. For instance in Figure 8, the accesses at addresses `p0` and `p1` operate on distinct memory fragments. They are thus semantically independent. In particular, one could commute the write on `p0` with the read on `p1` to parallelize the accesses. In the equivalent C function (Figure 8b), this transformation would require the inter-procedural information that pointers do not alias.

## 3.2 Footprints

Rather than having a single mutable global memory, Frag IR programs use several disjoint, immutable memory fragments. Memory fragments are values stored in variables but with a footprint representing their implementation in an unstructured memory. For instance, the footprint of a `cell<T> p` contains values for the addresses `[p; p + sizeof(T)]`. Formally

386

387

388

389

390

391

392

393

394

395

396

397

398

399

400

401

402

403

404

405

406

407

408

409

410

411

412

413

414

415

416

417

418

419

420

421

422

423

424

425

426

427

428

429

430

431

432

433

434

435

436

437

438

439

440
<figure><img src="image_5.png" /><figcaption>Figure 8. Updating Two Non-Aliasing Memory Cells in Frag IR (8a) and in C (8b)</figcaption></figure>

the footprint of a memory fragment is a heaplet in a simple separation logic [29]. The type of heaplets is described Figure 3. A heaplet is either invalid (⊥) or defined by a partial map from addresses to bytes and a set of permissions to deallocate memory ranges. We define a total disjoint union operator $\mathcal{W}$ on heaplets, it evaluates to ⊥ if its arguments are not disjoint. The empty heaplet ($\lambda_.(\mathit{None}, \mathit{None})$) is the neutral element of $\mathcal{W}$.

Our type of values includes two kinds of memory fragments: a generic one, $Vmem$, defined by an arbitrary valid heaplet and $Vcell$ which represents a memory cell that stores the byte encoding of a scalar value. We define a function `footprint`: `val` → `heaplet` which maps values to their memory footprints, using the empty heaplet for values that are not memory fragments. It is generalized to lists of values as the disjoint union of their footprints. We add dependent types inhabited by memory fragments. Memory cells inhabit types `cell<t> p`, where `t` is a scalar type and `p` a pointer variable. There are syntaxes for particular cases of $Vmem$, for instance `mrange p sz` is inhabited by memory fragments containing exactly the addresses `[p; p + sz]`. Similarly to abstract proposition, abstract memory fragments may be defined by predicates chosen by the producer of the program. Those predicates take as argument an heaplet and thus correspond to the notion of assertion in separation logic. More generally, any type $T$ closed in a context $\rho$ defines a set $\{\mathit{footprint}(v) | \rho \vdash v \in T\}$ of heaplets.

### 3.3 Memory Operations

Frag IR provides the equivalents of standard memory operations. Figure 9 describes their signatures. Instead of interacting with a global state, they take as argument and return memory fragments. Like for the functional stores used by Steensgaard [31], read and write operations take as arguments both a pointer `p` and a memory fragment `c` which

Frag.read<t>(p: ptr, c: cell<t> p)
: (r: t, post: *c = r)
Frag.write<t>(p: ptr, c: cell<t> p, v: t)
: (c': cell<t> p, post: *c' = v)
Frag.malloc sz: int) : (p: ptr, m: malloc p sz)
Frag.free(p: ptr, sz: int, m: malloc p sz) : ()
Frag.joinable(args...) : (post: joinable args)

<caption>Figure 9. Signatures of the Operations on Memory Fragments Described in §3.3 and §3.4</caption>

represent a cell at this address. The operation Frag.read retrieves the value `r` from its cell argument, its post-condition reflects the fact that `r` is the content `*c` of the cell. Since memory fragments are immutable, Frag.write returns a new cell `c'` at the same address `p` but which now stores the value `v` given as argument. Programs allocate memory fragments with Frag.malloc, which takes as argument the size `sz` of the range to allocate and return a pointer `p` and a memory fragment of type `malloc sz`. Its semantics is non-deterministic, it either fails and returns the null pointer and an empty fragment, or returns an arbitrary non-null pointer with a fragment containing arbitrary values for the range `[p; p + sz]` and the permission to deallocate this range. The semantics of the type `malloc` reflects those two cases. Conversely Frag.free represents the deallocation of a fragment of type `malloc sz`, semantically it is a no-op.

Since they do not access any implicit global state, memory operations that operate on distinct variables can always be commuted. Moreover, thanks to the dependent types of the memory fragments given as arguments, those operators, most interestingly Frag.read, are total.

The linearity condition on Frag IR considers that the fragments given as arguments to Frag.write and Frag.free are consumed and must not be used later. Reading a cell

496

497

498

499

500

501

502

503

504

505

506

507

508

509

510

511

512

513

514

515

516

517

518

519

520

521

522

523

524

525

526

527

528

529

530

531

532

533

534

535

536

537

538

539

540

541

542

543

544

545

546

547

548

549

550
does not consume it, but consumed cells can no longer be read. This linearity condition does not affect the semantics or typing of programs. It is thus possible to reason about programs that do not use fragments linearly. Our approach is to maintain this linearity as an informal invariant during the compilation pipeline and to validate it defensively during the translation to a global memory (§5), but the semantics still allow transformations to rely on the separation of fragments.

## 3.4 Non-Disjointness of the Fragments

Since Frag.malloc does not access a global state, the non-deterministic choice of the returned address is not constrained by other existing allocations. That is, in Figure 10, although p1 is allocated line 2 after p0 and before its deallocation, the semantics allows p1 to take the same value as p0. This may be surprising, but it avoids implicit dependencies between allocations and provides opportunities for optimisations. For instance, if m0 and m1 are used in non-overlapping ranges, they could be allocated at the same location. This semantics also enables the representation of pointers with bounded machine integers while avoiding issues related to the fact that there is only of finite number of them [3]. Indeed, in models where the set of pointers is finite, programs may exhaust this set with successful allocations and reach a state where a new allocation would necessarily fail. In such state, even if the result of this new allocation is freed immediately after a test of success, it would be unsound to remove it since it necessarily fails. Although such examples are artificial, they prevent the formal justification of some transformations in models with a finite global memory state.

We still provide a way for programs to require the disjointness of memory fragments, from which pointer inequalities can be deduced. We make such requirements explicit, with operations Frag.joinable (Figure 9). This operator takes arbitrary arguments args and ensures that their footprints can be joined into a valid heaplet. This property is reflected with the proposition joinable args as post-condition. The semantics of Frag.joinable is a particular case of assume instructions that can be found in verification languages [20]. That is, it is the opposite of an UB: executions that reach a Frag.joinable operation with non-disjoint arguments are ignored when considering the set of behaviors of a program. However, it does not cancel previous UBs or external events. For instance in Figure 10, an assertion $p0 = p1 = null \lor p0 \neq p1$ would still generate an UB line 3, but not line 5. Hence, operations Frag.joinable cannot be commuted below instructions which may have UB, like assert. Moreover, Frag.joinable restricts the set of valid compilations of a program. In particular, it could prevent the elimination of dead allocations.

## 3.5 Lemmas Operations on Memory Fragments

We need a way to split and merge memory fragments. Steensgaard [31] introduces two operations for this purpose: merge

1. `let p0, m0 = Frag.malloc sz);`
2. `let p1, m1 = Frag.malloc sz);`
3. This point can be reached with $p0 = p1 \neq null$
4. `let H = Frag.joinable(m0, m1);`
5. At this point $p0 = p1 = null \lor p0 \neq p1$
6. `Frag.free(p0, sz, m0); Frag.free(p1, sz, m1);`

<caption>**Figure 10.** A Frag IR Program Which Performs Two Memory Allocations with Overlapping Live Ranges</caption>

and restrict. For Frag IR, we generalize the lemmas so that they can consume as set of memory fragments to produce an equivalent set of new ones. For instance a memory range can be split using a lemma with the following signature:

(p: ptr, n: int, a: int, r: mrange p n, LE: a $\le$ n)
: (r0: mrange p a, r1: mrange (p+a) (n-a))

Formally, we generalize the semantics of lemma following the idea that footprint maps types to assertions of separation logic. Lemmas should then be the equivalent of entailments, which leads to the following soundness condition:

**Definition 3.1** (Soundness of lemmas, generalized version). A lemma with arguments types arg and result types res is sound if:

$$ 
\begin{align*}
\forall \text{varg. } (\text{varg} \vdash \text{varg} \in \text{arg}) &\Rightarrow \\
\exists \text{vres. } (\text{varg}, \text{vres} \vdash \text{vres} \in \text{res}) &\wedge \\
\text{footprint}(\text{varg}) \neq \perp &\wedge \\
\text{footprint}(\text{vres}) = \text{footprint}(\text{varg}) &
\end{align*}
$$

That is, we additionally require the disjointness of the footprints of the arguments, the disjointness of the footprints of the results and the (extensional) equality of their unions. Note that this definition coincides with definition 2.1 when the arguments and results are not memory fragments, since the additional conditions are true for empty heaplets. This formula differs from a standard separation logic entailment by the position of the disjointness of the footprints of the arguments ($\text{footprint}(\text{varg}) \neq \perp$). It would normally be given as an hypothesis (like $\text{varg} \vdash \text{varg} \in \text{arg}$) but we instead require lemmas to prove it. In a program verification setting, this disjointness is usually justified when using an entailment with the existence of a global state which satisfies the premises. In our semantics, there is no such state and variables can have non-disjoint footprints. We instead require lemmas to prove the validity of the footprint of their arguments from the types of the arguments. A Frag.joinable operation can always be used before a lemma to ensure this disjointness. For instance the lemma of Figure 11 merges the head of a linked list with its tail using the assumption that their footprints are disjoints.

Lemmas which return memory fragments have a non-deterministic semantics: their results is an arbitrary list of
```c
let JOINABLE = Frag.joinable(hd, tl);
let ll : mem<?linked_list> p0 = lemma {
    (p0: ptr, p1: ptr,
     hd: mem<?list_cell> p0 p1,
     tl: mem<?linked_list> p1,
     JOINABLE: joinable hd tl)
  : (ll: mem<?linked_list> p0)
}(p0, p1, hd, tl, JOINABLE);
```

<caption>Figure 11. Snippet of a toy program which uses singly linked lists. The lemma merges two memory fragments representing a list cell `hd`: `mem<?list_cell> p0 p1` at address `p0` pointing to `p1` and a linked list `tl`: `mem<?linked_list> p1` starting at `p1` into a linked list at address `p0`.</caption>

```c
let m0, m1 = lemma {
    (p: ptr, c: cell(int> p) : (m0: mtrue, m1: mtrue)
    }(p, c);
let _ = assert<is_cell p m0>();
```

<caption>Figure 12. A Program with an UB Due to the Non-Deterministic Semantics of lemma</caption>

values of the expected types whose footprint is equal to the footprint of the arguments. They thus do not require an effective way of transforming the memories (for instance using a set of addresses for each output fragment). However, the types of the results must be restrictive enough to ensure that the chosen fragments are the expected ones. As a counterexample, the program of Figure 12 uses a lemma to split a cell `c` into two memory fragments `m0` and `m1` of type `mtrue` (inhabited by all fragments). The lemma may thus put some of the bytes of the cell in the second fragment, and the following assertion that `m0` has the same footprint as a cell will have an UB in this case. This example could be fixed by adding a post-condition `is_cell p m0` in the results of the lemma.

The soundness condition ensures that there always exist values that satisfy our requirements on the results. Contrary to Frag.joinable, lemmas can thus be commuted with UB.

# 4 Parametrized IR in Functional SSA

Our formalisation of Frag IR is modularized into two parts. The first part defines a generic structure of programs which is parametrized by types and operators. The second part instantiates it with the types and operators of Frag IR. In Rocq, we implemented this parametrization using type classes.

In order to support dependent types, the generic structure implements a functional flavor of Static Single Assignment (SSA), described in §4.1. Keeping a modular approach, we define the semantics (§4.2) and some passes (§4.3) on the generic representation before instantiating them for Frag IR.

## 4.1 Functional SSA Structure

For our dependent type system to be sound, the variables that appear in the type of a variable `x` must have the same value when `x` is assigned and when `x` is used. This referential transparency property is enforced in Static Single Assignment (SSA) [28] representations of programs. We choose to implement a functional variant of SSA [1]: variables are immutable and their use syntactically restricted to a scope dominated by their point of definition. The instructions of our generic representation are defined inductively Figure 13. Each instruction has a static acidity corresponding to the number of values it evaluates to. Our type of instruction include a monadic return which evaluates a list of variables, in general, it does not terminate the enclosing function. The evaluation of operators of the IR instance on some type and value arguments returns their results but can also perform side-effects. Figure 13 recalls some operators of Frag IR, including lemma. Like in functional languages, a let construct executes sequentially two instructions with the results of the left-hand side bound in the right-hand side. A conditional `if` branch branches over a boolean variable `b` and reflects its value by binding a second variable `H` with a proposition type.

Functional SSA [1] implements arbitrary control flow graphs using locally defined functions that are called in terminal position. Our representation thus features krec blocks, which define local, mutually recursive continuations. Figure 14 illustrates their use to encode loops. Each block defines one or several continuations, which take some arguments and are implemented by instructions. The execution of a block starts with the first continuation, with the arguments given to krec. Continuations are not values, from within the block they can be jumped to using `kcall`. The call takes arguments corresponding to the signature of the continuation and does not return to the call point. The execution of a krec block ends when one of its continuations returns or calls a continuation defined in an outer block. Local continuations act as confluence points of the control flow graph. The arguments given to `kcall` play the same role as $\phi$-functions in standard SSA-representations [10]: the value bound to an argument depends on the point where the call is performed. It is crucial to be able to define continuations locally with krec blocks and not only at the top-level of functions. This enables continuations to access variables defined in outer scopes, such as `c` in Figure 14. Otherwise continuations would take as arguments all live variables, which would be the equivalent of adding a $\phi$-function for every variable at every confluence point. Without syntactical restriction, there can also be confluence points at the end of `if` and `krec`. If desirable, those confluence points could be turned into `kcall`.

Functions are called using `fcall`. They are defined by an instruction and return its evaluation. We allow functions with multiple results, which is useful for propositions and
<figure><img src="image_6.png" /><figcaption>**Figure 15.** Semantics of Instructions and Programs in Our Generic Representation</figcaption></figure>

This enables the use of a total function for the value environment $\rho$ and avoids taking into account in the semantics some errors that are statically ruled out. For instance in the semantics of programs, this justifies that there is always an implementation $p f$ for the functions called.

**Instantiation for Frag IR.** For Frag IR, we build a domain using the LTS model provided by `smonad` [5, §5]. We apply on it a transformer [5, §6.3] to add some external events of input/output. This yields a domain `Frag.sem_t` which supports the effects of divergence, non-determinism, UB and external events. The refinement relation on `Frag.sem_t` is a backward simulation [21], which implies the inclusion of the set of behaviors modulo the refinement of UBs.

## 4.3 Generic Passes over the Generic SSA IR

Our modular approach extends to the definition of passes and their proof of correctness. We define several passes on the generic representation: a type-checker, a simplification pass and an erasure pass. The generic parts of those passes deal with the structure of instructions and programs, in particular the handling of variables and continuations. They are parametrized by functions that handle the parts specific to the instances.

**Type-Checker.** Our type-checker verifies that its input program is well-formed (that is, that variables, continuations and functions are bounds and that the arities are respected) and well-typed. However, for Frag IR, it does not guarantee the soundness of lemmas. It is parametrized by functions that check that types and operator are well-formed, a comparison function on types and the signatures of operators.

**Simplification.** We implemented a simplification pass relying on the monad laws to linearise sequences of let binders and to reduce return when they appear on the left of

<figure><img src="image_7.png" /><figcaption>**Figure 16.** Example of the Simplification Pass</figcaption></figure>

a `let`. Figure 16 describes an example of simplification. This pass do not need anything specific to the instance, except the monad laws on the domain `sem_t`, which we always assume.

**Erasure.** The generic erasure pass removes dead variables and operations. It is inter-procedural: it is able to remove arguments and results of functions but not the function calls themselves. It is parametrized by boolean predicates which choose which variables and operators to remove. We do not require any formal specification on the choice of erased variables but fail during the execution of the pass if it is not consistent (for instance if an erased variable is used as argument in an operator which is kept). We require however that the erased operations only have side-effects that can be removed according to the refinement relation on `sem_t` [5, §6.2]. For instance, `assert` can be removed since UBs can be refined by anything. On the contrary, we must preserve external events and cannot remove operations that emit them. We prove that the result of a successful run of the erasure pass on a well-typed program is also well-typed and that its semantics refines the semantics of the source.

Thanks to the parametrization by the choice of erased variables and operations, the instances of the erasure pass can either be directed by the types of the variables, annotations or a dead code analysis. We implemented an analysis on the generic IR, parametrized by a function specifying which operations cannot be removed even if their results are not

881

882

883

884

885

886

887

888

889

890

891

892

893

894

895

896

897

898

899

900

901

902

903

904

905

906

907

908

909

910

911

912

913

914

915

916

917

918

919

920

921

922

923

924

925

926

927

928

929

930

931

932

933

934

935

936

937

938

939

940

941

942

943

944

945

946

947

948

949

950

951

952

953

954

955

956

957

958

959

960

961

962

963

964

965

966

967

968

969

970

971

972

973

974

975

976

977

978

979

980

981

982

983

984

985

986

987

988

989

990
<figure><img src="image_8.png" /><figcaption>**Figure 17.** Two semantically correct erasures of a dead allocation. However the left one introduces memory leak and uses memory fragments in an affine but non-linear way. Currently, our DCE leaves such program unchanged.</figcaption></figure>

used. Thanks to the SSA structure, this analysis is performed by generating and solving a sparse data-flow problem [8, 28]. Since the erasure pass checks defensively the consistency of the choice of the variables and operations removed, we do not prove formally the correctness of the analysis but still obtain the soundness of successful runs.

We instantiate the analysis and erasure on Frag IR. We do not prove formally that the pass preserves the linear usage of memory fragments, but this property is desirable. For this reason, we take into account the linearity when deciding which operators the analysis should consider as removable. In particular, the semantics of Frag.free has no side-effects and could always be considered as dead since it does not return any value. However, as illustrated Figure 17, one should only remove it if we are also able to remove a corresponding Frag.malloc. We currently prohibit the removal of all operators involving memory fragments, except Frag.read. In the future, we may extend this pass or write a dedicated one to remove dead stores and allocations.

# 5 Compilation to a Lower Level

In Frag IR, we introduced proposition types and memory fragments as means of propagating information and justifying transformations during compilation. However, in order to execute efficiently the programs, one needs to translate the transformed programs to a more standard representation. In particular, one must use a single global memory instead of memory fragments. We define in §5.1 Flat IR, a representation that extends Frag IR by adding a global memory state. We then consider the problem of compiling Frag IR programs into Flat IR programs that no longer contain propositions nor memory fragments. We implemented this compilation in two passes (Figure 18). The first one is a translation pass from Frag IR to Flat IR which inserts accesses to the global memory corresponding to the operations on memory fragments (§5.2). The second one is an instance of the erasure pass (§4.3) that removes propositions and memory fragments. Although the resulting programs still use functional SSA, they only contain usual operators of middle-end representations (e.g. Cminor of CompCert or LLVM IR).

## 5.1 Flat IR

We define Flat IR, a lower level representation. It is another instance of the generic representation of §4, in particular, it has the same syntax as Frag IR. We reuse the values and types of Frag IR and extends its set of operators. We add partial operations, without preconditions but which have UB for some values of their arguments. For instance, Flat IR has a partial division operation with the following signature:

```
pdiv(n: int, d: int) : (r: int, post: r = n / d)
```

We choose to keep a post-condition, to be consistent with the signature of the total operations such as add, inherited from Frag IR. Programs in Flat IR have access to a global memory, using standard operators described in Figure 19.

The semantics of Flat IR is defined in a stateful domain *Flat.sem_t*, derived from *Frag.sem_t* by applying a state transformer ([5, §6.3]). The semantics thus takes the global memory as input and output (its type *mem* is defined in Figure 3 as a total map with access and deallocation permissions). In particular, the memory is transmitted during the internal calls thanks to a family of events (*EventFam.State mem E*) which contains the events of *E* with the memory as additional argument and result. That is, we define:

$$ \mathit{Flat.sem}_t E A := \mathit{mem} \rightarrow \mathit{Frag.sem}_t (\mathit{EventFam.State mem E}) (A \times \mathit{mem}) $$

The domain *Flat.sem_t* inherits the effects of *Frag.sem_t*. In particular, we lift the semantics of the operators of Frag IR into *Flat.sem_t* by returning the input memory unchanged. We derive a refinement relation on *Flat.sem_t* from the backward simulation on *Frag.sem_t*.

## 5.2 Translation of the Memory Fragments

Memory fragments are an abstraction that we implement using a global memory state during the translation pass from Frag IR to Flat IR. As anticipated in §3, this translation requires a linear usage of the fragments [33], but we do not enforce formally this invariant during the compilation pipeline. Instead the translation pass checks this linearity defensively. This check is performed by computing at each program point a set of active memory fragments.

**Definition 5.1** (Set of active variables). During an execution, a variable storing a memory fragment is consumed if it is given as argument to *return*, *kcall*, *fcall*, *krec*, *Frag.write*, *Frag.free* or *lemma*.

Given a program point in a scope *V* of variables, a set *A* ⊆ *V* of *active variables* is a set of variables such that in any execution reaching this point, the variables of *V* that have not yet been consumed are exactly *A*.

The translation traverses the body of each function in a forward fashion, starting from the entry where the set of active variables is exactly the arguments of the function. Our definition of active sets requires a linear usage of the
<figure><img src="image_9.png" /><figcaption>Figure 18. Compilation of a program from Frag IR to Flat IR. Sets of active variables inferred by the translation are annotated.</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Figure 19. Signatures of the Operations on Global Memory</figcaption></figure>

memory fragments, not only an affine one. That is, memory fragments must be consumed explicitly in order to be removed from the set of active variables. A consequence is that the translation only need to pass once through each program point since the set of active variables at a point can be determined from any path reaching it. In particular, we do not need annotations to infer sets of active variables in loops built with `krec`. The translation checks that variables are only used at points where they are active, that incoming sets of active variables are equals at confluence points and that memory fragments are consumed at the end of their scopes. It also rejects programs containing unreachable code.

When it accepts its input program, the translation compiles it into Flat IR by inserting effectful operations. Proposition and memory fragments are kept as ghost variables, we delegate their removal to the erasure pass which is ran after the translation (Figure 18). Syntactically the translation of an instruction has thus access to the same variables and has the same parity. The correctness relies on an invariant (called `mem_match`) between the footprints of the active memory fragments and the global memory.

**Definition 5.2.** Given a heacket *h* and a memory *m* the relation `mem_match h m` holds if and only if:

* $h \neq \perp$

* The addresses with permission *Writable* in *m* are exactly those with a value in *h* and *m* agrees with *h* on them.

* They contain the same deallocation permissions.

The correctness of the translation of instructions is specified as a refinement in *Frag.sem_t* i.e. a backward simulation.

**Definition 5.3.** A Flat IR instruction *trg* is a correct translation of a Frag IR instruction *src* if for any well-typed values $\rho$ for their common scope, heacket *frame* and memory *m*:

$$ \text{mem\_match}(\text{footprint}(\rho(A_{\text{entry}})) \uplus \text{frame}) m \Rightarrow \\ \llbracket \text{src} \rrbracket_{\text{instr}} \rho \geq \text{Post} \llbracket \text{trg} \rrbracket_{\text{instr}} \rho m $$

where:

* $A_{\text{entry}}$ is the set of active variables at the entry of the instruction

* The relation *Post* requires the equality of the results of the semantics and *mem_match* to hold between the set $A_{\text{exit}}$ of active variables at the exit point, the values *vres* returned or given as argument to a continuation and the new global memory *m*':

$$ \text{mem\_match}(\text{footprint}(\rho(A_{\text{exit}})) \uplus \text{footprint}(vres) \uplus \text{frame}) m' $$

The heacket *frame* contains the part of the initial memory *m* not covere active variables. This specification ensures that this part is not modified, which enables reasoning similar to the frame rule of separation logic [29]. It is used during function calls: the correctness of the callee is instantiated with a frame extended with the active variables of the caller.

The translation of instructions is performed by induction on the syntax. The most interesting cases are the translations of operations, some of them can be observed in Figure 18. The operators of Frag IR with a pre-condition (such as `div`) are replaced by their partial counter-parts. Operators on the global memory are inserted to reflect the transformations on memory fragments. In order to return the same memory fragments and post-conditions as the source, we keep some operators on memory fragments, and use semantically justified assertions. Lemmas are unaffected, which is correct since the footprint of their result is equal to the footprint of the arguments they consume. Finally, the assumptions *Frag.joinable* are turned into assertions. Indeed, they are semantically justified by the fact that their arguments are simultaneously active, and are thus disjoints because of the hypothesis *mem_match*.
# 6 Related Works

**Proof Carrying Code.** Some properties of low-level code from an untrusted source or compiler can be verified using an accompanying machine-checkable proof [1, 26]. A compiler may produce such certificate by translating a source-level proof. Our encoding of information with dependent types is motivated by a similar need for expressiveness. However our goal is not to check the information encoded in a program. In particular, we do not carry a representation of the proofs of lemma instructions. Moreover, we prove once and for all that our compilation passes generate target code which semantically refine the source, according to a notion of backward simulation. One can thus establish complex properties on the behavior of the target without encoding them in the type system. This refinement property also enables the use of the `assert` instruction since it implies that the target does not have UB if the source does not.

**Representation of Aliasing Information.** Several encoding of generic aliasing information exist in the literature. Some approaches rely on variables representing fragments of the memory [9, 16, 31]. The memory fragments of Frag IR are close to the functional stores of Steensgaard [31]. Jung [16] gives a formal justification of the implementation of functional stores with a global memory using an affine type system. Both systems use operators (`restrict` or `split`) directed by annotations (abstract location or set of addresses) to transform fragments. Our lemma operation is directed by the types of the output fragments. Another difference is that our approach statically guarantees the validity of memory operations. However, we do not make any claim on the use of partial aliasing information provided by analyses and instead assume that precise information is known.

In FIRM [7] memory dependencies are represented using memory values. Contrary to Frag.read, their Load node produces a new memory which is used to express the ordering with later nodes. A Sync node combines several memories, but there is no explicit operation to split memories. It is thus unclear whether the semantics of this representation could be formalized without a global state. Some representations [15] use dependencies directly between memory accesses, without any explicit representation of the memory.

Other approaches [12, 27] associate to each syntactic address constraints on their dynamic values (result of points-to analysis, properties derived from the structure of the source language, annotations provided by the programmer...). Optimisations can then test if two addresses overlap by checking whether the sets of pointers allowed by their respective constraints intersect. In LLVM [22], the noalias and noalias scope metadata on memory accesses enable the propagation of source information (such as the `restrict` qualifier of C) in a way compatible with function inlining.

**Aliasing Models for Rust.** The borrow checker of the Rust language enforces non-aliasing properties. Stacked Borrows [17] and Tree Borrows [32] are memory models that encode this information by considering as UBs invalid uses of references. They can be used to obtain non-aliasing information on Rust programs, if the unsafe code also adheres to the formalised discipline. Some program transformations can be verified within representations using those memory models [13]. In particular, Tree Borrows inserts implicit accesses [32, §3.2] that justify the validity of speculative reads.

**Representation of the Memory with Values.** Several recent verification tools [11, 14, 23] leverage the non-aliasing guarantees of the safe fragment of Rust to avoid reasoning on a global state. References are instead directly represented as values. Melquiond and Moreau [25] designed a domain specific language for algebra libraries where arrays are stored in mutable variables and passed by copy-restore. Instead of using UB, they rely on dependant types to track the size of the arrays and to emit out-of-bounds checks.

**Formalisations of SSA.** Conventional forms of SSA and transformations exploiting it have been formalized in Vellvm [36] and CompCertSSA [2]. Both of those developments reason on the dominance relation in control flow graphs. In our approach based on functional SSA [1], syntactic scopes provide an under-approximation of dominance.

**Parametrization and Abstraction of Effects.** MLIR [18] is extensible thanks to dialects and enables the encoding of Domain Specific Languages. Abstracting over effects and arbitrary computations would be necessary for the formalisation of such highly generic compiler infrastructure.

CompCert [21] now supports several target assemblies. The intermediate representations and passes remain generic thanks to the use of target specific modules with a common signature. Vélus [6, §4.1] uses the module functors provided by Rocq for a similar purpose. The generic parts of those developments abstract over the semantics of operators but the effects of those semantics are a strict subset of the effects of the languages. In contrast, we abstract over operators that use nearly all effects and even over the effects themselves.

Interaction Trees [34, 35] enables the representation of effectful computations with events. Incrementally interpreting those events yields a sequence of semantics in increasingly expressive semantic domains. Thanks to a compatibility between this interpretation and refinements, transformations that preserve effectful computations may be proven without interpreting all events, that is, in simpler domains.

# References

[1] Andrew W. Appel. 1998. SSA is functional programming. ACM SIGPLAN Notices 33, 4 (April 1998), 17–20. doi:10.1145/278283.278285

[2] Gilles Barthe, Delphine Demange, and David Pichardie. 2014. Formal Verification of an SSA-Based Middle-End for CompCert. ACM Transactions on Programming Languages and Systems 36, 1 (March 2014),

1266

1267

1268

1269

1270

1271

1272

1273

1274

1275

1276

1277

1278

1279

1280

1281

1282

1283

1284

1285

1286

1287

1288

1289

1290

1291

1292

1293

1294

1295

1296

1297

1298

1299

1300

1301

1302

1303

1304

1305

1306

1307

1308

1309

1310

1311

1312

1313

1314

1315

1316

1317

1318

1319

1320
1321

1-35. doi:10.1145/2579080

1322

[3] Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, and Steve Zdancewic. 2024. A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction. *Proceedings of the ACM on Programming Languages* 8, ICFP (Aug. 2024), 789–817. doi:10.1145/3674652

1323

1324

1325

1326

1327

1328

1329

1330

1331

1332

1333

1334

1335

1336

1337

1338

1339

1340

1341

1342

1343

1344

1345

1346

1347

1348

1349

1350

1351

1352

1353

1354

1355

1356

1357

1358

1359

1360

1361

1362

1363

1364

1365

1366

1367

1368

1369

1370

1371

1372

1373

1374

1375

[4] Yves Bertot, Benjamin Grégoire, and Xavier Leroy. 2006. A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. In *Types for Proofs and Programs*, Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 66–81.

[5] Benjamin Bonneau. 2025. Relational reasoning on monadic semantics. In *36es Journées Francophones des Langages Applicatifs (JFLA 2025)*. Roiffé, France, 18–37. doi:10.5281/zenodo.14508391

[6] Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg. 2017. A formally verified compiler for Lustre. In *Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation*. ACM, Barcelona Spain, 586–601. doi:10.1145/3062341.3062358

[7] Matthias Braun, Sebastian Buchwald, and Andreas Zwinkau. 2011. *Firm-A Graph-Based Intermediate Representation*. Technical Report 35. Karlsruhe. https://pp.ipd.kit.edu/publication.php?id=braun11wir

[8] Jong-Deok Choi, Ron Cytron, and Jeanne Ferrante. 1991. Automatic construction of sparse data flow evaluation graphs. In *Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '91*. ACM Press, Orlando, Florida, United States, 55–66. doi:10.1145/99583.99594

[9] Fred Chow, Sun Chan, Shin Ming Liu, Raymond Lo, and Mark Streich. 1996. Effective representation of aliases and indirect memory operations in SSA form. In *Compiler Construction*. Vol. 1060. Springer Berlin Heidelberg, Berlin, Heidelberg, 253–267. doi:10.1007/3-540-61053-7_66 Series Title: Lecture Notes in Computer Science.

[10] Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. 1991. Efficiently computing static single assignment form and the control dependence graph. *ACM Transactions on Programming Languages and Systems* 13, 4 (Oct. 1991), 451–490. doi:10.1145/115372.115320

[11] Xavier Denis, Jacques-Henri Jourdan, and Claude Marché. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. In *Formal Methods and Software Engineering*. Vol. 13478. Springer International Publishing, Cham, 90–105. doi:10.1007/978-3-031-17244-1_6 Series Title: Lecture Notes in Computer Science.

[12] Rakesh Ghiya, Daniel Lavery, and David Sehr. 2001. On the importance of points-to analysis and other memory disambiguation methods for C programs. In *Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation*. ACM, Snowbird Utah USA, 47–58. doi:10.1145/378795.378806

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

[14] Son Ho and Jonathan Protzenko. 2022. Aeneas: Rust verification by functional translation. *Proceedings of the ACM on Programming Languages* 6, ICFP (Aug. 2022), 711–741. doi:10.1145/3547647

[15] W.W. Hwu, R.E. Hank, D.M. Gallagher, S.A. Mahlke, D.M. Lavery, G.E. Haab, J.C. Gyllenhaal, and D.I. August. 1995. Compiler technology for future microprocessors. *Proc. IEEE* 83, 12 (Dec. 1995), 1625–1640. doi:10.1109/5.476079

[16] Ralf Jung. 2013. *An Intermediate Language To Formally Justify Memory Access Reordering*. Bachelor's Thesis. Saarland University. https://research.ralfj.de/bachelor/bachelor.pdf

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

[18] Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, and Oleksandr Zinenko. 2021. MLIR: Scaling Compiler Infrastructure for Domain Specific Computation. In *2021 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)*. 2–14. doi:10.1109/CGO51591.2021.9370308

[19] Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, and Nuno P. Lopes. 2017. Taming undefined behavior in LLVM. In *Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation*. ACM, Barcelona Spain, 633–647. doi:10.1145/3062341.3062343

[20] K. Rustan M. Leino. 2008. This is Boogie 2. (June 2008). https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/

[21] Xavier Leroy. 2009. A Formally Verified Compiler Back-end. *Journal of Automated Reasoning* 43, 4 (Dec. 2009), 363–446. doi:10.1007/s10817-009-9155-4

[22] LLVM Project. 2025. LLVM Language Reference Manual. https://llvm.org/docs/LangRef.html

[23] Yusuke Matsushita, Takeshi Tsukada, and Naoki Kobayashi. 2021. RustHorn: CHC-based Verification for Rust Programs. *ACM Transactions on Programming Languages and Systems* 43, 4 (Dec. 2021), 1–54. doi:10.1145/3462205

[24] Conor McBride. 2015. Turing-Completeness Totally Free. In *Mathematics of Program Construction*. Vol. 9129. Springer International Publishing, Cham, 257–275. doi:10.1007/978-3-319-19797-5_13 Series Title: Lecture Notes in Computer Science.

[25] Guillaume Melquiond and Josué Moreau. 2024. A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler. *Proceedings of the ACM on Programming Languages* 8, ICFP (Aug. 2024), 121–146. doi:10.1145/3674629

[26] George C. Necula. 1997. Proof-Carrying Code. In *Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '97)*. Association for Computing Machinery, New York, NY, USA, 106–119. doi:10.1145/263699.263712 event-place: Paris, France.

[27] Steven Novack, Joseph Hummel, and Alexandru Nicolau. 1996. A simple mechanism for improving the accuracy and efficiency of instruction-level disambiguation. In *Languages and Compilers for Parallel Computing*, Chua-Huang Huang, Ponnuswamy Sadayappan, Utpal Banerjee, David Gelernter, Alex Nicolau, and David Padua (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 289–303.

[28] Fabrice Rastello and Florent Bouchez Tichadou (Eds.). 2022. SSA-based Compiler Design. Springer International Publishing, Cham. doi:10.1007/978-3-030-80515-9

[29] J.C. Reynolds. 2002. Separation logic: a logic for shared mutable data structures. In *Proceedings 17th Annual IEEE Symposium on Logic in Computer Science*. IEEE Comput. Soc, Copenhagen, Denmark, 55–74. doi:10.1109/LICS.2002.1029817

[30] Valentin Robert and Xavier Leroy. 2012. A Formally-Verified Alias Analysis. In *Certified Programs and Proofs*. Vol. 7679. Springer Berlin Heidelberg, Berlin, Heidelberg, 11–26. doi:10.1007/978-3-642-35308-6_5 Series Title: Lecture Notes in Computer Science.

[31] Bjarne Steensgaard. 1995. Sparse functional stores for imperative programs. In *Papers from the 1995 ACM SIGPLAN workshop on Intermediate representations*. ACM, San Francisco California USA, 62–70. doi:10.1145/202529.202536

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

1376

1377

1378

1379

1380

1381

1382

1383

1384

1385

1386

1387

1388

1389

1390

1391

1392

1393

1394

1395

1396

1397

1398

1399

1400

1401

1402

1403

1404

1405

1406

1407

1408

1409

1410

1411

1412

1413

1414

1415

1416

1417

1418

1419

1420

1421

1422

1423

1424

1425

1426

1427

1428

1429

1430

1369

1370

1365

1366

1367

1368

1369

1370

1371

1372

1373

1374

1375
1431

1432

1433

1434

1435

1436

1437

1438

1439

1440

1441

1442

1443

1444

1445

1446

1447

1448

1449

1450

1451

1452

1453

1454

1455

1456

1457

1458

1459

1460

1461

1462

1463

1464

1465

1466

1467

1468

1469

1470

1471

1472

1473

1474

1475

1476

1477

1478

1479

1480

1481

1482

1483

1484

1485

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

[34] Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. Interaction trees: representing recursive and impure programs in Coq. *Proceedings of the ACM on Programming Languages* 4, POPL (Jan. 2020), 1-32. doi:10.1145/3371119

[35] Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic. 2021. Modular, Compositional, and Executable

Formal Semantics for LLVM IR. *Proc. ACM Program. Lang.* 5, ICFP (Aug. 2021). doi:10.1145/3473572
Place: New York, NY, USA Publisher: Association for Computing Machinery.

[36] Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic. 2013. Formal verification of SSA-based optimizations for LLVM. *ACM SIGPLAN Notices* 48, 6 (June 2013), 175-186. doi:10.1145/2499370.2462164

1486

1487

1488

1489

1490

1491

1492

1493

1494

1495

1496

1497

1498

1499

1500

1501

1502

1503

1504

1505

1506

1507

1508

1509

1510

1511

1512

1513

1514

1515

1516

1517

1518

1519

1520

1521

1522

1523

1524

1525

1526

1527

1528

1529

1530

1531

1532

1533

1534

1535

1536

1537

1538

1539

1540