3 posts tagged with "agda"

This week, the Leios team focused on improving simulation capabilities, enhancing transaction processing, and expanding the test coverage. The team also made significant progress in addressing transaction inclusion rates and developing a comprehensive conformance testing framework.

Simulation improvements​

Rust simulation​

• Investigated and addressed poor transaction inclusion rates
• Implemented 'late IB inclusion' extension to Full Leios, significantly improving transaction ledger inclusion odds
• Identified and addressed issues with non-sharded input transactions causing excessive duplication
• Made several key enhancements:
  • Enabled late IB inclusion by default
  • Fixed the off-by-one error in late IB inclusion logic
  • Added praos-fallback-enabled setting for throughput investigation
  • Improved transaction deduplication in Praos blocks.

Testing framework​

Conformance testing​

• Developed a comprehensive catalog of potential conformance tests
• Implemented a property-based testing suite for trace verification
• Added both positive and negative test cases covering:
  • Genesis slot operations
  • Block production (RB, IB, EB)
  • Vote generation
  • Various production patterns (sporadic, noisy)
  • Invalid scenarios (equivocation, gaps)
• Successfully verified golden traces against the Agda specification.

Documentation​

Formal specification​

• Launched comprehensive web-based documentation for the Ouroboros Leios formal specification at leios.cardano-scaling.org/formal-spec
• Enhanced documentation features:
  • Interactive exploration of Leios modules
  • Type linking between related components
  • Full text search capabilities
  • Improved accessibility of formal specification details.

Transaction lifecycle analysis​

• Conducted detailed analysis of transaction processing efficiency
• Generated a cumulative probability model for transaction ledger inclusion
• Analyzed the relationship between IB production rate and stage length
• Created visualization of transaction-to-block inclusion probabilities.

Next steps​

• Continue monitoring and optimizing transaction inclusion rates
• Expand conformance test coverage as the Agda specification evolves
• Further investigate transaction sharding strategies
• Refine transaction lifecycle model based on simulation results.

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.