<commit_before>\newcommand\resultOk[2]{
  $R#2 = \Ok{\Store#2, \Perm#2, r#2}$
}
\newcommand\resultEnv[2]{
  $\SE#1 \le \SE#2$, $\Store#1 \le \Store#2$, $\vdash \Store#2 : \SE#2$
}
\newcommand\resultPermDom[2]{
  $\Perm#2$ is wellformed and
  $\Rawloc{\Perm#2} \subseteq \Dom{\Store#2} \setminus {\Store#2}^{-1}
  (\StFreed)$
}
\newcommand\resultReachPerm[2]{
  $\Reach{\Store#2}{r#2} \subseteq \Perm#2$
}
\newcommand\resultFrame[3]{
  % input, inputenv, output
  Frame: \\
  For all $\Loc \in \Dom{\Store#1} \setminus
  \Rawloc{\Reach{\Store#3}{\VEnv#2}}$ it must be that
  \begin{itemize}
  \item $\Store#3 (\Loc) = \Store#1 (\Loc)$ and
  \item  for any $\Addr$ with $\Rawloc\Addr = \{\Loc\}$,
    $\Addr \in \Perm#1 \Leftrightarrow \Addr\in\Perm#3$.
  \end{itemize}
}
\newcommand\resultImmutables[3]{
  % input, inputenv, output
  Unrestricted values, resources, and borrows: \\
  For all $\Addr \in
  \Reach{\Store#3}{\ImmutableBorrows{\VEnv#2}}$ with
  $\Rawloc\Addr = \{\Loc\}$, it must be that
  $\Loc\in\Dom{\Store#1}$,
  $\Store#3 (\Loc) = \Store#1 (\Loc) \ne \StFreed$
  and $\Addr\in\Perm#3$.
}
\newcommand\resultMutables[3]{
  % input, inputenv, output
  Affine borrows and resources:\\
  For all $\Addr \in  \Reach{\Store#3}{\MutableBorrows{\VEnv#2}}$
  with $\Rawloc\Addr = \{\Loc\}$, if
  $\Loc\in\Dom{\Store#1}$ and $\Addr\ne\Loc$, then
  $\Store#3 (\Loc) \ne \StFreed$.
}
\newcommand\resultSuspended[3]{
  % input, inputenv, output
  Suspended borrows: \\
  For all $\Addr \in \Reach{\Store#3}{\Suspended{\VEnv#2}}$ with
  $\Rawloc\Addr = \{\Loc\}$ it must be that $\Addr \in \Perm#3$
  and  $\Store#3 (\Loc) \ne \StFreed$.
  % \begin{itemize}
  % \item If $\Addr = \IBORROW\Addr'$, then $\Loc\in\Dom{\Store#1}$ and
  %   $\Store#3 (\Loc) = \Store#1 (\Loc) \ne \StFreed$.
  % \item If $\Addr = \MBORROW\Addr'$ and
  %   $\Loc\in\Dom{\Store#1}$, then
  %   $\Store#3 (\Loc) \ne \StFreed$.
  % \end{itemize}
}
\newcommand\resultResources[3]{
  % input, inputenv, output
  Resources: Let $\REACH#1 = \Reach{\Store#1}{\Active{\VEnv#2}}$.  Let
  $\REACH#3 =\Reach{\Store#3}{\Active{\VEnv#2}}$.
  \\
  For all $\Loc\in \REACH#1$ it must be that
  $\MultiNumber\Loc{\REACH#1}=\MultiNumber\Loc{\REACH#3}=1$,
  $\Loc\notin\Perm#3$, and if $\Store#1(\Loc)$ is a resource, then
  $\Store#3 (\Loc) = \StFreed$.
  % \begin{itemize}
  % \item if $\Linear{\SE#1}\Loc$
  %   then $n=n'=1$, $\Loc\notin\Perm#2$, and if $\Store#1(\Loc)$ is a
  %   resource, then $\Store#2 (\Loc) = \StFreed$;
  % \item if $\Affine{\SE#1}\Loc$ then $n=1$ and $n'\le 1$;
  % \item if $\Unrestricted{\SE#1}\Loc$ then
  %   $\Store#2 (\ell) = \Store#1 (\ell)$ and $\Loc\in \Perm#2$.
  % \end{itemize}
}
\newcommand\resultThinAir[2]{
  No thin air permission: \\
  $\Perm#2 \subseteq
  \Perm#1 \cup ( \Dom{\Store#2} \setminus \Dom{\Store#1})$.
  % For all $\Addr\in {\Perm#2}$, $\Addr
  % \in \Perm#1 \cup ( \Dom{\Store#2} \setminus \Dom{\Store#1})$.
}
\newcommand\assumeWellformed[1]{
  $\Perm#1$ is wellformed and $\Rawloc{\Perm#1} \subseteq
  \Dom{\Store#1} \setminus {\Store#1}^{-1} (\StFreed)$
}
\newcommand\assumeIncoming[2]{
  Incoming Resources:
  \begin{enumerate}
  \item $\forall \Loc\in \Rawloc{\Reach{\Store#1}{\VEnv#2}}$,
    $\Store#1 (\Loc) \ne \StFreed$.
    % suspended bindings must not point to freed resources
  \item $\forall \Loc \in \REACH
    =\Rawloc{\Reach{\Store#1}{\Active{\VEnv#2},\MutableBorrows{\VEnv#2},
      \Suspended{\VEnv#2}}}$,
    % if $\Affine\SE\Loc$ then
    $\MultiNumber\Loc\REACH= 1$.
  \end{enumerate}
}

\newcommand\SoundnessThmBody{
  Suppose that
  \begin{enumerate}[({A}1)]
  \item $\inferS{C}{\E}{e}{\tau}$
  \item $\SE \vdash \VEnv : \E$
  \item $\vdash \Store : \SE$
  \item\label{item:11} \assumeWellformed{}
  \item\label{item:12} $\Reach\Store{\Active\VEnv, \MutableBorrows\VEnv,
      \ImmutableBorrows\VEnv} \subseteq \Perm$
  \item $\Rawloc{\Active\VEnv}$,
    $\Rawloc{\MutableBorrows\VEnv}$,
    $\Rawloc{\ImmutableBorrows\VEnv}$, and
    $\Rawloc{\Suspended\VEnv}$ are all disjoint
  % \item  $\VEnv'$ with $\Rawloc{\VEnv'}
  %   \subseteq \Dom\Store$ and $\Dom\VEnv \cap \Dom{\VEnv'}=\emptyset$
  \item\label{item:15} \assumeIncoming{}{}
  \end{enumerate}
  For all $i\in\Nat$, if
  @R' = eval $\Store$ $\Perm$ $\VEnv$ i e@
  %$\Store, \Perm, \VEnv \vdash {e}  \Downarrow^i R'$
  and $R'\ne \TimeOut$,
  then
  $\exists$ $\Store'$, $\Perm'$, $r'$, $\SE'$ such that
  \begin{enumerate}[({R}1)]
  \item \resultOk{}{'}
  \item \resultEnv{}{'}
  \item $\SE' \vdash r' : \tau$
  \item \resultPermDom{}{'}
  \item \resultReachPerm{}{'}
  \item \resultFrame{}{}{'}
    %% must be \Store because \Perm has no idea of \Perm'
  \item \resultImmutables{}{}{'}
  \item \resultMutables{}{}{'}
    % \\\textbf{PJT: this is a really weak statement! anything else that<commit_msg>Metatheory: Fixed lstlisting bug...<commit_after>\newcommand\resultOk[2]{
  $R#2 = \Ok{\Store#2, \Perm#2, r#2}$
}
\newcommand\resultEnv[2]{
  $\SE#1 \le \SE#2$, $\Store#1 \le \Store#2$, $\vdash \Store#2 : \SE#2$
}
\newcommand\resultPermDom[2]{
  $\Perm#2$ is wellformed and
  $\Rawloc{\Perm#2} \subseteq \Dom{\Store#2} \setminus {\Store#2}^{-1}
  (\StFreed)$
}
\newcommand\resultReachPerm[2]{
  $\Reach{\Store#2}{r#2} \subseteq \Perm#2$
}
\newcommand\resultFrame[3]{
  % input, inputenv, output
  Frame: \\
  For all $\Loc \in \Dom{\Store#1} \setminus
  \Rawloc{\Reach{\Store#3}{\VEnv#2}}$ it must be that
  \begin{itemize}
  \item $\Store#3 (\Loc) = \Store#1 (\Loc)$ and
  \item  for any $\Addr$ with $\Rawloc\Addr = \{\Loc\}$,
    $\Addr \in \Perm#1 \Leftrightarrow \Addr\in\Perm#3$.
  \end{itemize}
}
\newcommand\resultImmutables[3]{
  % input, inputenv, output
  Unrestricted values, resources, and borrows: \\
  For all $\Addr \in
  \Reach{\Store#3}{\ImmutableBorrows{\VEnv#2}}$ with
  $\Rawloc\Addr = \{\Loc\}$, it must be that
  $\Loc\in\Dom{\Store#1}$,
  $\Store#3 (\Loc) = \Store#1 (\Loc) \ne \StFreed$
  and $\Addr\in\Perm#3$.
}
\newcommand\resultMutables[3]{
  % input, inputenv, output
  Affine borrows and resources:\\
  For all $\Addr \in  \Reach{\Store#3}{\MutableBorrows{\VEnv#2}}$
  with $\Rawloc\Addr = \{\Loc\}$, if
  $\Loc\in\Dom{\Store#1}$ and $\Addr\ne\Loc$, then
  $\Store#3 (\Loc) \ne \StFreed$.
}
\newcommand\resultSuspended[3]{
  % input, inputenv, output
  Suspended borrows: \\
  For all $\Addr \in \Reach{\Store#3}{\Suspended{\VEnv#2}}$ with
  $\Rawloc\Addr = \{\Loc\}$ it must be that $\Addr \in \Perm#3$
  and  $\Store#3 (\Loc) \ne \StFreed$.
  % \begin{itemize}
  % \item If $\Addr = \IBORROW\Addr'$, then $\Loc\in\Dom{\Store#1}$ and
  %   $\Store#3 (\Loc) = \Store#1 (\Loc) \ne \StFreed$.
  % \item If $\Addr = \MBORROW\Addr'$ and
  %   $\Loc\in\Dom{\Store#1}$, then
  %   $\Store#3 (\Loc) \ne \StFreed$.
  % \end{itemize}
}
\newcommand\resultResources[3]{
  % input, inputenv, output
  Resources: Let $\REACH#1 = \Reach{\Store#1}{\Active{\VEnv#2}}$.  Let
  $\REACH#3 =\Reach{\Store#3}{\Active{\VEnv#2}}$.
  \\
  For all $\Loc\in \REACH#1$ it must be that
  $\MultiNumber\Loc{\REACH#1}=\MultiNumber\Loc{\REACH#3}=1$,
  $\Loc\notin\Perm#3$, and if $\Store#1(\Loc)$ is a resource, then
  $\Store#3 (\Loc) = \StFreed$.
  % \begin{itemize}
  % \item if $\Linear{\SE#1}\Loc$
  %   then $n=n'=1$, $\Loc\notin\Perm#2$, and if $\Store#1(\Loc)$ is a
  %   resource, then $\Store#2 (\Loc) = \StFreed$;
  % \item if $\Affine{\SE#1}\Loc$ then $n=1$ and $n'\le 1$;
  % \item if $\Unrestricted{\SE#1}\Loc$ then
  %   $\Store#2 (\ell) = \Store#1 (\ell)$ and $\Loc\in \Perm#2$.
  % \end{itemize}
}
\newcommand\resultThinAir[2]{
  No thin air permission: \\
  $\Perm#2 \subseteq
  \Perm#1 \cup ( \Dom{\Store#2} \setminus \Dom{\Store#1})$.
  % For all $\Addr\in {\Perm#2}$, $\Addr
  % \in \Perm#1 \cup ( \Dom{\Store#2} \setminus \Dom{\Store#1})$.
}
\newcommand\assumeWellformed[1]{
  $\Perm#1$ is wellformed and $\Rawloc{\Perm#1} \subseteq
  \Dom{\Store#1} \setminus {\Store#1}^{-1} (\StFreed)$
}
\newcommand\assumeIncoming[2]{
  Incoming Resources:
  \begin{enumerate}
  \item $\forall \Loc\in \Rawloc{\Reach{\Store#1}{\VEnv#2}}$,
    $\Store#1 (\Loc) \ne \StFreed$.
    % suspended bindings must not point to freed resources
  \item $\forall \Loc \in \REACH
    =\Rawloc{\Reach{\Store#1}{\Active{\VEnv#2},\MutableBorrows{\VEnv#2},
      \Suspended{\VEnv#2}}}$,
    % if $\Affine\SE\Loc$ then
    $\MultiNumber\Loc\REACH= 1$.
  \end{enumerate}
}

\newcommand\SoundnessThmBody{
  Suppose that
  \begin{enumerate}[({A}1)]
  \item $\inferS{C}{\E}{e}{\tau}$
  \item $\SE \vdash \VEnv : \E$
  \item $\vdash \Store : \SE$
  \item\label{item:11} \assumeWellformed{}
  \item\label{item:12} $\Reach\Store{\Active\VEnv, \MutableBorrows\VEnv,
      \ImmutableBorrows\VEnv} \subseteq \Perm$
  \item $\Rawloc{\Active\VEnv}$,
    $\Rawloc{\MutableBorrows\VEnv}$,
    $\Rawloc{\ImmutableBorrows\VEnv}$, and
    $\Rawloc{\Suspended\VEnv}$ are all disjoint
  % \item  $\VEnv'$ with $\Rawloc{\VEnv'}
  %   \subseteq \Dom\Store$ and $\Dom\VEnv \cap \Dom{\VEnv'}=\emptyset$
  \item\label{item:15} \assumeIncoming{}{}
  \end{enumerate}
  For all $i\in\Nat$, if
  % Sorry for the ugly fix... I can't get lstinline to behave like
  % \lstMakeShortInline, but copy pasting would also be bad.
  \ \lstinline[style=rule]{R' = eval} $\Store$ $\Perm$ $\VEnv$ \lstinline[style=rule]{i e}
  %$\Store, \Perm, \VEnv \vdash {e}  \Downarrow^i R'$
  and $R'\ne \TimeOut$,
  then
  $\exists$ $\Store'$, $\Perm'$, $r'$, $\SE'$ such that
  \begin{enumerate}[({R}1)]
  \item \resultOk{}{'}
  \item \resultEnv{}{'}
  \item $\SE' \vdash r' : \tau$
  \item \resultPermDom{}{'}
  \item \resultReachPerm{}{'}
  \item \resultFrame{}{}{'}
    %% must be \Store because \Perm has no idea of \Perm'
  \item \resultImmutables{}{}{'}
  \item \resultMutables{}{}{'}
    % \\\textbf{PJT: this is a really weak statement! anything else that
{'fraction_non_alphanumeric': 0.23266721044045677, 'fraction_numerical': 0.022430668841761828, 'mean_word_length': 3.097326649958229, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5189143', 'n_tokens_mistral': 3964, 'n_tokens_neox': 3898, 'n_words': 866}