lh-l4v/proof/ROOT

237 lines
4.9 KiB
Plaintext
Raw Normal View History

2014-07-14 19:32:44 +00:00
(*
* Copyright 2014, General Dynamics C4 Systems
*
2020-03-09 06:18:30 +00:00
* SPDX-License-Identifier: GPL-2.0-only
2014-07-14 19:32:44 +00:00
*)
chapter "Proofs"
(*
* List of rules to make various images.
*
* Some rules have duplicate targets of the form:
*
* theories [condition = "MOO", quick_and_dirty]
* "foo"
* theories
* "foo"
*
* The idea is that if the environment variable "MOO" is defined we
* execute the first rule (doing the proof in quick-and-dirty mode), and
* then find we need not take any action for the second. Otherwise, we
* skip the first rule and only perform the second.
*)
(*
* Refinement proof.
*)
session Refine in "refine" = BaseRefine +
2019-06-05 10:18:48 +00:00
description \<open>Refinement between Haskell and Abstract spec.\<close>
sessions
Lib
CorresK
AInvs
directories
"$L4V_ARCH"
theories [condition = "REFINE_QUICK_AND_DIRTY", quick_and_dirty]
"$L4V_ARCH/Refine"
"$L4V_ARCH/RAB_FN"
"$L4V_ARCH/EmptyFail_H"
theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
"$L4V_ARCH/Refine"
"$L4V_ARCH/RAB_FN"
"$L4V_ARCH/EmptyFail_H"
2014-07-14 19:32:44 +00:00
theories
"$L4V_ARCH/Refine"
"$L4V_ARCH/RAB_FN"
"$L4V_ARCH/EmptyFail_H"
(*
* This theory is in a separate session because the proofs currently
* only work for ARM.
*)
session RefineOrphanage in "refine/$L4V_ARCH/orphanage" = Refine +
2019-06-05 10:18:48 +00:00
description \<open>Proof that the kernel does not orphan threads.\<close>
theories
"Orphanage"
(* FIXME isa
session BaseRefine2 = BaseRefine +
2019-06-05 10:18:48 +00:00
description \<open>Intermediate point in refinement proof. Useful for machines with small RAM.\<close>
theories [condition = "SKIP_AINVS_PROOFS", quick_and_dirty, skip_proofs]
"refine/$L4V_ARCH/Untyped_R"
"refine/$L4V_ARCH/Schedule_R"
theories
"refine/$L4V_ARCH/Untyped_R"
"refine/$L4V_ARCH/Schedule_R"
*)
2014-07-14 19:32:44 +00:00
session BaseRefine in "refine/base" = AInvs +
2019-06-05 10:18:48 +00:00
description \<open>Background theory and libraries for refinement proof.\<close>
sessions
Lib
CorresK
2014-07-14 19:32:44 +00:00
theories
"Include"
2014-07-14 19:32:44 +00:00
session AInvs in "invariant-abstract" = ASpec +
directories
"$L4V_ARCH"
theories [condition = "SKIP_AINVS_PROOFS", quick_and_dirty, skip_proofs]
"KernelInit_AI"
"$L4V_ARCH/ArchDetSchedSchedule_AI"
theories [condition = "AINVS_QUICK_AND_DIRTY", quick_and_dirty]
"KernelInit_AI"
"$L4V_ARCH/ArchDetSchedSchedule_AI"
2014-07-14 19:32:44 +00:00
theories
"KernelInit_AI"
"$L4V_ARCH/ArchDetSchedSchedule_AI"
2014-07-14 19:32:44 +00:00
(*
* C Refinement proof.
*)
(* FIXME isa
session CRefineSyscall = CBaseRefine +
theories [condition = "CREFINE_QUICK_AND_DIRTY", quick_and_dirty]
"crefine/$L4V_ARCH/Syscall_C"
theories
"crefine/$L4V_ARCH/Syscall_C"
*)
session CRefine in "crefine/$L4V_ARCH" = CBaseRefine +
theories [condition = "CREFINE_QUICK_AND_DIRTY", quick_and_dirty]
"Refine_C"
2014-07-14 19:32:44 +00:00
theories
"Refine_C"
2014-07-14 19:32:44 +00:00
session CBaseRefine in "crefine" = CSpec +
sessions
CLib
Refine
AutoCorres
directories
"lib"
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
(* crefine/lib/AutoCorres_C explains why L4VerifiedLinks is included here. *)
"lib/L4VerifiedLinks"
"Include_C"
2014-07-14 19:32:44 +00:00
theories
"lib/L4VerifiedLinks"
"Include_C"
2014-07-14 19:32:44 +00:00
(* FIXME isa
session AutoCorresCRefine = CRefine +
theories
"crefine/$L4V_ARCH/AutoCorresTest"
*)
2014-07-14 19:32:44 +00:00
(*
* CapDL Refinement
*)
session DBaseRefine in "drefine/base" = AInvs +
sessions
DSpec
2014-07-14 19:32:44 +00:00
theories
"Include_D"
2014-07-14 19:32:44 +00:00
session DRefine in "drefine" = DBaseRefine +
2014-07-14 19:32:44 +00:00
theories
"Refine_D"
2014-07-14 19:32:44 +00:00
session DPolicy in "dpolicy" = DRefine +
sessions
Access
2014-07-14 19:32:44 +00:00
theories
"Dpolicy"
2014-07-14 19:32:44 +00:00
(*
* Infoflow and Access
*)
session Access in "access-control" = AInvs +
theories
"ADT_AC"
2014-07-14 19:32:44 +00:00
"ExampleSystem"
session InfoFlow in "infoflow" = Access +
theories
"InfoFlow_Image_Toplevel"
2014-07-14 19:32:44 +00:00
session InfoFlowCBase in "infoflow/tools" = CRefine +
sessions
Refine
Access
InfoFlow
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
"../Include_IF_C"
theories
"../Include_IF_C"
session InfoFlowC = InfoFlowCBase +
2014-07-14 19:32:44 +00:00
theories
"infoflow/Noninterference_Refinement"
"infoflow/Example_Valid_StateH"
2014-07-14 19:32:44 +00:00
(*
* capDL
*)
session SepDSpec in "sep-capDL" = DSpec +
sessions
Sep_Algebra
SepTactics
2014-07-14 19:32:44 +00:00
theories
"Frame_SD"
2014-07-14 19:32:44 +00:00
session DSpecProofs in "capDL-api" = SepDSpec +
sessions
AInvs
2014-07-14 19:32:44 +00:00
theories
"Sep_Tactic_Examples"
"API_DP"
2014-07-14 19:32:44 +00:00
(*
* Static Separation Kernel Bisimilarity
*)
session Bisim in bisim = AInvs +
sessions
ASepSpec
theories
"Syscall_S"
document_files
"root.tex"
"build"
"Makefile"
2014-07-14 19:32:44 +00:00
2014-09-05 09:08:11 +00:00
(*
* Binary Verification Input Step
*)
session SimplExportAndRefine in "asmrefine" = CSpec +
2014-09-05 09:08:11 +00:00
theories
"SEL4SimplExport"
"SEL4GraphRefine"
2014-09-05 09:08:11 +00:00
(* FIXME isa
2015-05-22 03:55:35 +00:00
session SimplExportOnly = CSpec +
theories
"asmrefine/SEL4SimplExport"
*)
2015-05-22 03:55:35 +00:00
2014-07-14 19:32:44 +00:00
(*
* Libraries
*)
(* unused:
2014-07-14 19:32:44 +00:00
session AutoLevity = AutoLevity_Base +
theories
"../lib/autolevity_buckets/AutoLevity_Top"
session AutoLevity_Base = Word_Lib +
2014-07-14 19:32:44 +00:00
theories
"../lib/autolevity_buckets/AutoLevity_Base"
*)