Commit dedd8782 authored by charguer's avatar charguer

CF lift

parent 055eaac0
......@@ -210,4 +210,230 @@ DEPRECATED
Qed.
*)
\ No newline at end of file
*)
============
(*
{ forwards N: rule_new v. applys rule_consequence_frame H N.
{ rewrite~ hprop_star_empty_l. }
{ intros r. applys P r. } }
{ destruct P as (H'&l&w&R1&R2&R3). forwards N: rule_get w l.
rewrite R1. applys~ rule_consequence_frame H' N. }
{ destruct P as (H'&l&w&R1&R2&R3). forwards N: rule_set l w v0.
rewrite R1. applys~ rule_consequence_frame H' N. }
*)
(*
| Trm_new v => local (cf_new v)
| Trm_get r => local (cf_get r)
| Trm_set r w => local (cf_set r w)
*)
(*
Definition cf_new v : formula := fun H Q =>
(fun r => Hexists l, \[r = val_loc l] \* l ~~> v) \*+ H ===> Q.
Definition cf_get vl : formula := fun H Q =>
exists H' l v,
vl = val_loc l
/\ H ==> (l ~~> v) \* H'
/\ (fun x => \[x = v] \* l ~~> v) \*+ H' ===> Q.
Definition cf_set vl w : formula := fun H Q =>
exists H' l v,
vl = val_loc l
/\ H ==> (l ~~> v) \* H'
/\ (fun x => \[x = val_unit] \* l ~~> w) \*+ H' ===> Q.
*)
(*
Definition cf_new (v:val) : formula.
refine (fun H `{EA:Enc A} (Q:A->hprop) =>
exists (E : loc = A :> Type) (A1:Type) (EA1:Enc A1) (V:A1), v = enc V :> val /\ _).
Proof using.
subst A. refine ((fun (l:loc) => l ~~~> V) \*+ H ===> Q).
Defined.
Print cf_new.
*)
(*GOOD
Inductive cf_new (v:val) : formula :=
| cf_new_intro : forall H (Q:loc->hprop) `{EA1:Enc A1} (V:A1),
v = enc V ->
((fun l : loc => l ~~~> V) \*+ H ===> Q) ->
cf_new v H Enc_loc Q.
*)
(*
Definition cf_new v : formula := fun H `{EA:Enc A} (Q:A->hprop) =>
exists (E : A = loc)
(A1:Type) (EA1:Enc A1) (V:A1), v = enc V /\
Logic.eq_rect_r (fun A' => Enc A' -> (A' -> hprop) -> Prop)
(fun EA' Q' => EA' = Enc_loc /\ (fun l : loc => l ~~~> V) \*+ H ===> Q')
E EA Q.
*)
(*
Definition cf_new v : formula := fun H `{EA:Enc A} (Q:A->hprop) =>
exists (E : loc = A :> Type)
(A1:Type) (EA1:Enc A1) (V:A1), v = enc V /\
Logic.eq_rect loc (fun A' : Type => Enc A' -> (A' -> hprop) -> Prop)
(fun (EA' : Enc loc) (Q0 : loc -> hprop) =>
(fun l : loc => l ~~~> V) \*+ H ===> Q0) A E EA Q.
*)
(*
Definition cf_new v : formula := fun H `{EA1:Enc A1} (Q:A1->hprop) =>
exists (A1:Type) (EA1:Enc A1) (V:A1), v = enc V /\
(fun (l:loc) => l ~~~> V) \*+ H ===> Q.
Definition cf_get vl : formula := fun H `{Enc A} (Q:A->hprop) =>
exists H' l v,
vl = val_loc l
/\ H ==> (l ~~~> V) \* H'
/\ (fun x => \[x = v] \* l ~~> v) \*+ H' ===> Q.
Definition cf_set vl w : formula := fun H `{Enc A} (Q:A->hprop) =>
exists H' l v,
vl = val_loc l
/\ H ==> (l ~~> v) \* H'
/\ (fun x => \[x = val_unit] \* l ~~> w) \*+ H' ===> Q.
*)
(*
| Trm_new v => local (cf_new v)
*)
(*
| Trm_new v => local (fun _ _ _ _ => False)
*)
(*
| Trm_get r => local (fun _ _ _ _ => False)
| Trm_set r w => local (fun _ _ _ _ => False)
*)
(**
| Trm_get r => local (Cf_get r)
| Trm_set r w => local (Cf_set r w)
*)
(* GOOD
Focus 5.
inverts P as R _ _. (* TODO: inverts should remove refl proofs *)
forwards~ N: Rule_new V.
applys rule_consequence_frame H N.
{ rewrite~ hprop_star_empty_l. }
{ intros r. unfold PostEnc. rewrite extrude.
applys himpl_extract_exists. intros l.
specializes R l. rewrite hprop_star_assoc.
applys himpl_extract_prop. intro_subst.
applys himpl_trans (rm R).
applys himpl_inst_exists l.
applys~ himpl_inst_prop. }
*)
(* GOOD'
{ destruct P as (HA&A1&EA1&V&EV&HV). subst A.
(* rewrite eq_rect_eq in HV. *)
asserts (EAQ&R): (EA = Enc_loc /\ (fun x : loc => x ~~~> V \* H) ===> Q). { auto. }
clear HV. subst. (* TODO: simpl eq_rect *)
forwards~ N: Rule_new V.
applys rule_consequence_frame H N.
{ rewrite~ hprop_star_empty_l. }
{ intros r. unfold PostEnc. rewrite extrude.
applys himpl_extract_exists. intros l.
specializes R l. rewrite hprop_star_assoc.
applys himpl_extract_prop. intro_subst.
applys himpl_trans (rm R).
applys himpl_inst_exists l.
applys~ himpl_inst_prop. } }
*)
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* EXTRA *)
(*
(*------------------------------------------------------------------*)
(* ** Alternative definitions for operations on references *)
Definition hprop_single_val (vl:val) (v:val) : hprop :=
Hexists l, \[vl = val_loc l] \* (l ~~> v).
Definition hprop_single_val' (vl:val) (v:val) : hprop :=
fun h => exists l, vl = val_loc l /\ h = state_single l v.
Notation "vr '~~~>' v" := (hprop_single_val vr v)
(at level 32, no associativity) : heap_scope.
Definition cf_new' v : formula := fun H Q =>
(fun r => r ~~~> v) \*+ H ===> Q.
Definition cf_get' r : formula := fun H Q =>
exists H' v,
H ==> (r ~~~> v) \* H'
/\ (fun x => \[x = v] \* r ~~~> v) \*+ H' ===> Q.
Definition cf_set' r w : formula := fun H Q =>
exists H' v,
H ==> (r ~~~> v) \* H'
/\ (fun x => \[x = val_unit] \* r ~~~> w) \*+ H' ===> Q.
*)
(*
Instance Enc (A*B) => val_pair (enc A) (enc B)
App f x y H Q = app f (x,y) H Q
App f x y z H Q = app f (x,y,z) H Q
if computed, then:
enc (x,y)
vs
val_pair (enc x, enc y)
let f x y = t
let f (x,y) = t
let f v = let x = fst v in let y = snd v in t with x<>y and v\notin t.
f (a,b) --> [y->b][x->a]t.
CF_fix:
(forall `{EA2:Enc A2} (X:A2) H' Q', '(F1of F X) H' Q' -> app F X H' Q') ->
in proofs, do intros (x,y,z) if X is a tuple of arity 3.
for reasoning about the function, need to provide
the type of arguments and return type as well.
xfun (A*B*C->D). (* those types should have encoders *)
xfun (x:A) (y:B) (z:C) : D. => give the prototype.
xcf for local functions: split the
*)
......@@ -346,31 +346,13 @@ Definition cf_app f v : formula := fun H Q =>
app f v H Q.
Definition cf_fix (F1of : val -> val -> formula) (F2of : val -> formula) : formula := fun H Q =>
forall (F:val),
(forall X H' Q', (F1of F X) H' Q' -> app F X H' Q') ->
(F2of F) H Q.
(* ABOVE:
(forall X, (F1of F X) ===> app F X)
*)
forall (F:val), (forall X, (F1of F X) ===> app F X) -> (F2of F) H Q.
(*
Definition cf_new v : formula := fun H Q =>
(fun r => Hexists l, \[r = val_loc l] \* l ~~> v) \*+ H ===> Q.
Definition cf_get vl : formula := fun H Q =>
exists H' l v,
vl = val_loc l
/\ H ==> (l ~~> v) \* H'
/\ (fun x => \[x = v] \* l ~~> v) \*+ H' ===> Q.
Definition cf_set vl w : formula := fun H Q =>
exists H' l v,
vl = val_loc l
/\ H ==> (l ~~> v) \* H'
/\ (fun x => \[x = val_unit] \* l ~~> w) \*+ H' ===> Q.
*)
(* Same as:
forall (F:val),
(forall X H' Q', (F1of F X) H' Q' -> app F X H' Q') ->
(F2of F) H Q.
*)
(*------------------------------------------------------------------*)
......@@ -406,11 +388,6 @@ Definition cf_def cf (t:Trm) :=
(fun F X => cf (subst_Trm f F (subst_Trm x X t1)))
(fun F => cf (subst_Trm f F t2)))
| Trm_app f v => local (cf_app f v)
(*
| Trm_new v => local (cf_new v)
| Trm_get r => local (cf_get r)
| Trm_set r w => local (cf_set r w)
*)
end.
Definition cf := FixFun cf_def.
......@@ -515,15 +492,6 @@ Proof using.
{ hnf. rewrite Trm_size_subst_Trm_value.
rewrite~ Trm_size_subst_Trm_value. } } }
{ applys P. }
(*
{ forwards N: rule_new v. applys rule_consequence_frame H N.
{ rewrite~ hprop_star_empty_l. }
{ intros r. applys P r. } }
{ destruct P as (H'&l&w&R1&R2&R3). forwards N: rule_get w l.
rewrite R1. applys~ rule_consequence_frame H' N. }
{ destruct P as (H'&l&w&R1&R2&R3). forwards N: rule_set l w v0.
rewrite R1. applys~ rule_consequence_frame H' N. }
*)
Qed.
......@@ -536,7 +504,21 @@ Proof using. intros. applys* cf_sound. Qed.
(********************************************************************)
(* ** Completeness proof *)
(*
Lemma cf_name : forall (c:com) (H Q : Assertion),
(forall st, H st -> cf c (= st) Q) -> cf c H Q.
Proof. intros. apply cf_local. apply~ local_name. Qed.
*)
(********************************************************************)
......@@ -621,59 +603,21 @@ Definition cf_fix (F1of : func -> forall `{EA1:Enc A1}, A1 -> formula) (F2of : f
'(F2of F) H Q.
(*
Definition cf_new (v:val) : formula.
refine (fun H `{EA:Enc A} (Q:A->hprop) =>
exists (E : loc = A :> Type) (A1:Type) (EA1:Enc A1) (V:A1), v = enc V :> val /\ _).
Proof using.
subst A. refine ((fun (l:loc) => l ~~~> V) \*+ H ===> Q).
Defined.
Print cf_new.
*)
(*------------------------------------------------------------------*)
(* ** Instance of [app] for primitive operations *)
(*GOOD
Inductive cf_new (v:val) : formula :=
| cf_new_intro : forall H (Q:loc->hprop) `{EA1:Enc A1} (V:A1),
v = enc V ->
((fun l : loc => l ~~~> V) \*+ H ===> Q) ->
cf_new v H Enc_loc Q.
*)
Lemma app_new : forall A `{EA:Enc A} (V:A),
app prim_new V \[] (fun (l:loc) => l ~~~> V).
Proof using. intros. applys~ Rule_new. Qed.
(*
Definition cf_new v : formula := fun H `{EA:Enc A} (Q:A->hprop) =>
exists (E : A = loc)
(A1:Type) (EA1:Enc A1) (V:A1), v = enc V /\
Logic.eq_rect_r (fun A' => Enc A' -> (A' -> hprop) -> Prop)
(fun EA' Q' => EA' = Enc_loc /\ (fun l : loc => l ~~~> V) \*+ H ===> Q')
E EA Q.
*)
Lemma app_get : forall A `{EA:Enc A} (V:A) l,
app prim_get (val_loc l) (l ~~~> V) (fun (x:A) => \[x = V] \* (l ~~~> V)).
Proof using. intros. applys~ Rule_get. Qed.
(*
Definition cf_new v : formula := fun H `{EA:Enc A} (Q:A->hprop) =>
exists (E : loc = A :> Type)
(A1:Type) (EA1:Enc A1) (V:A1), v = enc V /\
Logic.eq_rect loc (fun A' : Type => Enc A' -> (A' -> hprop) -> Prop)
(fun (EA' : Enc loc) (Q0 : loc -> hprop) =>
(fun l : loc => l ~~~> V) \*+ H ===> Q0) A E EA Q.
*)
(*
Definition cf_new v : formula := fun H `{EA1:Enc A1} (Q:A1->hprop) =>
exists (A1:Type) (EA1:Enc A1) (V:A1), v = enc V /\
(fun (l:loc) => l ~~~> V) \*+ H ===> Q.
Definition cf_get vl : formula := fun H `{Enc A} (Q:A->hprop) =>
exists H' l v,
vl = val_loc l
/\ H ==> (l ~~~> V) \* H'
/\ (fun x => \[x = v] \* l ~~> v) \*+ H' ===> Q.
Definition cf_set vl w : formula := fun H `{Enc A} (Q:A->hprop) =>
exists H' l v,
vl = val_loc l
/\ H ==> (l ~~> v) \* H'
/\ (fun x => \[x = val_unit] \* l ~~> w) \*+ H' ===> Q.
Lemma app_set : forall A1 A2 `{EA1:Enc A1} `{EA2:Enc A2} l (V:A1) (W:A2),
app prim_set (val_pair (val_loc l) (enc W)) (l ~~~> V) (fun (_:unit) => l ~~~> W).
Proof using. intros. applys~ Rule_set. Qed.
*)
(*------------------------------------------------------------------*)
(* ** Definition of the CF generator *)
......@@ -692,20 +636,6 @@ Definition cf_def cf (t:Trm) :=
(fun F `{EA:Enc A} (X:A) => cf (subst_Trm f F (Subst_Trm x X t1)))
(fun F => cf (subst_Trm f F t2)))
| Trm_app f v => local (cf_app f v)
(*
| Trm_new v => local (cf_new v)
*)
(*
| Trm_new v => local (fun _ _ _ _ => False)
*)
(*
| Trm_get r => local (fun _ _ _ _ => False)
| Trm_set r w => local (fun _ _ _ _ => False)
*)
(**
| Trm_get r => local (Cf_get r)
| Trm_set r w => local (Cf_set r w)
*)
end.
Definition cf := FixFun cf_def.
......@@ -733,30 +663,30 @@ Qed.
(********************************************************************)
(* ** Soundness proof *)
(* TO BE COMPLETED *)
(*------------------------------------------------------------------*)
(* ** Soundness predicate *)
Definition sound_for (t:trm) (F:formula) :=
forall H `{EA:Enc A} (Q:A->hprop), 'F H Q -> Triple t H Q.
(*------------------------------------------------------------------*)
(* ** Soundness of local *)
Lemma local_sound : forall t (F:formula),
sound_for t F ->
sound_for t (local F).
Admitted.
(*------------------------------------------------------------------*)
(* ** Soundness predicate *)
Axiom extrude : forall (A:Type) (J:A->hprop) H,
(Hexists x, J x) \* H = Hexists x, (J x \* H).
Print Logic.eq_rect_r.
Search eq_rect.
Lemma cf_sound : forall (t:Trm),
sound_for t (cf t).
......@@ -765,37 +695,7 @@ Proof using.
rewrite cf_unfold. destruct t; simpl;
applys local_sound; intros H A EA Q P.
{ destruct P as (V&EV&HV). applys~ Rule_val V. }
(* GOOD
Focus 5.
inverts P as R _ _. (* TODO: inverts should remove refl proofs *)
forwards~ N: Rule_new V.
applys rule_consequence_frame H N.
{ rewrite~ hprop_star_empty_l. }
{ intros r. unfold PostEnc. rewrite extrude.
applys himpl_extract_exists. intros l.
specializes R l. rewrite hprop_star_assoc.
applys himpl_extract_prop. intro_subst.
applys himpl_trans (rm R).
applys himpl_inst_exists l.
applys~ himpl_inst_prop. }
*)
(* GOOD'
{ destruct P as (HA&A1&EA1&V&EV&HV). subst A.
(* rewrite eq_rect_eq in HV. *)
asserts (EAQ&R): (EA = Enc_loc /\ (fun x : loc => x ~~~> V \* H) ===> Q). { auto. }
clear HV. subst. (* TODO: simpl eq_rect *)
forwards~ N: Rule_new V.
applys rule_consequence_frame H N.
{ rewrite~ hprop_star_empty_l. }
{ intros r. unfold PostEnc. rewrite extrude.
applys himpl_extract_exists. intros l.
specializes R l. rewrite hprop_star_assoc.
applys himpl_extract_prop. intro_subst.
applys himpl_trans (rm R).
applys himpl_inst_exists l.
applys~ himpl_inst_prop. } }
*)
Abort.
(*
....
......@@ -834,76 +734,3 @@ End CFWithLifting.
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* EXTRA *)
(*
(*------------------------------------------------------------------*)
(* ** Alternative definitions for operations on references *)
Definition hprop_single_val (vl:val) (v:val) : hprop :=
Hexists l, \[vl = val_loc l] \* (l ~~> v).
Definition hprop_single_val' (vl:val) (v:val) : hprop :=
fun h => exists l, vl = val_loc l /\ h = state_single l v.
Notation "vr '~~~>' v" := (hprop_single_val vr v)
(at level 32, no associativity) : heap_scope.
Definition cf_new' v : formula := fun H Q =>
(fun r => r ~~~> v) \*+ H ===> Q.
Definition cf_get' r : formula := fun H Q =>
exists H' v,
H ==> (r ~~~> v) \* H'
/\ (fun x => \[x = v] \* r ~~~> v) \*+ H' ===> Q.
Definition cf_set' r w : formula := fun H Q =>
exists H' v,
H ==> (r ~~~> v) \* H'
/\ (fun x => \[x = val_unit] \* r ~~~> w) \*+ H' ===> Q.
*)
(*
Instance Enc (A*B) => val_pair (enc A) (enc B)
App f x y H Q = app f (x,y) H Q
App f x y z H Q = app f (x,y,z) H Q
if computed, then:
enc (x,y)
vs
val_pair (enc x, enc y)
let f x y = t
let f (x,y) = t
let f v = let x = fst v in let y = snd v in t with x<>y and v\notin t.
f (a,b) --> [y->b][x->a]t.
CF_fix:
(forall `{EA2:Enc A2} (X:A2) H' Q', '(F1of F X) H' Q' -> app F X H' Q') ->
in proofs, do intros (x,y,z) if X is a tuple of arity 3.
for reasoning about the function, need to provide
the type of arguments and return type as well.
xfun (A*B*C->D). (* those types should have encoders *)
xfun (x:A) (y:B) (z:C) : D. => give the prototype.
xcf for local functions: split the
*)
......@@ -728,7 +728,7 @@ Definition PostEnc `{Enc A} (Q:A->hprop) : val->hprop :=
Definition Triple (t:trm) (H:hprop) `{EA:Enc A} (Q:A->hprop) :=
triple t H (PostEnc Q).
Lemma Rule_val : forall `{EA:Enc A} (V:A) v H (Q:A->hprop),
Lemma Rule_val : forall A `{EA:Enc A} (V:A) v H (Q:A->hprop),
v = enc V ->
H ==> Q V ->
Triple (trm_val v) H Q.
......@@ -739,7 +739,7 @@ Proof using.
applys~ himpl_inst_prop.
Qed.
Lemma Rule_if : forall (V:int) v t1 t2 H `{EA:Enc A} (Q:A->hprop),
Lemma Rule_if : forall (V:int) v t1 t2 H A `{EA:Enc A} (Q:A->hprop),
v = enc V ->
Triple (If V = 0 then t2 else t1) H Q ->
Triple (trm_if v t1 t2) H Q.
......@@ -749,7 +749,7 @@ Proof using.
Qed.
Lemma Rule_let : forall x t1 t2 H,
forall `{EA:Enc A} (Q:A->hprop) `{EA1:Enc A1} (Q1:A1->hprop),
forall A `{EA:Enc A} (Q:A->hprop) A1 `{EA1:Enc A1} (Q1:A1->hprop),
Triple t1 H Q1 ->
(forall (X:A1), Triple (Subst_trm x X t2) (Q1 X) Q) ->
Triple (trm_let x t1 t2) H Q.
......@@ -763,7 +763,7 @@ Proof using.
Qed.
Lemma Rule_let_val_enc : forall `{Enc A1} (V1:A1) x v1 t2 H A `{EA: Enc A} (Q:A->hprop),
Lemma Rule_let_val_enc : forall A1 `{Enc A1} (V1:A1) x v1 t2 H A `{EA: Enc A} (Q:A->hprop),
v1 = enc V1 ->
(forall X, X = V1 -> Triple (Subst_trm x X t2) H Q) ->
Triple (trm_let x (trm_val v1) t2) H Q.
......@@ -815,14 +815,14 @@ Notation "r '~~~>' V" := (hprop_single_enc r V)
Instance Enc_loc : Enc loc.
Proof using. constructor. applys val_loc. Defined.
Lemma Rule_new : forall `{EA:Enc A} (V:A) v,
Lemma Rule_new : forall A `{EA:Enc A} (V:A) v,
v = enc V ->
Triple (prim_new v) \[] (fun l => l ~~~> V).
Proof using.
introv E. applys_eq rule_new 1. subst~.
Qed.
Lemma Rule_get : forall `{EA:Enc A} (V:A) l,
Lemma Rule_get : forall A `{EA:Enc A} (V:A) l,
Triple (prim_get (val_loc l)) (l ~~~> V) (fun x => \[x = V] \* (l ~~~> V)).
Proof using.
introv. applys rule_consequence. { auto. } { applys rule_get. }
......@@ -837,7 +837,7 @@ Qed.
Instance Enc_unit : Enc unit.
Proof using. constructor. applys (fun x:unit => val_unit). Defined.
Lemma Rule_set : forall `{EA1:Enc A1} (V1:A1) `{EA2:Enc A2} (V2:A2) l v2,
Lemma Rule_set : forall A1 A2 `{EA1:Enc A1} (V1:A1) `{EA2:Enc A2} (V2:A2) l v2,