Skip to content

Commit

Permalink
[move-prover] Specification of multitoken
Browse files Browse the repository at this point in the history 
Closes: aptos-labs#9733
  • Loading branch information
@rahxephon89 @bors-libra
rahxephon89 authored and bors-libra committed Dec 16, 2021
1 parent 14ef403 commit 0cf2397
Show file tree
Hide file tree
Showing 11 changed files with 789 additions and 13 deletions.
2 changes: 1 addition & 1 deletion ...m-framework/experimental/releases/artifacts/current/build/DiemExperimental/BuildInfo.yaml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -175,7 +175,7 @@ compiled_package_info:
? address: "00000000000000000000000000000001"
name: XUS
: DiemFramework
source_digest: C5415C7DFBC3B6BC4AB994BFE0B6B8C580089AD7D664589FF329434BA328B3AD
source_digest: 8728DA1AAB23BC8D232C36BB5800CD53D16D26533F5B895203D6C5EAE22C4EEA
build_flags:
dev_mode: false
test_mode: false
Expand Down
Binary file modified ...rimental/releases/artifacts/current/build/DiemExperimental/bytecode_modules/MultiToken.mv
View file
Binary file not shown.
Binary file modified ...l/releases/artifacts/current/build/DiemExperimental/bytecode_modules/MultiTokenBalance.mv
View file
Binary file not shown.
178 changes: 177 additions & 1 deletion ...perimental/releases/artifacts/current/build/DiemExperimental/docs/MultiToken.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
- [Function `split`](#0x1_MultiToken_split)
- [Function `initialize_multi_token`](#0x1_MultiToken_initialize_multi_token)
- [Function `create`](#0x1_MultiToken_create)
- [Module Specification](#@Module_Specification_1)


<pre><code><b>use</b> <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/Errors.md#0x1_Errors">0x1::Errors</a>;
Expand Down Expand Up @@ -451,6 +452,23 @@ Returns the supply of tokens with <code>id</code> on the chain.



</details>

<details>
<summary>Specification</summary>



<pre><code><b>let</b> addr = <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/GUID.md#0x1_GUID_id_creator_address">GUID::id_creator_address</a>(id);
<b>let</b> token_collection = <a href="MultiToken.md#0x1_MultiToken_get_tokens">get_tokens</a>&lt;TokenType&gt;(addr);
<b>let</b> min_token_idx = <a href="MultiToken.md#0x1_MultiToken_find_token_index_by_id">find_token_index_by_id</a>(token_collection,id);
<b>aborts_if</b> !<b>exists</b>&lt;<a href="MultiToken.md#0x1_MultiToken_TokenDataCollection">TokenDataCollection</a>&lt;TokenType&gt;&gt;(addr);
<b>aborts_if</b> !<a href="MultiToken.md#0x1_MultiToken_is_in_tokens">is_in_tokens</a>(token_collection, id);
<b>ensures</b> result == token_collection[min_token_idx].supply;
</code></pre>



</details>

<a name="0x1_MultiToken_extract_token"></a>
Expand Down Expand Up @@ -483,6 +501,27 @@ Extract the MultiToken data of the given token into a hot potato wrapper.



</details>

<details>
<summary>Specification</summary>



<pre><code><b>let</b> addr = <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/GUID.md#0x1_GUID_id_creator_address">GUID::id_creator_address</a>(nft.id);
<b>let</b> token_collection = <a href="MultiToken.md#0x1_MultiToken_get_tokens">get_tokens</a>&lt;TokenType&gt;(addr);
<b>let</b> id = nft.id;
<b>let</b> min_token_idx = <a href="MultiToken.md#0x1_MultiToken_find_token_index_by_id">find_token_index_by_id</a>(token_collection, id);
<b>aborts_if</b> !<b>exists</b>&lt;<a href="MultiToken.md#0x1_MultiToken_TokenDataCollection">TokenDataCollection</a>&lt;TokenType&gt;&gt;(addr);
<b>aborts_if</b> token_collection[min_token_idx].metadata == Option::spec_none();
<b>aborts_if</b> !<a href="MultiToken.md#0x1_MultiToken_is_in_tokens">is_in_tokens</a>(token_collection, id);
<b>ensures</b> result == <a href="MultiToken.md#0x1_MultiToken_TokenDataWrapper">TokenDataWrapper</a> { origin: addr, index: min_token_idx,
metadata: <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/Option.md#0x1_Option_borrow">Option::borrow</a>(token_collection[min_token_idx].metadata)};
<b>ensures</b> <a href="MultiToken.md#0x1_MultiToken_get_tokens">get_tokens</a>&lt;TokenType&gt;(addr)[min_token_idx].metadata == Option::spec_none();
</code></pre>



</details>

<a name="0x1_MultiToken_restore_token"></a>
Expand Down Expand Up @@ -513,6 +552,24 @@ Restore the token in the wrapper back into global storage under original address



</details>

<details>
<summary>Specification</summary>



<pre><code><b>let</b> addr = wrapper.origin;
<b>let</b> token_collection = <a href="MultiToken.md#0x1_MultiToken_get_tokens">get_tokens</a>&lt;TokenType&gt;(addr);
<b>let</b> item_opt = token_collection[wrapper.index].metadata;
<b>aborts_if</b> !<b>exists</b>&lt;<a href="MultiToken.md#0x1_MultiToken_TokenDataCollection">TokenDataCollection</a>&lt;TokenType&gt;&gt;(addr);
<b>aborts_if</b> len(token_collection) &lt;= wrapper.index;
<b>aborts_if</b> item_opt != Option::spec_none();
<b>ensures</b> <a href="MultiToken.md#0x1_MultiToken_get_tokens">get_tokens</a>&lt;TokenType&gt;(addr)[wrapper.index].metadata == Option::spec_some(wrapper.metadata);
</code></pre>



</details>

<a name="0x1_MultiToken_index_of_token"></a>
Expand All @@ -534,7 +591,11 @@ Finds the index of token with the given id in the gallery.
<pre><code><b>fun</b> <a href="MultiToken.md#0x1_MultiToken_index_of_token">index_of_token</a>&lt;TokenType: store&gt;(gallery: &vector&lt;<a href="MultiToken.md#0x1_MultiToken_TokenData">TokenData</a>&lt;TokenType&gt;&gt;, id: &<a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/GUID.md#0x1_GUID_ID">GUID::ID</a>): <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/Option.md#0x1_Option">Option</a>&lt;u64&gt; {
<b>let</b> i = 0;
<b>let</b> len = <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/Vector.md#0x1_Vector_length">Vector::length</a>(gallery);
<b>while</b> (i &lt; len) {
<b>while</b> ({<b>spec</b> {
<b>invariant</b> i &gt;= 0;
<b>invariant</b> i &lt;= len(gallery);
<b>invariant</b> <b>forall</b> k in 0..i: gallery[k].token_id.id != id;
};(i &lt; len)}) {
<b>if</b> (<a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/GUID.md#0x1_GUID_eq_id">GUID::eq_id</a>(&<a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/Vector.md#0x1_Vector_borrow">Vector::borrow</a>(gallery, i).token_id, id)) {
<b>return</b> <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/Option.md#0x1_Option_some">Option::some</a>(i)
};
Expand All @@ -546,6 +607,21 @@ Finds the index of token with the given id in the gallery.



</details>

<details>
<summary>Specification</summary>



<pre><code><b>let</b> min_token_idx = <a href="MultiToken.md#0x1_MultiToken_find_token_index_by_id">find_token_index_by_id</a>(gallery, id);
<b>let</b> <b>post</b> res_id = <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/Option.md#0x1_Option_borrow">Option::borrow</a>(result);
<b>ensures</b> <a href="MultiToken.md#0x1_MultiToken_is_in_tokens">is_in_tokens</a>(gallery, id) &lt;==&gt; (<a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/Option.md#0x1_Option_is_some">Option::is_some</a>(result) && res_id == min_token_idx);
<b>ensures</b> result == Option::spec_none() &lt;==&gt; !<a href="MultiToken.md#0x1_MultiToken_is_in_tokens">is_in_tokens</a>(gallery, id);
</code></pre>



</details>

<a name="0x1_MultiToken_join"></a>
Expand Down Expand Up @@ -574,6 +650,20 @@ Join two multi tokens and return a multi token with the combined value of the tw



</details>

<details>
<summary>Specification</summary>



<pre><code><b>aborts_if</b> token.id != other.id <b>with</b> <a href="MultiToken.md#0x1_MultiToken_EWRONG_TOKEN_ID">EWRONG_TOKEN_ID</a>;
<b>aborts_if</b> <a href="MultiToken.md#0x1_MultiToken_MAX_U64">MAX_U64</a> - token.<a href="MultiToken.md#0x1_MultiToken_balance">balance</a> &lt; other.balance <b>with</b> <a href="MultiToken.md#0x1_MultiToken_ETOKEN_BALANCE_OVERFLOWS">ETOKEN_BALANCE_OVERFLOWS</a>;
<b>ensures</b> token.balance == <b>old</b>(token).balance + other.balance;
</code></pre>



</details>

<a name="0x1_MultiToken_split"></a>
Expand Down Expand Up @@ -606,6 +696,21 @@ Split the token into two tokens, one with balance <code>amount</code> and the ot



</details>

<details>
<summary>Specification</summary>



<pre><code><b>aborts_if</b> token.<a href="MultiToken.md#0x1_MultiToken_balance">balance</a> &lt; amount <b>with</b> <a href="MultiToken.md#0x1_MultiToken_EAMOUNT_EXCEEDS_TOKEN_BALANCE">EAMOUNT_EXCEEDS_TOKEN_BALANCE</a>;
<b>ensures</b> result_1.balance == token.balance - amount;
<b>ensures</b> result_2.balance == amount;
<b>ensures</b> result_1.id == result_2.id;
</code></pre>



</details>

<a name="0x1_MultiToken_initialize_multi_token"></a>
Expand Down Expand Up @@ -634,6 +739,21 @@ Initialize this module, to be called in genesis.



</details>

<details>
<summary>Specification</summary>



<pre><code><b>let</b> addr = <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account);
<b>aborts_if</b> addr != <a href="MultiToken.md#0x1_MultiToken_ADMIN">ADMIN</a>;
<b>aborts_if</b> <b>exists</b>&lt;<a href="MultiToken.md#0x1_MultiToken_Admin">Admin</a>&gt;(addr);
<b>ensures</b> <b>exists</b>&lt;<a href="MultiToken.md#0x1_MultiToken_Admin">Admin</a>&gt;(addr);
</code></pre>



</details>

<a name="0x1_MultiToken_create"></a>
Expand Down Expand Up @@ -681,3 +801,59 @@ Create a<code> <a href="MultiToken.md#0x1_MultiToken_TokenData">TokenData</a>&lt


</details>

<details>
<summary>Specification</summary>



<pre><code><b>let</b> addr = <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/Signer.md#0x1_Signer_address_of">Signer::address_of</a>(account);
<b>let</b> <b>post</b> post_tokens = <a href="MultiToken.md#0x1_MultiToken_get_tokens">get_tokens</a>&lt;TokenType&gt;(addr);
<b>aborts_if</b> !<b>exists</b>&lt;<a href="MultiToken.md#0x1_MultiToken_Admin">Admin</a>&gt;(<a href="MultiToken.md#0x1_MultiToken_ADMIN">ADMIN</a>);
<b>aborts_if</b> <b>exists</b>&lt;<a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/GUID.md#0x1_GUID_Generator">GUID::Generator</a>&gt;(addr) && <b>global</b>&lt;<a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/GUID.md#0x1_GUID_Generator">GUID::Generator</a>&gt;(addr).counter + 1 &gt; <a href="MultiToken.md#0x1_MultiToken_MAX_U64">MAX_U64</a>;
<b>ensures</b> result.balance == amount;
<b>ensures</b> <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/GUID.md#0x1_GUID_id_creator_address">GUID::id_creator_address</a>(result.id) == addr;
<b>ensures</b> <b>exists</b>&lt;<a href="MultiToken.md#0x1_MultiToken_TokenDataCollection">TokenDataCollection</a>&lt;TokenType&gt;&gt;(addr);
<b>ensures</b> post_tokens[len(post_tokens) - 1] ==
<a href="MultiToken.md#0x1_MultiToken_TokenData">TokenData</a>&lt;TokenType&gt; {metadata: Option::spec_some(metadata), token_id: <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/GUID.md#0x1_GUID_GUID">GUID::GUID</a> {id: result.id}, content_uri, supply:amount};
</code></pre>



</details>

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

## Module Specification



<a name="0x1_MultiToken_get_tokens"></a>


<pre><code><b>fun</b> <a href="MultiToken.md#0x1_MultiToken_get_tokens">get_tokens</a>&lt;TokenType&gt;(addr: <b>address</b>): vector&lt;<a href="MultiToken.md#0x1_MultiToken_TokenData">TokenData</a>&lt;TokenType&gt;&gt;{
<b>global</b>&lt;<a href="MultiToken.md#0x1_MultiToken_TokenDataCollection">TokenDataCollection</a>&lt;TokenType&gt;&gt;(addr).tokens
}
</code></pre>




<a name="0x1_MultiToken_is_in_tokens"></a>


<pre><code><b>fun</b> <a href="MultiToken.md#0x1_MultiToken_is_in_tokens">is_in_tokens</a>&lt;TokenType&gt;(tokens: vector&lt;<a href="MultiToken.md#0x1_MultiToken_TokenData">TokenData</a>&lt;TokenType&gt;&gt;, token_id: <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/GUID.md#0x1_GUID_ID">GUID::ID</a>): bool {
<b>exists</b> token in tokens: token.token_id.id == token_id
}
</code></pre>




<a name="0x1_MultiToken_find_token_index_by_id"></a>


<pre><code><b>fun</b> <a href="MultiToken.md#0x1_MultiToken_find_token_index_by_id">find_token_index_by_id</a>&lt;TokenType&gt;(tokens: vector&lt;<a href="MultiToken.md#0x1_MultiToken_TokenData">TokenData</a>&lt;TokenType&gt;&gt;, id: <a href="../../../../../../../experimental/releases/artifacts/current/build/MoveStdlib/docs/GUID.md#0x1_GUID_ID">GUID::ID</a>): u64 {
<b>choose</b> <b>min</b> i in range(tokens) <b>where</b> tokens[i].token_id.id == id
}
</code></pre>
Loading

0 comments on commit 0cf2397

Please sign in to comment.