Update the tests for External

20 files changed, 470 insertions, 237 deletions

diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index e84d65ce..5ffda12f 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -489,6 +489,81 @@ Definition core_i64_max   := i64_max %i64.
 Definition core_i128_max  := i64_max %i128.
 Axiom core_isize_max : isize. (** TODO *)
 
+(*** core *)
+
+(** Trait declaration: [core::clone::Clone] *)
+Record core_clone_Clone (self : Type) := {
+  clone : self -> result self
+}.
+
+Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b.
+
+Definition core_clone_CloneBool : core_clone_Clone bool := {|
+  clone := fun b => Ok (core_clone_impls_CloneBool_clone b)
+|}.
+
+Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x.
+Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x.
+Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x.
+Definition core_clone_impls_CloneU32_clone (x : u32) : u32 := x.
+Definition core_clone_impls_CloneU64_clone (x : u64) : u64 := x.
+Definition core_clone_impls_CloneU128_clone (x : u128) : u128 := x.
+
+Definition core_clone_impls_CloneIsize_clone (x : isize) : isize := x.
+Definition core_clone_impls_CloneI8_clone (x : i8) : i8 := x.
+Definition core_clone_impls_CloneI16_clone (x : i16) : i16 := x.
+Definition core_clone_impls_CloneI32_clone (x : i32) : i32 := x.
+Definition core_clone_impls_CloneI64_clone (x : i64) : i64 := x.
+Definition core_clone_impls_CloneI128_clone (x : i128) : i128 := x.
+
+Definition core_clone_CloneUsize : core_clone_Clone usize := {|
+  clone := fun x => Ok (core_clone_impls_CloneUsize_clone x)
+|}.
+
+Definition core_clone_CloneU8 : core_clone_Clone u8 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU8_clone x)
+|}.
+
+Definition core_clone_CloneU16 : core_clone_Clone u16 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU16_clone x)
+|}.
+
+Definition core_clone_CloneU32 : core_clone_Clone u32 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU32_clone x)
+|}.
+
+Definition core_clone_CloneU64 : core_clone_Clone u64 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU64_clone x)
+|}.
+
+Definition core_clone_CloneU128 : core_clone_Clone u128 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU128_clone x)
+|}.
+
+Definition core_clone_CloneIsize : core_clone_Clone isize := {|
+  clone := fun x => Ok (core_clone_impls_CloneIsize_clone x)
+|}.
+
+Definition core_clone_CloneI8 : core_clone_Clone i8 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI8_clone x)
+|}.
+
+Definition core_clone_CloneI16 : core_clone_Clone i16 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI16_clone x)
+|}.
+
+Definition core_clone_CloneI32 : core_clone_Clone i32 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI32_clone x)
+|}.
+
+Definition core_clone_CloneI64 : core_clone_Clone i64 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI64_clone x)
+|}.
+
+Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
+|}.
+
 (*** core::ops *)
 
 (* Trait declaration: [core::ops::index::Index] *)
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index acdb09dc..c7c9f9db 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -465,6 +465,81 @@ let i64_shr #ty = scalar_shr #I64 #ty
 let i128_shr #ty = scalar_shr #I128 #ty
 let isize_shr #ty = scalar_shr #Isize #ty
 
