Module 0x1::chunky_dkg

Chunky DKG on-chain states and helper functions.

• Struct ChunkyDKGSessionMetadata
• Struct ChunkyDKGStartEvent
• Struct ChunkyDKGSessionState
• Resource ChunkyDKGState
• Constants
• Function initialize
• Function start
• Function finish
• Function try_clear_incomplete_session
• Function incomplete_session
• Function last_completed_session
• Function session_dealer_epoch
• Function session_start_time
• Function is_session_started
• Specification
  • 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

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

Struct ChunkyDKGSessionMetadata

This can be considered as the public input of Chunky DKG.

struct ChunkyDKGSessionMetadata has copy, drop, store

Struct ChunkyDKGStartEvent

#[event]
struct ChunkyDKGStartEvent has drop, store

Struct ChunkyDKGSessionState

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

struct ChunkyDKGSessionState has copy, drop, store

Resource ChunkyDKGState

The completed and in-progress Chunky DKG sessions.

struct ChunkyDKGState has key

Constants

const ECHUNKY_DKG_IN_PROGRESS: u64 = 1;

const ECHUNKY_DKG_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<ChunkyDKGState>(@aptos_framework)) {
        move_to<ChunkyDKGState>(
            aptos_framework,
            ChunkyDKGState {
                last_completed: std::option::none(),
                in_progress: std::option::none()
            }
        );
    }
}

Function start

Mark on-chain Chunky DKG state as in-progress. Notify validators to start Chunky 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 ChunkyDKGStartEvent per epoch.”

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

public(friend) fun start(
    dealer_epoch: u64,
    chunky_dkg_config: ChunkyDKGConfig,
    dealer_validator_set: vector<ValidatorConsensusInfo>,
    target_validator_set: vector<ValidatorConsensusInfo>
) acquires ChunkyDKGState {
    if (is_session_started(dealer_epoch)) { return };
    let chunky_dkg_state = borrow_global_mut<ChunkyDKGState>(@aptos_framework);
    let new_session_metadata = ChunkyDKGSessionMetadata {
        dealer_epoch,
        chunky_dkg_config,
        dealer_validator_set,
        target_validator_set
    };
    let start_time_us = timestamp::now_microseconds();
    chunky_dkg_state.in_progress = std::option::some(
        ChunkyDKGSessionState {
            metadata: new_session_metadata,
            start_time_us,
            aggregated_subtranscript: vector[]
        }
    );

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

Function finish

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

Abort if Chunky DKG is not in progress.

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

public(friend) fun finish(aggregated_subtranscript: vector<u8>) acquires ChunkyDKGState {
    let chunky_dkg_state = borrow_global_mut<ChunkyDKGState>(@aptos_framework);
    assert!(
        chunky_dkg_state.in_progress.is_some(),
        error::invalid_state(ECHUNKY_DKG_NOT_IN_PROGRESS)
    );
    let session = chunky_dkg_state.in_progress.extract();
    session.aggregated_subtranscript = aggregated_subtranscript;
    chunky_dkg_state.last_completed = option::some(session);
    chunky_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 ChunkyDKGState {
    system_addresses::assert_aptos_framework(fx);
    if (exists<ChunkyDKGState>(@aptos_framework)) {
        let chunky_dkg_state = borrow_global_mut<ChunkyDKGState>(@aptos_framework);
        chunky_dkg_state.in_progress = option::none();
    }
}

Function incomplete_session

Return the incomplete Chunky DKG session state, if it exists.

public fun incomplete_session(): option::Option<chunky_dkg::ChunkyDKGSessionState>

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

Function last_completed_session

Return the last completed Chunky DKG session state, if any.

public fun last_completed_session(): option::Option<chunky_dkg::ChunkyDKGSessionState>

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

Function session_dealer_epoch

Return the dealer epoch of a ChunkyDKGSessionState.

public fun session_dealer_epoch(session: &chunky_dkg::ChunkyDKGSessionState): u64

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

Function session_start_time

Return the start time in microseconds of a ChunkyDKGSessionState.

public fun session_start_time(session: &chunky_dkg::ChunkyDKGSessionState): u64

public fun session_start_time(session: &ChunkyDKGSessionState): u64 {
    session.start_time_us
}

Function is_session_started

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

public fun is_session_started(epoch: u64): bool

public fun is_session_started(epoch: u64): bool acquires ChunkyDKGState {
    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

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, chunky_dkg_config: chunky_dkg_config::ChunkyDKGConfig, dealer_validator_set: vector<validator_consensus_info::ValidatorConsensusInfo>, target_validator_set: vector<validator_consensus_info::ValidatorConsensusInfo>)

aborts_if !exists<ChunkyDKGState>(@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<ChunkyDKGState>(@aptos_framework)
        == old(global<ChunkyDKGState>(@aptos_framework));

Function finish

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

requires exists<ChunkyDKGState>(@aptos_framework);
requires option::is_some(global<ChunkyDKGState>(@aptos_framework).in_progress);
aborts_if 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<chunky_dkg::ChunkyDKGSessionState>

aborts_if false;

Function last_completed_session

public fun last_completed_session(): option::Option<chunky_dkg::ChunkyDKGSessionState>

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

Function session_dealer_epoch

public fun session_dealer_epoch(session: &chunky_dkg::ChunkyDKGSessionState): u64

aborts_if false;

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<ChunkyDKGState>(@aptos_framework) && (
       (option::is_some(global<ChunkyDKGState>(@aptos_framework).in_progress)
        && option::borrow(global<ChunkyDKGState>(@aptos_framework).in_progress)
               .metadata.dealer_epoch == epoch)
       || (option::is_some(global<ChunkyDKGState>(@aptos_framework).last_completed)
           && option::borrow(global<ChunkyDKGState>(@aptos_framework).last_completed)
                  .metadata.dealer_epoch == epoch)
   )
}