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::event

The Event module defines an EventHandleGenerator that is used to create EventHandles with unique GUIDs. It contains a counter for the number of EventHandles 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;

Struct EventHandle

A handle for an event such that:

  1. Other modules can emit events to this handle.
  2. 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.

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;

Function 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);
}

Function 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);

Function 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,
    }
}

Function 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 += 1;
}

Function 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
}

Function 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
}

Function write_to_event_store

Log msg as the countth 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);

Function 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.RequirementCriticalityImplementationEnforcement
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;

Function emit 

public fun emit<T: drop, store>(msg: T)

pragma opaque;

Function write_module_event_to_store 

fun write_module_event_to_store<T: drop, store>(msg: T)

Native function use opaque.

pragma opaque;

Function 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;

Function guid 

#[deprecated]
public fun guid<T: drop, store>(handle_ref: &event::EventHandle<T>): &guid::GUID

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

Function counter 

#[deprecated]
public fun counter<T: drop, store>(handle_ref: &event::EventHandle<T>): u64

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

Function 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;

Function destroy_handle 

#[deprecated]
public fun destroy_handle<T: drop, store>(handle: event::EventHandle<T>)

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