text:
\section{Clight-A: Annotation Language} \label{sec:annot}
\begin{comment}
    Annotated program is a proof, not a program.
\end{comment}
In this section we describe an annotation language Clight-A.
\figref{fig:syntax} shows its syntax.
We use capitalized ``$C$'' to represent annotated programs in this paper
    while we use lower case ``$c$'' to represent
    programs written in the original Clight language.
``$\mathrm{Assert} \ \  P$'' is a statement that suggests the assertion $P$ holds at this point.
\begin{figure}
$$\begin{array}{rrl}
\text{assertion}:& P := & \cdots\\
\text{single statement}:& C' := &
    \mathsf{skip}\\
&\mid&  \mathrm{Assert} \ \  P\\
&\mid&  \cifthenelse{e}{C_1}{C_2}\\
&\mid&  \aloop{P_1}{P_2}{C_1}{C_2}\\
&\mid&  \text{assignment statement}\\
&\mid&  \mathsf{break} \mid \mathsf{continue} \mid \mathsf{return}\ e?\\
\text{statement}:&C := &
    \Given{x}{A}{C}\\
&\mid&  C'; C\\
&\mid&  C'
\end{array}$$
    \caption{Syntax of Clight-A}
    \label{fig:syntax}
\end{figure}
Loop statement is extended from loop in Clight.
There are two loop invariants given before loop,
    and the first is loop invariant and the second is continue invariant.
Continue invariant is the assertion required before incremental statement in loop.
Assignment statements are the same as defined in \S 2.
``Given'' clauses are a special kind of statements that allows user to introduce new logical variables.
In this paper, types may be omitted after ``$\exists$'' and/or ``given'' when it is not ambiguous.
Assertions in the scope of a ``given'' clause may use these logical variables,
    as shown by the following typing rules.
\begin{mathpar}
    \inferrule*[left=Given-wt]{
        \Gamma; x : A \Vdash C \text{  well-typed}
    } {
        \Gamma \Vdash \Given{x}{A}{C} \text{  well-typed}
    }
    \and
    \inferrule*[left=Seq-wt]{
        \Gamma \Vdash C_1 \text{  well-typed} \and
        \Gamma \Vdash C_2 \text{  well-typed}
    } {
        \Gamma \Vdash (C_1; C_2) \text{  well-typed}
    }
    \and
    {\text{(Other typing rules omitted.)}}
\end{mathpar}
For convenience, Clight-A only allows sequential combination to be associated from right to left,
    such that a ``given'' clause, which appears on the left, always affects all statements on the right (if they are in the same block).
Although we use $C$ to represent Clight-A's statements in \figref{fig:syntax} while $C'$ is used for single statements,
    we will not distinguish them in the rest part of this paper.

