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 PageIndex.Layer.
Require Import PageIndex.Spec.
Require Import PageMgmt.Layer.
Require Import HypsecCommLib.
Require Import Constants.
Require Import RData.
Require Import PageMgmt.Spec.
Local Open Scope Z_scope.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.
Section PageMgmtProofHigh.
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 := PageMgmt_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := PageIndex_ops) HDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Definition valid_regions (regions: ZMap.t Memblock) :=
forall i, let reg := (ZMap.get i regions) in
is_addr (base reg) = true /\ is_int64 (size reg) = true /\ is_addr (base reg + size reg) = true /\
((is_s2page (index reg) = true /\ is_s2page (index reg + size reg / PAGE_SIZE) = true) \/ index reg = INVALID64).
Lemma mem_region_succ:
forall addr adt (Hvalid: valid_regions (regions adt)) (Hcnt: is_memblock (region_cnt adt) = true),
exists i' res, region_search_loop (Z.to_nat (region_cnt adt)) addr 0 INVALID (regions adt) = Some (i', res) /\
is_memblock i' = true /\ (res = INVALID \/ (is_memblock res = true /\
addr >= base (ZMap.get res (regions adt)) /\
addr < base (ZMap.get res (regions adt)) +
size (ZMap.get res (regions adt)))).
Proof.
intros. unfold valid_regions in Hvalid.
assert(forall n, Z.of_nat n <= (region_cnt adt) ->
exists i' res, region_search_loop n addr 0 INVALID (regions adt) = Some (i', res) /\
(0 <=? i') = true /\ i' = Z.of_nat n /\ (res = INVALID \/
(is_memblock res = true /\
addr >= base (ZMap.get res (regions adt)) /\
addr < base (ZMap.get res (regions adt)) +
size (ZMap.get res (regions adt))))).
{ autounfold. induction n. simpl. intros.
eexists. eexists. split_and. reflexivity. auto.
omega. left. reflexivity.
intros. rewrite Nat2Z.inj_succ, succ_plus_1 in *. simpl.
assert (Z.of_nat n <= region_cnt adt) by omega.
apply IHn in H0. destruct H0 as (i0 & res0 & spec0 & Hi0 & Hi0' & Hres0).
rewrite spec0. autounfold. rewrite Hi0.
assert(i0 <? 32 = true).
{ rewrite Hi0'. autounfold in *. destruct_con. bool_rel. omega. }
rewrite H0. simpl.
assert((0 <=? res0) && (res0 <=? 4294967295) = true).
{ destruct Hres0. rewrite H1. auto.
destruct H1. destruct_con. simpl. bool_rel. omega. }
rewrite H1. pose proof (Hvalid i0). destruct H2 as (Hb & Hs & Hbs & Hidx).
autounfold in *. rewrite Hb, Hs, Hbs.
destruct ((base (ZMap.get i0 (regions adt)) <=? addr) &&
(addr <? base (ZMap.get i0 (regions adt)) + size (ZMap.get i0 (regions adt)))) eqn:Haddr.
eexists. eexists. split_and. reflexivity. bool_rel. omega. omega.
right. rewrite Hi0, H0.
destruct_con; bool_rel.
split_and. reflexivity. omega. omega.
eexists. eexists. split_and. reflexivity. bool_rel. omega. omega.
assumption. }
assert(Z.of_nat (Z.to_nat (region_cnt adt)) <= region_cnt adt).
{ rewrite Z2Nat.id. reflexivity. autounfold in Hcnt. destruct_con. bool_rel. assumption. }
pose proof (H _ H0).
destruct H1 as (i0 & res0 & spec0 & Hi0 & Hi0' & Hres0).
exists i0, res0. split_and; try assumption.
bool_rel. rewrite Z2Nat.id in Hi0'. rewrite Hi0'. assumption.
autounfold in *. destruct_con. bool_rel. assumption.
Qed.
Lemma page_index_succ:
forall addr adt (Haddr: is_addr addr = true) (Hvalid: valid_regions (regions adt)) (Hcnt: is_memblock (region_cnt adt) = true),
exists idx , get_s2_page_index_spec (VZ64 addr) adt = Some (VZ64 idx) /\ (idx = INVALID64 \/ is_s2page idx = true).
Proof.
intros. unfold valid_regions in Hvalid. simpl. rewrite Hcnt. simpl. autounfold.
assert((0 <=? addr) && (addr <? 2199023255552) = true).
{ autounfold in Haddr. assumption. }
{
rewrite H.
{
exploit mem_region_succ. eauto 1; intros (labd' & Hspec & Hrel). rewrite Hcnt. reflexivity. intros.
destruct H0 as (i' & res & Hsr & Him & Hrest). rewrite Hsr.
assert((0 <=? i') && (i' <? 32) = true).
{ unfold is_memblock in Him. destruct Him. autounfold. reflexivity. }
rewrite H0.
assert(((0 <=? res) && (res <=? 4294967295)) = true).
{
unfold INVALID, is_memblock in Hrest. unfold MAX_MEMBLOCK_NUM in Hrest.
destruct Hrest as [Hrest1 | Hrest2 _].
{ rewrite Hrest1. reflexivity. }
{ destruct Hrest2. rewrite andb_true_iff in H1.
destruct H1 as [H1' H1'']. rewrite H1'.
assert(res <= 4294967295). bool_rel. omega. simpl. bool_rel. rewrite H1.
reflexivity. }
}
rewrite H1. unfold INVALID in Hrest.
destruct (res =? 4294967295) eqn:Inv. split_and.
{ eexists. split_and. reflexivity. left. reflexivity. }
destruct Hrest. bool_rel. contradiction.
assert((0<=?res) && (res <? 32) = true).
{ destruct H2 as (H2'). unfold is_memblock in H2'. unfold MAX_MEMBLOCK_NUM in H2'. rewrite H2'. reflexivity. }
rewrite H3. pose proof (Hvalid res).
destruct H4 as (Hb & Hs & Hbs & Hidx). unfold is_addr in Hb. unfold KVM_ADDR_SPACE in Hb. rewrite Hb.
unfold is_s2page, PAGE_SIZE, INVALID64 in Hidx. unfold MAX_S2PAGE_NUM in Hidx.
destruct Hidx. destruct H4. rewrite andb_true_iff in H4. destruct H4. rewrite H4.
assert((index (ZMap.get res (regions adt)) <=? 18446744073709551615 = true)). bool_rel. omega.
rewrite H7. simpl.
destruct (index (ZMap.get res (regions adt)) =? 18446744073709551615).
{ eexists. split_and. reflexivity. left. reflexivity. }
{
assert(index (ZMap.get res (regions adt)) <? 2199023255552 = true). Print get_s2_page_index_spec.
{ pose proof (Hvalid res).
repeat match goal with | [H: _ /\ _ |- _] => destruct H end.
bool_rel. omega. }
{
rewrite H8. destruct H2 as (Ht & Hbr & Hbrs).
assert( addr >=? base (ZMap.get res (regions adt)) = true).
{ bool_rel. omega. }
{
rewrite H2.
eexists. rewrite andb_true_iff in H5. split_and. trivial.
right.
assert((0 <=? index (ZMap.get res (regions adt)) + (addr - base (ZMap.get res (regions adt))) / 4096)
&&(index (ZMap.get res (regions adt)) + (addr - base (ZMap.get res (regions adt))) / 4096 <? 16777216) = true).
{ apply andb_true_iff. split.
repeat match goal with
| [H:_ && _ = true |- _] => apply andb_true_iff in H; destruct H
end.
bool_rel.
assert((addr - base (ZMap.get res (regions adt))) <= size (ZMap.get res (regions adt))) by omega.
assert(0 <= (addr - base (ZMap.get res (regions adt))) / 4096).
{ apply Z_div_pos. omega. omega. }
omega.
repeat match goal with
| [H:_ && _ = true |- _] => apply andb_true_iff in H; destruct H
end.
bool_rel.
assert((addr - base (ZMap.get res (regions adt))) <= size (ZMap.get res (regions adt))) by omega.
assert((addr - base (ZMap.get res (regions adt))) / 4096 <= size (ZMap.get res (regions adt)) / 4096).
{ apply Z_div_le. omega. omega. }
destruct H5. bool_rel. omega. }
apply H9.
}
}
}
{
rewrite H4. simpl. eexists. split_and. reflexivity. left. reflexivity.
}
}
}
Qed.
Definition valid_regions2 (regions: ZMap.t Memblock) :=
forall i j (Hne: i > j) ,
let reg1 := (ZMap.get i regions) in
let reg2 := (ZMap.get j regions) in
base reg1 >= base reg2 + size reg2 /\ index reg1 > index reg2 + size reg2.
Lemma page_index_unique:
forall adt pfn1 pfn2 idx1 idx2
(Hhalt: halt adt = false)
(Hregion: valid_regions (regions adt))
(Hregion2: valid_regions2 (regions adt))
(Hblock: is_memblock (region_cnt adt) = true)
(Hspec1: get_s2_page_index_spec (VZ64 (pfn1 * PAGE_SIZE)) adt = Some (VZ64 idx1))
(Hspec2: get_s2_page_index_spec (VZ64 (pfn2 * PAGE_SIZE)) adt = Some (VZ64 idx2))
(Hidx1: is_s2page idx1 = true) (Hidx2: is_s2page idx2 = true),
idx1 = idx2 -> pfn1 = pfn2.
Proof.
intros. hsimpl_func Hspec1; hsimpl_func Hspec2;
repeat match goal with
| [H: is_s2page 18446744073709551615 = true |- _] =>
autounfold in H; apply andb_true_iff in H; destruct H; bool_rel; omega
| [H1: 18446744073709551615 = ?x, H2: is_s2page ?x = true |- _] => rewrite <- H1 in H2
| _ => idtac
end.
pose proof (mem_region_succ (pfn1 * 4096) adt Hregion Hblock).
destruct H14 as (i' & res & Hreg1 & prop1).
unfold INVALID in Hreg1. rewrite H2 in Hreg1. inv Hreg1.
pose proof (mem_region_succ (pfn2 * 4096) adt Hregion Hblock).
destruct H14 as (i'0 & res0 & Hreg2 & prop2).
unfold INVALID in Hreg2. rewrite H13 in Hreg2. inv Hreg2.
repeat (destruct_con; contra).
repeat match goal with
| [H: is_memblock _ = true /\ (_ = INVALID \/ _) |- _] => destruct H
| [H1: _ = INVALID \/ is_memblock _ = true /\ _ |- _] => destruct H1
| [H2: _ = INVALID |- _] => autounfold in H2; bool_rel; contradiction
| [H3: is_memblock _ = true /\ _ /\ _ |- _] => destruct H3
| _ => idtac
end.
unfold valid_regions2 in Hregion2.
destruct (res0 >? res) eqn:Hrel1.
pose proof (Hregion2 res0 res) as Hr.
bool_rel. destruct Hr. omega.
assert ((pfn1 * 4096 - base (ZMap.get res (regions adt))) < size (ZMap.get res (regions adt))).
omega.
assert((index (ZMap.get res (regions adt)) + (pfn1 * 4096 - base (ZMap.get res (regions adt))) / 4096) <
index (ZMap.get res (regions adt)) + size (ZMap.get res (regions adt))).
apply Zplus_lt_compat_l. omega.
assert((pfn2 * 4096 - base (ZMap.get res0 (regions adt))) / 4096 >= 0).
assert((pfn2 * 4096 - base (ZMap.get res0 (regions adt))) >= 0). omega.
apply (Z_div_ge (pfn2 * 4096 - base (ZMap.get res0 (regions adt))) 0 4096) in H35.
rewrite Zdiv_0_l in H35. omega. reflexivity.
assert( index (ZMap.get res (regions adt)) + (pfn2 * 4096 - base (ZMap.get res (regions adt))) / 4096 <
index (ZMap.get res0 (regions adt)) + (pfn2 * 4096 - base (ZMap.get res0 (regions adt))) / 4096 ) as Hf.
omega. contradict Hf. omega.
destruct (res0 <? res) eqn:Hrel2.
pose proof (Hregion2 res res0) as Hr. destruct Hr. bool_rel. omega.
assert ((pfn2 * 4096 - base (ZMap.get res0 (regions adt))) < size (ZMap.get res0 (regions adt))).
omega.
assert((index (ZMap.get res0 (regions adt)) + (pfn2 * 4096 - base (ZMap.get res0 (regions adt))) / 4096) <
index (ZMap.get res0 (regions adt)) + size (ZMap.get res0 (regions adt))).
apply Zplus_lt_compat_l. omega.
assert((index (ZMap.get res0 (regions adt)) + (pfn2 * 4096 - base (ZMap.get res0 (regions adt))) / 4096) <
(index (ZMap.get res (regions adt)))).
omega.
assert((pfn1 * 4096 - base (ZMap.get res (regions adt))) / 4096 >= 0).
assert((pfn1 * 4096 - base (ZMap.get res (regions adt))) >= 0). omega.
apply (Z_div_ge (pfn1 * 4096 - base (ZMap.get res (regions adt))) 0 4096) in H36.
rewrite Zdiv_0_l in H36. omega. reflexivity.
assert( index (ZMap.get res0 (regions adt)) + (pfn2 * 4096 - base (ZMap.get res0 (regions adt))) / 4096 <
index (ZMap.get res (regions adt)) + (pfn1 * 4096 - base (ZMap.get res (regions adt))) / 4096 ) as Hf.
omega. contradict Hf. omega.
assert (res0 = res). bool_rel. omega.
rewrite H30 in H26.
assert ((pfn2 * 4096 - base (ZMap.get res (regions adt))) / 4096 = (pfn1 * 4096 - base (ZMap.get res (regions adt))) / 4096).
omega.
omega.
Qed.
Inductive relate_s2page (hadt: HDATA) (ladt: LDATA) :=
| RELATE_S2PAGE:
forall (Hs2rel: forall pfn idx (Hidx: get_s2_page_index_spec (VZ64 (pfn * PAGE_SIZE)) ladt = Some (VZ64 idx)),
(idx = INVALID64 <-> owner (ZMap.get pfn (s2page hadt)) = INVALID) /\
(idx = INVALID64 <-> count (ZMap.get pfn (s2page hadt)) = INVALID) /\
(is_s2page idx = true -> ZMap.get pfn (s2page hadt) = ZMap.get idx (s2page ladt))),
relate_s2page hadt ladt.
Record relate_RData (f:meminj) (hadt: HDATA) (ladt: LDATA) :=
mkrelate_RData {
id_halt: halt hadt = halt ladt;
id_icore: (halt hadt = false) -> (icore hadt = icore ladt);
id_ihost: (halt hadt = false) -> (ihost hadt = ihost ladt);
id_curid: (halt hadt = false) -> (curid hadt = curid ladt);
id_cur_vmid: (halt hadt = false) -> (cur_vmid hadt = cur_vmid ladt);
id_cur_vcpuid: (halt hadt = false) -> (cur_vcpuid hadt = cur_vcpuid ladt);
id_regs: (halt hadt = false) -> (regs hadt = regs ladt);
id_flatmem: (halt hadt = false) -> (flatmem hadt = flatmem ladt);
id_log: (halt hadt = false) -> (log hadt = log ladt);
id_oracle: (halt hadt = false) -> (oracle hadt = oracle ladt);
id_lock: (halt hadt = false) -> (lock hadt = lock ladt); id_data_log: (halt hadt = false) -> (data_log hadt = data_log ladt);
id_data_oracle: (halt hadt = false) -> (data_oracle hadt = data_oracle ladt);
id_npts: (halt hadt = false) -> (npts hadt = npts ladt);
region_cnt_rel: is_memblock (region_cnt ladt) = true;
regions_rel: valid_regions (regions ladt) /\ valid_regions2 (regions ladt);
s2page_rel: (halt hadt = false) -> relate_s2page hadt ladt;
id_core_data: (halt hadt = false) -> (core_data hadt = core_data ladt);
id_vminfos: (halt hadt = false) -> (vminfos hadt = vminfos ladt);
id_shadow_ctxts: (halt hadt = false) -> (shadow_ctxts hadt = shadow_ctxts ladt);
id_int_pte: (halt hadt = false) -> (int_pte hadt = int_pte ladt);
id_int_level: (halt hadt = false) -> (int_level hadt = int_level 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.
Lemma get_pfn_owner_spec_exists:
forall habd labd pfn res f
(Hspec: get_pfn_owner_spec (VZ64 pfn) habd = Some res)
(Hrel: relate_RData f habd labd),
get_pfn_owner_spec0 (VZ64 pfn) labd = Some res.
Proof.
intros.
assert(forall p:Prop, (false=false -> p) -> p) as exp_false.
assert(false = false) as AlwaysFalse. reflexivity.
{ intros. apply H in AlwaysFalse. assumption. }
inversion Hrel. destruct regions_rel0 as [Hreg0 Hreg1].
unfold get_pfn_owner_spec0. unfold_spec Hspec. autounfold in region_cnt_rel0. autounfold in Hspec. autounfold.
destruct ((0 <=? pfn) && (pfn <? 2199023255552)) eqn:Haddr0.
destruct ( (0 <=? pfn * 4096) && (pfn * 4096 <? 2199023255552)) eqn:Haddr1.
repeat simpl_hyp Hspec;
repeat match goal with
| [H: false = false -> _ |- _] => apply exp_false in H
| _ => idtac
end;
contra; unfold Spec.check_spec;
pose proof (page_index_succ (pfn * 4096) labd Haddr1 Hreg0 region_cnt_rel0) as Hpis;
destruct Hpis as (idx & Hidx & Hidxv);
rewrite Hidx; autounfold in Hidxv.
assert((0 <=? idx) && (idx <=? 18446744073709551615)=true) as Hidxv'.
{ destruct Hidxv as [Hidxv0 | Hidxv1]. rewrite Hidxv0. auto.
destruct_con. simpl. bool_rel; omega. }
rewrite Hidxv'.
destruct (idx =? 18446744073709551615) eqn:Heq. inversion Hspec.
rewrite <- id_halt0. reflexivity.
destruct Hidxv. bool_rel. contradiction.
assert((0 <=? idx) && (idx <? 2199023255552) = true) as Hval'.
{ apply andb_true_iff. apply andb_true_iff in H0. destruct H0. split_and. auto. bool_rel. omega. }
rewrite Hval'. unfold Spec.get_s2_page_vmid_spec. rewrite <- id_halt0.
bool_rel. auto.
assert((0 <=? idx) && (idx <=? 18446744073709551615)=true).
{ destruct Hidxv. rewrite H4. auto.
destruct_con. simpl. bool_rel; omega. }
rewrite H4.
destruct s2page_rel0.
pose proof (Hs2rel pfn idx) as Hrpi. unfold PAGE_SIZE in Hrpi.
duplicate Hidx. apply Hrpi in H5. destruct H5 as (Hinv & Hpi). bool_rel. autounfold in Hinv.
apply Hinv in H3. rewrite H3. simpl. rewrite <- id_halt0. auto.
destruct s2page_rel0.
pose proof (Hs2rel pfn idx) as Hrpi. autounfold in Hrpi.
duplicate Hidx. apply Hrpi in H4. destruct H4 as (Hinv & _). bool_rel.
assert(idx <> INVALID64).
{ autounfold. intros. apply Hinv in H4. omega. }
unfold INVALID64 in H4.
destruct Hidxv. omega.
assert( (0 <=? idx) && (idx <=? 18446744073709551615) = true).
{ apply andb_true_iff. apply andb_true_iff in H5. destruct H5. split_and. auto. bool_rel. omega. }
rewrite H6. assert(idx =? 18446744073709551615 = false). bool_rel. omega. rewrite H7.
assert((0 <=? idx) && (idx <? 2199023255552) = true) as Hval'.
{ apply andb_true_iff. apply andb_true_iff in H5. destruct H5. split_and. auto. bool_rel. omega. }
rewrite Hval'.
unfold Spec.get_s2_page_vmid_spec. rewrite <- id_halt0.
autounfold. rewrite H5. rewrite id_lock0 in H0. rewrite H0.
apply Hrpi in Hidx. destruct Hidx as (_ & Hpi).
apply Hpi in H5. rewrite H5 in Hspec.
rewrite H5 in H2. rewrite H2. auto. auto. auto.
Qed.
Lemma get_pfn_owner_spec_ref:
compatsim (crel RData RData) (gensem get_pfn_owner_spec) get_pfn_owner_spec_low.
Proof.
Opaque get_pfn_owner_spec.
compatsim_simpl (@match_RData).
exploit get_pfn_owner_spec_exists; eauto 1;
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma set_pfn_owner_spec_exists:
forall habd habd' labd pfn num vmid f
(Hspec: set_pfn_owner_spec pfn num vmid habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', set_pfn_owner_spec0 pfn num vmid labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros.
assert(forall p:Prop, (false=false -> p) -> p) as exp_false.
assert(false = false) as AlwaysFalse. reflexivity.
{ intros. apply H in AlwaysFalse. assumption. }
inversion Hrel. destruct regions_rel0 as [Hreg0 Hreg1].
unfold set_pfn_owner_spec0. unfold_spec Hspec. autounfold in region_cnt_rel0. autounfold in Hspec. autounfold.
induction pfn as [pfn0].
induction num as [num0].
destruct ((0 <=? num0) && (num0 <? 2199023255552)) eqn:Hnum0.
destruct ((0 <=? vmid) && (vmid <=? 257)) eqn:Hvmid0.
destruct ((0 <=? pfn0) && (pfn0 <? 2199023255552)) eqn:Haddr0.
destruct ((0 <=? pfn0 * 4096) && (pfn0 * 4096 <? 2199023255552)) eqn:Haddr1.
remember (pfn0 + num0) as pfn0'.
destruct ((0 <=? pfn0') && (pfn0' <? 2199023255552)) eqn:Haddr0'.
destruct ((0 <=? pfn0' * 4096) && (pfn0' * 4096 <? 2199023255552)) eqn:Haddr1'.
repeat simpl_hyp Hspec;
repeat match goal with
| [H: false = false -> _ |- _] => apply exp_false in H
| _ => idtac
end;
contra; unfold Spec.check_spec.
rename H0 into Hhalt.
assert(forall n:nat, Z.of_nat n <= num0 -> exists pfn' labd', set_pfn_owner_loop0 (n) vmid pfn0 labd = Some(pfn', labd') /\ pfn' = pfn0 + Z.of_nat n /\ labd' = labd).
{ intros.
induction n. unfold set_pfn_owner_loop0. simpl. eexists. eexists. split. auto. split. omega. reflexivity.
rewrite Nat2Z.inj_succ, succ_plus_1 in *. simpl.
assert (Z.of_nat n <= num0) by omega.
apply IHn in H1.
destruct H1 as (pfn0'' & labd'' & Hret & Hpfn & Hlabd).
rewrite Hret. autounfold.
assert ((0 <=? pfn0'') && (pfn0'' <? 2199023255552) = true).
{ rewrite Hpfn.
assert ((0 <=? pfn0 + Z.of_nat n) = true).
{ bool_rel. duplicate Haddr0. apply andb_true_iff in H1. destruct H1. bool_rel. omega.
}
rewrite H1. simpl.
duplicate Haddr0'. apply andb_true_iff in H2. destruct H2. bool_rel. rewrite Heqpfn0' in H3.
assert ((Z.of_nat n < num0)) by omega.
omega.
}
rewrite H1.
assert ((0 <=? pfn0'' * 4096) && (pfn0'' * 4096 <? 2199023255552) = true).
{ rewrite Hpfn.
assert ((0 <=? (pfn0 + Z.of_nat n) * 4096) = true).
{ bool_rel. duplicate Haddr0. apply andb_true_iff in H1. destruct H1. bool_rel. omega.
}
rewrite H2. simpl.
duplicate Haddr1'. apply andb_true_iff in H3. destruct H3. bool_rel. rewrite Heqpfn0' in H4.
assert ((Z.of_nat n < num0)) by omega.
omega.
}
rewrite H2. rewrite Hlabd.
rewrite region_cnt_rel0.
assert ((0 <=? 0) && (0 <=? 18446744073709551615) = true).
{ assert (0 <=? 0 = true). bool_rel. omega.
rewrite H3. simpl. bool_rel. omega.
}
rewrite H3.
assert ((0 =? 18446744073709551615) = false). bool_rel. omega.
rewrite H4.
assert ((0 <=? 0) && (0 <? 2199023255552) = true).
{ assert (0 <=? 0 = true). bool_rel. omega.
rewrite H5. simpl. bool_rel. omega.
}
rewrite H5. unfold Spec.set_s2_page_vmid_spec. rewrite <-id_halt0.
assert (Z.of_nat n <= num0) by omega. apply IHn in H6.
destruct H6 as (pfn' & labd' & Hset & Hpfn' & Hlabd').
eexists. eexists. split. auto. split. rewrite Hpfn. omega. reflexivity.
}
assert (Z.of_nat(Z.to_nat num0) <= num0).
{
rewrite Z2Nat.id. omega. duplicate Hnum0. apply andb_true_iff in H1. destruct H1. bool_rel. assumption.
}
pose proof H0 (Z.to_nat num0) H1.
destruct H2 as (pfn' & labd' & Hset & Hpfn' & Hlabd').
rewrite Hset.
rewrite Z2Nat.id in Hpfn'. rewrite Hlabd'. rewrite Hpfn'.
assert ((0 <=? pfn0 + num0) && (pfn0 + num0 <? 2199023255552) = true). rewrite <-Heqpfn0'. assumption.
rewrite H2.
assert((0 <=? (pfn0 + num0) * 4096) && ((pfn0 + num0) * 4096 <? 2199023255552) = true). rewrite <-Heqpfn0'. assumption.
rewrite H3.
eexists. split. auto. inversion Hspec. rewrite <-H5. assumption. omega.
(*ends for halt = true case*)
assert(forall n:nat, Z.of_nat n <= num0 -> exists hpfn' lpfn' hs2page' labd', set_pfn_owner_loop n vmid pfn0 (s2page habd) = Some (hpfn', hs2page') /\ hpfn' = pfn0 + Z.of_nat n /\ set_pfn_owner_loop0 n vmid pfn0 labd = Some (lpfn', labd') /\ lpfn' = pfn0 + Z.of_nat n /\ relate_RData f habd {s2page: hs2page'} labd').
{ intros.
induction n. eexists. eexists. eexists. eexists.
unfold set_pfn_owner_loop. split. auto. split. simpl. omega.
unfold set_pfn_owner_loop0. split. auto. split. simpl. omega.
constructor; inversion Hrel; try assumption.
intro. apply s2page_rel1 in H8.
constructor. inversion H8. assumption.
rewrite Nat2Z.inj_succ, succ_plus_1 in *.
assert (Z.of_nat n <= num0) by omega.
apply IHn in H8.
destruct H8 as (hpfn' & lpfn' & hs2page' & labd' & Hseth & Hhpfn & Hsetl & Hlpfn & Hrelate).
destruct ((owner (ZMap.get hpfn' hs2page') =? 4294967295)) eqn:Hownerinv.
eexists. eexists. eexists. eexists. split.
unfold set_pfn_owner_loop.
unfold set_pfn_owner_loop in Hseth. rewrite Hseth. autounfold.
assert ((0 <=? hpfn') && (hpfn' <? 2199023255552) = true).
{ rewrite Hhpfn.
assert ((0 <=? pfn0 + Z.of_nat n) = true).
{ bool_rel. duplicate Haddr0. apply andb_true_iff in H8. destruct H8. bool_rel. omega.
}
rewrite H8. simpl.
duplicate Haddr0'. apply andb_true_iff in H9. destruct H9. bool_rel. rewrite Heqpfn0' in H10.
assert ((Z.of_nat n < num0)) by omega.
omega.
}
rewrite H8.
assert ((0 <=? hpfn' * 4096) && (hpfn' * 4096 <? 2199023255552) = true).
{ rewrite Hhpfn.
assert ((0 <=? (pfn0 + Z.of_nat n) * 4096) = true).
{ bool_rel. duplicate Haddr0. apply andb_true_iff in H9. destruct H9. bool_rel. omega.
}
rewrite H9. simpl.
duplicate Haddr1'. apply andb_true_iff in H10. destruct H10. bool_rel. rewrite Heqpfn0' in H11.
assert ((Z.of_nat n < num0)) by omega.
omega.
}
rewrite H9.
assert ((hpfn' =? lpfn') = true) as Hequpfn. bool_rel. omega.
rewrite Hownerinv. auto. split. omega. split.
unfold set_pfn_owner_loop0. unfold set_pfn_owner_loop0 in Hsetl. rewrite Hsetl. autounfold.
assert ((0 <=? lpfn') && (lpfn' <? 2199023255552) = true).
{ rewrite Hlpfn.
assert ((0 <=? pfn0 + Z.of_nat n) = true).
{ bool_rel. duplicate Haddr0. apply andb_true_iff in H8. destruct H8. bool_rel. omega.
}
rewrite H8. simpl.
duplicate Haddr0'. apply andb_true_iff in H9. destruct H9. bool_rel. rewrite Heqpfn0' in H10.
assert ((Z.of_nat n < num0)) by omega.
omega.
}
rewrite H8.
assert ((0 <=? lpfn' * 4096) && (lpfn' * 4096 <? 2199023255552) = true).
{ rewrite Hlpfn.
assert ((0 <=? (pfn0 + Z.of_nat n) * 4096) = true).
{ bool_rel. duplicate Haddr0. apply andb_true_iff in H9. destruct H9. bool_rel. omega.
}
rewrite H9. simpl.
duplicate Haddr1'. apply andb_true_iff in H10. destruct H10. bool_rel. rewrite Heqpfn0' in H11.
assert ((Z.of_nat n < num0)) by omega.
omega.
}
rewrite H9.
inversion Hrelate.
assert (halt habd {s2page : hs2page'} = false). assumption.
apply s2page_rel1 in H10. inversion H10.
destruct regions_rel0 as [Hreg0' Hreg1'].
pose proof (page_index_succ (lpfn' * 4096) labd' H9 Hreg0' region_cnt_rel1) as Hpis;
destruct Hpis as (idx0 & Hidx & Hidxv).
duplicate Hidx. rename H11 into Hidx''.
assert ((hpfn' =? lpfn') = true) as Hequpfn. bool_rel. omega. rewrite Hidx.
eapply Hs2rel in Hidx. bool_rel. destruct Hidx. duplicate Hownerinv. rewrite Hequpfn in H13. apply H11 in H13.
assert((0 <=? idx0) && (idx0 <=? 18446744073709551615) = true).
apply andb_true_iff. split_and. bool_rel. rewrite H13. unfold INVALID64. omega. bool_rel. rewrite H13. unfold INVALID64. omega.
rewrite H14.
assert ((idx0 =? 18446744073709551615) = true). bool_rel. exact H13.
rewrite H15. auto. split. omega. assumption.
unfold set_pfn_owner_loop.
unfold set_pfn_owner_loop in Hseth. rewrite Hseth. autounfold.
assert ((0 <=? hpfn') && (hpfn' <? 2199023255552) = true).
{ rewrite Hhpfn.
assert ((0 <=? pfn0 + Z.of_nat n) = true).
{ bool_rel. duplicate Haddr0. apply andb_true_iff in H8. destruct H8. bool_rel. omega.
}
rewrite H8. simpl.
duplicate Haddr0'. apply andb_true_iff in H9. destruct H9. bool_rel. rewrite Heqpfn0' in H10.
assert ((Z.of_nat n < num0)) by omega.
omega.
}
rewrite H8.
assert ((0 <=? hpfn' * 4096) && (hpfn' * 4096 <? 2199023255552) = true).
{ rewrite Hhpfn.
assert ((0 <=? (pfn0 + Z.of_nat n) * 4096) = true).
{ bool_rel. duplicate Haddr0. apply andb_true_iff in H9. destruct H9. bool_rel. omega.
}
rewrite H9. simpl.
duplicate Haddr1'. apply andb_true_iff in H10. destruct H10. bool_rel. rewrite Heqpfn0' in H11.
assert ((Z.of_nat n < num0)) by omega.
omega.
}
rewrite H9. rewrite Hownerinv.
unfold set_pfn_owner_loop0. unfold set_pfn_owner_loop0 in Hsetl. rewrite Hsetl. autounfold.
assert ((0 <=? lpfn') && (lpfn' <? 2199023255552) = true).
{ rewrite Hlpfn.
assert ((0 <=? pfn0 + Z.of_nat n) = true).
{ bool_rel. duplicate Haddr0. apply andb_true_iff in H8. destruct H8. bool_rel. omega.
}
rewrite H10. simpl.
duplicate Haddr0'. apply andb_true_iff in H11. destruct H11. bool_rel. rewrite Heqpfn0' in H12.
assert ((Z.of_nat n < num0)) by omega.
omega.
}
rewrite H10.
assert ((0 <=? lpfn' * 4096) && (lpfn' * 4096 <? 2199023255552) = true).
{ rewrite Hlpfn.
assert ((0 <=? (pfn0 + Z.of_nat n) * 4096) = true).
{ bool_rel. duplicate Haddr0. apply andb_true_iff in H11. destruct H11. bool_rel. omega.
}
rewrite H11. simpl.
duplicate Haddr1'. apply andb_true_iff in H12. destruct H12. bool_rel. rewrite Heqpfn0' in H13.
assert ((Z.of_nat n < num0)) by omega.
omega.
}
rewrite H11.
inversion Hrelate.
assert (halt habd {s2page : hs2page'} = false). assumption.
apply s2page_rel1 in H12. inversion H12.
destruct regions_rel0 as [Hreg0' Hreg1'].
pose proof (page_index_succ (lpfn' * 4096) labd' H11 Hreg0' region_cnt_rel1) as Hpis;
destruct Hpis as (idx0 & Hidx & Hidxv).
duplicate Hidx. rename H13 into Hidx00'.
assert ((hpfn' =? lpfn') = true) as Hequpfn. bool_rel. omega. rewrite Hidx.
eapply Hs2rel in Hidx. bool_rel. destruct Hidx. duplicate Hownerinv. rewrite Hequpfn in H15.
assert((0 <=? idx0) && (idx0 <=? 18446744073709551615) = true).
{ destruct Hidxv. rewrite H16. auto. unfold is_s2page in H16.
destruct_con. simpl. unfold MAX_S2PAGE_NUM in Hcond0. bool_rel; omega.
}
rewrite H16.
assert(hs2page' = s2page habd {s2page : hs2page'}). unfold s2page. reflexivity.
assert(idx0 =? INVALID64 = false). bool_rel. rewrite <-H17 in H13. unfold INVALID in H13. omega.
unfold INVALID64 in H18. rewrite H18.
assert((0 <=? idx0) && (idx0 <? 2199023255552) = true) as Hval'.
{ destruct Hidxv. unfold INVALID64 in H19. bool_rel. contradiction.
unfold is_s2page in H19. unfold MAX_S2PAGE_NUM in H19.
apply andb_true_iff in H19. destruct H19. rewrite H19. simpl. bool_rel. omega.
}
rewrite Hval'.
unfold Spec.set_s2_page_vmid_spec. rewrite <-id_halt1.
assert (halt habd {s2page : hs2page'} = false). unfold halt. assumption.
rewrite H19. autounfold.
assert ((0 <=? idx0) && (idx0 <? 16777216) = true).
{ destruct Hidxv. unfold INVALID64 in H19. bool_rel. contradiction.
unfold is_s2page in H20. unfold MAX_S2PAGE_NUM in H20. assumption.
}
rewrite H20. rewrite Hvmid0. simpl.
assert (halt habd {s2page : hs2page'} = false). assumption.
apply id_lock1 in H21.
rewrite <-H21.
assert(lock habd {s2page : hs2page'} = lock habd). unfold lock. simpl. reflexivity.
rewrite H22. rewrite H0.
eexists. eexists. eexists. eexists. split. auto. split. omega. split. auto. split. omega.
constructor; inversion Hrelate; try assumption.
intro.
constructor.
intro pfn1. intro idx1. intro Hidx1.
pose proof (Hs2rel pfn1 idx1) as Hrpi1.
assert (forall pfn2, get_s2_page_index_spec (VZ64 (pfn2 * PAGE_SIZE)) labd' {s2page : ZMap.set idx0 (ZMap.get idx0 (s2page labd')) {owner : vmid} (s2page labd')} = get_s2_page_index_spec (VZ64 (pfn2 * PAGE_SIZE)) labd' ).
unfold get_s2_page_index_spec. simpl. reflexivity.
pose proof (H24 pfn1).
rewrite H25 in Hidx1.
duplicate Hidx1.
rename H26 into Hidx1'.
apply Hrpi1 in Hidx1.
split_and.
destruct Hidx1.
destruct H27.
Focus 2.
assert(count (ZMap.get pfn1 (s2page habd {s2page : ZMap.set hpfn' (ZMap.get hpfn' hs2page') {owner : vmid} hs2page'})) = count (ZMap.get pfn1 (s2page habd {s2page : hs2page'}))).
{ simpl. destruct ((pfn1=? hpfn')) eqn: Hpfn.
bool_rel. rewrite Hpfn. rewrite ZMap.gss.
unfold owner. simpl. reflexivity.
rewrite ZMap.gso. reflexivity. bool_rel. assumption.
}
rewrite H26. destruct Hidx1. destruct H28. assumption.
destruct ((pfn1 =? hpfn')) eqn: Hpfn.
bool_rel.
assert(get_s2_page_index_spec (VZ64 (pfn1 * PAGE_SIZE)) labd' = get_s2_page_index_spec (VZ64 (hpfn' * PAGE_SIZE)) labd').
rewrite Hpfn. reflexivity.
rewrite H29 in Hidx1'. unfold PAGE_SIZE in Hidx1'. rewrite Hequpfn in Hidx1'. rewrite Hidx00' in Hidx1'.
inversion Hidx1'.
assert((idx1=? INVALID64) = false).
rewrite H31 in H18. bool_rel. assumption.
rewrite Hpfn. simpl.
rewrite ZMap.gss.
unfold RData.owner.
simpl.
autounfold.
unfold INVALID64 in H30.
constructor.
intros.
bool_rel.
contradiction.
intros.
assert((4294967295 <=? 257) = false). bool_rel. omega. rewrite H32 in Hvmid0. rewrite andb_true_iff in Hvmid0. destruct Hvmid0. bool_rel. contradict H35. autounfold. omega.
bool_rel. simpl. rewrite ZMap.gso. assumption. assumption.
destruct Hidx1. destruct H27.
intro. duplicate H29. rename H30 into Hidxtrue. apply H28 in H29.
destruct ((pfn1 =? hpfn')) eqn: Hpfn.
assert(get_s2_page_index_spec (VZ64 (pfn1 * PAGE_SIZE)) labd' = get_s2_page_index_spec (VZ64 (hpfn' * PAGE_SIZE)) labd').
bool_rel. rewrite Hpfn. reflexivity.
rewrite H30 in Hidx1'. unfold PAGE_SIZE in Hidx1'. rewrite Hequpfn in Hidx1'. rewrite Hidx00' in Hidx1'.
inversion Hidx1'. simpl. bool_rel. rewrite <-Hpfn. rewrite ZMap.gss. simpl. rewrite ZMap.gss. simpl in H29. rewrite H29. reflexivity.
bool_rel. simpl.
rewrite ZMap.gso. simpl. rewrite ZMap.gso. assumption.
symmetry in id_halt2.
assert (is_memblock(region_cnt labd') = true).
unfold is_memblock. unfold MAX_MEMBLOCK_NUM. assumption.
assert(is_s2page idx0 = true).
unfold is_s2page. unfold MAX_S2PAGE_NUM. assumption.
assert ( halt habd {s2page : hs2page'} = false). unfold halt. simpl. assumption.
rewrite H32 in id_halt2.
destruct regions_rel0 as [Hreg00' Hreg10'].
rewrite <-Hequpfn in Hidx00'.
pose proof (page_index_unique labd' pfn1 hpfn' idx1 idx0 id_halt2 Hreg00' Hreg10' H30 Hidx1' Hidx00' Hidxtrue H31).
auto. assumption.
}
assert (Z.of_nat(Z.to_nat num0) <= num0).
{
rewrite Z2Nat.id. omega. duplicate Hnum0. apply andb_true_iff in H8. destruct H8. bool_rel. assumption.
}
pose proof H7 (Z.to_nat num0). apply H9 in H8.
destruct H8 as (hpfn' & lpfn' & hs2page' & labd' & Hseth' & Hhpfn' & Hsetl' & Hlpfn' & Hrelate).
rewrite Hsetl'.
assert ((0 <=? lpfn') && (lpfn' <? 2199023255552) = true).
{ rewrite Hlpfn'. simpl. rewrite Z2Nat.id.
rewrite <- Heqpfn0'.
assumption. apply andb_true_iff in Hnum0. bool_rel. assumption.
}
rewrite H8.
assert ((0 <=? lpfn' * 4096) && (lpfn' * 4096 <? 2199023255552) = true).
{ rewrite Hlpfn'. simpl. rewrite Z2Nat.id.
rewrite <- Heqpfn0'.
assumption. apply andb_true_iff in Hnum0. bool_rel. assumption.
}
rewrite H10. eexists. split. auto. inversion Hspec. rewrite Hseth' in H3. inversion H3. rewrite <-H14. assumption.
inversion Hspec.
inversion Hspec.
inversion Hspec.
inversion Hspec.
inversion Hspec.
inversion Hspec.
Qed.
Lemma set_pfn_owner_spec_ref:
compatsim (crel RData RData) (gensem set_pfn_owner_spec) set_pfn_owner_spec_low.
Proof.
Opaque set_pfn_owner_spec.
compatsim_simpl (@match_RData).
exploit set_pfn_owner_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma get_pfn_count_spec_exists:
forall habd labd pfn res f
(Hspec: get_pfn_count_spec (VZ64 pfn) habd = Some res)
(Hrel: relate_RData f habd labd),
get_pfn_count_spec0 (VZ64 pfn) labd = Some res.
Proof.
intros.
assert(forall p:Prop, (false=false -> p) -> p) as exp_false.
assert(false = false) as AlwaysFalse. reflexivity.
{ intros. apply H in AlwaysFalse. assumption. }
inversion Hrel. destruct regions_rel0 as [Hreg0 Hreg1].
unfold get_pfn_count_spec0. unfold_spec Hspec. autounfold in region_cnt_rel0. autounfold in Hspec. autounfold.
destruct ((0 <=? pfn) && (pfn <? 2199023255552)) eqn:Haddr0.
destruct ( (0 <=? pfn * 4096) && (pfn * 4096 <? 2199023255552)) eqn:Haddr1.
repeat simpl_hyp Hspec;
repeat match goal with
| [H: false = false -> _ |- _] => apply exp_false in H
| _ => idtac
end;
contra; unfold Spec.check_spec;
pose proof (page_index_succ (pfn * 4096) labd Haddr1 Hreg0 region_cnt_rel0) as Hpis;
destruct Hpis as (idx & Hidx & Hidxv);
rewrite Hidx; autounfold in Hidxv.
assert((0 <=? idx) && (idx <=? 18446744073709551615)=true) as Hidxv'.
{ destruct Hidxv as [Hidxv0 | Hidxv1]. rewrite Hidxv0. auto.
destruct_con. simpl. bool_rel; omega. }
rewrite Hidxv'.
destruct (idx =? 18446744073709551615) eqn:Heq. inversion Hspec.
rewrite <- id_halt0. reflexivity.
destruct Hidxv. bool_rel. contradiction.
assert((0 <=? idx) && (idx <? 2199023255552) = true) as Hval'.
{ apply andb_true_iff. apply andb_true_iff in H0. destruct H0. split_and. auto. bool_rel. omega. }
rewrite Hval'. unfold Spec.get_s2_page_count_spec. rewrite <- id_halt0.
bool_rel. auto.
apply andb_true_iff in H2. bool_rel. destruct H2. contradict H4. rewrite H3.
assert((4294967295 <=? 1024) = false). bool_rel. omega. rewrite H4. auto.
assert((0 <=? idx) && (idx <=? 18446744073709551615)=true).
{ destruct Hidxv. rewrite H4. auto.
destruct_con. simpl. bool_rel; omega. }
rewrite H4.
destruct s2page_rel0.
pose proof (Hs2rel pfn idx) as Hrpi. unfold PAGE_SIZE in Hrpi.
duplicate Hidx. apply Hrpi in H5. destruct H5 as (_ & Hinv & Hpi). bool_rel. autounfold in Hinv.
assert(idx <> INVALID64).
{ autounfold. intros. apply Hinv in H5. omega. }
assert(idx =? INVALID64 = false). bool_rel. omega. unfold INVALID64 in H6. rewrite H6.
destruct Hidxv. bool_rel. contradiction.
assert((0 <=? idx) && (idx <? 2199023255552) = true) as Hval'.
{ apply andb_true_iff. apply andb_true_iff in H7. destruct H7. split_and. auto. bool_rel. auto. omega. }
rewrite Hval'.
unfold Spec.get_s2_page_count_spec. rewrite <- id_halt0.
autounfold. rewrite H7. rewrite id_lock0 in H0. rewrite H0.
apply Hrpi in Hidx. destruct Hidx as (_ & _ & Hpi').
apply Hpi' in H7. rewrite H7 in Hspec.
rewrite H7 in H2. rewrite H2. auto. auto. auto.
Qed.
Lemma get_pfn_count_spec_ref:
compatsim (crel RData RData) (gensem get_pfn_count_spec) get_pfn_count_spec_low.
Proof.
Opaque get_pfn_count_spec.
compatsim_simpl (@match_RData).
exploit get_pfn_count_spec_exists; eauto 1;
refine_split; repeat (try econstructor; eauto).
Qed.
Lemma set_pfn_count_spec_exists:
forall habd habd' labd pfn count f
(Hspec: set_pfn_count_spec pfn count habd = Some habd')
(Hrel: relate_RData f habd labd),
exists labd', set_pfn_count_spec0 pfn count labd = Some labd' /\ relate_RData f habd' labd'.
Proof.
intros.
assert(forall p:Prop, (false=false -> p) -> p) as exp_false.
assert(false = false) as AlwaysFalse. reflexivity.
{ intros. apply H in AlwaysFalse. assumption. }
inversion Hrel. destruct regions_rel0 as [Hreg0 Hreg1].
unfold set_pfn_count_spec0. unfold_spec Hspec. autounfold in region_cnt_rel0. autounfold in Hspec. autounfold.
induction pfn as [pfn0].
destruct ((0 <=? pfn0) && (pfn0 <? 2199023255552)) eqn:Haddr0.
destruct ((0 <=? pfn0 * 4096) && (pfn0 * 4096 <? 2199023255552)) eqn:Haddr1.
destruct ((0 <=? count) && (count <=? 1024)) eqn:Hcount.
repeat simpl_hyp Hspec;
repeat match goal with
| [H: false = false -> _ |- _] => apply exp_false in H
| _ => idtac
end;
contra; unfold Spec.check_spec;
pose proof (page_index_succ (pfn0 * 4096) labd Haddr1 Hreg0 region_cnt_rel0) as Hpis;
destruct Hpis as (idx0 & Hidx & Hidxv);
rewrite Hidx; autounfold in Hidxv.
assert((0 <=? idx0) && (idx0 <=? 18446744073709551615)=true) as Hidxv'.
{ destruct Hidxv as [Hidxv0 | Hidxv1]. rewrite Hidxv0. auto.
destruct_con. simpl. bool_rel; omega. }
rewrite Hidxv'.
destruct (idx0 =? 18446744073709551615) eqn:Heq. inversion Hspec.
eexists.
split. auto. rewrite <- H1. assumption.
destruct Hidxv. bool_rel. contradiction.
assert((0 <=? idx0) && (idx0 <? 2199023255552) = true) as Hval'.
{ apply andb_true_iff. apply andb_true_iff in H0. destruct H0. split_and. auto. bool_rel. omega. }
rewrite Hval'.
unfold Spec.set_s2_page_count_spec. rewrite <- id_halt0.
eexists.
split. auto. inversion Hspec. rewrite <- H2. assumption.
(*ends for halt = true case *)
inversion s2page_rel0.
duplicate Hidx.
eapply Hs2rel in H3.
destruct H3.
bool_rel.
apply H3 in H2.
assert((0 <=? idx0) && (idx0 <=? 18446744073709551615) = true).
apply andb_true_iff. split_and. bool_rel. rewrite H2. unfold INVALID64. omega. bool_rel. rewrite H2. unfold INVALID64. omega.
rewrite H5.
rewrite H2.
unfold INVALID64.
assert (18446744073709551615 =? 18446744073709551615 = true).
bool_rel. omega. rewrite H6.
inversion Hspec.
eexists.
split. auto. rewrite <- H8. assumption.
(*ends for owner = invalid case*)
assert((0 <=? idx0) && (idx0 <=? 18446744073709551615)=true).
{ destruct Hidxv. rewrite H3. auto.
destruct_con. simpl. bool_rel; omega. }
rewrite H3.
destruct s2page_rel0.
pose proof (Hs2rel pfn0 idx0) as Hrpi. unfold PAGE_SIZE in Hrpi.
duplicate Hidx. apply Hrpi in H4. destruct H4 as (Hinv & _ & Hpi). bool_rel. autounfold in Hinv.
assert(idx0 <> INVALID64).
{ autounfold. intros. apply Hinv in H4. omega. }
assert(idx0 =? INVALID64 = false). bool_rel. omega. unfold INVALID64 in H5. rewrite H5.
destruct Hidxv. bool_rel. contradiction.
assert((0 <=? idx0) && (idx0 <? 2199023255552) = true) as Hval'.
{ apply andb_true_iff. apply andb_true_iff in H6. destruct H6. split_and. auto. bool_rel. auto. omega. }
rewrite Hval'.
unfold Spec.set_s2_page_count_spec. rewrite <- id_halt0.
autounfold. rewrite H6. rewrite id_lock0 in H0. rewrite H0.
rewrite Hcount.
eexists.
split. auto. inversion Hspec.
constructor; try simpl; try srewrite; try reflexivity.
unfold is_memblock. unfold MAX_MEMBLOCK_NUM. assumption. split; try assumption. intros. rewrite <-id_halt0 in H7.
constructor.
intro pfn1.
intro idx1.
intro Hidx1.
pose proof (Hs2rel pfn1 idx1) as Hrpi1.
assert (forall pfn2, get_s2_page_index_spec (VZ64 (pfn2 * PAGE_SIZE)) labd {s2page : ZMap.set idx0 (ZMap.get idx0 (s2page labd)) {count : count} (s2page labd)} = get_s2_page_index_spec (VZ64 (pfn2 * PAGE_SIZE)) labd ).
unfold get_s2_page_index_spec. simpl. reflexivity.
pose proof (H9 pfn1).
rewrite H10 in Hidx1.
duplicate Hidx1.
rename H11 into Hidx1'.
apply Hrpi1 in Hidx1.
split_and.
destruct Hidx1.
destruct H12.
assert (owner (ZMap.get pfn1 (s2page habd)) = owner (ZMap.get pfn1 (s2page habd')) ).
rewrite <-H8.
simpl.
destruct ((pfn1=?pfn0)) eqn: Hpfn.
bool_rel.
rewrite Hpfn.
rewrite ZMap.gss.
unfold owner. simpl. reflexivity.
rewrite ZMap.gso. reflexivity. bool_rel. assumption.
rewrite <-H14. assumption.
destruct ((pfn1=?pfn0)) eqn: Hpfn.
bool_rel.
assert(get_s2_page_index_spec (VZ64 (pfn1 * PAGE_SIZE)) labd = get_s2_page_index_spec (VZ64 (pfn0 * PAGE_SIZE)) labd).
rewrite Hpfn. reflexivity.
rewrite H11 in Hidx1'. unfold PAGE_SIZE in Hidx1'. rewrite Hidx in Hidx1'.
inversion Hidx1'.
assert((idx1=? INVALID64) = false).
rewrite H13 in H4. bool_rel. assumption.
rewrite <- H8.
rewrite Hpfn. simpl.
rewrite ZMap.gss.
unfold RData.count.
simpl.
autounfold.
unfold INVALID64 in H12.
constructor.
intros.
bool_rel.
contradiction.
intros.
assert((4294967295 <=? 1024) = false). bool_rel. omega. rewrite H14 in Hcount. rewrite andb_true_iff in Hcount. destruct Hcount. bool_rel. contradict H17. autounfold. omega.
bool_rel. rewrite <-H8. simpl. rewrite ZMap.gso. destruct Hidx1. destruct H12. assumption. assumption.
rewrite <- H8. destruct Hidx1. destruct H12.
intro. duplicate H14. rename H15 into Hidxtrue. apply H13 in H14.
destruct ((pfn1=?pfn0)) eqn: Hpfn.
assert(get_s2_page_index_spec (VZ64 (pfn1 * PAGE_SIZE)) labd = get_s2_page_index_spec (VZ64 (pfn0 * PAGE_SIZE)) labd).
bool_rel. rewrite Hpfn. reflexivity.
rewrite H15 in Hidx1'. unfold PAGE_SIZE in Hidx1'. rewrite Hidx in Hidx1'.
inversion Hidx1'. simpl. bool_rel. rewrite <-Hpfn. rewrite ZMap.gss. simpl. rewrite ZMap.gss. rewrite H14. reflexivity.
bool_rel. simpl.
rewrite ZMap.gso. simpl. rewrite ZMap.gso. assumption.
symmetry in id_halt0.
assert (is_memblock(region_cnt labd) = true).
unfold is_memblock. unfold MAX_MEMBLOCK_NUM. assumption.
assert(is_s2page idx0 = true).
unfold is_s2page. unfold MAX_S2PAGE_NUM. assumption.
pose proof (page_index_unique labd pfn1 pfn0 idx1 idx0 id_halt0 Hreg0 Hreg1 H15 Hidx1' Hidx Hidxtrue H16).
assert (forall p q:Prop, (p->q)->(~q->~p)).
intros. intro. apply H19. apply H18. exact H20.
apply H18 in H17. assumption. assumption. assumption.
(*ends for owner <> invlid case*)
inversion Hspec.
inversion Hspec.
inversion Hspec.
Qed.
Lemma set_pfn_count_spec_ref:
compatsim (crel RData RData) (gensem set_pfn_count_spec) set_pfn_count_spec_low.
Proof.
Opaque set_pfn_count_spec.
compatsim_simpl (@match_RData).
exploit set_pfn_count_spec_exists; eauto 1;
intros (labd' & Hspec & Hrel).
refine_split; repeat (try econstructor; eauto).
Qed.
End FreshPrim.
Section PassthroughPrim.
Lemma passthrough_correct:
sim (crel HDATA LDATA) PageMgmt_passthrough PageIndex.
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_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.
Qed.
End PassthroughPrim.
End WITHMEM.
End PageMgmtProofHigh.