PaperlayerView exact revision on arXiv

Source-linked AI summary

Preserving Separation Logic Specifications through Compilation

Carmine Abate, Kleio Liotati, František Farka, Sebastian Ertel

arXiv:2610.37244v1cs.PL

TL;DR

Separation-logic compiler correctness needs to relate source assertions and resource ownership to target resources, which behavioral semantics preservation does not provide by itself. The paper transports weakest preconditions through compilation using a resource-aware simulation over interaction trees. It establishes this transfer for closed programs and separately compiled modules, with module specifications preserved under linking, and identifies boundaries on the separate-compilation setting.

  • Problem

    Semantic compiler guarantees constrain behavior but do not specify how source assertions and ownership requirements are represented in compiled code.

    Source: §1 · pp. 1–2

  • Method

    A resource-aware simulation over interaction trees relates source and target event resources and tracks ownership through target-only operations such as register accesses.

    Source: §1 · p. 3, §3 · p. 6

  • Results

    The approach establishes WP-preservation for closed IMP-to-ASM programs and separately compiled modules, whose specifications carry over and are preserved when compiled modules are linked.

    Source: §1 · p. 3, §8 · p. 25

  • Takeaways & Limitations

    The target precondition can own only the compiled command’s memory cells and registers, allowing target clients to frame the rest of target memory.

    Source: §8 · p. 24

    Open modules are covered only through contracts with link-wide fixed register and local pools and visible variables, and target calls may overwrite every register in the pool.

    Source: §8 · p. 25

Abstract

from arXiv · show

Program specifications in separation logic describe ownership of resources and serve as logical interfaces for local reasoning. Compiler correctness, expressed as semantics preservation, does not by itself supply such an interface for compiled code, because it does not explicitly relate source and target resources and assertions. We investigate WP-preserving compilation: when a compiler translates a source program, the weakest preconditions that the program satisfies in a separation logic carry over to the compiled program. Our proof technique consists of a resource-aware simulation over interaction trees: it relates the resources required by corresponding source and target events, and tracks ownership through target operations, such as register accesses, that have no source counterpart. We apply the approach to a compiler from a structured imperative language to an assembly-like language, first for closed programs and then extended with modules and function calls. In the extended setting, each module can be verified in the source logic and compiled separately; its specifications carry over to the compiled module and are preserved when compiled modules are linked. All results are mechanized in Rocq.

1 Introduction

Separation-logic specifications provide resource-aware logical interfaces for clients, but semantic compiler correctness alone does not provide a corresponding interface for compiled code. The paper investigates WP-preserving compilation and develops a resource-aware simulation to transfer source proofs to compiled programs, including separately compiled modules.

1 Introduction

  • Separation-logic specifications describe resource ownership and let clients reason about components without inspecting their implementations.Clients can retain ownership of separately held resources.Source: §1 · p. 1
  • Behavioral compiler guarantees do not specify how source assertions and ownership requirements are represented in the target.A source variable may map to target memory, while compiled code may also use registers.Source: §1 · p. 2
  • WP-preserving compilation carries the weakest preconditions satisfied by a source program over to its compiled program.The paper notes that preserving weakest preconditions also preserves Hoare triples.Source: §1 · p. 2
  • A resource-aware simulation over interaction trees relates corresponding event resources, tracks ownership across steps, and accounts for target-only operations.The transfer lemma is independent of source and target event signatures, return types, and logical handlers, and the simulation is closed under bind and iteration.Source: §1 · p. 3
  • The approach establishes WP-preservation for IMP-to-ASM closed programs and extends it to separately compiled modules whose specifications survive linking.The modules example uses mutually recursive functions that decrement a shared counter while passing its ownership across module boundaries; the results are formalized in Rocq.Source: §1 · p. 3

2 Background on Interaction Trees

Interaction trees represent recursive, effectful computations, including infinite eventful behavior and silent divergence. Their event handlers support both executable interpretations and weakest-precondition program logics.

Interaction trees

  • An interaction tree has return, silent-step, and visible-event constructors, and its coinductive form can represent infinite computations.Visible events receive an answer from the environment before continuing; infinite silent steps represent divergence.Source: §2 · pp. 3–4

Equational theories

  • Weak bisimulation compares returns and visible events while ignoring finite silent steps, but still distinguishes silent divergence from termination.The relation can compare trees with different return and event types by relating their values and events.Source: §2 · p. 4