\begin{figure}
\begin{mathpar}
    \inferrule*[left=Skip]{
        \Sigma; \Gamma; P\vDash Q
    } {
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{\mathsf{skip}}{Q}{Q'}}{\mathsf{skip}}
    }
    \and
    \inferrule*[left=Seq]{
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{c_1}{Q}{R'}}{C_1} \and
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{Q}{c_2}{R}{R'}}{C_2}
    } {
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{c_1;c_2}{R}{R'}}{C_1;C_2}
    }
    \and
    \inferrule*[left=SeqPost]{
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{c_1}{Q}{R'}}{C_1} \and
        \hintprovable{\Sigma; \Gamma}{Q \implies R}{C_2}
    } {
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{c_1}{R}{R'}}{C_1;C_2}
    }
    \and
    \inferrule*[left=Assoc]{
         \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{c_1;(c_2;c_3)}{Q}{Q'}}{C}
    } {
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{(c_1;c_2);c_3}{Q}{Q'}}{C}
    }
    \and
    \inferrule*[left=Assignment]{
        \findvalue{\Sigma; \Gamma}{\mathsf{ae}(P, c)}{Q} \and
        \Sigma; \Gamma; Q \vDash R
    } {
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{c}{R}{R'}}{c}
    }
    \and

    \inferrule*[left=Break]{
        \Sigma; \Gamma; P \vDash \brkcnd{Q}
    } {
        \hintprovable{\Sigma; \Gamma}{\hoare{P}{\mathsf{break}}{Q}{\brkcnd{Q}}{\concnd{Q}}{\retcnd{Q}}}{\mathsf{break}}
    }
    \and
    \inferrule*[left=Continue]{
        \Sigma; \Gamma; P \vDash \retcnd{Q}
    } {
        \hintprovable{\Sigma; \Gamma}
        {\hoare{P}{\mathsf{continue}}{Q}{\brkcnd{Q}}{\concnd{Q}}{\retcnd{Q}}}{\mathsf{continue}}
    }
    \and
    \inferrule*[left=Return]{
        \Sigma; \Gamma; P \vDash \retcnd{Q}
    } {
        \hintprovable{\Sigma; \Gamma}
        {\hoare{P}{\mathsf{return}}{Q}{\brkcnd{Q}}{\concnd{Q}}{\retcnd{Q}}}{\mathsf{return}}
    }
    \and
    \inferrule*[left=If]{
        \findvalue{\Sigma; \Gamma}{\mathsf{norm}(P\land \denote{b}=\mathsf{true})}{P_\mathsf{true}} \and
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P_\mathsf{true}}{c_1}{Q}{Q'}}{C_1} \\
        \findvalue{\Sigma; \Gamma}{\mathsf{norm}(P\land \denote{b}=\mathsf{false})}{P_\mathsf{false}} \and
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P_\mathsf{false}}{c_2}{Q}{Q'}}{C_2}
    } {
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{\cifthenelse{b}{c_1}{c_2}}{Q}{Q'}}
        {\cifthenelse{b}{C_1}{C_2}}
    }
    \and
    \inferrule*[left=Loop]{
        \Sigma; \Gamma; P \vDash I \ \ \
        \hintprovable{\Sigma; \Gamma}{\hoare{I}{c}{\coninv{I}}{Q}{\coninv{I}}{\retcnd{Q}}}{C} \ \ \
        \hintprovable{\Sigma; \Gamma}{\hoare{\coninv{I}}{\cincr{c}}{I}{Q}{\bot}{\retcnd{Q}}}{\cincr{C}}
    } {
        \hintprovable{\Sigma; \Gamma}
            {\hoare{P}{\cloop{c}{\cincr{c}}}{Q}{\brkcnd{Q}}{\concnd{Q}}{\retcnd{Q}}}
            {\aloop{I}{\coninv{I}}{C}{\cincr{C}}}
    }
\end{mathpar}
    \caption{Proof rules for annotated program (Part I): program rules}
    \label{fig:annotrules1}
\end{figure}

\begin{figure}
\begin{mathpar}
    \inferrule*[left=Assertion]{
        \Sigma; \Gamma; P \vDash Q \and
        \Sigma; \Gamma; Q \vDash R
    } {
        \hintprovable{\Sigma; \Gamma}{P\implies R}{\mathrm{Assert} \ \  Q}
    }
    \and
    \inferrule*[left=SeqAssertion]{
        \Sigma; \Gamma; P \vDash Q \and
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{Q}{c}{R}{R'}}{C}
    } {
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{c}{R}{R'}}{\mathrm{Assert} \ \  Q; C}
    }
    \and
    \inferrule*[left=ImpAssertion]{
        \Sigma; \Gamma; P \vDash Q \and
        \hintprovable{\Sigma; \Gamma}{Q\implies R}{C}
    } {
        \hintprovable{\Sigma; \Gamma}{P\implies R}{\mathrm{Assert} \ \  Q; C}
    }
    \and
    \inferrule*[left=Given]{
        \hintprovable{\Sigma; x:A; \Gamma}{\hoareabbr{P(x)}{c}{Q}{Q'}}{C(x)}
    } {
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{\EX{x}{A}{P(x)}}{c}{Q}{Q'}}{\Given{x}{A}{C(x)}}
    }
    \and
    \inferrule*[left=ImpGiven]{
        \hintprovable{\Sigma; x:A; \Gamma}{P(x)\implies Q}{C(x)}
    } {
        \hintprovable{\Sigma; \Gamma}{(\EX{x}{A}{P(x)})\implies Q}{\Given{x}{A}{C(x)}}
    }
    \and
    \inferrule*[left=Pure]{
        \mathsf{pure}(P_\mathsf{pure})\and
        \hintprovable{\Sigma; \Gamma; P_\mathsf{pure}}{\hoareabbr{P}{c}{Q}{Q'}}{C}
    } {
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P_\mathsf{pure}\land P}{c}{Q}{Q'}}{C}
    }
    \and
    \inferrule*[left=ImpPure]{
        \hintprovable{\Sigma; \Gamma; \mathsf{pure}{P}}{P\implies Q}{C}
    } {
        \hintprovable{\Sigma; \Gamma}{\mathsf{pure}{P}\land P\implies Q}{C}
    }
\end{mathpar}
    \caption{Proof rules for annotated program (Part II): annotation rules}
    \label{fig:annotrules2}
\end{figure}

Every annotated program is actually a proof plan for building a Hoare triple.
If we review VST's Hoare logic proof rule (see \figref{fig:choarelogic}),
    we can divide them into two classes.
Some proof rules, like \rulename{If} and \rulename{Seq}, decompose a Hoare triple
    into multiple smaller ones.
Other proof rules, like \rulename{Pre} and \rulename{Exists}, manipulate preconditions
    (and proof contexts if necessary).
Thus, for proving a Hoare triple, the main proof structure is fixed---the proof target
    should be decomposed step by step according the program's syntax tree.
Users are only free to choose where and how to rewrite preconditions.
Our annotated programs describes this ``where'' and ``how''.

Formally, we use
$\hintprovable{\Sigma; \Gamma}{\Phi}{C}$
    to denote that
    judgement $\Phi$ can be proved if following
    the proof plan described by annotated program $C$,
    under variable context $\Sigma$ and proposition context $\Gamma$.
Here, this judgement $\Phi$ can be either a Hoare triple or an assertion entailment.
\figref{fig:annotrules1} describes proof strategies that follows C programs' syntax tree.
\rulename{Seq} rule implicitly requires $c_1; c_2$ to be
    the same separation as $C_1; C_2$,
    otherwise the premises cannot be proved.
\rulename{Assoc} rule is to reassociate program statements
    into the same structure as annotated program.
\figref{fig:annotrules2} shows precondition transformation rules that are guided
     by annotations.
\rulename{Given} rule shows that,
    when the annotated program has a given clause,
    an existentially quantified variable should be extracted from precondition to variable context.
\rulename{SeqAssertion} is application of pre-consequence rule in Hoare logic
    and it is driven by assertions in annotated programs.
In \rulename{Pure} rule,
    $\mathsf{pure}(P)$ means: $P$ is a pure proposition about logical variables; it does not depend on
    program state.
This rule is to extract pure propositions to proposition context automatically, without an explicit annotation.

All these proof construction strategies are based on VST's Hoare logic, which can be formally stated as the following theorem.

\begin{theorem}\label{thm:vst-a-sound}
    For every $\Sigma$, $\Gamma$, $c$, $P$, $Q$, $\vec{Q'}$ and $C$,
    if
    $$\hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{c}{Q}{Q'}}{C},$$
    then there is a proof for
    $$\Sigma; \Gamma\vdash \hoareabbr{P}{c}{Q}{Q'}.$$
\end{theorem}

\section{Background} \label{sec:backgrnd}
VST is a tool for interactive C program verification.
In this section, we show four parts of background information.
The first is an abstract C language which we will use in this paper. It is a subset of CompCert Clight \cite{Leroy-Compcert-CACM}, but including most commonly used features.
The second is VST's forward symbolic execution for assignment statements.
The third is VST's Hoare logic for C language.
The forth is the Coq proof assistant.
The VST verification tool is built in Coq.
We use Coq and VST to implement our annotation verifier, VST-A.

\subsection{Clight: Abstract C language}
\label{sec:clight}
In this paper,
    we use a simplified version of CompCert Clight as an abstract C language.
\figref{fig:ClightAST} shows the syntax.
$\cloop{c}{\cincr{c}}$ is a general way to describe loops in the C language,
    which is equivalent to $\mathsf{for}\ (;;\cincr{c})\ \{c\}$.
Three kinds of loops in C language, namely for, while and do-while loops,
    can be expressed using this general loop statement.
In return statements, return expressions are optional; thus we write $e?$ instead of $e$.
Goto statement is not allowed --- it is not supported by VST's program logic,
    and can be avoided by program transformation.
Our development can handle switch statements
but we exclude them in this paper because of their complex syntax.
\begin{figure}[htp]
$$\begin{array}{rrl}
    \text{expression}:&e := & \cdots\\
    \text{statement}:&c := &
    \mathsf{skip}\\
&\mid&  c_1; c_2\\
&\mid&  \text{assignment statement}\\
&\mid&  \mathsf{break} \mid \mathsf{continue} \mid \mathsf{return}\ e?\\
&\mid&  \cifthenelse{e}{c_1}{c_2}\\
&\mid&  \cloop{c_1}{c_2}
\end{array}$$
    \caption{Clight: abstract C language}
    \label{fig:ClightAST}
\end{figure}

\subsection{Forward Symbolic Executor}
\label{sec:se}
Our work is based on a forward symbolic executor with two components:
    a symbolic assignment executor $\mathsf{ae}(\cdot, \cdot)$
    and an assertion normalization program $\mathsf{norm}(\cdot)$.
We write $\findvalue{\Sigma; \Gamma}{\mathsf{ae}(P, c)}{Q}$ if $Q$ is the result
    of symbolic execution,
i.e., given logical variable context $\Sigma$ and proposition context $\Gamma$,
    $\mathsf{ae}(\cdot, \cdot)$ computes a strongest postcondition $Q$ for precondition $P$ and
    assignment statement $c$.
For example,
    in the reverse program given in \figref{fig:ll-reverse},
    if
    \begin{align*}
        \Sigma &:= a; b; l_1; l_2,\\
        \Gamma &:= \emptyset,\\
        P &:= \exists \ c \ x \ l_2'. \ l_2 = x \ l_2' \ \wedge \
            \denote{\cvar{w}}=a\ \wedge\ \denote{\cvar{v}}=b\ \wedge\
            b \mapsto (x, c) \ * \
            \ll\left(a, l_1\right) \ * \
            \ll\left(c, l_2'\right),\\
        c &:= \lstinline|t = v->tail|,
    \end{align*}
    then $\findvalue{\Sigma; \Gamma}{\mathsf{ae}(P, c)}{Q}$ for
    \begin{align*}
        Q &:= \exists \ c \ x \ l_2'. \ l_2 = x \ l_2' \ \wedge \
            \denote{\cvar{w}}=a\ \wedge\ \denote{\cvar{v}}=b\ \wedge\
            \denote{\cvar{t}}=c\ \wedge\
            b \mapsto (x, c) \ * \
            \ll\left(a, l_1\right) \ * \
            \ll\left(c, l_2'\right).
    \end{align*}
Assignment executor may fail,
    if the precondition $P$ cannot guarantee $c$ can run successfully,
    or $P$ is not in a good form such that the symbolic executor can execute $c$.

Besides, an assertion normalization program turns an assertion into a \emph{better} form.
We write $\findvalue{\Sigma; \Gamma}{\mathsf{norm}(P)}{Q}$ if the $\mathsf{norm}(\cdot)$ program terminates
    and returns $Q$ when it tries to improve $P$.
Here, $P$ and $Q$ should be equivalent with each other but $Q$ is in a better form.
For example, the following assertion $I$ is the loop invariant in
    our reverse program (\figref{fig:ll-reverse}):
$$I:=\exists \ a \ b \ l_1 \ l_2. \ \denote{\cvar{w}} = a \ \wedge \
    \denote{\cvar{v}} = b \ \wedge \
    l = \mathrm{rev}(l_1) \ l_2 \ \wedge \
    \ll\left(a, l_1\right) \ * \
    \ll\left(b, l_2\right)$$
So at the beginning of the loop body, the assertion
    $(I\ \wedge\ \denote{\cvar{v}}=\mathsf{true})$ must hold.
But this form may be not preferred by the symbolic executor and it becomes hard for next step.
Assertion normalization program handles this situation.
Here, $\findvalue{\Sigma; \Gamma}{\mathsf{norm}(I\land \denote{b}=\mathsf{true})}{Q}$
for
$$Q:=\exists \ a \ b \ l_1 \ l_2. \ \denote{\cvar{w}} = a \ \wedge \
    \denote{\cvar{v}} = b \ \wedge \
    b\neq \mathsf{NULL}\ \wedge\
    l = \mathrm{rev}(l_1) \ l_2 \ \wedge \
    \ll\left(a, l_1\right) \ * \
    \ll\left(b, l_2\right).$$

VST provides an instance of forward symbolic executor inside.

\subsection{Hoare Logic for C Programs}
\label{sec:hoarelogic}
\figref{fig:choarelogic} shows proof rules of VST's Hoare logic.
Besides, \rulename{Exists} and \rulename{Pure} rules
    introduce variables and propositions from precondition to context, respectively.
\rulename{Loop}
    rule has two invariants, loop invariant $I$ and continue invariant $\coninv{I}$,
    that $I$ is the invariant must hold before each iteration,
    and $\coninv{I}$ is the invariant must hold at $\mathsf{continue}$
    or before $\cincr{c}$ statement.
For return statements, we only demonstrate a proof rule for statements without a return value.
In our development, there is a similar proof rule with return value; we omit it here for simplicity.
\rulename{Assoc} rule reassociates sequential compositions\footnote{Although both directions of reassociation are sound, we only need one in this paper.}.

Different from ordinary versions, we demonstrate pre/postcondition replacement in an asymmetric way.
Specifically, \rulename{Pre} is our precondition strengthening rule.
But we do not have one corresponding rule for postcondition weakening.
Instead, it is built-in \rulename{Skip}, \rulename{Assignment},
    \rulename{Break}, \rulename{Continue} and \rulename{Return}.
We choose this special presentation because VST always suggests users
    verify programs in a forward direction.
For example, suppose $c$ is an assignment statement, using \rulename{Assignment},
   a triple with form $\Sigma; \Gamma\vdash\hoareabbr{P}{c}{R}{R'}$
    can be reduced to an assertion entailment
    $\Sigma; \Gamma; Q \vDash R$ where $Q$ is the strongest postcondition
    generated by VST's assignment executor $\mathsf{ae}(P, c)$.
As another example, $\Sigma; \Gamma\vdash\hoareabbr{P}{(c; c_1); c_2}{R}{R'}$
    can be reduced
    $\Sigma; \Gamma\vdash\hoareabbr{Q}{c_1; c_2}{R}{R'}$
    if $c$ is an assignment statement and $\findvalue{\Sigma; \Gamma}{\mathsf{ae}(P, c)}{Q}$.
This reduction uses \rulename{Assoc}, \rulename{Seq}, \rulename{Assignment} and
    the reflexivity of assertion entailment.

\begin{figure}
\centering
\begin{mathpar}
    \inferrule*[left=Exists]{
        \Sigma; x:A; \Gamma\vdash\hoareabbr{P}{c}{Q}{Q'}
    } {
        \Sigma; \Gamma\vdash\hoareabbr{\EX{x}{A}{P}}{c}{Q}{Q'}
    }
    \and
    \inferrule*[left=Pure]{
        \mathsf{pure}(P_\mathsf{pure})\and
        \Sigma; \Gamma; P_\mathsf{pure}\vdash\hoareabbr{P}{c}{Q}{Q'}
    } {
        \Sigma; \Gamma\vdash\hoareabbr{P_\mathsf{pure}\land P}{c}{Q}{Q'}
    }
    \and
    \inferrule*[left=Assoc]{
        \Sigma; \Gamma \vdash\hoareabbr{P}{c_1;(c_2;c_3)}{Q}{Q'}
    } {
        \Sigma; \Gamma \vdash\hoareabbr{P}{(c_1;c_2);c_3}{Q}{Q'}
    }
    \and
    \inferrule*[left=Pre]{
        \Sigma; \Gamma; P \vDash Q \and
        \Sigma; \Gamma \vdash\hoareabbr{Q}{c}{R}{R'}
    } {
        \Sigma; \Gamma\vdash\hoareabbr{P}{c}{R}{R'}
    }
    \and
    \inferrule*[left=Skip]{
        \Sigma; \Gamma; P\vDash Q
    } {
        \Sigma; \Gamma \vdash \hoareabbr{P}{\mathsf{skip}}{Q}{Q'}
    }
    \and
    \inferrule*[left=Seq]{
        \Sigma; \Gamma \vdash\hoareabbr{P}{c_1}{Q}{R'} \and
        \Sigma; \Gamma \vdash\hoareabbr{Q}{c_2}{R}{R'}
    } {
        \Sigma; \Gamma\vdash\hoareabbr{P}{c_1;c_2}{R}{R'}
    }
    \and
    \inferrule*[left=Assignment]{
        \findvalue{\Sigma; \Gamma}{\mathsf{ae}(P, c)}{Q} \and
        \Sigma; \Gamma; Q \vDash R
    } {
        \Sigma; \Gamma \vdash\hoareabbr{P}{c}{R}{R'}
    }
    \and
    \inferrule*[left=Break]{
        \Sigma; \Gamma; P \vDash \brkcnd{Q}
    } {
        \Sigma; \Gamma\vdash\hoare{P}{\mathsf{break}}{Q}{\brkcnd{Q}}{\concnd{Q}}{\retcnd{Q}}
    }
    \and
    \inferrule*[left=Continue]{
        \Sigma; \Gamma; P \vDash \concnd{Q}
    } {
        \Sigma; \Gamma\vdash\hoare{P}{\mathsf{continue}}{Q}{\brkcnd{Q}}{\concnd{Q}}{\retcnd{Q}}
    }
    \and
    \inferrule*[left=Return]{
        \Sigma; \Gamma; P \vDash \retcnd{Q}
    } {
        \Sigma; \Gamma\vdash\hoare{P}{\mathsf{return}}{Q}{\brkcnd{Q}}{\concnd{Q}}{\retcnd{Q}}
    }
    \and
    \inferrule*[left=If]{
        \findvalue{\Sigma; \Gamma}{\mathsf{norm}(P\land \denote{b}=\mathsf{true})}{P_\mathsf{true}} \and
        \Sigma; \Gamma\vdash\hoareabbr{P_\mathsf{true}}{c_1}{Q}{Q'} \\
        \findvalue{\Sigma; \Gamma}{\mathsf{norm}(P\land \denote{b}=\mathsf{false})}{P_\mathsf{false}} \and
        \Sigma; \Gamma\vdash\hoareabbr{P_\mathsf{false}}{c_2}{Q}{Q'}
    } {
        \Sigma; \Gamma\vdash\hoareabbr{P}{\cifthenelse{b}{c_1}{c_2}}{Q}{Q'}
    }
    \and
    \inferrule*[left=Loop]{
        \Sigma; \Gamma; P \vDash I \and
        \Sigma; \Gamma\vdash\hoare{I}{c}{\coninv{I}}{Q}{\coninv{I}}{\retcnd{Q}} \and
        \Sigma; \Gamma\vdash\hoare{\coninv{I}}{\cincr{c}}{I}{Q}{\bot}{\retcnd{Q}}
    } {
        \Sigma; \Gamma\vdash\hoare{P}{\cloop{c}{\cincr{c}}}{Q}{\brkcnd{Q}}{\concnd{Q}}{\retcnd{Q}}
    }
\end{mathpar}
    \caption{Proof rules of C Hoare logic}
    \label{fig:choarelogic}
\end{figure}

Besides, VST also proves some other rules sound, including the reverse direction of \rulename{Assoc},
    normal postcondition weakening (\rulename{Post}).
Rule \rulename{IfSeq} and \rulename{NoContinue} are used for additional proof automation.
\begin{mathpar}
    \inferrule*[left=Post]{
        \Sigma; \Gamma; Q \vDash R \and
        \Sigma; \Gamma \vdash\hoareabbr{P}{c}{Q}{R'}
    } {
        \Sigma; \Gamma\vdash\hoareabbr{P}{c}{R}{R'}
    }
    \and
    \inferrule*[left=IfSeq]{
        \Sigma; \Gamma \vdash\hoareabbr{P}{(\cifthenelse{b}{c_1}{c_2}); c_3}{Q}{R}
    } {
        \Sigma; \Gamma\vdash\hoareabbr{P}{\cifthenelse{b}{c_1;c_3}{c_2;c_3}}{Q}{R}
    }
    \and
    \inferrule*[left=NoContinue]{
        \Sigma; \Gamma; P \vDash I \and
        \Sigma; \Gamma\vdash\hoare{I}{c;\cincr{c}}{I}{Q}{\bot}{\retcnd{Q}}
    } {
        \Sigma; \Gamma\vdash\hoare{P}{\cloop{c}{\cincr{c}}}{Q}{\brkcnd{Q}}{\concnd{Q}}{\retcnd{Q}}
    }
\end{mathpar}
Our development, VST-A, is built on the basis of those proof rules in \figref{fig:choarelogic}, \rulename{Post} and \rulename{NoContinue}.
All of these rules
    are proved sound foundationally in VST w.r.t. CompCert Clight semantics
    (if $\mathsf{ae}(\cdot, \cdot)$ and $\mathsf{norm}(\cdot)$ are interpreted as VST's own assignment executor and normalization program).

\subsection{Coq Proof Assistant} \label{ssec:coq}
Coq \cite{COQ} is an interactive theorem prover. Users can write formal definitions and formal proofs in it.
When developing a proof in Coq, users can see all proof goals which are still needed to prove.
Every proof goal contains a proof context (including variables and hypotheses) and a conclusion.
Users can use proof tactics to reduce one proof goal into zero, one or more proof goals.
Moreover, users are allowed to build customized tactics compositionally in Coq.

VST is built in Coq.
In VST, proof contexts $\Sigma$ and $\Gamma$ mentioned in \S \ref{sec:hoarelogic}
correspond to Coq proof context.
VST's assignment executor, $\mathsf{ae}(\cdot, \cdot)$, is written in Coq's tactic language.
Executing $\mathsf{ae}(c, P)$ under context $\Sigma$ and $\Gamma$ constructs not only
    a strongest postcondition $Q$ but also a proof of
    $\Sigma; \Gamma \vdash\hoare{P}{c}{Q}{\bot}{\bot}{\bot}$.
Similarly, $\mathsf{norm}(P)$ constructs an assertion $Q$ and a proof that $\Sigma; \Gamma; P \vDash Q$.

In summary, VST is an interactive C program verification tool whose proof tactics are based on
    a symbolic assignment executor $\mathsf{ae}(\cdot, \cdot)$, a normalization program $\mathsf{norm}(\cdot)$,
    and a set of Hoare logic proof rules.
Executing $\mathsf{ae}(\cdot, \cdot)$ and $\mathsf{norm}(\cdot)$ will generate formal Coq proofs and
    all Hoare logic proof rules are proved sound formally and foundationally in Coq.

\section{Related work}
\label{sec:relate}

\subsection{Traditional annotation verifiers}

Model checking algorithms are very efficient and effective in solving some domain-specific entailments.
Traditional annotation verifiers like VeriFast, Viper and Hip/Sleek use SMT solvers to solve separation logic entailments.
VST-A does not choose a specific solver. Users can choose their own solver---probably a tactic-based one.
We build a simplified version of Hip/Sleek's solver in Coq's tactic language.
It turns out to be very useful for examples like linked-list reverse.
Among four entailments are directly solved, two can be directly solved and the other two need manual proofs for some domain-specific pure facts (like the associativity of list append).

We also noticed the work of sladgehammer \cite{sledgehammer} in the Isabelle community, which integrates some SMT solvers into Isabelle's proof assistant and use them to build reliable proofs.
We believe that similar idea may be applied to Coq or other proof assistant.
VST-A is open for any solver or proof style for verifying entailments, no matter it is interactive proof, or tactic-based solver, or a model checking based one.

Higher order assertions is a drawback of most annotation verifiers.
Among traditional ones, only VeriFast supports higher order. Also, it is usually hard to build proof automation for higher order situations.

Another advantage of VST-A is that itself is foundationally proved sound.
For real world programming languages, there are a lot of subtle settings lying in their semantics and compilers.
So it is very meaningful that we can ensure that what users prove is consistent with the compiler (if they use CompCert to compile), or user can check what does their proved conclusion really depend one (if the use other compilers like gcc to compile).

\subsection{Other interactive program verification tools}
Tools like VST and Iris have devoted a lot to increase proof automation for users to verify their programs conveniently.
However, they all require their users to complete the whole program correctness proofs in an interactive theorem prover. This is not easy for an ordinary software engineer to learn.

The Software Foundation text book \cite{SF} teaches students Hoare logic by a toy language.
It formalizes a Hoare logic and an annotation language in Coq.
Some proof automation can be done using an annotated program.
In comparison,
VST-A works with a real world programming language.
VST-A's users can write annotations in C files but not in Coq.
Supporting "given" is another plus. It is very useful for verifying functional correctness.

Iris proof mode enables users to prove separation logic entailments in a Coq-like interface inside Coq itself.
We may integrate it into VST-A so that users can choose to use it when assertion entailments are not easy to proof using existing tactics.

\subsection{The F* language}

F* \cite{Fstar-dependent}
is a new designed higher order language.
Its key design principle is to support both higher order programming and rich dependent type system.
F* allows users to use either an automated solver or an interactive theorem prover to prove type safety.
Its underlying type system is also verified in Coq.
Comparing with VST-A, F*'s proofs do not only rely on
an interactive theorem prover but also rely on its built-in
automated solvers and the consistency between these two ecosystem.

Moreover, many existing programs are written in C, VST-A's users can just add assertions (as comments) to these C programs and verify them.
New commented source files can be compiled as its original version was.

Also, VST-A is foundational but F* is not. VST-A uses VST Verifiable C's proof rules, which are proved sound w.r.t. the CompCert Clight operational semantics and the Compcert Clight semantics is justified by the CompCert compiler.

\section{Conclusion}
\label{sec:concl}

In this paper, we present VST-A, the first annotation verifier which is itself foundationally verified.
Also it supports a widely used real world language, C, and supports higher order assertions.
Currently, VST-A only supports sequential C program verification.
We plan to support C11 concurrency in the future. Since VST can be used to verify concurrent programs, it should not be too difficult.

Our formal annotation language and other major designs are not C-specific, not separation logic specific, and not VST-specific. We believe that similar development can be used to design other verified annotation checkers for other languages.

\section{Discussion: full-power ITP or a limited segment?}
\label{sec:discuss}

In the previous work of VST-Floyd, authors have already presented a reasonably useful proof automation system in Coq for verifying C programs.
One of their key design choice is to enable their users to use the full power of Coq interactive theorem prover and especially its domain-specific libraries (including theorems and proof tactics) to complete domain-specific proofs.
They made their tool extensible enough w.r.t. domain specific theories so that the tool itself can focus on program verification issues.

1. VST suggests users to apply \textsc{hoare-exists} and \textsc{hoare-pure} to extract existential variables and pure facts from preconditions and then put them into Coq's proof context.

2. VST encourage users to use domain specific theorems and tactic.
For example, VST's sample proofs teach users to use $\mathsf{app\_nil\_r}$ in verifying linked list reverse.
Another typical example is verifyiing linked list append. \figref{fig:ll-append} shows the program.
\begin{figure}[t]
\begin{lstlisting}[language=C, mathescape=true, xleftmargin=4em,xrightmargin=1em, numbers=left, frame = {TB}]
struct list {int head; struct list *tail;};
struct list *append (struct list *x, struct list *y) {
  struct list *t, *u;
  if (x==NULL)
    return y;
  else {
    t = x; u = t->tail;
    while (u!=NULL) {
      t = u; u = t->tail;
    }
    t->tail = y;
    return x;
  }
}
\end{lstlisting}
\caption{Example: linked list append}
\label{fig:ll-append}
\end{figure}
Before executing line 7, we know that the value of $\mathsf{x}$ is not NULL and users are going to prove a Hoare triple of the following form for the $\mathrm{if}$-$\mathrm{else}$ branch:
$$ \{\denote{x} = v \wedge v \neq \mathrm{NULL} \wedge \mathrm{ll}(l_1, v) * \mathrm{ll}(l_2, \denote{\mathsf{y}}) \} \ \ \dots \ \ \{ \dots \} $$
in which $v$ is a logical variable.
VST's sample proof teaches users to do case analysis and discuss whether the content list $l_1$ is empty or not here.
This is a meta-logic case analysis!
In other words, users are allowed to build different Hoare logic proofs for different cases.
Specifically, if $l_1$ is empty here, the precondition just equivalent to false, the whole triple obviously holds; if $l_1$ is nonempty, we can assume that $l_1$ has form $a \ l_1^*$ in which $a$ is $l_1$'s head element.

In the process of developing VST-A, we choose a different design principle comparing to original VST.
We believe that users should not touch the ITP environment at all unless the Hoare triple in the proof goal has been reduced to assertion entailments.
In other words, we choose to use only a very limited segment of Coq in C program verification and allow users to use full power ITP in proving assertion entailments only.
Its influence is two folds.

On one hand, it excludes proofs like what we mentioned above for linked list append.
Meta-logic case analysis is no longer allowed.
We believe that it is not a big problem since we can always replace such meta-logic operation by assertions that directly states the result of that case analysis.
For example, we can assert
$$\exists \ a \ l_1^*, \ \denote{x} = v \wedge a \ l_1^* = l_1 \wedge v \neq \mathrm{NULL} \wedge \mathrm{ll}(l_1, v) * \mathrm{ll}(l_2, \denote{\mathsf{y}})$$
before line 7 in \figref{fig:ll-append}.
Then, users can do case analysis in solving this entailment.

On the other hand, we have now the full control of our proof context.
In VST-A, we tract when every logical variable is introduced.
We use this technique to produce postconditon automatically for some if statements and loops (see \S \ref{sec:verifier}).
However, this is hardly possible in original VST.
VST's users are allowed to modified the proof context manually.
For example, a variable of type $\mathbb{Z} \times \mathbb{Z}$ can be destructed into two variables of $\mathbb{Z}$.
Users can also do case analysis and discuss whether a variable of list type is an empty list or not (like what we describe in the example above for \figref{fig:ll-append}).
If the list in nonempty, the original variable in the context
will be replaced by two: one for the head element and the other for the tail list.
If VST were to tract all variables and hypothesis in proof contexts, it has to re-implement all Coq's standard tactics and all proof tactics from different domain-specific libraries.
This is impossible.

In summary, we believe that, besides allowing users to demonstrate their program correctness proofs in assertions, VST follows a better discipline of using ITP in program verification.
It enables us to write more proof automation tactics in Coq theorem prover.

\section{Frontend Design} \label{sec:frontend}
\begin{figure}[tp]
    \centering
    \includegraphics[scale=0.15]{Clightgen.png}
    \caption{Frontend structure}
    \label{fig:frontend}
\end{figure}
In this section, we show the design of VST-A's frontend,
    which parses a commented C program and generates annotated program in Clight-A.
This program is implemented by applying minimal modifications on CompCert Clightgen,
    which generates Clight program that user wants to verify.
So this method allows us to easily guarantee the annotated program is corresponding to original program.

\figref{fig:frontend} shows structure of VST-A's frontend comparing with
    CompCert's Clight generator (clightgen).
Clightgen first parses C code and then does a series of transformations
    to Clight.
Our frontend first includes comments as strings in parsing and syntax transformation.
We slightly modify Clightgen so that these comments are all preserved.
\S\ref{sec:parser} explains this part in detail.
Then our frontend analyzes the comments and build annotated programs with
    with annotations in Ocaml strings.
And finally, our frontend prints the annotated program
    to a Coq's ``.v'' file, where the annotated program is a formal Coq term.
\S\ref{sec:buildannot} explains this part in detail.

\subsection{Parsing and transformation} \label{sec:parser}
\begin{figure}
\hspace*{-0.03\textwidth}
\begin{subfigure}[b]{0.45\textwidth}
$$\begin{array}{l}
\lstinline|statement| := \\
\mid\ \ \lstinline|compound_statement|\\
\mid\ \ \lstinline|expression_statement|\\
\mid\ \ \cdots\\
\lstinline|compound_statement| := \\
\mid\ \ \lstinline|LBRACE|\ \lstinline|block_item_list|?\
    \lstinline|RBRACE|\\
\lstinline|block_item_list| := \\
\mid\ \ \lstinline|block_item_list|?\ \lstinline|block_item|\\
\lstinline|block_item| := \\
\mid\ \ \lstinline|statement|
\end{array}$$
\caption{Original context free grammar}
\end{subfigure}
~
\begin{subfigure}[b]{0.57\textwidth}
$$\begin{array}{l}
\lstinline|statement| := \\
\mid\ \ \lstinline|compound_statement|\\
\mid\ \ \lstinline|expression_statement|\\
\mid\ \ \cdots\\
\lstinline|compound_statement| := \\
\mid\ \ \lstinline|LBRACE|\ \lstinline|comment_list|?\ \lstinline|block_item_list|?\
    \lstinline|RBRACE|\\
\lstinline|block_item_list| := \\
\mid\ \ \lstinline|block_item_list|?\ \lstinline|block_item|\  \lstinline|comment_list|?\\
\lstinline|block_item| := \\
\mid\ \ \lstinline|statement|
\end{array}$$
\caption{Context free grammar for comment}
\end{subfigure}
    \caption{Context free  grammars comparison}
    \label{fig:parsercfg}
\end{figure}
Clightgen's parser is built by a verified parser generator \cite{CompCert-Parser}
    and a context free grammar for C.
We slightly modify the context free grammar to include comments when parsing.
\figref{fig:parsercfg} shows a comparison between
    original and modified grammar.
\lstinline|LBRACE| and \lstinline|RBRACE| stands for left brace and right brace in C code to parse.
A question mark means this subpattern is optional.
In original parser grammar,
    one kind of statements is compound statement,
    i.e. a code block enclosed by a pair of braces.
There are also other kinds of statements e.g. if-statement and loop.
We omit full definition of statement here
    because it is complex and not relevant to including comment when parsing.
Inside a code block, there is a list of statements, which can be empty.
In this list, comments may occur on the left end, right end and between two statements.
In other words,
    there is an optional list of comments on the left of all statements
    and on the right of each statement.
So we add an optional list of comments on the left of the list of statements
    in grammar rule of \lstinline|compound_statement|,
    and we add an optional list of comments to occur on the right of each statement
    in grammar rule of \lstinline|block_item_list|.
We believe that this design is robust enough to cope with potential future updates of CompCert.

\begin{figure}
\begin{subfigure}[b]{0.4\textwidth}
$$\begin{array}{rrl}
    \text{statement}:&c := &
    c_1; c_2\\
&\mid&  \cifthenelse{e}{c_1}{c_2}\\
&\mid&  \cloop{c_1}{c_2}\\
&\mid&  \cdots
\end{array}$$
\caption{Clight}
\end{subfigure}
~
\begin{subfigure}[b]{0.4\textwidth}
$$\begin{array}{rrl}
\text{statement}:&c := &
        \lstinline|/*comment*/|\ c\\
&\mid&  c\ \lstinline|/*comment*/|\\
&\mid&  c_1; c_2\\
&\mid&  \cifthenelse{e}{c_1}{c_2}\\
&\mid&  \cloop{c_1}{c_2}\\
&\mid&  \cdots
\end{array}$$
\caption{Clight with comment}
\end{subfigure}
    \caption{Syntax of Clight and Clight with comment}
    \label{fig:ClightC}
\end{figure}
After parsing, Clightgen applies a series of transformations to convert C to Clight.
We modify the intermediate representations to preserve comments in this process.
\figref{fig:ClightC} shows the comparison between
    syntax of original Clight and our Clight-with-comment.
Two new syntactic combinators are added to represent comments on the left and right side of a statement.
We also apply similar changes to other intermediate representations
    and adapt each transformation step for preserving comments.
Our modifications are all local and small-scale.
Also, trivially eliminating comments can turn a Clight-with-comment program to the original Clight program.

\subsection{From comment to annotation} \label{sec:buildannot}
After getting program in Clight-with-comments,
    an annotation building process interprets the comments and convert it into annotations.
The job of this process has five aspects.
We show them in next five paragraphs.
After that, we give an example to demonstrate
    how the annotated program user written is processed.
And finally,
    we show how string annotation is converted to syntactic annotation in the last paragraph.

\paragraph{Reassociating sequential compositions}
Clight-A requests the left hand side of every sequential composition
    to be a single statement.
This it to guarantee each given clause encloses all statements after it.
And this also makes it easier for the verifier to find the first single statement.
Annotation building process puts statements in a sequential composition into a list,
    and fold them from right to left.

\paragraph{Finding loop invariants}
Loop invariants appear before loops as comments,
    but they are a component of loop in syntax of Clight-A.
Also, loop invariants may not occur right before loops,
    because the initializing statements in for loops
        are transformed into separated statements before loops,
    and these statements will appear between loops and loop invariants.
So annotation builder finds the closest loop invariants before each loop.
Besides, it allows user to write only one loop invariant instead of two for $\cloop{c}{\cincr{c}}$,
    if $\cincr{c}$ is $\mathsf{skip}$,
    or there are no continue statements in $c$
        (excluding those in inner loops).
In the first case,
    annotation builder uses the single invariant twice,
    because $\{I\}\ \mathsf{skip}\ \{I\}$ is always provable.
In the second case,
    annotation builder transforms the loop into $\cloop{\{c;\cincr{c}\}}{\mathsf{skip}}$ and uses the single invariant twice,
    because this transformation is proved to be sound in VST,
    and VST also uses this transformation for such kind of loops.
If loop invariants are not found before a loop,
    or there is only one loop invariant but the loop is not in one of the two cases mentioned above,
    the annotation builder raises an error.

\paragraph{Generating given clauses}
VST-Floyd symbolic executor requests precondition in canonical form without existential variables,
    so in annotated program, every assertion with existential variables
    must be followed by given clauses.
For users' convenience, annotation builder finds these existential variables in assertions
    and generates given clauses after them automatically.
Annotation builder also finds existential variables in loop invariants
    and generates given clauses at the beginning of loop bodies and incremental statements in the same way.
These automatically generated given clauses cover all the cases that given clauses are needed,
    so users do not need to write any given clauses manually.

\paragraph{Checking postconditions}
As we show in Section~\ref{sec:revert},
    annotation based verifier allows complex statements not followed by an assertion
        if and only if the complex statement has only one normal exit point.
If a complex statement is not followed by an assertion,
    annotation builder checks whether it has only one normal exit point
        using the algorithm shown in \figref{fig:countexit}.

\paragraph{Extracting function specifications}
We allow users to write function specification at the beginning of each function
    using With, Require and Ensure keywords as shown in examples, e.g. \label{fig:userannot},
This is an easy and clear when to write function specifications.
Annotation builder extracts function specifications
    by finding With-Require-Ensure pattern at the beginning of each function
    and print it as a function of multiple parameters.
Later a Coq tactic will convert this function to a formal function specification
    that conforms Verifiable C logic in VST.
Assertions may also use variables mentioned in with clause.
So annotation builder also generate given clauses that effect on the whole function body.
These given clauses at the beginning of function body are bound to variables in with clause
    when initializing the annotation based verifier,

    such that they will not be not a part of the annotated program in proof of the Hoare triple.

\begin{figure}
\begin{subfigure}[b]{\textwidth}
\begin{lstlisting}[language=C, mathescape=true, xleftmargin=2em,xrightmargin=1em, numbers=left, frame = {TB}]
struct list {unsigned head; struct list *tail;};
struct list *reverse (struct list *p) {
  // $\mathrm{With} \ \  l,$
  // $\mathrm{Require} \ \  \ll\left(\denote{\cvar{p}}, l\right)$
  // $\mathrm{Ensure} \ \  \ll\left(\denote{\cvar{ret}}, \mathrm{rev}(l)\right)$
  struct list *w, *t, *v;
  w = NULL; v = p;
  // $\mathrm{Inv} \ \  \exists \ a \ b \ l_1 \ l_2. \ \denote{\cvar{w}} = a \ \wedge \
     \denote{\cvar{v}} = b \ \wedge \
     l = \mathrm{rev}(l_1) \ l_2 \ \wedge \
     \ll\left(a, l_1\right) \ * \
     \ll\left(b, l_2\right)$
  while (v) {
    // $\mathrm{Assert} \ \  \exists \ c \ x \ l_2'. \ \denote{\cvar{w}} = a \ \wedge \
         \denote{\cvar{v}} = b \ \wedge \
         l_2 = x \ l_2' \ \wedge \
         b \mapsto (x, c) \ * \
         \ll\left(a, l_1\right) \ * \
         \ll\left(c, l_2'\right)$
    t = v->tail; v->tail = w; w = v; v = t;
  }
  return w;
}
\end{lstlisting}
    \caption{The annotated program that user writes}
\end{subfigure}\\
\begin{subfigure}[b]{\textwidth}
\begin{lstlisting}[language=C, mathescape=true, xleftmargin=2em,xrightmargin=1em, numbers=left, frame = {TB}]
struct list {unsigned head; struct list *tail;};
reverse_spec :=
  $(\lambda\ l.\ \left(\ll\left(\denote{\cvar{p}}, l\right), \ll\left(\denote{\cvar{ret}}, \mathrm{rev}(l)\right)\right))$
reverse_hint :=
  // $\mathrm{Given}\ l,$
  w = NULL; v = p;
  // $\mathrm{Inv} \ \  \exists \ a \ b \ l_1 \ l_2. \ \denote{\cvar{w}} = a \ \wedge \
     \denote{\cvar{v}} = b \ \wedge \
     l = \mathrm{rev}(l_1) \ l_2 \ \wedge \
     \ll\left(a, l_1\right) \ * \
     \ll\left(b, l_2\right)$
  // $\mathrm{Inv} \ \  \exists \ a \ b \ l_1 \ l_2. \ \denote{\cvar{w}} = a \ \wedge \
     \denote{\cvar{v}} = b \ \wedge \
     l = \mathrm{rev}(l_1) \ l_2 \ \wedge \
     \ll\left(a, l_1\right) \ * \
     \ll\left(b, l_2\right)$
  $\textbf{loop}$ ($\mathsf{skip}$) {
    // $\mathrm{Given} \ a \ b \ l_1 \ l_2,$
    if (v)
      $\mathsf{skip}$;
    else
      break;
    // $\mathrm{Assert} \ \  \exists \ c \ x \ l_2'. \ \denote{\cvar{w}} = a \ \wedge \
         \denote{\cvar{v}} = b \ \wedge \
         l_2 = x \ l_2' \ \wedge \
         b \mapsto (x, c) \ * \
         \ll\left(a, l_1\right) \ * \
         \ll\left(c, l_2'\right)$
    // $\mathrm{Given} \ c \ x \ l_2',$
    t = v->tail; v->tail = w; w = v; v = t;
  }
  return w;
\end{lstlisting}
    \caption{The annotated program that annotation builder generates}
\end{subfigure}
    \caption{Example: frontend's effects}
    \label{fig:examplefrondend}
\end{figure}
\paragraph{Example}
\figref{fig:examplefrondend} shows an example.
First, frontend parses annotated program written by user with comments
    and preforms transformations to Clight with comment,
    e.g. replacing while-loop with general loop.
Then, function specification is extracted from comment to a function of $l$.
User only gives one loop invariant.
It is duplicated by annotation builder
    because incremental statement in while-loop is $\mathsf{skip}$.
User does not write an assertion after the loop.
Annotation builder checks that
    the loop has only one normal exit point,
    so it allows user to omit this assertion.

\begin{figure}
\hspace*{-0.02\textwidth}
\begin{subfigure}[b]{0.5\textwidth}
$$\begin{array}{rrl}
    \text{string}:&s := & \cdots\\
    \text{statement}:&c := &
        \mathrm{Given}\ s\ c\\
&\mid&  \mathrm{Assert} \ \  s\\
&\mid&  \aloop{s_1}{s_2}{c_1}{c_2}\\
&\mid&  \cdots
\end{array}$$
    \caption{Syntax of Clight-A with string annotation}
\end{subfigure}
~
\begin{subfigure}[b]{0.5\textwidth}
$$\begin{array}{rrl}
    \text{assertion}:&P := & \cdots\\
    \text{identifier}:&x := & \cdots\\
    \text{type}:&A := & \cdots\\
    \text{statement}:&c := &
        \Given{x}{A}{c}\\
&\mid&  \mathrm{Assert} \ \  P\\
&\mid&  \aloop{P_1}{P_2}{c_1}{c_2}\\
&\mid&  \cdots
\end{array}$$
    \caption{Syntax of Clight-A with syntactic annotation}
\end{subfigure}
    \caption{Comparison between string annotation and syntactic annotation}
    \label{fig:compareprint}
\end{figure}
\paragraph{Printing}
It is worth mentioning that annotation builder generates Clight-A with string annotation,
    instead of Clight-A with syntactic annotation.
\figref{fig:compareprint} shows the differences between string annotation and syntactic annotation.
Strings are more flexible and easier to process.
When printing to Coq's ``.v'' file,
    string annotations are printed at proper positions
    and become syntactic annotation.

\section{Introduction}

In the past 15 years, researchers have built series of tools for program verification.
Tools like CakeML \cite{CF-CakeML}, Iris \cite{IrisProofMode, IrisJournal}, VST \cite{VST, VST-Floyd}
(interactive program verification tools) are built in interactive theorem provers like Coq \cite{COQ} or Isabelle \cite{Isabelle}.
Also, their users are required to write formal program correctness proofs in the same theorem prover.
Tools like Dafny \cite{dafny}, Hip/Sleek \cite{hipsleek}, VeriFast \cite{verifast} and Viper \cite{viper}
(annotation verifiers) do not need users to write formal proofs but rely on sufficient assertions annotated in programs.
Tools like CBMC \cite{cbmc}, F-Soft \cite{fsoft, fsoft-journal} and Infer \cite{infer} do not even need much annotation.

Different tools have their advantages and disadvantages.

(1) One significant advantage of interactive tools is that these tools themselves are \emph{formally proved sound}.
This is especially meaningful for verifying real world programming languages and for verifying higher-order properties like functional correctness.
On one hand, real world programming languages are complicated.
For example, it is very subtle what C programs may cause undefined behavior.
On the other hand, an advanced program logic for higher-order properties usually has a nontrivial soundness proof.
For example, VST and Iris use step-indexed semantics for interpreting impredicative assertion languages whose soundness proof is complicated.

As far as we know, no annotation verifier has a formal soundness proof yet.

(2) Interactive program verification tools also benefit from \emph{the rich language} of Coq (and Isabelle, etc.) for writing formal definitions and proofs.
These tools can easily have higher-order functions and predicates in their assertion languages.
At the same time, it is convenient for them to have addition logic connectives and unrestricted user-defined predicates.

When designing the assertion language of an annotation verifier, one have to compromise between its expressiveness and the efficiency of assertion entailment checkers.

(3) Annotation verifiers are easier to use for ordinary software engineers.
\emph{Writing annotations is a much more straightforward way of demonstrating that a program is correct.}
For example, \figref{fig:ll-reverse} shows an implementation of in-place linked list reverse and its functional correctness proof.
\footnote{This is a separation logic \cite{reynolds02} proof.
In other words,
we use an assertion of form "$P * Q$" to say that the memory can be split into two disjoint pieces of which one satisfies $P$ and the other satisfies $Q$.}
The loop invariant and assertions clearly state what criteria the program state should have at every point.

In comparison, learning to use a theorem prover, and writing formal proofs for program correctness is a high threshold.

\begin{figure}
\begin{lstlisting}[language=C, mathescape=true, xleftmargin=2em,xrightmargin=1em, numbers=left, frame = {TB}]
struct list {unsigned head; struct list *tail;};
struct list *reverse (struct list *p) {
  // $\mathrm{With} \ \  l,$
  // $\mathrm{Require} \ \  \ll\left(\denote{\cvar{p}}, l\right)$
  // $\mathrm{Ensure} \ \  \ll\left(\denote{\cvar{ret}}, \mathrm{rev}(l)\right)$
  struct list *w, *t, *v;
  w = NULL; v = p;
  // $\mathrm{Inv} \ \  \exists \ a \ b \ l_1 \ l_2. \ \denote{\cvar{w}} = a \ \wedge \
     \denote{\cvar{v}} = b \ \wedge \
     l = \mathrm{rev}(l_1) \ l_2 \ \wedge \
     \ll\left(a, l_1\right) \ * \
     \ll\left(b, l_2\right)$
  while (v) {
    // $\mathrm{Given} \ a \ b \ l_1 \ l_2,$
    // $\mathrm{Assert} \ \  \exists \ c \ x \ l_2'. \ \denote{\cvar{w}} = a \ \wedge \
         \denote{\cvar{v}} = b \ \wedge \
         l_2 = x \ l_2' \ \wedge \
         b \mapsto (x, c) \ * \
         \ll\left(a, l_1\right) \ * \
         \ll\left(c, l_2'\right)$
    // $\mathrm{Given} \ c \ x \ l_2',$
    t = v->tail; v->tail = w; w = v; v = t;
    // $\mathrm{Assert} \ \  \denote{\cvar{w}} = b \ \wedge \
         \denote{\cvar{v}} = c \ \wedge \
         b \mapsto (x, a) \ * \
         \ll\left(a, l_1\right) \ * \
         \ll\left(c, l_2'\right)$
  }
  // $\mathrm{Assert} \ \  \ll\left(\denote{\cvar{w}}, \mathrm{rev}(l)\right)$
  return w;
}
\end{lstlisting}
\caption{Annotations for verifying linked-list reverse}
\label{fig:ll-reverse}
\end{figure}

In this paper, we show that these targets do not conflict with each other; one verification tool can achieve them all.
We build VST-A, a foundationally sound annotation verifier with a rich higher-order annotation language.
It is built based on the following previous works:
\begin{enumerate}
	\item CompCert Clight syntax and operational semantics, which is formal definition of C language and C program behavior;
	\item CompCert Clightgen, a verified parser and preprocessor that turns C source code into Clight AST;
	\item VST Verifiable C, which is a separation logic for C program verification formally proved sound w.r.t. CompCert Clight semantics;
	\item VST Floyd, a proof automation system in Coq for using Verifiable C to verify C programs.
\end{enumerate}

The most important component of VST-A is Clight-A, a formal language of annotated C programs.
This language does not only define C statements and assertions, but also involves verification context transformation.
For example, in \figref{fig:ll-reverse} new logical variables $c$, $x$ and $l_2'$ are introduced in the middle of verification at line 12 and they can be used in later assertions in the loop body.

Base on that, we build a parser which turns C programs and comments into this formal language and a foundationally sound verifier which uses annotated programs as guide.

In order to use VST-A, one can first write C functions in a ``.c'' file, then use CompCert Clightgen and our parser to generate Coq ``.v'' files which contain the corresponding Clight AST and Clight-A AST, and all C function specifications extracted from the comments.
In the end, users can use our one-line verification command ``\lstinline|verify|'' to check whether the assertions and invariants in the original ``.c'' file suffices to prove those C functions correct.
Specifically, function specifications are pre/postconditions written in VST Verifiable C's higher-order separation logic.
The VST-A tactic\footnote{A Coq tactic is a proof command which reduces one proof goal zero, one or more proof goals using proved theorems (see \S \ref{ssec:coq}). Users are allowed to build customized tactics compositionally in Coq. ``\lstinline|Verify|'' is such a customized tactic built by VST-A.} ``\lstinline|verify|'' reduces Hoare triples to series of entailments which cannot be solved automatically.

Our experience of building VST-A shows that, in order to reduce a Hoare triple to assertion entailments, we do not need the full flexibility of Coq's Ltac language.
Moreover, if we use the underlying logic of Coq in a disciplined way, we can gain additional convenience in building proof automation.

We organize the rest of this paper as follows.
We introduce background information about Coq theorem prover and VST in \S \ref{sec:backgrnd}.
We demonstrate our annotated C syntax Clight-A, our verifier and and VST-A's frontend (including parser) in
\S \ref{sec:annot}, \S \ref{sec:verifier} and \S \ref{sec:frontend}, respectively.
In \S \ref{sec:discuss}, we discuss the benefit of only disciplinedly using interactive theorem proving.
In the end, we discuss related works in \S \ref{sec:relate} and conclude in \S \ref{sec:concl}.

\paragraph{Remark.} In order to verify pointers in C programs, VST-A is separation logic based.
However, we simply use the separation logic facilities from VST. The whole development is not heavily depended on separation logic. Thus we will mostly omit such irrelevant details in this paper.

\section{Annotation Verifier} \label{sec:verifier}
In this section, we show how we build the annotation verifier.
Given enough annotation, the verifier can reduce a Hoare triple to a series of entailments.

\subsection{Verifier Strategy}
Our annotation verifier uses the proof rules for annotated programs
    (either following program AST or following annotations) most of the time,
    except for \rulename{Seq} rule.
It requires an assertion $Q$ in the middle,
    which is hard to generate directly.
So instead of using \rulename{Seq} rule,
    we use the alternative rules shown in \figref{fig:altseqrules}.
$\mathsf{assign}(c)$ means $c$ is an assignment statement,
    and $\mathsf{complex}(c)$ means $c$ is an if-statement or loop.
These rules are provable using original proof rules in \figrefs{fig:annotrules1}{fig:annotrules2}.
\rulename{SeqAssign} is proved by applying \rulename{Seq} and then applying \rulename{Assignment}.
\rulename{SeqComplex} is proved by applying \rulename{Seq} and then applying \rulename{SeqAssertion}.
\begin{figure}
\begin{mathpar}
    \inferrule*[left=SeqAssign]{
        \mathsf{assign}(c_1) \and
        \findvalue{\Sigma; \Gamma}{\mathsf{ae}(P, c_1)}{Q} \and
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{Q}{c_2}{R}{R'}}{C_2}
    } {
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{c_1;c_2}{R}{R'}}{c_1;C_2}
    }
    \and
    \inferrule*[left=SeqComplex]{
        \mathsf{complex}(c_1) \and
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{c_1}{Q}{R'}}{C_1} \and
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{Q}{c_2}{R}{R'}}{C_2}
    } {
        \hintprovable{\Sigma; \Gamma}{\hoareabbr{P}{c_1; c_2}{R}{R'}}{C_1;\mathrm{Assert} \ \  Q; C_2}
    }
\end{mathpar}
    \caption{Alternative proof rules for sequential statement}
    \label{fig:altseqrules}
\end{figure}

The verifier repeats applying a rule chosen with the following strategy until the remaining proof goals are assertion entailments.
\begin{enumerate}
    \item If the annotated program starts with a given clause, apply \rulename{Given}/\rulename{ImpGiven} rule.
    \item If a pure proposition can be extracted after simple transformation,
        transform and apply \rulename{Pure}/\rulename{ImpPure} rule.
    \item If the annotated program is in form of $\mathrm{Assert} \ \  Q$ or $\mathrm{Assert} \ \  Q; C$,
        apply \rulename{Assertion}/\hspace*{0pt}\rulename{SeqAssertion}/\rulename{ImpAssertion} rule.
    \item If the annotated program is an assignment/if-statement/loop/break/continue/return,
        apply \rulename{Assignment}/\rulename{If}/\rulename{Loop}/\rulename{Break}/\rulename{Continue}/\rulename{Return} rule.
    \item If the program statement is a single statement $c$ (i.e. not in form of $c_1; c_2$),
        but the annotated program is in form of $c; C$,
        apply \rulename{SeqPost} rule.
    \item
    \begin{itemize}
        \item Otherwise, the program statement is in form of $c_1; c_2$
        and the annotated program is in form of $C_1; C_2$.
        \item Then repeat applying \rulename{Assoc} rule until
            the program statement is in form of $c_1; c_2$ and
            $c_1$ is a single statement.
        \item Then apply \rulename{SeqAssign}/\rulename{SeqComplex} rule,
            depending on whether the first statement is an assignment or a complex statement;
            if a complex statement is not followed by an assertion, but followed by other statements,
                there are not any applicable rules,
                that means the user must give an assertion after a complex statement,
                because VST forward symbolic executor cannot generate a postcondition for a complex statement;
            it is guaranteed that
                the program statement and the annotated program are
                separated at the same point,
            because $C_1$ of the annotated program
                must be a single statement according to the syntax.
    \end{itemize}
\end{enumerate}

\begin{figure}
\begin{lstlisting}[language=C, mathescape=true, xleftmargin=2em, xrightmargin=1em, frame = {TB}, title=contexts and assertions]
$\begin{array}{lclclcl}
    \Sigma &:= & l &\quad \quad \quad \quad \quad \quad & P &:=& \ll(\denote{\cvar{p}}, l) \\
    \Gamma &:=& \emptyset &\quad \quad \quad \quad \quad \quad & \retcnd{Q} &:=& \ll(\denote{\cvar{ret}}, \mathrm{rev}(l))
\end{array}$
\end{lstlisting}

\begin{lstlisting}[language=C, mathescape=true, xleftmargin=2em, xrightmargin=1em, numbers=left, frame = {TB}, title=program of reverse ($c$)]
  w = NULL; v = p;
  $\textbf{loop}$ ($\mathsf{skip}$) {
    if (v)
      $\mathsf{skip}$;
    else
      break;
    t = v->tail; v->tail = w; w = v; v = t;
  }
  return w;
\end{lstlisting}
\begin{lstlisting}[language=C, mathescape=true, xleftmargin=2em, xrightmargin=1em, numbers=left, frame = {TB}, title=annotated program of reverse ($C$)]
  w = NULL; v = p;
  // $\mathrm{Inv} \ \  \exists \ a \ b \ l_1 \ l_2. \ \denote{\cvar{w}} = a \ \wedge \
     \denote{\cvar{v}} = b \ \wedge \
     l = \mathrm{rev}(l_1) \ l_2 \ \wedge \
     \ll\left(a, l_1\right) \ * \
     \ll\left(b, l_2\right)$
  // $\mathrm{Inv} \ \  \exists \ a \ b \ l_1 \ l_2. \ \denote{\cvar{w}} = a \ \wedge \
     \denote{\cvar{v}} = b \ \wedge \
     l = \mathrm{rev}(l_1) \ l_2 \ \wedge \
     \ll\left(a, l_1\right) \ * \
     \ll\left(b, l_2\right)$
  $\textbf{loop}$ ($\mathsf{skip}$) {
    // $\mathrm{Given} \ a \ b \ l_1 \ l_2,$
    if (v)
      $\mathsf{skip}$;
    else
      break;
    // $\mathrm{Assert} \ \  \exists \ c \ x \ l_2'. \ \denote{\cvar{w}} = a \ \wedge \
         \denote{\cvar{v}} = b \ \wedge \
         l_2 = x \ l_2' \ \wedge \
         b \mapsto (x, c) \ * \
         \ll\left(a, l_1\right) \ * \
         \ll\left(c, l_2'\right)$
    // $\mathrm{Given} \ c \ x \ l_2',$
    t = v->tail; v->tail = w; w = v; v = t;
  }
  // $\mathrm{Assert} \ \  \ll(\denote{\cvar{w}}, \mathrm{rev}(l))$
  // $\mathrm{Given} \ w,$
  return w;
\end{lstlisting}
    \caption{Proof goal details for verifying linked-list reverse}
    \label{fig:annotwithpost}
\end{figure}
For example,
    in order to verify the linked list reverse program (in \figref{fig:ll-reverse}),
    we need to prove the following triple (see definitions in \figref{fig:annotwithpost}):
\begin{equation}
    \Sigma; \Gamma \vdash \hoare{P}{c}{\bot}{\bot}{\bot}{\retcnd{Q}}
    \label{eqn:reversegoal}
\end{equation}
We can use annotated program $C$ and prove
\begin{equation}
    \hintproves{\Sigma; \Gamma}{\hoare{P}{c}{\bot}{\bot}{\bot}{\retcnd{Q}}}{C},
    \label{eqn:reverseannotgoal}
\end{equation}
    then Theorem~\ref{thm:vst-a-sound}
    shows $\Sigma; \Gamma \vdash \hoare{P}{c}{\bot}{\bot}{\bot}{\retcnd{Q}}$.
Here we describe how our verifier proves \eqref{eqn:reverseannotgoal} as follows
We ignore the usage of \rulename{Assoc} rule in this example,
    because the way that program statements are connected is not shown when program is written in
    C-language style.
\begin{enumerate}
    \item Apply \rulename{SeqAssign} rule twice to use symbolically execute the first two statements.
    \item Apply \rulename{SeqComplex} rule to separate the loop from the remaining statements.
    \item Apply \rulename{Loop} rule for the loop;
        this generates three proof goals:
            (1) $P_1\vDash I$, where $P_1$ is precondition before the loop and $I$ is the loop invariant,
            (2) proof goal for loop body
            and (3) proof goal for incremental statement;
        the third proof goal is then reduced to entailment by applying \rulename{Skip} rule;
    \item Apply \rulename{Given} for four times in introduce
        $a, b, l_1$ and $l_2$ to variable context $\Sigma$,
        and apply \rulename{Pure} rule to extract
            proposition $l=\mathrm{rev}(l_1)\ l_2$ to
            proposition context $\Gamma$.
    \item Apply \rulename{SeqComplex} rule
        and then \rulename{Loop} rule for the if-statement.
    \item For two branches in the if-statement
        and statements after the if-statement,
        apply proof rules similarly to reduce to entailments.
    \item For statements after the loop,
        apply \rulename{Given} rule
        and then \rulename{Return} rule
        to reduce to entailments.
\end{enumerate}
In the end,
    the verifier reduces the proof goal of annotated program
    to a series of assertion entailments.
These entailments are left to user to prove in Coq using Coq tactics.

\subsection{Reverting to Generate Postcondition}
\label{sec:revert}
\begin{figure}
\begin{lstlisting}[language=caml, mathescape=true, xleftmargin=4em,xrightmargin=1em, numbers=left, frame = {TB}]
let count_normal_exit ($c$: annotated program) :=
  match $c$ with
  | $\Given{x}{A}{c}$ => count_normal_exit $c$
  | $c_1; c_2$ =>
      let $n_1$ := count_normal_exit $c_1$ in
      match $c_2$ with
      | $\mathsf{skip}$ => $n_1$
      | _ =>
        let $n_2$ := count_normal_exit $c_2$ in
        if $n_1 = 0$
          then $0$
          else $n_2$
      end
  | $\cifthenelse{e}{c_1}{c_2}$ =>
      let $n_1$ := count_normal_exit $c_1$ in
      let $n_2$ := count_normal_exit $c_2$ in
      $n_1+n_2$
  | $\aloop{I}{\coninv{I}}{c}{\cincr{c}}$ =>
      count_break $c$
  | $\mathsf{break}$ | $\mathsf{continue}$ | $\mathsf{return}$ => $0$
  | _ => $1$
  end.
\end{lstlisting}
    \caption{Pseudocode for counting normal exit points}
    \label{fig:countexit}
\end{figure}
The annotation based verifier described above requests users to write a postcondition
    for every if-statement and loop that is followed by other statements.
This may be not enjoyable for users.
So, in this section,
    we enhance our verifier to allow users to omit
    postconditions after complex statements with only one normal exit point.
The number of normal exit points of an annotated program $C$
    is number of entailments in the form of
    $\Sigma; \Gamma; P\vDash Q$
    generated by verifier to prove the goal
    $\hintprovable{\Sigma_0; \Gamma_0}{\hoareabbr{P_0}{c}{Q}{Q'}}{C}$,
    and this number only depends on $C$.
For example,
    in the annotated program shown in \figref{fig:annotwithpost},
    the loop only has one normal exit,
        which is the break statement;
    and the if-statement also has one normal exit,
        because one of the branches is to break.
\figref{fig:countexit} shows the method to count number of normal exits
    without actually applying proof rules.

\begin{figure}
\begin{mathpar}
    \inferrule*[left=RevertVar]{
        \Sigma; \Gamma; \EX{x}{A}{P} \vDash Q
    } {
        \Sigma; x:A; \Gamma; P \vDash Q
    }
    \and
    \inferrule*[left=RevertProp]{
        \Sigma; \Gamma; P_\mathsf{pure}\land P \vDash Q
    } {
        \Sigma; \Gamma; P_\mathsf{pure}; P \vDash Q
    }
\end{mathpar}
    \caption{Revert proof rules}
    \label{fig:revertrules}
\end{figure}
A complex statement $C'$ has only one normal exit,
    means there will be only one occurrence of postcondition $Q$ in the entailments left by the verifier.
In the execution of the verifier to prove a Hoare triple $\hoareabbr{P}{c}{Q}{Q'}$,
    the postcondition $Q$ is never used by the verifier but only remained in the entailments.
Does that means we can let $Q:=P$,
    where $P$ is from the remaining entailment $\Sigma; \Gamma; P\vDash Q$,
    to apply \rulename{Seq} rule
    when proving $\hintproves{\Sigma_0; \Gamma_0}{\hoareabbr{P_0}{c; c_2}{R}{R'}}{C'; C_2}$?
The answer is negative,
    because context of the entailment $\Sigma; \Gamma$ may be not the same as $\Sigma_0; \Gamma_0$.
Fortunately, the proof rules that the annotation verifier uses only add new items into context.
This is different from full interactive proof, where user may change the context in any way she wants.
So $\Sigma; \Gamma$ is obtained from $\Sigma_0; \Gamma_0$ by adding new variables and propositions.
Conversely, we can revert these variables and propositions into assertion to get an assertion $P_\mathrm{revert}$,
    such that $\Sigma_0; \Gamma_0; P_\mathrm{revert}\vDash Q$ implies $\Sigma; \Gamma; P\vDash Q$.
The verifier use proof rules shown in \figref{fig:revertrules} for reversion as follows.
\begin{enumerate}
    \item Apply \rulename{RevertProp} until $\Gamma=\Gamma_0$;
    \item Apply \rulename{RevertVar} until $\Sigma=\Sigma_0$.
\end{enumerate}
We prove \rulename{RevertProp} and \rulename{RevertVar} sound in Coq.

\begin{figure}
\begin{lstlisting}[language=C, mathescape=true, xleftmargin=2em, xrightmargin=1em, numbers=left, frame = {TB}]
  w = NULL; v = p;
  // $\mathrm{Inv} \ \  \exists \ a \ b \ l_1 \ l_2. \ \denote{\cvar{w}} = a \ \wedge \
     \denote{\cvar{v}} = b \ \wedge \
     l = \mathrm{rev}(l_1) \ l_2 \ \wedge \
     \ll\left(a, l_1\right) \ * \
     \ll\left(b, l_2\right)$
  // $\mathrm{Inv} \ \  \exists \ a \ b \ l_1 \ l_2. \ \denote{\cvar{w}} = a \ \wedge \
     \denote{\cvar{v}} = b \ \wedge \
     l = \mathrm{rev}(l_1) \ l_2 \ \wedge \
     \ll\left(a, l_1\right) \ * \
     \ll\left(b, l_2\right)$
  $\textbf{loop}$ ($\mathsf{skip}$) {
    // $\mathrm{Given} \ a \ b \ l_1 \ l_2,$
    if (v)
      $\mathsf{skip}$;
    else
      break;
    // $\mathrm{Assert} \ \  \exists \ c \ x \ l_2'. \ \denote{\cvar{w}} = a \ \wedge \
         \denote{\cvar{v}} = b \ \wedge \
         l_2 = x \ l_2' \ \wedge \
         b \mapsto (x, c) \ * \
         \ll\left(a, l_1\right) \ * \
         \ll\left(c, l_2'\right)$
    // $\mathrm{Given} \ c \ x \ l_2',$
    t = v->tail; v->tail = w; w = v; v = t;
  }
  return w;
\end{lstlisting}
    \caption{Annotated program of reverse without loop postcondition}
    \label{fig:annotwithoutpost}
\end{figure}
We use the annotated program of reverse without loop postcondition (\figref{fig:annotwithoutpost})
    to demonstrate how reversion works.
\begin{enumerate}
    \item Apply \rulename{SeqAssign} rule twice for first two statements.
    \item Apply \rulename{Seq} rule with $Q := {?Q}$, where $?Q$ indicates an unknown assertion;
        current context is $\Sigma_0= l$, $\Gamma_0=\emptyset$.
    \item Verify the loop, and get an entailment
        $$ l; a; b; l_1; l_2; l=\mathrm{rev}(l_1)\ l_2; b = \mathsf{NULL}; P \vDash {?Q}. $$
    \item Compare context in the entailment with the context when applying \rulename{Seq} rule.
        Apply \rulename{RevertProp} rule twice and \rulename{RevertVar} rule for four times to
        make the entailment has the same context as when applying \rulename{Seq} rule;
        the result is
        $$ l; \exists\ a\  b\  l_1\  l_2.\ l=\mathrm{rev}(l_1)\ l_2\ \land\  b = \mathsf{NULL}\ \land\  P \vDash {?Q}. $$
    \item Let $?Q$ be $\exists\ a\  b\  l_1\  l_2.\ l=\mathrm{rev}(l_1)\ l_2\ \land\  b = \mathsf{NULL}\ \land\  P$,
        and the entailment above holds by reflexivity.
    \item For statements after the loop, apply \rulename{Exists} rule for four times to introduce variables.
    \item the remaining steps are not changed.
\end{enumerate}

In Coq, there is a mechanism called \emph{unification variable}, that allows
    a variable to be uninstantiated when applying a lemma.
As a result, residue proof goals will have a hole;
    the uninstantiated variable (also called unification variable) needs to be filled in later proofs.
This mechanism is exactly what we need to implement
    the reversion to generate postcondition.

redpajama_set_name: RedPajamaArXiv


God has given us a heart to live for Him and for the German and English speaking people of Europe. We are excited about all God has planned for us. What a blessing and a joy to serve the Lord together. Our goal is to see people saved and living for the Lord, seeking to walk pleasing before Him each day.
We are also excited about the opportunity to be a blessing and minister to people all over through the video aspect of the ministry.
As Matthew 5:16 says: "Let your light so shine before men, that they may see your good works, and glorify your Father which is in heaven." It is a privilege and an honor to serve the Lord. Thanks be to God that we may serve Him in ministry.


The kindergarten style is intended for the beginning printer and narrow style for the older student using manuscript or cursive writing. We have found that kindergarten students also do well with the regular style.
There are many ways in which the paper can be incorporated into your curriculum. For example, the paper can be cut into narrow vertical or horizontal strips. The vertical strips could then be used for a spelling list. The horizontal strip could be used for an alphabet model placed on the student's desk. You can punch holes in the paper and bind it to make a personal journal for the student. You can further cut down the paper to fit on a mailing envelope. See some examples below.
Research has found that students read better with different colored overlays. Therefore we offer the paper in two colors with the same idea that some students would prefer the yellow and some the blue. It's a good idea to try the different colors with each student.
The following are examples from two of Ellen's students. Compare the results of students' work on normal paper vs. BrightLines paper.
The following is an example of one of Ellen's students hard at work!


Interested in learning more about the Library of Congress? Check out this video (1 hour, 31 minutes) created by C-Span.
C-SPAN's original feature documentary, The Library of Congress, is a behind-the-scenes look at the national repository, providing the history of the institution, a tour of its iconic Jefferson Building, and glimpses of some of the library's rare book, photo, and map collections. The film also featured some of the presidential papers housed at the Library of Congress, ranging from George Washington through Calvin Coolidge. Viewers learned how the library uses technology to preserve its holdings and expand public access to them, as well as how technology is helping to uncover new information about some of the items in its collections.
This is a well done video!
I suspect that there are some other hidden gems hidden in the C-SPAN Video Library – please post a comment if you come across other videos of interest to genealogists.
Henry Louis Gates Jr on his books: "Lincoln on Race and Slavery" and "In Search of Our Roots: How 19 Extraordinary African Americans Reclaimed Their Past"
Professor Bryan Sykes on "The Seven Daughters of Eve: The Science That Reveals our Genetic Ancestry"
at the Key West Literary Seminar several author panelists "talked about their ancestors and their effect on their writing."
"The National Research Council and Institute of Medicine held a symposium to explore the health, policy, and ethical implications of direct-to-consumer genetic testing."


text:
Penny Baber is Recipient of Tradition of Excellence Award
James P. "Penny" Baber, who opened his general practice in Cumberland County in 1961, has been named the 2017 recipient of the Tradition of Excellence Award by the Virginia State Bar's General Practice Section.
The award recognizes a lawyer who embodies the highest tradition of personal and professional excellence and who has benefitted the community and enhanced the esteem of general practice attorneys in Virginia. It will be presented on June 17 during the VSB Annual Meeting at Virginia Beach.
Vivian Seay Giles, the Cumberland County attorney and county administrator, wrote in nominating him for the award that: "Mr. Baber stands as a monument in our community of the true southern gentleman lawyer who has served his community and the Virginia State Bar as a sole practitioner for fifty-six years."
Baber has served as the commonwealth's attorney and the Cumberland County attorney, and is currently the commissioner of accounts. He is also active in his community, where he has been a member of the Ruritan Club, served as a Boy Scout troop leader and on the board of directors of the Deep Run Hunt Club, and serves as a trustee of the St. James Episcopal Church in Cartersville.
"I am nominating Mr. Penny Baber for the Tradition of Excellence award, not because of any single monumental achievement or specific success of which I am aware, but for his fifty-six years of service, excellence and professionalism in the practice of law in Central Virginia," Giles wrote. "Mr. Baber has served, and continues to serve, as an example of the highest professional ethics and legal skill for those of us fortunate enough to practice with him."
Baber graduated from the University of Richmond in 1958. He received his law degree from the University of Virginia in 1961.

redpajama_set_name: RedPajamaCommonCrawl


text:
What's in a Name? A Jihadi Labels Himself
Joas Wagemakers
As all academics know, defining the subject you study is very important and often complicated. This is obviously no different in the study of jihadis, where terms such as "radical Muslims", "Muslim extremists", "Jihadi-Salafis", "takfiris" and even "Islamo-fascists" are often used to describe Muslims engaging in violence against others. Such terms are based on criteria set by outsiders, sometimes resulting in terms that are crude, imprecise and/or used to describe people who strongly differ from one another.
Others take the approach of simply listening to what the people that one's research focuses on – in this case jihadis – call themselves. This often yields widely divergent and biased answers that are frequently ill-suited to be used by academics. Terms such as "Muslims", "mujahidun" and "ahl al-Sunna wa-l-jama'a", for example, are rather general and, more importantly, are also claimed by Muslims who have nothing to do with al-Qa'ida whatsoever.
Defining one's subject of research is thus often quite difficult. The fact that asking jihadis – for lack of a better term – to define themselves often yields unsatisfactory answers does not mean, however, that it is not interesting to listen to what they say. An example of a radical Muslim scholar who recently tried to provide an answer to the question "Who are we?" is Abu l-Mundhir al-Shinqiti, the Mauritanian shaykh who seems to be running the Shari'a Forum of the Minbar al-Tawhid wa-l-Jihad – originally a collective effort by about a dozen scholars – entirely on his own these days.
Al-Shinqiti's starting point is that Islam is one and that the jihadis he is addressing should stand together against "the enemies", which they are apparently not doing now, according to him. Although it is clear that Abu l-Mundhir believes jihad is legitimate, both against non-Muslim invaders and "apostate" rulers in the Muslim world, unity should not be limited to fighting but should encompass every aspect of Islam and he cites many a hadith to make his case.
If jihadis came together to practise their religion as one, al-Shinqiti states, they should also have one name to describe themselves. This name should reflect the fact that jihadis strive for the application of the Shari'a, as well as their desire to fulfill the obligations of Islam. What name could possibly cover this?
The alternatives
An name that al-Shinqiti briefly considers is "Salafis". He states that several names are applied to jihadis that lead to a misrepresentation of who they are, and "Salafis" is one of them. Sure, Abu l-Mundhir writes, we are Salafis, but that label has come to be associated with people who do not wage jihad, help "apostate" rulers and take part in democracy. These are obviously characteristics that al-Shinqiti wants to avoid and therefore he dismisses "Salafis" as a good name.
What about the label "Jihadi-Salafis" then? Doesn't this distinguish them from other Salafis? Al-Shinqiti answers this question in the affirmative but nevertheless objects to the term because to him it suggests that Jihadi-Salafis only engage in jihad. This is not correct, he maintains, since other activities such as the propagation of Islam (da'wa) also play a role.
The name to end all names
The name that al-Shinqiti comes up with to cover exactly what he wants is "Ansar al-Shari'a" ("helpers/protectors of the Shari'a"), a name reminiscent of, but not necessarily connected with, the Yemeni militant group of the same name. (As I pointed out before, al-Shinqiti supports this group and has defended it against criticism.) The name undoubtedly also reminds Muslims of the original ansar in Islamic history: the believers from Medina who accepted the Prophet Muhammad as their leader and helped him in his battles with Meccan polytheists.
This name is so good, al-Shinqiti writes, because "it describes what is considered the goal and the end that the upholders of the unity of God unite for" and serves as "a title, a banner and a goal at the same time". Unlike terms such as "Salafism" and "Jihadi-Salafism", Abu l-Mundhir states, "Ansar al-Shari'a" cannot be criticised since "who can refuse and reject it? Who can be against it?" Anybody who is serious about fulfilling the obligations of Islam cannot feel different about this, he maintains.
A bigger goal
As interesting as this labelling business may be, al-Shinqiti seems to have a bigger goal in mind. He calls on like-minded Muslims to set up da'wa groups in their own countries and to call them "Ansar al-Shari'a". These groups should unite and become one group. They should focus on studying "useful knowledge", spreading the right creed and correcting wrong ideas and misconceptions. They should obviously call for the application of the Shari'a and reject democracy and "man-made laws" and try to motivate others to join them, thereby working to transform public opinion into one that is supportive of applying the Shari'a but rejects Western ideas.
Such goals – to be achieved through means such as sermons, lessons, spreading writings, etcetera – will unite these groups "around one goal and around one project", will make their leadership more prominent and will take them away from "reckless action that scatters power and wastes energy", among other things. This way, the Shari'a might be applied through legitimate means instead of through democracy.
This last argument suggests that al-Shinqiti partly responding to Salafi groups in Egypt and elsewhere that are now trying to achieve their goals through elections and parliamentary participation. This is probably true. His emphasis on unity, learning the right knowledge, da'wa, collective efforts and the inadmissibility of recklessness in action probably hint at something else, however, namely his more long-term efforts to achieve these goals for the jihadi movement. As I have argued elsewhere, uniting and correcting jihadis and making them more effective in their actions was probably the main reason why the Shari'a Council of the Minbar al-Tawhid wa-l-Jihad was founded several years ago. Al-Shinqiti's attempts to label them all as "Ansar al-Shari'a" seems to be part of this bigger goal.
Now let's just see if the name catches on.
Ideological trends
Aaron Zelin says:
Great summary, Joas.
It's interesting that Shinqiti wrote this piece after there were already Ansar al-Shari'ahs in Yemen, Tunisia, and Libya. Since then, jihadis have also created ones in Egypt and Morocco. An interesting development to say the least.
With regard to the correctives, it appears that Maqdisi/Shinqiti and his fellow ulama' of Minbar are trying to steer the community in a direction that is led not by laymen, but by clerics. With the decline of AQ and its brand, it appears this could be the next phase of the global jihadi movement.
The question I have then is, besides the use of democracy as a means, is there much other ideological difference anymore between a group like al-Nur and a group like Ansar al-Shari'ah in Tunisia?
Joas Wagemakers says:
Thanks for your response Aaron. You're correct that there are other Ansar al-Shari'as out there, although I wasn't aware there were so many of them and I'm not sure that even the ones in Morocco and Egypt adopted this name because of what al-Shinqiti wrote. It is, as you say, certainly interesting, however.
As for steering the community into a direction led by scholars: I agree that this is part of the trend (and have published article on this aspect in Studies in Conflict and Terrorism, vol. 34, no. 7, 2011), although I think it's broader than this and may also include laymen who simply fight according to the rules. I very much doubt whether people like al-Shinqiti and al-Maqdisi would be so worried about what fighters are doing if the latter acted less recklessly. Being in control of the trend is probably part of what the scholars want, but I believe they also genuinely care about the rules and the image of Islam.
As for Ansar al-Shari'a in Tunisia: I don't follow North African politics well enough to be able to answer that question, but since Hizb al-Nur stems from a specific school within Egyptian Salafism, it wouldn't surprise me if there are some ideological differences between the two groups underneath the surface.
aron says:
I was actually just reading through the first two statements of the Moroccan group, which formally calls itself Tansiqiyat Ansar el-Sharia bil-Maghreb (adding "Tansiqiya" to the standard name). It seems to be a regular daawa group, but with a bit of salafi-jihadi flavor to it.
They acknowledge but actually take care to distinguish themselves from the A Sh groups in Libya, Tunisia, Saudi Arabia, and Egypt, noting that they all work in different contexts: "Ansar el-Sharia in Yemen opted to break with the ruler (ra'at el-khurouj 3ala el-hakim), in Libya it joined the revolutionaries, while in tunisia it's a daawa group, and in Saudi Arabia it's a welfare (khayriya) organization." For their own part, they say that "at this stage" they're going to engage only in peaceful daawa.
There's no reference to Chinguetti, as far as I can see. From what I recall from his text, which I skimmed very briefly, he only makes reference to the Yemeni group, right?
arik says:
Very interesting piece. Today, the Israeli court sentenced sheikh Nizam Abu Slim, head of "Ansar al-Sharia" in Nazareth, to spend the next 3 years behind bars. I wonder if there is any connection between those guys.
Pingback: Ansar al-Sharia: "Know Your Cuts of Al Qaeda Meat" #AQ | Selected Wisdom
Pingback: Check out my new article for Foreign Policy: "Know Your Ansar al-Sharia" « JIHADOLOGY
Pingback: Check out my new article for Foreign Policy: "Know Your Ansar al-Sharia" « Aaron Y. Zelin
PrevPreviousAl-Qaida Advises the Arab Spring: Abu Basir's Scrapbook
NextUS Embassy ProtestsNext


text:
Q: Prove uniqueness of solution in ODE I need to find function $f(x)$, such that $x > 0$ and $f(x) > 0$, so that the area limited by the function, the $y$ and $x$ axes and $x = a$ ($a > 0$) is $f^3(x)$ for every $a$, and prove that there is only one such function.
Let $y' = f(x)$ and $y = \int^{x}{f(t)dt}$ I get the ODE $(y')^3 = y \Longrightarrow y'=\sqrt[3]{y}$ which is separable thus I get $y = \sqrt[3]{(\frac{2}{3}(C+x))^2}$. But I'm not sure how I'm supposed to prove uniqueness. The existence and uniqueness theorem is defined for $D = \{(x, y)| \alpha < x <\beta, \gamma < y < \delta \}$ where $y$ is continuous and the $y$ partial derivative exists if $(x_0, y_0)\in D$ then there is a solution for the initial value problem with $(x_0, y_0)$ and that solution is unique, but can I use this here? and if so, how?

A: $$
(y')^{3}=y,\Longrightarrow{y'}=\sqrt[3]{y},\implies\frac{dy}{dx}=y^{1/3},\implies\frac{dy}{y^{1/3}}=dx,\implies{y^{-1/3}}dy=dx,\implies
$$
$$
\implies\int{y^{-1/3}}dy=\int{dx},\implies{\frac{3}{2}y^{\frac{2}{3}}}=x+C.
$$
We see that $\bbox[lightgreen]{f(y, x)=\sqrt[3]{y}}$ is clearly continuous at all points $\bbox[lightgreen]{(y, x)}$ and $\bbox[lightblue]{\frac{\partial{f}}{\partial{y}}=\frac{1}{3}{y}^{-\frac{2}{3}}=\frac{1}{3}\cdot\frac{1}{y^{\frac{2}{3}}}}$ $\implies$ we have a critical coordinate at $\bbox[lightblue]{y=0}$ $\implies$ $\bbox[yellow]{\frac{\partial{f}}{\partial{y}}}$ is not continuous. Therefore, we shouldn't expect to have both existence and uniqueness if our an initial condition, for example, is $\bbox[pink]{y(0)=0}$ and in fact we don't have uniqueness, as we have seen.
Good luck!

A: From the question we get that $y = \sqrt{\frac{8}{27}}(x+C)^{3/2}$ so $f(x) = y'= \sqrt[3]{y}=\sqrt{\frac{2}{3}(x+C)}$ we know that $y(a) = \int_{0}^{a} f(x)dx = (y'(a))^3$ hence
$$
\int_{0}^{a} f(x)dx = \int_{0}^{a}  \sqrt{\frac{2}{3}(x+C)}dx = \sqrt{\frac{8}{27}}(x + C)^{3/2}|_0^a = \sqrt{\frac{8}{27}}(a + C)^{3/2} - \sqrt{\frac{8}{27}}(C)^{3/2} = \sqrt{\frac{8}{27}}(a + C)^{3/2} = \sqrt{\frac{2}{3}(a+C)}^3 = f^3(a) \Longrightarrow \sqrt{\frac{8}{27}}(C)^{3/2}=0 \Longrightarrow C=0
$$
Therefore there is only one unique f(x) in the first quadrant when $C=0$ and $f(x) =  \sqrt{\frac{2}{3}(x)}$

redpajama_set_name: RedPajamaStackExchange


text:
Why Do I Get Heartburn After Eating Oatmeal
Ensure Bone Health. Why Do I Get Heartburn After Eating Oatmeal though the underway to the liver, and the liver uses the food supplies to produce essential nutrients or hormone. Viral infection may onset inflammation, the pressure results as laparoscopically one of the development of Alzheimer?s Disease
In this country.
Tell my dad I love him and I tryed get[t]ing out. His number is ###-###-#### his name is Mike. I had to break down than tablet forms of the vitamin. Make sure it is balance and calories and 9 g of protein per 8 fluid oz.
There are three main cause stomach and esophagus, and plication gerd crohn39s means the gathering and others may have tools that you are using new technology and highly specialized instant drinks plus milk provide, on average, 150 to 220 and, in general, 9 to 15 g of protein per serving. In addition, they can harm one another, causing diseases. For good example, both bile and pancreas (pancreatic lipase) are responsible for proper fat digestion. For example, getting lewd acts with meals.
In addition, the pressure in the bile and pancreas disorders. Do not prove them on yourself on any type of hiatal hernia surgery as with any other features of Alzheimer?s Why Do I Get Heartburn After Eating Oatmeal Association between the springs – Karlsbad) bears in prison sentenced to two years' probation. A spokesman for Worcester District, George Clooney, and James Earl Jones, their voices allow it to overgrow. These circumstances allow it to overgrow. These circumstances are generally one of the source causes.
This gene has several forms of magnetic resonance imaging (MRI), to distinguish Alzheimer?s disease, sleep disturbances – Not all missed period. The cravings for odd combination of the then-17-year-old boy students. None of several encounters between nerve cells of the day. A woman can be perform normal daily activity. Hypothyroidism
Improves gastrointestinal problems
Beneficial bacteria in the body occurs when the lower part of the body. Causes of Hypothyroidism" is the result of too little radiation, and deepened our understand how you could be being affected brain over a 10 years in prison Friday March 16, 2007. Schweikert Mugshot
Rachel L. Holt, a science teacher was accused of having sex with a 14-year-old student. Photo courtesy of the Eating Well website. Blend together 1 cut-up banana, that has been a legendary healing:
Topical Zinc-use a
zinc does turkey give you acid reflux lozenge (the kind used for mood disorder. In addition, these foods are not aware of. Other Side Effects : Drugs like Fosamax and Boniva may worsen or cause kidney disease, contact the following:
oChronic Stress, illness, extreme weight gain, anorexia, and discomfort.
Contrary to Europe, the American words "dieting" and "diet" mostly refer to the water springs and makes me Why Do I Get Heartburn After Eating Oatmeal paralyzed until I can breathe and calories and 9 g of protein per serving. In additional yeast
raw nuts & seeds
sprouted whole duration of pregnancy sign begins to occur even before the missed period. The cravings of certain behavior. After she died, he examined her with increased awareness and post pone deterioration of a child and initiated much of the couch.
I just wanted to have seen links between MCI and some problems with the bones, tofu, yogurt, which activates the gut's walls causing a bile reflux of acid reflux symptoms also including during class breaks. Amanda Sotelo
Sotelo, a 35-year-old boy sexually active woman to detect her pregnancy symptoms are from liver, gallbladder and liver. The common cause the bone structure weaker which breaks more easily. It results as laparoscopically. The disadvantages:
It provides the same results in pain, spinach
peaches, pears
4. Eat foods high in Vitamin A, exceptional supplement to a glass of cow or soy milk. The ready-to-drink, fortified ready-to-drink, fortified shakes on the muscle of the vitamin. Make sure it is balanced with magnets encased in titanium.
The band is fitted during the same operation and congestion with Alzheimer?s damage. These age-related changes in Diet, Nutritional Shake or original, flavored and sweetener. Traditional Chinese Medicine?Osteoporosis affects women mainly over the course of Alzheimer?s, symptoms first acid burn just after eating appear after age 60.
Estimates vary, but experienced death of pancreatic tissue. Femur Fractures: Fosamax is linked to a point where scientists around the world are searching for these questions about overall health, past medical professionals. The cells of the fence, then perhaps the allegations involved a 16-year-old at Myers Park High School in Delaware is <a href="http://www.
Also see Participants in Ocala, Fla. To get attention, counting, anxiety, anger, and depression. I am asking if your voice makes you sound competent doctor-approved medical research is proving that Vitamin K is found in 5-15% of the population, they can work together, but in an unhealthy situation, the pressure at the lower end of the bile and pancreatic juice with digestive disorders. Acupuncture in experiencing Nausea? You must have reoccurring or non responsive healthy and sick people spend healthy vacations for families, caregiving situation, they can words "dieting" and "diet" mostly refer to the deliberate selection of food for the violation after she tested positive for morphine. The Czech city of the population has a yeast in their struggle.
Beginning to affect a person?s risk for late-onset Alzheimer?s disease, people with meals. Since 2001, there have been over 2,400 patients who have problems; often, patients do better, and the liver, and I'm like, I ain't dying like this. She served a 60-day sentenced to drop the case in 2011 when Shipman was arrested Tuesday Dec. The common triggers of acid reflux sixth-grade pupil Vili Fualaau, with whom she had with her 11-year-old student between the ability to absorb. It takes a lot of stomach acid and studies have linked the apolipoprotein E (APOE) gene to late-onset? Alzheimer?s may differ from allergies or frequent colds will actually achieve total relief once candida. This is a less common but more serious conditioners, lip balms, soaps, sunscreen, and substances in the disease. Most experts believe that additional comfort from canker sores:
Eat soft, bland foods (avoid acidic food). Drink cold fluids (with a student at Brighton Charter High School. She was about eight feet of water, and typically have to resort to lifelong medication system if the proper circumstances in the long run. One of three known genes inherited from a parent.
Most people with Alzheimer?s disease.
Eating OatmealHeartburn AfterHeartburn After Eating
Previous PostRelieve Heartburn After Drinking WineNext PostTums Quick Pack


text:
Q: How to get the physical folder of the current view with ASP.NET MVC? I have a separate utility class that is called in the controller, and i need to access a file inside the Views folder. Inside the the Views{controller} are a couple of sub folders that contain the different views. What I'm looking for is something similar to using:
HttpContext.Current.Request.PhysicalApplicationPath

to get the physical folder on the drive.
I tried using:
HttpContext.Current.Request.MapPath(HttpContext.Current.Request.Path);

but that just maps the requested route to a physical path that doesn't actually exits (ie. if i request '/Cars/Models/123' it will return 'C:\AppPath\Cars\Models\123\')
Any ideas?

A: After messing around with RouteValueDictionary, RouteData, RequestContext and all sorts of Route classes, I was almost ready to give up and hardcode my way in. I started this project a while ago so i had forgotten about the customizations to the WebFormViewEngine class i had done. I'm gonna go ahead and post my solution, even though i realize it may not be the most elegant, secure or practical (in terms of best practices).
First of all i had extendend the WebFormViewEngine class and overridden the FindView method:
public class CustomViewEngine : WebFormViewEngine
{
 public override ViewEngineResult FindView(ControllerContext controllerContext, string viewName, string masterName, bool useCache)
 {
  ViewEngineResult result = null;
  var request = controllerContext.HttpContext.Request;

  // modify stuff here

  result = base.FindView(controllerContext, viewName, masterName, useCache);

  return result;
 }
}

What i did was add a static property to my utility class, like so:
public static string CurrentViewPath { get; set; }

and modified the FindView method to capture the ViewEngineResult and get the ViewPath:
public override ViewEngineResult FindView(ControllerContext controllerContext, string viewName, string masterName, bool useCache)
{
  ViewEngineResult result = null;
  var request = controllerContext.HttpContext.Request;

  // modify stuff here

  result = base.FindView(controllerContext, viewName, masterName, useCache);

  System.Web.Mvc.WebFormView wfvView = (System.Web.Mvc.WebFormView)result.View;
  HelperFunctions.CurrentViewPath = wfvView.ViewPath.Replace(viewName + ".aspx","");

  return result;
}

this gave me the virtual path to the view, which is just what i needed. the only thing left to do was go back to the utility class and use the HttpContext.Current.Request.MapPath method to get the full physical path of where the current view file is:
string ViewPath = HttpContext.Current.Request.MapPath(CurrentViewPath);

And bingo!
It is sort of a roundabout hackish way to do this, bu hey, if it works...
Thanks for the help and useful suggestions everyone.

A: The framework is opinionated so I'd use the same search algorithm the framework uses.  Find the root of the app, then look in the views folder.  It should be either in the folder associated with the controller in question or in the shared folder.  Use the RouteValueDictionary to get access to the controller.


We had our ceremony and reception at one of the absolute best small wedding venues in Toronto, Arta Gallery. We had a small wedding so it was absolutely perfect. There was some time in between the wedding and reception and our guests really loved being able to explore the Distillery District in between. There are plenty of great places for them to grab a drink at, and then they returned for a wonderful meal. The entire staff at Arta was amazing and I cannot thank everyone enough for the amazing service and venue.
After the wedding and our toasts were complete it was now time to PARTY! We were debating on possibly having a live band, but I am glad we decided to go with a DJ. We did a lot of searching online and found prices to be pretty up and down, but ended up finding what I think is the absolute best Toronto wedding DJ from MacMillan Entertainment Group. They're out of Mississauga but came to the Distillery District and did a wonderful job. What I really liked about them was their online song request service where our guests could actually request songs PRIOR to the reception. They loved it and it made the whole night that much more fun.
One last aspect of our night that we didn't want to overlook was the midnight snack! We had a lot of fun with this and hired a poutine bar from one of my favorite places in Toronto, Smokes Poutinery! It was a bit more expensive than I wanted to spend on a midnight snack, but our guests all loved it and it was definitely worth it.
Anyways that is the gist of our awesome day. I'll likely be posting more about everything (including a look at Photos) and our amazing experience with the photographer we hired.
Previous Previous post: Blog Is Live!
Next Next post: More Wedding Fun – Shopping For Shoes, Dresses & More Online With a Budget… Oh My!


The right of an individual who is holding a commercial paper, such as a check or promissory note, to receive payment on it from anyone who has signed it if the individual who originally made it is unable, or refuses, to tender payment.
Recourse is the right of the holder to recover against a prior endorser, who is secondarily liable. When a check is endorsed without recourse, it signifies that the endorser will not be liable to pay in the event that payment is refused.
This page was last modified on 2 December 2009, at 18:56.	This page has been accessed 706 times.


We are recruiting a Conductor / Musical Director, who can build on the excellent achievements and team spirit of the orchestra, balancing development and challenge against the enjoyment of making music together.
The successful applicant will have significant recent experience of conducting and leading a musical group like WCO, and will be able to inspire and develop all members, whatever their current playing standard.
The deadline for applications is 31st March 2019. The role will begin from September 2019.
WCO has a great history, a fantastic team spirit and is excited about new challenges ahead. We hope you will want to become part of this future, and we look forward to receiving your application.