+(*** core *)
+
+/// Trait declaration: [core::clone::Clone]
+noeq type core_clone_Clone (self : Type0) = {
+  clone : self → result self
+}
+
+let core_clone_impls_CloneBool_clone (b : bool) : bool = b
+
+let core_clone_CloneBool : core_clone_Clone bool = {
+  clone = fun b -> Ok (core_clone_impls_CloneBool_clone b)
+}
+
+let core_clone_impls_CloneUsize_clone (x : usize) : usize = x
+let core_clone_impls_CloneU8_clone (x : u8) : u8 = x
+let core_clone_impls_CloneU16_clone (x : u16) : u16 = x
+let core_clone_impls_CloneU32_clone (x : u32) : u32 = x
+let core_clone_impls_CloneU64_clone (x : u64) : u64 = x
+let core_clone_impls_CloneU128_clone (x : u128) : u128 = x
+
+let core_clone_impls_CloneIsize_clone (x : isize) : isize = x
+let core_clone_impls_CloneI8_clone (x : i8) : i8 = x
+let core_clone_impls_CloneI16_clone (x : i16) : i16 = x
+let core_clone_impls_CloneI32_clone (x : i32) : i32 = x
+let core_clone_impls_CloneI64_clone (x : i64) : i64 = x
+let core_clone_impls_CloneI128_clone (x : i128) : i128 = x
+
+let core_clone_CloneUsize : core_clone_Clone usize = {
+  clone = fun x -> Ok (core_clone_impls_CloneUsize_clone x)
+}
+
+let core_clone_CloneU8 : core_clone_Clone u8 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU8_clone x)
+}
+
+let core_clone_CloneU16 : core_clone_Clone u16 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU16_clone x)
+}
+
+let core_clone_CloneU32 : core_clone_Clone u32 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU32_clone x)
+}
+
+let core_clone_CloneU64 : core_clone_Clone u64 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU64_clone x)
+}
+
+let core_clone_CloneU128 : core_clone_Clone u128 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU128_clone x)
+}
+
+let core_clone_CloneIsize : core_clone_Clone isize = {
+  clone = fun x -> Ok (core_clone_impls_CloneIsize_clone x)
+}
+
+let core_clone_CloneI8 : core_clone_Clone i8 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI8_clone x)
+}
+
+let core_clone_CloneI16 : core_clone_Clone i16 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI16_clone x)
+}
+
+let core_clone_CloneI32 : core_clone_Clone i32 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI32_clone x)
+}
+
+let core_clone_CloneI64 : core_clone_Clone i64 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI64_clone x)
+}
+
+let core_clone_CloneI128 : core_clone_Clone i128 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
+}
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index 41d4a7bd..c4f70f75 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -12,64 +12,33 @@ Require Import External_FunsExternal.
 Include External_FunsExternal.
 Module External_Funs.
 
