Separation logic

AbbreviationHeap assertion#✓fully proved

A heap assertion is a predicate on a store and a heap: it assigns a proposition to every store \(s\) and every heap \(h\). Heap assertions serve as the preconditions and postconditions of separation logic.

abbrev HAssertion := State → Heap → Prop

Uses 2 · Used by 18

Statement usesHeap · IMP program states

Used byAssignment rule with a store-irrelevant heap assertion · Empty-heap assertion · Entailment of heap assertions · Existential rule for separation-logic triples · Frame rule · Store-irrelevant frames satisfy the frame-rule side condition · Conjunction of heap assertions · Existential heap assertion · Framed embedding of Hoare validity · Points-to assertion · Pure assertion · Local rule for a heap read · Separation-logic triple validity · Separating conjunction · Pulling a store fact out of a separating conjunction · Rearranging a separating conjunction · Store-irrelevant heap assertions · Separation-logic while rule

DefinitionEntailment of heap assertions#✓fully proved

A heap assertion \(P\) entails a heap assertion \(Q\) when, for every store \(s\) and every heap \(h\), if \(P\) holds of \(s\) and \(h\), then \(Q\) holds of \(s\) and \(h\).

def Entails (P Q : HAssertion) : Prop :=
  ∀ ⦃s h⦄, P s h → Q s h

Uses 3 · Used by 3

Statement usesHeap assertion · Heap · IMP program states

Used byAssignment rule with a store-irrelevant heap assertion · Local rule for a heap read · Rearranging a separating conjunction

DefinitionEmpty-heap assertion#✓fully proved

The heap assertion \(\mathrm{emp}\) holds of a store \(s\) and a heap \(h\) exactly when \(h\) is the empty heap, whatever the store \(s\) is.

def emp : HAssertion := fun _ h => h = ∅

Uses 3

Statement usesHeap assertion · Heap · IMP program states

DefinitionPure assertion#✓fully proved

For a proposition \(p\), the pure assertion of \(p\) holds of a store \(s\) and a heap \(h\) exactly when \(h\) is the empty heap and \(p\) is true.

def pure (p : Prop) : HAssertion := fun _ h => h = ∅ ∧ p

Uses 3

Statement usesHeap assertion · Heap · IMP program states

DefinitionPoints-to assertion#✓fully proved

For natural numbers \(a\) and \(v\), the assertion \(a \mapsto v\) holds of a store \(s\) and a heap \(h\) exactly when \(h\) is the singleton heap that maps the address \(a\) to the value \(v\) and allocates no other address.

def pointsTo (a v : Nat) : HAssertion :=
  fun _ h => h = Finmap.singleton a v

Uses 3 · Used by 1

Statement usesHeap assertion · Heap · IMP program states

Used byLocal rule for a heap read

DefinitionSeparating conjunction#✓fully proved

For heap assertions \(P\) and \(Q\), the assertion \(P \star Q\) holds of a store \(s\) and a heap \(h\) when there are disjoint heaps \(h_1\) and \(h_2\) with \(h = h_1 \cup h_2\) such that \(P(s, h_1)\) and \(Q(s, h_2)\).

def star (P Q : HAssertion) : HAssertion :=
  fun s h => ∃ h₁ h₂, Heap.Disjoint h₁ h₂ ∧ h = h₁ ∪ h₂ ∧ P s h₁ ∧ Q s h₂

Uses 4 · Used by 4

Statement usesHeap assertion · Heap · Disjoint heaps · IMP program states

Used byFrame rule · Framed embedding of Hoare validity · Pulling a store fact out of a separating conjunction · Rearranging a separating conjunction

DefinitionExistential heap assertion#✓fully proved

For a function \(p\) assigning a heap assertion \(p(n)\) to each natural number \(n\) (an address or a value), the assertion \(\exists n,\ p(n)\) holds of a store \(s\) and a heap \(h\) exactly when \(p(n)\) holds of \(s\) and \(h\) for some natural number \(n\).

def hexists (p : Nat → HAssertion) : HAssertion :=
  fun s h => ∃ a, p a s h

Uses 3

Statement usesHeap assertion · Heap · IMP program states

DefinitionConjunction of heap assertions#✓fully proved

For heap assertions \(P\) and \(Q\), the assertion \(P \wedge Q\) holds of a store \(s\) and a heap \(h\) exactly when \(P\) holds of \(s\) and \(h\) and \(Q\) holds of \(s\) and the same heap \(h\).

def hand (P Q : HAssertion) : HAssertion :=
  fun s h => P s h ∧ Q s h

Uses 3

Statement usesHeap assertion · Heap · IMP program states

DefinitionSeparation-logic triple validity#✓fully proved

