The encoding is deliberately dumb: it is exactly the input format, with nothing precomputed that an algorithm would otherwise have to compute. The word is required to have the right length, the offsets to be nondecreasing with the right two endpoints, and every target entry to be a vertex; beyond that the only condition is that each vertex's block lists exactly its neighbors. In particular the blocks are not required to be sorted and repetitions are not forbidden — the fewer conditions the encoding imposes, the more inputs a claim about programs reading it has to handle, so leaving them out strengthens every such claim rather than weakening it. For the same reason $m$ is only the declared length of the target array (which is $2m$): it is at least the number of edges, and equals it exactly when no block repeats a neighbor. Nothing forces each edge to be listed from both of its endpoints either — that is automatic, since adjacency in a simple graph is symmetric.

Cells are read with $List.getD$, which returns $0$ outside the word; the length condition pins down the word completely, so this default value is never reached at any position the other conditions constrain. The conditions are bundled as a structure so that each one is a named obligation a reader can check off separately.

Nothing here mentions the word length of the machine the encoding is handed to. It does not have to: every entry of an encoding is a vertex number, an offset into the target array, or one of the two header numbers, and each of those is smaller than the length of the word itself, so an encoding that a machine can address at all is one whose entries fit into that machine's words. The condition that it does fit belongs to the claims made about programs reading the encoding, and is stated there, once, as an explicit inequality against $2 ^ w$.