Library mcertikos.objects.ObjLMM1
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import ObjInterruptDriver.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalTicketLock.
Section OBJ_LMM.
Context `{real_params: RealParams}.
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.
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.
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
| LATCValid l ⇒
let pdt´:= ZMap.set pti PTEUnPresent pdt in
let pt´ := ZMap.set pdi (PDEValid pi pdt´) pt in
if zlt_le 0 (Z.of_nat (length l)) Int.max_unsigned then
Some (adt {LAT: ZMap.set padr (LATCValid (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, ikern adt, ihost adt, ipt adt, in_intr adt) with
| (false, false, true, true, true, false) ⇒
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)}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock 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
| LATCValid l ⇒
let pdt´:= ZMap.set pti PTEUnPresent pdt in
let pt´ := ZMap.set pdi (PDEValid pi pdt´) pt in
if zlt_le 0 (Z.of_nat (length l)) Int.max_unsigned then
Some (adt {LAT: ZMap.set padr (LATCValid (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, ikern adt, ihost adt, ipt adt, in_intr adt) with
| (false, false, true, true, true, false) ⇒
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)}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock 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 pt_new_spec (id q: Z) (adt: RData): option (RData × Z) :=
let c := ZMap.get id (AC adt) in
let i := id × max_children + 1 + Z_of_nat (length (cchildren c)) in
match (pg adt, ikern adt, ihost adt, ipt adt, cused c, cused (ZMap.get i (AC adt)), zle_lt 0 i num_proc,
zlt (Z_of_nat (length (cchildren c))) max_children,
zle_le 0 q (cquota c - cusage c)) with
| (true, true, true, true, true, false, left _, left _, left _) ⇒
let child := mkContainer q 0 id nil true in
let parent := (mkContainer (cquota c) (cusage c + q)
(cparent c) (i :: cchildren c) (cused c)) in
Some (adt {AC: ZMap.set i child (ZMap.set id parent (AC adt))}, i)
| _ ⇒ 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, ikern adt, ihost adt, ipt adt, in_intr adt) with
| (false, false, true, true, true, false) ⇒
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)}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock adt)}
{idpde: real_idpde (idpde 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 {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_AC_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_AC_update. assumption.
Qed.
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_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_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 {re10: relate_impl_vmxinfo}.
Context {re11: relate_impl_AC}.
Context {mt100: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {re20: relate_impl_multi_log}.
Context {re300: relate_impl_ioapic}.
Context {re301: relate_impl_lapic}.
Context {re302: relate_impl_in_intr}.
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_lock_eq; eauto.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_ioapic_eq; eauto; intros.
exploit relate_impl_lapic_eq; eauto; intros.
exploit relate_impl_in_intr_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_idpde_update.
apply relate_impl_lock_update.
apply relate_impl_multi_log_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 {mt9: match_impl_vmxinfo}.
Context {mt10: match_impl_AC}.
Context {mt50: match_impl_multi_log}.
Context {mt60: match_impl_ioapic}.
Context {mt61: 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_idpde_update.
eapply match_impl_lock_update.
eapply match_impl_multi_log_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 {re11: relate_impl_AC}.
Context {mt100: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {re20: relate_impl_multi_log}.
Context {re300: relate_impl_ioapic}.
Context {re301: relate_impl_lapic}.
Context {re302: relate_impl_in_intr}.
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_vmxinfo_eq; eauto.
exploit relate_impl_lock_eq; eauto.
exploit relate_impl_multi_log_eq; eauto.
exploit relate_impl_idpde_eq; eauto; intros.
exploit relate_impl_ioapic_eq; eauto; intros.
exploit relate_impl_lapic_eq; eauto; intros.
exploit relate_impl_in_intr_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_idpde_update.
apply relate_impl_lock_update.
apply relate_impl_multi_log_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 {mt50: match_impl_multi_log}.
Context {mt60: match_impl_ioapic}.
Context {mt61: 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_lock_update.
eapply match_impl_multi_log_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 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, ikern adt, ihost adt, ipt adt, in_intr adt) with
| (false, false, true, true, true, false) ⇒
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)}
{multi_log: real_multi_log (multi_log adt)}
{lock: real_lock (lock adt)}
{idpde: real_idpde (idpde 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 {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_AC_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_AC_update. assumption.
Qed.
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_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_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 {re10: relate_impl_vmxinfo}.
Context {re11: relate_impl_AC}.
Context {mt100: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {re20: relate_impl_multi_log}.
Context {re300: relate_impl_ioapic}.
Context {re301: relate_impl_lapic}.
Context {re302: relate_impl_in_intr}.
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_lock_eq; eauto.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_ioapic_eq; eauto; intros.
exploit relate_impl_lapic_eq; eauto; intros.
exploit relate_impl_in_intr_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_idpde_update.
apply relate_impl_lock_update.
apply relate_impl_multi_log_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 {mt9: match_impl_vmxinfo}.
Context {mt10: match_impl_AC}.
Context {mt50: match_impl_multi_log}.
Context {mt60: match_impl_ioapic}.
Context {mt61: 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_idpde_update.
eapply match_impl_lock_update.
eapply match_impl_multi_log_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 {re11: relate_impl_AC}.
Context {mt100: match_impl_lock}.
Context {re200: relate_impl_lock}.
Context {re20: relate_impl_multi_log}.
Context {re300: relate_impl_ioapic}.
Context {re301: relate_impl_lapic}.
Context {re302: relate_impl_in_intr}.
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_vmxinfo_eq; eauto.
exploit relate_impl_lock_eq; eauto.
exploit relate_impl_multi_log_eq; eauto.
exploit relate_impl_idpde_eq; eauto; intros.
exploit relate_impl_ioapic_eq; eauto; intros.
exploit relate_impl_lapic_eq; eauto; intros.
exploit relate_impl_in_intr_eq; eauto; intros.
revert H. subrewrite.
subdestruct; inv HQ; refine_split´; trivial.
apply relate_impl_idpde_update.
apply relate_impl_lock_update.
apply relate_impl_multi_log_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 {mt50: match_impl_multi_log}.
Context {mt60: match_impl_ioapic}.
Context {mt61: 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_lock_update.
eapply match_impl_multi_log_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 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.