diff options
Diffstat (limited to 'tests/fstar/misc')
| -rw-r--r-- | tests/fstar/misc/Constants.fst | 137 | ||||
| -rw-r--r-- | tests/fstar/misc/External.Funs.fst | 130 | ||||
| -rw-r--r-- | tests/fstar/misc/External.Opaque.fsti | 27 | ||||
| -rw-r--r-- | tests/fstar/misc/External.Types.fsti | 13 | ||||
| -rw-r--r-- | tests/fstar/misc/Makefile | 47 | ||||
| -rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 562 | ||||
| -rw-r--r-- | tests/fstar/misc/Paper.fst | 147 | ||||
| -rw-r--r-- | tests/fstar/misc/PoloniusList.fst | 41 | ||||
| -rw-r--r-- | tests/fstar/misc/Primitives.fst | 287 |
9 files changed, 1391 insertions, 0 deletions
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst new file mode 100644 index 00000000..884d1778 --- /dev/null +++ b/tests/fstar/misc/Constants.fst @@ -0,0 +1,137 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [constants] *) +module Constants +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [constants::X0] *) +let x0_body : result u32 = Return 0 +let x0_c : u32 = eval_global x0_body + +(** [core::num::u32::{9}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + +(** [constants::X1] *) +let x1_body : result u32 = Return core_num_u32_max_c +let x1_c : u32 = eval_global x1_body + +(** [constants::X2] *) +let x2_body : result u32 = Return 3 +let x2_c : u32 = eval_global x2_body + +(** [constants::incr] *) +let incr_fwd (n : u32) : result u32 = + begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end + +(** [constants::X3] *) +let x3_body : result u32 = + begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end +let x3_c : u32 = eval_global x3_body + +(** [constants::mk_pair0] *) +let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y) + +(** [constants::Pair] *) +type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; } + +(** [constants::mk_pair1] *) +let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) = + Return (Mkpair_t x y) + +(** [constants::P0] *) +let p0_body : result (u32 & u32) = + begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end +let p0_c : (u32 & u32) = eval_global p0_body + +(** [constants::P1] *) +let p1_body : result (pair_t u32 u32) = + begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end +let p1_c : pair_t u32 u32 = eval_global p1_body + +(** [constants::P2] *) +let p2_body : result (u32 & u32) = Return (0, 1) +let p2_c : (u32 & u32) = eval_global p2_body + +(** [constants::P3] *) +let p3_body : result (pair_t u32 u32) = Return (Mkpair_t 0 1) +let p3_c : pair_t u32 u32 = eval_global p3_body + +(** [constants::Wrap] *) +type wrap_t (t : Type0) = { wrap_val : t; } + +(** [constants::Wrap::{0}::new] *) +let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) = + Return (Mkwrap_t val0) + +(** [constants::Y] *) +let y_body : result (wrap_t i32) = + begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end +let y_c : wrap_t i32 = eval_global y_body + +(** [constants::unwrap_y] *) +let unwrap_y_fwd : result i32 = Return y_c.wrap_val + +(** [constants::YVAL] *) +let yval_body : result i32 = + begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end +let yval_c : i32 = eval_global yval_body + +(** [constants::get_z1::Z1] *) +let get_z1_z1_body : result i32 = Return 3 +let get_z1_z1_c : i32 = eval_global get_z1_z1_body + +(** [constants::get_z1] *) +let get_z1_fwd : result i32 = Return get_z1_z1_c + +(** [constants::add] *) +let add_fwd (a : i32) (b : i32) : result i32 = + begin match i32_add a b with | Fail -> Fail | Return i -> Return i end + +(** [constants::Q1] *) +let q1_body : result i32 = Return 5 +let q1_c : i32 = eval_global q1_body + +(** [constants::Q2] *) +let q2_body : result i32 = Return q1_c +let q2_c : i32 = eval_global q2_body + +(** [constants::Q3] *) +let q3_body : result i32 = + begin match add_fwd q2_c 3 with | Fail -> Fail | Return i -> Return i end +let q3_c : i32 = eval_global q3_body + +(** [constants::get_z2] *) +let get_z2_fwd : result i32 = + begin match get_z1_fwd with + | Fail -> Fail + | Return i -> + begin match add_fwd i q3_c with + | Fail -> Fail + | Return i0 -> + begin match add_fwd q1_c i0 with + | Fail -> Fail + | Return i1 -> Return i1 + end + end + end + +(** [constants::S1] *) +let s1_body : result u32 = Return 6 +let s1_c : u32 = eval_global s1_body + +(** [constants::S2] *) +let s2_body : result u32 = + begin match incr_fwd s1_c with | Fail -> Fail | Return i -> Return i end +let s2_c : u32 = eval_global s2_body + +(** [constants::S3] *) +let s3_body : result (pair_t u32 u32) = Return p3_c +let s3_c : pair_t u32 u32 = eval_global s3_body + +(** [constants::S4] *) +let s4_body : result (pair_t u32 u32) = + begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end +let s4_c : pair_t u32 u32 = eval_global s4_body + diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst new file mode 100644 index 00000000..68a0061e --- /dev/null +++ b/tests/fstar/misc/External.Funs.fst @@ -0,0 +1,130 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: function definitions *) +module External.Funs +open Primitives +include External.Types +include External.Opaque + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [external::swap] *) +let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) = + begin match core_mem_swap_fwd t x y st with + | Fail -> Fail + | Return (st0, _) -> + begin match core_mem_swap_back0 t x y st st0 with + | Fail -> Fail + | Return (st1, _) -> + begin match core_mem_swap_back1 t x y st st1 with + | Fail -> Fail + | Return (st2, _) -> Return (st2, ()) + end + end + end + +(** [external::swap] *) +let swap_back + (t : Type0) (x : t) (y : t) (st : state) (st0 : state) : + result (state & (t & t)) + = + begin match core_mem_swap_fwd t x y st with + | Fail -> Fail + | Return (st1, _) -> + begin match core_mem_swap_back0 t x y st st1 with + | Fail -> Fail + | Return (st2, x0) -> + begin match core_mem_swap_back1 t x y st st2 with + | Fail -> Fail + | Return (_, y0) -> Return (st0, (x0, y0)) + end + end + end + +(** [external::test_new_non_zero_u32] *) +let test_new_non_zero_u32_fwd + (x : u32) (st : state) : result (state & core_num_nonzero_non_zero_u32_t) = + begin match core_num_nonzero_non_zero_u32_new_fwd x st with + | Fail -> Fail + | Return (st0, opt) -> + begin match + core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0 + with + | Fail -> Fail + | Return (st1, nzu) -> Return (st1, nzu) + end + end + +(** [external::test_vec] *) +let test_vec_fwd : result unit = + let v = vec_new u32 in + begin match vec_push_back u32 v 0 with + | Fail -> Fail + | Return _ -> Return () + end + +(** Unit test for [external::test_vec] *) +let _ = assert_norm (test_vec_fwd = Return ()) + +(** [external::custom_swap] *) +let custom_swap_fwd + (t : Type0) (x : t) (y : t) (st : state) : result (state & t) = + begin match core_mem_swap_fwd t x y st with + | Fail -> Fail + | Return (st0, _) -> + begin match core_mem_swap_back0 t x y st st0 with + | Fail -> Fail + | Return (st1, x0) -> + begin match core_mem_swap_back1 t x y st st1 with + | Fail -> Fail + | Return (st2, _) -> Return (st2, x0) + end + end + end + +(** [external::custom_swap] *) +let custom_swap_back + (t : Type0) (x : t) (y : t) (st : state) (ret : t) (st0 : state) : + result (state & (t & t)) + = + begin match core_mem_swap_fwd t x y st with + | Fail -> Fail + | Return (st1, _) -> + begin match core_mem_swap_back0 t x y st st1 with + | Fail -> Fail + | Return (st2, _) -> + begin match core_mem_swap_back1 t x y st st2 with + | Fail -> Fail + | Return (_, y0) -> Return (st0, (ret, y0)) + end + end + end + +(** [external::test_custom_swap] *) +let test_custom_swap_fwd + (x : u32) (y : u32) (st : state) : result (state & unit) = + begin match custom_swap_fwd u32 x y st with + | Fail -> Fail + | Return (st0, _) -> Return (st0, ()) + end + +(** [external::test_custom_swap] *) +let test_custom_swap_back + (x : u32) (y : u32) (st : state) (st0 : state) : + result (state & (u32 & u32)) + = + begin match custom_swap_back u32 x y st 1 st0 with + | Fail -> Fail + | Return (st1, (x0, y0)) -> Return (st1, (x0, y0)) + end + +(** [external::test_swap_non_zero] *) +let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) = + begin match swap_fwd u32 x 0 st with + | Fail -> Fail + | Return (st0, _) -> + begin match swap_back u32 x 0 st st0 with + | Fail -> Fail + | Return (st1, (x0, _)) -> if x0 = 0 then Fail else Return (st1, x0) + end + end + diff --git a/tests/fstar/misc/External.Opaque.fsti b/tests/fstar/misc/External.Opaque.fsti new file mode 100644 index 00000000..7d86405a --- /dev/null +++ b/tests/fstar/misc/External.Opaque.fsti @@ -0,0 +1,27 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: opaque function definitions *) +module External.Opaque +open Primitives +include External.Types + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [core::mem::swap] *) +val core_mem_swap_fwd (t : Type0) : t -> t -> state -> result (state & unit) + +(** [core::mem::swap] *) +val core_mem_swap_back0 + (t : Type0) : t -> t -> state -> state -> result (state & t) + +(** [core::mem::swap] *) +val core_mem_swap_back1 + (t : Type0) : t -> t -> state -> state -> result (state & t) + +(** [core::num::nonzero::NonZeroU32::{14}::new] *) +val core_num_nonzero_non_zero_u32_new_fwd + : u32 -> state -> result (state & (option core_num_nonzero_non_zero_u32_t)) + +(** [core::option::Option::{0}::unwrap] *) +val core_option_option_unwrap_fwd + (t : Type0) : option t -> state -> result (state & t) + diff --git a/tests/fstar/misc/External.Types.fsti b/tests/fstar/misc/External.Types.fsti new file mode 100644 index 00000000..4a13a744 --- /dev/null +++ b/tests/fstar/misc/External.Types.fsti @@ -0,0 +1,13 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: type definitions *) +module External.Types +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [core::num::nonzero::NonZeroU32] *) +val core_num_nonzero_non_zero_u32_t : Type0 + +(** The state type used in the state-error monad *) +val state : Type0 + diff --git a/tests/fstar/misc/Makefile b/tests/fstar/misc/Makefile new file mode 100644 index 00000000..a16b0edb --- /dev/null +++ b/tests/fstar/misc/Makefile @@ -0,0 +1,47 @@ +INCLUDE_DIRS = . + +FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) + +FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints + +FSTAR_OPTIONS = $(FSTAR_HINTS) \ + --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ + --warn_error '+241@247+285-274' \ + +FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj + +FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) + +# The F* roots are used to compute the dependency graph, and generate the .depend file +FSTAR_ROOTS ?= $(wildcard *.fst *.fsti) + +# Build all the files +all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS))) + +# This is the right way to ensure the .depend file always gets re-built. +ifeq (,$(filter %-in,$(MAKECMDGOALS))) +ifndef NODEPEND +ifndef MAKE_RESTARTS +.depend: .FORCE + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@ + +.PHONY: .FORCE +.FORCE: +endif +endif + +include .depend +endif + +# For the interactive mode +%.fst-in %.fsti-in: + @echo $(FSTAR_OPTIONS) + +# Generete the .checked files in batch mode +%.checked: + $(FSTAR) $(FSTAR_OPTIONS) $< && \ + touch -c $@ + +.PHONY: clean +clean: + rm -f obj/* diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst new file mode 100644 index 00000000..8161e7cd --- /dev/null +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -0,0 +1,562 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [no_nested_borrows] *) +module NoNestedBorrows +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [no_nested_borrows::Pair] *) +type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; } + +(** [no_nested_borrows::List] *) +type list_t (t : Type0) = +| ListCons : t -> list_t t -> list_t t +| ListNil : list_t t + +(** [no_nested_borrows::One] *) +type one_t (t1 : Type0) = | OneOne : t1 -> one_t t1 + +(** [no_nested_borrows::EmptyEnum] *) +type empty_enum_t = | EmptyEnumEmpty : empty_enum_t + +(** [no_nested_borrows::Enum] *) +type enum_t = | EnumVariant1 : enum_t | EnumVariant2 : enum_t + +(** [no_nested_borrows::EmptyStruct] *) +type empty_struct_t = unit + +(** [no_nested_borrows::Sum] *) +type sum_t (t1 t2 : Type0) = +| SumLeft : t1 -> sum_t t1 t2 +| SumRight : t2 -> sum_t t1 t2 + +(** [no_nested_borrows::neg_test] *) +let neg_test_fwd (x : i32) : result i32 = + begin match i32_neg x with | Fail -> Fail | Return i -> Return i end + +(** [no_nested_borrows::add_test] *) +let add_test_fwd (x : u32) (y : u32) : result u32 = + begin match u32_add x y with | Fail -> Fail | Return i -> Return i end + +(** [no_nested_borrows::subs_test] *) +let subs_test_fwd (x : u32) (y : u32) : result u32 = + begin match u32_sub x y with | Fail -> Fail | Return i -> Return i end + +(** [no_nested_borrows::div_test] *) +let div_test_fwd (x : u32) (y : u32) : result u32 = + begin match u32_div x y with | Fail -> Fail | Return i -> Return i end + +(** [no_nested_borrows::div_test1] *) +let div_test1_fwd (x : u32) : result u32 = + begin match u32_div x 2 with | Fail -> Fail | Return i -> Return i end + +(** [no_nested_borrows::rem_test] *) +let rem_test_fwd (x : u32) (y : u32) : result u32 = + begin match u32_rem x y with | Fail -> Fail | Return i -> Return i end + +(** [no_nested_borrows::cast_test] *) +let cast_test_fwd (x : u32) : result i32 = + begin match scalar_cast U32 I32 x with + | Fail -> Fail + | Return i -> Return i + end + +(** [no_nested_borrows::test2] *) +let test2_fwd : result unit = + begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end + +(** Unit test for [no_nested_borrows::test2] *) +let _ = assert_norm (test2_fwd = Return ()) + +(** [no_nested_borrows::get_max] *) +let get_max_fwd (x : u32) (y : u32) : result u32 = + if x >= y then Return x else Return y + +(** [no_nested_borrows::test3] *) +let test3_fwd : result unit = + begin match get_max_fwd 4 3 with + | Fail -> Fail + | Return x -> + begin match get_max_fwd 10 11 with + | Fail -> Fail + | Return y -> + begin match u32_add x y with + | Fail -> Fail + | Return z -> if not (z = 15) then Fail else Return () + end + end + end + +(** Unit test for [no_nested_borrows::test3] *) +let _ = assert_norm (test3_fwd = Return ()) + +(** [no_nested_borrows::test_neg1] *) +let test_neg1_fwd : result unit = + begin match i32_neg 3 with + | Fail -> Fail + | Return y -> if not (y = -3) then Fail else Return () + end + +(** Unit test for [no_nested_borrows::test_neg1] *) +let _ = assert_norm (test_neg1_fwd = Return ()) + +(** [no_nested_borrows::refs_test1] *) +let refs_test1_fwd : result unit = if not (1 = 1) then Fail else Return () + +(** Unit test for [no_nested_borrows::refs_test1] *) +let _ = assert_norm (refs_test1_fwd = Return ()) + +(** [no_nested_borrows::refs_test2] *) +let refs_test2_fwd : result unit = + if not (2 = 2) + then Fail + else + if not (0 = 0) + then Fail + else if not (2 = 2) then Fail else if not (2 = 2) then Fail else Return () + +(** Unit test for [no_nested_borrows::refs_test2] *) +let _ = assert_norm (refs_test2_fwd = Return ()) + +(** [no_nested_borrows::test_list1] *) +let test_list1_fwd : result unit = Return () + +(** Unit test for [no_nested_borrows::test_list1] *) +let _ = assert_norm (test_list1_fwd = Return ()) + +(** [no_nested_borrows::test_box1] *) +let test_box1_fwd : result unit = + let b = 1 in let x = b in if not (x = 1) then Fail else Return () + +(** Unit test for [no_nested_borrows::test_box1] *) +let _ = assert_norm (test_box1_fwd = Return ()) + +(** [no_nested_borrows::copy_int] *) +let copy_int_fwd (x : i32) : result i32 = Return x + +(** [no_nested_borrows::test_unreachable] *) +let test_unreachable_fwd (b : bool) : result unit = + if b then Fail else Return () + +(** [no_nested_borrows::test_panic] *) +let test_panic_fwd (b : bool) : result unit = if b then Fail else Return () + +(** [no_nested_borrows::test_copy_int] *) +let test_copy_int_fwd : result unit = + begin match copy_int_fwd 0 with + | Fail -> Fail + | Return y -> if not (0 = y) then Fail else Return () + end + +(** Unit test for [no_nested_borrows::test_copy_int] *) +let _ = assert_norm (test_copy_int_fwd = Return ()) + +(** [no_nested_borrows::is_cons] *) +let is_cons_fwd (t : Type0) (l : list_t t) : result bool = + begin match l with + | ListCons x l0 -> Return true + | ListNil -> Return false + end + +(** [no_nested_borrows::test_is_cons] *) +let test_is_cons_fwd : result unit = + let l = ListNil in + begin match is_cons_fwd i32 (ListCons 0 l) with + | Fail -> Fail + | Return b -> if not b then Fail else Return () + end + +(** Unit test for [no_nested_borrows::test_is_cons] *) +let _ = assert_norm (test_is_cons_fwd = Return ()) + +(** [no_nested_borrows::split_list] *) +let split_list_fwd (t : Type0) (l : list_t t) : result (t & (list_t t)) = + begin match l with | ListCons hd tl -> Return (hd, tl) | ListNil -> Fail end + +(** [no_nested_borrows::test_split_list] *) +let test_split_list_fwd : result unit = + let l = ListNil in + begin match split_list_fwd i32 (ListCons 0 l) with + | Fail -> Fail + | Return p -> let (hd, _) = p in if not (hd = 0) then Fail else Return () + end + +(** Unit test for [no_nested_borrows::test_split_list] *) +let _ = assert_norm (test_split_list_fwd = Return ()) + +(** [no_nested_borrows::choose] *) +let choose_fwd (t : Type0) (b : bool) (x : t) (y : t) : result t = + if b then Return x else Return y + +(** [no_nested_borrows::choose] *) +let choose_back + (t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) = + if b then Return (ret, y) else Return (x, ret) + +(** [no_nested_borrows::choose_test] *) +let choose_test_fwd : result unit = + begin match choose_fwd i32 true 0 0 with + | Fail -> Fail + | Return z -> + begin match i32_add z 1 with + | Fail -> Fail + | Return z0 -> + if not (z0 = 1) + then Fail + else + begin match choose_back i32 true 0 0 z0 with + | Fail -> Fail + | Return (x, y) -> + if not (x = 1) then Fail else if not (y = 0) then Fail else Return () + end + end + end + +(** Unit test for [no_nested_borrows::choose_test] *) +let _ = assert_norm (choose_test_fwd = Return ()) + +(** [no_nested_borrows::test_char] *) +let test_char_fwd : result char = Return 'a' + +(** [no_nested_borrows::NodeElem] *) +type node_elem_t (t : Type0) = +| NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t +| NodeElemNil : node_elem_t t + +(** [no_nested_borrows::Tree] *) +and tree_t (t : Type0) = +| TreeLeaf : t -> tree_t t +| TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t + +(** [no_nested_borrows::odd] *) +let rec odd_fwd (x : u32) : result bool = + if x = 0 + then Return false + else + begin match u32_sub x 1 with + | Fail -> Fail + | Return i -> + begin match even_fwd i with | Fail -> Fail | Return b -> Return b end + end + +(** [no_nested_borrows::even] *) +and even_fwd (x : u32) : result bool = + if x = 0 + then Return true + else + begin match u32_sub x 1 with + | Fail -> Fail + | Return i -> + begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end + end + +(** [no_nested_borrows::test_even_odd] *) +let test_even_odd_fwd : result unit = + begin match even_fwd 0 with + | Fail -> Fail + | Return b -> + if not b + then Fail + else + begin match even_fwd 4 with + | Fail -> Fail + | Return b0 -> + if not b0 + then Fail + else + begin match odd_fwd 1 with + | Fail -> Fail + | Return b1 -> + if not b1 + then Fail + else + begin match odd_fwd 5 with + | Fail -> Fail + | Return b2 -> if not b2 then Fail else Return () + end + end + end + end + +(** Unit test for [no_nested_borrows::test_even_odd] *) +let _ = assert_norm (test_even_odd_fwd = Return ()) + +(** [no_nested_borrows::list_length] *) +let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 = + begin match l with + | ListCons x l1 -> + begin match list_length_fwd t l1 with + | Fail -> Fail + | Return i -> + begin match u32_add 1 i with | Fail -> Fail | Return i0 -> Return i0 end + end + | ListNil -> Return 0 + end + +(** [no_nested_borrows::list_nth_shared] *) +let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t = + begin match l with + | ListCons x tl -> + if i = 0 + then Return x + else + begin match u32_sub i 1 with + | Fail -> Fail + | Return i0 -> + begin match list_nth_shared_fwd t tl i0 with + | Fail -> Fail + | Return x0 -> Return x0 + end + end + | ListNil -> Fail + end + +(** [no_nested_borrows::list_nth_mut] *) +let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = + begin match l with + | ListCons x tl -> + if i = 0 + then Return x + else + begin match u32_sub i 1 with + | Fail -> Fail + | Return i0 -> + begin match list_nth_mut_fwd t tl i0 with + | Fail -> Fail + | Return x0 -> Return x0 + end + end + | ListNil -> Fail + end + +(** [no_nested_borrows::list_nth_mut] *) +let rec list_nth_mut_back + (t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) = + begin match l with + | ListCons x tl -> + if i = 0 + then Return (ListCons ret tl) + else + begin match u32_sub i 1 with + | Fail -> Fail + | Return i0 -> + begin match list_nth_mut_back t tl i0 ret with + | Fail -> Fail + | Return tl0 -> Return (ListCons x tl0) + end + end + | ListNil -> Fail + end + +(** [no_nested_borrows::list_rev_aux] *) +let rec list_rev_aux_fwd + (t : Type0) (li : list_t t) (lo : list_t t) : result (list_t t) = + begin match li with + | ListCons hd tl -> + begin match list_rev_aux_fwd t tl (ListCons hd lo) with + | Fail -> Fail + | Return l -> Return l + end + | ListNil -> Return lo + end + +(** [no_nested_borrows::list_rev] *) +let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) = + let li = mem_replace_fwd (list_t t) l ListNil in + begin match list_rev_aux_fwd t li ListNil with + | Fail -> Fail + | Return l0 -> Return l0 + end + +(** [no_nested_borrows::test_list_functions] *) +let test_list_functions_fwd : result unit = + let l = ListNil in + let l0 = ListCons 2 l in + let l1 = ListCons 1 l0 in + begin match list_length_fwd i32 (ListCons 0 l1) with + | Fail -> Fail + | Return i -> + if not (i = 3) + then Fail + else + begin match list_nth_shared_fwd i32 (ListCons 0 l1) 0 with + | Fail -> Fail + | Return i0 -> + if not (i0 = 0) + then Fail + else + begin match list_nth_shared_fwd i32 (ListCons 0 l1) 1 with + | Fail -> Fail + | Return i1 -> + if not (i1 = 1) + then Fail + else + begin match list_nth_shared_fwd i32 (ListCons 0 l1) 2 with + | Fail -> Fail + | Return i2 -> + if not (i2 = 2) + then Fail + else + begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with + | Fail -> Fail + | Return ls -> + begin match list_nth_shared_fwd i32 ls 0 with + | Fail -> Fail + | Return i3 -> + if not (i3 = 0) + then Fail + else + begin match list_nth_shared_fwd i32 ls 1 with + | Fail -> Fail + | Return i4 -> + if not (i4 = 3) + then Fail + else + begin match list_nth_shared_fwd i32 ls 2 with + | Fail -> Fail + | Return i5 -> + if not (i5 = 2) then Fail else Return () + end + end + end + end + end + end + end + end + +(** Unit test for [no_nested_borrows::test_list_functions] *) +let _ = assert_norm (test_list_functions_fwd = Return ()) + +(** [no_nested_borrows::id_mut_pair1] *) +let id_mut_pair1_fwd (t1 t2 : Type0) (x : t1) (y : t2) : result (t1 & t2) = + Return (x, y) + +(** [no_nested_borrows::id_mut_pair1] *) +let id_mut_pair1_back + (t1 t2 : Type0) (x : t1) (y : t2) (ret : (t1 & t2)) : result (t1 & t2) = + let (x0, x1) = ret in Return (x0, x1) + +(** [no_nested_borrows::id_mut_pair2] *) +let id_mut_pair2_fwd (t1 t2 : Type0) (p : (t1 & t2)) : result (t1 & t2) = + let (x, x0) = p in Return (x, x0) + +(** [no_nested_borrows::id_mut_pair2] *) +let id_mut_pair2_back + (t1 t2 : Type0) (p : (t1 & t2)) (ret : (t1 & t2)) : result (t1 & t2) = + let (x, x0) = ret in Return (x, x0) + +(** [no_nested_borrows::id_mut_pair3] *) +let id_mut_pair3_fwd (t1 t2 : Type0) (x : t1) (y : t2) : result (t1 & t2) = + Return (x, y) + +(** [no_nested_borrows::id_mut_pair3] *) +let id_mut_pair3_back'a + (t1 t2 : Type0) (x : t1) (y : t2) (ret : t1) : result t1 = + Return ret + +(** [no_nested_borrows::id_mut_pair3] *) +let id_mut_pair3_back'b + (t1 t2 : Type0) (x : t1) (y : t2) (ret : t2) : result t2 = + Return ret + +(** [no_nested_borrows::id_mut_pair4] *) +let id_mut_pair4_fwd (t1 t2 : Type0) (p : (t1 & t2)) : result (t1 & t2) = + let (x, x0) = p in Return (x, x0) + +(** [no_nested_borrows::id_mut_pair4] *) +let id_mut_pair4_back'a + (t1 t2 : Type0) (p : (t1 & t2)) (ret : t1) : result t1 = + Return ret + +(** [no_nested_borrows::id_mut_pair4] *) +let id_mut_pair4_back'b + (t1 t2 : Type0) (p : (t1 & t2)) (ret : t2) : result t2 = + Return ret + +(** [no_nested_borrows::StructWithTuple] *) +type struct_with_tuple_t (t1 t2 : Type0) = { struct_with_tuple_p : (t1 & t2); } + +(** [no_nested_borrows::new_tuple1] *) +let new_tuple1_fwd : result (struct_with_tuple_t u32 u32) = + Return (Mkstruct_with_tuple_t (1, 2)) + +(** [no_nested_borrows::new_tuple2] *) +let new_tuple2_fwd : result (struct_with_tuple_t i16 i16) = + Return (Mkstruct_with_tuple_t (1, 2)) + +(** [no_nested_borrows::new_tuple3] *) +let new_tuple3_fwd : result (struct_with_tuple_t u64 i64) = + Return (Mkstruct_with_tuple_t (1, 2)) + +(** [no_nested_borrows::StructWithPair] *) +type struct_with_pair_t (t1 t2 : Type0) = +{ + struct_with_pair_p : pair_t t1 t2; +} + +(** [no_nested_borrows::new_pair1] *) +let new_pair1_fwd : result (struct_with_pair_t u32 u32) = + Return (Mkstruct_with_pair_t (Mkpair_t 1 2)) + +(** [no_nested_borrows::test_constants] *) +let test_constants_fwd : result unit = + begin match new_tuple1_fwd with + | Fail -> Fail + | Return swt -> + let (i, _) = swt.struct_with_tuple_p in + if not (i = 1) + then Fail + else + begin match new_tuple2_fwd with + | Fail -> Fail + | Return swt0 -> + let (i0, _) = swt0.struct_with_tuple_p in + if not (i0 = 1) + then Fail + else + begin match new_tuple3_fwd with + | Fail -> Fail + | Return swt1 -> + let (i1, _) = swt1.struct_with_tuple_p in + if not (i1 = 1) + then Fail + else + begin match new_pair1_fwd with + | Fail -> Fail + | Return swp -> + if not (swp.struct_with_pair_p.pair_x = 1) + then Fail + else Return () + end + end + end + end + +(** Unit test for [no_nested_borrows::test_constants] *) +let _ = assert_norm (test_constants_fwd = Return ()) + +(** [no_nested_borrows::test_weird_borrows1] *) +let test_weird_borrows1_fwd : result unit = Return () + +(** Unit test for [no_nested_borrows::test_weird_borrows1] *) +let _ = assert_norm (test_weird_borrows1_fwd = Return ()) + +(** [no_nested_borrows::test_mem_replace] *) +let test_mem_replace_fwd_back (px : u32) : result u32 = + let y = mem_replace_fwd u32 px 1 in if not (y = 0) then Fail else Return 2 + +(** [no_nested_borrows::test_shared_borrow_bool1] *) +let test_shared_borrow_bool1_fwd (b : bool) : result u32 = + if b then Return 0 else Return 1 + +(** [no_nested_borrows::test_shared_borrow_bool2] *) +let test_shared_borrow_bool2_fwd : result u32 = Return 0 + +(** [no_nested_borrows::test_shared_borrow_enum1] *) +let test_shared_borrow_enum1_fwd (l : list_t u32) : result u32 = + begin match l with | ListCons i l0 -> Return 1 | ListNil -> Return 0 end + +(** [no_nested_borrows::test_shared_borrow_enum2] *) +let test_shared_borrow_enum2_fwd : result u32 = Return 0 + diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst new file mode 100644 index 00000000..424889ef --- /dev/null +++ b/tests/fstar/misc/Paper.fst @@ -0,0 +1,147 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [paper] *) +module Paper +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [paper::ref_incr] *) +let ref_incr_fwd_back (x : i32) : result i32 = + begin match i32_add x 1 with | Fail -> Fail | Return x0 -> Return x0 end + +(** [paper::test_incr] *) +let test_incr_fwd : result unit = + begin match ref_incr_fwd_back 0 with + | Fail -> Fail + | Return x -> if not (x = 1) then Fail else Return () + end + +(** Unit test for [paper::test_incr] *) +let _ = assert_norm (test_incr_fwd = Return ()) + +(** [paper::choose] *) +let choose_fwd (t : Type0) (b : bool) (x : t) (y : t) : result t = + if b then Return x else Return y + +(** [paper::choose] *) +let choose_back + (t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) = + if b then Return (ret, y) else Return (x, ret) + +(** [paper::test_choose] *) +let test_choose_fwd : result unit = + begin match choose_fwd i32 true 0 0 with + | Fail -> Fail + | Return z -> + begin match i32_add z 1 with + | Fail -> Fail + | Return z0 -> + if not (z0 = 1) + then Fail + else + begin match choose_back i32 true 0 0 z0 with + | Fail -> Fail + | Return (x, y) -> + if not (x = 1) then Fail else if not (y = 0) then Fail else Return () + end + end + end + +(** Unit test for [paper::test_choose] *) +let _ = assert_norm (test_choose_fwd = Return ()) + +(** [paper::List] *) +type list_t (t : Type0) = +| ListCons : t -> list_t t -> list_t t +| ListNil : list_t t + +(** [paper::list_nth_mut] *) +let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t = + begin match l with + | ListCons x tl -> + if i = 0 + then Return x + else + begin match u32_sub i 1 with + | Fail -> Fail + | Return i0 -> + begin match list_nth_mut_fwd t tl i0 with + | Fail -> Fail + | Return x0 -> Return x0 + end + end + | ListNil -> Fail + end + +(** [paper::list_nth_mut] *) +let rec list_nth_mut_back + (t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) = + begin match l with + | ListCons x tl -> + if i = 0 + then Return (ListCons ret tl) + else + begin match u32_sub i 1 with + | Fail -> Fail + | Return i0 -> + begin match list_nth_mut_back t tl i0 ret with + | Fail -> Fail + | Return tl0 -> Return (ListCons x tl0) + end + end + | ListNil -> Fail + end + +(** [paper::sum] *) +let rec sum_fwd (l : list_t i32) : result i32 = + begin match l with + | ListCons x tl -> + begin match sum_fwd tl with + | Fail -> Fail + | Return i -> + begin match i32_add x i with | Fail -> Fail | Return i0 -> Return i0 end + end + | ListNil -> Return 0 + end + +(** [paper::test_nth] *) +let test_nth_fwd : result unit = + let l = ListNil in + let l0 = ListCons 3 l in + let l1 = ListCons 2 l0 in + begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with + | Fail -> Fail + | Return x -> + begin match i32_add x 1 with + | Fail -> Fail + | Return x0 -> + begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with + | Fail -> Fail + | Return l2 -> + begin match sum_fwd l2 with + | Fail -> Fail + | Return i -> if not (i = 7) then Fail else Return () + end + end + end + end + +(** Unit test for [paper::test_nth] *) +let _ = assert_norm (test_nth_fwd = Return ()) + +(** [paper::call_choose] *) +let call_choose_fwd (p : (u32 & u32)) : result u32 = + let (px, py) = p in + begin match choose_fwd u32 true px py with + | Fail -> Fail + | Return pz -> + begin match u32_add pz 1 with + | Fail -> Fail + | Return pz0 -> + begin match choose_back u32 true px py pz0 with + | Fail -> Fail + | Return (px0, _) -> Return px0 + end + end + end + diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst new file mode 100644 index 00000000..73e98884 --- /dev/null +++ b/tests/fstar/misc/PoloniusList.fst @@ -0,0 +1,41 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [polonius_list] *) +module PoloniusList +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [polonius_list::List] *) +type list_t (t : Type0) = +| ListCons : t -> list_t t -> list_t t +| ListNil : list_t t + +(** [polonius_list::get_list_at_x] *) +let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) = + begin match ls with + | ListCons hd tl -> + if hd = x + then Return (ListCons hd tl) + else + begin match get_list_at_x_fwd tl x with + | Fail -> Fail + | Return l -> Return l + end + | ListNil -> Return ListNil + end + +(** [polonius_list::get_list_at_x] *) +let rec get_list_at_x_back + (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) = + begin match ls with + | ListCons hd tl -> + if hd = x + then Return ret + else + begin match get_list_at_x_back tl x ret with + | Fail -> Fail + | Return tl0 -> Return (ListCons hd tl0) + end + | ListNil -> Return ret + end + diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst new file mode 100644 index 00000000..96138e46 --- /dev/null +++ b/tests/fstar/misc/Primitives.fst @@ -0,0 +1,287 @@ +/// This file lists primitive and assumed functions and types +module Primitives +open FStar.Mul +open FStar.List.Tot + +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" + +(*** Utilities *) +val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) : + ls':list a{ + length ls' = length ls /\ + index ls' i == x + } +#push-options "--fuel 1" +let rec list_update #a ls i x = + match ls with + | x' :: ls -> if i = 0 then x :: ls else x' :: list_update ls (i-1) x +#pop-options + +(*** Result *) +type result (a : Type0) : Type0 = +| Return : v:a -> result a +| Fail : result a + +// Monadic bind and return. +// Re-definining those allows us to customize the result of the monadic notations +// like: `y <-- f x;` +let return (#a : Type0) (x:a) : result a = Return x +let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = + match m with + | Return x -> f x + | Fail -> Fail + +// Monadic assert(...) +let massert (b:bool) : result unit = if b then Return () else Fail + +// Normalize and unwrap a successful result (used for globals). +let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x + +(*** Misc *) +type char = FStar.Char.char +type string = string + +let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x +let mem_replace_back (a : Type0) (x : a) (y : a) : a = y + +(*** Scalars *) +/// Rk.: most of the following code was at least partially generated + +let isize_min : int = -9223372036854775808 // TODO: should be opaque +let isize_max : int = 9223372036854775807 // TODO: should be opaque +let i8_min : int = -128 +let i8_max : int = 127 +let i16_min : int = -32768 +let i16_max : int = 32767 +let i32_min : int = -2147483648 +let i32_max : int = 2147483647 +let i64_min : int = -9223372036854775808 +let i64_max : int = 9223372036854775807 +let i128_min : int = -170141183460469231731687303715884105728 +let i128_max : int = 170141183460469231731687303715884105727 +let usize_min : int = 0 +let usize_max : int = 4294967295 // TODO: should be opaque +let u8_min : int = 0 +let u8_max : int = 255 +let u16_min : int = 0 +let u16_max : int = 65535 +let u32_min : int = 0 +let u32_max : int = 4294967295 +let u64_min : int = 0 +let u64_max : int = 18446744073709551615 +let u128_min : int = 0 +let u128_max : int = 340282366920938463463374607431768211455 + +type scalar_ty = +| Isize +| I8 +| I16 +| I32 +| I64 +| I128 +| Usize +| U8 +| U16 +| U32 +| U64 +| U128 + +let scalar_min (ty : scalar_ty) : int = + match ty with + | Isize -> isize_min + | I8 -> i8_min + | I16 -> i16_min + | I32 -> i32_min + | I64 -> i64_min + | I128 -> i128_min + | Usize -> usize_min + | U8 -> u8_min + | U16 -> u16_min + | U32 -> u32_min + | U64 -> u64_min + | U128 -> u128_min + +let scalar_max (ty : scalar_ty) : int = + match ty with + | Isize -> isize_max + | I8 -> i8_max + | I16 -> i16_max + | I32 -> i32_max + | I64 -> i64_max + | I128 -> i128_max + | Usize -> usize_max + | U8 -> u8_max + | U16 -> u16_max + | U32 -> u32_max + | U64 -> u64_max + | U128 -> u128_max + +type scalar (ty : scalar_ty) : eqtype = x:int{scalar_min ty <= x && x <= scalar_max ty} + +let mk_scalar (ty : scalar_ty) (x : int) : result (scalar ty) = + if scalar_min ty <= x && scalar_max ty >= x then Return x else Fail + +let scalar_neg (#ty : scalar_ty) (x : scalar ty) : result (scalar ty) = mk_scalar ty (-x) + +let scalar_div (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = + if y <> 0 then mk_scalar ty (x / y) else Fail + +/// The remainder operation +let int_rem (x : int) (y : int{y <> 0}) : int = + if x >= 0 then (x % y) else -(x % y) + +(* Checking consistency with Rust *) +let _ = assert_norm(int_rem 1 2 = 1) +let _ = assert_norm(int_rem (-1) 2 = -1) +let _ = assert_norm(int_rem 1 (-2) = 1) +let _ = assert_norm(int_rem (-1) (-2) = -1) + +let scalar_rem (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = + if y <> 0 then mk_scalar ty (int_rem x y) else Fail + +let scalar_add (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = + mk_scalar ty (x + y) + +let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = + mk_scalar ty (x - y) + +let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) = + mk_scalar ty (x * y) + +(** Cast an integer from a [src_ty] to a [tgt_ty] *) +// TODO: check the semantics of casts in Rust +let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = + mk_scalar tgt_ty x + +/// The scalar types +type isize : eqtype = scalar Isize +type i8 : eqtype = scalar I8 +type i16 : eqtype = scalar I16 +type i32 : eqtype = scalar I32 +type i64 : eqtype = scalar I64 +type i128 : eqtype = scalar I128 +type usize : eqtype = scalar Usize +type u8 : eqtype = scalar U8 +type u16 : eqtype = scalar U16 +type u32 : eqtype = scalar U32 +type u64 : eqtype = scalar U64 +type u128 : eqtype = scalar U128 + +/// Negation +let isize_neg = scalar_neg #Isize +let i8_neg = scalar_neg #I8 +let i16_neg = scalar_neg #I16 +let i32_neg = scalar_neg #I32 +let i64_neg = scalar_neg #I64 +let i128_neg = scalar_neg #I128 + +/// Division +let isize_div = scalar_div #Isize +let i8_div = scalar_div #I8 +let i16_div = scalar_div #I16 +let i32_div = scalar_div #I32 +let i64_div = scalar_div #I64 +let i128_div = scalar_div #I128 +let usize_div = scalar_div #Usize +let u8_div = scalar_div #U8 +let u16_div = scalar_div #U16 +let u32_div = scalar_div #U32 +let u64_div = scalar_div #U64 +let u128_div = scalar_div #U128 + +/// Remainder +let isize_rem = scalar_rem #Isize +let i8_rem = scalar_rem #I8 +let i16_rem = scalar_rem #I16 +let i32_rem = scalar_rem #I32 +let i64_rem = scalar_rem #I64 +let i128_rem = scalar_rem #I128 +let usize_rem = scalar_rem #Usize +let u8_rem = scalar_rem #U8 +let u16_rem = scalar_rem #U16 +let u32_rem = scalar_rem #U32 +let u64_rem = scalar_rem #U64 +let u128_rem = scalar_rem #U128 + +/// Addition +let isize_add = scalar_add #Isize +let i8_add = scalar_add #I8 +let i16_add = scalar_add #I16 +let i32_add = scalar_add #I32 +let i64_add = scalar_add #I64 +let i128_add = scalar_add #I128 +let usize_add = scalar_add #Usize +let u8_add = scalar_add #U8 +let u16_add = scalar_add #U16 +let u32_add = scalar_add #U32 +let u64_add = scalar_add #U64 +let u128_add = scalar_add #U128 + +/// Substraction +let isize_sub = scalar_sub #Isize +let i8_sub = scalar_sub #I8 +let i16_sub = scalar_sub #I16 +let i32_sub = scalar_sub #I32 +let i64_sub = scalar_sub #I64 +let i128_sub = scalar_sub #I128 +let usize_sub = scalar_sub #Usize +let u8_sub = scalar_sub #U8 +let u16_sub = scalar_sub #U16 +let u32_sub = scalar_sub #U32 +let u64_sub = scalar_sub #U64 +let u128_sub = scalar_sub #U128 + +/// Multiplication +let isize_mul = scalar_mul #Isize +let i8_mul = scalar_mul #I8 +let i16_mul = scalar_mul #I16 +let i32_mul = scalar_mul #I32 +let i64_mul = scalar_mul #I64 +let i128_mul = scalar_mul #I128 +let usize_mul = scalar_mul #Usize +let u8_mul = scalar_mul #U8 +let u16_mul = scalar_mul #U16 +let u32_mul = scalar_mul #U32 +let u64_mul = scalar_mul #U64 +let u128_mul = scalar_mul #U128 + +(*** Vector *) +type vec (a : Type0) = v:list a{length v <= usize_max} + +let vec_new (a : Type0) : vec a = assert_norm(length #a [] == 0); [] +let vec_len (a : Type0) (v : vec a) : usize = length v + +// The **forward** function shouldn't be used +let vec_push_fwd (a : Type0) (v : vec a) (x : a) : unit = () +let vec_push_back (a : Type0) (v : vec a) (x : a) : + Pure (result (vec a)) + (requires True) + (ensures (fun res -> + match res with + | Fail -> True + | Return v' -> length v' = length v + 1)) = + if length v < usize_max then begin + (**) assert_norm(length [x] == 1); + (**) append_length v [x]; + (**) assert(length (append v [x]) = length v + 1); + Return (append v [x]) + end + else Fail + +// The **forward** function shouldn't be used +let vec_insert_fwd (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = + if i < length v then Return () else Fail +let vec_insert_back (a : Type0) (v : vec a) (i : usize) (x : a) : result (vec a) = + if i < length v then Return (list_update v i x) else Fail + +// The **backward** function shouldn't be used +let vec_index_fwd (a : Type0) (v : vec a) (i : usize) : result a = + if i < length v then Return (index v i) else Fail +let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = + if i < length v then Return () else Fail + +let vec_index_mut_fwd (a : Type0) (v : vec a) (i : usize) : result a = + if i < length v then Return (index v i) else Fail +let vec_index_mut_back (a : Type0) (v : vec a) (i : usize) (nx : a) : result (vec a) = + if i < length v then Return (list_update v i nx) else Fail + |