x64: spec+refine: remove VMIOSpaceMap, tighten valid_cap' map type guarantees

proof/refine/X64/Arch_R.thy

@@ -704,7 +704,6 @@ lemma decode_page_inv_corres:
    apply (case_tac excaps', simp)
    apply clarsimp
    apply (rule corres_guard_imp)
-     apply (rule whenE_throwError_corres, simp, simp)
      apply (rule corres_splitEE [where r' = "op ="])
         prefer 2
         apply (clarsimp simp: list_all2_Cons2)

proof/refine/X64/Invariants_H.thy

@@ -443,7 +443,7 @@ where valid_cap'_def:
     (\<forall>p < 2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT)
     (ref + p * 2 ^ pageBits) s) \<and>
     (case mapdata of None \<Rightarrow> (t=VMNoMap) | Some (asid, ref) \<Rightarrow>
-            0 < asid \<and> asid_wf asid \<and> vmsz_aligned' ref sz \<and> ref < pptrBase)
+            (t = VMVSpaceMap) \<and> 0 < asid \<and> asid_wf asid \<and> vmsz_aligned' ref sz \<and> ref < pptrBase)
   | PageTableCap ref mapdata \<Rightarrow>
     page_table_at' ref s \<and>
     (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow>

spec/abstract/X64/ArchDecode_A.thy

@@ -363,7 +363,8 @@ where
                   attr = args ! 1;
                   vspace_cap = fst (extra_caps ! 0)
          in doE
-             whenE (map_type = VMIOSpaceMap) $ throwError IllegalOperation;
+             (* FIXME x64-vtd: *)
+             (* whenE (map_type = VMIOSpaceMap) $ throwError IllegalOperation; *)
              (vspace,asid) \<leftarrow> (case vspace_cap of
                                   ArchObjectCap (PML4Cap pm (Some asid)) \<Rightarrow>
                                         returnOk (pm, asid)

spec/haskell/src/SEL4/Kernel/VSpace/X64.lhs

@@ -556,7 +556,8 @@ Note that implementations with separate high and low memory regions may also wis
 >                 pageMapVSpace = vspace }
 >         (ArchInvocationLabel X64PageMap, _, _) -> throw TruncatedMessage
 >         (ArchInvocationLabel X64PageRemap, rightsMask:attr:_, (vspaceCap,_):_) -> do
->             when (capVPMapType cap == VMIOSpaceMap) $ throw IllegalOperation
+>--           FIXME x64-vtd:
+>--           when (capVPMapType cap == VMIOSpaceMap) $ throw IllegalOperation
 >             (vspace,asid) <- case vspaceCap of
 >                 ArchObjectCap (PML4Cap {
 >                         capPML4MappedASID = Just asid,

spec/haskell/src/SEL4/Machine/Hardware/X64.lhs

@@ -523,7 +523,8 @@ Page entries -- any of PTEs, PDEs or PDPTEs.
 > data VMMapType
 >     = VMNoMap
 >     | VMVSpaceMap
->     | VMIOSpaceMap
+>--   FIXME x64-vtd:
+>--   | VMIOSpaceMap
 >     deriving (Show, Eq, Enum)
 
 > data VMRights