relational logic with framing and hypotheses

Relational properties arise in many settings: relating two versions of a program that use different data representations, noninterference properties for security, etc. The main ingredient of relational verification, relating aligned pairs of intermediate steps, has been used in numerous guises, but existing relational program logics are narrow in scope. This paper introduces a logic based on novel syntax that weaves together product programs to express alignment of control flow points at which relational formulas are asserted. Correctness judgments feature hypotheses with relational specifications, discharged by a rule for the linking of procedure implementations. The logic supports reasoning about program-pairs containing both similar and dissimilar control and data structures. Reasoning about dynamically allocated objects is supported by a frame rule based on frame conditions amenable to SMT provers. We prove soundness and sketch how the logic can be used for data abstraction, loop optimizations, and secure information flow.

section_content: Relational properties are ubiquitous. Compiler optimizations, changes of data representation, and refactoring involve two different programs. Non-interference (secure information flow) is a non-functional property of a single program; it says the program preserves a "low indistinguishability" relation [44]. Many recent works deal with one or more of these applications, using relational logic and/or some form of product construction that reduces the problem to partial correctness, though mostly for simple imperative programs. This paper advances extant work by providing a relational logic for local reasoning about heap data structures and programs with procedures. 

To set the stage, first consider the two simple imperative programs: C = x := 1; while y > 0 do x := x * y; y := y -1 od C = x := 1; y := y -1; while y ≥ 0 do x := x * y + x; y := y -1 od

Both C and C change x to be the factorial of the initial value of y, or to 1 if y is initially negative. For a context where y is known to be positive and its final value is not used, we could reason that they are interchangeable by showing both

This is our notation for partial correctness judgments, with evident pre-and postconditions, for C and C. It is not always easy to express and prove functional correctness, which motivates a less well developed approach to showing interchangeability of the examples. The two programs have a relational property which we write as

This relational correctness judgment says that a pair of terminating executions of C and C, from a pair of states which both satisfy y ≥ 0 and which agree on the value of y, yields a pair of final states that agree on the value of x. The relational formula x = x says that the value of x in the left state is the same as its value in the right state. Property ( 2 ) is a consequence of functional correctness (1), but there is a direct way to prove it. Any pair of runs, from states that agree on y, can be aligned in such a way that both x = x and y = y + 1 hold at the aligned pairs of intermediate states. The alignment is almost but not quite step by step, owing to the additional assignment in C. The relational property is more complicated than partial correctness, in that it involves pairs of runs. On the other hand the requisite intermediate assertions are much simpler; they do not involve ! which is recursively defined. Prior work showed such assertions are amenable to automated inference (see Section 7). 

Despite the ubiquity of relational properties and recent logic-based or product-based approaches to reasoning with them (see Section 7), simple heap-manipulating examples like the following remain out of reach: (1) ; while y > 0 do xp. set(xp. get() * y); y := y -1 od; x := xp. get() This Java-like program uses get/set procedures acting on an object that stores an integer value, and (C|C ) satisfies the same relational specification as (2). This code poses significant new challenges. It is not amenable to product reductions that rely on renaming of identifiers to encode two states as a single state: encoding of two heaps in one can be done, but at the cost of significant complexity [35] or exposing an underlying heap model below the level of abstraction of the programming language. Code like C also needs to be linked with implementations of the procedures it calls. For reasoning about two versions of a module or library, relational hypotheses are needed, and calls need to be aligned to enable use of such hypotheses. 

Floyd [22] articulates the fundamental method of inductive assertions for partial correctness: establish that certain conditions hold at certain intermediate steps of computation, designating those conditions/steps by associating formulas with control flow points. For relational reasoning, pairs of steps need to be aligned and it is again natural to designate those in terms of points in control flow. Alignment of steps has appeared in many guises in prior work, often implicit in simulation proofs but explicit in a few works [47, 8, 28].
section_name: Introduction

section_content: In this paper we embody the alignment principle in a formal system at the level of abstraction of the programming language -as Hoare logic does for the inductive assertion method -with sufficient generality to encompass many uses of relational
section_name: First contribution:

