examples/bitwalker.mlw

   1 module Bitwalker
   2   use int.Int
   3   use int.EuclideanDivision
   4   use array.Array
   5   use ref.Ref
   6   (* use bv.BV32 *)
   7   (* use bv.BV8 *)
   8   (* use bv.BV64 *)
   9   use mach.bv.BVCheck8  as BV8
  10   use mach.bv.BVCheck32 as BV32
  11   use mach.bv.BVCheck64 as BV64
  12   use bv.BVConverter_32_64 as C32_64
  13   use bv.BVConverter_8_32 as C8_32
  14
  15 (* file missing in repository
  16   use mach.bv.BV
  17 *)
  18
  19   function nth8_stream (stream : array BV8.t) (pos : int) : bool =
  20     BV8.nth stream[div pos 8] (7 - mod pos 8)
  21
  22   lemma nth64:
  23     forall value:BV64.t, i:int. 0 <= i < 64 ->
  24       BV64.nth value i = BV64.nth_bv value (C32_64.toBig (BV32.of_int i))
  25
  26   lemma nth8:
  27     forall value:BV8.t, i:int. 0 <= i < 8 ->
  28       BV8.nth value i = BV8.nth_bv value (C8_32.toSmall (BV32.of_int i))
  29
  30   (*  *)
  31   let function maxvalue (len : BV32.t) : BV64.t =
  32     BV64.lsl_bv (1:BV64.t) (C32_64.toBig len)
  33
  34   let lemma nth_ultpre0 (x:BV64.t) (len:BV32.t)
  35     requires { BV32.t'int len < 64}
  36     ensures { BV64.eq_sub x BV64.zeros (BV32.t'int len) (64 - BV32.t'int len)
  37           <-> BV64.t'int x < BV64.t'int (maxvalue len) }
  38   =
  39     assert { BV32.ult len (64:BV32.t) };
  40     assert { BV64.eq_sub_bv x BV64.zeros (C32_64.toBig len) (BV64.sub (64:BV64.t) (C32_64.toBig len))
  41          <-> BV64.ult x (maxvalue len) }
  42
  43  (** return `value` with the bit of index `left` from the left set to `flag` *)
  44   let poke_64bit_bv (value : BV64.t) (left : BV32.t) (flag : bool) : BV64.t
  45     requires { BV32.t'int left < 64 }
  46     ensures  { forall i. 0 <= i < 64 /\ i <> 63 - BV32.t'int left ->
  47                  BV64.nth result i = BV64.nth value i }
  48     ensures  { flag = BV64.nth result (63 - BV32.t'int left) }
  49   =
  50     assert { BV32.ult left (64:BV32.t) };
  51     begin
  52     ensures { forall i:BV32.t. i <> BV32.sub (63:BV32.t) left ->
  53                BV64.nth_bv result (C32_64.toBig i) =
  54                  BV64.nth_bv value (C32_64.toBig i) }
  55     ensures { flag = BV64.nth_bv result
  56                        (C32_64.toBig (BV32.sub (63:BV32.t) left)) }
  57       let mask =
  58         BV64.lsl_bv (1:BV64.t)
  59           (C32_64.toBig (BV32.u_sub (63:BV32.t) left))
  60       in
  61       match flag with
  62       | True -> BV64.bw_or value mask
  63       | False -> BV64.bw_and value (BV64.bw_not mask)
  64       end
  65     end
  66
  67  (** return `value` with the bit of index `left` from the left set to `flag` *)
  68 (* version where `left` is an int and not a bitvector, which
  69   is closer to the result of the SPARK translation from signed
  70   integers *)
  71   let poke_64bit (value : BV64.t) (left : int) (flag : bool) : BV64.t
  72     requires { 0 <= left < 64 }
  73     ensures  { forall i. 0 <= i < 64 /\ i <> 63 - left ->
  74                  BV64.nth result i = BV64.nth value i }
  75     ensures  { flag = BV64.nth result (63 - left) }
  76   =
  77     let ghost left_bv = BV64.of_int left in
  78     assert { BV64.ult left_bv (64:BV64.t) };
  79     assert { (BV64.sub (63:BV64.t) left_bv) = BV64.of_int (63 - left) };
  80     begin
  81     ensures { forall i:BV64.t. BV64.ule i (63:BV64.t) ->
  82                i <> BV64.sub (63:BV64.t) left_bv ->
  83                BV64.nth_bv result i = BV64.nth_bv value i }
  84     ensures { flag = BV64.nth_bv result (BV64.sub (63:BV64.t) left_bv) }
  85       let mask =
  86         BV64.lsl_bv (1:BV64.t) (BV64.of_int (63 - left))
  87       in
  88       match flag with
  89       | True -> BV64.bw_or value mask
  90       | False -> BV64.bw_and value (BV64.bw_not mask)
  91       end
  92     end
  93
  94
  95   (* return the bit of `byte` at position `left` starting from the
  96   left *)
  97
  98   let peek_8bit_bv (byte : BV8.t) (left : BV32.t) : bool
  99     requires { 0 <= BV32.t'int left < 8 }
 100     ensures  { result = BV8.nth byte (7 - BV32.t'int left) }
 101   =
 102     assert {BV32.ult left (8:BV32.t)};
 103     begin
 104       ensures {
 105         result = BV8.nth_bv
 106                    byte (BV8.sub (7:BV8.t) (C8_32.toSmall left))}
 107     let mask =
 108       BV32.lsl_bv (1:BV32.t) (BV32.u_sub (7:BV32.t) left)
 109     in
 110     not (BV32.eq (BV32.bw_and (C8_32.toBig byte) mask) 0x0)
 111     end
 112
 113   (* return the bit of the `left`/8 element of `addr` at position mod `left` 8 starting from the left *)
 114   let peek_8bit_array (addr : array BV8.t) (left : BV32.t) : bool
 115     requires { 8 * (length addr) < BV32.two_power_size }
 116     requires { BV32.t'int left < 8 * length addr }
 117     ensures  { result = nth8_stream addr (BV32.t'int left) }
 118   =
 119     peek_8bit_bv (addr[ BV32.to_uint (BV32.u_div left (8:BV32.t)) ]) (BV32.u_rem left (8:BV32.t))
 120
 121   (* return a bitvector of 64 bits with its `len` bits of the right
 122     set to the bits between `start` and `start+len` of `addr` *)
 123   let peek (start : BV32.t) (len : BV32.t) (addr : array BV8.t) : BV64.t
 124     requires { BV32.t'int len <= 64 }
 125     requires { BV32.t'int start + BV32.t'int len < BV32.two_power_size }
 126     requires { 8 * length addr < BV32.two_power_size }
 127     ensures  { BV32.t'int start + BV32.t'int len > (8 * length addr) ->
 128       result = BV64.zeros }
 129     ensures  { BV32.t'int start + BV32.t'int len <= (8 * length addr) ->
 130       (forall i:int. 0 <= i < BV32.t'int len ->
 131          BV64.nth result i
 132          = nth8_stream addr (BV32.t'int start + BV32.t'int len - i - 1))
 133       /\
 134       (forall i:int. BV32.t'int len <= i < 64 -> BV64.nth result i = False) }
 135   =
 136     if (BV32.to_uint (BV32.u_add start len) > ( 8 *length addr ))
 137     then
 138       0x0
 139     else
 140
 141     let retval = ref 0x0 in
 142     let i = ref 0x0 in
 143     let lstart = BV32.u_sub (64:BV32.t) len in
 144
 145     while BV32.ult !i len do variant{ BV32.t'int len - BV32.t'int !i }
 146     invariant {0 <= BV32.t'int !i <= BV32.t'int len}
 147     invariant {forall j:int. BV32.t'int len - BV32.t'int !i <= j < BV32.t'int len ->
 148                  BV64.nth !retval j
 149                = nth8_stream addr (BV32.t'int start + BV32.t'int len - j - 1)}
 150     invariant {forall j:int. 0 <= j < BV32.t'int len - BV32.t'int !i ->
 151                  BV64.nth !retval j
 152                = False}
 153     invariant {forall j:int. BV32.t'int len <= j < 64 ->
 154                  BV64.nth !retval j
 155                = False}
 156
 157       let flag = peek_8bit_array addr (BV32.u_add start !i) in
 158       retval := poke_64bit_bv !retval (BV32.u_add lstart !i) flag;
 159
 160       i := BV32.u_add !i (1:BV32.t);
 161
 162     done;
 163
 164     !retval
 165
 166   let peek_64bit (value : BV64.t) (left : BV32.t) : bool
 167     requires {BV32.t'int left < 64}
 168     ensures {result = BV64.nth value (63 - BV32.t'int left)}
 169   =
 170      assert {BV32.ult left (64:BV32.t)};
 171      begin
 172      ensures {result = BV64.nth_bv value
 173                        (BV64.sub (63:BV64.t) (C32_64.toBig left))}
 174        let mask = BV64.lsl_bv (1:BV64.t)
 175                   (C32_64.toBig (BV32.u_sub (63:BV32.t) left)) in
 176        not (BV64.eq (BV64.bw_and value mask) 0x0)
 177      end
 178
 179 (*
 180   static inline uint8_t PokeBit8(uint8_t byte, uint32_t left, int flag)
 181   {
 182     uint8_t mask = ((uint8_t) 1) << (7u - left);
 183
 184     return (flag == 0) ? (byte & ~mask) : (byte | mask);
 185   }
 186 *)
 187
 188   (* return `byte` with the bit at index `left` from the left set to `flag` *)
 189   let poke_8bit (byte : BV8.t) (left : BV32.t) (flag : bool) : BV8.t
 190     requires { BV32.t'int left < 8 }
 191     ensures  { forall i:int. 0 <= i < 8 -> i <> 7 - BV32.t'int left ->
 192                BV8.nth result i = BV8.nth byte i }
 193     ensures  { BV8.nth result (7 - BV32.t'int left) = flag }
 194   =
 195     assert { BV32.ult left (8:BV32.t) };
 196     begin
 197     ensures { forall i:BV32.t. BV32.ult i (8:BV32.t) ->
 198                i <> BV32.sub (7:BV32.t) left ->
 199                BV8.nth_bv result (C8_32.toSmall i)
 200              = BV8.nth_bv byte (C8_32.toSmall i) }
 201     ensures { BV8.nth_bv result (BV8.sub (7:BV8.t) (C8_32.toSmall left))
 202             = flag }
 203       let mask = BV8.lsl_bv (1:BV8.t) (BV8.u_sub (7:BV8.t) (C8_32.toSmall left)) in
 204       match flag with
 205       | True -> BV8.bw_or byte mask
 206       | False -> BV8.bw_and byte (BV8.bw_not mask)
 207       end
 208     end
 209
 210   let poke_8bit_array (addr : array BV8.t) (left : BV32.t) (flag : bool)
 211     requires { 8 * (length addr) < BV32.two_power_size }
 212     requires { BV32.t'int left < 8 * length addr }
 213     writes   { addr }
 214     ensures  { forall i:int. 0 <= i < 8 * length addr -> i <> BV32.t'int left ->
 215                nth8_stream addr i = nth8_stream (old addr) i}
 216     ensures  { nth8_stream addr (BV32.t'int left) = flag }
 217   =
 218     let i = BV32.u_div left (8:BV32.t) in
 219     let k = BV32.u_rem left (8:BV32.t) in
 220     addr[BV32.to_uint i] <- poke_8bit addr[BV32.to_uint i] k flag
 221
 222   let poke (start : BV32.t) (len : BV32.t) (addr : array BV8.t) (value : BV64.t) : int
 223     writes  { addr }
 224     requires{ BV32.t'int len < 64 } (* could be lower or equal if maxvalue and the condition to return -2 is corrected *)
 225     requires{ BV32.t'int start + BV32.t'int len < BV32.two_power_size }
 226     requires{ 8 * length addr < BV32.two_power_size }
 227     ensures { -2 <= result <= 0 }
 228     ensures { result = -1 <-> BV32.t'int start + BV32.t'int len > 8 * length addr }
 229     ensures { result = -2 <-> BV64.t'int (maxvalue len) <= BV64.t'int value /\ BV32.t'int start + BV32.t'int len <= 8 * length addr }
 230     ensures { result =  0 <-> BV64.t'int (maxvalue len) > BV64.t'int value /\ BV32.t'int start + BV32.t'int len <= 8 * length addr }
 231     ensures { result =  0 ->
 232               (forall i:int. 0 <= i < BV32.t'int start ->
 233                 nth8_stream (old addr) i
 234               = nth8_stream addr i)
 235            /\
 236               (forall i:int. BV32.t'int start <= i < BV32.t'int start + BV32.t'int len ->
 237                 nth8_stream addr i
 238               = BV64.nth value (BV32.t'int len - i - 1 + BV32.t'int start))
 239            /\
 240               (forall i:int. BV32.t'int start + BV32.t'int len <= i < 8 * length addr ->
 241                 nth8_stream addr i
 242               = nth8_stream (old addr) i) }
 243   =
 244     if BV32.to_uint (BV32.u_add start len) > 8 * length addr
 245     then
 246       -1                        (*error: invalid_bit_sequence*)
 247     else
 248
 249     if BV64.uge value (maxvalue len) (* should be len <> 64 && _..._ *)
 250     then
 251       -2                        (*error: value_too_big*)
 252     else
 253
 254     let lstart = BV32.u_sub (64:BV32.t) len in
 255     let i = ref 0x0 in
 256
 257     while BV32.ult !i len do variant { BV32.t'int len - BV32.t'int !i }
 258     invariant {0 <= BV32.t'int !i <= BV32.t'int len}
 259     invariant {forall j:int. 0 <= j < BV32.t'int start ->
 260                  nth8_stream (old addr) j
 261                = nth8_stream addr j}
 262     invariant {forall j:int. BV32.t'int start <= j < BV32.t'int start + BV32.t'int !i ->
 263                  nth8_stream addr j
 264                = BV64.nth value (BV32.t'int len - j - 1 + BV32.t'int start) }
 265     invariant {forall j:int. BV32.t'int start + BV32.t'int !i <= j < 8 * length addr ->
 266                  nth8_stream addr j
 267                = nth8_stream (old addr) j }
 268
 269       let flag = peek_64bit value (BV32.u_add lstart !i) in
 270
 271       poke_8bit_array addr (BV32.u_add start !i) flag;
 272
 273       assert {nth8_stream addr (BV32.t'int start + BV32.t'int !i)
 274             = BV64.nth value ((BV32.t'int len - BV32.t'int !i - 1))};
 275       assert { forall k. BV32.t'int start <= k < BV32.t'int start + BV32.t'int !i ->
 276                k <> BV32.t'int start + BV32.t'int !i &&
 277                0 <= k < 8 * length addr &&
 278                    nth8_stream addr k
 279                  = BV64.nth value (BV32.t'int start + BV32.t'int len - k - 1)};
 280
 281       i := BV32.u_add !i (1:BV32.t);
 282     done;
 283
 284     0
 285
 286   let peekthenpoke (start len : BV32.t) (addr : array BV8.t)
 287     requires {8 * length addr < BV32.two_power_size}
 288     requires {0 <= BV32.t'int len < 64}
 289     requires {BV32.t'int start + BV32.t'int len <= 8 * length addr}
 290     ensures {result = 0}
 291     ensures {forall i. 0 <= i < 8 * length addr ->
 292                nth8_stream addr i = nth8_stream (old addr) i}
 293   =
 294     let value = peek start len addr in
 295     let res = poke start len addr value in
 296
 297     assert {res = 0};
 298
 299     assert {forall i. BV32.t'int start <= i < BV32.t'int start + BV32.t'int len ->
 300          nth8_stream addr i
 301        = nth8_stream (old addr) i};
 302
 303     res
 304
 305   let pokethenpeek (start len : BV32.t) (addr : array BV8.t) (value : BV64.t)
 306     writes   {addr}
 307     requires {8 * length addr < BV32.two_power_size}
 308     requires {0 <= BV32.t'int len < 64}
 309     requires {BV32.t'int start + BV32.t'int len <= 8 * length addr}
 310     requires {BV64.t'int value < BV64.t'int (maxvalue len)}
 311     ensures  {result = value}
 312   =
 313     assert { forall i:int. BV32.t'int len <= i < 64 ->
 314                BV64.nth value i = False };
 315     let poke_result = poke start len addr value in
 316     assert { poke_result = 0 };
 317     let peek_result = peek start len addr in
 318     assert { BV64.(==) peek_result value };
 319     peek_result
 320
 321 end