Skip to content

Commit

Permalink
[move-prover][move framework] Vector cleanup
Browse files Browse the repository at this point in the history 
Small changes to fix up the documentation for Vector.

Closes: aptos-labs#6416
  • Loading branch information
@DavidLDill @bors-libra
DavidLDill authored and bors-libra committed Oct 7, 2020
1 parent d1f8a09 commit d56418b
Show file tree
Hide file tree
Showing 2 changed files with 71 additions and 49 deletions.
84 changes: 44 additions & 40 deletions language/stdlib/modules/Vector.move
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,15 @@
address 0x1 {

/// A variable-sized container that can hold both unrestricted types and resources.
/// A variable-sized container that can hold any type. Indexing is 0-based, and
/// vectors are growable. This module has many native functions.
/// Verification of modules that use this one uses model functions that are implemented
/// directly in Boogie. The specification language has built-in functions operations such
/// as `singleton_vector`. There are some helper functions defined here for specifications in other
/// modules as well.
///
/// >Note: We did not verify most of the
/// Move functions here because many have loops, requiring loop invariants to prove, and
/// the return on investment didn't seem worth it for these simple functions.
module Vector {

/// The index into the vector is out of bounds
Expand Down Expand Up @@ -42,7 +51,7 @@ module Vector {
v
}
spec fun singleton {
// TODO(wrwg): when using opaque here, we get verification errors.
// TODO: when using opaque here, we get verification errors.
// pragma opaque;
aborts_if false;
ensures result == spec_singleton(e);
Expand All @@ -66,13 +75,24 @@ module Vector {
back_index = back_index - 1;
}
}
spec fun reverse {
pragma intrinsic = true;
}


/// Moves all of the elements of the `other` vector into the `lhs` vector.
/// Pushes all of the elements of the `other` vector into the `lhs` vector.
public fun append<Element>(lhs: &mut vector<Element>, other: vector<Element>) {
reverse(&mut other);
while (!is_empty(&other)) push_back(lhs, pop_back(&mut other));
destroy_empty(other);
}
spec fun append {
pragma intrinsic = true;
}
spec fun is_empty {
pragma intrinsic = true;
}


/// Return `true` if the vector `v` has no elements and `false` otherwise.
public fun is_empty<Element>(v: &vector<Element>): bool {
Expand All @@ -89,6 +109,9 @@ module Vector {
};
false
}
spec fun contains {
pragma intrinsic = true;
}

/// Return `(true, i)` if `e` is in the vector `v` at index `i`.
/// Otherwise, returns `(false, 0)`.
Expand All @@ -101,7 +124,9 @@ module Vector {
};
(false, 0)
}

spec fun index_of {
pragma intrinsic = true;
}

/// Remove the `i`th element of the vector `v`, shifting all subsequent elements.
/// This is O(n) and preserves ordering of elements in the vector.
Expand All @@ -115,6 +140,9 @@ module Vector {
while (i < len) swap(v, i, { i = i + 1; i });
pop_back(v)
}
spec fun remove {
pragma intrinsic = true;
}

/// Swap the `i`th element of the vector `v` with the last element and then pop the vector.
/// This is O(1), but does not preserve ordering of elements in the vector.
Expand All @@ -124,67 +152,43 @@ module Vector {
swap(v, i, last_idx);
pop_back(v)
}
spec fun swap_remove {
pragma intrinsic = true;
}

// ------------------------------------------------------------------------
// Specification
// ------------------------------------------------------------------------
// =================================================================
// Module Specification

/// # Module specifications
spec module {} // Switch to module documentation context

/// # Helper Functions
spec module {
/// Auxiliary function to check whether a vector contains an element.
/// Check whether a vector contains an element.
define spec_contains<Element>(v: vector<Element>, e: Element): bool {
exists x in v: x == e
}

/// Auxiliary function to check if `v1` is equal to the result of adding `e` at the end of `v2`
/// Check if `v1` is equal to the result of adding `e` at the end of `v2`
define eq_push_back<Element>(v1: vector<Element>, v2: vector<Element>, e: Element): bool {
len(v1) == len(v2) + 1 &&
v1[len(v1)-1] == e &&
v1[0..len(v1)-1] == v2[0..len(v2)]
}

/// Auxiliary function to check if `v` is equal to the result of concatenating `v1` and `v2`
/// Check if `v` is equal to the result of concatenating `v1` and `v2`
define eq_append<Element>(v: vector<Element>, v1: vector<Element>, v2: vector<Element>): bool {
len(v) == len(v1) + len(v2) &&
v[0..len(v1)] == v1 &&
v[len(v1)..len(v)] == v2
}

// Auxiliary function to check if `v1` is equal to the result of removing the first element of `v2`
/// Check `v1` is equal to the result of removing the first element of `v2`
define eq_pop_front<Element>(v1: vector<Element>, v2: vector<Element>): bool {
len(v1) + 1 == len(v2) &&
v1 == v2[1..len(v2)]
}
}

spec fun reverse {
pragma intrinsic = true;
}

spec fun append {
pragma intrinsic = true;
}

spec fun is_empty {
pragma intrinsic = true;
}

spec fun contains {
pragma intrinsic = true;
}

spec fun index_of {
pragma intrinsic = true;
}

spec fun remove {
pragma intrinsic = true;
}

spec fun swap_remove {
pragma intrinsic = true;
}
}

}
36 changes: 27 additions & 9 deletions language/stdlib/modules/doc/Vector.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,16 @@

