Separation Logic Proofs in Coq

This page is an experiment to assist me in my separation logic class teaching how to use separation logic to prove programs. I use Arthur Charguéraud's material and Emilio Jesús Gallego Arias's JsCoq for running it in your browser.

 

Usage

Alt-Enter (Cmd should work in Macs too) goes to the current point; Alt-N/P or Alt-Down/Up will move through the proof; F8 or the power icon toggles the goal panel.

In case of stack overflow, try using Chrome and increasing the stack limit:

google-chrome --js-flags="--harmony-tailcalls" --js-flags="--stack-size=65536"

A command with orange background is being processed, so you might want to wait for it.

A command with kinda gray background is done processing, without error.

A command with red background raised an error -- see it in the bottom-right corner.

 

Loading the library

Your browser should first load the files from my server, which may take approximately 10 or 20 seconds, and then the following loading command should take about 20 seconds depending on your browser and computer.

 

(** From Arthur Charguéraud's Separation Logic Foundations -- see licencing in the material mentioned above *) Set Implicit Arguments. From SLF Require Import Example. (** Examples from lecture 1 *) (* no GC for now when using xwp *) Ltac xwp_xtriple_handle_gc ::= xwp_xtriple_remove_gc. Locate "\[]". Print hempty. Locate "\[ _ ]". Print hpure. Locate "\*". Print hstar. Locate "~~~>". Print hsingle. Locate "\exists". Print hexists. Lemma Triple_ref: TRIPLE (val_ref 3) PRE (\[]) POST (fun (r : loc) => (r ~~> 3)). Proof. xtriple. xapp. xsimpl. Qed. Definition hd : field := 0%nat. Definition tl : field := 1%nat. Definition Mcell (x : val) (p' : loc) (p : loc) : hprop := p`.hd ~~> x \* p`.tl ~~> p'. Fixpoint Mlist (l : list val) (p : loc) : hprop := match l with nil => \[p = null] | x :: l => \exists p', Mcell x p' p \* Mlist l p' end. Definition mcell : val := VFun 'x 'q := New`{ hd := 'x ; tl := 'q }. Lemma Triple_mcell : forall (x:int) (q:loc), TRIPLE (mcell x q) PRE \[] POST (fun (p:loc) => (p`.hd ~~> x) \* (p`.tl ~~> q)). Proof using. xwp. xapp. intro. do 2 rewrite Record_cons. rewrite Record_nil. xsimpl. Qed. Hint Extern 1 (Register_Spec mcell) => Provide Triple_mcell. Definition build : val := VFix 'b 'n 'v := If_ 'n '= 0 Then null Else Let 'q := 'b ('n '- 1) 'v in mcell 'v 'q. Lemma build_triple (n : int) (x : val) : TRIPLE (build n x) PRE \[n >= 0] POST (fun (p : loc) => \exists L : list val, Mlist L p \* \[ n = length L /\ forall i : nat, 0 <= i < to_nat n -> nth i L = x ]). Proof. induction_wf IHn: (wf_downto 0) n. xwp. xapp. intros. xif. - intros ->. xval. apply himpl_hexists_r with nil. simpl. xsimpl*. - intros Hne. xapp. xapp. math. math. intros. unfold "``". rewrite enc_loc_eq. Fail xapp. Abort. (* Verification of mrev: recursive version SLFList.v *) (* Verification of mlength: in SLFList.v *) Definition front : field := 0%nat. Definition back : field := 1%nat. Fixpoint MListSeg q (L:list int) (p :loc) : hprop := (* defines [p ~> MList L] *) match L with | nil => \[p = q] | x::L' => \exists q, (p`.hd ~~> x) \* (p`.tl ~~> q) \* (q ~> MListSeg q L') end. Definition MQueue (L : list int) (p : loc) : hprop := \exists f b, p`.front ~~> f \* p`.back ~~> b \* (MListSeg b L f) \* (\exists y q, b`.hd ~~> y \* b`.tl ~~> q). Definition item : field := 0%nat. Definition left : field := 1%nat. Definition right : field := 2%nat. Definition Mnode (x : val) (l r : loc) (p : loc) : hprop := p`.item ~~> x \* p`.left ~~> l \* p`.right ~~> r. Inductive tree : Type := | Leaf : tree | Node : int -> tree -> tree -> tree. Fixpoint Mtree (T : tree) (p : loc) : hprop := match T with Leaf => \[p = null] | Node x T1 T2 => \exists p1 p2, Mnode x p1 p2 p \* Mtree T1 p1 \* Mtree T2 p2 end. (* Examples left: depth, MtreeComplete, search, MSearchTree, UnionFind *) (* How triples are defined: *) Print triple. Print hoare. (** Examples from lecture 2 *) Lemma slide3_1 (r : loc) : TRIPLE (incr r) PRE (r ~~> 2) POST (fun (_ : unit) => (r ~~> 3)). Proof. xwp. xapp. xapp. xapp. xsimpl. Qed. Lemma slide3_2 (r s : loc) : TRIPLE (incr r) PRE (r ~~> 2 \* s ~~> 7) POST (fun (_ : unit) => (r ~~> 3 \* s ~~> 7)). Proof. xwp. xapp. xapp. xapp. xsimpl. Qed. Lemma slide3_3 (r : loc) (H : hprop) : TRIPLE (incr r) PRE (r ~~> 2 \* H) POST (fun (_ : unit) => (r ~~> 3 \* H)). Proof. xwp. xapp. xapp. xapp. xsimpl. Qed. Lemma frame_rule H1 t Q H2 : TRIPLE t PRE H1 POST Q -> TRIPLE t PRE (H1 \* H2) POST (Q \*+ H2). Proof. (* All of this is unfolding... *) unfold Triple, triple, hoare, LiftPost. intros HYP H' h Hh. destruct (HYP (H' \* H2) h) as (h' & v & Heval & h2 & hpoubelle & DIFF & Hpoubelle). revert h Hh. shelve. intuition. exists h', v. split; auto. exists h2, hpoubelle. intuition. revert DIFF. clear H3 H4. revert h2. shelve. (* Important part! *) Unshelve. match goal with |- forall h, ?A h -> ?B h => change (A ==> B) end. xsimpl*. match goal with |- forall h, ?A h -> ?B h => change (A ==> B) end. xsimpl*. Qed. (* Examples mlength, list_incr: in SLFList.v *) (* (where the frame process is automatically applied) *) (* Examples left: tree copy, small footprint, repr for arrays, quicksort *) (* Cells can be defined in terms of lists of (offset, val) *) (* Could be defined in terms of Fmaps but no constructive existential interface *) Fixpoint Cells (M : list (nat * val)) (p : loc) := match M with | nil => \[] | (i, v) :: M => (p + i)%nat ~~> v \* Cells M p end. Check hstar. Check hstar_assoc. Check hstar_comm. Check hstar_hempty_r. Check hstar_hexists. Check hstar_hpure. Check fun_ext_nondep_1. Check prop_ext. Locate "==>". Print himpl. Lemma slide_32 r : r ~~> 6 ==> \exists n, r ~~> n \* \[Z.even n]. Proof. xsimpl. compute. Set Printing All. reflexivity. Unset Printing All. Qed. Section heap_entailment. Variable r s : loc. Goal r ~~> 3 \* s ~~> 4 ==> s ~~> 4 \* r ~~> 3. xsimpl. Qed. Goal r ~~> 3 ==> s ~~> 4 \* r ~~> 3. xsimpl. Fail Qed. Abort. Goal s ~~> 4 \* r ~~> 3 ==> r ~~> 4. xsimpl. Fail Qed. Abort. Goal s ~~> 4 \* r ~~> 3 ==> r ~~> 3. xsimpl. Fail Qed. Abort. Goal \[False] \* r ~~> 3 ==> s ~~> 4 \* r ~~> 4. xsimpl. Qed. Goal r ~~> 4 \* s ~~> 3 ==> \[False]. xsimpl. Fail Qed. Abort. Goal r ~~> 4 \* r ~~> 3 ==> \[False]. apply himpl_trans with \[ r <> r ]. Abort (* TODO *). Goal r ~~> 3 \* r ~~> 3 ==> \[False]. apply himpl_trans with \[ r <> r ]. Abort (* TODO *). Goal r ~~> 3 ==> \exists n : int, r ~~> n. apply himpl_hexists_r with (x := 3). xsimpl. Qed. Goal (\exists n : int, r ~~> n) ==> r ~~> 3. Abort. Goal (\exists n : int, r ~~> n \* \[n > 0]) ==> (\exists n : int, \[n > 1] \* r ~~> (n - 1)). xpull. intros n Hn. apply himpl_hexists_r with (x := n + 1). xsimpl. math. math. Qed. Goal r ~~> 3 \* s ~~> 3 ==> (\exists n : int, r ~~> n \* s ~~> n). xsimpl. Qed. Goal forall n, (\exists n : int, r ~~> n \* \[n > 0] \* \[n < 0]) ==> r ~~> n \* s ~~> n. intros nn. xsimpl. math. math. Qed. (* Left: GC-POST+FRAME => GC-PRE, other structural rules, tree copy *)