A Usage-Aware Sequent Calculus
for Differential Dynamic Logic

Myra Dotzel1 Stefan Mitsch2 André Platzer3

M. Dotzel et al.

Carnegie Mellon University, Pittsburgh PA 15213, USA

<EMAIL_ADDRESS>DePaul University, Chicago IL 60614, USA

<EMAIL_ADDRESS>Karlsruhe Institute of Technology, Karlsruhe, Germany

Modeling languages like differential dynamic logic () have proof calculi capable of proving guarantees for safety-critical applications.
However, programmers may unintentionally over-specify assumptions and program statements, which results in overly constrained models, and consequently, weak or vacuous guarantees.
In hybrid systems models, such constraints come from multiple places, ranging from initial conditions to domain constraints in the middle of differential equations, thereby making it nontrivial to consistently track the conglomerate.
We present a novel sequent calculus for that tracks which constraints to weaken or remove while preserving correctness guarantees.
When properties follow entirely from constraints uninfluenced by program statements, this analysis spots outright flaws in models.
We prove soundness and completeness of our proof calculus.

§ INTRODUCTION

Hybrid systems verification establishes crucial correctness properties of cyber-physical systems models. Programmers who verify such properties may write a program that describes the physical behavior of their system. Then, they attempt to show that the desired postconditions hold after running the program under a certain set of assumptions by dissecting the model into a series of smaller proof obligations until elementary facts are reached.
To ensure fidelity, the programmer must be cautious that they are realistically capturing all behavior of the hybrid system.
The results are only useful if the models adequately capture the physical dynamics of the system [21, 29].
However, most cyber-physical systems models aspire to model reality which makes them inherently difficult to write and analyze. They combine descriptions of control algorithms with descriptions of the physical dynamics of that application, which can be represented as a system of differential equations and evolution domain constraints on which the dynamics is applicable.
While uncertainty about the fidelity of the control model can be overcome by verified compilation [4], the physics model involves assumptions that need a combination of offline and online verification at runtime [21].

Prior work on vacuity detection [10, 19] identifies vacuous components of a model as potential bugs. Yet, cyber-physical systems models are often prone to over-specification [29], which is not detected by these techniques. As a remedy, techniques like mutation testing can find bugs in cyber-physical systems models [3], but these techniques are limited to finding a single bug whereas multiple (interconnected) bugs may arise. Additionally, the complexity of conducting correctness proofs is inherently linked to proofs of real arithmetic statements, which is doubly-exponential in the number of variables [8]. This makes verification challenging and combinatorial exploration of proof alternatives infeasible [15].

This paper starts from the observation that the careful inspection of proofs of hybrid system correctness properties provides key insights about the fidelity of the models [28].
For example, a proof of safety about the effects of a hybrid systems controller is vacuous if safety already follows directly from the evolution domain constraints of its differential equations, which, after all, are assumptions about the physics, not conclusions about the safety of the control actions.
This phenomenon only gets more subtle, and the corresponding analysis of the proof more difficult, when a mix of assumptions about parameters, initial states, and evolution domain constraints is responsible for the proof of the safety property.

This paper introduces a sequent calculus for differential dynamic logic () [25, 27] that has built-in logical mechanisms for tracking constraints that were used in the proof, regardless of where they originated from in the hybrid systems model, and ways in which these constraints could be generalized to preserve the proof. This is accomplished by tracing the proof of a formula and computing usage information for constraints in each proof step.
We augment the sequent calculus with a dataflow analysis that tracks constraint usage and possible mutations by a propagation from the proofs of elementary facts to the proof of the desired conclusion.

The tracking of constraint usage and mutations serve complementary roles: constraint usage is useful while conducting the proof (i.e., where do facts come from, and how are they linked to the original conjecture), whereas mutations are most meaningful after the proof is done in a separate model improvement step, where a user selects from the tracked mutation alternatives.

The sequent calculus is flexible in that it provides different ways of instantiating the usage tracking.

One extreme explores proof branches in parallel and merges their usage information subsequently. The other provides a sequential analysis, threading usage information across sibling branches.
The proof calculi we introduce are general enough that the techniques could be extended to provide usage and data-flow analysis for other proof systems, yet the significance and subtleties are special for hybrid systems. This paper makes the following contributions:

* A novel proof calculus that tracks the propagation of information in a proof to discern constraint usage by analyzing proof branches in parallel.

* , the sequential counterpart of , that reuses information from previously-analyzed proof branches to guide the analysis.

* An extension of and for determining admissible cut mutations.

* Soundness and completeness guarantees for both calculi with respect to .

§ BACKGROUND AND MOTIVATION

is a language for specifying hybrid programs [25] that model cyber-physical systems. Programmers specify formulas to express properties of hybrid systems. programs consist of statements and formulas, as shown below.

\begin{align*}
\mathit{Term} \; e, d &::= x \mid c \mid e + d \mid e \cdot d \mid f(e_1, \dots ,e_k) \\
\mathit{Stmt} \; \alpha,\beta &::= x:=e \mid x:=* \mid x' = f(x) \& Q \mid \, ?Q \mid \alpha; \beta \mid \alpha \cup \beta \mid \alpha^*\\
\mathit{Fml} \; P,Q  &::= \text{true} \mid \text{false} \mid e \sim d \mid p(e_1, \dots, e_k)\mid \lnot P \mid P \bowtie Q
\mid \forall x \; P \mid \exists x \; P  \\
&\;\;\;\;\;\;\mid [\alpha] P \mid \langle\alpha\rangle P
\end{align*}

Terms $e, d$ in are variables $x$, rational constants $c \in \mathbb{Q}$, polynomials, and functions of variable arguments. statements $\alpha, \beta$ include deterministic and non-deterministic assignments of a term to a variable, differential equations, test statements, program sequencing, non-determinstic choice, and repetition. formulas $P, Q$ include boolean primitives, binary relations $\sim \; \in \{=, \geq, >\}$ between terms, boolean predicates, negation, boolean connectives $\bowtie \; \in \{\land, \lor, \rightarrow, \leftrightarrow\}$, universal and existential quantification, and two kinds of modalities $\left[\cdot\right]$ and $\langle\cdot\rangle$. The modality $\left[\alpha\right]P$ means that $P$ holds after all runs of $\alpha$, whereas $\langle\alpha\rangle P$ means that $P$ holds after some run of $\alpha$.

A sequent takes the form $\Gamma \vdash \Delta$ where $\Gamma$ and $\Delta$ are finite sets of formulas such that $\bigwedge_{p \in \Gamma} p \rightarrow \bigvee_{q \in \Delta} q$.

For example, consider a formula that models the aerodynamics of a skydiver's parachute (Fig. <ref>, with assumptions highlighted in bold).

\begin{align*}
& \mathbf{A} {\to} \left[\left(\left(?(\mathbf{v - gT > -\sqrt{g/r_{op}} \land r = r_{cl} \land x > 100}) \cup \; r := r_{op}\right) t:= 0; \text{ODE} \& \mathbf{Q}\right)^*\right] P\\
& \text{Parameters}~ \mathbf{g = 9.81, r_{op} = 1, r_{cl} = 0}, v_{max}, T, x, v, r, t \\
& A \triangleq \mathbf{g > 0 \land r_{op} > r_{cl} \land T > 0 \land v_{max} < -\sqrt{g/r_{op}} \land x \geq 0 \land -\sqrt{g/r_{op}} < v < 0 \land r = r_{cl}} \\
& P \triangleq \mathbf{x = 0} \to v \geq v_{max} \\
& Q \triangleq \mathbf{t \leq T,x \geq 0, v < 0} \\
%&I(v) \triangleq x \geq 0 \land -\sqrt{g/p} < v < 0 \\
& \text{ODE} \triangleq x' = v, v' = -g + rv^2, t' = 1
\end{align*}

Model of parachute dynamics, adopted from [13]

The program runs under a set of assumptions $A$, and under all iterations of the program, postcondition $P$ holds. The postcondition expresses that when the skydiver hits the ground, their velocity $v$ will be bounded by the maximal (w.r.t. magnitude) acceptable touchdown velocity $v_{max}$.

The overall program structure is a loop, and the $[\cdot]$ modality expresses that $P$ holds after all iterations of the loop. Here, we assume simple parameters $g=9.81, r_{op}=1, r_{cl}=0$ to explain the mechanics of our approach.

At the beginning of each loop iteration, the program may choose to either run the branch $?(v - gT > -\sqrt{g/r_{op}} \land r = r_{cl} \land x > 100)$ or the branch $r := r_{op}$. The first branch allows the skydiver to keep falling when safe, acting as a skip instruction if the aerodynamic drag coefficient is $r=r_{cl}$ and the skydiver's position is a safe distance from the ground (\(x>100\)).

The second branch simulates opening the parachute, inducing an aerodynamic drag coefficient by setting $r$ equal to the non-zero drag coefficient $r_{op}$ of the open parachute.
After this choice, time $t$ is reset to $0$ and the program runs the ODE as allowed by the domain constraint $Q$. The metavariable ODE models the dynamics of the skydiver's parachute in free fall but where velocity is affected by aerodynamic drag, while $t' = 1$ acts as a clock and $t\leq T$ imposes a time limit $T$.
Domain constraint $Q$ enforces that the skydiver's position is above ground and that velocity is negative during evolution (parachute descends).

i_5,i_6,i_7,u_1yellowI(x_0,v_0), j,k,lyellowL(x_0,v_0), nt= 0, rv = v_0 χχΣ s-g + rv^2 ≥-g

i_5,i_6,i_7,u_1yellowI(x_0,v_0), j,k,lyellowL(x_0,v_0), nt= 0, rv = v_0 χχΣ{{o_1}}

