The rounds of the evaluation, counted over the handed file

DescriptiveComplexity.Draw.Data.exists_valEnum builds the VAL loop's enumeration over the universe, where a space-bounded machine's registers are the elements themselves. A clocked machine counts the same rounds over the index of its file, so this file rebuilds the enumeration there: a chain of increments in the file's own order, from the empty address to the registers standing for inner elements.

Everything it needs is generic (DescriptiveComplexity.exists_wmChainOf, wmChainOf_lt) or a fact about the tags: the inner blocks are a final segment (DescriptiveComplexity.Draw.kinSeg), so above a register standing for an inner element every register does, and a marked address holds inner elements alone – which is what the semantic layer reads a round through.

How many elements there are, and how many the channel marks

The clock is met by comparing three numbers with 2 ^ (k · m), and two of them are sizes of the drawing: how many elements the universe has, and how many the channel writes for. Both are counted here, once, so that a reduction choosing k, j and m argues about its own tags and nothing else.