summaryrefslogtreecommitdiff
path: root/tests/fstar/betree_back_stateful/Primitives.fst
blob: a3ffbde4b1838bdfc5d4bd9624df64e12ee36c75 (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
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
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
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
/// 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 core_mem_replace (a : Type0) (x : a) (y : a) : a = x
let core_mem_replace_back (a : Type0) (x : a) (y : a) : a = y

// We don't really use raw pointers for now
type mut_raw_ptr (t : Type0) = { v : t }
type const_raw_ptr (t : Type0) = { v : t }

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

assume val size_numbits : pos

// TODO: we could use FStar.Int.int_t and FStar.UInt.int_t

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 is_unsigned = function
  | Isize | I8 | I16 | I32 | I64 | I128 -> false
  | Usize | U8 | U16 | U32 | U64 | U128 -> true

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)

let scalar_xor (#ty : scalar_ty)
    (x : scalar ty) (y : scalar ty) : scalar ty =
  match ty with
  | U8 -> FStar.UInt.logxor #8 x y
  | U16 -> FStar.UInt.logxor #16 x y
  | U32 -> FStar.UInt.logxor #32 x y
  | U64 -> FStar.UInt.logxor #64 x y
  | U128 -> FStar.UInt.logxor #128 x y
  | Usize -> admit() // TODO
  | I8 ->
    // Encoding issues...
    normalize_spec (FStar.Int.int_t 8);
    normalize_spec (scalar I8);
    FStar.Int.logxor #8 x y
  | I16 ->
    // Encoding issues...
    normalize_spec (FStar.Int.int_t 16);
    normalize_spec (scalar I16);
    FStar.Int.logxor #16 x y
  | I32 -> FStar.Int.logxor #32 x y
  | I64 -> FStar.Int.logxor #64 x y
  | I128 ->
    // Encoding issues...
    normalize_spec (FStar.Int.int_t 128);
    normalize_spec (scalar I128);
    FStar.Int.logxor #128 x y
  | Isize -> admit() // TODO

let scalar_or (#ty : scalar_ty)
    (x : scalar ty) (y : scalar ty) : scalar ty =
  match ty with
  | U8 -> FStar.UInt.logor #8 x y
  | U16 -> FStar.UInt.logor #16 x y
  | U32 -> FStar.UInt.logor #32 x y
  | U64 -> FStar.UInt.logor #64 x y
  | U128 -> FStar.UInt.logor #128 x y
  | Usize -> admit() // TODO
  | I8 ->
    // Encoding issues...
    normalize_spec (FStar.Int.int_t 8);
    normalize_spec (scalar I8);
    FStar.Int.logor #8 x y
  | I16 ->
    // Encoding issues...
    normalize_spec (FStar.Int.int_t 16);
    normalize_spec (scalar I16);
    FStar.Int.logor #16 x y
  | I32 -> FStar.Int.logor #32 x y
  | I64 -> FStar.Int.logor #64 x y
  | I128 ->
    // Encoding issues...
    normalize_spec (FStar.Int.int_t 128);
    normalize_spec (scalar I128);
    FStar.Int.logor #128 x y
  | Isize -> admit() // TODO

let scalar_and (#ty : scalar_ty)
    (x : scalar ty) (y : scalar ty) : scalar ty =
  match ty with
  | U8 -> FStar.UInt.logand #8 x y
  | U16 -> FStar.UInt.logand #16 x y
  | U32 -> FStar.UInt.logand #32 x y
  | U64 -> FStar.UInt.logand #64 x y
  | U128 -> FStar.UInt.logand #128 x y
  | Usize -> admit() // TODO
  | I8 ->
    // Encoding issues...
    normalize_spec (FStar.Int.int_t 8);
    normalize_spec (scalar I8);
    FStar.Int.logand #8 x y
  | I16 ->
    // Encoding issues...
    normalize_spec (FStar.Int.int_t 16);
    normalize_spec (scalar I16);
    FStar.Int.logand #16 x y
  | I32 -> FStar.Int.logand #32 x y
  | I64 -> FStar.Int.logand #64 x y
  | I128 ->
    // Encoding issues...
    normalize_spec (FStar.Int.int_t 128);
    normalize_spec (scalar I128);
    FStar.Int.logand #128 x y
  | Isize -> admit() // TODO

// Shift left
let scalar_shl (#ty0 #ty1 : scalar_ty)
    (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
  admit()

// Shift right
let scalar_shr (#ty0 #ty1 : scalar_ty)
    (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
  admit()

(** 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

// This can't fail, but for now we make all casts faillible (easier for the translation)
let scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) =
  mk_scalar tgt_ty (if x then 1 else 0)

/// 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

/// Subtraction
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

/// Xor
let u8_xor = scalar_xor #U8
let u16_xor = scalar_xor #U16
let u32_xor = scalar_xor #U32
let u64_xor = scalar_xor #U64
let u128_xor = scalar_xor #U128
let usize_xor = scalar_xor #Usize
let i8_xor = scalar_xor #I8
let i16_xor = scalar_xor #I16
let i32_xor = scalar_xor #I32
let i64_xor = scalar_xor #I64
let i128_xor = scalar_xor #I128
let isize_xor = scalar_xor #Isize

/// Or
let u8_or = scalar_or #U8
let u16_or = scalar_or #U16
let u32_or = scalar_or #U32
let u64_or = scalar_or #U64
let u128_or = scalar_or #U128
let usize_or = scalar_or #Usize
let i8_or = scalar_or #I8
let i16_or = scalar_or #I16
let i32_or = scalar_or #I32
let i64_or = scalar_or #I64
let i128_or = scalar_or #I128
let isize_or = scalar_or #Isize

/// And
let u8_and = scalar_and #U8
let u16_and = scalar_and #U16
let u32_and = scalar_and #U32
let u64_and = scalar_and #U64
let u128_and = scalar_and #U128
let usize_and = scalar_and #Usize
let i8_and = scalar_and #I8
let i16_and = scalar_and #I16
let i32_and = scalar_and #I32
let i64_and = scalar_and #I64
let i128_and = scalar_and #I128
let isize_and = scalar_and #Isize

/// Shift left
let u8_shl #ty = scalar_shl #U8 #ty
let u16_shl #ty = scalar_shl #U16 #ty
let u32_shl #ty = scalar_shl #U32 #ty
let u64_shl #ty = scalar_shl #U64 #ty
let u128_shl #ty = scalar_shl #U128 #ty
let usize_shl #ty = scalar_shl #Usize #ty
let i8_shl #ty = scalar_shl #I8 #ty
let i16_shl #ty = scalar_shl #I16 #ty
let i32_shl #ty = scalar_shl #I32 #ty
let i64_shl #ty = scalar_shl #I64 #ty
let i128_shl #ty = scalar_shl #I128 #ty
let isize_shl #ty = scalar_shl #Isize #ty

/// Shift right
let u8_shr #ty = scalar_shr #U8 #ty
let u16_shr #ty = scalar_shr #U16 #ty
let u32_shr #ty = scalar_shr #U32 #ty
let u64_shr #ty = scalar_shr #U64 #ty
let u128_shr #ty = scalar_shr #U128 #ty
let usize_shr #ty = scalar_shr #Usize #ty
let i8_shr #ty = scalar_shr #I8 #ty
let i16_shr #ty = scalar_shr #I16 #ty
let i32_shr #ty = scalar_shr #I32 #ty
let i64_shr #ty = scalar_shr #I64 #ty
let i128_shr #ty = scalar_shr #I128 #ty
let isize_shr #ty = scalar_shr #Isize #ty

(*** core::ops *)

// Trait declaration: [core::ops::index::Index]
noeq type core_ops_index_Index (self idx : Type0) = {
  output : Type0;
  index : self  idx  result output
}

// Trait declaration: [core::ops::index::IndexMut]
noeq type core_ops_index_IndexMut (self idx : Type0) = {
  indexInst : core_ops_index_Index self idx;
  index_mut : self  idx  result indexInst.output;
  index_mut_back : self  idx  indexInst.output  result self;
}

// Trait declaration [core::ops::deref::Deref]
noeq type core_ops_deref_Deref (self : Type0) = {
  target : Type0;
  deref : self  result target;
}

// Trait declaration [core::ops::deref::DerefMut]
noeq type core_ops_deref_DerefMut (self : Type0) = {
  derefInst : core_ops_deref_Deref self;
  deref_mut : self  result derefInst.target;
  deref_mut_back : self  derefInst.target  result self;
}

type core_ops_range_Range (a : Type0) = {
  start : a;
  end_ : a;
}

(*** [alloc] *)

let alloc_boxed_Box_deref (t : Type0) (x : t) : result t = Return x
let alloc_boxed_Box_deref_mut (t : Type0) (x : t) : result t = Return x
let alloc_boxed_Box_deref_mut_back (t : Type) (_ : t) (x : t) : result t = Return x

// Trait instance
let alloc_boxed_Box_coreopsDerefInst (self : Type0) : core_ops_deref_Deref self = {
  target = self;
  deref = alloc_boxed_Box_deref self;
}

// Trait instance
let alloc_boxed_Box_coreopsDerefMutInst (self : Type0) : core_ops_deref_DerefMut self = {
  derefInst = alloc_boxed_Box_coreopsDerefInst self;
  deref_mut = alloc_boxed_Box_deref_mut self;
  deref_mut_back = alloc_boxed_Box_deref_mut_back self;
}

(*** 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_usize (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_update_usize (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_usize (a : Type0) (x : slice a) (i : usize) : result a =
  if i < length x then Return (index x i)
  else Fail Failure

let slice_update_usize (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 (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x
let array_from_slice (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 (a : Type0) (n : usize) (x : array a n) (r : core_ops_range_Range usize) : result (slice a) =
  admit()

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

let array_repeat (a : Type0) (n : usize) (x : a) : array a n =
  admit()

let slice_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) : result (slice a) =
  admit()

let slice_update_subslice (a : Type0) (x : slice a) (r : core_ops_range_Range usize) (ns : slice a) : result (slice a) =
  admit()

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

let alloc_vec_Vec_new (a  : Type0) : alloc_vec_Vec a = assert_norm(length #a [] == 0); []
let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v

// Helper
let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a =
  if i < length v then Return (index v i) else Fail Failure
// Helper
let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
  if i < length v then Return (list_update v i x) else Fail Failure

// The **forward** function shouldn't be used
let alloc_vec_Vec_push_fwd (a  : Type0) (v : alloc_vec_Vec a) (x : a) : unit = ()
let alloc_vec_Vec_push (a  : Type0) (v : alloc_vec_Vec a) (x : a) :
  Pure (result (alloc_vec_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 alloc_vec_Vec_insert_fwd (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result unit =
  if i < length v then Return () else Fail Failure
let alloc_vec_Vec_insert (a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) =
  if i < length v then Return (list_update v i x) else Fail Failure

// Trait declaration: [core::slice::index::private_slice_index::Sealed]
type core_slice_index_private_slice_index_Sealed (self : Type0) = unit

// Trait declaration: [core::slice::index::SliceIndex]
noeq type core_slice_index_SliceIndex (self t : Type0) = {
  sealedInst : core_slice_index_private_slice_index_Sealed self;
  output : Type0;
  get : self  t  result (option output);
  get_mut : self  t  result (option output);
  get_mut_back : self  t  option output  result t;
  get_unchecked : self  const_raw_ptr t  result (const_raw_ptr output);
  get_unchecked_mut : self  mut_raw_ptr t  result (mut_raw_ptr output);
  index : self  t  result output;
  index_mut : self  t  result output;
  index_mut_back : self  t  output  result t;
}

// [core::slice::index::[T]::index]: forward function
let core_slice_index_Slice_index
  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
  (s : slice t) (i : idx) : result inst.output =
  let* x = inst.get i s in
  match x with
  | None -> Fail Failure
  | Some x -> Return x

// [core::slice::index::Range:::get]: forward function
let core_slice_index_RangeUsize_get (t : Type0) (i : core_ops_range_Range usize) (s : slice t) :
  result (option (slice t)) =
  admit () // TODO

// [core::slice::index::Range::get_mut]: forward function
let core_slice_index_RangeUsize_get_mut
  (t : Type0) : core_ops_range_Range usize  slice t  result (option (slice t)) =
  admit () // TODO

// [core::slice::index::Range::get_mut]: backward function 0
let core_slice_index_RangeUsize_get_mut_back
  (t : Type0) :
  core_ops_range_Range usize  slice t  option (slice t)  result (slice t) =
  admit () // TODO

// [core::slice::index::Range::get_unchecked]: forward function
let core_slice_index_RangeUsize_get_unchecked
  (t : Type0) :
  core_ops_range_Range usize  const_raw_ptr (slice t)  result (const_raw_ptr (slice t)) =
  // Don't know what the model should be - for now we always fail to make
  // sure code which uses it fails
  fun _ _ -> Fail Failure

// [core::slice::index::Range::get_unchecked_mut]: forward function
let core_slice_index_RangeUsize_get_unchecked_mut
  (t : Type0) :
  core_ops_range_Range usize  mut_raw_ptr (slice t)  result (mut_raw_ptr (slice t)) =
  // Don't know what the model should be - for now we always fail to make
  // sure code which uses it fails
  fun _ _ -> Fail Failure

// [core::slice::index::Range::index]: forward function
let core_slice_index_RangeUsize_index
  (t : Type0) : core_ops_range_Range usize  slice t  result (slice t) =
  admit () // TODO

// [core::slice::index::Range::index_mut]: forward function
let core_slice_index_RangeUsize_index_mut
  (t : Type0) : core_ops_range_Range usize  slice t  result (slice t) =
  admit () // TODO

// [core::slice::index::Range::index_mut]: backward function 0
let core_slice_index_RangeUsize_index_mut_back
  (t : Type0) : core_ops_range_Range usize  slice t  slice t  result (slice t) =
  admit () // TODO

// [core::slice::index::[T]::index_mut]: forward function
let core_slice_index_Slice_index_mut
  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
  slice t  idx  result inst.output =
  admit () // 

// [core::slice::index::[T]::index_mut]: backward function 0
let core_slice_index_Slice_index_mut_back
  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t)) :
  slice t  idx  inst.output  result (slice t) =
  admit () // TODO

// [core::array::[T; N]::index]: forward function
let core_array_Array_index
  (t idx : Type0) (n : usize) (inst : core_ops_index_Index (slice t) idx)
  (a : array t n) (i : idx) : result inst.output =
  admit () // TODO

// [core::array::[T; N]::index_mut]: forward function
let core_array_Array_index_mut
  (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
  (a : array t n) (i : idx) : result inst.indexInst.output =
  admit () // TODO

// [core::array::[T; N]::index_mut]: backward function 0
let core_array_Array_index_mut_back
  (t idx : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) idx)
  (a : array t n) (i : idx) (x : inst.indexInst.output) : result (array t n) =
  admit () // TODO

// Trait implementation: [core::slice::index::private_slice_index::Range]
let core_slice_index_private_slice_index_SealedRangeUsizeInst
  : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) = ()

// Trait implementation: [core::slice::index::Range]
let core_slice_index_SliceIndexRangeUsizeSliceTInst (t : Type0) :
  core_slice_index_SliceIndex (core_ops_range_Range usize) (slice t) = {
  sealedInst = core_slice_index_private_slice_index_SealedRangeUsizeInst;
  output = slice t;
  get = core_slice_index_RangeUsize_get t;
  get_mut = core_slice_index_RangeUsize_get_mut t;
  get_mut_back = core_slice_index_RangeUsize_get_mut_back t;
  get_unchecked = core_slice_index_RangeUsize_get_unchecked t;
  get_unchecked_mut = core_slice_index_RangeUsize_get_unchecked_mut t;
  index = core_slice_index_RangeUsize_index t;
  index_mut = core_slice_index_RangeUsize_index_mut t;
  index_mut_back = core_slice_index_RangeUsize_index_mut_back t;
}

// Trait implementation: [core::slice::index::[T]]
let core_ops_index_IndexSliceTIInst (t idx : Type0)
  (inst : core_slice_index_SliceIndex idx (slice t)) :
  core_ops_index_Index (slice t) idx = {
  output = inst.output;
  index = core_slice_index_Slice_index t idx inst;
}

// Trait implementation: [core::slice::index::[T]]
let core_ops_index_IndexMutSliceTIInst (t idx : Type0)
  (inst : core_slice_index_SliceIndex idx (slice t)) :
  core_ops_index_IndexMut (slice t) idx = {
  indexInst = core_ops_index_IndexSliceTIInst t idx inst;
  index_mut = core_slice_index_Slice_index_mut t idx inst;
  index_mut_back = core_slice_index_Slice_index_mut_back t idx inst;
}

// Trait implementation: [core::array::[T; N]]
let core_ops_index_IndexArrayInst (t idx : Type0) (n : usize)
  (inst : core_ops_index_Index (slice t) idx) :
  core_ops_index_Index (array t n) idx = {
  output = inst.output;
  index = core_array_Array_index t idx n inst;
}

// Trait implementation: [core::array::[T; N]]
let core_ops_index_IndexMutArrayIInst (t idx : Type0) (n : usize)
  (inst : core_ops_index_IndexMut (slice t) idx) :
  core_ops_index_IndexMut (array t n) idx = {
  indexInst = core_ops_index_IndexArrayInst t idx n inst.indexInst;
  index_mut = core_array_Array_index_mut t idx n inst;
  index_mut_back = core_array_Array_index_mut_back t idx n inst;
}

// [core::slice::index::usize::get]: forward function
let core_slice_index_usize_get
  (t : Type0) : usize  slice t  result (option t) =
  admit () // TODO

// [core::slice::index::usize::get_mut]: forward function
let core_slice_index_usize_get_mut
  (t : Type0) : usize  slice t  result (option t) =
  admit () // TODO

// [core::slice::index::usize::get_mut]: backward function 0
let core_slice_index_usize_get_mut_back
  (t : Type0) : usize  slice t  option t  result (slice t) =
  admit () // TODO

// [core::slice::index::usize::get_unchecked]: forward function
let core_slice_index_usize_get_unchecked
  (t : Type0) : usize  const_raw_ptr (slice t)  result (const_raw_ptr t) =
  admit () // TODO

// [core::slice::index::usize::get_unchecked_mut]: forward function
let core_slice_index_usize_get_unchecked_mut
  (t : Type0) : usize  mut_raw_ptr (slice t)  result (mut_raw_ptr t) =
  admit () // TODO

// [core::slice::index::usize::index]: forward function
let core_slice_index_usize_index (t : Type0) : usize  slice t  result t =
  admit () // TODO

// [core::slice::index::usize::index_mut]: forward function
let core_slice_index_usize_index_mut (t : Type0) : usize  slice t  result t =
  admit () // TODO

// [core::slice::index::usize::index_mut]: backward function 0
let core_slice_index_usize_index_mut_back
  (t : Type0) : usize  slice t  t  result (slice t) =
  admit () // TODO

// Trait implementation: [core::slice::index::private_slice_index::usize]
let core_slice_index_private_slice_index_SealedUsizeInst
  : core_slice_index_private_slice_index_Sealed usize = ()

// Trait implementation: [core::slice::index::usize]
let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) :
  core_slice_index_SliceIndex usize (slice t) = {
  sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
  output = t;
  get = core_slice_index_usize_get t;
  get_mut = core_slice_index_usize_get_mut t;
  get_mut_back = core_slice_index_usize_get_mut_back t;
  get_unchecked = core_slice_index_usize_get_unchecked t;
  get_unchecked_mut = core_slice_index_usize_get_unchecked_mut t;
  index = core_slice_index_usize_index t;
  index_mut = core_slice_index_usize_index_mut t;
  index_mut_back = core_slice_index_usize_index_mut_back t;
}

// [alloc::vec::Vec::index]: forward function
let alloc_vec_Vec_index (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
  (self : alloc_vec_Vec t) (i : idx) : result inst.output =
  admit () // TODO

// [alloc::vec::Vec::index_mut]: forward function
let alloc_vec_Vec_index_mut (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
  (self : alloc_vec_Vec t) (i : idx) : result inst.output =
  admit () // TODO

// [alloc::vec::Vec::index_mut]: backward function 0
let alloc_vec_Vec_index_mut_back
  (t idx : Type0) (inst : core_slice_index_SliceIndex idx (slice t))
  (self : alloc_vec_Vec t) (i : idx) (x : inst.output) : result (alloc_vec_Vec t) =
  admit () // TODO

// Trait implementation: [alloc::vec::Vec]
let alloc_vec_Vec_coreopsindexIndexInst (t idx : Type0)
  (inst : core_slice_index_SliceIndex idx (slice t)) :
  core_ops_index_Index (alloc_vec_Vec t) idx = {
  output = inst.output;
  index = alloc_vec_Vec_index t idx inst;
}

// Trait implementation: [alloc::vec::Vec]
let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
  (inst : core_slice_index_SliceIndex idx (slice t)) :
  core_ops_index_IndexMut (alloc_vec_Vec t) idx = {
  indexInst = alloc_vec_Vec_coreopsindexIndexInst t idx inst;
  index_mut = alloc_vec_Vec_index_mut t idx inst;
  index_mut_back = alloc_vec_Vec_index_mut_back t idx inst;
}

(*** Theorems *)

let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
  Lemma (
    alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
      alloc_vec_Vec_index_usize v i)
  [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
  =
  admit()

let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
  Lemma (
    alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
      alloc_vec_Vec_index_usize v i)
  [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
  =
  admit()

let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
  Lemma (
    alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x ==
      alloc_vec_Vec_update_usize v i x)
  [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x)]
  =
  admit()