Toward Structured Proofs for Dynamic Logics

TL;DR

Kaisar is a structured proof language for differential dynamic logic that introduces nominals to simplify reasoning about historical states in safety-critical cyber-physical systems, supported by formal metatheory.

Contribution

The paper introduces Kaisar, a novel structured proof language with first-class nominals for differential dynamic logic, enhancing CPS proofs and providing formal semantics and metatheory.

Findings

Successfully implemented Kaisar in KeYmaera X

Reproduced safety proofs for parachute and robot control

Proved soundness, completeness, and formal properties of Kaisar

Abstract

We present Kaisar, a structured interactive proof language for differential dynamic logic (dL), for safety-critical cyber-physical systems (CPS). The defining feature of Kaisar is *nominal terms*, which simplify CPS proofs by making the frequently needed historical references to past program states first-class. To support nominals, we extend the notion of structured proof with a first-class notion of *structured symbolic execution* of CPS models. We implement Kaisar in the theorem prover KeYmaera X and reproduce an example on the safe operation of a parachute and a case study on ground robot control. We show how nominals simplify common CPS reasoning tasks when combined with other features of structured proof. We develop an extensive metatheory for Kaisar. In addition to soundness and completeness, we show a formal specification for Kaisar's nominals and relate Kaisar to a nominal variant of dL.

Equations

$$r=a\wedge \underset{\text{dc}}{\underbrace{\left(x\ge 0\wedge v<0\right)}}$$

$$\displaystyle\rightarrow[\big{\{}~{}(?\underbrace{\left(r{}=a{}\land v-g\cdot\varepsilon>-\sqrt{\frac{g}{p}}\right)}_{\textit{Dive}}~{}\cup~{}r\mathrel{{:}{=}}p);$$

$$\displaystyle\phantom{\rightarrow[\big{\{}}~{}\ t\mathrel{{:}{=}}0;~{}\{x^{\prime}=v,~{}v^{\prime}=r\cdot v^{2}-g~{}\&~{}x\geq 0\land v<0\land t\leq\varepsilon\}$$

$$\displaystyle\phantom{\rightarrow[\big{\{}}\big{\}}^{*}](x=0\rightarrow\lvert v\rvert\leq m)$$

$$|v|\le loop(|v|)+g\cdot t\to loop(|v|)+g\cdot t\le loop(|v|)+g\cdot \epsilon \to loop(|v|)+g\cdot \epsilon <\sqrt{\frac{g}{p}}\to |v|<\sqrt{\frac{g}{p}}$$

$$\mathtt{SP}::=$$

$$\mathtt{PR}::=$$

$$|\left(\text{case}(x:p_{\varphi }\vee y:p_{\psi })\mathtt{SP}\right)|\left(\text{case}(x:p_{\varphi }\leftrightarrow y:p_{\psi })ofL\Rightarrow {\mathtt{SP}}_1|R\Rightarrow {\mathtt{SP}}_2\right)$$

$$p::=$$

$${\text{match}}_{\Gamma }(\otimes (p,q),\otimes (e,f))={\Gamma }_q\text{lx@proof@logical@and}{\text{match}}_{\Gamma }(p,e)={\Gamma }_p{\text{match}}_{{\Gamma }_p}(q,f)={\Gamma }_q$$

$$\mathtt{FP}::=$$

$$\begin{array}[b]{@{}c@{\linferRefSeparation}r@{\linferSequentSeparation}l@{}}&~{}&\ast\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:closeId}}}$}&x_{0}=2,x=1~{}&\vdash x+5=3\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:sub}}}$}&x_{0}=2,x=1~{}&\vdash[x:=x+5]x=3\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:eq}}}$}&x=2~{}&\vdash[x:=1][x:=x+5]x=3\\ \cline{2-3}\cr\raisebox{4.30554pt}{$\scriptstyle{\text{\ref{ir:eq}}}$}&~{}&\vdash[x:=2][x:=1][x:=x+5]x=3\end{array}$$

$$tr::=\mathtt{sub}(x,\theta )|\mathtt{eq}(x,x_i,\theta )|\mathtt{any}(x,x_i)|t$$

$${\mathrm{now}}_{ϵ}(x)$$

$${\mathrm{now}}_{H,\mathtt{any}(x,x_i)}(x)$$

$${\mathrm{now}}_{H,\mathtt{hr}}(x)$$

$${\mathrm{t}}_{H,t}(x)$$

$${\mathrm{t}}_{H,\mathtt{any}(x,x_i)}(x)$$

$$\mathfrak{S}((\omega );ϵ)$$

$$\mathfrak{S}(\eta ,\omega ;H,\mathtt{any}(x,x_i))$$

$$\mathfrak{S}(\eta ,\omega ;H,\mathtt{eq}(x,x_i,\theta ))$$

$$\mathfrak{S}(\eta ,\omega ;H,\mathtt{sub}(x,\theta ))$$

$$\mathfrak{S}(\eta ,t;H,t)$$

$$Pre$$

$$dc$$

$$dyn$$

$$\mathtt{BR}::=$$

$$\displaystyle|\$$

$$\left(H⇝H_{\varphi }\right)\text{assume}x:p\mathtt{SP}:\left(\Gamma ⊢[?\psi ]\varphi ,\Delta \right)\text{lx@proof@logical@and}{\text{match}}_{\Gamma }(p,\psi )={\Gamma }_{\psi }\left(H⇝H_{\varphi }\right)\mathtt{SP}:\left({\Gamma }_{\psi },x:\psi ⊢\varphi ,\Delta \right)$$

$$\left(H⇝H_1\right)\text{assign}x:=\ast \mathtt{SP}:\left(\Gamma ⊢[x:=\ast ]\varphi ,\Delta \right)\left(H,\mathtt{any}(x,x_i)⇝H_1\right)\mathtt{SP}:\left({\Gamma }_x^{x_i}⊢\varphi ,{\Delta }_x^{x_i}\right)$$

$$\left(H⇝H\right)\left(\text{case}p\Rightarrow {\mathtt{SP}}_{\alpha }|q\Rightarrow {\mathtt{SP}}_{\beta }\right):\left(\Gamma ⊢[\alpha \cup \beta ]\varphi ,\Delta \right)\left(H⇝H_{\alpha }\right){\mathtt{SP}}_{\alpha }:\left({\Gamma }_{\alpha }⊢[\alpha ]\varphi ,\Delta \right)\left(H⇝H_{\beta }\right){\mathtt{SP}}_{\beta }:\left({\Gamma }_{\beta }⊢[\beta ]\varphi ,\Delta \right)\text{lx@proof@logical@and}{\text{match}}_{\Gamma }(p,\alpha )={\Gamma }_{\alpha }{\text{match}}_{\Gamma }(q,\beta )={\Gamma }_{\beta }$$

$$\left(H⇝H_{\varphi }\right)\text{after}\{{\mathtt{SP}}_{\psi }\}\text{have}\psi \text{then}\{{\mathtt{SP}}_{\varphi }\}:\left(\Gamma ⊢[\alpha ][\beta ]\varphi ,\Delta \right)\left(H⇝H_{\psi }\right){\mathtt{SP}}_{\psi }:\left(\Gamma ⊢[\alpha ]\bar{\psi },\Delta \right)\left({H_{\psi }}^{\alpha }⇝H_{\varphi }\right){\mathtt{SP}}_{\varphi }:\left({\Gamma }^{\alpha },\bar{\psi }⊢[\beta ]\varphi ,{\Delta }^{\alpha }\right)$$

$$\left(H⇝H_{\varphi }\right)\text{state}t\mathtt{SP}:\left(\Gamma ⊢\varphi ,\Delta \right)\left(H,t⇝H_{\varphi }\right)\mathtt{SP}:\left(\Gamma ⊢\varphi ,\Delta \right)$$

$$\mathtt{IP}::=$$

$$\left(H⇝H_{\varphi }\right)\text{finally}\mathtt{SP}:\left(\Gamma ,[{\alpha }^{\ast }]J\mathrm{s}⊢[{\alpha }^{\ast }]\varphi ,\Delta \right)\left(H^{\alpha }⇝H_{\varphi }\right)\mathtt{SP}:\left({\Gamma }^{\alpha },J\mathrm{s}⊢\varphi ,{\Delta }^{\alpha }\right)$$

$$\left(H⇝H\right)\text{inv}x:\psi \{\text{Pre}\Rightarrow {\mathtt{SP}}_{Pre}|\text{Ind}\Rightarrow {\mathtt{SP}}_{Inv}\}\mathtt{IP}:\left(\Gamma ,[{\alpha }^{\ast }]J\mathrm{s}⊢[{\alpha }^{\ast }]\varphi ,\Delta \right)\left(H⇝H_{Pre}\right){\mathtt{SP}}_{Pre}:\left(\Gamma ,J\mathrm{s}⊢\bar{\psi },\Delta \right)\left(H^{\alpha }⇝H_{Inv}\right){\mathtt{SP}}_{Inv}:\left({\Gamma }^{\alpha },J\mathrm{s},\bar{\psi }⊢[\alpha ]\bar{\psi },{\Delta }^{\alpha }\right)\left(H⇝H_{Tail}\right)\mathtt{IP}:\left(\Gamma ,[{\alpha }^{\ast }]J\mathrm{s},x:[{\alpha }^{\ast }]\bar{\psi }⊢[{\alpha }^{\ast }]\varphi ,\Delta \right)$$

$$\left(H⇝H_{\mathtt{SP}}\right)\text{let}t(x\_)=e\mathtt{SP}:\left(\Gamma ⊢\varphi ,\Delta \right)\left(H,t_{now}⇝H_{\mathtt{SP}}\right)\mathtt{SP}:\left(\Gamma ,t(x\_):{mob}_{\{\}}(e,t_{now})⊢\varphi ,\Delta \right)$$

Full text

We implement Kaisar in the theorem prover KeYmaera X and reproduce an example on the safe operation of a parachute and a case study on ground robot control. We show how nominals simplify common CPS reasoning tasks when combined with other features of structured proof. We develop an extensive metatheory for Kaisar. In addition to soundness and completeness, we show a formal specification for Kaisar’s nominals and relate Kaisar to a nominal variant of dL.

††journalvolume: 1††journalnumber: 1††article: 1††journalyear: 2019††publicationmonth: 1††doi: 10.1145/nnnnnnn.nnnnnnn††journalyear: 2019††isbn: 978-x-xxxx-xxxx-x/YY/MM††doi: 10.1145/nnnnnnn.nnnnnnn††ccs: Theory of computation Logic and verification

1. Introduction

Many cyber-physical systems (CPS) such as autonomous cars (Loos et al., 2011), airborne collision-avoidance systems (Jeannin et al., 2015) and surgical robots (Kouskoulas et al., 2013) are safety-critical, and thus their correctness is of utmost importance. Differential dynamic logic (dL) (Platzer, 2008) is a domain-specific logic which expresses correctness theorems such as safety and liveness for hybrid dynamical systems models of CPS, which combine discrete computation with ordinary differential equations (ODEs).

Because safety and liveness for hybrid systems are undecidable, (Henzinger, 1996) achieving strong correctness results for nontrivial systems demands an interactive technique that allows users to provide human insight when automation does not suffice. The KeYmaera X (Fulton et al., 2015) theorem prover for dL (in comparison to, e.g. model checking  (Frehse et al., 2011; Dreossi, 2017; Frehse, 2005; Boker et al., 2014; Henzinger et al., 1997; Kido et al., 2016; Suenaga and Hasuo, 2011; Gao et al., 2013b, a) approaches) enables human insight through interactive theorem proving. The advantage of this interaction-based approach is its flexibility. For any given hybrid system, the proof difficulty may lie in the complexity of discrete dynamics, continuous dynamics, solving first-order real arithmetic at the leaves, or all three. Through interactivity, the proof author can address the difficult aspects of their system, while letting automation handle simpler parts. Interactive theorem-proving for CPS verification has proven fruitful through a number of case studies (Loos et al., 2011; Jeannin et al., 2015; Kouskoulas et al., 2013; Platzer and Clarke, 2009; Platzer and Quesel, 2009; Loos et al., 2013; Müller et al., 2015, 2015).

While these results demonstrate the significant potential that deduction has in CPS, it remains to be seen what the most productive way is for writing interactive CPS proofs. Interactive point-and-click interfaces are available for KeYmaera X (Mitsch and Platzer, 2016) and its predecessor KeYmaera (Platzer and Quesel, 2008), which are useful for learning, but become tedious at scale. Tactical theorem proving is available for CPS (Fulton et al., 2017), which is useful for programming generic proof search procedures, but requires a certain level of aptitude in the proof system and is harder to scale for complex applications. We, thus, argue that CPS proofs are to be taken seriously and merit the full attention of a first-class approach.

We focus on the opportunity provided by the hybrid mixture of discrete and continuous invariants inherent to hybrid systems. Typical proofs combine discrete and continuous invariants, which in turn combine continuously-evolving, discretely-evolving, and constant variables. CPS invariant proofs often relate the present state to multiple historical system states. It has long been known that historical reference, implementable with ghost state, is an essential component of proof in many domains (Apt et al., 1979; Owicki and Gries, 1976; Owicki, 1975; Apt et al., 2010; Clint, 1973). It has been known equally long (Clarke, 1980) that manual ghost arguments can make proofs clumsy. For example, stating even a single invariant might require multiple non-local changes to introduce ghost state. This is especially noticeable for CPS proofs, which typically contain nested invariants with references to multiple states.

In this paper, we devise a proof language Kaisar for CPS that addresses the problem of automating historical reference. The distinguishing feature of Kaisar is nominal proof: proof authors can give names $t$ to abstract proof states and then refer to the value of any term $\theta$ in proof state $t$ by a nominal term $t(\theta)$. We show through the examples of this paper (Fulton et al., 2017) that nominal terms simplify the complex historical reasoning necessary for CPS verification: Instead of cluttering a proof with explicit ghosts of each term, the author can write down values from past states directly when needed, and the Kaisar nominal system will automatically supply the necessary ghost state.

The automation of historical reference in Kaisar is supported by structured symbolic execution, an extension of the structured proof paradigm introduced in Mizar (Bancerek et al., 2015), and seen in Isabelle’s Isar (Wenzel, 1999) and ${\rm TLA}^{+}$’s TLAPS (Cousineau et al., 2012; Lamport, 1992). Symbolic execution is a first-class proof language feature in Kaisar, enabling the language to automatically maintain an abstract execution trace, introducing ghost variables when needed. This trace enables automatically reducing nominal terms to ghost state, solving the historical reference automation problem. Hence the name: Kaisar is to KeYmaera X as Isar is to Isabelle: A structured proof language tailored to the needs of each prover’s logic.

In structuring proofs around first-class symbolic execution, it is non-obvious but essential that we do not restrict which formulas are provable. To this end, we develop a comprehensive metatheory for Kaisar, showing it is not only sound, but complete with respect to existing calculi (Platzer, 2008), which are themselves sound and relatively complete for hybrid systems (Platzer, 2016, 2012b, 2008). We also give a precise semantics to nominal terms via dynamic execution traces: the nominal term computed by Kaisar for $t(\theta)$ equals the value of $\theta$ in the concrete program state corresponding to abstract state $t$. We relate nominal terms to a nominal dialect of dL called d$\mathcal{L}_{h}$: (Platzer, 2007b) the meaning of proof-level named states $t$ can be understood via the logic-level nominal states of d$\mathcal{L}_{h}$. The above applies for both discrete and continuous dynamics and for both initial and intermediate states.

In adopting structured symbolic execution, we import the existing benefits of structured proof to hybrid systems for the first time. It has long been noted (Wenzel, 2006) that structured proof languages improve scalability and maintainability via block structure, and improve readability via their declarative style, with readability benefits extending to natural-language structured proofs (Lamport, 2012, 1995). This is important for CPS verification as the scale of systems verified continues to grow (Jeannin et al., 2015; Müller et al., 2015).

Lastly, we believe the nominal mechanism of Kaisar is of interest beyond CPS verification. A number of verification tools  (Ahrendt et al., 2016; Fulton et al., 2015; Leino, 2010, 2008; Barnett et al., 2005; Leino et al., 2009; Leavens et al., 1999) offer ad-hoc constructs without theoretical justification which can reference only the initial program state. We generalize and formally justify them.

We show that Kaisar works in practice with a prototype for Kaisar in KeYmaera X. We evaluate our implementation using the examples in this paper, including a representative proof on parachute control. We evaluate further by reproducing a case study on the control of ground robots (Section 9).

In Section 2 we provide a primer on dL, hybrid systems and dynamic logics, giving an informal structured proof following Lamport (Lamport, 2012, 1995). In Section 3, we present the propositional fragment of Kaisar, introducing structural constructs and pattern-matching to aid in making proofs concise. This fragment borrows from Isar; we present it separately to show its relationship with prior work. In Section 4, we detail the technical challenge and solution for nominals. In Section 5 we add that solution to Kaisar, generalizing it to the discrete fragment of dL by introducing nominal terms. In Section 6 we show that our notion of nominal terms generalizes to full dL. In Section 7 we validate Kaisar by developing its metatheory. In Section 8 we compare Kaisar with other proof languages.

2. Background: Differential Dynamic Logic

Differential dynamic logic (dL) (Platzer, 2012b, 2008) is a dynamic logic (Pratt, 1976; Harel et al., 2000) for formally verifying hybrid (dynamical) systems models of cyber-physical systems (CPS), which is implemented in the theorem prover KeYmaera X (Fulton et al., 2015) and has seen successful application in a number of case studies (Mitsch et al., 2013; Jeannin et al., 2015; Kouskoulas et al., 2013; Loos et al., 2011). In dL, a hybrid systems model of a CPS is expressed as a (nondeterministic) program in the language of hybrid programs. The distinguishing feature of hybrid programs is the ability to model continuous physics with ordinary differential equations (ODEs). Combined with nondeterminism, real arithmetic, and standard discrete constructs, this suffices to express hybrid systems.

