x64 refine: arch-split up to InvariantUpdates_H

Updates the rest of X64 Refine to conform to the generic arch-split
invariant interface. When things broke and when possible, we took the
proof or chunks of proof from AARCH64.

Otherwise:
- projectKOs is not in the simpset
- ioport_control/valid_arch_mdb_ctes hasn't been renamed in all cases, only
  made to work for now
- the power-of-two vs mask situation is still a mess, requiring changing
  proofs to go one way or the other
- unfolding tcb_cte_cases_def would benefit from tcb_cte_cases_neqs
  being in the simpset so that people avoid unfolding cteSizeBits when
  not necessary, but that can be done via a separate pass later

Signed-off-by: Rafal Kolanski <[email protected]>

proof/refine/X64/ArchMove_R.thy

@@ -17,7 +17,7 @@ lemmas cte_index_repair_sym = cte_index_repair[symmetric]
 
 lemmas of_nat_inj64 = of_nat_inj[where 'a=machine_word_len, folded word_bits_def]
 
-context begin interpretation Arch .
+context Arch begin arch_global_naming
 
 lemma no_fail_in8[wp]:
   "no_fail \<top> (in8 a)"

proof/refine/X64/Arch_R.thy

@@ -86,10 +86,10 @@ lemma createObject_typ_at':
   apply (unfold pspace_no_overlap'_def)
   apply (erule allE)+
   apply (erule(1) impE)
-  apply (subgoal_tac "x \<in> {x..x + 2 ^ objBitsKO y - 1}")
-   apply (fastforce simp:is_aligned_neg_mask_eq p_assoc_help)
+  apply (subgoal_tac "x \<in> mask_range x (objBitsKO y)")
+   apply (fastforce simp: is_aligned_neg_mask_eq)
   apply (drule(1) pspace_alignedD')
-  apply (clarsimp simp: is_aligned_no_wrap' p_assoc_help)
+  apply (clarsimp simp: is_aligned_no_overflow_mask)
   done
 
 lemma retype_region2_ext_retype_region_ArchObject:
@@ -210,6 +210,7 @@ lemma performASIDControlInvocation_corres:
               apply (simp add:objBits_simps archObjSize_def range_cover_full valid_cap'_def)+
             apply (fastforce elim!: canonical_address_neq_mask)
            apply (rule in_kernel_mappings_neq_mask, (simp add: valid_cap'_def bit_simps)+)[1]
+           apply (simp add: valid_cap'_def bit_simps)
           apply (clarsimp simp:valid_cap'_def)
           apply (wp createObject_typ_at'
                     createObjects_orig_cte_wp_at'[where sz = pageBits])
@@ -334,13 +335,15 @@ lemma performASIDControlInvocation_corres:
          simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2
                        null_filter_descendants_of'[OF null_filter_simp']
                        capAligned_def asid_low_bits_def)
-       apply (erule descendants_range_caps_no_overlapI')
-        apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq)
-       apply (simp add:empty_descendants_range_in')
-      apply (simp add:word_bits_def bit_simps)
-     apply (rule is_aligned_weaken)
-      apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified])
-     apply (simp add:pageBits_def)
+         apply (erule descendants_range_caps_no_overlapI')
+          apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq)
+         apply (simp add:empty_descendants_range_in')
+        apply (simp add:word_bits_def bit_simps)
+       apply (rule is_aligned_weaken)
+        apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified])
+       apply (simp add: pageBits_def)
+      apply (simp add: pageBits_def)
+     apply (simp add: pageBits_def)
     apply clarsimp
     apply (drule(1) cte_cap_in_untyped_range)
          apply (fastforce simp: cte_wp_at_ctes_of)
@@ -2035,7 +2038,7 @@ lemma performASIDControlInvocation_invs' [wp]:
       apply (wp createObjects'_wp_subst[OF
                 createObjects_no_cte_invs[where sz = pageBits and ty="Inl (KOArch (KOASIDPool pool))" for pool]]
                 createObjects_orig_cte_wp_at'[where sz = pageBits]  hoare_vcg_const_imp_lift
-         |simp add: makeObjectKO_def projectKOs asid_pool_typ_at_ext' valid_cap'_def cong: rev_conj_cong
+         |simp add: makeObjectKO_def projectKOs asid_pool_typ_at_ext' valid_cap'_def valid_arch_cap'_def cong: rev_conj_cong
          |strengthen safe_parent_strg'[where idx= "2^ pageBits"])+
       apply (rule hoare_vcg_conj_lift)
        apply (rule descendants_of'_helper)
@@ -2107,8 +2110,9 @@ lemma performASIDControlInvocation_invs' [wp]:
    apply (simp add: pageBits_def untypedBits_defs)
   apply (frule_tac cte="CTE (capability.UntypedCap False a b c) m" for a b c m in valid_global_refsD', clarsimp)
   apply (simp add: Int_commute)
+  apply (prop_tac "w1 \<in> kernel_mappings")
   by (auto simp:empty_descendants_range_in' objBits_simps max_free_index_def
-                    archObjSize_def asid_low_bits_def word_bits_def
+                    archObjSize_def asid_low_bits_def word_bits_def live'_def hyp_live'_def
                     range_cover_full descendants_range'_def2 is_aligned_mask
                     null_filter_descendants_of'[OF null_filter_simp'] bit_simps
                     valid_cap_simps' mask_def)+

proof/refine/X64/Bits_R.thy

@@ -457,7 +457,7 @@ lemma ko_at_cte_ipcbuffer:
   "ko_at' tcb p s \<Longrightarrow> cte_wp_at' (\<lambda>x. x = tcbIPCBufferFrame tcb) (p + tcbIPCBufferSlot * 0x20) s"
   apply (clarsimp simp: obj_at'_def projectKOs objBits_simps)
   apply (erule (2) cte_wp_at_tcbI')
-   apply (fastforce simp add: tcb_cte_cases_def tcbIPCBufferSlot_def)
+   apply (fastforce simp: tcb_cte_cases_def tcbIPCBufferSlot_def cteSizeBits_def)
   apply simp
   done
 

proof/refine/X64/CNodeInv_R.thy

@@ -4781,51 +4781,55 @@ lemma irq_control_n: "irq_control n"
   apply clarsimp
   done
 
+context begin interpretation Arch . (* FIXME arch-split *)
+
 lemma ioport_control_n: "ioport_control n"
   using src dest dest_derived src_derived
   apply (clarsimp simp: ioport_control_def)
   apply (frule revokable)
   apply (drule n_cap)
   apply (clarsimp split: if_split_asm)
     apply (clarsimp simp: weak_derived'_def)
-    apply (frule ioport_revocable, rule ioport_control)
+    apply (frule ioport_revocable, rule arch_mdb_ctes[simplified])
     apply clarsimp
     apply (drule n_cap)
     apply (split if_split_asm)
      apply (thin_tac "capability.ArchObjectCap X64_H.IOPortControlCap = dcap")
      apply clarsimp
     apply (clarsimp split: if_split_asm)
-     apply (drule (1) ioport_controlD, rule ioport_control)
+     apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified])
      apply simp
-    apply (drule (1) ioport_controlD, rule ioport_control)
+    apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified])
     apply simp
    apply (clarsimp simp: weak_derived'_def)
-   apply (frule ioport_revocable, rule ioport_control)
+   apply (frule ioport_revocable, rule arch_mdb_ctes[simplified])
    apply clarsimp
    apply (drule n_cap)
     apply (split if_split_asm)
      apply clarsimp
-    apply (drule (1) ioport_controlD, rule ioport_control)
+    apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified])
     apply simp
    apply (split if_split_asm)
     apply (thin_tac "capability.ArchObjectCap X64_H.IOPortControlCap = scap")
     apply clarsimp
    apply (clarsimp split: if_split_asm)
-   apply (drule (1) ioport_controlD, rule ioport_control)
+   apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified])
    apply simp
   apply (clarsimp simp: weak_derived'_def)
-  apply (frule ioport_revocable, rule ioport_control)
+  apply (frule ioport_revocable, rule arch_mdb_ctes[simplified])
   apply clarsimp
   apply (drule n_cap)
   apply (clarsimp split: if_split_asm)
-    apply (drule (1) ioport_controlD, rule ioport_control)
+    apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified])
     apply simp
-   apply (drule (1) ioport_controlD, rule ioport_control)
+   apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified])
    apply clarsimp
-  apply (drule (1) ioport_controlD, rule ioport_control)
+  apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified])
   apply clarsimp
   done
 
