# AffineAffine Separation Logic

Set Implicit Arguments.

From SLF Require Rules.

From SLF Require Export LibSepReference.

Implicit Types f : var.

Implicit Types b : bool.

Implicit Types v : val.

Implicit Types h : heap.

Implicit Types P : Prop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

From SLF Require Rules.

From SLF Require Export LibSepReference.

Implicit Types f : var.

Implicit Types b : bool.

Implicit Types v : val.

Implicit Types h : heap.

Implicit Types P : Prop.

Implicit Types H : hprop.

Implicit Types Q : val→hprop.

# First Pass

- first, we recall the example illustrating the limitation of a logic without a discard rule for a garbage-collected language;
- second, we present several versions of the "discard rule";
- third, we show how to refine the definition of Separation Logic triples in such a way that the discard rules are satisfied for certain classes of heap predicates.

Recall the example of the function succ_using_incr_attempt from chapter
Basic. This function allocates a reference with contents n, then
increments that reference, and finally returning its contents, that is,
n+1. Let us revisit this example, this time with the intention of
establishing for it a postcondition that does not leak the existence of a
left-over reference cell.

In the framework developed so far, the heap predicate describing the
reference cell allocated by the function cannot be discarded, because the
code does not include a deallocation operation. Thus, we are forced to
include in the postcondition the description of a left-over reference with a
heap predicate, e.g., \∃ p, p ~~> (n+1), or \∃ p m, p ~~> m.

Lemma triple_succ_using_incr : ∀ (n:int),

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1] \* \∃ p, (p ~~> (n+1))).

Proof using.

xwp. xapp. intros p. xapp. xapp. xsimpl. auto.

Qed.

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1] \* \∃ p, (p ~~> (n+1))).

Proof using.

xwp. xapp. intros p. xapp. xapp. xsimpl. auto.

Qed.

If we try to prove a specification that does not mention the left-over
reference, then we get stuck with a proof obligation of the form
p ~~> (n+1) ==> \[].

Lemma triple_succ_using_incr' : ∀ (n:int),

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

xwp. xapp. intros p. xapp. xapp. xsimpl. { auto. } (* stuck here *)

Abort.

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

xwp. xapp. intros p. xapp. xapp. xsimpl. { auto. } (* stuck here *)

Abort.

In what follows, we extend our Separation Logic with a "discard rule" that
allows proving the above specification for succ_using_incr.

## Statement of The Discard Rule

Let us show that, using the rule triple_hany_post, we can derive the
desired specification for the motivating example from the specification that
mentions the left-over postcondition.

Module MotivatingExampleSolved.

Export MotivatingExample.

Lemma triple_succ_using_incr' : ∀ (n:int),

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

intros. applys triple_hany_post. applys triple_succ_using_incr.

Qed.

End MotivatingExampleSolved.

Export MotivatingExample.

Lemma triple_succ_using_incr' : ∀ (n:int),

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

intros. applys triple_hany_post. applys triple_succ_using_incr.

Qed.

End MotivatingExampleSolved.

A symmetric rule, named triple_hany_pre, asserts that an arbitrary heap
predicate H' can be dropped from the precondition, simplifying it from
H \* H' to H.

Observe the difference between the two rules. In triple_hany_post, the
discarded predicate H' appears in the premise, reflecting the fact that we
discard it after the evaluation of the term t.
Conversely, in triple_hany_pre, the discarded predicate H' appears in
the conclusion, reflecting the fact that we discard it before the evaluation
of t.
The rules triple_hany_pre and triple_hany_post can be derived from each
other. As we will establish further on, triple_hany_pre is derivable from
triple_hany_post by a simple application of the frame rule. Reciprocally,
triple_hany_post is derivable from triple_hany_pre, though the proof is
slightly more involved. This proof appears in lemma
triple_hgc_post_from_hgc_pre in the "optional material" section.

### Axiomatization of heap_affine and haffine

Module Preview.

Parameter haffine : hprop → Prop.

Parameter triple_haffine_post : ∀ t H H' Q,

haffine H' →

