Reorganize the project to prepare for new backends

9 files changed, 0 insertions, 1391 deletions

diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
deleted file mode 100644
index 884d1778..00000000
--- a/tests/misc/Constants.fst
+++ /dev/null
@@ -1,137 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [constants] *)
-module Constants
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [constants::X0] *)
-let x0_body : result u32 = Return 0
-let x0_c : u32 = eval_global x0_body
-
-(** [core::num::u32::{9}::MAX] *)
-let core_num_u32_max_body : result u32 = Return 4294967295
-let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
-
-(** [constants::X1] *)
-let x1_body : result u32 = Return core_num_u32_max_c
-let x1_c : u32 = eval_global x1_body
-
-(** [constants::X2] *)
-let x2_body : result u32 = Return 3
-let x2_c : u32 = eval_global x2_body
-
-(** [constants::incr] *)
-let incr_fwd (n : u32) : result u32 =
-  begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end
-
-(** [constants::X3] *)
-let x3_body : result u32 =
-  begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end
-let x3_c : u32 = eval_global x3_body
-
-(** [constants::mk_pair0] *)
-let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y)
-
-(** [constants::Pair] *)
-type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
-
-(** [constants::mk_pair1] *)
-let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
-  Return (Mkpair_t x y)
-
-(** [constants::P0] *)
-let p0_body : result (u32 & u32) =
-  begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
-let p0_c : (u32 & u32) = eval_global p0_body
-
-(** [constants::P1] *)
-let p1_body : result (pair_t u32 u32) =
-  begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
-let p1_c : pair_t u32 u32 = eval_global p1_body
-
-(** [constants::P2] *)
-let p2_body : result (u32 & u32) = Return (0, 1)
-let p2_c : (u32 & u32) = eval_global p2_body
-
-(** [constants::P3] *)
-let p3_body : result (pair_t u32 u32) = Return (Mkpair_t 0 1)
-let p3_c : pair_t u32 u32 = eval_global p3_body
-
-(** [constants::Wrap] *)
-type wrap_t (t : Type0) = { wrap_val : t; }
-
-(** [constants::Wrap::{0}::new] *)
-let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
-  Return (Mkwrap_t val0)
-
-(** [constants::Y] *)
-let y_body : result (wrap_t i32) =
-  begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end
-let y_c : wrap_t i32 = eval_global y_body
-
-(** [constants::unwrap_y] *)
-let unwrap_y_fwd : result i32 = Return y_c.wrap_val
-
-(** [constants::YVAL] *)
-let yval_body : result i32 =
-  begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end
-let yval_c : i32 = eval_global yval_body
-
-(** [constants::get_z1::Z1] *)
-let get_z1_z1_body : result i32 = Return 3
-let get_z1_z1_c : i32 = eval_global get_z1_z1_body
-
-(** [constants::get_z1] *)
-let get_z1_fwd : result i32 = Return get_z1_z1_c
-
-(** [constants::add] *)
-let add_fwd (a : i32) (b : i32) : result i32 =
-  begin match i32_add a b with | Fail -> Fail | Return i -> Return i end
-
-(** [constants::Q1] *)
-let q1_body : result i32 = Return 5
-let q1_c : i32 = eval_global q1_body
-
-(** [constants::Q2] *)
-let q2_body : result i32 = Return q1_c
-let q2_c : i32 = eval_global q2_body
-
-(** [constants::Q3] *)
-let q3_body : result i32 =
-  begin match add_fwd q2_c 3 with | Fail -> Fail | Return i -> Return i end
-let q3_c : i32 = eval_global q3_body
-
-(** [constants::get_z2] *)
-let get_z2_fwd : result i32 =
-  begin match get_z1_fwd with
-  | Fail -> Fail
-  | Return i ->
-    begin match add_fwd i q3_c with
-    | Fail -> Fail
-    | Return i0 ->
-      begin match add_fwd q1_c i0 with
-      | Fail -> Fail
-      | Return i1 -> Return i1
-      end
-    end
-  end
-
-(** [constants::S1] *)
-let s1_body : result u32 = Return 6
-let s1_c : u32 = eval_global s1_body
-
-(** [constants::S2] *)
-let s2_body : result u32 =
-  begin match incr_fwd s1_c with | Fail -> Fail | Return i -> Return i end
-let s2_c : u32 = eval_global s2_body
-
-(** [constants::S3] *)
-let s3_body : result (pair_t u32 u32) = Return p3_c
-let s3_c : pair_t u32 u32 = eval_global s3_body
-
-(** [constants::S4] *)
-let s4_body : result (pair_t u32 u32) =
-  begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end
-let s4_c : pair_t u32 u32 = eval_global s4_body
-
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
deleted file mode 100644
index 68a0061e..00000000
--- a/tests/misc/External.Funs.fst
+++ /dev/null
@@ -1,130 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: function definitions *)
-module External.Funs
-open Primitives
-include External.Types
-include External.Opaque
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [external::swap] *)
-let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) =
-  begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
-  | Return (st0, _) ->
-    begin match core_mem_swap_back0 t x y st st0 with
-    | Fail -> Fail
-    | Return (st1, _) ->
-      begin match core_mem_swap_back1 t x y st st1 with
-      | Fail -> Fail
-      | Return (st2, _) -> Return (st2, ())
-      end
-    end
-  end
-
-(** [external::swap] *)
-let swap_back
-  (t : Type0) (x : t) (y : t) (st : state) (st0 : state) :
-  result (state & (t & t))
-  =
-  begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
-  | Return (st1, _) ->
-    begin match core_mem_swap_back0 t x y st st1 with
-    | Fail -> Fail
-    | Return (st2, x0) ->
-      begin match core_mem_swap_back1 t x y st st2 with
-      | Fail -> Fail
-      | Return (_, y0) -> Return (st0, (x0, y0))
-      end
-    end
-  end
-
-(** [external::test_new_non_zero_u32] *)
-let test_new_non_zero_u32_fwd
-  (x : u32) (st : state) : result (state & core_num_nonzero_non_zero_u32_t) =
-  begin match core_num_nonzero_non_zero_u32_new_fwd x st with
-  | Fail -> Fail
-  | Return (st0, opt) ->
-    begin match
-      core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
-      with
-    | Fail -> Fail
-    | Return (st1, nzu) -> Return (st1, nzu)
-    end
-  end
-
-(** [external::test_vec] *)
-let test_vec_fwd : result unit =
-  let v = vec_new u32 in
-  begin match vec_push_back u32 v 0 with
-  | Fail -> Fail
-  | Return _ -> Return ()
-  end
-
-(** Unit test for [external::test_vec] *)
-let _ = assert_norm (test_vec_fwd = Return ())
-
-(** [external::custom_swap] *)
-let custom_swap_fwd
-  (t : Type0) (x : t) (y : t) (st : state) : result (state & t) =
-  begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
-  | Return (st0, _) ->
-    begin match core_mem_swap_back0 t x y st st0 with
-    | Fail -> Fail
-    | Return (st1, x0) ->
-      begin match core_mem_swap_back1 t x y st st1 with
-      | Fail -> Fail
-      | Return (st2, _) -> Return (st2, x0)
-      end
-    end
-  end
-
-(** [external::custom_swap] *)
-let custom_swap_back
-  (t : Type0) (x : t) (y : t) (st : state) (ret : t) (st0 : state) :
-  result (state & (t & t))
-  =
-  begin match core_mem_swap_fwd t x y st with
-  | Fail -> Fail
-  | Return (st1, _) ->
-    begin match core_mem_swap_back0 t x y st st1 with
-    | Fail -> Fail
-    | Return (st2, _) ->
-      begin match core_mem_swap_back1 t x y st st2 with
-      | Fail -> Fail
-      | Return (_, y0) -> Return (st0, (ret, y0))
-      end
-    end
-  end
-
-(** [external::test_custom_swap] *)
-let test_custom_swap_fwd
-  (x : u32) (y : u32) (st : state) : result (state & unit) =
-  begin match custom_swap_fwd u32 x y st with
-  | Fail -> Fail
-  | Return (st0, _) -> Return (st0, ())
-  end
-
-(** [external::test_custom_swap] *)
-let test_custom_swap_back
-  (x : u32) (y : u32) (st : state) (st0 : state) :
-  result (state & (u32 & u32))
-  =
-  begin match custom_swap_back u32 x y st 1 st0 with
-  | Fail -> Fail
-  | Return (st1, (x0, y0)) -> Return (st1, (x0, y0))
-  end
-
-(** [external::test_swap_non_zero] *)
-let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
-  begin match swap_fwd u32 x 0 st with
-  | Fail -> Fail
-  | Return (st0, _) ->
-    begin match swap_back u32 x 0 st st0 with
-    | Fail -> Fail
-    | Return (st1, (x0, _)) -> if x0 = 0 then Fail else Return (st1, x0)
-    end
-  end
-
diff --git a/tests/misc/External.Opaque.fsti b/tests/misc/External.Opaque.fsti
deleted file mode 100644
index 7d86405a..00000000
--- a/tests/misc/External.Opaque.fsti
+++ /dev/null
@@ -1,27 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: opaque function definitions *)
-module External.Opaque
-open Primitives
-include External.Types
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [core::mem::swap] *)
-val core_mem_swap_fwd (t : Type0) : t -> t -> state -> result (state & unit)
-
-(** [core::mem::swap] *)
-val core_mem_swap_back0
-  (t : Type0) : t -> t -> state -> state -> result (state & t)
-
-(** [core::mem::swap] *)
-val core_mem_swap_back1
-  (t : Type0) : t -> t -> state -> state -> result (state & t)
-
-(** [core::num::nonzero::NonZeroU32::{14}::new] *)
-val core_num_nonzero_non_zero_u32_new_fwd
-  : u32 -> state -> result (state & (option core_num_nonzero_non_zero_u32_t))
-
-(** [core::option::Option::{0}::unwrap] *)
-val core_option_option_unwrap_fwd
-  (t : Type0) : option t -> state -> result (state & t)
-
diff --git a/tests/misc/External.Types.fsti b/tests/misc/External.Types.fsti
deleted file mode 100644
index 4a13a744..00000000
--- a/tests/misc/External.Types.fsti
+++ /dev/null
@@ -1,13 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [external]: type definitions *)
-module External.Types
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [core::num::nonzero::NonZeroU32] *)
-val core_num_nonzero_non_zero_u32_t : Type0
-
-(** The state type used in the state-error monad *)
-val state : Type0
-
diff --git a/tests/misc/Makefile b/tests/misc/Makefile
deleted file mode 100644
index a16b0edb..00000000
--- a/tests/misc/Makefile
+++ /dev/null
@@ -1,47 +0,0 @@
-INCLUDE_DIRS = .
-
-FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
-
-FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
-
-FSTAR_OPTIONS = $(FSTAR_HINTS) \
-  --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
-  --warn_error '+241@247+285-274' \
-
-FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
-
-FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
-
-# The F* roots are used to compute the dependency graph, and generate the .depend file
-FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
-
-# Build all the files
-all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
-
-# This is the right way to ensure the .depend file always gets re-built.
-ifeq (,$(filter %-in,$(MAKECMDGOALS)))
-ifndef NODEPEND
-ifndef MAKE_RESTARTS
-.depend: .FORCE
-	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@
-
-.PHONY: .FORCE
-.FORCE:
-endif
-endif
-
-include .depend
-endif
-
-# For the interactive mode
-%.fst-in %.fsti-in:
-	@echo $(FSTAR_OPTIONS)
-
-# Generete the .checked files in batch mode
-%.checked:
-	$(FSTAR) $(FSTAR_OPTIONS) $< && \
-	touch -c $@
-
-.PHONY: clean
-clean:
-	rm -f obj/*
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
deleted file mode 100644
index 8161e7cd..00000000
--- a/tests/misc/NoNestedBorrows.fst
+++ /dev/null
@@ -1,562 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [no_nested_borrows] *)
-module NoNestedBorrows
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [no_nested_borrows::Pair] *)
-type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
-
-(** [no_nested_borrows::List] *)
-type list_t (t : Type0) =
-| ListCons : t -> list_t t -> list_t t
-| ListNil : list_t t
-
-(** [no_nested_borrows::One] *)
-type one_t (t1 : Type0) = | OneOne : t1 -> one_t t1
-
-(** [no_nested_borrows::EmptyEnum] *)
-type empty_enum_t = | EmptyEnumEmpty : empty_enum_t
-
-(** [no_nested_borrows::Enum] *)
-type enum_t = | EnumVariant1 : enum_t | EnumVariant2 : enum_t
-
-(** [no_nested_borrows::EmptyStruct] *)
-type empty_struct_t = unit
-
-(** [no_nested_borrows::Sum] *)
-type sum_t (t1 t2 : Type0) =
-| SumLeft : t1 -> sum_t t1 t2
-| SumRight : t2 -> sum_t t1 t2
-
-(** [no_nested_borrows::neg_test] *)
-let neg_test_fwd (x : i32) : result i32 =
-  begin match i32_neg x with | Fail -> Fail | Return i -> Return i end
-
-(** [no_nested_borrows::add_test] *)
-let add_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_add x y with | Fail -> Fail | Return i -> Return i end
-
-(** [no_nested_borrows::subs_test] *)
-let subs_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_sub x y with | Fail -> Fail | Return i -> Return i end
-
-(** [no_nested_borrows::div_test] *)
-let div_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_div x y with | Fail -> Fail | Return i -> Return i end
-
-(** [no_nested_borrows::div_test1] *)
-let div_test1_fwd (x : u32) : result u32 =
-  begin match u32_div x 2 with | Fail -> Fail | Return i -> Return i end
-
-(** [no_nested_borrows::rem_test] *)
-let rem_test_fwd (x : u32) (y : u32) : result u32 =
-  begin match u32_rem x y with | Fail -> Fail | Return i -> Return i end
-
-(** [no_nested_borrows::cast_test] *)
-let cast_test_fwd (x : u32) : result i32 =
-  begin match scalar_cast U32 I32 x with
-  | Fail -> Fail
-  | Return i -> Return i
-  end
-
-(** [no_nested_borrows::test2] *)
-let test2_fwd : result unit =
-  begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end
-
-(** Unit test for [no_nested_borrows::test2] *)
-let _ = assert_norm (test2_fwd = Return ())
-
-(** [no_nested_borrows::get_max] *)
-let get_max_fwd (x : u32) (y : u32) : result u32 =
-  if x >= y then Return x else Return y
-
-(** [no_nested_borrows::test3] *)
-let test3_fwd : result unit =
-  begin match get_max_fwd 4 3 with
-  | Fail -> Fail
-  | Return x ->
-    begin match get_max_fwd 10 11 with
-    | Fail -> Fail
-    | Return y ->
-      begin match u32_add x y with
-      | Fail -> Fail
-      | Return z -> if not (z = 15) then Fail else Return ()
-      end
-    end
-  end
-
-(** Unit test for [no_nested_borrows::test3] *)
-let _ = assert_norm (test3_fwd = Return ())
-
-(** [no_nested_borrows::test_neg1] *)
-let test_neg1_fwd : result unit =
-  begin match i32_neg 3 with
-  | Fail -> Fail
-  | Return y -> if not (y = -3) then Fail else Return ()
-  end
-
-(** Unit test for [no_nested_borrows::test_neg1] *)
-let _ = assert_norm (test_neg1_fwd = Return ())
-
-(** [no_nested_borrows::refs_test1] *)
-let refs_test1_fwd : result unit = if not (1 = 1) then Fail else Return ()
-
-(** Unit test for [no_nested_borrows::refs_test1] *)
-let _ = assert_norm (refs_test1_fwd = Return ())
-
-(** [no_nested_borrows::refs_test2] *)
-let refs_test2_fwd : result unit =
-  if not (2 = 2)
-  then Fail
-  else
-    if not (0 = 0)
-    then Fail
-    else if not (2 = 2) then Fail else if not (2 = 2) then Fail else Return ()
-
-(** Unit test for [no_nested_borrows::refs_test2] *)
-let _ = assert_norm (refs_test2_fwd = Return ())
-
-(** [no_nested_borrows::test_list1] *)
-let test_list1_fwd : result unit = Return ()
-
-(** Unit test for [no_nested_borrows::test_list1] *)
-let _ = assert_norm (test_list1_fwd = Return ())
-
-(** [no_nested_borrows::test_box1] *)
-let test_box1_fwd : result unit =
-  let b = 1 in let x = b in if not (x = 1) then Fail else Return ()
-
-(** Unit test for [no_nested_borrows::test_box1] *)
-let _ = assert_norm (test_box1_fwd = Return ())
-
-(** [no_nested_borrows::copy_int] *)
-let copy_int_fwd (x : i32) : result i32 = Return x
-
-(** [no_nested_borrows::test_unreachable] *)
-let test_unreachable_fwd (b : bool) : result unit =
-  if b then Fail else Return ()
-
-(** [no_nested_borrows::test_panic] *)
-let test_panic_fwd (b : bool) : result unit = if b then Fail else Return ()
-
-(** [no_nested_borrows::test_copy_int] *)
-let test_copy_int_fwd : result unit =
-  begin match copy_int_fwd 0 with
-  | Fail -> Fail
-  | Return y -> if not (0 = y) then Fail else Return ()
-  end
-
-(** Unit test for [no_nested_borrows::test_copy_int] *)
-let _ = assert_norm (test_copy_int_fwd = Return ())
-
-(** [no_nested_borrows::is_cons] *)
-let is_cons_fwd (t : Type0) (l : list_t t) : result bool =
-  begin match l with
-  | ListCons x l0 -> Return true
-  | ListNil -> Return false
-  end
-
-(** [no_nested_borrows::test_is_cons] *)
-let test_is_cons_fwd : result unit =
-  let l = ListNil in
-  begin match is_cons_fwd i32 (ListCons 0 l) with
-  | Fail -> Fail
-  | Return b -> if not b then Fail else Return ()
-  end
-
-(** Unit test for [no_nested_borrows::test_is_cons] *)
-let _ = assert_norm (test_is_cons_fwd = Return ())
-
-(** [no_nested_borrows::split_list] *)
-let split_list_fwd (t : Type0) (l : list_t t) : result (t & (list_t t)) =
-  begin match l with | ListCons hd tl -> Return (hd, tl) | ListNil -> Fail end
-
-(** [no_nested_borrows::test_split_list] *)
-let test_split_list_fwd : result unit =
-  let l = ListNil in
-  begin match split_list_fwd i32 (ListCons 0 l) with
-  | Fail -> Fail
-  | Return p -> let (hd, _) = p in if not (hd = 0) then Fail else Return ()
-  end
-
-(** Unit test for [no_nested_borrows::test_split_list] *)
-let _ = assert_norm (test_split_list_fwd = Return ())
-
-(** [no_nested_borrows::choose] *)
-let choose_fwd (t : Type0) (b : bool) (x : t) (y : t) : result t =
-  if b then Return x else Return y
-
-(** [no_nested_borrows::choose] *)
-let choose_back
-  (t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) =
-  if b then Return (ret, y) else Return (x, ret)
-
-(** [no_nested_borrows::choose_test] *)
-let choose_test_fwd : result unit =
-  begin match choose_fwd i32 true 0 0 with
-  | Fail -> Fail
-  | Return z ->
-    begin match i32_add z 1 with
-    | Fail -> Fail
-    | Return z0 ->
-      if not (z0 = 1)
-      then Fail
-      else
-        begin match choose_back i32 true 0 0 z0 with
-        | Fail -> Fail
-        | Return (x, y) ->
-          if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
-        end
-    end
-  end
-
-(** Unit test for [no_nested_borrows::choose_test] *)
-let _ = assert_norm (choose_test_fwd = Return ())
-
-(** [no_nested_borrows::test_char] *)
-let test_char_fwd : result char = Return 'a'
-
-(** [no_nested_borrows::NodeElem] *)
-type node_elem_t (t : Type0) =
-| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t
-| NodeElemNil : node_elem_t t
-
-(** [no_nested_borrows::Tree] *)
-and tree_t (t : Type0) =
-| TreeLeaf : t -> tree_t t
-| TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t
-
-(** [no_nested_borrows::odd] *)
-let rec odd_fwd (x : u32) : result bool =
-  if x = 0
-  then Return false
-  else
-    begin match u32_sub x 1 with
-    | Fail -> Fail
-    | Return i ->
-      begin match even_fwd i with | Fail -> Fail | Return b -> Return b end
-    end
-
-(** [no_nested_borrows::even] *)
-and even_fwd (x : u32) : result bool =
-  if x = 0
-  then Return true
-  else
-    begin match u32_sub x 1 with
-    | Fail -> Fail
-    | Return i ->
-      begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end
-    end
-
-(** [no_nested_borrows::test_even_odd] *)
-let test_even_odd_fwd : result unit =
-  begin match even_fwd 0 with
-  | Fail -> Fail
-  | Return b ->
-    if not b
-    then Fail
-    else
-      begin match even_fwd 4 with
-      | Fail -> Fail
-      | Return b0 ->
-        if not b0
-        then Fail
-        else
-          begin match odd_fwd 1 with
-          | Fail -> Fail
-          | Return b1 ->
-            if not b1
-            then Fail
-            else
-              begin match odd_fwd 5 with
-              | Fail -> Fail
-              | Return b2 -> if not b2 then Fail else Return ()
-              end
-          end
-      end
-  end
-
-(** Unit test for [no_nested_borrows::test_even_odd] *)
-let _ = assert_norm (test_even_odd_fwd = Return ())
-
-(** [no_nested_borrows::list_length] *)
-let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
-  begin match l with
-  | ListCons x l1 ->
-    begin match list_length_fwd t l1 with
-    | Fail -> Fail
-    | Return i ->
-      begin match u32_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end
-    end
-  | ListNil -> Return 0
-  end
-
-(** [no_nested_borrows::list_nth_shared] *)
-let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
-  begin match l with
-  | ListCons x tl ->
-    if i = 0
-    then Return x
-    else
-      begin match u32_sub i 1 with
-      | Fail -> Fail
-      | Return i0 ->
-        begin match list_nth_shared_fwd t tl i0 with
-        | Fail -> Fail
-        | Return x0 -> Return x0
-        end
-      end
-  | ListNil -> Fail
-  end
-
-(** [no_nested_borrows::list_nth_mut] *)
-let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
-  begin match l with
-  | ListCons x tl ->
-    if i = 0
-    then Return x
-    else
-      begin match u32_sub i 1 with
-      | Fail -> Fail
-      | Return i0 ->
-        begin match list_nth_mut_fwd t tl i0 with
-        | Fail -> Fail
-        | Return x0 -> Return x0
-        end
-      end
-  | ListNil -> Fail
-  end
-
-(** [no_nested_borrows::list_nth_mut] *)
-let rec list_nth_mut_back
-  (t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) =
-  begin match l with
-  | ListCons x tl ->
-    if i = 0
-    then Return (ListCons ret tl)
-    else
-      begin match u32_sub i 1 with
-      | Fail -> Fail
-      | Return i0 ->
-        begin match list_nth_mut_back t tl i0 ret with
-        | Fail -> Fail
-        | Return tl0 -> Return (ListCons x tl0)
-        end
-      end
-  | ListNil -> Fail
-  end
-
-(** [no_nested_borrows::list_rev_aux] *)
-let rec list_rev_aux_fwd
-  (t : Type0) (li : list_t t) (lo : list_t t) : result (list_t t) =
-  begin match li with
-  | ListCons hd tl ->
-    begin match list_rev_aux_fwd t tl (ListCons hd lo) with
-    | Fail -> Fail
-    | Return l -> Return l
-    end
-  | ListNil -> Return lo
-  end
-
-(** [no_nested_borrows::list_rev] *)
-let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) =
-  let li = mem_replace_fwd (list_t t) l ListNil in
-  begin match list_rev_aux_fwd t li ListNil with
-  | Fail -> Fail
-  | Return l0 -> Return l0
-  end
-
-(** [no_nested_borrows::test_list_functions] *)
-let test_list_functions_fwd : result unit =
-  let l = ListNil in
-  let l0 = ListCons 2 l in
-  let l1 = ListCons 1 l0 in
-  begin match list_length_fwd i32 (ListCons 0 l1) with
-  | Fail -> Fail
-  | Return i ->
-    if not (i = 3)
-    then Fail
-    else
-      begin match list_nth_shared_fwd i32 (ListCons 0 l1) 0 with
-      | Fail -> Fail
-      | Return i0 ->
-        if not (i0 = 0)
-        then Fail
-        else
-          begin match list_nth_shared_fwd i32 (ListCons 0 l1) 1 with
-          | Fail -> Fail
-          | Return i1 ->
-            if not (i1 = 1)
-            then Fail
-            else
-              begin match list_nth_shared_fwd i32 (ListCons 0 l1) 2 with
-              | Fail -> Fail
-              | Return i2 ->
-                if not (i2 = 2)
-                then Fail
-                else
-                  begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with
-                  | Fail -> Fail
-                  | Return ls ->
-                    begin match list_nth_shared_fwd i32 ls 0 with
-                    | Fail -> Fail
-                    | Return i3 ->
-                      if not (i3 = 0)
-                      then Fail
-                      else
-                        begin match list_nth_shared_fwd i32 ls 1 with
-                        | Fail -> Fail
-                        | Return i4 ->
-                          if not (i4 = 3)
-                          then Fail
-                          else
-                            begin match list_nth_shared_fwd i32 ls 2 with
-                            | Fail -> Fail
-                            | Return i5 ->
-                              if not (i5 = 2) then Fail else Return ()
-                            end
-                        end
-                    end
-                  end
-              end
-          end
-      end
-  end
-
-(** Unit test for [no_nested_borrows::test_list_functions] *)
-let _ = assert_norm (test_list_functions_fwd = Return ())
-
-(** [no_nested_borrows::id_mut_pair1] *)
-let id_mut_pair1_fwd (t1 t2 : Type0) (x : t1) (y : t2) : result (t1 & t2) =
-  Return (x, y)
-
-(** [no_nested_borrows::id_mut_pair1] *)
-let id_mut_pair1_back
-  (t1 t2 : Type0) (x : t1) (y : t2) (ret : (t1 & t2)) : result (t1 & t2) =
-  let (x0, x1) = ret in Return (x0, x1)
-
-(** [no_nested_borrows::id_mut_pair2] *)
-let id_mut_pair2_fwd (t1 t2 : Type0) (p : (t1 & t2)) : result (t1 & t2) =
-  let (x, x0) = p in Return (x, x0)
-
-(** [no_nested_borrows::id_mut_pair2] *)
-let id_mut_pair2_back
-  (t1 t2 : Type0) (p : (t1 & t2)) (ret : (t1 & t2)) : result (t1 & t2) =
-  let (x, x0) = ret in Return (x, x0)
-
-(** [no_nested_borrows::id_mut_pair3] *)
-let id_mut_pair3_fwd (t1 t2 : Type0) (x : t1) (y : t2) : result (t1 & t2) =
-  Return (x, y)
-
-(** [no_nested_borrows::id_mut_pair3] *)
-let id_mut_pair3_back'a
-  (t1 t2 : Type0) (x : t1) (y : t2) (ret : t1) : result t1 =
-  Return ret
-
-(** [no_nested_borrows::id_mut_pair3] *)
-let id_mut_pair3_back'b
-  (t1 t2 : Type0) (x : t1) (y : t2) (ret : t2) : result t2 =
-  Return ret
-
-(** [no_nested_borrows::id_mut_pair4] *)
-let id_mut_pair4_fwd (t1 t2 : Type0) (p : (t1 & t2)) : result (t1 & t2) =
-  let (x, x0) = p in Return (x, x0)
-
-(** [no_nested_borrows::id_mut_pair4] *)
-let id_mut_pair4_back'a
-  (t1 t2 : Type0) (p : (t1 & t2)) (ret : t1) : result t1 =
-  Return ret
-
-(** [no_nested_borrows::id_mut_pair4] *)
-let id_mut_pair4_back'b
-  (t1 t2 : Type0) (p : (t1 & t2)) (ret : t2) : result t2 =
-  Return ret
-
-(** [no_nested_borrows::StructWithTuple] *)
-type struct_with_tuple_t (t1 t2 : Type0) = { struct_with_tuple_p : (t1 & t2); }
-
-(** [no_nested_borrows::new_tuple1] *)
-let new_tuple1_fwd : result (struct_with_tuple_t u32 u32) =
-  Return (Mkstruct_with_tuple_t (1, 2))
-
-(** [no_nested_borrows::new_tuple2] *)
-let new_tuple2_fwd : result (struct_with_tuple_t i16 i16) =
-  Return (Mkstruct_with_tuple_t (1, 2))
-
-(** [no_nested_borrows::new_tuple3] *)
-let new_tuple3_fwd : result (struct_with_tuple_t u64 i64) =
-  Return (Mkstruct_with_tuple_t (1, 2))
-
-(** [no_nested_borrows::StructWithPair] *)
-type struct_with_pair_t (t1 t2 : Type0) =
-{
-  struct_with_pair_p : pair_t t1 t2;
-}
-
-(** [no_nested_borrows::new_pair1] *)
-let new_pair1_fwd : result (struct_with_pair_t u32 u32) =
-  Return (Mkstruct_with_pair_t (Mkpair_t 1 2))
-
-(** [no_nested_borrows::test_constants] *)
-let test_constants_fwd : result unit =
-  begin match new_tuple1_fwd with
-  | Fail -> Fail
-  | Return swt ->
-    let (i, _) = swt.struct_with_tuple_p in
-    if not (i = 1)
-    then Fail
-    else
-      begin match new_tuple2_fwd with
-      | Fail -> Fail
-      | Return swt0 ->
-        let (i0, _) = swt0.struct_with_tuple_p in
-        if not (i0 = 1)
-        then Fail
-        else
-          begin match new_tuple3_fwd with
-          | Fail -> Fail
-          | Return swt1 ->
-            let (i1, _) = swt1.struct_with_tuple_p in
-            if not (i1 = 1)
-            then Fail
-            else
-              begin match new_pair1_fwd with
-              | Fail -> Fail
-              | Return swp ->
-                if not (swp.struct_with_pair_p.pair_x = 1)
-                then Fail
-                else Return ()
-              end
-          end
-      end
-  end
-
-(** Unit test for [no_nested_borrows::test_constants] *)
-let _ = assert_norm (test_constants_fwd = Return ())
-
-(** [no_nested_borrows::test_weird_borrows1] *)
-let test_weird_borrows1_fwd : result unit = Return ()
-
-(** Unit test for [no_nested_borrows::test_weird_borrows1] *)
-let _ = assert_norm (test_weird_borrows1_fwd = Return ())
-
-(** [no_nested_borrows::test_mem_replace] *)
-let test_mem_replace_fwd_back (px : u32) : result u32 =
-  let y = mem_replace_fwd u32 px 1 in if not (y = 0) then Fail else Return 2
-
-(** [no_nested_borrows::test_shared_borrow_bool1] *)
-let test_shared_borrow_bool1_fwd (b : bool) : result u32 =
-  if b then Return 0 else Return 1
-
-(** [no_nested_borrows::test_shared_borrow_bool2] *)
-let test_shared_borrow_bool2_fwd : result u32 = Return 0
-
-(** [no_nested_borrows::test_shared_borrow_enum1] *)
-let test_shared_borrow_enum1_fwd (l : list_t u32) : result u32 =
-  begin match l with | ListCons i l0 -> Return 1 | ListNil -> Return 0 end
-
-(** [no_nested_borrows::test_shared_borrow_enum2] *)
-let test_shared_borrow_enum2_fwd : result u32 = Return 0
-
diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst
deleted file mode 100644
index 424889ef..00000000
--- a/tests/misc/Paper.fst
+++ /dev/null
@@ -1,147 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [paper] *)
-module Paper
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [paper::ref_incr] *)
-let ref_incr_fwd_back (x : i32) : result i32 =
-  begin match i32_add x 1 with | Fail -> Fail | Return x0 -> Return x0 end
-
-(** [paper::test_incr] *)
-let test_incr_fwd : result unit =
-  begin match ref_incr_fwd_back 0 with
-  | Fail -> Fail
-  | Return x -> if not (x = 1) then Fail else Return ()
-  end
-
-(** Unit test for [paper::test_incr] *)
-let _ = assert_norm (test_incr_fwd = Return ())
-
-(** [paper::choose] *)
-let choose_fwd (t : Type0) (b : bool) (x : t) (y : t) : result t =
-  if b then Return x else Return y
-
-(** [paper::choose] *)
-let choose_back
-  (t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) =
-  if b then Return (ret, y) else Return (x, ret)
-
-(** [paper::test_choose] *)
-let test_choose_fwd : result unit =
-  begin match choose_fwd i32 true 0 0 with
-  | Fail -> Fail
-  | Return z ->
-    begin match i32_add z 1 with
-    | Fail -> Fail
-    | Return z0 ->
-      if not (z0 = 1)
-      then Fail
-      else
-        begin match choose_back i32 true 0 0 z0 with
-        | Fail -> Fail
-        | Return (x, y) ->
-          if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
-        end
-    end
-  end
-
-(** Unit test for [paper::test_choose] *)
-let _ = assert_norm (test_choose_fwd = Return ())
-
-(** [paper::List] *)
-type list_t (t : Type0) =
-| ListCons : t -> list_t t -> list_t t
-| ListNil : list_t t
-
-(** [paper::list_nth_mut] *)
-let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
-  begin match l with
-  | ListCons x tl ->
-    if i = 0
-    then Return x
-    else
-      begin match u32_sub i 1 with
-      | Fail -> Fail
-      | Return i0 ->
-        begin match list_nth_mut_fwd t tl i0 with
-        | Fail -> Fail
-        | Return x0 -> Return x0
-        end
-      end
-  | ListNil -> Fail
-  end
-
-(** [paper::list_nth_mut] *)
-let rec list_nth_mut_back
-  (t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) =
-  begin match l with
-  | ListCons x tl ->
-    if i = 0
-    then Return (ListCons ret tl)
-    else
-      begin match u32_sub i 1 with
-      | Fail -> Fail
-      | Return i0 ->
-        begin match list_nth_mut_back t tl i0 ret with
-        | Fail -> Fail
-        | Return tl0 -> Return (ListCons x tl0)
-        end
-      end
-  | ListNil -> Fail
-  end
-
-(** [paper::sum] *)
-let rec sum_fwd (l : list_t i32) : result i32 =
-  begin match l with
-  | ListCons x tl ->
-    begin match sum_fwd tl with
-    | Fail -> Fail
-    | Return i ->
-      begin match i32_add x i with | Fail -> Fail | Return i0 -> Return i0 end
-    end
-  | ListNil -> Return 0
-  end
-
-(** [paper::test_nth] *)
-let test_nth_fwd : result unit =
-  let l = ListNil in
-  let l0 = ListCons 3 l in
-  let l1 = ListCons 2 l0 in
-  begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with
-  | Fail -> Fail
-  | Return x ->
-    begin match i32_add x 1 with
-    | Fail -> Fail
-    | Return x0 ->
-      begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with
-      | Fail -> Fail
-      | Return l2 ->
-        begin match sum_fwd l2 with
-        | Fail -> Fail
-        | Return i -> if not (i = 7) then Fail else Return ()
-        end
-      end
-    end
-  end
-
-(** Unit test for [paper::test_nth] *)
-let _ = assert_norm (test_nth_fwd = Return ())
-
-(** [paper::call_choose] *)
-let call_choose_fwd (p : (u32 & u32)) : result u32 =
-  let (px, py) = p in
-  begin match choose_fwd u32 true px py with
-  | Fail -> Fail
-  | Return pz ->
-    begin match u32_add pz 1 with
-    | Fail -> Fail
-    | Return pz0 ->
-      begin match choose_back u32 true px py pz0 with
-      | Fail -> Fail
-      | Return (px0, _) -> Return px0
-      end
-    end
-  end
-
diff --git a/tests/misc/PoloniusList.fst b/tests/misc/PoloniusList.fst
deleted file mode 100644
index 73e98884..00000000
--- a/tests/misc/PoloniusList.fst
+++ /dev/null
@@ -1,41 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [polonius_list] *)
-module PoloniusList
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [polonius_list::List] *)
-type list_t (t : Type0) =
-| ListCons : t -> list_t t -> list_t t
-| ListNil : list_t t
-
-(** [polonius_list::get_list_at_x] *)
-let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
-  begin match ls with
-  | ListCons hd tl ->
-    if hd = x
-    then Return (ListCons hd tl)
-    else
-      begin match get_list_at_x_fwd tl x with
-      | Fail -> Fail
-      | Return l -> Return l
-      end
-  | ListNil -> Return ListNil
-  end
-
-(** [polonius_list::get_list_at_x] *)
-let rec get_list_at_x_back
-  (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) =
-  begin match ls with
-  | ListCons hd tl ->
-    if hd = x
-    then Return ret
-    else
-      begin match get_list_at_x_back tl x ret with
-      | Fail -> Fail
-      | Return tl0 -> Return (ListCons hd tl0)
-      end
-  | ListNil -> Return ret
-  end
-
diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst
deleted file mode 100644
index 96138e46..00000000
--- a/tests/misc/Primitives.fst
+++ /dev/null
@@ -1,287 +0,0 @@
-/// 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
-
-// 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 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 // 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
-
-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)
-
-(** 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
-
-/// 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
-