Library mcertikos.clib.CalRealPTPool
Require Export AuxStateDataType.
Require Import Constant.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import XOmega.
Require Import CLemmas.
Section Real_PTP.
Opaque Z.of_nat Z.to_nat.
Function Calculate_PDE_at_i (i: Z) (index: Z) (ptp: PMapPool) : PMapPool :=
if zle (kern_low / one_k) i then
if zlt i (kern_high / one_k) then
(ZMap.set index (ZMap.set i PDEUnPresent (ZMap.get index ptp)) ptp)
else (ZMap.set index (ZMap.set i PDEID (ZMap.get index ptp)) ptp)
else (ZMap.set index (ZMap.set i PDEID (ZMap.get index ptp)) ptp).
Fixpoint Calculate_PDE (i: nat) (index: Z) (ptp: PMapPool) : PMapPool :=
match i with
| O ⇒ Calculate_PDE_at_i 0 index ptp
| S k ⇒ Calculate_PDE_at_i (Z.of_nat (S k)) index (Calculate_PDE k index ptp)
end.
Function Calculate_pt_comm_at_i (i: Z) (ptp: PMapPool) : PMapPool :=
(Calculate_PDE (Z.to_nat (maxpage / one_k) - 1) i ptp).
Fixpoint Calculate_pt_comm (i: nat) (ptp: PMapPool) : PMapPool :=
match i with
| O ⇒ Calculate_pt_comm_at_i 0 ptp
| S k ⇒ Calculate_pt_comm_at_i (Z.of_nat (S k)) (Calculate_pt_comm k ptp)
end.
Definition real_ptp (ptp: PMapPool) := Calculate_pt_comm (Z.to_nat (num_proc - 1)) ptp.
Lemma calculate_PDE_at_i_local: ∀ i index ptp j,
i ≠ j →
ZMap.get i
(ZMap.get index (Calculate_PDE_at_i j index ptp)) =
ZMap.get i (ZMap.get index ptp).
Proof.
intros.
unfold Calculate_PDE_at_i.
destruct (zle (262144 / 1024) j).
destruct (zlt j (983040/1024)).
{
rewrite ZMap.gss.
rewrite ZMap.gso.
reflexivity.
assumption.
}
{
rewrite ZMap.gss.
rewrite ZMap.gso.
reflexivity.
assumption.
}
{
rewrite ZMap.gss.
rewrite ZMap.gso.
reflexivity.
assumption.
}
Qed.
Lemma calculate_PDE_at_i_local_index: ∀ i index index´ ptp,
index´ ≠ index →
ZMap.get index´ (Calculate_PDE_at_i i index ptp) = ZMap.get index´ ptp.
Proof.
intros.
unfold Calculate_PDE_at_i.
destruct (zle (262144 / 1024) i).
destruct (zlt i (983040 / 1024)).
rewrite ZMap.gso.
reflexivity.
assumption.
rewrite ZMap.gso.
reflexivity.
assumption.
rewrite ZMap.gso.
reflexivity.
assumption.
Qed.
Lemma calculate_PDE_at_i_pmap_common: ∀ i index ptp,
0 ≤ i < kern_low ∨ kern_high ≤ i < maxpage →
PDE_kern (ZMap.get index (Calculate_PDE_at_i (i/one_k) index ptp)) i.
Proof.
intros.
unfold Calculate_PDE_at_i.
destruct H as [H1 | H2].
{
destruct H1.
rewrite zle_false.
rewrite ZMap.gss.
unfold PDE_kern.
unfold PDX.
simpl.
replace (i × 4096 / 4194304) with (i / 1024).
rewrite ZMap.gss.
reflexivity.
xomega.
xomega.
}
{
destruct H2.
rewrite zle_true.
rewrite zlt_false.
rewrite ZMap.gss.
unfold PDE_kern.
unfold PDX.
simpl.
replace (i × 4096 / 4194304) with (i / 1024).
rewrite ZMap.gss.
reflexivity.
xomega.
xomega.
xomega.
}
Qed.
Lemma calculate_PDE_pmap_common: ∀ i j index ptp,
0 ≤ i < kern_low ∨ kern_high ≤ i < maxpage →
i / one_k ≤ Z.of_nat j →
PDE_kern (ZMap.get index (Calculate_PDE j index ptp)) i.
Proof.
intros.
induction j as [|j´ iH].
{
unfold Calculate_PDE.
replace 0 with (i / 1024).
apply calculate_PDE_at_i_pmap_common.
left.
xomega.
xomega.
}
{
simpl.
destruct (Z.eq_dec (i / 1024) (Z.of_nat (S j´))).
{
unfold Calculate_PDE_at_i.
destruct H.
rewrite zle_false.
rewrite ZMap.gss.
unfold PDE_kern.
unfold PDX.
replace (i × 4096 / (4096 × 1024)) with (i / 1024).
rewrite e.
rewrite ZMap.gss.
reflexivity.
xomega.
xomega.
rewrite zle_true.
rewrite zlt_false.
rewrite ZMap.gss.
unfold PDE_kern.
unfold PDX.
replace (i × 4096 / (4096 × 1024)) with (i / 1024).
rewrite e.
rewrite ZMap.gss.
reflexivity.
xomega.
xomega.
xomega.
}
{
unfold PDE_kern.
rewrite calculate_PDE_at_i_local.
unfold PDE_kern in iH.
apply iH.
xomega.
unfold PDX.
replace (i × 4096 / (4096 × 1024)) with (i / 1024).
assumption.
xomega.
}
}
Qed.
Lemma calculate_PDE_comm_local: ∀ i ptp index index´,
index´ ≠ index →
ZMap.get index´ (Calculate_PDE i index ptp) =
ZMap.get index´ ptp.
Proof.
intros.
induction i.
{
simpl.
rewrite calculate_PDE_at_i_local_index.
reflexivity.
assumption.
}
{
simpl.
rewrite calculate_PDE_at_i_local_index.
assumption.
assumption.
}
Qed.
Lemma calculate_pt_comm_at_i_pmap_common: ∀ i ptp,
PMap_common (ZMap.get i (Calculate_pt_comm_at_i i ptp)).
Proof.
unfold Calculate_pt_comm_at_i.
unfold PMap_common.
intros.
apply calculate_PDE_pmap_common.
assumption.
xomega.
Qed.
Lemma calculate_pt_comm_at_i_local: ∀ i j ptp,
i ≠ j →
ZMap.get i (Calculate_pt_comm_at_i j ptp) = ZMap.get i ptp.
Proof.
intros.
unfold Calculate_pt_comm_at_i.
rewrite calculate_PDE_comm_local.
reflexivity.
assumption.
Qed.
Lemma calculate_pt_comm_pmap_common: ∀ i j ptp,
0 ≤ i ≤ (Z.of_nat j) → PMap_common (ZMap.get i (Calculate_pt_comm j ptp)).
Proof.
intros.
induction j.
{
replace i with 0.
apply calculate_pt_comm_at_i_pmap_common.
xomega.
}
{
destruct (Z.eq_dec i (Z.of_nat (S j))).
{
simpl.
rewrite <- e.
apply calculate_pt_comm_at_i_pmap_common.
}
{
simpl.
rewrite calculate_pt_comm_at_i_local.
apply IHj.
xomega.
assumption.
}
}
Qed.
Lemma real_ptp_PMap_common_nonkern: ∀ i ptp,
0 ≤ i < num_proc →
PMap_common (ZMap.get i (real_ptp ptp)).
Proof.
intros.
unfold real_ptp.
apply calculate_pt_comm_pmap_common.
xomega.
Qed.
Lemma calculate_PDE_at_i_UP_or_ID: ∀ i index ptp,
ZMap.get i (ZMap.get index (Calculate_PDE_at_i i index ptp)) = PDEUnPresent ∨
ZMap.get i (ZMap.get index (Calculate_PDE_at_i i index ptp)) = PDEID.
Proof.
intros.
unfold Calculate_PDE_at_i.
destruct (zle (262144 / 1024) i).
destruct (zlt i (983040 / 1024)).
left.
rewrite ZMap.gss.
rewrite ZMap.gss.
reflexivity.
right.
rewrite ZMap.gss.
rewrite ZMap.gss.
reflexivity.
right.
rewrite ZMap.gss.
rewrite ZMap.gss.
reflexivity.
Qed.
Lemma calculate_PDE_UP_or_ID: ∀ i j index ptp,
0 ≤ j ≤ Z.of_nat i →
ZMap.get j (ZMap.get index (Calculate_PDE i index ptp)) = PDEUnPresent ∨
ZMap.get j (ZMap.get index (Calculate_PDE i index ptp)) = PDEID.
Proof.
intros.
induction i.
{
replace j with 0.
apply calculate_PDE_at_i_UP_or_ID.
xomega.
}
{
simpl.
destruct (Z.eq_dec j (Z.of_nat (S i))).
rewrite <- e.
apply calculate_PDE_at_i_UP_or_ID.
rewrite calculate_PDE_at_i_local.
apply IHi.
xomega.
assumption.
}
Qed.
Lemma calculate_pt_comm_at_i_usr: ∀ i j ptp,
0 ≤ j < one_k →
ZMap.get j (ZMap.get i (Calculate_pt_comm_at_i i ptp)) = PDEUnPresent ∨
ZMap.get j (ZMap.get i (Calculate_pt_comm_at_i i ptp)) = PDEID.
Proof.
intros.
apply calculate_PDE_UP_or_ID.
xomega.
Qed.
Lemma calculate_pt_comm_usr: ∀ i j k ptp,
0 ≤ j < one_k → 0 ≤ k ≤ Z.of_nat i →
ZMap.get j (ZMap.get k (Calculate_pt_comm i ptp)) = PDEUnPresent ∨
ZMap.get j (ZMap.get k (Calculate_pt_comm i ptp)) = PDEID.
Proof.
intros.
induction i.
{
replace k with 0.
apply calculate_pt_comm_at_i_usr.
assumption.
xomega.
}
{
destruct (Z.eq_dec k (Z.of_nat (S i))).
simpl.
rewrite <- e.
apply calculate_pt_comm_at_i_usr.
assumption.
simpl.
rewrite calculate_pt_comm_at_i_local.
apply IHi.
xomega.
assumption.
}
Qed.
Lemma real_ptp_usr: ∀ j k ptp,
0 ≤ j < one_k → 0 ≤ k < num_proc →
ZMap.get j (ZMap.get k (real_ptp ptp)) = PDEUnPresent ∨
ZMap.get j (ZMap.get k (real_ptp ptp)) = PDEID.
Proof.
intros.
unfold real_ptp.
apply calculate_pt_comm_usr.
assumption.
xomega.
Qed.
End Real_PTP.
Require Import Constant.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import XOmega.
Require Import CLemmas.
Section Real_PTP.
Opaque Z.of_nat Z.to_nat.
Function Calculate_PDE_at_i (i: Z) (index: Z) (ptp: PMapPool) : PMapPool :=
if zle (kern_low / one_k) i then
if zlt i (kern_high / one_k) then
(ZMap.set index (ZMap.set i PDEUnPresent (ZMap.get index ptp)) ptp)
else (ZMap.set index (ZMap.set i PDEID (ZMap.get index ptp)) ptp)
else (ZMap.set index (ZMap.set i PDEID (ZMap.get index ptp)) ptp).
Fixpoint Calculate_PDE (i: nat) (index: Z) (ptp: PMapPool) : PMapPool :=
match i with
| O ⇒ Calculate_PDE_at_i 0 index ptp
| S k ⇒ Calculate_PDE_at_i (Z.of_nat (S k)) index (Calculate_PDE k index ptp)
end.
Function Calculate_pt_comm_at_i (i: Z) (ptp: PMapPool) : PMapPool :=
(Calculate_PDE (Z.to_nat (maxpage / one_k) - 1) i ptp).
Fixpoint Calculate_pt_comm (i: nat) (ptp: PMapPool) : PMapPool :=
match i with
| O ⇒ Calculate_pt_comm_at_i 0 ptp
| S k ⇒ Calculate_pt_comm_at_i (Z.of_nat (S k)) (Calculate_pt_comm k ptp)
end.
Definition real_ptp (ptp: PMapPool) := Calculate_pt_comm (Z.to_nat (num_proc - 1)) ptp.
Lemma calculate_PDE_at_i_local: ∀ i index ptp j,
i ≠ j →
ZMap.get i
(ZMap.get index (Calculate_PDE_at_i j index ptp)) =
ZMap.get i (ZMap.get index ptp).
Proof.
intros.
unfold Calculate_PDE_at_i.
destruct (zle (262144 / 1024) j).
destruct (zlt j (983040/1024)).
{
rewrite ZMap.gss.
rewrite ZMap.gso.
reflexivity.
assumption.
}
{
rewrite ZMap.gss.
rewrite ZMap.gso.
reflexivity.
assumption.
}
{
rewrite ZMap.gss.
rewrite ZMap.gso.
reflexivity.
assumption.
}
Qed.
Lemma calculate_PDE_at_i_local_index: ∀ i index index´ ptp,
index´ ≠ index →
ZMap.get index´ (Calculate_PDE_at_i i index ptp) = ZMap.get index´ ptp.
Proof.
intros.
unfold Calculate_PDE_at_i.
destruct (zle (262144 / 1024) i).
destruct (zlt i (983040 / 1024)).
rewrite ZMap.gso.
reflexivity.
assumption.
rewrite ZMap.gso.
reflexivity.
assumption.
rewrite ZMap.gso.
reflexivity.
assumption.
Qed.
Lemma calculate_PDE_at_i_pmap_common: ∀ i index ptp,
0 ≤ i < kern_low ∨ kern_high ≤ i < maxpage →
PDE_kern (ZMap.get index (Calculate_PDE_at_i (i/one_k) index ptp)) i.
Proof.
intros.
unfold Calculate_PDE_at_i.
destruct H as [H1 | H2].
{
destruct H1.
rewrite zle_false.
rewrite ZMap.gss.
unfold PDE_kern.
unfold PDX.
simpl.
replace (i × 4096 / 4194304) with (i / 1024).
rewrite ZMap.gss.
reflexivity.
xomega.
xomega.
}
{
destruct H2.
rewrite zle_true.
rewrite zlt_false.
rewrite ZMap.gss.
unfold PDE_kern.
unfold PDX.
simpl.
replace (i × 4096 / 4194304) with (i / 1024).
rewrite ZMap.gss.
reflexivity.
xomega.
xomega.
xomega.
}
Qed.
Lemma calculate_PDE_pmap_common: ∀ i j index ptp,
0 ≤ i < kern_low ∨ kern_high ≤ i < maxpage →
i / one_k ≤ Z.of_nat j →
PDE_kern (ZMap.get index (Calculate_PDE j index ptp)) i.
Proof.
intros.
induction j as [|j´ iH].
{
unfold Calculate_PDE.
replace 0 with (i / 1024).
apply calculate_PDE_at_i_pmap_common.
left.
xomega.
xomega.
}
{
simpl.
destruct (Z.eq_dec (i / 1024) (Z.of_nat (S j´))).
{
unfold Calculate_PDE_at_i.
destruct H.
rewrite zle_false.
rewrite ZMap.gss.
unfold PDE_kern.
unfold PDX.
replace (i × 4096 / (4096 × 1024)) with (i / 1024).
rewrite e.
rewrite ZMap.gss.
reflexivity.
xomega.
xomega.
rewrite zle_true.
rewrite zlt_false.
rewrite ZMap.gss.
unfold PDE_kern.
unfold PDX.
replace (i × 4096 / (4096 × 1024)) with (i / 1024).
rewrite e.
rewrite ZMap.gss.
reflexivity.
xomega.
xomega.
xomega.
}
{
unfold PDE_kern.
rewrite calculate_PDE_at_i_local.
unfold PDE_kern in iH.
apply iH.
xomega.
unfold PDX.
replace (i × 4096 / (4096 × 1024)) with (i / 1024).
assumption.
xomega.
}
}
Qed.
Lemma calculate_PDE_comm_local: ∀ i ptp index index´,
index´ ≠ index →
ZMap.get index´ (Calculate_PDE i index ptp) =
ZMap.get index´ ptp.
Proof.
intros.
induction i.
{
simpl.
rewrite calculate_PDE_at_i_local_index.
reflexivity.
assumption.
}
{
simpl.
rewrite calculate_PDE_at_i_local_index.
assumption.
assumption.
}
Qed.
Lemma calculate_pt_comm_at_i_pmap_common: ∀ i ptp,
PMap_common (ZMap.get i (Calculate_pt_comm_at_i i ptp)).
Proof.
unfold Calculate_pt_comm_at_i.
unfold PMap_common.
intros.
apply calculate_PDE_pmap_common.
assumption.
xomega.
Qed.
Lemma calculate_pt_comm_at_i_local: ∀ i j ptp,
i ≠ j →
ZMap.get i (Calculate_pt_comm_at_i j ptp) = ZMap.get i ptp.
Proof.
intros.
unfold Calculate_pt_comm_at_i.
rewrite calculate_PDE_comm_local.
reflexivity.
assumption.
Qed.
Lemma calculate_pt_comm_pmap_common: ∀ i j ptp,
0 ≤ i ≤ (Z.of_nat j) → PMap_common (ZMap.get i (Calculate_pt_comm j ptp)).
Proof.
intros.
induction j.
{
replace i with 0.
apply calculate_pt_comm_at_i_pmap_common.
xomega.
}
{
destruct (Z.eq_dec i (Z.of_nat (S j))).
{
simpl.
rewrite <- e.
apply calculate_pt_comm_at_i_pmap_common.
}
{
simpl.
rewrite calculate_pt_comm_at_i_local.
apply IHj.
xomega.
assumption.
}
}
Qed.
Lemma real_ptp_PMap_common_nonkern: ∀ i ptp,
0 ≤ i < num_proc →
PMap_common (ZMap.get i (real_ptp ptp)).
Proof.
intros.
unfold real_ptp.
apply calculate_pt_comm_pmap_common.
xomega.
Qed.
Lemma calculate_PDE_at_i_UP_or_ID: ∀ i index ptp,
ZMap.get i (ZMap.get index (Calculate_PDE_at_i i index ptp)) = PDEUnPresent ∨
ZMap.get i (ZMap.get index (Calculate_PDE_at_i i index ptp)) = PDEID.
Proof.
intros.
unfold Calculate_PDE_at_i.
destruct (zle (262144 / 1024) i).
destruct (zlt i (983040 / 1024)).
left.
rewrite ZMap.gss.
rewrite ZMap.gss.
reflexivity.
right.
rewrite ZMap.gss.
rewrite ZMap.gss.
reflexivity.
right.
rewrite ZMap.gss.
rewrite ZMap.gss.
reflexivity.
Qed.
Lemma calculate_PDE_UP_or_ID: ∀ i j index ptp,
0 ≤ j ≤ Z.of_nat i →
ZMap.get j (ZMap.get index (Calculate_PDE i index ptp)) = PDEUnPresent ∨
ZMap.get j (ZMap.get index (Calculate_PDE i index ptp)) = PDEID.
Proof.
intros.
induction i.
{
replace j with 0.
apply calculate_PDE_at_i_UP_or_ID.
xomega.
}
{
simpl.
destruct (Z.eq_dec j (Z.of_nat (S i))).
rewrite <- e.
apply calculate_PDE_at_i_UP_or_ID.
rewrite calculate_PDE_at_i_local.
apply IHi.
xomega.
assumption.
}
Qed.
Lemma calculate_pt_comm_at_i_usr: ∀ i j ptp,
0 ≤ j < one_k →
ZMap.get j (ZMap.get i (Calculate_pt_comm_at_i i ptp)) = PDEUnPresent ∨
ZMap.get j (ZMap.get i (Calculate_pt_comm_at_i i ptp)) = PDEID.
Proof.
intros.
apply calculate_PDE_UP_or_ID.
xomega.
Qed.
Lemma calculate_pt_comm_usr: ∀ i j k ptp,
0 ≤ j < one_k → 0 ≤ k ≤ Z.of_nat i →
ZMap.get j (ZMap.get k (Calculate_pt_comm i ptp)) = PDEUnPresent ∨
ZMap.get j (ZMap.get k (Calculate_pt_comm i ptp)) = PDEID.
Proof.
intros.
induction i.
{
replace k with 0.
apply calculate_pt_comm_at_i_usr.
assumption.
xomega.
}
{
destruct (Z.eq_dec k (Z.of_nat (S i))).
simpl.
rewrite <- e.
apply calculate_pt_comm_at_i_usr.
assumption.
simpl.
rewrite calculate_pt_comm_at_i_local.
apply IHi.
xomega.
assumption.
}
Qed.
Lemma real_ptp_usr: ∀ j k ptp,
0 ≤ j < one_k → 0 ≤ k < num_proc →
ZMap.get j (ZMap.get k (real_ptp ptp)) = PDEUnPresent ∨
ZMap.get j (ZMap.get k (real_ptp ptp)) = PDEID.
Proof.
intros.
unfold real_ptp.
apply calculate_pt_comm_usr.
assumption.
xomega.
Qed.
End Real_PTP.