Below, we present the pre- and post-condition of the random-sampling statement:

${\color{ACMDarkBlue} \{  \; \langle 1,2(d\!-\!x)\!+\!4, 4(d\!-\!x)^2\!+\!22(d\!-\!x)\!+\!28 \rangle \; \}  }$

$\isample{t}{ \kw{uniform}({-1},2)}$;

${\color{ACMDarkBlue} \{  \; \langle 1, 2(d\!-\!x\!-\!t)\!+\!5,4(d\!-\!x\!-\!t)^2\!+\!26(d\!-\!x\!-\!t)\!+\!37 \rangle \; \}}$

Suppose that we want to apply the classic OST to ensuring the second-moment component is sound.

Let us use $\Phi_n'$ and $Y_n'$ to denote the over-approximations of the second moment in $\Phi_n$ and $Y_n$, respectively.

It has been shown that for such a random walk, the stopping time $T$ is not bounded but $\expe[T] < \infty$ <cit.>.

Thus, the applicable OST criterion could be <ref><ref>, which requires some $C>0$ such that $|Y'_{n+1}-Y'_n| \le C$ for all $n \in \bbZ^+$.

Consider the case where the $n$-th evaluation step of a trace $\omega$ executes the random-sampling statement.

Let $\alpha_o \defeq A_n(\omega)$.
By the definition that $Y_n(\omega) \defeq \many{ ([\alpha_o^k,\alpha_o^k])_{0 \le k \le m} } \otimes \Phi_n(\omega)$, we have[When we use a program variable $x$ in $Y_n(\omega)$, it represents $\gamma(x)$ where $\omega_n = \tuple{\gamma,\_,\_,\_}$.]

\begin{align*}
& Y_n'(\omega) \\
={} & \alpha_o^2 \!+\! 2 \cdot \alpha_o \!\cdot\! (2(d\!-\!x)\!+\!4) \!+\! (4(d\!-\!x)^2\!+\!22(d\!-\!x)\!+\!28), \\
& Y_{n+1}'(\omega) \\
={} & \alpha_o^2 \!+\! 2 \!\cdot\! \alpha_o \!\cdot\! (2(d\!-\!x\!-\!t)\!+\!5) \!+\! (4(d\!-\!x\!-\!t)^2\!+\!26(d\!-\!x\!-\!t) \!+\!37),
\end{align*}

\begin{align*}
& Y_{n+1}'(\omega)\!-\!Y_n'(\omega) \\
={} & 2 \!\cdot\! \alpha_o \!\cdot\! (-2t\!+\!1) \!+\! (-4t(2d\!-\!2x\!-\!t) \!+\! 4(d\!-\!x) \!-\!26t\! +\!9),
\end{align*}

where $t \in [{-1},2]$, $d$ is a constant, but $\alpha_o$ and $x$ are generally unbounded,
thus $|Y_{n+1}'-Y_n'|$ cannot be bounded by a constant.

§ SOUNDNESS OF BOUND INFERENCE

