Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Several sorries in IpcCancel_C #789

Merged
merged 1 commit into from
Jul 15, 2024
Merged

Several sorries in IpcCancel_C #789

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 12 additions & 4 deletions proof/crefine/RISCV64/Arch_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1087,7 +1087,7 @@ lemma decodeRISCVPageTableInvocation_ccorres:
apply (clarsimp simp: ct_in_state'_def isCap_simps valid_tcb_state'_def)
apply (case_tac v1; clarsimp) (* is PT mapped *)
apply (auto simp: ct_in_state'_def isCap_simps valid_tcb_state'_def valid_cap'_def
wellformed_mapdata'_def sch_act_wf_def sch_act_simple_def
wellformed_mapdata'_def weak_sch_act_wf_def sch_act_simple_def
elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')
done
apply (rule conjI)
Expand All @@ -1102,7 +1102,7 @@ lemma decodeRISCVPageTableInvocation_ccorres:
slotcap_in_mem_def dest!: ctes_of_valid')
by (auto simp: ct_in_state'_def pred_tcb_at' mask_def valid_tcb_state'_def
valid_cap'_def wellformed_acap'_def wellformed_mapdata'_def
sch_act_wf_def sch_act_simple_def
weak_sch_act_wf_def sch_act_simple_def
elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')[1]

apply (rule conjI)
Expand Down Expand Up @@ -2105,15 +2105,15 @@ lemma decodeRISCVFrameInvocation_ccorres:
subgoal
by (auto simp: ct_in_state'_def pred_tcb_at' mask_def valid_tcb_state'_def
valid_cap'_def wellformed_acap'_def wellformed_mapdata'_def
sch_act_wf_def sch_act_simple_def
weak_sch_act_wf_def sch_act_simple_def
elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')

(* RISCVPageUnMap, Haskell side *)
apply (rule conjI)
subgoal
by (auto simp: isCap_simps comp_def ct_in_state'_def pred_tcb_at' mask_def valid_tcb_state'_def
valid_cap'_def wellformed_acap'_def wellformed_mapdata'_def
sch_act_wf_def sch_act_simple_def
weak_sch_act_wf_def sch_act_simple_def
elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')

(* C side of precondition satisfaction *)
Expand Down Expand Up @@ -2847,6 +2847,10 @@ lemma decodeRISCVMMUInvocation_ccorres:
apply (rule conjI; clarsimp)+
apply (rule conjI, erule ctes_of_valid', clarsimp)
apply (intro conjI)
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply (fastforce elim!: pred_tcb'_weakenE)
apply (clarsimp simp: excaps_in_mem_def slotcap_in_mem_def)
Expand All @@ -2864,6 +2868,10 @@ lemma decodeRISCVMMUInvocation_ccorres:
apply (clarsimp simp: isCap_simps valid_tcb_state'_def)
apply (frule invs_arch_state', clarsimp)
apply (intro conjI)
apply (fastforce simp: ct_in_state'_def elim!: pred_tcb'_weakenE)
apply fastforce
apply fastforce
apply fastforce
apply (fastforce simp: ct_in_state'_def elim!: pred_tcb'_weakenE)
apply (fastforce simp: ct_in_state'_def elim!: pred_tcb'_weakenE)
apply (cases extraCaps; simp)
Expand Down
45 changes: 26 additions & 19 deletions proof/crefine/RISCV64/Finalise_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1173,17 +1173,18 @@ lemma tcb_queue_relation2_cong:

context kernel_m begin

lemma setThreadState_ccorres_valid_queues'_simple:
lemma setThreadState_ccorres_simple:
"ccorres dc xfdc
(tcb_at' thread)
({s'. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := ts_' s' && mask 4\<rparr>, fl))}
\<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) []
(\<lambda>s. tcb_at' thread s \<and> sch_act_simple s \<and> no_0_obj' s
\<and> weak_sch_act_wf (ksSchedulerAction s) s)
(\<lbrace>\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace>
\<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>) []
(setThreadState st thread) (Call setThreadState_'proc)"
apply (cinit lift: tptr_' cong add: call_ignore_cong)
apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres)
apply (ctac add: scheduleTCB_ccorres_valid_queues'_simple)
apply wpsimp
apply (clarsimp simp: weak_sch_act_wf_def)
apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres)
apply (ctac add: scheduleTCB_ccorres_simple)
apply (wpsimp wp: threadSet_valid_objs')
apply clarsimp
done

lemma updateRestartPC_ccorres:
Expand Down Expand Up @@ -1401,23 +1402,27 @@ lemma active_runnable':

crunches updateRestartPC
for no_0_obj'[wp]: no_0_obj'
and weak_sch_act_wf[wp]: "\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s"
(wp: crunch_wps)

lemma suspend_ccorres:
assumes cteDeleteOne_ccorres:
"\<And>w slot. ccorres dc xfdc
(invs' and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap
\<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)
({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w}
"\<And>w slot.
ccorres dc xfdc
(invs'
and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap
\<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)
({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w}
\<inter> {s. slot_' s = Ptr slot}) []
(cteDeleteOne slot) (Call cteDeleteOne_'proc)"
shows
"ccorres dc xfdc
(invs' and tcb_at' thread and (\<lambda>s. thread \<noteq> ksIdleThread s))
(UNIV \<inter> {s. target_' s = tcb_ptr_to_ctcb_ptr thread}) []
(suspend thread) (Call suspend_'proc)"
(invs' and sch_act_simple and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and tcb_at' thread
and (\<lambda>s. thread \<noteq> ksIdleThread s))
\<lbrace>\<acute>target = tcb_ptr_to_ctcb_ptr thread\<rbrace> []
(suspend thread) (Call suspend_'proc)"
apply (cinit lift: target_')
apply (rule ccorres_stateAssert)
apply (rule ccorres_stateAssert)
apply (ctac(no_vcg) add: cancelIPC_ccorres1 [OF cteDeleteOne_ccorres])
apply (rule getThreadState_ccorres_foo)
apply (rename_tac threadState)
Expand All @@ -1444,7 +1449,7 @@ lemma suspend_ccorres:
apply (ctac (no_vcg) add: updateRestartPC_ccorres)
apply (rule ccorres_return_Skip)
apply ceqv
apply (ctac(no_vcg) add: setThreadState_ccorres_valid_queues'_simple)
apply (ctac(no_vcg) add: setThreadState_ccorres_simple)
apply (ctac (no_vcg) add: tcbSchedDequeue_ccorres)
apply (ctac (no_vcg) add: tcbReleaseRemove_ccorres)
apply (ctac (no_vcg) add: schedContext_cancelYieldTo_ccorres)
Expand All @@ -1454,10 +1459,12 @@ lemma suspend_ccorres:
apply clarsimp
apply (rule conseqPre, vcg)
apply (rule subset_refl)
apply (rule_tac Q="\<lambda>_. invs' and tcb_at' thread" in hoare_post_imp)
apply (rule_tac Q="\<lambda>_ s. invs' s \<and> tcb_at' thread s \<and> sch_act_simple s
\<and> weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp)
apply fastforce
apply (wpsimp wp: hoare_vcg_all_lift)
by (auto simp: ThreadState_defs)[1]
apply (auto simp: ThreadState_defs)
done

lemma cap_to_H_NTFNCap_tag:
"\<lbrakk> cap_to_H cap = NotificationCap word1 word2 a b;
Expand Down
28 changes: 15 additions & 13 deletions proof/crefine/RISCV64/Interrupt_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -250,13 +250,13 @@ lemma decodeIRQHandlerInvocation_ccorres:
apply (rule ccorres_alternative2)
apply (rule ccorres_return_CE, simp+)[1]
apply (wp sts_invs_minor')+
apply (rule ccorres_equals_throwError)
apply (fastforce simp: invocationCatch_def throwError_bind
split: gen_invocation_labels.split)
apply (simp add: ccorres_cond_iffs cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply simp
apply (rule ccorres_equals_throwError)
apply (fastforce simp: invocationCatch_def throwError_bind
split: gen_invocation_labels.split)
apply (simp add: ccorres_cond_iffs cong: StateSpace.state.fold_congs globals.fold_congs)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
apply simp
apply (clarsimp simp: Collect_const_mem)
apply (clarsimp simp: invs_valid_objs'
ct_in_state'_def
Expand All @@ -270,16 +270,18 @@ lemma decodeIRQHandlerInvocation_ccorres:
slotcap_in_mem_def valid_tcb_state'_def
dest!: interpret_excaps_eq split: bool.splits)
apply (intro conjI impI allI)
apply (clarsimp simp: cte_wp_at_ctes_of neq_Nil_conv sysargs_rel_def n_msgRegisters_def
excaps_map_def excaps_in_mem_def word_less_nat_alt hd_conv_nth
slotcap_in_mem_def valid_tcb_state'_def
dest!: interpret_excaps_eq split: bool.splits)+
apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')[6]
apply (clarsimp simp: cte_wp_at_ctes_of neq_Nil_conv sysargs_rel_def n_msgRegisters_def
excaps_map_def excaps_in_mem_def word_less_nat_alt hd_conv_nth
slotcap_in_mem_def valid_tcb_state'_def
dest!: interpret_excaps_eq split: bool.splits)+
apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')[6]
apply fastforce
apply fastforce
apply (drule ctes_of_valid')
apply fastforce
apply (clarsimp simp add:valid_cap_simps' RISCV64.maxIRQ_def)
apply (erule order.trans,simp)
apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')
apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')
done

declare mask_of_mask[simp]
Expand Down
11 changes: 8 additions & 3 deletions proof/crefine/RISCV64/Invoke_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,9 +40,12 @@ lemma cap_case_ThreadCap2:
by (simp add: isCap_simps
split: capability.split)

crunches tcbSchedEnqueue
for weak_sch_act_wf[wp]: "\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s"

lemma setDomain_ccorres:
"ccorres dc xfdc
(invs' and tcb_at' t and (\<lambda>s. d \<le> maxDomain))
(invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and tcb_at' t and (\<lambda>s. d \<le> maxDomain))
(UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. dom_' s = ucast d})
[] (setDomain t d) (Call setDomain_'proc)"
apply (rule ccorres_gen_asm)
Expand Down Expand Up @@ -75,12 +78,14 @@ lemma setDomain_ccorres:
apply (simp add: guard_is_UNIV_def)
apply simp
apply wp
apply (rule_tac Q="\<lambda>rv'. invs' and tcb_at' t and (\<lambda>s. curThread = ksCurThread s)"
apply (rule_tac Q="\<lambda>rv'. invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
and tcb_at' t and (\<lambda>s. curThread = ksCurThread s)"
in hoare_strengthen_post)
apply (wpsimp wp: isSchedulable_wp)
apply (fastforce simp: valid_pspace_valid_objs' weak_sch_act_wf_def
split: if_splits)
apply (rule_tac Q="\<lambda>_. invs' and tcb_at' t and (\<lambda>s. curThread = ksCurThread s)"
apply (rule_tac Q="\<lambda>_. invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
and tcb_at' t and (\<lambda>s. curThread = ksCurThread s)"
in hoare_strengthen_post)
apply (wpsimp wp: threadSet_tcbDomain_update_invs' hoare_vcg_imp_lift'
threadSet_isSchedulable_bool)+
Expand Down
Loading
Loading