Module 0x1::dkg

DKG on-chain states and helper functions.

• Struct DKGSessionMetadata
• Struct DKGStartEvent
• Struct DKGSessionState
• Resource DKGState
• Constants
• Function initialize
• Function start
• Function finish
• Function try_clear_incomplete_session
• Function incomplete_session
• Function last_completed_session
• Function session_dealer_epoch
• Function is_session_started
• Specification
  • Function initialize
  • Function start
  • Function finish
  • Function try_clear_incomplete_session
  • Function incomplete_session
  • Function last_completed_session
  • Function is_session_started

use 0x1::error;
use 0x1::event;
use 0x1::option;
use 0x1::randomness_config;
use 0x1::system_addresses;
use 0x1::timestamp;
use 0x1::validator_consensus_info;

Struct DKGSessionMetadata

This can be considered as the public input of DKG.

struct DKGSessionMetadata has copy, drop, store

Struct DKGStartEvent

#[event]
struct DKGStartEvent has drop, store

Struct DKGSessionState

The input and output of a DKG session. The validator set of epoch x works together for an DKG output for the target validator set of epoch x+1.

struct DKGSessionState has copy, drop, store

Resource DKGState

The completed and in-progress DKG sessions.

struct DKGState has key

Constants

const EDKG_IN_PROGRESS: u64 = 1;

const EDKG_NOT_IN_PROGRESS: u64 = 2;

Function initialize

Called in genesis to initialize on-chain states.

public fun initialize(aptos_framework: &signer)

public fun initialize(aptos_framework: &signer) {
    system_addresses::assert_aptos_framework(aptos_framework);
    if (!exists<DKGState>(@aptos_framework)) {
        move_to<DKGState>(
            aptos_framework,
            DKGState {
                last_completed: std::option::none(),
                in_progress: std::option::none(),
            }
        );
    }
}

Function start

Mark on-chain DKG state as in-progress. Notify validators to start DKG. Idempotent for dealer_epoch: if a session for this epoch has already been started (in_progress or last_completed), returns without overwriting state or re-emitting an event. This enforces the invariant “at most one DKGStartEvent per epoch.”

public(friend) fun start(dealer_epoch: u64, randomness_config: randomness_config::RandomnessConfig, dealer_validator_set: vector<validator_consensus_info::ValidatorConsensusInfo>, target_validator_set: vector<validator_consensus_info::ValidatorConsensusInfo>)

public(friend) fun start(
    dealer_epoch: u64,
    randomness_config: RandomnessConfig,
    dealer_validator_set: vector<ValidatorConsensusInfo>,
    target_validator_set: vector<ValidatorConsensusInfo>,
) acquires DKGState {
    if (is_session_started(dealer_epoch)) { return };
    let dkg_state = borrow_global_mut<DKGState>(@aptos_framework);
    let new_session_metadata = DKGSessionMetadata {
        dealer_epoch,
        randomness_config,
        dealer_validator_set,
        target_validator_set,
    };
    let start_time_us = timestamp::now_microseconds();
    dkg_state.in_progress = std::option::some(DKGSessionState {
        metadata: new_session_metadata,
        start_time_us,
        transcript: vector[],
    });

    emit(DKGStartEvent {
        start_time_us,
        session_metadata: new_session_metadata,
    });
}

Function finish

Put a transcript into the currently incomplete DKG session, then mark it completed.

Abort if DKG is not in progress.

public(friend) fun finish(transcript: vector<u8>)

public(friend) fun finish(transcript: vector<u8>) acquires DKGState {
    let dkg_state = borrow_global_mut<DKGState>(@aptos_framework);
    assert!(dkg_state.in_progress.is_some(), error::invalid_state(EDKG_NOT_IN_PROGRESS));
    let session = dkg_state.in_progress.extract();
    session.transcript = transcript;
    dkg_state.last_completed = option::some(session);
    dkg_state.in_progress = option::none();
}

Function try_clear_incomplete_session

Delete the currently incomplete session, if it exists.

public fun try_clear_incomplete_session(fx: &signer)

public fun try_clear_incomplete_session(fx: &signer) acquires DKGState {
    system_addresses::assert_aptos_framework(fx);
    if (exists<DKGState>(@aptos_framework)) {
        let dkg_state = borrow_global_mut<DKGState>(@aptos_framework);
        dkg_state.in_progress = option::none();
    }
}

Function incomplete_session

