Skip to content

Commit dfd122e

Browse files
Refactor get_* calls in harnesses for fewer steps (#88)
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 --------- Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
1 parent beed3f4 commit dfd122e

File tree

1 file changed

+398
-404
lines changed

1 file changed

+398
-404
lines changed

0 commit comments

Comments
 (0)