bitwalker.mlw 12.3 KB
Newer Older
1
module Bitwalker
2 3 4 5
  use int.Int
  use int.EuclideanDivision
  use array.Array
  use ref.Ref
6 7 8 9 10 11
  (* 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
12 13 14
  use bv.BVConverter_32_64 as C32_64
  use bv.BVConverter_8_32 as C8_32

15
(* file missing in repository
16
  use mach.bv.BV
17 18
*)

19
  function nth8_stream (stream : array BV8.t) (pos : int) : bool =
20 21 22 23 24 25 26 27
    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 ->
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 =
MARCHE Claude's avatar
MARCHE Claude committed
32
    BV64.lsl_bv (1:BV64.t) (C32_64.toBig len)
33

34
  let lemma nth_ultpre0 (x:BV64.t) (len:BV32.t)
Clément Fumex's avatar
Clément Fumex committed
35 36 37
    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) }
38
  =
MARCHE Claude's avatar
MARCHE Claude committed
39 40
    assert { BV32.ult len (64:BV32.t) };
    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` *)
MARCHE Claude's avatar
MARCHE Claude committed
44
  let poke_64bit_bv (value : BV64.t) (left : BV32.t) (flag : bool) : BV64.t
Clément Fumex's avatar
Clément Fumex committed
45 46
    requires { BV32.t'int left < 64 }
    ensures  { forall i. 0 <= i < 64 /\ i <> 63 - BV32.t'int left ->
47
                 BV64.nth result i = BV64.nth value i }
Clément Fumex's avatar
Clément Fumex committed
48
    ensures  { flag = BV64.nth result (63 - BV32.t'int left) }
49
  =
MARCHE Claude's avatar
MARCHE Claude committed
50
    assert { BV32.ult left (64:BV32.t) };
51
    begin
MARCHE Claude's avatar
MARCHE Claude committed
52
    ensures { forall i:BV32.t. i <> BV32.sub (63:BV32.t) left ->
53 54 55
               BV64.nth_bv result (C32_64.toBig i) =
                 BV64.nth_bv value (C32_64.toBig i) }
    ensures { flag = BV64.nth_bv result
MARCHE Claude's avatar
MARCHE Claude committed
56
                       (C32_64.toBig (BV32.sub (63:BV32.t) left)) }
57
      let mask =
58 59
        BV64.lsl_bv (1:BV64.t)
          (C32_64.toBig (BV32.sub_check (63:BV32.t) left))
60 61 62 63 64 65 66
      in
      match flag with
      | True -> BV64.bw_or value mask
      | False -> BV64.bw_and value (BV64.bw_not mask)
      end
    end

67 68
 (** 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
69 70 71 72 73 74 75 76 77
  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
MARCHE Claude's avatar
MARCHE Claude committed
78 79
    assert { BV64.ult left_bv (64:BV64.t) };
    assert { (BV64.sub (63:BV64.t) left_bv) = BV64.of_int (63 - left) };
80
    begin
MARCHE Claude's avatar
MARCHE Claude committed
81 82
    ensures { forall i:BV64.t. BV64.ule i (63:BV64.t) ->
               i <> BV64.sub (63:BV64.t) left_bv ->
83
               BV64.nth_bv result i = BV64.nth_bv value i }
MARCHE Claude's avatar
MARCHE Claude committed
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 88 89 90 91 92 93 94
      in
      match flag with
      | True -> BV64.bw_or value mask
      | False -> BV64.bw_and value (BV64.bw_not mask)
      end
    end


95
  (* return the bit of `byte` at position `left` starting from the
96
  left *)
97

MARCHE Claude's avatar
MARCHE Claude committed
98
  let peek_8bit_bv (byte : BV8.t) (left : BV32.t) : bool
Clément Fumex's avatar
Clément Fumex committed
99 100
    requires { 0 <= BV32.t'int left < 8 }
    ensures  { result = BV8.nth byte (7 - BV32.t'int left) }
101
  =
MARCHE Claude's avatar
MARCHE Claude committed
102
    assert {BV32.ult left (8:BV32.t)};
103
    begin
104
      ensures {
105
        result = BV8.nth_bv
MARCHE Claude's avatar
MARCHE Claude committed
106
                   byte (BV8.sub (7:BV8.t) (C8_32.toSmall left))}
107
    let mask =
108
      BV32.lsl_bv (1:BV32.t) (BV32.sub_check (7:BV32.t) left)
109
    in
110
    not (BV32.eq (BV32.bw_and (C8_32.toBig byte) mask) BV32.zeros)
111 112
    end

113
  (* return the bit of the `left`/8 element of `addr` at position mod `left` 8 starting from the left *)
MARCHE Claude's avatar
MARCHE Claude committed
114 115
  let peek_8bit_array (addr : array BV8.t) (left : BV32.t) : bool
    requires { 8 * (length addr) < BV32.two_power_size }
Clément Fumex's avatar
Clément Fumex committed
116 117
    requires { BV32.t'int left < 8 * length addr }
    ensures  { result = nth8_stream addr (BV32.t'int left) }
118
  =
119
    peek_8bit_bv (addr[ BV32.to_uint (BV32.udiv_check left (8:BV32.t)) ]) (BV32.urem_check left (8:BV32.t))
120

121 122
  (* return a bitvector of 64 bits with its `len` bits of the right
    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
Clément Fumex's avatar
Clément Fumex committed
124 125
    requires { BV32.t'int len <= 64 }
    requires { BV32.t'int start + BV32.t'int len < BV32.two_power_size }
MARCHE Claude's avatar
MARCHE Claude committed
126
    requires { 8 * length addr < BV32.two_power_size }
Clément Fumex's avatar
Clément Fumex committed
127
    ensures  { BV32.t'int start + BV32.t'int len > (8 * length addr) ->
128
      result = BV64.zeros }
Clément Fumex's avatar
Clément Fumex committed
129 130
    ensures  { BV32.t'int start + BV32.t'int len <= (8 * length addr) ->
      (forall i:int. 0 <= i < BV32.t'int len ->
MARCHE Claude's avatar
MARCHE Claude committed
131
         BV64.nth result i
Clément Fumex's avatar
Clément Fumex committed
132
         = nth8_stream addr (BV32.t'int start + BV32.t'int len - i - 1))
MARCHE Claude's avatar
MARCHE Claude committed
133
      /\
Clément Fumex's avatar
Clément Fumex committed
134
      (forall i:int. BV32.t'int len <= i < 64 -> BV64.nth result i = False) }
135
  =
136
    if (BV32.to_uint (BV32.add_check start len) > ( 8 *length addr ))
137
    then
138
      BV64.zeros
139 140
    else

141 142
    let retval = ref BV64.zeros in
    let i = ref BV32.zeros in
MARCHE Claude's avatar
MARCHE Claude committed
143
    let lstart = BV32.sub_check (64:BV32.t) len in
144

145
    while BV32.ult !i len do variant{ BV32.t'int len - BV32.t'int !i }
Clément Fumex's avatar
Clément Fumex committed
146 147
    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 ->
148
                 BV64.nth !retval j
Clément Fumex's avatar
Clément Fumex committed
149 150
               = 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 ->
151 152
                 BV64.nth !retval j
               = False}
Clément Fumex's avatar
Clément Fumex committed
153
    invariant {forall j:int. BV32.t'int len <= j < 64 ->
154 155 156
                 BV64.nth !retval j
               = False}

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

160
      i := BV32.add_check !i (1:BV32.t);
161 162 163

    done;

164
    !retval
165

166
  let peek_64bit (value : BV64.t) (left : BV32.t) : bool
Clément Fumex's avatar
Clément Fumex committed
167 168
    requires {BV32.t'int left < 64}
    ensures {result = BV64.nth value (63 - BV32.t'int left)}
169
  =
MARCHE Claude's avatar
MARCHE Claude committed
170
     assert {BV32.ult left (64:BV32.t)};
171
     begin
172
     ensures {result = BV64.nth_bv value
MARCHE Claude's avatar
MARCHE Claude committed
173
                       (BV64.sub (63:BV64.t) (C32_64.toBig left))}
174 175
       let mask = BV64.lsl_bv (1:BV64.t)
                  (C32_64.toBig (BV32.sub_check (63:BV32.t) left)) in
176
       not (BV64.eq (BV64.bw_and value mask) BV64.zeros)
177
     end
178

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

184 185 186
    return (flag == 0) ? (byte & ~mask) : (byte | mask);
  }
*)
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
Clément Fumex's avatar
Clément Fumex committed
190 191
    requires { BV32.t'int left < 8 }
    ensures  { forall i:int. 0 <= i < 8 -> i <> 7 - BV32.t'int left ->
192
               BV8.nth result i = BV8.nth byte i }
Clément Fumex's avatar
Clément Fumex committed
193
    ensures  { BV8.nth result (7 - BV32.t'int left) = flag }
194
  =
MARCHE Claude's avatar
MARCHE Claude committed
195
    assert { BV32.ult left (8:BV32.t) };
196
    begin
MARCHE Claude's avatar
MARCHE Claude committed
197 198
    ensures { forall i:BV32.t. BV32.ult i (8:BV32.t) ->
               i <> BV32.sub (7:BV32.t) left ->
199 200
               BV8.nth_bv result (C8_32.toSmall i)
             = BV8.nth_bv byte (C8_32.toSmall i) }
MARCHE Claude's avatar
MARCHE Claude committed
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.sub_check (7:BV8.t) (C8_32.toSmall left)) in
204 205 206 207 208
      match flag with
      | True -> BV8.bw_or byte mask
      | False -> BV8.bw_and byte (BV8.bw_not mask)
      end
    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 }
Clément Fumex's avatar
Clément Fumex committed
212
    requires { BV32.t'int left < 8 * length addr }
213
    writes   { addr }
Clément Fumex's avatar
Clément Fumex committed
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}
Clément Fumex's avatar
Clément Fumex committed
216
    ensures  { nth8_stream addr (BV32.t'int left) = flag }
217
  =
218 219 220
    let i = BV32.udiv_check left (8:BV32.t) in
    let k = BV32.urem_check left (8:BV32.t) in
    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 }
Clément Fumex's avatar
Clément Fumex committed
224 225
    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 }
226
    requires{ 8 * length addr < BV32.two_power_size }
227
    ensures { -2 <= result <= 0 }
Clément Fumex's avatar
Clément Fumex committed
228 229 230
    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 }
231
    ensures { result =  0 ->
Clément Fumex's avatar
Clément Fumex committed
232
              (forall i:int. 0 <= i < BV32.t'int start ->
233 234 235
                nth8_stream (old addr) i
              = nth8_stream addr i)
           /\
Clément Fumex's avatar
Clément Fumex committed
236
              (forall i:int. BV32.t'int start <= i < BV32.t'int start + BV32.t'int len ->
237
                nth8_stream addr i
Clément Fumex's avatar
Clément Fumex committed
238
              = BV64.nth value (BV32.t'int len - i - 1 + BV32.t'int start))
239
           /\
Clément Fumex's avatar
Clément Fumex committed
240
              (forall i:int. BV32.t'int start + BV32.t'int len <= i < 8 * length addr ->
241 242
                nth8_stream addr i
              = nth8_stream (old addr) i) }
243
  =
244
    if BV32.to_uint (BV32.add_check start len) > 8 * length addr
245 246 247 248
    then
      -1                        (*error: invalid_bit_sequence*)
    else

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

MARCHE Claude's avatar
MARCHE Claude committed
254
    let lstart = BV32.sub_check (64:BV32.t) len in
255
    let i = ref BV32.zeros in
256

257
    while BV32.ult !i len do variant { BV32.t'int len - BV32.t'int !i }
Clément Fumex's avatar
Clément Fumex committed
258 259
    invariant {0 <= BV32.t'int !i <= BV32.t'int len}
    invariant {forall j:int. 0 <= j < BV32.t'int start ->
260
                 nth8_stream (old addr) j
261
               = nth8_stream addr j}
Clément Fumex's avatar
Clément Fumex committed
262
    invariant {forall j:int. BV32.t'int start <= j < BV32.t'int start + BV32.t'int !i ->
263
                 nth8_stream addr j
Clément Fumex's avatar
Clément Fumex committed
264 265
               = 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 ->
266
                 nth8_stream addr j
267
               = nth8_stream (old addr) j }
268

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

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

Clément Fumex's avatar
Clément Fumex committed
273 274 275 276
      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 &&
277 278
               0 <= k < 8 * length addr &&
                   nth8_stream addr k
Clément Fumex's avatar
Clément Fumex committed
279
                 = BV64.nth value (BV32.t'int start + BV32.t'int len - k - 1)};
280

281
      i := BV32.add_check !i (1:BV32.t);
282 283 284 285 286
    done;

    0

  let peekthenpoke (start len : BV32.t) (addr : array BV8.t)
287
    requires {8 * length addr < BV32.two_power_size}
Clément Fumex's avatar
Clément Fumex committed
288 289
    requires {0 <= BV32.t'int len < 64}
    requires {BV32.t'int start + BV32.t'int len <= 8 * length addr}
290
    ensures {result = 0}
291 292
    ensures {forall i. 0 <= i < 8 * length addr ->
               nth8_stream addr i = nth8_stream (old addr) i}
293 294 295 296
  =
    let value = peek start len addr in
    let res = poke start len addr value in

297 298
    assert {res = 0};

Clément Fumex's avatar
Clément Fumex committed
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 304 305 306

    res

  let pokethenpeek (start len : BV32.t) (addr : array BV8.t) (value : BV64.t)
    writes   {addr}
307
    requires {8 * length addr < BV32.two_power_size}
Clément Fumex's avatar
Clément Fumex committed
308 309 310
    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)}
311 312
    ensures  {result = value}
  =
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 320 321
    peek_result

end