-(** [external::swap]:
-    Source: 'src/external.rs', lines 6:0-6:46 *)
-Definition swap
-  (T : Type) (x : T) (y : T) (st : state) : result (state * (T * T)) :=
-  core_mem_swap T x y st
+(** Trait implementation: [core::marker::{(core::marker::Copy for u32)#40}]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 47:29-47:65
+    Name pattern: core::marker::Copy<u32> *)
+Definition core_marker_CopyU32 : core_marker_Copy_t u32 := {|
+  core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst := core_clone_CloneU32;
+|}.
+
+(** [external::use_get]:
+    Source: 'src/external.rs', lines 5:0-5:37 *)
+Definition use_get
+  (rc : core_cell_Cell_t u32) (st : state) : result (state * u32) :=
+  core_cell_Cell_get u32 core_marker_CopyU32 rc st
 .
 
-(** [external::test_new_non_zero_u32]:
-    Source: 'src/external.rs', lines 11:0-11:60 *)
-Definition test_new_non_zero_u32
-  (x : u32) (st : state) : result (state * core_num_nonzero_NonZeroU32_t) :=
-  p <- core_num_nonzero_NonZeroU32_new x st;
-  let (st1, o) := p in
-  core_option_Option_unwrap core_num_nonzero_NonZeroU32_t o st1
-.
-
-(** [external::test_vec]:
-    Source: 'src/external.rs', lines 17:0-17:17 *)
-Definition test_vec : result unit :=
-  _ <- alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0%u32; Ok tt
-.
-
-(** Unit test for [external::test_vec] *)
-Check (test_vec )%return.
-
-(** [external::custom_swap]:
-    Source: 'src/external.rs', lines 24:0-24:66 *)
-Definition custom_swap
-  (T : Type) (x : T) (y : T) (st : state) :
-  result (state * (T * (T -> state -> result (state * (T * T)))))
+(** [external::incr]:
+    Source: 'src/external.rs', lines 9:0-9:31 *)
+Definition incr
+  (rc : core_cell_Cell_t u32) (st : state) :
+  result (state * (core_cell_Cell_t u32))
   :=
-  p <- core_mem_swap T x y st;
-  let (st1, p1) := p in
-  let (x1, y1) := p1 in
-  let back := fun (ret : T) (st2 : state) => Ok (st2, (ret, y1)) in
-  Ok (st1, (x1, back))
-.
-
-(** [external::test_custom_swap]:
-    Source: 'src/external.rs', lines 29:0-29:59 *)
-Definition test_custom_swap
-  (x : u32) (y : u32) (st : state) : result (state * (u32 * u32)) :=
-  p <- custom_swap u32 x y st;
-  let (st1, p1) := p in
-  let (_, custom_swap_back) := p1 in
-  p2 <- custom_swap_back 1%u32 st1;
-  let (_, p3) := p2 in
-  let (x1, y1) := p3 in
-  Ok (st1, (x1, y1))
-.
-
-(** [external::test_swap_non_zero]:
-    Source: 'src/external.rs', lines 35:0-35:44 *)
-Definition test_swap_non_zero (x : u32) (st : state) : result (state * u32) :=
-  p <- swap u32 x 0%u32 st;
+  p <- core_cell_Cell_get_mut u32 rc st;
   let (st1, p1) := p in
-  let (x1, _) := p1 in
-  if x1 s= 0%u32 then Fail_ Failure else Ok (st1, x1)
+  let (i, get_mut_back) := p1 in
+  i1 <- u32_add i 1%u32;
+  p2 <- get_mut_back i1 st1;
+  let (_, rc1) := p2 in
+  Ok (st1, rc1)
 .
 
 End External_Funs.
diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v
index 39f4a60e..a25d9c33 100644
--- a/tests/coq/misc/External_FunsExternal.v
+++ b/tests/coq/misc/External_FunsExternal.v
@@ -9,22 +9,15 @@ Require Export External_Types.
 Include External_Types.
 Module External_FunsExternal.
 
-(** [core::mem::swap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
-Definition core_mem_swap (T : Type) (x : T) (y : T) (s : state) :=
-  Ok (s, (y, x))
+Axiom core_cell_Cell_get :
+  forall(T : Type) (markerCopyInst : core_marker_Copy_t T),
+        core_cell_Cell_t T -> state -> result (state * T)
 .
 
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
-Axiom core_num_nonzero_NonZeroU32_new
-  : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
-.
-
-(** [core::option::{core::option::Option<T>}::unwrap]: forward function
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
-Axiom core_option_Option_unwrap :
-  forall(T : Type), option T -> state -> result (state * T)
+Axiom core_cell_Cell_get_mut :
+  forall(T : Type),
+        core_cell_Cell_t T -> state -> result (state * (T * (T -> state ->
+          result (state * (core_cell_Cell_t T)))))
 .
 
 End External_FunsExternal.
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 24dd2d47..b3e4a129 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -11,25 +11,21 @@ Require Import External_Types.
 Include External_Types.
 Module External_FunsExternal_Template.
 
-(** [core::mem::swap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
-    Name pattern: core::mem::swap *)
-Axiom core_mem_swap :
-  forall(T : Type), T -> T -> state -> result (state * (T * T))
+(** [core::cell::{core::cell::Cell<T>#10}::get]:
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26
+    Name pattern: core::cell::{core::cell::Cell<@T>}::get *)
+Axiom core_cell_Cell_get :
+  forall(T : Type) (markerCopyInst : core_marker_Copy_t T),
+        core_cell_Cell_t T -> state -> result (state * T)
 .
 
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
-    Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
-Axiom core_num_nonzero_NonZeroU32_new
-  : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
-.
-
-(** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
-    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
-Axiom core_option_Option_unwrap :
-  forall(T : Type), option T -> state -> result (state * T)
+(** [core::cell::{core::cell::Cell<T>#11}::get_mut]:
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 574:4-574:39
+    Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *)
+Axiom core_cell_Cell_get_mut :
+  forall(T : Type),
+        core_cell_Cell_t T -> state -> result (state * (T * (T -> state ->
+          result (state * (core_cell_Cell_t T)))))
 .
 
 End External_FunsExternal_Template.
diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v
index b42c2ecf..5b233c62 100644
--- a/tests/coq/misc/External_Types.v
+++ b/tests/coq/misc/External_Types.v
@@ -10,4 +10,14 @@ Require Import External_TypesExternal.
 Include External_TypesExternal.
 Module External_Types.
 
+(** Trait declaration: [core::marker::Copy]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 450:0-450:21
+    Name pattern: core::marker::Copy *)
+Record core_marker_Copy_t (Self : Type) := mkcore_marker_Copy_t {
+  core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst : core_clone_Clone Self;
+}.
+
+Arguments mkcore_marker_Copy_t { _ }.
+Arguments core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst { _ }.
+
 End External_Types.
diff --git a/tests/coq/misc/External_TypesExternal.v b/tests/coq/misc/External_TypesExternal.v
index 734c66e5..6bb2b1db 100644
--- a/tests/coq/misc/External_TypesExternal.v
+++ b/tests/coq/misc/External_TypesExternal.v
@@ -8,9 +8,8 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Module External_TypesExternal.
 
-(** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
-Axiom core_num_nonzero_NonZeroU32_t : Type.
+(** [core::cell::Cell] *)
+Axiom core_cell_Cell_t : forall (T : Type), Type.
 
 (** The state type used in the state-error monad *)
 Axiom state : Type.
diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v
index 7d6af202..87b1c826 100644
--- a/tests/coq/misc/External_TypesExternal_Template.v
+++ b/tests/coq/misc/External_TypesExternal_Template.v
@@ -9,10 +9,10 @@ Import ListNotations.
 Local Open Scope Primitives_scope.
 Module External_TypesExternal_Template.
 
-(** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
-    Name pattern: core::num::nonzero::NonZeroU32 *)
-Axiom core_num_nonzero_NonZeroU32_t : Type.
+(** [core::cell::Cell]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 293:0-293:26
+    Name pattern: core::cell::Cell *)
+Axiom core_cell_Cell_t : forall (T : Type), Type.
 
 (** The state type used in the state-error monad *)
 Axiom state : Type.
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index e84d65ce..5ffda12f 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -489,6 +489,81 @@ Definition core_i64_max   := i64_max %i64.
 Definition core_i128_max  := i64_max %i128.
 Axiom core_isize_max : isize. (** TODO *)
 
+(*** core *)
+
+(** Trait declaration: [core::clone::Clone] *)
+Record core_clone_Clone (self : Type) := {
+  clone : self -> result self
+}.
+
+Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b.
+
+Definition core_clone_CloneBool : core_clone_Clone bool := {|
+  clone := fun b => Ok (core_clone_impls_CloneBool_clone b)
+|}.
+
+Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x.
+Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x.
+Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x.
+Definition core_clone_impls_CloneU32_clone (x : u32) : u32 := x.
+Definition core_clone_impls_CloneU64_clone (x : u64) : u64 := x.
+Definition core_clone_impls_CloneU128_clone (x : u128) : u128 := x.
+
+Definition core_clone_impls_CloneIsize_clone (x : isize) : isize := x.
+Definition core_clone_impls_CloneI8_clone (x : i8) : i8 := x.
+Definition core_clone_impls_CloneI16_clone (x : i16) : i16 := x.
+Definition core_clone_impls_CloneI32_clone (x : i32) : i32 := x.
+Definition core_clone_impls_CloneI64_clone (x : i64) : i64 := x.
+Definition core_clone_impls_CloneI128_clone (x : i128) : i128 := x.
+
+Definition core_clone_CloneUsize : core_clone_Clone usize := {|
+  clone := fun x => Ok (core_clone_impls_CloneUsize_clone x)
+|}.
+
+Definition core_clone_CloneU8 : core_clone_Clone u8 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU8_clone x)
+|}.
+
+Definition core_clone_CloneU16 : core_clone_Clone u16 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU16_clone x)
+|}.
+
+Definition core_clone_CloneU32 : core_clone_Clone u32 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU32_clone x)
+|}.
+
+Definition core_clone_CloneU64 : core_clone_Clone u64 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU64_clone x)
+|}.
+
+Definition core_clone_CloneU128 : core_clone_Clone u128 := {|
+  clone := fun x => Ok (core_clone_impls_CloneU128_clone x)
+|}.
+
+Definition core_clone_CloneIsize : core_clone_Clone isize := {|
+  clone := fun x => Ok (core_clone_impls_CloneIsize_clone x)
+|}.
+
+Definition core_clone_CloneI8 : core_clone_Clone i8 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI8_clone x)
+|}.
+
+Definition core_clone_CloneI16 : core_clone_Clone i16 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI16_clone x)
+|}.
+
+Definition core_clone_CloneI32 : core_clone_Clone i32 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI32_clone x)
+|}.
+
+Definition core_clone_CloneI64 : core_clone_Clone i64 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI64_clone x)
+|}.
+
+Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
+  clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
+|}.
+
 (*** core::ops *)
 
 (* Trait declaration: [core::ops::index::Index] *)
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index d4247b8f..d8457ce3 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -7,48 +7,26 @@ include External.FunsExternal
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [external::swap]:
-    Source: 'src/external.rs', lines 6:0-6:46 *)
-let swap (t : Type0) (x : t) (y : t) (st : state) : result (state & (t & t)) =
-  core_mem_swap t x y st
-
-(** [external::test_new_non_zero_u32]:
-    Source: 'src/external.rs', lines 11:0-11:60 *)
-let test_new_non_zero_u32
-  (x : u32) (st : state) : result (state & core_num_nonzero_NonZeroU32_t) =
-  let* (st1, o) = core_num_nonzero_NonZeroU32_new x st in
-  core_option_Option_unwrap core_num_nonzero_NonZeroU32_t o st1
-
-(** [external::test_vec]:
-    Source: 'src/external.rs', lines 17:0-17:17 *)
-let test_vec : result unit =
-  let* _ = alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0 in Ok ()
-
-(** Unit test for [external::test_vec] *)
-let _ = assert_norm (test_vec = Ok ())
-
-(** [external::custom_swap]:
-    Source: 'src/external.rs', lines 24:0-24:66 *)
-let custom_swap
-  (t : Type0) (x : t) (y : t) (st : state) :
-  result (state & (t & (t -> state -> result (state & (t & t)))))
+(** Trait implementation: [core::marker::{(core::marker::Copy for u32)#40}]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 47:29-47:65
+    Name pattern: core::marker::Copy<u32> *)
+let core_marker_CopyU32 : core_marker_Copy_t u32 = {
+  cloneCloneInst = core_clone_CloneU32;
+}
+
+(** [external::use_get]:
+    Source: 'src/external.rs', lines 5:0-5:37 *)
+let use_get (rc : core_cell_Cell_t u32) (st : state) : result (state & u32) =
+  core_cell_Cell_get u32 core_marker_CopyU32 rc st
+
+(** [external::incr]:
+    Source: 'src/external.rs', lines 9:0-9:31 *)
+let incr
+  (rc : core_cell_Cell_t u32) (st : state) :
+  result (state & (core_cell_Cell_t u32))
   =
-  let* (st1, (x1, y1)) = core_mem_swap t x y st in
-  let back = fun ret st2 -> Ok (st2, (ret, y1)) in
-  Ok (st1, (x1, back))
-
-(** [external::test_custom_swap]:
-    Source: 'src/external.rs', lines 29:0-29:59 *)
-let test_custom_swap
-  (x : u32) (y : u32) (st : state) : result (state & (u32 & u32)) =
-  let* (st1, (_, custom_swap_back)) = custom_swap u32 x y st in
-  let* (_, (x1, y1)) = custom_swap_back 1 st1 in
-  Ok (st1, (x1, y1))
-
-(** [external::test_swap_non_zero]:
-    Source: 'src/external.rs', lines 35:0-35:44 *)
-let test_swap_non_zero (x : u32) (st : state) : result (state & u32) =
-  let* (st1, p) = swap u32 x 0 st in
-  let (x1, _) = p in
-  if x1 = 0 then Fail Failure else Ok (st1, x1)
+  let* (st1, (i, get_mut_back)) = core_cell_Cell_get_mut u32 rc st in
+  let* i1 = u32_add i 1 in
+  let* (_, rc1) = get_mut_back i1 st1 in
+  Ok (st1, rc1)
 
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index 4c1c58b7..9436cf86 100644
--- a/tests/fstar/misc/External.FunsExternal.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -6,20 +6,18 @@ include External.Types
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [core::mem::swap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
-    Name pattern: core::mem::swap *)
-val core_mem_swap (t : Type0) : t -> t -> state -> result (state & (t & t))
+(** [core::cell::{core::cell::Cell<T>#10}::get]:
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26
+    Name pattern: core::cell::{core::cell::Cell<@T>}::get *)
+val core_cell_Cell_get
+  (t : Type0) (markerCopyInst : core_marker_Copy_t t) :
+  core_cell_Cell_t t -> state -> result (state & t)
 
-(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
-    Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
-val core_num_nonzero_NonZeroU32_new
-  : u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
-
-(** [core::option::{core::option::Option<T>}::unwrap]:
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
-    Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
-val core_option_Option_unwrap
-  (t : Type0) : option t -> state -> result (state & t)
+(** [core::cell::{core::cell::Cell<T>#11}::get_mut]:
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 574:4-574:39
+    Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *)
+val core_cell_Cell_get_mut
+  (t : Type0) :
+  core_cell_Cell_t t -> state -> result (state & (t & (t -> state -> result
+    (state & (core_cell_Cell_t t)))))
 
diff --git a/tests/fstar/misc/External.Types.fst b/tests/fstar/misc/External.Types.fst
index 4fbcec47..143f24dd 100644
--- a/tests/fstar/misc/External.Types.fst
+++ b/tests/fstar/misc/External.Types.fst
@@ -6,3 +6,10 @@ include External.TypesExternal
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
+(** Trait declaration: [core::marker::Copy]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 450:0-450:21
+    Name pattern: core::marker::Copy *)
+noeq type core_marker_Copy_t (self : Type0) = {
+  cloneCloneInst : core_clone_Clone self;
+}
+
diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti
index 45174c7e..c0b7e43f 100644
--- a/tests/fstar/misc/External.TypesExternal.fsti
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -5,10 +5,10 @@ open Primitives
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [core::num::nonzero::NonZeroU32]
-    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
-    Name pattern: core::num::nonzero::NonZeroU32 *)
-val core_num_nonzero_NonZeroU32_t : Type0
+(** [core::cell::Cell]
+    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 293:0-293:26
+    Name pattern: core::cell::Cell *)
+val core_cell_Cell_t (t : Type0) : Type0
 
 (** The state type used in the state-error monad *)
 val state : Type0
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index acdb09dc..c7c9f9db 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -465,6 +465,81 @@ let i64_shr #ty = scalar_shr #I64 #ty
 let i128_shr #ty = scalar_shr #I128 #ty
 let isize_shr #ty = scalar_shr #Isize #ty
 
+(*** core *)
+
+/// Trait declaration: [core::clone::Clone]
+noeq type core_clone_Clone (self : Type0) = {
+  clone : self → result self
+}
+
+let core_clone_impls_CloneBool_clone (b : bool) : bool = b
+
+let core_clone_CloneBool : core_clone_Clone bool = {
+  clone = fun b -> Ok (core_clone_impls_CloneBool_clone b)
+}
+
+let core_clone_impls_CloneUsize_clone (x : usize) : usize = x
+let core_clone_impls_CloneU8_clone (x : u8) : u8 = x
+let core_clone_impls_CloneU16_clone (x : u16) : u16 = x
+let core_clone_impls_CloneU32_clone (x : u32) : u32 = x
+let core_clone_impls_CloneU64_clone (x : u64) : u64 = x
+let core_clone_impls_CloneU128_clone (x : u128) : u128 = x
+
+let core_clone_impls_CloneIsize_clone (x : isize) : isize = x
+let core_clone_impls_CloneI8_clone (x : i8) : i8 = x
+let core_clone_impls_CloneI16_clone (x : i16) : i16 = x
+let core_clone_impls_CloneI32_clone (x : i32) : i32 = x
+let core_clone_impls_CloneI64_clone (x : i64) : i64 = x
+let core_clone_impls_CloneI128_clone (x : i128) : i128 = x
+
+let core_clone_CloneUsize : core_clone_Clone usize = {
+  clone = fun x -> Ok (core_clone_impls_CloneUsize_clone x)
+}
+
+let core_clone_CloneU8 : core_clone_Clone u8 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU8_clone x)
+}
+
+let core_clone_CloneU16 : core_clone_Clone u16 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU16_clone x)
+}
+
+let core_clone_CloneU32 : core_clone_Clone u32 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU32_clone x)
+}
+
+let core_clone_CloneU64 : core_clone_Clone u64 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU64_clone x)
+}
+
+let core_clone_CloneU128 : core_clone_Clone u128 = {
+  clone = fun x -> Ok (core_clone_impls_CloneU128_clone x)
+}
+
+let core_clone_CloneIsize : core_clone_Clone isize = {
+  clone = fun x -> Ok (core_clone_impls_CloneIsize_clone x)
+}
+
+let core_clone_CloneI8 : core_clone_Clone i8 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI8_clone x)
+}
+
+let core_clone_CloneI16 : core_clone_Clone i16 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI16_clone x)
+}
+
+let core_clone_CloneI32 : core_clone_Clone i32 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI32_clone x)
+}
+
+let core_clone_CloneI64 : core_clone_Clone i64 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI64_clone x)
+}
+
+let core_clone_CloneI128 : core_clone_Clone i128 = {
+  clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
+}
+
 (*** core::ops *)
 
 // Trait declaration: [core::ops::index::Index]
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 78e0f95c..20c4b8e5 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -7,58 +7,28 @@ open Primitives
 
 namespace external
 
