theory CSpace_C

lemma maskVMRights_spec:
  "\<forall>s. \<Gamma> \<turnstile> ({s} \<inter>
           \<lbrace> \<acute>vm_rights && mask 2 = \<acute>vm_rights \<rbrace>)
  Call maskVMRights_'proc
  \<lbrace> vmrights_to_H \<acute>ret__unsigned_long =
    maskVMRights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) (cap_rights_to_H (seL4_CapRights_lift \<^bsup>s\<^esup>cap_rights_mask)) \<and>
    \<acute>ret__unsigned_long && mask 2 = \<acute>ret__unsigned_long \<rbrace>" apply vcg apply clarsimp apply (rule conjI) apply ((auto simp: vmrights_to_H_def maskVMRights_def vmrights_defs
                      cap_rights_to_H_def
               split: bool.split
         | simp add: mask_def
         | word_bitwise)+)[1] apply clarsimp apply (subgoal_tac "vm_rights = 0 \<or> vm_rights = 1 \<or> vm_rights = 2 \<or> vm_rights = 3") apply (auto simp: vmrights_to_H_def maskVMRights_def vmrights_defs
                     cap_rights_to_H_def seL4_CapRights_lift_def
                     to_bool_def mask_def
                   split: bool.splits)[1] apply (subst(asm) mask_eq_iff_w2p) apply (simp add: word_size) apply (rule ccontr, clarsimp) apply (drule inc_le, simp, drule(1) order_le_neq_trans [OF _ not_sym])+ apply (drule inc_le, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> ({s} \<inter> \<lbrace>\<acute>vm_rights && mask 2 = \<acute>vm_rights\<rbrace>) Call maskVMRights_'proc \<lbrace>vmrights_to_H \<acute>ret__unsigned_long = maskVMRights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) (cap_rights_to_H (seL4_CapRights_lift \<^bsup>s\<^esup>cap_rights_mask)) \<and> \<acute>ret__unsigned_long && mask 2 = \<acute>ret__unsigned_long\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap_rights_mask vm_rights. vm_rights && mask 2 = vm_rights \<Longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess \<longrightarrow> ((if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> ((if capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> ((if capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> ((if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> ((if capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> ((if capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) \<and> ((if capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) \<and> ((if capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) = 0 then 1 else 0) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)))) \<and> ((if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)))) \<and> (\<not> (if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly then 1 else 0) \<noteq> 0 \<longrightarrow> ((if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly then 1 else 0) \<noteq> 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (\<not> (if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly then 1 else 0) \<noteq> 0 \<longrightarrow> ((if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> ((if capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite))) \<and> ((if capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> ((if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> ((if capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> ((if capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) \<and> ((if capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) \<and> ((if capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) = 0 then 1 else 0) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) \<and> ((if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)))) \<and> (\<not> (if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> ((if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite))) \<and> (\<not> (if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> ((if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> ((if capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) = 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> ((if capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) \<and> ((if capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) \<and> ((if capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) = 0 then 1 else 0) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) \<and> (\<not> (if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> ((if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> (\<forall>ret__unsigned. ret__unsigned = capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> ((if capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) \<and> ((if capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) \<and> (\<not> (if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> ((if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) \<and> (\<not> (if vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite then 1 else 0) \<noteq> 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)))))))) proof (prove)
goal (1 subgoal):
 1. \<And>cap_rights_mask vm_rights. vm_rights && mask 2 = vm_rights \<Longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess \<longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly \<longrightarrow> (0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (\<not> 0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (Kernel_C.VMReadOnly = Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) \<and> (Kernel_C.VMReadOnly \<noteq> Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly \<longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite \<longrightarrow> (0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (0 < capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) \<and> (\<not> 0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) proof (prove)
goal (2 subgoals):
 1. \<And>cap_rights_mask vm_rights. vm_rights && mask 2 = vm_rights \<Longrightarrow> vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess
 2. \<And>cap_rights_mask vm_rights. vm_rights && mask 2 = vm_rights \<Longrightarrow> vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess \<longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly \<longrightarrow> (0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (\<not> 0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (Kernel_C.VMReadOnly = Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) \<and> (Kernel_C.VMReadOnly \<noteq> Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly \<longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite \<longrightarrow> (0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (0 < capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) \<and> (\<not> 0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)) proof (prove)
goal (1 subgoal):
 1. \<And>cap_rights_mask vm_rights. vm_rights && mask 2 = vm_rights \<Longrightarrow> vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess \<longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly \<longrightarrow> (0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (\<not> 0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (Kernel_C.VMReadOnly = Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) \<and> (Kernel_C.VMReadOnly \<noteq> Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly \<longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite \<longrightarrow> (0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (0 < capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) \<and> (\<not> 0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)) proof (prove)
goal (1 subgoal):
 1. \<And>cap_rights_mask vm_rights. \<lbrakk>vm_rights && mask 2 = vm_rights; vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess\<rbrakk> \<Longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly \<longrightarrow> (0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (\<not> 0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (Kernel_C.VMReadOnly = Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) \<and> (Kernel_C.VMReadOnly \<noteq> Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly \<longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite \<longrightarrow> (0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (0 < capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) \<and> (\<not> 0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)) proof (prove)
goal (2 subgoals):
 1. \<And>cap_rights_mask vm_rights. \<lbrakk>vm_rights && mask 2 = vm_rights; vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess; vm_rights = 0 \<or> vm_rights = 1 \<or> vm_rights = 2 \<or> vm_rights = 3\<rbrakk> \<Longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly \<longrightarrow> (0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (\<not> 0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (Kernel_C.VMReadOnly = Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) \<and> (Kernel_C.VMReadOnly \<noteq> Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly \<longrightarrow> (vm_rights = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite \<longrightarrow> (0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> (capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) = 0 \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly) \<and> (0 < capAllowWrite_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) \<and> (\<not> 0 < capAllowRead_CL (seL4_CapRights_lift cap_rights_mask) \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite)) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly)) \<and> (vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite \<longrightarrow> vmrights_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly) = maskVMRights (vmrights_to_H vm_rights) (cap_rights_to_H (seL4_CapRights_lift cap_rights_mask)) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly && mask 2 = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly))
 2. \<And>cap_rights_mask vm_rights. \<lbrakk>vm_rights && mask 2 = vm_rights; vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess\<rbrakk> \<Longrightarrow> vm_rights = 0 \<or> vm_rights = 1 \<or> vm_rights = 2 \<or> vm_rights = 3 proof (prove)
goal (1 subgoal):
 1. \<And>cap_rights_mask vm_rights. \<lbrakk>vm_rights && mask 2 = vm_rights; vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess\<rbrakk> \<Longrightarrow> vm_rights = 0 \<or> vm_rights = 1 \<or> vm_rights = 2 \<or> vm_rights = 3 proof (prove)
goal (2 subgoals):
 1. \<And>cap_rights_mask vm_rights. vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess \<Longrightarrow> 2 < size vm_rights
 2. \<And>cap_rights_mask vm_rights. \<lbrakk>vm_rights < 2\<^sup>2; vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess\<rbrakk> \<Longrightarrow> vm_rights = 0 \<or> vm_rights = 1 \<or> vm_rights = 2 \<or> vm_rights = 3 proof (prove)
goal (1 subgoal):
 1. \<And>cap_rights_mask vm_rights. \<lbrakk>vm_rights < 2\<^sup>2; vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess\<rbrakk> \<Longrightarrow> vm_rights = 0 \<or> vm_rights = 1 \<or> vm_rights = 2 \<or> vm_rights = 3 proof (prove)
goal (1 subgoal):
 1. \<And>vm_rights. \<lbrakk>vm_rights < 4; vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess; 0 < vm_rights; vm_rights \<noteq> 1; vm_rights \<noteq> 2; vm_rights \<noteq> 3\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>vm_rights. \<lbrakk>vm_rights < 4; vm_rights \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess; vm_rights \<noteq> 1; vm_rights \<noteq> 2; vm_rights \<noteq> 3; 3 < vm_rights\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!