TypesAndMutation: type safety with garbage collection

Map.v

@@ -12,7 +12,7 @@ Module Type S.
   Parameter remove : forall A B, fmap A B -> A -> fmap A B.
   Parameter join : forall A B, fmap A B -> fmap A B -> fmap A B.
   Parameter merge : forall A B, (option B -> option B -> option B) -> fmap A B -> fmap A B -> fmap A B.
-  Parameter restrict : forall A B, (A -> bool) -> fmap A B -> fmap A B.
+  Parameter restrict : forall A B, (A -> Prop) -> fmap A B -> fmap A B.
   Parameter includes : forall A B, fmap A B -> fmap A B -> Prop.
 
   Notation "$0" := (empty _ _).
@@ -121,8 +121,17 @@ Module Type S.
   Axiom dom_add : forall A B (m : fmap A B) (k : A) (v : B),
     dom (add m k v) = {k} \cup dom m.
 
-  Axiom lookup_restrict : forall A B (f : A -> bool) (m : fmap A B) k,
+  Axiom lookup_restrict_true : forall A B (P : A -> Prop) (m : fmap A B) k,
-    lookup (restrict f m) k = if f k then lookup m k else None.
+    P k
+    -> lookup (restrict P m) k = lookup m k.
+
+  Axiom lookup_restrict_false : forall A B (P : A -> Prop) (m : fmap A B) k,
+    ~P k
+    -> lookup (restrict P m) k = None.
+
+  Axiom lookup_restrict_true_fwd : forall A B (P : A -> Prop) (m : fmap A B) k v,
+    lookup (restrict P m) k = Some v
+    -> P k.
 
   Hint Extern 1 => match goal with
                      | [ H : lookup (empty _ _) _ = Some _ |- _ ] =>
@@ -132,7 +141,7 @@ Module Type S.
   Hint Resolve includes_lookup includes_add empty_includes.
 
   Hint Rewrite lookup_empty lookup_add_eq lookup_add_ne lookup_remove_eq lookup_remove_ne
-       lookup_merge lookup_restrict using congruence.
+       lookup_merge lookup_restrict_true lookup_restrict_false using congruence.
 
   Hint Rewrite dom_empty dom_add.
 
@@ -187,8 +196,8 @@ Module M : S.
   Definition merge A B f (m1 m2 : fmap A B) : fmap A B :=
     fun k => f (m1 k) (m2 k).
   Definition lookup A B (m : fmap A B) (k : A) := m k.
-  Definition restrict A B (f : A -> bool) (m : fmap A B) : fmap A B :=
+  Definition restrict A B (P : A -> Prop) (m : fmap A B) : fmap A B :=
-    fun k => if f k then m k else None.
+    fun k => if decide (P k) then m k else None.
   Definition includes A B (m1 m2 : fmap A B) :=
     forall k v, m1 k = Some v -> m2 k = Some v.
 