For heap assertions \(P\), \(Q\) and a heap command \(c\), the triple \(\lbrace P \rbrace\ c\ \lbrace Q \rbrace\) is valid (in the fault-avoiding sense) when, for every store \(s\) and heap \(h\) with \(P(s, h)\), the configuration \((c, s, h)\) is safe (no configuration reachable from it is stuck at a command other than \(\mathtt{skip}\)), and whenever \((c, s, h)\) reaches \((\mathtt{skip}, s', h')\) in finitely many heap steps, \(Q(s', h')\) holds.

def SepValid (P : HAssertion) (c : HeapCmd) (Q : HAssertion) : Prop :=
  ∀ ⦃s h⦄, P s h → Safe (c, s, h) ∧
    ∀ ⦃s' h'⦄, HSteps (c, s, h) (.skip, s', h') → Q s' h'

Uses 6 · Used by 7

Statement usesHeap assertion · Multi-step heap execution · Heap · Heap commands · Safe heap configurations · IMP program states

Used byAssignment rule with a store-irrelevant heap assertion · Existential rule for separation-logic triples · Frame rule · Hoare validity embeds into separation validity · Framed embedding of Hoare validity · Local rule for a heap read · Separation-logic while rule

TheoremSeparation-logic while rule#✓fully proved

Let \(I\) be a heap assertion, \(b\) a Boolean expression and \(c\) a heap command. Write \(I \wedge b\) for the assertion that holds of a store \(s\) and a heap \(h\) when \(I(s, h)\) holds and \(b\) evaluates to true in \(s\), and \(I \wedge \neg b\) for the one that holds when \(I(s, h)\) holds and \(b\) evaluates to false in \(s\). If the triple \(\lbrace I \wedge b \rbrace\ c\ \lbrace I \rbrace\) is valid, then so is the triple \(\lbrace I \rbrace\ \mathtt{while}\ b\ \mathtt{do}\ c\ \lbrace I \wedge \neg b \rbrace\).

theorem whileLoop {I : HAssertion} {guard : BExp} {body : HeapCmd}
    (hbody : SepValid (fun s h => I s h ∧ guard.eval s = true) body I) :
    SepValid I (.while guard body)
      (fun s h => I s h ∧ guard.eval s = false)

Uses 13

Statement usesBoolean expressions of IMP · Evaluation of IMP Boolean expressions · Heap assertion · Heap · Heap commands · Separation-logic triple validity · IMP program states

Proof usesArithmetic expressions of IMP · Evaluation of IMP arithmetic expressions · Heap configurations · Small-step semantics of heap commands · Multi-step heap execution · Safe heap configurations

TheoremFrame rule#✓fully proved

Let \(P\), \(Q\) and \(R\) be heap assertions and \(c\) a heap command. Suppose the separation-logic triple with precondition \(P\), command \(c\) and postcondition \(Q\) is valid, and suppose that whenever \(R\) holds of a store \(s\) and a heap \(h\), it also holds of \(s'\) and \(h\) for every store \(s'\) that agrees with \(s\) on every variable outside the set of variables that \(c\) may assign to. Then the triple with precondition \(P \star R\), command \(c\) and postcondition \(Q \star R\) is valid, where \(\star\) denotes separating conjunction.

