Assignment 2: Separation logic theory

October 4, 2024

Assignment 2: Separation logic theory

Info

This is a theory assignment: you'll submit written responses rather than doing proofs in a computer.

In this assignment, you'll answer some questions about Hoare logic and separation logic on paper rather than submitting mechanized proofs. The goal is to build and exercise your mental model for the specifications, proof rules, and program proofs, without having to work out all the details or translate your argument to something Coq understands. The two downsides are that you have to do all the calculations yourself, and there's no computer patiently checking your work and confirming when you're done; you'll have to think about it and wait for (much slower) feedback from me.

%% basic math \gdef\intersect{\cap} \gdef\union{\cup} \gdef\dom{\operatorname{dom}} \gdef\disjoint{\mathrel{\bot}} \gdef\finto{\overset{\text{fin}}{\rightharpoonup}} \gdef\listapp{\mathbin{+\mkern-10mu+}} \gdef\bool{\operatorname{bool}} \gdef\box{\Box} \gdef\iProp{\operatorname{iProp}} \gdef\Prop{\operatorname{Prop}} %% language \gdef\ife#1#2#3{\text{\textbf{if} } #1 \text{ \textbf{then} } #2 \text{ \textbf{else} } #3} \gdef\lete#1#2{\text{\textbf{let} } #1 := #2 \text{ \textbf{in} }} \gdef\letV#1#2{&\text{\textbf{let} } #1 := #2 \text{ \textbf{in} }} \gdef\num#1{\overline{#1}} \gdef\true{\mathrm{true}} \gdef\false{\mathrm{false}} \gdef\skip{\mathrm{skip}} \gdef\fun#1{\lambda #1.\,} \gdef\funblank{\fun{\_}} \gdef\rec#1#2{\text{\textbf{rec} } #1 \; #2.\;\,} \gdef\app#1#2{#1 \, #2} \gdef\then{;\;} \gdef\assert#1{\operatorname{assert} \, #1} \gdef\val{\mathrm{val}} \gdef\purestep{\xrightarrow{\text{pure}}} \gdef\spawn{\text{\textbf{spawn}}} %% hoare logic \gdef\False{\mathrm{False}} \gdef\True{\mathrm{True}} \gdef\hoare#1#2#3{\left\{#1\right\} \, #2 \, \left\{#3\right\}} \gdef\hoareV#1#2#3{\begin{aligned}% &\left\{#1\right\} \\ &\quad #2 \\ &\left\{#3\right\}% \end{aligned}} \gdef\wp{\operatorname{wp}} \gdef\outlineSpec#1{\left\{#1\right\}} \gdef\entails{\vdash} \gdef\bient{\dashv\vdash} \gdef\eqnlabel#1{\:\:\text{#1}} \gdef\lift#1{\lceil #1 \rceil} %% separation logic % imperative constructs \gdef\load#1{{!}\,#1} \gdef\store#1#2{#1 \mathbin{\gets} #2} \gdef\free#1{\operatorname{free} \, #1} \gdef\alloc#1{\operatorname{alloc} \, #1} % logic \gdef\sep{\mathbin{\raisebox{1pt}{$\star$}}} %% Iris actually uses \ast (6-pointed) not \star (5-pointed) %\gdef\sep{\mathbin{\ast}} \gdef\bigsep{\mathop{\vcenter{\LARGE\hbox{$\star$}}}} \gdef\bigast{\mathop{\vcenter{\LARGE\hbox{$\ast$}}}} \gdef\wand{\mathbin{\raisebox{1pt}{$-\hspace{-0.06em}\star$}}} \gdef\emp{\mathrm{emp}} \gdef\pointsto{\mapsto} \gdef\Heap{\mathrm{Heap}} \gdef\Loc{\mathrm{loc}} \gdef\valid{\text{\checkmark}} \gdef\pcore{\operatorname{pcore}} \gdef\errorval{\bot} \gdef\option{\operatorname{option}} \gdef\Some{\operatorname{Some}} \gdef\None{\operatorname{None}} \gdef\own{\operatorname{own}} %% concurrent separation logic \gdef\isLock{\mathrm{isLock}} % \pvs is the iris.sty macro for a basic update modality (without the super dot) \gdef\pvs{\mathord{{{\mid\kern-0.5ex\Rrightarrow\kern-0.25ex}}\kern0.2ex}} \gdef\vs{\Rrightarrow} \gdef\vsWand{\displaystyle\equiv\kern-1.6ex-\kern-1.5ex\smash{\bigast}\kern-0.2ex} % frame-preserving updates (macro matches iris.sty) \gdef\mupd{\rightsquigarrow}

