GRANDPA formal verification grant proposal

[AltiMario]

Project Abstract

This application is in response to the RFP "Formal Guarantees for GRANDPA Finality Gadget"

Grant level

• Level 1: Up to $10,000, 2 approvals
• Level 2: Up to $30,000, 3 approvals
• [x ] Level 3: Unlimited, 5 approvals (for >$100k: Web3 Foundation Council approval)

Application Checklist

• The application template has been copied and aptly renamed (grandpa_verification.md).
• I have read the application guidelines.
• Payment details have been provided (bank details via email or Polkadot (USDC & USDT) address in the application).
• I am aware that, in order to receive a grant, I (and the entity I represent) have to successfully complete a KYC/KYB check.
• The software delivered for this grant will be released under an open-source license specified in the application.
• The initial PR contains only one commit (squash and force-push if needed).
• The grant will only be announced once the first milestone has been accepted (see the announcement guidelines).
• I prefer the discussion of this application to take place in a private Element/Matrix channel. My username is: @_______:matrix.org (change the homeserver if you use a different one)

[semuelle]

Hi @AltiMario, nice to see interest in this RFP. However, we usually only sign one grant at a time for any team. We can leave this open until a decision is made on the other one, but if you prefer this one over the other, then we should close the first one.

[AltiMario]

Hi @semuelle I added this note https://github.com/AltiMario/Grants-Program/blob/grandpa-formal-verification/applications/grandpa_verification.md#additional-information-heavy_plus_sign hoping for a not restrictive policy.
Unfortunately, I cannot pause the previous one because it is already been delayed due to a paperwork issue.
However, if you begin the review process by sharing your expectations and requirements, even if the official approval is still pending (due to the other work) we may start some parallel activities to speed up the release once officially approved.
Is it acceptable for you?

[semuelle]

@AltiMario thanks for the update. We will discuss this and get back to you next week.

[bhargavbh]

Hi @AltiMario! Great to know that your team is interested in the GRANDPA formal verification RFC. I have a few questions/comments:

1. Could you elaborate why you have structured verifying using a proof-assistant (Coq) as your first Milestone and applying model-checkers as your second milestone? In general, formally specifying a verifying GRANDPA in an ITP like Coq is a lot more intensive and laborious than using a Model-Checker. Hence, as a first step it might make sense to work on the TLA+ specification, and in the process get a better understanding of the protocol and its invariants (to get thru the induction proofs later). These specs can be then checked using bounded model-checkers like TLC or even Apalache (a symbolic model-checker for TLA+ with backend-solver Z3). I recommend swapping the two milestones, focusing first on the lower-risk milestone.
2. The 'Detailed Activities' section lists a bunch of lemmas from the GRANDPA paper that need to be formalised. Could you please add details on techniques/approaches you plan to use for abstraction, for e.g., how would partially synchrony be modelled, the gossip network, the consistency oracle which used in definition of safety and liveness? What about the changes to the protocol to add notion of time, as its crucial to reason about block finality time in liveness arguments. An high-level overview would strengthen the proposal.
3. I would like to point out some related work on modelling and verifying Tendermint consensus in TLA+, and also in Ivy here. Although the setting and consensus mechanisms are quite different, it might still be a good source of inspiration for modelling.

[AltiMario]

hi @bhargavbh I swapped the order as you suggested, it makes more sense now.

• Your questions answered by @sparsa Sparsa Roychowdhury

How would partial synchrony be modelled?
Partially synchronous systems(PSS) have been a very important research topic in distributed systems. There are many work in the literature that tries to prove protocols for the consensus problem of PSS. One of them is Ceph consensus algorithm. Ceph consensus algorithm is modelled in TLA+ as shown in the repo:
https://github.com/afonsonf/ceph-consensus-spec
We are planning to follow similar modelling for GRANDPA.

How the gossip network be modelled?
One interesting difference between conventional partial synchronous systems and the one implemented in GRANDPA is, that the processes may not have a direct communication channel. The whole process space can be modelled using different subsets of itself. Processes that belong to the same subset have direct communication channels within themselves. The subsets communicate using the gossip protocol. Note that the following assumptions must hold to model the system:

1. The subsets must have a common node so that indirect communication is possible. This criterion will ensure which subsets are valid and which are not.
2. The union of the subsets must give us the complete set of processes
   For the case of Coq, we aren’t interested in the gossip network particularly but in a property like

