Module 0x1::copyable_any

• Struct Any
• Constants
• Function pack
• Function unpack
• Function type_name
• Specification
  • Function pack
  • Function unpack
  • Function type_name

use 0x1::bcs;
use 0x1::error;
use 0x1::from_bcs;
use 0x1::string;
use 0x1::type_info;

Struct Any

The same as any::Any but with the copy ability.

struct Any has copy, drop, store

Constants

The type provided for unpack is not the same as was given for pack.

const ETYPE_MISMATCH: u64 = 0;

Function pack

Pack a value into the Any representation. Because Any can be stored, dropped, and copied this is also required from T.

public fun pack<T: copy, drop, store>(x: T): copyable_any::Any

public fun pack<T: drop + store + copy>(x: T): Any {
    Any {
        type_name: type_info::type_name<T>(),
        data: bcs::to_bytes(&x)
    }
}

Function unpack

Unpack a value from the Any representation. This aborts if the value has not the expected type T.

public fun unpack<T>(self: copyable_any::Any): T

public fun unpack<T>(self: Any): T {
    assert!(type_info::type_name<T>() == self.type_name, error::invalid_argument(ETYPE_MISMATCH));
    from_bytes<T>(self.data)
}

Function type_name

Returns the type name of this Any

public fun type_name(self: &copyable_any::Any): &string::String

public fun type_name(self: &Any): &String {
    &self.type_name
}

Specification

Function pack

public fun pack<T: copy, drop, store>(x: T): copyable_any::Any

aborts_if false;
pragma opaque;
ensures result == Any {
    type_name: type_info::type_name<T>(),
    data: bcs::serialize<T>(x)
};
ensures [abstract] from_bcs::deserializable<T>(result.data);

Function unpack

public fun unpack<T>(self: copyable_any::Any): T

include UnpackAbortsIf<T>;
ensures result == from_bcs::deserialize<T>(self.data);

schema UnpackAbortsIf<T> {
    self: Any;
    aborts_if type_info::type_name<T>() != self.type_name;
    aborts_if !from_bcs::deserializable<T>(self.data);
}

Function type_name

public fun type_name(self: &copyable_any::Any): &string::String

aborts_if false;
ensures result == self.type_name;