(*
 * 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 (Con -- Sen *)

Set Implicit Arguments.

Require Import Global.
Require SemCon SemSen GamSen.
Require Import UserProofType.
Require Import vgtac.

Module Make (Import PInput : PINPUT).

Module Sen := SemSen.Make PInput.

Module GSen := GamSen.Make PInput.

Definition correctness :
  forall (g : G.t)
         s (Hpostfix : Sen.postfix g s),
  forall con_s (Hsem : SemCon.Sem g con_s), GSen.State_g con_s s.
Proof.
i; induction Hsem; simpl GSen.State_g.
{ by apply mem_g_init. }
{
edestruct (Hpostfix cn calls) as [Hpostfix_cmd _]; [by auto|].
eapply mem_g_monotone; [|apply Hpostfix_cmd; by apply Hcmd].
eapply correct_run; by eauto.
}
{
inversion Hrun; i; subst.
- edestruct (Hpostfix (p, n) rets) as [_ [Hpostfix_intra _]]; [by auto|].
  eapply mem_g_monotone; [|apply Hpostfix_intra with cfg; by auto].
  by apply IHHsem.
- edestruct (Hpostfix cn calls) as [_ [_ [Hpostfix_call _]]]; [by auto|].
  eapply mem_g_monotone; [|apply Hpostfix_call; by apply Hsucc].
  by apply IHHsem.
- edestruct (Hpostfix (p, IntraNode.Exit) calls) as [_ [_ [_ Hpostfix_ret]]]
  ; [by inversion Hreach|].
  eapply mem_g_monotone
  ; [|eapply Hpostfix_ret; [reflexivity|by apply Hsucc|by apply Hret]].
  by apply IHHsem.
}
Qed.

End Make.