guid - [mainnet]
A module for generating globally unique identifiers
Constants
GUID generator must be published ahead of first usage of create_with_capability
function.
const EGUID_GENERATOR_NOT_PUBLISHED: u64 = 0;
Structs
GUID
A globally unique identifier derived from the sender’s address and a counter
struct GUID has drop, store
Fields
-
id: guid::ID
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 thei+1
th GUID created byaddr
-
addr: address
- Address that created the GUID
Functions
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, } }}
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 }}
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}
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}
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}
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}
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}
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. | Requirement | Criticality | Implementation | Enforcement |
---|---|---|---|---|
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;
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;
create_id
public fun create_id(addr: address, creation_num: u64): guid::ID
// This enforces high-level requirement 2:aborts_if false;
id
public fun id(guid: &guid::GUID): guid::ID
// This enforces high-level requirement 2:aborts_if false;
creator_address
public fun creator_address(guid: &guid::GUID): address
// This enforces high-level requirement 2:aborts_if false;
id_creator_address
public fun id_creator_address(id: &guid::ID): address
// This enforces high-level requirement 2:aborts_if false;
creation_num
public fun creation_num(guid: &guid::GUID): u64
// This enforces high-level requirement 2:aborts_if false;
id_creation_num
public fun id_creation_num(id: &guid::ID): u64
// This enforces high-level requirement 2:aborts_if false;
eq_id
public fun eq_id(guid: &guid::GUID, id: &guid::ID): bool
// This enforces high-level requirement 2:aborts_if false;