-
Notifications
You must be signed in to change notification settings - Fork 0
/
macros.tex
229 lines (219 loc) · 8.83 KB
/
macros.tex
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
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
\ExplSyntaxOn
\DeclareExpandableDocumentCommand{\IfNoValueOrEmptyTF}{mmm}
{
\IfNoValueTF{#1}{#2}
{
\tl_if_empty:nTF {#1} {#2} {#3}
}
}
\ExplSyntaxOff
\newcommand{\TODO}[1]{%
\textcolor{red}{#1}%
}
\newcommand{\BRAINDUMP}[1]{\textcolor{blue}{#1}}
\newcommand{\lang}{Flamio\xspace}
\newcommand{\name}{n}
\newcommand{\Nameset}{\mathcal{N}}
\newcommand{\conj}{\mathrel{\land}}
\newcommand{\disj}{\mathrel{\lor}}
\newcommand{\conf}[1]{#1^{\rightarrow}}
\newcommand{\integ}[1]{#1^{\leftarrow}}
\newcommand{\owner}[2]{#1 \colon \!#2}
\newcommand{\addr}{a}
\newcommand{\Attacker}{\mathcal{A}}
\newcommand{\Loc}{\mathsf{Loc}}
\newcommand{\val}{v}
\newcommand{\expr}{e}
\newcommand{\Var}{\mathsf{Var}}
\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}
\newcommand{\abs}[4]{\lambda^{#1}_{#2}\,#3.\,#4}
\newcommand{\lb}[2]{#2 \mathbin{@} #1}
\newcommand{\type}{\tau}
\newcommand{\consop}{\mathbin{::}}
\newcommand{\cons}[2]{#1 \consop #2}
\newcommand{\nil}{\mathsf{nil}}
\newcommand{\liokw}{\mathsf{LIO}}
\newcommand{\lio}[1]{(#1)^{\liokw}}
\newcommand{\app}[2]{#1\;#2}
\newcommand{\proj}[2]{\pi_{#1}\,#2}
\newcommand{\ifkw}{\mathsf{if}}
\newcommand{\thenkw}{\mathsf{then}}
\newcommand{\elsekw}{\mathsf{else}}
\newcommand{\ifexpr}[3]{\ifkw\;#1\;\thenkw\;#2\;\elsekw\;#3}
\newcommand{\casekw}{\mathsf{case}}
\newcommand{\ofkw}{\mathsf{of}}
\newcommand{\case}[3]{\casekw\;#1\;\ofkw\;#2\;#3}
\newcommand{\fixkw}{\mathsf{fix}}
\newcommand{\fix}[1]{\fixkw\;#1}
\newcommand{\returnkw}{\mathsf{return}}
\newcommand{\return}[1]{\returnkw\;#1}
\newcommand{\bindop}{\ensuremath{\gg=}}
\newcommand{\bind}[2]{#1 \bindop #2}
\DeclareMathOperator{\readrefkw}{!}
\newcommand{\readref}[1]{\readrefkw #1}
\newcommand{\writeref}[2]{#1 := #2}
\newcommand{\getlabel}{\mathsf{getLabel}}
\newcommand{\getclearance}{\mathsf{getClearance}}
\newcommand{\labelofkw}{\mathsf{labelOf}}
\newcommand{\labelof}[1]{\labelofkw\;#1}
\newcommand{\newkw}{\mathsf{new}}
\newcommand{\new}[2]{\newkw\;#1\;#2}
\newcommand{\labelkw}{\mathsf{label}}
\newcommand{\Label}[2]{\labelkw\;#1\;#2}
\newcommand{\unlabelkw}{\mathsf{unlabel}}
\newcommand{\unlabel}[1]{\unlabelkw\;#1}
\newcommand{\tolabeledkw}{\mathsf{toLabeled}}
\newcommand{\tolabeled}[2]{\tolabeledkw\;#1\;#2}
\newcommand{\withscopekw}{\mathsf{withScope}}
\newcommand{\withscope}[1]{\withscopekw\;#1}
\newcommand{\withstrategykw}{\mathsf{withStrategy}}
\newcommand{\withstrategy}[2]{\withstrategykw\;#1\;#2}
\newcommand{\adddelegatekw}{\mathsf{assume}}
\newcommand{\adddelegate}[3]{\adddelegatekw\;(#1 \actsfor #2) \;@ \; #3}
\newcommand{\removedelegatekw}{\mathsf{discard}}
\newcommand{\removedelegate}[3]{\removedelegatekw\;(#1 \actsfor #2)\;#3}
\newcommand{\getstrategy}{\mathsf{getStrategy}}
\newcommand{\actsfor}{\succcurlyeq}
\NewDocumentCommand{\wait}{O{}}{\mathsf{wait}(#1)}
\newcommand{\resetstrategy}[2]{\mathsf{resetStrategy}_{#1}(#2)}
\newcommand{\resetscope}[2]{\mathsf{resetScope}_{#1}(#2)}
\NewDocumentCommand{\internalTolabeled}{ O{} m m m }{\tolabeledkw^{#1}_{#2}\;#3\;#4}
\newcommand{\scope}{\Delta}
\newcommand{\termsym}{\bullet}
\newcommand{\bool}{\mathsf{Bool}}
\newcommand{\unit}{\mathsf{Unit}}
\newcommand{\String}{\mathsf{String}}
\newcommand{\Integer}{\mathsf{Int}}
\newcommand{\lbool}{\mathsf{LBool}}
\newcommand{\lunit}{\mathsf{LUnit}}
\newcommand{\lString}{\mathsf{LString}}
\newcommand{\lInteger}{\mathsf{LInt}}
\newcommand{\func}[2]{#1 \to #2}
\newcommand{\pair}[2]{#1 \times #2}
\newcommand{\listtype}[1]{\lbrack#1\rbrack}
\newcommand{\labeltype}{\mathsf{Principal}}
\newcommand{\llabeltype}{\mathsf{LPrincipal}}
\newcommand{\labeledkw}{\mathsf{Labeled}}
\newcommand{\labeled}[1]{\labeledkw\,#1}
\newcommand{\liotype}[1]{\liokw\,#1}
\newcommand{\refkw}{\mathsf{Ref}}
\newcommand{\lrefkw}{\mathsf{LRef}}
\NewDocumentCommand{\reftype}{ O{} m}{\refkw_{#1}\,#2}
\newcommand{\store}{\phi}
\newcommand{\altstore}{\psi}
\newcommand{\ruleref}[1]{\textsc{#1}}
\definecolor{verylightgray}{rgb}{0.9,0.9,0.9}
\newcommand{\graybox}[1]{\fcolorbox{white}{verylightgray}{\ensuremath{#1}}}
\NewDocumentCommand{\stepsto}{ O{} O{} }{\xrightarrow[#1]{\mathmakebox[1em]{#2}}}
\NewDocumentCommand{\steppure}{O{} O{} m m }{#3 \stepsto[#1][#2] #4}
\newcommand{\ectx}{E}
\newcommand{\hole}{\lbrack \bullet \rbrack}
\newcommand{\efill}[1]{\ectx\lbrack #1 \rbrack}
\newcommand{\hd}{\mathsf{hd}}
\newcommand{\tl}{\mathsf{tl}}
\newcommand{\cur}{\level_{\mathsf{cur}}}
\newcommand{\clr}{\level_{\mathsf{clr}}}
\newcommand{\config}[2]{\langle #1 \mid #2 \rangle}
\NewDocumentCommand{\step}{ m O{} O{} m m m }{#1 \vdash #4 \stepsto[#2][#3] #5 : #6}
\newcommand{\env}{\Sigma}
\newcommand{\lblkw}{\mathsf{lbl}}
\NewDocumentCommand{\flowstoquery}{mommm}{
#1 \IfNoValueTF{#2}{\vdash}{\vdash_{#2}} #3 \flowsto #4 \IfNoValueOrEmptyTF{#5}{}{: #5}
}
\newcommand{\flowsto}{\sqsubseteq}
\newcommand{\nflowsto}{\not\flowsto}
\newcommand{\level}{\ell}
\newcommand{\extend}[3]{#1 \left\lbrack #2 \mapsto #3 \right\rbrack}
\newcommand{\join}{\sqcup}
\newcommand{\bigjoin}{\bigsqcup}
\newcommand{\meet}{\sqcap}
\newcommand{\dom}{\mathsf{dom}}
\newcommand{\nopostflowstoquery}[3]{#1 \vdash #2 \flowsto #3}
\newcommand{\nopostactsforquery}[3]{#1 \vdash #2 \actsfor #3}
\NewDocumentCommand{\actsforquery}{mommm}{
#1 \IfNoValueTF{#2}{\vdash}{\vdash_{#2}} #3 \actsfor #4 \IfNoValueOrEmptyTF{#5}{}{: #5}
}
\NewDocumentCommand{\notactsforquery}{momm}{
#1 \IfNoValueTF{#2}{\vdash}{\vdash_{#2}} #3 \actsfor #4 : \mathsf{fail}
}
\newcommand{\strategy}{\mathsf{strat}}
\NewDocumentCommand{\stratelem}{s}{
\IfBooleanTF{#1}{\mathsf{ss}}{\mathsf{s}}
}
\newcommand{\option}[1]{#1^?}
\newcommand{\none}{\circ}
\newcommand{\voicekw}{\nabla}
\newcommand{\voice}[1]{\voicekw(#1)}
\newcommand{\extends}[2]{#1 \left\lbrack #2 \right\rbrack}
\newcommand{\actsforquerycount}[5]{#1 \vdash^{#5} #2 \actsfor #3 : #4}
\newcommand{\nopostnotflowstoquery}[3]{#1 \vdash #2 \not\flowsto #3}
\newcommand{\gconfig}[3]{\llparenthesis #1, #2, #3 \rrparenthesis}
\NewDocumentCommand{\gstepsto}{ O{} O{} }{\xRightarrow[#1]{\mathmakebox[1em]{#2}}}
\NewDocumentCommand{\gstepstos}{ O{} O{} O{*} }{{\xRightarrow[#1]{\IfNoValueOrEmptyTF{#2}{\mathmakebox[1em]{}}{\mathmakebox[\maxof{\widthof{\ensuremath{#2}}-1.2em}{1em}]{#2}}}{}\!\!^{#3}}}
\newcommand{\Assumps}{\mathcal{H}}
\newcommand{\authproj}[1]{#1^{\pi}}
\WithSuffix\newcommand\actsforquerymany*[5]{#1 \vdash^*_{#2} #3 \actsfor #4 : #5}
\newcommand{\actsforquerysmany}[5]{#1 \vdash_{#2} #3 \actsfor #4 : #5}
\NewDocumentCommand{\hastype}{ O{} m m m }{#2 \vdash_{#1} #3 : #4}
\newcommand{\tenv}{\Gamma}
\newcommand{\wf}[2]{#1 \vdash #2}
\newcommand{\botinfoflow}{\bot^{\!\!\scalebox{0.5}[0.5]{$\flowsto$}}}
\newcommand{\topinfoflow}{\top_{\!\!\scalebox{0.5}[0.5]{$\flowsto$}}}
\newcommand{\noevent}{\varepsilon}
\newcommand{\writeeventkw}{\mathsf{write}}
\newcommand{\neweventkw}{\mathsf{new}}
\newcommand{\calleventkw}{\mathsf{call}}
\newcommand{\returneventkw}{\mathsf{ret}}
\newcommand{\releaseeventkw}{\mathsf{release}}
\newcommand{\writeevent}[2]{\writeeventkw(#1, #2)}
\newcommand{\newevent}[2]{\neweventkw(#1, #2)}
\newcommand{\callevent}[2]{\calleventkw(#1, #2)}
\newcommand{\returnevent}[2]{\returneventkw(#1, #2)}
\newcommand{\releaseevent}[3]{\releaseeventkw(#1, #2, #3)}
\newcommand{\event}{\mathit{ev}}
\newcommand{\good}[2]{#1 \vdash \mathsf{good}(#2)}
\newcommand{\bad}[2]{#1 \vdash \mathsf{bad}(#2)}
\newcommand{\globalstore}{\Phi}
\newcommand{\altglobalstore}{\Psi}
\newcommand{\emptytrace}{\varepsilon}
\newcommand{\filtertrace}{\leadsto}
\NewDocumentCommand{\traceloweq}{m m m O{} }{#1 \simeq_{#2}^{#4} #3}
\NewDocumentCommand{\loweq}{ m m O{} m m }{#1 \vdash #4 \simeq_{#2}^{#3} #5}
\newcommand{\emptyenv}{\varnothing}
\newcommand{\nodelegations}{\nil}
\newcommand{\bijection}{\theta}
\newcommand{\partialto}{\rightharpoonup}
\NewDocumentCommand{\termknowledge}{mO{\Attacker}}{k^{\downarrow#1}_{#2}}
\NewDocumentCommand{\knowledge}{mO{\Attacker}}{k^{#1}_{#2}}
\definecolor{bluekeywords}{rgb}{0.13, 0.13, 1}
\definecolor{greencomments}{rgb}{0, 0.5, 0}
\definecolor{redstrings}{rgb}{0.9, 0, 0}
\definecolor{graynumbers}{rgb}{0.5, 0.5, 0.5}
\lstset{
numbers=left,
stepnumber=1,
columns=fullflexible,
showspaces=false,
showtabs=false,
numbersep=15pt,
breaklines=true,
showstringspaces=false,
breakatwhitespace=true,
escapeinside={(*@}{@*)},
commentstyle=\color{greencomments},
keywordstyle=\color{bluekeywords},
stringstyle=\color{redstrings},
%numberstyle=\color{greencomments},
basicstyle=\ttfamily\footnotesize,
frame=l,
framesep=12pt,
xleftmargin=12pt,
tabsize=4,
captionpos=b,
emph={%
true, false, nil, if, then, else, case, of, fix, return, new, label, unlabel, toLabeled, getLabel, getClearance, labelOf, withScope, withStrategy, assume, discard, getStrategy, wait, resetStrategy, resetScope, Bool, Unit, Principal, Labeled, LIO, Ref, LBool, LUnit, LPrincipal, LString, LLabeled, LLIO, LRef, let, in, do
},
emphstyle={\bfseries}
}
\newtheorem{theorem}{Theorem}[section]