+end
+
 lemma distinct_zombies_m:
   "distinct_zombies m"
   using valid by auto
@@ -4872,7 +4876,7 @@ lemma cteSwap_valid_mdb_helper:
         cteSwap_chunked caps_contained untyped_mdb_n untyped_inc_n
         nullcaps_n ut_rev_n class_links_n irq_control_n ioport_control_n
         distinct_zombies_n reply_masters_rvk_fb_n
-  by (auto simp:untyped_eq)
+  by (auto simp: untyped_eq X64.valid_arch_mdb_ctes_def)
 
 end
 
@@ -5317,16 +5321,16 @@ lemma Final_notUntyped_capRange_disjoint:
   apply (clarsimp simp: cteCaps_of_def)
   apply (drule(1) ctes_of_valid')
   apply (elim disjE isCapDs[elim_format])
-   apply (clarsimp simp: valid_cap'_def bit_simps
+   apply (clarsimp simp: valid_cap'_def bit_simps valid_arch_cap'_def
                          obj_at'_def projectKOs objBits_simps'
-                         typ_at'_def ko_wp_at'_def
+                         typ_at'_def ko_wp_at'_def live'_def
                   split: capability.split_asm zombie_type.split_asm
                          arch_capability.split_asm
                   dest!: spec[where x=0])
      apply (clarsimp simp: sameObjectAs_def3 isCap_simps)
     apply (simp add: isCap_simps)
    apply (simp add: isCap_simps)
-  apply (clarsimp simp: valid_cap'_def bit_simps
+  apply (clarsimp simp: valid_cap'_def bit_simps valid_arch_cap'_def
                         obj_at'_def projectKOs objBits_simps
                         typ_at'_def ko_wp_at'_def pd_pointer_table_at'_def
                         page_table_at'_def page_directory_at'_def
@@ -5644,7 +5648,7 @@ lemma make_zombie_invs':
                                \<and> bound_tcb_at' ((=) None) p' s
                                \<and> obj_at' (\<lambda>tcb. tcbSchedNext tcb = None
                                                 \<and> tcbSchedPrev tcb = None) p' s")
-    apply (clarsimp simp: pred_tcb_at'_def obj_at'_def ko_wp_at'_def projectKOs)
+    apply (clarsimp simp: pred_tcb_at'_def obj_at'_def ko_wp_at'_def projectKOs live'_def hyp_live'_def)
    apply (auto dest!: isCapDs)[1]
   apply (clarsimp simp: cte_wp_at_ctes_of disj_ac
                  dest!: isCapDs)
@@ -5759,7 +5763,7 @@ lemma shrink_zombie_invs':
   apply clarsimp
   apply (rule ccontr, erule notE, rule imageI)
   apply (drule word_le_minus_one_leq)
-  apply (rule ccontr, simp add: linorder_not_less mult.commute mult.left_commute)
+  apply (rule ccontr, simp add: linorder_not_less mult.commute mult.left_commute shiftl_t2n)
   done
 
 lemma setQueue_cte_wp_at':
@@ -5809,6 +5813,7 @@ crunch doMachineOp
 
 lemma valid_Zombie_cte_at':
   "\<lbrakk> s \<turnstile>' Zombie p zt m; n < zombieCTEs zt \<rbrakk> \<Longrightarrow> cte_at' (p + (of_nat n * 2^cteSizeBits)) s"
+  supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *)
   apply (clarsimp simp: valid_cap'_def split: zombie_type.split_asm)
    apply (clarsimp simp: obj_at'_def projectKOs objBits_simps)
    apply (subgoal_tac "tcb_cte_cases (of_nat n * 2^cteSizeBits) \<noteq> None")
@@ -6070,7 +6075,7 @@ lemma ex_Zombie_to2:
   apply (intro exI, rule conjI, assumption)
   apply (simp add: image_def)
   apply (rule bexI[where x="of_nat n - 1"])
-   apply (fastforce simp: objBits_defs)
+   apply (fastforce simp: objBits_defs shiftl_t2n)
   apply (subgoal_tac "n \<in> unats (len_of TYPE(machine_word_len))")
    apply (simp add: word_less_nat_alt)
    apply (subst unat_minus_one)
@@ -6270,7 +6275,8 @@ proof (induct arbitrary: P p rule: finalise_spec_induct2)
                      \<or> (\<exists>zb n cp. cteCap cte = Zombie q zb n
                           \<and> Q cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> q))"
   note hyps = "1.hyps"[folded reduceZombie_def[unfolded cteDelete_def finaliseSlot_def]]
-  have Q: "\<And>x y n. {x :: machine_word} = (\<lambda>x. y + x * 2^cteSizeBits) ` {0 ..< n} \<Longrightarrow> n = 1"
+  have Q: "\<And>x y n. {x :: machine_word} = (\<lambda>x. y + (x << cteSizeBits)) ` {0 ..< n} \<Longrightarrow> n = 1"
+    apply (simp only: shiftl_t2n mult_ac)
     apply (drule sym)
     apply (case_tac "1 < n")
      apply (frule_tac x = "y + 0 * 2^cteSizeBits" in eqset_imp_iff)
@@ -6373,14 +6379,15 @@ proof (induct arbitrary: P p rule: finalise_spec_induct2)
                simp_all add: isCap_simps removeable'_def
                              fun_eq_iff[where f="cte_refs' cap" for cap]
                              fun_eq_iff[where f=tcb_cte_cases]
-                             tcb_cte_cases_def)[1]
-         apply (frule Q)
+                             tcb_cte_cases_def cteSizeBits_def)[1]
+         apply (frule Q[unfolded cteSizeBits_def, simplified])
          apply clarsimp
+        apply (simp add: mask_def)
         apply (subst(asm) R)
          apply (drule valid_capAligned [OF ctes_of_valid'])
           apply fastforce
          apply (simp add: capAligned_def word_bits_def)
-        apply (frule Q)
+         apply (frule Q[unfolded cteSizeBits_def, simplified])
         apply clarsimp
        apply (clarsimp simp: cte_wp_at_ctes_of capRemovable_def)
        apply (subgoal_tac "final_matters' (cteCap rv) \<and> \<not> isUntypedCap (cteCap rv)")
@@ -7449,7 +7456,7 @@ next
     apply (rule_tac x="cte_map slot" in exI)
     apply (clarsimp simp: image_def)
     apply (rule_tac x="of_nat n" in bexI)
-     apply (fastforce simp: cte_level_bits_def objBits_defs mult.commute mult.left_commute)
+     apply (fastforce simp: cte_level_bits_def shiftl_t2n objBits_defs mult.commute mult.left_commute)
     apply simp
     apply (subst field_simps, rule plus_one_helper2)
      apply simp
@@ -8486,26 +8493,26 @@ proof
     apply (erule (1) irq_controlD, rule irq_control)
     done
 
-  show "ioport_control m'" using src dest parency
+  show "valid_arch_mdb_ctes m'" using src dest parency
     apply (clarsimp simp: ioport_control_def)
     apply (frule m'_revocable)
     apply (drule m'_cap)
     apply (clarsimp split: if_split_asm)
      apply (clarsimp simp add: weak_derived'_def)
-     apply (frule ioport_revocable, rule ioport_control)
+     apply (frule ioport_revocable, rule arch_mdb_ctes[simplified])
      apply clarsimp
      apply (drule m'_cap)
      apply (clarsimp split: if_split_asm)
-     apply (drule (1) ioport_controlD, rule ioport_control)
+     apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified])
      apply simp
-    apply (frule ioport_revocable, rule ioport_control)
+    apply (frule ioport_revocable, rule arch_mdb_ctes[simplified])
     apply clarsimp
     apply (drule m'_cap)
     apply (clarsimp split: if_split_asm)
      apply (clarsimp simp: weak_derived'_def)
-     apply (drule (1) ioport_controlD, rule ioport_control)
+     apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified])
      apply simp
-    apply (erule (1) ioport_controlD, rule ioport_control)
+    apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified])
     done
 
   have distz: "distinct_zombies m"