Acki Nacki documentation
Acki Nacki docsFor DevelopersWhat is Acki Nacki?
  • Acki Nacki Overview
  • Glossary
  • Launch & Genesis
  • Tokenomics
    • Fee System
  • Protocol participation
    • License
      • Acki Nacki Node License
      • Working with Licenses
      • License Delegation Guide
    • Block Keeper
      • Guide for Block Keeper testing on Shellnet
      • Join DNSP Gossip
      • Setting up Block Keeper Node
      • How to join the protocol as Block Keeper?
      • Formal Verification
        • Block Keeper Contracts Business-Level Specification
        • Block Keeper Contracts High Level Specification
    • Block Manager
      • Setting up Block Manager Node
    • Proxy service
  • Wallet
    • Create Your Wallet
    • ZK Login Authentication Flow
Powered by GitBook
On this page
  • Purpose
  • Introduction
  • Single participation period
  • Repeated participation
  • Stake workflow
  • Auxiliary values
  • Reward
  • Licences
  • Slashing
  • Details
  • Common
  • Participant registration
  • Withdraw
  • Participation
  • Proxy
  • License management
  • Top-level scenarios
  1. Protocol participation
  2. Block Keeper
  3. Formal Verification

Block Keeper Contracts Business-Level Specification

Prepared by Pruvendo

PreviousFormal VerificationNextBlock Keeper Contracts High Level Specification

Last updated 23 days ago

Purpose

The purpose of the present document is to create business-level specification (highest-level of specification) for the Block Keeper set of smart contracts. This document is intended to:

  • Be thoroughly reviewed by the Customer

  • Act as a base for the high-level specification

Introduction

The key intention of the Block Keeper set of smart contracts is to let any participant become a Block Keeper either for a single participation (in Acki Nacki protocol as Block Keeper) period (called Epoch) or repeatedly.

Single participation period

In this case the following stages are introduced:

  • Pre Epoch. This stage is relatively short (a few minutes) and intended to let the Block Keeper to finish synchronizing its node if necessary

  • Epoch - the main stage where the participant acts as a Block Keeper. Its duration is usually is most than one day

  • Cooling - the terminating stage where the Block Keeper can still be slashed (up to 30% of Epoch’s duration)

The workflow described below must be followed:

  • Participant must be registered as a Block Keeper

  • Stake (exceeding minimally allowed value, which is a dynamic parameter) must be deposited

  • Pre Epoch must be started and, then, finished

  • Then, Epoch:

    • Must be started

    • Throughout the Epoch, the participant is a Block Keeper

    • Later Epoch must be finished

  • Then, Cooling:

    • Must be started

    • At any time the Block Keeper can be slashed

    • Later Cooling must be finished and:

    • Then, stake can be withdrawn or reinvested

Graphically, the described workflow can be presented by the following chart:

Repeated participation

The main difference with the Single Participation Period is that upon Epoch completion, a new Epoch starts immediately.

The workflow described below must be followed:

  • Participant must be registered as a Block Keeper

  • Stake (exceeding minimally allowed value) must be deposited

  • Pre Epoch must be started and, then, finished

  • Then, Epoch:

    • Must be started

    • Another (additional) stake must be deposited making the workflow repeated thus turning Epoch into continue state

    • Later Epoch must be finished

  • Then:

    • New Epoch (in non-continued state) starts immediately with additional stake

    • Cooling:

      • Must be started with the rest of stake

      • At any time the Block Keeper can be slashed

      • Later Cooling must be finished and:

      • Then, stake can be withdrawn or reinvested any time in future

The described workflow is illustrated by the following diagram:

Stake workflow

Throughout the loop, stakes are transferred from one entity to another. For single participation their workflow can be illustrated by the following diagram (the second row indicated what entity the stake belongs to at each stage):

For repeated participation the diagram is more complicated:

It’s important to mention that in case the participant (owner) reinvests each stake for the repeated participation immediately after cooling down by continuing the current Epoch, he gets some kind of a carousel of continuous participation.