-/- [external::swap]:
-   Source: 'src/external.rs', lines 6:0-6:46 -/
-def swap
-  (T : Type) (x : T) (y : T) (st : State) : Result (State × (T × T)) :=
-  core.mem.swap T x y st
-
-/- [external::test_new_non_zero_u32]:
-   Source: 'src/external.rs', lines 11:0-11:60 -/
-def test_new_non_zero_u32
-  (x : U32) (st : State) : Result (State × core.num.nonzero.NonZeroU32) :=
-  do
-  let (st1, o) ← core.num.nonzero.NonZeroU32.new x st
-  core.option.Option.unwrap core.num.nonzero.NonZeroU32 o st1
-
-/- [external::test_vec]:
-   Source: 'src/external.rs', lines 17:0-17:17 -/
-def test_vec : Result Unit :=
-  do
-  let _ ← alloc.vec.Vec.push U32 (alloc.vec.Vec.new U32) 0#u32
-  Result.ok ()
-
-/- Unit test for [external::test_vec] -/
-#assert (test_vec == Result.ok ())
-
-/- [external::custom_swap]:
-   Source: 'src/external.rs', lines 24:0-24:66 -/
-def custom_swap
-  (T : Type) (x : T) (y : T) (st : State) :
-  Result (State × (T × (T → State → Result (State × (T × T)))))
+/- Trait implementation: [core::marker::{(core::marker::Copy for u32)#40}]
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 47:29-47:65
+   Name pattern: core::marker::Copy<u32> -/
+def core.marker.CopyU32 : core.marker.Copy U32 := {
+  cloneCloneInst := core.clone.CloneU32
+}
+
+/- [external::use_get]:
+   Source: 'src/external.rs', lines 5:0-5:37 -/
+def use_get (rc : core.cell.Cell U32) (st : State) : Result (State × U32) :=
+  core.cell.Cell.get U32 core.marker.CopyU32 rc st
+
+/- [external::incr]:
+   Source: 'src/external.rs', lines 9:0-9:31 -/
+def incr
+  (rc : core.cell.Cell U32) (st : State) :
+  Result (State × (core.cell.Cell U32))
   :=
   do
-  let (st1, (x1, y1)) ← core.mem.swap T x y st
-  let back := fun ret st2 => Result.ok (st2, (ret, y1))
-  Result.ok (st1, (x1, back))
-
-/- [external::test_custom_swap]:
-   Source: 'src/external.rs', lines 29:0-29:59 -/
-def test_custom_swap
-  (x : U32) (y : U32) (st : State) : Result (State × (U32 × U32)) :=
-  do
-  let (st1, (_, custom_swap_back)) ← custom_swap U32 x y st
-  let (_, (x1, y1)) ← custom_swap_back 1#u32 st1
-  Result.ok (st1, (x1, y1))
-
-/- [external::test_swap_non_zero]:
-   Source: 'src/external.rs', lines 35:0-35:44 -/
-def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) :=
-  do
-  let (st1, p) ← swap U32 x 0#u32 st
-  let (x1, _) := p
-  if x1 = 0#u32
-  then Result.fail .panic
-  else Result.ok (st1, x1)
+  let (st1, (i, get_mut_back)) ← core.cell.Cell.get_mut U32 rc st
+  let i1 ← i + 1#u32
+  let (_, rc1) ← get_mut_back i1 st1
+  Result.ok (st1, rc1)
 
 end external
diff --git a/tests/lean/External/FunsExternal.lean b/tests/lean/External/FunsExternal.lean
index b6efc65f..28ba2077 100644
--- a/tests/lean/External/FunsExternal.lean
+++ b/tests/lean/External/FunsExternal.lean
@@ -4,19 +4,14 @@ import External.Types
 open Primitives
 open external
 
--- TODO: fill those bodies
+/- [core::cell::{core::cell::Cell<T>#10}::get]: -/
+def core.cell.Cell.get
+  (T : Type) (markerCopyInst : core.marker.Copy T) (c : core.cell.Cell T) (s : State) :
+  Result (State × T) :=
+  sorry
 
-/- [core::mem::swap] -/
-def core.mem.swap
-  (T : Type) : T → T → State → Result (State × (T × T)) :=
-  fun x y s => .ok (s, (y, x))
+/- [core::cell::{core::cell::Cell<T>#11}::get_mut]: -/
+def core.cell.Cell.get_mut (T : Type) (c : core.cell.Cell T) (s : State) :
+  Result (State × (T × (T → State → Result (State × (core.cell.Cell T))))) :=
+  sorry
 
-/- [core::num::nonzero::NonZeroU32::{14}::new] -/
-def core.num.nonzero.NonZeroU32.new :
-  U32 → State → Result (State × (Option core_num_nonzero_non_zero_u32_t)) :=
-  fun _ _ => .fail .panic
-
-/- [core::option::Option::{0}::unwrap] -/
-def core.option.Option.unwrap
-  (T : Type) : Option T → State → Result (State × T) :=
-  fun _ _ => .fail .panic
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index f0e771f7..a6163c96 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -6,15 +6,18 @@ import External.Types
 open Primitives
 open external
 
-/- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
-   Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new -/
-axiom core.num.nonzero.NonZeroU32.new
-  : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32))
+/- [core::cell::{core::cell::Cell<T>#10}::get]:
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26
+   Name pattern: core::cell::{core::cell::Cell<@T>}::get -/
+axiom core.cell.Cell.get
+  (T : Type) (markerCopyInst : core.marker.Copy T) :
+  core.cell.Cell T → State → Result (State × T)
 
-/- [core::option::{core::option::Option<T>}::unwrap]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
-   Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
-axiom core.option.Option.unwrap
-  (T : Type) : Option T → State → Result (State × T)
+/- [core::cell::{core::cell::Cell<T>#11}::get_mut]:
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 574:4-574:39
+   Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut -/
+axiom core.cell.Cell.get_mut
+  (T : Type) :
+  core.cell.Cell T → State → Result (State × (T × (T → State → Result
+    (State × (core.cell.Cell T)))))
 
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index 961f3e8a..5d4cfc77 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -6,4 +6,10 @@ open Primitives
 
 namespace external
 
+/- Trait declaration: [core::marker::Copy]
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 450:0-450:21
+   Name pattern: core::marker::Copy -/
+structure core.marker.Copy (Self : Type) where
+  cloneCloneInst : core.clone.Clone Self
+
 end external
diff --git a/tests/lean/External/TypesExternal.lean b/tests/lean/External/TypesExternal.lean
index 7c30f792..d0f5a0cc 100644
--- a/tests/lean/External/TypesExternal.lean
+++ b/tests/lean/External/TypesExternal.lean
@@ -1,11 +1,20 @@
 -- [external]: external types.
 import Base
-open Primitives
+open Lean Primitives
 
 /- [core::num::nonzero::NonZeroU32]
    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
-axiom core.num.nonzero.NonZeroU32 : Type
+structure core.cell.Cell (T : Type) :=
+  id : Nat
 
-/- The state type used in the state-error monad -/
-axiom State : Type
+def CellValue := (T:Type) × T
+
+/- The state type used in the state-error monad
 
+   TODO: we tried the following definition, but it makes State a Type 1, leading
+   to type errors later:
+
+     structure State :=
+       cells : AssocList Nat CellValue
+  -/
+axiom State : Type
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
index 84245531..2e6ed6e0 100644
--- a/tests/lean/External/TypesExternal_Template.lean
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -4,10 +4,10 @@
 import Base
 open Primitives
 
-/- [core::num::nonzero::NonZeroU32]
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
-   Name pattern: core::num::nonzero::NonZeroU32 -/
-axiom core.num.nonzero.NonZeroU32 : Type
+/- [core::cell::Cell]
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 293:0-293:26
+   Name pattern: core::cell::Cell -/
+axiom core.cell.Cell (T : Type) : Type
 
 /- The state type used in the state-error monad -/
 axiom State : Type