section_content: properties for programs including procedures and dynamically allocated mutable objects. Our logic (Section 6) manifests the reasoning principle directly, in structured syntax. It also embodies other reasoning principles, such as frame rules, case analysis, and hypothetical specifications for procedures. The rules encompass relations between both similarly-and differently-structured programs, and handle partially and fully aligned iterations. This achievement brings together ideas from many recent works (Section 7), together with two ingredients we highlight as contributions in their own right. 

Second contribution: Our relational assertion language (Section 4) can describe agreement between unbounded pointer structures, allowing for differences in object allocation, as is needed to specify noninterference [4] and for simulation relations [3] in languages like Java and ML where references are abstract. Such agreements are expressed without the need for recursively defined predicates, and the assertion language has a direct translation to SMT-friendly encodings of the heap. (For lack of space we do not dwell on such encodings in this paper, which has a foundational focus, but see [40, 7]. ) Third contribution: We introduce a novel form of "biprogram" (Section 5) that makes explicit the reasoner's choice of alignments. A biprogram run models an aligned pair of executions of the underlying programs. The semantics of biprograms involves a number of subtleties: To provide a foundation for extending the logic with encapsulation (based on [5] ), we need to use small-step semantics -which makes it difficult to prove soundness of linking, even in the unary case [5]. For this to work we need to keep the semantics deterministic and to deal with semantics of hypotheses in judgments. 

Section 2 provides background and Section 3 is an overview of the logic using examples. We have chosen to use the available space to explain fundamental intuitions. An accompanying technical report includes worked proofs of the examples, additional examples like a loop tiling transformation, details of semantics, and the soundness theorem.
section_name: 11:3

section_content: For reasoning about the heap, separation logic is very effective, with modal operators that implicitly describe heap regions. But for relations on unbounded heap structures at the Java/ML level of abstraction we need explicit means to refer to heap regions, as in the dependency logic of Amtoft et al. [2]. Our relational logic is based on an underlying unary logic dubbed "region logic" (RL), developed in a series of papers [10, 5, 7] to which we refer for rationale and omitted details. RL is a Hoare logic augmented with some side conditions (first order verification conditions) which facilitate local reasoning about frame conditions [10] in the manner of dynamic frames [27, 31]. In the logic such reasoning hinges on a frame rule. 

In a verifier, framing can be done by the VC-generator, optionally guided by annotation [40]. 

Stateful frame conditions also support an approach to encapsulation that validates a second order frame rule (at the cost of needing to use small-step semantics) [5]. Read effects enable the use of pure method calls in assertions and in frame conditions [7] and are useful for proving some equivalences, like commuting assignments, that hold in virtue of disjointness of effects [15]. The logic is formalized for imperative programs with first order procedures and dynamically allocated mutable objects (records), see Fig. 1. As in Java and ML, references are distinct from integers; they can be tested for equality but there is no pointer arithmetic. Typing of programs is standard. In specifications we use ghost variables and fields of type rgn. A region is a set of object references, which may include the improper null reference. 

A specification P ; Q [ε] is comprised of precondition P, postcondition Q, and frame condition ε. Frame conditions include both read and write effects:

The form rd G'f means the program may read locations o. f where o is a reference in the region denoted by expression G. We write rw x to abbreviate the composite effect rd x, wr x, and omit repeated tags: rd x, y abbreviates rd x, rd y. Predicate formulas P include standard first order logic with equality, region subset (G ⊆ G), and the "points-to" relation x. f = E, which says x is non-null and the value of field f equals E. A correctness judgment has the form Φ C : P ; Q [ε] where the hypothesis context Φ maps procedure names to specifications. In C there may be environment calls to procedures bound by let inside C, and also context calls to procedures in Φ. The form G'f is termed an image expression. For an example of image expressions, consider this command which sums the elements of a singly-linked null-terminated list, ignoring nodes for which a deletion flag, del, has been set. C 1 = s := 0; while p = null do if ¬p. del then s := s + p. val fi; p := p. nxt od For its specification we use ghost variable r : rgn to contain the nodes. Its being closed under nxt is expressed by r'nxt ⊆ r in this specification:

