This week in Leios development, the team focused on simulation analysis, formal methods, and documentation updates. Key accomplishments include in-depth analysis of simulations at tag leios-2025w10, advancements in formal methods through a working trace verifier, and the development of technical reports.

Cross-simulation analysis​

• Completed a comprehensive analysis of simulations at tag leios-2025w10:
  • Analyzed Haskell simulation performance with and without CPU usage considerations
  • Varying key protocol parameters:
    • IB production rate
    • IB size
    • Length of Leios stages
  • Identified the following aspects of Leios:
    • Delay between IB generation and receipt at nodes
    • Peak and mean CPU usage over time
    • Breakdown of CPU usage by task type
    • Sizes of IBs, EBs, and RBs
    • Duplicate IB references in EBs
    • Reference to EBs from RBs
    • Resource utilization in network traffic.

Protocol and formal methods​

• Began developing a trace verifier in Agda:
  • Implemented event trace parsing using the Haskell module leios-trace-hs.

Documentation and research​

• Completed the full draft of the Leios technical report #1
• Created a skeletal draft of the Leios CIP
• Aligned with the latest CIP template
• Developed a detailed simulation analysis for the 100-node Leios network.

Programming and testing​

• Resolved several simulation issues:
  • #235: RB size does not reflect the presence of a certificate
  • #234: Fast transmission of large blocks at moderate IB rate
  • #232: Monotonicity of EB inclusion in RBs
  • #230: EBs are not large enough to include their IBs
  • #229: Rust simulations panics from overflow
• Enabled the visualization of network traffic and logging messages for multiple predefined 'scenarios' instead of a single hard-coded trace
• Updated the visualization to display resource utilization in network traffic.

Rust simulation visualization​

• Improved visualization capabilities:
  • Added support for multiple predefined 'scenarios' instead of single hard-coded trace
  • Moved the visualization logic to the client-side web worker for better performance
  • Added the visualization of per-node network traffic breakdown by message type
• Fixed critical simulation bugs:
  • Resolved issue #229 causing time travel and crashes in high-traffic high-latency scenarios.

This week in Leios development, the team focused on simulation analysis and formal methods. Key accomplishments include detailed analyses of both Haskell and Rust simulations, initial work on a protocol dashboard, and advancements in formal methods through trace verification in Agda.

Cross-simulation analysis​

• Completed a comprehensive analysis of simulations at tag leios-2025w09:
  • Refactored the ELT workflow to improve simulation data processing
  • Modified the Rust simulator to generate fixed-size input blocks (IBs) for comparison with Haskell
  • Partially resolved discrepancies in congestion metrics between simulators
  • Developed detailed analyses of:
    • IB generation to receipt elapsed time
    • Time-in-flight over node-to-node links
  • Identified the dual role of network bandwidth and CPU bottlenecks in high throughput congestion.

Protocol dashboard initiative​

• Initiated the design of an interactive protocol dashboard with planned features:
  • Protocol parameter configuration
  • Stake distribution settings
  • Performance visualization:
    • Block arrival efficiency
    • Transaction duplication
    • Leios operation rewards
    • Resource utilization
  • Security metrics visualization:
    • Quorum failure analysis
    • Certificate forgery detection
    • Adversarial block tracking.

Rust simulation​

• Enhanced parallel message handling capabilities:
  • Implemented parallel mini-protocol message transmission
  • Added even bandwidth distribution between mini-protocols
  • Introduced the simulate-transactions configuration option
  • Updated simulation output for better Haskell compatibility
  • Improved block visualization for scenarios with high IB counts.

Formal methods​

• Commenced trace verifier development in Agda:
  • Added decidability to Short Leios protocol relational specification
  • Implemented a proof-by-computation approach for execution traces
  • Applied the successful methodology from Streamlet formalization.

This week in Leios development, CPS-0018 for transaction throughput was approved, along with improved Docker support for simulations and analysis of cross-simulation results. The team also examined input block (IB) production rates and their impact on network performance.

Protocol development​

• CPS-0018 'Greater transaction throughput' officially approved:
  • Merged into Cardano Foundation's CIP/CPS repository
  • Documents urgency of higher transaction throughput
  • Defines goals for the Leios initiative
  • Identifies key open questions and use cases.

Cross-simulation analysis​

