int.mlw 15.8 KB
Newer Older
1

2
(** {1 Machine Arithmetic} *)
3
4
5
6
7
8
9
10
11
12
13
14

(** {2 Integer Division}

It is checked that divisor is not null.

*)

module Int

  use export int.Int
  use export int.ComputerDivision

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15
  let (/) (x: int) (y: int)
16
    requires { [@expl:check division by zero] y <> 0 }
17
    ensures  { result = div x y }
18
19
  = div x y

20
  let (%) (x: int) (y: int)
21
    requires { [@expl:check modulo by zero] y <> 0 }
22
23
24
    ensures  { result = mod x y }
  = mod x y

25
26
27
28
end

(** {2 Machine integers}

29
  Bounded integers, typically n-bit signed and unsigned integers, go
30
  here. We first introduce a generic theory [Bounded_int] of bounded
31
  integers, with minimal and maximal values (resp. [min] and [max]).
32
33
  Then we instantiate it to get 32-bit and 64-bit signed and unsigned integers
  ([Int32], [UInt32], [Int64], and [UInt64]) as well as 31-bit and 63-bit signed
34
  integers ([Int31] and [Int63]) to be used in OCaml programs.
35
36
37
38
39

*)

module Bounded_int

40
  use int.Int
41
42
43
44
45
46

  type t

  constant min : int
  constant max : int

Guillaume Melquiond's avatar
Guillaume Melquiond committed
47
  function to_int (n:t) : int
Mário Pereira's avatar
Mário Pereira committed
48
  meta coercion function to_int
Guillaume Melquiond's avatar
Guillaume Melquiond committed
49
  meta "model_projection" function to_int
50

51
52
53
  val to_int (n:t) : int
    ensures { result = n }

54
55
  predicate in_bounds (n:int) = min <= n <= max

Mário Pereira's avatar
Mário Pereira committed
56
  axiom to_int_in_bounds: forall n:t. in_bounds n
57
58

  val of_int (n:int) : t
59
    requires { [@expl:integer overflow] in_bounds n }
Mário Pereira's avatar
Mário Pereira committed
60
    ensures  { result = n }
61
62

  val (+) (a:t) (b:t) : t
63
    requires { [@expl:integer overflow] in_bounds (a + b) }
Mário Pereira's avatar
Mário Pereira committed
64
    ensures   { result = a + b }
65
66

  val (-) (a:t) (b:t) : t
67
    requires { [@expl:integer overflow] in_bounds (a - b) }
Mário Pereira's avatar
Mário Pereira committed
68
    ensures  { result = a - b }
69

70
  val (*) (a:t) (b:t) : t
71
    requires { [@expl:integer overflow] in_bounds (a * b) }
Mário Pereira's avatar
Mário Pereira committed
72
    ensures  { result = a * b }
73
74

  val (-_) (a:t) : t
75
    requires { [@expl:integer overflow] in_bounds (- a) }
Mário Pereira's avatar
Mário Pereira committed
76
    ensures  { result = - a }
77
78
79

  axiom extensionality: forall x y: t. to_int x = to_int y -> x = y

Guillaume Melquiond's avatar
Guillaume Melquiond committed
80
  val (=) (a:t) (b:t) : bool
81
82
    ensures { to_int a = to_int b -> result }
    ensures { result -> a = b }
Guillaume Melquiond's avatar
Guillaume Melquiond committed
83

84
  val (<=) (a:t) (b:t) : bool
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
85
    ensures  { result <-> to_int a <= to_int b }
86
87

  val (<) (a:t) (b:t) : bool
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
88
    ensures  { result <-> to_int a < to_int b }
89
90

  val (>=) (a:t) (b:t) : bool
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91
    ensures  { result <-> to_int a >= to_int b }
92
93

  val (>) (a:t) (b:t) : bool
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94
    ensures  { result <-> to_int a > to_int b }
95

96
  use int.ComputerDivision
