Module 0x2f66c09143acc52a85fec529a4e20c85::Ownable

A tao for implementing a simple ownership model: owner can extract the content.

• Resource Tao
• Function wrap
• Function read
• Function unwrap

use 0x1::signer;
use 0x2f66c09143acc52a85fec529a4e20c85::Errors;

Resource Tao

Simple ownership tao: the owner can extract content.

struct Tao<Content> has store, key

Fields

owner: address

content: Content

Function wrap

Wrapping content into a tao the owner can only extract.

public fun wrap<Content>(owner: address, content: Content): Ownable::Tao<Content>

Implementation

public fun wrap<Content>(owner: address, content: Content): Tao<Content> {
    Tao<Content> { owner, content }
}

Specification

ensures result.owner == owner && result.content == content;

Function read

Immutable read-only reference to the owner address, and content.

public fun read<Content>(tao: &Ownable::Tao<Content>): (&address, &Content)

Implementation

public fun read<Content>(tao: &Tao<Content>): (&address, &Content) {
    let Tao<Content> { owner, content } = tao;

    (owner, content)
}

Specification

ensures result_1 == tao.owner;
ensures result_2 == tao.content;

Function unwrap

If account is the owner, extract content.

public fun unwrap<Content>(account: &signer, tao: Ownable::Tao<Content>): Content

Implementation

public fun unwrap<Content>(account: &signer, tao: Tao<Content>): Content {
    let Tao<Content> { owner, content } = tao;

    assert!(owner == signer::address_of(account), Errors::ownable_not_owned());

    content
}

Specification

aborts_if tao.owner != signer::address_of(account);
ensures result == tao.content;

pragma aborts_if_is_strict;