Verify the p-token

[clarus]

Here is an optimized Solana smart contract: https://github.com/solana-program/token/tree/main/p-token with Pinocchio. The goal is to show it as equivalent to the original version https://github.com/solana-program/token/tree/main/program .

So we need to:

• Translate p-token to Rocq
• Make links for p-token
• Make a simulation for p-token
• Translate token to Rocq
• Make links for token
• Make a simulation for token
• Prove that the two programs above are equivalent!