Algebraic structure

  • ITrees form a monad whose bind replaces return leaves with continuations while preserving silent steps and visible events.The monadic laws hold up to weak bisimulation.Source: §2 · p. 4

Computational and logical interpretations

  • An algebraic handler interprets events as computations, while a logical handler assigns event specifications and supports weakest-precondition reasoning over an entire tree.Handlers combine over disjoint event signatures, and their interpretations have laws for iteration and recursion.Source: §2 · p. 4

Program logics from ITree semantics

  • ITree semantics yield language program logics by combining a weakest-precondition calculus with logical handlers for language events.Adding an effect can extend the logic by supplying a handler for the new events while leaving existing handlers unchanged.Source: §2 · pp. 4–5

3 WP-preservation Overview

The overview illustrates how a source separation-logic proof can yield a target weakest precondition for compiled code. A resource-aware simulation relates source and target events while tracking the additional register ownership required by the target.

3 WP-preservation Overview

  • The example starts from the source specification that incrementing x returns ownership of x with its updated value.The compiled sequence loads x, places 1 in a register, adds, and stores the result to ax.Source: §3 · p. 5
  • The simulation relates source variable reads and writes to target memory loads and stores, supplying resources for subsequent proof obligations.For the example, GetVar(x) matches Load(ax), and SetVar(x, ·) matches Store(ax, ·).Source: Figure 2 · p. 6, §3 · p. 6
  • Target-only register operations let the source stutter while the simulation tracks register contents and carries ownership forward.The example requires ownership of r0 and r1 even though their initial values are arbitrary, because both are overwritten before being read.Source: §3 · p. 7
  • A state correspondence relates the source variable x to target cell ax and supports extracting target ownership from the source postcondition.The correspondence owns the cell and source authority; the target frame rule can then add separately owned memory such as ay.Source: §3 · p. 7
  • The compiled increment program satisfies a target weakest precondition owning the source variable’s target cell and compiled-code registers, while preserving framed ownership of another cell.The resulting postcondition includes ax at n+1 and ay at 0.Source: §3 · p. 7

4 IMP-to-ASM: Languages, Logic, and Compilation

This section sets up WP-preservation for an IMP-to-ASM compiler by presenting the languages, their semantics, the IMP logic, and the compilation scheme.

4 IMP-to-ASM: Languages, Logic, and Compilation

  • The section instantiates the approach with the IMP-to-ASM compiler of Xia et al., while noting that arbitrary source assertions may lack target counterparts.The stated correspondence applies to points-to assertions.Source: §4 · p. 7

4.1 Source Language: IMP

  • IMP commands use a store mapping variable identifiers to optional natural numbers; reading an undeclared or unset variable triggers undefined behavior.Its ITree semantics represents reads and writes as events, with sequencing, conditionals, and loops expressed compositionally.Source: §4.1 · p. 8

4.2 IMP Program Logic

  • The IMP logic derives weakest preconditions from ITree semantics, with points-to assertions describing ownership of individual variables and framing retaining untouched resources.Reads permit fractional ownership, writes require full ownership, and proving a weakest precondition requires ruling out undefined behavior.Source: §4.2 · pp. 8–9

4.3 Target Language: ASM

  • ASM is a control-flow-graph language whose instructions transform register and memory state, while jumps, branches, and halt govern control between blocks.Its semantics distinguishes absent locations from existing but uninitialized ones, and models register, memory, exit, and step events.Source: §4.3 · pp. 9–10

4.4 Compilation

  • Compilation follows IMP syntax: expressions use registers and loads, assignments store through variable addresses, and graph combinators implement sequencing, branches, and loops.Denotation laws express sequencing as bind and looping as ITree iteration, supporting compositional compiler proofs.Source: §4.4 · p. 10

5 WP-Preservation

The section develops a resource-aware simulation principle for transferring weakest preconditions over interaction trees, then applies it to preserve IMP specifications under compilation to ASM. The resulting target weakest preconditions retain source postconditions alongside state correspondence, enabling target-level framing and reasoning.

5.1 Abstract Transfer Lemma

  • The abstract transfer lemma transports an entire weakest precondition when the simulation handles returns, silent steps, and matched visible events with resource-aware answer relations.Source and target assertions share an Iris resource universe, allowing the simulation to relate returned values and available resources.Source: §5.1 · p. 11

