Library mcertikos.clib.CalRealPT

Require Export AuxStateDataType.
Require Import Constant.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import XOmega.
Require Import CalRealPTPool.
Require Import CLemmas.

Section Real_PT.

  Function Calculate_pt_kern_at_i (i: Z) (ptp: PMapPool) : PMapPool :=
    (ZMap.set 0
              (ZMap.set i PDEID (ZMap.get 0 ptp)) ptp).

  Fixpoint Calculate_pt_kern (i: nat) (ptp: PMapPool) : PMapPool :=
    match i with
      | O ⇒ Calculate_pt_kern_at_i (kern_low / one_k) ptp
      | S k ⇒ Calculate_pt_kern_at_i (Z.of_nat (S k) + kern_low / one_k) (Calculate_pt_kern k ptp)
    end.

  Definition real_pt (ptp: PMapPool) :=
    (Calculate_pt_kern (Z.to_nat ((kern_high - kern_low) / one_k - 1)) (real_ptp ptp)).

  Lemma calculate_pt_kern_at_i_0_PDEID: ∀ i ptp,
    ZMap.get i (ZMap.get 0 (Calculate_pt_kern_at_i i ptp)) = PDEID.
  Proof.
    intros.
    unfold Calculate_pt_kern_at_i.
    rewrite ZMap.gss.
    rewrite ZMap.gss.
    reflexivity.
  Qed.

  Lemma calculate_pt_kern_at_i_0_local: ∀ i j ptp,
    j ≠ i →
      ZMap.get j (ZMap.get 0 (Calculate_pt_kern_at_i i ptp)) =
      ZMap.get j (ZMap.get 0 ptp).
  Proof.
    intros.
    unfold Calculate_pt_kern_at_i.
    rewrite ZMap.gss.
    rewrite ZMap.gso.
    reflexivity.
    assumption.
  Qed.

  Lemma calculate_pt_kern_at_i_local: ∀ i j ptp,
    j ≠ 0 → ZMap.get j (Calculate_pt_kern_at_i i ptp) = ZMap.get j ptp.
  Proof.
    intros.
    unfold Calculate_pt_kern_at_i.
    rewrite ZMap.gso.
    reflexivity.
    assumption.
  Qed.

  Lemma calculate_pt_kern_0_PDEID: ∀ i j ptp,
    kern_low / one_k ≤ j ≤ Z.of_nat i + kern_low/one_k →
      ZMap.get j (ZMap.get 0 (Calculate_pt_kern i ptp)) = PDEID.
  Proof.
    intros.
    induction i.
    {
      simpl.
      assert (j = (262144 / 1024)).
      xomega.
      rewrite H0.
      rewrite calculate_pt_kern_at_i_0_PDEID.
      reflexivity.
    }
    {
      simpl.
      assert ((Z.pos (Pos.of_succ_nat i + 256)) = Z.of_nat (S i) + kern_low / one_k).
      reflexivity.
      rewrite H0.
      destruct (Z.eq_dec j (Z.of_nat (S i) + kern_low / one_k)).
      rewrite <- e.
      rewrite calculate_pt_kern_at_i_0_PDEID.
      reflexivity.
      rewrite calculate_pt_kern_at_i_0_local.
      apply IHi.
      xomega.
      assumption.
    }
  Qed.

  Lemma calculate_pt_kern_0_local: ∀ i j ptp,
    j < kern_low / one_k ∨ j > Z.of_nat i + kern_low/one_k →
      ZMap.get j (ZMap.get 0 (Calculate_pt_kern i ptp)) = ZMap.get j (ZMap.get 0 ptp).
  Proof.
    intros.
    induction i.
    {
      simpl.
      rewrite calculate_pt_kern_at_i_0_local.
      reflexivity.
      destruct (Z.eq_dec j (262144 / 1024)).
      rewrite <- e in H.
      destruct H; simpl in H; xomega.
      assumption.
    }
    {
      simpl.
      replace (Z.pos (Pos.of_succ_nat i + 256)) with (Z.of_nat (S i) + kern_low / one_k).
      rewrite calculate_pt_kern_at_i_0_local.
      apply IHi.
      destruct H.
      left.
      assumption.
      right.
      xomega.
      destruct (Z.eq_dec j (Z.of_nat (S i) + 262144 / 1024)).
      rewrite <- e in H.
      xomega.
      assumption.
      reflexivity.
    }
  Qed.

  Lemma calculate_pt_kern_local: ∀ i j ptp,
    j ≠ 0 → ZMap.get j (Calculate_pt_kern i ptp) = ZMap.get j ptp.
  Proof.
    intros.
    induction i.
    simpl.
    rewrite calculate_pt_kern_at_i_local.
    reflexivity.
    assumption.
    simpl.
    rewrite calculate_pt_kern_at_i_local.
    assumption.
    assumption.
  Qed.

  Lemma real_pt_0_PDEID: ∀ i ptp,
    kern_low/one_k ≤ i < kern_high/one_k →
      ZMap.get i (ZMap.get 0 (real_pt ptp)) = PDEID.
  Proof.
    intros.
    unfold real_pt.
    rewrite calculate_pt_kern_0_PDEID.
    reflexivity.
    xomega.
  Qed.

  Lemma real_pt_0_local: ∀ j ptp,
    j < kern_low / one_k ∨ j ≥ kern_high/one_k →
      ZMap.get j (ZMap.get 0 (real_pt ptp)) = ZMap.get j (ZMap.get 0 (real_ptp ptp)).
  Proof.
    intros.
    unfold real_pt.
    rewrite calculate_pt_kern_0_local.
    reflexivity.
    destruct H.
    left.
    assumption.
    right.
    xomega.
  Qed.

  Lemma real_pt_PMap_common_0: ∀ ptp,
     PMap_common (ZMap.get 0 ((real_pt) ptp)).
  Proof.
    intros.
    unfold PMap_common.
    unfold real_pt.
    intros.
    unfold PDE_kern.
    rewrite calculate_pt_kern_0_local.
    assert (tmp: PMap_common (ZMap.get 0 (real_ptp ptp))).
    apply real_ptp_PMap_common_nonkern.
    xomega.
    unfold PMap_common in tmp.
    unfold PDE_kern in tmp.
    apply tmp.
    assumption.
    unfold PDX.
    replace (i × 4096 / (4096 × 1024)) with (i / 1024).
    destruct H.
    left.
    xomega.
    right.
    xomega.
    xomega.
  Qed.

  Lemma real_pt_nonkern_local: ∀ i ptp, i ≠ 0 →
     ZMap.get i (real_pt ptp) = ZMap.get i (real_ptp ptp).
  Proof.
    intros.
    unfold real_pt.
    rewrite calculate_pt_kern_local.
    reflexivity.
    assumption.
  Qed.

  Lemma real_pt_PMap_common_local:
    ∀ ptp i,
      0 < i < num_proc →
      PMap_common (ZMap.get i (real_pt ptp)).
  Proof.
    intros.
    rewrite real_pt_nonkern_local.
    apply real_ptp_PMap_common_nonkern.
    xomega.
    xomega.
  Qed.

  Lemma real_pt_PMap_valid:
    ∀ ptp i,
      0 ≤ i < num_proc →
      PMap_valid (ZMap.get i (real_pt ptp)).
  Proof.
    intros.
    unfold PMap_valid.
    split.

    {
      destruct (Z.eq_dec i 0).
        rewrite e.
        apply real_pt_PMap_common_0.
        apply real_pt_PMap_common_local.
        xomega.
    }
    {
      destruct (Z.eq_dec i 0).
      {
        rewrite e.
        unfold PMap_usr.
        unfold PDE_usr.
        intros.
        right.
        left.
        rewrite real_pt_0_PDEID.
        reflexivity.
        unfold PDX.
        xomega.
      }
      {
        rewrite real_pt_nonkern_local.
        unfold PMap_usr.
        unfold PDE_usr.
        intros.
        assert (tmp: ZMap.get (PDX (i0 × 4096)) (ZMap.get i (real_ptp ptp)) = PDEUnPresent ∨
   ZMap.get (PDX (i0 × 4096)) (ZMap.get i (real_ptp ptp)) = PDEID).
        apply real_ptp_usr.
        unfold PDX.
        xomega.
        assumption.
        destruct tmp.
        left.
        assumption.
        right.
        left.
        assumption.
        assumption.
      }
    }
  Qed.

  Lemma real_pt_PMap_kern:
    ∀ ptp,
      PMap_kern (ZMap.get 0 (real_pt ptp)).
  Proof.
    unfold PMap_kern.
    unfold PDE_kern.
    intros.
    apply real_pt_0_PDEID.
    unfold PDX.
    xomega.
  Qed.

  Lemma real_pt_consistent_pmap:
    ∀ ptp p a la n,
      consistent_pmap (real_pt ptp) p a la n.
  Proof.
    intros.
    unfold consistent_pmap.
    intros.
    destruct (Z.eq_dec i 0).
    {
      rewrite e in ×.
      destruct (zle_lt (kern_low/one_k) (PDX j) (kern_high/one_k)).
      rewrite real_pt_0_PDEID in H1.
      discriminate H1.
      assumption.
      assert (tmp : ZMap.get (PDX j) (ZMap.get 0 (real_ptp ptp)) = PDEUnPresent ∨
        ZMap.get (PDX j) (ZMap.get 0 (real_ptp ptp)) = PDEID).
      apply real_ptp_usr.
      unfold PDX in ×.
      xomega.
      xomega.
      rewrite real_pt_0_local in H1.
      destruct tmp; rewrite H2 in H1; discriminate H1.
      unfold PDX in ×.
      destruct o.
      left.
      xomega.
      right.
      assumption.
    }
    {
      assert (ZMap.get (PDX j) (ZMap.get i (real_pt ptp)) = PDEUnPresent ∨
        ZMap.get (PDX j) (ZMap.get i (real_pt ptp)) = PDEID).
      rewrite real_pt_nonkern_local.
      apply real_ptp_usr.
      unfold PDX.
      xomega.
      assumption.
      assumption.
      destruct H2; rewrite H2 in H1; discriminate H1.
    }
  Qed.

  Lemma real_pt_consistent_pmap_domain:
    ∀ ptp p a n,
      consistent_pmap_domain (real_pt ptp) p a n.
  Proof.
    intros.
    unfold consistent_pmap_domain.
    intros.
    destruct (Z.eq_dec i 0).
    {
      rewrite e in ×.
      destruct (zle_lt (kern_low/one_k) (PDX j) (kern_high/one_k)).
      rewrite real_pt_0_PDEID in H1.
      discriminate H1.
      assumption.
      assert (tmp : ZMap.get (PDX j) (ZMap.get 0 (real_ptp ptp)) = PDEUnPresent ∨
        ZMap.get (PDX j) (ZMap.get 0 (real_ptp ptp)) = PDEID).
      apply real_ptp_usr.
      unfold PDX in ×.
      xomega.
      xomega.
      rewrite real_pt_0_local in H1.
      destruct tmp; rewrite H3 in H1; discriminate H1.
      unfold PDX in ×.
      destruct o.
      left.
      xomega.
      right.
      assumption.
    }
    {
      assert (ZMap.get (PDX j) (ZMap.get i (real_pt ptp)) = PDEUnPresent ∨
        ZMap.get (PDX j) (ZMap.get i (real_pt ptp)) = PDEID).
      rewrite real_pt_nonkern_local.
      apply real_ptp_usr.
      unfold PDX.
      xomega.
      assumption.
      assumption.
      destruct H3; rewrite H3 in H1; discriminate H1.
    }
  Qed.


End Real_PT.