[Move][Spec] Fix specs and other miscs

aptos-move/flow/src/mcp/tools/package_spec_infer.rs

@@ -89,6 +89,7 @@ impl FlowSession {
                 })?;
                 let mut options = move_prover::cli::Options::default();
                 options.prover.verify_scope = verification_scope;
+                aptos_framework::prover::configure_aptos_custom_natives(&mut options);
                 options.inference.inference = true;
                 options.inference.inference_output = match spec_output {
                     SpecOutput::Inline => InferenceOutput::Unified,

aptos-move/flow/src/mcp/tools/package_verify.rs

@@ -24,7 +24,7 @@ struct MovePackageVerifyParams {
     /// Each entry follows the same format as `filter`: `module_name` or
     /// `module_name::function_name`. Exclusions take precedence over the filter scope.
     exclude: Option<Vec<String>>,
-    /// Solver timeout per verification condition, in seconds. Default: 10. Maximum: 10.
+    /// Solver timeout per verification condition, in seconds. Default: 10. Maximum: 60.
     timeout: Option<usize>,
 }
 
@@ -120,6 +120,7 @@ impl FlowSession {
                 options.prover.verify_scope = verification_scope;
                 options.prover.verify_exclude = verify_exclude;
                 options.backend.vc_timeout = vc_timeout;
+                aptos_framework::prover::configure_aptos_custom_natives(&mut options);
                 #[cfg(test)]
                 {
                     options.prover.stable_test_output = true;

aptos-move/flow/src/tests/list_tools/success.exp

@@ -183,7 +183,7 @@
           "nullable": true
         },
         "timeout": {
-          "description": "Solver timeout per verification condition, in seconds. Default: 10. Maximum: 10.",
+          "description": "Solver timeout per verification condition, in seconds. Default: 10. Maximum: 60.",
           "type": "integer",
           "format": "uint",
           "minimum": 0,

aptos-move/framework/aptos-framework/doc/transaction_limits.md

@@ -32,6 +32,7 @@ than or equal to the requested multiplier is chosen.
 -  [Function `update_config`](#0x1_transaction_limits_update_config)
 -  [Function `validate_enough_stake`](#0x1_transaction_limits_validate_enough_stake)
 -  [Function `validate_high_txn_limits`](#0x1_transaction_limits_validate_high_txn_limits)
+-  [Specification](#@Specification_1)
 
 
 <pre><code><b>use</b> <a href="delegation_pool.md#0x1_delegation_pool">0x1::delegation_pool</a>;
@@ -737,5 +738,14 @@ for the requested limit multipliers.
 
 </details>
 
+<a id="@Specification_1"></a>
+
+## Specification
+
+
+
+<pre><code><b>pragma</b> verify = <b>false</b>;
+</code></pre>
+
 
 [move-book]: https://aptos.dev/move/book/SUMMARY

aptos-move/framework/aptos-framework/sources/transaction_limits.spec.move

@@ -0,0 +1,5 @@
+spec aptos_framework::transaction_limits {
+    spec module {
+        pragma verify = false;
+    }
+}

aptos-move/framework/aptos-stdlib/doc/big_vector.md

@@ -6,6 +6,7 @@
 
 
 -  [Struct `BigVector`](#0x1_big_vector_BigVector)
+-  [Resource `Ghost$initial_end_index`](#0x1_big_vector_Ghost$initial_end_index)
 -  [Constants](#@Constants_0)
 -  [Function `empty`](#0x1_big_vector_empty)
 -  [Function `singleton`](#0x1_big_vector_singleton)
@@ -38,8 +39,8 @@
     -  [Function `remove`](#@Specification_1_remove)
     -  [Function `swap_remove`](#@Specification_1_swap_remove)
     -  [Function `swap`](#@Specification_1_swap)
-    -  [Function `reverse`](#@Specification_1_reverse)
     -  [Function `index_of`](#@Specification_1_index_of)
+    -  [Function `contains`](#@Specification_1_contains)
 
 
 <pre><code><b>use</b> <a href="table_with_length.md#0x1_table_with_length">0x1::table_with_length</a>;
@@ -87,6 +88,33 @@ Each bucket has a capacity of <code>bucket_size</code> elements.
 </dl>
 
 
+</details>
+
+<a id="0x1_big_vector_Ghost$initial_end_index"></a>
+
+## Resource `Ghost$initial_end_index`
+
+
+
+<pre><code><b>struct</b> Ghost$<a href="big_vector.md#0x1_big_vector_initial_end_index">initial_end_index</a> <b>has</b> <b>copy</b>, drop, store, key
+</code></pre>
+
+
+
+<details>
+<summary>Fields</summary>
+
+
+<dl>
+<dt>
+<code>v: u64</code>
+</dt>
+<dd>
+
+</dd>
+</dl>
+
+
 </details>
 
 <a id="@Constants_0"></a>
@@ -331,10 +359,20 @@ Disclaimer: This function is costly. Use it at your own discretion.
     <b>while</b> (i &lt; half_other_len) {
         self.<a href="big_vector.md#0x1_big_vector_push_back">push_back</a>(other.<a href="big_vector.md#0x1_big_vector_swap_remove">swap_remove</a>(i));
         i += 1;
+    }
+    <b>spec</b> {
+        <b>invariant</b> i &lt;= half_other_len;
+        <b>invariant</b> other.<a href="big_vector.md#0x1_big_vector_length">length</a>() == other_len - i;
+        <b>invariant</b> self.<a href="big_vector.md#0x1_big_vector_length">length</a>() == <a href="big_vector.md#0x1_big_vector_length">length</a>(<b>old</b>(self)) + i;
     };
     <b>while</b> (i &lt; other_len) {
         self.<a href="big_vector.md#0x1_big_vector_push_back">push_back</a>(other.<a href="big_vector.md#0x1_big_vector_pop_back">pop_back</a>());
         i += 1;
+    }
+    <b>spec</b> {
+        <b>invariant</b> half_other_len &lt;= i && i &lt;= other_len;
+        <b>invariant</b> other.<a href="big_vector.md#0x1_big_vector_length">length</a>() == other_len - i;
+        <b>invariant</b> self.<a href="big_vector.md#0x1_big_vector_length">length</a>() == <a href="big_vector.md#0x1_big_vector_length">length</a>(<b>old</b>(self)) + i;
     };
     other.<a href="big_vector.md#0x1_big_vector_destroy_empty">destroy_empty</a>();
 }
@@ -441,13 +479,10 @@ Disclaimer: This function is costly. Use it at your own discretion.
     <b>let</b> res = cur_bucket.<a href="big_vector.md#0x1_big_vector_remove">remove</a>(i % self.bucket_size);
     self.end_index -= 1;
     <b>move</b> cur_bucket;
-    <b>while</b> ({
-        <b>spec</b> {
-            <b>invariant</b> cur_bucket_index &lt;= num_buckets;
-            <b>invariant</b> <a href="table_with_length.md#0x1_table_with_length_spec_len">table_with_length::spec_len</a>(self.buckets) == num_buckets;
-        };
-        (cur_bucket_index &lt; num_buckets)
-    }) {
+    <b>spec</b> {
+        <b>update</b> <a href="big_vector.md#0x1_big_vector_initial_end_index">initial_end_index</a> = self.end_index;
+    };
+    <b>while</b> (cur_bucket_index &lt; num_buckets) {
         // remove one element from the start of current <a href="../../move-stdlib/doc/vector.md#0x1_vector">vector</a>
         <b>let</b> cur_bucket = self.buckets.<a href="big_vector.md#0x1_big_vector_borrow_mut">borrow_mut</a>(cur_bucket_index);
         <b>let</b> t = cur_bucket.<a href="big_vector.md#0x1_big_vector_remove">remove</a>(0);
@@ -456,6 +491,14 @@ Disclaimer: This function is costly. Use it at your own discretion.
         <b>let</b> prev_bucket = self.buckets.<a href="big_vector.md#0x1_big_vector_borrow_mut">borrow_mut</a>(cur_bucket_index - 1);
         prev_bucket.<a href="big_vector.md#0x1_big_vector_push_back">push_back</a>(t);
         cur_bucket_index += 1;
+    }
+    <b>spec</b> {
+        <b>invariant</b> 1 &lt;= cur_bucket_index && cur_bucket_index &lt;= num_buckets;
+        <b>invariant</b> self.end_index == <b>old</b>(self).end_index - 1;
+        <b>invariant</b> self.bucket_size == <b>old</b>(self).bucket_size;
+        <b>invariant</b> <a href="table_with_length.md#0x1_table_with_length_spec_len">table_with_length::spec_len</a>(self.buckets) == num_buckets;
+        <b>invariant</b> <b>forall</b> j in 0..<a href="table_with_length.md#0x1_table_with_length_spec_len">table_with_length::spec_len</a>(self.buckets):
+            <a href="table_with_length.md#0x1_table_with_length_spec_contains">table_with_length::spec_contains</a>(self.buckets, j);
     };
     <b>spec</b> {
         <b>assert</b> cur_bucket_index == num_buckets;
@@ -649,6 +692,13 @@ Disclaimer: This function is costly. Use it at your own discretion.
             <b>return</b> (<b>true</b>, bucket_index * self.bucket_size + i)
         };
         bucket_index += 1;
+    }
+    <b>spec</b> {
+        <b>invariant</b> bucket_index &lt;= num_buckets;
+        // All buckets checked so far contain no element equal <b>to</b> val.
+        <b>invariant</b> <b>forall</b> j in 0..bucket_index:
+            (<b>forall</b> k in 0..len(<a href="table_with_length.md#0x1_table_with_length_spec_get">table_with_length::spec_get</a>(self.buckets, j)):
+                <a href="table_with_length.md#0x1_table_with_length_spec_get">table_with_length::spec_get</a>(self.buckets, j)[k] != val);
     };
     (<b>false</b>, 0)
 }
@@ -773,6 +823,15 @@ Return <code><b>true</b></code> if the vector <code>v</code> has no elements and
 ## Specification
 
 
+
+<a id="0x1_big_vector_initial_end_index"></a>
+
+
+<pre><code><b>global</b> <a href="big_vector.md#0x1_big_vector_initial_end_index">initial_end_index</a>: u64;
+</code></pre>
+
+
+
 <a id="@Specification_1_BigVector"></a>
 
 ### Struct `BigVector`
@@ -815,15 +874,12 @@ Return <code><b>true</b></code> if the vector <code>v</code> has no elements and
 <b>invariant</b> <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets) == 0
     || len(<a href="table_with_length.md#0x1_table_with_length_spec_get">table_with_length::spec_get</a>(buckets, <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets) -1 )) &lt;= bucket_size;
 <b>invariant</b> <b>forall</b> i in 0..<a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets): <a href="big_vector.md#0x1_big_vector_spec_table_contains">spec_table_contains</a>(buckets, i);
-<b>invariant</b> <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets) == (end_index + bucket_size - 1) / bucket_size;
+<b>invariant</b> <b>forall</b> i: u64 {<a href="big_vector.md#0x1_big_vector_spec_table_contains">spec_table_contains</a>(buckets, i)}: <a href="big_vector.md#0x1_big_vector_spec_table_contains">spec_table_contains</a>(buckets, i) ==&gt; i &lt; <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets);
 <b>invariant</b> (<a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets) == 0 && end_index == 0)
     || (<a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets) != 0 && ((<a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets) - 1) * bucket_size) + (len(<a href="table_with_length.md#0x1_table_with_length_spec_get">table_with_length::spec_get</a>(buckets, <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets) - 1))) == end_index);
-<b>invariant</b> <b>forall</b> i: u64 <b>where</b> i &gt;= <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets):  {
+<b>invariant</b> <b>forall</b> i: u64 {<a href="big_vector.md#0x1_big_vector_spec_table_contains">spec_table_contains</a>(buckets, i)} <b>where</b> i &gt;= <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets):  {
     !<a href="big_vector.md#0x1_big_vector_spec_table_contains">spec_table_contains</a>(buckets, i)
 };
-<b>invariant</b> <b>forall</b> i: u64 <b>where</b> i &lt; <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets):  {
-    <a href="big_vector.md#0x1_big_vector_spec_table_contains">spec_table_contains</a>(buckets, i)
-};
 <b>invariant</b> <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets) == 0
     || (len(<a href="table_with_length.md#0x1_table_with_length_spec_get">table_with_length::spec_get</a>(buckets, <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(buckets) - 1)) &gt; 0);
 </code></pre>
@@ -927,7 +983,7 @@ Return <code><b>true</b></code> if the vector <code>v</code> has no elements and
 
 
 
-<pre><code><b>pragma</b> verify=<b>false</b>;
+<pre><code><b>ensures</b> self.<a href="big_vector.md#0x1_big_vector_length">length</a>() == <b>old</b>(self.<a href="big_vector.md#0x1_big_vector_length">length</a>()) + other.<a href="big_vector.md#0x1_big_vector_length">length</a>();
 </code></pre>
 
 
@@ -943,7 +999,8 @@ Return <code><b>true</b></code> if the vector <code>v</code> has no elements and
 
 
 
-<pre><code><b>let</b> num_buckets = <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(self.buckets);
+<pre><code><b>pragma</b> opaque;
+<b>let</b> num_buckets = <a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(self.buckets);
 <b>include</b> <a href="big_vector.md#0x1_big_vector_PushbackAbortsIf">PushbackAbortsIf</a>&lt;T&gt;;
 <b>ensures</b> self.<a href="big_vector.md#0x1_big_vector_length">length</a>() == <b>old</b>(self).<a href="big_vector.md#0x1_big_vector_length">length</a>() + 1;
 <b>ensures</b> self.end_index == <b>old</b>(self.end_index) + 1;
@@ -979,10 +1036,16 @@ Return <code><b>true</b></code> if the vector <code>v</code> has no elements and
 
 
 
-<pre><code><b>aborts_if</b> self.<a href="big_vector.md#0x1_big_vector_is_empty">is_empty</a>();
+<pre><code><b>pragma</b> opaque;
+<b>aborts_if</b> self.<a href="big_vector.md#0x1_big_vector_is_empty">is_empty</a>();
 <b>ensures</b> self.<a href="big_vector.md#0x1_big_vector_length">length</a>() == <b>old</b>(self).<a href="big_vector.md#0x1_big_vector_length">length</a>() - 1;
 <b>ensures</b> result == <b>old</b>(<a href="big_vector.md#0x1_big_vector_spec_at">spec_at</a>(self, self.end_index-1));
 <b>ensures</b> <b>forall</b> i in 0..self.end_index: <a href="big_vector.md#0x1_big_vector_spec_at">spec_at</a>(self, i) == <a href="big_vector.md#0x1_big_vector_spec_at">spec_at</a>(<b>old</b>(self), i);
+<b>ensures</b> <b>forall</b> b in 0..<a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(self.buckets):
+    <b>forall</b> p in 0..len(<a href="table_with_length.md#0x1_table_with_length_spec_get">table_with_length::spec_get</a>(self.buckets, b)):
+        <a href="table_with_length.md#0x1_table_with_length_spec_get">table_with_length::spec_get</a>(self.buckets, b)[p] ==
+        <a href="table_with_length.md#0x1_table_with_length_spec_get">table_with_length::spec_get</a>(<b>old</b>(self).buckets, b)[p];
+<b>ensures</b> self.bucket_size == <b>old</b>(self).bucket_size;
 </code></pre>
 
 
@@ -998,7 +1061,11 @@ Return <code><b>true</b></code> if the vector <code>v</code> has no elements and
 
 
 
-<pre><code><b>pragma</b> verify=<b>false</b>;
+<pre><code><b>pragma</b> opaque;
+<b>aborts_if</b> i &gt;= self.<a href="big_vector.md#0x1_big_vector_length">length</a>();
+<b>ensures</b> self.<a href="big_vector.md#0x1_big_vector_length">length</a>() == <b>old</b>(self.<a href="big_vector.md#0x1_big_vector_length">length</a>()) - 1;
+<b>ensures</b> self.bucket_size == <b>old</b>(self.bucket_size);
+<b>ensures</b> result == <a href="big_vector.md#0x1_big_vector_spec_at">spec_at</a>(<b>old</b>(self), i);
 </code></pre>
 
 
@@ -1014,7 +1081,7 @@ Return <code><b>true</b></code> if the vector <code>v</code> has no elements and
 
 
 
-<pre><code><b>pragma</b> verify_duration_estimate = 120;
+<pre><code><b>pragma</b> opaque;
 <b>aborts_if</b> i &gt;= self.<a href="big_vector.md#0x1_big_vector_length">length</a>();
 <b>ensures</b> self.<a href="big_vector.md#0x1_big_vector_length">length</a>() == <b>old</b>(self).<a href="big_vector.md#0x1_big_vector_length">length</a>() - 1;
 <b>ensures</b> result == <a href="big_vector.md#0x1_big_vector_spec_at">spec_at</a>(<b>old</b>(self), i);
@@ -1033,7 +1100,7 @@ Return <code><b>true</b></code> if the vector <code>v</code> has no elements and
 
 
 
-<pre><code><b>pragma</b> verify_duration_estimate = 1000;
+<pre><code><b>pragma</b> opaque;
 <b>aborts_if</b> i &gt;= self.<a href="big_vector.md#0x1_big_vector_length">length</a>() || j &gt;= self.<a href="big_vector.md#0x1_big_vector_length">length</a>();
 <b>ensures</b> self.<a href="big_vector.md#0x1_big_vector_length">length</a>() == <b>old</b>(self).<a href="big_vector.md#0x1_big_vector_length">length</a>();
 <b>ensures</b> <a href="big_vector.md#0x1_big_vector_spec_at">spec_at</a>(self, i) == <a href="big_vector.md#0x1_big_vector_spec_at">spec_at</a>(<b>old</b>(self), j);
@@ -1045,34 +1112,40 @@ Return <code><b>true</b></code> if the vector <code>v</code> has no elements and
 
 
 
-<a id="@Specification_1_reverse"></a>
+<a id="@Specification_1_index_of"></a>
 
-### Function `reverse`
+### Function `index_of`
 
 
-<pre><code><b>public</b> <b>fun</b> <a href="big_vector.md#0x1_big_vector_reverse">reverse</a>&lt;T&gt;(self: &<b>mut</b> <a href="big_vector.md#0x1_big_vector_BigVector">big_vector::BigVector</a>&lt;T&gt;)
+<pre><code><b>public</b> <b>fun</b> <a href="big_vector.md#0x1_big_vector_index_of">index_of</a>&lt;T&gt;(self: &<a href="big_vector.md#0x1_big_vector_BigVector">big_vector::BigVector</a>&lt;T&gt;, val: &T): (bool, u64)
 </code></pre>
 
 
 
 
-<pre><code><b>pragma</b> verify=<b>false</b>;
+<pre><code><b>pragma</b> opaque;
+<b>aborts_if</b> <b>false</b>;
+<b>ensures</b> result_1 ==&gt; result_2 &lt; self.<a href="big_vector.md#0x1_big_vector_length">length</a>();
+<b>ensures</b> result_1 ==&gt; <a href="big_vector.md#0x1_big_vector_spec_at">spec_at</a>(self, result_2) == val;
+<b>ensures</b> !result_1 ==&gt; (<b>forall</b> j in 0..<a href="big_vector.md#0x1_big_vector_spec_table_len">spec_table_len</a>(self.buckets):
+    <b>forall</b> k in 0..len(<a href="table_with_length.md#0x1_table_with_length_spec_get">table_with_length::spec_get</a>(self.buckets, j)):
+        <a href="table_with_length.md#0x1_table_with_length_spec_get">table_with_length::spec_get</a>(self.buckets, j)[k] != val);
 </code></pre>
 
 
 
-<a id="@Specification_1_index_of"></a>
+<a id="@Specification_1_contains"></a>
 
-### Function `index_of`
+### Function `contains`
 
 
-<pre><code><b>public</b> <b>fun</b> <a href="big_vector.md#0x1_big_vector_index_of">index_of</a>&lt;T&gt;(self: &<a href="big_vector.md#0x1_big_vector_BigVector">big_vector::BigVector</a>&lt;T&gt;, val: &T): (bool, u64)
+<pre><code><b>public</b> <b>fun</b> <a href="big_vector.md#0x1_big_vector_contains">contains</a>&lt;T&gt;(self: &<a href="big_vector.md#0x1_big_vector_BigVector">big_vector::BigVector</a>&lt;T&gt;, val: &T): bool
 </code></pre>
 
 
 
 
-<pre><code><b>pragma</b> verify=<b>false</b>;
+<pre><code><b>aborts_if</b> <b>false</b>;
 </code></pre>
 
 

aptos-move/framework/aptos-stdlib/doc/capability.md

@@ -682,6 +682,7 @@ Helper specification function to check whether a delegated capability exists at
 
 
 <pre><code><b>let</b> addr = <a href="../../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<b>to</b>);
+<b>aborts_if</b> !<a href="capability.md#0x1_capability_spec_has_delegate_cap">spec_has_delegate_cap</a>&lt;Feature&gt;(addr) && !<a href="capability.md#0x1_capability_spec_has_cap">spec_has_cap</a>&lt;Feature&gt;(self.root);
 <b>ensures</b> <a href="capability.md#0x1_capability_spec_has_delegate_cap">spec_has_delegate_cap</a>&lt;Feature&gt;(addr);
 <b>ensures</b> !<b>old</b>(<a href="capability.md#0x1_capability_spec_has_delegate_cap">spec_has_delegate_cap</a>&lt;Feature&gt;(addr)) ==&gt; <b>global</b>&lt;<a href="capability.md#0x1_capability_CapDelegateState">CapDelegateState</a>&lt;Feature&gt;&gt;(addr).root == self.root;
 <b>ensures</b> !<b>old</b>(<a href="capability.md#0x1_capability_spec_has_delegate_cap">spec_has_delegate_cap</a>&lt;Feature&gt;(addr)) ==&gt; <a href="../../move-stdlib/doc/vector.md#0x1_vector_spec_contains">vector::spec_contains</a>(<a href="capability.md#0x1_capability_spec_delegates">spec_delegates</a>&lt;Feature&gt;(self.root), addr);
@@ -700,7 +701,8 @@ Helper specification function to check whether a delegated capability exists at
 
 
 
-<pre><code><b>ensures</b> !<a href="capability.md#0x1_capability_spec_has_delegate_cap">spec_has_delegate_cap</a>&lt;Feature&gt;(from);
+<pre><code><b>aborts_if</b> <a href="capability.md#0x1_capability_spec_has_delegate_cap">spec_has_delegate_cap</a>&lt;Feature&gt;(from) && !<a href="capability.md#0x1_capability_spec_has_cap">spec_has_cap</a>&lt;Feature&gt;(self.root);
+<b>ensures</b> !<a href="capability.md#0x1_capability_spec_has_delegate_cap">spec_has_delegate_cap</a>&lt;Feature&gt;(from);
 </code></pre>
 
 

aptos-move/framework/aptos-stdlib/doc/comparator.md

@@ -328,7 +328,8 @@ Provides a framework for comparing two elements
 
 
 
-<pre><code><b>let</b> left_bytes = <a href="../../move-stdlib/doc/bcs.md#0x1_bcs_to_bytes">bcs::to_bytes</a>(left);
+<pre><code><b>aborts_if</b> <b>false</b>;
+<b>let</b> left_bytes = <a href="../../move-stdlib/doc/bcs.md#0x1_bcs_to_bytes">bcs::to_bytes</a>(left);
 <b>let</b> right_bytes = <a href="../../move-stdlib/doc/bcs.md#0x1_bcs_to_bytes">bcs::to_bytes</a>(right);
 <b>ensures</b> result == <a href="comparator.md#0x1_comparator_spec_compare_u8_vector">spec_compare_u8_vector</a>(left_bytes, right_bytes);
 </code></pre>