Skip to content

Commit

Permalink
[compiler-v2 framework] framework testsuite: fixed treasury module …
Browse files Browse the repository at this point in the history
…test
  • Loading branch information
welbon committed Nov 24, 2024
1 parent 845334e commit 33338e9
Show file tree
Hide file tree
Showing 12 changed files with 487 additions and 88 deletions.
1 change: 1 addition & 0 deletions vm/framework/starcoin-framework/doc/overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,7 @@ This is the reference documentation of the Starcoin framework.
- [`0x1::stc_block`](stc_block.md#0x1_stc_block)
- [`0x1::stc_genesis`](stc_genesis.md#0x1_stc_genesis)
- [`0x1::stc_language_version`](stc_language_version.md#0x1_stc_language_version)
- [`0x1::stc_offer`](stc_offer.md#0x1_stc_offer)
- [`0x1::stc_transaction_fee`](stc_transaction_fee.md#0x1_stc_transaction_fee)
- [`0x1::stc_transaction_package_validation`](stc_transaction_package_validation.md#0x1_stc_transaction_package_validation)
- [`0x1::stc_transaction_timeout`](stc_transaction_timeout.md#0x1_stc_transaction_timeout)
Expand Down
289 changes: 289 additions & 0 deletions vm/framework/starcoin-framework/doc/stc_offer.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,289 @@

<a id="0x1_stc_offer"></a>

# Module `0x1::stc_offer`



- [Resource `Offer`](#0x1_stc_offer_Offer)
- [Constants](#@Constants_0)
- [Function `create`](#0x1_stc_offer_create)
- [Function `redeem`](#0x1_stc_offer_redeem)
- [Function `exists_at`](#0x1_stc_offer_exists_at)
- [Function `address_of`](#0x1_stc_offer_address_of)
- [Specification](#@Specification_1)
- [Function `create`](#@Specification_1_create)
- [Function `redeem`](#@Specification_1_redeem)
- [Function `exists_at`](#@Specification_1_exists_at)
- [Function `address_of`](#@Specification_1_address_of)


<pre><code><b>use</b> <a href="../../move-stdlib/doc/error.md#0x1_error">0x1::error</a>;
<b>use</b> <a href="../../move-stdlib/doc/signer.md#0x1_signer">0x1::signer</a>;
<b>use</b> <a href="timestamp.md#0x1_timestamp">0x1::timestamp</a>;
</code></pre>



<a id="0x1_stc_offer_Offer"></a>

## Resource `Offer`

A wrapper around value <code>offered</code> that can be claimed by the address stored in <code>for</code> when after lock time.


<pre><code><b>struct</b> <a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>&lt;Offered&gt; <b>has</b> key
</code></pre>



<details>
<summary>Fields</summary>


<dl>
<dt>
<code>offered: Offered</code>
</dt>
<dd>

</dd>
<dt>
<code>for_address: <b>address</b></code>
</dt>
<dd>

</dd>
<dt>
<code>time_lock: u64</code>
</dt>
<dd>

</dd>
</dl>


</details>

<a id="@Constants_0"></a>

## Constants


<a id="0x1_stc_offer_EOFFER_DNE_FOR_ACCOUNT"></a>

An offer of the specified type for the account does not match


<pre><code><b>const</b> <a href="stc_offer.md#0x1_stc_offer_EOFFER_DNE_FOR_ACCOUNT">EOFFER_DNE_FOR_ACCOUNT</a>: u64 = 101;
</code></pre>



<a id="0x1_stc_offer_EOFFER_NOT_UNLOCKED"></a>

Offer is not unlocked yet.


<pre><code><b>const</b> <a href="stc_offer.md#0x1_stc_offer_EOFFER_NOT_UNLOCKED">EOFFER_NOT_UNLOCKED</a>: u64 = 102;
</code></pre>



<a id="0x1_stc_offer_create"></a>

## Function `create`

Publish a value of type <code>Offered</code> under the sender's account. The value can be claimed by
either the <code>for</code> address or the transaction sender.


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_create">create</a>&lt;Offered: store&gt;(<a href="account.md#0x1_account">account</a>: &<a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>, offered: Offered, for_address: <b>address</b>, lock_period: u64)
</code></pre>



<details>
<summary>Implementation</summary>


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_create">create</a>&lt;Offered: store&gt;(<a href="account.md#0x1_account">account</a>: &<a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>, offered: Offered, for_address: <b>address</b>, lock_period: u64) {
<b>let</b> time_lock = <a href="timestamp.md#0x1_timestamp_now_seconds">timestamp::now_seconds</a>() + lock_period;
//TODO should support multi <a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>?
<b>move_to</b>(<a href="account.md#0x1_account">account</a>, <a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>&lt;Offered&gt; {
offered,
for_address,
time_lock
});
}
</code></pre>



</details>

<a id="0x1_stc_offer_redeem"></a>

## Function `redeem`

Claim the value of type <code>Offered</code> published at <code>offer_address</code>.
Only succeeds if the sender is the intended recipient stored in <code>for</code> or the original
publisher <code>offer_address</code>, and now >= time_lock
Also fails if no such value exists.


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_redeem">redeem</a>&lt;Offered: store&gt;(<a href="account.md#0x1_account">account</a>: &<a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>, offer_address: <b>address</b>): Offered
</code></pre>



<details>
<summary>Implementation</summary>


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_redeem">redeem</a>&lt;Offered: store&gt;(<a href="account.md#0x1_account">account</a>: &<a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>, offer_address: <b>address</b>): Offered <b>acquires</b> <a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a> {
<b>let</b> <a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>&lt;Offered&gt; { offered, for_address, time_lock } = <b>move_from</b>&lt;<a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>&lt;Offered&gt;&gt;(offer_address);
<b>let</b> sender = <a href="../../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="account.md#0x1_account">account</a>);
<b>let</b> now = <a href="timestamp.md#0x1_timestamp_now_seconds">timestamp::now_seconds</a>();
<b>assert</b>!(sender == for_address || sender == offer_address, <a href="../../move-stdlib/doc/error.md#0x1_error_invalid_argument">error::invalid_argument</a>(<a href="stc_offer.md#0x1_stc_offer_EOFFER_DNE_FOR_ACCOUNT">EOFFER_DNE_FOR_ACCOUNT</a>));
<b>assert</b>!(now &gt;= time_lock, <a href="../../move-stdlib/doc/error.md#0x1_error_invalid_state">error::invalid_state</a>(<a href="stc_offer.md#0x1_stc_offer_EOFFER_NOT_UNLOCKED">EOFFER_NOT_UNLOCKED</a>));
offered
}
</code></pre>



</details>

<a id="0x1_stc_offer_exists_at"></a>

## Function `exists_at`

Returns true if an offer of type <code>Offered</code> exists at <code>offer_address</code>.


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_exists_at">exists_at</a>&lt;Offered: store&gt;(offer_address: <b>address</b>): bool
</code></pre>



<details>
<summary>Implementation</summary>


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_exists_at">exists_at</a>&lt;Offered: store&gt;(offer_address: <b>address</b>): bool {
<b>exists</b>&lt;<a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>&lt;Offered&gt;&gt;(offer_address)
}
</code></pre>



</details>

<a id="0x1_stc_offer_address_of"></a>

## Function `address_of`

Returns the address of the <code>Offered</code> type stored at <code>offer_address</code>.
Fails if no such <code><a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a></code> exists.


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_address_of">address_of</a>&lt;Offered: store&gt;(offer_address: <b>address</b>): <b>address</b>
</code></pre>



<details>
<summary>Implementation</summary>


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_address_of">address_of</a>&lt;Offered: store&gt;(offer_address: <b>address</b>): <b>address</b> <b>acquires</b> <a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a> {
<b>borrow_global</b>&lt;<a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>&lt;Offered&gt;&gt;(offer_address).for_address
}
</code></pre>



</details>

<a id="@Specification_1"></a>

## Specification



<pre><code><b>pragma</b> verify = <b>true</b>;
<b>pragma</b> aborts_if_is_strict = <b>true</b>;
</code></pre>



<a id="@Specification_1_create"></a>

### Function `create`


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_create">create</a>&lt;Offered: store&gt;(<a href="account.md#0x1_account">account</a>: &<a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>, offered: Offered, for_address: <b>address</b>, lock_period: u64)
</code></pre>




<pre><code><b>aborts_if</b> <a href="timestamp.md#0x1_timestamp_now_seconds">timestamp::now_seconds</a>() + lock_period &gt; max_u64();
<b>aborts_if</b> <b>exists</b>&lt;<a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>&lt;Offered&gt;&gt;(<a href="../../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="account.md#0x1_account">account</a>));
</code></pre>



<a id="@Specification_1_redeem"></a>

### Function `redeem`


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_redeem">redeem</a>&lt;Offered: store&gt;(<a href="account.md#0x1_account">account</a>: &<a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>, offer_address: <b>address</b>): Offered
</code></pre>




<pre><code><b>aborts_if</b> !<b>exists</b>&lt;<a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>&lt;Offered&gt;&gt;(offer_address);
<b>aborts_if</b>
<a href="../../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="account.md#0x1_account">account</a>) != <b>global</b>&lt;<a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>&lt;Offered&gt;&gt;(offer_address).for_address
&& <a href="../../move-stdlib/doc/signer.md#0x1_signer_address_of">signer::address_of</a>(<a href="account.md#0x1_account">account</a>) != offer_address;
<b>aborts_if</b> <a href="timestamp.md#0x1_timestamp_now_seconds">timestamp::now_seconds</a>() &lt; <b>global</b>&lt;<a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>&lt;Offered&gt;&gt;(offer_address).time_lock;
</code></pre>



<a id="@Specification_1_exists_at"></a>

### Function `exists_at`


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_exists_at">exists_at</a>&lt;Offered: store&gt;(offer_address: <b>address</b>): bool
</code></pre>




<pre><code><b>aborts_if</b> <b>false</b>;
</code></pre>



<a id="@Specification_1_address_of"></a>

### Function `address_of`


<pre><code><b>public</b> <b>fun</b> <a href="stc_offer.md#0x1_stc_offer_address_of">address_of</a>&lt;Offered: store&gt;(offer_address: <b>address</b>): <b>address</b>
</code></pre>




<pre><code><b>aborts_if</b> !<b>exists</b>&lt;<a href="stc_offer.md#0x1_stc_offer_Offer">Offer</a>&lt;Offered&gt;&gt;(offer_address);
</code></pre>


[move-book]: https://starcoin.dev/move/book/SUMMARY
14 changes: 7 additions & 7 deletions vm/framework/starcoin-framework/doc/timestamp.md
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,7 @@ Marks that time has started. This can only be called from genesis and with the s
Updates the wall clock time by consensus. Requires VM privilege and will be invoked during block prologue.


<pre><code><b>public</b> <b>fun</b> <a href="timestamp.md#0x1_timestamp_update_global_time">update_global_time</a>(<a href="account.md#0x1_account">account</a>: &<a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>, proposer: <b>address</b>, <a href="timestamp.md#0x1_timestamp">timestamp</a>: u64)
<pre><code><b>public</b> <b>fun</b> <a href="timestamp.md#0x1_timestamp_update_global_time">update_global_time</a>(<a href="account.md#0x1_account">account</a>: &<a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>, _proposer: <b>address</b>, <a href="timestamp.md#0x1_timestamp">timestamp</a>: u64)
</code></pre>


Expand All @@ -148,7 +148,7 @@ Updates the wall clock time by consensus. Requires VM privilege and will be invo

<pre><code><b>public</b> <b>fun</b> <a href="timestamp.md#0x1_timestamp_update_global_time">update_global_time</a>(
<a href="account.md#0x1_account">account</a>: &<a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>,
proposer: <b>address</b>,
_proposer: <b>address</b>,
<a href="timestamp.md#0x1_timestamp">timestamp</a>: u64
) <b>acquires</b> <a href="timestamp.md#0x1_timestamp_CurrentTimeMicroseconds">CurrentTimeMicroseconds</a> {
<a href="../../starcoin-stdlib/doc/debug.md#0x1_debug_print">debug::print</a>(&std::string::utf8(b"<a href="timestamp.md#0x1_timestamp_update_global_time">timestamp::update_global_time</a> | Entered"));
Expand Down Expand Up @@ -324,15 +324,15 @@ Gets the current time in seconds.
### Function `update_global_time`


<pre><code><b>public</b> <b>fun</b> <a href="timestamp.md#0x1_timestamp_update_global_time">update_global_time</a>(<a href="account.md#0x1_account">account</a>: &<a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>, proposer: <b>address</b>, <a href="timestamp.md#0x1_timestamp">timestamp</a>: u64)
<pre><code><b>public</b> <b>fun</b> <a href="timestamp.md#0x1_timestamp_update_global_time">update_global_time</a>(<a href="account.md#0x1_account">account</a>: &<a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>, _proposer: <b>address</b>, <a href="timestamp.md#0x1_timestamp">timestamp</a>: u64)
</code></pre>




<pre><code><b>requires</b> <a href="chain_status.md#0x1_chain_status_is_operating">chain_status::is_operating</a>();
<b>include</b> <a href="timestamp.md#0x1_timestamp_UpdateGlobalTimeAbortsIf">UpdateGlobalTimeAbortsIf</a>;
<b>ensures</b> (proposer != @vm_reserved) ==&gt; (<a href="timestamp.md#0x1_timestamp_spec_now_microseconds">spec_now_microseconds</a>() == <a href="timestamp.md#0x1_timestamp">timestamp</a>);
<b>ensures</b> (_proposer != @vm_reserved) ==&gt; (<a href="timestamp.md#0x1_timestamp_spec_now_microseconds">spec_now_microseconds</a>() == <a href="timestamp.md#0x1_timestamp">timestamp</a>);
</code></pre>


Expand All @@ -343,13 +343,13 @@ Gets the current time in seconds.

<pre><code><b>schema</b> <a href="timestamp.md#0x1_timestamp_UpdateGlobalTimeAbortsIf">UpdateGlobalTimeAbortsIf</a> {
<a href="account.md#0x1_account">account</a>: <a href="../../move-stdlib/doc/signer.md#0x1_signer">signer</a>;
proposer: <b>address</b>;
_proposer: <b>address</b>;
<a href="timestamp.md#0x1_timestamp">timestamp</a>: u64;
// This enforces <a id="high-level-req-3" href="#high-level-req">high-level requirement 3</a>:
<b>aborts_if</b> !<a href="system_addresses.md#0x1_system_addresses_is_vm">system_addresses::is_vm</a>(<a href="account.md#0x1_account">account</a>);
// This enforces <a id="high-level-req-4" href="#high-level-req">high-level requirement 4</a>:
<b>aborts_if</b> (proposer == @vm_reserved) && (<a href="timestamp.md#0x1_timestamp_spec_now_microseconds">spec_now_microseconds</a>() != <a href="timestamp.md#0x1_timestamp">timestamp</a>);
<b>aborts_if</b> (proposer != @vm_reserved) && (<a href="timestamp.md#0x1_timestamp_spec_now_microseconds">spec_now_microseconds</a>() &gt;= <a href="timestamp.md#0x1_timestamp">timestamp</a>);
<b>aborts_if</b> (_proposer == @vm_reserved) && (<a href="timestamp.md#0x1_timestamp_spec_now_microseconds">spec_now_microseconds</a>() != <a href="timestamp.md#0x1_timestamp">timestamp</a>);
<b>aborts_if</b> (_proposer != @vm_reserved) && (<a href="timestamp.md#0x1_timestamp_spec_now_microseconds">spec_now_microseconds</a>() &gt;= <a href="timestamp.md#0x1_timestamp">timestamp</a>);
}
</code></pre>

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,24 +2,24 @@ processed 9 tasks

task 2 'run'. lines 5-20:
{
"gas_used": 37319,
"gas_used": 48026,
"status": "Executed"
}

task 4 'run'. lines 24-40:
{
"gas_used": 141885,
"gas_used": 351963,
"status": "Executed"
}

task 6 'run'. lines 45-61:
task 6 'run'. lines 45-62:
{
"gas_used": 141885,
"gas_used": 351963,
"status": "Executed"
}

task 8 'run'. lines 66-83:
task 8 'run'. lines 67-89:
{
"gas_used": 138625,
"gas_used": 354815,
"status": "Executed"
}
Loading

0 comments on commit 33338e9

Please sign in to comment.