Commit 1cd8e4ea authored by charguer's avatar charguer

jfla_file

parent d3e563ca
......@@ -19,21 +19,6 @@ Implicit Types n : int.
(* ********************************************************************** *)
(* * Basic functions *)
(* ---------------------------------------------------------------------- *)
(* ** Decrement *)
(** [val_decr] defined in [ExampleBasicNonLifted.v] *)
Lemma Rule_decr : forall (p:loc) (n:int),
Triple (val_decr `p)
PRE (p ~~> n)
POST (fun (r:unit) => p ~~> (n-1)).
Proof using.
xcf. xapps. xapps. xapps. hsimpl~.
Qed.
Hint Extern 1 (Register_Spec val_decr) => Provide Rule_decr.
(* ---------------------------------------------------------------------- *)
(** Swap function *)
......
......@@ -180,27 +180,6 @@ Lemma rule_incr_with_frame : forall p n H,
Proof using. intros. xapps. hsimpl~. Qed.
(* ---------------------------------------------------------------------- *)
(** Decrement function -- details *)
Definition val_decr :=
ValFun 'p :=
Let 'n := val_get 'p in
Let 'm := 'n '- 1 in
val_set 'p 'm.
Lemma rule_decr : forall p n,
triple (val_decr p)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n-1))).
Proof using.
xcf. xapps. xapps. xapps. hsimpl~.
Qed.
Hint Extern 1 (Register_spec val_decr) => Provide rule_decr.
(* ---------------------------------------------------------------------- *)
(** Swap function *)
......@@ -249,6 +228,33 @@ Proof using.
Qed.
(* ---------------------------------------------------------------------- *)
(** Two calls to incr *)
(*
let val_incr_twice r =
incr r;
incr r
*)
Definition val_incr_twice :=
ValFun 'p :=
val_incr 'p ;;
val_incr 'p.
Lemma rule_incr_twice : forall p n,
triple (val_incr_twice p)
(p ~~~> n)
(fun r => \[r = val_unit] \* p ~~~> (n+2)).
Proof using.
xcf. xapp. auto.
xapps. (* same as [xapp; hpull] *)
intros; subst.
math_rewrite ((n + 1) + 1 = (n + 2)). (* TODO: avoid this ?*)
hsimpl. auto.
Qed.
(* ---------------------------------------------------------------------- *)
(** Basic let-binding example *)
......@@ -268,11 +274,42 @@ Proof using.
Qed.
(* ---------------------------------------------------------------------- *)
(** Basic one references *)
(*
let val_example_one_ref n =
let i = ref 0 in
incr i;
!i
*)
Definition val_example_one_ref :=
ValFun 'n :=
Let 'k := 'n '+ 1 in
Let 'i := 'ref 'k in
val_incr 'i ;;
'!'i.
Lemma rule_example_one_ref : forall n,
triple (val_example_one_ref n)
\[]
(fun r => \[r = n+2]).
Proof using.
xcf.
xapp. intros; subst.
xapp. intros I i ?. subst.
xapp. auto.
xapp. intros r. hsimpl. intros; subst. fequals. math.
Qed.
(* ---------------------------------------------------------------------- *)
(** Basic two references *)
(*
let val_example_ref n =
let val_example_two_ref n =
let i = ref 0 in
let r = ref n in
decr r;
......@@ -281,7 +318,7 @@ Qed.
!i + !r
*)
Definition val_example_ref :=
Definition val_example_two_ref :=
ValFun 'n :=
Let 'i := 'ref 0 in
Let 'r := 'ref 'n in
......@@ -295,8 +332,8 @@ Definition val_example_ref :=
Let 'r2 := '!'r in
'i2 '+ 'r2.
Lemma rule_val_example_ref : forall n,
triple (val_example_ref n)
Lemma rule_example_two_ref : forall n,
triple (val_example_two_ref n)
\[]
(fun r => \[r = n+1]).
Proof using.
......
......@@ -262,6 +262,8 @@ Hint Extern 1 (Register_Spec val_mlist_copy) => Provide Rule_mlist_copy.
(* ********************************************************************** *)
(* * Length of a mutable list *)
(** Note: same definition as in [ExampleListNonLifted] *)
Definition val_mlist_length : val :=
ValFix 'f 'p :=
If_ 'p '<> null Then (
......@@ -278,10 +280,9 @@ Lemma Rule_mlist_length : forall A `{EA:Enc A} (L:list A) (p:loc),
POST (fun (r:int) => \[r = length L] \* p ~> MList L).
Proof using.
intros. gen p. induction_wf: list_sub_wf L; intros. xcf.
(* fold val_mlist_length *)
xapps~. xif ;=> C.
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p' L' EL.
xapps. xapps~ IH. xchange (MList_cons p).
xapps. xapps~ (IH L'). xchange (MList_cons p).
xapps. hsimpl. isubst. auto. }
{ subst. xchanges MList_null_inv ;=> EL. xvals~. }
Qed.
......
(**
This file formalizes mutable list examples in plain Separation Logic,
using both triples and characteristic formulae.
illustrating the direct use of triples on one example, and conducting
other proofs using characteristic formulae.
Author: Arthur Charguéraud.
License: MIT.
......@@ -419,10 +420,11 @@ Lemma rule_mlist_length_1 : forall L p,
(MList L p)
(fun r => \[r = val_int (length L)] \* MList L p).
Proof using.
intros L. induction_wf: list_sub_wf L. xcf. fold val_mlist_length.
intros L. induction_wf: list_sub_wf L. xcf.
(* TODO URGENT: will be removed soon *) fold val_mlist_length.
xapps. xif ;=> C.
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p' L' EL. subst L.
xapps. xapps~ IH.
xapps. xapps~ (IH L').
xchange (MList_cons p).
xapps. hsimpl. isubst. rew_list. fequals. math. }
{ inverts C. xchanges MList_null_inv ;=> EL. subst. xvals~. }
......@@ -436,7 +438,7 @@ Qed.
(** Implementation *)
Definition val_mlist_length_loop : val :=
ValFun 'p1 :=
ValFun 'p1 :=
Let 'r := val_ref 'p1 in
Let 'n := val_ref 0 in
While (Let 'p := val_get 'r in
......@@ -564,157 +566,3 @@ End Properties.
Arguments MListSeg_then_MCell_inv_neq : clear implicits.
(* ********************************************************************** *)
(* * Mutable queue *)
(* ---------------------------------------------------------------------- *)
(** Representation *)
Definition MQueue (L:list val) (p:loc) :=
Hexists (pf:loc), Hexists (pb:loc), Hexists (vx:val), Hexists (vy:val),
MCell pf pb p \* MListSeg pb L pf \* MCell vx vy pb.
Definition val_create :=
ValFun 'v :=
Let 'r := val_alloc 2 in
val_new_cell 'r 'r.
Lemma rule_create :
triple (val_create val_unit)
\[]
(fun r => Hexists p, \[r = val_loc p] \* MQueue nil p).
Proof using.
xcf. unfold MQueue.
xapp rule_alloc_cell as r. intros p v1 v2. intro_subst.
xapp~. hpull ;=> r x E. hsimpl~.
{ rewrite MListSeg_nil_eq. hsimpl~. }
Qed.
(* ---------------------------------------------------------------------- *)
(** Is empty *)
Definition val_is_empty :=
ValFun 'p :=
Let 'x := val_get_hd 'p in
Let 'y := val_get_tl 'p in
val_eq 'x 'y.
Lemma rule_is_empty : forall p L,
triple (val_is_empty p)
(MQueue L p)
(fun r => \[r = isTrue (L = nil)] \* MQueue L p).
Proof using.
xcf. unfold MQueue. xpull ;=> pf pb vx vy.
xapps. xapps.
xchanges (MListSeg_then_MCell_inv_neq pf pb) ;=> R.
(* xchange (MListSeg_then_MCell_inv_neq pf pb). xpull ;=> R. *)
xapp. hsimpl. isubst. fequals. rew_bool_eq. rewrite R. iff; congruence.
Qed.
Hint Extern 1 (Register_spec val_is_empty) => Provide rule_is_empty.
(* ---------------------------------------------------------------------- *)
(** Push back *)
Definition val_push_back :=
ValFun 'v 'p :=
Let 'q := val_get_tl 'p in
Let 'r := val_alloc 2 in
val_set_hd 'q 'v ;;
val_set_tl 'q 'r ;;
val_set_tl 'p 'r.
Lemma rule_push_back : forall v p L,
triple (val_push_back v p)
(MQueue L p)
(fun r => \[r = val_unit] \* MQueue (L&v) p).
Proof using.
xcf. unfold MQueue. xpull ;=> pf pb vx vy.
xapps. xapp rule_alloc_cell as r. intros pb' v1 v2. intro_subst.
xapp~. xapp~. xapp~. hchanges~ MListSeg_last.
Qed.
(* ---------------------------------------------------------------------- *)
(** Push front *)
Definition val_push_front :=
ValFun 'v 'p :=
Let 'q := val_get_hd 'p in
Let 'r := val_new_cell 'v 'q in
val_set_hd 'p 'r.
Lemma rule_push_front : forall v p L,
triple (val_push_front v p)
(MQueue L p)
(fun r => \[r = val_unit] \* MQueue (v::L) p).
Proof using.
xcf. unfold MQueue. xpull ;=> pf pb vx vy.
xapps. xapp as r. intros x. intro_subst.
xapp. hsimpl~. isubst. hchanges (@MListSeg_cons x).
Qed.
(* ---------------------------------------------------------------------- *)
(** Pop front *)
Definition val_pop_front :=
ValFun 'v 'p :=
Let 'q := val_get_hd 'p in
Let 'x := val_get_hd 'q in
Let 'r := val_get_tl 'q in
val_set_hd 'p 'r;;
'x.
Lemma rule_pop_front : forall v p L,
L <> nil ->
triple (val_pop_front v p)
(MQueue L p)
(fun v => Hexists L', \[L = v::L'] \* MQueue L' p).
Proof using.
xcf. unfold MQueue. xpull ;=> pf pb vx vy.
destruct L as [|x L']; tryfalse.
rewrite MListSeg_cons_eq. xpull ;=> pf'.
xapps. xapps. xapps. xapp~. xvals~.
Qed.
(* ---------------------------------------------------------------------- *)
(** Transfer *)
Definition val_transfer :=
ValFun 'p1 'p2 :=
Let 'e2 := val_is_empty 'p2 in
If_ val_not 'e2 Then
Let 'b1 := val_get_tl 'p1 in
Let 'f2 := val_get_hd 'p2 in
Let 'x2 := val_get_hd 'f2 in
Let 'n2 := val_get_tl 'f2 in
Let 'b2 := val_get_tl 'p2 in
val_set_tl 'p1 'b2 ;;
val_set_hd 'b1 'x2 ;;
val_set_tl 'b1 'n2 ;;
val_set_tl 'p2 'f2
End.
Lemma rule_transfer : forall p1 p2 L1 L2,
triple (val_transfer p1 p2)
(MQueue L1 p1 \* MQueue L2 p2)
(fun r => \[r = val_unit] \* MQueue (L1 ++ L2) p1 \* MQueue nil p2).
Proof using.
xcf. xapps. xapps. xif ;=> C; rew_bool_eq.
{ unfold MQueue. xpull ;=> pf2 pb2 vx2 vy2 pf1 pb1 vx1 vy1.
destruct L2 as [|x L2']; tryfalse.
rewrite MListSeg_cons_eq. xpull ;=> pf2'.
xapps. xapps. xapps. xapps.
xapps~. xapps~. xapps~. xapps~. xapps~.
intros r. hchange (MListSeg_last pf1).
hchange (MListSeg_concat pf1 pf2' pb2). rew_list.
hchange (MListSeg_nil pf2). hsimpl~. }
{ subst. rew_list. xvals~. }
Qed.
(**
This file formalizes mutable queues in plain Separation Logic,
using characteristic formulae.
Author: Arthur Charguéraud.
License: MIT.
*)
Set Implicit Arguments.
From Sep Require Import LambdaCF LambdaStruct.
From Sep Require Import ExampleListNonlifted.
Generalizable Variables A B.
Ltac auto_star ::= jauto.
Implicit Types p q : loc.
Implicit Types n : int.
Implicit Types v : val.
(* ********************************************************************** *)
(* * Mutable queue *)
(* ---------------------------------------------------------------------- *)
(** Representation *)
Definition MQueue (L:list val) (p:loc) :=
Hexists (pf:loc), Hexists (pb:loc), Hexists (vx:val), Hexists (vy:val),
MCell pf pb p \* MListSeg pb L pf \* MCell vx vy pb.
Definition val_create :=
ValFun 'v :=
Let 'r := val_alloc 2 in
val_new_cell 'r 'r.
Lemma rule_create :
triple (val_create val_unit)
\[]
(fun r => Hexists p, \[r = val_loc p] \* MQueue nil p).
Proof using.
xcf. unfold MQueue.
xapp rule_alloc_cell as r. intros p v1 v2. intro_subst.
xapp~. hpull ;=> r x E. hsimpl~.
{ rewrite MListSeg_nil_eq. hsimpl~. }
Qed.
(* ---------------------------------------------------------------------- *)
(** Is empty *)
Definition val_is_empty :=
ValFun 'p :=
Let 'x := val_get_hd 'p in
Let 'y := val_get_tl 'p in
val_eq 'x 'y.
Lemma rule_is_empty : forall L p,
triple (val_is_empty p)
(MQueue L p)
(fun r => \[r = isTrue (L = nil)] \* MQueue L p).
Proof using.
xcf. unfold MQueue. xpull ;=> pf pb vx vy.
xapps. xapps.
xchanges (MListSeg_then_MCell_inv_neq pf pb) ;=> R.
(* xchange (MListSeg_then_MCell_inv_neq pf pb). xpull ;=> R. *)
xapp. hsimpl. isubst. fequals. rew_bool_eq. rewrite R. iff; congruence.
Qed.
Hint Extern 1 (Register_spec val_is_empty) => Provide rule_is_empty.
(* ---------------------------------------------------------------------- *)
(** Push back *)
Definition val_push_back :=
ValFun 'v 'p :=
Let 'q := val_get_tl 'p in
Let 'r := val_alloc 2 in
val_set_hd 'q 'v ;;
val_set_tl 'q 'r ;;
val_set_tl 'p 'r.
Lemma rule_push_back : forall L v p,
triple (val_push_back v p)
(MQueue L p)
(fun r => \[r = val_unit] \* MQueue (L&v) p).
Proof using.
xcf. unfold MQueue. xpull ;=> pf pb vx vy.
xapps. xapp rule_alloc_cell as r. intros pb' v1 v2. intro_subst.
xapp~. xapp~. xapp~. hchanges~ MListSeg_last.
Qed.
(* ---------------------------------------------------------------------- *)
(** Push front *)
Definition val_push_front :=
ValFun 'v 'p :=
Let 'q := val_get_hd 'p in
Let 'r := val_new_cell 'v 'q in
val_set_hd 'p 'r.
Lemma rule_push_front : forall L v p,
triple (val_push_front v p)
(MQueue L p)
(fun r => \[r = val_unit] \* MQueue (v::L) p).
Proof using.
xcf. unfold MQueue. xpull ;=> pf pb vx vy.
xapps. xapp as r. intros x. intro_subst.
xapp. hsimpl~. isubst. hchanges (@MListSeg_cons x).
Qed.
(* ---------------------------------------------------------------------- *)
(** Pop front *)
Definition val_pop_front :=
ValFun 'v 'p :=
Let 'q := val_get_hd 'p in
Let 'x := val_get_hd 'q in
Let 'r := val_get_tl 'q in
val_set_hd 'p 'r;;
'x.
Lemma rule_pop_front : forall L v p,
L <> nil ->
triple (val_pop_front v p)
(MQueue L p)
(fun v => Hexists L', \[L = v::L'] \* MQueue L' p).
Proof using.
xcf. unfold MQueue. xpull ;=> pf pb vx vy.
destruct L as [|x L']; tryfalse.
rewrite MListSeg_cons_eq. xpull ;=> pf'.
xapps. xapps. xapps. xapp~. xvals~.
Qed.
Lemma rule_pop_front' : forall L v p x,
triple (val_pop_front v p)
(MQueue (x::L) p)
(fun r => \[r = x] \* MQueue L p).
Proof using.
intros. xapply (@rule_pop_front (x::L)).
{ auto_false. }
{ hsimpl. }
{ intros r. hpull ;=> L' E. inverts E. hsimpl~. }
Qed.
(* ---------------------------------------------------------------------- *)
(** Transfer *)
Definition val_transfer :=
ValFun 'p1 'p2 :=
Let 'e2 := val_is_empty 'p2 in
If_ val_not 'e2 Then
Let 'b1 := val_get_tl 'p1 in
Let 'f2 := val_get_hd 'p2 in
Let 'x2 := val_get_hd 'f2 in
Let 'n2 := val_get_tl 'f2 in
Let 'b2 := val_get_tl 'p2 in
val_set_tl 'p1 'b2 ;;
val_set_hd 'b1 'x2 ;;
val_set_tl 'b1 'n2 ;;
val_set_tl 'p2 'f2
End.
Lemma rule_transfer : forall L1 L2 p1 p2,
triple (val_transfer p1 p2)
(MQueue L1 p1 \* MQueue L2 p2)
(fun r => \[r = val_unit] \* MQueue (L1 ++ L2) p1 \* MQueue nil p2).
Proof using.
xcf. xapps. xapps. xif ;=> C.
{ unfold MQueue. xpull ;=> pf2 pb2 vx2 vy2 pf1 pb1 vx1 vy1.
destruct L2 as [|x L2']; tryfalse.
xchanges MListSeg_cons_eq ;=> pf2'.
xapps. xapps. xapps. xapps.
xapps~. xapps~. xapps~. xapps~. xapps~.
intros r. hchange (MListSeg_last pf1).
hchange (MListSeg_concat pf1 pf2' pb2). rew_list.
hchange (MListSeg_nil pf2). hsimpl~. }
{ subst. rew_list. xvals~. }
Qed.
This diff is collapsed.
......@@ -566,7 +566,7 @@ Ltac xcf_get_fun_from_goal tt ::=
Ltac xcf_post tt ::=
simpl; rew_enc_dyn.
(** todo: follow similar strategy to avoid the need to fold in LambdaCF *)
(** TODO URGENT: follow similar strategy to avoid the need to fold in LambdaCF *)
Ltac xcf_trm n :=
applys Triple_trm_of_Cf_iter n; [ xcf_post tt ].
......
......@@ -54,6 +54,26 @@ Qed.
Hint Extern 1 (Register_spec val_incr) => Provide rule_incr.
(* ---------------------------------------------------------------------- *)
(** Decrement function *)
Definition val_decr :=
ValFun 'p :=
Let 'n := val_get 'p in
Let 'm := 'n '- 1 in
val_set 'p 'm.
Lemma rule_decr : forall p n,
triple (val_decr p)
(p ~~~> n)
(fun r => \[r = val_unit] \* (p ~~~> (n-1))).
Proof using.
xcf. xapps. xapps. xapps. hsimpl~.
Qed.
Hint Extern 1 (Register_spec val_decr) => Provide rule_decr.
(* ---------------------------------------------------------------------- *)
(** Negation *)
......
......@@ -111,6 +111,22 @@ Qed.
Hint Extern 1 (Register_Spec val_incr) => Provide Rule_incr.
(* ---------------------------------------------------------------------- *)
(* ** Decrement *)
(** [val_decr] defined in [ExampleBasicNonLifted.v] *)
Lemma Rule_decr : forall (p:loc) (n:int),
Triple (val_decr `p)
PRE (p ~~> n)
POST (fun (r:unit) => p ~~> (n-1)).
Proof using.
xcf. xapps. xapps. xapps. hsimpl~.
Qed.
Hint Extern 1 (Register_Spec val_decr) => Provide Rule_decr.
(* ---------------------------------------------------------------------- *)
(* ** Negation *)
......
......@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term
# Compilation.
# Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList
# The official list of files that should be compiled by [make]
......
......@@ -294,7 +294,7 @@ Delimit Scope heap_scope with heap.
(** [H1 ==+> H2] is short for [H1 ==> H1 \* H2] *)
Notation "H1 ==+> H2" := (H1%heap ==> H1%heap \* H2%heap)
(at level 55) : heap_scope.
(at level 55, only parsing) : heap_scope.
(* ---------------------------------------------------------------------- *)
......