(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

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 +
  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"
    "$L4V_ARCH/Init_R"
  theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
    "$L4V_ARCH/Refine"
    "$L4V_ARCH/RAB_FN"
    "$L4V_ARCH/EmptyFail_H"
    "$L4V_ARCH/Init_R"
  theories
    "$L4V_ARCH/Refine"
    "$L4V_ARCH/RAB_FN"
    "$L4V_ARCH/EmptyFail_H"
    "$L4V_ARCH/Init_R"

(*
 * This theory is in a separate session because the proofs currently
 * only work for ARM.
 *)
session RefineOrphanage in "refine/$L4V_ARCH/orphanage" = Refine +
  description \<open>Proof that the kernel does not orphan threads.\<close>
  theories
    "Orphanage"

session BaseRefine in "refine/base" = AInvs +
  description \<open>Background theory and libraries for refinement proof.\<close>
  sessions
    Lib
    CorresK
  theories
    "Include"

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"
  theories
    "KernelInit_AI"
    "$L4V_ARCH/ArchDetSchedSchedule_AI"

(*
 * C Refinement proof.
 *)

session CRefineSyscall in "crefine/intermediate" = CBaseRefine +
  sessions
    CRefine
  theories [condition = "CREFINE_QUICK_AND_DIRTY", quick_and_dirty]
    "Intermediate_C"
  theories
    "Intermediate_C"

session CRefine in "crefine" = CBaseRefine +
  directories
    "lib"
    "$L4V_ARCH"
  theories [condition = "CREFINE_QUICK_AND_DIRTY", quick_and_dirty]
    "Refine_C"
  theories
    "Refine_C"

session CBaseRefine in "crefine/base" = CSpec +
  sessions
    CLib
    Refine
    AutoCorres
  theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
    (* crefine/lib/AutoCorres_C explains why L4VerifiedLinks is included here. *)
    "L4VerifiedLinks"
    "Include_C"
  theories
    "L4VerifiedLinks"
    "Include_C"

session AutoCorresCRefine in "crefine/autocorres-test" = CRefine +
  theories
    "AutoCorresTest"

(*
 * CapDL Refinement
 *)

session DBaseRefine in "drefine/base" = AInvs +
  sessions
    DSpec
  theories
    "Include_D"

session DRefine in "drefine" = DBaseRefine +
  theories
    "Refine_D"

session DPolicy in "dpolicy" = DRefine +
  sessions
    Access
  theories
    "Dpolicy"

(*
 * Infoflow and Access
 *)

session Access in "access-control" = AInvs +
  directories
    "$L4V_ARCH"
  theories
    "ArchADT_AC"
    "ExampleSystem"

session InfoFlow in "infoflow" = Access +
  directories
    "$L4V_ARCH"
  theories
    "InfoFlow_Image_Toplevel"

session InfoFlowCBase in "infoflow/refine/base" = CRefine +
  sessions
    Refine
    Access
    InfoFlow
  theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
    "Include_IF_C"
  theories
    "Include_IF_C"

session InfoFlowC in "infoflow/refine" = InfoFlowCBase +
  directories
    "$L4V_ARCH"
  theories
    "Noninterference_Refinement"
    "Example_Valid_StateH"

(*
 * capDL
 *)

session SepDSpec in "sep-capDL" = DSpec +
  sessions
    Sep_Algebra
    SepTactics
  theories
    "Frame_SD"

session DSpecProofs in "capDL-api" = SepDSpec +
  sessions
    AInvs
  theories
    "Sep_Tactic_Examples"
    "API_DP"

(*
 * Static Separation Kernel Bisimilarity
 *)

session Bisim in bisim = AInvs +
  sessions
    ASepSpec
  theories
    "Syscall_S"
  document_files
    "root.tex"
    "build"
    "Makefile"


(*
 * Binary Verification Input Step
*)
session SimplExportAndRefine in "asmrefine" = SimplExport +
  sessions
    SimplExport
  theories
    "SEL4GraphRefine"

session SimplExport in "asmrefine/export" = CSpec +
  directories
    "$L4V_ARCH"
  theories
    "SEL4SimplExport"