As usual in dynamic logic, dL internalizes program execution with first-class modal operators $[\alpha]\phi$ and $\langle\alpha\rangle\phi$ stating $\phi$ is true after all or some execution paths of the program $\alpha$, respectively. Dynamic logics are a generalization of Hoare logics, e.g. any Hoare triple $\{P\}\alpha\{Q\}$ can be expressed in dynamic logic as the formula $P\rightarrow[\alpha]Q$. Dynamic logic is more general because the modal operators are first-class and may be nested freely. Throughout this paper, we let $e,f,g$ range over expressions of dL. Expressions are divided into propositions $\phi,\psi$, hybrid programs $\alpha,\beta$, and real-valued terms $\theta$. The proposition language of dL combines first-order arithmetic ($FOL_{\mathbb{R}}{}$) with the dynamic logic modalities ${[{\alpha}]}\phi$ and ${\langle{\alpha}\rangle}\phi$:

$\phi,\psi,P,Q~{}::=~{}\phi\wedge\psi\ |\ \phi\vee\psi\ |\ \neg{\phi}\ |\ \forall x~{}\phi\ |\ \exists x~{}\phi\ |\ [\alpha]\phi\ |\ \langle\alpha\rangle\phi\ |\ \theta_{1}\sim\theta_{2}$

where $\sim$ is a comparison operator on the (classical) reals, i.e. $\sim\ \in\{<,\leq,=,\geq,>,\neq\}$.

The term language of dL consists of basic arithmetic operations on real-valued variables with rational literals $q\in\mathbb{Q}$ and rational exponentiation $\theta^{q}$:

$\theta~{}::=~{}x\ |\ q\ |\ \theta_{1}+\theta_{2}\ |\ \theta_{1}-\theta_{2}\ |\ \theta_{1}\cdot\ \theta_{2}\ |\ \theta_{1}/\theta_{2}\ |\ \theta^{q}$

This means that the program-free fragment of dL is equivalent to first-order classical logic over real-closed fields ($FOL_{\mathbb{R}}$), which is decidable but unscalable, requiring doubly-exponential time (Davenport and Heintz, 1988). The hybrid programs of dL include typical discrete constructs and differential equation systems:

$\alpha,\beta~{}::=~{}x:=\theta\ |\ x\mathrel{{:}{=}}\ast\ |\ ?\phi\ |\ \alpha;\beta\ |\ \alpha\cup\beta\ |\ \alpha^{*}\ |\ {{x^{\prime}=\theta}}\,\&\,Q$

• •

Assignment $x:=\theta$ Sets a variable $x$ to the current value of term $\theta$.

• •

Nondeterministic Assignment $x\mathrel{{:}{=}}\ast$ Sets $x$ nondeterministically to an arbitrary real.

• •

Assertion $?\phi$ Execution transitions to the current state if formula $\phi$ is true, else the program has no transitions. In typical models $\phi$ is first-order arithmetic.

• •

Sequential Composition $\alpha;\beta$ Runs program $\alpha$, then runs $\beta$ in some resulting state.

• •

Choice $\alpha\cup\beta$ Nondeterministically runs either program $\alpha$ or $\beta$.

• •

Iteration $\alpha^{*}$ Nondeterministically runs program $\alpha$ zero or more times.

• •

ODE Evolution $\{x^{\prime}=\theta\&Q\}$ Evolves the ODE system $x^{\prime}=\theta$ nondeterministically for any duration $r\in\mathbb{R}_{\geq{0}}$ that never leaves the evolution domain formula $Q$.

We illustrate dL with a running example in Model 1, which models the decision-making of a skydiver opening their parachute at a safe time. We intentionally chose this example because it demonstrates the techniques necessary for more complex systems within the space provided. As further validation we reproduced a larger case study (Mitsch et al., 2013), see Section 9.

Model 1 (Safety specification for the skydiver model).

[TABLE]

This structure is typical: the system is a control-plant loop, alternating between the skydiver’s control decisions and evolution of the environment or plant (i.e. gravity and drag). The diver has a downward velocity $v<0$, with a maximum safe landing speed $m$. The chute is initially closed ($r=a$) until opened by the controller ($r\mathrel{{:}{=}}p$). The controller can choose not to open the chute if it will not exceed the equilibrium velocity $-\sqrt{\frac{g}{p}}$, where $g$ is gravity and $p$ is the resistance of an open chute. The plant evolves altitude $x$ at velocity $v$, which itself evolves at $v^{\prime}=v^{2}\cdot{r}-g$: Newton drag is proportional to $v^{2}$ by a factor $r$ and gravity $g$ is constant. The domain constraint stops the ODE upon hitting the ground ($x=0$) or reaching the next control time ($t=\varepsilon$ for time limit $\varepsilon$). It also simplifies the proof by providing an assumption $v<0$, which is always true for a falling diver. In this hybrid program model, when the diver lands ($x=0$), they have a safe velocity $v\geq m$.

2.1. A Structured Natural-Language Proof

We introduce the reasoning principles for dL by giving an informal structured proof of skydiver safety. Beyond discrete program reasoning and first-order real arithmetic, the defining proof techniques of dL are differential induction (Platzer, 2016, 2012a, 2010, 2007a) and differential ghosts (Platzer, 2011). Differential induction and ghosts are important because they enable rigorous proofs about ODEs whose solutions are outside the decidable fragment of arithmetic, in our example the drag equation. Differential induction states that a formula $\phi$ is invariant if it is true initially and its differential $(\phi)^{\prime}$ is invariant, e.g. $\theta_{1}>\theta_{2}$ is invariant if $\theta_{1}>\theta_{2}$ initially and $(\theta_{1})^{\prime}\geq(\theta_{2})^{\prime}$ is invariant. Differential ghosts enable augmenting ODEs with continuously-evolving ghost state. If a formula $\phi$ is invariant, but not inductive, ghosts enable restating it as a formula that holds by differential induction. This occurs, e.g. if $\theta_{1}$ converges asymptotically toward $\theta_{2}$ like velocity converges to the equilibrium in Model 1.

In this proof, we loosely follow the Lamport’s (Lamport, 2012, 1995) hierarchical style with numbered proof steps, but use our own keywords, such as State for giving names to states and Introduce for introducing differential ghost variables. We restate in abbreviated form the theorem of Model 1:

Theorem 2.1 (Skydiver Safety).

$\mathit{pre}\rightarrow{[(\mathit{ctrl;plant}^{*})](x=0\rightarrow\lvert v\rvert\leq m)}\ \text{is valid}$**

State init: Assume $init(pre)$.

Invariant: $\mathit{const}$ vacuously because the free variables of $\mathit{const}$ are not written in $(\mathit{ctrl;plant})$.

Invariant: $\mathit{dc}$ by loop induction.Base Case: by arithmetic and 1.

Inductive Case:  $\mathit{dc}\rightarrow[\mathit{(ctrl;{{plant}}\,\&\,dc)}]\mathit{dc}$ holds by the domain constraint.

Invariant: $\mathit{dyn}$ by loop induction. Base Case: by arithmetic and 2. Inductive Case: We establish differential invariants for each control case.

State loop:. Here $\mathit{dc},\mathit{const},\mathit{dyn}$ hold by 2, 3,4

Control Case: $?(r=a\land\lvert v\rvert+g\cdot\epsilon>\sqrt{\frac{g}{p}});t:=0$

Invariant: $g>0\land{p>0}$ vacuously.

Invariant: $\lvert v\rvert<\lvert loop(v)\rvert+g\cdot{t}$ by differential induction.

Base Case: by arithmetic and 4.2.

Inductive Case: $\lvert v\rvert^{\prime}\leq\lvert loop(v)\rvert+g\cdot{t}^{\prime}$ holds because $(v)^{\prime}=r\cdot{v^{2}}-g\geq-g=(loop(v)-g\cdot{t})^{\prime}$ by arithmetic and 4.2.1.

Invariant: $t\leq{\epsilon}\land{v\geq{0}}$ by domain constraint.

Invariant: $loop(\lvert v\rvert)+g\cdot{t}\leq loop(\lvert v\rvert)+g\cdot\epsilon$ by arithmetic, 4.2.1, and 4.2.3.

Invariant: $loop(\lvert v\rvert)+g\cdot\epsilon<\sqrt{\frac{g}{p}}$ by arithmetic and 4.2.

Q.E.D. Because $\lvert v\rvert>\sqrt{\frac{g}{p}}$ by transitivity, 4.2.2, 4.2.4, and 4.2.5.

Control Case: $r:=p;t:=0$. Safety is invariant but not inductive: $\lvert v\rvert^{\prime}>\left(-\sqrt{\frac{g}{p}}\right)^{\prime}$. We augment the ODE with a differential ghost variable, enabling an inductive invariant.

Invariant: $g>0\land{p>0}$ is invariant.

Introduce $y^{\prime}=-\frac{p}{2}\cdot\left(\lvert v\rvert+\sqrt{\frac{g}{p}}\right)\cdot{y}$ with $loop(y)^{2}\cdot\left(-\lvert v\rvert+\sqrt{\frac{g}{p}}\right)=1$ for fresh variable $y$. This is sound since $y^{\prime}$ is linear in $y$ and thus duration of the ODE is unchanged, and since $y$ is fresh the augmented ODE agrees with the original on all other variables.

Invariant: $y^{2}\cdot\left(-\lvert v\rvert+\sqrt{\frac{g}{p}}\right)=1$ by differential induction. The base case holds by 4.3.2; the inductive step holds by construction of $y^{\prime}$ and arithmetic.

Invariant: $\lvert v\rvert<\sqrt{\frac{g}{p}}$ because it is arithmetically equivalent to 4.3.3.

Q.E.D. Because 4 implies the postcondition by arithmetic.

We mechanize this proof in Kaisar as a guiding example throughout the paper.

3. First-Order Kaisar

We present the first-order (real-arithmetic, i.e. $FOL_{\mathbb{R}}$) fragment of Kaisar alone before considering dynamic logic. The examples of Figure 1 demonstrate the key features of First-Order Kaisar:

• •

Block-structuring elements (have, note, let, show) introduce intermediate facts, definitions, and conclusions. Facts $\phi$ are assigned names $x:\phi$ for later reference.

• •

Unstructured proof methods (using $\mathit{facts}$ by $\langle{\mathit{method}}\rangle$) close the leaves of proofs.

• •

Backward-chaining propositional rules (assume, case) decompose logical connectives.

• •

Forward-chaining proof terms (note $x={\tt FP}$) make arithmetic lemmas convenient.

• •

Patterns and abbreviations (let $x\_=\ldots$) improve conciseness.

All of these features have appeared previously in some form in the literature (Wenzel, 2006). Here we make clear any differences specific to Kaisar and in doing so lay a solid foundation for the development of nominals. We do so by expanding upon the examples with formal syntax and semantics, given as a proof-checking relation. Note that the examples in this section, because they fall under $FOL_{\mathbb{R}}$, are in principle decidable. For that reason we focus here on techniques that vastly improve the speed of decision procedures (arithmetic proving with note and have), and which generalize to the undecidable fragments of dL handled in Sections 5 and 6 (block-structuring and pattern-matching).

Examples

For a first-order example, consider the transitivity reasoning of Step ?? in Section 2.1. Figure 1 presents four proofs of the following arithmetic subgoal in dL:

[TABLE]

Figure 1 develops a proof as one might in interactive proof. Examples 1a and 1b both appeal immediately to an arithmetic solver, with Example 1b using pattern-matching to introduce concise names, e.g. ${\tt vt\_}=loop(\lvert v\rvert)+g\cdot{t}$. Pattern-matching makes Example 1b more flexible: it will work even if the definition of $\mathit{vt\_},\mathit{vEps\_},$ or $\mathit{vBound\_}$ changes. However, the $\mathbb{R}$ will be prohibitively slow if $\mathit{vt\_},\mathit{vEps\_},\mathit{vBound\_}$ become too large (all reasoning is performed on the expanded terms). Example 1c restores speed by isolating the transitivity axiom in the fact trans and instantiating it with note to recover the result. The note step supplies term inputs $\mathit{v},\mathit{vt\_},\mathit{vEps\_},\mathit{vBound\_}$ first, then propositions v, gt, gEps, matching the structure of the formula trans. The id proof method closes the proof once we provide a proof of the goal with using.

The let statement reuses the pattern-matching mechanism to introduce definitions for readability at will. Example 1d uses let to ensure that the bound vBound_ is specifically $\sqrt{\frac{g}{p}}$. This provides machine-checked documentation if, e.g. we did not intend this proof to be general or if the proof depended on the value of vBound_.

Definitions

The proof-checking judgements of Kaisar maintain a context $\Gamma$ which maps names to assumptions (or conclusions for succedents $\Delta$) and abbreviations introduced through pattern-matching. Abbreviation variables are suffixed with an underscore , so $\Gamma\equiv\{xz\mapsto(x>0),{\tt{y\_}}\mapsto y_{0}+5\}$ means we have the assumption that $x>0$ via the name $xz$ and we have abbreviated $y_{0}+5$ as $y$. Throughout the paper, subscripts are mnemonic, e.g. $\Gamma_{\phi}$ could be a context associated with $\phi$ in any way. Kaisar expands abbreviations before reasoning to ensure no extensions to dL are necessary. Substitution of $x$ with $\theta$ in $\phi$ is denoted ${\phi}_{x}^{\theta}$.

The primary proof-checking judgement ${\tt SP}:(\Gamma\vdash{\Delta})$ says that ${\tt SP}$ is a structured proof of the classical sequent $\Gamma\vdash\Delta$ (i.e. the formula $\bigwedge_{\phi\in\Gamma}{\phi}\rightarrow\bigvee_{\psi\in\Delta}\psi$). In proving safety theorems $\phi\rightarrow[\alpha]\psi$, the succedent $\Delta$ typically consists of a single formula. The auxilliary judgement ${\tt FP}:(\Gamma\vdash\Delta)$ for forward-chaining proofs is analogous. In Section 5 we will extend the judgement ${\tt SP}:(\Gamma\vdash{\Delta})$ with static execution traces to support structured symbolic execution.

Expressions written in proofs can contain abbreviations, but sequents, being pure dL, do not. We write $\bar{e}_{\Gamma}$ (or, when clear, simply $\bar{e}$) for the expansion of $e$ which replaces all abbreviations with their values. We also use matching of patterns $p$ with $\textbf{match}_{\Gamma}(p,e)=\Gamma_{p}$ where $\Gamma_{p}$ extends $\Gamma$ with bindings produced by matching $e$ against $p$.

Block Structure

The top level of a Kaisar proof is a structured proof (SP)

[TABLE]

The propositional rules (PR) assume and case perform propositional reasoning. The case construct is multi-purpose, supporting the connectives $\vee,\leftrightarrow,\land$. Here a vertical bar $|$ outside parentheses separates syntactic productions, while a bar inside parentheses is syntax to separate cases:

[TABLE]

We give only right rules: left rules are analogous and derivable with the focus construct of Section 5. In each rule we assume fresh variables $x,y$:

[TABLE]

Pattern-matching reduces verbosity vs. writing complete formulas. In Example 1b, we shorten the Kaisar proof of Example 1a by applying variable patterns $x\_$ and $y\_$ to the assumption (thus matching any conjunction) and a wildcard pattern _ to the goal (thus matching any goal).

[TABLE]

The have construct cuts, proves, and names an intermediate fact $\psi$ with ${\tt SP}_{1}$, then continues the main proof ${\tt SP}_{2}$. When ${\tt SP}_{1}$ immediately show’s $\phi$, as in Example 1c, we omit the show keyword in the concrete syntax. The use of have in Example 1c is typical: the direct application of $\mathbb{R}$ in Example 1(a,b) does not scale if $\mathit{vt\_},mathit{v\varepsilon{}},\mathit{vBound\_}$ are large terms. By isolating the ${\mathit{trans}}$ axiom with have, we enable the arithmetic reasoning to scale.

The let keyword, as used in Example 1d, performs a general-purpose pattern-match, which in this case simply binds $goal{\tt\_}$ to $v>-\sqrt{\frac{g}{p}}$, then continues the proof ${\tt SP}$. The note construct is similar to have, except that the intermediate fact is proven by a forward-chaining proof term. It is often convenient for instantiating (derived) axioms or performing propositional reasoning, as in Example 1c. Because note uses a forward-chaining proof, we need not specify the proven formula, but rather the proof-checking judgement synthesizes it as an output.

Unstructured Proof Methods

As shown in Example 1, show closes a proof leaf by specifying facts (using) and an automatic proof method ($\mathbb{R}$, id, auto). In contrast to other languages (Wenzel, 2006), these methods are the only unstructured language construct, as we have found no need for a full-fledged unstructured language. The ident method is extremely fast but expects the conclusion to appear verbatim in the context or using clause. The $\mathbb{R}$ method invokes a $FOL_{\mathbb{R}}{}$ decision procedure (Collins and Hong, 1991; Arnon et al., 1984). We typically assist $\mathbb{R}$ on difficult goals by specifying facts with a using clause for speed. The using clause can specify both assumptions from the context and additional facts by forward proof. When the using block is empty, it defaults to the entire context. The auto method applies general-purpose but incomplete proof heuristics including symbolic execution and also benefits from using. Note the auto method does not have a simple proof rule. This is okay at the unstructured proof level: any sound proof method is adequate for closing leaves of a proof.111The auto method (tactic) of KeYmaera X is sound because it uses only operations of a sound LCF-style core (Fulton et al., 2015).

${\textbf{facts}({p}s,{{\tt FP}}s)}$ defines the facts available to the proof method (assumptions and FP conclusions). The pattern $q$ selects a conclusion from $\Delta$, else we default to the entire succedent.

${\textbf{facts}({p}s,{{\tt FP}}s)}\equiv\{\phi\in\Gamma~{}|~{}\exists\exists{}{i~{}\,}\textbf{match}_{\Gamma}(p_{i},\phi)\}\cup\{\phi~{}|~{}\exists\exists{}{i~{}\,}~{}{\tt FP}_{i}:(\Gamma\vdash\phi)\}$

[TABLE]

Pattern Matching

Throughout the examples of Figure 1, we use pattern-matching to describe the shapes of expressions and select assumptions for use in automation. The above features suffice for structural proof steps. The pattern language of Kaisar is defined inductively:

[TABLE]

