Fix spec and add spec for supra governance #63
Conversation
| aborts_if !table::spec_contains(voting_forum.proposals, proposal_id); | ||
| aborts_if is_voting_period_over(proposal); | ||
| aborts_if proposal.is_resolved; | ||
| aborts_if !exists<timestamp::CurrentTimeMicroseconds>(@supra_framework); |
There was a problem hiding this comment.
@axiongsupra not sure why this aborts_if is required and what purpose does it serve.
| // }; | ||
| let timestamp_secs_bytes = std::bcs::serialize(timestamp::spec_now_seconds()); | ||
| let key = std::string::spec_utf8(RESOLVABLE_TIME_METADATA_KEY); | ||
| ensures simple_map::spec_get(post_proposal.metadata, key) == timestamp_secs_bytes; |
There was a problem hiding this comment.
This property only ensures that time is recorded. Other properties we should aim at adding are
- vote by the voter is recorded (if not already voted)
- vote by the voter is recorded (if vote is flipped)
- total yes/no votes should tally (increase/decrease appropriately)
| requires chain_status::is_operating(); | ||
| //TODO: Remove pragma aborts_if_is_partial; | ||
| pragma aborts_if_is_partial = true; | ||
| // include IsProposalResolvableAbortsIf<ProposalType>; |
| aborts_if has_multi_step_key && !from_bcs::deserializable<bool>(simple_map::spec_get(proposal.metadata, multi_step_key)); | ||
| aborts_if has_multi_step_key && from_bcs::deserialize<bool>(simple_map::spec_get(proposal.metadata, multi_step_key)); |
There was a problem hiding this comment.
Not sure I understand the role of these. @axiongsupra
|
|
||
| let post post_voting_forum = global<VotingForum<ProposalType>>(voting_forum_address); | ||
| let post post_proposal = table::spec_get(post_voting_forum.proposals, proposal_id); | ||
| aborts_if !exists<timestamp::CurrentTimeMicroseconds>(@supra_framework); |
| from_bcs::deserialize(simple_map::spec_get(proposal.metadata, multi_step_key)); | ||
| aborts_if !is_multi_step && len(next_execution_hash) != 0; | ||
|
|
||
| aborts_if len(next_execution_hash) == 0 && !exists<timestamp::CurrentTimeMicroseconds>(@supra_framework); |
There was a problem hiding this comment.
Again, not sure at this point why !exist<timestamp::CurrentTimeMicroseconds>(@supra_framework) is needed. I do not see this in the source code.
| requires chain_status::is_operating(); | ||
| //TODO: Remove pragma aborts_if_is_partial; | ||
| pragma aborts_if_is_partial = true; | ||
| include AbortsIfNotContainProposalID<ProposalType>; |
There was a problem hiding this comment.
There is no ensures here, it seems commented out, why?
| pragma aborts_if_is_partial = true; | ||
| include AbortsIfNotContainProposalID<ProposalType>; | ||
|
|
||
| let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address); |
There was a problem hiding this comment.
No property here either, it's commented out, why?
| let proposal = table::spec_get(voting_forum.proposals, proposal_id); | ||
| let voting_closed = spec_is_voting_closed<ProposalType>(voting_forum_address, proposal_id); | ||
| // Avoid Overflow | ||
| aborts_if voting_closed && (proposal.yes_votes <= proposal.no_votes || proposal.yes_votes + proposal.no_votes < proposal.min_vote_threshold); |
There was a problem hiding this comment.
It doesn't seem it reflects our logic wrt yes and no votes. We would abort if voting_closed && !(proposal.yes_votes >= proposal.min_vote_threshold) isn't it?
| voting_forum_address: address, | ||
| proposal_id: u64, | ||
| ): u64 { | ||
| let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address); |
There was a problem hiding this comment.
Don't we need aborts_if if proposal_id doesn't exist? Perhaps some earlier schema that has been used can be reused here?
| proposal_id: u64, | ||
| voting_forum: VotingForum<ProposalType> | ||
| ): u64 { | ||
| let proposal = table::spec_get(voting_forum.proposals, proposal_id); |
| } | ||
|
|
||
| spec fun spec_is_voting_closed<ProposalType: store>(voting_forum_address: address, proposal_id: u64): bool { | ||
| let voting_forum = global<VotingForum<ProposalType>>(voting_forum_address); |
| @@ -113,7 +113,8 @@ spec supra_framework::reconfiguration { | |||
| /// Should equal to 0 | |||
| spec emit_genesis_reconfiguration_event { | |||
| use supra_framework::reconfiguration::{Configuration}; | |||
|
|
|||
| // TODO remove aborts_if_is_partial after the property proved | |||
| pragma aborts_if_is_partial; | |||
There was a problem hiding this comment.
AbortsIfNotAptosFramework earlier need to be renamed to AbortsIfNotSupraFramework
No description provided.