This assignment is due Tuesday, Oct 22, 2024 at 11pm. Submit solutions to Canvas. You can submit either handwritten (digital or paper) answers, or typeset your solution with LaTeX using the assignment 2 template .

Exercise 1

Rule of consequence (5 points)

Prove the rule of consequence for Hoare logic, from the soundness definition for a Hoare triple.

Exercise 2

Understanding separation logic propositions (10 points)

For each separation logic proposition below, describe precisely the set of heaps where it is true. If you think the answer is non-trivial or are unsure of your answer, briefly explain so I can see your thought process. Assume a linear separation logic - remember that $\True(h)$ holds for any heap, even in a linear logic.

Note that the overlapping conjunction $(P \land Q)(h)$ is defined to be true when $P(h)$ and $Q(h)$ . While not commonly used, this is a perfectly valid separation logic proposition.

If a variable is free (that is, not bound by a $\forall$ or $\exists$ quantifier), assume it to be a constant throughout the problem (but each problem is independent).

Here is a worked example:

$\ell_1 \mapsto v \sep \ell_2 \mapsto v$ . If $\ell_1 \neq \ell_2$ , holds for only the two-element heap $\{\ell_1 \mapsto v; \ell_2 \mapsto v\}$ ; if $\ell_1 = \ell_2$ , never holds.

(a) $\exists v.\, \ell \pointsto v$
(b) $\exists \ell'.\, \ell' \pointsto v$
(c) $\forall v.\, \ell \pointsto v$
(d) $(\ell \pointsto v) \sep \True$
(e) $(\ell \pointsto v) \sep (\True \land \emp)$
(f) $\ell \pointsto v \land \ell \pointsto v$
(g) $\ell \pointsto v \sep \ell \pointsto v$
(h) $(\exists v.\, \ell_1 \pointsto v) \sep (\exists \ell.\, \ell \pointsto \num{3})$
(i) $(\exists v.\, \ell \pointsto v) \land (\exists \ell'.\, \ell' \pointsto \num{3})$
(j) $(\exists x. \lift{x > 2}) \sep (\exists x. \lift{x < 2})$

Exercise 3

Frame rule vs consequence (10 points)

Compare the separation logic frame rule to the consequence/weaken rule. Explain why the consequence rule does not imply the frame rule. Explain why the frame rule does not imply the consequence rule. These explanations are not meant to be fully formal proofs (which is well beyond the scope of this class for this question), but should aim to be convincing explanations - in this case, convincing me that you've understood what these rules mean.

Rule of consequence = weaken rule

This assignment originally only used the term "weaken rule", but the notes say "rule of consequence". These are the same thing; sorry for the confusion. Note that this question not referring to weakening propositions, $P \sep Q \entails P$ .

Exercise 4

A bug in separation logic? (15 points)

Your friend Ben Bitdiddle has read the section on recursion and loops and thinks he has found a bug in separation logic. He claims to have proven the following triple:

\hoare{\True}{(\rec{f}{x} f \, x) \, ()}{\fun{\_} \False}

"This proves False with no hypotheses, which makes separation logic unsound!" he exclaims, a little too excited at having broken what you spent so much time learning.

What do you say to Ben?

Exercise 5

Verifying linked list implementation (35 points, total)

