(*
 * Copyright (c) 2017-present,
 * Programming Research Laboratory (ROPAS), Seoul National University, Korea
 * This software is distributed under the term of the BSD-3 clause license.
 *)
(** * Correctness sub-proof (Sen -- SenLocal *)

Set Implicit Arguments.

Require Import hpattern vgtac Global.
Require SemSen SemSenLocal ExtSenLocal.
Require Import DenSenLocal.
Require Import UserProofType.

Module Make (Import PInput : PINPUT).

Module Sen := SemSen.Make PInput.

Module SenLocal := SemSenLocal.Make PInput.

Module ESenLocal := ExtSenLocal.Make PInput.

Module DSenLocal := DenSenLocal.Make PInput.

Section RunParam.

Variable (g : G.t) (Hg : G.wf g) (amap : access_map).

Let icfg := G.icfg g.

Let mode : UserInputType.update_mode := UserInputType.Strong.

Variable s : Sen.state_t.

Lemma densify_mem_reachables :
  forall ns n pid (Hreachs: InterCfg.reachables icfg (n :: ns) pid)
         (Hamap_reachable: SenLocal.sound_amap_reachable g amap),
    disjoint
      (DSenLocal.densify_mem amap s (InterNode.get_pid n) ns)
      (get_access pid amap).
Proof.
induction ns; s; i.
- by apply disjoint_bot.
- apply disjoint_join.
  + apply disjoint_le with (get_access (InterNode.get_pid n) amap).
    * apply Hamap_reachable. by inversion Hreachs.
    * unfold disjoint. intros l Hacc. by apply Mem.subtract_1.
  + apply IHns; [by inversion Hreachs|by auto].
Qed.

Lemma cor_amap :
  forall cn calls cmd (Hcmd : Some cmd = InterCfg.get_cmd icfg cn)
         (Hr: InterCfg.reachables icfg calls (InterNode.get_pid cn))
         (Hamap_reachable: SenLocal.sound_amap_reachable g amap)
         (Hamap_run: SenLocal.sound_amap_run g amap s),
    disjoint
      (DSenLocal.densify_mem amap s (InterNode.get_pid cn) calls)
      (Acc.get_acc
         (run_access mode g cn cmd (s (cn, SemCommon.Inputof, calls)))).
Proof.
i. apply disjoint_le with (get_access (InterNode.get_pid cn) amap)
   ; [by apply Hamap_run|].
apply densify_mem_reachables; [|by auto]; constructor; [by constructor|by auto].
Qed.

Lemma cor_cmd :
  forall cn calls (Hcmd : SenLocal.postfix_cmd g cn calls s)
         (Hr: InterCfg.reachables icfg calls (InterNode.get_pid cn))
         (Hamap_reachable: SenLocal.sound_amap_reachable g amap)
         (Hamap_run: SenLocal.sound_amap_run g amap s),
    Sen.postfix_cmd g cn calls (DSenLocal.densify_state amap s).
Proof.
unfold SenLocal.postfix_cmd, SenLocal.Sen.postfix_cmd, Sen.postfix_cmd; i.
unfold DSenLocal.densify_state.
eapply Mem.le_trans
; [| apply Mem.join_le
     ; [by apply Hcmd, Hcmd0|by apply Mem.le_refl, Mem.eq_refl]].
do 2 rewrite run_only_access_same. apply Mem.le_refl.
assert (Hcor := run_access_sound g cn cmd). unfold aeqm1 in Hcor.
exploit Hcor; [|intro Hcor'].
- apply cor_amap; [|by apply Hr| |]; by auto.
- match goal with |- context[Acc.get_v ?x] => destruct x end; s.
  match goal with |- context[Acc.get_v ?x] => destruct x end.
  by apply Hcor'.
Qed.

Lemma cor_intra :
  forall cn calls (Hedge : SenLocal.postfix_intra_edge g cn calls s),
    Sen.postfix_intra_edge g cn calls (DSenLocal.densify_state amap s).
Proof.
unfold Sen.postfix_intra_edge, DSenLocal.densify_state; i.
apply Mem.join_le.
- by apply Hedge with (cfg:=cfg).
- apply Mem.le_refl; by apply Mem.eq_refl.
Qed.

Lemma cor_inter_call :
forall cn calls (Hinter : SenLocal.postfix_inter_call g amap cn calls s),
  Sen.postfix_inter_call g cn calls (DSenLocal.densify_state amap s).
Proof.
unfold SenLocal.postfix_inter_call, Sen.postfix_inter_call
; unfold DSenLocal.densify_state; i.
apply Mem.join_lub.
- eapply Mem.le_trans; [apply Mem.le_refl; apply Mem.restrict_subtract_1|].
  apply Mem.join_le; [by apply Hinter|].
  simpl DSenLocal.densify_mem; by apply Mem.join_left.
- simpl DSenLocal.densify_mem.
  eapply Mem.le_trans; [by apply Mem.join_right|].
  by apply Mem.join_right.
Qed.

Lemma cor_inter_ret :
  forall cn calls (Hret : SenLocal.postfix_inter_ret g cn calls s)
         (Hintra : forall cn calls,
                     SenLocal.postfix_intra_call g amap cn calls s),
    Sen.postfix_inter_ret g cn calls (DSenLocal.densify_state amap s).
Proof.
unfold Sen.postfix_inter_ret; i; s.
apply Mem.join_lub.
- eapply Mem.le_trans; [|by apply Mem.join_left].
  by apply Hret with p.
- apply Mem.join_lub.
  + eapply Mem.le_trans; [|by apply Mem.join_left].
    apply Hintra; [|by auto]. subst.
    destruct Hg as [Hg_callof_returnof [_ [Hg_call_edge _]]].
    apply Hg_callof_returnof in Hret0.
    by apply Hg_call_edge with cn'.
  + eapply Mem.le_trans; [|by apply Mem.join_right].
    exploit InterCfg.returnof_same_pid; [apply Hret0 | intro Hpid].
    rewrite Hpid; apply Mem.le_refl; by apply Mem.eq_refl.
Qed.

Lemma correctness :
  forall (Hpostfix : SenLocal.postfix g amap s)
     (Hamap : SenLocal.sound_amap g amap s),
  exists s', Sen.postfix g s' /\ ESenLocal.extends g amap s s'.
Proof.
i; exists (DSenLocal.densify_state amap s); split.
{
unfold SenLocal.postfix in Hpostfix; unfold Sen.postfix; i.
splits.
- apply cor_cmd; [by apply Hpostfix|by auto|by apply Hamap|by apply Hamap].
- apply cor_intra; by apply Hpostfix.
- apply cor_inter_call; by apply Hpostfix.
- apply cor_inter_ret; by apply Hpostfix.
}
{
unfold ESenLocal.extends, ESenLocal.extends_mem. i. s.
eapply Val.eq_trans; [|apply Val.eq_sym; by apply Mem.join_find].
apply Val.le_antisym; [by apply Val.join_left|].
apply Val.join_lub; [apply Val.le_refl; by apply Val.eq_refl|].
apply Val.le_trans with Val.bot; [|by apply Val.bot_prop].
apply Val.le_refl.
assert (disjoint
          (DSenLocal.densify_mem amap s (InterNode.get_pid n) calls)
          (get_access (InterNode.get_pid n) amap))
  as Hdisj.
- apply densify_mem_reachables.
  + constructor; [by constructor|by auto].
  + by apply Hamap.
- by apply Hdisj.
}
Qed.

End RunParam.

End Make.