Library mcertikos.invariants.INVLemmaContainer

***********************************************************************
*                                                                     *
*            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 Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import Constant.

Require Import AbstractDataType.
Require Import ObjContainer.

Lemma empty_container_valid : Container_valid (ZMap.init Container_unused).
Proof.
  constructor; simpl; intros; try rewrite ZMap.gi in *; simpl; auto; try discriminate.
Qed.

Lemma AC_init_container_valid : Container_valid AC_init.
Proof.
  unfold AC_init; constructor; intros.
  -
    destruct (zeq i 0); subst; try omega.
    rewrite ZMap.gso in H; auto.
    rewrite ZMap.gi in H; inv H.
  -
     destruct (zeq i 0); subst.
     rewrite ZMap.gss; simpl; reflexivity.
     rewrite ZMap.gso in H; auto.
     rewrite ZMap.gi in H; inv H.
  -
    change Integers.Int.max_unsigned with 4294967295.
    destruct (zeq i 0); subst.
    rewrite ZMap.gss; simpl; omega.
    rewrite ZMap.gso in H; auto.
    rewrite ZMap.gi in H; inv H.
  -
    destruct (zeq i 0); subst.
    rewrite ZMap.gss; simpl; omega.
    rewrite ZMap.gso in H; auto.
    rewrite ZMap.gi in H; inv H.
  -
    destruct (zeq i 0); subst.
    rewrite ZMap.gss; simpl; auto.
    rewrite ZMap.gso in H; auto.
    rewrite ZMap.gi in H; inv H.
  -
    destruct (zeq i 0); subst.
    rewrite ZMap.gss; simpl; auto.
    rewrite ZMap.gso in H; auto.
    rewrite ZMap.gi in H; inv H.
  -
    rewrite ZMap.gso in H; auto.
    rewrite ZMap.gi in H; inv H.
  -
    destruct (zeq i 0); subst.
    rewrite ZMap.gss; simpl; auto.
    rewrite ZMap.gso in H; auto.
    rewrite ZMap.gi in H; inv H.
  -
    destruct (zeq i 0); subst.
    rewrite ZMap.gss; simpl; constructor; reflexivity.
    rewrite ZMap.gso in H; auto.
    rewrite ZMap.gi in H; inv H.
  -
    destruct (zeq i 0); subst.
    rewrite ZMap.gss; constructor.
    rewrite ZMap.gso; auto.
    rewrite ZMap.gi; constructor.
Qed.

Lemma split_container_valid i n j adt adt´ :
    Container_valid (AC adt) →
    container_split_spec i n j adt = Some (adt´, j)
    Container_valid (AC adt´).
