MiniPNG spec

[jklmnn]

https://paperstreet.picty.org/POS/ (section "TP noté").

[jklmnn]

The MiniPNG format consists of a magic string and 3 different block types:

• Header
  • Exactly once
  • Contains image width and height, pixel format
• Data
  • Zero or more
  • Contains image data depending on pixel format
• Comment
  • Zero or more
  • Contains comments

The current specification uses an inlined header block at the beginning and then an array of a block type that can contain either data or comment blocks. This restricts the parser to files that have the header block at the beginning.

Furthermore the image data is specified as Opaque and needs to be interpreted separately depending on the pixel type. Furthermore it is not checked if there's enough image data for the given image size and color depth.

Both problems could be solved by having invariants over arrays. There could be an invariant each for:

• There must be exactly one header block in the array
• The sum of the Image data bytes must be sufficient to fill the image size (e.g. an 8x8x24 image must contain at least 1536 bits of image data).

[senier]

For the magic string you should use the new string comparison:

   type File is
      message
         null
            then Magic
               with Length => 64;
         Magic        : Opaque
            then Tag
               if Magic = "Mini-PNG";
         Tag          : Header_Type;
         Length       : Header_Length;
         Image_Width  : Image_Size;
         Image_Height : Image_Size;
         Pixel        : Pixel_Type
            then Blocks 
            with Length => Message'Last - Pixel'Last;
         Blocks       : CD_Blocks;
   end message;

[senier]

The spec is even worse that I expected ;) I have no good idea how we'd specify that the sum of bytes in all data blocks of the array equals width x height x depth. This is related to #78, but I don't have the faintest idea how to express that.

@treiher What do you think? (Here is the spec: https://translate.google.de/translate?sl=fr&tl=en&u=https%3A%2F%2Fpaperstreet.picty.org%2FPOS%2Fminipng%2Fminipng.pdf)

[treiher]

It is different to #78 in that it is not just an invariant over an array. We would need (1) to extract the size of the image from the header block, (2) determine the actual length of the data stored in data blocks from an array and (3) compare the results.

Just an idea how that could be specified:

(1) That is mostly straightforward, except that a method for determining the depth based on the pixel type is needed. An interpretation of an type is needed, maybe defined by an aspect:

   type Pixel_Type is (Black_White => 0, Greyscale => 1, Palette => 2, Truecolor => 3) with
      Size => 8,
      Value => (if Pixel_Type = Black_White then 1 elsif [...] elsif Pixel_Type = Truecolor then 24);

(2) Based on a Sum function and a list comprehension we could define the value of an array:

   type CD_Blocks is array of CD_Block with
      Value => Sum (for B in CD_Block => (if B.Tag = Data then B.Length else 0));

(3) Comparing the results is straightforward again:

         ...
         Image_Width  : Image_Size;
         Image_Height : Image_Size;
         Pixel        : Pixel_Type
            then Blocks
               with Length => Message'Last - Pixel'Last;
         Blocks       : CD_Blocks
            then null
               if Blocks'Value = Image_Width * Image_Height * Pixel'Value
   end message;

That is just a rough idea how this could be specified. It is unclear how good such a specification would be for generating verifiable code based on it.

[senier]

I like the idea, especially as we want the Value construct for other reasons (e.g. #8). I created #237 to track this feature eventually.

Generally, I think the spec should be more generic:

   type Block is
      message
         Tag : Block_Type;
         Length : Block_Length
            then Image_Width
               if Tag = Data,
            then Content
               with Length => Length * 8
                  if Tag = Header or Tag = Comment;
         Width : Image_Size;
         Height : Image_Size;
         Pixel : Pixel_Type
            then null;
         Content : Opaque;
      end message;

   type Blocks is array of Block;

   type File is
      message
         null
            then Magic
               with Length => 64;
         Magic : Opaque
            then Blocks
               with Length => Message'Last - Magic'Last
                  if Magic = "Mini-PNG";
         Blocks : Blocks;
      end message;

This is a valid spec, but we lose the property that the header is at the start of the message. However, the spec does not state that anyway (to my understanding):

a header block H (header);
zero, one or more comment blocks C (comment);
one or more data blocks D (data).

(and I don't think that "un bloc d'en-tête H" states anything about its position either). Of cause, that ambiguity is deliberate in a security class to make students (fail to) think about such problems.

The current spec also lacks the other two properties. I think this should all be part of a condition on Blocks:

   Blocks : Block
      if Header'Length = 1
         and [for B in Block => B when B.Tag = Data]'Length > 0
         and Blocks'Value = Header.Width * Header.Height * Header.Pixel'Value
            where Header = [for B in Block => B when B.Tag = Header]'Head

I agree that its unclear how to ensure a verifiable parser from this spec.

[senier]

@jklmnn Have you noticed this in the spec: "The pixels are arranged from top to bottom, then from left to right." I guess that means you'll have to store all the data chunks before being able to print them. Evil! We will want to make sure (i.e. show) that we're bounded stack here.

[jklmnn]

This is a valid spec, but we lose the property that the header is at the start of the message.

This is also the spec I had in mind initially. The goal of my current version was not to have the header at the beginning (which isn't specified) but to have exactly one header (which is specified).

un bloc d'en-tête

This literally translates to "head(er) block". So except from the expectation that a header should be at the beginning I cannot see from the spec that the header is required to be at the start.

Have you noticed this in the spec: "The pixels are arranged from top to bottom, then from left to right." I guess that means you'll have to store all the data chunks before being able to print them. Evil! We will want to make sure (i.e. show) that we're bounded stack here.

I do not see any difference here from them being stored left to right first top to bottom second except that the image is built up column wise except line wise. Since already know the size and format of the image I can't see the problem here.

Another problem is that the header is not necessarily at the beginning of the file so we have to load the whole file (or at least until we find the header) to start processing it. This isn't a problem now since RecordFlux is parsing the whole image anyway.

[senier]

I do not see any difference here from them being stored left to right first top to bottom second except that the image is built up column wise except line wise. Since already know the size and format of the image I can't see the problem here.

With left-to-right you could just go through the data block incrementally and output a pixel as soon as you have enough data. This way you either need to jump between the blocks or cache the data in the right format.

[jklmnn]

But this depends on your output format. If you have a framebuffer (or even a double buffered graphics output) this shouldn't be a problem.

[jklmnn]

To properly support specifying pixels in Data blocks a fragmentation concept is required. Furthermore the payload of these blocks behaves like a inner protocol that is specified by the Pixel field. This is similar to fragmented IP.