diff --git a/proof/crefine/X64/Arch_C.thy b/proof/crefine/X64/Arch_C.thy index 3334d0d3e..7ffe58826 100644 --- a/proof/crefine/X64/Arch_C.thy +++ b/proof/crefine/X64/Arch_C.thy @@ -5119,7 +5119,7 @@ lemma invokeX86PortControl_ccorres: apply (clarsimp simp: is_simple_cap'_def isCap_simps invs_mdb' invs_valid_objs' invs_pspace_aligned' invs_pspace_canonical' valid_cap_simps' capAligned_def word_bits_def) apply (rule conjI) - apply (clarsimp simp: Collect_const_mem cap_io_port_cap_lift ccap_relation_def cap_to_H_def mask_def) + apply (clarsimp simp: cap_io_port_cap_lift ccap_relation_def cap_to_H_def mask_def) apply word_bitwise apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def global_ioport_bitmap_relation_def Let_def typ_heap_simps) diff --git a/proof/crefine/X64/CSpace_C.thy b/proof/crefine/X64/CSpace_C.thy index 8dc70a6ba..738e39499 100644 --- a/proof/crefine/X64/CSpace_C.thy +++ b/proof/crefine/X64/CSpace_C.thy @@ -850,12 +850,12 @@ lemma ccorres_cases: done (* FIXME: move *) -lemma word_and_le': "\ b \ c \ \ (a :: machine_word) && b \ c" +lemma word_and_le': "\ b \ c \ \ (a :: 'a::len word) && b \ c" apply (metis word_and_le1 order_trans) done (* FIXME: move *) -lemma word_and_less': "\ b < c \ \ (a :: machine_word) && b < c" +lemma word_and_less': "\ b < c \ \ (a :: 'a::len word) && b < c" apply (metis word_and_le1 xtr7) done @@ -2042,24 +2042,639 @@ where "cleanup_info_wf' cap \ case cap of IRQHandlerCap irq \ UCAST(8\16) irq \ SCAST(32 signed\16) Kernel_C.maxIRQ | ArchObjectCap acap \ arch_cleanup_info_wf' acap | _ \ True" +(* FIXME: move *) +lemma hrs_mem_update_compose: + "hrs_mem_update f (hrs_mem_update g h) = hrs_mem_update (f \ g) h" + by (auto simp: hrs_mem_update_def split: prod.split) + +(* FIXME: move *) +lemma packed_heap_update_collapse': + fixes p :: "'a::packed_type ptr" + shows "heap_update p v \ heap_update p u = heap_update p v" + by (auto simp: packed_heap_update_collapse) + +(* FIXME: move *) +lemma access_array_from_elements: + fixes v :: "'a::packed_type['b::finite]" + assumes "\i < CARD('b). h_val h (array_ptr_index p False i) = v.[i]" + shows "h_val h p = v" + by (rule cart_eq[THEN iffD2]) (simp add: assms heap_access_Array_element') + +(* FIXME: move *) +lemma h_val_foldr_heap_update: + fixes v :: "'i \ 'a::mem_type" + assumes "\x y. {x,y} \ set xs \ x \ y \ ptr_span (p x) \ ptr_span (p y) = {}" + assumes "distinct xs" "i \ set xs" + shows "h_val (foldr (\i. heap_update (p i) (v i)) xs h) (p i) = v i" + using assms by (induct xs arbitrary: h; + fastforce simp: h_val_heap_update h_val_update_regions_disjoint) + +(* FIXME: move *) +lemma ptr_span_array_ptr_index_disjoint: + fixes p :: "('a::packed_type['b::finite]) ptr" + assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" + assumes b: "x < CARD('b)" "y < CARD('b)" + assumes n: "x \ y" + shows "ptr_span (array_ptr_index p False x) \ ptr_span (array_ptr_index p False y) = {}" + proof - + have l: "CARD('b) * size_of TYPE('a) \ 2 ^ LENGTH(64)" using s by simp + have p: "\x k. x < CARD('b) \ k < size_of TYPE('a) + \ x * size_of TYPE('a) + k < 2 ^ LENGTH(64)" + by (metis less_le_trans[OF _ l] Divides.mod_less Fields.sign_simps(5) mod_lemma + zero_less_card_finite) + show ?thesis + apply (clarsimp simp: array_ptr_index_def ptr_add_def intvl_disj_offset) + apply (rule disjointI) + apply (clarsimp simp: intvl_def) + apply (subst (asm) of_nat_mult[symmetric])+ + apply (subst (asm) of_nat_add[symmetric])+ + apply (subst (asm) of_nat_inj[OF p p]; (simp add: b)?) + apply (drule arg_cong[where f="\x. x div size_of TYPE('a)"]; simp add: n) + done + qed + +(* FIXME: move *) +lemma h_val_heap_update_Array: + fixes v :: "'a::packed_type['b::finite]" + assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" + shows "h_val (heap_update p v h) p = v" + apply (rule access_array_from_elements) + apply (clarsimp simp: heap_update_Array foldl_conv_foldr) + apply (rule h_val_foldr_heap_update; clarsimp simp: ptr_span_array_ptr_index_disjoint[OF s]) + done + +(* FIXME: move *) +lemma foldr_heap_update_commute: + assumes "\y. y \ set xs \ ptr_span q \ ptr_span (p y) = {}" + shows "foldr (\i. heap_update (p i) (v i)) xs (heap_update q u h) + = heap_update q u (foldr (\i. heap_update (p i) (v i)) xs h)" + using assms by (induct xs) (auto simp: LemmaBucket_C.heap_update_commute) + +(* FIXME: move *) +lemma foldr_packed_heap_update_collapse: + fixes u v :: "'i \ 'a::packed_type" + assumes "\x y. {x,y} \ set xs \ y \ x \ ptr_span (p x) \ ptr_span (p y) = {}" + assumes "distinct xs" + shows "foldr (\i. heap_update (p i) (v i)) xs (foldr (\i. heap_update (p i) (u i)) xs h) + = foldr (\i. heap_update (p i) (v i)) xs h" + using assms + apply - + apply (induct xs arbitrary: h; clarsimp; rename_tac x xs h) + apply (drule_tac x=x in spec; clarsimp) + apply (subst foldr_heap_update_commute; clarsimp simp: packed_heap_update_collapse) + apply (drule_tac x=y in spec; clarsimp) + done + +(* FIXME: move *) +lemma packed_Array_heap_update_collapse: + fixes p :: "('a::packed_type['b::finite]) ptr" + assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" + shows "heap_update p v (heap_update p u h) = heap_update p v h" + by (simp add: heap_update_Array foldl_conv_foldr foldr_packed_heap_update_collapse + ptr_span_array_ptr_index_disjoint[OF s]) + +(* FIXME: move *) +lemma packed_Array_heap_update_collapse': + fixes p :: "('a::packed_type['b::finite]) ptr" + assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" + shows "heap_update p v \ heap_update p u = heap_update p v" + by (auto simp: packed_Array_heap_update_collapse[OF s]) + +(* FIXME: move *) +definition + heap_modify :: "'a::c_type ptr \ ('a \ 'a) \ heap_mem \ heap_mem" +where + "heap_modify p f \ \h. heap_update p (f (h_val h p)) h" + +(* FIXME: move *) +lemma heap_modify_def2: + "heap_modify (p::'a::c_type ptr) f \ + \h. let bytes = heap_list h (size_of TYPE('a)) (ptr_val p) in + heap_update_list (ptr_val p) (to_bytes (f (from_bytes bytes)) bytes) h" + by (simp add: heap_modify_def Let_def heap_update_def h_val_def) + +(* FIXME: move *) +lemma heap_modify_compose: + fixes p :: "'a::packed_type ptr" + shows "heap_modify p f \ heap_modify p g = heap_modify p (f \ g)" + and "heap_modify p f (heap_modify p g h) = heap_modify p (f \ g) h" + by (auto simp: heap_modify_def h_val_heap_update packed_heap_update_collapse) + +(* FIXME: move *) +lemma heap_modify_compose_Array: + fixes p :: "('a::packed_type['b::finite]) ptr" + assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" + shows "heap_modify p f \ heap_modify p g = heap_modify p (f \ g)" + and "heap_modify p f (heap_modify p g h) = heap_modify p (f \ g) h" + by (auto simp: heap_modify_def h_val_heap_update_Array[OF s] + packed_Array_heap_update_collapse[OF s]) + +(* FIXME: move *) +lemma fold_heap_modify_commute: + fixes p :: "'a::packed_type ptr" + shows "fold (heap_modify p \ f) upds = heap_modify p (fold f upds)" + apply (induction upds) + apply (simp add: heap_modify_def heap_update_id) + apply (clarsimp simp: heap_modify_compose[THEN fun_cong, simplified] o_def) + done + +(* FIXME: move *) +lemma fold_heap_modify_commute_Array: + fixes p :: "('a::packed_type['b::finite]) ptr" + assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" + shows "fold (heap_modify p \ f) upds = heap_modify p (fold f upds)" + apply (induction upds) + apply (simp add: heap_modify_def heap_update_id_Array) + apply (clarsimp simp: heap_modify_compose_Array[OF s, THEN fun_cong, simplified] o_def) + done + +(* FIXME: move *) +lemma msb_le_mono: + fixes v w :: "'a::len word" + shows "v \ w \ msb v \ msb w" + by (simp add: msb_big) + +(* FIXME: move *) +lemma neg_msb_le_mono: + fixes v w :: "'a::len word" + shows "v \ w \ \ msb w \ \ msb v" + by (simp add: msb_big) + +(* FIXME: move *) +lemmas msb_less_mono = msb_le_mono[OF less_imp_le] +lemmas neg_msb_less_mono = neg_msb_le_mono[OF less_imp_le] + +(* FIXME: move *) +lemma word_sless_iff_less: + "\ \ msb v; \ msb w \ \ v v < w" + by (simp add: word_sless_alt sint_eq_uint word_less_alt) + +(* FIXME: move *) +lemmas word_sless_imp_less = word_sless_iff_less[THEN iffD1, rotated 2] +lemmas word_less_imp_sless = word_sless_iff_less[THEN iffD2, rotated 2] + +(* FIXME: move *) +lemma word_sle_iff_le: + "\ \ msb v; \ msb w \ \ v <=s w \ v \ w" + by (simp add: word_sle_def sint_eq_uint word_le_def) + +(* FIXME: move *) +lemmas word_sle_imp_le = word_sle_iff_le[THEN iffD1, rotated 2] +lemmas word_le_imp_sle = word_sle_iff_le[THEN iffD2, rotated 2] + +(* FIXME: move to Word_Lib *) +lemma word_upcast_shiftr: + assumes "LENGTH('a::len) \ LENGTH('b::len)" + shows "UCAST('a \ 'b) (w >> n) = UCAST('a \ 'b) w >> n" + apply (intro word_eqI impI iffI; clarsimp simp: word_size nth_shiftr nth_ucast) + apply (drule test_bit_size) + using assms by (simp add: word_size) + +lemma word_upcast_neg_msb: + "LENGTH('a::len) < LENGTH('b::len) \ \ msb (UCAST('a \ 'b) w)" + apply (clarsimp simp: ucast_def msb_word_of_int) + apply (drule bin_nth_uint_imp) + by simp + +(* FIXME: move to Word_Lib *) +lemma word_upcast_0_sle: + "LENGTH('a::len) < LENGTH('b::len) \ 0 <=s UCAST('a \ 'b) w" + by (simp add: word_sle_iff_le[OF word_msb_0 word_upcast_neg_msb]) + +(* FIXME: move to Word_Lib *) +lemma scast_ucast_up_eq_ucast: + assumes "LENGTH('a::len) < LENGTH('b::len)" + shows "SCAST('b \ 'c) (UCAST('a \ 'b) w) = UCAST('a \ 'c::len) w" + using assms + apply (subst scast_eq_ucast; simp) + apply (clarsimp simp: ucast_def msb_word_of_int) + apply (drule bin_nth_uint_imp) + apply simp + done + +lemma not_max_word_iff_less: + "w \ max_word \ w < max_word" + by (simp add: order_less_le) + +lemma ucast_increment: + assumes "w \ max_word" + shows "UCAST('a::len \ 'b::len) w + 1 = UCAST('a \ 'b) (w + 1)" + apply (cases "LENGTH('b) \ LENGTH('a)") + apply (simp add: ucast_down_add is_down) + apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('a)") + apply (subgoal_tac "uint w + 1 < 2 ^ LENGTH('b)") + apply (subst word_uint_eq_iff) + apply (simp add: uint_arith_simps uint_up_ucast is_up) + apply (erule less_trans, rule power_strict_increasing, simp, simp) + apply (subst less_diff_eq[symmetric]) + using assms + apply (simp add: not_max_word_iff_less word_less_alt) + apply (erule less_le_trans) + apply (simp add: max_word_def) + done + +lemma max_word_gt_0: + "0 < max_word" + by (simp add: le_neq_trans[OF max_word_max] max_word_not_0) + +lemma and_not_max_word: + "m \ max_word \ w && m \ max_word" + by (simp add: not_max_word_iff_less word_and_less') + +lemma mask_not_max_word: + "m < LENGTH('a::len) \ mask m \ (max_word :: 'a word)" + by (metis shiftl_1_not_0 shiftl_mask_is_0 word_bool_alg.conj_one_right) + +lemmas and_mask_not_max_word = + and_not_max_word[OF mask_not_max_word] + +lemma shiftr_not_max_word: + "0 < n \ w >> n \ max_word" + apply (simp add: not_max_word_iff_less) + apply (cases "n < size w") + apply (cases "w = 0") + apply (simp add: max_word_gt_0) + apply (subst shiftr_div_2n_w, assumption) + apply (rule less_le_trans[OF div_less_dividend_word max_word_max]) + apply simp + apply (metis word_size_gt_0 less_numeral_extra(3) mask_def nth_mask power_0 shiftl_t2n) + apply (simp add: not_less word_size) + apply (subgoal_tac "w >> n = 0"; simp add: max_word_gt_0 shiftr_eq_0) + done + +lemma word_sandwich1: + fixes a b c :: "'a::len word" + assumes "a < b" + assumes "b <= c" + shows "0 < b - a \ b - a <= c" + using assms diff_add_cancel order_less_irrefl add_0 word_le_imp_diff_le + word_le_less_eq word_neq_0_conv + by metis + +lemma word_sandwich2: + fixes a b :: "'a::len word" + assumes "0 < a" + assumes "a <= b" + shows "b - a < b" + using assms less_le_trans word_diff_less + by blast + +lemma make_pattern_spec: + defines "bits \ 0x40 :: 32 sword" + notes word_less_imp_less_0 = revcut_rl[OF word_less_imp_sless[OF _ word_msb_0]] + notes word_le_imp_le_0 = revcut_rl[OF word_le_imp_sle[OF _ word_msb_0]] + shows + "\\. \ \ + {s. s = \ \ start___int_' s < end___int_' s + \ end___int_' s \ bits } + Call make_pattern_'proc + {t. ret__unsigned_long_' t = + mask (unat (end___int_' \)) && ~~ mask (unat (start___int_' \))}" + apply (rule allI, rule conseqPre, hoare_rule HoarePartial.ProcNoRec1, vcg, clarsimp) + apply (fold bits_def) + subgoal for \ + apply (frule (1) word_sandwich1[of "start___int_' \" "end___int_' \" bits]; clarsimp) + apply (frule (1) word_sandwich2[of "end___int_' \ - start___int_' \" bits]) + apply (subgoal_tac "\ msb bits") + prefer 2 subgoal by (simp add: bits_def) + apply (frule (1) neg_msb_le_mono[of "end___int_' \"]) + apply (frule (1) neg_msb_less_mono[of "start___int_' \"]) + apply (frule (1) neg_msb_le_mono[of "end___int_' \ - start___int_' \"]) + apply (frule (1) neg_msb_less_mono[of "bits - (end___int_' \ - start___int_' \)"]) + apply (rule word_le_imp_le_0[of "start___int_' \"], simp, simp) + apply (frule (2) word_less_imp_sless[of "start___int_' \" "end___int_' \"]) + apply (frule (2) word_le_imp_sle[of "end___int_' \" bits]) + apply (rule word_less_imp_less_0[of "end___int_' \ - start___int_' \"], simp, simp) + apply (frule (2) word_le_imp_sle[of "end___int_' \ - start___int_' \" bits]) + apply (rule word_le_imp_le_0[of "bits - (end___int_' \ - start___int_' \)"], simp, simp) + apply (frule (2) word_less_imp_sless[of "bits - (end___int_' \ - start___int_' \)" bits]) + apply (intro conjI; (fastforce simp: word_sle_def word_sless_def bits_def | simp)?) + apply (subgoal_tac "start___int_' \ \ bits - (end___int_' \ - start___int_' \)") + prefer 2 + apply (meson le_minus_minus order.strict_implies_order order_trans word_le_minus_mono_left) + apply (simp add: shiftr_shiftl1 word_le_nat_alt[symmetric] unat_sub[symmetric] max_word_mask) + apply (subst shiftr_mask2, simp) + apply (simp add: unat_sub word_le_nat_alt bits_def) + done + done + +definition + word_set_or_clear :: "bool \ 'a::len word \ 'a::len word \ 'a::len word" +where + "word_set_or_clear s p w \ if s then w || p else w && ~~ p" + +lemma apply_pattern_spec: + "\\. \ \ + {s. s = \ \ s \\<^sub>c w___ptr_to_unsigned_long_' \} + Call apply_pattern_'proc + {globals_update + (t_hrs_'_update + (hrs_mem_update + (heap_update (w___ptr_to_unsigned_long_' \) + (word_set_or_clear (to_bool (set_' \)) + (pattern_' \) + (h_val (hrs_mem (t_hrs_' (globals \))) + (w___ptr_to_unsigned_long_' \)))))) \}" + apply (rule allI, rule conseqPre, hoare_rule HoarePartial.ProcNoRec1, vcg) + apply (clarsimp simp: word_set_or_clear_def to_bool_def) + done + +(* FIXME: move *) +lemma whileAnno_subst_invariant: + "whileAnno b I' V c = whileAnno b I V c" + by (simp add: whileAnno_def) + +abbreviation + ioport_table_ptr_coerce :: "'a ptr \ ioport_table_C ptr" +where + "ioport_table_ptr_coerce \ ptr_coerce" + +lemma hoarep_conseq_spec_state: + fixes \ :: "'p \ ('s,'p,'f) com option" + assumes "\\. \ \ {s. s = \ \ P s} c (Q \)" + assumes "\\. \ \ P' \ P \ \ Q \ \ Q'" + shows "\ \ P' c Q'" + using assms by (fastforce intro: hoarep.Conseq) + +lemma hrs_simps: + "hrs_mem (mem, htd) = mem" + "hrs_mem_update f (mem, htd) = (f mem, htd)" + "hrs_htd (mem, htd) = htd" + "hrs_htd_update g (mem, htd) = (mem, g htd)" + by (auto simp: hrs_mem_def hrs_mem_update_def hrs_htd_def hrs_htd_update_def) + +lemma clift_heap_modify_same: + fixes p :: "'a :: mem_type ptr" + assumes "hrs_htd hp \\<^sub>t p" + assumes "typ_uinfo_t TYPE('a) \\<^sub>t typ_uinfo_t TYPE('b)" + shows "clift (hrs_mem_update (heap_modify p f) hp) = (clift hp :: 'b :: mem_type typ_heap)" + using assms unfolding hrs_mem_update_def + apply (cases hp) + apply (simp add: split_def hrs_htd_def heap_modify_def) + apply (erule lift_t_heap_update_same) + apply simp + done + +lemma zero_ranges_are_zero_modify[simp]: + "h_t_valid (hrs_htd hrs) c_guard (ptr :: 'a ptr) + \ typ_uinfo_t TYPE('a :: wf_type) \ typ_uinfo_t TYPE(word8) + \ zero_ranges_are_zero rs (hrs_mem_update (heap_modify ptr f) hrs) + = zero_ranges_are_zero rs hrs" + apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update + intro!: ball_cong[OF refl] conj_cong[OF refl]) + apply (drule region_actually_is_bytes) + apply (drule(2) region_is_bytes_disjoint) + apply (simp add: heap_modify_def heap_update_def heap_list_update_disjoint_same Int_commute) + done + +lemma h_val_heap_modify: + fixes p :: "'a::mem_type ptr" + shows "h_val (heap_modify p f h) p = f (h_val h p)" + by (simp add: heap_modify_def h_val_heap_update) + +lemma array_fupdate_index: + fixes arr :: "'a::c_type['b::finite]" + assumes "i < CARD('b)" "j < CARD('b)" + shows "fupdate i f arr.[j] = (if i = j then f (arr.[i]) else arr.[j])" + using assms by (cases "i = j"; simp add: fupdate_def) + +lemma foldl_map_pair_constant: + "foldl (\acc p. f acc (fst p) (snd p)) z (map (\x. (x,v)) xs) = foldl (\acc x. f acc x v) z xs" + by (induct xs arbitrary: z) auto + +lemma word_set_or_clear_test_bit: + fixes w :: "'a::len word" + shows "i < LENGTH('a) \ word_set_or_clear b p w !! i = (if p !! i then b else w !! i)" + by (auto simp: word_set_or_clear_def word_ops_nth_size word_size split: if_splits) + +lemma unat_and_mask_less_2p: + fixes w :: "'a::len word" + shows "m < LENGTH('a) \ unat (w && mask m) < 2 ^ m" + by (simp add: unat_less_helper and_mask_less') + +lemma unat_shiftr_less_2p: + fixes w :: "'a::len word" + shows "n + m = LENGTH('a) \ unat (w >> n) < 2 ^ m" + by (cases "n = 0"; simp add: unat_less_helper shiftr_less_t2n3) + +lemma nat_div_less_mono: + fixes m n :: nat + shows "m div d < n div d \ m < n" + by (meson div_le_mono not_less) + +lemma word_shiftr_less_mono: + fixes w :: "'a::len word" + shows "w >> n < v >> n \ w < v" + by (auto simp: word_less_nat_alt shiftr_div_2n' elim: nat_div_less_mono) + +lemma word_shiftr_less_mask: + fixes w :: "'a::len word" + shows "(w >> n < v >> n) \ (w && ~~mask n < v && ~~mask n)" + by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less) + +lemma word_shiftr_le_mask: + fixes w :: "'a::len word" + shows "(w >> n \ v >> n) \ (w && ~~mask n \ v && ~~mask n)" + by (metis (mono_tags) le_shiftr mask_shift shiftr_eq_neg_mask_eq word_le_less_eq word_le_not_less) + +lemma word_shiftr_eq_mask: + fixes w :: "'a::len word" + shows "(w >> n = v >> n) \ (w && ~~mask n = v && ~~mask n)" + by (metis (mono_tags) mask_shift shiftr_eq_neg_mask_eq) + +lemmas word_shiftr_cmp_mask = + word_shiftr_less_mask word_shiftr_le_mask word_shiftr_eq_mask + +lemma fold_array_update_index: + fixes arr :: "'a::c_type['b::finite]" + assumes "i < CARD('b)" + shows "fold (\i arr. Arrays.update arr i (f i)) is arr.[i] = (if i \ set is then f i else arr.[i])" + using assms by (induct "is" arbitrary: arr) (auto split: if_splits) + +lemma if_if_if_same_output: + "(if c1 then if c2 then t else f else if c3 then t else f) = (if c1 \ c2 \ \c1 \ c3 then t else f)" + by (simp split: if_splits) + +lemma word_le_split_mask: + "(w \ v) \ (w >> n < v >> n \ w >> n = v >> n \ w && mask n \ v && mask n)" + apply (simp add: word_shiftr_eq_mask word_shiftr_less_mask) + apply (rule subst[where P="\c. c \ d = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]]) + apply (rule subst[where P="\c. d \ c = e" for d e, OF AND_NOT_mask_plus_AND_mask_eq[where n=n]]) + apply (rule iffI) + apply safe + apply (fold_subgoals (prefix))[2] + apply (subst atomize_conj) + apply (rule context_conjI) + apply (metis AND_NOT_mask_plus_AND_mask_eq neg_mask_mono_le word_le_less_eq) + apply (metis add.commute word_and_le1 word_bw_comms(1) word_plus_and_or_coroll2 word_plus_mcs_4) + apply (metis Groups.add_ac(2) neg_mask_mono_le word_le_less_eq word_not_le word_plus_and_or_coroll2) + apply (metis add.commute word_and_le1 word_bw_comms(1) word_plus_and_or_coroll2 word_plus_mcs_3) + done + +lemma heap_modify_fold: + "heap_update p (f (h_val h p)) h = heap_modify p f h" + by (simp add: heap_modify_def) + +lemma t_hrs_'_update_heap_modify_fold: + "gs\ t_hrs_' := hrs_mem_update (heap_update p (f (h_val (hrs_mem (t_hrs_' gs)) p))) (t_hrs_' gs) \ + = t_hrs_'_update (hrs_mem_update (heap_modify p f)) gs" + by (clarsimp simp: heap_modify_def hrs_mem_update_def hrs_mem_def split: prod.splits) + +lemma heap_modify_Array_element: + fixes p :: "'a::packed_type ptr" + fixes p' :: "('a['b::finite]) ptr" + assumes "p = ptr_coerce p' +\<^sub>p int n" + assumes "n < CARD('b)" + assumes "CARD('b) * size_of TYPE('a) < 2 ^ addr_bitsize" + shows "heap_modify p f = heap_modify p' (fupdate n f)" + using assms by (simp add: heap_access_Array_element heap_update_Array_element' + heap_modify_def fupdate_def) + +lemma fupdate_word_set_or_clear_max_word: + "fupdate i (word_set_or_clear b max_word) arr = Arrays.update arr i (if b then max_word else 0)" + by (simp add: fupdate_def word_set_or_clear_def) + +lemma h_t_valid_Array_element': + "\ htd \\<^sub>t (p :: (('a :: mem_type)['b :: finite]) ptr); 0 \ n; n < CARD('b) \ + \ htd \\<^sub>t ((ptr_coerce p :: 'a ptr) +\<^sub>p n)" + apply (drule_tac n="nat n" and coerce=False in h_t_valid_Array_element') + apply simp + apply (simp add: array_ptr_index_def) + done + +lemma setIOPortMask_spec: + notes ucast_mask = ucast_and_mask[where n=6, simplified mask_def, simplified] + notes not_max_word_simps = and_not_max_word shiftr_not_max_word and_mask_not_max_word + notes ucast_cmp_ucast = ucast_le_ucast ucast_less_ucast + notes array_assert = array_assertion_shrink_right[OF array_ptr_valid_array_assertionD] + notes word_unat.Rep_inject[simp del] + shows + "\\. \ \ + {s. s = \ \ low_' s \ high_' s \ s \\<^sub>c ioport_table_ptr_coerce (ioport_bitmap_' s)} + Call setIOPortMask_'proc + {t. globals t = t_hrs_'_update + (hrs_mem_update + (heap_modify + (ioport_table_ptr_coerce (ioport_bitmap_' \)) + (let low_word = low_' \ >> wordRadix; + high_word = high_' \ >> wordRadix; + low_mask = ~~ mask (unat (low_' \ && mask wordRadix)); + high_mask = mask (Suc (unat (high_' \ && mask wordRadix))); + b = to_bool (set_' \) in + if low_word = high_word + then fupdate (unat low_word) (word_set_or_clear b (high_mask && low_mask)) + else fupdate (unat high_word) (word_set_or_clear b high_mask) + \ fold (\i arr. Arrays.update arr i (if b then max_word else 0)) + ([Suc (unat low_word) ..< unat high_word]) + \ fupdate (unat low_word) (word_set_or_clear b low_mask)))) + (globals \)}" + apply (rule allI) + apply (hoare_rule HoarePartial.ProcNoRec1) + apply (simp add: scast_ucast_up_eq_ucast word_upcast_shiftr[symmetric] ucast_mask[symmetric] + word_upcast_0_sle) + apply (rule ssubst[where P="\c. hoarep \ {} {} P (Catch (c1;; (Cond b c2 (c3;; c;; c4;; c5))) Skip) Q A" + for P c1 b c2 c3 c4 c5 Q A], + rule_tac I="{s. s \\<^sub>c ioport_table_ptr_coerce (bitmap_' s) + \ bitmap_' s = ptr_coerce (ioport_bitmap_' \) + \ ucast (low_' \ >> wordRadix) < low_word_' s + \ low_word_' s <= high_word_' s + \ high_word_' s = ucast (high_' \ >> wordRadix) + \ high_index_' s = ucast (high_' \ && mask wordRadix) + \ set_' s = set_' \ + \ globals s = t_hrs_'_update + (hrs_mem_update + (heap_modify + (ioport_table_ptr_coerce (ioport_bitmap_' \)) + (fold (\i arr. Arrays.update arr i (if to_bool (set_' \) then max_word else 0)) + ([Suc (unat (low_' \ >> wordRadix)) ..< unat (low_word_' s)]) + \ fupdate + (unat (low_' \ >> wordRadix)) + (word_set_or_clear + (to_bool (set_' \)) + (~~ mask (unat (low_' \ && mask wordRadix))))))) + (globals \)}" + in whileAnno_subst_invariant) + apply (rule conseqPre, vcg) + apply (all \clarsimp simp: Let_def wordRadix_def hrs_simps is_up is_down + unat_ucast_upcast uint_up_ucast sint_ucast_eq_uint up_ucast_inj_eq + not_max_word_simps[THEN ucast_increment, simplified max_word_def] + ucast_cmp_ucast ucast_cmp_ucast[where 'a=16 and y="0x40", simplified] + heap_modify_fold t_hrs_'_update_heap_modify_fold + cong: conj_cong\) + subgoal for mem htd ioport_bitmap high set low low_word + (* Loop invariant is preserved. *) + apply (frule neg_msb_le_mono[OF _ word_upcast_neg_msb]; + simp add: word_sless_iff_less[OF _ word_upcast_neg_msb] sint_eq_uint unat_arith_simps) + apply (frule less_trans[OF _ unat_shiftr_less_2p[where m=10]]; simp) + apply (frule h_t_valid_Array_element[where n="uint low_word"]; + simp add: uint_nat heap_modify_compose o_def fupdate_word_set_or_clear_max_word + heap_modify_Array_element[where 'b=1024 and p'="ptr_coerce ioport_bitmap"]) + apply (clarsimp elim!: array_assertion_shrink_right dest!: array_ptr_valid_array_assertionD) + done + subgoal for mem htd ioport_bitmap high set low low_word + (* Invariant plus loop termination condition is sufficient to establish VCG postcondition. *) + apply (frule neg_msb_le_mono[OF _ word_upcast_neg_msb]; + simp add: word_sless_iff_less[OF _ word_upcast_neg_msb] sint_eq_uint unat_arith_simps) + apply (cut_tac unat_and_mask_less_2p[of 6 high]; simp) + apply (cut_tac unat_shiftr_less_2p[of 6 10 high]; simp) + apply (frule h_t_valid_Array_element[where n="uint low_word"]; + simp add: uint_nat heap_modify_compose o_def fupdate_word_set_or_clear_max_word + heap_modify_Array_element[where 'b=1024 and p'="ptr_coerce ioport_bitmap"]) + apply (clarsimp elim!: array_assertion_shrink_right dest!: array_ptr_valid_array_assertionD) + done + subgoal for \' + (* VCG precondition is sufficient to establish loop invariant. *) + apply (frule word_le_split_mask[where n=6, THEN iffD1]) + apply (simp add: unat_arith_simps) + apply (cut_tac unat_shiftr_less_2p[of 6 10 "low_' \'"]; simp) + apply (cut_tac unat_shiftr_less_2p[of 6 10 "high_' \'"]; simp) + apply (cut_tac unat_and_mask_less_2p[of 6 "low_' \'"]; simp) + apply (cut_tac unat_and_mask_less_2p[of 6 "high_' \'"]; simp) + apply (simp add: uint_nat mask_def[where n=6] mask_def[where n=64] less_Suc_eq_le Suc_le_eq + heap_modify_Array_element[where 'b=1024 and p'="ptr_coerce (ioport_bitmap_' \')"]) + apply (frule h_t_valid_Array_element[where n="uint (low_' \' >> 6)"]; simp add: uint_nat) + apply (frule h_t_valid_Array_element[where n="uint (high_' \' >> 6)"]; simp add: uint_nat) + apply (frule array_assert[where n'="unat (low_' \' >> 6)"]; simp) + apply (frule array_assert[where n'="unat (high_' \' >> 6)"]; simp) + by auto + done + lemma setIOPortMask_ccorres: notes Collect_const[simp del] shows "ccorres dc xfdc - \ (* this is probably wrong *) + (\_. f \ l) (UNIV \ \\ioport_bitmap = Ptr (symbol_table ''x86KSAllocatedIOPorts'')\ \ \\low = f\ \ \\high = l\ \ \\set = from_bool b\) hs (setIOPortMask f l b) (Call setIOPortMask_'proc)" - apply (cinit lift: ioport_bitmap_' low_' high_' set_') - apply csymbr - apply (rule ccorres_Guard_Seq) - apply csymbr - apply (rule ccorres_Guard_Seq) - apply csymbr - sorry (* setIOPortMask_ccorres *) + apply (intro ccorres_from_vcg hoarep_conseq_spec_state[OF setIOPortMask_spec] allI) + apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def Let_def + global_ioport_bitmap_relation_def2 + setIOPortMask_def gets_def get_def modify_def put_def + monad_simps in_monad + hrs_mem_update h_val_heap_modify + clift_heap_modify_same tag_disj_via_td_name + cpspace_relation_def carch_globals_def cmachine_state_relation_def + fpu_null_state_relation_def) + apply (match premises in H: \cioport_bitmap_to_H _ = _\ and O: \low_' s \ high_' s\ for s + \ \match premises in _[thin]: _(multi) \ \insert O H\\) + apply (clarsimp simp: cioport_bitmap_to_H_def wordRadix_def, rule ext, drule_tac x=port in fun_cong) + apply (clarsimp simp: foldl_map_pair_constant foldl_fun_upd_value) + apply (rule ssubst[where P="\f. test_bit f i = e" for e i, OF if_distrib[where f="\c. c v.[i]" for v i]]) + apply (simp add: array_fupdate_index fold_array_update_index word_set_or_clear_test_bit + if_distrib[where f="\c. test_bit c i" for i] word_ops_nth_size word_size + unat_shiftr_less_2p[of 6 10, simplified] unat_and_mask_less_2p[of 6, simplified] + less_Suc_eq_le Suc_le_eq not_less unat_arith_simps(1,2)[symmetric] + if_if_same_output if_if_if_same_output) + apply (thin_tac "_ = _") + apply (rule if_weak_cong) + apply (rule ssubst[OF word_le_split_mask[where n=6], where P="\f. e \ f \ c" for e c]) + apply (rule ssubst[OF word_le_split_mask[where n=6], where P="\f. e \ c \ f" for e c]) + apply (drule word_le_split_mask[where n=6, THEN iffD1]) + by auto lemma freeIOPortRange_ccorres: "ccorres dc xfdc (\ and (\s. f \ l)) diff --git a/proof/crefine/X64/Retype_C.thy b/proof/crefine/X64/Retype_C.thy index ffafe90d5..2e9f8391e 100644 --- a/proof/crefine/X64/Retype_C.thy +++ b/proof/crefine/X64/Retype_C.thy @@ -3601,134 +3601,6 @@ abbreviation where "fpu_state_of_tcb_Ptr p \ fpu_state_Ptr &(tcbContext_of_tcb_Ptr p\[''fpuState_C''])" -lemma hrs_mem_update_compose: - "hrs_mem_update f (hrs_mem_update g h) = hrs_mem_update (f \ g) h" - by (auto simp: hrs_mem_update_def split: prod.split) - -lemma packed_heap_update_collapse': - fixes p :: "'a::packed_type ptr" - shows "heap_update p v \ heap_update p u = heap_update p v" - by (auto simp: packed_heap_update_collapse) - -lemma access_array_from_elements: - fixes v :: "'a::packed_type['b::finite]" - assumes "\i < CARD('b). h_val h (array_ptr_index p False i) = v.[i]" - shows "h_val h p = v" - by (rule cart_eq[THEN iffD2]) (simp add: assms heap_access_Array_element') - -lemma h_val_foldr_heap_update: - fixes v :: "'i \ 'a::mem_type" - assumes "\x y. {x,y} \ set xs \ x \ y \ ptr_span (p x) \ ptr_span (p y) = {}" - assumes "distinct xs" "i \ set xs" - shows "h_val (foldr (\i. heap_update (p i) (v i)) xs h) (p i) = v i" - using assms by (induct xs arbitrary: h; - fastforce simp: h_val_heap_update h_val_update_regions_disjoint) - -lemma ptr_span_array_ptr_index_disjoint: - fixes p :: "('a::packed_type['b::finite]) ptr" - assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" - assumes b: "x < CARD('b)" "y < CARD('b)" - assumes n: "x \ y" - shows "ptr_span (array_ptr_index p False x) \ ptr_span (array_ptr_index p False y) = {}" - proof - - have l: "CARD('b) * size_of TYPE('a) \ 2 ^ LENGTH(64)" using s by simp - have p: "\x k. x < CARD('b) \ k < size_of TYPE('a) - \ x * size_of TYPE('a) + k < 2 ^ LENGTH(64)" - by (metis less_le_trans[OF _ l] Divides.mod_less Fields.sign_simps(5) mod_lemma - zero_less_card_finite) - show ?thesis - apply (clarsimp simp: array_ptr_index_def ptr_add_def intvl_disj_offset) - apply (rule disjointI) - apply (clarsimp simp: intvl_def) - apply (subst (asm) of_nat_mult[symmetric])+ - apply (subst (asm) of_nat_add[symmetric])+ - apply (subst (asm) of_nat_inj[OF p p]; (simp add: b)?) - apply (drule arg_cong[where f="\x. x div size_of TYPE('a)"]; simp add: n) - done - qed - -lemma h_val_heap_update_Array: - fixes v :: "'a::packed_type['b::finite]" - assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" - shows "h_val (heap_update p v h) p = v" - apply (rule access_array_from_elements) - apply (clarsimp simp: heap_update_Array foldl_conv_foldr) - apply (rule h_val_foldr_heap_update; clarsimp simp: ptr_span_array_ptr_index_disjoint[OF s]) - done - -lemma foldr_heap_update_commute: - assumes "\y. y \ set xs \ ptr_span q \ ptr_span (p y) = {}" - shows "foldr (\i. heap_update (p i) (v i)) xs (heap_update q u h) - = heap_update q u (foldr (\i. heap_update (p i) (v i)) xs h)" - using assms by (induct xs) (auto simp: LemmaBucket_C.heap_update_commute) - -lemma foldr_packed_heap_update_collapse: - fixes u v :: "'i \ 'a::packed_type" - assumes "\x y. {x,y} \ set xs \ y \ x \ ptr_span (p x) \ ptr_span (p y) = {}" - assumes "distinct xs" - shows "foldr (\i. heap_update (p i) (v i)) xs (foldr (\i. heap_update (p i) (u i)) xs h) - = foldr (\i. heap_update (p i) (v i)) xs h" - using assms - apply - - apply (induct xs arbitrary: h; clarsimp; rename_tac x xs h) - apply (drule_tac x=x in spec; clarsimp) - apply (subst foldr_heap_update_commute; clarsimp simp: packed_heap_update_collapse) - apply (drule_tac x=y in spec; clarsimp) - done - -lemma packed_Array_heap_update_collapse: - fixes p :: "('a::packed_type['b::finite]) ptr" - assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" - shows "heap_update p v (heap_update p u h) = heap_update p v h" - by (simp add: heap_update_Array foldl_conv_foldr foldr_packed_heap_update_collapse - ptr_span_array_ptr_index_disjoint[OF s]) - -lemma packed_Array_heap_update_collapse': - fixes p :: "('a::packed_type['b::finite]) ptr" - assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" - shows "heap_update p v \ heap_update p u = heap_update p v" - by (auto simp: packed_Array_heap_update_collapse[OF s]) - -definition - heap_modify :: "'a::c_type ptr \ ('a \ 'a) \ heap_mem \ heap_mem" -where - "heap_modify p f \ \h. heap_update p (f (h_val h p)) h" - -lemma heap_modify_def2: - "heap_modify (p::'a::c_type ptr) f \ - \h. let bytes = heap_list h (size_of TYPE('a)) (ptr_val p) in - heap_update_list (ptr_val p) (to_bytes (f (from_bytes bytes)) bytes) h" - by (simp add: heap_modify_def Let_def heap_update_def h_val_def) - -lemma heap_modify_compose: - fixes p :: "'a::packed_type ptr" - shows "heap_modify p f \ heap_modify p g = heap_modify p (f \ g)" - by (auto simp: heap_modify_def h_val_heap_update packed_heap_update_collapse) - -lemma heap_modify_compose_Array: - fixes p :: "('a::packed_type['b::finite]) ptr" - assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" - shows "heap_modify p f \ heap_modify p g = heap_modify p (f \ g)" - by (auto simp: heap_modify_def h_val_heap_update_Array[OF s] - packed_Array_heap_update_collapse[OF s]) - -lemma fold_heap_modify_commute: - fixes p :: "'a::packed_type ptr" - shows "fold (heap_modify p \ f) upds = heap_modify p (fold f upds)" - apply (induction upds) - apply (simp add: heap_modify_def heap_update_id) - apply (clarsimp simp: heap_modify_compose[THEN fun_cong, simplified] o_def) - done - -lemma fold_heap_modify_commute_Array: - fixes p :: "('a::packed_type['b::finite]) ptr" - assumes s: "CARD('b) * size_of TYPE('a) \ 2 ^ addr_bitsize" - shows "fold (heap_modify p \ f) upds = heap_modify p (fold f upds)" - apply (induction upds) - apply (simp add: heap_modify_def heap_update_id_Array) - apply (clarsimp simp: heap_modify_compose_Array[OF s, THEN fun_cong, simplified] o_def) - done - definition array_updates :: "'a::c_type['b::finite] \ (nat \ 'a) list \ 'a['b]" where @@ -3813,7 +3685,6 @@ lemma fpu_null_state_retyp_disjoint: end -(* FIXME x64: this needs more array updates from initContext *) lemma cnc_tcb_helper: fixes p :: "tcb_C ptr" defines "kotcb \ (KOTCB (makeObject :: tcb))" diff --git a/proof/crefine/X64/StateRelation_C.thy b/proof/crefine/X64/StateRelation_C.thy index 7ac46667b..06f4b107e 100644 --- a/proof/crefine/X64/StateRelation_C.thy +++ b/proof/crefine/X64/StateRelation_C.thy @@ -149,20 +149,11 @@ where None \ False (* should never happen *) | Some x \ s = x86_irq_state_to_H x" -(* 1024 = number of entries in ioport table - = 2^16 (total number of ioports) / word_bits *) -type_synonym ioport_table_C = "machine_word[1024]" - (* This is required for type collision shenanigans, 1024 matches above *) lemma ntbs_1024[simp]: "nat_to_bin_string 1024 = ''000000000010''" by (simp add: nat_to_bin_string_simps) -abbreviation - ioport_table_Ptr :: "machine_word \ ioport_table_C ptr" -where - "ioport_table_Ptr \ Ptr" - definition cioport_bitmap_to_H :: "ioport_table_C \ (ioport \ bool)" where diff --git a/proof/crefine/X64/Wellformed_C.thy b/proof/crefine/X64/Wellformed_C.thy index 95282ff5f..fab60db0d 100644 --- a/proof/crefine/X64/Wellformed_C.thy +++ b/proof/crefine/X64/Wellformed_C.thy @@ -45,6 +45,10 @@ abbreviation abbreviation pml4e_Ptr :: "word64 \ pml4e_C ptr" where "pml4e_Ptr == Ptr" +(* 1024 = number of entries in ioport table + = 2^16 (total number of ioports) / word_bits *) +type_synonym ioport_table_C = "machine_word[1024]" + type_synonym tcb_cnode_array = "cte_C[5]" type_synonym fpu_bytes_array = "word8[fpu_bytes]" type_synonym registers_array = "machine_word[23]" @@ -55,6 +59,7 @@ abbreviation "tcb_cnode_Ptr \ Ptr :: addr \ tcb_cnode_array p abbreviation "fpu_state_Ptr \ Ptr :: addr \ user_fpu_state_C ptr" abbreviation "fpu_bytes_Ptr \ Ptr :: addr \ fpu_bytes_array ptr" abbreviation "registers_Ptr \ Ptr :: addr \ registers_array ptr" +abbreviation "ioport_table_Ptr \ Ptr :: addr \ ioport_table_C ptr" lemma halt_spec: "Gamma \ {} Call halt_'proc {}"