Skip to content

Conversation

@dkcumming
Copy link
Collaborator

@dkcumming dkcumming commented Nov 4, 2025

This PR refactors calls to get_{account, mint, multisig} where possible in all proof harnesses to reduce the amount of steps proofs need to take. A selection of proofs were run again to see the reduction in steps, not every harness could be refactored and some proofs go for long without stopping so it is hard to see how the count changes.

The naming convention introduced is inspired by specification languages that have an old(...) operator to talk about pre-strate (e.g. Dafny). In the post state I added new to variable so it would be clear this is captured after the implementation has executed.

Proofs run and change in steps:

  • initialize_account: 89207 -> 89207 = no change, probably indicates not getting into the else branch
  • transfer: 4011 -> 3459 = 14% reduction
  • mint_to: 3248 -> 2834 = 13% reduction
  • burn: 4699 -> 3457 = 26% reduction
  • close_account: 3711 -> 3021 = 19% reduction
  • transfer_checked: 4755 -> 4065 = 15% reduction
  • burn_checked: 5290 -> 3910 = 26% reduction
  • approve: 3049 -> 2773 = 9% reduction
  • approve_checked: 3793 -> 3517 = 7% reduction
  • revoke: 2409 -> 2133 = 11% reduction
  • freeze_account: 3199 -> 2647 = 17% reduction
  • thaw_account: 3199 -> 2647 = 17% reduction
  • mint_to_checked: 3689 -> 3275 = 11% reduction
  • sync_native: 2331 -> 2055 = 12% reduction

The concrete test harnesses that are able to run with our restricted harnesses were also run successfully

Improvement from 3711 steps to 3021 steps for the proof.
`test_process_initialize_mint_{freeze, no_freeze}` did not have the
proofs run again as they do not finish to tell if there is a step
reduction
This DOES NOT reduce the amount of proofs steps compared to if this
change is not present (both 89207 steps), indicating that our proofs are not getting into the
`else` brach of the post-condition.
@dkcumming dkcumming self-assigned this Nov 4, 2025
@dkcumming dkcumming marked this pull request as ready for review November 5, 2025 15:10
@dkcumming
Copy link
Collaborator Author

Concrete tests have been run post merge for both p-token and programs and passed all (except the malformed input tests we do not handle)

@dkcumming dkcumming requested a review from JuanCoRo November 5, 2025 15:11
Copy link
Member

@jberthold jberthold left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM
Nice refactoring, code is much easier to read/follow now.

@automergerpr-permission-manager automergerpr-permission-manager bot merged commit dfd122e into proofs Nov 6, 2025
1 check passed
@jberthold jberthold deleted the dc/fewer-calls branch November 6, 2025 07:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants