An introduction to Program Logics

So far, we've seen ways to reason about programs, by defining the program itself as an object in Coq and giving it operational semantics (big or small-step). Program logics are another way to reason about the execution of programs, not by describing how the programs compute, but by using logical rules that describe the properties satisfied by a program. A traditional program logic is called Hoare logic, and has spawned many extensions (such as separation logic).

In Hoare Logic, we're going to prove Hoare triples, properties that look like {P} c {Q}, meaning that if we execute the program c from a state satisfying property P (the precondition), we end up in a state satisfying property Q (the postcondition). More on these triples later.

To define Hoare Logics, we then need to define two languages, one for our programs and one for our properties (P and Q). Today, for the programs, we'll look at an imperative programming language, that can manipulate a heap (so it will be a bit different from the Imp language we've seen before). But for a change, we're not going to define programs the same way as before. This time, we'll go for a shallow embedding, meaning that we will describe our programs with equivalent Coq functions.

Shallow VS Deep Embeddings

So far, what we used to study a language is Coq was the following approach. We defined a new custom datatype representing the programs. To execute our programs, we wrote an interpreter, a Coq function manipulating this program datatype. To give semantics to our programs, we defined operational semantics statements, in big or small step style. This approach is called a deep embedding of the language.

To show you another approach, today we'll explore using a shallow embedding for our programs. In a shallow-embedding, our programs are simply going to be encoded as Coq functions. To execute our programs, we can then simply compute them within Coq, using something like Compute. Their semantics is now defined by whatever the Coq function does.

This means we reuse the metalanguage of Coq to build the constructs of our language. With shallow embedding, we inherit all the strengths and weaknesses of the metalanguage. For example, we can't write down general non-terminating functions directly because that's not part of Gallina. On the other hand, we get dependent types and all the other machinery of Coq.

Imperative Programming in Coq

In order to do this shallow embedding, let's take a look at the language we want to define. We want programs that manipulate a heap. The heap associates a value to some pointers that have been allocated. So the programming language should include commands like new to allocate a pointer, free to remove one, or read and write to manipulate the data stored on the heap.

In our language, each command will return a value (it can be a unit value for commands like write). An commands can be chained together, passing the returned value of the first command to the next one.

But how can we do a shallow embedding of these programs if Coq functions are pure functional programs with no control over the heap? One solution in functional programming languages is to use monads. We'll take a look at a state-and-error monad, allowing us to represent programs that can manipulate a global state (the heap) and fail (for instance, reading an unallocated pointer) in a pure functional language.

The development below builds a module that is parameterized by some universe of values that we can store in the heap, and then later instantiate the universe with a type of my choice. In the module, we will define basic notions of a heap, of commands as a monad which manipulates heaps, and appropriate Hoare-logic rules for reasoning about these commands.

Module Type UNIVERSE.
  Parameter t : Type.
End UNIVERSE.

Module FunctionalIMP (U : UNIVERSE).

We will model pointers using nats, but any type that provides an equality and way to generate a fresh value would do.

  Definition ptr := nat.
  Definition ptr_eq_dec := eq_nat_dec.
  Definition ptr_le_gt_dec := le_gt_dec.

We will model heaps as lists of pointers and values drawn from the universe.

  Definition heap := list (ptr * U.t).

We model commands of type t as functions that take a heap and return an optional pair of a heap and a t. So this is really a combination of the state and option monad.

  Definition Cmd (t : Type) := heap -> option (heap * t).

To put it simply, commands are Coq functions that take as an argument the initial heap, and produce either None, meaning that the program has failed, or Some new heap and returned value, meaning that the program has successfully terminated and might have modified the heap.

  Declare Scope cmd_scope.

Now let's define two natural functions that let us chain together commands (bind) and simply return value witout changing the heap (ret).

  Definition ret t (x : t) : Cmd t := fun h => Some (h, x).
  Definition bind t u (c : Cmd t) (f : t -> Cmd u) : Cmd u :=
    fun h1 =>
      match c h1 with
      | None => None
      | Some (h2,v) => f v h2
      end.

Here is some notation to approximate Haskell's "do" notation.

  Notation "x <- c ; f" := (bind c (fun x => f))
    (right associativity, at level 84, c at next level) : cmd_scope.
  Notation "c ;; f" := (bind c (fun _ : unit => f))
    (right associativity, at level 84) : cmd_scope.
  Local Open Scope cmd_scope.

We can provide a run command for the monad, which starts executing the command from an empty heap.

  Definition run (t : Type) (c : Cmd t) := c nil.

Here are a few examples of programs

  Definition c1 := ret 0.
  Compute run c1.
= Some (nil, 0)
: option (heap * nat)
  Definition c2 := x <- ret 0; y <- ret 1; ret (x + y).
  Compute run c2.
= Some (nil, 1)
: option (heap * nat)

We can model failures similar to throwing an exception.

  Definition exit t : Cmd t := fun h => None.

Exercise: Let's define a simplistic error handler

  Definition try_catch t (c : Cmd t) (e : Cmd t) : Cmd t :=
    fun h =>
      match c h with
      | Some p => Some p
      | None => e h
      end.

Allocation -- to allocate a fresh location, we run through the heap and find the biggest pointer, and simply return the next biggest pointer. Another good homework is to change the definitions here to carry along the "next available pointer" as part of the state of the system.

  Definition max (p1 p2 : ptr) :=
    if ptr_le_gt_dec p1 p2 then p2 else p1.

  Fixpoint max_heap (h : heap) :=
    match h with
    | nil => 0
    | (p, _) :: rest => max p (max_heap rest)
    end.

  Fixpoint insert (h : heap) (x : ptr) (v : U.t) : heap :=
    match h with
    | nil => (x, v) :: nil
    | (y, w) :: h' =>
        if ptr_le_gt_dec x y then (x, v) :: (y, w) :: h'
        else (y, w) :: (insert h' x v)
    end.

The new u command allocates a new location in the heap, initializes it with the value u, and returns the pointer to the freshly-allocated location.

  Definition new (u : U.t) : Cmd ptr :=
    fun h => let p := 1 + max_heap h in Some (insert h p u, p).

The lookup h p command looks up pointer p in the heap h, returning the value associated with it if any.

  Fixpoint lookup (h : heap) (p : ptr) : option U.t :=
    match h with
    | nil => None
    | (p', u') :: rest =>
        if ptr_eq_dec p p' then Some u'
        else lookup rest p
    end.

The read p command looks up pointer p and returns the value if any, and fails if there is no value present. It leaves the heap unchanged.

  Definition read (p : ptr) : Cmd U.t :=
    fun h => match lookup h p with
             | None => None
             | Some u => Some (h, u)
             end.

The remove h p command removes the pointer p from the heap h, returning a new heap.

  Fixpoint remove (h : heap) (p : ptr) : heap :=
    match h with
    | nil => nil
    | (p', u') :: h =>
        if ptr_eq_dec p p' then remove h p
        else (p', u') :: (remove h p)
    end.

To write u into the pointer p, we first check that p is defined in the heap, and then remove it, and add it back with the value u.

  Definition write (p : ptr) (u : U.t) : Cmd unit :=
    fun h => match lookup h p with
             | None => None
             | Some _ => Some (insert (remove h p) p u, tt)
             end.

To free the pointer p, we simply remove it from the heap. Again, this will fail if p wasn't in the heap to begin with.

  Definition free (p : ptr) : Cmd unit :=
    fun h => match lookup h p with
             | None => None
             | Some _ => Some (remove h p, tt)
             end.

Hoare Logic

Now that we have a shallow-embedding of our programming language, we're ready to define Hoare Logic rules to reason about programs. Note however that our definitions are going to differ from the standard Hoare Logic definitions you can see in other lectures, for two reasons. First, we have this shallow embedding of our programs (and as we'll see later, of the language of properties). Second, we'll look into total correctness Hoare triples, instead of the more common partial correctness ones.

A partial correctness triple, {P} c {Q}, holds when: if we run c from a state where P holds AND c terminates without failing, then we end up in a state where Q holds. A total correctness triple, {{P}} c {{Q}} holds when: if we run c from a state where P holds, THEN c terminates without failing and we end up in a state where Q holds. Since here we don't have non-terminating programs, it should be easier to prove total correctness triples.

The idea of Hoare logic is to define rules to deduce Hoare triples. Of course, each program may have several valid Hoare triples. For instance, {x=2} x:=x+3 {x=5} is valid, but so is {False} x:=x+3 {True}. Here, we'll try to define valid triples where the precondition is as weak as possible, and the postcondition is as strong as possible (these triples imply other, less general triples, see below).

Before we start our definitions, let's look at the standard, partial correctness rules, for the standard Imp language. For a full formalisation of the standard partial correctness triples for a deep embedding of Imp, you can refer to https://softwarefoundations.cis.upenn.edu/plf-current/Hoare.html