Proof.
  intros valid_container split_spec.
  destruct valid_container.
  functional inversion split_spec.

  constructor; simpl; intros;
    rename i0 into , _x0 into Hn, _x into Hj,
      H2 into Hj_unused, H3 into Hused, H6 into Hused´; clear H0 H1.
  -
    destruct (zeq j); try subst .
    omega.
    rewrite ZMap.gso in Hused´; auto.
    destruct (zeq i); try subst .
    apply (cvalid_id _ Hused).
    rewrite ZMap.gso in Hused´; auto.
  -
    destruct (zeq j); try subst .
    rewrite ZMap.gss; simpl.
    split; intro Heq.
    subst c; rewrite <- Heq in Hused; rewrite Hj_unused in Hused; inv Hused.
    rewrite Heq in Hj; omega.
    rewrite ZMap.gso; auto.
    destruct (zeq i); try subst .
    rewrite ZMap.gss; simpl; subst c; auto.
    rewrite ZMap.gso; auto.
    rewrite 2 ZMap.gso in Hused´; auto.
  -
    destruct (zeq j); try subst .
    + rewrite ZMap.gss; simpl.
      specialize (cvalid_quota i Hused).
      specialize (cvalid_usage i Hused).
      unfold c in Hn; omega.
    + rewrite ZMap.gso; auto.
      destruct (zeq i); try subst .
      rewrite ZMap.gss; simpl; try omega.
      apply cvalid_quota; assumption.
      rewrite 2 ZMap.gso in Hused´; auto.
      rewrite ZMap.gso; auto.
  -
    destruct (zeq j); try subst .
    rewrite ZMap.gss; simpl; omega.
    rewrite ZMap.gso; auto.
    destruct (zeq i); try subst .
    rewrite ZMap.gss; simpl; split; try omega.
    apply Z.add_nonneg_nonneg; auto; try omega.
    rewrite ZMap.gso in Hused´; auto; rewrite ZMap.gss in Hused´.
    apply cvalid_usage; auto.
    rewrite ZMap.gso; auto.
    rewrite 2 ZMap.gso in Hused´; auto.
  -
    destruct (zeq j); try subst .
    + rewrite ZMap.gss; simpl.
      destruct (zeq i j) as [eq|neq].
      rewrite eq; rewrite ZMap.gss; auto.
      rewrite ZMap.gso; auto; rewrite ZMap.gss; auto.
    + replace (ZMap.get (ZMap.set j child (ZMap.set i cur (AC adt))))
         with (ZMap.get (ZMap.set i cur (AC adt))).
      destruct (zeq i); try subst .
      rewrite ZMap.gss; simpl.
      destruct (zeq (cparent c) j) as [eq1|neq1].
      rewrite eq1; rewrite ZMap.gss; auto.
      rewrite ZMap.gso; auto.
      destruct (zeq (cparent c) i) as [eq2|neq2].
      rewrite eq2; rewrite ZMap.gss; auto.
      rewrite ZMap.gso; auto.
      apply cvalid_parent_used; auto.
      replace (ZMap.get (ZMap.set i cur (AC adt))) with (ZMap.get (AC adt)).
      destruct (zeq (cparent (ZMap.get (AC adt))) j) as [eq1|neq1].
      rewrite eq1; rewrite ZMap.gss; auto.
      rewrite ZMap.gso; auto.
      destruct (zeq (cparent (ZMap.get (AC adt))) i) as [eq2|neq2].
      rewrite eq2; rewrite ZMap.gss; auto.
      rewrite ZMap.gso; auto.
      rewrite 2 ZMap.gso in Hused´; auto; apply cvalid_parent_used.
      rewrite ZMap.gso; auto.
      symmetry; rewrite ZMap.gso; auto.
  -
    destruct (zeq j) as [Heq|Hneq]; try subst .
    rewrite ZMap.gss; simpl; apply Forall_nil.
    rewrite ZMap.gso; auto.
    destruct (zeq i) as [Heq´|Hneq´]; try subst .
    + rewrite ZMap.gso in Hused´; auto.
      rewrite ZMap.gss in Hused´ |- *; simpl.
      apply Forall_cons.
      rewrite ZMap.gss; auto.
      apply Forall_forall; intros k Hin.
      destruct (zeq k j); try subst k.
      rewrite ZMap.gss; auto.
      rewrite ZMap.gso; auto.
      destruct (zeq k i); try subst k.
      rewrite ZMap.gss; auto.
      rewrite ZMap.gso; auto.
      specialize (cvalid_children_used _ Hused).
      rewrite Forall_forall in cvalid_children_used.
      apply (cvalid_children_used k Hin).
    + rewrite 2 ZMap.gso in Hused´; auto.
      rewrite ZMap.gso; auto.
      apply Forall_forall; intros k Hin.
      destruct (zeq k j); try subst k.
      specialize (cvalid_children_used _ Hused´).
      rewrite Forall_forall in cvalid_children_used.
      specialize (cvalid_children_used _ Hin).
      rewrite Hj_unused in cvalid_children_used; inv cvalid_children_used.
      rewrite ZMap.gso; auto.
      specialize (cvalid_children_used _ Hused´).
      rewrite Forall_forall in cvalid_children_used.
      specialize (cvalid_children_used _ Hin).
      destruct (zeq k i); try subst k.
      rewrite ZMap.gss; auto.
      rewrite ZMap.gso; auto.
  -
    rename H7 into Hi´_neq.
    destruct (zeq j) as [Heq|Hneq]; try subst .
    + rewrite ZMap.gss; simpl.
      destruct (zeq i j) as [Heq´|Hneq´].
      subst c; rewrite Heq´ in Hused; rewrite Hj_unused in Hused; inv Hused.
      rewrite ZMap.gso; auto; rewrite ZMap.gss; simpl; auto.
    + rewrite (ZMap.gso _ _ Hneq); auto.
      destruct (zeq i) as [Heq´|Hneq´]; try subst .
      rewrite ZMap.gss; simpl.
      destruct (zeq (cparent c) j) as [Heq1|Hneq1].
      subst c; specialize (cvalid_parent_used i Hused); rewrite Heq1 in cvalid_parent_used.
      rewrite Hj_unused in cvalid_parent_used; inv cvalid_parent_used.
      rewrite ZMap.gso; auto.
      destruct (zeq (cparent c) i) as [Heq2|Hneq2].
      rewrite Heq2; rewrite ZMap.gss; simpl; right.
      specialize (cvalid_parents_child i Hused Hi´_neq).
      subst c; rewrite Heq2 in cvalid_parents_child; auto.
      rewrite ZMap.gso; auto.
      apply cvalid_parents_child; auto.
      rewrite 2 ZMap.gso in Hused´; auto.
      rewrite (ZMap.gso _ _ Hneq´); auto.
      destruct (zeq (cparent (ZMap.get (AC adt))) j) as [Heq1|Hneq1].
      specialize (cvalid_parent_used Hused´); rewrite Heq1 in cvalid_parent_used.
      rewrite Hj_unused in cvalid_parent_used; inv cvalid_parent_used.
      rewrite ZMap.gso; auto.
      destruct (zeq (cparent (ZMap.get (AC adt))) i) as [Heq2|Hneq2].
      rewrite Heq2; rewrite ZMap.gss; simpl; right.
      specialize (cvalid_parents_child Hused´ Hi´_neq); rewrite Heq2 in cvalid_parents_child; auto.
      rewrite ZMap.gso; auto.
  -
    destruct (zeq j) as [Heq|Hneq]; try subst .
    rewrite ZMap.gss; simpl; constructor.
    rewrite ZMap.gso; auto.
    destruct (zeq i) as [Heq´|Hneq´]; try subst .
    + rewrite ZMap.gss; simpl; constructor.
      rewrite ZMap.gss; auto.
      apply Forall_forall; intros k Hin.
      destruct (zeq k j); try subst k.
      rewrite ZMap.gss; auto.
      rewrite ZMap.gso; auto.
      specialize (cvalid_childrens_parent _ Hused).
      rewrite Forall_forall in cvalid_childrens_parent.
      specialize (cvalid_childrens_parent k Hin).
      destruct (zeq k i); try subst k.
      rewrite ZMap.gss; auto.
      rewrite ZMap.gso; auto.
    + rewrite 2 ZMap.gso in Hused´; auto.
      rewrite ZMap.gso; auto.
      apply Forall_forall; intros k Hin.
      destruct (zeq k j); try subst k.
      specialize (cvalid_children_used _ Hused´).
      rewrite Forall_forall in cvalid_children_used.
      specialize (cvalid_children_used _ Hin).
      rewrite Hj_unused in cvalid_children_used; inv cvalid_children_used.
      rewrite ZMap.gso; auto.
      specialize (cvalid_childrens_parent _ Hused´).
      rewrite Forall_forall in cvalid_childrens_parent.
      specialize (cvalid_childrens_parent _ Hin).
      destruct (zeq k i); try subst k.
      rewrite ZMap.gss; auto.
      rewrite ZMap.gso; auto.
  -
    destruct (zeq j) as [Heq|Hneq]; try subst .
    rewrite ZMap.gss; simpl; constructor; reflexivity.
    rewrite ZMap.gso; auto.
    destruct (zeq i) as [Heq´|Hneq´]; try subst .
    + rewrite ZMap.gso in Hused´; auto; rewrite ZMap.gss in Hused´.
      rewrite ZMap.gss; simpl; constructor.
      rewrite ZMap.gss; simpl; omega.
      apply cqb_notin.
      apply cqb_weaken.
      apply cvalid_cqb; auto.
      split; try reflexivity; simpl; subst c.
      specialize (cvalid_usage _ Hused); omega.
      specialize (cvalid_children_used _ Hused).
      rewrite Forall_forall in cvalid_children_used.
      intro Hin; specialize (cvalid_children_used _ Hin).
      rewrite Hj_unused in cvalid_children_used; inv cvalid_children_used.
    + rewrite 2 ZMap.gso in Hused´; auto.
      rewrite ZMap.gso; auto.
      apply cqb_notin.
      apply cqb_weaken.
      apply cvalid_cqb; auto.
      split; try reflexivity; simpl; subst c.
      specialize (cvalid_usage _ Hused); omega.
      specialize (cvalid_children_used _ Hused´).
      rewrite Forall_forall in cvalid_children_used.
      intro Hin; specialize (cvalid_children_used _ Hin).
      rewrite Hj_unused in cvalid_children_used; inv cvalid_children_used.
  -
    destruct (zeq j) as [Heq|Hneq]; try subst .
    rewrite ZMap.gss; simpl; constructor.
    rewrite ZMap.gso; auto.
    destruct (zeq i) as [Heq´|Hneq´]; try subst .
    rewrite ZMap.gss; simpl; constructor.
    specialize (cvalid_children_used _ Hused).
    rewrite Forall_forall in cvalid_children_used.
    intro Hin; specialize (cvalid_children_used _ Hin).
    rewrite Hj_unused in cvalid_children_used; inv cvalid_children_used.
    apply cvalid_nodup; auto.
    rewrite 2 ZMap.gso in Hused´; auto.
    rewrite ZMap.gso; auto.