Such a carousel is illustrated in the diagram below. For simplicity, all the “gray” periods between ending of the particular stages and external actions are omitted. Green dots stay for the “first” stake, while the red one - for the “second” stake.

Auxiliary values

Number of active blockkeepers

  • Increased when a new blockkeeper arranges its first stake

  • Decreased when a blockkeeper is fully slashed

Is_min

where:

  • L - set of licenses assigned to the wallet

  • r - reputation time of the license

  • s - start time of the license

  • d - Epoch duration

  • t - current time

  • 𝜎 - current stake

  • 𝜎。 - last stake

  • f - time, when the licenses become free

Minimal Stake

Minimal stake is calculated is by calling a special TVM instruction with the following parameters:

    • r - total reward assigned

    • s - total amount slashed

    • t - current time

    • t。 - time when network started

    • w - wait step

  • Number of active blockkeepers

Virtual Stake

Local Stake

  • Otherwise, it’s just a stake

Total Stake

Planned Epoch Finish Time

  • s - Epoch start time

  • d - Epoch duration

Reward

Reward is calculated at the end of Epoch, but remains locked until the cooler stage ends.. It is implemented using a special TVM instruction and depends on:

  • Total reward already assigned at the time of calculation

    • t - current time

    • t。 - time when the Epoch started

    • s -

    • n - number of participating licenses

    • d - Epoch duration

    • t - current time

Reward Adjustment

  • l - last time adjustment was performed

  • p - minimal period between adjustments

  • t - current time

  • n - number of adjustments

When performed the special TVM instruction is called with the following parameters and the number of adjustments is increased as well as a reward period:

  • Total amount of assigned rewards

  • Reputation coefficient, that is:

    • MIN_REP_COEF constant, in case if equals to zero

    • average reputation coefficient, otherwise

  • Reward period, that is calculated as follows:

  • Previous value of Reward Adjustment

  • Current time

Licences

License smart contract is controlled by the License Owner’s cryptographic keys (ED25519). Without an active License smart contract, Block Keeper won’t function (it won’t be able to submit a stake to Epoch smart contract).

In order to submit stakes at least one License must be delegated to BK Wallet. Up to 10 Licenses can be delegated. A License can be delegated just to one BK wallet.

The rewards are split equally between all Licenses currently delegated. The stake is blocked for active wallet Licenses, in proportion to their wallet balances. If a slashing occurred the remaining stake will be divided proportionally between original stake owners.

The License contains text of provisions of GOSH Business License and AGPL. The License contains a provision that changes the Business License for AGPL two years after the first Acki Nacki block has been produced.

Licenses are transferable, i.e. their keys can be changed by the key owner without interrupting operations.

Within the first 2 years License (under Business License terms) give users an ability to join the network at any time without a minimum required stake, when certain conditions are met. This is further described in Block Keeper System Root below.

License Root

Licenses are always deployed by License Root to avoid a possibility of unauthorized/non-existent Licenses to be deployed.

GOSH holds keys for the License Root contract that allows it to issue new Licenses, but not revoke already issued ones.

Reputation

Reputation coefficient is recorded in the License contract and updated by Epoch smart contract with start block sequence number and end block sequence number. Epoch Smart Contract won’t be deployed if the reputation coefficient [1.0…3.0] between all licenses is inconsistent.

Reputation time

Reputation time is the total time of the license usage in stakes since the latter of:

  • License start

  • The last full slashing of the stake where the license participated

Average Reputation Coefficient

In case of increase:

    • a - the previous value of the Average Reputation Coefficient

      • s -

      • n - quantity of licenses assigned for the particular Epoch

In case of decrease:

    • a - the previous value of the Average Reputation Coefficient

      • s -

      • n - quantity of licenses assigned for the particular Epoch

Sum Reputation Coefficient

The Sum Reputation Coefficient is a sum of all the t of all the participating licenses at the time of Epoch creation, but slashed.

Reputation Coefficient

Reputation Coefficient is calculated by applying a special TVM instruction with as a parameter.

Auxiliary values

Balance

