Commit 8860950f authored by charguer's avatar charguer

progress lifted

parent c644ef07
......@@ -57,9 +57,6 @@ Proof using. intros. unfolds. rewrite~ local_local. Qed.
Hint Resolve local_is_local.
Ltac xlocal_core tt ::=
try first [ applys local_is_local | applys is_local_triple | assumption ].
(********************************************************************)
(* ** Characteristic formula generator *)
......@@ -474,10 +471,18 @@ Proof using. introv EF M. applys* cf_sound_app. Qed.
(********************************************************************)
(* ** CF tactics *)
Module MLCFTactics.
Ltac xlocal_core tt ::=
try first [ applys local_is_local | applys is_local_triple | assumption ].
(*------------------------------------------------------------------*)
(* ** Notation for characteristic formulae *)
Notation "'Ret' v" :=
Notation "'Val' v" :=
(local (cf_val v))
(at level 69) : charac.
......@@ -519,25 +524,7 @@ Notation "'Fail'" :=
(at level 69) : charac.
Open Scope charac.
(*--------------------------------------------------------*)
(* ** Tactic [xspec] *)
(** [xspec] shows the specification that [xapp] would use. More generally,
[xspec f] retreives from either the context or from
the database of characteristic formulae (i.e. "database_spec")
the specification associated with [f].
It places the specification as hypothesis at the head of the goal. *)
Definition database_spec := True.
Notation "'RegisterSpec' T" := (Register database_spec T)
(at level 69) : charac.
Tactic Notation "xspec" constr(f) :=
ltac_database_get database_spec f.
(*--------------------------------------------------------*)
(* ** Tactics for conducting proofs *)
......@@ -548,7 +535,7 @@ Tactic Notation "xcf" :=
[ try reflexivity
| simpl; try fold f].
Tactic Notation "xret" :=
Tactic Notation "xval" :=
applys local_erase; unfold cf_val.
Tactic Notation "xif" :=
......@@ -583,3 +570,4 @@ Hint Extern 1 (RegisterSpec (app (val_prim prim_add) _ _ _)) =>
Provide rule_add.
End MLCFTactics.
......@@ -11,7 +11,7 @@ License: MIT.
Set Implicit Arguments.
Require Import LibCore MLSepLifted MLCF.
Require Export LibCore MLSepLifted MLCF.
Generalizable Variables A B.
Open Scope trm_scope.
......@@ -60,7 +60,7 @@ Definition local (F:formula) : formula :=
(** Lifting of the [app] predicate *)
Definition App f (Vs:dyns) `{Enc A} H (Q:A->hprop) :=
Definition App (f:func) (Vs:dyns) `{Enc A} H (Q:A->hprop) :=
Triple (trm_app f (encs Vs)) H Q.
......@@ -80,8 +80,9 @@ Proof using. intros. unfolds. rewrite~ Local_local. Qed.
Hint Resolve Local_is_local.
Ltac xlocal_core tt ::=
try first [ applys Local_is_local | applys is_local_triple | assumption ].
Lemma App_is_local : forall (f:func) (Vs:dyns) A `{EA:Enc A},
is_local (@App f Vs A EA).
Proof using. intros. unfold App. applys Triple_is_local. Qed.
(*------------------------------------------------------------------*)
......@@ -90,10 +91,10 @@ Ltac xlocal_core tt ::=
(** These auxiliary definitions give the characteristic formula
associated with each term construct. *)
Definition Cf_val v : formula := fun `{Enc A} H (Q:A->hprop) =>
Definition Cf_val (v:val) : formula := fun `{Enc A} H (Q:A->hprop) =>
exists V, v = enc V /\ H ==> Q V.
Definition Cf_if_val v (F1 F2 : formula) : formula := fun `{Enc A} H (Q:A->hprop) =>
Definition Cf_if_val (v:val) (F1 F2 : formula) : formula := fun `{Enc A} H (Q:A->hprop) =>
exists (V:int), v = enc V /\
(V <> 0 -> 'F1 H Q) /\ (V = 0 -> 'F2 H Q).
......@@ -110,7 +111,7 @@ Definition Cf_let (F1 : formula) (F2of : forall `{EA1:Enc A1}, A1 -> formula) :
Definition Cf_if (F0 F1 F2 : formula) : formula :=
Cf_let F0 (fun A1 EA1 X => Cf_if_val (enc X) F1 F2).
Definition Cf_app f vs : formula := fun `{Enc A} H (Q:A->hprop) =>
Definition Cf_app (f:val) (vs:vals) : formula := fun `{Enc A} H (Q:A->hprop) =>
exists Vs, vs = encs Vs /\ App f Vs H Q.
Definition Cf_fix (n:nat) (F1of : func -> dyns -> formula) (F2of : func -> formula) : formula :=
......@@ -255,8 +256,6 @@ Proof. intros. simpl_Cf. destruct T; apply Local_is_local. Qed.
Definition Sound_for (t:trm) (F:formula) :=
forall `{EA:Enc A} H (Q:A->hprop), 'F H Q -> Triple t H Q.
Print Triple.
(* todo: move *)
Lemma is_local_Triple : forall A `{EA:Enc A} (t:trm),
is_local (@Triple t A EA).
......@@ -353,51 +352,88 @@ Proof using. introv EF M. applys* Cf_sound_App. Qed.
(********************************************************************)
(* ** CFLifted tactics *)
Module MLCFLiftedTactics.
Ltac xlocal_core tt ::=
try first [ applys Local_is_local
| applys App_is_local
| applys is_local_triple
| assumption ].
(*------------------------------------------------------------------*)
(* ** Notation for characteristic formulae *)
Notation "'Ret' v" :=
(local (Cf_val v))
Notation "'Val' v" :=
(Local (Cf_val v))
(at level 69) : charac.
Notation "'If_' v 'Then' F1 'Else' F2" :=
(local (Cf_if_val v F1 F2))
(Local (Cf_if_val v F1 F2))
(at level 69, v at level 0) : charac.
(*
Notation "'If_'' V 'Then' F1 'Else' F2" :=
(Local (Cf_if_val (enc V) F1 F2))
(at level 69, V at level 0) : charac.
*)
Notation "'Seq_' F1 ;; F2" :=
(local (Cf_seq F1 F2))
(Local (Cf_seq F1 F2))
(at level 68, right associativity,
format "'[v' 'Seq_' '[' F1 ']' ;; '/' '[' F2 ']' ']'") : charac.
Notation "'Let' x ':=' F1 'in' F2" :=
(local (Cf_let F1 (fun x => F2)))
(Local (Cf_let F1 (fun _ _ x => F2)))
(at level 69, x ident, right associativity,
format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac.
(* TODO: notation for App should not include local, same for Cf *)
Notation "'Let' [ A EA ] x ':=' F1 'in' F2" :=
(Local (Cf_let F1 (fun A EA x => F2)))
(at level 69, A at level 0, EA at level 0, x ident, right associativity,
format "'[v' '[' 'Let' [ A EA ] x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac.
Notation "'App' f x1 ;" :=
(local (Cf_app f [x1]))
Notation "'App_' f x1 ;" :=
(Local (Cf_app f [x1]))
(at level 68, f at level 0, x1 at level 0) : charac.
Notation "'App' f x1 x2 ;" :=
(local (Cf_app f [x1; x2]))
Notation "'App_' f x1 x2 ;" :=
(Local (Cf_app f [x1; x2]))
(at level 68, f at level 0, x1 at level 0,
x2 at level 0) : charac.
Notation "'App' f x1 x2 x3 ;" :=
(local (Cf_app f [x1; x2; x3]))
Notation "'App_' f x1 x2 x3 ;" :=
(Local (Cf_app f [x1; x2; x3]))
(at level 68, f at level 0, x1 at level 0, x2 at level 0,
x3 at level 0) : charac.
Notation "'App' f x1 x2 x3 x4 ;" :=
(local (Cf_app f [x1; x2; x3; x4]))
Notation "'App_' f x1 x2 x3 x4 ;" :=
(Local (Cf_app f [x1; x2; x3; x4]))
(at level 68, f at level 0, x1 at level 0, x2 at level 0,
x3 at level 0, x4 at level 0) : charac.
Notation "'Fail'" :=
(local Cf_fail)
(at level 69) : charac.
(** Record contents *)
Notation "`'{ f1 := x1 }" :=
((f1, Dyn x1)::nil)
(at level 0, f1 at level 0)
: charac.
Notation "`'{ f1 := x1 ; f2 := x2 }" :=
((f1, Dyn x1)::(f2, Dyn x2)::nil)
(at level 0, f1 at level 0, f2 at level 0)
: charac.
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 }" :=
((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0)
: charac.
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" :=
((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::(f4, Dyn x4)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
: charac.
Open Scope charac.
......@@ -405,28 +441,47 @@ Open Scope charac.
(*--------------------------------------------------------*)
(* ** Tactics for conducting proofs *)
(* TODO: update
Tactic Notation "xCf" :=
let f := match goal with |- app ?f _ _ _ => constr:(f) end in
Tactic Notation "xcf" :=
let f := match goal with |- App ?f _ _ _ => constr:(f) end in
applys Cf_sound_App1 20%nat;
[ try reflexivity
| simpl; try fold f].
| simpl; unfold dyn_val; simpl; try fold f; try fold dyn_val].
Tactic Notation "xret" :=
applys local_erase; unfold Cf_val.
Tactic Notation "xval" :=
applys local_erase; unfold Cf_val;
try (
match goal with |- exists _, ?v = _ /\ _ => exists (dyn_value (decode v)) end;
simpl enc; simpl dyn_value; split; [ reflexivity | ]).
Tactic Notation "xif" :=
applys local_erase; split.
applys local_erase; unfold Cf_if;
try esplit; split; [ reflexivity | split ].
Lemma Cf_let_prove : forall A1 (EA1:id Enc A1) (Q1:A1->hprop) (F1 : formula) (F2of : forall A1 `{EA1:Enc A1}, A1 -> formula),
forall A (EA:id Enc A) H (Q:A->hprop),
F1 A1 EA1 H Q1 ->
(forall (X:A1), (@F2of A1 EA1 X) A EA (Q1 X) Q) ->
(Cf_let F1 (@F2of)) A EA H Q.
Proof using. intros. hnf. exists A1 EA1 Q1. auto. Qed.
Tactic Notation "xlet" :=
applys local_erase; esplit; split.
applys local_erase; eapply @Cf_let_prove.
(* TODO: why does not work?
applys local_erase;
let A := fresh "A" in let EA := fresh "E" A in
evar (A:Type); evar (EA:Enc A); exists A EA; subst A EA;
esplit; split. *)
Ltac xapp_setup tt :=
applys local_erase; unfold Cf_app;
match goal with |- exists _, ?L = _ /\ _ => exists (decodes L) end;
simpl decodes; split; [ reflexivity | ].
Tactic Notation "xapp" constr(E) :=
applys local_erase; unfold Cf_app;
xapplys E.
xapp_setup tt; xapplys E.
Tactic Notation "xapp" :=
applys local_erase; unfold Cf_app;
xapp_setup tt;
let G := match goal with |- ?G => constr:(G) end in
xspec G;
let H := fresh "TEMP" in intros H;
......@@ -435,9 +490,13 @@ Tactic Notation "xapp" :=
Tactic Notation "xfail" :=
applys local_erase; unfold Cf_fail.
*)
Open Scope charac.
End MLCFLiftedTactics.
(********************************************************************)
......
......@@ -9,7 +9,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import LibCore MLSep MLCF.
Require Import MLCF MLCFLifted.
Open Scope trm_scope.
Open Scope heap_scope.
Open Scope charac.
......@@ -33,7 +33,7 @@ Definition tl : field := 1.
Fixpoint MList (L:list val) (p:loc) : hprop :=
match L with
| nil => \[p = null]
| x::L' => Hexists (p':loc), (p ~> Record`{ hd := x; tl := val_loc p' }) \* (p' ~> MList L')
| x::L' => Hexists (p':loc), (p ~> record`{ hd := x; tl := val_loc p' }) \* (p' ~> MList L')
end.
Section Properties.
......@@ -73,11 +73,11 @@ Qed.
Lemma MList_cons : forall p x L',
p ~> MList (x::L') =
Hexists p', (p ~> Record`{ hd := x; tl := val_loc p' }) \* p' ~> MList L'.
Hexists p', (p ~> record`{ hd := x; tl := val_loc p' }) \* p' ~> MList L'.
Proof using. intros. xunfold MList at 1. simple~. Qed.
Lemma MList_uncons : forall p p' x L',
(p ~> Record`{ hd := x; tl := val_loc p' }) \* p' ~> MList L' ==>
(p ~> record`{ hd := x; tl := val_loc p' }) \* p' ~> MList L' ==>
p ~> MList (x::L').
Proof using. intros. rewrite MList_cons. hsimpl. Qed.
......@@ -94,7 +94,7 @@ Lemma MList_not_null : forall p L,
p <> null ->
p ~> MList L ==> Hexists x p' L',
\[L = x::L']
\* (p ~> Record`{ hd := x; tl := val_loc p' })
\* (p ~> record`{ hd := x; tl := val_loc p' })
\* p' ~> MList L'.
Proof using.
intros. hchange~ (@MList_not_null_keep p). hpull. intros.
......@@ -114,18 +114,6 @@ Global Opaque MList.
(********************************************************************)
(* * Auxiliary lemmas *)
Parameter rule_get_tl : forall p x p',
triple (trm_app prim_get [val_loc p; val_field tl])
(p ~> Record `{ hd := x; tl := p'})
(fun r => \[r = p'] \* p ~> Record `{ hd := x; tl := p'}).
(* TODO: this specification will be computed on the fly using a tactic *)
Hint Extern 1 (RegisterSpec (app (val_prim prim_get) [_;val_field tl] _ _)) =>
Provide rule_get_tl.
(********************************************************************)
(* * Definition of the list increment program *)
......@@ -151,7 +139,6 @@ Definition mlist_length : val :=
val_int 0
).
(** Helper for simplifying substitutions *)
Parameter mlist_length_closed : forall E,
......@@ -163,6 +150,16 @@ Hint Rewrite mlist_length_closed : rew_subst.
Ltac simpl_subst := simpl; autorewrite with rew_subst.
(** Temporary auxiliary specification *)
Parameter rule_get_tl : forall p x p',
triple (trm_app prim_get [val_loc p; val_field tl])
(p ~> record `{ hd := x; tl := p'})
(fun r => \[r = p'] \* p ~> record `{ hd := x; tl := p'}).
(* TODO: this specification will be computed on the fly using a tactic *)
(********************************************************************)
(* * Mutable list increment verification, using triples *)
......@@ -196,6 +193,19 @@ Qed.
End ProofWithTriples.
(********************************************************************)
(* * Demos of characteristic formulae *)
Module MLCFDemo.
Import MLCFTactics.
Open Scope charac.
Hint Extern 1 (RegisterSpec (app (val_prim prim_get) [_;val_field tl] _ _)) =>
Provide rule_get_tl.
(********************************************************************)
(* * Mutable list increment verification, using characteristic formulae,
without tactics. *)
......@@ -235,7 +245,7 @@ Qed.
(** Remark: in Ltac script below, "=>" is an alias for "intros" *)
Lemma mlist_incr_spec' : forall L p,
Lemma mlist_incr_spec'' : forall L p,
app mlist_length [val_loc p]
(p ~> MList L)
(fun r => \[r = val_int (length L)] \* p ~> MList L).
......@@ -250,14 +260,203 @@ Proof using.
xlet. { xapp IH. { subst~. } }
{ intros r. xpull ;=> Er. xchange (MList_uncons p).
subst r. xapp. subst. rew_length. fequals. math. } }
{ xret. inverts C'. xchange MList_null_keep.
{ xval. inverts C'. xchange MList_null_keep.
hpull ;=> EL. hsimpl. subst~. }
Qed.
End MLCFDemo.
(********************************************************************)
(* * Demos of characteristic formulae *)
Module MLCFLiftedDemo.
Import MLCFLiftedTactics.
Open Scope charac.
(********************************************************************)
(* * Mutable lists *)
(** Layout in memory:
type 'a mlist = { mutable hd : 'a ; mutable tl : 'a mlist }
// empty lists represented using null
*)
(** Record contents *)
Notation "`'{ f1 := x1 }" :=
((f1, Dyn x1)::nil)
(at level 0, f1 at level 0)
: trm_scope.
Notation "`'{ f1 := x1 ; f2 := x2 }" :=
((f1, Dyn x1)::(f2, Dyn x2)::nil)
(at level 0, f1 at level 0, f2 at level 0)
: trm_scope.
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 }" :=
((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0)
: trm_scope.
Notation "`'{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" :=
((f1, Dyn x1)::(f2, Dyn x2)::(f3, Dyn x3)::(f4, Dyn x4)::nil)
(at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0)
: trm_scope.
Open Scope trm_scope.
(*
Definition hd : field := 0.
Definition tl : field := 1.
*)
Fixpoint MList A `{EA:Enc A} (L:list A) (p:loc) : hprop :=
match L with
| nil => \[p = null]
| x::L' => Hexists (p':loc), (p ~> Record`'{ hd := x; tl := p' }) \* (p' ~> MList L')
end.
Section Properties.
Context (A:Type) `{EA:Enc A}.
Implicit Types L : list A.
Implicit Types p : loc.
(** Conversion lemmas for empty lists *)
Lemma MList_nil : forall p,
p ~> MList nil = \[p = null].
Proof using. intros. xunfold~ MList. Qed.
Lemma MList_unnil :
\[] ==> null ~> MList nil.
Proof using. intros. rewrite MList_nil. hsimpl~. Qed.
Lemma MList_null : forall L,
(null ~> MList L) = \[L = nil].
Proof using.
intros. destruct L.
{ xunfold MList. applys himpl_antisym; hsimpl~. }
{ xunfold MList. applys himpl_antisym.
{ hpull ;=> p'. hchange (hprop_Record_not_null null); auto_false.
hpull; auto_false. }
{ hpull. } }
Qed.
Lemma MList_null_keep : forall L,
null ~> MList L ==>
null ~> MList L \* \[L = nil].
Proof using.
intros. destruct L.
{ hsimpl~. }
{ rewrite MList_null. hsimpl. }
Qed.
(** Conversion lemmas for non-empty lists *)
Lemma MList_cons : forall p x L',
p ~> MList (x::L') =
Hexists p', (p ~> Record`'{ hd := x; tl := p' }) \* p' ~> MList L'.
Proof using. intros. xunfold MList at 1. simple~. Qed.
Lemma MList_uncons : forall p p' x L',
(p ~> Record`'{ hd := x; tl := p' }) \* p' ~> MList L' ==>
p ~> MList (x::L').
Proof using. intros. rewrite MList_cons. hsimpl. Qed.
Lemma MList_not_null_keep : forall p L,
p <> null ->
p ~> MList L ==> p ~> MList L \* \[L <> nil].
Proof using.
intros. destruct L.
{ hchanges -> (MList_nil p). }
{ hsimpl. auto_false. }
Qed.
Lemma MList_not_null : forall p L,
p <> null ->
p ~> MList L ==> Hexists x p' L',
\[L = x::L']
\* (p ~> Record`'{ hd := x; tl := p' })
\* p' ~> MList L'.
Proof using.
intros. hchange~ (@MList_not_null_keep p). hpull. intros.
destruct L; tryfalse.
hchange (MList_cons p). hsimpl~.
Qed.
End Properties.
Implicit Arguments MList_null_keep [A [EA]].
Implicit Arguments MList_cons [A [EA]].
Implicit Arguments MList_uncons [A [EA]].
Implicit Arguments MList_not_null [A [EA]].
Implicit Arguments MList_not_null_keep [A [EA]].
Global Opaque MList.
(********************************************************************)
(* TODO: prove spec of primitives *)
Parameter Rule_add : forall (n1 n2:int),
App' prim_add n1 n2;
\[]
(fun (r:int) => \[r = (n1 + n2)]).
Parameter Rule_neq : forall (v1 v2:loc),
App' prim_neq v1 v2;
\[]
(fun (r:int) => \[r = (If v1 = v2 then 0 else 1)]).
Parameter Rule_get_tl : forall p A `{EA:Enc A} (x:A) (p':loc),
App' prim_get (p:loc) (tl:field);
(p ~> Record `'{ hd := x; tl := p'})
(fun (r:loc) => \[r = p'] \* p ~> Record `'{ hd := x; tl := p'}).
Hint Extern 1 (RegisterSpec (App' (val_prim prim_get) _ tl; _ _)) =>
Provide Rule_get_tl.
Hint Extern 1 (RegisterSpec (App' (val_prim prim_neq) _ _; _ _)) =>
Provide Rule_neq.
Hint Extern 1 (RegisterSpec (App' (val_prim prim_add) _ _; _ _)) =>
Provide Rule_add.
(********************************************************************)
(* * Mutable list increment verification, using lifted characteristic formulae *)
Lemma mlist_incr_spec : forall A `{EA:Enc A} (L:list A) (p:loc),
App' mlist_length p;
(p ~> MList L)
(fun (r:int) => \[r = length L] \* p ~> MList L).
Proof using.
intros. gen p. induction_wf: list_sub_wf L; intros. xcf.
xlet. { xapp. }
intros X. xpull ;=> EX.
subst X. xif ;=> C; case_if as C'; clear C.
{ xchange (MList_not_null p). { auto. } xpull ;=> x p' L' EL.
xlet. { xapp. }
intros p''. xpull ;=> E. subst p''.
xlet. { xapp IH. { subst~. } }
{ intros r. xpull ;=> Er. xchange (MList_uncons p).
subst r. xapp. subst. rew_length. fequals. math. } }
{ xval. xchanges MList_null_keep ;=> EL. hsimpl. subst~. }
Qed.
End MLCFLiftedDemo.
......
......@@ -243,21 +243,21 @@ Ltac hcancel_hook H ::=
Definition record_descr := list (field * val).
Fixpoint Record (L:record_descr) (r:loc) : hprop :=
Fixpoint record (L:record_descr) (r:loc) : hprop :=
match L with
| nil => \[]
| (f, v)::L' => (r `.` f ~> v) \* (r ~> Record L')
| (f, v)::L' => (r `.` f ~> v) \* (r ~> record L')
end.
Lemma hprop_record_not_null : forall (r:loc) (L:record_descr),
L <> nil ->
(r ~> Record L) ==> (r ~> Record L) \* \[r <> null].
(r ~> record L) ==> (r ~> record L) \* \[r <> null].
Proof using.
intros. destruct L as [|(f,v) L']; tryfalse.
xunfold Record. hchange (hprop_single_not_null r). hsimpl~.
xunfold record. hchange (hprop_single_not_null r). hsimpl~.
Qed.
Global Opaque Record.
Global Opaque record.
(********************************************************************)
......@@ -479,7 +479,7 @@ Parameter rule_neq : forall v1 v2,
Parameter rule_new_record : forall (L:record_descr),
triple (trm_new_record L)
\[]
(fun r => Hexists l, \[r = val_loc l] \* l ~> Record L).
(fun r => Hexists l, \[r = val_loc l] \* l ~> record L).
Parameter rule_get : forall l f v,
triple (prim_get [val_loc l])
......@@ -643,10 +643,11 @@ Proof using.
rewrite (hprop_star_comm_assoc \GC H'). hsimpl. }
Qed.
(** Make [xlocal] aware that triples are local *)
(** Make [xlocal] aware that triples are local
Ltac xlocal_core tt ::=
try first [ assumption | applys is_local_triple ].
*)