secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
seL4-L4.verified/proof/invariant-abstract
History
Gerwin Klein de07915334 arm+arm-hyp+aarch64 ainvs: SGISignalCap proofs 
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
 		2025-07-07 08:53:07 +10:00
..
AARCH64 arm+arm-hyp+aarch64 ainvs: SGISignalCap proofs 2025-07-07 08:53:07 +10:00
ARM arm+arm-hyp+aarch64 ainvs: SGISignalCap proofs 2025-07-07 08:53:07 +10:00
ARM_HYP arm+arm-hyp+aarch64 ainvs: SGISignalCap proofs 2025-07-07 08:53:07 +10:00
RISCV64 x64+riscv ainvs: adjust for new CDT interface 2025-07-07 08:53:07 +10:00
X64 x64+riscv ainvs: adjust for new CDT interface 2025-07-07 08:53:07 +10:00
ADT_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
AInvs.thy ainvs: move Arch theory requalifies to generic 2024-08-08 18:05:03 +10:00
AInvsPre.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
Arch_AI.thy lib+proof: rename crunches to crunch 2024-07-08 23:02:12 +10:00
BCorres2_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
BCorres_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
Bits_AI.thy proof: update to Isabelle2023 mapsto syntax 2023-10-06 14:41:41 +11:00
CNodeInv_AI.thy x64 ainvs: fold valid_ioports into valid_arch_state 2024-12-04 18:11:22 +11:00
CSpaceInvPre_AI.thy ainvs: deploy arch_requalify infrastructure 2024-08-08 18:05:03 +10:00
CSpaceInv_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
CSpacePre_AI.thy ainvs: move Arch theory requalifies to generic 2024-08-08 18:05:03 +10:00
CSpace_AI.thy x64+riscv ainvs: adjust for new CDT interface 2025-07-07 08:53:07 +10:00
DetSchedAux_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
DetSchedDomainTime_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
DetSchedInvs_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
DetSchedSchedule_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
Deterministic_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
Detype_AI.thy x64 ainvs: fold valid_ioports into valid_arch_state 2024-12-04 18:11:22 +11:00
EmptyFail_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
Finalise_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
Include_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
InterruptAcc_AI.thy x64 ainvs: fold valid_ioports into valid_arch_state 2024-12-04 18:11:22 +11:00
Interrupt_AI.thy ainvs: deploy arch_requalify infrastructure 2024-08-08 18:05:03 +10:00
InvariantsPre_AI.thy ainvs: deploy arch_requalify infrastructure 2024-08-08 18:05:03 +10:00
Invariants_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
IpcCancel_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
Ipc_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
KHeapPre_AI.thy ainvs: refactor arch_thread_get/set lemmas 2025-02-17 15:50:04 +11:00
KHeap_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
KernelInitSepProofs_AI.thy lib+proof+autocorres: update for renamed monad lemmas 2024-06-11 10:04:55 +10: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 ainvs: move Arch theory requalifies to generic 2024-08-08 18:05:03 +10:00
README.md lib+spec+proof+autocorres: consistent Nondet filename prefix 2023-08-09 12:07:06 +10:00
Retype_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
Rights_AI.thy licenses: convert license tags to SPDX 2020-03-13 14:38:24 +08:00
Schedule_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
SubMonad_AI.thy proofs: updates for monad refactor 2023-02-09 11:46:55 +11:00
Syscall_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
TcbAcc_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
Tcb_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
Untyped_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
VSpaceEntries_AI.thy lib+proof+autocorres: update for renamed monad lemmas 2024-06-11 10:04:55 +10:00
VSpacePre_AI.thy aarch64 proof: update for det_ext refactor 2025-05-01 10:55:20 +10:00
VSpace_AI.thy ainvs: disambiguate acap_rights_update_id 2024-08-08 18:05:03 +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.