MemAuxSpec

Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import GenSem.
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 PageMgmt.Spec.
Require Import NPTOps.Spec.
Require Import AbsMachine.Spec.
Require Import RData.
Require Import PageMgmt.Layer.
Require Import Constants.
Require Import HypsecCommLib.
Require Import MmioSPTOps.Spec.
Require Import NPTWalk.Spec.
Require Import MmioSPTWalk.Spec.

Local Open Scope Z_scope.

Section MemAuxSpec.

  Definition map_page_host_spec (addr: Z64) (adt: RData) : option RData :=
    match addr with
    | VZ64 addr =>
      rely is_addr addr;
      let pfn := addr / PAGE_SIZE in
      if halt adt then Some adt else
      let cpu := curid adt in
      let ptid := NPT_ID in
      match S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt), ptid @ (lock adt), ptid @ (log adt), ptid @ (oracle adt) with
      | LockFalse, spl0, spo, LockFalse, ptl0, pto =>
        let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
        let pt := CalNPT (HOSTVISOR @ (npts (shared adt))) (pto cpu ptl0) in
        let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
        let ptl := TEVENT cpu (TSHARED (OPULL ptid)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
        match H_CalLock ((spo cpu spl0) ++ spl0), H_CalLock ((pto cpu ptl0) ++ ptl0) with
        | Some (_, LEMPTY, None), Some (_, LEMPTY, None) =>
          let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p)) :: spl in
          let page := pfn @ s2p in
          rely is_int (s2_owner page); rely is_int (s2_count page);
          if (s2_owner page =? INVALID) || (s2_owner page =? HOSTVISOR) || (s2_count page >? 0) then
            let pte := (if s2_owner page =? INVALID then Z.lor (pfn * PAGE_SIZE) (Z.lor PAGE_S2_DEVICE S2_RDWR)
                        else Z.lor (pfn * PAGE_SIZE) PAGE_S2_KERNEL) in
            match local_mmap HOSTVISOR addr 3 pte pt with
            | Some (halt', npt') =>
              let ptl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (ONPT npt')) :: ptl in
              Some adt {halt: halt'} {tstate: if halt' then 0 else 1}
                   {shared: (shared adt) {npts: (npts (shared adt)) # HOSTVISOR == npt'} {s2page: s2p}}
                   {log: ((log adt) # S2PAGE_ID == (if halt' then spl else spl'))
                            # ptid == (if halt' then ptl else ptl')}
                   {lock: ((lock adt) # S2PAGE_ID == (if halt' then LockOwn true else LockFalse))
                             # ptid == (if halt' then LockOwn true else LockFalse)}
            | _ => None
            end
          else
            Some adt {halt: true} {tstate: 0} {shared: (shared adt) {s2page: s2p}}
                 {log: (log adt) # S2PAGE_ID == spl} {lock: (lock adt) # S2PAGE_ID == (LockOwn true)}
        | _, _ => None
        end
      | _, _, _, _, _, _ => None
      end
    end.

  Definition clear_vm_page_spec (vmid: Z) (pfn: Z64) (adt: RData) : option RData :=
    match pfn with
    | VZ64 pfn =>
      rely is_vmid vmid; rely is_pfn pfn;
      if halt adt then Some adt else
      let cpu := curid adt in
      match S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt), FLATMEM_ID @ (log adt), FLATMEM_ID @ (oracle adt) with
      | LockFalse, spl0, spo, fml0, fmo =>
        let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
        let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
        let fmem := CalFlatmem (flatmem (shared adt)) (fmo cpu fml0) in
        match H_CalLock ((spo cpu spl0) ++ spl0) with
        | Some (_, LEMPTY, None) =>
          let page := pfn @ s2p in
          rely is_int (s2_owner page);
          if s2_owner page =? vmid then
            let page' := mkS2Page HOSTVISOR 0 (pfn + SMMU_HOST_OFFSET) in
            let s2p' := s2p # pfn == page' in
            let fmem' := fmem # pfn == 0 in
            let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p')) :: spl in
            let fml' := TEVENT cpu (TSHARED (OFLATMEM fmem')) :: (fmo cpu fml0) ++ fml0 in
            Some adt {tstate: 1} {shared: (shared adt) {s2page: s2p'} {flatmem: fmem'}}
                 {log: ((log adt) # S2PAGE_ID == spl') # FLATMEM_ID == fml'} {lock: (lock adt) # S2PAGE_ID == LockFalse}
          else
            let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p)) :: spl in
            Some adt {tstate: 1} {shared: (shared adt) {s2page: s2p}}
                 {log: (log adt) # S2PAGE_ID == spl'} {lock: (lock adt) # S2PAGE_ID == LockFalse}
        | _ => None
        end
      | _, _, _, _, _ => None
      end
    end.


  Definition assign_pfn_to_vm_spec (vmid: Z) (gfn: Z64) (pfn: Z64) (adt: RData) : option RData :=
    match gfn, pfn with
    | VZ64 gfn, VZ64 pfn =>
      rely is_vmid vmid; rely is_gfn gfn; rely is_pfn pfn;
      if halt adt then Some adt else
      let cpu := curid adt in
      let ptid := NPT_ID in
      match S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt),
            ptid @ (lock adt), ptid @ (log adt), ptid @ (oracle adt),
            FLATMEM_ID @ (log adt), FLATMEM_ID @ (oracle adt)
      with
      | LockFalse, spl0, spo, LockFalse, ptl0, pto, fml0, fmo =>
        let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
        let npt := CalNPT (HOSTVISOR @ (npts (shared adt))) (pto cpu ptl0) in
        let fmem := CalFlatmem (flatmem (shared adt)) (fmo cpu fml0) in
        let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
        let ptl := TEVENT cpu (TSHARED (OPULL ptid)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
        match H_CalLock ((spo cpu spl0) ++ spl0), H_CalLock ((pto cpu ptl0) ++ ptl0) with
        | Some (_, LEMPTY, None), Some (_, LEMPTY, None) =>
          let page := pfn @ s2p in
          rely is_int (s2_owner page); rely is_int (s2_count page); rely is_int64 (s2_gfn page);
          if s2_owner page =? HOSTVISOR then
            if s2_count page =? 0 then
              let s2p' := s2p # pfn == (mkS2Page vmid 0 gfn) in
              let logn := vmid @ (data_log adt) in
              let fmem' := fmem # pfn == ((doracle adt) vmid logn) in
              match pfn @ (pt npt) with
              | (_, level, pte) =>
                rely is_int level;
                match (if (if phys_page pte =? 0 then 0 else level) =? 0 then Some (false, npt)
                      else local_mmap HOSTVISOR (pfn * PAGE_SIZE) 3 PAGE_GUEST npt) with
                | Some (halt', npt') =>
                  let ptl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (ONPT npt')) :: ptl in
                  let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p')) :: spl in
                  let fml' := TEVENT cpu (TSHARED (OFLATMEM fmem')) :: (fmo cpu fml0) ++ fml0 in
                  Some adt {halt: halt'} {tstate: if halt' then 0 else 1}
                       {data_log: if halt' then (data_log adt) else (data_log adt) # vmid == (logn + 1)}
                       {shared: (shared adt) {npts: (npts (shared adt)) # HOSTVISOR == npt'} {s2page: s2p'} {flatmem: if halt' then (flatmem (shared adt)) else fmem'}}
                       {log: if halt' then (((log adt) # S2PAGE_ID == spl) # ptid == ptl)
                             else (((log adt) # S2PAGE_ID == spl') # ptid == ptl') # FLATMEM_ID == fml'}
                       {lock: ((lock adt) # S2PAGE_ID == (if halt' then LockOwn true else LockFalse))
                                # ptid == (if halt' then LockOwn true else LockFalse)}
                | _ => None
                end
              end
            else
              Some adt {halt: true} {tstate: 0} {shared: (shared adt) {s2page: s2p}}
                  {log: ((log adt) # S2PAGE_ID == spl)} {lock: (lock adt) # S2PAGE_ID == (LockOwn true)}
          else
            if (s2_owner page =? vmid) && (gfn =? s2_gfn page) then
              if s2_count page =? INVALID then
                let page' := page {s2_count: 0} in
                let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE (s2p # pfn == page'))) :: spl in
                Some adt {tstate: 1} {shared: (shared adt) {s2page: s2p # pfn == page'}}
                     {log: ((log adt) # S2PAGE_ID == spl')} {lock: (lock adt) # S2PAGE_ID == LockFalse}
              else
                let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p)) :: spl in
                Some adt {tstate: 1} {shared: (shared adt) {s2page: s2p}}
                     {log: ((log adt) # S2PAGE_ID == spl')} {lock: (lock adt) # S2PAGE_ID == LockFalse}
            else
              Some adt {halt: true} {tstate: 0} {shared: (shared adt) {s2page: s2p}}
                  {log: ((log adt) # S2PAGE_ID == spl)} {lock: (lock adt) # S2PAGE_ID == (LockOwn true)}
      | _, _ => None
      end
    | _, _, _, _, _, _, _, _ => None
    end
  end.

  Definition map_pfn_vm_spec (vmid: Z) (addr: Z64) (pte: Z64) (level: Z) (adt: RData) : option RData :=
    match addr, pte with
    | VZ64 addr, VZ64 pte =>
      rely is_vmid vmid; rely is_addr addr; rely is_int64 pte;
      if halt adt then Some adt else
      let id := NPT_ID + vmid in
      let cpu := curid adt in
      match id @ (lock adt), id @ (log adt), id @ (oracle adt) with
      | LockFalse, l, orac =>
        let npt := CalNPT (vmid @ (npts (shared adt))) (orac cpu l) in
        let l' := TEVENT cpu (TSHARED (OPULL id)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (orac cpu l) ++ l in
        match H_CalLock ((orac cpu l) ++ l) with
        | Some (_, LEMPTY, None) =>
          let paddr := phys_page pte in
          let perm := PAGE_S2_KERNEL in
          let pte' := (if level =? 2 then Z.land (Z.lor paddr perm) NOT_PMD_TABLE_BIT else Z.lor paddr perm) in
          let level' := (if level =? 2 then 2 else 3) in
          match local_mmap vmid addr level' pte' npt with
          | Some (halt', npt') =>
            let l'' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (ONPT npt')) :: l' in
            Some adt {halt: halt'} {tstate: if halt' then 0 else 1}
                 {shared: (shared adt) {npts: (npts (shared adt)) # vmid == npt'}}
                 {log: (log adt) # id == (if halt' then l' else l'')}
                 {lock: (lock adt) # id == (if halt' then LockOwn true else LockFalse)}
          | _ => None
          end
        | _ => None
        end
      | _, _, _ => None
      end
    end.

  Definition map_vm_io_spec (vmid: Z) (gpa: Z64) (pa: Z64) (adt: RData) : option RData :=
    match gpa, pa with
    | VZ64 gpa, VZ64 pa =>
      rely is_vmid vmid; rely is_addr gpa; rely is_addr pa;
      if halt adt then Some adt else
      let cpu := curid adt in
      let ptid := NPT_ID + vmid in
      match S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt), ptid @ (lock adt), ptid @ (log adt), ptid @ (oracle adt) with
      | LockFalse, spl0, spo, LockFalse, ptl0, pto =>
        let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
        let npt := CalNPT (vmid @ (npts (shared adt))) (pto cpu ptl0) in
        let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
        let ptl := TEVENT cpu (TSHARED (OPULL ptid)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
        match H_CalLock ((spo cpu spl0) ++ spl0), H_CalLock ((pto cpu ptl0) ++ ptl0) with
        | Some (_, LEMPTY, None), Some (_, LEMPTY, None) =>
          let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p)) :: spl in
          let gfn := gpa / PAGE_SIZE in
          let pfn := pa / PAGE_SIZE in
          let pte := Z.lor (phys_page pa) (Z.lor PAGE_S2_DEVICE S2_RDWR) in
          let page := pfn @ s2p in
          rely is_int (s2_owner page);
          if s2_owner page =? INVALID then
            match local_mmap vmid gpa 3 pte npt with
            | Some (halt', npt') =>
              let ptl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (ONPT npt')) :: ptl in
              Some adt {halt: halt'} {tstate: if halt' then 0 else 1}
                   {shared: (shared adt) {npts: (npts (shared adt)) # vmid == npt'} {s2page: s2p}}
                   {log: ((log adt) # S2PAGE_ID == (if halt' then spl else spl'))
                            # ptid == (if halt' then ptl else ptl')}
                   {lock: ((lock adt) # S2PAGE_ID == (if halt' then LockOwn true else LockFalse))
                             # ptid == (if halt' then LockOwn true else LockFalse)}
            | _ => None
            end
          else
            Some adt {tstate: 1} {shared: (shared adt) {s2page: s2p}}
                 {log: (log adt) # S2PAGE_ID == spl'} {lock: (lock adt) # S2PAGE_ID == LockFalse}
        | _, _ => None
        end
      | _, _, _, _, _, _ => None
      end
    end.

  Definition grant_vm_page_spec (vmid: Z) (pfn: Z64) (adt: RData) : option RData :=
    match pfn with
    | VZ64 pfn =>
      rely is_vmid vmid; rely is_pfn pfn;
      if halt adt then Some adt else
      let cpu := curid adt in
      match S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt) with
      | LockFalse, spl0, spo =>
        let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
        let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
        match H_CalLock ((spo cpu spl0) ++ spl0) with
        | Some (_, LEMPTY, None) =>
          let page := pfn @ s2p in
          rely is_int (s2_owner page); rely is_int (s2_count page);
          let s2p' := (if (s2_owner page =? vmid) && (s2_count page <? MAX_SHARE_COUNT)
                       then s2p # pfn == (page {s2_count: (s2_count page) + 1})
                       else s2p) in
          let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p')) :: spl in
          Some adt {tstate: 1} {shared: (shared adt) {s2page: s2p'}}
               {log: (log adt) # S2PAGE_ID == spl'} {lock: (lock adt) # S2PAGE_ID == LockFalse}
        | _ => None
        end
      | _, _, _ => None
      end
    end.

  Definition revoke_vm_page_spec (vmid: Z) (pfn: Z64) (adt: RData) : option RData :=
    match pfn with
    | VZ64 pfn =>
      rely is_vmid vmid; rely is_pfn pfn;
      if halt adt then Some adt else
      let cpu := curid adt in
      let ptid := NPT_ID in
      match S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt),
            ptid @ (lock adt), ptid @ (log adt), ptid @ (oracle adt),
            FLATMEM_ID @ (log adt), FLATMEM_ID @ (oracle adt)
      with
      | LockFalse, spl0, spo, LockFalse, ptl0, pto, fml0, fmo =>
        let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
        let npt := CalNPT (HOSTVISOR @ (npts (shared adt))) (pto cpu ptl0) in
        let fmem := CalFlatmem (flatmem (shared adt)) (fmo cpu fml0) in
        let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
        let ptl := TEVENT cpu (TSHARED (OPULL ptid)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
        match H_CalLock ((spo cpu spl0) ++ spl0), H_CalLock ((pto cpu ptl0) ++ ptl0) with
        | Some (_, LEMPTY, None), Some (_, LEMPTY, None) =>
          let page := pfn @ s2p in
          rely is_int (s2_owner page); rely is_int (s2_count page);
          if (s2_owner page =? vmid) && (s2_count page >? 0) then
            let s2p' := s2p # pfn == (page {s2_count: (s2_count page) - 1}) in
            let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p')) :: spl in
            if s2_count page =? 1 then
              let logn := vmid @ (data_log adt) in
              let fmem' := fmem # pfn == ((doracle adt) vmid logn) in
              match pfn @ (pt npt) with
              | (_, level, pte) =>
                rely is_int level;
                match (if (if phys_page pte =? 0 then 0 else level) =? 0 then Some (false, npt)
                      else local_mmap HOSTVISOR (pfn * PAGE_SIZE) 3 PAGE_GUEST npt) with
                | Some (halt', npt') =>
                  let ptl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (ONPT npt')) :: ptl in
                  let fml' := TEVENT cpu (TSHARED (OFLATMEM fmem')) :: (fmo cpu fml0) ++ fml0 in
                  Some adt {halt: halt'} {tstate: if halt' then 0 else 1}
                       {data_log: if halt' then (data_log adt) else (data_log adt) # vmid == (logn + 1)}
                       {shared: (shared adt) {npts: (npts (shared adt)) # HOSTVISOR == npt'}
                                             {s2page: s2p'} {flatmem: if halt' then (flatmem (shared adt)) else fmem'}}
                       {log: if halt' then (((log adt) # S2PAGE_ID == spl) # ptid == ptl)
                             else (((log adt) # S2PAGE_ID == spl') # ptid == ptl') # FLATMEM_ID == fml'}
                       {lock: ((lock adt) # S2PAGE_ID == (if halt' then LockOwn true else LockFalse))
                                # ptid == (if halt' then LockOwn true else LockFalse)}
                | _ => None
                end
              end
            else
              Some adt {tstate: 1} {shared: (shared adt) {s2page: s2p'}}
                  {log: (log adt) # S2PAGE_ID == spl'} {lock: (lock adt) # S2PAGE_ID == LockFalse}
          else
            let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p)) :: spl in
            Some adt {tstate: 1} {shared: (shared adt) {s2page: s2p}}
                 {log: (log adt) # S2PAGE_ID == spl'} {lock: (lock adt) # S2PAGE_ID == LockFalse}
        | _, _ => None
        end
      | _, _, _, _, _, _, _, _ => None
      end
    end.

  Definition assign_pfn_to_smmu_spec (vmid: Z) (gfn: Z64) (pfn: Z64) (adt: RData) : option RData :=
    match gfn, pfn with
    | VZ64 gfn, VZ64 pfn =>
      rely is_vmid vmid; rely is_gfn gfn; rely is_pfn pfn;
      if halt adt then Some adt else
      let cpu := curid adt in
      let ptid := NPT_ID in
      match S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt),
            ptid @ (lock adt), ptid @ (log adt), ptid @ (oracle adt),
            FLATMEM_ID @ (log adt), FLATMEM_ID @ (oracle adt)
      with
      | LockFalse, spl0, spo, LockFalse, ptl0, pto, fml0, fmo =>
        let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
        let npt := CalNPT (HOSTVISOR @ (npts (shared adt))) (pto cpu ptl0) in
        let fmem := CalFlatmem (flatmem (shared adt)) (fmo cpu fml0) in
        let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
        let ptl := TEVENT cpu (TSHARED (OPULL ptid)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
        match H_CalLock ((spo cpu spl0) ++ spl0), H_CalLock ((pto cpu ptl0) ++ ptl0) with
        | Some (_, LEMPTY, None), Some (_, LEMPTY, None) =>
          let page := pfn @ s2p in
          rely is_int (s2_owner page); rely is_int (s2_count page); rely is_int64 (s2_gfn page);
          if s2_owner page =? HOSTVISOR then
            if s2_count page =? 0 then
              let s2p' := s2p # pfn == (mkS2Page vmid INVALID gfn) in
              let logn := vmid @ (data_log adt) in
              let fmem' := fmem # pfn == ((doracle adt) vmid logn) in
              match pfn @ (pt npt) with
              | (_, level, pte) =>
                rely is_int level;
                match (if (if phys_page pte =? 0 then 0 else level) =? 0 then Some (false, npt)
                      else local_mmap HOSTVISOR (pfn * PAGE_SIZE) 3 PAGE_GUEST npt) with
                | Some (halt', npt') =>
                  let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p')) :: spl in
                  let ptl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (ONPT npt')) :: ptl in
                  let fml' := TEVENT cpu (TSHARED (OFLATMEM fmem')) :: (fmo cpu fml0) ++ fml0 in
                  Some adt {halt: halt'} {tstate: if halt' then 0 else 1}
                      {data_log: if halt' then (data_log adt) else (data_log adt) # vmid == (logn + 1)}
                      {shared: (shared adt) {npts: (npts (shared adt)) # HOSTVISOR == npt'}
                                            {s2page: if halt' then s2p else s2p'}
                                            {flatmem: if halt' then (flatmem (shared adt)) else fmem'}}
                      {log: if halt' then (((log adt) # S2PAGE_ID == spl) # ptid == ptl)
                            else (((log adt) # S2PAGE_ID == spl') # ptid == ptl') # FLATMEM_ID == fml'}
                      {lock: ((lock adt) # S2PAGE_ID == (if halt' then LockOwn true else LockFalse))
                                # ptid == (if halt' then LockOwn true else LockFalse)}
                | _ => None
                end
              end
            else
              Some adt {halt: true} {tstate: 0} {shared: (shared adt) {s2page: s2p}}
                  {log: (log adt) # S2PAGE_ID == spl} {lock: (lock adt) # S2PAGE_ID == (LockOwn true)}
          else
            if s2_owner page =? vmid then
              let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p)) :: spl in
              Some adt {tstate: 1} {shared: (shared adt) {s2page: s2p}}
                  {log: (log adt) # S2PAGE_ID == spl'} {lock: (lock adt) # S2PAGE_ID == LockFalse}
            else
              Some adt {halt: true} {tstate: 0} {shared: (shared adt) {s2page: s2p}}
                  {log: (log adt) # S2PAGE_ID == spl} {lock: (lock adt) # S2PAGE_ID == (LockOwn true)}
        | _, _ => None
        end
      | _, _, _, _, _, _, _, _ => None
      end
    end.

  Definition update_smmu_page_spec (vmid: Z) (cbndx: Z) (index: Z) (iova: Z64) (pte: Z64) (adt: RData) : option RData :=
    match iova, pte with
    | VZ64 iova, VZ64 pte =>
      rely is_vmid vmid; rely is_smmu index; rely is_smmu_cfg cbndx; rely is_smmu_addr iova; rely is_int64 pte;
      if halt adt then Some adt else
      let cpu := curid adt in
      match S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt),
            SPT_ID @ (lock adt), SPT_ID @ (log adt), SPT_ID @ (oracle adt) with
      | LockFalse, spl0, spo, LockFalse, ptl0, pto =>
        let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
        let spt := CalSPT (spts (shared adt)) (pto cpu ptl0) in
        let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
        let ptl := TEVENT cpu (TSHARED (OPULL SPT_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
        match H_CalLock ((spo cpu spl0) ++ spl0), H_CalLock ((pto cpu ptl0) ++ ptl0) with
        | Some (_, LEMPTY, None), Some (_, LEMPTY, None) =>
          let pfn := phys_page pte / PAGE_SIZE in
          let gfn := iova / PAGE_SIZE in
          let page := pfn @ s2p in
          rely is_int (s2_owner page); rely is_int (s2_count page); rely is_int64 (s2_gfn page);
          if (vmid =? s2_owner page) && (gfn =? s2_gfn page) then
            match local_spt_map cbndx index iova pte spt with
            | Some (halt', spt') =>
              if halt' then
                Some adt {halt: halt'} {tstate: 0} {shared: (shared adt) {spts: spt'} {s2page: s2p}}
                    {log: ((log adt) # S2PAGE_ID == spl) # SPT_ID == ptl}
                    {lock: ((lock adt) # S2PAGE_ID == (LockOwn true)) # SPT_ID == (LockOwn true)}
              else
                let s2p' := (if (s2_owner page =? HOSTVISOR) && (s2_count page <? EL2_SMMU_CFG_SIZE)
                              then s2p # pfn == (page {s2_count: (s2_count page) + 1}) else s2p) in
                let ptl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSPT spt')) :: ptl in
                let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p')) :: spl in
                Some adt {halt: halt'} {tstate: 1} {shared: (shared adt) {spts: spt'} {s2page: s2p'}}
                    {log: ((log adt) # S2PAGE_ID == spl') # SPT_ID == ptl'}
                    {lock: ((lock adt) # S2PAGE_ID == LockFalse) # SPT_ID == LockFalse}
            | _ => None
            end
          else
            Some adt {halt: true} {tstate: 0} {shared: (shared adt) {s2page: s2p}}
                {log: (log adt) # S2PAGE_ID == spl} {lock: (lock adt) # S2PAGE_ID == (LockOwn true)}
        | _, _ => None
        end
      | _, _, _, _, _, _ => None
      end
    end.

  Definition unmap_smmu_page_spec (cbndx: Z) (index: Z) (iova: Z64) (adt: RData) : option RData :=
    match iova with
    | VZ64 iova =>
      rely is_smmu index; rely is_smmu_cfg cbndx; rely is_smmu_addr iova;
      if halt adt then Some adt else
      let cpu := curid adt in
      match S2PAGE_ID @ (lock adt), S2PAGE_ID @ (log adt), S2PAGE_ID @ (oracle adt),
            SPT_ID @ (lock adt), SPT_ID @ (log adt), SPT_ID @ (oracle adt) with
      | LockFalse, spl0, spo, LockFalse, ptl0, pto =>
        let s2p := CalS2Page (s2page (shared adt)) (spo cpu spl0) in
        let spt := CalSPT (spts (shared adt)) (pto cpu ptl0) in
        let spl := TEVENT cpu (TSHARED (OPULL S2PAGE_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (spo cpu spl0) ++ spl0 in
        let ptl := TEVENT cpu (TSHARED (OPULL SPT_ID)) :: TEVENT cpu (TTICKET (WAIT_LOCK local_lock_bound)) :: (pto cpu ptl0) ++ ptl0 in
        match H_CalLock ((spo cpu spl0) ++ spl0), H_CalLock ((pto cpu ptl0) ++ ptl0) with
        | Some (_, LEMPTY, None), Some (_, LEMPTY, None) =>
          let ttbr := SMMU_TTBR index cbndx in
          let pt := ttbr @ (spt_pt spt) in
          let gfn := iova / PAGE_SIZE in
          let (_, pte) := gfn @ pt in
          rely is_int64 pte;
          match (if pte =? 0 then Some (false, spt) else local_spt_map cbndx index iova 0 spt) with
          | Some (halt', spt') =>
            if halt' then
              Some adt {halt: halt'} {tstate: 0} {shared: (shared adt) {spts: spt'} {s2page: s2p}}
                  {log: ((log adt) # S2PAGE_ID == spl) # SPT_ID == ptl}
                  {lock: ((lock adt) # S2PAGE_ID == (LockOwn true)) # SPT_ID == (LockOwn true)}
            else
              let pfn := phys_page pte / PAGE_SIZE in
              let page := pfn @ s2p in
              rely is_int (s2_owner page); rely is_int (s2_count page);
              let s2p' := (if (s2_owner page =? HOSTVISOR) && (s2_count page >? 0)
                            then s2p # pfn == (page {s2_count: (s2_count page) - 1}) else s2p) in
              let spl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OS2_PAGE s2p')) :: spl in
              let ptl' := TEVENT cpu (TTICKET REL_LOCK) :: TEVENT cpu (TSHARED (OSPT spt')) :: ptl in
              Some adt {halt: halt'} {tstate: 1} {shared: (shared adt) {spts: spt'} {s2page: s2p'}}
                  {log: ((log adt) # S2PAGE_ID == spl') # SPT_ID == ptl'}
                  {lock: ((lock adt) # S2PAGE_ID == LockFalse) # SPT_ID == LockFalse}
          | _ => None
          end
        | _, _ => None
        end
      | _, _, _, _, _, _ => None
      end
    end.

  Definition mem_load_no_check_spec (gfn: Z64) (reg: Z) (bypass: Z) (adt: RData) : option RData :=
    match gfn, icore adt with
    | VZ64 gfn, false =>
      let vmid := cur_vmid adt in
      match gfn @ (pt (vmid @ (npts (shared adt)))) with
      | (pfn, level, pte) =>
        if pfn =? 0 then None
        else
          if bypass =? 0 then
            let (valc, labelc) := (pfn @ (cache (shared adt))) in
            if (labelc =? -1) then
              let (valm, labelm) := (pfn @ (flatmem (shared adt))) in
              let cache' := ((cache (shared adt)) # pfn == (valm, labelm)) in
              let adt' := adt {shared: (shared adt) {cache: cache'}} in
              Some adt'
            else
              Some adt
          (* cache bypass *)
          else
            let (valm, labelm) := (pfn @ (flatmem (shared adt))) in
            Some adt
      end
    | _, _ => None
    end.

  Definition mem_store_no_check_spec (gfn: Z64) (reg: Z) (bypass: Z) (adt: RData) : option RData :=
    match gfn, icore adt with
    | VZ64 gfn, false =>
      let vmid := cur_vmid adt in
      match gfn @ (pt (vmid @ (npts (shared adt)))) with
      | (pfn, level, pte) =>
        if pfn =? 0 then None
        else
          let new_label := (
          if (s2_owner (pfn @ (s2page (shared adt))) =? INVALID) ||
              (s2_count (pfn @ (s2page (shared adt))) >? 0) then
              -2
          else
              vmid
          ) in
          if bypass =? 0 then
            let (valc, label) := (pfn @ (cache (shared adt))) in 
            if (label =? -1) then
              let fm' := ((flatmem (shared adt)) # pfn == (val, new_label)) in
              let cache' := ((cache (shared adt)) # pfn == (val, new_label)) in
              let adt' := adt {shared: (shared adt) {flatmem: fm'} {cache: cache'}} in
              Some adt'
            else
              let cache' := ((cache (shared adt)) # pfn == (val, new_label)) in
              let adt' := adt {shared: (shared adt) {cache: cache'}} in
              Some adt'
          (* cache bypass *)
          else
            let (valm, labelm) := (pfn @ (flatmem (shared adt))) in
            let fm' := ((flatmem (shared adt)) # pfn == (val, new_label)) in
            let adt' := adt {shared: (shared adt) {flatmem: fm'}} in
            Some adt'
      end
    | _, _ => None
    end.

End MemAuxSpec.

Section MemAuxSpecLow.

  Context `{real_params: RealParams}.

  Notation LDATA := RData.

  Notation LDATAOps := (cdata (cdata_ops := PageMgmt_ops) LDATA).

  Definition map_page_host_spec0 (addr: Z64) (adt: RData) : option RData :=
    match addr with
    | VZ64 addr =>
      rely is_addr addr;
      let pfn := addr / PAGE_SIZE in
      when adt0 == acquire_lock_s2page_spec adt;
      when owner == get_pfn_owner_spec (VZ64 pfn) adt0;
      rely is_int owner;
      when count == get_pfn_count_spec (VZ64 pfn) adt0;
      rely is_int count;
      if owner =? INVALID then
        let perm := Z.lor PAGE_S2_DEVICE S2_RDWR in
        let pte := Z.lor (pfn * PAGE_SIZE) perm in
        when adt1 == map_s2pt_spec HOSTVISOR (VZ64 addr) 3 (VZ64 pte) adt0;
        release_lock_s2page_spec adt1
      else
        if (owner =? HOSTVISOR) || (count >? 0) then
          let perm := PAGE_S2_KERNEL in
          let pte := Z.lor (pfn * PAGE_SIZE) perm in
          when adt1 == map_s2pt_spec HOSTVISOR (VZ64 addr) 3 (VZ64 pte) adt0;
          release_lock_s2page_spec adt1
        else
          when adt1 == panic_spec adt0;
          release_lock_s2page_spec adt1
  end.

  Definition clear_vm_page_spec0 (vmid: Z) (pfn: Z64) (adt: RData) : option RData :=
    match pfn with
    | VZ64 pfn =>
      rely is_pfn pfn;
      when adt1 == acquire_lock_s2page_spec adt;
      when owner == get_pfn_owner_spec (VZ64 pfn) adt1;
      rely is_int owner;
      if owner =? vmid then
        when adt2 == set_pfn_owner_spec (VZ64 pfn) HOSTVISOR adt1;
        when adt3 == set_pfn_count_spec (VZ64 pfn) 0 adt2;
        when adt4 == set_pfn_map_spec (VZ64 pfn) (VZ64 (pfn + SMMU_HOST_OFFSET)) adt3;
        when adt5 == clear_phys_page_spec (VZ64 pfn) adt4;
        release_lock_s2page_spec adt5
      else
        release_lock_s2page_spec adt1
    end.

  Definition assign_pfn_to_vm_spec0 (vmid: Z) (gfn: Z64) (pfn: Z64) (adt: RData) : option RData :=
    match gfn, pfn with
    | VZ64 gfn, VZ64 pfn =>
      rely is_gfn gfn; rely is_pfn pfn;
      when adt1 == acquire_lock_s2page_spec adt;
      when owner == get_pfn_owner_spec (VZ64 pfn) adt1;
      rely is_int owner;
      when count == get_pfn_count_spec (VZ64 pfn) adt1;
      rely is_int count;
      if (owner =? HOSTVISOR) then
        if (count =? 0) then
          when adt2 == set_pfn_owner_spec (VZ64 pfn) vmid adt1;
          when adt3 == set_pfn_map_spec (VZ64 pfn) (VZ64 gfn) adt2;
          when adt4 == clear_pfn_host_spec (VZ64 pfn) adt3;
          when adt5 == fetch_from_doracle_spec vmid (VZ64 pfn) (VZ64 1) adt4;
          release_lock_s2page_spec adt5
        else
          when adt2 == panic_spec adt1;
          release_lock_s2page_spec adt2
      else
        if owner =? vmid then
          when' map == get_pfn_map_spec (VZ64 pfn) adt1;
          rely is_int64 map;
          if gfn =? map then
            if count =? INVALID then
              when adt2 == set_pfn_count_spec (VZ64 pfn) 0 adt1;
              release_lock_s2page_spec adt2
            else
              release_lock_s2page_spec adt1
          else
            when adt2 == panic_spec adt1;
            release_lock_s2page_spec adt2
        else
          when adt2 == panic_spec adt1;
          release_lock_s2page_spec adt2
    end.

  Definition map_pfn_vm_spec0 (vmid: Z) (addr: Z64) (pte: Z64) (level: Z) (adt: RData) : option RData :=
    match addr, pte with
    | VZ64 addr, VZ64 pte =>
      rely is_addr addr;
      let paddr := phys_page pte in
      let perm := PAGE_S2_KERNEL in
      if level =? 2 then
        let pte := Z.land (Z.lor paddr perm) NOT_PMD_TABLE_BIT in
        map_s2pt_spec vmid (VZ64 addr) 2 (VZ64 pte) adt
      else
        let pte := Z.lor paddr perm in
        map_s2pt_spec vmid (VZ64 addr) 3 (VZ64 pte) adt
    end.

  Definition map_vm_io_spec0 (vmid: Z) (gpa: Z64) (pa: Z64) (adt: RData) : option RData :=
    match gpa, pa with
    | VZ64 gpa, VZ64 pa =>
      rely is_addr gpa; rely is_addr pa;
      let gfn := gpa / PAGE_SIZE in
      let pfn := pa / PAGE_SIZE in
      let pte := Z.lor (phys_page pa) (Z.lor PAGE_S2_DEVICE S2_RDWR) in
      when adt1 == acquire_lock_s2page_spec adt;
      when owner == get_pfn_owner_spec (VZ64 pfn) adt1;
      rely is_int owner;
      if owner =? INVALID then
        when adt2 == map_s2pt_spec vmid (VZ64 gpa) 3 (VZ64 pte) adt1;
        release_lock_s2page_spec adt2
      else
        release_lock_s2page_spec adt1
    end.

  Definition grant_vm_page_spec0 (vmid: Z) (pfn: Z64) (adt: RData) : option RData :=
    match pfn with
    | VZ64 pfn =>
      rely is_addr pfn;
      when adt1 == acquire_lock_s2page_spec adt;
      when owner == get_pfn_owner_spec (VZ64 pfn) adt1;
      rely is_int owner;
      when count == get_pfn_count_spec (VZ64 pfn) adt1;
      rely is_int count;
      if (owner =? vmid) && (count <? MAX_SHARE_COUNT) then
        when adt2 == set_pfn_count_spec (VZ64 pfn) (count + 1) adt1;
        release_lock_s2page_spec adt2
      else
        release_lock_s2page_spec adt1
    end.

  Definition revoke_vm_page_spec0 (vmid: Z) (pfn: Z64) (adt: RData) : option RData :=
    match pfn with
    | VZ64 pfn =>
      rely is_addr pfn;
      when adt1 == acquire_lock_s2page_spec adt;
      when owner == get_pfn_owner_spec (VZ64 pfn) adt1;
      rely is_int owner;
      when count == get_pfn_count_spec (VZ64 pfn) adt1;
      rely is_int count;
      if (owner =? vmid) && (count >? 0) then
        when adt2 == set_pfn_count_spec (VZ64 pfn) (count - 1) adt1;
          if count =? 1 then
            when adt3 == clear_pfn_host_spec (VZ64 pfn) adt2;
            when adt4 == fetch_from_doracle_spec vmid (VZ64 pfn) (VZ64 1) adt3;
            release_lock_s2page_spec adt4
          else
            release_lock_s2page_spec adt2
      else
        release_lock_s2page_spec adt1
    end.

  Definition assign_pfn_to_smmu_spec0 (vmid: Z) (gfn: Z64) (pfn: Z64) (adt: RData) : option RData :=
    match gfn, pfn with
    | VZ64 gfn, VZ64 pfn =>
      rely is_vmid vmid; rely is_gfn gfn; rely is_pfn pfn;
      when adt1 == acquire_lock_s2page_spec adt;
      when owner == get_pfn_owner_spec (VZ64 pfn) adt1;
      rely is_int owner;
      when count == get_pfn_count_spec (VZ64 pfn) adt1;
      rely is_int count;
      when' map == get_pfn_map_spec (VZ64 pfn) adt1;
      rely is_int64 map;
      if owner =? HOSTVISOR then
        if count =? 0 then
          when adt2 == clear_pfn_host_spec (VZ64 pfn) adt1;
          when adt3 == fetch_from_doracle_spec vmid (VZ64 pfn) (VZ64 1) adt2;
          when adt4 == set_pfn_owner_spec (VZ64 pfn) vmid adt3;
          when adt5 == set_pfn_map_spec (VZ64 pfn) (VZ64 gfn) adt4;
          when adt6 == set_pfn_count_spec (VZ64 pfn) INVALID adt5;
          release_lock_s2page_spec adt6
        else
          when adt2 == panic_spec adt1;
          release_lock_s2page_spec adt2
      else
        if owner =? vmid then
          release_lock_s2page_spec adt1
        else
          when adt2 == panic_spec adt1;
          release_lock_s2page_spec adt2
    end.

  Definition update_smmu_page_spec0 (vmid: Z) (cbndx: Z) (index: Z) (iova: Z64) (pte: Z64) (adt: RData) : option RData :=
    match iova, pte with
    | VZ64 iova, VZ64 pte =>
      rely is_addr iova;
      when adt1 == acquire_lock_s2page_spec adt;
      let pfn := phys_page pte / PAGE_SIZE in
      let gfn := iova / PAGE_SIZE in
      when owner == get_pfn_owner_spec (VZ64 pfn) adt1;
      rely is_int owner;
      when' map == get_pfn_map_spec (VZ64 pfn) adt1;
      rely is_int64 map;
      if (vmid =? owner) && (gfn =? map) then
        when adt2 == map_spt_spec cbndx index (VZ64 iova) (VZ64 pte) adt1;
        if owner =? HOSTVISOR then
          when count == get_pfn_count_spec (VZ64 pfn) adt2;
          rely is_int count;
          if count <? EL2_SMMU_CFG_SIZE then
            when adt3 == set_pfn_count_spec (VZ64 pfn) (count+1) adt2;
            release_lock_s2page_spec adt3
          else
            release_lock_s2page_spec adt2
        else
          release_lock_s2page_spec adt2
      else
        when adt2 == panic_spec adt1;
        release_lock_s2page_spec adt2
    end.

  Definition unmap_smmu_page_spec0 (cbndx: Z) (index: Z) (iova: Z64) (adt: RData) : option RData :=
    match iova with
    | VZ64 iova =>
      rely is_addr iova;
      when adt1 == acquire_lock_s2page_spec adt;
      when' pte, adt2 == unmap_spt_spec cbndx index (VZ64 iova) adt1;
      rely is_int64 pte;
      let pfn := phys_page pte / PAGE_SIZE in
      when owner == get_pfn_owner_spec (VZ64 pfn) adt2;
      rely is_int owner;
      if owner =? HOSTVISOR then
        when count == get_pfn_count_spec (VZ64 pfn) adt2;
        rely is_int count;
        if count >? 0 then
          when adt3 == set_pfn_count_spec (VZ64 pfn) (count-1) adt2;
          release_lock_s2page_spec adt3
        else
          release_lock_s2page_spec adt2
      else
        release_lock_s2page_spec adt2
    end.

  Definition mem_load_no_check_spec0 (gfn: Z64) (reg: Z) (bypass: Z) (adt: RData) : option RData :=
    mem_load_check_spec gfn reg bypass adt.

  Definition mem_store_no_check_spec0 (gfn: Z64) (reg: Z) (bypass: Z) (adt: RData) : option RData :=
    mem_store_check_spec gfn reg bypass adt.

  Inductive map_page_host_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | map_page_host_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' addr
      (Hinv: high_level_invariant labd)
      (Hspec: map_page_host_spec0 (VZ64 (Int64.unsigned addr)) labd = Some labd'):
      map_page_host_spec_low_step s WB ((Vlong addr)::nil) (m'0, labd) Vundef (m'0, labd').

  Inductive clear_vm_page_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | clear_vm_page_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid pfn
      (Hinv: high_level_invariant labd)
      (Hspec: clear_vm_page_spec0 (Int.unsigned vmid) (VZ64 (Int64.unsigned pfn)) labd = Some labd'):
      clear_vm_page_spec_low_step s WB ((Vint vmid)::(Vlong pfn)::nil) (m'0, labd) Vundef (m'0, labd').

  Inductive assign_pfn_to_vm_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | assign_pfn_to_vm_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid gfn pfn
      (Hinv: high_level_invariant labd)
      (Hspec: assign_pfn_to_vm_spec0 (Int.unsigned vmid) (VZ64 (Int64.unsigned gfn)) (VZ64 (Int64.unsigned pfn)) labd = Some labd'):
      assign_pfn_to_vm_spec_low_step s WB ((Vint vmid)::(Vlong gfn)::(Vlong pfn)::nil) (m'0, labd) Vundef (m'0, labd').

  Inductive map_pfn_vm_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | map_pfn_vm_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid addr pte level
      (Hinv: high_level_invariant labd)
      (Hspec: map_pfn_vm_spec0 (Int.unsigned vmid) (VZ64 (Int64.unsigned addr)) (VZ64 (Int64.unsigned pte)) (Int.unsigned level) labd = Some labd'):
      map_pfn_vm_spec_low_step s WB ((Vint vmid)::(Vlong addr)::(Vlong pte)::(Vint level)::nil) (m'0, labd) Vundef (m'0, labd').

  Inductive map_vm_io_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | map_vm_io_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid gpa pa
      (Hinv: high_level_invariant labd)
      (Hspec: map_vm_io_spec0 (Int.unsigned vmid) (VZ64 (Int64.unsigned gpa)) (VZ64 (Int64.unsigned pa)) labd = Some labd'):
      map_vm_io_spec_low_step s WB ((Vint vmid)::(Vlong gpa)::(Vlong pa)::nil) (m'0, labd) Vundef (m'0, labd').

  Inductive grant_vm_page_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | grant_vm_page_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid pfn
      (Hinv: high_level_invariant labd)
      (Hspec: grant_vm_page_spec0 (Int.unsigned vmid) (VZ64 (Int64.unsigned pfn)) labd = Some labd'):
      grant_vm_page_spec_low_step s WB ((Vint vmid)::(Vlong pfn)::nil) (m'0, labd) Vundef (m'0, labd').

  Inductive revoke_vm_page_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | revoke_vm_page_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid pfn
      (Hinv: high_level_invariant labd)
      (Hspec: revoke_vm_page_spec0 (Int.unsigned vmid) (VZ64 (Int64.unsigned pfn)) labd = Some labd'):
      revoke_vm_page_spec_low_step s WB ((Vint vmid)::(Vlong pfn)::nil) (m'0, labd) Vundef (m'0, labd').

  Inductive assign_pfn_to_smmu_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | assign_pfn_to_smmu_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid gfn pfn
      (Hinv: high_level_invariant labd)
      (Hspec: assign_pfn_to_smmu_spec0 (Int.unsigned vmid) (VZ64 (Int64.unsigned gfn)) (VZ64 (Int64.unsigned pfn)) labd = Some labd'):
      assign_pfn_to_smmu_spec_low_step s WB ((Vint vmid)::(Vlong gfn)::(Vlong pfn)::nil) (m'0, labd) Vundef (m'0, labd').

  Inductive update_smmu_page_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | update_smmu_page_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' vmid cbndx index iova pte
      (Hinv: high_level_invariant labd)
      (Hspec: update_smmu_page_spec0 (Int.unsigned vmid) (Int.unsigned cbndx) (Int.unsigned index) (VZ64 (Int64.unsigned iova)) (VZ64 (Int64.unsigned pte)) labd = Some labd'):
      update_smmu_page_spec_low_step s WB ((Vint vmid)::(Vint cbndx)::(Vint index)::(Vlong iova)::(Vlong pte)::nil) (m'0, labd) Vundef (m'0, labd').

  Inductive unmap_smmu_page_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | unmap_smmu_page_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' cbndx index iova
      (Hinv: high_level_invariant labd)
      (Hspec: unmap_smmu_page_spec0 (Int.unsigned cbndx) (Int.unsigned index) (VZ64 (Int64.unsigned iova)) labd = Some labd'):
      unmap_smmu_page_spec_low_step s WB ((Vint cbndx)::(Vint index)::(Vlong iova)::nil) (m'0, labd) Vundef (m'0, labd').

  Inductive mem_load_no_check_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | mem_load_no_check_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' gfn reg bypass
      (Hinv: high_level_invariant labd)
      (Hspec: mem_load_no_check_spec0 (VZ64 (Int64.unsigned gfn)) (Int.unsigned reg) (Int.unsigned bypass) labd = Some labd'):
      mem_load_no_check_spec_low_step s WB ((Vlong gfn)::(Vint reg)::(Vint bypass)::nil) (m'0, labd) Vundef (m'0, labd').

  Inductive mem_store_no_check_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps) :=
  | mem_store_no_check_spec_low_intro s (WB: _ -> Prop) m'0 labd labd' gfn reg bypass
      (Hinv: high_level_invariant labd)
      (Hspec: mem_store_no_check_spec0 (VZ64 (Int64.unsigned gfn)) (Int.unsigned reg) (Int.unsigned bypass) labd = Some labd'):
      mem_store_no_check_spec_low_step s WB ((Vlong gfn)::(Vint reg)::(Vint bypass)::nil) (m'0, labd) Vundef (m'0, labd').

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.

    Definition map_page_host_spec_low: compatsem LDATAOps :=
      csem map_page_host_spec_low_step (type_of_list_type (Tint64::nil)) Tvoid.

    Definition clear_vm_page_spec_low: compatsem LDATAOps :=
      csem clear_vm_page_spec_low_step (type_of_list_type (Tint32::Tint64::nil)) Tvoid.

    Definition assign_pfn_to_vm_spec_low: compatsem LDATAOps :=
      csem assign_pfn_to_vm_spec_low_step (type_of_list_type (Tint32::Tint64::Tint64::nil)) Tvoid.

    Definition map_pfn_vm_spec_low: compatsem LDATAOps :=
      csem map_pfn_vm_spec_low_step (type_of_list_type (Tint32::Tint64::Tint64::Tint32::nil)) Tvoid.

    Definition map_vm_io_spec_low: compatsem LDATAOps :=
      csem map_vm_io_spec_low_step (type_of_list_type (Tint32::Tint64::Tint64::nil)) Tvoid.

    Definition grant_vm_page_spec_low: compatsem LDATAOps :=
      csem grant_vm_page_spec_low_step (type_of_list_type (Tint32::Tint64::nil)) Tvoid.

    Definition revoke_vm_page_spec_low: compatsem LDATAOps :=
      csem revoke_vm_page_spec_low_step (type_of_list_type (Tint32::Tint64::nil)) Tvoid.

    Definition assign_pfn_to_smmu_spec_low: compatsem LDATAOps :=
      csem assign_pfn_to_smmu_spec_low_step (type_of_list_type (Tint32::Tint64::Tint64::nil)) Tvoid.

    Definition update_smmu_page_spec_low: compatsem LDATAOps :=
      csem update_smmu_page_spec_low_step (type_of_list_type (Tint32::Tint32::Tint32::Tint64::Tint64::nil)) Tvoid.

    Definition unmap_smmu_page_spec_low: compatsem LDATAOps :=
      csem unmap_smmu_page_spec_low_step (type_of_list_type (Tint32::Tint32::Tint64::nil)) Tvoid.

    Definition mem_load_no_check_spec_low: compatsem LDATAOps :=
      csem mem_load_no_check_spec_low_step (type_of_list_type (Tint64::Tint32::Tint32::nil)) Tvoid.

    Definition mem_store_no_check_spec_low: compatsem LDATAOps :=
      csem mem_store_no_check_spec_low_step (type_of_list_type (Tint64::Tint32::Tint32::nil)) Tvoid.

  End WITHMEM.

End MemAuxSpecLow.