Skip to content

Commit

Permalink
riscv refine+infoflow: fixup InfoFlowC
Browse files Browse the repository at this point in the history 
Signed-off-by: Michael McInerney <[email protected]>
  • Loading branch information
@michaelmcinerney
michaelmcinerney committed May 7, 2024
1 parent 108d2d6 commit d92de72
Show file tree
Hide file tree
Showing 4 changed files with 40 additions and 17 deletions.
2 changes: 1 addition & 1 deletion proof/infoflow/refine/ADT_IF_Refine.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -509,7 +509,7 @@ lemma scheduler'_if_ex_abs[wp]:
apply wp
apply (clarsimp simp: ex_abs_def)
apply (rule exI, rule conjI, assumption)
apply (frule state_relation_schact)
apply (frule state_relation_sched_act_relation)
apply (auto simp: domain_list_rel_eq domain_time_rel_eq)
done

Expand Down
18 changes: 10 additions & 8 deletions proof/infoflow/refine/RISCV64/ArchADT_IF_Refine_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,9 +47,7 @@ qed

lemma handleInvocation_ccorres'[ADT_IF_Refine_assms]:
"ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and arch_extras and
ct_active' and sch_act_simple and
(\<lambda>s. \<forall>x. ksCurThread s \<notin> set (ksReadyQueues s x)))
(invs' and arch_extras and ct_active' and sch_act_simple)
(UNIV \<inter> {s. isCall_' s = from_bool isCall}
\<inter> {s. isBlocking_' s = from_bool isBlocking}) []
(handleInvocation isCall isBlocking) (Call handleInvocation_'proc)"
Expand Down Expand Up @@ -119,20 +117,24 @@ lemma do_user_op_if_C_corres[ADT_IF_Refine_assms]:
apply (rule corres_gen_asm)
apply (simp add: doUserOp_if_def doUserOp_C_if_def uop_nonempty_def del: split_paired_All)
apply (rule corres_gets_same)
apply (clarsimp simp: absKState_crelation ptable_rights_s'_def ptable_rights_s''_def
rf_sr_def cstate_relation_def Let_def cstate_to_H_correct)
apply (fastforce dest: ex_abs_ksReadyQueues_asrt
simp: absKState_crelation ptable_rights_s'_def ptable_rights_s''_def
rf_sr_def cstate_relation_def Let_def cstate_to_H_correct)
apply simp
apply (rule corres_gets_same)
apply (clarsimp simp: ptable_xn_s'_def ptable_xn_s''_def ptable_attrs_s_def
absKState_crelation ptable_attrs_s'_def ptable_attrs_s''_def rf_sr_def)
apply (fastforce dest: ex_abs_ksReadyQueues_asrt
simp: ptable_xn_s'_def ptable_xn_s''_def ptable_attrs_s_def
absKState_crelation ptable_attrs_s'_def ptable_attrs_s''_def rf_sr_def)
apply simp
apply (rule corres_gets_same)
apply clarsimp
apply (frule ex_abs_ksReadyQueues_asrt)
apply (clarsimp simp: absKState_crelation curthread_relation ptable_lift_s'_def ptable_lift_s''_def
ptable_lift_s_def rf_sr_def)
apply simp
apply (simp add: getCurThread_def)
apply (rule corres_gets_same)
apply (simp add: absKState_crelation rf_sr_def)
apply (fastforce dest: ex_abs_ksReadyQueues_asrt simp: absKState_crelation rf_sr_def)
apply simp
apply (rule corres_gets_same)
apply (rule fun_cong[where x=ptrFromPAddr])
Expand Down
33 changes: 25 additions & 8 deletions proof/infoflow/refine/RISCV64/Example_Valid_StateH.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -216,6 +216,8 @@ definition Low_tcbH :: tcb where
\<comment> \<open>tcbFaultHandler =\<close> 0
\<comment> \<open>tcbIPCBuffer =\<close> 0
\<comment> \<open>tcbBoundNotification =\<close> None
\<comment> \<open>tcbSchedPrev =\<close> None
\<comment> \<open>tcbSchedNext =\<close> None
\<comment> \<open>tcbContext =\<close> (ArchThread undefined)"


Expand All @@ -240,6 +242,8 @@ definition High_tcbH :: tcb where
\<comment> \<open>tcbFaultHandler =\<close> 0
\<comment> \<open>tcbIPCBuffer =\<close> 0
\<comment> \<open>tcbBoundNotification =\<close> None
\<comment> \<open>tcbSchedPrev =\<close> None
\<comment> \<open>tcbSchedNext =\<close> None
\<comment> \<open>tcbContext =\<close> (ArchThread undefined)"


Expand All @@ -262,6 +266,8 @@ definition idle_tcbH :: tcb where
\<comment> \<open>tcbFaultHandler =\<close> 0
\<comment> \<open>tcbIPCBuffer =\<close> 0
\<comment> \<open>tcbBoundNotification =\<close> None
\<comment> \<open>tcbSchedPrev =\<close> None
\<comment> \<open>tcbSchedNext =\<close> None
\<comment> \<open>tcbContext =\<close> (ArchThread empty_context)"


Expand Down Expand Up @@ -1175,7 +1181,7 @@ definition s0H_internal :: "kernel_state" where
ksDomSchedule = [(0, 10), (1, 10)],
ksCurDomain = 0,
ksDomainTime = 5,
ksReadyQueues = const [],
ksReadyQueues = const (TcbQueue None None),
ksReadyQueuesL1Bitmap = const 0,
ksReadyQueuesL2Bitmap = const 0,
ksCurThread = Low_tcb_ptr,
Expand Down Expand Up @@ -3253,8 +3259,6 @@ lemma s0H_invs:
s0H_internal_def s0_ptrs_aligned objBitsKO_def Low_tcbH_def)
apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct', simplified s0H_internal_def])
apply (simp add: objBitsKO_def)
apply (rule conjI)
apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs s0H_internal_def)
apply (rule conjI)
apply (clarsimp simp: sym_refs_def state_refs_of'_def refs_of'_def split: option.splits)
apply (frule kh0H_SomeD)
Expand Down Expand Up @@ -3421,9 +3425,16 @@ lemma s0H_invs:
apply (rule conjI)
apply (clarsimp simp: irqs_masked'_def s0H_internal_def maxIRQ_def timer_irq_def irqInvalid_def)
apply (rule conjI)
apply (clarsimp simp: valid_queues'_def obj_at'_def s0H_internal_def inQ_def)
apply (frule kh0H_dom_tcb)
apply (elim disjE, (clarsimp simp: kh0H_obj_def)+)[1]
apply (clarsimp simp: sym_heap_def opt_map_def projectKOs split: option.splits)
using kh0H_dom_tcb
apply (fastforce simp: kh0H_obj_def)
apply (rule conjI)
apply (clarsimp simp: valid_sched_pointers_def opt_map_def projectKOs split: option.splits)
using kh0H_dom_tcb
apply (fastforce simp: kh0H_obj_def)
apply (rule conjI)
apply (clarsimp simp: valid_bitmaps_def valid_bitmapQ_def bitmapQ_def s0H_internal_def
tcbQueueEmpty_def bitmapQ_no_L1_orphans_def bitmapQ_no_L2_orphans_def)
apply (rule conjI)
apply (clarsimp simp: ct_not_inQ_def obj_at'_def objBitsKO_def
s0H_internal_def s0_ptrs_aligned Low_tcbH_def)
Expand Down Expand Up @@ -3596,7 +3607,7 @@ lemma s0_pspace_rel:
apply (clarsimp simp: kh0_obj_def bit_simps dest!: less_0x200_exists_ucast)
defer
apply ((clarsimp simp: kh0_obj_def kh0H_obj_def bit_simps word_bits_def
other_obj_relation_def fault_rel_optionation_def
fault_rel_optionation_def tcb_relation_cut_def
tcb_relation_def arch_tcb_relation_def the_nat_to_bl_simps
split del: if_split)+)[3]
prefer 13
Expand Down Expand Up @@ -3657,7 +3668,13 @@ lemma s0_srel:
High_etcb_def Low_etcb_def default_etcb_def
split: if_split_asm)
apply (simp add: s0_internal_def exst0_def s0H_internal_def sched_act_relation_def)
apply (simp add: s0_internal_def exst0_def s0H_internal_def ready_queues_relation_def)
apply (clarsimp simp: s0_internal_def exst0_def s0H_internal_def
ready_queues_relation_def list_queue_relation_def
queue_end_valid_def prev_queue_head_def inQ_def
tcbQueueEmpty_def projectKOs opt_map_def opt_pred_def
split: option.splits)
using kh0H_dom_tcb
apply (fastforce simp: kh0H_obj_def)
apply (clarsimp simp: s0_internal_def exst0_def s0H_internal_def ghost_relation_def)
apply (rule conjI)
apply (fastforce simp: kh0_def kh0_obj_def dest: kh0_SomeD)
Expand Down
4 changes: 4 additions & 0 deletions proof/refine/RISCV64/Refine.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -496,6 +496,10 @@ qed
definition
"ex_abs G \<equiv> \<lambda>s'. \<exists>s. ((s :: (det_ext) state),s') \<in> state_relation \<and> G s"

lemma ex_abs_ksReadyQueues_asrt:
"ex_abs P s \<Longrightarrow> ksReadyQueues_asrt s"
by (fastforce simp: ex_abs_def intro: ksReadyQueues_asrt_cross)

lemma device_update_invs':
"\<lbrace>invs'\<rbrace>doMachineOp (device_memory_update ds)
\<lbrace>\<lambda>_. invs'\<rbrace>"
Expand Down

0 comments on commit d92de72

Please sign in to comment.