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

ADT_C sorry-free #685

Merged
merged 7 commits into from
Oct 23, 2023
Merged

ADT_C sorry-free #685

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
0b8eb8d
rt aspec: zero out budget when finalising a scheduling context
michaelmcinerney Sep 13, 2022
f1471bd
rt ainvs: add invariant for inactive sc implies zero budget
michaelmcinerney Sep 13, 2022
75f732a
rt design+haskell: remove scBudget field from SchedContext record
michaelmcinerney Sep 12, 2022
18b1641
rt riscv refine: update after removing scBudget field
michaelmcinerney Sep 13, 2022
fa57dc4
rt arm refine: update after removing scBudget field
michaelmcinerney Sep 15, 2022
d0fdb09
rt crefine: clear sorries related to cpspace_refill_relation_unique
michaelmcinerney Sep 12, 2022
b843dad
rt crefine: ADT_C.thy sorry free
michaelmcinerney Sep 20, 2022
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
124 changes: 82 additions & 42 deletions proof/crefine/RISCV64/ADT_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,12 +113,14 @@ lemma setTCBContext_C_corres:
apply (apply_conjunct \<open>match conclusion in \<open>cready_queues_relation _ _ _\<close> \<Rightarrow>
\<open>erule cready_queues_relation_not_queue_ptrs; rule ext; simp split: if_split\<close>\<close>)
apply (drule ko_at_projectKO_opt)
apply (erule (2) cmap_relation_upd_relI)
apply (simp add: ctcb_relation_def carch_tcb_relation_def)
apply assumption
apply simp
apply (rule conjI)
apply (erule (2) cmap_relation_upd_relI)
apply (simp add: ctcb_relation_def carch_tcb_relation_def)
apply assumption
apply simp
apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1])
apply (rule ext, simp split: if_splits)+
done

end

definition
Expand Down Expand Up @@ -615,6 +617,18 @@ lemma cready_queues_to_H_correct:
apply (rule_tac hp="clift s" in tcb_queue_rel'_unique, simp_all add: lift_t_NULL)
done

definition crelease_queue_to_H :: "(tcb_C ptr \<rightharpoonup> tcb_C) \<Rightarrow> tcb_C ptr \<Rightarrow> machine_word list" where
"crelease_queue_to_H h_tcb qhead \<equiv> THE aq. sched_queue_relation h_tcb aq NULL qhead"

lemma crelease_queue_to_H_correct:
"sched_queue_relation (clift s) ls NULL release_hd \<Longrightarrow>
crelease_queue_to_H (clift s) release_hd = ls"
apply (clarsimp simp: crelease_queue_to_H_def fun_eq_iff)
apply (rule the_equality)
apply simp
apply (rule_tac hp="clift s" in tcb_queue_rel_unique, simp_all add: lift_t_NULL)
done

(* showing that cpspace_relation is actually unique >>>*)

lemma cmap_relation_unique_0:
Expand Down Expand Up @@ -1256,17 +1270,32 @@ lemma ksPSpace_eq_imp_valid_tcb'_eq:
valid_tcb'_def valid_tcb_state'_def valid_bound_ntfn'_def
split: thread_state.splits option.splits)

lemma ksPSpace_eq_imp_valid_sc'_eq:
assumes ksPSpace: "ksPSpace s' = ksPSpace s"
shows "valid_sched_context' sc s' = valid_sched_context' sc s"
by (auto simp: ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace]
valid_sched_context'_def valid_bound_ntfn'_def
split: option.splits)

lemma ksPSpace_eq_imp_valid_reply'_eq:
assumes ksPSpace: "ksPSpace s' = ksPSpace s"
shows "valid_reply' reply s' = valid_reply' reply s"
by (auto simp: ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace]
valid_reply'_def valid_bound_ntfn'_def
split: option.splits)

