summaryrefslogtreecommitdiff
path: root/tests/fstar/betree_back_stateful/Primitives.fst
blob: cd18cf29a13810f406179c403844d6545fbc5434 (plain)
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
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
/// This file lists primitive and assumed functions and types
module Primitives
open FStar.Mul
open FStar.List.Tot

#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"

(*** Utilities *)
val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) :
  ls':list a{
    length ls' = length ls /\
    index ls' i == x
  }
#push-options "--fuel 1"
let rec list_update #a ls i x =
  match ls with
  | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x
#pop-options

(*** Result *)
type error : Type0 =
| Failure
| OutOfFuel

type result (a : Type0) : Type0 =
| Return : v:a -> result a
| Fail : e:error -> result a

// Monadic return operator
unfold let return (#a : Type0) (x : a) : result a = Return x

// Monadic bind operator.
// Allows to use the notation:
// ```
// let* x = y in
// ...
// ```
unfold let (let*) (#a #b : Type0) (m: result a)
  (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) :
  result b =
  match m with
  | Return x -> f x
  | Fail e   -> Fail e

// Monadic assert(...)
let massert (b:bool) : result unit = if b then Return () else Fail Failure

// Normalize and unwrap a successful result (used for globals).
let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x

(*** Misc *)
type char = FStar.Char.char
type string = string

let is_zero (n: nat) : bool = n = 0
let decrease (n: nat{n > 0}) : nat = n - 1

let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
let mem_replace_back (a : Type0) (x : a) (y : a) : a = y

(*** Scalars *)
/// Rem.: most of the following code was partially generated

let isize_min : int = -9223372036854775808 // TODO: should be opaque
let isize_max : int = 9223372036854775807 // TODO: should be opaque
let i8_min : int = -128
let i8_max : int = 127
let i16_min : int = -32768
let i16_max : int = 32767
let i32_min : int = -2147483648
let i32_max : int = 2147483647
let i64_min : int = -9223372036854775808
let i64_max : int = 9223372036854775807
let i128_min : int = -170141183460469231731687303715884105728
let i128_max : int = 170141183460469231731687303715884105727
let usize_min : int = 0
let usize_max : int = 4294967295 // TODO: should be opaque
let u8_min : int = 0
let u8_max : int = 255
let u16_min : int = 0
let u16_max : int = 65535
let u32_min : int = 0
let u32_max : int = 4294967295
let u64_min : int = 0
let u64_max : int = 18446744073709551615
let u128_min : int = 0
let u128_max : int = 340282366920938463463374607431768211455

type scalar_ty =
| Isize
| I8
| I16
| I32
| I64
| I128
| Usize
| U8
| U16
| U32
| U64
| U128

let scalar_min (ty : scalar_ty) : int =
  match ty with
  | Isize -> isize_min
  | I8 -> i8_min
  | I16 -> i16_min
  | I32 -> i32_min
  | I64 -> i64_min
  | I128 -> i128_min
  | Usize -> usize_min
  | U8 -> u8_min
  | U16 -> u16_min
  | U32 -> u32_min
  | U64 -> u64_min
  | U128 -> u128_min

let scalar_max (ty : scalar_ty) : int =
  match ty with
  | Isize -> isize_max
  | I8 -> i8_max
  | I16 -> i16_max
  | I32 -> i32_max
  | I64 -> i64_max
  | I128 -> i128_max
  | Usize -> usize_max
  | U8 -> u8_max
  | U16 -> u16_max
  | U32 -> u32_max
  | U64 -> u64_max
  | U128 -> u128_max

type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty}

let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) =
  if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail Failure

let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x)

let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
  if y <> 0 then mk_scalar ty (x / y) else Fail Failure

/// The remainder operation
let int_rem (x : int) (y : int{y <> 0}) : int =
  if x >= 0 then (x % y) else -(x % y)

