summaryrefslogtreecommitdiff
path: root/tests/fstar/arrays
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/arrays')
-rw-r--r--tests/fstar/arrays/Arrays.Clauses.Template.fst17
-rw-r--r--tests/fstar/arrays/Arrays.Clauses.fst18
-rw-r--r--tests/fstar/arrays/Arrays.Funs.fst55
3 files changed, 90 insertions, 0 deletions
diff --git a/tests/fstar/arrays/Arrays.Clauses.Template.fst b/tests/fstar/arrays/Arrays.Clauses.Template.fst
index 8cc32583..89654992 100644
--- a/tests/fstar/arrays/Arrays.Clauses.Template.fst
+++ b/tests/fstar/arrays/Arrays.Clauses.Template.fst
@@ -19,3 +19,20 @@ let sum2_loop_decreases (s : slice u32) (s2 : slice u32) (sum1 : u32)
(i : usize) : nat =
admit ()
+(** [arrays::zero_slice]: decreases clause
+ Source: 'src/arrays.rs', lines 303:0-310:1 *)
+unfold
+let zero_slice_loop_decreases (a : slice u8) (i : usize) (len : usize) : nat =
+ admit ()
+
+(** [arrays::iter_mut_slice]: decreases clause
+ Source: 'src/arrays.rs', lines 312:0-318:1 *)
+unfold
+let iter_mut_slice_loop_decreases (len : usize) (i : usize) : nat = admit ()
+
+(** [arrays::sum_mut_slice]: decreases clause
+ Source: 'src/arrays.rs', lines 320:0-328:1 *)
+unfold
+let sum_mut_slice_loop_decreases (a : slice u32) (i : usize) (s : u32) : nat =
+ admit ()
+
diff --git a/tests/fstar/arrays/Arrays.Clauses.fst b/tests/fstar/arrays/Arrays.Clauses.fst
index aca328c2..f314eabf 100644
--- a/tests/fstar/arrays/Arrays.Clauses.fst
+++ b/tests/fstar/arrays/Arrays.Clauses.fst
@@ -17,3 +17,21 @@ 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
+(** [arrays::zero_slice]: decreases clause
+ Source: 'src/arrays.rs', lines 303:0-310:1 *)
+unfold
+let zero_slice_loop_decreases (a : slice u8) (i : usize) (len : usize) : nat =
+ if i < len then len - i else 0
+
+(** [arrays::iter_mut_slice]: decreases clause
+ Source: 'src/arrays.rs', lines 312:0-318:1 *)
+unfold
+let iter_mut_slice_loop_decreases (len : usize) (i : usize) : nat =
+ if i < len then len - i else 0
+
+(** [arrays::sum_mut_slice]: decreases clause
+ Source: 'src/arrays.rs', lines 320:0-328:1 *)
+unfold
+let sum_mut_slice_loop_decreases (a : slice u32) (i : usize) (s : u32) : nat =
+ if i < slice_len u32 a then slice_len u32 a - i else 0
+
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index b0df7fc2..ac57b8fc 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -418,3 +418,58 @@ let ite : result unit =
let* _ = to_slice_mut_back s1 in
Return ()
+(** [arrays::zero_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 303:0-310:1 *)
+let rec zero_slice_loop
+ (a : slice u8) (i : usize) (len : usize) :
+ Tot (result (slice u8)) (decreases (zero_slice_loop_decreases a i len))
+ =
+ if i < len
+ then
+ let* (_, index_mut_back) = slice_index_mut_usize u8 a i in
+ let* i1 = usize_add i 1 in
+ let* a1 = index_mut_back 0 in
+ zero_slice_loop a1 i1 len
+ else Return a
+
+(** [arrays::zero_slice]:
+ Source: 'src/arrays.rs', lines 303:0-303:31 *)
+let zero_slice (a : slice u8) : result (slice u8) =
+ let len = slice_len u8 a in zero_slice_loop a 0 len
+
+(** [arrays::iter_mut_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 312:0-318:1 *)
+let rec iter_mut_slice_loop
+ (len : usize) (i : usize) :
+ Tot (result unit) (decreases (iter_mut_slice_loop_decreases len i))
+ =
+ if i < len
+ then
+ let* i1 = usize_add i 1 in let* _ = iter_mut_slice_loop len i1 in Return ()
+ else Return ()
+
+(** [arrays::iter_mut_slice]:
+ Source: 'src/arrays.rs', lines 312:0-312:35 *)
+let iter_mut_slice (a : slice u8) : result (slice u8) =
+ let len = slice_len u8 a in let* _ = iter_mut_slice_loop len 0 in Return a
+
+(** [arrays::sum_mut_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 320:0-328:1 *)
+let rec sum_mut_slice_loop
+ (a : slice u32) (i : usize) (s : u32) :
+ Tot (result u32) (decreases (sum_mut_slice_loop_decreases a i s))
+ =
+ let i1 = slice_len u32 a in
+ if i < i1
+ then
+ let* i2 = slice_index_usize u32 a i in
+ let* s1 = u32_add s i2 in
+ let* i3 = usize_add i 1 in
+ sum_mut_slice_loop a i3 s1
+ else Return s
+
+(** [arrays::sum_mut_slice]:
+ Source: 'src/arrays.rs', lines 320:0-320:42 *)
+let sum_mut_slice (a : slice u32) : result (u32 & (slice u32)) =
+ let* i = sum_mut_slice_loop a 0 0 in Return (i, a)
+