frap/frap_book.tex

\documentclass{amsbook}

\usepackage{hyperref,url,amsmath,amssymb,proof,stmaryrd,tikz-cd}

\newtheorem{theorem}{Theorem}[chapter]
\newtheorem{lemma}[theorem]{Lemma}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{xca}[theorem]{Exercise}

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\numberwithin{section}{chapter}
\numberwithin{equation}{chapter}

%    For a single index; for multiple indexes, see the manual
%    "Instructions for preparation of papers and monographs:
%    AMS-LaTeX" (instr-l.pdf in the AMS-LaTeX distribution).
\makeindex

\begin{document}

\frontmatter

\title{Formal Reasoning About Programs}

%    Remove any unused author tags.

%    author one information
\author{Adam Chlipala}
\address{MIT, Cambridge, MA, USA}
\email{adamc@csail.mit.edu}

\begin{abstract}
  \emph{Briefly}, this book is about an approach to bringing software engineering up to speed with more traditional engineering disciplines, providing a mathematical foundation for rigorous analysis of realistic computer systems. As civil engineers apply their mathematical canon to reach high certainty that bridges will not fall down, the software engineer should apply a different canon to argue that programs behave properly. As other engineering disciplines have their computer-aided-design tools, computer science has proof assistants, IDEs for logical arguments. We will learn how to apply these tools to certify that programs behave as expected.

  \emph{More specifically}: Introductions to two intertangled subjects: the Coq proof assistant, a tool for machine-checked mathematical theorem proving; and formal logical reasoning about the correctness of programs.
\end{abstract}

\maketitle

\newpage

For more information, see the book's home page:

\begin{center} \url{http://adam.chlipala.net/frap/} \end{center}

\thispagestyle{empty}
\mbox{}\vfill
\begin{center}

Copyright Adam Chlipala 2015-2016.


This work is licensed under a
Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
The license text is available at:

\end{center}

\begin{center} \url{https://creativecommons.org/licenses/by-nc-nd/4.0/} \end{center}

\newpage

\setcounter{page}{4}

\tableofcontents

\mainmatter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Why Prove the Correctness of Programs?}

The classic engineering disciplines all have their standard mathematical techniques that are applied to the design of any artifact, before it is deployed, to gain confidence about its safety, suitability for some purpose, and so on.
The engineers in a discipline more or less agree on what are ``the rules'' to be followed in vetting a design.
Those rules are specified with a high degree of rigor, so that it isn't a matter of opinion whether a design is safe.
Why doesn't software engineering have a corresponding agreed-upon standard, whereby programmers convince themselves that their systems are safe, secure, and correct?
The concepts and tools may not quite be ready yet for broad adoption, but they have been under deveopment for decades.
This book introduces one particular tool and a body of ideas for how to apply it to different tasks in program proof.

As this document is in a very early draft stage, no more will be said here, in favor of jumping right into the technical material.
Eventually, there will no doubt be some sort of historical overview here, as part of a general placing-in-context of the particular approach that will come next.
There will also be plenty of scholarly citations (here and throughout the book).
In this early version, you get to take the author's word for it that we are about to learn a promising approach!

However, one overarching element of our strategy is important enough to deserve to be called out here.
We will study a variety of different approaches for formalizing what a program should do and for proving that a program does what it should.
At every step, we will pay close attention to the \emph{common foundation} that underlies everything.
For one thing, we will be proving all of our theorems with the Coq proof assistant, a powerful framework for writing and machine-checking proofs.
Coq itself is based on a relatively small set of core features, much like a well-designed programming language, and in both we build up increasingly sophisticated abstractions as libraries.
Those features can be thought of as the core of all mathematical reasoning.

We will also apply a recipe specific to program proof.
When we encounter a new challenge, to prove a new kind of property about a new kind of program, we will generally be considering four broad elements that appear in nearly all techniques.

\begin{itemize}
  \item \index{encoding}\textbf{Encoding.}
    Every programming language has both \index{syntax}\emph{syntax}, which defines what programs look like, and \index{semantics}\emph{semantics}, which defines how programs behave when run.
    Even when these elements seem obvious intuitively, we often find that there are surprisingly subtle choices to be made in defining syntax and semantics at the highest level of rigor.
    Seemingly minor decisions can have big impacts on how smoothly our proofs go.

  \item \textbf{Invariants.}
    Nearly every theorem about a program is stated in terms of a \index{transition system}\emph{transition system}, with some set of states and a relation for stepping from one state to the next, moving forward in time.
    Nearly every program proof also works by finding an \index{invariant}\emph{invariant} of a transition system, or a property that always holds of every state reachable from some starting state.
    The concept of invariant is very close to being a direct reinterpretation of mathematical induction, that glue of every serious mathematical development, known and loved by all.

  \item \index{abstraction}\textbf{Abstraction.}
    Often a transition system is too complex to analyze directly.
    Instead, we \emph{abstract} it with another transition system that is somehow more tractable, proving that the new system preserves all relevant properties of the original.

  \item \index{modularity}\textbf{Modularity.}
    Similarly, when a transition system is too complex, we often break it into separate \emph{modules} and use some well-behaved composition operators to reassemble them into the whole.
    Often abstraction and modularity go together, as we decompose a system both \index{horizontal decomposition}\emph{horizontally} (i.e., with modularity), splitting it into more manageable parts, and \index{vertical decomposition}\emph{vertically} (i.e., with abstraction), simplifying parts in ways that preserve key properties.
    We can even alternate between strategies, breaking a system into parts, abstracting one as a simpler part, further decomposing that part into pieces, and so on.
\end{itemize}

\newcommand{\encoding}[0]{\marginpar{\fbox{\textbf{Encoding}}}}

In the course of the book, we will never quite define any of these meta-techniques in complete formality.
Instead, we'll meet many examples of each, called out by eye-catching margin notes.
Generalizing from the examples should help the reader start developing an intuition for when to use each element and for the common design patterns that apply.

The core subject matter of the book is often grouped under traditional disciplinary headers like \index{semantics}\emph{semantics}, \index{programming-languages theory}\emph{programming-languages theory}, \index{formal methods}\emph{formal methods}, and \index{verification}\emph{verification}.
Often these different traditions have their own competing terminology for shared concepts.
We'll follow one particular set of unified terminology and notation, cherry-picked from the conventions of different communities.
There really is a huge amount of commonality across everything that we'll study, so we don't want to distract by constantly translating between notations.
It is quite important to be literate in the standard notational conventions, which are almost always implemented with \index{\LaTeX{}}\LaTeX{}, and we stick entirely to that kind of notation in this book.
However, we follow another, much less usual convention: while we give theorem and lemma statements, we rarely give their proofs.
The reason is that the author and many other researchers today feel that proofs on paper have outlived their usefulness.
Instead, the proofs are all found in the parallel world of the accompanying Coq source code.

That is, each chapter of this book has a corresponding Coq source file, distributed with the general book source code.
The Coq sources are heavily commented and may even, in many cases, be feasible to read without also reading the book chapters.
More importantly, the Coq sources aren't just meant to be \emph{read}.
They are meant to be \emph{executed}.
We suggest stepping through them interactively, seeing intermediate states of proofs as appropriate.
The book proper can be read without the Coq sources, to learn the standard background material of program proof; and the Coq sources can be read without the book proper, to learn a particular concrete realization of those ideas.
However, they go better together.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Formalizing Program Syntax}

\section{Concrete Syntax}

The definition of a program starts with the definition of a programming language, and the definition of a programming language starts with its \emph{syntax}\index{syntax}, which covers which sorts of phrases are basically well-formed.
In the next chapter, we turn to \emph{semantics}\index{semantics}, which, in the course of saying what programs \emph{mean}, may impose further validity conditions.
Turning to examples, let's start with \emph{concrete syntax}\index{concrete syntax}, which decrees which sequences of characters are acceptable.
For a simple language of arithmetic expressions, we might accept the following strings as valid.
$$\begin{array}{l}
  3 \\
  x \\
  3 + x \\
  y * (3 + x)
\end{array}$$

Plenty of other strings might be invalid, like these.
$$\begin{array}{l}
  1 + + \; 2 \\
  x \; y \; z
\end{array}$$

Rather than appeal to our intuition about grade-school arithmetic, we prefer to formalize concrete syntax with a \emph{grammar}\index{grammar}, following a style known as \emph{Backus-Naur Form (BNF)}\index{Backus-Naur Form}\index{BNF}.
We have a set of \emph{nonterminals}\index{nonterminal} (e.g., $e$ below), standing for sets of allowable strings.
Some are defined by appeal to existing sets, as below, when we define constants $n$ in terms of the well-known set $\mathbb N$\index{N@$\mathbb N$} of natural numbers\index{natural numbers} (nonnegative integers).
\encoding
$$\begin{array}{rrcl}
  \textrm{Constants} & n &\in& \mathbb N \\
  \textrm{Variables} & x &\in& \mathsf{Strings} \\
  \textrm{Expressions} & e &::=& n \mid x \mid e + e \mid e \times e
\end{array}$$

To interpret the grammar in plain English: we assume sets of constants and variables, based on well-known sets of natural numbers and strings, respectively.
We then define expressions to include constants, variables, addition, and multiplication.
Crucially, the last two cases are specified \emph{recursively}: we show how to build bigger expressions out of smaller ones.

Incidentally, we're already seeing how many different formal notations creep into the discussion of formal program proofs.
All of this content is typeset in \LaTeX{}\index{\LaTeX{}}, and it may be helpful to consult the book sources, to see how it's all done.

Throughout the subject, one of our most crucial tools will be \emph{inductive definitions}\index{inductive definition}, explaining how to build up bigger sets from smaller ones.
The recursive nature of the grammar above is implicitly giving an inductive definition.
A more general notation for inductive definitions provides a series of \emph{inference rules}\index{inference rules} that define a set.
Formally, the set is defined to be \emph{the smallest one that satisfies all the rules}.
Each rule has \emph{premises}\index{premise} and a \emph{conclusion}\index{conclusion}.
We illustrate with four rules that together are equivalent to the BNF grammar above, for defining a set $\mathsf{Exp}$ of expressions.
\encoding
$$\infer{n \in \mathsf{Exp}}{
  n \in \mathbb N
}
\quad \infer{x \in \mathsf{Exp}}{
  x \in \mathsf{Strings}
}
\quad \infer{e_1 + e_2 \in \mathsf{Exp}}{
  e_1 \in \mathsf{Exp}
  & e_2 \in \mathsf{Exp}
}
\quad \infer{e_1 \times e_2 \in \mathsf{Exp}}{
  e_1 \in \mathsf{Exp}
  & e_2 \in \mathsf{Exp}
}$$

The general reading of an inference rule is: \textbf{if} all the facts above the horizontal line are true, \textbf{then} the fact below the line is true, too.
The rule implicitly needs to hold for \emph{all} values of the \emph{metavariables}\index{metavariable} (like $n$ and $e_1$) that appear within it; we can model them more explicitly with a sort of top-level universal quantification.
Newcomers to semantics often react negatively to seeing this style of definition, but very quickly it becomes apparent as a remarkably compact notation for expressing many concepts.
Think of it as a domain-specific programming language for mathematical definitions, an analogy that becomes quite concrete in the associated Coq code!

\section{Abstract Syntax}

After that brief interlude with concrete syntax, we now drop all formal treatment of it, for the rest of the book!
Instead, we concern ourselves with \emph{abstract syntax}\index{abstract syntax}, the real heart of language definitions.
Now programs are \emph{abstract syntax trees}\index{abstract syntax tree} (\emph{ASTs}\index{AST}), corresponding to inductive type definitions in Coq or algebraic datatype\index{algebraic datatype} definitions in Haskell\index{Haskell}.
Such types can be defined by enumerating their \emph{constructor}\index{constructor} functions with types.
\encoding
\begin{eqnarray*}
  \mathsf{Const} &:& \mathbb{N} \to \mathsf{Exp} \\
  \mathsf{Var} &:& \mathsf{Strings} \to \mathsf{Exp} \\
  \mathsf{Plus} &:& \mathsf{Exp} \times \mathsf{Exp} \to \mathsf{Exp} \\
  \mathsf{Times} &:& \mathsf{Exp} \times \mathsf{Exp} \to \mathsf{Exp}
\end{eqnarray*}

Such a list of constructors defines the set $\mathsf{Exp}$ to contain exactly those terms that can be built up with the constructors.
In inference-rule notation:
\encoding
$$\infer{\mathsf{Const}(n) \in \mathsf{Exp}}{
  n \in \mathbb N
}
\quad \infer{\mathsf{Var}(x) \in \mathsf{Exp}}{
  x \in \mathsf{Strings}
}
\quad \infer{\mathsf{Plus}(e_1, e_2) \in \mathsf{Exp}}{
  e_1 \in \mathsf{Exp}
  & e_2 \in \mathsf{Exp}
}
\quad \infer{\mathsf{Times}(e_1, e_2) \in \mathsf{Exp}}{
  e_1 \in \mathsf{Exp}
  & e_2 \in \mathsf{Exp}
}$$

Actually, semanticists get tired of writing such verbose descriptions, so proofs on paper tend to use exactly the sort of notation that we associated with concrete syntax.
The trick is mental desugaring of the concrete-syntax notation into abstract syntax!
We will generally not dwell on the particularities of that process.
Instead, we repeatedly illustrate it by example, using Coq code that starts with abstract syntax, accompanied by \LaTeX{}-based ``code'' in this book that applies concrete syntax freely.

