Commit a761ee45 authored by charguer's avatar charguer

restructure cf tactic notation

parent 76cbd8d1
......@@ -10,7 +10,8 @@ License: MIT.
From Sep Require Export LambdaSepLifted LambdaCFLifted.
From Sep Require Export LambdaStructLifted.
From TLC Require Export LibListZ.
From TLC Require Export LibList LibListZ.
Open Scope liblist_scope.
Open Scope Z_scope.
(* Open Scope charac. TODO: not needed? *)
......
......@@ -220,7 +220,8 @@ Lemma rule_test_mkcounter :
\[]
(fun r => \[r = 3]).
Proof using.
xcf. xapp as C.
xcf_trm 100%nat. (* todo: make xcf work *)
xapp as C.
xapps Rule_MCount.
xapps Rule_MCount.
xapps.
......
......@@ -30,6 +30,10 @@ 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.
(* ---------------------------------------------------------------------- *)
(** Create *)
Definition val_create :=
ValFun 'v :=
Let 'r := val_alloc 2 in
......
(**
This file formalizes example in Separation Logic with read-only predicates
Author: Arthur Charguéraud.
License: MIT.
*)
Set Implicit Arguments.
From Sep Require Import LambdaCFSep.
Generalizable Variables A B.
Ltac auto_star ::= jauto.
Implicit Types p q : loc.
Implicit Types n : int.
Implicit Types v : val.
(* ********************************************************************** *)
(* * Formalisation of higher-order iterator on a reference *)
(* ---------------------------------------------------------------------- *)
(** Apply a function to the contents of a reference *)
Definition val_ref_apply :=
ValFun 'f 'p :=
Let 'x := val_get 'p in
'f 'x.
Lemma rule_ref_apply : forall (f:val) (p:loc) (v:val),
(triple (f v)
PRE (RO(p ~~~> v) \* H)
POST Q)
->
(triple (val_ref_apply f r)
PRE (RO(p ~~~> v) \* H)
POST Q).
Proof using.
admit.
Qed.
(* Note: this specification allows [f] to call [val_get] on [r],
as illustrated next *)
Definition val_demo_1 :=
ValFun 'n :=
Let 'p := val_ref n in
LetFun 'f 'x :=
Let 'y := val_get 'p in
val_add 'x 'y in
val_ref_apply 'f 'p.
Lemma rule_demo_1 : forall (n:int),
(triple (val_demo_1 n)
PRE \[]
POST (fun r => \[r = val_int (2*n)]).
Proof using.
admit.
Qed.
(* ---------------------------------------------------------------------- *)
(** In-place update of a reference by applying a function *)
Definition val_ref_update :=
ValFun 'f 'p :=
Let 'x := val_get 'p in
Let 'y := 'f 'x in
val_set 'r 'y.
Lemma rule_ref_update : forall (f:val) (p:loc) (v:val),
(triple (f v)
PRE (RO(p ~~~> v) \* H)
POST Q)
->
(triple (val_ref_apply f r)
PRE (p ~~~> v \* H)
POST (fun r => \[r = val_unit] \* \Hexists w, (p ~~~> w) \* (Q w))).
Proof using.
admit.
Qed.
(* ********************************************************************** *)
(* * Formalisation of records *)
(* ---------------------------------------------------------------------- *)
(** Read to a record field *)
Definition val_get_field (k:field) :=
ValFun 'p :=
Let 'q := val_ptr_add 'p (nat_to_Z k) in
val_get 'q.
Lemma rule_get_field : forall l k v,
triple ((val_get_field k) l)
(l `.` k ~~~> v)
(fun r => \[r = v] \* (l `.` k ~~~> v)).
Proof using.
intros. applys rule_app_fun. reflexivity. simpl.
applys rule_let. { xapplys rule_ptr_add_nat. }
intros r. simpl. xpull. intro_subst.
rewrite hfield_eq_fun_hsingle.
xpull ;=> N. xapplys~ rule_get.
Qed.
(* ---------------------------------------------------------------------- *)
(** Write to a record field *)
Definition val_set_field (k:field) :=
ValFun 'p 'v :=
Let 'q := val_ptr_add 'p (nat_to_Z k) in
val_set 'q 'v.
Lemma rule_set_field : forall v' l k v,
triple ((val_set_field k) l v)
(l `.` k ~~~> v')
(fun r => \[r = val_unit] \* (l `.` k ~~~> v)).
Proof using.
intros. applys rule_app_fun2. reflexivity. auto. simpl.
applys rule_let. { xapplys rule_ptr_add_nat. }
intros r. simpl. xpull. intro_subst.
rewrite hfield_eq_fun_hsingle.
xpull ;=> N. xapplys~ rule_set.
Qed.
Arguments rule_set_field : clear implicits.
(* ********************************************************************** *)
(* * List cells *)
(* ---------------------------------------------------------------------- *)
(** Representation *)
(** Identification of head and tail fields *)
Definition hd : field := 0%nat.
Definition tl : field := 1%nat.
(** [Mcell v q p] describes one list cell allocated at address [p],
with head value [v] and tail value [q]. *)
Definition MCell (v:val) (q:val) (p:loc) :=
(p `.` hd ~~~> v) \* (p `.` tl ~~~> q).
(* ---------------------------------------------------------------------- *)
(** Tactics *)
(** Tactic hack to make [hsimpl] able to cancel out [hfield]
and [Mcell] predicates in heap entailment.
Later won't be needed when using [~>] notation. *)
Ltac hcancel_hook H ::=
match H with
| hsingle _ _ => hcancel_try_same tt
| hfield _ _ _ => hcancel_try_same tt
| MCell _ _ _ => hcancel_try_same tt
end.
(* ---------------------------------------------------------------------- *)
(** Properties of list cells *)
Lemma MCell_eq : forall (v:val) (q:val) (p:loc),
MCell v q p = (p `.` hd ~~~> v) \* (p `.` tl ~~~> q).
Proof using. auto. Qed.
Lemma MCell_inv_not_null : forall p v q,
(MCell v q p) ==+> \[p <> null].
(* i.e. (MCell v q p) ==> (MCell v q p) \* \[p <> null]. *)
Proof using.
intros. unfold MCell, hd.
hchange~ (hfield_not_null p hd). hsimpl~.
Qed.
Arguments MCell_inv_not_null : clear implicits.
Lemma MCell_null_false : forall v q,
(MCell v q null) ==> \[False].
Proof using. intros. hchanges~ (MCell_inv_not_null null). Qed.
Arguments MCell_null_false : clear implicits.
Lemma MCell_hstar_MCell_inv : forall p1 p2 x1 x2 y1 y2,
MCell x1 y1 p1 \* MCell x2 y2 p2 ==+> \[p1 <> p2].
Proof using.
intros. do 2 rewrite MCell_eq. tests C: (p1 = p2).
{ hchanges (@hstar_hfield_same_loc_disjoint p2 hd). }
{ hsimpl~. }
Qed.
(* ---------------------------------------------------------------------- *)
(** Access to list cells *)
(** Read to head *)
Definition val_get_hd := val_get_field hd.
Lemma rule_get_hd : forall p v q,
triple (val_get_hd p)
(MCell v q p)
(fun r => \[r = v] \* (MCell v q p)).
Proof using.
intros. unfold MCell. xapplys rule_get_field. auto.
Qed.
Hint Extern 1 (Register_spec val_get_hd) => Provide rule_get_hd.
(** Read to tail *)
Definition val_get_tl := val_get_field tl.
Lemma rule_get_tl : forall p v q,
triple (val_get_tl p)
(MCell v q p)
(fun r => \[r = q] \* (MCell v q p)).
Proof using.
intros. unfold MCell.
xapplys rule_get_field. auto.
Qed.
Hint Extern 1 (Register_spec val_get_tl) => Provide rule_get_tl.
(** Write to head *)
Definition val_set_hd := val_set_field hd.
Lemma rule_set_hd : forall p v' v vq,
triple (val_set_hd p v)
(MCell v' vq p)
(fun r => \[r = val_unit] \* MCell v vq p).
Proof using.
intros. unfold MCell. xapplys (rule_set_field v'). auto.
Qed.
Hint Extern 1 (Register_spec val_set_hd) => Provide rule_set_hd.
(** Write to tail *)
Definition val_set_tl := val_set_field tl.
Lemma rule_set_tl : forall p v q vq',
triple (val_set_tl p q)
(MCell v vq' p)
(fun r => \[r = val_unit] \* MCell v q p).
Proof using.
intros. unfold MCell. xapplys (rule_set_field vq'). auto.
Qed.
Hint Extern 1 (Register_spec val_set_tl) => Provide rule_set_tl.
(* ---------------------------------------------------------------------- *)
(** Allocation of list cells *)
Definition val_new_cell :=
ValFun 'x 'y :=
Let 'p := val_alloc 2 in
val_set_hd 'p 'x;;;
val_set_tl 'p 'y;;;
'p.
Lemma rule_alloc_cell :
triple (val_alloc 2)
\[]
(fun r => Hexists (p:loc), Hexists v1 v2,
\[r = p] \* MCell v1 v2 p).
Proof using.
xapply rule_alloc. { math. } { hsimpl. }
{ intros r. hpull ;=> l (E&N). subst.
simpl_abs. rew_Alloc. hpull ;=> v1 v2.
unfold MCell. rewrite hfield_eq_fun_hsingle.
unfold hd, tl. hsimpl~ l v1 v2.
math_rewrite (l + 1 = S l)%nat.
math_rewrite (l+0 = l)%nat. hsimpl. }
Qed.
Lemma rule_new_cell : forall v q,
triple (val_new_cell v q)
\[]
(fun r => Hexists p, \[r = val_loc p] \* MCell v q p).
Proof using.
intros. xcf. xapp rule_alloc_cell.
intros p p' v' q'. intro_subst.
xapps~. xapps~. xvals~.
Qed.
(* TODO: update?
Lemma rule_new_cell : forall v q,
triple (val_new_cell v q)
\[]
(fun r => Hexists p, \[r = val_loc p] \* MCell v q p).
Proof using.
intros. applys rule_app_fun2. reflexivity. auto. simpl.
applys rule_let. { applys rule_alloc_cell. }
intros p. xpull ;=> p' v' q'. intro_subst. simpl.
applys rule_seq. { xapplys rule_set_hd. }
applys rule_seq. { xapplys rule_set_tl. }
applys rule_val. hsimpl. auto.
Qed.
*)
Hint Extern 1 (Register_spec val_new_cell) => Provide rule_new_cell.
Global Opaque MCell_eq.
(* ********************************************************************** *)
(* * Mutable lists Segments *)
(* ---------------------------------------------------------------------- *)
(** Representation *)
Fixpoint MListSeg (q:loc) (L:list val) (p:loc) : hprop :=
match L with
| nil => \[p = q]
| x::L' => Hexists (p':loc), (MCell x p' p) \* (MListSeg q L' p')
end.
(* ---------------------------------------------------------------------- *)
(** Hack *)
(** Tactic hack to make [hsimpl] able to cancel out [MList]
in heap entailment. *)
Ltac hcancel_hook H ::=
match H with
| hsingle _ _ => hcancel_try_same tt
| hfield _ _ _ => hcancel_try_same tt
| MCell _ _ _ => hcancel_try_same tt
(* TODO | MList _ _ => hcancel_try_same tt *)
| MListSeg _ _ _ => hcancel_try_same tt
end.
(* ---------------------------------------------------------------------- *)
(** Properties *)
Section Properties.
Implicit Types L : list val.
Lemma MListSeg_nil_eq : forall p q,
MListSeg q nil p = \[p = q].
Proof using. intros. unfolds~ MListSeg. Qed.
Lemma MListSeg_cons_eq : forall p q x L',
MListSeg q (x::L') p =
Hexists (p':loc), MCell x p' p \* MListSeg q L' p'.
Proof using. intros. unfold MListSeg at 1. simple~. Qed.
Global Opaque MListSeg.
Lemma MListSeg_nil : forall p,
\[] ==> MListSeg p nil p.
Proof using. intros. rewrite MListSeg_nil_eq. hsimpl~. Qed.
Lemma MListSeg_cons : forall p p' q x L',
MCell x p' p \* MListSeg q L' p' ==> MListSeg q (x::L') p.
Proof using. intros. rewrite MListSeg_cons_eq. hsimpl. Qed.
Lemma MListSeg_one : forall p q x,
MCell x q p ==> MListSeg q (x::nil) p.
Proof using.
intros. hchange (@MListSeg_nil q). hchange MListSeg_cons. hsimpl.
Qed.
Lemma MListSeg_concat : forall p1 p2 p3 L1 L2,
MListSeg p2 L1 p1 \* MListSeg p3 L2 p2 ==> MListSeg p3 (L1++L2) p1.
Proof using.
intros. gen p1. induction L1 as [|x L1']; intros.
{ rewrite MListSeg_nil_eq. hpull ;=> E. subst. rew_list~. }
{ rew_list. hchange (MListSeg_cons_eq p1). hpull ;=> p1'.
hchange (IHL1' p1'). hchanges (@MListSeg_cons p1). }
Qed.
Lemma MListSeg_last : forall p1 p2 p3 x L,
MListSeg p2 L p1 \* MCell x p3 p2 ==> MListSeg p3 (L&x) p1.
Proof using.
intros. hchange (@MListSeg_one p2). hchanges MListSeg_concat.
Qed.
Lemma MListSeg_then_MCell_inv_neq : forall p q L v1 v2,
MListSeg q L p \* MCell v1 v2 q ==>
MListSeg q L p \* MCell v1 v2 q \* \[L = nil <-> p = q].
Proof using.
intros. destruct L.
{ rewrite MListSeg_nil_eq. hsimpl*. split*. (* TODO: why not proved? *) }
{ rewrite MListSeg_cons_eq. hpull ;=> p'. tests: (p = q).
{ hchanges (@MCell_hstar_MCell_inv q). }
{ hsimpl. split; auto_false. } }
Qed.
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.
(* ---------------------------------------------------------------------- *)
(** Copy *)
Parameter val_mqueue_copy : val.
Parameter rule_mqueue_copy : forall p (L:list val),
triple (val_mqueue_copy p)
PRE (RO (p ~> MList L))
POST (fun r => Hexists p', \[r = val_loc p'] \* (p' ~> MList L)).
Hint Extern 1 (Register_spec val_mqueue_copy) => Provide rule_mqueue_copy.
(* ---------------------------------------------------------------------- *)
(** Transfer *)
Parameter val_transfer : val.
Parameter rule_transfer : forall L1 L2 p1 p2,
triple (val_transfer p1 p2)
PRE (p1 ~> MQueue L1 \* p2 ~> MQueue L2)
POST (fun r => \[r = val_unit] \* p1 ~> MQueue (L1 ++ L2) \* p2 ~> MQueue nil).
Hint Extern 1 (Register_spec val_transfer) => Provide rule_transfer.
(* ---------------------------------------------------------------------- *)
(** Copy-Transfer *)
Definition val_copy_transfer :=
ValFun 'p1 'p2 :=
Let 'p3 := val_mqueue_copy 'p2 in
val_transfer 'p1 'p3.
Lemma rule_copy_transfer : forall L1 L2 p1 p2,
triple (val_transfer p1 p2)
PRE (p1 ~> MQueue L1 \* RO(p2 ~> MQueue L2))
POST (fun r => \[r = val_unit] \* p1 ~> MQueue (L1 ++ L2)).
Proof using.
Qed.
Hint Extern 1 (Register_spec val_copy_transfer) => Provide rule_copy_transfer.
......@@ -11,6 +11,7 @@ License: MIT.
Set Implicit Arguments.
From Sep Require Import LambdaCF LambdaStruct.
From TLC Require Import LibList.
Generalizable Variables A B.
Ltac auto_star ::= jauto.
......
......@@ -10,7 +10,7 @@ License: MIT.
Set Implicit Arguments.
From TLC Require Export LibFix.
From Sep Require Export LambdaSep.
From Sep Require Export LambdaSepRO LambdaCFTactics.
Open Scope heap_scope.
Implicit Types v w : val.
......@@ -408,7 +408,7 @@ Notation "'Register_spec' f" := (Register_rule (trm_apps (trm_val f) _))
the specification that could apply to a goal [G].
It places the specification as hypothesis at the head of the goal. *)
Ltac xapp_basic_prepare tt := (* defined further *)
Ltac xapp_basic_prepare tt ::= (* actually defined further *)
idtac.
Ltac xspec_context G := (* refined only in LambdaCFLifted *)
......@@ -449,41 +449,21 @@ Hint Extern 1 (Register_spec (val_prim val_ptr_add)) => Provide rule_ptr_add.
(* ********************************************************************** *)
(* * Tactics for progressing through proofs *)
(** Extends tactics defined in [LambdaCFTactics.v] *)
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xcf] *)
Ltac xcf_get_fun_remove_encs f :=
constr:(f).
Ltac xcf_get_fun_from_trm t :=
match t with
| trm_apps (trm_val ?f) _ => xcf_get_fun_remove_encs f
| trm_app ?t1 ?t2 =>
match t1 with
| trm_app ?t11 ?t12 => xcf_get_fun_from_trm t1
| ?f => xcf_get_fun_remove_encs f
end
end.
Ltac xcf_get_fun_from_goal tt :=
Ltac xcf_get_fun_from_goal tt ::=
match goal with |- triple ?t _ _ => xcf_get_fun_from_trm t end.
Ltac xcf_get_fun tt :=
xcf_get_fun_from_goal tt.
Ltac xcf_reveal_fun tt :=
try (let f := xcf_get_fun tt in
first [ unfold f
| match goal with H: f = _ |- _ => rewrite H end ]).
Ltac xcf_post tt :=
simpl.
Ltac xcf_trm n :=
Ltac xcf_trm n ::=
applys triple_trm_of_cf_iter n; [ xcf_post tt ].
Ltac xcf_basic_fun n f' :=
Ltac xcf_basic_fun n f' ::=
let f := xcf_get_fun tt in
match f with
| val_funs _ _ => (* TODO: use (apply (@..)) instead of applys? same in cflifted *)
......@@ -497,79 +477,37 @@ Ltac xcf_basic_fun n f' :=
| xcf_post tt ]
end.
Ltac xcf_prepare_args tt :=
rew_nary.
Ltac xcf_fun n :=
xcf_prepare_args tt;
let f' := xcf_get_fun tt in
xcf_reveal_fun tt;
rew_nary;
rew_vals_to_trms;
xcf_basic_fun n f'.
Ltac xcf_core n :=
intros; first [ xcf_fun n | xcf_trm n ].
Tactic Notation "xcf" :=
xcf_core 100%nat.
Tactic Notation "xcf_depth" constr(depth) :=
xcf_core depth.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xseq] *)
Ltac xseq_core tt :=
Ltac xseq_core tt ::=
applys local_erase; esplit; split.
Tactic Notation "xseq" :=
xseq_core tt.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xlet] *)
Ltac xlet_core tt :=
Ltac xlet_core tt ::=
applys local_erase; esplit; split.
Tactic Notation "xlet" :=
xlet_core tt.
Ltac xlet_as_core X :=
xlet_core tt; [ | intros X ].
Tactic Notation "xlet" "as" simple_intropattern(X) :=
xlet_as_core X.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xif] *)
Ltac xif_post tt :=
rew_bool_eq.
Ltac xif_core tt :=
Ltac xif_core tt ::=
applys local_erase; esplit; splits;
[ try reflexivity
| xif_post tt
| xif_post tt ].
Tactic Notation "xif" :=
xif_core tt.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xfail] *)
Ltac xfail_core tt :=
Ltac xfail_core tt ::=
applys local_erase; unfold cf_fail.
Tactic Notation "xfail" :=
xfail_core tt.
(* ---------------------------------------------------------------------- *)
(* * [xapp] and [xapps] and [xapp as] *)
......@@ -588,19 +526,25 @@ Tactic Notation "xfail" :=
*)
Ltac xapp_let_cont tt :=
Ltac hpull_cont tt ::=
try hpull.
Ltac hsimpl_cont tt ::=
hsimpl.
Ltac xapp_let_cont tt ::=
let X := fresh "X" in intros X;
instantiate; try xpull; gen X.
Ltac xapp_as_let_cont tt :=
Ltac xapp_as_let_cont tt ::=
instantiate; try xpull.
Ltac xapps_let_cont tt :=
Ltac xapps_let_cont tt ::=
let X := fresh "X" in intros X;
instantiate; try xpull;
first [ intro_subst | gen X ].
Ltac xapp_template xlet_tactic xapp_tactic xlet_cont :=
Ltac xapp_template xlet_tactic xapp_tactic xlet_cont ::=
match goal with
| |- local (cf_let _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
| |- local (cf_if _ _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
......@@ -620,13 +564,7 @@ Ltac xapp_basic_prepare tt ::=
try match goal with |- local _ _ _ => apply local_erase end;
rew_nary.
Ltac hpull_cont tt :=
try hpull.
Ltac hsimpl_cont tt :=
hsimpl.
Ltac xapp_with_args E cont_xapply :=
Ltac xapp_with_args E cont_xapply ::=
match E with
| __ => (* no spec provided *)
let S := fresh "Spec" in
......@@ -647,75 +585,11 @@ Ltac xapp_with_args E cont_xapply :=
end
end.
Ltac xapp_basic E cont_post tt :=
Ltac xapp_basic E cont_post tt ::=
xapp_basic_prepare tt;
xapp_with_args E ltac:(fun H =>
xapp_xapply H cont_post).
Ltac xapp_debug tt :=
xapp_basic_prepare tt;
xapp_with_args __ ltac:(fun H => generalize H).
Ltac xapp_core tt :=
xapp_template ltac:(fun tt => xlet) ltac:(xapp_basic __ idcont) ltac:(xapp_let_cont).
Ltac xapp_arg_core E :=
xapp_template ltac:(fun tt => xlet) ltac:(xapp_basic E idcont) ltac:(xapp_let_cont).
Ltac xapp_as_core X :=