AArch64 Information Flow: initial setup #944
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,352 @@ | ||
| (* | ||
| * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) | ||
| * | ||
| * SPDX-License-Identifier: GPL-2.0-only | ||
| *) | ||
|
|
||
| text \<open> | ||
| This file sets up a kernel automaton, ADT_A_if, which is | ||
| slightly different from ADT_A. | ||
| It then setups a big step framework to transfrom this automaton in the | ||
| big step automaton on which the infoflow theorem will be proved | ||
| \<close> | ||
|
|
||
| theory ArchADT_IF | ||
| imports ADT_IF | ||
| begin | ||
|
|
||
| context Arch begin global_naming AARCH64 | ||
|
|
||
| named_theorems ADT_IF_assms | ||
|
|
||
| (* FIXME: clagged from AInvs.do_user_op_invs *) | ||
| lemma do_user_op_if_invs[ADT_IF_assms]: | ||
| "\<lbrace>invs and ct_running\<rbrace> | ||
| do_user_op_if f tc | ||
| \<lbrace>\<lambda>_. invs and ct_running\<rbrace>" | ||
| apply (simp add: do_user_op_if_def split_def) | ||
| apply (wp do_machine_op_ct_in_state device_update_invs | wp (once) dmo_invs | simp)+ | ||
| apply (clarsimp simp: user_mem_def user_memory_update_def simpler_modify_def restrict_map_def | ||
| invs_def cur_tcb_def ptable_rights_s_def ptable_lift_s_def) | ||
| apply (frule ptable_rights_imp_frame) | ||
| apply fastforce | ||
| apply simp | ||
| apply (clarsimp simp: valid_state_def device_frame_in_device_region) | ||
| done | ||
|
|
||
| crunch do_user_op_if | ||
| for domain_sep_inv[ADT_IF_assms, wp]: "domain_sep_inv irqs st" | ||
| (ignore: user_memory_update) | ||
|
|
||
| crunch do_user_op_if | ||
| for valid_sched[ADT_IF_assms, wp]: "valid_sched" | ||
| (ignore: user_memory_update) | ||
|
|
||
| crunch do_user_op_if | ||
| for irq_masks[ADT_IF_assms, wp]: "\<lambda>s. P (irq_masks_of_state s)" | ||
| (ignore: user_memory_update wp: dmo_wp no_irq) | ||
|
|
||
| crunch do_user_op_if | ||
| for valid_list[ADT_IF_assms, wp]: "valid_list" | ||
| (ignore: user_memory_update) | ||
|
|
||
| lemma do_user_op_if_scheduler_action[ADT_IF_assms, wp]: | ||
| "do_user_op_if f tc \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace>" | ||
| by (simp add: do_user_op_if_def | wp | wpc)+ | ||
|
|
||
| lemma do_user_op_silc_inv[ADT_IF_assms, wp]: | ||
| "do_user_op_if f tc \<lbrace>silc_inv aag st\<rbrace>" | ||
| apply (simp add: do_user_op_if_def) | ||
| apply (wp | wpc | simp)+ | ||
| done | ||
|
|
||
| lemma do_user_op_pas_refined[ADT_IF_assms, wp]: | ||
| "do_user_op_if f tc \<lbrace>pas_refined aag\<rbrace>" | ||
| apply (simp add: do_user_op_if_def) | ||
| apply (wp | wpc | simp)+ | ||
| done | ||
|
|
||
| crunch do_user_op_if | ||
| for cur_thread[ADT_IF_assms, wp]: "\<lambda>s. P (cur_thread s)" | ||
| and cur_domain[ADT_IF_assms, wp]: "\<lambda>s. P (cur_domain s)" | ||
| and idle_thread[ADT_IF_assms, wp]: "\<lambda>s. P (idle_thread s)" | ||
| and domain_fields[ADT_IF_assms, wp]: "domain_fields P" | ||
| (ignore: user_memory_update) | ||
|
|
||
| lemma do_use_op_guarded_pas_domain[ADT_IF_assms, wp]: | ||
| "do_user_op_if f tc \<lbrace>guarded_pas_domain aag\<rbrace>" | ||
| by (rule guarded_pas_domain_lift; wp) | ||
|
|
||
| lemma tcb_arch_ref_tcb_context_set[ADT_IF_assms, simp]: | ||
| "tcb_arch_ref (tcb_arch_update (arch_tcb_context_set tc) tcb) = tcb_arch_ref tcb" | ||
| by (simp add: tcb_arch_ref_def arch_tcb_context_set_def) | ||
|
|
||
| crunch arch_activate_idle_thread, arch_switch_to_thread | ||
| for cur_thread[ADT_IF_assms, wp]: "\<lambda>s. P (cur_thread s)" | ||
|
|
||
| lemma arch_activate_idle_thread_scheduler_action[ADT_IF_assms, wp]: | ||
| "arch_activate_idle_thread t \<lbrace>\<lambda>s :: det_state. P (scheduler_action s)\<rbrace>" | ||
| by (wpsimp simp: arch_activate_idle_thread_def) | ||
|
|
||
| crunch handle_vm_fault, handle_hypervisor_fault | ||
| for domain_fields[ADT_IF_assms, wp]: "domain_fields P" | ||
|
|
||
| lemma arch_perform_invocation_noErr[ADT_IF_assms, wp]: | ||
| "\<lbrace>\<top>\<rbrace> arch_perform_invocation a -, \<lbrace>Q\<rbrace>" | ||
| by (wpsimp simp: arch_perform_invocation_def) | ||
|
|
||
| lemma arch_invoke_irq_control_noErr[ADT_IF_assms, wp]: | ||
| "\<lbrace>\<top>\<rbrace> arch_invoke_irq_control a -, \<lbrace>Q\<rbrace>" | ||
| by (cases a; wpsimp) | ||
|
|
||
| lemma getActiveIRQ_None[ADT_IF_assms]: | ||
| "(None,s') \<in> fst (do_machine_op (getActiveIRQ in_kernel) s) \<Longrightarrow> | ||
| irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = None" | ||
| apply (erule use_valid) | ||
| apply (wp dmo_getActiveIRQ_wp) | ||
| by simp | ||
|
|
||
| lemma getActiveIRQ_Some[ADT_IF_assms]: | ||
| "(Some i, s') \<in> fst (do_machine_op (getActiveIRQ in_kernel) s) | ||
| \<Longrightarrow> irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = Some i" | ||
| apply (erule use_valid) | ||
| apply (wp dmo_getActiveIRQ_wp) | ||
| by simp | ||
|
|
||
| lemma idle_equiv_as_globals_equiv: | ||
| "arm_us_global_vspace (arch_state s) \<noteq> idle_thread s | ||
| \<Longrightarrow> idle_equiv st s = | ||
| globals_equiv (st\<lparr>arch_state := arch_state s, machine_state := machine_state s, | ||
| kheap:= (kheap st)(arm_us_global_vspace (arch_state s) := | ||
| kheap s (arm_us_global_vspace (arch_state s))), | ||
| cur_thread := cur_thread s\<rparr>) s" | ||
| by (clarsimp simp: idle_equiv_def globals_equiv_def tcb_at_def2) | ||
|
|
||
| lemma idle_globals_lift: | ||
| assumes g: "\<And>st. \<lbrace>globals_equiv st and P\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" | ||
| assumes i: "\<And>s. P s \<Longrightarrow> arm_us_global_vspace (arch_state s) \<noteq> idle_thread s" | ||
| shows "\<lbrace>idle_equiv st and P\<rbrace> f \<lbrace>\<lambda>_. idle_equiv st\<rbrace>" | ||
| apply (clarsimp simp: valid_def) | ||
| apply (subgoal_tac "arm_us_global_vspace (arch_state s) \<noteq> idle_thread s") | ||
| apply (subst (asm) idle_equiv_as_globals_equiv,simp+) | ||
| apply (frule use_valid[OF _ g]) | ||
| apply simp+ | ||
| apply (clarsimp simp: idle_equiv_def globals_equiv_def tcb_at_def2) | ||
| apply (erule i) | ||
| done | ||
|
|
||
| lemma idle_equiv_as_globals_equiv_scheduler: | ||
| "arm_us_global_vspace (arch_state s) \<noteq> idle_thread s | ||
| \<Longrightarrow> idle_equiv st s = | ||
| globals_equiv_scheduler (st\<lparr>arch_state := arch_state s, machine_state := machine_state s, | ||
| kheap:= (kheap st)(arm_us_global_vspace (arch_state s) := | ||
| kheap s (arm_us_global_vspace (arch_state s)))\<rparr>) s" | ||
| by (clarsimp simp: idle_equiv_def tcb_at_def2 globals_equiv_scheduler_def | ||
| arch_globals_equiv_scheduler_def) | ||
|
|
||
| lemma idle_globals_lift_scheduler: | ||
| assumes g: "\<And>st. \<lbrace>globals_equiv_scheduler st and P\<rbrace> f \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>" | ||
| assumes i: "\<And>s. P s \<Longrightarrow> arm_us_global_vspace (arch_state s) \<noteq> idle_thread s" | ||
| shows "\<lbrace>idle_equiv st and P\<rbrace> f \<lbrace>\<lambda>_. idle_equiv st\<rbrace>" | ||
| apply (clarsimp simp: valid_def) | ||
| apply (subgoal_tac "arm_us_global_vspace (arch_state s) \<noteq> idle_thread s") | ||
| apply (subst (asm) idle_equiv_as_globals_equiv_scheduler,simp+) | ||
| apply (frule use_valid[OF _ g]) | ||
| apply simp+ | ||
| apply (clarsimp simp: idle_equiv_def globals_equiv_scheduler_def tcb_at_def2) | ||
| apply (erule i) | ||
| done | ||
|
|
||
| lemma invs_pt_not_idle_thread[intro]: | ||
| "invs s \<Longrightarrow> arm_us_global_vspace (arch_state s) \<noteq> idle_thread s" | ||
| by (fastforce dest: valid_global_arch_objs_pt_at | ||
| simp: invs_def valid_state_def valid_arch_state_def valid_global_objs_def | ||
| obj_at_def valid_idle_def pred_tcb_at_def empty_table_def) | ||
|
|
||
| lemma kernel_entry_if_idle_equiv[ADT_IF_assms]: | ||
| "\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and idle_equiv st | ||
| and (\<lambda>s. ct_idle s \<longrightarrow> tc = idle_context s)\<rbrace> | ||
| kernel_entry_if e tc | ||
| \<lbrace>\<lambda>_. idle_equiv st\<rbrace>" | ||
| apply (rule hoare_pre) | ||
| apply (rule idle_globals_lift) | ||
| apply (wp kernel_entry_if_globals_equiv) | ||
| apply force | ||
| apply (fastforce intro!: invs_pt_not_idle_thread)+ | ||
| done | ||
|
|
||
| lemmas handle_preemption_idle_equiv[ADT_IF_assms, wp] = | ||
| idle_globals_lift[OF handle_preemption_globals_equiv invs_pt_not_idle_thread, simplified] | ||
|
|
||
| lemmas schedule_if_idle_equiv[ADT_IF_assms, wp] = | ||
| idle_globals_lift_scheduler[OF schedule_if_globals_equiv_scheduler invs_pt_not_idle_thread, simplified] | ||
|
|
||
| lemma do_user_op_if_idle_equiv[ADT_IF_assms, wp]: | ||
| "\<lbrace>idle_equiv st and invs\<rbrace> | ||
| do_user_op_if uop tc | ||
| \<lbrace>\<lambda>_. idle_equiv st\<rbrace>" | ||
| unfolding do_user_op_if_def | ||
| by (wpsimp wp: dmo_user_memory_update_idle_equiv dmo_device_memory_update_idle_equiv) | ||
|
|
||
| lemma kernel_entry_if_valid_vspace_objs_if[ADT_IF_assms, wp]: | ||
| "\<lbrace>valid_vspace_objs_if and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace> | ||
| kernel_entry_if e tc | ||
| \<lbrace>\<lambda>_. valid_vspace_objs_if\<rbrace>" | ||
| by wpsimp | ||
|
|
||
| lemma handle_preemption_if_valid_pdpt_objs[ADT_IF_assms, wp]: | ||
| "\<lbrace>valid_vspace_objs_if\<rbrace> handle_preemption_if a \<lbrace>\<lambda>rv s. valid_vspace_objs_if s\<rbrace>" | ||
| by wpsimp | ||
|
|
||
| lemma schedule_if_valid_pdpt_objs[ADT_IF_assms, wp]: | ||
| "\<lbrace>valid_vspace_objs_if\<rbrace> schedule_if a \<lbrace>\<lambda>rv s. valid_vspace_objs_if s\<rbrace>" | ||
| by wpsimp | ||
|
|
||
| lemma do_user_op_if_valid_pdpt_objs[ADT_IF_assms, wp]: | ||
| "\<lbrace>valid_vspace_objs_if\<rbrace> do_user_op_if a b \<lbrace>\<lambda>rv s. valid_vspace_objs_if s\<rbrace>" | ||
| by wpsimp | ||
|
|
||
| lemma valid_vspace_objs_if_ms_update[ADT_IF_assms, simp]: | ||
| "valid_vspace_objs_if (machine_state_update f s) = valid_vspace_objs_if s" | ||
| by simp | ||
|
|
||
| lemma do_user_op_if_irq_state_of_state[ADT_IF_assms]: | ||
| "do_user_op_if utf uc \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>" | ||
| apply (rule hoare_pre) | ||
| apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp | wpc)+ | ||
| done | ||
|
|
||
| lemma do_user_op_if_irq_masks_of_state[ADT_IF_assms]: | ||
| "do_user_op_if utf uc \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>" | ||
| apply (rule hoare_pre) | ||
| apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp | wpc)+ | ||
| done | ||
|
|
||
| lemma do_user_op_if_irq_measure_if[ADT_IF_assms]: | ||
| "do_user_op_if utf uc \<lbrace>\<lambda>s. P (irq_measure_if s)\<rbrace>" | ||
| apply (rule hoare_pre) | ||
| apply (simp add: do_user_op_if_def user_memory_update_def irq_measure_if_def | ||
| | wps |wp dmo_wp | wpc)+ | ||
| done | ||
|
|
||
| crunch set_flags, arch_post_set_flags | ||
| for irq_states_of_state[wp]: "\<lambda>s. P (irq_state_of_state s)" | ||
|
|
||
| lemma invoke_tcb_irq_state_inv[ADT_IF_assms]: | ||
| "\<lbrace>(\<lambda>s. irq_state_inv st s) and domain_sep_inv False sta | ||
| and tcb_inv_wf tinv and K (irq_is_recurring irq st)\<rbrace> | ||
| invoke_tcb tinv | ||
| \<lbrace>\<lambda>_ s. irq_state_inv st s\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>" | ||
| apply (case_tac tinv) | ||
| apply ((wp hoare_vcg_if_lift mapM_x_wp[OF _ subset_refl] | ||
| | wpc | ||
| | simp split del: if_split add: check_cap_at_def | ||
| | clarsimp | ||
| | wp (once) irq_state_inv_triv)+)[3] | ||
| defer | ||
| apply ((wp irq_state_inv_triv | simp)+)[2] | ||
| apply (simp add: split_def cong: option.case_cong) | ||
| by (clarsimp split del: if_split cong: conj_cong | ||
| | wp hoare_vcg_all_liftE_R hoare_vcg_all_lift hoare_vcg_const_imp_liftE_R | ||
| checked_cap_insert_domain_sep_inv cap_delete_deletes | ||
| cap_delete_irq_state_inv[where st=st and sta=sta and irq=irq] | ||
| cap_delete_irq_state_next[where st=st and sta=sta and irq=irq] | ||
| cap_delete_valid_cap cap_delete_cte_at | ||
| | wpc | ||
| | simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def | ||
| tcb_at_st_tcb_at option_update_thread_def | ||
| | strengthen use_no_cap_to_obj_asid_strg | ||
| | wp (once) irq_state_inv_triv hoare_drop_imps | ||
| | clarsimp split: option.splits | intro impI conjI allI)+ | ||
|
|
||
| lemma reset_untyped_cap_irq_state_inv[ADT_IF_assms]: | ||
| "\<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> | ||
| reset_untyped_cap slot | ||
| \<lbrace>\<lambda>y. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>y. irq_state_next st\<rbrace>" | ||
| apply (cases "irq_is_recurring irq st", simp_all) | ||
| apply (simp add: reset_untyped_cap_def) | ||
| apply (rule hoare_pre) | ||
| apply (wp no_irq_clearMemory mapME_x_wp' hoare_vcg_const_imp_lift | ||
| get_cap_wp preemption_point_irq_state_inv'[where irq=irq] | ||
| | rule irq_state_inv_triv | ||
| | simp add: unless_def | ||
| | wp (once) dmo_wp)+ | ||
| done | ||
|
|
||
| lemma handle_vm_fault_irq_state_of_state[ADT_IF_assms]: | ||
| "handle_vm_fault thread fault \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>" | ||
| unfolding handle_vm_fault_def addressTranslateS1_def | ||
| by (wpsimp wp: dmo_wp) | ||
|
|
||
| lemma handle_hypervisor_fault_irq_state_of_state[ADT_IF_assms]: | ||
| "handle_hypervisor_fault thread fault \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>" | ||
| by (cases fault, wpsimp wp: dmo_wp split_del: if_split) | ||
|
|
||
|
|
||
| text \<open>Not true of invoke_untyped any more.\<close> | ||
| crunch create_cap | ||
| for irq_state_of_state[ADT_IF_assms, wp]: "\<lambda>s. P (irq_state_of_state s)" | ||
| (ignore: freeMemory | ||
| wp: dmo_wp modify_wp crunch_wps | ||
| simp: freeMemory_def storeWord_def clearMemory_def | ||
| machine_op_lift_def machine_rest_lift_def mapM_x_defsym) | ||
|
|
||
| crunch arch_invoke_irq_control | ||
| for irq_state_of_state[ADT_IF_assms, wp]: "\<lambda>s. P (irq_state_of_state s)" | ||
| (wp: dmo_wp crunch_wps simp: setIRQTrigger_def machine_op_lift_def machine_rest_lift_def) | ||
|
|
||
| lemma handle_reserved_irq_non_kernel_IRQs[ADT_IF_assms]: | ||
| "\<lbrace>P and K (irq \<notin> non_kernel_IRQs)\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>_. P\<rbrace>" | ||
| unfolding handle_reserved_irq_def | ||
| apply (rule hoare_gen_asm) | ||
| apply (wpsimp wp: when_wp[where P'="\<bottom>"] simp: non_kernel_IRQs_def irq_vppi_event_index_def) | ||
| done | ||
|
|
||
| lemma thread_set_context_state_hyp_refs_of[CNode_AC_assms]: | ||
| "thread_set (tcb_arch_update (arch_tcb_context_set ctxt)) t \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>" | ||
| apply (wpsimp simp: thread_set_def wp: set_object_wp ) | ||
| apply (erule_tac P=P in back_subst) | ||
| apply (rule ext) | ||
| apply (simp add: state_hyp_refs_of_def get_tcb_def arch_tcb_context_set_def | ||
| split: option.splits kernel_object.splits) | ||
| done | ||
|
|
||
| (* FIXME AARCH64 IF: make generic *) | ||
| lemma thread_set_context_pas_refined[ADT_IF_assms]: | ||
| "thread_set (tcb_arch_update (arch_tcb_context_set ctxt)) t \<lbrace>pas_refined aag\<rbrace>" | ||
| unfolding pas_refined_def state_objs_to_policy_def | ||
| apply (rule hoare_weaken_pre) | ||
| apply (wpsimp wp: tcb_domain_map_wellformed_lift_strong thread_set_edomains) | ||
| apply (wps thread_set_state_vrefs thread_set_context_state_hyp_refs_of) | ||
| apply (rule hoare_lift_Pf2[where f="caps_of_state"]) | ||
| apply (rule hoare_lift_Pf2[where f="thread_st_auth"]) | ||
| apply (rule hoare_lift_Pf2[where f="thread_bound_ntfns"]) | ||
|
Contributor
Author
There was a problem hiding this comment. I'll review, but I recall there being a reason why it didn't work. |
||
| apply wp | ||
| apply (wpsimp wp: thread_set_thread_bound_ntfns_trivT ) | ||
| apply (wpsimp wp: thread_set_thread_st_auth_trivT) | ||
| apply (wpsimp wp: thread_set_caps_of_state_trivial simp: ran_tcb_cap_cases) | ||
| apply simp | ||
| done | ||
|
|
||
| crunch init_arch_objects | ||
| for irq_states_of_state[ADT_IF_assms, wp]: "\<lambda>s. P (irq_state_of_state s)" | ||
| (wp: crunch_wps dmo_wp) | ||
|
|
||
| end | ||
|
|
||
|
|
||
| global_interpretation ADT_IF_1?: ADT_IF_1 | ||
| proof goal_cases | ||
| interpret Arch . | ||
| case 1 show ?case | ||
| by (unfold_locales; (fact ADT_IF_assms | wp )?) | ||
| qed | ||
|
|
||
| sublocale valid_initial_state \<subseteq> valid_initial_state?: ADT_valid_initial_state .. | ||
|
|
||
|
|
||
| hide_fact ADT_IF_1.do_user_op_silc_inv | ||
| requalify_facts AARCH64.do_user_op_silc_inv | ||
| declare do_user_op_silc_inv[wp] | ||
|
|
||
| end | ||
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
this kind of thing feels like it could be moved to AInvs during cleanup, possible FIXME move?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I should be able to cut it altogether.
CNode_AC_assmsappearing here makes me think it's an unused remnant from WIP proofs.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Likely. I think normally we don't unfold it, i.e.
but then we have this:
which can't be interfaced directly. There's an instantiated version for FPU state, but not one for state_hyp_refs_of. There's also an ominous comment a bit above it in ArchTcbAcc_AI:
so that might be worth fixing up.