lemma ksPSpace_eq_imp_valid_objs'_eq:
assumes ksPSpace: "ksPSpace s' = ksPSpace s"
shows "valid_objs' s' = valid_objs' s"
using assms
apply (clarsimp simp: valid_objs'_def valid_obj'_def valid_ep'_def
by (clarsimp simp: valid_objs'_def valid_obj'_def valid_ep'_def
ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace]
ksPSpace_eq_imp_valid_tcb'_eq[OF ksPSpace]
ksPSpace_eq_imp_valid_cap'_eq[OF ksPSpace]
ksPSpace_eq_imp_valid_sc'_eq[OF ksPSpace]
ksPSpace_eq_imp_valid_reply'_eq[OF ksPSpace]
valid_ntfn'_def valid_cte'_def valid_bound_tcb'_def
split: kernel_object.splits endpoint.splits ntfn.splits option.splits)
sorry (* FIXME RT: ksPSpace_eq_imp_valid_objs'_eq *)

lemma ksPSpace_eq_imp_valid_pspace'_eq:
assumes ksPSpace: "ksPSpace s' = ksPSpace s"
Expand Down Expand Up @@ -1309,12 +1338,10 @@ context state_rel begin
lemma cDomScheduleIdx_to_H_correct:
assumes valid: "invs' as"
assumes cstate_rel: "cstate_relation as cs"
assumes ms: "cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)"
shows "unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as"
using assms
apply (clarsimp simp: cstate_relation_def Let_def observable_memory_def invs'_def
newKernelState_def unat_of_nat_eq cdom_schedule_relation_def)
sorry (* FIXME RT: cDomScheduleIdx_to_H_correct *)
by (clarsimp simp: cstate_relation_def Let_def invs'_def valid_dom_schedule'_def
unat_of_nat_eq cdom_schedule_relation_def)

definition
cDomSchedule_to_H :: "(dschedule_C['b :: finite]) \<Rightarrow> (8 word \<times> machine_word) list"
Expand Down Expand Up @@ -1412,12 +1439,12 @@ where
ksCurDomain = ucast (ksCurDomain_' s),
ksDomainTime = ksDomainTime_' s,
ksReadyQueues = cready_queues_to_H (clift (t_hrs_' s)) (ksReadyQueues_' s),
ksReleaseQueue = undefined, \<comment> \<open>FIXME RT: write crelease_queue_to_H\<close>
ksReleaseQueue = crelease_queue_to_H (clift (t_hrs_' s)) (ksReleaseHead_' s),
ksReadyQueuesL1Bitmap = cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' s),
ksReadyQueuesL2Bitmap = cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' s),
ksCurThread = ctcb_ptr_to_tcb_ptr (ksCurThread_' s),
ksIdleThread = ctcb_ptr_to_tcb_ptr (ksIdleThread_' s),
ksIdleSC = undefined, \<comment> \<open>FIXME RT: the idle sc in the C is the sc of ksIdleThread\<close>
ksIdleSC = ptr_val (ksIdleSC_' s),
ksConsumedTime = ksConsumed_' s,
ksCurTime = ksCurTime_' s,
ksCurSc = ptr_val (ksCurSC_' s),
Expand All @@ -1437,15 +1464,16 @@ lemma trivial_eq_conj: "B = C \<Longrightarrow> (A \<and> B) = (A \<and> C)"
by simp

lemma cstate_to_H_correct:
assumes valid: "invs' as"
assumes invs': "invs' as"
and schact: "sch_act_wf (ksSchedulerAction as) as"
assumes cstate_rel: "cstate_relation as cs"
shows "cstate_to_H cs = as \<lparr>ksMachineState:= observable_memory (ksMachineState as) (user_mem' as)\<rparr>"
apply (subgoal_tac "cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)")
apply (rule kernel_state.equality, simp_all add: cstate_to_H_def)
apply (rule cstate_to_pspace_H_correct)
using valid
using invs'
apply (simp add: invs'_def)
using cstate_rel valid
using cstate_rel invs'
apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def
observable_memory_def invs'_def valid_pspace'_def)
using cstate_rel
Expand All @@ -1457,39 +1485,51 @@ lemma cstate_to_H_correct:
using cstate_rel
apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def
prod_eq_iff)
using valid cstate_rel
using invs' cstate_rel
apply (rule mk_gsUntypedZeroRanges_correct)
subgoal
using cstate_rel
by (fastforce simp: cstate_relation_def cpspace_relation_def
Let_def ghost_size_rel_def unat_eq_0
split: if_split)
using valid cstate_rel
using invs' cstate_rel
apply (rule cDomScheduleIdx_to_H_correct)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
using valid cstate_rel
apply (rule cDomSchedule_to_H_correct)
using invs' cstate_rel
apply (rule cDomSchedule_to_H_correct)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def ucast_up_ucast_id is_up_8_32)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
apply (rule cready_queues_to_H_correct)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def ucast_up_ucast_id is_up_8_32)
apply (clarsimp simp: cstate_relation_def Let_def)
apply (rule crelease_queue_to_H_correct)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
apply (rule cready_queues_to_H_correct)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
sorry (* FIXME RT: cstate_to_H_correct
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
apply (rule cbitmap_L1_to_H_correct)
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
apply (rule cbitmap_L2_to_H_correct)
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
apply (rule cbitmap_L1_to_H_correct)
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
apply (rule cbitmap_L2_to_H_correct)
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
Expand All @@ -1498,41 +1538,41 @@ sorry (* FIXME RT: cstate_to_H_correct
apply (clarsimp simp: cstate_relation_def Let_def)
apply (rule csch_act_rel_to_H[THEN iffD1])
apply (case_tac "ksSchedulerAction as", simp+)
using valid
using schact
subgoal
by (clarsimp simp: valid_state'_def st_tcb_at'_def
obj_at'_real_def ko_wp_at'_def objBitsKO_def projectKO_opt_tcb
split: kernel_object.splits)
by (clarsimp simp: st_tcb_at'_def obj_at'_real_def ko_wp_at'_def objBitsKO_def
projectKO_opt_tcb
split: kernel_object.splits)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
apply (rule cint_rel_to_H)
using valid
apply (simp add: valid_state'_def)
using invs'
apply (simp add: invs'_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
apply (rule carch_state_to_H_correct)
using valid
apply (simp add: valid_state'_def)
using invs'
apply (simp add: invs'_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def carch_state_relation_def carch_globals_def)
using cstate_rel
apply (clarsimp simp: cstate_relation_def Let_def carch_state_relation_def carch_globals_def)
apply (rule cstate_to_machine_H_correct[simplified])
using valid
apply (simp add: valid_state'_def)
using invs'
apply (simp add: invs'_def)
using cstate_rel
apply (simp add: cstate_relation_def Let_def)
using cstate_rel
apply (simp add: cstate_relation_def Let_def cpspace_relation_def)
using cstate_rel
apply (simp add: cstate_relation_def Let_def cpspace_relation_def)
using valid
apply (clarsimp simp add: valid_state'_def)
done *)
using invs'
apply (clarsimp simp add: invs'_def)
done

end

Expand Down
42 changes: 37 additions & 5 deletions proof/crefine/RISCV64/Detype_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -859,15 +859,14 @@ proof -
qed
qed


lemma tcb_queue_relation_live_restrict:
lemma tcb_queue_relation_live_restrict':
assumes vuc: "s \<turnstile>' capability.UntypedCap d ptr bits idx"
and rel: "\<forall>t \<in> set q. tcb_at' t s"
and live: "\<forall>t \<in> set q. ko_wp_at' live' t s"
and rl: "\<forall>(p :: machine_word) P. ko_wp_at' P p s \<and> (\<forall>ko. P ko \<longrightarrow> live' ko) \<longrightarrow> p \<notin> {ptr..ptr + 2 ^ bits - 1}"
shows "tcb_queue_relation' getNext getPrev (cm |` (- Ptr ` {ptr..+2 ^ bits})) q cend chead =
tcb_queue_relation' getNext getPrev cm q cend chead"
proof (rule tcb_queue_relation'_cong [OF refl refl refl])
shows "tcb_queue_relation getNext getPrev (cm |` (- Ptr ` {ptr..+2 ^ bits})) q prev chead =
tcb_queue_relation getNext getPrev cm q prev chead"
proof (rule tcb_queue_relation_cong [OF refl refl refl])
fix p
assume "p \<in> tcb_ptr_to_ctcb_ptr ` set q"

Expand Down Expand Up @@ -896,6 +895,16 @@ proof (rule tcb_queue_relation'_cong [OF refl refl refl])
thus "(cm |` (- Ptr ` {ptr..+2 ^ bits})) p = cm p" by simp
qed

lemma tcb_queue_relation_live_restrict:
assumes vuc: "s \<turnstile>' capability.UntypedCap d ptr bits idx"
and rel: "\<forall>t \<in> set q. tcb_at' t s"
and live: "\<forall>t \<in> set q. ko_wp_at' live' t s"
and rl: "\<forall>(p :: machine_word) P. ko_wp_at' P p s \<and> (\<forall>ko. P ko \<longrightarrow> live' ko) \<longrightarrow> p \<notin> {ptr..ptr + 2 ^ bits - 1}"
shows "tcb_queue_relation' getNext getPrev (cm |` (- Ptr ` {ptr..+2 ^ bits})) q cend chead =
tcb_queue_relation' getNext getPrev cm q cend chead"
using assms
by (fastforce simp: tcb_queue_relation'_def tcb_queue_relation_live_restrict')

fun
epQ :: "endpoint \<Rightarrow> machine_word list"
where
Expand Down Expand Up @@ -1693,6 +1702,29 @@ proof -
[OF D.valid_untyped tat tlive rl])
done

moreover
from rlqrun have "\<forall>t \<in> set (ksReleaseQueue s). tcb_at' t s \<and> ko_wp_at' live' t s"
apply clarsimp
apply (rule context_conjI)
apply fastforce
apply (drule_tac x=t in spec)
apply (clarsimp simp: ko_wp_at'_def obj_at_simps split: kernel_object.splits)
apply (rule_tac x="KOTCB obj" in exI)
apply (case_tac "tcbState obj"; clarsimp split: thread_state.splits)
done
hence tat: "\<forall>t \<in> set (ksReleaseQueue s). tcb_at' t s"
and tlive: "\<forall>t \<in> set (ksReleaseQueue s). ko_wp_at' live' t s"
by auto
from sr have
"sched_queue_relation (clift ?th_s) (ksReleaseQueue s) NULL (ksReleaseHead_' (globals s'))"
unfolding rf_sr_def cstate_relation_def cpspace_relation_def
apply (simp add: tcb_queue_relation_live_restrict')
apply (clarsimp simp: Let_def all_conj_distrib)
apply ((subst lift_t_typ_region_bytes, rule cm_disj_tcb, assumption+, simp_all)[1])+
apply (insert rlqrun tat tlive rl)
apply (rule tcb_queue_relation_live_restrict'[THEN iffD2], (fastforce intro!: D.valid_untyped)+)
done

moreover
{
assume "s' \<Turnstile>\<^sub>c riscvKSGlobalPT_Ptr"
Expand Down
Loading