Pattern-matching is formalized as a judgement $\textbf{match}_{\Gamma}(p,e)=\Gamma_{p}$, where $\Gamma_{p}$ extends $\Gamma$ with bindings resulting from the match (we omit $\Gamma_{p}$ when it is not used and omit $\Gamma$ when it is clear from context). We write $\textbf{match}(p,e)=\bot$ when no pattern-matching rule applies. In the definition below, we use the notation $\otimes(e,f)$ to generically say that all operators $\otimes$ (where the arguments are expressions $e,f$) of the dL language are supported in patterns. The dL operators are matched structurally.

[TABLE]

The meaning of a variable pattern ident_ depends on whether it is bound in $\Gamma$. If ident is free, the pattern matches anything and binds it to ident. If ident is bound, the pattern matches only the value of ident. Wildcard patterns _ match anything and do not introduce a binding.

[TABLE]

The above patterns often suffice for selecting individual facts, as done in forward proofs. However, when referencing a large number of facts (e.g. in show), it helps to select facts in bulk, for which the following patterns are also useful. Variable occurrence patterns $p(vars)$ and $p(\neg vars)$ select all formulas $\phi$ where the given variables do or do not occur in its free variables $\mathop{\text{FV}}(\phi)$, respectively:

[TABLE]

Patterns support set operations. Set patterns proceed left-to-right. Union short-circuits on success and intersection short-circuits on failure. Negation patterns $\neg p$ match only when $p$ fails to match, so we require that $p$ binds no variables in this case for the sake of clarity. This is not a restriction because any free variable patterns in $p$ can be replaced with wildcards, which never bind.

[TABLE]

Extended Expression Evaluation

In order to keep abbreviations ident_ outside the core language of dL, we automatically expand extended terms featuring abbreviations ident_ to proper terms with the term expansion function $\bar{e}_{\Gamma}=f$ (we omit $\Gamma$ when clear). As in pattern-matching, expression constructors map through homomorphically and identifiers are substituted with their values:

[TABLE]

Forward-Chaining Proof Terms

A comprehensive structured language should provide both backward and forward-chaining proof. Wenzel (Wenzel, 1999) observes that backward chaining is often most natural for major steps and forward chaining more natural for minor intermediate steps. Backward chaining works well when the proof can be guided either by the structure of a formula (e.g. during symbolic execution) or by human intuition (e.g. when choosing invariants). The addition of forward chaining becomes desireable when we wish to experiment with free-form compositions of known facts, e.g. when trying to assist an arithmetic solver with manual simplifications. In Kaisar, forward-chaining proofs are built from atomic facts in $\Gamma$ and a standard library of first-order logic rules, which are composed with application $({\tt FP}~{}{\tt FP})$ and instantiation $({\tt FP}~{}\theta)$.

[TABLE]

The judgement $\Gamma\vdash_{\Sigma}e:\phi$ says $e$ is a proof of $\phi$ using assumptions $\Gamma$, where $\Sigma$ is a library of builtin propositional rules. Facts and rules can be selected from $\Gamma$ and $\Sigma$ with patterns:

[TABLE]

4. Static and Dynamic Execution Traces

We describe the static execution trace mechanism used to implement nominals and automate historical reference. We present the challenges of historical reference by an easy example with sequent calculus proofs for assignment. Consider the sequent calculus assignment rules:

[TABLE]

In $[:=]sub$, reference to the initial state stays simple, while the final value does not. In the resulting goal $\Gamma\vdash{\phi}_{x}^{\theta},\Delta$, the variable $x$ refers to the initial value, but we must write $\theta$ (which may be a large term) to refer to the final value. In $[:=]eq$, the opposite is true: $x$ now refers to the final value, but the initial value of $x$ is stored in a fresh ghost variable $x_{i}$, which we must remember.

Complicating matters further, in practice we wish to use a combination of $[:=]sub$ and $[:=]eq$. The $[:=]sub$ rule only applies when the substitution ${\phi}_{x}^{\theta}$ is admissible, e.g. when $\mathop{\text{FV}}(\theta)\cap\mathop{\text{BV}}(\phi)=\emptyset$. However, we wish to use it whenever it applies to reduce the total number of variables and formulas in the context, which are essential to the performance of real-arithmetic decision procedures (Collins and Hong, 1991). Therefore the natural approach is to use $[:=]sub$ when it applies and $[:=]eq$ otherwise.

After a number of such reasoning steps, the meaning of a variable $x$ in a sequent (we call this the sequent-level meaning) may disagree with the value of both the initial and final values of the program variable $x$ (we call these the program-level meaning in the initial and final states). To observe this issue in action, consider the following (trivial) sequent proof:

[TABLE]

There are four program states in the above proof: one before each assignment and one at the end. Throughout the first two steps, the sequent-level meaning of $x$ corresponds exactly with its program-level meaning in the current state. At the final state of the program, the value of $x$ in the program corresponds to $x+5$ in the sequent, whereas $x$ in the sequent refers to the value of $x$ from its previous state. This is a problem: It is non-trivial to reference initial and final, let alone intermediate state in a proof regime that mixes $[:=]eq$ and $[:=]sub$, yet we want them all.

We address this problem by automating state-change bookkeeping in a static execution trace data structure. Static execution traces automate state navigation by providing a static, finitary abstraction of a dynamic program execution trace.

Definition 4.1 (Static Traces).

A static trace is an ordered list of four kinds of trace records (tr):

[TABLE]

We denote the empty trace by $\epsilon{}$. For any state name $t$ appearing in $H$ (i.e. $t\in\mathrm{Dom}(H)$) we denote by $t(H)$ the unique prefix of $\eta$ ending at state $t$.

By maintaining a substitution record ${\tt sub}(x,\theta)$ for each substitution, we can automatically translate between the sequent-level and (current) program-level meaning of an expression. For example, if you wish to know the sequent-level value of the program-level term $x^{2}$ in the final state, after ${\tt sub}(x,x+5)$, it suffices to compute ${(x^{2})}_{x}^{x+5}=(x+5)^{2}$. We enable nominal references to past states by adding a $t$ record at each named state $t$ and an ${\tt eq}(x,x_{i},\theta)$ any time the $[:=]eq$ rule is used to rename $x_{i}=x$ and introduce an assumption $x=\theta$. This allows us to determine, e.g. that the second value of $x$ was ultimately renamed to $x_{0}$. The case for $x\mathrel{{:}{=}}\ast$ is marked with ${\tt any}(x,x_{i})$, which is analogous to ${\tt eq}(x,x_{i},\theta)$, without any assumption on the $x$ value.

Given a trace, we can reconstruct the value at any proof state by replaying the composition of all substitutions since the renaming of interest. We begin by defining the pseudo-nominal $\mathrm{now}_{H}(x)$ which computes the current sequent-level equivalent for a program-level variable $x$ at the end of trace $H$. All expressions are by default assumed to occur at state now. Because expressions depend only on the values of variables, it suffices to define the variable case:

[TABLE]

We recurse until we find a record for the $x$ of interest.

If it is a sub record, we stop immediately and return $\theta$: even if the trace contains multiple subs for the same $x$, they are cumulative (the last record contains the composition of all subs). If it is a eq record, then we use the current value of $x$.

To compute a nominal $\mathrm{t}_{H}(x)$, we determine the name $x$ has at state $t$ in the history $H$, which is either $x$ or some ghost $x_{i}$ (if $x$ has been ghosted since state $t$). We then compute $\mathrm{now}_{H^{\prime},t}(x)$ or $\mathrm{now}_{H^{\prime},t}(x_{i})$ accordingly where $H^{\prime}$ is the prefix of $H$ preceding state $t$. As in the program variable case, $\mathrm{now}_{H}(x_{i})$ can either be exactly $x_{i}$ or the result of a substitution.

[TABLE]

It is now natural to ask the question: If $\mathrm{now}_{H}(x)$ converts between the program-level state and sequent-level state, can we give a precise meaning to the notion of sequent-level state? The answer is yes, but in general the sequent-level state will not be identical to any specific state the program passed through, but rather each variable might take its meaning from different past states. To this end, we define a notion of dynamic trace encapsulating all past program states.

Definition 4.2 (Dynamic Traces).

A dynamic trace $\eta$ is a non-empty list of program states $\omega$, possibly interleaved with state names $t$ (but always containing at least one state). The first state is denoted ${\tt fst}(\eta)$, the last state ${\tt last}(\eta)$. As with static traces, for any state name $t$ appering in the trace (i.e. $t\in\mathrm{Dom}(\eta)$), we denote by $t(\eta)$ the longest prefix of $\eta$ preceding state name $t$. We denote singleton traces $(\omega)$.

Definition 4.3 (Sequent-Level State).

We define sequent-level state $\mathfrak{S}(\eta;~{}H)$ for dynamic and static traces $\eta$ and $H$. Recall that after ${\tt eq}(x,x_{i},\theta)$ the variable $x$ represents the end state of the assignment, while after ${\tt sub}(x,\theta)$ it represents the start state. We take each program variable $x$ from its most recent ${\tt eq}(x,x_{i},\theta)$ or ${\tt any}(x,x_{i})$ state, or the initial state if none exists. Each ghost is assigned at most once and takes its value from the state in which it was assigned. We give an inductive definition:

[TABLE]

5. Discrete Dynamic Kaisar

We now extend Kaisar with its core feature: nominal terms. We add a construct state $t$ which gives a name $t$ to the current abstract proof state, after which we can write nominal terms $t(\theta)$ to reference the value of term $\theta$ at state $t$ from future states. Nominal terms are supported by structured symbolic execution rules for each program construct, which automatically maintain the corresponding static execution trace. As before we proceed from examples to syntax and proof-checking rules.

Examples

We continue the proof of Model 1, augmenting it with loop invariants and other discrete program reasoning, but we leave differential equation reasoning for Section 6. Recall the program and statement of Theorem 2.1 (Skydiver Safety for Model 1):

[TABLE]

Proposition 5.1.

$r=a\land{dc}\land{const}\land{dyn}\rightarrow[\{\mathit{ctrl};\mathit{plant}\}^{*}](x=0\rightarrow v\leq m)$* is valid.*

Examples 2(a-c) are proofs of this Proposition 2.1 (with differential equation reasoning postponed until Section 6). As before, we proceed from basic to advanced proof techniques. Examples 2(a,b) both use a single loop invariant, and begin by splitting the conclusion into $[\{ctrl;plant\}](dc\land const)$ and $[\{ctrl;plant\}]dyn$ to separate the discrete and continuous reasoning. Example 2a splits eagerly on the control decision, which is straightforward but often requires duplication of proofs about the plant. Example 2b uses Hoare-style composition reasoning instead, which reduces duplication. In general, Hoare-style composition adds the cost of the user supplying a composition formula $I$, but $I$ is trivial in this case. Example 2c proves the loop invariants $\mathit{dc},\mathit{const},\mathit{dyn}$ separately, which is useful in interactive proofs when some invariants ($\mathit{dc},\mathit{const}$) prove trivially while others ($\mathit{dyn}$) are complex. Example 2d proves a slightly different theorem which establishes a bound on the position $x$, showcasing discrete nominals ($init(v),init(x)$). More advanced uses of nominals are in the full proof in Section 6.

Structured Symbolic Execution

Symbolic execution is implemented by adding to the class of structured proofs (SP) a set of box rules (BRs) for proving formulas of the form ${[{\alpha}]}\phi$ and a set of diamond rules (DR) for proving formulas of form ${\langle{\alpha}\rangle}\phi$. The diamond rules are largely symmetric to the box rules, so we only present the box rules here and give the full list of rules in Appendix C:

[TABLE]

To improve concision, many proof languages automate steps deemed obvious (Rudnicki, 1987; Davis, 1981). For us, these include the rules for the $\alpha;\beta$ and $?(\phi)$ connectives, i.e. reducing sequential compositions $[\alpha;\beta]\phi$ to nested modalities $[\alpha][\beta]\phi$ and assertions $[?P]Q$ to implications $P\rightarrow{Q}$. Negations are implicitly pushed inside other connectives, e.g. $\neg(P\land{Q})\leftrightarrow(\neg{P})\lor(\neg{Q})$ and $\neg{[{\alpha}]}\phi\leftrightarrow{\langle{\alpha}\rangle}\neg\phi$. These implicit rules reduce verbosity by automating obvious steps. This also enables us, for example, to reuse the $(\textbf{assume}~{}x:p~{}{\tt SP})$ rule for implication as if it applied to tests as well, as in Example 2a.

Because structured symbolic execution rules affect the trace, we now extend the ${\tt SP}$ checking judgment to $\left({H_{1}}\leadsto{H_{2}}\right){\tt SP}:\left({\Gamma}\vdash{\Delta}\right)$ where $H_{1}$ is the initial trace and $H_{2}$ is the final trace. The final trace helps reference the internal states of one subproof within another: see the after rule.

[TABLE]

The assignment rule itself is completely transparent to the user, but its presence as an explicit rule aids readability and supports the implementation of nominals. As discussed in Section 4, assignments update the trace because they modify the state. How they update the trace depends on whether we can perform assignment by substitution or whether we must add an equality to $\Gamma$:

[TABLE]

Nondeterministic assignment is analogous to the equality case of assignment:

[TABLE]

Nondeterministic choices are proven by proving both branches, matched by patterns $p$ and $q$:

[TABLE]

This case rule is notable because it produces non-exhaustive final traces. In general, an execution of $\alpha\cup\beta$ executes $\alpha$ or $\beta$, but not both. We return the input trace $H$ because the final trace only contains changes which (are syntactically obvious to) occur in every branch. This means any states introduced in ${\tt SP}_{\alpha}$ or ${\tt SP}_{\beta}$ have local scope and cannot be accessed externally.

Definition 5.2 (Abstraction).

When executing certain programs $\alpha$, it is not known exactly which variables are bound on a given run of $\alpha$. In these cases, we can reason by abstraction over all bound variables $\mathop{\text{BV}}(\alpha)$: we treat their final values as arbitrary. Abstraction is denoted with superscripts ${\phi}^{\alpha},$ not to be confused with subscripts, which are mnemonic. Let $\mathop{\text{BV}}(\alpha)=x_{1},\ldots,x_{n}$ and $y_{1},\ldots,y_{n}$ fresh ghost variables. We define ${H}^{\alpha}=H,{\tt any}(x_{1},y_{1}),\ldots{\tt any}(x_{n},y_{n})$, ${\phi}^{\alpha}={\phi}_{x_{1}}^{y_{1}}\cdots{}{~{}}_{x_{n}}^{y_{n}}$, and ${\omega}^{\alpha}=\eta,{\omega}_{x_{1}}^{\omega(y_{1})}\cdots{}{~{}}_{y_{n}}^{\omega(x_{n}))}$. In Section 7 we show soundness and nominalization results for abstraction.

As shown in Example 2a, using case too soon increases the complexity of a proof: in a proof of $\{\alpha\cup\beta\};\gamma,$ the proof of $\gamma$ may be duplicated. Example 2b reduces proof size with Hoare-style (Hoare, 1969) composition by specifying an intermediate condition $\psi$ which holds between $\{\alpha\cup\beta\}$ and $\gamma$.

[TABLE]

Hoare composition is notable because $H_{\psi}$ contains only changes that happened with certainty: the bound variables of $\alpha$ may have been modified in ways not reflected by $H_{\alpha}$. Thus we treat the values of bound variables after running $\alpha$ as arbitrary, abstracting over them.

The state construct gives a name to the current program state. This has no effect on the proof state, but allows that state to be referenced later on by nominal terms, as shown in Example 2c:

[TABLE]

Invariant Proofs

We verify discrete loops via invariants. Consider the proofs in Figure 2. In Examples 2a and 2b we prove a single loop invariant, where the base case proves automatically, as is often the case. In Example 2c we subdivide the proof into several invariants which we prove successively. These styles of proof are interchangeable, but the latter is convenient during proof development to separate simple cases from difficult cases.

If (as in Example 2c) an invariant is provable automatically, we may omit the branches Pre and Ind. After proving invariants, the finally keyword returns us to a standard structured proof with all invariants available as assumptions.

[TABLE]

While checking invariant proofs, we add a context $J{\rm{s}}{}$ of all the invariants, which are made available both while proving further invariants and at the end of the invariant chain. As in Hoare composition, we abstract over the history because the inductive step must work after any number of iterations.

[TABLE]

[TABLE]

Focus

The box rules presented here implicitly operate on the first formula of the succedent. In the common case of proving a safety theorem $\phi\rightarrow{[{\alpha}]}\psi$ where all tests $?(\phi)$ contain only first-order arithmetic, this is enough. Hewever, this does not provide completeness for liveness properties ${\langle{\alpha}\rangle}\phi$ which produce multi-formula succedents, or for tests containing modalities. We restore completeness for these cases, extending the class SP with a focus construct which brings an arbitrary formula (selected by pattern-matching) to the first succedent position:

A focus in the antecedent is the inverse of $\neg{R}$; in the succedent it is the exchange rule:

[TABLE]

Recall that negations are pushed inward implicitly, so upon focusing a formula ${[{\alpha}]}\phi$ from the antecedent, we will ultimately have ${\langle{\alpha}\rangle}\neg{\phi}$ in the succedent, for example. As with case, the subproof ${\tt SP}$ can access both the initial trace $H$ and any local changes from the proof of $\neg\phi$, but any such changes leave scope here. Regardless of the origin of $\neg\phi,$ any structured symbolic execution proof can employ state-based reasoning, but as with case it does not follow that those state changes remain meaningful in any broader context.

In Section 7 we show that focus, combined with the execution rules for boxes and diamonds in the succedent, provides completeness. This formulation minimizes the core proof calculus, but focus-based derived rules for antecedent execution may be useful in practice. The completeness proof of Section 7 provides intuition for how such constructs would be derived.

Extended Expressions and Patterns

Discrete Dynamic Kaisar adds nominal terms $t(\theta)$ (where $t$ is the name of some named state) to the language of expressions $e$. This change raises a design question: when defining an abbreviation, should program variables refer to their bind-time values, or their expand-time values? We choose bind-time evaluation as the default, so $\bar{e}$ evaluates nominals, performing structural recursion and using the rules of Section 4 in the variable case. When a variable $x$ appears outside a nominal, it is interpreted at the current state, which we denote here using the notation $now(x)$. For pattern-matching to work with nominals, matching against (program) variable patterns performs expansion before matching:

