diff options
| author | Son Ho | 2023-11-09 18:37:07 +0100 |
|---|---|---|
| committer | Son Ho | 2023-11-09 18:37:07 +0100 |
| commit | 00705bba68fed61d3b0bcde2c5fe0ecc83880870 (patch) | |
| tree | 8531640066e9983264ba88f552571836922a6809 /tests/fstar/betree | |
| parent | 49ffc966cfdbd71f8c83a3c72ab81e1bb101f420 (diff) | |
Update the failing proofs
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/betree/Primitives.fst | 18 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/Primitives.fst | 18 |
2 files changed, 34 insertions, 2 deletions
diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst index 71d75c11..3297803c 100644 --- a/tests/fstar/betree/Primitives.fst +++ b/tests/fstar/betree/Primitives.fst @@ -427,7 +427,7 @@ let alloc_vec_Vec_new (a : Type0) : alloc_vec_Vec a = assert_norm(length #a [] let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v // Helper -let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result a = +let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a = if i < length v then Return (index v i) else Fail Failure // Helper let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) = @@ -704,6 +704,22 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0) (*** Theorems *) +let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : + Lemma ( + alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i == + alloc_vec_Vec_index_usize v i) + [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)] + = + admit() + +let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : + Lemma ( + alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i == + alloc_vec_Vec_index_usize v i) + [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)] + = + admit() + let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : Lemma ( alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x == diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst index 71d75c11..3297803c 100644 --- a/tests/fstar/betree_back_stateful/Primitives.fst +++ b/tests/fstar/betree_back_stateful/Primitives.fst @@ -427,7 +427,7 @@ let alloc_vec_Vec_new (a : Type0) : alloc_vec_Vec a = assert_norm(length #a [] let alloc_vec_Vec_len (a : Type0) (v : alloc_vec_Vec a) : usize = length v // Helper -let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result a = +let alloc_vec_Vec_index_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : result a = if i < length v then Return (index v i) else Fail Failure // Helper let alloc_vec_Vec_update_usize (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : result (alloc_vec_Vec a) = @@ -704,6 +704,22 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0) (*** Theorems *) +let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : + Lemma ( + alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i == + alloc_vec_Vec_index_usize v i) + [SMTPat (alloc_vec_Vec_index a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)] + = + admit() + +let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) : + Lemma ( + alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i == + alloc_vec_Vec_index_usize v i) + [SMTPat (alloc_vec_Vec_index_mut a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i)] + = + admit() + let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) : Lemma ( alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x == |