Abstract syntax is handy for writing \emph{recursive definitions}\index{recursive definition} of functions.
Here is one in the clausal\index{clausal function definition} style of Haskell\index{Haskell}.
\begin{eqnarray*}
  \mathsf{size}(\mathsf{Const}(n)) &=& 1 \\
  \mathsf{size}(\mathsf{Var}(x)) &=& 1 \\
  \mathsf{size}(\mathsf{Plus}(e_1, e_2)) &=& 1 + \mathsf{size}(e_1) + \mathsf{size}(e_2) \\
  \mathsf{size}(\mathsf{Times}(e_1, e_2)) &=& 1 + \mathsf{size}(e_1) + \mathsf{size}(e_2)
\end{eqnarray*}

It is important that we include \emph{one clause per constructor of the inductive type}.
Otherwise, the function would not be \emph{total}\index{total function}.
We also need to be careful to ensure \emph{termination}\index{termination of recursive definitions}, by making recursive calls only on the arguments of the constructors.
This termination criterion, adopted by Coq, is called \emph{primitive recursion}\index{primitive recursion}.

\newcommand{\size}[1]{{\left \lvert #1 \right \rvert}}

It is also common to associate a recursive definition with a new notation.
For example, we might prefer to write $\size{e}$ for $\mathsf{size}(e)$, as follows.
\begin{eqnarray*}
  \size{\mathsf{Const}(n)} &=& 1 \\
  \size{\mathsf{Var}(x)} &=& 1 \\
  \size{\mathsf{Plus}(e_1, e_2)} &=& 1 + \size{e_1} + \size{e_2} \\
  \size{\mathsf{Times}(e_1, e_2)} &=& 1 + \size{e_1} + \size{e_2}
\end{eqnarray*}

\newcommand{\depth}[1]{{\left \lceil #1 \right \rceil}}

Let's continue to exercise our creative license and write $\depth{e}$ for the \emph{depth} of $e$, that is, the length of the longest downward path from the syntax-tree root to any leaf.
\begin{eqnarray*}
  \depth{\mathsf{Const}(n)} &=& 1 \\
  \depth{\mathsf{Var}(x)} &=& 1 \\
  \depth{\mathsf{Plus}(e_1, e_2)} &=& 1 + \max(\depth{e_1}, \depth{e_2}) \\
  \depth{\mathsf{Times}(e_1, e_2)} &=& 1 + \max(\depth{e_1}, \depth{e_2})
\end{eqnarray*}


\section{Structural Induction Principles}

The main reason to prefer abstract syntax is that, while strings of text \emph{seem} natural and simple to our human brains, they are really a lot of trouble to treat in complete formality.
Inductive trees are much nicer to manipulate.
Considering the name, it's probably not surprising that the main thing we want to do on them is \emph{induction}\index{induction}, an activity most familiar in the form of \emph{mathematical induction}\index{mathematical induction} over the natural numbers.
In this book, we will not dwell on many proofs about natural numbers, instead presenting the more general and powerful idea of \emph{structural induction}\index{structural induction} that subsumes mathematical induction in a formal sense, based on viewing the natural numbers as one simple inductively defined set.

There is a general recipe to go from an inductive definition to its associated induction principle.
When we define set $S$ inductively, we gain an induction principle for proving that some predicate $P$ holds for all elements of $S$.
To make this conclusion, we must discharge one proof obligation per rule of the inductive definition.
Recall our last rule-based definition above, for the abstract syntax of $\mathsf{Exp}$.
To derive an $\mathsf{Exp}$ structural induction principle, we produce a new set of rules, cloning each rule with two key modifications:
\begin{enumerate}
  \item Replace each conclusion, of the form $E \in S$, with a conclusion $P(E)$.  That is, the obligations involve \emph{showing} that $P$ holds of certain terms.
  \item For each premise $E \in S$, add a companion premise $P(E)$.  That is, the obligation allows \emph{assuming} that $P$ holds of certain terms.  Each such assumption is called an \emph{inductive hypothesis}\index{inductive hypothesis} (\emph{IH}\index{IH}).
\end{enumerate}

That mechanical procedure derives the following four proof obligations, associated with an inductive proof that $\forall x \in \mathsf{X}. \; P(x)$.
$$\infer{P(\mathsf{Const}(n))}{
  n \in \mathbb N
}
\quad \infer{P(\mathsf{Var}(x))}{
  x \in \mathsf{Strings}
}$$
$$\quad \infer{P(\mathsf{Plus}(e_1, e_2))}{
  e_1 \in \mathsf{Exp}
  & P(e_1)
  & e_2 \in \mathsf{Exp}
  & P(e_2)
}
\quad \infer{P(\mathsf{Times}(e_1, e_2))}{
  e_1 \in \mathsf{Exp}
  & P(e_1)
  & e_2 \in \mathsf{Exp}
  & P(e_2)
}$$

In other words, to establish $\forall x \in \mathsf{X}. \; P(x)$, we need to prove that each of these inference rules is valid.

To see induction in action, we prove a theorem giving a sanity check on our two recursive definitions from earlier: depth can never exceed size.
\begin{theorem}
  For all $e \in \mathsf{Exp}$, $\depth{e} \leq \size{e}$.
\end{theorem}
\begin{proof}
  By induction on the structure of $e$.
\end{proof}

That sort of minimalist proof often surprises and frustrates newcomers.
Our position here is that proof checking is an activity fit for machines, not people, so we will leave out gory details, which are to be found in the accompanying Coq code, for this theorem and many others associated with this chapter.
Actually, even published proofs on paper tend to use ``proofs'' as brief as the one above, relying on the reader's experience to ``fill in the blanks''!
Unsurprisingly, fairly often there are logical errors in such arguments, leading to acceptance of bogus theorems.
For that reason, we stick to machine-checked proofs here, using the book chapters to introduce concepts, reasoning principles, and statements of key theorems and lemmas.

\section{\label{decidable}Decidable Theories}

We do, however, need to get all the proof details filled in somehow.
One of the most convenient cases is when a proof goal fits into some \emph{decidable theory}\index{decidable theory}.
We follow the sense from computability theory\index{computability theory}, where we consider some \emph{decision problem}\index{decision problem}, as a (usually infinite) set $F$ of formulas and some subset $T \subseteq F$ of \emph{true} formulas, possibly considering only those provable using some limited set of inference rules.
The decision problem is \emph{decidable} if and only if there exists some always-terminating program that, when passed some $f \in F$ as input, returns ``true'' if and only if $f \in T$.
Decidability of theories is handy because, whenever our goal belongs to the $F$ set of a decidable theory, we can discharge the goal automatically by running the deciding program that must exist.

One common decidable theory is \emph{linear arithmetic}\index{linear arithmetic}, whose $F$ set is generated by the following grammar as $\phi$.
$$\begin{array}{rrcl}
  \textrm{Constants} & n &\in& \mathbb Z \\
  \textrm{Variables} & x &\in& \mathsf{Strings} \\
  \textrm{Terms} & e &::=& x \mid n \mid e + e \mid e - e \\
  \textrm{Propositions} & \phi &::=& e = e \mid e < e \mid \neg \phi \mid \phi \land \phi
\end{array}$$

The arithmetic terms used here are \emph{linear} in the same sense as \emph{linear algebra}\index{linear algebra}: we never multiply together two terms containing variables.
Actually, multiplication is prohibited outright, but we allow multiplication by a constant as an abbreviation (logically speaking) for repeated addition.
Propositions are formed out of equality and less-than tests on terms, and we also have the Boolean negation (``not'') operator $\neg$ and conjunction (``and'') operator $\land$.
This set of propositional\index{propositional logic} operators is enough to encode the other usual inequality and propositional operators, so we allow them, too, as convenient shorthands.

Using decidable theories in a proof assistant like Coq, it is important to understand how a theory may apply to formulas that don't actually satisfy its grammar literally.
For instance, we may want to prove $f(x) - f(x) = 0$, for some fancy function $f$ well outside the grammar above.
However, we only need to introduce a new variable $y$, defined with the equation $y = f(x)$, to arrive at a new goal $y - y = 0$.
A linear-arithmetic procedure makes short work of this goal, and we may then derive the original goal by substituting back in for $y$.
Coq's tactics based on decidable theories do all that hard work for us.

\medskip

Another important decidable theory is of \emph{equality with uninterpreted functions}\index{theory of equality with uninterpreted functions}.
$$\begin{array}{rrcl}
  \textrm{Variables} & x &\in& \mathsf{Strings} \\
  \textrm{Functions} & f &\in& \mathsf{Strings} \\
  \textrm{Terms} & e &::=& x \mid f(e, \ldots, e) \\
  \textrm{Propositions} & \phi &::=& e = e \mid \neg \phi \mid \phi \land \phi
\end{array}$$

In this theory, we know nothing about the detailed properties of the variables or functions that we use.
Instead, we must reason solely from the basic properties of equality:
$$\infer[\mathsf{Reflexivity}]{e = e}{}
\quad \infer[\mathsf{Symmetry}]{e_1 = e_2}{
  e_2 = e_1
}
\quad \infer[\mathsf{Transitivity}]{e_1 = e_2}{
  e_1 = e_3
  & e_3 = e_2
}$$
$$\infer[\mathsf{Congruence}]{f(e_1, \ldots, e_n) = f'(e'_1, \ldots, e'_n)}{
  f = f'
  & e_1 = e'_1
  & \ldots
  & e_n = e'_n
}$$

\medskip

As one more example of a decidable theory, consider the algebraic structure of \emph{semirings}\index{semirings}, which may profitably be remembered as ``types that act like natural numbers.''
A semiring is any set containing two elements notated 0 and 1, closed under two binary operators notated $+$ and $\times$.
The notations are suggestive, but in fact we have free reign in choosing the set, elements, and operators, so long as the following axioms\footnote{The equations are taken almost literally from \url{https://en.wikipedia.org/wiki/Semiring}.} are satisfied:
\begin{eqnarray*}
  (a + b) + c &=& a + (b + c) \\
  0 + a &=& a \\
  a + 0 &=& a \\
  a + b &=& b + a \\
  (a \times b) \times c &=& a \times (b \times c) \\
  1 \times a &=& a \\
  a \times 1 &=& a \\
  a \times (b + c) &=& (a \times b) + (a \times c) \\
  (a + b) \times c &=& (a \times c) + (b \times c) \\
  0 \times a &=& 0 \\
  a \times 0 &=& 0
\end{eqnarray*}

The formal theory is then as follows, where we consider as ``true'' only those equalities that follow from the axioms.
$$\begin{array}{rrcl}
  \textrm{Variables} & x &\in& \mathsf{Strings} \\
  \textrm{Terms} & e &::=& x \mid e + e \mid e \times e \\
  \textrm{Propositions} & \phi &::=& e = e
\end{array}$$

Note how the applicability of the semiring theory is incomparable to the applicability of the linear-arithmetic theory.
That is, while some goals are provable via either, some are provable only via the semiring theory and some provable only by linear arithmetic.
For instance, by the semiring theory, we can prove $x \times y = y \times x$, while linear arithmetic can prove $x - x = 0$.

\section{Simplification and Rewriting}

While we leave most proof details to the accompanying Coq code, it does seem important to introduce two key principles that are often implicit in proofs on paper.

The first is \emph{algebraic simplification}\index{algebraic simplification}, where we apply the defining equations of a recursive definition to simplify a goal.
For example, recall that our definition of expression size included this clause.
\begin{eqnarray*}
  \size{\mathsf{Plus}(e_1, e_2)} &=& 1 + \size{e_1} + \size{e_2}
\end{eqnarray*}
Now imagine that we are trying to prove this formula.
$$\size{\mathsf{Plus}(e, \mathsf{Const}(7))} = 2 + \size{e}$$
We may apply the defining equation to rewrite into a different formula, where we have essential pushed the definition of $\size{\cdot}$ through the $\mathsf{Plus}$.
$$1 + \size{e} + \size{\mathsf{Const}(7)} = 2 + \size{e}$$
Another application of a different defining equation, this time for $\mathsf{Const}$, takes us to here.
$$1 + \size{e} + 1 = 2 + \size{e}$$
From here, the goal follows by linear arithmetic.

\medskip

Such a proof establishes a theorem $\forall e \in \mathsf{Exp}. \; \size{\mathsf{Plus}(e, \mathsf{Const}(7))} = 2 + \size{e}$.
We may use already-proved theorems via a more general \emph{rewriting}\index{rewriting} mechanism, applying whenever we know some quantified equality.
Within a new goal we are proving, we find some subterm that matches the lefthand side of that equality, after we choose the proper values of the quantified variables.
The process of finding those values automatically is called \emph{unification}\index{unification}.
Rewriting enables us to take the subterm we found and replace it with the righthand side of the equation.

As an example, assume that, for some $P$, we know $P(2 + \size{\mathsf{Var}(x)})$ and are trying to prove $P(\size{\mathsf{Plus}(\mathsf{Var}(x), \mathsf{Const}(7))})$.
We may use our earlier fact to rewrite the argument of $P$ in what we are trying to show, so that it now matches the argument from what we already know, at which point the proof is trivial to finish.
Here, unification found the assignment $e = \mathsf{Var}(x)$.

\medskip

\encoding
We close the chapter with an important note on terminology.
A formula like $P(\size{\mathsf{Plus}(\mathsf{Var}(x), \mathsf{Const}(7))})$ combines several levels of notation.
We consider that we are doing our mathematical reasoning in some \emph{metalanguage}\index{metalanguage}, which is often applicable to a wide variety of proof tasks.
We also happen to be applying it here to reason about some \emph{object language}\index{object language}, a programming language whose syntax is defined formally, here the language of arithmetic expressions.
We have $x$ as a variable of the metalanguage, while $\mathsf{Var}(x)$ is a variable expression of the object language.
It is difficult to use English to explain the distinction between the two in complete formality, but be on the lookout for places where formulas mix concepts of the metalanguage and object language!
The general patterns should soon become clear, as they are somehow already familiar to us from natural-language sentences like:
\begin{quote}
  The wise man said ``it is time to prove some theorems.''
\end{quote}
The quoted remark could just as well be in Spanish instead of English, in which case we have two languages nested in a nontrivial way.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Semantics via Interpreters}

That's enough about what programs \emph{look like}.
Let's shift our attention to what programs \emph{mean}.

\section{Semantics for Arithmetic Expressions via Finite Maps}

\newcommand{\mempty}[0]{\bullet}
\newcommand{\msel}[2]{#1(#2)}
\newcommand{\mupd}[3]{#1[#2 \mapsto #3]}

To explain the meaning of one of last chapter's arithmetic expressions, we need a way to indicate the value of each variable.
\encoding
A theory of \emph{finite maps}\index{finite map} is helpful here.
We apply the following notations throughout the book: \\

\begin{tabular}{rl}
  $\mempty$ & empty map, with $\emptyset$ as its domain \\
  $\msel{m}{k}$ & mapping of key $k$ in map $m$ \\
  $\mupd{m}{k}{v}$ & extension of map $m$ to also map key $k$ to value $v$
\end{tabular} \\

As the name advertises, finite maps are functions with finite domains, where the domain may be expanded by each extension operation.
Two axioms explain the essential interactions of the basic operators.

$$\infer{\msel{\mupd{m}{k}{v}}{k} = v}{}
\quad
\infer{\msel{\mupd{m}{k_1}{v}}{k_2} = m(k_2)}{
  k_1 \neq k_2
}$$

\newcommand{\denote}[1]{{\left \llbracket #1 \right \rrbracket}}

With these operators in hand, we can write a semantics for arithmetic expressions.
This is a recursive function that \emph{maps variable valuations to numbers}.
We write $\denote{e}$ for the meaning of $e$; this notation is often referred to as \emph{Oxford brackets}\index{Oxford brackets}.
Recall that we allow notations like this as syntactic sugar for arbitrary functions, even when giving the equations that define those functions.
We write $v$ for a valuation (finite map).
\encoding
\begin{eqnarray*}
  \denote{n}v &=& n \\
  \denote{x}v &=& v(x) \\
  \denote{e_1 + e_2}v &=& \denote{e_1}v + \denote{e_2}v \\
  \denote{e_1 \times e_2}v &=& \denote{e_1}v \times \denote{e_2}v
\end{eqnarray*}

Note how parts of the definition feel a little bit like cheating, as we just ``push notations inside the brackets.''
It's important to remember that plus \emph{inside} the brackets is syntax, while plus \emph{outside} the brackets is the normal addition of math!

\newcommand{\subst}[3]{[#3/#2]#1}

To test our semantics, we define a \emph{variable substitution} function\index{substitution}.
A substitution $\subst{e}{x}{e'}$ stands for the result of running through the syntax of $e$,
replacing every occurrence of variable $x$ with expression $e'$.

\begin{eqnarray*}
  \subst{n}{x}{e} &=& n \\
  \subst{x}{x}{e} &=& e \\
  \subst{y}{x}{e} &=& y \textrm{, when $y \neq x$} \\
  \subst{(e_1 + e_2)}{x}{e} &=& \subst{e_1}{x}{e} + \subst{e_2}{x}{e} \\
  \subst{(e_1 \times e_2)}{x}{e} &=& \subst{e_1}{x}{e} \times \subst{e_2}{x}{e}
\end{eqnarray*}

We can prove a key compatibility property of these two recursive functions.

\begin{theorem}
  For all $e$, $e'$, $x$, and $v$, $\denote{\subst{e}{x}{e'}}{v} = \denote{e}{(\mupd{v}{x}{\denote{e'}{v}})}$.
\end{theorem}

That is, in some sense, the operations of interpretation and substitution \emph{commute} with each other.
That intuition gives rise to the common notion of a \emph{commuting diagram}\index{commuting diagram}, like the one below for this particular example.

\[
\begin{tikzcd}
(e, v) \arrow{r}{\subst{\ldots}{x}{e'}} \arrow{d}{\mupd{\ldots}{x}{\denote{e'}v}} & (\subst{e}{x}{e'}, v) \arrow{d}{\denote{\ldots}} \\
(e, \mupd{v}{x}{\denote{e'}v}) \arrow{r}{\denote{\ldots}} & \denote{\subst{e}{x}{e'}}v
\end{tikzcd}
\]

We start at the top left, with a given expresson $e$ and valuation $v$.
The diagram shows the equivalence of \emph{two different paths} to the bottom right.
Each individual arrow is labeled with some description of the transformation it performs, to get from the term at its source to the term at its destination.
The right-then-down path is based on substituting and then interpreting, while the down-then-right path is based on extending the valuation and then interpreting.
Since both paths wind up at the same spot, the diagram indicates an equality between the corresponding terms.

It's a matter of taste whether the theorem statement or the diagram expresses the property more clearly!

\section{A Stack Machine}

As an example of a very different language, consider a \emph{stack machine}\index{stack machine}, similar at some level to, for instance, the Forth\index{Forth} programming language, or to various postfix\index{postfix} calculators.
\encoding
$$\begin{array}{rrcl}
  \textrm{Instructions} & i &::=& \mathsf{PushConst}(n) \mid \mathsf{PushVar}(x) \mid \mathsf{Add} \mid \mathsf{Multiply} \\
  \textrm{Programs} & \overline{i} &::=& \cdot \mid i; \overline{i}
\end{array}$$

Though here we defined an explicit grammar for programs, which are just sequences of instructions, in general we'll use the notation $\overline{X}$ to stand for sequences of $X$'s, and the associated concrete syntax won't be so important.
We also freely use single instructions to stand for programs, writing just $i$ in place of $i; \cdot$.

\newcommand{\push}[2]{#1 \rhd #2}

Each instruction of this language transforms a \emph{stack}\index{stack}, a last-in-first-out list of numbers.
Rather than spend more words on it, here is an interpreter that makes everythig precise.
Here and elsewhere, we overload the Oxford brackets $\denote{\ldots}$ shamelessly, where context makes clear which language or interpreter we are dealing with.
We write $s$ for stacks, and we write $\push{n}{s}$ for pushing number $n$ onto the top of stack $s$.

\encoding
\begin{eqnarray*}
  \denote{\mathsf{PushConst}(n)}(v,s) &=& \push{n}{s} \\
  \denote{\mathsf{PushVar}(x)}(v,s) &=& \push{\msel{v}{x}}{s} \\
  \denote{\mathsf{Add}}(v,\push{n_2}{\push{n_1}{s}}) &=& \push{(n_1 + n_2)}{s} \\
  \denote{\mathsf{Multiply}}(v,\push{n_2}{\push{n_1}{s}}) &=& \push{(n_1 \times n_2)}{s}
\end{eqnarray*}

The last two cases require the stack have at least a certain height.
Here we'll ignore what happens when the stack is too short, though it suffices, for our purposes, to add pretty much any default behavior for the missing cases.
We overload $\denote{\overline{i}}$ to refer to the \emph{composition} of the interpretations of the different instructions within $\overline{i}$, in order.

Next, we give our first example of what might be called a \emph{compiler}\index{compiler}, or a translation from one language to another.
Let's compile arithmetic expressions into stack programs, which then become easy to map onto the instructions of common assembly languages.
In that sense, with this translation, we make progress toward efficient implementation on commodity hardware.

\newcommand{\compile}[1]{{\left \lfloor #1 \right \rfloor}}
\newcommand{\concat}[2]{#1 \bowtie #2}

Throughout this book, we will use notation $\compile{\ldots}$ for compilation, where the floor-based notation suggests \emph{moving downward} to a lower abstraction level.
Here is the compiler that concerns us now, where we write $\concat{s_1}{s_2}$ for concatenation of two stacks $s_1$ and $s_2$.
\encoding
\begin{eqnarray*}
  \compile{n} &=& \mathsf{PushConst}(n) \\
  \compile{x} &=& \mathsf{PushVar}(n) \\
  \compile{e_1 + e_2} &=& \concat{\compile{e_1}}{\concat{\compile{e_2}}{\mathsf{Add}}} \\
  \compile{e_1 \times e_2} &=& \concat{\compile{e_1}}{\concat{\compile{e_2}}{\mathsf{Multiply}}}
\end{eqnarray*}

The first two cases are straightforward: their compilations just push the obvious values onto the stack.
The binary operators are just slightly more tricky.
Each first evaluates its operands in order, where each operand leaves its final result on the stack.
With both of them in place, we run the instruction to pop them, combine them, and push the result back onto the stack.

The correctness theorem for compilation must refer to both of our interpreters.
From here on, we consider that all unaccounted-for variables in a theorem statement are quantified universally.

\begin{theorem}
  $\denote{\compile{e}}(v, \cdot) = \denote{e}v$.
\end{theorem}

Here's a restatement as a commuting diagram.

\[
\begin{tikzcd}
e \arrow{r}{\compile{\ldots}} \arrow{dr}{\denote{\ldots}} & \compile{e} \arrow{d}{\denote{\ldots}} \\
& \denote{e}
\end{tikzcd}
\]

As usual, we leave proof details for the associated Coq code, but the key insight of the proof is to strengthen the induction hypothesis via a lemma.

\begin{lemma}
  $\denote{\concat{\compile{e}}{\overline{i}}}(v, s) = \denote{\overline{i}}(v, \concat{\denote{e}v}{s})$.
\end{lemma}

We strengthen the statement by considering both an arbitrary initial stack $s$ and a sequence of extra instructions $\overline{i}$ to be run after $e$.

\section{A Simple Higher-Level Imperative Language}

\newcommand{\repet}[2]{\mathsf{repeat} \; #1 \; \mathsf{do} \; #2 \; \mathsf{done}}

The interpreter approach to semantics is usually the most convenient one, when it applies.
Coq requires that all programs terminate, and that requirement is effectively also present in informal math, though it is seldom called out with the same terms.
Instead, with math, we worry about whether recursive systems of equations are well-founded, in appropriate senses.
From either perspective, extra encoding tricks are required to write a well-formed interpreter for a Turing-complete\index{Turing-completeness} language.
We will dodge those complexities for now by defining a simple imperative language with bounded loops, where termination is easy to prove.
We take the arithmetic expression language as a base.
\encoding
$$\begin{array}{rrcl}
  \textrm{Command} & c &::=& \mathsf{skip} \mid x \leftarrow e \mid c; c \mid \repet{e}{c}
\end{array}$$

Now the implicit state, read and written by a command, is a variable valuation, as we used in the interpreter for expressions.
A $\mathsf{skip}$ command does nothing, while $x \leftarrow e$ extends the valuation to map $x$ to the value of expression $e$.
We have simple command sequencing $c_1; c_2$, in addition to the bounded loop $\repet{e}{c}$, which executes $c$ a number of times equal to the value of $e$.

\newcommand{\id}[0]{\mathsf{id}}

To give the semantics, we need a few commonplace notations that are worth reviewing.
We write $\id$ for the identity function\index{identity function}, where $\id(x) = x$; and we write $f \circ g$ for composition of functions\index{composition of functions} $f$ and $g$, where $(f \circ g)(x) = f(g(x))$.
We also have iterated self-composition\index{self-composition}, written like \emph{exponentiation} of functions\index{exponentiation of functions} $f^n$, defined as follows.
\begin{eqnarray*}
  f^0 &=& \id \\
  f^{n+1} &=& f^n \circ f
\end{eqnarray*}

From here, $\denote{\ldots}$ is easy to define yet again, as a transformer over variable valuations.
\encoding
\begin{eqnarray*}
  \denote{\mathsf{skip}}v &=& v \\
  \denote{x \leftarrow e}v &=& \mupd{v}{x}{\denote{e}v} \\
  \denote{c_1; c_2}v &=& \denote{c_2}(\denote{c_1}v) \\
  \denote{\repet{e}{c}}v &=& \denote{c}^{\denote{e}v}(v)
\end{eqnarray*}

To put this semantics through a workout, let's consider a simple \emph{optimization}\index{optimization}, a transformation whose input and output programs are in the same language.
There's an additional, fuzzier criterion for an optimization, which is that it should improve the program somehow, usually in terms of running time, memory usage, etc.
The optimization we choose here may be a bit dubious in that respect, though it is related to an optimization found in every serious C\index{C programming language} compiler.

In particular, let's tackle \emph{loop unrolling}\index{loop unrolling}.
When the iteration count of a loop is a constant $n$, we can replace the loop with $n$ sequenced copies of its body.
C compilers need to work harder to find the iteration count of a loop, but luckily our language includes loops with very explicit iteration counts!
To define the transformation, we'll want a recursive function and notation for sequencing of $n$ copies of a command $c$, written $^nc$.
\begin{eqnarray*}
  ^0c &=& \mathsf{skip} \\
  ^{n+1}c &=& c; {^nc}
\end{eqnarray*}

\newcommand{\opt}[1]{{\left | #1 \right |}}

Now the optimization itself is easy to define.
We'll write $\opt{\ldots}$ for this and other optimizations, which move neither down nor up a tower of program abstraction levels.
\encoding
\begin{eqnarray*}
  \opt{\mathsf{skip}} &=& \mathsf{skip} \\
  \opt{x \leftarrow e} &=& x \leftarrow e \\
  \opt{c_1; c_2} &=& \opt{c_1}; \opt{c_2} \\
  \opt{\repet{n}{c}} &=& ^n\opt{c} \\
  \opt{\repet{e}{c}} &=& \repet{e}{\opt{c}}
\end{eqnarray*}

Note that, when multiple defining equations apply to some function input, by convention we apply the \emph{earliest} equation that matches.

Let's prove that this optimization preserves program behavior; that is, we prove that it is \emph{semantics preserving}\index{semantics preservation}.

\begin{theorem}\label{unroll}
  $\denote{\opt{c}}v = \denote{c}v$.
\end{theorem}

It all looks so straightforward from that statement, doesn't it?
Indeed, there actually isn't so much work to do to prove this theorem.
We can also present it as a commuting diagram much like the prior one.

\[
\begin{tikzcd}
c \arrow{r}{\opt{\ldots}} \arrow{dr}{\denote{\ldots}} & \opt{c} \arrow{d}{\denote{\ldots}} \\
& \denote{c}
\end{tikzcd}
\]

The statement of Theorem \ref{unroll} happens to already be in the right form to do induction directly, but we need a helper lemma, capturing the interaction of $^nc$ and the semantics.

\begin{lemma}
  $\denote{^nc} = \denote{c}^n$.
\end{lemma}

Let us end the chapter with the commuting-diagram version of the lemma statement.

\[
\begin{tikzcd}
c \arrow{r}{^n\ldots} \arrow{d}{\denote{\ldots}} & ^nc \arrow{d}{\denote{\ldots}} \\
\denote{c} \arrow{r}{\ldots^n} & \denote{c}^n
\end{tikzcd}
\]


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Transition Systems and Invariants}

For simple programming languages where programs always terminate, it is often most convenient to formalize them using interpreters, as in the last chapter.
However, many important languages don't fall into that category, and for them we need different techniques.
Nontermination isn't always a bug; for instance, we expect a network server to run indefinitely.
We still need to be able to talk about the correct behavior of programs that run forever, by design.
For that reason, in this chapter and in most of the rest of the book, we model programs using relations, in much the same way that may be familiar from automata theory\index{automata theory}.
An important difference, though, is that, while undergraduate automata-theory classes generally study \emph{finite-state machines}\index{finite-state machines}, for general program reasoning we want to allow infinite sets of states, otherwise referred to as \emph{infinite-state systems}\index{infnite-state systems}.

Let's start with an example that almost seems too mundane to be associated with such terms.

\section{Factorial as a State Machine}

We're familiar with the factorial operation, implemented as an imperative program with a loop.
\begin{verbatim}
factorial(n) {
  a = 1;
  while (n > 0) {
    a = a * n;
    n = n - 1;
  }
  return a;
}
\end{verbatim}

In the analysis to follow, consider some value $n_0 \in \mathbb N$ fixed, as the input passed to this operation.
A state machine is lurking within the surface syntax of the program.
\encoding
In fact, we have a variety of choices in modeling it as a state machine.
Here is the set of states that we choose to use here:
$$\begin{array}{rrcl}
  \textrm{Natural numbers} & n &\in& \mathbb N \\
  \textrm{States} & s &::=& \mathsf{AnswerIs}(n) \mid \mathsf{WithAccumulator}(n, n)
\end{array}$$

There are two types of states.
An $\mathsf{AnswerIs}(a)$ state corresponds to the \texttt{return} statement.
It records the final result $a$ of the factorial operation.
A $\mathsf{WithAccumulator}(n, a)$ records an intermediate state, giving the values of the two local variables, just before a loop iteration begins.

Following the more familiar parts of automata theory, let's define a set of \emph{initial states}\index{initial state} for this machine.
$$\infer{\mathsf{WithAccumulator}(n_0, 1) \in \mathcal F_0}{}$$
For consistency with the notation we will be using later, we define the set $\mathcal F_0$ using an inference rule.
Equivalently, we could just write $\mathcal F_0 = \{\mathsf{WithAccumulator}(n_0, 1)\}$, essentially reading off the initial variable values from the first lines of the code above.

Similarly, we also define a set of \emph{final states}\index{final state}.
$$\infer{\mathsf{AnswerIs}(a) \in \mathcal F_\omega}{}$$
Equivalently: $\mathcal F_\omega = \{\mathsf{AnswerIs}(a) \mid a \in \mathbb N\}$.
Note that this definition only captures when the program is \emph{done}, not when it \emph{returns the right answer}.
It follows from the last line of the code.

The last and most important ingredient of our state machine is its \emph{transition relation}, where we write $s \to s'$ to indicate that state $s$ advances to state $s'$ in one step, following the semantics of the program.
Here inference rules are more obviously a good fit.
$$\infer{\mathsf{WithAccumulator}(0, a) \to \mathsf{AnswerIs}(a)}{}$$
$$\infer{\mathsf{WithAccumulator}(n+1, a) \to \mathsf{WithAccumulator}(n, a \times (n+1))}{}$$
The first rule corresponds to the case where the program ends, because the loop test has failed and we now know the final answer.
The second rule corresponds to going once around the loop, following directly from the code in the loop body.

We can fit these ingredients into the general concept of a \emph{transition system}\index{transition system}, the term we will use throughout this book for this sort of state machine.
Actually, the words ``state machine'' suggest to many people that the state set must be finite, hence our preference for ``transition system,'' which is also used fairly frequently in semantics.

\newcommand{\angled}[1]{{\left \langle #1 \right \rangle}}

\begin{definition}
  A \emph{transition system} is a triple $\angled{S, S_0, \to}$, with $S$ a set of states, $S_0 \subseteq S$ a set of initial states, and $\to \; \subseteq S \times S$ a transition relation.
\end{definition}

For an arbitrary transition relation $\to$, not just the one defined above for factorial, we define its \emph{transitive-reflexive closure}\index{transitive-reflexive closure} $\to^*$ with two inference rules:
$$\infer{s \to^* s}{}
\quad \infer{s \to^* s''}{
  s \to s'
  & s' \to^* s''
}$$
That is, a formal claim $s \to^* s'$ corresponds exactly to the informal claim that ``starting from state $s$, we can reach state $s'$.''

\begin{definition}
  For transition system $\angled{S, S_0, \to}$, we say that a state $s$ is \emph{reachable} if and only if there exists $s_0 \in S_0$ such that $s_0 \to^* s$.
\end{definition}

Building on these notations, here is one way to state the correctness of our factorial program, which, defining $S$ according to the state grammar above, we model as $\mathcal F = \angled{S, \mathcal F_0, \to}$.

\begin{theorem}\label{factorial_ok}
  For any state $s$ reachable in $\mathcal F$, if $s \in \mathcal F_\omega$, then $s = \mathsf{AnswerIs}(n_0!)$.
\end{theorem}

That is, whenever the program finishes, it returns the right answer.
(Recall that $n_0$ is the initial value of the input variable.)

We could prove this theorem now in a relatively ad-hoc way.
Instead, let's develop the general machinery of \emph{invariants}.


\section{Invariants}

The concept of ``invariant'' may be familiar from such relatively informal notions as ``loop invariant''\index{loop invariant} in introductory programming classes.
Intuitively, an invariant is a property of program state that \emph{starts true and stays true}, but let's make that idea a bit more formal, as applied to our transition-system formalism.

\newcommand{\invariants}[0]{\marginpar{\fbox{\textbf{Invariants}}}}

\invariants
\begin{definition}
  An \emph{invariant} of a transition system is a property that is always true, in all reachable states of a transition system.  That is, for transition system $\angled{S, S_0, \to}$, where $R$ is the set of all its reachable states, some $I \subseteq S$ is an invariant iff $R \subseteq I$.
\end{definition}

At first look, the definition may appear a bit silly.
Why not always just take the reachable states $R$ as the invariant, instead of scrambling to invent something new?
The reason is the same as for strengthening induction hypotheses to make proofs easier.
Often it is easier to characterize an invariant that isn't fully precise, admitting some states that the system can never actually reach.
Additionally, it can be easier to prove existence of an approximate invariant by induction, by the method that the next key theorem formalizes.

\begin{theorem}\label{invariant_induction}
  Consider a transition system $\angled{S, S_0, \to}$ and its candidate invariant $I$.  The candidate is truly an invariant if (1) $S_0 \subseteq I$ and (2) for every $s \in I$ where $s \to s'$, we also have $s' \in I$.
\end{theorem}

That's enough generalities for now.
Let's define a suitable invariant for factorial.
\invariants
\begin{eqnarray*}
  I(\mathsf{AnswerIs}(a)) &=& n_0! = a \\
  I(\mathsf{WithAccumulator}(n, a)) &=& n_0! = n! \times a
\end{eqnarray*}

It is an almost-routine exercise to prove that $I$ really is an invariant, using Theorem \ref{invariant_induction}.
The key new ingredient we need is \emph{inversion}, a principle for deducing which inference rules may have been used to prove a fact.

For instance, at one point in the proof, we need to draw a conclusion from a premise $s \in \mathcal F_0$, meaning that $s$ is an initial state.
By inversion, because set $\mathcal F_0$ is defined by a single inference rule, that rule must have been used to conclude the premise, so it must be that $s = \mathsf{WithAccumulator}(n_0, 1)$.

Similarly, at another point in the proof, we must reason from a premise $s \to s'$.
The relation $\to$ is defined by two inference rules, so inversion leads us to two cases to consider.
In the first case, corresponding to the first rule, $s = \mathsf{WithAccumulator}(0, a)$ and $s' = \mathsf{AnswerIs}(a)$.
In the second case, corresponding to the second rule, $s = \mathsf{WithAccumulator}(n+1, a)$ and $s' = \mathsf{WithAccumulator}(n, a \times (n+1))$.
It's worth checking that these values of $s$ and $s'$ are read off directly from the rules.

Though a completely formal and exhaustive treatment of inversion is beyond the scope of this text, generally it follows standard intuitions about ``reverse-engineering'' a set of rules that could have been used to derive some premise.

Another important property of invariants formalizes the connection with weakening an induction hypothesis.

\begin{theorem}\label{invariant_weaken}
  If $I$ is an invariant of a transition system, then $I' \supseteq I$ (a superset of the original) is also an invariant of the same system.
\end{theorem}

Note that the larger $I'$ above may not be suitable to use in an inductive proof by Theorem \ref{invariant_induction}!
For instance, for factorial, we might define $I' = \mathcal \{\mathsf{AnswerIs}(n_0)\} \cup \{\mathsf{WithAccumulator}(n, a) \mid n, a \in \mathbb N\}$, clearly a superset of $I$.
However, by forgetting everything that we know about intermediate $\mathsf{WithAccumulator}$ states, we will get stuck on the inductive step of the proof.
Thus, what we call invariants here needn't also be \emph{inductive invariants}\index{inductive invariants}, and there may be slight terminology mismatches with other sources.

Combining Theorems \ref{invariant_induction} and \ref{invariant_weaken}, it is now easy to prove Theorem \ref{factorial_ok}, establishing the correctness of our particular factorial system $\mathcal F$.
First, we use Theorem \ref{invariant_induction} to deduce that $I$ is an invariant of $\mathcal F$.
Then, we choose the very same $I'$ that we warned above is not an inductive invariant, but which is fairly easily shown to be a superset of $I$.
Therefore, by Theorem \ref{invariant_weaken}, $I'$ is also an invariant of $\mathcal F$, and Theorem \ref{factorial_ok} follows quite directly from that fact, as $I'$ is essentially a restatement of Theorem \ref{factorial_ok}.

\section{Rule Induction}

Another crucial reasoning technique was hidden within the elided proof of Theorem \ref{invariant_induction}.
That technique is \emph{rule induction}\index{rule induction}, which generalizes inversion just as normal structural induction generalizes case analysis.
As an example, consider again the definition of transitive-reflexive closure by inference rules.
$$\infer{s \to^* s}{}
\quad \infer{s \to^* s''}{
  s \to s'
  & s' \to^* s''
}$$

The relation $\to^*$ is a subset of $S \times S$.
Imagine that we want to prove that some relation $P$ holds of all pairs of states, where the first can reach the second.
That is, we want to prove $\forall s, s'. \; (s \to^* s') \Rightarrow P(s, s')$, where $\Rightarrow$ is logical implication.
We can actually derive a suitable induction principle, in the same way that we produced structural induction principles from definitions of inductive datatypes.
We modify each defining rule of $\to^*$, replacing its conclusion with a use of $P$ and adding a $P$ induction hypothesis for each recursive premise.
$$\infer{P(s, s)}{}
\quad \infer{P(s, s'')}{
  s \to s'
  & s' \to^* s''
  & P(s', s'')
}$$
As before, where the defining rules of $\to^*$ show us how to \emph{conclude} facts, the two new rules here are \emph{proof obligations}.
To apply rule induction and establish $P$ for all reachability pairs, we must prove that each new rule is correct, as a kind of quantified implication.

As a simpler example than the invariant-induction theorem, consider transitivity for reachability.

\begin{theorem}
  If $s \to^* s'$ and $s' \to^* s''$, then $s \to^* s''$.
\end{theorem}
\begin{proof}
  By rule induction on the derivation of $s \to^* s'$, taking $P(s_1, s_2)$ to be that, if $s_2 = s'$, then $s_1 \to^* s''$.  We consider variables $s'$ and $s''$ fixed throughout the induction, along with their associated premise $s' \to^* s''$.

  \emph{Base case:} We must show $P(s, s)$ for an arbitrary $s$.  Given that (based on the definition of $P$) we may assume $s = s'$, our premise $s' \to^* s''$ precisely matches the desired conclusion $s \to^* s''$.

  \emph{Induction step:} Assume $s \to s_1$, $s_1 \to^* s'$, and $P(s_1, s')$.  We may apply the second rule defining $\to^*$, whose two premises become $s \to s_1$ and $s_1 \to^* s''$.  The first is one of the available premises of the induction step.  The second follows by the induction hypothesis about $P$.
\end{proof}

This sort of proof really is easier to follow in Coq code, so we especially encourage the reader to consult the mechanized version here!

In general, any inductive definition of a predicate, via a set of inference rules, implies a rule-induction principle.
We will meet many such definitions throughout the book, and we will apply rule induction to most of them.
It is valuable to understand basically how the rule-induction principle of a definition is read off from its original rules, but it is also true that Coq comes up with these principles automatically.


\section{An Example with a Concurrent Program}

Imagine that we want to verify a multithreaded\index{multithreaded programs}, shared-memory program\index{shared-memory programming} where multiple threads run this code at once.
\begin{verbatim}
f() {
  lock();
  local = global;
  global = local + 1;
  unlock();
}
\end{verbatim}

Consider \texttt{global} as a variable shared across all threads, while each thread has its own version of variable \texttt{local}.
The meaning of \texttt{lock()} and \texttt{unlock()} is as usual\index{locks}, where at most one thread can hold the lock at once, claiming it via \texttt{lock()} and relinquishing it via \texttt{unlock()}.
When variable \texttt{global} is initialized to 0 and $n$ threads run this code at once and all terminate, we expect that \texttt{global} finishes with value $n$.
Of course, bugs in this program, like forgetting to include the locking, could lead to all sorts of wrong answers, with any value between 1 and $n$ possible with the right demonic thread interleaving.

\encoding
To prove that we got the program right, let's formalize it as a transition system.  First, our state set:
$$\begin{array}{rrcl}
  \textrm{States} & S &::=& \mathsf{Lock} \mid \mathsf{Read} \mid \mathsf{Write}(n) \mid \mathsf{Unlock} \mid \mathsf{Done}
\end{array}$$

Compared to the last example, here we see more clearly that kinds of states correspond to \emph{program counters}\index{program counters} in the imperative code.
The first four state kinds respectively mean that the program counter is right before the matching line in the program's code.
The last state kind means the program counter is past the end of the function.
Only $\mathsf{Write}$ states carry extra information, in this case the value of variable \texttt{local}.
At every other program counter, we can prove that the value of variable \texttt{local} has no effect on further transitions, so we don't bother to store it.
We will account for the value of variable \texttt{global} separately, in a way to be described shortly.

In particular, we will define a transition system for a single thread as $\mathcal L = \angled{(\mathbb N \times \mathbb B) \times S, \mathcal L_0, \to_{\mathcal L}}$.
We define the state to include not only the thread-local state $S$ but also the value of \texttt{global} (in $\mathbb N$) and whether the lock is currently taken (in $\mathbb B$, the Booleans, with values $\top$ [true] and $\bot$ [false]).
There is one designated initial state.

$$\infer{((0, \bot), \mathsf{Lock}) \in \mathcal L_0}{}$$

Four inference rules explain the four transitions between program counters that a single thread can make, reading and writing shared state as needed.

$$\infer{((\bot, g), \mathsf{Lock}) \to_{\mathcal L} ((\top, g), \mathsf{Read})}{}
\quad \infer{((\ell, g), \mathsf{Read}) \to_{\mathcal L} ((\ell, g), \mathsf{Write}(g))}{}$$
$$\infer{((\ell, g), \mathsf{Write}(n)) \to_{\mathcal L} ((\ell, n+1), \mathsf{Unlock})}{}
\quad \infer{((\ell, g), \mathsf{Unlock}) \to_{\mathcal L} ((\bot, g), \mathsf{Done})}{}$$

\smallskip

Note that these rules will allow a thread to read and write the shared state even without holding the lock.
The rules also allow any thread to unlock the lock, with no consideration for whether that thread must be the current lock holder.
We must use an invariant-based proof to show that there are, in fact, no lurking violations of the lock-based concurrency discipline.

Of course, with just a single thread running, there aren't any interesting violations!
However, we have been careful to describe system $\mathcal L$ in a generic way, with its state a pair of shared and private components.
We can define a generic notion of a multithreaded system, with two systems that share some state and maintain their own private state.

\encoding
\begin{definition}
  Let $T^1 = \angled{S \times P^1, S_0 \times P^1_0, \to^1}$ and $T^2 = \angled{S \times P^2, S_0 \times P^2_0, \to^2}$ be two transition systems, with a shared-state type $S$ in common between their state sets, also agreeing on the initial values $S_0$ for that shared state.  We define the \emph{parallel composition} $T^1 \mid T^2$ as $\angled{S \times (P^1 \times P^2), S_0 \times (P^1_0 \times P^2_0), \to}$, defining new transition relation $\to$ with the following inference rules, which capture the usual notion of thread interleaving.
  $$\infer{(s, (p_1, p_2)) \to (s', (p'_1, p_2))}{
    (s, p_1) \to^1 (s', p'_1)
  }
  \quad \infer{(s, (p_1, p_2)) \to (s', (p_1, p'_2))}{
    (s, p_2) \to^2 (s', p'_2)
  }$$
\end{definition}

Note that the operator $\mid$ is carefully defined so that its output is suitable as input to a further instance of itself.
As a result, while $\mathcal L \mid \mathcal L$ is a transition system modeling two threads running the code from above, we also have $\mathcal L \mid (\mathcal L \mid \mathcal L)$ as a three-thread system based on that code, $(\mathcal L \mid \mathcal L) \mid (\mathcal L \mid \mathcal L)$ as a four-thread system based on that code, etc.

Also note that $\mid$ constructs transition systems with our first examples of \emph{nondeterminism}\index{nondeterminism} in transition relations.
That is, given a particular starting state, there are multiple different places it may wind up after a given number of execution steps.
In general, with thread-interleaving concurrency, the set of possible final states grows exponentially in the number of steps, a fact that torments concurrent-software testers to no end!
Rather than consider all possible runs of the program, we will use an invariant to tame the complexity.

First, we should be clear on what we mean to prove about this program.
Let's also restrict our attention to the two-thread case for the rest of this section; the $n$-thread case is left as an exercise for the reader!
\begin{theorem}
  For any reachable state $((\ell, g), (p^1, p^2))$ of $\mathcal L \mid \mathcal L$, if $p^1 = p^2 = \mathsf{Done}$, then $g = 2$.
\end{theorem}
That is, when both threads terminate, \texttt{global} equals 2.

As a first step toward an invariant, define function $\mathcal C$ from private states to numbers, capturing the \emph{contribution of} a thread with that state, summarizing how much that thread has added to \texttt{globals}.
\begin{eqnarray*}
  \mathcal C(p) &=& \begin{cases}
    1 & p \in \{\mathsf{Unlock}, \mathsf{Done}\} \\
    0 & \mathrm{otherwise}
  \end{cases}
\end{eqnarray*}

Next, we define a function that, given a thread's private state, determines whether that thread \emph{holds the lock}.
\begin{eqnarray*}
  \mathcal H(p) &=& \begin{cases}
    \bot & p \in \{\mathsf{Lock}, \mathsf{Done}\} \\
    \top & \mathrm{otherwise}
  \end{cases}
\end{eqnarray*}

Now, the main insight: we can reconstruct the shared state uniquely from the two private states!
Function $\mathcal S$ does exactly that.
\begin{eqnarray*}
  \mathcal S(p^1, p^2) &=& (\mathcal H(p^1) \lor \mathcal H(p^2), \mathcal C(p^1) + \mathcal C(p^2))
\end{eqnarray*}

One last ingredient will help us write the invariant: a predicate $\mathcal O(p, p')$ capturing when, given the state $p$ of one thread, the state $p'$ is compatible with all of the implications of $p$'s state, primarily in terms of mutual exclusion\index{mutual exclusion} for the lock.
\begin{eqnarray*}
  \mathcal O(p, p') &=& \begin{cases}
    \top & p \in \{\mathsf{Lock}, \mathsf{Done}\} \\
    \neg \mathcal H(p') & p \in \{\mathsf{Read}, \mathsf{Unlock}\} \\
    \neg \mathcal H(p') \land n = \mathcal C(p') & p = \mathsf{Write}(n)
  \end{cases}
\end{eqnarray*}

Finally, we can write the invariant.
\invariants
\begin{eqnarray*}
  I(s, (p^1, p^2)) &=& \mathcal O(p^1, p^2) \land \mathcal O(p^2, p^1) \land s = \mathcal S(p^1, p^2)
\end{eqnarray*}

As is often the case, defining the invariant is the hard part of the proof, and the rest follows by the standard methodology that we used for factorial.
To recap that method, first we use Theorem \ref{invariant_induction} to show that $I$ really is an invariant of $\mathcal L \mid \mathcal L$.
Next, we use Theorem \ref{invariant_weaken} to show that $I$ implies the original property of interest, that finished program states have value 2 for \texttt{global}.
Most of the action is in the first step, where we must work through fussy details of all the different steps that could happen from a state within the invariant, using arithmetic reasoning in each case to either derive a contradiction (that step couldn't happen from this starting state) or show that a specific new state also belongs to the invariant.
We leave those details to the Coq code, as usual.

The reader may be worried at this point that coming up with invariants can be rather tedious!
In the next chapter, we meet a technique for finding invariants automatically, in some limited but important circumstances.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Model Checking}

Our analyses so far have been tedious for at least two different reasons.
First, we've hand-crafted definitions of transition systems, rather than just writing programs in conventional programming languages.
The next chapter will clear that obstacle, by introducing operational semantics, for building transition systems automatically from programs.
The other inconvenience we've faced is defining invariants manually.
There isn't a silver bullet to get us out of this duty, when working with Turing-complete languages\index{Turing-completeness}, where almost all interesting questions, this one included, are undecidable.
However, when we can phrase problems in terms of transition systems with \emph{finitely many reachable states}, we can construct invariants automatically by \emph{exhaustive exploration of the state space}, an approach otherwise known as \emph{model checking}\index{model checking}.
Surprisingly many real programs can be reduced to finite state spaces, using the techniques introduced in this chapter.
First, though, let's formalize our intuitions about exhaustive state-space exploration as a sound way to find invariants.

\section{Exhaustive Exploration}

For an arbitrary binary relation $R$, we write $R^n$ for the $n$-times self-composition of $R$\index{self-composition of relations}.
Formally, where $\mathsf{id}$ is the identity relation\index{identity relation} that only relates values to themselves, we have:
\begin{eqnarray*}
  R^0 &=& \mathsf{id} \\
  R^{n+1} &=& R \circ R^n
\end{eqnarray*}

For some set $S$ and binary relation $R$, we also write $R(S)$ for the composition of $R$ and $S$\index{composition of a relation and a set}, namely $\{x \mid \exists y \in S. \; y \; R \; x\}$.

\newcommand{\ns}[0]{\hspace{-.05in}}

Which states of transition system $\angled{S, S_0, \to}$ are reachable after 0 steps?
That would be precisely the initial states $S_0$, which we can also write as $\to^0\ns(S_0)$.

Which states are reachable after exactly 1 step?
That is $\to\ns(S_0)$, or $\to^1\ns(S_0)$.

How about 2, 3, and 4 steps?
There we have $\to^2\ns(S_0)$, $\to^3\ns(S_0)$, and $\to^4\ns(S_0$).

It follows that the set of states reachable after $n$ steps is:
\begin{eqnarray*}
  \mathsf{reach}(n) &=& \bigcup_{i < n} \to^i\ns(S_0)
\end{eqnarray*}

This iteration process is not obviously executable yet, because, a priori, we seem to need to consider all possible $n$ values, to characterize the state space fully.
However, a crucial property allows us to terminate our search soundly under some conditions.

\begin{theorem}
  \invariants
  If $\mathsf{reach}(n+1) = \mathsf{reach}(n)$ for some $n$, then $\mathsf{reach}(n)$ is an invariant of the system.
\end{theorem}

Here we call $\mathsf{reach}(n)$ a \emph{fixed point}\index{fixed point} of the transition system, because it is closed under further exploration.
To find a fixed point with a concrete system, we start with $S_0$.
We repeatedly take the \emph{single-step closure}\index{single-step closure} corresponding to composition with $\to$.
At each step, we check whether the expanded set is actually equal to the previous set.
If so, our process of \emph{multi-step closure}\index{multi-step closure} has terminated, and we have an invariant, by construction.
Again, keep in mind that multi-step closure will not terminate for most transition systems, and there is an art to phrasing a problem in terms of systems where it \emph{will} terminate.


\section{Abstracting a Transition System}

When analyzing an infinite-state system, it is not necessary to give up hope for model checking.
For instance, consider this program.
\begin{verbatim}
int global = 0;

thread() {
 int local;

 while (true) {
   local = global;
   global = local + 2;
 }
}
\end{verbatim}

If we assume infinite-precision integers, then the state space is infinite.
Considering just the global variable, every even number is reachable, even if we only run a single thread.
However, there is a high degree of regularity across this state space.
In particular, those values really are all even.
Consider this other program, which is hauntingly similar to the last one, in a way that we will make precise shortly.
\begin{verbatim}
bool global = true;

thread() {
  bool local;

  while (true) {
    local = global;
    global = local;
  }
}
\end{verbatim}

We replaced every use of an integer with \emph{a Boolean that is true iff the integer is even}.
Notice that now the program has a finite state space, and model checking applies easily!
We can formalize such a transformation via the general principle of \emph{abstraction of a transition system}\index{abstraction}.

\newcommand{\simulate}[0]{\prec}

The key idea is that every state of the concrete system (with relatively many states) can be associated to one or more states of the abstract system (with relatively few states).
We formalize this association via a \emph{simulation relation}\index{simulation relation} $R$, and we define what makes a choice of $R$ sound, via a notion of \emph{simulation}\index{simulation} via a binary operator $\simulate$, subscripted by $R$.

$$\infer{\angled{S, S_0, \to} \simulate_R \angled{S', S'_0, \to'}}{
  (\forall s \in S_0. \; \exists s' \in S'_0. \; s \; R \; s')
  & (\forall s, s', s_1. \; s \; R \; s' \land s \to s_1 \Rightarrow \exists s'_1. \; s' \to' s'_1 \land s_1 \; R \; s'_1)
}$$

The simpler condition is that every concrete initial state must be related to at least one abstract initial state.
The second, more complex condition essentially says that every step in the concrete world must be matchable by some related step in the abstract world.
A commuting diagram may express the second condition more clearly.
\[
\begin{tikzcd}
s \arrow{r}{\to} \arrow{d}{R} & s_1 \arrow{d}{R} \\
s' \arrow{r}{\exists \to'} & s'_1
\end{tikzcd}
\]

At an even higher intuitive level, what simulation says is that every execution of the concrete system may be matched, step for step, by an execution of the abstract system.
The relation $R$ explains the rules for which states match across systems.
For our purposes, the key pay-off from this connection is that we may translate any invariant of the abstract system into an invariant of the concrete system.

\newcommand{\abstraction}[0]{\marginpar{\fbox{\textbf{Abstraction}}}}

\begin{theorem}\label{abstract_simulation}
  \abstraction
  If $\angled{S, S_0, \to} \simulate_R \angled{S', S'_0, \to'}$, and if $I$ is an invariant of $\angled{S', S'_0, \to'}$, then $R^{-1}(I)$ is an invariant of $\angled{S, S_0, \to}$.
\end{theorem}

We can apply this theorem to the two example programs from earlier in the section.
The concrete system can be represented with thread-local states $\{\mathsf{Read}\} \cup \{\mathsf{Write}(n) \mid n \in \mathbb N\}$ and the abstract system with $\{\mathsf{BRead}\} \cup \{\mathsf{BWrite}(b) \mid b \in \mathbb B\}$, for the Booleans $\mathbb B$.
We define compatibility between local states.

$$\infer{\mathsf{Read} \sim \mathsf{BRead}}{}
\quad \infer{\mathsf{Write}(n) \sim \mathsf{BWrite}(b)}{
  n \; \textrm{even} \Leftrightarrow b = \mathsf{true}
}$$

We also define the overall state simulation relation $R$, which also covers state shared by threads.

$$\infer{(n, (\ell_1, \ell_2)) \; R \; (b, (\ell'_1, \ell'_2))}{
  (n \; \textrm{even} \Leftrightarrow b = \mathsf{true})
  & \ell_1 \sim \ell'_1
  & \ell_2 \sim \ell'_2
}$$

By proving that $R$ is truly a simulation relation, we reduce the problem to finding an invariant for the abstract system, which is easy to do with model checking.

One crucial consequence of abstraction-by-simulation deserves mentioning:
We show that every concrete execution is matched abstractly, but there may also be additional abstract executions that don't match any concrete ones.
In model checking the abstract system, we may do extra work to handle these ``useless'' paths!
If we do manage to handle them all, then Theorem \ref{abstract_simulation} applies perfectly well.
However, we should be careful, in our choices of abstractions, to bias our designs toward those that don't introduce extra complexities.


\section{Modular Decomposition of Invariant-Finding}

Many transition systems are straightforward to abstract into others, as single global steps.
Other times, the right way to tame a complex system is to decompose it into others and analyze them separately for invariants.
In such cases, the key is a proof principle to combine the invariants of the component systems into an invariant of the overall system.
We will refer to this style of proof decomposition as \emph{modularity}\index{modularity}, and this section gives our first example of modularity, for multithreaded systems.

Imagine that we have a system consisting of $n$ different copies of a transition system $\angled{S, S_0, \to}$ running as concurrent threads, modeled in the way introduced in the previous chapter.
It's not obvious that we can analyze each thread separately, since, during that thread's execution, the other threads are constantly interrupting and modifying global state.
To make matters worse, we can only understand their patterns of state modification by analyzing their thread-local state.
The situation seems inherently unmodular.

However, consider the following construction on transition systems.
Given a transition relation $\to$ and an invariant $I$ on the global state shared by all threads, we define a new transition relation $\to^I$ as follows.
$$\infer{s \to^I s'}{
  s \to s'
}
\quad \infer{(g, \ell) \to^I (g', \ell)}{
  I(g')
}$$

The first rule says that any step of the original relation is also a step of the new relation.
However, the second rule adds a new kind of step: the global state may change \emph{arbitrarily}, so long as the new value satisfies invariant $I$.
We lift this operation to full transition systems, defining $\angled{S, S_0, \to}^I = \angled{S, S_0, \to^I}$.

This construction trivially acts as an abstraction.
\begin{theorem}\label{shared_invariant_abstract}
  \abstraction
  $\mathbb S \simulate_\mathsf{id} {\mathbb S}^I$, for any system $\mathbb S$ and property $I$.
\end{theorem}

\newcommand{\modularity}[0]{\marginpar{\fbox{\textbf{Modularity}}}}

However, we wouldn't want to make this abstraction step in a proof about a single thread.
We needlessly complicate our model checking by forcing ourselves to consider all modifications of the global state that obey $I$.
The payoff comes in analyzing multithreaded systems.
\begin{theorem}\label{shared_invariant_modular}
  \modularity
  Where $I$ is an invariant over only the shared state of a multithreaded system, let $I' = \{(g, \ell) \mid I(g)\}$ be the lifting of $I$ to cover full states, local parts included.  If $I'$ is an invariant for both ${\mathbb S}_1^I$ and ${\mathbb S}_2^I$, then $I'$ is also an invariant for $({\mathbb S}_1 \mid {\mathbb S}_2)^I$.
\end{theorem}

This theorem gives us a way to analyze the threads in a system separately.
As an example, consider this program, where multiple threads will run \texttt{f()} simultaneously.
\begin{verbatim}
int global = 0;

f() {
  int local = 0;

  while (true) {
    local = global;
    local = 3 + local;
    local = 7 + local;
    global = local;
  }
}
\end{verbatim}

Call the transition-system encoding of this code $\mathbb S$.
We can apply the Boolean-for-evenness abstraction to model a single thread with finite state, but we are left needing to account for interference by other threads.
However, we can apply Theorem \ref{shared_invariant_modular} to analyze threads separately.

For instance, we want to show that ``\texttt{global} is always even'' is an invariant of ${\mathbb S} \mid {\mathbb S}$.
By Theorem \ref{shared_invariant_abstract}, we can switch to analyzing system $({\mathbb S} \mid {\mathbb S})^I$, where $I$ is the evenness invariant.
By Theorem \ref{shared_invariant_modular}, we can switch to proving the same invariant separately for systems ${\mathbb S}^I$ and ${\mathbb S}^I$, which are, of course, the same system in this case.
We apply the Boolean-for-evenness abstraction to this system, to get one with a finite state space, so we can check the invariant automatically by model checking.
Following the chain of reasoning backward, we have proved the invariant for ${\mathbb S} \mid {\mathbb S}$.

Even better, that last proof includes the hardest steps that carry over to the proof for an arbitrary number of threads.
Define an exponentially growing system of threads ${\mathbb S}^n$ by:
\begin{eqnarray*}
  {\mathbb S}^0 &=& \mathbb S \\
  {\mathbb S}^{n+1} &=& {\mathbb S}^n \mid {\mathbb S}^n
\end{eqnarray*}

\begin{theorem}
  For any $n$, it is an invariant of ${\mathbb S}^n$ that the global variable is always even.
\end{theorem}

\begin{proof}
  By induction on $n$, repeatedly using Theorem \ref{shared_invariant_modular} to push the obligation down to the leaves of the tree of concurrent compositions, after applying Theorem \ref{shared_invariant_abstract} at the start to introduce the use of $\ldots^I$.
  Every leaf is the same system $\mathbb S$, for which we abstract and apply model checking, appealing to the step above where we ran the same analysis.
\end{proof}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Operational Semantics}

It gets tedious to define a relation from first principles, to explain the behaviors of any concrete program.
We do more things with programs than just reason about them.
For instance, we compile them into other languages.
To get the most mileage out of our correctness proofs, we should connect them to the same program syntax that we pass to compilers.
\emph{Operational semantics}\index{operational semantics} is a family of techniques for automatically defining a transition system, or other relational characterization, from program syntax.

\newcommand{\assign}[2]{#1 \leftarrow #2}
\newcommand{\skipe}[0]{\mathsf{skip}}
\newcommand{\ifte}[3]{\mathsf{if} \; #1 \; \mathsf{then} \; #2 \; \mathsf{else} \; #3}
\newcommand{\while}[2]{\mathsf{while} \; #1 \; \mathsf{do} \; #2}

Throughout this chapter, we will demonstrate the different operational-semantics techniques on a single source language, defined like so.
$$\begin{array}{rrcl}
  \textrm{Numbers} & n &\in& \mathbb N \\
  \textrm{Variables} & x &\in& \mathsf{Strings} \\
  \textrm{Expressions} & e &::=& n \mid x \mid e + e \mid e - e \mid e \times e \\
  \textrm{Commands} & c &::=& \skipe \mid \assign{x}{e} \mid c; c \mid \ifte{e}{c}{c} \mid \while{e}{c}
\end{array}$$


\section{Big-Step Semantics}

\newcommand{\bigstep}[2]{#1 \Downarrow #2}

\emph{Big-step operational semantics}\index{big-step operational semantics} explains what it means to run a program to completion.
For our example language, we define a relation written $\bigstep{(v, c)}{v'}$, for ``command $c$, run with variable valuation $v$, terminates, modifying the valuation to $v'$.''

This relation is fairly straightforward to define with inference rules.
\encoding
$$\infer{\bigstep{(v, \skipe)}{v}}{}
\quad \infer{\bigstep{(v, \assign{x}{e})}{\mupd{v}{x}{\denote{e}v}}}{}
\quad \infer{\bigstep{(v, c_1; c_2)}{v_2}}{
  \bigstep{(v, c_1)}{v_1}
  & \bigstep{(v_1, c_2)}{v_2}
}$$
$$\infer{\bigstep{(v, \ifte{e}{c_1}{c_2})}{v'}}{
  \denote{e}{v} \neq 0
  & \bigstep{(v, c_1)}{v'}
}
\quad \infer{\bigstep{(v, \ifte{e}{c_1}{c_2})}{v'}}{
  \denote{e}{v} = 0
  & \bigstep{(v, c_2)}{v'}
}$$
$$\infer{\bigstep{(v, \while{e}{c_1})}{v_2}}{
  \denote{e}{v} \neq 0
  & \bigstep{(v, c_1)}{v_1}
  & \bigstep{(v_1, \while{e}{c_1})}{v_2}
}
\quad \infer{\bigstep{(v, \while{e}{c_1})}{v}}{
  \denote{e}{v} = 0
}$$

Notice how the definition is quite similar to a recursive interpreter\index{interpreters} written in a high-level programming language, though we write with the language of relations instead of functional programming.
For instance, consider the simple case of the rule for sequencing, ``;''.
We first ``call the interpreter'' on the first subcommand $c_1$ with the original valuation $v$.
The result of the ``recursive call'' is a new valuation $v_1$, which we then feed into another ``recursive call'' on $c_2$, whose result becomes the overall result.

Why write this interpreter relationally instead of as a functional program?
The most relevant answer applies to situations like ours as users of Coq or even of informal mathematics, where we must be very careful that all of our recursive definitions are well-founded.
The recursive version of this relation is clearly not well-founded, as it would run forever on a nonterminating $\mathsf{while}$ loop.
It is also easier to incorporate \emph{nondeterminism}\index{nondeterminism} in the relational style, a possibility that we will return to at the end of the chapter.

The big-step semantics is easy to apply to concrete programs.
For instance, define $\mathtt{factorial}$ as the program $\assign{\mathtt{output}}{1}; \while{\mathtt{input}}{(\assign{\mathtt{output}}{\mathtt{output} \times \mathtt{input}}; \assign{\mathtt{input}}{\mathtt{input} - 1})}$.

\begin{theorem}
  There exists $v$ such that $\bigstep{(\mupd{\mempty}{\mathtt{input}}{2}, \mathtt{factorial})}{v}$ and $\msel{v}{\mathtt{output}} = 2$.
\end{theorem}

\begin{proof}
  By repeated application of the big-step inference rules.
\end{proof}

We can even prove that $\mathtt{factorial}$ behaves correctly on all inputs, by way of a lemma about $\mathtt{factorial\_loop}$ defined as $\while{\mathtt{input}}{(\assign{\mathtt{output}}{\mathtt{output} \times \mathtt{input}}; \assign{\mathtt{input}}{\mathtt{input} - 1})}$.

\begin{lemma}\label{factorial_loop}
  If $\msel{v}{\mathtt{input}} = n$ and $\msel{v}{\mathtt{output}} = o$, then there exists $v'$ such that $\bigstep{(v, \mathtt{factorial\_loop})}{v'}$ and $\msel{v'}{\mathtt{output}} = n! \times o$.
\end{lemma}

\begin{proof}
  By induction on $n$.
\end{proof}

\begin{lemma}
  If $\msel{v}{\mathtt{input}} = n$, then there exists $v'$ such that $\bigstep{(v, \mathtt{factorial})}{v'}$ and $\msel{v'}{\mathtt{output}} = n!$.
\end{lemma}

\begin{proof}
  Largely by direct appeal to Lemma \ref{factorial_loop}.
\end{proof}

Most of our program proofs in this book establish \emph{safety properties}\index{safety properties}, or invariants of transition systems.
However, these last two examples with big-step semantics also establish program termination, taking us a few steps into the world of \emph{liveness properties}\index{liveness properties}.


\section{Small-Step Semantics}

Often it is convenient to break a system's execution into small sequential steps, rather than executing a whole program in one go.
Perhaps the most compelling example comes from concurrency, where it is difficult to give a big-step semantics directly.
Nonterminating programs are the other standard example.
We want to be able to establish invariants for those programs, all the same, and we need a semantics to help us state what it means to be an invariant.

\newcommand{\smallstep}[2]{#1 \to #2}

The canonical solution is \emph{small-step operational semantics}\index{small-step operational semantics}, probably the most common approach to formal program semantics in contemporary research.
Now we define a single-step relation $\smallstep{(v, c)}{(v', c')}$, meaning that one execution step transforms the first state into the second state.
Each state is a valuation $v$ and a current command $c$.

These inference rules give the details.
\encoding
$$\infer{\smallstep{(v, \assign{x}{e})}{(\mupd{v}{x}{\denote{e}v}, \skipe)}}{}
\quad \infer{\smallstep{(v, c_1; c_2)}{(v', c'_1; c_2)}}{
    \smallstep{(v, c_1)}{(v', c'_1)}
}
\quad \infer{\smallstep{(v, \skipe; c_2)}{(v, c_2)}}{}$$
$$\infer{\smallstep{(v, \ifte{e}{c_1}{c_2})}{(v, c_1)}}{
  \denote{e}v \neq 0
}
\quad \infer{\smallstep{(v, \ifte{e}{c_1}{c_2})}{(v, c_2)}}{
  \denote{e}v = 0
}$$
$$\infer{\smallstep{(v, \while{e}{c_1})}{(v, c_1; \while{e}{c_1})}}{
  \denote{e}v \neq 0
}
\quad \infer{\smallstep{(v, \while{e}{c_1})}{(v, \skipe)}}{
  \denote{e}v = 0
}$$

The intuition behind the rules may come best from working out an example.

\newcommand{\smallsteps}[2]{#1 \to^* #2}

\begin{theorem}
  There exists valuation $v$ such that $\smallsteps{(\mupd{\mempty}{\mathtt{input}}{2}, \mathtt{factorial})}{(v, \skipe)}$ and $\msel{v}{\mathtt{output}} = 2$.
\end{theorem}

\begin{proof}
  Here is a step-by-step (literally!) derivation that finds $v$.
  $$\begin{array}{cl}
    & (\mupd{\mempty}{\mathtt{input}}{2}, \assign{\mathtt{output}}{1}; \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{1}, \skipe; \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{1}, \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{1}, (\assign{\mathtt{output}}{\mathtt{output} \times \mathtt{input}}; \assign{\mathtt{input}}{\mathtt{input} - 1}); \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{2}, (\skipe; \assign{\mathtt{input}}{\mathtt{input} - 1}); \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{2}, \assign{\mathtt{input}}{\mathtt{input} - 1}; \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{1}}{\mathtt{output}}{2}, \skipe; \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{1}}{\mathtt{output}}{2}, \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{1}}{\mathtt{output}}{2}, (\assign{\mathtt{output}}{\mathtt{output} \times \mathtt{input}}; \assign{\mathtt{input}}{\mathtt{input} - 1}); \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{1}}{\mathtt{output}}{2}, (\skipe; \assign{\mathtt{input}}{\mathtt{input} - 1}); \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{1}}{\mathtt{output}}{2}, \assign{\mathtt{input}}{\mathtt{input} - 1}; \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{0}}{\mathtt{output}}{2}, \skipe; \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{0}}{\mathtt{output}}{2}, \mathtt{factorial\_loop}) \\
    \to & (\mupd{\mupd{\mempty}{\mathtt{input}}{0}}{\mathtt{output}}{2}, \skipe)
  \end{array}$$

  Clearly the final valuation assigns $\mathtt{output}$ to 2.
\end{proof}

\subsection{Equivalence of Big-Step and Small-Step}

Different theorems are easier to prove with different semantics, so it is helpful to establish formally the intuitive connection between big and small steps.

\begin{lemma}
  If $\smallsteps{(v, c_1)}{(v', c'_1)}$, then $\smallsteps{(v, c_1; c_2)}{(v', c'_1; c_2)}$,
\end{lemma}

\begin{proof}
  By induction on the derivation of $\smallsteps{(v, c_1)}{(v', c'_1)}$.
\end{proof}

\begin{theorem}
  If $\bigstep{(v, c)}{v'}$, then $\smallsteps{(v, c)}{(v', \skipe)}$.
\end{theorem}

\begin{proof}
  By induction on the derivation of $\bigstep{(v, c)}{v'}$, appealing to the last lemma at two points.
\end{proof}

\begin{lemma}
  If $\smallstep{(v, c)}{(v', c')}$ and $\bigstep{(v', c')}{v''}$, then $\bigstep{(v, c)}{v''}$.  In other words, we can add a small step to the beginning of any big-step derivation.
\end{lemma}

\begin{proof}
  By induction on the derivation of $\smallstep{(v, c)}{(v', c')}$.
\end{proof}

\begin{lemma}
  If $\smallsteps{(v, c)}{(v', c')}$ and $\bigstep{(v', c')}{v''}$, then $\bigstep{(v, c)}{v''}$.  In other words, we can add any number of small steps to the beginning of any big-step derivation.
\end{lemma}

\begin{proof}
  By induction on the derivation of $\smallsteps{(v, c)}{(v', c')}$, appealing to the last lemma.
\end{proof}

\begin{theorem}
  If $\smallsteps{(v, c)}{(v', \skipe)}$, then $\bigstep{(v, c)}{v'}$.
\end{theorem}

\begin{proof}
  Largely by appeal to the last lemma, considering that $\bigstep{(v', \skipe)}{v'}$.
\end{proof}

\subsection{Transition Systems from Small-Step Semantics}

The small-step semantics is a natural fit with our working definition of transition systems.
We can define a transition system from any valuation and command, where $\mathbb V$ is the set of valuations and $\mathbb C$ the set of commands, by $\mathbb T(v, c) = \angled{\mathbb V \times \mathbb C, \{(v, c)\}, \to}$.
Now we bring to bear all of our machinery about invariants and their proof methods.

For instance, consider program $P = \while{\mathtt{n}}{\assign{\mathtt{a}}{\mathtt{a} + \mathtt{n}}; \assign{\mathtt{n}}{\mathtt{n} - 2}}$.

\invariants
\begin{theorem}
  Given even $n$, for $\mathbb T(\mupd{\mupd{\mempty}{\mathtt{n}}{n}}{\mathtt{a}}{0}, P)$, it is an invariant that the valuation maps variable $\mathtt{a}$ to an even number.
\end{theorem}

\begin{proof}
  First, we strengthen the invariant.
  We compute the set $\overline{P}$ of all commands that can be reached from $P$ by stepping the small-step semantics.
  This set is finite, even though the set of \emph{reachable valuations} is infinite, considering all potential $n$ values.
  Our strengthened invariant is $I(v, c) = c \in \overline{P} \land (\exists n. \; \msel{v}{\mathtt{n}} = n \land \textrm{even}(n)) \land (\exists a. \; \msel{v}{\mathtt{a}} = a \land \textrm{even}(a))$.
  In other words, we strengthen by adding the constraints that (1) we do not stray from the expected set of reachable commands and (2) variable \texttt{n} also remains even.

  The strengthened invariant is straightforward to prove by invariant induction, using repeated inversion on $\to$ facts.
\end{proof}


\section{Contextual Small-Step Semantics}

The reader may have noticed some tedium in certain rules of the small-step semantics, like this one.
$$\infer{\smallstep{(v, c_1; c_2)}{(v', c'_1; c_2)}}{
    \smallstep{(v, c_1)}{(v', c'_1)}
}$$
This rule is an example of a \emph{congruence rule}\index{congruence rule}, which shows how to take a step and \emph{lift} it into a step within a larger command, whose other subcommands are unaffected.
Complex languages can require many congruence rules, and yet we feel like we should be able to avoid repeating all this boilerplate logic somehow.
A common way to do so is switching to \emph{contextual small-step semantics}\index{contextual small-step semantics}.

We illustrate with our running example language.
The first step is to define a set of \emph{evaluation contexts}\index{evaluation contexts}, which formalize the spots within a larger command where steps are enabled.
\encoding
$$\begin{array}{rrcl}
  \textrm{Evaluation contexts} & C &::=& \Box \mid C; c
\end{array}$$

\newcommand{\plug}[2]{#1[#2]}
We define the operator of \emph{plugging}\index{plugging evaluation contexts} an evaluation context in the natural way.
\begin{eqnarray*}
  \plug{\Box}{c} &=& c \\
  \plug{(C; c_2)}{c} &=& \plug{C}{c}; c_2
\end{eqnarray*}

For this language, the only interesting case of evaluation contexts is the one that allows us to \emph{descend into the left subcommand}, because the old congruence rule invoked the step relation recursively for that position.

\newcommand{\smallstepo}[2]{#1 \to_0 #2}

The next ingredient is a reduced set of basic step rules, where we have dropped the congruence rule.
$$\infer{\smallstepo{(v, \assign{x}{e})}{(\mupd{v}{x}{\denote{e}v}, \skipe)}}{}
\quad \infer{\smallstepo{(v, \skipe; c_2)}{(v, c_2)}}{}$$
$$\infer{\smallstepo{(v, \ifte{e}{c_1}{c_2})}{(v, c_1)}}{
  \denote{e}v \neq 0
}
\quad \infer{\smallstepo{(v, \ifte{e}{c_1}{c_2})}{(v, c_2)}}{
  \denote{e}v = 0
}$$
$$\infer{\smallstepo{(v, \while{e}{c_1})}{(v, c_1; \while{e}{c_1})}}{
  \denote{e}v \neq 0
}
\quad \infer{\smallstepo{(v, \while{e}{c_1})}{(v, \skipe)}}{
  \denote{e}v = 0
}$$

\newcommand{\smallstepc}[2]{#1 \to_\mathsf{c} #2}

We regain the full coverage of the original rules with a new relation $\to_\mathsf{c}$, saying that we may apply $\to_0$ at the active subcommand within a larger command.
$$\infer{\smallstepc{(v, C[c])}{(v', C[c'])}}{
  \smallstepo{(v, c)}{(v', c')}
}$$

Let's revisit last section's example, to see contextual semantics in action, especially to demonstrate how to express an arbitrary command as an evaluation context plugged with another command.

\newcommand{\smallstepcs}[2]{#1 \to^*_\mathsf{c} #2}

\begin{theorem}
  There exists valuation $v$ such that $\smallstepcs{(\mupd{\mempty}{\mathtt{input}}{2}, \mathtt{factorial})}{(v, \skipe)}$ and $\msel{v}{\mathtt{output}} = 2$.
\end{theorem}

\begin{proof}
  $$\begin{array}{cl}
    & (\mupd{\mempty}{\mathtt{input}}{2}, \assign{\mathtt{output}}{1}; \mathtt{factorial\_loop}) \\
    = & (\mupd{\mempty}{\mathtt{input}}{2}, \plug{(\Box; \mathtt{factorial\_loop})}{\assign{\mathtt{output}}{1}}) \\
    \to_\mathsf{c} & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{1}, \skipe; \mathtt{factorial\_loop}) \\
    = & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{1}, \plug{\Box}{\skipe; \mathtt{factorial\_loop}}) \\
    \to_\mathsf{c} & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{1}, \mathtt{factorial\_loop}) \\
    = & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{1}, \plug{\Box}{\mathtt{factorial\_loop}}) \\
    \to_\mathsf{c} & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{1}, (\assign{\mathtt{output}}{\mathtt{output} \times \mathtt{input}}; \assign{\mathtt{input}}{\mathtt{input} - 1}); \mathtt{factorial\_loop}) \\
    = & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{1}, \plug{((\Box; \assign{\mathtt{input}}{\mathtt{input} - 1}); \mathtt{factorial\_loop})}{\assign{\mathtt{output}}{\mathtt{output} \times \mathtt{input}}}) \\
    \to_\mathsf{c} & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{2}, (\skipe; \assign{\mathtt{input}}{\mathtt{input} - 1}); \mathtt{factorial\_loop}) \\
    = & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{2}, \plug{(\Box; \mathtt{factorial\_loop})}{\skipe; \assign{\mathtt{input}}{\mathtt{input} - 1})} \\
    \to_\mathsf{c} & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{2}, \assign{\mathtt{input}}{\mathtt{input} - 1}; \mathtt{factorial\_loop}) \\
    = & (\mupd{\mupd{\mempty}{\mathtt{input}}{2}}{\mathtt{output}}{2}, \plug{(\Box; \mathtt{factorial\_loop})}{\assign{\mathtt{input}}{\mathtt{input} - 1}}) \\
    \to_\mathsf{c} & (\mupd{\mupd{\mempty}{\mathtt{input}}{1}}{\mathtt{output}}{2}, \skipe; \mathtt{factorial\_loop}) \\
    = & (\mupd{\mupd{\mempty}{\mathtt{input}}{1}}{\mathtt{output}}{2}, \plug{\Box}{\skipe; \mathtt{factorial\_loop}}) \\
    \to^*_\mathsf{c} & \ldots \\
    \to_\mathsf{c} & (\mupd{\mupd{\mempty}{\mathtt{input}}{0}}{\mathtt{output}}{2}, \skipe)
  \end{array}$$

  Clearly the final valuation assigns $\mathtt{output}$ to 2.
\end{proof}

\subsection{Equivalence of Small-Step, With and Without Evaluation Contexts}

This new semantics formulation is equivalent to the other two, as we establish now.

\begin{theorem}
  If $\smallstep{(v, c)}{(v', c')}$, then $\smallstepc{(v, c)}{(v', c')}$.
\end{theorem}

\begin{proof}
  By induction on the derivation of $\smallstep{(v, c)}{(v', c')}$.
\end{proof}

\begin{lemma}
  If $\smallstepo{(v, c)}{(v', c')}$, then $\smallstep{(v, c)}{(v', c')}$.
\end{lemma}

\begin{proof}
  By cases on the derivation of $\smallstepo{(v, c)}{(v', c')}$.
\end{proof}

\begin{lemma}
  If $\smallstepo{(v, c)}{(v', c')}$, then $\smallstep{(v, C[c])}{(v', C[c'])}$.
\end{lemma}

\begin{proof}
  By induction on the structure of evaluation context $C$, appealing to the last lemma.
\end{proof}

\begin{theorem}
  If $\smallstepc{(v, c)}{(v', c')}$, then $\smallstep{(v, c)}{(v', c')}$.
\end{theorem}

\begin{proof}
  By inversion on the derivation of $\smallstepc{(v, c)}{(v', c')}$, followed by an appeal to the last lemma.
\end{proof}

\subsection{Evaluation Contexts Pay Off: Adding Concurrency}

To showcase the convenience of contextual semantics, let's extend our example language with a simple construct for running two commands in parallel\index{parallel composition of threads}, implicitly extending the definition of plugging accordingly.
$$\begin{array}{rrcl}
  \textrm{Commands} & c &::=& \ldots \mid c || c
\end{array}$$

To capture that idea that \emph{either} command in a parallel construct is allowed to step next, we extend evaluation contexts like so:
\encoding
$$\begin{array}{rrcl}
  \textrm{Evaluation contexts} & C &::=& \ldots \mid C || c \mid c || C
\end{array}$$

We need one more basic step rule, to ``garbage-collect'' threads that have finished.
$$\infer{\smallstepo{(v, \skipe || c)}{(v, c)}}{}$$

And that's it!
The new system faithfully captures our usual idea of threads executing in parallel.
All of the theorems proved previously about contextual steps continue to hold.
In fact, in the accompanying Coq code, literally the same proof scripts establish the new versions of the theorems, with no new human proof effort.
It's not often that concurrency comes for free in a rigorous proof!


\section{Determinism}

Our last extension with parallelism introduced intentional nondeterminism in the semantics: a single starting state can step to multiple different next states.
However, the three semantics for the original language are deterministic, and we can prove it.

\begin{theorem}
  If $\bigstep{(v, c)}{v_1}$ and $\bigstep{(v, c)}{v_2}$, then $v_1 = v_2$.
\end{theorem}

\begin{proof}
  By induction on the derivation of $\bigstep{(v, c)}{v_1}$ and inversion on the derivation of $\bigstep{(v, c)}{v_2}$.
\end{proof}

\begin{theorem}
  If $\smallstep{(v, c)}{(v_1, c_1)}$ and $\smallstep{(v, c)}{(v_2, c_2)}$, then $v_1 = v_2$ and $c_1 = c_2$.
\end{theorem}

\begin{proof}
  By induction on the derivation of $\smallstep{(v, c)}{(v_1, c_1)}$ and inversion on the derivation of $\smallstep{(v, c)}{(v_2, c_2)}$.
\end{proof}

\begin{theorem}
  If $\smallstepc{(v, c)}{(v_1, c_1)}$ and $\smallstepc{(v, c)}{(v_2, c_2)}$, then $v_1 = v_2$ and $c_1 = c_2$.
\end{theorem}

\begin{proof}
  Follows from the last theorem and the equivalence we proved between $\to$ and $\to_\mathsf{c}$.
\end{proof}

We'll stop, for now, in our tour of useful properties of operational semantics.
All of the rest of the book is based on small-step semantics, with or without evaluation contexts.
As we study new kinds of programming languages, we will see how to model them operationally.
Almost every new proof technique is phrased as an approach to establishing invariants of transition systems based on small-step semantics.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\appendix

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{The Coq Proof Assistant}

Coq\index{Coq} is a proof-assistant software package developed as open source, primarily by Inria\index{Inria}, the French national computer-science lab.

\section{Installation and Basic Use}

The project home page is:
\begin{center}
  \url{https://coq.inria.fr/}
\end{center}
The code associated with this book is designed to work with Coq versions 8.4 and higher.
The project Web site makes a number of versions available, and versions are also available in popular OS package distributions, along with binaries for platforms where open-source package systems are less common.
We assume that readers have installed Coq by one of those means or another.
It will also be almost essential to use some graphical interface for Coq editing.
The author prefers Proof General\index{Proof General}, an Emacs\index{Emacs} mode:
\begin{center}
  \url{http://proofgeneral.inf.ed.ac.uk/}
\end{center}
It should be possible to follow along using CoqIDE\index{CoqIDE}, a standalone tool distributed with Coq itself, but we will not give any CoqIDE-specific instructions.

The Proof General instructions are simple: after installing, within a regular Emacs session, open a file with the Coq extension \texttt{.v}.
Move the point (cursor) to a position where you would like to examine the current state of a proof, etc.
Then press C-C C-RET (``control-C, control-enter'') to run Coq up to that point.
Several display panes will open, showing different aspects of Coq's state, any error messages it wants to report, etc.
This feature is the main workhorse of Proof General.
It can be used both to move \emph{forward}, checking that Coq accepts a command; and to move \emph{backward}, to undo commands processed previously.

Proof General has plenty of other bells and whistles, but we won't go into them here.

\section{Tactic Reference}

\emph{Tactics} are the commands run in Coq to advance the state of a proof, corresponding to deduction steps at different granularities.
Here we collect all of the short explanations of tactics that appear in Coq source files associated with the chapters included in this document.
Note that many of these are specific to the \texttt{Frap} library distributed with this book, where built-in tactics often do quite similar things, but in a way that the author judges to be more of a hassle for beginners.

\begin{description}
  \item[\texttt{apply} $H$] For $H$ a hypothesis or previously proved theorem, establishing some fact that matches the structure of the current conclusion, switch to proving $H$'s own hypotheses.  This is \emph{backwards reasoning} via a known fact.
  \item[\texttt{apply} $H$ \texttt{with} \texttt{(}$x_1$\texttt{ := }$e_1$\texttt{) ... (}$x_n$\texttt{ := }$e_n$\texttt{)}] Like the last one, supplying values for quantified variables in $H$'s statement, especially for those variables whose values aren't immediately implied by the current goal.
  \item[\texttt{apply} $H_1$ \texttt{in} $H_2$] Like \texttt{apply} $H_1$, but used in a \emph{forward} direction rather than \emph{backward}.  For instance, if $H_1$ proves $P \Rightarrow Q$ and $H_2$ proves $P$, then the effect is to change $H_2$ to $Q$.
  \item[\texttt{assert} $P$] First prove proposition $P$, then continue with it as a new hypothesis.
  \item[\texttt{assumption}] Prove a conclusion that matches a hypothesis exactly.
  \item[\texttt{cases} $e$] Break the proof into one case for each constructor that might have been used to build the value of expression $e$.  In the special case where $e$ essentially has a Boolean type, we consider whether $e$ is true or false.
  \item[\texttt{constructor}] When proving an instance of an inductive predicate, \texttt{apply} the first matching rule of that predicate.
  \item[\texttt{eapply} $H$] Like \texttt{apply} but will work even when some quantified variables from $H$ do not have their values determined immediately by the form of the goal.  Instead, \emph{existential variables} (with names starting with question marks) are introduced for those values.
  \item[\texttt{eassumption}] Like \texttt{assumption} but will figure out values of existential variables.
  \item[\texttt{econstructor}] When proving an instance of an inductive predicate, \texttt{eapply} the first matching rule of that predicate.
  \item[\texttt{eexists}] To prove $\exists x. \; P(x)$, switch to proving $P(?y)$, for a new existential variable $?y$.
  \item[\texttt{equality}] A complete decision procedure for the theory of equality and uninterpreted functions.  That is, the goal must follow from only reflexivity, symmetry, transitivity, and congruence of equality, including that functions really do behave as functions.  See Section \ref{decidable}.
  \item[\texttt{exfalso}] From any proof state, switch to proving \texttt{False}.  In other words, indicate a switch to a proof by contradiction.
  \item[\texttt{exists} $e$] Prove $\exists x. \; P(x)$ by proving $P(e)$.
  \item[\texttt{first\_order}] Simplify a goal into zero or more new goals, based on the rules of first-order logic alone.  \emph{Warning:} this tactic is especially likely to run forever, on complex enough goals!  (While entailment for propositional logic is decidable, entailment for first-order logic isn't.)
  \item[\texttt{f\_equal}] When the goal is an equality between two applications of the same function, switch to proving that the function arguments are pairwise equal.
  \item[\texttt{induct} $x$] Where $x$ is a variable in the theorem statement, structure the proof by induction on the structure of $x$.  You will get one generated subgoal per constructor in the inductive definition of $x$.  (Indeed, it is required that $x$'s type was introduced with \texttt{Inductive}.)
  \item[\texttt{invert} $H$] Replace hypothesis $H$ with other facts that can be deduced from the structure of $H$'s statement.  More detail to be added here soon!
  \item[\texttt{linear\_arithmetic}] A complete decision procedure for linear arithmetic.  Relevant formulas are essentially those built up from variables and constant natural numbers and integers using only addition and subtraction, with equality and inequality comparisons on top.  (Multiplication by constants is supported, as a shorthand for repeated addition.) See Section \ref{decidable}.
  \item[\texttt{left}] Prove a disjunction by proving its left side.
  \item[\texttt{maps\_equal}] Prove that two finite maps are equal by considering all the relevant cases for mappings of different keys.
  \item[\texttt{propositional}] Simplify a goal into zero or more new goals, based on the rules of propositional logic alone.
  \item[\texttt{replace} $e_1$ \texttt{with} $e_2$ \texttt{by} \texttt{tac}] Replace occurrences of $e_1$ with $e_2$, proving $e_2 = e_1$ with tactic \texttt{tac}.
  \item[\texttt{rewrite} $H$] Where $H$ is a hypothesis or previously proved theorem, establishing \texttt{forall x1 .. xN, e1 = e2}, find a subterm of the goal that equals \texttt{e1}, given the right choices of \texttt{xi} values, and replace that subterm with \texttt{e2}.
  \item[\texttt{rewrite} $H_1$ \texttt{in} $H_2$] Like \texttt{rewrite} $H_1$ but performs the rewrite in hypothesis $H_2$ instead of in the conclusion.
  \item[\texttt{right}] Prove a disjunction by proving its right side.
  \item[\texttt{ring}] Prove goals that are equalities over some registered ring or semiring, in the sense of algebra, where the goal follows solely from the axioms of that algebraic structure.  See Section \ref{decidable}.
  \item[\texttt{simplify}] Simplify throughout the goal, applying the definitions of recursive functions directly.  That is, when a subterm matches one of the \texttt{match} cases in a defining \texttt{Fixpoint}, replace with the body of that case, then repeat.
  \item[\texttt{subst}] Remove all hypotheses like $x = e$ for variables $x$, simply replacing all uses of $x$ by $e$.
  \item[\texttt{symmetry}] When proving $X = Y$, switch to proving $Y = X$.
  \item[\texttt{transitivity} $X$] When proving $Y = Z$, switch to proving $Y = X$ and $X = Z$.
  \item[\texttt{trivial}] Coq maintains a database of simple proof steps, such as proving a fact by direct appeal to a matching hypothesis.  \texttt{trivial} asks to try all such simple steps.
  \item[\texttt{unfold} $X$] Replace $X$ by its definition.
  \item[\texttt{unfold} $X$ \texttt{in} \texttt{*}] Like the last one, but unfolds in hypotheses as well as conclusion.
\end{description}

\section{Proof-Automation Basics}

Coming soon!

\section{Further Reading}

For more Coq information, we recommend a few books (beyond the Coq reference manual).  Some focus purely on introducing Coq:

\begin{itemize}
  \item Adam Chlipala, \emph{Certified Programming with Dependent Types}, MIT Press, \url{http://adam.chlipala.net/cpdt/}
  \item Yves Bertot and Pierre Cast\'eran, \emph{Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions}, Springer, \url{https://www.labri.fr/perso/casteran/CoqArt/}
\end{itemize}

The first of these two, especially, goes in-depth on the automated proof-scripting principles showcased from time to time in the Coq example code associated with the present book.

There are also other sources that introduce program-reasoning principles at the same time, including:

\begin{itemize}
  \item Benjamin C. Pierce et al., \emph{Software Foundations}, \url{http://www.cis.upenn.edu/~bcpierce/sf/}
\end{itemize}

\emph{Software Foundations} generally proceeds at a slower pace than this book does.

\backmatter
%    Bibliography styles amsplain or harvard are also acceptable.
%% \bibliographystyle{amsalpha}
%% \bibliography{}
%    See note above about multiple indexes.
\printindex

\end{document}