Module `0x1::Offer`

Provides a way to transfer structs from one account to another in two transactions. Unlike many languages, Move cannot move data from one account to another with single-signer transactions. As of this writing, ordinary transactions can only have a single signer, and Move code can only store to an address (via <code>move_to</code>) if it can supply a reference to a signer for the destination address (there are special case exceptions in Genesis and DiemAccount where there can temporarily be multiple signers).

Offer solves this problem by providing an <code><a href="Offer.md#0x1_Offer">Offer</a></code> resource. To move a struct <code>T</code> from account A to B, account A first publishes an <code><a href="Offer.md#0x1_Offer">Offer</a><T></code> resource at <code><a href="Offer.md#0x1_Offer_address_of">address_of</a>(A)</code>, using the <code><a href="Offer.md#0x1_Offer_create">Offer::create</a></code> function. Then account B, in a separate transaction, can move the struct <code>T</code> from the <code><a href="Offer.md#0x1_Offer">Offer</a></code> at A's address to the desired destination. B accesses the resource using the <code>redeem</code> function, which aborts unless the <code>for</code> field is B's address (preventing other addresses from accessing the <code>T</code> that is intended only for B). A can also redeem the <code>T</code> value if B hasn't redeemed it.

Resource Offer
Constants
Function create
Function redeem
Function exists_at
Function address_of
Module Specification
- Access Control
  - Creation of Offers
  - Removal of Offers
- Helper Functions

<pre><code>use <a href="">0x1::Errors</a>; use <a href="">0x1::Signer</a>; </code></pre>

Resource `Offer`

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

<pre><code>struct <a href="Offer.md#0x1_Offer">Offer</a><Offered> has key </code></pre> <details> <summary>Fields</summary> <dl> <dt> <code>offered: Offered</code> </dt> <dd> </dd> <dt> <code>for: address</code> </dt> <dd> </dd> </dl> </details>

Constants

Address already has an offer of this type.

<pre><code>const <a href="Offer.md#0x1_Offer_EOFFER_ALREADY_CREATED">EOFFER_ALREADY_CREATED</a>: u64 = 1; </code></pre>

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

<pre><code>const <a href="Offer.md#0x1_Offer_EOFFER_DNE_FOR_ACCOUNT">EOFFER_DNE_FOR_ACCOUNT</a>: u64 = 0; </code></pre>

Address does not have an offer of this type to redeem.

<pre><code>const <a href="Offer.md#0x1_Offer_EOFFER_DOES_NOT_EXIST">EOFFER_DOES_NOT_EXIST</a>: u64 = 2; </code></pre>

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>public fun <a href="Offer.md#0x1_Offer_create">create</a><Offered: store>(account: &signer, offered: Offered, for: address) </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Offer.md#0x1_Offer_create">create</a><Offered: store>(account: &signer, offered: Offered, for: address) { assert(!exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(<a href="_address_of">Signer::address_of</a>(account)), <a href="_already_published">Errors::already_published</a>(<a href="Offer.md#0x1_Offer_EOFFER_ALREADY_CREATED">EOFFER_ALREADY_CREATED</a>)); move_to(account, <a href="Offer.md#0x1_Offer">Offer</a><Offered> { offered, for }); } </code></pre> </details> <details> <summary>Specification</summary>

Offer a struct to the account under address <code>for</code> by placing the offer under the signer's address

<pre><code>aborts_if exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(<a href="_spec_address_of">Signer::spec_address_of</a>(account)) with <a href="_ALREADY_PUBLISHED">Errors::ALREADY_PUBLISHED</a>; ensures exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(<a href="_spec_address_of">Signer::spec_address_of</a>(account)); ensures global<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(<a href="_spec_address_of">Signer::spec_address_of</a>(account)) == <a href="Offer.md#0x1_Offer">Offer</a><Offered> { offered: offered, for: for }; </code></pre> </details>

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>. Also fails if there is no <code><a href="Offer.md#0x1_Offer">Offer</a><Offered></code> published.

<pre><code>public fun <a href="Offer.md#0x1_Offer_redeem">redeem</a><Offered: store>(account: &signer, offer_address: address): Offered </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Offer.md#0x1_Offer_redeem">redeem</a><Offered: store>(account: &signer, offer_address: address): Offered acquires <a href="Offer.md#0x1_Offer">Offer</a> { assert(exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_address), <a href="_not_published">Errors::not_published</a>(<a href="Offer.md#0x1_Offer_EOFFER_DOES_NOT_EXIST">EOFFER_DOES_NOT_EXIST</a>)); let <a href="Offer.md#0x1_Offer">Offer</a><Offered> { offered, for } = move_from<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_address); let sender = <a href="_address_of">Signer::address_of</a>(account); assert(sender == for || sender == offer_address, <a href="_invalid_argument">Errors::invalid_argument</a>(<a href="Offer.md#0x1_Offer_EOFFER_DNE_FOR_ACCOUNT">EOFFER_DNE_FOR_ACCOUNT</a>)); offered } </code></pre> </details> <details> <summary>Specification</summary>

