Commit b1b14570 authored by charguer's avatar charguer
Browse files

typecheck_model

parent 4e655c8e
Set Implicit Arguments.
Require Import LibCore Shared CFLib.
Require Import LibCore Shared.
(************************************************************)
......@@ -54,23 +54,52 @@ with subst_trm (y : var) (w : val) (t : trm) : trm :=
| trm_app v1 v2 => trm_app (subst_val y w v1) (subst_val y w v2)
| trm_letfix f x t1 t2 =>
trm_letfix f x
(If x = y \/ f = y then t1 else val_fix f x (subst_trm y w t1))
(If x = y \/ f = y then t1 else subst_trm y w t1)
(If f = y then t2 else subst_trm y w t2)
| trm_new v => trm_new (subst_val y w v)
| trm_get v => trm_get (subst_val y w v)
| trm_set v1 v2 => trm_set (subst_val y w v1) (subst_val y w v2)
end.
(*
Implicit Types t : trm.
Implicit Types v : val.
Implicit Types x f : var.
Implicit Types l : loc.
*)
(********************************************************************)
(* ** States *)
(** Representation of partial functions => see CFHeaps.v *)
(*------------------------------------------------------------------*)
(* ** Representation of partial functions *)
(** Type of partial functions from A to B *)
Definition pfun (A B : Type) :=
A -> option B.
(** Finite domain of a partial function *)
Definition pfun_finite (A B : Type) (f : pfun A B) :=
exists (L : list A), forall (x:A), f x <> None -> Mem x L.
(** Disjointness of domain of two partial functions *)
Definition pfun_disjoint (A B : Type) (f1 f2 : pfun A B) :=
forall (x:A), f1 x = None \/ f2 x = None.
(** Disjoint union of two partial functions *)
Definition pfun_union (A B : Type) (f1 f2 : pfun A B) :=
fun (x:A) => match f1 x with
| Some y => Some y
| None => f2 x
end.
(*------------------------------------------------------------------*)
(** Representation of state *)
Section State.
......@@ -80,26 +109,25 @@ Inductive state : Type := state_of {
state_data :> pfun loc val;
state_finite : pfun_finite state_data }.
Implicit Arguments state_of [].
(** Proving states equals *)
Lemma state_eq : forall f1 f2 F1 F2,
(forall x, f1 x = f2 x) ->
state_of f1 F1 = state_of f2 F2.
Proof using.
introv H. asserts: (f1 = f2). extens~. subst.
fequals. (* note: involves proof irrelevance *)
Qed.
Implicit Arguments state_of [].
(** Disjoint states *)
Definition state_disjoint (h1 h2 : state) : Prop :=
pfun_disjoint h1 h2.
Notation "\# h1 h2" := (state_disjoint h1 h2)
(at level 40, h1 at level 0, h2 at level 0, no associativity) : state_scope.
Local Open Scope state_scope.
Definition state_disjoint_3 h1 h2 h3 :=
state_disjoint h1 h2 /\ state_disjoint h2 h3 /\ state_disjoint h1 h3.
(** Finiteness of union *)
Lemma pfun_union_finite : forall (A B : Type) (f1 f2 : pfun A B),
pfun_finite f1 -> pfun_finite f2 -> pfun_finite (pfun_union f1 f2).
Proof using.
introv [L1 F1] [L2 F2]. exists (L1 ++ L2). introv M.
specializes F1 x. specializes F2 x. unfold pfun_union in M.
apply Mem_app_or. destruct~ (f1 x).
Qed.
(** Union of states *)
......@@ -107,9 +135,6 @@ Program Definition state_union (h1 h2 : state) : state :=
state_of (pfun_union h1 h2) _.
Next Obligation. destruct h1. destruct h2. apply~ pfun_union_finite. Qed.
Notation "h1 \+ h2" := (state_union h1 h2)
(at level 51, right associativity) : state_scope.
(** Empty state *)
Program Definition state_empty : state :=
......@@ -124,11 +149,30 @@ Next Obligation.
exists (l::nil). intros. case_if. subst~.
Qed.
End State.
Implicit Arguments state_of [].
Notation "\# h1 h2" := (state_disjoint h1 h2)
(at level 40, h1 at level 0, h2 at level 0, no associativity) : state_scope.
Notation "\# h1 h2 h3" := (state_disjoint_3 h1 h2 h3)
(at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity)
: state_scope.
Notation "h1 \+ h2" := (state_union h1 h2)
(at level 51, right associativity) : state_scope.
(************************************************************)
(* * Source language semantics *)
Section Red.
Local Open Scope state_scope.
Inductive red : state -> trm -> state -> val -> Prop :=
| red_val : forall m v,
red m (trm_val v) m v
......@@ -139,27 +183,28 @@ Inductive red : state -> trm -> state -> val -> Prop :=
red m1 t1 m2 v1 ->
red m2 (subst_trm x v1 t2) m3 r ->
red m1 (trm_let x t1 t2) m3 r
| red_app : forall m1 m2 v1 v2 f x t v r,
| red_app : forall m1 m2 v1 v2 f x t r,
v1 = val_fix f x t ->
red m1 (subst_trm f v1 (subst_trm x v2 t)) m2 r ->
red m1 (subst f (trm_fix f x t) (subst x v1 t)) m2 r
| red_fix : forall m f x t1,
red m1 (trm_app v1 v2) m2 r
| red_fix : forall m1 m2 f x t1 t2 r,
red m1 (subst_trm f (val_fix f x t1) t2) m2 r ->
red m1 (trm_letfix f x t1 t2) m2 r
| red_new : forall m v l mlv,
mb = (heap_single l v) ->
| red_new : forall ma mb v l,
mb = (state_single l v) ->
\# ma mb ->
red ma (trm_new v) (ma \+ mb) val_unit
red ma (trm_new v) (ma \+ mb) (val_loc l)
| red_get : forall ma mb l v,
ma = (heap_single l v) ->
ma = (state_single l v) ->
\# ma mb ->
red (ma \+ mb) (trm_get l) (ma \+ mb) v
red (ma \+ mb) (trm_get (val_loc l)) (ma \+ mb) v
| red_set : forall ma1 ma2 mb l v1 v2,
ma1 = (heap_single l v1) ->
ma2 = (heap_single l v2) ->
ma1 = (state_single l v1) ->
ma2 = (state_single l v2) ->
\# ma1 mb ->
red (ma1 \+ mb) (trm_set l v2) (ma2 \+ mb) val_unit.
red (ma1 \+ mb) (trm_set (val_loc l) v2) (ma2 \+ mb) val_unit.
End Red.
(********************************************************************)
......@@ -191,21 +236,15 @@ Definition prod_func A B (F:A->A->A) (G:B->B->B) (v1 v2:A*B) := (* todo move to
(** Disjoint heaps *)
Definition heap_disjoint (h1 h2 : heap) : Prop :=
state_disjoint.
state_disjoint h1 h2.
(* prod_st2 state_disjoint (fun _ _ => True) h1 h2. *)
Notation "\# h1 h2" := (heap_disjoint h1 h2)
(at level 40, h1 at level 0, h2 at level 0, no associativity).
(** Union of heaps *)
Definition heap_union (h1 h2 : heap) : heap :=
state_union.
state_union h1 h2.
(* prod_func state_union (fun a b => (a + b)%nat) h1 h2. *)
Notation "h1 \+ h2" := (heap_union h1 h2)
(at level 51, right associativity).
(** Empty heap *)
Definition heap_empty : heap :=
......@@ -260,19 +299,27 @@ Definition heap_is_gc : hprop :=
Instance hprop_inhab : Inhab hprop.
Proof using. intros. apply (prove_Inhab heap_is_empty). Qed.
Global Opaque heap_is_empty_st heap_is_single.
(*------------------------------------------------------------------*)
(* ** Notation for heap predicates *)
Notation "\[]" := (heap_is_empty)
(at level 0) : heap_scope.
Notation "\# h1 h2" := (heap_disjoint h1 h2)
(at level 40, h1 at level 0, h2 at level 0, no associativity) : heap_scope.
Notation "\# h1 h2 h3" := (state_disjoint_3 h1 h2 h3)
(at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity) : heap_scope.
Notation "h1 \+ h2" := (heap_union h1 h2)
(at level 51, right associativity) : heap_scope.
Open Scope heap_scope.
Bind Scope heap_scope with hprop.
Delimit Scope heap_scope with h.
Notation "\[]" := (heap_is_empty)
(at level 0) : heap_scope.
Notation "\[ L ]" := (heap_is_empty_st L)
(at level 0, L at level 99) : heap_scope.
......@@ -311,19 +358,6 @@ Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) ( x4 : T4 ) ( x5 : T5 )
(Hexists x1:T1, Hexists x2:T2, Hexists x3:T3, Hexists x4:T4, Hexists x5:T5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 x2 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, H)
(at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 x2 x3 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, Hexists x3:T, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 x2 x3 x4 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, Hexists x3:T, Hexists x4:T, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 x2 x3 x4 x5 : T ) , H" :=
(Hexists x1:T, Hexists x2:T, Hexists x3:T, Hexists x4:T, Hexists x5:T, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) x2 , H" :=
(Hexists x1:T1, Hexists x2, H)
(at level 39, x1 ident, x2 ident, H at level 50, only parsing) : heap_scope.
......@@ -385,6 +419,41 @@ Definition triple t H Q :=
(********************************************************************)
(* ** Lemmas on states and heaps *)
(*------------------------------------------------------------------*)
(* ** Properties on states *)
(** Symmetry of disjointness *)
Lemma pfun_disjoint_sym : forall (A B : Type),
sym (@pfun_disjoint A B).
Proof using.
introv H. unfolds pfun_disjoint. intros z. specializes H z. intuition.
Qed.
(** Commutativity of disjoint union *)
Tactic Notation "cases" constr(E) := (* TODO: move *)
let H := fresh "Eq" in cases E as H.
Lemma pfun_union_comm : forall (A B : Type) (f1 f2 : pfun A B),
pfun_disjoint f1 f2 ->
pfun_union f1 f2 = pfun_union f2 f1.
Proof using.
introv H. extens. intros x. unfolds pfun_disjoint, pfun_union.
specializes H x. cases (f1 x); cases (f2 x); auto. destruct H; false.
Qed.
(** Proving states equals *)
Lemma state_eq : forall (f1 f2: loc -> option val) F1 F2,
(forall x, f1 x = f2 x) ->
state_of f1 F1 = state_of f2 F2.
Proof using.
introv H. asserts: (f1 = f2). extens~. subst.
fequals. (* note: involves proof irrelevance *)
Qed.
(*------------------------------------------------------------------*)
(* ** Properties on states *)
......@@ -396,7 +465,7 @@ Proof using. intros [f1 F1] [f2 F2]. apply pfun_disjoint_sym. Qed.
Lemma state_disjoint_comm : forall h1 h2,
\# h1 h2 = \# h2 h1.
Proof using. lets: state_disjoint_sym. extens*. Qed.
Proof using. unfold heap_disjoint. lets: state_disjoint_sym. extens*. Qed.
Lemma state_disjoint_empty_l : forall h,
state_disjoint state_empty h.
......@@ -429,13 +498,6 @@ Proof using.
apply state_disjoint_union_eq_r.
Qed.
Definition state_disjoint_3 h1 h2 h3 :=
state_disjoint h1 h2 /\ state_disjoint h2 h3 /\ state_disjoint h1 h3.
Notation "\# h1 h2 h3" := (state_disjoint_3 h1 h2 h3)
(at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity)
: state_scope.
Lemma state_disjoint_3_unfold : forall h1 h2 h3,
\# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3).
Proof using. auto. Qed.
......@@ -471,8 +533,6 @@ Proof using.
apply state_eq. intros x. unfold pfun_union. destruct~ (f1 x).
Qed.
End State.
(** Hints and tactics *)
Hint Resolve state_union_neutral_l state_union_neutral_r.
......@@ -501,6 +561,10 @@ Proof using.
Qed.*)
Admitted.
Notation "\# h1 h2" := (heap_disjoint h1 h2)
(at level 40, h1 at level 0, h2 at level 0, no associativity) : heap_scope.
Open Scope heap_scope.
Lemma heap_disjoint_comm : forall h1 h2,
\# h1 h2 = \# h2 h1.
Proof using.
......@@ -607,9 +671,16 @@ Tactic Notation "rew_disjoint" "*" :=
(* ** Predicate on Heaps *)
Global Opaque heap_is_empty_st heap_is_single.
(*------------------------------------------------------------------*)
(* ** Properties of heap empty *)
Section HeapEmpty.
Transparent heap_is_empty_st.
Lemma heap_is_empty_prove :
\[] heap_empty.
Proof using. hnfs~. Qed.
......@@ -618,12 +689,14 @@ Lemma heap_is_empty_st_prove : forall (P:Prop),
P -> \[P] heap_empty.
Proof using. intros. hnfs~. Qed.
End HeapEmpty.
Hint Resolve heap_is_empty_prove heap_is_empty_st_prove.
(*------------------------------------------------------------------*)
(* ** Properties of [star] and [pack] *)
Section Star.
Section HeapStar.
Transparent heap_is_star heap_union.
Lemma star_comm : comm heap_is_star.
......@@ -676,11 +749,11 @@ Lemma star_cancel : forall H1 H2 H2',
H2 ==> H2' -> H1 \* H2 ==> H1 \* H2'.
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
Lemma star_is_single_same_loc : forall (l:loc) A (v1 v2:A),
Lemma star_is_single_same_loc : forall (l:loc) (v1 v2:val),
(heap_is_single l v1) \* (heap_is_single l v2) ==> \[False].
Proof using.
Transparent heap_is_single state_single.
intros. intros h ((m1&n1)&(m2&n2)&(E1&?&?)&(E2&?&?)&(D&?)&E).
intros. intros h ((m1&n1)&(m2&n2)&E1&E2&D&E).
unfolds heap_disjoint, state_disjoint, prod_st2, pfun_disjoint.
specializes D l. rewrite E1, E2 in D.
unfold state_single in D. simpls. case_if. destruct D; tryfalse.
......@@ -701,12 +774,13 @@ Lemma heap_weaken_pack : forall A (x:A) H J,
Proof using. introv W h. exists x. apply~ W. Qed.
End Star.
End HeapStar.
(*------------------------------------------------------------------*)
(* ** Separation Logic monoid *)
Require Import LibStruct.
Definition sep_monoid := monoid_ heap_is_star heap_is_empty.
Global Instance sep_Monoid : Monoid sep_monoid.
......@@ -850,10 +924,6 @@ Proof using.
rewrite heap_union_neutral_l in *. splits~.
Qed.
Lemma hpull_id : forall A (x X : A) H1 H2 H',
(x = X -> H1 \* H2 ==> H') -> H1 \* (x ~> Id X \* H2) ==> H'.
Proof using. intros. unfold Id. apply~ hpull_prop. Qed.
Lemma hpull_exists : forall A H1 H2 H' (J:A->hprop),
(forall x, H1 \* J x \* H2 ==> H') -> H1 \* (heap_is_pack J \* H2) ==> H'.
Proof using.
......@@ -992,14 +1062,6 @@ Proof using.
exists h1 h2. splits~. exists heap_empty h2. splits~.
Qed.
Lemma hsimpl_id : forall A (x X : A) H' H1 H2,
H' ==> H1 \* H2 -> x = X -> H' ==> H1 \* (x ~> Id X \* H2).
Proof using. intros. unfold Id. apply~ hsimpl_prop. Qed.
Lemma hsimpl_id_unify : forall A (x : A) H' H1 H2,
H' ==> H1 \* H2 -> H' ==> H1 \* (x ~> Id x \* H2).
Proof using. intros. apply~ hsimpl_id. Qed.
Lemma hsimpl_exists : forall A (x:A) H' H1 H2 (J:A->hprop),
H' ==> H1 \* J x \* H2 -> H' ==> H1 \* (heap_is_pack J \* H2).
Proof using.
......@@ -1210,7 +1272,6 @@ Ltac check_arg_true v :=
Ltac hsimpl_setup process_credits :=
prepare_goal_hpull_himpl tt;
try (check_arg_true process_credits; credits_join_left_repeat tt);
hsimpl_left_empty tt;
apply hsimpl_start.
......@@ -1251,19 +1312,6 @@ Ltac hsimpl_find_same H HL :=
| _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* H \* _ => apply hsimpl_cancel_10
end.
Ltac hsimpl_find_data l HL cont :=
match HL with
| hdata _ l \* _ => apply hsimpl_cancel_eq_1
| _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_2
| _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_3
| _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_4
| _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_5
| _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_6
| _ \* _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_7
| _ \* _ \* _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_8
| _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_9
| _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_10
end; [ cont tt | ].
Ltac hsimpl_extract_exists tt :=
first [
......@@ -1277,18 +1325,7 @@ Ltac hsimpl_extract_exists tt :=
Ltac hsimpl_find_data_post tt :=
try solve
[ reflexivity
| fequal; fequal; first [ eassumption | symmetry; eassumption ] ];
try match goal with |- hdata ?X ?l = hdata ?Y ?l => match constr:(X,Y) with
| (?F1 _, ?F1 _) => fequal; fequal
| (?F1 ?F2 _, ?F1 ?F2 _) => fequal; fequal
| (?F1 ?F2 ?F3 _, ?F1 ?F2 ?F3 _) => fequal; fequal
| (?F1 ?F2 ?F3 ?F4 _, ?F1 ?F2 ?F3 ?F4 _) => fequal; fequal
| (?F1 ?F2 ?F3 ?F4 ?F5 _, ?F1 ?F2 ?F3 ?F4 ?F5 _) => fequal; fequal
| (?F1 ?F2 ?F3 ?F4 ?F5 ?F6 _, ?F1 ?F2 ?F3 ?F4 ?F5 ?F6 _) => fequal; fequal
| (?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 _, ?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 _) => fequal; fequal
| (?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 ?F8 _, ?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 ?F8 _) => fequal; fequal
| (?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 ?F8 ?F9 _, ?F1 ?F2 ?F3 ?F4 ?F5 ?F6 ?F7 ?F8 ?F9 _) => fequal; fequal
end end.
| fequal; fequal; first [ eassumption | symmetry; eassumption ] ].
(* todo: better implemented in cps style ? *)
......@@ -1322,7 +1359,6 @@ Ltac hsimpl_step process_credits :=
| heap_is_pack _ => hsimpl_extract_exists tt
| _ \* _ => apply hsimpl_assoc
| heap_is_single _ _ => hsimpl_try_same tt
| Group _ _ => hsimpl_try_same tt (* may fail *)
| ?H => (* should be check_noevar3 on the next line TODO *)
first [ is_evar H; fail 1 | idtac ];
hsimpl_find_same H HL (* may fail *)
......@@ -1516,12 +1552,12 @@ Tactic Notation "hchange" constr(E1) constr(E2) constr(E3) :=
(********************************************************************)
(* ** Soundness *)
Implicit Types H : hprop.
Implicit Types Q : val -> hprop.
Lemma frame_rule : forall t H Q H',
triple t H Q ->
triple t (H \* H') (Q \*+ H').
......
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