[o_1x' := v] s-g + rv^2 ≥-g

i_5,i_6,i_7,u_1yellowI(x_0,v_0), j,k,lyellowL(x_0,v_0), nt= 0, rv = v_0 χχΣ{{o_1}, {o_2}_id}

[o_2v' := -g + rv^2][o_1x' := v] sv' ≥-g

i_5,i_6,i_7,u_1yellowI(x_0,v_0), j,k,lyellowL(x_0,v_0), nt= 0, rv = v_0
χχΣ{{o_1}, {o_2}_id, {o_3}_id}

[o_3t' := 1][o_2v' := -g + rv^2][o_1x' := v] sv' ≥-gt'

i_5,i_6,i_7,u_1yellowI(x,v), j,k,lyellowL(x,v), nt= 0

[o⃗ODE & p⃗Q]sv≥v_0-gt

i_5,i_6,i_7,u_1yellowI(x,v), j,k,lyellowL(x,v), nt= 0

χχΘ [o⃗ODE & p⃗Q] i_7v > -√(g/r_op)

i_5,i_6,i_7,u_1yellowI(x,v), j,k,lyellowL(x,v), nt= 0 χχΘ

[o⃗ODE & p⃗Q] (i_5x ≥0 i_6v < 0 u_1x > -1)
[o⃗ODE & p⃗Q] i_7v > -√(g/r_op)

i_5,i_6,i_7,u_1yellowI(x,v) χχΘ
[?j,k,lyellowL(x,v)] [nt:= 0; o⃗ODE & p⃗Q] i_5,i_6,i_7,u_1yellowI(x,v)

u_1  fresh

i⃗A χχΩ
[({?(j,k,lyellowL(x,v)); ∪  mr := r_op;} nt:= 0; o⃗ODE & p⃗Q)^*]

i⃗A →[({?(j,k,lyellowL(x,v)); ∪  mr := r_op;} nt:= 0; o⃗ODE & p⃗Q)^*]

$\atomlabel{j,k,l}L(x,v) \triangleq \atomlabel{j}{\mathcolorbox{yellow}{v - gT > -\sqrt{g/r_{op}}}} \land \atomlabel{k}{r = r_{cl}} \land \atomlabel{l}{\mathcolorbox{yellow}{x > 100}}$

$\atomlabel{\phinode{ }{\vec{i}}{\vec{u}}}I(x,v) = \atomlabel{i_5,i_6,i_7,u_1}I(x,v) \triangleq \atomlabel{i_5}x \geq 0 \land \atomlabel{i_6}v<0 \land \atomlabel{i_7}v>-\sqrt{g/r_{op}} \land \atomlabel{u_1}{\mathcolorbox{yellow}{x > -1}} \color{blue}$

$\color{blue}\chi = \emptyset$

$\color{blue}\Sigma = \{\color{red}k_{\color{violet}id}\color{blue}, \color{red}s_{\color{violet}id}\color{blue}, \any{\color{red}\{i_5\}}\color{blue}, \any{\color{red}\{i_6\}}\color{blue}, \any{\color{red}\{i_7\}}\color{blue}, \any{\color{red}j}\color{blue}, \any{\color{red}l}\color{blue}, \color{red}n_{\color{violet}any}\color{blue}, \any{\color{red}r}\color{blue}, \any{\color{red}\{u_1\}}\color{blue}\}$

$\color{blue}\Theta = \{{\color{red}\fuse{i_5}{p_2}}_{\color{violet}\{id,W\}}\color{blue},\any{\color{red}\fuse{i_6}{p_3}}\color{blue}, \any{\color{red}j}\color{blue}, \any{\color{red}l}\color{blue}, \any{\color{red}\{p_1\}}\color{blue}, \color{red}\{i_7\}_{\color{violet}id}\color{blue}, \color{red}k_{\color{violet}id}\color{blue}, \any{\color{red}\{o_1\}}\color{blue}, \color{red}\{o_2\}_{\color{violet}id}\color{blue}, \color{red}\{o_3\}_{\color{violet}id}\color{blue}, \color{red}n_{\color{violet}id}\color{blue}, \any{\color{red}\{u_1\}}\color{blue}\}$

$\color{blue}\Omega = \{\color{red}k_{\color{violet}id}\color{blue}, \any{\color{red}j}\color{blue}, \any{\color{red}l}\color{blue}, \any{\color{red}\{o_1\}}\color{blue}, \color{red}\{o_2\}_{\color{violet}id}\color{blue}, \color{red}\{o_3\}_{\color{violet}id}\color{blue}, \color{red}n_{\color{violet}id}\color{blue}, \color{red}\{i_7\}_{\color{violet}id}, \any{\color{red}m}\color{blue}, \color{red}\{i_5\}_{\color{violet}id}\color{blue}, \color{red}\{i_6\}_{\color{violet}id}\color{blue}, \any{\color{red}\{p_1\}}\color{blue}, \color{red}\{p_2\}_{\color{violet}id}\color{blue},$

$\color{red}\{p_3\}_{\color{violet}id}\color{blue}, \any{\color{red}\{i_1\}}\color{blue}, \any{\color{red}\{i_2\}}\color{blue}, \any{\color{red}\{i_3\}}\color{blue}, \any{\color{red}\{i_4\}}\color{blue}, \any{\color{red}\{i_8\}}\color{blue}, \color{red}\vec{q}_{\color{violet}id}\color{blue}\}$

Parachute example proof fragments

Since the formula is valid, it has a proof in the proof calculus.
We show a small chunk of an example proof, or proof tree, in boxes in Fig. <ref> (full proof in Appendix <ref>). A zig-zag border at the top indicates that the proof continues in another snippet at the annotated subgoals, while a zig-zag border at the bottom indicates that the snippet continues from an open subgoal of another snippet. For now, ignore all the red, blue, and violet  annotations and just focus on the black proof tree and $\mathcolorbox{yellow}{\text{yellow}}$ highlights.

The proof begins in the bottom fragment of Fig. <ref>. The proof rules will be discussed in greater detail in Sec. <ref>. The first proof step, M:$\rightarrow$R, moves the left-hand side $A$ into the set of assumptions to the left of the turnstile. In the next step, M:loop dissects the loop which spawns three sub-branches.

In branch (3a), the proof continues with M:$[?]$, and up to M:$[]\land$. The axiom M:$[]\land$, while not included in the core calculus, is derivable from the axiom M:K.

At the step M:$\land$R, the proof forks into two branches, proving each conjunct separately.
The branch that proves the right conjunct forks into two sub-branches with M:dC. The proof continues in branch (3h) until the leaf rule M:QE is reached.

By carefully inspecting the proof tree in Fig. <ref>, we notice that the original model is over-specified.
That is, some information could be mutated or generalized while still maintaining validity. In particular, $\mathcolorbox{yellow}{\text{highlighted}}$ components $x > 100$, $v - gT > - \sqrt{g/r_{op}}$, and $x > -1$ are not used; they are neither necessary to prove the closing step M:QE in (3h) nor are they involved in proving the rest of the branch. Therefore, they could be entirely removed while producing the same or a similar proof. Thus, a formula without this information, or some generalized form of it, would still uphold its original correctness properties, i.e. the formula would still be valid.

Here, we automate the detection of model components that can be generalized by systematically tracking the usage of information in a proof.
The analysis determines model components that could be mutated, i.e. those that were overspecified in the original formula. To demonstrate the utility of this technique, we develop for the proof calculus which handles safety-critical applications. The proof tree in Fig. <ref> is the translation of a proof into .

§ PRELIMINARIES

This section sets the stage for , a refinement of the sequent proof calculus that determines admissible mutations for a formula while tracing its proof.
We embellish sequents with annotations, introducing usage-aware sequents $\atomlabel{\vec{i}}{\Gamma} \vdashu{\chi}{\Sigma} \atomlabel{\vec{j}}{\Delta}$. The annotations $\color{red}\vec{i}, \vec{j}, \color{blue}\chi, \Sigma$, e.g. in Fig. <ref>, facilitate data-flow analysis throughout a proof where $\color{blue}\chi\color{black}$ is the input and $\color{blue}\Sigma\color{black}$ is the output.

§.§ Atoms and Labels

An atom is an atomic statement or an atomic formula. Note that the ODE $x' = f(x)$ is atomic whereas $x' = f(x) \& Q$ is not due to the domain constraint $Q$. In Fig. <ref>, $x > 100$, $v - gT > - \sqrt{g/r_{op}}$, and $r:=r_{op}$ are examples of atoms whereas $\text{ODE}$ is not due to the combination of equations.

\begin{align*}
\text{atom} &::= \text{true} \mid \text{false} \mid e \sim d \mid p(e_1 \dots e_k) \mid x := e \mid x := * \mid x' = f(x)
\end{align*}

We extend the syntax of formulas and statements to include labels that serve as identifiers to these atoms.
Each atom in a formula gets a unique label and the propagation of labels throughout a proof tree allows us to track atom usage. Labels in the conclusion of a proof (i.e. the input model) are distinct from each other even if the same atom occurs multiple times. We define labeling as follows. The single label $\color{red}l$ labels an atom, and $\color{red}{\vec{l}}$, $\color{red}\vec{l}_1$, $\color{red}\vec{l}_2$ are sets of labels where $\color{red}\vec{l}=\vec{l}_1\cup\vec{l}_2$. The set $\color{red}\vec{l}$ refers to the set of all labels in a non-atomic statement or formula $\atomlabel{\vec{l}}{P}$.

\begin{align*}
\atomlabel{\vec{l}}{\alpha}, {\beta} ::=\, &\atomlabel{l}{x := e} {\kern-0.20em}
\mid \atomlabel{l}{x := *} {\kern-0.20em}
\mid {\atomlabel{l_1}{x' = f(x) \& \atomlabel{\vec{l}_2}{Q}}} {\kern-0.20em}
\mid \, ?\atomlabel{\vec{l}}{Q} {\kern-0.20em}
\mid {\atomlabel{\vec{l}_1}{\alpha};\atomlabel{\vec{l}_2}{\beta}} {\kern-0.20em} \mid (\atomlabel{\vec{l}}{\alpha})^* {\kern-0.20em} \mid {\atomlabel{\vec{l}_1}{\alpha}\cup\atomlabel{\vec{l}_2}{\beta}}\\
\atomlabel{\vec{l}}{P,Q} ::=\, &\atomlabel{l}{\text{true}} \mid \atomlabel{l}{\text{false}} \mid \atomlabel{l}{e \sim d}
\mid \atomlabel{l}{p(e_1,\dots,e_k)}
\mid \neg \atomlabel{\vec{l}}{P}
\mid {\atomlabel{\vec{l}_1}{P} \bowtie \atomlabel{\vec{l}_2}{Q}}
\mid  \forall x\, \atomlabel{\vec{l}}{P} \\
&\mid  \exists x\, \atomlabel{\vec{l}}{P}
\mid  {[\atomlabel{\vec{l}_1}{\alpha}] \atomlabel{\vec{l}_2}{P}}
\mid  {\langle\atomlabel{\vec{l}_1}{\alpha}\rangle \atomlabel{\vec{l}_2}{P}}
\end{align*}

Labels in Fig. <ref> are denoted in red. In the definition of $I(x,v)$, the labels $\color{red}i_5$, $\color{red}i_6$, $\color{red}i_7$, $\color{red}u_1$ identify the atoms $x \geq 0$, $v < 0$, $v > -\sqrt{g/r_{op}}$, $x > -1$, respectively.

§.§ Labeling Cut Atoms: Old or New?

Some rules (e.g. M:loop, M:cut, M:dC which we will see in Sec. <ref>) cut atoms into the proof. These atoms could either arise elsewhere or be new. To facilitate label tracking, we introduce $\phi$ labels
. The label $\phi(\vec{k},\vec{l})$  decides whether each atom in a cut is new or already appears elsewhere in the formula. In the former case, the atom deserves a fresh label chosen from the second argument set $\color{red}\vec{l}\color{black}$. In the latter, the atom preserves the appropriate label used for other occurrences of that atom, i.e. from the first argument set $\color{red}\vec{k}\color{black}$. We define the label $\phi_i(\vec{k},\vec{l})$  for a single atom below.

if  k C_i  (for some $\color{red}k\color{black} \in \color{red}\vec{k}$)

else  (for some $\color{red}l \color{black}\in \color{red}\vec{l}$)

We write $k \labels C_i$ if the atom labeled by $k$ and $C_i$ are syntactically equal, and $k$ is the labeling context, i.e. $k$ knows which atom it labels. When the labeling context contains multiple identical atoms, the cut is cross-referenced by each of these labels. We introduce the mechanism that handles cross-labeling in Sec. <ref>.

For example, the loop invariant $I(x,v)$ in Fig. <ref> uses $\phi$ labels. Initially, the labels of $I(x,v)$ are given by $\color{red}\phinode{ }{\vec{i}}{\vec{u}}$ where $\color{red}\vec{i}$ are the labels of $A$ and $\color{red}\vec{u}$ are fresh labels. For each atom in $I(x,v)$, $\phi$ computes the appropriate label $\color{red}\phinode{i}{\vec{i}}{\vec{u}}$. Since $x \geq 0$ appears in $A$, we reuse its corresponding label $\color{red}i_5$, i.e. $\color{red}\phinode{1}{\vec{i}}{\vec{u}}\color{black} = \color{red}i_5$. Analogously, the labels of $v < 0$ and $v > -\sqrt{g/r_{op}}$ in $A$ are $\color{red}i_6$ and $\color{red}i_7$, i.e. $\color{red}\phinode{2}{\vec{i}}{\vec{u}}\color{black} = \color{red}i_6$ and $\color{red}\phinode{3}{\vec{i}}{\vec{u}}\color{black} = \color{red}i_7$. The atom $x > -1$, however, does not appear in the labeling context $A$. It is newly cut into the proof, and hence deserves a fresh label $\color{red}\phinode{4}{\vec{i}}{\vec{u}}\color{black} = \color{red}u_1$ which is drawn from a supply of fresh labels $\color{red}\vec{u}$.

§.§ Tracking Label Sets

The ultimate goal of the data-flow analysis is to determine which atoms must remain unchanged and which ones can be mutated while preserving the proof. In this work, we consider three kinds of mutations— $\color{violet}id$, $\color{violet}W$, and $\color{violet}R$, which are written in violet.

When applied, $\color{violet}id$ produces an atom identical to the original whereas $\color{violet}R$ indicates that an atom may be completely removed from a formula while maintaining the validity of that formula. Lastly, $\color{violet}W$ indicates that an atom may be generalized to encompass a wider range of states while maintaining validity. For example, in the sequent $I(x_0,v_0), L(x_0,v_0), t = 0, v = v_0 \vdash -g + rv^2 \geq -g$ of Fig. <ref>, the more general atom $x_0 \geq 0$ could replace $x_0 > 100$, and the proof still succeeds (in fact, $x_0 > 100$ could be entirely removed).

To facilitate the data-flow analysis, usage-aware sequents track sets $\color{blue}\chi$, $\color{blue}\Sigma$ containing labels that each track a set of mutations. We write mutation-tracking labels as $\color{red}l_{\color{violet}\mathcal{M}}$ where $\color{violet}\mathcal{M}$ is the set of mutations admissible for the atom labeled by $\color{red}l$. For example, we write $\color{red}l_{\color{violet}\{id, W, R\}}$ if $\color{violet}id$, $\color{violet}W$, and $\color{violet}R$ are all admissible for $\color{red}l$, or $\color{red}\any{l}$ as shorthand because any mutation is permitted. Labels like $\color{red}l$ identify atoms in a formula, and the goal of the analysis is to solve for their mutation sets $\color{violet}\mathcal{M}$.

We define set difference and merge over sets of mutation-tracking labels. Set difference $\color{blue}\Sigma\color{black} \setminus \color{blue}\{\color{red}{l}\color{blue}\}$ discards all occurrences of a label $\color{red}l$ from a set $\color{blue}\Sigma$ no matter what mutation, i.e. $\color{blue}\Sigma \color{black}\setminus \color{blue}\{\color{red}l\color{blue}\} \color{black}= \color{blue}\Sigma \color{black}\setminus \color{blue}\{\color{red}l_{\color{violet}\mathcal{M}}\color{black}: \; \text{for any} \; \color{violet}\mathcal{M}\color{blue}\}$.

The union $\cupm$ merges output sets from different proof branches such that $\color{blue}\Sigma_1 \cupm \Sigma_2$ contains all labels of $\color{blue}\Sigma_1$ and $\color{blue}\Sigma_2$. Labels track mutation sets that are the set intersection of each label's respective mutation set in $\color{blue}\Sigma_1$ and $\color{blue}\Sigma_2$.

Letting $\color{blue}\Sigma_1 \color{black}= \color{red}i_{\color{violet}\mathcal{M}} \color{black}\cup \color{blue}\Sigma'_1$ and $\color{blue}\Sigma_2 \color{black}= \color{blue}\color{red}i_{\color{violet}\mathcal{N}} \color{black}\cup \color{blue}\Sigma'_2$ for sets $\color{blue}\Sigma'_1$ and $\color{blue}\Sigma'_2$ such that $\color{red}i \color{black}\notin \color{blue}\Sigma'_1\color{black}, \color{blue}\Sigma'_2$, we define $\cupm$ as follows:

\begin{align*}
\color{blue}\Sigma_1 \color{black}\cupm \color{blue}\Sigma_2 \color{black}&= \color{red}i_{\color{violet}\mathcal{M} \cap \mathcal{N}} \color{black}\cup \left(\color{blue}\Sigma'_1 \color{black}\cupm \color{blue}\Sigma'_2\right) &(1)\\
\color{blue}\Sigma_1 \color{black}\cupm \color{blue}\Sigma'_2 \color{black}&= \color{red}i_{\color{violet}\mathcal{M}} \color{black}\cup \color{black}\left(\color{blue}\Sigma'_1 \color{black}\cupm \color{blue}\Sigma'_2\color{black}\right) &(2) \\
\color{blue}\Sigma'_1 \color{black}\cupm \color{blue}\Sigma_2 \color{black}&= \color{red}i_{\color{violet}\mathcal{N}} \color{black}\cup \left(\color{blue}\Sigma'_1 \color{black}\cupm \color{blue}\Sigma'_2\right) &(3)
\end{align*}

When labels between output sets are disjoint, $\cupm$ is treated as a set union, as in (2) and (3). Otherwise, the label sets are merged by (1) which computes the set intersection of their mutation sets, thus retaining only the mutations that all branches agree on. For example, consider $\color{blue}\Sigma_1 \color{black}= \color{blue}\{\color{red}l_{\color{violet}id}\color{black}, \any{\color{red}m}\color{black}, \color{red}n_{\color{violet}\{id, W\}}\color{black}\color{blue}\}$ and $\color{blue}\Sigma_2 \color{black}= \color{blue}\{\any{\color{red}l}\color{black}, \color{red}m_{\color{violet}id}\color{black}, \any{\color{red}o}\color{black}\color{blue}\}$. The label $\color{red}l$ appears in both $\color{blue}\Sigma_1$ and $\color{blue}\Sigma_2$. By (1), these occurrences $\color{red}l_{\color{violet}id}$ and $\any{\color{red}l}$ merge and produce the combined mutation set $\color{violet}id$ because $\color{violet}id \color{black}\cap \color{violet}any \color{black}= \color{violet}id \color{black}\cap \color{violet}\{id, W, R\} \color{black}=\color{violet}id$. Similarly, the occurrences of $\color{red}m$ merge to produce the combined mutation set $\color{violet}id$. The label $\color{red}n$ appears in $\color{blue}\Sigma_1$ but not in $\color{blue}\Sigma_2$, so $\color{red}n_{\color{violet}\{id, W\}}\color{black}$ gets added to the final set by (2). Analogously, $\any{\color{red}o}\color{black}$ gets added to the final set by (3). Therefore, $\color{blue}\Sigma_1 \color{black}\cupm \color{blue}\Sigma_2 \color{black}= \color{blue}\{\color{red}l_{\color{violet}id}\color{black}, \color{red}m_{\color{violet}id}\color{black}, \color{red}n_{\color{violet}\{id, W\}}\color{black}, \any{\color{red}o}\color{black}\color{blue}\}$.

§.§ Applying Mutations

To apply mutations, we define the mutation operator $\mu_{\color{blue}\Sigma}$ for formulas that chooses a single mutation for each label in $\color{blue}\Sigma$.

Rigorously, we define a choice of $\mu_{\color{blue}\Sigma}$ as $\mu_{\color{blue}\Sigma} = \color{blue}\{\color{red}l_{\color{violet}m} \mid \color{red}l_{\color{violet}\mathcal{M}} \color{blue}\in \Sigma, \color{violet}m \color{blue}\in \mathcal{M}\color{blue}\}$.

For example, if $\color{blue}\Sigma \color{black}= \color{blue}\{\color{red}i_{\color{violet}id}\color{black}, \any{\color{red}j}\color{blue}\}$, one such choice of $\mu_{\color{blue}\Sigma}$ could be $ \color{blue}\{\color{red}i_{\color{violet}id}\color{black}, \color{red}j_{\color{violet}W}\color{blue}\}$, whereas $\color{blue}\{\color{red}j_{\color{violet}W}, \color{red}j_{\color{violet}R}\color{blue}\}$ is unacceptable because $\color{violet}W$ and $\color{violet}R$ conflict and a choice of mutation for label $\color{red}i$ is not included.

As shown in Fig. <ref>, $\mu_{\color{blue}\Sigma}$ maps statements to statements, and formulas to formulas, performing a recursive traversal until it reaches the atoms.

At the atomic level (Fig. <ref>), $\mu_{\color{blue}\Sigma}$ either skips over “atom” if the relevant label $\color{red}l$ is not in the set $\color{blue}\Sigma$, if the mutation is $\color{violet}id$, or if “atom” is true or false.

Otherwise, it applies mutations: $\color{violet}R$ replaces formulas with “true” (uninformative assumption) and programs with “?true” (program without effect). Mutation $\color{violet}W$ translates $e > d$ to $e \geq d$, or to $e > f$ for a term $f$ such that the replacement of $e > d$ with $e > f$ in a formula preserves its proof (and similarly for $e \geq d$). The choice of term $f$ is a customizable part of the framework. In this work, we consider a limited set of mutations. Which mutations to consider overall is a separate question that is not treated here.

\begin{align*}
\mu_{\color{blue}\Sigma} &: \mathit{Stmt} \to \mathit{Stmt},\mathit{Fml} \to \mathit{Fml} \\
\mu_{\color{blue}\Sigma}(\lnot P) &\triangleq \lnot \mu_{\color{blue}\Sigma}(P) \\
\mu_{\color{blue}\Sigma}(P \bowtie Q) &\triangleq \mu_{\color{blue}\Sigma}(P) \bowtie \mu_{\color{blue}\Sigma}(Q) &\text{where}~{\bowtie}\in\{\land,\lor,\rightarrow,\leftrightarrow\}\\
\mu_{\color{blue}\Sigma}(\mathcal Q\, x \, P) &\triangleq \mathcal Q\, x \, \mu_{\color{blue}\Sigma}(P) &\text{where}~{\mathcal Q}\in\{\forall, \exists\}\\
\mu_{\color{blue}\Sigma}(\lstrike\alpha\rstrike P) &\triangleq \lstrike\mu_{\color{blue}\Sigma}(\alpha)\rstrike \mu_{\color{blue}\Sigma}(P) &
\text{where}~{\lstrike\cdot\rstrike}\in\{\left[\cdot\right], \langle\cdot\rangle\} \\
\mu_{\color{blue}\Sigma}(?Q) &\triangleq \;?\mu_{\color{blue}\Sigma}(Q) \\
\mu_{\color{blue}\Sigma}(\alpha\triangleright\beta) &\triangleq \mu_{\color{blue}\Sigma}(\alpha) \triangleright \mu_{\color{blue}\Sigma}(\beta) &
\text{where}~{\triangleright}\in\{\cup, ;\} \\
\mu_{\color{blue}\Sigma}(\alpha^*) &\triangleq \mu_{\color{blue}\Sigma}(\alpha)^* \\
\mu_{\color{blue}\Sigma}(x' = f(x) \, \& \, Q) &\triangleq x' = f(x) \,\& \,\mu_{\color{blue}\Sigma}(Q) &\quad{\text{if} \, \color{red}l_{\color{violet}\mathcal{M}} \color{black}\notin \color{blue}\Sigma \, \color{black}\text{for all}\, \color{violet}\mathcal{M} \; \color{black}\text{and} \; \atomlabel{l}{x' = f(x)}}
\end{align*}

Definition of $\mu_{\color{blue}\Sigma}$ for non-atomic formulas and statements

In the example sequent above, the $\color{violet}W$ mutation of $\atomlabel{l}x > 100$ corresponds to replacing all occurrences of $\atomlabel{l}x > 100$ in the formula with $x \geq 0$, for which we write $\mu_{\color{red}l_{\color{violet}W}}(x > 100) \equiv x \geq 0$. Alternatively, the $\color{violet}R$ mutation of $x > 100$ corresponds to replacing all occurrences of $\atomlabel{l}x > 100$ in the formula with “true” because $x > 100$ is a formula. In this case, we write $\mu_{\color{red}l_{\color{violet}R}}(x > 100) \equiv \text{true}$.

We write $\mu_{\color{blue}\Sigma}(\Gamma \vdash \Delta)$ for $\mu_{\color{blue}\Sigma}(P_1), \dots, \mu_{\color{blue}\Sigma}(P_n) \vdash \mu_{\color{blue}\Sigma}(Q_1), \dots, \mu_{\color{blue}\Sigma}(Q_m)$ where $P_i \in \Gamma$ for $1 \leq i \leq n$ and $Q_j \in \Delta$ for $1 \leq j \leq m$.

Statements in Fig. <ref> are accompanied by the side condition $\vars{\mu_{\color{blue}\Sigma}(\alpha)} \subseteq \vars{\alpha}$
enforcing that mutations do not introduce new variables which is important for axioms that constrain variables in a formula.
The definition of $\mu$ could be extended with any mutation if a proper semantic definiton is provided and proved sound.

Generalizations to systems of differential equations follow accordingly.

\begin{align*}
\mu_{\color{blue}\{l_{m}\} \cup \Sigma}(e = d) &\triangleq \begin{cases} e = d  \; &\quad{\text{if} \; m = {\color{violet}id}}   \\
e = f  \; &\quad{\text{if} \; m = {\color{violet}W}}   \\
\text{true}  \; &\quad{\text{if} \; m = {\color{violet}R}}   \\
\end{cases}  \qquad\qquad\qquad\qquad\;\;\;\; \text{where} \; \atomlabel{l}{e = d} \\
\mu_{\color{blue}\{l_{m}\} \cup \Sigma}(e \;\sim \;d) &\triangleq \begin{cases} e \;\dot\sim\; d  \; &\quad{\text{if} \; m = {\color{violet}id}}   \\
e \geq f  \; &\quad{\text{if} \; m = {\color{violet}W}}   \\
\text{true}  \; &\quad{\text{if} \; m = {\color{violet}R}}   \\
\end{cases}  \qquad\quad\;\;\; \text{where} \; \atomlabel{l}{e \;\sim \;d}, \; \sim \in \{>,\geq\} \\
% \mu_{\{l_{m}\} \cup \Sigma}(e \geq d) &\triangleq
%          \begin{cases} e \geq d  \; &\quad{\text{if} \; m = {id}}   \\
%                        e \geq f  \; &\quad{\text{if} \; m = {W}}   \\
%                        true  \; &\quad{\text{if} \; m = {R}}   \\
%          \end{cases}  \;\; &\text{, where} \; \atomlabel{l}{e \geq d} \\
\mu_{\color{blue}\{l_{m}\} \cup \Sigma}(p(e_1 \dots e_k)) &\triangleq \begin{cases} p(e_1 \dots e_k)  \; &\quad{\text{if} \; m = \color{violet}{id}, {W}}   \\
\text{true}  \; &\quad{\text{if} \; m = {\color{violet}R}}   \\
\end{cases}  \qquad\quad\;\; \text{where} \; \atomlabel{l}{p(e_1 \dots e_k)} \\
\mu_{\color{blue}\{l_{m}\} \cup \Sigma}(x := e) &\triangleq \begin{cases} x := e  \; &\quad{\text{if} \; m = {\color{violet}id}}   \\
x := f  \; &\quad{\text{if} \; m = {\color{violet}W}}   \\
?\text{true}  \; &\quad{\text{if} \; m = {\color{violet}R}}   \\
\end{cases}  \qquad\qquad\qquad\qquad\;\; \text{where} \; \atomlabel{l}{x := e} \\
\mu_{\color{blue}\{l_{m}\} \cup \Sigma}(x := *) &\triangleq \begin{cases}
x := *  \; &\quad{\text{if} \; m = \color{violet}{id}, {W}}   \\
?\text{true}  \; &\quad{\text{if} \; m = {\color{violet}R}}   \\
\end{cases}  \qquad\qquad\qquad\quad\;\; \text{where} \; \atomlabel{l}{x := *} \\
\mu_{\color{blue}\{l_{m}\} \cup \Sigma}(x' = f(x) \; \& \; Q) &\triangleq \begin{cases} x' = f(x) \; \& \; \mu_{\color{blue}\Sigma}(Q)  \; &\quad{\text{if} \; m = \color{violet}{id}, {W}}   \\
? \mu_{\color{blue}\Sigma}(Q)  \; &\quad{\text{if} \; m = {\color{violet}R}}   \\
\end{cases}  \;\; \text{where} \; \atomlabel{l}{x' = f(x)} \\
\mu_{\color{blue}\Sigma}(\text{atom}) &\triangleq \text{atom} \; \quad{\text{if} \;{l_{\color{violet}\mathcal{M}}} \notin \color{blue}\Sigma\color{black} \, \text{for all} \, \color{violet}\mathcal{M} \; \color{black}\text{and} \; \atomlabel{l}{\text{atom},} \; \text{or atom$\,\in \{\text{true},\text{false}\}$} }&
\end{align*}

Definition of $\mu_\Sigma$ for atoms

In a usage-aware sequent $\atomlabel{\vec{i}}{\Gamma} \vdashu{\chi}{\Sigma} \atomlabel{\vec{j}}{\Delta}$, the annotations $\color{red}\vec{i}, \vec{j}$ are labels and $\color{blue}\chi\color{black}, \color{blue}\Sigma$ are sets of labels that help track atom usage. Each atom in a usage-aware sequent has a label $\color{red}\vec{i}\color{black}, \color{red}\vec{j}$ that the analysis uses to track its propagation throughout a proof. Superscript $\color{blue}\chi$ is an input label set to be preserved. It is either provided by the user or produced earlier in the analysis. Subscript $\color{blue}\Sigma$ is an output label set that tracks which mutations are admissible for specific atoms in a given formula.

§ USAGE-AWARE PROOF CALCULUS ()

In this section, we introduce ,
a proof calculus that annotates the proof rules with labels and label sets. preserves the structure of the proof rules while determining label usage at each proof step. We say that a label $\color{red}l$ is fresh for valid sequent $\atomlabel{\vec{i}}{\Gamma} \vdashu{\chi}{\Sigma} \atomlabel{\vec{j}}{\Delta}$ if $\color{red}l \color{black}\notin \color{blue}\chi\color{black}, \color{blue}\Sigma\color{black}, \color{red}\vec{i}\color{black}, \color{red}\vec{j}$.

Additionally, $p(x)$ is a predicate of a single free variable $x$, and $p(\bar{x})$ of free vectorial $\bar{x}$. We give a few rules to explain the mechanics of .
The full calculus can be found in Appendix <ref>.

To illustrate the connection between the input $\color{blue}\chi$
and output $\color{blue}\Sigma$, consider the rule M:id which closes a branch by propagating $\color{blue}\chi$ and $\color{blue}\vec{i},\vec{j},\vec{k},\vec{l}$ into $\color{blue}\Sigma$:

i⃗P, k⃗Γ χ{i⃗j⃗_any, k⃗_any, l⃗_any} χ j⃗P, l⃗Δ

Given an input set $\color{blue}\chi$, the computed output set is $\color{blue}\{\any{\color{red}\fuse{\vec{i}}{\vec{j}}}\color{blue}, \any{\color{red}\vec{k}}\color{blue}, \any{\color{red}\vec{l}}\color{blue}\} \cupm \chi$.

We write $\any{\color{red}\fuse{\vec{i}}{\vec{j}}}$ to mean that when applied, the labels $\color{red}\vec{i}$ and $\color{red}\vec{j}$ are allowed to take on any mutation so long as they share the same mutation.

This is required only of $\color{red}\vec{i}$ and $\color{red}\vec{j}$, the labels of $P$. Any mutations are admissible for $\Gamma$ and $\Delta$, for these could be weakened or even removed and the proof would still close by M:id.

§.§ Propositional and Quantifier Sequent Calculus Proof Rules

The rules in Fig. <ref> correspond to those of propositional sequent calculus annotated to reflect which labels were used at a given proof step.

k⃗Γ χΣ l⃗Δ, i⃗P, j⃗Q
k⃗Γ χΣ i⃗P j⃗Q, l⃗Δ
k⃗Γ, i⃗P χΣ j⃗Q,l⃗Δ
k⃗Γ χΣ i⃗P →j⃗Q,l⃗Δ
k⃗Γ χΣ i⃗P

k⃗Γ χΩ j⃗Q
k⃗Γ χΣΩ i⃗P j⃗Q
k⃗Γ χΣ l⃗Δ
i⃗P, k⃗Γ χΣi⃗ l⃗Δ
i⃗Γ, i⃗l⃗C χΣ k⃗Δ

i⃗Γ χΩ k⃗Δ, i⃗l⃗C

i⃗Γ χ(ΣΩ) ∖l⃗ k⃗Δ
( l⃗  fresh )
i⃗Γ χΣ j⃗p(y), k⃗Δ
i⃗Γ χΣ ∀x   j⃗p(x), k⃗Δ
(y ∉Γ, Δ, ∀x   p(x))
i⃗Γ χΣ j⃗p(e), k⃗Δ
i⃗Γ χΣ ∃x   j⃗p(x), k⃗Δ
(arbitrary term $e$)

Representative propositional and quantifier sequent calculus proof rules

For example, the rules M:$\lor$R and M:$\rightarrow$R each have only one premise which maintains the same labels as the conclusion, so they propagate the input $\color{blue}\chi\color{black}$ from conclusion to premise and the output $\color{blue}\Sigma\color{black}$ from premise to conclusion. In other words, there is no new information that can be obtained between premise and conclusion in these proof steps.

In Fig. <ref>, the M:$\rightarrow$R proof step simply moves the formula $A$ to the left of the turnstile while passing the output set of the premise onto the conclusion.

In the rule M:$\land$R, the labels $\color{blue}\Sigma$ were used in the proof of the first premise and the labels $\color{blue}\Omega$ were used in the proof of the second premise. Recalling that the set $\color{blue}\Sigma \cupm \Omega$ is computed by merging the label sets $\color{blue}\Sigma$ and $\color{blue}\Omega$, M:$\land$R concludes that the labels $\color{blue}\Sigma \cupm \Omega$ are used in the proof.

In Fig. <ref>, M:$\land$R merges the output sets from (3c) and the branch that proves $\atomlabel{i_5,i_6,i_7,u_1}{{I(x,v)}}, \atomlabel{j,k,l}{{L(x,v)}}, \atomlabel{n}t= 0 \vdashu{\chi}{\chi \cupm \Theta} \left[\atomlabel{\vec{o}}\text{ODE} \& \atomlabel{\vec{p}}Q\right] \atomlabel{i_7}v > -\sqrt{g/r_{op}}$. These output sets are $\color{blue}\chi \cupm \{{\color{red}\fuse{i_5}{p_2}}_{\color{violet}\{id,W\}}\color{blue},\any{\color{red}\fuse{i_6}{p_3}}\color{blue}, \any{\color{red}j}\color{blue}, \any{\color{red}k}\color{blue}, \any{\color{red}l}\color{blue}, \any{\color{red}n}\color{blue}, \any{\color{red}\{p_1\}}\color{blue},\\ \any{\color{red}\vec{o}}\color{blue},\any{\color{red}\{u_1\}}\color{blue}, \any{\color{red}\{i_7\}}\color{blue}\}$ and $\color{blue}\chi \cupm \Theta$, respectively. The merged set retains $\color{blue}\chi$ as it is common to both of these sets. The output set of (3c) is a subset of the labels present in the other output set but with more liberal mutations. Thus, the final output set contains the already more constrained $\color{blue}\Theta$, i.e. $\color{blue}\chi \cupm \Theta$ overall.

The rule M:cut corresponds to cut of propositional sequent calculus. The label of formula $C$ is $\color{red}\phinode{}{\vec{i}}{\vec{l}}$ to account for new or previously seen atoms. New atoms deserve a fresh label, and those previously seen maintain a label consistent with $\Gamma$, as suggested by the first premise. The conclusion of M:cut merges the output sets of the two premises and discards fresh labels $\color{red}\vec{l}$ from the prevailing output set as these were used to analyze the cut and yield no valuable information before the cut.

The rule M:WL says that if there exists a proof of the premise, then there exists a proof of the conclusion independent of the assumption $\atomlabel{\vec{i}}{P}$. records this observation by asserting the output set to be $\color{blue}\Sigma \cupm \any {\color{red}\vec{i}}$ where $P$ could take on any mutation while maintaining validity. The rules M:$\forall$R and M:$\exists$R follow a propagation of label sets similar to M:$\lor$R. The rule M:$\forall$R eliminates the quantifier $\forall x$ by binding a variable $y$ to every free instance of $x$ in $p(x)$. The restriction $y \notin \Gamma, \Delta, \forall x \; p(x)$ ensures that the concretizing variable $y$ does not clash with variables already present in the sequent. From conclusion to premise, the formula $p(x)$ transforms into $p(y)$, maintaining the same label $\color{red}\vec{j}$. Analogously, the rule M:$\exists$R eliminates an existential quantifier from conclusion to premise by instantiating $x$ with an arbitrary term $e$. is also equipped with first-order axioms that provide an alternative way of eliminating quantifiers.

§.§ Sequent Calculus Proof Rules

In Fig. <ref>, we introduce the sequent calculus proof rules that characterize how hybrid programs are used in proofs.

k⃗Γ χΣ k⃗l⃗J, i⃗Δ

k⃗l⃗J χΩ j⃗P

k⃗l⃗J χΘ [m⃗α] k⃗l⃗J

k⃗Γ χ(ΣΩΘ) ∖l⃗ [m⃗α^*]j⃗P,i⃗Δ
( l⃗  fresh )
i⃗Γ_const χΩ k⃗P, l⃗Δ_const
i⃗Γ χΩj⃗ [j⃗α] k⃗P, l⃗Δ
i⃗Γ χΩ m⃗C(l⃗j⃗Q), k⃗Δ

χΣ l⃗j⃗Q ↔l⃗P
i⃗Γ χ(ΩΣ) ∖j⃗ m⃗C(l⃗P), k⃗Δ
( j⃗  fresh )

Representative sequent calculus proof rules

For example, in the rule M:GVR, $\atomlabel{\vec{j}}{\alpha}$ is not in the proof of the premise, so the output set is $\color{blue}\Omega \cupm \any{\color{red}\vec{j}}\color{blue}$. Additionally, $\Gamma_\text{const}$ and $\Delta_\text{const}$ are $\Gamma$ and $\Delta$ restricted to formulas whose free variables do not intersect with the bound variables of $\alpha$. We label both $\Gamma$ and $\Gamma_\text{const}$ with the same $\color{red}\vec{i}$ because the labels of $\Gamma_\text{const}$ draw from the labels $\color{red}\vec{i}$ in the conclusion.

The rule M:loop provides an induction proof of a repeating program by introducing a loop invariant $J$. A proof of the conclusion exists if the loop invariant (1) holds under the assumptions $\Gamma$, (2) implies the post condition, and (3) holds after one loop iteration provided that it held previously. These requirements correspond to the premises of M:loop, and the output set of the conclusion is obtained by merging the outputs from these three premises, excluding fresh labels. As with M:cut, the loop invariant is labeled by $\color{red}\phinode{}{\vec{k}}{\vec{l}}$, indicating that atoms occurring in $\Gamma$ could appear in the loop invariant.

In Fig. <ref>, the proof step M:loop forks the proof into branches (1), (2), and (3), each corresponding to one of these conditions. The loop invariant is given by formula $I(x,v)$ which we label by $\color{red}\phi(\vec{i},\vec{u})$. The output set $\color{blue}\chi \cupm \Omega$ is the (simplified) merged outputs of proof branches (1), (2), and (3).

The contextual equivalence rule M:CER applies the equivalence axioms of the next section to replace formulas by their equivalents in any context by using a predicate $C(\cdot)$ that takes formulas as arguments. As with M:loop, M:CER analyzes one proof branch at a time. As usual, each atom in the conclusion is assigned a unique label where each occurrence of $P$ in $C(\cdot)$ is labeled by $\color{red}\vec{l}$. The second premise gives an equivalence between formulas $P$ and $Q$, reusing the same labels for $P$. We use $\phi$ labels for $Q$ because some of these atoms are spawned by $P$ while others are new. The first premise plugs in $Q$ for all occurrences of $P$ in the original formula. $\Gamma$, $C$, and $\Delta$ carry the same labels from the conclusion.

§.§ Axioms

In Fig. <ref>, we give selected axioms of . In proofs, these axioms are used in combination with the proof rules for contextual equivalence like M:CER.

\begin{align*}
\quad{\text{\color{violet}M:\color{black}$[?]$}} \;\; &\vdashu{\chi}{\{\any{\color{blue}\vec{j}}, \any{\color{blue}\vec{k}}\color{blue}\} \cupm \chi} [?\atomlabel{\vec{j}}{Q}]\atomlabel{\vec{k}}{P} \leftrightarrow \left(\atomlabel{\vec{j}}{Q} \to \atomlabel{\vec{k}}{P}\right) & \\
\quad{\text{\color{violet}M:\color{black}$[{;}]$}} \;\; &\vdashu{\chi}{\{\any{\color{blue}\vec{i}}, \any{\color{blue}\vec{j}}, \any{\color{blue}\vec{k}}\color{blue}\} \cupm \chi} [\atomlabel{\vec{i}}{\alpha};\atomlabel{\vec{j}}{\beta}]\atomlabel{\vec{k}}{P} \leftrightarrow [\atomlabel{\vec{i}}{\alpha}][\atomlabel{\vec{j}}{\beta}]\atomlabel{\vec{k}}{P} & \\
\quad{\text{\color{violet}M:\color{black}$\langle\cdot\rangle$}} \;\; &\vdashu{\chi}{\{\any{\color{blue}\vec{j}}, \any{\color{blue}\vec{k}}\color{blue}\} \cupm \chi} \neg \left[\atomlabel{\vec{j}}{\alpha}\right]\neg \atomlabel{\vec{k}}{P} \leftrightarrow \langle \atomlabel{\vec{j}}{\alpha} \rangle \atomlabel{\vec{k}}{P} & \\
\quad{\text{\color{violet}M:\color{black}$[\cup]$}} \;\; &\vdashu{\chi}{\{\any{\color{blue}\vec{i}}, \any{\color{blue}\vec{j}}, \any{\fuse{\vec{k}}{\vec{l}}}\color{blue}\} \cupm \chi} [\atomlabel{\vec{i}}{\alpha} \cup \atomlabel{\vec{j}}{\beta}] \atomlabel{\fuse{\vec{k}}{\vec{l}}}{P} \leftrightarrow \left([\atomlabel{\vec{i}}{\alpha}]\atomlabel{\vec{k}}{P} \land [\atomlabel{\vec{j}}{\beta}]\atomlabel{\vec{l}}{P}\right) & \\
%\quad{\text{\color{violet}M:\color{black}$[']$}} \;\; &\vdash^\chi_{\{\vec{m}_{id}, \vec{n}_{id}, \vec{k}_{any}, \vec{j}_{any}, \vec{l}_{any}\} \cupm \chi} [\atomlabel{{k}}x' = f(x) \;\& \atomlabel{\vec{j}}q(x)] \atomlabel{\vec{l}}p(x) &\\
% &\leftrightarrow \left(\forall \atomlabel{\vec{m}}{t {\geq} 0} \;((\forall \atomlabel{\vec{n}}{0 {\leq} s {\leq} t} \; \atomlabel{\vec{j}}q(x(s))) \to [\atomlabel{{k}}x:=x(t)]\atomlabel{\vec{l}}p(x))\right) &\quad{(\text{if } x'(t) = f(x(t)))}\\
\quad{\text{\color{violet}M:\color{black}V}} \;\; &\vdashu{\chi}{\{\any{\color{blue}\vec{j}}, \any{\color{blue}\vec{k}}\color{blue}\} \cupm \chi} \atomlabel{\vec{k}}{p} \rightarrow \left[\atomlabel{\vec{j}}{\alpha}\right]\atomlabel{\vec{k}}{p} \qquad\qquad\qquad {(\text{$FV(p) \cap BV(\alpha) = \emptyset$})} \\
\quad{\text{\color{violet}M:\color{black}$[:=]_1$}} \;\; &\vdashu{\chi}{\{{\color{blue}j}_{\color{violet}id}, \any{\color{blue}\vec{k}}\color{blue}\} \cupm \chi} [\atomlabel{j}{x:=e}\;] \atomlabel{\vec{k}}{p(x)} \leftrightarrow \atomlabel{\vec{k}}{p(e)} \qquad{(x \in FV(p(x)))} \\
\quad{\text{\color{violet}M:\color{black}$[:=]_2$}} \;\; &\vdashu{\chi}{{\{\any{\color{blue}j}, \any{\color{blue}\vec{k}}\color{blue}\} \cupm \chi}} [\atomlabel{j}{x:=e}\;] \atomlabel{\vec{k}}{p} \leftrightarrow \atomlabel{\vec{k}}{p} \qquad\qquad {(x \notin FV(p))}
%    \quad{\text{\color{violet}M:\color{black}$[{:}{*}]_1$}} \;\; &\vdashu{\chi}{{\{j_{id}, \vec{k}_{any}\} \cupm \chi}} [\atomlabel{j}{x:=*}\;] \atomlabel{\vec{k}}{p(x)} \leftrightarrow \forall x \atomlabel{\vec{k}}{p(x)} \;\; &\quad{x \in FV(p(x))} \\
%    \quad{\text{\color{violet}M:\color{black}$[{:}{*}]_2$}} \;\; &\vdashu{\chi}{{\{j_{any}, \vec{k}_{any}\} \cupm \chi}} [\atomlabel{j}{x:=*}\;] \atomlabel{\vec{k}}{p} \leftrightarrow \atomlabel{\vec{k}}{p} &\quad{x \notin FV(p)}
\end{align*}

Representative axioms

When M:[?] is used with contextual equivalence, the same labels appear between conclusion and proof premise, and retains all possible mutations in this premise to capture the result of the other proof branch in the prevailing output set. In other words, both sides of M:[?] retain the same labels, and similarly for M:[;], which gives the sequencing rule for hybrid programs enveloped in box modalities, and M:$\langle\cdot\rangle$, which translates between modalities by duality.

The axiom M:$\left[\cup\right]$ reasons about non-deterministic choice in a program. Since M:$\left[\cup\right]$ is bidirectional, it may be applied in two different ways. When M:$[\cup]$ is applied in the backward direction (as shown in Fig. <ref> (B)), the conclusion of the proof is $[\atomlabel{\vec{i}}{\alpha} \cup \atomlabel{\vec{j}}{\beta}] \atomlabel{\vec{k}}{P}$, and the premise spawned by contextual equivalence is $[\atomlabel{\vec{i}}{\alpha}] \atomlabel{\vec{k}}{P} \land [\atomlabel{\vec{j}}{\beta}] \atomlabel{\vec{k}}{P}$.
Alternatively, when M:$[\cup]$ is applied in the forward direction (as shown in Fig. <ref> (A)), the conclusion is $[\atomlabel{\vec{i}}{\alpha}]\atomlabel{\vec{k}}{P} \land [\atomlabel{\vec{j}}{\beta}]\atomlabel{\vec{l}}{P}$, the premise spawned by contextual equivalence only has a single occurrence of $P$ that could be labeled by either $\color{red}\vec{k}$ or $\color{red}\vec{l}$. To guarantee the preservation of the proof, $P$ takes on both labels such that the mutated atoms labeled by $\color{red}\vec{k}$ or $\color{red}\vec{l}$ in the formula are identical. Towards this, we introduce a cross-labeling scheme called fusing.

n⃗Γ χΩ m⃗C(pink[i⃗α ∪j⃗β] k⃗l⃗P), o⃗Δ

·  χ{i⃗, j⃗, k⃗l⃗} χ [i⃗α ∪j⃗β] k⃗l⃗P
↔([i⃗α]k⃗P [j⃗β]l⃗P)

n⃗Γ χΩ{i⃗, j⃗, k⃗l⃗} χ m⃗C(pink[i⃗α]k⃗P [j⃗β]l⃗P), o⃗Δ

n⃗Γ χΩ m⃗C(pink[i⃗α]k⃗P [j⃗β]k⃗P), o⃗Δ

·  χ{i⃗, j⃗, k⃗k⃗} χ [i⃗α ∪j⃗β] k⃗k⃗P
↔([i⃗α]k⃗P [j⃗β]k⃗P)

n⃗Γ χΩ{i⃗, j⃗, k⃗k⃗} χ m⃗C(pink[i⃗α ∪j⃗β] k⃗k⃗P), o⃗Δ

Using axiom M:$[\cup]$ with contextual equivalence rule M:CER

This arises when the conclusion of a proof references an identical atom multiple times while the premise only references that atom once, caused by applying axioms in a usage-aware proof. The mutations for that atom's label in the premise must transfer to all of its occurrences in the conclusion. We write $\atomlabel{\fuse{\vec{k}}{\vec{l}}}{P}$, meaning that the atoms in $P$ correspond to both labels $\color{red}\vec{k}$ and $\color{red}\vec{l}$. In label sets, $\any{\color{red}\fuse{\vec{k}}{\vec{l}}}$ means that any mutation is admissible for $\color{red}\vec{k}$ and $\color{red}\vec{l}$ as long as these mutations are identical, i.e., a programmer could choose $\color{red}\vec{k}_{\color{violet}W}$ and $\color{red}\vec{l}_{\color{violet}W}$, but not, for example, $\color{red}\vec{k}_{\color{violet}W}$ and $\color{red}\vec{l}_{\color{violet}R}$. Fusing ensures that identical mutations correspond to identical mutated atoms. The labeling $\atomlabel{\fuse{\vec{k}}{\vec{k}}}{P}$ simplifies as $\atomlabel{\vec{k}}{P}$, and $\any{\color{red}\fuse{\vec{k}}{\vec{k}}}$ is simply $\any{\color{red}\vec{k}}$. Def. <ref> states that if the fused label $\color{red}\fuse{\vec{j}}{\vec{k}}_{\color{violet}\mathcal{M}}$ appears in the output set $\color{blue}\Sigma$, then the choice of $\mu_{\color{blue}\Sigma}$ imposes that $\color{red}\vec{j}$ and $\color{red}\vec{k}$ take on the same mutation $\color{violet}m$ in $\color{violet}\mathcal{M}$.

If $\atomlabel{\vec{i}}{\Gamma} \vdashu{\chi}{\Sigma} \atomlabel{\fuse{\vec{j}}{\vec{k}}}{P}$ where ${\color{red}\fuse{\vec{j}}{\vec{k}}}_{\color{violet}\mathcal{M}}, \color{red}\vec{i}_{\color{violet}\mathcal{N}} \color{blue}\in \Sigma$ for some $\color{violet}\mathcal{M}$ and $\color{violet}\mathcal{N}$, then $\mu_{\color{blue}\Sigma} = \mu_{\color{blue}\{\color{red}\vec{i}_{\color{violet}n}, \color{red}\vec{j}_{\color{violet}m}, \color{red}\vec{k}_{\color{violet}m}\color{blue}\}}$ for all $\color{violet}m \color{black}\in \color{violet}\mathcal{M}$ and $\color{violet}n \color{black}\in \color{violet}\mathcal{N}$.

In M:$[\cup]$, the single occurrence of $P$ in the premise is cross-labeled by $\color{red}\vec{k}$ and $\color{red}\vec{l}$, and fusing enforces that the mutations on these labels agree by including $\color{red}\any{\fuse{\vec{k}}{\vec{l}}}$ in the output set of M:$[\cup]$. In Fig. <ref> (B), $[\atomlabel{\vec{i}}{\alpha} \cup \atomlabel{\vec{j}}{\beta}] \atomlabel{\fuse{\vec{k}}{\vec{k}}}{P}$ means $[\atomlabel{\vec{i}}{\alpha} \cup \atomlabel{\vec{j}}{\beta}] \atomlabel{\vec{k}}{P}$. Fusing is a nuance not needed for typical proofs with axioms like M:$[\cup]$ which transform the left-hand side into the right-hand side when moving from conclusion to premise. Here, the fused label degenerates into a single label.

Axiom M:V reasons about hybrid programs that do not bind variables in the postcondition. In particular, the formula $p$ implies $[\alpha]p$ where the bound variables in $\alpha$ are disjoint from the free variables of $p$, i.e. the variable names do not clash. This side condition is maintained even after mutation. The definition of the mutation operator $\mu_{\color{blue}\Sigma}$ from Sec. <ref> for a given set ${\color{blue}\Sigma}$ imposes the constraint that $\mu_{\color{blue}\Sigma}(\alpha)$ binds at most the variables bound in $\alpha$. Hence, the bound variables in $\mu_{\color{blue}\Sigma}(\alpha)$ are disjoint from the free variables of $p$. The axiom $[:=]_1$ enforces $x:=e$ be kept identical because $x$ appears in $p(x)$, whereas $[:=]_2$ says that $x:=e$ could be mutated in any way because $x$ does not appear in $p$.

§.§ Leaf Rules

In Fig. <ref>, we give the leaf rules of . These rules provide the base cases for the proof and the analysis; given a concrete input set, the analysis will return a concrete output set that is some function of the input set and atom labels present at that proof step.

i⃗P, k⃗Γ χ{i⃗j⃗_any, k⃗_any, l⃗_any} χ j⃗P, l⃗Δ

i⃗Γ χDA(i⃗, j⃗) χ j⃗Δ

k⃗Γ χ{i_id, k⃗_any, j⃗_any} χ itrue, j⃗Δ

i⃗Γ χDA(i⃗, j⃗) χ j⃗Δ

ifalse, k⃗Γ χ{i_id, k⃗_any, j⃗_any} χ j⃗Δ

i⃗Γ χDA(i⃗, j⃗) χ j⃗Δ

leaf rules

The rule M:id was explained above, and the rules M:$\mathbb{R}$ and M:auto take an input set $\color{blue}\chi$ and produce an output set $\color{blue}DA(\vec{i}, \vec{j}) \cupm \chi$ where $\color{blue}DA(\vec{i}, \vec{j})$ is a set of labels whose application of mutations yields a valid mutated sequent, as characterized by Def. <ref>. The first property corresponds to soundness which we will see in Sec. <ref> while the second property ensures that every label in the leaf formula is analyzed.

A naive implementation of M:$\mathbb{R}$ would involve an exponential search on top of a doubly-exponential decision procedure; for each atom in a given leaf formula, the analysis tests each mutation and selects the ones that maintain validity. However, a implementation would use the input set $\color{blue}\chi\color{black}$ to guide the analysis thus reducing search.

$\mu_{\color{blue}DA(\vec{i}, \vec{j})}$ chooses a mutation for each mutation-tracking label in the set $\color{blue}DA(\vec{i}, \vec{j})$ according to their sets of admissible mutations.

$\color{blue}DA(\vec{i}, \vec{j})$ is a set of mutation-tracking labels such that:

* $\mu_{\color{blue}DA(\vec{i}, \vec{j})}(\Gamma \vdash \Delta)$ is valid for any $\mu_{\color{blue}DA(\vec{i}, \vec{j})}$, if $\atomlabel{\vec{i}}\Gamma \vdashu{\chi}{{\chi \cupm DA(\vec{i}, \vec{j})}} \atomlabel{\vec{j}}\Delta$ is valid.

* Each label $\color{red}\vec{i}, \vec{j}$ appears in $\color{blue}DA(\vec{i}, \vec{j})$.

For example, consider the valid sequent $\atomlabel{i}{x > 1} \vdashu{\chi}{{\chi \cupm DA({i}, {j})}} \atomlabel{j}{x \geq 0}$ where $\color{blue}DA({i}, {j}) = \{\color{red}i_{\color{violet}\{id, W\}}\color{blue}, \color{red}j_{\color{violet}id}\color{blue}\}$. A choice of $\mu_{\color{blue}DA({i}, {j})}$ is $\color{blue}\{\color{red}i_{\color{violet}W}\color{blue}, \color{red}j_{\color{violet}id}\color{blue}\}$ such that $\mu_{\color{blue}\{\color{red}i_{\color{violet}W}\color{blue}, \color{red}j_{\color{violet}id}\color{blue}\}}(x > 1 \vdash x \geq 0)$ becomes $x \geq 0 \vdash x \geq 0$, supposing that $\mu_{\color{red}i_{\color{violet}W}}(x > 1) \equiv x \geq 0$.

§ EXAMPLE

In this section, we revisit the parachute example from Sec. <ref>.

The analysis begins at the base of the proof tree shown in the bottom fragment. For simplicity, we choose the input set $\color{blue}\chi$ to be $\color{blue}\emptyset$ (assume no initial constraints). The objective of the analysis is to solve for the output set. The analysis propagates $\color{blue}\chi\color{black}$ up through each proof step until it reaches the leaves. At leaf rules, the output set is computed and then passed back down the proof tree. For example, consider the branch (3h) of Fig. <ref>. The analysis at M:QE concludes that $r = r_{cl}$ and $-g + rv^2 \geq -g$ should remain untouched. The atom $-g + rv^2 \geq -g$ is spawned by $v' \geq -g t'$ which is the derivative of $v \geq v_0 - gt$ via the rule M:dI. Additionally, the analysis observes that the assignment derived from $x' = v$ is unused ($\color{violet}any$ mutation allowed), while the assignments from $v' = -g + rv^2$ and $t' = 1$ are used (only $\color{violet}id$ allowed).

All of this information is propagated back to (3a), where the rule M:$\land$R merges the two output sets from its premises. The conglomerate is passed down the proof tree. The rule M:loop merges the output sets of (1), (2), and (3), discarding any fresh labels, i.e. $\color{red}u_1$, from the output set. The output set $\color{blue}\chi \cupm \Omega$ is then passed down to M:$\rightarrow$R where it serves as the final output of the entire analysis. Since $\color{blue}\chi = \emptyset$, this reduces to $\color{blue}\Omega = \{\color{red}k_{\color{violet}id}\color{blue}, \any{\color{red}j}\color{blue}, \any{\color{red}l}\color{blue}, \any{\color{red}\{o_1\}}\color{blue}, \color{red}\{o_2\}_{\color{violet}id}\color{blue}, \color{red}\{o_3\}_{\color{violet}id}\color{blue}, \color{red}n_{\color{violet}id}\color{blue}, \color{red}\{i_7\}_{\color{violet}id}, \any{\color{red}m}\color{blue}, \color{red}\{i_5\}_{\color{violet}id}\color{blue}, \color{red}\{i_6\}_{\color{violet}id}\color{blue}, \any{\color{red}\{p_1\}}\color{blue}, \\\color{red}\{p_2\}_{\color{violet}id}\color{blue}, \color{red}\{p_3\}_{\color{violet}id}\color{blue}, \any{\color{red}\{i_1\}}\color{blue}, \any{\color{red}\{i_2\}}\color{blue}, \any{\color{red}\{i_3\}}\color{blue}, \any{\color{red}\{i_4\}}\color{blue}, \any{\color{red}\{i_8\}}\color{blue}, \color{red}\vec{q}_{\color{violet}id}\color{blue}\}$. From this, we see that atoms labelled by $\color{red}k$, $\color{red}o_2$, $\color{red}o_3$, $\color{red}n$, $\color{red}i_5$, $\color{red}i_6$, $\color{red}i_7$, $\color{red}p_2$, $\color{red}p_3$, and $\color{red}\vec{q}$ should remain unmutated, while all other atoms can take on any mutation. In particular, we conclude that the atoms labelled by $\color{red}l$ and $\color{red}j$, i.e. $x > 100$ and $v - gT > - \sqrt{g/r_{op}}$ were unused in this proof branch. As they do not appear in other proof branches, they could be weakened, or entirely removed, without impacting validity. In this way, is capable of automatically detecting atoms that were overspecified in the input model and proposing appropriate mutations.

§ METATHEORY

This section presents the metatheory of . Proofs of all results are in Appendix <ref>.

Obs. <ref> enforces that labels appearing in the conclusion of a proof are unique, or have been introduced fresh. Fresh labels typically arise in places where atoms are cut into the proof, e.g. M:cut and M:loop.

Obs. <ref> is the invariant that analyzes every atom in a formula; every label of a formula will appear in the output set. In this way, the analysis always provides some information about every atom in the formula.

Obs. <ref> expresses that the output label set $\color{blue}\Sigma$ is a super-set of the input label set $\color{blue}\chi$ up to mutations. From input to output, this means that the analysis only learns new things and records these findings in $\color{blue}\Sigma$ which retains all labels that were already in $\color{blue}\chi$.

[Labeling schema]
Labels are unique and either appear in the conclusion of a proof, or are freshly introduced throughout the proof.

[Maximal output]
In $\atomlabel{\vec{i}}\Gamma \vdashu{\chi}{\Sigma} \atomlabel{\vec{j}}{\Delta}$, the output set $\color{blue}\Sigma$ must mention at least the labels that appear in $\Gamma \vdash \Delta$.

[Output subsumes input]
In $\atomlabel{\vec{i}}{\Gamma} \vdashu{\chi}{\Sigma} \atomlabel{\vec{j}}{\Delta}$, it is the case that $\color{blue}\chi \subseteq \Sigma$. That is, $\color{blue}\Sigma$ mentions at least every label in $\color{blue}\chi$.

Obs. <ref> asserts that output set $\color{blue}\Sigma$ always contains the identity mutation $\color{violet}id$ of all labels in the local formula. That is, not mutating the formula is always a safe choice, yet strives to provide more specific mutational diagnostics where applicable.

Lemma <ref> enforces that mutations can be applied in any order, one at a time, while producing the same mutated formula.

[Identity admissibility]
If the sequent $\atomlabel{\vec{i}}{\Gamma} \vdashu{\chi}{\Sigma} \atomlabel{\vec{j}}{\Delta}$ is valid, then $\mu_{\color{blue}\{\vec{i}_{id}, \vec{j}_{id}\}}(\Gamma \vdash \Delta)$ is valid.

If $\color{blue}\Sigma \color{black}\cap \color{blue}\Omega \color{black}= \color{blue}\emptyset$, then $\mu_{\color{blue}\Sigma \cup \Omega}(\Gamma \vdash \Delta) \equiv \mu_{\color{blue}\Sigma}(\mu_{\color{blue}\Omega}(\Gamma \vdash \Delta)) \equiv \mu_{\color{blue}\Omega}(\mu_{\color{blue}\Sigma}(\Gamma \vdash \Delta))$.

The justifications of correctness exploit that additional mutational constraints could be specified without affecting the validity of a given formula. The key intuition here is that introducing more mutational constraints limits the overall pool of mutations a given atom can take on due to the semantics of merge $\cupm$. This idea is formalized in Lemma <ref> which is key to proving soundness.

If $\mu_{\color{blue}\Sigma}(\Gamma \vdash \Delta)$ is valid for all choices of $\mu_\Sigma$, then $\mu_{\color{blue}\Sigma \cupm \Omega}(\Gamma \vdash \Delta)$ is valid for all $\color{blue}\Omega$.

If $\mu_{\color{blue}\Sigma}(\Gamma \vdash \Delta)$ is valid, then $\mu_{\color{blue}\Sigma \setminus {\vec{l}}}(\Gamma \vdash \Delta)$ is valid where $\color{red}\vec{l}$ fresh for $\Gamma \vdash \Delta$.

Soundness and completeness of are given by Theorems <ref> and <ref>. Soundness means that if a formula has a proof in , then it has a proof in the sequent calculus [27]. This means that a valid formula, when mutated according to mutations found by , will still be valid.
Conversely, completeness means that if a formula has a proof in the sequent calculus, then for all input sets $\color{blue}\chi$ there exists a corresponding output set $\color{blue}\Sigma$ that can be computed by .

If $\atomlabel{\vec{i}}{\Gamma} \vdashu{\chi}{\Sigma} \atomlabel{\vec{j}}{\Delta}$, then $\mu_{\color{blue}\Sigma}(\Gamma \vdash \Delta)$ is valid for all $\mu_{\color{blue}\Sigma}$.

If $\Gamma \vdash \Delta$ is valid, then for all $\color{blue}\chi$ there exists $\color{blue}\Sigma$ such that $\atomlabel{\vec{i}}{\Gamma} \vdashu{\chi}{\Sigma} \atomlabel{\vec{j}}{\Delta}$.

The significance is that mutations suggested by can be applied to a valid formula while preserving its proof, and can analyze any formula.

§ USAGE-AWARE PROOF CALCULUS$^{+}$ ()

This section presents , a variant of   that executes sequentially rather than in parallel by reusing information determined by earlier stages of the analysis. In , each branch must determine its own mutations, merging them at the end of the analysis into a single output set.

is derivable from , but analyzes rules with multiple premises by solving for the output set of the first premise, feeding it into the input set of the next premise, and so on for all premises. The final output set is a function of the output set from the last-analyzed premise. The prototypical case is M$^+$:loop which has multiple premises, each spawning its own proof branch. The prevailing output set is simply the output of the third premise sans the fresh labels $\color{red}\vec{l}$.

k⃗Γ χΣ k⃗l⃗J, i⃗Δ

k⃗l⃗J ΣΩ j⃗P

k⃗l⃗J ΩΘ [m⃗α] k⃗l⃗J

k⃗Γ χΘ∖l⃗ [m⃗α^*]j⃗P,i⃗Δ
( l⃗  fresh )

This kind of analysis reduces search at the leaves of the proof tree where $DA$ may infer information about which mutations to test from the input set $\color{blue}\chi$, and reduces the number of merges. We provide a version of each rule in . We only show M$^+$:loop and include the full calculus in Appendix <ref>.

All other rules follow analogous reasoning, threading the output set of the preceding premise into the input set of the next premise. Rules with a single premise are identical to those of . derives from , and soundness and completeness, Theorems <ref> and <ref>, which we have proved for , extend to via Lemma <ref>.
These theorems and their proofs are in Appendix <ref>.

§ EXTENSION TO PROOF DIAGNOSTICS

In this section, we extend to record proof diagnostics which track ways in which atoms of a cut can be mutated.

To this end, we extend each applicable rule of with a set $\color{blue}\Xi\color{black}$ that tracks the fresh labels introduced in that proof step, recording the usage of freshly-cut atoms whereas they would otherwise be completely discarded by the analysis. The prototypical example is again M:loop.

k⃗Γ χΣ k⃗l⃗J, i⃗Δ

k⃗l⃗J χΩ j⃗P

k⃗l⃗J χΘ [m⃗α] k⃗l⃗J

k⃗Γ χ(ΣΩΘ) ∖l⃗ [m⃗α^*]j⃗P,i⃗Δ
( l⃗  fresh ;   Ξ= l^Σ_ℳ1 l^Ω_ℳ2 l^Θ_ℳ3)

In M:loop, $\color{blue}\Xi = \overrightarrow{l^\Sigma_{\mathcal{M}_1}} \cupm \overrightarrow{l^\Omega_{\mathcal{M}_2}} \cupm \overrightarrow{l^\Theta_{\mathcal{M}_3}}$ determines the usage of $\color{red}\vec{l}$ in each of the three branches by performing a merge across the occurrences of $\color{red}\vec{l}$ ($\color{red}\overrightarrow{l^\Sigma_{\mathcal{M}_1}}$, $\color{red}\overrightarrow{l^\Omega_{\mathcal{M}_2}}$, $\color{red}\overrightarrow{l^\Theta_{\mathcal{M}_3}}$) in $\color{blue}\Sigma$, $\color{blue}\Omega$, and $\color{blue}\Theta$, respectively. The construction of $\color{blue}\Xi\color{black}$ relies on Obs. <ref> which guarantees the existence of $\color{red}\vec{l}$ in $\color{blue}\Sigma$, $\color{blue}\Omega$, and $\color{blue}\Theta$.

A similar condition is inserted in any rule that introduces fresh labels, i.e. M:cut, M:loop, M:MR, M:ML, M:CER, M:CQR, M:CQL.

We provide the full set of rules and proofs in Appendix <ref>, and formalization for the analogous extension to in Appendx <ref>.

§.§ Metatheory

We prove that cut mutation is sound in . For M:loop, this means that applying a mutation from the merged mutation set to each of the three branches maintains proof structure. In practice, this amounts to the admissibility of mutating (or in the case of $\color{violet}R$, eliminating) a cut in a proof. We formalize this additonal guarantee for in Lemma <ref>. Here, we write $\atomlabel{\vec{l}, \vec{m}}(\Gamma \vdashu{\chi}{\Sigma} \Delta)$ to mean that the sequent $\Gamma \vdash \Delta$ is labeled by $\color{red}\vec{l}$ and $\color{red}\vec{m}$, i.e. $\atomlabel{\vec{l}, \vec{m}}(\Gamma \vdashu{\chi}{\Sigma} \Delta) \equiv \atomlabel{\vec{l}, \vec{m}}\Gamma \vdashu{\chi}{\Sigma} \atomlabel{\vec{l}, \vec{m}}\Delta$.

If $\atomlabel{\vec{l}, \vec{o}}(\Gamma \vdashu{\chi}{\Sigma \cupm \dots \cupm \Omega \setminus \vec{l}} \Delta)$ such that

*[ ]
l⃗, m⃗(Γ_1 χΣ Δ_1)  … l⃗, k⃗(Γ_n χΩ Δ_n)

l⃗, o⃗(ΓχΣ…Ω∖l⃗ Δ)

(l⃗  fresh; Ξ= l^Σ_ℳ …l^Ω_𝒩)

then $\mu_{\color{blue}\Xi}(\Gamma_1 \vdash \Delta_1) \, \dots \,\mu_{\color{blue}\Xi}(\Gamma_n \vdash \Delta_n)$ are valid.

The significance is that cut atoms identified by with $\color{violet}W$ or $\color{violet}R$ could be weakened or removed while preserving the proof.

§.§ Diagnostics for the Parachute Example

The need for such diagnostics arises in the parachute example in Fig. <ref>. By inspecting the branch (3a) output $\color{blue}\Theta$, any mutation (including removal) is admissible for $\color{red}u_1$. Thus, $\color{red}u_1$, which was freshly cut into the proof via M:loop, was unnecessary in this proof branch. In fact, this is the case overall if we were to look at the output sets of all three branches (1), (2), (3). In this extension, $\Xi$ indicates that the atom labeled by $\color{red}u_1$ was an unnecessary cut in the proof. Lemma <ref> guarantees that the elimination of this atom maintains the proof structure.

§ RELATED WORK

ModelPlex [21] can identify modeling errors in formulas via synthesizing monitors that identify at runtime whether or not a model conforms to the real-world (or simulated) environment. Similarly, ULGEN [31] provides assurance for programming cyber-physical systems with concurrently interacting components.
We instead statically identify modeling errors prior to runtime.

Fulton & Platzer [14] describe the use of mutations to hybrid models in synthesizing candidate models which are then validated against the real-world-environment at runtime.

Additionally, Selvaraj et al. [29] discuss the difficulties of writing formulas that realistically describe physical systems. They classify two kinds of modeling errors in formulas, and provide theorems that ensure a model susceptible to these modeling errors cannot be proven safe. Our work provides the mechanism that diagnoses these modeling errors.

Dokhanchi et al. [10] proposed a debugging framework for finding specification errors in Signal Temporal Logic [20] formulas. They check for validity and account for two classes of errors: redundancy and vacuity. They extended Linear Temporal Logic with vacuity detection to find program traces that vacuously satisfy the specification, and redundancy detection for conjuncts in a formula.

Additionally, Kupferman & Vardi [19] developed a vacuity detector for temporal logic formulas that checks whether all subformulas of a specification affect its truth value. For formulas that contain conflicting assumptions, does provide vacuity detection by suggesting atoms that could be safely removed from a formula, but additionally suggests ways in which atoms could be generalized.

In recent work, Bartocci et al. [2] have developed an adaptive test case generation method for identifying bugs in Signal Temporal Logic [20] formulas for cyber-physical systems.

In other work, Bartocci et al. [3] develop property-based mutation testing and apply it to find bugs in Signal Temporal Logic formulas that model cyber-physical systems.
Their technique operates similarly to mutation testing [1] by modifying small components of a program, and accepting or rejecting the mutated programs according to whether they satisfy some property. The approach presented in [3] is limited to single-fault models, i.e. only one mutation can be applied to a model and tested at a time, whereas our work considers the application of multiple mutations, and potential relationships between mutations is captured via fusing.
Both approaches [20, 3] operate directly on the formula whereas our approach operates on the formula's proof tree which we use to glean information about both the formula and potential proof diagnostics. We expect the forthcoming implementaion of DA to take advantage of techniques from mutation testing while reaping the correctness guarantees ensured by .

Bug detection tools for other languages also rely on static analysis [12]. Cppcheck [18] generates bug reports for C++ programs at compile-time, which is analogous to the feedback generated by for . Alloy [16] is an object modeling language for modeling designs and prove properties about those designs, and Torlak et al. [30] find an unsatisfiable core of a larger, unsatisfiable model.

O'Hearn developed incorrectness logic [23] which exploits underapproximate reasoning to find bugs in programs.

Incorrectness logic can be used to diagnose which initial presumptions trigger error states but cannot track constraint usage.

Weakest precondition calculi compute the weakest set of assumptions under which a program could run while satisfying the desired postcondition [17, 22, 9].
The result of this analysis could be used to point to overspecified assumptions in a program. is more fine-grained in that it provides such information about general program statements and formulas appearing throughout a model.

Linear logic enforces that atoms must be used as resources in a proof exactly once [5, 6]. determines how atoms themselves can be modified rather than quantifying usage of these atoms. Atom usage in a proof is non-linear, making it important to reason about the extent to which all occurrences of a given atom could be generalized while preserving the proof. Proof normalization and cut elimination operate on proofs [7]. In particular, cut elimination asserts that if there exists a proof of a sequent, there exists a cut free proof of that sequent [24]. In this work, operates on the conjecture itself, producing a mutated proof in the process.

However, the extension in Sec. <ref> provides a mechanism of working towards a cut-free proof by determining atoms in a cut that can be removed.

§ CONCLUSION AND FUTURE WORK

This work provides a novel usage-aware proof calculus. Integrating a dataflow analysis with the proof calculus, we introduce a technique that infers information about atom usage in a proof, i.e. which pieces of information in a formula can be weakened or removed while maintaining the proof, yielding more generalized models and stronger safety guarantees regardless of where the atoms originate in a model. We proved soundness and completeness for both and , and developed an extension of these calculi that provides diagnostics for proof cuts. We believe the core calculus to be extensible to other proof calculi, and could also be equipped to track the propagation of other varieties of data and mutations. The results could be used to infer which proof steps are necessary or unnecessary from usage of a cut in a proof. Such information could be useful in developing optimal proofs of formulas. Implementations of and are forthcoming, yet we anticipate these to be straightforward with the proposed formulation. Like all other high-level reasoning and tracking relation among proof steps, and will be implemented outside the KeYmaera X core [26]. The metatheoretic properties proved in this work ensure that this implementation produces mutations and proof steps that are guaranteed to succeed in the core.

[1]
Aichernig, B.K., Brandl, H., Jöbstl, E., Krenn, W., Schlick, R., Tiran, S.:
Killing strategies for model-based mutation testing. Software Testing,
Verification and Reliability  25(8),  716–748 (2015).

[2]
Bartocci, E., Bloem, R., Maderbacher, B., Manjunath, N., Ničković, D.:
Adaptive testing for specification coverage and refinement in CPS models.
Nonlinear Analysis: Hybrid Systems  46,  101254 (2022).

[3]
Bartocci, E., Mariani, L., Ničković, D., Yadav, D.: Property-based mutation
testing. In: 2023 IEEE Conference on Software Testing, Verification and
Validation (ICST). pp. 222–233 (2023). 10.1109/ICST57152.2023.00029

[4]
Bohrer, R., Tan, Y.K., Mitsch, S., Myreen, M.O., Platzer, A.: VeriPhy:
Verified controller executables from verified cyber-physical system models.
In: Grossman, D. (ed.) PLDI. pp. 617–630. ACM (2018).

[5]
Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for
linear logic proof search. In: Dyckhoff, R., Herre, H., Schroeder-Heister, P.
(eds.) Extensions of Logic Programming. pp. 67–81. Springer, Berlin,
Heidelberg (1996)

[6]
Chirimar, J., Gunter, C.A., Riecke, J.G.: Reference counting as a computational
interpretation of linear logic. Journal of Functional Programming
6(2),  195–244 (1996). 10.1017/S0956796800001660

[7]
Cockett, R.: Deforestation, program transformation, and cut-elimination.
Electronic Notes in Theoretical Computer Science  44(1),  88–127
(2001). 10.1016/S1571-0661(04)80904-6, cMCS 2001, Coalgebraic Methods
in Computer Science (a Satellite Event of ETAPS 2001)

[8]
Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential.
J. Symb. Comput.  5(1/2),  29–35 (1988).

[9]
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of
programs. Commun. ACM  18(8),  453–457 (aug 1975).

[10]
Dokhanchi, A., Hoxha, B., Fainekos, G.: Formal requirement debugging for
testing and verification of cyber-physical systems. ACM Trans. Embed. Comput.
Syst.  17(2) (dec 2017). 10.1145/3147451

[11]
Dotzel, M., Mitsch, S., Platzer, A.: A Usage-Aware Sequent Calculus for
Differential Dynamic Logic. Tech. rep., Carnegie Mellon University (2023).

[12]
Engler, D., Musuvathi, M.: Static analysis versus software model checking for
bug finding. Verification, Model Checking, and Abstract Interpretation
2937 (2004)

[13]
Fulton, N., Mitsch, S., Bohrer, R., Platzer, A.: Bellerophon: Tactical theorem
proving for hybrid systems. In: Ayala-Rincón, M., Muñoz, C.A. (eds.)
ITP. LNCS, vol. 10499, pp. 207–224. Springer (2017).

[14]
Fulton, N., Platzer, A.: Verifiably safe off-model reinforcement learning. In:
Vojnar, T., Zhang, L. (eds.) TACAS. LNCS, vol. 11427, pp. 413–430. Springer
(2019). 10.1007/978-3-030-17462-0_28

[15]
Grebing, S., Ulbrich, M.: Usability recommendations for user guidance in
deductive program verification. Deductive Software Verification: Future
Perspectives: Reflections on the Occasion of 20 Years of KeY pp. 261–284

[16]
Jackson, D.: Alloy: A lightweight object modelling notation. Tech. rep., MIT
Laboratory for Computer Science (2000)

[17]
Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition
reasoning for expected runtimes of randomized algorithms. J. ACM
65(5) (aug 2018). 10.1145/3208102

[18]
Kaur, A., Nayyar, R.: A comparative study of static code analysis tools for
vulnerability detection in C/C++ and Java source code. Procedia
Computer Science  (2020)

[19]
Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking.
International Journal on Software Tools for Technology Transfer
4(2),  224–233 (2003). 10.1007/s100090100062

[20]
Maler, O., Ničković, D.: Monitoring properties of analog and
mixed-signal circuits. International Journal on Software Tools for Technology
Transfer  15(3),  247–268 (2013). 10.1007/s10009-012-0247-9

[21]
Mitsch, S., Platzer, A.: ModelPlex: Verified runtime validation of verified
cyber-physical system models. Form. Methods Syst. Des.  49(1),
33–74 (2016). 10.1007/s10703-016-0241-z, special issue of selected
papers from RV'14

[22]
Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM
Trans. Program. Lang. Syst.  18(3),  325–353 (may 1996).

[23]
O'Hearn, P.W.: Incorrectness logic. Proc. ACM Program. Lang.  4(POPL)
(dec 2019). 10.1145/3371078

[24]
Pfenning, F.: Lecture notes on cut elimination (September 2009)

[25]
Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas.
41(2),  143–189 (2008). 10.1007/s10817-008-9103-8

[26]
Platzer, A.: A uniform substitution calculus for differential dynamic logic.
In: Felty, A.P., Middeldorp, A. (eds.) CADE. LNCS, vol. 9195, pp. 467–481.
Springer (2015). 10.1007/978-3-319-21401-6_32

[27]
Platzer, A.: A complete uniform substitution calculus for differential dynamic
logic. J. Autom. Reas.  59(2),  219–265 (2017).

[28]
Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham
(2018). 10.1007/978-3-319-63588-0

[29]
Selvaraj, Y., Krook, J., Ahrendt, W., Fabian, M.: On how to not prove faulty
controllers safe in differential dynamic logic. In: International Conference
on Formal Engineering Methods, ICFEM'22. p. 281–297. LNCS, Springer-Verlag,
Berlin, Heidelberg (2022). 10.1007/978-3-031-17244-1_17

[30]
Torlak, E., C., F.S., Jackson, D.: Finding Minimal Unsatisfiable Cores of
Declarative Specifications. In: International Symposium on Formal Methods.
Springer, Berlin, Heidelberg (2008)

[31]
Yalcinkaya, B., Torfah, H., Desai, A., Seshia, S.A.: ULGEN: A runtime
assurance framework for programming safe cyber-physical systems. IEEE
Transactions on Computer-Aided Design of Integrated Circuits and Systems
pp. 1–1 (2023). 10.1109/TCAD.2023.3246386