5.2 A Resource-Aware Simulation for the ITrees of IMP and ASM

  • The IMP–ASM simulation matches variable reads and writes while tracking their resources, and permits target register operations and silent steps between matched events.Its return relation restores state correspondence so subsequent commands can reuse registers; the simulation satisfies the transfer conditions and is closed under bind and iteration, assuming loops cannot silently restart forever.Source: §5.2 · p. 13

5.3 WP-Preservation for IMP-to-ASM

  • For every IMP command, the compiled ASM program satisfies a target weakest precondition returning the source postcondition together with correspondence for the command’s variables and registers.Because that correspondence owns only resources used by the command, the target frame rule preserves separately owned resources.Source: §5.3 · p. 15
  • The theorem retains the source postcondition with correspondence rather than translating arbitrary assertions; points-to assertions can be extracted as target memory assertions when the required target ownership is available.Cells of variables unused by the command can be framed separately in the target logic.Source: §5.3 · pp. 15–16
  • The Fibonacci example begins with ownership of its variables at arbitrary values and yields target points-to assertions together with register ownership and the correspondence cell for temp.The target precondition owns only the program’s five variable cells and registers, so unrelated memory can be framed.Source: §5.3 · p. 16

6 Separate Compilation

Separate compilation extends WP-preservation from closed programs to modules and linked programs. Modules can be verified against contracts and compiled separately, with their specifications preserved for compiled code and linked programs.

6.1 Modules, Calls, and Linking

  • Modules declare globals, functions, and imported or exported signatures; linking maps qualified function names to definitions, and a resolver handles calls through that table.IMP calls return a result expression evaluated after the body, whereas ASM functions return through register r0.Source: §6.1 · p. 17

6.2 Contracts

  • Function contracts pair argument preconditions with result postconditions, using a caller-chosen witness to relate handed-over and returned resources.For internal calls, scoped contracts also lend callers’ local-variable ownership and return those locals unchanged; target contracts include state correspondence.Source: §6.2 · pp. 18–19

6.3 WP-Preservation under Separate Compilation

  • The proof relates each source function run by its resolver to its compiled counterpart, then shows that resolving related calls recursively preserves the relation.The state correspondence is maintained across calls, and the transfer lemma is reused unchanged.Source: §6 · p. 16, §6.3 · p. 19
  • A function proved against its source contract satisfies a corresponding target contract, assuming its callees satisfy their target contracts.Applying function-level preservation across a module yields per-module contract preservation.Source: §6.3 · p. 20
  • Separate compilation preserves source weakest preconditions for linked programs, including proofs against contracts where modules and entry commands are verified separately.Each module is verified once against its contracts; the entry command uses the same contracts without a proof of the linked source program.Source: §6.3 · pp. 20–21

6.4 Case Study: a Shared Counter

  • In the shared-counter example, independently proved mutually recursive functions pass counter ownership to each other and return it set to zero.After linking the compiled modules, the entry command ends with the counter set to zero in target memory.Source: §6.4 · p. 21

7 Related Work

Prior compiler results preserve behaviors, predicates, or translated proofs, but do not generally provide compiled code with a separation-logic specification. This work instead transports weakest preconditions, including ownership, to compiled code and extends that guarantee to separately compiled modules.

Specification-preserving compilation

  • Unlike behavioral refinement and whole-state predicate preservation, WP-preservation transports separation-logic judgments with ownership and a footprint limited to what compiled code uses.The target specification can be used in target-level reasoning, including across separately compiled functions.Source: §7 · pp. 22–23

Proof-transforming compilation

  • Proof-transforming compilers translate proofs, specifications, or verification conditions, whereas this compiler operates on programs alone and preserves every semantic weakest precondition.The approach requires a simulation rather than identical proof obligations and extends to separate compilation.Source: §7 · pp. 22–23

Interaction trees and compiler verification

  • Prior interaction-tree compiler results establish behavioral equivalence or refinement; this simulation instead ties events to logical specifications to transport weakest preconditions across lowering.The paper also distinguishes its guarantee from robust compilation: it does not consider adversarial contexts.Source: §7 · pp. 23–24

8 Conclusions and Future Work

The paper presents WP-preserving compilation as a way to carry source logical interfaces, including resource ownership, to compiled code. It extends this result to separately compiled modules, while identifying boundaries and directions for generalization.

