summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/arrays/Arrays.v69
-rw-r--r--tests/coq/misc/Loops.v64
-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
-rw-r--r--tests/fstar/misc/Loops.Clauses.Template.fst13
-rw-r--r--tests/fstar/misc/Loops.Clauses.fst14
-rw-r--r--tests/fstar/misc/Loops.Funs.fst56
-rw-r--r--tests/lean/Arrays.lean59
-rw-r--r--tests/lean/Loops.lean55
10 files changed, 420 insertions, 0 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 3a6fb02f..79be3678 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -516,4 +516,73 @@ Definition ite : result unit :=
Return tt
.
+(** [arrays::zero_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 303:0-310:1 *)
+Fixpoint zero_slice_loop
+ (n : nat) (a : slice u8) (i : usize) (len : usize) : result (slice u8) :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s< len
+ then (
+ p <- slice_index_mut_usize u8 a i;
+ let (_, index_mut_back) := p in
+ i1 <- usize_add i 1%usize;
+ a1 <- index_mut_back 0%u8;
+ zero_slice_loop n1 a1 i1 len)
+ else Return a
+ end
+.
+
+(** [arrays::zero_slice]:
+ Source: 'src/arrays.rs', lines 303:0-303:31 *)
+Definition zero_slice (n : nat) (a : slice u8) : result (slice u8) :=
+ let len := slice_len u8 a in zero_slice_loop n a 0%usize len
+.
+
+(** [arrays::iter_mut_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 312:0-318:1 *)
+Fixpoint iter_mut_slice_loop
+ (n : nat) (len : usize) (i : usize) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s< len
+ then (
+ i1 <- usize_add i 1%usize; _ <- iter_mut_slice_loop n1 len i1; Return tt)
+ else Return tt
+ end
+.
+
+(** [arrays::iter_mut_slice]:
+ Source: 'src/arrays.rs', lines 312:0-312:35 *)
+Definition iter_mut_slice (n : nat) (a : slice u8) : result (slice u8) :=
+ let len := slice_len u8 a in _ <- iter_mut_slice_loop n len 0%usize; Return a
+.
+
+(** [arrays::sum_mut_slice]: loop 0:
+ Source: 'src/arrays.rs', lines 320:0-328:1 *)
+Fixpoint sum_mut_slice_loop
+ (n : nat) (a : slice u32) (i : usize) (s : u32) : result u32 :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ let i1 := slice_len u32 a in
+ if i s< i1
+ then (
+ i2 <- slice_index_usize u32 a i;
+ s1 <- u32_add s i2;
+ i3 <- usize_add i 1%usize;
+ sum_mut_slice_loop n1 a i3 s1)
+ else Return s
+ end
+.
+
+(** [arrays::sum_mut_slice]:
+ Source: 'src/arrays.rs', lines 320:0-320:42 *)
+Definition sum_mut_slice
+ (n : nat) (a : slice u32) : result (u32 * (slice u32)) :=
+ i <- sum_mut_slice_loop n a 0%usize 0%u32; Return (i, a)
+.
+
End Arrays.
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 8260db02..e235b60d 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -688,4 +688,68 @@ Definition list_nth_shared_mut_loop_pair_merge
Return (p1, back_'a)
.
+(** [loops::ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 345:0-349:1 *)
+Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 345:0-345:56 *)
+Definition ignore_input_mut_borrow
+ (n : nat) (_a : u32) (i : u32) : result u32 :=
+ _ <- ignore_input_mut_borrow_loop n i; Return _a
+.
+
+(** [loops::incr_ignore_input_mut_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 353:0-358:1 *)
+Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32;
+ _ <- incr_ignore_input_mut_borrow_loop n1 i1;
+ Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::incr_ignore_input_mut_borrow]:
+ Source: 'src/loops.rs', lines 353:0-353:60 *)
+Definition incr_ignore_input_mut_borrow
+ (n : nat) (a : u32) (i : u32) : result u32 :=
+ a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Return a1
+.
+
+(** [loops::ignore_input_shared_borrow]: loop 0:
+ Source: 'src/loops.rs', lines 362:0-366:1 *)
+Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n1 =>
+ if i s> 0%u32
+ then (
+ i1 <- u32_sub i 1%u32;
+ _ <- ignore_input_shared_borrow_loop n1 i1;
+ Return tt)
+ else Return tt
+ end
+.
+
+(** [loops::ignore_input_shared_borrow]:
+ Source: 'src/loops.rs', lines 362:0-362:59 *)
+Definition ignore_input_shared_borrow
+ (n : nat) (_a : u32) (i : u32) : result u32 :=
+ _ <- ignore_input_shared_borrow_loop n i; Return _a
+.
+
End Loops.
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
+
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 07:38:40 +0000