Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Module 0x1::guid

A module for generating globally unique identifiers

Struct GUID

A globally unique identifier derived from the sender’s address and a counter

struct GUID has drop, store
Fields
id: guid::ID

Struct ID

A non-privileged identifier that can be freely created by anyone. Useful for looking up GUID’s.

struct ID has copy, drop, store
Fields
creation_num: u64
If creation_num is i, this is the i+1th GUID created by addr
addr: address
Address that created the GUID

Constants

GUID generator must be published ahead of first usage of create_with_capability function.

const EGUID_GENERATOR_NOT_PUBLISHED: u64 = 0;

Function create

Create and return a new GUID from a trusted module.

public(friend) fun create(addr: address, creation_num_ref: &mut u64): guid::GUID
Implementation 
public(friend) fun create(addr: address, creation_num_ref: &mut u64): GUID {
    let creation_num = *creation_num_ref;
    *creation_num_ref = creation_num + 1;
    GUID {
        id: ID {
            creation_num,
            addr,
        }
    }
}

Function create_id

Create a non-privileged id from addr and creation_num

public fun create_id(addr: address, creation_num: u64): guid::ID
Implementation 
public fun create_id(addr: address, creation_num: u64): ID {
    ID { creation_num, addr }
}

Function id

Get the non-privileged ID associated with a GUID

public fun id(guid: &guid::GUID): guid::ID
Implementation 
public fun id(guid: &GUID): ID {
    guid.id
}

Function creator_address

Return the account address that created the GUID

public fun creator_address(guid: &guid::GUID): address
Implementation 
public fun creator_address(guid: &GUID): address {
    guid.id.addr
}

Function id_creator_address

Return the account address that created the guid::ID

public fun id_creator_address(id: &guid::ID): address
Implementation 
public fun id_creator_address(id: &ID): address {
    id.addr
}

Function creation_num

Return the creation number associated with the GUID

public fun creation_num(guid: &guid::GUID): u64
Implementation 
public fun creation_num(guid: &GUID): u64 {
    guid.id.creation_num
}

Function id_creation_num

Return the creation number associated with the guid::ID

public fun id_creation_num(id: &guid::ID): u64
Implementation 
public fun id_creation_num(id: &ID): u64 {
    id.creation_num
}

Function eq_id

Return true if the GUID’s ID is id

public fun eq_id(guid: &guid::GUID, id: &guid::ID): bool
Implementation 
public fun eq_id(guid: &GUID, id: &ID): bool {
    &guid.id == id
}

Specification

High-level Requirements

No.RequirementCriticalityImplementationEnforcement
1 The creation of GUID constructs a unique GUID by combining an address with an incremented creation number. Low The create function generates a new GUID by combining an address with an incremented creation number, effectively creating a unique identifier. Enforced via create.
2 The operations on GUID and ID, such as construction, field access, and equality comparison, should not abort. Low The following functions will never abort: (1) create_id, (2) id, (3) creator_address, (4) id_creator_address, (5) creation_num, (6) id_creation_num, and (7) eq_id. Verified via create_id, id, creator_address, id_creator_address, creation_num, id_creation_num, and eq_id.
3 The creation number should increment by 1 with each new creation. Low An account can only own up to MAX_U64 resources. Not incrementing the guid_creation_num constantly could lead to shrinking the space for new resources. Enforced via create.
4 The creation number and address of an ID / GUID must be immutable. Medium The addr and creation_num values are meant to be constant and never updated as they are unique and used for identification. Audited: This is enforced through missing functionality to update the creation_num or addr.

Module-level Specification 

pragma verify = true;
pragma aborts_if_is_strict;

Function create 

public(friend) fun create(addr: address, creation_num_ref: &mut u64): guid::GUID

aborts_if creation_num_ref + 1 > MAX_U64;
// This enforces high-level requirement 1:
ensures result.id.creation_num == old(creation_num_ref);
// This enforces high-level requirement 3:
ensures creation_num_ref == old(creation_num_ref) + 1;

Function create_id 

public fun create_id(addr: address, creation_num: u64): guid::ID

// This enforces high-level requirement 2:
aborts_if false;

Function id 

public fun id(guid: &guid::GUID): guid::ID

// This enforces high-level requirement 2:
aborts_if false;

Function creator_address 

public fun creator_address(guid: &guid::GUID): address

// This enforces high-level requirement 2:
aborts_if false;

Function id_creator_address 

public fun id_creator_address(id: &guid::ID): address

// This enforces high-level requirement 2:
aborts_if false;

Function creation_num 

public fun creation_num(guid: &guid::GUID): u64

// This enforces high-level requirement 2:
aborts_if false;

Function id_creation_num 

public fun id_creation_num(id: &guid::ID): u64

// This enforces high-level requirement 2:
aborts_if false;

Function eq_id 

public fun eq_id(guid: &guid::GUID, id: &guid::ID): bool

// This enforces high-level requirement 2:
aborts_if false;