8 Conclusions and Future Work

  • A resource-aware simulation over interaction trees and a generic WP-transfer lemma transport source weakest preconditions to compiled IMP-to-ASM programs despite differing effects and target administrative operations.The target precondition has a limited footprint, owning only the compiled command’s variable cells and registers.Source: §8 · pp. 24–25
  • Modules verified against import contracts can be compiled separately, with their specifications preserved in compiled modules and when those modules are linked.Callers also retain their local values across calls.Source: §8 · p. 25
  • Separate-compilation results cover closed programs whose target modules all come from this compiler; open modules are covered through contracts under fixed register, local, and visible-variable pools.The target call contract permits a callee to overwrite every register in the pool, so clients cannot keep register values across calls.Source: §8 · p. 25
  • Future work includes value and location relations, fractional points-to extraction, a reusable resource-aware ITree relation, and preservation against adversarial target contexts.Robust preservation would require restricting target modules, for example through link-time checks or capabilities.Source: §8 · p. 25

A Details of WP-Preservation

A.1 The abstract transfer interface

The abstract transfer interface specifies what a resource-aware simulation must establish to carry weakest preconditions between interaction trees. For matched visible events, it connects the source and target logical handlers while preserving the continuation relationship.

A.1 The abstract transfer interface

  • For a matched visible event, the simulation must relate events and answers and provide a handler-transport wand connecting the source and target handler assertions.The target event’s weakest precondition is established using the event relation, continuation simulation, and transport wand.Source: §A.1 · pp. 30–31
  • The visible-event premise quantifies over target answer types, events, and continuations, allowing the transfer interface to relate different event signatures.The IMP and ASM handlers ignore the auxiliary thread-spawning continuation assertion.Source: §A.1 · p. 30
  • The transfer condition permits an Iris fancy update, which supports ghost updates even when logical handlers specify events only with points-to assertions.For matched IMP and ASM writes, the transport updates the source authority of the written variable.Source: §A.1 · pp. 30–31

A.2 The IMP–ASM simulation

The IMP–ASM simulation uses a resource correspondence for command variables and compiler registers. Its composition and iteration properties let the simulation extend across sequential commands and loops.

A.2 The IMP–ASM simulation

  • The simulation uses CorrX,V, which owns the compiler’s register footprint and the command’s variables, and supports larger register and variable sets.For command c, the resource relation is Corrc, with X ⊇ Xc and V ⊇ Vc.Source: §A.2 · p. 31

A.3 Composition and iteration

  • The simulation composes over binds when corresponding initial states and intermediate returns satisfy their relations.The composition properties include both state-relation preservation and a bind rule.Source: §A.3 · p. 31

3. Let I relate loop states, and define

  • Loop simulation relates loop states through an invariant, with inl restarting and inr returning; its reusable body premise requires well-founded source restarts without visible events.The body premise is reusable via □.Source: §3 · pp. 31–32

A.4 Specification transfer and target points-to

The transfer results preserve source weakest preconditions for compiled commands, including when target exit postconditions are arbitrary. A second theorem provides target points-to assertions for initialized variables.

A.4 Specification transfer and target points-to

  • Table 1 summarizes resource ownership across the source WP, simulation correspondence, and target WP; whole-store, memory, and register authorities occur only in handler adequacy proofs.A dash marks a resource absent from that part of the account.Source: Table 1 · p. 32, §A.4 · p. 32
  • WP preservation holds for every command under the same invariant mask and step modality, with an arbitrary target exit postcondition.The theorem transfers a source weakest-precondition premise to the compiled command.Source: §A.4 · p. 32
  • The proof extracts target points-to assertions from the correspondence, then applies WP preservation to derive the target specification.The extraction uses agreement between the authority and the target cell; assertions about cells outside Vc are preserved by the target frame rule.Source: §A.4 · pp. 32–33
  • For initialized variables in F, the target precondition includes their points-to assertions alongside register ownership, Q, and correspondence for variables outside dom F.The theorem assumes dom F ⊆ Vc.Source: §A.4 · p. 32

B The IMP Program Logic

The appendices detail the IMP logic and extend WP preservation to separately verified modules with calls. They specify the ownership, contracts, and compatibility conditions used in that extension.

B The IMP Program Logic

  • IMP’s logic fixes a mask and step modality; its rules preserve ownership through expression evaluation, assignment, sequencing, and guarded while reasoning.Expression evaluation is left to right, and assignment can reuse the assigned variable’s ownership if it is returned before the write.Source: B The IMP Program Logic · p. 33

