The Hoare chapters have developed a logical framework for program verification based on Hoare logic.

• On the one hand, a Hoare triple {{P}} c {{Q}} posits that a program c satisfies the specification given by precondition P and postcondition Q.
• On the other, the rules of the logic allow us to formally prove valid Hoare triples.

So Hoare logic lets us state and prove formally properties of programs. These properties relate the initial and final states of an execution. The ability to reason about programs written in languages of our choice is very useful! But there are many useful properties that can't be expressed using Hoare logic. In this chapter we begin to explore what are these richer properties and how to formally reason about them. The first thing to note is that Hoare triples talk about a single execution of a given program, but we're often interested in properties that can only be expressed in terms of multiple executions.

• A fundamental property of this kind is determinism, which states that the final state obtained by running a program c is uniquely determined by the initial state:
  st =[ c ]=> st₁' → st =[ c ]=> st₂' → st₁' = st₂'
  Clearly, we need to run a program twice with the same initial state before we can check the equality of the final states. So this property cannot be expressed in Hoare logic.
  In the case of Imp, the language itself is deterministic, as we proved in the Imp chapter of Logical Foundations, so this always holds in our simple setting.

• Many common properties follow a similar pattern. For instance, we can define that a computation c is monotonic with respect to the value of some variable X as follows:
  st₁ X ≤ st₂ X → st₁ =[ c ]=> st₁' → st₂ =[ c ]=> st₂' → st₁' X ≤ st₂' X
  For example, the command X := X + 42 is monotonic in X.
• Finally, as explained in Noninterference.v, confidentiality is commonly expressed as a property called noninterference.
  Simply stated, in our setting, we can divide the variables of a program as either public or secret. A public observer can only inspect the values of public variables, not secret ones.
  A program is noninterferent if, when it runs from a pair of states with equal public variables, those public variables remain equal in the pair of final states (assuming both runs terminate). We formally defined this as follows in Noninterference.v:

Definition noninterferent_while pub c := ∀ s₁ s₂ s₁' s₂',
  pub_equiv pub s₁ s₂ →
  s₁ =[ c ]=> s₁' →
  s₂ =[ c ]=> s₂' →
  pub_equiv pub s₁' s₂'. Again, noninterference requires reasoning about how the program states vary between two program executions. So noninterference cannot be expressed in Hoare logic. A second important observation is that Hoare triples don't help us relate the behaviors of different commands. Even for showing noninterference, where we start with a single program, we often still need to relate different parts of the program to each other, but this is not something we can properly do with Hoare logic. Another case where we would like to formally relate the behavior of different programs is proving program equivalence, for instance for showing the correctness of program transformations. Again, this is not something we can properly do with Hoare logic. So far, the Imp and Equiv chapters have presented some small arithmetic optimizations and proved directly from the semantics that optimized programs behave exactly like the originals. We could prove these transformations correct directly from the semantics because they were very simple. In particular, our language of arithmetic expressions includes an evaluation function and properties about this function were relatively easy to prove, and they lifted trivially to commands. For verifying the correctness of less trivial transformations of commands, which are stateful and can loop, Relational Hoare Logic will generally work much better than the operational semantics. Moreover, Relational Hoare Logic will allow us to specify and prove more flexible notions of program equivalence. The Equiv chapter introduces a notion of program equivalence that lets us relate different programs when they "behave exactly the same." But this is too restrictive in practice. Take the Imp program that swaps the values of variables X and Y using an auxiliary variable, here Z.

The program that swaps the values of X and Y using arithmetic operations intuitively achieves the same thing.

However, these two programs are not equivalent with respect to the restrictive program equivalence notion from Equiv:

• In the first program, the final value of Z equals the initial value of X.
• In the second program, the value of Z does not change.

The problem is that the restrictive notion of program equivalence from Equiv doesn't allow any variables to differ in the final states, even if we may intuitively not care about the final values of some auxiliary variables (like Z above). Even simpler transformations, like renaming the auxiliary variable (here, W instead of X, are enough to invalidate program equivalence.

To compare different programs and have anything meaningful to say about them, we're going to need more general and flexible tools. So a natural question is how to generalize Hoare logic to state and prove properties that relate two executions, each possibly of a different program. Relational Hoare Logic (commonly RHL) is an inference system that achieves just this. In this chapter, we build and use this logic for Imp, based on what we learned from the Hoare chapters. The literature has different versions of the RHL rules, some quite complex, but in this chapter we stick to a relatively simple version.

Relational Assertions

In the relational setting, an assertion is a logical property of two states (of two potentially different programs).

