Start tracking the automatically generated/copied files for hashmap

3 files changed, 963 insertions, 0 deletions

diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
new file mode 100644
index 00000000..3828ae98
--- /dev/null
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -0,0 +1,663 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap]: function definitions *)
+module Hashmap.Funs
+open Primitives
+include Hashmap.Types
+include Hashmap.Clauses
+
+#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+
+(** [hashmap::hash_key] *)
+let hash_key_fwd (k : usize) : result usize = Return k
+
+(** [hashmap::HashMap::allocate_slots] *)
+let rec hash_map_allocate_slots_fwd
+  (t : Type0) (slots : vec (list_t t)) (n : usize) :
+  Tot (result (vec (list_t t)))
+  (decreases (hash_map_allocate_slots_decreases t slots n))
+  =
+  begin match n with
+  | 0 -> Return slots
+  | _ ->
+    begin match vec_push_back (list_t t) slots ListNil with
+    | Fail -> Fail
+    | Return v ->
+      begin match usize_sub n 1 with
+      | Fail -> Fail
+      | Return i ->
+        begin match hash_map_allocate_slots_fwd t v i with
+        | Fail -> Fail
+        | Return v0 -> Return v0
+        end
+      end
+    end
+  end
+
+(** [hashmap::HashMap::new_with_capacity] *)
+let hash_map_new_with_capacity_fwd
+  (t : Type0) (capacity : usize) (max_load_dividend : usize)
+  (max_load_divisor : usize) :
+  result (hash_map_t t)
+  =
+  let v = vec_new (list_t t) in
+  begin match hash_map_allocate_slots_fwd t v capacity with
+  | Fail -> Fail
+  | Return v0 ->
+    begin match usize_mul capacity max_load_dividend with
+    | Fail -> Fail
+    | Return i ->
+      begin match usize_div i max_load_divisor with
+      | Fail -> Fail
+      | Return i0 ->
+        Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 v0)
+      end
+    end
+  end
+
+(** [hashmap::HashMap::new] *)
+let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
+  begin match hash_map_new_with_capacity_fwd t 32 4 5 with
+  | Fail -> Fail
+  | Return h -> Return h
+  end
+
+(** [hashmap::HashMap::clear_slots] *)
+let rec hash_map_clear_slots_fwd_back
+  (t : Type0) (slots : vec (list_t t)) (i : usize) :
+  Tot (result (vec (list_t t)))
+  (decreases (hash_map_clear_slots_decreases t slots i))
+  =
+  let i0 = vec_len (list_t t) slots in
+  let b = i < i0 in
+  if b
+  then
+    begin match vec_index_mut_back (list_t t) slots i ListNil with
+    | Fail -> Fail
+    | Return v ->
+      begin match usize_add i 1 with
+      | Fail -> Fail
+      | Return i1 ->
+        begin match hash_map_clear_slots_fwd_back t v i1 with
+        | Fail -> Fail
+        | Return v0 -> Return v0
+        end
+      end
+    end
+  else Return slots
+
+(** [hashmap::HashMap::clear] *)
+let hash_map_clear_fwd_back
+  (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
+  let p = self.hash_map_max_load_factor in
+  let i = self.hash_map_max_load in
+  let v = self.hash_map_slots in
+  begin match hash_map_clear_slots_fwd_back t v 0 with
+  | Fail -> Fail
+  | Return v0 -> let self0 = Mkhash_map_t 0 p i v0 in Return self0
+  end
+
+(** [hashmap::HashMap::len] *)
+let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
+  let i = self.hash_map_num_entries in Return i
+
+(** [hashmap::HashMap::insert_in_list] *)
+let rec hash_map_insert_in_list_fwd
+  (t : Type0) (key : usize) (value : t) (ls : list_t t) :
+  Tot (result bool)
+  (decreases (hash_map_insert_in_list_decreases t key value ls))
+  =
+  begin match ls with
+  | ListCons ckey cvalue ls0 ->
+    let b = ckey = key in
+    if b
+    then Return false
+    else
+      begin match hash_map_insert_in_list_fwd t key value ls0 with
+      | Fail -> Fail
+      | Return b0 -> Return b0
+      end
+  | ListNil -> Return true
+  end
+
+(** [hashmap::HashMap::insert_in_list] *)
+let rec hash_map_insert_in_list_back
+  (t : Type0) (key : usize) (value : t) (ls : list_t t) :
+  Tot (result (list_t t))
+  (decreases (hash_map_insert_in_list_decreases t key value ls))
+  =
+  begin match ls with
+  | ListCons ckey cvalue ls0 ->
+    let b = ckey = key in
+    if b
+    then let ls1 = ListCons ckey value ls0 in Return ls1
+    else
+      begin match hash_map_insert_in_list_back t key value ls0 with
+      | Fail -> Fail
+      | Return l -> let ls1 = ListCons ckey cvalue l in Return ls1
+      end
+  | ListNil -> let l = ListNil in let ls0 = ListCons key value l in Return ls0
+  end
+
+(** [hashmap::HashMap::insert_no_resize] *)
+let hash_map_insert_no_resize_fwd_back
+  (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
+  result (hash_map_t t)
+  =
+  begin match hash_key_fwd key with
+  | Fail -> Fail
+  | Return i ->
+    let i0 = self.hash_map_num_entries in
+    let p = self.hash_map_max_load_factor in
+    let i1 = self.hash_map_max_load in
+    let v = self.hash_map_slots in
+    let i2 = vec_len (list_t t) v in
+    begin match usize_rem i i2 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match vec_index_mut_fwd (list_t t) v hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hash_map_insert_in_list_fwd t key value l with
+        | Fail -> Fail
+        | Return b ->
+          if b
+          then
+            begin match usize_add i0 1 with
+            | Fail -> Fail
+            | Return i3 ->
+              begin match hash_map_insert_in_list_back t key value l with
+              | Fail -> Fail
+              | Return l0 ->
+                begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+                | Fail -> Fail
+                | Return v0 ->
+                  let self0 = Mkhash_map_t i3 p i1 v0 in Return self0
+                end
+              end
+            end
+          else
+            begin match hash_map_insert_in_list_back t key value l with
+            | Fail -> Fail
+            | Return l0 ->
+              begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+              | Fail -> Fail
+              | Return v0 ->
+                let self0 = Mkhash_map_t i0 p i1 v0 in Return self0
+              end
+            end
+        end
+      end
+    end
+  end
+
+(** [hashmap::HashMap::move_elements_from_list] *)
+let rec hash_map_move_elements_from_list_fwd_back
+  (t : Type0) (ntable : hash_map_t t) (ls : list_t t) :
+  Tot (result (hash_map_t t))
+  (decreases (hash_map_move_elements_from_list_decreases t ntable ls))
+  =
+  begin match ls with
+  | ListCons k v tl ->
+    begin match hash_map_insert_no_resize_fwd_back t ntable k v with
+    | Fail -> Fail
+    | Return h ->
+      begin match hash_map_move_elements_from_list_fwd_back t h tl with
+      | Fail -> Fail
+      | Return h0 -> Return h0
+      end
+    end
+  | ListNil -> Return ntable
+  end
+
+(** [hashmap::HashMap::move_elements] *)
+let rec hash_map_move_elements_fwd_back
+  (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
+  Tot (result ((hash_map_t t) & (vec (list_t t))))
+  (decreases (hash_map_move_elements_decreases t ntable slots i))
+  =
+  let i0 = vec_len (list_t t) slots in
+  let b = i < i0 in
+  if b
+  then
+    begin match vec_index_mut_fwd (list_t t) slots i with
+    | Fail -> Fail
+    | Return l ->
+      let l0 = mem_replace_fwd (list_t t) l ListNil in
+      begin match hash_map_move_elements_from_list_fwd_back t ntable l0 with
+      | Fail -> Fail
+      | Return h ->
+        let l1 = mem_replace_back (list_t t) l ListNil in
+        begin match vec_index_mut_back (list_t t) slots i l1 with
+        | Fail -> Fail
+        | Return v ->
+          begin match usize_add i 1 with
+          | Fail -> Fail
+          | Return i1 ->
+            begin match hash_map_move_elements_fwd_back t h v i1 with
+            | Fail -> Fail
+            | Return (h0, v0) -> Return (h0, v0)
+            end
+          end
+        end
+      end
+    end
+  else Return (ntable, slots)
+
+(** [hashmap::HashMap::try_resize] *)
+let hash_map_try_resize_fwd_back
+  (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
+  let i = self.hash_map_num_entries in
+  let p = self.hash_map_max_load_factor in
+  let i0 = self.hash_map_max_load in
+  let v = self.hash_map_slots in
+  let i1 = vec_len (list_t t) v in
+  begin match usize_div 4294967295 2 with
+  | Fail -> Fail
+  | Return n1 ->
+    let (i2, i3) = p in
+    begin match usize_div n1 i2 with
+    | Fail -> Fail
+    | Return i4 ->
+      let b = i1 <= i4 in
+      if b
+      then
+        begin match usize_mul i1 2 with
+        | Fail -> Fail
+        | Return i5 ->
+          begin match hash_map_new_with_capacity_fwd t i5 i2 i3 with
+          | Fail -> Fail
+          | Return h ->
+            begin match hash_map_move_elements_fwd_back t h v 0 with
+            | Fail -> Fail
+            | Return (h0, v0) ->
+              let i6 = h0.hash_map_max_load in
+              let v1 = h0.hash_map_slots in
+              let v2 = mem_replace_back (vec (list_t t)) v0 v1 in
+              let self0 = Mkhash_map_t i (i2, i3) i6 v2 in
+              Return
+              self0
+            end
+          end
+        end
+      else let self0 = Mkhash_map_t i (i2, i3) i0 v in Return self0
+    end
+  end
+
+(** [hashmap::HashMap::insert] *)
+let hash_map_insert_fwd_back
+  (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
+  result (hash_map_t t)
+  =
+  begin match hash_map_insert_no_resize_fwd_back t self key value with
+  | Fail -> Fail
+  | Return h ->
+    begin match hash_map_len_fwd t h with
+    | Fail -> Fail
+    | Return i ->
+      let i0 = h.hash_map_num_entries in
+      let p = h.hash_map_max_load_factor in
+      let i1 = h.hash_map_max_load in
+      let v = h.hash_map_slots in
+      let b = i > i1 in
+      if b
+      then
+        begin match hash_map_try_resize_fwd_back t (Mkhash_map_t i0 p i1 v)
+          with
+        | Fail -> Fail
+        | Return h0 -> Return h0
+        end
+      else let self0 = Mkhash_map_t i0 p i1 v in Return self0
+    end
+  end
+
+(** [hashmap::HashMap::get_in_list] *)
+let rec hash_map_get_in_list_fwd
+  (t : Type0) (key : usize) (ls : list_t t) :
+  Tot (result t) (decreases (hash_map_get_in_list_decreases t key ls))
+  =
+  begin match ls with
+  | ListCons ckey cvalue ls0 ->
+    let b = ckey = key in
+    if b
+    then Return cvalue
+    else
+      begin match hash_map_get_in_list_fwd t key ls0 with
+      | Fail -> Fail
+      | Return x -> Return x
+      end
+  | ListNil -> Fail
+  end
+
+(** [hashmap::HashMap::get] *)
+let hash_map_get_fwd
+  (t : Type0) (self : hash_map_t t) (key : usize) : result t =
+  begin match hash_key_fwd key with
+  | Fail -> Fail
+  | Return i ->
+    let v = self.hash_map_slots in
+    let i0 = vec_len (list_t t) v in
+    begin match usize_rem i i0 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match vec_index_fwd (list_t t) v hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hash_map_get_in_list_fwd t key l with
+        | Fail -> Fail
+        | Return x -> Return x
+        end
+      end
+    end
+  end
+
+(** [hashmap::HashMap::get_mut_in_list] *)
+let rec hash_map_get_mut_in_list_fwd
+  (t : Type0) (key : usize) (ls : list_t t) :
+  Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls))
+  =
+  begin match ls with
+  | ListCons ckey cvalue ls0 ->
+    let b = ckey = key in
+    if b
+    then Return cvalue
+    else
+      begin match hash_map_get_mut_in_list_fwd t key ls0 with
+      | Fail -> Fail
+      | Return x -> Return x
+      end
+  | ListNil -> Fail
+  end
+
+(** [hashmap::HashMap::get_mut_in_list] *)
+let rec hash_map_get_mut_in_list_back
+  (t : Type0) (key : usize) (ls : list_t t) (ret : t) :
+  Tot (result (list_t t))
+  (decreases (hash_map_get_mut_in_list_decreases t key ls))
+  =
+  begin match ls with
+  | ListCons ckey cvalue ls0 ->
+    let b = ckey = key in
+    if b
+    then let ls1 = ListCons ckey ret ls0 in Return ls1
+    else
+      begin match hash_map_get_mut_in_list_back t key ls0 ret with
+      | Fail -> Fail
+      | Return l -> let ls1 = ListCons ckey cvalue l in Return ls1
+      end
+  | ListNil -> Fail
+  end
+
+(** [hashmap::HashMap::get_mut] *)
+let hash_map_get_mut_fwd
+  (t : Type0) (self : hash_map_t t) (key : usize) : result t =
+  begin match hash_key_fwd key with
+  | Fail -> Fail
+  | Return i ->
+    let v = self.hash_map_slots in
+    let i0 = vec_len (list_t t) v in
+    begin match usize_rem i i0 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match vec_index_mut_fwd (list_t t) v hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hash_map_get_mut_in_list_fwd t key l with
+        | Fail -> Fail
+        | Return x -> Return x
+        end
+      end
+    end
+  end
+
+(** [hashmap::HashMap::get_mut] *)
+let hash_map_get_mut_back
+  (t : Type0) (self : hash_map_t t) (key : usize) (ret : t) :
+  result (hash_map_t t)
+  =
+  begin match hash_key_fwd key with
+  | Fail -> Fail
+  | Return i ->
+    let i0 = self.hash_map_num_entries in
+    let p = self.hash_map_max_load_factor in
+    let i1 = self.hash_map_max_load in
+    let v = self.hash_map_slots in
+    let i2 = vec_len (list_t t) v in
+    begin match usize_rem i i2 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match vec_index_mut_fwd (list_t t) v hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hash_map_get_mut_in_list_back t key l ret with
+        | Fail -> Fail
+        | Return l0 ->
+          begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+          | Fail -> Fail
+          | Return v0 -> let self0 = Mkhash_map_t i0 p i1 v0 in Return self0
+          end
+        end
+      end
+    end
+  end
+
+(** [hashmap::HashMap::remove_from_list] *)
+let rec hash_map_remove_from_list_fwd
+  (t : Type0) (key : usize) (ls : list_t t) :
+  Tot (result (option t))
+  (decreases (hash_map_remove_from_list_decreases t key ls))
+  =
+  begin match ls with
+  | ListCons ckey x tl ->
+    let b = ckey = key in
+    if b
+    then
+      let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
+      begin match mv_ls with
+      | ListCons i cvalue tl0 -> Return (Some cvalue)
+      | ListNil -> Fail
+      end
+    else
+      begin match hash_map_remove_from_list_fwd t key tl with
+      | Fail -> Fail
+      | Return opt -> Return opt
+      end
+  | ListNil -> Return None
+  end
+
+(** [hashmap::HashMap::remove_from_list] *)
+let rec hash_map_remove_from_list_back
+  (t : Type0) (key : usize) (ls : list_t t) :
+  Tot (result (list_t t))
+  (decreases (hash_map_remove_from_list_decreases t key ls))
+  =
+  begin match ls with
+  | ListCons ckey x tl ->
+    let b = ckey = key in
+    if b
+    then
+      let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
+      begin match mv_ls with
+      | ListCons i cvalue tl0 -> Return tl0
+      | ListNil -> Fail
+      end
+    else
+      begin match hash_map_remove_from_list_back t key tl with
+      | Fail -> Fail
+      | Return l -> let ls0 = ListCons ckey x l in Return ls0
+      end
+  | ListNil -> let ls0 = ListNil in Return ls0
+  end
+
+(** [hashmap::HashMap::remove] *)
+let hash_map_remove_fwd
+  (t : Type0) (self : hash_map_t t) (key : usize) : result (option t) =
+  begin match hash_key_fwd key with
+  | Fail -> Fail
+  | Return i ->
+    let i0 = self.hash_map_num_entries in
+    let v = self.hash_map_slots in
+    let i1 = vec_len (list_t t) v in
+    begin match usize_rem i i1 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match vec_index_mut_fwd (list_t t) v hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hash_map_remove_from_list_fwd t key l with
+        | Fail -> Fail
+        | Return x ->
+          begin match x with
+          | None -> Return None
+          | Some x0 ->
+            begin match usize_sub i0 1 with
+            | Fail -> Fail
+            | Return _ -> Return (Some x0)
+            end
+          end
+        end
+      end
+    end
+  end
+
+(** [hashmap::HashMap::remove] *)
+let hash_map_remove_back
+  (t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) =
+  begin match hash_key_fwd key with
+  | Fail -> Fail
+  | Return i ->
+    let i0 = self.hash_map_num_entries in
+    let p = self.hash_map_max_load_factor in
+    let i1 = self.hash_map_max_load in
+    let v = self.hash_map_slots in
+    let i2 = vec_len (list_t t) v in
+    begin match usize_rem i i2 with
+    | Fail -> Fail
+    | Return hash_mod ->
+      begin match vec_index_mut_fwd (list_t t) v hash_mod with
+      | Fail -> Fail
+      | Return l ->
+        begin match hash_map_remove_from_list_fwd t key l with
+        | Fail -> Fail
+        | Return x ->
+          begin match x with
+          | None ->
+            begin match hash_map_remove_from_list_back t key l with
+            | Fail -> Fail
+            | Return l0 ->
+              begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+              | Fail -> Fail
+              | Return v0 ->
+                let self0 = Mkhash_map_t i0 p i1 v0 in Return self0
+              end
+            end
+          | Some x0 ->
+            begin match usize_sub i0 1 with
+            | Fail -> Fail
+            | Return i3 ->
+              begin match hash_map_remove_from_list_back t key l with
+              | Fail -> Fail
+              | Return l0 ->
+                begin match vec_index_mut_back (list_t t) v hash_mod l0 with
+                | Fail -> Fail
+                | Return v0 ->
+                  let self0 = Mkhash_map_t i3 p i1 v0 in Return self0
+                end
+              end
+            end
+          end
+        end
+      end
+    end
+  end
+
+(** [hashmap::test1] *)
+let test1_fwd : result unit =
+  begin match hash_map_new_fwd u64 with
+  | Fail -> Fail
+  | Return h ->
+    begin match hash_map_insert_fwd_back u64 h 0 42 with
+    | Fail -> Fail
+    | Return h0 ->
+      begin match hash_map_insert_fwd_back u64 h0 128 18 with
+      | Fail -> Fail
+      | Return h1 ->
+        begin match hash_map_insert_fwd_back u64 h1 1024 138 with
+        | Fail -> Fail
+        | Return h2 ->
+          begin match hash_map_insert_fwd_back u64 h2 1056 256 with
+          | Fail -> Fail
+          | Return h3 ->
+            begin match hash_map_get_fwd u64 h3 128 with
+            | Fail -> Fail
+            | Return i ->
+              let b = i = 18 in
+              let b0 = not b in
+              if b0
+              then Fail
+              else
+                begin match hash_map_get_mut_back u64 h3 1024 56 with
+                | Fail -> Fail
+                | Return h4 ->
+                  begin match hash_map_get_fwd u64 h4 1024 with
+                  | Fail -> Fail
+                  | Return i0 ->
+                    let b1 = i0 = 56 in
+                    let b2 = not b1 in
+                    if b2
+                    then Fail
+                    else
+                      begin match hash_map_remove_fwd u64 h4 1024 with
+                      | Fail -> Fail
+                      | Return x ->
+                        begin match x with
+                        | None -> Fail
+                        | Some x0 ->
+                          let b3 = x0 = 56 in
+                          let b4 = not b3 in
+                          if b4
+                          then Fail
+                          else
+                            begin match hash_map_remove_back u64 h4 1024 with
+                            | Fail -> Fail
+                            | Return h5 ->
+                              begin match hash_map_get_fwd u64 h5 0 with
+                              | Fail -> Fail
+                              | Return i1 ->
+                                let b5 = i1 = 42 in
+                                let b6 = not b5 in
+                                if b6
+                                then Fail
+                                else
+                                  begin match hash_map_get_fwd u64 h5 128 with
+                                  | Fail -> Fail
+                                  | Return i2 ->
+                                    let b7 = i2 = 18 in
+                                    let b8 = not b7 in
+                                    if b8
+                                    then Fail
+                                    else
+                                      begin match hash_map_get_fwd u64 h5 1056
+                                        with
+                                      | Fail -> Fail
+                                      | Return i3 ->
+                                        let b9 = i3 = 256 in
+                                        let b10 = not b9 in
+                                        if b10 then Fail else Return ()
+                                      end
+                                  end
+                              end
+                            end
+                        end
+                      end
+                  end
+                end
+            end
+          end
+        end
+      end
+    end
+  end
+
+(** Unit test for [hashmap::test1] *)
+let _ = assert_norm (test1_fwd = Return ())
+
diff --git a/tests/hashmap/Hashmap.Types.fst b/tests/hashmap/Hashmap.Types.fst
new file mode 100644
index 00000000..22cdecff
--- /dev/null
+++ b/tests/hashmap/Hashmap.Types.fst
@@ -0,0 +1,21 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [hashmap]: type definitions *)
+module Hashmap.Types
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
+
+(** [hashmap::List] *)
+type list_t (t : Type0) =
+| ListCons : usize -> t -> list_t t -> list_t t
+| ListNil : list_t t
+
+(** [hashmap::HashMap] *)
+type hash_map_t (t : Type0) =
+{
+  hash_map_num_entries : usize;
+  hash_map_max_load_factor : (usize & usize);
+  hash_map_max_load : usize;
+  hash_map_slots : vec (list_t t);
+}
+
diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst
new file mode 100644
index 00000000..77cf59aa
--- /dev/null
+++ b/tests/hashmap/Primitives.fst
@@ -0,0 +1,279 @@
+/// 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 result (a : Type0) : Type0 =
+| Return : v:a -> result a
+| Fail : result a
+
+// Monadic bind and return.
+// Re-definining those allows us to customize the result of the monadic notations
+// like: `y <-- f x;`
+let return (#a : Type0) (x:a) : result a = Return x
+let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
+    match m with
+    | Return x -> f x
+    | Fail -> Fail
+
+// Monadic assert(...)
+let massert (b:bool) : result unit = if b then Return () else Fail
+
+(*** Misc *)
+type char = FStar.Char.char
+type string = string
+
+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 *)
+/// Rk.: most of the following code was at least partially generated
+
+let isize_min : int = -9223372036854775808
+let isize_max : int = 9223372036854775807
+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 // being conservative here: [u32_max] instead of [u64_max]
+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
+
+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
+
+/// 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
+
+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)
+
+/// 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
+
+/// 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
+
+(*** 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 -> True
+    | 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
+
+// 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
+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
+
+// 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
+let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit =
+  if i < length v then Return () else Fail
+
+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
+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
+