Definition binaryExpMetadataSection (m : metadata) : binaryExp := BiRecord [
  ("id",   u64 0x434C4E5F4D455441);
  ("size", u64 (binarySize (binaryExpMetadata m)));
  ("data", binaryExpMetadata m)
].