In other words, it is a binary relation between states. (Binary relations are discussed in more detail in the Rel optional chapter of Logical Foundations.) Basic assertions work much like they did in Hoare Logic. For example,

• fun st₁ st₂ ⇒ True holds for every two states, and
• fun st₁ st₂ ⇒ False holds for no two states, as before.
• fun st₁ st₂ ⇒ st₁ X = 3 holds when the value of X in the first state is 3,
• fun st₁ st₂ ⇒ st₂ Y = 5 holds when the value of Y in the second state is 5, and
• fun st₁ st₂ ⇒ st₁ X = 3 ∧ st₂ Y = 5 holds when the value of X in the first state is 3 and the value of Y in the second state is 5,

More interestingly, now we can write relational assertions that connect the contents of the two states to each other in a more direct way:

• fun st₁ st₂ ⇒ st₁ X = st₂ X holds when the value of variable X is the same in the two executions.
  We will use such equality assertions to specify that a program is noninterferent and that two programs are equivalent. For instance, for specifying that two versions of swap are equivalent we will use the following relational assertion: fun st₁ st₂ ⇒ st₁ X = st₂ X ∧ st₁ Y = st₂ Y.
• fun st₁ st₂ ⇒ st₁ X ≤ st₂ X holds when the value of X in the first execution is smaller than the value of X in the second execution. We will use this in the precondition and postcondition to define that a command is monotonic in X.

Notations for Relational Assertions

As in the Hoare chapter, we introduce Coq notations to write more readable assertions, as in pen and paper proofs. The key difference is that, in a relational assertion, each reference to a variable must refer explicitly to one of the two program states. We will write X.1 to refer to the value of X in the first state, and X.2 to refer to the value of X in the second state.

• X.1 = 3 ∧ Y.2 = 5
• X.1 = X.2
• X.1 = X.2 ∧ Y.1 = Y.2
• X.1 ≤ X.2

We try to keep notations as close as possible to those used for Hoare logic, but separated in a dedicated scope of their own. Implications look exactly as they did before.

As usual, coercions and annotation scopes are used to lift the various types of expressions to the level of relational assertions. We need to be a bit more careful now when treating arithmetic expressions, as we need to ensure that they're evaluated in the right state. There are now two ways to evaluate an expression, either in the first state or in the second state. This distinction needs to be made explicitly: a simple coercion couldn't decide which way to go!

Relational Judgments, Informally

A Hoare triple was a statement involving three parts (precondition, command and postcondition), and this becomes a "quadruple" in the relational world:

• The precondition and the postcondition remain but become relational assertions.
• Those now apply to two commands instead of one.

We will call these relational judgments or simply judgments, and write them like so:
      ⊢ c₁ ~~ c₂ : P ⇒ Q The interpretation of a judgment is a direct extension of that of Hoare triples:

• If initial states s₁ and s₂ together satisfy the relational precondition P,
• and if c₁ runs from s₁ and eventually terminates in some state s₁',
• and if c₂ runs from s₂ and eventually terminates in some state s₂',
• then the final states s₁' and s₂' together satisfy the relational postcondition Q.

Let's return to some of the examples we discussed above and encode them as relational judgments.

• We can state that command X := X + 42 is monotonic in the variable X as follows:
  ⊢ X := X + 42 ~~ X := X + 42 : (X.1 <= X.2) => (X.1 <= X.2)
• We can state that swap_aux and swap_arith are equivalent:
          ⊢ swap_aux ~~ swap_arith : (X.1 = X.2 ∧ Y.1 = Y.2) ⇒
                                      (X.1 = X.2 ∧ Y.1 = Y.2) Here we have the flexibility to ignore all variables other than X and Y, which can be used as auxiliaries, but which don't store the arguments and result of the commands.

Now consider the following command (taken from Noninterference.v):

If we assume that variable X is public and variable Y is secret, we can state noninterference for secure_com as follows:
        ⊢ secure_com ~~ secure_com : (X.1 = X.2) ⇒ (X.1 = X.2) As usual for noninterference, we assume that the public variables are equal in the precondition, and prove that the public variables are still equal after executing the command by encoding this in the postcondition.

Relational Judgments, Formally

Let us now formalize what it means for a relational judgment to be valid, that is, for the pair of programs to satisfy the specification given by the relational pre- and postconditions:

Using this we can formalize all the statements above in a very direct way:

Proof Rules

The structure of non-relational program logics like Hoare logic is rather simple:

• Each syntactic construction of the language (assignments, conditionals, etc.) has an associated proof rule.
• A small number of structural rules help with logical manipulations.

