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

fix leftover typos and tweaks from #773 #790

Merged
merged 3 commits into from
Jul 12, 2024
Merged

fix leftover typos and tweaks from #773 #790

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
3b6ee9d
trivial: fix typos
lsf37 Jul 11, 2024
858dd86
design/skel: remove duplicate abbreviation
lsf37 Jul 11, 2024
a30419f
arm-hyp crefine: reduce diff to arm crefine
lsf37 Jul 11, 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
2 changes: 1 addition & 1 deletion proof/crefine/AARCH64/Finalise_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -965,7 +965,7 @@ lemma unbindMaybeNotification_ccorres:

(* On ARM, irqInvalid is 2^16-1 (i.e. -1 in 16-bit), which, by type, is always greater than maxIRQ *)
(* This means we could remove the cirq \<noteq> irqInvalid part in the Some clause. Currently left in for
proof convencience *)
proof convenience *)
definition irq_opt_relation :: "irq option \<Rightarrow> machine_word \<Rightarrow> bool" where
"irq_opt_relation airq cirq \<equiv>
case airq of
Expand Down
2 changes: 1 addition & 1 deletion proof/crefine/ARM/Finalise_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -929,7 +929,7 @@ lemma unbindMaybeNotification_ccorres:

(* On ARM, irqInvalid is 2^16-1 (i.e. -1 in 16-bit), which, by type, is always greater than maxIRQ *)
(* This means we could remove the cirq \<noteq> irqInvalid part in the Some clause. Currently left in for
proof convencience *)
proof convenience *)
definition irq_opt_relation :: "irq option \<Rightarrow> machine_word \<Rightarrow> bool" where
"irq_opt_relation airq cirq \<equiv>
case airq of
Expand Down
2 changes: 1 addition & 1 deletion proof/crefine/ARM_HYP/Finalise_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -963,7 +963,7 @@ lemma unbindMaybeNotification_ccorres:

(* On ARM, irqInvalid is 2^16-1 (i.e. -1 in 16-bit), which, by type, is always greater than maxIRQ *)
(* This means we could remove the cirq \<noteq> irqInvalid part in the Some clause. Currently left in for
proof convencience *)
proof convenience *)
definition irq_opt_relation :: "irq option \<Rightarrow> machine_word \<Rightarrow> bool" where
"irq_opt_relation airq cirq \<equiv>
case airq of
Expand Down
6 changes: 3 additions & 3 deletions proof/crefine/ARM_HYP/Refine_C.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,7 +274,7 @@ lemma handleSyscall_ccorres:
apply (subst ccorres_seq_skip'[symmetric])
apply (rule ccorres_split_nothrow_novcg)
apply (rule_tac R=\<top> and xf=xfdc in ccorres_when)
apply (case_tac rv; clarsimp simp: irq_type_never_invalid)
apply (auto simp: irq_type_never_invalid split: option.splits)[1]
apply (ctac (no_vcg) add: handleInterrupt_ccorres)
apply ceqv
apply (rule_tac r=dc and xf=xfdc in ccorres_returnOk_skip[unfolded returnOk_def,simplified])
Expand Down Expand Up @@ -303,7 +303,7 @@ lemma handleSyscall_ccorres:
apply (rule ccorres_split_nothrow_novcg)
apply (rule ccorres_Guard)?
apply (rule_tac R=\<top> and xf=xfdc in ccorres_when)
apply (case_tac rv; clarsimp simp: irq_type_never_invalid)
apply (auto simp: irq_type_never_invalid split: option.splits)[1]
apply (ctac (no_vcg) add: handleInterrupt_ccorres)
apply ceqv
apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified])
Expand Down Expand Up @@ -331,7 +331,7 @@ lemma handleSyscall_ccorres:
apply (rule ccorres_split_nothrow_novcg)
apply (rule ccorres_Guard)?
apply (rule_tac R=\<top> and xf=xfdc in ccorres_when)
apply (case_tac rv; clarsimp simp: irq_type_never_invalid)
apply (auto simp: irq_type_never_invalid split: option.splits)[1]
apply (ctac (no_vcg) add: handleInterrupt_ccorres)
apply ceqv
apply (rule_tac ccorres_returnOk_skip[unfolded returnOk_def,simplified])
Expand Down
2 changes: 1 addition & 1 deletion spec/abstract/X64/ArchInterrupt_A.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ end

context begin interpretation Arch .

(* On Arm architectures, maxIRQ is defined in Kernel_Config. On RISCV64 it is defined manually. *)
(* On Arm architectures, maxIRQ is defined in Kernel_Config. On X64 it is defined manually. *)
requalify_consts
maxIRQ

Expand Down
4 changes: 0 additions & 4 deletions spec/design/skel/AARCH64/ArchInterrupt_H.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,6 @@ begin

context Arch begin global_naming AARCH64_H

(* Kernel_Config provides a generic numeral, Haskell expects type irq *)
abbreviation (input) maxIRQ :: irq where
"maxIRQ == Kernel_Config.maxIRQ"

#INCLUDE_HASKELL SEL4/Object/Interrupt/AARCH64.hs CONTEXT AARCH64_H bodies_only ArchInv= Arch= NOT plic_complete_claim

end
Expand Down
4 changes: 0 additions & 4 deletions spec/design/skel/ARM/ArchInterrupt_H.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,6 @@ begin

context Arch begin global_naming ARM_H

(* Kernel_Config provides a generic numeral, Haskell expects type irq *)
abbreviation (input) maxIRQ :: irq where
"maxIRQ == Kernel_Config.maxIRQ"

#INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs Arch= CONTEXT ARM_H bodies_only ArchInv=

end
Expand Down
4 changes: 0 additions & 4 deletions spec/design/skel/ARM_HYP/ArchInterrupt_H.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,6 @@ begin

context Arch begin global_naming ARM_HYP_H

(* Kernel_Config provides a generic numeral, Haskell expects type irq *)
abbreviation (input) maxIRQ :: irq where
"maxIRQ == Kernel_Config.maxIRQ"

#INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs Arch= CONTEXT ARM_HYP_H bodies_only ArchInv= NOT initInterruptController

definition initInterruptController :: "unit kernel"
Expand Down