Merge pull request #32 from AeneasVerif/son_arrays

Add support for arrays/slices and const generics

1 files changed, 467 insertions, 0 deletions

diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array_Funs.v
new file mode 100644
index 00000000..6d791873
--- /dev/null
+++ b/tests/coq/array/Array_Funs.v
@@ -0,0 +1,467 @@
+(** 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::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_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 [ 0%u32; 0%u32 ])
+      s1;
+  Return tt
+.
+
+(** [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_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 :=
+  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::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.
+
+(** [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
+.
+
+(** [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 .