The r-value of the image expression r'nxt is the set of values of nxt fields of the objects in r. In frame conditions, expressions are used for their l-values. In this case, the frame condition uses image expressions to say that for any object o in r, locations o. val, o. nxt, o. del may be read. The frame condition also says that variables s and p may be both read and written. Let function listnd give the mathematical list of non-deleted values. Some proof rules in RL have side conditions which are first order formulas on one or two states. One kind of side condition, dubbed the "frames judgment", delimits the part of state on which a formula depends (its read effect). RL's use of stateful frame conditions provides for a useful frame rule, and even second order frame rule [37, 5], but there is a price to be paid. Frame conditions involving state dependent region expressions are themselves susceptible to interference by commands. That necessitates side conditions, termed "immunity" and "read-framed", in the proof rules for sequence and iteration [5, 7]. The frame rule allows to infer from Φ C : P

R is framed by read effects η (written η frm R) for locations disjoint from those writable according to ε (written η •/. ε). 

In keeping with our goal to develop a comprehensive deductive system, our unary and relational logics include a rule for discharging hypotheses, expressed in terms of the linking construct. Here is the special case of a single non-recursive procedure. 

3
section_name: Background: synopsis of region logic

section_content: This section sketches highlights of relational reasoning about a number of illustrative examples, introducing features of the logic incrementally. Some details are glossed over. We write (C|C ) : Q ≈> R to express that a pair of programs C, C satisfies the relational contract with precondition Q and postcondition R, leaving aside frame conditions for now. The judgment constrains executions of C and C from pairs of states related by Q. (For the grammar of relational formulas, see (7) in Section 4. ) It says neither execution faults (e. g., due to null dereference), and if both terminate then the final states are related by R. Moreover no context procedure is called outside its precondition. (We call this property the ∀∀ form, for contrast with refinement properties of ∀∃ form. )

Assume f, g are pure functions. The programs

are equivalent. Focusing on relevant variables, the equivalence can be specified as

which can be proved as follows. Both C 0 and C 0 satisfy true

) by an embedding rule. 

The general form of embedding combines two different unary judgments, with different specifications, using relational formulas that assert a predicate on just the left ( ) or right ( ) state. So BP is short for P ∧ P. Since z is not written by C 0 or C 1, we can introduce z = z using the relational frame rule, to obtain

This yields (3) using the relational rule of consequence with the two valid relational assertion

For the factorial example (C|C ) in Section 1, we would like to align the loops and use the simple relational invariant x = x ∧ y = y + 1. We consider the form (C|C ) as a biprogram which can be rewritten to equivalent forms using the weaving relation which preserves the underlying programs but aligns control points together so that relational assertions can be used. (A minor difference from most other forms of product program is that we do not need to rename apart the variables on the left and right. ) The weaving relation is given in Section 5. In this case we weave to the form

This enables us to assert the relational invariant at the beginning and end of the loop bodies. Indeed, we can also assert it just before the last assignments to y. The rule for this form of loop requires the invariant to imply equivalence of the two loops' guard conditions, which it does: x = x ∧ y = y + 1 ⇒ (y > 0 = y ≥ 0). For a biprogram of the split form (C|C ),
section_name: Overview of the relational logic

section_content: Relational Logic with Framing and Hypotheses the primary reasoning principle is the lifting of unary judgments about C and C. For an atomic command A, the sync notation A is an alternative to (A|A) that indicates its left and right transition are considered together. This enables the use of relational specifications for procedures, and a relational principle for object allocation. For an ordinary assignment, sync merely serves to abbreviate, as in y := y -1 above. 

The next example involves the heap and it also involves a loop that is "dissonant" in the sense that we do not want to align all iterations -that is, alignment is ultimately about traces, not program texts. Imagine the command C 1 from Section 2 is run on a list from which secret values have been deleted. To specify that no secrets are leaked, we use the relational judgment (C 1 |C 1 ) : listnd(p) = listnd(p) ≈> s = s which says: Starting from any two states containing the same non-deleted values, terminating computations agree on the sums. The judgment can be proved by showing the functional property that s ends up as sum(listnd(old(p))). But we can avoid reasoning about list sums and prove this relational property by aligning some of the loop iterations in such a way that listnd(p) = listnd(p) ∧ s = s holds at every aligned pair, that is, it is a relational invariant. Not every pair of loop iterations should be aligned: When p. del holds for the left state but not the right, a left-only iteration maintains the invariant, and mutatis mutandis when p. del holds only on the right. To handle such non-aligned iterations we use a novel syntactic annotation dubbed alignment guards. The idea is that the loop conditions are in agreement, and thus the iterations are synchronized, unless one of the alignment guards hold -and then that iteration is unsynchronized but the relational invariant must still be preserved. We weave (C 1 |C 1 ) to the form

