theory Retype_IF

lemma invoke_untyped_reads_respects_g:
  "reads_respects_g aag l (invs and valid_untyped_inv ui and only_timer_irq_inv irq st
                                and ct_active and pas_refined aag
                                and K (authorised_untyped_inv aag ui)) (invoke_untyped ui)" apply (rule_tac fn="\<lambda>s. caps_of_state s (slot_of_untyped_inv ui)" in equiv_valid_obtain) apply (cases ui, clarsimp simp: valid_untyped_inv_wcap reads_equiv_g_def) apply (simp add: authorised_untyped_inv_def
                    reads_equiv_caps_of_state) apply (case_tac "x \<noteq> None \<and> is_untyped_cap (the x)") apply (clarsimp simp: is_cap_simps) apply (rule equiv_valid_guard_imp, rule invoke_untyped_reads_respects_g_wcap) apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state valid_untyped_inv_wcap) apply auto[1] apply (rule equiv_valid_guard_imp, rule gen_asm_ev'[where Q=False]) apply simp apply (cases ui, clarsimp simp: valid_untyped_inv_wcap cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui)) (invoke_untyped ui) proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>reads_equiv_g aag s t; affects_equiv aag l s t; (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui)) s; (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui)) t\<rbrakk> \<Longrightarrow> caps_of_state s (slot_of_untyped_inv ui) = caps_of_state t (slot_of_untyped_inv ui)
 2. \<And>x. reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = x)) (invoke_untyped ui) proof (prove)
goal (2 subgoals):
 1. \<And>s t a b x2 x4 x5 x6 x7 x8 sz idx sza idxa. \<lbrakk>affects_equiv aag l s t; ui = Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8; reads_equiv aag s t; globals_equiv s t; invs s; invs t; only_timer_irq_inv irq st s; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sz) sz idx) (a, b) s; only_timer_irq_inv irq st t; cte_wp_at (\<lambda>c. c = UntypedCap x8 (x4 && ~~ mask sz) sza idxa) (a, b) t; ct_active s; range_cover x4 sz (obj_bits_api x5 x6) (length x7); ct_active t; pas_refined aag t; range_cover x4 sza (obj_bits_api x5 x6) (length x7); pas_refined aag s; authorised_untyped_inv aag (Retype (a, b) x2 (x4 && ~~ mask sz) x4 x5 x6 x7 x8); idx \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; idxa \<le> unat (x4 && mask sz) \<or> x2 \<and> x4 = x4 && ~~ mask sz; x4 && ~~ mask sza = x4 && ~~ mask sz; x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x2 \<longrightarrow> descendants_of (a, b) (cdt t) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. cte_wp_at ((=) NullCap) slot s \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; \<forall>slot\<in>set x7. cte_wp_at ((=) NullCap) slot t \<and> ex_cte_cap_wp_to is_cnode_cap slot t \<and> real_cte_at slot t; x5 \<noteq> ArchObject ASIDPoolObj; x7 \<noteq> []; x8 \<longrightarrow> x5 = Untyped \<or> is_frame_type x5\<rbrakk> \<Longrightarrow> caps_of_state s (a, b) = caps_of_state t (a, b)
 2. \<And>x. reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = x)) (invoke_untyped ui) proof (prove)
goal (1 subgoal):
 1. \<And>x. reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = x)) (invoke_untyped ui) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<noteq> None \<and> is_untyped_cap (the x) \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = x)) (invoke_untyped ui)
 2. \<And>x. \<not> (x \<noteq> None \<and> is_untyped_cap (the x)) \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = x)) (invoke_untyped ui) proof (prove)
goal (2 subgoals):
 1. \<And>dev r bits f. reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and (\<lambda>y. authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = Some (UntypedCap dev r bits f))) (invoke_untyped ui)
 2. \<And>x. \<not> (x \<noteq> None \<and> is_untyped_cap (the x)) \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = x)) (invoke_untyped ui) proof (prove)
