Grants Application
Project: RocketProof
What is the work being proposed?
Build a formal model of the Rocket Pool protocol (the smart contracts) and its execution environment (Ethereum) in higher-order logic.
As an initial foray in this direction, we propose only to build a model at a suitable and convenient level of abstraction, with a view to future extension (with a formal connection e.g. via refinement) to more accurate low-level details (e.g. EVM opcode semantics).
Is there any related work this builds off of?
No, although we will use existing generic tooling and libraries e.g. https://hol-theorem-prover.org.
Will the results of this project be entirely open source (MIT, GPL, Apache, CC BY license or similar)? If not, which parts will not be, why, and under what license will they be published?
Pure unadulterated free software. 100% GPL.
Benefits - enter N/A where appropriate
How does this benefit Rocket Pool?
There is no difference to the answer for all Rocket Pool variants for this question, so I provide the answer once:
- Provide machine-checked confidence in the safety and security of the protocol.
- A unique marketing opportunity: that the protocol has been formally verified to the proposed degree of thoroughness.
- In case any bug bounties are found to be claimable during the course of the verification, these will be claimed and mitigated, which further enhances the quality and security of the protocol. 10% of all bug bounties claimed will be donated back to the GMC budget.
(Note: no marketing of the results is included specifically in this proposal.)
What other non-RPL protocols, DAOs, projects, or individuals, would stand to benefit from this grant?
The Ethereum (both execution and consensus layer) protocol model will be reusable for other verification projects. And the methodology for smart contract protocol verification may also be reusable.
Will the resulting project be open source?
How could it possibly not be?
Team
Who is doing the work?
- Ramana
- Team member TBD - I will post a bounty
What is the background of the person(s) doing the work? What experience do they have with such projects in the past?
- Rocket Pool node operator, and holder of rETH and RPL
- Has an award-winning PhD in formal verification, and is a primary author of a large project in this area, https://cakeml.org, amongst other theorem-proving projects.
What is the breakdown of the proposed work, in terms of milestones and/or deadlines?
Here’s an example roadmap for the first 1-2 months:
- Define basic model of EVM
- probably not including bytecode initially, but just high-level operations, e.g., shallowly embedded state change functions
- Define basic model of beacon chain
- Define model of Rocket Storage contract, based on shallow embedding of the Solidity implementation
- Prove some basic properties of Rocket Storage as a quick check of the methodology and setup
My rough sense of the size of this project is 6 months.
How is the work being tested? Is testing included in the schedule?
Base level: all proofs will be machine-checked by the HOL theorem prover, for every commit to the main branch of the repository.
Furthermore, the high-level theorem statements will be scrutinised and offered (as with all the work, but these can be highlighted) to the community and team members for inspection.
Optional extra: we may include correspondence checks between contract execution in logic and execution in an external test harness (e.g. traces from mainnet, or testnet/devnet executions). Some of these correspondences could be included as theorems above - the extra testing described here is more about building infrastructure for extracting traces to check against.
How will the work be maintained after delivery?
No maintenance included by default: the final commit will build and verify with a specified HOL version. Updates should, however, be straightforward in the future, whether due to Rocket Pool, Ethereum, or HOL updates.
Payment and Verification
I propose a budget of 1000 RPL for the main work, with up to 250 RPL in reserve for additional extras.
Since this project is in part a research project, the exact targets and direction may diverge from the text of this application - please consider the spirit of the application, i.e. to formally model and verify the Rocket Pool protocol with machine-checked proofs, as the guiding direction. If this application is supported and its work is done, I expect there will be further applications in the future for extending and improving the work.
I am very open to negotiation and stewarding from the GMC on deciding on the payment level and schedule, and on the verification criteria.
What is the acceptance criteria?
- Minimum criterion: There is a formally proved theorem about some non-trivial (although it can be simple) property of the Rocket Pool protocol. This implies there are sufficiently good models of Ethereum and Rocket Pool defined in order to state the theorem.
- The primary judgement will be made by Ramana and their collaborator(s).
- An additional judgement will be made by a Rocket Pool community member (the GMC can choose), with the requirement being that the result is explained/documented/AMA’d by Ramana to sufficient detail that this community member is satisfied, assuming a good-faith attempt is made to understand it by the community member.
What is the proposed payment schedule for the grant? How much RPL and over what period of time is the applicant requesting?
I am open to whatever the GMC suggests on this point.
How will the GMC verify that the work’s deliveries match the proposed cadence?
All development will be in a public git repository, and the team will make themselves available for Q&A as desired (within reason).
What alternatives or options have been considered in order to save costs for the proposed project?
None. There’s a K framework formalisation of Ethereum I think, but probably it’s not suitable for the depth of smart contract verification we eventually want to do.
Conflict of Interest
Does the person or persons proposing the grant have any conflicts of interest to disclose? (Please disclose here if you are a member of the GMC or if any member of the GMC would benefit directly financially from the grant).
No.
Will the recipient of the grant, or any protocol or project in which the recipient has a vested interest (other than Rocket Pool), benefit financially if the grant is successful?
No.