Qed.

Lemma alloc_container_valid´:
   i (ac: ContainerPool),
    let c := ZMap.get i ac in
    let cur := mkContainer (cquota c) (cusage c + 1) (cparent c)
                           (cchildren c) (cused c) in
    Container_valid ac
    (cusage c <? cquota c) = true
    cused c = true
    Container_valid (ZMap.set i cur ac).
Proof.
  intros. destruct H.
  econstructor; eauto 1; simpl; intros.
  -
    destruct (zeq i0 i); subst.
    rewrite ZMap.gss in H; auto.
    rewrite ZMap.gso in H; auto.
  -
    destruct (zeq i0 i); subst.
    rewrite ZMap.gss in H |- *; simpl.
    subst c; auto.
    rewrite ZMap.gso in H |- *; auto.
  -
    destruct (zeq i0 i); subst.
    rewrite ZMap.gss in *; simpl.
    apply cvalid_quota; auto.
    rewrite ZMap.gso in H |- *; auto.
  -
    destruct (zeq i0 i); subst.
    rewrite ZMap.gss in *; simpl.
    rewrite Z.ltb_lt in H0.
    specialize (cvalid_usage _ H); subst c; omega.
    rewrite ZMap.gso in H |- *; auto.
  -
    destruct (zeq i0 i) as [Heq|Hneq]; subst.
    rewrite ZMap.gss in *; simpl.
    destruct (zeq (cparent c) i) as [Heq´|Hneq´].
    rewrite Heq´; rewrite ZMap.gss; auto.
    subst c; rewrite ZMap.gso; auto.
    rewrite (ZMap.gso _ _ Hneq); auto; simpl.
    destruct (zeq (cparent (ZMap.get i0 ac)) i) as [Heq´´|Hneq´´].
    rewrite Heq´´; rewrite ZMap.gss in *; simpl; auto.
    rewrite ZMap.gso in *; auto.
  -
    apply Forall_forall; intros i´´ Hin.
    destruct (zeq i´´ i); subst.
    rewrite ZMap.gss; simpl; auto.
    rewrite ZMap.gso; auto.
    destruct (zeq i0 i); subst.
    rewrite ZMap.gss in H, Hin; simpl in H, Hin.
    specialize (cvalid_children_used _ H).
    rewrite Forall_forall in cvalid_children_used; auto.
    rewrite ZMap.gso in H, Hin; auto.
    specialize (cvalid_children_used _ H).
    rewrite Forall_forall in cvalid_children_used; auto.
  -
    rename H2 into Hi´_neq.
    destruct (zeq i0 i) as [Heq|Hneq]; subst.
    rewrite ZMap.gss; simpl.
    destruct (zeq (cparent c) i) as [Heq´|Hneq´].
    rewrite Heq´; rewrite ZMap.gss in *; simpl.
    specialize (cvalid_parents_child _ H1 Hi´_neq).
    subst c; rewrite Heq´ in cvalid_parents_child; auto.
    rewrite ZMap.gso; auto.
    specialize (cvalid_parents_child _ H1 Hi´_neq); auto.
    rewrite (ZMap.gso _ _ Hneq) in H |- *; auto.
    destruct (zeq (cparent (ZMap.get i0 ac)) i) as [Heq´´|Hneq´´].
    specialize (cvalid_parents_child _ H Hi´_neq).
    rewrite Heq´´ in cvalid_parents_child; rewrite Heq´´; rewrite ZMap.gss; simpl; auto.
    rewrite ZMap.gso; auto.
  -
    apply Forall_forall; intros i´´ Hin.
    destruct (zeq i´´ i); subst.
    rewrite ZMap.gss; simpl.
    destruct (zeq i0 i); subst.
    rewrite ZMap.gss in H, Hin; simpl in H, Hin.
    specialize (cvalid_childrens_parent _ H).
    rewrite Forall_forall in cvalid_childrens_parent; subst c; auto.
    rewrite ZMap.gso in H, Hin; auto.
    specialize (cvalid_childrens_parent _ H).
    rewrite Forall_forall in cvalid_childrens_parent; subst c; auto.
    rewrite ZMap.gso; auto.
    destruct (zeq i0 i); subst.
    rewrite ZMap.gss in H, Hin; simpl in H, Hin.
    specialize (cvalid_childrens_parent _ H).
    rewrite Forall_forall in cvalid_childrens_parent; subst c; auto.
    rewrite ZMap.gso in H, Hin; auto.
    specialize (cvalid_childrens_parent _ H).
    rewrite Forall_forall in cvalid_childrens_parent; subst c; auto.
  -
    apply cqb_weaken; simpl.
    destruct (zeq i0 i); subst.
    rewrite ZMap.gss; simpl.
    apply cqb_bound with (n1 := cusage c); try omega.
    subst c; auto.
    rewrite ZMap.gso in H |- *; auto.
    specialize (cvalid_usage _ H1); subst c; omega.
  -
    destruct (zeq i0 i); subst.
    rewrite ZMap.gss; simpl; subst c; auto.
    rewrite ZMap.gso in H |- *; auto.
