Wiki Agenda Contact Version française

Bitwalker

The Bitwalker case study is about interacting with a stream of bytes: copying from the byte stream to a 64-bit unsigned integer, and conversely. This case study is detailed in Specification and proof of high-level functional properties of bit-level programs.


Authors: Claude Marché / Clément Fumex

Topics: Bitwise operations

Tools: Why3

References: ProofInUse joint laboratory

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


module Bitwalker
  use import int.Int
  use import int.EuclideanDivision
  use import array.Array
  use import ref.Ref
  (* use bv.BV32 *)
  (* use bv.BV8 *)
  (* use bv.BV64 *)
  use mach.bv.BVCheck8  as BV8
  use mach.bv.BVCheck32 as BV32
  use mach.bv.BVCheck64 as BV64
  use bv.BVConverter_32_64 as C32_64
  use bv.BVConverter_8_32 as C8_32

(* file missing in repository
  use import mach.bv.BV
*)

  function nth8_stream (stream : array BV8.t) (pos : int) : bool =
    BV8.nth stream[div pos 8] (7 - mod pos 8)

  lemma nth64:
    forall value:BV64.t, i:int. 0 <= i < 64 ->
      BV64.nth value i = BV64.nth_bv value (C32_64.toBig (BV32.of_int i))

  lemma nth8:
    forall value:BV8.t, i:int. 0 <= i < 8 ->
      BV8.nth value i = BV8.nth_bv value (C8_32.toSmall (BV32.of_int i))

  (*  *)
  function maxvalue (len : BV32.t) : BV64.t = BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig len)

  let lemma nth_ultpre0 (x:BV64.t) (len:BV32.t)
    requires { BV32.t'int len < 64}
    ensures { BV64.eq_sub x BV64.zeros (BV32.t'int len) (64 - BV32.t'int len)
          <-> BV64.t'int x < BV64.t'int (maxvalue len) }
  =
    assert { BV32.ult len (BV32.of_int 64) };
    assert { BV64.eq_sub_bv x BV64.zeros (C32_64.toBig len) (BV64.sub (BV64.of_int 64) (C32_64.toBig len))
         <-> BV64.ult x (maxvalue len) }

return value with the bit of index left from the left set to flag

  let poke_64bit_bv (value : BV64.t) (left : BV32.t) (flag : bool) : BV64.t
    requires { BV32.t'int left < 64 }
    ensures  { forall i. 0 <= i < 64 /\ i <> 63 - BV32.t'int left ->
                 BV64.nth result i = BV64.nth value i }
    ensures  { flag = BV64.nth result (63 - BV32.t'int left) }
  =
    assert { BV32.ult left (BV32.of_int 64) };
    abstract
    ensures { forall i:BV32.t. i <> BV32.sub (BV32.of_int 63) left ->
               BV64.nth_bv result (C32_64.toBig i) =
                 BV64.nth_bv value (C32_64.toBig i) }
    ensures { flag = BV64.nth_bv result
                       (C32_64.toBig (BV32.sub (BV32.of_int 63) left)) }
      let mask =
        BV64.lsl_bv (BV64.int_check 1)
          (C32_64.toBig (BV32.sub_check (BV32.int_check 63) left))
      in
      match flag with
      | True -> BV64.bw_or value mask
      | False -> BV64.bw_and value (BV64.bw_not mask)
      end
    end

return value with the bit of index left from the left set to flag

(* version where [left] is an int and not a bitvector, which
  is closer to the result of the SPARK translation from signed
  integers *)
  let poke_64bit (value : BV64.t) (left : int) (flag : bool) : BV64.t
    requires { 0 <= left < 64 }
    ensures  { forall i. 0 <= i < 64 /\ i <> 63 - left ->
                 BV64.nth result i = BV64.nth value i }
    ensures  { flag = BV64.nth result (63 - left) }
  =
    let ghost left_bv = BV64.of_int left in
    assert { BV64.ult left_bv (BV64.of_int 64) };
    assert { (BV64.sub (BV64.of_int 63) left_bv) = BV64.of_int (63 - left) };
    abstract
    ensures { forall i:BV64.t. BV64.ule i (BV64.of_int 63) ->
               i <> BV64.sub (BV64.of_int 63) left_bv ->
               BV64.nth_bv result i = BV64.nth_bv value i }
    ensures { flag = BV64.nth_bv result (BV64.sub (BV64.of_int 63) left_bv) }
      let mask =
        BV64.lsl_bv (BV64.int_check 1) (BV64.of_int (63 - left))
      in
      match flag with
      | True -> BV64.bw_or value mask
      | False -> BV64.bw_and value (BV64.bw_not mask)
      end
    end

  (* return the bit of [byte] at position [left] starting from the
  left *)

  let peek_8bit_bv (byte : BV8.t) (left : BV32.t) : bool
    requires { 0 <= BV32.t'int left < 8 }
    ensures  { result = BV8.nth byte (7 - BV32.t'int left) }
  =
    assert {BV32.ult left (BV32.of_int 8)};
    abstract
      ensures {
        result = BV8.nth_bv
                   byte (BV8.sub (BV8.of_int 7) (C8_32.toSmall left))}
    let mask =
      BV32.lsl_bv (BV32.int_check 1) (BV32.sub_check (BV32.int_check 7) left)
    in
    BV32.bw_and (C8_32.toBig byte) mask <> BV32.zeros
    end

  (* return the bit of the [left]/8 element of [addr] at position mod [left] 8 starting from the left *)
  let peek_8bit_array (addr : array BV8.t) (left : BV32.t) : bool
    requires { 8 * (length addr) < BV32.two_power_size }
    requires { BV32.t'int left < 8 * length addr }
    ensures  { result = nth8_stream addr (BV32.t'int left) }
  =
    peek_8bit_bv (addr[ BV32.t'int (BV32.udiv_check left (BV32.int_check 8)) ]) (BV32.urem_check left (BV32.int_check 8))

  (* return a bitvector of 64 bits with its [len] bits of the right
    set to the bits between [start] and [start] + [len] of [addr] *)
  let peek (start : BV32.t) (len : BV32.t) (addr : array BV8.t) : BV64.t
    requires { BV32.t'int len <= 64 }
    requires { BV32.t'int start + BV32.t'int len < BV32.two_power_size }
    requires { 8 * length addr < BV32.two_power_size }
    ensures  { BV32.t'int start + BV32.t'int len > (8 * length addr) ->
      result = BV64.zeros }
    ensures  { BV32.t'int start + BV32.t'int len <= (8 * length addr) ->
      (forall i:int. 0 <= i < BV32.t'int len ->
         BV64.nth result i
         = nth8_stream addr (BV32.t'int start + BV32.t'int len - i - 1))
      /\
      (forall i:int. BV32.t'int len <= i < 64 -> BV64.nth result i = False) }
  =
    if (BV32.t'int (BV32.add_check start len) > ( 8 *length addr ))
    then
      BV64.zeros
    else

    let retval = ref BV64.zeros in
    let i = ref BV32.zeros in
    let lstart = BV32.sub_check (BV32.of_int 64) len in

    while BV32.ult !i len do variant{ !i with BV32.ugt }
    invariant {0 <= BV32.t'int !i <= BV32.t'int len}
    invariant {forall j:int. BV32.t'int len - BV32.t'int !i <= j < BV32.t'int len ->
                 BV64.nth !retval j
               = nth8_stream addr (BV32.t'int start + BV32.t'int len - j - 1)}
    invariant {forall j:int. 0 <= j < BV32.t'int len - BV32.t'int !i ->
                 BV64.nth !retval j
               = False}
    invariant {forall j:int. BV32.t'int len <= j < 64 ->
                 BV64.nth !retval j
               = False}

      let flag = peek_8bit_array addr (BV32.add_check start !i) in
      retval := poke_64bit_bv !retval (BV32.add_check lstart !i) flag;

      i := BV32.add_check !i (BV32.int_check 1);

    done;

    !retval

  let peek_64bit (value : BV64.t) (left : BV32.t) : bool
    requires {BV32.t'int left < 64}
    ensures {result = BV64.nth value (63 - BV32.t'int left)}
  =
     assert {BV32.ult left (BV32.of_int 64)};
     abstract
     ensures {result = BV64.nth_bv value
                       (BV64.sub (BV64.of_int 63) (C32_64.toBig left))}
       let mask = BV64.lsl_bv (BV64.int_check 1)
                  (C32_64.toBig (BV32.sub_check (BV32.int_check 63) left)) in
       BV64.bw_and value mask <> BV64.zeros
     end

(*
  static inline uint8_t PokeBit8(uint8_t byte, uint32_t left, int flag)
  {
    uint8_t mask = ((uint8_t) 1) << (7u - left);

    return (flag == 0) ? (byte & ~mask) : (byte | mask);
  }
*)

  (* return [byte] with the bit at index [left] from the left set to [flag] *)
  let poke_8bit (byte : BV8.t) (left : BV32.t) (flag : bool) : BV8.t
    requires { BV32.t'int left < 8 }
    ensures  { forall i:int. 0 <= i < 8 -> i <> 7 - BV32.t'int left ->
               BV8.nth result i = BV8.nth byte i }
    ensures  { BV8.nth result (7 - BV32.t'int left) = flag }
  =
    assert { BV32.ult left (BV32.of_int 8) };
    abstract
    ensures { forall i:BV32.t. BV32.ult i (BV32.of_int 8) ->
               i <> BV32.sub (BV32.of_int 7) left ->
               BV8.nth_bv result (C8_32.toSmall i)
             = BV8.nth_bv byte (C8_32.toSmall i) }
    ensures { BV8.nth_bv result (BV8.sub (BV8.of_int 7) (C8_32.toSmall left))
            = flag }
      let mask = BV8.lsl_bv (BV8.int_check 1) (BV8.sub_check (BV8.int_check 7) (C8_32.toSmall left)) in
      match flag with
      | True -> BV8.bw_or byte mask
      | False -> BV8.bw_and byte (BV8.bw_not mask)
      end
    end

  let poke_8bit_array (addr : array BV8.t) (left : BV32.t) (flag : bool)
    writes {addr}
    requires { 8 * (length addr) < BV32.two_power_size }
    requires { BV32.t'int left < 8 * length addr }
    ensures  { forall i:int. 0 <= i < 8 * length addr -> i <> BV32.t'int left ->
               nth8_stream addr i = nth8_stream (old addr) i}
    ensures  { nth8_stream addr (BV32.t'int left) = flag }
  =
    let i = BV32.udiv_check left (BV32.int_check 8) in
    let k = BV32.urem_check left (BV32.int_check 8) in
    addr[BV32.t'int i] <- poke_8bit addr[BV32.t'int i] k flag

  let poke (start : BV32.t) (len : BV32.t) (addr : array BV8.t) (value : BV64.t)
    writes  { addr }
    requires{ BV32.t'int len < 64 } (* could be lower or equal if maxvalue and the condition to return -2 is corrected *)
    requires{ BV32.t'int start + BV32.t'int len < BV32.two_power_size }
    requires{ 8 * length addr < BV32.two_power_size }
    ensures { -2 <= result <= 0 }
    ensures { result = -1 <-> BV32.t'int start + BV32.t'int len > 8 * length addr }
    ensures { result = -2 <-> BV64.t'int (maxvalue len) <= BV64.t'int value /\ BV32.t'int start + BV32.t'int len <= 8 * length addr }
    ensures { result =  0 <-> BV64.t'int (maxvalue len) > BV64.t'int value /\ BV32.t'int start + BV32.t'int len <= 8 * length addr }
    ensures { result =  0 ->
              (forall i:int. 0 <= i < BV32.t'int start ->
                nth8_stream (old addr) i
              = nth8_stream addr i)
           /\
              (forall i:int. BV32.t'int start <= i < BV32.t'int start + BV32.t'int len ->
                nth8_stream addr i
              = BV64.nth value (BV32.t'int len - i - 1 + BV32.t'int start))
           /\
              (forall i:int. BV32.t'int start + BV32.t'int len <= i < 8 * length addr ->
                nth8_stream addr i
              = nth8_stream (old addr) i) }
  =
    if BV32.t'int (BV32.add_check start len) > 8 * length addr
    then
      -1                        (*error: invalid_bit_sequence*)
    else

    if BV64.uge value (maxvalue len) (* should be len <> 64 && _..._ *)
    then
      -2                        (*error: value_too_big*)
    else

    let lstart = BV32.sub_check (BV32.of_int 64) len in
    let i = ref BV32.zeros in

    'Init:
    while BV32.ult !i len do variant { !i with BV32.ugt }
    invariant {0 <= BV32.t'int !i <= BV32.t'int len}
    invariant {forall j:int. 0 <= j < BV32.t'int start ->
                 nth8_stream (at addr 'Init) j
               = nth8_stream addr j}
    invariant {forall j:int. BV32.t'int start <= j < BV32.t'int start + BV32.t'int !i ->
                 nth8_stream addr j
               = BV64.nth value (BV32.t'int len - j - 1 + BV32.t'int start) }
    invariant {forall j:int. BV32.t'int start + BV32.t'int !i <= j < 8 * length addr ->
                 nth8_stream addr j
               = nth8_stream (at addr 'Init) j }

      let flag = peek_64bit value (BV32.add_check lstart !i) in

      poke_8bit_array addr (BV32.add_check start !i) flag;

      assert {nth8_stream addr (BV32.t'int start + BV32.t'int !i)
            = BV64.nth value ((BV32.t'int len - BV32.t'int !i - 1))};
      assert { forall k. BV32.t'int start <= k < BV32.t'int start + BV32.t'int !i ->
               k <> BV32.t'int start + BV32.t'int !i &&
               0 <= k < 8 * length addr &&
                   nth8_stream addr k
                 = BV64.nth value (BV32.t'int start + BV32.t'int len - k - 1)};

      i := BV32.add_check !i (BV32.int_check 1);
    done;

    0

  let peekthenpoke (start len : BV32.t) (addr : array BV8.t)
    requires {8 * length addr < BV32.two_power_size}
    requires {0 <= BV32.t'int len < 64}
    requires {BV32.t'int start + BV32.t'int len <= 8 * length addr}
    ensures {result = 0}
    ensures {forall i. 0 <= i < 8 * length addr ->
               nth8_stream addr i = nth8_stream (old addr) i}
  =
    'Init:
    let value = peek start len addr in
    let res = poke start len addr value in

    assert {res = 0};

    assert {forall i. BV32.t'int start <= i < BV32.t'int start + BV32.t'int len ->
         nth8_stream addr i
       = nth8_stream (at addr 'Init) i};

    res

  let pokethenpeek (start len : BV32.t) (addr : array BV8.t) (value : BV64.t)
    writes   {addr}
    requires {8 * length addr < BV32.two_power_size}
    requires {0 <= BV32.t'int len < 64}
    requires {BV32.t'int start + BV32.t'int len <= 8 * length addr}
    requires {BV64.t'int value < BV64.t'int (maxvalue len)}
    ensures  {result = value}
  =
    assert { forall i:int. BV32.t'int len <= i < 64 -> BV64.nth value i = False };
    let poke_result = poke start len addr value in
    assert {poke_result = 0};
    let peek_result = peek start len addr in

    assert {BV64.eq peek_result value};

    peek_result

end

download ZIP archive

Why3 Proof Results for Project "bitwalker"

Theory "bitwalker.Bitwalker": fully verified in 0.40 s

ObligationsAlt-Ergo (0.99.1)Alt-Ergo (1.00.prv)Alt-Ergo (1.01)Alt-Ergo (1.10.prv)CVC3 (2.4.1)CVC4 (1.4)CVC4 (1.4 noBV)Z3 (4.4.0)Z3 (4.4.1)Z3 (4.5.0 noBV)
nth640.10---------------------------
nth80.30---------------------------
3. VC for nth_ultpre0------------------------------
split_goal_wp
  1. assertion0.03---------------------------
2. assertion---------------0.16------------
3. postcondition4.38---------------0.34---------
4. VC for poke_64bit_bv------------------------------
split_goal_wp
  1. assertion0.04---------------------------
2. precondition0.02------------0.01------------
3. precondition0.02------------0.02------------
4. precondition0.03------------0.01------------
5. VC for poke_64bit_bv---------------0.08------------
6. VC for poke_64bit_bv---------------0.08------------
7. VC for poke_64bit_bv---------------0.08------------
8. VC for poke_64bit_bv---------------0.06------------
9. postcondition0.61---------------0.40---------
10. postcondition0.52---------------0.41---------
5. VC for poke_64bit------------------------------
split_goal_wp
  1. assertion0.04---------------------------
2. assertion0.64---------------------------
3. precondition0.04---------------------------
4. VC for poke_64bit---------------0.31------------
5. VC for poke_64bit---------------0.18------------
6. VC for poke_64bit---------------0.32------------
7. VC for poke_64bit---------------0.07------------
8. postcondition0.77---------------------------
9. postcondition0.08---------------------------
6. VC for peek_8bit_bv------------------------------
split_goal_wp
  1. assertion0.03---------------------------
2. precondition0.05------------0.02------------
3. precondition0.06------------0.02------------
4. precondition0.06------------0.01------------
5. VC for peek_8bit_bv---------------0.09------------
6. postcondition1.22---------------------------
7. VC for peek_8bit_array------------------------------
split_goal_wp
  1. precondition0.02---------0.060.04------------
2. precondition0.06---------0.040.04------------
3. precondition0.03---------0.040.04------------
4. precondition0.05---------0.040.04------------
5. index in array bounds0.26---------0.05---------------
6. precondition0.35---------2.220.08------------
7. postcondition0.33---------------------------
8. VC for peek------------------------------
split_goal_wp
  1. precondition0.11---------0.13---0.07------0.12
2. postcondition0.03---------0.070.04------------
3. postcondition0.03---------0.090.10------------
4. precondition0.04---------0.04---------------
5. loop invariant init0.05---------0.09---------------
6. loop invariant init0.03---------0.04---------------
7. loop invariant init---------0.030.05---0.060.01------
8. loop invariant init0.03---------0.04---------------
9. precondition------------0.05---------------
10. precondition0.06---------0.090.18------------
11. precondition------------0.08---------------
12. precondition0.05---------0.06---------------
13. precondition------------2.14---0.09------0.12
14. precondition0.10---------0.120.06------------
15. precondition0.06---------0.03---------------
16. loop invariant preservation0.19---------0.12---------------
17. loop invariant preservation---3.08------------------------
18. loop invariant preservation---------------------0.01------
19. loop invariant preservation------------------0.330.02------
20. loop variant decrease0.14---------1.96---------------
21. postcondition0.05---------0.080.14------------
22. postcondition------------0.11---------------
9. VC for peek_64bit------------------------------
split_goal_wp
  1. assertion0.03---------0.04---------------
2. precondition0.02---------0.080.06------------
3. precondition0.05---------0.040.12------------
4. precondition0.02---------0.070.06------------
5. VC for peek_64bit---------------0.22------------
6. postcondition0.07---------------------------
10. VC for poke_8bit------------------------------
split_goal_wp
  1. assertion0.03---------0.04---------------
2. precondition0.02---------0.080.06------------
3. precondition0.10---------0.770.10------------
4. precondition0.02---------0.080.06------------
5. VC for poke_8bit---------------0.08------------
6. VC for poke_8bit---------------0.09------------
7. VC for poke_8bit---------------0.08------------
8. VC for poke_8bit---------------0.08------------
9. postcondition------------2.82---------------
10. postcondition------------0.78---------------
11. VC for poke_8bit_array------------------------------
split_goal_wp
  1. precondition0.03---------0.080.03---0.00------
2. precondition0.05---------0.040.04---0.00------
3. precondition0.02---------0.060.04---0.00------
4. precondition0.04---------0.040.03---0.00------
5. index in array bounds0.27---------0.05---------------
6. precondition0.34---------1.950.08---0.01------
7. index in array bounds0.03---------0.090.09---0.01------
8. postcondition---------------------0.01------
9. postcondition0.08------------------0.01------
12. VC for poke------------------------------
split_goal_wp
  1. precondition0.05---------0.15---0.08------0.12
2. postcondition0.03---------0.070.05------------
3. postcondition0.05---------0.080.12------------
4. postcondition0.04---------0.09---------------
5. postcondition0.04---------0.05---------------
6. postcondition0.03---------0.090.02------------
7. postcondition0.03---------0.090.06------------
8. postcondition0.05---------0.070.10------------
9. postcondition0.04---------0.09---0.07------0.12
10. postcondition0.06---------0.09---0.08------0.11
11. postcondition0.03---------0.100.06------------
12. precondition0.04---------0.04---------------
13. loop invariant init0.06---------0.09---------------
14. loop invariant init------------0.050.10------------
15. precondition------------0.07---------------
16. precondition------------2.01---0.09------0.13
17. precondition0.20---------0.05---------------
18. type invariant0.06---------0.100.16------------
19. precondition0.06---------0.090.16------------
20. precondition------------0.07---------------
21. assertion---0.82------0.06---------------
22. assertion------------------------------
split_goal_wp
  1. assertion0.05---------0.130.06------------
2. assertion------------0.06---------------
3. assertion0.13---------0.120.10------------
4. assertion------------------0.320.02------
23. precondition0.04---------0.050.02------------
24. precondition0.06---------0.04---------------
25. loop invariant preservation0.22---------0.06---------------
26. loop invariant preservation0.96---------------------------
27. loop invariant preservation2.43---------------------------
28. loop invariant preservation1.57---------------------------
29. loop variant decrease0.20---------2.01---------------
30. type invariant0.05---------0.080.08------------
31. postcondition0.03---------0.080.04------------
32. postcondition0.05---------0.100.07------------
33. postcondition0.03---------0.08---------------
34. postcondition0.04---------0.08---------------
35. postcondition------------------------------
split_goal_wp
  1. VC for poke0.27---------0.07---------------
2. VC for poke0.60---------------------------
3. VC for poke0.45---------------------------
13. VC for peekthenpoke------------------------------
split_goal_wp
  1. precondition0.03---------0.080.11------------
2. precondition0.02---------0.090.13------------
3. precondition0.02---------0.080.11------------
4. precondition0.02---------0.090.13------------
5. precondition0.02---------0.090.11------------
6. precondition0.02---------0.100.13------------
7. assertion---------------------0.00------
8. assertion------------0.99---------------
9. postcondition0.02---------0.040.07------------
10. postcondition0.48---------0.08---------------
14. VC for pokethenpeek------------------------------
split_goal_wp
  1. assertion---------------------0.01------
2. precondition0.02---------0.080.15------------
3. precondition0.03---------0.080.13------------
4. precondition0.02---------0.050.11------------
5. assertion0.02---------0.070.14------------
6. precondition0.02---------0.060.14------------
7. precondition0.02---------0.050.11------------
8. precondition0.03---------0.080.13------------
9. assertion------0.93---------------0.02---
10. postcondition0.18---------0.05---------------