Aborts if there is no offer under <code>offer_address</code> or if the account cannot redeem the offer. Ensures that the offered struct under <code>offer_address</code> is removed.

<pre><code>aborts_if !exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_address) with <a href="_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; aborts_if !<a href="Offer.md#0x1_Offer_is_allowed_recipient">is_allowed_recipient</a><Offered>(offer_address, <a href="_spec_address_of">Signer::spec_address_of</a>(account)) with <a href="_INVALID_ARGUMENT">Errors::INVALID_ARGUMENT</a>; ensures !exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_address); ensures result == old(global<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_address).offered); </code></pre> </details>

Function `exists_at`

<pre><code>public fun <a href="Offer.md#0x1_Offer_exists_at">exists_at</a><Offered: store>(offer_address: address): bool </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Offer.md#0x1_Offer_exists_at">exists_at</a><Offered: store>(offer_address: address): bool { exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_address) } </code></pre> </details> <details> <summary>Specification</summary> <pre><code>aborts_if false; </code></pre>

Returns whether or not an <code><a href="Offer.md#0x1_Offer">Offer</a></code> resource is under the given address <code>offer_address</code>.

<pre><code>ensures result == exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_address); </code></pre> </details>

Function `address_of`

<pre><code>public fun <a href="Offer.md#0x1_Offer_address_of">address_of</a><Offered: store>(offer_address: address): address </code></pre> <details> <summary>Implementation</summary> <pre><code>public fun <a href="Offer.md#0x1_Offer_address_of">address_of</a><Offered: store>(offer_address: address): address acquires <a href="Offer.md#0x1_Offer">Offer</a> { assert(exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_address), <a href="_not_published">Errors::not_published</a>(<a href="Offer.md#0x1_Offer_EOFFER_DOES_NOT_EXIST">EOFFER_DOES_NOT_EXIST</a>)); borrow_global<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_address).for } </code></pre> </details> <details> <summary>Specification</summary>

Aborts is there is no offer resource <code><a href="Offer.md#0x1_Offer">Offer</a></code> at the <code>offer_address</code>. Returns the address of the intended recipient of the Offer under the <code>offer_address</code>.

<pre><code>aborts_if !exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_address) with <a href="_NOT_PUBLISHED">Errors::NOT_PUBLISHED</a>; ensures result == global<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_address).for; </code></pre> </details>

Module Specification

Access Control

Creation of Offers

Says no offer is created for any address. Later, it is applied to all functions except <code>create</code>

<pre><code>schema <a href="Offer.md#0x1_Offer_NoOfferCreated">NoOfferCreated</a><Offered> { ensures forall addr: address where !old(exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(addr)) : !exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(addr); } </code></pre>

Apply OnlyCreateCanCreateOffer to every function except <code>create</code>

<pre><code>apply <a href="Offer.md#0x1_Offer_NoOfferCreated">NoOfferCreated</a><Offered> to *<Offered>, * except create; </code></pre>

Removal of Offers

Says no offer is removed for any address. Applied below to everything except <code>redeem</code>

<pre><code>schema <a href="Offer.md#0x1_Offer_NoOfferRemoved">NoOfferRemoved</a><Offered> { ensures forall addr: address where old(exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(addr)) : (exists<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(addr) && global<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(addr) == old(global<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(addr))); } </code></pre>

Only <code>redeem</code> can remove an offer from the global store.

<pre><code>apply <a href="Offer.md#0x1_Offer_NoOfferRemoved">NoOfferRemoved</a><Offered> to *<Offered>, * except redeem; </code></pre>

Helper Functions

Returns true if the recipient is allowed to redeem <code><a href="Offer.md#0x1_Offer">Offer</a><Offered></code> at <code>offer_address</code> and false otherwise.

<pre><code>fun <a href="Offer.md#0x1_Offer_is_allowed_recipient">is_allowed_recipient</a><Offered>(offer_addr: address, recipient: address): bool { recipient == global<<a href="Offer.md#0x1_Offer">Offer</a><Offered>>(offer_addr).for || recipient == offer_addr } </code></pre>

Module `0x1::Offer`

Module 0x1::Offer

Resource Offer

Constants

Function create

Function redeem

Function exists_at

Function address_of

Module Specification

Access Control

Creation of Offers

Removal of Offers

Helper Functions

Module `0x1::Offer`

Resource `Offer`

Function `create`

Function `redeem`

Function `exists_at`

Function `address_of`