isabelle2021-1 riscv: Infoflow

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2022-01-21 13:17:30 +11:00 · 2022-01-21 13:17:30 +11:00 · bf8431d765
parent 6c938f2a35
commit bf8431d765
1 changed files with 2 additions and 97 deletions
--- a/proof/infoflow/RISCV64/Example_Valid_State.thy
+++ b/proof/infoflow/RISCV64/Example_Valid_State.thy
@ -1345,103 +1345,8 @@ lemma pspace_distinct_s0:
   apply (drule irq_node_offs_range_correct)+
   apply clarsimp
   apply (clarsimp simp: s0_ptr_defs cte_level_bits_def)
-   apply (case_tac "(ucast irq << 5) < (ucast irqa << 5)")
-    apply (frule udvd_decr'[where K="0x20::obj_ref" and ua=0, simplified])
-       apply (simp add: shiftl_t2n uint_word_ariths)
-       apply (subst mod_mult_mult1[where c="2^5" and b="2^59", simplified])
-       apply simp
-      apply (simp add: shiftl_t2n uint_word_ariths)
-      apply (subst mod_mult_mult1[where c="2^5" and b="2^59", simplified])
-      apply simp
-     apply (simp add: uint_shiftl word_size bintrunc_shiftl)
-     apply (simp add: shiftl_int_def take_bit_eq_mod)
-    apply (frule_tac y="ucast irq << 5" in word_plus_mono_right[where x="0xFFFFFFC00000301F"])
-     apply (simp add: shiftl_t2n)
-     apply (case_tac "(1::obj_ref) \<le> ucast irqa")
-      apply (drule_tac i=1 and k="0x20" in word_mult_le_mono1)
-        apply simp
-       apply (cut_tac x=irqa and 'a=64 in ucast_less)
-        apply simp
-       apply (simp add: word_less_nat_alt)
-      apply (simp add: mult.commute)
-      apply (drule_tac y="0x20" and x="0xFFFFFFC000002FFF" in word_plus_mono_right)
-       apply (rule_tac sz=59 in machine_word_plus_mono_right_split)
-        apply (simp add: unat_word_ariths mask_def)
-        apply (cut_tac x=irqa and 'a=64 in ucast_less)
-         apply simp
-        apply (simp add: word_less_nat_alt)
-       apply (simp add: word_bits_def)
-      apply simp
-     apply (simp add: lt1_neq0)
-    apply (drule(1) order_trans_rules(23))
-    apply clarsimp
-    apply (drule_tac a="0xFFFFFFC000003000 + (ucast irqa << 5)" and b="ucast irqa << 5"
-                 and c="0xFFFFFFC000002FFF + (ucast irqa << 5)" and d="ucast irqa << 5" in word_sub_mono)
-       apply simp
-      apply simp
-      apply (rule_tac sz=59 in machine_word_plus_mono_right_split)
-       apply (simp add: unat_word_ariths mask_def shiftl_t2n)
-       apply (cut_tac x=irqa and 'a=64 in ucast_less)
-        apply simp
-       apply (simp add: word_less_nat_alt)
-      apply (simp add: word_bits_def)
-     apply simp
-     apply (rule_tac sz=59 in machine_word_plus_mono_right_split)
-      apply (simp add: unat_word_ariths mask_def shiftl_t2n)
-      apply (cut_tac x=irqa and 'a=64 in ucast_less)
-       apply simp
-      apply (simp add: word_less_nat_alt)
-     apply (simp add: word_bits_def)
-    apply simp
-   apply (case_tac "(ucast irq << 5) > (ucast irqa << 5)")
-    apply (frule udvd_decr'[where K="0x20 :: obj_ref" and ua=0, simplified])
-       apply (simp add: shiftl_t2n uint_word_ariths)
-       apply (subst mod_mult_mult1[where c="2^5" and b="2^59", simplified])
-       apply simp
-      apply (simp add: shiftl_t2n uint_word_ariths)
-      apply (subst mod_mult_mult1[where c="2^5" and b="2^59", simplified])
-      apply simp
-     apply (simp add: uint_shiftl word_size bintrunc_shiftl)
-     apply (simp add: shiftl_int_def take_bit_eq_mod)
-    apply (frule_tac y="ucast irqa << 5" in word_plus_mono_right[where x="0xFFFFFFC00000301F"])
-     apply (simp add: shiftl_t2n)
-     apply (case_tac "(1::obj_ref) \<le> ucast irq")
-      apply (drule_tac i=1 and k="0x20" in word_mult_le_mono1)
-        apply simp
-       apply (cut_tac x=irq and 'a=64 in ucast_less)
-        apply simp
-       apply (simp add: word_less_nat_alt)
-      apply (simp add: mult.commute)
-      apply (drule_tac y="0x20" and x="0xFFFFFFC000002FFF" in word_plus_mono_right)
-       apply (rule_tac sz=28 in machine_word_plus_mono_right_split)
-        apply (simp add: unat_word_ariths mask_def)
-        apply (cut_tac x=irq and 'a=64 in ucast_less)
-         apply simp
-        apply (simp add: word_less_nat_alt)
-       apply (simp add: word_bits_def)
-      apply simp
-     apply (simp add: lt1_neq0)
-    apply (drule(1) order_trans_rules(23))
-    apply clarsimp
-    apply (drule_tac a="0xFFFFFFC000003000 + (ucast irq << 5)" and b="ucast irq << 5"
-                 and c="0xFFFFFFC000002FFF + (ucast irq << 5)" and d="ucast irq << 5" in word_sub_mono)
-       apply simp
-      apply simp
-      apply (rule_tac sz=59 in machine_word_plus_mono_right_split)
-       apply (simp add: unat_word_ariths mask_def shiftl_t2n)
-       apply (cut_tac x=irq and 'a=64 in ucast_less)
-        apply simp
-       apply (simp add: word_less_nat_alt)
-      apply (simp add: word_bits_def)
-     apply simp
-     apply (rule_tac sz=59 in machine_word_plus_mono_right_split)
-      apply (simp add: unat_word_ariths mask_def shiftl_t2n)
-      apply (cut_tac x=irq and 'a=64 in ucast_less)
-       apply simp
-      apply (simp add: word_less_nat_alt)
-     apply (simp add: word_bits_def)
-    apply simp
-   apply simp
+   apply word_bitwise
+   apply auto[1]
  apply (elim disjE)
  (* slow *)
  by (simp | clarsimp simp: kh0_obj_def cte_level_bits_def s0_ptr_defs pte_bits_def bit_simps