From 60db3c210aeaf66a4fe312544c6e5d4662681de7 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 4 Aug 2023 22:33:05 +0200 Subject: Generate the array test files for Coq and F* --- tests/coq/array/Array_Funs.v | 300 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 300 insertions(+) create mode 100644 tests/coq/array/Array_Funs.v (limited to 'tests/coq/array/Array_Funs.v') diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array_Funs.v new file mode 100644 index 00000000..4a862d1b --- /dev/null +++ b/tests/coq/array/Array_Funs.v @@ -0,0 +1,300 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [array]: function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Export Array_Types. +Import Array_Types. +Module Array_Funs. + +(** [array::array_to_shared_slice_]: forward function *) +Definition array_to_shared_slice__fwd + (T : Type) (s : array T 32%usize) : result (slice T) := + array_to_slice_shared T 32%usize s +. + +(** [array::array_to_mut_slice_]: forward function *) +Definition array_to_mut_slice__fwd + (T : Type) (s : array T 32%usize) : result (slice T) := + array_to_slice_mut_fwd T 32%usize s +. + +(** [array::array_to_mut_slice_]: backward function 0 *) +Definition array_to_mut_slice__back + (T : Type) (s : array T 32%usize) (ret : slice T) : + result (array T 32%usize) + := + array_to_slice_mut_back T 32%usize s ret +. + +(** [array::array_len]: forward function *) +Definition array_len_fwd (T : Type) (s : array T 32%usize) : result usize := + s0 <- array_to_slice_shared T 32%usize s; let i := slice_len T s0 in Return i +. + +(** [array::shared_array_len]: forward function *) +Definition shared_array_len_fwd + (T : Type) (s : array T 32%usize) : result usize := + s0 <- array_to_slice_shared T 32%usize s; let i := slice_len T s0 in Return i +. + +(** [array::shared_slice_len]: forward function *) +Definition shared_slice_len_fwd (T : Type) (s : slice T) : result usize := + let i := slice_len T s in Return i +. + +(** [array::index_array_shared]: forward function *) +Definition index_array_shared_fwd + (T : Type) (s : array T 32%usize) (i : usize) : result T := + array_index_shared T 32%usize s i +. + +(** [array::index_array_u32]: forward function *) +Definition index_array_u32_fwd + (s : array u32 32%usize) (i : usize) : result u32 := + array_index_shared u32 32%usize s i +. + +(** [array::index_array_generic]: forward function *) +Definition index_array_generic_fwd + (N : usize) (s : array u32 N) (i : usize) : result u32 := + array_index_shared u32 N s i +. + +(** [array::index_array_generic_call]: forward function *) +Definition index_array_generic_call_fwd + (N : usize) (s : array u32 N) (i : usize) : result u32 := + index_array_generic_fwd N s i +. + +(** [array::index_array_copy]: forward function *) +Definition index_array_copy_fwd (x : array u32 32%usize) : result u32 := + array_index_shared u32 32%usize x 0%usize +. + +(** [array::index_mut_array]: forward function *) +Definition index_mut_array_fwd + (T : Type) (s : array T 32%usize) (i : usize) : result T := + array_index_mut_fwd T 32%usize s i +. + +(** [array::index_mut_array]: backward function 0 *) +Definition index_mut_array_back + (T : Type) (s : array T 32%usize) (i : usize) (ret : T) : + result (array T 32%usize) + := + array_index_mut_back T 32%usize s i ret +. + +(** [array::index_slice]: forward function *) +Definition index_slice_fwd (T : Type) (s : slice T) (i : usize) : result T := + slice_index_shared T s i +. + +(** [array::index_mut_slice]: forward function *) +Definition index_mut_slice_fwd + (T : Type) (s : slice T) (i : usize) : result T := + slice_index_mut_fwd T s i +. + +(** [array::index_mut_slice]: backward function 0 *) +Definition index_mut_slice_back + (T : Type) (s : slice T) (i : usize) (ret : T) : result (slice T) := + slice_index_mut_back T s i ret +. + +(** [array::slice_subslice_shared_]: forward function *) +Definition slice_subslice_shared__fwd + (x : slice u32) (y : usize) (z : usize) : result (slice u32) := + slice_subslice_shared u32 x (mk_range y z) +. + +(** [array::slice_subslice_mut_]: forward function *) +Definition slice_subslice_mut__fwd + (x : slice u32) (y : usize) (z : usize) : result (slice u32) := + slice_subslice_mut_fwd u32 x (mk_range y z) +. + +(** [array::slice_subslice_mut_]: backward function 0 *) +Definition slice_subslice_mut__back + (x : slice u32) (y : usize) (z : usize) (ret : slice u32) : + result (slice u32) + := + slice_subslice_mut_back u32 x (mk_range y z) ret +. + +(** [array::array_to_slice_shared_]: forward function *) +Definition array_to_slice_shared__fwd + (x : array u32 32%usize) : result (slice u32) := + array_to_slice_shared u32 32%usize x +. + +(** [array::array_to_slice_mut_]: forward function *) +Definition array_to_slice_mut__fwd + (x : array u32 32%usize) : result (slice u32) := + array_to_slice_mut_fwd u32 32%usize x +. + +(** [array::array_to_slice_mut_]: backward function 0 *) +Definition array_to_slice_mut__back + (x : array u32 32%usize) (ret : slice u32) : result (array u32 32%usize) := + array_to_slice_mut_back u32 32%usize x ret +. + +(** [array::array_subslice_shared_]: forward function *) +Definition array_subslice_shared__fwd + (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) := + array_subslice_shared u32 32%usize x (mk_range y z) +. + +(** [array::array_subslice_mut_]: forward function *) +Definition array_subslice_mut__fwd + (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) := + array_subslice_mut_fwd u32 32%usize x (mk_range y z) +. + +(** [array::array_subslice_mut_]: backward function 0 *) +Definition array_subslice_mut__back + (x : array u32 32%usize) (y : usize) (z : usize) (ret : slice u32) : + result (array u32 32%usize) + := + array_subslice_mut_back u32 32%usize x (mk_range y z) ret +. + +(** [array::index_slice_0]: forward function *) +Definition index_slice_0_fwd (T : Type) (s : slice T) : result T := + slice_index_shared T s 0%usize +. + +(** [array::index_array_0]: forward function *) +Definition index_array_0_fwd (T : Type) (s : array T 32%usize) : result T := + array_index_shared T 32%usize s 0%usize +. + +(** [array::index_index_array]: forward function *) +Definition index_index_array_fwd + (s : array (array u32 32%usize) 32%usize) (i : usize) (j : usize) : + result u32 + := + a <- array_index_shared (array u32 32%usize) 32%usize s i; + array_index_shared u32 32%usize a j +. + +(** [array::update_update_array]: forward function *) +Definition update_update_array_fwd + (s : array (array u32 32%usize) 32%usize) (i : usize) (j : usize) : + result unit + := + a <- array_index_mut_fwd (array u32 32%usize) 32%usize s i; + a0 <- array_index_mut_back u32 32%usize a j 0%u32; + _ <- array_index_mut_back (array u32 32%usize) 32%usize s i a0; + Return tt +. + +(** [array::array_local_deep_copy]: forward function *) +Definition array_local_deep_copy_fwd (x : array u32 32%usize) : result unit := + Return tt +. + +(** [array::f0]: forward function *) +Definition f0_fwd : result unit := + s <- + array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]); + s0 <- slice_index_mut_back u32 s 0%usize 1%u32; + _ <- + array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]) + s0; + Return tt +. + +(** [array::f1]: forward function *) +Definition f1_fwd : result unit := + _ <- + array_index_mut_back u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]) + 0%usize 1%u32; + Return tt +. + +(** [array::sum]: loop 0: forward function *) +Fixpoint sum_loop_fwd + (n : nat) (s : slice u32) (sum : u32) (i : usize) : result u32 := + match n with + | O => Fail_ OutOfFuel + | S n0 => + let i0 := slice_len u32 s in + if i s< i0 + then ( + i1 <- slice_index_shared u32 s i; + sum0 <- u32_add sum i1; + i2 <- usize_add i 1%usize; + sum_loop_fwd n0 s sum0 i2) + else Return sum + end +. + +(** [array::sum]: forward function *) +Definition sum_fwd (n : nat) (s : slice u32) : result u32 := + sum_loop_fwd n s 0%u32 0%usize +. + +(** [array::sum2]: loop 0: forward function *) +Fixpoint sum2_loop_fwd + (n : nat) (s : slice u32) (s2 : slice u32) (sum : u32) (i : usize) : + result u32 + := + match n with + | O => Fail_ OutOfFuel + | S n0 => + let i0 := slice_len u32 s in + if i s< i0 + then ( + i1 <- slice_index_shared u32 s i; + i2 <- slice_index_shared u32 s2 i; + i3 <- u32_add i1 i2; + sum0 <- u32_add sum i3; + i4 <- usize_add i 1%usize; + sum2_loop_fwd n0 s s2 sum0 i4) + else Return sum + end +. + +(** [array::sum2]: forward function *) +Definition sum2_fwd (n : nat) (s : slice u32) (s2 : slice u32) : result u32 := + let i := slice_len u32 s in + let i0 := slice_len u32 s2 in + if negb (i s= i0) then Fail_ Failure else sum2_loop_fwd n s s2 0%u32 0%usize +. + +(** [array::f2]: forward function *) +Definition f2_fwd (i : u32) : result unit := + Return tt. + +(** [array::f4]: forward function *) +Definition f4_fwd + (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) := + array_subslice_shared u32 32%usize x (mk_range y z) +. + +(** [array::f3]: forward function *) +Definition f3_fwd (n : nat) : result u32 := + i <- + array_index_shared u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]) + 0%usize; + _ <- f2_fwd i; + s <- + array_to_slice_shared u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]); + s0 <- + f4_fwd + (mk_array u32 32%usize [ + 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; + 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; + 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; 0%u32; + 0%u32; 0%u32 + ]) 16%usize 18%usize; + sum2_fwd n s s0 +. + +End Array_Funs . -- cgit v1.2.3 From d25287dcc5435d3784de284dafe3746e13467f49 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 7 Aug 2023 08:59:59 +0200 Subject: Regenerate the test files --- tests/coq/array/Array_Funs.v | 187 ++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 177 insertions(+), 10 deletions(-) (limited to 'tests/coq/array/Array_Funs.v') diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array_Funs.v index 4a862d1b..6d791873 100644 --- a/tests/coq/array/Array_Funs.v +++ b/tests/coq/array/Array_Funs.v @@ -199,25 +199,156 @@ Definition array_local_deep_copy_fwd (x : array u32 32%usize) : result unit := Return tt . -(** [array::f0]: forward function *) -Definition f0_fwd : result unit := +(** [array::take_array]: forward function *) +Definition take_array_fwd (a : array u32 2%usize) : result unit := + Return tt. + +(** [array::take_array_borrow]: forward function *) +Definition take_array_borrow_fwd (a : array u32 2%usize) : result unit := + Return tt +. + +(** [array::take_slice]: forward function *) +Definition take_slice_fwd (s : slice u32) : result unit := + Return tt. + +(** [array::take_mut_slice]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +Definition take_mut_slice_fwd_back (s : slice u32) : result (slice u32) := + Return s +. + +(** [array::take_all]: forward function *) +Definition take_all_fwd : result unit := + _ <- take_array_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + _ <- take_array_borrow_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); s <- - array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]); - s0 <- slice_index_mut_back u32 s 0%usize 1%u32; + array_to_slice_shared u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + _ <- take_slice_fwd s; + s0 <- + array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + s1 <- take_mut_slice_fwd_back s0; _ <- - array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]) - s0; + array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]) + s1; Return tt . -(** [array::f1]: forward function *) -Definition f1_fwd : result unit := +(** [array::index_array]: forward function *) +Definition index_array_fwd (x : array u32 2%usize) : result u32 := + array_index_shared u32 2%usize x 0%usize +. + +(** [array::index_array_borrow]: forward function *) +Definition index_array_borrow_fwd (x : array u32 2%usize) : result u32 := + array_index_shared u32 2%usize x 0%usize +. + +(** [array::index_slice_u32_0]: forward function *) +Definition index_slice_u32_0_fwd (x : slice u32) : result u32 := + slice_index_shared u32 x 0%usize +. + +(** [array::index_mut_slice_u32_0]: forward function *) +Definition index_mut_slice_u32_0_fwd (x : slice u32) : result u32 := + slice_index_shared u32 x 0%usize +. + +(** [array::index_mut_slice_u32_0]: backward function 0 *) +Definition index_mut_slice_u32_0_back (x : slice u32) : result (slice u32) := + _ <- slice_index_shared u32 x 0%usize; Return x +. + +(** [array::index_all]: forward function *) +Definition index_all_fwd : result u32 := + i <- index_array_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + i0 <- index_array_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + i1 <- u32_add i i0; + i2 <- index_array_borrow_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + i3 <- u32_add i1 i2; + s <- + array_to_slice_shared u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + i4 <- index_slice_u32_0_fwd s; + i5 <- u32_add i3 i4; + s0 <- + array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + i6 <- index_mut_slice_u32_0_fwd s0; + i7 <- u32_add i5 i6; + s1 <- index_mut_slice_u32_0_back s0; _ <- - array_index_mut_back u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]) - 0%usize 1%u32; + array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]) + s1; + Return i7 +. + +(** [array::update_array]: forward function *) +Definition update_array_fwd (x : array u32 2%usize) : result unit := + _ <- array_index_mut_back u32 2%usize x 0%usize 1%u32; Return tt +. + +(** [array::update_array_mut_borrow]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +Definition update_array_mut_borrow_fwd_back + (x : array u32 2%usize) : result (array u32 2%usize) := + array_index_mut_back u32 2%usize x 0%usize 1%u32 +. + +(** [array::update_mut_slice]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +Definition update_mut_slice_fwd_back (x : slice u32) : result (slice u32) := + slice_index_mut_back u32 x 0%usize 1%u32 +. + +(** [array::update_all]: forward function *) +Definition update_all_fwd : result unit := + _ <- update_array_fwd (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + x <- + update_array_mut_borrow_fwd_back (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + s <- array_to_slice_mut_fwd u32 2%usize x; + s0 <- update_mut_slice_fwd_back s; + _ <- array_to_slice_mut_back u32 2%usize x s0; Return tt . +(** [array::range_all]: forward function *) +Definition range_all_fwd : result unit := + s <- + array_subslice_mut_fwd u32 4%usize + (mk_array u32 4%usize [ 0%u32; 0%u32; 0%u32; 0%u32 ]) (mk_range 1%usize + 3%usize); + s0 <- update_mut_slice_fwd_back s; + _ <- + array_subslice_mut_back u32 4%usize + (mk_array u32 4%usize [ 0%u32; 0%u32; 0%u32; 0%u32 ]) (mk_range 1%usize + 3%usize) s0; + Return tt +. + +(** [array::deref_array_borrow]: forward function *) +Definition deref_array_borrow_fwd (x : array u32 2%usize) : result u32 := + array_index_shared u32 2%usize x 0%usize +. + +(** [array::deref_array_mut_borrow]: forward function *) +Definition deref_array_mut_borrow_fwd (x : array u32 2%usize) : result u32 := + array_index_shared u32 2%usize x 0%usize +. + +(** [array::deref_array_mut_borrow]: backward function 0 *) +Definition deref_array_mut_borrow_back + (x : array u32 2%usize) : result (array u32 2%usize) := + _ <- array_index_shared u32 2%usize x 0%usize; Return x +. + +(** [array::take_array_t]: forward function *) +Definition take_array_t_fwd (a : array T_t 2%usize) : result unit := + Return tt. + +(** [array::non_copyable_array]: forward function *) +Definition non_copyable_array_fwd : result unit := + _ <- take_array_t_fwd (mk_array T_t 2%usize [ TA; TB ]); Return tt +. + (** [array::sum]: loop 0: forward function *) Fixpoint sum_loop_fwd (n : nat) (s : slice u32) (sum : u32) (i : usize) : result u32 := @@ -268,6 +399,25 @@ Definition sum2_fwd (n : nat) (s : slice u32) (s2 : slice u32) : result u32 := if negb (i s= i0) then Fail_ Failure else sum2_loop_fwd n s s2 0%u32 0%usize . +(** [array::f0]: forward function *) +Definition f0_fwd : result unit := + s <- + array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]); + s0 <- slice_index_mut_back u32 s 0%usize 1%u32; + _ <- + array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]) + s0; + Return tt +. + +(** [array::f1]: forward function *) +Definition f1_fwd : result unit := + _ <- + array_index_mut_back u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]) + 0%usize 1%u32; + Return tt +. + (** [array::f2]: forward function *) Definition f2_fwd (i : u32) : result unit := Return tt. @@ -297,4 +447,21 @@ Definition f3_fwd (n : nat) : result u32 := sum2_fwd n s s0 . +(** [array::ite]: forward function *) +Definition ite_fwd : result unit := + s <- + array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + s0 <- + array_to_slice_mut_fwd u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]); + s1 <- index_mut_slice_u32_0_back s0; + _ <- + array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]) + s1; + s2 <- index_mut_slice_u32_0_back s; + _ <- + array_to_slice_mut_back u32 2%usize (mk_array u32 2%usize [ 0%u32; 0%u32 ]) + s2; + Return tt +. + End Array_Funs . -- cgit v1.2.3