(*


--------------------  (skip)
{ P } skip { P }


 { P } c1 { Q }
 { Q } c2 { R }
----------------------  (seq)
{ P } c1;c2 { R }


---------------------------- (assign)
 {Q [X |-> a]} X := a {Q}


       {P'} c {Q'}
          P ->> P'
          Q' ->> Q
-----------------------------   (consequence)
       {P} c {Q}


      {I /\ b} c {I}
--------------------------------- (while)
{I} while b do c end {I /\ ~b}

*)

The rule for assign can be a bit counter-intuitive, but you'll quickly see on some examples that substitution has to be done on the precondition. The consequence rule shows that some triples imply others, whenever we have a weak precondition and a strong postcondition. In the rule for the while, the property I is called an invariant of the loop.

Now, we'll revisit these definitions, but adapt them for several reasons. One, our progamming language is different from Imp. Second, our use of the shallow-embedding will change some definitions. Finally, we'll look at total correctness instead of partial correctness.

Now that we've defined a language of commands, we can define a logic for reasoning about commands.

A Hoare Logic proposition hprop is just a Coq function from heap to Prop.

  Definition hprop := heap -> Prop.

The Hoare Total-Correctness Triple {{P}} c {{Q}} holds when: if we run c in a heap h satisfying P, we get back a heap h' and value v, satisfying Q h v h'.

  Definition hoare_tc_triple (t : Type)
    (P : hprop) (c : Cmd t) (Q : heap -> t -> hprop) : Prop :=
    forall h, P h ->
              match c h with
              | None => False
              | Some (h', v) => Q h v h'
              end.

A boilerplate simplification tactic.

  Ltac smash :=
    unfold hprop, hoare_tc_triple, bind, max, free, read, write in *;
    intros;
    repeat
      (match goal with
       | [ H : _ /\ _ |- _] => destruct H
       | [ H : (_ * _)%type |- _] => destruct H
       | [ H1 : forall _, ?P1 _ -> _, H2 : ?P1 ?h |- _] =>
           generalize (H1 h H2); clear H1; intros
       | [ H1 : forall _ _ _, ?P1 _ _ -> _, H2 : ?P1 ?x ?h |- _] =>
           generalize (H1 _ _ _ H2); clear H1; intros
       | [ H : match ?e with | Some _ => _ | None => _ end |- _ ] =>
           destruct e
       | [ |- context[ptr_eq_dec ?x ?y] ] =>
           destruct (ptr_eq_dec x y); subst
       | [ H : context[ptr_le_gt_dec ?x ?y] |- _ ] =>
           destruct (ptr_le_gt_dec x y); subst
       | [ |- _ /\ _ ] => split
       | [ H : exists _, _ |- _] => destruct H
       | [ H : Some ?x = Some ?y |- _ ] => inversion H; clear H; subst
       | _ => assert False; [contradiction | lia]
       end);
    subst; simpl in *; try firstorder; auto with arith.

A heap h always satisfies the predicate top.

  Definition top : hprop := fun _ => True.

The Hoare-rule for return: We can run the command in any initial state and end up in a state where the heap is unchanged, and the return value is equal to the value we passed in. This is pretty obviously the weakest precondition needed to ensure the command won't fail, and the strongest post-condition we can show about the resulting state.

  Lemma ret_tc (t : Type) (v : t) :
    {{ top }} ret v {{ fun h x h' => x=v /\ h=h' }}.
t: Type
v: t
{{top}} ret v
{{fun (h : heap) (x : t) (h' : heap) =>
  x = v /\ h = h'}}
  Proof.
t: Type
v: t
{{top}} ret v
{{fun (h : heap) (x : t) (h' : heap) =>
  x = v /\ h = h'}}
    smash.
  Qed.

An alternative, more conventional rule. I don't like this because it forces me to come up with a predicate -- i.e., we can only use it in a context where P is already known.

  Lemma ret_tc' (t : Type) (v : t) (P : t -> hprop) :
    {{ P v }} ret v {{ fun _ x => P x }}.
t: Type
v: t
P: t -> hprop
{{P v}} ret v {{fun (_ : heap) (x : t) => P x}}
  Proof.
t: Type
v: t
P: t -> hprop
{{P v}} ret v {{fun (_ : heap) (x : t) => P x}}
    smash.
  Qed.

The rule of consequence: we can strengthen the pre-condition (i.e., require more before executing), and weaken the post-condition (i.e., ensure less.)

  Lemma consequence_tc
        {t : Type} {c : Cmd t} {P1 P2 : hprop}
        {Q1 Q2 : heap -> t -> hprop} :
    {{ P1 }} c {{ Q1 }} ->
    (forall h, P2 h -> P1 h) ->
    (forall h x h', Q1 h x h' -> Q2 h x h') ->
    {{ P2 }} c {{ Q2 }}.
t: Type
c: Cmd t
P1, P2: hprop
Q1, Q2: heap -> t -> hprop
{{P1}} c {{Q1}} ->
(forall h : heap, P2 h -> P1 h) ->
(forall (h : heap) (x : t) (h' : heap),
 Q1 h x h' -> Q2 h x h') -> {{P2}} c {{Q2}}
  Proof.
t: Type
c: Cmd t
P1, P2: hprop
Q1, Q2: heap -> t -> hprop
{{P1}} c {{Q1}} ->
(forall h : heap, P2 h -> P1 h) ->
(forall (h : heap) (x : t) (h' : heap),
 Q1 h x h' -> Q2 h x h') -> {{P2}} c {{Q2}}
    smash.
  Qed.

Some helpful lemmas about max and lookup.

  Lemma max_zero : forall n, max 0 n = n.
forall n : ptr, max 0 n = n
  Proof.
forall n : ptr, max 0 n = n
    induction n; auto.
  Qed.

  Lemma lookup_max h : forall n, n > max_heap h -> lookup h n = None.
h: heap
forall n : nat, n > max_heap h -> lookup h n = None
  Proof.
h: heap
forall n : nat, n > max_heap h -> lookup h n = None
    induction h; simpl; intros; smash.
p: ptr
t: U.t
h: list (ptr * U.t)
IHh: forall n : nat, n > max_heap h -> lookup h n = None
l: p <= max_heap h
H: p > max_heap h
Some t = None
p: ptr
t: U.t
h: list (ptr * U.t)
IHh: forall n : nat, n > max_heap h -> lookup h n = None
g: p > max_heap h
H: p > p
Some t = None
p: ptr
t: U.t
h: list (ptr * U.t)
IHh: forall n : nat, n > max_heap h -> lookup h n = None
n: nat
g: p > max_heap h
H: n > p
n0: n <> p
lookup h n = None
    -
p: ptr
t: U.t
h: list (ptr * U.t)
IHh: forall n : nat, n > max_heap h -> lookup h n = None
l: p <= max_heap h
H: p > max_heap h
Some t = None lia.
    -
p: ptr
t: U.t
h: list (ptr * U.t)
IHh: forall n : nat, n > max_heap h -> lookup h n = None
g: p > max_heap h
H: p > p
Some t = None lia.
    -
p: ptr
t: U.t
h: list (ptr * U.t)
IHh: forall n : nat, n > max_heap h -> lookup h n = None
n: nat
g: p > max_heap h
H: n > p
n0: n <> p
lookup h n = None apply IHh.
p: ptr
t: U.t
h: list (ptr * U.t)
IHh: forall n : nat, n > max_heap h -> lookup h n = None
n: nat
g: p > max_heap h
H: n > p
n0: n <> p
n > max_heap h lia.
  Qed.
  Hint Resolve lookup_max : core.

The new u command can be run in any initial state h, and results in a state (p,u) :: h where p is fresh. The freshness is captured by the fact that lookup h p = None, i.e., the pointer was unallocated in the pre-state.

Note that the post-condition for new is weaker than it has to be. We could strengthen it to capture the fact that p is actually 1 greater than the max pointer in the heap. But leaving the specification weaker allows us to change our allocation strategy.

  Lemma new_tc (u : U.t) :
    {{ top }}
    new u
    {{ fun h p h' => lookup h p = None /\ h' = insert h p u }}.
u: U.t
{{top}} new u
{{fun (h : heap) (p : ptr) (h' : heap) =>
  lookup h p = None /\ h' = insert h p u}}
  Proof.
u: U.t
{{top}} new u
{{fun (h : heap) (p : ptr) (h' : heap) =>
  lookup h p = None /\ h' = insert h p u}}
    smash.
  Qed.

The free p command can be run in any state where p is defined, and results in a state where p is removed.

  Lemma free_tc (p : ptr) :
    {{ fun h => lookup h p <> None }}
    free p
    {{ fun h _ h' => h' = remove h p }}.
p: ptr
{{fun h : heap => lookup h p <> None}} free p
{{fun (h : heap) (_ : unit) (h' : heap) =>
  h' = remove h p}}
  Proof.
p: ptr
{{fun h : heap => lookup h p <> None}} free p
{{fun (h : heap) (_ : unit) (h' : heap) =>
  h' = remove h p}}
    smash; induction h; simpl in *; smash.
p, p0: ptr
t: U.t
h: list (ptr * U.t)
n: p <> p0
H: lookup h p <> None
H0: match
  match lookup h p with
  | Some _ => Some (remove h p, tt)
  | None => None
  end
with
| Some (h', _) => h' = remove h p
| None => False
end
match
  match lookup h p with
  | Some _ => Some ((p0, t) :: remove h p, tt)
  | None => None
  end
with
| Some (h', _) => h' = (p0, t) :: remove h p
| None => False
end
    destruct (lookup h p); smash.
  Qed.

The read p command can be run in any state where p is defined, and results in an unchanged state. The value returned is equal to the the value associated with p.

  Lemma read_tc (p : ptr) :
    {{ fun h => lookup h p <> None }}
    read p
    {{ fun h v h' => h = h' /\ lookup h p = Some v }}.
p: ptr
{{fun h : heap => lookup h p <> None}} read p
{{fun (h : heap) (v : U.t) (h' : heap) =>
  h = h' /\ lookup h p = Some v}}
  Proof.
p: ptr
{{fun h : heap => lookup h p <> None}} read p
{{fun (h : heap) (v : U.t) (h' : heap) =>
  h = h' /\ lookup h p = Some v}}
    smash.
p: ptr
h: heap
H: lookup h p <> None
match
  match lookup h p with
  | Some u => Some (h, u)
  | None => None
  end
with
| Some (h', v) => h = h' /\ lookup h p = Some v
| None => False
end destruct (lookup h p); smash.
  Qed.

The write p u command can be run in any state where p is defined, and results in a state where p maps to u, but is otherwise unchanged.

  Lemma write_tc (p : ptr) (u : U.t) :
    {{ fun h => lookup h p <> None }}
    write p u
    {{ fun h _ h' => h' = insert (remove h p) p u}}.
p: ptr
u: U.t
{{fun h : heap => lookup h p <> None}} write p u
{{fun (h : heap) (_ : unit) (h' : heap) =>
  h' = insert (remove h p) p u}}
  Proof.
p: ptr
u: U.t
{{fun h : heap => lookup h p <> None}} write p u
{{fun (h : heap) (_ : unit) (h' : heap) =>
  h' = insert (remove h p) p u}}
    smash; destruct (lookup h p); smash.
  Qed.

The rule for bind is the most complicated, but that's more because we want to support dependency than anything else. Intuitively, if {{P1}} c {{Q1}} and {{P2 x}} f x {{Q2 x}}, then the compound command x <- c; f has as the weakest pre-condition needed to ensure we don't fail that P1 holds and for any (demonically-chosen state and value) x and h' which c might compute (and hence satisfies Q1 h x h'), we can show that P2 x h' holds. Both conditions are needed to ensure that neither command will fail.

The post-condition is the strongest post-condition we can calculate as the composition of the commands. It is effectively the relational composition of the post-conditions for c and f respectively.

Again, note that we can effectively compute the pre- and post- conditions instead of forcing a prover to magically come up with appropriate conditions.

  Definition precomp (t : Type)
             (P1 : hprop)
             (Q1 : heap -> t -> hprop)
             (P2 : t -> hprop) : hprop :=
    fun h => P1 h /\ (forall (x : t) (h' : heap), Q1 h x h' -> P2 x h').

  Definition postcomp (t u : Type)
             (Q1 : heap-> t -> hprop)
             (Q2 : t -> heap -> u -> hprop)
    : heap -> u -> hprop :=
    fun h x h' => exists y h'', Q1 h y h'' /\ Q2 y h'' x h'.

  Lemma bind_tc
    {t u : Type} {c : Cmd t} {f : t -> Cmd u}
    {P1 : hprop} {Q1 : heap -> t -> hprop}
    {P2 : t -> hprop} {Q2 : t -> heap -> u -> hprop} :
    {{ P1 }} c {{ Q1 }} ->
    (forall x : t, {{ P2 x }} (f x) {{ Q2 x }}) ->
    {{ precomp P1 Q1 P2 }}
    x <- c; f x
    {{ postcomp Q1 Q2 }}.
t, u: Type
c: Cmd t
f: t -> Cmd u
P1: hprop
Q1: heap -> t -> hprop
P2: t -> hprop
Q2: t -> heap -> u -> hprop
{{P1}} c {{Q1}} ->
(forall x : t, {{P2 x}} f x {{Q2 x}}) ->
{{precomp P1 Q1 P2}} x <- c; f x {{postcomp Q1 Q2}}
  Proof.
t, u: Type
c: Cmd t
f: t -> Cmd u
P1: hprop
Q1: heap -> t -> hprop
P2: t -> hprop
Q2: t -> heap -> u -> hprop
{{P1}} c {{Q1}} ->
(forall x : t, {{P2 x}} f x {{Q2 x}}) ->
{{precomp P1 Q1 P2}} x <- c; f x {{postcomp Q1 Q2}}
    unfold precomp, postcomp; smash.
t, u: Type
c: Cmd t
f: t -> Cmd u
P1: heap -> Prop
Q1: heap -> t -> heap -> Prop
P2: t -> heap -> Prop
Q2: t -> heap -> u -> heap -> Prop
H0: forall (x : t) (h : heap),
P2 x h ->
match f x h with
| Some (h', v) => Q2 x h v h'
| None => False
end
h: heap
H1: P1 h
H2: forall (x : t) (h' : heap), Q1 h x h' -> P2 x h'
h0: heap
t0: t
H: Q1 h t0 h0
match f t0 h0 with
| Some (h', v) =>
    exists (y : t) (h'' : heap),
      Q1 h y h'' /\ Q2 y h'' v h'
| None => False
end
    firstorder smash.
  Qed.

  Notation "x <-- c ; f" := (bind_tc c (fun x => f))
    (right associativity, at level 84, c at next level) : cmd_scope.
  Notation "c ;;; f" := (bind_tc c (fun _ => f))
    (right associativity, at level 84) : cmd_scope.

Just for fun, we can define our own version of if.

  Lemma if_tc {t : Type}
        {B1 B2 : Prop}
        (b : {B1} + {B2})
        (c1 c2 : Cmd t)
        {P1} {P2} {Q1} {Q2} :
    {{P1}} c1 {{Q1}} ->
    {{P2}} c2 {{Q2}} ->
    {{fun h => if b then P1 h else P2 h}}
    if b then c1 else c2
    {{fun h x h' => if b then Q1 h x h' else Q2 h x h'}}.
t: Type
B1, B2: Prop
b: {B1} + {B2}
c1, c2: Cmd t
P1, P2: hprop
Q1, Q2: heap -> t -> hprop
{{P1}} c1 {{Q1}} ->
{{P2}} c2 {{Q2}} ->
{{fun h : heap => if b then P1 h else P2 h}} if b
                                             then c1
                                             else c2
{{fun (h : heap) (x : t) (h' : heap) =>
  if b then Q1 h x h' else Q2 h x h'}}
  Proof.
t: Type
B1, B2: Prop
b: {B1} + {B2}
c1, c2: Cmd t
P1, P2: hprop
Q1, Q2: heap -> t -> hprop
{{P1}} c1 {{Q1}} ->
{{P2}} c2 {{Q2}} ->
{{fun h : heap => if b then P1 h else P2 h}} if b
                                             then c1
                                             else c2
{{fun (h : heap) (x : t) (h' : heap) =>
  if b then Q1 h x h' else Q2 h x h'}}
    destruct b; smash.
  Qed.

Now we can give a proper interface to run -- we should only pass it commands that will return a value and then we can guarantee that we won't get a failure.

  Definition run_tc {t : Type} (c : Cmd t) :
    {{top}} c {{fun _ _ => top}} -> t.
t: Type
c: Cmd t
{{top}} c {{fun (_ : heap) (_ : t) => top}} -> t
  Proof.
t: Type
c: Cmd t
{{top}} c {{fun (_ : heap) (_ : t) => top}} -> t
    unfold top; intros; smash.
t: Type
c: Cmd t
H: forall h : heap,
True ->
match c h with
| Some (_, _) => True
| None => False
end
t
    generalize (H nil I).
t: Type
c: Cmd t
H: forall h : heap,
True ->
match c h with
| Some (_, _) => True
| None => False
end
match c nil with
| Some (_, _) => True
| None => False
end -> t
    destruct (c nil); smash.
  Qed.


End FunctionalIMP.

Module MyUniverse <: UNIVERSE.

Now, we'll choose a type for values to put on the heap, and reason about programs that actually read and write to the heap. We could use any type for values.

However, as an exercise, what happens if we tried to add functions from U to U to the type below? Coq would reject the definition. This is known as a non-strict positive occurence, because the type that we are defining appears on the left side of a function in one of its constructors. In short, despite being a valid algebraic type (it would be accepted in a language like OCaml), defining such a type in Coq would allow the construction of non-terminating functions. Coq rejects these definitions to ensure termination.

  Inductive U : Type :=
  | Nat_t : nat -> U
  | Pair_t : U -> U -> U.

  Definition t := U.
End MyUniverse.

Module MyFunctionalImp := FunctionalIMP (MyUniverse).

Import MyUniverse.
Import MyFunctionalImp.
Local Open Scope cmd_scope.

More examples. Note that some can "go wrong"!

Definition c3 := z <- new (Nat_t 0); w <- read z; ret w.
Compute run c3.
= Some ((1, Nat_t 0) :: nil, Nat_t 0)
: option (heap * t)
Definition c4 := z <- new (Nat_t 0); write z (Nat_t z);; ret z.
Compute run c4.
= Some ((1, Nat_t 1) :: nil, 1)
: option (heap * ptr)
Definition c5 := free 1.
Compute run c5.
= None
: option (heap * unit)
Definition c6 := x <- new (Nat_t 0); free x;; read x.
Compute run c6.
= None
: option (heap * t)
Definition c7 :=
  x <- new (Nat_t 0);
  (if ptr_le_gt_dec x 10 then free x else ret tt);;
  z <- new (Nat_t 0);
  (if ptr_le_gt_dec x 10 then ret (Nat_t 42) else read x).

Does c7 succeed? Notice that the two if expressions have the same guard.

Compute run c7.
= Some ((1, Nat_t 0) :: nil, Nat_t 42)
: option (heap * U)

Some example proofs that these commands have specifications -- one way to view this is that we are building commands and inferring specifications for them, fully automatically!

Definition p1 := ret_tc 0.
Check p1.
p1
     : {{top}} ret 0
       {{fun (h : heap) (x : nat) (h' : heap) =>
         x = 0 /\ h = h'}}

Unfortunately, the specifications that we calculate are rather unwieldy. Even these simple proofs yield default specifications that are impossible to read.

Definition p2 :=
  x <-- ret_tc 0; y <-- ret_tc 1; ret_tc (x + y).
Check p2.
p2
     : {{precomp top
           (fun (h : heap) (x : nat) (h' : heap) =>
            x = 0 /\ h = h')
           (fun _ : nat =>
            precomp top
              (fun (h : heap) (x : nat) (h' : heap) =>
               x = 1 /\ h = h') (fun _ : nat => top))}} 
       x <- ret 0; x0 <- ret 1; ret (x + x0)
       {{postcomp
           (fun (h : heap) (x : nat) (h' : heap) =>
            x = 0 /\ h = h')
           (fun x : nat =>
            postcomp
              (fun (h : heap) (x0 : nat) (h' : heap)
               => x0 = 1 /\ h = h')
              (fun (y : nat) (h : heap) (x0 : nat)
                 (h' : heap) => x0 = x + y /\ h = h'))}}

Definition p3 :=
  z <-- new_tc (Nat_t 0); w <-- read_tc z; ret_tc w.
Check p3.
p3
     : {{precomp top
           (fun (h : heap) (p : ptr) (h' : heap) =>
            lookup h p = None /\
            h' = insert h p (Nat_t 0))
           (fun z : ptr =>
            precomp
              (fun h : heap => lookup h z <> None)
              (fun (h : heap) (v : t) (h' : heap) =>
               h = h' /\ lookup h z = Some v)
              (fun _ : t => top))}} x <-
                                    new (Nat_t 0);
                                    x0 <- read x;
                                    ret x0
       {{postcomp
           (fun (h : heap) (p : ptr) (h' : heap) =>
            lookup h p = None /\
            h' = insert h p (Nat_t 0))
           (fun z : ptr =>
            postcomp
              (fun (h : heap) (v : t) (h' : heap) =>
               h = h' /\ lookup h z = Some v)
              (fun (w : t) (h : heap) (x : t)
                 (h' : heap) => x = w /\ h = h'))}}

Definition p4 :=
  z <-- new_tc (Nat_t 0); write_tc z (Nat_t z);;; ret_tc z.
Check p4.
p4
     : {{precomp top
           (fun (h : heap) (p : ptr) (h' : heap) =>
            lookup h p = None /\
            h' = insert h p (Nat_t 0))
           (fun z : ptr =>
            precomp
              (fun h : heap => lookup h z <> None)
              (fun (h : heap) (_ : unit) (h' : heap)
               => h' = insert (remove h z) z (Nat_t z))
              (fun _ : unit => top))}} x <-
                                       new (Nat_t 0);
                                       write x
                                         (Nat_t x);;
                                       ret x
       {{postcomp
           (fun (h : heap) (p : ptr) (h' : heap) =>
            lookup h p = None /\
            h' = insert h p (Nat_t 0))
           (fun z : ptr =>
            postcomp
              (fun (h : heap) (_ : unit) (h' : heap)
               => h' = insert (remove h z) z (Nat_t z))
              (fun (_ : unit) (h : heap) (x : ptr)
                 (h' : heap) => x = z /\ h = h'))}}

Definition p5 :=
  free_tc 1.
Check p5.
p5
     : {{fun h : heap => lookup h 1 <> None}} free 1
       {{fun (h : heap) (_ : unit) (h' : heap) =>
         h' = remove h 1}}

Definition p6 :=
  x <-- new_tc (Nat_t 0); free_tc x;;; read_tc x.
Check p6.
p6
     : {{precomp top
           (fun (h : heap) (p : ptr) (h' : heap) =>
            lookup h p = None /\
            h' = insert h p (Nat_t 0))
           (fun x : ptr =>
            precomp
              (fun h : heap => lookup h x <> None)
              (fun (h : heap) (_ : unit) (h' : heap)
               => h' = remove h x)
              (fun (_ : unit) (h : heap) =>
               lookup h x <> None))}} x <-
                                      new (Nat_t 0);
                                      free x;; read x
       {{postcomp
           (fun (h : heap) (p : ptr) (h' : heap) =>
            lookup h p = None /\
            h' = insert h p (Nat_t 0))
           (fun x : ptr =>
            postcomp
              (fun (h : heap) (_ : unit) (h' : heap)
               => h' = remove h x)
              (fun (_ : unit) (h : heap) (v : t)
                 (h' : heap) =>
               h = h' /\ lookup h x = Some v))}}

Definition p7 :=
  x <-- new_tc (Nat_t 0);
  (if_tc (ptr_le_gt_dec x 10) (free_tc x) (ret_tc tt));;;
  z <-- new_tc (Nat_t 0);
  (if_tc (ptr_le_gt_dec x 10) (ret_tc (Nat_t 42)) (read_tc x)).
Check p7.
p7
     : {{precomp top
           (fun (h : heap) (p : ptr) (h' : heap) =>
            lookup h p = None /\
            h' = insert h p (Nat_t 0))
           (fun x : ptr =>
            precomp
              (fun h : heap =>
               if ptr_le_gt_dec x 10
               then lookup h x <> None
               else top h)
              (fun (h : heap) (x0 : unit) (h' : heap)
               =>
               if ptr_le_gt_dec x 10
               then h' = remove h x
               else x0 = tt /\ h = h')
              (fun _ : unit =>
               precomp top
                 (fun (h : heap) (p : ptr) (h' : heap)
                  =>
                  lookup h p = None /\
                  h' = insert h p (Nat_t 0))
                 (fun (_ : ptr) (h : heap) =>
                  if ptr_le_gt_dec x 10
                  then top h
                  else lookup h x <> None)))}} x <-
                                               new
                                                 (Nat_t
                                                 0);
                                               (if
                                                 ptr_le_gt_dec
                                                 x 10
                                                then
                                                 free
                                                 x
                                                else
                                                 ret
                                                 tt);;
                                               _ <-
                                               new
                                                 (Nat_t
                                                 0);
                                               (if
                                                 ptr_le_gt_dec
                                                 x 10
                                                then
                                                 ret
                                                 (Nat_t
                                                 42)
                                                else
                                                 read
                                                 x)
       {{postcomp
           (fun (h : heap) (p : ptr) (h' : heap) =>
            lookup h p = None /\
            h' = insert h p (Nat_t 0))
           (fun x : ptr =>
            postcomp
              (fun (h : heap) (x0 : unit) (h' : heap)
               =>
               if ptr_le_gt_dec x 10
               then h' = remove h x
               else x0 = tt /\ h = h')
              (fun _ : unit =>
               postcomp
                 (fun (h : heap) (p : ptr) (h' : heap)
                  =>
                  lookup h p = None /\
                  h' = insert h p (Nat_t 0))
                 (fun (_ : ptr) (h : heap) (x0 : U)
                    (h' : heap) =>
                  if ptr_le_gt_dec x 10
                  then x0 = Nat_t 42 /\ h = h'
                  else h = h' /\ lookup h x = Some x0)))}}

More generally, we can write a function, like swap, and give it a human-readable specification. Then we can use the combinators to build most of the proof, and all we are left with are the two verification conditions from the rule of consequence.

Definition swap x y : Cmd unit :=
  xv <- read x; yv <- read y; write x yv;; write y xv.

We first prove a key lemma from the "McCarthy" axioms of memory that allows us to reason about updates when two pointers are different.

Lemma lookup_remove_other : forall h p1 p2,
  p1 <> p2 ->
  lookup h p2 = lookup (remove h p1) p2.
forall (h : heap) (p1 p2 : ptr),
p1 <> p2 -> lookup h p2 = lookup (remove h p1) p2
Proof.
forall (h : heap) (p1 p2 : ptr),
p1 <> p2 -> lookup h p2 = lookup (remove h p1) p2
  induction h; repeat smash.
Qed.

Lemma lookup_insert_other : forall h p1 v p2,
  p1 <> p2 ->
  lookup h p2 = lookup (insert h p1 v) p2.
forall (h : heap) (p1 : ptr) (v : t) (p2 : ptr),
p1 <> p2 -> lookup h p2 = lookup (insert h p1 v) p2
Proof.
forall (h : heap) (p1 : ptr) (v : t) (p2 : ptr),
p1 <> p2 -> lookup h p2 = lookup (insert h p1 v) p2
  induction h; repeat smash;
  destruct ptr_le_gt_dec; repeat smash.
Qed.

Lemma lookup_insert :  forall h p v,
    lookup (insert h p v) p = Some v.
forall (h : heap) (p : ptr) (v : t),
lookup (insert h p v) p = Some v
Proof.
forall (h : heap) (p : ptr) (v : t),
lookup (insert h p v) p = Some v
  induction h; repeat smash.
p0: ptr
t0: t
h: list (ptr * t)
IHh: forall (p : ptr) (v : t), lookup (insert h p v) p = Some v
p: ptr
v: t
lookup
  (if ptr_le_gt_dec p p0
   then (p, v) :: (p0, t0) :: h
   else (p0, t0) :: insert h p v) p = Some v
  destruct ptr_le_gt_dec; repeat smash.
p0: ptr
t0: t
h: list (ptr * t)
IHh: forall (p : ptr) (v : t), lookup (insert h p v) p = Some v
v: t
g: p0 > p0
Some t0 = Some v
  lia.
Qed.

Next, we build a tactic that simplifies memory lookups.

Ltac s :=
  match goal with
  | [ H : ?y <> ?x |- context[lookup (remove ?h ?x) ?y] ] =>
      rewrite <- (@lookup_remove_other h x y); [auto | try congruence]
  | [ H : ?y <> ?x |- context[lookup (insert ?h ?x ?v) ?y] ] =>
      rewrite <- (@lookup_insert_other h x v y);
      [auto | try congruence]
  | [ |- context [lookup (insert ?h ?x ?v) ?x] ] =>
      rewrite (lookup_insert h x v)
  | _ => smash; simpl in *; subst; try congruence; auto
  end.
Ltac memsimp := repeat progress (s; intros).

Finally, we build the proof that swap has the following "nice" specification.

Definition automatic_swap_tc x y :=
  xv <-- read_tc x; yv <-- read_tc y; write_tc x yv;;; write_tc y xv.
Check automatic_swap_tc.
automatic_swap_tc
     : forall x y : ptr,
       {{precomp (fun h : heap => lookup h x <> None)
           (fun (h : heap) (v : t) (h' : heap) =>
            h = h' /\ lookup h x = Some v)
           (fun _ : t =>
            precomp
              (fun h : heap => lookup h y <> None)
              (fun (h : heap) (v : t) (h' : heap) =>
               h = h' /\ lookup h y = Some v)
              (fun yv : t =>
               precomp
                 (fun h : heap => lookup h x <> None)
                 (fun (h : heap) (_ : unit)
                    (h' : heap) =>
                  h' = insert (remove h x) x yv)
                 (fun (_ : unit) (h : heap) =>
                  lookup h y <> None)))}} x0 <-
                                          read x;
                                          x1 <-
                                          read y;
                                          write x x1;;
                                          write y x0
       {{postcomp
           (fun (h : heap) (v : t) (h' : heap) =>
            h = h' /\ lookup h x = Some v)
           (fun xv : t =>
            postcomp
              (fun (h : heap) (v : t) (h' : heap) =>
               h = h' /\ lookup h y = Some v)
              (fun yv : t =>
               postcomp
                 (fun (h : heap) (_ : unit)
                    (h' : heap) =>
                  h' = insert (remove h x) x yv)
                 (fun (_ : unit) (h : heap) (_ : unit)
                    (h' : heap) =>
                  h' = insert (remove h y) y xv)))}}

Definition swap_tc x y :
  {{ fun h => lookup h x <> None /\ lookup h y <> None }}
  swap x y
  {{fun h _ h' => lookup h' y = lookup h x /\
                lookup h' x = lookup h y}}.
x, y: ptr
{{fun h : heap =>
  lookup h x <> None /\ lookup h y <> None}} swap x y
{{fun (h : heap) (_ : unit) (h' : heap) =>
  lookup h' y = lookup h x /\ lookup h' x = lookup h y}}
Proof.
x, y: ptr
{{fun h : heap =>
  lookup h x <> None /\ lookup h y <> None}} swap x y
{{fun (h : heap) (_ : unit) (h' : heap) =>
  lookup h' y = lookup h x /\ lookup h' x = lookup h y}}
  apply (consequence_tc (automatic_swap_tc x y)).
x, y: ptr
forall h : heap,
lookup h x <> None /\ lookup h y <> None ->
precomp (fun h0 : heap => lookup h0 x <> None)
  (fun (h0 : heap) (v : t) (h' : heap) =>
   h0 = h' /\ lookup h0 x = Some v)
  (fun _ : t =>
   precomp (fun h0 : heap => lookup h0 y <> None)
     (fun (h0 : heap) (v : t) (h' : heap) =>
      h0 = h' /\ lookup h0 y = Some v)
     (fun yv : t =>
      precomp (fun h0 : heap => lookup h0 x <> None)
        (fun (h0 : heap) (_ : unit) (h' : heap) =>
         h' = insert (remove h0 x) x yv)
        (fun (_ : unit) (h0 : heap) =>
         lookup h0 y <> None))) h
x, y: ptr
forall (h : heap) (x0 : unit) (h' : heap),
postcomp
  (fun (h0 : heap) (v : t) (h'0 : heap) =>
   h0 = h'0 /\ lookup h0 x = Some v)
  (fun xv : t =>
   postcomp
     (fun (h0 : heap) (v : t) (h'0 : heap) =>
      h0 = h'0 /\ lookup h0 y = Some v)
     (fun yv : t =>
      postcomp
        (fun (h0 : heap) (_ : unit) (h'0 : heap) =>
         h'0 = insert (remove h0 x) x yv)
        (fun (_ : unit) (h0 : heap) (_ : unit)
           (h'0 : heap) =>
         h'0 = insert (remove h0 y) y xv))) h x0 h' ->
lookup h' y = lookup h x /\ lookup h' x = lookup h y
  -
x, y: ptr
forall h : heap,
lookup h x <> None /\ lookup h y <> None ->
precomp (fun h0 : heap => lookup h0 x <> None)
  (fun (h0 : heap) (v : t) (h' : heap) =>
   h0 = h' /\ lookup h0 x = Some v)
  (fun _ : t =>
   precomp (fun h0 : heap => lookup h0 y <> None)
     (fun (h0 : heap) (v : t) (h' : heap) =>
      h0 = h' /\ lookup h0 y = Some v)
     (fun yv : t =>
      precomp (fun h0 : heap => lookup h0 x <> None)
        (fun (h0 : heap) (_ : unit) (h' : heap) =>
         h' = insert (remove h0 x) x yv)
        (fun (_ : unit) (h0 : heap) =>
         lookup h0 y <> None))) h unfold precomp; memsimp.
x, y: ptr
h'0: heap
H: lookup h'0 x <> None
H0: lookup h'0 y <> None
x0: t
H2: lookup h'0 x = Some x0
x1: t
H4: lookup h'0 y = Some x1
x2: unit
lookup (insert (remove h'0 x) x x1) y <> None
    destruct (ptr_eq_dec y x); memsimp.
  -
x, y: ptr
forall (h : heap) (x0 : unit) (h' : heap),
postcomp
  (fun (h0 : heap) (v : t) (h'0 : heap) =>
   h0 = h'0 /\ lookup h0 x = Some v)
  (fun xv : t =>
   postcomp
     (fun (h0 : heap) (v : t) (h'0 : heap) =>
      h0 = h'0 /\ lookup h0 y = Some v)
     (fun yv : t =>
      postcomp
        (fun (h0 : heap) (_ : unit) (h'0 : heap) =>
         h'0 = insert (remove h0 x) x yv)
        (fun (_ : unit) (h0 : heap) (_ : unit)
           (h'0 : heap) =>
         h'0 = insert (remove h0 y) y xv))) h x0 h' ->
lookup h' y = lookup h x /\ lookup h' x = lookup h y unfold postcomp; memsimp.
x, y: ptr
x0: unit
x1: t
x4: heap
H1: lookup x4 x = Some x1
x3: t
H3: lookup x4 y = Some x3
x5: unit
lookup
  (insert (remove (insert (remove x4 x) x x3) y) y x1)
  x = lookup x4 y
    destruct (ptr_eq_dec x y); memsimp.
Qed.

Definition c :=
  x <- new (Nat_t 0);
  y <- new (Nat_t x);
  z <- new (Nat_t 3);
  v <- read y;
  swap z y.

Definition c_tc :
  {{ top }} c {{ fun _ _ => top }}.
{{top}} c {{fun (_ : heap) (_ : unit) => top}}
  refine (consequence_tc
            (x <-- new_tc (Nat_t 0);
             y <-- new_tc (Nat_t x);
             z <-- new_tc (Nat_t 3);
             v <-- read_tc y;
             swap_tc z y) _ _).
forall h : heap,
top h ->
precomp top
  (fun (h0 : heap) (p : ptr) (h' : heap) =>
   lookup h0 p = None /\ h' = insert h0 p (Nat_t 0))
  (fun x : ptr =>
   precomp top
     (fun (h0 : heap) (p : ptr) (h' : heap) =>
      lookup h0 p = None /\ h' = insert h0 p (Nat_t x))
     (fun y : ptr =>
      precomp top
        (fun (h0 : heap) (p : ptr) (h' : heap) =>
         lookup h0 p = None /\
         h' = insert h0 p (Nat_t 3))
        (fun z : ptr =>
         precomp
           (fun h0 : heap => lookup h0 y <> None)
           (fun (h0 : heap) (v : t) (h' : heap) =>
            h0 = h' /\ lookup h0 y = Some v)
           (fun (_ : t) (h0 : heap) =>
            lookup h0 z <> None /\ lookup h0 y <> None))))
  h
forall (h : heap) (x : unit) (h' : heap),
postcomp
  (fun (h0 : heap) (p : ptr) (h'0 : heap) =>
   lookup h0 p = None /\ h'0 = insert h0 p (Nat_t 0))
  (fun x0 : ptr =>
   postcomp
     (fun (h0 : heap) (p : ptr) (h'0 : heap) =>
      lookup h0 p = None /\
      h'0 = insert h0 p (Nat_t x0))
     (fun y : ptr =>
      postcomp
        (fun (h0 : heap) (p : ptr) (h'0 : heap) =>
         lookup h0 p = None /\
         h'0 = insert h0 p (Nat_t 3))
        (fun z : ptr =>
         postcomp
           (fun (h0 : heap) (v : t) (h'0 : heap) =>
            h0 = h'0 /\ lookup h0 y = Some v)
           (fun (_ : t) (h0 : heap) (_ : unit)
              (h'0 : heap) =>
            lookup h'0 y = lookup h0 z /\
            lookup h'0 z = lookup h0 y)))) h x h' ->
top h'
  -
forall h : heap,
top h ->
precomp top
  (fun (h0 : heap) (p : ptr) (h' : heap) =>
   lookup h0 p = None /\ h' = insert h0 p (Nat_t 0))
  (fun x : ptr =>
   precomp top
     (fun (h0 : heap) (p : ptr) (h' : heap) =>
      lookup h0 p = None /\ h' = insert h0 p (Nat_t x))
     (fun y : ptr =>
      precomp top
        (fun (h0 : heap) (p : ptr) (h' : heap) =>
         lookup h0 p = None /\
         h' = insert h0 p (Nat_t 3))
        (fun z : ptr =>
         precomp
           (fun h0 : heap => lookup h0 y <> None)
           (fun (h0 : heap) (v : t) (h' : heap) =>
            h0 = h' /\ lookup h0 y = Some v)
           (fun (_ : t) (h0 : heap) =>
            lookup h0 z <> None /\ lookup h0 y <> None))))
  h unfold precomp.
forall h : heap,
top h ->
top h /\
(forall (x : ptr) (h' : heap),
 lookup h x = None /\ h' = insert h x (Nat_t 0) ->
 top h' /\
 (forall (x0 : ptr) (h'0 : heap),
  lookup h' x0 = None /\ h'0 = insert h' x0 (Nat_t x) ->
  top h'0 /\
  (forall (x1 : ptr) (h'1 : heap),
   lookup h'0 x1 = None /\
   h'1 = insert h'0 x1 (Nat_t 3) ->
   lookup h'1 x0 <> None /\
   (forall (x2 : t) (h'2 : heap),
    h'1 = h'2 /\ lookup h'1 x0 = Some x2 ->
    lookup h'2 x1 <> None /\ lookup h'2 x0 <> None)))) memsimp.
h: heap
H: top h
x: ptr
H0: lookup h x = None
x0: ptr
H2: lookup (insert h x (Nat_t 0)) x0 = None
x1: ptr
H4: lookup
  (insert (insert h x (Nat_t 0)) x0 (Nat_t x)) x1 =
None
lookup
  (insert (insert (insert h x (Nat_t 0)) x0 (Nat_t x))
     x1 (Nat_t 3)) x0 <> None
    destruct (ptr_eq_dec x0 x1); memsimp.
  -
forall (h : heap) (x : unit) (h' : heap),
postcomp
  (fun (h0 : heap) (p : ptr) (h'0 : heap) =>
   lookup h0 p = None /\ h'0 = insert h0 p (Nat_t 0))
  (fun x0 : ptr =>
   postcomp
     (fun (h0 : heap) (p : ptr) (h'0 : heap) =>
      lookup h0 p = None /\
      h'0 = insert h0 p (Nat_t x0))
     (fun y : ptr =>
      postcomp
        (fun (h0 : heap) (p : ptr) (h'0 : heap) =>
         lookup h0 p = None /\
         h'0 = insert h0 p (Nat_t 3))
        (fun z : ptr =>
         postcomp
           (fun (h0 : heap) (v : t) (h'0 : heap) =>
            h0 = h'0 /\ lookup h0 y = Some v)
           (fun (_ : t) (h0 : heap) (_ : unit)
              (h'0 : heap) =>
            lookup h'0 y = lookup h0 z /\
            lookup h'0 z = lookup h0 y)))) h x h' ->
top h' unfold postcomp.
forall h : heap,
unit ->
forall h' : heap,
(exists (y : ptr) (h'' : heap),
   (lookup h y = None /\ h'' = insert h y (Nat_t 0)) /\
   (exists (y0 : ptr) (h''0 : heap),
      (lookup h'' y0 = None /\
       h''0 = insert h'' y0 (Nat_t y)) /\
      (exists (y1 : ptr) (h''1 : heap),
         (lookup h''0 y1 = None /\
          h''1 = insert h''0 y1 (Nat_t 3)) /\
         (exists (y2 : t) (h''2 : heap),
            (h''1 = h''2 /\ lookup h''1 y0 = Some y2) /\
            lookup h' y0 = lookup h''2 y1 /\
            lookup h' y1 = lookup h''2 y0)))) ->
top h' memsimp.
Defined.

We might like to add a new command that reads out a number or that reads out a pair.

Definition read_nat (p : ptr) : Cmd nat :=
  v <- read p;
  match v with
  | Nat_t n => ret n
  | _ => exit _
  end.

Definition read_pair (p : ptr) : Cmd (U*U) :=
  v <- read p;
  match v with
  | Pair_t x y => ret (x, y)
  | _ => exit _
  end.

We can define appropriate proof rules for these now.

Definition read_nat_tc (p : ptr) :
  {{ fun h => exists n, lookup h p = Some (Nat_t n) }}
  read_nat p
  {{ fun h v h' => h = h' /\ lookup h p = Some (Nat_t v) }}.
p: ptr
{{fun h : heap =>
  exists n : nat, lookup h p = Some (Nat_t n)}} read_nat
                                                 p
{{fun (h : heap) (v : nat) (h' : heap) =>
  h = h' /\ lookup h p = Some (Nat_t v)}}
Proof.
p: ptr
{{fun h : heap =>
  exists n : nat, lookup h p = Some (Nat_t n)}} read_nat
                                                 p
{{fun (h : heap) (v : nat) (h' : heap) =>
  h = h' /\ lookup h p = Some (Nat_t v)}}
  unfold read_nat; smash; destruct (lookup h p); smash; congruence.
Qed.

Definition read_pair_tc (p : ptr) :
  {{ fun h => exists us, lookup h p = Some (Pair_t (fst us) (snd us)) }}
  read_pair p
  {{ fun h v h' =>
       h = h' /\ lookup h p = Some (Pair_t (fst v) (snd v)) }}.
p: ptr
{{fun h : heap =>
  exists us : U * U,
    lookup h p = Some (Pair_t (fst us) (snd us))}} 
read_pair p
{{fun (h : heap) (v : U * U) (h' : heap) =>
  h = h' /\ lookup h p = Some (Pair_t (fst v) (snd v))}}
Proof.
p: ptr
{{fun h : heap =>
  exists us : U * U,
    lookup h p = Some (Pair_t (fst us) (snd us))}} 
read_pair p
{{fun (h : heap) (v : U * U) (h' : heap) =>
  h = h' /\ lookup h p = Some (Pair_t (fst v) (snd v))}}
  unfold read_pair; smash; destruct (lookup h p); smash; congruence.
Qed.

Now we can prove that the following code will not get stuck.

Definition alloc_and_swap :=
  x <- new (Nat_t 0);
  y <- new (Pair_t (Nat_t 1) (Nat_t 2));
  swap x y;;
  read_nat y.

Here is the proof...

Definition alloc_and_swap_tc :
  {{ top }} alloc_and_swap {{ fun _ _ => top }}.
{{top}} alloc_and_swap
{{fun (_ : heap) (_ : nat) => top}}
Proof.
{{top}} alloc_and_swap
{{fun (_ : heap) (_ : nat) => top}}
  refine (
      consequence_tc
        (x <-- new_tc (Nat_t 0);
         y <-- new_tc (Pair_t (Nat_t 1) (Nat_t 2));
         swap_tc x y;;;
         read_nat_tc y) _ _);
    unfold precomp, postcomp; memsimp.
h: heap
H: top h
x: ptr
H0: lookup h x = None
x0: ptr
H2: lookup (insert h x (Nat_t 0)) x0 = None
lookup
  (insert (insert h x (Nat_t 0)) x0
     (Pair_t (Nat_t 1) (Nat_t 2))) x <> None
h: heap
H: top h
x: ptr
H0: lookup h x = None
x0: ptr
H2: lookup (insert h x (Nat_t 0)) x0 = None
x1: unit
h'1: heap
H5: lookup h'1 x =
lookup
  (insert (insert h x (Nat_t 0)) x0
     (Pair_t (Nat_t 1) (Nat_t 2))) x0
H4: lookup h'1 x0 =
lookup
  (insert (insert h x (Nat_t 0)) x0
     (Pair_t (Nat_t 1) (Nat_t 2))) x
exists n : nat, lookup h'1 x0 = Some (Nat_t n)
  -
h: heap
H: top h
x: ptr
H0: lookup h x = None
x0: ptr
H2: lookup (insert h x (Nat_t 0)) x0 = None
lookup
  (insert (insert h x (Nat_t 0)) x0
     (Pair_t (Nat_t 1) (Nat_t 2))) x <> None destruct (ptr_eq_dec x x0); memsimp.
  -
h: heap
H: top h
x: ptr
H0: lookup h x = None
x0: ptr
H2: lookup (insert h x (Nat_t 0)) x0 = None
x1: unit
h'1: heap
H5: lookup h'1 x =
lookup
  (insert (insert h x (Nat_t 0)) x0
     (Pair_t (Nat_t 1) (Nat_t 2))) x0
H4: lookup h'1 x0 =
lookup
  (insert (insert h x (Nat_t 0)) x0
     (Pair_t (Nat_t 1) (Nat_t 2))) x
exists n : nat, lookup h'1 x0 = Some (Nat_t n) rewrite H4.
h: heap
H: top h
x: ptr
H0: lookup h x = None
x0: ptr
H2: lookup (insert h x (Nat_t 0)) x0 = None
x1: unit
h'1: heap
H5: lookup h'1 x =
lookup
  (insert (insert h x (Nat_t 0)) x0
     (Pair_t (Nat_t 1) (Nat_t 2))) x0
H4: lookup h'1 x0 =
lookup
  (insert (insert h x (Nat_t 0)) x0
     (Pair_t (Nat_t 1) (Nat_t 2))) x
exists n : nat,
  lookup
    (insert (insert h x (Nat_t 0)) x0
       (Pair_t (Nat_t 1) (Nat_t 2))) x =
  Some (Nat_t n) destruct (ptr_eq_dec x x0); memsimp; eauto.
h: heap
H: top h
x0: ptr
H2: lookup (insert h x0 (Nat_t 0)) x0 = None
H0: lookup h x0 = None
x1: unit
h'1: heap
H4, H5: lookup h'1 x0 =
lookup
  (insert (insert h x0 (Nat_t 0)) x0
     (Pair_t (Nat_t 1) (Nat_t 2))) x0
exists n : nat,
  Some (Pair_t (Nat_t 1) (Nat_t 2)) = Some (Nat_t n)
    rewrite lookup_insert in H2.
h: heap
H: top h
x0: ptr
H2: Some (Nat_t 0) = None
H0: lookup h x0 = None
x1: unit
h'1: heap
H4, H5: lookup h'1 x0 =
lookup
  (insert (insert h x0 (Nat_t 0)) x0
     (Pair_t (Nat_t 1) (Nat_t 2))) x0
exists n : nat,
  Some (Pair_t (Nat_t 1) (Nat_t 2)) = Some (Nat_t n) congruence.
Defined.

Exercise: print out the proof -- it's huge!

We can even define loops and infer pre- and post-conditions for them, thanks to our ability to define predicates inductively. Here, we define a loop that iterates n times a command body.

Definition iter (t : Type) (body : t -> Cmd t) : nat -> t -> Cmd t :=
  fix loop(n : nat) : t -> Cmd t :=
    match n with
    | 0 => body
    | S n => fun x => v <- body x; loop n v
    end.

The pre-condition for the loop can be computed by composing the pre-condition of the body P with its post-condition Q using the precomp predicate transformer.

Definition iter_precomp (t : Type)
           (P : t -> hprop) (Q : t -> heap -> t -> hprop)
  : nat -> t -> hprop :=
  fix loop (n : nat) : t -> hprop :=
    match n with
    | 0 => P
    | S n => fun x => precomp (P x) (Q x) (loop n)
    end.

The post-condition for the loop can be computed by composing the post-condition of the body Q with itself, using the postcomp predicate transformer.

Definition iter_postcomp (t : Type) (Q : t -> heap -> t -> hprop)
  : nat -> t -> heap -> t -> hprop :=
  fix loop(n : nat) : t -> heap -> t -> hprop :=
    match n with
    | 0 => Q
    | S n => fun x => postcomp (Q x) (loop n)
    end.

Finally, if we can show that a loop body has pre-condition P and post-condition Q, then we can conclude that iterating the body n times results in a command with pre-condition obtained by iter_precomp P Q and post-condition obtained by iter_postcomp Q.

Lemma iter_tc {t : Type} {P} {Q} {body} :
  (forall x : t, {{ P x }} body x {{ Q x }}) ->
  forall n x,
    {{ fun h => iter_precomp P Q n x h }}
    iter body n x
    {{ fun h v h' => iter_postcomp Q n x h v h' }}.
t: Type
P: t -> hprop
Q: t -> heap -> t -> hprop
body: t -> Cmd t
(forall x : t, {{P x}} body x {{Q x}}) ->
forall (n : nat) (x : t),
{{fun h : heap => iter_precomp P Q n x h}} iter body n
                                             x
{{fun (h : heap) (v : t) (h' : heap) =>
  iter_postcomp Q n x h v h'}}
Proof.
t: Type
P: t -> hprop
Q: t -> heap -> t -> hprop
body: t -> Cmd t
(forall x : t, {{P x}} body x {{Q x}}) ->
forall (n : nat) (x : t),
{{fun h : heap => iter_precomp P Q n x h}} 
iter body n x
{{fun (h : heap) (v : t) (h' : heap) =>
  iter_postcomp Q n x h v h'}}
  induction n; simpl; auto using bind_tc.
Qed.

Definition chain n :=
  v <- new (Nat_t 0); iter (fun x => new (Nat_t x)) n v.

Definition chain_tc n :=
  v <-- new_tc (Nat_t 0); iter_tc (fun x => new_tc (Nat_t x)) n v.

Problems with Hoare Logic

One well-known problem with Hoare logic is that it doesn't support abstraction very well. Consider the following situation: We first define an increment function and then give it a specification.

Definition inc (p : ptr) :=
  v <- read_nat p; write p (Nat_t (1 + v)).

The specification tells us that if p points to n, then running inc p results in a state where p points to 1+n.

Definition inc_tc (p : ptr) :
  {{ fun h => exists n, lookup h p = Some (Nat_t n) }}
  inc p
  {{ fun h1 _ h2 => exists n, (lookup h1 p = Some (Nat_t n) /\
                               lookup h2 p = Some (Nat_t (1 + n))) }}.
p: ptr
{{fun h : heap =>
  exists n : nat, lookup h p = Some (Nat_t n)}} inc p
{{fun (h1 : heap) (_ : unit) (h2 : heap) =>
  exists n : nat,
    lookup h1 p = Some (Nat_t n) /\
    lookup h2 p = Some (Nat_t (1 + n))}}
Proof.
p: ptr
{{fun h : heap =>
  exists n : nat, lookup h p = Some (Nat_t n)}} inc p
{{fun (h1 : heap) (_ : unit) (h2 : heap) =>
  exists n : nat,
    lookup h1 p = Some (Nat_t n) /\
    lookup h2 p = Some (Nat_t (1 + n))}}
  unfold inc.
p: ptr
{{fun h : heap =>
  exists n : nat, lookup h p = Some (Nat_t n)}} v <-
                                                read_nat
                                                 p;
                                                write
                                                 p
                                                 (Nat_t
                                                 (1 +
                                                 v))
{{fun (h1 : heap) (_ : unit) (h2 : heap) =>
  exists n : nat,
    lookup h1 p = Some (Nat_t n) /\
    lookup h2 p = Some (Nat_t (1 + n))}}
  eapply consequence_tc.
p: ptr
{{?P1}} v <- read_nat p; write p (Nat_t (1 + v))
{{?Q1}}
p: ptr
forall h : heap,
(exists n : nat, lookup h p = Some (Nat_t n)) -> ?P1 h
p: ptr
forall (h : heap) (x : unit) (h' : heap),
?Q1 h x h' ->
exists n : nat,
  lookup h p = Some (Nat_t n) /\
  lookup h' p = Some (Nat_t (1 + n))
  -
p: ptr
{{?P1}} v <- read_nat p; write p (Nat_t (1 + v))
{{?Q1}} eapply bind_tc.
p: ptr
{{?P1}} read_nat p {{?Q1}}
p: ptr
forall x : nat,
{{?P2 x}} write p (Nat_t (1 + x)) {{?Q2 x}}
    +
p: ptr
{{?P1}} read_nat p {{?Q1}} apply read_nat_tc.
    +
p: ptr
forall x : nat,
{{?P2 x}} write p (Nat_t (1 + x)) {{?Q2 x}} intros x.
p: ptr
x: nat
{{?P2 x}} write p (Nat_t (1 + x)) {{?Q2 x}} apply write_tc.
  -
p: ptr
forall h : heap,
(exists n : nat, lookup h p = Some (Nat_t n)) ->
precomp
  (fun h0 : heap =>
   exists n : nat, lookup h0 p = Some (Nat_t n))
  (fun (h0 : heap) (v : nat) (h' : heap) =>
   h0 = h' /\ lookup h0 p = Some (Nat_t v))
  (fun (_ : nat) (h0 : heap) => lookup h0 p <> None) h memsimp.
  -
p: ptr
forall (h : heap) (x : unit) (h' : heap),
postcomp
  (fun (h0 : heap) (v : nat) (h'0 : heap) =>
   h0 = h'0 /\ lookup h0 p = Some (Nat_t v))
  (fun (x0 : nat) (h0 : heap) (_ : unit) (h'0 : heap)
   => h'0 = insert (remove h0 p) p (Nat_t (1 + x0))) h
  x h' ->
exists n : nat,
  lookup h p = Some (Nat_t n) /\
  lookup h' p = Some (Nat_t (1 + n)) memsimp.
Qed.

Now consider where we have two points, and some information about both of the pointers. Unfortunately, our specification for inc is too weak to allow us to recover the fact that p2 still points to some number, so we'll no longer be able to dereference it!

Definition problem (p1 p2 : ptr) :
  {{ fun h => (exists n1, lookup h p1 = Some (Nat_t n1)) /\
              (exists n2, lookup h p2 = Some (Nat_t n2)) }}
  inc p1
  {{ fun h1 _ h2 =>
       (exists n1, lookup h1 p1 = Some (Nat_t n1) /\
                lookup h2 p1 = Some (Nat_t (1+n1))) /\
         (exists n2, lookup h1 p2 = Some (Nat_t n2) /\
                  lookup h2 p2 = Some (Nat_t n2)) }}.
p1, p2: ptr
{{fun h : heap =>
  (exists n1 : nat, lookup h p1 = Some (Nat_t n1)) /\
  (exists n2 : nat, lookup h p2 = Some (Nat_t n2))}} 
inc p1
{{fun (h1 : heap) (_ : unit) (h2 : heap) =>
  (exists n1 : nat,
     lookup h1 p1 = Some (Nat_t n1) /\
     lookup h2 p1 = Some (Nat_t (1 + n1))) /\
  (exists n2 : nat,
     lookup h1 p2 = Some (Nat_t n2) /\
     lookup h2 p2 = Some (Nat_t n2))}}
Proof.
p1, p2: ptr
{{fun h : heap =>
  (exists n1 : nat, lookup h p1 = Some (Nat_t n1)) /\
  (exists n2 : nat, lookup h p2 = Some (Nat_t n2))}} 
inc p1
{{fun (h1 : heap) (_ : unit) (h2 : heap) =>
  (exists n1 : nat,
     lookup h1 p1 = Some (Nat_t n1) /\
     lookup h2 p1 = Some (Nat_t (1 + n1))) /\
  (exists n2 : nat,
     lookup h1 p2 = Some (Nat_t n2) /\
     lookup h2 p2 = Some (Nat_t n2))}}
  eapply consequence_tc.
p1, p2: ptr
{{?P1}} inc p1 {{?Q1}}
p1, p2: ptr
forall h : heap,
(exists n1 : nat, lookup h p1 = Some (Nat_t n1)) /\
(exists n2 : nat, lookup h p2 = Some (Nat_t n2)) ->
?P1 h
p1, p2: ptr
forall (h : heap) (x : unit) (h' : heap),
?Q1 h x h' ->
(exists n1 : nat,
   lookup h p1 = Some (Nat_t n1) /\
   lookup h' p1 = Some (Nat_t (1 + n1))) /\
(exists n2 : nat,
   lookup h p2 = Some (Nat_t n2) /\
   lookup h' p2 = Some (Nat_t n2))
  -
p1, p2: ptr
{{?P1}} inc p1 {{?Q1}} apply inc_tc.
  -
p1, p2: ptr
forall h : heap,
(exists n1 : nat, lookup h p1 = Some (Nat_t n1)) /\
(exists n2 : nat, lookup h p2 = Some (Nat_t n2)) ->
(fun h0 : heap =>
 exists n : nat, lookup h0 p1 = Some (Nat_t n)) h memsimp.
  -
p1, p2: ptr
forall (h : heap) (x : unit) (h' : heap),
(fun (h1 : heap) (_ : unit) (h2 : heap) =>
 exists n : nat,
   lookup h1 p1 = Some (Nat_t n) /\
   lookup h2 p1 = Some (Nat_t (1 + n))) h x h' ->
(exists n1 : nat,
   lookup h p1 = Some (Nat_t n1) /\
   lookup h' p1 = Some (Nat_t (1 + n1))) /\
(exists n2 : nat,
   lookup h p2 = Some (Nat_t n2) /\
   lookup h' p2 = Some (Nat_t n2)) memsimp.
p1, p2: ptr
h: heap
x: unit
h': heap
x0: nat
H: lookup h p1 = Some (Nat_t x0)
H0: lookup h' p1 = Some (Nat_t (S x0))
exists n2 : nat,
  lookup h p2 = Some (Nat_t n2) /\
  lookup h' p2 = Some (Nat_t n2)
Abort.

The problem is even more compounded when we use abstract predicates, which are necessary to get at the notion of abstract types. Here, the inc provider has no way to anticipate what properties P might be preserved by inc, since P could talk about any property of the heap.

Definition problem2 (p1 : ptr)(P : hprop) :
  {{ fun h => (exists n1, lookup h p1 = Some (Nat_t n1)) /\ P h }}
  inc p1
  {{ fun h1 _ h2 =>
       (exists n1, lookup h1 p1 = Some (Nat_t n1) /\
                   lookup h2 p1 = Some (Nat_t (1+n1)))
       (* /\ P h2 *) }}.
p1: ptr
P: hprop
{{fun h : heap =>
  (exists n1 : nat, lookup h p1 = Some (Nat_t n1)) /\
  P h}} inc p1
{{fun (h1 : heap) (_ : unit) (h2 : heap) =>
  exists n1 : nat,
    lookup h1 p1 = Some (Nat_t n1) /\
    lookup h2 p1 = Some (Nat_t (1 + n1))}}
Proof.
p1: ptr
P: hprop
{{fun h : heap =>
  (exists n1 : nat, lookup h p1 = Some (Nat_t n1)) /\
  P h}} inc p1
{{fun (h1 : heap) (_ : unit) (h2 : heap) =>
  exists n1 : nat,
    lookup h1 p1 = Some (Nat_t n1) /\
    lookup h2 p1 = Some (Nat_t (1 + n1))}}
  eapply consequence_tc.
p1: ptr
P: hprop
{{?P1}} inc p1 {{?Q1}}
p1: ptr
P: hprop
forall h : heap,
(exists n1 : nat, lookup h p1 = Some (Nat_t n1)) /\
P h -> ?P1 h
p1: ptr
P: hprop
forall (h : heap) (x : unit) (h' : heap),
?Q1 h x h' ->
exists n1 : nat,
  lookup h p1 = Some (Nat_t n1) /\
  lookup h' p1 = Some (Nat_t (1 + n1))
  -
p1: ptr
P: hprop
{{?P1}} inc p1 {{?Q1}} apply inc_tc.
  -
p1: ptr
P: hprop
forall h : heap,
(exists n1 : nat, lookup h p1 = Some (Nat_t n1)) /\
P h ->
(fun h0 : heap =>
 exists n : nat, lookup h0 p1 = Some (Nat_t n)) h memsimp.
  -
p1: ptr
P: hprop
forall (h : heap) (x : unit) (h' : heap),
(fun (h1 : heap) (_ : unit) (h2 : heap) =>
 exists n : nat,
   lookup h1 p1 = Some (Nat_t n) /\
   lookup h2 p1 = Some (Nat_t (1 + n))) h x h' ->
exists n1 : nat,
  lookup h p1 = Some (Nat_t n1) /\
  lookup h' p1 = Some (Nat_t (1 + n1)) memsimp.
Qed.

To address these problems, we can revise our logic using ideas from separation logic. But that will have to wait for another lecture...