Library iris.heap_lang.lang

From iris.program_logic Require Export ectx_language ectxi_language binders.
From iris.algebra Require Export cofe.
From iris.prelude Require Export strings.
From iris.prelude Require Import gmap.

Module heap_lang.
Open Scope Z_scope.

Expressions and vals.
Definition loc := positive.
Inductive base_lit : Set :=
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
Inductive un_op : Set :=
  | NegOp | MinusUnOp.
Inductive bin_op : Set :=
  | PlusOp | MinusOp | LeOp | LtOp | EqOp.

Inductive expr :=
  
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
  
  | Lit (l : base_lit)
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
  
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
  | Letp (x y : binder) (e1 e2 : expr)
  
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
  
  | Fork (e : expr)
  
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
  
  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
  | Swap (e0 : expr) (e1: expr)
  
  | FAI (e0 : expr).

Bind Scope expr_scope with expr.
Delimit Scope expr_scope with E.
Arguments Rec _ _ _%E.
Arguments App _%E _%E.
Arguments Lit _.
Arguments UnOp _ _%E.
Arguments BinOp _ _%E _%E.
Arguments If _%E _%E _%E.
Arguments Pair _%E _%E.
Arguments Fst _%E.
Arguments Letp _ _ _%E _%E.
Arguments Snd _%E.
Arguments InjL _%E.
Arguments InjR _%E.
Arguments Case _%E _%E _%E.
Arguments Fork _%E.
Arguments Alloc _%E.
Arguments Load _%E.
Arguments Store _%E _%E.
Arguments CAS _%E _%E _%E.
Arguments Swap _%E _%E.
Arguments FAI _%E.

Fixpoint is_closed (X : list string) (e : expr) : bool :=
  match e with
  | Var xbool_decide (x X)
  | Rec f x eis_closed (f :b: x :b: X) e
  | Letp x y e1 e2is_closed X e1 && is_closed (x :b: y :b: X) e2
  | Lit _true
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e | FAI e
     is_closed X e
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | Swap e1 e2
     is_closed X e1 && is_closed X e2
  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2
     is_closed X e0 && is_closed X e1 && is_closed X e2
  end.

Class Closed (X : list string) (e : expr) := closed : is_closed X e.
Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
Proof. rewrite /Closed. apply _. Qed.
Instance closed_decision env e : Decision (Closed env e).
Proof. rewrite /Closed. apply _. Qed.

Inductive val :=
  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
  | LitV (l : base_lit)
  | PairV (v1 v2 : val)
  | InjLV (v : val)
  | InjRV (v : val).

Bind Scope val_scope with val.
Delimit Scope val_scope with V.
Arguments PairV _%V _%V.
Arguments InjLV _%V.
Arguments InjRV _%V.

Fixpoint of_val (v : val) : expr :=
  match v with
  | RecV f x e _Rec f x e
  | LitV lLit l
  | PairV v1 v2Pair (of_val v1) (of_val v2)
  | InjLV vInjL (of_val v)
  | InjRV vInjR (of_val v)
  end.

Fixpoint to_val (e : expr) : option val :=
  match e with
  | Rec f x e
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
  | Lit lSome (LitV l)
  | Pair e1 e2v1 to_val e1; v2 to_val e2; Some (PairV v1 v2)
  | InjL eInjLV <$> to_val e
  | InjR eInjRV <$> to_val e
  | _None
  end.

The state: heaps of vals.
Definition state := gmap loc val.

