Library iris.heap_lang.proofmode

From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export weakestpre.
From iris.heap_lang Require Export wp_tactics heap.
Import uPred.

Ltac wp_strip_later ::= iNext.

Section heap.
Context `{heapG Σ}.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val iPropG heap_lang Σ.
Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)).

Global Instance into_sep_mapsto l q v :
  IntoSep false (l ↦{q} v) (l ↦{q/2} v) (l ↦{q/2} v).
Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed.

Lemma tac_wp_alloc Δ Δ' E i j e v Φ :
  to_val e = Some v
  envs_lookup i Δ = Some (true, heap_ctx) nclose heapN E
  IntoLaterEnvs Δ Δ'
  ( l, Δ'',
    envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ''
    (Δ'' |={E heapN}=>> Φ (LitV (LitLoc l))))
  Δ WP Alloc e @ E {{ Φ }}.
Proof.
  intros ???? . rewrite -wp_alloc //.
  rewrite envs_lookup_relevant_sound //=; simpl.
  apply sep_mono; first auto using relevant_elim.
  rewrite into_later_env_sound. apply later_mono, forall_introl.
  destruct ( l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.

Lemma tac_wp_load Δ Δ' E i k l q v Φ :
  envs_lookup k Δ = Some (true, heap_ctx) nclose heapN E
  IntoLaterEnvs Δ Δ'
  envs_lookup i Δ' = Some (false, l ↦{q} v)%I
  (Δ' |={E heapN}=>> Φ v)
  Δ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
  intros. rewrite -wp_load // envs_lookup_relevant_sound //=; simpl.
  apply sep_mono; first auto using relevant_elim.
  rewrite into_later_env_sound -later_sep_affine_l envs_lookup_split //; simpl.
  rewrite -(affine_affine (l ↦{q} v)).
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_store Δ Δ' Δ'' E i k l v e v' Φ :
  to_val e = Some v'
  envs_lookup k Δ = Some (true, heap_ctx) nclose heapN E
  IntoLaterEnvs Δ Δ'
  envs_lookup i Δ' = Some (false, l v)%I
  envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
  (Δ'' |={E heapN}=>> Φ (LitV LitUnit))
  Δ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
  intros. rewrite -wp_store // envs_lookup_relevant_sound //=; simpl.
  apply sep_mono; first auto using relevant_elim.
  rewrite into_later_env_sound -later_sep_affine_l envs_simple_replace_sound //; simpl.
  rewrite right_id.
  rewrite -(affine_affine (l v)).
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_cas_fail Δ Δ' E i k l q v e1 v1 e2 v2 Φ :
  to_val e1 = Some v1 to_val e2 = Some v2
  envs_lookup k Δ = Some (true, heap_ctx) nclose heapN E
  IntoLaterEnvs Δ Δ'
  envs_lookup i Δ' = Some (false, l ↦{q} v)%I v v1
  (Δ' |={E heapN}=>> Φ (LitV (LitBool false)))
  Δ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
  intros. rewrite -wp_cas_fail // envs_lookup_relevant_sound //=; simpl.
  apply sep_mono; first auto using relevant_elim.
  rewrite into_later_env_sound -later_sep_affine_l envs_lookup_split //; simpl.
  rewrite -(affine_affine (l ↦{q} v)).
  apply later_mono, sep_mono_r, wand_mono; auto.
  by apply affine_intro; first apply _.
Qed.

Lemma tac_wp_cas_suc Δ Δ' Δ'' E i k l v e1 v1 e2 v2 Φ :
  to_val e1 = Some v1 to_val e2 = Some v2
  envs_lookup k Δ = Some (true, heap_ctx) nclose heapN E
  IntoLaterEnvs Δ Δ'
  envs_lookup i Δ' = Some (false, l v)%I v = v1
  envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
  (Δ'' |={E heapN}=>> Φ (LitV (LitBool true)))
  Δ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
  intros; subst.
  rewrite -wp_cas_suc // envs_lookup_relevant_sound //=; simpl.
  apply sep_mono; first auto using relevant_elim.
  rewrite into_later_env_sound -later_sep_affine_l envs_simple_replace_sound //; simpl.
  rewrite right_id.
  rewrite -{1}(affine_affine (l v1)).
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_swap Δ Δ' Δ'' E i k l v e v' Φ :
  to_val e = Some v'
  envs_lookup k Δ = Some (true, heap_ctx) nclose heapN E
  IntoLaterEnvs Δ Δ'
  envs_lookup i Δ' = Some (false, l v)%I
  envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
  (Δ'' |={E heapN}=>> Φ v)
  Δ WP Swap (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
  intros. rewrite -wp_swap // envs_lookup_relevant_sound //=; simpl.
  apply sep_mono; first auto using relevant_elim.
  rewrite into_later_env_sound -later_sep_affine_l envs_simple_replace_sound //; simpl.
  rewrite right_id.
  rewrite -(affine_affine (l v)).
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_fai Δ Δ' Δ'' E i k l k' Φ :
  envs_lookup k Δ = Some (true, heap_ctx) nclose heapN E
  IntoLaterEnvs Δ Δ'
  envs_lookup i Δ' = Some (false, l (LitV $ LitInt k'))%I
  envs_simple_replace i false (Esnoc Enil i (l (LitV $ LitInt (k'+1)))) Δ' = Some Δ''
  (Δ'' |={E heapN}=>> Φ (LitV $ LitInt k'))
  Δ WP FAI (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
  intros. rewrite -wp_fai // envs_lookup_relevant_sound //=; simpl.
  apply sep_mono; first auto using relevant_elim.
  rewrite into_later_env_sound -later_sep_affine_l envs_simple_replace_sound //; simpl.
  rewrite right_id.
  rewrite -(affine_affine (l (LitV $ LitInt k'))).
  by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
  lazymatch goal with
  | |- _ wp ?E ?e ?Qreshape_expr e ltac:(fun K e'
    wp_bind K; iApply lem; try iNext)
  | _fail "wp_apply: not a 'wp'"
  end.

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
  lazymatch goal with
  | |- _ wp ?E ?e ?Q
    first
      [reshape_expr e ltac:(fun K e'
         match eval hnf in e' with Alloc _wp_bind K end)
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
    eapply tac_wp_alloc with _ _ H _;
      [let e' := match goal with |- to_val ?e' = _e' end in
       wp_done || fail "wp_alloc:" e' "not a value"
      |iAssumptionCore || fail "wp_alloc: cannot find heap_ctx"
      |solve_ndisj || fail "wp_alloc: cannot open heap invariant"
      |apply _
      |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
        eexists; split;
          [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
          |wp_finish]]
| _fail "wp_alloc: not a 'wp'"
  end.

Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.

Tactic Notation "wp_load" :=
  lazymatch goal with
  | |- _ wp ?E ?e ?Q
    first
      [reshape_expr e ltac:(fun K e'
         match eval hnf in e' with Load _wp_bind K end)
      |fail 1 "wp_load: cannot find 'Load' in" e];
    eapply tac_wp_load;
      [iAssumptionCore || fail "wp_load: cannot find heap_ctx"
      |solve_ndisj || fail "wp_load: cannot open heap invariant"
      |apply _
      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I)l end in
       iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
      |wp_finish]
  | _fail "wp_load: not a 'wp'"
  end.

Tactic Notation "wp_store" :=
  lazymatch goal with
  | |- _ wp ?E ?e ?Q
    first
      [reshape_expr e ltac:(fun K e'
         match eval hnf in e' with Store _ _wp_bind K end)
      |fail 1 "wp_store: cannot find 'Store' in" e];
    eapply tac_wp_store;
      [let e' := match goal with |- to_val ?e' = _e' end in
       wp_done || fail "wp_store:" e' "not a value"
      |iAssumptionCore || fail "wp_store: cannot find heap_ctx"
      |solve_ndisj || fail "wp_store: cannot open heap invariant"
      |apply _
      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I)l end in
       iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
      |env_cbv; reflexivity
      |wp_finish]
  | _fail "wp_store: not a 'wp'"
  end.

Tactic Notation "wp_cas_fail" :=
  lazymatch goal with
  | |- _ wp ?E ?e ?Q
    first
      [reshape_expr e ltac:(fun K e'
         match eval hnf in e' with CAS _ _ _wp_bind K end)
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
    eapply tac_wp_cas_fail;
      [let e' := match goal with |- to_val ?e' = _e' end in
       wp_done || fail "wp_cas_fail:" e' "not a value"
      |let e' := match goal with |- to_val ?e' = _e' end in
       wp_done || fail "wp_cas_fail:" e' "not a value"
      |iAssumptionCore || fail "wp_cas_fail: cannot find heap_ctx"
      |solve_ndisj || fail "wp_cas_fail: cannot open heap invariant"
      |apply _
      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I)l end in
       iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
      |try congruence
      |wp_finish]
  | _fail "wp_cas_fail: not a 'wp'"
  end.

Tactic Notation "wp_cas_suc" :=
  lazymatch goal with
  | |- _ wp ?E ?e ?Q
    first
      [reshape_expr e ltac:(fun K e'
         match eval hnf in e' with CAS _ _ _wp_bind K end)
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
    eapply tac_wp_cas_suc;
      [let e' := match goal with |- to_val ?e' = _e' end in
       wp_done || fail "wp_cas_suc:" e' "not a value"
      |let e' := match goal with |- to_val ?e' = _e' end in
       wp_done || fail "wp_cas_suc:" e' "not a value"
      |iAssumptionCore || fail "wp_cas_suc: cannot find heap_ctx"
      |solve_ndisj || fail "wp_cas_suc: cannot open heap invariant"
      |apply _
      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I)l end in
       iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
      |try congruence
      |env_cbv; reflexivity
      |wp_finish]
  | _fail "wp_cas_suc: not a 'wp'"
  end.

Tactic Notation "wp_swap" :=
  lazymatch goal with
  | |- _ wp ?E ?e ?Q
    first
      [reshape_expr e ltac:(fun K e'
         match eval hnf in e' with Swap _ _wp_bind K end)
      |fail 1 "wp_store: cannot find 'Swap' in" e];
    eapply tac_wp_swap;
      [let e' := match goal with |- to_val ?e' = _e' end in
       wp_done || fail "wp_store:" e' "not a value"
      |iAssumptionCore || fail "wp_swap: cannot find heap_ctx"
      |solve_ndisj || fail "wp_swap: cannot open heap invariant"
      |apply _
      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I)l end in
       iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
      |env_cbv; reflexivity
      |wp_finish]
  | _fail "wp_store: not a 'wp'"
  end.

Tactic Notation "wp_fai" :=
  lazymatch goal with
  | |- _ wp ?E ?e ?Q
    first
      [reshape_expr e ltac:(fun K e'
         match eval hnf in e' with FAI _wp_bind K end)
      |fail 1 "wp_store: cannot find 'Swap' in" e];
    eapply tac_wp_fai;
      [ iAssumptionCore || fail "wp_swap: cannot find heap_ctx"
      |solve_ndisj || fail "wp_swap: cannot open heap invariant"
      |apply _
      |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I)l end in
       iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
      |env_cbv; reflexivity
      |wp_finish]
  | _fail "wp_store: not a 'wp'"
  end.