Add Formal Specifications for Vouch & Burn Module Safety and Correctness #328
Conversation
- Added global invariants for vector alignment - Added specs for true_friends, revoke, all_not_expired - Added VouchInvariant schema - Added specs for bulk_set and get_vouch_price
added indepth spec for burn.move module
Jayfromthe13th
changed the title
| pragma aborts_if_is_strict = true; | ||
|
|
||
| // Global invariant: BurnCounter must be initialized before any operations | ||
| invariant [suspendable] exists<BurnCounter>(@ol_framework); |
There was a problem hiding this comment.
good one, an important check for all system state
|
|
||
| spec BurnCounter { | ||
| // Resource invariant | ||
| invariant lifetime_burned <= MAX_U64; |
There was a problem hiding this comment.
nice. it might be good to check that some of the interim calculations don't overflow as well.
| let addr = signer::address_of(vm); | ||
|
|
||
| // Preconditions | ||
| requires system_addresses::is_ol_framework_address(addr); |
There was a problem hiding this comment.
Great. For future reference: this is an important check for all initializers. There is the 0x0 address which is the VM and the 0x1 which is framework. In the past, and in tests we have used is_root(), which would actually cause missing state if we used 0x0. So yes, this is an important check going forward.
| ensures global<BurnCounter>(@ol_framework).lifetime_recycled == 0; | ||
| } | ||
|
|
||
| spec epoch_burn_fees { |
There was a problem hiding this comment.
Nicely done here. Perhaps add a comment about where result_1 comes from.
| old(global<BurnCounter>(@ol_framework).lifetime_recycled); | ||
| } | ||
|
|
||
| spec set_send_community(sender: &signer, community: bool) { |
There was a problem hiding this comment.
Looks good. One check we could possibly add for completeness, is that system addresses should not be able to add this.
| pragma verify = true; | ||
| pragma aborts_if_is_strict = false; | ||
|
|
||
| // Global invariant: ensure vectors are always aligned |
There was a problem hiding this comment.
Great! Something we have been concerned about in the past.
| @@ -0,0 +1,93 @@ | |||
| spec ol_framework::vouch { | |||
There was a problem hiding this comment.
Would be great if you added the same code comments as you did in burn.move.spec: preconditions, aborts, postconditions.
|
|
||
| spec is_valid_voucher_for(voucher: address, recipient: address): bool { | ||
| aborts_if false; | ||
| ensures result == vector::contains(true_friends(recipient), voucher); |
There was a problem hiding this comment.
I'm not 100% what is being checked here, it may be I forgot how it this check works. Can you add a comment?
|
@Jayfromthe13th All looks good above, except that one of our CI tests is failing on a Move compilation issue. I haven't seen this before. The rest of the Move code compiles and tests fine. It's just on our Upgrade verification. |
|
This looks great thanks. However I noticed that these tests appear to fail in CI: |
|
|
|
Thanks for the feedback. I'll make those changes @0o-de-lally . Also, thanks for catching this @dboreham ! It does seem like there's an issue with the make command not propagating the error correctly. I’ll investigate further and see locally to confirm. Ik there was some recent updates with the fv which may be causing issues depending |
Description:
This PR adds comprehensive formal specifications to the vouch module to ensure safety, correctness, and proper state management. The specifications verify critical properties of the vouching system.
File Location:
vouch.spec.move
Key Specifications Added:
These specifications help ensure:
Testing:
Add Formal Specifications for Burn Module Safety and Correctness
This PR adds comprehensive formal specifications to the burn module to ensure safety, correctness, and proper state management of burning operations.
File Location:
burn.spec.move
Key Specifications Added:
These specifications help ensure:
Testing:
The burn module specifications provide critical safety guarantees for:
These formal specifications help ensure the burn module operates safely and correctly under all conditions.