Nick Benton

♥ ✐❝❦❅

Nicolas Tabareau

Compiling Functional Types to Relational Specifications for Low Level Imperative Code

Keywords: F.3.1 [Logics and meanings of programs]: Specifying and Verifying and Reasoning about Programs-Mechanical verification, Specification techniques, F.3.3 [Logics and meanings of programs]: Studies of Program Constructs-Type structure, D.3.4 [Programming Languages]: Processors-Compilers, D.2.4 [Software Engineering]: Software / Program Verification-Correctness proofs, formal methods Languages, theory Compiler verification, type soundness, relational parametricity, separation logic, proof assistants

We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple functional language into an idealized assembly language. Types in the highlevel language are interpreted as binary relations, built using both second-order quantification and separation, over stores and values in the low-level machine.

Introduction

What kinds of correctness properties do we wish to establish of our compilers? The most obvious answer is that when a high-level source program is compiled to produce a low-level target, the behaviour of the target always agrees with a high-level semantics of the source. But we usually also want to be sure that the target code satisfies certain safety or liveness properties, ensuring that 'bad things' don't happen, or that 'good' ones do. Such properties include memory safety, adherence to information flow policies, termination, and various forms of resource boundedness. For applications in language-based security, the good news is that (fancy) type-like properties of this kind, which at least seem less complex to state and check than full functional correctness, are the important ones. On the other hand, for such applications one would really like to certify the code that actually runs, which involves formalizing and verifying type-like properties of machine code. How to do that is the problem we address here.

