1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
(** {2 One-time integers}
This module implements the idea described in this paper:
{h <a href="https://hal.inria.fr/hal-01162661">
How to avoid proving the absence of integer overflows</a>}
When extracted to OCaml, the following type `OneTime.t` will be mapped to
OCaml's type `int` (63-bit signed integers).
See also `mach.peano`.
*)
module OneTime
use int.Int
type t = abstract { v: int; mutable valid: bool }
meta coercion function v
val to_int (x: t) : int
ensures { result = x.v }
val zero (): t
ensures { result.valid }
ensures { result.v = 0 }
val one () : t
ensures { result.valid }
ensures { result.v = 1 }
val succ (x: t) : t
requires { x.valid }
writes { x.valid }
ensures { result.valid /\ not x.valid }
ensures { result.v = x.v + 1 }
val pred (x: t) : t
requires { x.valid }
writes { x.valid }
ensures { result.valid /\ not x.valid }
ensures { result.v = x.v - 1 }
val lt (x y: t) : bool
ensures { result <-> x.v < y.v }
val le (x y: t) : bool
ensures { result <-> x.v <= y.v }
val gt (x y: t) : bool
ensures { result <-> x.v > y.v }
val ge (x y: t) : bool
ensures { result <-> x.v >= y.v }
val eq (x y: t) : bool
ensures { result <-> x.v = y.v }
val ne (x y: t) : bool
ensures { result <-> x.v <> y.v }
use mach.peano.Peano as P
val to_peano (x: t) : P.t
ensures { result.P.v = x.v }
val transfer (x: t) : t
requires { x.valid }
writes { x.valid }
ensures { result.valid /\ not x.valid }
ensures { result.v = x.v }
val neg (x: t) : t
requires { x.valid }
writes { x.valid }
ensures { result.valid /\ not x.valid }
ensures { result.v = - x.v }
val abs (x: t) : t
requires { x.valid }
writes { x.valid }
ensures { result.valid /\ not x.valid }
ensures { result.v = if x.v >= 0 then x.v else - x.v }
val add (x y: t) : t
requires { x.valid /\ y.valid }
writes { x.valid, y.valid }
ensures { result.valid /\ not x.valid /\ not y.valid }
ensures { result.v = x.v + y.v }
val sub (x y: t) : t
requires { x.valid /\ y.valid }
writes { x.valid, y.valid }
ensures { result.valid /\ not x.valid /\ not y.valid }
ensures { result.v = x.v - y.v }
val split (x: t) (p: P.t) : (t, t)
requires { x.valid }
requires { 0 <= p.P.v <= x.v \/ x.v <= p.P.v <= 0 }
writes { x.valid }
ensures { not x.valid }
returns { a, b -> a.valid /\ b.valid /\ a.v = x.v - b.v /\ b.v = p.P.v }
end
|