(* Checking consistency with Rust *)
let _ = assert_norm(int_rem 1 2 = 1)
let _ = assert_norm(int_rem (-1) 2 = -1)
let _ = assert_norm(int_rem 1 (-2) = 1)
let _ = assert_norm(int_rem (-1) (-2) = -1)

let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
  if y <> 0 then mk_scalar ty (int_rem x y) else Fail Failure

let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
  mk_scalar ty (x + y)

let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
  mk_scalar ty (x - y)

let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
  mk_scalar ty (x * y)

(** Cast an integer from a [src_ty] to a [tgt_ty] *)
// TODO: check the semantics of casts in Rust
let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
  mk_scalar tgt_ty x

/// The scalar types
type isize : eqtype = scalar Isize
type i8    : eqtype = scalar I8
type i16   : eqtype = scalar I16
type i32   : eqtype = scalar I32
type i64   : eqtype = scalar I64
type i128  : eqtype = scalar I128
type usize : eqtype = scalar Usize
type u8    : eqtype = scalar U8
type u16   : eqtype = scalar U16
type u32   : eqtype = scalar U32
type u64   : eqtype = scalar U64
type u128  : eqtype = scalar U128


let core_isize_min : isize = isize_min
let core_isize_max : isize = isize_max
let core_i8_min    : i8 = i8_min
let core_i8_max    : i8 = i8_max
let core_i16_min   : i16 = i16_min
let core_i16_max   : i16 = i16_max
let core_i32_min   : i32 = i32_min
let core_i32_max   : i32 = i32_max
let core_i64_min   : i64 = i64_min
let core_i64_max   : i64 = i64_max
let core_i128_min  : i128 = i128_min
let core_i128_max  : i128 = i128_max

let core_usize_min : usize = usize_min
let core_usize_max : usize = usize_max
let core_u8_min    : u8 = u8_min
let core_u8_max    : u8 = u8_max
let core_u16_min   : u16 = u16_min
let core_u16_max   : u16 = u16_max
let core_u32_min   : u32 = u32_min
let core_u32_max   : u32 = u32_max
let core_u64_min   : u64 = u64_min
let core_u64_max   : u64 = u64_max
let core_u128_min  : u128 = u128_min
let core_u128_max  : u128 = u128_max

/// Negation
let isize_neg = scalar_neg #Isize
let i8_neg = scalar_neg #I8
let i16_neg = scalar_neg #I16
let i32_neg = scalar_neg #I32
let i64_neg = scalar_neg #I64
let i128_neg = scalar_neg #I128

/// Division
let isize_div = scalar_div #Isize
let i8_div = scalar_div #I8
let i16_div = scalar_div #I16
let i32_div = scalar_div #I32
let i64_div = scalar_div #I64
let i128_div = scalar_div #I128
let usize_div = scalar_div #Usize
let u8_div = scalar_div #U8
let u16_div = scalar_div #U16
let u32_div = scalar_div #U32
let u64_div = scalar_div #U64
let u128_div = scalar_div #U128

/// Remainder
let isize_rem = scalar_rem #Isize
let i8_rem = scalar_rem #I8
let i16_rem = scalar_rem #I16
let i32_rem = scalar_rem #I32
let i64_rem = scalar_rem #I64
let i128_rem = scalar_rem #I128
let usize_rem = scalar_rem #Usize
let u8_rem = scalar_rem #U8
let u16_rem = scalar_rem #U16
let u32_rem = scalar_rem #U32
let u64_rem = scalar_rem #U64
let u128_rem = scalar_rem #U128

/// Addition
let isize_add = scalar_add #Isize
let i8_add = scalar_add #I8
let i16_add = scalar_add #I16
let i32_add = scalar_add #I32
let i64_add = scalar_add #I64
let i128_add = scalar_add #I128
let usize_add = scalar_add #Usize
let u8_add = scalar_add #U8
let u16_add = scalar_add #U16
let u32_add = scalar_add #U32
let u64_add = scalar_add #U64
let u128_add = scalar_add #U128