Valid-Ctx f ∈dom(Δ)(Γ;Q,Γ;Q') ∈Δ(f) Δ⊢{Γ;Q} (f) {Γ';Q'}  ⊢Δ
Q-Skip  Δ⊢{ Γ;Q }   { Γ;Q }
Q-Tick    Q = [c^k,c^k]_0 ≤k ≤m ⊗Q'  Δ⊢{ Γ;Q } c { Γ;Q' }
Q-Assign Γ= [E/x]Γ'
Q = [E/x]Q'  Δ⊢{ Γ;Q  } xE { Γ';Q' }
Q-Sample Γ=x ∈supp(μ_D) Γ'
Q = _x ∼μ_D[Q']  Δ⊢{  Γ;Q   } xD { Γ' ;Q' }
Q-Loop Δ⊢{ Γ∧L;Q } S_1 { Γ;Q }   Δ⊢{ Γ;Q } LS_1 { Γ∧L; Q }
Q-Cond Δ⊢{ Γ∧L; Q } S_1 {Γ';Q' }

Δ⊢{ Γ∧L; Q } S_2 {Γ';Q' }   Δ⊢{ Γ;Q } LS_1S_2 { Γ';Q' }
Q-Seq Δ⊢{Γ;Q } S_1 {Γ';Q' }

Δ⊢{ Γ';Q' } S_2 {Γ”;Q”}   Δ⊢{ Γ;Q } S_1;S_2 {Γ”;Q”}
Q-Call  i (Γ;Q_i,Γ';Q_i') ∈Δ(f)    Δ⊢{ Γ; ⊕_i Q_i } f { Γ'; ⊕_i Q_i' }
Q-Prob  Δ⊢{ Γ;Q_1 } S_1 { Γ';Q' }
Δ⊢{ Γ;Q_2 }  S_2 { Γ';Q' }

Q = P ⊕R
P = [p,p],[0,0],⋯,[0,0] ⊗Q_1
R = [1-p,1-p],[0,0],⋯,[0,0] ⊗Q_2  Δ⊢{ Γ;Q }  pS_1S_2 { Γ'; Q' }
Q-Weaken Δ⊢{ Γ_0;Q_0 } S { Γ_0';Q_0' }
Γ_0' Γ'
ΓQ ⊒Q_0
Γ_0' Q_0' ⊒Q'   Δ⊢{Γ;Q } S {Γ';Q'}
Valid-Cfg γΓ
Δ⊢{Γ;Q} S {Γ';Q'}
Δ⊢{ Γ'; Q' } K  Δ⊢{ Γ; Q } γ,S,K,α
QK-Stop  Δ⊢{ Γ; Q }
QK-Loop  Δ⊢{ Γ∧L; Q} S {Γ;Q}
Δ⊢{ Γ∧L ;Q} K  Δ⊢{ Γ;Q } LSK
QK-Seq Δ⊢{ Γ;Q} S {Γ';Q'}
Δ⊢{Γ';Q'} K  Δ⊢{ Γ;Q } SK
QK-Weaken Δ⊢{Γ';Q'} K
ΓQ ⊒Q'  Δ⊢{Γ;Q} K

Inference rules of the derivation system.

<ref> presents the inference rules of the derivation system.

Note that we prove the soundness on a more declarative system where the two rules for function calls are merged into one.

The validity of a context $\Delta$ for function specifications is then established by the validity of all specifications in $\Delta$, denoted by $\vdash \Delta$.

In addition to rules of the judgments for statements and function specifications, we also include rules for continuations and configurations that are used in the operational semantics.

A continuation $K$ is valid with a pre-condition $\{\Gamma;Q\}$, written $\Delta \vdash \{\Gamma;Q\}~K$, if $\phi_Q$ describes a bound on the moments of the accumulated cost of the computation represented by $K$ on the condition that the valuation before $K$ satisfies $\Gamma$.

Validity for configurations, written $\Delta \vdash \{\Gamma;Q\}~\tuple{\gamma,S,K,\alpha}$, is established by validity of the statement $S$ and the continuation $K$, as well as the requirement that the valuation $\gamma$ satisfies the pre-condition $\Gamma$.

Here $\phi_Q$ also describes an interval bound on the moments of the accumulated cost of the computation that continues from the configuration $\tuple{\gamma,S,K,\alpha}$.

The rule (Q-Weaken) and (QK-Weaken) are used to strengthen the pre-condition and relax the post-condition.

In terms of the bounds on moments of the accumulated cost, if the triple $\{\cdot;Q\}~S~\{\cdot;Q'\}$ is valid, then we can safely widen the intervals in the pre-condition $Q$ and narrow the intervals in the post-condition $Q'$.

To handle the judgment $\Gamma \models Q \sqsupseteq Q'$ in constraint generation,
we adapt the idea of rewrite functions <cit.>.

Intuitively, to ensure that $[L_1,U_1] \sqsupseteq_{\calP\calI} [L_2,U_2]$, i.e., $L_1 \le L_2$ and $U_2 \le U_1$, under the logical context $\Gamma$, we generate constraints indicating that there exist two polynomials $T_1,T_2$ that are always nonnegative under $\Gamma$, such that $L_1=L_2+T_1$ and $U_1=U_2-T_2$.

In our implementation, $\Gamma$ is a set of linear constraints over program variables of the form $\calE \ge 0$ , then we can represent $T_1,T_2$ by conical combinations (i.e., linear combinations with nonnegative scalars) of expressions $\calE$ in $\Gamma$.

To reduce the soundness proof to the extended OST for interval-valued bounds, we construct an annotated transition kernel from validity judgements $\vdash \Delta$ and $\Delta \vdash \{\Gamma;Q\}~S_{\mathsf{main}}~\{\Gamma';Q'\}$.

Suppose $\vdash \Delta$ and $\Delta \vdash \{\Gamma;Q\}~S_{\mathsf{main}}~\{\Gamma';Q'\}$.

An annotated program configuration has the form $\tuple{\Gamma,Q ,\gamma,S,K,\alpha}$ such that $\Delta \vdash \{\Gamma;Q\}~\tuple{\gamma,S,K,\alpha}$.

Then there exists a probability kernel $\kappa$ over annotated program configurations such that:

For all $\sigma=\tuple{\Gamma,Q,\gamma,S,K,\alpha} \in \mathrm{dom}(\kappa)$, it holds that

* $\kappa$ is the same as the evaluation relation $\mapsto$ if the annotations are omitted, i.e.,

\[
\kappa(\sigma) \bind \lambda\tuple{\_,\_,\gamma',S',K',\alpha'}. \delta(\tuple{\gamma',S',K',\alpha'}) = {\mapsto}(\tuple{\gamma,S,K,\alpha}),
\]

* $\phi_Q(\gamma) \sqsupseteq \expe_{\sigma' \sim \kappa(\sigma)} [\many{ \tuple{[(\alpha'\!-\!\alpha)^k,(\alpha'\!-\!\alpha)^k]}_{0 \le k \le m}} \otimes \phi_{Q'}(\gamma') ]$ where $\sigma'=\tuple{\_,Q',\gamma',\_,\_,\alpha'}$.

Before proving the soundness, we show that the derivation system for bound inference admits a relaxation rule.

Suppose that $\vdash \Delta$.

If $\Delta \vdash \{\Gamma;Q_1\}~S~\{\Gamma';Q_1'\}$ and $\Delta \vdash \{ \Gamma;Q_2 \}~S~\{\Gamma';Q_2'\}$, then the judgment $\Delta \vdash \{\Gamma;Q_1 \oplus Q_2 \}~S~\{\Gamma'; Q_1' \oplus Q_2' \}$ is derivable.

By nested induction on the derivation of the judgment $\Delta \vdash \{\Gamma;Q_1\}~S~\{\Gamma';Q_1'\}$, followed by inversion on $\Delta \vdash \{ \Gamma;Q_2 \}~S~\{\Gamma';Q_2'\}$.

We assume the derivations have the same shape and the same logical contexts; in practice, we can ensure this by explicitly inserting weakening positions, e.g., all the branching points, and by doing a first pass to obtain logical contexts.

* $\small\Rule{Q-Skip}{ }{ \Delta \vdash \{\Gamma;Q_1\}~\iskip~\{\Gamma;Q_1\} }$

By inversion, we have $Q_2=Q_2'$.

By (Q-Skip), we immediately have $\Delta \vdash \{\Gamma;Q_1 \oplus Q_2 \}~\iskip~\{\Gamma;Q_1 \oplus Q_2 \}$.

* $\small\Rule{Q-Tick}{ Q_1 = \many{\tuple{[c^k,c^k]}_{0 \le k \le m}} \otimes Q_1'  }{ \Delta \vdash \{\Gamma;Q_1\}~\itick{c}~\{\Gamma;Q_1'\} }$

By inversion, we have $Q_2 = \many{\tuple{[c^k,c^k]}_{0 \le k \le m}} \otimes Q_2'$.

By distributivity, we have $\many{\tuple{[c^k,c^k]}_{0 \le k \le m}} \otimes (Q_1' \oplus Q_2') = (\many{\tuple{[c^k,c^k]}_{0 \le k \le m}} \otimes Q_1') \oplus (\many{\tuple{[c^k,c^k]}_{0 \le k \le m}} \oplus  Q_2') = Q_1 \oplus Q_2$.

Then we conclude by (Q-Tick).

* $\small\Rule{Q-Assign}{ \Gamma = [E/x]\Gamma' \\ Q_1 = [E/x]Q_1' }{ \Delta \vdash \{\Gamma;Q_1\}~\iassign{x}{E}~\{\Gamma';Q_1'\} }$

By inversion, we have $Q_2 = [E/x]Q_2'$.

Then we know that $[E/x](Q_1' \oplus Q_2') = [E/x]Q_1' \oplus [E/x]Q_2' = Q_1 \oplus Q_2$.

Then we conclude by (Q-Assign).

* $\small\Rule{Q-Sample}{ \Gamma = \Forall{x \in \mathrm{supp}(\mu_D)} \Gamma' \\ Q_1 = \expe_{x \sim \mu_D}[Q_1'] }{ \Delta \vdash \{\Gamma;Q_1\}~\isample{x}{D}~\{\Gamma';Q_1'\} }$

By inversion, we have $Q_2 = \expe_{x \sim \mu_D}[Q_2']$.

By <ref>, we know that $\expe_{x \sim \mu_D}[Q_1' \oplus Q_2'] = \expe_{x \sim \mu_D}[Q_1'] \oplus \expe_{x \sim \mu_D}[Q_2'] = Q_1 \oplus Q_2$.

Then we conclude by (Q-Sample).

* $\small\Rule{Q-Call}{ \Forall{i} (\Gamma;Q_{1i},\Gamma';Q_{1i}') \in \Delta(f)  }{ \Delta \vdash \{\Gamma; \textstyle \bigoplus_i Q_{1i} \}~\iinvoke{f}~\{\Gamma'; \textstyle \bigoplus_i Q_{1i}' \} }$

By inversion, $Q_2 = \bigoplus_j Q_{2j}$ and $Q_2' = \bigoplus_j Q_{2j}'$ where $(\Gamma;Q_{2j}, \Gamma';Q_{2j}') \in \Delta(f)$ for each $j$.

Then by (Q-Call), we have
$\Delta \vdash \{ \Gamma; \bigoplus_i Q_{1i} \oplus \bigoplus_j Q_{2j} \} ~ \iinvoke{f} ~ \{ \Gamma'; \bigoplus_i Q_{1i}' \oplus \bigoplus_j Q_{2j}' \}$.

* $\small\Rule{Q-Prob}{ \Delta \vdash \{\Gamma;Q_{11}\}~S_1~\{\Gamma';Q_1'\} \\ \Delta \vdash \{\Gamma;Q_{12}\}~S_2~\{\Gamma';Q_1'\} \\ Q_1 = P_1 \oplus R_1 \\ P_1 = \tuple{[p,p],[0,0],\cdots,[0,0]} \otimes Q_{11} \\ R_1 = \tuple{[1-p,1-p],[0,0],\cdots,[0,0]} \otimes Q_{12} }{ \Delta \vdash \{\Gamma;Q_1\}~\iprob{p}{S_1}{S_2}~\{\Gamma';Q_1'\} }$

By inversion, we know that $Q_2 = P_2 \oplus R_2$ for some $Q_{21},Q_{22}$ such that
$\Delta \vdash \{ \Gamma; Q_{21} \}~S_1~\{\Gamma';Q_{2}' \}$,
$\Delta \vdash \{ \Gamma; Q_{22} \}~S_2~\{\Gamma';Q_2' \}$,
$P_2 = \tuple{[p,p],[0,0],\cdots,[0,0]} \otimes Q_{21}$,
and $R_2 = \tuple{[1-p,1-p],[0,0],\cdots,[0,0]} \otimes Q_{22}$.

By induction hypothesis, we have $\Delta \vdash \{\Gamma;Q_{11} \oplus Q_{21} \}~S_1~\{\Gamma'; Q_1' \oplus Q_2' \}$ and $\Delta \vdash \{\Gamma; Q_{12} \oplus Q_{22} \}~S_2~\{\Gamma'; Q_1' \oplus Q_2' \}$.

\begin{align*}
& \tuple{[p,p],\cdots,[0,0]} \otimes (Q_{11} \oplus Q_{21}) \\
={} & (\tuple{[p,p],\cdots,[0,0]} \otimes Q_{11}) \oplus (\tuple{[p,p],\cdots,[0,0]} \oplus Q_{21}) \\
={} & P_1 \oplus P_2, \\
& \tuple{[1-p,1-p],\cdots,[0,0]} \otimes (Q_{12} \oplus Q_{22}) \\
={} & (\tuple{[1\!-\!p,\!1\!-\!p],\!\cdots\!,\![0,0]} \!\otimes\! Q_{12}) \!\oplus\! (\tuple{[1\!-\!p,\!1\!-\!p],\!\cdots\!,\![0,0]} \!\otimes\! Q_{22}) \\
={} & R_1 \oplus R_2, \\
& (P_1 \oplus P_2) \oplus (R_1 \oplus R_2) \\
={} & (P_1 \oplus R_1) \oplus (P_2 \oplus R_2) \\
={} & Q_1 \oplus Q_2.
\end{align*}

Thus we conclude by (Q-Prob).

* $\small\Rule{Q-Cond}{ \Delta \vdash \{\Gamma \wedge L; Q_1\}~S_1~\{\Gamma';Q_1'\} \\ \Delta \vdash \{\Gamma \wedge \neg L;Q_1\} ~S_2~\{\Gamma';Q_1'\}  }{ \Delta \vdash \{\Gamma;Q_1\}~\icond{L}{S_1}{S_2}~\{\Gamma';Q_1'\} }$

By inversion, we have
$\Delta \vdash \{ \Gamma \wedge L; Q_2 \}~S_1~\{\Gamma';Q_2'\}$, and
$\Delta \vdash \{ \Gamma \wedge \neg L; Q_2\} ~ S_2 ~ \{\Gamma'; Q_2'\}$.

By induction hypothesis, we have $\Delta \vdash \{\Gamma \wedge L; Q_1 \oplus Q_2 \}~S_1~\{\Gamma';Q_1' \oplus Q_2'\}$ and $\Delta \vdash \{\Gamma \wedge \neg L; Q_1 \oplus Q_2 \}~S_2~\{\Gamma'; Q_1' \oplus Q_2' \}$.

Then we conclude by (Q-Cond).

* $\small\Rule{Q-Loop}{ \Delta \vdash \{\Gamma \wedge L;Q_1\}~S~\{\Gamma;Q_1\} }{ \Delta \vdash \{\Gamma;Q_1\}~\iloop{L}{S}~\{\Gamma \wedge \neg L; Q_1\} }$

By inversion, we have $\Delta \vdash \{ \Gamma \wedge L; Q_2 \} ~ S ~ \{\Gamma; Q_2\}$.

By induction hypothesis, we have $\Delta \vdash \{\Gamma \wedge L; Q_1 \oplus Q_2 \}~S~\{\Gamma; Q_1 \oplus Q_2  \}$.

Then we conclude by (Q-Loop).

* $\small\Rule{Q-Seq}{ \Delta \vdash \{\Gamma;Q_1\}~S_1~\{\Gamma'';Q_1''\} \\ \Delta \vdash \{\Gamma'';Q_1''\}~S_2~\{\Gamma';Q_1'\} }{ \Delta \vdash \{\Gamma;Q_1\}~S_1;S_2~\{\Gamma';Q_1'\} }$

By inversion, there exists $Q_2''$ such that
$\Delta \vdash \{ \Gamma; Q_2 \}~S_1 ~ \{ \Gamma''; Q_2'' \}$, and
$\Delta \vdash \{\Gamma'';Q_2'' \} ~S_2 ~ \{ \Gamma'; Q_2' \}$.

By induction hypothesis, we have $\Delta \vdash \{\Gamma; Q_1 \oplus Q_2 \}~S_1~\{\Gamma''; Q_1'' \oplus Q_2'' \}$ and $\Delta \vdash \{\Gamma''; Q_1'' \oplus Q_2'' \}~S_2~\{\Gamma'; Q_1' \oplus Q_2' \}$.

Then we conclude by (Q-Seq).

* $\small\Rule{Q-Weaken}{ \Delta \vdash \{\Gamma_0;Q_0\}~S~\{\Gamma_0';Q_0'\} \\ \Gamma \models \Gamma_0 \\ \Gamma_0' \models \Gamma' \\ \Gamma \models Q_1 \sqsupseteq Q_0 \\ \Gamma_0' \models Q_0' \sqsupseteq Q_1' }{ \Delta \vdash \{\Gamma;Q_1\}~S~\{\Gamma';Q_1'\} }$

By inversion, there exist $Q_3,Q_3'$ such that
$\Gamma \models Q_2 \sqsupseteq Q_3$, $\Gamma_0' \models Q_3' \sqsupseteq Q_2'$, and
$\Delta \vdash \{ \Gamma_0; Q_3 \} ~S~ \{ \Gamma_0'; Q_3' \}$.

By induction hypothesis, we have $\Delta \vdash \{\Gamma_0; Q_0 \oplus Q_3 \}~S~\{\Gamma_0';Q_0' \oplus Q_3' \}$.

To apply (Q-Weaken), we need to show that $\Gamma \models Q_1 \oplus Q_2  \sqsupseteq Q_0 \oplus Q_3$ and $\Gamma_0' \models Q_0' \oplus Q_3' \sqsupseteq  Q_1' \oplus Q_2'$.

Then appeal to <ref>.

Now we can construct the annotated transition kernel to reduce the soundness proof to OST.

Let $\nu \defeq {\mapsto}(\tuple{\gamma,S,K,\alpha})$.

By inversion on $\Delta \vdash \{\Gamma;Q\}~\tuple{\gamma,S,K,\alpha}$, we know that $\gamma \models \Gamma$, $\Delta \vdash \{\Gamma;Q\}~S~\{\Gamma';Q'\}$, and $\Delta \vdash \{\Gamma';Q'\}~K$ for some $\Gamma',Q'$.

We construct a probability measure $\mu$ as $\kappa(\tuple{\Gamma,Q,\gamma,S,K,\alpha})$ by induction on the derivation of $\Delta \vdash \{\Gamma;Q\}~S~\{\Gamma';Q'\}$.

* $\small\Rule{Q-Skip}{ }{ \Delta \vdash \{ \Gamma;Q \}~\iskip~\{\Gamma;Q\} }$

By induction on the derivation of $\Delta \vdash \{\Gamma;Q\}~K$.

* $\small\Rule{QK-Stop}{ }{ \Delta \vdash \{ \Gamma;Q \}~\kstop }$

We have $\nu = \delta(\tuple{\gamma,\iskip,\kstop,\alpha})$.

Then we set $\mu = \delta(\tuple{\Gamma,Q,\gamma,\iskip,\kstop,\alpha })$.

It is clear that $\phi_Q(\gamma) = \aone \otimes \phi_Q(\gamma)$.

* $\small\Rule{QK-Loop}{ \Delta \vdash \{\Gamma \wedge L; Q\}~S~\{\Gamma;Q\} \\ \Delta \vdash \{\Gamma \wedge \neg L; Q\}~K }{ \Delta \vdash \{\Gamma;Q\}~\kloop{L}{S}{K} }$

Let $b \in \{\bot,\top\}$ be such that $\gamma \vdash L \Downarrow b$.

If $b = \top$, then $\nu = \delta(\tuple{\gamma,S,\kloop{L}{S}{K},\alpha})$.

We set $\mu = \delta(\tuple{ \Gamma \wedge L,Q,\gamma,S,\kloop{L}{S}{K},\alpha })$.

In this case, we know that $\gamma \models \Gamma \wedge L$.

By the premise, we know that $\Delta \vdash \{\Gamma\wedge L;Q\}~S~\{\Gamma;Q\}$.

It then remains to show that $\Delta \vdash \{ \Gamma;Q\}~\kloop{L}{S}{K}$.

By (QK-Loop), it suffices to show that $\Delta \vdash \{\Gamma \wedge L; Q\}~S~\{\Gamma;Q\}$ and $\Delta \vdash \{\Gamma \wedge \neg L; Q\}~K$.

Then appeal to the premise.

If $b = \bot$, then $\mu = \delta(\tuple{\gamma,\iskip,K,\alpha})$.

We set $\mu = \delta(\tuple{\Gamma \wedge \neg L, Q, \gamma,\iskip,K,\alpha})$.

In this case, we know that $\gamma \models \Gamma \wedge \neg L$.

By (Q-Skip), we have $\Delta \vdash \{\Gamma \wedge \neg L;Q\}~\iskip~\{\Gamma \wedge \neg L; Q\}$.

It then remains to show that $\Delta \vdash \{\Gamma \wedge \neg L; Q\}~K$.

Then appeal to the premise.

In both cases, $\gamma$ and $Q$ do not change, thus we conclude that $\phi_Q(\gamma) = \aone \otimes \phi_Q(\gamma)$.

* $\small\Rule{QK-Seq}{ \Delta \vdash \{\Gamma;Q\}~S~\{\Gamma';Q'\} \\ \Delta \vdash \{\Gamma';Q'\}~K }{ \Delta \vdash \{\Gamma;Q\}~\kseq{S}{K} }$

We have $\nu = \delta(\tuple{\gamma,S,K,\alpha})$.

Then we set $\mu = \delta(\tuple{\Gamma,Q,\gamma,S,K,\alpha})$.

By the premise, we know that $\Delta \vdash \{\Gamma;Q\}~S~\{\Gamma';Q'\}$ and $\Delta \vdash \{\Gamma';Q'\}~K$.

Because $\gamma$ and $Q$ do not change, we conclude that $\phi_Q(\gamma) = \aone \otimes \phi_Q(\gamma)$.

* $\small\Rule{QK-Weaken}{ \Delta \vdash \{\Gamma';Q'\}~K \\ \Gamma \models \Gamma' \\ \Gamma \models Q \sqsupseteq Q' }{ \Delta \vdash \{\Gamma;Q\}~K }$

Because $\gamma \models \Gamma$ and $\Gamma \models \Gamma'$, we know that $\gamma \models \Gamma'$.

Let $\mu'$ be obtained from the induction hypothesis on $\Delta \vdash \{\Gamma';Q'\}~K$.

Then $\phi_{Q'}(\gamma) \sqsupseteq \expe_{\sigma' \sim \mu'}[\many{\tuple{[(\alpha'-\alpha)^k,(\alpha'-\alpha)^k]}_{0 \le k \le m}} \otimes \phi_{Q''}(\gamma')]$, where $\sigma'=\tuple{\_,Q'',\gamma',\_,\_,\alpha'}$.

We set $\mu = \mu'$.

Because $\Gamma \models Q \sqsupseteq Q'$ and $\gamma \models \Gamma$, we conclude that $\phi_Q(\gamma) \sqsupseteq \phi_{Q'}(\gamma)$.

* $\small\Rule{Q-Tick}{ Q = \many{\tuple{[c^k,c^k]}_{0 \le k \le m}} \otimes Q' }{ \Delta \vdash \{\Gamma;Q\}~\itick{c}~\{\Gamma;Q'\} }$

We have $\nu = \delta(\tuple{\gamma,\iskip,K,\alpha+c})$.

Then we set $\mu = \delta(\tuple{\Gamma,Q',\gamma,\iskip,K,\alpha+c})$.

By (Q-Skip), we have $\Delta \vdash \{\Gamma;Q'\}~\iskip~\{\Gamma;Q'\}$.

Then by the assumption, we have $\Delta \vdash \{\Gamma;Q'\}~K$.

It remains to show that $\phi_Q(\gamma) \sqsupseteq \many{\tuple{[c^k,c^k]}_{0 \le k \le m}} \otimes \phi_{Q'}(\gamma)$.

Indeed, we have $\phi_Q(\gamma) = \many{\tuple{[c^k,c^k]}_{0 \le k \le m}} \otimes \phi_{Q'}(\gamma)$ by the premise.

* $\small\Rule{Q-Assign}{ \Gamma = [E/x]\Gamma' \\ Q = [E/x]Q' }{ \Delta \vdash \{\Gamma;Q\}~\iassign{x}{E}~\{\Gamma';Q'\} }$

Let $r \in \bbR$ be such that $\gamma \vdash E \Downarrow r$.

We have $\nu = \delta(\tuple{\gamma[x \mapsto r],\iskip,K,\alpha})$.

Then we set $\mu = \delta(\tuple{\Gamma',Q',\gamma[x \mapsto r],\iskip,K,\alpha})$.

Because $\gamma \vdash \Gamma$, i.e., $\gamma \vdash [E/x]\Gamma'$, we know that $\gamma[x \mapsto r] \vdash \Gamma'$.

By (Q-Skip), we have $\Delta \vdash \{\Gamma';Q'\}~\iskip~\{\Gamma';Q'\}$.

Then by the assumption, we have $\Delta \vdash \{\Gamma';Q'\}~K$.

It remains to show that $\phi_Q(\gamma) = \aone \otimes \phi_{Q'}(\gamma[x \mapsto r])$.

By the premise, we have $Q = [E/x]Q'$, thus $\phi_Q(\gamma) = \phi_{[E/x]Q'}(\gamma) = \phi_{Q'}(\gamma[x \mapsto r])$.

* $\small\Rule{Q-Sample}{ \Gamma = \Forall{x \in \mathrm{supp}(\mu_D)} \Gamma' \\ Q = \expe_{x \sim \mu_D}[Q'] }{ \Delta \vdash \{\Gamma;Q\}~\isample{x}{D}~\{\Gamma';Q'\} }$

We have $\nu = \mu_D \bind \lambda r. \delta(\tuple{\gamma[x \mapsto r],\iskip,K,\alpha})$.

Then we set $\mu = \mu_D \bind \lambda r. \delta(\tuple{\Gamma',Q',\gamma[x \mapsto r],\iskip,K,\alpha})$.

For all $r \in \mathrm{supp}(\mu_D)$, because $\gamma \models \Forall{x \in \mathrm{supp}(\mu_D)} \Gamma'$, we know that $\gamma[x \mapsto r] \models \Gamma'$.

By (Q-Skip), we have $\Delta \vdash \{\Gamma';Q'\}~\iskip~\{\Gamma';Q'\}$.

Then by the assumption, we have $\Delta \vdash \{\Gamma';Q'\}~K$.

It remains to show that $\phi_Q(\gamma) \sqsupseteq \expe_{r \sim \mu_D}[\aone \otimes \phi_{Q'}(\gamma[x \mapsto r])]$.

Indeed, because $Q = \expe_{x \sim \mu_D}[Q']$, we know that $\phi_Q(\gamma) = \phi_{\expe_{x \sim \mu_D}[Q']}(\gamma) = \expe_{r \sim \mu_D}[\phi_{Q'}(\gamma[x \mapsto r])]$.

* $\small\Rule{Q-Call}{ \Forall{i} (\Gamma;Q_i,\Gamma';Q_i') \in \Delta(f) }{ \Delta \vdash \{\Gamma; \textstyle \bigoplus_i Q_i \}~\iinvoke{f}~\{\Gamma'; \textstyle \bigoplus_i Q_i' \} }$

We have $\nu = \delta(\tuple{\gamma,\scrD(f),K,\alpha})$.

Then we set $\mu = \delta(\tuple{\Gamma, \bigoplus_i Q_i ,\gamma,\scrD(f),K,\alpha})$.

By the premise, we know that $\Delta \vdash \{\Gamma;Q_i\}~\scrD(f)~\{\Gamma';Q_i'\}$ for each $i$.

By <ref> and simple induction, we know that $\Delta \vdash \{\Gamma; \bigoplus_i Q_i \}~\scrD(f)~\{\Gamma'; \bigoplus_i Q_i' \} $.

Because $\gamma$ and $\bigoplus_i Q_i$ do not change, we conclude that $\phi_{\bigoplus_i Q_i}(\gamma) = \aone \otimes \phi_{\bigoplus_i Q_i}(\gamma)$.

* $\small\Rule{Q-Prob}{ \Delta \vdash \{\Gamma;Q_1\}~S_1~\{\Gamma';Q'\} \\ \Delta \vdash \{\Gamma;Q_2\}~S_2~\{\Gamma';Q'\} \\ Q = P \oplus R \\ P = \tuple{[p,p],[0,0],\cdots,[0,0]} \otimes Q_1 \\ R = \tuple{[1-p,1-p],[0,0],\cdots,[0,0]} \otimes Q_2 }{ \Delta \vdash \{\Gamma;Q\}~\iprob{p}{S_1}{S_2} ~\{\Gamma';Q'\} }$

We have $\nu = p \cdot \delta(\tuple{\gamma,S_1,K,\alpha}) + (1-p) \cdot \delta(\tuple{\gamma,S_2,K,\alpha})$.

Then we set $\mu = p \cdot \delta(\tuple{\Gamma,Q_1,\gamma,S_1,K,\alpha} + (1-p) \cdot \delta(\tuple{\Gamma,Q_2,\gamma,S_2,K,\alpha})$.

From the assumption and the premise, we know that $\gamma \models \Gamma$, $\Delta \vdash \{\Gamma';Q'\}~K$, and $\Delta \vdash \{\Gamma;Q_1\}~S_1~\{\Gamma';Q'\}$, $\Delta \vdash \{\Gamma;Q_2\}~S_2~\{\Gamma';Q'\}$.

It remains to show that $\phi_Q(\gamma)_k \ge_{\calI} (p \cdot \phi_{Q_1}(\gamma)_k) +_\calI ((1-p) \cdot \phi_{Q_2}(\gamma)_k)$, where the scalar product $p \cdot [a,b] \defeq [pa,pb]$ for $p \ge 0$.

On the other hand, from the premise, we have $Q_k = P_k +_{\calP\calI} R_k$ and $P_k = (([p,p],\cdots,[0,0]) \otimes Q_1)_k = \binom{k}{0} \times_{\calP\calI} ([p,p] \cdot_{\calP\calI} (Q_1)_k) = p \cdot (Q_1)_k$, as well as $R_k = (1-p) \cdot (Q_2)_k$.

Therefore, we have $\phi_Q(\gamma)_k = \phi_{\many{\tuple{P_k +_{\calP\calI} R_k}_{0 \le k \le m}}}(\gamma)_k = p \cdot \phi_{Q_1}(\gamma)_k +_\calI (1-p) \cdot \phi_{Q_2}(\gamma)_k$.

* $\small\Rule{Q-Cond}{ \Delta \vdash \{\Gamma \wedge L;Q\}~S_1~\{\Gamma';Q'\} \\ \Delta \vdash \{\Gamma \wedge \neg L; Q\}~S_2~\{\Gamma';Q'\} }{ \Delta \vdash \{\Gamma;Q\}~\icond{L}{S_1}{S_2}~\{\Gamma';Q'\} }$

Let $b \in \{\top,\bot\}$ be such that $\gamma \vdash L \Downarrow b$.

If $b = \top$, then $\nu = \delta(\tuple{\gamma,S_1,K,\alpha})$.

We set $\mu = \delta(\tuple{\Gamma \wedge L,Q,\gamma,S_1,K,\alpha})$.

In this case, we know that $\gamma \models \Gamma \wedge L$.

By the premise and the assumption, we know that $\Delta \vdash \{\Gamma \wedge L; Q\}~S_1~\{\Gamma';Q'\}$ and $\Delta \vdash \{\Gamma';Q'\}~K$.

If $b = \bot$, then $\nu = \delta(\tuple{\gamma,S_2,K,\alpha})$.

We set $\mu = \delta(\tuple{\Gamma \wedge \neg L,Q,\gamma,S_2,K,\alpha})$.

In this case, we know that $\gamma \models \Gamma \wedge \neg L$.

By the premise and the assumption, we know that $\Delta \vdash \{\Gamma \wedge \neg L; Q\}~S_2~\{\Gamma';Q'\}$ and $\Delta \vdash \{\Gamma';Q'\}~K$.

In both cases, $\gamma$ and $Q$ do not change, thus we conclude that $\phi_Q(\gamma) = \aone \otimes \phi_Q(\gamma)$.

* $\small\Rule{Q-Loop}{ \Delta \vdash \{\Gamma \wedge L;Q\}~S~\{\Gamma;Q\} }{ \Delta \vdash \{\Gamma;Q\}~\iloop{L}{S_1}~\{\Gamma \wedge \neg L;Q \} }$

We have $\nu = \delta(\tuple{\gamma,\iskip,\kloop{L}{S}{K},\alpha})$.

Then we set $\mu = \delta(\tuple{\Gamma,Q,\gamma,\iskip,\kloop{L}{S}{K},\alpha})$.

By (Q-Skip), we have $\Delta \vdash \{\Gamma;Q\}~\iskip~\{\Gamma;Q\}$.

Then by the assumption $\Delta \vdash \{\Gamma \wedge \neg L;Q\}~K$ and the premise, we know that $\Delta \vdash \{\Gamma;Q\}~\kloop{L}{S}{K}$ by (QK-Loop).

Because $\gamma$ and $Q$ do not change, we conclude that $\phi_Q(\gamma) = \aone \otimes \phi_Q(\gamma)$.

* $\small\Rule{Q-Seq}{ \Delta \vdash \{\Gamma;Q\}~S_1~\{\Gamma';Q'\} \\ \Delta \vdash \{\Gamma';Q'\}~S_2~\{\Gamma'';Q''\} }{ \Delta \vdash \{\Gamma;Q\}~S_1;S_2~\{\Gamma'';Q''\} }$

We have $\nu = \delta(\tuple{\gamma,S_1,\kseq{S_2}{K},\alpha})$.

Then we set $\mu = \delta(\tuple{\Gamma,Q,\gamma,S_1,\kseq{S_2}{K},\alpha})$.

By the first premise, we have $\Delta \vdash \{\Gamma;Q\}~S_1~\{\Gamma';Q'\}$.

By the assumption $\Delta \vdash \{\Gamma'';Q''\}~K$ and the second premise, we know that $\Delta \vdash \{\Gamma';Q'\}~\kseq{S_2}{K}$ by (QK-Seq).

Because $\gamma$ and $Q$ do not change, we conclude that $\phi_Q(\gamma) = \aone \otimes \phi_Q(\gamma)$.

* $\small\Rule{Q-Weaken}{ \Delta \vdash \{\Gamma_0;Q_0\}~S~\{\Gamma_0';Q_0'\} \\ \Gamma \models \Gamma_0 \\ \Gamma_0' \models \Gamma' \\ \Gamma \models Q \sqsupseteq Q_0 \\ \Gamma_0' \models Q_0' \sqsupseteq Q' }{ \Delta \vdash \{\Gamma;Q\}~S~\{\Gamma';Q'\} }$

By $\gamma \models \Gamma$ and $\Gamma \models \Gamma_0$, we know that $\gamma \models \Gamma_0$.

By the assumption $\Delta \vdash \{\Gamma';Q'\}~K$ and the premise $\Gamma_0' \models \Gamma'$, $\Gamma_0' \models Q_0' \sqsupseteq Q'$, we derive $\Delta \vdash \{\Gamma_0';Q_0'\}~K$ by (QK-Weaken).

Thus let $\mu_0$ be obtained by the induction hypothesis on $\Delta \vdash \{\Gamma_0;Q_0\}~S~\{\Gamma_0';Q_0'\}$.

Then $\phi_{Q_0}(\gamma) \sqsupseteq \expe_{\sigma' \sim \mu_0}[\many{\tuple{[(\alpha'-\alpha)^k,(\alpha'-\alpha)^k]}_{0 \le k \le m}} \otimes \phi_{Q''}(\gamma')]$, where $\sigma' = \tuple{\_,Q'',\gamma',\_,\_,\alpha'}$.

We set $\mu = \mu_0$.

By the premise $\Gamma \models Q \sqsupseteq Q_0$ and $\gamma \models \Gamma$, we conclude that $\phi_{Q}(\gamma) \sqsupseteq \phi_{Q_0}(\gamma)$.

Therefore, we can use the annotated kernel $\kappa$ above to re-construct the trace-based moment semantics in <ref>.

Then we can define the potential function on annotated program configurations as $\phi(\sigma) \defeq \phi_Q(\gamma)$ where $\sigma=\tuple{\_,Q,\gamma,\_,\_,\_}$.

The next step is to apply the extended OST for interval bounds (<ref>).

Recall that the theorem requires that for some $\ell \in \bbN$ and $C \ge 0$, $\norm{Y_n}_\infty \le C \cdot (n+1)^{\ell}$ almost surely for all $n \in \bbZ^+$.

One sufficient condition for the requirement is to assume the bounded-update property, i.e., every (deterministic or probabilistic) assignment to a program variable updates the variable with a bounded change.

As observed by <cit.>, bounded updates are common in practice.

We formulate the idea as follows.

If there exists $C_0 \ge 0$ such that for all $n \in \bbZ^+$ and $x \in \mathsf{VID}$, it holds that $\prob[\abs{\gamma_{n+1}(x)- \gamma_n(x) } \le C_0] = 1$ where $\omega$ is an infinite trace, $\omega_n = \tuple{\gamma_n,\_,\_,\_}$, and $\omega_{n+1} = \tuple{\gamma_{n+1},\_,\_,\_}$,

then there exists $C \ge 0$ such that  for all $n \in \bbZ^+$, $\norm{Y_n}_\infty \le C \cdot (n+1)^{md}$ almost surely.

Let $C_1 \ge 0$ be such that for all $\itick{c}$ statements in the program, $|c| \le C_1$.

Then for all $\omega$, if $\omega_n = \tuple{\_,\_,\_,\alpha_n}$, then $|\alpha_n| \le n \cdot C_1$.

On the other hand, we know that $\prob[|\gamma_n(x) - \gamma_0(x)| \le C_0 \cdot n] = 1$ for any variable $x$.

As we assume all the program variables are initialized to zero, we know that $\prob[|\gamma_n(x)| \le C_0 \cdot n] = 1$.

From the construction in the proof of <ref>, we know that all the templates used to define the interval-valued potential function should have almost surely bounded coefficients.

Let $C_2 \ge 0$ be such a bound.

Also, the $k$-th component in a template is a polynomial in $\bbR_{kd}[\mathsf{VID}]$.

Therefore, $\Phi_n(\omega) = \phi(\omega_n) = \phi_{Q_n}(\gamma_n)$, and

\[
|\phi_{Q_n}(\gamma_n)_k| \le \sum_{i=0}^{kd} C_2 \cdot |\mathsf{VID}|^{i} \cdot |C_0 \cdot n|^i \le C_3 \cdot (n+1)^{kd}, \textrm{a.s.},
\]

for some sufficiently large constant $C_3$.

\begin{align*}
& |(Y_n)_k| = |(A_n \otimes \Phi_n)_k| \\
={} & |\mathop{{\sum}_\calI}_{i=0}^k \binom{k}{i} \times_\calI ((A_n)_i \cdot_\calI (\Phi_n)_{k-i})| \\
{}\le{} & \sum_{i=0}^k \binom{k}{i} \cdot (n \cdot C_1)^i \cdot (C_3 \cdot (n+1))^{(k-i)d} \\
{}\le{} & C_4 \cdot (n+1)^{kd}, \textrm{a.s.},
\end{align*}

for some sufficiently large constant $C_4$.

Therefore $\norm{Y_n}_\infty \le C_5 \cdot (n+1)^{md}$, a.s., for some sufficiently large constant $C_5$.

Now we prove the soundness of bound inference.

Suppose $\Delta \vdash \{\Gamma;Q\}~S_{\mathsf{main}}~\{\Gamma';\aone\}$ and $\vdash \Delta$.

Then $\expe[A_T] \aord \phi_Q(\lambda\_.0)$, i.e., the moments $\expe[A_T]$ of the accumulated cost upon program termination are bounded by intervals in $\phi_Q(\lambda\_.0)$ where $Q$ is the quantitative context and $\lambda\_.0$ is the initial valuation, if both of the following properties hold:

* $\expe[T^{md}] < \infty$, and

* there exists $C_0 \ge 0$ such that for all $n \in \bbZ^+$ and $x \in \mathsf{VID}$, it holds almost surely that $|\gamma_{n+1}(x) - \gamma_n(x)| \le C_0$ where $\tuple{\gamma_n,\_,\_,\_} = \omega_n$ and $\tuple{\gamma_{n+1},\_,\_,\_} = \omega_{n+1}$ of an infinite trace $\omega$.

By <ref>, there exists $C \ge 0$ such that $\norm{Y_n}_\infty \le C \cdot (n+1)^{md}$ almost surely for all $n \in \bbZ^+$.

By the assumption, we also know that $\expe[T^{md}] < \infty$.

Thus by <ref>, we conclude that $\expe[Y_T] \aord \expe[Y_0]$, i.e., $\expe[A_T] \aord \expe[\Phi_0] = \phi_Q(\lambda\_.0)$.

§ TERMINATION ANALYSIS

In this section, we develop a technique to reason about upper bounds on higher moments $\expe[T^m]$ of the stopping time $T$.

We adapt the idea of expected-potential functions, but rely on a simpler convergence proof.

In this section, we assume $\calR = ([0,\infty], {\le},{+},{\cdot},0,1)$ to be a partially ordered semiring on extended nonnegative real numbers.

A map $\psi : \Sigma \to \calM_\calR^{(m)}$ is said to be an expected-potential function for upper bounds on stopping time if

* $\psi(\sigma)_0 = 1$ for all $\sigma \in \Sigma$,

* $\psi(\sigma) = \aone$ if $\sigma = \tuple{\_,\iskip,\kstop,\_}$, and

* $\psi(\sigma) \sqsupseteq \expe_{\sigma' \sim {\mapsto}(\sigma)}[\tuple{1,1,\cdots,1} \otimes \psi(\sigma')]$ for all non-terminating configuration $\sigma \in \Sigma$.

Intuitively, $\psi(\sigma)$ is an upper bound on the moments of the evaluation steps upon termination for the computation that continues from the configuration $\sigma$.

We define $A_n$ and $\Psi_n$ where $n \in \bbZ^+$ to be random variables on the probability space $(\Omega,\calF,\prob)$ of the trace semantics as
$A_n(\omega) \defeq \many{\tuple{n^k}_{0 \le k \le m}}$ and $\Psi_n(\omega) \defeq \psi(\omega_n)$.

Then we define $A_T(\omega) \defeq A_{T(\omega)}(\omega)$.

Note that $A_T = \many{\tuple{T^k}_{0 \le k \le m}}$.

We now show that a valid potential function for stopping time always gives a sound upper bound.

$\expe[A_T] \aord \expe[\Psi_0]$.

Let $C_n(\omega) \defeq \tuple{1,1,\cdots,1}$ if $n < T(\omega)$, otherwise $C_n(\omega) \defeq \tuple{1,0,\cdots,0}$.

Then $A_T = \bigotimes_{i=0}^\infty C_i$.

By <ref>, we know that $\expe[A_T] = \lim_{n \to \infty} \expe[\bigotimes_{i=0}^n C_i]$.

Thus it suffices to show that for all $n \in \bbZ^+$, $\expe[\bigotimes_{i=0}^n C_i] \aord \expe[\Psi_0]$.

Observe that $\{C_n\}_{n \in \bbZ^+}$ is adapted to $\{\calF_n\}_{n \in \bbZ^+}$, because the event $\{ T \le n\}$ is $\calF_n$-measurable.

Then we have

\begin{align*}
& \expe[\bigotimes\nolimits_{i=0}^n C_i \otimes \Psi_{n+1} \mid \calF_n] \\
={} & \bigotimes\nolimits_{i=0}^{n-1} C_i \otimes \expe[C_n \otimes \Psi_{n+1} \mid \calF_n], a.s., \\
{}\aord{} & \bigotimes\nolimits_{i=0}^{n-1} C_i \otimes \Psi_n.
\end{align*}

Therefore, $\expe[\bigotimes_{i=0}^n C_i \otimes \Psi_{n+1}] \aord \expe[\Psi_0]$ for all $n \in \bbZ^+$ by a simple induction.

Because $\Psi_{n+1} \sqsupseteq \aone$, we conclude that

\[
\expe[\bigotimes\nolimits_{i=0}^n C_i] \aord \expe[\bigotimes\nolimits_{i=0}^n C_i \otimes \Psi_{n+1}] \aord \expe[\Psi_0].
\]

§ EXPERIMENTAL EVALUATION

<ref> and <ref> are the complete versions of the statistics in <ref> and the plots in <ref>, respectively.

Upper bound of the tail probability $\prob[T \ge d]$ as a function of $d$, with comparison to <cit.>. Each gray line is the minimum of tail bounds obtained from the raw moments of degree up to four inferred by <cit.>. Green lines and red lines are the tail bounds given by 2nd and 4th central moments inferred by our tool, respectively.

<ref> compares our tool with <cit.> on their benchmarks for upper bounds on the first moments of runtimes.

The programs (1-1) and (1-2) are coupon-collector problems with a total of two and four coupons, respectively.
The other five are variants of random walks.
The first three are one-dimensional random walks: (2-1) is integer-valued, (2-2) is real-valued with continuous sampling, and (2-3) exhibits adversarial nondeterminism.
The programs (2-4) and (2-5) are two-dimensional random walks.

In the parentheses after the bounds, we record the degree of polynomials for the templates and the running time of the analysis.

All analyses completed is less than half a second, and our tool can derive better bounds than the compared tool <cit.>.

Upper bounds of the expectations of runtimes, with comparison to <cit.>.

program     pre-condition     upper bound by our tool     upper bound by <cit.>
(1-1)     $\top$     $13$ (deg 2, 0.106s)     $13$ (deg 1, 0.011s)

(1-2)     $\top$     $44.6667$ (deg 4, 0.417s)     $68$ (deg 1, 0.020s)

(2-1)     $x \ge 1$     $20$ (deg 1, 0.096s)     $20$ (deg 1, 0.011s)

(2-2)     $x \ge 0$     $75$ (deg 1, 0.116s)     $75$ (deg 1, 0.015s)

(2-3)     $x > 0$     $42$ (deg 1, 0.260s)     $62$ (deg 1, 0.017s)

(2-4)     $x > 0 \wedge y > 0$     $73$ (deg 1, 0.143s)     $96$ (deg 1, 0.013s)

(2-5)     $x > y$     $90$ (deg 1, 0.244s)     $90$ (deg 1, 0.017s)

Upper bounds on the raw/central moments of runtimes, with comparison to <cit.>. “T/O” stands for timeout after 30 minutes. “N/A” means that the tool is not applicable. “-” indicates that the tool fails to infer a bound. Entries with more precise results or less analysis time are marked in bold.

2*program     2*moment     2c@||@this work     2c<cit.>
upper bnd.     time (sec)     upper bnd.     time (sec)
5*(1-1)     2nd raw     201     0.019     201
3rd raw     3829     0.019     3829     0.020
4th raw     90705     0.023     90705     0.027
2nd central     32     0.029     N/A     N/A
4th central     9728     0.058     N/A     N/A
5*(1-2)     2nd raw     2357     1.068     3124     0.037
3rd raw     148847     1.512     171932     0.062
4th raw      11285725     1.914     12049876     0.096
2nd central     362     3.346     N/A     N/A
4th central     955973     9.801     N/A     N/A
5*(2-1)     2nd raw     2320     0.016     2320     11.380
3rd raw     691520     0.018     -     16.056
4th raw     340107520     0.021     -     23.414
2nd central     1920     0.026     N/A     N/A
4th central     289873920     0.049     N/A     N/A
5*(2-2)     2nd raw     8375     0.022     8375     38.463
3rd raw     1362813     0.028     -     73.408
4th raw     306105209     0.035     -     141.072
2nd central      5875     0.029     N/A     N/A
4th central     447053126     0.086     N/A     N/A
5*(2-3)     2nd raw     3675     0.039     6710     48.662
3rd raw     618584     0.049     19567045     0.039
4th raw     164423336     0.055      -     T/O
2nd central     3048     0.053     N/A     N/A
4th central     196748763     0.123     N/A     N/A
5*(2-4)     2nd raw     6625     0.035     10944     216.352
3rd raw     742825     0.048     -     453.435
4th raw     101441320     0.072     -     964.579
2nd central     6624     0.051     N/A     N/A
4th central     313269063      0.215     N/A     N/A
5*(2-5)     2nd raw     21060     0.045     -     216.605
3rd raw     9860940     0.063     -     467.577
4th raw     7298339760     0.101     -     1133.947
2nd central     20160     0.068     N/A     N/A
4th central     8044220161     0.271     N/A     N/A

<ref> compares our tool with Absynth by <cit.> on their benchmarks for upper bounds on the first moments of monotone cost accumulators.

Both tools are able to infer symbolic polynomial bounds.

Absynth uses a finer-grained set of base functions, and it supports bounds of the form $\maxp{x,y}$, which is defined as $\max(0,y-x)$.

Our tool is as precise as, and sometimes more precise than Absynth,[We compared the precision by first simplifying the bounds derived by Absynth using the pre-conditions shown in <ref>, and then comparing the polynomials.] but it is less efficient than Absynth.

One reason for this could be that we use a full-fledged numerical abstract domain to derive the logical contexts, while Absynth employs less powerful but more efficient heuristics to do that step.

Nevertheless, all the analyses completed in less than one second.

Upper bounds of the expectations of monotone costs, with comparison to <cit.>.

program     pre-condition      termination check     upper bound by our tool     lower bound     upper bound by Absynth <cit.>
$d<n$     $\bbE[T] < \infty$ (deg 1, 0.267s)      $2(n-d+1)$ (deg 1, 0.269s)     $n-d$ (deg 1, 0.256s)     $2\maxp{d,n+1}$ (deg 1, 0.170s)

$x>0$     $\bbE[T]<\infty$ (deg 1, 0.060s)     $17x$ (deg 1, 0.061s)     $1.6667 (x-1)$ (deg 1, 0.060s)     $17\maxp{0,x}$ (deg 1, 0.014s)

$x>0 \wedge y >0$     $\bbE[T]<\infty$ (deg 1, 0.063s)     $1.25x+y$ (deg 1, 0.060s)     $x$ (deg 1, 0.061s)     $1.25 \maxp{0,x} + \maxp{0,y}$ (deg 1, 0.008s)

$x > y \wedge y > 0$     $\bbE[T]<\infty$ (deg 1, 0.144s)     $1.1667x$ (deg 1, 0.072s)      $0.6667 (x -  y)$ (deg 1, 0.086s)     $1.3333\maxp{0,x}$ (deg 1, 0.014s)

$i>100 \wedge k >0$      $\bbE[T] < \infty$ (deg 1, 0.059s)     $k+2i-49$ (deg 1, 0.059s)      $k+2i-49$ (deg 1, 0.058s)     $\maxp{0,51+i+k} + 2 \maxp{0,i}$ (deg 1, 0.010s)

$x>0 \wedge y > 0$      $\bbE[T]<\infty$ (deg 1, 0.063s)     $0.5x+0.5y+2$ (deg 1, 0.044s)     $0$ (deg 1, 0.051s)     $0.5\maxp{0,x+2} + 0.5\maxp{0,y+2}$ (deg 1, 0.007s)

$l \ge 8$     $ \bbE[T] < \infty$ (deg 1, 0.058s)     $1.4286l$ (deg 1, 0.046s)     $ 1.4286 l -3$ (deg 1, 0.054s)     $\maxp{0,l} + 0.5 \maxp{1,l}$ (deg 1, 0.007s)

$n>0$       $\bbE[T]<\infty$ (deg 1, 0.309s)      $4n$ (deg 1, 0.264s)     $4n$ (deg 1, 0.292s)     $4\maxp{0,n}$ (deg 1, 0.057s)

$x<n$      $\bbE[T]<\infty$ (deg 1, 0.041s)     $2(n-x)$ (deg 1, 0.035s)     $2(n-x)$ (deg 1, 0.041s)     $2\maxp{x,n}$ (deg 1, 0.004s)

$n>0$     $\bbE[T]<\infty$ (deg 1, 0.042s)     $0.2(n+9)$ (deg 1, 0.036s)     $0.2n$ (deg 1, 0.039s)     $0.2 \maxp{0,n+9}$ (deg 1, 0.030s)

$n>0\wedge m>0$      $\bbE[T]<\infty$ (deg 1, 0.044s)     $2m$ (deg 1, 0.042s)     $0$ (deg 1, 0.043s)     $2\maxp{0,m}$ (deg 1, 0.004s)

$mt > st \wedge t >0$      $\bbE[T]<\infty$ (deg 1, 0.080s)     $mt-st+0.42t+2.1$ (deg 1, 0.071s)     $0$ (deg 1, 0.076s)     $0.42\maxp{0,t+5} + \maxp{st,mt}$ (deg 1, 0.017s)

$\top$      $\bbE[T^4]<\infty$ (deg 4, 0.118s)     $11.6667$ (deg 4, 0.066s)     $6.0624$ (deg 4, 0.063s)     $15$ (deg 1, 0.016s)

$\top$      $\bbE[T]<\infty$ (deg 1, 0.041s)     $1.2$ (deg 1, 0.030s)     $1.2$ (deg 1, 0.036s)     $1.2$ (deg 1, 0.004s)

$\top$      $\bbE[T]<\infty$ (deg 1, 0.127s)     $2.0833$ (deg 1, 0.110s)     $1$ (deg 1, 0.130s)     $2.0833$ (deg 1, 0.142s)

$x < n$      $\bbE[T^2]<\infty$ (deg 2, 0.066s)     $2(n-x)$ (deg 1, 0.053s)     $2(n-x)$ (deg 1, 0.059s)     $2\maxp{x,n}$ (deg 1, 0.004s)

$volTF > 0$      $ \bbE[T]<\infty$ (deg 1, 0.096s)     $0.6667 volTF + 7$ (deg 1, 0.082s)     $ 0.1 volTF+0.05$ (deg 1, 0.092s)     $0.3333 \maxp{0,volTF+10} + 0.3333 \maxp{0, volTF + 11}$ (deg 1, 0.079s)

$\top$      $\bbE[T]<\infty$ (deg 1, 0.072s)     $5$ (deg 1, 0.061s)     $5$ (deg 1, 0.068s)     $5$ (deg 1, 0.003s)

$x<n$      $\bbE[T]<\infty$ (deg 1, 0.041s)     $5(n-x)$ (deg 1, 0.035s)     $5 (n-x-1)$ (deg 1, 0.042s)     $5 \maxp{x,n}$ (deg 1, 0.005s)

$x>2$      $\bbE[T]<\infty$ (deg 1, 0.040s)     $0.6x$ (deg 1, 0.034s)     $0.6(x-1)$ (deg 1, 0.038s)     $0.6\maxp{0,x}$ (deg 1, 0.008s)

$x<n$      $\bbE[T]<\infty$ (deg 1, 0.047s)     $1.1429(n-x+4)$ (deg 1, 0.037s)     $1.1429 (n -x)$ (deg 1, 0.051s)     $1.1429 \maxp{x,n+4}$ (deg 1, 0.011s)

$y>0 \wedge n <0$      $\bbE[T]<\infty$ (deg 1, 0.082s)     $- 68.4795n+0.0526(y-1)$ (deg 1, 0.071s)      $-10 n$ (deg 1, 0.084s)     $68.4795 \maxp{n,0} + 0.0526\maxp{0,y}$ (deg 1, 0.016s)

$y > 9 \wedge x - y > 2$      $\bbE[T]<\infty$ (deg 1, 0.073s)     $1.65x-1.5y$ (deg 1, 0.061s)     $1.65 x - 1.5 y -4.65$ (deg 1, 0.072s)     $1.65 \maxp{y,x} + 0.15 \maxp{0,y}$ (deg 1, 0.011s)

$x+1<n \wedge y<m$      $\bbE[T]<\infty $ (deg 1, 0.076s)     $2(m-y)+0.6667(n-x)$ (deg 1, 0.065s)      $0.6667(n-x)-1.3333$ (deg 1, 0.074s)     $2\maxp{y,m} + 0.6667 \maxp{x,n}$ (deg 1, 0.010s)

$h<t$      $\bbE[T]<\infty $ (deg 1, 0.052s)     $0.6667(t-h+9)$ (deg 1, 0.039s)     $0.6667 (t-h+1) $ (deg 1, 0.048s)     $0.6667 \maxp{h, t+9}$ (deg 1, 0.027s)

$x>0 \wedge y>0$      $\bbE[T]<\infty$ (deg 1, 0.069s)     $2.25x+y$ (deg 1, 0.059s)     $2.25x$ (deg 1, 0.069s)     $2.25\maxp{0,x}+\maxp{0,y}$ (deg 1, 0.008s)

$x+1<n \wedge y <m$      $\bbE[T]<\infty$ (deg 1, 0.065s)     $2(m-y)+0.6667(n-x)$ (deg 1, 0.062s)      $0.6667(n-x)-1.3333$ (deg 1, 0.077s)     $2\maxp{y,m} + 0.6667\maxp{x,n}$ (deg 1, 0.010s)

$x<n$      $\bbE[T]<\infty$ (deg 1, 0.039s)     $2(n-x+1)$ (deg 1, 0.035s)     $2(n-x)$ (deg 1, 0.041s)     $2 \maxp{x,n+1}$ (deg 1, 0.004s)

$n>0$      $\bbE[T^2]<\infty$ (deg 3, 0.171s)     $2n$ (deg 2, 0.071s)     $n$ (deg 2, 0.080s)     $2\maxp{0,n}$ (deg 1, 0.350s)

$\top$      $\bbE[T]<\infty$ (deg 1, 0.033s)     $2$ (deg 1, 0.033s)     $2$ (deg 1, 0.035s)     $2$ (deg 1, 0.004s)

$k>0$      $\bbE[T]<\infty$ (deg 1, 0.048s)     $2$ (deg 1, 0.047s)     $0$ (deg 1, 0.052s)     $\maxp{0,k}$ (deg 1, 0.007s)

$n>0$      $\bbE[T] < \infty$ (deg 1, 0.054s)     $0.2778(n+7)$ (deg 1, 0.047s)     $0.2778 n$ (deg 1, 0.051s)     $0.3846 \maxp{0,n+6}$ (deg 1, 0.017s)

$n<10$      $ \bbE[T]<\infty $ (deg 1, 0.067s)     $-4.9333n+98.6667$ (deg 1, 0.057s)     $ - 4.9333 n + 54.2667 $ (deg 1, 0.064s)     $4.9333 \maxp{n,20}$ (deg 1, 0.073s)

$x<n$      $\bbE[T]<\infty$ (deg 1, 0.042s)     $2(n-x)$ (deg 1, 0.036s)     $2(n-x)$ (deg 1, 0.042s)     $2\maxp{x,n}$ (deg 1, 0.004s)

$n>0$      $\bbE[T]<\infty$ (deg 1, 0.095s)     $7.5n$ (deg 1, 0.081s)     $7.5n$ (deg 1, 0.097s)     $7.5\maxp{0,n}$ (deg 1, 0.015s)

$y,w,n,m>0$     $\bbE[T]<\infty$ (deg 2, 0.145s)     $4mn+2n+w+0.6667(y+1)$ (deg 2, 0.142s)     $6n+0.6667y$ (deg 1, 0.142s)     $(4\maxp{0,m}+2)\maxp{0,n}+(\maxp{0,w} +0.3333\maxp{0,y})\maxp{0,y+1}+0.6667$ (deg 2, 0.451s)

$n>0 \wedge m>0$      $\bbE[T^2] < \infty$ (deg 4, 0.506s)     $2mn+4n$ (deg 2, 0.080s)        $2mn+2n$ (deg 2, 0.083s)     $2\maxp{0,m}\maxp{0,n} + 4\maxp{0,n}$ (deg 2, 0.692s)

$x>0$      $ \bbE[T^2] < \infty$ (deg 4, 0.062s)      $4.5x^2+10.5x$ (deg 2, 0.052s)     $4.5 x^2 + 1.5 x $ (deg 2, 0.052s)     $1.5\maxp{0,x}^2+3\maxp{1,x}\maxp{0,x} + 10.5 \maxp{0,x}$ (deg 2, 0.101s)

$x>0$      $ \bbE[T^2] < \infty$ (deg 4, 0.085s)      $0.6667(x^2+3x)$ (deg 2, 0.059s)      $ 0.6667 (x^2- x)$ (deg 2, 0.059s)     $2\maxp{0,x+1}\maxp{0,x}$ (deg 2, 0.133s)

$n>1$      $\bbE[T^2] < \infty$ (deg 4, 0.100s)     $1.5n^2-4.5n+3$ (deg 2, 0.057s)     $1.5n^2-4.5n+3$ (deg 2, 0.058s)     $1.5\maxp{1,n} \maxp{2,n}$ (deg 2, 0.203s)

$n>0$      $\bbE[T^2] < \infty$ (deg 4, 0.105s)     $3n^2$ (deg 2, 0.055s)     $3 n^2$ (deg 2, 0.059s)     $3\maxp{0,n}^2$ (deg 2, 0.030s)

$arg_l < arg_h$     T/O     $0.25 (arg_h -arg_l)^2 + 1.75 (arg_h  - arg_l)$ (deg 2, 0.313s)     $2 (arg_h -  arg_l)$ (deg 1, 0.233s)      $0.25\maxp{arg_l,arg_h}^2+1.75\maxp{arg_l,arg_h}$ (deg 2, 0.398s)

$mP > 0 \wedge sP > mP$     $\bbE[T^2]<\infty$ (deg 2, 0.079)     $1.5(sP^2-mP^2+sP - mP)$ (deg 2, 0.073s)     $1.5(sP^2-mP^2+sP-mP)$ (deg 2, 0.074s)     $1.5\maxp{mP,sP}^2+3 \maxp{mP,sP} \maxp{0,mP} +1.5\maxp{mP,sP} $ (deg 2, 0.192s)

<ref> compares our tool with <cit.> on their benchmarks for lower and upper bounds on the first moments of accumulated costs.

All the benchmark programs satisfy the bounded-update property.

To ensure soundness, our tool has to perform an extra termination check required by <ref>.

Our tool derives similar symbolic lower and upper bounds, compared to the results of <cit.>.

Meanwhile, our tool is more efficient than the compared tool.

One source of slowdown for <cit.> could be that they use Matlab as the LP backend, and the initialization of Matlab has significant overhead.

Upper and lower bounds of the expectation of (possibly) non-monotone costs, with comparison to <cit.>.

program     pre-cond.      termination          bounds by our tool     bounds by <cit.>
Bitcoin     2*$x \ge 1$      $\bbE[T]<\infty$      ub.     $-1.475x$ (deg 1, 0.078s)       $-1.475 x + 1.475$ (deg 2, 3.705s)
| || |-|-||-
Mining         (deg 1, 0.080s)     lb.     $-1.5x$ (deg 1, 0.088s)      $-1.5x$ (deg 2, 3.485s)
Bitcoin     2*$y \ge 0$      $\bbE[T^2] < \infty$      ub.     $-7.375y^2 -66.375y$ (deg 2, 0.127s)      $-7.375 y^2 - 41.625 y + 49$ (deg 2, 5.936s)
| || |-|-||-
Mining Pool         (deg 4, 0.168s)     lb.     $- 7.5y^2-67.5 y$ (deg 2, 0.134s)      $-7.5y^2 -67.5y$ (deg 2, 6.157s)
Queueing     2*$ n > 0$      $\bbE[T^2] < \infty$      ub.      $0.0531 n$ (deg 2, 0.134s)      $0.0492n$ (deg 3, 69.669s)
| || |-|-||-
Network         (deg 2, 0.208s)     lb.     $0.028n$ (deg 2, 0.139s)      $0.0384n$ (deg 3, 68.849s)
Running     2*$ x \ge 0$      $\bbE[T^2] < \infty$      ub.     $0.3333 (x^2 + x)$ (deg 2, 0.063s)      $0.3333 x^2 + 0.3333 x$ (deg 2, 3.766s)
| || |-|-||-
Example          (deg 2, 0.064s)    lb.     $0.3333( x^2 + x)$ (deg 2, 0.059s)      $0.3333 x^2+0.3333x -0.6667$ (deg 2, 3.555s)
Nested     2*$i \ge 0$      $\bbE[T^2] < \infty$      ub.     $0.3333i^2+i$ (deg 2, 0.117s)      $0.3333 i^2 + i$ (deg 2, 28.398s)
| || |-|-||-
Loop         (deg 4, 0.127s)     lb.      $0.3333 i^2 + i$ (deg 2, 0.115s)      $0.3333 i^2-i$ (deg 2, 7.299s)
Random     2*$x \le n$      $\bbE[T]<\infty$     ub.      $2.5x-2.5n-2.5$ (deg 1, 0.064s)       $2.5x-2.5n$ (deg 2, 4.536s)
| || |-|-||-
Walk         (deg 1, 0.063s)    lb.     $2.5 x-2.5n-2.5$ (deg 1, 0.068s)      $2.5x-2.5n-2.5$ (deg 2, 4.512s)
2*2D Robot     2*$ x \ge y$     $\bbE[T^2] < \infty$      ub.      $1.7280(x-y)^2 +31.4539(x-y)+126.5167$ (deg 2, 0.132s)      $1.7280(x-y)^2 + 31.4539 (x- y)+126.5167$ (deg 2, 7.133s)
| || |-|-||-
(deg 2, 0.145s)    lb.     $1.7280(x-y)^2+31.4539(x -y)+29.7259$ (deg 2, 0.121s)       $1.7280(x-y)^2 + 31.4539 (x -y)$ (deg 2, 7.040s)
Good       $d \le 30 \wedge {}$       $\bbE[T^2] < \infty$       ub.     $-0.5n - 3.6667d + 117.3333$ (deg 2, 0.093s)       $0.0067 dn -0.7n-3.8035 d+0.0022d^2 +119.4351$ (deg 2, 5.272s)
| || |-|-||-
Discount     $n \ge 1$     (deg 2, 0.093s)    lb.     $ - 0.005 n^2-0.5 n$ (deg 2, 0.092s)      $0.0067 dn - 0.7133n-3.8123d + 0.0022d^2+112.3704$ (deg 2, 5.323s)
Pollutant      2*$n \ge 0$        $\bbE[T^2] <\infty$      ub.     $-0.2n^2 +50.2 n$ (deg 2, 0.092s)     $-0.2 n^2 + 50.2n$ (deg 2, 5.851s)
| || |-|-||-
Disposal        (deg 2, 0.091s)     lb.     $ -0.2 n^2+50.2n -435.6$ (deg 2, 0.094s)      $-0.2n^2 +50.2n-482$ (deg 2, 5.215s)
Species     $a \ge 5 \wedge {}$     $\bbE[T^2] < \infty$      ub.      $40ab-180a-180b+810$ (deg 2, 0.045s)      $40ab-180a-180b+810$ (deg 3, 5.545s)
| || |-|-||-
Fight     $b \ge 5$     (deg 2, 0.042s)      lb.     N/A      N/A

§ CASE STUDY: TIMING-ATTACK ANALYSIS

We motivate our work on central-moment analysis using a probabilistic program
with a timing-leak vulnerability, and demonstrate how the results from an analysis
can be used to bound the success rate of an attack program that attempts to exploit the vulnerability.

The program is extracted and modified from a web application provided by DARPA
during engagements as part of the STAC program <cit.>.

In essence, the program models a password checker that compares an input 𝕀guess with
an internally stored password 𝕀secret, represented as two $N$-bit vectors.

The program in <ref>(a) is the interface of the checker,
and <ref>(b) is the comparison function ,
which carries out most of the computation.

The statements of the form “$\kw{tick}(\cdot)$” represent a cost model for the
running time of , which is assumed to be observable by the

iterates over the bits from high-index to low-index,
and the running time expended during the processing of bit $i$ depends on
the current comparison result (stored in $\id{cmp}$), as well as on the
values of the $i$-th bits of $\id{guess}$ and $\id{secret}$.

Because the running time of  might leak information about the
relationship between $\id{guess}$ and $\id{secret}$,  introduces some random delays
to add noise to its running time.

However, we will see shortly that such a countermeasure does not protect the
program from a timing attack.

func (𝕀guess, 𝕀secret) begin
$i \coloneqq N; \id{cmp} \coloneqq 0;$

while $i>0$ do

while $i>0$ do
if prob($0.5$) then break fi

if $\id{cmp} > 0 \vee (\id{cmp} = 0 \wedge \id{guess}[i] > \id{secret}[i])$

then $\id{cmp} \coloneqq 1$

if $\id{cmp} < 0 \vee (\id{cmp} = 0 \wedge \id{guess}[i] < \id{secret}[i])$

then $\id{cmp} \coloneqq {-1}$

$i \coloneqq i - 1$

return 𝕀cmp

func (𝕀guess) begin
$\id{cmp} \coloneqq \mathsf{compare}(\id{guess}, \id{secret});$

if $\id{cmp} = 0$ then

$\id{guess} \coloneqq \vec{0}$;

$i \coloneqq N$;

while $i > 0$ do
$\id{next} \coloneqq \id{guess};$

$\id{next}[i] \coloneqq 1;$

$\id{est} \coloneqq \kw{estimateTime}(K,\mathsf{check}(\id{next}));$

if $\id{est} \le 13N - 1.5i$ then
$\id{guess}[i] \coloneqq 0$
$\id{guess}[i] \coloneqq 1$

$i \coloneqq i - 1$

(a) The interface of the password checker.
(b) A function that compares two bit vectors, adding some random noise.
(c) An attack program that attempts to exploit the timing properties of  to
find the value of the password stored in $\id{secret}$.

We now show how the moments of the running time of —the
kind of information provided by our central-moment analysis (<ref>)—are
useful for analyzing the success probability of the attack program given in

Let $T$ be the random variable for the running time of .

A standard timing attack for such programs is to guess the bits of $\mathit{secret}$ successively.

The idea is the following: Suppose that we have successfully obtained the bits $\mathit{secret}[i+1]$ through
we now guess that the next bit, $\mathit{secret}[i]$, is $1$ and set $\mathit{guess}[i] \coloneqq 1$.

Theoretically, if the following two conditional expectations

\begin{align}
\begin{split} \expe[T_1] & \defeq \expe[T \mid \textstyle{\bigwedge_{j=i+1}^N (\id{secret}[j] = \id{guess}[j])} \\ & \qquad\qquad {} \wedge (\id{secret}[i] = 1 \wedge \id{guess}[i] = 1)] \end{split} \label{Eq:GuessCorrect} \\
\begin{split} \expe[T_0] & \defeq \expe[T \mid \textstyle{\bigwedge_{j=i+1}^N (\id{secret}[j] = \id{guess}[j])}\\ & \qquad \qquad {} \wedge (\id{secret}[i] = 0 \wedge \id{guess}[i] = 1)] \end{split} \label{Eq:GuessWrong}
\end{align}

have a significant difference, then there is an opportunity to check our guess by
running the program multiple times, using the average running time as
an estimate of $\expe[T]$, and choosing the value of $\mathit{guess}[i]$ according
to whichever of (<ref>) and (<ref>) is closest to our

However, if the difference between $\expe[T_1]$ and $\expe[T_0]$ is not significant enough,
or the program produces a large amount of noise in its running time, the attack might not be
realizable in practice.

To determine whether the timing difference represents an exploitable vulnerability,
we need to reason about the attack program's success rate.

Toward this end, we can analyze the failure probability for setting $\mathit{guess}[i]$
incorrectly, which happens when, due to an unfortunate fluctuation, the running-time
estimate $\id{est}$ is closer to one of $\expe[T_1]$ and $\expe[T_0]$, but the truth is actually
the other.

For instance, suppose that $\expe[T_0] < \expe[T_1]$ and $est < \frac{\expe[T_0]+\expe[T_1]}{2}$;
the attack program would pick $T_0$ as the truth, and set $\mathit{guess}[i]$ to $0$.

If such a choice is incorrect, then the actual distribution of $\id{est}$
on the $i$-th round of the attack program satisfies $\expe[\id{est}] = \expe[T_1]$,
and the probability of this failure event is

\begin{align*}
& \prob\lrsq{\id{est} < \frac{\expe[T_0]+\expe[T_1]}{2}} \\
={} & \prob\lrsq{ \id{est} - \expe[T_1] < \frac{\expe[T_0]-\expe[T_1] }{2} } \\
={} & \prob\lrsq{ \id{est} - \expe[\id{est}] < \frac{\expe[T_0]-\expe[T_1] }{2} }
\end{align*}

under the condition given by the conjunction in (<ref>).

This formula has exactly the same shape as a tail probability,
which makes it possible to utilize moments and concentration-of-measure inequalities <cit.> to bound the probability.

The attack program is parameterized by $K > 0$, which represents the number of trials it performs
for each bit position to obtain an estimate of the running time.

Assume that we have applied our central-moment-analysis technique
and obtained the following inequalities on the
mean (i.e., the first moment), the second moment, and the variance (i.e., the second
central moment) of the quantities (<ref>) and

Missing: add the second moment for use later to contrast the attack-program bounds we
obtain via variances versus the weaker bounds one would obtain using Markov's inequality.

\begin{align}
\expe[T_1] & \ge 13N,      & \expe[T_1] & \le 15N,    \notag  \\
\vari[T_1] & \le 26N^2 + 42N, \label{Eq:TimeCorrect}  \\
\expe[T_0] & \ge 13N - 5i, & \expe[T_0] & \le 13N - 3i, \notag \\
\vari[T_0] & \le 8N-36i^2+52Ni+24i. \label{Eq:TimeWrong}
\end{align}

To bound the probability that the attack program makes an incorrect
guess for the $i$-th bit, we do case analysis:

* Suppose that $\id{secret}[i] = 1$, but the attack program assigns $\id{guess}[i] \coloneqq  0$.
The truth—with respect to the actual distribution of the running time $T$ of
for the $i$-th bit—is that $\expe[\id{est}] = \expe[T_1]$,
but the attack program in <ref>(c)
executes the then-branch of the conditional statement.

Thus, our task reduces to that of bounding $\prob[\id{est} < 13N - 1.5i]$.

The estimate $\id{est}$ is the average of $K$ i.i.d. random variables drawn from a distribution with
mean $\expe[T_1]$ and variance $\vari[T_1]$.

We derive the following, using the inequalities from (<ref>):

\begin{align}
\expe[\id{est}] & = \expe[T_1] \ge 13N, \notag \\
\vari[\id{est}] & = \frac{\vari[T_1]}{K} \le \frac{26N^2+42N}{K}. \label{Eq:EstMoments}
\end{align}

We now use Cantelli's inequality.

[Cantelli's inequality]
If $X$ is a random variable and $a>0$,
then we have $\prob[X - \expe[X] \le -a] \le \frac{\vari[X]}{\vari[X]+a^2}$
and $\prob[X - \expe[X] \ge a] \le \frac{\vari[X]}{\vari[X]+a^2}$.

We are now able to derive an upper bound on $\prob[\id{est} < 13N - 1.5i]$ as follows:

\begin{align*}
& \prob[\id{est} \le 13N - 1.5i] \\
={} & \prob[\id{est} - 13N \le -1.5i]  \\
{}\le{} & \prob[\id{est} - \expe[\id{est}] \le -1.5i]  & \reason{$\expe[\id{est}] \ge 13N$ by \eqref{Eq:EstMoments}} \\
{}\le{} & \frac{\vari[\id{est}]}{\vari[\id{est}]+(1.5i)^2} & \reason{Cantelli's inequality} \\
={} & \frac{26N^2+42N}{26N^2+42N+2.25Ki^2}.
\end{align*}

* The other case, in which $\id{secret}[i]=0$ but the attack program
chooses to set $\id{guess}[i] \coloneqq 1$, can be analyzed in a similar
way to the previous case, and the bound obtained is the following:

\begin{align*}
& \prob[\id{est} > 13N - 1.5i] \\
{} \le {} & \prob[\id{est} \ge 13N - 1.5i] \\
{}\le{} & \frac{8N-36i^2+52Ni+24i }{8N-36i^2+52Ni+24i + 2.25Ki^2 }.
\end{align*}

Let $F^i_1$ and $F^i_0$, respectively, denote the two upper bounds on the failure probabilities
for the $i$-th bit.

For the attack program to succeed, it has to succeed for all bits.
If the number of bits is $N=32$, and in each iteration the number of trials that the
attack program uses to estimate the running time is $K=10^4$, we derive a
lower bound on the success rate of the attack program from the
upper bounds on the failure probabilities derived above:

\[
\prob[\textsc{Success}] \ge \prod_{i=1}^{32} (1 - \max(F^i_1, F^i_0)) \ge 0.219413,
\]

which is low, but not insignificant.

However, the somewhat low probability is caused by a property of :
if $\id{guess}$ and $\id{secret}$ share a very long prefix, then the running-time behavior on different values of $guess$
becomes indistinguishable.

However, if instead we bound the success rate for all but the last six bits, we obtain:

\[
\prob[\textsc{Success for all but the last six bits}] \ge 0.830561,
\]

which is a much higher probability!

The attack program can enumerate all the possibilities to resolve the last six bits.
(Moreover, by brute-forcing the last six bits, a total of $10,\!000 \times 26 + 64 = 260,\!064$
calls to  would be performed, rather than $320,\!000$.)

Overall, our analysis concludes that the  and  procedures in
<ref> are vulnerable to a timing attack.