97
98

  val (/) (a:t) (b:t) : t
99
100
    requires { [@expl:division by zero] b <> 0 }
    requires { [@expl:integer overflow] in_bounds (div a b) }
101
    ensures  { result = div a b }
102

103
  val (%) (a:t) (b:t) : t
104
105
    requires { [@expl:division by zero] b <> 0 }
    requires { [@expl:integer overflow] in_bounds (mod a b) }
106
    ensures  { result = mod a b }
107

108
109
end

110
111
module Unsigned

112
  use int.Int
113

114
  let constant min_unsigned : int = 0
115
116

  clone export Bounded_int with
117
    constant min = min_unsigned, axiom .
118

119
120
121
122
  constant zero_unsigned : t

  axiom zero_unsigned_is_zero : to_int zero_unsigned = 0

123
124
125
126
  constant radix : int

  axiom radix_def : radix = max+1

127
128
129
130
131
132
end

module UnsignedGMP

  (** Additional GMP-inspired arithmetic primitives *)

133
  use int.Int
134
  clone export Unsigned with axiom .
135
  use int.EuclideanDivision
136

137
138
139
  val add_mod (x y:t) : t
    ensures { to_int result = mod (to_int x + to_int y) (max+1) }

140
  val add_with_carry (x y:t) (c:t) : (t,t)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
141
    requires { 0 <= to_int c <= 1 }
142
    returns { (r,d) ->
143
      to_int r + radix * to_int d =
144
145
      to_int x + to_int y + to_int c
      /\ 0 <= to_int d <= 1 }
146

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
  (* add_ssaaaa *)
  val add_double (a1 a0 b1 b0:t) : (t,t)
    returns { (h,l) -> l + radix * h
                     = mod (a0 + radix * a1 + b0 + radix * b1) (radix * radix) }

  (* add_ssaaaa with no overflow *)
  val add_double_nc (a1 a0 b1 b0:t) : (t,t)
    requires { a0 + radix * a1 + b0 + radix * b1 < radix * radix }
    returns  { (h, l) -> l + radix * h = a0 + radix * a1 + b0 + radix * b1 }

  (* add_ssaaaa with ghost carry *)
  val add_double_gc (a1 a0 b1 b0:t) : (ghost t, t, t)
    returns  { (c,h,l) -> l + radix * h + radix * radix * c
                          = a0 + radix * a1 + b0 + radix * b1
                        /\ 0 <= to_int c <= 1 }

163
  val sub_mod (x y:t) : t
164
    ensures { to_int result = mod (to_int x - to_int y) radix }
165

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
166
167
168
  val sub_with_borrow (x y:t) (b:t) : (t,t)
    requires { 0 <= to_int b <= 1 }
    returns { (r, d) ->
169
      to_int r - radix * to_int d  =
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
170
171
      to_int x - to_int y - to_int b
      /\ 0 <= to_int d <= 1 }
172

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
  (* sub_ddmmss *)
  val sub_double (a1 a0 b1 b0:t) : (t,t)
    returns { (h,l) -> l + radix * h
                       = mod ((a0 + radix * a1) - (b0 + radix * b1))
                             (radix * radix) }

  (* sub_ddmmss with no underflow *)
  val sub_double_nb (a1 a0 b1 b0:t) : (t,t)
    requires { 0 <= ((a0 + radix * a1) - (b0 + radix * b1)) }
    returns { (h,l) -> l + radix * h = ((a0 + radix * a1) - (b0 + radix * b1)) }

  (* sub_ddmmss with ghost borrow *)
  val sub_double_gb (a1 a0 b1 b0:t) : (ghost t,t,t)
    returns { (b,h,l) -> l + radix * h - radix*radix*b
                         = ((a0 + radix * a1) - (b0 + radix * b1))
                      /\ 0 <= b <= 1 }

Guillaume Melquiond's avatar
Guillaume Melquiond committed
190
  val add3 (x y z:t) : (t,t)
