Library mcertikos.objects.ObjLMM1
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealPTB.
Require Import DeviceStateDataType.
Require Import ObjInterruptDriver.
Section OBJ_LMM.
Context `{real_params: RealParams}.
Function pfree_spec (i: Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, pg adt, ipt adt) with
| (true, true, true, true) ⇒
if zle_lt 0 i maxpage then
match (ZMap.get i (LAT adt), ZMap.get i (pperm adt)) with
| (LATValid true ATNorm nil, PGAlloc) ⇒
Some adt {LAT: ZMap.set i (LATValid false ATNorm nil) (LAT adt)}
{pperm: ZMap.set i PGUndef (pperm adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function setPT_spec (n: Z) (adt: RData) : option RData :=
match (ikern adt, ihost adt, ipt adt) with
| (true, true, false) ⇒
if zle_lt 0 n num_proc then
Some adt {PT: n}
else None
| _ ⇒ None
end.
primitve: in the kernel mode, after switching to kernel's page table, set ipt to true
Function ptin_spec (adt: RData): option RData :=
match (ipt adt, ikern adt, ihost adt) with
| (false, true, true) ⇒
if zeq (PT adt) 0 then
Some adt {ipt: true}
else None
| _ ⇒ None
end.
Remark Freeable_PTE_dec´ (pte: PTE):
{∀ i, 0 ≤ i < PTX (Int.max_unsigned) + 1 → ZMap.get i pte = PTEUnPresent}
+ {~(∀ i, 0 ≤ i < PTX (Int.max_unsigned) + 1 → ZMap.get i pte = PTEUnPresent)}.
Proof.
eapply general_range_dec.
intros. destruct (ZMap.get i pte).
- right; red; intros; congruence.
- left; trivial.
- right; red; intros; congruence.
Qed.
Remark Freeable_PTE_dec (pte: PTE):
{∀ i, 0 ≤ i ≤ PTX (Int.max_unsigned) → ZMap.get i pte = PTEUnPresent}
+ {¬ (∀ i, 0 ≤ i ≤ PTX (Int.max_unsigned) → ZMap.get i pte = PTEUnPresent)}.
Proof.
pose proof (Freeable_PTE_dec´ pte) as HR.
inv HR.
- left. intros. apply H; eauto. omega.
- right. red; intros. elim H; intros.
apply H0; eauto. omega.
Defined.
Function ptFreePDE0_spec (n vadr: Z) (adt: RData): option RData :=
let pdi := PDX vadr in
match (ikern adt, ihost adt, pg adt, ipt adt, pt_Arg´ n vadr) with
| (true, true, true, true, true) ⇒
match ZMap.get pdi (ZMap.get n (ptpool adt)) with
| PDEValid pi pte ⇒
if Freeable_PTE_dec pte then
let pt´:= ZMap.set pdi PDEUnPresent (ZMap.get n (ptpool adt)) in
Some adt {LAT: ZMap.set pi (LATValid false ATNorm nil) (LAT adt)}
{pperm: ZMap.set pi PGUndef (pperm adt)}
{ptpool: ZMap.set n pt´ (ptpool adt)}
else None
| _ ⇒ None
end
| _ ⇒ None
end.
match (ipt adt, ikern adt, ihost adt) with
| (false, true, true) ⇒
if zeq (PT adt) 0 then
Some adt {ipt: true}
else None
| _ ⇒ None
end.
Remark Freeable_PTE_dec´ (pte: PTE):
{∀ i, 0 ≤ i < PTX (Int.max_unsigned) + 1 → ZMap.get i pte = PTEUnPresent}
+ {~(∀ i, 0 ≤ i < PTX (Int.max_unsigned) + 1 → ZMap.get i pte = PTEUnPresent)}.
Proof.
eapply general_range_dec.
intros. destruct (ZMap.get i pte).
- right; red; intros; congruence.
- left; trivial.
- right; red; intros; congruence.
Qed.
Remark Freeable_PTE_dec (pte: PTE):
{∀ i, 0 ≤ i ≤ PTX (Int.max_unsigned) → ZMap.get i pte = PTEUnPresent}
+ {¬ (∀ i, 0 ≤ i ≤ PTX (Int.max_unsigned) → ZMap.get i pte = PTEUnPresent)}.
Proof.
pose proof (Freeable_PTE_dec´ pte) as HR.
inv HR.
- left. intros. apply H; eauto. omega.
- right. red; intros. elim H; intros.
apply H0; eauto. omega.
Defined.
Function ptFreePDE0_spec (n vadr: Z) (adt: RData): option RData :=
let pdi := PDX vadr in
match (ikern adt, ihost adt, pg adt, ipt adt, pt_Arg´ n vadr) with
| (true, true, true, true, true) ⇒
match ZMap.get pdi (ZMap.get n (ptpool adt)) with
| PDEValid pi pte ⇒
if Freeable_PTE_dec pte then
let pt´:= ZMap.set pdi PDEUnPresent (ZMap.get n (ptpool adt)) in
Some adt {LAT: ZMap.set pi (LATValid false ATNorm nil) (LAT adt)}
{pperm: ZMap.set pi PGUndef (pperm adt)}
{ptpool: ZMap.set n pt´ (ptpool adt)}
else None
| _ ⇒ None
end
| _ ⇒ None
end.
primitve: set the n-th page table with virtual address vadr to unpresent
Function ptRmv0_spec (n vadr: Z) (adt: RData): option (RData × Z) :=
match (ikern adt, ihost adt, ipt adt, pg adt, pt_Arg´ n vadr) with
| (true, true, true, true, true) ⇒
let pt:= ZMap.get n (ptpool adt) in
let pdi := PDX vadr in
match ZMap.get pdi pt with
| PDEValid pi pdt ⇒
if zlt_lt 0 pi maxpage then
let pti := PTX vadr in
match ZMap.get pti pdt with
| PTEValid padr _ ⇒
match ZMap.get padr (LAT adt) with
| LATValid true ATNorm l ⇒
let pdt´:= ZMap.set pti PTEUnPresent pdt in
let pt´ := ZMap.set pdi (PDEValid pi pdt´) pt in
if zle (Z.of_nat (length l)) Int.max_unsigned then
Some (adt {LAT: ZMap.set padr (LATValid true ATNorm (Lremove (LATO n pdi pti) l)) (LAT adt)}
{ptpool: ZMap.set n pt´ (ptpool adt)} , padr)
else None
| _ ⇒ None
end
| PTEUnPresent ⇒ Some (adt, 0)
| _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end.
Function pt_init_spec (mbi_adr:Z) (adt: RData): option RData :=
match (init adt, pg adt, in_intr adt, ikern adt, ihost adt, ipt adt) with
| (false, false, false, true, true, true) ⇒
let n := adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
if zeq n (Zlength (adt.(ioapic).(s).(IoApicIrqs))) then
if zeq n (Zlength (adt.(ioapic).(s).(IoApicEnables))) then
Some adt {ioapic/s: ioapic_init_aux adt.(ioapic).(s) (Z.to_nat (n - 1))} {lapic: (mkLApicData
(mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic adt))) true
(32 + 7) true true true 0 50 false 0))
{l1: l1 (lapic adt)}
{l2: l2 (lapic adt)}
{l3: l3 (lapic adt)}
}
{ioapic / s / CurrentIrq: None} {vmxinfo: real_vmxinfo} {pg: true} {LAT: real_LAT (LAT adt)} {nps: real_nps}
{AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool adt)}
{idpde: real_idpde (idpde adt)}
else
None
else
None
| _ ⇒ None
end.
match (ikern adt, ihost adt, ipt adt, pg adt, pt_Arg´ n vadr) with
| (true, true, true, true, true) ⇒
let pt:= ZMap.get n (ptpool adt) in
let pdi := PDX vadr in
match ZMap.get pdi pt with
| PDEValid pi pdt ⇒
if zlt_lt 0 pi maxpage then
let pti := PTX vadr in
match ZMap.get pti pdt with
| PTEValid padr _ ⇒
match ZMap.get padr (LAT adt) with
| LATValid true ATNorm l ⇒
let pdt´:= ZMap.set pti PTEUnPresent pdt in
let pt´ := ZMap.set pdi (PDEValid pi pdt´) pt in
if zle (Z.of_nat (length l)) Int.max_unsigned then
Some (adt {LAT: ZMap.set padr (LATValid true ATNorm (Lremove (LATO n pdi pti) l)) (LAT adt)}
{ptpool: ZMap.set n pt´ (ptpool adt)} , padr)
else None
| _ ⇒ None
end
| PTEUnPresent ⇒ Some (adt, 0)
| _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end.
Function pt_init_spec (mbi_adr:Z) (adt: RData): option RData :=
match (init adt, pg adt, in_intr adt, ikern adt, ihost adt, ipt adt) with
| (false, false, false, true, true, true) ⇒
let n := adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
if zeq n (Zlength (adt.(ioapic).(s).(IoApicIrqs))) then
if zeq n (Zlength (adt.(ioapic).(s).(IoApicEnables))) then
Some adt {ioapic/s: ioapic_init_aux adt.(ioapic).(s) (Z.to_nat (n - 1))} {lapic: (mkLApicData
(mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic adt))) true
(32 + 7) true true true 0 50 false 0))
{l1: l1 (lapic adt)}
{l2: l2 (lapic adt)}
{l3: l3 (lapic adt)}
}
{ioapic / s / CurrentIrq: None} {vmxinfo: real_vmxinfo} {pg: true} {LAT: real_LAT (LAT adt)} {nps: real_nps}
{AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool adt)}
{idpde: real_idpde (idpde adt)}
else
None
else
None
| _ ⇒ None
end.
primitve: returns whether the i-th page table has been used or not
Function is_pt_used_spec (i: Z) (adt: RData): option Z :=
match (ikern adt, ihost adt, ipt adt) with
| (true, true, true) ⇒
if zle_lt 0 i num_proc then
match ZMap.get i (pb adt) with
| PTTrue ⇒ Some 1
| PTFalse ⇒ Some 0
| _ ⇒ None
end
else None
| _ ⇒ None
end.
match (ikern adt, ihost adt, ipt adt) with
| (true, true, true) ⇒
if zle_lt 0 i num_proc then
match ZMap.get i (pb adt) with
| PTTrue ⇒ Some 1
| PTFalse ⇒ Some 0
| _ ⇒ None
end
else None
| _ ⇒ None
end.
primitve: set the used bit of the i-th page table to p
Function set_pt_bit_spec (i p: Z) (adt: RData): option (RData) :=
match (ikern adt, ihost adt, ipt adt) with
| (true, true, true) ⇒
if zle_lt 0 i num_proc then
match ZtoPTBit p with
| Some p´ ⇒ Some adt {pb: ZMap.set i p´ (pb adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function pt_new_spec (id q: Z) (adt: RData): option (RData × Z) :=
match (pg adt, ikern adt, ihost adt, ipt adt, cused (ZMap.get id (AC adt)),
zle_le 0 q (cquota (ZMap.get id (AC adt)) - cusage (ZMap.get id (AC adt)))) with
| (true, true, true, true, true, left _) ⇒
if PTB_defined_dec (pb adt) 0 num_proc then
match first_free_PT (pb adt) num_proc with
| inleft (exist i _) ⇒
Some (adt {AC: ZMap.set i (mkContainer q 0 id nil true)
(ZMap.set id (mkContainer (cquota (ZMap.get id (AC adt)))
(cusage (ZMap.get id (AC adt)) + q)
(cparent (ZMap.get id (AC adt)))
(i :: cchildren (ZMap.get id (AC adt)))
(cused (ZMap.get id (AC adt)))) (AC adt))}
{pb: ZMap.set i PTTrue (pb adt)}, i)
| _ ⇒ Some (adt, num_proc)
end
else None
| _ ⇒ None
end.
match (ikern adt, ihost adt, ipt adt) with
| (true, true, true) ⇒
if zle_lt 0 i num_proc then
match ZtoPTBit p with
| Some p´ ⇒ Some adt {pb: ZMap.set i p´ (pb adt)}
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function pt_new_spec (id q: Z) (adt: RData): option (RData × Z) :=
match (pg adt, ikern adt, ihost adt, ipt adt, cused (ZMap.get id (AC adt)),
zle_le 0 q (cquota (ZMap.get id (AC adt)) - cusage (ZMap.get id (AC adt)))) with
| (true, true, true, true, true, left _) ⇒
if PTB_defined_dec (pb adt) 0 num_proc then
match first_free_PT (pb adt) num_proc with
| inleft (exist i _) ⇒
Some (adt {AC: ZMap.set i (mkContainer q 0 id nil true)
(ZMap.set id (mkContainer (cquota (ZMap.get id (AC adt)))
(cusage (ZMap.get id (AC adt)) + q)
(cparent (ZMap.get id (AC adt)))
(i :: cchildren (ZMap.get id (AC adt)))
(cused (ZMap.get id (AC adt)))) (AC adt))}
{pb: ZMap.set i PTTrue (pb adt)}, i)
| _ ⇒ Some (adt, num_proc)
end
else None
| _ ⇒ None
end.
primitive: initialize the allocation table, all the page tables,
set the 0th page table as the kernel's page table and enable paging
Function pmap_init_spec (mbi_adr:Z) (adt: RData): option RData :=
match (init adt, pg adt, in_intr adt, ikern adt, ihost adt, ipt adt) with
| (false, false, false, true, true, true) ⇒
let n := adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
if zeq n (Zlength (adt.(ioapic).(s).(IoApicIrqs))) then
if zeq n (Zlength (adt.(ioapic).(s).(IoApicEnables))) then
Some adt {ioapic/s: ioapic_init_aux adt.(ioapic).(s) (Z.to_nat (n - 1))} {lapic: (mkLApicData
(mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic adt))) true
(32 + 7) true true true 0 50 false 0))
{l1: l1 (lapic adt)}
{l2: l2 (lapic adt)}
{l3: l3 (lapic adt)}
}
{ioapic / s / CurrentIrq: None} {vmxinfo: real_vmxinfo} {pg: true} {LAT: real_LAT (LAT adt)} {nps: real_nps}
{AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool adt)}
{idpde: real_idpde (idpde adt)} {pb: real_ptb (pb adt)}
else
None
else
None
| _ ⇒ None
end.
End OBJ_LMM.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Section PT_NEW_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_pb}.
Context {re4: relate_impl_AC}.
Lemma pt_new_exist:
∀ s habd habd´ labd id q i f,
pt_new_spec id q habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, pt_new_spec id q labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold pt_new_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto; intros.
exploit relate_impl_pb_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_pb_update.
apply relate_impl_AC_update. assumption.
Qed.
Context {mt1: match_impl_pb}.
Context {mt2: match_impl_AC}.
Lemma pt_new_match:
∀ s d d´ m id q i f,
pt_new_spec id q d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold pt_new_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_pb_update.
eapply match_impl_AC_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) pt_new_spec}.
Context {inv0: PreservesInvariants (HD:= data0) pt_new_spec}.
Lemma pt_new_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem pt_new_spec)
(id ↦ gensem pt_new_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pt_new_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply pt_new_match; eauto.
Qed.
End PT_NEW_SIM.
Section PT_FREE_PDE0_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_LAT}.
Context {re5: relate_impl_pperm}.
Context {re6: relate_impl_ipt}.
Context {re7: relate_impl_ptpool}.
Lemma ptFreePDE0_exist:
∀ s n v habd habd´ labd f,
ptFreePDE0_spec n v habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ptFreePDE0_spec n v labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptFreePDE0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ptpool_eq; eauto; intros.
exploit relate_impl_LAT_eq; eauto; intros.
exploit relate_impl_ipt_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_ptpool_update.
apply relate_impl_pperm_update.
apply relate_impl_LAT_update.
assumption.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_LAT}.
Lemma ptFreePDE0_match:
∀ s n v d d´ m f,
ptFreePDE0_spec n v d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptFreePDE0_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ptpool_update.
eapply match_impl_pperm_update.
eapply match_impl_LAT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ptFreePDE0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ptFreePDE0_spec}.
Lemma ptFreePDE0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ptFreePDE0_spec)
(id ↦ gensem ptFreePDE0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ptFreePDE0_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ptFreePDE0_match; eauto.
Qed.
End PT_FREE_PDE0_SIM.
Section PT_RMV0_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_LAT}.
Context {re6: relate_impl_ipt}.
Context {re7: relate_impl_ptpool}.
Lemma ptRmv0_exist:
∀ s n v habd habd´ labd i f,
ptRmv0_spec n v habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptRmv0_spec n v labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptRmv0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ptpool_eq; eauto; intros.
exploit relate_impl_LAT_eq; eauto; intros.
exploit relate_impl_ipt_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_ptpool_update.
apply relate_impl_LAT_update.
assumption.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_LAT}.
Lemma ptRmv0_match:
∀ s n v d d´ m f i,
ptRmv0_spec n v d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptRmv0_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ptpool_update.
eapply match_impl_LAT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ptRmv0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ptRmv0_spec}.
Lemma ptRmv0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ptRmv0_spec)
(id ↦ gensem ptRmv0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ptRmv0_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ptRmv0_match; eauto.
Qed.
End PT_RMV0_SIM.
Section PMAP_INIT_SIM.
Context `{real_params: RealParams}.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_PT}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_nps}.
Context {re6: relate_impl_ipt}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_idpde}.
Context {re9: relate_impl_pb}.
Context {re10: relate_impl_vmxinfo}.
Context {re11: relate_impl_AC}.
Context {re12: relate_impl_in_intr}.
Context {re13: relate_impl_ioapic}.
Context {re14: relate_impl_lapic}.
Lemma pmap_init_exist:
∀ s (habd habd´ labd: RData) (n:Z) f,
pmap_init_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, pmap_init_spec n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold pmap_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_PT_eq; eauto.
exploit relate_impl_vmxinfo_eq; eauto.
exploit relate_impl_LAT_eq; eauto.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_nps_eq; eauto.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_idpde_eq; eauto.
exploit relate_impl_in_intr_eq; eauto.
exploit relate_impl_pb_eq; eauto; intros.
exploit relate_impl_ioapic_eq; eauto; intros.
exploit relate_impl_lapic_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_pb_update.
apply relate_impl_idpde_update.
apply relate_impl_ptpool_update.
apply relate_impl_PT_update.
apply relate_impl_init_update.
apply relate_impl_AC_update.
apply relate_impl_nps_update.
apply relate_impl_LAT_update.
apply relate_impl_pg_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_ioapic_update.
apply relate_impl_lapic_update.
apply relate_impl_ioapic_update.
assumption.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_LAT}.
Context {mt3: match_impl_idpde}.
Context {mt4: match_impl_PT}.
Context {mt5: match_impl_init}.
Context {mt6: match_impl_nps}.
Context {mt7: match_impl_iflags}.
Context {mt8: match_impl_pb}.
Context {mt9: match_impl_vmxinfo}.
Context {mt10: match_impl_AC}.
Context {mt11: match_impl_ioapic}.
Context {mt12: match_impl_lapic}.
Lemma pmap_init_match:
∀ s n d d´ m f,
pmap_init_spec n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold pmap_init_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_pb_update.
eapply match_impl_idpde_update.
eapply match_impl_ptpool_update.
eapply match_impl_PT_update.
eapply match_impl_init_update.
eapply match_impl_AC_update.
eapply match_impl_nps_update.
eapply match_impl_LAT_update.
eapply match_impl_pg_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) pmap_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) pmap_init_spec}.
Lemma pmap_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem pmap_init_spec)
(id ↦ gensem pmap_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pmap_init_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply pmap_init_match; eauto.
Qed.
End PMAP_INIT_SIM.
Section PT_INIT_SIM.
Context `{real_params: RealParams}.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_PT}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_nps}.
Context {re6: relate_impl_ipt}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_idpde}.
Context {re9: relate_impl_vmxinfo}.
Context {re10: relate_impl_in_intr}.
Context {re11: relate_impl_AC}.
Context {re12: relate_impl_ioapic}.
Context {re13: relate_impl_lapic}.
Lemma pt_init_exist:
∀ s (habd habd´ labd: RData) (n:Z) f,
pt_init_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, pt_init_spec n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold pt_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_PT_eq; eauto.
exploit relate_impl_LAT_eq; eauto.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_nps_eq; eauto.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_in_intr_eq; eauto.
exploit relate_impl_vmxinfo_eq; eauto.
exploit relate_impl_idpde_eq; eauto; intros.
exploit relate_impl_ioapic_eq; eauto; intros.
exploit relate_impl_lapic_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_idpde_update.
apply relate_impl_ptpool_update.
apply relate_impl_PT_update.
apply relate_impl_init_update.
apply relate_impl_AC_update.
apply relate_impl_nps_update.
apply relate_impl_LAT_update.
apply relate_impl_pg_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_ioapic_update.
apply relate_impl_lapic_update.
apply relate_impl_ioapic_update.
assumption.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_LAT}.
Context {mt3: match_impl_idpde}.
Context {mt4: match_impl_PT}.
Context {mt5: match_impl_init}.
Context {mt6: match_impl_nps}.
Context {mt7: match_impl_iflags}.
Context {mt8: match_impl_vmxinfo}.
Context {mt9: match_impl_AC}.
Context {mt10: match_impl_ioapic}.
Context {mt11: match_impl_lapic}.
Lemma pt_init_match:
∀ s n d d´ m f,
pt_init_spec n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold pt_init_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_idpde_update.
eapply match_impl_ptpool_update.
eapply match_impl_PT_update.
eapply match_impl_init_update.
eapply match_impl_AC_update.
eapply match_impl_nps_update.
eapply match_impl_LAT_update.
eapply match_impl_pg_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) pt_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) pt_init_spec}.
Lemma pt_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem pt_init_spec)
(id ↦ gensem pt_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pt_init_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply pt_init_match; eauto.
Qed.
End PT_INIT_SIM.
Section PFREE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_pperm}.
Context {re6: relate_impl_ipt}.
Lemma pfree_exist:
∀ s habd habd´ labd i f,
pfree_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, pfree_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold pfree_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_LAT_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
exploit relate_impl_ipt_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_pperm_update.
apply relate_impl_LAT_update. assumption.
Qed.
Context {mt1: match_impl_pperm}.
Context {mt2: match_impl_LAT}.
Lemma pfree_match:
∀ s d d´ m i f,
pfree_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold pfree_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_pperm_update.
eapply match_impl_LAT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) pfree_spec}.
Context {inv0: PreservesInvariants (HD:= data0) pfree_spec}.
Lemma pfree_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem pfree_spec)
(id ↦ gensem pfree_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pfree_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply pfree_match; eauto.
Qed.
End PFREE_SIM.
Section SETPT_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_PT}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_ptpool}.
Lemma setPT_exist:
∀ s habd habd´ labd i f,
setPT_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setPT_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold setPT_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_ptpool_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
eapply relate_impl_PT_update; assumption.
Qed.
Context {mt1: match_impl_PT}.
Lemma setPT_match:
∀ s d d´ m i f,
setPT_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setPT_spec; intros. subdestruct; trivial.
inv H. eapply match_impl_PT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) setPT_spec}.
Context {inv0: PreservesInvariants (HD:= data0) setPT_spec}.
Lemma setPT_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem setPT_spec)
(id ↦ gensem setPT_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit setPT_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply setPT_match; eauto.
Qed.
End SETPT_SIM.
Section PTIN_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_PT}.
Context {re3: relate_impl_ipt}.
Lemma ptin_exist:
∀ s habd habd´ labd f,
ptin_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ptin_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold ptin_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_PT_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ipt_update. assumption.
Qed.
Context {mt1: match_impl_ipt}.
Lemma ptin_match:
∀ s d d´ m f,
ptin_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptin_spec; intros. subdestruct.
inv H. eapply match_impl_ipt_update. assumption.
Qed.
Context {inv: PrimInvariants (data_ops:= data_ops) ptin_spec}.
Context {inv0: PrimInvariants (data_ops:= data_ops0) ptin_spec}.
Lemma ptin_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem´ ptin_spec (prim_ident:= id))
(id ↦ primcall_general_compatsem´ ptin_spec (prim_ident:= id)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
exploit ptin_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ptin_match; eauto.
Qed.
End PTIN_SIM.
End OBJ_SIM.
match (init adt, pg adt, in_intr adt, ikern adt, ihost adt, ipt adt) with
| (false, false, false, true, true, true) ⇒
let n := adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
if zeq n (Zlength (adt.(ioapic).(s).(IoApicIrqs))) then
if zeq n (Zlength (adt.(ioapic).(s).(IoApicEnables))) then
Some adt {ioapic/s: ioapic_init_aux adt.(ioapic).(s) (Z.to_nat (n - 1))} {lapic: (mkLApicData
(mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic adt))) true
(32 + 7) true true true 0 50 false 0))
{l1: l1 (lapic adt)}
{l2: l2 (lapic adt)}
{l3: l3 (lapic adt)}
}
{ioapic / s / CurrentIrq: None} {vmxinfo: real_vmxinfo} {pg: true} {LAT: real_LAT (LAT adt)} {nps: real_nps}
{AC: AC_init} {init: true} {PT: 0} {ptpool: real_pt (ptpool adt)}
{idpde: real_idpde (idpde adt)} {pb: real_ptb (pb adt)}
else
None
else
None
| _ ⇒ None
end.
End OBJ_LMM.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Section PT_NEW_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_pb}.
Context {re4: relate_impl_AC}.
Lemma pt_new_exist:
∀ s habd habd´ labd id q i f,
pt_new_spec id q habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, pt_new_spec id q labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold pt_new_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto; intros.
exploit relate_impl_pb_eq; eauto; intros.
exploit relate_impl_AC_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_pb_update.
apply relate_impl_AC_update. assumption.
Qed.
Context {mt1: match_impl_pb}.
Context {mt2: match_impl_AC}.
Lemma pt_new_match:
∀ s d d´ m id q i f,
pt_new_spec id q d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold pt_new_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_pb_update.
eapply match_impl_AC_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) pt_new_spec}.
Context {inv0: PreservesInvariants (HD:= data0) pt_new_spec}.
Lemma pt_new_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem pt_new_spec)
(id ↦ gensem pt_new_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pt_new_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply pt_new_match; eauto.
Qed.
End PT_NEW_SIM.
Section PT_FREE_PDE0_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_LAT}.
Context {re5: relate_impl_pperm}.
Context {re6: relate_impl_ipt}.
Context {re7: relate_impl_ptpool}.
Lemma ptFreePDE0_exist:
∀ s n v habd habd´ labd f,
ptFreePDE0_spec n v habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ptFreePDE0_spec n v labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptFreePDE0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ptpool_eq; eauto; intros.
exploit relate_impl_LAT_eq; eauto; intros.
exploit relate_impl_ipt_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_ptpool_update.
apply relate_impl_pperm_update.
apply relate_impl_LAT_update.
assumption.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_LAT}.
Lemma ptFreePDE0_match:
∀ s n v d d´ m f,
ptFreePDE0_spec n v d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptFreePDE0_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ptpool_update.
eapply match_impl_pperm_update.
eapply match_impl_LAT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ptFreePDE0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ptFreePDE0_spec}.
Lemma ptFreePDE0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ptFreePDE0_spec)
(id ↦ gensem ptFreePDE0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ptFreePDE0_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ptFreePDE0_match; eauto.
Qed.
End PT_FREE_PDE0_SIM.
Section PT_RMV0_SIM.
Context {re1: relate_impl_iflags}.
Context {re3: relate_impl_LAT}.
Context {re6: relate_impl_ipt}.
Context {re7: relate_impl_ptpool}.
Lemma ptRmv0_exist:
∀ s n v habd habd´ labd i f,
ptRmv0_spec n v habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptRmv0_spec n v labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptRmv0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ptpool_eq; eauto; intros.
exploit relate_impl_LAT_eq; eauto; intros.
exploit relate_impl_ipt_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_ptpool_update.
apply relate_impl_LAT_update.
assumption.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_LAT}.
Lemma ptRmv0_match:
∀ s n v d d´ m f i,
ptRmv0_spec n v d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptRmv0_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_ptpool_update.
eapply match_impl_LAT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) ptRmv0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) ptRmv0_spec}.
Lemma ptRmv0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem ptRmv0_spec)
(id ↦ gensem ptRmv0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit ptRmv0_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply ptRmv0_match; eauto.
Qed.
End PT_RMV0_SIM.
Section PMAP_INIT_SIM.
Context `{real_params: RealParams}.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_PT}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_nps}.
Context {re6: relate_impl_ipt}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_idpde}.
Context {re9: relate_impl_pb}.
Context {re10: relate_impl_vmxinfo}.
Context {re11: relate_impl_AC}.
Context {re12: relate_impl_in_intr}.
Context {re13: relate_impl_ioapic}.
Context {re14: relate_impl_lapic}.
Lemma pmap_init_exist:
∀ s (habd habd´ labd: RData) (n:Z) f,
pmap_init_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, pmap_init_spec n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold pmap_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_PT_eq; eauto.
exploit relate_impl_vmxinfo_eq; eauto.
exploit relate_impl_LAT_eq; eauto.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_nps_eq; eauto.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_idpde_eq; eauto.
exploit relate_impl_in_intr_eq; eauto.
exploit relate_impl_pb_eq; eauto; intros.
exploit relate_impl_ioapic_eq; eauto; intros.
exploit relate_impl_lapic_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_pb_update.
apply relate_impl_idpde_update.
apply relate_impl_ptpool_update.
apply relate_impl_PT_update.
apply relate_impl_init_update.
apply relate_impl_AC_update.
apply relate_impl_nps_update.
apply relate_impl_LAT_update.
apply relate_impl_pg_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_ioapic_update.
apply relate_impl_lapic_update.
apply relate_impl_ioapic_update.
assumption.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_LAT}.
Context {mt3: match_impl_idpde}.
Context {mt4: match_impl_PT}.
Context {mt5: match_impl_init}.
Context {mt6: match_impl_nps}.
Context {mt7: match_impl_iflags}.
Context {mt8: match_impl_pb}.
Context {mt9: match_impl_vmxinfo}.
Context {mt10: match_impl_AC}.
Context {mt11: match_impl_ioapic}.
Context {mt12: match_impl_lapic}.
Lemma pmap_init_match:
∀ s n d d´ m f,
pmap_init_spec n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold pmap_init_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_pb_update.
eapply match_impl_idpde_update.
eapply match_impl_ptpool_update.
eapply match_impl_PT_update.
eapply match_impl_init_update.
eapply match_impl_AC_update.
eapply match_impl_nps_update.
eapply match_impl_LAT_update.
eapply match_impl_pg_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) pmap_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) pmap_init_spec}.
Lemma pmap_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem pmap_init_spec)
(id ↦ gensem pmap_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pmap_init_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply pmap_init_match; eauto.
Qed.
End PMAP_INIT_SIM.
Section PT_INIT_SIM.
Context `{real_params: RealParams}.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_PT}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_nps}.
Context {re6: relate_impl_ipt}.
Context {re7: relate_impl_ptpool}.
Context {re8: relate_impl_idpde}.
Context {re9: relate_impl_vmxinfo}.
Context {re10: relate_impl_in_intr}.
Context {re11: relate_impl_AC}.
Context {re12: relate_impl_ioapic}.
Context {re13: relate_impl_lapic}.
Lemma pt_init_exist:
∀ s (habd habd´ labd: RData) (n:Z) f,
pt_init_spec n habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, pt_init_spec n labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold pt_init_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_PT_eq; eauto.
exploit relate_impl_LAT_eq; eauto.
exploit relate_impl_init_eq; eauto.
exploit relate_impl_nps_eq; eauto.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_in_intr_eq; eauto.
exploit relate_impl_vmxinfo_eq; eauto.
exploit relate_impl_idpde_eq; eauto; intros.
exploit relate_impl_ioapic_eq; eauto; intros.
exploit relate_impl_lapic_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_idpde_update.
apply relate_impl_ptpool_update.
apply relate_impl_PT_update.
apply relate_impl_init_update.
apply relate_impl_AC_update.
apply relate_impl_nps_update.
apply relate_impl_LAT_update.
apply relate_impl_pg_update.
apply relate_impl_vmxinfo_update.
apply relate_impl_ioapic_update.
apply relate_impl_lapic_update.
apply relate_impl_ioapic_update.
assumption.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_LAT}.
Context {mt3: match_impl_idpde}.
Context {mt4: match_impl_PT}.
Context {mt5: match_impl_init}.
Context {mt6: match_impl_nps}.
Context {mt7: match_impl_iflags}.
Context {mt8: match_impl_vmxinfo}.
Context {mt9: match_impl_AC}.
Context {mt10: match_impl_ioapic}.
Context {mt11: match_impl_lapic}.
Lemma pt_init_match:
∀ s n d d´ m f,
pt_init_spec n d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold pt_init_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_idpde_update.
eapply match_impl_ptpool_update.
eapply match_impl_PT_update.
eapply match_impl_init_update.
eapply match_impl_AC_update.
eapply match_impl_nps_update.
eapply match_impl_LAT_update.
eapply match_impl_pg_update.
eapply match_impl_vmxinfo_update.
eapply match_impl_ioapic_update.
eapply match_impl_lapic_update.
eapply match_impl_ioapic_update.
assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) pt_init_spec}.
Context {inv0: PreservesInvariants (HD:= data0) pt_init_spec}.
Lemma pt_init_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem pt_init_spec)
(id ↦ gensem pt_init_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pt_init_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply pt_init_match; eauto.
Qed.
End PT_INIT_SIM.
Section PFREE_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_init}.
Context {re3: relate_impl_LAT}.
Context {re4: relate_impl_nps}.
Context {re5: relate_impl_pperm}.
Context {re6: relate_impl_ipt}.
Lemma pfree_exist:
∀ s habd habd´ labd i f,
pfree_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, pfree_spec i labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold pfree_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_LAT_eq; eauto; intros.
exploit relate_impl_pperm_eq; eauto; intros.
exploit relate_impl_ipt_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_pperm_update.
apply relate_impl_LAT_update. assumption.
Qed.
Context {mt1: match_impl_pperm}.
Context {mt2: match_impl_LAT}.
Lemma pfree_match:
∀ s d d´ m i f,
pfree_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold pfree_spec; intros. subdestruct; inv H; trivial.
eapply match_impl_pperm_update.
eapply match_impl_LAT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) pfree_spec}.
Context {inv0: PreservesInvariants (HD:= data0) pfree_spec}.
Lemma pfree_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem pfree_spec)
(id ↦ gensem pfree_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit pfree_exist; eauto 1; intros (labd´ & HP & HM).
match_external_states_simpl.
eapply pfree_match; eauto.
Qed.
End PFREE_SIM.
Section SETPT_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_PT}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_ptpool}.
Lemma setPT_exist:
∀ s habd habd´ labd i f,
setPT_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, setPT_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold setPT_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_ptpool_eq; eauto. intros.
revert H; subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
eapply relate_impl_PT_update; assumption.
Qed.
Context {mt1: match_impl_PT}.
Lemma setPT_match:
∀ s d d´ m i f,
setPT_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold setPT_spec; intros. subdestruct; trivial.
inv H. eapply match_impl_PT_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) setPT_spec}.
Context {inv0: PreservesInvariants (HD:= data0) setPT_spec}.
Lemma setPT_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem setPT_spec)
(id ↦ gensem setPT_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit setPT_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply setPT_match; eauto.
Qed.
End SETPT_SIM.
Section PTIN_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_PT}.
Context {re3: relate_impl_ipt}.
Lemma ptin_exist:
∀ s habd habd´ labd f,
ptin_spec habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, ptin_spec labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold ptin_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_PT_eq; eauto. intros.
revert H; subrewrite. subdestruct.
inv HQ. refine_split´; trivial.
eapply relate_impl_ipt_update. assumption.
Qed.
Context {mt1: match_impl_ipt}.
Lemma ptin_match:
∀ s d d´ m f,
ptin_spec d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptin_spec; intros. subdestruct.
inv H. eapply match_impl_ipt_update. assumption.
Qed.
Context {inv: PrimInvariants (data_ops:= data_ops) ptin_spec}.
Context {inv0: PrimInvariants (data_ops:= data_ops0) ptin_spec}.
Lemma ptin_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_general_compatsem´ ptin_spec (prim_ident:= id))
(id ↦ primcall_general_compatsem´ ptin_spec (prim_ident:= id)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
inv match_extcall_states.
exploit ptin_exist; eauto 1. intros [labd´ [HP HM]].
match_external_states_simpl.
eapply ptin_match; eauto.
Qed.
End PTIN_SIM.
End OBJ_SIM.