Module IdSimClightExtra

Require Import Program.

Require Import Sem SimProg Skeleton Mod ModSem SimMod SimModSem SimSymb SimMem Sound SimSymb.
Require Import Cop Ctypes ClightC.
Require Import AsmC.
Require SimMemInjInvC.
Require Import CoqlibC.
Require Import ValuesC.
Require Import LinkingC.
Require Import MapsC.
Require Import AxiomsC.
Require Import Ord.
Require Import MemoryC.
Require Import SmallstepC.
Require Import Events.
Require Import Preservation.
Require Import Integers.
Require Import LocationsC Conventions.
Require Import Conventions1C.

Require Import AsmregsC.
Require Import MatchSimModSem.
Require Import StoreArguments.
Require Import AsmStepInj IntegersC.
Require Import Coq.Logic.PropExtensionality.
Require Import AsmExtra IdSimExtra IdSimAsmExtra IdSimInvExtra.

Require Import MatchSimModSem.
Require Import Conventions1C.

Require Import ClightStepInj.
Require Import IdSimExtra IdSimInvExtra.
Require Import mktac.

Set Implicit Arguments.

Local Opaque Z.mul Z.add Z.sub Z.div.

Lemma val_casted_inject val0 val1 j ty
      (VAL: Val.inject j val0 val1)
      (CAST: val_casted val0 ty):
    val_casted val1 ty.
Proof.
  inv CAST; inv VAL; clarify; try econs; eauto.
Qed.

Require Import CtypingC.
Require Import CopC.

Lemma typecheck_inject vals0 vals1 j ty
      (VALS: Val.inject_list j vals0 vals1)
      (TYP: typecheck vals0 ty):
    typecheck vals1 ty.
Proof.
  inv TYP. econs; eauto. clear - VALS TYP0.
  revert vals1 VALS TYP0. generalize (typelist_to_listtype ty).
  clear ty. induction vals0; ss; i; inv VALS; inv TYP0; econs.
  - eapply val_casted_inject; eauto.
  - eapply IHvals0; eauto.
Qed.

Lemma wt_retval_inject j v_src v_tgt ty
      (INJ: Val.inject j v_src v_tgt)
      (TYP: wt_retval v_tgt ty):
    wt_retval v_src ty.
Proof.
  inv TYP; inv WTV; inv INJ; clarify; try by repeat (econs; eauto).
  exploit NVOID; eauto. clarify.
Qed.

Lemma typify_c_inject j retv_src retv_tgt tres tv_src
      (TYP: typify_c retv_src tres tv_src)
      (INJ: Val.inject j retv_src retv_tgt):
    exists tv_tgt,
      (<<TYP: typify_c retv_tgt tres tv_tgt>>) /\
      (<<INJ: Val.inject j tv_src tv_tgt>>).
Proof.
  inv TYP.
  - destruct (classic (wt_retval retv_tgt tres)).
    + esplits; eauto. econs; eauto.
    + exists Vundef. esplits; eauto.
      * econs 2. eauto.
      * assert (tv_src = Vundef); clarify; eauto.
        inv INJ; inv WT; inv WTV; clarify;
          exfalso; eapply H; econs; clarify; try (econs; eauto).
        exploit NVOID; eauto. clarify.
  - exists Vundef. esplits; eauto. econs 2. ii. exploit wt_retval_inject; eauto.
Qed.

Lemma vals_casted_inject j vals_src vals_tgt tys
      (VALS: Val.inject_list j vals_src vals_tgt)
      (TYP: Forall2 val_casted vals_src tys):
    Forall2 val_casted vals_tgt tys.
Proof.
  ginduction vals_src; i.
  - inv VALS. inv TYP. econs.
  - inv VALS. inv TYP. econs; eauto. eapply val_casted_inject; eauto.
Qed.

Definition cgenv skenv_link clight :=
  Build_genv
    (SkEnv.revive (SkEnv.project skenv_link (CtypesC.CSk.of_program signature_of_function clight)) clight)
    (prog_comp_env clight).