Library mcertikos.clib.CalRealPTB

***********************************************************************
*                                                                     *
*            The CertiKOS Certified Kit Operating System              *
*                                                                     *
*                   The FLINT Group, Yale University                  *
*                                                                     *
*  Copyright The FLINT Group, Yale University.  All rights reserved.  *
*  This file is distributed under the terms of the Yale University    *
*  Non-Commercial License Agreement.                                  *
*                                                                     *
*********************************************************************** 

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

Section Real_PTB.

  Opaque Z.of_nat Z.to_nat.

  Fixpoint Calculate_pb (i: nat) (pb: PTBitMap) : PTBitMap :=
    match i with
      | O ⇒ ZMap.set 0 PTTrue pb
      | S O ⇒ ZMap.set 1 PTFalse (ZMap.set 0 PTTrue pb)
      | S k ⇒ ZMap.set (Z.of_nat (S k)) PTFalse (Calculate_pb k pb)
    end.

  Definition real_ptb (pb: PTBitMap) := Calculate_pb (Z.to_nat (num_proc - 1)) pb.

  Lemma real_PTB_0_valid: ∀ pb, ZMap.get 0 (real_ptb pb) = PTTrue.
  Proof.
    unfold real_ptb.
    intros.
    induction (Z.to_nat (64 - 1)).
    simpl.
    rewrite ZMap.gss.
    reflexivity.
    simpl.
    destruct n.
    rewrite ZMap.gso; try (intro contra; discriminate contra).
    rewrite ZMap.gss; reflexivity.
    rewrite ZMap.gso.
    assumption.
    rewrite Nat2Z.inj_succ.
    rewrite Nat2Z.inj_succ.
    unfold Z.succ.
    intro contra.
    generalize (Nat2Z.is_nonneg n); intro.
    assert(Z.of_nat n + 1 + 1 ≤ 0).
    rewrite <- contra.
    omega.
    omega.
  Qed.

  Lemma Calculate_pb_false :
    ∀ n i pb, (0 < i ≤ n)%nat → ZMap.get (Z.of_nat i) (Calculate_pb n pb) = PTFalse.
  Proof.
    induction n; intros; try omega.
    destruct (eq_nat_dec i (S n)); subst.
    destruct n; simpl; rewrite ZMap.gss; auto.
    destruct n; simpl.
    assert (∀ i, (0 < i ≤ 1)%nat → i = 1%nat).
    induction i0; intros; try omega.
    destruct i0; try omega.
    inv H0.
    inv H2.
    inv H3.
    apply H0 in H; contradiction.
    rewrite ZMap.gso.
    assert ((0 < i ≤ S n)%nat) by omega.
    apply (IHn _ pb) in H0; simpl in H0; auto.
    intro Hcon; contradict n0.
    apply f_equal with (f := nat_of_Z) in Hcon.
    rewrite 2 nat_of_Z_of_nat in Hcon; auto.
  Qed.

  Lemma real_PTB_non0_valid:
    ∀ i pb, 0 < i < num_id → ZMap.get i (real_ptb pb) = PTFalse.
  Proof.
    unfold real_ptb; intros.
    rewrite <- (nat_of_Z_eq i); try omega.
    apply Calculate_pb_false; simpl; split.
    Print Nat2Z.
    rewrite Nat2Z.inj_lt.
    rewrite nat_of_Z_eq; [|omega].
    rewrite Nat2Z.inj_0; omega.
    rewrite Nat2Z.inj_le.
    rewrite 2 nat_of_Z_eq; omega.
  Qed.

  Lemma real_PTB_valid: ∀ pb, PTB_defined (real_ptb pb) 0 num_proc.
  Proof.
    unfold PTB_defined.
    intros.
    unfold real_ptb.
    assert(ir: 0 ≤ i ≤ 64 - 1) by omega.
    rewrite <- Z2Nat.id with (64 - 1) in ir; try omega.
    induction (Z.to_nat (64 - 1)).
    simpl.
    rewrite Nat2Z.inj_0 in ir.
    replace i with 0 by omega.
    rewrite ZMap.gss.
    intro contra; discriminate contra.
    Opaque Z.of_nat.
    simpl.
    destruct n.
    change (Z.of_nat 1) with 1 in ir.
    assert(icase: i = 0 ∨ i = 1) by omega.
    Caseeq icase; intro; subst.
    rewrite ZMap.gso; try (intro contra; discriminate contra).
    rewrite ZMap.gss.
    intro contra; discriminate contra.
    rewrite ZMap.gss.
    intro contra; discriminate contra.
    rewrite ZMap.gsspec.
    destruct (ZIndexed.eq i (Z.of_nat (S (S n)))).
    intro contra; discriminate contra.
    rewrite Nat2Z.inj_succ in ×.
    rewrite Nat2Z.inj_succ in ×.
    unfold Z.succ in ×.
    apply IHn.
    omega.
  Qed.

  Lemma real_PTB_AC_valid:
    ∀ (pb : PTBitMap) (ac : ContainerPool) i, 0 ≤ i < num_id →
      (∀ i, 0 ≤ i < num_id →
         (ZMap.get i pb = PTTrue ↔ cused (ZMap.get i ac) = true)) →
      (ZMap.get i (real_ptb pb) = PTTrue ↔ cused (ZMap.get i AC_init) = true).
  Proof.
    intros pb ac i; destruct (zeq i 0); subst; simpl.
    rewrite real_PTB_0_valid; split; auto.
    intros; rewrite real_PTB_non0_valid; try omega.
    unfold AC_init; rewrite ZMap.gso; auto.
    rewrite ZMap.gi; simpl; split; intro Hcon; inv Hcon.
  Qed.

End Real_PTB.