with alignment guards p. del and p. del. The rule for the while biprogram has three premises for the loop body: for executions on the left (resp. right) under alignment guard p. del (resp. p. del) and for simultaneous executions when neither of the alignment guards hold. Each premise requires the invariant to be preserved. 

The final example is a change of data representation. It illustrates dynamic allocation and frame conditions, as well as procedures and linking. A substantive example of this sort would be quite lengthy, so we contrive a toy example to provide hints of the issues that motivate various elements of our formal development. Our goal is to prove a conditional equivalence between these programs, whose components are defined in due course. 

These differ only in the implementations B, B of the stack interface (here stripped down to a single procedure), to which the client program Cli is linked. For modular reasoning, the unary contract for push should not expose details of the data representation. We also want to avoid reliance on strong functional specifications -the goal is equivalence of the two versions, not functional correctness of the client. The client, however, should respect encapsulation of the stack representation, to which end frame conditions are crucial. A simple pattern is for contracts to expose a ghost variable rep (of type rgn) for the set of objects considered to be owned by a program module. Here is the specification for push, with parts named for later reference. Let size and rep be spec-public, i. e., they can be used in public contracts but not in client code [30]. Variables rep and size can be read and written (keyword rw) by push. This needs to be explicit, even though client code cannot access them, because reasoning about client code involves them. The notation rep'any designates all fields of objects in rep; these too may be read and written. The specification makes clear that calls to push affect the encapsulated state, while not exposing details. Here is one implementation of push(x). This form is convenient in using ghost code to express shapes of data structures without recourse to reachability or other inductive predicates [10, 40]. 

As a specific Cli, we consider one that allocates and updates a node of the same type as used by the list implementation; this gets assigned to a global variable p. Cli = push(1); p := new Node(null, 2); p. val := 3; push (4) Having completed the definitions of C 4, C 4 we can ask: In what sense are C 4, C 4 equivalent? A possible specification for (C 4 |C 4 ) requires agreement on size and ensures agreement on size and on p and p. val. However, the latter agreements cannot be literal equality: following the call push (1), one implementation has allocated a N ode whereas the array implementation has not. Depending on the allocator, different references may be assigned to p in the two executions. The appropriate relation is "equivalence modulo renaming of references" [2, 3, 4, 16, 17]. For region expression G and field name f, we write AG'f for the agreement relation that says there is a partial bijection on references between the two states, that is total on the region G, and for which corresponding f -fields are equal. The notation AG'any means agreement on all fields. In the present example, we only need the singleton region {p} containing the reference denoted by p. 

To prove a relational judgment for (C 4 |C 4 ) we need suitable relational judgments for (B|B ) for the implementations of push. It is standard [26] that they should preserve a "coupling relation" that connects the two data representations and also includes the data invariants for each representation. For the example, the connection is that the sequence of elements reached from top, written list(top), is the same as the reversed sequence of elements in slots[0. . f ree -1]. Writing rev for reversal, we define the coupling and specification
section_name: F S T T C S 2 0 1 6 11:6

section_content: 11:8
section_name: F S T T C S 2 0 1 6

section_content: We now proceed to sketch a proof of (6). First, we weave (C 4 |C 4 ) to let push(x : int) = (B|B ) in Cli. Here Cli abbreviates the fully aligned biprogram push(1) ; p := new Node(null, 2) ; p. val := 3 ; push(4). This biprogram simultaneously links the procedure bodies on left and right, and aligns the client. Using p := new Node(null, 2) enables use of a relational postcondition that says the objects are in agreement. Using push(4) enables use of push's relational specification. Like in unary RL, the proof rule for linking has two premises: one says the bodies (B|B ) satisfy their specification, the other says Cli satisfies the overall specification under the hypothesis that push satisfies its spec (see rLink in Fig. 2 ). This hypothesis context gives push a relational specification, using Ax as sugar for x = x:

