Merge branch 'main' of github.com:input-output-hk/ouroboros-leios int…

…o feat/large-data

.vscode/settings.json

@@ -3,5 +3,6 @@
     "source.fixAll.eslint": "always",
     "source.organizeImports": "explicit",
   },
-  "editor.formatOnSave": true, // Disable default formatter if ESLint is handling formatting
+  "editor.formatOnSave": true,
+  "haskell.formattingProvider": "fourmolu", // Disable default formatter if ESLint is handling formatting
 }

Logbook.md

@@ -1,5 +1,82 @@
 # Leios logbook
 
+## 2024-11-22
+
+### Haskell simulation
+
+- Relay protocol works as expected when reading messages from a single
+  thread, sufficient workaround atm but would be good to investigate
+  in future.
+- Fixed inaccuracy in praos simulation where it was possible for a
+  block to validate without having validated the previous one.  The
+  fix also allows for validation to happen via a dedicated queue.
+- Defined "business logic" of (Uniform) Short Leios, referencing the
+  most recent draft.
+- Used relay protocols to define a node for Leios, extending the one
+  we had for Praos. Validation delays still missing atm.
+
+### Formal specification
+
+- More generic design to support Leios variants
+- Added the specification for Uniform Short Leios
+- A new data type that allows building execution paths
+- Initial work to make the relational specification executable
+
+## 2024-11-21
+
+Market data that compares Cardano `mainnet` to other prominent blockchain's throughput was added to the [Transaction Throughput CPS](https://github.com/cardano-scaling/CIPs/pull/5).
+
+### Rust simulation
+
+Visualization: We're able to animate a network of 3000 nodes with 100x mainnet transaction volume, running at about 1/10th speed. Using server-side events to cope with scale looks fast enough, but we haven't wired it up yet.
+
+Simulation: Implemented generation and distribution of votes. Because of the sheer number of votes needed by the protocol, voting involves sending an order of magnitude more messages than anything else, regardless of the transaction volume running through the system. We now need to run the sim at 1/32 of realtime for accurate results.
+
+When simulating 1000x current mainnet transaction volume for 30 seconds:
+112750061 TX message(s) were sent. 112619569 of them were received (99.884%).
+140953 IB message(s) were sent. 140953 of them were received (100.000%).
+917595 EB message(s) were sent. 917595 of them were received (100.000%).
+355863732 Vote message(s) were sent. 355863732 of them were received (100.000%).
+
+We also need a more accurate stake distribution. The current model just assumes it's uniformly distributed, but only a minority of nodes get a vote (~500 of the ~2500 mainnet stake pools) and we (presumably?) need a majority of stake attached to that vote.
+
+## 2024-11-20
+
+### Model of Cardano throughput
+
+The system-dynamics simulation of Cardano throughput was enhanced and checked.
+
+- Documented all variables.
+- Adjusted slider ranges.
+- Added constraint for valid ranges of variables.
+- Tested scenarios.
+- Checked equations.
+- Fixed extreme scenario were funds flow into reserve.
+- Created [tutorial video](https://drive.google.com/file/d/1YrQLLsgsPt4XHa707c-CfTLkivKRyaa0/view?usp=sharing)
+- Published [version 0.2](https://www.insightmaker.com/insight/5B3Sq5gsrcGzTD11GyZJ0u/Cardano-Throughput-v0-2) of the model.
+
+## 2024-11-19
+
+### Rust simulation
+
+Visualization: More work on streaming, and direct canvas rendering for best performance. There's still too much data to send to the UI at once, and we want to be able to filter "live" for better UX.
+
+## 2024-11-18
+
+### Rust simulation
+
+Visualization: Working on streaming events from a server to the UI for better performance. 
+
+### Items of interest from Intersect Network WG
+
+- Many SPOs have a hot backup of their block producer running.
+- Relays actually have more than 200 downstream p2p connections.
+    - For example, the IOG ones have ~500 downstream peers.
+
+### Rust simulation
+
+Started work on visualizing simulation against a full-sized network. Unsurprisingly, there is too much data to render straightforwardly we will probably prioritize "zooming in" on a small part of the sim and visualizing that.
+
 ## 2024-11-15
 
 ### Analysis of Leios challenges, part 1

formal-spec/Class/Computational22.agda

@@ -0,0 +1,35 @@
+{-# OPTIONS --safe #-}
+
+--------------------------------------------------------------------------------
+-- Variant of `Computational` for relations with two inputs and outputs
+--------------------------------------------------------------------------------
+
+module Class.Computational22 where
+
+open import Leios.Prelude
+open import Class.Computational
+
+private variable
+  S I O Err : Type
+
+module _ (STS : S → I → O → S → Type) where
+  record Computational22 Err : Type₁ where
+    constructor MkComputational
+    field
+      computeProof : (s : S) (i : I) → ComputationResult Err (∃[ (o , s') ] STS s i o s')
+
+    compute : S → I → ComputationResult Err (O × S)
+    compute s i = map proj₁ $ computeProof s i
+
+    field
+      completeness : ∀ s i o s' → STS s i o s' → compute s i ≡ success (o , s')
+
+  STS' : S × I → O × S → Type
+  STS' (s , i) (o , s') = STS s i o s'
+
+  module _ ⦃ _ : Computational22 Err ⦄ where
+    open Computational22 it
+    instance
+      comp22⇒comp : Computational STS' Err
+      comp22⇒comp .Computational.computeProof (s , i)          = computeProof s i
+      comp22⇒comp .Computational.completeness (s , i) (o , s') = completeness s i o s'

formal-spec/Everything.agda

@@ -2,5 +2,6 @@
 
 module Everything where
 
-open import Leios.SimpleSpec
+open import Leios.Simplified
+open import Leios.UniformShort
 open import Leios.Network

formal-spec/Leios/Abstract.agda

@@ -14,5 +14,5 @@ record LeiosAbstract : Type₁ where
         vote : PrivKey → Hash → Vote
         sign : PrivKey → Hash → Sig
         ⦃ Hashable-Txs ⦄ : Hashable (List Tx) Hash
-        L Λ μ : ℕ
+        L : ℕ
         ⦃ NonZero-L ⦄ : NonZero L

formal-spec/Leios/Prelude.agda

@@ -11,9 +11,18 @@ open import Class.HasOrder public
 open import Class.Hashable public
 open import Prelude.InferenceRules public
 
+import Data.List as L
+
 fromTo : ℕ → ℕ → List ℕ
 fromTo m n = map (_+ m) (upTo (n ∸ m))
 
 slice : (L : ℕ) → ⦃ NonZero L ⦄ → ℕ → ℕ → ℙ ℕ
 slice L s x = fromList (fromTo s' (s' + (L ∸ 1)))
   where s' = ((s / L) ∸ x) * L -- equivalent to the formula in the paper
+
+filter : {A : Set} → (P : A → Type) ⦃ _ : P ⁇¹ ⦄ → List A → List A
+filter P = L.filter ¿ P ¿¹
+
+instance
+  IsSet-List : {A : Set} → IsSet (List A) A
+  IsSet-List .toSet A = fromList A

formal-spec/Leios/Protocol.agda

@@ -0,0 +1,136 @@
+{-# OPTIONS --safe #-}
+
+open import Leios.Prelude hiding (id)
+open import Leios.FFD
+
+import Data.List as L
+import Data.List.Relation.Unary.Any as A
+
+open import Leios.SpecStructure
+
+module Leios.Protocol (⋯ : SpecStructure) (let open SpecStructure ⋯) (SlotUpkeep : Type) where
+
+open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot)
+open GenFFD
+
+-- High level structure:
+
+
+--                                      (simple) Leios
+--                                        /         |
+-- +-------------------------------------+          |
+-- | Header Diffusion     Body Diffusion |          |
+-- +-------------------------------------+       Base Protocol
+--                                        \      /
+--                                        Network
+
+data LeiosInput : Type where
+  INIT     : VTy → LeiosInput
+  SUBMIT   : EndorserBlock ⊎ List Tx → LeiosInput
+  SLOT     : LeiosInput
+  FTCH-LDG : LeiosInput
+
+data LeiosOutput : Type where
+  FTCH-LDG : List Tx → LeiosOutput
+  EMPTY    : LeiosOutput
+
+record LeiosState : Type where
+  field V         : VTy
+        SD        : StakeDistr
+        FFDState  : FFD.State
+        Ledger    : List Tx
+        ToPropose : List Tx
+        IBs       : List InputBlock
+        EBs       : List EndorserBlock
+        Vs        : List (List Vote)
+        slot      : ℕ
+        IBHeaders : List IBHeader
+        IBBodies  : List IBBody
+        Upkeep    : ℙ SlotUpkeep
+        BaseState : B.State
+
+  lookupEB : EBRef → Maybe EndorserBlock
+  lookupEB r = find (λ b → getEBRef b ≟ r) EBs
+
+  lookupIB : IBRef → Maybe InputBlock
+  lookupIB r = find (λ b → getIBRef b ≟ r) IBs
+
+  lookupTxs : EndorserBlock → List Tx
+  lookupTxs eb = do
+    eb′ ← mapMaybe lookupEB $ ebRefs eb
+    ib  ← mapMaybe lookupIB $ ibRefs eb′
+    txs $ body ib
+    where open EndorserBlockOSig
+          open IBBody
+          open InputBlock
+
+  constructLedger : List EndorserBlock → List Tx
+  constructLedger = concatMap lookupTxs
+
+  needsUpkeep : SlotUpkeep → Set
+  needsUpkeep = _∉ Upkeep
+
+addUpkeep : LeiosState → SlotUpkeep → LeiosState
+addUpkeep s u = let open LeiosState s in record s { Upkeep = Upkeep ∪ ❴ u ❵ }
+
+initLeiosState : VTy → StakeDistr → B.State → LeiosState
+initLeiosState V SD bs = record
+  { V           = V
+  ; SD          = SD
+  ; FFDState    = FFD.initFFDState
+  ; Ledger      = []
+  ; ToPropose   = []
+  ; IBs         = []
+  ; EBs         = []
+  ; Vs          = []
+  ; slot        = initSlot V
+  ; IBHeaders   = []
+  ; IBBodies    = []
+  ; Upkeep      = ∅
+  ; BaseState   = bs
+  }
+
+-- some predicates about EBs
+module _ (s : LeiosState) (eb : EndorserBlock) where
+  open EndorserBlockOSig eb
+  open LeiosState s
+
+  allIBRefsKnown : Type
+  allIBRefsKnown = ∀[ ref ∈ fromList ibRefs ] ref ∈ˡ map getIBRef IBs
+
+stake : LeiosState → ℕ
+stake record { SD = SD } = case lookupᵐ? SD id of λ where
+  (just s) → s
+  nothing  → 0
+
+module _ (s : LeiosState) where
+
+  open LeiosState s
+
+  upd : Header ⊎ Body → LeiosState
+  upd (inj₁ (ebHeader eb)) = record s { EBs = eb ∷ EBs }
+  upd (inj₁ (vHeader vs)) = record s { Vs = vs ∷ Vs }
+  upd (inj₁ (ibHeader h)) with A.any? (matchIB? h) IBBodies
+  ... | yes p =
+    record s
+      { IBs = record { header = h ; body = A.lookup p } ∷ IBs
+      ; IBBodies = IBBodies A.─ p
+      }
+  ... | no _ =
+    record s
+      { IBHeaders = h ∷ IBHeaders
+      }
+  upd (inj₂ (ibBody b)) with A.any? (flip matchIB? b) IBHeaders
+  ... | yes p =
+    record s
+      { IBs = record { header = A.lookup p ; body = b } ∷ IBs
+      ; IBHeaders = IBHeaders A.─ p
+      }
+  ... | no _ =
+    record s
+      { IBBodies = b ∷ IBBodies
+      }
+
+infix 25 _↑_
+_↑_ : LeiosState → List (Header ⊎ Body) → LeiosState
+_↑_ = foldr (flip upd)