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

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

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?

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

Present​

• Brian Bush is definitely joining the team, as is Yves Hauser in the capacity of Formal Method engineer
  • Yves has already done some work in modeling network performance and already started learning Agda within the Marlowe team
• Artjoms Sinkarovs passed on our hiring proposal and accepted another offer
• David Rosales has been appointed as Head of Delivery for Innovation projects and he’s been updated on the current status of Peras
• Writing a SoW with Quviq to involve them as consultants for our Model-Based Testing approach to specifying protocol and verifying implementation

Future​

• Complete Quviq’s SoW and file a ticket with Flow Office and Procurement to be able to start working with them officially
• Organise an in-person workshop
  • Targeting the week of April 8th, somewhere in Europe (Edinburgh? Zurich? Paris?)
• Complete PI5 Planning process
• Start regular working sessions with the team