-
Notifications
You must be signed in to change notification settings - Fork 0
/
ROOT
172 lines (134 loc) · 3.18 KB
/
ROOT
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
(*
* 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 "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 = BaseRefine +
description {* Refinement between Haskell and Abstract spec. *}
options [timeout=3600]
theories
"refine/Refine"
"refine/Orphanage"
session BaseRefine = AInvs +
description {* Background theory and libraries for refinement proof. *}
options [timeout=600]
theories
"refine/Include"
session AInvs = ASpec +
options [timeout=3600]
theories
"invariant-abstract/AInvs"
"invariant-abstract/EmptyFail_AI"
"invariant-abstract/KernelInit_AI"
"invariant-abstract/DetSchedSchedule_AI"
(*
* C Refinement proof.
*)
session CRefine = CBaseRefine +
theories
"crefine/Refine_C"
session CBaseRefine = CSpec +
theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
"crefine/Include_C"
theories
"crefine/Include_C"
(*
* CapDL Refinement
*)
session DBaseRefine = Refine +
theories
"drefine/Include_D"
session DRefine = DBaseRefine +
theories
"drefine/Refine_D"
session DPolicy = DRefine +
theories
"access-control/Dpolicy"
(*
* Infoflow and Access
*)
session Access in "access-control" = AInvs +
options [timeout=3600]
theories
"Syscall_AC"
"ExampleSystem"
session InfoFlow in "infoflow" = Access +
theories
"Noninterference"
theories
"Noninterference_Base_Refinement"
"PolicyExample"
"PolicySystemSAC"
"ExampleSystemPolicyFlows"
"Example_Valid_State"
session InfoFlowC = CRefine +
theories
"infoflow/Noninterference_Refinement"
session InfoFlowCCount = InfoFlowC +
theories
"../lib/proof_counting/ProofGraph_Serialize_InfoflowC"
(*
* Separation Kernel
*)
(*
session SepASpec = AInvs +
theories
"sep-abstract/Syscall_SA"
session BiSim in "bisim" = AInvs +
options [document = pdf]
theories
"../sep-abstract/Syscall_SA"
"Syscall_S"
files
"document/root.tex"
*)
(*
* capDL
*)
session SepDSpec = DSpec +
theories
"sep-capDL/Frame_SD"
session DSpecProofs in "capDL-api" = SepDSpec +
theories
"API_DP"
(*
* Separation Logic
*)
session SepTactics = Word +
theories
"../lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics"
session SepTacticsExamples = SepTactics +
theories [quick_and_dirty]
"capDL-api/Sep_Tactic_Examples"
(*
* Libraries
*)
session AutoLevity = AutoLevity_Base +
theories
"../lib/autolevity_buckets/AutoLevity_Top"
session AutoLevity_Base = Word +
theories
"../lib/autolevity_buckets/AutoLevity_Base"