Skip to main content

Weekly Summary – March 3, 2025

· 2 min read
William Wolff
Architect

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

Programming and testing

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.