theory Invoke_C

lemma isUntypedCap_ccap_relation_helper:
  "ccap_relation cap ccap
    \<Longrightarrow> isUntypedCap cap
    \<Longrightarrow> cap_get_tag ccap = scast cap_untyped_cap
      \<and> cap_lift ccap = Some (Cap_untyped_cap (cap_untyped_cap_lift ccap))
      \<and> cap_untyped_cap_lift ccap =
            \<lparr> capFreeIndex_CL = of_nat (capFreeIndex cap) >> 4,
                       capIsDevice_CL = from_bool (capIsDevice cap),
                       capBlockSize_CL = of_nat (capBlockSize cap),
                       capPtr_CL = capPtr cap\<rparr>" apply (simp add: cap_get_tag_isCap[symmetric]) apply (frule(1) cap_get_tag_UntypedCap[THEN iffD1]) apply (frule cap_lift_untyped_cap) apply (simp add: cap_untyped_cap_lift_def) apply (clarsimp simp: shiftl_shiftr1 word_size from_to_bool_last_bit) apply (simp add: mask_def word_bw_assocs ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap ccap; isUntypedCap cap\<rbrakk> \<Longrightarrow> cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> cap_lift ccap = Some (Cap_untyped_cap (cap_untyped_cap_lift ccap)) \<and> cap_untyped_cap_lift ccap = \<lparr>capFreeIndex_CL = word_of_nat (capFreeIndex cap) >> 4, capIsDevice_CL = from_bool (capIsDevice cap), capBlockSize_CL = word_of_nat (capBlockSize cap), capPtr_CL = capPtr cap\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap ccap; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap\<rbrakk> \<Longrightarrow> cap_lift ccap = Some (Cap_untyped_cap (cap_untyped_cap_lift ccap)) \<and> cap_untyped_cap_lift ccap = \<lparr>capFreeIndex_CL = word_of_nat (capFreeIndex cap) >> 4, capIsDevice_CL = from_bool (capIsDevice cap), capBlockSize_CL = word_of_nat (capBlockSize cap), capPtr_CL = capPtr cap\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap ccap; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap = capability.UntypedCap (to_bool (capIsDevice_CL (cap_untyped_cap_lift ccap))) (capPtr_CL (cap_untyped_cap_lift ccap)) (unat (capBlockSize_CL (cap_untyped_cap_lift ccap))) (unat (capFreeIndex_CL (cap_untyped_cap_lift ccap) << 4))\<rbrakk> \<Longrightarrow> cap_lift ccap = Some (Cap_untyped_cap (cap_untyped_cap_lift ccap)) \<and> cap_untyped_cap_lift ccap = \<lparr>capFreeIndex_CL = word_of_nat (capFreeIndex cap) >> 4, capIsDevice_CL = from_bool (capIsDevice cap), capBlockSize_CL = word_of_nat (capBlockSize cap), capPtr_CL = capPtr cap\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap ccap; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap = capability.UntypedCap (to_bool (capIsDevice_CL (cap_untyped_cap_lift ccap))) (capPtr_CL (cap_untyped_cap_lift ccap)) (unat (capBlockSize_CL (cap_untyped_cap_lift ccap))) (unat (capFreeIndex_CL (cap_untyped_cap_lift ccap) << 4)); cap_lift ccap = Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C ccap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C ccap.[0] << 0) && ~~ mask 4\<rparr>)\<rbrakk> \<Longrightarrow> cap_lift ccap = Some (Cap_untyped_cap (cap_untyped_cap_lift ccap)) \<and> cap_untyped_cap_lift ccap = \<lparr>capFreeIndex_CL = word_of_nat (capFreeIndex cap) >> 4, capIsDevice_CL = from_bool (capIsDevice cap), capBlockSize_CL = word_of_nat (capBlockSize cap), capPtr_CL = capPtr cap\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation (capability.UntypedCap (to_bool ((cap_C.words_C ccap.[Suc 0] >> 5) && 1)) (cap_C.words_C ccap.[0] && ~~ mask 4) (unat (cap_C.words_C ccap.[Suc 0] && mask 5)) (unat ((cap_C.words_C ccap.[Suc 0] >> 6) && mask 26 << 4))) ccap; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap = capability.UntypedCap (to_bool ((cap_C.words_C ccap.[Suc 0] >> 5) && 1)) (cap_C.words_C ccap.[0] && ~~ mask 4) (unat (cap_C.words_C ccap.[Suc 0] && mask 5)) (unat ((cap_C.words_C ccap.[Suc 0] >> 6) && mask 26 << 4)); cap_lift ccap = Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[Suc 0] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[Suc 0] >> 5) && 1, capBlockSize_CL = cap_C.words_C ccap.[Suc 0] && mask 5, capPtr_CL = cap_C.words_C ccap.[0] && ~~ mask 4\<rparr>)\<rbrakk> \<Longrightarrow> (cap_C.words_C ccap.[Suc 0] >> 6) && mask 26 = (cap_C.words_C ccap.[Suc 0] >> 6) && mask 26 << 4 >> 4 \<and> (cap_C.words_C ccap.[Suc 0] >> 5) && 1 = from_bool (to_bool ((cap_C.words_C ccap.[Suc 0] >> 5) && 1)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation (capability.UntypedCap (to_bool ((cap_C.words_C ccap.[Suc 0] >> 5) && 1)) (cap_C.words_C ccap.[0] && ~~ mask 4) (unat (cap_C.words_C ccap.[Suc 0] && mask 5)) (unat ((cap_C.words_C ccap.[Suc 0] >> 6) && mask 26 << 4))) ccap; cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cap = capability.UntypedCap (to_bool ((cap_C.words_C ccap.[Suc 0] >> 5) && 1)) (cap_C.words_C ccap.[0] && ~~ mask 4) (unat (cap_C.words_C ccap.[Suc 0] && mask 5)) (unat ((cap_C.words_C ccap.[Suc 0] >> 6) && mask 26 << 4)); cap_lift ccap = Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C ccap.[Suc 0] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C ccap.[Suc 0] >> 5) && 1, capBlockSize_CL = cap_C.words_C ccap.[Suc 0] && mask 5, capPtr_CL = cap_C.words_C ccap.[0] && ~~ mask 4\<rparr>)\<rbrakk> \<Longrightarrow> (cap_C.words_C ccap.[Suc 0] >> 6) && mask 26 = ((cap_C.words_C ccap.[Suc 0] >> 6) && mask 26) && mask 28 proof (prove)
goal:
No subgoals!