Commit a8dedefc authored by charguer's avatar charguer

alloc

parent 658f5d63
(* TODO: why jauto does clearbody? *)
=============
-- lib/stdlib should have make quick target
......
......@@ -20,40 +20,6 @@ Tactic Notation "cases" constr(E) := (* TODO For TLC *)
let H := fresh "Eq" in cases E as H.
(* ********************************************************************** *)
(** * Fresh locations *)
(* ---------------------------------------------------------------------- *)
(** ** Existence of fresh locations *)
(** These lemmas are useful to prove:
[forall h v, exists l, fmap_disjoint (fmap_single l v) h]. *)
Definition loc_fresh_gen (L : list nat) :=
(1 + fold_right plus O L)%nat.
Lemma loc_fresh_ind : forall x L,
Mem x L ->
(x < loc_fresh_gen L)%nat.
Proof using.
intros x L. unfold loc_fresh_gen.
induction L; introv M; inverts M; rew_list.
{ math. }
{ forwards~: IHL. math. }
Qed.
Definition loc_fresh_exists (A:Type) :=
forall (L:list A), exists (x:A), ~ Mem x L.
Lemma loc_fresh_nat : loc_fresh_exists nat.
Proof using.
intros L. exists (loc_fresh_gen L). intros M.
lets: loc_fresh_ind M. math.
Qed.
Hint Resolve loc_fresh_nat.
(* ********************************************************************** *)
(** * Maps (partial functions) *)
......@@ -288,7 +254,14 @@ Proof using.
apply fmap_disjoint_union_eq_r.
Qed.
Lemma fmap_single_same_loc_disjoint : forall (x:A) (v1 v2:B),
Lemma fmap_disjoint_single_single : forall (x1 x2:A) (v1 v2:B),
x1 <> x2 ->
\# (fmap_single x1 v1) (fmap_single x2 v2).
Proof using.
introv N. intros x. simpls. do 2 case_if; auto.
Qed.
Lemma fmap_single_single_same_inv : forall (x:A) (v1 v2:B),
\# (fmap_single x v1) (fmap_single x v2) ->
False.
Proof using.
......@@ -299,20 +272,6 @@ Lemma fmap_disjoint_3_unfold : forall h1 h2 h3,
\# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3).
Proof using. auto. Qed.
Lemma fmap_disjoint_new : forall null h v,
loc_fresh_exists A ->
exists l, \# (fmap_single l v) h /\ l <> null.
Proof using.
intros null (m&(L&M)) v HF.
unfold fmap_disjoint, map_disjoint. simpl.
lets (l&F): (HF (null::L)).
exists l. split.
{ intros l'. case_if~.
{ right. applys not_not_elim. intros H. applys F.
constructor. applys~ M. } }
{ intro_subst. applys~ F. }
Qed.
Lemma fmap_disjoint_single_set : forall h l v1 v2,
\# (fmap_single l v1) h ->
\# (fmap_single l v2) h.
......@@ -795,3 +754,117 @@ Tactic Notation "fmap_red" "~" :=
Tactic Notation "fmap_red" "*" :=
fmap_red; auto_star.
(* ********************************************************************** *)
(** * Consecutive locations and fresh locations *)
(* ---------------------------------------------------------------------- *)
(** ** Existence of fresh locations *)
Fixpoint nat_fold A (f:nat->A->A) (k:nat) (z:A) : A :=
match k with
| O => z
| S k' => f k' (nat_fold f k' z)
end.
Definition fmap_conseq B (l:nat) (k:nat) (v:B) : fmap nat B :=
nat_fold (fun i m => (fmap_single (l+i)%nat v) \+ m) k fmap_empty.
Lemma fmap_conseq_zero : forall B (l:nat) (v:B),
fmap_conseq l O v = fmap_empty.
Proof using. auto. Qed.
Lemma fmap_conseq_succ : forall B (l:nat) (k:nat) (v:B),
fmap_conseq l (S k) v = (fmap_single (l+k)%nat v) \+ (fmap_conseq l k v).
Proof using. auto. Qed.
Opaque fmap_conseq.
(* ---------------------------------------------------------------------- *)
(** ** Existence of fresh locations *)
(** These lemmas are useful to prove:
[forall h v, exists l, fmap_disjoint (fmap_single l v) h]. *)
Definition loc_fresh_gen (L : list nat) :=
(1 + fold_right plus O L)%nat.
Lemma loc_fresh_ind : forall l L,
Mem l L ->
(l < loc_fresh_gen L)%nat.
Proof using.
intros l L. unfold loc_fresh_gen.
induction L; introv M; inverts M; rew_list.
{ math. }
{ forwards~: IHL. math. }
Qed.
Lemma loc_fresh_nat_ge : forall (L:list nat),
exists (l:nat), forall (i:nat), ~ Mem (l+i)%nat L.
Proof using.
intros L. exists (loc_fresh_gen L). intros i M.
lets: loc_fresh_ind M. math.
Qed.
Lemma loc_fresh_nat : forall (L:list nat),
exists (l:nat), ~ Mem l L.
Proof using.
intros L. forwards (l&P): loc_fresh_nat_ge L.
exists l. intros M. applys (P 0%nat). applys_eq M 2. math.
Qed.
(* ---------------------------------------------------------------------- *)
(** ** Extension of a finite map with at fresh locations *)
Section FmapFresh.
Variables (B : Type).
Implicit Types h : fmap nat B.
Lemma fmap_single_fresh : forall null h v,
exists l, \# (fmap_single l v) h /\ l <> null.
Proof using.
intros null (m&(L&M)) v.
unfold fmap_disjoint, map_disjoint. simpl.
lets (l&F): (loc_fresh_nat (null::L)).
exists l. split.
{ intros l'. case_if~.
{ right. applys not_not_elim. intros H. applys F.
constructor. applys~ M. } }
{ intro_subst. applys~ F. }
Qed.
Lemma fmap_conseq_fresh : forall null h k v,
exists l, \# (fmap_conseq l k v) h /\ l <> null.
Proof using.
intros null (m&(L&M)) k v.
unfold fmap_disjoint, map_disjoint. simpl.
lets (l&F): (loc_fresh_nat_ge (null::L)).
exists l. split.
{ intros l'. induction k. { simple~. }
{ rewrite fmap_conseq_succ. destruct IHk as [E|?].
{ simpl. unfold map_union. case_if~.
{ right. applys not_not_elim. intros H. applys F k.
constructor. applys~ M. } }
{ auto. } } }
{ intro_subst. applys~ F 0%nat. rew_nat. auto. }
Qed.
Lemma fmap_disjoint_single_conseq : forall B l l' k (v:B),
(l' >= l + k)%nat ->
\# (fmap_single l' v) (fmap_conseq l k v).
Proof using.
intros. induction k.
{ rewrite~ fmap_conseq_zero. }
{ rewrite fmap_conseq_succ. rew_disjoint. split.
{ applys fmap_disjoint_single_single. math. }
{ applys IHk. math. } }
Qed.
End FmapFresh.
......@@ -134,15 +134,6 @@ Definition nat_fold A (f:A->nat->A) (i:A) (n:nat) : A :=
Definition fields := list field.
*)
(** l `.` f ~> v *)
Definition hfield (l:loc) (f:field) (v:val) : hprop :=
(l+f)%nat ~~> v.
(* Notation for parsing *)
Notation "l `.` f '~~>' v" := (hfield l f v)
(at level 32, f at level 0, no associativity,
format "l `.` f '~~>' v") : heap_scope.
(*
Definition star_fields_values l fvs :=
......@@ -183,15 +174,7 @@ Global Opaque field var loc.
Definition val_neq :=
Fun M N := If_ prim_eq M N Then 0 Else 1.
Lemma rule_eq : forall v1 v2,
triple (prim_eq v1 v2)
\[]
(fun r => \[r = val_int (If v1 = v2 then 1 else 0)]).
Proof using.
introv Hh. exists___. splits.
{ applys* red_eq. }
{ hhsimpl. case_if*. }
Qed.
Lemma rule_neq : forall v1 v2,
triple (val_neq v1 v2)
......@@ -217,27 +200,6 @@ Definition val_set_field (f:field) :=
prim_set Q V.
Implicit Types n : int.
Lemma rule_add_int : forall n1 n2,
triple (prim_add n1 n2)
\[]
(fun r => \[r = val_int (n1 + n2)]).
Proof using.
introv Hh. exists___. splits.
{ applys* red_add_int. }
{ hhsimpl*. }
Qed.
Lemma rule_add_loc : forall l f,
triple (prim_add l (my_Z_of_nat f))
\[]
(fun r => \[r = val_loc (l+f)%nat]).
Proof using.
introv Hh. exists___. splits.
{ applys* red_add_loc. }
{ hhsimpl*. }
Qed.
(** Make [xlocal] aware that triples are local *)
......
......@@ -77,6 +77,14 @@ Fixpoint subst (y:var) (w:val) (t:trm) : trm :=
end.
(* ---------------------------------------------------------------------- *)
(** Inhabited types *)
Global Instance Inhab_val : Inhab val.
Proof using. apply (prove_Inhab val_unit). Qed.
(* ---------------------------------------------------------------------- *)
(** Coercions *)
......@@ -146,6 +154,19 @@ Notation "'ValFun' x1 ':=' t" :=
(* ********************************************************************** *)
(* * Source language semantics *)
(* ---------------------------------------------------------------------- *)
(** State produced by [alloc] *)
Fixpoint nat_fold A (f:nat->A->A) (k:nat) (z:A) : A :=
match k with
| O => z
| S k' => f k' (nat_fold f k' z)
end.
Definition alloc_state (l:loc) (k:nat) :=
nat_fold (fun i m => (fmap_single (l+i)%nat val_unit) \+ m) k fmap_empty.
(* ---------------------------------------------------------------------- *)
(** Big-step evaluation *)
......@@ -157,7 +178,7 @@ Local Open Scope fmap_scope.
Implicit Types t : trm.
Implicit Types v : val.
Implicit Types f : field.
Implicit Types i : field.
Inductive red : state -> trm -> state -> val -> Prop :=
| red_val : forall m v,
......@@ -188,8 +209,8 @@ Inductive red : state -> trm -> state -> val -> Prop :=
red m3 t4 m4 r ->
red m1 (trm_app t1 t2) m4 r
| red_ref : forall ma mb v l,
l <> null ->
mb = (fmap_single l v) ->
l <> null ->
\# ma mb ->
red ma (prim_ref v) (mb \+ ma) (val_loc l)
| red_get : forall m l v,
......@@ -198,18 +219,18 @@ Inductive red : state -> trm -> state -> val -> Prop :=
| red_set : forall m m' l v,
m' = fmap_update m l v ->
red m (prim_set (val_loc l) v) m' val_unit
(*| red_alloc : forall n ma mb l vs,
| red_alloc : forall k n ma mb l,
mb = fmap_conseq l k val_unit ->
n = my_Z_of_nat k ->
l <> null ->
mb = fold_right (fun m v => fmap_union m (fmap_single (l+k)%nat v)) fmap_empty vs ->
\# ma mb ->
length vs = n ->
red ma (prim_alloc (val_int n)) (mb \+ ma) (val_loc l).*)
red ma (prim_alloc (val_int n)) (mb \+ ma) (val_loc l)
| red_add_int : forall m n1 n2 n',
n' = n1 + n2 ->
red m (prim_add (val_int n1) (val_int n2)) m (val_int n')
| red_add_loc : forall m l n f,
n = f ->
red m (prim_add (val_loc l) (val_int n)) m (val_loc (l+f)%nat)
| red_add_loc : forall m l n i,
n = i ->
red m (prim_add (val_loc l) (val_int n)) m (val_loc (l+i)%nat)
| red_eq : forall m v1 v2 n,
n = (If v1 = v2 then 1 else 0) ->
red m (prim_eq v1 v2) m (val_int n).
......
......@@ -228,11 +228,21 @@ Lemma hstar_single_same_loc_disjoint : forall (l:loc) (v1 v2:val),
(l ~~> v1) \* (l ~~> v2) ==> \[False].
Proof using.
intros. unfold hsingle. intros h (h1&h2&E1&E2&D&E). false.
subst. applys* fmap_single_same_loc_disjoint.
subst. applys* fmap_disjoint_single_single_same_inv.
Qed.
Global Opaque hsingle.
(** l `.` f ~> v *)
Definition hfield (l:loc) (i:field) (v:val) : hprop :=
(l+i)%nat ~~> v.
(* Notation for parsing *)
Notation "l `.` i '~~>' v" := (hfield l i v)
(at level 32, i at level 0, no associativity,
format "l `.` i '~~>' v") : heap_scope.
(* ** Configure [hsimpl] to make it aware of [hsingle] *)
Ltac hcancel_hook H ::=
......@@ -246,6 +256,9 @@ Ltac hcancel_hook H ::=
Implicit Types v w : val.
Implicit Types t : trm.
Implicit Types n : int.
Implicit Types l : loc.
Implicit Types f : field.
Implicit Types H : hprop.
Implicit Types Q : val->hprop.
......@@ -486,24 +499,28 @@ Proof using.
{ intros F. applys rule_extract_hprop. applys M. }
Qed.
Section RulesPrimitiveOps.
Transparent hstar hsingle.
Section RulesStateOps.
Transparent hstar hsingle hexists loc null.
Lemma rule_ref : forall v,
triple (prim_ref v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
triple (prim_ref v)
\[]
(fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
Proof using.
intros. intros HF h N.
forwards~ (l&Dl&Nl): (fmap_disjoint_new null h v).
forwards~ (l&Dl&Nl): (fmap_single_fresh null h v).
sets h1': (fmap_single l v).
exists (h1' \u h) (val_loc l). splits~.
{ applys~ red_ref. }
{ exists h1' h. split.
{ exists l. unfold h1'. applys~ himpl_hprop_r (l ~~> v). hnfs~. }
{ exists l. applys~ himpl_hprop_r. unfold h1'. hnfs~. }
{ splits~. hhsimpl~. } }
Qed.
Lemma rule_get : forall v l,
triple (prim_get (val_loc l)) (l ~~> v) (fun x => \[x = v] \* (l ~~> v)).
triple (prim_get (val_loc l))
(l ~~> v)
(fun x => \[x = v] \* (l ~~> v)).
Proof using.
intros. intros HF h N. exists h v. splits~.
{ applys red_get. destruct N as (?&?&(?&?)&?&?&?).
......@@ -512,7 +529,9 @@ Proof using.
Qed.
Lemma rule_set : forall w l v,
triple (prim_set (val_loc l) w) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w).
triple (prim_set (val_loc l) w)
(l ~~> v)
(fun r => \[r = val_unit] \* l ~~> w).
Proof using.
intros. intros HF h N. destruct N as (h1&h2&(N0&N1)&N2&N3&N4).
hnf in N1. sets h1': (fmap_single l w).
......@@ -525,7 +544,81 @@ Proof using.
{ subst h1. applys~ fmap_disjoint_single_set v. } } }
Qed.
End RulesPrimitiveOps.
Definition alloc_post (l:loc) (k:nat) :=
nat_fold (fun i H => (Hexists v, l`.`i ~~> v) \* H) k \[].
Lemma alloc_post_zero : forall l,
alloc_post l O = \[].
Proof using. auto. Qed.
Lemma alloc_post_succ : forall l k,
alloc_post l (S k) = (Hexists v, l`.`k ~~> v) \* alloc_post l k.
Proof using. auto. Qed.
Global Opaque alloc_post.
Lemma alloc_post_fmap_conseq : forall l k v,
l <> null ->
alloc_post l k (fmap_conseq l k v).
Proof using.
introv N. induction k; simpl.
{ rewrite fmap_conseq_zero, alloc_post_zero. applys~ hempty_intro. }
{ rewrite fmap_conseq_succ, alloc_post_succ.
exists (fmap_single (l + k)%nat v) (fmap_conseq l k v). splits~.
{ applys hexists_intro. split~. unfolds loc, null. math. }
{ applys~ fmap_disjoint_single_conseq. } }
Qed.
Lemma rule_alloc : forall n,
n > 0 ->
triple (prim_alloc (val_int n))
\[]
(fun r => Hexists l, \[r = val_loc l] \* alloc_post l (abs n)).
Proof using. (* Note: [abs n] currently does not compute in Coq. *)
introv N Hh.
forwards~ (l&Dl&Nl): (fmap_conseq_fresh null h (abs n) val_unit).
sets h1': (fmap_conseq l (abs n) val_unit).
exists (h1' \u h) (val_loc l). splits~.
{ applys (red_alloc (abs n)); eauto.
rewrite~ abs_pos. math. }
{ exists h1' h. split.
{ exists l. applys~ himpl_hprop_r. applys~ alloc_post_fmap_conseq. }
{ splits~. hhsimpl~. } }
Qed.
End RulesStateOps.
Lemma rule_eq : forall v1 v2,
triple (prim_eq v1 v2)
\[]
(fun r => \[r = val_int (If v1 = v2 then 1 else 0)]).
Proof using.
introv Hh. exists___. splits.
{ applys* red_eq. }
{ hhsimpl. case_if*. }
Qed.
Lemma rule_add_int : forall n1 n2,
triple (prim_add n1 n2)
\[]
(fun r => \[r = val_int (n1 + n2)]).
Proof using.
introv Hh. exists___. splits.
{ applys* red_add_int. }
{ hhsimpl*. }
Qed.
Lemma rule_add_loc : forall l f,
triple (prim_add l (my_Z_of_nat f))
\[]
(fun r => \[r = val_loc (l+f)%nat]).
Proof using.
introv Hh. exists___. splits.
{ applys* red_add_loc. }
{ hhsimpl*. }
Qed.
(* ********************************************************************** *)
......
......@@ -465,7 +465,7 @@ Lemma hstar_single_same_loc_disjoint : forall (l:loc) (v1 v2:val),
Proof using.
intros. unfold hsingle.
intros h ((m1&n1)&(m2&n2)&(E1&X1&N1)&(E2&X2&N2)&D&E). false.
subst. applys* fmap_single_same_loc_disjoint l v1 v2.
subst. applys* fmap_disjoint_single_single_same_inv l v1 v2.
unfolds in D. rewrite <- E1. rewrite <- E2. auto.
Qed.
......@@ -709,12 +709,12 @@ Lemma rule_ref : forall v,
triple (prim_ref v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
Proof using.
intros. intros HF h N. rew_heap in N.
forwards~ (l&Dl&Nl): (fmap_disjoint_new null (h^s) v).
forwards~ (l&Dl&Nl): (fmap_single_fresh null (h^s) v).
sets m1': (fmap_single l v).
exists 0%nat ((m1' \+ h^s),h^c) (val_loc l). splits~.
{ applys~ red_ref. }
{ exists (m1',0%nat) h. split.
{ exists l. unfold m1'. applys~ himpl_hprop_r (l ~~> v). hnfs~. }
{ exists l. applys~ himpl_hprop_r. unfold m1'. hnfs~. }
{ splits~. hhsimpl~. } }
Qed.
......
......@@ -615,7 +615,7 @@ Lemma hstar_single_same_loc_disjoint : forall (l:loc) (v1 v2:val),
Proof using.
intros. unfold hsingle.
intros h (((m1&n1)&D1)&((m2&n2)&D2)&(E1&X1)&(E2&X2)&D&E). false.
subst. simpls. subst. applys* fmap_single_same_loc_disjoint l v1 v2.
subst. simpls. subst. applys* fmap_disjoint_single_single_same_inv l v1 v2.
Qed.
Global Opaque hsingle.
......@@ -1134,7 +1134,7 @@ Lemma rule_ref : forall v,
Proof using.
intros. intros h1 h2 _ P1.
lets E: hempty_inv P1. subst h1.
forwards~ (l&Dl&Nl): (fmap_disjoint_new null (heap_state h2) v).
forwards~ (l&Dl&Nl): (fmap_single_fresh null (heap_state h2) v).
lets~ (h1'&E1&E2): heap_make (fmap_single l v) (fmap_empty:state).
asserts E3: (heap_state h1' = fmap_single l v).
{ unstate. rewrite E1,E2. fmap_eq. }
......
......@@ -247,7 +247,7 @@ Lemma rule_ref : forall v,
triple (prim_ref v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
Proof using.
intros. intros HF h N.
forwards~ (l&Dl&Nl): (fmap_disjoint_new null (heap_state h) v).
forwards~ (l&Dl&Nl): (fmap_single_fresh null (heap_state h) v).
lets~ (h1'&E1&E2): heap_make (fmap_single l v) (fmap_empty:state).
asserts E3: (heap_state h1' = fmap_single l v).
{ unstate. rewrite E1,E2. fmap_eq. }
......@@ -668,7 +668,7 @@ Lemma rule_ref : forall v,
triple (prim_ref v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
Proof using.
intros. intros HF h N.
forwards~ (l&Dl&Nl): (fmap_disjoint_new null (heap_state h) v).
forwards~ (l&Dl&Nl): (fmap_single_fresh null (heap_state h) v).
lets~ (h1'&E1&E2): heap_make (fmap_single l v) (fmap_empty:state).
asserts E3: (heap_state h1' = fmap_single l v).
{ unstate. rewrite E1,E2. fmap_eq. }
......
......@@ -246,7 +246,7 @@ Lemma hstar_single_same_loc_disjoint : forall (l:loc) (f:field) (v1 v2:val),
(l `.` f ~> v1) \* (l`.`f ~> v2) ==> \[False].
Proof using.
intros. unfold hsingle. intros h (h1&h2&E1&E2&D&E). false.
subst. applys* fmap_single_same_loc_disjoint.
subst. applys* fmap_disjoint_single_single_same_inv.
Qed.
Implicit Arguments hstar_single_same_loc_disjoint [].
......
......@@ -304,6 +304,16 @@ Lemma hpure_eq_hexists_empty : forall P,
\[P] = (Hexists (p:P), \[]).
Proof using. auto. Qed.
Lemma hexists_intro : forall A (x:A) (J:A->hprop) h,
J x h ->
(hexists J) h.
Proof using. intros. exists~ x. Qed.
Lemma hexists_inv : forall A (J:A->hprop) h,
(hexists J) h ->
exists x, J x h.
Proof using. intros. destruct H as [x H]. exists~ x. Qed.
Lemma htop_intro : forall h,
\Top h.
Proof using. intros. exists~ (=h). Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment