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

Small IPC lemmas #822

Open
wants to merge 14 commits into
base: rt
Choose a base branch
from
Open

Small IPC lemmas #822

Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
b8d82aa
rt riscv refine: add cursc_relation
michaelmcinerney Aug 7, 2024
6458c49
rt haskell+design+haskell translator: add readStateAssert
michaelmcinerney Aug 7, 2024
4d274ae
rt haskell+design+proof: reduce use of active_sc_at' in CRefine
michaelmcinerney Aug 7, 2024
1a6fb39
rt crefine: move tcbReleaseEnqueue_ccorres
michaelmcinerney Aug 7, 2024
e6c78f5
rt riscv refine: speed up proof of commitTime_corres
michaelmcinerney Aug 7, 2024
ee7f1f5
rt crefine: prove postpone_ccorres
michaelmcinerney Aug 7, 2024
6d71f59
rt crefine: prove schedContext_resume_ccorres
michaelmcinerney Aug 7, 2024
ce90c1c
rt crefine: add obj_at_cslift_ntfn
michaelmcinerney Aug 7, 2024
fae09d1
rt crefine: prove maybeDonateSchedContext_ccorres
michaelmcinerney Aug 7, 2024
d54d658
rt haskell+riscv refine+crefine: prove schedContext_bindTCB_ccorres
michaelmcinerney Aug 7, 2024
edc2057
rt haskell+riscv refine+crefine: prove schedContext_bindNtfn_ccorres
michaelmcinerney Aug 7, 2024
afa5a87
rt haskell+riscv refine+crefine: prove maybeReturnSchedContext_ccorres
michaelmcinerney Aug 7, 2024
c7875aa
rt crefine: remove duplicate of sc_released_ccorres
michaelmcinerney Aug 7, 2024
acf0754
rt riscv refine: add sym_refs_asrt_def to global [simp] set
michaelmcinerney Aug 7, 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
12 changes: 12 additions & 0 deletions proof/crefine/RISCV64/Ipc_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6082,6 +6082,18 @@ lemma schedContext_resume_ccorres:
to_bool_def)
done

lemma obj_at_cslift_ntfn:
fixes P :: "notification \<Rightarrow> bool"
shows "\<lbrakk>obj_at' P ntfn s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow>
\<exists>ko ko'. ko_at' ko ntfn s \<and> P ko \<and>
cslift s' (Ptr ntfn) = Some ko' \<and>
cnotification_relation (cslift s') ko ko'"
Comment on lines +6085 to +6090
Copy link
Member

Choose a reason for hiding this comment

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

Do you actually need the type annotation/fixes? I would have thought the cnotification_relation would constrain ko, which then should constrain P.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I can check this. This lemma started off life as a copy paste of the analogous lemma for TCBs and was then modified. That’s where the fixes and type annotations would be from

apply (frule obj_at_ko_at')
apply clarsimp
apply (frule cmap_relation_ntfn)
apply (drule (1) cmap_relation_ko_atD)
apply fastforce
done

lemma maybeDonateSchedContext_ccorres:
"ccorres dc xfdc
Expand Down