/// Substraction
let isize_sub = scalar_sub #Isize
let i8_sub = scalar_sub #I8
let i16_sub = scalar_sub #I16
let i32_sub = scalar_sub #I32
let i64_sub = scalar_sub #I64
let i128_sub = scalar_sub #I128
let usize_sub = scalar_sub #Usize
let u8_sub = scalar_sub #U8
let u16_sub = scalar_sub #U16
let u32_sub = scalar_sub #U32
let u64_sub = scalar_sub #U64
let u128_sub = scalar_sub #U128

/// Multiplication
let isize_mul = scalar_mul #Isize
let i8_mul = scalar_mul #I8
let i16_mul = scalar_mul #I16
let i32_mul = scalar_mul #I32
let i64_mul = scalar_mul #I64
let i128_mul = scalar_mul #I128
let usize_mul = scalar_mul #Usize
let u8_mul = scalar_mul #U8
let u16_mul = scalar_mul #U16
let u32_mul = scalar_mul #U32
let u64_mul = scalar_mul #U64
let u128_mul = scalar_mul #U128

(*** Range *)
type range (a : Type0) = {
  start : a;
  end_ : a;
}

(*** Array *)
type array (a : Type0) (n : usize) = s:list a{length s = n}

// We tried putting the normalize_term condition as a refinement on the list
// but it didn't work. It works with the requires clause.
let mk_array (a : Type0) (n : usize)
  (l : list a) :
  Pure (array a n)
  (requires (normalize_term(FStar.List.Tot.length l) = n))
  (ensures (fun _ -> True)) =
  normalize_term_spec (FStar.List.Tot.length l);
  l

let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a =
  if i < length x then Return (index x i)
  else Fail Failure

let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a =
  if i < length x then Return (index x i)
  else Fail Failure

let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) =
  if i < length x then Return (list_update x i nx)
  else Fail Failure

(*** Slice *)
type slice (a : Type0) = s:list a{length s <= usize_max}

let slice_len (a : Type0) (s : slice a) : usize = length s

let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a =
  if i < length x then Return (index x i)
  else Fail Failure

let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a =
  if i < length x then Return (index x i)
  else Fail Failure

let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) =
  if i < length x then Return (list_update x i nx)
  else Fail Failure

(*** Subslices *)

let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) =
  if length s = n then Return s
  else Fail Failure

// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *)
let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) =
  admit()

let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) =
  admit()

let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) =
  admit()

let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) =
  admit()

let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) =
  admit()

let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) =
  admit()

(*** Vector *)
type vec (a : Type0) = v:list a{length v <= usize_max}

let vec_new (a  : Type0) : vec a = assert_norm(length #a [] == 0); []
let vec_len (a : Type0) (v : vec a) : usize = length v

// The **forward** function shouldn't be used
let vec_push_fwd (a  : Type0) (v : vec a) (x : a) : unit = ()
let vec_push_back (a  : Type0) (v : vec a) (x : a) :
  Pure (result (vec a))
  (requires True)
  (ensures (fun res ->
    match res with
    | Fail e -> e == Failure
    | Return v' -> length v' = length v + 1)) =
  if length v < usize_max then begin
    (**) assert_norm(length [x] == 1);
    (**) append_length v [x];
    (**) assert(length (append v [x]) = length v + 1);
    Return (append v [x])
    end
  else Fail Failure

// The **forward** function shouldn't be used
let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
  if i < length v then Return () else Fail Failure
let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) =
  if i < length v then Return (list_update v i x) else Fail Failure

// The **backward** function shouldn't be used
let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a =
  if i < length v then Return (index v i) else Fail Failure
let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
  if i < length v then Return () else Fail Failure

let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a =
  if i < length v then Return (index v i) else Fail Failure
let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) =
  if i < length v then Return (list_update v i nx) else Fail Failure