goal (2 subgoals):
 1. \<And>dev r bits f s. (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and (\<lambda>y. authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = Some (UntypedCap dev r bits f))) s \<Longrightarrow> (invs and valid_untyped_inv_wcap ui (Some (UntypedCap (?dev61 dev r bits f) (?ptr61 dev r bits f) (?sz61 dev r bits f) (?idx61 dev r bits f))) and only_timer_irq_inv (?irq61 dev r bits f) (?st61 dev r bits f) and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui)) s
 2. \<And>x. \<not> (x \<noteq> None \<and> is_untyped_cap (the x)) \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = x)) (invoke_untyped ui) proof (prove)
goal (2 subgoals):
 1. \<And>dev bits f s a b x2 x4 x5 x6 x7. \<lbrakk>ui = Retype (a, b) x2 (x4 && ~~ mask bits) x4 x5 x6 x7 dev; invs s; only_timer_irq_inv irq st s; ct_active s; range_cover x4 bits (obj_bits_api x5 x6) (length x7); pas_refined aag s; f \<le> unat (x4 && mask bits) \<or> x2 \<and> x4 = x4 && ~~ mask bits; authorised_untyped_inv aag (Retype (a, b) x2 (x4 && ~~ mask bits) x4 x5 x6 x7 dev); caps_of_state s (a, b) = Some (UntypedCap dev (x4 && ~~ mask bits) bits f); x2 \<longrightarrow> descendants_of (a, b) (cdt s) = {}; x5 = CapTableObject \<longrightarrow> 0 < x6; x5 = Untyped \<longrightarrow> untyped_min_bits \<le> x6; (a, b) \<notin> set x7; distinct x7; \<forall>slot\<in>set x7. caps_of_state s slot = Some NullCap \<and> ex_cte_cap_wp_to is_cnode_cap slot s \<and> real_cte_at slot s; x5 \<noteq> ArchObject ASIDPoolObj; x7 \<noteq> []; dev \<longrightarrow> x5 = Untyped \<or> is_frame_type x5\<rbrakk> \<Longrightarrow> bits = ?sz61 dev (x4 && ~~ mask bits) bits f \<and> f = ?idx61 dev (x4 && ~~ mask bits) bits f \<and> ?dev61 dev (x4 && ~~ mask bits) bits f = dev \<and> ?ptr61 dev (x4 && ~~ mask bits) bits f = x4 && ~~ mask bits \<and> range_cover x4 (?sz61 dev (x4 && ~~ mask bits) bits f) (obj_bits_api x5 x6) (length x7) \<and> (?idx61 dev (x4 && ~~ mask bits) bits f \<le> unat (x4 && mask bits) \<or> x2 \<and> x4 = x4 && ~~ mask bits) \<and> x4 && ~~ mask (?sz61 dev (x4 && ~~ mask bits) bits f) = x4 && ~~ mask bits \<and> only_timer_irq_inv (?irq61 dev (x4 && ~~ mask bits) bits f) (?st61 dev (x4 && ~~ mask bits) bits f) s
 2. \<And>x. \<not> (x \<noteq> None \<and> is_untyped_cap (the x)) \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = x)) (invoke_untyped ui) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<not> (x \<noteq> None \<and> is_untyped_cap (the x)) \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = x)) (invoke_untyped ui) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> (x \<noteq> None \<and> is_untyped_cap (the x)); False\<rbrakk> \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?P109 x) (invoke_untyped ui)
 2. \<And>x s. \<lbrakk>\<not> (x \<noteq> None \<and> is_untyped_cap (the x)); (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = x)) s\<rbrakk> \<Longrightarrow> (?P109 x and K False) s proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<lbrakk>\<not> (x \<noteq> None \<and> is_untyped_cap (the x)); (invs and valid_untyped_inv ui and only_timer_irq_inv irq st and ct_active and pas_refined aag and K (authorised_untyped_inv aag ui) and (\<lambda>s. caps_of_state s (slot_of_untyped_inv ui) = x)) s\<rbrakk> \<Longrightarrow> (?P109 x and K False) s proof (prove)
goal:
No subgoals!