[TABLE]

We also want the option to mix bind-time and expand-time reference, for example in Section 6. This enables reusable definitions that still refer to fixed past values. We support this with a new functional variant of the let construct, which is parameterized by a state $t$. Any subterm $\theta$ under the nominal $t(\_)$ uses the expand-time state, while plain subterms use the bind-time state:

[TABLE]

Functional let uses a let mobilization helper judgment, which (a) expands references to current-state variables and (b) wraps all references to arguments in the $now(x)$ pseudo-nominal:

[TABLE]

Note that due to the addition of functional let, the context $\Gamma$ may now contain extended terms. As before, any unadorned variable $x$ in $\Gamma$ refers to the current sequent-level meaning of $x$. Elements of $\Gamma$ can contain extended subterms $now(\theta)$ (for proper terms $\theta$), which are adequately resolved by recursively evaluating any extended terms found during expansion:

[TABLE]

6. Differential Dynamic Kaisar

We extend Kaisar to support differential equations, the defining feature of differential dynamic logic. The examples of this section illustrate the necessity of historical reference to both initial and intermediate states. We show that nominals work even when mixing discrete and continuous invariants, continuous ghosts necessary for ODEs and first-order reasoning necessary for arithmetic.

Examples

First we complete the proof of Model 1. Recall the statement of Theorem 2.1:

[TABLE]

Theorem 6.1 (Skydiver Safety).

$r=a\land{dc}\land{const}\land{dyn}\rightarrow[(\mathit{ctrl};\mathit{plant})^{*}](x=0\rightarrow v\leq m)$* valid*

The proof mirrors the natural-language proof of Section 2.1 and builds upon Examples 1 and 2. Recall that we use differential invariants to reason about the drag equation, because it does not have a closed-form solution in decidable real arithmetic. In the open-parachute case, recall that while dyn is invariant ($\lvert v\rvert$ never reaches the bound $\sqrt{\frac{g}{p}}$) it is not inductive because it approaches the bound asymptotically. Adding a differential ghost (Platzer, 2011) variable $y$, makes it possible to write an equivalent invariant that holds inductively. An equivalent invariant can be derived mechanically: in this case $y^{2}\cdot\left(v+\sqrt{\frac{g}{p}}\right)=1$ which implies $\lvert v\rvert<\sqrt{\frac{g}{p}}$.

Having finished the proof of Model 1, we consider a second example system that does have solvable continuous dynamics, in which case ODEs can be symbolically executed directly without appealing to differential invariants. Consider a one-dimensional model of a bouncing ball, with vertical position $y$, vertical velocity $v$, acceleration due to gravity $g$ and initial height $H$. This perfectly-elastic bouncing ball discretely inverts its velocity whenever it hits the ground ($y=0$). Because it started with $v=0$, we will prove that it never exceeds the initial height. At the same time, we prove that it never goes through the floor ($y\geq 0$):

Model 2 (Safety specification for bouncing ball).

[TABLE]

The proof in Figure 4 follows physical intuitions: total energy ($E\_$) is conserved, from which we show arithmetically that the height bound always holds.

Because this example has a solvable ODE, it suffices to add a construct for solving ODEs (below, dom is short for domain constraint):

[TABLE]

Lastly, consider the proof in Example 3. We reason about unsolvable ODEs using differential invariants (Platzer, 2016, 2012a, 2010) and differential ghosts (Platzer, 2011), which we add to the syntax of invariant proofs:

[TABLE]

Unlike in loops, it is essential for soundness that we do not assume the current invariant (only previous invariants) while proving it. Differential invariant (Platzer, 2007a) reasoning uses the differential of a formula $(\phi)^{\prime}$ to compute its Lie derivative, and then proves it to be inductive. Traces are general enough to support loops and differental equations uniformly. Because the differential equation $\alpha$ will modify $x$, we abstract over the variables of $\alpha\equiv{\{x^{\prime}=\theta~{}\&~{}Q\}}$ (i.e. $x$):

[TABLE]

[TABLE]

[TABLE]

When introducing a new variable $y$, we ensure the right-hand side of $y^{\prime}$ is linear in $y$ to ensure the existence interval of the ODE does not change, which is essential for soundness (Platzer, 2011).

7. Metatheory

The value of a nominal $t(\theta)$ in the sequent-level state agrees with the value of $\theta$ in the corresponding program state. We begin here with the simplest case, pseudo-nominals of variables $\mathrm{now}_{H}(x)$, from which we then derive nominals of variables $\mathrm{t}_{H}(x)$ and arbitrary nominals $\mathrm{t}_{H}(\theta)$.

Lemma 7.1.

For all $\eta\sim{H}$ and all variables $x$, ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={\tt last}(\eta)(x)$.

Straightforward induction on the derivation of $\eta\sim{H}$.

Case $(\nu)\sim{\epsilon{}}$: Then ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{(\nu)}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\nu}=\nu(x)={\tt last}(\eta){x}$.

Case $\eta^{\prime},\omega\sim{H^{\prime},{\tt any}(x,x_{i})}$: Then ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}=\mathfrak{S}(\eta;~{}H)(x)=\omega(x)={\tt last}(\eta)(x)$.

Case $\eta^{\prime},\omega\sim{H^{\prime},{\tt eq}(x,x_{i},\theta)}$: Then ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}=\mathfrak{S}(\eta;~{}H)(x)=\omega(x)={\tt last}(\eta)(x)$.

Case $\eta^{\prime},\omega\sim{H^{\prime},{\tt sub}(x,\theta)}$: Then ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}={\tt last}(\eta)(x)$, where the last equation is from the definition of $\sim{}$.

Case $\eta^{\prime},t\sim{H^{\prime},t}$: Then ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H^{\prime}}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}={\tt last}(\eta^{\prime})(x)={\tt last}(\eta){x}$. The remaining cases are symmetric.

This lemma generalizes to arbitrary nominals, but first it will require the generalization of the coincidence theorem for dL formulas  (Platzer, 2015) to nominals:

Lemma 7.2 (Coincidence for “now”).

If $\eta\sim{H}$ and $y\notin\mathop{\text{FV}}(H)$ then ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{{\mathfrak{S}(\eta;~{}H)}_{y}^{r}}$ for all $y\neq{x}$ and $r\in\mathbb{R}$.

By induction on $\eta\sim{H}$.

Case $(()\omega)\sim{\epsilon{}}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}=\omega(x)={\omega}_{y}^{r}(x)$ because $x\neq{y}$.

Case $\eta^{\prime},\omega\sim{H^{\prime},{\tt any}(x,x_{i})}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}x\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}=\omega(x)={\omega}_{y}^{r}(x)$ because $y\neq{x}$.

Case $\eta^{\prime},\omega\sim{H^{\prime},{\tt eq}(x,x_{i},\theta)}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}x\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}=\omega(x)={\omega}_{y}^{r}(x)$ because $y\neq{x}$.

Case $\eta^{\prime},\omega\sim{H^{\prime},{\tt sub}(x,\theta)}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}_{y}^{r}}$ by term coincidence (Platzer, 2015) and because $y\notin\mathop{\text{FV}}(\theta)$ when $y\notin\mathop{\text{FV}}(H)$.

Case $\eta^{\prime},t\sim{H,t}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H^{\prime}}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H^{\prime}}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}_{y}^{r}}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{{\mathfrak{S}(\eta;~{}H)}_{y}^{r}}$. The remaining cases are symmetric.

Lemma 7.3 (Coincidence for Nominals).

If $\eta\sim{H}$ and $y\neq{\mathop{\text{FV}}(H)}$ and $x\neq{y}$ then ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{{\mathfrak{S}(\eta;~{}H)}_{y}^{r}}$.

Case $(\omega)\sim{\epsilon{}}$: True by contradiction.

Case $\eta,\omega\sim{H,{\tt any}(x,x_{i})}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}=_{def}{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H^{\prime}}(x_{i})\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}=_{IH}{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H^{\prime}}(x_{i})\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}_{y}^{r}}=_{def}{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}_{y}^{r}}$ by invariants for $\sim{}$. The proof for $h,{\tt eq}(x,x_{i},$) is symmetric.

Case $\eta,\omega\sim{H,{\tt sub}(x,\theta)}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H^{\prime}}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H^{\prime}}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}_{y}^{r}}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{{\mathfrak{S}(\eta;~{}H)}_{y}^{r}}$. All other cases except $H,t$ are symmetric.

Case $\eta,t\sim{H,t}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}_{y}^{r}}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{{\mathfrak{S}(\eta;~{}H)}_{y}^{r}}$ by Lemma 7.2.

Given the coincidence lemmas above, we have correspondence for nominals of variables:

Lemma 7.4 (Correspondence for Nominals).

For all $\eta\sim{H}$, all state names $t\in\mathrm{Dom}(H)$, and all variables $x$, ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}=t(\eta)(x)$.

By induction on the derivation $\eta\sim{H}$.

Case $(\nu)\sim{\epsilon{}}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\nu;~{}H)}=\nu(x)=t(\eta)(x)$.

Case $\eta^{\prime},\omega\sim{H^{\prime},{\tt any}(x,x_{i})}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H^{\prime}}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})_{x}^{\omega(x)}}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H^{\prime}}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}=t(\eta^{\prime})(x_{i})=t(\eta^{\prime})(x)=t(\eta)(x)$, by definition of $\mathrm{t}_{H}(x)$ and $\mathfrak{S}$, induction, definition of $\sim{}$ and definition of $t(\eta)$ respectively.

Case $\eta^{\prime},\omega\sim{H^{\prime},{\tt eq}(x,x_{i},\theta)}$: Symmetric.

Case $\eta^{\prime},\omega\sim{H^{\prime},{\tt sub}(x,\theta)}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H^{\prime}}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}=t(\eta^{\prime})(x)=t(\eta)(x)$.

Case $\eta^{\prime},t\sim{H,t}$: ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{t}_{H}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}H)}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H^{\prime}}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta^{\prime};~{}H^{\prime})}={\tt last}(\eta^{\prime})(x)=t(\eta)(x)$ by Lemma 7.3.

Case other: Symmetric.

Furthermore, note that prefixes preserve correctness of nominalization, thus nominals behave correctly even when evaluated from an intermediate state of $\eta$:

Corollary 7.5.

For all $\eta\sim{H}$, all state names $s\leq{t}\in\mathrm{Dom}(H)$, all variables $x$, ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{s}_{t(H)}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}t(H))}=s(t(\eta))(x)$

From Lemma 7.4, it suffices to show for any $\eta\sim{H}$ and $t\in\mathrm{Dom}(H)$ that $t(\eta)\sim{t(H)}$, which holds by a trivial induction since $\eta\sim{H}$ contains a derivation $\eta^{\prime}\sim{H^{\prime}}$ for all same-length prefixes $\eta^{\prime}$ and $H^{\prime}$, including $t(\eta)$ and $H(\eta)$. Then note since $s\leq{t}\in{H}$ then $s\in\mathrm{Dom}(t(H))$, so the preconditions of the lemma are satisfied.

Because the meaning of nominal terms is uniquely determined by the meaning of nominal variables, the above lemmas suffice to show that all nominal and pseudo-nominal terms are well-behaved:

Theorem 7.6 (Nominal Term Correspondence).

For all $\eta\sim{H}$, all state names $s\leq{t}\in\mathrm{Dom}(H)$, all terms $\theta$, ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{s}_{t(H)}(\theta)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}t(H))}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{s(t(\eta))}$.

By induction on the structure of terms $\theta$.

Case $\theta=x$: Then ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{s}_{t(H)}(\theta)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}t(H))}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{s}_{t(H)}(x)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}t(H))}=s(t(\eta))(x)={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{s(t(\eta))}$ by corollary above.

Case $\theta=q\in\mathbb{Q}$: Then ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{s}_{t(H)}(\theta)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}t(H))}=q={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{s(t(\eta))}$.

Case $\theta=\otimes(\theta_{1},\theta_{2})$ for any operator $\otimes$: Then ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{s}_{t(H)}(\theta)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}t(H))}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{s}_{t(H)}(\otimes(\theta_{1},\theta_{2}))\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}t(H))}=\otimes({{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{s}_{t(H)}(\theta_{1})\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}t(H))},{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{s}_{t(H)}(\theta_{2})\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta;~{}t(H))})=\otimes({{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta_{1}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{s(t(\eta))},{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta_{2}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{s(t(\eta))})={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\otimes(\theta_{1},\theta_{2})\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{s(t(\eta))}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{s(t(\eta))}.$

In the above theorems, we assumed that the dynamic and static traces are always in correspondence $\eta\sim{H}$ holds. We now show that this is always the case at every proof state within a proof:

Theorem 7.7 (Intermediate Nominal Term Correspondence).

For any program $\alpha$ with $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and any $\eta_{\omega}\sim{H}$ where ${\tt last}(\eta_{\omega})=\omega$ and $\left({H}\leadsto{H_{1}}\right){\tt SP}:\left({\Gamma}\vdash{\mathrm{now}_{H}([\alpha]\phi)}\right)$ there exists $\eta_{\nu}$ where ${\tt fst}(\eta_{\nu})=\nu$ and $\eta_{\omega}\eta_{\nu}\sim{H_{1}}$.

Note that ${\tt last}(\eta_{\nu})$ is not always $\nu$: Following the proof-checking rules, any states defined inside the nondeterministic constructs $\alpha\cup\beta$ and $\alpha^{*}$ leave scope and are absent in the final trace. Since the theorem holds inductively at every proof state it thus shows that even for choices and loops, nominals have their intended meaning in the local context.

The proof is by induction on the derivation $\left({H}\leadsto{H^{\prime}}\right){\tt SP}:\left({\Gamma}\vdash{[\alpha]\phi}\right)$. The only significant cases are those which modify the trace.

Case show: Let $\eta_{\omega}^{\prime}=\eta_{\omega}$ and $\eta_{\nu}=({\tt last}(\eta_{\omega})),$ then $\eta_{\omega}^{\prime}\eta_{\nu}=\eta_{\omega}$ and $H^{\prime}=H$ so $\eta_{\omega}^{\prime}\eta_{\nu}\sim{H^{\prime}}$ because $\eta_{\omega}\sim{H}$ by assumption.

Case $\left(\textbf{case}~{}p_{\alpha}~{}\Rightarrow~{}{\tt SP}_{1}~{}|~{}p_{\beta}~{}\Rightarrow~{}{\tt SP}_{2}\right)$: Let $\eta_{\omega}^{\prime}=\eta_{\omega}$ and $\eta_{\nu}=({\tt last}(\eta_{\omega})),$ then $\eta_{\omega}^{\prime}\eta_{\nu}=\eta_{\omega}$ and $H^{\prime}=H$ so $\eta_{\omega}^{\prime}\eta_{\nu}\sim{H^{\prime}}$ because $\eta_{\omega}\sim{H}$ by assumption.

Case $\textbf{assign}~{}x:=\tilde{\theta}~{}{\tt SP}$, $\alpha=x:=\mathrm{now}_{H}(\theta);\mathrm{now}_{H}(\alpha^{\prime}),x\notin\mathop{\text{BV}}(\alpha^{\prime})$: Let $H^{*}=H,{\tt sub}(x,\mathrm{now}(H){\theta}),\eta^{*}=\eta,\omega,{\omega}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}}$. To show $\eta^{*}\sim{H^{*}}$ it suffices to show ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}(H){\theta}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta,\omega;~{}H)={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}}$ which holds by Theorem 7.6. To apply the IH, lastly observe $\mathrm{now}_{H^{*}}(\alpha^{\prime})={\mathrm{now}_{H}(\alpha^{\prime})}_{x}^{\mathrm{now}_{H}(\theta)}$. Then by IH, $\exists\eta^{*}_{\nu}~{}{\tt fst}(\nu)={\omega}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}}$, so let $\eta_{\nu}=\omega,\eta^{*}_{\nu}$ and observe $\eta,\omega,{\omega}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}},\eta^{*}_{\nu}=\eta,\omega,\eta^{*}$ so $\eta,\omega,\eta^{*}\sim{H^{\prime}}$ by IH.

Case $\textbf{assign}~{}x:=\tilde{\theta}~{}{\tt SP}$, $\alpha=x:=\mathrm{now}_{H}(\theta);\mathrm{now}_{H}(\alpha^{\prime}),x\in\mathop{\text{BV}}(\alpha^{\prime})$: By symmetry since the rule for $\eta,\omega\sim{H,{\tt eq}(x,x_{i},\theta)}$ is symmetric with $\eta,\omega\sim{H,{\tt sub}(x,\theta)}$. To apply the IH observe $hnow{H^{*}}{\alpha^{\prime}}=\mathrm{now}_{H}(\alpha^{\prime})$.

Lemma 7.8 (Ghosting).

If $\eta,\omega\sim{H}$ and $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then $\exists\eta_{\nu}~{}(\eta,\omega,\eta_{\nu})\sim{{H}^{\alpha}}$.

Let $x_{1},\ldots,x_{n}=\mathop{\text{BV}}(\alpha)$. Define $\omega_{1}={\omega}_{x_{1}}^{\nu(x_{1})},\omega_{i}={\omega_{i-1}}_{x_{i}}^{\nu(x_{i})}$ for all $i\leq n$. Then $\omega_{n}=\nu$ because by bound effect $\omega$ and $\nu$ differ only by $\mathop{\text{BV}}(\alpha)$. By definition, ${H}^{\alpha}=H,{\tt any}(x_{1},x_{1}^{*}),\ldots,{\tt any}(x_{n},x_{n}^{*})$ for ghosts $x_{i}^{*}$. Then let $\eta_{\nu}=\eta,\omega,\omega_{1},\ldots,\omega_{n}$ and the result holds.

