Definition endSection : list (string * binaryExp) := [
  ("ID",       U64 endSectionIdentifier);
  ("DataSize", U64 0)
].
