Module JunkBlock

Require Import CoqlibC Maps.
Require Import ASTC Integers ValuesC EventsC MemoryC Globalenvs.
Require Import Op Registers.
Require Import sflib.
Require Import SmallstepC.

Set Implicit Arguments.



Fixpoint assign_junk_blocks (m0: mem) (n: nat): mem :=
  match n with
  | O => m0
  | S n' => let (m1, _) := Mem.alloc m0 0%Z 0%Z in assign_junk_blocks m1 n'
  end.

Definition is_junk_value (m0 m1: mem) (v: val): Prop :=
  match v with
  | Vptr blk _ => ~ Mem.valid_block m0 blk /\ Mem.valid_block m1 blk
  | _ => True
  end.



Section PROPS.

  Lemma assign_junk_blocks_perm: forall m0 n,
    <<EQ: Mem.perm (assign_junk_blocks m0 n) = Mem.perm m0>>.
Proof.
    i. repeat (apply func_ext1; i). apply AxiomsC.prop_ext.
    ginduction n; ii; ss. des_ifs. split; i; cycle 1.
    - erewrite IHn. eauto with mem.
    - erewrite IHn in H. destruct (peq x0 b).
      { clarify. exploit Mem.perm_alloc_3; eauto. xomega. }
      eapply Mem.perm_alloc_4; eauto.
  Qed.

  Lemma assign_junk_blocks_nextblock: forall m0 n,
    <<NB: (Mem.nextblock (assign_junk_blocks m0 n) = if Zerob.zerob n then Mem.nextblock m0 else Mem.nextblock m0 + Pos.of_nat n)%positive>>.
Proof.
    i. unfold NW. ginduction n; ii; ss. des_ifs_safe.
    erewrite IHn; eauto. erewrite Mem.nextblock_alloc; eauto. rewrite ! Pplus_one_succ_r; ss.
    des_ifs; try xomega. rewrite <- Pos.add_assoc. rewrite Pos.add_comm with (p := 1%positive). ss.
  Qed.

  Lemma assign_junk_blocks_nextblock'
        m0 n
        (NZR: n <> O):
    <<NB: (Mem.nextblock (assign_junk_blocks m0 n) = Mem.nextblock m0 + Pos.of_nat n)%positive>>.
Proof.
rewrite assign_junk_blocks_nextblock. destruct n; ss. Qed.

  Lemma assign_junk_blocks_unchanged_on: forall m0 n,
      <<UNCH: Mem.unchanged_on top2 m0 (assign_junk_blocks m0 n)>>.
Proof.
    i. ginduction n; ii; ss.
    { eapply Mem.unchanged_on_refl; eauto. }
    des_ifs. r. etrans; cycle 1.
    { eapply IHn; eauto. }
    eapply Mem.alloc_unchanged_on; eauto.
  Qed.

  Lemma assign_junk_blocks_load
        m0 chunk n blk ofs
        (VALID: Mem.valid_block m0 blk):
      Mem.load chunk (assign_junk_blocks m0 n) blk ofs = Mem.load chunk m0 blk ofs.
Proof.
    ginduction n; ii; ss. des_ifs. erewrite IHn; eauto with mem. repeat (apply func_ext1; i).
    eapply Mem.load_alloc_unchanged; eauto.
  Qed.

  Lemma assign_junk_block_extends
        m_src m_tgt
        (EXT: Mem.extends m_src m_tgt):
      forall n, <<EXT: Mem.extends (assign_junk_blocks m_src n) (assign_junk_blocks m_tgt n)>>.
Proof.
    i. ginduction n; ii; ss. des_ifs. eapply IHn.
    exploit (Mem.alloc_extends m_src m_tgt 0 0 b m 0 0); eauto; try lia. i; des. rewrite H in *. clarify.
  Qed.

End PROPS.