metatheory.v 9.37 KB
Newer Older
1
From stdpp Require Import gmap.
2
From iris.heap_lang Require Export lang.
3 4 5 6 7 8 9 10 11 12

(* This file contains some metatheory about the heap_lang language,
  which is not needed for verifying programs. *)

(* Closed expressions and values. *)
Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
  match e with
  | Val v => is_closed_val v
  | Var x => bool_decide (x  X)
  | Rec f x e => is_closed_expr (f :b: x :b: X) e
Amin Timany's avatar
Amin Timany committed
13
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Load e =>
14
     is_closed_expr X e
15
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 =>
16
     is_closed_expr X e1 && is_closed_expr X e2
Ralf Jung's avatar
Ralf Jung committed
17
  | If e0 e1 e2 | Case e0 e1 e2 | CmpXchg e0 e1 e2 | Resolve e0 e1 e2 =>
18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
     is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
  | NewProph => true
  end
with is_closed_val (v : val) : bool :=
  match v with
  | LitV _ => true
  | RecV f x e => is_closed_expr (f :b: x :b: []) e
  | PairV v1 v2 => is_closed_val v1 && is_closed_val v2
  | InjLV v | InjRV v => is_closed_val v
  end.

Lemma is_closed_weaken X Y e : is_closed_expr X e  X  Y  is_closed_expr Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

Lemma is_closed_weaken_nil X e : is_closed_expr [] e  is_closed_expr X e.
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.

Lemma is_closed_subst X e x v :
  is_closed_val v  is_closed_expr (x :: X) e  is_closed_expr X (subst x v e).