Evaluation contexts
Inductive ectx_item :=
  | AppLCtx (e2 : expr)
  | AppRCtx (v1 : val)
  | UnOpCtx (op : un_op)
  | BinOpLCtx (op : bin_op) (e2 : expr)
  | BinOpRCtx (op : bin_op) (v1 : val)
  | IfCtx (e1 e2 : expr)
  | PairLCtx (e2 : expr)
  | PairRCtx (v1 : val)
  | FstCtx
  | SndCtx
  | LetpCtx (x y : binder) (eb : expr)
  | InjLCtx
  | InjRCtx
  | CaseCtx (e1 : expr) (e2 : expr)
  | AllocCtx
  | LoadCtx
  | StoreLCtx (e2 : expr)
  | StoreRCtx (v1 : val)
  | CasLCtx (e1 : expr) (e2 : expr)
  | CasMCtx (v0 : val) (e2 : expr)
  | CasRCtx (v0 : val) (v1 : val)
  | SwapLCtx (e2 : expr)
  | SwapRCtx (v1 : val)
  | FaiCtx.

Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
  match Ki with
  | AppLCtx e2App e e2
  | AppRCtx v1App (of_val v1) e
  | UnOpCtx opUnOp op e
  | BinOpLCtx op e2BinOp op e e2
  | BinOpRCtx op v1BinOp op (of_val v1) e
  | IfCtx e1 e2If e e1 e2
  | PairLCtx e2Pair e e2
  | PairRCtx v1Pair (of_val v1) e
  | FstCtxFst e
  | SndCtxSnd e
  | LetpCtx x y ebLetp x y e eb
  | InjLCtxInjL e
  | InjRCtxInjR e
  | CaseCtx e1 e2Case e e1 e2
  | AllocCtxAlloc e
  | LoadCtxLoad e
  | StoreLCtx e2Store e e2
  | StoreRCtx v1Store (of_val v1) e
  | CasLCtx e1 e2CAS e e1 e2
  | CasMCtx v0 e2CAS (of_val v0) e e2
  | CasRCtx v0 v1CAS (of_val v0) (of_val v1) e
  | SwapLCtx e2Swap e e2
  | SwapRCtx v1Swap (of_val v1) e
  | FaiCtxFAI e
  end.

Substitution
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
  match e with
  | Var yif decide (x = y) then es else Var y
  | Rec f y e
     Rec f y $ if decide (BNamed x f BNamed x y) then subst x es e else e
  | App e1 e2App (subst x es e1) (subst x es e2)
  | Lit lLit l
  | UnOp op eUnOp op (subst x es e)
  | BinOp op e1 e2BinOp op (subst x es e1) (subst x es e2)
  | If e0 e1 e2If (subst x es e0) (subst x es e1) (subst x es e2)
  | Pair e1 e2Pair (subst x es e1) (subst x es e2)
  | Fst eFst (subst x es e)
  | Snd eSnd (subst x es e)
  | Letp y z e1 e2
    Letp y z (subst x es e1) $ if decide (BNamed x y BNamed x z) then subst x es e2 else e2
  | InjL eInjL (subst x es e)
  | InjR eInjR (subst x es e)
  | Case e0 e1 e2Case (subst x es e0) (subst x es e1) (subst x es e2)
  | Fork eFork (subst x es e)
  | Alloc eAlloc (subst x es e)
  | Load eLoad (subst x es e)
  | Store e1 e2Store (subst x es e1) (subst x es e2)
  | CAS e0 e1 e2CAS (subst x es e0) (subst x es e1) (subst x es e2)
  | Swap e0 e1Swap (subst x es e0) (subst x es e1)
  | FAI e0FAI (subst x es e0)
  end.

Definition subst' (mx : binder) (es : expr) : expr expr :=
  match mx with BNamed xsubst x es | BAnonid end.

The stepping relation
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
  match op, l with
  | NegOp, LitBool bSome (LitBool (negb b))
  | MinusUnOp, LitInt nSome (LitInt (- n))
  | _, _None
  end.

Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
  match op, l1, l2 with
  | PlusOp, LitInt n1, LitInt n2Some $ LitInt (n1 + n2)
  | MinusOp, LitInt n1, LitInt n2Some $ LitInt (n1 - n2)
  | LeOp, LitInt n1, LitInt n2Some $ LitBool $ bool_decide (n1 n2)
  | LtOp, LitInt n1, LitInt n2Some $ LitBool $ bool_decide (n1 < n2)
  | EqOp, LitInt n1, LitInt n2Some $ LitBool $ bool_decide (n1 = n2)
  | _, _, _None
  end.

