theory Untyped_AI

lemma set_cap_caps_no_overlap:
  "\<lbrace>cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cref and caps_no_overlap ptr sz\<rbrace>  set_cap cap cref
  \<lbrace>\<lambda>r s. caps_no_overlap ptr sz s\<rbrace>" apply (simp add: caps_no_overlap_def) apply wp apply (clarsimp simp: cte_wp_at_caps_of_state caps_no_overlap_def
              simp del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
                        Int_atLeastAtMost atLeastatMost_empty_iff ) apply (erule ranE) apply (simp split: if_splits
    del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff ) apply (drule bspec) apply fastforce apply (clarsimp simp
      del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff ) apply (erule(1) set_mp) apply (drule_tac x = capa in bspec) apply fastforce apply (clarsimp simp
      del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff ) apply (erule(1) set_mp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cref and caps_no_overlap ptr sz\<rbrace> set_cap cap cref \<lbrace>\<lambda>r. caps_no_overlap ptr sz\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cref and caps_no_overlap ptr sz\<rbrace> set_cap cap cref \<lbrace>\<lambda>r s. \<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at (\<lambda>c. untyped_range c = untyped_range cap) cref and caps_no_overlap ptr sz) s \<Longrightarrow> \<forall>cap\<in>ran ((caps_of_state s)(cref \<mapsto> cap)). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s capa capaa x. \<lbrakk>capa \<in> ran (\<lambda>a. if a = cref then Some cap else caps_of_state s a); \<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range cap; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa proof (prove)
goal (1 subgoal):
 1. \<And>s capa capaa x xa. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range cap; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; (if xa = cref then Some cap else caps_of_state s xa) = Some capa\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa proof (prove)
goal (2 subgoals):
 1. \<And>s capa capaa x xa. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range capa; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa = cref; cap = capa\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa
 2. \<And>s capa capaa x xa. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range cap; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<noteq> cref; caps_of_state s xa = Some capa\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa proof (prove)
goal (3 subgoals):
 1. \<And>s capa capaa x xa. \<lbrakk>caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range capa; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa = cref; cap = capa\<rbrakk> \<Longrightarrow> ?cap23 s capa capaa x xa \<in> ran (caps_of_state s)
 2. \<And>s capa capaa x xa. \<lbrakk>caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range capa; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa = cref; cap = capa; untyped_range (?cap23 s capa capaa x xa) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range (?cap23 s capa capaa x xa)\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa
 3. \<And>s capa capaa x xa. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range cap; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<noteq> cref; caps_of_state s xa = Some capa\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa proof (prove)
goal (2 subgoals):
 1. \<And>s capa capaa x xa. \<lbrakk>caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range capa; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa = cref; cap = capa; untyped_range capaa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range capaa\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa
 2. \<And>s capa capaa x xa. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range cap; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<noteq> cref; caps_of_state s xa = Some capa\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa proof (prove)
goal (2 subgoals):
 1. \<And>s capa x a b. \<lbrakk>caps_of_state s (a, b) = Some capa; untyped_range capa = untyped_range cap; untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; cref = (a, b)\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap
 2. \<And>s capa capaa x xa. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range cap; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<noteq> cref; caps_of_state s xa = Some capa\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa proof (prove)
goal (1 subgoal):
 1. \<And>s capa capaa x xa. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap; caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range cap; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<noteq> cref; caps_of_state s xa = Some capa\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa proof (prove)
goal (2 subgoals):
 1. \<And>s capa capaa x xa. \<lbrakk>caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range cap; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<noteq> cref; caps_of_state s xa = Some capa\<rbrakk> \<Longrightarrow> capa \<in> ran (caps_of_state s)
 2. \<And>s capa capaa x xa. \<lbrakk>caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range cap; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<noteq> cref; caps_of_state s xa = Some capa; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range capa\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa proof (prove)
goal (1 subgoal):
 1. \<And>s capa capaa x xa. \<lbrakk>caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range cap; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; xa \<noteq> cref; caps_of_state s xa = Some capa; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range capa\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa proof (prove)
goal (1 subgoal):
 1. \<And>s capa capaa x a b. \<lbrakk>caps_of_state s cref = Some capaa; untyped_range capaa = untyped_range cap; untyped_range capa \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; (a, b) \<noteq> cref; caps_of_state s (a, b) = Some capa; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range capa\<rbrakk> \<Longrightarrow> x \<in> untyped_range capa proof (prove)
goal:
No subgoals!