• For a particular round r, after time GST+T we have that V_r_v_t is a constant.
  Of course, the real property is more complex, but this captures the idea.
  We aren’t interested in proving the good behavior of a gossip network, but in the properties of it that allow us to accomplish our proofs. Otherwise, we would end with the task of implementing a full network in Coq, and such a thing is completely out of scope.
  So, most of the time we won’t handle the passing of messages between voters, we would instead express them as changes in the output of the function V_r_v_t.

How do we model the consistency oracle used in the definition of safety and liveness?
A consistency oracle in the context of GRANDPA refers to a mechanism that determines whether the nodes in the network have reached a consistent view of the blockchain's finality. Modelling a consistency oracle involves specifying the conditions under which nodes agree on the finalized state. We need to add an extra variable to the state of the model that will tell us if the consistency criterion is met. During the transition, the variable will be updated against the following consistency checks:

• Agreement: No two correct processes decide on different values
• Termination: All correct processes eventually decide on a value
• Validity: A decided value is valid,

What about the changes to the protocol to add the notion of time?
We need to incorporate timing when we want to deal with weakly synchronous gossip network mode. We have to declare two system parameters GST (Global Stability Time) and \delta. In addition to that, each process will have a clock to measure time outs. This will add more dimensions to the states of the underlying state transition system defined by TLA+. We have to carefully chalk out what will be the measure of a one-time unit.
Having that we have to have the following assumption:
\delta-timely: If a correct process p sends message m at time t \geq GST to a correct process q, then q will receive message m before time t + \delta.

• This is the comment from @Luis-omega Luis Alberto Díaz Díaz

In the case of coq we plan to start modeling the time dependency as a function from some domain T to the values. For example, we can do a direct translation of a set of votes V_r_v_t as a function V that relates a round of votes, a voter, and a time to a particular set of voters.
We think that a discrete model of time using the Naturals is possible, after all, there is a physical limit on how low we can measure time.
The plan is to add further predicates (constraints) in the statement of the lemmas, in such a way that the structures V, E and others follow the appropriate properties for the corresponding lemma.
Of course, this requires the cautious introduction of the predicates, we don’t want to add by accident more than what is needed or more than what is possible to really have. However, we believe that additional predicates are straightforward in most if not all the cases they are needed.

[bhargavbh]

Hi @AltiMario thanks for the detailed responses. I have left a few suggestion for changes, please address them.
From a technical viewpoint, i am happy to approve the proposal. Feel free to contact me if you need clarifications during the project, happy to get involved.
I'll let the grants team @semuelle @Noc2 decide what is the best way forward, either the current W3F grants program or via Decentralised Futures program.

[bhargavbh]

Can you please add documentation for the techniques and abstractions used for modelling as a deliverable. Ideally with in-line comments in the TLA+ spec.

[bhargavbh]

Thanks for responding to my queries in detail. Could you please incorporate and consolidate those responses in the proposal itself. Maybe you can create a new subsection "Modelling Techniques".

[Sparsa]

Hi, I have created a pull-request on this branch with the modeling and abstraction techniques we are planning to use on TLA+ once @AltiMario approves it should show here.
Thank you.

[Noc2]

@AltiMario: This looks interesting. I have one question: This looks like a very interesting initiative to kickstart formal verification in our ecosystem. In this case, it might make sense, to rather get funding via the decentralized futures program: https://futures.web3.foundation/ Would you potentially interested in applying for the DF program instead? This way we might be able to support this initiative with a bigger amount.

[AltiMario]

hi @Noc2 It sounds like a good idea, especially if a formal verification is performed regularly on critical areas.
I will read more about the decentralized futures program and get back to you.

[github-actions]

CLA Assistant Lite bot: Thank you for your submission, we really appreciate it. Like many open source projects, we ask that you sign our Contributor License Agreement before we can accept your contribution. Please submit the following text as a separate comment:

---

I have read and hereby sign the Contributor License Agreement.

---

2 out of 3 committers have signed the CLA.
✅ @AltiMario
✅ @NadigerAmit
❌ @Sparsa Roychowdhury
Sparsa Roychowdhury seems not to be a GitHub user. You need a GitHub account to be able to sign the CLA. If you have already a GitHub account, please add the email address used for this commit to your account.
_{You can retrigger this bot by commenting recheck in this Pull Request}

[Noc2]

It sounds like you are applying for the DF program instead. So, I'm closing the application for now. But I'm happy to reopen it in the future.

[AltiMario]

hi @Noc2 yes I will apply for DF. Thank you for your support.