(*
 * 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 (SenLocal -- InsenLocal *)

Set Implicit Arguments.

Require Import vgtac.
Require Import Global.
Require SemSenLocal SemInsenLocal ExtInsenLocal.
Require Import UserProofType.

Module Make (Import PInput : PINPUT).

Module SenLocal := SemSenLocal.Make PInput.

Module InsenLocal := SemInsenLocal.Make PInput.

Module EInsenLocal := ExtInsenLocal.Make PInput.

Section correctness.

Variables (g : G.t) (amap : access_map)
          (s : InsenLocal.state_t)
          (Hpostfix : InsenLocal.postfix g amap s)
          (Hamap : InsenLocal.sound_amap g amap s).

Definition sen_s (sen_idx : SenLocal.index_t) :=
  let '(n, pos, _) := sen_idx in
  s (n, pos).

Lemma cor_cmd : forall cn calls, SenLocal.postfix_cmd g cn calls sen_s.
Proof. i. decompose [and] (Hpostfix cn). unfold sen_s. by auto. Qed.

Lemma cor_intra_edge :
  forall cn calls, SenLocal.postfix_intra_edge g cn calls sen_s.
Proof. i. decompose [and] (Hpostfix cn). unfold sen_s. by auto. Qed.

Lemma cor_intra_call :
  forall cn calls, SenLocal.postfix_intra_call g amap cn calls sen_s.
Proof. i. decompose [and] (Hpostfix cn). unfold sen_s. by auto. Qed.

Lemma cor_inter_call :
  forall cn calls, SenLocal.postfix_inter_call g amap cn calls sen_s.
Proof. i. decompose [and] (Hpostfix cn). unfold sen_s. by auto. Qed.

Lemma cor_inter_ret :
  forall cn calls, SenLocal.postfix_inter_ret g cn calls sen_s.
Proof. i. decompose [and] (Hpostfix cn). unfold sen_s. by auto. Qed.

Definition correctness :
  exists s',
    SenLocal.postfix g amap s'
    /\ SenLocal.sound_amap g amap s'
    /\ EInsenLocal.extends g amap s s'.
Proof.
exists sen_s. split; [|split].
{
unfold SenLocal.postfix. i. repeat split.
- by apply cor_cmd.
- by apply cor_intra_edge.
- by apply cor_intra_call.
- by apply cor_inter_call.
- by apply cor_inter_ret.
}
{
split.
- unfold SenLocal.sound_amap_run. i. by apply Hamap.
- by apply Hamap.
}
{
unfold EInsenLocal.extends, EInsenLocal.extends_mem. i.
by apply Val.eq_refl.
}
Qed.

End correctness.

End Make.