@@ -414,10 +423,28 @@ Module M : S.
     destruct (decide (k' = k)); intuition congruence.
   Qed.
 
-  Theorem lookup_restrict : forall A B (f : A -> bool) (m : fmap A B) k,
+  Theorem lookup_restrict_true : forall A B (P : A -> Prop) (m : fmap A B) k,
-    lookup (restrict f m) k = if f k then lookup m k else None.
+    P k
+    -> lookup (restrict P m) k = lookup m k.
   Proof.
-    auto.
+    unfold lookup, restrict; intros.
+    destruct (decide (P k)); tauto.
+  Qed.
+
+  Theorem lookup_restrict_false : forall A B (P : A -> Prop) (m : fmap A B) k,
+    ~P k
+    -> lookup (restrict P m) k = None.
+  Proof.
+    unfold lookup, restrict; intros.
+    destruct (decide (P k)); tauto.
+  Qed.
+
+  Theorem lookup_restrict_true_fwd : forall A B (P : A -> Prop) (m : fmap A B) k v,
+    lookup (restrict P m) k = Some v
+    -> P k.
+  Proof.
+    unfold lookup, restrict; intros.
+    destruct (decide (P k)); intuition congruence.
   Qed.
 End M.
 

TypesAndMutation.v

@@ -5,7 +5,7 @@
 
 Require Import Frap.
 
-Module Rlc.
+Module References.
   Notation loc := nat.
 
   Inductive exp : Set :=
@@ -389,4 +389,202 @@ Module Rlc.
     cases s.
     eauto.
   Qed.
-End Rlc.
+End References.
+
+Module GarbageCollection.
+  Import References.
+
+  Fixpoint freeLocs (e : exp) : set loc :=
+    match e with
+    | Var _ => {}
+    | Const _ => {}
+    | Plus e1 e2 => freeLocs e1 \cup freeLocs e2
+    | Abs _ e1 => freeLocs e1
+    | App e1 e2 => freeLocs e1 \cup freeLocs e2
+    | New e1 => freeLocs e1
+    | Read e1 => freeLocs e1
+    | Write e1 e2 => freeLocs e1 \cup freeLocs e2
+    | Loc l => {l}
+    end.
+
+  Inductive reachableLoc (h : heap) : loc -> loc -> Prop :=
+  | ReachSelf : forall l, reachableLoc h l l
+  | ReachLookup : forall l e l' l'',
+      h $? l = Some e
+      -> l' \in freeLocs e
+      -> reachableLoc h l' l''
+      -> reachableLoc h l l''.
+
+  Inductive reachableLocFromExp (h : heap) : exp -> loc -> Prop :=
+  | ReachFromExp : forall l e l',
+      l \in freeLocs e
+      -> reachableLoc h l l'
+      -> reachableLocFromExp h e l'.
+
+  Inductive step : heap * exp -> heap * exp -> Prop :=
+  | StepRule : forall C e1 e2 e1' e2' h h',
+    plug C e1 e1'
+    -> plug C e2 e2'
+    -> step0 (h, e1) (h', e2)
+    -> step (h, e1') (h', e2')
+  | StepGc : forall h h' e lDefinitelyGone,
+    (forall l e',
+        reachableLocFromExp h e l
+        -> h $? l = Some e'
+        -> h' $? l = Some e')
+    -> (forall l e',
+           h' $? l = Some e'
+           -> h $? l = Some e')
+    -> h $? lDefinitelyGone <> None
+    -> h' $? lDefinitelyGone = None
+    -> step (h, e) (h', e).
+
+  Hint Constructors step.
+
+  Definition trsys_of (e : exp) := {|
+    Initial := {($0, e)};
+    Step := step
+  |}.
+
+
+  (** * Type soundness *)
+
+  Definition unstuck (he : heap * exp) := value (snd he)
+    \/ (exists he', step he he').
+
+  Lemma progress : forall ht h, heapty ht h
+    -> forall e t,
+      hasty ht $0 e t
+      -> value e
+         \/ exists he', step (h, e) he'.
+  Proof.
+    intros.
+    eapply References.progress in H0; t.
+  Qed.
+
+  Lemma reachableLocFromExp_trans : forall h e1 l e2,
+      reachableLocFromExp h e1 l
+      -> freeLocs e1 \subseteq freeLocs e2
+      -> reachableLocFromExp h e2 l.
+  Proof.
+    invert 1; simplify.
+    econstructor.
+    sets; eauto.
+    assumption.
+  Qed.
+
+  Hint Resolve reachableLocFromExp_trans.
+  Hint Extern 1 (_ \in _) => simplify; solve [ sets ].
+  Hint Extern 1 (_ \subseteq _) => simplify; solve [ sets ].
+  Hint Constructors reachableLoc reachableLocFromExp.
+
+  Lemma hasty_restrict : forall H h H' G e t,
+      heapty H h
+      -> hasty H G e t
+      -> (forall l t, reachableLocFromExp h e l
+                      -> H $? l = Some t
+                      -> H' $? l = Some t)
+      -> hasty H' G e t.
+  Proof.
+    induct 2; simplify; econstructor; eauto.
+  Qed.
+
+  Lemma reachableLoc_sandwich : forall h l l' e l'',
+    reachableLoc h l l'
+    -> h $? l' = Some e
+    -> reachableLocFromExp h e l''
+    -> reachableLoc h l l''.
+  Proof.
+    induct 1; simplify; eauto.
+    invert H0; eauto.
+  Qed.
+
+  Lemma reachableLocFromExp_sandwich : forall h e l e' l',
+    reachableLocFromExp h e l
+    -> h $? l = Some e'
+    -> reachableLocFromExp h e' l'
+    -> reachableLocFromExp h e l'.
+  Proof.
+    invert 1; simplify.
+    econstructor; eauto.
+    eapply reachableLoc_sandwich; eauto.
+  Qed.
+
+  Lemma preservation : forall h1 e1 h2 e2,
+    step (h1, e1) (h2, e2)
+    -> forall H1 t, hasty H1 $0 e1 t
+                   -> heapty H1 h1
+                   -> exists H2, hasty H2 $0 e2 t
+                                 /\ heapty H2 h2.
+  Proof.
+    invert 1; simplify.
+
+    eapply generalize_plug in H; eauto.
+    invert H; propositional.
+    eapply preservation0 in H6; eauto.
+    invert H6; propositional.
+    eauto.
+
+    exists (restrict (reachableLocFromExp h1 e2) H1).
+    propositional.
+
+    eapply hasty_restrict; eauto.
+    simplify.
+    invert H0.
+    assert (H1 $? l = Some t0) by assumption.
+    apply H8 in H0.
+    invert H0; propositional.
+
+    assert (heapty H1 h1) by assumption.
+    invert H2.
+    exists bound; simplify; propositional.
+    assert (reachableLocFromExp h1 e2 l) by (eapply lookup_restrict_true_fwd; eassumption).
+    simplify.
+    apply H3 in H2.
+    invert H2; propositional.
+    apply H4 in H2; auto.
+    eexists; propositional.
+    eauto.
+    eapply hasty_restrict.
+    eauto.
+    eauto.
+    simplify.
+    assert (H1 $? l0 = Some t1) by assumption.
+    apply H3 in H13.
+    invert H13; propositional.
+    simplify.
+    rewrite lookup_restrict_true; auto.
+    eapply reachableLocFromExp_sandwich; eauto.
+
+    cases (h2 $? l); eauto.
+    apply H8 in H2.
+    apply H5 in Heq.
+    equality.
+  Qed.
+
+  Hint Resolve progress preservation.
+
+  Theorem safety : forall e t, hasty $0 $0 e t
+    -> invariantFor (trsys_of e)
+                    (fun he' => value (snd he')
+                                \/ exists he'', step he' he'').
+  Proof.
+    simplify.
+    apply invariant_weaken with (invariant1 := fun he' => exists H,
+                                                   hasty H $0 (snd he') t
+                                                   /\ heapty H (fst he')); eauto.
+    apply invariant_induction; simplify; eauto.
+    propositional.
+    subst; simplify.
+    eauto.
+    invert H0.
+    propositional.
+    cases s; cases s'; simplify.
+    eauto.
+
+    invert 1.
+    propositional.
+    cases s.
+    eauto.
+  Qed.
+End GarbageCollection.

_CoqProject

@@ -21,3 +21,4 @@ OperationalSemantics.v
 AbstractInterpretation.v
 LambdaCalculusAndTypeSoundness_template.v
 LambdaCalculusAndTypeSoundness.v
+TypesAndMutation.v