Interesting example of internal padding

[Jose E. Marchesi]

Implementing the PE/COFF pickle is fun.  I just made use of internal
padding to implement this excerpt of the spec:

  "The virtual address value from the Certificate Table entry in the
   Optional Header Data Directory is a file offset to the first
   attribute certificate entry. Subsequent entries are accessed by
   advancing that entry's dwLength bytes, rounded up to an 8-byte
   multiple, from the start of the current attribute certificate
   entry. This continues until the sum of the rounded dwLength values
   equals the Size value from the Certificates Table entry in the
   Optional Header Data Directory. If the sum of the rounded dwLength
   values does not equal the Size value, then either the attribute
   certificate table or the Size field is corrupted."

Each attribute certificate looks like this:

  type PE_Attribute_Certificate =
    struct
    {
      offset<uint<32>,B> length;
      uint<16> revision;
      uint<16> cert_type;

      /* Note: we use internal padding here so we can map arrays of
         attribute certificates by total size.  */
      byte[0] certificate_begin;
      byte[0] certificate_end @ length + alignto (length, 8#B);
    };

Note how I am avoiding mapping the contents of the certificate itself,
as I think these things can be big (convenience zero sized fields
certificate_begin and certificate_end can then be used to poke at them
if that's what the user wants.)

Anyhow, the table of certificates, if present, is at the end of the PE
file.  Checking the data integrity described in the spec paragraph above
can be implemented very naturally by mapping the table as an array of
variable-length values with internal padding (the
PE_Attribute_Certificate struct above) itself size-bounded by total
size:

type PE_File =
  struct
  {
    [...]
    var certs_datadir = opt_hdr.data_directories.certificate_table;

    PE_Attribute_Certificate[certs_datadir.size] certificates
      @ certs_datadir.rva
      if certs_datadir.size > 0#B;
  };

poke will thus detect file corruption as expected in the spec by raising
an exception if it cannot fill an exact number of variable-length
certificates in exactly certs_datadir.size bytes.