From iris_logrel.F_mu_ref_conc Require Export context_refinement adequacy.
From iris.algebra Require Import auth frac agree.
From iris.base_logic Require Import big_op lib.auth.
From iris.proofmode Require Import tactics.

Class logrelPreG Σ := LogrelPreG {
  logrel_preG_heap :> heapPreG Σ;
  logrel_preG_cfg  :> inG Σ (authR cfgUR)
}.

Definition logrelΣ : gFunctors := #[heapΣ; authΣ cfgUR].
Instance subG_heapPreG {Σ} : subG logrelΣ Σ → logrelPreG Σ.
Proof. solve_inG. Qed.

Lemma logrel_adequate Σ `{logrelPreG Σ}
    e e' τ σ :
  (∀ `{logrelG Σ}, ∅ ⊨ e ≤log≤ e' : τ) →
  adequate e σ (λ v, ∃ thp' h v', rtc step ([e'], ∅) (of_val v' :: thp', h) 
    ∧ (ObsType τ → v = v')).
Proof.
  intros Hlog.
  eapply (heap_adequacy Σ _); iIntros (Hinv).
  iMod (own_alloc (● (to_tpool [e'], ∅)
    ⋅ ◯ ((to_tpool [e'] : tpoolUR, ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
  { apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. }
  set (Hcfg := LogrelG _ _ _ γc).
  iMod (inv_alloc specN _ (spec_inv ([e'], ∅)) with "[Hcfg1]") as "#Hcfg".
  { iNext. iExists [e'], ∅. 
    rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
  iApply wp_fupd. iApply wp_wand_r.
  iSplitL.
  - iPoseProof (Hlog _) as "Hrel".
    rewrite bin_log_related_eq /bin_log_related_def.
    iSpecialize ("Hrel" $! [] with "[$Hcfg] []").
    { iApply logrel_binary.interp_env_nil. }
    rewrite /env_subst !fmap_empty !subst_p_empty. 
    iApply fupd_wp.
    iApply ("Hrel" $! 0 []). simpl.
    rewrite tpool_mapsto_eq /tpool_mapsto_def. iFrame.
  - iIntros (v1).
    iDestruct 1 as (v2) "[Hj #Hinterp]". 
    iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
    rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
    iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
    move: Hvalid=> /auth_valid_discrete_2
       [/prod_included [/tpool_singleton_included Hv2 _] _].
    destruct tp as [|? tp']; simplify_eq/=.
    iMod ("Hclose" with "[-]") as "_".
    { iExists (_ :: tp'), σ'. eauto. }
    iDestruct (interp_ObsType_agree with "Hinterp") as %Hobs.
    iIntros "!> !%"; eauto.
Qed.


Theorem logrel_typesafety Σ `{logrelPreG Σ} e τ e' thp σ σ' :
  (∀ `{logrelG Σ}, ∅ ⊨ e ≤log≤ e : τ) →
  rtc step ([e], σ) (thp, σ') → e' ∈ thp →
  is_Some (to_val e') ∨ reducible e' σ'.
Proof.
  intros Hlog ??.
  cut (adequate e σ (λ v, ∃ thp' h v', rtc step ([e], ∅) (of_val v' :: thp', h) ∧ (ObsType τ → v = v'))); first (intros [_ ?]; eauto).
  eapply logrel_adequate; eauto.
Qed.

Lemma logrel_simul Σ `{logrelPreG Σ}
    e e' τ v thp hp :
  (∀ `{logrelG Σ}, ∅ ⊨ e ≤log≤ e' : τ) →
  rtc step ([e], ∅) (of_val v :: thp, hp) →
  (∃ thp' hp' v', rtc step ([e'], ∅) (of_val v' :: thp', hp') ∧ (ObsType τ → v = v')).
Proof.
  intros Hlog Hsteps.
  cut (adequate e ∅ (λ v, ∃ thp' h v', rtc step ([e'], ∅) (of_val v' :: thp', h) ∧ (ObsType τ → v = v'))).
  { destruct 1; naive_solver. }
  eapply logrel_adequate; eauto.
Qed.

Lemma logrel_ctxequiv Σ `{logrelPreG Σ} Γ e e' τ :
  Closed (dom _ Γ) e →
  Closed (dom _ Γ) e' →
  (∀ `{logrelG Σ}, Γ ⊨ e ≤log≤ e' : τ) →
  Γ ⊨ e ≤ctx≤ e' : τ.
Proof.
  intros He He' Hlog K thp σ ? τ' ? ? Hstep.
  cut (∃ thp' hp' v', rtc step ([fill_ctx K e'], ∅) (of_val v' :: thp', hp') ∧ (ObsType τ'  → v = v')).
  { naive_solver. }
  eapply (logrel_simul Σ _); last by apply Hstep.
  intros ?.
  iApply (bin_log_related_under_typed_ctx _ _ _ _ ∅); eauto.
  iPoseProof (Hlog _) as "Hrel". auto.
Qed.