adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof/invariant-abstract
History
Achim D. Brucker e59d6ad091 Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
..
AARCH64 proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
ARM lib: reorder assumptions of no_fail_bind 2024-01-15 18:08:12 +10:30
ARM_HYP lib: reorder assumptions of no_fail_bind 2024-01-15 18:08:12 +10:30
RISCV64 proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
X64 proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
ADT_AI.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
AInvs.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
AInvsPre.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
Arch_AI.thy isabelle2021-1: remove no_take_bit 2022-03-29 08:38:25 +11:00
BCorres2_AI.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
BCorres_AI.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Bits_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
CNodeInv_AI.thy proof: update for changes to nondet monad 2023-10-05 11:24:05 +11:00
CSpaceInvPre_AI.thy isabelle-2021 arm: AInvs update 2021-09-30 16:53:17 +10:00
CSpaceInv_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
CSpacePre_AI.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
CSpace_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
DetSchedAux_AI.thy ainvs: update proofs to never unfold numDomains 2021-12-22 23:50:22 +11:00
DetSchedDomainTime_AI.thy proof+autocorres: update for select_wp and alternative_wp 2023-08-09 16:42:01 +10:00
DetSchedInvs_AI.thy proof: update for changes to nondet monad 2023-10-05 11:24:05 +11:00
DetSchedSchedule_AI.thy proof: update for changes to nondet monad 2023-10-05 11:24:05 +11:00
Deterministic_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
Detype_AI.thy proof: rename corres_split' to corres_underlying_split 2022-10-20 08:59:52 +11:00
EmptyFail_AI.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Finalise_AI.thy proof: update for changes to nondet monad 2023-10-05 11:24:05 +11:00
Include_AI.thy lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
InterruptAcc_AI.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
Interrupt_AI.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
InvariantsPre_AI.thy isabelle-2021 arm: AInvs update 2021-09-30 16:53:17 +10:00
Invariants_AI.thy aarch64 ainvs+refine: move lemmas from Refine 2023-09-27 14:28:36 +10:00
IpcCancel_AI.thy proof: update for changes to nondet monad 2023-10-05 11:24:05 +11:00
Ipc_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
KHeapPre_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
KHeap_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
KernelInitSepProofs_AI.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
KernelInitSep_AI.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
KernelInit_AI.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
LevityCatch_AI.thy proof+autocorres: update for select_wp and alternative_wp 2023-08-09 16:42:01 +10:00
README.md lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Retype_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
Rights_AI.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Schedule_AI.thy proof+autocorres: update for select_wp and alternative_wp 2023-08-09 16:42:01 +10:00
SubMonad_AI.thy proofs: updates for monad refactor 2023-02-09 11:46:55 +11:00
Syscall_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
TcbAcc_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
Tcb_AI.thy proof: update for changes to nondet monad 2023-10-05 11:24:05 +11:00
Untyped_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
VSpaceEntries_AI.thy lib+ainvs+aarch64 refine: move+consolidate vcg_op_lift lemmas 2023-09-27 14:28:36 +10:00
VSpacePre_AI.thy Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
VSpace_AI.thy aspec+access: Syscall_AC arch split 2021-06-21 20:10:32 +10:00

README.md

Abstract Spec Invariant Proof

This proof defines and proves the global invariants of seL4's abstract specification. The invariants are phrased and proved using a monadic Hoare logic described in a TPHOLS '08 paper.

Building

To build for the ARM architecture from the l4v/ directory, run:

L4V_ARCH=ARM ./run_tests AInvs

Important Theories

The top-level theory where the invariants are proved over the kernel is Syscall_AI; the bottom-level theory where they are defined is Invariants_AI.