triple t H (Q \*+ H') →

triple t H Q.

Parameter triple_haffine_pre : ∀ t H H' Q,

haffine H' →

triple t H Q →

triple t (H \* H') Q.

End Preview.

Parameter haffine : hprop → Prop.

Parameter triple_haffine_post : ∀ t H H' Q,

haffine H' →

triple t H (Q \*+ H') →

triple t H Q.

Parameter triple_haffine_pre : ∀ t H H' Q,

haffine H' →

triple t H Q →

triple t (H \* H') Q.

End Preview.

The predicate haffine H is defined in terms of a lower-level predicate
heap_affine. The proposition heap_affine h asserts that the piece of
heap h may be freely discarded, in the sense that it does not have to be
accounted for in the program logic. The question of whether a heap or a heap
predicate should be affine or not is to be decided on a case-by-case basis.
It depends on the intention of the designer of the program logic. For the
moment, we leave the predicate heap_affine abstract, and allow it to be
customized later on.

The only assumptions we need to make about heap_affine is that it holds of
the empty heap and that it is preserved by a disjoint union operation.

Parameter heap_affine_empty :

heap_affine Fmap.empty.

Parameter heap_affine_union : ∀ h

heap_affine h

heap_affine h

Fmap.disjoint h

heap_affine (Fmap.union h

heap_affine Fmap.empty.

Parameter heap_affine_union : ∀ h

_{1}h_{2},heap_affine h

_{1}→heap_affine h

_{2}→Fmap.disjoint h

_{1}h_{2}→heap_affine (Fmap.union h

_{1}h_{2}).
We will later show two extreme instantiations: one that leads to a logic
where all predicates are affine (i.e. can be freely discarded), and one that
leads to a logic where all predicates are linear (i.e. none can be freely
discarded, like in our previous set up).

### Definition and Properties of heap_affine

The predicate haffine distributes in a natural way over each of the
operators of Separation Logic -- i.e., the combination of affine heap
predicates yields affine heap predicates. In particular:
The treatment of universal quantifiers can be explained as follows. Consider
a heap h that satisfies \∀ (x:A), H, and consider a particular
value v of type A. The heap h also satisfies [x:=v]H. Thus, if the
heap predicate [x:=v]H can be discarded, the stronger predicate
\∀ (x:A), H can also be discarded.
Existential quantifiers can be explained as follows. Consider a heap h
that satisfies \∃ (x:A), H. We know that there exists a value v of
type A such that h satisfies [x:=v]H. However, we know nothing about
this value v. Therefore, to discard \∃ (x:A), H, we need to know
that [x:=v]H can be discarded for every possible v.

- \[] and \[P], which describe empty heaps, can always be discarded;
- H
_{1}\* H_{2}can be discarded if both H_{1}and H_{2}can be discarded; - \∀ x, H can be discarded if H can be discarded for at least one x;
- \∃ x, H can be discarded if H can be discarded for every x.

Lemma haffine_hempty :

haffine \[].

Proof using.

introv K. lets E: hempty_inv K. subst. applys heap_affine_empty.

Qed.

Lemma haffine_hpure : ∀ P,

haffine \[P].

Proof using.

intros. intros h K. lets (HP&M): hpure_inv K.

subst. applys heap_affine_empty.

Qed.

Lemma haffine_hstar : ∀ H

haffine H

haffine H

haffine (H

Proof using.

introv M

subst. applys* heap_affine_union.

Qed.

Lemma haffine_hexists : ∀ A (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∃ x, (J x)).

Proof using. introv F

Lemma haffine_hforall' : ∀ A (J:A→hprop),

(∃ x, haffine (J x)) →

haffine (\∀ x, (J x)).

Proof using.

introv (x&Hx) M. lets N: hforall_inv M. applys* Hx.

Qed.

haffine \[].

Proof using.

introv K. lets E: hempty_inv K. subst. applys heap_affine_empty.

Qed.

Lemma haffine_hpure : ∀ P,

haffine \[P].

Proof using.

intros. intros h K. lets (HP&M): hpure_inv K.

subst. applys heap_affine_empty.

Qed.

Lemma haffine_hstar : ∀ H

_{1}H_{2},haffine H

_{1}→haffine H

_{2}→haffine (H

_{1}\* H_{2}).Proof using.

introv M

_{1}M_{2}K. lets (h_{1}&h_{2}&K_{1}&K_{2}&D&U): hstar_inv K.subst. applys* heap_affine_union.

Qed.

Lemma haffine_hexists : ∀ A (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∃ x, (J x)).

Proof using. introv F

_{1}(x&Hx). applys* F_{1}. Qed.Lemma haffine_hforall' : ∀ A (J:A→hprop),

(∃ x, haffine (J x)) →

haffine (\∀ x, (J x)).

Proof using.

introv (x&Hx) M. lets N: hforall_inv M. applys* Hx.

Qed.

The rule haffine_hforall' requires the user to provide evidence that there
exists at least one value x of type A for which haffine (J x) is true.
In practice, the user is generally not interested in proving properties of a
specific value x, but is happy to justify that J x is affine for any
x. The corresponding statement appears below, with an assumption Inhab A
asserting that the type A is inhabited. In practice, the \∀
quantifier is always invoked on inhabited types, so this is a benign
restriction.

Lemma haffine_hforall : ∀ A `{Inhab A} (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∀ x, (J x)).

Proof using.

introv IA M. applys haffine_hforall'. ∃ (arbitrary (A:=A)). applys M.

Qed.

(∀ x, haffine (J x)) →

haffine (\∀ x, (J x)).

Proof using.

introv IA M. applys haffine_hforall'. ∃ (arbitrary (A:=A)). applys M.

Qed.

Another useful fact about haffine is that to prove haffine (\[P] \* H)
it is sufficient to prove haffine H under the hypothesis that P is true.
Formally:

Lemma haffine_hstar_hpure_l : ∀ P H,

(P → haffine H) →

haffine (\[P] \* H).

Proof using. introv M. intros h K. rewrite hstar_hpure_l in K. applys* M. Qed.

(P → haffine H) →

haffine (\[P] \* H).

Proof using. introv M. intros h K. rewrite hstar_hpure_l in K. applys* M. Qed.

### Definition of The Affine-Top Predicate

Definition hgc : hprop :=

\∃ H, \[haffine H] \* H.

Declare Scope hgc_scope.

Open Scope hgc_scope.

Notation "\GC" := (hgc) : hgc_scope.

\∃ H, \[haffine H] \* H.

Declare Scope hgc_scope.

Open Scope hgc_scope.

Notation "\GC" := (hgc) : hgc_scope.

The following introduction lemma asserts that \GC h holds when h
satisfies heap_affine.

#### Exercise: 2 stars, standard, especially useful (triple_frame)

Prove that the affine heap predicate holds of any affine heap.#### Exercise: 2 stars, standard, optional (hgc_inv)

Prove the elimination lemma for \GC expressed using heap_affine.
Lemma hgc_eq_heap_affine :

hgc = heap_affine.

Proof using.

intros. applys himpl_antisym.

{ intros h M. applys* hgc_inv. }

{ intros h M. applys* hgc_intro. }

Qed.

hgc = heap_affine.

Proof using.

intros. applys himpl_antisym.

{ intros h M. applys* hgc_inv. }

{ intros h M. applys* hgc_intro. }

Qed.

### Properties of the Affine-Top Predicate

Lemma hstar_hgc_hgc :

(\GC \* \GC) = \GC.

Proof using.

unfold hgc. applys himpl_antisym.

{ xpull. intros H

{ xpull. intros H K. xsimpl H \[]. auto. applys haffine_hempty. }

Qed.

(\GC \* \GC) = \GC.

Proof using.

unfold hgc. applys himpl_antisym.

{ xpull. intros H

_{1}K_{1}H_{2}K_{2}. xsimpl (H_{1}\* H_{2}). applys* haffine_hstar. }{ xpull. intros H K. xsimpl H \[]. auto. applys haffine_hempty. }

Qed.

Another useful property is that the heap predicate \GC itself satisifes
haffine.

Lemma haffine_hgc :

haffine \GC.

Proof using.

applys haffine_hexists. intros H. applys haffine_hstar_hpure_l. auto.

Qed.

haffine \GC.

Proof using.

applys haffine_hexists. intros H. applys haffine_hstar_hpure_l. auto.

Qed.

The process of exploiting \GC to "absorb" affine heap predicates is
captured by the following lemma, which asserts that a heap predicate H
entails \GC whenever H is affine.

Lemma himpl_hgc_r : ∀ H,

haffine H →

H ==> \GC.

Proof using. introv M. intros h K. applys hgc_intro. applys M K. Qed.

haffine H →

H ==> \GC.

Proof using. introv M. intros h K. applys hgc_intro. applys M K. Qed.

In particular, the empty heap predicate \[] entails \GC, because the
empty heap predicate is affine (lemma haffine_hempty).

#### Exercise: 3 stars, standard, especially useful (himpl_hgc_absorb)

Show that \GC * H entails \GC for any H satisfying haffine.
Lemma himpl_hgc_absorb_r : ∀ H,

haffine H →

\GC \* H ==> \GC.

Proof using. (* FILL IN HERE *) Admitted.

☐

haffine H →

\GC \* H ==> \GC.

Proof using. (* FILL IN HERE *) Admitted.

☐

This rule is more concise than triple_haffine_post. Moreover, the piece of
heap being discarded, previously described by H', no longer needs to be
provided up front, at the moment of applying the rule. Instead, it can be
provided further on in the reasoning, by exploiting himpl_hgc_r to prove
an entailment of the form H' ==> \GC.

To set up a fully affine logic, we consider a definition of heap_affine
that holds of any heap.

It is trivial to check that heap_affine satisfies the required
distribution properties on the empty heap and the union of heaps.

Lemma heap_affine_empty :

heap_affine Fmap.empty.

Proof using. rewrite* heap_affine_def. Qed.

Lemma heap_affine_union : ∀ h

heap_affine h

heap_affine h

Fmap.disjoint h

heap_affine (Fmap.union h

Proof using. intros. rewrite* heap_affine_def. Qed.

heap_affine Fmap.empty.

Proof using. rewrite* heap_affine_def. Qed.

Lemma heap_affine_union : ∀ h

_{1}h_{2},heap_affine h

_{1}→heap_affine h

_{2}→Fmap.disjoint h

_{1}h_{2}→heap_affine (Fmap.union h

_{1}h_{2}).Proof using. intros. rewrite* heap_affine_def. Qed.

With that instantiation, haffine holds of any heap predicate.

Lemma haffine_equiv : ∀ H,

(haffine H) ↔ True.

Proof using.

intros. iff M.

{ auto. }

{ unfold haffine. intros. rewrite* heap_affine_def. }

Qed.

(haffine H) ↔ True.

Proof using.

intros. iff M.

{ auto. }

{ unfold haffine. intros. rewrite* heap_affine_def. }

Qed.

Moreover, the affine top predicate \GC is equivalent to the top predicate
htop, defined as fun h ⇒ True or equivalently as \∃ H, H.

Definition htop : hprop :=

\∃ H, H.

Lemma hgc_eq_htop : hgc = htop.

Proof using.

unfold hgc, htop. applys himpl_antisym.

{ xsimpl. }

{ xsimpl. intros. rewrite* haffine_equiv. }

Qed.

End FullyAffineLogic.

\∃ H, H.

Lemma hgc_eq_htop : hgc = htop.

Proof using.

unfold hgc, htop. applys himpl_antisym.

{ xsimpl. }

{ xsimpl. intros. rewrite* haffine_equiv. }

Qed.

End FullyAffineLogic.

To set up a fully affine logic, we consider a definition of heap_affine
that holds only of empty heaps.

Again, it is not hard to check that heap_affine satisfies the required
distributivity properties.

Lemma heap_affine_empty :

heap_affine Fmap.empty.

Proof using. rewrite* heap_affine_def. Qed.

Lemma heap_affine_union : ∀ h

heap_affine h

heap_affine h

Fmap.disjoint h

heap_affine (Fmap.union h

Proof using.

introv K

subst. rewrite* Fmap.union_empty_r.

Qed.

heap_affine Fmap.empty.

Proof using. rewrite* heap_affine_def. Qed.

Lemma heap_affine_union : ∀ h

_{1}h_{2},heap_affine h

_{1}→heap_affine h

_{2}→Fmap.disjoint h

_{1}h_{2}→heap_affine (Fmap.union h

_{1}h_{2}).Proof using.

introv K

_{1}K_{2}D. rewrite heap_affine_def in *.subst. rewrite* Fmap.union_empty_r.

Qed.

With that instantiation, the predicate haffine H is equivalent to
H ==> \[], that is, it characterizes heap predicates that hold of the
empty heap.

Lemma haffine_equiv : ∀ H,

haffine H ↔ (H ==> \[]).

Proof using.

intros. unfold haffine. iff M.

{ intros h K. specializes M K. rewrite heap_affine_def in M.

subst. applys hempty_intro. }

{ intros h K. specializes M K. rewrite heap_affine_def.

applys hempty_inv M. }

Qed.

haffine H ↔ (H ==> \[]).

Proof using.

intros. unfold haffine. iff M.

{ intros h K. specializes M K. rewrite heap_affine_def in M.

subst. applys hempty_intro. }

{ intros h K. specializes M K. rewrite heap_affine_def.

applys hempty_inv M. }

Qed.

Moreover, the affine top predicate \GC is equivalent to the empty heap
predicate hempty.

Lemma hgc_eq_hempty : hgc = hempty.

Proof using.

unfold hgc. applys himpl_antisym.

{ xpull. introv N. rewrite* haffine_equiv in N. }

{ xsimpl \[]. applys haffine_hempty. }

Qed.

End FullyLinearLogic.

Proof using.

unfold hgc. applys himpl_antisym.

{ xpull. introv N. rewrite* haffine_equiv in N. }

{ xsimpl \[]. applys haffine_hempty. }

Qed.

End FullyLinearLogic.

We now explain how to refine the notion of Separation Logic triple so as to
accomodate the discard rule. Recall the previous definition of triples,
capturing a linear logic.

Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ s, H s → eval s t Q. The new discard rule triple_htop_post asserts that postconditions may be freely extended with the \GC predicate. To support this rule, it suffices to modify the definition of triple to include the predicate \GC in the postcondition of the underlying Hoare triple, as follows.

Definition triple (t:trm) (H:hprop) (Q:val→hprop) : Prop :=

∀ s, H s → eval s t Q. The new discard rule triple_htop_post asserts that postconditions may be freely extended with the \GC predicate. To support this rule, it suffices to modify the definition of triple to include the predicate \GC in the postcondition of the underlying Hoare triple, as follows.

Next, for the updated definition of triple using \GC, we establish:

- that all the existing reasoning rules of Separation Logic remain sound, and
- that the new discard rules triple_htop_post, triple_haffine_hpost, and triple_haffine_hpre are provable.

### Soundness of the Existing Rules

Lemma triple_conseq : ∀ t H' Q' H Q,

triple t H' Q' →

H ==> H' →

Q' ===> Q →

triple t H Q.

Proof using.

unfolds triple. introv M MH MQ HF. applys* eval_conseq. xsimpl*.

Qed.

Lemma triple_frame : ∀ t H Q H',

triple t H Q →

triple t (H \* H') (Q \*+ H').

Proof using.

introv M HF. lets (h

subst. specializes M M

{ applys eval_frame M MD. } { xsimpl. intros h' →. applys M

Qed.

Lemma triple_hpure : ∀ t (P:Prop) H Q,

(P → triple t H Q) →

triple t (\[P] \* H) Q.

Proof using.

introv M. intros h (h

lets E: hempty_inv HP. subst. rewrite Fmap.union_empty_l. applys¬M.

Qed.

Lemma triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,

(∀ (x:A), triple t (J x) Q) →

triple t (hexists J) Q.

Proof using. introv M (x&K). applys M K. Qed.

triple t H' Q' →

H ==> H' →

Q' ===> Q →

triple t H Q.

Proof using.

unfolds triple. introv M MH MQ HF. applys* eval_conseq. xsimpl*.

Qed.

Lemma triple_frame : ∀ t H Q H',

triple t H Q →

triple t (H \* H') (Q \*+ H').

Proof using.

introv M HF. lets (h

_{1}&h_{2}&M_{1}&M_{2}&MD&MU): hstar_inv (rm HF).subst. specializes M M

_{1}. applys eval_conseq.{ applys eval_frame M MD. } { xsimpl. intros h' →. applys M

_{2}. }Qed.

Lemma triple_hpure : ∀ t (P:Prop) H Q,

(P → triple t H Q) →

triple t (\[P] \* H) Q.

Proof using.

introv M. intros h (h

_{1}&h_{2}&M_{1}&M_{2}&D&U). destruct M_{1}as (M_{1}&HP).lets E: hempty_inv HP. subst. rewrite Fmap.union_empty_l. applys¬M.

Qed.

Lemma triple_hexists : ∀ t (A:Type) (J:A→hprop) Q,

(∀ (x:A), triple t (J x) Q) →

triple t (hexists J) Q.

Proof using. introv M (x&K). applys M K. Qed.

We also need to update the reasoning rules for terms. We present one
representative example: the proof rule for sequences.

Lemma triple_seq : ∀ t

triple t

triple t

triple (trm_seq t

Proof using.

_{1}t_{2}H Q H_{1},triple t

_{1}H (fun v ⇒ H_{1}) →triple t

_{2}H_{1}Q →triple (trm_seq t

_{1}t_{2}) H Q.Proof using.

The proof is structured like in lemma triple_seq from chapter
Rules.

unfold triple. introv M

{ applys M

{ simpl. intros v

applys eval_conseq. { applys eval_frame D. applys* M

_{1}M_{2}. intros s Hs. applys eval_seq.{ applys M

_{1}Hs. }{ simpl. intros v

_{1}s_{2}Hs_{2}. lets (h_{1}&h_{2}&N_{1}&N_{2}&D&->): hstar_inv (rm Hs_{2}).applys eval_conseq. { applys eval_frame D. applys* M

_{2}. }
The main difference is the need to to invoke the lemma hstar_hgc_hgc for
merging the left-over that originates from t

_{1}with the \GC that originates from t_{2}into a single \GC.
asserts R: ((= h

xchange hstar_hgc_hgc. xsimpl. }

Qed.

_{2}) ==> \GC). { intros ? →. auto. } xchange (rm R).xchange hstar_hgc_hgc. xsimpl. }

Qed.

### Soundness of the Discard Rules

#### Exercise: 3 stars, standard, especially useful (triple_hgc_post)

Prove triple_hgc_post with respect to the refined definition of triple that includes \GC in the postcondition. Hint: exploit hstar_hgc_hgc, with help from the tactics xchange and xsimpl.
Lemma triple_hgc_post : ∀ t H Q,

triple t H (Q \*+ \GC) →

triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

triple t H (Q \*+ \GC) →

triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

#### Exercise: 1 star, standard, especially useful (triple_haffine_post)

Prove that triple_haffine_post is derivable from triple_hgc_post. Hint: use the property himpl_hgc_r, which asserts H' ==> \GC.
Lemma triple_haffine_post : ∀ t H H' Q,

haffine H' →

triple t H (Q \*+ H') →

triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

haffine H' →

triple t H (Q \*+ H') →

triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

#### Exercise: 1 star, standard, optional (triple_hgc_post_from_triple_haffine_post)

Conversely, prove that triple_hgc_post is derivable from triple_haffine_post.
Lemma triple_hgc_post_from_triple_haffine_post : ∀ t H Q,

triple t H (Q \*+ \GC) →

triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

triple t H (Q \*+ \GC) →

triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

#### Exercise: 1 star, standard, optional (triple_haffine_pre)

Prove that triple_haffine_pre is derivable from triple_hgc_post. Hint: exploit the frame rule, and leverage triple_hgc_post either directly or by invoking its corollary triple_haffine_post.
Lemma triple_haffine_pre : ∀ t H H' Q,

haffine H' →

triple t H Q →

triple t (H \* H') Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

haffine H' →

triple t H Q →

triple t (H \* H') Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

### Combined Structural Rules

#### Exercise: 2 stars, standard, optional (triple_conseq_frame_hgc)

Prove the combined structural rule triple_conseq_frame_hgc, which extends triple_conseq_frame with the discard rule, replacing Q_{1}\*+ H

_{2}===> Q with Q

_{1}\*+ H

_{2}===> Q \*+ \GC.

Lemma triple_conseq_frame_hgc : ∀ H

triple t H

H ==> H

Q

triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

_{2}H_{1}Q_{1}t H Q,triple t H

_{1}Q_{1}→H ==> H

_{1}\* H_{2}→Q

_{1}\*+ H_{2}===> Q \*+ \GC →triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

#### Exercise: 1 star, standard, optional (triple_ramified_frame_hgc)

Prove the following generalization of the ramified frame rule that includes the discard rule. Hint: take inspiration from the proof of triple_ramified_frame presented in the chapter Wand.
Lemma triple_ramified_frame_hgc : ∀ H

triple t H

H ==> H

triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

_{1}Q_{1}t H Q,triple t H

_{1}Q_{1}→H ==> H

_{1}\* (Q_{1}\−−∗ (Q \*+ \GC)) →triple t H Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

### Definition of WP for a Partially Affine Separation Logic

The characteristic equivalence of wp remains valid, with respect to the
definition of wp extended with \GC and the definition of triple
extended with \GC.

Lemma wp_equiv : ∀ t H Q,

(H ==> wp t Q) ↔ (triple t H Q).

Proof using. iff M; introv Hs; applys M Hs. Qed.

(H ==> wp t Q) ↔ (triple t H Q).

Proof using. iff M; introv Hs; applys M Hs. Qed.

The structural reasoning rules also remain valid.

Lemma wp_conseq : ∀ t Q

Q

wp t Q

Proof using.

unfold wp. introv M. intros s Hs. applys* eval_conseq. xsimpl*.

Qed.

Lemma wp_frame : ∀ t H Q,

(wp t Q) \* H ==> wp t (Q \*+ H).

Proof using.

intros. unfold wp. intros h HF.

lets (h

subst. applys eval_conseq.

{ applys eval_frame M

{ xsimpl. intros h' →. applys M

Qed.

_{1}Q_{2},Q

_{1}===> Q_{2}→wp t Q

_{1}==> wp t Q_{2}.Proof using.

unfold wp. introv M. intros s Hs. applys* eval_conseq. xsimpl*.

Qed.

Lemma wp_frame : ∀ t H Q,

(wp t Q) \* H ==> wp t (Q \*+ H).

Proof using.

intros. unfold wp. intros h HF.

lets (h

_{1}&h_{2}&M_{1}&M_{2}&MD&MU): hstar_inv (rm HF).subst. applys eval_conseq.

{ applys eval_frame M

_{1}MD. }{ xsimpl. intros h' →. applys M

_{2}. }Qed.

In weakest precondition style, the discard rule triple_hgc_post translates
into the entailment wp t (Q \*+ \GC) ==> wp t Q.

#### Exercise: 1 star, standard, optional (wp_hgc_post)

#### Exercise: 3 stars, standard, optional (wp_haffine_pre)

Prove wp_haffine_pre. Hint: one possibility is to use eval_conseq and wp_frame, as well as himpl_hgc_r and hstar_hgc_hgc. Another possibility is to refine the proof of wp_frame.
Lemma wp_haffine_pre : ∀ t H Q,

haffine H →

(wp t Q) \* H ==> wp t Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

haffine H →

(wp t Q) \* H ==> wp t Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

#### Exercise: 3 stars, standard, optional (wp_haffine_pre)

Prove wp_ramified with support for \GC.
Lemma wp_ramified : ∀ Q

(wp t Q

Proof using. (* FILL IN HERE *) Admitted.

☐

_{1}Q_{2}t,(wp t Q

_{1}) \* (Q_{1}\−−∗ (Q_{2}\*+ \GC)) ==> (wp t Q_{2}).Proof using. (* FILL IN HERE *) Admitted.

☐

### Exploiting the Discard Rule in Proofs

- by invoking triple_haffine_pre to remove a specific predicate from the current state, i.e., the precondition; or
- by invoking triple_htop_post to add a \GC into the current postcondition and allow subsequent removal of any predicate that may be left-over in the final entailment justifying that the final state satisfies the postcondition.

Parameter xwp_lemma : ∀ v

v

H ==> wpgen ((x,v

triple (trm_app v

_{1}v_{2}x t_{1}H Q,v

_{1}= val_fun x t_{1}→H ==> wpgen ((x,v

_{2})::nil) t_{1}Q →triple (trm_app v

_{1}v_{2}) H Q.
Its generalized form extends the postcondition from Q to Q \*+ \GC, as
shown below.

Lemma xwp_lemma' : ∀ v

v

H ==> wpgen ((x,v

triple (trm_app v

Proof using. introv E M. applys triple_hgc_post. applys* xwp_lemma. Qed.

_{1}v_{2}x t_{1}H Q,v

_{1}= val_fun x t_{1}→H ==> wpgen ((x,v

_{2})::nil) t_{1}(Q \*+ \GC) →triple (trm_app v

_{1}v_{2}) H Q.Proof using. introv E M. applys triple_hgc_post. applys* xwp_lemma. Qed.

We update the tactic xwp to exploit the lemma xwp_lemma' instead of
xwp_lemma.

Tactic Notation "xwp" :=

intros; applys xwp_lemma';

[ reflexivity | simpl; unfold wpgen_var; simpl ].

intros; applys xwp_lemma';

[ reflexivity | simpl; unfold wpgen_var; simpl ].

### Example Proof in an Affine Separation Logic

Assume a fully affine logic.

Observe, in the proof below, the \GC introduced in the postcondition by
the call to xwp.

Lemma triple_succ_using_incr : ∀ (n:int),

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

xwp. xapp. intros r. xapp. xapp. xsimpl. { auto. }

(* It remains to absorb the left-over reference into the \GC predicate *)

applys himpl_hgc_r. applys haffine_hany.

Qed.

triple (succ_using_incr n)

\[]

(fun r ⇒ \[r = n+1]).

Proof using.

xwp. xapp. intros r. xapp. xapp. xsimpl. { auto. }

(* It remains to absorb the left-over reference into the \GC predicate *)

applys himpl_hgc_r. applys haffine_hany.

Qed.

We will show further on how to automate the work from the last line of the
proof above, by setting up xsimpl to automatically resolve goals of the
form H ==> \GC.

## Revised Definition of mkstruct

Definition mkstruct (F:formula) : formula :=

fun Q ⇒ \∃ Q', (F Q') \* (Q' \−−∗ Q). This definition can be generalized to handle not just the consequence and frame rules, but also the discard rule. To that end, mkstruct is extended with an additional \GC, as follows.

Let us prove that this revised definition of mkstruct does indeed satisfy
the wp-style statement of the discard rule, which is stated in a way
similar to wp_hgc_post.

Lemma mkstruct_hgc : ∀ Q F,

mkstruct F (Q \*+ \GC) ==> mkstruct F Q.

Proof using.

intros. unfold mkstruct. set (X := hgc) at 3. replace X with (\GC \* \GC).

{ xsimpl. } { subst X. apply hstar_hgc_hgc. }

Qed.

mkstruct F (Q \*+ \GC) ==> mkstruct F Q.

Proof using.

intros. unfold mkstruct. set (X := hgc) at 3. replace X with (\GC \* \GC).

{ xsimpl. } { subst X. apply hstar_hgc_hgc. }

Qed.

Further, let us prove that the revised definition of mkstruct still
satisfies the four originally required properties: erasure, consequence,
frame, and monoticity.

Lemma mkstruct_erase : ∀ F Q,

F Q ==> mkstruct F Q.

Proof using.

intros. unfold mkstruct. xsimpl Q. apply himpl_hgc_r. apply haffine_hempty.

Qed.

Lemma mkstruct_conseq : ∀ F Q

Q

mkstruct F Q

Proof using.

introv WQ. unfold mkstruct. xpull. intros Q'. xsimpl Q'. xchange WQ.

Qed.

Lemma mkstruct_frame : ∀ F H Q,

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Proof using.

intros. unfold mkstruct. xpull. intros Q'. xsimpl Q'.

Qed.

Lemma mkstruct_monotone : ∀ F

(∀ Q, F

mkstruct F

Proof using.

introv WF. unfolds mkstruct. xpull. intros Q'. xchange WF. xsimpl Q'.

Qed.

F Q ==> mkstruct F Q.

Proof using.

intros. unfold mkstruct. xsimpl Q. apply himpl_hgc_r. apply haffine_hempty.

Qed.

Lemma mkstruct_conseq : ∀ F Q

_{1}Q_{2},Q

_{1}===> Q_{2}→mkstruct F Q

_{1}==> mkstruct F Q_{2}.Proof using.

introv WQ. unfold mkstruct. xpull. intros Q'. xsimpl Q'. xchange WQ.

Qed.

Lemma mkstruct_frame : ∀ F H Q,

(mkstruct F Q) \* H ==> mkstruct F (Q \*+ H).

Proof using.

intros. unfold mkstruct. xpull. intros Q'. xsimpl Q'.

Qed.

Lemma mkstruct_monotone : ∀ F

_{1}F_{2}Q,(∀ Q, F

_{1}Q ==> F_{2}Q) →mkstruct F

_{1}Q ==> mkstruct F_{2}Q.Proof using.

introv WF. unfolds mkstruct. xpull. intros Q'. xchange WF. xsimpl Q'.

Qed.

#### Exercise: 2 stars, standard, optional (mkstruct_haffine_post)

Prove the reformulation of triple_haffine_post adapted to mkstruct, for discarding an affine piece of postcondition.
Lemma mkstruct_haffine_post : ∀ H Q F,

haffine H →

mkstruct F (Q \*+ H) ==> mkstruct F Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

haffine H →

mkstruct F (Q \*+ H) ==> mkstruct F Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

#### Exercise: 2 stars, standard, optional (mkstruct_haffine_pre)

Prove the reformulation of triple_haffine_pre adapted to mkstruct, for discarding an affine piece of postcondition.
Lemma mkstruct_haffine_pre : ∀ H Q F,

haffine H →

(mkstruct F Q) \* H ==> mkstruct F Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

haffine H →

(mkstruct F Q) \* H ==> mkstruct F Q.

Proof using. (* FILL IN HERE *) Admitted.

☐

The tactic xaffine applies to a goal of the form haffine H. It
simplifies the goal using all the distributivity rules associated with
haffine. Ultimately, it invokes eauto with haffine, which can leverage
knowledge specific to the definition of haffine from the Separation Logic
setup at hand.

Create HintDb haffine.

Tactic Notation "xaffine" :=

repeat match goal with ⊢ haffine ?H ⇒

match H with

| (hempty) ⇒ apply haffine_hempty

| (hpure _) ⇒ apply haffine_hpure

| (hstar _ _) ⇒ apply haffine_hstar

| (hexists _) ⇒ apply haffine_hexists

| (hforall _) ⇒ apply haffine_hforall

| (hgc) ⇒ apply haffine_hgc

| _ ⇒ eauto with haffine

end

end.

Lemma xaffine_demo : ∀ H

haffine H

haffine H

haffine (H

Proof using. introv K

End Xaffine.

Module XsimplExtended.

Import LibSepReference.

Tactic Notation "xaffine" :=

repeat match goal with ⊢ haffine ?H ⇒

match H with

| (hempty) ⇒ apply haffine_hempty

| (hpure _) ⇒ apply haffine_hpure

| (hstar _ _) ⇒ apply haffine_hstar

| (hexists _) ⇒ apply haffine_hexists

| (hforall _) ⇒ apply haffine_hforall

| (hgc) ⇒ apply haffine_hgc

| _ ⇒ eauto with haffine

end

end.

Lemma xaffine_demo : ∀ H

_{1}H_{2}H_{3},haffine H

_{1}→haffine H

_{3}→haffine (H

_{1}\* H_{2}\* H_{3}).Proof using. introv K

_{1}KJ. xaffine. (* remains haffine H_{2}*) Abort.End Xaffine.

Module XsimplExtended.

Import LibSepReference.

The tactic xsimpl is extended with support for simplifying goals of the
form H ==> \GC into haffine H, using lemma himpl_hgc_r. For example,
xsimpl can simplify the goal H

_{1}\* H_{2}==> H_{2}\* \GC into just haffine H_{1}.
Lemma xsimpl_xgc_demo : ∀ H

H

Proof using. intros. xsimpl. (* remains haffine H

_{1}H_{2},H

_{1}\* H_{2}==> H_{2}\* \GC.Proof using. intros. xsimpl. (* remains haffine H

_{1}*) Abort.
In addition, xsimpl invokes the tactic xaffine to simplify
side-conditions of the form haffine H. For example, xsimpl can prove the
following lemma.

Lemma xsimpl_xaffine_demo : ∀ H

haffine H

H

Proof using. introv K

End XsimplExtended.

_{1}H_{2},haffine H

_{1}→H

_{1}\* H_{2}==> H_{2}\* \GC.Proof using. introv K

_{1}. xsimpl. Qed.End XsimplExtended.

This section presents the discard tactics xgc, xc_keep, and xgc_post.
Their implementation leverages the discard property of mkstruct,
reproduced below.

The tactic xgc H

_{1}removes H_{1}from the precondition (i.e., from the current state), in the course of a proof exploiting a formula produced by wpgen. More precisely, the tactic xgc H_{1}removes H_{1}from the current precondition H. It leverages xsimpl to simplify the entailment H ==> H_{1}\* H_{2}and infer H_{2}, which describes what remains after removing H_{1}from H.
Lemma xgc_lemma: ∀ H

H ==> H

haffine H

H

H ==> mkstruct F Q.

Proof using.

introv WH K M. xchange WH. xchange M.

applys himpl_trans mkstruct_frame.

applys himpl_trans mkstruct_hgc.

applys mkstruct_conseq. xsimpl.

Qed.

Tactic Notation "xgc" constr(H) :=

eapply (@xgc_lemma H); [ xsimpl | xaffine | ].

Lemma xgc_demo : ∀ H

haffine H

(H

Proof using. introv K

_{1}H_{2}H F Q,H ==> H

_{1}\* H_{2}→haffine H

_{1}→H

_{2}==> mkstruct F Q →H ==> mkstruct F Q.

Proof using.

introv WH K M. xchange WH. xchange M.

applys himpl_trans mkstruct_frame.

applys himpl_trans mkstruct_hgc.

applys mkstruct_conseq. xsimpl.

Qed.

Tactic Notation "xgc" constr(H) :=

eapply (@xgc_lemma H); [ xsimpl | xaffine | ].

Lemma xgc_demo : ∀ H

_{1}H_{2}H_{3}F Q,haffine H

_{2}→(H

_{1}\* H_{2}\* H_{3}) ==> mkstruct F Q.Proof using. introv K

_{2}. xgc H_{2}. (* clears H_{2}*) Abort.
The tactic xgc_keep H is a variant of xgc that enables discarding
everything but H from the precondition.
The implementation of the tactic leverages the same lemma xgc_lemma, but
providing H

_{2}instead of H_{1}.
Tactic Notation "xgc_keep" constr(H) :=

eapply (@xgc_lemma _ H); [ xsimpl | xaffine | ].

Lemma xgc_keep_demo : ∀ H

haffine H

haffine H

(H

Proof using. introv K

eapply (@xgc_lemma _ H); [ xsimpl | xaffine | ].

Lemma xgc_keep_demo : ∀ H

_{1}H_{2}H_{3}F Q,haffine H

_{1}→haffine H

_{3}→(H

_{1}\* H_{2}\* H_{3}) ==> mkstruct F Q.Proof using. introv K

_{1}K_{3}. xgc_keep H_{2}. Abort.
The tactic xgc_post simply extends the postcondition with a \GC, to
enable subsequent discarding of heap predicates in the final entailment.

Lemma xgc_post_lemma : ∀ H Q F,

H ==> mkstruct F (Q \*+ \GC) →

H ==> mkstruct F Q.

Proof using. introv M. xchange M. applys mkstruct_hgc. Qed.

Tactic Notation "xgc_post" :=

apply xgc_post_lemma.

H ==> mkstruct F (Q \*+ \GC) →

H ==> mkstruct F Q.

Proof using. introv M. xchange M. applys mkstruct_hgc. Qed.

Tactic Notation "xgc_post" :=

apply xgc_post_lemma.

The example below illustrates a usage of the xgc_post tactic.

Lemma xgc_keep_demo : ∀ H

haffine H

haffine H

H

H

Proof using.

introv K

xgc_post. (* add \GC to the postcondition Q *)

xchange M. applys mkstruct_conseq.

xsimpl.

Qed.

End XGC.

_{1}H_{2}H_{3}F Q,haffine H

_{1}→haffine H

_{3}→H

_{1}==> mkstruct F (Q \*+ H_{2}\*+ H_{3}) →H

_{1}==> mkstruct F Q.Proof using.

introv K

_{1}K_{3}M.xgc_post. (* add \GC to the postcondition Q *)

xchange M. applys mkstruct_conseq.

xsimpl.

Qed.

End XGC.

Recall the lemmas haffine_hexists and haffine_hforall.

Lemma haffine_hexists : ∀ A (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∃ x, (J x)).

Lemma haffine_hforall : ∀ A `{Inhab A} (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∀ x, (J x)). They can be reformulated in a more concise way, as explained next.
First, to smoothly handle the distribution on the quantifiers, let us extend
the notion of "affinity" to postconditions. The predicate haffine_post J
asserts that haffine holds of J x for any x.

Lemma haffine_hexists : ∀ A (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∃ x, (J x)).

Lemma haffine_hforall : ∀ A `{Inhab A} (J:A→hprop),

(∀ x, haffine (J x)) →

haffine (\∀ x, (J x)). They can be reformulated in a more concise way, as explained next.

The rules then reformulate as follows.

Lemma haffine_hexists : ∀ A (J:A→hprop),

haffine_post J →

haffine (hexists J).

Proof using. introv F

Lemma haffine_hforall : ∀ A `{Inhab A} (J:A→hprop),

haffine_post J →

haffine (hforall J).

Proof using.

introv IA F

Qed.

End HaffineQuantifiers.

haffine_post J →

haffine (hexists J).

Proof using. introv F

_{1}(x&Hx). applys* F_{1}. Qed.Lemma haffine_hforall : ∀ A `{Inhab A} (J:A→hprop),

haffine_post J →

haffine (hforall J).

Proof using.

introv IA F

_{1}Hx. lets N: hforall_inv Hx. applys* F_{1}(arbitrary (A:=A)).Qed.

End HaffineQuantifiers.

Earlier on, we proved that triple_hgc_pre is derivable from
triple_hgc_post, through a simple application of the frame rule. We wrote
that, reciprocally, the rule triple_hgc_post is derivable from
triple_hgc_pre, yet with a slightly more involved proof. Let us present
this proof. Concretely, assume triple_hgc_pre and let us prove the result
triple_hgc_post.

Parameter triple_hgc_pre : ∀ t H Q,

triple t H Q →

triple t (H \* \GC) Q.

Parameter triple_hgc_post : ∀ t H Q,

triple t H (Q \*+ \GC) →

triple t H Q.

triple t H Q →

triple t (H \* \GC) Q.

Parameter triple_hgc_post : ∀ t H Q,

triple t H (Q \*+ \GC) →

triple t H Q.

The key idea of the proof is that a term t admits the same behavior as
let x = t in x. Recall from chapter Rules the lemma
eta_same_triples which asserts the equivalence of t and
let x = t in x.

To discard a predicate from the postcondition of t if we only have at hand
a rule for discarding predicates from preconditions, we replace t with
let x = t in x and apply the discard rule after evaluating t but before
returning the variable x.

Lemma triple_hgc_post_from_hgc_pre : ∀ t H Q,

triple t H (Q \*+ \GC) →

triple t H Q.

Proof using.

introv M. rewrite (eta_same_triples t "x"). applys triple_let.

{ applys M. }

{ intros v. simpl. applys triple_hgc_pre. applys triple_val. auto. }

Qed.

End FromPreToPostGC.

triple t H (Q \*+ \GC) →

triple t H Q.

Proof using.

introv M. rewrite (eta_same_triples t "x"). applys triple_let.

{ applys M. }

{ intros v. simpl. applys triple_hgc_pre. applys triple_val. auto. }

Qed.

End FromPreToPostGC.

## Historical Notes

(* 2024-08-25 14:53 *)