Adding Formal Verification Report #153
Closed
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Collaborator
dkcumming
commented
Jan 21, 2026
dkcumming
commented
- Adds report that contains:
- details of Solana
- details of equivalence proofs
- hand proofs for equivalence of P-Token and SPL-Token
- Updates VERIFICATION.md:
- Assumptions
- Limitations
- Shared harnesses
…pendency (#134) * `withdraw_excess_lamports_account` used a wrong error code for the overflow case * `withdraw_excess_lamports_mint` skipped checking overflow errors when the mint auth flag was set * `transfer_checked` had a stray `assert(result.is_ok())` placed before some error checks * `close_account` skipped checking for overflow when the account was owned by system or incinerator Also updates the `mir-semantics` dependency to the latest feature branch. --------- Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>
* revised SPL cheat codes * Partial implementation of `ptr_offset_from[_unsigned]`
In checking all branches asserted that the result was either `Err` (an
error with specified error code) or `Ok` I found the success case for
`InitializeMint{2}` proof harnesses was missing the assertion. This PR
adds those assertions.
- Python tool updates runtimeverification/mir-semantics#893 , runtimeverification/mir-semantics#892 - Function pointer support runtimeverification/mir-semantics#894 - Stable-MIR-JSON update runtimeverification/mir-semantics#896, runtimeverification/mir-semantics#898 - [update spl/p-token.md to use #execTerminatorCall](runtimeverification/mir-semantics@39ce2a6) - Add --fail-fast and --maintainence-rate pyk flags (Add --fail-fast and --maintainence-rate pyk flags #900)
…ey eq (#143) This PR makes the following specs passed: - test_process_initialize_mint_freeze - test_process_initialize_mint_no_freeze - test_process_initialize_mint2_freeze - test_process_initialize_mint2_no_freeze
With the follow changes the `Burn` proof passes for non-multisig - corrects the check on owner to be for the src `AccountInfo` not `Account` - renames the mint owner to be clearly from the `AccountInfo` - adds `!src_owner_sys_inc` to the guard for the delegate logic - adds an else case for the delegate logic to claim nothing is changed for the delegate account and amount
See #144 as these are the same changes With the follow changes the `BurnChecked` P-Token proof passes for non-multisig - corrects the check on owner to be for the src AccountInfo not Account - renames the mint owner to be clearly from the AccountInfo - adds !src_owner_sys_inc to the guard for the delegate logic - adds an else case for the delegate logic to claim nothing is changed for the delegate account and amount Updates are also propagated to SPL-Token however there is not testing or proving done
…alidInstruction` (#146) `process_withdraw_excess_lamports` is missed in spl-token and implemented in token-2022.
Correcting index for destination account in `TransferChecked` harness
Adds guard on postcondition check for `owner`, `lamports`, and `data_len` behind a feature flag, specifically `target_os = "solana"` and `target_arch = "bpf"`. This means that `CloseAccount` now passes for non-multisig. However this proof passing is slightly limited in strength since it does not check that the `data`, `lamports`, and `owner` field are zeroed when `close_unchecked` is called in the implementation.
…tency (#150) The refactoring makes it straightforward to compare and verify that both token implementations (spl-token and p-token) follow the same specifications. The key changes are: 1. Extracted shared specs - Moved 43 test specification files to a new specs/shared/ directory, covering all major token operations. 3. Created separate preludes - Added prelude-p-token.rs and prelude-spl-token.rs to handle implementation-specific setup while sharing common test logic. 4. Massive deduplication - Removed ~4,200 lines from p-token and ~4,500 lines from spl-token entrypoint files by extracting common code. 5. Added documentation - New specs/README.md explaining the structure. --------- Co-authored-by: dkcumming <daniel.cumming@runtimeverification.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.