Create Preparing Polkadot pallet_balances for Formal Verification.md

[SurfingBowser]

Inferara Grant application

Project Abstract

This project is an R&D initiative to further secure Polkadot and subsequent parachains. With the recent increase in discussions of stablecoins across all ecosystem, we observed the benefit of gaining mathematical assurance for the safety of functions within pallet_assets for future integration of Circle’s CCTP (Cross Chain Transfer Protocol).
Since pallets are an essential part of the Polkadot infrastructure, we want to take a deep look at exactly how the current logic functions. pallet_balances is used by every token on Polkadot. Within pallet_balances, the fungible traits are what will be researched specifically.
We plan how to apply our Rocq-based framework Inference to Polkadot’s fungible trait set.
Adaptation of the fungible trait set for formal verifications within our non-deterministic WASM framework will enable complete trait extraction with validated semantic mapping ready for formal specification.

Grant level

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

Application Checklist

• The application template has been copied and aptly renamed (project_name.md).
• I have read the application guidelines.
• Payment details have been provided (Polkadot AssetHub (USDC & DOT) address in the application and bank details via email, if applicable).
• I understand that an agreed upon percentage of each milestone will be paid in vested DOT, to the Polkadot address listed 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)

[SurfingBowser]

I have read and hereby sign the Contributor License Agreement.

[takahser]

@SurfingBowser thanks for your interest in our grant program.

I've got a few questions regarding your application:

• You mention both pallet_balances and pallet_assets in your doc; is this proposal focused on one of the two, or on both of them?
• The deliverables are currently very vague, could you add more details on what we can expect? For example, "research findings and results" sounds rather generic.
• If we would sign the grant, what would you envision to be the next step(s) after its completion? Would you continue to work on this, and if yes, in what capacity?

[github-actions]

CLA Assistant Lite bot All contributors have signed the CLA ✍️ ✅

[SurfingBowser]

@takahser Thank you for the comment and questions.
I've updated the .md file with the following changes

You mention both pallet_balances and pallet_assets in your doc; is this proposal focused on one of the two, or on both of them?

Our initial interest began with pallet_assets but we will only be focused on pallet_balances

The deliverables are currently very vague, could you add more details on what we can expect? For example, "research findings and results" sounds rather generic.

We have updated the deliverables to include more details. We have notably merged 0d & 0e into one Final Research Article.

Number	Deliverable	Specification
0a.	License	MIT.
0b.	Documentation	We will provide informative documentation on our research process and findings. This will be in a dedicated GitHub repository. Will also include 0c-0d deliverables and research artifacts.
0c.	Reproducibility	We will provide step-by-step guides for the grants team to know what we have done. Includes rust code of the functionality that has been researched and resulting byte code.
0d.	Final Research Article	We will publish a detailed research article to the Github repository and our website that explains our research findings and results. This includes the reproducibility guide of the 0c deliverable, notably WASM binary compilation artifacts. Textual description of fungible traits specification along with discovered assumptions regarding execution environment, required for its implementation. This article will include a cleaned up and annotated WASM module of pallet_balances. Includes Rust code that is distilled and ready to reason about. Ordinary unit tests to confirm its faithfulness to the original in a classical sense. This prepares pallet_balances for future reasoning.

If we would sign the grant, what would you envision to be the next step(s) after its completion? Would you continue to work on this, and if yes, in what capacity?

Here is a detailed description of how we envision the research steps:

Research findings and next steps.

Our general plan for the complete research consists of three major phases:

1. Land clearing. Our in-development methodology for program verification relies on reasoning about already compiled WASM modules, so we can not treat them as black-box objects that just need to work somehow. It is important to isolate meaningful code, that specification should be covering, from the surrounding elements of infrastructure, that may slip into compiled modules due to the uncontrollable complexities of build process. To be properly specified, pallet_balances must be first stripped of everything not directly related to its core functionality. If there are any algorithm subtasks, currently delegated to external frameworks, they must be either re-implemented inline, or comprehensively annotated to become explicit suppositions of future spec. Basically, pallet_balances should start looking like it was hand-written with a systematically minimalist approach.
2. Specification design. Using our in-development language Inference, we write formal specification of traits implemented in subject module, with regard to suppositions, discovered in the previous step. By nature of our tool-chain, this formal specification itself targets a variety of WASM for compilation, though the resulting module is not executable due to its reliance on the controllable non-determinism to express para-virtual branching.
3. Formal verification. We link together WASM modules of the covered pallet and its formal specification in our in-development Coq-based reasoning environment. Such linking produces Coq theories, that can be roughly summarized as "If non-deterministic execution was possible, this code would terminate successfully". Proving resulting theories by logical means essentially implies, that subject module adheres to the specification in all cases.
   This particular grant application covers only the first point of this plan (Land Clearing), but we are looking forward to continuing our work on the next steps, depending on eligibility of results and your concernment.

As for capacity, for any future grants we hope to increase the existing team capacity. Such an increase would be from FTE of 1.25 to 2. The increase of capacity opens up the opportunity to involve more individuals into the research project. The scale of the team depends on the grant size of course.

[SurfingBowser]

I have read and hereby sign the Contributor License Agreement.