Here η is the effect rw rep, size, rep'any in the original specification (5) of push. 

The specification in Φ is not simply a relational lift of push's public specification (5). Invariants I and I on internal data structures should not appear in push's API: they should be hidden, because the client should not touch the internal state on which they depend. Effects on module variables (like top) should also be hidden. This kind of reasoning is the gist of second order framing [37, 5]. The relational counterpart is a relational second order frame rule which says that any client that respects encapsulation will preserve L. Hiding is the topic of another paper, for which this one is laying the groundwork (see Section 8).
section_name: Relational Logic with Framing and

section_content: The relational assertion language is essentially syntax for a first order structure comprised of the variables and heaps of two states, together with a refperm connecting the states. 

A refperm is a type-respecting partial bijection from references allocated in one state to references allocated in the other state. For use with SMT provers, a refperm can be encoded by a pair of maps with universal formulas stating they are inverse [7]. The syntax for relations caters for dynamic allocation by providing primitives such as F = F that says the value of F in the left state equals that of F in the right state, modulo the refperm. In case of integer expressions, this is ordinary equality. For reference expressions, it means the two values are related by the refperm. For region expressions, G = G means the refperm forms a bijection between the reference set denoted by G in the left state and G in the right state (ignoring null). The agreement formula AG'f says, of a pair of states, that the refperm is total on the set denoted by G in the left state, and moreover the f -field of each object in that set has the same value, modulo refperm, as the f -field of its corresponding object in the right state. For commands that allocate, the postcondition needs to allow the refperm to be extended, which is expressed by the modal operator (read "later"): P holds if there is an extension of the refperm with zero or more pairs of references for which P holds. For example, after the assignment to p in the stack example, the relational rule for allocation yields postcondition (p = p ∧ A{p}'any). Aside from the left and right embeddings of unary predicates ( P and P ), the only other constructs are the logical ones (conjunction, implication, quantification over values). 

Let 2P = ¬ ¬P. Validity of P ⇒ 2P is equivalent to P being monotonic, i. e., not falsified by extension of the refperm. Here are some valid schemas: P ⇒ P, P ⇒ P, and (P ∧ Q) ⇒ P ∧ Q. The converse of the latter is not valid. For framing, a key property is that P ∧ Q ⇒ (P ∧ Q) is valid if Q is monotonic. In practice, is only needed in postconditions, and only at the top level. Owing to P ⇒ P, this works fine with sequenced commands. Many useful formulas are monotonic, including AG'f and F = F, but not ¬(F = F ).
section_name: Relational formulas

section_content: A biprogram CC (Fig. 1 ) represents a pair of commands, which are given by syntactic projections defined by clauses including the following: -----------------

The weaving relation has clauses including the following. 

(A|A) → A (for atomic commands A)

Commands are deterministic (modulo allocation), so termination-insensitive noninterference and equivalence properties can be expressed in a simple ∀∀ form described at the start of Section 3, rather than the ∀∃ form needed for refinement and for possibilistic noninterference ("for all runs. . . there exists a run. . . "). The transition rules for biprograms must ensure that the behavior is compatible with the underlying unary semantics, while enforcing the intended alignment. That would still allow some degree of nondeterminacy in biprogram transitions. However, we make biprograms deterministic (modulo allocation), because it greatly simplifies the soundness proofs. Rather than determinize by means of a scheduling oracle or other artifacts that would clutter the semantics, we build determinacy into the transition semantics. Whereas the syntax aligns points of interest in control flow, biprogram traces explicitly represent aligned pairs of executions. We make the arbitrary choice of left-then-right semantics for the split form. In a trace of (C|C ), every step taken by C is effectively aligned with the initial state for C. This is followed by the steps of C, each aligned with the final state of C. To illustrate the idea, here is a sketch of the trace of a split biprogram (center column) and its alignment with left and right unary traces. This pattern is also typical for "high conditionals" in noninterference proofs, where different branches may be taken (cf. rule rIf4). Here is the sync'd version in action. The relational correctness judgment has the form Φ CC :

