Library mcertikos.clib.RealParams

Require Export AuxStateDataType.
Require CalRealPT.
Require Import Constant.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.

Section WithRealParamsOps.

  Context `{real_params_ops : RealParamsOps}.

  Class RealParams
  : Prop :=
    {
      real_valid_mm: MM_valid real_mm real_size;
      real_correct_mm: MM_correct real_mm real_size;
      real_valid_mm_kern: MM_kern real_mm real_size;
      real_valid_mm_size: 0< real_size ≤ Int.max_unsigned;
      real_vmxinfo_range: ∀ vmxinfo_idx, 1 ≤ vmxinfo_idx ≤ 14 → 0 ≤ ZMap.get vmxinfo_idx real_vmxinfo ≤ Int.max_unsigned
    }.

  Section AT_and_NPS.

    Function maxs_at_i (i: Z) (mm: MMTable) : Z :=
      match ZMap.get i mm with
        | MMValid s l _ ⇒ (s + l) / PgSize + 1
        | _ ⇒ 0
      end.

    Fixpoint Calculate_nps (i: nat) (mm: MMTable) (size: Z) : Z :=
      match i with
        | O ⇒ maxs_at_i (Z.of_nat i) mm
        | S k ⇒ let (recnps, newnps) := (Calculate_nps k mm size, maxs_at_i (Z.of_nat (S k)) mm)
                 in if Z_lt_dec recnps newnps then newnps else recnps
      end.

    Definition real_nps := Calculate_nps (Z.to_nat (real_size - 1)) real_mm real_size.

    Fixpoint Calculate_AT (n:nat) (nps: Z) (mm:MMTable) (size:Z) (At: ATable) : ATable :=
      match n with
        | O ⇒ ZMap.set (Z.of_nat n) (ATValid false ATKern) At
        | S k ⇒ if Z_le_dec kern_low (Z.of_nat (S k))
                 then if Z_lt_dec (Z.of_nat (S k)) (Z.min kern_high nps)
                      then if MM_kern_valid_dec mm (Z.of_nat (S k)) size
                           then ZMap.set (Z.of_nat (S k)) (ATValid false ATNorm) (Calculate_AT k nps mm size At)
                           else ZMap.set (Z.of_nat (S k)) (ATValid false ATResv) (Calculate_AT k nps mm size At)
                      else ZMap.set (Z.of_nat (S k)) (ATValid false ATKern) (Calculate_AT k nps mm size At)
                 else ZMap.set (Z.of_nat (S k)) (ATValid false ATKern) (Calculate_AT k nps mm size At)
      end.

    Definition real_AT (AT: ATable) := Calculate_AT (Z.to_nat (real_nps-1)) real_nps real_mm real_size AT.

    Fixpoint Calculate_ATC (n:nat) (nps: Z) (Atc: ATCTable) : ATCTable :=
      match n with
        | O ⇒ ZMap.set (Z.of_nat n) (ATCValid 0) Atc
        | S k ⇒ ZMap.set (Z.of_nat (S k)) (ATCValid 0)
                          (Calculate_ATC k nps Atc)
      end.

    Definition real_ATC (ATc: ATCTable) := Calculate_ATC (Z.to_nat (real_nps-1)) real_nps
                                                         ATc.

    Fixpoint Calculate_LAT (n:nat) (nps: Z) (Atc: LATCTable) : LATCTable :=
      match n with
        | O ⇒ ZMap.set (Z.of_nat n) (LATCValid nil) Atc
        | S k ⇒ ZMap.set (Z.of_nat (S k)) (LATCValid nil)
                          (Calculate_LAT k nps Atc)
      end.

    Definition real_LAT (ATc: LATCTable) := Calculate_LAT (Z.to_nat (real_nps-1)) real_nps ATc.


    Context `{real_params: RealParams}.

    Lemma max_unsigned_val: Int.max_unsigned = 4294967295.
    Proof.
      repeat autounfold; reflexivity.
    Qed.

    Lemma max_signed_val: Int.max_signed = 2147483647.
    Proof.
      repeat autounfold; reflexivity.
    Qed.

    Ltac Caseeq H := generalize H; apply or_ind; clear H.

    Lemma real_nps_range: kern_low ≤ real_nps ≤ maxpage.
    Proof.
      generalize max_unsigned_val; intro muval.
      generalize real_valid_mm_size; intro mmsize.
      generalize real_valid_mm; intro mmvalid.
      generalize real_valid_mm_kern; intro mmkern.
      unfold MM_valid in mmvalid.
      unfold MM_range in mmvalid.
      unfold MM_kern in mmkern.
      unfold MM_kern_range in mmkern.
      unfold MM_kern_valid in mmkern.
      unfold real_nps.
      assert(mmkern´: ∃ i0 s l : Z,
                        0 ≤ i0 < real_size ∧
                        ZMap.get i0 real_mm = MMValid s l MMUsable ∧
                        s ≤ 262143 × 4096 ∧ l + s ≥ 262144 × 4096).
      assert(tmp: 0 ≤ 262143 < kern_low) by omega.
      generalize (mmkern 262143 tmp); intro tmpH.
      simpl in ×.
      assumption.
      clear mmkern.
      replace real_size with (real_size - 1 + 1) in mmvalid, mmkern´ by omega.
      rewrite <- Z2Nat.id with (real_size - 1) in mmvalid, mmkern´; try omega.
      split.
      clear mmvalid.
      induction (Z.to_nat (real_size - 1)).
      rewrite Nat2Z.inj_0 in ×.
      simpl in ×.
      unfold maxs_at_i.
      do 5 (destruct mmkern´ as [? mmkern´]).
      destruct mmkern´.
      replace x with 0 in × by omega.
      rewrite H0.
      assert((x0 + x1) / 4096 ≥ 262144 × 4096 / 4096).
      apply Z_div_ge; omega.
      rewrite Z_div_mult_full in H3; try omega.

      Opaque Z.of_nat.
      simpl.
      destruct (Z_lt_dec (Calculate_nps n real_mm real_size)).
      do 5 (destruct mmkern´ as [? mmkern´]).
      destruct mmkern´.
      assert(icase: x = Z.of_nat (S n) ∨ x ≠ Z.of_nat (S n)) by omega.
      Caseeq icase; intro.
      rewrite H3 in ×.
      unfold maxs_at_i.
      rewrite H0.
      assert((x0 + x1) / 4096 ≥ 262144 × 4096 / 4096).
      apply Z_div_ge; omega.
      rewrite Z_div_mult_full in H4; try omega.
      rewrite Nat2Z.inj_succ in ×.
      unfold Z.succ in ×.
      assert(262144 ≤ Calculate_nps n real_mm real_size).
      apply IHn.
      intros.
      ∃ x, x0, x1.
      split.
      omega.
      auto.
      omega.
      assert(Calculate_nps n real_mm real_size ≥ maxs_at_i (Z.of_nat (S n)) real_mm) by omega.
      do 5 (destruct mmkern´ as [? mmkern´]).
      destruct mmkern´.
      assert(icase: x = Z.of_nat (S n) ∨ x ≠ Z.of_nat (S n)) by omega.
      Caseeq icase; intro.
      rewrite H4 in ×.
      assert(kern_low ≤ maxs_at_i (Z.of_nat (S n)) real_mm).
      unfold maxs_at_i.
      rewrite H1.
      assert((x0 + x1) / 4096 ≥ 262144 × 4096 / 4096).
      apply Z_div_ge; omega.
      rewrite Z_div_mult_full in H5; try omega.
      omega.
      rewrite Nat2Z.inj_succ in ×.
      unfold Z.succ in ×.
      assert(262144 ≤ Calculate_nps n real_mm real_size).
      apply IHn.
      ∃ x, x0, x1.
      split.
      omega.
      auto.
      omega.

      clear mmkern´.
      induction (Z.to_nat (real_size - 1)).
      simpl.
      rewrite Nat2Z.inj_0 in ×.
      simpl in ×.
      unfold maxs_at_i.
      assert(tmp: 0 ≤ 0 < 1) by omega.
      generalize (mmvalid 0 tmp); intro tmpH.
      do 5 (destruct tmpH as [? tmpH]).
      destruct tmpH.
      rewrite H.
      assert((x + x0) / 4096 ≤ 4294967294 / 4096).
      apply Z_div_le; omega.
      change (4294967294 / 4096) with 1048575 in H3.
      omega.

      Opaque Z.of_nat.
      simpl.
      destruct (Z_lt_dec (Calculate_nps n real_mm real_size)).
      assert(Calculate_nps n real_mm real_size ≤ 1048576).
      rewrite Nat2Z.inj_succ in ×.
      unfold Z.succ in ×.
      apply IHn.
      intros.
      apply mmvalid.
      omega.
      assert(tmp: 0 ≤ Z.of_nat (S n) < Z.of_nat (S n) + 1) by omega.
      generalize (mmvalid (Z.of_nat (S n)) tmp); intro tmpH.
      do 5 (destruct tmpH as [? tmpH]).
      destruct tmpH.
      unfold maxs_at_i.
      rewrite H0.
      assert((x + x0) / 4096 ≤ 4294967294 / 4096).
      apply Z_div_le; omega.
      change (4294967294 / 4096) with 1048575 in H4.
      omega.
      apply IHn.
      intros.
      apply mmvalid.
      rewrite Nat2Z.inj_succ in ×.
      unfold Z.succ in ×.
      omega.
    Qed.

    Definition Cal_at_Well (x:Z) :=
      ∀ n m i nps mm size AT,
        0 ≤ i
        → i≤ n ≤ m
        → m - n = x
        → ZMap.get i (Calculate_AT (Z.to_nat n) nps mm size AT)
           = ZMap.get i (Calculate_AT (Z.to_nat (m)) nps mm size AT).

    Lemma cal_at_correct´:
      ∀ x, 0≤ x→ Cal_at_Well x.
    Proof.
      apply natlike_rec2.
      unfold Cal_at_Well.
      intros.
      assert(HP: m = n).
      omega.
      subst m.
      trivial.

      intros.
      unfold Cal_at_Well in ×.
      intros.
      specialize (H0 n (Z.pred m) i nps mm size AT).
      assert(HM: i ≤ n ≤ m-1).
      omega.
      assert(HN: Z.pred m -n = z).
      omega.
      specialize (H0 H1 HM HN).
      rewrite H0.
      unfold Calculate_AT.
      case_eq (Z.to_nat m).
      intros.
      assert(HZM: (Z.to_nat (Z.pred m)) = 0%nat).
      rewrite Z2Nat.inj_pred.
      rewrite H4.
      reflexivity.
      rewrite HZM.
      trivial.
      fold Calculate_AT.

      intros.
      assert(HZM: Z.to_nat (Z.pred m) = n0).
      rewrite Z2Nat.inj_pred.
      rewrite H4; reflexivity.
      rewrite HZM.
      assert(HNOT: i ≠ Z.of_nat (S n0)).
      red.
      rewrite <- H4.
      erewrite Z2Nat.id.
      intros.
      omega.
      omega.

      destruct ( Z_le_dec kern_low (Z.of_nat (S n0))).
      destruct ( Z_lt_dec (Z.of_nat (S n0)) (Z.min kern_high nps)).
      destruct (MM_kern_valid_dec mm (Z.of_nat (S n0)) size).
      erewrite ZMap.gso; trivial.

      erewrite ZMap.gso; trivial.

      erewrite ZMap.gso; trivial.

      erewrite ZMap.gso; trivial.
    Qed.

    Lemma real_at_kern_valid:
      ∀ AT, AT_kern (real_AT AT) real_nps.
    Proof.
      generalize real_nps_range; intro.
      unfold AT_kern.
      intros.
      specialize (cal_at_correct´ (real_nps-1 -i)).
      intros.
      assert(0 ≤ real_nps - 1 - i) by omega.
      unfold real_AT.
      specialize (H1 H2).
      unfold Cal_at_Well in H1.
      specialize (H1 i (real_nps -1) i real_nps real_mm real_size AT).

      destruct H0 as [HH |HH].
      rewrite <- H1; try omega.
      clear H1.
      unfold Calculate_AT.
      case_eq (Z.to_nat i).
      intros.
      assert(HI: i = 0).
      case_eq (Z_eq_dec i 0).
      intros.
      trivial.
      intros.
      assert(HI: 0< i).
      omega.
      specialize (Z2Nat.inj_lt 0 i).
      intros.
      assert(HI1: 0≤0).
      omega.
      assert(HI2:0≤i).
      omega.
      specialize (H3 HI1 HI2).
      inv H3.
      specialize (H4 HI).
      rewrite H0 in H4.
      change (0%nat) with (Z.to_nat 0) in H0.
      apply Z2Nat.inj in H0.
      assumption.
      omega.
      omega.

      subst i.
      rewrite Nat2Z.inj_0.
      apply ZMap.gss.

      fold Calculate_AT.
      intros.
      rewrite <- H0.
      rewrite Z2Nat.id; try omega.
      case_eq (Z_le_dec kern_low i).
      intros.
      omega.
      intros.
      apply ZMap.gss.

      rewrite <- H1; try omega.
      clear H2.
      unfold Calculate_AT.
      case_eq (Z.to_nat i).
      intros.
      specialize (Z2Nat.inj_lt 0 i).
      intros.
      assert(HI1: 0≤0).
      omega.
      assert(HI2:0≤i).
      omega.
      specialize (H2 HI1 HI2).
      inv H2.
      assert(HI: 0< i).
      omega.
      specialize (H3 HI).
      rewrite H0 in H3.
      change (Z.to_nat 0) with 0%nat in H3.
      omega.

      fold Calculate_AT.
      intros.
      rewrite <- H0.
      rewrite Z2Nat.id; try omega.
      case_eq (Z_le_dec kern_low i).
      intros.
      case_eq (Z_lt_dec i (Z.min kern_high real_nps)).
      intros.
      case_eq (Z_le_dec kern_high real_nps).
      intros.
      assert(HP: Z.min kern_high real_nps = kern_high).
      rewrite Z.min_l; trivial.
      omega.

      intros.
      omega.

      intros.
      apply ZMap.gss.

      intros.
      omega.
    Qed.

    Lemma real_at_usr_valid:
      ∀ AT,
        AT_usr (real_AT AT) real_nps.
    Proof.
      generalize real_nps_range; intro.
      unfold AT_usr.
      intros.
      assert(HIN: i < real_nps).
      case_eq (Z_le_dec kern_high real_nps).
      intros.
      rewrite Z.min_l in H0; trivial.
      omega.

      intros.
      rewrite Z.min_r in H0; omega.

      specialize (cal_at_correct´ (real_nps-1 -i)).
      intros.
      assert(HT: 0 ≤ real_nps - 1 - i).
      omega.
      specialize (H1 HT).
      unfold Cal_at_Well in H1.
      specialize (H1 i (real_nps -1) i real_nps real_mm real_size AT).
      unfold real_AT.

      rewrite <- H1; try omega.
      clear H1.
      ∃ false.
      unfold Calculate_AT.
      case_eq (Z.to_nat i).
      intros.
      specialize (Z2Nat.inj_lt 0 i).
      intros.
      assert(HI1: 0≤0).
      omega.
      assert(HI2:0≤i).
      omega.
      specialize (H2 HI1 HI2).
      inv H2.
      assert(HI: 0< i).
      omega.
      specialize (H3 HI).
      rewrite H1 in H3.
      change (Z.to_nat 0) with 0%nat in H3.
      omega.

      fold Calculate_AT.
      intros.
      rewrite <- H1.
      rewrite Z2Nat.id; try omega.
      case_eq (Z_le_dec kern_low i).
      intros.
      case_eq (Z_lt_dec i (Z.min kern_high real_nps)).
      intros.
      destruct (MM_kern_valid_dec real_mm i real_size).
      left. apply ZMap.gss.
      right.
      apply ZMap.gss.

      intros.
      omega.
      intros.
      omega.
    Qed.

    Lemma real_pperm_valid:
      ∀ AT,
        consistent_ppage (real_AT AT) (ZMap.init PGUndef) real_nps.
    Proof.
      unfold consistent_ppage; intros.
      generalize real_nps_range; intro.
      assert(HIN: i < real_nps) by omega.
      assert(HT: 0 ≤ real_nps - 1 - i) by omega.
      specialize (cal_at_correct´ _ HT).
      unfold Cal_at_Well.
      intros HCal.
      specialize (HCal i (real_nps -1) i real_nps real_mm real_size AT).
      unfold real_AT.

      rewrite <- HCal; try omega.
      clear HCal.
      unfold Calculate_AT.
      case_eq (Z.to_nat i); simpl.
      - intros.
        destruct (zeq i 0); subst.
        + change (Z.of_nat 0) with 0.
          rewrite ZMap.gss. rewrite ZMap.gi.
          split; intros.
          elim H2; trivial.
          inv H2.
        + specialize (Z2Nat.inj_lt 0 i).
          intros.
          assert(HI1: 0≤0) by omega.
          assert(HI2: 0≤i) by omega.
          specialize (H2 HI1 HI2).
          rewrite H1 in H2. simpl in H2.
          inv H2. exploit H3. omega.
          intros HF. inv HF.
      - fold Calculate_AT.
        intros.
        rewrite <- H1.
        rewrite Z2Nat.id; try omega.
        rewrite ZMap.gi.
        destruct (Z_le_dec 262144 i);
          [destruct (Z_lt_dec i (Z.min 983040 real_nps))|];
          [destruct (MM_kern_valid_dec real_mm i real_size)| | ];
          rewrite ZMap.gss; split; intros; try (elim H2; trivial; fail); inv H2.
    Qed.

    Definition Cal_lat_Well (x:Z) :=
      ∀ n m i nps AT,
        0 ≤ i
        → i≤ n ≤ m
        → m - n = x
        → ZMap.get i (Calculate_LAT (Z.to_nat n) nps AT)
           = ZMap.get i (Calculate_LAT (Z.to_nat (m)) nps AT).

    Lemma cal_lat_correct´:
      ∀ x, 0≤ x→ Cal_lat_Well x.
    Proof.
      apply natlike_rec2.
      unfold Cal_lat_Well.
      intros.
      assert(HP: m = n).
      omega.
      subst m.
      trivial.

      intros.
      unfold Cal_lat_Well in ×.
      intros.
      specialize (H0 n (Z.pred m) i nps AT).
      assert(HM: i ≤ n ≤ m-1).
      omega.
      assert(HN: Z.pred m -n = z).
      omega.
      specialize (H0 H1 HM HN).
      rewrite H0.
      unfold Calculate_LAT.
      case_eq (Z.to_nat m).
      intros.
      assert(HZM: (Z.to_nat (Z.pred m)) = 0%nat).
      rewrite Z2Nat.inj_pred.
      rewrite H4.
      reflexivity.
      rewrite HZM.
      trivial.
      fold Calculate_LAT.

      intros.
      assert(HZM: Z.to_nat (Z.pred m) = n0).
      rewrite Z2Nat.inj_pred.
      rewrite H4; reflexivity.
      rewrite HZM.
      assert(HNOT: i ≠ Z.of_nat (S n0)).
      red.
      rewrite <- H4.
      erewrite Z2Nat.id.
      intros.
      omega.
      omega.

      erewrite ZMap.gso; trivial.
    Qed.



    Lemma real_LAT_all_valid_false_nil :
        ∀ a v, 0 < v < real_nps →
          ZMap.get v (real_LAT a) = LATCValid nil.
    Proof.
      unfold real_LAT.
      destruct real_nps in |- × at 1 2.
      - intros ? ? [ H0 H1 ].
        contradiction (Z.lt_irrefl _ (Z.lt_trans _ _ _ H0 H1)).
      - generalize dependent p.
        refine (Pos.peano_ind _ _ _).
        {
          intros ? ? [ H0 H1 ].
          rewrite <- Z.le_succ_l in H0.
          contradiction (Zle_not_lt _ _ H0 H1).
        }
        intros.
        rewrite Pos2Z.inj_succ in H0 |- ×.
        change (Z.succ (Z.pos p) - 1) with (Z.pred (Z.succ (Z.pos p))).
        rewrite Z.pred_succ.

        destruct (Z.to_nat (Z.pos p)) eqn:p_to_nat_eq; simpl.
        {
          simpl in p_to_nat_eq.
          destruct (Pos2Nat.is_succ p) as [ n eq_S_n ].
          rewrite eq_S_n in p_to_nat_eq; discriminate p_to_nat_eq.
        }
        rewrite <- p_to_nat_eq.
        rewrite Z2Nat.id; try discriminate.

        destruct (zeq v (Z.pos p)) as [ → |].
        + rewrite ZMap.gss; eexists; reflexivity.
        + change (Z.pos p - 1) with (Z.pred (Z.pos p)) in H.
          rewrite Z2Nat.inj_pred, p_to_nat_eq in H.
          change (pred (S n)) with n in H.
          assert (0 < v < Z.pos p).
          { destruct H0; split; try assumption.
            rewrite Z.lt_succ_r in H1.
            apply Z.lt_eq_cases in H1.
            destruct H1; [ assumption | contradiction ].
          }
          rewrite ZMap.gso; auto.
      - intros ? ? [ H0 H1 ].
        assert (H2 := Z.lt_trans _ _ _ H0 H1).
        discriminate H2.
    Qed.

    Lemma Lreal_at_consistent_lat_domain:
      ∀ p a,
        consistent_lat_domain (CalRealPT.real_pt p) (real_LAT a) real_nps.
    Proof.
      intros ? a ? v_range ?.
      rewrite (real_LAT_all_valid_false_nil a _ v_range).
      intros HF. inv HF. intros. inv H.
    Qed.

    Lemma LATable_nil_real:
      ∀ la a,
        LATCTable_nil la a →
        LATCTable_nil (real_LAT la) a.
    Proof.
      unfold real_LAT.
      generalize (Z.to_nat (real_nps - 1)).
      induction n.
      - simpl. intros.
        eapply LATCTable_nil_gss_nil; eauto.
      - simpl. intros.
        eapply LATCTable_nil_gss_nil; eauto.
    Qed.

  End AT_and_NPS.

End WithRealParamsOps.