Case ($(\textbf{after}{}~{}\{{\tt SP}_{1}\}~{}\textbf{have}{}~{}x:\phi~{}\textbf{then}{}~{}\{{\tt SP}_{2}\})$ and $(\alpha=\alpha_{1};\alpha_{2})$): By inversion on $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{},\exists\mu~{}(\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha_{1}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $(\mu,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha_{2}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By the IH on ${\tt SP}_{1},\exists\eta_{\mu}\sim{H^{\prime}}$. Let $\vec{x}=x_{1},\ldots,x_{n}=\mathop{\text{BV}}(\alpha)$ then define $H^{*}=H,{\tt any}(x_{1},x_{1,i}),\ldots,{\tt any}(x_{n},x_{n,i})$ and define $\omega_{1}={\omega}_{x_{1}}^{\mu(x_{1})},\omega_{i}={\omega_{i-1}}_{x_{i}}^{\mu(x_{i})}$ for all $i\leq n$, then observe $\omega_{n}=\mu$ because by bound effect (Platzer, 2015) for programs, $\omega$ and $\mu$ differ only on $\mathop{\text{BV}}(\alpha)$. Let $\eta^{*}=\eta,\omega,\omega_{1},\ldots,\omega_{n}$ and observe $\eta^{*}\sim{H^{*}}$ so we can apply the IH on ${\tt SP}_{2}$, yielding $\exists\eta^{*}_{\nu}\sim{H^{\prime\prime}}$. Now let $\eta_{\nu}={\tt any}(x_{1},x_{1,i}),\ldots,{\tt any}(x_{n},x_{n,i}),\eta^{*}_{\nu}$ and observe $\eta,\omega,\eta^{*}=\eta,\omega,{\tt any}(x_{1},x_{1,i}),\ldots,{\tt any}(x_{n},x_{n,i}),\eta^{*}_{\nu}$ so $\eta,\omega,\eta_{\nu}\sim{H^{\prime\prime}}$, concluding the case.

Case $\textbf{assume}~{}x:\tilde{\phi}~{}{\tt SP},\alpha=?(\phi);\alpha_{1}$: Let $H^{*}=H,\eta^{*}=\eta$ then $\eta^{*}\sim{H^{*}}$ and by IH $\exists\eta^{*}_{\nu}$ where $\eta^{*}\eta^{*}_{\nu}\sim{H^{\prime}}$. Let $\eta_{\nu}=\eta^{*}_{\nu}$ and the result holds by definition of $\eta^{*}$ and $\eta_{\nu}$.

Case $\textbf{let}~{}p~{}=~{}\tilde{e}~{}{\tt SP}$: Symmetric.

Case $\textbf{let}~{}t(?x)~{}=~{}\tilde{e}~{}{\tt SP}$: Symmetric.

Case $\textbf{note}~{}x~{}=~{}{\tt FP}~{}{\tt SP}$: Symmetric.

Case $\textbf{have}~{}x:\tilde{e}~{}{\tt SP}_{1}~{}{\tt SP}_{2}$: Symmetric, except apply the IH on ${\tt SP}_{2}$.

Case $\textbf{state}~{}t~{}{\tt SP}$: Let $H^{*}=H,t$ and $\eta^{*}=\eta,t$ so $\eta^{*}\sim{H^{*}}$ so the result follows by IH.

Case $\textbf{solve}~{}p_{ode}~{}t\colon{}{}p_{t}~{}\ dom\colon{}{}p_{dom}~{}{\tt SP}$: By inversion on $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}x^{\prime}=\theta;\alpha_{1}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ there exists $\mu={\omega}_{x}^{y(t)}$ for some $t\geq 0$ such that $\forall s~{}\in~{}[0,t]~{}Q(s)$ and where $(\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}x^{\prime}=\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $(\mu,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha_{1}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Let $H^{*}=H,{\tt sub}(x,y(t))$ and $\eta^{*}=\eta,\omega,{\omega}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}y(t)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}}$ then have $\eta^{*}\sim{H^{*}}$ by Theorem 7.6 saying ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}y(t)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathrm{now}_{H}(y(t))\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\mathfrak{S}(\eta,\omega;~{}H)}$ for any such $t$. Then we can apply the IH since $\mathrm{now}_{H^{*}}(\alpha_{1})=\mathrm{now}_{H}({\alpha_{1}}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}y(t)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}})$, yielding $\eta^{*}_{\nu}$ where $\eta,\omega,{\omega}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}y(t)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}},\eta^{*}_{\nu}\sim{H^{\prime}}$. So let $\eta_{\nu}={\omega}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}y(t)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}},\eta^{*}_{\nu}$ and the result holds.

Case $\textbf{inv}~{}J:\tilde{\phi}\{\textbf{Pre}~{}\Rightarrow~{}{\tt SP}_{1}~{}|~{}\textbf{Ind}~{}\Rightarrow~{}{\tt SP}_{2}\}~{}{\tt IP},\alpha=\alpha^{*}_{1};\alpha_{2}$: Let $H^{*}=H,\eta^{*}=\eta$ then $\eta^{*}\sim{H^{*}}$. by IH $\exists\eta^{*}_{\nu}$ where $\eta,\omega,\eta^{*}_{\nu}\sim{H^{\prime}}$ so let $\eta_{\nu}=\eta^{*}_{\nu}$ and then $\eta,\omega,\eta_{\nu}\sim{H^{\prime}}$.

Case $\textbf{finally}~{}{\tt SP},\alpha=\alpha_{1}^{*};\alpha_{2}$: By inversion, exists $\mu$ where $(\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha_{1}^{*}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $(\mu,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha_{2}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By Lemma 7.9 have ${\eta,\omega}^{\alpha}\sim{{H}^{\alpha}}$ (where ${(\eta,\omega)}^{\alpha}=\eta,\omega,\omega_{1},\ldots,\omega_{n}$) and by bound effect (Platzer, 2015) lemma have $\omega_{n}=\mu$. By IH have $\eta^{*}_{\nu}$ where $\eta,\omega,\omega_{1},\ldots,\omega_{n},\eta^{*}_{\nu}\sim{H^{\prime}}$ so let $\eta_{\nu}=\omega_{1},\ldots,\omega_{n},\eta^{*}_{\nu}$.

Case $\textbf{inv}~{}J:\tilde{\phi}\{\textbf{Pre}~{}\Rightarrow~{}{\tt SP}_{1}~{}|~{}\textbf{Ind}~{}\Rightarrow~{}{\tt SP}_{2}\}~{}{\tt IP},\alpha=\{x^{\prime}=\theta\};\alpha_{2}$: Symmetric to the case for loops.

Case $\textbf{Ghost}~{}y\mathrel{{:}{=}}\theta_{3};y^{\prime}=\theta_{2}~{}{\tt IP},\alpha=\{x^{\prime}=\theta\};\alpha_{2}$: By inversion, $\exists\mu={\omega}_{x}^{\varphi(t)}$ for some $t\geq 0$ such that $\varphi(t)$ is the solution of $x^{\prime}=\theta$ for time $t$ and $\forall s\in[0,t]~{}{\omega}_{x}^{\varphi(t)}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $(\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\{x^{\prime}=\theta\}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $(\mu,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha_{2}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By linearity of $\{y^{\prime}=\theta_{2}\}$, the solution of $\{x^{\prime}=\theta,y^{\prime}=\theta_{2}\}$ exists for the same time $t$ and the solution agrees on $x$. Since $y$ is a ghost variable then $y\notin\mathop{\text{FV}}(\alpha_{2})$ and so $(\mu,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha_{2}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ so the IH applies and $\exists\eta^{*}_{\nu}$ where $\eta\omega,\eta^{*}_{\nu}\sim{H^{\prime}}$ and letting $\eta_{\nu}=\eta^{*}_{\nu}$ the result holds.

Case $\textbf{finally}~{}{\tt SP},\alpha=\{x^{\prime}=\theta\};\alpha_{2}$: Symmetric to the case for loops, except note $\mathop{\text{BV}}(\{x^{\prime}=\theta\})=\{x,x^{\prime}\}$ so we apply the bound effect (Platzer, 2015) lemma only for $x$. We assume as a side condition that $x^{\prime}\notin{\mathop{\text{FV}}(\eta)}$ in which case $\eta^{*}\sim{H^{*}}$ still holds when setting $\omega_{n}(x^{\prime})=\mu(x^{\prime})$.

7.1. Nominalization

The relation $\eta\sim{H}$ relates static and dynamic traces, but not the executed program $\alpha$. We wish for the trace $\eta_{\nu}$ to assign each nominal $t$ the actual state that $\alpha$ had during the state $t$ in the proof.222Since we can add names at any point in a proof, this implies that the proof and program agree at every state.

We show this with semantics of the nominal hybrid logic d$\mathcal{L}_{h}$, (Platzer, 2007b) which extends the logic of dL with propositions $t$ which are true iff the current state is the unique state identified by $t$.333d$\mathcal{L}_{h}$ also adds propositions $@_{i}\phi$ indicating truth of $\phi$ in state $\phi$, but they are not needed to specify our metatheory. Accordingly, we extend the semantics with interpretations that assign a specific state to each $t$. We write the interpretation corresponding to a trace $\eta$ as $\mathit{interp}(\eta)$, i.e. the interpretation which maps each $t$ to ${\tt last}(t(\eta))$. Thus $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta)}$ means $\phi$ holds in state $\omega$ in the interpretation constructed from $\eta$, and likewise for $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta)}$. We give a nominalization judgment $nom({\alpha},{{\tt SP}})={\alpha_{h}}$ which augments a program $\alpha$ with a test $?(t)$ for each named state $\textbf{state}~{}t~{}$ in ${\tt SP}$, producing a d$\mathcal{L}_{h}$ program $\alpha_{h}$. Every transition of $\alpha_{h}$ is a transition of $\alpha$ because we do not introduce state mutation. We show the converse holds too: all our additional tests (which depend solely on $\mathit{interp}(\eta)$) pass. This formally justifies the claim that the states of $\eta$ match the states of $\alpha$:

Theorem 7.9.

If $\left({H}\leadsto{H_{\alpha}}\right){\tt SP}:\left({\Gamma}\vdash{[\alpha]\phi,\Delta}\right)$ for $\eta,\omega\sim{H}$ and $\eta,\omega,\eta_{\nu}\sim{H_{\alpha}}$ then let $\nu$ such that $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Then in d$\mathcal{L}_{h}$, $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}nom(\alpha,{\tt SP})\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta)}$.

By induction on the derivation of $\left({H}\leadsto{H^{\prime}}\right){\tt SP}:\left({\Gamma}\vdash{[\alpha]\phi}\right)$. The essence of the proof is the definition of $nom({\alpha},{{\tt SP}})={\alpha^{\prime}}$:

[TABLE]

Throughout the proof, let $\eta^{\prime}\equiv\eta,\omega,\omega^{*}_{\nu}$, that is the trace resulting from the IH, such that $\eta^{\prime}\sim{H^{\prime}}$.

Case $nom({?(\phi);\alpha},{\textbf{assume}~{}x:\phi~{}{\tt SP}})={?(\phi);nom(\alpha,{\tt SP})}$: By inversion $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By IH, $\exists\alpha^{\prime}~{}nom({{\tt SP}},{\alpha})={\alpha^{\prime}}$ and $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Then $nom({\textbf{assume}~{}x:\phi~{}{\tt SP}},{?(\phi);\alpha})={?(\phi),\alpha^{\prime}}$ and since $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $\phi$ is nominal-free, then $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$ for any $\eta^{\prime}$ and also $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ so $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}?(\phi);\alpha^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$.

Case $nom({\alpha},{\textbf{have}~{}x:\phi~{}{\tt SP}_{1}~{}{\tt SP}_{2}})={nom(\alpha,{\tt SP}_{2})}$: By the IH, $\exists\alpha^{\prime}~{}nom({{\tt SP}},{\alpha})={\alpha^{\prime}}$ and $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$ then by inversion $nom({\alpha},{\textbf{have}~{}x:\phi~{}{\tt SP}_{1}~{}{\tt SP}_{2}})={\alpha^{\prime}}$ for the same $\alpha^{\prime}$, completing the case.

Case $nom({\alpha},{\textbf{let}~{}p~{}=~{}\tilde{e}~{}{\tt SP}})={nom(\alpha,{\tt SP})}$: Symmetric.

Case $nom({\alpha},{\textbf{let}~{}t(?X)~{}=~{}\tilde{e}~{}{\tt SP}})={nom(\alpha,{\tt SP})}$: Symmetric.

Case $nom({\alpha},{\textbf{note}~{}x~{}=~{}{\tt FP}~{}{\tt SP}})={nom(\alpha,{\tt SP})}$: Symmetric.

Case $nom(\alpha^{*},\left(\textbf{case}~{}p_{\phi}~{}\Rightarrow~{}{\tt SP}_{\phi}~{}|~{}p_{\alpha}~{}\Rightarrow~{}{\tt SP}_{\alpha}\right))$: Symmetric.

Case $nom(\alpha,\textbf{focus}{}~{}p~{}{\tt SP})$: Symmetric.

Case $\textbf{after}{}~{}\{{\tt SP}_{\psi}\}~{}\textbf{have}{}~{}\psi~{}\textbf{then}{}~{}\{{\tt SP}_{\phi}\}$: By inversion, $\exists\mu~{}((\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}\land(\mu,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\beta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{})$. Split the trace $\eta,\omega¸\eta_{\nu}$ into $\eta,\omega,\eta_{\mu},\mu,\eta_{\nu}^{*}$. By IH1, $(\omega,\mu)\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}nom({\tt SP}_{1},\alpha)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta,\omega,\eta_{\mu},\mu)}}$. By interpretation weakening, $(\omega,\mu)\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}nom({\tt SP}_{1},\alpha)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta,\omega¸\eta_{\nu})}}$. By Lemma , IH2 is applicable and $(\mu,\nu)\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}nom({\tt SP}_{2},\beta)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta,\omega¸\eta_{\nu})}}$. The result holds by semantics of $[;]$.

Case $nom({\alpha},{\textbf{state}~{}t~{}{\tt SP}})={?t;nom(\alpha,{\tt SP})}$: Then by IH with $\eta^{*}=\eta,\omega,t$ and $H^{*}=H,t$ have $\exists\alpha^{\prime}~{}nom({{\tt SP}},{\alpha})={\alpha^{\prime}}$ for some $\alpha^{\prime}$ where $(\omega,\nu)\in_{\mathit{interp}(\eta^{\prime})}{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Then $nom({\alpha},{\textbf{state}~{}t~{}{\tt SP}})={?t;\alpha^{\prime}}$. We have $\mathit{interp}(\eta^{\prime})={\mathit{interp}(\eta^{*})}_{t}^{\omega}$. Since $\mathit{interp}(\eta^{\prime})=\mathit{interp}(\eta^{*})$ on $\Sigma(\alpha^{\prime})$ then by coincidence (Platzer, 2015), $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{*})}$. And by the definition of $\eta^{*}$ we have $\mathit{interp}(\eta^{*})(t)=\omega$ so $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}t\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{*})}$ and thus $(\omega,\nu)\in{?t;\alpha^{\prime}}{\mathit{interp}(\eta^{*})}$.

Case $nom({\alpha\cup\beta},{{\tt SP}})={\alpha\cup\beta}$: Since $(\omega,\nu){{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\cup\beta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\cup\beta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{*})}$ and since $nom({\alpha\cup\beta},{{\tt SP}})={\alpha\cup\beta}$ the case is complete.

Case $nom({x:=\theta;\alpha},{\textbf{assign}~{}x:=\tilde{\theta}~{}{\tt SP}})={x:=\theta;nom(\alpha,{\tt SP})}$: By IH $\exists\alpha^{\prime}~{}nom({{\tt SP}},{\alpha})={\alpha^{\prime}}$ then $nom({x:=\theta;\alpha},{\textbf{assign}~{}x:=\tilde{\theta}~{}{\tt SP}})={x:=\theta;\alpha^{\prime}}$ and $({\omega}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}},\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{*})}$ and since (by inversion) $(\omega,{\omega}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}})\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}x:=\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}}$ then also $(\omega,{\omega}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}})\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}x:=\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$ and finally $(\omega,\nu)\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}x:=\theta;\alpha^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}}$.

Case $nom({x\mathrel{{:}{=}}\ast;\alpha},{\textbf{assign}~{}x\mathrel{{:}{=}}\ast~{}{\tt SP}})={x\mathrel{{:}{=}}\ast;nom(\alpha,{\tt SP})}$: By IH $\exists\alpha^{\prime}~{}nom({{\tt SP}},{\alpha})={\alpha^{\prime}}$ then $nom({x:=\theta;\alpha},{\textbf{assign}~{}x\mathrel{{:}{=}}\ast~{}{\tt SP}})={x\mathrel{{:}{=}}\ast;\alpha^{\prime}}$ and $({\omega}_{x}^{r},\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{*})}$ and since (by inversion) $(\omega,{\omega}_{x}^{r})\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}x\mathrel{{:}{=}}\ast\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}}$ then also $(\omega,{\omega}_{x}^{r})\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}x\mathrel{{:}{=}}\ast\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}}$ and finally $(\omega,\nu)\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}x\mathrel{{:}{=}}\ast;\alpha^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}}$.

Case $nom({{{x^{\prime}=\theta}}\,\&\,H;\alpha},{\textbf{solve}~{}p_{ode}~{}t\colon{}{}p_{t}~{}\ dom\colon{}{}p_{dom}~{}{\tt SP}})={{{x^{\prime}=\theta}}\,\&\,H;nom(\alpha,{\tt SP})}$: By IH have $\exists\alpha^{\prime}~{}nom({{\tt SP}},{\alpha})={\alpha^{\prime}}$ then $nom({{{x^{\prime}=\theta}}\,\&\,Q;\alpha},{\textbf{solve}~{}p_{ode}~{}t\colon{}{}p_{t}~{}\ dom\colon{}{}p_{dom}~{}{\tt SP}})={{{x^{\prime}=\theta}}\,\&\,H;\alpha^{\prime}}$ and $({\omega}_{x}^{\varphi(t)},\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{*})}$ for some $t\geq 0$ such that $\forall~{}s\in[0,t]~{}\varphi(s)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and where $\varphi$ is the unique solution to $x^{\prime}=\theta$ on $[0,t]$. Since (by inversion) $(\omega,{\omega}_{x}^{\varphi(t)})\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta}}\,\&\,Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}}$ then also $(\omega,{\omega}_{x}^{\varphi(t)})\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta}}\,\&\,Q{\mathit{interp}(\eta^{\prime})}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}}$ and finally $(\omega,\nu)\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta}}\,\&\,Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}}$.