MARCHE Claude's avatar
MARCHE Claude committed
191
    returns { (r,d) ->
192
      to_int r + radix * to_int d =
193
      to_int x + to_int y + to_int z
194
      /\ 0 <= to_int d <= 2 }
MARCHE Claude's avatar
MARCHE Claude committed
195

196
  val mul_mod (x y:t) : t
197
    ensures { to_int result = mod (to_int x * to_int y) radix }
198

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
199
  val mul_double (x y:t) : (t,t) (* umul_ppmm *)
MARCHE Claude's avatar
MARCHE Claude committed
200
    returns { (r,d) ->
201
      to_int r + radix * to_int d =
Guillaume Melquiond's avatar
Guillaume Melquiond committed
202
      to_int x * to_int y }
MARCHE Claude's avatar
MARCHE Claude committed
203

204
205
end

206
207
module Int31

208
  use int.Int
209

210
  type int31 = < range -0x4000_0000 0x3fff_ffff >
211

212
213
214
  let constant min_int31 : int = - 0x4000_0000
  let constant max_int31 : int =   0x3fff_ffff
  function to_int (x : int31) : int = int31'int x
215
216
217

  clone export Bounded_int with
    type t = int31,
218
219
220
221
222
    constant min = int31'minInt,
    constant max = int31'maxInt,
    function to_int = int31'int,
    lemma to_int_in_bounds,
    lemma extensionality
223

224
(*  use bv.BV31 as BV31
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
225
226
227
228
229

  val to_bv (x: int31) : BV31.t
    ensures { BV31.to_int result = to_int x }
  val of_bv (x: BV31.t) : int31
    ensures { to_int result = BV31.to_int x }
230
*)
231
232
end

233
234
module Int32

235
  use int.Int
236

237
  type int32 = < range -0x8000_0000 0x7fff_ffff >
238

239
240
241
  let constant min_int32 : int = - 0x8000_0000
  let constant max_int32 : int =   0x7fff_ffff
  function to_int (x : int32) : int = int32'int x
242
243
244

  clone export Bounded_int with
    type t = int32,
245
246
247
248
249
    constant min = int32'minInt,
    constant max = int32'maxInt,
    function to_int = int32'int,
    lemma to_int_in_bounds,
    lemma extensionality
250

Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
251
(*
252
  use bv.BV32 as BV32
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
253
254
255
256
257

  val to_bv (x: int32) : BV32.t
    ensures { BV32.to_int result = to_int x }
  val of_bv (x: BV32.t) : int32
    ensures { to_int result = BV32.to_int x }
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
258
*)
259
260
end

261
262
263
264
module Int32BV

  use export Int32

265
  use bv.BV32 as BV32
266
267
268
269
270
271
272
273

  val to_bv (x: int32) : BV32.t
    ensures { BV32.to_int result = to_int x }
  val of_bv (x: BV32.t) : int32
    ensures { to_int result = BV32.to_int x }

end

274
module UInt32Gen
275

276
  use int.Int
277

278
  type uint32 = < range 0 0xffff_ffff >
279

280
  let constant max_uint32 : int = 0xffff_ffff
281
  let constant length : int = 32
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
282
  let constant radix : int = max_uint32 + 1
283
  function to_int (x : uint32) : int = uint32'int x
284

285
286
287
288
289
290
end

module UInt32

  use export UInt32Gen

291
  clone export Unsigned with
292
    type t = uint32,
293
    constant max = uint32'maxInt,
294
295
    constant radix = radix,
    goal radix_def,
296
297
298
299
    function to_int = uint32'int,
    lemma zero_unsigned_is_zero,
    lemma to_int_in_bounds,
    lemma extensionality
300

301
302
303
304
end

module UInt32GMP

305
306
307
308
  use int.Int
  use int.EuclideanDivision
  use int.Power
  use Int32
