From 703261b6c8ad680a925ae0550117a85d9dfa40fe Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 25 Apr 2024 13:42:23 +0200 Subject: Update the tests for External --- tests/fstar/misc/External.Funs.fst | 64 ++++++++---------------- tests/fstar/misc/External.FunsExternal.fsti | 28 +++++------ tests/fstar/misc/External.Types.fst | 7 +++ tests/fstar/misc/External.TypesExternal.fsti | 8 +-- tests/fstar/misc/Primitives.fst | 75 ++++++++++++++++++++++++++++ 5 files changed, 120 insertions(+), 62 deletions(-) (limited to 'tests/fstar/misc') 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 *) +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#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}::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#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] -- cgit v1.2.3