Case $nom({\alpha^{*};\beta},{\textbf{inv}~{}pre:{\tt SP}_{1}\{\textbf{Pre}~{}\Rightarrow~{}ind~{}|~{}\textbf{Ind}~{}\Rightarrow~{}{\tt SP}_{2}\}~{}{\tt SP}})={nom(\alpha^{*};\beta,{\tt SP})}$: By IH, have $\exists~{}\beta^{\prime}~{}nom({{\tt SP}},{\alpha^{*};\beta})={\alpha^{*};\beta^{\prime}},$ and $nom({\alpha^{*};\beta},{\textbf{finally}~{}{\tt SP}})={\alpha^{*};\beta^{\prime}}$ for the same $\beta^{\prime}$ and by IH, $(\omega,\nu)\in{\alpha^{*};\beta^{\prime}}{\mathit{interp}(\eta^{\prime})}$.

Case $nom({\alpha^{*};\beta},{\textbf{finally}~{}{\tt SP}})={\alpha^{*};nom(\beta,{\tt SP})}$: By inversion, $\exists\mu~{}(\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{*}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $(\mu,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\beta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By IH, $\exists~{}\beta^{\prime}~{}nom({{\tt SP}},{\beta})={\beta^{\prime}}$ and $(\mu,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\beta^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$. Then since $(\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{*}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then also $(\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{*}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$ and thus $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{*};\beta^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$ as desired.

Case $nom({{{x^{\prime}=\theta}}\,\&\,H;\alpha},{\textbf{Ghost}~{}y\mathrel{{:}{=}}\theta_{3};y^{\prime}=\theta_{2}~{}{\tt IP}})={{{y^{\prime}=\theta,\alpha}}\,\&\,Q;\beta^{\prime}}$: By inversion, $\exists\mu~{}(\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta}}\,\&\,Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $(\mu,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\beta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $\mu={\omega}_{x}^{\varphi_{x}(t)}$ for some $t\geq 0$ such that $\forall~{}s\in[0,t]~{}{\omega}_{x}^{\varphi_{x}(t)}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By applying the IH, we then have $\exists~{}\beta^{\prime}~{}nom({{\tt SP}},{{{x^{\prime}=\theta,y^{\prime}=\theta_{2}}}\,\&\,H;\beta})={{{x^{\prime}=\theta,y^{\prime}=\theta_{2}}}\,\&\,H;\beta^{\prime}},$ and $nom({{{x^{\prime}=\theta,y^{\prime}=\theta_{2}}}\,\&\,;\beta},{\textbf{Ghost}~{}y\mathrel{{:}{=}}\theta_{3};y^{\prime}=\theta_{2}~{}{\tt IP}})={{{x^{\prime}=\theta}}\,\&\,H;\beta^{\prime}}$ for the same $\beta^{\prime}$ and by IH, $({\omega}_{y}^{y_{0}},\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta,y^{\prime}=\theta_{2}}}\,\&\,;\beta^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$. By soundness for dG, $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta}}\,\&\,;\beta^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$.

Case $nom({{{x^{\prime}=\theta}}\,\&\,H;\alpha},{\textbf{inv}~{}pre:{\tt SP}_{1}\{\textbf{Pre}~{}\Rightarrow~{}ind~{}|~{}\textbf{Ind}~{}\Rightarrow~{}{\tt SP}_{2}\}~{}{\tt SP}})={nom({{x^{\prime}=\theta}}\,\&\,H;\alpha,{\tt SP})}$: By IH, $\exists~{}\beta^{\prime}~{}nom({{\tt SP}},{{{x^{\prime}=\theta}}\,\&\,H;\beta})={{{x^{\prime}=\theta}}\,\&\,H;\beta^{\prime}},$ and $nom({\alpha^{*};\beta},{\textbf{finally}~{}{\tt SP}})={{{x^{\prime}=\theta}}\,\&\,H;\beta^{\prime}}$ for the same $\beta^{\prime}$ and by IH, $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta}}\,\&\,H;\beta^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$.

Case $nom({{{x^{\prime}=\theta}}\,\&\,H;\alpha},{\textbf{finally}~{}{\tt SP}})={{{x^{\prime}=\theta}}\,\&\,H;nom(\alpha,{\tt SP})}$: By inversion, $\exists\mu~{}(\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta}}\,\&\,Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $(\mu,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\beta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By IH, $\exists~{}\beta^{\prime}~{}nom({{\tt SP}},{\beta})={\beta^{\prime}}$ and $(\mu,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\beta^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$. Then since $(\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta}}\,\&\,Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then also $(\omega,\mu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta}}\,\&\,Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\mathit{interp}(\eta^{\prime})}$ and thus $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta}}\,\&\,Q;\beta^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\eta^{\prime}}$ as desired.

Note that, as with the traces themselves, nondeterministic choices and loops discard nominals from their subprograms. As before, this does not weaken the theorem, it simply means those nominals are local in scope.

Theorem 7.10.

*Nominalization is sound when applied to proofs that check. That is, for all $\left({H}\leadsto{H_{\phi}}\right){\tt SP}:\left({\Gamma}\vdash{[\alpha]\phi}\right)$ and all d$\mathcal{L}_{h}$ interpretations $\mathit{interp}(\eta),$ we have $\Gamma\vdash_{\mathit{interp}(\eta)}[nom(\alpha,{\tt SP})]\phi$. *

The claim holds by observing that the transitions for $\alpha_{1}$ (which holds easily by induction) are a subset of those for $\alpha$, regardless of $\eta$, and the result holds from soundness for Kaisar: $[\alpha]\phi$ implies $[\beta]\phi$ for any $\beta$ where ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\beta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{}\subseteq{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{}$ by the semantics of the box modality.

Lastly we show standard soundness and completeness theorems:

7.2. Soundness and Completeness

Lemma 7.11 (Soundness of Pattern Matching).

If $\textbf{match}_{\Gamma_{1}}(p,e)=\Gamma_{2}$ then ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma_{1}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma_{2}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. That is, pattern-matching never affects the assumptions of a context, only the abbreviations, which are not soundness-critical.

By induction on $\textbf{match}_{\Gamma_{1}}(p,e)$. In every case, $\Gamma_{1}=\Gamma_{2}$ or $\Gamma_{1}$ adds a definition to $\Gamma_{2}$ or $\Gamma_{2}$ comes from an inductive call.

Lemma 7.12.

If $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then ${\nu}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\Gamma}^{\alpha}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$, where ${\nu}^{\alpha}$ ghosts all $x\in\mathop{\text{BV}}(\alpha)$ in $\omega$.

By renaming, ${\omega}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\Gamma}^{\alpha}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By program coincidence (Platzer, 2016), there exists $\tilde{\nu}$ where $({\omega}^{\alpha},\tilde{\nu})\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $\tilde{\nu}$ agrees with ${\omega}^{\alpha}$ on $\mathrm{Dom}(\omega)$. Then $\left(\mathrm{Dom}(\tilde{\omega})\setminus\mathrm{Dom}(\omega)\right)\cap\mathop{\text{BV}}(\alpha)=\emptyset$, so by bound effect lemma (Platzer, 2016) $\tilde{\nu}={\nu}^{\alpha}$. Since ${\omega}^{\alpha}$ and ${\nu}^{\alpha}$ agree on ghosts, by formula coincidence ${\omega}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\Gamma}^{\alpha}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$.

Lemma 7.13 (Soundness of Forward Proof).

If ${\tt FP}:(\Gamma;H\vdash\Delta)$ then $\Gamma\vdash\Delta$ is valid formula of dL.

Case $p$: If $\phi\in\Gamma$ then the conclusion holds by the hypothesis rule, otherwise $\phi\in\Sigma$ and since $\Sigma$ consists only of the axiom schemata of first-order arithmetic, which are sound, the result also holds.

Case ${\tt FP}_{1}\ {\tt FP}_{2}$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then by IH both $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\rightarrow\psi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ so by modus ponens $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\psi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ as desired.

Case ${\tt FP}_{1}\ \theta$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and then by IH $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\forall x~{}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and by forall instantiation/substitution $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\phi}_{x}^{\theta}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$.

Theorem 7.14 (Soundness of SP).

If $\left({H}\leadsto{H^{\prime\prime}}\right){\tt SP}:\left({\Gamma}\vdash{\Delta}\right)$ then $\Gamma\vdash\Delta$ is a valid formula of dL. Recall that while the LCF architecture ensures the implementation of Kaisar is sound, this soundness theorem is still essential to validate our calculus.

(Note: This proof has a lot of cases. Even for the extended version of the proof, we leave out the diamond rules, which are analogous to the box rules, and the implict rules, which follow directly from soundness of propositional logic and a handful of dL axioms). By induction on the derivation.

Case $\textbf{assume}~{}x:\phi~{}{\tt SP}$: By definition of $[?(\psi)]\phi$ suffices to show $\Gamma\vdash(\psi\rightarrow\phi),\Delta$ is valid, i.e. $\Gamma,\psi\vdash\phi,\Delta$. This holds directly by IH.

Case $\textbf{have}~{}x:\psi~{}{\tt SP}_{1}~{}{\tt SP}_{2}$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By IH1, $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\psi,\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. If $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then we’re done. Else $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\psi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ so $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma,\psi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Then IH2 is applicable and $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ as desired.

Case $\textbf{let}~{}p~{}=~{}\tilde{e}~{}{\tt SP}$: Note the context $\Gamma^{\prime}$ produced by pattern matching contains only definitions, so for all $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ also have $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma,\Gamma^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and the IH applies directly, giving $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ as desired.

Case $\textbf{let}~{}t(?x)~{}=~{}\tilde{e}~{}{\tt SP}$: Symmetric.

Case $\textbf{note}~{}x~{}=~{}{\tt FP}~{}{\tt SP}$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then by Lemma 7.13, $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\psi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and thus $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\psi\land\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and by IH, $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ as desired.

Case $\textbf{show}~{}x~{}\phi{{\tt UP}}$: First note all facts in the using clause hold. Those on the LHS of the union are in $\Gamma$ and thus hold by hypothesis rule. Those on the RHS are the results of forward proofs and thus hold by soundness of forward proof. Thus $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Proceed by cases on the proof method.

Case id: Holds by hypothesis rule.

Case $\mathbb{R}$: Holds by the side condition that $\Gamma\rightarrow\Delta$ is valid in first-order logic over the reals and the fact that dL conservatively extends FOL.

Case auto: We do not give a precise proof rule for this case since auto is ever-changing heuristic automation, we merely note that it is the result of operations in an LCF-style which itself has been verified, and thus soundness follows as a result.

Case $\left({H}\leadsto{H}\right)\left(\textbf{case}~{}p_{\phi}~{}\Rightarrow~{}{\tt SP}_{\phi}~{}|~{}p_{\alpha}~{}\Rightarrow~{}{\tt SP}_{\alpha}\right):\left({\Gamma}\vdash{[\alpha^{*}]\phi,\Delta}\right)$: By the IH, $\Gamma_{\phi}\vdash\phi,\Delta$ and $\Gamma_{\psi}\vdash[\alpha][\alpha^{*}]\phi,\Delta$ where $\textbf{match}(p_{\phi},\phi)=\Gamma_{\phi}$ $\textbf{match}(p_{\alpha},\alpha)=\Gamma_{\alpha}$. By Lemma LABEL:lem:pat-mon, $\Gamma$ and $\Gamma_{\psi}$ contain the same facts, as do $\Gamma$ and$\Gamma_{\alpha}$, so $\Gamma\vdash\phi,\Delta$ and $\Gamma\vdash[\alpha][\alpha^{*}]\phi$. Then by the semantics of loops (or soundness of the $[*]$ axiom of dL), $\Gamma\vdash[\alpha^{*}]\phi,\Delta$.

Case $\textbf{state}~{}t~{}{\tt SP}$: Directly by the IH on $\left({H,t}\leadsto{H_{\phi}}\right){\tt SP}:\left({\Gamma}\vdash{\phi,\Delta}\right)$.

Case $\textbf{focus}{}~{}p~{}{\tt SP}$ on the left: By the IH, $\Gamma_{1},\Gamma_{2}\vdash\neg\phi,\Delta$. The inverse of $\neg{R}$ is sound (derivable from cut and double negation elimination and $\neg{L}$), so $\Gamma_{1},\phi\Gamma_{2}\vdash\Delta$ as desired.

Case $\textbf{focus}{}~{}p~{}{\tt SP}$ on the right: By the IH, $\Gamma\vdash\phi,\Delta_{1},\Delta_{2}$ and $\Gamma\vdash\Delta_{1},\phi,\Delta_{2}$ follows by soundness of exchange.

Case $\left(\textbf{case}~{}p_{\alpha}~{}\Rightarrow~{}{\tt SP}_{\alpha}~{}|~{}p_{\beta}~{}\Rightarrow~{}{\tt SP}_{\beta}\right)$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Note $\Gamma_{1}$ and $\Gamma_{2}$ contain only pattern-matching definitions. So we can apply both IHs and get $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\alpha]\phi\lor\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\beta]\phi\lor\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. In the case that $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then we’re done, else $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\alpha]\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\beta]\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and by the semantics of $\cup$ then $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\alpha\cup\beta]\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ as desired.

Case $\textbf{assign}~{}x:=p_{\theta}~{}{\tt SP},x\notin\mathop{\text{BV}}(\phi)$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By IH have $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\phi}_{x}^{\theta},\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. If $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ we’re done, else by substitution ${\omega}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\omega}}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and by definition $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[x:=\theta]\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ as desired.

Case $\textbf{assign}~{}x:=p_{\theta}~{}{\tt SP},x\in\mathop{\text{BV}}(\phi)$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Define $\omega_{1}={\left(\omega,x_{i}=\omega(x)\right)}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\omega\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\theta}}$ for fresh $x_{i}$. Observe by construction and freshness of i.e. and soundness of renaming that $\omega_{1}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\Gamma}_{x_{i}}^{x}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $\omega_{1}(x)={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\theta}_{x}^{x_{i}}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega_{1}}$ so the IH applies, giving $\omega_{1}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi,{\Delta}_{x_{i}}^{x}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ which again by renaming and construction of $\omega_{1}$ gives either ${\omega}_{x}^{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{\omega}}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ or $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and in either case the result holds.

Case $\textbf{assign}~{}x\mathrel{{:}{=}}\ast~{}{\tt SP}$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Define $\omega_{1}={\left(\omega,x_{i}=\omega(x)\right)}_{x}^{r}$ for fresh $x_{i}$ and some $r\in\mathbb{R}.$ Observe by construction and freshness of i.e. and soundness of renaming that $\omega_{1}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\Gamma}_{x_{i}}^{x}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ so the IH applies, giving $\omega_{1}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi,{\Delta}_{x_{i}}^{x}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ which again by renaming and construction of $\omega_{1}$ gives either ${\omega}_{x}^{r}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ or $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and in either case the result holds (since this is true for all such $r$).

Case $\left({H}\leadsto{H_{\alpha}}\right)\textbf{after}{}~{}\{{\tt SP}_{1}\}~{}\textbf{have}{}~{}\psi~{}\textbf{then}{}~{}\{{\tt SP}_{2}\}:\left({\Gamma}\vdash{[\alpha]\phi,\Delta}\right)$: By IH, $\Gamma\vdash[\alpha]\bar{\psi},\Delta$ and ${\Gamma}^{\alpha},\bar{\psi}\vdash\phi,{\Delta}^{\alpha}$. Assume $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}\setminus{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ (else the sequent is trivially true). Then by IH1 $\nu\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\bar{\psi}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Also by Lemma 7.12 $\nu\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\Gamma}^{\alpha}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}}\setminus{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\arg{\Delta}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\alpha}$ and so by IH2 $\nu\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Since this holds for all such $\nu$ then $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\vdash[\alpha]\phi,\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ as desired.

Case $\textbf{solve}~{}p_{ode}~{}t\colon{}{}p_{t}~{}\ dom\colon{}{}p_{dom}~{}{\tt SP}$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$, then let $\nu={\omega}_{x}^{\varphi(t)}$ for any $t\geq 0$ where $\forall~{}s\in[0,t]~{}{\omega}_{x}^{\varphi(s)}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $\varphi$ is the solution for $x^{\prime}=\theta$. Then let $t$ be a fresh variable which agrees everywhere with the above time $t$. Note that $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}t\geq{0}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\forall~{}s\in[0,t]~{}Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ by choice of $t$. Then the IH applies and $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\phi}_{x}^{y(t)},\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. If $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ we’re done, else note by choice of $\nu$ we have $\nu\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ by substitution and this holds for all such $\nu$ and so $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[{{x^{\prime}=\theta}}\,\&\,Q]\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ as desired.

The cases for invariants are proven by simultaneous induction, where for the additional context of invariants $\delta\in\Delta$ we assume $[\alpha]\delta$ instead of $\delta$.

Case $\textbf{inv}~{}x:J\{\textbf{Pre}~{}\Rightarrow~{}{\tt SP}_{pre}~{}|~{}\textbf{Ind}~{}\Rightarrow~{}sproof_{inv}\}~{}{\tt IP}$, loop $\alpha^{*}$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By IH1, $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\psi,\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. If $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ we’re done, else $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\psi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. By Lemma 7.12 ${\omega}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\Gamma}^{\alpha}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $({\omega}^{\alpha},{\omega}^{\alpha})\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{*}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and ${\omega}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\Gamma}^{\alpha}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Thus by IH2 ${\omega}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\alpha]\phi,{\Delta}^{\alpha}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. If ${\omega}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\Delta}^{\alpha}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then by coincedence and renaming $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and we’re done. Else ${\omega}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\alpha]\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and this holds for all such ${\omega}^{\alpha}$ so ${\omega}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\alpha^{*}](\phi\rightarrow[\alpha]\phi)\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and by renaming so is $\omega$, and by the induction axiom $\omega\in{{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\alpha^{*}]\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}}$.