We will develop a linked list implementation in our "lecture notes" programming language (which I'll call expr here) and give it a specification using a representation predicate.

This problem will follow the presentation of linked lists in Robbert Krebbers's program verification course. We will be following the notes from that class on separation logic.

Exercise 5a

Reading (0 points)

Read the notes linked above. You should be able to skim the first part, since it's very similar to our own class notes. The new material relevant to this problem starts at Linked data structures and representation predicates.

Be careful reading the notation: code in the language is written in Coq syntax, with type annotations to clarify what's going on, but these are not functional programs. The types are mostly straightforward to understand, except that ref T is used for a pointer to a T (ref stands for "reference"); a value of this type will always be a location, and when dereferenced will return a value of type T. The syntax alloc, !x, and x ← v is the same as our programming language.

Our language did not have a way of doing pattern matching, which makes it awkward to implement linked lists. For the purpose of this exercise let's assume it has a way to represent the inductive type for a linked list holding values of type A:

llist A :=
| lnil
| lcons (hd: A) (tl: ref (llist A))

Notice that this is not like the Coq list A type in that the tl field is a pointer to the rest of the list.

To use this inductive, we need pattern matching. Assume a match construct in expr that behaves like Coq's match; here's an example, the sum_list from the notes linked above:

Fixpoint sum_list (x: ref nat) (l: ilist nat) :=
  match l
  | lnil => ()
  | lcons hd tl =>
    x <- !x + hd
    let k := !tl in
    sum_list x k
  end

We use Fixpoint for clarity but this function can also be written using the recursive anonymous function $\rec{f}{x}{e}$ in the notes.

The program verification notes linked above include several examples of proof outlines, especially those using pattern matching.

To specify functions over linked lists, we will use the following representation invariant for linked lists (this is a Coq definition for a separation logic proposition, except that v would just be a val; we give here its type in the expr language for clarity):

Fixpoint list_rep (v: llist A) (xs: list A): hProp :=
  match xs with
  | [] => v = lnil
  | hd :: xs' => ∃ tl v',
     (v = lcons hd tl) ∗
     (tl ↦ v') ∗
     list_rep v' xs'
   end.

This definition says that v is the value of a linked list that holds abstract values xs in the current heap. It relates a programming value v, which has references, to a purely mathematical list. Importantly, list_rep is a separation logic proposition hProp; it only makes sense to have a linked list in some heap, since the code representation involves pointers. However the mathematical part does not involve pointers.

This is the separation logic analog to the ADT specifications we saw earlier for functional programs. The model of a linked list will be a Coq list, as expected. We will be using abstraction relations rather than functions. If linked lists were implemented in a functional programming language, we would specify sum_list using an abstraction relation list_absr l xs : Prop that said ∀ l xs, list_absr l xs → sum_list l = sum xs. Now, a similar specification is written as a triple {list_rep l xs} sum_list l {λv. v = sum xs * list_rep l xs}. Notice that we need to re-state list_rep l xs in the postcondition; otherwise, the specification allows sum_list to de-allocate l, or re-use its memory for something else.

Side note: where does "xs" come from?

The name xs is meant to evoke xs, the plural of x. It's a common variable name for a list of values (similarly you'll see ys) in functional languages like OCaml or Haskell.

This shorthand is also useful for a reference to a linked list, since that is how the tail is stored in an llist A:

Definition list_ref_rep (v: ref (llist A)) (xs: list A): hProp :=
  ∃ (p: loc) (l: llist A), (v = p) * (p ↦ l) * list_rep l xs.

There is nothing to turn in for this part.

Exercise 5b

Specification for append (10 points)

Consider the following function for appending two linked lists. It's your job to figure out exactly how it works (that is, how does it manage the memory of the two lists?).

Fixpoint app_list (l1: ref (llist A)) (l2: ref (llist A)) :=
  match !l1 with
  | lnil => l1 <- !l2; free l2; ()
  | lcons hd tl => app_list tl l2
  end.

Write a specification for app_list l1 l2. You may assume an affine separation logic, so the postcondition can drop any facts you don't think are relevant.

Exercise 5c

Proof of append (15 points)

Write a proof outline that shows app_list l1 l2 meets your specification. You may assume an affine separation logic.

Remember that if you think something is wrong here, you may need to re-visit your specification. I can check your specification and give feedback before you spend too much time proving it.

Exercise 5d

Specification for tail (10 points)

Let us now implement a function to get the tail of a list:

Definition tail (l: llist A) : llist A :=
match l with
| lnil => ()
| lcons hd tl => !tl
end.

Consider the following specification for tail:

[ list_rep l (x :: xs) ]
  tail l
[ v. list_rep l (x :: xs) * list_rep v xs ]

Is this specification true? If yes, prove this specification. If not, explain why, find another valid specification, and prove it.

Bonus exercise (optional)

5-15 bonus points (depending on importance of contribution)

Find a typo in the lecture notes on Hoare logic or Separation Logic. Submit a GitHub pull request with a fix.