(*
 * Copyright 2016, 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)
 *)

(* Experimental AutoCorres proofs over CRefine: work in progress *)

theory AutoCorresTest
imports (* Frameworks and tactics *)
        AutoCorres_C
        (* import Refine_C last to minimise change to global context *)
        Refine_C
begin

section \<open>Simple test case: handleYield\<close>

autocorres
  [
   skip_heap_abs, skip_word_abs, (* for compatibility *)
   scope = handleYield,
   scope_depth = 0,
   c_locale = kernel_all_substitute,
   no_c_termination
  ] "c/kernel_all.c_pp"

context kernel_m begin

text \<open>Export corres_underlying rules for handleYield's callees.\<close>
thm getCurThread_ccorres
lemma getCurThread_wrapper_corres:
  "corres_underlying {(x, y). cstate_relation x y} True True (\<lambda>ct ct'. tcb_ptr_to_ctcb_ptr ct = ct') invs' (\<lambda>_. True) getCurThread (gets ksCurThread_')"
  by (simp add: getCurThread_def cstate_relation_def Let_def)

thm ccorres_pre_getCurThread
lemma corres_pre_getCurThread_wrapper:
  assumes cc: "\<And>rv rv'. rv' = tcb_ptr_to_ctcb_ptr rv \<Longrightarrow>
                  corres_underlying {(x, y). cstate_relation x y} True True R (P rv) (P' rv) (f rv) (f' rv')"
  shows   "corres_underlying {(x, y). cstate_relation x y} True True R
                  (\<lambda>s. \<forall>rv. ksCurThread s = rv \<longrightarrow> P rv s)
                  (\<lambda>s. \<forall>rv. ksCurThread_' s = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> P' rv s)
                  (getCurThread >>= f) (gets ksCurThread_' >>= f')"
  (* ugly but works -- corres_symb_exec_l doesn't *)
  using cc
  apply (clarsimp simp: corres_underlying_def getCurThread_def)
  apply monad_eq
  apply (clarsimp simp: cstate_relation_def Let_def)
  done

thm tcbSchedDequeue_ccorres
lemma tcbSchedDequeue_wrapper_corres:
  "tcb_ptr_to_ctcb_ptr ct = ct' \<Longrightarrow>
   corres_underlying {(x, y). cstate_relation x y} True True (op=)
     (Invariants_H.valid_queues and valid_queues' and tcb_at' ct and valid_objs') \<top>
     (tcbSchedDequeue ct) (tcbSchedDequeue' ct')"
  apply (rule ccorres_to_corres_no_termination)
   apply (simp add: tcbSchedDequeue'_def)
  apply (clarsimp simp: ccorres_rrel_nat_unit tcbSchedDequeue_ccorres[simplified])
  done

thm tcbSchedAppend_ccorres
lemma tcbSchedAppend_wrapper_corres:
  "tcb_ptr_to_ctcb_ptr ct = ct' \<Longrightarrow>
   corres_underlying {(x, y). cstate_relation x y} True True (op=)
     (Invariants_H.valid_queues and tcb_at' ct and valid_objs') \<top>
     (tcbSchedAppend ct) (tcbSchedAppend' ct')"
  apply (rule ccorres_to_corres_no_termination)
   apply (simp add: tcbSchedAppend'_def)
  apply (clarsimp simp: ccorres_rrel_nat_unit tcbSchedAppend_ccorres[simplified])
  done

thm rescheduleRequired_ccorres
lemma rescheduleRequired_wrapper_corres:
  "corres_underlying {(x, y). cstate_relation x y} True True (op=)
     (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') \<top>
     rescheduleRequired rescheduleRequired'"
  apply (rule ccorres_to_corres_no_termination)
   apply (simp add: rescheduleRequired'_def)
  apply (clarsimp simp: ccorres_rrel_nat_unit rescheduleRequired_ccorres[simplified])
  done

text \<open>
  Proving handleYield_ccorres via handleYield'.
  The handleYield spec has one less getCurThread, so we need to use the fact
  that tcbSchedDequeue does not modify ksCurThread.
\<close>
local_setup \<open>AutoCorresModifiesProofs.new_modifies_rules "c/kernel_all.c_pp"\<close>
thm tcbSchedDequeue'_modifies

text \<open>Existing ccorres proof, for reference\<close>
lemma (* handleYield_ccorres: *)
  "ccorres dc xfdc
       (invs' and ct_active')
       UNIV
       []
       (handleYield)
       (Call handleYield_'proc)"
  apply cinit
   apply (rule ccorres_pre_getCurThread)
   apply (ctac add: tcbSchedDequeue_ccorres)
     apply (ctac  add: tcbSchedAppend_ccorres)
       apply (ctac add: rescheduleRequired_ccorres)
      apply (wp weak_sch_act_wf_lift_linear tcbSchedAppend_valid_objs')
     apply (vcg exspec= tcbSchedAppend_modifies)
    apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues)
   apply (vcg exspec= tcbSchedDequeue_modifies)
  apply (clarsimp simp: tcb_at_invs' invs_valid_objs'
                        valid_objs'_maxPriority valid_objs'_maxDomain)
  apply (auto simp: obj_at'_def st_tcb_at'_def ct_in_state'_def valid_objs'_maxDomain)
  done

lemma reorder_gets:
  "(\<And>x. \<lbrace> \<lambda>s. x = f s \<rbrace> g \<lbrace> \<lambda>_ s. x = f s \<rbrace>) \<Longrightarrow>
   (do x \<leftarrow> gets f;
       g;
       h x od) =
   (do g;
       x \<leftarrow> gets f;
       h x od)"
  by (fastforce simp: bind_def' valid_def gets_def get_def return_def)

text \<open>Now the proof.\<close>
lemma (* handleYield_ccorres: *)
  "ccorres dc xfdc
       (invs' and ct_active')
       UNIV
       []
       (handleYield)
       (Call handleYield_'proc)"
  apply (rule ac_corres_to_ccorres)
    apply (rule kernel_all_substitute.handleYield'_ac_corres)
   apply simp
  apply (simp add: handleYield_def handleYield'_def)

  apply (rule corres_guard_imp)
    (* Show that current thread is unmodified.
     * FIXME: proper way to do this? *)
    apply (subst reorder_gets[symmetric, unfolded K_bind_def])
     using tcbSchedDequeue'_modifies apply (fastforce simp: valid_def)
    apply (subst gets_gets)

    apply (rule corres_pre_getCurThread_wrapper)
    apply (rule corres_split[OF _ tcbSchedDequeue_wrapper_corres])
       apply (rule corres_split[OF _ tcbSchedAppend_wrapper_corres])
          apply (rule rescheduleRequired_wrapper_corres)
         apply (solves simp)
        apply (solves \<open>wp tcbSchedAppend_valid_objs' weak_sch_act_wf_lift_linear | simp\<close>)+
     apply (solves \<open>wp tcbSchedDequeue_invs' tcbSchedDequeue_typ_at'
                       tcbSchedDequeue_valid_queues tcbSchedDequeue_valid_objs'
                       weak_sch_act_wf_lift_linear\<close>)
    apply (solves wp)
   apply (clarsimp simp: invs_valid_objs' invs_queues invs_valid_queues' tcb_at_invs'
                         valid_objs'_maxPriority valid_objs'_maxDomain)
   apply (fastforce simp: obj_at'_def st_tcb_at'_def ct_in_state'_def dest: ct_active_runnable')
  apply fastforce
  done

end


section \<open>Function call testcase: handleFault and handleDoubleFault\<close>

autocorres
  [
   skip_heap_abs, skip_word_abs, (* for compatibility *)
   scope = handleDoubleFault,
   scope_depth = 0,
   c_locale = kernel_all_substitute,
   no_c_termination
  ] "c/kernel_all.c_pp"

context kernel_m begin
local_setup \<open>AutoCorresModifiesProofs.new_modifies_rules "c/kernel_all.c_pp"\<close>

text \<open>Export corres_underlying rules for handleDoubleFault's callees.\<close>
thm setThreadState_ccorres[no_vars]
lemma setThreadState_wrapper_corres:
  "(\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := ts && mask 4\<rparr>, fl)) \<and>
   tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow>
   corres_underlying {(x, y). cstate_relation x y} True True (op=)
     (\<lambda>s. tcb_at' thread s \<and>
       Invariants_H.valid_queues s \<and>
       valid_objs' s \<and>
       valid_tcb_state' st s \<and>
       (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' st) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' st) \<and> sch_act_wf (ksSchedulerAction s) s) \<top>
     (setThreadState st thread) (setThreadState' tptr ts)"
  apply (rule ccorres_to_corres_no_termination)
   apply (simp add: setThreadState'_def)
  apply (clarsimp simp: ccorres_rrel_nat_unit)
  using setThreadState_ccorres
  apply (fastforce simp: ccorres_underlying_def Ball_def)
  done

text \<open>Extra corres_underlying rules.\<close>
lemma corres_gen_asm':
  "\<lbrakk> corres_underlying sr nf nf' r Q P' f g; \<And>s s'. \<lbrakk> (s, s') \<in> sr; P s; P' s' \<rbrakk> \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow>
   corres_underlying sr nf nf' r P P' f g"
  by (fastforce simp: corres_underlying_def)

lemma corres_add_noop_rhs2:
  "corres_underlying sr nf nf' r P P' f (do _ \<leftarrow> g; return () od)
      \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
  by simp

(* Use termination (nf=True) to avoid exs_valid *)
lemma corres_noop2_no_exs:
  assumes x: "\<And>s. P s  \<Longrightarrow> \<lbrace>op = s\<rbrace> f \<lbrace>\<lambda>r. op = s\<rbrace> \<and> empty_fail f"
  assumes y: "\<And>s. P' s \<Longrightarrow> \<lbrace>op = s\<rbrace> g \<lbrace>\<lambda>r. op = s\<rbrace>"
  assumes z: "nf' \<Longrightarrow> no_fail P f" "no_fail P' g"
  shows      "corres_underlying sr True nf' dc P P' f g"
  apply (clarsimp simp: corres_underlying_def)
  apply (rule conjI)
   apply (drule x, drule y)
   apply (clarsimp simp: valid_def empty_fail_def Ball_def Bex_def)
   apply fast
  apply (insert z)
  apply (clarsimp simp: no_fail_def)
  done

lemma corres_symb_exec_l_no_exs:
  assumes z: "\<And>rv. corres_underlying sr True nf' r (Q rv) P' (x rv) y"
  assumes x: "\<And>s. P s \<Longrightarrow> \<lbrace>op = s\<rbrace> m \<lbrace>\<lambda>r. op = s\<rbrace> \<and> empty_fail m"
  assumes y: "\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>"
  assumes nf: "nf' \<Longrightarrow> no_fail P m"
  shows      "corres_underlying sr True nf' r P P' (m >>= (\<lambda>rv. x rv)) y"
  apply (rule corres_guard_imp)
    apply (subst gets_bind_ign[symmetric], rule corres_split)
       apply (rule z)
      apply (rule corres_noop2_no_exs)
         apply (erule x)
        apply (rule gets_wp)
       apply (erule nf)
      apply (rule non_fail_gets)
     apply (rule y)
    apply (rule gets_wp)
   apply simp+
  done

text \<open>Existing ccorres proof, for reference\<close>
lemma (* handleDoubleFault_ccorres: *)
  "ccorres dc xfdc (invs' and  tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and
        sch_act_not tptr and (\<lambda>s. \<forall>p. tptr \<notin> set (ksReadyQueues s p)))
      (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr tptr})
      [] (handleDoubleFault tptr ex1 ex2)
         (Call handleDoubleFault_'proc)"
  apply (cinit lift: tptr_')
   apply (subst ccorres_seq_skip'[symmetric])
   apply (ctac (no_vcg))
    apply (rule ccorres_symb_exec_l)
       apply (rule ccorres_return_Skip)
      apply (wp asUser_inv getRestartPC_inv)
    apply (rule empty_fail_asUser)
    apply (simp add: getRestartPC_def)
   apply wp
  apply clarsimp
  apply (simp add: ThreadState_Inactive_def)
  apply (fastforce simp: valid_tcb_state'_def)
  done

text \<open>New proof of handleDoubleFault\<close>
lemma (* handleDoubleFault_ccorres: *)
  "ccorres dc xfdc (invs' and tcb_at' tptr and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and
        sch_act_not tptr and (\<lambda>s. \<forall>p. tptr \<notin> set (ksReadyQueues s p)))
      (UNIV \<inter> {s. ex1_' s = ex1' \<and> tptr_' s = tcb_ptr_to_ctcb_ptr tptr})
      [] (handleDoubleFault tptr ex1 ex2)
         (Call handleDoubleFault_'proc)"
  apply (rule ac_corres_to_ccorres[where R="op="])
    apply (rule handleDoubleFault'_ac_corres)
   apply (simp add: pred_conj_def)
  apply (unfold handleDoubleFault_def handleDoubleFault'_def)
  apply (simp only: K_bind_def) -- "normalise"
  apply (rule corres_add_noop_rhs2) -- "split out extra haskell code"
  apply (rule corres_split')
     (* call setThreadState *)
     apply (rule corres_gen_asm')
      apply (rule setThreadState_wrapper_corres)
      apply (simp add: ThreadState_Inactive_def)
     apply (fastforce simp: valid_tcb_state'_def ThreadState_Inactive_def)
    (* extra haskell code *)
    apply simp
    apply (rule corres_symb_exec_l_no_exs)
       apply simp
      apply (rule conjI)
       apply (wp asUser_inv getRestartPC_inv)
      apply (wp empty_fail_asUser)[1]
     apply (rule hoare_TrueI)
    apply (simp add: getRestartPC_def)
    apply wp
   apply simp
  apply (rule hoare_TrueI)
  done

end

autocorres
  [
   skip_heap_abs, skip_word_abs, (* for compatibility *)
   scope = handleFault,
   scope_depth = 0,
   c_locale = kernel_all_substitute,
   no_c_termination
  ] "c/kernel_all.c_pp"

(* Prove and store modifies rules. *)
context kernel_m begin
local_setup \<open>AutoCorresModifiesProofs.new_modifies_rules "c/kernel_all.c_pp"\<close>

(* TODO: proof for handleFault' *)
thm handleFault'_def
thm handleFault_ccorres

end




section \<open>Experiment: translating clzl\<close>
text \<open>
  __builtin_clzl is defined using guarded_spec_body,
  which is a bit hard to translate generically.
  This is an experiment to translate clzl manually.
\<close>
context kernel_all_substitute begin

thm kernel_m.clzl_spec clzl_body_def

definition l1_clzl' :: "nat \<Rightarrow> (globals myvars, unit + unit) nondet_monad" where
  "l1_clzl' rec_measure' \<equiv>
     L1_spec ({(s', t). (\<forall>s. s' \<in> \<lbrace>s. \<^bsup>s\<^esup>x \<noteq> 0\<rbrace> \<longrightarrow> t \<in> \<lbrace>\<acute>ret__long = of_nat (word_clz \<^bsup>s\<^esup>x)\<rbrace>) \<and>
                          (\<exists>s. s' \<in> \<lbrace>s. \<^bsup>s\<^esup>x \<noteq> 0\<rbrace>)} \<inter> {(s, t). t may_not_modify_globals s})"

lemma l1_clzl'_corres:
  "L1corres ct \<Gamma> (l1_clzl' rec_measure') (Call clzl_'proc)"
  apply (unfold l1_clzl'_def)
  apply (rule L1corres_Call)
   apply (rule clzl_impl)
  apply (unfold clzl_body_def)
  apply (rule L1corres_guarded_spec)
  done

definition l2_clzl' :: "nat \<Rightarrow> 32 word \<Rightarrow> (globals, unit + 32 signed word) nondet_monad" where
  "l2_clzl' rec_measure' x \<equiv>
     L2_seq (L2_guard (\<lambda>_. x \<noteq> 0))
       (\<lambda>_. L2_gets (\<lambda>_. of_nat (word_clz x)) [''ret''])"

lemma l2_clzl'_corres:
  "L2corres globals ret__long_' (\<lambda>_. ()) (\<lambda>s. x_' s = x) (l2_clzl' rec_measure' x) (l1_clzl' rec_measure')"
  apply (unfold l2_clzl'_def l1_clzl'_def)
  (* TODO: how to automate this? *)
  apply (monad_eq simp: L1_defs L2_defs L2corres_def corresXF_def meq_def)
  apply (subst myvars.splits)
  apply simp
  done

definition clzl' :: "32 word \<Rightarrow> (globals, 32 signed word) nondet_monad" where
  "clzl' x \<equiv> do guard (\<lambda>_. x \<noteq> 0);
                return (of_nat (word_clz x)) od"

lemma clzl'_TScorres:
  "L2_call (l2_clzl' rec_measure' x) = liftE (clzl' x)"
  apply (unfold l2_clzl'_def clzl'_def)
  apply (tactic {* simp_tac (@{context} addsimps
      (#lift_rules (the (Monad_Types.get_monad_type "nondet" (Context.Proof @{context})))
       |> Thmtab.dest |> map fst)) 1 *})
  done

lemma clzl'_ac_corres: "ac_corres globals ct \<Gamma> ret__long_' (\<lambda>s. x_' s = x) (liftE (clzl' x)) (Call clzl_'proc)"
  apply (rule ac_corres_chain[OF _ _ L2Tcorres_id corresTA_trivial, simplified o_def, simplified])
    apply (rule l1_clzl'_corres)
   apply (rule l2_clzl'_corres)
  apply (rule clzl'_TScorres)
  done
end

text \<open>Add our manual translation of clzl into the AutoCorres function info.\<close>
ML \<open>
fun phasetab_merge_with merge (tab1, tab2) =
  sort_distinct FunctionInfo.phase_ord
      (FunctionInfo.Phasetab.keys tab1 @ FunctionInfo.Phasetab.keys tab2)
  |> map (fn k => (k, case (FunctionInfo.Phasetab.lookup tab1 k, FunctionInfo.Phasetab.lookup tab2 k) of
                          (SOME x1, SOME x2) => merge (x1, x2)
                        | (SOME x1, NONE) => x1
                        | (NONE, SOME x2) => x2
                        (* (NONE, NONE) impossible *)))
  |> FunctionInfo.Phasetab.make;
\<close>
setup {*
fn thy =>
let val clzl_cp = {
      name = "clzl",
      invented_body = false,
      is_simpl_wrapper = false,
      callees = Symset.empty,
      rec_callees = Symset.empty,
      phase = FunctionInfo.CP,
      args = [("x", @{typ "32 word"})],
      return_type = @{typ "32 signed word"},
      const = @{term "clzl_'proc"},
      raw_const = @{term "clzl_'proc"},
      definition = @{thm kernel_all_substitute.clzl_body_def},
      mono_thm = NONE,
      corres_thm = @{thm TrueI}
    }: FunctionInfo.function_info;
    val clzl_l1 = clzl_cp
      |> FunctionInfo.function_info_upd_phase FunctionInfo.L1
      |> FunctionInfo.function_info_upd_const @{term "kernel_all_substitute.l1_clzl'"}
      |> FunctionInfo.function_info_upd_definition @{thm kernel_all_substitute.l1_clzl'_def}
      |> FunctionInfo.function_info_upd_corres_thm @{thm "kernel_all_substitute.l1_clzl'_corres"};
    val clzl_l2 = clzl_l1
      |> FunctionInfo.function_info_upd_phase FunctionInfo.L2
      |> FunctionInfo.function_info_upd_const @{term "kernel_all_substitute.l2_clzl'"}
      |> FunctionInfo.function_info_upd_definition @{thm kernel_all_substitute.l2_clzl'_def}
      |> FunctionInfo.function_info_upd_corres_thm @{thm "kernel_all_substitute.l2_clzl'_corres"};
    val clzl_ts = clzl_l2
      |> FunctionInfo.function_info_upd_phase FunctionInfo.TS
      |> FunctionInfo.function_info_upd_const @{term "kernel_all_substitute.clzl'"}
      |> FunctionInfo.function_info_upd_definition @{thm kernel_all_substitute.clzl'_def}
      |> FunctionInfo.function_info_upd_corres_thm @{thm "kernel_all_substitute.clzl'_TScorres"};
    val clzl_info = FunctionInfo.Phasetab.make
          (map (fn info => (#phase info, Symtab.make [("clzl", info)]))
               [clzl_cp, clzl_l1, clzl_l2, clzl_ts]);
    val file = "c/kernel_all.c_pp";
    val fn_info = the (Symtab.lookup (AutoCorresFunctionInfo.get thy) file);
    val fn_info' = phasetab_merge_with (Symtab.merge (K false)) (fn_info, clzl_info);
in
  thy
  |> AutoCorresFunctionInfo.map (Symtab.update (file, fn_info'))
end
*}

text \<open>Now AutoCorres will use our specification in calls to clzl.\<close>
autocorres
  [
   skip_heap_abs, skip_word_abs, (* for compatibility *)
   scope = chooseThread,
   scope_depth = 0,
   c_locale = kernel_all_substitute,
   no_c_termination
  ] "c/kernel_all.c_pp"

context kernel_m begin
thm clzl'_def
thm chooseThread'_def
end



subsection \<open>Test recursion + call to previously translated (cap_get_capType)\<close>
autocorres
  [
   skip_heap_abs, skip_word_abs, ts_rules = nondet, (* for compatibility *)
   scope = cap_get_capType,
   scope_depth = 0,
   c_locale = kernel_all_substitute
  ] "c/kernel_all.c_pp"

thm kernel_all_substitute.cap_get_capType'_def
    kernel_all_substitute.cap_get_capType_body_def

autocorres
  [
   skip_heap_abs, skip_word_abs, ts_rules = nondet, (* for compatibility *)
   scope = cteDelete finaliseSlot reduceZombie,
   scope_depth = 0,
   c_locale = kernel_all_substitute
  ] "c/kernel_all.c_pp"

context kernel_m begin
thm cteDelete'.simps finaliseSlot'.simps reduceZombie'.simps
end

text \<open>Test call to recursive function group\<close>
autocorres
  [
   skip_heap_abs, skip_word_abs, ts_rules = nondet, (* for compatibility *)
   scope = cteRevoke,
   scope_depth = 0,
   c_locale = kernel_all_substitute
  ] "c/kernel_all.c_pp"

context kernel_m begin
thm cteRevoke'_def
end



subsection \<open>Experiment with proving bitfield specs\<close>

text \<open>
  Here we translate some bitfield functions, then separately prove that
  the translated functions satisfy the bitfield_gen specs.
\<close>
autocorres
  [
   skip_heap_abs, skip_word_abs, ts_rules = nondet, (* for compatibility *)
   scope = cap_capType_equals
     cap_cnode_cap_get_capCNodePtr
     cap_cnode_cap_get_capCNodeGuard
     cap_cnode_cap_get_capCNodeRadix,
   scope_depth = 0,
   c_locale = kernel_all_substitute
  ] "c/kernel_all.c_pp"

lemma of_bl_from_cond:
  "(if C then 1 else 0) = of_bl [C]"
  by (simp add: word_1_bl)
lemma of_bl_cond:
  "(if C then of_bl [A] else of_bl [B]) = of_bl [if C then A else B]"
  by (rule if_f)

context kernel_m begin
lemma "\<lbrace>\<lambda>_. cap_get_tag cap = scast cap_cnode_cap\<rbrace>
         cap_cnode_cap_get_capCNodePtr' cap
       \<lbrace>\<lambda>r _. r = capCNodePtr_CL (cap_cnode_cap_lift cap)\<rbrace>!"
  apply (unfold cap_cnode_cap_get_capCNodePtr'_def)
  apply wp
  apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values shiftr_over_and_dist)
  done

lemma "\<lbrace>\<lambda>_. cap_get_tag cap = scast cap_cnode_cap\<rbrace>
         cap_cnode_cap_get_capCNodeGuard' cap
       \<lbrace>\<lambda>r _. r = capCNodeGuard_CL (cap_cnode_cap_lift cap)\<rbrace>!"
  apply (unfold cap_cnode_cap_get_capCNodeGuard'_def)
  apply wp
  apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values shiftr_over_and_dist)
  done

lemma "\<lbrace>\<lambda>_. cap_get_tag cap = scast cap_cnode_cap\<rbrace>
         cap_cnode_cap_get_capCNodeRadix' cap
       \<lbrace>\<lambda>r _. r = capCNodeRadix_CL (cap_cnode_cap_lift cap)\<rbrace>!"
  apply (unfold cap_cnode_cap_get_capCNodeRadix'_def)
  apply wp
  apply (simp add: cap_get_tag_def cap_cnode_cap_lift_def cap_lift_def cap_tag_values shiftr_over_and_dist)
  done

end


subsection \<open>Experiment with transferring bitfield specs\<close>

text \<open>
  For wrapped bitfield functions, the @{term hoarep} triples for them can be transferred
  to @{term valid} triples.
\<close>
context kernel_m begin

thm cap_zombie_cap_get_capZombiePtr_spec
lemma cap_zombie_cap_get_capZombiePtr'_spec:
  "\<lbrace>\<lambda>s. s = s0 \<and> cap_get_tag cap = scast cap_zombie_cap \<and> get_capZombieBits_CL (cap_zombie_cap_lift cap) < 0x1F\<rbrace>
     cap_zombie_cap_get_capZombiePtr' cap
   \<lbrace>\<lambda>r s. s = s0 \<and> r = get_capZombiePtr_CL (cap_zombie_cap_lift cap)\<rbrace>"
  (* setup *)
  apply (rule hoare_weaken_pre)
   apply (rule hoare_strengthen_post)
    (* generic transfer operation *)
    thm autocorres_transfer_spec_no_modifies[OF
          cap_zombie_cap_get_capZombiePtr'_def cap_zombie_cap_get_capZombiePtr_spec]
    apply (rule autocorres_transfer_spec_no_modifies[OF
                  cap_zombie_cap_get_capZombiePtr'_def cap_zombie_cap_get_capZombiePtr_spec _ refl,
                  where cs="undefined\<lparr>globals := s0, cap_' := cap\<rparr>"])
                        (* the standard tactics can't invent a suitable cs automatically *)
      apply (rule cap_zombie_cap_get_capZombiePtr_modifies)
     (* prove sanity conditions on local variables and preconds *)
     apply auto
  done

thm cap_zombie_cap_get_capZombieType_spec
lemma cap_zombie_cap_get_capZombieType'_spec:
  "\<lbrace>\<lambda>s. s = s0 \<and> cap_get_tag cap = scast cap_zombie_cap \<rbrace>
     cap_zombie_cap_get_capZombieType' cap
   \<lbrace>\<lambda>r s. s = s0 \<and> r = capZombieType_CL (cap_zombie_cap_lift cap)\<rbrace>"
  apply (rule hoare_weaken_pre)
   apply (rule hoare_strengthen_post)
    thm autocorres_transfer_spec_no_modifies[OF
          cap_zombie_cap_get_capZombieType'_def cap_zombie_cap_get_capZombieType_spec]
    apply (rule autocorres_transfer_spec_no_modifies[OF
                  cap_zombie_cap_get_capZombieType'_def cap_zombie_cap_get_capZombieType_spec _ refl,
                  where cs="undefined\<lparr>globals := s0, cap_' := cap\<rparr>"])
      apply (rule cap_zombie_cap_get_capZombieType_modifies)
     apply auto
  done

text \<open>There are some extra complications when transferring bitfield update specs\<close>
thm cap_zombie_cap_set_capZombieNumber_spec (* extra quantified var; precond talks about initial state *)
lemma cap_zombie_cap_set_capZombieNumber'_spec:
  "\<lbrace>\<lambda>s. s = s0 \<and> ccap_relation cap' cap \<and> isZombie cap' \<and> capAligned cap' \<and> unat n \<le> zombieCTEs (capZombieType cap')\<rbrace>
     cap_zombie_cap_set_capZombieNumber' cap n
   \<lbrace>\<lambda>r s. s = s0 \<and> ccap_relation (capZombieNumber_update (\<lambda>_. unat n) cap') r\<rbrace>"
  apply (rule hoare_weaken_pre)
   apply (rule hoare_strengthen_post)
    (* All_to_all' drops the extra quantifier. (rule_format would remove both) *)
    thm autocorres_transfer_spec_no_modifies[OF
          cap_zombie_cap_set_capZombieNumber'_def cap_zombie_cap_set_capZombieNumber_spec[THEN All_to_all']]
    apply (rule autocorres_transfer_spec_no_modifies[OF
                  cap_zombie_cap_set_capZombieNumber'_def cap_zombie_cap_set_capZombieNumber_spec[THEN All_to_all'],
                  where cs="undefined\<lparr>globals := s0, cap_' := cap, n_' := n\<rparr>"])
      apply (rule cap_zombie_cap_set_capZombieNumber_modifies)
     (* swap initial state var to allow unification *)
     apply (rule collect_unlift)
    apply auto
  done

thm cap_capType_equals_spec
lemma cap_capType_equals'_spec:
  "\<lbrace>\<lambda>s. s = s0 \<rbrace>
     AC_call_L1 (\<lambda>s. cap_' s = cap \<and> cap_type_tag_' s = cap_type_tag) globals ret__int_'
       (L1_call_simpl check_termination \<Gamma> cap_capType_equals_'proc)
   \<lbrace>\<lambda>r s. s = s0 \<and> r = of_bl [cap_get_tag cap = cap_type_tag]\<rbrace>"
  apply (rule hoare_weaken_pre)
   apply (rule hoare_strengthen_post)
    thm autocorres_transfer_spec_no_modifies[OF reflexive cap_capType_equals_spec]
    apply (rule autocorres_transfer_spec_no_modifies[
                  OF reflexive cap_capType_equals_spec,
                  where cs="undefined\<lparr>globals := s0, cap_' := cap, cap_type_tag_' := cap_type_tag\<rparr>"])
      apply (rule cap_capType_equals_modifies)
     apply auto
  done

(* TODO: any other types of bitfield_gen functions? *)

end



context kernel_m begin
text \<open>Termination proofs for use with @{thm ccorres_to_corres_with_termination}. Currently unused.\<close>

lemma cap_get_capType_terminates:
  "\<Gamma> \<turnstile> Call cap_get_capType_'proc \<down> Normal s"
  apply (tactic \<open>ALLGOALS (terminates_trivial_tac @{context})\<close>;
         fail)
  done

lemma thread_state_get_tcbQueued_terminates:
  "\<Gamma> \<turnstile> Call thread_state_get_tcbQueued_'proc \<down> Normal s"
  apply (tactic \<open>ALLGOALS (terminates_trivial_tac @{context})\<close>;
         fail)
  done

lemma thread_state_ptr_set_tcbQueued_terminates:
  "\<Gamma> \<turnstile> Call thread_state_ptr_set_tcbQueued_'proc \<down> Normal s"
  apply (tactic \<open>ALLGOALS (terminates_trivial_tac @{context})\<close>;
         fail)
  done

lemma ready_queues_index_terminates:
  "\<Gamma> \<turnstile> Call ready_queues_index_'proc \<down> Normal s"
  apply (tactic \<open>ALLGOALS (terminates_trivial_tac @{context})\<close>;
         fail)
  done

lemma prio_to_l1index_terminates:
  "\<Gamma> \<turnstile> Call prio_to_l1index_'proc \<down> Normal s"
  apply (tactic \<open>ALLGOALS (terminates_trivial_tac @{context})\<close>;
         fail)
  done

lemma removeFromBitmap_terminates:
  "\<Gamma> \<turnstile> Call removeFromBitmap_'proc \<down> Normal s"
  apply (tactic \<open>ALLGOALS (terminates_trivial_tac @{context})\<close>;
         rule prio_to_l1index_terminates)
  done

lemma addToBitmap_terminates:
  "\<Gamma> \<turnstile> Call addToBitmap_'proc \<down> Normal s"
  apply (tactic \<open>ALLGOALS (terminates_trivial_tac @{context})\<close>;
         rule prio_to_l1index_terminates)
  done

lemma tcbSchedDequeue_terminates:
   "\<Gamma> \<turnstile> Call tcbSchedDequeue_'proc \<down> Normal s"
  apply (tactic \<open>ALLGOALS (terminates_trivial_tac @{context})\<close>;
         rule thread_state_get_tcbQueued_terminates
              thread_state_ptr_set_tcbQueued_terminates
              ready_queues_index_terminates
              removeFromBitmap_terminates)
  done

lemma tcbSchedAppend_terminates:
   "\<Gamma> \<turnstile> Call tcbSchedAppend_'proc \<down> Normal s"
  apply (tactic \<open>ALLGOALS (terminates_trivial_tac @{context})\<close>;
         rule thread_state_get_tcbQueued_terminates
              thread_state_ptr_set_tcbQueued_terminates
              ready_queues_index_terminates
              addToBitmap_terminates)
  done

lemma tcbSchedEnqueue_terminates:
   "\<Gamma> \<turnstile> Call tcbSchedEnqueue_'proc \<down> Normal s"
  apply (tactic \<open>ALLGOALS (terminates_trivial_tac @{context})\<close>;
         rule thread_state_get_tcbQueued_terminates
              thread_state_ptr_set_tcbQueued_terminates
              ready_queues_index_terminates
              addToBitmap_terminates)
  done

lemma rescheduleRequired_terminates:
   "\<Gamma> \<turnstile> Call rescheduleRequired_'proc \<down> Normal s"
  apply (tactic \<open>ALLGOALS (terminates_trivial_tac @{context})\<close>;
         rule tcbSchedEnqueue_terminates)
  done

end

end