In this way, proofs closely follow the structure of the programs being analyzed. In a relational setting, things get more complicated because in general we're trying to connect two programs that structurally may be similar or they may be different. Like Hoare logic, RHL is structured as a collection of inference rules. We can divide these into three main groups:

• Two-sided rules for each syntactic form of the language, when the same form appears at the same point in both programs.
• One-sided rules, also for each syntactic form, when we need to look at one of the two programs and leave the other unchanged.
• Structural rules for program transformation and spec manipulation.

Very roughly speaking, two-sided rules are used to relate syntactically similar programs (e.g, for noninterference or monotonicity we start with the same program on both sides). One-sided rules are used to relate dissimilar programs (e.g., like swap_aux and swap_arith above, or like mult_simple and mult_iter).

Skip

To begin with, two programs that don't do anything trivially preserve any relational assertions between their states.

	(rhoare_skip)
⊢ <{skip}> ~~ <{skip}> : P => P

Formally:

Consequence

As in Hoare logic, we need structural rules to manipulate the pre- and postconditions of a pair of commands. These fill the gaps between the relational assertions we have and the ones needed by one- and two-sided rules.

The combined rule of consequence puts together relational assertion implications on both precondition and postcondition.

Assignment

To formalize the relational rules for assignment, we need to extend assertion substitution to relational assertions. In the same way that we evaluate arithmetic expressions inside relational assertions, a substitution takes place either in the first memory or in the second memory. Our operations make this choice explicit.

We also redefine one of our automation tactics from Hoare2, this time specialized for unfolding rassert_implies, assn_sub_1, and assn_sub_2.

Using the new substitution operations, we can define the two-sided proof rule for assignment:

	(rhoare_asgn)
⊢ <{X1 := a1}> ~~ <{X2 := a2}> :
(Q [X1.1 ⊢> a1] [X2.2 ⊢> a2]) => Q

Formally:

This two-sided rule is all we need to prove monotonicity of the "add42" command:

The two-sided assignment rule is, perhaps, more general than we might have expected. Specifically, it doesn't require us to assign a value to the same variable on both sides. In fact, we're always able to take an arithmetic expression and substitute it for any instances of a variable in a relational assertion. If one of the variables belongs to the first program and the other to the second program, the two assignments are necessarily independent. This suggests several possibilities for one-sided rules. One of them is to combine an assignment and a skip into a sort of specialized two-sided rule without any additional premises.

We will see more interesting examples below, but for now we can use rhoare_asgn_1 to prove that the command X := X is equivalent to skip.

Above we stated program equivalence only looking at the value of variable X, but we can strengthen this to look at the values of all variables (basically obtaining a termination-insensitive version of cequiv from Equiv):

Sequencing

The two-sided sequencing rule for RHL is an extension of the Hoare sequencing rule: run the first pair of commands from the initial precondition to an intermediate assertion, then the second pair of commands from that assertion to the postcondition.

⊢ c1 ~~ c2 : P => Q
⊢ d1 ~~ d2 : Q => R	(rhoare_seq)
⊢ <{c1; d1}> ~~ <{c2; d2}> : P => R

Formally:

We can use this two-sided sequencing rule to relate two programs in lock-step. For instance for proving noninterference of secure_com we relate each assignment to itself:

Alignment: Skip Consuming and Padding

Now we can begin to introduce one-sided rules that leave one of the two programs in a relational judgment untouched. Because we want to be able to relate programs with different control structures, we need to go beyond the simple two-sided rules, which closely resemble those of standard Hoare logic. Otherwise, we'll end up with a weak logical system. In particular, we need rules that allow us to manipulate the alignment of which commands of one program we want to match to which commands of the other. These make up an essential part of any moderately complex proofs in RHL. skip; skip and skip For this task, the sequencing operator will be our fulcrum. We can start by stating and proving one-sided rules for skip. These rules will unilaterally consume a skip command on one side, and leave the other unchanged. skip doesn't modify the state of its program and trivially preserves all assertions. Starting with the left program:

⊢ c1 ~~ c2 : P => Q	(rhoare_skip_seq_1)
⊢ <{skip; c1}> ~~ c2 : P => Q

⊢ c1 ~~ c2 : P => Q	(rhoare_seq_skip_1)
⊢ <{c1; skip}> ~~ c2 : P => Q

Formally:

Here is a simple example using this rule:

And similarly for the right side:

⊢ c1 ~~ c2 : P => Q	(rhoare_skip_seq_2)
⊢ c1 ~~ <{skip; c2}> : P => Q

⊢ c1 ~~ c2 : P => Q	(rhoare_seq_skip_2)
⊢ c1 ~~ <{c2; skip}> : P => Q

Formally:

