Specify that an index contains the number of entries

[jeltsch]

At the moment, the number of entries of a run is stored with the index. We shall specify this explicitly in format-run.md. In fact, we shall say more concretely that there must be a footer and that the number of entries must be stored within this footer.

Alternatively, we may choose to store the number of entries elsewhere, as it actually isn’t directly related to the index.