1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8 * CAMKES
9 *)
10
11chapter CAmkES
12
13session CamkesAdlSpec (Camkes) in "adl-spec" = Access +
14  options [document = pdf]
15  theories
16    "Wellformed_CAMKES"
17    "Examples_CAMKES"
18  document_files
19    "imgs/compilation.pdf"
20    "imgs/composite-passthrough.pdf"
21    "imgs/dataport.pdf"
22    "imgs/echo.pdf"
23    "imgs/event.pdf"
24    "imgs/terminal.pdf"
25    "intro.tex"
26    "root.tex"
27    "comment.sty"
28    "ulem.sty"
29
30(* Base session for CAmkES<->CapDL reasoning. This session is intended to be simply a combination
31 * of CamkesAdlSpec and DSpec, and is defined because we can't easily depend on both.
32 *)
33session CamkesCdlBase (Camkes) = DPolicy +
34  sessions
35    DSpec
36    CamkesAdlSpec
37    Lib
38  theories
39    "DSpec.Syscall_D"
40    "CamkesAdlSpec.Wellformed_CAMKES"
41    "CamkesAdlSpec.Examples_CAMKES"
42    "Lib.LemmaBucket"
43
44(* CAmkES<->CapDL reasoning. *)
45session CamkesCdlRefine (Camkes) in "cdl-refine" = CamkesCdlBase +
46  theories
47    Policy_CAMKES_CDL
48    Eval_CAMKES_CDL
49
50session CamkesGlueSpec (Camkes) in "glue-spec" = HOL +
51  options [document = pdf]
52  directories
53    "example-procedure"
54    "example-event"
55    "example-dataport"
56    "example-untrusted"
57    "example-trusted"
58  theories
59    Abbreviations
60    CIMP
61    Connector
62    Types
63    UserStubs
64    "example-procedure/GenSimpleSystem"
65    "example-event/GenEventSystem"
66    "example-dataport/GenDataportSystem"
67    "example-untrusted/EgTop"
68    "example-trusted/EgTop2"
69  document_files
70    "dataport.camkes"
71    "event.camkes"
72    "imgs/echo.pdf"
73    "imgs/filter.pdf"
74    "imgs/thydeps.pdf"
75    "intro.tex"
76    "root.bib"
77    "root.tex"
78    "filter.camkes"
79    "simple.camkes"
80    "comment.sty"
81    "ulem.sty"
82
83session CamkesGlueProofs (Camkes) in "glue-proofs" = AutoCorres +
84  options [document = pdf, quick_and_dirty]
85  theories
86    Syntax
87    RPCFrom
88    RPCTo
89    EventFrom
90    EventTo
91    DataIn
92  document_files
93    "eventfrom-emit-underlying.c"
94    "eventto-poll.c"
95    "eventto-wait.c"
96    "from-echo-int.c"
97    "intro.tex"
98    "root.bib"
99    "root.tex"
100    "simple.camkes"
101    "to-echo-int.c"
102    "comment.sty"
103    "ulem.sty"
104