Each license has a balance associated with it.

  • Balance can be increased by running a public method to the wallet (the license must be owned by the wallet)

  • In case of license removal the balance must be zeroed, all the assets are to be transferred to the address provided by the license owner

  • In case of full slashing, the balance is decreased by the stake amount

  • In case of partial slashing, the balance is decreased by the corresponding portion of the stake amount

Lock Stake

The amount owned by the license but locked by the current Epoch.

    • 𝜎 - stake

    • 𝜆 - the current license

    • L - the set of the all participating licenses

    • b - the license

    • c - the amount locked by the Cooler

  • In case of too long PreEpoch it must be unlocked

    • e - locked stake

  • The locked amount can not be used for withdrawal

  • In case of slashing the locked amount is either zeroed or decreased proportionally

  • The locked stake must be released upon finished Epoch without continuation

Lock Cooler

This value represents the share of the license balance locked throughout the cooling phase.

  • Upon normal end of the cooling phase the locked amount is released

  • In case of slashing:

    • In case of full slashing the full amount is released

    • In case of partial slashing the proportional amount is released

Block Keeper Wallet

It is a smart contract which transmits user funds to an Epoch smart contract for staking, receives rewards, manages License rights and administers stakes in the Epoch contracts.

Block Keeper System Root

Block Keeper System Root is a smart contract which performs minimum stake validation, stores active validators number, manages Wallet and Epoch contract deployments, calculates rewards and mints them.

Any new License owner joining the network within the first 2 years is able to start validating without a need for stake. Note that such License owners can only join the network on these terms once. The perfect reputation count must be ensured therefore. In order to combat potential loss of stake due to bleeding the check is performed that the last stake without rewards is not less than a previous stake without rewards. The bleeding will come only from Rewards.

Slashing

Slashing is initiated by the node itself and can be applied both at Epoch and Cooler stages.

When the slashing is full:

  • All the deposited stakes are confiscated

  • The reputation time of all licenses, including old ones (possibly, owned by other people), is zeroed

  • All the keys are invalidated

  • is decreased accordingly in case the slashed license has participated

In case of partial slashing:

  • The provided percentage of the deposited stakes is confiscated

  • The reputation time of all licenses, including old ones (possibly, owned by other people), is zeroed

  • Auxiliary values of each license are changed as described in the corresponding section

  • is decreased accordingly in case the slashed license has participated

Details

Common

Before any action any participating system contract must be supplied with gas enough to perform this action, if necessary.

Participant registration

  • External request comes from anybody

  • New unique BNW (Block Keeper Node Wallet) is created

  • Newly created BNW is initialized

Withdraw

Can be called by License only.

Checks

  • if:

    • the required amount of tokens is available, and

    • the required amount of tokens is available at the License balance

  • If yes:

    • The balance of tokens is decreased by the required amount from the node wallet

    • The balance of the License is decreased by the required amount

    • The balance of tokens is increased by the required amount to the recipient

  • Otherwise:

    • Exception is raised

Participation

Stake placement

  • Owner sends a request to BNW

  • BNW checks if:

    • Owner is correct

    • Stake value is available (in ECC that serves as a secondary currency)

    • No stake already exists or being processed

    • At least one license is available

    • In case of success:

      • For each license:

        • There are “issues” if and only if:

          • Any License was not used at lease for a half of Epoch,

          or

          • Provided stake is less than last stake,

          or

          • GPL license is still in place

        • Reputation time becomes the sum of the reputation times of all the Licenses

        • Root is informed (alongside side with other information, it is informed, whether there were any issues, as well as sum of reputation times of all licenses being used)

  • Root checks if:

    • Stake exceeds minimally allowed value and no issues were received, otherwise it must be sent back

    • In case of success:

      • BLS key is created

      • BLS key is asked for acceptance

  • BLS key:

    • transfers this request to Root, informing alongside with other information, whether this was already used

      • marks the key as used

  • Root:

    • checks if the BLS key was not used, otherwise it sends stake back

    • In case of success:

      • Signer is created

      • Signer is asked for acceptance

  • Signer:

    • transfers this request to Root, informing alongside with other information, whether this was already used

    • marks the key as used

  • Root:

    • checks if the Singer was not used, otherwise:

      • it sends stake back

      • destroys BLS key

    • In case of success BNW is informed

  • New BKPE (Block Keeper Pre Epoch) created

  • Stake is moved to Pre Epoch

