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
|
%\newcommand{\xxx}[1]{{\color{BrickRed}{#1}}}
%\newcommand{\xxx}[1]{\marginpar{\footnotesize\color{red}{#1}}}
\newcommand{\xxx}{}
\newcommand{\comment}{}
\newcommand{\cminor}{Cminor}
\newcommand{\compcert}{CompCert}
\newcommand{\defeq}{=_{\mathrm{def}}}
% Abbreviations
% \newtheorem{thm}{Theorem}[section]
% \newtheorem{lemma}[thm]{Lemma}
% \newtheorem{corollary}[theorem]{Corollary}
% \newtheorem{dfn}[theorem]{Definition}
% \newtheorem{definition}[theorem]{Definition}
% Operators, relations, etc.
\def\seq#1{#1^*}
\def\opt#1{#1^?}
\def\some#1{\lfloor #1 \rfloor}
\def\Clight{{Clight{}}}
\def\tr{{\it tr}}
\def\vg{{\it lv}}
\def\ls{\it ls}
\def\ofs{{\it ofs}}
\def\op{{\it op}}
\def\chunk{\kappa} %{\it chunk}}
\def\sig{{\sigma}}
\def\fn{{\it def{\char95}fn}}
\def\cfn{{\it fn}}
\def\prog{{\it prog}}
\def\evv{{\it ev}}
\def\ev{{\it e}}
\def\tr{{\it tr}}
\def\E0{{\it \emptyset_\tr}}
\def\fl{{\it fl}}
\def\cenv{\gamma}
\def\tcast#1#2{{\cal C}_{#1}^{#2}}
\def\tcasta{{\cal C}_1}
\def\tcastb{{\cal C}_2}
\def\tlval{{\cal L}}
\def\trval{{\cal R}}
\def\tstmt{{\cal S}}
\def\tfunction{{\cal F}}
\def\valinj#1{\stackrel{#1}{\approx}}
\def\meminj#1{\stackrel{#1}{\approx}}
\def\outinj#1#2{\stackrel{#1,#2}{\approx}}
\def\loc{{\it loc}}
\def\envmatch{{\it EnvMatch}}
\def\csmatch{{\it CallInv}}
\def\sp{{\it sp}}
\def\cs{{\it cs}}
\def\evallvalue{\stackrel{l}{\Rightarrow}}
\def\evalexpr{\Rightarrow}
\def\evalstmt{\Rightarrow}
\def\evalfunc{\stackrel{f}{\Rightarrow}}
\def\evalprog{\Rightarrow}
%\def\evalexpr2{\rightarrow}
%\def\evalstmt2{\rightarrow}
%\def\evalfunc2{\rightarrow}
%\def\evalprog2{\rightarrow}
\def\inj{\alpha}
\def\accessmode{{\cal A}}
\newcommand{\sbcm}[1]{\textcolor{red}{\textit{#1}}}
\newcommand{\guardbox}{\raisebox{1pt}{\makebox[0pt][l]{\(\sqcap\)}}{\raisebox{-1pt}{\(\sqcup\)}}}
\newcommand{\danscarre}[2]{ \makebox[0pt][l]{\scriptsize \hspace{1pt}#1}{\guardbox{}^{#2}} }
\newcommand{\unannot}[2]{{\underline{#1}}^{#2}}
%\newcommand{\unannot}[2]{\mbox{\fbox{#1}\textsuperscript{#2}}}
%\newcommand{\unannot}[2]{\danscarre{#1}{#2}}
\newcommand{\tyface}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\option}{\tyface{option}}
\newcommand{\val}{\tyface{val}}
\newcommand{\Vundef}{\tyface{Vundef}}
\newcommand{\Vint}{\tyface{Vint}}
\newcommand{\Vfloat}{\tyface{Vfloat}}
\newcommand{\Vptr}{\tyface{Vptr}}
\newcommand{\expr}{\tyface{expr}}
\newcommand{\env}{\tyface{env}}
\newcommand{\mem}{\tyface{mem}}
\newcommand{\exprlist}{\tyface{exprlist}}
\newcommand{\Some}{\tyface{Some}}
\newcommand{\None}{\tyface{None}}
\newcommand{\Eval}{\tyface{Eval}}
\newcommand{\Evar}{\tyface{Evar}}
\newcommand{\Eop}{\tyface{Eop}}
\newcommand{\Eload}{\tyface{Eload}}
\newcommand{\Econdition}{\tyface{Econdition}}
\newcommand{\Elet}{\tyface{Elet}}
\newcommand{\Eletvar}{\tyface{Eletvar}}
\newcommand{\Enil}{\tyface{Enil}}
\newcommand{\Econs}{\tyface{Econs}}
\newcommand{\Sassign}[2]{#1:=#2}
\newcommand{\Sstore}[3]{\tyface{[}#2\tyface{]}_{#1}\tyface{:=}#3}
\newcommand{\Scall}[4]{\tyface{call}\,#1\,#3\,#4}
\newcommand{\Sif}[3]{\tyface{if}\,#1\,\tyface{then}\,#2\,\tyface{else}\,#3}
\newcommand{\Sloop}[1]{\tyface{loop}\,#1}
\newcommand{\Sblock}[1]{\tyface{block}\,#1}
\newcommand{\Sexit}[1]{\tyface{exit}\,#1}
\newcommand{\Sreturn}[1]{\tyface{return}\,#1}
\newcommand{\Sseq}[2]{#1;#2}
\newcommand{\Sskip}{\tyface{skip}}
\newcommand{\spt}{\ensuremath{\mathit{sp}}}
\newcommand{\stmt}{\tyface{stmt}}
\newcommand{\id}{\ensuremath{\mathit{id}}}
\newcommand{\out}{\ensuremath{\mathit{out}}}
\newcommand{\outcome}{\tyface{outcome}}
\newcommand{\outn}{\tyface{Out_{normal}}}
\newcommand{\oute}[1]{\tyface{Out_{exit}\,#1}}
\newcommand{\outr}[1]{\tyface{Out_{return}\,#1}}
\newcommand{\updrho}[2]{\tyface{update_{rho}}(#1,#2)}
\newcommand{\updmem}[2]{\tyface{update_{mem}}(#1,#2)}
\newcommand{\updsp}[2]{\tyface{update_{sp}}(#1,#2)}
\newcommand{\updphi}[2]{\tyface{update_{phi}}(#1,#2)}
\newcommand{\strho}[1]{\tyface{get_{rho}}(#1)}
\newcommand{\stmem}[1]{\tyface{get_{mem}}(#1)}
\newcommand{\stsp}[1]{\tyface{get_{sp}}(#1)}
%\newcommand{\evalexpr}[8]{#1;(#2;#3;#4;#5;#6) \vdash #7 \Downarrow #8}
%\newcommand{\evalexp}[3]{\fmap; #1 \vdash #2 \Downarrow #3}
\newcommand{\evaloperation}[5]{#1;#2 \vdash #3(#4) \Downarrow_\tyface{eval\_operation} #5}
\newcommand{\execstmts}[8]{#1;(#2;#3;#4) \Downarrow_#5 (#6;#7;#8)}
\newcommand{\execstmt}[4]{(#2,#1) \Downarrow_#3 #4}
\newcommand{\execstmtk}[5]{(#2,\Kseq{#1}{#3}) \Downarrow_{#4} #5}
\newcommand{\execpgm}[2]{\vdash #1 \Downarrow #2}
\newcommand{\loadv}[4]{#1\vdash #2\stackrel{#3}{\mapsto}#4}
\newcommand{\storev}[5]{#5=#2[#3\stackrel{#1}{:=}#4]}
\newcommand{\agree}{\approx}
\newcommand{\safe}[1]{\tyface{safe}\,#1}
\newcommand{\cat}[2]{#1 \circ #2}
\newcommand{\ceq}[3]{#2\stackrel{#1}{\mbox{\texttt{==}}}#3}
\newcommand{\ieq}[2]{\ceq{\mathrm{int}}{#1}{#2}}
\newcommand{\nomem}[1]{\lfloor{#1}\rfloor}
\newcommand{\withmem}[2]{\lceil{#1}\rceil^{#2}}
|