# Module `0x1::Vector`

A variable-sized container that can hold both unrestricted types and resources.
A variable-sized container that can hold any type. Indexing is 0-based, and
vectors are growable. This module has many native functions.
Verification of modules that use this one uses model functions that are implemented
directly in Boogie. The specification language has built-in functions operations such
as <code>singleton_vector</code>. There are some helper functions defined here for specifications in other
modules as well.

>Note: We did not verify most of the
Move functions here because many have loops, requiring loop invariants to prove, and
the return on investment didn't seem worth it for these simple functions.


- [Constants](#@Constants_0)
Expand All @@ -24,7 +33,7 @@ A variable-sized container that can hold both unrestricted types and resources.
- [Function `remove`](#0x1_Vector_remove)
- [Function `swap_remove`](#0x1_Vector_swap_remove)
- [Module Specification](#@Module_Specification_1)
- [Module specifications](#@Module_specifications_2)
- [Helper Functions](#@Helper_Functions_2)


<pre><code></code></pre>
Expand Down Expand Up @@ -336,7 +345,7 @@ Reverses the order of the elements in the vector <code>v</code> in place.

## Function `append`

Moves all of the elements of the <code>other</code> vector into the <code>lhs</code> vector.
Pushes all of the elements of the <code>other</code> vector into the <code>lhs</code> vector.


<pre><code><b>public</b> <b>fun</b> <a href="Vector.md#0x1_Vector_append">append</a>&lt;Element&gt;(lhs: &<b>mut</b> vector&lt;Element&gt;, other: vector&lt;Element&gt;)
Expand Down Expand Up @@ -586,12 +595,13 @@ Aborts if <code>i</code> is out of bounds.
## Module Specification


<a name="@Module_specifications_2"></a>

### Module specifications
<a name="@Helper_Functions_2"></a>

### Helper Functions


Auxiliary function to check whether a vector contains an element.
Check whether a vector contains an element.


<a name="0x1_Vector_spec_contains"></a>
Expand All @@ -603,7 +613,7 @@ Auxiliary function to check whether a vector contains an element.
</code></pre>


Auxiliary function to check if <code>v1</code> is equal to the result of adding <code>e</code> at the end of <code>v2</code>
Check if <code>v1</code> is equal to the result of adding <code>e</code> at the end of <code>v2</code>


<a name="0x1_Vector_eq_push_back"></a>
Expand All @@ -617,7 +627,7 @@ Auxiliary function to check if <code>v1</code> is equal to the result of adding
</code></pre>


Auxiliary function to check if <code>v</code> is equal to the result of concatenating <code>v1</code> and <code>v2</code>
Check if <code>v</code> is equal to the result of concatenating <code>v1</code> and <code>v2</code>


<a name="0x1_Vector_eq_append"></a>
Expand All @@ -628,8 +638,16 @@ Auxiliary function to check if <code>v</code> is equal to the result of concaten
v[0..len(v1)] == v1 &&
v[len(v1)..len(v)] == v2
}
</code></pre>


Check <code>v1</code> is equal to the result of removing the first element of <code>v2</code>


<a name="0x1_Vector_eq_pop_front"></a>
<b>define</b> <a href="Vector.md#0x1_Vector_eq_pop_front">eq_pop_front</a>&lt;Element&gt;(v1: vector&lt;Element&gt;, v2: vector&lt;Element&gt;): bool {


<pre><code><b>define</b> <a href="Vector.md#0x1_Vector_eq_pop_front">eq_pop_front</a>&lt;Element&gt;(v1: vector&lt;Element&gt;, v2: vector&lt;Element&gt;): bool {
len(v1) + 1 == len(v2) &&
v1 == v2[1..len(v2)]
}
Expand Down

0 comments on commit d56418b

Please sign in to comment.