Module 0x2f66c09143acc52a85fec529a4e20c85::Immutable

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

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

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 unwrap, 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;