309
310
311
312
313
314
315
316
317
318
319
320
  use export UInt32Gen

  clone export UnsignedGMP with
    type t = uint32,
    constant max = uint32'maxInt,
    constant radix = radix,
    goal radix_def,
    function to_int = uint32'int,
    lemma zero_unsigned_is_zero,
    lemma to_int_in_bounds,
    lemma extensionality

321
  val lsld (x cnt:uint32) : (uint32,uint32)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
322
    requires { 0 < to_int cnt < 32 }
323
324
325
    returns { (r,d) -> to_int r + (max_uint32+1) * to_int d =
              (power 2 (to_int cnt)) * to_int x }

326
  val lsl (x cnt:uint32) : uint32
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
327
    requires { 0 <= to_int cnt < 32 }
328
329
330
    requires { (power 2 (to_int cnt)) * to_int x <= max_uint32 }
    ensures { to_int result = (power 2 (to_int cnt)) * to_int x }

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
331
332
333
  val lsr (x cnt:uint32) : uint32
    requires { 0 <= to_int cnt < 32 }
    requires { mod (to_int x) (power 2 (to_int cnt)) = 0 }
334
335
    ensures { to_int x = (power 2 (to_int cnt)) * to_int result }

336
  val div2by1 (l h d:uint32) : uint32
337
338
339
340
341
342
343
344
345
    requires { to_int h < to_int d }
    (* this pre implies d > 0 and also
       l + (max+1)*h < (max+1)+(max+1)*h
                     = (max+1)*(h+1)
       thus
       (l + (max+1)*h)/d < (max+1)*(h+1)/d
                         <= max+1   (since h < d)
       thus the result is <= max, no overflow
    *)
346
347
348
    ensures { to_int result
            = div (to_int l + (max_uint32+1) * to_int h) (to_int d) }

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
349
  val predicate is_msb_set (x:uint32) : bool
350
351
    ensures { result <-> 2 * to_int x > max_uint32 }

352
  val count_leading_zeros (x:uint32) : int32
353
    requires { to_int x > 0 }
354
355
    ensures { (power 2 (Int32.to_int result)) * to_int x <= max_uint32 }
    ensures { 2 * (power 2 (Int32.to_int result)) * to_int x > max_uint32 }
356
357
358
359
360
    ensures { 0 <= Int32.to_int result < 32 }

  val of_int32(x:int32) : uint32
    requires { Int32.to_int x >= 0 }
    ensures { to_int result = Int32.to_int x }
361

362
(*  use bv.BV32 as BV32
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
363
364
365
366
367

  val to_bv (x: uint32) : BV32.t
    ensures { BV32.to_uint result = to_int x }
  val of_bv (x: BV32.t) : uint32
    ensures { to_int result = BV32.to_uint x }
368
*)
369
370
end

371
372
module Int63

373
  use int.Int
374

375
  type int63 = < range -0x4000_0000_0000_0000 0x3fff_ffff_ffff_ffff >
376

377
378
379
  let constant min_int63 : int = - 0x4000_0000_0000_0000
  let constant max_int63 : int =   0x3fff_ffff_ffff_ffff
  function to_int (x : int63) : int = int63'int x
380
381
382

  clone export Bounded_int with
    type t = int63,
383
384
385
386
387
    constant min = int63'minInt,
    constant max = int63'maxInt,
    function to_int = int63'int,
    lemma to_int_in_bounds,
    lemma extensionality
388

