-
Notifications
You must be signed in to change notification settings - Fork 3
/
mmmacros.sty
455 lines (398 loc) · 22 KB
/
mmmacros.sty
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
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
% requires extpfeil package
\newextarrow{\injectc}{5599}{\succ\relbar\rightarrow}
\usetikzlibrary{calc,decorations.pathmorphing,shapes}
\newcounter{sarrow}
\newcommand\xrsquigarrow[1]{%
\stepcounter{sarrow}%
\mathrel{\begin{tikzpicture}[baseline= {( $ (current bounding box.south) + (0,-0.5ex) $ )}]
\node[inner sep=.5ex] (\thesarrow) {$\scriptstyle #1$};
\path[draw,<-,decorate,
decoration={zigzag,amplitude=0.7pt,segment length=1.2mm,pre=lineto,pre length=4pt}]
(\thesarrow.south east) -- (\thesarrow.south west);
\end{tikzpicture}}%
}
\newenvironment{importantthm}[1][]{\textbf{Theorem~\refstepcounter{theoremcounter}~(#1).~}\begin{scontents}[store-env=buffer]}{\end{scontents}\getstored{buffer}\medskip}
\newcommand*{\incompleteproofname}{Proof}
\newenvironment{incompleteproof}[1][\incompleteproofname]{\begin{proof}[#1]\renewcommand*{\qedsymbol}{\fbox{}}}{\end{proof}}
\newcommand{\mi}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\mr}[1]{\ensuremath{\mathrm{#1}}}
\newcommand{\mt}[1]{\ensuremath{\texttt{#1}}}
\newcommand{\mtt}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\mf}[1]{\ensuremath{\mathbf{#1}}}
\newcommand{\mk}[1]{\ensuremath{\mathfrak{#1}}}
\newcommand{\mc}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\ms}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\mb}[1]{\ensuremath{\mathbb{#1}}}
\newcommand{\msc}[1]{\ensuremath{\mathscr{#1}}}
%\newcommand{\myfig}[3]{\begin{figure} [!ht]
%#1
%\caption{\label{fig:#2}#3}
%\end{figure}}
\newcounter{pseudofigcounter}
\crefalias{pseudofig}{pseudofigcounter}
\crefname{pseudofig}{Figure}{Figures}
\newcommand{\myfig}[3]{%
\noindent
\begin{minipage}{\textwidth}
\begin{center}
\fbox{\begin{minipage}{\textwidth}
\begin{center}
#1
\end{center}
\end{minipage}}
$\;$\\
\parbox{\textwidth}{Figure \refstepcounter{pseudofigcounter}\thepseudofigcounter:\label[pseudofig]{fig:#2} #3}
\end{center}
\end{minipage}
$\;$\\
}
\newcommand{\textgraybox}[1]{\boxed{#1}}
\newdimen\zzfontsz
\newcommand{\fontsz}[2]{\zzfontsz=#1%
{\fontsize{\zzfontsz}{1.2\zzfontsz}\selectfont{#2}}}
\newcommand{\mathsz}[2]{\text{\fontsz{#1}{$#2$}}}
\newcommand{\instsymColon}{%
\raisebox{-0.09ex}{\text{\normalfont{:}}}}
\newcommand{\judgboxfontsize}[1]{%
\mathsz{11pt}{#1}%
}
\newcommand{\judgbox}[2]{%
{\raggedright \textgraybox{\ensuremath{\judgboxfontsize{#1}}}\!%
\fontsz{9pt}{\begin{tabular}[c]{l} #2 \end{tabular}} %
}}
\newcounter{typerule}
\crefname{typerule}{rule}{rules}
\newcommand{\typeruleInt}[5]{%
\def\thetyperule{#1}%
\refstepcounter{typerule}%
\label{tr:#4}%
%
\ensuremath{\begin{array}{c}#5 \inference{#2}{#3}\end{array}}
}
\newcommand{\typerule}[4]{%
\typeruleInt{#1}{#2}{#3}{#4}{\textsf{\scriptsize ({#1})} \\ }
}
\newcommand{\typerulenolabel}[3]{%
\def\thetyperule{#1}%
\refstepcounter{typerule}%
\ensuremath{\begin{array}{c} \inference{#2}{#3}\end{array}}
}
\newcommand{\typerulederiv}[3]{%
\ensuremath{\begin{array}{c} \inference{#2}{#3} #1\end{array}}
}
\newcommand{\nat}[0]{\ensuremath{\mb{N}}\xspace}
\newcommand{\arr}[0]{\ensuremath{\mb{A}}\xspace}
\newcommand\bnfdef{\ensuremath{\mathrel{::=}}}
\newcommand{\hole}[1]{\ensuremath{\left[#1\right]}}
\newcommand{\Gammas}[0]{\src{\Gamma}\xspace}
\newcommand{\Deltas}[0]{\src{\Delta}\xspace}
\newcommand{\Deltat}[0]{\trg{\Delta}\xspace}
\newcommand{\propositions}{\ensuremath\bm{P}}
\newcommand{\powerset}[1]{\mathscr{P}\left({#1}\right)}
\newcommand{\partials}{\ensuremath\mathcal{P}}
\newcommand{\wholes}{\ensuremath\mathcal{W}}
\newcommand{\wellf}{\vdash_{\text{\tiny W}}}
\newcommand{\singlestep}{\stackrel{e}{\hookrightarrow}}
\newcommand{\linker}{\mathrel\blacktriangleright\joinrel\mathrel\blacktriangleleft}
\newcommand{\emptyevent}{\varepsilon}
\newcommand{\terminationevent}{\lightning}
\newcommand{\estep}[3]{{#1}\stackrel{#2}{\hookrightarrow}{#3}}
\newcommand{\step}[2]{{#1}\hookrightarrow{#2}}
\newcommand{\terminates}[1]{{#1}\Downarrow}
\newcommand{\seqnil}{\cdot}
\newcommand{\seqcons}[2]{{{#1}:{\kern-6.25pt}:{#2}}}
\newcommand{\valueexpr}{v}
\newcommand{\finalexprnoerr}{f}
\newcommand{\finalexpr}{f_{\lightning}}
\newcommand{\type}{\tau}
\newcommand{\types}{\src{\type}}
\newcommand{\events}{E\cup\{\lightning\}}
\newcommand{\behav}[1]{\text{Behav}({#1})}
\newcommand{\event}[1][]{a#1}
\newcommand{\absevent}[1][]{\bm{a}#1}
\newcommand{\trace}[1][]{\overline{a#1}}
\newcommand{\abstrace}[1][]{\bm{\overline{a}}#1}
\newcommand{\mstrace}[1][]{\overline{a^{\text{\tiny ms}}#1}}
\newcommand{\sccttrace}[1][]{\overline{a^{\text{\tiny scct}}#1}}
\newcommand{\spectrace}[1][]{\overline{a^{\mathghost}#1}}
\newcommand{\msevent}[1][]{a^{\text{\tiny ms}}#1}
\newcommand{\scctevent}[1][]{a^{\text{\tiny scct}}#1}
\newcommand{\specevent}[1][]{a^{\mathghost}#1}
\newcommand{\mktrace}[2]{{#1}\leadsto{#2}}
\newcommand{\prop}{\pi}
\newcommand{\traces}{\text{Traces}}
\newcommand{\lift}[1]{\left\lceil{#1}\right\rceil}
\newcommand{\policy}{\text{Policy}}
\newcommand{\abstermination}{\lightning{\kern-5.7pt}\lightning}
\newcommand{\fresh}[2]{{#1}\vdash {#2}\ \textit{fresh}\xspace}
\newcommand{\dontcare}[2]{{#1}\vdash {#2}\ \textit{trash}\xspace}
\newcommand{\loweq}[2]{{#1}=_L{#2}}
\newcommand{\selfcompo}[2]{{#1}\thicksim{#2}}
\newcommand{\classcollapse}{\star}
\newcommand{\collapse}[1]{{#1}^{\classcollapse}}
\newcommand{\class}[1]{\mathbb{#1}}
\newcommand{\cC}{\class{C}}
\newcommand{\cSafety}{\text{Safety}}
\newcommand{\cHSafety}{\text{HyperSafety}}
\newcommand{\cTwoHSafety}{\text{2-HyperSafety}}
\newcommand{\cKHSafety}{\text{K-HyperSafety}}
\newcommand{\cSS}{\text{SSC}}
\newcommand{\mutex}{\text{MutEx}}
\newcommand{\nonterm}{\text{Nontermination}}
\newcommand{\determ}{\text{Determinism}}
\renewcommand{\ss}{\text{SS}}
\newcommand{\rss}{\text{RSS}}
\newcommand{\Ni}{\text{NI}}
\newcommand{\RNi}{\text{RNI}}
\newcommand{\nvOne}{\text{No-v1}}
\newcommand{\nvFour}{\text{No-v4}}
\newcommand{\nvOneFour}{\text{No-v1-v4}}
\newcommand{\fccomp}[2]{{#1}\overset{\bullet}{\cap}{#2}}
\newcommand{\fcleq}[2]{{#1}\overset{\bullet}{\subseteq}{#2}}
\newcommand{\sat}[2]{{#1}\vDash{#2}}
\newcommand{\nsat}[2]{{#1}\not\vDash{#2}}
\newcommand{\rsat}[2]{{#1}\vDash_{\scriptstyle R}{#2}}
\newcommand{\nrsat}[2]{{#1}\not\vDash_{\scriptstyle R}{#2}}
\newcommand{\instr}[2]{{#1}\injectc[]{}{#2}}
\newcommand{\sinstr}[3]{{#1}\injectc[]{#2}{#3}}
\newcommand{\neutcol}[0]{black}
\newcommand{\stlccol}[0]{RoyalBlue}
\newcommand{\irccol}[0]{Apricot} %CarnationPink} %Apricot}
\newcommand{\ulccol}[0]{RedOrange}
\newcommand{\objcol}[0]{Emerald} %CarnationPink}
\newcommand{\irdcol}[0]{CarnationPink}
\newcommand{\commoncol}[0]{black}
\newcommand{\col}[2]{\ensuremath{{\color{#1}{#2}}}}
\newcommand{\com}[1]{\ensuremath\mathit{\col{\neutcol}{#1}}}
\newcommand{\src}[1]{\ensuremath\mathsf{\col{\stlccol}{#1}}}
\newcommand{\irl}[1]{\ensuremath\mathit{\col{\irccol}{#1}}}
\newcommand{\trg}[1]{\ensuremath\mathbf{\col{\ulccol}{#1}}}
\newcommand{\obj}[1]{\ensuremath\mathtt{\col{\objcol}{#1}}}
\newcommand{\ird}[1]{\ensuremath\mathsf{\col{\irdcol}{#1}}}
\renewcommand{\S}{\src{S}}
\newcommand{\I}{\irl{I}}
\newcommand{\T}{\trg{T}}
\renewcommand{\O}{\obj{O}}
\newcommand{\full}{\src{1}}
\newcommand{\half}{\src{\sfrac{1}{2}}}
\newcommand{\ptr}{\src{ref_\full\ \nat}}
\newcommand{\wptr}{\src{ref_\half\ \nat}}
\newcommand{\poison}{\rho}
\newcommand{\poisoned}{\text{\Biohazard}}
\newcommand{\poisonless}{\square}
\newcommand{\specificev}[1]{\underline{#1}}
\newcommand{\specificevs}[1]{\src{\underline{#1}}}
\newcommand{\specificevt}[1]{\trg{\underline{#1}}}
\newcommand{\thetospecificfilter}{\theta}
\newcommand{\tospecificev}[1]{\thetospecificfilter\left({#1}\right)}
\newcommand{\tospecificevs}[2][]{\thetospecificfilter#1\left(\src{#2}\right)}
\newcommand{\tospecificevo}[2][]{\thetospecificfilter#1\left(\obj{#2}\right)}
\newcommand{\tospecificevt}[2][]{\thetospecificfilter#1\left(\trg{#2}\right)}
\newcommand{\tospecificevi}[2][]{\thetospecificfilter#1\left(\irl{#2}\right)}
\newcommand{\tospecificevctx}[1]{\thetospecificfilter_{\text{ctx}}\left({#1}\right)}
\newcommand{\tospecificevctxs}[1]{\thetospecificfilter_{\text{ctx}}\left(\src{#1}\right)}
\newcommand{\tospecificevctxt}[1]{\thetospecificfilter_{\text{ctx}}\left(\trg{#1}\right)}
\newcommand{\tospecificevcomps}[1]{\thetospecificfilter_{p}\left(\src{#1}\right)}
\newcommand{\tospecificevcompt}[1]{\thetospecificfilter_{p}\left(\trg{#1}\right)}
\newcommand{\tenc}[1]{\trg{\lfloor} {#1} \trg{\rfloor}}
\newcommand{\stinterp}{\trg{\mathbb{i}}^{\S}}
\newcommand{\ttspec}[1]{\trg{\llbracket{#1}\rrbracket}^{\T\to\T}}
% Different compilers; color automatically applied
\newcommand{\stcomp}[1]{\llbracket\src{#1}\rrbracket^{\S\to\T}}
\newcommand{\sicomp}[1]{\llbracket\src{#1}\rrbracket^{\S\to\I}}
\newcommand{\itcomp}[1]{\llbracket\irl{#1}\rrbracket^{\I\to\T}}
\newcommand{\ttcomp}[1]{\llbracket\trg{#1}\rrbracket^{\T\to\T}}
\newcommand{\sitcomp}[1]{\llbracket\src{#1}\rrbracket^{\S\to\I\to\T}}
\newcommand{\uhcsitcomp}[1]{\llbracket{#1}\rrbracket^{\S+\I\to\T}}
\newcommand{\lhcsitcomp}[1]{\llbracket\src{#1}\rrbracket^{\S\to\I+\T}}
\newcommand{\lhcsiocomp}[1]{\llbracket\src{#1}\rrbracket^{\S\to\I+\O}}
\newcommand{\uhciotcomp}[1]{\llbracket{#1}\rrbracket^{\I+\O\to\T}}
% same compilers, but color not automatically applied
\newcommand{\stcompN}[1]{\llbracket{#1}\rrbracket^{\S\to\T}}
\newcommand{\sicompN}[1]{\llbracket{#1}\rrbracket^{\S\to\I}}
\newcommand{\itcompN}[1]{\llbracket{#1}\rrbracket^{\I\to\T}}
\newcommand{\ttcompN}[1]{\llbracket{#1}\rrbracket^{\T\to\T}}
\newcommand{\thexlangtraceeq}[1][\delta,\src{X}]{\approxeq^*_{#1}\xspace}
\newcommand{\thexlangeventeq}[1][\delta]{\approxeq_{#1}\xspace}
\newcommand{\xlangeventeq}[3][\delta]{\src{#2}\thexlangeventeq[#1]\trg{#3}\xspace}
\newcommand{\xlangeventeqc}[3][\delta]{\irl{#2}\thexlangeventeq[#1]\obj{#3}\xspace}
\newcommand{\xlangtraceeq}[3][\delta;\src{X}]{\src{#2}\thexlangtraceeq[#1]\trg{#3}\xspace}
\newcommand{\xlangtraceeqc}[3][]{\irl{#2}\thexlangtraceeq[#1]\obj{#3}\xspace}
\newcommand{\xlangtraceneq}[3][\delta;\src{X}]{\src{#2}\not\thexlangtraceeq[#1]\trg{#3}\xspace}
\newcommand{\xlangtraceeqn}[3][\delta;\src{X}]{{#2}\thexlangtraceeq[#1]{#3}\xspace}
\newcommand{\thexlangstateeq}[1][\delta;\src{L}]{\approx_{#1}\xspace}
\newcommand{\xlangstateeq}[3][\delta;\src{L}]{\src{#2}\thexlangstateeq[#1]\trg{#3}\xspace}
\newcommand{\xlangstateeqc}[3][\delta_{scct}]{\irl{#2}\thexlangstateeq[#1]\obj{#3}\xspace}
\newcommand{\xlangstateneq}[3][\delta;\src{L}]{\src{#2}\not\thexlangstateeq[#1]\trg{#3}\xspace}
\newcommand{\thexlangbackstateeq}[1][\delta;\src{L}]{\multimap_{#1}\xspace}
\newcommand{\xlangbackstateeq}[3][\delta;\src{L}]{\trg{#2}\thexlangbackstateeq[#1]\src{#3}\xspace}
\newcommand{\xlangbackstateeqc}[3][\delta_{scct}]{\irl{#2}\thexlangbackstateeq[#1]\obj{#3}\xspace}
\newcommand{\tmssafe}{\ensuremath\operatorname{tms}}
\newcommand{\smssafe}{\ensuremath\operatorname{sms}}
\newcommand{\mssafe}{\ensuremath\operatorname{ms}}
\newcommand{\scctsafe}{\ensuremath\operatorname{scct}}
\newcommand{\ctsafe}{\ensuremath\operatorname{ct}}
\newcommand{\specsafe}{\ensuremath\operatorname{spec}}
\newcommand{\specmssafe}{\ensuremath\operatorname{MS}\mathghost}
\newcommand{\Ltms}{\ensuremath\src{L_{\tmssafe}}}
\newcommand{\Ltrg}{\ensuremath\trg{L}}
\newcommand{\Lms}{\ensuremath\irl{L_{\mssafe}}}
\newcommand{\Lscct}{\ensuremath\obj{L_{\scctsafe}}}
\newcommand{\Lspec}{\ensuremath\ird{L_{\mathghost}}}
\newcommand{\mmlAtmmlAtmscomp}[1]{\llbracket\trg{#1}\rrbracket^{\mmlAt\to\mmlAtms}\xspace}
\newcommand{\dcecomp}[1]{\llbracket\irl{#1}\rrbracket_{dce}^{\mmlAtms\to\mmlAtms}\xspace}
\newcommand{\cfcomp}[2][\overline{\rho}]{\llbracket\irl{#2},\irl{#1}\rrbracket_{cf}^{\mmlAtms\to\mmlAtms}\xspace}
\newcommand{\mmlAtmsmmlAtscctcomp}[1]{\llbracket\irl{#1}\rrbracket^{\mmlAtms\to\mmlAtscct}\xspace}
\newcommand{\mmlAtscctmmlAspeccomp}[1]{\llbracket\obj{#1}\rrbracket^{\mmlAtscct\to\mmlAspec}\xspace}
\newcommand{\mmlAmmlAtcomp}[1]{\llbracket\src{#1}\rrbracket^{\mmlAs\to\mmlAt}\xspace}
\newcommand{\mmlAmmlAtcompN}[1]{\llbracket{#1}\rrbracket^{\mmlAs\to\mmlAt}\xspace}
\newcommand{\CRhash}{\texttt{CR}^\#\xspace}
\newcommand{\sCCT}{\texttt{sCCT}\xspace}
\newcommand{\varmapbacktransds}{\texttt{VarMap}\xspace}
\newcommand{\mmlAmmlAtback}[2][\Game]{\langle{\kern-1.5pt}\langle{\kern-1.5pt}\langle\trg{#2}\rangle{\kern-1.5pt}\rangle{\kern-1.5pt}\rangle^{\mmlAt\to\mmlAs}_{#1}\xspace}
\newcommand{\mmlAmmlAtbackcomptoctx}[2][\Game]{\ensuremath\:^{\trg{\comptoctx}}{\kern-2.5pt}\langle{\kern-1.5pt}\langle\trg{#2}\rangle{\kern-1.5pt}\rangle_{#1}^{\mmlAt\to\mmlAs}\xspace}
\newcommand{\mmlAmmlAtbackctxtocomp}[2][\Game]{\ensuremath\:^{\trg{\ctxtocomp}}{\kern-2.5pt}\langle{\kern-1.5pt}\langle\trg{#2}\rangle{\kern-1.5pt}\rangle_{#1}^{\mmlAt\to\mmlAs}\xspace}
\newcommand{\mmlAmmlAtbacksubtop}[2][\Game]{\ensuremath\:^{\trg{\comptoctx\ctxtocomp}}{\kern-2.5pt}\langle{\kern-1.5pt}\langle\trg{#2}\rangle{\kern-1.5pt}\rangle_{#1}^{\mmlAt\to\mmlAs}\xspace}
\newcommand{\mmlAmmlAtbackdetail}[2][\Game]{\ensuremath\langle{\kern-1.5pt}\langle\trg{#2}\rangle{\kern-1.5pt}\rangle_{#1}^{\mmlAt\to\mmlAs}\xspace}
\newcommand{\mmlAmmlAtbackv}[2][\Game]{\langle{\kern-1.5pt}\langle{\kern-1.5pt}\langle\trg{#2}\rangle{\kern-1.5pt}\rangle{\kern-1.5pt}\rangle{\kern-1.5pt}_{#1}^{\mmlAt\to\mmlAs}\xspace}
\newcommand{\mmlAtmsmmlAtscct}[2][\Game]{\langle{\kern-1.5pt}\langle{\kern-1.5pt}\langle\obj{#2}\rangle{\kern-1.5pt}\rangle{\kern-1.5pt}\rangle^{\mmlAtscct\to\mmlAtms}_{#1}\xspace}
\newcommand{\mmlAtmsmmlAtscctcomptoctx}[2][\Game]{\ensuremath\:^{\obj{\comptoctx}}{\kern-2.5pt}\langle{\kern-1.5pt}\langle\obj{#2}\rangle{\kern-1.5pt}\rangle_{#1}^{\mmlAtms\to\mmlAtscct}\xspace}
\newcommand{\mmlAtmsmmlAtscctctxtocomp}[2][\Game]{\ensuremath\:^{\obj{\ctxtocomp}}{\kern-2.5pt}\langle{\kern-1.5pt}\langle\obj{#2}\rangle{\kern-1.5pt}\rangle_{#1}^{\mmlAtms\to\mmlAtscct}\xspace}
\newcommand{\mmlAtmsmmlAtscctsubtop}[2][\Game]{\ensuremath\:^{\obj{\comptoctx\ctxtocomp}}{\kern-2.5pt}\langle{\kern-1.5pt}\langle\obj{#2}\rangle{\kern-1.5pt}\rangle_{#1}^{\mmlAtms\to\mmlAtscct}\xspace}
\newcommand{\mmlAtmsmmlAtscctdetail}[2][\Game]{\ensuremath\langle{\kern-1.5pt}\langle\obj{#2}\rangle{\kern-1.5pt}\rangle_{#1}^{\mmlAtms\to\mmlAtscct}\xspace}
\newcommand{\mmlAtmsmmlAtscctv}[2][\Game]{\langle{\kern-1.5pt}\langle{\kern-1.5pt}\langle\obj{#2}\rangle{\kern-1.5pt}\rangle{\kern-1.5pt}\rangle{\kern-1.5pt}_{#1}^{\mmlAtms\to\mmlAtscct}\xspace}
% compiler robustly preserves
\newcommand{\rtp}[2]{\vdash{#1}:{#2}}
\newcommand{\rtpsigma}[3][\sim]{\vdash_{\sigma_{#1}}{#2}:{#3}}
\newcommand{\rtptau}[3][\sim]{\vdash_{\tau_{#1}}{#2}:{#3}}
\newcommand{\wf}[2]{\ensuremath\vdash{#1}:{#2}}
\newcommand{\wfc}[2]{\ensuremath\vdash_{\mathit{wf}}{#1}:{#2}}
\newcommand{\wfctau}[2]{\ensuremath\vdash_{\mathit{wf}}{#1}:{#2}}
\newcommand{\wfcsig}[2]{\ensuremath\vdash_{\mathit{wf}}{#1}:{#2}}
\newcommand{\lock}{\text{\scriptsize\faIcon{lock}}}
\newcommand{\unlock}{\text{\scriptsize\faIcon{lock-open}}}
% concrete language definitions
\newcommand{\mmlA}[1][]{\ensuremath\mathtt{L}_{\text{#1}}\xspace}
\newcommand{\mmlAs}{\src{\mmlA[tms]}}
\newcommand{\mmlAo}{\obj{\mmlA[scct]}}
\newcommand{\smsmmlAs}{\src{\mmlA[sms]}}
\newcommand{\mmlAt}{\trg{\mmlA[ms]}}
\newcommand{\mmlAtms}{\irl{\mmlA}}
\newcommand{\mmlAtscct}{\obj{\mmlA[scct]}}
\newcommand{\mmlAspec}{\ird{\mmlA[$\mathghost$]}}
\newcommand{\nospecASM}{\irl{ASM_{\not\mathghost}}}
\newcommand{\ctASM}{\irl{ASM_{sCCT}}}
\newcommand{\loc}{\ell}
\newcommand{\configs}{\src{\Omega}}
\newcommand{\qconfig}[1][\diamond]{\Omega^{#1}}
\newcommand{\qconfigs}[1][\diamond]{\src{\Omega^{#1}}}
\newcommand{\configt}{\trg{\Omega}}
\newcommand{\qconfigt}[1][\diamond]{\trg{\Omega^{#1}}}
\newcommand{\config}[2]{{#1};{#2}\xspace}
\newcommand{\sconfig}[2]{\config{\src{#1}}{\src{#2}}}
\newcommand{\tconfig}[2]{\config{\trg{#1}}{\trg{#2}}}
\newcommand{\subst}[3]{{#1}[{#2}\hookrightarrow{#3}]\xspace}
\newcommand{\grow}[2]{{#1}\ll{#2}\xspace}
\newcommand{\grows}[2]{\grow{\src{#1}}{\src{#2}}}
\newcommand{\noptr}[1]{\text{NoOwnedPtr}\ {#1}}
\newcommand{\ctxtocomp}{\xspace ? \xspace}
\newcommand{\comptoctx}{\xspace ! \xspace}
\newcommand{\nocomm}{\xspace \varnothing \xspace}
\newcommand{\comm}{\xspace \mathbf{c} \xspace}
\newcommand{\commlib}{\xspace\xi\xspace}
\newcommand{\callstack}{\xspace \overline{F^c}\xspace}
\newcommand{\memstate}{\xspace \Psi \xspace}
\newcommand{\cfstate}{\xspace \Phi \xspace}
\newcommand{\ctx}{{ctx}}
\newcommand{\comp}{{comp}}
\newcommand{\sandboxtag}{\xspace {t}\xspace}
\newcommand{\interfacevalue}{\xspace{i{\kern-1.5pt}v}\xspace}
\newcommand{\monitorcheck}[4][{\kern-3.5pt}^*]{%
\vdash\xspace{#2}\xspace \xrsquigarrow{#4}{#1}\xspace{#3}\xspace%
}
\newcommand{\traceagree}[3][]{\xspace{#2}\xspace \cong_{#1}\xspace{#3}\xspace}
\newcommand{\tmstraceagree}[3][]{\xspace{#2}\xspace \cong#1\xspace{#3}\xspace}
\newcommand{\smstraceagree}[3][]{\xspace{#2}\xspace \cong#1\xspace{#3}\xspace}
\newcommand{\mstraceagree}[3][]{\xspace{#2}\xspace \cong#1\xspace{#3}\xspace}
\newcommand{\sccttraceagree}[3][]{\xspace{#2}\xspace \cong#1\xspace{#3}\xspace}
\newcommand{\spectraceagree}[3][]{\xspace{#2}\xspace \cong#1\xspace{#3}\xspace}
\newcommand{\storeagree}[3][\delta]{\xspace{#2}\xspace \simeq_{#1}\xspace{#3}\xspace}
\newcommand{\storeagreetms}[3][\delta_{MS}]{\storeagree[#1]{#2}{#3}}
\newcommand{\storeagreesms}[3][\delta_{MS}]{\storeagree[#1]{#2}{#3}}
\newcommand{\storeagreescct}[3][\delta_{sCCT}]{\storeagree[#1]{#2}{#3}}
\newcommand{\tmsmonitor}[1][]{\xspace T_{\text{TMS}}{#1}\xspace}
\newcommand{\smsmonitor}[1][]{\xspace T_{\text{SMS}}{#1}\xspace}
\newcommand{\msmonitor}[1][]{\xspace T_{\text{MS}}{#1}\xspace}
\newcommand{\scctmonitor}[1][]{\xspace T_{\text{sCCT}}{#1}\xspace}
\newcommand{\specmonitor}[1][]{\xspace T_{\mathghost}{#1}\xspace}
\newcommand{\typecheck}[3]{{#1}\xspace \vdash\xspace {#2} :\ {#3}\xspace}
\newcommand{\typechecks}[3]{\typecheck{\src{#1}}{\src{#2}}{\src{#3}}}
\newcommand{\hasholes}[3]{\xspace\vdash\xspace\src{#2}\xspace\ni_1\src{hole:({#1})\to{#3}}\xspace}
\newcommand{\hasholet}[2]{\xspace\vdash\xspace\trg{#2}\xspace\ni_1\trg{hole:#1}\xspace}
\newcommand{\asymbol}{\xspace F\xspace}
\newcommand{\kontstack}{\xspace\overline{K}\xspace}
\newcommand{\library}{\xspace\Xi\xspace}
\newcommand{\plug}[3]{\xspace\operatorname{fill}_{#1} {#2}\xspace\operatorname{in}{#3}\xspace}
\newcommand{\plugs}[3][Q]{\plug{#1}{\src{#2}}{\src{#3}}}
\newcommand{\plugt}[3][Q]{\plug{#1}{\trg{#2}}{\trg{#3}}}
\newcommand{\closed}[2]{\xspace\left\{{#1}\right\}\vdash_\copyright{#2}\xspace}
\newcommand{\eval}[3]{{#1}\xspace\xrightarrow{#2}\xspace{#3}\xspace}
\newcommand{\evals}[3]{\src{\eval{#1}{#2}{#3}}}
\newcommand{\ctxeval}[3]{{#1}\xspace\xrightarrow{#2}_{ctx}\xspace{#3}\xspace}
\newcommand{\ctxevals}[3]{\src{\ctxeval{#1}{#2}{#3}}}
\newcommand{\expreval}[5]{{#1}\triangleright\xspace {#2}\xrightarrow{#5}\ {#3}\triangleright\xspace {#4}\xspace}
\newcommand{\exprevals}[5]{\expreval{\src{#1}}{\src{#2}}{\src{#3}}{\src{#4}}{\src{#5}}}
\newcommand{\exprevali}[5]{\expreval{\irl{#1}}{\irl{#2}}{\irl{#3}}{\irl{#4}}{\irl{#5}}}
\newcommand{\exprevalt}[5]{\expreval{\trg{#1}}{\trg{#2}}{\trg{#3}}{\trg{#4}}{\trg{#5}}}
\newcommand{\exprevalo}[5]{\expreval{\obj{#1}}{\obj{#2}}{\obj{#3}}{\obj{#4}}{\obj{#5}}}
\newcommand{\exprevald}[5]{\expreval{\ird{#1}}{\ird{#2}}{\ird{#3}}{\ird{#4}}{\ird{#5}}}
\newcommand{\exec}[6][{\kern-11.5pt}^*\ \ ]{{#2}\triangleright\xspace {#3}\xrightarrow{#6}{}{\kern-3.5pt}_{\text{ctx}}\xspace{#1}\;\xspace{#4}\triangleright\xspace {#5}\xspace}
\newcommand{\execN}[6][{\kern-11.5pt}^n\ \ ]{{#2}\triangleright\xspace {#3}\xrightarrow{#6}{}{\kern-3.5pt}_{\text{ctx}}\xspace{#1}\;\xspace{#4}\triangleright\xspace {#5}\xspace}
\newcommand{\execn}[6][{\kern-11.5pt}^*\ \ ]{{#2}\triangleright\xspace {#3}\not\xrightarrow{#6}{}{\kern-3.5pt}_{\text{ctx}}\xspace{#1}\;\xspace{#4}\triangleright\xspace {#5}\xspace}
\newcommand{\execs}[6][{\kern-11.5pt}^*\ \ ]{\exec[#1]{\src{#2}}{\src{#3}}{\src{#4}}{\src{#5}}{\src{#6}}}
\newcommand{\execsn}[6][^n]{\execN[{\kern-11.5pt}#1\ \ ]{\src{#2}}{\src{#3}}{\src{#4}}{\src{#5}}{\src{#6}}}
\newcommand{\exect}[6][{\kern-11.5pt}^*\ \ ]{\exec[#1]{\trg{#2}}{\trg{#3}}{\trg{#4}}{\trg{#5}}{\trg{#6}}}
\newcommand{\exectN}[6][{\kern-11.5pt}^n\ \ ]{\execN[#1]{\trg{#2}}{\trg{#3}}{\trg{#4}}{\trg{#5}}{\trg{#6}}}
\newcommand{\execo}[6][{\kern-11.5pt}^*\ \ ]{\exec[#1]{\obj{#2}}{\obj{#3}}{\obj{#4}}{\obj{#5}}{\obj{#6}}}
\newcommand{\execd}[6][{\kern-11.5pt}^*\ \ ]{\exec[#1]{\ird{#2}}{\ird{#3}}{\ird{#4}}{\ird{#5}}{\ird{#6}}}
\newcommand{\execoN}[6][{\kern-11.5pt}^n\ \ ]{\execN[#1]{\obj{#2}}{\obj{#3}}{\obj{#4}}{\obj{#5}}{\obj{#6}}}
\newcommand{\execdN}[6][{\kern-11.5pt}^n\ \ ]{\execN[#1]{\ird{#2}}{\ird{#3}}{\ird{#4}}{\ird{#5}}{\ird{#6}}}
\newcommand{\execiN}[6][{\kern-11.5pt}^n\ \ ]{\execN[#1]{\irl{#2}}{\irl{#3}}{\irl{#4}}{\irl{#5}}{\irl{#6}}}
\newcommand{\exectn}[6][{\kern-11.5pt}^*\ \ ]{\execn[#1]{\trg{#2}}{\trg{#3}}{\trg{#4}}{\trg{#5}}{\trg{#6}}}
\newcommand{\exectms}[6][{\kern-11.5pt}^*\ \ ]{\exec[#1]{\irl{#2}}{\irl{#3}}{\irl{#4}}{\irl{#5}}{\irl{#6}}}
\newcommand{\wexec}[4]{{#1}\xspace\xRightarrow{#4}\xspace{#2}\xspace\triangleright\xspace{#3}\xspace}
\newcommand{\wexecs}[4]{\wexec{\src{#1}}{\src{#2}}{\src{#3}}{\src{#4}}}
\newcommand{\wexect}[4]{\wexec{\trg{#1}}{\trg{#2}}{\trg{#3}}{\trg{#4}}}
\newcommand{\wexeco}[4]{\wexec{\obj{#1}}{\obj{#2}}{\obj{#3}}{\obj{#4}}}
\newcommand{\wexecd}[4]{\wexec{\ird{#1}}{\ird{#2}}{\ird{#3}}{\ird{#4}}}
\newcommand{\case}[1]{\item \textbf{Case} \ref{#1}\textbf{:}}
% the following environments require the enumitem package
\crefalias{ass}{enumi}
\crefalias{goal}{enumi}
\crefname{ass}{assumption}{assumptions}
\crefname{goal}{goal}{goals}
\newenvironment{assumptions}
{\begin{enumerate}[label=(\alph*)]
}
{
\end{enumerate}
}
\newenvironment{goals}
{\begin{enumerate}[label=(\roman*)]
}
{
\end{enumerate}
}
\newcommand{\IH}[1][]{I{\kern-1.5pt}H#1}
\newenvironment{passumptions}[1]
{%
\begin{enumerate}[label={$\left(#1_{\arabic*}\right)$}]%
}
{%
\end{enumerate}%
}
\newcommand{\thmref}[1]{\cref{#1}~(\nameref{#1})}
\newcommand{\Thmref}[1]{\Cref{#1}~(\nameref{#1})}
\newenvironment{thmstate}[1]{\noindent\textbf{Statement of \Cref{#1}}~(\nameref{#1})\textbf{.}}{\medskip}
\newcommand{\mockthm}[2]{\begin{thmstate}{#1}\getstored[#2]{buffer}\end{thmstate}}
\newcommand{\realthm}[3]{\begin{theorem}[#3]\label{#1}\getstored[#2]{buffer}\end{theorem}}