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 i´, _x0 into Hn, _x into Hj,
H2 into Hj_unused, H3 into Hused, H6 into Hused´; clear H0 H1.
-
destruct (zeq i´ j); try subst i´.
omega.
rewrite ZMap.gso in Hused´; auto.
destruct (zeq i´ i); try subst i´.
apply (cvalid_id _ Hused).
rewrite ZMap.gso in Hused´; auto.
-
destruct (zeq i´ j); try subst i´.
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´ i); try subst i´.
rewrite ZMap.gss; simpl; subst c; auto.
rewrite ZMap.gso; auto.
rewrite 2 ZMap.gso in Hused´; auto.
-
destruct (zeq i´ j); try subst i´.
+ 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´ i); try subst i´.
rewrite ZMap.gss; simpl; try omega.
apply cvalid_quota; assumption.
rewrite 2 ZMap.gso in Hused´; auto.
rewrite ZMap.gso; auto.
-
destruct (zeq i´ j); try subst i´.
rewrite ZMap.gss; simpl; omega.
rewrite ZMap.gso; auto.
destruct (zeq i´ i); try subst i´.
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 i´ j); try subst i´.
+ 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 i´ (ZMap.set j child (ZMap.set i cur (AC adt))))
with (ZMap.get i´ (ZMap.set i cur (AC adt))).
destruct (zeq i´ i); try subst i´.
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 i´ (ZMap.set i cur (AC adt))) with (ZMap.get i´ (AC adt)).
destruct (zeq (cparent (ZMap.get i´ (AC adt))) j) as [eq1|neq1].
rewrite eq1; rewrite ZMap.gss; auto.
rewrite ZMap.gso; auto.
destruct (zeq (cparent (ZMap.get i´ (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 i´ j) as [Heq|Hneq]; try subst i´.
rewrite ZMap.gss; simpl; apply Forall_nil.
rewrite ZMap.gso; auto.
destruct (zeq i´ i) as [Heq´|Hneq´]; try subst i´.
+ 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 i´ j) as [Heq|Hneq]; try subst i´.
+ 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´ i) as [Heq´|Hneq´]; try subst i´.
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 i´ (AC adt))) j) as [Heq1|Hneq1].
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 (ZMap.get i´ (AC adt))) i) as [Heq2|Hneq2].
rewrite Heq2; rewrite ZMap.gss; simpl; right.
specialize (cvalid_parents_child i´ Hused´ Hi´_neq); rewrite Heq2 in cvalid_parents_child; auto.
rewrite ZMap.gso; auto.
-
destruct (zeq i´ j) as [Heq|Hneq]; try subst i´.
rewrite ZMap.gss; simpl; constructor.
rewrite ZMap.gso; auto.
destruct (zeq i´ i) as [Heq´|Hneq´]; try subst i´.
+ 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 i´ j) as [Heq|Hneq]; try subst i´.
rewrite ZMap.gss; simpl; constructor; reflexivity.
rewrite ZMap.gso; auto.
destruct (zeq i´ i) as [Heq´|Hneq´]; try subst i´.
+ 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 i´ j) as [Heq|Hneq]; try subst i´.
rewrite ZMap.gss; simpl; constructor.
rewrite ZMap.gso; auto.
destruct (zeq i´ i) as [Heq´|Hneq´]; try subst i´.
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 = true → ihost d = true → cused (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 = true → ihost d = true → cused (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.