x64: progress in CSpace1_R.thy

proof/refine/X64/CSpace1_R.thy

@@ -146,7 +146,7 @@ lemma obj_size_relation:
   apply (rename_tac arch_cap)
   apply (case_tac arch_cap,
     simp_all add: objBits_def X64_H.capUntypedSize_def asid_low_bits_def
-                  pageBits_def)
+                  bit_simps)
   done
 
 lemma same_region_as_relation:
@@ -291,13 +291,13 @@ lemma cap_relation_masks:
   "cap_relation c c' \<Longrightarrow> cap_relation
       (cap_rights_update (cap_rights c \<inter> rmask) c)
       (RetypeDecls_H.maskCapRights (rights_mask_map rmask) c')"
-apply (case_tac c, simp_all add: isCap_defs maskCapRights_def Let_def
+  apply (case_tac c, simp_all add: isCap_defs maskCapRights_def Let_def
                                  rights_mask_map_def maskVMRights_def
                                  AllowSend_def AllowRecv_def
                                  cap_rights_update_def
                           split del: if_split)
-apply (clarsimp simp add: isCap_defs)
-by (rule ArchAcc_R.arch_cap_rights_update
+  apply (clarsimp simp add: isCap_defs)
+  by (rule ArchAcc_R.arch_cap_rights_update
          [simplified, simplified rights_mask_map_def])
 
 lemma getCTE_wp:
@@ -422,15 +422,15 @@ lemma cap_map_update_data:
   shows   "cap_relation (update_cap_data p x c) (updateCapData p x c')"
 proof -
   note simps = update_cap_data_def updateCapData_def word_size
-               isCap_defs is_cap_defs Let_def
+               isCap_defs is_cap_defs Let_def badge_bits_def
                cap_rights_update_def badge_update_def
-  { fix x :: word32
-    def y \<equiv> "(x >> 8) && mask 18"
-    def z \<equiv> "unat ((x >> 3) && mask 5)"
-    have "of_bl (to_bl (y && mask z)) = (of_bl (replicate (32-z) False @ drop (32-z) (to_bl y))::word32)"
+  { fix x :: machine_word
+    def y \<equiv> "(x >> 8) && mask 18" (* guard_bits *)
+    def z \<equiv> "unat ((x >> 2) && mask 6)" (* cnode_padding_bits, cnode_guard_size_bits *)
+    have "of_bl (to_bl (y && mask z)) = (of_bl (replicate (64-z) False @ drop (64-z) (to_bl y))::machine_word)"
       by (simp add: bl_and_mask)
     then
-    have "y && mask z = of_bl (drop (32 - z) (to_bl y))"
+    have "y && mask z = of_bl (drop (64 - z) (to_bl y))"
       apply simp
       apply (subst test_bit_eq_iff [symmetric])
       apply (rule ext)

proof/refine/X64/Invariants_H.thy

@@ -421,7 +421,7 @@ where valid_cap'_def:
   | Structures_H.CNodeCap r bits guard guard_sz \<Rightarrow>
     bits \<noteq> 0 \<and> bits + guard_sz \<le> word_bits \<and>
     guard && mask guard_sz = guard \<and>
-    (\<forall>addr. real_cte_at' (r + 16 * (addr && mask bits)) s)
+    (\<forall>addr. real_cte_at' (r + 32 * (addr && mask bits)) s)
   | Structures_H.ThreadCap r \<Rightarrow> tcb_at' r s
   | Structures_H.ReplyCap r m \<Rightarrow> tcb_at' r s
   | Structures_H.IRQControlCap \<Rightarrow> True

proof/refine/X64/StateRelation.thy

@@ -22,7 +22,7 @@ context begin interpretation Arch . (*FIXME: arch_split*)
 definition
   cte_map :: "cslot_ptr \<Rightarrow> machine_word"
 where
- "cte_map \<equiv> \<lambda>(oref, cref). oref + (of_bl cref * 16)"
+ "cte_map \<equiv> \<lambda>(oref, cref). oref + (of_bl cref * 32)"
 
 definition
   lookup_failure_map :: "ExceptionTypes_A.lookup_failure \<Rightarrow> Fault_H.lookup_failure"