Proof.
  intros Hv. revert X.
  induction e=> X /= ?; destruct_and?; split_and?; simplify_option_eq;
    try match goal with
    | H : ¬(_  _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
    end; eauto using is_closed_weaken with set_solver.
Qed.
Lemma is_closed_subst' X e x v :
  is_closed_val v  is_closed_expr (x :b: X) e  is_closed_expr X (subst' x v e).
Proof. destruct x; eauto using is_closed_subst. Qed.

(* Substitution *)
Lemma subst_is_closed X e x es : is_closed_expr X e  x  X  subst x es e = e.
Proof.
  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.

Lemma subst_is_closed_nil e x v : is_closed_expr [] e  subst x v e = e.
Proof. intros. apply subst_is_closed with []; set_solver. Qed.

Lemma subst_subst e x v v' :
  subst x v (subst x v' e) = subst x v' e.
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst' e x v v' :
  subst' x v (subst' x v' e) = subst' x v' e.
Proof. destruct x; simpl; auto using subst_subst. Qed.

Lemma subst_subst_ne e x y v v' :
  x  y  subst x v (subst y v' e) = subst y v' (subst x v e).
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using eq_sym, subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst_ne' e x y v v' :
  x  y  subst' x v (subst' y v' e) = subst' y v' (subst' x v e).
Proof. destruct x, y; simpl; auto using subst_subst_ne with congruence. Qed.

Lemma subst_rec' f y e x v :
  x = f  x = y  x = BAnon 
  subst' x v (Rec f y e) = Rec f y e.
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
Lemma subst_rec_ne' f y e x v :
  (x  f  f = BAnon)  (x  y  y = BAnon) 
  subst' x v (Rec f y e) = Rec f y (subst' x v e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.

Amin Timany's avatar
Amin Timany committed
87 88 89 90
Lemma  bin_op_eval_closed op v1 v2 v':
  is_closed_val v1  is_closed_val v2  bin_op_eval op v1 v2 = Some v' 
  is_closed_val v'.
Proof.
91
  rewrite /bin_op_eval /bin_op_eval_bool /bin_op_eval_int /bin_op_eval_loc;
Amin Timany's avatar
Amin Timany committed
92 93 94 95 96 97 98 99 100
    repeat case_match; by naive_solver.
Qed.

Lemma heap_closed_alloc σ l n w :
  0 < n 
  is_closed_val w 
  map_Forall (λ _ v, is_closed_val v) (heap σ) 
  ( i : Z, 0  i  i < n  heap σ !! (l + i) = None) 
  map_Forall (λ _ v, is_closed_val v)
Ralf Jung's avatar
Ralf Jung committed
101
             (heap_array l (replicate (Z.to_nat n) w)  heap σ).
Amin Timany's avatar
Amin Timany committed
102 103 104
Proof.
  intros Hn Hw Hσ Hl.
  eapply (map_Forall_ind
Ralf Jung's avatar
Ralf Jung committed
105
            (λ k v, ((heap_array l (replicate (Z.to_nat n) w)  heap σ)
Amin Timany's avatar
Amin Timany committed
106 107 108 109 110
                       !! k = Some v))).
  - apply map_Forall_empty.
  - intros m i x Hi Hix Hkwm Hm.
    apply map_Forall_insert_2; auto.
    apply lookup_union_Some in Hix; last first.
Ralf Jung's avatar
Ralf Jung committed
111
    { eapply heap_array_map_disjoint;
Amin Timany's avatar
Amin Timany committed
112
        rewrite replicate_length Z2Nat.id; auto with lia. }
Ralf Jung's avatar
Ralf Jung committed
113 114 115 116 117
    destruct Hix as [(?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup|
                     [j Hj]%elem_of_map_to_list%elem_of_list_lookup_1].
    + rewrite !Z2Nat.id in Hlt; eauto with lia.
    + apply map_Forall_to_list in Hσ.
      by eapply Forall_lookup in Hσ; eauto; simpl in *.
Amin Timany's avatar
Amin Timany committed
118 119 120 121
  - apply map_Forall_to_list, Forall_forall.
    intros [? ?]; apply elem_of_map_to_list.
Qed.

122 123 124
(* The stepping relation preserves closedness *)
Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
  is_closed_expr [] e1 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
125
  map_Forall (λ _ v, is_closed_val v) σ1.(heap) 
126 127 128
  head_step e1 σ1 obs e2 σ2 es 

  is_closed_expr [] e2  Forall (is_closed_expr []) es 
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
129
  map_Forall (λ _ v, is_closed_val v) σ2.(heap).
130 131
Proof.
  intros Cl1 Clσ1 STEP.
132
  induction STEP; simpl in *; split_and!;
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
133
    try apply map_Forall_insert_2; try by naive_solver.
134 135
  - subst. repeat apply is_closed_subst'; naive_solver.
  - unfold un_op_eval in *. repeat case_match; naive_solver.
Amin Timany's avatar
Amin Timany committed
136 137
  - eapply bin_op_eval_closed; eauto; naive_solver.
  - by apply heap_closed_alloc.
138
  - case_match; try apply map_Forall_insert_2; by naive_solver.
139
Qed.
140 141 142 143 144 145 146

(* Parallel substitution with maps of values indexed by strings *)
Definition binder_delete {A} (x : binder) (vs : gmap string A) : gmap string A :=
  if x is BNamed x' then delete x' vs else vs.
Definition binder_insert {A} (x : binder) (v : A) (vs : gmap string A) : gmap string A :=
  if x is BNamed x' then <[x':=v]>vs else vs.

147 148 149
Lemma binder_insert_fmap {A B : Type} (f : A  B) (x : A) b vs :
  f <$> binder_insert b x vs = binder_insert b (f x) (f <$> vs).
Proof. destruct b; rewrite ?fmap_insert //. Qed.
150 151 152
Lemma lookup_binder_delete_None {A : Type} (vs : gmap string A) x y :
  binder_delete x vs !! y = None  x = BNamed y  vs !! y = None.
Proof. destruct x; rewrite /= ?lookup_delete_None; naive_solver. Qed.
153

154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169
Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
  match e with
  | Val _ => e
  | Var y => if vs !! y is Some v then Val v else Var y
  | Rec f y e => Rec f y (subst_map (binder_delete y (binder_delete f vs)) e)
  | App e1 e2 => App (subst_map vs e1) (subst_map vs e2)
  | UnOp op e => UnOp op (subst_map vs e)
  | BinOp op e1 e2 => BinOp op (subst_map vs e1) (subst_map vs e2)
  | If e0 e1 e2 => If (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
  | Pair e1 e2 => Pair (subst_map vs e1) (subst_map vs e2)
  | Fst e => Fst (subst_map vs e)
  | Snd e => Snd (subst_map vs e)
  | InjL e => InjL (subst_map vs e)
  | InjR e => InjR (subst_map vs e)
  | Case e0 e1 e2 => Case (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
  | Fork e => Fork (subst_map vs e)
Amin Timany's avatar
Amin Timany committed
170
  | AllocN e1 e2 => AllocN (subst_map vs e1) (subst_map vs e2)
171 172
  | Load e => Load (subst_map vs e)
  | Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
Ralf Jung's avatar
Ralf Jung committed
173
  | CmpXchg e0 e1 e2 => CmpXchg (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
174 175
  | FAA e1 e2 => FAA (subst_map vs e1) (subst_map vs e2)
  | NewProph => NewProph
176
  | Resolve e0 e1 e2 => Resolve (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203
  end.

Lemma subst_map_empty e : subst_map  e = e.
Proof.
  assert ( x, binder_delete x (:gmap _ val) = ) as Hdel.
  { intros [|x]; by rewrite /= ?delete_empty. }
  induction e; simplify_map_eq; rewrite ?Hdel; auto with f_equal.
Qed.
Lemma subst_map_insert x v vs e :
  subst_map (<[x:=v]>vs) e = subst x v (subst_map (delete x vs) e).
Proof.
  revert vs. assert ( (y : binder) (vs : gmap _ val), y  BNamed x 
    binder_delete y (<[x:=v]> vs) = <[x:=v]> (binder_delete y vs)) as Hins.
  { intros [|y] vs ?; rewrite /= ?delete_insert_ne //; congruence. }
  assert ( (y : binder) (vs : gmap _ val),
    binder_delete y (delete x vs) = delete x (binder_delete y vs)) as Hdel.
  { by intros [|y] ?; rewrite /= 1?delete_commute. }
  induction e=> vs; simplify_map_eq; auto with f_equal.
  - match goal with
    | |- context [ <[?x:=_]> _ !! ?y ] =>
       destruct (decide (x = y)); simplify_map_eq=> //
    end. by case (vs !! _); simplify_option_eq.
  - destruct (decide _) as [[??]|[<-%dec_stable|[<-%dec_stable ?]]%not_and_l_alt].
    + rewrite !Hins // !Hdel. eauto with f_equal.
    + by rewrite /= delete_insert_delete delete_idemp.
    + by rewrite /= Hins // delete_insert_delete !Hdel delete_idemp.
Qed.
204 205 206 207
Lemma subst_map_binder_insert b v vs e :
  subst_map (binder_insert b v vs) e =
  subst' b v (subst_map (binder_delete b vs) e).
Proof. destruct b; rewrite ?subst_map_insert //. Qed.
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224

(* subst_map on closed expressions *)
Lemma subst_map_is_closed X e vs :
  is_closed_expr X e 
  ( x, x  X  vs !! x = None) 
  subst_map vs e = e.
Proof.
  revert X vs. assert ( x x1 x2 X (vs : gmap string val),
    ( x, x  X  vs !! x = None) 
    x  x2 :b: x1 :b: X 
    binder_delete x1 (binder_delete x2 vs) !! x = None).
  { intros x x1 x2 X vs ??. rewrite !lookup_binder_delete_None. set_solver. }
  induction e=> X vs /= ? HX; repeat case_match; naive_solver eauto with f_equal.
Qed.

Lemma subst_map_is_closed_nil e vs : is_closed_expr [] e  subst_map vs e = e.
Proof. intros. apply subst_map_is_closed with []; set_solver. Qed.