Module MachExtra

Require Import CoqlibC.
Require Import MemoryC.
Require Import Values.
Require Import Maps.
Require Import Events.
Require Import Globalenvs.
Require Import AST.

Require Import IntegersC SimMemLift SimMemInjC.
Require Import Conventions1.
Require Export SimMemInj.
Require StoreArguments.

Set Implicit Arguments.

Local Opaque Z.mul.

Hint Unfold valid_blocks src_private tgt_private range.

Lemma mach_store_arguments_simmem
      sm0 rs vs sg m_tgt0
      (MWF: SimMem.wf sm0)
      (STORE: StoreArguments.store_arguments sm0.(SimMem.tgt) rs vs sg m_tgt0):
    exists sm1,
    <<SM: sm1 = (mk sm0.(src) m_tgt0 sm0.(inj)
                         sm0.(src_external) sm0.(tgt_external)
                         sm0.(src_parent_nb) sm0.(tgt_parent_nb)
                         sm0.(src_ge_nb) sm0.(tgt_ge_nb))>> /\
    <<MWF: SimMem.wf sm1>> /\
    <<MLE: SimMem.le sm0 sm1>> /\
    <<PRIV: forall ofs (IN: 0 <= ofs < 4 * size_arguments sg),
             sm1.(tgt_private) sm0.(SimMem.tgt).(Mem.nextblock) ofs>>.
Proof.
  i. subst_locals. inv STORE.
  exploit Mem.alloc_right_inject; try apply MWF; eauto. i; des.
  hexpl Mem.alloc_result. clarify.
  hexpl Mem.nextblock_alloc.
  esplits; eauto.
  - econs; ss; try apply MWF; eauto.
    + eapply Mem.inject_extends_compose; eauto. econs; eauto.
      { econs.
        - ii. inv H0. replace (ofs + 0) with ofs by omega.
          destruct (eq_block b2 (Mem.nextblock (tgt sm0))); destruct (zle 0 ofs); destruct (zlt ofs (4 * size_arguments sg));
            try (eapply Mem.perm_unchanged_on; eauto; ss; des_ifs; omega).
          subst b2. exploit (PERM ofs). omega. i. eapply Mem.perm_cur. eapply Mem.perm_implies; eauto. econs.
        - ii. inv H0. eapply Z.divide_0_r.
        - ii. inv H0. replace (ofs + 0) with ofs by omega.
          destruct (eq_block b2 (Mem.nextblock (tgt sm0))); destruct (zle 0 ofs); destruct (zlt ofs (4 * size_arguments sg));
            try (exploit Mem.unchanged_on_contents; eauto; ss; des_ifs; try omega; i; rewrite H0; eapply memval_inject_Reflexive).
          Transparent Mem.alloc. unfold Mem.alloc in ALC. inv ALC. ss.
          rewrite PMap.gss. rewrite ZMap.gi. eapply memval_inject_undef.
      }
      { i. left. assert(Mem.valid_block m1 b).
        { r. rewrite NB. eapply Mem.perm_valid_block; eauto. }
        destruct (eq_block b (Mem.nextblock (tgt sm0))) eqn:BEQ; destruct (zle 0 ofs); destruct (zlt ofs (4 * size_arguments sg));
          try by (eapply Mem.perm_unchanged_on_2; eauto; ss; rewrite BEQ; eauto; try omega).
        subst b. eapply Mem.perm_cur. eapply Mem.perm_implies. eapply Mem.perm_alloc_2; eauto. econs.
      }
    + etransitivity; try apply MWF; eauto. unfold tgt_private. ss. u. ii; des. esplits; eauto with congruence.
      unfold Mem.valid_block in *. rewrite <- NB in *. eauto with xomega.
    + etransitivity; try apply MWF; eauto with mem congruence. rewrite <- NB. lia.
  - econs; ss; try eapply frozen_refl.
    + eauto with mem xomega.
    + inv MWF. etrans.
      { eapply Mem.alloc_unchanged_on; eauto. }
      eapply Mem.unchanged_on_implies; eauto. i. ss. des_ifs. apply TGTEXT in H0. u in H0. des.
      exfalso. eapply Mem.fresh_block_alloc; eauto.
    + ii. eauto with mem xomega.
    + i. r. etrans; cycle 1.
      { ii. eapply Mem.perm_alloc_4; et. }
      { ii. eapply Mem.perm_unchanged_on_2; et.
        - ss. des_ifs. unfold Mem.valid_block in *. xomega.
        - unfold Mem.valid_block in *. xomega.
      }
  - ii. u. esplits; eauto.
    + ii. exploit Mem.mi_perm; try apply MWF; eauto. i.
      zsimpl. hexpl Mem_alloc_fresh_perm. eapply NOPERM; eauto.
    + unfold Mem.valid_block. rewrite <- NB. ss. eauto with xomega.
Qed.