Library mcertikos.mm.ContainerGen
*********************************************************************** * * * 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. * * * ***********************************************************************
This file provide the contextual refinement proof between MBoot layer and MALInit layer
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem1.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import MContainer.
Require Import DAbsHandler.
Require Import ProofIrrelevance.
Require Import ContainerGenSpec.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem1.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import MContainer.
Require Import DAbsHandler.
Require Import ProofIrrelevance.
Require Import ContainerGenSpec.
Section Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mcontainer_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := dabshandler_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mcontainer_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := dabshandler_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Relation between Z and int
Inductive match_int: Z → int → Prop :=
| MATCH_INT: ∀ v, 0 ≤ v ≤ Int.max_unsigned → match_int v (Int.repr v).
| MATCH_INT: ∀ v, 0 ≤ v ≤ Int.max_unsigned → match_int v (Int.repr v).
Relation between a single container and the underlying memory
Inductive match_container: Container → val → val → val → val → val → Prop :=
| MATCH_CONTAINER_UNUSED:
∀ q u p c v1 v2 v3 v4,
match_container (mkContainer q u p c false) v1 v2 v3 v4 (Vint Int.zero)
| MATCH_CONTAINER_USED:
∀ q u p c,
match_int q (Int.repr q) → match_int u (Int.repr u) → match_int p (Int.repr p) →
match_int (Z_of_nat (length c)) (Int.repr (Z_of_nat (length c))) →
match_container (mkContainer q u p c true)
(Vint (Int.repr q)) (Vint (Int.repr u)) (Vint (Int.repr p))
(Vint (Int.repr (Z_of_nat (length c)))) (Vint Int.one).
| MATCH_CONTAINER_UNUSED:
∀ q u p c v1 v2 v3 v4,
match_container (mkContainer q u p c false) v1 v2 v3 v4 (Vint Int.zero)
| MATCH_CONTAINER_USED:
∀ q u p c,
match_int q (Int.repr q) → match_int u (Int.repr u) → match_int p (Int.repr p) →
match_int (Z_of_nat (length c)) (Int.repr (Z_of_nat (length c))) →
match_container (mkContainer q u p c true)
(Vint (Int.repr q)) (Vint (Int.repr u)) (Vint (Int.repr p))
(Vint (Int.repr (Z_of_nat (length c)))) (Vint Int.one).
Relation between the container pool and the underlying memory
Inductive match_RData: stencil → HDATA → mem → meminj → Prop :=
| MATCH_CP: ∀ m b s hadt f,
(∀ i, 0 ≤ i < num_id →
(∃ v1 v2 v3 v4 v5,
Mem.load Mint32 m b (i×CSIZE+QUOTA) = Some (Vint v1) ∧
Mem.load Mint32 m b (i×CSIZE+USAGE) = Some (Vint v2) ∧
Mem.load Mint32 m b (i×CSIZE+PARENT) = Some (Vint v3) ∧
Mem.load Mint32 m b (i×CSIZE+NCHILDREN) = Some (Vint v4) ∧
Mem.load Mint32 m b (i×CSIZE+USED) = Some (Vint v5) ∧
Mem.valid_access m Mint32 b (i×CSIZE+QUOTA) Writable ∧
Mem.valid_access m Mint32 b (i×CSIZE+USAGE) Writable ∧
Mem.valid_access m Mint32 b (i×CSIZE+PARENT) Writable ∧
Mem.valid_access m Mint32 b (i×CSIZE+NCHILDREN) Writable ∧
Mem.valid_access m Mint32 b (i×CSIZE+USED) Writable ∧
match_container (ZMap.get i (AC hadt)) (Vint v1) (Vint v2)
(Vint v3) (Vint v4) (Vint v5)))
→ find_symbol s AC_LOC = Some b
→ match_RData s hadt m f.
| MATCH_CP: ∀ m b s hadt f,
(∀ i, 0 ≤ i < num_id →
(∃ v1 v2 v3 v4 v5,
Mem.load Mint32 m b (i×CSIZE+QUOTA) = Some (Vint v1) ∧
Mem.load Mint32 m b (i×CSIZE+USAGE) = Some (Vint v2) ∧
Mem.load Mint32 m b (i×CSIZE+PARENT) = Some (Vint v3) ∧
Mem.load Mint32 m b (i×CSIZE+NCHILDREN) = Some (Vint v4) ∧
Mem.load Mint32 m b (i×CSIZE+USED) = Some (Vint v5) ∧
Mem.valid_access m Mint32 b (i×CSIZE+QUOTA) Writable ∧
Mem.valid_access m Mint32 b (i×CSIZE+USAGE) Writable ∧
Mem.valid_access m Mint32 b (i×CSIZE+PARENT) Writable ∧
Mem.valid_access m Mint32 b (i×CSIZE+NCHILDREN) Writable ∧
Mem.valid_access m Mint32 b (i×CSIZE+USED) Writable ∧
match_container (ZMap.get i (AC hadt)) (Vint v1) (Vint v2)
(Vint v3) (Vint v4) (Vint v5)))
→ find_symbol s AC_LOC = Some b
→ match_RData s hadt m f.
Relation between the shared raw data at two layers
Record relate_RData (f:meminj) (hadt: HDATA) (ladt: LDATA) :=
mkrelate_RData {
flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
MM_re: MM hadt = MM ladt;
MMSize_re: MMSize hadt = MMSize ladt;
vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
CR3_re: CR3 hadt = CR3 ladt;
ikern_re: ikern hadt = ikern ladt;
pg_re: pg hadt = pg ladt;
ihost_re: ihost hadt = ihost ladt;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
init_re: init hadt = init ladt;
com1_re: com1 hadt = com1 ladt;
console_re: console hadt = console ladt;
console_concrete_re: console_concrete hadt = console_concrete ladt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr ladt = in_intr hadt;
drv_serial_re: drv_serial hadt = drv_serial ladt
}.
Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
{
relate_AbData s f d1 d2 := relate_RData f d1 d2;
match_AbData s d1 m f := match_RData s d1 m f;
new_glbl := AC_LOC :: nil
}.
Definition AC_glbl : In AC_LOC new_glbl.
Proof.
simpl; auto.
Defined.
End REFINEMENT_REL.
mkrelate_RData {
flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
MM_re: MM hadt = MM ladt;
MMSize_re: MMSize hadt = MMSize ladt;
vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
CR3_re: CR3 hadt = CR3 ladt;
ikern_re: ikern hadt = ikern ladt;
pg_re: pg hadt = pg ladt;
ihost_re: ihost hadt = ihost ladt;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
init_re: init hadt = init ladt;
com1_re: com1 hadt = com1 ladt;
console_re: console hadt = console ladt;
console_concrete_re: console_concrete hadt = console_concrete ladt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr ladt = in_intr hadt;
drv_serial_re: drv_serial hadt = drv_serial ladt
}.
Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
{
relate_AbData s f d1 d2 := relate_RData f d1 d2;
match_AbData s d1 m f := match_RData s d1 m f;
new_glbl := AC_LOC :: nil
}.
Definition AC_glbl : In AC_LOC new_glbl.
Proof.
simpl; auto.
Defined.
End REFINEMENT_REL.
Section Rel_Property.
Lemma inject_match_correct:
∀ s d1 m2 f m2´ j,
match_RData s d1 m2 f →
Mem.inject j m2 m2´ →
inject_incr (Mem.flat_inj (genv_next s)) j →
match_RData s d1 m2´ (compose_meminj f j).
Proof.
inversion 1; subst; intros.
assert (HFB: j b = Some (b, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
econstructor; eauto; intros i Hi.
destruct (H0 i Hi) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ v1, v2, v3, v4, v5.
refine_split; auto.
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H2 HL1 HFB).
rewrite Z.add_0_r; intros [v1´ [HL1´ Hv1´]]; inv Hv1´; auto.
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H2 HL2 HFB).
rewrite Z.add_0_r; intros [v1´ [HL2´ Hv2´]]; inv Hv2´; auto.
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H2 HL3 HFB).
rewrite Z.add_0_r; intros [v1´ [HL3´ Hv3´]]; inv Hv3´; auto.
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H2 HL4 HFB).
rewrite Z.add_0_r; intros [v1´ [HL4´ Hv4´]]; inv Hv4´; auto.
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H2 HL5 HFB).
rewrite Z.add_0_r; intros [v1´ [HL5´ Hv5´]]; inv Hv5´; auto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB H2 HA1).
rewrite Z.add_0_r; auto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB H2 HA2).
rewrite Z.add_0_r; auto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB H2 HA3).
rewrite Z.add_0_r; auto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB H2 HA4).
rewrite Z.add_0_r; auto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB H2 HA5).
rewrite Z.add_0_r; auto.
Qed.
Lemma store_match_correct:
∀ s abd m0 m0´ f b2 v v´ chunk,
match_RData s abd m0 f →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.store chunk m0 b2 v v´ = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros; inv H.
econstructor; eauto; intros i Hi.
specialize (H0 _ _ AC_glbl H3).
destruct (H2 i Hi) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ v1, v2, v3, v4, v5.
refine_split; auto; try solve [rewrite (Mem.load_store_other _ _ _ _ _ _ H1); auto];
try solve [eapply Mem.store_valid_access_1; eauto].
Qed.
Lemma storebytes_match_correct:
∀ s abd m0 m0´ f b2 v v´,
match_RData s abd m0 f →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.storebytes m0 b2 v v´ = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros; inv H.
econstructor; eauto; intros i Hi.
specialize (H0 _ _ AC_glbl H3).
destruct (H2 i Hi) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ v1, v2, v3, v4, v5.
refine_split; auto; try solve [rewrite (Mem.load_storebytes_other _ _ _ _ _ H1); auto];
try solve [eapply Mem.storebytes_valid_access_1; eauto].
Qed.
Lemma free_match_correct:
∀ s abd m0 m0´ f ofs sz b2,
match_RData s abd m0 f→
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.free m0 b2 ofs sz = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros; inv H.
econstructor; eauto; intros i Hi.
specialize (H0 _ _ AC_glbl H3).
destruct (H2 i Hi) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ v1, v2, v3, v4, v5.
refine_split; auto; try solve [rewrite (Mem.load_free _ _ _ _ _ H1); auto];
try solve [eapply Mem.valid_access_free_1; eauto].
Qed.
Lemma alloc_match_correct:
∀ s abd m´0 m´1 f f´ ofs sz b0 b´1,
match_RData s abd m´0 f→
Mem.alloc m´0 ofs sz = (m´1, b´1) →
f´ b0 = Some (b´1, 0%Z) →
(∀ b : block, b ≠ b0 → f´ b = f b) →
inject_incr f f´ →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b0) →
match_RData s abd m´1 f´.
Proof.
intros; inv H.
econstructor; eauto; intros i Hi.
specialize (H4 _ _ AC_glbl H6).
destruct (H5 i Hi) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ v1, v2, v3, v4, v5.
refine_split; auto; try solve [apply (Mem.load_alloc_other _ _ _ _ _ H0); auto];
try solve [eapply Mem.valid_access_alloc_other; eauto].
Qed.
Lemma inject_match_correct:
∀ s d1 m2 f m2´ j,
match_RData s d1 m2 f →
Mem.inject j m2 m2´ →
inject_incr (Mem.flat_inj (genv_next s)) j →
match_RData s d1 m2´ (compose_meminj f j).
Proof.
inversion 1; subst; intros.
assert (HFB: j b = Some (b, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
econstructor; eauto; intros i Hi.
destruct (H0 i Hi) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ v1, v2, v3, v4, v5.
refine_split; auto.
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H2 HL1 HFB).
rewrite Z.add_0_r; intros [v1´ [HL1´ Hv1´]]; inv Hv1´; auto.
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H2 HL2 HFB).
rewrite Z.add_0_r; intros [v1´ [HL2´ Hv2´]]; inv Hv2´; auto.
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H2 HL3 HFB).
rewrite Z.add_0_r; intros [v1´ [HL3´ Hv3´]]; inv Hv3´; auto.
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H2 HL4 HFB).
rewrite Z.add_0_r; intros [v1´ [HL4´ Hv4´]]; inv Hv4´; auto.
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H2 HL5 HFB).
rewrite Z.add_0_r; intros [v1´ [HL5´ Hv5´]]; inv Hv5´; auto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB H2 HA1).
rewrite Z.add_0_r; auto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB H2 HA2).
rewrite Z.add_0_r; auto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB H2 HA3).
rewrite Z.add_0_r; auto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB H2 HA4).
rewrite Z.add_0_r; auto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB H2 HA5).
rewrite Z.add_0_r; auto.
Qed.
Lemma store_match_correct:
∀ s abd m0 m0´ f b2 v v´ chunk,
match_RData s abd m0 f →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.store chunk m0 b2 v v´ = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros; inv H.
econstructor; eauto; intros i Hi.
specialize (H0 _ _ AC_glbl H3).
destruct (H2 i Hi) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ v1, v2, v3, v4, v5.
refine_split; auto; try solve [rewrite (Mem.load_store_other _ _ _ _ _ _ H1); auto];
try solve [eapply Mem.store_valid_access_1; eauto].
Qed.
Lemma storebytes_match_correct:
∀ s abd m0 m0´ f b2 v v´,
match_RData s abd m0 f →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.storebytes m0 b2 v v´ = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros; inv H.
econstructor; eauto; intros i Hi.
specialize (H0 _ _ AC_glbl H3).
destruct (H2 i Hi) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ v1, v2, v3, v4, v5.
refine_split; auto; try solve [rewrite (Mem.load_storebytes_other _ _ _ _ _ H1); auto];
try solve [eapply Mem.storebytes_valid_access_1; eauto].
Qed.
Lemma free_match_correct:
∀ s abd m0 m0´ f ofs sz b2,
match_RData s abd m0 f→
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.free m0 b2 ofs sz = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros; inv H.
econstructor; eauto; intros i Hi.
specialize (H0 _ _ AC_glbl H3).
destruct (H2 i Hi) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ v1, v2, v3, v4, v5.
refine_split; auto; try solve [rewrite (Mem.load_free _ _ _ _ _ H1); auto];
try solve [eapply Mem.valid_access_free_1; eauto].
Qed.
Lemma alloc_match_correct:
∀ s abd m´0 m´1 f f´ ofs sz b0 b´1,
match_RData s abd m´0 f→
Mem.alloc m´0 ofs sz = (m´1, b´1) →
f´ b0 = Some (b´1, 0%Z) →
(∀ b : block, b ≠ b0 → f´ b = f b) →
inject_incr f f´ →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b0) →
match_RData s abd m´1 f´.
Proof.
intros; inv H.
econstructor; eauto; intros i Hi.
specialize (H4 _ _ AC_glbl H6).
destruct (H5 i Hi) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ v1, v2, v3, v4, v5.
refine_split; auto; try solve [apply (Mem.load_alloc_other _ _ _ _ _ H0); auto];
try solve [eapply Mem.valid_access_alloc_other; eauto].
Qed.
Prove that after taking one step, the refinement relation still holds
Lemma relate_incr:
∀ abd abd´ f f´,
relate_RData f abd abd´
→ inject_incr f f´
→ relate_RData f´ abd abd´.
Proof.
inversion 1; subst; intros; inv H; constructor; eauto.
Qed.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor.
- apply inject_match_correct.
- apply store_match_correct.
- apply alloc_match_correct.
- apply free_match_correct.
- apply storebytes_match_correct.
- intros. eapply relate_incr; eauto.
Qed.
End Rel_Property.
∀ abd abd´ f f´,
relate_RData f abd abd´
→ inject_incr f f´
→ relate_RData f´ abd abd´.
Proof.
inversion 1; subst; intros; inv H; constructor; eauto.
Qed.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor.
- apply inject_match_correct.
- apply store_match_correct.
- apply alloc_match_correct.
- apply free_match_correct.
- apply storebytes_match_correct.
- intros. eapply relate_incr; eauto.
Qed.
End Rel_Property.
Section OneStep_Forward_Relation.
Section container_init_ref.
Lemma container_init_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_init_spec) container_init_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (0 ≤ 0 < 64) as Hi0; try omega.
destruct (H 0 Hi0) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
simpl in ×.
remember HA1 as HA1old; clear HeqHA1old.
remember HA2 as HA2old; clear HeqHA2old.
remember HA3 as HA3old; clear HeqHA3old.
remember HA4 as HA4old; clear HeqHA4old.
remember HA5 as HA5old; clear HeqHA5old.
apply Mem.valid_access_store with (v := Vint (Int.repr root_quota)) in HA1.
destruct HA1 as [m3 HA1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1) in HA3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1) in HA4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1) in HA5.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA2.
destruct HA2 as [m4 HA2].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2) in HA3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2) in HA4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2) in HA5.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA3.
destruct HA3 as [m5 HA3].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3) in HA4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3) in HA5.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA4.
destruct HA4 as [m6 HA4].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4) in HA5.
apply Mem.valid_access_store with (v := Vint Int.one) in HA5.
destruct HA5 as [m7 HA5].
inv Hι.
inv H4; inv H6.
∃ ι, Vundef, m7, (d2 { ioapic
: DeviceStateDataType.update_s (ioapic d1)
(ioapic_init_aux (DeviceStateDataType.s (ioapic d1))
(Z.to_nat
(DeviceStateDataType.IoApicMaxIntr
(DeviceStateDataType.s (ioapic d1)) + 1 - 1)))} {
lapic
: DeviceStateDataType.update_l3
(DeviceStateDataType.update_l2
(DeviceStateDataType.update_l1
(DeviceStateDataType.mkLApicData
{|
DeviceStateDataType.LapicEsr := 0;
DeviceStateDataType.LapicEoi := DeviceStateDataType.NoIntr;
DeviceStateDataType.LapicMaxLvt := DeviceStateDataType.LapicMaxLvt
(DeviceStateDataType.s
(lapic d1));
DeviceStateDataType.LapicEnable := true;
DeviceStateDataType.LapicSpurious := 32 + 7;
DeviceStateDataType.LapicLint0Mask := true;
DeviceStateDataType.LapicLint1Mask := true;
DeviceStateDataType.LapicPcIntMask := true;
DeviceStateDataType.LapicLdr := 0;
DeviceStateDataType.LapicErrorIrq := 50;
DeviceStateDataType.LapicEsrClrPen := false;
DeviceStateDataType.LapicTpr := 0 |})
(DeviceStateDataType.l1 (lapic d1)))
(DeviceStateDataType.l2 (lapic d1)))
(DeviceStateDataType.l3 (lapic d1))} { ioapic / s /
CurrentIrq : None} {MM: real_mm} {MMSize: real_size} {vmxinfo: real_vmxinfo} {init : true}).
repeat (apply conj).
- apply (container_init_low_intro _ _ _ m7 m3 m4 m5 m6 d2 _ b); auto.
functional inversion H1; inv match_related; unfold bootloader0_spec.
rewrite <- pg_re0; rewrite H7.
rewrite <- ikern_re0; rewrite H5.
rewrite <- ihost_re0; rewrite H4.
rewrite in_intr_re0; rewrite H6.
rewrite ioapic_re0.
rewrite lapic_re0.
rewrite <- init_re0; rewrite H3; auto.
unfold container_init_spec in H1.
subdestruct.
reflexivity.
inv match_related.
unfold container_init_spec in H1.
subdestruct. eauto.
- constructor.
- functional inversion H1; inv match_related.
split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
constructor; auto.
econstructor; eauto.
intros i´ Hi´. unfold AC_init in ×.
destruct (zeq i´ 0); subst; simpl.
rewrite ZMap.gss.
∃ (Int.repr root_quota), Int.zero, Int.zero, Int.zero, Int.one.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
apply (Mem.load_store_same _ _ _ _ _ _ HA1).
simpl; unfold USAGE; right; left; omega.
simpl; unfold PARENT; right; left; omega.
simpl; unfold NCHILDREN; right; left; omega.
simpl; unfold USED; right; left; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
apply (Mem.load_store_same _ _ _ _ _ _ HA2).
simpl; unfold PARENT; right; left; omega.
simpl; unfold NCHILDREN; right; left; omega.
simpl; unfold USED; right; left; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
apply (Mem.load_store_same _ _ _ _ _ _ HA3).
simpl; unfold NCHILDREN; right; left; omega.
simpl; unfold USED; right; left; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
apply (Mem.load_store_same _ _ _ _ _ _ HA4).
simpl; unfold USED; right; left; omega.
split.
apply (Mem.load_store_same _ _ _ _ _ _ HA5).
repeat (split; try solve [
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1); auto]).
constructor; constructor; unfold Int.max_unsigned; simpl; omega.
rewrite ZMap.gso; auto.
destruct (H i´ Hi´) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1); auto.
simpl; unfold QUOTA; unfold CSIZE; right; right; omega.
simpl; unfold QUOTA; unfold USAGE; unfold CSIZE; right; right; omega.
simpl; unfold QUOTA; unfold PARENT; unfold CSIZE; right; right; omega.
simpl; unfold QUOTA; unfold NCHILDREN; unfold CSIZE; right; right; omega.
simpl; unfold QUOTA; unfold USED; unfold CSIZE; right; right; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1); auto.
simpl; unfold USAGE; unfold QUOTA; unfold CSIZE; right; right; omega.
simpl; unfold USAGE; unfold CSIZE; right; right; omega.
simpl; unfold USAGE; unfold PARENT; unfold CSIZE; right; right; omega.
simpl; unfold USAGE; unfold NCHILDREN; unfold CSIZE; right; right; omega.
simpl; unfold USAGE; unfold USED; unfold CSIZE; right; right; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1); auto.
simpl; unfold PARENT; unfold QUOTA; unfold CSIZE; right; right; omega.
simpl; unfold PARENT; unfold USAGE; unfold CSIZE; right; right; omega.
simpl; unfold PARENT; unfold CSIZE; right; right; omega.
simpl; unfold PARENT; unfold NCHILDREN; unfold CSIZE; right; right; omega.
simpl; unfold PARENT; unfold USED; unfold CSIZE; right; right; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1); auto.
simpl; unfold NCHILDREN; unfold QUOTA; unfold CSIZE; right; right; omega.
simpl; unfold NCHILDREN; unfold USAGE; unfold CSIZE; right; right; omega.
simpl; unfold NCHILDREN; unfold PARENT; unfold CSIZE; right; right; omega.
simpl; unfold NCHILDREN; unfold CSIZE; right; right; omega.
simpl; unfold NCHILDREN; unfold USED; unfold CSIZE; right; right; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1); auto.
simpl; unfold USED; unfold QUOTA; unfold CSIZE; right; right; omega.
simpl; unfold USED; unfold USAGE; unfold CSIZE; right; right; omega.
simpl; unfold USED; unfold PARENT; unfold CSIZE; right; right; omega.
simpl; unfold USED; unfold NCHILDREN; unfold CSIZE; right; right; omega.
simpl; unfold USED; unfold CSIZE; right; right; omega.
repeat (split; try solve [
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1); auto]).
rewrite ZMap.gi.
inv Hm´.
constructor.
pose proof (valid_preinit_container _ Hhigh´ H3 _ Hi´) as _x2.
rewrite <- H2 in _x2; contradict _x2; auto.
- auto.
Qed.
End container_init_ref.
Section container_get_parent_ref.
Lemma container_get_parent_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_get_parent_spec)
container_get_parent_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H8; inv H10.
inv Hhigh´.
destruct valid_container.
specialize (cvalid_id _ H3).
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H7 in H3; inv H3.
rewrite <- H6 in H1.
simpl in H1; subst.
rewrite Int.repr_unsigned in HL3; auto.
simpl; inv match_related; split; congruence.
- constructor.
- assumption.
- auto.
Qed.
End container_get_parent_ref.
Section container_get_quota_ref.
Lemma container_get_quota_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_get_quota_spec)
container_get_quota_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H8; inv H10.
inv Hhigh´.
destruct valid_container.
specialize (cvalid_id _ H3).
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H7 in H3; inv H3.
rewrite <- H6 in H1.
simpl in H1; subst.
rewrite Int.repr_unsigned in HL1; auto.
simpl; inv match_related; split; congruence.
- constructor.
- assumption.
- auto.
Qed.
End container_get_quota_ref.
Section container_get_usage_ref.
Lemma container_get_usage_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_get_usage_spec)
container_get_usage_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H8; inv H10.
inv Hhigh´.
destruct valid_container.
specialize (cvalid_id _ H3).
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H7 in H3; inv H3.
rewrite <- H6 in H1.
simpl in H1; subst.
rewrite Int.repr_unsigned in HL2; auto.
simpl; inv match_related; split; congruence.
- constructor.
- assumption.
- auto.
Qed.
End container_get_usage_ref.
Section container_can_consume_ref.
Lemma container_can_consume_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_can_consume_spec)
container_can_consume_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv Hι.
inv H4; inv H6.
inv H4; inv H7.
rename i0 into n.
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- functional inversion H2.
× inv Hhigh´.
destruct valid_container.
specialize (cvalid_id _ H3).
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H3; inv H3.
replace z with
(match (Int.unsigned n <=? Int.unsigned (Int.repr (cquota (ZMap.get (Int.unsigned i) (AC d1´)))),
Int.unsigned (Int.repr (cusage (ZMap.get (Int.unsigned i) (AC d1´)))) <=?
Int.unsigned (Int.repr (cquota (ZMap.get (Int.unsigned i) (AC d1´)))) - Int.unsigned n) with
| (true, true) ⇒ Int.one
| _ ⇒ Int.zero end).
econstructor; eauto.
rewrite <- H7; auto.
rewrite <- H7; auto.
simpl; inv match_related; split; congruence.
specialize (cvalid_quota _ H3); specialize (cvalid_usage _ H3).
rewrite 2 Int.unsigned_repr; try omega.
assert (Hle1: Int.unsigned n ≤ cquota (ZMap.get (Int.unsigned i) (AC d1´))) by omega.
assert (Hle2: cusage (ZMap.get (Int.unsigned i) (AC d1´)) ≤
cquota (ZMap.get (Int.unsigned i) (AC d1´)) - Int.unsigned n) by omega.
rewrite <- Z.leb_le in Hle1, Hle2; rewrite Hle1, Hle2.
apply f_equal with (f := Int.repr) in H1.
rewrite Int.repr_unsigned in H1; auto.
× inv Hhigh´.
destruct valid_container.
specialize (cvalid_id _ H3).
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H3; inv H3.
replace z with
(match (Int.unsigned n <=? Int.unsigned (Int.repr (cquota (ZMap.get (Int.unsigned i) (AC d1´)))),
Int.unsigned (Int.repr (cusage (ZMap.get (Int.unsigned i) (AC d1´)))) <=?
Int.unsigned (Int.repr (cquota (ZMap.get (Int.unsigned i) (AC d1´)))) - Int.unsigned n) with
| (true, true) ⇒ Int.one
| _ ⇒ Int.zero end).
econstructor; eauto.
rewrite <- H7; auto.
rewrite <- H7; auto.
simpl; inv match_related; split; congruence.
specialize (cvalid_quota _ H3); specialize (cvalid_usage _ H3).
rewrite 2 Int.unsigned_repr; try omega.
assert (Hrange:= Int.unsigned_range n).
assert (Hle: ¬ Int.unsigned n ≤ cquota (ZMap.get (Int.unsigned i) (AC d1´)) ∨
¬ cusage (ZMap.get (Int.unsigned i) (AC d1´)) ≤
cquota (ZMap.get (Int.unsigned i) (AC d1´)) - Int.unsigned n) by omega.
rewrite <- Z.leb_le in Hle; rewrite <- Z.leb_le in Hle; destruct Hle as [Hle|Hle].
destruct (Int.unsigned n <=? cquota (ZMap.get (Int.unsigned i) (AC d1´))).
contradict Hle; auto.
apply f_equal with (f := Int.repr) in H1.
rewrite Int.repr_unsigned in H1; auto.
destruct (cusage (ZMap.get (Int.unsigned i) (AC d1´)) <=?
cquota (ZMap.get (Int.unsigned i) (AC d1´)) - Int.unsigned n).
contradict Hle; auto.
apply f_equal with (f := Int.repr) in H1.
rewrite Int.repr_unsigned in H1.
destruct (Int.unsigned n <=? cquota (ZMap.get (Int.unsigned i) (AC d1´))); auto.
- constructor.
- assumption.
- auto.
Qed.
End container_can_consume_ref.
Section container_split_ref.
Lemma norepet_nodup {A} :
∀ l : list A, list_norepet l ↔ NoDup l.
Proof.
induction l; split; intros.
constructor.
constructor.
inv H; constructor; auto.
apply IHl; auto.
inv H; constructor; auto.
apply IHl; auto.
Qed.
Lemma nodup_length_ub :
∀ l l´, incl(A:=Z) l l´ → NoDup l → (length l ≤ length l´)%nat.
Proof.
intros l l´; rewrite <- norepet_nodup.
intros; apply PTree_Properties.list_incl_length; auto.
Qed.
Fixpoint build_range (n : nat) (z : Z) : list Z :=
match n with
| O ⇒ nil
| S n ⇒ z :: build_range n (z+1)
end.
Lemma build_range_length :
∀ n z, length (build_range n z) = n.
Proof.
induction n; simpl; auto.
Qed.
Lemma build_range_charact :
∀ n z z´, In z´ (build_range n z) ↔ z ≤ z´ < z + Z_of_nat n.
Proof.
induction n; intros.
simpl; omega.
rewrite Nat2Z.inj_succ; simpl; split; intros.
destruct H; subst; try omega.
rewrite IHn in H; omega.
rewrite IHn; omega.
Qed.
Lemma nodup_length :
∀ l a b,
a ≤ b → NoDup l → Forall (fun z ⇒ a ≤ z < b) l → Z_of_nat (length l) ≤ b - a.
Proof.
intros l a b Hle Hnodup Hrange.
rewrite <- nat_of_Z_eq; try omega; apply inj_le.
rewrite <- (build_range_length (nat_of_Z (b-a)) a).
apply nodup_length_ub; auto.
unfold incl; intros z Hin.
rewrite Forall_forall in Hrange; specialize (Hrange z Hin).
rewrite build_range_charact.
rewrite nat_of_Z_eq; omega.
Qed.
Lemma container_split_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_split_spec)
container_split_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H1; subst c cur child.
replace z with (Int.repr (Int.unsigned z)); try apply Int.repr_unsigned.
rewrite <- H3 in *; clear H3 z.
rename i0 into n, i1 into j, H0 into Hfind, _x into Hh, _x0 into Hn,
H6 into Hj_unused, H7 into Hused; clear H4 H5.
inv Hhigh´.
destruct valid_container.
assert (cvalid_id´:= cvalid_id); specialize (cvalid_id _ Hused).
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
assert (0 ≤ Int.unsigned j < num_id) as Hj; try omega.
destruct (H (Int.unsigned j) Hj) as
[v1z[v2z[v3z[v4z[v5z[HL1z[HL2z[HL3z[HL4z[HL5z[HA1z[HA2z[HA3z[HA4z[HA5z Hmz]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H2 in Hused; inv Hused.
inv Hι.
inv H4; inv H6.
inv H4; inv H13.
inv H4; inv H6.
simpl in ×.
assert (HA1old := HA1).
assert (HA2old := HA2).
assert (HA3old := HA3).
assert (HA4old := HA4).
assert (HA5old := HA5).
assert (HA1zold := HA1z).
assert (HA2zold := HA2z).
assert (HA3zold := HA3z).
assert (HA4zold := HA4z).
assert (HA5zold := HA5z).
apply Mem.valid_access_store with (v := Vint Int.one) in HA5z.
destruct HA5z as [m3 HA5z].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA1z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA2z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA3z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA4z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA4.
apply Mem.valid_access_store with (v := Vint n) in HA1z.
destruct HA1z as [m4 HA1z].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z) in HA2z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z) in HA3z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z) in HA4z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z) in HA4.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA2z.
destruct HA2z as [m5 HA2z].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z) in HA3z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z) in HA4z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z) in HA4.
apply Mem.valid_access_store with (v := Vint i) in HA3z.
destruct HA3z as [m6 HA3z].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z) in HA4z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z) in HA4.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA4z.
destruct HA4z as [m7 HA4z].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4z) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4z) in HA4.
apply Mem.valid_access_store with (v := Vint (Int.add (Int.repr u) n)) in HA2.
destruct HA2 as [m8 HA2].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2) in HA4.
apply Mem.valid_access_store with (v := Vint (Int.add (Int.repr (Z.of_nat (length c))) Int.one)) in HA4.
destruct HA4 as [m9 HA4].
rename H7 into Hmq, H10 into Hmu, H11 into Hmp, H12 into Hmc.
∃ ι, (Vint j), m9, d2; repeat (apply conj).
- apply (container_split_low_step_intro _ _ _ _
(m3,d2) (m4,d2) (m5,d2) (m6,d2) (m7,d2) (m8,d2)
b _ _ _ (Int.repr u) (Int.repr (Z.of_nat (length c)))); auto;
try solve [simpl; unfold lift; simpl;
first [rewrite HA5z | rewrite HA1z | rewrite HA2z | rewrite HA3z | rewrite HA4z |
rewrite HA2 | rewrite HA4 | rewrite HL2 | rewrite HL4]; auto].
inv Hmz; auto.
rewrite <- H2 in Hj_unused; inv Hj_unused.
simpl; inv match_related; split; congruence.
- rewrite Int.repr_unsigned; constructor.
- split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
inv match_related; constructor; auto.
econstructor; eauto.
assert (Int.unsigned j ≠ Int.unsigned i) as Hneq.
intro Hcon; rewrite Hcon in Hj_unused; rewrite Hj_unused in Hused; inv Hused.
assert (Int.unsigned j < Int.unsigned i ∨ Int.unsigned j > Int.unsigned i) as Hzi by omega.
intros i´ Hi´.
destruct (zeq i´ (Int.unsigned j)); subst; simpl.
Section container_init_ref.
Lemma container_init_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_init_spec) container_init_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (0 ≤ 0 < 64) as Hi0; try omega.
destruct (H 0 Hi0) as [v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
simpl in ×.
remember HA1 as HA1old; clear HeqHA1old.
remember HA2 as HA2old; clear HeqHA2old.
remember HA3 as HA3old; clear HeqHA3old.
remember HA4 as HA4old; clear HeqHA4old.
remember HA5 as HA5old; clear HeqHA5old.
apply Mem.valid_access_store with (v := Vint (Int.repr root_quota)) in HA1.
destruct HA1 as [m3 HA1].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1) in HA3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1) in HA4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1) in HA5.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA2.
destruct HA2 as [m4 HA2].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2) in HA3.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2) in HA4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2) in HA5.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA3.
destruct HA3 as [m5 HA3].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3) in HA4.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3) in HA5.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA4.
destruct HA4 as [m6 HA4].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4) in HA5.
apply Mem.valid_access_store with (v := Vint Int.one) in HA5.
destruct HA5 as [m7 HA5].
inv Hι.
inv H4; inv H6.
∃ ι, Vundef, m7, (d2 { ioapic
: DeviceStateDataType.update_s (ioapic d1)
(ioapic_init_aux (DeviceStateDataType.s (ioapic d1))
(Z.to_nat
(DeviceStateDataType.IoApicMaxIntr
(DeviceStateDataType.s (ioapic d1)) + 1 - 1)))} {
lapic
: DeviceStateDataType.update_l3
(DeviceStateDataType.update_l2
(DeviceStateDataType.update_l1
(DeviceStateDataType.mkLApicData
{|
DeviceStateDataType.LapicEsr := 0;
DeviceStateDataType.LapicEoi := DeviceStateDataType.NoIntr;
DeviceStateDataType.LapicMaxLvt := DeviceStateDataType.LapicMaxLvt
(DeviceStateDataType.s
(lapic d1));
DeviceStateDataType.LapicEnable := true;
DeviceStateDataType.LapicSpurious := 32 + 7;
DeviceStateDataType.LapicLint0Mask := true;
DeviceStateDataType.LapicLint1Mask := true;
DeviceStateDataType.LapicPcIntMask := true;
DeviceStateDataType.LapicLdr := 0;
DeviceStateDataType.LapicErrorIrq := 50;
DeviceStateDataType.LapicEsrClrPen := false;
DeviceStateDataType.LapicTpr := 0 |})
(DeviceStateDataType.l1 (lapic d1)))
(DeviceStateDataType.l2 (lapic d1)))
(DeviceStateDataType.l3 (lapic d1))} { ioapic / s /
CurrentIrq : None} {MM: real_mm} {MMSize: real_size} {vmxinfo: real_vmxinfo} {init : true}).
repeat (apply conj).
- apply (container_init_low_intro _ _ _ m7 m3 m4 m5 m6 d2 _ b); auto.
functional inversion H1; inv match_related; unfold bootloader0_spec.
rewrite <- pg_re0; rewrite H7.
rewrite <- ikern_re0; rewrite H5.
rewrite <- ihost_re0; rewrite H4.
rewrite in_intr_re0; rewrite H6.
rewrite ioapic_re0.
rewrite lapic_re0.
rewrite <- init_re0; rewrite H3; auto.
unfold container_init_spec in H1.
subdestruct.
reflexivity.
inv match_related.
unfold container_init_spec in H1.
subdestruct. eauto.
- constructor.
- functional inversion H1; inv match_related.
split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
constructor; auto.
econstructor; eauto.
intros i´ Hi´. unfold AC_init in ×.
destruct (zeq i´ 0); subst; simpl.
rewrite ZMap.gss.
∃ (Int.repr root_quota), Int.zero, Int.zero, Int.zero, Int.one.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
apply (Mem.load_store_same _ _ _ _ _ _ HA1).
simpl; unfold USAGE; right; left; omega.
simpl; unfold PARENT; right; left; omega.
simpl; unfold NCHILDREN; right; left; omega.
simpl; unfold USED; right; left; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
apply (Mem.load_store_same _ _ _ _ _ _ HA2).
simpl; unfold PARENT; right; left; omega.
simpl; unfold NCHILDREN; right; left; omega.
simpl; unfold USED; right; left; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
apply (Mem.load_store_same _ _ _ _ _ _ HA3).
simpl; unfold NCHILDREN; right; left; omega.
simpl; unfold USED; right; left; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
apply (Mem.load_store_same _ _ _ _ _ _ HA4).
simpl; unfold USED; right; left; omega.
split.
apply (Mem.load_store_same _ _ _ _ _ _ HA5).
repeat (split; try solve [
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1); auto]).
constructor; constructor; unfold Int.max_unsigned; simpl; omega.
rewrite ZMap.gso; auto.
destruct (H i´ Hi´) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1); auto.
simpl; unfold QUOTA; unfold CSIZE; right; right; omega.
simpl; unfold QUOTA; unfold USAGE; unfold CSIZE; right; right; omega.
simpl; unfold QUOTA; unfold PARENT; unfold CSIZE; right; right; omega.
simpl; unfold QUOTA; unfold NCHILDREN; unfold CSIZE; right; right; omega.
simpl; unfold QUOTA; unfold USED; unfold CSIZE; right; right; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1); auto.
simpl; unfold USAGE; unfold QUOTA; unfold CSIZE; right; right; omega.
simpl; unfold USAGE; unfold CSIZE; right; right; omega.
simpl; unfold USAGE; unfold PARENT; unfold CSIZE; right; right; omega.
simpl; unfold USAGE; unfold NCHILDREN; unfold CSIZE; right; right; omega.
simpl; unfold USAGE; unfold USED; unfold CSIZE; right; right; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1); auto.
simpl; unfold PARENT; unfold QUOTA; unfold CSIZE; right; right; omega.
simpl; unfold PARENT; unfold USAGE; unfold CSIZE; right; right; omega.
simpl; unfold PARENT; unfold CSIZE; right; right; omega.
simpl; unfold PARENT; unfold NCHILDREN; unfold CSIZE; right; right; omega.
simpl; unfold PARENT; unfold USED; unfold CSIZE; right; right; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1); auto.
simpl; unfold NCHILDREN; unfold QUOTA; unfold CSIZE; right; right; omega.
simpl; unfold NCHILDREN; unfold USAGE; unfold CSIZE; right; right; omega.
simpl; unfold NCHILDREN; unfold PARENT; unfold CSIZE; right; right; omega.
simpl; unfold NCHILDREN; unfold CSIZE; right; right; omega.
simpl; unfold NCHILDREN; unfold USED; unfold CSIZE; right; right; omega.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1); auto.
simpl; unfold USED; unfold QUOTA; unfold CSIZE; right; right; omega.
simpl; unfold USED; unfold USAGE; unfold CSIZE; right; right; omega.
simpl; unfold USED; unfold PARENT; unfold CSIZE; right; right; omega.
simpl; unfold USED; unfold NCHILDREN; unfold CSIZE; right; right; omega.
simpl; unfold USED; unfold CSIZE; right; right; omega.
repeat (split; try solve [
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1); auto]).
rewrite ZMap.gi.
inv Hm´.
constructor.
pose proof (valid_preinit_container _ Hhigh´ H3 _ Hi´) as _x2.
rewrite <- H2 in _x2; contradict _x2; auto.
- auto.
Qed.
End container_init_ref.
Section container_get_parent_ref.
Lemma container_get_parent_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_get_parent_spec)
container_get_parent_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H8; inv H10.
inv Hhigh´.
destruct valid_container.
specialize (cvalid_id _ H3).
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H7 in H3; inv H3.
rewrite <- H6 in H1.
simpl in H1; subst.
rewrite Int.repr_unsigned in HL3; auto.
simpl; inv match_related; split; congruence.
- constructor.
- assumption.
- auto.
Qed.
End container_get_parent_ref.
Section container_get_quota_ref.
Lemma container_get_quota_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_get_quota_spec)
container_get_quota_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H8; inv H10.
inv Hhigh´.
destruct valid_container.
specialize (cvalid_id _ H3).
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H7 in H3; inv H3.
rewrite <- H6 in H1.
simpl in H1; subst.
rewrite Int.repr_unsigned in HL1; auto.
simpl; inv match_related; split; congruence.
- constructor.
- assumption.
- auto.
Qed.
End container_get_quota_ref.
Section container_get_usage_ref.
Lemma container_get_usage_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_get_usage_spec)
container_get_usage_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H8; inv H10.
inv Hhigh´.
destruct valid_container.
specialize (cvalid_id _ H3).
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H7 in H3; inv H3.
rewrite <- H6 in H1.
simpl in H1; subst.
rewrite Int.repr_unsigned in HL2; auto.
simpl; inv match_related; split; congruence.
- constructor.
- assumption.
- auto.
Qed.
End container_get_usage_ref.
Section container_can_consume_ref.
Lemma container_can_consume_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_can_consume_spec)
container_can_consume_spec_low.
Proof.
compatsim_simpl (@match_AbData).
inv Hι.
inv H4; inv H6.
inv H4; inv H7.
rename i0 into n.
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- functional inversion H2.
× inv Hhigh´.
destruct valid_container.
specialize (cvalid_id _ H3).
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H3; inv H3.
replace z with
(match (Int.unsigned n <=? Int.unsigned (Int.repr (cquota (ZMap.get (Int.unsigned i) (AC d1´)))),
Int.unsigned (Int.repr (cusage (ZMap.get (Int.unsigned i) (AC d1´)))) <=?
Int.unsigned (Int.repr (cquota (ZMap.get (Int.unsigned i) (AC d1´)))) - Int.unsigned n) with
| (true, true) ⇒ Int.one
| _ ⇒ Int.zero end).
econstructor; eauto.
rewrite <- H7; auto.
rewrite <- H7; auto.
simpl; inv match_related; split; congruence.
specialize (cvalid_quota _ H3); specialize (cvalid_usage _ H3).
rewrite 2 Int.unsigned_repr; try omega.
assert (Hle1: Int.unsigned n ≤ cquota (ZMap.get (Int.unsigned i) (AC d1´))) by omega.
assert (Hle2: cusage (ZMap.get (Int.unsigned i) (AC d1´)) ≤
cquota (ZMap.get (Int.unsigned i) (AC d1´)) - Int.unsigned n) by omega.
rewrite <- Z.leb_le in Hle1, Hle2; rewrite Hle1, Hle2.
apply f_equal with (f := Int.repr) in H1.
rewrite Int.repr_unsigned in H1; auto.
× inv Hhigh´.
destruct valid_container.
specialize (cvalid_id _ H3).
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H3; inv H3.
replace z with
(match (Int.unsigned n <=? Int.unsigned (Int.repr (cquota (ZMap.get (Int.unsigned i) (AC d1´)))),
Int.unsigned (Int.repr (cusage (ZMap.get (Int.unsigned i) (AC d1´)))) <=?
Int.unsigned (Int.repr (cquota (ZMap.get (Int.unsigned i) (AC d1´)))) - Int.unsigned n) with
| (true, true) ⇒ Int.one
| _ ⇒ Int.zero end).
econstructor; eauto.
rewrite <- H7; auto.
rewrite <- H7; auto.
simpl; inv match_related; split; congruence.
specialize (cvalid_quota _ H3); specialize (cvalid_usage _ H3).
rewrite 2 Int.unsigned_repr; try omega.
assert (Hrange:= Int.unsigned_range n).
assert (Hle: ¬ Int.unsigned n ≤ cquota (ZMap.get (Int.unsigned i) (AC d1´)) ∨
¬ cusage (ZMap.get (Int.unsigned i) (AC d1´)) ≤
cquota (ZMap.get (Int.unsigned i) (AC d1´)) - Int.unsigned n) by omega.
rewrite <- Z.leb_le in Hle; rewrite <- Z.leb_le in Hle; destruct Hle as [Hle|Hle].
destruct (Int.unsigned n <=? cquota (ZMap.get (Int.unsigned i) (AC d1´))).
contradict Hle; auto.
apply f_equal with (f := Int.repr) in H1.
rewrite Int.repr_unsigned in H1; auto.
destruct (cusage (ZMap.get (Int.unsigned i) (AC d1´)) <=?
cquota (ZMap.get (Int.unsigned i) (AC d1´)) - Int.unsigned n).
contradict Hle; auto.
apply f_equal with (f := Int.repr) in H1.
rewrite Int.repr_unsigned in H1.
destruct (Int.unsigned n <=? cquota (ZMap.get (Int.unsigned i) (AC d1´))); auto.
- constructor.
- assumption.
- auto.
Qed.
End container_can_consume_ref.
Section container_split_ref.
Lemma norepet_nodup {A} :
∀ l : list A, list_norepet l ↔ NoDup l.
Proof.
induction l; split; intros.
constructor.
constructor.
inv H; constructor; auto.
apply IHl; auto.
inv H; constructor; auto.
apply IHl; auto.
Qed.
Lemma nodup_length_ub :
∀ l l´, incl(A:=Z) l l´ → NoDup l → (length l ≤ length l´)%nat.
Proof.
intros l l´; rewrite <- norepet_nodup.
intros; apply PTree_Properties.list_incl_length; auto.
Qed.
Fixpoint build_range (n : nat) (z : Z) : list Z :=
match n with
| O ⇒ nil
| S n ⇒ z :: build_range n (z+1)
end.
Lemma build_range_length :
∀ n z, length (build_range n z) = n.
Proof.
induction n; simpl; auto.
Qed.
Lemma build_range_charact :
∀ n z z´, In z´ (build_range n z) ↔ z ≤ z´ < z + Z_of_nat n.
Proof.
induction n; intros.
simpl; omega.
rewrite Nat2Z.inj_succ; simpl; split; intros.
destruct H; subst; try omega.
rewrite IHn in H; omega.
rewrite IHn; omega.
Qed.
Lemma nodup_length :
∀ l a b,
a ≤ b → NoDup l → Forall (fun z ⇒ a ≤ z < b) l → Z_of_nat (length l) ≤ b - a.
Proof.
intros l a b Hle Hnodup Hrange.
rewrite <- nat_of_Z_eq; try omega; apply inj_le.
rewrite <- (build_range_length (nat_of_Z (b-a)) a).
apply nodup_length_ub; auto.
unfold incl; intros z Hin.
rewrite Forall_forall in Hrange; specialize (Hrange z Hin).
rewrite build_range_charact.
rewrite nat_of_Z_eq; omega.
Qed.
Lemma container_split_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_split_spec)
container_split_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H1; subst c cur child.
replace z with (Int.repr (Int.unsigned z)); try apply Int.repr_unsigned.
rewrite <- H3 in *; clear H3 z.
rename i0 into n, i1 into j, H0 into Hfind, _x into Hh, _x0 into Hn,
H6 into Hj_unused, H7 into Hused; clear H4 H5.
inv Hhigh´.
destruct valid_container.
assert (cvalid_id´:= cvalid_id); specialize (cvalid_id _ Hused).
destruct (H (Int.unsigned i) cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
assert (0 ≤ Int.unsigned j < num_id) as Hj; try omega.
destruct (H (Int.unsigned j) Hj) as
[v1z[v2z[v3z[v4z[v5z[HL1z[HL2z[HL3z[HL4z[HL5z[HA1z[HA2z[HA3z[HA4z[HA5z Hmz]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H2 in Hused; inv Hused.
inv Hι.
inv H4; inv H6.
inv H4; inv H13.
inv H4; inv H6.
simpl in ×.
assert (HA1old := HA1).
assert (HA2old := HA2).
assert (HA3old := HA3).
assert (HA4old := HA4).
assert (HA5old := HA5).
assert (HA1zold := HA1z).
assert (HA2zold := HA2z).
assert (HA3zold := HA3z).
assert (HA4zold := HA4z).
assert (HA5zold := HA5z).
apply Mem.valid_access_store with (v := Vint Int.one) in HA5z.
destruct HA5z as [m3 HA5z].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA1z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA2z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA3z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA4z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z) in HA4.
apply Mem.valid_access_store with (v := Vint n) in HA1z.
destruct HA1z as [m4 HA1z].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z) in HA2z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z) in HA3z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z) in HA4z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z) in HA4.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA2z.
destruct HA2z as [m5 HA2z].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z) in HA3z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z) in HA4z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z) in HA4.
apply Mem.valid_access_store with (v := Vint i) in HA3z.
destruct HA3z as [m6 HA3z].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z) in HA4z.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z) in HA4.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA4z.
destruct HA4z as [m7 HA4z].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4z) in HA2.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4z) in HA4.
apply Mem.valid_access_store with (v := Vint (Int.add (Int.repr u) n)) in HA2.
destruct HA2 as [m8 HA2].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2) in HA4.
apply Mem.valid_access_store with (v := Vint (Int.add (Int.repr (Z.of_nat (length c))) Int.one)) in HA4.
destruct HA4 as [m9 HA4].
rename H7 into Hmq, H10 into Hmu, H11 into Hmp, H12 into Hmc.
∃ ι, (Vint j), m9, d2; repeat (apply conj).
- apply (container_split_low_step_intro _ _ _ _
(m3,d2) (m4,d2) (m5,d2) (m6,d2) (m7,d2) (m8,d2)
b _ _ _ (Int.repr u) (Int.repr (Z.of_nat (length c)))); auto;
try solve [simpl; unfold lift; simpl;
first [rewrite HA5z | rewrite HA1z | rewrite HA2z | rewrite HA3z | rewrite HA4z |
rewrite HA2 | rewrite HA4 | rewrite HL2 | rewrite HL4]; auto].
inv Hmz; auto.
rewrite <- H2 in Hj_unused; inv Hj_unused.
simpl; inv match_related; split; congruence.
- rewrite Int.repr_unsigned; constructor.
- split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
inv match_related; constructor; auto.
econstructor; eauto.
assert (Int.unsigned j ≠ Int.unsigned i) as Hneq.
intro Hcon; rewrite Hcon in Hj_unused; rewrite Hj_unused in Hused; inv Hused.
assert (Int.unsigned j < Int.unsigned i ∨ Int.unsigned j > Int.unsigned i) as Hzi by omega.
intros i´ Hi´.
destruct (zeq i´ (Int.unsigned j)); subst; simpl.
CASE 1: i' is the newly-added child
rewrite ZMap.gss.
∃ (Int.repr (Int.unsigned n)), (Int.repr 0), (Int.repr (Int.unsigned i)), (Int.repr 0), Int.one.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z).
rewrite Int.repr_unsigned; apply (Mem.load_store_same _ _ _ _ _ _ HA1z).
simpl; unfold CSIZE; unfold QUOTA; unfold USAGE; right; left; omega.
simpl; unfold CSIZE; unfold QUOTA; unfold PARENT; right; left; omega.
simpl; unfold CSIZE; unfold QUOTA; unfold NCHILDREN; right; left; omega.
simpl; unfold CSIZE; unfold QUOTA; unfold USAGE; destruct Hzi;
[right; left; omega | right; right; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold NCHILDREN; destruct Hzi;
[right; left; omega | right; right; omega].
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
apply (Mem.load_store_same _ _ _ _ _ _ HA2z).
simpl; unfold CSIZE; unfold USAGE; unfold PARENT; right; left; omega.
simpl; unfold CSIZE; unfold USAGE; unfold NCHILDREN; right; left; omega.
simpl; unfold CSIZE; unfold USAGE; unfold USAGE; destruct Hzi;
[right; left; omega | right; right; omega].
simpl; unfold CSIZE; unfold USAGE; unfold NCHILDREN; destruct Hzi;
[right; left; omega | right; right; omega].
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite Int.repr_unsigned; apply (Mem.load_store_same _ _ _ _ _ _ HA3z).
simpl; unfold CSIZE; unfold PARENT; unfold NCHILDREN; right; left; omega.
simpl; unfold CSIZE; unfold PARENT; unfold USAGE; destruct Hzi;
[right; left; omega | right; right; omega].
simpl; unfold CSIZE; unfold PARENT; unfold NCHILDREN; destruct Hzi;
[right; left; omega | right; right; omega].
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
apply (Mem.load_store_same _ _ _ _ _ _ HA4z).
simpl; unfold CSIZE; unfold NCHILDREN; unfold USAGE; destruct Hzi;
[right; left; omega | right; right; omega].
simpl; unfold CSIZE; unfold NCHILDREN; unfold NCHILDREN; destruct Hzi;
[right; left; omega | right; right; omega].
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z).
apply (Mem.load_store_same _ _ _ _ _ _ HA5z).
simpl; unfold CSIZE; unfold USED; unfold QUOTA; right; right; omega.
simpl; unfold CSIZE; unfold USED; unfold USAGE; right; right; omega.
simpl; unfold CSIZE; unfold USED; unfold PARENT; right; right; omega.
simpl; unfold CSIZE; unfold USED; unfold NCHILDREN; right; right; omega.
simpl; unfold CSIZE; unfold USED; unfold USAGE; destruct Hzi;
[right; left; omega | right; right; omega].
simpl; unfold CSIZE; unfold USED; unfold NCHILDREN; destruct Hzi;
[right; left; omega | right; right; omega].
repeat (split; try solve [
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z); auto]).
constructor; constructor;
try solve [apply Int.unsigned_range_2];
try solve [unfold Int.max_unsigned; simpl; omega].
rewrite ZMap.gso; auto.
destruct (zeq i´ (Int.unsigned i)); subst.
∃ (Int.repr (Int.unsigned n)), (Int.repr 0), (Int.repr (Int.unsigned i)), (Int.repr 0), Int.one.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z).
rewrite Int.repr_unsigned; apply (Mem.load_store_same _ _ _ _ _ _ HA1z).
simpl; unfold CSIZE; unfold QUOTA; unfold USAGE; right; left; omega.
simpl; unfold CSIZE; unfold QUOTA; unfold PARENT; right; left; omega.
simpl; unfold CSIZE; unfold QUOTA; unfold NCHILDREN; right; left; omega.
simpl; unfold CSIZE; unfold QUOTA; unfold USAGE; destruct Hzi;
[right; left; omega | right; right; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold NCHILDREN; destruct Hzi;
[right; left; omega | right; right; omega].
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
apply (Mem.load_store_same _ _ _ _ _ _ HA2z).
simpl; unfold CSIZE; unfold USAGE; unfold PARENT; right; left; omega.
simpl; unfold CSIZE; unfold USAGE; unfold NCHILDREN; right; left; omega.
simpl; unfold CSIZE; unfold USAGE; unfold USAGE; destruct Hzi;
[right; left; omega | right; right; omega].
simpl; unfold CSIZE; unfold USAGE; unfold NCHILDREN; destruct Hzi;
[right; left; omega | right; right; omega].
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite Int.repr_unsigned; apply (Mem.load_store_same _ _ _ _ _ _ HA3z).
simpl; unfold CSIZE; unfold PARENT; unfold NCHILDREN; right; left; omega.
simpl; unfold CSIZE; unfold PARENT; unfold USAGE; destruct Hzi;
[right; left; omega | right; right; omega].
simpl; unfold CSIZE; unfold PARENT; unfold NCHILDREN; destruct Hzi;
[right; left; omega | right; right; omega].
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
apply (Mem.load_store_same _ _ _ _ _ _ HA4z).
simpl; unfold CSIZE; unfold NCHILDREN; unfold USAGE; destruct Hzi;
[right; left; omega | right; right; omega].
simpl; unfold CSIZE; unfold NCHILDREN; unfold NCHILDREN; destruct Hzi;
[right; left; omega | right; right; omega].
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z).
apply (Mem.load_store_same _ _ _ _ _ _ HA5z).
simpl; unfold CSIZE; unfold USED; unfold QUOTA; right; right; omega.
simpl; unfold CSIZE; unfold USED; unfold USAGE; right; right; omega.
simpl; unfold CSIZE; unfold USED; unfold PARENT; right; right; omega.
simpl; unfold CSIZE; unfold USED; unfold NCHILDREN; right; right; omega.
simpl; unfold CSIZE; unfold USED; unfold USAGE; destruct Hzi;
[right; left; omega | right; right; omega].
simpl; unfold CSIZE; unfold USED; unfold NCHILDREN; destruct Hzi;
[right; left; omega | right; right; omega].
repeat (split; try solve [
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z); auto]).
constructor; constructor;
try solve [apply Int.unsigned_range_2];
try solve [unfold Int.max_unsigned; simpl; omega].
rewrite ZMap.gso; auto.
destruct (zeq i´ (Int.unsigned i)); subst.
CASE 2: i' is the parent that we split
rewrite ZMap.gss.
∃ (Int.repr q), (Int.repr (u + Int.unsigned n)), (Int.repr p),
(Int.repr (Z.of_nat (length (Int.unsigned j :: c)))), Int.one.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); auto.
simpl; unfold CSIZE; unfold QUOTA; unfold USED; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold QUOTA; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold USAGE; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold PARENT; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold NCHILDREN; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold USAGE; right; left; omega.
simpl; unfold CSIZE; unfold QUOTA; unfold NCHILDREN; right; left; omega.
split.
rewrite Int.add_unsigned in HA2; rewrite Int.unsigned_repr in HA2.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
apply (Mem.load_store_same _ _ _ _ _ _ HA2).
simpl; unfold CSIZE; unfold USAGE; unfold NCHILDREN; right; left; omega.
inv Hmu; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); auto.
simpl; unfold CSIZE; unfold PARENT; unfold USED; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold PARENT; unfold QUOTA; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold PARENT; unfold USAGE; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold PARENT; unfold PARENT; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold PARENT; unfold NCHILDREN; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold PARENT; unfold USAGE; right; right; omega.
simpl; unfold CSIZE; unfold PARENT; unfold NCHILDREN; right; left; omega.
split.
rewrite Int.add_unsigned in HA4; rewrite Int.unsigned_repr in HA4.
replace (Z.of_nat (length (Int.unsigned j :: c))) with (Z.of_nat (length c) + 1).
apply (Mem.load_store_same _ _ _ _ _ _ HA4).
replace 1 with (Z.of_nat 1); try solve [simpl; auto].
rewrite <- Nat2Z.inj_add; rewrite plus_comm; simpl; auto.
inv Hmc; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); auto.
simpl; unfold CSIZE; unfold USED; unfold USED; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold USED; unfold QUOTA; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold USED; unfold USAGE; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold USED; unfold PARENT; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold USED; unfold NCHILDREN; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold USED; unfold USAGE; right; right; omega.
simpl; unfold CSIZE; unfold USED; unfold NCHILDREN; right; right; omega.
repeat (split; try solve [
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z); auto]).
constructor; auto.
constructor; split.
apply Z.add_nonneg_nonneg.
inv Hmu; omega.
apply Int.unsigned_range_2.
apply Zle_trans with (m := q).
rewrite <- H0 in Hn; simpl in Hn; omega.
inv Hmq; omega.
constructor; split.
apply Zle_0_nat.
rewrite max_unsigned_val; apply Z.le_trans with (m:= num_id - 0); try omega.
apply nodup_length; try omega.
specialize (cvalid_nodup (Int.unsigned i)).
rewrite <- H0 in cvalid_nodup; simpl in cvalid_nodup; specialize (cvalid_nodup eq_refl).
constructor; auto.
specialize (cvalid_children_used (Int.unsigned i)).
rewrite Forall_forall in cvalid_children_used.
replace c with (cchildren (ZMap.get (Int.unsigned i) (AC d1))); try solve [rewrite <- H0; auto].
intro Hcon; specialize (cvalid_children_used Hused _ Hcon); congruence.
rewrite Forall_forall; intros x Hin.
inv Hin; auto.
specialize (cvalid_children_used (Int.unsigned i)).
rewrite Forall_forall in cvalid_children_used.
replace c with (cchildren (ZMap.get (Int.unsigned i) (AC d1))) in H2; try solve [rewrite <- H0; auto].
apply (cvalid_id´ _ (cvalid_children_used Hused _ H2)).
rewrite ZMap.gso; auto.
destruct (H _ Hi´) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
assert (∀ m k1 k2 a b : Z, a ≠ b → 0 ≤ m →
0 ≤ k1 → k1 + size_chunk Mint32 ≤ m → 0 ≤ k2 → k2 + size_chunk Mint32 ≤ m →
a × m + k1 + size_chunk Mint32 ≤ b × m + k2 ∨ b × m + k2 + size_chunk Mint32 ≤ a × m + k1) as Hsep.
intros m k1 k2 a1 a2 Ha_neq Hm_0 Hk1_0 Hle1 Hk2_0 Hle2.
assert (a1 < a2 ∨ a2 < a1) as Ha; try omega.
destruct Ha; [left | right].
apply Z.le_trans with (m := a1 × m + m); try omega.
replace (a1 × m + m) with ((a1 + 1) × m).
assert (a1 + 1 ≤ a2) as Hle_a; try omega.
apply Z.mul_le_mono_nonneg_r with (p := m) in Hle_a; auto; omega.
rewrite Z.mul_add_distr_r; omega.
apply Z.le_trans with (m := a2 × m + m); try omega.
replace (a2 × m + m) with ((a2 + 1) × m).
assert (a2 + 1 ≤ a1) as Hle_a; try omega.
apply Z.mul_le_mono_nonneg_r with (p := m) in Hle_a; auto; omega.
rewrite Z.mul_add_distr_r; omega.
unfold CSIZE in *; unfold QUOTA in *; unfold USAGE in *;
unfold PARENT in *; unfold NCHILDREN in *; unfold USED in ×.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); try solve [right; apply Hsep; simpl; auto; try omega]; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); try solve [right; apply Hsep; simpl; auto; try omega]; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); try solve [right; apply Hsep; simpl; auto; try omega]; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); try solve [right; apply Hsep; simpl; auto; try omega]; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); try solve [right; apply Hsep; simpl; auto; try omega]; auto.
repeat (split; try solve [
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z); auto]).
assumption.
- auto.
Qed.
End container_split_ref.
Section container_alloc_ref.
Lemma container_alloc_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_alloc_spec)
container_alloc_spec_low.
Proof.
constructor; split; simpl in *; try reflexivity; [|apply res_le_error].
intros s WB1 WB2 ι vargs1 m1 d1 vres1 m1´ d1´ vargs2 m2 d2
HWB _ Hlow Hhigh Hhigh´ H Hι Hmd.
compatsim_simpl_inv_match H Hmd @match_AbData.
inv Hι.
inv H4; inv H6.
inv Hhigh´.
destruct valid_container.
functional inversion H1; subst c cur.
{
specialize (cvalid_id _ H4).
destruct (H _ cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
assert (HA2old := HA2).
apply Mem.valid_access_store with (v := Vint (Int.add v2 Int.one)) in HA2.
destruct HA2 as [m2´ HA2].
∃ ι, Vone, m2´, d2; repeat (apply conj).
- econstructor; eauto.
inv Hm.
rewrite <- H10 in H4; inv H4.
rewrite <- H9 in H8; rewrite Z.ltb_lt in H8; simpl in H8.
rewrite 2 Int.unsigned_repr; auto.
inv H15; auto.
inv H16; auto.
simpl; unfold lift; simpl; rewrite HA2; auto.
simpl; inv match_related; split; congruence.
- apply f_equal with (f:= Int.repr) in H3.
rewrite Int.repr_unsigned in H3; subst; constructor.
- split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
econstructor; eauto.
intros i´ Hi´.
unfold QUOTA in *; unfold USAGE in *; unfold PARENT in *; unfold NCHILDREN in *;
unfold USED in *; unfold CSIZE in ×.
destruct (zeq i´ (Int.unsigned i)); subst.
∃ v1, (Int.add v2 Int.one), v3, v4, v5.
repeat (split; try solve
[(rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); auto; right; left; simpl; omega) |
(rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); auto; right; right; simpl; omega) |
(apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2); auto)]).
rewrite (Mem.load_store_same _ _ _ _ _ _ HA2); auto.
inv Hm; simpl; rewrite ZMap.gss.
rewrite <- H9 in H4; inv H4.
replace (Int.add (Int.repr u) Int.one) with (Int.repr (u+1)).
constructor; auto.
constructor; split.
inv H15; omega.
inv H15; inv H14.
rewrite Z.ltb_lt in H8; rewrite <- H2 in H8; simpl in H8; omega.
inv H15.
rewrite <- (Int.unsigned_repr _ H9) at 1; auto.
destruct (H _ Hi´) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
assert (∀ m k1 k2 a b : Z,
a ≠ b → 0 ≤ m → 0 ≤ k1 → k1 + size_chunk Mint32 ≤ m →
0 ≤ k2 → k2 + size_chunk Mint32 ≤ m →
a × m + k1 + size_chunk Mint32 ≤ b × m + k2 ∨
b × m + k2 + size_chunk Mint32 ≤ a × m + k1) as Hsep.
intros m k1 k2 a1 a2 Ha_neq Hm_0 Hk1_0 Hle1 Hk2_0 Hle2.
assert (a1 < a2 ∨ a2 < a1) as Ha; try omega.
destruct Ha; [left | right].
apply Z.le_trans with (m := a1 × m + m); try omega.
replace (a1 × m + m) with ((a1 + 1) × m).
assert (a1 + 1 ≤ a2) as Hle_a; try omega.
apply Z.mul_le_mono_nonneg_r with (p := m) in Hle_a; auto; omega.
rewrite Z.mul_add_distr_r; omega.
apply Z.le_trans with (m := a2 × m + m); try omega.
replace (a2 × m + m) with ((a2 + 1) × m).
assert (a2 + 1 ≤ a1) as Hle_a; try omega.
apply Z.mul_le_mono_nonneg_r with (p := m) in Hle_a; auto; omega.
rewrite Z.mul_add_distr_r; omega.
repeat (split; try solve
[(rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); auto; right;
apply Hsep; simpl; auto; try omega) |
(apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2); auto)]).
simpl; rewrite ZMap.gso; auto.
- auto.
}
{
subst; specialize (cvalid_id _ H4).
destruct (H _ cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ ι, Vzero, m2, d2; repeat (apply conj).
- econstructor; eauto.
inv Hm.
rewrite <- H9 in H4; inv H4.
specialize (cvalid_usage _ H4).
rewrite <- H2 in H8, cvalid_usage; simpl in H8, cvalid_usage; rewrite Z.ltb_nlt in H8.
assert (u = q) by omega; subst; auto.
simpl; inv match_related; split; congruence.
- apply f_equal with (f:= Int.repr) in H3.
rewrite Int.repr_unsigned in H3; subst; constructor.
- split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
- auto.
}
Qed.
End container_alloc_ref.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store´) (lflatmem_store:= flatmem_store´)).
Proof.
accessor_prop_tac.
- eapply flatmem_store´_exists; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) mcontainer_passthrough dabshandler.
Proof.
sim_oplus_split_final (cdata LDATA).
- apply fload´_sim.
- apply fstore´_sim.
- apply flatmem_copy´_sim.
- apply vmxinfo_get_sim.
- apply setPG_sim.
- apply setCR3_sim.
- apply get_size_sim.
- apply is_mm_usable_sim.
- apply get_mm_s_sim.
- apply get_mm_l_sim.
- apply cli_sim.
- apply sti_sim.
- apply cons_buf_read_sim.
- apply serial_putc_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply trapin_sim.
- apply trapout´_sim.
- apply hostin_sim.
- apply hostout´_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End OneStep_Forward_Relation.
End WITHMEM.
End Refinement.
∃ (Int.repr q), (Int.repr (u + Int.unsigned n)), (Int.repr p),
(Int.repr (Z.of_nat (length (Int.unsigned j :: c)))), Int.one.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); auto.
simpl; unfold CSIZE; unfold QUOTA; unfold USED; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold QUOTA; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold USAGE; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold PARENT; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold NCHILDREN; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold QUOTA; unfold USAGE; right; left; omega.
simpl; unfold CSIZE; unfold QUOTA; unfold NCHILDREN; right; left; omega.
split.
rewrite Int.add_unsigned in HA2; rewrite Int.unsigned_repr in HA2.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
apply (Mem.load_store_same _ _ _ _ _ _ HA2).
simpl; unfold CSIZE; unfold USAGE; unfold NCHILDREN; right; left; omega.
inv Hmu; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); auto.
simpl; unfold CSIZE; unfold PARENT; unfold USED; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold PARENT; unfold QUOTA; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold PARENT; unfold USAGE; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold PARENT; unfold PARENT; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold PARENT; unfold NCHILDREN; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold PARENT; unfold USAGE; right; right; omega.
simpl; unfold CSIZE; unfold PARENT; unfold NCHILDREN; right; left; omega.
split.
rewrite Int.add_unsigned in HA4; rewrite Int.unsigned_repr in HA4.
replace (Z.of_nat (length (Int.unsigned j :: c))) with (Z.of_nat (length c) + 1).
apply (Mem.load_store_same _ _ _ _ _ _ HA4).
replace 1 with (Z.of_nat 1); try solve [simpl; auto].
rewrite <- Nat2Z.inj_add; rewrite plus_comm; simpl; auto.
inv Hmc; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); auto.
simpl; unfold CSIZE; unfold USED; unfold USED; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold USED; unfold QUOTA; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold USED; unfold USAGE; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold USED; unfold PARENT; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold USED; unfold NCHILDREN; destruct Hzi;
[right; right; omega | right; left; omega].
simpl; unfold CSIZE; unfold USED; unfold USAGE; right; right; omega.
simpl; unfold CSIZE; unfold USED; unfold NCHILDREN; right; right; omega.
repeat (split; try solve [
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z); auto]).
constructor; auto.
constructor; split.
apply Z.add_nonneg_nonneg.
inv Hmu; omega.
apply Int.unsigned_range_2.
apply Zle_trans with (m := q).
rewrite <- H0 in Hn; simpl in Hn; omega.
inv Hmq; omega.
constructor; split.
apply Zle_0_nat.
rewrite max_unsigned_val; apply Z.le_trans with (m:= num_id - 0); try omega.
apply nodup_length; try omega.
specialize (cvalid_nodup (Int.unsigned i)).
rewrite <- H0 in cvalid_nodup; simpl in cvalid_nodup; specialize (cvalid_nodup eq_refl).
constructor; auto.
specialize (cvalid_children_used (Int.unsigned i)).
rewrite Forall_forall in cvalid_children_used.
replace c with (cchildren (ZMap.get (Int.unsigned i) (AC d1))); try solve [rewrite <- H0; auto].
intro Hcon; specialize (cvalid_children_used Hused _ Hcon); congruence.
rewrite Forall_forall; intros x Hin.
inv Hin; auto.
specialize (cvalid_children_used (Int.unsigned i)).
rewrite Forall_forall in cvalid_children_used.
replace c with (cchildren (ZMap.get (Int.unsigned i) (AC d1))) in H2; try solve [rewrite <- H0; auto].
apply (cvalid_id´ _ (cvalid_children_used Hused _ H2)).
rewrite ZMap.gso; auto.
destruct (H _ Hi´) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
assert (∀ m k1 k2 a b : Z, a ≠ b → 0 ≤ m →
0 ≤ k1 → k1 + size_chunk Mint32 ≤ m → 0 ≤ k2 → k2 + size_chunk Mint32 ≤ m →
a × m + k1 + size_chunk Mint32 ≤ b × m + k2 ∨ b × m + k2 + size_chunk Mint32 ≤ a × m + k1) as Hsep.
intros m k1 k2 a1 a2 Ha_neq Hm_0 Hk1_0 Hle1 Hk2_0 Hle2.
assert (a1 < a2 ∨ a2 < a1) as Ha; try omega.
destruct Ha; [left | right].
apply Z.le_trans with (m := a1 × m + m); try omega.
replace (a1 × m + m) with ((a1 + 1) × m).
assert (a1 + 1 ≤ a2) as Hle_a; try omega.
apply Z.mul_le_mono_nonneg_r with (p := m) in Hle_a; auto; omega.
rewrite Z.mul_add_distr_r; omega.
apply Z.le_trans with (m := a2 × m + m); try omega.
replace (a2 × m + m) with ((a2 + 1) × m).
assert (a2 + 1 ≤ a1) as Hle_a; try omega.
apply Z.mul_le_mono_nonneg_r with (p := m) in Hle_a; auto; omega.
rewrite Z.mul_add_distr_r; omega.
unfold CSIZE in *; unfold QUOTA in *; unfold USAGE in *;
unfold PARENT in *; unfold NCHILDREN in *; unfold USED in ×.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); try solve [right; apply Hsep; simpl; auto; try omega]; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); try solve [right; apply Hsep; simpl; auto; try omega]; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); try solve [right; apply Hsep; simpl; auto; try omega]; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); try solve [right; apply Hsep; simpl; auto; try omega]; auto.
split.
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA4z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA3z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA2z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA1z); try solve [right; apply Hsep; simpl; auto; try omega].
rewrite (Mem.load_store_other _ _ _ _ _ _ HA5z); try solve [right; apply Hsep; simpl; auto; try omega]; auto.
repeat (split; try solve [
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA4z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA3z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA1z);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA5z); auto]).
assumption.
- auto.
Qed.
End container_split_ref.
Section container_alloc_ref.
Lemma container_alloc_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_alloc_spec)
container_alloc_spec_low.
Proof.
constructor; split; simpl in *; try reflexivity; [|apply res_le_error].
intros s WB1 WB2 ι vargs1 m1 d1 vres1 m1´ d1´ vargs2 m2 d2
HWB _ Hlow Hhigh Hhigh´ H Hι Hmd.
compatsim_simpl_inv_match H Hmd @match_AbData.
inv Hι.
inv H4; inv H6.
inv Hhigh´.
destruct valid_container.
functional inversion H1; subst c cur.
{
specialize (cvalid_id _ H4).
destruct (H _ cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
assert (HA2old := HA2).
apply Mem.valid_access_store with (v := Vint (Int.add v2 Int.one)) in HA2.
destruct HA2 as [m2´ HA2].
∃ ι, Vone, m2´, d2; repeat (apply conj).
- econstructor; eauto.
inv Hm.
rewrite <- H10 in H4; inv H4.
rewrite <- H9 in H8; rewrite Z.ltb_lt in H8; simpl in H8.
rewrite 2 Int.unsigned_repr; auto.
inv H15; auto.
inv H16; auto.
simpl; unfold lift; simpl; rewrite HA2; auto.
simpl; inv match_related; split; congruence.
- apply f_equal with (f:= Int.repr) in H3.
rewrite Int.repr_unsigned in H3; subst; constructor.
- split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
econstructor; eauto.
intros i´ Hi´.
unfold QUOTA in *; unfold USAGE in *; unfold PARENT in *; unfold NCHILDREN in *;
unfold USED in *; unfold CSIZE in ×.
destruct (zeq i´ (Int.unsigned i)); subst.
∃ v1, (Int.add v2 Int.one), v3, v4, v5.
repeat (split; try solve
[(rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); auto; right; left; simpl; omega) |
(rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); auto; right; right; simpl; omega) |
(apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2); auto)]).
rewrite (Mem.load_store_same _ _ _ _ _ _ HA2); auto.
inv Hm; simpl; rewrite ZMap.gss.
rewrite <- H9 in H4; inv H4.
replace (Int.add (Int.repr u) Int.one) with (Int.repr (u+1)).
constructor; auto.
constructor; split.
inv H15; omega.
inv H15; inv H14.
rewrite Z.ltb_lt in H8; rewrite <- H2 in H8; simpl in H8; omega.
inv H15.
rewrite <- (Int.unsigned_repr _ H9) at 1; auto.
destruct (H _ Hi´) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
assert (∀ m k1 k2 a b : Z,
a ≠ b → 0 ≤ m → 0 ≤ k1 → k1 + size_chunk Mint32 ≤ m →
0 ≤ k2 → k2 + size_chunk Mint32 ≤ m →
a × m + k1 + size_chunk Mint32 ≤ b × m + k2 ∨
b × m + k2 + size_chunk Mint32 ≤ a × m + k1) as Hsep.
intros m k1 k2 a1 a2 Ha_neq Hm_0 Hk1_0 Hle1 Hk2_0 Hle2.
assert (a1 < a2 ∨ a2 < a1) as Ha; try omega.
destruct Ha; [left | right].
apply Z.le_trans with (m := a1 × m + m); try omega.
replace (a1 × m + m) with ((a1 + 1) × m).
assert (a1 + 1 ≤ a2) as Hle_a; try omega.
apply Z.mul_le_mono_nonneg_r with (p := m) in Hle_a; auto; omega.
rewrite Z.mul_add_distr_r; omega.
apply Z.le_trans with (m := a2 × m + m); try omega.
replace (a2 × m + m) with ((a2 + 1) × m).
assert (a2 + 1 ≤ a1) as Hle_a; try omega.
apply Z.mul_le_mono_nonneg_r with (p := m) in Hle_a; auto; omega.
rewrite Z.mul_add_distr_r; omega.
repeat (split; try solve
[(rewrite (Mem.load_store_other _ _ _ _ _ _ HA2); auto; right;
apply Hsep; simpl; auto; try omega) |
(apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA2); auto)]).
simpl; rewrite ZMap.gso; auto.
- auto.
}
{
subst; specialize (cvalid_id _ H4).
destruct (H _ cvalid_id) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
∃ ι, Vzero, m2, d2; repeat (apply conj).
- econstructor; eauto.
inv Hm.
rewrite <- H9 in H4; inv H4.
specialize (cvalid_usage _ H4).
rewrite <- H2 in H8, cvalid_usage; simpl in H8, cvalid_usage; rewrite Z.ltb_nlt in H8.
assert (u = q) by omega; subst; auto.
simpl; inv match_related; split; congruence.
- apply f_equal with (f:= Int.repr) in H3.
rewrite Int.repr_unsigned in H3; subst; constructor.
- split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
- auto.
}
Qed.
End container_alloc_ref.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store´) (lflatmem_store:= flatmem_store´)).
Proof.
accessor_prop_tac.
- eapply flatmem_store´_exists; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) mcontainer_passthrough dabshandler.
Proof.
sim_oplus_split_final (cdata LDATA).
- apply fload´_sim.
- apply fstore´_sim.
- apply flatmem_copy´_sim.
- apply vmxinfo_get_sim.
- apply setPG_sim.
- apply setCR3_sim.
- apply get_size_sim.
- apply is_mm_usable_sim.
- apply get_mm_s_sim.
- apply get_mm_l_sim.
- apply cli_sim.
- apply sti_sim.
- apply cons_buf_read_sim.
- apply serial_putc_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply trapin_sim.
- apply trapout´_sim.
- apply hostin_sim.
- apply hostout´_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End OneStep_Forward_Relation.
End WITHMEM.
End Refinement.