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