event - [mainnet]
The Event module defines an EventHandleGenerator
that is used to create
EventHandle
s with unique GUIDs. It contains a counter for the number
of EventHandle
s it generates. An EventHandle
is used to count the number of
events emitted to a handle and emit events to the event store.
use 0x1::bcs;use 0x1::guid;
Constants
An event cannot be created. This error is returned by native implementations when
- The type tag for event is too deeply nested.
const ECANNOT_CREATE_EVENT: u64 = 1;
Structs
EventHandle
A handle for an event such that:
- Other modules can emit events to this handle.
- Storage can use this handle to prove the total number of events that happened in the past.
#[deprecated]struct EventHandle<T: drop, store> has store
Fields
-
counter: u64
- Total number of events emitted to this event stream.
-
guid: guid::GUID
- A globally unique ID for this event stream.
Functions
emit
Emit a module event with payload msg
.
public fun emit<T: drop, store>(msg: T)
Implementation
public fun emit<T: store + drop>(msg: T) { write_module_event_to_store<T>(msg);}
write_module_event_to_store
Log msg
with the event stream identified by T
fun write_module_event_to_store<T: drop, store>(msg: T)
Implementation
native fun write_module_event_to_store<T: drop + store>(msg: T);
new_event_handle
Use EventHandleGenerator to generate a unique event handle for sig
#[deprecated]public(friend) fun new_event_handle<T: drop, store>(guid: guid::GUID): event::EventHandle<T>
Implementation
public(friend) fun new_event_handle<T: drop + store>(guid: GUID): EventHandle<T> { EventHandle<T> { counter: 0, guid, }}
emit_event
Emit an event with payload msg
by using handle_ref
’s key and counter.
#[deprecated]public fun emit_event<T: drop, store>(handle_ref: &mut event::EventHandle<T>, msg: T)
Implementation
public fun emit_event<T: drop + store>(handle_ref: &mut EventHandle<T>, msg: T) { write_to_event_store<T>(bcs::to_bytes(&handle_ref.guid), handle_ref.counter, msg); spec { assume handle_ref.counter + 1 <= MAX_U64; }; handle_ref.counter = handle_ref.counter + 1;}
guid
Return the GUID associated with this EventHandle
#[deprecated]public fun guid<T: drop, store>(handle_ref: &event::EventHandle<T>): &guid::GUID
Implementation
public fun guid<T: drop + store>(handle_ref: &EventHandle<T>): &GUID { &handle_ref.guid}
counter
Return the current counter associated with this EventHandle
#[deprecated]public fun counter<T: drop, store>(handle_ref: &event::EventHandle<T>): u64
Implementation
public fun counter<T: drop + store>(handle_ref: &EventHandle<T>): u64 { handle_ref.counter}
write_to_event_store
Log msg
as the count
th event associated with the event stream identified by guid
#[deprecated]fun write_to_event_store<T: drop, store>(guid: vector<u8>, count: u64, msg: T)
Implementation
native fun write_to_event_store<T: drop + store>(guid: vector<u8>, count: u64, msg: T);
destroy_handle
Destroy a unique handle.
#[deprecated]public fun destroy_handle<T: drop, store>(handle: event::EventHandle<T>)
Implementation
public fun destroy_handle<T: drop + store>(handle: EventHandle<T>) { EventHandle<T> { counter: _, guid: _ } = handle;}
Specification
High-level Requirements
No. | Requirement | Criticality | Implementation | Enforcement |
---|---|---|---|---|
1 | Each event handle possesses a distinct and unique GUID. | Critical | The new_event_handle function creates an EventHandle object with a unique GUID, ensuring distinct identification. | Audited: GUIDs are created in guid::create. Each time the function is called, it increments creation_num_ref. Multiple calls to the function will result in distinct GUID values. |
2 | Unable to publish two events with the same GUID & sequence number. | Critical | Two events may either have the same GUID with a different counter or the same counter with a different GUID. | This is implied by high-level requirement 1. |
3 | Event native functions respect normal Move rules around object creation and destruction. | Critical | Must follow the same rules and principles that apply to object creation and destruction in Move when using event native functions. | The native functions of this module have been manually audited. |
4 | Counter increases monotonically between event emissions | Medium | With each event emission, the emit_event function increments the counter of the EventHandle by one. | Formally verified in the post condition of emit_event. |
5 | For a given EventHandle, it should always be possible to: (1) return the GUID associated with this EventHandle, (2) return the current counter associated with this EventHandle, and (3) destroy the handle. | Low | The following functions should not abort if EventHandle exists: guid(), counter(), destroy_handle(). | Formally verified via guid, counter and destroy_handle. |
Module-level Specification
pragma verify = true;pragma aborts_if_is_strict;
emit
public fun emit<T: drop, store>(msg: T)
pragma opaque;
write_module_event_to_store
fun write_module_event_to_store<T: drop, store>(msg: T)
Native function use opaque.
pragma opaque;
emit_event
#[deprecated]public fun emit_event<T: drop, store>(handle_ref: &mut event::EventHandle<T>, msg: T)
pragma opaque;aborts_if [abstract] false;// This enforces high-level requirement 4:ensures [concrete] handle_ref.counter == old(handle_ref.counter) + 1;
guid
#[deprecated]public fun guid<T: drop, store>(handle_ref: &event::EventHandle<T>): &guid::GUID
// This enforces high-level requirement 5:aborts_if false;
counter
#[deprecated]public fun counter<T: drop, store>(handle_ref: &event::EventHandle<T>): u64
// This enforces high-level requirement 5:aborts_if false;
write_to_event_store
#[deprecated]fun write_to_event_store<T: drop, store>(guid: vector<u8>, count: u64, msg: T)
Native function use opaque.
pragma opaque;
destroy_handle
#[deprecated]public fun destroy_handle<T: drop, store>(handle: event::EventHandle<T>)
// This enforces high-level requirement 5:aborts_if false;