(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * This software may be distributed and modified according to the terms of
 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
 * See "LICENSE_GPLv2.txt" for details.
 *
 * @TAG(GD_GPL)
 *)

chapter "Specifications"

(*
 * 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.
 *)

(*
 * Abstract Specification
 *)

(* Session on which most other sessions build. *)
session ASpec in "abstract" = Word_Lib +
  options [document=false]
  sessions
    "HOL-Library"
    Lib
    ExecSpec
  theories
    "Syscall_A"

(* We build the abstract specification document in a separate session,
   to avoid rebuilding ASpec (and every session that depends on it)
   whenever the git commit ID changes. *)
session ASpecDoc in "abstract" = Word_Lib +
  options [document=pdf]
  sessions
    "HOL-Library"
    Lib
    ExecSpec
  theories
    "Intro_Doc"
  theories
    "Syscall_A"
    "Glossary_Doc"
    (* "KernelInit_A" *)
  document_files
    "VERSION"    (* generated by `make ASpec` *)
    "gitrev.tex" (* generated by `make ASpec` *)
    "root.tex"
    "root.bib"
    "defs.bib"
    "ulem.sty"
    "imgs/CDT.pdf"
    "imgs/seL4-background_01.pdf"
    "imgs/seL4-background_03.pdf"
    "imgs/seL4-background_04.pdf"
    "imgs/sel4objects_01.pdf"
    "imgs/sel4objects_05.pdf"
    "imgs/sel4_internals_01.pdf"
  document_files (in "document/$L4V_ARCH")
    "ARCH.tex"

(*
 * Executable/Design Specification
 *)

session ExecSpec = Word_Lib +
  options [document = false]
  sessions
    Lib
    "HOL-Eisbach"
  theories
    "design/API_H"
    "design/$L4V_ARCH/ArchIntermediate_H"


(*
 * C Kernel
 *)

session CSpec = CKernel +
  theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty]
    "cspec/Substitute"
  theories [condition = "SORRY_BITFIELD_PROOFS", quick_and_dirty]
    "cspec/KernelInc_C"
  theories
    "cspec/KernelInc_C"
    "cspec/KernelState_C"

session CKernel = CParser +
  sessions
    "ExecSpec"
    "CLib"
    "AsmRefine"
  theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty]
    "cspec/$L4V_ARCH/Kernel_C"
  theories
    "cspec/$L4V_ARCH/Kernel_C"


(*
 * CapDL
 *)

session DSpec in capDL = Word_Lib +
  sessions
    ExecSpec
    ASpec
  theories
    Syscall_D


(*
 * Take-Grant.
 *)

session TakeGrant in "take-grant" = Word_Lib +
  theories
    "System_S"
    "Isolation_S"
    "Example"
    "Example2"


(*
 * Separation Kernel Setup Specification
 *)

session ASepSpec = ASpec +
  options [document = false]
  theories
    "sep-abstract/Syscall_SA"