Definition binaryEndSection : binaryExp :=
  BiRecord [
    ("id",   u64 0x4D54505F454E4421);
    ("size", u64 0)
  ].
