Module LineartypingC

Require Import CoqlibC.
Require Import ASTC.
Require Import Integers.
Require Import ValuesC.
Require Import GlobalenvsC.
Require Import Memory.
Require Import Events.
Require Import Op.
Require Import Machregs.
Require Import LocationsC.
Require Import Conventions.
Require Import LTL.
Require Import Linear.
Require Import sflib.
newly added *
Require Export Lineartyping.
Require SoundTop.
Require Import Preservation.
Require Import ModSem.
Require Import LinearC.

Set Implicit Arguments.



Lemma ls_init_has_type
      ls_init sg vs
      (LEN: length vs = length sg)
      ir fr ofs
      (LOCSET: typify_list vs sg = map (fun p => Locmap.getpair p ls_init) (loc_arguments_64 sg ir fr ofs))
      sl pos ty
      (IN: In (S sl pos ty) (regs_of_rpairs (loc_arguments_64 sg ir fr ofs)))
      (ONES: forall lp, In lp (loc_arguments_64 sg ir fr ofs) -> is_one lp):
    <<TY: Val.has_type (ls_init (S sl pos ty)) ty>>.
Proof.
  remember (loc_arguments_64 sg ir fr ofs) as locs in *.
  Local Opaque Z.add Z.mul Z.sub Z.div.
  Local Opaque loc_arguments_64.
  ginduction locs; ii; ss. destruct vs; ss. destruct sg; ss. clarify. unfold typify_list in *.
  exploit ONES; eauto. i. destruct a; ss. clarify. des; cycle 1.
  - Local Transparent loc_arguments_64.
    ss. des_ifs; eapply IHlocs; eauto.
  - clarify. rewrite <- H3.
    assert(t = ty).
    { clear - Heqlocs. ss. des_ifs. }
    clarify.
    eapply typify_has_type.
Qed.


Section SOUNDNESS.

  Variable prog: program.

  Hypothesis wt_prog:
    forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd.

  Lemma mreg_type_any: forall mr, <<ANY: mreg_type mr = Tany64>>.
Proof.
i. rr. unfold mreg_type. des_ifs. Qed.

  Lemma has_type_any: forall v, <<ANY: Val.has_type v Tany64>>.
Proof.
i. rr. destruct v; ss. Qed.

  Theorem wt_state_local_preservation: forall skenv_link,
      local_preservation (modsem skenv_link prog) (fun _ _ st => wt_state st).
Proof.
    econs; ii; ss; eauto.
    - (* init *)
      inv INIT.
      assert(WTLS: wt_locset ls_init).
      { ii.
        destruct l; ss.
        { rewrite mreg_type_any. apply has_type_any. }
        destruct (classic (In (S sl pos ty) (regs_of_rpairs (loc_arguments (fn_sig fd))))).
        - clear - TYP H. inv TYP.
          abstr (fn_sig fd) sg. abstr (Args.vs args) vs. clear_tac.
          generalize (loc_arguments_one sg). intro ONES.
          destruct sg; ss. unfold loc_arguments in *. ss. des_ifs. clear_tac.
          eapply ls_init_has_type; eauto.
        - erewrite SLOT; eauto.
      }
      econs; ss; eauto. econs; eauto. econs; eauto.
    - inv STEP. eapply step_type_preservation; eauto.
      ii. unfold Genv.find_funct, Genv.find_funct_ptr in *. des_ifs.
      unfold Skeleton.SkEnv.revive in *.
      eapply Genv_map_defs_def in Heq. des. u in MAP. des_ifs_safe. bsimpl.
      esplits. eapply in_prog_defmap; eauto.
    - inv AT; ss. esplits; eauto.
      { rr. esplits; ss; eauto. rr. rewrite Forall_forall. ii; ss. }
      ii. inv AFTER. inv SUST.

      hexploit (loc_result_caller_save sg); eauto. intro RES.
      hexploit (loc_result_one sg); eauto. intro ONE. des.

      econs; eauto.
      + destruct stack; ss. des_ifs. inv WTSTK.
        econs; eauto. unfold undef_outgoing_slots. ii. des_ifs.
      + ii. unfold Locmap.setpair. des_ifs. ss.
        apply wt_setreg; ss; cycle 1.
        { apply wt_undef_caller_save_regs; ss. }
        rewrite mreg_type_any. apply has_type_any.
      + ii. destruct l; ss.
        { rewrite locmap_get_set_loc_result; ss. des_ifs. rewrite AGCS; ss.
          hexploit (parent_locset_after_external stack); et. i; des; clarify. rewrite AFTER.
          (* TODO: we can remove spurious case by strengthening wt_callstack -> *)
          (* we know stack >= 1, because of dummy stack *)
          unfold undef_caller_save_regs. des_ifs.
        }
        { rewrite locmap_get_set_loc_result; ss. rewrite AGCS; ss.
          hexploit (parent_locset_after_external stack); et. i.
          des_ifs; des; clarify; rewrite AFTER; ss.
        }
      + ii. rewrite locmap_get_set_loc_result; ss.
    - inv FINAL. esplits; eauto. ss.
  Unshelve.
    all: ss.
  Qed.

End SOUNDNESS.