Case $\textbf{finally}~{}{\tt SP}$, loop $\alpha^{*}$: Let $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and let $\nu$ such that $(\omega,\nu)\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha^{*}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Then ${\omega}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\Gamma}^{\alpha}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and ${\nu}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{\Gamma}^{\alpha}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ by Lemma 7.12. By IH ${\nu}^{\alpha}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi,{\Delta}^{\alpha}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. In the latter case by renaming we’re done. Else since this holds for all possible $\nu$ we have $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\alpha^{*}]\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ as desired (by renaming again also).

Case $\textbf{inv}~{}x:J\{\textbf{Pre}~{}\Rightarrow~{}{\tt SP}_{pre}~{}|~{}\textbf{Ind}~{}\Rightarrow~{}{\tt SP}_{inv}\}~{}{\tt IP}$, ODE $\alpha={{x^{\prime}=\theta}}\,\&\,Q$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\land[\alpha]\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then by IH $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\psi,\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. If $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ we’re done else $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\psi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Then let $\nu={\omega}_{x}^{\varphi(t)}$ for any $t\geq 0$ where $\forall s~{}\in[0,t]{\omega}_{x}^{\varphi(s)}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $\varphi$ is the solution to $x^{\prime}=\theta$ for time $t$. By renaming and unpacking semantics in $\Delta$ then $\nu\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma_{1}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\Delta}$ and so by IH $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{(\phi)^{\prime}}_{x^{\prime}}^{\theta},\Delta_{1}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. In the case $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta_{1}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ then by renaming $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and we’re done, else by soundness of differential effects, $\nu\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}(\phi)^{\prime}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Since this holds for any such $\nu$, then by soundness of differential invariants, $\nu\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\psi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ for all such $\nu$ and so $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\alpha]\psi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ so we can apply the second IH from which the result follows.

Case $\textbf{finally}~{}{\tt SP}$, ODE ${{x^{\prime}=\theta}}\,\&\,Q$: Assume $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Then let $\nu={\omega}_{x}^{\varphi(t)}$ for any $t\geq 0$ where $\forall s~{}\in[0,t]{\omega}_{x}^{\varphi(s)}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and $\varphi$ is the solution to $x^{\prime}=\theta$ for time $t$. By renaming $\nu\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma_{1}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and by diff weakening $\nu\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and by unpacking semantics $\nu\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ so the IH applies giving $\nu\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$. Since this held for all $\nu$ then by renaming again $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[\alpha]\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ as desired.

Case $\textbf{Ghost}~{}y\mathrel{{:}{=}}\theta_{3};y^{\prime}=\theta_{2}~{}{\tt IP}$: Let $\omega_{1}=\omega,y={{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta_{3}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}{\omega}$. Then by coincidence (Platzer, 2015) $\omega_{1}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\Gamma,\Delta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and by construction $\omega_{I}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}y=\theta_{3}\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ So by IH, $\omega_{1}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}{{x^{\prime}=\theta_{1},y^{\prime}=\theta_{2}}}\,\&\,Q\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ By linearity of $\theta_{2}$ the existence interval of ${{x^{\prime}=\theta_{1},y^{\prime}=\theta_{2}}}\,\&\,Q$ agrees with ${{x^{\prime}=\theta_{1}}}\,\&\,Q$ so they have transitions for all the same times $t$. And since $y$ was fresh they agree on all variables but $y$ and by coincidence (Platzer, 2015) $\nu\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ whenever $\nu_{1}\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ and so by renaming $\omega\in{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}[{{x^{\prime}=\theta_{1}}}\,\&\,Q]\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}{}$ as desired.

Theorem 7.15 (Completeness).

Kaisar is complete with respect to sequent calculus for dL, that is for all $\Gamma,\Delta$ if $\Gamma\vdash\Delta$ is provable in dL sequent calculus then $\left({H}\leadsto{H_{\tt SP}}\right){\tt SP}:\left({\Gamma}\vdash{\Delta}\right)$ for some $H,H_{\tt SP},{\tt SP}$.

(Note: This proof has a lot of cases. Even for the extended version of the proof, we present only the cases for right rules for boxes and left rules for diamonds — the other cases are analogous). The proof proceeds by induction on sequent calculus proofs of dL, but we first establish several preliminary observations resolving the key differences between sequent calculus and Kaisar.

Observation 1: Rules such as $\forall$ instantiation require specifying an input. Inputs in Kaisar are extended terms, thus completeness requires all terms are expressible as extended terms (i.e. expansion is surjective). This is true when all states are named, in which case we call the trace complete, a property we maintain as an invariant.

By induction on the term $\theta$ we wish to express. All cases except variables hold by IH. In the (ghost or program) variable case, produce a nominal for the state at which the name was introduced.

Observation 2: All Kaisar proofs produced in this proof support weakening, so if $\left({H}\leadsto{H_{\tt SP}}\right){\tt SP}:\left({\Gamma_{1}}\vdash{\Delta_{1}}\right)$ then $\left({H}\leadsto{H_{\tt SP}}\right){\tt SP}:\left({\Gamma_{1},\Gamma_{2}}\vdash{\Delta_{1},\Delta_{2}}\right)$ for any contexts $\Gamma_{2},\Delta_{2}$ that introduce only fresh variables, i.e. contexts where $\mathrm{Dom}(\Gamma_{1})\cap\mathrm{Dom}(\Gamma_{2})=\mathrm{Dom}(\Delta_{1})\cap\mathrm{Dom}(\Delta_{2})=\emptyset$.

By inspection on the cases of the completeness proof. Weakening could only fail if adding assumptions caused a pattern-match to be ambiguous, but we fully disambiguate all patterns.

Observation 3: Kaisar is complete even ignoring forward proof, abbreviations and using clauses. While these features are essential in practical usage, they will not be needed in this proof.

An essential part of the proof is our choice of induction metric, because we often induct on formulas that are not strict subformulas of the input. We define a total ordering on sequents $(\Gamma_{1}\vdash\Delta_{1})\prec(\Gamma_{2}\vdash\Delta_{2})$ as the lexicographic ordering of:

1. (1)

The number of formulas containing modalities in the antecedent. 2. (2)

The number of nondeterministic choices $\alpha\cup\beta$. 3. (3)

The number of loops $\alpha^{*}$ 4. (4)

The number of compositions $\alpha;\beta$ 5. (5)

The total number of modalities ${[{\alpha}]}\phi$ or ${\langle{\alpha}\rangle}phi$. 6. (6)

The number of symbols occuring under some negation (i.e. sum of the number of symbols in $\phi$ for each $\neg(\phi)$) 7. (7)

The total number of formula connectives, (which does not include the comma separator, nor term connectives.)

Rule (1) ensures the focus rule can be used to implement antecedent structured execution. Rules (2-4) support the cases for the compound programs and (5) supports the atomic programs. Rule (6) supports the negation-normal form implicit rules, e.g. this definition ensures $(\Gamma\vdash\neg{P}\lor\neg{P},\Delta)\prec(\Gamma\vdash\neg(P\land{Q}),\Delta)$ Rule (7) supports the propositional and quantifier cases.

The main proof now proceeds by induction on sequent calculus proofs of dL under $\prec$.

In each case, let $\phi$ refer to the formula acted upon by the SC rule. The structured execution rules assume a formula in the first succedent position, thus (at the beginning of each case) we immediately pull $\phi$ to first succedent position with focus. Well-ordering is preserved here: For right rules, the metric $\prec$ is unchanged when acting on the succedent. For left rules, it strictly decreases by Rule (1).

Case cut: Can be assumed not to happen by admissibility of discrete cut elimination, but even without that, reduces to have.

Case $\phi\in FOL_{\mathbb{R}}$: By decidability of $FOL_{\mathbb{R}}$, $\left({H}\leadsto{H}\right)\textbf{show}~{}x~{}\_{\tt auto}:\left({\Gamma}\vdash{\phi,\Delta}\right)$.

Case $\phi\in\Gamma$: By hypothesis rule, $\left({H}\leadsto{H}\right)\textbf{show}~{}x~{}\_{\tt id}:\left({\Gamma,\phi}\vdash{\phi,\Delta}\right)$.

Case $\phi=\phi_{1}\land\phi_{2}$: By invertibility of the $\land{R}$ sequent calculus rule, $\Gamma\vdash{\phi_{1}},\Delta$ and $\Gamma\vdash{\phi_{2}},\Delta$ are derivable. By IH, $\exists{\tt SP}_{1},{\tt SP}_{2}$ where $\left({H}\leadsto{H}\right){\tt SP}_{1}:\left({\Gamma}\vdash{\phi_{1}}\right)$ and $\left({H}\leadsto{H}\right){\tt SP}_{2}:\left({\Gamma}\vdash{\phi_{2}}\right)$, from which we apply the case rule for conjunctions on the right: $\left({H}\leadsto{H}\right)\left(\textbf{case}~{}\phi_{1}~{}\Rightarrow~{}{\tt SP}1~{}|~{}\phi_{2}~{}\Rightarrow~{}{\tt SP}_{2}\right):\left({\Gamma}\vdash{\phi_{1}\land\phi_{2},\Delta}\right)$.

Case $\phi=\phi_{1}\lor\phi_{2}$: Let $\Delta_{1}=\phi_{1},\phi_{2},\Delta$. Notice $\Delta_{1}\prec{\phi_{1}\lor\phi_{2},\Delta}$ so apply the IH yielding $\left({H}\leadsto{H^{\prime}}\right){\tt SP}:\left({\Gamma}\vdash{\phi_{1},\phi_{2},\Delta}\right)$ then apply the case rule for disjunction on the right and we get: $\left({H}\leadsto{H^{\prime}}\right)\left(\textbf{case}~{}\phi_{1}~{}\Rightarrow~{}\phi_{2}~{}|~{}{\tt SP}~{}\Rightarrow~{}:\right)\left({\Gamma}\vdash{\phi_{1}\lor\phi_{2},\Delta}\right)$.

Case $\phi=\neg\phi_{1}$: By rule (6) we apply whichever negation-normal form (NNF) implicit rule applies based on the shape of $\phi$. Because SC is sufficient to implement NNF normalization, if $\Gamma\vdash\phi,\Delta$ is true in SC then $\Gamma\vdash{\tt nnf}(\phi),\Delta$ is as well, and is simpler, so true in Kaisar as well, then by the implicit normalization rules of Kaisar, $\Gamma\vdash{\phi},\Delta$ is as well.

Case $\phi=\phi_{1}\rightarrow\phi_{2}$: By IH (applicable because we removed propositional connectives), $\exists{\tt SP}~{}\left({H}\leadsto{H^{\prime}}\right){\tt SP}:\left({\Gamma,\phi_{1}}\vdash{\phi_{2},\Delta}\right)$, Then $\left({H}\leadsto{H^{\prime}}\right)\textbf{assume}~{}x:\phi_{1}~{}{\tt SP}:\left({\Gamma}\vdash{\phi_{1}\rightarrow\phi_{2},\Delta}\right)$

Case $\phi=\phi_{1}\leftrightarrow\phi_{2}$: By IH (applicable because we removed propositional connectives), both $\left({H}\leadsto{H_{1}}\right){\tt SP}_{1}:\left({\Gamma,\phi_{1}}\vdash{\phi_{2},\Delta}\right)$ and $\left({H}\leadsto{H_{2}}\right){\tt SP}_{2}:\left({\Gamma,\phi_{2}}\vdash{\phi_{1},\Delta}\right)$ and then we apply the casing form for equivalences: $\left({H}\leadsto{H}\right)\left(\textbf{case}~{}\phi_{1}\rightarrow\phi_{2}~{}\Rightarrow~{}\textbf{assume}~{}x_{1}:\phi_{1}~{}{\tt SP}_{1}~{}|~{}\phi_{2}\rightarrow\phi_{1}~{}\Rightarrow~{}\textbf{assume}~{}x_{2}:\phi_{2}~{}{\tt SP}_{2}\right):\left({\Gamma}\vdash{\phi_{1}\leftrightarrow\phi_{2},\Delta}\right)$.

Case $\phi=\forall~{}x~{}\phi_{1}$: Symmetric with the case for $[x\mathrel{{:}{=}}\ast]\phi_{1}$, except the reason for well-foundedness is that we removed a quantifier and added only term connectives.

Case $\phi=\exists~{}x~{}\phi_{1}$: Symmetric with the case for $\langle{x\mathrel{{:}{=}}\ast}\rangle{\phi_{1}}$.

Case $\phi=[x:=\theta]\phi_{1}$ where $x\notin\mathop{\text{BV}}(\phi_{1})$ : By IH (because we remove a modality), we then have $\exists{\tt SP}~{}\left({H,{\tt sub}(x,\theta)}\leadsto{H^{\prime}}\right){\tt SP}:\left({\Gamma}\vdash{{\phi_{1}}_{x}^{\theta},\Delta}\right)$. Then $\left({H}\leadsto{H^{\prime}}\right)\textbf{state}~{}t~{}\textbf{assign}~{}x:=\theta~{}{\tt SP}:\left({\Gamma}\vdash{[x:=\theta]\phi_{1},\Delta}\right)$ and $H,t,{\tt sub}(x,\theta)$ is a complete history and the inner proof still holds by weakening (i.e. addition of state namesm).

Case $\phi=[x:=\theta]\phi_{1}$ where $x\notin\mathop{\text{FV}}(\Gamma,\Delta,\theta)$: By IH (because we remove a modality), we then have $\exists{\tt SP}~{}\left({H,{\tt eq}(x,x_{i},\theta)}\leadsto{H^{\prime}}\right){\tt SP}:\left({\Gamma}\vdash{\phi_{1},\Delta}\right)$. Then $\left({H}\leadsto{H^{\prime}}\right)\textbf{state}~{}t~{}\textbf{assign}~{}x:=\theta~{}{\tt SP}:\left({\Gamma}\vdash{[x:=\theta]\phi_{1},\Delta}\right)$ and $H,t,{\tt eq}(x,\theta,$) is a complete history and the inner proof still holds by weakening (i.e. addition of state names).

Case $\phi=[x\mathrel{{:}{=}}\ast]\phi_{1}$ where $x\notin\mathop{\text{FV}}(\Gamma,\Delta,)$: By IH (because we remove a modality), we then have $\exists{\tt SP}~{}\left({H,{\tt any}(x,x_{i})}\leadsto{H^{\prime}}\right){\tt SP}:\left({\Gamma}\vdash{\phi_{1},\Delta}\right)$. Then $\left({H}\leadsto{H^{\prime}}\right)\textbf{state}~{}t~{}\textbf{assign}~{}x\mathrel{{:}{=}}\ast~{}{\tt SP}:\left({\Gamma}\vdash{[x\mathrel{{:}{=}}\ast]\phi_{1},\Delta}\right)$ and $H,t,{\tt any}(x,x_{i})$ is a complete history and the inner proof still holds by weakening (i.e. addition of state names).

Case $\phi=[\alpha;\beta]\phi_{1}$: By IH (because we remove a sequential composition), $\exists{\tt SP}~{}\left({H}\leadsto{H^{\prime}}\right){\tt SP}:\left({\Gamma}\vdash{[\alpha][\beta]\phi_{1},\Delta}\right)$ then by the implicit rule for $[;]$ have $\left({H}\leadsto{H^{\prime}}\right){\tt SP}:\left({\Gamma}\vdash{[\alpha;\beta]\phi_{1}}\right)$.

Case $\phi=[\alpha\cup\beta]\phi_{1}$: By IH (because we remove a $\cup$ operator), $\exists{\tt SP}_{1}~{}\left({H}\leadsto{H^{\prime}}\right){\tt SP}_{1}:\left({\Gamma}\vdash{[\alpha]\phi_{1},\Delta}\right)$ and $\exists{\tt SP}_{2}~{}\left({H}\leadsto{H^{\prime}}\right){\tt SP}_{2}:\left({\Gamma}\vdash{[\beta]\phi_{1},\Delta}\right)$. By $[\cup]$ casing have $\left({H}\leadsto{H}\right)\left(\textbf{case}~{}\alpha~{}\Rightarrow~{}{\tt SP}_{1}~{}|~{}\beta~{}\Rightarrow~{}{\tt SP}_{2}\right):\left({\Gamma}\vdash{[\alpha\cup\beta]\phi_{1},\Delta}\right)$.

Case $\Gamma,{\langle{\alpha\cup\beta}\rangle{\phi}}\vdash\Delta\lx@proof@logical@and\mathcal{D}_{1}=\Gamma,{\langle{\alpha}\rangle{\phi}}\vdash\Delta\mathcal{D}_{2}=\Gamma,{\langle{\beta}\rangle{\phi}}\vdash\Delta$: Observe in SC $\Gamma\vdash{[\alpha\cup\beta]\neg\phi},\Delta$ by the following derivation:

[TABLE]

And then since this sequent is simpler (less modalities on the left), it’s derivable by some ${\tt SP}$ in Kaisar by IH, so we derive $\left({H}\leadsto{H}\right)\textbf{focus}{}~{}\langle{\alpha\cup\beta}\rangle{\phi}~{}{\tt SP}:\left({\Gamma}\vdash{\langle{\alpha\cup\beta}\rangle{\phi},\Delta}\right)$.

Case $\Gamma,{\langle{\alpha;\beta}\rangle{\phi}}\vdash\Delta\mathcal{D}_{1}=\Gamma,{\langle{\alpha}\rangle{\langle{\beta}\rangle{\phi}}}\vdash\Delta$: Observe in SC $\Gamma\vdash{[\alpha][\beta]\neg\phi},\Delta$ by the following derivation:

[TABLE]

And then since this sequent is simpler (less modalities on the left), it’s derivable by some ${\tt SP}$ in Kaisar by IH, so we derive $\left({H}\leadsto{H}\right)\textbf{focus}{}~{}\langle{\alpha;\beta}\rangle{\phi}~{}{\tt SP}:\left({\Gamma}\vdash{\langle{\alpha;\beta}\rangle{\phi},\Delta}\right)$.

Case $\Gamma,{\langle{x:=\theta}\rangle{\phi}}\vdash\Delta\mathcal{D}_{1}=\Gamma,{{\phi}_{x}^{\theta}}\vdash\Delta(\text{if}x\notin\mathop{\text{BV}}(\phi))$: Observe $\Gamma\vdash{[x:=\theta]\neg\phi},\Delta$ in SC by (noting $\neg\left({\phi}_{x}^{\theta}\right)={(\neg\phi)}_{x}^{\theta}$)

