Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[move] formal specifications for vouch & burn modules #330

Merged
merged 13 commits into from
Jan 8, 2025
Merged

[move] formal specifications for vouch & burn modules #330

merged 13 commits into from
Jan 8, 2025

Conversation

Jayfromthe13th
Copy link
Contributor

Specification Updates for Vouch and Burn Modules

Changes

Vouch Specification (vouch.spec.move)

  • Completely redid specifications due to previous compilation errors
  • Added detailed comments explaining each specification block
  • Improved readability and clarity of specifications

Key Links:

Burn Specification (burn.spec.move)

  • Rebuilt specifications to resolve previous compilation issues
  • Enhanced existing specifications with more descriptive comments
  • Added invariants to prevent potential integer overflow

Key Links:

Verification Checklist for Vouch Specification

  • Added pragma verify = true
  • Implemented preconditions for true_friends
  • Added overflow checks for vector lengths
  • Ensured valid vector properties
  • Checked vouch existence conditions
  • Verified revoke operation specifications
  • Added checks for bulk vouch setting

Verification Checklist for Burn Specification

  • Added pragma verify = true
  • Implemented strict aborts checking
  • Added invariants for BurnCounter
  • Checked system address requirements
  • Verified burn tracking mechanisms
  • Added overflow prevention for lifetime counters
  • Ensured community preference settings

Jayfromthe13th and others added 12 commits November 17, 2024 13:28
@Jayfromthe13th
feat: add comprehensive vouch specifications
00c5c57 
- 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
@Jayfromthe13th
feat: add vouch specifications
88f2829
@Jayfromthe13th
Update burn and vouch specifications with detailed comments and overf…
7dc11a1 
…low checks
@Jayfromthe13th
Trigger workflow rerun
ff1cff0
@Jayfromthe13th
Delete framework/libra-framework/backup_specs/slow_wallet.spec.move
947d8ae
@Jayfromthe13th
Delete framework/libra-framework/backup_specs/burn.spec.move
2436910
@Jayfromthe13th
Delete framework/libra-framework/backup_specs/demo.spec.move
ba480b6
@Jayfromthe13th
Delete framework/libra-framework/backup_specs/libra_coin.spec.move
f2c55f9
@Jayfromthe13th
Delete framework/libra-framework/backup_specs/ol_account.spec.move
d9565ce
@Jayfromthe13th
Delete framework/libra-framework/backup_specs/sacred_cows.spec.move
b91a279
@Jayfromthe13th
Remove backup_specs folder
f489889
@Jayfromthe13th
Trigger workflow
a7b3feb
@0o-de-lally 0o-de-lally changed the title Feature/burn vouch spec updates [move] formal specifications for vouch & burn modules Jan 7, 2025
@0o-de-lally 0o-de-lally changed the title [move] formal specifications for vouch & burn modules NEW [move] formal specifications for vouch & burn modules Jan 7, 2025
@0o-de-lally 0o-de-lally changed the title NEW [move] formal specifications for vouch & burn modules [move] formal specifications for vouch & burn modules Jan 7, 2025
@0o-de-lally
Copy link
Contributor

Congrats @Jayfromthe13th you earned your stripes! Big value in this commit.

@0o-de-lally 0o-de-lally merged commit 2a310b2 into 0LNetworkCommunity:main Jan 8, 2025
14 checks passed
@Jayfromthe13th
Copy link
Contributor Author

Ty! Means a lot 🙏🏽

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@Jayfromthe13th @0o-de-lally