% generated by paper/tools/snippets.py from run_voblint_source_sound.thy (* src/Executable_Surface/CLI/Analysis_Certified.thy *)
\begin{flushleft}\fontsize{8}{10}\selectfont\ttfamily
\textbf{theorem}\ run\_voblint\_source\_sound:\\
\hspace*{1.0em}\textbf{fixes}\ p\ ::\ imp\_prog\ \textbf{and}\ s0\ s\ ::\ store\\
\hspace*{1.0em}\textbf{defines}\ G\_def:\ "\ensuremath{\mathcal{G}}\ \ensuremath{\equiv}\ declared\_global\ p"\\
\hspace*{3.0em}\textbf{and}\ Pi\_def:\ "\ensuremath{\Pi}\ \ensuremath{\equiv}\ prog\_table\ p"\\
\hspace*{3.0em}\textbf{and}\ g\_def:\ "g\ \ensuremath{\equiv}\ prog\_cfg\ p"\\
\hspace*{1.0em}\textbf{assumes}\ s0:\ "s0\ \ensuremath{\in}\ cinit\_stores\ \ensuremath{\mathcal{G}}"\\
\hspace*{3.0em}\textbf{and}\ run:\ "\ensuremath{\mathcal{G}},\ \ensuremath{\Pi}\ \ensuremath{\vdash}\ (main\_body\ \ensuremath{\Pi},\ s0,\ [])\ \ensuremath{\rightarrow}\textsubscript{p}\textsuperscript{*}\ (residual,\ s,\ frs)"\\
\hspace*{3.0em}\textbf{and}\ ans:\ "run\_voblint\ config\ p\ =\ Analysed\ res"\\
\hspace*{1.0em}\textbf{shows}\ "(\ensuremath{\exists}v.\ p,\ s0\ \ensuremath{\vdash}\ (residual,\ s,\ frs)\ \ensuremath{\rhd}\ v)\\
\hspace*{3.5em}\ensuremath{\wedge}\ (\ensuremath{\forall}v.\ p,\ s0\ \ensuremath{\vdash}\ (residual,\ s,\ frs)\ \ensuremath{\rhd}\ v\ \ensuremath{\longrightarrow}\\
\hspace*{8.0em}s\ \ensuremath{\in}\ \ensuremath{\mathcal{C}}\textsubscript{\ensuremath{\mathcal{G}},g,cinit\_stores\ \ensuremath{\mathcal{G}}}\ v\\
\hspace*{7.0em}\ensuremath{\wedge}\ s\ \ensuremath{\in}\ \ensuremath{\mathcal{R}}\textsubscript{res}\ v\\
\hspace*{7.0em}\ensuremath{\wedge}\ s\ \ensuremath{\in}\ \ensuremath{\mathcal{V}}\textsubscript{res}\ v)"
\end{flushleft}