Update the tests for External

5 files changed, 120 insertions, 62 deletions

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]