diff options
author | Son Ho | 2024-03-09 00:49:10 +0100 |
---|---|---|
committer | Son Ho | 2024-03-09 00:49:10 +0100 |
commit | 181749b50ef5f71e8639a5c2e97be99a6710e698 (patch) | |
tree | 53c93e14776510b59f44104e70621bb9d4c6a98b /tests/fstar | |
parent | 814f94b9e60818aac8060715e82edeffa6d5233f (diff) |
Regenerate the test files
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/arrays/Arrays.Clauses.Template.fst | 17 | ||||
-rw-r--r-- | tests/fstar/arrays/Arrays.Clauses.fst | 18 | ||||
-rw-r--r-- | tests/fstar/arrays/Arrays.Funs.fst | 55 | ||||
-rw-r--r-- | tests/fstar/misc/Loops.Clauses.Template.fst | 13 | ||||
-rw-r--r-- | tests/fstar/misc/Loops.Clauses.fst | 14 | ||||
-rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 56 |
6 files changed, 173 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) + diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst index 244761d3..c8ed16f4 100644 --- a/tests/fstar/misc/Loops.Clauses.Template.fst +++ b/tests/fstar/misc/Loops.Clauses.Template.fst @@ -136,3 +136,16 @@ let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat = admit () +(** [loops::ignore_input_mut_borrow]: decreases clause + Source: 'src/loops.rs', lines 345:0-349:1 *) +unfold let ignore_input_mut_borrow_loop_decreases (i : u32) : nat = admit () + +(** [loops::incr_ignore_input_mut_borrow]: decreases clause + Source: 'src/loops.rs', lines 353:0-358:1 *) +unfold +let incr_ignore_input_mut_borrow_loop_decreases (i : u32) : nat = admit () + +(** [loops::ignore_input_shared_borrow]: decreases clause + Source: 'src/loops.rs', lines 362:0-366:1 *) +unfold let ignore_input_shared_borrow_loop_decreases (i : u32) : nat = admit () + diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst index 13f5513d..7d3c3ae6 100644 --- a/tests/fstar/misc/Loops.Clauses.fst +++ b/tests/fstar/misc/Loops.Clauses.fst @@ -110,3 +110,17 @@ unfold let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0) (l : list_t t) (l0 : list_t t) (i : u32) : list_t t = l + +(** [loops::ignore_input_mut_borrow]: decreases clause + Source: 'src/loops.rs', lines 345:0-349:1 *) +unfold let ignore_input_mut_borrow_loop_decreases (i : u32) : nat = i + +(** [loops::incr_ignore_input_mut_borrow]: decreases clause + Source: 'src/loops.rs', lines 353:0-358:1 *) +unfold +let incr_ignore_input_mut_borrow_loop_decreases (i : u32) : nat = i + +(** [loops::ignore_input_shared_borrow]: decreases clause + Source: 'src/loops.rs', lines 362:0-366:1 *) +unfold let ignore_input_shared_borrow_loop_decreases (i : u32) : nat = i + diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 209c48cd..5f24fe7a 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -548,3 +548,59 @@ let list_nth_shared_mut_loop_pair_merge let* (p, back_'a) = list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i in Return (p, back_'a) +(** [loops::ignore_input_mut_borrow]: loop 0: + Source: 'src/loops.rs', lines 345:0-349:1 *) +let rec ignore_input_mut_borrow_loop + (i : u32) : + Tot (result unit) (decreases (ignore_input_mut_borrow_loop_decreases i)) + = + if i > 0 + then + let* i1 = u32_sub i 1 in + let* _ = ignore_input_mut_borrow_loop i1 in + Return () + else Return () + +(** [loops::ignore_input_mut_borrow]: + Source: 'src/loops.rs', lines 345:0-345:56 *) +let ignore_input_mut_borrow (_a : u32) (i : u32) : result u32 = + let* _ = ignore_input_mut_borrow_loop i in Return _a + +(** [loops::incr_ignore_input_mut_borrow]: loop 0: + Source: 'src/loops.rs', lines 353:0-358:1 *) +let rec incr_ignore_input_mut_borrow_loop + (i : u32) : + Tot (result unit) (decreases (incr_ignore_input_mut_borrow_loop_decreases i)) + = + if i > 0 + then + let* i1 = u32_sub i 1 in + let* _ = incr_ignore_input_mut_borrow_loop i1 in + Return () + else Return () + +(** [loops::incr_ignore_input_mut_borrow]: + Source: 'src/loops.rs', lines 353:0-353:60 *) +let incr_ignore_input_mut_borrow (a : u32) (i : u32) : result u32 = + let* a1 = u32_add a 1 in + let* _ = incr_ignore_input_mut_borrow_loop i in + Return a1 + +(** [loops::ignore_input_shared_borrow]: loop 0: + Source: 'src/loops.rs', lines 362:0-366:1 *) +let rec ignore_input_shared_borrow_loop + (i : u32) : + Tot (result unit) (decreases (ignore_input_shared_borrow_loop_decreases i)) + = + if i > 0 + then + let* i1 = u32_sub i 1 in + let* _ = ignore_input_shared_borrow_loop i1 in + Return () + else Return () + +(** [loops::ignore_input_shared_borrow]: + Source: 'src/loops.rs', lines 362:0-362:59 *) +let ignore_input_shared_borrow (_a : u32) (i : u32) : result u32 = + let* _ = ignore_input_shared_borrow_loop i in Return _a + |