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.
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;