Library mcertikos.mm.ContainerIntroGen
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 DeviceStateDataType.
Require Import MContainerIntro.
Require Import DAbsHandler.
Require Import ProofIrrelevance.
Require Import ContainerIntroGenSpec.
Require Import CalTicketLock.
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 DeviceStateDataType.
Require Import MContainerIntro.
Require Import DAbsHandler.
Require Import ProofIrrelevance.
Require Import ContainerIntroGenSpec.
Require Import CalTicketLock.
Section Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mcontainerintro_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := dabshandler_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mcontainerintro_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := dabshandler_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
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_proc →
(∃ 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_proc →
(∃ 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;
buffer_re: buffer hadt = buffer 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;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
multi_oracle_re: multi_oracle hadt = multi_oracle ladt;
multi_log_re: multi_log hadt = multi_log ladt;
lock_re : lock hadt = lock 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;
buffer_re: buffer hadt = buffer 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;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
cid_re: cid hadt = cid ladt;
multi_oracle_re: multi_oracle hadt = multi_oracle ladt;
multi_log_re: multi_log hadt = multi_log ladt;
lock_re : lock hadt = lock 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.
Section OneStep_Forward_Relation.
Section container_node_init_ref.
Lemma container_node_init_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_node_init_spec) container_init_node_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H1.
destruct (H (Int.unsigned i) _x)
as [v01[v02[v03[v04[v05[HL01[HL02[HL03[HL04[HL05[HA01[HA02[HA03[HA04[HA05 Hm0]]]]]]]]]]]]]]].
simpl in ×.
remember HA01 as HA01old; clear HeqHA01old.
remember HA02 as HA02old; clear HeqHA02old.
remember HA03 as HA03old; clear HeqHA03old.
remember HA04 as HA04old; clear HeqHA04old.
remember HA05 as HA05old; clear HeqHA05old.
apply Mem.valid_access_store with (v := Vint i0) in HA01.
destruct HA01 as [m03 HA01].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01) in HA02.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01) in HA03.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01) in HA04.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01) in HA05.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA02.
destruct HA02 as [m04 HA02].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA03.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA04.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA05.
apply Mem.valid_access_store with (v := Vint i1) in HA03.
destruct HA03 as [m05 HA03].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03) in HA04.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03) in HA05.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA04.
destruct HA04 as [m06 HA04].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04) in HA05.
apply Mem.valid_access_store with (v := Vint Int.one) in HA05.
destruct HA05 as [m07 HA05].
inv Hι.
inv H11.
inv H13.
inv H10.
inv H12.
inv H10.
inv H13.
repeat (apply conj).
refine_split´; eauto.
- econstructor; eauto.
unfold kernel_mode.
simpl.
inv match_related; simpl.
rewrite <- ikern_re0.
rewrite <- ihost_re0.
auto.
- functional inversion H1; inv match_related.
split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
constructor; auto.
econstructor; eauto.
intros.
destruct (zeq i2 (Int.unsigned i)); subst; simpl.
{ subst.
∃ i0, Int.zero, i1, Int.zero, Int.one.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
apply (Mem.load_store_same _ _ _ _ _ _ HA01).
simpl; unfold CSIZE, USAGE, QUOTA.
right; left; omega.
simpl; unfold CSIZE, PARENT, QUOTA.
right; left; omega.
simpl; unfold CSIZE, NCHILDREN, QUOTA.
right; left; omega.
simpl; unfold CSIZE, USED, QUOTA.
right; left; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
apply (Mem.load_store_same _ _ _ _ _ _ HA02).
simpl; unfold CSIZE, PARENT, USAGE.
right; left; omega.
simpl; unfold CSIZE, NCHILDREN, USAGE.
right; left; omega.
simpl; unfold CSIZE, USED, USAGE.
right; left; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
apply (Mem.load_store_same _ _ _ _ _ _ HA03).
simpl; unfold CSIZE, PARENT, NCHILDREN.
right; left; omega.
simpl; unfold CSIZE, PARENT, USED.
right; left; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
apply (Mem.load_store_same _ _ _ _ _ _ HA04).
simpl; unfold CSIZE, USED, NCHILDREN.
right; left; omega.
- apply (Mem.load_store_same _ _ _ _ _ _ HA05).
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- unfold new_c.
rewrite ZMap.gss.
generalize (MATCH_CONTAINER_USED (Int.unsigned i0) 0 (Int.unsigned i1) nil);
intros.
assert (match_int (Int.unsigned i0) (Int.repr (Int.unsigned i0))) by (econstructor; eauto).
assert (match_int 0 (Int.repr 0)) by (econstructor; eauto; omega).
assert (match_int (Int.unsigned i1) (Int.repr (Int.unsigned i1))).
econstructor; unfold Int.max_unsigned; simpl; omega.
simpl in H15.
rewrite Int.repr_unsigned in H15, H16, H18, H15.
eapply H15; eauto. }
{ rewrite ZMap.gso; auto.
destruct (H i2 H14) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA01); auto.
simpl. unfold QUOTA; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold QUOTA, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold QUOTA, PARENT; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold QUOTA, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold QUOTA, USED; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA01); auto.
simpl. unfold USAGE, QUOTA ; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USAGE, PARENT; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USAGE, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USAGE, USED; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA01); auto.
simpl. unfold PARENT, QUOTA ; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold PARENT, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold PARENT; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold PARENT, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold PARENT, USED; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA01); auto.
simpl. unfold NCHILDREN, QUOTA ; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold NCHILDREN, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold NCHILDREN, PARENT; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold NCHILDREN, USED; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA01); auto.
simpl. unfold USED, QUOTA ; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USED, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USED, PARENT; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USED, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USED; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- auto. }
Qed.
End container_node_init_ref.
Section container_set_usage_ref.
Lemma container_set_usage_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_set_usage_spec)
container_set_usage_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H1.
destruct (H (Int.unsigned i) _x)
as [v01[v02[v03[v04[v05[HL01[HL02[HL03[HL04[HL05[HA01[HA02[HA03[HA04[HA05 Hm0]]]]]]]]]]]]]]].
simpl in ×.
remember HA01 as HA01old; clear HeqHA01old.
remember HA02 as HA02old; clear HeqHA02old.
remember HA03 as HA03old; clear HeqHA03old.
remember HA04 as HA04old; clear HeqHA04old.
remember HA05 as HA05old; clear HeqHA05old.
apply Mem.valid_access_store with (v := Vint i0) in HA02.
destruct HA02 as [m03 HA02].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA03.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA04.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA05.
inv Hι.
inv H11.
inv H13.
inv H10.
inv H12.
repeat (apply conj).
refine_split´; eauto.
- econstructor; eauto.
unfold kernel_mode.
simpl.
inv match_related; simpl.
rewrite <- ikern_re0.
rewrite <- ihost_re0.
auto.
- functional inversion H1; inv match_related.
split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
constructor; auto.
econstructor; eauto.
intros.
destruct (zeq i1 (Int.unsigned i)); subst; simpl.
{ subst.
∃ v01, i0, v03, v04, v05.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); eauto.
simpl; unfold CSIZE, USAGE, QUOTA.
right; left; omega.
- apply (Mem.load_store_same _ _ _ _ _ _ HA02).
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); eauto.
simpl; unfold CSIZE, USAGE, PARENT.
right; right; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); eauto.
simpl; unfold CSIZE, USAGE, NCHILDREN.
right; right; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); eauto.
simpl; unfold CSIZE, USAGE, USED.
right; right; omega.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); auto.
- rewrite ZMap.gss.
unfold new_c.
rewrite H5.
inv Hm0.
{ assert (cused {| cquota := q;
cusage := u;
cparent := p;
cchildren := c1;
cused := false |} = true).
{ rewrite H16; fold c; rewrite H5; auto. }
simpl in H14; inv H15. }
simpl.
generalize (MATCH_CONTAINER_USED (cquota c) (Int.unsigned i0) (cparent c) (cchildren c)); intros.
unfold c.
rewrite <- H15; simpl.
unfold c in H16. rewrite <- H15 in H16. simpl in H16.
assert (match_int (Int.unsigned i0) (Int.repr (Int.unsigned i0))).
{ inv H21.
clear H4.
rewrite <- H15 in _x0.
revert _x0.
simpl.
intros.
constructor.
omega. }
rewrite Int.repr_unsigned in H16, H17.
eapply H16; eauto. }
{ rewrite ZMap.gso; auto.
destruct (H i1 H14) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); auto.
simpl. unfold QUOTA, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); auto.
simpl. unfold USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); auto.
simpl. unfold PARENT, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); auto.
simpl. unfold NCHILDREN, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); auto.
simpl. unfold USED, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); eauto.
- auto. }
Qed.
End container_set_usage_ref.
Section container_set_nchildren_ref.
Lemma container_set_nchildren_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_set_nchildren_spec)
container_set_nchildren_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H1.
destruct (H (Int.unsigned i) _x)
as [v01[v02[v03[v04[v05[HL01[HL02[HL03[HL04[HL05[HA01[HA02[HA03[HA04[HA05 Hm0]]]]]]]]]]]]]]].
simpl in ×.
remember HA01 as HA01old; clear HeqHA01old.
remember HA02 as HA02old; clear HeqHA02old.
remember HA03 as HA03old; clear HeqHA03old.
remember HA04 as HA04old; clear HeqHA04old.
remember HA05 as HA05old; clear HeqHA05old.
apply Mem.valid_access_store with (v := Vint (Int.add v04 Int.one)) in HA04.
destruct HA04 as [m03 HA04].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04) in HA05.
inv Hι.
inv H11.
inv H13.
inv H10.
inv H12.
repeat (apply conj).
refine_split´; eauto.
- econstructor; eauto.
unfold kernel_mode.
simpl.
inv match_related; simpl.
rewrite <- ikern_re0.
rewrite <- ihost_re0.
auto.
- functional inversion H1; inv match_related.
split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
constructor; auto.
econstructor; eauto.
intros.
destruct (zeq i1 (Int.unsigned i)); subst; simpl.
{ subst.
∃ v01, v02, v03, (Int.add v04 Int.one), v05.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); eauto.
simpl; unfold CSIZE, NCHILDREN, QUOTA.
right; left; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); eauto.
simpl; unfold CSIZE, NCHILDREN, USAGE.
right; left; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); eauto.
simpl; unfold CSIZE, PARENT, NCHILDREN.
right; left; omega.
- apply (Mem.load_store_same _ _ _ _ _ _ HA04).
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); eauto.
simpl; unfold CSIZE, NCHILDREN, USED.
right; right; omega.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); auto.
- rewrite ZMap.gss.
unfold new_c.
rewrite H5.
inv Hm0.
{ assert (cused {| cquota := q;
cusage := u;
cparent := p;
cchildren := c1;
cused := false |} = true).
{ rewrite H16; fold c; rewrite H5; auto. }
simpl in H15; inv H15. }
simpl.
generalize (MATCH_CONTAINER_USED (cquota c) (cusage c) (cparent c) (Int.unsigned i0::cchildren c)); intros.
unfold c.
rewrite <- H15; simpl.
unfold c in H16. rewrite <- H15 in H16. simpl in H16.
assert (match_int (Z.pos (Pos.of_succ_nat (length c1)))
(Int.repr (Z.pos (Pos.of_succ_nat (length c1))))).
{ constructor.
rewrite Zpos_P_of_succ_nat.
unfold c in _x0.
clear H4.
rewrite <- H15 in _x0; simpl in _x0.
unfold Int.max_unsigned; simpl in ×.
omega. }
assert ((Int.add (Int.repr (Z.of_nat (length c1))) Int.one) = Int.repr (Z.pos (Pos.of_succ_nat (length c1)))).
{ simpl.
unfold Int.add.
unfold Int.one.
unfold c in _x0.
clear H4.
rewrite <- H15 in _x0; simpl in _x0.
rewrite Int.unsigned_repr; eauto; try (unfold Int.max_unsigned; simpl; omega).
rewrite Int.unsigned_repr; eauto; try (unfold Int.max_unsigned; simpl; omega).
rewrite Zpos_P_of_succ_nat.
rewrite Z.add_1_r; auto. }
rewrite H18.
eapply H16; eauto. }
{ rewrite ZMap.gso; auto.
destruct (H i1 H14) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); auto.
simpl. unfold QUOTA, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); auto.
simpl. unfold USAGE, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); auto.
simpl. unfold PARENT, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); auto.
simpl. unfold NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); auto.
simpl. unfold USED, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); eauto.
- auto. }
Qed.
End container_set_nchildren_ref.
Section container_get_nchildren_intro_ref.
Lemma container_get_nchildren_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_get_nchildren_intro_spec)
container_get_nchildren_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H9; inv H11.
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H4; inv H4.
rewrite <- H7 in H1.
simpl in H1; subst.
rewrite H1 in HL4.
rewrite Int.repr_unsigned in HL4; auto.
simpl; inv match_related; split; congruence.
- constructor.
- assumption.
- auto.
Qed.
End container_get_nchildren_intro_ref.
Section container_get_quota_intro_ref.
Lemma container_get_quota_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_get_quota_intro_spec)
container_get_quota_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H9; inv H11.
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H4; inv H4.
rewrite <- H7 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_intro_ref.
Section container_get_usage_intro_ref.
Lemma container_get_usage_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_get_usage_intro_spec)
container_get_usage_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H9; inv H11.
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H4; inv H4.
rewrite <- H7 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_intro_ref.
Section container_get_parent_intro_ref.
Lemma container_get_parent_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_get_parent_intro_spec)
container_get_parent_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H9; inv H11.
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H4; inv H4.
rewrite <- H7 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_intro_ref.
Section container_can_consume_intro_ref.
Lemma container_can_consume_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_can_consume_intro_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.
× destruct (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H11 in H6; inv H6.
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 <- H10; auto.
rewrite <- H10; auto.
simpl; inv match_related; split; congruence.
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 (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H11 in H6; inv H6.
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 <- H10; auto.
rewrite <- H10; auto.
simpl; inv match_related; split; congruence.
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_intro_ref.
Section container_alloc_intro_ref.
Lemma container_alloc_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_alloc_intro_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.
functional inversion H1; subst c cur.
{
destruct (H (Int.unsigned i) _x) 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 <- H13 in H7; inv H7.
rewrite <- H12 in H11; rewrite Z.ltb_lt in H11; simpl in H11.
rewrite 2 Int.unsigned_repr; auto.
inv H18; auto.
inv H19; 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 <- H12 in H7; inv H7.
replace (Int.add (Int.repr u) Int.one) with (Int.repr (u+1)).
constructor; auto.
constructor; split.
inv H18; omega.
inv H18; inv H17.
rewrite Z.ltb_lt in H11; rewrite <- H2 in H11; simpl in H11; omega.
inv H18.
rewrite <- (Int.unsigned_repr _ H12) 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.
destruct (H (Int.unsigned i) _x) 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 <- H12 in H7; inv H7.
clear H6.
rewrite <- H2 in H11, _x1; simpl in H11, _x1; rewrite Z.ltb_nlt in H11.
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_intro_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) mcontainerintro_passthrough dabshandler.
Proof.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply page_copy´_sim.
- apply page_copy_back´_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 get_CPU_ID_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply (release_lock_sim (valid_arg_imply:= Shared2ID0_imply)).
-
eapply acquire_lock_sim0; eauto.
intros. inv H; trivial; try inv H0.
- apply ticket_lock_init0_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_sim.
- apply trapin_sim.
- apply trapout´_sim.
- apply hostin_sim.
- apply hostout´_sim.
- apply proc_create_postinit_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.
∀ 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_node_init_ref.
Lemma container_node_init_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_node_init_spec) container_init_node_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H1.
destruct (H (Int.unsigned i) _x)
as [v01[v02[v03[v04[v05[HL01[HL02[HL03[HL04[HL05[HA01[HA02[HA03[HA04[HA05 Hm0]]]]]]]]]]]]]]].
simpl in ×.
remember HA01 as HA01old; clear HeqHA01old.
remember HA02 as HA02old; clear HeqHA02old.
remember HA03 as HA03old; clear HeqHA03old.
remember HA04 as HA04old; clear HeqHA04old.
remember HA05 as HA05old; clear HeqHA05old.
apply Mem.valid_access_store with (v := Vint i0) in HA01.
destruct HA01 as [m03 HA01].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01) in HA02.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01) in HA03.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01) in HA04.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01) in HA05.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA02.
destruct HA02 as [m04 HA02].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA03.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA04.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA05.
apply Mem.valid_access_store with (v := Vint i1) in HA03.
destruct HA03 as [m05 HA03].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03) in HA04.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03) in HA05.
apply Mem.valid_access_store with (v := Vint Int.zero) in HA04.
destruct HA04 as [m06 HA04].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04) in HA05.
apply Mem.valid_access_store with (v := Vint Int.one) in HA05.
destruct HA05 as [m07 HA05].
inv Hι.
inv H11.
inv H13.
inv H10.
inv H12.
inv H10.
inv H13.
repeat (apply conj).
refine_split´; eauto.
- econstructor; eauto.
unfold kernel_mode.
simpl.
inv match_related; simpl.
rewrite <- ikern_re0.
rewrite <- ihost_re0.
auto.
- functional inversion H1; inv match_related.
split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
constructor; auto.
econstructor; eauto.
intros.
destruct (zeq i2 (Int.unsigned i)); subst; simpl.
{ subst.
∃ i0, Int.zero, i1, Int.zero, Int.one.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
apply (Mem.load_store_same _ _ _ _ _ _ HA01).
simpl; unfold CSIZE, USAGE, QUOTA.
right; left; omega.
simpl; unfold CSIZE, PARENT, QUOTA.
right; left; omega.
simpl; unfold CSIZE, NCHILDREN, QUOTA.
right; left; omega.
simpl; unfold CSIZE, USED, QUOTA.
right; left; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
apply (Mem.load_store_same _ _ _ _ _ _ HA02).
simpl; unfold CSIZE, PARENT, USAGE.
right; left; omega.
simpl; unfold CSIZE, NCHILDREN, USAGE.
right; left; omega.
simpl; unfold CSIZE, USED, USAGE.
right; left; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
apply (Mem.load_store_same _ _ _ _ _ _ HA03).
simpl; unfold CSIZE, PARENT, NCHILDREN.
right; left; omega.
simpl; unfold CSIZE, PARENT, USED.
right; left; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
apply (Mem.load_store_same _ _ _ _ _ _ HA04).
simpl; unfold CSIZE, USED, NCHILDREN.
right; left; omega.
- apply (Mem.load_store_same _ _ _ _ _ _ HA05).
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- unfold new_c.
rewrite ZMap.gss.
generalize (MATCH_CONTAINER_USED (Int.unsigned i0) 0 (Int.unsigned i1) nil);
intros.
assert (match_int (Int.unsigned i0) (Int.repr (Int.unsigned i0))) by (econstructor; eauto).
assert (match_int 0 (Int.repr 0)) by (econstructor; eauto; omega).
assert (match_int (Int.unsigned i1) (Int.repr (Int.unsigned i1))).
econstructor; unfold Int.max_unsigned; simpl; omega.
simpl in H15.
rewrite Int.repr_unsigned in H15, H16, H18, H15.
eapply H15; eauto. }
{ rewrite ZMap.gso; auto.
destruct (H i2 H14) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA01); auto.
simpl. unfold QUOTA; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold QUOTA, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold QUOTA, PARENT; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold QUOTA, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold QUOTA, USED; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA01); auto.
simpl. unfold USAGE, QUOTA ; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USAGE, PARENT; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USAGE, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USAGE, USED; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA01); auto.
simpl. unfold PARENT, QUOTA ; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold PARENT, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold PARENT; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold PARENT, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold PARENT, USED; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA01); auto.
simpl. unfold NCHILDREN, QUOTA ; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold NCHILDREN, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold NCHILDREN, PARENT; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold NCHILDREN, USED; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA05).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA04).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA03).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA02).
rewrite (Mem.load_store_other _ _ _ _ _ _ HA01); auto.
simpl. unfold USED, QUOTA ; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USED, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USED, PARENT; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USED, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
simpl. unfold USED; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i2); [right; omega | left; omega].
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA05);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA03);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02);
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA01); auto.
- auto. }
Qed.
End container_node_init_ref.
Section container_set_usage_ref.
Lemma container_set_usage_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_set_usage_spec)
container_set_usage_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H1.
destruct (H (Int.unsigned i) _x)
as [v01[v02[v03[v04[v05[HL01[HL02[HL03[HL04[HL05[HA01[HA02[HA03[HA04[HA05 Hm0]]]]]]]]]]]]]]].
simpl in ×.
remember HA01 as HA01old; clear HeqHA01old.
remember HA02 as HA02old; clear HeqHA02old.
remember HA03 as HA03old; clear HeqHA03old.
remember HA04 as HA04old; clear HeqHA04old.
remember HA05 as HA05old; clear HeqHA05old.
apply Mem.valid_access_store with (v := Vint i0) in HA02.
destruct HA02 as [m03 HA02].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA03.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA04.
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02) in HA05.
inv Hι.
inv H11.
inv H13.
inv H10.
inv H12.
repeat (apply conj).
refine_split´; eauto.
- econstructor; eauto.
unfold kernel_mode.
simpl.
inv match_related; simpl.
rewrite <- ikern_re0.
rewrite <- ihost_re0.
auto.
- functional inversion H1; inv match_related.
split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
constructor; auto.
econstructor; eauto.
intros.
destruct (zeq i1 (Int.unsigned i)); subst; simpl.
{ subst.
∃ v01, i0, v03, v04, v05.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); eauto.
simpl; unfold CSIZE, USAGE, QUOTA.
right; left; omega.
- apply (Mem.load_store_same _ _ _ _ _ _ HA02).
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); eauto.
simpl; unfold CSIZE, USAGE, PARENT.
right; right; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); eauto.
simpl; unfold CSIZE, USAGE, NCHILDREN.
right; right; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); eauto.
simpl; unfold CSIZE, USAGE, USED.
right; right; omega.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); auto.
- rewrite ZMap.gss.
unfold new_c.
rewrite H5.
inv Hm0.
{ assert (cused {| cquota := q;
cusage := u;
cparent := p;
cchildren := c1;
cused := false |} = true).
{ rewrite H16; fold c; rewrite H5; auto. }
simpl in H14; inv H15. }
simpl.
generalize (MATCH_CONTAINER_USED (cquota c) (Int.unsigned i0) (cparent c) (cchildren c)); intros.
unfold c.
rewrite <- H15; simpl.
unfold c in H16. rewrite <- H15 in H16. simpl in H16.
assert (match_int (Int.unsigned i0) (Int.repr (Int.unsigned i0))).
{ inv H21.
clear H4.
rewrite <- H15 in _x0.
revert _x0.
simpl.
intros.
constructor.
omega. }
rewrite Int.repr_unsigned in H16, H17.
eapply H16; eauto. }
{ rewrite ZMap.gso; auto.
destruct (H i1 H14) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); auto.
simpl. unfold QUOTA, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); auto.
simpl. unfold USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); auto.
simpl. unfold PARENT, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); auto.
simpl. unfold NCHILDREN, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA02); auto.
simpl. unfold USED, USAGE; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA02); eauto.
- auto. }
Qed.
End container_set_usage_ref.
Section container_set_nchildren_ref.
Lemma container_set_nchildren_spec_ref:
compatsim (crel HDATA LDATA) (gensem container_set_nchildren_spec)
container_set_nchildren_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H1.
destruct (H (Int.unsigned i) _x)
as [v01[v02[v03[v04[v05[HL01[HL02[HL03[HL04[HL05[HA01[HA02[HA03[HA04[HA05 Hm0]]]]]]]]]]]]]]].
simpl in ×.
remember HA01 as HA01old; clear HeqHA01old.
remember HA02 as HA02old; clear HeqHA02old.
remember HA03 as HA03old; clear HeqHA03old.
remember HA04 as HA04old; clear HeqHA04old.
remember HA05 as HA05old; clear HeqHA05old.
apply Mem.valid_access_store with (v := Vint (Int.add v04 Int.one)) in HA04.
destruct HA04 as [m03 HA04].
apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04) in HA05.
inv Hι.
inv H11.
inv H13.
inv H10.
inv H12.
repeat (apply conj).
refine_split´; eauto.
- econstructor; eauto.
unfold kernel_mode.
simpl.
inv match_related; simpl.
rewrite <- ikern_re0.
rewrite <- ihost_re0.
auto.
- functional inversion H1; inv match_related.
split; eauto; pattern2_refinement_simpl´ (@relate_AbData).
constructor; auto.
econstructor; eauto.
intros.
destruct (zeq i1 (Int.unsigned i)); subst; simpl.
{ subst.
∃ v01, v02, v03, (Int.add v04 Int.one), v05.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); eauto.
simpl; unfold CSIZE, NCHILDREN, QUOTA.
right; left; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); eauto.
simpl; unfold CSIZE, NCHILDREN, USAGE.
right; left; omega.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); eauto.
simpl; unfold CSIZE, PARENT, NCHILDREN.
right; left; omega.
- apply (Mem.load_store_same _ _ _ _ _ _ HA04).
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); eauto.
simpl; unfold CSIZE, NCHILDREN, USED.
right; right; omega.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); auto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); auto.
- rewrite ZMap.gss.
unfold new_c.
rewrite H5.
inv Hm0.
{ assert (cused {| cquota := q;
cusage := u;
cparent := p;
cchildren := c1;
cused := false |} = true).
{ rewrite H16; fold c; rewrite H5; auto. }
simpl in H15; inv H15. }
simpl.
generalize (MATCH_CONTAINER_USED (cquota c) (cusage c) (cparent c) (Int.unsigned i0::cchildren c)); intros.
unfold c.
rewrite <- H15; simpl.
unfold c in H16. rewrite <- H15 in H16. simpl in H16.
assert (match_int (Z.pos (Pos.of_succ_nat (length c1)))
(Int.repr (Z.pos (Pos.of_succ_nat (length c1))))).
{ constructor.
rewrite Zpos_P_of_succ_nat.
unfold c in _x0.
clear H4.
rewrite <- H15 in _x0; simpl in _x0.
unfold Int.max_unsigned; simpl in ×.
omega. }
assert ((Int.add (Int.repr (Z.of_nat (length c1))) Int.one) = Int.repr (Z.pos (Pos.of_succ_nat (length c1)))).
{ simpl.
unfold Int.add.
unfold Int.one.
unfold c in _x0.
clear H4.
rewrite <- H15 in _x0; simpl in _x0.
rewrite Int.unsigned_repr; eauto; try (unfold Int.max_unsigned; simpl; omega).
rewrite Int.unsigned_repr; eauto; try (unfold Int.max_unsigned; simpl; omega).
rewrite Zpos_P_of_succ_nat.
rewrite Z.add_1_r; auto. }
rewrite H18.
eapply H16; eauto. }
{ rewrite ZMap.gso; auto.
destruct (H i1 H14) as
[v1´[v2´[v3´[v4´[v5´[HL1´[HL2´[HL3´[HL4´[HL5´[HA1´[HA2´[HA3´[HA4´[HA5´ Hm´]]]]]]]]]]]]]]].
∃ v1´, v2´, v3´, v4´, v5´.
refine_split.
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); auto.
simpl. unfold QUOTA, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); auto.
simpl. unfold USAGE, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); auto.
simpl. unfold PARENT, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); auto.
simpl. unfold NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- rewrite (Mem.load_store_other _ _ _ _ _ _ HA04); auto.
simpl. unfold USED, NCHILDREN; unfold CSIZE.
right; destruct (zle (Int.unsigned i) i1); [right; omega | left; omega].
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); eauto.
- apply (Mem.store_valid_access_1 _ _ _ _ _ _ HA04); eauto.
- auto. }
Qed.
End container_set_nchildren_ref.
Section container_get_nchildren_intro_ref.
Lemma container_get_nchildren_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_get_nchildren_intro_spec)
container_get_nchildren_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H9; inv H11.
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H4; inv H4.
rewrite <- H7 in H1.
simpl in H1; subst.
rewrite H1 in HL4.
rewrite Int.repr_unsigned in HL4; auto.
simpl; inv match_related; split; congruence.
- constructor.
- assumption.
- auto.
Qed.
End container_get_nchildren_intro_ref.
Section container_get_quota_intro_ref.
Lemma container_get_quota_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_get_quota_intro_spec)
container_get_quota_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H9; inv H11.
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H4; inv H4.
rewrite <- H7 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_intro_ref.
Section container_get_usage_intro_ref.
Lemma container_get_usage_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_get_usage_intro_spec)
container_get_usage_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H9; inv H11.
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H4; inv H4.
rewrite <- H7 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_intro_ref.
Section container_get_parent_intro_ref.
Lemma container_get_parent_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_get_parent_intro_spec)
container_get_parent_spec_low.
Proof.
compatsim_simpl (@match_AbData).
functional inversion H2; subst c.
inv Hι.
inv H9; inv H11.
∃ ι, (Vint z), m2, d2; repeat (apply conj).
- econstructor; eauto.
destruct (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H8 in H4; inv H4.
rewrite <- H7 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_intro_ref.
Section container_can_consume_intro_ref.
Lemma container_can_consume_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_can_consume_intro_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.
× destruct (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H11 in H6; inv H6.
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 <- H10; auto.
rewrite <- H10; auto.
simpl; inv match_related; split; congruence.
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 (H (Int.unsigned i) _x) as
[v1[v2[v3[v4[v5[HL1[HL2[HL3[HL4[HL5[HA1[HA2[HA3[HA4[HA5 Hm]]]]]]]]]]]]]]].
inv Hm.
rewrite <- H11 in H6; inv H6.
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 <- H10; auto.
rewrite <- H10; auto.
simpl; inv match_related; split; congruence.
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_intro_ref.
Section container_alloc_intro_ref.
Lemma container_alloc_spec_intro_ref:
compatsim (crel HDATA LDATA) (gensem container_alloc_intro_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.
functional inversion H1; subst c cur.
{
destruct (H (Int.unsigned i) _x) 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 <- H13 in H7; inv H7.
rewrite <- H12 in H11; rewrite Z.ltb_lt in H11; simpl in H11.
rewrite 2 Int.unsigned_repr; auto.
inv H18; auto.
inv H19; 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 <- H12 in H7; inv H7.
replace (Int.add (Int.repr u) Int.one) with (Int.repr (u+1)).
constructor; auto.
constructor; split.
inv H18; omega.
inv H18; inv H17.
rewrite Z.ltb_lt in H11; rewrite <- H2 in H11; simpl in H11; omega.
inv H18.
rewrite <- (Int.unsigned_repr _ H12) 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.
destruct (H (Int.unsigned i) _x) 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 <- H12 in H7; inv H7.
clear H6.
rewrite <- H2 in H11, _x1; simpl in H11, _x1; rewrite Z.ltb_nlt in H11.
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_intro_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) mcontainerintro_passthrough dabshandler.
Proof.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply page_copy´_sim.
- apply page_copy_back´_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 get_CPU_ID_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply (release_lock_sim (valid_arg_imply:= Shared2ID0_imply)).
-
eapply acquire_lock_sim0; eauto.
intros. inv H; trivial; try inv H0.
- apply ticket_lock_init0_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_sim.
- apply trapin_sim.
- apply trapout´_sim.
- apply hostin_sim.
- apply hostout´_sim.
- apply proc_create_postinit_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.