Skip to main content

2024-03-15

· 2 min read

Present

  • Got results from "split-brain" experiment with 100 nodes that basically confirm the faithfulness of the IOSim implementation and highlights some "interesting" consequences of Peras, namely that when the split-brain heals, it's not the longest chain that wins but the one with the most votes
  • Started work on implementing IOSim node that represents network interactions more faithfully, eg. using a pull model that mirrors the actual ChainSync protocol implemented in the cardano-node
  • Rust node passes the NetworkModel tests, with multiple nodes connected through a netsim-based layer. Aligning the implementations posed some interesting challenges, especially in the domain of time management (real vs. simulated time) and the scheduling of the various "actors" in the system
  • Research shared with engineering a new version of the protocol which introduces Certificates to aggregate votes in the block headers and mostly get rid of the problematic dangling votes concept
  • First meeting with PNSol on ΔQSD modelling of the protocol
  • Meeting with Spyros Voulgaris on Peernet on the topic of network simulator. This is the tool that's used by researchers when they need some numbers.
  • Starting significant redesign of IOSim node to cope with changes in the protocol

Issues

  • We need to improve communication between research and engineering, and how changes are shared and notified

2024-03-08

· One min read

Present

  • Continued work on Rust Peras node to be able to pass the NetworkModel tests. This implies integration with netsim library which is under active development
  • IOSim-based prototype now implements complete validation including tallying votes
  • Started experimentations on modelling Peras using ΔQ methodology, exploring various available libraries

Issues

None

2024-03-01

· 2 min read

Present

  • Quviq SoW has been signed and we had a first meeting with the team, presenting them the current state of the prototype and what our expectations were
  • Refactored Agda specification to support easier proofs of some properties. This rippled over the code base as Agda types representation is our reference
  • First (simple) implementation of a Rust Peras node which passes the peras-quickcheck NodeModel tests, albeit quite slowly
  • More faithful implementation of Peras protocol in peras-iosim including cooldown period
  • Started experimenting with ΔQ modeling and tinkering with existing core repositories
  • First Monthly review presented and recorded
  • Workshop in Paris confirmed, will take place on April 9-10 at the Mobiskill office in the 9th district
  • Started discussion with Consensus team over downstream implementation challenges for Peras
  • Clarified the situation of alternative remediations to finality: They should be addressed directly by the Consensus team as there's no need for Innovation stream to be involved

Future

  • Work on providing some answer to a key question raised by Core tech team: How does Peras will fare when the network load increase from the current 40% to expected 80%?
  • Some secondary questions to answer when it comes to engineer Peras in Cardano:
    1. Can we get rid of counting dangling votes when selecting best chain?
    2. How to deal with the size of votes to diffuse if they are needed for chain selection, given the necessity of header/body split in Cardano?
  • Improve fidelity of the simulation w.r.t. actual network protocol used in Cardano, eg. push vs. pull model
  • Complete Rust node and use netsim library to manage routing between nodes
  • Start more concrete work with PNSol and Quviq on their respective area of expertise

Issues

None

2024-02-16

· One min read

Present

  • We managed to scaffold a "chain of evidence" from Agda model to prototype implementation, gathering knowledge and good intuition in the process on how the various pieces fit together
  • Creative engineering continued work on a Network simulator in Rust, completing FFI so that it can be used in to build a prototype that we can test against
  • Investigation on what's the current state of ΔQ resources and how it could be applied to our problem
  • Quviq SoW still in the hands of Procurement, waiting finalization

Future

  • Quviq SoW signature and execution
  • Implement an IOSim version of Praos/Peras (honest) node, porting existing code from previous experiment
  • Implement a Rust version of Praos/Peras node
  • Demonstrate "evidence trail" on a Peras-related property (selection of heaviest chain by honest nodes?)
  • Engage with PnSol on ΔQ
  • Prepare in 1st monthly demo meeting
  • Organise in-person workshop in Paris, April 9-10

Issues

  • Still unclear what's the situation of alternative remediations for faster settlement proposed during the Edinburgh Peras workshop?

2024-02-09

· 2 min read

Present

  • Started "serious" work with the team on modeling and simulating Peras protocol.
  • Main focus is currently on ensuring all the pieces of the puzzle fit together:
    • Yves is working on the modelisation in Agda of the protocol, leveraging previous work done in Coq on Ouroboros Praos
    • Brian is experimenting with simulation of Praos/Peras in Haskell, with the goal of being able to visualise the evolution of the system over large periods of time and simulating the impact of the protocol parameters
    • Arnaud is exploring model-based testing, towards applying quickcheck-dynamic generated tests on a simulated network of nodes
  • Creative engineering started work on a Network simulator in Rust and we have made some preliminary experiments to connect such a simulator to tests generation process
  • Quviq SoW has been completed and is now in the hands of Procurement to be hopefully finalised in the forthcoming days

Future

  • Quviq SoW signature and execution
  • Continue work on the whole "Simulation process", fitting the various parts together:
    • Express (and prove?) some properties in Agda...
    • ... then generate code from Agda to use in Model-based tests generation and simulations ...
    • ... to run properties against code and produce simulation results.
  • We plan to start recording hosting monthly demos

Issues

  • What's the situation of the alternative remediations for faster settlement proposed during the Edinburgh Peras workshop?
  • Open-sourcing the repository is not desirable while research is still working on the paper