taohe

Move smart contracts implementing nestable resources on MoveVM blockchains

View on GitHub

Module 0x2f66c09143acc52a85fec529a4e20c85::Immutable

A simple tao whose only purpose is to keep the content immutable

Resource Tao

Static tao containing a resource. Can’t be extracted.

struct Tao<Content> has store, key
Fields
content: Content

Function wrap

Creating a static tao whose content cannot be extracted.

public fun wrap<Content>(content: Content): Immutable::Tao<Content>
Implementation
public fun wrap<Content>(content: Content): Tao<Content> {
    Tao<Content> { content }
}
Specification
ensures result.content == content;

Function read

Immutable read-only reference to the content.

public fun read<Content>(tao: &Immutable::Tao<Content>): &Content
Implementation
public fun read<Content>(tao: &Tao<Content>): &Content {
    let Tao<Content> { content } = tao;

    content
}
Specification
ensures result == tao.content;

Function unwrap

For semantic reasons providing extract, although it always fails.

public fun unwrap<Content>(_tao: Immutable::Tao<Content>): Content
Implementation
public fun unwrap<Content>(_tao: Tao<Content>): Content {
    // Aborting with general error for now: using our
    // Errors module would break formal verification
    // (https://github.com/diem/diem/issues/8303).
    abort(1)
}
Specification
aborts_if true with 1;
pragma aborts_if_is_strict;