Wiki Agenda Contact English version

The BitWalker, SPARK version

This program was originally a case study in C from Siemens rewritten by the Fraunhofer FOKUS research group for applying the Frama-C formal verification tool to it. It was later on rewritten in SPARK and formally proved correct with GNATprove (with 100% of checks automatically proved). This work is described in the article Specification and Proof of High-Level Functional Properties of Bit-Level Programs published at NFM 2016 conference.

This program introduces a function and procedure that read and respectively write a word of bits of a given length from a stream of bytes at a given position. It heavily uses bitwise arithmetic and is fully specified with contracts and automatically proved by GNATprove. In addition, two test procedures call read-then-write and write-then-read and GNATprove is able to prove the expected properties on the interplay between reading and writing.

In this program we use an external axiomatization in order to lift some operators from the underlying Why3 theory of bitvectors to SPARK. In particular the Nth function, at the core of the specification of the program, lets us check if a specific bit in a modular value is set or not. Note that while such a function could be easily implemented in SPARK, using the one defined in the Why3 theory leads to more automatic proofs because it lets the provers use the associated axioms and lemmas.


Auteurs: Clément Fumex / Claire Dross / Claude Marché

Catégories: Bitwise operations

Outils: SPARK 2014

Références: ProofInUse joint laboratory

see also the index (by topic, by tool, by reference, by year)


download ZIP archive
The full code is in the ZIP archive above. Here are below the specifications. The proofs can be replayed using SPARK Community 2018 and invoking the test.cmd script from the archive. bitwalker.ads

File : bitwalker.ads


with Interfaces; use Interfaces;
with BitTypes;   use BitTypes;
with BitSpec;    use BitSpec;
with Bvext;      use Bvext;

package Bitwalker with
SPARK_Mode
is
   function PeekBit8 (Byte : Unsigned_8; Left : Natural) return Boolean
   with
     Pre  => Left < 8,
     Post => PeekBit8'Result = Nth (Byte, 7 - Left);

   function PeekBit8Array (Addr : Byte_Sequence; Left : Natural) return Boolean is
     (PeekBit8 (Addr (Left / 8), Left rem 8))
   with
     Pre    => Addr'First = 0 and then
               Left < 8 * Addr'Length,
     Global => null,
     Post   => PeekBit8Array'Result = Nth8_Stream (Addr, Left);

   function PokeBit64
      (Value : Unsigned_64;
       Left  : Natural;
       Flag  : Boolean) return Unsigned_64
   with
     Pre    => Left < 64,
     Global => null,
     Post   => (for all I in Natural range 0 .. 63 =>
                  (if I /= 63 - Left then
                         Nth (PokeBit64'Result, I) = Nth (Value, I)))
               and
                 (Flag = Nth (PokeBit64'Result, 63 - Left));

   function Peek
     (Start, Length : Natural;
      Addr          : Byte_Sequence) return Unsigned_64
     with
       Pre            => Addr'First = 0 and then
                         Length <= 64 and then
                         Start + Length <= Natural'Last and then
                         8 * Addr'Length <= Natural'Last,
       Global         => null,
       Contract_Cases =>
         (Start + Length > 8 * Addr'Length =>
            Peek'Result = 0,
         (Start + Length <= 8 * Addr'Length) =>
           (for all I in 0 .. Length - 1 =>
                    Nth8_Stream (Addr, Start + Length - I - 1)
                  = Nth (Peek'Result, I))
          and then
           (for all I in Length .. 63 => not Nth (Peek'Result, I)));

   function PeekBit64 (Value : Unsigned_64;
                       Left  : Natural)
                       return Boolean
   is
     ((Value and Shift_Left (1, 63 - Left)) /= 0)
   with
       Pre  => Left < 64,
       Post => PeekBit64'Result = Nth (Value, (63 - Left));

   function PokeBit8 (Byte : Unsigned_8;
                      Left : Natural;
                      Flag : Boolean)
                      return Unsigned_8
     with
       Pre  => Left < 8,
       Post =>
         (for all I in 0 .. 7 =>
            (if I /= 7 - Left then
              Nth (PokeBit8'Result, I) = Nth (Byte, I))) and then
         Nth (PokeBit8'Result, 7 - Left) = Flag;

   procedure PokeBit8Array (Addr : in out Byte_Sequence;
                            Left : Natural;
                            Flag : Boolean)
     with
       Pre  => Addr'First = 0 and then Left < 8 * Addr'Length,
       Post =>
         (for all I in 0 .. 8 * Addr'Length - 1 =>
            (if I /= Left then
                     Nth8_Stream (Addr, I) = Nth8_Stream (Addr'Old, I)))
          and then
            Nth8_Stream (Addr, Left) = Flag;

   procedure Poke (Start, Len : Natural;
                   Addr       : in out Byte_Sequence;
                   Value      : Unsigned_64;
                   Result     : out Integer)
     with
       Pre  => Addr'First = 0 and then
               8 * Addr'Length <= Natural'Last and then
               Start + Len < Natural'Last and then
               Len in 0 .. 63,
       Post => (Result in -2 .. 0) and then
               ((Result = -1) = (Start + Len > 8 * Addr'Length)) and then
               ((Result = -2) = (MaxValue (Len) <= Value
                                 and Start + Len <= 8 * Addr'Length))
             and then
               ((Result = 0) = (MaxValue (Len) > Value
                                and Start + Len <= 8 * Addr'Length))
             and then
               (if Result = 0 then
                  (for all I in 0 .. Start - 1 =>
                         Nth8_Stream (Addr'Old, I) = Nth8_Stream (Addr, I)))
             and then
               (if Result = 0 then
                  (for all I in Start .. Start + Len - 1 =>
                         Nth8_Stream (Addr, I)
                   = Nth (Value, Len - I - 1 + Start )))
             and then
               (if Result = 0 then
                  (for all I in Start + Len .. 8 * Addr'Length - 1=>
                         Nth8_Stream (Addr, I)
                   = Nth8_Stream (Addr'Old ,I)));

   function LemmaFunction (X : Unsigned_64; Len : Integer) return Unit
     with
       Ghost,
       Pre  => Len in 0 .. 63 and then
               (for all I in Len .. 63 => not Nth (X, I)),
       Post => LemmaFunction'Result = Void and then
               X < MaxValue (Len);

   function LemmaFunction2 (X : Unsigned_64; Len : Integer) return Unit
     with
       Ghost,
       Pre  => Len in 0 .. 63 and then X < MaxValue (Len),
       Post => LemmaFunction2'Result = Void and then
               (for all I in Len .. 63 => not Nth (X, I));

   procedure PeekThenPoke (Start, Len : Natural;
                           Addr       : in out Byte_Sequence;
                           Result     : out Integer)
     with
       Ghost,
       Pre =>
         Addr'First = 0 and then
         8 * Addr'Length <= Natural'Last and then
         Len in 0 .. 63 and then
         Start + Len <= 8 * Addr'Length,
       Post =>
           Result = 0 and then
           (for all I in 0 .. 8 * Addr'Length - 1 =>
              Nth8_Stream (Addr, I) = Nth8_Stream (Addr'Old, I));

   procedure PokeThenPeek (Start, Len : Natural;
                           Addr : in out Byte_Sequence;
                           Value : Unsigned_64;
                           Result : out Unsigned_64)
     with
       Ghost,
       Pre =>
         Addr'First = 0 and then
         8 * Addr'Length < Natural'Last and then
         Len in 0 .. 63 and then
         Start + Len <= Addr'Length and then
         Value < MaxValue (Len),
       Post =>
          Result = Value;

end Bitwalker;