The approach is essentially that of our earlier work on specifying and verifying memory managers [START_REF] Benton | Abstracting allocation: The new new thing[END_REF] and type preservation for a simple imperative language (Benton and Zarfaty Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. TLDI'09, January 24, 2009, Savannah, Georgia, USA. Copyright c 2009 ACM 978-1-60558-420-1/09/01. . . $5.00 2007), and we will not repeat all the methodological arguments here. Briefly, we want to find low-level specifications that should be satisfied by target code compiled from source phrases of particular high-level types. Ideally, these specifications should be both modular and expressed without reference to concepts that are specific to the particular high-level language. This is important: we are not just interested in proving properties of complete, closed programs. We want (and have) to prove things about the result of linking or replacing bits of compiled code with code from elsewhere, including both the runtime system (which may be handcrafted machine code) or code compiled from other high-level languages. For maximum flexibility and strong guarantees, we would like these specifications to be semantic, i.e. defined extensionally in terms of the observable behaviour of programs rather than in terms of a purely syntactic type system for low-level code. One way of characterizing our goal is that we would like to know just what contract should be satisfied by a C or assembly language function that is intended to behave as an ML value of some (possibly higher order) type.

In previous work, we have proposed that these goals can be achieved by giving a semantics for high-level types as relational specifications over low-level code, and we have shown how this works out in the case of a very simple imperative language. The main contribution of the present paper is to show how such a low-level relational interpretation of types can be extended to a language with higher-order functions. The definitions and results presented here have been formalized in the Coq proof assistant. As we will explain, both our general low-level reasoning framework and its encoding in Coq have been improved relative to our earlier work. The Coq development is available from the authors' home pages.

Source and Target Languages 2.1 The Low Level Target

The idealized low level machine code into which we compile is the same as in our previous work. There is a single datatype, the natural numbers, though different instructions treat elements of that type as code pointers, heap addresses, integers, etc.. The store is a total function from naturals to naturals and the code heap is a total function from naturals to instructions (immutable and distinct from the data heap). Computed branches and address arithmetic are perfectly allowable. There is no built-in notion of allocation and no notion of stuckness or 'going wrong': the only observable behaviours are termination and divergence. There are no registers; we simply adopt a programming convention of using the first few memory locations in a register-like fashion.

The Coq specification of our machine involves an inductive type of ✐♥str✉❝t✐♦♥s, including halting, direct and indirect loads, stores and jumps, arithmetic and tests. Details can be found in the proof scripts or our earlier paper [START_REF] Benton | Formalizing and verifying semantic type soundness of a simple compiler[END_REF]; here we just use an obvious pseudocode in which, for example ✶✵✵✿ ❬✺( ← ❬❬✻(✰✶( ✴✴ ✐♥ ❈✿ ✯✺ ❂ ✯✭✯✻ ✰ ✶✮❀ means that the instruction at code address 100 reads the contents of the memory location following that pointed to by location 6, and stores the result in location 5. The mutable state of our machine is specified by

❉❡❢✐♥✐t✐♦♥ st❛t❡ ✿❂ ♥❛t → ♥❛t✳ ❉❡❢✐♥✐t✐♦♥ ♣r♦❣r❛♠ ✿❂ ♥❛t → ✐♥str✉❝t✐♦♥✳
and there is then a one-step transition function

❉❡❢✐♥✐t✐♦♥ s❡♠❴✐♥str ✭✐♥s✿✐♥str✉❝t✐♦♥✮ ✭s✿st❛t❡✮ ✭♣❝✿♥❛t✮ ✿ ♦♣t✐♦♥ ✭st❛t❡ ✯ ♥❛t✮ ✿❂ ✳✳✳
❋✐①♣♦✐♥t ❦st❡♣t❡r♠ ✭❦✿♥❛t✮ ✭♣✿♣r♦❣r❛♠✮ ✭s✿st❛t❡✮ ✭•✿♥❛t✮ ④str✉❝t ❦⑥ ✿ Pr♦♣ ✿❂ ♠❛t❝❤ ❦ ✇✐t❤ ⑤ ❖ ⇒ ❋❛•s❡ ⑤ ✭❙ •✮ ⇒ ♠❛t❝❤ s❡♠❴✐♥str ✭♣ •✮ s • ✇✐t❤ ⑤ ◆♦♥❡ ⇒ ❚r✉❡ ⑤ ❙♦♠❡ ✭s✬✱ •✬✮ ⇒ ❦st❡♣t❡r♠ • ♣ s✬ •✬ ❡♥❞ ❡♥❞✳ ❉❡❢✐♥✐t✐♦♥ t❡r♠✐♥❛t❡s ♣ s • := ∃ ❦✱ ❦st❡♣t❡r♠ ❦ ♣ s •✳
So a configuration terminates if there is some natural number k such that it terminates within k steps.

The High Level Source Language

Our source is a fairly conventional simply-typed, call-by-value functional language with recursion. The only mild novelty is that we have included a rudimentary form of refinement typing on the integer and boolean base types, indexing them by arbitrary Coq predicates:

A, B ::= Nat Pn | Bool P b | A → B | A × B
where Pn ⊆ N and P b ⊆ B. The refinements are not very sophisticated, but their addition is easy, mildly interesting and strengthens the type soundness result somewhat. Entailment on refinement predicates induces a subtype relation A <: B:

Pn ⊆ P ′ n Nat Pn <: Nat P ′ n P b ⊆ P ′ b Bool P b <: Bool P ′ b A <: A ′ B <: B ′ A × B <: A ′ × B ′ A ′ <: A B <: B ′ A → B <: A ′ → B ′
The terms are given by the following grammar:

M, N, P ::= b | n | x | λx.M | M N | Fixf x = M | M ⋆ N | M > N | if M then N else P | M, N | π1(M ) | π2(M )
where b ∈ B = {t, f}, n ∈ N and ⋆ ∈ {-, +, * }.

The type rules for our source language are shown in Figure 1. To deal with the presence of simple refinements, the type rules [Op] and [Gt] for the basic operations on integers involve abstract (in the sense of abstract interpretation) operations, lifting the concrete ones to predicates. The definitions of these abstract operations are:

P1 b ⋆ P2 = {n | ∃x ∈ P1, ∃y ∈ P2, (x ⋆ y = n)} P1 b > P2 = {b | ∃x ∈ P1, ∃y ∈ P2, (x > y ⇔ b)}.
The boolean refinements show up in the typing of conditionals, allowing one to type the branches under additional (meta-level) hypotheses about which way the test evaluated, much as in Hoare logic, GADTs or dependent type theories.

The Coq definition of the syntax and type rules of our source language comprises inductive definitions that translate the types, subtyping relation, untyped syntax and typing relation shown above in an entirely straightforward way. The only real differences between the LaTeX and Coq is that the Coq syntax uses de Bruijn indices rather than variable names, and that (slightly hackily) the Fix constructor in the Coq datatype really only binds f with the typing rule then insisting that the body be a lambda abstraction, binding x.

The Compiler

The compiler is a structurally-inductive Coq function that takes as input an untyped source expression ❡ and produces two pieces of low-level code: an auxiliary section, containing the code for the bodies of functions occurring in ❡, and a main section, which actually computes the value of ❡. In more detail:

❋✐①♣♦✐♥t ❝♦♠♣✐•❡ ✭❡ ✿ ❊①♣✮ ✭❛✉①❴❝♦❞❡✿ •✐st ✐♥str✉❝t✐♦♥✮ ✭❛✉①❴♥❡①t ✿ ♥❛t✮ ✭❛••♦❝ ❞❡❛••♦❝✿♥❛t✮ ④str✉❝t ❡⑥ ✿ ✭ ✭♥❛t ✲❃ •✐st ✐♥str✉❝t✐♦♥ ✯ ♥❛t ✯ ♥❛t✮ ✯ •✐st ✐♥str✉❝t✐♦♥ ✯ ♥❛t✮ ✿❂ ✳✳✳
Here ❛✉①❴❝♦❞❡ is a list of already-generated auxiliary instructions, ❛✉①❴♥❡①t is the code address from which further auxiliary instructions should be produced, and ❛••♦❝ and ❞❡❛••♦❝ are the entry points of the allocation and deallocation routines with which the compiled code will eventually be linked. The second and third components of the return value are the extended auxiliary code and and updated ❛✉①❴♥❡①t. The first component of the return value is a function that takes as input a start address for the main code and produces a triple comprising the instructions of the main code, the amount of stack space required by those instructions and the (slightly unnecessary) next free main code address. The generation of the main code is delayed in this way because we do not initially know how large the auxiliary code will be, and hence where we may produce the main code. When compiled code is running, the memory is broadly divided into a number of regions:

• The low-numbered locations 0-9, used in a register like fashion for passing arguments and returning results by compiled functions and by the allocator routines, as workspace and as special registers (stack pointer etc.).

• The private storage of the memory allocator, comprising free memory and whatever private datastructures the allocator module uses to keep track of what is free.

• The language heap, storing allocated pairs, closures and environments. We sometimes call this the 'cloud'.

• A linked list of allocation records comprising the call stack, each of which includes a local stack for expression evaluation.

The important pseudo-registers are

[Coerce] Γ ⊢ M : A A <: B Γ ⊢ M : B Figure 1.
Typing rules for PCFv

• s♣, pointing to the top of the current evaluation stack (a contiguous block of memory whose maximum depth is statically determinable, even for untyped code).

• ❡♥✈, pointing to the current environment, which is represented as a linked list of cons cells in the language heap.

• ✇❦, used as temporary workspace and to pass the block to be freed to the deallocator.

We now describe the code generated for some of the highlevel constructs in our language and explain the conventions and representations it uses. As an aid to understanding these descriptions, Figure 2 roughly illustrates part of a 'typical' memory layout, showing the four main regions. The dark blue gradient-filled cons cells are the ones that are part of environments; as we shall explain, these are initially allocated along with frames, but should be thought of as belonging to the language heap.

We should state explicitly at this point that there is no garbage collector, so compiled code will leak memory in the heap. We do, however, deallocate activation records when functions return.

Integer constants. To compile code for the integer constant n, we first increment the stack pointer and then store the value n on the new top of the stack: ❬s♣( ← ❬s♣(✰✶ ❬❬s♣(( ← ♥

In the figure, the integer 42 has been pushed and then another value (a closure) has been pushed on top of it.

Variables. Our source language represents variables by de Bruijn indices. So the code for a reference to variable n has to look up the n-th element of the environment and push it onto the top of the stack. The loop stepping through the linked list representing the environment is unrolled in place, like this: ❬s♣( ← ❬s♣(✰✶ ❬✇❦( ← ❬❡♥✈( ❬✇❦( ← ❬❬✇❦(✰✶( ✳✳✳ ♥ t✐♠❡s ✳✳✳ ❬✇❦( ← ❬❬✇❦(✰✶( ❬❬s♣(( ← ❬❬✇❦(( In the figure, the zeroth environment entry (the argument to the current function call) is a heap-allocated pair, the entry at position one is a recursive closure and that at position two is the same pair as at position zero.

Pairs. To construct a pair, we assume that elements of the pair have already been constructed on the top of the stack (in the 'wrong' order). We then need to call the allocator. We load the register arg with the size of the required block (here 2) put the return address •❛❜✰✹ into ret and jump to the allocation routine at address ❛••♦❝. On return to •❛❜✰✹, ret will point to a fresh block of two cells. We then (in a slightly optimized way) pop the top two elements from the stack, store them in the new block and push the address of that block: Closures To compile a lambda abstraction λx.M we compile, in the auxiliary code, the code for the body M , preceded by a header that allocates space for a new activation record and does bits of callee-saving, and followed by an epilogue that restores caller context and returns a value. Then in the main code, we build and push a closure value that pairs the current environment with a pointer to the wrapped body code.

•❛❜✿ ❬s♣( ← ❬s♣(✲✶ ❬❛r❣( ← ✷ ❬r❡t( ← •❛❜✰✹ •♠♣ ❛••♦❝ •❛❜✰✹✿
The function header expects an argument and a pointer to the closure being called to be on the top of the caller's stack. It allocates st❛❝❦❴s✐③❡✰✺ words for the new activation record, grabs the stored environment from the closure object and stores it at offset 1 in the new activation record. The argument is then popped from the caller's stack and stored at offset zero in the new activation record. The caller's environment is stored at offset 2, and his stack pointer at offset 3. We then set the environment pointer up for the body of the function by setting it to the base of the new activation record and set the stack pointer to offset 4 within the record. Note how the first element of the new environment list (the argument and the pointer to the rest of the environment) is contiguous with the remainder of the activation record. Here is the code:

•❛❜✿ ❬❛r❣( ← st❛❝❦❴s✐③❡ ✰ ✺ ❛••♦❝❛t❡ ❢r❛♠❡ ❬r❡t( ← •❛❜ ✰ ✸ •♠♣ ❛••♦❝ •❛❜✰✸✿ ❬✇❦( ← ❬❬s♣(( t❛❦❡ ❝•♦s✉r❡ ♣tr
❡♥t ✐♥ ❡♥✈ ❬❬r❡t(✰✷( ← ❬❡♥✈( st♦r❡ ❝❛••✐♥❣ ❡♥✈ ❬❬r❡t(✰✸( ← ❬s♣( st♦r❡ ❝❛••✐♥❣ s♣ ❬❡♥✈( ← ❬r❡t( s✇✐t❝❤ t♦ ♥❡✇ ❡♥✈ ❬s♣( ← ❬r❡t( ✰ ✹ s✇✐t❝❤ t♦ ♥❡✇ st❛❝❦
The saved environment and stack pointer can be seen in the figure as the two left-pointing arrows from the current frame to the parent frame. The head cell of the current environment is the darker pair of cells at the base of the current frame.

The function epilogue has the job of restoring the caller's environment and stack pointer, putting the value computed by the function on the caller's stack, deallocating the callee's frame and returning to the caller's code. The interesting points here are that we do not deallocate the first two elements of the frame that we originally allocated, as they are part of the environment and may by now be shared by other closures, and that the return address is stored at offset 4 in the caller's frame:

•❛❜✿ ❬✇❦( ← ❬❬s♣(( s❛✈❡ r❡t✉r♥ ✈❛•✉❡ ❬s♣( ← ❬❬❡♥✈(✰✸( r❡st♦r❡ ♦•❞ s♣ ❬❬s♣(( ← ❬✇❦( ♣✉s❤ r❡t✉r♥ ✈❛•✉❡ ❬✇❦( ← ❬❡♥✈( ✰✷ ❜❛s❡ t♦ ❢r❡❡ ❬❡♥✈( ← ❬❬❡♥✈(✰✷( r❡st♦r❡ ♦•❞ ❢r❛♠❡ ❬❛r❣( ← st❛❝❦❴s✐③❡✰✸ s✐③❡ t♦ ❢r❡❡ ❬r❡t( ← •❛❜ ✰ ✽ •♠♣ ❞❡❛••♦❝ •❛❜✰✽✿ •♠♣ ❬❬❡♥✈(✰✹( r❡t✉r♥ t♦ ❝❛••❡r
In the figure, one can see the return address to which we will jump when returning from the current call at offset 4 in the parent frame, pointing into the program. The code to actually build a closure allocates a new pair, fills in the first field with the code pointer to the appropriate function header and the second with the current environment, and pushes the address of the pair onto the stack.

Application. The code produced for an application assumes that there is an argument and a pointer to a closure on the stack. It stores a return address in the current frame and then branches to the code pointer part of the closure:

•❛❜✿ ❬❬❡♥✈(✰✹( ← •❛❜✰✸ ❬✇❦( ← ❬❬s♣(( •♠♣ ❬✇❦( •❛❜✰✸✿ ✳✳✳
Recursive closures. The compilation scheme for recursive function Fixf x = M relies on that non-recursive functions. We first extend the environment with an unfilled hole using the following code:

•❛❜✿ ❬❛r❣( ← ✷ ❬r❡t( ← •❛❜✰✸ •♠♣ ❛••♦❝ •❛❜✰✸✿ ❬❬r❡t(✰✶( ← ❬❡♥✈( ❬❡♥✈( ← ❬r❡t(
We then compile code to build the closure for λx.M in this environment, just as above. After that, we tie the recursive knot by overwriting the hole with the address of the constructed closure and finally restore the original environment:

❬❬❡♥✈(( ← ❬❬s♣(( ✴✴ ❦♥♦t ❬❡♥✈( ← ❬❬❡♥✈(✰✶( ✴✴ r❡st♦r❡
In the figure, the value on the top of the stack (and at position 1 in the environment) is a recursive closure. Observe that the environment part of the closure, the second component, points to the two element environment drawn within the cloud, and that the zeroth value in that environment is the closure itself.

Low-level Relations

As we said in the introduction, we specify low-level code in terms of binary relations, rather than the unary predicates that are more common in Hoare-style program logics. There are three main types of relation with which we work: over states, over natural numbers and over programs.

In defining relations over states, we will make much use of a form of separating conjunction, ⊗. Previously we worked with relations equipped with accessibility maps [START_REF] Benton | Relational reasoning in a nominal semantics for storage[END_REF], specifying the (state-varying) part of the state about which a particular relation cares (its support), and used disjointness of supports to define the separating conjunction. However, supported relations do not admit general notions of disjunction or existential quantification, which made some definitions in our previous work rather complex: we had to define combinators for special shapes of existentially quantified formula in which the satisfying witness was always uniquely determined. Furthermore, every inductive relation required separate inductive definitions for the relation and for its support and an inductive proof that the one supported the other, which was rather painful. In the current work, we have moved from supported relations over total states to working with relations over partial states (which is just the way everybody else working in separation logic does things). Our original motivation for eschewing partial states was that we did not wish to introduce any fictional notion of 'going wrong' into the operational semantics. We still manage to achieve that, however, by defining the operational semantics over total states (a special case of partial ones) and restricting attention to relations that are preserved by extension of partial states.

There is also an additive conjunction of relations, ×, which plays a larger role in giving the semantics to our functional language than was the case for an imperative one, because there are more potentially shared immutable runtime datastructures in the functional case.

We use various different relations over natural numbers, but the most interesting construction is the 'perp' operation (•) ⊤ , which takes a binary relation on states, R, and produces a relation over natural numbers R ⊤ . This is the way we specify code pointers: R ⊤ relates two natural numbers l and l ′ if for any states s and s ′ related by R, executing from l in initial state s and from l ′ in state s ′ yields equitermination: either both executions halt or both executions diverge. Equitermination is our basic notion of equivalence of observable behaviour, and all our program specifications will be in terms of equitermination when placed in related contexts.

Of course, we can only talk about whether or not jumping to a particular address in a particular state halts or not if we specify the program as well. For this reason, all our state relations and natural number relations are also parameterized by a pair of programs. Finally, to deal with recursion, we also index all our relations by natural number step-indices [START_REF] Appel | An indexed model of recursive types for foundational proof-carrying code[END_REF]. The intuition here is that if a relation represents a particular notion of equivalence, then its k-th approximant is 'indistinguishable within k steps'. Rather than manipulate natural numbers everywhere (as we did in our previous work), we now use a modal operator [START_REF] Appel | A very modal model of a modern, major, general type system[END_REF]) to tweak step-indices just where they matter. A further advantage of making this change is that we no longer build step manipulation into the definition of (•) ⊤ , which means that there is now a well-behaved Galois connection between relations on states and relations on natural numbers.

We now sketch the more formal definitions of the relations and relation constructors with which we use.

Relations on states and naturals DEFINITION 1 (State relation).

A relation in stateRel is a predicate over two partial states, two programs and a step index, satisfying a monotonicity condition with respect to decreasing indices and extension of partial states:

|❡❝♦r❞ st❛t❡|❡• ✿ ❚②♣❡ := ♠❦❙t❛t❡|❡• ④ R ✿❃ ♣st❛t❡ → ♣st❛t❡ → ♣r♦❣r❛♠ → ♣r♦❣r❛♠ → ♥❛t → Pr♦♣❀ st❛t❡|❡•❴❝♦♥❞ ✿ ∀ s1 s2 s ′ 1 s ′ 2 p1 p2 k1 k2✱ ✭R s1 s2 p1 p2 k1 ∧ s1 ⊂ s ′ 1 ∧ s2 ⊂ s ′ 2 ∧ k2 ≤ k1) → R s ′ 1 s ′ 2 p1 p2 k2 ⑥✳
where ♣st❛t❡ denotes partial functions from ♥❛t to ♥❛t and s ⊂ s ′ means inclusion of partial functions. stateRels are ordered by:

❉❡❢✐♥✐t✐♦♥ st❛t❡|❡•▲❡q ✭R R ′ ✿ st❛t❡|❡•✮ := ∀ s s ′ p p ′ k, R s s ′ p p ′ k → R ′ s s ′ p p ′ k✳
and we will write for this order.

Disjointness of partial states allows us to define a multiplicative tensor product, or separating conjunction, of relations [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF][START_REF] Yang | Relational separation logic[END_REF]), which we here give in mathematical notation: DEFINITION 2 (Separating conjunction). The separating conjunction R ⊗ R ′ of two relations in stateRel is the stateRel defined by

(R⊗R ′ ) s s ′ p p ′ k def ⇐⇒ ∃s1 s2 s ′ 1 s ′ 2 , s = s1#s2 ∧ s ′ = s ′ 1 #s ′ 2 ∧R s1 s ′ 1 p p ′ k ∧ R ′ s2 s ′ 2 p p ′ k where s = s1#s2
means that the domains of s1 and s2 are disjoint and that the union of s1 and s2 is equal to s. DEFINITION 3. An element of natRel is a relation between two natural numbers, two programs and a step index, satisfying a monotonicity condition:

|❡❝♦r❞ ♥❛t|❡• ✿ ❚②♣❡ := ♠❦◆❛t|❡• ④ R ✿❃ ♥❛t → ♥❛t → ♣r♦❣r❛♠ → ♣r♦❣r❛♠ → ♥❛t → Pr♦♣❀ ♥❛t|❡•❴❝♦♥❞ ✿ ∀ l l ′ p p ′ k1 k2, (R l l ′ p p ′ k1 ∧ k2 ≤ k1) → R l l ′ p p ′ k2 ⑥✳
and again there is a natural order:

❉❡❢✐♥✐t✐♦♥ ♥❛t|❡•▲❡q ✭r r ′ ✿ ♥❛t|❡•✮ := ∀ l l ′ p p ′ k, r l l ′ p p ′ k → r ′ l l ′ p p ′ k✳
We overload ❚♦♣ to mean the constantly total relation on both states and naturals. The following is a (non-exhaustive) list of some of the primitive stateRels we will combine with ⊗ to build specifications:

({n1, n2} → r) s s ′ p p ′ k def ⇐⇒ ∃l, l ′ s(n1) = l ∧ s ′ (n2) = l ′ ∧ r l l ′ p p ′ k (r ∈ natRel) ({n1, n2} → {m1, m2}) s s ′ p p ′ k def ⇐⇒ s(n1) = m1 ∧ s ′ (n2) = m2 n → {m1, m2} def = {n1, n2} → {m1, m2} (lif tP ) s s ′ p p ′ k def ⇐⇒ P (P : Pr♦♣) {n1, n2} → - def = {n1, n2} → Top ❇•♦❝❦ m n def = N 0≤i≤n-1 (m + i → -) (❚♦♣❢r♦♠ m m ′ ) s s ′ p p ′ k def ⇐⇒ ∀n n ′ , n ≥ m ⇒ n ′ ≥ m ′ ⇒ ({n, n ′ } → -)
The separating conjunction is crucial when we wish to make an update to the store whilst guaranteeing that certain other parts of the relation are not invalidated. However, we will also need to reason about the relatedness of closures, pairs and environments stored in the heap of our functional language, which are all allowed to share in unpredictable ways. To combine these specifications, we need a non-separating (Cartesian, additive) form of conjunction: DEFINITION 4 (Additive conjunction). The conjunction R ×R ′ of two relations in stateRel is the relation defined by

(R × R ′ ) s s ′ p p ′ k def ⇐⇒ R s s ′ p p ′ k ∧ R ′ s s ′ p p ′ k.
PROPOSITION 1. Viewing stateRel with the order as a category, ⊗ gives a symmetric monoidal structure and × a cartesian product. These are related by the distributive law:

(R × S) ⊗ T (R ⊗ T ) × (S ⊗ T ).

An adjunction with natRel

We relate relations on states and relations on code pointers via an adjunction between stateRel and natRel.

DEFINITION 5 (adjunction Perp ⊣ Perpnat). The two functors (order-reversing functions) Perp and Perpnat defined by

❉❡❢✐♥✐t✐♦♥ P❡r♣ ✭❙✿st❛t❡|❡•✮ := ❢✉♥ ♣ ♣✬ • •✬ ❦ ⇒ ∀ s s✬ •✱ ✭• ≤ ❦ ∧ ❙ s s✬ ♣ ♣✬ •✮ → ✭✭❦st❡♣t❡r♠ • ♣ s • → t❡r♠✐♥❛t❡s ♣✬ s✬ •✬✮ ∧ ✭❦st❡♣t❡r♠ • ♣✬ s✬ •✬ → t❡r♠✐♥❛t❡s ♣ s •✮✮✳ ❉❡❢✐♥✐t✐♦♥ P❡r♣❴♥❛t ✭▲✿♥❛t|❡•✮ := ❢✉♥ s s✬ ♣ ♣✬ ❦ ⇒ ∀ • •✬ •✱ ✭• ≤ ❦ ∧ ▲ ♣ ♣✬ • •✬ •✮ → ✭✭❦st❡♣t❡r♠ • ♣ s • → t❡r♠✐♥❛t❡s ♣✬ s✬ •✬✮ ∧ ✭❦st❡♣t❡r♠ • ♣✬ s✬ •✬ → t❡r♠✐♥❛t❡s ♣ s •✮✮✳ yield an adjunction (Galois connection): stateRel Perp $ $ ⊥ natRel op
Perp nat e e

In mathematical notation, we'll write R ⊤ for the image of the relation R by Perp. In our previous work, we defined P❡r♣ with a strict less than (<) relation on the step indices, which gave an operator without an adjoint, a point to which we will return later. DEFINITION 6 (judgement). We say two programs p and p ′ are equidivergent, or equiterminate under the relation R ∈ stateRel at points l and l ′ if they are in the relation R ⊤ for all indices:

|= p, p ′ l, l ′ : R ⊤ def = ∀k, R ⊤ l l ′ p p ′ k.
The above form of judgement is the one that we will use in specifying the relatedness of program fragments. Instead of saying that two programs are related if they map states satisfying a prerelation into states satisfying a postrelation, we specify and reason backwards, in a 'continuation-passing style', saying that two programs are related when if the exit points are equidivergent under the postrelation then the entry points are equidivergent under the prerelation.

EXAMPLE 1. For any two programs p and p ′ containing the following two instructions ❬✺( ← ❬✺( ✰ ✶ ❬❬✺(( ← ❬✵( at respective addresses l, l + 1 and l ′ , l ′ + 1, and for any R ∈ stateRel, if

|= p, p ′ l + 2, l ′ + 2 : ((0 → {28, 15}) ⊗ (5 → 13) ⊗ (13 → -) ⊗ R) ⊤ then |= p, p ′ l, l ′ : ((0 → {28, 15}) ⊗ (5 → 13) ⊗ (13 → {28, 15}) ⊗ R) ⊤
This is just the 'doubling up' of a very simple unary property, but it serves to illustrate a simple use of perping and the way in which we use quantification over separated relations to make frames explicit: we do not have a 'frame rule' like that of separation logic, but achieve much the same effect using second-order quantification.

Later, we'll see more interesting relational judgements involving non-trivial behavioural relationships between data and code pointers in the stores on the two sides. Note that specifications like this are 'partial', in that they are also satisfied by a pair of programs which always diverge (or indeed always halt) when started at the respective entry points. Relational reasoning is stronger regarding termination than traditional partial correctness in unary logics, since termination can be captured via equitermination with something that terminates, but the diagonal part of this kind of specification on code (i.e. which program fragments are related to themselves) does not rule out divergence.

Internalised quantification

We define stateRels quantified both universally and existentially over arbitrary Coq types in a straightforward higher-order style.

DEFINITION 7 (quantifiers). If X is a type and h : X → stateRel, define

(Ex h) s s ′ p p ′ k def ⇐⇒ ∃x, hx s s ′ p p ′ k (All h) s s ′ p p ′ k def ⇐⇒ ∀x, hx s s ′ p p ′ k

The modality and the Löb rule

So far, most of our constructions have essentially just passed step indices around. The reason they are there is to enable inductive reasoning about looping and recursion. Previously, we did this by making the index j strictly smaller than k in the definition of P❡r♣ and did explicit induction over indices to prove loops and recursion. Following the work of [START_REF] Appel | A very modal model of a modern, major, general type system[END_REF], we now abstract and encapsulate some of this reasoning in a modality , which satisfies a form of the 'Löb rule' (sometimes also called the Gödel-Löb axiom). This modal rule is given by α ⊢ α ⊢ α understood as "if α is valid assuming that α is valid in the future, then α is always valid". Reading 'in the future' as 'after the machine has taken at least one step', this yields an induction scheme that we can use to reason about recursion.

DEFINITION 8 ( modality). The modality ('later') is defined on elements r of natRel by

r l l ′ p p ′ k def ⇐⇒ ∃j < k, r l l ′ p p ′ j
The modality satisfies a lemma that is the essence of a continuation-passing version of the Löb rule:

LEMMA 1 (Löb rule). For all programs p and p ′ , all locations ptr, ptr ′ , all program points l and l ′ , and all stateRels R, the following rule is sound:

|= p, p ′ l, l ′ : ((ptr, ptr ′ → ((ptr, ptr ′ → l, l ′ ) ⊗ R) ⊤ ) ⊗ R) ⊤ |= p, p ′ l, l ′ : ((ptr, ptr ′ → l, l ′ ) ⊗ R) ⊤

Specifications and Verifications

In this section we explain the specifications for compiled code and for the memory allocation module on which compiled code relies.

Allocator specification

Code produced by the compiler expects to be linked with a memory allocation module, which it uses to allocate and deallocate activation records and to allocate data structures in the heap. The reasoning is properly modular: we have an independent specification of the allocator to which the specification of compiled code refers, and we independently verify the output of the compiler and particular allocator implementations. The specification of the allocator is essentially the same as in our previous work, but with a slight twist relating to termination.

We have said that we generally use specifications that do not rule out divergence. This works for interpreting types of our highlevel language, since those all include divergent programs. However, were we to try to prove that two different low-level program fragments (e.g. the compilation of two different source expressions) were in the relation associated with a type, relying only on an allocator specification that allows divergence, there would be a problem: if the two fragments make different calls to the allocator, then we would not be able to prove that the programs equiterminate. So we have slightly modified the allocator specification of our earlier work to ensure totality. DEFINITION 9 (total judgment). We define when two programs p and p' satisfy t♦t❛•❴•✉❞❣♠❡♥t Rpre Rpost p p ′ l0 l ′ 0 for program points l0 and l ′ 0 , Rpre : ♥❛t → ♥❛t → stateRel and Rpost :

stateRel thus t♦t❛•❴•✉❞❣♠❡♥t Rpre Rpost p p ′ l0 l ′ 0 def ⇐⇒ ∀l1 l ′ 1 k s0 s ′ 0 , (Rprel1l ′ 1 ) s0 s ′ 0 p p ′ k ⇒ ∃j1 j ′ 1 s1 s ′ 1 , ❦st❡♣r❡❞✉❝❡ j1 p s0 s1 l0 l1 ∧ ❦st❡♣r❡❞✉❝❡ j ′ 1 p ′ s ′ 0 s ′ 1 l ′ 0 l ′ 1 ∧ Rpost s1 s ′ 1 p p ′ k
where ❦st❡♣r❡❞✉❝❡ j1 p s0 s1 l0 l1 means that the program p takes j1 steps from the configuration s0, p, l0 to the configuration s1, p, l1 .

Note that total judgements are more like those of traditional Hoare logics, and that this is less behavioural (i.e. more intensional) than our other form of specification: the relation Rpre is explicitly parameterized by the return addresses, so we are asserting that particular program counters will be reached.

We now define the prerelations and postrelations used in the specs of the three entry points of the allocator, initialization, allocation and deallocation. Each of these is parameterized by a relation Ra which will be a private invariant relating two different, equivalent, allocators. Ra will be existentially quantified (i.e. made abstract) on the outside of the whole module. Each of the other parameters will be universally quantified over the total judgement for that particular entry point. 1The parameterized relations |Pr❡❴✐♥✐t and |P♦st❴✐♥✐t for the initialization routine of the allocator are given by

❉❡❢✐♥✐t✐♦♥ |Pr❡❴✐♥✐t ✭Ra✿st❛t❡|❡•✮ ✭n5 n ′ 5 n6 n ′ 6 • •✬ ✿ ♥❛t✮ := ✭r❡t → •✱•✬✮ ⊗ ✭s♣ → n5✱n ′ 5 ✮ ⊗ ✭❡♥✈ → n6✱n ′ 6 ✮ ⊗ ❚♦♣❢r♦♠ ✶✵ ✶✵✳ ❉❡❢✐♥✐t✐♦♥ |P♦st❴✐♥✐t ✭Ra✿st❛t❡|❡•✮ ✭n5 n ′ 5 n6 n ′ 6 ✿ ♥❛t✮ := Ra ⊗ ✭r❡t → -✮ ⊗ ✭s♣ → n5, n ′ 5 ✮ ⊗ ✭❡♥✈ → n6, n ′ 6 ✮✳ ❉❡❢✐♥✐t✐♦♥ t♦t❛•❴✐♥✐t |❛ ♣ ♣✬ ✐♥✐t ✐♥✐t✬ ✿❂ ❢♦r❛•• ♥✺ ♥✬✺ ♥✻ ♥✬✻✱ t♦t❛•❴•✉❞❣♠❡♥t ✭|Pr❡❴✐♥✐t |❛ ♥✺ ♥✬✺ ♥✻ ♥✬✻✮ ✭|P♦st❴✐♥✐t |❛ ♥✺ ♥✬✺ ♥✻ ♥✬✻✮ ♣ ♣✬ ✐♥✐t ✐♥✐t✬✳
The intuition here is that if one calls the initialization routines of two related allocators, passing return addresses l and l ′ , and with the values n5 and n ′ 5 in the pseudo-register sp on the two sides, and n6 and n ′ 6 in env, then the two sides will each take some number of steps to reach l and l ′ in two states in which the invariant Ra has been established, the original values in sp and env have been preserved and nothing is guaranteed about the contents of ret.

The parameterized relations |Pr❡❴❛••♦❝ and |P♦st❴❛••♦❝ for the allocation routine are given by

❉❡❢✐♥✐t✐♦♥ |Pr❡❴❛••♦❝ ✭Ra Rc✿st❛t❡|❡•✮ ✭♥ ♥✬ n5 n ′ 5 n6 n ′ 6 • •✬✿ ♥❛t✮ := ✭r❡t → •✱•✬✮ ⊗ Ra ⊗ Rc ⊗ ✭❛r❣ → ♥✱♥✬✮ ⊗ ✭s♣ → n5, n ′ 5 ✮ ⊗ ✭❡♥✈ → n6, n ′ 6 ✮✳ ❉❡❢✐♥✐t✐♦♥ |P♦st❴❛••♦❝ ✭Ra Rc✿st❛t❡|❡•✮ ✭♥ ♥✬ n5 n ′ 5 n6 n ′ 6 ✿ ♥❛t✮ := ✭❊① ❢❜✱❊① ❢❜✬✱✭✭r❡t → ❢❜✱❢❜✬✮ ⊗ ✭❇•♦❝❦ ❢❜ ❢❜✬ ♥ ♥✬✮✮✮ ⊗ Ra ⊗ Rc ⊗ ✭❛r❣ → -✮ ⊗ ✭s♣ → n5, n ′ 5 ✮ ⊗ ✭❡♥✈ → n6, n ′ 6 ✮✳ ❉❡❢✐♥✐t✐♦♥ t♦t❛•❴❛••♦❝ |❛ ♣ ♣✬ ❛••♦❝ ❛••♦❝✬ ✿❂ ❢♦r❛•• |❝ ♥ ♥✬ ♥✺ ♥✬✺ ♥✻ ♥✬✻✱ t♦t❛•❴•✉❞❣♠❡♥t ✭|Pr❡❴❛••♦❝ |❛ |❝ ♥ ♥✬ ♥✺ ♥✬✺ ♥✻ ♥✬✻✮ ✭|P♦st❴❛••♦❝ |❛ |❝ ♥ ♥✬ ♥✺ ♥✬✺ ♥✻ ♥✬✻✮ ♣ ♣✬ ❛••♦❝ ❛••♦❝✬✳
❉❡❢✐♥✐t✐♦♥ |Pr❡❴❞❡❛••♦❝ ✭Ra Rc✿st❛t❡|❡•✮ ✭❢❜ ❢❜✬ ♥ ♥✬ n5 n ′ 5 n6 n ′ 6 • •✬✿ ♥❛t✮ := ✭r❡t → •✱•✬✮ ⊗ ✭❛r❣ → ♥✱♥✬✮ ⊗ ✭✇❦ → ❢❜✱❢❜✬✮ ⊗ ❇•♦❝❦ ❢❜ ❢❜✬ ♥ ♥✬ ⊗ Ra ⊗ Rc ⊗ ✭s♣ → n5, n ′ 5 ✮ ⊗ ✭❡♥✈ → n6, n ′ 6 ✮✳ ❉❡❢✐♥✐t✐♦♥ |P♦st❴❞❡❛••♦❝ ✭Ra Rc✿st❛t❡|❡•✮ ✭n5 n ′ 5 n6 n ′ 6 ✿ ♥❛t✮ := ✭r❡t → -✮ ⊗ ✭❛r❣ → -✮ ⊗ ✭✇❦ → -✮ ⊗ Ra ⊗ Rc ⊗ ✭s♣ → n5, n ′ 5 ✮ ⊗ ✭❡♥✈ → n6, n ′ 6 ✮✳ ❉❡❢✐♥✐t✐♦♥ t♦t❛•❴❞❡❛••♦❝ |❛ ♣ ♣✬ ❞❡❛••♦❝ ❞❡❛••♦❝✬✿❂ ❢♦r❛•• |❝ ❢❜ ❢❜✬ ♥ ♥✬ ♥✺ ♥✬✺ ♥✻ ♥✬✻✱ t♦t❛•❴•✉❞❣♠❡♥t ✭|Pr❡❴❞❡❛••♦❝ |❛ |❝ ❢❜ ❢❜✬ ♥ ♥✬ ♥✺ ♥✬✺ ♥✻ ♥✬✻✮ ✭|P♦st❴❞❡❛••♦❝ |❛ |❝ ♥✺ ♥✬✺ ♥✻ ♥✬✻✮ ♣ ♣✬ ❞❡❛••♦❝ ❞❡❛••♦❝✬✳
Here the precondition is that there are blocks of memory of the appropriate sizes and disjoint from Ra, Rc and the registers on the two sides. The postcondition just says that Ra, Rc still hold and that the values in sp and env are preserved. The relation between programs p and p ′ that says that they have allocator modules related by Ra with entry points ✐♥✐t, ❛

••♦❝ and ❞❡❛••♦❝ and ✐♥✐t✬, ❛••♦❝✬ and ❞❡❛••♦❝✬ is then just ❉❡❢✐♥✐t✐♦♥ ❆••♦❝❙♣❡❝ ♣ ♣✬ |❛ ✐♥✐t ✐♥✐t✬ ❛••♦❝ ❛••♦❝✬ ❞❡❛••♦❝ ❞❡❛••♦❝✬ ✿❂ ✭t♦t❛•❴✐♥✐t |❛ ♣ ♣✬ ✐♥✐t ✐♥✐t✬✮ ∧ ✭t♦t❛•❴❛••♦❝ |❛ ♣ ♣✬ ❛••♦❝ ❛••♦❝✬✮ ∧ ✭t♦t❛•❴❞❡❛••♦❝ |❛ ♣ ♣✬ ❞❡❛••♦❝ ❞❡❛••♦❝✬✮✳

Semantics of types

We can now define the low-level specifications corresponding to our high-level types. The basic idea is that for each source type A, we define A : nat → nat → stateRel such that A l l ′ relates pairs of states in which l and l ′ can be interpreted as pointing to equivalent values of type A. Since our values include closures, the dependency of stateRels on the programs really gets used, as we will need to say that the values in the heap involve code pointers with certain behaviours. Using this notion of equivalent values in the state, we define when states contain equivalent environments and evaluation stacks of particular types. Finally, we specify compiled code fragments in terms of equitermination when started in sufficiently equivalent states, and linked with sufficiently equivalence-respecting continuations.

The inductive definition of s❡♠❛♥t✐❝s❴♦❢❴t②♣❡s is shown in Figure 3. Although this looks complex, it really amounts to a fairly familiar logical relational interpretation of types, but recast in a lower-level setting that naturally introduces more details.

The first clause says that two values ptr and ptr ′ are equal when considered at type ■♥t P when they are equal natural numbers and also satisfy the predicate P , just as one would expect. The second clause says that they are equal at ❇♦♦• P when they both represent the same boolean value according to our chosen representation of booleans (♥✷❜ maps zero to false and successors to true), and that boolean satisfies the predicate P .

The third clause says ptr and ptr ′ represent equivalent values of type A×B in respective stores s and s ′ just when ptr is the address of two consecutive cells in s with contents value and value2, ptr ′ is the address of a pair of cells holding value ′ and value ′ 2 in the state s ′ , value and value ′ are equivalent values of type B, and value2 and value ′ 2 are equivalent values of type A. So values are related at a product type if they are both pairs and their components are related pointwise.

The real work is in the fourth clause, which says what it means for values to be related at a function type. A functional value will contain some code, to which we will jump when we apply the function. So relatedness of functional values is a constraint on the behaviour of that code in certain contexts. The first thing to observe is that part of that contract will be that the code is allowed to assume that the allocator has been initialized, and must promise to maintain the allocator's private invariant -that explains why the definition of the semantics of types is parameterized by the allocator's private invariant Ra. The second thing to note is that all the functional values that are constructed by code produced by our compiler will be closures: pairs of a code pointer and an environment. But recall that we are trying to come up with maximally permissive extensional specifications, that will be satisfied by any code that behaves like a function when we apply it. So we certainly do not want to require that functions have environments containing values of some (even hidden) source language types. In fact, our calling convention does not even require that there is an environment at all -the function code gets passed a pointer to the function object itself, from which it can recover an environment if it has one, but the caller does not know anything about environments. So from an external point of view, the specification of what it means for ptr and ptr ′ to be related elements of A → B is just that there exists some private invariant relation Rprivate such that ptr and ptr ′ point to code pointers that behave in a certain way and Rprivate actually holds now (so the functions are set up and ready to call). In the case of code produced by the compiler, that private invariant will get instantiated with assertions about the environment part of closures. Note that we have used the additive conjunction, so the private invariant is allowed to overlap/involve the memory locations ptr and ptr ′ themselves; this will actually happen when there is (direct or indirect) recursion.

So what are the details of the 'certain way' in which code of equivalent functions must behave? Firstly, this is where we use the 'later' modality discussed earlier, on which we rely when showing that the code produced for recursive functions satisfies the specification. The operational intuition is that for functions to be indistinguishable for k steps, it suffices for their bodies to be indistinguishable for k -1 steps, as testing them (i.e. applying them) involves jumping to them, which takes a step. Underneath the modality, the specification is a perp, a requirement that the two code pointers will equiterminate whenever they are jumped to in states related by the precondition Pr❡❴❛rr♦✇, which is parameterized by the private invariant, the two function values themselves, the invariant of the allocator and the semantics of the types A and B. At the risk of labouring the point, note that we pass in the semantic objects here, not the syntactic types, so the arrow construction works over arbitrary (appropriately parameterized) relations.

The precondition Pr❡❴❛rr♦✇ says under what conditions the entry points of the two functions have to promise to behave equivalently for them to be regarded as representing equal functions. We are essentially translating a CPS transformed version of the standard logical relations definition, that functions are related when they take related arguments to related results. So Pr❡❴❛rr♦✇ relates two states just when they represent calls to the two functions with A -related arguments and B ⊤ -related continuations. The tops of the two stacks are expected to point to the original function objects (from which they can get to any local state, usually an environment, they might need). Below that on the stacks are two arguments, ptr_arg and ptr_arg ′ which are themselves equivalent according to A . The allocator invariant Ra is assumed to hold, disjoint from everything else. The environment registers point to

❋✐①♣♦✐♥t s❡♠❛♥t✐❝s❴♦❢❴t②♣❡s ✭t✿❊①♣❚②♣❡✮ ✭|❛✿st❛t❡|❡•✮ ♣tr ♣tr✬ str✉❝t t ✿❂ ♠❛t❝❤ t ✇✐t❤ ⑤ ■♥t P ⇒ •✐❢t ✭P ♣tr ∧ ✭♣tr ❂ ♣tr✬✮✮ ⑤ ❇♦♦• P ⇒ •✐❢t ✭P ✭♥✷❜ ♣tr✮ ∧ ✭♥✷❜ ♣tr ❂ ♥✷❜ ♣tr✬✮✮ ⑤ ❛ * ❜ ⇒ ❊① ✈❛•✉❡✱ ❊① ✈❛•✉❡✷✱ ❊① ✈❛•✉❡✬✱ ❊① ✈❛•✉❡✷✬✱ ✭♣tr✱♣tr✬ →✈❛•✉❡✱✈❛•✉❡✬✮ × ✭♣tr✰✶✱♣tr✬✰✶ →✈❛•✉❡✷✱✈❛•✉❡✷✬✮ × ❜ |❛ ✈❛•✉❡ ✈❛•✉❡✬ × ❛ |❛ ✈❛•✉❡✷ ✈❛•✉❡✷✬✮ ⑤ ❛ -→ ❜ ⇒ ❊① |♣r✐✈❛t❡✱ ✭♣tr✱♣tr✬ → ▲❛t❡r ✭ P❡r♣ ✭Pr❡❴❛rr♦✇ |♣r✐✈❛t❡ ♣tr ♣tr✬ |❛ ✭ ❛ ✮ ✭ ❜ ✮✮✮ × |♣r✐✈❛t❡✮ ❡♥❞ ✇❤❡r❡ ✧✬ ✬ t ✬ ✬✧ ✿❂ ✭s❡♠❛♥t✐❝s❴♦❢❴t②♣❡s t ✮✳ ❉❡❢✐♥✐t✐♦♥ P♦st❴❛rr♦✇ ❜ ✭|❛ |❝✿ st❛t❡|❡•✮ |❝❴❝•♦✉❞ ✭♥ ♥✬ st❛❝❦❴♣tr st❛❝❦❴♣tr✬✿ ♥❛t✮✿❂ ❊① ♣tr❴r❡s✉•t✱ ❊① ♣tr❴r❡s✉•t✬✱ ✭st❛❝❦❴♣tr✱st❛❝❦❴♣tr✬ → ♣tr❴r❡s✉•t✱♣tr❴r❡s✉•t✬✮ ⊗ ✭st❛❝❦❴♣tr✰✶✱st❛❝❦❴♣tr✬✰✶ →✲✮ ⊗ ✭✭❜ |❛ ♣tr❴r❡s✉•t ♣tr❴r❡s✉•t✬✮ × |❝❴❝•♦✉❞✮ ⊗ ✭✇♦r❦r❡❣ → ✲✮ ⊗ ✭❛r❣r❡❣ → ✲✮ ⊗ ✭r❡tr❡❣ → ✲✮ ⊗ |❛ ⊗ |❝ ⊗ ✭✸ →✲✮ ⊗ ✭✹ →✲✮ ⊗ ✭s♣r❡❣ → st❛❝❦❴♣tr✱st❛❝❦❴♣tr✬✮ ⊗ ✭❡♥✈r❡❣ → ♥✱♥✬✮ ⊗ ✉♥✉s❡❞❴s♣❛❝❡✳ ❉❡❢✐♥✐t✐♦♥ Pr❡❴❛rr♦✇ |❴♣r✐✈❛t❡ ♣tr❴❢✉♥❝t✐♦♥ ♣tr❴❢✉♥❝t✐♦♥✬ |❛ ❛ ❜✿❂ ❊① |❝✱ ❊① |❝❴❝•♦✉❞✱ ❊① ♥✱ ❊① ♥✬✱ ❊① ♣tr❴❛r❣✱ ❊① ♣tr❴❛r❣✬✱ ❊① st❛❝❦❴♣tr✱ ❊① st❛❝❦❴♣tr✬✱ ✭st❛❝❦❴♣tr✱st❛❝❦❴♣tr✬ → ♣tr❴❛r❣✱♣tr❴❛r❣✬✮ ⊗ ✭st❛❝❦❴♣tr✰✶✱st❛❝❦❴♣tr✬✰✶ → ♣tr❴❢✉♥❝t✐♦♥✱♣tr❴❢✉♥❝t✐♦♥✬✮ ⊗ ✭|❴♣r✐✈❛t❡ × ❛ |❛ ♣tr❴❛r❣ ♣tr❴❛r❣✬ × |❝❴❝•♦✉❞✮ ⊗ ✭✭♥✰✹✱♥✬✰✹ → ▲❛t❡r ✭P❡r♣ ✭P♦st❴❛rr♦✇ ❜ |❛ |❝ |❝❴❝•♦✉❞ ♥ ♥✬ st❛❝❦❴♣tr st❛❝❦❴♣tr✬✮✮✮ × |❝✮ ⊗ ✭✇♦r❦r❡❣ → ✲✮ ⊗ ✭❛r❣r❡❣ → ✲✮ ⊗ ✭r❡tr❡❣ → ✲✮ ⊗ |❛ ⊗ ✭✸ → ✲✮ ⊗ ✭✹ → ✲✮ ⊗ ✭s♣r❡❣ → st❛❝❦❴♣tr✰✶✱st❛❝❦❴♣tr✬✰✶✮ ⊗ ✭❡♥✈r❡❣ → ♥✱♥✬✮ ⊗ ✉♥✉s❡❞❴s♣❛❝❡✳ Figure 3
. Relational semantics of types the callers' stack frames, each of which contains a return address at offset 4. The entry point can also assume that the private invariant Rprivate, relating the two functions' private storage, holds at entry. In general, this invariant will be over the language heap, which contains immutable values with unspecified sharing between them, including the representation of the argument value if that is of non-primitive type. These assumptions about the language heap are captured by an additive, non separating, conjunction of Rprivate, the A -relatedness of the argument and some unknown further assumptions Rc_cloud on which the continuation may be depending. There is also an unknown invariant Rc that holds over state disjoint from the language heap, the allocators state and the pseudo registers, but which may share with the return address slot of the callers' frames. This Rc will typically be instantiated with assumptions about the linked list of activation records comprising the call stack -note again that we do not explicitly model such a list-like structure at all, as each individual function call can just treat it as abstract.

The specifications for the two related return addresses, stored in the callers' frames, are once again modalized perped formulae, asking that those two return addresses behave equivalently whenever they are returned to with states that are appropriately related according to conditions that are made precise in the definition of P♦st❴❛rr♦✇. The return addresses can assume that the stack pointers point to equivalent returned values according to B and that the local frame invariant Rc_cloud from the precondition has been preserved, sharing storage with the return value. They can also assume that the allocators' private invariant has been maintained and that the frame condition on the rest of the state, Rc, has been preserved. The environments will have been put back to what they were before the call (the preservation of n and n ′ ) and the stack pointer will be one less than it was before the call (because we have popped the argument and the function object and pushed a return value).

The above specification of type-dependent relatedness of values in the heap of the machine is a stepping stone on our way to writing specifications for computations. The actual programs that manipulate and generate values are the things we ultimately want to verify. Given a context Γ and a type A, we need to define a specification for low-level programs that corresponds to producing equal results of type A when started in equal contexts of type Γ. The definition of equal contexts of type Γ is the stateRel that says there are two linked lists (starting at particular locations) with elements that are pairwise related by the interpretation of the corresponding type in Γ. This is a fairly straightforward induction over Γ, using the semantics of types defined above:

❋✐①♣♦✐♥t s❡♠❛♥t✐❝s❴♦❢❴❡♥✈ ✭❡♥✈✿❊♥✈❚②♣❡✮ |❛ ❝✉rr❡♥t ❝✉rr❡♥t✬ str✉❝t ❡♥✈ ✿❂ ♠❛t❝❤ ❡♥✈ ✇✐t❤ ⑤ ♥✐• ⇒ ❚♦♣ ⑤ ❤ ✿✿ t ⇒ ❊① ♣tr✱ ❊① ♣tr✬✱ ❊① ♥❡①t✱ ❊① ♥❡①t✬✱ ✭✭❝✉rr❡♥t✱❝✉rr❡♥t✬ → ♣tr✱♣tr✬✮ × ✭❝✉rr❡♥t✰✶✱❝✉rr❡♥t✬✰✶ → ♥❡①t✱♥❡①t✬✮ × ❤ |❛ ♣tr ♣tr✬ × t |❛ ♥❡①t ♥❡①t✬✮ ❡♥❞ ✇❤❡r❡ ✧✬ ✬ ❡♥✈ ✬ ✬✧ ✿❂ ✭s❡♠❛♥t✐❝s❴♦❢❴❡♥✈ ❡♥✈✮✳
Note that we have used the additive conjunction again here, so elements of the environment can share heap storage with one another. Environments do not have to be terminated and are even allowed to be cyclic (directly through the link structure, or indirectly through closure values).

Compiled expressions also make use of a local evaluation stack (not to be confused with the call stack of activation records). This is separate from the language heap (cloud) and gets read and written as values are pushed and popped. The values on the stack, however, will generally be related by relations that involve the cloud and can overlap. To specify relatedness of stacks we therefore define a 'fold' operation that relates states in which there are particular sequences of values in consecutive memory locations and disjoint regions of memory in which an additive conjunction of relations, indexed by the values in the sequences, holds.2

❉❡❢✐♥✐t✐♦♥ •st❛❝❦❴t②♣❡ ✿❂ •✐st ✭✭♥❛t → ♥❛t → st❛t❡|❡•✮ ✯ ✭♥❛t ✯ ♥❛t✮✮✳ ❋✐①♣♦✐♥t st❛❝❦❴❞❡s❝r✐♣t✐♦♥ ✭st❛❝❦❴•✐st✿•st❛❝❦❴t②♣❡✮ ♣tr ♣tr✬ ❝•♦✉❞r❡• str✉❝t st❛❝❦❴•✐st ✿❂ ♠❛t❝❤ st❛❝❦❴•✐st ✇✐t❤ ⑤ ♥✐• ⇒ ❝•♦✉❞r❡• ⑤ ♣❛✐r ❤ ✭♣❛✐r ♣tr❴❤ ♣tr❴❤✬✮ ✿✿ t ⇒ ✭♣tr✱♣tr✬ → ♣tr❴❤✱♣tr❴❤✬✮ ⊗ st❛❝❦❴❞❡s❝r✐♣t✐♦♥ t ✭♣tr✲✶✮ ✭♣tr✬✲✶✮ ✭✭❤ ♣tr❴❤ ♣tr❴❤✬✮ × ❝•♦✉❞r❡•✮ ❡♥❞✳
We then package up a description of entire related memory configurations like this:

❉❡❢✐♥✐t✐♦♥ ♠❡♠♦r②❴s♣❡❝✐❢✐❝❛t✐♦♥ |❛ |❝ |❝❴❝•♦✉❞ ❡♥✈ st❛❝❦❴•✐st st❛❝❦❴❢r❡❡ st❛❝❦❴❢r❡❡✬ st❛❝❦❴♣tr st❛❝❦❴♣tr✬ ♥ ♥✷ ♥✸ ♥✬ ♥✷✬ ♥✸✬✿❂ ✭s♣r❡❣ →st❛❝❦❴♣tr✱st❛❝❦❴♣tr✬✮ ⊗ ❇•♦❝❦ ✭st❛❝❦❴♣tr✰✶✮ ✭st❛❝❦❴♣tr✬✰✶✮ st❛❝❦❴❢r❡❡ st❛❝❦❴❢r❡❡✬ ⊗ ✭❡♥✈r❡❣ → ♥✱♥✬✮ ⊗ st♦r✐♥❣❴s♣❛❝❡ ♥ ♥✷ ♥✸ ♥✬ ♥✷✬ ♥✸✬ ⊗ st❛❝❦❴❞❡s❝r✐♣t✐♦♥ st❛❝❦❴•✐st st❛❝❦❴♣tr st❛❝❦❴♣tr✬ ✭ ❡♥✈ |❛ ♥ ♥✬ × |❝❴❝•♦✉❞✮ ⊗ ✭✇♦r❦r❡❣ → ✲✮ ⊗ ✭❛r❣r❡❣ → ✲✮ ⊗ ✭r❡tr❡❣ → ✲✮ ⊗ |❛ ⊗ |❝ ⊗ ✭✸ →✲✮ ⊗ ✭✹ →✲✮ ⊗ ✉♥✉s❡❞❴s♣❛❝❡✳
which relates two states when the 'active' parts of the stack are related according to st❛❝❦❴•✐st, there is a Block of unused stack slots above that, the environments on the two sides are related according to the interpretation of the type environment ❡♥✈ (with appropriate sharing), the allocator invariant Ra holds and an invariant Rc holds on the rest of the state. The relation st♦r✐♥❣❴s♣❛❝❡ describes the contents of the callee-saves slots in the current activation record, we also specify that the various registers point to arbitrary values.

Type Soundness

We are finally in a position to state our main result, that the compiler produces code that respects our relational interpretation of types. The theorem as stated in Coq is given in Figure 4. Although the statement looks rather complex, what it really says is not too hard to understand. The functions we have not defined, such as ❡①tr❛❝t❴❝♦❞❡❴❢r♦♠❴❣•♦❜❛•❝♦❞❡, just project components from the result of compilation. We start with a source level expression ❡ which has type ❛ in source-level type environment ❡♥✈. We compile ❡ twice, once starting from the location st❛rt and linking against allocation and deallocation routines at addresses ❛••♦❝ and ❞❡❛••♦❝, and once starting at st❛rt✬ linking against ❛••♦❝✬ and ❞❡❛••♦❝✬.

Then for any complete program ♣ that extends the main and auxiliary code produced by the first compilation, and for any ♣✬ that extends the code produced by the second compilation, if ♣ and ♣✬ have |❛-related memory allocation routines at the entry points we used in the respective compilations, then we get the result about the relatedness of the behaviour of the two bits of compiled code.

The judgement about the compiled code says that executing from program counter st❛rt in program ♣ and from program counter st❛rt✬ in program ♣✬ yields equitermination provided that (a) the two initial states are related by a memory specification corresponding to the type environment ❡♥✈, together with some arbitrary other bits, and (b) the labels after the code compiled from ❡ on the two sides always equiterminate when they are started in states that are related by the same memory specification that we assumed at the entry points, modified to add A -related values on top of the evaluation stack (with appropriate modifications to both the stack pointers and the size of the unused stack locations).

So what does that tell us? One consequence is about the behaviour of closed programs of ground type, such as ■♥t P. The theorem says that if you compile such a program and link it against a well-behaved allocator then it will either always diverge or produce the same ground value, which will moreover satisfy the predicate refinement P. The observable behaviour will not change according to what locations are returned by the allocator, what the initial contents of any bits of memory are, where we initially put the stack, or anything else it should not depend upon. Moreover, the computation will not write to any areas of memory that it should not (because of the preservation of an arbitrary |❝).

More importantly, the specification is entirely modular and semantic. The proof obligations for writing non-standard implementations of higher-order functions that are extensionally indistinguishable from (and so can interoperate with) those produced by our compiler, yet might be implemented quite differently, are made explicit and could be verified without the compiler source.

Remarks on the Coq formalization

Our Coq formalization covers everything discussed here: the low level machine, high level language, the compiler, two allocator modules, the general relational reasoning framework, the specifications and the proof of semantic type preservation. (The famous Knuth quote "Beware of bugs in the above code; I have only proved it correct, not tried it." almost applies, though we have compiled and executed just a few simple programs within Coq and obtained the right answers.)

The entire development is around 14000 lines and relies heavily on our previous work, though few things have been left completely unchanged. The code for the memory allocators is the same, but moving to relations over partial states instead of using accessibility maps and changing the treatment of step indices have meant small changes throughout. In general, the proof assistant helps rather than hinders such evolution -one can change basic definitions and then update the scripts so that proofs of basic properties still go through surprisingly quickly and sometimes almost automatically.

We make heavy use of Setoid rewriting modulo the preorder , but have replace our earlier handcrafted reflective tactics for reorganising long sequences of ⊗-ed stateRels modulo associativity and commutativity with uses of the library-provided r✐♥❣ tactic. This removes the two-level (syntactic and semantic) structure of our explicitly reflective approach which we were never sufficiently disciplined to use cleanly before.

The proofs also make rather more use of specialized tactics than our earlier ones, and we have overall managed to keep the size of this formulation about the same as that of our previous one, for a simple imperative language with no procedures, despite the fact that the specifications and proofs here are much more complex and the compiler is considerably larger.

The general pattern of reasoning is, as in our earlier work, forward Hoare style proving, using rules for entailments on stateRels and judgements to set the goal up in the right form to apply instruction-specific lemmas such as the following, for an unconditional indirect branch: LEMMA 2 (Branch). For all p, p ′ , l, l ′ , m and R, if

p(l) = •♠♣ ❬♠(, p ′ (l ′ ) = •♠♣ ❬♠( ❚❤❡♦r❡♠ ❝♦♠♣✐•❡r❴s♦✉♥❞ ✿ ❢♦r❛•• ❜❛s❡ ❜❛s❡✬ |❛ ✐♥✐t ✐♥✐t✬ ❛••♦❝ ❛••♦❝✬ ❞❡❛••♦❝ ❞❡❛••♦❝✬ Γ ❛ ❡ ✭t✿Γ ⊢ ❡ ✿ ❛✮ |❝ |❝❴❝•♦✉❞ st❛rt st❛rt✬ st❛❝❦❴♣tr st❛❝❦❴♣tr✬ ♥ ♥✷ ♥✸ ♥✬ ♥✷✬ ♥✸✬ ♣ ♣✬ st❛❝❦❴•✐st✱ •❡t ❣•♦❜❛•❴❝♦❞❡ ✿❂ ❝♦♠♣✐•❡ ❡ ♥✐• ❜❛s❡ ❛••♦❝ ❞❡❛••♦❝ ✐♥ •❡t ❝♦❞❡ ✿❂ ❡①tr❛❝t❴❝♦❞❡❴❢r♦♠❴❣•♦❜❛•❝♦❞❡ ❣•♦❜❛•❴❝♦❞❡ st❛rt ✐♥ •❡t st❛❝❦❴❢r❡❡ ✿❂ ❡①tr❛❝t❴st❛❝❦s✐③❡❴❢r♦♠❴❝♦❞❡ ❝♦❞❡ ✐♥ •❡t ❣•♦❜❛•❴❝♦❞❡✬ ✿❂ ❝♦♠♣✐•❡ ❡ ♥✐• ❜❛s❡✬ ❛••♦❝✬ ❞❡❛••♦❝✬ ✐♥ •❡t ❝♦❞❡✬ ✿❂ ❡①tr❛❝t❴❝♦❞❡❴❢r♦♠❴❣•♦❜❛•❝♦❞❡ ❣•♦❜❛•❴❝♦❞❡✬ st❛rt✬ ✐♥ •❡t st❛❝❦❴❢r❡❡✬ ✿❂ ❡①tr❛❝t❴st❛❝❦s✐③❡❴❢r♦♠❴❝♦❞❡ ❝♦❞❡✬ ✐♥ ♣r♦❣❴❡①t❡♥❞s❴❛✉①❝♦❞❡ ❣•♦❜❛•❴❝♦❞❡ ♣ ❜❛s❡ → ♣r♦❣❴❡①t❡♥❞s❴❝♦❞❡ ❣•♦❜❛•❴❝♦❞❡ ♣ st❛rt → ♣r♦❣❴❡①t❡♥❞s❴❛✉①❝♦❞❡ ❣•♦❜❛•❴❝♦❞❡✬ ♣✬ ❜❛s❡✬ → ♣r♦❣❴❡①t❡♥❞s❴❝♦❞❡ ❣•♦❜❛•❴❝♦❞❡✬ ♣✬ st❛rt✬ → ❆••♦❝❙♣❡❝ ♣ ♣✬ |❛ ✐♥✐t ✐♥✐t✬ ❛••♦❝ ❛••♦❝✬ ❞❡❛••♦❝ ❞❡❛••♦❝✬ → ✭❢♦r❛•• ♣tr ♣tr✬✱ |= ♣ ♣✬ ✭st❛rt✰•❡♥❣t❤ ✭✐♥str✉❝t❴♦❢ ❝♦❞❡✮✮ ✭st❛rt✬✰•❡♥❣t❤ ✭✐♥str✉❝t❴♦❢ ❝♦❞❡✬✮✮ ✿ ✭♠❡♠♦r②❴s♣❡❝✐❢✐❝❛t✐♦♥ |❛ |❝ |❝❴❝•♦✉❞ Γ ✭✭ a |❛✱✭♣tr✱♣tr✬✮✮ ✿✿ st❛❝❦❴•✐st✮ ✭st❛❝❦❴❢r❡❡✲✶✮ ✭st❛❝❦❴❢r❡❡✬✲✶✮ ✭st❛❝❦❴♣tr✰✶✮ ✭st❛❝❦❴♣tr✬✰✶✮ ♥ ♥✷ ♥✸ ♥✬ ♥✷✬ ♥✸✬✮ ⊤ ✮ → |= ♣ ♣✬ st❛rt st❛rt✬ ✿ ✭♠❡♠♦r②❴s♣❡❝✐❢✐❝❛t✐♦♥ |❛ |❝ |❝❴❝•♦✉❞ Γ st❛❝❦❴•✐st st❛❝❦❴❢r❡❡ st❛❝❦❴❢r❡❡✬ st❛❝❦❴♣tr st❛❝❦❴♣tr✬ ♥ ♥✷ ♥✸ ♥✬ ♥✷✬ ♥✸✬✮ ⊤ ✳ Figure 4. Semantic Type Soundness and R (m → R ⊤ ) then |= p, p ′ l, l ′ : R ⊤
which says that we get equitermination by executing the jump instructions at l and l ′ in states satisfying R if R entails that the location m through which we jump points to code pointers that later yield equitermination when jumped to in states satisfying R.

The crucial lemma for proving the recursive functions is the following, proved by appeal to the Löb rule we gave earlier:

▲❡♠♠❛ r❡❝✉rs✐♦♥❴❝♦♥t✐♥✉❛t✐♦♥ ✿ ❢♦r❛•• ♣tr ♣tr✬ ❢❝♦❞❡ ❢❝♦❞❡✬ |❛ ❛ ❜ | ♣ ♣✬✱ •✉❞❣♠❡♥t ✭Pr❡❴❛rr♦✇ ✭✭ ❛-→❜ ✮ |❛ ♣tr ♣tr✬ × |✮ ♣tr ♣tr✬ |❛ ✭ ❛ ✮ ✭ ❜ ✮✮ ♣ ♣✬ ❢❝♦❞❡ ❢❝♦❞❡✬ → •✉❞❣♠❡♥t ✭Pr❡❴❛rr♦✇✭✭♣tr✱♣tr✬ → ❢❝♦❞❡✱ ❢❝♦❞❡✬✮×|✮ ♣tr ♣tr✬ |❛ ✭ ❛ ✮ ✭ ❜ ✮✮ ♣ ♣✬ ❢❝♦❞❡ ❢❝♦❞❡✬✳
The antecedent is what we initially prove about the code pointers ❢❝♦❞❡ and ❢❝♦❞❡✬: that they will equiterminate appropriately provided that ♣tr and ♣tr✬ (which will be the heads of the two closure environments) point to equivalent functions. The consequent is what want to conclude about the result of tying the knot: that we then get equitermination when ♣tr and ♣tr✬ point, respectively, to ❢❝♦❞❡ and ❢❝♦❞❡✬ themselves.

Discussion

We have shown how to specify and verify a low-level relational interpretation of functional types. The construction involves a number of familiar ideas: the logical interpretation of types as relations, separation logic, orthogonality, step-indexing and so on, but putting them all together in the right way is far from trivial, and we certainly would not claim to have completely solved the problem. The existentially-quantified private invariant Rprivate at the top level of our interpretation of function types is a semantic generalization of the well-known use of existentially quantified types to abstract the type of environments in typed closure conversion [START_REF] Minamide | Typed closure conversion[END_REF][START_REF] Glew | Object closure conversion[END_REF][START_REF] Ahmed | Typed closure conversion preserves observational equivalence[END_REF]. Our general use of second order existential quantification over stateRels to express private invariants generalizes the standard treatment of type abstraction via existential types [START_REF] Mitchell | Abstract types have existential type[END_REF].

The use of 'orthogonality' or 'perping' in realizability was pioneered by [START_REF] Pitts | Operational reasoning for functions with local state[END_REF] and by Krivine, and has received much attention, notably by [START_REF] Vouillon | Semantic types: A fresh look at the ideal model for types[END_REF]. A general theory of such 'tensorial negations' is investigated in more detail in the thesis of the second author [START_REF] Tabareau | Modalités de Ressource et Contrôle en Logique Tensorielle[END_REF], but there are still open questions about their use in low-level settings. One such question is whether, now we have an adjunction and hence a (•) ⊤⊤ closure operator on stateRels, we really need explicit step indices too; in higher-level models, biorthogonal closed relations are automatically admissible. Another very important question is how one would adapt the kinds of specification used here to real machines with finite memory; it is not obvious what the 'corresponding' theorems should be.

Note that our interpretation of function types and general computations in context constrains them to be rather pure -the extent to which they can read or write the state is severely constrained. Our hope is to be able to do equational reasoning at the level of lowlevel code, proving that different bits of machine code are in the relation associated with a particular type. However, we have not yet managed to make this work, despite our move to total correctness specifications of the allocator. The CPS treatment of prerelations and postrelations seems to give us an equational theory which is roughly that of call-by-value CPS-transformed high-level functions. Whilst this is a strong constraint on the behaviour of machine code programs, it is still too weak to prove something as trivial as the high-level commutativity of addition, as the CPS transforms of

•❡t ① ❂ ▼ ✐♥ •❡t ② ❂ ◆ ✐♥ ①✰② and •❡t ② ❂ ◆ ✐♥ •❡t ① ❂ ▼ ✐♥ ①✰②
are not generally observationally equivalent. A related annoyance is that our CPS interpretation does not seem to validate the wellknown rule for conjunctive types

(A → B1) ∧ (A → B2) <:(A → B1 ∧ B2)
or the morally equivalent rule for introducing universal quantification over logical variables used in our refinement types:

[∀I] Γ ⊢ M : A(i) i ∈ Γ Γ ⊢ M : ∀i.A(i)
It is well known that these rules can be unsound in the presence of effects [START_REF] Davies | Intersection types and computational effects[END_REF], but our language is sufficiently pure that we should not require a value restriction here: we just have not quite captured that purity in our specifications.

Yet another wart on our otherwise beautiful theory is the way the treatment of total correctness makes explicit reference to particular code pointers. This is just about bearable for simple first-order procedures like the allocator, but would be untenable and insufficiently modular if we were to, say, try to interpret types of a normalizing lambda calculus. We are currently investigating some ideas about parametricity in the notion of 'observation' (here it was always equitermination) with respect to which one takes perps, which may help here.

One of our initial goals was that our interpretations of types be expressed in a logic that was essentially independent of the source. This seems desirable in multilanguage PCC settings, but certainly introduces some complexity. An alternative approach would be to define a 'represents' logical relation between a high-level semantics for the source language and the low-level compiled code (this would then induce a partial equivalence relation on low-level programs). [START_REF] Chlipala | A certified type-preserving compiler from lambda calculus to assembly language[END_REF] has already done this for a simple total functional language, which can be given a straightforward typetheoretic denotational semantics; we plan to do something similar using a formalized domain-theoretic semantics for our partial language. Our hope is that this will help us better understand the shortcomings of the low-level relations.

Finally, of course, we want to look at various forms of compiler correctness for high-level languages with effects. We and others have successfully applied essentially the same mathematical machinery to reasoning about higher-order functions with encapsulated local state [START_REF] Ahmed | Semantics of types for mutable state[END_REF][START_REF] Benton | Relational reasoning in a nominal semantics for storage[END_REF][START_REF] Pitts | Operational reasoning for functions with local state[END_REF][START_REF] Ahmed | State-dependent representation independence[END_REF], so moving those ideas down to the low level looks very doable.

There is a great deal of related work on program logics, compiler correctness and the semantics of types, much of which we have plundered here. Formal verification of compilers goes back over four decades [START_REF] Mccarthy | Correctness of a Compiler for Arithmetic Expressions[END_REF][START_REF] Dave | Compiler verification: a bibliography[END_REF] and has recently received increased attention, with notable automated efforts including Leroy's verification of an optimizing compiler for a C-like language [START_REF] Leroy | Formal certification of a compiler back-end, or: programming a compiler with a proof assistant[END_REF]). Appel's Foundational Proof Carrying Code project [START_REF] Appel | Foundational proof-carrying code[END_REF]) at Princeton has very similar goals to this work, and many of the techniques we use were introduced by Appel and his coauthors. We mention in particular the use of step-indexing [START_REF] Appel | An indexed model of recursive types for foundational proof-carrying code[END_REF][START_REF] Tan | Construction of a semantic model for a typed assembly language[END_REF] and its modal refinement [START_REF] Appel | A very modal model of a modern, major, general type system[END_REF]). Shao's group at Yale have also done impressive work on formalizing and verifying specifications for low-level code in Coq, including memory managers, garbage collectors and other challenging pieces of systems code [START_REF] Ni | Certified assembly programming with embedded code pointers[END_REF][START_REF] Yu | Building certified libraries for PCC: Dynamic storage allocation[END_REF]). It will be interesting to see if we can do similar things in our relational style.

  mapping an instruction, state and program counter to either a new state and program counter, or ◆♦♥❡ in the case that the instruction is a ❤❛•t. A configuration is thus a triple of a program, a state and a program counter. All our notions of behaviour arise from the primitive notion of termination:

  These say that if one calls related allocators in states in which the private invariant Ra holds (so the two allocators have been initialized), some separate invariant relation Rc holds on other parts of the stores, passing argument values n and n ′ , then the executions will end up at the return addresses with Ra and Rc still holding and r❡t pointing to disjoint blocks of memory of sizes n and n ′ on the respective sides.The relations |Pr❡❴❞❡❛••♦❝ and |P♦st❴❞❡❛••♦❝ used to specify the deallocator are given by

• ❛r❣ and r❡t, which are used in the call/return convention of the memory allocator.[V ar] Γ, x : A ⊢ x : A [Bool] b ∈ P Γ ⊢ b : Bool P [N at] n ∈ P Γ ⊢ n : Nat P [Abs] Γ, x : A ⊢ M : B Γ ⊢ λx.M : A → B [App] Γ ⊢ M : A → B Γ ⊢ N : A Γ ⊢ M N : B [F ix] Γ, f : A → B, x : A ⊢ M : B Γ ⊢ Fix f x = M : A → B [If ] Γ ⊢ M : Bool P P t ⇒ Γ ⊢ M1 : A P f ⇒ Γ ⊢ M2 : A Γ ⊢ if M then M1 else M2 : A [Op] Γ ⊢ M : Nat P1 Γ ⊢ N : Nat P2 Γ ⊢ M ⋆ N : Nat(P1 b ⋆ P2) [Gt] Γ ⊢ M : Nat P1 Γ ⊢ N : Nat P2 Γ ⊢ M > N : Bool(P1 b > P2) [P air] Γ ⊢ Mi : Ai (i = 1, 2) Γ ⊢ M1, M2 : A1 × A2 [P roj] Γ ⊢ M : A1 × A2 Γ ⊢ πi(M ) : Ai (i = 1, 2)

We have slightly simplified these specifications in this presentation by leaving out parts that just mention unused pseudo-registers.

This is essentially the same as the pexconj construction of[START_REF] Benton | Formalizing and verifying semantic type soundness of a simple compiler[END_REF].

Acknowledgments

Many thanks to Ivana Mijajlovic, who wrote the 'non-trivial' memory allocator module and did the initial correctness proof for it, and to Uri Zarfaty, who wrote the compiler itself.