Prove correctness of frame delimiter encoding. (#7)

This strengthens the postcondition of the Encode procedure
to prove that the encoder only outputs a frame delimiter (zero byte)
for the last byte, and that all preceding bytes have a non-zero value.

Author: damaki

README.md

@@ -67,8 +67,12 @@ end Example;
 This project takes a "hybrid verification" approach combining formal
 verification and testing.
 
-GNATprove is used to prove absence of run-time errors. At the time of writing
-there are 139 checks that are automatically proved.
+GNATprove is used to prove absence of run-time errors and some limited
+functional properties:
+ * the encoder only emits a frame delimiter (zero byte) at the end
+   of the encoded frame.
+
+At the time of writing there are 163 checks that are automatically proved.
 
 The unit tests are used to check that the encoder and decoder produce the
 correct results for a variety of inputs, with 100% MC/DC source coverage.

src/generic_cobs.adb

@@ -105,6 +105,11 @@ is
                          Output'First + Index'Base (Length - 1) =>
                 Output (I)'Initialized);
 
+         pragma Loop_Invariant
+           (for all I in Output'First ..
+                         Output'First + Index'Base (Length - 1) =>
+                Output (I) /= Frame_Delimiter);
+
          Encode_Block
            (Input  (Input'First  + Index'Base (Offset) .. Input'Last),
             Output (Output'First + Index'Base (Length) .. Output'Last),
@@ -117,6 +122,11 @@ is
          Remaining := Remaining - (Block_Length - 1);
       end loop;
 
+      pragma Assert
+        (for all I in Output'First ..
+                      Output'First + Index'Base (Length - 1) =>
+             Output (I) /= Frame_Delimiter);
+
       Output (Output'First + Index'Base (Length)) := Frame_Delimiter;
 
       Length := Length + 1;
@@ -148,7 +158,11 @@ is
 
       if Input'Length > 0 then
          for I in Byte_Count range 0 .. Input'Length - 1 loop
-            pragma Loop_Invariant (Code <= Maximum_Run_Length + 1);
+            pragma Warnings
+              (Off, """Output"" may be referenced before it has a value",
+               Reason => "Initialization of Output is guaranteed via proof");
+
+            pragma Loop_Invariant (Code in 1 .. Maximum_Run_Length + 1);
 
             pragma Loop_Invariant
               (Code = Length - Byte_Count (Code_Pos - Output'First));
@@ -166,6 +180,14 @@ is
                             Output'First + Index'Base (Length) - 1 =>
                    (if I /= Code_Pos then Output (I)'Initialized));
 
+            --  The frame delimiter is never written to the output.
+            pragma Loop_Invariant
+              (for all I in Output'First ..
+                            Output'First + Index'Base (Length) - 1 =>
+                   (if I /= Code_Pos then Output (I) /= Frame_Delimiter));
+
+            pragma Warnings (On);
+
             --  Stop when a complete block is reached.
             exit when Code = Maximum_Run_Length + 1;
 

src/generic_cobs.ads

@@ -117,7 +117,16 @@ is
               --  Only the first 'Length' bytes of the Output are initialized.
               and then
                 Output (Output'First ..
-                        Output'First + Index'Base (Length - 1))'Initialized),
+                        Output'First + Index'Base (Length - 1))'Initialized
+
+              --  The last byte in the output is a frame delimiter.
+              --  All other bytes before the frame delimiter are non-zero.
+              and then
+                (for all I in Output'First ..
+                              Output'First + Index'Base (Length - 1) =>
+                   (if I < Output'First + Index'Base (Length - 1)
+                    then Output (I) /= Frame_Delimiter
+                    else Output (I) = Frame_Delimiter))),
      Annotate => (GNATProve, Terminating);
    --  Encode a byte array.
    --
@@ -129,8 +138,7 @@ is
    --  @param Input The bytes to encode.
    --
    --  @param Output The COBS-encoded data is written to the first "Length"
-   --                bytes of this array. Any unused bytes at the end of the
-   --                array are initialised to the frame delimiter value (zero).
+   --                bytes of this array. The last byte is a frame delimiter.
    --
    --  @param Length The length of the encoded frame is written here.
 
@@ -201,7 +209,11 @@ private
                         then Length >= Maximum_Run_Length + 1)
               and then
                 Output (Output'First ..
-                        Output'First + Index'Base (Length - 1))'Initialized),
+                        Output'First + Index'Base (Length - 1))'Initialized
+              and then
+                (for all I in Output'First ..
+                              Output'First + Index'Base (Length - 1) =>
+                    Output (I) /= Frame_Delimiter)),
      Annotate => (GNATProve, Terminating);
    --  Encodes a single block of bytes.
    --