summaryrefslogtreecommitdiff
path: root/tests/fstar/misc
diff options
context:
space:
mode:
authorSon HO2023-08-07 10:42:15 +0200
committerGitHub2023-08-07 10:42:15 +0200
commit1cbc7ce007cf3433a6df9bdeb12c4e27511fad9c (patch)
treec15a16b591cf25df3ccff87ad4cd7c46ddecc489 /tests/fstar/misc
parent887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (diff)
parent9e14cdeaf429e9faff2d1efdcf297c1ac7dc7f1f (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/misc/Primitives.fst75
1 files changed, 75 insertions, 0 deletions
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}