Leios.Base

This module defines core components for the base layer of Leios protocol. It includes stake distribution, ranking blocks, and base layer abstractions.

open import Leios.Prelude
open import Leios.Abstract
open import Leios.VRF
 
module Leios.Base (a : LeiosAbstract) (open LeiosAbstract a) (vrf' : LeiosVRF a)
  (let open LeiosVRF vrf') where
 
open import Leios.Blocks a using (EndorserBlock; EBRef)
 
StakeDistr : Type
StakeDistr = TotalMap PoolID ℕ
 
record RankingBlock : Type where
  field txs : List Tx
        announcedEB : Maybe Hash
        ebCert : Maybe EBCert
 
record BaseAbstract : Type₁ where
  field Cert : Type
        VTy : Type
        initSlot : VTy → ℕ
        V-chkCerts : List PubKey → EndorserBlock × Cert → Bool

        
      

Input data type represents the possible inputs to the base layer functionality.

The base layer can receive three types of inputs: - Initialization with a certificate validation function - Submission of ranking blocks for processing - Requests to fetch the current ledger state

  data Input : Type where

        
      

INIT: Initialize the base layer with a certificate validation function.

Parameters: - (EndorserBlock × Cert → Bool): A validation function that checks whether an endorser block and certificate pair is valid. Returns True if the pair is valid, False otherwise.

    INIT   : (EndorserBlock × Cert → Bool) → Input

        
      

SUBMIT: Submit a ranking block to the base layer for processing.

Parameters: - RankingBlock: A ranking block containing either an endorser block, a list of transactions, or both (using the These type constructor). This represents new content to be added to the ledger.

    SUBMIT : RankingBlock → Input

        
      

FTCH-LDG: Request to fetch the current ledger state.

This input has no parameters and is used to query the current state of the base layer ledger.

    FTCH-LDG : Input

        
      

Output data type represents the possible outputs from the base layer functionality.

The base layer can produce three types of outputs: - Stake distribution information - Empty response (no meaningful output) - Base layer ledger contents

  data Output : Type where

        
      

STAKE: Output containing the current stake distribution.

Parameters: - StakeDistr: A total map from pool identifiers to their stake amounts (ℕ). This represents how stake is distributed across different pools in the system.

    STAKE : StakeDistr → Output

        
      

EMPTY: Empty output indicating no meaningful result.

This output is used when an operation completes successfully but produces no data that needs to be returned to the caller.

    EMPTY : Output

        
      

BASE-LDG: Output containing the base layer ledger contents.

Parameters: - List RankingBlock: A list of ranking blocks that constitute the current state of the base layer ledger. Each ranking block may contain endorser blocks, transactions, or both.

    BASE-LDG : List RankingBlock → Output

        
      

  record Functionality : Type₁ where
    field State : Type
          _-⟦_/_⟧⇀_ : State → Input → Output → State → Type
          SUBMIT-total : ∀ {s b} → ∃[ s' ] s -⟦ SUBMIT b / EMPTY ⟧⇀ s'
          FTCH-total : ∀ {s} → ∃[ r ] (∃[ s' ] (s -⟦ FTCH-LDG / BASE-LDG r ⟧⇀ s'))
          -- FTCH-unique : ∀ {s s' o} → s -⟦ FTCH-LDG / o ⟧⇀ s' → ∃[ r ] o ≡ BASE-LDG r
 
    open Input public
    open Output public