Library iris.heap_lang.metatheory

From stdpp Require Import gmap.
From iris.heap_lang Require Export lang.


Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
  match e with
  | Val vis_closed_val v
  | Var xbool_decide (x X)
  | Rec f x eis_closed_expr (f :b: x :b: X) e
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Free e | Load e
     is_closed_expr X e
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2
     is_closed_expr X e1 && is_closed_expr X e2
  | If e0 e1 e2 | Case e0 e1 e2 | CmpXchg e0 e1 e2 | Resolve e0 e1 e2
     is_closed_expr X e0 && is_closed_expr X e1 && is_closed_expr X e2
  | NewProphtrue
  end
with is_closed_val (v : val) : bool :=
  match v with
  | LitV _true
  | RecV f x eis_closed_expr (f :b: x :b: []) e
  | PairV v1 v2is_closed_val v1 && is_closed_val v2
  | InjLV v | InjRV vis_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 eX /= ?; 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.

Lemma subst_is_closed X e x es : is_closed_expr X e x X subst x es e = e.
Proof.
  revert X. induction eX /=; 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.

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.
  rewrite /bin_op_eval /bin_op_eval_bool /bin_op_eval_int /bin_op_eval_loc;
    repeat case_match; by naive_solver.
Qed.

Lemma heap_closed_alloc σ l n w :
  (0 < n)%Z
  is_closed_val w
  map_Forall (λ _ v, from_option is_closed_val true v) (heap σ)
  ( i : Z, (0 i)%Z (i < n)%Z heap σ !! (l +ₗ i) = None)
  map_Forall (λ _ v, from_option is_closed_val true v)
             (heap_array l (replicate (Z.to_nat n) w) heap σ).
Proof.
  intros Hn Hw Hσ Hl.
  eapply (map_Forall_ind
            (λ k v, ((heap_array l (replicate (Z.to_nat n) w) heap σ)
                       !! 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.
    { eapply heap_array_map_disjoint;
        rewrite replicate_length Z2Nat.id; auto with lia. }
    destruct Hix as [(?&?&?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup|
                     [j Hj]%elem_of_map_to_list%elem_of_list_lookup_1].
    + simplify_eq/=. rewrite !Z2Nat.id in Hlt; eauto with lia.
    + apply map_Forall_to_list in Hσ.
      by eapply Forall_lookup in Hσ; eauto; simpl in ×.
  - apply map_Forall_to_list, Forall_forall.
    intros [? ?]; apply elem_of_map_to_list.
Qed.

Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
  is_closed_expr [] e1
  map_Forall (λ _ v, from_option is_closed_val true v) σ1.(heap)
  head_step e1 σ1 obs e2 σ2 es
  is_closed_expr [] e2 Forall (is_closed_expr []) es
  map_Forall (λ _ v, from_option is_closed_val true v) σ2.(heap).
Proof.
  intros Cl1 Clσ1 STEP.
  induction STEP; simpl in *; split_and!;
    try apply map_Forall_insert_2; try by naive_solver.
  - subst. repeat apply is_closed_subst'; naive_solver.
  - unfold un_op_eval in ×. repeat case_match; naive_solver.
  - eapply bin_op_eval_closed; eauto; naive_solver.
  - by apply heap_closed_alloc.
  - select (_ !! _ = Some _) ltac:(fun Hby specialize (Clσ1 _ _ H)).
  - select (_ !! _ = Some _) ltac:(fun Hby specialize (Clσ1 _ _ H)).
  - case_match; try apply map_Forall_insert_2; by naive_solver.
Qed.

Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
  match e with
  | Val _e
  | Var yif vs !! y is Some v then Val v else Var y
  | Rec f y eRec f y (subst_map (binder_delete y (binder_delete f vs)) e)
  | App e1 e2App (subst_map vs e1) (subst_map vs e2)
  | UnOp op eUnOp op (subst_map vs e)
  | BinOp op e1 e2BinOp op (subst_map vs e1) (subst_map vs e2)
  | If e0 e1 e2If (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
  | Pair e1 e2Pair (subst_map vs e1) (subst_map vs e2)
  | Fst eFst (subst_map vs e)
  | Snd eSnd (subst_map vs e)
  | InjL eInjL (subst_map vs e)
  | InjR eInjR (subst_map vs e)
  | Case e0 e1 e2Case (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
  | Fork eFork (subst_map vs e)
  | AllocN e1 e2AllocN (subst_map vs e1) (subst_map vs e2)
  | Free eFree (subst_map vs e)
  | Load eLoad (subst_map vs e)
  | Store e1 e2Store (subst_map vs e1) (subst_map vs e2)
  | CmpXchg e0 e1 e2CmpXchg (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
  | FAA e1 e2FAA (subst_map vs e1) (subst_map vs e2)
  | NewProphNewProph
  | Resolve e0 e1 e2Resolve (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
  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. induction evs; 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 !binder_delete_insert // !binder_delete_delete; eauto with f_equal.
    + by rewrite /= delete_insert_delete delete_idemp.
    + by rewrite /= binder_delete_insert // delete_insert_delete
        !binder_delete_delete delete_idemp.
Qed.
Lemma subst_map_singleton x v e :
  subst_map {[x:=v]} e = subst x v e.
Proof. by rewrite subst_map_insert delete_empty subst_map_empty. Qed.

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.
Lemma subst_map_binder_insert_empty b v e :
  subst_map (binder_insert b v ) e = subst' b v e.
Proof. by rewrite subst_map_binder_insert binder_delete_empty subst_map_empty. Qed.

Lemma subst_map_binder_insert_2 b1 v1 b2 v2 vs e :
  subst_map (binder_insert b1 v1 (binder_insert b2 v2 vs)) e =
  subst' b2 v2 (subst' b1 v1 (subst_map (binder_delete b2 (binder_delete b1 vs)) e)).
Proof.
  destruct b1 as [|s1], b2 as [|s2]=> /=; auto using subst_map_insert.
  rewrite subst_map_insert. destruct (decide (s1 = s2)) as [->|].
  - by rewrite delete_idemp subst_subst delete_insert_delete.
  - by rewrite delete_insert_ne // subst_map_insert subst_subst_ne.
Qed.
Lemma subst_map_binder_insert_2_empty b1 v1 b2 v2 e :
  subst_map (binder_insert b1 v1 (binder_insert b2 v2 )) e =
  subst' b2 v2 (subst' b1 v1 e).
Proof.
  by rewrite subst_map_binder_insert_2 !binder_delete_empty subst_map_empty.
Qed.

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 eX 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.