From ab4e713c09e87493249cc7691edfd488fdf1260a Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Fri, 2 Aug 2024 13:09:00 +1000 Subject: [PATCH] rt spec+proof: restrict reply grant rights In MCS configurations, a server's ability to grant capabilities when replying to a call were previously determined entirely by the grant right on the reply capability the server supplied when calling `receiveIPC`. If the server had sufficient untyped memory, it could create arbitrary reply capabilities, giving itself the ability to grant to its clients. Consequently, the only way to restrict a server's ability to grant to its clients was to avoid giving it untyped memory. This would break the expected authority confinement property. Contrast this with non-MCS configurations, where the grant rights on a server's receive endpoint control the server's ability to grant capabilities when replying to calls. This makes it much easier to restrict a server's ability to grant when replying. This commit makes MCS configurations behave more like non-MCS configurations: In order to grant capabilities when replying to a call, a server must have a grant right on the receive endpoint capability when it calls `receiveIPC`. This commit also removes the grant right from reply caps, as following the previous change this right has no clear use case. Signed-off-by: Corey Lewis --- proof/crefine/RISCV64/CSpace_C.thy | 30 +-- proof/crefine/RISCV64/Ipc_C.thy | 8 - proof/crefine/RISCV64/SR_lemmas_C.thy | 18 +- proof/crefine/RISCV64/StateRelation_C.thy | 1 + proof/crefine/RISCV64/Syscall_C.thy | 7 +- proof/crefine/RISCV64/Wellformed_C.thy | 2 +- proof/invariant-abstract/AInvs.thy | 11 +- .../invariant-abstract/ARM/ArchCSpace_AI.thy | 2 +- .../ARM/ArchInterrupt_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchIpc_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchKHeap_AI.thy | 9 + proof/invariant-abstract/CSpaceInv_AI.thy | 41 +-- proof/invariant-abstract/CSpacePre_AI.thy | 4 +- proof/invariant-abstract/CSpace_AI.thy | 13 +- .../DetSchedSchedule_AI.thy | 19 +- proof/invariant-abstract/Detype_AI.thy | 2 +- proof/invariant-abstract/Invariants_AI.thy | 19 +- proof/invariant-abstract/IpcCancel_AI.thy | 6 +- proof/invariant-abstract/IpcDet_AI.thy | 40 +-- proof/invariant-abstract/Ipc_AI.thy | 2 +- proof/invariant-abstract/KHeap_AI.thy | 240 +++++++++++++++++- .../RISCV64/ArchCSpace_AI.thy | 2 +- .../RISCV64/ArchInterrupt_AI.thy | 2 +- .../invariant-abstract/RISCV64/ArchIpc_AI.thy | 2 +- .../RISCV64/ArchKHeap_AI.thy | 9 + proof/invariant-abstract/Syscall_AI.thy | 2 +- proof/invariant-abstract/TcbAcc_AI.thy | 2 +- proof/refine/RISCV64/ADT_H.thy | 16 +- proof/refine/RISCV64/Bits_R.thy | 4 +- proof/refine/RISCV64/CSpace_I.thy | 10 +- proof/refine/RISCV64/Finalise_R.thy | 6 +- proof/refine/RISCV64/Invariants_H.thy | 8 +- proof/refine/RISCV64/IpcCancel_R.thy | 9 + proof/refine/RISCV64/Ipc_R.thy | 79 ++++-- proof/refine/RISCV64/KHeap_R.thy | 176 +++++++++++++ proof/refine/RISCV64/Reply_R.thy | 19 +- proof/refine/RISCV64/StateRelation.thy | 6 +- proof/refine/RISCV64/Syscall_R.thy | 14 +- spec/abstract/CSpace_A.thy | 8 +- spec/abstract/Decode_A.thy | 4 +- spec/abstract/Invocations_A.thy | 2 +- spec/abstract/Ipc_A.thy | 14 +- spec/abstract/KHeap_A.thy | 11 + spec/abstract/Retype_A.thy | 2 +- spec/abstract/Structures_A.thy | 19 +- spec/abstract/Syscall_A.thy | 3 +- spec/design/skel/Intermediate_H.thy | 2 +- spec/haskell/src/SEL4/API/Invocation.lhs | 2 +- spec/haskell/src/SEL4/Object/Endpoint.lhs | 9 +- spec/haskell/src/SEL4/Object/Instances.lhs | 2 +- spec/haskell/src/SEL4/Object/ObjectType.lhs | 10 +- spec/haskell/src/SEL4/Object/Structures.lhs | 4 +- 52 files changed, 685 insertions(+), 251 deletions(-) diff --git a/proof/crefine/RISCV64/CSpace_C.thy b/proof/crefine/RISCV64/CSpace_C.thy index be35878710..1d0ba728da 100644 --- a/proof/crefine/RISCV64/CSpace_C.thy +++ b/proof/crefine/RISCV64/CSpace_C.thy @@ -30,9 +30,6 @@ lemma maskCapRights_cap_cases: (\_. capNtfnCanReceive c \ capAllowRead R) (capNtfnCanSend_update (\_. capNtfnCanSend c \ capAllowWrite R) c)) - | ReplyCap _ _ \ - return (capReplyCanGrant_update - (\_. capReplyCanGrant c \ capAllowGrant R) c) | _ \ return c)" apply (simp add: maskCapRights_def Let_def split del: if_split) apply (cases c; simp add: isCap_simps split del: if_split) @@ -63,10 +60,9 @@ lemma maskVMRights_spec: \ret__unsigned_long && mask 2 = \ret__unsigned_long \ \ret__unsigned_long \ 0 \" apply vcg - apply (clarsimp simp: vmrights_defs vmrights_to_H_def maskVMRights_def mask_def - cap_rights_to_H_def to_bool_def - split: bool.split) - done + by (clarsimp simp: vmrights_defs vmrights_to_H_def maskVMRights_def mask_def + cap_rights_to_H_def to_bool_def + split: bool.split) lemma frame_cap_rights [simp]: "cap_get_tag cap = scast cap_frame_cap @@ -134,15 +130,6 @@ lemma to_bool_ntfn_cap_bf: apply simp done -lemma to_bool_reply_cap_bf: - "cap_lift c = Some (Cap_reply_cap cap) - \ to_bool (capReplyCanGrant_CL cap) = to_bool_bf (capReplyCanGrant_CL cap)" - apply (simp add: cap_lift_def Let_def split: if_split_asm) - apply (subst to_bool_bf_to_bool_mask, - clarsimp simp: cap_lift_thread_cap mask_def word_bw_assocs)+ - apply simp - done - lemma to_bool_ep_cap_bf: "cap_lift c = Some (Cap_endpoint_cap cap) \ to_bool (capCanSend_CL cap) = to_bool_bf (capCanSend_CL cap) \ @@ -291,17 +278,6 @@ lemma maskCapRights_ccorres [corres]: apply (rule conseqPre) apply vcg apply (simp add: cap_get_tag_isCap isCap_simps return_def) - apply clarsimp - apply (unfold ccap_relation_def)[1] - apply (simp add: cap_reply_cap_lift [THEN iffD1]) - apply (clarsimp simp: cap_to_H_def) - apply (simp add: map_option_case split: option.splits) - apply (clarsimp simp add: cap_to_H_def Let_def - split: cap_CL.splits if_split_asm) - apply (simp add: cap_reply_cap_lift_def) - apply (simp add: ccap_rights_relation_def cap_rights_to_H_def - to_bool_reply_cap_bf - to_bool_mask_to_bool_bf[simplified] to_bool_cap_rights_bf) apply (simp add: Collect_const_mem) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index 1f80932177..6bc7f7e70d 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -283,14 +283,6 @@ lemma ccap_relation_ep_helpers: cap_endpoint_cap_lift_def word_size elim!: ccap_relationE) -(* FIXME move *) -lemma ccap_relation_reply_helpers: - "\ ccap_relation cap cap'; cap_get_tag cap' = scast cap_reply_cap \ \ - capReplyCanGrant_CL (cap_reply_cap_lift cap') = from_bool (capReplyCanGrant cap)" - by (clarsimp simp: cap_lift_reply_cap cap_to_H_simps - cap_reply_cap_lift_def word_size - elim!: ccap_relationE) - (*FIXME: arch_split: C kernel names hidden by Haskell names *) (*FIXME: fupdate simplification issues for 2D arrays *) abbreviation "syscallMessageC \ kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]" diff --git a/proof/crefine/RISCV64/SR_lemmas_C.thy b/proof/crefine/RISCV64/SR_lemmas_C.thy index f004d6ca24..7f8d225766 100644 --- a/proof/crefine/RISCV64/SR_lemmas_C.thy +++ b/proof/crefine/RISCV64/SR_lemmas_C.thy @@ -253,8 +253,7 @@ lemma cap_get_tag_ReplyCap: assumes cr: "ccap_relation cap cap'" shows "(cap_get_tag cap' = scast cap_reply_cap) = (cap = - ReplyCap (capReplyPtr_CL (cap_reply_cap_lift cap')) - (to_bool (capReplyCanGrant_CL (cap_reply_cap_lift cap'))))" + ReplyCap (capReplyPtr_CL (cap_reply_cap_lift cap')))" using cr apply - apply (rule iffI) @@ -1787,6 +1786,19 @@ lemma obj_at_cslift_sc: apply fastforce done +lemma obj_at_cslift_reply: + fixes P :: "reply \ bool" + shows "\obj_at' P sc s; (s, s') \ rf_sr\ \ + \ko ko'. ko_at' ko sc s \ P ko \ + cslift s' (Ptr sc) = Some ko' \ + creply_relation ko ko'" + apply (frule obj_at_ko_at') + apply clarsimp + apply (frule cmap_relation_reply) + apply (drule (1) cmap_relation_ko_atD) + apply fastforce + done + fun thread_state_to_tsType :: "thread_state \ machine_word" where @@ -1987,7 +1999,7 @@ lemma cap_get_tag_isCap_unfolded_H_cap: and "ccap_relation (capability.IRQHandlerCap v13) cap' \ (cap_get_tag cap' = scast cap_irq_handler_cap)" and "ccap_relation (capability.IRQControlCap) cap' \ (cap_get_tag cap' = scast cap_irq_control_cap)" and "ccap_relation (capability.Zombie v14 v15 v16) cap' \ (cap_get_tag cap' = scast cap_zombie_cap)" - and "ccap_relation (capability.ReplyCap v17 v18) cap' \ (cap_get_tag cap' = scast cap_reply_cap)" + and "ccap_relation (capability.ReplyCap v17) cap' \ (cap_get_tag cap' = scast cap_reply_cap)" and "ccap_relation (capability.UntypedCap v100 v19 v20 v20b) cap' \ (cap_get_tag cap' = scast cap_untyped_cap)" and "ccap_relation (capability.CNodeCap v21 v22 v23 v24) cap' \ (cap_get_tag cap' = scast cap_cnode_cap)" and "ccap_relation (capability.DomainCap) cap' \ (cap_get_tag cap' = scast cap_domain_cap)" diff --git a/proof/crefine/RISCV64/StateRelation_C.thy b/proof/crefine/RISCV64/StateRelation_C.thy index d6b53caa34..9767ed17c7 100644 --- a/proof/crefine/RISCV64/StateRelation_C.thy +++ b/proof/crefine/RISCV64/StateRelation_C.thy @@ -498,6 +498,7 @@ lemma refill_buffer_relation_size_eq: definition creply_relation :: "Structures_H.reply \ reply_C \ bool" where "creply_relation areply creply \ option_to_ptr (replyTCB areply) = replyTCB_C creply + \ from_bool (replyCanGrant areply) = canGrant_C creply \ option_to_ptr (replyPrev areply) = ((Ptr \ callStackPtr_CL \ call_stack_lift \ replyPrev_C) creply :: reply_C ptr) \ isHead (replyNext areply) = to_bool ((isHead_CL \ call_stack_lift \ replyNext_C) creply) diff --git a/proof/crefine/RISCV64/Syscall_C.thy b/proof/crefine/RISCV64/Syscall_C.thy index 426bfb742c..ca54052a2d 100644 --- a/proof/crefine/RISCV64/Syscall_C.thy +++ b/proof/crefine/RISCV64/Syscall_C.thy @@ -96,10 +96,9 @@ lemma performInvocation_Notification_ccorres: lemma performInvocation_Reply_ccorres: "ccorres (K (K \) \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') - (invs' and tcb_at' sender and reply_at' reply) + (invs' and tcb_at' sender and reply_at' reply and obj_at' (\reply. replyCanGrant reply = grant) reply) (\\thread = tcb_ptr_to_ctcb_ptr sender\ - \ \\reply = reply_Ptr reply\ - \ \\canGrant = from_bool grant\) [] + \ \\reply = reply_Ptr reply\) [] (liftE (doReplyTransfer sender reply grant)) (Call performInvocation_Reply_'proc)" apply cinit @@ -109,7 +108,7 @@ lemma performInvocation_Reply_ccorres: apply wp apply simp apply (vcg exspec=doReplyTransfer_modifies) - apply (simp add: rf_sr_ksCurThread) + apply (fastforce dest: obj_at_cslift_reply simp: creply_relation_def typ_heap_simps) done lemma decodeInvocation_ccorres: diff --git a/proof/crefine/RISCV64/Wellformed_C.thy b/proof/crefine/RISCV64/Wellformed_C.thy index 28f07a1fe1..e296d28e84 100644 --- a/proof/crefine/RISCV64/Wellformed_C.thy +++ b/proof/crefine/RISCV64/Wellformed_C.thy @@ -323,7 +323,7 @@ where | Cap_notification_cap ntfn \ NotificationCap (capNtfnPtr_CL ntfn)(capNtfnBadge_CL ntfn)(to_bool(capNtfnCanSend_CL ntfn)) (to_bool(capNtfnCanReceive_CL ntfn)) - | Cap_reply_cap rc \ ReplyCap (capReplyPtr_CL rc) (to_bool (capReplyCanGrant_CL rc)) + | Cap_reply_cap rc \ ReplyCap (capReplyPtr_CL rc) | Cap_sched_context_cap sc \ SchedContextCap (capSCPtr_CL sc) (unat (capSCSizeBits_CL sc)) | Cap_sched_control_cap sc \ SchedControlCap | Cap_thread_cap tc \ ThreadCap(ctcb_ptr_to_tcb_ptr (Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) diff --git a/proof/invariant-abstract/AInvs.thy b/proof/invariant-abstract/AInvs.thy index 5df6ff4184..3fb70426ab 100644 --- a/proof/invariant-abstract/AInvs.thy +++ b/proof/invariant-abstract/AInvs.thy @@ -1017,7 +1017,8 @@ lemma receive_ipc_schact_is_rct_imp_ct_not_in_release_q: apply (wpsimp wp: complete_signal_schact_is_rct_imp_ct_not_in_release_q) apply ((wpsimp wp: hoare_vcg_imp_lift' thread_get_wp')+)[2] apply (wpsimp wp: thread_get_wp') - apply (wpsimp wp: hoare_vcg_imp_lift') + apply (wpsimp wp: hoare_vcg_imp_lift') + apply wpsimp apply wpsimp apply (wpsimp wp: hoare_vcg_imp_lift') apply (wpsimp wp: hoare_vcg_imp_lift') @@ -1886,6 +1887,10 @@ lemma check_budget_restart_schact_is_rct_imp_ct_activatable[wp]: "check_budget_restart \\s. schact_is_rct s \ ct_in_state activatable s\" by (wpsimp simp: check_budget_restart_def) +lemma update_reply_schact_is_rct_imp_ct_activatable[wp]: + "update_reply ptr f \\s. schact_is_rct s \ ct_in_state activatable s\" + by (wpsimp simp: update_reply_def set_object_def get_object_def obj_at_def pred_tcb_at_def ct_in_state_def) + lemma receive_ipc_schact_is_rct_imp_ct_activatable[wp]: "receive_ipc thread cap is_blocking reply_cap \\s :: det_state. schact_is_rct s \ ct_in_state activatable s\" @@ -1899,8 +1904,8 @@ lemma receive_ipc_schact_is_rct_imp_ct_activatable[wp]: apply (case_tac ep; clarsimp) apply (cases is_blocking; clarsimp) apply (rule bind_wp_fwd_skip, solves \(wpsimp | wpsimp wp: hoare_vcg_imp_lift')+\)+ - apply (wpsimp wp: set_simple_ko_wp hoare_vcg_imp_lift') - apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def simple_obj_at_def) + apply (wpsimp wp: set_simple_ko_wp update_reply_wp update_sk_obj_ref_wp) + apply (fastforce simp: ct_in_state_def pred_tcb_at_def obj_at_def simple_obj_at_def) apply (wpsimp wp: set_simple_ko_wp hoare_vcg_imp_lift') apply (rule bind_wp_fwd_skip, solves \(wpsimp | wpsimp wp: hoare_vcg_imp_lift')+\)+ apply (intro hoare_if) diff --git a/proof/invariant-abstract/ARM/ArchCSpace_AI.thy b/proof/invariant-abstract/ARM/ArchCSpace_AI.thy index 84f042b83a..ee346b8f88 100644 --- a/proof/invariant-abstract/ARM/ArchCSpace_AI.thy +++ b/proof/invariant-abstract/ARM/ArchCSpace_AI.thy @@ -543,7 +543,7 @@ lemma is_cap_simps': "is_ntfn_cap cap = (\r b R. cap = cap.NotificationCap r b R)" "is_zombie cap = (\r b n. cap = cap.Zombie r b n)" "is_arch_cap cap = (\a. cap = cap.ArchObjectCap a)" - "is_reply_cap cap = (\x R. cap = cap.ReplyCap x R)" + "is_reply_cap cap = (\x. cap = cap.ReplyCap x)" "is_sched_context_cap cap = (\x n. cap = cap.SchedContextCap x n)" "is_nondevice_page_cap cap = (\ u v w x. cap = ArchObjectCap (PageCap False u v w x))" by (cases cap, (auto simp: is_zombie_def is_arch_cap_def is_nondevice_page_cap_def diff --git a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy index 12a9cfaaff..c111c5f315 100644 --- a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy @@ -121,7 +121,7 @@ lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: (\s. cte_wp_at (is_derived (cdt s) src cap) src s) and (\s. cte_wp_at (\cap'. \irq\cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s) and - (\s. \t R. cap = ReplyCap t R \ + (\s. \t. cap = ReplyCap t \ st_tcb_at awaiting_reply t s \ \ has_reply_cap t s))\ cap_insert cap src dest \\rv s. invs s \ ex_inv s\" apply wp diff --git a/proof/invariant-abstract/ARM/ArchIpc_AI.thy b/proof/invariant-abstract/ARM/ArchIpc_AI.thy index dd434a0ee2..b5f267ca08 100644 --- a/proof/invariant-abstract/ARM/ArchIpc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchIpc_AI.thy @@ -27,7 +27,7 @@ lemma update_cap_data_closedform: | cap.DomainCap \ cap.DomainCap | cap.UntypedCap d p n idx \ cap.UntypedCap d p n idx | cap.NullCap \ cap.NullCap - | cap.ReplyCap t rights \ cap.ReplyCap t rights + | cap.ReplyCap t \ cap.ReplyCap t | cap.SchedContextCap s n \ cap.SchedContextCap s n | cap.SchedControlCap \ cap.SchedControlCap | cap.IRQControlCap \ cap.IRQControlCap diff --git a/proof/invariant-abstract/ARM/ArchKHeap_AI.thy b/proof/invariant-abstract/ARM/ArchKHeap_AI.thy index f712691b1b..3a5b57977f 100644 --- a/proof/invariant-abstract/ARM/ArchKHeap_AI.thy +++ b/proof/invariant-abstract/ARM/ArchKHeap_AI.thy @@ -926,6 +926,15 @@ lemma update_sched_context_hyp_refs_of[wp]: split: kernel_object.splits) done +lemma update_reply_hyp_refs_of[wp]: + "update_reply ptr f \\s. P (state_hyp_refs_of s)\" + apply (wpsimp simp: update_reply_def wp: set_object_wp get_object_wp) + apply (clarsimp elim!: rsubst[where P=P]) + apply (rule all_ext) + apply (clarsimp simp: state_hyp_refs_of_def obj_at_def hyp_refs_of_def + split: kernel_object.splits) + done + lemma update_valid_tcb[simp]: "\f. valid_tcb ptr tcb (release_queue_update f s) = valid_tcb ptr tcb s" "\f. valid_tcb ptr tcb (reprogram_timer_update f s) = valid_tcb ptr tcb s" diff --git a/proof/invariant-abstract/CSpaceInv_AI.thy b/proof/invariant-abstract/CSpaceInv_AI.thy index 71422a485f..01b18d913c 100644 --- a/proof/invariant-abstract/CSpaceInv_AI.thy +++ b/proof/invariant-abstract/CSpaceInv_AI.thy @@ -46,7 +46,7 @@ lemma is_valid_vtable_root_simps[simp]: "\ is_valid_vtable_root (CNodeCap cnode_ref sz guard)" "\ is_valid_vtable_root (EndpointCap ep_ref badge R)" "\ is_valid_vtable_root (NotificationCap ep_ref badge R)" - "\ is_valid_vtable_root (ReplyCap tcb_ref R)" + "\ is_valid_vtable_root (ReplyCap tcb_ref)" "\ is_valid_vtable_root (Zombie e f g)" "\ is_valid_vtable_root (NullCap)" "\ is_valid_vtable_root (DomainCap)" @@ -365,7 +365,7 @@ where | cap.ThreadCap ref \ cap.ThreadCap ref | cap.DomainCap \ cap.DomainCap | cap.SchedContextCap ref n \ cap.SchedContextCap ref n \ \?\ - | cap.ReplyCap ref R \ cap.ReplyCap ref UNIV + | cap.ReplyCap ref \ cap.ReplyCap ref | cap.UntypedCap dev ref n f \ cap.UntypedCap dev ref n 0 | cap.ArchObjectCap acap \ cap.ArchObjectCap (cap_master_arch_cap acap) | _ \ cap" @@ -398,8 +398,8 @@ lemma cap_master_cap_eqDs1: \ cap = cap.SchedContextCap ref n" "cap_master_cap cap = cap.SchedControlCap \ cap = cap.SchedControlCap" - "cap_master_cap cap = cap.ReplyCap ref rghts - \ rghts = UNIV \ (\rghts. cap = cap.ReplyCap ref rghts)" + "cap_master_cap cap = cap.ReplyCap ref + \ cap = cap.ReplyCap ref" by (clarsimp simp: cap_master_cap_def split: cap.split_asm)+ @@ -423,7 +423,7 @@ lemma cap_badge_simps [simp]: "cap_badge (cap.CNodeCap r bits guard) = None" "cap_badge (cap.ThreadCap r) = None" "cap_badge (cap.DomainCap) = None" - "cap_badge (cap.ReplyCap r rights) = None" + "cap_badge (cap.ReplyCap r) = None" "cap_badge (cap.IRQControlCap) = None" "cap_badge (cap.SchedContextCap sc n) = None" "cap_badge (cap.SchedControlCap) = None" @@ -1250,37 +1250,6 @@ lemma set_cap_valid_pspace: apply (clarsimp elim!: cte_wp_at_weakenE | rule conjI)+ done - -lemma set_object_idle [wp]: - "\valid_idle and - (\s. \ko t t' sc n. ko_at ko p s \ (p \ idle_thread_ptr \ p \ idle_sc_ptr \ - (ko = (TCB t) \ ko' = (TCB t') \ - tcb_state t = tcb_state t' \ - tcb_bound_notification t = tcb_bound_notification t' \ - tcb_sched_context t = tcb_sched_context t' \ - tcb_yield_to t = tcb_yield_to t' \ - valid_arch_idle (tcb_iarch t')) \ - (ko = (SchedContext sc n) \ ko' = (SchedContext sc n))))\ - set_object p ko' - \\rv. valid_idle\" - apply (wpsimp wp: set_object_wp_strong) - apply (auto simp: valid_idle_def pred_tcb_at_def obj_at_def) - done - -lemma set_object_fault_tcbs_valid_states[wp]: - "\\s. fault_tcbs_valid_states s \ - (\t. ko' = TCB t - \ (\t'. ko_at (TCB t') p s \ - tcb_state t' = tcb_state t \ - tcb_fault t' = tcb_fault t))\ - set_object p ko' - \\rv. fault_tcbs_valid_states\" - apply (wpsimp wp: set_object_wp_strong) - apply (clarsimp simp: fault_tcbs_valid_states_def pred_tcb_at_def obj_at_def) - apply (drule_tac x=p in spec) - apply clarsimp - done - lemma set_cap_idle[wp]: "\\s. valid_idle s\ set_cap cap p diff --git a/proof/invariant-abstract/CSpacePre_AI.thy b/proof/invariant-abstract/CSpacePre_AI.thy index e32a6d8863..3e8224481f 100644 --- a/proof/invariant-abstract/CSpacePre_AI.thy +++ b/proof/invariant-abstract/CSpacePre_AI.thy @@ -66,7 +66,7 @@ lemma masked_as_full_simps[simp]: "masked_as_full (cap.ArchObjectCap x) cap = (cap.ArchObjectCap x)" "masked_as_full (cap.CNodeCap r n g) cap = (cap.CNodeCap r n g)" "masked_as_full (cap.SchedContextCap r m) cap = (cap.SchedContextCap r m)" - "masked_as_full (cap.ReplyCap r R) cap = (cap.ReplyCap r R)" + "masked_as_full (cap.ReplyCap r) cap = (cap.ReplyCap r)" "masked_as_full cap.NullCap cap = cap.NullCap" "masked_as_full cap.DomainCap cap = cap.DomainCap" "masked_as_full (cap.ThreadCap r) cap = cap.ThreadCap r" @@ -75,7 +75,7 @@ lemma masked_as_full_simps[simp]: "masked_as_full cap (cap.ArchObjectCap x) = cap" "masked_as_full cap (cap.CNodeCap r n g) = cap" "masked_as_full cap (cap.SchedContextCap r m) = cap" - "masked_as_full cap (cap.ReplyCap r R) = cap" + "masked_as_full cap (cap.ReplyCap r) = cap" "masked_as_full cap cap.NullCap = cap" "masked_as_full cap cap.DomainCap = cap" "masked_as_full cap (cap.ThreadCap r) = cap" diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy index eead885c70..b271e481a3 100644 --- a/proof/invariant-abstract/CSpace_AI.thy +++ b/proof/invariant-abstract/CSpace_AI.thy @@ -660,7 +660,7 @@ where | Structures_A.ThreadCap r \ True | Structures_A.DomainCap \ False | Structures_A.SchedContextCap r n \ False - | Structures_A.ReplyCap r rights \ False + | Structures_A.ReplyCap r \ False | Structures_A.SchedControlCap \ False | Structures_A.IRQControlCap \ False | Structures_A.IRQHandlerCap irq \ True @@ -984,7 +984,7 @@ lemma cap_master_cap_simps: "cap_master_cap (cap.NullCap) = cap.NullCap" "cap_master_cap (cap.DomainCap) = cap.DomainCap" "cap_master_cap (cap.UntypedCap dev r n f) = cap.UntypedCap dev r n 0" - "cap_master_cap (cap.ReplyCap r rights) = cap.ReplyCap r UNIV" + "cap_master_cap (cap.ReplyCap r) = cap.ReplyCap r" "cap_master_cap (cap.IRQControlCap) = cap.IRQControlCap" "cap_master_cap (cap.SchedContextCap r n) = cap.SchedContextCap r n" "cap_master_cap (cap.SchedControlCap) = cap.SchedControlCap" @@ -3056,15 +3056,6 @@ lemma non_arch_cap_asid_vptr_None: using assms by (cases cap; simp add: is_cap_simps cap_asid_def cap_asid_base_def cap_vptr_def)+ end -lemma weak_derived_Reply: - "weak_derived (cap.ReplyCap t R) c = (\ R'. c = cap.ReplyCap t R')" - "weak_derived c (cap.ReplyCap t R) = (\ R'. c = cap.ReplyCap t R')" - by (auto simp: weak_derived_def copy_of_def - same_object_as_def is_cap_simps - non_arch_cap_asid_vptr_None[simplified is_cap_simps] - split: if_split_asm cap.split_asm) - - lemmas (in CSpace_AI_weak_derived) weak_derived_replies = weak_derived_is_reply weak_derived_obj_ref_of diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index 79f069d9ae..d054712852 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -7374,13 +7374,13 @@ lemma finalise_cap_cur_sc_chargeable: apply wpsimp apply wpsimp apply (wpsimp wp: cancel_all_ipc_cur_sc_chargeable split: if_split) - apply (wpsimp wp: cancel_all_signals_cur_sc_chargeable unbind_maybe_notification_invs split: if_split) + apply (wpsimp wp: cancel_all_signals_cur_sc_chargeable unbind_maybe_notification_invs split: if_split) apply (wpsimp wp: reply_remove_cur_sc_chargeable cancel_ipc_cur_sc_chargeable gts_wp get_simple_ko_wp split: if_split) - apply (rename_tac r R s ntfn x st) - apply (subgoal_tac "st_tcb_at (ipc_queued_thread_state) x s") - apply (clarsimp simp: obj_at_kh_kheap_simps ct_in_state_kh_simp) - apply (intro conjI; intro allI impI; clarsimp simp: invs_def pred_map_simps) + apply (rename_tac r s ntfn x st) + apply (subgoal_tac "st_tcb_at (ipc_queued_thread_state) x s") + apply (clarsimp simp: obj_at_kh_kheap_simps ct_in_state_kh_simp) + apply (intro conjI; intro allI impI; clarsimp simp: invs_def pred_map_simps) apply (subgoal_tac "(r, TCBReply) \ state_refs_of s x") apply (clarsimp simp: pred_tcb_at_def obj_at_def state_refs_of_def get_refs_def2 tcb_st_refs_of_def pred_neg_def @@ -15567,6 +15567,11 @@ crunch receive_ipc_preamble for released_if_bound[wp]: "released_if_bound_sc_tcb_at t" (ignore: thread_set update_sched_context wp: crunch_wps) +lemma update_reply_valid_sched_pred[wp]: + "update_reply ptr f \valid_sched_pred_strong P\" + by (wpsimp wp: update_reply_wp + simp: fun_upd_def obj_at_kh_kheap_simps vs_all_heap_simps) + (* Preconditions for the guts of receive_ipc, after the reply preamble *) abbreviation (input) receive_ipc_valid_sched_preconds :: "obj_ref \ obj_ref \ cap \ obj_ref option \ endpoint \ ('state_ext state \ bool) \ 'state_ext state \ bool" @@ -15586,7 +15591,7 @@ abbreviation (input) receive_ipc_valid_sched_preconds :: lemma receive_ipc_blocked_valid_sched': assumes ep: "case ep of IdleEP \ queue = [] | RecvEP q \ queue = q | SendEP _ \ False" shows "\ receive_ipc_valid_sched_preconds t ep_ptr reply reply_opt ep invs \ - receive_ipc_blocked is_blocking t ep_ptr reply_opt pl queue + receive_ipc_blocked is_blocking t ep_ptr ep_rights reply_opt pl queue \ \rv. valid_sched \" apply (cases reply_opt; clarsimp simp: receive_ipc_blocked_def) apply (wpsimp wp: set_thread_state_valid_sched) @@ -15597,7 +15602,7 @@ lemma receive_ipc_blocked_valid_sched': lemma receive_ipc_idle_valid_sched: "\ receive_ipc_valid_sched_preconds t ep_ptr reply reply_opt IdleEP invs \ - receive_ipc_idle is_blocking t ep_ptr reply_opt pl + receive_ipc_idle is_blocking t ep_ptr ep_rights reply_opt pl \ \rv. valid_sched \" apply (rule hoare_weaken_pre, rule monadic_rewrite_refine_valid[where P''=\]) apply (rule monadic_rewrite_receive_ipc_idle) diff --git a/proof/invariant-abstract/Detype_AI.thy b/proof/invariant-abstract/Detype_AI.thy index 2d5072dbcf..25f27fa292 100644 --- a/proof/invariant-abstract/Detype_AI.thy +++ b/proof/invariant-abstract/Detype_AI.thy @@ -100,7 +100,7 @@ definition obj_reply_refs :: "cap \ machine_word set" where "obj_reply_refs cap \ obj_refs cap \ - (case cap of cap.ReplyCap t R \ {t} | _ \ {})" + (case cap of cap.ReplyCap t \ {t} | _ \ {})" lemma ex_cte_cap_to_obj_ref_disj: diff --git a/proof/invariant-abstract/Invariants_AI.thy b/proof/invariant-abstract/Invariants_AI.thy index 03cd92f40a..d14aa8527b 100644 --- a/proof/invariant-abstract/Invariants_AI.thy +++ b/proof/invariant-abstract/Invariants_AI.thy @@ -415,7 +415,7 @@ where | "untyped_range (cap.CNodeCap r bits guard) = {}" | "untyped_range (cap.ThreadCap r) = {}" | "untyped_range (cap.DomainCap) = {}" -| "untyped_range (cap.ReplyCap r rights) = {}" +| "untyped_range (cap.ReplyCap r) = {}" | "untyped_range (cap.SchedContextCap r n) = {}" | "untyped_range (cap.SchedControlCap) = {}" | "untyped_range (cap.IRQControlCap) = {}" @@ -454,7 +454,7 @@ where | "cap_bits (CNodeCap r b m) = cte_level_bits + b" | "cap_bits (ThreadCap r) = obj_bits (TCB undefined)" | "cap_bits (DomainCap) = 0" -| "cap_bits (ReplyCap r R) = obj_bits (Reply undefined)" +| "cap_bits (ReplyCap r) = obj_bits (Reply undefined)" | "cap_bits (Zombie r zs n) = (case zs of None \ obj_bits (TCB undefined) | Some n \ cte_level_bits + n)" @@ -500,8 +500,6 @@ where | Some b \ n \ 2 ^ b \ b \ 0) | ArchObjectCap ac \ wellformed_acap ac | SchedContextCap scp n \ valid_sched_context_size n - | ReplyCap t rights \ AllowWrite \ rights \ AllowRead \ rights \ - AllowGrantReply \ rights | _ \ True" definition @@ -515,7 +513,7 @@ where | CNodeCap r bits guard \ cap_table_at bits r s | ThreadCap r \ tcb_at r s | DomainCap \ True - | ReplyCap r rights \ reply_at r s + | ReplyCap r \ reply_at r s | SchedContextCap r n \ sc_obj_at n r s | SchedControlCap \ True | IRQControlCap \ True @@ -538,8 +536,7 @@ where cap_table_at bits r s \ bits \ 0 \ length guard \ word_bits | ThreadCap r \ tcb_at r s | DomainCap \ True - | ReplyCap r rights \ reply_at r s - \ AllowWrite \ rights \ AllowRead \ rights \ AllowGrantReply \ rights + | ReplyCap r \ reply_at r s | SchedContextCap r n \ sc_obj_at n r s \ valid_sched_context_size n | SchedControlCap \ True | IRQControlCap \ True @@ -573,7 +570,7 @@ where | "cap_class (cap.SchedControlCap) = SchedControlClass" | "cap_class (cap.IRQControlCap) = IRQClass" | "cap_class (cap.IRQHandlerCap irq) = IRQClass" -| "cap_class (cap.ReplyCap tcb rights) = PhysicalClass" +| "cap_class (cap.ReplyCap tcb) = PhysicalClass" | "cap_class (cap.ArchObjectCap cap) = acap_class cap" @@ -1001,7 +998,7 @@ where | "cte_refs (SchedControlCap) f = {}" | "cte_refs (IRQControlCap) f = {}" | "cte_refs (IRQHandlerCap irq) f = {(f irq, [])}" -| "cte_refs (ReplyCap r rights) f = {}" +| "cte_refs (ReplyCap r) f = {}" | "cte_refs (ArchObjectCap cap) f = {}" definition @@ -1142,7 +1139,7 @@ definition \p. is_original_cap s p \ cte_wp_at (\x. x \ NullCap) p s" definition - "is_reply_cap_to t \ \cap. \rights. cap = ReplyCap t rights" + "is_reply_cap_to t \ \cap. cap = ReplyCap t" definition "has_reply_cap t s \ \p. cte_wp_at (is_reply_cap_to t) p s" @@ -3011,7 +3008,7 @@ lemma is_cap_simps: "is_sched_context_cap cap = (\r n. cap = SchedContextCap r n)" "is_zombie cap = (\r b n. cap = Zombie r b n)" "is_arch_cap cap = (\a. cap = ArchObjectCap a)" - "is_reply_cap cap = (\x R. cap = ReplyCap x R)" + "is_reply_cap cap = (\x. cap = ReplyCap x)" by (cases cap, auto simp: is_zombie_def is_arch_cap_def is_reply_cap_def)+ diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index e58794000f..67d2a01d5c 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -1706,18 +1706,18 @@ crunch cancel_ipc (wp: assert_inv thread_set_no_change_tcb_pred) lemma fast_finalise_bound_tcb_at: - "\\s. bound_tcb_at P t s \ (\tt r. cap = ReplyCap tt r) \ fast_finalise cap final \\_. bound_tcb_at P t\" + "\\s. bound_tcb_at P t s \ (\tt. cap = ReplyCap tt) \ fast_finalise cap final \\_. bound_tcb_at P t\" apply (case_tac cap, simp_all) apply (wpsimp wp: hoare_drop_imps hoare_vcg_all_lift) done lemma get_cap_reply_cap_helper: - "\\s. \t r. Some (ReplyCap t r) = caps_of_state s slot \ get_cap slot \\rv s. \t r. rv = ReplyCap t r\" + "\\s. \t. Some (ReplyCap t) = caps_of_state s slot \ get_cap slot \\rv s. \t. rv = ReplyCap t\" by (auto simp: valid_def get_cap_caps_of_state[symmetric]) lemma cap_delete_one_bound_tcb_at: - "\\s. bound_tcb_at P t s \ (\t r. caps_of_state s c = Some (ReplyCap t r)) \ + "\\s. bound_tcb_at P t s \ (\t. caps_of_state s c = Some (ReplyCap t)) \ cap_delete_one c \\_. bound_tcb_at P t\" by (wpsimp simp: cap_delete_one_def unless_def wp: fast_finalise_bound_tcb_at hoare_vcg_if_lift2 get_cap_reply_cap_helper diff --git a/proof/invariant-abstract/IpcDet_AI.thy b/proof/invariant-abstract/IpcDet_AI.thy index 995af624df..49727da433 100644 --- a/proof/invariant-abstract/IpcDet_AI.thy +++ b/proof/invariant-abstract/IpcDet_AI.thy @@ -227,7 +227,7 @@ definition receive_ipc_preamble :: where "receive_ipc_preamble reply t \ case reply of NullCap \ return None - | ReplyCap r _ \ + | ReplyCap r \ do tptr <- get_reply_tcb r; when (tptr \ None \ the tptr \ t) $ cancel_ipc (the tptr); return (Some r) @@ -337,23 +337,29 @@ lemma tcb_ep_append_not_null [wp]: done definition receive_ipc_blocked :: - "bool \ obj_ref \ obj_ref \ obj_ref option \ receiver_payload \ obj_ref list \ + "bool \ obj_ref \ obj_ref \ cap_rights \ obj_ref option \ receiver_payload \ obj_ref list \ ('a::state_ext state, unit) nondet_monad" where - "receive_ipc_blocked is_blocking t ep_ptr reply pl queue \ + "receive_ipc_blocked is_blocking t ep_ptr ep_rights reply pl queue \ case is_blocking of True \ do _ <- set_thread_state t (BlockedOnReceive ep_ptr reply pl); - _ <- when (\r. reply = Some r) (set_reply_obj_ref reply_tcb_update (the reply) (Some t)); + _ <- when (\r. reply = Some r) (do + _ <- set_reply_obj_ref reply_tcb_update (the reply) (Some t); + update_reply (the reply) (reply_can_grant_update (\_. AllowGrant \ ep_rights)) + od); q <- tcb_ep_append t queue; set_endpoint ep_ptr (RecvEP q) od | False \ do_nbrecv_failed_transfer t" definition receive_ipc_idle :: - "bool \ obj_ref \ obj_ref \ obj_ref option \ receiver_payload \ ('a::state_ext state, unit) nondet_monad" + "bool \ obj_ref \ obj_ref \ cap_rights \ obj_ref option \ receiver_payload \ ('a::state_ext state, unit) nondet_monad" where - "receive_ipc_idle is_blocking t ep_ptr reply pl \ + "receive_ipc_idle is_blocking t ep_ptr ep_rights reply pl \ case is_blocking of True \ do _ <- set_thread_state t (BlockedOnReceive ep_ptr reply pl); - _ <- when (\r. reply = Some r) (set_reply_obj_ref reply_tcb_update (the reply) (Some t)); + _ <- when (\r. reply = Some r) (do + _ <- set_reply_obj_ref reply_tcb_update (the reply) (Some t); + update_reply (the reply) (reply_can_grant_update (\_. AllowGrant \ ep_rights)) + od); set_endpoint ep_ptr (RecvEP [t]) od | False \ do_nbrecv_failed_transfer t" @@ -372,8 +378,8 @@ lemma monadic_rewrite_sort_queue_singleton: qed lemma monadic_rewrite_receive_ipc_idle: - "monadic_rewrite False True (tcb_at t) (receive_ipc_blocked is_blocking t ep_ptr reply pl []) - (receive_ipc_idle is_blocking t ep_ptr reply pl)" + "monadic_rewrite False True (tcb_at t) (receive_ipc_blocked is_blocking t ep_ptr ep_rights reply pl []) + (receive_ipc_idle is_blocking t ep_ptr ep_rights reply pl)" apply (cases is_blocking; simp add: receive_ipc_blocked_def receive_ipc_idle_def monadic_rewrite_guard_imp[OF monadic_rewrite_refl]) apply (rule monadic_rewrite_bind_tail[OF _ set_thread_state_tcb]) @@ -387,8 +393,8 @@ primrec receive_ipc_preamble_rv :: where "receive_ipc_preamble_rv reply None = (\s. reply = NullCap)" | "receive_ipc_preamble_rv reply (Some reply_ptr) = - (\s. (\R. reply = ReplyCap reply_ptr R) \ reply_tcb_reply_at (\t. t = None) reply_ptr s - \ reply_sc_reply_at (\sc. sc = None) reply_ptr s)" + (\s. (reply = ReplyCap reply_ptr) \ reply_tcb_reply_at (\t. t = None) reply_ptr s + \ reply_sc_reply_at (\sc. sc = None) reply_ptr s)" (* Preconditions for the guts of receive_ipc, after the reply preamble *) abbreviation (input) receive_ipc_preconds :: @@ -434,7 +440,7 @@ global_interpretation set_reply_tcb_obj_ref: lemma receive_ipc_blocked_invs': assumes ep: "case ep of IdleEP \ queue = [] | RecvEP q \ queue = q | SendEP _ \ False" shows "\ receive_ipc_preconds t ep_ptr reply reply_opt ep invs \ - receive_ipc_blocked is_blocking t ep_ptr reply_opt pl queue + receive_ipc_blocked is_blocking t ep_ptr ep_rights reply_opt pl queue \ \rv. invs \" proof - have ep_valid: @@ -462,7 +468,7 @@ lemma receive_ipc_blocked_invs': , assumption , fastforce simp: replies_blocked_def st_tcb_at_def obj_at_def\) apply (all \rule revcut_rl[where V="ep_ptr \ t"], fastforce simp: obj_at_def pred_tcb_at_def\) - apply (all \(match premises in \reply = ReplyCap r_ptr R\ for r_ptr R \ + apply (all \(match premises in \reply = ReplyCap r_ptr\ for r_ptr \ \rule revcut_rl[where V="r_ptr \ {t, ep_ptr}"]\ , fastforce simp: obj_at_def reply_tcb_reply_at_def pred_tcb_at_def)?\) apply (all \frule obj_at_state_refs_ofD; clarsimp simp: ep_queue\) @@ -478,7 +484,7 @@ lemma receive_ipc_blocked_invs': lemma receive_ipc_idle_invs: "\ receive_ipc_preconds t ep_ptr reply reply_opt IdleEP invs \ - receive_ipc_idle is_blocking t ep_ptr reply_opt pl + receive_ipc_idle is_blocking t ep_ptr ep_rights reply_opt pl \ \rv. invs \" apply (rule hoare_weaken_pre, rule monadic_rewrite_refine_valid[where P''=\]) apply (rule monadic_rewrite_receive_ipc_idle) @@ -773,7 +779,7 @@ lemma receive_ipc_preamble_rv: "\st_tcb_at active t and invs\ receive_ipc_preamble reply t \receive_ipc_preamble_rv reply\" unfolding receive_ipc_preamble_def apply (cases reply; clarsimp intro!: hoare_weaken_pre[OF return_wp]) - apply (thin_tac _, rename_tac reply_ptr R) + apply (thin_tac _, rename_tac reply_ptr) apply (rule bind_wp[OF _ grt_sp]; simp?) apply (rename_tac t_opt) apply (case_tac t_opt; @@ -1356,7 +1362,7 @@ lemma ri_invs[wp]: ko_at (Endpoint ep) ep_ptr s \ invs s" in bind_wp_fwd) apply (wpsimp wp: hoare_vcg_ball_lift split: if_split) - apply (fastforce dest: st_tcb_at_idle_thread split: if_split) + apply (fastforce dest: st_tcb_at_idle_thread split: if_split) (* IdleEP, RecvEP *) apply (case_tac ep; clarsimp simp: receive_ipc_blocked_invs[where reply=reply]) (* SendEP *) @@ -1440,7 +1446,7 @@ lemma ri_invs[wp]: apply (rule bind_wp[OF _ gsc_sp]) apply (clarsimp) apply (rename_tac rply) - apply (wp reply_push_sender_sc_Some_invs) + apply (wp reply_push_sender_sc_Some_invs hoare_vcg_ball_lift receive_ipc_preamble_rv_lift) apply (clarsimp) apply (intro conjI) prefer 3 diff --git a/proof/invariant-abstract/Ipc_AI.thy b/proof/invariant-abstract/Ipc_AI.thy index 223f0d6a37..3b5aea70f8 100644 --- a/proof/invariant-abstract/Ipc_AI.thy +++ b/proof/invariant-abstract/Ipc_AI.thy @@ -2085,7 +2085,7 @@ lemma cap_delete_one_valid_tcb_state: done lemma cte_wp_at_reply_cap_can_fast_finalise: - "cte_wp_at ((=) (cap.ReplyCap tcb R)) slot s \ cte_wp_at can_fast_finalise slot s" + "cte_wp_at ((=) (cap.ReplyCap tcb)) slot s \ cte_wp_at can_fast_finalise slot s" by (clarsimp simp: cte_wp_at_caps_of_state can_fast_finalise_def) context Ipc_AI begin diff --git a/proof/invariant-abstract/KHeap_AI.thy b/proof/invariant-abstract/KHeap_AI.thy index e0fbc72341..14f3f2de37 100644 --- a/proof/invariant-abstract/KHeap_AI.thy +++ b/proof/invariant-abstract/KHeap_AI.thy @@ -58,6 +58,7 @@ requalify_facts state_hyp_refs_of_tcb_domain_update state_hyp_refs_of_tcb_priority_update update_sched_context_hyp_refs_of + update_reply_hyp_refs_of arch_valid_obj_same_type default_arch_object_not_live @@ -75,6 +76,7 @@ requalify_facts end declare update_sched_context_hyp_refs_of[wp] +declare update_reply_hyp_refs_of[wp] lemmas cap_is_device_obj_is_device[simp] = cap_is_device_obj_is_device lemmas storeWord_device_state_hoare[wp] = storeWord_device_state_inv @@ -807,6 +809,12 @@ lemma update_sched_context_mdb [wp]: "\valid_mdb\ update_sched_context ptr val \\r. valid_mdb\" by (wpsimp simp: update_sched_context_def get_object_def wp: valid_mdb_lift) +lemma update_reply_caps_of_state[wp]: + "update_reply ptr val \\s. P (caps_of_state s)\" + apply (wpsimp simp: update_reply_def get_object_def set_object_def) + apply (subst cte_wp_caps_of_lift; auto simp: cte_wp_at_cases) + done + lemma cte_wp_at_after_update: "\ obj_at (same_caps val) p' s \ \ cte_wp_at P p (kheap_update (\a b. if b = p' then Some val else kheap s b) s) @@ -1754,11 +1762,12 @@ interpretation set_tcb_sched_context: non_aobj_non_cap_non_mem_op "set_tcb_obj_ref tcb_sched_context_update p sc" + update_sched_context: non_aobj_non_cap_non_mem_op "update_sched_context p sc'" + update_sched_context: non_aobj_non_cap_non_mem_op "update_sched_context p update" + + update_reply: non_aobj_non_cap_non_mem_op "update_reply p update'" + set_tcb_yt: non_aobj_non_cap_non_mem_op "set_tcb_obj_ref tcb_yield_to_update p sc" apply (all \unfold_locales; (wp ; fail)?\) unfolding set_simple_ko_def set_thread_state_def set_tcb_obj_ref_def thread_set_def set_cap_def[simplified split_def] - as_user_def set_mrs_def update_sched_context_def update_sched_context_def + as_user_def set_mrs_def update_sched_context_def update_sched_context_def update_reply_def apply - supply validNF_prop[wp_unsafe del] apply (all \(wp set_object_non_arch[THEN hoare_set_object_weaken_pre] get_object_wp | wpc @@ -1963,7 +1972,7 @@ lemma valid_irq_states_scheduler_action[simp]: by (simp add: valid_irq_states_def) crunch - set_simple_ko, set_cap, thread_set, set_thread_state, set_tcb_obj_ref, update_sched_context + set_simple_ko, set_cap, thread_set, set_thread_state, set_tcb_obj_ref, update_sched_context, update_reply for valid_irq_states[wp]: "valid_irq_states" (wp: crunch_wps simp: crunch_simps rule: valid_irq_states_triv) @@ -2342,10 +2351,10 @@ lemma get_sc_obj_ref_wp: by (wpsimp simp: get_sc_obj_ref_def) lemma update_sched_context_wp: - "\ \s. \sc n. ko_at (SchedContext sc n) sc_ptr s - \ Q (s\kheap := (kheap s)(sc_ptr \ SchedContext (f sc) n)\) \ + "\\s. \sc n. ko_at (SchedContext sc n) sc_ptr s + \ Q (s\kheap := (kheap s)(sc_ptr \ SchedContext (f sc) n)\)\ update_sched_context sc_ptr f - \ \rv. Q \" + \\rv. Q\" by (wpsimp simp: update_sched_context_def wp: set_object_wp get_object_wp) lemma update_sched_context_obj_at_trivial: @@ -2474,6 +2483,36 @@ lemma set_object_dom_shrink[wp]: apply (clarsimp simp: obj_at_def split: if_split_asm) done +lemma set_object_idle[wp]: + "\valid_idle and + (\s. \ko t t' sc n. ko_at ko p s \ (p \ idle_thread_ptr \ p \ idle_sc_ptr \ + (ko = (TCB t) \ ko' = (TCB t') \ + tcb_state t = tcb_state t' \ + tcb_bound_notification t = tcb_bound_notification t' \ + tcb_sched_context t = tcb_sched_context t' \ + tcb_yield_to t = tcb_yield_to t' \ + valid_arch_idle (tcb_iarch t')) \ + (ko = (SchedContext sc n) \ ko' = (SchedContext sc n))))\ + set_object p ko' + \\rv. valid_idle\" + apply (wpsimp wp: set_object_wp_strong) + apply (auto simp: valid_idle_def pred_tcb_at_def obj_at_def) + done + +lemma set_object_fault_tcbs_valid_states[wp]: + "\\s. fault_tcbs_valid_states s \ + (\t. ko' = TCB t + \ (\t'. ko_at (TCB t') p s \ + tcb_state t' = tcb_state t \ + tcb_fault t' = tcb_fault t))\ + set_object p ko' + \\rv. fault_tcbs_valid_states\" + apply (wpsimp wp: set_object_wp_strong) + apply (clarsimp simp: fault_tcbs_valid_states_def pred_tcb_at_def obj_at_def) + apply (drule_tac x=p in spec) + apply clarsimp + done + lemma set_aobject_zombies[wp]: "set_object ptr (ArchObj obj) \\s. zombies_final s\" apply (wp set_object_zombies[THEN hoare_set_object_weaken_pre]) @@ -2620,4 +2659,195 @@ lemma update_sched_context_no_fail[wp]: apply (clarsimp simp: obj_at_def a_type_def) done +lemma update_reply_no_fail[wp]: + "no_fail (\s. \reply. kheap s reply_ptr = Some (Reply reply)) (update_reply reply_ptr f)" + apply (clarsimp simp: update_reply_def) + apply (wpsimp wp: get_object_wp) + apply (clarsimp simp: obj_at_def) + done + +lemma update_reply_wp: + "\\s. \reply. ko_at (Reply reply) reply_ptr s + \ Q (s\kheap := (kheap s)(reply_ptr \ Reply (f reply))\)\ + update_reply reply_ptr f + \\_. Q\" + by (wpsimp simp: update_reply_def wp: set_object_wp get_object_wp) + +lemma update_reply_obj_at_trivial: + "\obj_at P t' and K (\reply. P (Reply reply) \ P (Reply (f reply)))\ + update_reply reply_ptr f + \\_. obj_at P t'\" + by (wpsimp wp: update_reply_wp simp: obj_at_def) + +lemma update_reply_typ_at[wp]: + "update_reply ptr f \\s. P (typ_at T p s)\" + by (wpsimp simp: update_reply_def get_object_def wp: set_object_typ_at) + +lemmas update_reply_typ_ats [wp] = abs_typ_at_lifts [OF update_reply_typ_at] + +lemma update_reply_cte_wp_at[wp]: + "update_reply ptr f \cte_wp_at P p\" + by (wpsimp simp: update_reply_def set_object_def cte_wp_at_cases get_object_def) + +crunch update_reply + for ex_nonz_cap_to[wp]: "ex_nonz_cap_to p" + (wp: ex_nonz_cap_to_pres) + +lemma update_reply_pred_tcb_at[wp]: + "update_reply ptr update \\s. P (pred_tcb_at proj f t s)\" + by (wpsimp simp: update_reply_def set_object_def get_object_def pred_tcb_at_def obj_at_def) + +lemma update_reply_valid_replies[wp]: + "update_reply ptr f \valid_replies_pred P\" + apply (rule hoare_lift_Pf2[where f=replies_blocked, rotated]) + apply (wp replies_blocked_lift) + apply (wp replies_with_sc_lift) + apply (wp update_reply_wp) + apply (clarsimp simp: sc_replies_sc_at_def obj_at_def ) + apply clarsimp + done + +lemma update_reply_can_grant_reply_tcb_reply_at[wp]: + "update_reply ptr (reply_can_grant_update f) \\s. P (reply_tcb_reply_at Q t s) \" + by (wpsimp simp: update_reply_def reply_at_ppred_def obj_at_def + wp: set_object_wp get_object_wp) + +lemma update_reply_can_grant_reply_sc_reply_at[wp]: + "update_reply ptr (reply_can_grant_update f) \\s. P (reply_sc_reply_at Q t s) \" + by (wpsimp simp: update_reply_def reply_at_ppred_def obj_at_def + wp: set_object_wp get_object_wp) + +lemma update_reply_refs_of_same: + "\\s. P (state_refs_of s) \ (\reply. refs_of_reply reply = refs_of_reply (f reply))\ + update_reply ptr f + \\rv s. P (state_refs_of s)\" + apply (wpsimp simp: update_reply_def set_object_def get_object_def) + apply (clarsimp simp: state_refs_of_def ext elim!: rsubst[where P = P]) + done + +lemma update_reply_can_grant_sym_refs[wp]: + "update_reply ptr (reply_can_grant_update f) \\s. P (state_refs_of s)\" + by (wpsimp wp: update_reply_refs_of_same) + +lemma update_reply_valid_objs_same: + "\\s. valid_objs s \ (\reply. valid_reply reply s \ valid_reply (f reply) s)\ + update_reply ref f + \\_. valid_objs\" + apply (wpsimp simp: update_reply_def get_object_def) + apply (auto simp: valid_obj_def) + done + +lemmas reply_can_grant_update_valid_objs[wp] + = update_reply_valid_objs_same[where f="reply_can_grant_update f" for f, + simplified valid_reply_def, simplified] + +lemma update_reply_aligned[wp]: + "update_reply ptr v \pspace_aligned\" + by (wpsimp simp: update_reply_def wp: set_object_aligned get_object_wp) + +lemma update_reply_distinct[wp]: + "update_reply ptr f \pspace_distinct\" + by (wpsimp simp: update_reply_def wp: set_object_distinct get_object_wp) + +lemma update_reply_valid_ioc[wp]: + "update_reply ptr f \valid_ioc\" + by (wpsimp simp: update_reply_def obj_at_def is_tcb is_cap_table + wp: set_object_valid_ioc_no_caps get_object_wp) + +lemma update_reply_iflive_implies: + "\\s. if_live_then_nonz_cap s \ (\reply. live_reply (f reply) \ live_reply reply)\ + update_reply ptr f + \\rv. if_live_then_nonz_cap\" + by (wpsimp simp: update_reply_def get_object_def obj_at_def if_live_then_nonz_cap_def live_def is_reply) + +lemma reply_can_grant_update_iflive[wp]: + "update_reply ptr (reply_can_grant_update f) \if_live_then_nonz_cap\" + by (wpsimp simp: live_reply_def wp: update_reply_iflive_implies) + +lemma update_reply_zombies[wp]: + "update_reply ptr f \zombies_final\" + by (wpsimp simp: update_reply_def get_object_def obj_at_def is_reply) + +lemma update_reply_revokable[wp]: + "update_reply ptr val \\s. P (is_original_cap s)\" + by (wpsimp simp: update_reply_def set_object_def get_object_def) + +crunch update_reply + for no_cdt[wp]: "\s. P (cdt s)" + and interrupt_states[wp]: "\s. P (interrupt_states s)" + +lemma update_reply_mdb[wp]: + "update_reply ptr f \valid_mdb\" + by (wpsimp wp: valid_mdb_lift) + +lemma update_reply_valid_idle[wp]: + "update_reply ptr f \valid_idle\" + apply (wpsimp simp: update_reply_def get_object_def) + apply (auto simp: valid_idle_def pred_tcb_at_def obj_at_def) + done + +crunch update_reply + for it[wp]: "\s. P (idle_thread s)" + +lemma update_reply_only_idle[wp]: + "update_reply ptr f \only_idle\" + by (wpsimp wp: only_idle_lift) + +lemma update_reply_ifunsafe[wp]: + "update_reply ptr f \if_unsafe_then_cap\" + by (wpsimp simp: update_reply_def get_object_def obj_at_def is_reply) + +lemma update_reply_global_refs[wp]: + "update_reply ptr f \valid_global_refs\" + by (wpsimp simp: update_reply_def get_object_def wp: valid_global_refs_cte_lift) + +crunch update_reply + for irq_node[wp]: "\s. P (interrupt_irq_node s)" + +lemma update_reply_valid_irq_node[wp]: + "update_reply ptr f \valid_irq_node\" + by (wpsimp wp: valid_irq_node_typ) + +lemma update_reply_valid_irq_handlers[wp]: + "update_reply ptr f \valid_irq_handlers\" + apply (wpsimp simp: update_reply_def set_object_def get_object_def valid_irq_handlers_def + irq_issued_def ran_def) + apply (subgoal_tac "caps_of_state s (a, b) = Some cap") + apply fastforce + apply (subst cte_wp_caps_of_lift; auto simp: cte_wp_at_cases) + done + +lemma update_reply_kernel_window[wp]: + "update_reply ptr f \pspace_in_kernel_window\" + by (wpsimp simp: update_reply_def get_object_def + wp: set_object_pspace_in_kernel_window) + +lemma update_reply_cap_refs_kernel_window[wp]: + "update_reply ptr f \cap_refs_in_kernel_window\" + by (wpsimp simp: update_reply_def obj_at_def is_reply + wp: set_object_cap_refs_in_kernel_window get_object_wp) + +lemma update_reply_respect_device_region[wp]: + "update_reply ptr f \pspace_respects_device_region\" + by (wpsimp simp: update_reply_def get_object_def + wp: set_object_pspace_respects_device_region) + +lemma update_reply_cap_refs_respects_device_region[wp]: + "update_reply ptr f \cap_refs_respects_device_region\" + by (wpsimp simp: update_reply_def get_object_def obj_at_def is_reply + wp: set_object_cap_refs_respects_device_region) + +lemma update_reply_fault_tcbs_valid_states[wp]: + "update_reply ref f \fault_tcbs_valid_states\" + apply (wpsimp simp: update_reply_def get_object_def) + done + +lemma update_reply_cur_tcb[wp]: + "update_reply ptr f \cur_tcb\" + by (wpsimp simp: update_reply_def set_object_def get_object_def cur_tcb_def tcb_at_def get_tcb_def) + +lemma update_reply_cur_sc_tcb[wp]: + "update_reply ptr f \cur_sc_tcb\" + by (wpsimp simp: update_reply_def set_object_def get_object_def cur_sc_tcb_def sc_tcb_sc_at_def obj_at_def) + end diff --git a/proof/invariant-abstract/RISCV64/ArchCSpace_AI.thy b/proof/invariant-abstract/RISCV64/ArchCSpace_AI.thy index 8d7e5a762a..1b88e34d2e 100644 --- a/proof/invariant-abstract/RISCV64/ArchCSpace_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchCSpace_AI.thy @@ -503,7 +503,7 @@ lemma is_cap_simps': "is_ntfn_cap cap = (\r b R. cap = cap.NotificationCap r b R)" "is_zombie cap = (\r b n. cap = cap.Zombie r b n)" "is_arch_cap cap = (\a. cap = cap.ArchObjectCap a)" - "is_reply_cap cap = (\x R. cap = cap.ReplyCap x R)" + "is_reply_cap cap = (\x. cap = cap.ReplyCap x)" "is_sched_context_cap cap = (\x n. cap = cap.SchedContextCap x n)" "is_nondevice_page_cap cap = (\ u v w x. cap = ArchObjectCap (FrameCap u v w False x))" by (cases cap, auto simp: is_zombie_def is_arch_cap_def is_nondevice_page_cap_def diff --git a/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy b/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy index c456a81654..363b4ac631 100644 --- a/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy @@ -132,7 +132,7 @@ lemma invoke_irq_handler_invs'[Interrupt_AI_asms]: (\s. cte_wp_at (is_derived (cdt s) src cap) src s) and (\s. cte_wp_at (\cap'. \irq\cap_irqs cap - cap_irqs cap'. irq_issued irq s) src s) and - (\s. \t R. cap = ReplyCap t R \ + (\s. \t. cap = ReplyCap t \ st_tcb_at awaiting_reply t s \ \ has_reply_cap t s))\ cap_insert cap src dest \\rv s. invs s \ ex_inv s\" apply wp diff --git a/proof/invariant-abstract/RISCV64/ArchIpc_AI.thy b/proof/invariant-abstract/RISCV64/ArchIpc_AI.thy index 30173693c3..bea6b47c32 100644 --- a/proof/invariant-abstract/RISCV64/ArchIpc_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchIpc_AI.thy @@ -30,7 +30,7 @@ lemma update_cap_data_closedform: | DomainCap \ DomainCap | UntypedCap dev p n idx \ UntypedCap dev p n idx | NullCap \ NullCap - | ReplyCap t rights \ ReplyCap t rights + | ReplyCap t \ ReplyCap t | SchedContextCap s n \ SchedContextCap s n | SchedControlCap \ SchedControlCap | IRQControlCap \ IRQControlCap diff --git a/proof/invariant-abstract/RISCV64/ArchKHeap_AI.thy b/proof/invariant-abstract/RISCV64/ArchKHeap_AI.thy index 712561e98d..85f7bed694 100644 --- a/proof/invariant-abstract/RISCV64/ArchKHeap_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchKHeap_AI.thy @@ -860,6 +860,15 @@ lemma update_sched_context_hyp_refs_of[wp]: split: kernel_object.splits) done +lemma update_reply_hyp_refs_of[wp]: + "update_reply ptr f \\s. P (state_hyp_refs_of s)\" + apply (wpsimp simp: update_reply_def wp: set_object_wp get_object_wp) + apply (clarsimp elim!: rsubst[where P=P]) + apply (rule all_ext) + apply (clarsimp simp: state_hyp_refs_of_def obj_at_def hyp_refs_of_def + split: kernel_object.splits) + done + lemma update_valid_tcb[simp]: "\f. valid_tcb ptr tcb (release_queue_update f s) = valid_tcb ptr tcb s" "\f. valid_tcb ptr tcb (reprogram_timer_update f s) = valid_tcb ptr tcb s" diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index 182e4c001f..d5e92c797e 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -207,7 +207,7 @@ where | "valid_invocation (InvokeNotification w w2) = (ntfn_at w and ex_nonz_cap_to w)" | "valid_invocation (InvokeTCB i) = tcb_inv_wf i" | "valid_invocation (InvokeDomain thread domain) = (tcb_at thread and (\s. thread \ idle_thread s))" -| "valid_invocation (InvokeReply reply grant) = (reply_at reply and ex_nonz_cap_to reply)" +| "valid_invocation (InvokeReply reply) = (reply_at reply and ex_nonz_cap_to reply)" | "valid_invocation (InvokeIRQControl i) = irq_control_inv_valid i" | "valid_invocation (InvokeIRQHandler i) = irq_handler_inv_valid i" | "valid_invocation (InvokeCNode i) = valid_cnode_inv i" diff --git a/proof/invariant-abstract/TcbAcc_AI.thy b/proof/invariant-abstract/TcbAcc_AI.thy index 8f51839263..86b47942ad 100644 --- a/proof/invariant-abstract/TcbAcc_AI.thy +++ b/proof/invariant-abstract/TcbAcc_AI.thy @@ -1887,7 +1887,7 @@ lemma set_tcb_sched_context_valid_ioc[wp]: if_split_asm) done -crunch set_thread_state, update_sched_context +crunch set_thread_state, update_sched_context, update_reply for valid_ioports[wp]: valid_ioports (wp: valid_ioports_lift) diff --git a/proof/refine/RISCV64/ADT_H.thy b/proof/refine/RISCV64/ADT_H.thy index 6f953fe3e9..01cbef0c9f 100644 --- a/proof/refine/RISCV64/ADT_H.thy +++ b/proof/refine/RISCV64/ADT_H.thy @@ -133,8 +133,8 @@ fun CapabilityMap :: "capability \ cap" where cap.CNodeCap ref n (bin_to_bl l (uint L))" | "CapabilityMap (capability.ThreadCap ref) = cap.ThreadCap ref" | "CapabilityMap capability.DomainCap = cap.DomainCap" -| "CapabilityMap (capability.ReplyCap ref gr) = - cap.ReplyCap ref {x. gr \ x = AllowGrant \ x = AllowWrite}" +| "CapabilityMap (capability.ReplyCap ref) = + cap.ReplyCap ref" | "CapabilityMap (SchedContextCap sc n) = cap.SchedContextCap sc (n - min_sched_context_bits)" | "CapabilityMap SchedControlCap = cap.SchedControlCap" | "CapabilityMap capability.IRQControlCap = cap.IRQControlCap" @@ -156,13 +156,11 @@ fun CapabilityMap :: "capability \ cap" where lemma cap_relation_imp_CapabilityMap: "\wellformed_cap c; cap_relation c c'\ \ CapabilityMap c' = c" apply (case_tac c; simp add: wellformed_cap_simps) - apply (rule set_eqI, clarsimp) - apply (case_tac "x", simp_all) apply (rule set_eqI, clarsimp) - apply (case_tac "x", simp_all add: word_bits_def) - apply clarsimp - apply (simp add: set_eq_iff, rule allI) - apply (case_tac x; clarsimp) + apply (case_tac "x", simp_all) + apply (rule set_eqI, clarsimp) + apply (case_tac "x", simp_all add: word_bits_def) + apply clarsimp apply (simp add: uint_of_bl_is_bl_to_bin bl_bin_bl[simplified]) apply (simp add: zbits_map_def split: option.splits) apply (rename_tac arch_cap) @@ -293,7 +291,7 @@ definition scMap :: "(obj_ref \ obj_ref) \ sched_con \" definition replyMap :: "reply \ Structures_A.reply" where - "replyMap r = \ reply_tcb = replyTCB r, reply_sc = replySC r \" + "replyMap r = \ reply_tcb = replyTCB r, reply_sc = replySC r, reply_can_grant = replyCanGrant r \" definition absHeap :: "(machine_word \ vmpage_size) \ (machine_word \ nat) \ diff --git a/proof/refine/RISCV64/Bits_R.thy b/proof/refine/RISCV64/Bits_R.thy index bd9054cff3..7ca2d44eef 100644 --- a/proof/refine/RISCV64/Bits_R.thy +++ b/proof/refine/RISCV64/Bits_R.thy @@ -55,7 +55,7 @@ lemma isCap_simps: "isNotificationCap v = (\v0 v1 v2 v3. v = NotificationCap v0 v1 v2 v3)" "isEndpointCap v = (\v0 v1 v2 v3 v4 v5. v = EndpointCap v0 v1 v2 v3 v4 v5)" "isUntypedCap v = (\d v0 v1 f. v = UntypedCap d v0 v1 f)" - "isReplyCap v = (\v0 v1. v = ReplyCap v0 v1)" + "isReplyCap v = (\v0. v = ReplyCap v0)" "isSchedContextCap v = (\v0 v1. v = SchedContextCap v0 v1)" "isSchedControlCap v = (v = SchedControlCap)" "isIRQControlCap v = (v = IRQControlCap)" @@ -163,7 +163,7 @@ lemma capAligned_tcbI: done lemma capAligned_replyI: - "reply_at' p s \ capAligned (ReplyCap p r)" + "reply_at' p s \ capAligned (ReplyCap p)" apply (clarsimp simp: obj_at'_real_def capAligned_def objBits_simps word_bits_def capUntypedPtr_def isCap_simps) apply (fastforce dest: ko_wp_at_norm diff --git a/proof/refine/RISCV64/CSpace_I.thy b/proof/refine/RISCV64/CSpace_I.thy index 2076b96bda..9f3dfb41b8 100644 --- a/proof/refine/RISCV64/CSpace_I.thy +++ b/proof/refine/RISCV64/CSpace_I.thy @@ -539,7 +539,7 @@ definition capMasterCap :: "capability \ capability" where | NotificationCap ref bdg s r \ NotificationCap ref 0 True True | CNodeCap ref bits gd gs \ CNodeCap ref bits 0 0 | ThreadCap ref \ ThreadCap ref - | ReplyCap ref g \ ReplyCap ref True + | ReplyCap ref \ ReplyCap ref | UntypedCap d ref n f \ UntypedCap d ref n 0 | ArchObjectCap acap \ ArchObjectCap (case acap of FrameCap ref rghts sz d mapdata \ @@ -580,8 +580,8 @@ lemma capMasterCap_eqDs1: \ cap = Zombie ref tp n" "capMasterCap cap = UntypedCap d ref bits 0 \ \f. cap = UntypedCap d ref bits f" - "capMasterCap cap = ReplyCap ref g - \ g \ (\g. cap = ReplyCap ref g)" + "capMasterCap cap = ReplyCap ref + \ cap = ReplyCap ref" "capMasterCap cap = ArchObjectCap (FrameCap ref rghts sz d mapdata) \ rghts = VMReadWrite \ mapdata = None \ (\rghts mapdata. cap = ArchObjectCap (FrameCap ref rghts sz d mapdata))" @@ -617,7 +617,7 @@ lemma capBadge_simps[simp]: "capBadge (ArchObjectCap cap) = None" "capBadge (IRQControlCap) = None" "capBadge (IRQHandlerCap irq) = None" - "capBadge (ReplyCap tcb g) = None" + "capBadge (ReplyCap tcb) = None" by (simp add: capBadge_def isCap_defs)+ lemma capClass_Master: @@ -779,7 +779,7 @@ lemma capUntypedSize_simps [simp]: "capUntypedSize (ArchObjectCap x) = Arch.capUntypedSize x" "capUntypedSize (UntypedCap d r n f) = 1 << n" "capUntypedSize (CNodeCap r n g n2) = 1 << (objBits (undefined::cte) + n)" - "capUntypedSize (ReplyCap r a) = 1 << objBits (undefined :: reply)" + "capUntypedSize (ReplyCap r) = 1 << objBits (undefined :: reply)" "capUntypedSize (SchedContextCap sc sz) = 1 << sz" "capUntypedSize SchedControlCap = 1" "capUntypedSize IRQControlCap = 1" diff --git a/proof/refine/RISCV64/Finalise_R.thy b/proof/refine/RISCV64/Finalise_R.thy index a341e510da..fe0d6293d9 100644 --- a/proof/refine/RISCV64/Finalise_R.thy +++ b/proof/refine/RISCV64/Finalise_R.thy @@ -1799,7 +1799,7 @@ where "final_matters' cap \ case cap of EndpointCap ref bdg s r g gr \ True | NotificationCap ref bdg s r \ True - | ReplyCap ref gr \ True + | ReplyCap ref \ True | ThreadCap ref \ True | SchedContextCap ref sz \ True | CNodeCap ref bits gd gs \ True @@ -3026,7 +3026,7 @@ crunch replyClear (wp: crunch_wps simp: crunch_simps ignore: threadSet) lemma finaliseCapTrue_standin_bound_tcb_at': - "\\s. bound_tcb_at' P t s \ (\tt r. cap = ReplyCap tt r) \ + "\\s. bound_tcb_at' P t s \ (\tt. cap = ReplyCap tt) \ finaliseCapTrue_standin cap final \\_. bound_tcb_at' P t\" apply (case_tac cap; simp add: finaliseCapTrue_standin_def isCap_simps) @@ -4253,7 +4253,7 @@ lemma fast_finaliseCap_corres: apply (clarsimp simp: valid_cap'_def) (* ReplyCap *) apply clarsimp - apply (rename_tac rptr rs) + apply (rename_tac rptr) apply (add_sym_refs, add_valid_replies rptr simp: valid_cap_def, add_sch_act_wf) apply (rule corres_stateAssert_assume; (simp add: sym_refs_asrt_def)?) apply (rule corres_stateAssert_assume; simp?) diff --git a/proof/refine/RISCV64/Invariants_H.thy b/proof/refine/RISCV64/Invariants_H.thy index 26e11faccc..5f07dabf7d 100644 --- a/proof/refine/RISCV64/Invariants_H.thy +++ b/proof/refine/RISCV64/Invariants_H.thy @@ -405,7 +405,7 @@ fun zobj_refs' :: "capability \ obj_ref set" where | "zobj_refs' (NotificationCap r _ _ _) = {r}" | "zobj_refs' (ThreadCap r) = {r}" | "zobj_refs' (SchedContextCap r _) = {r}" -| "zobj_refs' (ReplyCap r _) = {r}" +| "zobj_refs' (ReplyCap r) = {r}" | "zobj_refs' _ = {}" definition ex_nonz_cap_to' :: "obj_ref \ kernel_state \ bool" where @@ -463,7 +463,7 @@ primrec capBits :: "capability \ nat" where | "capBits (Zombie _ z _) = zBits z" | "capBits (IRQControlCap) = 0" | "capBits (IRQHandlerCap _) = 0" -| "capBits (ReplyCap tcb m) = objBits (undefined :: reply)" +| "capBits (ReplyCap tcb) = objBits (undefined :: reply)" | "capBits (SchedContextCap sc n) = n" | "capBits SchedControlCap = 0" | "capBits (ArchObjectCap x) = acapBits x" @@ -569,7 +569,7 @@ where valid_cap'_def: bits \ 0 \ bits + guard_sz \ word_bits \ guard && mask guard_sz = guard \ (\addr. real_cte_at' (r + 2^cteSizeBits * (addr && mask bits)) s) | ThreadCap r \ tcb_at' r s - | ReplyCap r m \ reply_at' r s + | ReplyCap r \ reply_at' r s | IRQControlCap \ True | IRQHandlerCap irq \ irq \ maxIRQ \ irq \ irqInvalid | SchedControlCap \ True @@ -830,7 +830,7 @@ where | "capClass (IRQControlCap) = IRQClass" | "capClass (SchedControlCap) = SchedControlClass" | "capClass (IRQHandlerCap irq) = IRQClass" -| "capClass (ReplyCap tcb m) = PhysicalClass" +| "capClass (ReplyCap tcb) = PhysicalClass" | "capClass (ArchObjectCap cap) = acapClass cap" definition diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy index f0ac9a59df..6206a97df8 100644 --- a/proof/refine/RISCV64/IpcCancel_R.thy +++ b/proof/refine/RISCV64/IpcCancel_R.thy @@ -1042,6 +1042,15 @@ crunch updateReply, setSchedContext, updateSchedContext and valid_sched_pointers[wp]: valid_sched_pointers (simp: crunch_simps opt_map_Some_eta_fold wp: crunch_wps) +lemma updateReply_replyCanGrant_projs[wp]: + "updateReply rptr (replyCanGrant_update f) + \\s. P (tcbSCs_of s) (scTCBs_of s) (scReplies_of s) (replyNexts_of s) (replyPrevs_of s) (replyTCBs_of s) (replySCs_of s)\" + unfolding updateReply_def + apply (wpsimp | wps)+ + apply (erule rsubst4[where P="P (tcbSCs_of s) (scTCBs_of s) (scReplies_of s) " for s]) + apply (clarsimp simp: ext opt_map_def obj_at'_def)+ + done + lemma scReplies_of_scTCB_update[simp]: "\ ko_at' sc scp s\ \ P (\a. if a = scp then scReply (scTCB_update (\_. Some tp) sc) else scReplies_of s a) diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index 9b321d418f..b37f27af1b 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -2026,12 +2026,19 @@ crunch update_sk_obj_ref lemma update_sched_context_in_correct_ready_q[wp]: "update_sched_context ptr f \in_correct_ready_q\" - unfolding update_sched_context_def set_simple_ko_def get_simple_ko_def + unfolding update_sched_context_def apply (wpsimp wp: set_object_wp get_object_wp) apply (clarsimp simp: vs_all_heap_simps obj_at_kh_kheap_simps in_correct_ready_q_def) apply (fastforce simp: pred_map_def map_project_def opt_map_def tcbs_of_kh_def) done +lemma update_reply_in_correct_ready_q[wp]: + "update_reply ptr f \in_correct_ready_q\" + unfolding update_reply_def + apply (wpsimp wp: set_object_wp get_object_wp) + apply (clarsimp simp: vs_all_heap_simps obj_at_kh_kheap_simps in_correct_ready_q_def) + done + crunch bind_sc_reply for release_queue[wp]: "\s. P (release_queue s)" and in_correct_ready_q[wp]: in_correct_ready_q @@ -2049,7 +2056,7 @@ lemma sched_context_donate_in_correct_ready_q[wp]: apply (wpsimp wp: thread_set_in_correct_ready_q) done -crunch thread_set, update_sched_context +crunch update_sched_context, update_reply for ready_qs_distinct[wp]: ready_qs_distinct (wp: ready_qs_distinct_lift) @@ -5205,7 +5212,7 @@ crunch doIPCTransfer definition receiveIPC_preamble where "receiveIPC_preamble replyCap thread \ case replyCap of NullCap \ return Nothing - | ReplyCap r _ \ + | ReplyCap r \ (do tptrOpt <- liftM replyTCB (getReply (r)); when (tptrOpt \ Nothing \ tptrOpt \ Some thread) $ cancelIPC (the tptrOpt); return (Just r) @@ -5299,7 +5306,7 @@ lemma ri_preamble_not_in_sc: lemma receiveIPC_corres_helper: "(do replyOpt <- case replyCap of capability.NullCap \ return Nothing - | capability.ReplyCap r v18 \ return (Just r) + | capability.ReplyCap r \ return (Just r) | _ \ haskell_fail []; y <- when (\y. replyOpt = Some y) @@ -5310,7 +5317,7 @@ lemma receiveIPC_corres_helper: f replyOpt od) = (do replyOpt <- case replyCap of capability.NullCap \ return Nothing - | capability.ReplyCap r _ \ + | capability.ReplyCap r \ (do tptrOpt <- liftM replyTCB (getReply (r)); when (tptrOpt \ Nothing \ tptrOpt \ Some thread) $ cancelIPC (the tptrOpt); return (Just r) @@ -5343,6 +5350,18 @@ crunch ifCondRefillUnblockCheck for reply_projs[wp]: "\s. P (replyNexts_of s) (replyPrevs_of s) (replyTCBs_of s) (replySCs_of s)" (wp: crunch_wps simp: crunch_simps) +lemma replyCanGrant_update_valid_replies'_sc_asrt[wp]: + shows "updateReply ptr (replyCanGrant_update f) \valid_replies'_sc_asrt ptr\" + apply (rule valid_replies'_sc_asrt_lift; wpsimp wp: updateReply_wp_all) + apply (subst opt_map_upd_triv) + apply (clarsimp simp: opt_map_def obj_at'_def) + apply clarsimp + apply (subst opt_map_upd_triv) + apply (clarsimp simp: opt_map_def obj_at'_def) + apply clarsimp + apply (fastforce simp: pred_tcb_at'_def obj_at'_def) + done + lemma receiveIPC_corres: assumes "is_ep_cap cap" and "cap_relation cap cap'" and "cap_relation reply_cap replyCap" and "is_reply_cap reply_cap \ (reply_cap = cap.NullCap)" @@ -5408,13 +5427,14 @@ lemma receiveIPC_corres: apply (simp add: ep_relation_def) apply (fold dc_def)[1] apply (rule corres_guard_imp) - apply (case_tac isBlocking; simp) + apply (corres_cases; clarsimp) apply (rule corres_split[OF setThreadState_corres], simp) apply (rule corres_split[OF corres_when setEndpoint_corres], clarsimp) - apply (rule replyTCB_update_corres) + apply (rule corres_split[OF replyTCB_update_corres]) + apply (rule replyCanGrant_update_corres, simp) + apply wpsimp+ prefer 6 \ \ defer wp until corres complete \ - apply (rule corres_guard_imp, rule doNBRecvFailedTransfer_corres, clarsimp) - apply simp + apply (rule doNBRecvFailedTransfer_corres) apply (simp add: ep_relation_def) \ \ corres logic done \ apply wpsimp+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def @@ -5461,6 +5481,7 @@ lemma receiveIPC_corres: and valid_sched_pointers and valid_objs' and valid_bound_obj' valid_replies'_sc_asrt replyOpt + and valid_bound_reply' replyOpt and pspace_aligned' and pspace_distinct' and pspace_bounded' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)" @@ -5468,16 +5489,20 @@ lemma receiveIPC_corres: apply (simp add: fault_rel_optionation_def) apply (rule corres_if2) apply simp - apply (rule corres_split_eqr[OF threadGet_corres replyPush_corres]) + apply (rule corres_split_eqr[OF threadGet_corres]) apply (clarsimp simp: tcb_relation_def) - apply (clarsimp simp: fault_rel_optionation_def split: option.splits) - prefer 3 \ \ defer wp until corres complete \ - apply (rule setThreadState_corres, simp) - prefer 3 \ \ defer wp until corres complete \ - apply (rule corres_split[OF setThreadState_corres], simp) - apply (rule possibleSwitchTo_corres, simp) - apply (wpsimp wp: set_thread_state_valid_sched_action) - apply wpsimp + apply (rule corres_split[OF replyCanGrant_update_corres replyPush_corres]) + apply simp + apply (clarsimp simp: fault_rel_optionation_def split: option.splits) + prefer 5 \ \ defer wp until corres complete \ + apply (rule setThreadState_corres, simp) + prefer 5 \ \ defer wp until corres complete \ + apply (rule corres_split[OF setThreadState_corres], simp) + apply (rule possibleSwitchTo_corres, simp) + apply (wpsimp wp: set_thread_state_valid_sched_action) + apply wpsimp + apply wpsimp + apply (wpsimp wp: updateReply_valid_objs') apply wpsimp apply wpsimp apply clarsimp @@ -5496,11 +5521,10 @@ lemma receiveIPC_corres: apply (fastforce elim!: pred_tcb_weakenE simp: is_blocked_on_send_def) apply (frule valid_sched_action_weak_valid_sched_action) apply (clarsimp simp: valid_sched_def split: if_splits cong: conj_cong) - apply fastforce + subgoal by (fastforce simp: reply_at_ppred_reply_at) apply (fastforce simp: image_def) apply (clarsimp, frule valid_objs'_valid_tcbs') - apply (clarsimp simp: valid_sched_def split: if_splits - cong: conj_cong) + apply (clarsimp simp: valid_reply'_def split: if_splits) apply (case_tac replyOpt; simp) apply wpsimp apply wpsimp @@ -5565,11 +5589,11 @@ lemma receiveIPC_corres: valid_objs' s \ pspace_aligned' s \ pspace_distinct' s \ pspace_bounded' s \ - valid_bound_obj' valid_replies'_sc_asrt replyOpt - s \ + valid_bound_obj' valid_replies'_sc_asrt replyOpt s \ + valid_bound_reply' replyOpt s \ sch_act_wf (ksSchedulerAction s) s)" in hoare_strengthen_post[rotated]) - apply (clarsimp simp: sch_act_wf_weak obj_at'_def split: option.split) + apply (clarsimp simp: sch_act_wf_weak split: option.split) apply (wpsimp wp: valid_replies'_sc_asrt_lift valid_bound_obj'_lift) apply (wpsimp wp: gts_st_tcb_at) apply wpsimp @@ -5604,7 +5628,10 @@ lemma receiveIPC_corres: apply (case_tac isBlocking; simp) apply (rule corres_split[OF setThreadState_corres], simp) apply (rule corres_split [where r=dc]) - apply (rule corres_when[OF _ replyTCB_update_corres], simp) + apply (rule corres_when, simp) + apply (rule corres_split[OF replyTCB_update_corres]) + apply (rule replyCanGrant_update_corres, simp) + apply wpsimp+ apply (rule corres_split[OF tcbEPAppend_corres setEndpoint_corres]) apply (simp add: ep_relation_def) apply (wpsimp wp: hoare_vcg_ball_lift)+ @@ -6641,7 +6668,7 @@ lemma ri_invs' [wp]: apply (drule_tac ko="ko :: endpoint" for ko in sym_refs_ko_atD'[rotated]) apply (fastforce simp: obj_at'_def) apply (fastforce simp: ep_q_refs_of'_def refs_of_rev' ko_wp_at'_def split: endpoint.splits) - apply (prop_tac "\r g. replyCap = ReplyCap r g \ \obj_at' (\a. replyTCB a = Some t) r s") + apply (prop_tac "\r. replyCap = ReplyCap r \ \obj_at' (\a. replyTCB a = Some t) r s") apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) apply (drule_tac ko="ko :: reply" for ko in sym_refs_ko_atD'[rotated]) apply (fastforce simp: obj_at'_def) diff --git a/proof/refine/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy index e1efe240eb..56fc8237ef 100644 --- a/proof/refine/RISCV64/KHeap_R.thy +++ b/proof/refine/RISCV64/KHeap_R.thy @@ -1862,6 +1862,14 @@ lemma getReply_TCB_corres: apply (clarsimp simp: reply_relation_def) done +lemma getReply_canGrant_corres: + "corres (=) (reply_at ptr) (reply_at' ptr) + (get_reply_can_grant ptr) (liftM replyCanGrant (getReply ptr))" + apply clarsimp + apply (rule get_reply_corres[THEN corres_rel_imp]) + apply (clarsimp simp: reply_relation_def) + done + lemma get_sc_corres: "corres (\sc sc'. \n. sc_relation sc n sc') (sc_at ptr) (sc_at' ptr) (get_sched_context ptr) (getSchedContext ptr)" @@ -4625,6 +4633,174 @@ lemma updateSchedContext_no_stack_update_corres: (* end : updateSchedContext *) +(* updateReply *) + +lemma no_fail_setReply [wp]: + "no_fail (reply_at' p) (setReply p reply)" + unfolding setReply_def + by (wpsimp simp: objBits_simps) + +lemma no_fail_updateReply [wp]: + "no_fail (reply_at' rp) (updateReply rp f)" + unfolding updateReply_def by wpsimp + +lemma setReply_replyPrev_same_corres: (* for reply update that doesn't touch the reply stack *) + assumes R': "reply_relation reply reply'" + shows + "corres dc + \ + (obj_at' (\k::reply. objBits k = objBits reply') ptr + and obj_at' (\ko. replyPrev_same reply' ko) ptr) + (set_object ptr (kernel_object.Reply reply)) (setReply ptr reply')" + proof - + have z: "\s. reply_at' ptr s + \ map_to_ctes ((ksPSpace s) (ptr \ injectKO reply')) = map_to_ctes (ksPSpace s)" + by (clarsimp simp: obj_at_simps) + show ?thesis + apply (insert R') + apply (clarsimp simp: setReply_def) + apply (rule corres_no_failI) + apply (rule no_fail_pre) + apply wp + apply clarsimp + apply clarsimp + apply clarsimp + apply (rename_tac s s' rv; prop_tac "reply_at ptr s") + apply (fastforce intro!: reply_at'_cross + simp: obj_at'_def) + apply (clarsimp simp: obj_at_def is_reply obj_at'_def) + apply (unfold set_object_def setObject_def) + apply (clarsimp simp: in_monad split_def bind_def gets_def get_def Bex_def + put_def return_def modify_def get_object_def2 + obj_at_def a_type_def updateObject_default_def in_magnitude_check[OF _] + split: Structures_A.kernel_object.splits) + apply (prop_tac "obj_at (same_caps (kernel_object.Reply reply)) ptr s") + apply (clarsimp simp: obj_at_def is_reply) + apply (clarsimp simp: state_relation_def + z[simplified obj_at'_def is_reply projectKO_eq projectKO_opts_defs, simplified]) + apply (clarsimp simp: caps_of_state_after_update cte_wp_at_after_update + swp_def fun_upd_def obj_at_def is_reply) + apply (subst conj_assoc[symmetric]) + apply (extract_conjunct \match conclusion in "ghost_relation _ _ _" \ -\) + apply (clarsimp simp: ghost_relation_def) + apply (erule_tac x=ptr in allE)+ + apply (clarsimp simp: obj_at_def a_type_def + split: Structures_A.kernel_object.splits if_split_asm) + apply (extract_conjunct \match conclusion in "pspace_relation _ _" \ -\) + apply (fold fun_upd_def) + apply (simp only: pspace_relation_def simp_thms + pspace_dom_update[where x="kernel_object.Reply _" + and v="kernel_object.Reply _", + simplified a_type_def, simplified]) + apply (simp only: dom_fun_upd2 simp_thms) + apply (elim conjE) + apply (frule bspec, erule domI) + apply (rule ballI, drule(1) bspec) + apply (drule domD) + apply (clarsimp simp: project_inject split: if_split_asm kernel_object.split_asm) + apply (rename_tac reply0 obj x bb aa ba) + apply (drule_tac x="(aa, ba)" in bspec, simp) + apply clarsimp + apply (frule_tac ko'="kernel_object.Reply reply0" and x'=ptr + in obj_relation_cut_same_type) + apply simp+ + apply (clarsimp simp: a_type_def split: Structures_A.kernel_object.split_asm if_split_asm) + apply (extract_conjunct \match conclusion in "sc_replies_relation_2 _ _ _" \ -\) + apply (clarsimp simp: sc_replies_relation_def sc_replies_of_scs_def map_project_def scs_of_kh_def) + apply (drule_tac x=p in spec) + subgoal + by (subst replyPrevs_of_replyPrev_same_update[simplified, where ob'=reply', simplified]; + simp add: typ_at'_def ko_wp_at'_def obj_at'_def project_inject opt_map_def) + by (auto simp: opt_map_def projectKO_opts_defs) + qed + +lemma setReply_update_corres_Q: + assumes R': "\reply_relation reply reply'; Q reply; Q' reply'\ + \ reply_relation (f reply) (f' (reply'::reply))" + and RP_same: "replyPrev_same (f' reply') reply'" + shows + "corres dc + (\s. kheap s ptr = Some (kernel_object.Reply reply) \ Q reply) + (obj_at' (\obj. obj = reply' \ Q' reply') ptr) + (set_object ptr (kernel_object.Reply (f reply))) + (setReply ptr (f' reply'))" + apply (insert R') + apply (rule_tac F="reply_relation reply reply' \ Q reply \ Q' reply'" in corres_req) + apply (drule state_relation_pspace_relation) + apply clarsimp + apply (drule (1) pspace_relation_absD) + apply (clarsimp simp: obj_at'_def split: if_split_asm) + apply (rule corres_guard_imp) + apply (rule setReply_replyPrev_same_corres) + apply fastforce + apply clarsimp + apply (clarsimp simp: obj_at'_def objBits_simps RP_same) + done + +lemmas setReply_update_corres = setReply_update_corres_Q[where Q=\ and Q'=\, simplified] + +lemma updateReply_corres_Q: + "\\reply reply'. \reply_relation reply reply'; Q reply; Q' reply'\ \ reply_relation (f reply) (f' reply'); + \reply'. replyPrev_same (f' reply') reply'\ \ + corres dc + (\s. \reply. kheap s ptr = Some (kernel_object.Reply reply) \ Q reply) + (\s'. \reply'. ko_at' reply' ptr s' \ Q' reply') + (update_reply ptr f) (updateReply ptr f')" + apply (clarsimp simp: update_reply_def) + apply (rule corres_symb_exec_l[rotated 2, OF get_object_sp]) + apply (find_goal \match conclusion in "\P\ f \\Q\" for P f Q \ -\) + apply (fastforce intro: get_object_exs_valid + simp: obj_at_def) + apply wpsimp + apply (clarsimp simp: obj_at_def) + apply (rename_tac obj) + apply (case_tac obj; + clarsimp, (solves \clarsimp simp: obj_at_def is_sc_obj_def corres_underlying_def\)?) + apply (clarsimp simp: pred_conj_def) + apply (rule abs_ex_lift_corres) + apply clarsimp + apply (rule corres_underlying_lift_ex2') + apply (rule_tac F="reply_relation reply reply' \ Q reply \ Q' reply'" in corres_req) + apply (drule state_relation_pspace_relation) + apply clarsimp + apply (drule (1) pspace_relation_absD) + apply (clarsimp simp: obj_at'_def split: if_split_asm) + apply (clarsimp simp: updateReply_def) + apply (rule corres_symb_exec_r) + apply (rule corres_guard_imp) + apply (rule_tac f=f and f'="f'" and Q=Q and Q'=Q' + in setReply_update_corres_Q; + simp?) + apply (clarsimp simp: obj_at_def) + apply fastforce + apply wpsimp + apply (clarsimp simp: obj_at'_def) + apply wpsimp + apply wpsimp + apply (clarsimp simp: obj_at'_def) + done + +lemma updateReply_corres: + "\\reply reply'. reply_relation reply reply' \ reply_relation (f reply) (f' reply'); + \reply'. replyPrev_same (f' reply') reply'\ \ + corres dc (reply_at ptr) (reply_at' ptr) (update_reply ptr f) (updateReply ptr f')" + apply (corres corres: updateReply_corres_Q[where f=f and f'=f' and Q=\ and Q'=\]) + apply (clarsimp simp: obj_at_def is_reply) + apply (clarsimp simp: obj_at'_def) + done + +lemma replyCanGrant_update_corres: + "\\can_grant canGrant. can_grant = canGrant \ f can_grant = f' canGrant\ \ + corres dc (reply_at ptr) (reply_at' ptr) (update_reply ptr (reply_can_grant_update f)) (updateReply ptr (replyCanGrant_update f'))" + apply (corres corres: updateReply_corres_Q[where Q=\ and Q'=\]) + apply (simp add: reply_relation_def) + apply (simp add: replyPrev_same_def) + apply (clarsimp simp: obj_at_def is_reply) + apply (clarsimp simp: obj_at'_def) + done + +(* end : updateReply *) + end (* this lets cross the sc size information from concrete to abstract *) diff --git a/proof/refine/RISCV64/Reply_R.thy b/proof/refine/RISCV64/Reply_R.thy index 0e450dd1d4..134ec34a3b 100644 --- a/proof/refine/RISCV64/Reply_R.thy +++ b/proof/refine/RISCV64/Reply_R.thy @@ -894,6 +894,16 @@ lemma updateReply_replyTCB_invs': split: option.split_asm) by (auto simp: obj_at'_def opt_map_def) +lemma updateReply_replyCanGrant_invs'[wp]: + "updateReply rptr (replyCanGrant_update f) \invs'\" + apply (simp only: invs'_def valid_pspace'_def) + apply (wpsimp wp: updateReply_valid_objs' updateReply_iflive' updateReply_valid_replies' updateReply_list_refs_of_replies') + apply (clarsimp simp: valid_replies'_def2 valid_reply'_def live_reply'_def + dest: pspace_alignedD' pspace_distinctD') + apply (erule delta_sym_refs) + by (auto simp: list_refs_of_reply'_def map_set_def opt_map_def obj_at'_def + split: option.splits if_splits) + lemma bindScReply_valid_objs'[wp]: "\valid_objs' and reply_at' replyPtr\ bindScReply scp replyPtr @@ -1071,15 +1081,6 @@ lemma sym_refs_replySCs_of_None: crunch cleanReply for valid_tcbs'[wp]: valid_tcbs' -lemma no_fail_setReply [wp]: - "no_fail (reply_at' p) (setReply p reply)" - unfolding setReply_def - by (wpsimp simp: objBits_simps) - -lemma no_fail_updateReply [wp]: - "no_fail (reply_at' rp) (updateReply rp f)" - unfolding updateReply_def by wpsimp - lemma no_fail_cleanReply [wp]: "no_fail (reply_at' rp) (cleanReply rp)" unfolding cleanReply_def diff --git a/proof/refine/RISCV64/StateRelation.thy b/proof/refine/RISCV64/StateRelation.thy index 722421cafa..01f00e79c6 100644 --- a/proof/refine/RISCV64/StateRelation.thy +++ b/proof/refine/RISCV64/StateRelation.thy @@ -83,8 +83,8 @@ primrec cap_relation :: "cap \ capability \ bool" where (c = Structures_H.CNodeCap ref n (of_bl L) (length L))" | "cap_relation (Structures_A.ThreadCap ref) c = (c = Structures_H.ThreadCap ref)" -| "cap_relation (Structures_A.ReplyCap ref r) c = (c = - Structures_H.ReplyCap ref (AllowGrant \ r))" +| "cap_relation (Structures_A.ReplyCap ref) c = (c = + Structures_H.ReplyCap ref)" | "cap_relation (Structures_A.SchedContextCap ref n) c = (c = Structures_H.SchedContextCap ref (min_sched_context_bits + n))" | "cap_relation (Structures_A.SchedControlCap) c = (c = @@ -290,7 +290,7 @@ lemma maxReleaseTime_equiv: definition reply_relation :: "Structures_A.reply \ Structures_H.reply \ bool" where "reply_relation \ \reply reply'. - reply_sc reply = replySC reply' \ reply_tcb reply = replyTCB reply'" + reply_sc reply = replySC reply' \ reply_tcb reply = replyTCB reply' \ reply_can_grant reply = replyCanGrant reply'" \ \ A pair of objects @{term "(obj, obj')"} should satisfy the following relation when, under further diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 1a7c2074a8..6ce6e88e9e 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -88,8 +88,8 @@ where (x = InvokeEndpoint w w2 b c)" | "inv_relation (Invocations_A.InvokeNotification w w2) x = (x = InvokeNotification w w2)" -| "inv_relation (Invocations_A.InvokeReply w grant) x = - (x = InvokeReply w grant)" +| "inv_relation (Invocations_A.InvokeReply w) x = + (x = InvokeReply w)" | "inv_relation (Invocations_A.InvokeTCB i) x = (\i'. tcbinv_relation i i' \ x = InvokeTCB i')" | "inv_relation (Invocations_A.InvokeDomain tptr domain) x = @@ -124,7 +124,7 @@ where | "valid_invocation' (InvokeDomain thread domain) = (tcb_at' thread and K (domain \ maxDomain))" | "valid_invocation' (InvokeSchedContext i) = valid_sc_inv' i" | "valid_invocation' (InvokeSchedControl i) = valid_sc_ctrl_inv' i" -| "valid_invocation' (InvokeReply reply grant) = reply_at' reply" +| "valid_invocation' (InvokeReply reply) = reply_at' reply" | "valid_invocation' (InvokeIRQControl i) = irq_control_inv_valid' i" | "valid_invocation' (InvokeIRQHandler i) = irq_handler_inv_valid' i" | "valid_invocation' (InvokeCNode i) = valid_cnode_inv' i" @@ -472,9 +472,11 @@ lemma performInvocation_corres: apply wpsimp+ apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF getCurThread_corres]) - apply (rule corres_split_nor[OF doReplyTransfer_corres]) - apply (rule corres_trivial, simp) - apply wp+ + apply (rule corres_split[OF getReply_canGrant_corres]) + apply clarsimp + apply (rule corres_split_nor[OF doReplyTransfer_corres]) + apply (rule corres_trivial, simp) + apply (wp get_simple_ko_wp)+ apply (clarsimp simp: tcb_at_invs) apply simp apply (clarsimp simp: liftME_def) diff --git a/spec/abstract/CSpace_A.thy b/spec/abstract/CSpace_A.thy index 4d150368bb..8382228afd 100644 --- a/spec/abstract/CSpace_A.thy +++ b/spec/abstract/CSpace_A.thy @@ -320,7 +320,7 @@ fun fast_finalise :: "cap \ bool \ (unit, 'z::state_ext) s_monad" where "fast_finalise NullCap final = return ()" -| "fast_finalise (ReplyCap r _) final = +| "fast_finalise (ReplyCap r) final = (when final $ do tptr \ get_reply_tcb r; case tptr of @@ -476,7 +476,7 @@ fun where "finalise_cap NullCap final = return (NullCap, NullCap)" | "finalise_cap (UntypedCap dev r bits f) final = return (NullCap, NullCap)" -| "finalise_cap (ReplyCap r _) final = +| "finalise_cap (ReplyCap r) final = (liftM (K (NullCap, NullCap)) $ when final $ do tptr \ get_reply_tcb r; case tptr of @@ -533,7 +533,7 @@ where definition can_fast_finalise :: "cap \ bool" where "can_fast_finalise cap \ case cap of - ReplyCap r R \ True + ReplyCap r \ True | EndpointCap r b R \ True | NotificationCap r b R \ True | NullCap \ True @@ -721,7 +721,7 @@ where (is_ntfn_cap c' \ obj_ref_of c' = r)" | "same_region_as (CNodeCap r bits g) c' = (is_cnode_cap c' \ obj_ref_of c' = r \ bits_of c' = bits)" -| "same_region_as (ReplyCap n cr) c' = (\cr'. c' = ReplyCap n cr')" +| "same_region_as (ReplyCap n) c' = (c' = ReplyCap n)" | "same_region_as (ThreadCap r) c' = (is_thread_cap c' \ obj_ref_of c' = r)" | "same_region_as (SchedContextCap sc n) c' = diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index 7e4b4c7ef8..83c1cb570c 100644 --- a/spec/abstract/Decode_A.thy +++ b/spec/abstract/Decode_A.thy @@ -781,8 +781,8 @@ where if AllowSend \ rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 - | ReplyCap reply rights \ - returnOk $ InvokeReply reply (AllowGrant \ rights) + | ReplyCap reply \ + returnOk $ InvokeReply reply | IRQControlCap \ liftME InvokeIRQControl $ decode_irq_control_invocation label args slot (map fst excaps) diff --git a/spec/abstract/Invocations_A.thy b/spec/abstract/Invocations_A.thy index 5f837e5a40..72684511e4 100644 --- a/spec/abstract/Invocations_A.thy +++ b/spec/abstract/Invocations_A.thy @@ -79,7 +79,7 @@ datatype invocation = InvokeUntyped untyped_invocation | InvokeEndpoint obj_ref machine_word bool bool | InvokeNotification obj_ref machine_word - | InvokeReply obj_ref bool + | InvokeReply obj_ref | InvokeTCB tcb_invocation | InvokeDomain obj_ref word8 | InvokeSchedContext sched_context_invocation diff --git a/spec/abstract/Ipc_A.thy b/spec/abstract/Ipc_A.thy index 333157230e..ad49278b1f 100644 --- a/spec/abstract/Ipc_A.thy +++ b/spec/abstract/Ipc_A.thy @@ -367,7 +367,7 @@ where of EndpointCap ref badge rights \ return (ref,rights) | _ \ fail); reply \ (case reply_cap of - ReplyCap r _ \ do + ReplyCap r \ do tptr \ get_reply_tcb r; when (tptr \ None \ the tptr \ thread) $ cancel_ipc (the tptr); return (Some r) @@ -386,16 +386,21 @@ where of IdleEP \ (case is_blocking of True \ do set_thread_state thread (BlockedOnReceive epptr reply \receiver_can_grant = (AllowGrant \ rights)\); - when (reply \ None) $ + when (reply \ None) $ do set_reply_obj_ref reply_tcb_update (the reply) (Some thread); + update_reply (the reply) (reply_can_grant_update (\_. AllowGrant \ rights)) + od; set_endpoint epptr (RecvEP [thread]) od | False \ do_nbrecv_failed_transfer thread) - | RecvEP queue \ (case is_blocking of + | RecvEP queue \ (case is_blocking of True \ do set_thread_state thread (BlockedOnReceive epptr reply \receiver_can_grant = (AllowGrant \ rights)\); - when (reply \ None) $ set_reply_obj_ref reply_tcb_update (the reply) (Some thread); + when (reply \ None) $ do + set_reply_obj_ref reply_tcb_update (the reply) (Some thread); + update_reply (the reply) (reply_can_grant_update (\_. AllowGrant \ rights)) + od; \<^cancel>\FIXME RT: schedule_tcb?\ qs' \ tcb_ep_append thread queue; set_endpoint epptr (RecvEP qs') @@ -423,6 +428,7 @@ where then do sender_sc \ get_tcb_obj_ref tcb_sched_context sender; donate \ return $ (sender_sc \ None) \ \(case_option False is_timeout_fault fault); + update_reply (the reply) (reply_can_grant_update (\_. AllowGrant \ rights)); reply_push sender thread (the reply) donate od else set_thread_state sender Inactive diff --git a/spec/abstract/KHeap_A.thy b/spec/abstract/KHeap_A.thy index 69f72edcf3..25175567dd 100644 --- a/spec/abstract/KHeap_A.thy +++ b/spec/abstract/KHeap_A.thy @@ -223,9 +223,20 @@ abbreviation set_reply :: "obj_ref \ reply \ (unit,'z::state_ext) s_monad" where "set_reply \ set_simple_ko Reply" +definition + update_reply :: "obj_ref \ (reply \ reply) \ (unit,'z::state_ext) s_monad" +where + "update_reply ptr f \ do + obj \ get_object ptr; + case obj of Reply reply \ set_object ptr (Reply (f reply)) | _ \ fail + od" + abbreviation "get_reply_tcb r \ liftM reply_tcb (get_reply r)" + +abbreviation + "get_reply_can_grant r \ liftM reply_can_grant (get_reply r)" (* abbreviation "get_reply_caller r \ liftM reply_caller (get_reply r)" diff --git a/spec/abstract/Retype_A.thy b/spec/abstract/Retype_A.thy index 9402f9bd24..c50231ec99 100644 --- a/spec/abstract/Retype_A.thy +++ b/spec/abstract/Retype_A.thy @@ -41,7 +41,7 @@ where | "default_cap EndpointObject oref s _ = EndpointCap oref 0 UNIV" | "default_cap NotificationObject oref s _ = NotificationCap oref 0 {AllowRead, AllowWrite}" | "default_cap SchedContextObject oref s _ = SchedContextCap oref (s - min_sched_context_bits)" -| "default_cap ReplyObject oref _ _ = ReplyCap oref {AllowGrant, AllowWrite}" +| "default_cap ReplyObject oref _ _ = ReplyCap oref" | "default_cap (ArchObject aobj) oref s dev = ArchObjectCap (arch_default_cap aobj oref s dev)" text \Create and install a new capability to a newly created object.\ diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy index 874342814d..ac59dcd06c 100644 --- a/spec/abstract/Structures_A.thy +++ b/spec/abstract/Structures_A.thy @@ -115,7 +115,7 @@ datatype cap \ \device flag, pointer, size in bits (i.e. @{text "size = 2^bits"}) and freeIndex (i.e. @{text "freeRef = obj_ref + (freeIndex * 2^4)"})\ | EndpointCap obj_ref badge cap_rights | NotificationCap obj_ref badge cap_rights - | ReplyCap obj_ref cap_rights + | ReplyCap obj_ref | CNodeCap obj_ref nat "bool list" \ \CNode ptr, number of bits translated, guard\ | ThreadCap obj_ref @@ -175,7 +175,7 @@ definition definition is_reply_cap :: "cap \ bool" where - "is_reply_cap cap \ case cap of ReplyCap _ _ \ True | _ \ False" + "is_reply_cap cap \ case cap of ReplyCap _ \ True | _ \ False" definition is_zombie :: "cap \ bool" where "is_zombie cap \ case cap of Zombie _ _ _ \ True | _ \ False" @@ -227,7 +227,6 @@ primrec (nonexhaustive) where "cap_rights (EndpointCap _ _ cr) = cr" | "cap_rights (NotificationCap _ _ cr) = cr" -| "cap_rights (ReplyCap _ cr) = cr" | "cap_rights (ArchObjectCap acap) = acap_rights acap" end @@ -240,7 +239,6 @@ definition EndpointCap oref badge cr \ EndpointCap oref badge cr' | NotificationCap oref badge cr \ NotificationCap oref badge (cr' - {AllowGrant, AllowGrantReply}) - | ReplyCap t cr \ ReplyCap t (cr' - {AllowRead, AllowGrantReply} \ {AllowWrite}) | ArchObjectCap acap \ ArchObjectCap (acap_rights_update cr' acap) | _ \ cap" @@ -579,11 +577,12 @@ definition \" record reply = - reply_tcb :: "obj_ref option" - reply_sc :: "obj_ref option" + reply_tcb :: "obj_ref option" + reply_sc :: "obj_ref option" + reply_can_grant :: "bool" definition - "default_reply = \ reply_tcb = None, reply_sc = None \" + "default_reply = \ reply_tcb = None, reply_sc = None, reply_can_grant = False \" text \ All kernel objects are CNodes, TCBs, Endpoints, Notifications or architecture @@ -641,7 +640,7 @@ where | "obj_size (CNodeCap r bits g) = 1 << (cte_level_bits + bits)" | "obj_size (ThreadCap r) = 1 << obj_bits (TCB undefined)" | "obj_size (SchedContextCap r bits) = 1 << (min_sched_context_bits + bits)" -| "obj_size (ReplyCap r _) = 1 << obj_bits (Reply undefined)" +| "obj_size (ReplyCap r) = 1 << obj_bits (Reply undefined)" | "obj_size (Zombie r zb n) = (case zb of None \ 1 << obj_bits (TCB undefined) | Some n \ 1 << (cte_level_bits + n))" | "obj_size (ArchObjectCap a) = 1 << arch_obj_size a" @@ -798,7 +797,7 @@ primrec obj_refs :: "cap \ obj_ref set" where "obj_refs NullCap = {}" -| "obj_refs (ReplyCap r _) = {r}" +| "obj_refs (ReplyCap r) = {r}" | "obj_refs IRQControlCap = {}" | "obj_refs (IRQHandlerCap irq) = {}" | "obj_refs (UntypedCap dev r s f) = {}" @@ -821,7 +820,7 @@ primrec (nonexhaustive) obj_ref_of :: "cap \ obj_ref" where "obj_ref_of (UntypedCap dev r s f) = r" -| "obj_ref_of (ReplyCap r _) = r" +| "obj_ref_of (ReplyCap r) = r" | "obj_ref_of (CNodeCap r bits guard) = r" | "obj_ref_of (EndpointCap r b cr) = r" | "obj_ref_of (NotificationCap r b cr) = r" diff --git a/spec/abstract/Syscall_A.thy b/spec/abstract/Syscall_A.thy index d500b5d3e3..f1f023e2ed 100644 --- a/spec/abstract/Syscall_A.thy +++ b/spec/abstract/Syscall_A.thy @@ -179,9 +179,10 @@ where | "perform_invocation _ _ _ (InvokeDomain tptr d) = invoke_domain tptr d" -| "perform_invocation _ _ _ (InvokeReply reply grant) = +| "perform_invocation _ _ _ (InvokeReply reply) = liftE (do sender \ gets cur_thread; + grant \ get_reply_can_grant reply; do_reply_transfer sender reply grant; return [] od)" diff --git a/spec/design/skel/Intermediate_H.thy b/spec/design/skel/Intermediate_H.thy index eef031bf95..d6154e1ef7 100644 --- a/spec/design/skel/Intermediate_H.thy +++ b/spec/design/skel/Intermediate_H.thy @@ -74,7 +74,7 @@ defs createNewCaps_def: od) | Some ReplyObject \ (do addrs \ createObjects regionBase numObjects (injectKO (makeObject ::reply)) 0; - return $ map (\ addr. ReplyCap addr True) addrs + return $ map (\ addr. ReplyCap addr) addrs od) | Some ArchTypes_H.CapTableObject \ (do addrs \ createObjects regionBase numObjects (injectKO (makeObject ::cte)) userSize; diff --git a/spec/haskell/src/SEL4/API/Invocation.lhs b/spec/haskell/src/SEL4/API/Invocation.lhs index 197692d4c7..1abb401262 100644 --- a/spec/haskell/src/SEL4/API/Invocation.lhs +++ b/spec/haskell/src/SEL4/API/Invocation.lhs @@ -37,7 +37,7 @@ The following type can specify any kernel object invocation. It contains physica > = InvokeUntyped UntypedInvocation > | InvokeEndpoint (PPtr Endpoint) Word Bool Bool > | InvokeNotification (PPtr Notification) Word -> | InvokeReply (PPtr Reply) Bool +> | InvokeReply (PPtr Reply) > | InvokeDomain (PPtr TCB) Domain > | InvokeTCB TCBInvocation > | InvokeSchedContext SchedContextInvocation diff --git a/spec/haskell/src/SEL4/Object/Endpoint.lhs b/spec/haskell/src/SEL4/Object/Endpoint.lhs index 2c9d0d9ef0..296337b2c9 100644 --- a/spec/haskell/src/SEL4/Object/Endpoint.lhs +++ b/spec/haskell/src/SEL4/Object/Endpoint.lhs @@ -140,7 +140,7 @@ The IPC receive operation is essentially the same as the send operation, but wit > stateAssert valid_idle'_asrt > "Assert that `valid_idle' s` holds" > replyOpt <- (case replyCap of -> ReplyCap r _ -> return (Just r) +> ReplyCap r -> return (Just r) > NullCap -> return Nothing > _ -> fail "receiveIPC: replyCap must be ReplyCap or NullCap") > when (replyOpt /= Nothing) $ do @@ -164,8 +164,9 @@ The IPC receive operation is essentially the same as the send operation, but wit > blockingObject = epptr, > blockingIPCCanGrant = recvCanGrant, > replyObject = replyOpt }) thread -> when (replyOpt /= Nothing) $ +> when (replyOpt /= Nothing) $ do > updateReply (fromJust replyOpt) (\reply -> reply { replyTCB = Just thread }) +> updateReply (fromJust replyOpt) (\reply -> reply { replyCanGrant = recvCanGrant }) > setEndpoint epptr $ RecvEP [thread] > False -> doNBRecvFailedTransfer thread > RecvEP queue -> case isBlocking of @@ -174,8 +175,9 @@ The IPC receive operation is essentially the same as the send operation, but wit > blockingObject = epptr, > blockingIPCCanGrant = recvCanGrant, > replyObject = replyOpt}) thread -> when (replyOpt /= Nothing) $ +> when (replyOpt /= Nothing) $ do > updateReply (fromJust replyOpt) (\reply -> reply { replyTCB = Just thread }) +> updateReply (fromJust replyOpt) (\reply -> reply { replyCanGrant = recvCanGrant }) > qs' <- tcbEPAppend thread queue > setEndpoint epptr $ RecvEP $ qs' > False -> doNBRecvFailedTransfer thread @@ -199,6 +201,7 @@ The IPC receive operation is essentially the same as the send operation, but wit > then do > senderSc <- threadGet tcbSchedContext sender > donate <- return ((senderSc /= Nothing) && not (isJust fault && isTimeoutFault (fromJust fault))) +> updateReply (fromJust replyOpt) (\reply -> reply { replyCanGrant = recvCanGrant }) > replyPush sender thread (fromJust replyOpt) donate > else setThreadState Inactive sender > else do diff --git a/spec/haskell/src/SEL4/Object/Instances.lhs b/spec/haskell/src/SEL4/Object/Instances.lhs index 98460cbea9..80bbe75fdc 100644 --- a/spec/haskell/src/SEL4/Object/Instances.lhs +++ b/spec/haskell/src/SEL4/Object/Instances.lhs @@ -60,7 +60,7 @@ The following are the instances of "Storable" for the four main types of kernel > _ -> typeError "SchedContext" o > instance PSpaceStorable Reply where -> makeObject = Reply Nothing Nothing Nothing +> makeObject = Reply Nothing False Nothing Nothing > injectKO = KOReply > projectKO o = case o of > KOReply e -> return e diff --git a/spec/haskell/src/SEL4/Object/ObjectType.lhs b/spec/haskell/src/SEL4/Object/ObjectType.lhs index e33d233fb6..ba98eaf169 100644 --- a/spec/haskell/src/SEL4/Object/ObjectType.lhs +++ b/spec/haskell/src/SEL4/Object/ObjectType.lhs @@ -359,8 +359,7 @@ The "maskCapRights" function restricts the operations that can be performed on a > capNtfnCanSend = capNtfnCanSend c && capAllowWrite r, > capNtfnCanReceive = capNtfnCanReceive c && capAllowRead r } -> maskCapRights r c@(ReplyCap {}) = c{ -> capReplyCanGrant = capReplyCanGrant c && capAllowGrant r } +> maskCapRights _ c@(ReplyCap {}) = c > maskCapRights _ c@(CNodeCap {}) = c @@ -409,7 +408,7 @@ New threads are placed in the current security domain, which must be the domain > return $ newCap > Just ReplyObject -> do > placeNewObject regionBase (makeObject :: Reply) 0 -> return $ ReplyCap (PPtr $ fromPPtr regionBase) True +> return $ ReplyCap (PPtr $ fromPPtr regionBase) > Just CapTableObject -> do > placeNewObject (PPtr $ fromPPtr regionBase) (makeObject :: CTE) userSize > modify (\ks -> ks { gsCNodes = @@ -439,7 +438,7 @@ The "decodeInvocation" function parses the message, determines the operation tha > return $ InvokeNotification (capNtfnPtr cap) (capNtfnBadge cap) > > decodeInvocation _ _ _ _ cap@(ReplyCap {}) _ _ _ = do -> return $ InvokeReply (capReplyPtr cap) (capReplyCanGrant cap) +> return $ InvokeReply (capReplyPtr cap) > > decodeInvocation > label args _ slot cap@(ThreadCap {}) extraCaps False _ = @@ -500,9 +499,10 @@ This function just dispatches invocations to the type-specific invocation functi > withoutPreemption $ sendSignal ep badge > return $ [] > -> performInvocation _ _ _ (InvokeReply reply canGrantReply) = +> performInvocation _ _ _ (InvokeReply reply) = > withoutPreemption $ do > thread <- getCurThread +> canGrantReply <- liftM replyCanGrant (getReply reply) > doReplyTransfer thread reply canGrantReply > return $ [] > diff --git a/spec/haskell/src/SEL4/Object/Structures.lhs b/spec/haskell/src/SEL4/Object/Structures.lhs index 17762d9619..55693d3cb0 100644 --- a/spec/haskell/src/SEL4/Object/Structures.lhs +++ b/spec/haskell/src/SEL4/Object/Structures.lhs @@ -70,8 +70,7 @@ This is the type used to represent a capability. > | ArchObjectCap { > capCap :: ArchCapability } > | ReplyCap { -> capReplyPtr :: PPtr Reply, -> capReplyCanGrant :: Bool } +> capReplyPtr :: PPtr Reply } > | UntypedCap { > capIsDevice :: Bool, > capPtr :: PPtr (), @@ -245,6 +244,7 @@ list of pointers to waiting threads; > data Reply = Reply { > replyTCB :: Maybe (PPtr TCB), +> replyCanGrant :: Bool, > replyPrev :: Maybe (PPtr Reply), > replyNext :: Maybe ReplyNext }