We can be more general if we replace skip command with an arbitrary command related to a skip on the other side, and chain intermediate assertions as usual.

Here is a simple example using these rules to remove a dead store and relate the live stores to each other:

We also use rules rhoare_seq_1 and rhoare_seq_2 when we want to relate commands that are syntactically dissimilar and we only want to separately reason about their effects on the state, as we were doing in Hoare logic. Note that the two-sided skip rule can be used to finish a derivation by consuming two lined-up "empty" programs. By contrast, one-sided rules can't be used to completely discharge a proof obligation, because one of the two programs always remains unfinished. If we need to, we can also add skips to ease the task of aligning program structures.

Conditionals

To model conditional statements, once again we need to lift boolean expressions to the language of assertions. Here, as in the case of arithmetic expressions, we'll need to state explicitly in which of the two memories we intend to evaluate each expression.

We also update our automation tactic to unfold bassn_1, bassn_2, etc.

The basic relational rule for conditionals resembles its Hoare logic counterpart: the spec of the joint conditional is satisfied if each of the branches satisfies it. As before, the proof of the spec for each branch is extended with corresponding assumption about the evaluation of the guard condition. The difference now is that we have two conditions, not one! How do we account for this in a two-sided rule? The simplest two-sided rule for conditionals considers the case where the control flow of both conditionals is in lockstep. That is, the guard conditions are equivalent in their evaluation context. In this case, either the two then branches or the two else branches are taken.

⊢ t1 ~~ t2 : (P /\   b1!1 /\   b2!2) => Q
⊢ e1 ~~ e2 : (P /\ ~ b1!1 /\ ~ b2!2) => Q	(rhoare_if)
⊢ <{if b1 then t1 else e1 end}> ~~
<{if b2 then t2 else e2 end}> :
(P /\ (b1!1 <-> b2!2)) => Q

We can formalize this rule and prove it.

The two-sided rules for conditionals is useful for proving noninterference of programs that branch on public information, and where the two conditionals will execute in lockstep. For instance, assume that X and Y are public variables, and Z is a secret variable, then we can prove the following program p₁ is noninterferent:

The one-sided rules for conditionals relate a conditional to an arbitrary command by relating that command to each of the branches of the conditional under appropriate conditions.

The one-sided rules for conditionals allow us to reason about programs that branch on secrets, so the two conditionals will *not* run in lockstep. For instance, assuming that variable X is public and variable Y is secret then the following program p₂ is noninterferent:

Intuitively, even if this program branches on the secret Y, it always assigns the value 0 to X, so no secret is leaked. To prove this we use the one-sided rules for conditionals to consider all the ways in which the two conditionals could execute (then-then, then-else, else-then, and else-else). This goes beyond what the simple type systems we will consider in this course can analyze (they will reject this noninterferent program as potentially insecure).

When the value of a branch condition can be statically known, we can use this fact to simplify the inference rules. Let's consider the one-sided versions of this.

While Loops

The rules for while extend loop invariants to relate the execution of the two programs. Here we will consider the two-sided rule where both loops iterate in lockstep. That is, whenever one loop iterates, so does the other, so they perform the same number of iterations. In proof terms, this means that:

• The loop conditions agree before entering (or not) the loops, as well as after each iteration.
• Both loop conditions are satisfied at the beginning of each iteration.
• Both loop conditions are false when the loops end.

Because the loops execute in lockstep, this rule looks similar to its Hoare logic counterpart, with added conditions to enforce synchronicity.

⊢ c1 ~~ c2 : (P /\ b1!1 /\ b2!2) => (P /\ (b1!1 <-> b2!2))	(rhoare_while)
⊢ <{while b1 do c1 end}> ~~ <{while b2 do c2 end}> :
(P /\ (b1!1 <-> b2!2)) => (P /\ ~ b1!1 /\ ~ b2!2).

Where P is the loop invariant. Formally:

One-sided rules where a loop is matched to a skip are straightforward and very similar to the original Hoare logic rules.

A more interesting problem is what happens when we want to relate the computations carried out by two loops, but where the loops don't iterate in lockstep. Consider the following examples:

To prove properties of programs like these, we need rules with additional "knobs," for example letting us characterize:

• When the two loops perform an iteration in lockstep.
• When the first loop performs an iteration while the second loop waits for it.
• When the second loop performs an iteration while the first loop waits for it.

To Know More

Relational Hoare logic was introduced by Benton in his classic POPL paper. EasyCrypt is a proof assistant based on a probabilistic version of relational Hoare logic. The literature has different versions of the RHL rules, some quite complex, but in this chapter we presented a relatively simple version.