Pre Epoch

  • Upon creation:

    • BKPE is initialized

    • BNW is moved to “Pre Epoch” state

  • Then, at any moment external touch message can be received

  • If time for the next stage still did not come, nothing happens

  • Otherwise:

    • New Epoch created

    • Stake is moved to Epoch

    • BKPE is self-destructed and all its assets are transferred to Epoch

Epoch

  • Upon creation:

    • Epoch is initialized

    • Root is informed to enlist the Block Keeper

    • BNW is moved to “Epoch” state

  • Then, at any moment external touch message can be received

  • Also, at any moment external slash message can be received, and:

    • The whole stake will be confiscated

      • Reputation time for all existing and previous licenses is zeroed

      • BLS key is destroyed

      • Signer is destroyed

    • Wallet will be delisted

    • Continuation is canceled

      • All the licences mark as unused

      • BLS key is destroyed

      • Signer is destroyed

  • If time for the next stage still did not come, nothing happens

  • Otherwise:

    • Root is informed

    • Root checks if it’s possible to end an Epoch and does nothing if negative

    • Otherwise:

      • Block Keeper is delisted

      • Epoch is informed and:

        • Cooler is created

        • Stake (with reward) is moved to Cooler

        • Epoch is self-destructed in favor of Cooler

Cooler

  • Upon creation:

    • Cooler is initialized

    • BNW is moved to “Cooler” state

  • Then, at any moment external touch message can be received

  • Also, at any moment external slash message can be received, and:

    • The whole stake will be confiscated

      • Reputation time for all existing and previous licenses is zeroed

      • BLS key is destroyed

      • Signer is destroyed

    • Wallet will be delisted

    • Continuation is canceled

      • All the licences mark as unused

      • BLS key is destroyed

      • Signer is destroyed

  • If time for the next stage still did not come, nothing happens

  • Otherwise:

    • BNW is moved to initial state

    • BKPE is self-destructed and all stake transferred to the BNW

    • If any license exists, the profit is distributed evenly among them

    • BLS key is destroyed

    • Signer is destroyed

Epoch (Repeated)

  • Upon creation:

    • Epoch is initialized

    • Root is informed to enlist the Block Keeper

    • BNW is moved to “Epoch” state

  • Then, at any moment external touch message can be received

  • If time for the next stage still did not come, nothing happens

  • Otherwise:

    • Root is informed

    • Root checks if it’s possible to end an Epoch and does nothing if negative

    • Otherwise:

      • Epoch is informed and:

        • New repeated Epoch is created with additional stake

        • Cooler is created is the rest of stake with reward

        • Epoch is self-destructed in favor of Cooler

Proxy

This scenario handles the proxy system. Proxy List is created for any Epoch and stays until it ends (as an uncontinued one). In case of continued Epoch, the same Proxy List stands until it is canceled. Throughout the lifetime of the Proxy List, Proxy elements can be added or removed to/from it.

  • Initialization the proxy (during Pre Epoch creation)

  • Destruction of the proxy (by the end of an uncontinued Epoch)

  • Adding new elements to the Proxy List

  • Removal of elements from the Proxy List

License management

All the licenses can be created by License Root only.

Before moving to GPL they can be created by Owner only, later by anybody.

Attach to BK Wallet

License can be attached to BK Wallet by request from the license Owner.

In this case:

  • License:

    • Checks if the License is not attached to any other BK Wallet

    • Checks if the License attachment is not in progress

    • Informs the BK Wallet that it is going to be added

  • BK Wallet:

    • Checks if a number of Licenses does not exceed maximally allowed value

    • Increased a number of licenses

    • Increases a total reputation time

    • Informs License about acceptance

  • License:

    • Starts the license, if not started yet

    • Attaches the license to the BK Wallet

Detaching from BK Wallet

License can be detached from BK Wallet by request from the license Owner.