C Details of Separate WP-Preservation

  • The shared ghost state uses per-key authorities and points-to assertions, allowing correspondence to own only selected variables while handlers implement per-key events over whole maps.The store treats absent keys as undefined behavior, whereas register and memory reads can return None and writes can insert a key.Source: B The IMP Program Logic · pp. 33, 35

C.1 Modules, Linking, and Compilation

  • Linking qualifies module function names and unions their tables; compiling linked modules yields the same table as compiling each function after linking.Compiled functions map parameters to registers and locals, and the partial resolver re-emits calls outside its table as external events.Source: §C.1 · pp. 36–37

C.2 Rules for Function Calls

  • Call contracts specify argument preconditions and result postconditions; the call rule evaluates arguments, establishes the precondition, and assigns the result to an owned variable.Scoped contracts additionally lend the caller’s local pool and return it unchanged, except for the result variable.Source: §C.2 · pp. 37–38

C.3 Contracts and Call Contexts

  • Internal calls lend the full pool of linked-function locals because a callee may overwrite caller locals, then restore their saved values; external calls share a context on both sides.Internal calls also carry the state correspondence to the target callee; the caller retains it across external calls.Source: §C.3 · p. 38

C.4 Resources and State Correspondence

  • The link-wide correspondence owns the register pool and visible-variable cells, while allocation establishes the state interpretations and points-to assertions needed for the transfer theorems.The correspondence does not own a resource over the whole store or memory.Source: §C.4 · pp. 38–39

C.5 The Simulation with Calls

  • Commands using only the designated pool and visible variables preserve WPs across calls when source and target call contexts answer compatibly.The simulation relates calls with the same function and arguments, handing the correspondence to the callee and receiving it back.Source: §C.5 · p. 39

C.6 Well-Formedness of Modules

  • A module is well formed when its functions satisfy naming, variable, and arity conditions and are proved against their contracts; that proof obligation mentions other modules only through contracts.Parameters and locals must be distinct and belong to the designated pool; linked source and target tables must contain the module functions with distinct names.Source: §C.6 · p. 40

C.7 Proofs of the Main Results

The per-function open simulation relates execution of a function and its compiled body step by step, including calls left visible as events. A source contract proof then supplies a target WP for the compiled function.

C.7 Proofs of the Main Results

  • The open simulation relates function executions step by step, leaving calls as events related when callee names and arguments match.The function prologue’s parameter stores correspond to source argument passing, and the body simulation composes with the result-expression case.Source: §C.7 · p. 40
  • A source contract proof yields a source WP for the function run, which the per-function simulation transfers to a target WP under the target context.The proof supplies the local pool at known values and returns the callee’s saved locals.Source: §C.7 · p. 40
  • Applying the per-function result to every module function establishes the module result; internal calls are re-tagged as internal events without changing their WP.The simulation uses the empty mask on both sides.Source: §C.7 · p. 40

C.8 Linked Programs and Adequacy

The linked-program results extend the simulation to resolved calls, yielding weakest-precondition guarantees for compiled linked programs and contracts. A shared-counter example illustrates modular verification across calls and linking.

C.8 Linked Programs and Adequacy

  • The linking law turns related open simulations into a closed simulation when the source and target call resolvers are pointwise related and each call computation is guarded by a step.The proof applies the law to the compiled entry command and uses the resulting closed simulation to establish item 1 of Theorem 3.Source: §C.8 · p. 41
  • Under item 1 of Theorem 3’s hypotheses, the compiled linked program satisfies an Iris weakest precondition, never exits, and reaches the specified postcondition when fuel is exhausted or it terminates.A pure final-state statement would additionally require Iris adequacy, which is not mechanized.Source: §C.8 · p. 41
  • For item 2 of Theorem 3, module contracts assume internal-call contracts, and Löb induction discharges them for all linked functions at once, fixing the step modality to Later.The compiled entry-command weakest precondition is preserved when its calls are resolved by T.Source: §C.8 · p. 41

C.9 The Shared Counter in Full

  • In the shared-counter example, f and g pass the decremented counter’s ownership to each other through Call-Scoped, and linking with contracts yields the entry-command result for every frame R.The proof treats the zero-counter case immediately; otherwise PRED decrements the counter, and the proof for g is symmetric.Source: §C.9 · p. 42
  • The example’s precondition owns no target cells beyond k, r, and G.c, alongside correspondence cells for k and r.PRED is given by a loop that increments k while k + 2 ≤ x, then assigns x := k.Source: §C.9 · pp. 41–42
Loading 2610.37244v1…