The hypothesis context Φ maps some procedure names to their specifications: Φ(m) may be a unary specification as before or else a relational one of the form R ≈> S [ε|ε ]. Frame conditions retain their meaning, separately for the left and the right side. In case ε is the same as ε, the judgment or specification is abbreviated as

The semantics of biprograms uses small steps, which makes alignments explicit. A configuration is comprised of a biprogram, two states, and two environments for procedures. The transition relation depends on a semantic interpretation for each procedure in the hypothesis context Φ. Context calls, i. e., calls to procedures in the context, take a single step in accord with the interpretation. For the sake of determinacy, this is formalized in the semantics of relational correctness by quantifying over deterministic "interpretations" of the specifications (as in [7] ), rather than a single nondeterministic transition rule (as in [5, 37] ). 

Let us sketch the semantic consistency theorem, which confirms that executions of a biprogram from a pair of states correspond to pairs of executions of the underlying commands, so that judgments about biprograms represent relational properties of the underlying commands. Suppose Φ (C|C ) : P ≈> Q [ε|ε ] is valid and Φ has only unary specifications. Consider any states σ, σ that are related by P (modulo some refperm). Suppose C and C, when executed from σ, σ, reach final states τ, τ. (In the formal semantics, transitions are defined in terms of interpretations ϕ that satisfy the specifications Φ, so this is written C, σ ϕ -→ * skip, τ and C, σ ϕ -→ * skip, τ. ) Then τ, τ satisfy Q.
section_name: Biprograms

section_content: Selected proof rules appear in Fig. 2. 

For linking a procedure with its implementation, rule rLink caters for a client program C related to itself, in such a way that its executions can be aligned to use the same pattern of calls. The procedure implementations may differ, as in the stack example, Section 3. The rule shown here is for the special case of a single procedure, and the judgment for (B|B ) has empty hypothesis context, to disallow recursion. We see no difficulty to add mutually recursive procedures, as done for the unary logic in [5], but have not yet included that in a detailed soundness proof. The soundness proof is basically an induction on steps as in [5] but with the construction of an interpretation as in the proof of the linking rule in [7]. The general rule also provides for un-discharged hypotheses for ambient libraries used in the client and in the procedure implementations [5]. 

Rule rIf4 is the obvious rule that considers all paths for a conditional not aligned with itself (e. g., for "high branches"), whereas rIf leverages the alignment designated by the biprogram form. The disjunction rule -i. e., from Φ CC : P 0 ≈> Q [ε|ε ] and Φ CC : P 1 ≈> Q [ε|ε ] infer Φ CC : P 0 ∨ P 1 ≈> Q [ε|ε ] -serves to split cases on the initial states, allowing different weavings to be used for different circumstances, which is why there is no notion like alignment guards for the biprogram conditional. The obvious conjunction rule is sound. It is useful for deriving other rules. For example, we have this simple axiom for allocation:

x := new K : true ≈> (x = x) [wr x, rw alloc]. Using conjunction, embedding, and framing, one can add postconditions like A{x}'f and freshness of x. 

A consequence of our design decisions is "one-sided divergence" of biprograms, which comes into play with weaving. For example, assuming loop diverges, (y := 0; z. f := 0 | loop; x := 0) assigns z. f before diverging. But it weaves to (y := 0|loop); (z. f := 0|x := 0) which never assigns z. f. This biprogram's executions do not cover all executions of the underlying unary programs. The phenomenon becomes a problem for code that can fault (e. g., if z is null). Were the correctness judgments to assert termination, this shortcoming would not be an issue, but in this paper we choose the simplicity of partial correctness. Rule rWeave needs to be restricted to prevent one-sided divergence of the premise biprogram DD from states where CC in the conclusion terminates. For simplicity in this paper we assume given a termination check: terminates(P, C) means that C faults or terminates normally, from any initial state satisfying P, This is about unary programs, so the condition can be discharged by standard means. 

