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

Lemmas for simplifying masking and thread states #817

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Lemmas for simplifying masking and thread states #817

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
668c4dd
crefine: lemmas for simplifying masking and thread states
michaelmcinerney Sep 9, 2024
ba8ac98
crefine: address Raf's comment and hopefully fix errors squash
michaelmcinerney Sep 10, 2024
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
18 changes: 16 additions & 2 deletions proof/crefine/AARCH64/Wellformed_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -666,9 +666,23 @@ lemma ptrFromPAddr_mask_cacheLineSize[simp]:
by (simp add: ptrFromPAddr_def add_mask_ignore)

(* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
lemma ThreadState_Restart_mask[simp]:
lemma
shows ThreadState_Restart_mask[simp]:
"(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
by (simp add: ThreadState_Restart_def mask_def)
and ThreadState_Inactive_mask[simp]:
"(scast ThreadState_Inactive::machine_word) && mask 4 = scast ThreadState_Inactive"
and ThreadState_Running_mask[simp]:
"(scast ThreadState_Running::machine_word) && mask 4 = scast ThreadState_Running"
and ThreadState_BlockedOnReceive_mask[simp]:
"(scast ThreadState_BlockedOnReceive::machine_word) && mask 4 = scast ThreadState_BlockedOnReceive"
and ThreadState_BlockedOnSend_mask[simp]:
"(scast ThreadState_BlockedOnSend::machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
and ThreadState_BlockedOnReply_mask[simp]:
"(scast ThreadState_BlockedOnReply::machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
and ThreadState_BlockedOnNotification_mask[simp]:
"(scast ThreadState_BlockedOnNotification::machine_word) && mask 4
= scast ThreadState_BlockedOnNotification"
by (simp add: ThreadState_defs mask_def)+

lemma aligned_tcb_ctcb_not_NULL:
assumes "is_aligned p tcbBlockSizeBits"
Expand Down
19 changes: 19 additions & 0 deletions proof/crefine/ARM/Wellformed_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -575,6 +575,25 @@ abbreviation(input)
where
"prioInvalid == seL4_InvalidPrio"

(* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
lemma
shows ThreadState_Restart_mask[simp]:
"(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
and ThreadState_Inactive_mask[simp]:
"(scast ThreadState_Inactive::machine_word) && mask 4 = scast ThreadState_Inactive"
and ThreadState_Running_mask[simp]:
"(scast ThreadState_Running::machine_word) && mask 4 = scast ThreadState_Running"
and ThreadState_BlockedOnReceive_mask[simp]:
"(scast ThreadState_BlockedOnReceive::machine_word) && mask 4 = scast ThreadState_BlockedOnReceive"
and ThreadState_BlockedOnSend_mask[simp]:
"(scast ThreadState_BlockedOnSend::machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
and ThreadState_BlockedOnReply_mask[simp]:
"(scast ThreadState_BlockedOnReply::machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
and ThreadState_BlockedOnNotification_mask[simp]:
"(scast ThreadState_BlockedOnNotification::machine_word) && mask 4
= scast ThreadState_BlockedOnNotification"
by (simp add: ThreadState_defs mask_def)+

end

end
19 changes: 19 additions & 0 deletions proof/crefine/ARM_HYP/Wellformed_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -612,6 +612,25 @@ abbreviation(input)
where
"prioInvalid == seL4_InvalidPrio"

(* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
lemma
shows ThreadState_Restart_mask[simp]:
"(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
and ThreadState_Inactive_mask[simp]:
"(scast ThreadState_Inactive::machine_word) && mask 4 = scast ThreadState_Inactive"
and ThreadState_Running_mask[simp]:
"(scast ThreadState_Running::machine_word) && mask 4 = scast ThreadState_Running"
and ThreadState_BlockedOnReceive_mask[simp]:
"(scast ThreadState_BlockedOnReceive::machine_word) && mask 4 = scast ThreadState_BlockedOnReceive"
and ThreadState_BlockedOnSend_mask[simp]:
"(scast ThreadState_BlockedOnSend::machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
and ThreadState_BlockedOnReply_mask[simp]:
"(scast ThreadState_BlockedOnReply::machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
and ThreadState_BlockedOnNotification_mask[simp]:
"(scast ThreadState_BlockedOnNotification::machine_word) && mask 4
= scast ThreadState_BlockedOnNotification"
by (simp add: ThreadState_defs mask_def)+

end

end
19 changes: 19 additions & 0 deletions proof/crefine/RISCV64/Wellformed_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -556,6 +556,25 @@ abbreviation(input)
where
"prioInvalid == seL4_InvalidPrio"

(* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
lemma
shows ThreadState_Restart_mask[simp]:
"(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
and ThreadState_Inactive_mask[simp]:
"(scast ThreadState_Inactive::machine_word) && mask 4 = scast ThreadState_Inactive"
and ThreadState_Running_mask[simp]:
"(scast ThreadState_Running::machine_word) && mask 4 = scast ThreadState_Running"
and ThreadState_BlockedOnReceive_mask[simp]:
"(scast ThreadState_BlockedOnReceive::machine_word) && mask 4 = scast ThreadState_BlockedOnReceive"
and ThreadState_BlockedOnSend_mask[simp]:
"(scast ThreadState_BlockedOnSend::machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
and ThreadState_BlockedOnReply_mask[simp]:
"(scast ThreadState_BlockedOnReply::machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
and ThreadState_BlockedOnNotification_mask[simp]:
"(scast ThreadState_BlockedOnNotification::machine_word) && mask 4
= scast ThreadState_BlockedOnNotification"
by (simp add: ThreadState_defs mask_def)+

(* generic lemmas with arch-specific consequences *)

schematic_goal size_gpRegisters:
Expand Down
19 changes: 19 additions & 0 deletions proof/crefine/X64/Wellformed_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -614,6 +614,25 @@ abbreviation(input)
where
"prioInvalid == seL4_InvalidPrio"

(* The magic 4 comes out of the bitfield generator -- this applies to all versions of the kernel. *)
lemma
shows ThreadState_Restart_mask[simp]:
"(scast ThreadState_Restart::machine_word) && mask 4 = scast ThreadState_Restart"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nitpick: I'd much prefer scast ThreadState_Restart :: machine_word to the version with no spaces; the no-space version visually indicates a cast of ThreadState_Restart as if it were an 'a, but I assume that what's intended is that machine_word is the target of the scast

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

by the way: is ThreadSTate_Restart coming from the C or the Haskell? I'm trying to think if there's a nice way to generate these lemmas in one go.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These are all from the C, in include/object/structures.h. The Haskell has similar things, but doesn't use the ThreadState prefix in the names.

And due to an ifdef in the C, I forgot to include IdleThreadState. I'll add a fixup commit for that

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right, then there's probably no nice way to generate these lemmas. There might be some hack where we go from x : set [ThreadState_Restart, ...] ==> (scast x :: machine_word) && mask 4 = scast x and explode it, but I'm not sure how much nicer that is.

and ThreadState_Inactive_mask[simp]:
"(scast ThreadState_Inactive::machine_word) && mask 4 = scast ThreadState_Inactive"
and ThreadState_Running_mask[simp]:
"(scast ThreadState_Running::machine_word) && mask 4 = scast ThreadState_Running"
and ThreadState_BlockedOnReceive_mask[simp]:
"(scast ThreadState_BlockedOnReceive::machine_word) && mask 4 = scast ThreadState_BlockedOnReceive"
and ThreadState_BlockedOnSend_mask[simp]:
"(scast ThreadState_BlockedOnSend::machine_word) && mask 4 = scast ThreadState_BlockedOnSend"
and ThreadState_BlockedOnReply_mask[simp]:
"(scast ThreadState_BlockedOnReply::machine_word) && mask 4 = scast ThreadState_BlockedOnReply"
and ThreadState_BlockedOnNotification_mask[simp]:
"(scast ThreadState_BlockedOnNotification::machine_word) && mask 4
= scast ThreadState_BlockedOnNotification"
by (simp add: ThreadState_defs mask_def)+

end

end
Loading