InvariantProof

Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import GenSem.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import RealParams.
Require Import GenSem.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import PrimSemantics.
Require Import CompatClightSem.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.

Require Import RData.
Require Import Constants.
Require Import HypsecCommLib.
Require Import Specs.
Require Import Invs.

Local Open Scope Z.

Lemma map_host_inv:
  forall addr s s' a b
    (ex: local_map_host addr s = (s', false, a, b))
    (Haddr: valid_addr addr),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex.
  destruct (s2_owner (addr / 4096) @ (s2page s) =? 4294967295) eqn:Hinvalid; simpl in *.
  pose proof (local_mmap_level3 _ _ _ _ _ C0) as Hn.
  destruct H; autounfold in *.
  constructor; autounfold; simpl; try assumption.
  rewrite ZMap.gss. intros until pte. rewrite Hn.
  destruct_zmap. intros. inv H. reflexivity. apply host_npt_cons0.
  rewrite ZMap.gss. intros until pte. rewrite Hn.
  destruct_zmap. intros. inv H.
  rewrite host_pte_pfn_dev. reflexivity.  assumption.
  apply host_flatmap0.
  rewrite ZMap.gss. intros until pte. rewrite Hn.
  destruct_zmap. intros. inv Hpfn. rewrite host_pte_pfn_dev; try assumption.
  left. assumption. apply host_iso0.
  intros. assert_gsoH H. red; intro. subst. omega. rewrite (ZMap.gso _ _ Hneq) in H.
  eapply vm_iso0; eassumption.
  pose proof (local_mmap_level3 _ _ _ _ _ C0) as Hn.
  destruct H; autounfold in *.
  constructor; autounfold; simpl; try assumption.
  rewrite ZMap.gss. intros until pte. rewrite Hn.
  destruct_zmap. intros. inv H. reflexivity. apply host_npt_cons0.
  rewrite ZMap.gss. intros until pte. rewrite Hn.
  destruct_zmap. intros. inv H.
  rewrite host_pte_pfn_mem. reflexivity.  assumption.
  apply host_flatmap0.
  rewrite ZMap.gss. intros until pte. rewrite Hn.
  destruct_zmap. intros. inv Hpfn. rewrite host_pte_pfn_mem; try assumption.
  right. bool_rel_all; autounfold in *; omega. apply host_iso0.
  intros. assert_gsoH H. red; intro. subst. omega. rewrite (ZMap.gso _ _ Hneq) in H.
  eapply vm_iso0; eassumption.
Qed.

Lemma clear_vm_page_inv:
  forall vmid pfn s s' a b c
    (ex: local_clear_vm_page vmid pfn s = (s', false, a, b, c))
    (valid_vm': valid_vm vmid)
    (valid_state': vm_state (VS (vmid @ (vminfos s))) = POWEROFF),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex; bool_rel; try assumption.
  destruct H; autounfold in *.
  assert(Hcount0: forall n, 0 <= Z.of_nat n <= EL2_SMMU_CFG_SIZE -> count_smmu_map n pfn (smmu_vmid s) (spts s) = 0).
  { Local Transparent count_smmu_map.
    induction n0. intros; reflexivity.
    rewrite Nat2Z.inj_succ, succ_plus_1. intros.
    simpl. rewrite IHn0. repeat destruct_if; try omega.
    match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) eqn: Hsp end.
    autounfold in *; bool_rel. destruct_if; try reflexivity; bool_rel.
    exploit (smmu_iso0 0 (Z.of_nat n0 mod 8) (Z.of_nat n0 / 8) (pfn + 1000000000) z2 z3);
      autounfold; try eassumption; try omega.
    rewrite Z.mul_comm. rewrite <- Z.div_mod. assumption. omega.
    assert(0 <= Z.of_nat n0 <= 15) by omega.
    assert(0 <= Z.of_nat n0 / 8 <= 1).
    eapply (Z_div_le_le 0 _ 15 8); omega. omega.
    apply Z_mod_lt; omega.
    intros (? & ?).
    rewrite Z.mul_comm, <- Z.div_mod in H0; try omega.
    rewrite Case in H0.
    pose proof (host_s2_map0 z2 H0). rewrite H1 in H2.
    destruct (zeq z2 pfn); srewrite; omega.
    match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) eqn: Hsp end.
    destruct_if; reflexivity. omega.
    Local Opaque count_smmu_map. }
  destruct (z =? 0) eqn:Hz.
  inv C2; bool_rel; srewrite.
  replace z0 with 0 in *.
  rewrite zmap_set_id.
  constructor; autounfold; simpl; try assumption.
  intros. destruct_zmap. simpl. reflexivity.
  apply host_s2_map0. rewrite (ZMap.gso _ _ Heq) in H. assumption.
  assert_gso. red; intro T. rewrite T in page_0_invalid0. omega.
  rewrite (ZMap.gso _ _ Hneq). assumption.
  intros. destruct_zmap. simpl. auto.
  eapply host_iso0; try eassumption.
  intros. destruct_zmap. srewrite.
  exploit (vm_iso0 _ _ _ _ _ H); try eassumption. omega.
  intros. srewrite. omega. eapply vm_iso0; try eassumption.
  rewrite (ZMap.gso _ _ Heq) in H3. assumption.
  intros. destruct_zmap. rewrite Heq in *.
  exploit (smmu_iso0 vmid cbndx index gfn pfn pte); try eassumption.
  intros (? & ?). srewrite. destruct Hvalid_vmid; omega.
  eapply smmu_iso0; eassumption.
  intro. destruct_zmap. simpl; intros.
  rewrite Hcount0. omega. simpl; autounfold. omega.
  apply smmu_count0. pose proof (host_npt_cons0 _ _ _ _ C0).
  rewrite H. reflexivity.
  pose proof (local_mmap_level3 _ _ _ _ _ C2).
  constructor; autounfold; simpl; try assumption.
  intros until pte. rewrite ZMap.gss. rewrite H. destruct_zmap.
  intro T. inv T. reflexivity. apply host_npt_cons0.
  intros until pte. rewrite ZMap.gss. rewrite H. destruct_zmap.
  replace (phys_page 144115188075855872 / PAGE_SIZE) with 0 by reflexivity.
  intros. inv H0. contra. apply host_flatmap0.
  intros. destruct_zmap. simpl. reflexivity.
  apply host_s2_map0. rewrite (ZMap.gso _ _ Heq) in H0. assumption.
  assert_gso. red; intro T. rewrite T in page_0_invalid0. omega.
  rewrite (ZMap.gso _ _ Hneq). assumption.
  rewrite ZMap.gss. intros until pte. rewrite H.
  replace (phys_page 144115188075855872 / PAGE_SIZE) with 0 by reflexivity.
  destruct_zmap. intros. destruct_zmap. simpl. auto. inv Hpfn. contra.
  destruct_zmap. simpl. intros; auto.
  eapply host_iso0; try eassumption.
  intros. assert_gsoH H0. red; intro. rewrite H5 in H1; omega.
  rewrite (ZMap.gso _ _ Hneq) in H0.
  destruct_zmap. srewrite.
  exploit (vm_iso0 _ _ _ _ _ H0); try eassumption. omega.
  intros. srewrite. omega. eapply vm_iso0; try eassumption.
  rewrite (ZMap.gso _ _ Heq) in H4. assumption.
  intros. destruct_zmap. rewrite Heq in *.
  exploit (smmu_iso0 vmid0 cbndx index gfn pfn pte); try eassumption.
  intros (? & ?). srewrite. destruct Hvalid_vmid; omega.
  eapply smmu_iso0; eassumption.
  intro. destruct_zmap. simpl; intros.
  rewrite Hcount0. omega. simpl; autounfold. omega.
  apply smmu_count0.
Qed.

Lemma assign_pfn_to_vm_inv:
  forall vmid gfn pfn dorc logn s s' n a b c
    (ex: local_assign_pfn_to_vm vmid gfn pfn dorc logn s = (s', false, n, a, b, c))
    (valid_vm': valid_vm vmid),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex; bool_rel; try assumption.
  - duplicate H; destruct H; autounfold in *.
    pose proof (smmu_count_0_no_map _ D _ C C0) as Hcount0.
    destruct (z =? 0) eqn:Hz.
    + inv C3; bool_rel; srewrite.
      replace z0 with 0 in *.
      rewrite zmap_set_id.
      constructor; autounfold; simpl; try assumption.
      * intro. destruct_zmap. simpl. intros; omega. apply host_s2_map0.
      * assert_gso. red; intro T. rewrite T in page_0_invalid0. omega.
        rewrite (ZMap.gso _ _ Hneq). assumption.
      * intros. destruct_zmap. rewrite Heq in *.
        rewrite (host_flatmap0 _ _ _ _ Hpfn) in Hpfn. rewrite C1 in Hpfn. inv Hpfn.
        contra. assumption. eapply host_iso0; try eassumption.
      * intros. destruct_zmap. rewrite Heq in *.
        exploit (vm_iso0 _ _ _ _ _ H); try eassumption. omega.
        intros. rewrite C in H4. omega. rewrite (ZMap.gso _ _ Heq) in H3.
         eapply vm_iso0; eassumption.
      * intros. destruct_zmap. simpl. rewrite Heq in *.
        exploit (smmu_iso0 vmid0 cbndx index gfn0 pfn pte); try eassumption.
        intros (? & ?). srewrite. eapply Hcount0 in Heq; try eassumption. inv Heq.
        rewrite Heq. apply Hspt. eapply smmu_iso0; eassumption.
      * intro. destruct_zmap. simpl; intros.
        rewrite <- C0. eapply smmu_count0; eassumption. eapply smmu_count0.
      * pose proof (host_npt_cons0 _ _ _ _ C1). rewrite H. reflexivity.
    + pose proof (local_mmap_level3 _ _ _ _ _ C3).
      constructor; autounfold; simpl; try assumption.
      * intros until pte. rewrite ZMap.gss. rewrite H. destruct_zmap.
        intro T. inv T. reflexivity. apply host_npt_cons0.
      * intros until pte. rewrite ZMap.gss. rewrite H. destruct_zmap.
        replace (phys_page 144115188075855872 / PAGE_SIZE) with 0 by reflexivity.
        intros. inv H0. contra. apply host_flatmap0.
      * intro. destruct_zmap. simpl. intros; omega. apply host_s2_map0.
      * assert_gso. red; intro T. rewrite T in page_0_invalid0. omega.
        rewrite (ZMap.gso _ _ Hneq). assumption.
      * rewrite ZMap.gss. rewrite H. intros until pte.
        replace (phys_page 144115188075855872 / PAGE_SIZE) with 0 by reflexivity.
        destruct_zmap. intros. inv Hpfn. contra.
        intros. autounfold in *. assert_gso. red; intro.
        inv H0. pose proof (host_flatmap0 _ _ _ _ Hpfn Hexists). inv H0.
        apply Heq. rewrite Z_div_mult_full. reflexivity. omega.
        rewrite (ZMap.gso _ _ Hneq). eapply host_iso0; eassumption.
      * intros. destruct_zmap. rewrite Heq in *.
        assert_gsoH H0. red; intro; srewrite; omega. rewrite (ZMap.gso _ _ Hneq) in H0.
        exploit (vm_iso0 _ _ _ _ _ H0); try eassumption. omega. intros.
        rewrite C in H5. omega.
        assert_gsoH H0. red; intro; srewrite; omega. rewrite (ZMap.gso _ _ Hneq) in H0.
        rewrite (ZMap.gso _ _ Heq) in H4. eapply vm_iso0; eassumption.
      * intros. destruct_zmap. simpl. rewrite Heq in *.
        exploit (smmu_iso0 vmid0 cbndx index gfn0 pfn pte); try eassumption.
        intros (? & ?). srewrite. eapply Hcount0 in Heq; try eassumption. inv Heq.
        rewrite Heq. apply Hspt. eapply smmu_iso0; eassumption.
      * intro. destruct_zmap. simpl; intros.
        rewrite <- C0. eapply smmu_count0; eassumption. eapply smmu_count0.
  - rewrite zmap_set_id. destruct s; simpl in *. assumption.
Qed.

Lemma map_pfn_vm_inv:
  forall vmid addr pte level s s' a
    (ex: local_map_pfn_vm vmid addr pte level s = (s', false, a))
    (Howner: forall pfn, (if level =? 2 then phys_page pte / PAGE_SIZE <= pfn < phys_page pte / PAGE_SIZE + 512
                     else pfn = phys_page pte / PAGE_SIZE) -> s2_owner (pfn @ (s2page s)) = vmid)
    (valid_vm: valid_vm vmid),
    shared_inv s -> shared_inv s'.
Proof.
  Local Transparent Z.sub.
  intros. hsimpl_func ex; bool_rel; try assumption.
  duplicate H; destruct H; autounfold in *.
  assert(Hnhost: 0 <> vmid) by omega.
  constructor; autounfold; simpl; repeat rewrite (ZMap.gso _ _ Hnhost); try assumption.
  intros until pte0. destruct_zmap; try eapply vm_iso0. inv Heq.
  intros. destruct (level =? 2) eqn:Hlevel.
  - pose proof (local_mmap_level2 _ _ _ _ _ C gfn) as Hn.
    rewrite vm_pte_pfn_level2 in Hn.
    destruct in_range_n in Hn. rewrite H in Hn. inv Hn. simpl.
    apply Howner. autounfold in *. omega. rewrite Hn in H.
    eapply vm_iso0; try eassumption.
  - pose proof (local_mmap_level3 _ _ _ _ _ C) as Hn.
    rewrite Hn in H. destruct (gfn =? addr / PAGE_SIZE) eqn:Hsame.
    bool_rel. rewrite Hsame in H. rewrite ZMap.gss in H. inv H.
    rewrite vm_pte_pfn_level3 in *. apply Howner; reflexivity.
    bool_rel. rewrite (ZMap.gso _ _ Hsame) in H.
    eapply vm_iso0; eassumption.
Qed.

Lemma map_io_inv:
  forall vmid gpa pa s s' a b c
    (ex: local_map_io vmid gpa pa s = (s', false, a, b, c))
    (valid_addr: valid_paddr pa)
    (valid_vm': valid_vm vmid),
    shared_inv s -> shared_inv s'.
Proof.
  intros; hsimpl_func ex; try assumption; destruct H; autounfold in *.
  assert(Hnhost: 0 <> vmid) by omega.
  constructor; autounfold; simpl; repeat rewrite (ZMap.gso _ _ Hnhost); try assumption.
  intros until pte. destruct_zmap; try eapply vm_iso0. inv Heq.
  intros. rewrite (local_mmap_level3 _ _ _ _ _ C1) in H.
  destruct (gfn =? gpa / PAGE_SIZE) eqn:Hsame; bool_rel; subst.
  rewrite ZMap.gss in H. inv H.
  rewrite vm_pte_pfn_dev in H3; try assumption. autounfold in H3; omega.
  rewrite (ZMap.gso _ _ Hsame) in H. eapply vm_iso0; eassumption.
Qed.

Lemma grant_vm_page_inv:
  forall vmid pfn s s' a
    (ex: local_grant_vm_page vmid pfn s = (s', a))
    (valid_vm': valid_vm vmid),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex. destruct_if.
  - bool_rel_all. destruct H; autounfold in *.
    constructor; autounfold; simpl; try assumption.
    + intro pfn0. destruct_zmap. inv Heq. simpl. intros. omega.
      eapply host_s2_map0; eassumption.
    + destruct_zmap. inv Heq. omega. assumption.
    + intros until pte. destruct_zmap. inv Heq.
      intros. pose proof (host_iso0 _ _ _ _ Hpfn Hexists).
      simpl. omega. apply host_iso0.
    + intros until pte. destruct_zmap. inv Heq.
      simpl. apply vm_iso0. apply vm_iso0.
    + intros until pte. destruct_zmap. inv Heq. simpl.
      apply smmu_iso0. apply smmu_iso0.
    + intro. destruct_zmap. inv Heq. simpl. intros. omega.
      apply smmu_count0.
  - destruct s; simpl in *; assumption.
Qed.

Lemma revoke_vm_page_inv:
  forall vmid pfn dorc logn s s' a b c n
    (ex: local_revoke_vm_page vmid pfn dorc logn s = (s', false, n, a, b, c))
    (valid_vm': valid_vm vmid),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex.
  - destruct H; autounfold in *.
    destruct (z =? 0) eqn:Hz; bool_rel_all.
    + inv C3. rewrite zmap_set_id.
      constructor; autounfold; simpl; try assumption.
      * intro pfn0. destruct_zmap. inv Heq. simpl. intros. omega.
        eapply host_s2_map0; eassumption.
      * destruct_zmap. inv Heq. omega. assumption.
      * intros until pte. destruct_zmap. intros.
        simpl. pose proof (host_flatmap0 _ _ _ _ Hpfn Hexists).
        inv H. pose proof (host_npt_cons0 _ _ _ _ C1).
        rewrite C1 in Hpfn. inv Hpfn.
        replace (phys_page 0 / 4096) with 0 in H1 by reflexivity. omega.
        apply host_iso0.
      * intros until pte. destruct_zmap. inv Heq.
        simpl. apply vm_iso0. apply vm_iso0.
      * intros until pte. destruct_zmap. inv Heq. simpl.
        apply smmu_iso0. apply smmu_iso0.
      * intro. destruct_zmap. inv Heq. simpl. intros. omega.
        apply smmu_count0.
    + pose proof (local_mmap_level3 _ _ _ _ _ C3) as Hn.
      constructor; autounfold; simpl; try assumption.
      * rewrite ZMap.gss. intros until pte. rewrite Hn.
        destruct_zmap. intros. inv H. reflexivity.
        apply host_npt_cons0.
      * rewrite ZMap.gss. intros until pte. rewrite Hn.
        destruct_zmap. intros. inv H.
        replace (phys_page 144115188075855872 / PAGE_SIZE) with 0 in H0 by reflexivity.
        contra. apply host_flatmap0.
      * intro pfn0. destruct_zmap. simpl. intros; omega.
        eapply host_s2_map0; eassumption.
      * destruct_zmap. simpl. rewrite <- Heq. eapply page_0_invalid0. assumption.
      * rewrite ZMap.gss. rewrite Hn. intros until pte.
        destruct_zmap. intros. inv Hpfn.
        replace (phys_page 144115188075855872 / PAGE_SIZE) with 0 in Hexists by reflexivity.
        contra. intros. pose proof (host_flatmap0 _ _ _ _ Hpfn Hexists).
        rewrite Z_div_mult_full in Heq. rewrite H in Heq. rewrite (ZMap.gso _ _ Heq).
        eapply host_iso0; eassumption. autounfold; omega.
      * intros until pte. intros. assert_gsoH H. red; intro; srewrite; omega.
        rewrite (ZMap.gso _ _ Hneq) in H.
        destruct_zmap. inv Heq. simpl. eapply vm_iso0; try eassumption.
        rewrite ZMap.gss in H3. simpl in H3. assumption.
        eapply vm_iso0; try eassumption. rewrite (ZMap.gso _ _ Heq) in H3. assumption.
      * intros until pte. destruct_zmap. inv Heq. simpl.
        apply smmu_iso0. apply smmu_iso0.
      * intro. destruct_zmap. inv Heq. simpl. intros. omega.
        apply smmu_count0.
  - bool_rel_all. destruct H; autounfold in *.
    constructor; autounfold; simpl; try assumption.
    + intro pfn0. destruct_zmap. inv Heq. simpl. intros. omega.
      eapply host_s2_map0; eassumption.
    + destruct_zmap. inv Heq. omega. assumption.
    + intros until pte. destruct_zmap. inv Heq.
      intros. pose proof (host_iso0 _ _ _ _ Hpfn Hexists).
      simpl. omega. apply host_iso0.
    + intros until pte. destruct_zmap. inv Heq.
      simpl. apply vm_iso0. apply vm_iso0.
    + intros until pte. destruct_zmap. inv Heq. simpl.
      apply smmu_iso0. apply smmu_iso0.
    + intro. destruct_zmap. inv Heq. simpl. intros. omega.
      apply smmu_count0.
  - assumption.
Qed.

Lemma set_vcpu_active_inv:
  forall vmid vcpuid s s' a
    (ex: local_set_vcpu_active vmid vcpuid s = (s', false, a)),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex. destruct H.
  constructor; simpl; try assumption.
  intros until pte. destruct_zmap; simpl; apply vm_iso0.
  intros until pte. destruct_zmap; simpl; apply smmu_iso0.
Qed.

Lemma register_vcpu_inv:
  forall vmid vcpuid s s' a
    (ex: local_register_vcpu vmid vcpuid s = (s', false, a)),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex. destruct H.
  constructor; simpl; try assumption.
  intros until pte. destruct_zmap; simpl; apply vm_iso0.
  intros until pte. destruct_zmap; simpl; apply smmu_iso0.
Qed.

Lemma gen_vmid_inv:
  forall s s' a
    (ex: local_gen_vmid s = (s', false, a)),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex. destruct H.
  constructor; simpl; try assumption.
Qed.

Lemma register_kvm_inv:
  forall vmid s s' a
    (ex: local_register_kvm vmid s = (s', false, a)),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex. destruct H.
  constructor; simpl; try assumption.
  intros until pte. destruct_zmap; simpl.
  intros. eapply vm_iso0; try eassumption. rewrite C. omega.
  apply vm_iso0.
  intros until pte. destruct_zmap; simpl.
  intros. eapply smmu_iso0; try eassumption. rewrite C.
  autounfold in *; bool_rel; omega.
  apply smmu_iso0.
Qed.

Lemma set_boot_info_inv:
  forall vmid load_addr size s s' a b
    (ex: local_set_boot_info vmid load_addr size s = (s', false, a, b)),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex. destruct H.
  constructor; simpl; try assumption.
  intros until pte. destruct_zmap; simpl; apply vm_iso0.
  intros until pte. destruct_zmap; simpl; apply smmu_iso0.
  assumption.
Qed.

Lemma remap_vm_image_inv:
  forall vmid pfn load_idx s s' a b
    (ex: local_remap_vm_image vmid pfn load_idx s = (s', false, a, b)),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex. destruct H; autounfold in *.
  assert(0 <> 16) by omega.
  constructor; autounfold; simpl; try rewrite (ZMap.gso _ _ H); try assumption.
  intros until pte. intros ? ?. assert_gsoH H0.
  red; intro; srewrite; omega. rewrite (ZMap.gso _ _ Hneq) in H0.
  destruct_zmap; simpl; eapply vm_iso0; try eassumption.
  rewrite Heq in H0; eassumption. omega.
  intros until pte. destruct_zmap; simpl; apply smmu_iso0.
  assumption. assumption.
Qed.

Lemma smmu_assign_page_inv:
  forall vmid cbndx index pfn gfn s s' a b c d
    (ex: local_smmu_assign_page cbndx index pfn gfn s = (s', false, a, b, c, d))
    (valid_cbndx: valid_smmu_cfg cbndx)
    (valid_index: valid_smmu index)
    (Hvm: valid_vm vmid),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex; try assumption; bool_rel_all.
  pose proof (smmu_count_0_no_map _ H _ C2 C3) as Hcount0.
  destruct H; autounfold in *.
  destruct (z =? 0) eqn:Hz; bool_rel_all.
  - inv C6. rewrite zmap_set_id.
    constructor; autounfold; simpl; try assumption.
    + intro pfn0. destruct_zmap. inv Heq. simpl. intros. omega.
      eapply host_s2_map0; eassumption.
    + destruct_zmap. inv Heq. omega. assumption.
    + intros until pte. destruct_zmap. intros.
      simpl. pose proof (host_flatmap0 _ _ _ _ Hpfn Hexists).
      inv H. pose proof (host_npt_cons0 _ _ _ _ C4).
      rewrite C4 in Hpfn. inv Hpfn.
      replace (phys_page 0 / 4096) with 0 in H1 by reflexivity. omega.
      apply host_iso0.
    + intros until pte. destruct_zmap. simpl.
      intros. exploit vm_iso0; try eassumption. omega.
      intros. omega. apply vm_iso0.
    + intros until pte. destruct_zmap. simpl.
      intros. exploit smmu_iso0; try eassumption.
      intros (? & ?). srewrite.
      exploit Hcount0; try eassumption. reflexivity. intros. inv H2.
      apply smmu_iso0.
    + intro. destruct_zmap. simpl. intros.
      pose proof (smmu_count0 _ C2). rewrite C3 in H0. omega.
      apply smmu_count0.
  - pose proof (local_mmap_level3 _ _ _ _ _ C6) as Hn.
    constructor; autounfold; simpl; try assumption.
    + rewrite ZMap.gss. intros until pte. rewrite Hn.
      destruct_zmap. intros. inv H. reflexivity.
      apply host_npt_cons0.
    + rewrite ZMap.gss. intros until pte. rewrite Hn.
      destruct_zmap. intros. inv H.
      replace (phys_page 144115188075855872 / PAGE_SIZE) with 0 in H0 by reflexivity.
      contra. apply host_flatmap0.
    + intro pfn0. destruct_zmap. simpl. intros; omega.
      eapply host_s2_map0; eassumption.
    + destruct_zmap. inv Heq. omega. assumption.
    + rewrite ZMap.gss. rewrite Hn. intros until pte.
      destruct_zmap. intros. inv Hpfn.
      replace (phys_page 144115188075855872 / PAGE_SIZE) with 0 in Hexists by reflexivity.
      contra. intros. pose proof (host_flatmap0 _ _ _ _ Hpfn Hexists).
      rewrite Z_div_mult_full in Heq. rewrite H in Heq. rewrite (ZMap.gso _ _ Heq).
      eapply host_iso0; eassumption. autounfold; omega.
    + intros until pte. intros ? ?.  assert_gsoH H. red; intro; srewrite; omega.
      rewrite (ZMap.gso _ _ Hneq) in H.
      destruct_zmap. simpl.
      intros. exploit vm_iso0; try eassumption. omega. rewrite Heq. omega.
      intros. rewrite Heq in H4. omega. eapply vm_iso0; try eassumption.
    + intros until pte. destruct_zmap. simpl. intros.
      exploit smmu_iso0; try eassumption. intros (? & ?).
      srewrite. pose proof (Hcount0 _ _ Hvalid_smmu Hvalid_cfg Hsmmu _ _ _ Hspt).
      contra. apply smmu_iso0.
    + intro. destruct_zmap. inv Heq. simpl. intros. omega.
      apply smmu_count0.
Qed.

Lemma smmu_map_page_inv:
  forall cbndx index iova pte s s' a b c d
    (ex: local_smmu_map_page cbndx index iova pte s = (s', false, a, b, c, d))
    (valid_cbndx: valid_smmu_cfg cbndx)
    (valid_index: valid_smmu index),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex; try assumption.
  apply andb_true_iff in C1. destruct C1 as (C10 & C11). bool_rel.
  pose proof (local_spt_map_pt _ _ _ _ _ _ C2) as Hn.
  destruct_if. apply andb_true_iff in Case. destruct Case; bool_rel.
  - destruct H; autounfold in *.
    constructor; autounfold; simpl; try assumption.
    + rewrite Hn. intros until pte0. destruct_zmap.
      destruct_zmap. intros. inv H3. reflexivity.
      rewrite <- Heq. eapply spt_cons0; eassumption.
      apply spt_cons0.
    + intro. destruct_zmap. simpl.
      intros. eapply host_s2_map0; try eassumption. apply host_s2_map0.
    + destruct_zmap. simpl. rewrite <- Heq. assumption. assumption.
    + intros until pte0. destruct_zmap. simpl. intros. auto.
      apply host_iso0.
    + intros until pte0. destruct_zmap. simpl. intros.
      exploit vm_iso0; try eassumption. intros. omega.
      apply vm_iso0.
    + intros until pte0. rewrite Hn. destruct_zmap.
      destruct_zmap. intros. inv Hspt. rewrite ZMap.gss.
      simpl. rewrite H0 in *.
      split. assert((index0 * 8 + cbndx0) = (index * 8 + cbndx)) by omega.
      rewrite H2. rewrite C10. reflexivity. rewrite C11. reflexivity.
      intros. assert((index0 * 8 + cbndx0) = (index * 8 + cbndx)) by omega.
      rewrite <- H2 in Hspt.
      exploit smmu_iso0; try eassumption. intros (? & ?).
      destruct_zmap. simpl. srewrite. auto. auto.
      intros. exploit smmu_iso0; try eassumption. intros (? & ?).
      destruct_zmap. simpl. srewrite. auto. auto.
    + intro. destruct_zmap. simpl. intros. pose proof (smmu_count0 _ H).
      Local Transparent count_smmu_map.
      assert(forall n, (Z.of_nat n <= smmu_id index cbndx) ->
                  count_smmu_map n (phys_page pte / 4096) (smmu_vmid s) s0 =
                  count_smmu_map n (phys_page pte / 4096) (smmu_vmid s) (spts s)).
      { induction n. reflexivity.
        rewrite Nat2Z.inj_succ, succ_plus_1. intros.
        simpl; autounfold in *. rewrite Hn. assert_gso.
        replace (Z.of_nat n / 8 * 8) with (8 * (Z.of_nat n / 8)) by apply Z.mul_comm.
        rewrite <- Z_div_mod_eq. omega. omega. rewrite (ZMap.gso _ _ Hneq).
        rewrite IHn. reflexivity. omega. }
      pose proof (host_s2_map0 _ H0).
      assert(forall n, (Z.of_nat n > smmu_id index cbndx) ->
                  count_smmu_map n (phys_page pte / 4096) (smmu_vmid s) s0 <=
                  count_smmu_map n (phys_page pte / 4096) (smmu_vmid s) (spts s) + 1).
      { induction n. intros. autounfold in *. simpl in H5. omega.
        rewrite Nat2Z.inj_succ, succ_plus_1. intros.
        destruct (smmu_id index cbndx =? Z.of_nat n) eqn:Hsame. bool_rel.
        simpl; autounfold in *. rewrite Hn.
        replace (Z.of_nat n / 8 * 8) with (8 * (Z.of_nat n / 8)) by apply Z.mul_comm.
        rewrite <- Z_div_mod_eq.
        rewrite <- Hsame. rewrite ZMap.gss. simpl.
        srewrite. rewrite ZMap.gss. rewrite <- Heq.
        destruct_if. bool_rel. srewrite. omega. simpl_bool_eq.
        srewrite. rewrite H3. match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        destruct_if; omega. omega. omega.
        bool_rel. simpl. autounfold in *.
        replace (Z.of_nat n / 8 * 8) with (8 * (Z.of_nat n / 8)) by apply Z.mul_comm.
        rewrite <- Z_div_mod_eq. rewrite Hn. assert_gso. omega. rewrite (ZMap.gso _ _ Hneq).
        match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        repeat destruct_if. apply IHn. omega.
        assert(Z.of_nat n > index * 8 + cbndx) by omega. apply IHn in H6. omega.
        apply IHn. omega. omega. }
      pose proof (H5 16%nat). replace (Pos.to_nat 16) with (16%nat) by reflexivity.
      assert(Z.of_nat 16 > smmu_id index cbndx). autounfold; simpl; omega.
      apply H6 in H7. replace (Z.to_nat 16) with 16%nat in H2 by reflexivity. omega.
      pose proof (host_s2_map0 _ H0). srewrite.
      assert(forall n, (Z.of_nat n <= EL2_SMMU_CFG_SIZE) ->
                  count_smmu_map n pfn (smmu_vmid s) s0 =
                  count_smmu_map n pfn (smmu_vmid s) (spts s)).
      { induction n. reflexivity.
        rewrite Nat2Z.inj_succ, succ_plus_1. intros.
        simpl. autounfold in *. rewrite Hn.
        replace (Z.of_nat n / 8 * 8) with (8 * (Z.of_nat n / 8)) by apply Z.mul_comm.
        rewrite <- Z_div_mod_eq. destruct_zmap.
        assert_gso. omega. rewrite (ZMap.gso _ _ Hneq). rewrite IHn. reflexivity.
        omega. rewrite IHn. reflexivity. omega. omega. }
      rewrite H2. apply smmu_count0. autounfold; simpl. omega.
      Local Opaque count_smmu_map.
  - destruct H; autounfold in *.
    constructor; autounfold; simpl.
    + rewrite Hn. intros until pte0. destruct_zmap.
      destruct_zmap. intros. inv H1. reflexivity.
      rewrite <- Heq. eapply spt_cons0; eassumption.
      apply spt_cons0.
    + assumption. + assumption. + assumption. + assumption.
    + assumption. + assumption. + assumption.
    + rewrite Hn. intros until pte0. destruct_zmap.
      destruct_zmap. intros. inv Hspt.
      assert(index0 * 8 + cbndx0 = index * 8 + cbndx) by omega.
      srewrite. auto.
      assert(index0 * 8 + cbndx0 = index * 8 + cbndx) by omega.
      rewrite <- H. apply smmu_iso0. apply smmu_iso0.
    + intro. destruct (zeq pfn (phys_page pte / 4096)).
      srewrite. intros. assert(s2_count (phys_page pte / 4096) @ (s2page s) >= 16).
      bool_rel_all; omega.
      Local Transparent count_smmu_map.
      assert(forall n pfn a b, count_smmu_map n pfn a b <= Z.of_nat n).
      { induction n. intros. simpl. omega.
        intros. rewrite Nat2Z.inj_succ, succ_plus_1. intros.
        simpl. match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        pose proof (IHn pfn0 a b).
        repeat destruct_if; omega. }
      pose proof (H1 (Pos.to_nat 16) (phys_page pte / 4096) (smmu_vmid s) s0).
      replace (Z.of_nat (Pos.to_nat 16)) with 16 in H2 by reflexivity. omega.
      intros. pose proof (host_s2_map0 _ H).
      assert(forall n, (Z.of_nat n <= EL2_SMMU_CFG_SIZE) ->
                  count_smmu_map n pfn (smmu_vmid s) s0 =
                  count_smmu_map n pfn (smmu_vmid s) (spts s)).
      { induction n0. reflexivity.
        rewrite Nat2Z.inj_succ, succ_plus_1. intros.
        simpl. autounfold in *. rewrite Hn.
        replace (Z.of_nat n0 / 8 * 8) with (8 * (Z.of_nat n0 / 8)) by apply Z.mul_comm.
        rewrite <- Z_div_mod_eq. destruct_zmap.
        assert(Z.of_nat n0 = index * 8 + cbndx) by omega. rewrite H2.
        destruct_zmap.
        assert((index * 8 + cbndx) @ (smmu_vmid s) =? 0 = false).
        bool_rel. red; intro T. rewrite T in C10. symmetry in C10.
        pose proof (host_s2_map0 _ C10). srewrite. omega. rewrite H3.
        match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        repeat destruct_if; apply IHn0; omega. rewrite IHn0. reflexivity. omega.
        rewrite IHn0. reflexivity. omega. omega. }
      rewrite H1. apply smmu_count0. assumption. autounfold; simpl. omega.
      Local Opaque count_smmu_map.
Qed.

Lemma smmu_clear_inv:
  forall iova cbndx index s s' a b c d
    (ex: local_smmu_clear iova cbndx index s = (s', false, a, b, c, d))
    (valid_cbndx: valid_smmu_cfg cbndx)
    (valid_index: valid_smmu index),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex; try assumption.
  destruct_if. apply andb_true_iff in Case. destruct Case; bool_rel.
  - destruct H; autounfold in *.
    constructor; autounfold; simpl; try assumption.
    + destruct (z0 =? 0) eqn:Hz; bool_rel. inv C2. apply spt_cons0.
      rewrite (local_spt_map_pt _ _ _ _ _ _ C2). intros until pte.
      destruct_zmap. destruct_zmap. intros. inv H3. reflexivity.
      rewrite <- Heq. eapply spt_cons0; eassumption. apply spt_cons0.
    + intro. destruct_zmap. simpl.
      intros. eapply host_s2_map0; try eassumption. apply host_s2_map0.
    + destruct_zmap. simpl. rewrite <- Heq. assumption. assumption.
    + intros until pte. destruct_zmap. simpl. intros. auto.
      apply host_iso0.
    + intros until pte. destruct_zmap. simpl. intros.
      exploit vm_iso0; try eassumption. intros. omega.
      apply vm_iso0.
    + intros until pte.
      destruct (z0 =? 0) eqn:Hz; bool_rel. inv C2.
      intros. destruct_zmap. simpl. replace (phys_page 0 / 4096) with 0 in Heq by reflexivity.
      contra. eapply smmu_iso0; try eassumption.
      rewrite (local_spt_map_pt _ _ _ _ _ _ C2). destruct_zmap.
      destruct_zmap. intros. inv Hspt.
      replace (phys_page 0 / PAGE_SIZE) with 0 in H by reflexivity. contra.
      intros. destruct_zmap. simpl.
      autounfold in *.
      assert((index0 * 8 + cbndx0) = (index * 8 + cbndx)) by omega.
      rewrite <- H2 in Hspt. rewrite Heq1 in Hspt.
      eapply smmu_iso0; try eassumption. omega.
      autounfold in *.
      assert((index0 * 8 + cbndx0) = (index * 8 + cbndx)) by omega.
      rewrite <- H2 in Hspt.
      eapply smmu_iso0; try eassumption.
      destruct_zmap. simpl. intros.
      eapply smmu_iso0; try eassumption.
      eapply smmu_iso0; try eassumption.
    + intro. destruct_zmap. simpl. intros. pose proof (smmu_count0 _ H).
      Local Transparent count_smmu_map.
      destruct (z0 =? 0) eqn:Hz; bool_rel. srewrite.
      replace (phys_page 0 / 4096) with 0 in H by reflexivity. omega.
      pose proof (local_spt_map_pt _ _ _ _ _ _ C2) as Hn.
      assert(forall n, (Z.of_nat n <= smmu_id index cbndx) ->
                  count_smmu_map n (phys_page z0 / 4096) (smmu_vmid s) s0 =
                  count_smmu_map n (phys_page z0 / 4096) (smmu_vmid s) (spts s)).
      { induction n. reflexivity.
        rewrite Nat2Z.inj_succ, succ_plus_1. intros.
        simpl; autounfold in *. rewrite Hn. assert_gso.
        replace (Z.of_nat n / 8 * 8) with (8 * (Z.of_nat n / 8)) by apply Z.mul_comm.
        rewrite <- Z_div_mod_eq. omega. omega. rewrite (ZMap.gso _ _ Hneq).
        rewrite IHn. reflexivity. omega. }
      pose proof (host_s2_map0 _ H0).
      assert(forall n, (Z.of_nat n > smmu_id index cbndx) ->
                  count_smmu_map n (phys_page z0 / 4096) (smmu_vmid s) s0 <=
                  count_smmu_map n (phys_page z0 / 4096) (smmu_vmid s) (spts s) - 1).
      { induction n. intros. autounfold in *. simpl in H5. omega.
        rewrite Nat2Z.inj_succ, succ_plus_1. intros.
        destruct (smmu_id index cbndx =? Z.of_nat n) eqn:Hsame. bool_rel.
        simpl; autounfold in *. rewrite Hn.
        replace (Z.of_nat n / 8 * 8) with (8 * (Z.of_nat n / 8)) by apply Z.mul_comm.
        rewrite <- Z_div_mod_eq.
        rewrite <- Hsame in *. rewrite ZMap.gss. simpl.
        remember ((index * 8 + cbndx) @ (smmu_vmid s)) as vmid0.
        symmetry in Heqvmid0. exploit (smmu_vm0 cbndx index); try eassumption.
        srewrite. assumption. intros.
        exploit spt_cons0; try eapply C1; try eassumption. intros.
        exploit smmu_iso0; try eapply C1; try eassumption.
        destruct (zeq vmid0 0). auto. right. split. omega.
        replace (0 <? vmid0) with true in C0 by (symmetry; bool_rel; omega).
        replace (vmid0 <? 16) with true in C0 by (symmetry; bool_rel; omega).
        simpl in C0. bool_rel. omega. intro. srewrite. inversion H7.
        intros (? & ?). srewrite. rewrite <- H9. rewrite ZMap.gss. rewrite <- Heq.
        replace (phys_page 0 / 4096 =? 0) with true by reflexivity.
        rewrite Heq. rewrite H9. rewrite C1.
        destruct_if. bool_rel. srewrite. inversion page_0_invalid0.
        rewrite H3. omega. omega. rewrite <- H8. simpl_bool_eq.
        rewrite H3. omega. omega. omega. bool_rel.
        simpl. autounfold in *.
        replace (Z.of_nat n / 8 * 8) with (8 * (Z.of_nat n / 8)) by apply Z.mul_comm.
        rewrite <- Z_div_mod_eq. rewrite Hn. assert_gso. omega. rewrite (ZMap.gso _ _ Hneq).
        match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        repeat destruct_if. apply IHn. omega.
        assert(Z.of_nat n > index * 8 + cbndx) by omega. apply IHn in H6. omega.
        apply IHn. omega. omega. }
      pose proof (H5 16%nat). replace (Pos.to_nat 16) with (16%nat) by reflexivity.
      assert(Z.of_nat 16 > smmu_id index cbndx). autounfold; simpl; omega.
      apply H6 in H7. replace (Z.to_nat 16) with 16%nat in H2 by reflexivity. omega.
      destruct (z0 =? 0) eqn:Hz; bool_rel.
      inv C2. apply smmu_count0.
      pose proof (local_spt_map_pt _ _ _ _ _ _ C2) as Hn.
      pose proof (host_s2_map0 _ H0). srewrite.
      assert(forall n, (Z.of_nat n <= EL2_SMMU_CFG_SIZE) ->
                  count_smmu_map n pfn (smmu_vmid s) s0 =
                  count_smmu_map n pfn (smmu_vmid s) (spts s)).
      { induction n. reflexivity.
        rewrite Nat2Z.inj_succ, succ_plus_1. intros.
        simpl. autounfold in *. rewrite Hn.
        replace (Z.of_nat n / 8 * 8) with (8 * (Z.of_nat n / 8)) by apply Z.mul_comm.
        rewrite <- Z_div_mod_eq. destruct_zmap.
        remember ((index * 8 + cbndx) @ (smmu_vmid s)) as vmid0.
        symmetry in Heqvmid0. exploit (smmu_vm0 cbndx index); try eassumption.
        srewrite. assumption. intros.
        exploit spt_cons0; try eapply C1; try eassumption. intros.
        exploit smmu_iso0; try eapply C1; try eassumption.
        destruct (zeq vmid0 0). auto. right. split. omega.
        replace (0 <? vmid0) with true in C0 by (symmetry; bool_rel; omega).
        replace (vmid0 <? 16) with true in C0 by (symmetry; bool_rel; omega).
        simpl in C0. bool_rel. omega. intro. srewrite. inversion H4.
        intros (? & ?). srewrite. assert_gso. omega.
        rewrite (ZMap.gso _ _ Hneq). rewrite IHn. reflexivity.
        omega. rewrite IHn. reflexivity. omega. omega. }
      rewrite H2. apply smmu_count0. autounfold; simpl. omega.
      Local Opaque count_smmu_map.
  - destruct H; autounfold in *.
    constructor; autounfold; simpl.
    + destruct (z0 =? 0) eqn:Hz; bool_rel. inv C2. apply spt_cons0.
      rewrite (local_spt_map_pt _ _ _ _ _ _ C2). intros until pte.
      destruct_zmap. destruct_zmap. intros. inv H1. reflexivity.
      rewrite <- Heq. eapply spt_cons0; eassumption. apply spt_cons0.
    + assumption. + assumption. + assumption. + assumption.
    + assumption. + assumption. + assumption.
    + destruct (z0 =? 0) eqn:Hz; bool_rel. inv C2. apply smmu_iso0.
      pose proof (local_spt_map_pt _ _ _ _ _ _ C2) as Hn.
      rewrite Hn. intros until pte. destruct_zmap.
      destruct_zmap. intros. inv Hspt.
      replace (phys_page 0 / PAGE_SIZE) with 0 in H by reflexivity.
      contra. rewrite <- Heq. eapply smmu_iso0; eassumption. apply smmu_iso0.
    + destruct (z0 =? 0) eqn:Hz; bool_rel. inv C2. assumption.
      pose proof (local_spt_map_pt _ _ _ _ _ _ C2) as Hn.
      intros. destruct (zeq pfn (phys_page z0 / 4096)).
      srewrite. intros. assert(s2_count (phys_page z0 / 4096) @ (s2page s) <= 0).
      bool_rel_all; omega.
      pose proof (smmu_count0 _ H).
      Local Transparent count_smmu_map.
      assert(forall n, count_smmu_map n (phys_page z0 / 4096) (smmu_vmid s) s0 <=
                  count_smmu_map n (phys_page z0 / 4096) (smmu_vmid s) (spts s)).
      { induction n. simpl. omega.
        simpl. rewrite Hn. destruct_zmap. destruct_zmap.
        replace (phys_page 0 / PAGE_SIZE =? 0) with true by reflexivity.
        match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        repeat destruct_if; omega.
        repeat match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        repeat destruct_if; omega.
        repeat match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        repeat destruct_if; omega. }
      pose proof (H2 (Z.to_nat 16)). replace (Pos.to_nat 16) with (Z.to_nat 16) by reflexivity.
      omega.
      pose proof (host_s2_map0 _ H).
      assert(forall n, (Z.of_nat n <= EL2_SMMU_CFG_SIZE) ->
                  count_smmu_map n pfn (smmu_vmid s) s0 <=
                  count_smmu_map n pfn (smmu_vmid s) (spts s)).
      { induction n0. reflexivity.
        rewrite Nat2Z.inj_succ, succ_plus_1. intros.
        simpl. autounfold in *. rewrite Hn.
        replace (Z.of_nat n0 / 8 * 8) with (8 * (Z.of_nat n0 / 8)) by apply Z.mul_comm.
        rewrite <- Z_div_mod_eq. destruct_zmap.
        assert(Z.of_nat n0 = index * 8 + cbndx) by omega. rewrite H2.
        destruct_zmap. replace (phys_page 0 / 4096 =? 0) with true by reflexivity.
        rewrite C1. rewrite IHn0. repeat destruct_if; try reflexivity. omega. omega.
        repeat match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        repeat destruct_if; omega.
        repeat match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        repeat destruct_if; omega. omega. }
      assert(Z.of_nat (Pos.to_nat 16) <= EL2_SMMU_CFG_SIZE).
      simpl. autounfold. omega. apply H1 in H2.
      pose proof (smmu_count0 _ H).
      replace (Pos.to_nat 16) with (Z.to_nat 16) in * by reflexivity.
      omega.
      Local Opaque count_smmu_map.
Qed.

Lemma free_smmu_pgd_inv:
  forall cbndx index s s' a b
    (ex: local_free_smmu_pgd cbndx index s = (s', false, a, b))
    (valid_cbndx: valid_smmu_cfg cbndx)
    (valid_index: valid_smmu index),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex. assumption.
  destruct H. constructor; autounfold in *; simpl; try assumption.
  - intros. destruct_zmap. srewrite. rewrite ZMap.gss in H. contra.
    eapply smmu_vm0; try eassumption. rewrite (ZMap.gso _ _ Heq) in H.
    assumption.
  - intros until pte. destruct_zmap. intros. omega.
    apply smmu_iso0.
  - intros.
      assert(forall n, (Z.of_nat n <= EL2_SMMU_CFG_SIZE) ->
                  count_smmu_map n pfn (smmu_vmid s) # index * 8 + cbndx == 4294967295 (spts s) <=
                  count_smmu_map n pfn (smmu_vmid s) (spts s)).
      { induction n. reflexivity.
        rewrite Nat2Z.inj_succ, succ_plus_1. intros.
        Local Transparent count_smmu_map.
        simpl; autounfold in *.
        destruct_zmap.
        repeat match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        repeat destruct_if; bool_rel; try omega.
        assert(Z.of_nat n <= 16) by omega. apply IHn in H1.
        repeat match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
        repeat destruct_if; omega.
        Local Opaque count_smmu_map. }
      assert(Z.of_nat (Pos.to_nat 16) <= EL2_SMMU_CFG_SIZE).
      simpl. autounfold. omega. apply H0 in H1.
      pose proof (smmu_count0 _ H).
      replace (Pos.to_nat 16) with (Z.to_nat 16) in * by reflexivity.
      omega.
Qed.

Lemma alloc_smmu_pgd_inv:
  forall cbndx vmid index num s s' a b c
    (ex: local_alloc_smmu_pgd cbndx vmid index num s = (s', false, a, b, c))
    (Hvmid: HOSTVISOR <= vmid < COREVISOR)
    (valid_cbndx: valid_smmu_cfg cbndx)
    (valid_index: valid_smmu index),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex; try assumption.
  destruct H. constructor; autounfold in *; simpl; try assumption.
  - intros until pte. destruct_zmap. rewrite ZMap.gi. intros. inv H1. reflexivity.
    apply spt_cons0.
  - intros. destruct_zmap. omega. apply smmu_vm0; try assumption.
    rewrite (ZMap.gso _ _ Heq) in H. assumption.
  - intros until pte. destruct_zmap. rewrite ZMap.gi. intros.
    inv Hspt. contra. intros. assert_gsoH Hspt. omega.
    rewrite (ZMap.gso _ _ Hneq) in Hspt. eapply smmu_iso0; eassumption.
  - intros.
    match goal with
    | |- _ >= count_smmu_map _ _ ?a ?b =>
      assert(forall n, (Z.of_nat n) <= EL2_SMMU_CFG_SIZE -> count_smmu_map n pfn a b <= count_smmu_map n pfn (smmu_vmid s) (spts s))
    end.
    { induction n. reflexivity.
      rewrite Nat2Z.inj_succ, succ_plus_1. intros.
      Local Transparent count_smmu_map.
      simpl; autounfold in *.
      replace (Z.of_nat n / 8 * 8) with (8 * (Z.of_nat n / 8)) by apply Z.mul_comm.
      rewrite <- Z_div_mod_eq.
      destruct_zmap.
      assert (Z.of_nat n = index * 8 + cbndx) by omega.
      rewrite H1 in *. rewrite ZMap.gi. simpl_bool_eq.
      repeat match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
      repeat destruct_if; bool_rel; try omega.
      assert (Z.of_nat n <> index * 8 + cbndx) by omega.
      rewrite (ZMap.gso _ _ H1).
      assert(Z.of_nat n <= 16) by omega. apply IHn in H2.
      repeat match goal with |- context[?a @ (?b @ ?c)] => destruct (a @ (b @ c)) end.
      repeat destruct_if; omega. omega.
      Local Opaque count_smmu_map. }
    assert(Z.of_nat (Pos.to_nat 16) <= EL2_SMMU_CFG_SIZE).
    simpl. autounfold. omega. apply H0 in H1.
    pose proof (smmu_count0 _ H).
    replace (Pos.to_nat 16) with (Z.to_nat 16) in * by reflexivity.
    omega.
Qed.

Lemma set_vm_poweroff_inv:
  forall vmid s s' a
    (ex: local_set_vm_poweroff vmid s = (s', a)),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex. destruct H; autounfold in *.
  constructor; autounfold; simpl; try assumption.
  - intros until pte. destruct_zmap. simpl. intros. omega.
    apply vm_iso0.
  - intros until pte. destruct_zmap. simpl. intros.
    eapply smmu_iso0; try eassumption. destruct Hvalid_vmid; omega.
    apply smmu_iso0.
Qed.

Lemma verify_vm_inv:
  forall vmid s s' a
    (ex: local_verify_vm vmid s = (s', false, a)),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex. destruct H; autounfold in *.
  constructor; autounfold; simpl; try assumption.
  - intros until pte. destruct_zmap. simpl. intros.
    eapply vm_iso0; try eassumption. omega.
    apply vm_iso0.
  - intros until pte. destruct_zmap. simpl. intros.
    eapply smmu_iso0; try eassumption. omega.
    apply smmu_iso0.
Qed.

Lemma load_encrypted_vcpu_inv:
  forall vmid vcpuid cregs cstates dorc logn s s' cr cs n' a
    (ex: local_load_encryted_vcpu vmid vcpuid cregs cstates dorc logn s = (s', false, cr, cs, n', a)),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex; destruct H; autounfold in *.
  constructor; autounfold; simpl; try assumption.
  - intros until pte. destruct_zmap. simpl. intros.
    eapply vm_iso0; try eassumption.
    apply vm_iso0.
  - intros until pte. destruct_zmap. simpl. intros.
    eapply smmu_iso0; try eassumption.
    apply smmu_iso0.
Qed.

Lemma load_save_encrypt_buf_inv:
  forall vmid inbuf outbuf dorc logn s s' n' a b
    (ex: local_save_encrypt_buf vmid inbuf outbuf dorc logn s = (s', false, n', a, b)),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex; destruct H; autounfold in *.
  constructor; autounfold; simpl; try assumption.
Qed.

Lemma load_load_decrypt_buf_inv:
  forall vmid inbuf dorc logn s s' n' a b c d
    (Hvalid_vm: valid_vm vmid)
    (ex: local_load_decrypt_buf vmid inbuf dorc logn s = (s', false, n', a, b, c, d)),
    shared_inv s -> shared_inv s'.
Proof.
  intros. hsimpl_func ex; bool_rel_all.
  pose proof (smmu_count_0_no_map _ H _ Hcond Hcond0) as Hcount0.
  destruct H; autounfold in *; bool_rel_all.
  destruct (z =? 0) eqn:Hz.
  - inv C3; bool_rel; srewrite.
    replace z0 with 0 in *.
    rewrite zmap_set_id.
    constructor; autounfold; simpl; try assumption.
    + intro. destruct_zmap. simpl. intros; omega. apply host_s2_map0.
    + assert_gso. red; intro T. rewrite T in page_0_invalid0. omega.
      rewrite (ZMap.gso _ _ Hneq). assumption.
    + intros. destruct_zmap. rewrite Heq in *.
      rewrite (host_flatmap0 _ _ _ _ Hpfn) in Hpfn. rewrite C1 in Hpfn. inv Hpfn.
      rewrite H0 in Hexists. contra. assumption. eapply host_iso0; try eassumption.
    + intros. destruct_zmap. rewrite Heq in *.
      exploit (vm_iso0 _ _ _ _ _ H); try eassumption. omega.
      intros. rewrite Hcond in H4. omega. rewrite (ZMap.gso _ _ Heq) in H3.
      eapply vm_iso0; eassumption.
    + intros. destruct_zmap. simpl. rewrite Heq in *.
      exploit (smmu_iso0 vmid0 cbndx index gfn pfn pte); try eassumption.
      rewrite Heq. assumption. omega.
      intros (? & ?). srewrite. eapply Hcount0 in Heq; try eassumption. inv Heq.
      rewrite H0. assumption. rewrite Heq. apply Hspt. eapply smmu_iso0; eassumption.
    + intro. destruct_zmap. simpl; intros.
      rewrite <- Hcond0. eapply smmu_count0; eassumption. eapply smmu_count0.
    + pose proof (host_npt_cons0 _ _ _ _ C1). rewrite H. reflexivity.
  - pose proof (local_mmap_level3 _ _ _ _ _ C3).
    constructor; autounfold; simpl; try assumption.
    + intros until pte. rewrite ZMap.gss. rewrite H. destruct_zmap.
      intro T. inv T. reflexivity. apply host_npt_cons0.
    + intros until pte. rewrite ZMap.gss. rewrite H. destruct_zmap.
      replace (phys_page 144115188075855872 / PAGE_SIZE) with 0 by reflexivity.
      intros. inv H0. contra. apply host_flatmap0.
    + intro. destruct_zmap. simpl. intros; omega. apply host_s2_map0.
    + assert_gso. red; intro T. rewrite T in page_0_invalid0. omega.
      rewrite (ZMap.gso _ _ Hneq). assumption.
    + rewrite ZMap.gss. rewrite H. intros until pte.
      replace (phys_page 144115188075855872 / PAGE_SIZE) with 0 by reflexivity.
      destruct_zmap. intros. inv Hpfn. contra.
      intros. autounfold in *. assert_gso. red; intro.
      inv H0. pose proof (host_flatmap0 _ _ _ _ Hpfn Hexists). inv H0.
      apply Heq. rewrite Z_div_mult_full. reflexivity. omega.
      rewrite (ZMap.gso _ _ Hneq). eapply host_iso0; eassumption.
    + intros. destruct_zmap. rewrite Heq in *.
      assert_gsoH H0. red; intro; srewrite; omega. rewrite (ZMap.gso _ _ Hneq) in H0.
      exploit (vm_iso0 _ _ _ _ _ H0); try eassumption. omega. intros.
      rewrite Hcond in H5. omega.
      assert_gsoH H0. red; intro; srewrite; omega. rewrite (ZMap.gso _ _ Hneq) in H0.
      rewrite (ZMap.gso _ _ Heq) in H4. eapply vm_iso0; eassumption.
    + intros. destruct_zmap. simpl. rewrite Heq in *.
      exploit (smmu_iso0 vmid0 cbndx index gfn pfn pte); try eassumption.
      rewrite Heq. assumption. omega.
      intros (? & ?). srewrite. eapply Hcount0 in Heq; try eassumption. inv Heq.
      rewrite H1. assumption.
      rewrite Heq. apply Hspt. eapply smmu_iso0; eassumption.
    + intro. destruct_zmap. simpl; intros.
      rewrite <- Hcond0. eapply smmu_count0; eassumption. eapply smmu_count0.
Qed.