Qed.

Lemma alloc_container_valid i adt adt´ z :
    Container_valid (AC adt) →
    container_alloc_spec i adt = Some (adt´,z)
    Container_valid (AC adt´).
Proof.
  intros. functional inversion H0.
  eapply alloc_container_valid´; eauto.
  subst. assumption.
Qed.

Lemma container_split_some :
   d i q j,
    ( i : Z, 0 i < num_id
       (ZMap.get i (pb d) = PTTrue cused (ZMap.get i (AC d)) = true)) →
    ikern d = trueihost d = truecused (ZMap.get i (AC d)) = true
    ZMap.get j (pb d) PTTrue → 0 < j < num_id
    0 q cquota (ZMap.get i (AC d)) - cusage (ZMap.get i (AC d)) →
    container_split_spec i q j d =
    Some (d {AC: ZMap.set j (mkContainer q 0 i nil true)
              (ZMap.set i (mkContainer (cquota (ZMap.get i (AC d)))
                                       (cusage (ZMap.get i (AC d)) + q)
                                       (cparent (ZMap.get i (AC d)))
                                       (j :: cchildren (ZMap.get i (AC d)))
                                       (cused (ZMap.get i (AC d)))) (AC d))}, j).
Proof.
  unfold container_split_spec; intros.
  rewrite H0, H1, H2.
  rewrite H in H3; try omega.
  destruct (cused (ZMap.get j (AC d))); try solve [contradict H3; auto].
  destruct (zlt_lt 0 j num_id); try omega.
  destruct (zle_le 0 q (cquota (ZMap.get i (AC d)) - cusage (ZMap.get i (AC d)))); try omega; auto.
