(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * This software may be distributed and modified according to the terms of
 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
 * See "LICENSE_GPLv2.txt" for details.
 *
 * @TAG(GD_GPL)
 *)

theory SyscallArgs_C
imports
  TcbQueue_C
  CSpace_RAB_C
  StoreWord_C
  DetWP
begin

declare word_neq_0_conv[simp del]

definition
  cintr :: "irq \<Rightarrow> word32 \<Rightarrow> errtype \<Rightarrow> bool"
where
 "cintr a x err \<equiv> x = scast EXCEPTION_PREEMPTED"

definition
  replyOnRestart :: "word32 \<Rightarrow> word32 list \<Rightarrow> bool \<Rightarrow> unit kernel"
where
 "replyOnRestart thread reply isCall \<equiv>
  do state \<leftarrow> getThreadState thread;
     when (state = Restart) (do
       _ \<leftarrow> when isCall (replyFromKernel thread (0, reply));
       setThreadState Running thread
     od)
  od"

crunch typ_at'[wp]: replyOnRestart "\<lambda>s. P (typ_at' T p s)"
  (wp: crunch_wps simp: crunch_simps)

lemmas replyOnRestart_typ_ats[wp] = typ_at_lifts [OF replyOnRestart_typ_at']

lemma replyOnRestart_invs'[wp]:
  "\<lbrace>invs'\<rbrace> replyOnRestart thread reply isCall \<lbrace>\<lambda>rv. invs'\<rbrace>"
  apply (simp add: replyOnRestart_def)
  apply (wp setThreadState_nonqueued_state_update rfk_invs' static_imp_wp)
  apply (rule hoare_vcg_all_lift)
  apply (wp setThreadState_nonqueued_state_update rfk_invs' hoare_vcg_all_lift rfk_ksQ)
 
   apply (rule hoare_strengthen_post, rule gts_sp')
  apply (clarsimp simp: st_tcb_at_tcb_at')
  apply (auto elim!: st_tcb'_weakenE st_tcb_ex_cap''
               dest: st_tcb_at_idle_thread')
  done 


declare psubset_singleton[simp]

lemma gts_eq:
  "st_tcb_at' (\<lambda>st. st = state) t s
     \<Longrightarrow> (getThreadState t s = return state s)"
  apply (simp add: Pair_fst_snd_eq return_def)
  apply (subst conj_commute, rule context_conjI)
   apply (rule no_failD[OF no_fail_getThreadState])
   apply (erule st_tcb_at_tcb_at')
  apply (rule not_psubset_eq)
   apply clarsimp
   apply (drule empty_failD [OF empty_fail_getThreadState])
   apply simp
  apply clarsimp
  apply (frule in_inv_by_hoareD[OF gts_inv'])
  apply (drule use_valid [OF _ gts_sp', OF _ TrueI])
  apply (clarsimp simp: st_tcb_at'_def obj_at'_def projectKOs objBits_simps)
  done

lemma replyOnRestart_twice':
  "((), s') \<in> fst (replyOnRestart t reply isCall s)
       \<Longrightarrow> replyOnRestart t reply' isCall' s'
             = return () s'"
  apply (clarsimp simp add: replyOnRestart_def in_monad)
  apply (drule use_valid [OF _ gts_sp', OF _ TrueI])
  apply (case_tac "state = Restart")
   apply clarsimp
   apply (drule use_valid [OF _ setThreadState_st_tcb'], simp)
   apply (simp add: gts_eq when_def cong: bind_apply_cong)
  apply (simp add: gts_eq when_def cong: bind_apply_cong)
  done

lemma replyOnRestart_twice[simplified]:
  "do replyOnRestart t reply isCall; replyOnRestart t reply' isCall'; m od
   = do replyOnRestart t reply isCall; m od"
  apply (rule ext)
  apply (rule bind_apply_cong[OF refl])
  apply simp
  apply (subst bind_apply_cong [OF _ refl])
   apply (erule replyOnRestart_twice')
  apply simp
  done

context kernel_m begin

(* FIXME: move *)
lemma register_from_H_bound[simp]:
  "unat (register_from_H v) < 18"
  by (cases v, simp_all add: "StrictC'_register_defs")

(* FIXME: move *)
lemma register_from_H_inj:
  "inj register_from_H"
  apply (rule inj_onI)
  apply (case_tac x)
  apply (case_tac y, simp_all add: "StrictC'_register_defs")+
  done

(* FIXME: move *)
lemmas register_from_H_eq_iff[simp]
    = inj_on_iff [OF register_from_H_inj, simplified]

lemma setRegister_ccorres:
  "ccorres dc xfdc \<top>
       (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace>
             \<inter> {s. w_' s = val}) []
       (asUser thread (setRegister reg val))
       (Call setRegister_'proc)"
  apply (cinit' lift: thread_' reg_' w_')
   apply (simp add: asUser_def dc_def[symmetric] split_def split del: split_if)
   apply (rule ccorres_pre_threadGet)
   apply (rule ccorres_Guard)
   apply (simp add: setRegister_def simpler_modify_def exec_select_f_singleton)
   apply (rule_tac P="\<lambda>tcb. tcbContext tcb = rv"
                in threadSet_ccorres_lemma2 [unfolded dc_def])
    apply vcg
   apply (clarsimp simp: setRegister_def HaskellLib_H.runState_def
                         simpler_modify_def typ_heap_simps)
   apply (subst StateSpace.state.fold_congs[OF refl refl])
    apply (rule globals.fold_congs[OF refl refl])
    apply (rule heap_update_field_hrs, simp)
     apply (fastforce intro: typ_heap_simps)
    apply simp
   apply (erule(1) rf_sr_tcb_update_no_queue2,
               (simp add: typ_heap_simps)+)
    apply (rule ball_tcb_cte_casesI, simp+)
   apply (clarsimp simp: ctcb_relation_def ccontext_relation_def
                  split: split_if)
  apply (clarsimp simp: Collect_const_mem register_from_H_sless
                        register_from_H_less)
  apply (auto intro: typ_heap_simps elim: obj_at'_weakenE)
  done

lemma isIRQPending_ccorres:
  "ccorres (\<lambda>rv rv'. rv' = from_bool (rv \<noteq> None)) ret__unsigned_long_'
      \<top> UNIV []
      (doMachineOp getActiveIRQ) (Call isIRQPending_'proc)"
  apply (cinit')
   apply (rule ccorres_add_return2)

   apply (ctac(no_vcg) add: getActiveIRQ_ccorres)
    apply (rule_tac P="\<lambda>s. rv \<noteq> Some 0xFF"
                   in ccorres_from_vcg_throws[where P'=UNIV])
    apply (rule allI, rule conseqPre, vcg)
    apply (clarsimp simp: return_def from_bool_def if_1_0_0
                          irqInvalid_def
                   split: option.split_asm)
   apply (wp getActiveIRQ_neq_Some0xFF)
  apply simp
  done


lemma ccorres_pre_getWorkUnits:
  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
  shows "ccorres r xf
   (\<lambda>s. \<forall>rv. ksWorkUnitsCompleted s = rv \<longrightarrow> P rv s)
   {s. \<forall>rv. s \<in> P' rv} hs (getWorkUnits >>= f) c"
  apply (simp add: getWorkUnits_def)
  apply (rule ccorres_guard_imp)
    apply (rule ccorres_symb_exec_l)
       defer
       apply wp[1]
      apply (rule gets_sp)
     apply (clarsimp simp: empty_fail_def simpler_gets_def)
    apply assumption      
   apply clarsimp
   defer
   apply (rule ccorres_guard_imp)
     apply (rule cc)
    apply clarsimp
   apply assumption
  apply clarsimp
  done

lemma preemptionPoint_ccorres:
  "ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
      invs' UNIV []
      preemptionPoint (Call preemptionPoint_'proc)"
  apply (cinit simp: workUnitsLimit_def whenE_def)   
   apply (rule ccorres_liftE_Seq)
   apply (rule ccorres_split_nothrow 
               [where P=\<top> and P'=UNIV and r'=dc and xf'=xfdc])
       apply (rule ccorres_from_vcg)
       apply (rule allI, rule conseqPre, vcg)
       apply (clarsimp simp: modifyWorkUnits_def simpler_modify_def)
       apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 
                             carch_state_relation_def 
                             cmachine_state_relation_def)
      apply ceqv
     apply (rule ccorres_liftE_Seq)
     apply (rule ccorres_pre_getWorkUnits)
     apply (rule ccorres_cond_seq)
     apply (rule_tac R="\<lambda>s. rv = ksWorkUnitsCompleted s" in ccorres_cond2)
       apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
      prefer 2
      apply simp
      apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV])
      apply (rule allI, rule conseqPre, vcg)
      apply (simp add: returnOk_def return_def)
     apply (rule ccorres_liftE_Seq)
     apply (rule ccorres_rhs_assoc)+
     apply (rule ccorres_split_nothrow 
                 [where P=\<top> and P'=UNIV and r'=dc and xf'=xfdc])
         apply (rule ccorres_from_vcg)
	 apply (rule allI, rule conseqPre, vcg)
	 apply (thin_tac "?P")+
	 apply (clarsimp simp: setWorkUnits_def simpler_modify_def)
	 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
	                       carch_state_relation_def 
                               cmachine_state_relation_def)
	apply ceqv
       apply (rule ccorres_liftE_Seq)
       apply (ctac (no_vcg) add: isIRQPending_ccorres)
        apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
        apply (rule allI, rule conseqPre, vcg)
        apply (simp add: from_bool_0 whenE_def returnOk_def throwError_def
                         return_def split: option.splits)
        apply (clarsimp simp: cintr_def exception_defs)
       apply wp
     apply vcg
    apply (unfold modifyWorkUnits_def)[1]
    apply wp
   apply vcg
  apply simp
  done 

definition
  "invocationCatch thread isBlocking isCall inject
   \<equiv>
   sum.sum_case (throwError \<circ> Inl)
    (\<lambda>oper. doE y \<leftarrow> liftE (setThreadState Structures_H.thread_state.Restart thread);
             reply \<leftarrow> RetypeDecls_H.performInvocation isBlocking isCall (inject oper)
                           >>= sum.sum_case (throwError \<circ> Inr) returnOk;
             liftE (if reply = [] then replyOnRestart thread [] isCall \<sqinter> return ()
                        else replyOnRestart thread reply isCall)
       odE)"

definition
  "intr_and_se_rel seOrIRQ status err
    \<equiv> case seOrIRQ of Inl se \<Rightarrow> syscall_error_rel se status err
           | Inr irq \<Rightarrow> cintr irq status err"

lemma intr_and_se_rel_simps[simp]:
  "intr_and_se_rel (Inl se) = syscall_error_rel se"
  "intr_and_se_rel (Inr irq) = cintr irq"
  by (rule ext | simp add: intr_and_se_rel_def)+

lemma errstate_globals_overwrite[simp]:
  "errstate (s \<lparr> globals := globals t \<rparr>) = errstate t"
  by (simp add: errstate_def)

definition
  array_to_list :: "('a['b :: finite]) \<Rightarrow> 'a list"
where
 "array_to_list arr \<equiv> map (index arr) ([0 ..< card (UNIV :: 'b set)])"

definition
  interpret_excaps :: "extra_caps_C \<Rightarrow> cte_C ptr list"
where
 "interpret_excaps excps \<equiv>
    (takeWhile (\<lambda>x. ptr_val x \<noteq> 0)
          (array_to_list (excaprefs_C excps)))"

lemma interpret_excaps_test_null[unfolded array_to_list_def, simplified]:
  "\<lbrakk> length (interpret_excaps excps) \<ge> n;
        n < length (array_to_list (excaprefs_C excps)) \<rbrakk>
     \<Longrightarrow> (index (excaprefs_C excps) n = NULL) = (length (interpret_excaps excps) = n)"
  apply (simp add: interpret_excaps_def)
  apply (rule iffI)
   apply (erule order_antisym[rotated])
   apply (rule length_takeWhile_le)
   apply (simp add: array_to_list_def)
  apply simp
  apply (drule length_takeWhile_ge)
  apply (simp add: array_to_list_def NULL_ptr_val)
  done

definition
  excaps_map :: "(capability \<times> word32) list
                     \<Rightarrow> cte_C ptr list"
where
 "excaps_map \<equiv> map (\<lambda>(cp, slot). cte_Ptr slot)"

definition
  slotcap_in_mem :: "capability \<Rightarrow> word32
                        \<Rightarrow> cte_heap \<Rightarrow> bool"
where
 "slotcap_in_mem cap slot
    \<equiv> \<lambda>cte_heap. \<exists>cte. cte_heap slot = Some cte \<and> cap = cteCap cte"

lemma slotcap_in_mem_def2:
  "slotcap_in_mem cap slot (ctes_of s)
    = cte_wp_at' (\<lambda>cte. cap = cteCap cte) slot s"
  by (simp add: slotcap_in_mem_def cte_wp_at_ctes_of)

definition
  excaps_in_mem :: "(capability \<times> word32) list
                            \<Rightarrow> cte_heap \<Rightarrow> bool"
where
 "excaps_in_mem cps \<equiv> \<lambda>cte_heap.
     \<forall>(cp, slot) \<in> set cps. slotcap_in_mem cp slot cte_heap"


lemma ccorres_alternative1:
  "ccorres rvr xf P P' hs f c
     \<Longrightarrow> ccorres rvr xf P P' hs (f \<sqinter> g) c"
  apply (simp add: ccorres_underlying_def)
  apply (erule ballEI, clarsimp del: allI)
  apply (simp add: alternative_def)
  apply (elim allEI)
  apply (auto simp: alternative_def split: xstate.split_asm)
  done

lemma ccorres_alternative2:
  "ccorres rvr xf P P' hs g c
     \<Longrightarrow> ccorres rvr xf P P' hs (f \<sqinter> g) c"
  apply (simp add: ccorres_underlying_def)
  apply (erule ballEI, clarsimp del: allI)
  apply (simp add: alternative_def)
  apply (elim allEI)
  apply (auto simp: alternative_def split: xstate.split_asm)
  done

lemma o_xo_injector:
  "((f o f') \<currency> r) = ((f \<currency> r) o sum_case (Inl o f') Inr)"
  by (intro ext, simp split: sum.split)

lemma ccorres_invocationCatch_Inr:
  "ccorres (f \<currency> r) xf P P' hs
   (invocationCatch thread isBlocking isCall injector (Inr v)) c
   =
   ccorres ((f \<circ> Inr) \<currency> r) xf P P' hs
   (do _ \<leftarrow> setThreadState Restart thread;
       doE reply \<leftarrow> performInvocation isBlocking isCall (injector v);
           if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk ()
                         else liftE (replyOnRestart thread reply isCall)
       odE od) c"
  apply (simp add: invocationCatch_def liftE_bindE o_xo_injector)
  apply (subst ccorres_liftM_simp[symmetric])
  apply (simp add: liftM_def bind_assoc bindE_def)
  apply (rule_tac f="\<lambda>f. ccorres ?rvr ?xs P P' hs f c" in arg_cong)
  apply (rule ext)
  apply (rule bind_apply_cong [OF refl])+
  apply (simp add: throwError_bind returnOk_bind lift_def liftE_def
                   alternative_bind
            split: sum.split split_if)
  apply (simp add: throwError_def)
  done

lemma getSlotCap_eq:
  "slotcap_in_mem cap slot (ctes_of s)
    \<Longrightarrow> getSlotCap slot s = return cap s"
  apply (clarsimp simp: slotcap_in_mem_def2 getSlotCap_def)
  apply (frule cte_wp_at_weakenE'[OF _ TrueI])
  apply (drule no_failD[OF no_fail_getCTE])
  apply (clarsimp simp: cte_wp_at'_def getCTE_def[symmetric]
                        bind_def return_def)
  done

lemma getSlotCap_ccorres_fudge:
  "ccorres_underlying sr Gamm rvr xf ar axf P Q hs (do rv \<leftarrow> getSlotCap slot; _ \<leftarrow> assert (rv = cp); a rv od) c
    \<Longrightarrow> ccorres_underlying sr Gamm rvr xf ar axf
          (P and (slotcap_in_mem cp slot o ctes_of))
          Q hs (a cp) c"
  apply (simp add: ccorres_underlying_def)
  apply (erule ballEI, clarsimp del: allI)
  apply (simp add: bind_apply_cong [OF getSlotCap_eq refl]
             cong: xstate.case_cong)
  done

lemma getSlotCap_ccorres_fudge_n:
  "ccorres_underlying sr Gamm rvr xf ar axf P Q hs
     (do rv \<leftarrow> getSlotCap (snd (vals ! n));
         _ \<leftarrow> assert (rv = fst (vals ! n)); a od) c
    \<Longrightarrow> ccorres_underlying sr Gamm rvr xf ar axf
            ((\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = fst (vals ! n))
                        (snd (vals ! n)) s \<longrightarrow> P s)
              and (excaps_in_mem vals \<circ> ctes_of) and K (n < length vals)) Q
           hs a c"
  apply (rule ccorres_guard_imp2)
   apply (erule getSlotCap_ccorres_fudge)
  apply (clarsimp simp: excaps_in_mem_def)
  apply (drule bspec, erule nth_mem)
  apply (clarsimp simp: slotcap_in_mem_def cte_wp_at_ctes_of)
  done

definition
 "is_syscall_error_code f code
    = (\<forall>Q. (\<Gamma> \<turnstile> {s. global_exn_var_'_update (\<lambda>_. Return)
                      (ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR)
                        (globals_update (current_syscall_error_'_update f) s)) \<in> Q}
           code {}, Q))"

abbreviation(input)
  (* no longer needed *)
  "Basic_with_globals f == (Basic f)"

lemma is_syscall_error_codes:
  "is_syscall_error_code f
       (Basic (globals_update (current_syscall_error_'_update f));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  "is_syscall_error_code (f' o f)
       (Basic (globals_update (current_syscall_error_'_update f));;
        Basic (globals_update (current_syscall_error_'_update f'));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  "is_syscall_error_code (f'' o f' o f)
       (Basic (globals_update (current_syscall_error_'_update f));;
        Basic (globals_update (current_syscall_error_'_update f'));;
        Basic (globals_update (current_syscall_error_'_update f''));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  "is_syscall_error_code f
       (SKIP;;
        Basic (globals_update (current_syscall_error_'_update f));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  "is_syscall_error_code (f' o f)
       (SKIP;;
        Basic (globals_update (current_syscall_error_'_update f));;
        Basic (globals_update (current_syscall_error_'_update f'));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  "is_syscall_error_code (f'' o f' o f)
       (SKIP;;
        Basic (globals_update (current_syscall_error_'_update f));;
        Basic (globals_update (current_syscall_error_'_update f'));;
        Basic (globals_update (current_syscall_error_'_update f''));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  "is_syscall_error_code f
       (Basic_with_globals (globals_update (current_syscall_error_'_update f));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  "is_syscall_error_code (f' o f)
       (Basic_with_globals (globals_update (current_syscall_error_'_update f));;
        Basic_with_globals (globals_update (current_syscall_error_'_update f'));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  "is_syscall_error_code (f'' o f' o f)
       (Basic_with_globals (globals_update (current_syscall_error_'_update f));;
        Basic_with_globals (globals_update (current_syscall_error_'_update f'));;
        Basic_with_globals (globals_update (current_syscall_error_'_update f''));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  "is_syscall_error_code f
       (SKIP;;
        Basic_with_globals (globals_update (current_syscall_error_'_update f));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  "is_syscall_error_code (f' o f)
       (SKIP;;
        Basic_with_globals (globals_update (current_syscall_error_'_update f));;
        Basic_with_globals (globals_update (current_syscall_error_'_update f'));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  "is_syscall_error_code (f'' o f' o f)
       (SKIP;;
        Basic_with_globals (globals_update (current_syscall_error_'_update f));;
        Basic_with_globals (globals_update (current_syscall_error_'_update f'));;
        Basic_with_globals (globals_update (current_syscall_error_'_update f''));;
        return_C ret__unsigned_long_'_update (\<lambda>_. scast EXCEPTION_SYSCALL_ERROR))"
  by ((rule iffD2[OF is_syscall_error_code_def], intro allI,
      rule conseqPre, vcg, safe, (simp_all add: o_def)?)+)

lemma syscall_error_throwError_ccorres_direct:
  "\<lbrakk> is_syscall_error_code f code;
     \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err \<rbrakk>
   \<Longrightarrow>
   ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id v' ret__unsigned_long_')
      \<top> (UNIV) (SKIP # hs)
      (throwError (Inl err)) code"
  apply (rule ccorres_from_vcg_throws)
  apply (rule allI, rule conseqPre)
  apply (erule iffD1[OF is_syscall_error_code_def, THEN spec])
  apply (clarsimp simp: throwError_def return_def)
  apply (simp add: syscall_error_rel_def exception_defs)
  done

lemma syscall_error_throwError_ccorres_succs:
  "\<lbrakk> is_syscall_error_code f code;
     \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err \<rbrakk>
   \<Longrightarrow>
   ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id v' ret__unsigned_long_')
      \<top> (UNIV) (SKIP # hs)
      (throwError (Inl err)) (code ;; remainder)"
  apply (rule ccorres_guard_imp2,
         rule ccorres_split_throws)
    apply (erule syscall_error_throwError_ccorres_direct)
    apply simp
   apply (rule HoarePartialProps.augment_Faults)
    apply (erule iffD1[OF is_syscall_error_code_def, THEN spec])
   apply simp+
  done

lemmas syscall_error_throwError_ccorres_n =
    is_syscall_error_codes[THEN syscall_error_throwError_ccorres_direct,
                           simplified o_apply]
    is_syscall_error_codes[THEN syscall_error_throwError_ccorres_succs,
                           simplified o_apply]

definition idButNot :: "'a \<Rightarrow> 'a"
where "idButNot x = x"

lemma interpret_excaps_test_null2:
  "n < 3 \<Longrightarrow>
   (index (excaprefs_C excps) n = NULL)
      = (length (interpret_excaps excps) \<le> n
            \<and> index (idButNot excaprefs_C excps) n = NULL)"
  unfolding idButNot_def
  apply safe
  apply (rule ccontr, simp only: linorder_not_le)
  apply (frule(1) interpret_excaps_test_null [OF order_less_imp_le])
  apply simp
  done

lemma interpret_excaps_eq[unfolded array_to_list_def, simplified]:
  "interpret_excaps excps = xs \<Longrightarrow>
   \<forall>n < length xs. (index (excaprefs_C excps) n) = (xs ! n)
         \<and> (length xs < length (array_to_list (excaprefs_C excps))
              \<longrightarrow> index (excaprefs_C excps) (length xs) = NULL)"
  apply (clarsimp simp: interpret_excaps_def)
  apply (drule length_takeWhile_gt)
  apply (clarsimp simp: nth_append)
  apply (clarsimp simp: array_to_list_def)
  apply (frule_tac f=length in arg_cong, subst(asm) length_map,
         simp(no_asm_use))
  apply (rule conjI)
   apply (rule trans, erule map_upt_eq_vals_D, simp)
   apply (simp add: nth_append)
  apply clarsimp
  apply (frule nth_length_takeWhile)
  apply (rule trans, erule map_upt_eq_vals_D, simp)
  apply (simp add: nth_append NULL_ptr_val)
  done

lemma ctes_of_0_contr[elim]:
  "\<lbrakk> ctes_of s 0 = Some cte; valid_mdb' s \<rbrakk> \<Longrightarrow> P"
  by (drule(1) ctes_of_not_0, simp)

lemma invocationCatch_use_injection_handler:
  "(v >>= invocationCatch thread isBlocking isCall injector)
     = (injection_handler Inl v >>=E
           (invocationCatch thread isBlocking isCall injector o Inr))"
  apply (simp add: injection_handler_def handleE'_def
                   bind_bindE_assoc)
  apply (rule ext, rule bind_apply_cong [OF refl])
  apply (simp add: invocationCatch_def return_returnOk
            split: sum.split)
  done

lemma injection_handler_returnOk:
  "injection_handler injector (returnOk v) = returnOk v"
  by (simp add: returnOk_liftE injection_liftE)

lemma injection_handler_If:
  "injection_handler injector (If P a b)
     = If P (injection_handler injector a)
            (injection_handler injector b)"
  by (simp split: split_if)

(* FIXME: duplicated in CSpace_All *)
lemma injection_handler_liftM:
  "injection_handler f
    = liftM (\<lambda>v. case v of Inl ex \<Rightarrow> Inl (f ex) | Inr rv \<Rightarrow> Inr rv)"
  apply (intro ext, simp add: injection_handler_def liftM_def
                              handleE'_def)
  apply (rule bind_apply_cong, rule refl)
  apply (simp add: throwError_def split: sum.split)
  done

lemma injection_handler_throwError:
  "injection_handler f (throwError v) = throwError (f v)"
  by (simp add: injection_handler_def handleE'_def
                throwError_bind)

lemmas injection_handler_bindE = injection_bindE [OF refl refl]
lemmas injection_handler_wp = injection_wp [OF refl]

lemma ccorres_injection_handler_csum1:
  "ccorres (f \<currency> r) xf P P' hs a c
    \<Longrightarrow> ccorres
           ((\<lambda>rv a b. \<exists>rv'. rv = injector rv' \<and> f rv' a b) \<currency> r) xf P P' hs
           (injection_handler injector a) c"
  apply (simp add: injection_handler_liftM)
  apply (erule ccorres_rel_imp)
  apply (auto split: sum.split)
  done

lemma ccorres_injection_handler_csum2:
  "ccorres ((f o injector) \<currency> r) xf P P' hs a c
    \<Longrightarrow> ccorres (f \<currency> r) xf P P' hs
            (injection_handler injector a) c"
  apply (simp add: injection_handler_liftM)
  apply (erule ccorres_rel_imp)
  apply (auto split: sum.split)
  done

definition
  is_nondet_refinement :: "('a, 's) nondet_monad
                              \<Rightarrow> ('a, 's) nondet_monad \<Rightarrow> bool"
where
 "is_nondet_refinement f g \<equiv> \<forall>s. (snd (f s) \<longrightarrow> snd (g s)) \<and> fst (f s) \<subseteq> fst (g s)"

lemma is_nondet_refinement_refl[simp]:
  "is_nondet_refinement a a"
  by (simp add: is_nondet_refinement_def)

lemma is_nondet_refinement_bind:
  "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk>
     \<Longrightarrow> is_nondet_refinement (a >>= b) (c >>= d)"
  apply (clarsimp simp: is_nondet_refinement_def bind_def split_def)
  apply blast
  done

lemma is_nondet_refinement_bindE:
  "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk>
     \<Longrightarrow> is_nondet_refinement (a >>=E b) (c >>=E d)"
  apply (simp add: bindE_def)
  apply (erule is_nondet_refinement_bind)
  apply (simp add: lift_def split: sum.split)
  done

lemma ccorres_nondet_refinement:
  "\<lbrakk> is_nondet_refinement a b;
       ccorres_underlying sr Gamm rvr xf arrel axf G G' hs a c \<rbrakk>
     \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G G' hs b c"
  apply (simp add: ccorres_underlying_def is_nondet_refinement_def
                   split_def)
  apply (rule ballI, drule(1) bspec)
  apply (intro impI)
  apply (drule mp, blast)
  apply (elim allEI)
  apply (clarsimp split: xstate.split_asm)
  apply blast
  done

lemma is_nondet_refinement_alternative1:
  "is_nondet_refinement a (a \<sqinter> b)"
  by (clarsimp simp add: is_nondet_refinement_def alternative_def)

lemma ccorres_defer:
  assumes c: "ccorres r xf P P' hs H C"
  assumes f: "no_fail Q H"
  shows "ccorres (\<lambda>_. r rv) xf (\<lambda>s. P s \<and> Q s \<and> (P s \<and> Q s \<longrightarrow> fst (H s) = {(rv,s)})) P' hs (return ()) C"
  using c
  apply (clarsimp simp: ccorres_underlying_def split: xstate.splits)
  apply (drule (1) bspec)
  apply clarsimp
  apply (erule impE)
   apply (insert f)[1]
   apply (clarsimp simp: no_fail_def)
  apply (clarsimp simp: return_def)
  apply (rule conjI)
   apply clarsimp
   apply (erule_tac x=n in allE)
   apply (erule_tac x="Normal s" in allE)
   apply (clarsimp simp: unif_rrel_def)
  apply fastforce
  done

lemma no_fail_loadWordUser:
  "no_fail (pointerInUserData x and K (is_aligned x 2)) (loadWordUser x)"
  apply (simp add: loadWordUser_def)
  apply (rule no_fail_pre, wp no_fail_stateAssert)
  apply simp
  done

lemma no_fail_getMRs:
  "no_fail (tcb_at' thread and option_case \<top> valid_ipc_buffer_ptr' buffer)
           (getMRs thread buffer info)"
  apply (rule det_wp_no_fail)
  apply (rule det_wp_getMRs)
  done

lemma msgRegisters_scast:
  "n < unat (scast n_msgRegisters :: word32) \<Longrightarrow> 
  unat (scast (index msgRegisters n)::word32) = unat (index msgRegisters n)"
  apply (simp add: msgRegisters_def fupdate_def update_def n_msgRegisters_def fcp_beta 
                   Kernel_C.R2_def Kernel_C.R3_def Kernel_C.R4_def Kernel_C.R5_def 
                   Kernel_C.R6_def Kernel_C.R7_def)
  done
   
lemma msgRegisters_ccorres:
  "n < unat n_msgRegisters \<Longrightarrow> 
  register_from_H (State_H.msgRegisters ! n) = (index msgRegisters n)"
  apply (simp add: msgRegisters_def msgRegisters_unfold fupdate_def)
  apply (simp add: Arrays.update_def n_msgRegisters_def fcp_beta nth_Cons' split: split_if)
  done


lemma asUser_cur_obj_at':
  assumes f: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
  shows "\<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. P (tcbContext tcb)) (ksCurThread s) s \<and> t = ksCurThread s\<rbrace> 
          asUser t f \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. Q rv (tcbContext tcb)) (ksCurThread s) s\<rbrace>"
  apply (simp add: asUser_def split_def)
  apply (wp)
    apply (rule hoare_lift_Pf2 [where f=ksCurThread])
    apply (wp threadSet_obj_at')
  apply (clarsimp simp: threadGet_def)
  apply (wp getObject_tcb_wp)
  apply clarsimp
  apply (drule obj_at_ko_at')
  apply clarsimp
  apply (rename_tac tcb)
  apply (rule_tac x=tcb in exI)
  apply clarsimp
  apply (drule use_valid, rule f, assumption)
  apply clarsimp
  done

lemma asUser_const_rv:
  assumes f: "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv\<rbrace>"
  shows "\<lbrace>\<lambda>s. P\<rbrace> asUser t f \<lbrace>\<lambda>rv s. Q rv\<rbrace>"
  apply (simp add: asUser_def split_def)
  apply (wp)
  apply (clarsimp simp: threadGet_def)
  apply (wp getObject_tcb_wp)
  apply clarsimp
  apply (drule obj_at_ko_at')
  apply clarsimp
  apply (rename_tac tcb)
  apply (rule_tac x=tcb in exI)
  apply clarsimp
  apply (drule use_valid, rule f, assumption)
  apply clarsimp
  done
  

lemma getMRs_tcbContext:
  "\<lbrace>\<lambda>s. n < unat n_msgRegisters \<and> n < unat (msgLength info) \<and> thread = ksCurThread s \<and> cur_tcb' s\<rbrace>
  getMRs thread buffer info 
  \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. tcbContext tcb (State_H.msgRegisters ! n) = rv ! n) (ksCurThread s) s\<rbrace>"
  apply (rule hoare_assume_pre)
  apply (elim conjE)
  apply (thin_tac "thread = ?t")
  apply (clarsimp simp add: getMRs_def)
  apply (rule hoare_pre)
   apply (wp|wpc)+
     apply (rule_tac P="n < length x" in hoare_gen_asm)
     apply (clarsimp simp: nth_append)
     apply (wp mapM_wp' static_imp_wp)
    apply simp 
    apply (rule asUser_cur_obj_at')
    apply (simp add: getRegister_def msgRegisters_unfold)
    apply (simp add: mapM_Cons bind_assoc mapM_empty)
    apply wp[1]
   apply (wp hoare_drop_imps hoare_vcg_all_lift)
   apply (wp asUser_cur_obj_at')
    apply (simp add: getRegister_def msgRegisters_unfold)
    apply (simp add: mapM_Cons bind_assoc mapM_empty)
    apply (wp asUser_const_rv)
   apply clarsimp
   apply (wp asUser_const_rv)
  apply (clarsimp simp: n_msgRegisters_def msgRegisters_unfold)
  apply (simp add: nth_Cons' cur_tcb'_def split: split_if)
  done

lemma threadGet_tcbIpcBuffer_ccorres [corres]:
  "ccorres (op =) w_bufferPtr_' (tcb_at' tptr) UNIV hs 
           (threadGet tcbIPCBuffer tptr)
           (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr tptr\<rbrace>
               (\<acute>w_bufferPtr :==
                  h_val (hrs_mem \<acute>t_hrs)
                   (Ptr &(tcb_ptr_to_ctcb_ptr tptr\<rightarrow>[''tcbIPCBuffer_C''])::word32 ptr)))"
  apply (rule ccorres_guard_imp2)
   apply (rule ccorres_add_return2)
   apply (rule ccorres_pre_threadGet)
   apply (rule_tac P = "obj_at' (\<lambda>tcb. tcbIPCBuffer tcb = x) tptr" and
                   P'="{s'. \<exists>ctcb.
          cslift s' (tcb_ptr_to_ctcb_ptr tptr) = Some ctcb \<and>
                 tcbIPCBuffer_C ctcb = x }" in ccorres_from_vcg)
   apply (rule allI, rule conseqPre, vcg)
   apply clarsimp
   apply (clarsimp simp: return_def typ_heap_simps')
  apply (clarsimp simp: obj_at'_def ctcb_relation_def)
  done 

(* FIXME: move *)
lemma ccorres_bool_cases:
  assumes P: "ccorres r xf P P' hs (a True) (c True)"
  assumes Q: "ccorres r xf Q Q' hs (a False) (c False)"
  shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s))
                      ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'}) 
                      hs (a b) (c b)"
  apply (cases b)
   apply (auto simp: P Q)
  done

lemma ccorres_cond_both':
  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
  shows  "ccorres_underlying sr G r xf arrel axf
          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
          hs 
          (if P then a else b) (Cond P' c d)"
  apply (rule ccorres_guard_imp2)
   apply (rule ccorres_if_lhs)
    apply (rule ccorres_cond_true)
    apply (erule ac)
   apply (rule ccorres_cond_false)
   apply (erule bd)
  apply clarsimp
  apply (frule abs[rule_format, OF conjI], simp+)
  done

lemma pageBitsForSize_32 [simp]:
  "pageBitsForSize sz < 32"
  by (cases sz, auto)

lemma ccap_relation_frame_tags:
  "ccap_relation (ArchObjectCap (PageCap v0 v1 v2 v3)) cap \<Longrightarrow> 
  cap_get_tag cap = scast cap_frame_cap \<or> cap_get_tag cap = scast cap_small_frame_cap"
  apply (case_tac "v2 = ARMSmallPage")
   apply (auto simp: cap_get_tag_isCap_unfolded_H_cap)
  done

(* FIXME: move *)
lemma ccorres_bool_cases':
  assumes P: "b \<Longrightarrow> ccorres r xf P P' hs (a True) (c True)"
  assumes Q: "\<not> b \<Longrightarrow> ccorres r xf Q Q' hs (a False) (c False)"
  shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s))
                      ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'}) 
                      hs (a b) (c b)"
  apply (cases b)
   apply (auto simp: P Q)
  done

lemma lookupIPCBuffer_ccorres:
  "ccorres (op = \<circ> option_to_ptr) ret__ptr_to_unsigned_long_'
           (tcb_at' t) 
           (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr t}
                  \<inter> {s. isReceiver_' s = from_bool isReceiver}) []
      (lookupIPCBuffer isReceiver t) (Call lookupIPCBuffer_'proc)"
  apply (cinit lift: thread_' isReceiver_')
   apply (unfold ArchVSpace_H.lookupIPCBuffer_def Let_def)
   apply (rule ccorres_split_nothrow)
       apply simp
       apply (rule threadGet_tcbIpcBuffer_ccorres)
      apply ceqv
     apply (simp add: getThreadBufferSlot_def locateSlot_conv
                 del: Collect_const)
     apply (rule ccorres_getSlotCap_cte_at)
     apply (rule ccorres_move_c_guard_cte)
     apply (ctac (no_vcg))
       apply csymbr
       apply (rule_tac b="isArchObjectCap rva \<and> isPageCap (capCap rva)" in ccorres_bool_cases')
        apply simp
        apply (rule ccorres_symb_exec_r)
          apply (rule_tac b="capVPSize (capCap rva) \<noteq> ARMSmallPage" in ccorres_bool_cases')
           apply (rule ccorres_cond_true_seq)
           apply (rule ccorres_rhs_assoc)+
           apply csymbr
           apply csymbr
           apply (simp (no_asm) add: if_1_0_0 del: Collect_const)
           apply (rule ccorres_cond_false_seq)
           apply simp
           apply csymbr
           apply (rule_tac Q="\<top>" and Q'=\<top> in ccorres_cond_both')
             apply (clarsimp simp: from_bool_0 isCap_simps Collect_const_mem)
             apply (frule ccap_relation_PageCap_generics)
             apply clarsimp
             apply (clarsimp simp: vmrights_to_H_def)
             apply (simp add: Kernel_C.VMReadOnly_def Kernel_C.VMKernelOnly_def 
                              Kernel_C.VMReadWrite_def Kernel_C.VMNoAccess_def
                         split: split_if)
             apply (drule less_4_cases)
             apply auto[1]
            apply (rule ccorres_rhs_assoc)+
            apply csymbr
            apply csymbr
            apply csymbr
            apply csymbr
            apply csymbr
            apply (rule ccorres_Guard)
            apply simp
            apply (rule ccorres_assert)+
            apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
            apply (rule allI, rule conseqPre, vcg)
            apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps)
            apply (clarsimp simp: mask_def)
            apply (clarsimp simp: ccap_relation_PageCap_generics)
           apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
           apply (rule allI, rule conseqPre, vcg)
           apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def)
          apply (rule ccorres_cond_false_seq)
          apply (simp (no_asm))
          apply (rule ccorres_cond_false_seq)
          apply (simp (no_asm))
          apply csymbr 
          apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_cond_both')
            apply (clarsimp simp: from_bool_0 isCap_simps)
            apply (frule ccap_relation_PageCap_generics)
            apply clarsimp
            apply (clarsimp simp: vmrights_to_H_def)
            apply (simp add: Kernel_C.VMReadOnly_def Kernel_C.VMKernelOnly_def 
                             Kernel_C.VMReadWrite_def Kernel_C.VMNoAccess_def
                        split: split_if)
            apply clarsimp
            apply (drule less_4_cases)
            apply auto[1]
           apply (rule ccorres_rhs_assoc)+
           apply csymbr
           apply csymbr
           apply csymbr
           apply csymbr
           apply csymbr
           apply (rule ccorres_Guard)
           apply simp
           apply (rule ccorres_assert)+
           apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
           apply (rule allI, rule conseqPre, vcg)
           apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def isCap_simps)
           apply (clarsimp simp: mask_def)
           apply (clarsimp simp: ccap_relation_PageCap_generics)
          apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
          apply (rule allI, rule conseqPre, vcg)
          apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def)
         apply (clarsimp simp: from_bool_0)
         apply vcg
        apply (rule conseqPre, vcg)
        apply clarsimp
       apply (simp (no_asm))
       apply (rule ccorres_symb_exec_r)
         apply (rule ccorres_cond_true_seq)
         apply (rule ccorres_rhs_assoc)+
         apply csymbr
         apply csymbr
         apply (rule ccorres_cond_true_seq)
         apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
         apply (rule allI, rule conseqPre, vcg)
         apply (clarsimp simp: return_def option_to_ptr_def option_to_0_def)
        apply vcg
       apply (rule conseqPre, vcg)
       apply clarsimp
      apply (rule_tac Q=\<top> in hoare_weaken_pre,simp add:hoare_TrueI)
      apply assumption
     apply (clarsimp simp: if_1_0_0 Collect_const_mem)
     apply (rule conjI)
      apply (clarsimp simp: isCap_simps word_less_nat_alt)
      apply (frule ccap_relation_frame_tags)
      apply (simp add: generic_frame_cap_size)
      apply (simp add: cap_get_tag_PageCap_small_frame cap_get_tag_PageCap_frame)
      apply (auto simp: cap_tag_defs)[1]
     apply (auto simp: cap_get_tag_isCap isArchPageCap_def isCap_simps
                split: capability.split arch_capability.split)[1]
    apply wp
   apply vcg
  apply (simp add: word_sle_def Collect_const_mem
                   tcb_cnode_index_defs tcbSlots cte_level_bits_def
                   size_of_def)
  done

lemma doMachineOp_pointerInUserData:
  "\<lbrace>pointerInUserData p\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. pointerInUserData p\<rbrace>"
  by (simp add: pointerInUserData_def) wp

lemma loadWordUser_wp:
  "\<lbrace>\<lambda>s. is_aligned p 2 \<and> (\<forall>v. user_word_at v p s \<longrightarrow> P v s)\<rbrace>
    loadWordUser p
   \<lbrace>P\<rbrace>"
  apply (simp add: loadWordUser_def loadWord_def stateAssert_def
                   user_word_at_def valid_def)
  apply (clarsimp simp: in_monad in_doMachineOp)
  done

lemma ccorres_pre_loadWordUser:
  "(\<And>rv. ccorres r xf (P rv) (Q rv) hs (a rv) c) \<Longrightarrow>
   ccorres r xf (valid_pspace' and K (is_aligned ptr 2) and
                 (\<lambda>s. \<forall>v. user_word_at v ptr s \<longrightarrow> P v s))
     {s. \<forall>v. cslift s (Ptr ptr :: word32 ptr) = Some v \<longrightarrow>
               s \<in> Q v} hs
     (loadWordUser ptr >>= a) c"
  apply (rule ccorres_guard_imp)
    apply (rule_tac Q="\<lambda>rv. P rv and user_word_at rv ptr" and Q'=Q in 
          ccorres_symb_exec_l [OF _ loadWordUser_inv loadWordUser_wp])
     apply (fastforce intro: ccorres_guard_imp)
    apply simp
   apply simp
  apply clarsimp
  apply (drule(1) user_word_at_cross_over, simp)
  apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff)
  done

lemma loadWordUser_user_word_at:
  "\<lbrace>\<lambda>s. \<forall>rv. user_word_at rv x s \<longrightarrow> Q rv s\<rbrace> loadWordUser x \<lbrace>Q\<rbrace>"
  apply (simp add: loadWordUser_def user_word_at_def
                   doMachineOp_def split_def)
  apply wp
  apply (clarsimp simp: pointerInUserData_def
                        loadWord_def in_monad
                        is_aligned_mask)
  done

lemma mapM_loadWordUser_user_words_at:
  "\<lbrace>\<lambda>s. \<forall>rv. (\<forall>x < length xs. user_word_at (rv ! x) (xs ! x) s)
              \<and> length rv = length xs \<longrightarrow> Q rv s\<rbrace>
    mapM loadWordUser xs \<lbrace>Q\<rbrace>"
  apply (induct xs arbitrary: Q)
   apply (simp add: mapM_def sequence_def)
   apply wp
  apply (simp add: mapM_Cons)
  apply wp
   apply assumption
  apply (wp loadWordUser_user_word_at)
  apply clarsimp
  apply (drule spec, erule mp)
  apply clarsimp
  apply (case_tac x)
   apply simp
  apply simp
  done


lemma getMRs_user_word:
  "\<lbrace>\<lambda>s. valid_ipc_buffer_ptr' buffer s \<and> i < msgLength info
      \<and> msgLength info \<le> msgMaxLength \<and> i >= scast n_msgRegisters\<rbrace>
  getMRs thread (Some buffer) info  
  \<lbrace>\<lambda>xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\<rbrace>"
  apply (rule hoare_assume_pre)
  apply (elim conjE)
  apply (thin_tac "valid_ipc_buffer_ptr' ?x ?y")
  apply (simp add: getMRs_def)
  apply wp
   apply (rule_tac P="length hardwareMRValues = unat n_msgRegisters" in hoare_gen_asm)
   apply (clarsimp simp: nth_append word_le_nat_alt 
                         word_less_nat_alt word_size
                         linorder_not_less [symmetric])
   apply (wp mapM_loadWordUser_user_words_at)
   apply (wp hoare_vcg_all_lift)
    apply (rule_tac Q="\<lambda>_. \<top>" in hoare_strengthen_post)
     apply wp
    apply clarsimp
    defer
    apply simp
    apply (wp asUser_const_rv)
    apply (simp add: msgRegisters_unfold n_msgRegisters_def)
   apply simp
  apply (erule_tac x="unat i - unat n_msgRegisters" in allE)
  apply (erule impE) 
   apply (simp add: msgRegisters_unfold
                    msgMaxLength_def msgLengthBits_def n_msgRegisters_def)
   apply (drule (1) order_less_le_trans)
   apply (simp add: word_less_nat_alt word_le_nat_alt)
  apply (simp add: msgRegisters_unfold
                   msgMaxLength_def msgLengthBits_def n_msgRegisters_def)
  apply (simp add: upto_enum_word del: upt_rec_numeral)
  apply (subst (asm) nth_map)
   apply (simp del: upt_rec_numeral)
   apply (drule (1) order_less_le_trans)
   apply (simp add: word_less_nat_alt word_le_nat_alt)
  apply (subst (asm) nth_upt)
   apply simp
   apply (drule (1) order_less_le_trans)
   apply (simp add: word_less_nat_alt word_le_nat_alt)
  apply (simp add: word_le_nat_alt add_ac mult_ac)
  done

declare split_if [split]

definition
  "getMRs_rel args buffer \<equiv> \<lambda>s. \<exists>mi. msgLength mi \<le> msgMaxLength \<and> fst (getMRs (ksCurThread s) buffer mi s) = {(args, s)}"

definition
  "sysargs_rel args buffer \<equiv> 
          cur_tcb'
          and option_case \<top> valid_ipc_buffer_ptr' buffer
          and getMRs_rel args buffer
          and (\<lambda>_. length args > unat (scast n_msgRegisters :: word32) \<longrightarrow> buffer \<noteq> None)"

definition
  "sysargs_rel_n args buffer n \<equiv> \<lambda>s. n < length args \<and> (unat (scast n_msgRegisters :: word32) \<le> n \<longrightarrow> buffer \<noteq> None)"

lemma sysargs_rel_to_n:
  "sysargs_rel args buffer s \<Longrightarrow> sysargs_rel_n args buffer n s = (n < length args)"
  by (auto simp add: sysargs_rel_def sysargs_rel_n_def)

lemma getMRs_rel:
  "\<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength \<and> thread = ksCurThread s \<and> 
        option_case \<top> valid_ipc_buffer_ptr' buffer s \<and>
        cur_tcb' s\<rbrace> 
  getMRs thread buffer mi \<lbrace>\<lambda>args. getMRs_rel args buffer\<rbrace>"
  apply (simp add: getMRs_rel_def)
  apply (rule hoare_pre)
   apply (rule_tac x=mi in hoare_vcg_exI) 
   apply wp
   apply (rule_tac Q="\<lambda>rv s. thread = ksCurThread s \<and> fst (getMRs thread buffer mi s) = {(rv,s)}" in hoare_strengthen_post)
    apply (wp det_result det_wp_getMRs)
   apply clarsimp
  apply (clarsimp simp: cur_tcb'_def)
  done

lemma length_msgRegisters:
  "length State_H.msgRegisters = unat (scast n_msgRegisters :: word32)"
  by (simp add: msgRegisters_unfold n_msgRegisters_def)

lemma getMRs_len[simplified]:
  "\<lbrace>\<top>\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. length args > unat (scast n_msgRegisters :: word32) \<longrightarrow> buffer \<noteq> None\<rbrace>"
  apply (simp add: getMRs_def)
  apply (cases buffer, simp_all add:hoare_TrueI)
  apply (wp asUser_const_rv | simp)+
  apply (simp add: length_msgRegisters)
  done

lemma getMRs_sysargs_rel:  
  "\<lbrace>(\<lambda>s. thread = ksCurThread s) and cur_tcb' and option_case \<top> valid_ipc_buffer_ptr' buffer and K (msgLength mi \<le> msgMaxLength)\<rbrace> 
  getMRs thread buffer mi \<lbrace>\<lambda>args. sysargs_rel args buffer\<rbrace>"
  apply (simp add: sysargs_rel_def)
  apply (wp getMRs_rel getMRs_len|simp)+
  done

lemma ccorres_assume_pre:
  assumes "\<And>s. P s \<Longrightarrow> ccorres r xf (P and (\<lambda>s'. s' = s)) P' hs H C"
  shows "ccorres r xf P P' hs H C"
  apply (clarsimp simp: ccorres_underlying_def)
  apply (frule assms)
  apply (simp add: ccorres_underlying_def)
  apply blast
  done

lemma getMRs_length:
  "\<lbrace>\<lambda>s. msgLength mi \<le> msgMaxLength\<rbrace> getMRs thread buffer mi
  \<lbrace>\<lambda>args s. if buffer = None then length args = min (unat (scast n_msgRegisters :: word32)) (unat (msgLength mi))
            else length args = unat (msgLength mi)\<rbrace>"
  apply (cases buffer)
   apply (simp add: getMRs_def)
   apply (rule hoare_pre, wp)
    apply (rule asUser_const_rv)
    apply simp
    apply (wp mapM_length)
   apply (simp add: min_def length_msgRegisters)
  apply clarsimp
  apply (simp add: getMRs_def)
  apply (rule hoare_pre, wp)
    apply simp
    apply (wp mapM_length asUser_const_rv mapM_length)
  apply (clarsimp simp: length_msgRegisters)
  apply (simp add: min_def split: if_splits)
  apply (clarsimp simp: word_le_nat_alt)
  apply (simp add: msgMaxLength_def msgLengthBits_def n_msgRegisters_def)
  done

lemma index_msgRegisters_less':
  "n < 4 \<Longrightarrow> index msgRegisters n < 0x12"
  by (simp add: msgRegisters_def fupdate_def Arrays.update_def
                fcp_beta "StrictC'_register_defs")

lemma index_msgRegisters_less:
  "n < 4 \<Longrightarrow> index msgRegisters n <s 0x12"
  "n < 4 \<Longrightarrow> index msgRegisters n < 0x12"
  using index_msgRegisters_less'
  by (simp_all add: word_sless_msb_less)

(* FIXME: move *)
lemma ucast_nat_def':
  "of_nat (unat x) = (ucast :: ('a :: len) word \<Rightarrow> ('b :: len) signed word) x"
  by (simp add: ucast_def word_of_int_nat unat_def)

(* FIXME: move *)
lemma ucast_add:
     "ucast (a + (b :: 'a :: len word)) = ucast a + (ucast b :: ('a signed word))"
  apply (case_tac "len_of TYPE('a) = 1")
   apply (clarsimp simp: ucast_def)
   apply (metis (hide_lams, mono_tags) One_nat_def len_signed plus_word.abs_eq uint_word_arith_bintrs(2) word_ubin.Abs_norm)
  apply (clarsimp simp: ucast_def)
  apply (metis le_refl len_signed plus_word.abs_eq uint_word_arith_bintrs(2) wi_bintr)
  done

(* FIXME: move *)
lemma ucast_minus:
     "ucast (a - (b :: 'a :: len word)) = ucast a - (ucast b :: ('a signed word))"
  apply (insert ucast_add [where a=a and b="-b"])
  apply (metis (hide_lams, no_types) is_num_normalize(10) is_num_normalize(8) is_num_normalize(9) minus_minus ucast_add)
  done

(* FIXME : move *)
lemma scast_ucast_add_one [simp]:
  "scast (ucast (x :: 'a::len word) + (1 :: 'a signed word)) = x + 1"
  apply (subst ucast_1 [symmetric])
  apply (subst ucast_add [symmetric])
  apply clarsimp
  done


lemma getSyscallArg_ccorres_foo:
  "ccorres (\<lambda>a rv. rv = args ! n) ret__unsigned_long_'
         (sysargs_rel args buffer and sysargs_rel_n args buffer n)
         (UNIV \<inter> \<lbrace>unat \<acute>i = n\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = option_to_ptr buffer\<rbrace>) []
    (return ()) (Call getSyscallArg_'proc)"
  apply (rule ccorres_assume_pre)
  apply (subst (asm) sysargs_rel_def)
  apply (subst (asm) getMRs_rel_def)
  apply (subst (asm) pred_conj_def)+
  apply (elim conjE exE)
  apply (cinit lift: i_' ipc_buffer_') 
   apply (fold return_def)
   apply (rule_tac H="do thread \<leftarrow> gets ksCurThread; getMRs thread buffer mi od" in ccorres_defer)
    prefer 2
    apply (rule no_fail_pre, wp no_fail_getMRs)
    apply assumption
   apply (rule ccorres_cond_seq) 
   apply (rule_tac R=\<top> and P="\<lambda>_. n < unat (scast n_msgRegisters :: word32)" in ccorres_cond_both)
     apply (simp add: word_less_nat_alt split: split_if)
    apply (rule ccorres_add_return2)
    apply (rule ccorres_symb_exec_l)
       apply (rule_tac P="\<lambda>s. n < unat (scast n_msgRegisters :: word32) \<and> obj_at' (\<lambda>tcb. tcbContext tcb (State_H.msgRegisters!n) = x!n) (ksCurThread s) s" 
                   and P' = UNIV 
         in ccorres_from_vcg_split_throws)
        apply vcg
       apply (simp add: return_def del: Collect_const)
       apply (rule conseqPre, vcg)
       apply (clarsimp simp: rf_sr_ksCurThread)
       apply (drule (1) obj_at_cslift_tcb)
       apply (clarsimp simp: typ_heap_simps' msgRegisters_scast)
       apply (clarsimp simp: ctcb_relation_def ccontext_relation_def msgRegisters_ccorres)
       apply (subst (asm) msgRegisters_ccorres)
        apply (clarsimp simp: n_msgRegisters_def)
       apply (simp add: n_msgRegisters_def word_less_nat_alt)
       apply (simp add: index_msgRegisters_less unat_less_helper)
      apply wp[1]
     apply (wp getMRs_tcbContext)
    apply simp
   apply (rule ccorres_seq_skip [THEN iffD2])
   apply (rule ccorres_seq_skip [THEN iffD2])
   apply (rule ccorres_add_return2)
   apply (rule ccorres_symb_exec_l)
      apply (rule_tac P="\<lambda>s. user_word_at (x!n) (ptr_val (CTypesDefs.ptr_add ipc_buffer (of_nat n + 1))) s" 
                  and P'=UNIV 
                   in ccorres_from_vcg_throws)
      apply (simp add: return_def split del: split_if)
      apply (rule allI, rule conseqPre, vcg)
      apply (clarsimp split del: split_if)
      apply (rule conjI)
       apply (clarsimp simp: CTypesDefs.ptr_add_def)
       apply (frule (1) user_word_at_cross_over)
        apply simp
       apply (clarsimp simp: mult_ac ucast_nat_def')
      apply (clarsimp simp: CTypesDefs.ptr_add_def)
      apply (frule (1) user_word_at_cross_over)
       apply simp
      apply (clarsimp simp: mult_ac ucast_nat_def)
     apply wp[1]
    apply (rule_tac P="\<exists>b. buffer = Some b" in hoare_gen_asm)
    apply (clarsimp simp: option_to_ptr_def option_to_0_def)
    apply (rule_tac P="\<lambda>s. valid_ipc_buffer_ptr' (ptr_val (Ptr b)) s \<and> i < msgLength mi \<and> 
                           msgLength mi \<le> msgMaxLength \<and> scast n_msgRegisters \<le> i" 
                 in hoare_pre(1))
     apply (wp getMRs_user_word)
    apply clarsimp
   apply simp
  apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def)
  apply (rule conjI, clarsimp simp: unat_of_nat32 word_bits_def)
   apply (drule equalityD2)
   apply clarsimp
   apply (drule use_valid, rule getMRs_length, assumption)
   apply (simp add: n_msgRegisters_def  split: split_if_asm)
  apply (rule conjI)
   apply (clarsimp simp: option_to_ptr_def option_to_0_def
      word_less_nat_alt word_le_nat_alt unat_of_nat32 word_bits_def
      n_msgRegisters_def not_less msgMaxLength_def)
   apply (drule equalityD2)
   apply clarsimp
   apply (drule use_valid, rule getMRs_length)
    apply (simp add: word_le_nat_alt msgMaxLength_def)
   apply (simp split: split_if_asm)
  apply (rule conjI, clarsimp simp: cur_tcb'_def)
  apply clarsimp
  apply (clarsimp simp: bind_def gets_def return_def split_def get_def)  
  done

lemma wordFromMessageInfo_spec:
  defines "mil s \<equiv> message_info_lift \<^bsup>s\<^esup>mi"
  shows "\<forall>s. \<Gamma> \<turnstile> {s} Call wordFromMessageInfo_'proc
                  \<lbrace>\<acute>ret__unsigned_long = (msgLabel_CL (mil s) << 12)
                                      || (msgCapsUnwrapped_CL (mil s) << 9)
                                      || (msgExtraCaps_CL (mil s) << 7)
                                      || msgLength_CL (mil s)\<rbrace>"
  unfolding mil_def
  apply vcg
  apply (simp add: message_info_lift_def mask_shift_simps word_sless_def word_sle_def)
  apply word_bitwise
  done

lemmas wordFromMessageInfo_spec2 = wordFromMessageInfo_spec

lemma wordFromMessageInfo_ccorres [corres]:
  "\<And>mi. ccorres (op =) ret__unsigned_long_' \<top> {s. mi = message_info_to_H (mi_' s)} []
           (return (wordFromMessageInfo mi)) (Call wordFromMessageInfo_'proc)"
  apply (rule ccorres_from_spec_modifies [where P = \<top>, simplified])
     apply (rule wordFromMessageInfo_spec)
    apply (rule wordFromMessageInfo_modifies)
   apply simp
  apply simp
  apply (simp add: return_def wordFromMessageInfo_def Let_def message_info_to_H_def 
    Types_H.msgLengthBits_def Types_H.msgExtraCapBits_def
    Types_H.msgMaxExtraCaps_def shiftL_nat word_bw_assocs word_bw_comms word_bw_lcs)
  done

(* FIXME move *)
lemma unat_register_from_H_range:
  "unat (register_from_H r) < 18"
  by (case_tac r, simp_all add: C_register_defs)

(* FIXME move *)
lemma register_from_H_eq:
  "(r = r') = (register_from_H r = register_from_H r')"
  apply (case_tac r, simp_all add: C_register_defs)
                   apply (case_tac r', simp_all add: C_register_defs)+
  done

lemma setMessageInfo_ccorres:
  "ccorres dc xfdc (tcb_at' thread)
           (UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>) hs
           (setMessageInfo thread mi)
           (\<acute>ret__unsigned_long :== CALL wordFromMessageInfo(mi');;
            CALL setRegister(tcb_ptr_to_ctcb_ptr thread, scast Kernel_C.msgInfoRegister, \<acute>ret__unsigned_long))"
  unfolding setMessageInfo_def
  apply (rule ccorres_guard_imp2)
   apply ctac
     apply simp
     apply (ctac add: setRegister_ccorres)
    apply wp
   apply vcg
  apply (simp add: State_H.msgInfoRegister_def ARMMachineTypes.msgInfoRegister_def
                   Kernel_C.msgInfoRegister_def Kernel_C.R1_def)
  done

end

lemma invocation_eq_use_type:
  "\<lbrakk> value \<equiv> (value' :: 32 signed word);
       unat (scast value' :: word32) < length (enum :: invocation_label list); (scast value' :: word32) \<noteq> 0 \<rbrakk>
     \<Longrightarrow> (label = (scast value)) = (invocation_type label = enum ! unat (scast value' :: word32))"
  apply (fold invocation_type_eq, unfold invocationType_def)
  apply (simp add: maxBound_is_length Let_def toEnum_def
                   nth_eq_iff_index_eq nat_le_Suc_less_imp
            split: split_if)
  apply (intro impI conjI)
   apply (simp add: enum_invocation_label)
  apply (subgoal_tac "InvalidInvocation = enum ! 0")
   apply (erule ssubst, subst nth_eq_iff_index_eq, simp+)
   apply (clarsimp simp add: unat_eq_0)
  apply (simp add: enum_invocation_label)
  done

lemmas all_invocation_label_defs = invocation_label_defs arch_invocation_label_defs

lemmas invocation_eq_use_types
    = all_invocation_label_defs[THEN invocation_eq_use_type, simplified,
                            unfolded enum_invocation_label, simplified]

lemma ccorres_equals_throwError:
  "\<lbrakk> f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \<rbrakk>
     \<Longrightarrow> ccorres_underlying sr Gamm rr xf arr axf P P' hs f c"
  by simp

end