# 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 move_to) 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 Offer resource. To move a struct T from account A to B, account A first publishes an Offer<T> resource at address_of(A), using the offer::create function. Then account B, in a separate transaction, can move the struct T from the Offer at A's address to the desired destination. B accesses the resource using the redeem function, which aborts unless the for field is B's address (preventing other addresses from accessing the T that is intended only for B). A can also redeem the T value if B hasn't redeemed it. - [Resource `Offer`](#0x1_offer_Offer) - [Constants](#@Constants_0) - [Function `create`](#0x1_offer_create) - [Function `redeem`](#0x1_offer_redeem) - [Function `exists_at`](#0x1_offer_exists_at) - [Function `address_of`](#0x1_offer_address_of) - [Module Specification](#@Module_Specification_1) - [Access Control](#@Access_Control_2) - [Creation of Offers](#@Creation_of_Offers_3) - [Removal of Offers](#@Removal_of_Offers_4) - [Helper Functions](#@Helper_Functions_5)

use 0x1::error;
use 0x1::signer;

## Resource `Offer` A wrapper around value offered that can be claimed by the address stored in for.

struct Offer<Offered> has key

Fields

offered: Offered
for: address

## Constants Address already has an offer of this type.

const EOFFER_ALREADY_CREATED: u64 = 1;

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

const EOFFER_DNE_FOR_ACCOUNT: u64 = 0;

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

const EOFFER_DOES_NOT_EXIST: u64 = 2;

## Function `create` Publish a value of type Offered under the sender's account. The value can be claimed by either the for address or the transaction sender.

public fun create<Offered: store>(account: &signer, offered: Offered, for: address)

Implementation

public fun create<Offered: store>(account: &signer, offered: Offered, for: address) {
  assert!(!exists<Offer<Offered>>(signer::address_of(account)), error::already_exists(EOFFER_ALREADY_CREATED));
  move_to(account, Offer<Offered> { offered, for });
}

Specification

Offer a struct to the account under address for by placing the offer under the signer's address

aborts_if exists<Offer<Offered>>(signer::address_of(account));
ensures exists<Offer<Offered>>(signer::address_of(account));
ensures global<Offer<Offered>>(signer::address_of(account)) == Offer<Offered> { offered: offered, for: for };

## Function `redeem` Claim the value of type Offered published at offer_address. Only succeeds if the sender is the intended recipient stored in for or the original publisher offer_address. Also fails if there is no Offer<Offered> published.

public fun redeem<Offered: store>(account: &signer, offer_address: address): Offered

Implementation

public fun redeem<Offered: store>(account: &signer, offer_address: address): Offered acquires Offer {
  assert!(exists<Offer<Offered>>(offer_address), error::not_found(EOFFER_DOES_NOT_EXIST));
  let Offer<Offered> { offered, for } = move_from<Offer<Offered>>(offer_address);
  let sender = signer::address_of(account);
  assert!(sender == for || sender == offer_address, error::invalid_argument(EOFFER_DNE_FOR_ACCOUNT));
  offered
}

Specification

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

aborts_if !exists<Offer<Offered>>(offer_address);
aborts_if !is_allowed_recipient<Offered>(offer_address, signer::address_of(account));
ensures !exists<Offer<Offered>>(offer_address);
ensures result == old(global<Offer<Offered>>(offer_address).offered);

## Function `exists_at`

public fun exists_at<Offered: store>(offer_address: address): bool

Implementation

public fun exists_at<Offered: store>(offer_address: address): bool {
  exists<Offer<Offered>>(offer_address)
}

Specification

aborts_if false;

Returns whether or not an Offer resource is under the given address offer_address.

ensures result == exists<Offer<Offered>>(offer_address);

## Function `address_of`

public fun address_of<Offered: store>(offer_address: address): address

Implementation

public fun address_of<Offered: store>(offer_address: address): address acquires Offer {
  assert!(exists<Offer<Offered>>(offer_address), error::not_found(EOFFER_DOES_NOT_EXIST));
  borrow_global<Offer<Offered>>(offer_address).for
}

Specification

Aborts is there is no offer resource Offer at the offer_address. Returns the address of the intended recipient of the Offer under the offer_address.

aborts_if !exists<Offer<Offered>>(offer_address);
ensures result == global<Offer<Offered>>(offer_address).for;

## Module Specification ### Access Control #### Creation of Offers Says no offer is created for any address. Later, it is applied to all functions except create

schema NoOfferCreated<Offered> {
    ensures forall addr: address where !old(exists<Offer<Offered>>(addr)) : !exists<Offer<Offered>>(addr);
}

Apply OnlyCreateCanCreateOffer to every function except create

apply NoOfferCreated<Offered> to *<Offered>, * except create;

#### Removal of Offers Says no offer is removed for any address. Applied below to everything except redeem

schema NoOfferRemoved<Offered> {
    ensures forall addr: address where old(exists<Offer<Offered>>(addr)) :
              (exists<Offer<Offered>>(addr) && global<Offer<Offered>>(addr) == old(global<Offer<Offered>>(addr)));
}

Only redeem can remove an offer from the global store.

apply NoOfferRemoved<Offered> to *<Offered>, * except redeem;

### Helper Functions Returns true if the recipient is allowed to redeem Offer<Offered> at offer_address and false otherwise.

fun is_allowed_recipient<Offered>(offer_addr: address, recipient: address): bool {
  recipient == global<Offer<Offered>>(offer_addr).for || recipient == offer_addr
}