Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import ZSet.
Require Import ListLemma2.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import AuxStateDataType.
Require Import RealParams.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import LayerCalculusLemma.
Require Import TacticsForTesting.
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 MmioSPTWalk.Spec.
Require Import MmioPTWalk.Spec.
Require Import AbsMachine.Spec.
Require Import MmioPTAlloc.Spec.
Require Import RData.
Require Import MmioSPTWalk.Layer.
Require Import Constants.
Require Import HypsecCommLib.
Require Import MmioPTWalk.Layer.
Require Import NPTWalk.ProofHighAux.
Local Open Scope Z_scope.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.
Section MmioSPTWalkProofHigh.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := MmioSPTWalk_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := MmioPTWalk_ops) HDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Inductive relate_entry (cbndx: Z) (index: Z) (hspt: SPT) (lspt: SPT): Z -> Z -> Z -> Prop :=
| RELATE_ENTRY:
forall addr pfn pte
(Hpfn: pfn = phys_page pte / PAGE_SIZE)
(Hpte: let vttbr_pa := SMMU_TTBR index cbndx in
let pgd_idx := stage2_pgd_index addr in
let pgd_p := Z.lor vttbr_pa (pgd_idx * 8) in
let pgd := ZMap.get pgd_p (spt_vttbr_pool lspt) in
let pgd_pa := phys_page pgd in
((pgd = 0 /\ pte = 0) \/
(pgd <> 0 /\ let pmd_idx := pmd_index addr in
let pmd_p := Z.lor pgd_pa (pmd_idx * 8) in
let pmd := ZMap.get pmd_p (spt_pgd_pool lspt) in
let pmd_pa := phys_page pmd in
(pmd = 0 /\ pte = 0) \/
(pmd <> 0 /\ let pte_idx := pte_index addr in
let pte_p := Z.lor pmd_pa (pte_idx * 8) in
ZMap.get pte_p (spt_pmd_pool lspt) = pte)))),
relate_entry cbndx index hspt lspt addr pfn pte.
Inductive valid_lspt (lspt: SPT) : Prop :=
| VALID_LSPT
(Hvttbr_pool_range: forall p, is_int64 (p @ (spt_vttbr_pool lspt)) = true)
(Hpgd_pool_range: forall p, is_int64 (p @ (spt_pgd_pool lspt)) = true)
(Hpmd_pool_range: forall p, is_int64 (p @ (spt_pmd_pool lspt)) = true)
(Hpgd_next_range: SMMU_PGD_START <= spt_pgd_next lspt <= SMMU_PMD_START)
(Hpmd_next_range: SMMU_PMD_START <= spt_pmd_next lspt <= SMMU_POOL_END)
(Hpgd_next_align: phys_page (spt_pgd_next lspt) = (spt_pgd_next lspt))
(Hpmd_next_align: phys_page (spt_pmd_next lspt) = (spt_pmd_next lspt))
(Hpgd_next: forall addr, addr >= spt_pgd_next lspt -> addr @ (spt_pgd_pool lspt) = 0)
(Hpmd_next: forall addr, addr >= spt_pmd_next lspt -> addr @ (spt_pmd_pool lspt) = 0)
(Hvttbr_pool: forall addr, addr @ (spt_vttbr_pool lspt) = 0 \/
(SMMU_PGD_START <= phys_page (addr @ (spt_vttbr_pool lspt)) < spt_pgd_next lspt /\
(phys_page (addr @ (spt_vttbr_pool lspt))) @ (spt_pgd_par lspt) = addr))
(Hpgd_pool: forall addr, addr @ (spt_pgd_pool lspt) = 0 \/
(SMMU_PMD_START <= phys_page (addr @ (spt_pgd_pool lspt)) < spt_pmd_next lspt /\
(phys_page (addr @ (spt_pgd_pool lspt))) @ (spt_pmd_par lspt) = addr)):
valid_lspt lspt.
Inductive relate_spt : SPT -> SPT -> Prop :=
| RELATE_SPT:
forall hspt lspt
(Hvalid: valid_lspt lspt)
(Hnext_pgd: spt_pgd_next hspt = spt_pgd_next lspt)
(Hnext_pmd: spt_pmd_next hspt = spt_pmd_next lspt)
(Hpgd_t: forall cbndx index addr (ge0: 0 <= addr),
let vttbr_p := SMMU_TTBR index cbndx in
let pgd_idx := stage2_pgd_index addr in
pgd_idx @ (vttbr_p @ (spt_pgd_t hspt)) = true <->
let pgd_p := Z.lor vttbr_p (pgd_idx * 8) in
pgd_p @ (spt_vttbr_pool lspt) <> 0)
(Hpmd_t: forall cbndx index addr (ge0: 0 <= addr),
let vttbr_p := SMMU_TTBR index cbndx in
let pgd_idx := stage2_pgd_index addr in
let pmd_idx := pmd_index addr in
pmd_idx @ (pgd_idx @ (vttbr_p @ (spt_pmd_t hspt))) = true <->
let pgd_p := Z.lor vttbr_p (pgd_idx * 8) in
let pgd := pgd_p @ (spt_vttbr_pool lspt) in
pgd <> 0 /\
let pmd_p := Z.lor (phys_page pgd) (pmd_idx * 8) in
let pmd := pmd_p @ (spt_pgd_pool lspt) in
pmd <> 0)
(Hrelate: forall cbndx index addr pfn pte
(Hvalid: valid_smmu_addr addr)
(Hhpt: (addr / PAGE_SIZE) @ ((SMMU_TTBR index cbndx) @ (spt_pt hspt)) = (pfn, pte)),
relate_entry cbndx index hspt lspt addr pfn pte),
relate_spt hspt lspt.
Record relate_RData (f:meminj) (hadt: HDATA) (ladt: LDATA) :=
mkrelate_RData {
id_icore: icore hadt = icore ladt;
id_ihost: ihost hadt = ihost ladt;
id_tstate: tstate hadt = tstate ladt;
id_curid: curid hadt = curid ladt;
id_cur_vmid: cur_vmid hadt = cur_vmid ladt;
id_cur_vcpuid: cur_vcpuid hadt = cur_vcpuid ladt;
id_regs: regs hadt = regs ladt;
id_lock: lock hadt = lock ladt;
id_region_cnt: region_cnt hadt = region_cnt ladt;
id_regions: regions hadt = regions ladt;
id_shadow_ctxts: shadow_ctxts hadt = shadow_ctxts ladt;
id_smmu_conf: smmu_conf hadt = smmu_conf ladt;
id_log: log hadt = log ladt;
id_oracle: oracle hadt = oracle ladt;
id_doracle: doracle hadt = doracle ladt;
id_core_doracle: core_doracle hadt = core_doracle ladt;
id_data_log: data_log hadt = data_log ladt;
id_core_data_log: core_data_log hadt = core_data_log ladt;
id_halt: halt (shared hadt) = halt (shared ladt);
id_flatmem: flatmem (shared hadt) = flatmem (shared ladt);
id_s2page: s2page (shared hadt) = s2page (shared ladt);
id_core_data: core_data (shared hadt) = core_data (shared ladt);
id_vminfos: vminfos (shared hadt) = vminfos (shared ladt);
id_npts: npts (shared hadt) = npts (shared ladt);
id_smmu_vmid: smmu_vmid (shared hadt) = smmu_vmid (shared ladt);
id_spts: (halt (shared ladt) = false) -> relate_spt (spts (shared hadt)) (spts (shared ladt))
}.
Inductive match_RData: stencil -> HDATA -> mem -> meminj -> Prop :=
| MATCH_RDATA: forall habd m f s, match_RData s habd m f.
Local Hint Resolve MATCH_RDATA.
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 := nil
}.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor; intros; simpl; trivial.
constructor; inv H; trivial.
Qed.
Section FreshPrim.
Hint Unfold
is_smmu_addr
valid_smmu_addr
get_smmu_cfg_hw_ttbr_spec
walk_smmu_pgd_spec
walk_smmu_pmd_spec
walk_smmu_pte_spec
set_smmu_pte_spec
check64_spec
panic_spec.
Lemma set_smmu_pt_spec_pgd_exists:
forall habd habd' labd cbndx index addr pte f
(Hspec: set_smmu_pt_spec cbndx index addr pte habd = Some habd')
(Hhalt: halt (shared habd) = false)
(Hpgd: match addr with VZ64 addr => (stage2_pgd_index addr) @ ((SMMU_TTBR index cbndx) @ (spt_pgd_t (spts (shared habd)))) = false end)
(Hrel: relate_RData f habd labd),
exists labd', set_smmu_pt_spec0 cbndx index addr pte labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros.
assert(range3: 0 <= 3 < 4096) by omega.
pose proof phys_page_or_not_change as phys_or.
assert(Hhaltl: halt (shared labd) = false).
{ destruct Hrel. srewrite. reflexivity. }
hsimpl_func Hspec.
rename z into addr. rename z0 into pte.
remember (spts (shared habd)) as hspt in *; symmetry in Heqhspt.
remember (spts (shared labd)) as lspt in *; symmetry in Heqlspt.
destruct Hrel. rewrite Hhaltl, Heqhspt, Heqlspt in id_spts0.
clear_hyp; simpl_local. destruct Hlocal.
unfold local_spt_map in C9. rename C9 into Hspec.
rewrite Hpgd in Hspec.
assert (Hpmd: (pmd_index addr) @ ((stage2_pgd_index addr) @ ((SMMU_TTBR index cbndx) @ (spt_pmd_t hspt))) = false).
{ match goal with | |- ?x = false => destruct x eqn: Hpmd end.
apply Hpmd_t in Hpmd. destruct Hpmd. apply Hpgd_t in H. contra.
bool_rel_all; omega. bool_rel_all; omega. reflexivity. }
rewrite Hpmd in Hspec. simpl_hyp Hspec; contra.
duplicate Hvalid. destruct D.
unfold set_smmu_pt_spec0.
repeat autounfold in *.
autounfold. repeat (srewrite; simpl). bool_rel_all; clear_hyp.
assert(Hlock: 2 @ (lock labd) = LockOwn true). srewrite. reflexivity.
assert(Htstate: (tstate labd =? 0) = true). srewrite. reflexivity.
extract_if. apply andb_true_iff; split; bool_rel; somega. rewrite Cond.
pose proof (vttbr_val cbndx index) as Hvttbr. autounfold in Hvttbr.
assert(vttbr_align: phys_page (SMMU_TTBR index cbndx) = SMMU_TTBR index cbndx).
{ autounfold. rewrite <- Hvttbr. rewrite phys_page_fixed. reflexivity. omega. omega. }
autounfold in vttbr_align. rewrite vttbr_align.
extract_if. unfold stage2_pgd_index.
match goal with |- context [Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 8192) end.
autounfold; apply or_index_range_8192; somega. apply andb_true_iff; split; bool_rel; omega. rewrite Cond0.
extract_if. apply Hvttbr_pool_range. rewrite Cond1.
rewrite andb_comm. simpl. destruct_if.
extract_if. apply andb_true_iff; split; bool_rel; omega. rewrite Cond2.
destruct_if.
simpl. extract_if. apply andb_true_iff; split; bool_rel; somega. rewrite Cond4.
rewrite Hhaltl, Hlock.
match goal with |- context [?c =? 0] => assert(c =? 0 = false) end.
bool_rel. apply or3nz. rewrite H. clear H.
extract_if. erewrite phys_or; try solve [assumption|omega].
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega.
apply andb_true_iff; split; bool_rel; omega. rewrite Cond5.
rewrite Hpgd_pool_range.
rewrite andb_comm. simpl. destruct_if.
extract_if. apply andb_true_iff; split; bool_rel; omega. rewrite Cond6.
destruct_if.
simpl. extract_if. apply andb_true_iff; split; bool_rel; somega. rewrite Cond8.
rewrite Hhaltl, Hlock, Htstate.
extract_if. erewrite phys_or; try solve [assumption|omega].
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega.
apply andb_true_iff; split; bool_rel; omega. rewrite Cond9.
simpl in Hspec. inv Hspec. clear Cond3 Cond7.
eexists; split. reflexivity. constructor; try assumption.
simpl. reflexivity. simpl. rewrite Hhaltl. reflexivity. simpl. intro T; clear T.
{
bool_rel_all. constructor; simpl.
- constructor; simpl; autounfold; intros.
+ destruct_zmap. apply andb_true_iff; split; bool_rel; somega.
apply Hvttbr_pool_range.
+ destruct_zmap. apply andb_true_iff; split; bool_rel; somega.
apply Hpgd_pool_range.
+ destruct_zmap. apply andb_true_iff; split; bool_rel; somega.
apply Hpmd_pool_range.
+ omega. + omega.
+ eapply phys_page_a_page. assumption. omega.
+ eapply phys_page_a_page. assumption. omega.
+ assert_gso. erewrite phys_or; try solve [assumption|omega].
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega. omega.
rewrite (ZMap.gso _ _ Hneq). apply Hpgd_next. omega.
+ assert_gso. erewrite phys_or; try solve [assumption|omega].
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega. omega.
rewrite (ZMap.gso _ _ Hneq). apply Hpmd_next. omega.
+ destruct_zmap. right. erewrite phys_or; try solve [assumption|omega].
rewrite ZMap.gss. split_and; try omega.
pose proof (Hvttbr_pool addr0). destruct H. left; assumption.
destruct H as (? & ?). right. split. omega.
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq). assumption.
+ destruct_zmap. right. erewrite phys_or; try solve [assumption|omega].
rewrite ZMap.gss. split_and; try omega.
pose proof (Hpgd_pool addr0). destruct H. left; assumption.
destruct H as (? & ?). right. split. omega.
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq). assumption.
- reflexivity. - reflexivity.
- intros.
destruct_zmap. destruct_zmap. split; intros; try reflexivity. apply or3nz.
assert_gso. apply or_index_ne_cond_8192. right; assumption. rewrite (ZMap.gso _ _ Hneq).
apply Hpgd_t. assumption.
assert_gso. apply or_index_ne_cond_8192. left; assumption. rewrite (ZMap.gso _ _ Hneq).
apply Hpgd_t. assumption.
- autounfold; intros.
destruct_zmap. destruct_zmap. destruct_zmap. split; intros; try reflexivity. split; apply or3nz.
assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
right; assumption. rewrite (ZMap.gso _ _ Hneq). split. intro T.
rewrite <- Heq, <- Heq0 in T; apply Hpmd_t in T. destruct T as (? & ?).
rewrite Heq, Heq0 in H. contra. assumption. intros (? & ?).
match type of H0 with ?a -> False => assert(a) end. apply Hpgd_next.
rewrite phys_or; try assumption.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega. omega. contra.
assert_gso. apply or_index_ne_cond_8192. right; assumption. rewrite (ZMap.gso _ _ Hneq).
assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
left. rewrite phys_or; try assumption.
match goal with |- phys_page (?a @ _) <> _ => pose proof (Hvttbr_pool a) end.
destruct H. rewrite H. replace (phys_page 0) with 0 by reflexivity. omega.
destruct H. clear H0. omega. rewrite (ZMap.gso _ _ Hneq0). apply Hpmd_t. assumption.
assert_gso. apply or_index_ne_cond_8192. left; assumption. rewrite (ZMap.gso _ _ Hneq).
assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
left. rewrite phys_or; try assumption.
match goal with |- phys_page (?a @ _) <> _ => pose proof (Hvttbr_pool a) end.
destruct H. rewrite H. replace (phys_page 0) with 0 by reflexivity. omega.
destruct H. clear H0. omega. rewrite (ZMap.gso _ _ Hneq0). apply Hpmd_t. assumption.
- intros. repeat autounfold in *.
destruct (SMMU_TTBR index0 cbndx0 =? SMMU_TTBR index cbndx) eqn:Heqvttbr; bool_rel.
autounfold in Heqvttbr. rewrite Heqvttbr in *; rewrite ZMap.gss in Hhpt.
destruct (addr0 / 4096 =? addr / 4096) eqn:Heqaddr; bool_rel.
rewrite Heqaddr in Hhpt. rewrite ZMap.gss in Hhpt. inv Hhpt. apply pte_same_cond in Heqaddr.
destruct Heqaddr as (pgd_same & pmd_same & pte_same).
constructor. reflexivity.
simpl. autounfold in *. rewrite Heqvttbr. rewrite pgd_same. rewrite pmd_same. rewrite pte_same.
repeat rewrite ZMap.gss. right. split. apply or3nz. right. split. apply or3nz. reflexivity.
autounfold; assumption. autounfold; split; assumption.
rewrite (ZMap.gso _ _ Heqaddr) in Hhpt.
rewrite <- Heqvttbr in Hhpt. apply Hrelate in Hhpt. destruct Hhpt; autounfold in *.
constructor. assumption. simpl. autounfold. rewrite Heqvttbr. repeat rewrite ZMap.gss.
destruct (stage2_pgd_index addr0 =? stage2_pgd_index addr) eqn:pgd_same; bool_rel.
rewrite pgd_same; repeat rewrite ZMap.gss. right. split. apply or3nz.
destruct (pmd_index addr0 =? pmd_index addr) eqn:pmd_same; bool_rel.
rewrite pmd_same; repeat rewrite ZMap.gss. right. split. apply or3nz.
destruct (pte_index addr0 =? pte_index addr) eqn:pte_same; bool_rel.
assert(addr0 / 4096 = addr / 4096).
apply pte_same_cond; try split_and; try assumption. autounfold; split; assumption. contra.
destruct Hpte. destruct H. rewrite H0.
assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
right; assumption. rewrite (ZMap.gso _ _ Hneq). apply Hpmd_next.
rewrite phys_or; try assumption.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega. omega. destruct H. rewrite Heqvttbr, pgd_same in H; contra.
destruct Hpte. destruct H. rewrite H0.
left. assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
right; assumption. rewrite (ZMap.gso _ _ Hneq). split. apply Hpgd_next.
rewrite phys_or; try assumption.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega. omega. reflexivity.
destruct H. rewrite Heqvttbr, pgd_same in H; contra.
assert_gso. apply or_index_ne_cond_8192. right; assumption. rewrite (ZMap.gso _ _ Hneq).
destruct Hpte. left; rewrite <- Heqvttbr; assumption. right. rewrite <- Heqvttbr.
destruct H as (T0 & T). split. assumption.
assert_gso. rewrite phys_or; try assumption. apply vttbr_pool_ne_pgd_next.
assumption. autounfold; somega. autounfold; somega.
rewrite (ZMap.gso _ _ Hneq0). destruct T as [T|T]. left; assumption. right.
destruct T as [T1 T]. split. assumption.
assert_gso. rewrite phys_or; try assumption.
apply pgd_pool_ne_pmd_next. assumption. autounfold; somega. autounfold; somega.
rewrite (ZMap.gso _ _ Hneq1). assumption. assumption.
autounfold in *. rewrite (ZMap.gso _ _ Heqvttbr) in Hhpt.
apply Hrelate in Hhpt. destruct Hhpt; autounfold in *.
constructor. assumption. autounfold. simpl.
assert_gso. apply or_index_ne_cond_8192. left; assumption. rewrite (ZMap.gso _ _ Hneq).
destruct Hpte. left; assumption. right.
destruct H as (T0 & T). split. assumption.
assert_gso. rewrite phys_or; try assumption. apply vttbr_pool_ne_pgd_next.
assumption. autounfold; somega. autounfold; somega.
rewrite (ZMap.gso _ _ Hneq0). destruct T as [T|T]. left; assumption. right.
destruct T as [T1 T]. split. assumption.
assert_gso. rewrite phys_or; try assumption.
apply pgd_pool_ne_pmd_next. assumption. autounfold; somega. autounfold; somega.
rewrite (ZMap.gso _ _ Hneq1). assumption. assumption.
}
simpl in Hspec; inv Hspec.
eexists; split. reflexivity. constructor; try assumption. simpl. omega. simpl. reflexivity. simpl. intro T; inversion T.
erewrite Hpgd_next in Case1. inversion Case1.
rewrite phys_or; try assumption.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega. omega.
simpl in Hspec; inv Hspec.
eexists; split. reflexivity. constructor; try assumption. simpl. omega. simpl. reflexivity. simpl. intro T; inversion T.
bool_rel. apply Hpgd_t in Case. contra. assumption.
Qed.
Lemma set_smmu_pt_spec_pmd_exists:
forall habd habd' labd cbndx index addr pte f
(Hspec: set_smmu_pt_spec cbndx index addr pte habd = Some habd')
(Hhalt: halt (shared habd) = false)
(Hpgd: match addr with VZ64 addr => (stage2_pgd_index addr) @ ((SMMU_TTBR index cbndx) @ (spt_pgd_t (spts (shared habd)))) = true end)
(Hpmd: match addr with VZ64 addr => (pmd_index addr) @ ((stage2_pgd_index addr) @ ((SMMU_TTBR index cbndx) @ (spt_pmd_t (spts (shared habd))))) = false end)
(Hrel: relate_RData f habd labd),
exists labd', set_smmu_pt_spec0 cbndx index addr pte labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros.
assert(range3: 0 <= 3 < 4096) by omega.
pose proof phys_page_or_not_change as phys_or.
assert(Hhaltl: halt (shared labd) = false).
{ destruct Hrel. srewrite. reflexivity. }
hsimpl_func Hspec.
rename z into addr. rename z0 into pte.
remember (spts (shared habd)) as hspt in *; symmetry in Heqhspt.
remember (spts (shared labd)) as lspt in *; symmetry in Heqlspt.
destruct Hrel. rewrite Hhaltl, Heqhspt, Heqlspt in id_spts0.
clear_hyp; simpl_local. destruct Hlocal.
unfold local_spt_map in C9. rename C9 into Hspec.
rewrite Hpgd, Hpmd in Hspec. simpl_hyp Hspec; contra.
duplicate Hvalid. destruct D.
unfold set_smmu_pt_spec0.
repeat autounfold in *.
autounfold. repeat (srewrite; simpl). bool_rel_all; clear_hyp.
assert(Hlock: 2 @ (lock labd) = LockOwn true). srewrite. reflexivity.
assert(Htstate: (tstate labd =? 0) = true). srewrite. reflexivity.
extract_if. apply andb_true_iff; split; bool_rel; somega. rewrite Cond.
pose proof (vttbr_val cbndx index) as Hvttbr. autounfold in Hvttbr.
assert(vttbr_align: phys_page (SMMU_TTBR index cbndx) = SMMU_TTBR index cbndx).
{ autounfold. rewrite <- Hvttbr. rewrite phys_page_fixed. reflexivity. omega. omega. }
autounfold in vttbr_align. rewrite vttbr_align.
extract_if. unfold stage2_pgd_index.
match goal with |- context [Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 8192) end.
autounfold; apply or_index_range_8192; somega. apply andb_true_iff; split; bool_rel; omega. rewrite Cond0.
extract_if. apply Hvttbr_pool_range. rewrite Cond1.
rewrite andb_comm. simpl. destruct_if.
bool_rel. apply Hpgd_t in Hpgd. inversion Hpgd. assumption. assumption.
rewrite Hvttbr_pool_range. rewrite Hhaltl, Hlock. rewrite Case.
extract_if. match goal with |- context[?a @ (spt_vttbr_pool _)] => pose proof (Hvttbr_pool a) end.
destruct H. rewrite H in Case. inversion Case. destruct H. clear H0.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega.
bool_rel_all; apply andb_true_iff; split; bool_rel. omega.
match type of H0 with _ <= _ < ?a => assert(a <= spt_pgd_next lspt) end.
eapply phys_page_lt_4096. apply phys_page_fixed. assumption. destruct H; assumption. omega. rewrite Cond2.
rewrite Heqlspt. rewrite Hpgd_pool_range. rewrite andb_comm. simpl. destruct_if.
extract_if. apply andb_true_iff; split; bool_rel; omega. rewrite Cond3.
destruct_if.
simpl. extract_if. apply andb_true_iff; split; bool_rel; somega. rewrite Cond5.
rewrite Hhaltl, Hlock, Htstate.
extract_if. erewrite phys_or; try solve [assumption|omega].
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega.
apply andb_true_iff; split; bool_rel; omega. rewrite Cond6.
rewrite andb_comm in Hspec; simpl in Hspec.
replace (spt_pgd_next lspt <=? 2162688) with true in Hspec by (symmetry; bool_rel; omega).
inv Hspec. clear Cond4.
eexists; split. reflexivity. constructor; try assumption.
simpl. reflexivity. simpl. rewrite Hhaltl. reflexivity. simpl. intro T; clear T.
{
bool_rel_all. constructor; simpl.
- constructor; simpl; autounfold; intros.
+ apply Hvttbr_pool_range.
+ destruct_zmap. apply andb_true_iff; split; bool_rel; somega.
apply Hpgd_pool_range.
+ destruct_zmap. apply andb_true_iff; split; bool_rel; somega.
apply Hpmd_pool_range.
+ omega. + omega.
+ assumption.
+ eapply phys_page_a_page. assumption. omega.
+ assert_gso. match goal with |- context[?a @ (spt_vttbr_pool _)] => pose proof (Hvttbr_pool a) end.
destruct H0. rewrite H0. replace (phys_page 0) with 0 by reflexivity.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. reflexivity. autounfold; somega. omega.
destruct H0. match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega.
match type of H2 with _ <= _ < ?a => assert(a <= spt_pgd_next (spts (shared labd))) end.
eapply phys_page_lt_4096. apply phys_page_fixed. assumption. omega. omega.
rewrite (ZMap.gso _ _ Hneq). apply Hpgd_next. omega.
+ assert_gso. erewrite phys_or; try solve [assumption|omega].
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega. omega.
rewrite (ZMap.gso _ _ Hneq). apply Hpmd_next. omega.
+ apply Hvttbr_pool.
+ destruct_zmap. right. erewrite phys_or; try solve [assumption|omega].
rewrite ZMap.gss. split_and; try omega.
pose proof (Hpgd_pool addr0). destruct H. left; assumption.
destruct H as (? & ?). right. split. omega.
assert_gso. omega. rewrite (ZMap.gso _ _ Hneq). assumption.
- reflexivity. - reflexivity.
- intros; autounfold.
match goal with |- ?c = true <-> _ =>
assert(c = ((stage2_pgd_index addr0) @ ((SMMU_TTBR index0 cbndx0) @ (spt_pgd_t (spts (shared habd)))))) end.
destruct (SMMU_TTBR index0 cbndx0 =? SMMU_TTBR index cbndx) eqn:Httbr_same; bool_rel; autounfold in Httbr_same.
rewrite Httbr_same. rewrite ZMap.gss.
destruct (stage2_pgd_index addr0 =? stage2_pgd_index addr) eqn:Hpgd_same; bool_rel.
rewrite Hpgd_same. rewrite ZMap.gss. autounfold; rewrite Httbr_same; rewrite Hpgd. reflexivity.
rewrite (ZMap.gso _ _ Hpgd_same). autounfold; rewrite Httbr_same; reflexivity.
rewrite (ZMap.gso _ _ Httbr_same). reflexivity.
rewrite H. apply Hpgd_t. assumption.
- autounfold; intros.
destruct_zmap. destruct_zmap. destruct_zmap. split; intros; try reflexivity. split. assumption. apply or3nz.
assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
right; assumption. rewrite (ZMap.gso _ _ Hneq). split. intro T.
rewrite <- Heq, <- Heq0 in T; apply Hpmd_t in T. rewrite Heq, Heq0 in *; assumption. assumption.
rewrite <- Heq, <- Heq0. apply Hpmd_t. assumption.
split. intro T. apply Hpmd_t in T. destruct T.
assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
left. apply pgd_index_diff_res_diff; auto. rewrite (ZMap.gso _ _ Hneq). split; assumption. assumption.
intros (? & ?). assert_gsoH H0. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
left. apply pgd_index_diff_res_diff; auto. rewrite (ZMap.gso _ _ Hneq) in H0.
apply Hpmd_t. assumption. split; assumption.
split. intro T. apply Hpmd_t in T. destruct T.
assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
left. apply pgd_index_diff_res_diff; auto. rewrite (ZMap.gso _ _ Hneq). split; assumption. assumption.
intros (? & ?). assert_gsoH H0. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
left. apply pgd_index_diff_res_diff; auto. rewrite (ZMap.gso _ _ Hneq) in H0.
apply Hpmd_t. assumption. split; assumption.
- intros. repeat autounfold in *.
destruct (SMMU_TTBR index0 cbndx0 =? SMMU_TTBR index cbndx) eqn:Heqvttbr; bool_rel.
autounfold in Heqvttbr. rewrite Heqvttbr in *; rewrite ZMap.gss in Hhpt.
destruct (addr0 / 4096 =? addr / 4096) eqn:Heqaddr; bool_rel.
rewrite Heqaddr in Hhpt. rewrite ZMap.gss in Hhpt. inv Hhpt. apply pte_same_cond in Heqaddr.
destruct Heqaddr as (pgd_same & pmd_same & pte_same).
constructor. reflexivity.
simpl. autounfold in *. rewrite Heqvttbr. rewrite pgd_same. rewrite pmd_same. rewrite pte_same.
repeat rewrite ZMap.gss. right. split. assumption. right. split. apply or3nz. reflexivity.
autounfold; assumption. autounfold; split; assumption.
rewrite (ZMap.gso _ _ Heqaddr) in Hhpt.
rewrite <- Heqvttbr in Hhpt. apply Hrelate in Hhpt. destruct Hhpt; autounfold in *.
constructor. assumption. simpl. autounfold. rewrite Heqvttbr. repeat rewrite ZMap.gss.
destruct (stage2_pgd_index addr0 =? stage2_pgd_index addr) eqn:pgd_same; bool_rel.
rewrite pgd_same; repeat rewrite ZMap.gss. right. split. assumption.
destruct (pmd_index addr0 =? pmd_index addr) eqn:pmd_same; bool_rel.
rewrite pmd_same; repeat rewrite ZMap.gss. right. split. apply or3nz.
destruct (pte_index addr0 =? pte_index addr) eqn:pte_same; bool_rel.
assert(addr0 / 4096 = addr / 4096).
apply pte_same_cond; try split_and; try assumption. autounfold; split; assumption. contra.
destruct Hpte. destruct H. rewrite H0.
assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
right; assumption. rewrite (ZMap.gso _ _ Hneq). apply Hpmd_next.
rewrite phys_or; try assumption.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega. omega. destruct H. destruct H0.
destruct H0. rewrite H1. assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
right; assumption. rewrite (ZMap.gso _ _ Hneq). rewrite phys_or; try assumption.
apply Hpmd_next.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega. omega.
destruct H0; rewrite Heqvttbr, pgd_same, pmd_same in H0; contra.
assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
right; assumption. rewrite (ZMap.gso _ _ Hneq).
destruct Hpte. destruct H; rewrite Heqvttbr, pgd_same in H; contra.
destruct H as (T0 & T). rewrite <- Heqvttbr, <- pgd_same.
destruct T as [T|T]. left; assumption. right. destruct T as (T1 & T).
split. assumption. assert_gso. rewrite phys_or; try assumption.
apply pgd_pool_ne_pmd_next. assumption. autounfold; somega. autounfold; somega.
rewrite (ZMap.gso _ _ Hneq0). assumption.
rewrite <- Heqvttbr. destruct Hpte as [T|T]. left; assumption. right.
destruct T as (T8 & T). split. assumption.
assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed. left.
apply pgd_index_diff_res_diff; auto. autounfold; rewrite Heqvttbr; assumption.
rewrite (ZMap.gso _ _ Hneq). destruct T as [T|T]. left; assumption. right.
destruct T as (T2 & T). split. assumption.
assert_gso. rewrite phys_or; try assumption.
apply pgd_pool_ne_pmd_next. assumption. autounfold; somega. autounfold; somega.
rewrite (ZMap.gso _ _ Hneq0). assumption. assumption.
autounfold in *. rewrite (ZMap.gso _ _ Heqvttbr) in Hhpt.
apply Hrelate in Hhpt. destruct Hhpt; autounfold in *.
constructor. assumption. autounfold. simpl.
destruct Hpte as [T|T]. left; assumption. right.
destruct T as (T0 & T). split. assumption.
assert_gso. apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed. left.
apply pgd_index_diff_res_diff; auto.
rewrite (ZMap.gso _ _ Hneq). destruct T as [T|T]. left; assumption. right.
destruct T as (T2 & T). split. assumption.
assert_gso. rewrite phys_or; try assumption.
apply pgd_pool_ne_pmd_next. assumption. autounfold; somega. autounfold; somega.
rewrite (ZMap.gso _ _ Hneq0). assumption. assumption.
}
rewrite andb_comm in Hspec; simpl in Hspec; inv Hspec.
eexists; split. reflexivity. constructor; try assumption. simpl. omega. simpl. reflexivity. simpl. intro T; inversion T.
bool_rel.
assert((pmd_index addr) @ ((stage2_pgd_index addr) @ ((65536 + (16 * index + cbndx) * 4096 * 2) @ (spt_pmd_t hspt))) = true).
apply Hpmd_t. assumption. split; assumption. contra.
Qed.
Lemma set_smmu_pt_spec_pte_exists:
forall habd habd' labd cbndx index addr pte f
(Hspec: set_smmu_pt_spec cbndx index addr pte habd = Some habd')
(Hhalt: halt (shared habd) = false)
(Hpgd: match addr with VZ64 addr => (stage2_pgd_index addr) @ ((SMMU_TTBR index cbndx) @ (spt_pgd_t (spts (shared habd)))) = true end)
(Hpmd: match addr with VZ64 addr => (pmd_index addr) @ ((stage2_pgd_index addr) @ ((SMMU_TTBR index cbndx) @ (spt_pmd_t (spts (shared habd))))) = true end)
(Hrel: relate_RData f habd labd),
exists labd', set_smmu_pt_spec0 cbndx index addr pte labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros.
assert(range3: 0 <= 3 < 4096) by omega.
pose proof phys_page_or_not_change as phys_or.
assert(Hhaltl: halt (shared labd) = false).
{ destruct Hrel. srewrite. reflexivity. }
hsimpl_func Hspec.
rename z into addr. rename z0 into pte.
remember (spts (shared habd)) as hspt in *; symmetry in Heqhspt.
remember (spts (shared labd)) as lspt in *; symmetry in Heqlspt.
destruct Hrel. rewrite Hhaltl, Heqhspt, Heqlspt in id_spts0.
clear_hyp; simpl_local. destruct Hlocal.
unfold local_spt_map in C9. rename C9 into Hspec.
rewrite Hpgd, Hpmd in Hspec. simpl_hyp Hspec; contra.
duplicate Hvalid. destruct D.
unfold set_smmu_pt_spec0.
repeat autounfold in *.
autounfold. repeat (srewrite; simpl). bool_rel_all; clear_hyp.
assert(Hlock: 2 @ (lock labd) = LockOwn true). srewrite. reflexivity.
assert(Htstate: (tstate labd =? 0) = true). srewrite. reflexivity.
extract_if. apply andb_true_iff; split; bool_rel; somega. rewrite Cond.
pose proof (vttbr_val cbndx index) as Hvttbr. autounfold in Hvttbr.
assert(vttbr_align: phys_page (SMMU_TTBR index cbndx) = SMMU_TTBR index cbndx).
{ autounfold. rewrite <- Hvttbr. rewrite phys_page_fixed. reflexivity. omega. omega. }
autounfold in vttbr_align. rewrite vttbr_align.
extract_if. unfold stage2_pgd_index.
match goal with |- context [Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 8192) end.
autounfold; apply or_index_range_8192; somega. apply andb_true_iff; split; bool_rel; omega. rewrite Cond0.
extract_if. apply Hvttbr_pool_range. rewrite Cond1.
rewrite andb_comm. simpl. destruct_if.
bool_rel. apply Hpgd_t in Hpgd. inversion Hpgd. assumption. assumption.
rewrite Hvttbr_pool_range. rewrite Hhaltl, Hlock. rewrite Case.
extract_if. match goal with |- context[?a @ (spt_vttbr_pool _)] => pose proof (Hvttbr_pool a) end.
destruct H. rewrite H in Case. inversion Case. destruct H. clear H0.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega.
bool_rel_all; apply andb_true_iff; split; bool_rel. omega.
match type of H0 with _ <= _ < ?a => assert(a <= spt_pgd_next lspt) end.
eapply phys_page_lt_4096. apply phys_page_fixed. assumption. destruct H; assumption. omega. rewrite Cond2.
rewrite Heqlspt. rewrite Hpgd_pool_range. rewrite andb_comm. simpl. destruct_if.
apply Hpmd_t in Hpmd. destruct Hpmd. bool_rel; contra. assumption.
rewrite Hpgd_pool_range. rewrite Hhaltl, Hlock, Htstate.
extract_if. match goal with |- context[?a @ (spt_pgd_pool _)] => pose proof (Hpgd_pool a) end.
destruct H. rewrite H in Case0. inversion Case0. destruct H. clear H0.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega.
bool_rel_all; apply andb_true_iff; split; bool_rel. omega.
match type of H0 with _ <= _ < ?a => assert(a <= spt_pmd_next lspt) end.
eapply phys_page_lt_4096. apply phys_page_fixed. assumption. destruct H; assumption. omega. rewrite Cond3.
replace (spt_pgd_next lspt <=? 2162688) with true in Hspec by (symmetry; bool_rel; omega).
replace (spt_pmd_next lspt <=? 3211264) with true in Hspec by (symmetry; bool_rel; omega).
inv Hspec. eexists; split. reflexivity. constructor; try assumption.
simpl. reflexivity. simpl. rewrite Hhaltl. reflexivity. simpl. intro T; clear T.
{
bool_rel_all. constructor; simpl.
- constructor; simpl; autounfold; intros.
+ apply Hvttbr_pool_range.
+ apply Hpgd_pool_range.
+ destruct_zmap. apply andb_true_iff; split; bool_rel; somega.
apply Hpmd_pool_range.
+ omega. + omega.
+ assumption. + assumption.
+ apply Hpgd_next. assumption.
+ assert_gso. match goal with |- context[?a @ (spt_pgd_pool _)] => pose proof (Hpgd_pool a) end.
destruct H0. rewrite H0. replace (phys_page 0) with 0 by reflexivity.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. reflexivity. autounfold; somega. omega.
destruct H0. match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. autounfold; somega.
match type of H2 with _ <= _ < ?a => assert(a <= spt_pmd_next (spts (shared labd))) end.
eapply phys_page_lt_4096. apply phys_page_fixed. assumption. omega. omega.
rewrite (ZMap.gso _ _ Hneq). apply Hpmd_next. omega.
+ apply Hvttbr_pool.
+ apply Hpgd_pool.
- reflexivity. - reflexivity.
- intros; autounfold.
match goal with |- ?c = true <-> _ =>
assert(c = ((stage2_pgd_index addr0) @ ((SMMU_TTBR index0 cbndx0) @ (spt_pgd_t (spts (shared habd)))))) end.
destruct (SMMU_TTBR index0 cbndx0 =? SMMU_TTBR index cbndx) eqn:Httbr_same; bool_rel; autounfold in Httbr_same.
rewrite Httbr_same. rewrite ZMap.gss.
destruct (stage2_pgd_index addr0 =? stage2_pgd_index addr) eqn:Hpgd_same; bool_rel.
rewrite Hpgd_same. rewrite ZMap.gss. autounfold; rewrite Httbr_same; rewrite Hpgd. reflexivity.
rewrite (ZMap.gso _ _ Hpgd_same). autounfold; rewrite Httbr_same; reflexivity.
rewrite (ZMap.gso _ _ Httbr_same). reflexivity.
rewrite H. apply Hpgd_t. assumption.
- intros; autounfold.
match goal with |- ?c = true <-> _ =>
assert(c = (pmd_index addr0) @ ((stage2_pgd_index addr0) @ ((SMMU_TTBR index0 cbndx0) @ (spt_pmd_t (spts (shared habd)))))) end.
destruct (SMMU_TTBR index0 cbndx0 =? SMMU_TTBR index cbndx) eqn:Httbr_same; bool_rel; autounfold in Httbr_same.
rewrite Httbr_same. rewrite ZMap.gss.
destruct (stage2_pgd_index addr0 =? stage2_pgd_index addr) eqn:Hpgd_same; bool_rel.
rewrite Hpgd_same. rewrite ZMap.gss.
destruct (pmd_index addr0 =? pmd_index addr) eqn:Hpmd_same; bool_rel.
rewrite Hpmd_same. rewrite ZMap.gss.
autounfold; rewrite Httbr_same; rewrite Hpmd. reflexivity.
rewrite (ZMap.gso _ _ Hpmd_same). rewrite <- Httbr_same; reflexivity.
rewrite (ZMap.gso _ _ Hpgd_same). autounfold; rewrite Httbr_same; reflexivity.
rewrite (ZMap.gso _ _ Httbr_same). reflexivity.
rewrite H. apply Hpmd_t. assumption.
- intros. repeat autounfold in *.
destruct (SMMU_TTBR index0 cbndx0 =? SMMU_TTBR index cbndx) eqn:Heqvttbr; bool_rel.
autounfold in Heqvttbr. rewrite Heqvttbr in *; rewrite ZMap.gss in Hhpt.
destruct (addr0 / 4096 =? addr / 4096) eqn:Heqaddr; bool_rel.
rewrite Heqaddr in Hhpt. rewrite ZMap.gss in Hhpt. inv Hhpt. apply pte_same_cond in Heqaddr.
destruct Heqaddr as (pgd_same & pmd_same & pte_same).
constructor. reflexivity.
simpl. autounfold in *. rewrite Heqvttbr. rewrite pgd_same. rewrite pmd_same. rewrite pte_same.
repeat rewrite ZMap.gss. right. split. assumption. right. split. assumption. reflexivity.
autounfold; assumption. autounfold; split; assumption.
rewrite (ZMap.gso _ _ Heqaddr) in Hhpt.
rewrite <- Heqvttbr in Hhpt. apply Hrelate in Hhpt. destruct Hhpt; autounfold in *.
constructor. assumption. simpl. autounfold. rewrite Heqvttbr. repeat rewrite ZMap.gss.
rewrite <- Heqvttbr.
destruct Hpte as [T|T]. left; assumption. right. destruct T as (T1 & T). split. assumption.
destruct T as [T|T]. left; assumption. right. destruct T as (T2 & T). split. assumption.
destruct_zmap. match type of Heq with ?a = ?b => assert(a <> b) end.
destruct (stage2_pgd_index addr0 =? stage2_pgd_index addr) eqn:pgd_same; bool_rel.
destruct (pmd_index addr0 =? pmd_index addr) eqn:pmd_same; bool_rel.
destruct (pte_index addr0 =? pte_index addr) eqn:pte_same; bool_rel.
assert(addr0 / 4096 = addr / 4096).
apply pte_same_cond; try split_and; try assumption. autounfold; split; assumption. contra.
apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed. right; assumption.
apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
left; apply pmd_index_diff_res_diff; auto. autounfold; rewrite Heqvttbr; assumption.
autounfold; rewrite Heqvttbr; assumption.
apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
left; apply pmd_index_diff_res_diff; auto. autounfold; rewrite Heqvttbr; assumption.
autounfold; rewrite Heqvttbr; assumption. contra. assumption. assumption.
autounfold in *. rewrite (ZMap.gso _ _ Heqvttbr) in Hhpt.
apply Hrelate in Hhpt. destruct Hhpt; autounfold in *.
constructor. assumption. autounfold. simpl.
destruct Hpte as [T|T]. left; assumption. right. destruct T as (T1 & T). split. assumption.
destruct T as [T|T]. left; assumption. right. destruct T as (T2 & T). split. assumption.
destruct_zmap. match type of Heq with ?a = ?b => assert(a <> b) end.
apply or_index_ne_cond. apply phys_page_fixed. apply phys_page_fixed.
left; apply pmd_index_diff_res_diff; auto. contra. assumption. assumption.
}
Qed.
Lemma set_smmu_pt_spec_exists:
forall habd habd' labd cbndx index addr pte f
(Hspec: set_smmu_pt_spec cbndx index addr pte habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', set_smmu_pt_spec cbndx index addr pte labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros. duplicate Hspec. unfold_spec D; autounfold in D; repeat simpl_hyp D; contra.
assert(halt (shared labd) = true) by (destruct Hrel; srewrite; reflexivity).
assert(tstate labd =? 0 = true) by (destruct Hrel; srewrite; assumption).
unfold set_smmu_pt_spec0; repeat autounfold. repeat srewrite. simpl. inv D.
destruct_if. eexists; split. reflexivity. assumption.
eexists; split. reflexivity. rewrite <- H.
assert (labd {shared : (shared labd) {halt : halt (shared labd)}} = labd).
destruct labd. simpl. destruct shared. simpl. reflexivity.
rewrite H1; assumption.
bool_rel_all. subst. inversion Hcond6.
destruct ((pgd_index z) @ (pgd_t (vmid @ (npts (shared habd))))) eqn:Hpgd.
destruct ((pud_index z) @ ((pgd_index z) @ (pud_t (vmid @ (npts (shared habd)))))) eqn:Hpud.
eapply set_smmu_pt_spec_1_pmd_exists; eassumption.
eapply set_smmu_pt_spec_1_pud_exists; eassumption.
eapply set_smmu_pt_spec_1_pgd_exists; eassumption.
Qed.
Lemma set_smmu_pt_spec_ref:
compatsim (crel RData RData) (gensem set_smmu_pt_spec) set_smmu_pt_spec_low.
Proof.
Opaque set_smmu_pt_spec.
compatsim_simpl (@match_RData).
exploit set_smmu_pt_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma clear_smmu_pt_spec_exists:
forall habd habd' labd cbndx index f
(Hspec: clear_smmu_pt_spec cbndx index habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', clear_smmu_pt_spec cbndx index labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros until f.
solve_refine_proof clear_smmu_pt0; repeat hstep; try htrivial.
Qed.
Lemma clear_smmu_pt_spec_ref:
compatsim (crel RData RData) (gensem clear_smmu_pt_spec) clear_smmu_pt_spec_low.
Proof.
Opaque clear_smmu_pt_spec.
compatsim_simpl (@match_RData).
exploit clear_smmu_pt_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma walk_smmu_pt_spec_exists:
forall habd labd cbndx index addr res f
(Hspec: walk_smmu_pt_spec cbndx index addr habd = Some (VZ64 res))
(Hrel: relate_RData f habd labd),
walk_smmu_pt_spec cbndx index addr labd = Some (VZ64 res).
Proof.
intros. unfold_spec Hspec; autounfold in Hspec.
simpl_hyp Hspec. simpl_hyp Hspec. simpl_hyp Hspec. simpl_hyp Hspec.
destruct Hrel. unfold get_npt_level_spec0; repeat autounfold; srewrite; simpl.
Local Transparent Z.land. simpl. reflexivity. Local Opaque Z.land.
pose proof phys_page_or_not_change as phys_or.
rename C2 into Hhalt.
assert (Hrelate: forall i : Z, relate_npt i i @ (npts (shared habd)) i @ (npts (shared labd))).
{ destruct Hrel. rewrite id_halt0 in Hhalt. rewrite Hhalt in id_npts0.
clear_hyp; simpl_local. assumption. }
assert(Hhaltl: halt (shared labd) = false).
{ destruct Hrel. srewrite. reflexivity. }
pose proof (Hrelate vmid).
remember (vmid @ (npts (shared habd))) as hnpt in *; symmetry in Heqhnpt.
remember (vmid @ (npts (shared labd))) as lnpt in *; symmetry in Heqlnpt.
destruct H; simpl in *.
simpl_hyp Hspec; contra. destruct b; contra.
assert(Hlock: (4 + vmid) @ (lock labd) = LockOwn true).
{ destruct Hrel. srewrite. reflexivity. }
simpl_hyp Hspec. simpl_hyp Hspec.
exploit (Hrelate0 z z1 z2 z0). autounfold; bool_rel_all; omega.
assumption. intro T; destruct T.
duplicate Hvalid. destruct D.
destruct Hlevel as [Hlevel|Hlevel]; [|destruct Hlevel as [Hlevel|Hlevel]].
rewrite Hlevel in Hspec. duplicate Hlevel. duplicate Hlevel. duplicate Hlevel.
apply Hlevel0 in D. apply Hpfn0 in D0. apply Hpte0 in D1.
clear Hlevel0 Hlevel1 Hlevel3.
repeat autounfold in *; simpl in *; srewrite.
clear_hyp. bool_rel_all.
extract_if. clear D. apply andb_true_iff; split; bool_rel; somega. rewrite Cond.
pose proof (vttbr_val vmid) as Hvttbr. autounfold in Hvttbr.
assert(vttbr_align: phys_page (pool_start vmid) = pool_start vmid).
{ autounfold. rewrite <- Hvttbr. rewrite phys_page_fixed. reflexivity. omega. }
autounfold in vttbr_align. rewrite Hvttbr; try omega.
extract_if. clear D. unfold pgd_index.
exploit (or_index_range (65536 + 33554432 * vmid) (Z.shiftr addr0 PGDIR_SHIFT)); try assumption; try omega.
autounfold; somega. intro range. apply andb_true_iff; split; bool_rel; omega. rewrite Cond0.
rewrite Hvttbr_pool_range.
rewrite andb_comm. simpl. rewrite Hvttbr_pool_range.
destruct D. rewrite H. simpl.
Local Transparent Z.land. simpl. Local Opaque Z.land.
simpl_hyp Hspec; assumption.
destruct H as (Hvt & D). destruct_if. bool_rel; contra.
extract_if. clear D. match goal with |- context[?a @ (pt_vttbr_pool _)] => pose proof (Hvttbr_pool a) end.
destruct H. rewrite H in Case. inversion Case. destruct H. clear H0.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. apply phys_page_fixed. autounfold; somega.
bool_rel_all; apply andb_true_iff; split; bool_rel. omega.
match type of H0 with _ <= _ < ?a => assert(a <= pt_pgd_next vmid @ (npts (shared labd))) end.
eapply phys_page_lt_4096. apply phys_page_fixed. srewrite; assumption.
destruct H; srewrite; assumption. srewrite; omega. rewrite Cond1.
rewrite Hpgd_pool_range. rewrite andb_comm. simpl.
rewrite Hpgd_pool_range. destruct D. rewrite H. simpl.
Local Transparent Z.land. simpl. Local Opaque Z.land.
simpl_hyp Hspec; assumption.
destruct H as (Hpg & D). destruct_if. bool_rel; contra.
extract_if. clear D. match goal with |- context[?a @ (pt_pgd_pool _)] => pose proof (Hpgd_pool a) end.
destruct H. rewrite H in Case0. inversion Case0. destruct H. clear H0.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. apply phys_page_fixed. autounfold; somega.
bool_rel_all; apply andb_true_iff; split; bool_rel. omega.
match type of H0 with _ <= _ < ?a => assert(a <= pt_pud_next lnpt) end.
eapply phys_page_lt_4096. apply phys_page_fixed. assumption. destruct H; assumption. omega. rewrite Cond2.
rewrite Hpud_pool_range. rewrite andb_comm. simpl. rewrite Hpud_pool_range.
destruct D. rewrite H. Local Transparent Z.land. simpl. Local Opaque Z.land.
simpl_hyp Hspec; assumption.
destruct H as (D2 & D3 & D4). srewrite. simpl.
destruct_if. bool_rel. rewrite Case1 in D3. inversion D3.
extract_if. match goal with |- context[?a @ (pt_pud_pool _)] => pose proof (Hpud_pool a) end.
destruct H. rewrite H in Case1. inversion Case1. destruct H. bool_rel; contra. destruct H as (? & ? & ?).
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. apply phys_page_fixed. autounfold; somega.
bool_rel_all; apply andb_true_iff; split; bool_rel. omega.
match type of H2 with _ <= _ < ?a => assert(a <= pt_pmd_next lnpt) end.
eapply phys_page_lt_4096. apply phys_page_fixed. assumption. destruct H0; assumption. omega. rewrite Cond3.
Local Transparent Z.land. simpl. Local Opaque Z.land.
simpl_hyp Hspec; assumption.
rewrite Hlevel in Hspec. apply Hlevel1 in Hlevel.
destruct Hlevel as (D1 & D2 & D3 & D4). clear Hlevel0 Hlevel1 Hlevel3 Hpfn0 Hpfn2.
repeat autounfold in *; simpl in *; srewrite.
clear_hyp. bool_rel_all.
extract_if. apply andb_true_iff; split; bool_rel; somega. rewrite Cond.
pose proof (vttbr_val vmid) as Hvttbr. autounfold in Hvttbr.
assert(vttbr_align: phys_page (pool_start vmid) = pool_start vmid).
{ autounfold. rewrite <- Hvttbr. rewrite phys_page_fixed. reflexivity. omega. }
autounfold in vttbr_align. rewrite Hvttbr; try omega.
extract_if. unfold pgd_index.
exploit (or_index_range (65536 + 33554432 * vmid) (Z.shiftr addr0 PGDIR_SHIFT)); try assumption; try omega.
autounfold; somega. intro range. apply andb_true_iff; split; bool_rel; omega. rewrite Cond0.
rewrite Hvttbr_pool_range.
rewrite andb_comm. simpl. rewrite Hvttbr_pool_range.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. apply phys_page_fixed. autounfold; somega.
bool_rel_all; apply andb_true_iff; split; bool_rel. omega.
match type of H0 with _ <= _ < ?a => assert(a <= pt_pud_next lnpt) end.
eapply phys_page_lt_4096. apply phys_page_fixed. assumption. destruct H; assumption. omega. rewrite Cond2.
rewrite Hpud_pool_range. rewrite andb_comm. simpl. rewrite Hpud_pool_range.
destruct_if. bool_rel; srewrite; contra. rewrite D3; assumption.
rewrite Hlevel in Hspec. apply Hlevel3 in Hlevel.
destruct Hlevel as (D1 & D2 & D3 & D4 & D5). simpl in D5.
clear Hlevel0 Hlevel1 Hlevel3 Hpfn0 Hpfn2 Hpte0 Hpfn3.
repeat autounfold in *; simpl in *; srewrite.
clear_hyp. bool_rel_all.
extract_if. apply andb_true_iff; split; bool_rel; somega. rewrite Cond.
pose proof (vttbr_val vmid) as Hvttbr. autounfold in Hvttbr.
assert(vttbr_align: phys_page (pool_start vmid) = pool_start vmid).
{ autounfold. rewrite <- Hvttbr. rewrite phys_page_fixed. reflexivity. omega. }
autounfold in vttbr_align. rewrite Hvttbr; try omega.
extract_if. unfold pgd_index.
exploit (or_index_range (65536 + 33554432 * vmid) (Z.shiftr addr0 PGDIR_SHIFT)); try assumption; try omega.
autounfold; somega. intro range. apply andb_true_iff; split; bool_rel; omega. rewrite Cond0.
rewrite Hvttbr_pool_range.
rewrite andb_comm. simpl. rewrite Hvttbr_pool_range.
destruct_if. bool_rel; contra.
extract_if. match goal with |- context[?a @ (pt_vttbr_pool _)] => pose proof (Hvttbr_pool a) end.
destruct H. rewrite H in Case. inversion Case. destruct H. clear H0.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. apply phys_page_fixed. autounfold; somega.
bool_rel_all; apply andb_true_iff; split; bool_rel. omega.
match type of H0 with _ <= _ < ?a => assert(a <= pt_pgd_next vmid @ (npts (shared labd))) end.
eapply phys_page_lt_4096. apply phys_page_fixed. srewrite; assumption.
destruct H; srewrite; assumption. srewrite; omega. rewrite Cond1.
rewrite Hpgd_pool_range. rewrite andb_comm. simpl.
rewrite Hpgd_pool_range. destruct_if. bool_rel; contra.
extract_if. match goal with |- context[?a @ (pt_pgd_pool _)] => pose proof (Hpgd_pool a) end.
destruct H. rewrite H in Case0. inversion Case0. destruct H. clear H0.
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. apply phys_page_fixed. autounfold; somega.
bool_rel_all; apply andb_true_iff; split; bool_rel. omega.
match type of H0 with _ <= _ < ?a => assert(a <= pt_pud_next lnpt) end.
eapply phys_page_lt_4096. apply phys_page_fixed. assumption. destruct H; assumption. omega. rewrite Cond2.
rewrite Hpud_pool_range. rewrite andb_comm. simpl. rewrite Hpud_pool_range.
srewrite. simpl. destruct_if. bool_rel; contra.
extract_if. match goal with |- context[?a @ (pt_pud_pool _)] => pose proof (Hpud_pool a) end.
destruct H. rewrite H in Case1. inversion Case1. destruct H. bool_rel; contra. destruct H as (? & ? & ?).
match goal with |- context[Z.lor ?a ?b] => assert(a <= Z.lor a b < a + 4096) end.
apply or_index_range. omega. apply phys_page_fixed. autounfold; somega.
bool_rel_all; apply andb_true_iff; split; bool_rel. omega.
match type of H2 with _ <= _ < ?a => assert(a <= pt_pmd_next lnpt) end.
eapply phys_page_lt_4096. apply phys_page_fixed. assumption. destruct H0; assumption. omega. rewrite Cond3.
rewrite Hpmd_pool_range. rewrite Hpmd_pool_range. rewrite D5; assumption.
Qed.
Lemma walk_smmu_pt_spec_ref:
compatsim (crel RData RData) (gensem walk_smmu_pt_spec) walk_smmu_pt_spec_low.
Proof.
Opaque walk_smmu_pt_spec.
compatsim_simpl (@match_RData).
exploit walk_smmu_pt_spec_exists; eauto 1;
refine_split; repeat (try econstructor; eauto).
Qed.
End FreshPrim.
Section PassthroughPrim.
Lemma passthrough_correct:
sim (crel HDATA LDATA) MmioSPTWalk_passthrough MmioPTWalk.
Proof.
sim_oplus; layer_sim_simpl; compatsim_simpl (@match_AbData);
match_external_states_simpl; destruct match_related; srewrite; try reflexivity.
- unfold host_dabt_is_write_spec; srewrite; reflexivity.
- unfold host_get_fault_ipa_spec; srewrite; reflexivity.
- unfold set_vm_remap_addr_spec; srewrite; reflexivity.
- unfold host_dabt_get_rd_spec; srewrite; reflexivity.
- unfold clear_phys_page_spec; srewrite; reflexivity.
- unfold get_mem_region_cnt_spec; srewrite; reflexivity.
- unfold get_exception_vector_spec; srewrite; reflexivity.
- unfold read_hpfar_el2_spec; srewrite; reflexivity.
- unfold read_actlr_el1_spec; srewrite; reflexivity.
- unfold host_dabt_get_as_spec; srewrite; reflexivity.
- unfold read_esr_el2_spec; srewrite; reflexivity.
- unfold set_vm_kvm_spec; srewrite; reflexivity.
- unfold set_vm_mapped_pages_spec; srewrite; reflexivity.
- unfold readl_relaxed_spec; srewrite; reflexivity.
- unfold set_shadow_dirty_bit_spec; srewrite; reflexivity.
- unfold set_vm_load_size_spec; srewrite; reflexivity.
- unfold host_skip_instr_spec; srewrite; reflexivity.
- unfold set_vm_load_addr_spec; srewrite; reflexivity.
- unfold set_vm_vcpu_spec; srewrite; reflexivity.
- unfold readq_relaxed_spec; srewrite; reflexivity.
End.
End PassthroughPrim.
End WITHMEM.
End MmioSPTWalkProofHigh.