Qed.

Lemma container_split_PTB_AC_valid :
   d i q j id,
    ( i : Z,
       0 i < num_id
       (ZMap.get i (pb d) = PTTrue cused (ZMap.get i (AC d)) = true)) →
    cused (ZMap.get i (AC d)) = true → 0 id < num_id
    (ZMap.get id (ZMap.set j PTTrue (pb d)) = PTTrue
     cused (ZMap.get id (ZMap.set j (mkContainer q 0 i nil true)
                        (ZMap.set i (mkContainer (cquota (ZMap.get i (AC d)))
                                       (cusage (ZMap.get i (AC d)) + q)
                                       (cparent (ZMap.get i (AC d)))
                                       (j :: cchildren (ZMap.get i (AC d)))
                                       (cused (ZMap.get i (AC d)))) (AC d)))) = true).
Proof.
  intros.
  destruct (zeq id j); subst.
  rewrite 2 ZMap.gss; simpl; split; auto.
  rewrite 2 ZMap.gso; auto.
  destruct (zeq id i); subst.
  rewrite ZMap.gss; simpl.
  rewrite H; auto; rewrite H0; split; auto.
  rewrite ZMap.gso; auto.
Qed.

Lemma container_split_some´ :
   d i q j,
    ( i : Z, 0 i < num_id
       (ZMap.get i (pb d) = PTTrue cused (ZMap.get i (AC d)) = true)) →
    ikern d = trueihost d = truecused (ZMap.get i (AC d)) = true
    ZMap.get j (pb d) PTTrue → 0 < j < num_id
    0 q cquota (ZMap.get i (AC d)) - cusage (ZMap.get i (AC d)) →
    container_split_spec i q j d =
    Some (d {AC: ZMap.set j (mkContainer q 0 i nil true)
              (ZMap.set i (mkContainer (cquota (ZMap.get i (AC d)))
                                       (cusage (ZMap.get i (AC d)) + q)
                                       (cparent (ZMap.get i (AC d)))
                                       (j :: cchildren (ZMap.get i (AC d)))
                                       true) (AC d))}, j).
