The overall statement requires that we identify pairs of Clight states that are
measurable - in the sense that we can identify a chunk of machine code that
the cost labels provide timing for.  A core part of this is that they must be
labelled states, so that we can spot the corresponding labels for the machine
code.

My first notion of a labelled Clight state was a syntactic version of
identifying states that will produce a cost label when stepped (actually, it
was even more wrong, but never mind).  However, this can't be right - a cost
label may appear deep in the statement (in particular, a subexpression of an
Econd) which corresponds to a point in the machine code rather later than we
intend.

Instead, we need the labelled states to be those which start with a cost label
(or better, consist entirely of processing the cost label).  This is easy at
the moment because they are just the states about to execute Scost, but if we
embed cost labels into other statements for (e.g.) solving our problem with
Swhile, then the natural solution becomes to avoid emitting the cost label
with the Swhile, but add in an Scost statement.  (Note that Sskip is already
added in this way.)