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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
module Python
use int.Int
use ref.Ref
use seq.Seq
use int.EuclideanDivision as E
type list 'a = private {
mutable elts: seq 'a;
mutable len: int;
} invariant { len = length elts }
meta coercion function elts
function ([]) (l: list 'a) (i: int) : 'a
= [@inline:trivial]
if i >= 0 then Seq.(l[i]) else Seq.(l[l.len + i])
val ghost function create (s: seq 'a) : list 'a
ensures { result = s }
ensures { len result = length s }
function ([<-]) (l: list 'a) (i: int) (v: 'a) : list 'a
= [@inline:trivial]
create (if i >= 0 then Seq.(l.elts[i <- v]) else Seq.(l.elts[l.len + i <- v]))
let ([]) (l: list 'a) (i: int) : 'a
requires { [@expl:index in array bounds] -len l <= i < len l }
ensures { result = l[i] }
= if i >= 0 then Seq.(l.elts[i]) else Seq.(l.elts[len l + i])
val ([]<-) (l: list 'a) (i: int) (v: 'a) : unit
requires { [@expl:index in array bounds] -len l <= i < len l }
writes { l.elts }
ensures { l.elts = (old l)[i <- v].elts }
val empty () : list 'a
ensures { result = Seq.empty }
val make (n: int) (v: 'a) : list 'a
requires { n >= 0 }
ensures { len result = n }
ensures { forall i. -n <= i < n -> result[i] = v }
(* ad-hoc facts about exchange *)
use seq.Occ
function occurrence (v: 'a) (l: list 'a) (lo hi: int): int =
Occ.occ v l lo hi
use int.Abs
(* Python's division and modulus according are neither Euclidean division,
nor computer division, but something else defined in
https://docs.python.org/3/reference/expressions.html *)
function (//) (x y: int) : int =
let q = E.div x y in
if y >= 0 then q else if E.mod x y > 0 then q-1 else q
function (%) (x y: int) : int =
let r = E.mod x y in
if y >= 0 then r else if r > 0 then r+y else r
lemma div_mod:
forall x y:int. y <> 0 -> x = y * (x // y) + (x % y)
lemma mod_bounds:
forall x y:int. y <> 0 -> 0 <= abs (x % y) < abs y
lemma mod_sign:
forall x y:int. y <> 0 -> if y < 0 then x % y <= 0 else x % y >= 0
val (//) (x y: int) : int
requires { [@expl:check division by zero] y <> 0 }
ensures { result = x // y }
val (%) (x y: int) : int
requires { [@expl:check division by zero] y <> 0 }
ensures { result = x % y }
(* random.randint *)
val randint (l u: int) : int
requires { [@expl:valid range] l <= u }
ensures { l <= result <= u }
use int.Power
function pow (x y: int) : int = power x y
val input () : int
val int (n: int) : int
ensures { result = n }
(* ajouts réalisés *)
val range (lo hi: int) : list int
requires { [@expl:valid range] lo <= hi }
ensures { len result = hi - lo }
ensures { forall i. 0 <= i < hi - lo -> result[i] = i + lo }
let range3 (le ri step: int) : list int
requires { [@expl:valid range] (le <= ri /\ step > 0) \/ (ri <= le /\ step < 0) }
ensures { len result = E.div (ri - le) step + if E.mod (ri - le) step <> 0 then 1 else 0 }
ensures { forall i. 0 <= i < len result -> result[i] = le + i * step }
= let n = E.div (ri - le) step + if E.mod (ri - le) step <> 0 then 1 else 0 in
let a = make n 0 in
for i=0 to n-1 do
invariant { forall j. 0 <= j < i -> a[j] = le + j * step }
a[i] <- le + i * step;
done;
assert { step > 0 -> le + n * step >= ri
/\ step > 0 -> le + (n-1) * step < ri
/\ step < 0 -> le + n * step <= ri
/\ step < 0 -> le + (n-1) * step > ri };
return a
val pop (l: list 'a) : 'a
requires { len l > 0 }
writes { l }
ensures { len l = len (old l) - 1 }
ensures { result = (old l)[len l] }
ensures { forall i. 0 <= i < len l -> l[i] = (old l)[i] }
val append (l: list 'a) (v: 'a) : unit
writes { l }
ensures { len l = len (old l) + 1 }
ensures { l[len (old l)] = v }
ensures { forall i. 0 <= i < len (old l) -> l[i] = (old l)[i] }
val function add_list (a1: list 'a) (a2: list 'a) : list 'a
ensures { len result = len a1 + len a2 }
ensures { forall i. 0 <= i < len a1 -> result[i] = a1[i] }
ensures { forall i. len a1 <= i < len result -> result[i] = a2[i-len a1] }
function transform_idx (l: list 'a) (i: int): int
= [@inline:trivial]
if i < 0 then len l + i else i
val function slice (l: list 'a) (lo hi: int) : list 'a
requires { transform_idx l lo >= 0 }
requires { transform_idx l hi <= len l }
requires { transform_idx l lo <= transform_idx l hi }
ensures { len result = transform_idx l hi - transform_idx l lo }
ensures { forall i. 0 <= i < len result -> result[i] = l[transform_idx l lo + i] }
val clear (l : list 'a) : unit
writes { l }
ensures { len l = 0 }
val copy (l: list 'a): list 'a
ensures { len result = len l }
ensures { result.elts = l.elts }
use seq.Permut
predicate is_permutation (l1 l2: list 'a)
= ([@expl:equality of length] length l1 = length l2)
/\ ([@expl:equality of elements] permut l1 l2 0 (length l2))
val sort (l : list int) : unit
writes { l.elts }
ensures { is_permutation l (old l) }
ensures { forall i, j. 0 <= i <= j < len(l) -> l[i] <= l[j] }
val reverse (l: list 'a) : unit
writes { l.elts }
ensures { len l = len (old l) }
ensures { forall i. 0 <= i < len l -> l[i] = (old l)[-(i+1)] }
ensures { forall i. 0 <= i < len l -> (old l)[i] = l[-(i+1)] }
ensures { is_permutation l (old l) }
end
|
