From a0c58326c43a7a8026b3d4c158017bf126180e90 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 22 Dec 2023 23:23:30 +0100 Subject: Regenerate the test files and add the fstar-split tests --- tests/fstar/misc/External.Funs.fst | 76 ++++++++++++-------------------------- 1 file changed, 24 insertions(+), 52 deletions(-) (limited to 'tests/fstar/misc/External.Funs.fst') diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index 00995634..bb1b9a64 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -7,33 +7,19 @@ include External.FunsExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [external::swap]: forward function +(** [external::swap]: Source: 'src/external.rs', lines 6:0-6:46 *) -let swap (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) = - let* (st0, _) = core_mem_swap t x y st in - let* (st1, _) = core_mem_swap_back0 t x y st st0 in - let* (st2, _) = core_mem_swap_back1 t x y st st1 in - Return (st2, ()) +let swap (t : Type0) (x : t) (y : t) (st : state) : result (state & (t & t)) = + core_mem_swap t x y st -(** [external::swap]: backward function 0 - Source: 'src/external.rs', lines 6:0-6:46 *) -let swap_back - (t : Type0) (x : t) (y : t) (st : state) (st0 : state) : - result (state & (t & t)) - = - let* (st1, _) = core_mem_swap t x y st in - let* (st2, x0) = core_mem_swap_back0 t x y st st1 in - let* (_, y0) = core_mem_swap_back1 t x y st st2 in - Return (st0, (x0, y0)) - -(** [external::test_new_non_zero_u32]: forward function +(** [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* (st0, o) = core_num_nonzero_NonZeroU32_new x st in - core_option_Option_unwrap core_num_nonzero_NonZeroU32_t o st0 + 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]: forward function +(** [external::test_vec]: Source: 'src/external.rs', lines 17:0-17:17 *) let test_vec : result unit = let v = alloc_vec_Vec_new u32 in @@ -43,42 +29,28 @@ let test_vec : result unit = (** Unit test for [external::test_vec] *) let _ = assert_norm (test_vec = Return ()) -(** [external::custom_swap]: forward function - Source: 'src/external.rs', lines 24:0-24:66 *) -let custom_swap (t : Type0) (x : t) (y : t) (st : state) : result (state & t) = - let* (st0, _) = core_mem_swap t x y st in - let* (st1, x0) = core_mem_swap_back0 t x y st st0 in - let* (st2, _) = core_mem_swap_back1 t x y st st1 in - Return (st2, x0) - -(** [external::custom_swap]: backward function 0 +(** [external::custom_swap]: Source: 'src/external.rs', lines 24:0-24:66 *) -let custom_swap_back - (t : Type0) (x : t) (y : t) (st : state) (ret : t) (st0 : state) : - result (state & (t & t)) +let custom_swap + (t : Type0) (x : t) (y : t) (st : state) : + result (state & (t & (t -> state -> result (state & (t & t))))) = - let* (st1, _) = core_mem_swap t x y st in - let* (st2, _) = core_mem_swap_back0 t x y st st1 in - let* (_, y0) = core_mem_swap_back1 t x y st st2 in - Return (st0, (ret, y0)) - -(** [external::test_custom_swap]: forward function - Source: 'src/external.rs', lines 29:0-29:59 *) -let test_custom_swap (x : u32) (y : u32) (st : state) : result (state & unit) = - let* (st0, _) = custom_swap u32 x y st in Return (st0, ()) + let* (st1, (x1, x2)) = core_mem_swap t x y st in + let back_'a = fun ret st2 -> Return (st2, (ret, x2)) in + Return (st1, (x1, back_'a)) -(** [external::test_custom_swap]: backward function 0 +(** [external::test_custom_swap]: Source: 'src/external.rs', lines 29:0-29:59 *) -let test_custom_swap_back - (x : u32) (y : u32) (st : state) (st0 : state) : - result (state & (u32 & u32)) - = - custom_swap_back u32 x y st 1 st0 +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 + Return (st1, (x1, y1)) -(** [external::test_swap_non_zero]: forward function +(** [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* (st0, _) = swap u32 x 0 st in - let* (st1, (x0, _)) = swap_back u32 x 0 st st0 in - if x0 = 0 then Fail Failure else Return (st1, x0) + let* (st1, p) = swap u32 x 0 st in + let (x1, _) = p in + if x1 = 0 then Fail Failure else Return (st1, x1) -- cgit v1.2.3 From a4decc7654bc6f3301c0174124d21fdbc2dbc708 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sat, 23 Dec 2023 00:59:55 +0100 Subject: Regenerate the files --- tests/fstar/misc/External.Funs.fst | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'tests/fstar/misc/External.Funs.fst') diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index bb1b9a64..6672b523 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -22,9 +22,7 @@ let test_new_non_zero_u32 (** [external::test_vec]: Source: 'src/external.rs', lines 17:0-17:17 *) let test_vec : result unit = - let v = alloc_vec_Vec_new u32 in - let* _ = alloc_vec_Vec_push u32 v 0 in - Return () + let* _ = alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0 in Return () (** Unit test for [external::test_vec] *) let _ = assert_norm (test_vec = Return ()) -- cgit v1.2.3