[TABLE]

And then since this sequent is simpler (less modalities on the left), it’s derivable by some ${\tt SP}$ in Kaisar by IH, so we derive $\left({H}\leadsto{H}\right)\textbf{focus}{}~{}\langle{x:=\theta}\rangle{\phi}~{}{\tt SP}:\left({\Gamma}\vdash{\langle{x:=\theta}\rangle{\phi},\Delta}\right)$.

Case $\Gamma,{\langle{x:=\theta}\rangle{\phi}}\vdash\Delta\mathcal{D}_{1}=\Gamma,{{\phi}_{x}^{\theta}}\vdash\Delta(\text{if}x\notin\mathop{\text{FV}}(\Gamma,\Delta))$: Observe $\Gamma\vdash{[x:=\theta]\neg\phi},\Delta$ in SC by (noting $\neg\left({\phi}_{x}^{\theta}\right)={(\neg\phi)}_{x}^{\theta}$)

[TABLE]

And then since this sequent is simpler (less modalities on the left), it’s derivable by some ${\tt SP}$ in Kaisar by IH, so we derive $\left({H}\leadsto{H}\right)\textbf{focus}{}~{}\langle{x:=\theta}\rangle{\phi}~{}{\tt SP}:\left({\Gamma}\vdash{\langle{x:=\theta}\rangle{\phi},\Delta}\right)$.

Case $\Gamma,{\langle{x\mathrel{{:}{=}}\ast}\rangle{\phi}}\vdash\Delta\mathcal{D}_{1}=\Gamma,{\exists~{}x~{}\phi}\vdash\Delta$: Observe $\Gamma\vdash{[x\mathrel{{:}{=}}\ast]\neg\phi},\Delta$ in SC by

[TABLE]

And then since this sequent is simpler (less modalities on the left), it’s derivable by some ${\tt SP}$ in Kaisar by IH, so we derive $\left({H}\leadsto{H}\right)\textbf{focus}{}~{}\langle{x\mathrel{{:}{=}}\ast}\rangle{\phi}~{}{\tt SP}:\left({\Gamma}\vdash{\langle{x\mathrel{{:}{=}}\ast}\rangle{\phi},\Delta}\right)$.

Case $\Gamma,{\langle{?(\psi)}\rangle{\phi}}\vdash\Delta\mathcal{D}_{1}=\Gamma,{\psi\land\phi}\vdash\Delta$: Observe $\Gamma\vdash{[?(\psi)]\neg\phi},\Delta$ in SC by

[TABLE]

And then since this sequent is simpler (less modalities on the left), it’s derivable by some ${\tt SP}$ in Kaisar by IH, so we derive $\left({H}\leadsto{H}\right)\textbf{focus}{}~{}\langle{?(\psi)}\rangle{\phi}~{}{\tt SP}:\left({\Gamma}\vdash{\langle{?(\psi)}\rangle{\phi},\Delta}\right)$.

Case $\Gamma,{\langle{\alpha^{*}}\rangle{\phi}}\vdash\Delta\Gamma,{\phi\lor\langle{\alpha}\rangle{\langle{\alpha^{*}}\rangle{\phi}}}\vdash\Delta$: Observe $\Gamma\vdash{[\alpha^{*}]\neg\phi},\Delta$ in SC by

[TABLE]

And then since this sequent is simpler (less modalities on the left), it’s derivable by some ${\tt SP}$ in Kaisar by IH, so we derive $\left({H}\leadsto{H}\right)\textbf{focus}{}~{}\langle{\alpha^{*}}\rangle{\phi}~{}{\tt SP}:\left({\Gamma}\vdash{\langle{\alpha^{*}}\rangle{\phi},\Delta}\right)$.

Case $\Gamma,{\langle{{{x^{\prime}=\theta}}\,\&\,Q}\rangle{\phi(x)}}\vdash\Delta\Gamma,t\geq 0,\forall~{}s~{}\in[0,t]~{}{Q}_{x}^{y(t)},\phi(y(t))\vdash\Delta$: Observe $\Gamma\vdash{[{{x^{\prime}=\theta}}\,\&\,Q]\neg\phi},\Delta$ in SC by

[TABLE]

And then since this sequent is simpler (less modalities on the left), it’s derivable by some ${\tt SP}$ in Kaisar by IH, so we derive $\left({H}\leadsto{H}\right)\textbf{focus}{}~{}\langle{{{x^{\prime}=\theta}}\,\&\,Q}\rangle{\phi(x)}~{}{\tt SP}:\left({\Gamma}\vdash{\langle{{{x^{\prime}=\theta}}\,\&\,Q}\rangle{\phi(x)},\Delta}\right)$.

Case (${[{\alpha^{*}}]}\phi$, rule I): We have by assumption

[TABLE]

And the proof follows trivially from Inv and finally.

Case ${[{M}]}$: In the case of a box monotonicity proof, note that the mid rule as presented in the paper is simply a special case of:

[TABLE]

We presented it in its special-case form due to its close analogy with Hoare logic for explanatory purposes, but structured symbolic execution works just as well with the general form, and with the general form ${[{M}]}$ falls out by propositional reasoning.

Case ${\langle{M}\rangle}$: Symmetric.

Case ${[*]}$ iter on the right: Direct from the IH and from the rule:

[TABLE]

Case ${\langle{\alpha^{*}}\rangle}\phi$ on the right: Rule

[TABLE]

translates to

[TABLE]

Case $\Gamma\vdash{[{{x^{\prime}=\theta}}\,\&\,Q]\phi},\Delta$: In the ODE case, we assume without loss of generality that the proof is not a proof by the solve axiom $[^{\prime}]$ since $[^{\prime}]$ is implementable with DG,DC, and DI (Platzer, 2015). Further note we can restrict our consideration to a simplied fragment of ODE proofs which is in turn complete for SC. We say an ODE proof is in linear-normal form if it consists of 0 or more DG’s, followed by zero or more DCs (where the proof of each cut is a single DI), ending in DW.

We notate linear-normal proofs as $(DGs,DCsDIs,DW)$ with empty lists denoted $\epsilon$ and concatenation $(\mathcal{D}_{1}{\rm::}\mathcal{D}_{2})$

Lemma 7.16.

Linear-normal ODE proofs in SC are complete for ODE proofs in SC.

We define normalization ${\mathcal{D}}\Mapsto{(DGs,DCsDIs,DW)}$, then show the proofs check:

[TABLE]

${{DC(\phi)\mathcal{D}_{1}}\mathcal{D}_{2}}\Mapsto{((DGs_{1}{\rm::}DGs_{2}),(DCs_{1}{\rm::}DCs_{2}{\rm::}DC(\phi))(DIs_{1}{\rm::}DIs_{2}{\rm::}DW_{1}),DW_{2})}\lx@proof@logical@and{\mathcal{D}{}_{1}}\Mapsto{(DGs_{1},DCs_{1}DIs_{1},DW_{1})}{\mathcal{D}{}_{2}}\Mapsto{(DCs_{2},DCs_{2}DIs_{2},DW_{2})}$

Proceed by induction on the derivation. Case DW:: The proof is already linear-normal.

Case DI:: We cut in $\phi$, the formula proved by $DI(\phi),$ thus the cut holds. The cut holds because $DI(\phi)$ is a proof of some Case DG:: Direct by the IH.

Case DC:: $DGs_{1}$ check trivially by IH. $DGs_{2}$ check by IH and because the ghosted system after $DGs_{1}$ with the input system on non-ghost variables. $DCs_{1}$ and $DIs_{1}$ check because all invariants of the input system are invariants of the ghosted system. $DCs_{2}$ and $DIs_{2}$ check for this reason and because the addition of further invariants $DCs_{1}$ does not reduce provability. $DC(\phi)$ and $DW_{1}$ prove because addition of $DCs_{1}$ and $DCs_{2}$ never reduces provability. $DW_{2}$ proves because $\phi$ is available in the domain constraint and the addition of $DCs_{1}$ does not reduce provability.

Lemma 7.17.

Kaisar is complete for linear-normal SC proofs.

We proceed by a simultaneous induction on invariant proofs in normal form:

Case $\Gamma\vdash{[{{x^{\prime}=\theta}}\,\&\,Q]\phi},\Delta Q\vdash\phi$: By the outer IH $Q\vdash\phi$ is provable by some ${\tt SP}$ because it eliminates a modality. The proof follows by applying the finally  rule:

[TABLE]

Case $\Gamma\vdash{[{{x^{\prime}=\theta}}\,\&\,Q]\phi},\Delta\lx@proof@logical@and\Gamma\vdash{[{{x^{\prime}=\theta}}\,\&\,Q]\psi},\Delta Q\vdash{{(\psi)^{\prime}}_{x^{\prime}}^{\theta}}\Gamma\vdash{[{{x^{\prime}=\theta}}\,\&\,Q\land\psi]\phi},\Delta$: By the inner IH, the “use” case is provable by some ${\tt IP}$. By the linear-normal assumption, the “show” case is a single DI, and thus follows from the Inv rule:

[TABLE]

Case $\Gamma\vdash{[{{x^{\prime}=\theta}}\,\&\,Q]\phi},\Delta\lx@proof@logical@and\phi\leftrightarrow{\exists y~{}\psi}\Gamma\vdash{[{{x^{\prime}=\theta,y^{\prime}=\theta_{2}}}\,\&\,Q]\psi},\Delta$: By inner IH, the use case is provable by some ${\tt IP},$ and the result follows by ghosting:

[TABLE]

By composing the above lemmas, Kaisar is complete for ODE proofs in sequent calculus.

Corollary 7.18.

By Gödel’s incompleteness theorem, any sound calculus for dL is incomplete in the absolute sense (Platzer, 2008) and thus so is Kaisar. However, sequent calculus for dL is relatively complete (Platzer, 2008) both with respect to any differentially expressive logic and with respect to discrete dynamics. Thus Kaisar is as well.

8. Related Work

Structured proof languages were first introduced in the theorem prover Mizar (Bancerek et al., 2015; Wenzel and Wiedijk, 2002), then expanded upon in systems such as Isar (Wenzel, 2006, 1999, 2007). Other structured proof languages/extensions include the DECLARE (Syme, 1997) proof system for HOL, TLAPS for ${\rm TLA}^{+}$ (Cousineau et al., 2012; Lamport, 1992), Coq’s declarative proof language (Corbineau, 2007) and SSReflect extension (Gonthier and Mahboubi, 2010), and several “Mizar modes” implementing structured languages in provers including Cambridge HOL (Harrison, 1996), Isabelle (Kaliszyk et al., 2016), and HOL Light (Wiedijk, 2001). Kaisar is heavily inspired by Isar specifically, though we do not use every feature of Isar. The assume, note, show, and have are taken directly from Isar, and Kaisar’s let construct is a straightforward generalization of Isar’s let construct with pattern-matching. The use of pattern-matching for formula selection has been investigated, e.g. by Traut  (Traut and Noschinski, 2014) and by Gonthier  (Gonthier and Tassi, 2012).

In contrast with all the above, Kaisar has an extensive metatheory to justify its defining features: nominal terms and structured symbolic execution. While Isar and Coq’s declarative language have formally defined semantics, we know of only one interactive proof language besides Kaisar with significant metatheoretic results: VeriML (Stampoulis and Shao, 2010, 2012). We share with VeriML the goal of solving practical interactive proof problems via principled proof languages with metatheoretic guarantees. We differ in that VeriML addresses extending logical frameworks with automation while we address verification of concrete systems in a domain-specific logic for CPS.

Nominal terms are unique to Kaisar among interactive proof languages, and give it a unique advantage in expressing the rich ghost state of hybrid systems proofs. Other structured languages such as Isar have been used extensively for program verification (for example:  (Nipkow, 2002; Klein et al., 2010; Lochbihler, 2007)). However, because the above languages target general logics, they lack the language-level awareness of state change required for nominals. We provide this language-level support through the novel technical features of structured symbolic execution and static traces. We then implement the resulting language, reusing the infrastructure of an existing prover KeYmaera X.

An alternate approach is to implement a language at the user-level, in the tactics language of an existing prover. This approach was taken, e.g. by the Iris Proof Mode (IPM) for Coq, (Krebbers et al., 2017) which implements reasoning for concurrent separation logic in Coq’s $\mathcal{L}_{\tt tac}$ language. We work in the implementation language of KeYmaera X because it is far more expressive than its tactics language. Language choice is incidental: the key is preserving the underlying prover’s soundness guarantees. As with Coq (Barras and Werner, 1997), KeYmaera X has an LCF-style core supported by mechanized soundness results for the underlying calculus (Bohrer et al., 2017), making the Kaisar implementation highly trustworthy. Kaisar and IPM share a goal of building generalizable interactive proof technology for program logics, but they target vastly different logics and address different aspects of proof: IPM uses Coq’s unstructured proof style and focuses (a) on embedding object logics in metalogics and (b) on the concerns of separation logic (e.g. managing of different context types, state ownership). In contrast, we augment structured proof with nominals to provide natural reasoning across states as needed in hybrid systems. We conjecture that our basic approach applies to many logics, including separation logics.

Two closely related language classes are tactics languages (which implement reuseable automation) and unstructured proof languages (which implement concrete proofs). Automation can often be written in the prover’s implementation language: OCaml in Coq, ML in Isabelle, or Scala in KeYmaera X. Domain-specific languages for tactics include untyped $\mathcal{L}_{\tt tac}$  (Delahaye, 2000), reflective Rtac  (Malecha and Bengtson, 2015), and dependently typed Mtac (Ziliani et al., 2013) in Coq, Eisbach (Matichuk et al., 2016) in Isabelle, and VeriML (Stampoulis and Shao, 2010, 2012). Examples of unstructured languages are the Coq (Team, 2017) script language and the Isabelle (Nipkow et al., 2002) apply-script language. KeYmaera X features a language named Bellerophon (Fulton et al., 2017) for unstructured proofs and tactics. The Bellerophon language consists of regular expression-style tactic combinators (sequential composition, repetition, etc.) and a standard tactics library featuring, e.g. sequent calculus rules and general-purpose automation. Bellerophon’s strength is in tactics that compose the significant automation provided in its library. Its weakness is in performing large-scale concrete proofs. It lacks both the nominals unique to Kaisar and the constructs shared by Isar and Kaisar. For example, assumptions in Bellerophon are unnamed and referred to by their index or by search, which can become unreadable or brittle at scale.

Our nominal terms relate to nominal differential dynamic logic (Platzer, 2007b) d$\mathcal{L}_{h}$. In d$\mathcal{L}_{h}$, nominal formulas enable stating and proving theorems about named states. Our goal differs: we apply named states to simplify proofs of theorems of plain dL. In our metatheory, d$\mathcal{L}_{h}$ formulas provide a clean specification for the nominal terms of Kaisar.

The main hybrid systems verification alternative to theorem proving is model-checking. Because the uncountable state spaces of hybrid systems do not admit equivalent finite-state abstractions (Henzinger, 1996), model-checking approaches (Frehse, 2005; Frehse et al., 2011; Dreossi, 2017; Henzinger et al., 1997; Gao et al., 2013a, b; Chen et al., 2013) must approximate continuous dynamics, whereas dL can reason about exact dynamics. All of the above have limitations including (1) finite time horizons, (2) compact (and thus bounded) starting regions, (3) discrete notions of time, (4) and/or restriction to linear ODEs. Restrictions (1) and (2) greatly reduce the scope of safety results, (3) reduces their accuracy and (4) reduces the class of systems considered. In contrast, ${\sf{dL}}$ supports unbounded continuous time with non-linear ODEs.

9. Conclusion

To simplify and systematize historical reference for verification of safety-critical CPS, we developed the Kaisar proof language for dL, which introduces nominal terms supported by structured symbolic execution. Our metatheory shows Kaisar is sound and as expressive as other calculi. It shows that nominal automation is correct and nominals are the proof-language analog of nominal dL. In doing so we provide a foundation for ad-hoc historical reference in other provers.

Through our parachute example, we showed that nominals are desirable in CPS practice and that Kaisar proofs can be concise. We provided empirical support by prototyping Kaisar in KeYmaera X, an implementation which supports the parachute example and other examples of this paper. For evaluation, we reproduced a series of 5 safety proofs for ground robots (Mitsch et al., 2013), combining differential invariant reasoning for nonsolvable dynamics with nontrivial arithmetic proofs, for models supporting avoidance of moving obstacles under position and actuator uncertainty.

Appendix A Sequent Calculus for dL

First-Order Rules

[TABLE]

[TABLE]

[TABLE]

Symmetric Program Rules

[TABLE]

[TABLE]

[TABLE]

[TABLE]

[TABLE]

Asymetric Program Rules

[TABLE]

[TABLE]

Appendix B Denotational Semantics

The denotational semantics of dL are given as interpretation functions ${{{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\theta\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}}\omega$ for terms, ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\phi\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}$ for formulas, and ${{{\mathopen{\mathrel{[}\joinrel\mathrel{[}}\alpha\mathclose{\mathrel{]}\joinrel\mathrel{]}}{}}}}$ for programs. Terms denote reals, formulas denote sets of states, and programs denote transition relations (i.e. sets of pairs of states).

Term Semantics

[TABLE]

The differential $(\theta)^{\prime}$ of a term $\theta$ is denoted by the total derivative, the sum of all partial derivatives.

Formula Semantics

[TABLE]

Program Semantics

[TABLE]

Appendix C Complete Proof Rules of Kaisar

Pattern-Matching

[TABLE]

[TABLE]

Forward-Chaining Proof

[TABLE]

[TABLE]

[TABLE]

Structural Rules

[TABLE]

[TABLE]

Backward-Chaining First-Order Proof

[TABLE]

[TABLE]

Backward-Chaining Structured Box Execution

[TABLE]

Backward-Chaining Structured Diamond Execution

[TABLE]

Invariant (and Variant) Execution

[TABLE]

[TABLE]

[TABLE]

Implicit Conversion Rules

The implicit conversions leave the proof and history untouched, so we write only their effect on the sequent.

[TABLE]

[TABLE]

[TABLE]