theory Untyped_AI

lemma detype_descendants_range_in:
  "ptr && ~~ mask sz = ptr \<Longrightarrow> descendants_range_in usable_range cref (detype usable_range s)" using misc cte_wp_at apply - apply (frule detype_invariants) apply (simp) using descendants_range apply (clarsimp simp: blah descendants_range_def2) apply (simp add: invs_untyped_children blah
              invs_valid_reply_caps invs_valid_reply_masters)+ apply (subst valid_mdb_descendants_range_in) apply (clarsimp dest!:invs_mdb simp:detype_clear_um_independent) apply (frule detype_locale) apply (drule detype_locale.non_filter_detype[symmetric]) apply (simp add:blah) using descendants_range(1) apply - apply (subst (asm)valid_mdb_descendants_range_in) apply (simp add:invs_mdb) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr && ~~ mask sz = ptr \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (detype {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s) proof (prove)
using this:
ct_active s
invs s
cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s

goal (1 subgoal):
 1. ptr && ~~ mask sz = ptr \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (detype {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (detype {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap dev (ptr && ~~ mask sz) sz idx)
 2. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> descendants_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s
 3. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> invs s
 4. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 5. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> ct_active s
 6. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; (invs and untyped_children_in_mdb) (detype (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (clear_um (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)) s))\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (detype {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> descendants_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s
 2. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> invs s
 3. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 4. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> ct_active s
 5. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; (invs and untyped_children_in_mdb) (detype (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (clear_um (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)) s))\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (detype {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s) proof (prove)
using this:
descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s
descendants_range_in {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} cref s

goal (5 subgoals):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> descendants_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s
 2. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> invs s
 3. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 4. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> ct_active s
 5. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; (invs and untyped_children_in_mdb) (detype (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (clear_um (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)) s))\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (detype {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> invs s
 2. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 3. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s\<rbrakk> \<Longrightarrow> ct_active s
 4. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; (invs and untyped_children_in_mdb) (detype (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)) (clear_um (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)) s))\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (detype {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s))\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref (detype {ptr..ptr + 2 ^ sz - 1} s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s))\<rbrakk> \<Longrightarrow> valid_mdb (detype {ptr..ptr + 2 ^ sz - 1} s)
 2. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s))\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of cref (cdt (detype {ptr..ptr + 2 ^ sz - 1} s)). \<exists>c. null_filter (caps_of_state (detype {ptr..ptr + 2 ^ sz - 1} s)) p' = Some c \<and> cap_range c \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s))\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of cref (cdt (detype {ptr..ptr + 2 ^ sz - 1} s)). \<exists>c. null_filter (caps_of_state (detype {ptr..ptr + 2 ^ sz - 1} s)) p' = Some c \<and> cap_range c \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)); detype_locale (UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of cref (cdt (detype {ptr..ptr + 2 ^ sz - 1} s)). \<exists>c. null_filter (caps_of_state (detype {ptr..ptr + 2 ^ sz - 1} s)) p' = Some c \<and> cap_range c \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)); null_filter (caps_of_state (detype (untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)) s)) = null_filter (caps_of_state s)\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of cref (cdt (detype {ptr..ptr + 2 ^ sz - 1} s)). \<exists>c. null_filter (caps_of_state (detype {ptr..ptr + 2 ^ sz - 1} s)) p' = Some c \<and> cap_range c \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)); null_filter (\<lambda>p. if ptr \<le> fst p \<and> fst p \<le> ptr + 2 ^ sz - 1 then None else caps_of_state s p) = null_filter (caps_of_state s)\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of cref (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
using this:
descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s

goal (1 subgoal):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)); null_filter (\<lambda>p. if ptr \<le> fst p \<and> fst p \<le> ptr + 2 ^ sz - 1 then None else caps_of_state s p) = null_filter (caps_of_state s)\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of cref (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)); null_filter (\<lambda>p. if ptr \<le> fst p \<and> fst p \<le> ptr + 2 ^ sz - 1 then None else caps_of_state s p) = null_filter (caps_of_state s); descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of cref (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)); null_filter (\<lambda>p. if ptr \<le> fst p \<and> fst p \<le> ptr + 2 ^ sz - 1 then None else caps_of_state s p) = null_filter (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_mdb s
 2. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)); null_filter (\<lambda>p. if ptr \<le> fst p \<and> fst p \<le> ptr + 2 ^ sz - 1 then None else caps_of_state s p) = null_filter (caps_of_state s); \<forall>p'\<in>descendants_of cref (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of cref (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr && ~~ mask sz = ptr; ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev ptr sz idx)) cref s; invs (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)) \<and> untyped_children_in_mdb (detype {ptr..ptr + 2 ^ sz - 1} (clear_um {ptr..ptr + 2 ^ sz - 1} s)); null_filter (\<lambda>p. if ptr \<le> fst p \<and> fst p \<le> ptr + 2 ^ sz - 1 then None else caps_of_state s p) = null_filter (caps_of_state s); \<forall>p'\<in>descendants_of cref (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> \<forall>p'\<in>descendants_of cref (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> {ptr..ptr + 2 ^ sz - 1} = {} proof (prove)
goal:
No subgoals!