The other camp
Yesterday I joined a discussion with some of the program verification people at IIS, and found that we think about the same logical formulas in different or even opposite ways, which is quite interesting. When thinking about the validity of a formula, my first instinct is to do it in type theory, that is, construct a term of the corresponding type, aided by some classical equivalences if thinking about classical validity; in short, I think syntactically (as a typed term is equivalent to a derivation in natural deduction) and intuitionistically (by default). On the other hand, the verification people (at least when using an SMT solver) negate the formula and think whether there is a model, which is semantic, and they (almost?) exclusively use classical logic. Another contrast is that I assume higher-order logic and happily quantify over whatever I want to quantify, whereas they seem to want to get rid of as many quantifiers as possible (so that the formulas are simple enough to be handled by the solver). The rest of this post is an abstracted (and in fact distorted) version of the problem we discussed yesterday, and I’ll make a few more observations.
Suppose that we’re dealing with an array $a : \mathbf{n} \to \mathsf V$ represented as a function, where $\mathbf{n} \defeq \set{0, 1, \ldots, n-1}$ and $\mathsf V$ is some set of values. This array is used as a container of pairs of type $\mathbf{n} \times \mathsf V$, and we use a pointer $p : \mathbf{n}$ to indicate that $\set{(i, a\ i)}_{0 \leq i < p}$ are the pairs currently stored in the container. Define an invariant on $a$ and $p$ of the form
\begin{align*} \mathsf{Inv}\ a\ p\ \defeq \forall v : \mathsf V.\ (&\exists i : \mathbf n.\ i < p \wedge a\ i = v) \to \\ & \exists j : \mathbf n.\ j < p \wedge a\ j = v \wedge (\forall k : \mathbf n.\ j < k \wedge k < p \to a\ k \neq v) \wedge \mathsf P\ j \end{align*}
which says that if there is some $v : \mathsf V$ in the container, then we should be able to find the index $j$ of its last occurrence and establish some property $\mathsf P$ about $j$. Then for some state transition relation $(\leadsto)$, we want to show that the invariant is preserved:
\begin{equation} \forall (a, p) \leadsto (a', p').\ \mathsf{Inv}\ a\ p \to \mathsf{Inv}\ a'\ p' \label{eq:original-preservation} \end{equation}
However, if we try to prove the above by SMT solving, the solver won’t be too happy about $\mathsf{Inv}$, apparently because quantifier alternation — in this case there are two alternations in the sequence $\forall v\thinspace(i)\ \exists j\ \forall k$ — is very expensive to deal with. My colleague Yun-Sheng Chang came up with a way to eliminate the $\exists j$ quantification, which looks like a form of Skolemisation to me, and I decided to try to apply a more standard version of Skolemisation. The idea is that the computation of $j$ is really independent of the invariant, and can be formulated independently as a function $f : (\mathbf n \to \mathsf V) \to \mathbf n \to \mathsf V \to \mathbf n$ satisfying the spec
$$ \mathsf{Lookup}\ f \defeq \forall a : \mathbf n \to \mathsf V.\ \forall p : \mathbf n. \forall v : \mathsf V.\ \mathsf{LastIndex}\ a\ p\ v\ (f\ a\ p\ v) $$
where
\begin{align*} \mathsf{LastIndex}\ a\ p\ v\ j \defeq{}& \mathsf{OccursIn}\ a\ p\ v \to \\ & j < p \wedge a\ j = v \wedge (\forall k : \mathbf n.\ j < k \wedge k < p \to a\ k \neq v) \\ \mathsf{OccursIn}\ a\ p\ v \defeq{}& \exists i : \mathbf n.\ i < p \wedge a\ i = v \end{align*} If we remove the spec of $f$ from $\mathsf{Inv}$, we’ll be left with
$$ \mathsf{Inv}^*\ f\ a\ p \defeq \forall v : \mathsf V.\ \mathsf{OccursIn}\ a\ p\ v \to \mathsf P\ (f\ a\ p\ v) $$
and it should suffice to just prove that $\mathsf{Inv}^*$ is preserved by the transition relation assuming $f$ and its spec:
\begin{equation} \forall f.\ \mathsf{Lookup}\ f \to \forall (a, p) \leadsto (a', p').\ \mathsf{Inv}^*\ f\ a\ p \to \mathsf{Inv}^*\ f\ a'\ p' \label{eq:nicer-preservation} \end{equation}
In more detail, we transform $\mathsf{Inv}$ as follows
\begin{align*} & \mathsf{Inv}\ a\ p \\ {}\equiv{}& \reason{definition of $\mathsf{Inv}$} \\ & \forall v : \mathsf V.\ \mathsf{OccursIn}\ a\ p\ v \to \\ & \quad \exists j : \mathbf n.\ j < p \wedge a\ j = v \wedge (\forall k : \mathbf n.\ j < k \wedge k < p \to a\ k \neq v) \wedge \mathsf P\ j \\ {}\equiv{} & \reason{$A \to \exists x. B \equiv \exists x. A \to B$ when $x$ does not occur free in $A$ (classically)} \\ & \forall v : \mathsf V.\ \exists j : \mathbf n.\ \mathsf{OccursIn}\ a\ p\ v \to \\ & \quad j < p \wedge a\ j = v \wedge (\forall k : \mathbf n.\ j < k \wedge k < p \to a\ k \neq v) \wedge \mathsf P\ j \\ {}\equiv{}& \reason{Skolemisation} \\ & \exists f.\ \forall v : \mathsf V.\ \mathsf{OccursIn}\ a\ p\ v \to \\ & \quad f\ a\ p\ v < p \wedge a\ (f\ a\ p\ v) = v \wedge (\forall k : \mathbf n.\ f\ a\ p\ v < k \wedge k < p \to a\ k \neq v) \wedge \mathsf P\ (f\ a\ p\ v) \\ {}\equiv{}& \reason{$\forall$ and $(A \to)$ distributes over conjunction} \\ & \exists f.\ \bigl(\forall v : \mathsf V.\ \mathsf{OccursIn}\ a\ p\ v \to \\ & \phantom{\exists f.\ \bigl(} \quad f\ a\ p\ v < p \wedge a\ (f\ a\ p\ v) = v \wedge (\forall k : \mathbf n.\ f\ a\ p\ v < k \wedge k < p \to a\ k \neq v)\bigr) \wedge {} \\ & \phantom{\exists f.\ } \bigl(\forall v : \mathsf V.\ \mathsf{OccursIn}\ a\ p\ v \to \mathsf P\ (f\ a\ p\ v)\bigr) \\ {}\Leftarrow{}& \reason{$\forall$-elimination; definition of $\mathsf{Lookup}$} \\ & \exists f.\ \mathsf{Lookup}\ f \wedge \forall v : \mathsf V.\ \mathsf{OccursIn}\ a\ p\ v \to \mathsf P\ (f\ a\ p\ v) \\ {}\equiv{}& \reason{definition of $\mathsf{Inv}^*$} \\ & \exists f.\ \mathsf{Lookup}\ f \wedge \mathsf{Inv}^*\ f\ a\ p \end{align*}
and use the resulting stronger predicate as the new invariant. The preservation of this new invariant can then be transformed as follows (where we omit the opening $\forall (a, p) \leadsto (a', p')$):
\begin{align*} & (\exists f.\ \mathsf{Lookup}\ f \wedge \mathsf{Inv}^*\ f\ a\ p) \to (\exists f.\ \mathsf{Lookup}\ f \wedge \mathsf{Inv}^*\ f\ a'\ p') \\ {}\equiv{}& \reason{currying} \\ & \forall f.\ \mathsf{Lookup}\ f \to \mathsf{Inv}^*\ f\ a\ p \to (\exists f.\ \mathsf{Lookup}\ f \wedge \mathsf{Inv}^*\ f\ a'\ p') \end{align*}
Here the $\exists$-quantified $f$ does not need to be the same as the $\forall$-quantified one in general, but since we know that $f$ is really an independent function that’s used throughout, we don’t need to vary the choice of $f$, and we don’t need to re-establish $\mathsf{Lookup}\ f$ at every step:
\begin{align*} & \forall f.\ \mathsf{Lookup}\ f \to \mathsf{Inv}^*\ f\ a\ p \to (\exists f.\ \mathsf{Lookup}\ f \wedge \mathsf{Inv}^*\ f\ a'\ p') \\ {}\Leftarrow{}& \reason{$\exists$-introduction} \\ & \forall f.\ \mathsf{Lookup}\ f \to \mathsf{Inv}^*\ f\ a\ p \to \mathsf{Lookup}\ f \wedge \mathsf{Inv}^*\ f\ a'\ p' \\ {}\equiv{}& \reason{$A \to A \wedge B \equiv A \to B$} \\ & \forall f.\ \mathsf{Lookup}\ f \to \mathsf{Inv}^*\ f\ a\ p \to \mathsf{Inv}^*\ f\ a'\ p' \end{align*}
We can then move the opening $\forall (a, p) \leadsto (a', p')$ inwards and arrive at Formula \ref{eq:nicer-preservation}.
From my point of view, Formula \ref{eq:nicer-preservation} is nicer to prove than Formula \ref{eq:original-preservation} since we can just assume the existence of $f$ and its correctness, and what we need to establish now ($\mathsf{Inv}^*$) is simpler than before ($\mathsf{Inv}$). The verification people don’t buy this argument though. To prove the validity of Formula \ref{eq:nicer-preservation}, they negate it
$$ \exists f.\ \mathsf{Lookup}\ f \wedge \exists (a, p) \leadsto (a', p').\ \mathsf{Inv}^*\ f\ a\ p \wedge \exists v : \mathsf V.\ \mathsf{OccursIn}\ a'\ p'\ v \wedge \neg \mathsf P\ (f\ a'\ p'\ v) $$
and prove by SMT solving that the negated version does not have a model. Again by Skolemisation, the existential quantifiers can be removed without changing the satisfiability of the formula, so we would try to give the SMT solver the formula
\begin{equation} \mathsf{Lookup}\ f \wedge (a, p) \leadsto (a', p') \wedge \mathsf{Inv}^*\ f\ a\ p \wedge i < p' \wedge a'\ i = v \wedge \neg \mathsf P\ (f\ a'\ p'\ v) \label{eq:original-negation} \end{equation}
which contains no quantifier alternation. I’m somewhat dismayed by this change of view, because (at least conceptually) $f$ now needs to be found by the SMT solver and seems to become a burden rather than an asset as I originally thought.
Moreover, the SMT solver doesn’t like Formula \ref{eq:original-negation}: $f$ is a higher-order function (whose first argument is a function), and subsequently $\mathsf{Lookup}\ f$ contains a higher-order quantification as well; this ‘higher-orderness’ cannot be handled by the solver. But this problem can be remedied: cleverly, my colleague Yu-Fang Chen observed that we don’t really need to use the whole $f$ and $\mathsf{Lookup}\ f$ — in the invariant preservation part of Formula \ref{eq:nicer-preservation} we use only $f\ a\ p$ and $f\ a'\ p'$, that is, we need to look up the last index only in $(a, p)$ and $(a', p')$, so it should suffice to assume the existence of two functions $g, g' : \mathsf V \to \mathbf n$ satisfying $\mathsf{LookupIn}\ a\ p\ g$ and $\mathsf{LookupIn}\ a'\ p'\ g'$ where
$$ \mathsf{LookupIn}\ a\ p\ g \defeq \forall v : \mathsf V.\ \mathsf{LastIndex}\ a\ p\ v\ (g\ v) $$
which is a generalisation of $\mathsf{Lookup}$ since we can express $\mathsf{Lookup}$ in terms of $\mathsf{LookupIn}$: $\mathsf{Lookup}\ f \equiv \forall a : \mathbf n \to \mathsf V.\ \forall p : \mathbf n.\ \mathsf{LookupIn}\ a\ p\ (f\ a\ p)$.
More formally, defining
$$ \mathsf{Inv}^{**}\ a\ p\ g \defeq \forall v : \mathsf V.\ \mathsf{OccursIn}\ a\ p\ v \to \mathsf P\ (g\ v) $$
so that $\mathsf{Inv}^*\ f\ a\ p \equiv \mathsf{Inv}^{**}\ a\ p\ (f\ a\ p)$, we strengthen Formula \ref{eq:nicer-preservation} as follows:
\begin{align*} & \forall f.\ \mathsf{Lookup}\ f \to \forall (a, p) \leadsto (a', p').\ \mathsf{Inv}^{**}\ a\ p\ (f\ a\ p) \to \mathsf{Inv}^{**}\ a'\ p'\ (f\ a'\ p') \\ {}\equiv{}& \reason{swapping; definitions of $\mathsf{Lookup}$ and $\mathsf{LookupIn}$} \\ & \forall (a, p) \leadsto (a', p').\ \forall f. \\ & \quad (\forall a : \mathbf n \to \mathsf V.\ \forall p : \mathbf n. \mathsf{LookupIn}\ a\ p\ (f\ a\ p)) \to \\ & \quad \mathsf{Inv}^{**}\ a\ p\ (f\ a\ p) \to \mathsf{Inv}^{**}\ a'\ p'\ (f\ a'\ p') \\ {}\Leftarrow{}& \reason{weakening the antecedent by extracting two instances using $\forall$-elimination} \\ & \forall (a, p) \leadsto (a', p').\ \forall f. \\ & \quad \mathsf{LookupIn}\ a\ p\ (f\ a\ p) \wedge \mathsf{LookupIn}\ a'\ p'\ (f\ a'\ p') \to \mathsf{Inv}^{**}\ a\ p\ (f\ a\ p) \to \mathsf{Inv}^{**}\ a'\ p'\ (f\ a'\ p') \\ {}\Leftarrow{}& \reason{$\forall$-elimination (backwards)} \\ & \forall (a, p) \leadsto (a', p').\ \forall f.\ \forall g, g' : \mathsf V \to \mathbf n. \\ & \quad \mathsf{LookupIn}\ a\ p\ g \wedge \mathsf{LookupIn}\ a'\ p'\ g' \to \mathsf{Inv}^{**}\ a\ p\ g \to \mathsf{Inv}^{**}\ a'\ p'\ g' \\ {}\equiv{}& \reason{redundant $\forall f$} \\ & \forall (a, p) \leadsto (a', p').\ \forall g, g' : \mathsf V \to \mathbf n. \\ & \quad \mathsf{LookupIn}\ a\ p\ g \wedge \mathsf{LookupIn}\ a'\ p'\ g' \to \mathsf{Inv}^{**}\ a\ p\ g \to \mathsf{Inv}^{**}\ a'\ p'\ g' \end{align*}
Now the negated formula which we need to show doesn’t have a model is
\begin{equation} (a, p) \leadsto (a', p') \wedge \mathsf{LookupIn}\ a\ p\ g \wedge \mathsf{LookupIn}\ a'\ p'\ g' \wedge \mathsf{Inv}^{**}\ a\ p\ g \wedge i < p' \wedge a'\ i = v \wedge \neg \mathsf P\ (g'\ v) \label{eq:first-order-negation} \end{equation}
which is no longer higher-order. This is a step I didn’t anticipate, probably because $f$ and $\mathsf{Lookup}\ f$ are premises and it’s kind of counterintuitive/unnecessary to weaken them (throw away what you have). It remains to be seen whether this formula can be handled efficiently or even successfully by the solver though.
The last interesting contrast between the two camps’ thinking is how we think about a formula being ‘stronger’. To me, a formula is stronger when it can be used to prove more things, whereas to the verification people a formula is stronger when it has less models. So when we move from Formula \ref{eq:original-negation} to Formula \ref{eq:first-order-negation}, for example, they would see that Formula \ref{eq:first-order-negation} has more models than Formula \ref{eq:original-negation}. Then, if we can show by SMT solving that Formula \ref{eq:first-order-negation} has no model, then Formula \ref{eq:original-negation} must have no model either, which is what we want. Somehow I failed to figure out this argument during the discussion — it could be because I needed more time to overcome the disorientation brought by the change of view, or simply because I’d drained most of my brain power at that point.
Follow-up: 0007 (A ‘systematic’ reformulation)
