theory Finalise_C

lemma Zombie_new_spec:
  "\<forall>s. \<Gamma>\<turnstile> ({s} \<inter> {s. type_' s = 32 \<or> type_' s < 31}) Call Zombie_new_'proc
          {s'. cap_zombie_cap_lift (ret__struct_cap_C_' s') =
                \<lparr> capZombieID_CL = \<^bsup>s\<^esup>ptr && ~~ mask (if \<^bsup>s\<^esup>type = (1 << 5) then 5 else unat (\<^bsup>s\<^esup>type + 1))
                                    || \<^bsup>s\<^esup>number___unsigned_long && mask (if \<^bsup>s\<^esup>type = (1 << 5) then 5 else unat (\<^bsup>s\<^esup>type + 1)),
                  capZombieType_CL = \<^bsup>s\<^esup>type && mask 6 \<rparr>
               \<and> cap_get_tag (ret__struct_cap_C_' s') = scast cap_zombie_cap}" apply vcg apply (clarsimp simp: word_sle_def) apply (simp add: mask_def word_log_esimps[where 'a=32, simplified]) apply clarsimp apply (simp add: word_add_less_mono1[where k=1 and j="0x1F", simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> ({s} \<inter> \<lbrace>\<acute>type = 0x20 \<or> \<acute>type < 0x1F\<rbrace>) Call Zombie_new_'proc \<lbrace>cap_zombie_cap_lift \<acute>ret__struct_cap_C = \<lparr>capZombieID_CL = \<^bsup>s\<^esup>ptr && ~~ mask (if \<^bsup>s\<^esup>type = 1 << 5 then 5 else unat (\<^bsup>s\<^esup>type + 1)) || \<^bsup>s\<^esup>number___unsigned_long && mask (if \<^bsup>s\<^esup>type = 1 << 5 then 5 else unat (\<^bsup>s\<^esup>type + 1)), capZombieType_CL = \<^bsup>s\<^esup>type && mask 6\<rparr> \<and> cap_get_tag \<acute>ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>number___unsigned_long type ptr. type = 0x20 \<or> type < 0x1F \<Longrightarrow> 0 \<le>s 5 \<and> 5 <s 0x20 \<and> (type = 1 << unat 5 \<longrightarrow> 0 \<le>s 4 + 1 \<and> 4 + 1 <s 0x20 \<and> - 2147483648 \<le> sint 4 + sint 1 \<and> sint 4 + sint 1 \<le> 2147483647 \<and> (\<forall>ret__struct_cap_C. cap_zombie_cap_lift ret__struct_cap_C = \<lparr>capZombieID_CL = UCAST(32 \<rightarrow> 32) (ptr && ~~ ((1 << unat (4 + 1)) - 1) || number___unsigned_long && (1 << unat (4 + 1)) - 1) && mask 32, capZombieType_CL = UCAST(32 \<rightarrow> 32) (1 << unat 5) && mask 6\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> \<lparr>capZombieID_CL = UCAST(32 \<rightarrow> 32) (ptr && ~~ ((1 << unat (4 + 1)) - 1) || number___unsigned_long && (1 << unat (4 + 1)) - 1) && mask 32, capZombieType_CL = UCAST(32 \<rightarrow> 32) (1 << unat 5) && mask 6\<rparr> = \<lparr>capZombieID_CL = ptr && ~~ mask (if type = 1 << 5 then 5 else unat (type + 1)) || number___unsigned_long && mask (if type = 1 << 5 then 5 else unat (type + 1)), capZombieType_CL = type && mask 6\<rparr>)) \<and> (type \<noteq> 1 << unat 5 \<longrightarrow> type + SCAST(32 signed \<rightarrow> 32) 1 < SCAST(32 signed \<rightarrow> 32) 0x20 \<and> (\<forall>ret__struct_cap_C. cap_zombie_cap_lift ret__struct_cap_C = \<lparr>capZombieID_CL = UCAST(32 \<rightarrow> 32) (ptr && ~~ ((1 << unat (type + SCAST(32 signed \<rightarrow> 32) 1)) - 1) || number___unsigned_long && (1 << unat (type + SCAST(32 signed \<rightarrow> 32) 1)) - 1) && mask 32, capZombieType_CL = UCAST(32 \<rightarrow> 32) type && mask 6\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<longrightarrow> \<lparr>capZombieID_CL = UCAST(32 \<rightarrow> 32) (ptr && ~~ ((1 << unat (type + SCAST(32 signed \<rightarrow> 32) 1)) - 1) || number___unsigned_long && (1 << unat (type + SCAST(32 signed \<rightarrow> 32) 1)) - 1) && mask 32, capZombieType_CL = UCAST(32 \<rightarrow> 32) type && mask 6\<rparr> = \<lparr>capZombieID_CL = ptr && ~~ mask (if type = 1 << 5 then 5 else unat (type + 1)) || number___unsigned_long && mask (if type = 1 << 5 then 5 else unat (type + 1)), capZombieType_CL = type && mask 6\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>number___unsigned_long type ptr. type = 0x20 \<or> type < 0x1F \<Longrightarrow> (type = 0x20 \<longrightarrow> (\<exists>ret__struct_cap_C. cap_zombie_cap_lift ret__struct_cap_C = \<lparr>capZombieID_CL = ptr && 0xFFFFFFE0 || number___unsigned_long && 0x1F, capZombieType_CL = 0x20 && mask 6\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap) \<longrightarrow> ptr && 0xFFFFFFE0 || number___unsigned_long && 0x1F = ptr && ~~ mask 5 || number___unsigned_long && mask 5) \<and> (type \<noteq> 0x20 \<longrightarrow> type + 1 < 0x20 \<and> ((\<exists>ret__struct_cap_C. cap_zombie_cap_lift ret__struct_cap_C = \<lparr>capZombieID_CL = ptr && ~~ (2 ^ unat (type + 1) - 1) || number___unsigned_long && 2 ^ unat (type + 1) - 1, capZombieType_CL = type && mask 6\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap) \<longrightarrow> ptr && ~~ (2 ^ unat (type + 1) - 1) || number___unsigned_long && 2 ^ unat (type + 1) - 1 = ptr && ~~ mask (unat (type + 1)) || number___unsigned_long && mask (unat (type + 1)))) proof (prove)
goal (1 subgoal):
 1. \<And>type. type = 0x20 \<or> type < 0x1F \<Longrightarrow> type \<noteq> 0x20 \<longrightarrow> type + 1 < 0x20 proof (prove)
goal (1 subgoal):
 1. \<And>type. \<lbrakk>type \<noteq> 0x20; type < 0x1F\<rbrakk> \<Longrightarrow> type + 1 < 0x20 proof (prove)
goal:
No subgoals!