Inductive head_step : expr state expr state option (expr) Prop :=
  | BetaS f x e1 e2 v2 e' σ :
     to_val e2 = Some v2
     Closed (f :b: x :b: []) e1
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1)
     head_step (App (Rec f x e1) e2) σ e' σ None
  | UnOpS op l l' σ :
     un_op_eval op l = Some l'
     head_step (UnOp op (Lit l)) σ (Lit l') σ None
  | BinOpS op l1 l2 l' σ :
     bin_op_eval op l1 l2 = Some l'
     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
  | IfTrueS e1 e2 σ :
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
  | IfFalseS e1 e2 σ :
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1 to_val e2 = Some v2
     head_step (Fst (Pair e1 e2)) σ e1 σ None
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1 to_val e2 = Some v2
     head_step (Snd (Pair e1 e2)) σ e2 σ None
  | LetpS x y e1 v1 e2 v2 eb eb' σ:
     to_val e1 = Some v1 to_val e2 = Some v2
     Closed (x :b: y :b: []) eb
     eb' = subst' y (of_val v2) (subst' x (of_val v1) eb)
     head_step (Letp x y (Pair e1 e2) eb) σ eb' σ None
  | CaseLS e0 v0 e1 e2 σ :
     to_val e0 = Some v0
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
  | CaseRS e0 v0 e1 e2 σ :
     to_val e0 = Some v0
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
  | ForkS e σ:
     head_step (Fork e) σ (Lit LitUnit) σ (Some e)
  | AllocS e v σ l :
     to_val e = Some v l = fresh (dom _ σ)
     
     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) None
  | LoadS l v σ :
     σ !! l = Some v
     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ None
  | StoreS l e v σ :
     to_val e = Some v is_Some (σ !! l)
     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1 to_val e2 = Some v2
     σ !! l = Some vl vl v1
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ None
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1 to_val e2 = Some v2
     σ !! l = Some v1
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None
  | SwapS l e1 v1 vl σ :
     to_val e1 = Some v1
     σ !! l = Some vl
     head_step (Swap (Lit $ LitLoc l) e1) σ (of_val vl) (<[l:=v1]>σ) None
  | FaiS l k σ:
     σ !! l = Some (LitV $ LitInt k)
     head_step (FAI (Lit $ LitLoc l)) σ (Lit $ LitInt k) (<[l:=LitV $ LitInt (k+1)]>σ) None.

Basic properties about the language
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof.
  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.

Lemma of_to_val e v : to_val e = Some v of_val v = e.
Proof.
  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
Qed.

Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.

Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.

Lemma fill_item_val Ki e :
  is_Some (to_val (fill_item Ki e)) is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.

Lemma val_stuck e1 σ1 e2 σ2 ef : head_step e1 σ1 e2 σ2 ef to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.

Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
  head_step (fill_item Ki e) σ1 e2 σ2 ef is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.

Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
  to_val e1 = None to_val e2 = None
  fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2.
Proof.
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
    repeat match goal with
    | H : to_val (of_val _) = None |- _by rewrite to_of_val in H
    end; auto.
Qed.

Lemma alloc_fresh e v σ :
  let l := fresh (dom _ σ) in
  to_val e = Some v head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
Proof. by intros; apply AllocS. Qed.

Closed expressions
Lemma is_closed_weaken X Y e : is_closed X e X `included` Y is_closed Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

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

Lemma is_closed_subst X e x es : is_closed 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 is_closed_nil_subst e x es : is_closed [] e subst x es e = e.
Proof. intros. apply is_closed_subst with []; set_solver. Qed.

Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.

Lemma is_closed_perm X X' e: is_closed X e Permutation X X' is_closed X' e.
Proof.
  revert X X'. induction eX X' /=; rewrite ?bool_decide_spec ?andb_trueHclosed Hperm;
                 try set_solver.
  - rewrite -Hperm; eauto.
  - eapply IHe; eauto; rewrite /cons_binder; destruct f, x; eauto.
  - apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
    eapply IHe2; eauto; rewrite /cons_binder; destruct x, y; eauto.
Qed.

Lemma is_closed_subst_remove X e x es:
  is_closed [] es is_closed (x :: X) e is_closed X (subst x es e).
Proof.
  revert X. induction eX /=; rewrite ?bool_decide_spec ?andb_true⇒ ? Hclosed;
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver; try set_solver.
  - eapply is_closed_weaken; eauto. set_solver.
  - eapply IHe; auto. eapply is_closed_perm; eauto.
    rewrite /cons_binder; destruct f, x0; eauto using perm_swap.
      by do 2 rewrite (perm_swap x).
  - destruct f, x0; simpl in ×.
    × exfalso; try naive_solver.
    × case (decide (x = s)).
      ** intros →. eapply is_closed_weaken; set_solver.
      ** intros ?; exfalso; naive_solver.
    × case (decide (x = s)).
      ** intros →. eapply is_closed_weaken; set_solver.
      ** intros ?; exfalso; naive_solver.
    × case (decide (x = s)).
      ** intros →. eapply is_closed_weaken; set_solver.
      ** case (decide (x = s0)).
         *** intros → ?. eapply is_closed_weaken; set_solver.
         *** intros ??; exfalso; naive_solver.
  - apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
    rewrite /cons_binder; destruct x0, y;
    eapply is_closed_perm in H2; eauto using perm_swap.
    by do 2 rewrite //= (perm_swap x).
  - apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
    destruct x0, y; simpl in ×.
    × exfalso; try naive_solver.
    × case (decide (x = s)).
      ** intros →. eapply is_closed_weaken; set_solver.
      ** intros ?; exfalso; naive_solver.
    × case (decide (x = s)).
      ** intros →. eapply is_closed_weaken; set_solver.
      ** intros ?; exfalso; naive_solver.
    × case (decide (x = s)).
      ** intros →. eapply is_closed_weaken; set_solver.
      ** case (decide (x = s0)).
         *** intros → ?. eapply is_closed_weaken; set_solver.
         *** intros ??; exfalso; naive_solver.
Qed.

Lemma is_closed_subst_inv_1 X e x es:
  is_closed [] es is_closed X (subst x es e) is_closed (x :: X) e.
Proof.
  revert X. induction eX /=; rewrite ?bool_decide_spec ?andb_true⇒ ? Hclosed;
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver; try set_solver.
  - eapply (is_closed_perm (x :: f :b: x0 :b: X)); first eapply IHe; eauto.
    rewrite /cons_binder; destruct f, x0; eauto using perm_swap.
      by do 2 rewrite (perm_swap x).
  - destruct f, x0; simpl in *; eapply is_closed_weaken; eauto; set_solver.
  - apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
    eapply (is_closed_perm (x :: x0 :b: y :b: X)); first eapply IHe2; eauto;
    rewrite /cons_binder; destruct x0, y; eauto using perm_swap.
      by do 2 rewrite (perm_swap x).
  - apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
    destruct x0, y; simpl in *; eapply is_closed_weaken; eauto; set_solver.
Qed.

Lemma is_closed_subst_inv_2 X e x es:
  is_closed [] es is_closed (x :: X) (subst x es e) is_closed (x :: X) e.
Proof.
  revert X. induction eX /=; rewrite ?bool_decide_spec ?andb_true⇒ ? Hclosed;
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver; try set_solver.
  - move: Hclosed. rewrite ?bool_decide_spec. auto.
  - eapply (is_closed_perm (x :: f :b: x0 :b: X)); first eapply IHe; eauto using is_closed_perm.
    × eapply is_closed_perm; eauto.
      rewrite /cons_binder; destruct f, x0; simpl in *; eauto using perm_swap.
        by do 2 rewrite (perm_swap x).
    × rewrite /cons_binder; destruct f, x0; simpl in *; eauto using perm_swap.
        by do 2 rewrite (perm_swap x).
  - apply andb_prop_elim in Hclosed as (?&?). apply andb_prop_intro; split; eauto.
    eapply (is_closed_perm (x :: x0 :b: y :b: X)); first eapply IHe2; eauto using is_closed_perm.
    × eapply is_closed_perm; eauto.
      rewrite /cons_binder; destruct x0, y; simpl in *; eauto using perm_swap.
        by do 2 rewrite (perm_swap x).
    × rewrite /cons_binder; destruct x0, y; simpl in *; eauto using perm_swap.
        by do 2 rewrite (perm_swap x).
Qed.

Equality and other typeclass stuff
Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
Proof. solve_decision. Defined.
Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
Proof. solve_decision. Defined.
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
Proof.
 refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.

Instance expr_inhabited : Inhabited (expr) := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).

Ltac existT_eq_elim :=
  (match goal with
            [ H: existT ?x ?e1 = existT ?x ?e2 |- _ ] ⇒
            apply Eqdep_dec.inj_pair2_eq_dec in H; eauto
   end).

Lemma head_step_det e σ e1' σ1' ef1' e2' σ2' ef2':
            head_step e σ e1' σ1' ef1'
            head_step e σ e2' σ2' ef2'
            e1' = e2' σ1' = σ2' ef1' = ef2'.
Proof.
  induction 1; subst;
  inversion 1; subst;
  split_and!; try congruence; auto.
Qed.

Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.
End heap_lang.

Language