The relational frame rule is a straightforward extension of the unary frame rule. From a judgment Φ CC : P ≈> Q [ε|ε ] it infers Φ CC : P ∧ R ≈> Q ∧ R [ε|ε ] provided that R is framed by read effects (on the left and right) that are disjoint from the write effects in ε|ε. 

To prove a judgment Φ while E|E • P|P do CC :

the rule has three main premises: Φ

for right-only, and Φ CC :

for aligned execution. A side condition requires that the invariant Q implies these cases are exhaustive: Q ⇒ E = E ∨ (P ∧ E) ∨ (P ∧ E ). Additional side conditions require the effects to be self-immune, just as in unary RL [10, 7]. Finally, the formulas P ⇒ P and P ⇒ P must be valid; this says the alignment guards are refperm-independent, which is needed because refperms are part of the semantics of judgments but are not part of the semantics of biprograms. 

The above rule is compatible with weaving a loop body, as in (4). The left and right projections -CC and -CC undo the weaving and take care of unaligned iterations. There are many other valid and useful rules. Explicit frame conditions are convenient, both in tools and in a logic, in part because they compose in simple ways. This may lose precision, but that can be overcome using postconditions to express, e. g., that x := x does not observably write x. This is addressed, in unary RL, by a rule to "mask" write effects [10]. Similarly, the relational logic supports a rule to mask read effects. There is a rule of transitivity along these lines: from (B|C) : P ≈> Q and (C|D) : R ≈> S infer (B|D) : P; R ≈> Q; S where (; ) denotes composition of relations. A special case is where the pre-relations (resp. post-relations) are the same, transitive, relation. The rule needs to take care about termination of C.
section_name: Relational region logic

section_content: Benton [15] introduced relational Hoare logic, around the same time that Yang was developing relational separation logic [45]. Benton's logic does not encompass the heap. Yang's does; it features separating conjunction and a frame rule. Pointers are treated concretely in [45] ; agreement means identical addresses, which suffices for some low level C code. Neither work includes procedures. Beringer [18] reduces relational verification to unary verification via specifications and uses that technique to derive rules of a relational Hoare logic for programs including the heap (but not procedures). Whereas the logics of Benton, Yang, and others provide only rules for synchronized alignment of loops, Beringer derives a rule that allows for unsynchronized ("dissonant") iterations; our alignment guards are similar to side conditions of that rule. RHTT [34] implements a relational program logic in dependent type theory (Coq). The work focuses on applications to information flow. It handles dynamically allocated mutable state and procedures, and both similar and dissimilar control structures. Like the other relational logics it does not feature frame conditions. RHTT is the only prior relational logic to include both the heap and procedures, and the only one to have a procedure linking rule. It is also the only one to address any form of encapsulation; it does so using abstract predicates, as opposed to hiding [5, 37]. 

Several works investigate construction of product programs that encode nontrivial choices of alignment [38, 42, 46, 11, 12, 13]. In particular, our weaving relation was inspired by [11, 13] which address programs that differ in structure. In contrast to the 2-safety properties for deterministic programs considered in this paper and most prior work, Barthe et al. [12] handle properties of the form "for all traces. . . there exists a trace. . . " which are harder to work with but which encompass notions of refinement and continuity. Relational specifications of procedures are used in a series of papers by Barthe et al. (e. g., [14] ) for computer-aided cryptographic proofs. Sousa and Dillig [41] implement a logic that encompasses k-ary relations, e. g., the 3-safety property that a binary method is computing a transitive relation; their verification algorithm is based on an implicit product construction. None of these works address the heap or the linking of procedure implementations. Several works show that syntactic heuristics can often find good weavings in the case of similarly-structured programs not involving the heap [28, 32, 41]. Mueller et al. [32] use a form of product program and a relational logic to prove correctness of a static analysis for dependency, including procedures but no heap. 

