summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
authorSon HO2024-03-09 01:12:20 +0100
committerGitHub2024-03-09 01:12:20 +0100
commit14171474f9a4a45874d181cdb6567c7af7dc32cd (patch)
treef4c7dcd5b172e8922487dec83070e2c38e7b441a /tests/lean
parent169d011cbfa83d853d0148bbf6b946e6ccbe4c4c (diff)
parent46f2f1c0c4c37f089e42c82d76d79817101c5407 (diff)
Merge pull request #85 from AeneasVerif/son/fix_loops3
Fix some issues with the loops
Diffstat (limited to '')
-rw-r--r--tests/lean/Arrays.lean59
-rw-r--r--tests/lean/Loops.lean55
2 files changed, 114 insertions, 0 deletions
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index d2bb7cf2..59458393 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -473,4 +473,63 @@ def ite : Result Unit :=
let _ ← to_slice_mut_back s1
Result.ret ()
+/- [arrays::zero_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 303:0-310:1 -/
+divergent def zero_slice_loop
+ (a : Slice U8) (i : Usize) (len : Usize) : Result (Slice U8) :=
+ if i < len
+ then
+ do
+ let (_, index_mut_back) ← Slice.index_mut_usize U8 a i
+ let i1 ← i + 1#usize
+ let a1 ← index_mut_back 0#u8
+ zero_slice_loop a1 i1 len
+ else Result.ret a
+
+/- [arrays::zero_slice]:
+ Source: 'src/arrays.rs', lines 303:0-303:31 -/
+def zero_slice (a : Slice U8) : Result (Slice U8) :=
+ let len := Slice.len U8 a
+ zero_slice_loop a 0#usize len
+
+/- [arrays::iter_mut_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 312:0-318:1 -/
+divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
+ if i < len
+ then
+ do
+ let i1 ← i + 1#usize
+ let _ ← iter_mut_slice_loop len i1
+ Result.ret ()
+ else Result.ret ()
+
+/- [arrays::iter_mut_slice]:
+ Source: 'src/arrays.rs', lines 312:0-312:35 -/
+def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
+ do
+ let len := Slice.len U8 a
+ let _ ← iter_mut_slice_loop len 0#usize
+ Result.ret a
+
+/- [arrays::sum_mut_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 320:0-328:1 -/
+divergent def sum_mut_slice_loop
+ (a : Slice U32) (i : Usize) (s : U32) : Result U32 :=
+ let i1 := Slice.len U32 a
+ if i < i1
+ then
+ do
+ let i2 ← Slice.index_usize U32 a i
+ let s1 ← s + i2
+ let i3 ← i + 1#usize
+ sum_mut_slice_loop a i3 s1
+ else Result.ret s
+
+/- [arrays::sum_mut_slice]:
+ Source: 'src/arrays.rs', lines 320:0-320:42 -/
+def sum_mut_slice (a : Slice U32) : Result (U32 × (Slice U32)) :=
+ do
+ let i ← sum_mut_slice_loop a 0#usize 0#u32
+ Result.ret (i, a)
+
end arrays
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index f8e1a8cc..433ca8f0 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -557,4 +557,59 @@ def list_nth_shared_mut_loop_pair_merge
let (p, back_'a) ← list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
Result.ret (p, back_'a)
+/- [loops::ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 345:0-349:1 -/
+divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
+ if i > 0#u32
+ then
+ do
+ let i1 ← i - 1#u32
+ let _ ← ignore_input_mut_borrow_loop i1
+ Result.ret ()
+ else Result.ret ()
+
+/- [loops::ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 345:0-345:56 -/
+def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
+ do
+ let _ ← ignore_input_mut_borrow_loop i
+ Result.ret _a
+
+/- [loops::incr_ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 353:0-358:1 -/
+divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
+ if i > 0#u32
+ then
+ do
+ let i1 ← i - 1#u32
+ let _ ← incr_ignore_input_mut_borrow_loop i1
+ Result.ret ()
+ else Result.ret ()
+
+/- [loops::incr_ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 353:0-353:60 -/
+def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
+ do
+ let a1 ← a + 1#u32
+ let _ ← incr_ignore_input_mut_borrow_loop i
+ Result.ret a1
+
+/- [loops::ignore_input_shared_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 362:0-366:1 -/
+divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
+ if i > 0#u32
+ then
+ do
+ let i1 ← i - 1#u32
+ let _ ← ignore_input_shared_borrow_loop i1
+ Result.ret ()
+ else Result.ret ()
+
+/- [loops::ignore_input_shared_borrow]:
+ Source: 'src/loops.rs', lines 362:0-362:59 -/
+def ignore_input_shared_borrow (_a : U32) (i : U32) : Result U32 :=
+ do
+ let _ ← ignore_input_shared_borrow_loop i
+ Result.ret _a
+
end loops