A tao for implementing a simple ownership model: owner can extract the content.
Simple ownership tao: the owner
can extract content
.
struct Tao<Content> has store, key
Fields
-
owner: address
-
content: Content
Wrapping content
into a tao the owner
can only extract.
public fun wrap<Content>(owner: address, content: Content): Ownable::Tao<Content>
Implementation
Specification
ensures result.owner == owner && result.content == content;
Immutable read-only reference to the owner address, and content
.
public fun read<Content>(tao: &Ownable::Tao<Content>): (&address, &Content)
Implementation
Specification
ensures result_1 == tao.owner;
ensures result_2 == tao.content;
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;