{-# OPTIONS --safe #-}
 
open import Leios.Prelude hiding (id; _⊗_)
 
open import CategoricalCrypto hiding (id; _∘_)
 
open import Blockchain.Safety using (Deployment)
 
import Data.Integer as ℤ
import Data.Rational as ℚ
open ℚ using (ℚ)
 
module Blockchain.Liveness
  (Block : Type)
  (S     : Deployment Block)
  where
 
open Deployment S
 
ℕ→ℚ : ℕ → ℚ
ℕ→ℚ n = (ℤ.+ n) ℚ./ 
 
isHonestBlock : Block → Type
isHonestBlock b = producer b ∈ honest-nodes
 
-- --------------------------------------------------------------------
-- (HCG) Honest Chain Growth
--
-- For every honest block `b` in an honest party's chain, the number
-- of blocks that follow `b` is at least τ · (currentSlot ∸ slotOf b).
 
hcgState : {A : Channel} → ℚ → (E : Environment A) → Machine.State (protocol E) → Type
hcgState τ E S₀ =
    {p : Fin n} (hp : p ∈ honest-nodes)
    {pref suff : List Block} {b : Block}
  → getChain E S₀ hp ≡ pref ++ (b ∷ suff)
  → isHonestBlock b
  → τ ℚ.* ℕ→ℚ (getSlot E S₀ hp ∸ slotOf b) ℚ.≤ ℕ→ℚ (length suff)
 
hcg : ℚ → Type₁
hcg τ = ∀ {A} (E : Environment A) → Invariant (protocol E) (hcgState τ E)
 
-- --------------------------------------------------------------------
-- (∃CQ) Existential Chain Quality
--
-- In every honest party's chain, the suffix of blocks whose slot is
-- within the last T slots contains at least one honest block.
 
recent : ℕ → ℕ → List Block → List Block
recent T s = filter (λ b → slotOf b + T ≥ s)
 
∃cqState : {A : Channel} → ℕ → (E : Environment A) → Machine.State (protocol E) → Type
∃cqState T E S₀ =
    {p : Fin n} (hp : p ∈ honest-nodes)
  → Any.Any isHonestBlock (recent T (getSlot E S₀ hp) (getChain E S₀ hp))
 
∃cq : ℕ → Type₁
∃cq T = ∀ {A} (E : Environment A) → Invariant (protocol E) (∃cqState T E)