Return the incomplete DKG session state, if it exists.

public fun incomplete_session(): option::Option<dkg::DKGSessionState>

public fun incomplete_session(): Option<DKGSessionState> acquires DKGState {
    if (exists<DKGState>(@aptos_framework)) {
        borrow_global<DKGState>(@aptos_framework).in_progress
    } else {
        option::none()
    }
}

Function last_completed_session

Return the last completed DKG session state, if any.

public fun last_completed_session(): option::Option<dkg::DKGSessionState>

public fun last_completed_session(): Option<DKGSessionState> acquires DKGState {
    if (exists<DKGState>(@aptos_framework)) {
        borrow_global<DKGState>(@aptos_framework).last_completed
    } else {
        option::none()
    }
}

Function session_dealer_epoch

Return the dealer epoch of a DKGSessionState.

public fun session_dealer_epoch(session: &dkg::DKGSessionState): u64

public fun session_dealer_epoch(session: &DKGSessionState): u64 {
    session.metadata.dealer_epoch
}

Function is_session_started

True iff a DKG session has ever been started for epoch (in_progress for epoch OR last_completed for epoch). Used by dkg::start to enforce “at most one DKGStartEvent per epoch”.

public fun is_session_started(epoch: u64): bool

public fun is_session_started(epoch: u64): bool acquires DKGState {
    let in_prog = incomplete_session();
    if (in_prog.is_some() && session_dealer_epoch(in_prog.borrow()) == epoch) {
        return true
    };
    let last = last_completed_session();
    if (last.is_some() && session_dealer_epoch(last.borrow()) == epoch) {
        return true
    };
    false
}

Specification

invariant [suspendable] chain_status::is_operating() ==> exists<DKGState>(@aptos_framework);

Function initialize

public fun initialize(aptos_framework: &signer)

let aptos_framework_addr = signer::address_of(aptos_framework);
aborts_if aptos_framework_addr != @aptos_framework;

Function start

public(friend) fun start(dealer_epoch: u64, randomness_config: randomness_config::RandomnessConfig, dealer_validator_set: vector<validator_consensus_info::ValidatorConsensusInfo>, target_validator_set: vector<validator_consensus_info::ValidatorConsensusInfo>)

aborts_if !exists<DKGState>(@aptos_framework);
aborts_if !spec_is_session_started(dealer_epoch)
    && !exists<timestamp::CurrentTimeMicroseconds>(@aptos_framework);
ensures spec_is_session_started(dealer_epoch);
ensures old(spec_is_session_started(dealer_epoch))
    ==> global<DKGState>(@aptos_framework) == old(global<DKGState>(@aptos_framework));

Function finish

public(friend) fun finish(transcript: vector<u8>)

requires exists<DKGState>(@aptos_framework);
requires option::is_some(global<DKGState>(@aptos_framework).in_progress);
aborts_if false;

fun has_incomplete_session(): bool {
   if (exists<DKGState>(@aptos_framework)) {
       option::is_some(global<DKGState>(@aptos_framework).in_progress)
   } else {
       false
   }
}

Function try_clear_incomplete_session

public fun try_clear_incomplete_session(fx: &signer)

let addr = signer::address_of(fx);
aborts_if addr != @aptos_framework;

Function incomplete_session

public fun incomplete_session(): option::Option<dkg::DKGSessionState>

aborts_if false;

Function last_completed_session

public fun last_completed_session(): option::Option<dkg::DKGSessionState>

aborts_if false;
ensures result == if (exists<DKGState>(@aptos_framework)) {
    global<DKGState>(@aptos_framework).last_completed
} else {
    option::spec_none()
};

Function is_session_started

public fun is_session_started(epoch: u64): bool

aborts_if false;
ensures result == spec_is_session_started(epoch);

A session has been started for epoch iff either the in-progress or the last-completed session on chain has dealer_epoch == epoch.

fun spec_is_session_started(epoch: u64): bool {
   exists<DKGState>(@aptos_framework) && (
       (option::is_some(global<DKGState>(@aptos_framework).in_progress)
        && option::borrow(global<DKGState>(@aptos_framework).in_progress)
               .metadata.dealer_epoch == epoch)
       || (option::is_some(global<DKGState>(@aptos_framework).last_completed)
           && option::borrow(global<DKGState>(@aptos_framework).last_completed)
                  .metadata.dealer_epoch == epoch)
   )
}