389
390
391
392
393
394
  let constant zero = (0:int63)
  let constant one = (1:int63)
  val constant max_int:int63
     ensures { int63'int result = max_int63)
  val constant min_int:int63
     ensures { int63'int result = min_int63
395

396
(*  use bv.BV63 as BV63
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
397
398
399
400
401

  val to_bv (x: int63) : BV63.t
    ensures { BV63.to_int result = to_int x }
  val of_bv (x: BV63.t) : int63
    ensures { to_int result = BV63.to_int x }
402
*)
403
404
end

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
405
406
module Refint63

407
408
  use int.Int
  use Int63
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
409
410
411
  use export ref.Ref

  let incr (r: ref int63) : unit
412
    requires { [@expl:integer overflow] to_int !r < max_int63 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
413
    ensures  { to_int !r = to_int (old !r) + 1 }
414
  = r := !r + (1:int63)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
415
  let decr (r: ref int63) : unit
416
    requires { [@expl:integer overflow] min_int63 < to_int !r }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
417
    ensures  { to_int !r = to_int (old !r) - 1 }
418
  = r := !r - (1:int63)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
419
420

  let (+=) (r: ref int63) (v: int63) : unit
421
    requires { [@expl:integer overflow] in_bounds (to_int !r + to_int v) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
422
423
424
425
    ensures { to_int !r = to_int (old !r) + to_int v }
  = r := !r + v

  let (-=) (r: ref int63) (v: int63) : unit
426
    requires { [@expl:integer overflow] in_bounds (to_int !r - to_int v) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
427
428
429
430
    ensures  { to_int !r = to_int (old !r) - to_int v }
  = r := !r - v

  let ( *= ) (r: ref int63) (v: int63) : unit
431
    requires { [@expl:integer overflow] in_bounds (to_int !r * to_int v) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
432
433
434
435
436
437
438
    ensures { to_int !r = to_int (old !r) * to_int v }
  = r := !r * v

end

module MinMax63

439
440
  use int.Int
  use Int63
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
441
442
443
444
445
446
447
448
449
450
451

  let min (x y: int63) : int63
    ensures { result = if to_int x <= to_int y then x else y }
  = if x <= y then x else y

  let max (x y: int63) : int63
    ensures { result = if to_int x >= to_int y then x else y }
  = if x >= y then x else y

end

452
453
454
455
456
457
458

(** {2 Mutable states of pseudo-random generators}

  Basically a reference containing a pure generator. *)

module State63

459
460
  use int.Int
  use Int63
461

462
  type state = private mutable { }
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481

  val create (seed: int63) : state

  val init (s: state) (seed: int63) : unit writes {s}

  val self_init (s: state) : unit writes {s}

  val random_bool (s: state) : bool writes {s}

  val random_int63 (s: state) (n: int63) : int63 writes {s}
    requires { 0 < n }
    ensures  { 0 <= result < n }

end

(** {2 A global pseudo-random generator} *)

module Random63

482
483
484
  use int.Int
  use Int63
  use State63
485
486
487

  val s: state

488
  let init (seed: int63) = init s seed
489
490
491
492

  let self_init () = self_init s

  let random_bool ()
493
    writes { s }
494
495
496
  = random_bool s

  let random_int63 (n: int63) : int63
497
    requires { 0 < n } (* FIXME: n should be less than 2^30 *)
498
    writes   { s }
499
500
501
502
503
    ensures  { 0 <= result < n }
  = random_int63 s n

end

504
505
module Int64

506
  use int.Int
507

508
  type int64 = < range -0x8000_0000_0000_0000 0x7fff_ffff_ffff_ffff >
509

510
511
512
  let constant min_int64 : int = - 0x8000_0000_0000_0000
  let constant max_int64 : int =   0x7fff_ffff_ffff_ffff
  function to_int (x : int64) : int = int64'int x
513
514
515

  clone export Bounded_int with
    type t = int64,
516
517
518
519
520
    constant min = int64'minInt,
    constant max = int64'maxInt,
    function to_int = int64'int,
    lemma to_int_in_bounds,
    lemma extensionality
521

522
(*  use bv.BV64 as BV64
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
523
524
525
526
527

  val to_bv (x: int64) : BV64.t
    ensures { BV64.to_int result = to_int x }
  val of_bv (x: BV64.t) : int64
    ensures { to_int result = BV64.to_int x }
528
*)
529
530
end

531
module UInt64Gen
532

533
  use int.Int
534

535
  type uint64 = < range 0 0xffff_ffff_ffff_ffff >
536

537
  let constant max_uint64 : int = 0xffff_ffff_ffff_ffff
538
  let constant length : int = 64
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
539
  let constant radix : int = max_uint64 + 1
540

541
  function to_int (x : uint64) : int = uint64'int x
542

543
544
545
546
547
548
end

module UInt64

  use export UInt64Gen

549
  clone export Unsigned with
550
    type t = uint64,
551
    constant max = uint64'maxInt,
552
553
    constant radix = radix,
    goal radix_def,
554
555
556
557
    function to_int = uint64'int,
    lemma zero_unsigned_is_zero,
    lemma to_int_in_bounds,
    lemma extensionality
558

559
(*  use bv.BV64 as BV64
560
561
562
563
564
565
566
567
568
569

  val to_bv (x: uint64) : BV64.t
    ensures { BV64.to_uint result = to_int x }
  val of_bv (x: BV64.t) : uint64
    ensures { to_int result = BV64.to_uint x }
*)
end

module UInt64GMP

570
571
572
573
  use int.Int
  use int.EuclideanDivision
  use int.Power
  use Int32
Raphaël Rieu-Helft's avatar
Toom32    
Raphaël Rieu-Helft committed
574
  use Int64
575
576
577
578
579
580
581
582
583
584
585
586
  use export UInt64Gen

  clone export UnsignedGMP with
    type t = uint64,
    constant max = uint64'maxInt,
    constant radix = radix,
    goal radix_def,
    function to_int = uint64'int,
    lemma zero_unsigned_is_zero,
    lemma to_int_in_bounds,
    lemma extensionality

587
  val lsld (x cnt:uint64) : (uint64,uint64)
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
588
    requires { 0 < to_int cnt < 64 }
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
    returns { (r,d) -> to_int r + (max_uint64+1) * to_int d =
              (power 2 (to_int cnt)) * to_int x }

  val lsl (x cnt:uint64) : uint64
    requires { 0 <= to_int cnt < 64 }
    requires { (power 2 (to_int cnt)) * to_int x <= max_uint64 }
    ensures { to_int result = (power 2 (to_int cnt)) * to_int x }

  val lsr (x cnt:uint64) : uint64
    requires { 0 <= to_int cnt < 64 }
    requires { mod (to_int x) (power 2 (to_int cnt)) = 0 }
    ensures { to_int x = (power 2 (to_int cnt)) * to_int result }

  val div2by1 (l h d:uint64) : uint64
    requires { to_int h < to_int d }
    (* this pre implies d > 0 and also
       l + (max+1)*h < (max+1)+(max+1)*h
                     = (max+1)*(h+1)
       thus
       (l + (max+1)*h)/d < (max+1)*(h+1)/d
                         <= max+1   (since h < d)
       thus the result is <= max, no overflow
    *)
    ensures { to_int result
            = div (to_int l + (max_uint64+1) * to_int h) (to_int d) }

  val predicate is_msb_set (x:uint64) : bool
    ensures { result <-> 2 * to_int x > max_uint64 }

618
  val count_leading_zeros (x:uint64) : int32
619
    requires { to_int x > 0 }
620
621
    ensures { (power 2 (Int32.to_int result)) * to_int x <= max_uint64 }
    ensures { 2 * (power 2 (Int32.to_int result)) * to_int x > max_uint64 }
622
623
624
625
626
    ensures { 0 <= Int32.to_int result < 64 }

  val of_int32(x:int32) : uint64
    requires { Int32.to_int x >= 0 }
    ensures { to_int result = Int32.to_int x }
627

Raphaël Rieu-Helft's avatar
Toom32    
Raphaël Rieu-Helft committed
628
629
630
631
632
633
634
635
  val to_int64(x:uint64) : int64
    requires { x <= max_int64 }
    ensures  { Int64.to_int result = x }

  val of_int64(x:int64) : uint64
    requires { 0 <= x }
    ensures  { to_int result = x }

636
end