Proof.
  unfold container_split_spec; intros.
  rewrite H0, H1, H2.
  rewrite H in H3; try omega.
  destruct (cused (ZMap.get j (AC d))); try solve [contradict H3; auto].
  destruct (zlt_lt 0 j num_id); try omega.
  destruct (zle_le 0 q (cquota (ZMap.get i (AC d)) - cusage (ZMap.get i (AC d)))); try omega; auto.
Qed.

Lemma container_split_PTB_AC_valid´ :
   d i q j id,
    ( i : Z,
       0 i < num_id
       (ZMap.get i (pb d) = PTTrue cused (ZMap.get i (AC d)) = true)) →
    cused (ZMap.get i (AC d)) = true → 0 id < num_id
    (ZMap.get id (ZMap.set j PTTrue (pb d)) = PTTrue
     cused (ZMap.get id (ZMap.set j (mkContainer q 0 i nil true)
                        (ZMap.set i (mkContainer (cquota (ZMap.get i (AC d)))
                                       (cusage (ZMap.get i (AC d)) + q)
                                       (cparent (ZMap.get i (AC d)))
                                       (j :: cchildren (ZMap.get i (AC d)))
                                       true) (AC d)))) = true).
Proof.
  intros.
  destruct (zeq id j); subst.
  rewrite 2 ZMap.gss; simpl; split; auto.
  rewrite 2 ZMap.gso; auto.
  destruct (zeq id i); subst.
  rewrite ZMap.gss; simpl.
  rewrite H; auto; rewrite H0; split; auto.
  rewrite ZMap.gso; auto.
Qed.

Lemma container_alloc_PTB_AC_valid :
   d id i,
    ( i : Z,
       0 i < num_id
       (ZMap.get i (pb d) = PTTrue cused (ZMap.get i (AC d)) = true)) →
    0 id < num_id
    (ZMap.get id (pb d) = PTTrue
     cused (ZMap.get id (ZMap.set i
              (mkContainer (cquota (ZMap.get i (AC d)))
                           (cusage (ZMap.get i (AC d)) + 1)
                           (cparent (ZMap.get i (AC d)))
                           (cchildren (ZMap.get i (AC d)))
                           (cused (ZMap.get i (AC d)))) (AC d))) = true).
Proof.
  intros.
  destruct (zeq id i); subst.
  rewrite ZMap.gss; simpl; auto.
  rewrite ZMap.gso; auto.
Qed.