From 0e37851cc4a6ec9660bd2c03ddd48bfc2844653f Mon Sep 17 00:00:00 2001 From: allarious Date: Tue, 7 Mar 2023 13:38:27 -0700 Subject: [PATCH 1/6] refactored checkPendingToCancelledOrStarted to increase readability --- .../MeetingScheduler/meetings.spec | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec b/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec index 735f9f05..3ec846e5 100644 --- a/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec @@ -67,9 +67,11 @@ rule checkPendingToCancelledOrStarted(method f, uint256 meetingId) { uint8 stateBefore = getStateById(e, meetingId); f(e, args); - assert (stateBefore == 1 => (getStateById(e, meetingId) == 1 || getStateById(e, meetingId) == 2 || getStateById(e, meetingId) == 4)), "invalidation of the state machine"; - assert ((stateBefore == 1 && getStateById(e, meetingId) == 2) => f.selector == startMeeting(uint256).selector), "the status of the meeting changed from PENDING to STARTED through a function other then startMeeting()"; - assert ((stateBefore == 1 && getStateById(e, meetingId) == 4) => f.selector == cancelMeeting(uint256).selector), "the status of the meeting changed from PENDING to CANCELLED through a function other then cancelMeeting()"; + uint8 stateAfter = getStateById(e.meetingId); + + assert (stateBefore == 1 => (stateAfter == 1 || stateAfter == 2 || stateAfter == 4)), "invalidation of the state machine"; + assert ((stateBefore == 1 && stateAfter == 2) => f.selector == startMeeting(uint256).selector), "the status of the meeting changed from PENDING to STARTED through a function other then startMeeting()"; + assert ((stateBefore == 1 && stateAfter == 4) => f.selector == cancelMeeting(uint256).selector), "the status of the meeting changed from PENDING to CANCELLED through a function other then cancelMeeting()"; } From a83266c5a710aa2c42c4b927397cd98df9081f18 Mon Sep 17 00:00:00 2001 From: allarious Date: Tue, 7 Mar 2023 13:40:37 -0700 Subject: [PATCH 2/6] refactored checkPendingToCancelledOrStarted to increase readability --- 02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec b/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec index 3ec846e5..4299b47c 100644 --- a/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec @@ -67,7 +67,7 @@ rule checkPendingToCancelledOrStarted(method f, uint256 meetingId) { uint8 stateBefore = getStateById(e, meetingId); f(e, args); - uint8 stateAfter = getStateById(e.meetingId); + uint8 stateAfter = getStateById(e, meetingId); assert (stateBefore == 1 => (stateAfter == 1 || stateAfter == 2 || stateAfter == 4)), "invalidation of the state machine"; assert ((stateBefore == 1 && stateAfter == 2) => f.selector == startMeeting(uint256).selector), "the status of the meeting changed from PENDING to STARTED through a function other then startMeeting()"; From 115759273bbc3cc73d2936e4c6a843de82810cac Mon Sep 17 00:00:00 2001 From: allarious Date: Tue, 7 Mar 2023 13:45:10 -0700 Subject: [PATCH 3/6] refactored checkStartedToStateTransition to increase readability --- .../MeetingScheduler/meetings.spec | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec b/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec index 4299b47c..72e5848b 100644 --- a/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec @@ -53,8 +53,10 @@ rule checkStartedToStateTransition(method f, uint256 meetingId) { calldataarg args; uint8 stateBefore = getStateById(e, meetingId); f(e, args); - assert (stateBefore == 2 => (getStateById(e, meetingId) == 2 || getStateById(e, meetingId) == 4)), "the status of the meeting changed from STARTED to an invalid state"; - assert ((stateBefore == 2 && getStateById(e, meetingId) == 4) => f.selector == endMeeting(uint256).selector), "the status of the meeting changed from STARTED to ENDED through a function other then endMeeting()"; + uint8 stateAfter = getStateById(e, meetingId); + + assert (stateBefore == 2 => (stateAfter == 2 || stateAfter == 4)), "the status of the meeting changed from STARTED to an invalid state"; + assert ((stateBefore == 2 && stateAfter == 4) => f.selector == endMeeting(uint256).selector), "the status of the meeting changed from STARTED to ENDED through a function other then endMeeting()"; } From 8eae1fa76d9f0d4c8413fcacdd9973cf343caf66 Mon Sep 17 00:00:00 2001 From: allarious Date: Tue, 7 Mar 2023 13:47:20 -0700 Subject: [PATCH 4/6] corrected the checkStartedToStateTransition specification --- .../MeetingScheduler/meetings.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec b/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec index 72e5848b..46ec057c 100644 --- a/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec +++ b/02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec @@ -55,8 +55,8 @@ rule checkStartedToStateTransition(method f, uint256 meetingId) { f(e, args); uint8 stateAfter = getStateById(e, meetingId); - assert (stateBefore == 2 => (stateAfter == 2 || stateAfter == 4)), "the status of the meeting changed from STARTED to an invalid state"; - assert ((stateBefore == 2 && stateAfter == 4) => f.selector == endMeeting(uint256).selector), "the status of the meeting changed from STARTED to ENDED through a function other then endMeeting()"; + assert (stateBefore == 2 => (stateAfter == 2 || stateAfter == 3)), "the status of the meeting changed from STARTED to an invalid state"; + assert ((stateBefore == 2 && stateAfter == 3) => f.selector == endMeeting(uint256).selector), "the status of the meeting changed from STARTED to ENDED through a function other then endMeeting()"; } From 3cdd6e86a07f89eb08a46a6718bb713711f9652e Mon Sep 17 00:00:00 2001 From: allarious Date: Tue, 7 Mar 2023 14:03:42 -0700 Subject: [PATCH 5/6] refactored integrityOfTransfer to improve readability --- 02.Lesson_InvestigateViolations/ERC20/ERC20.spec | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/02.Lesson_InvestigateViolations/ERC20/ERC20.spec b/02.Lesson_InvestigateViolations/ERC20/ERC20.spec index c0aa40da..78e08920 100644 --- a/02.Lesson_InvestigateViolations/ERC20/ERC20.spec +++ b/02.Lesson_InvestigateViolations/ERC20/ERC20.spec @@ -11,8 +11,10 @@ rule integrityOfTransfer(address recipient, uint256 amount) { uint256 balanceSenderBefore = balanceOf(e, e.msg.sender); uint256 balanceRecipientBefore = balanceOf(e, recipient); transfer(e, recipient, amount); + uint256 balanceSenderAfter = balanceOf(e, e.msg.sender); + uint256 balanceRecipientAfter = balanceOf(e, recipient); - assert balanceRecipientBefore + balanceSenderBefore == balanceOf(e, e.msg.sender) + balanceOf(e, recipient), "the total funds before and after a transfer should remain the constant"; + assert balanceRecipientBefore + balanceSenderBefore == balanceRecipientAfter + balanceSenderAfter, "the total funds before and after a transfer should remain constant"; } From e1d25cc73768a5376551f3cb92c9633d3c9d07d0 Mon Sep 17 00:00:00 2001 From: allarious Date: Tue, 7 Mar 2023 20:54:45 -0700 Subject: [PATCH 6/6] fixed a typo inside auctionBroken --- .../AuctionDemonstration/AuctionBroken.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol b/06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol index cce3d0a8..e356dcc8 100644 --- a/06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol +++ b/06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol @@ -101,7 +101,7 @@ contract AuctionImpl is TokenInterface { require(auctions[id].bid_expiry != 0 && (auctions[id].bid_expiry < now || auctions[id].end_time < now)); - mint(auctions[id].winner, auctions[id].prize);n + mint(auctions[id].winner, auctions[id].prize); delete auctions[id]; }