In this case:

  • License:

    • Checks if the License is attached to some BK Wallet

    • Informs the BK Wallet that it is going to be removed

  • BK Wallet:

    • Checks if the License exists

    • Decreased a number of licenses

    • Decreases a total reputation time

    • Transfers all the License balance to the specified address

    • Informs License about acceptance

  • License:

    • Detaches the license from the BK Wallet

    • Keeps the reputation time

Top-level scenarios

To formally specify the behavior briefly described above the following top-level scenarios were identified for further creation of high-level and, then, low-level formal specification:

  • Registration

  • ECC Withdrawal

  • Participation

  • Proxy

  • License management

This value indicates if the low stakes (below minimal value) are accepted (using the mechanism of ) or rejected. It’s calculated using the following formula:

∏l∈L(r(l)+s(l)+32d≥t)∧(σ≥σ0)∧(f≥t)\prod_{l \in L} \bigg(r(l)+s(l)+\frac 3 2 d\geq t\bigg) \land (\sigma \geq \sigma_0) \land (f \geq t)l∈L∏​(r(l)+s(l)+23​d≥t)∧(σ≥σ0​)∧(f≥t)

r−sr - sr−s, where:

t−t0+w3t - t_0 + \frac w 3t−t0​+3w​, where:

at block start

Virtual stake is a value assigned in case of is true and stake is lower than a

.

If some virtual stake exists, then it’s a

Total stake is a sum of all ever deposited.

Calculated as s+ds+ds+d, where:

t−t0t - t_0t−t0​, where:

Reputation time, that is calculated according to the following formula: sn+d+t−f\frac s n+d+t-fns​+d+t−f, where:

f -

Invoked every time the Root method is called and l+p<t∨n=0l+p<t \lor n=0l+p<t∨n=0, where:

n=0  ⟹  t−ln=0 \implies t-ln=0⟹t−l

n>0  ⟹  πn+t−ln+1n>0\implies \frac{\pi n+t-l}{n+1}n>0⟹n+1πn+t−l​, where 𝜋 - the previous value of reward period

The Average Reputation Coefficient is recalculated in case of changing the .

In case the is zero, it’s assigned to MIN_REP_COEF constant

Otherwise, it’s assigned to a(t−l)+rlt\frac {a(t-l)+rl} {t}ta(t−l)+rl​, where:

t -

l -

r=snr=\frac s nr=ns​, where:

In case the equals to , it’s assigned to MIN_REP_COEF constant

Otherwise, it’s assigned to a−rlt−l\frac {a-rl} {t-l}t−la−rl​, where:

t -

l -

r=snr=\frac s nr=ns​, where:

In case of Epoch starting the following amount is locked: σ(b(λ)−c(λ))∑l∈L(b(l)−c(l))\frac {\sigma(b(\lambda)-c(\lambda))} {\sum_{l \in L}( b(l)-c(l))}∑l∈L​(b(l)−c(l))σ(b(λ)−c(λ))​, where:

In case of repeated Epoch the following amount is locked: σ(b(λ)−c(λ)−e(λ))∑l∈L(b(l)−c(l)−e(l))\frac {\sigma(b(\lambda)-c(\lambda)-e(\lambda))} {\sum_{l \in L}( b(l)-c(l)-e(l))}∑l∈L​(b(l)−c(l)−e(l))σ(b(λ)−c(λ)−e(λ))​, where:

Auxiliary values of each license are changed as described in the

Then, at any moment additional stake request can be received with continue flag, following the logic, where the Epoch repeated instead of PreEpoch creation

Also, at any moment external slash message can be received, and logic is followed

virtual stakes
Number of active blockkeepers
Is_min
minimal Stake
virtual Stake
Local Stakes
Reward adjustment
Number of active blockkeepers
Total Stake
Local Stake
planned Epoch finish time
number of active blockkeepers
Total Stake
Total Stake
Local Stake
Total Stake
Local Stake
Total Stake
Local Stake
corresponding section
Stake Placement
Epoch
Single participation period
Repeated participation
Stake workflow (single participation period)
Stake workflow (repeated participation period)