• Conducted a comprehensive analysis of IB production rates ranging from 1 IB/s to 100 IB/s:
  • Developed an ELT workflow for data processing via MongoDB
  • Created an R Jupyter notebook for analysis and visualization
  • Identified and addressed three significant bugs (#207, #208, #209)
• Key findings from the Haskell simulation:
  • Network congestion emerges at high IB production rates
  • Both average propagation time and slow propagation tail increase
  • A critical threshold of ~40 IBs/s was identified, beyond which network congestion severely impacts block reception
• Comparison of PeerNet and Haskell simulations:
  • Both exhibit qualitatively similar block propagation distributions
  • Both demonstrate protocol breakdown under high block production rates
  • Differences in resolution and configuration prevent exact comparison.

Infrastructure improvements​

• Added comprehensive Docker support for both simulations:
  • Optimized multi-stage Docker files for Haskell and Rust
  • Simplified deployment process
  • Enabled easy configuration via volume mounts and parameters
  • Documented usage in README.md.

Rust simulation​

• Enhanced Rust simulation capabilities:
  • Implemented bandwidth usage tracking
  • Added configurable bandwidth limits per connection
  • Fixed issues identified in cross-simulation comparisons
  • Started updating visualizations for improved clarity.

Haskell simulation​

• Enhanced IB sortition handling for IB/slot < 1
• Began integrating block expiration and diffusion-halt proposal
• Implemented ideal timing calculations for diffusion:
  • Added uniform block behavior configuration
  • Identified relay mini-protocol complexities:
    • Variable latency (3-4) for block transfer
    • Latency depends on traffic conditions and request handling.

Formal methods​

• Moved formal specification to a dedicated repository
• Established a conformance testing framework:
  • Enabled testing between Short Leios implementations
  • Documented the test suite execution process
• Initiated a survey of network models across IO consensus projects.

This week, the Leios team made significant progress across multiple areas. Major developments included detailed DeltaQ analysis of network topologies, extensive BLS cryptography benchmarking, and improvements to both simulations. The team also explored succinct schemes for BLS key registration and conducted a detailed certificate performance analysis. Both Haskell and Rust simulations received substantial updates to improve visualization and support more realistic testing conditions.

DeltaQ analysis​

• Enhanced the topology-checker with ΔQSD analysis capabilities:
  • Extracts inter-node latencies from given topologies
  • Classifies latencies into near/far components
  • Builds parameterized ΔQ models
  • Outputs fitted models in delta_q web app syntax
• Key findings from topology analysis:
  • Clear distinction between near/far components in examined topologies
  • Unexpectedly high hop counts in latency-weighted Dijkstra paths:
    • Min 4-5, max 8 for topology - 100
    • Min 8, max 20 for 'realistic' topology
  • Model fitting achieved rough shape matching but showed significant deviations at low latencies
  • Resource usage tracking goals remain unmet due to complexity in understanding load multiplication factors.

BLS cryptography​

• Completed comprehensive benchmarking of certificate operations:
  • Detailed performance analysis across committee sizes (500-1000 seats)
  • Certificate generation: 63.4ms - 92.5ms
  • Certificate verification: 104.8ms - 144.9ms
  • Certificate weighing: ~12ms consistently
• Explored succinct schemes for key registration:
  • Proposed 90-day key evolution with 124-byte KZG commitments
  • Analyzed message sizes for key opening (316 bytes per pool)
  • Investigated SNARK-based alternatives for proof of possession
• Added BLS crypto to the CI pipeline with automated testing
• Documented parallelization strategies for certificate operations.

Formal methods​

• Added a conformance testing client for the executable Short Leios specification
• Successfully merged the executable specification for Simplified Leios into main.

Haskell simulation​

• Updated configuration defaults for block sizes and timings
• Added support for idealized simulation conditions:
  • Single-peer block body requests
  • TCP congestion window modeling
  • Mini-protocol multiplexing
  • Unlimited bandwidth links support
• Enhanced simulation output and analysis:
  • Added raw field for accumulated data
  • Implemented block diffusion CDF extraction
  • Created multi-CDF plotting capabilities.

Rust simulation​

• Enhanced visualization capabilities:
  • Added block size breakdown display
  • Implemented total bytes sent/received tracking
  • Added total TX count and CPU time metrics
• Improved event handling:
  • Updated to standard timestamp format (seconds)
  • Enhanced CPU task event structure
  • Added CBOR output support
• Added support for multiple strategies:
  • Implemented ib-diffusion-strategy (freshest-first, oldest-first, peer-order)
  • Added relay-strategy affecting TXs, IBs, EBs, votes, and RBs
  • Enabled unlimited EB and vote bundle downloads from peers.

This week, the Leios team worked on cryptography benchmarking and cost calculator improvements. The team completed a reference implementation for Leios cryptography and enhanced the online cost calculator with user-requested features. They also updated both Haskell and Rust simulations to improve visualization and network modeling capabilities.

Haskell simulation​

• Added support for Send and Receive voting stages, providing:
  • A new leios-vote-send-recv-stages configuration option
  • A configurable stage length via leios-stage-active-voting-slots
• Implemented multiple diffusion strategies:
  • Added oldest-first strategy
  • Added configurable strategies for IBs, EBs, and votes via *-diffusion-strategy configurations
• Created a new small scenario for 100 nodes with 2,000 kB links
  • Tuned IB parameters to utilize one-third of link capacity
  • Added configurations for both single-stage and send-recv voting
• Fixed several simulation behaviors:
  • Improved block generation logic
  • Prevented duplicate EB inclusion in the base chain
  • Confirmed proper EB inclusion timing relative to vote diffusion
• The main difference observed between single-stage and send-recv is that the former shows a longer tail in the CPU usage CDF when the simulation is run with unlimited cores.

Cryptography implementation​

The Rust benchmarks for Leios cryptography were redesigned as a reference implementation:

• Implemented the Fait Accompli sortition
• Enhanced sortition to use rational arithmetic instead of quad-precision floats
• Added Quickcheck tests for all capabilities
• Added benchmarks for serialization
• Optimized vote and certificate size.

Cost calculator improvements​

The team enhanced the online Leios cost calculator:

• Added support for both hyperscale and discount cloud providers
• Made discount providers the default option
• Added option to amortize storage costs perpetually
• Updated defaults:
  • Single relay deployment
  • More conservative 50% disk compression
  • Perpetual storage cost amortization.

Throughput simulator​

The team updated the Cardano throughput simulator with:

• The latest cloud-computing cost model
• Synchronized assumptions with an online cost calculator.

Rust simulation​

• Made minor fixes to the new graph generation strategy
• Planned out a roadmap for visualization work focusing on the Leios transaction lifecycle.

The Leios team continued refining Haskell and Rust simulations, standardizing inputs, outputs, and event logging for better comparability. The team defined standard formats for configuration parameters and network topology for running the Leios protocol. They also worked on logging identical simulation events to compare and feed them into the DeltaQ model and, consequently, the executable specification, ensuring alignment with formal methods.

Haskell simulation updates​

• The short-leios simulation now outputs diffusion latency data
• Added support for different input block (IB) diffusion strategies:
  • freshest-first: higher slot numbers requested first
  • peer-order: requested in order of peer announcement
• Added support for Vote (Send) and Vote (Recv) stages.

Rust simulation progress​

• Added an 'organic' topology generator that better matches mainnet topology
• The generator creates clusters of colocated stake pools and relays
• The simulation uses stake to determine relay connectivity
• Topology insights gathered from stake pool owners:
  • Most pools have multiple relays (2,312 relays across 1,278 pools)
  • Pool operators often run multiple colocated pools sharing relays
  • Relays typically maintain ~25 active outgoing connections
  • Incoming connections scale with stake weight (10-400+ connections).

DeltaQ update​

• Wrote a comprehensive 2025-01 report covering work since September 2024.

Formal methods​

• Finalizing executable specifications for simplified and short Leios
• Extracted short Leios specification to Haskell for conformance testing.

Simulation progress​

Haskell implementation​

• Enhanced parameter handling with support for reading configurations and topologies from disk
• Added a new generate-topology command for random topology generation
• Aligned Leios sortition with algorithms from sortition benchmarks and the technical report
• Completed analysis comparing the Praos simulation with the benchmark cluster
  • Adoption times within 10% of measured values
  • Review of simulation parameters pending
• Next steps identified:
  • Generate topologies with block producers behind relays
  • Begin comparison with the idealized diffusion model
  • Configure and run simulations for higher throughput.

Rust implementation​

• Completed the first pass of block-level visualization
• Updated topology files to include baked-in latencies
• Improved output with human-readable names from the shared topology format
• Enhanced simulation output comparability across different simulations.

Analysis and research​

Sortition analysis​

• Completed a detailed analysis of the 'Fiat Accompli' sortition scheme using mainnet stake distribution (Epoch 535)
• Key findings for 500-vote committees:
  • 406 largest stake block-producers would be deterministic voters
  • ~88 voters would be randomly selected
  • Significant certificate size reduction achieved through deterministic voter selection.

Downstream impact assessment​

Started comprehensive analysis of Leios's impact on the ecosystem:

• Identified impacts on indexers, explorers, SDKs, and APIs resulting from ledger and node changes
• Transaction construction and memory-pool sharding effects on DApps and wallets
• Physical layer visibility considerations for sophisticated use cases
• High throughput implications for event filtering efficiency
• Transaction journey time considerations from memory pool to Praos block reference.

DeltaQ analysis​

• Successfully matched ΔQ model for IB diffusion across both simulations and implementations
• Identified key differences in simulation approaches:
  • Haskell simulation includes bandwidth effects (328ms network delay per hop at 1MB/s)
  • Rust simulation currently excludes bandwidth effects
• Enabled cross-simulation topology sharing for consistent testing.

Cryptography benchmarks​

• Implemented and benchmarked the complete Leios cryptography suite in the leios_crypto_benchmarks Rust crate
• Key VRF performance metrics:
  • Proving: 240 µs
  • Verifying: 390 µs
• Sortition performance (excluding VRF):
  • Leadership checks (RB/IB/EB): 0.17 µs per slot/pipeline
  • Vote number calculation: 3.8 µs per pipeline
• BLS operations benchmarked:
  • Key possession proof verification: 1.5 ms per key
  • Vote generation/verification: 280 µs / 1.4 ms per vote
  • Certificate operations (300-vote quorum): 50 ms generation, 90 ms verification.

Cryptography design progress​

• Optimized vote signature size to potentially as small as 192 bytes
• Determined that 500-vote committee certificates (60% quorum) would fit within Praos blocks at ~58 kB
• Explored potential synergies with KES rotation and Praos VRF BLS keys
• Completed cryptography sections for the first technical report
• Decision made to freeze current report content and move new findings to future documents.

Simulation development​

Haskell simulation​

• Achieved diffusion latency comparable to benchmark cluster data for Praos blocks
• Integrated agreed-upon simulation parameters with the Rust team
• Added event log output functionality with JSON support
• Implemented 'short-leios' simulation variant matching mainnet ranking block interval
• Fixed coordination issues in Relay mini-protocol consumers
• Completed the PI goal by adding total data transmitted per node visualization.

Rust simulation​

• Implemented more granular CPU simulation times
• Fixed race condition in the simulated clock
• Started consuming a new shared configuration file format
• Established a shared configuration format with default parameters in data/simulation/default.yaml.

Rust simulation​

• Added a basic simulation of central processing unit (CPU) usage/latency
• Implemented 'lottery won' events to identify the start of CPU processing
• Configured each node with four simulated cores, adjustable per node
• Transaction validation and ranking block/input block/endorser block generation/validation each take one CPU task
• All virtual CPU costs were copied from the cost estimator.

DeltaQ summary update​

• Added MIN/MAX combinators for best- and worst-case simulation results
• The Rust simulation best case does not match the analytically best behavior
• The Haskell simulation best case is too fast; the ΔQ expression must assume more than 200 peers per node.

Cost dashboard updates​

• Improved input parameters and computations
• Lengthened phases and reduced endorser block rate
• Updated CPU costs for votes and certificates
• Revised input/output operations per second (IOPS) values based on empirical data from Cardano nodes.

Benchmarking BLS signatures​

• Benchmarked BLS votes using the Rust bls-signatures package
• Aggregate verification significantly speeds up the process
• Provided CPU time estimates for various operations.

Votes and certificates​

• Updated size estimates for votes
• Added CPU time estimates for BLS votes and certificates
• Drafted technical report sections on BLS and MUSEN certificates.

Sortition analysis​

• Analyzed sortition for input and endorser blocks and votes
• Added findings to the draft of the first technical report.

Rust simulation​

• Abandoned Waxman graph generation favoring a more straightforward distance-weighted approach to better control graph connectivity.

Haskell simulation​

• Added support for bounded and unbounded parallelism to the Leios node
• Fixed relay protocol messages to ensure ordered delivery
• Next steps include loading protocol configuration from disk and investigating endorser block (EB) inclusion rates.

Revised analysis of votes and certificates​

• Continued research on cryptographic options for Leios votes and certificates
• BLS was identified as the most viable option.

Jupyter support for DeltaQ​

• Introduced new high-performance Haskell packages for DeltaQ with comprehensive test suites.