Works on translation validation and conditional equivalence checking use verification conditions (VCs) with implicit or explicit product constructions [46, 47]. Godlin and Strichman formulate and prove soundness of rules for proving equivalence of programs with similar control structure [23]. They use one of the rules to devise an algorithm for VCs using uninterpreted functions to encode equivalence of called procedures, which has been implemented in two prototype tools for equivalence checking [24]. (Pointer structures are limited to trees, i. e., no sharing. ) Hawblitzel et al. [25] and Lahiri et al. [29] use relational procedure summaries for intra-and inter-procedural reasoning about program transformations. The heap is modeled by maps. These and related works report good experimental results using SMT or SAT solvers to discharge VCs. Felsing et al. [21] use Horn constraint solving to infer coupling relations and relational procedure summaries, which works well for similarly structured programs; they do not deal with the heap. The purpose of our logic is not to supplant VC-based tools approaches but rather to provide a foundation for them. Our biprograms and relational assertions are easily translated to SMT-based back ends like Boogie and Why3. Amtoft et al. [2] introduce a logic for information flow in object-based programs, using abstract locations to specify agreements in the heap. It was proposed in [8] to extend this approach to more general relational specifications, for fine-grained declassification policies. Banerjee et al. [9] showed how region-based reasoning including a frame rule can be encoded, using ghost code, with standard FOL assertions instead of an ancillary notion of abstract region. This evolved to the logic in Section 6. 

Relational properties have been considered in the context of separation logic: [19] and [43] both give relational interpretations of unary separation logic that account for representation independence, using second order framing [19] or abstract predicates [43]. Extension of this work to a relational logic seems possible, but the semantics does not validate the rule of conjunction so it may not be a good basis for verification tools. Tools often rely heavily on splitting conjunctions in postconditions. 

Ahmed et al. [1] address representation independence for higher order code and code pointers, using a step-indexed relational model, and prove challenging instances of contextual equivalence. Based on that work, Dreyer et al. [20] formulate a relational modal logic for proving contextual equivalence for a language that has general recursive types and general ML-style references atop System F. The logic serves to abstract from details of semantics in ways likely to facilitate interactive proofs of interesting contextual equivalences, but it includes intensional atomic propositions about steps in the transition semantics of terms. Whereas contextual equivalence means equivalent in all contexts, general relational logics can express equivalences conditioned on the initial state. For example, the assignments x := y. f and z. f := w do not commute, in general, because their effects can overlap. But they do commute under the precondition y = z. We can easily prove equivalence judgments such as (x := y. f ; z. f := w | z. f := w; x := y. f ) : B(y = z) ∧ A{y}'f ∧ w = w ≈> x = x ∧ A{z}'f. By contrast with [1, 34], we do not rely on embedding in higher-order logic.
section_name: Related work

section_content: We provide a general relational logic that encompasses the heap and includes procedures. It handles both similarly-and differently-structured programs. We use small-step semantics with the goal to leverage, in future work, our prior work on SMT-friendly heap encapsulation [40, 5, 7] for representation independence, which is not addressed in prior relational logics. 1 s articulated long ago by Hoare [26] but never fully formalized in a logic of programs, reasoning about change of data representation is based on simulation relations on encapsulated state, which are necessarily preserved by client code in virtue of encapsulation. For functional correctness this corresponds to "hiding" of invariants on encapsulated data, i. e., not including the invariant in the specification used by a client. O'Hearn et al. [37] formalize this as a hypothetical or second order framing rule (which has been adapted to RL [5] ). In ongoing work, the logic presented here has been extended to address encapsulation and provides a relational second order frame rule which embodies Reynolds' abstraction theorem [39]. Whereas framing of invariants relies on write effects, framing of encapsulated relations also relies on read effects. Our ongoing work also addresses observational purity, which is known to be closely related to representation independence [26, 36]. 

Although we can prove equivalence for loop tiling, some array-oriented loop optimizations seem to be out of reach of the logic as currently formulated. Loop interchange changes F S T T C S 2 0 1 6
section_name: Conclusion

section_content: Relational Logic with Framing and matrix row to column order, reordering unboundedly many atomic assignments, as does loop fusion/distribution. Most prior work does not handle these examples; [47] does handle them, with a non-syntactic proof rule that involves permutations on transition steps, cf. [33].
section_name: 11:14

section_content: * A. Banerjee was partially supported by the U. S. National Science Foundation (NSF). D. A. Naumann and M. Nikouei were partially supported by NSF award 1228930. Any opinion, findings, and conclusions or recommendations expressed in the material are those of the authors and do not necessarily reflect the views of NSF.