Definition indexSection (data : indexArrayT) : list (string * binaryExp) :=
  let outData     := serializeIndex data   in
  let outDataSize := lengthN outData       in
  let sizeSum     := 16 + outDataSize      in
  let pad         := Pad (sizePad sizeSum) in
  [
    ("ID",       U64 indexSectionIdentifier);
    ("DataSize", U64 outDataSize);
    ("Data",     Octets outData);
    ("Padding",  pad)
  ].
