{-# OPTIONS --safe #-}
 
{- Module: 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)
 
StakeDistr : Type
StakeDistr = TotalMap PoolID ℕ
 
RankingBlock : Type
RankingBlock = These EndorserBlock (List Tx)
 
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'))
 
    open Input public
    open Output public