Make good progress on the Coq backend

12 files changed, 1431 insertions, 53 deletions

diff --git a/tests/Makefile b/tests/Makefile
new file mode 100644
index 00000000..dfb20cc4
--- /dev/null
+++ b/tests/Makefile
@@ -0,0 +1,3 @@
+all:
+	cd fstar && $(MAKE) all
+	cd coq && $(MAKE) all
diff --git a/tests/coq/Makefile b/tests/coq/Makefile
new file mode 100644
index 00000000..5fead9c9
--- /dev/null
+++ b/tests/coq/Makefile
@@ -0,0 +1,3 @@
+# TODO: make this more general
+all:
+	cd misc && $(MAKE) all
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
new file mode 100644
index 00000000..677aae8c
--- /dev/null
+++ b/tests/coq/misc/Constants.v
@@ -0,0 +1,138 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [constants] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module Constants .
+
+(** [constants::X0] *)
+Definition x0_body : result u32 := Return (0 %u32) .
+Definition x0_c : u32 := x0_body%global .
+
+(** [core::num::u32::{9}::MAX] *)
+Definition core_num_u32_max_body : result u32 := Return (4294967295 %u32) .
+Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global .
+
+(** [constants::X1] *)
+Definition x1_body : result u32 := Return core_num_u32_max_c .
+Definition x1_c : u32 := x1_body%global .
+
+(** [constants::X2] *)
+Definition x2_body : result u32 := Return (3 %u32) .
+Definition x2_c : u32 := x2_body%global .
+
+(** [constants::incr] *)
+Definition incr_fwd (n : u32) : result u32 := i <- u32_add n 1 %u32; Return i .
+
+(** [constants::X3] *)
+Definition x3_body : result u32 := i <- incr_fwd (32 %u32); Return i .
+Definition x3_c : u32 := x3_body%global .
+
+(** [constants::mk_pair0] *)
+Definition mk_pair0_fwd (x : u32) (y : u32) : result (u32 * u32) :=
+  Return (x, y) .
+
+(** [constants::Pair] *)
+Record Pair_t (T1 T2 : Type) := mkPair_t { Pair_x : T1; Pair_y : T2; } .
+
+Arguments mkPair_t {T1} {T2} _ _  .
+Arguments Pair_x {T1} {T2}  .
+Arguments Pair_y {T1} {T2}  .
+
+(** [constants::mk_pair1] *)
+Definition mk_pair1_fwd (x : u32) (y : u32) : result (Pair_t u32 u32) :=
+  Return (mkPair_t x y) .
+
+(** [constants::P0] *)
+Definition p0_body : result (u32 * u32) :=
+  p <- mk_pair0_fwd (0 %u32) (1 %u32); Return p
+  .
+Definition p0_c : (u32 * u32) := p0_body%global .
+
+(** [constants::P1] *)
+Definition p1_body : result (Pair_t u32 u32) :=
+  p <- mk_pair1_fwd (0 %u32) (1 %u32); Return p
+  .
+Definition p1_c : Pair_t u32 u32 := p1_body%global .
+
+(** [constants::P2] *)
+Definition p2_body : result (u32 * u32) := Return (0 %u32, 1 %u32) .
+Definition p2_c : (u32 * u32) := p2_body%global .
+
+(** [constants::P3] *)
+Definition p3_body : result (Pair_t u32 u32) :=
+  Return (mkPair_t (0 %u32) (1 %u32))
+  .
+Definition p3_c : Pair_t u32 u32 := p3_body%global .
+
+(** [constants::Wrap] *)
+Record Wrap_t (T : Type) := mkWrap_t { Wrap_val : T; } .
+
+Arguments mkWrap_t {T} _  .
+Arguments Wrap_val {T}  .
+
+(** [constants::Wrap::{0}::new] *)
+Definition wrap_new_fwd (T : Type) (val : T) : result (Wrap_t T) :=
+  Return (mkWrap_t val) .
+
+(** [constants::Y] *)
+Definition y_body : result (Wrap_t i32) :=
+  w <- wrap_new_fwd i32 (2 %i32); Return w
+  .
+Definition y_c : Wrap_t i32 := y_body%global .
+
+(** [constants::unwrap_y] *)
+Definition unwrap_y_fwd : result i32 :=
+  match y_c with | mkWrap_t i => Return i end .
+
+(** [constants::YVAL] *)
+Definition yval_body : result i32 := i <- unwrap_y_fwd; Return i .
+Definition yval_c : i32 := yval_body%global .
+
+(** [constants::get_z1::Z1] *)
+Definition get_z1_z1_body : result i32 := Return (3 %i32) .
+Definition get_z1_z1_c : i32 := get_z1_z1_body%global .
+
+(** [constants::get_z1] *)
+Definition get_z1_fwd : result i32 := Return get_z1_z1_c .
+
+(** [constants::add] *)
+Definition add_fwd (a : i32) (b : i32) : result i32 :=
+  i <- i32_add a b; Return i .
+
+(** [constants::Q1] *)
+Definition q1_body : result i32 := Return (5 %i32) .
+Definition q1_c : i32 := q1_body%global .
+
+(** [constants::Q2] *)
+Definition q2_body : result i32 := Return q1_c .
+Definition q2_c : i32 := q2_body%global .
+
+(** [constants::Q3] *)
+Definition q3_body : result i32 := i <- add_fwd q2_c (3 %i32); Return i .
+Definition q3_c : i32 := q3_body%global .
+
+(** [constants::get_z2] *)
+Definition get_z2_fwd : result i32 :=
+  i <- get_z1_fwd; i0 <- add_fwd i q3_c; i1 <- add_fwd q1_c i0; Return i1 .
+
+(** [constants::S1] *)
+Definition s1_body : result u32 := Return (6 %u32) .
+Definition s1_c : u32 := s1_body%global .
+
+(** [constants::S2] *)
+Definition s2_body : result u32 := i <- incr_fwd s1_c; Return i .
+Definition s2_c : u32 := s2_body%global .
+
+(** [constants::S3] *)
+Definition s3_body : result (Pair_t u32 u32) := Return p3_c .
+Definition s3_c : Pair_t u32 u32 := s3_body%global .
+
+(** [constants::S4] *)
+Definition s4_body : result (Pair_t u32 u32) :=
+  p <- mk_pair1_fwd (7 %u32) (8 %u32); Return p
+  .
+Definition s4_c : Pair_t u32 u32 := s4_body%global .
+
+End Constants .
diff --git a/tests/coq/misc/External__Funs.v b/tests/coq/misc/External__Funs.v
new file mode 100644
index 00000000..77b738b0
--- /dev/null
+++ b/tests/coq/misc/External__Funs.v
@@ -0,0 +1,100 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: function definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Require Export External__Types .
+Import External__Types .
+Require Export External__Opaque .
+Import External__Opaque .
+Module External__Funs .
+
+(** [external::swap] *)
+Definition swap_fwd
+  (T : Type) (x : T) (y : T) (st : state) : result (state * unit) :=
+  p <- core_mem_swap_fwd T x y st;
+  let (st0, _) := p in
+  p0 <- core_mem_swap_back0 T x y st st0;
+  let (st1, _) := p0 in
+  p1 <- core_mem_swap_back1 T x y st st1;
+  let (st2, _) := p1 in Return (st2, tt)
+  .
+
+(** [external::swap] *)
+Definition swap_back
+  (T : Type) (x : T) (y : T) (st : state) (st0 : state) :
+  result (state * (T * T))
+  :=
+  p <- core_mem_swap_fwd T x y st;
+  let (st1, _) := p in
+  p0 <- core_mem_swap_back0 T x y st st1;
+  let (st2, x0) := p0 in
+  p1 <- core_mem_swap_back1 T x y st st2;
+  let (_, y0) := p1 in Return (st0, (x0, y0))
+  .
+
+(** [external::test_new_non_zero_u32] *)
+Definition test_new_non_zero_u32_fwd
+  (x : u32) (st : state) : result (state * Core_num_nonzero_non_zero_u32_t) :=
+  p <- core_num_nonzero_non_zero_u32_new_fwd x st;
+  let (st0, opt) := p in
+  p0 <- core_option_option_unwrap_fwd Core_num_nonzero_non_zero_u32_t opt st0;
+  let (st1, nzu) := p0 in Return (st1, nzu)
+  .
+
+(** [external::test_vec] *)
+Definition test_vec_fwd : result unit :=
+  let v := vec_new u32 in
+  v0 <- vec_push_back u32 v (0 %u32); let _ := v0 in Return tt
+  .
+
+(** [external::custom_swap] *)
+Definition custom_swap_fwd
+  (T : Type) (x : T) (y : T) (st : state) : result (state * T) :=
+  p <- core_mem_swap_fwd T x y st;
+  let (st0, _) := p in
+  p0 <- core_mem_swap_back0 T x y st st0;
+  let (st1, x0) := p0 in
+  p1 <- core_mem_swap_back1 T x y st st1;
+  let (st2, _) := p1 in Return (st2, x0)
+  .
+
+(** [external::custom_swap] *)
+Definition custom_swap_back
+  (T : Type) (x : T) (y : T) (st : state) (ret : T) (st0 : state) :
+  result (state * (T * T))
+  :=
+  p <- core_mem_swap_fwd T x y st;
+  let (st1, _) := p in
+  p0 <- core_mem_swap_back0 T x y st st1;
+  let (st2, _) := p0 in
+  p1 <- core_mem_swap_back1 T x y st st2;
+  let (_, y0) := p1 in Return (st0, (ret, y0))
+  .
+
+(** [external::test_custom_swap] *)
+Definition test_custom_swap_fwd
+  (x : u32) (y : u32) (st : state) : result (state * unit) :=
+  p <- custom_swap_fwd u32 x y st; let (st0, _) := p in Return (st0, tt) .
+
+(** [external::test_custom_swap] *)
+Definition test_custom_swap_back
+  (x : u32) (y : u32) (st : state) (st0 : state) :
+  result (state * (u32 * u32))
+  :=
+  p <- custom_swap_back u32 x y st (1 %u32) st0;
+  let (st1, tmp) := p in
+  let (x0, y0) := tmp in Return (st1, (x0, y0))
+  .
+
+(** [external::test_swap_non_zero] *)
+Definition test_swap_non_zero_fwd
+  (x : u32) (st : state) : result (state * u32) :=
+  p <- swap_fwd u32 x (0 %u32) st;
+  let (st0, _) := p in
+  p0 <- swap_back u32 x (0 %u32) st st0;
+  let (st1, (x0, _)) := p0 in if x0 s= 0 %u32 then Fail_ else Return (st1, x0)
+  .
+
+End External__Funs .
diff --git a/tests/coq/misc/External__Opaque.v b/tests/coq/misc/External__Opaque.v
new file mode 100644
index 00000000..19111a37
--- /dev/null
+++ b/tests/coq/misc/External__Opaque.v
@@ -0,0 +1,36 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: opaque function definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Require Export External__Types .
+Import External__Types .
+Module External__Opaque .
+
+(** [core::mem::swap] *)
+Axiom core_mem_swap_fwd :
+  forall(T : Type) , T -> T -> state -> result (state * unit)
+  .
+
+(** [core::mem::swap] *)
+Axiom core_mem_swap_back0 :
+  forall(T : Type) , T -> T -> state -> state -> result (state * T)
+  .
+
+(** [core::mem::swap] *)
+Axiom core_mem_swap_back1 :
+  forall(T : Type) , T -> T -> state -> state -> result (state * T)
+  .
+
+(** [core::num::nonzero::NonZeroU32::{14}::new] *)
+Axiom 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] *)
+Axiom core_option_option_unwrap_fwd :
+  forall(T : Type) , option T -> state -> result (state * T)
+  .
+
+End External__Opaque .
diff --git a/tests/coq/misc/External__Types.v b/tests/coq/misc/External__Types.v
new file mode 100644
index 00000000..1513ec4a
--- /dev/null
+++ b/tests/coq/misc/External__Types.v
@@ -0,0 +1,15 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [external]: type definitions *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module External__Types .
+
+(** [core::num::nonzero::NonZeroU32] *)
+Axiom Core_num_nonzero_non_zero_u32_t : Type .
+
+(** The state type used in the state-error monad *)
+Axiom state : Type.
+
+End External__Types .
diff --git a/tests/coq/misc/Makefile b/tests/coq/misc/Makefile
new file mode 100644
index 00000000..ff1ccd39
--- /dev/null
+++ b/tests/coq/misc/Makefile
@@ -0,0 +1,22 @@
+# Makefile originally taken from coq-club
+
+%: Makefile.coq phony
+	+make -f Makefile.coq $@
+
+all: Makefile.coq
+	+make -f Makefile.coq all
+
+clean: Makefile.coq
+	+make -f Makefile.coq clean
+	rm -f Makefile.coq
+
+Makefile.coq: _CoqProject Makefile
+	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
+
+_CoqProject: ;
+
+Makefile: ;
+
+phony: ;
+
+.PHONY: all clean phony
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
new file mode 100644
index 00000000..6dc41204
--- /dev/null
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -0,0 +1,510 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [no_nested_borrows] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module NoNestedBorrows .
+
+(** [no_nested_borrows::Pair] *)
+Record Pair_t (T1 T2 : Type) := mkPair_t { Pair_x : T1; Pair_y : T2; } .
+
+Arguments mkPair_t {T1} {T2} _ _  .
+Arguments Pair_x {T1} {T2}  .
+Arguments Pair_y {T1} {T2}  .
+
+(** [no_nested_borrows::List] *)
+Inductive List_t (T : Type) :=
+| ListCons : T -> List_t T -> List_t T
+| ListNil : List_t T
+.
+
+Arguments ListCons {T} _ _  .
+Arguments ListNil {T}  .
+
+(** [no_nested_borrows::One] *)
+Inductive One_t (T1 : Type) := | OneOne : T1 -> One_t T1 .
+
+Arguments OneOne {T1} _  .
+
+(** [no_nested_borrows::EmptyEnum] *)
+Inductive Empty_enum_t := | EmptyEnumEmpty : Empty_enum_t .
+
+Arguments EmptyEnumEmpty  .
+
+(** [no_nested_borrows::Enum] *)
+Inductive Enum_t := | EnumVariant1 : Enum_t | EnumVariant2 : Enum_t .
+
+Arguments EnumVariant1  .
+Arguments EnumVariant2  .
+
+(** [no_nested_borrows::EmptyStruct] *)
+Record Empty_struct_t := mkEmpty_struct_t {  } .
+
+Arguments mkEmpty_struct_t  .
+
+(** [no_nested_borrows::Sum] *)
+Inductive Sum_t (T1 T2 : Type) :=
+| SumLeft : T1 -> Sum_t T1 T2
+| SumRight : T2 -> Sum_t T1 T2
+.
+
+Arguments SumLeft {T1} {T2} _  .
+Arguments SumRight {T1} {T2} _  .
+
+(** [no_nested_borrows::neg_test] *)
+Definition neg_test_fwd (x : i32) : result i32 := i <- i32_neg x; Return i .
+
+(** [no_nested_borrows::add_test] *)
+Definition add_test_fwd (x : u32) (y : u32) : result u32 :=
+  i <- u32_add x y; Return i .
+
+(** [no_nested_borrows::subs_test] *)
+Definition subs_test_fwd (x : u32) (y : u32) : result u32 :=
+  i <- u32_sub x y; Return i .
+
+(** [no_nested_borrows::div_test] *)
+Definition div_test_fwd (x : u32) (y : u32) : result u32 :=
+  i <- u32_div x y; Return i .
+
+(** [no_nested_borrows::div_test1] *)
+Definition div_test1_fwd (x : u32) : result u32 :=
+  i <- u32_div x 2 %u32; Return i .
+
+(** [no_nested_borrows::rem_test] *)
+Definition rem_test_fwd (x : u32) (y : u32) : result u32 :=
+  i <- u32_rem x y; Return i .
+
+(** [no_nested_borrows::cast_test] *)
+Definition cast_test_fwd (x : u32) : result i32 :=
+  i <- scalar_cast U32 I32 x; Return i .
+
+(** [no_nested_borrows::test2] *)
+Definition test2_fwd : result unit :=
+  i <- u32_add 23 %u32 44 %u32; let _ := i in Return tt .
+
+(** Unit test for [no_nested_borrows::test2] *)
+Check (test2_fwd )%return.
+
+(** [no_nested_borrows::get_max] *)
+Definition get_max_fwd (x : u32) (y : u32) : result u32 :=
+  if x s>= y then Return x else Return y .
+
+(** [no_nested_borrows::test3] *)
+Definition test3_fwd : result unit :=
+  x <- get_max_fwd (4 %u32) (3 %u32);
+  y <- get_max_fwd (10 %u32) (11 %u32);
+  z <- u32_add x y; if negb (z s= 15 %u32) then Fail_ else Return tt
+  .
+
+(** Unit test for [no_nested_borrows::test3] *)
+Check (test3_fwd )%return.
+
+(** [no_nested_borrows::test_neg1] *)
+Definition test_neg1_fwd : result unit :=
+  y <- i32_neg (3 %i32); if negb (y s= (-3) %i32) then Fail_ else Return tt .
+
+(** Unit test for [no_nested_borrows::test_neg1] *)
+Check (test_neg1_fwd )%return.
+
+(** [no_nested_borrows::refs_test1] *)
+Definition refs_test1_fwd : result unit :=
+  if negb (1 %i32 s= 1 %i32) then Fail_ else Return tt .
+
+(** Unit test for [no_nested_borrows::refs_test1] *)
+Check (refs_test1_fwd )%return.
+
+(** [no_nested_borrows::refs_test2] *)
+Definition refs_test2_fwd : result unit :=
+  if negb (2 %i32 s= 2 %i32)
+  then Fail_
+  else
+    if negb (0 %i32 s= 0 %i32)
+    then Fail_
+    else
+      if negb (2 %i32 s= 2 %i32)
+      then Fail_
+      else if negb (2 %i32 s= 2 %i32) then Fail_ else Return tt
+  .
+
+(** Unit test for [no_nested_borrows::refs_test2] *)
+Check (refs_test2_fwd )%return.
+
+(** [no_nested_borrows::test_list1] *)
+Definition test_list1_fwd : result unit := Return tt .
+
+(** Unit test for [no_nested_borrows::test_list1] *)
+Check (test_list1_fwd )%return.
+
+(** [no_nested_borrows::test_box1] *)
+Definition test_box1_fwd : result unit :=
+  let b := 1 %i32 in
+  let x := b in if negb (x s= 1 %i32) then Fail_ else Return tt
+  .
+
+(** Unit test for [no_nested_borrows::test_box1] *)
+Check (test_box1_fwd )%return.
+
+(** [no_nested_borrows::copy_int] *)
+Definition copy_int_fwd (x : i32) : result i32 := Return x .
+
+(** [no_nested_borrows::test_unreachable] *)
+Definition test_unreachable_fwd (b : bool) : result unit :=
+  if b then Fail_ else Return tt .
+
+(** [no_nested_borrows::test_panic] *)
+Definition test_panic_fwd (b : bool) : result unit :=
+  if b then Fail_ else Return tt .
+
+(** [no_nested_borrows::test_copy_int] *)
+Definition test_copy_int_fwd : result unit :=
+  y <- copy_int_fwd (0 %i32); if negb (0 %i32 s= y) then Fail_ else Return tt .
+
+(** Unit test for [no_nested_borrows::test_copy_int] *)
+Check (test_copy_int_fwd )%return.
+
+(** [no_nested_borrows::is_cons] *)
+Definition is_cons_fwd (T : Type) (l : List_t T) : result bool :=
+  match l with | ListCons t l0 => Return true | ListNil => Return false end .
+
+(** [no_nested_borrows::test_is_cons] *)
+Definition test_is_cons_fwd : result unit :=
+  let l := ListNil in
+  b <- is_cons_fwd i32 (ListCons (0 %i32) l);
+  if negb b then Fail_ else Return tt
+  .
+
+(** Unit test for [no_nested_borrows::test_is_cons] *)
+Check (test_is_cons_fwd )%return.
+
+(** [no_nested_borrows::split_list] *)
+Definition split_list_fwd
+  (T : Type) (l : List_t T) : result (T * (List_t T)) :=
+  match l with | ListCons hd tl => Return (hd, tl) | ListNil => Fail_ end .
+
+(** [no_nested_borrows::test_split_list] *)
+Definition test_split_list_fwd : result unit :=
+  let l := ListNil in
+  p <- split_list_fwd i32 (ListCons (0 %i32) l);
+  let (hd, _) := p in if negb (hd s= 0 %i32) then Fail_ else Return tt
+  .
+
+(** Unit test for [no_nested_borrows::test_split_list] *)
+Check (test_split_list_fwd )%return.
+
+(** [no_nested_borrows::choose] *)
+Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T :=
+  if b then Return x else Return y .
+
+(** [no_nested_borrows::choose] *)
+Definition choose_back
+  (T : Type) (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] *)
+Definition choose_test_fwd : result unit :=
+  z <- choose_fwd i32 true (0 %i32) (0 %i32);
+  z0 <- i32_add z 1 %i32;
+  if negb (z0 s= 1 %i32)
+  then Fail_
+  else
+    (
+      p <- choose_back i32 true (0 %i32) (0 %i32) z0;
+      let (x, y) := p in
+      if negb (x s= 1 %i32)
+      then Fail_
+      else if negb (y s= 0 %i32) then Fail_ else Return tt )
+  .
+
+(** Unit test for [no_nested_borrows::choose_test] *)
+Check (choose_test_fwd )%return.
+
+(** [no_nested_borrows::test_char] *)
+Definition test_char_fwd : result char :=
+  Return (char_of_byte Coq.Init.Byte.x61) .
+
+(** [no_nested_borrows::NodeElem] *)
+Inductive Node_elem_t (T : Type) :=
+| NodeElemCons : Tree_t T -> Node_elem_t T -> Node_elem_t T
+| NodeElemNil : Node_elem_t T
+
+(** [no_nested_borrows::Tree] *)
+with Tree_t (T : Type) :=
+| TreeLeaf : T -> Tree_t T
+| TreeNode : T -> Node_elem_t T -> Tree_t T -> Tree_t T
+.
+
+Arguments NodeElemCons {T} _ _  .
+Arguments NodeElemNil {T}  .
+
+Arguments TreeLeaf {T} _  .
+Arguments TreeNode {T} _ _ _  .
+
+(** [no_nested_borrows::list_length] *)
+Fixpoint list_length_fwd (T : Type) (l : List_t T) : result u32 :=
+  match l with
+  | ListCons t l1 =>
+    i <- list_length_fwd T l1; i0 <- u32_add 1 %u32 i; Return i0
+  | ListNil => Return (0 %u32)
+  end
+  .
+
+(** [no_nested_borrows::list_nth_shared] *)
+Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
+  match l with
+  | ListCons x tl =>
+    if i s= 0 %u32
+    then Return x
+    else ( i0 <- u32_sub i 1 %u32; t <- list_nth_shared_fwd T tl i0; Return t )
+  | ListNil => Fail_
+  end
+  .
+
+(** [no_nested_borrows::list_nth_mut] *)
+Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
+  match l with
+  | ListCons x tl =>
+    if i s= 0 %u32
+    then Return x
+    else ( i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t )
+  | ListNil => Fail_
+  end
+  .
+
+(** [no_nested_borrows::list_nth_mut] *)
+Fixpoint list_nth_mut_back
+  (T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) :=
+  match l with
+  | ListCons x tl =>
+    if i s= 0 %u32
+    then Return (ListCons ret tl)
+    else
+      (
+        i0 <- u32_sub i 1 %u32;
+        tl0 <- list_nth_mut_back T tl i0 ret; Return (ListCons x tl0) )
+  | ListNil => Fail_
+  end
+  .
+
+(** [no_nested_borrows::list_rev_aux] *)
+Fixpoint list_rev_aux_fwd
+  (T : Type) (li : List_t T) (lo : List_t T) : result (List_t T) :=
+  match li with
+  | ListCons hd tl => l <- list_rev_aux_fwd T tl (ListCons hd lo); Return l
+  | ListNil => Return lo
+  end
+  .
+
+(** [no_nested_borrows::list_rev] *)
+Definition list_rev_fwd_back (T : Type) (l : List_t T) : result (List_t T) :=
+  let li := mem_replace_fwd (List_t T) l ListNil in
+  l0 <- list_rev_aux_fwd T li ListNil; Return l0
+  .
+
+(** [no_nested_borrows::test_list_functions] *)
+Definition test_list_functions_fwd : result unit :=
+  let l := ListNil in
+  let l0 := ListCons (2 %i32) l in
+  let l1 := ListCons (1 %i32) l0 in
+  i <- list_length_fwd i32 (ListCons (0 %i32) l1);
+  if negb (i s= 3 %u32)
+  then Fail_
+  else
+    (
+      i0 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (0 %u32);
+      if negb (i0 s= 0 %i32)
+      then Fail_
+      else
+        (
+          i1 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (1 %u32);
+          if negb (i1 s= 1 %i32)
+          then Fail_
+          else
+            (
+              i2 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (2 %u32);
+              if negb (i2 s= 2 %i32)
+              then Fail_
+              else
+                (
+                  ls <-
+                    list_nth_mut_back i32 (ListCons (0 %i32) l1) (1 %u32) (3
+                      %i32);
+                  i3 <- list_nth_shared_fwd i32 ls (0 %u32);
+                  if negb (i3 s= 0 %i32)
+                  then Fail_
+                  else
+                    (
+                      i4 <- list_nth_shared_fwd i32 ls (1 %u32);
+                      if negb (i4 s= 3 %i32)
+                      then Fail_
+                      else
+                        (
+                          i5 <- list_nth_shared_fwd i32 ls (2 %u32);
+                          if negb (i5 s= 2 %i32) then Fail_ else Return tt ) )
+                  ) ) ) )
+  .
+
+(** Unit test for [no_nested_borrows::test_list_functions] *)
+Check (test_list_functions_fwd )%return.
+
+(** [no_nested_borrows::id_mut_pair1] *)
+Definition id_mut_pair1_fwd
+  (T1 T2 : Type) (x : T1) (y : T2) : result (T1 * T2) :=
+  Return (x, y) .
+
+(** [no_nested_borrows::id_mut_pair1] *)
+Definition id_mut_pair1_back
+  (T1 T2 : Type) (x : T1) (y : T2) (ret : (T1 * T2)) : result (T1 * T2) :=
+  let (t, t0) := ret in Return (t, t0) .
+
+(** [no_nested_borrows::id_mut_pair2] *)
+Definition id_mut_pair2_fwd
+  (T1 T2 : Type) (p : (T1 * T2)) : result (T1 * T2) :=
+  let (t, t0) := p in Return (t, t0) .
+
+(** [no_nested_borrows::id_mut_pair2] *)
+Definition id_mut_pair2_back
+  (T1 T2 : Type) (p : (T1 * T2)) (ret : (T1 * T2)) : result (T1 * T2) :=
+  let (t, t0) := ret in Return (t, t0) .
+
+(** [no_nested_borrows::id_mut_pair3] *)
+Definition id_mut_pair3_fwd
+  (T1 T2 : Type) (x : T1) (y : T2) : result (T1 * T2) :=
+  Return (x, y) .
+
+(** [no_nested_borrows::id_mut_pair3] *)
+Definition id_mut_pair3_back'a
+  (T1 T2 : Type) (x : T1) (y : T2) (ret : T1) : result T1 :=
+  Return ret .
+
+(** [no_nested_borrows::id_mut_pair3] *)
+Definition id_mut_pair3_back'b
+  (T1 T2 : Type) (x : T1) (y : T2) (ret : T2) : result T2 :=
+  Return ret .
+
+(** [no_nested_borrows::id_mut_pair4] *)
+Definition id_mut_pair4_fwd
+  (T1 T2 : Type) (p : (T1 * T2)) : result (T1 * T2) :=
+  let (t, t0) := p in Return (t, t0) .
+
+(** [no_nested_borrows::id_mut_pair4] *)
+Definition id_mut_pair4_back'a
+  (T1 T2 : Type) (p : (T1 * T2)) (ret : T1) : result T1 :=
+  Return ret .
+
+(** [no_nested_borrows::id_mut_pair4] *)
+Definition id_mut_pair4_back'b
+  (T1 T2 : Type) (p : (T1 * T2)) (ret : T2) : result T2 :=
+  Return ret .
+
+(** [no_nested_borrows::StructWithTuple] *)
+Record Struct_with_tuple_t (T1 T2 : Type) :=
+mkStruct_with_tuple_t
+{
+  Struct_with_tuple_p : (T1 * T2);
+}
+.
+
+Arguments mkStruct_with_tuple_t {T1} {T2} _  .
+Arguments Struct_with_tuple_p {T1} {T2}  .
+
+(** [no_nested_borrows::new_tuple1] *)
+Definition new_tuple1_fwd : result (Struct_with_tuple_t u32 u32) :=
+  Return (mkStruct_with_tuple_t (1 %u32, 2 %u32)) .
+
+(** [no_nested_borrows::new_tuple2] *)
+Definition new_tuple2_fwd : result (Struct_with_tuple_t i16 i16) :=
+  Return (mkStruct_with_tuple_t (1 %i16, 2 %i16)) .
+
+(** [no_nested_borrows::new_tuple3] *)
+Definition new_tuple3_fwd : result (Struct_with_tuple_t u64 i64) :=
+  Return (mkStruct_with_tuple_t (1 %u64, 2 %i64)) .
+
+(** [no_nested_borrows::StructWithPair] *)
+Record Struct_with_pair_t (T1 T2 : Type) :=
+mkStruct_with_pair_t
+{
+  Struct_with_pair_p : Pair_t T1 T2;
+}
+.
+
+Arguments mkStruct_with_pair_t {T1} {T2} _  .
+Arguments Struct_with_pair_p {T1} {T2}  .
+
+(** [no_nested_borrows::new_pair1] *)
+Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) :=
+  Return (mkStruct_with_pair_t (mkPair_t (1 %u32) (2 %u32))) .
+
+(** [no_nested_borrows::test_constants] *)
+Definition test_constants_fwd : result unit :=
+  swt <- new_tuple1_fwd;
+  match swt with
+  | mkStruct_with_tuple_t p =>
+    let (i, _) := p in
+    if negb (i s= 1 %u32)
+    then Fail_
+    else
+      (
+        swt0 <- new_tuple2_fwd;
+        match swt0 with
+        | mkStruct_with_tuple_t p0 =>
+          let (i0, _) := p0 in
+          if negb (i0 s= 1 %i16)
+          then Fail_
+          else
+            (
+              swt1 <- new_tuple3_fwd;
+              match swt1 with
+              | mkStruct_with_tuple_t p1 =>
+                let (i1, _) := p1 in
+                if negb (i1 s= 1 %u64)
+                then Fail_
+                else
+                  (
+                    swp <- new_pair1_fwd;
+                    match swp with
+                    | mkStruct_with_pair_t p2 =>
+                      match p2 with
+                      | mkPair_t i2 i3 =>
+                        if negb (i2 s= 1 %u32) then Fail_ else Return tt
+                      end
+                    end )
+              end )
+        end )
+  end
+  .
+
+(** Unit test for [no_nested_borrows::test_constants] *)
+Check (test_constants_fwd )%return.
+
+(** [no_nested_borrows::test_weird_borrows1] *)
+Definition test_weird_borrows1_fwd : result unit := Return tt .
+
+(** Unit test for [no_nested_borrows::test_weird_borrows1] *)
+Check (test_weird_borrows1_fwd )%return.
+
+(** [no_nested_borrows::test_mem_replace] *)
+Definition test_mem_replace_fwd_back (px : u32) : result u32 :=
+  let y := mem_replace_fwd u32 px (1 %u32) in
+  if negb (y s= 0 %u32) then Fail_ else Return (2 %u32)
+  .
+
+(** [no_nested_borrows::test_shared_borrow_bool1] *)
+Definition test_shared_borrow_bool1_fwd (b : bool) : result u32 :=
+  if b then Return (0 %u32) else Return (1 %u32) .
+
+(** [no_nested_borrows::test_shared_borrow_bool2] *)
+Definition test_shared_borrow_bool2_fwd : result u32 := Return (0 %u32) .
+
+(** [no_nested_borrows::test_shared_borrow_enum1] *)
+Definition test_shared_borrow_enum1_fwd (l : List_t u32) : result u32 :=
+  match l with
+  | ListCons i l0 => Return (1 %u32)
+  | ListNil => Return (0 %u32)
+  end
+  .
+
+(** [no_nested_borrows::test_shared_borrow_enum2] *)
+Definition test_shared_borrow_enum2_fwd : result u32 := Return (0 %u32) .
+
+End NoNestedBorrows .
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
new file mode 100644
index 00000000..5d9598eb
--- /dev/null
+++ b/tests/coq/misc/Paper.v
@@ -0,0 +1,114 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [paper] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Primitives_scope.
+Module Paper .
+
+(** [paper::ref_incr] *)
+Definition ref_incr_fwd_back (x : i32) : result i32 :=
+  x0 <- i32_add x 1 %i32; Return x0 .
+
+(** [paper::test_incr] *)
+Definition test_incr_fwd : result unit :=
+  x <- ref_incr_fwd_back (0 %i32);
+  if negb (x s= 1 %i32) then Fail_ else Return tt
+  .
+
+(** Unit test for [paper::test_incr] *)
+Check (test_incr_fwd )%return.
+
+(** [paper::choose] *)
+Definition choose_fwd (T : Type) (b : bool) (x : T) (y : T) : result T :=
+  if b then Return x else Return y .
+
+(** [paper::choose] *)
+Definition choose_back
+  (T : Type) (b : bool) (x : T) (y : T) (ret : T) : result (T * T) :=
+  if b then Return (ret, y) else Return (x, ret) .
+
+(** [paper::test_choose] *)
+Definition test_choose_fwd : result unit :=
+  z <- choose_fwd i32 true (0 %i32) (0 %i32);
+  z0 <- i32_add z 1 %i32;
+  if negb (z0 s= 1 %i32)
+  then Fail_
+  else
+    (
+      p <- choose_back i32 true (0 %i32) (0 %i32) z0;
+      let (x, y) := p in
+      if negb (x s= 1 %i32)
+      then Fail_
+      else if negb (y s= 0 %i32) then Fail_ else Return tt )
+  .
+
+(** Unit test for [paper::test_choose] *)
+Check (test_choose_fwd )%return.
+
+(** [paper::List] *)
+Inductive List_t (T : Type) :=
+| ListCons : T -> List_t T -> List_t T
+| ListNil : List_t T
+.
+
+Arguments ListCons {T} _ _  .
+Arguments ListNil {T}  .
+
+(** [paper::list_nth_mut] *)
+Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
+  match l with
+  | ListCons x tl =>
+    if i s= 0 %u32
+    then Return x
+    else ( i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t )
+  | ListNil => Fail_
+  end
+  .
+
+(** [paper::list_nth_mut] *)
+Fixpoint list_nth_mut_back
+  (T : Type) (l : List_t T) (i : u32) (ret : T) : result (List_t T) :=
+  match l with
+  | ListCons x tl =>
+    if i s= 0 %u32
+    then Return (ListCons ret tl)
+    else
+      (
+        i0 <- u32_sub i 1 %u32;
+        tl0 <- list_nth_mut_back T tl i0 ret; Return (ListCons x tl0) )
+  | ListNil => Fail_
+  end
+  .
+
+(** [paper::sum] *)
+Fixpoint sum_fwd (l : List_t i32) : result i32 :=
+  match l with
+  | ListCons x tl => i <- sum_fwd tl; i0 <- i32_add x i; Return i0
+  | ListNil => Return (0 %i32)
+  end
+  .
+
+(** [paper::test_nth] *)
+Definition test_nth_fwd : result unit :=
+  let l := ListNil in
+  let l0 := ListCons (3 %i32) l in
+  let l1 := ListCons (2 %i32) l0 in
+  x <- list_nth_mut_fwd i32 (ListCons (1 %i32) l1) (2 %u32);
+  x0 <- i32_add x 1 %i32;
+  l2 <- list_nth_mut_back i32 (ListCons (1 %i32) l1) (2 %u32) x0;
+  i <- sum_fwd l2; if negb (i s= 7 %i32) then Fail_ else Return tt
+  .
+
+(** Unit test for [paper::test_nth] *)
+Check (test_nth_fwd )%return.
+
+(** [paper::call_choose] *)
+Definition call_choose_fwd (p : (u32 * u32)) : result u32 :=
+  let (px, py) := p in
+  pz <- choose_fwd u32 true px py;
+  pz0 <- u32_add pz 1 %u32;
+  p0 <- choose_back u32 true px py pz0; let (px0, _) := p0 in Return px0
+  .
+
+End Paper .
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
new file mode 100644
index 00000000..c27b8aed
--- /dev/null
+++ b/tests/coq/misc/Primitives.v
@@ -0,0 +1,478 @@
+Require Import Lia.
+Require Coq.Strings.Ascii.
+Require Coq.Strings.String.
+Require Import Coq.Program.Equality.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.ZArith.Znat.
+Require Import List.
+Import ListNotations.
+
+Module Primitives.
+
+  (* TODO: use more *)
+Declare Scope Primitives_scope.
+
+(*** Result *)
+  
+Inductive result A :=
+  | Return : A -> result A
+  | Fail_ : result A.
+
+Arguments Return {_} a.
+Arguments Fail_ {_}.
+
+Definition bind {A B} (m: result A) (f: A -> result B) : result B :=
+  match m with
+  | Fail_ => Fail_
+  | Return x => f x
+  end.
+
+Definition return_ {A: Type} (x: A) : result A := Return x .
+Definition fail_ {A: Type} : result A := Fail_ .
+
+Notation "x <- c1 ; c2" := (bind c1 (fun x => c2))
+  (at level 61, c1 at next level, right associativity).
+
+(** Monadic assert *)
+Definition massert (b: bool) : result unit :=
+  if b then Return tt else Fail_.
+
+(** Normalize and unwrap a successful result (used for globals) *)
+Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A :=
+  match a as r return (r = Return x -> A) with
+  | Return a' => fun _  => a'
+  | Fail_     => fun p' =>
+      False_rect _ (eq_ind Fail_
+          (fun e : result A =>
+          match e with
+          | Return _ => False
+          | Fail_ => True
+          end)
+        I (Return x) p')
+  end p.
+
+Notation "x %global" := (eval_result_refl x eq_refl) (at level 40).
+Notation "x %return" := (eval_result_refl x eq_refl) (at level 40).
+
+(* Sanity check *)
+Check (if true then Return (1 + 2) else Fail_)%global = 3.
+
+(*** Misc *)
+
+
+Definition string := Coq.Strings.String.string.
+Definition char := Coq.Strings.Ascii.ascii.
+Definition char_of_byte := Coq.Strings.Ascii.ascii_of_byte.
+
+Definition mem_replace_fwd (a : Type) (x : a) (y : a) : a := x .
+Definition mem_replace_back (a : Type) (x : a) (y : a) : a := y .
+
+(*** Scalars *)
+
+Definition i8_min   : Z := -128%Z.
+Definition i8_max   : Z := 127%Z.
+Definition i16_min  : Z := -32768%Z.
+Definition i16_max  : Z := 32767%Z.
+Definition i32_min  : Z := -2147483648%Z.
+Definition i32_max  : Z := 2147483647%Z.
+Definition i64_min  : Z := -9223372036854775808%Z.
+Definition i64_max  : Z := 9223372036854775807%Z.
+Definition i128_min : Z := -170141183460469231731687303715884105728%Z.
+Definition i128_max : Z := 170141183460469231731687303715884105727%Z.
+Definition u8_min   : Z := 0%Z.
+Definition u8_max   : Z := 255%Z.
+Definition u16_min  : Z := 0%Z.
+Definition u16_max  : Z := 65535%Z.
+Definition u32_min  : Z := 0%Z.
+Definition u32_max  : Z := 4294967295%Z.
+Definition u64_min  : Z := 0%Z.
+Definition u64_max  : Z := 18446744073709551615%Z.
+Definition u128_min : Z := 0%Z.
+Definition u128_max : Z := 340282366920938463463374607431768211455%Z.
+
+(** The bounds of [isize] and [usize] vary with the architecture. *)
+Axiom isize_min : Z.
+Axiom isize_max : Z.
+Definition usize_min : Z := 0%Z.
+Axiom usize_max : Z.
+
+Open Scope Z_scope.
+
+(** We provide those lemmas to reason about the bounds of [isize] and [usize] *)
+Axiom isize_min_bound : isize_min <= i32_min.
+Axiom isize_max_bound : i32_max <= isize_max.
+Axiom usize_max_bound : u32_max <= usize_max.
+
+Inductive scalar_ty :=
+  | Isize
+  | I8
+  | I16
+  | I32
+  | I64
+  | I128
+  | Usize
+  | U8
+  | U16
+  | U32
+  | U64
+  | U128
+.
+
+Definition scalar_min (ty: scalar_ty) : Z :=
+  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
+end.
+
+Definition scalar_max (ty: scalar_ty) : Z :=
+  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
+end.
+
+(** We use the following conservative bounds to make sure we can compute bound
+    checks in most situations *)
+Definition scalar_min_cons (ty: scalar_ty) : Z :=
+  match ty with
+  | Isize => i32_min
+  | Usize => u32_min
+  | _ => scalar_min ty
+end.
+
+Definition scalar_max_cons (ty: scalar_ty) : Z :=
+  match ty with
+  | Isize => i32_max
+  | Usize => u32_max
+  | _ => scalar_max ty
+end.
+
+Lemma scalar_min_cons_valid : forall ty, scalar_min ty <= scalar_min_cons ty .
+Proof.
+  destruct ty; unfold scalar_min_cons, scalar_min; try lia.
+  - pose isize_min_bound; lia.
+  - apply Z.le_refl.
+Qed.
+
+Lemma scalar_max_cons_valid : forall ty, scalar_max ty >= scalar_max_cons ty .
+Proof.
+  destruct ty; unfold scalar_max_cons, scalar_max; try lia.
+  - pose isize_max_bound; lia.
+  - pose usize_max_bound. lia.
+Qed.
+
+Definition scalar (ty: scalar_ty) : Type :=
+ { x: Z | scalar_min ty <= x <= scalar_max ty }.
+
+Definition to_Z {ty} (x: scalar ty) : Z := proj1_sig x.
+
+(** Bounds checks: we start by using the conservative bounds, to make sure we
+    can compute in most situations, then we use the real bounds (for [isize]
+    and [usize]). *)
+Definition scalar_ge_min (ty: scalar_ty) (x: Z) : bool :=
+  Z.leb (scalar_min_cons ty) x || Z.leb (scalar_min ty) x.
+
+Definition scalar_le_max (ty: scalar_ty) (x: Z) : bool :=
+  Z.leb x (scalar_max_cons ty) || Z.leb x (scalar_max ty).
+
+Lemma scalar_ge_min_valid (ty: scalar_ty) (x: Z) :
+  scalar_ge_min ty x = true -> scalar_min ty <= x .
+Proof.
+  unfold scalar_ge_min.
+  pose (scalar_min_cons_valid ty).
+  lia.
+Qed.
+
+Lemma scalar_le_max_valid (ty: scalar_ty) (x: Z) :
+  scalar_le_max ty x = true -> x <= scalar_max ty .
+Proof.
+  unfold scalar_le_max.
+  pose (scalar_max_cons_valid ty).
+  lia.
+Qed.
+
+Definition scalar_in_bounds (ty: scalar_ty) (x: Z) : bool :=
+  scalar_ge_min ty x && scalar_le_max ty x .
+
+Lemma scalar_in_bounds_valid (ty: scalar_ty) (x: Z) :
+  scalar_in_bounds ty x = true -> scalar_min ty <= x <= scalar_max ty .
+Proof.
+  unfold scalar_in_bounds.
+  intros H.
+  destruct (scalar_ge_min ty x) eqn:Hmin.
+  - destruct (scalar_le_max ty x) eqn:Hmax.
+    + pose (scalar_ge_min_valid ty x Hmin).
+      pose (scalar_le_max_valid ty x Hmax).
+      lia.
+    + inversion H.
+  - inversion H.
+Qed.
+
+Import Sumbool.
+
+Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) :=
+  match sumbool_of_bool (scalar_in_bounds ty x) with
+  | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H))
+  | right _ => Fail_
+  end.
+
+Definition scalar_add {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x + to_Z y).
+
+Definition scalar_sub {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x - to_Z y).
+
+Definition scalar_mul {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x * to_Z y).
+
+Definition scalar_div {ty} (x y: scalar ty) : result (scalar ty) :=
+  if to_Z y =? 0 then Fail_ else
+  mk_scalar ty (to_Z x / to_Z y).
+
+Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (Z.rem (to_Z x) (to_Z y)).
+  
+Definition scalar_neg {ty} (x: scalar ty) : result (scalar ty) := mk_scalar ty (-(to_Z x)).
+
+(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+(* TODO: check the semantics of casts in Rust *)
+Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) :=
+  mk_scalar tgt_ty (to_Z x).
+
+(** Comparisons *)
+Print Z.leb .
+
+Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
+  Z.leb (to_Z x) (to_Z y) .
+
+Definition scalar_ltb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
+  Z.ltb (to_Z x) (to_Z y) .
+
+Definition scalar_geb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
+  Z.geb (to_Z x) (to_Z y) .
+
+Definition scalar_gtb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
+  Z.gtb (to_Z x) (to_Z y) .
+
+Definition scalar_eqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
+  Z.eqb (to_Z x) (to_Z y) .
+
+Definition scalar_neqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
+  negb (Z.eqb (to_Z x) (to_Z y)) .
+
+
+(** The scalar types *)
+Definition isize := scalar Isize.
+Definition i8    := scalar I8.
+Definition i16   := scalar I16.
+Definition i32   := scalar I32.
+Definition i64   := scalar I64.
+Definition i128  := scalar I128.
+Definition usize := scalar Usize.
+Definition u8    := scalar U8.
+Definition u16   := scalar U16.
+Definition u32   := scalar U32.
+Definition u64   := scalar U64.
+Definition u128  := scalar U128.
+
+(** Negaion *)
+Definition isize_neg := @scalar_neg Isize.
+Definition i8_neg    := @scalar_neg I8.
+Definition i16_neg   := @scalar_neg I16.
+Definition i32_neg   := @scalar_neg I32.
+Definition i64_neg   := @scalar_neg I64.
+Definition i128_neg  := @scalar_neg I128.
+
+(** Division *)
+Definition isize_div := @scalar_div Isize.
+Definition i8_div    := @scalar_div I8.
+Definition i16_div   := @scalar_div I16.
+Definition i32_div   := @scalar_div I32.
+Definition i64_div   := @scalar_div I64.
+Definition i128_div  := @scalar_div I128.
+Definition usize_div := @scalar_div Usize.
+Definition u8_div    := @scalar_div U8.
+Definition u16_div   := @scalar_div U16.
+Definition u32_div   := @scalar_div U32.
+Definition u64_div   := @scalar_div U64.
+Definition u128_div  := @scalar_div U128.
+
+(** Remainder *)
+Definition isize_rem := @scalar_rem Isize.
+Definition i8_rem    := @scalar_rem I8.
+Definition i16_rem   := @scalar_rem I16.
+Definition i32_rem   := @scalar_rem I32.
+Definition i64_rem   := @scalar_rem I64.
+Definition i128_rem  := @scalar_rem I128.
+Definition usize_rem := @scalar_rem Usize.
+Definition u8_rem    := @scalar_rem U8.
+Definition u16_rem   := @scalar_rem U16.
+Definition u32_rem   := @scalar_rem U32.
+Definition u64_rem   := @scalar_rem U64.
+Definition u128_rem  := @scalar_rem U128.
+
+(** Addition *)
+Definition isize_add := @scalar_add Isize.
+Definition i8_add    := @scalar_add I8.
+Definition i16_add   := @scalar_add I16.
+Definition i32_add   := @scalar_add I32.
+Definition i64_add   := @scalar_add I64.
+Definition i128_add  := @scalar_add I128.
+Definition usize_add := @scalar_add Usize.
+Definition u8_add    := @scalar_add U8.
+Definition u16_add   := @scalar_add U16.
+Definition u32_add   := @scalar_add U32.
+Definition u64_add   := @scalar_add U64.
+Definition u128_add  := @scalar_add U128.
+
+(** Substraction *)
+Definition isize_sub := @scalar_sub Isize.
+Definition i8_sub    := @scalar_sub I8.
+Definition i16_sub   := @scalar_sub I16.
+Definition i32_sub   := @scalar_sub I32.
+Definition i64_sub   := @scalar_sub I64.
+Definition i128_sub  := @scalar_sub I128.
+Definition usize_sub := @scalar_sub Usize.
+Definition u8_sub    := @scalar_sub U8.
+Definition u16_sub   := @scalar_sub U16.
+Definition u32_sub   := @scalar_sub U32.
+Definition u64_sub   := @scalar_sub U64.
+Definition u128_sub  := @scalar_sub U128.
+
+(** Multiplication *)
+Definition isize_mul := @scalar_mul Isize.
+Definition i8_mul    := @scalar_mul I8.
+Definition i16_mul   := @scalar_mul I16.
+Definition i32_mul   := @scalar_mul I32.
+Definition i64_mul   := @scalar_mul I64.
+Definition i128_mul  := @scalar_mul I128.
+Definition usize_mul := @scalar_mul Usize.
+Definition u8_mul    := @scalar_mul U8.
+Definition u16_mul   := @scalar_mul U16.
+Definition u32_mul   := @scalar_mul U32.
+Definition u64_mul   := @scalar_mul U64.
+Definition u128_mul  := @scalar_mul U128.
+
+(** Small utility *)
+Definition usize_to_nat (x: usize) : nat := Z.to_nat (to_Z x).
+
+(** Notations *)
+Notation "x %isize" := ((mk_scalar Isize x)%return) (at level 9).
+Notation "x %i8"    := ((mk_scalar I8    x)%return) (at level 9).
+Notation "x %i16"   := ((mk_scalar I16   x)%return) (at level 9).
+Notation "x %i32"   := ((mk_scalar I32   x)%return) (at level 9).
+Notation "x %i64"   := ((mk_scalar I64   x)%return) (at level 9).
+Notation "x %i128"  := ((mk_scalar I128  x)%return) (at level 9).
+Notation "x %usize" := ((mk_scalar Usize x)%return) (at level 9).
+Notation "x %u8"    := ((mk_scalar U8    x)%return) (at level 9).
+Notation "x %u16"   := ((mk_scalar U16   x)%return) (at level 9).
+Notation "x %u32"   := ((mk_scalar U32   x)%return) (at level 9).
+Notation "x %u64"   := ((mk_scalar U64   x)%return) (at level 9).
+Notation "x %u128"  := ((mk_scalar U128  x)%return) (at level 9).
+
+Notation "x s= y" := (scalar_eqb x y)  (at level 80) : Primitives_scope.
+Notation "x s<> y" := (scalar_neqb x y) (at level 80) : Primitives_scope.
+Notation "x s<= y" := (scalar_leb x y)  (at level 80) : Primitives_scope.
+Notation "x s< y" := (scalar_ltb x y)  (at level 80) : Primitives_scope.
+Notation "x s>= y" := (scalar_geb x y)  (at level 80) : Primitives_scope.
+Notation "x s> y" := (scalar_gtb x y)  (at level 80) : Primitives_scope.
+
+(*** Vectors *)
+
+Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }.
+
+Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v.
+
+Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+
+Lemma le_0_usize_max : 0 <= usize_max.
+Proof.
+  pose (H := usize_max_bound).
+  unfold u32_max in H.
+  lia.
+Qed.
+
+Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max).
+
+Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max.
+Proof.
+  unfold vec_length, usize_min.
+  split.
+  - lia.
+  - apply (proj2_sig v).
+Qed.
+
+Definition vec_len (T: Type) (v: vec T) : usize :=
+  exist _ (vec_length v) (vec_len_in_usize v).
+
+Fixpoint list_update {A} (l: list A) (n: nat) (a: A)
+  : list A :=
+  match l with
+  | []     => []
+  | x :: t => match n with
+    | 0%nat => a :: t
+    | S m => x :: (list_update t m a)
+end end.
+
+Definition vec_bind {A B} (v: vec A) (f: list A -> result (list B)) : result (vec B) :=
+  l <- f (vec_to_list v) ;
+  match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with
+  | left H => Return (exist _ l (scalar_le_max_valid _ _ H))
+  | right _ => Fail_
+  end.
+
+(* The **forward** function shouldn't be used *)
+Definition vec_push_fwd (T: Type) (v: vec T) (x: T) : unit := tt.
+
+Definition vec_push_back (T: Type) (v: vec T) (x: T) : result (vec T) :=
+  vec_bind v (fun l => Return (l ++ [x])).
+
+(* The **forward** function shouldn't be used *)
+Definition vec_insert_fwd (T: Type) (v: vec T) (i: usize) (x: T) : result unit :=
+  if to_Z i <? vec_length v then Return tt else Fail_.
+
+Definition vec_insert_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) :=
+  vec_bind v (fun l =>
+    if to_Z i <? Z.of_nat (length l)
+    then Return (list_update l (usize_to_nat i) x)
+    else Fail_).
+
+(* The **backward** function shouldn't be used *)
+Definition vec_index_fwd (T: Type) (v: vec T) (i: usize) : result T :=
+  match nth_error (vec_to_list v) (usize_to_nat i) with
+  | Some n => Return n
+  | None   => Fail_
+  end.
+
+Definition vec_index_back (T: Type) (v: vec T) (i: usize) (x: T) : result unit :=
+  if to_Z i <? vec_length v then Return tt else Fail_.
+
+(* The **backward** function shouldn't be used *)
+Definition vec_index_mut_fwd (T: Type) (v: vec T) (i: usize) : result T :=
+  match nth_error (vec_to_list v) (usize_to_nat i) with
+  | Some n => Return n
+  | None   => Fail_
+  end.
+
+Definition vec_index_mut_back (T: Type) (v: vec T) (i: usize) (x: T) : result (vec T) :=
+  vec_bind v (fun l =>
+    if to_Z i <? Z.of_nat (length l)
+    then Return (list_update l (usize_to_nat i) x)
+    else Fail_).
+
+End Primitives.
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
new file mode 100644
index 00000000..7f4981fa
--- /dev/null
+++ b/tests/coq/misc/_CoqProject
@@ -0,0 +1,12 @@
+-R . Lib
+-arg -w
+-arg all
+
+Primitives.v
+
+Constants.v
+External__Funs.v
+External__Opaque.v
+External__Types.v
+NoNestedBorrows.v
+Paper.v
\ No newline at end of file
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 8161e7cd..36dea95b 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -228,59 +228,6 @@ 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