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

Update proofs for AArch64 seL4 PR #663

Merged
merged 5 commits into from
Aug 14, 2023
Merged

Update proofs for AArch64 seL4 PR #663

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
22685e6
arm abstract+design: reorder object_type enum
lsf37 Aug 11, 2023
e65939a
drefine: adjust for object_type enum reorder
lsf37 Aug 11, 2023
c657c9f
arm crefine: proof updates for object_type enum reorder
lsf37 Aug 11, 2023
29def88
arm-hyp abstract+design: object_type enum reorder
lsf37 Aug 11, 2023
a49dfab
arm-hyp crefine: proof update for object_type enum reorder
lsf37 Aug 11, 2023
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
3 changes: 3 additions & 0 deletions proof/crefine/ARM/Retype_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2391,6 +2391,9 @@ lemma ccorres_fail:
apply (simp add: fail_def)
done

(* always unfold StrictC'_mode_object_defs together with api_object_defs *)
lemmas api_object_defs = api_object_defs StrictC'_mode_object_defs

lemma object_type_from_H_toAPIType_simps:
"(object_type_from_H tp = scast seL4_UntypedObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.Untyped)"
"(object_type_from_H tp = scast seL4_TCBObject) = (toAPIType tp = Some ArchTypes_H.apiobject_type.TCBObject)"
Expand Down
3 changes: 3 additions & 0 deletions proof/crefine/ARM_HYP/Retype_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2332,6 +2332,9 @@ definition
| ARM_HYP_H.PageDirectoryObject \<Rightarrow> scast seL4_ARM_PageDirectoryObject
| ARM_HYP_H.VCPUObject \<Rightarrow> scast seL4_ARM_VCPUObject"

(* always unfold StrictC'_mode_object_defs together with api_object_defs *)
lemmas api_object_defs = api_object_defs StrictC'_mode_object_defs
Copy link
Member

Choose a reason for hiding this comment

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

I'm not 100% on whether having this kind of def override so far into CRefine is a risky approach. Should be ok here, but made me stop and think.

Copy link
Member Author

Choose a reason for hiding this comment

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

In this case I think it's fine for ARM/ARM_HYP, because it recreates the old situation before it matters the first time. But generally I agree, it's a bit risky.


lemmas nAPIObjects_def = seL4_NonArchObjectTypeCount_def

lemma nAPIOBjects_object_type_from_H:
Expand Down
12 changes: 6 additions & 6 deletions proof/drefine/StateTranslation_D.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,12 +53,12 @@ where
else if x = 2 then Some EndpointType
else if x = 3 then Some NotificationType
else if x = 4 then Some CNodeType
else if x = 5 then Some (FrameType 12)
else if x = 6 then Some (FrameType 16)
else if x = 7 then Some (FrameType 20)
else if x = 8 then Some (FrameType 24)
else if x = 9 then Some PageTableType
else if x = 10 then Some PageDirectoryType
else if x = 5 then Some PageDirectoryType
else if x = 6 then Some (FrameType 12)
else if x = 7 then Some (FrameType 16)
else if x = 8 then Some (FrameType 20)
else if x = 9 then Some (FrameType 24)
else if x = 10 then Some PageTableType
else None"

definition
Expand Down
12 changes: 6 additions & 6 deletions spec/abstract/ARM/ArchDecode_A.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -241,12 +241,12 @@ where
definition
arch_data_to_obj_type :: "nat \<Rightarrow> aobject_type option" where
"arch_data_to_obj_type n \<equiv>
if n = 0 then Some SmallPageObj
else if n = 1 then Some LargePageObj
else if n = 2 then Some SectionObj
else if n = 3 then Some SuperSectionObj
else if n = 4 then Some PageTableObj
else if n = 5 then Some PageDirectoryObj
if n = 0 then Some PageDirectoryObj
else if n = 1 then Some SmallPageObj
else if n = 2 then Some LargePageObj
else if n = 3 then Some SectionObj
else if n = 4 then Some SuperSectionObj
else if n = 5 then Some PageTableObj
else None"

definition
Expand Down
12 changes: 6 additions & 6 deletions spec/abstract/ARM_HYP/ArchDecode_A.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -259,12 +259,12 @@ where
definition
arch_data_to_obj_type :: "nat \<Rightarrow> aobject_type option" where
"arch_data_to_obj_type n \<equiv>
if n = 0 then Some SmallPageObj
else if n = 1 then Some LargePageObj
else if n = 2 then Some SectionObj
else if n = 3 then Some SuperSectionObj
else if n = 4 then Some PageTableObj
else if n = 5 then Some PageDirectoryObj
if n = 0 then Some PageDirectoryObj
else if n = 1 then Some SmallPageObj
else if n = 2 then Some LargePageObj
else if n = 3 then Some SectionObj
else if n = 4 then Some SuperSectionObj
else if n = 5 then Some PageTableObj
else if n = 6 then Some VCPUObj
else None"

Expand Down
6 changes: 3 additions & 3 deletions spec/design/skel/ARM/ArchTypes_H.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,12 +34,12 @@ interpretation Arch .
definition
enum_object_type: "enum_class.enum \<equiv>
map APIObjectType (enum_class.enum :: apiobject_type list) @
[SmallPageObject,
[PageDirectoryObject,
SmallPageObject,
LargePageObject,
SectionObject,
SuperSectionObject,
PageTableObject,
PageDirectoryObject
PageTableObject
]"

definition
Expand Down
4 changes: 2 additions & 2 deletions spec/design/skel/ARM_HYP/ArchTypes_H.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,12 +34,12 @@ interpretation Arch .
definition
enum_object_type: "enum_class.enum \<equiv>
map APIObjectType (enum_class.enum :: apiobject_type list) @
[SmallPageObject,
[PageDirectoryObject,
SmallPageObject,
LargePageObject,
SectionObject,
SuperSectionObject,
PageTableObject,
PageDirectoryObject,
VCPUObject
]"

Expand Down