theory ArchVSpaceEntries_AI

lemma arch_decode_invocation_valid_pdpt[wp]:
  "\<lbrace>invs and valid_cap (cap.ArchObjectCap cap) and valid_pdpt_objs\<rbrace>
   arch_decode_invocation label args cap_index slot cap excaps
   \<lbrace>invocation_duplicates_valid o Invocations_A.InvokeArchObject\<rbrace>,-" proof - have bitwise:"\<And>a. (ucast (((a::word32) && ~~ mask 6) && mask 14 >> 2)::12 word)
    = (ucast (a  && mask 14 >> 2)::12 word) && ~~ mask 4" apply (simp add: mask_def) apply word_bitwise done have sz:
    "\<And>vmpage_size. \<lbrakk>args ! 0 + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base;
      vmsz_aligned (args ! 0) vmpage_size\<rbrakk>
     \<Longrightarrow> args ! 0 < kernel_base" apply (rule le_less_trans[OF is_aligned_no_overflow]) apply (simp add: vmsz_aligned_def) apply simp done show ?thesis supply if_split[split del] apply (simp add: arch_decode_invocation_def)
    \<comment> \<open>Handle the easy cases first (trivial because of the post-condition invocation_duplicates_valid)\<close> apply (cases "invocation_type label \<notin> {ArchInvocationLabel ARMPageTableMap, ArchInvocationLabel ARMPageMap}") apply (wpsimp simp: invocation_duplicates_valid_def page_inv_duplicates_valid_def
                         pti_duplicates_valid_def Let_def
                   cong: if_cong)
    \<comment> \<open>Handle the two interesting cases now\<close> apply (clarsimp; erule disjE; cases cap;
           simp add: isPDFlushLabel_def isPageFlushLabel_def throwError_R')
     \<comment> \<open>PageTableMap\<close> apply (wpsimp simp: Let_def get_master_pde_def invocation_duplicates_valid_def
                         pti_duplicates_valid_def mask_lower_twice pd_bits_def bitwise pageBits_def
                         obj_at_def
                     wp: get_pde_wp hoare_drop_imps hoare_vcg_if_lift_ER split: if_splits) apply (intro conjI; clarsimp)
    \<comment> \<open>PageMap\<close> apply (rename_tac dev pg_ptr rights sz pg_map) apply (wpsimp simp: Let_def invocation_duplicates_valid_def page_inv_duplicates_valid_def
                    wp: ensure_safe_mapping_ensures[THEN hoare_post_imp_R]
                        check_vp_wpR hoare_vcg_if_lift_ER find_pd_for_asid_lookup_pd_wp) apply (fastforce simp: invs_psp_aligned page_directory_at_aligned_pd_bits
                           word_not_le sz valid_cap_def valid_arch_cap_def lookup_pd_slot_eq
                    split: if_splits) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap (ArchObjectCap cap) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> arch_decode_invocation label args cap_index slot cap excaps \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (state)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap (ArchObjectCap cap) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> arch_decode_invocation label args cap_index slot cap excaps \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>a. UCAST(32 \<rightarrow> 12) ((a && ~~ mask 6) && mask 14 >> 2) = UCAST(32 \<rightarrow> 12) (a && mask 14 >> 2) && ~~ mask 4 proof (prove)
goal (1 subgoal):
 1. \<And>a. UCAST(32 \<rightarrow> 12) ((a && 0xFFFFFFC0) && 0x3FFF >> 2) = UCAST(32 \<rightarrow> 12) (a && 0x3FFF >> 2) && 0xFF0 proof (prove)
goal:
No subgoals! proof (state)
this:
UCAST(32 \<rightarrow> 12) ((?a && ~~ mask 6) && mask 14 >> 2) = UCAST(32 \<rightarrow> 12) (?a && mask 14 >> 2) && ~~ mask 4

goal (1 subgoal):
 1. \<lbrace>invs and valid_cap (ArchObjectCap cap) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> arch_decode_invocation label args cap_index slot cap excaps \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>vmpage_size. \<lbrakk>args ! 0 + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base; vmsz_aligned (args ! 0) vmpage_size\<rbrakk> \<Longrightarrow> args ! 0 < kernel_base proof (prove)
goal (2 subgoals):
 1. \<And>vmpage_size. \<lbrakk>args ! 0 + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base; vmsz_aligned (args ! 0) vmpage_size\<rbrakk> \<Longrightarrow> is_aligned (args ! 0) (?sz1 vmpage_size)
 2. \<And>vmpage_size. \<lbrakk>args ! 0 + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base; vmsz_aligned (args ! 0) vmpage_size\<rbrakk> \<Longrightarrow> args ! 0 + 2 ^ ?sz1 vmpage_size - 1 < kernel_base proof (prove)
goal (1 subgoal):
 1. \<And>vmpage_size. \<lbrakk>args ! 0 + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base; vmsz_aligned (args ! 0) vmpage_size\<rbrakk> \<Longrightarrow> args ! 0 + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>args ! 0 + 2 ^ pageBitsForSize ?vmpage_size - 1 < kernel_base; vmsz_aligned (args ! 0) ?vmpage_size\<rbrakk> \<Longrightarrow> args ! 0 < kernel_base

goal (1 subgoal):
 1. \<lbrace>invs and valid_cap (ArchObjectCap cap) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> arch_decode_invocation label args cap_index slot cap excaps \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap (ArchObjectCap cap) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> arch_decode_invocation label args cap_index slot cap excaps \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap (ArchObjectCap cap) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> arch_decode_invocation label args cap_index slot cap excaps \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap (ArchObjectCap cap) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> case cap of ASIDPoolCap p base \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMASIDPoolAssign then if 0 < length excaps then let (pd_cap, pd_cap_slot) = excaps ! 0 in case pd_cap of ArchObjectCap (PageDirectoryCap x None) \<Rightarrow> doE asid_table <- liftE $ gets (arm_asid_table \<circ> arch_state);
pool_ptr <- returnOk (asid_table (asid_high_bits_of base));
whenE (pool_ptr = None) $ throwError $ FailedLookup False InvalidRoot;
whenE (p \<noteq> the pool_ptr) $ throwError $ InvalidCapability 0;
pool <- liftE $ get_asid_pool p;
free_set <- returnOk (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + base \<noteq> 0});
whenE (free_set = {}) $ throwError DeleteFirst;
offset <- liftE $ select_ext (\<lambda>_. free_asid_pool_select pool base) free_set;
returnOk $ InvokeASIDPool $ Assign (UCAST(10 \<rightarrow> 32) offset + base) p pd_cap_slot
odE | ArchObjectCap (PageDirectoryCap x (Some a)) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1 else throwError TruncatedMessage else throwError IllegalOperation | ASIDControlCap \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMASIDControlMakePool then if 1 < length args \<and> 1 < length excaps then let index = args ! 0; depth = args ! 1; (untyped, parent_slot) = excaps ! 0; root = fst (excaps ! 1) in doE asid_table <- liftE $ gets (arm_asid_table \<circ> arch_state);
free_set <- returnOk (- dom asid_table \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1});
whenE (free_set = {}) $ throwError DeleteFirst;
free <- liftE $ select_ext (\<lambda>_. free_asid_select asid_table) free_set;
base <- returnOk (UCAST(7 \<rightarrow> 32) free << local.asid_low_bits);
(p, n) <- case untyped of UntypedCap True p n f \<Rightarrow> throwError $ InvalidCapability 1 | UntypedCap False p n f \<Rightarrow> returnOk (p, n) | _ \<Rightarrow> throwError $ InvalidCapability 1;
frame <- if n = pageBits then doE ensure_no_children parent_slot;
returnOk p
odE else throwError $ InvalidCapability 1;
dest_slot <- lookup_target_slot root (to_bl index) (unat depth);
ensure_empty dest_slot;
returnOk $ InvokeASIDControl $ MakePool frame dest_slot parent_slot base
odE else throwError TruncatedMessage else throwError IllegalOperation | PageCap dev p R pgsz mapped_address \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMPageMap then if 2 < length args \<and> 0 < length excaps then let vaddr = args ! 0; rights_mask = args ! 1; attr = args ! 2; pd_cap = fst (excaps ! 0) in doE (pd, asid) <- case pd_cap of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
case mapped_address of None \<Rightarrow> doE vtop <- returnOk (vaddr + (1 << pageBitsForSize pgsz) - 1);
whenE (kernel_base \<le> vtop) $ throwError $ InvalidArgument 0
odE | Some (asid', vaddr') \<Rightarrow> doE whenE (asid' \<noteq> asid) (throwError $ InvalidCapability 1);
whenE (vaddr' \<noteq> vaddr) (throwError $ InvalidArgument 0)
odE;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
vm_rights <- returnOk (mask_vm_rights R (data_to_rights rights_mask));
check_vp_alignment pgsz vaddr;
entries <- create_mapping_entries (addrFromPPtr p) vaddr pgsz vm_rights (attribs_from_word attr) pd;
ensure_safe_mapping entries;
returnOk $ InvokePage $ PageMap asid (ArchObjectCap $ PageCap dev p R pgsz (Some (asid, vaddr))) slot entries
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageUnmap then returnOk $ InvokePage $ PageUnmap cap slot else if isPageFlushLabel (invocation_type label) then if 1 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case mapped_address of None \<Rightarrow> throwError IllegalOperation | Some a \<Rightarrow> returnOk a;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize pgsz;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ InvalidArgument 0;
returnOk $ InvokePage $ PageFlush (label_to_flush_type (invocation_type label)) (start + vaddr) (end + vaddr - 1) (addrFromPPtr p + start) pd asid
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageGetAddress then returnOk $ InvokePage $ PageGetAddr p else throwError IllegalOperation | PageTableCap p mapped_address \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMPageTableMap then if 1 < length args \<and> 0 < length excaps then let vaddr = args ! 0; attr = args ! 1; pd_cap = fst (excaps ! 0) in doE whenE (mapped_address \<noteq> None) $ throwError $ InvalidCapability 0;
(pd, asid) <- case pd_cap of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
whenE (kernel_base \<le> vaddr) $ throwError $ InvalidArgument 0;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
pd_index <- returnOk (vaddr >> 20);
vaddr' <- returnOk (vaddr && ~~ mask 20);
pd_slot <- returnOk (pd + (pd_index << 2));
oldpde <- liftE $ get_master_pde pd_slot;
unlessE (oldpde = InvalidPDE) $ throwError DeleteFirst;
pde <- returnOk (PageTablePDE (addrFromPPtr p) (attribs_from_word attr \<inter> {ParityEnabled}) 0);
returnOk $ InvokePageTable $ PageTableMap (ArchObjectCap $ PageTableCap p (Some (asid, vaddr'))) slot pde pd_slot
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageTableUnmap then doE final <- liftE $ is_final_cap (ArchObjectCap cap);
unlessE final $ throwError RevokeFirst;
returnOk $ InvokePageTable $ PageTableUnmap (ArchObjectCap cap) slot
odE else throwError IllegalOperation | PageDirectoryCap x xa \<Rightarrow> if isPDFlushLabel (invocation_type label) then if 1 < length args then let start = args ! 0; end = args ! 1 in doE whenE (end \<le> start) $ throwError $ InvalidArgument 1;
whenE (kernel_base \<le> start \<or> kernel_base < end) $ throwError IllegalOperation;
(pd, asid) <- case cap of PageDirectoryCap pd None \<Rightarrow> throwError $ InvalidCapability 0 | PageDirectoryCap pd (Some asid) \<Rightarrow> returnOk (pd, asid) | _ \<Rightarrow> throwError $ InvalidCapability 0;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 0;
frame_info <- liftE $ resolve_vaddr pd start;
case frame_info of None \<Rightarrow> returnOk $ InvokePageDirectory PageDirectoryNothing | Some (frame_size, frame_base) \<Rightarrow> let base_start = page_base start frame_size; base_end = page_base (end - 1) frame_size; offset = start && mask (pageBitsForSize frame_size); pstart = frame_base + offset in doE whenE (base_start \<noteq> base_end) $ throwError $ RangeError start (base_start + mask (pageBitsForSize frame_size));
returnOk $ InvokePageDirectory $ PageDirectoryFlush (label_to_flush_type (invocation_type label)) start (end - 1) pstart pd asid
odE
odE else throwError TruncatedMessage else throwError IllegalOperation \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. invocation_type label \<notin> {ArchInvocationLabel ARMPageTableMap, ArchInvocationLabel ARMPageMap} \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap cap) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> case cap of ASIDPoolCap p base \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMASIDPoolAssign then if 0 < length excaps then let (pd_cap, pd_cap_slot) = excaps ! 0 in case pd_cap of ArchObjectCap (PageDirectoryCap x None) \<Rightarrow> doE asid_table <- liftE $ gets (arm_asid_table \<circ> arch_state);
pool_ptr <- returnOk (asid_table (asid_high_bits_of base));
whenE (pool_ptr = None) $ throwError $ FailedLookup False InvalidRoot;
whenE (p \<noteq> the pool_ptr) $ throwError $ InvalidCapability 0;
pool <- liftE $ get_asid_pool p;
free_set <- returnOk (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + base \<noteq> 0});
whenE (free_set = {}) $ throwError DeleteFirst;
offset <- liftE $ select_ext (\<lambda>_. free_asid_pool_select pool base) free_set;
returnOk $ InvokeASIDPool $ Assign (UCAST(10 \<rightarrow> 32) offset + base) p pd_cap_slot
odE | ArchObjectCap (PageDirectoryCap x (Some a)) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1 else throwError TruncatedMessage else throwError IllegalOperation | ASIDControlCap \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMASIDControlMakePool then if 1 < length args \<and> 1 < length excaps then let index = args ! 0; depth = args ! 1; (untyped, parent_slot) = excaps ! 0; root = fst (excaps ! 1) in doE asid_table <- liftE $ gets (arm_asid_table \<circ> arch_state);
free_set <- returnOk (- dom asid_table \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1});
whenE (free_set = {}) $ throwError DeleteFirst;
free <- liftE $ select_ext (\<lambda>_. free_asid_select asid_table) free_set;
base <- returnOk (UCAST(7 \<rightarrow> 32) free << local.asid_low_bits);
(p, n) <- case untyped of UntypedCap True p n f \<Rightarrow> throwError $ InvalidCapability 1 | UntypedCap False p n f \<Rightarrow> returnOk (p, n) | _ \<Rightarrow> throwError $ InvalidCapability 1;
frame <- if n = pageBits then doE ensure_no_children parent_slot;
returnOk p
odE else throwError $ InvalidCapability 1;
dest_slot <- lookup_target_slot root (to_bl index) (unat depth);
ensure_empty dest_slot;
returnOk $ InvokeASIDControl $ MakePool frame dest_slot parent_slot base
odE else throwError TruncatedMessage else throwError IllegalOperation | PageCap dev p R pgsz mapped_address \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMPageMap then if 2 < length args \<and> 0 < length excaps then let vaddr = args ! 0; rights_mask = args ! 1; attr = args ! 2; pd_cap = fst (excaps ! 0) in doE (pd, asid) <- case pd_cap of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
case mapped_address of None \<Rightarrow> doE vtop <- returnOk (vaddr + (1 << pageBitsForSize pgsz) - 1);
whenE (kernel_base \<le> vtop) $ throwError $ InvalidArgument 0
odE | Some (asid', vaddr') \<Rightarrow> doE whenE (asid' \<noteq> asid) (throwError $ InvalidCapability 1);
whenE (vaddr' \<noteq> vaddr) (throwError $ InvalidArgument 0)
odE;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
vm_rights <- returnOk (mask_vm_rights R (data_to_rights rights_mask));
check_vp_alignment pgsz vaddr;
entries <- create_mapping_entries (addrFromPPtr p) vaddr pgsz vm_rights (attribs_from_word attr) pd;
ensure_safe_mapping entries;
returnOk $ InvokePage $ PageMap asid (ArchObjectCap $ PageCap dev p R pgsz (Some (asid, vaddr))) slot entries
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageUnmap then returnOk $ InvokePage $ PageUnmap cap slot else if isPageFlushLabel (invocation_type label) then if 1 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case mapped_address of None \<Rightarrow> throwError IllegalOperation | Some a \<Rightarrow> returnOk a;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize pgsz;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ InvalidArgument 0;
returnOk $ InvokePage $ PageFlush (label_to_flush_type (invocation_type label)) (start + vaddr) (end + vaddr - 1) (addrFromPPtr p + start) pd asid
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageGetAddress then returnOk $ InvokePage $ PageGetAddr p else throwError IllegalOperation | PageTableCap p mapped_address \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMPageTableMap then if 1 < length args \<and> 0 < length excaps then let vaddr = args ! 0; attr = args ! 1; pd_cap = fst (excaps ! 0) in doE whenE (mapped_address \<noteq> None) $ throwError $ InvalidCapability 0;
(pd, asid) <- case pd_cap of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
whenE (kernel_base \<le> vaddr) $ throwError $ InvalidArgument 0;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
pd_index <- returnOk (vaddr >> 20);
vaddr' <- returnOk (vaddr && ~~ mask 20);
pd_slot <- returnOk (pd + (pd_index << 2));
oldpde <- liftE $ get_master_pde pd_slot;
unlessE (oldpde = InvalidPDE) $ throwError DeleteFirst;
pde <- returnOk (PageTablePDE (addrFromPPtr p) (attribs_from_word attr \<inter> {ParityEnabled}) 0);
returnOk $ InvokePageTable $ PageTableMap (ArchObjectCap $ PageTableCap p (Some (asid, vaddr'))) slot pde pd_slot
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageTableUnmap then doE final <- liftE $ is_final_cap (ArchObjectCap cap);
unlessE final $ throwError RevokeFirst;
returnOk $ InvokePageTable $ PageTableUnmap (ArchObjectCap cap) slot
odE else throwError IllegalOperation | PageDirectoryCap x xa \<Rightarrow> if isPDFlushLabel (invocation_type label) then if 1 < length args then let start = args ! 0; end = args ! 1 in doE whenE (end \<le> start) $ throwError $ InvalidArgument 1;
whenE (kernel_base \<le> start \<or> kernel_base < end) $ throwError IllegalOperation;
(pd, asid) <- case cap of PageDirectoryCap pd None \<Rightarrow> throwError $ InvalidCapability 0 | PageDirectoryCap pd (Some asid) \<Rightarrow> returnOk (pd, asid) | _ \<Rightarrow> throwError $ InvalidCapability 0;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 0;
frame_info <- liftE $ resolve_vaddr pd start;
case frame_info of None \<Rightarrow> returnOk $ InvokePageDirectory PageDirectoryNothing | Some (frame_size, frame_base) \<Rightarrow> let base_start = page_base start frame_size; base_end = page_base (end - 1) frame_size; offset = start && mask (pageBitsForSize frame_size); pstart = frame_base + offset in doE whenE (base_start \<noteq> base_end) $ throwError $ RangeError start (base_start + mask (pageBitsForSize frame_size));
returnOk $ InvokePageDirectory $ PageDirectoryFlush (label_to_flush_type (invocation_type label)) start (end - 1) pstart pd asid
odE
odE else throwError TruncatedMessage else throwError IllegalOperation \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, -
 2. \<not> invocation_type label \<notin> {ArchInvocationLabel ARMPageTableMap, ArchInvocationLabel ARMPageMap} \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap cap) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> case cap of ASIDPoolCap p base \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMASIDPoolAssign then if 0 < length excaps then let (pd_cap, pd_cap_slot) = excaps ! 0 in case pd_cap of ArchObjectCap (PageDirectoryCap x None) \<Rightarrow> doE asid_table <- liftE $ gets (arm_asid_table \<circ> arch_state);
pool_ptr <- returnOk (asid_table (asid_high_bits_of base));
whenE (pool_ptr = None) $ throwError $ FailedLookup False InvalidRoot;
whenE (p \<noteq> the pool_ptr) $ throwError $ InvalidCapability 0;
pool <- liftE $ get_asid_pool p;
free_set <- returnOk (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + base \<noteq> 0});
whenE (free_set = {}) $ throwError DeleteFirst;
offset <- liftE $ select_ext (\<lambda>_. free_asid_pool_select pool base) free_set;
returnOk $ InvokeASIDPool $ Assign (UCAST(10 \<rightarrow> 32) offset + base) p pd_cap_slot
odE | ArchObjectCap (PageDirectoryCap x (Some a)) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1 else throwError TruncatedMessage else throwError IllegalOperation | ASIDControlCap \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMASIDControlMakePool then if 1 < length args \<and> 1 < length excaps then let index = args ! 0; depth = args ! 1; (untyped, parent_slot) = excaps ! 0; root = fst (excaps ! 1) in doE asid_table <- liftE $ gets (arm_asid_table \<circ> arch_state);
free_set <- returnOk (- dom asid_table \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1});
whenE (free_set = {}) $ throwError DeleteFirst;
free <- liftE $ select_ext (\<lambda>_. free_asid_select asid_table) free_set;
base <- returnOk (UCAST(7 \<rightarrow> 32) free << local.asid_low_bits);
(p, n) <- case untyped of UntypedCap True p n f \<Rightarrow> throwError $ InvalidCapability 1 | UntypedCap False p n f \<Rightarrow> returnOk (p, n) | _ \<Rightarrow> throwError $ InvalidCapability 1;
frame <- if n = pageBits then doE ensure_no_children parent_slot;
returnOk p
odE else throwError $ InvalidCapability 1;
dest_slot <- lookup_target_slot root (to_bl index) (unat depth);
ensure_empty dest_slot;
returnOk $ InvokeASIDControl $ MakePool frame dest_slot parent_slot base
odE else throwError TruncatedMessage else throwError IllegalOperation | PageCap dev p R pgsz mapped_address \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMPageMap then if 2 < length args \<and> 0 < length excaps then let vaddr = args ! 0; rights_mask = args ! 1; attr = args ! 2; pd_cap = fst (excaps ! 0) in doE (pd, asid) <- case pd_cap of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
case mapped_address of None \<Rightarrow> doE vtop <- returnOk (vaddr + (1 << pageBitsForSize pgsz) - 1);
whenE (kernel_base \<le> vtop) $ throwError $ InvalidArgument 0
odE | Some (asid', vaddr') \<Rightarrow> doE whenE (asid' \<noteq> asid) (throwError $ InvalidCapability 1);
whenE (vaddr' \<noteq> vaddr) (throwError $ InvalidArgument 0)
odE;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
vm_rights <- returnOk (mask_vm_rights R (data_to_rights rights_mask));
check_vp_alignment pgsz vaddr;
entries <- create_mapping_entries (addrFromPPtr p) vaddr pgsz vm_rights (attribs_from_word attr) pd;
ensure_safe_mapping entries;
returnOk $ InvokePage $ PageMap asid (ArchObjectCap $ PageCap dev p R pgsz (Some (asid, vaddr))) slot entries
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageUnmap then returnOk $ InvokePage $ PageUnmap cap slot else if isPageFlushLabel (invocation_type label) then if 1 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case mapped_address of None \<Rightarrow> throwError IllegalOperation | Some a \<Rightarrow> returnOk a;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize pgsz;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ InvalidArgument 0;
returnOk $ InvokePage $ PageFlush (label_to_flush_type (invocation_type label)) (start + vaddr) (end + vaddr - 1) (addrFromPPtr p + start) pd asid
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageGetAddress then returnOk $ InvokePage $ PageGetAddr p else throwError IllegalOperation | PageTableCap p mapped_address \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMPageTableMap then if 1 < length args \<and> 0 < length excaps then let vaddr = args ! 0; attr = args ! 1; pd_cap = fst (excaps ! 0) in doE whenE (mapped_address \<noteq> None) $ throwError $ InvalidCapability 0;
(pd, asid) <- case pd_cap of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
whenE (kernel_base \<le> vaddr) $ throwError $ InvalidArgument 0;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
pd_index <- returnOk (vaddr >> 20);
vaddr' <- returnOk (vaddr && ~~ mask 20);
pd_slot <- returnOk (pd + (pd_index << 2));
oldpde <- liftE $ get_master_pde pd_slot;
unlessE (oldpde = InvalidPDE) $ throwError DeleteFirst;
pde <- returnOk (PageTablePDE (addrFromPPtr p) (attribs_from_word attr \<inter> {ParityEnabled}) 0);
returnOk $ InvokePageTable $ PageTableMap (ArchObjectCap $ PageTableCap p (Some (asid, vaddr'))) slot pde pd_slot
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageTableUnmap then doE final <- liftE $ is_final_cap (ArchObjectCap cap);
unlessE final $ throwError RevokeFirst;
returnOk $ InvokePageTable $ PageTableUnmap (ArchObjectCap cap) slot
odE else throwError IllegalOperation | PageDirectoryCap x xa \<Rightarrow> if isPDFlushLabel (invocation_type label) then if 1 < length args then let start = args ! 0; end = args ! 1 in doE whenE (end \<le> start) $ throwError $ InvalidArgument 1;
whenE (kernel_base \<le> start \<or> kernel_base < end) $ throwError IllegalOperation;
(pd, asid) <- case cap of PageDirectoryCap pd None \<Rightarrow> throwError $ InvalidCapability 0 | PageDirectoryCap pd (Some asid) \<Rightarrow> returnOk (pd, asid) | _ \<Rightarrow> throwError $ InvalidCapability 0;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 0;
frame_info <- liftE $ resolve_vaddr pd start;
case frame_info of None \<Rightarrow> returnOk $ InvokePageDirectory PageDirectoryNothing | Some (frame_size, frame_base) \<Rightarrow> let base_start = page_base start frame_size; base_end = page_base (end - 1) frame_size; offset = start && mask (pageBitsForSize frame_size); pstart = frame_base + offset in doE whenE (base_start \<noteq> base_end) $ throwError $ RangeError start (base_start + mask (pageBitsForSize frame_size));
returnOk $ InvokePageDirectory $ PageDirectoryFlush (label_to_flush_type (invocation_type label)) start (end - 1) pstart pd asid
odE
odE else throwError TruncatedMessage else throwError IllegalOperation \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<not> invocation_type label \<notin> {ArchInvocationLabel ARMPageTableMap, ArchInvocationLabel ARMPageMap} \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap cap) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> case cap of ASIDPoolCap p base \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMASIDPoolAssign then if 0 < length excaps then let (pd_cap, pd_cap_slot) = excaps ! 0 in case pd_cap of ArchObjectCap (PageDirectoryCap x None) \<Rightarrow> doE asid_table <- liftE $ gets (arm_asid_table \<circ> arch_state);
pool_ptr <- returnOk (asid_table (asid_high_bits_of base));
whenE (pool_ptr = None) $ throwError $ FailedLookup False InvalidRoot;
whenE (p \<noteq> the pool_ptr) $ throwError $ InvalidCapability 0;
pool <- liftE $ get_asid_pool p;
free_set <- returnOk (- dom pool \<inter> {x. UCAST(10 \<rightarrow> 32) x + base \<noteq> 0});
whenE (free_set = {}) $ throwError DeleteFirst;
offset <- liftE $ select_ext (\<lambda>_. free_asid_pool_select pool base) free_set;
returnOk $ InvokeASIDPool $ Assign (UCAST(10 \<rightarrow> 32) offset + base) p pd_cap_slot
odE | ArchObjectCap (PageDirectoryCap x (Some a)) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1 else throwError TruncatedMessage else throwError IllegalOperation | ASIDControlCap \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMASIDControlMakePool then if 1 < length args \<and> 1 < length excaps then let index = args ! 0; depth = args ! 1; (untyped, parent_slot) = excaps ! 0; root = fst (excaps ! 1) in doE asid_table <- liftE $ gets (arm_asid_table \<circ> arch_state);
free_set <- returnOk (- dom asid_table \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1});
whenE (free_set = {}) $ throwError DeleteFirst;
free <- liftE $ select_ext (\<lambda>_. free_asid_select asid_table) free_set;
base <- returnOk (UCAST(7 \<rightarrow> 32) free << local.asid_low_bits);
(p, n) <- case untyped of UntypedCap True p n f \<Rightarrow> throwError $ InvalidCapability 1 | UntypedCap False p n f \<Rightarrow> returnOk (p, n) | _ \<Rightarrow> throwError $ InvalidCapability 1;
frame <- if n = pageBits then doE ensure_no_children parent_slot;
returnOk p
odE else throwError $ InvalidCapability 1;
dest_slot <- lookup_target_slot root (to_bl index) (unat depth);
ensure_empty dest_slot;
returnOk $ InvokeASIDControl $ MakePool frame dest_slot parent_slot base
odE else throwError TruncatedMessage else throwError IllegalOperation | PageCap dev p R pgsz mapped_address \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMPageMap then if 2 < length args \<and> 0 < length excaps then let vaddr = args ! 0; rights_mask = args ! 1; attr = args ! 2; pd_cap = fst (excaps ! 0) in doE (pd, asid) <- case pd_cap of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
case mapped_address of None \<Rightarrow> doE vtop <- returnOk (vaddr + (1 << pageBitsForSize pgsz) - 1);
whenE (kernel_base \<le> vtop) $ throwError $ InvalidArgument 0
odE | Some (asid', vaddr') \<Rightarrow> doE whenE (asid' \<noteq> asid) (throwError $ InvalidCapability 1);
whenE (vaddr' \<noteq> vaddr) (throwError $ InvalidArgument 0)
odE;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
vm_rights <- returnOk (mask_vm_rights R (data_to_rights rights_mask));
check_vp_alignment pgsz vaddr;
entries <- create_mapping_entries (addrFromPPtr p) vaddr pgsz vm_rights (attribs_from_word attr) pd;
ensure_safe_mapping entries;
returnOk $ InvokePage $ PageMap asid (ArchObjectCap $ PageCap dev p R pgsz (Some (asid, vaddr))) slot entries
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageUnmap then returnOk $ InvokePage $ PageUnmap cap slot else if isPageFlushLabel (invocation_type label) then if 1 < length args then let start = args ! 0; end = args ! 1 in doE (asid, vaddr) <- case mapped_address of None \<Rightarrow> throwError IllegalOperation | Some a \<Rightarrow> returnOk a;
pd <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (end \<le> start) $ throwError $ InvalidArgument 1;
page_size <- returnOk $ 1 << pageBitsForSize pgsz;
whenE (page_size \<le> start \<or> page_size < end) $ throwError $ InvalidArgument 0;
returnOk $ InvokePage $ PageFlush (label_to_flush_type (invocation_type label)) (start + vaddr) (end + vaddr - 1) (addrFromPPtr p + start) pd asid
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageGetAddress then returnOk $ InvokePage $ PageGetAddr p else throwError IllegalOperation | PageTableCap p mapped_address \<Rightarrow> if invocation_type label = ArchInvocationLabel ARMPageTableMap then if 1 < length args \<and> 0 < length excaps then let vaddr = args ! 0; attr = args ! 1; pd_cap = fst (excaps ! 0) in doE whenE (mapped_address \<noteq> None) $ throwError $ InvalidCapability 0;
(pd, asid) <- case pd_cap of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
whenE (kernel_base \<le> vaddr) $ throwError $ InvalidArgument 0;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
pd_index <- returnOk (vaddr >> 20);
vaddr' <- returnOk (vaddr && ~~ mask 20);
pd_slot <- returnOk (pd + (pd_index << 2));
oldpde <- liftE $ get_master_pde pd_slot;
unlessE (oldpde = InvalidPDE) $ throwError DeleteFirst;
pde <- returnOk (PageTablePDE (addrFromPPtr p) (attribs_from_word attr \<inter> {ParityEnabled}) 0);
returnOk $ InvokePageTable $ PageTableMap (ArchObjectCap $ PageTableCap p (Some (asid, vaddr'))) slot pde pd_slot
odE else throwError TruncatedMessage else if invocation_type label = ArchInvocationLabel ARMPageTableUnmap then doE final <- liftE $ is_final_cap (ArchObjectCap cap);
unlessE final $ throwError RevokeFirst;
returnOk $ InvokePageTable $ PageTableUnmap (ArchObjectCap cap) slot
odE else throwError IllegalOperation | PageDirectoryCap x xa \<Rightarrow> if isPDFlushLabel (invocation_type label) then if 1 < length args then let start = args ! 0; end = args ! 1 in doE whenE (end \<le> start) $ throwError $ InvalidArgument 1;
whenE (kernel_base \<le> start \<or> kernel_base < end) $ throwError IllegalOperation;
(pd, asid) <- case cap of PageDirectoryCap pd None \<Rightarrow> throwError $ InvalidCapability 0 | PageDirectoryCap pd (Some asid) \<Rightarrow> returnOk (pd, asid) | _ \<Rightarrow> throwError $ InvalidCapability 0;
pd' <- lookup_error_on_failure False $ find_pd_for_asid asid;
whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 0;
frame_info <- liftE $ resolve_vaddr pd start;
case frame_info of None \<Rightarrow> returnOk $ InvokePageDirectory PageDirectoryNothing | Some (frame_size, frame_base) \<Rightarrow> let base_start = page_base start frame_size; base_end = page_base (end - 1) frame_size; offset = start && mask (pageBitsForSize frame_size); pstart = frame_base + offset in doE whenE (base_start \<noteq> base_end) $ throwError $ RangeError start (base_start + mask (pageBitsForSize frame_size));
returnOk $ InvokePageDirectory $ PageDirectoryFlush (label_to_flush_type (invocation_type label)) start (end - 1) pstart pd asid
odE
odE else throwError TruncatedMessage else throwError IllegalOperation \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableMap; cap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap (PageTableCap x41 x42)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> if Suc 0 < length args \<and> excaps \<noteq> [] then let vaddr = args ! 0 in doE y <- whenE (\<exists>a b. x42 = Some (a, b)) (throwError (InvalidCapability 0));
(pd, asid) <- case fst (excaps ! 0) of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
y <- whenE (kernel_base \<le> vaddr) (throwError (InvalidArgument 0));
pd' <- lookup_error_on_failure False (find_pd_for_asid asid);
y <- whenE (pd' \<noteq> pd) (throwError (InvalidCapability (Suc 0)));
oldpde <- liftE (get_master_pde (pd + (vaddr >> 20 << 2)));
y <- unlessE (oldpde = InvalidPDE) (throwError DeleteFirst);
returnOk (InvokePageTable (PageTableMap (ArchObjectCap (PageTableCap x41 (Some (asid, vaddr && ~~ mask 20)))) slot (PageTablePDE (addrFromPPtr x41) (attribs_from_word (args ! Suc 0) \<inter> {ParityEnabled}) 0) (pd + (vaddr >> 20 << 2))))
odE else throwError TruncatedMessage \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, -
 2. \<And>x31 x32 x33 x34 x35. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageMap; cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> if 2 < length args \<and> excaps \<noteq> [] then let vaddr = args ! 0 in doE (pd, asid) <- case fst (excaps ! 0) of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
y <- case x35 of None \<Rightarrow> whenE (kernel_base \<le> vaddr + 2 ^ pageBitsForSize x34 - 1) (throwError (InvalidArgument 0)) | Some (asid', vaddr') \<Rightarrow> doE y <- whenE (asid' \<noteq> asid) (throwError (InvalidCapability (Suc 0)));
whenE (vaddr' \<noteq> vaddr) (throwError (InvalidArgument 0))
odE;
pd' <- lookup_error_on_failure False (find_pd_for_asid asid);
y <- whenE (pd' \<noteq> pd) (throwError (InvalidCapability (Suc 0)));
y <- check_vp_alignment x34 vaddr;
entries <- create_mapping_entries (addrFromPPtr x32) vaddr x34 (mask_vm_rights x33 (data_to_rights (args ! Suc 0))) (attribs_from_word (args ! 2)) pd;
y <- ensure_safe_mapping entries;
returnOk (InvokePage (PageMap asid (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (asid, vaddr)))) slot entries))
odE else throwError TruncatedMessage \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>x41 s xa xc pd. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableMap; cap = PageTableCap x41 None; invs s; s \<turnstile> ArchObjectCap (PageTableCap x41 None); \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; Suc 0 < length args; excaps \<noteq> []; fst (excaps ! 0) = ArchObjectCap (PageDirectoryCap xa (Some xc)); \<not> kernel_base \<le> args ! 0; kheap s (xa + (args ! 0 >> 20 << 2) && ~~ mask 14) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> ((\<exists>x xb xc. pd (UCAST(32 \<rightarrow> 12) (xa + (args ! 0 >> 20 << 2) && mask 14 >> 2) && ~~ mask 4) = PageTablePDE x xb xc) \<longrightarrow> pd (UCAST(32 \<rightarrow> 12) (xa + (args ! 0 >> 20 << 2) && mask 14 >> 2)) = InvalidPDE \<longrightarrow> pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (xa + (args ! 0 >> 20 << 2) && mask 14 >> 2) && ~~ mask 4)) = 0) \<and> ((\<exists>x xb xc xd. pd (UCAST(32 \<rightarrow> 12) (xa + (args ! 0 >> 20 << 2) && mask 14 >> 2) && ~~ mask 4) = SectionPDE x xb xc xd) \<longrightarrow> pd (UCAST(32 \<rightarrow> 12) (xa + (args ! 0 >> 20 << 2) && mask 14 >> 2)) = InvalidPDE \<longrightarrow> pde_range_sz (pd (UCAST(32 \<rightarrow> 12) (xa + (args ! 0 >> 20 << 2) && mask 14 >> 2) && ~~ mask 4)) = 0)
 2. \<And>x31 x32 x33 x34 x35. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageMap; cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> if 2 < length args \<and> excaps \<noteq> [] then let vaddr = args ! 0 in doE (pd, asid) <- case fst (excaps ! 0) of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
y <- case x35 of None \<Rightarrow> whenE (kernel_base \<le> vaddr + 2 ^ pageBitsForSize x34 - 1) (throwError (InvalidArgument 0)) | Some (asid', vaddr') \<Rightarrow> doE y <- whenE (asid' \<noteq> asid) (throwError (InvalidCapability (Suc 0)));
whenE (vaddr' \<noteq> vaddr) (throwError (InvalidArgument 0))
odE;
pd' <- lookup_error_on_failure False (find_pd_for_asid asid);
y <- whenE (pd' \<noteq> pd) (throwError (InvalidCapability (Suc 0)));
y <- check_vp_alignment x34 vaddr;
entries <- create_mapping_entries (addrFromPPtr x32) vaddr x34 (mask_vm_rights x33 (data_to_rights (args ! Suc 0))) (attribs_from_word (args ! 2)) pd;
y <- ensure_safe_mapping entries;
returnOk (InvokePage (PageMap asid (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (asid, vaddr)))) slot entries))
odE else throwError TruncatedMessage \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageMap; cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> if 2 < length args \<and> excaps \<noteq> [] then let vaddr = args ! 0 in doE (pd, asid) <- case fst (excaps ! 0) of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
y <- case x35 of None \<Rightarrow> whenE (kernel_base \<le> vaddr + 2 ^ pageBitsForSize x34 - 1) (throwError (InvalidArgument 0)) | Some (asid', vaddr') \<Rightarrow> doE y <- whenE (asid' \<noteq> asid) (throwError (InvalidCapability (Suc 0)));
whenE (vaddr' \<noteq> vaddr) (throwError (InvalidArgument 0))
odE;
pd' <- lookup_error_on_failure False (find_pd_for_asid asid);
y <- whenE (pd' \<noteq> pd) (throwError (InvalidCapability (Suc 0)));
y <- check_vp_alignment x34 vaddr;
entries <- create_mapping_entries (addrFromPPtr x32) vaddr x34 (mask_vm_rights x33 (data_to_rights (args ! Suc 0))) (attribs_from_word (args ! 2)) pd;
y <- ensure_safe_mapping entries;
returnOk (InvokePage (PageMap asid (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (asid, vaddr)))) slot entries))
odE else throwError TruncatedMessage \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>dev pg_ptr rights sz pg_map. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageMap; cap = PageCap dev pg_ptr rights sz pg_map\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap (PageCap dev pg_ptr rights sz pg_map)) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> if 2 < length args \<and> excaps \<noteq> [] then let vaddr = args ! 0 in doE (pd, asid) <- case fst (excaps ! 0) of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError $ InvalidCapability 1 | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> returnOk (pd, asid) | ArchObjectCap _ \<Rightarrow> throwError $ InvalidCapability 1 | _ \<Rightarrow> throwError $ InvalidCapability 1;
y <- case pg_map of None \<Rightarrow> whenE (kernel_base \<le> vaddr + 2 ^ pageBitsForSize sz - 1) (throwError (InvalidArgument 0)) | Some (asid', vaddr') \<Rightarrow> doE y <- whenE (asid' \<noteq> asid) (throwError (InvalidCapability (Suc 0)));
whenE (vaddr' \<noteq> vaddr) (throwError (InvalidArgument 0))
odE;
pd' <- lookup_error_on_failure False (find_pd_for_asid asid);
y <- whenE (pd' \<noteq> pd) (throwError (InvalidCapability (Suc 0)));
y <- check_vp_alignment sz vaddr;
entries <- create_mapping_entries (addrFromPPtr pg_ptr) vaddr sz (mask_vm_rights rights (data_to_rights (args ! Suc 0))) (attribs_from_word (args ! 2)) pd;
y <- ensure_safe_mapping entries;
returnOk (InvokePage (PageMap asid (ArchObjectCap (PageCap dev pg_ptr rights sz (Some (asid, vaddr)))) slot entries))
odE else throwError TruncatedMessage \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>dev pg_ptr rights sz pg_map s xa xc. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageMap; cap = PageCap dev pg_ptr rights sz pg_map; invs s; s \<turnstile> ArchObjectCap (PageCap dev pg_ptr rights sz pg_map); \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; 2 < length args; excaps \<noteq> []; fst (excaps ! 0) = ArchObjectCap (PageDirectoryCap xa (Some xc))\<rbrakk> \<Longrightarrow> (pg_map = None \<longrightarrow> (if kernel_base \<le> args ! 0 + 2 ^ pageBitsForSize sz - 1 then \<lambda>s. True else (\<lambda>s. valid_vspace_objs s \<and> (\<forall>pd. vspace_at_asid xc pd s \<and> typ_at (AArch APageDirectory) pd s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> (if pd \<noteq> xa then \<lambda>s. True else (\<lambda>s. vmsz_aligned (args ! 0) sz \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> (\<exists>ref. (ref \<rhd> xa) s) \<and> is_aligned xa pd_bits \<and> args ! 0 < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot xa (args ! 0) && ~~ mask pd_bits)) s))) s))) s) \<and> (\<forall>a b. pg_map = Some (a, b) \<longrightarrow> (if a \<noteq> xc then \<lambda>s. True else (\<lambda>s. b = args ! 0 \<longrightarrow> valid_vspace_objs s \<and> (\<forall>pd. vspace_at_asid xc pd s \<and> typ_at (AArch APageDirectory) pd s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<longrightarrow> (if pd \<noteq> xa then \<lambda>s. True else (\<lambda>s. vmsz_aligned (args ! 0) sz \<longrightarrow> (\<forall>x\<in>ran (kheap s). obj_valid_pdpt x) \<and> (\<exists>ref. (ref \<rhd> xa) s) \<and> is_aligned xa pd_bits \<and> args ! 0 < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot xa (args ! 0) && ~~ mask pd_bits)) s))) s))) s) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>invs and valid_cap (ArchObjectCap cap) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x)\<rbrace> arch_decode_invocation label args cap_index slot cap excaps \<lbrace>invocation_duplicates_valid \<circ> InvokeArchObject\<rbrace>, -

goal:
No subgoals!