diff options
author | Son HO | 2023-08-07 10:42:15 +0200 |
---|---|---|
committer | GitHub | 2023-08-07 10:42:15 +0200 |
commit | 1cbc7ce007cf3433a6df9bdeb12c4e27511fad9c (patch) | |
tree | c15a16b591cf25df3ccff87ad4cd7c46ddecc489 /tests/fstar | |
parent | 887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (diff) | |
parent | 9e14cdeaf429e9faff2d1efdcf297c1ac7dc7f1f (diff) |
Merge pull request #32 from AeneasVerif/son_arrays
Add support for arrays/slices and const generics
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/.gitignore | 1 | ||||
-rw-r--r-- | tests/fstar/array/Array.Clauses.Template.fst | 18 | ||||
-rw-r--r-- | tests/fstar/array/Array.Clauses.fst | 19 | ||||
-rw-r--r-- | tests/fstar/array/Array.Funs.fst | 355 | ||||
-rw-r--r-- | tests/fstar/array/Array.Types.fst | 10 | ||||
-rw-r--r-- | tests/fstar/array/Makefile | 49 | ||||
-rw-r--r-- | tests/fstar/array/Primitives.fst | 375 | ||||
-rw-r--r-- | tests/fstar/betree/Primitives.fst | 75 | ||||
-rw-r--r-- | tests/fstar/betree_back_stateful/Primitives.fst | 75 | ||||
-rw-r--r-- | tests/fstar/hashmap/Primitives.fst | 75 | ||||
-rw-r--r-- | tests/fstar/hashmap_on_disk/Primitives.fst | 75 | ||||
-rw-r--r-- | tests/fstar/misc/Primitives.fst | 75 |
12 files changed, 1202 insertions, 0 deletions
diff --git a/tests/fstar/.gitignore b/tests/fstar/.gitignore new file mode 100644 index 00000000..28a11147 --- /dev/null +++ b/tests/fstar/.gitignore @@ -0,0 +1 @@ +*/obj
\ No newline at end of file diff --git a/tests/fstar/array/Array.Clauses.Template.fst b/tests/fstar/array/Array.Clauses.Template.fst new file mode 100644 index 00000000..8a15e230 --- /dev/null +++ b/tests/fstar/array/Array.Clauses.Template.fst @@ -0,0 +1,18 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [array]: templates for the decreases clauses *) +module Array.Clauses.Template +open Primitives +open Array.Types + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [array::sum]: decreases clause *) +unfold +let sum_loop_decreases (s : slice u32) (sum : u32) (i : usize) : nat = admit () + +(** [array::sum2]: decreases clause *) +unfold +let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum : u32) + (i : usize) : nat = + admit () + diff --git a/tests/fstar/array/Array.Clauses.fst b/tests/fstar/array/Array.Clauses.fst new file mode 100644 index 00000000..68cbf216 --- /dev/null +++ b/tests/fstar/array/Array.Clauses.fst @@ -0,0 +1,19 @@ +(** [array]: decreases clauses *) +module Array.Clauses +open Primitives +open Array.Types +open FStar.List.Tot + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [array::sum]: decreases clause *) +unfold +let sum_loop_decreases (s : slice u32) (sum : u32) (i : usize) : nat = + if i < length s then length s - i else 0 + +(** [array::sum2]: decreases clause *) +unfold +let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum : u32) + (i : usize) : nat = + if i < length s then length s - i else 0 + diff --git a/tests/fstar/array/Array.Funs.fst b/tests/fstar/array/Array.Funs.fst new file mode 100644 index 00000000..7c1d0b09 --- /dev/null +++ b/tests/fstar/array/Array.Funs.fst @@ -0,0 +1,355 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [array]: function definitions *) +module Array.Funs +open Primitives +include Array.Types +include Array.Clauses + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [array::array_to_shared_slice_]: forward function *) +let array_to_shared_slice__fwd + (t : Type0) (s : array t 32) : result (slice t) = + array_to_slice_shared t 32 s + +(** [array::array_to_mut_slice_]: forward function *) +let array_to_mut_slice__fwd (t : Type0) (s : array t 32) : result (slice t) = + array_to_slice_mut_fwd t 32 s + +(** [array::array_to_mut_slice_]: backward function 0 *) +let array_to_mut_slice__back + (t : Type0) (s : array t 32) (ret : slice t) : result (array t 32) = + array_to_slice_mut_back t 32 s ret + +(** [array::array_len]: forward function *) +let array_len_fwd (t : Type0) (s : array t 32) : result usize = + let* s0 = array_to_slice_shared t 32 s in let i = slice_len t s0 in Return i + +(** [array::shared_array_len]: forward function *) +let shared_array_len_fwd (t : Type0) (s : array t 32) : result usize = + let* s0 = array_to_slice_shared t 32 s in let i = slice_len t s0 in Return i + +(** [array::shared_slice_len]: forward function *) +let shared_slice_len_fwd (t : Type0) (s : slice t) : result usize = + let i = slice_len t s in Return i + +(** [array::index_array_shared]: forward function *) +let index_array_shared_fwd + (t : Type0) (s : array t 32) (i : usize) : result t = + array_index_shared t 32 s i + +(** [array::index_array_u32]: forward function *) +let index_array_u32_fwd (s : array u32 32) (i : usize) : result u32 = + array_index_shared u32 32 s i + +(** [array::index_array_generic]: forward function *) +let 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 *) +let 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 *) +let index_array_copy_fwd (x : array u32 32) : result u32 = + array_index_shared u32 32 x 0 + +(** [array::index_mut_array]: forward function *) +let index_mut_array_fwd (t : Type0) (s : array t 32) (i : usize) : result t = + array_index_mut_fwd t 32 s i + +(** [array::index_mut_array]: backward function 0 *) +let index_mut_array_back + (t : Type0) (s : array t 32) (i : usize) (ret : t) : result (array t 32) = + array_index_mut_back t 32 s i ret + +(** [array::index_slice]: forward function *) +let index_slice_fwd (t : Type0) (s : slice t) (i : usize) : result t = + slice_index_shared t s i + +(** [array::index_mut_slice]: forward function *) +let index_mut_slice_fwd (t : Type0) (s : slice t) (i : usize) : result t = + slice_index_mut_fwd t s i + +(** [array::index_mut_slice]: backward function 0 *) +let index_mut_slice_back + (t : Type0) (s : slice t) (i : usize) (ret : t) : result (slice t) = + slice_index_mut_back t s i ret + +(** [array::slice_subslice_shared_]: forward function *) +let slice_subslice_shared__fwd + (x : slice u32) (y : usize) (z : usize) : result (slice u32) = + slice_subslice_shared u32 x (Mkrange y z) + +(** [array::slice_subslice_mut_]: forward function *) +let slice_subslice_mut__fwd + (x : slice u32) (y : usize) (z : usize) : result (slice u32) = + slice_subslice_mut_fwd u32 x (Mkrange y z) + +(** [array::slice_subslice_mut_]: backward function 0 *) +let slice_subslice_mut__back + (x : slice u32) (y : usize) (z : usize) (ret : slice u32) : + result (slice u32) + = + slice_subslice_mut_back u32 x (Mkrange y z) ret + +(** [array::array_to_slice_shared_]: forward function *) +let array_to_slice_shared__fwd (x : array u32 32) : result (slice u32) = + array_to_slice_shared u32 32 x + +(** [array::array_to_slice_mut_]: forward function *) +let array_to_slice_mut__fwd (x : array u32 32) : result (slice u32) = + array_to_slice_mut_fwd u32 32 x + +(** [array::array_to_slice_mut_]: backward function 0 *) +let array_to_slice_mut__back + (x : array u32 32) (ret : slice u32) : result (array u32 32) = + array_to_slice_mut_back u32 32 x ret + +(** [array::array_subslice_shared_]: forward function *) +let array_subslice_shared__fwd + (x : array u32 32) (y : usize) (z : usize) : result (slice u32) = + array_subslice_shared u32 32 x (Mkrange y z) + +(** [array::array_subslice_mut_]: forward function *) +let array_subslice_mut__fwd + (x : array u32 32) (y : usize) (z : usize) : result (slice u32) = + array_subslice_mut_fwd u32 32 x (Mkrange y z) + +(** [array::array_subslice_mut_]: backward function 0 *) +let array_subslice_mut__back + (x : array u32 32) (y : usize) (z : usize) (ret : slice u32) : + result (array u32 32) + = + array_subslice_mut_back u32 32 x (Mkrange y z) ret + +(** [array::index_slice_0]: forward function *) +let index_slice_0_fwd (t : Type0) (s : slice t) : result t = + slice_index_shared t s 0 + +(** [array::index_array_0]: forward function *) +let index_array_0_fwd (t : Type0) (s : array t 32) : result t = + array_index_shared t 32 s 0 + +(** [array::index_index_array]: forward function *) +let index_index_array_fwd + (s : array (array u32 32) 32) (i : usize) (j : usize) : result u32 = + let* a = array_index_shared (array u32 32) 32 s i in + array_index_shared u32 32 a j + +(** [array::update_update_array]: forward function *) +let update_update_array_fwd + (s : array (array u32 32) 32) (i : usize) (j : usize) : result unit = + let* a = array_index_mut_fwd (array u32 32) 32 s i in + let* a0 = array_index_mut_back u32 32 a j 0 in + let* _ = array_index_mut_back (array u32 32) 32 s i a0 in + Return () + +(** [array::array_local_deep_copy]: forward function *) +let array_local_deep_copy_fwd (x : array u32 32) : result unit = + Return () + +(** [array::take_array]: forward function *) +let take_array_fwd (a : array u32 2) : result unit = + Return () + +(** [array::take_array_borrow]: forward function *) +let take_array_borrow_fwd (a : array u32 2) : result unit = + Return () + +(** [array::take_slice]: forward function *) +let take_slice_fwd (s : slice u32) : result unit = + Return () + +(** [array::take_mut_slice]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +let take_mut_slice_fwd_back (s : slice u32) : result (slice u32) = + Return s + +(** [array::take_all]: forward function *) +let take_all_fwd : result unit = + let* _ = take_array_fwd (mk_array u32 2 [ 0; 0 ]) in + let* _ = take_array_borrow_fwd (mk_array u32 2 [ 0; 0 ]) in + let* s = array_to_slice_shared u32 2 (mk_array u32 2 [ 0; 0 ]) in + let* _ = take_slice_fwd s in + let* s0 = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 0; 0 ]) in + let* s1 = take_mut_slice_fwd_back s0 in + let* _ = array_to_slice_mut_back u32 2 (mk_array u32 2 [ 0; 0 ]) s1 in + Return () + +(** [array::index_array]: forward function *) +let index_array_fwd (x : array u32 2) : result u32 = + array_index_shared u32 2 x 0 + +(** [array::index_array_borrow]: forward function *) +let index_array_borrow_fwd (x : array u32 2) : result u32 = + array_index_shared u32 2 x 0 + +(** [array::index_slice_u32_0]: forward function *) +let index_slice_u32_0_fwd (x : slice u32) : result u32 = + slice_index_shared u32 x 0 + +(** [array::index_mut_slice_u32_0]: forward function *) +let index_mut_slice_u32_0_fwd (x : slice u32) : result u32 = + slice_index_shared u32 x 0 + +(** [array::index_mut_slice_u32_0]: backward function 0 *) +let index_mut_slice_u32_0_back (x : slice u32) : result (slice u32) = + let* _ = slice_index_shared u32 x 0 in Return x + +(** [array::index_all]: forward function *) +let index_all_fwd : result u32 = + let* i = index_array_fwd (mk_array u32 2 [ 0; 0 ]) in + let* i0 = index_array_fwd (mk_array u32 2 [ 0; 0 ]) in + let* i1 = u32_add i i0 in + let* i2 = index_array_borrow_fwd (mk_array u32 2 [ 0; 0 ]) in + let* i3 = u32_add i1 i2 in + let* s = array_to_slice_shared u32 2 (mk_array u32 2 [ 0; 0 ]) in + let* i4 = index_slice_u32_0_fwd s in + let* i5 = u32_add i3 i4 in + let* s0 = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 0; 0 ]) in + let* i6 = index_mut_slice_u32_0_fwd s0 in + let* i7 = u32_add i5 i6 in + let* s1 = index_mut_slice_u32_0_back s0 in + let* _ = array_to_slice_mut_back u32 2 (mk_array u32 2 [ 0; 0 ]) s1 in + Return i7 + +(** [array::update_array]: forward function *) +let update_array_fwd (x : array u32 2) : result unit = + let* _ = array_index_mut_back u32 2 x 0 1 in Return () + +(** [array::update_array_mut_borrow]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +let update_array_mut_borrow_fwd_back (x : array u32 2) : result (array u32 2) = + array_index_mut_back u32 2 x 0 1 + +(** [array::update_mut_slice]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +let update_mut_slice_fwd_back (x : slice u32) : result (slice u32) = + slice_index_mut_back u32 x 0 1 + +(** [array::update_all]: forward function *) +let update_all_fwd : result unit = + let* _ = update_array_fwd (mk_array u32 2 [ 0; 0 ]) in + let* x = update_array_mut_borrow_fwd_back (mk_array u32 2 [ 0; 0 ]) in + let* s = array_to_slice_mut_fwd u32 2 x in + let* s0 = update_mut_slice_fwd_back s in + let* _ = array_to_slice_mut_back u32 2 x s0 in + Return () + +(** [array::range_all]: forward function *) +let range_all_fwd : result unit = + let* s = + array_subslice_mut_fwd u32 4 (mk_array u32 4 [ 0; 0; 0; 0 ]) (Mkrange 1 3) + in + let* s0 = update_mut_slice_fwd_back s in + let* _ = + array_subslice_mut_back u32 4 (mk_array u32 4 [ 0; 0; 0; 0 ]) (Mkrange 1 3) + s0 in + Return () + +(** [array::deref_array_borrow]: forward function *) +let deref_array_borrow_fwd (x : array u32 2) : result u32 = + array_index_shared u32 2 x 0 + +(** [array::deref_array_mut_borrow]: forward function *) +let deref_array_mut_borrow_fwd (x : array u32 2) : result u32 = + array_index_shared u32 2 x 0 + +(** [array::deref_array_mut_borrow]: backward function 0 *) +let deref_array_mut_borrow_back (x : array u32 2) : result (array u32 2) = + let* _ = array_index_shared u32 2 x 0 in Return x + +(** [array::take_array_t]: forward function *) +let take_array_t_fwd (a : array t_t 2) : result unit = + Return () + +(** [array::non_copyable_array]: forward function *) +let non_copyable_array_fwd : result unit = + let* _ = take_array_t_fwd (mk_array t_t 2 [ TA; TB ]) in Return () + +(** [array::sum]: loop 0: forward function *) +let rec sum_loop_fwd + (s : slice u32) (sum : u32) (i : usize) : + Tot (result u32) (decreases (sum_loop_decreases s sum i)) + = + let i0 = slice_len u32 s in + if i < i0 + then + let* i1 = slice_index_shared u32 s i in + let* sum0 = u32_add sum i1 in + let* i2 = usize_add i 1 in + sum_loop_fwd s sum0 i2 + else Return sum + +(** [array::sum]: forward function *) +let sum_fwd (s : slice u32) : result u32 = + sum_loop_fwd s 0 0 + +(** [array::sum2]: loop 0: forward function *) +let rec sum2_loop_fwd + (s : slice u32) (s2 : slice u32) (sum : u32) (i : usize) : + Tot (result u32) (decreases (sum2_loop_decreases s s2 sum i)) + = + let i0 = slice_len u32 s in + if i < i0 + then + let* i1 = slice_index_shared u32 s i in + let* i2 = slice_index_shared u32 s2 i in + let* i3 = u32_add i1 i2 in + let* sum0 = u32_add sum i3 in + let* i4 = usize_add i 1 in + sum2_loop_fwd s s2 sum0 i4 + else Return sum + +(** [array::sum2]: forward function *) +let sum2_fwd (s : slice u32) (s2 : slice u32) : result u32 = + let i = slice_len u32 s in + let i0 = slice_len u32 s2 in + if not (i = i0) then Fail Failure else sum2_loop_fwd s s2 0 0 + +(** [array::f0]: forward function *) +let f0_fwd : result unit = + let* s = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 1; 2 ]) in + let* s0 = slice_index_mut_back u32 s 0 1 in + let* _ = array_to_slice_mut_back u32 2 (mk_array u32 2 [ 1; 2 ]) s0 in + Return () + +(** [array::f1]: forward function *) +let f1_fwd : result unit = + let* _ = array_index_mut_back u32 2 (mk_array u32 2 [ 1; 2 ]) 0 1 in + Return () + +(** [array::f2]: forward function *) +let f2_fwd (i : u32) : result unit = + Return () + +(** [array::f4]: forward function *) +let f4_fwd (x : array u32 32) (y : usize) (z : usize) : result (slice u32) = + array_subslice_shared u32 32 x (Mkrange y z) + +(** [array::f3]: forward function *) +let f3_fwd : result u32 = + let* i = array_index_shared u32 2 (mk_array u32 2 [ 1; 2 ]) 0 in + let* _ = f2_fwd i in + let* s = array_to_slice_shared u32 2 (mk_array u32 2 [ 1; 2 ]) in + let* s0 = + f4_fwd + (mk_array u32 32 [ + 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; + 0; 0; 0; 0; 0; 0; 0; 0 + ]) 16 18 in + sum2_fwd s s0 + +(** [array::ite]: forward function *) +let ite_fwd : result unit = + let* s = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 0; 0 ]) in + let* s0 = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 0; 0 ]) in + let* s1 = index_mut_slice_u32_0_back s0 in + let* _ = array_to_slice_mut_back u32 2 (mk_array u32 2 [ 0; 0 ]) s1 in + let* s2 = index_mut_slice_u32_0_back s in + let* _ = array_to_slice_mut_back u32 2 (mk_array u32 2 [ 0; 0 ]) s2 in + Return () + diff --git a/tests/fstar/array/Array.Types.fst b/tests/fstar/array/Array.Types.fst new file mode 100644 index 00000000..5e8e81d8 --- /dev/null +++ b/tests/fstar/array/Array.Types.fst @@ -0,0 +1,10 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [array]: type definitions *) +module Array.Types +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [array::T] *) +type t_t = | TA : t_t | TB : t_t + diff --git a/tests/fstar/array/Makefile b/tests/fstar/array/Makefile new file mode 100644 index 00000000..fa7d1f36 --- /dev/null +++ b/tests/fstar/array/Makefile @@ -0,0 +1,49 @@ +# This file was automatically generated - modify ../Makefile.template instead +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_EXE ?= fstar.exe +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/array/Primitives.fst b/tests/fstar/array/Primitives.fst new file mode 100644 index 00000000..9db82069 --- /dev/null +++ b/tests/fstar/array/Primitives.fst @@ -0,0 +1,375 @@ +/// 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 error : Type0 = +| Failure +| OutOfFuel + +type result (a : Type0) : Type0 = +| Return : v:a -> result a +| Fail : e:error -> result a + +// Monadic return operator +unfold let return (#a : Type0) (x : a) : result a = Return x + +// Monadic bind operator. +// Allows to use the notation: +// ``` +// let* x = y in +// ... +// ``` +unfold let (let*) (#a #b : Type0) (m: result a) + (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) : + result b = + match m with + | Return x -> f x + | Fail e -> Fail e + +// Monadic assert(...) +let massert (b:bool) : result unit = if b then Return () else Fail Failure + +// 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 is_zero (n: nat) : bool = n = 0 +let decrease (n: nat{n > 0}) : nat = n - 1 + +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 *) +/// Rem.: most of the following code was 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 Failure + +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 Failure + +/// 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 Failure + +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 + +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + +(*** 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 e -> e == Failure + | 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 Failure + +// 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 Failure +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 Failure + +// 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 Failure +let vec_index_back (a : Type0) (v : vec a) (i : usize) (x : a) : result unit = + if i < length v then Return () else Fail Failure + +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 Failure +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 Failure diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst index 98a696b6..9db82069 100644 --- a/tests/fstar/betree/Primitives.fst +++ b/tests/fstar/betree/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst index 98a696b6..9db82069 100644 --- a/tests/fstar/betree_back_stateful/Primitives.fst +++ b/tests/fstar/betree_back_stateful/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst index 98a696b6..9db82069 100644 --- a/tests/fstar/hashmap/Primitives.fst +++ b/tests/fstar/hashmap/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst index 98a696b6..9db82069 100644 --- a/tests/fstar/hashmap_on_disk/Primitives.fst +++ b/tests/fstar/hashmap_on_disk/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst index 98a696b6..9db82069 100644 --- a/tests/fstar/misc/Primitives.fst +++ b/tests/fstar/misc/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} |