theorem frame {P Q R : HAssertion} {c : HeapCmd}
    (hvalid : SepValid P c Q)
    (hR : ∀ ⦃s h s'⦄, R s h →
      (∀ x, x ∉ c.modVars → s' x = s x) → R s' h) :
    SepValid (P ⋆ R) c (Q ⋆ R)

Uses 15 · Used by 1

Statement usesHeap assertion · Separating conjunction · Heap · Heap commands · Modified variables of a heap command · Separation-logic triple validity · IMP program states

Proof usesHeap configurations · Small-step semantics of heap commands · Adding a frame heap preserves the ability to step · Multi-step heap execution · Frame decomposition of heap executions · Heap executions only change assignable variables · Disjoint heaps · Safe heap configurations

Used byFramed embedding of Hoare validity

TheoremHoare validity embeds into separation validity#✓fully proved

Let \(P\) and \(Q\) be store assertions and \(c\) a command of plain IMP. If the partial-correctness Hoare triple with precondition \(P\), command \(c\) and postcondition \(Q\) is valid, then the separation-logic triple for the embedding of \(c\) into heap IMP is valid with the precondition that holds of a store \(s\) and any heap exactly when \(P(s)\) holds and the postcondition that holds of a store \(s\) and any heap exactly when \(Q(s)\) holds.

Embedded commands are always safe, never change the heap, and terminate exactly when the plain command does.

theorem of_valid {P Q : Assertion} {c : Cmd} (hvalid : Valid P c Q) :
    SepValid (fun s _ => P s) c.toHeap (fun s _ => Q s)

Uses 17 · Used by 1

Statement usesAssertion · Commands of IMP · Embedding of IMP into the heap language · Heap · Separation-logic triple validity · IMP program states · Validity of a Hoare triple

Proof usesArithmetic expressions of IMP · Boolean expressions of IMP · Multi-step heap execution · Executions of embedded commands are plain executions · Heap commands · Safe heap configurations · IMP multi-step relation · Termination of an IMP command · Hoare validity via small-step termination · Embedded plain commands are safe

Used byFramed embedding of Hoare validity

TheoremFramed embedding of Hoare validity#✓fully proved

Let \(P\) and \(Q\) be store assertions, \(R\) a heap assertion and \(c\) a command of plain IMP, and write \(\hat c\) for the embedding of \(c\) into heap IMP. Suppose the partial-correctness Hoare triple with precondition \(P\), command \(c\) and postcondition \(Q\) is valid, and suppose that whenever \(R\) holds of a store \(s\) and a heap \(h\), it also holds of \(s'\) and \(h\) for every store \(s'\) that agrees with \(s\) on every variable outside the set of variables that \(\hat c\) may assign to. Write \(\tilde P\) and \(\tilde Q\) for the heap assertions that hold of a store \(s\) and any heap exactly when \(P(s)\), respectively \(Q(s)\), holds. Then the separation-logic triple with precondition \(\tilde P \star R\), command \(\hat c\) and postcondition \(\tilde Q \star R\) is valid, where \(\star\) denotes separating conjunction.

theorem of_valid_frame {P Q : Assertion} {R : HAssertion} {c : Cmd}
    (h : Valid P c Q)
    (hR : ∀ ⦃s h s'⦄, R s h →
      (∀ x, x ∉ c.toHeap.modVars → s' x = s x) → R s' h) :
    SepValid ((fun s _ => P s) ⋆ R) c.toHeap ((fun s _ => Q s) ⋆ R)

Uses 12

Statement usesAssertion · Commands of IMP · Embedding of IMP into the heap language · Heap assertion · Separating conjunction · Heap · Modified variables of a heap command · Separation-logic triple validity · IMP program states · Validity of a Hoare triple

Proof usesFrame rule · Hoare validity embeds into separation validity

DefinitionStore-irrelevant heap assertions#✓fully proved

A heap assertion \(P\) is store-irrelevant when for all stores \(s, s'\) and every heap \(h\), \(P(s, h)\) implies \(P(s', h)\); that is, whether \(P\) holds does not depend on the store.

The empty-heap and points-to assertions are store-irrelevant, and so is the separating conjunction of two store-irrelevant assertions.

def StoreIrrel (P : HAssertion) : Prop :=
  ∀ (s s' : State) (h : Heap), P s h → P s' h

Uses 3 · Used by 2

Statement usesHeap assertion · Heap · IMP program states

Used byAssignment rule with a store-irrelevant heap assertion · Store-irrelevant frames satisfy the frame-rule side condition

TheoremStore-irrelevant frames satisfy the frame-rule side condition#✓fully proved

Let \(R\) be a store-irrelevant heap assertion and \(c\) a heap command. For all stores \(s, s'\) and every heap \(h\), if \(R(s, h)\) holds and \(s'(x) = s(x)\) for every variable \(x\) outside the set of variables that \(c\) may assign to, then \(R(s', h)\) holds.

This is the side condition on the frame in the frame rule.

theorem frame_of_storeIrrel {R : HAssertion} (hR : StoreIrrel R)
    (c : HeapCmd) :
    ∀ ⦃s : State⦄ ⦃h : Heap⦄ ⦃s' : State⦄, R s h →
      (∀ x, x ∉ c.modVars → s' x = s x) → R s' h

Uses 6

Statement usesHeap assertion · Heap · Heap commands · Modified variables of a heap command · IMP program states · Store-irrelevant heap assertions

TheoremPulling a store fact out of a separating conjunction#✓fully proved

Let \(p\) be a predicate on stores and \(P\), \(R\) heap assertions. Write \(A \star B\) for the separating conjunction of heap assertions \(A\) and \(B\) (the heap splits into two disjoint parts satisfying \(A\) and \(B\), respectively, at the same store), and \(p \land P\) for the heap assertion that holds at store \(s\) and heap \(h\) when \(p(s)\) and \(P(s, h)\) both hold. Then \((p \land P) \star R = p \land (P \star R)\).

This lets framed local triples be stated with the store facts kept outside the separating conjunction.

theorem star_and_left {p : State → Prop} {P R : HAssertion} :
    ((fun s h => p s ∧ P s h) ⋆ R) = (fun s h => p s ∧ (P ⋆ R) s h)

Uses 5

Statement usesHeap assertion · Separating conjunction · Heap · IMP program states

Proof usesDisjoint heaps

TheoremRearranging a separating conjunction#✓fully proved

For heap assertions \(P\), \(Q\) and \(R\), write \(A \star B\) for the separating conjunction of heap assertions \(A\) and \(B\) (the heap splits into two disjoint parts satisfying \(A\) and \(B\), respectively, at the same store). Then \(P \star (Q \star R)\) entails \((P \star R) \star Q\): every store and heap satisfying the first assertion satisfy the second.

theorem star_swap_right {P Q R : HAssertion} :
    (P ⋆ (Q ⋆ R)).Entails ((P ⋆ R) ⋆ Q)

Uses 7

Statement usesHeap assertion · Entailment of heap assertions · Separating conjunction

Proof usesHeap · Disjoint heaps · Symmetry of heap disjointness · IMP program states

TheoremLocal rule for a heap read#✓fully proved

Let \(x\) and \(y\) be variables, let \(a\) and \(v\) be natural numbers, and let \(p\) and \(q\) be predicates on stores. Write \(s[x := n]\) for the store that agrees with \(s\) except that it maps \(x\) to \(n\), and \(a \mapsto v\) for the heap assertion that holds when the heap is the single cell at address \(a\) holding \(v\). If every store \(s\) satisfying \(p\) has \(s(y) = a\) and \(q(s[x := v])\), then the separation-logic triple for the heap read \(x := [y]\) (which loads into \(x\) the value stored at the address held in \(y\)) is valid with precondition "\(p(s)\) and \(a \mapsto v\) holds at \((s, h)\)" and postcondition "\(q(s)\) and \(a \mapsto v\) holds at \((s, h)\)", where \(s\) is the store and \(h\) the heap.

theorem read_local {name addrName a v : Nat} {p q : State → Prop}
    (hpq : ∀ s, p s → s addrName = a ∧
      q (Function.update s name v)) :
    SepValid (fun s h => p s ∧ pointsTo a v s h)
      (.read name (.var addrName))
      (fun s h => q s ∧ pointsTo a v s h)

Uses 15

Statement usesArithmetic expressions of IMP · Points-to assertion · Heap · Heap commands · Separation-logic triple validity · IMP program states

Proof usesEvaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Heap assertion · Entailment of heap assertions · Heap configurations · Small-step semantics of heap commands · Multi-step heap execution · Safe heap configurations

TheoremAssignment rule with a store-irrelevant heap assertion#✓fully proved

Let \(x\) and \(y\) be variables, let \(p\) and \(q\) be predicates on stores, and let \(H\) be a store-irrelevant heap assertion. Write \(s[x := n]\) for the store that agrees with \(s\) except that it maps \(x\) to \(n\). If every store \(s\) satisfying \(p\) has \(q(s[x := s(y)])\), then the separation-logic triple for the assignment \(x := y\) is valid with precondition "\(p(s)\) and \(H(s, h)\)" and postcondition "\(q(s)\) and \(H(s, h)\)", where \(s\) is the store and \(h\) the heap.

An assignment leaves the heap untouched, so no framing is needed.

theorem assign_step {name src : Nat} {p q : State → Prop}
    {H : HAssertion} (hH : StoreIrrel H)
    (hpq : ∀ s, p s → q (Function.update s name (s src))) :
    SepValid (fun s h => p s ∧ H s h) (.assign name (.var src))
      (fun s h => q s ∧ H s h)

Uses 15

Statement usesArithmetic expressions of IMP · Heap assertion · Heap · Heap commands · Separation-logic triple validity · IMP program states · Store-irrelevant heap assertions

Proof usesEvaluation of IMP arithmetic expressions · Boolean expressions of IMP · Evaluation of IMP Boolean expressions · Entailment of heap assertions · Heap configurations · Small-step semantics of heap commands · Multi-step heap execution · Safe heap configurations

TheoremExistential rule for separation-logic triples#✓fully proved

Let \(c\) be a heap command, let \(\iota\) be an arbitrary index (any type or proposition), and let \(P_i\) and \(Q_i\) be heap assertions for each \(i\) in \(\iota\). If for every \(i\) the triple with precondition \(P_i\), command \(c\) and postcondition \(Q_i\) is valid, then the triple with precondition "there is \(i\) with \(P_i\)", command \(c\) and postcondition "there is \(i\) with \(Q_i\)" is valid.

theorem SepValid.exists {ι : Sort*} {P Q : ι → HAssertion} {c : HeapCmd}
    (hstep : ∀ i, SepValid (P i) c (Q i)) :
    SepValid (fun s h => ∃ i, P i s h) c (fun s h => ∃ i, Q i s h)

Uses 7

Statement usesHeap assertion · Heap · Heap commands · Separation-logic triple validity · IMP program states

Proof usesMulti-step heap execution · Safe heap configurations

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.