Skip to content
This repository was archived by the owner on Sep 27, 2023. It is now read-only.

Refactor to increase readability#30

Open
Allarious wants to merge 6 commits into
base:master
Choose a base branch
from
Open

Refactor to increase readability #30

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
0e37851
refactored checkPendingToCancelledOrStarted to increase readability
Mar 7, 2023
a83266c
refactored checkPendingToCancelledOrStarted to increase readability
Mar 7, 2023
1157592
refactored checkStartedToStateTransition to increase readability
Mar 7, 2023
8eae1fa
corrected the checkStartedToStateTransition specification
Mar 7, 2023
3cdd6e8
refactored integrityOfTransfer to improve readability
Mar 7, 2023
e1d25cc
fixed a typo inside auctionBroken
Mar 8, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion 02.Lesson_InvestigateViolations/ERC20/ERC20.spec
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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";
}


Expand Down
14 changes: 9 additions & 5 deletions 02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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 == 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()";
}


Expand All@@ -67,9 +69,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()";
}


Expand Down
2 changes: 1 addition & 1 deletion 06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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];
}

Expand Down
, 'i'); if (__m === '*' || __re.test(location.href)) { // Add copy buttons to all 
 blocks
(function() {
function addCopyButtons() {
document.querySelectorAll('pre code').forEach(function(codeBlock) {
if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;
codeBlock.parentElement.setAttribute('data-copy-added', 'true');
var btn = document.createElement('button');
btn.textContent = 'Copy';
btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';
btn.onmouseover = function() { this.style.opacity = '1'; };
btn.onmouseout = function() { this.style.opacity = '0.7'; };
btn.onclick = function() {
navigator.clipboard.writeText(codeBlock.textContent).then(function() {
btn.textContent = 'Copied!';
setTimeout(function() { btn.textContent = 'Copy'; }, 1500);
});
};
codeBlock.parentElement.style.position = 'relative';
codeBlock.parentElement.appendChild(btn);
});
}
addCopyButtons();
// Re-run on dynamic content
var observer = new MutationObserver(addCopyButtons);
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '
Refactor to increase readability by Allarious · Pull Request #30 · Certora/Tutorials · GitHub
Skip to content

This repository was archived by the owner on Sep 27, 2023. It is now read-only.

Refactor to increase readability#30
 Open

Allarious
wants to merge
6
commits into

base:master
Choose a base branch

from

 Open


Refactor to increase readability
#30
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
0e37851

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
a83266c

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
1157592

refactored checkStartedToStateTransition to increase readability

Mar 7, 2023
8eae1fa

corrected the checkStartedToStateTransition specification

Mar 7, 2023
3cdd6e8

refactored integrityOfTransfer to improve readability

Mar 7, 2023
e1d25cc

fixed a typo inside auctionBroken

Mar 8, 2023

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 3 additions & 1 deletion
02.Lesson_InvestigateViolations/ERC20/ERC20.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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";
}


Expand Down

14 changes: 9 additions & 5 deletions
02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 == 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()";
}


Expand All@@ -67,9 +69,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()";
}


Expand Down

2 changes: 1 addition & 1 deletion
06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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];
	}

Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Force GitHub README to respect dark mode
(function() {
var style = document.createElement('style');
style.textContent = '
.markdown-body {
color-scheme: dark light;
}
.markdown-body pre { background: #161b22 !important; }
.markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }
.markdown-body table th, .markdown-body table td { border-color: #30363d !important; }
.markdown-body img { background: #0d1117; }
.markdown-body blockquote { border-left-color: #8b949e; }
.markdown-body hr { border-color: #30363d; }
';
document.head.appendChild(style);
})();
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '
Refactor to increase readability by Allarious · Pull Request #30 · Certora/Tutorials · GitHub
Skip to content

This repository was archived by the owner on Sep 27, 2023. It is now read-only.

Refactor to increase readability#30
 Open

Allarious
wants to merge
6
commits into

base:master
Choose a base branch

from

 Open


Refactor to increase readability
#30
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
0e37851

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
a83266c

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
1157592

refactored checkStartedToStateTransition to increase readability

Mar 7, 2023
8eae1fa

corrected the checkStartedToStateTransition specification

Mar 7, 2023
3cdd6e8

refactored integrityOfTransfer to improve readability

Mar 7, 2023
e1d25cc

fixed a typo inside auctionBroken

Mar 8, 2023

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 3 additions & 1 deletion
02.Lesson_InvestigateViolations/ERC20/ERC20.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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";
}


Expand Down

14 changes: 9 additions & 5 deletions
02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 == 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()";
}


Expand All@@ -67,9 +69,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()";
}


Expand Down

2 changes: 1 addition & 1 deletion
06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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];
	}

Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Highlight search terms from Google/DuckDuckGo/Bing referrer
(function() {
var ref = document.referrer;
var terms = [];
if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {
var url = new URL(ref);
var q = url.searchParams.get('q') || url.searchParams.get('p');
if (q) {
terms = q.split(/\s+/).filter(function(t) { return t.length > 2; });
}
}
if (terms.length === 0) return;
var style = document.createElement('style');
style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';
document.head.appendChild(style);
function highlight(node) {
if (node.nodeType === 3) { // text node
var text = node.textContent;
var found = false;
terms.forEach(function(term) {
var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\]\\]/g, '\\') + ')', 'gi');
if (regex.test(text)) {
found = true;
var frag = document.createDocumentFragment();
var parts = text.split(regex);
parts.forEach(function(part, i) {
if (i % 2 === 0) {
frag.appendChild(document.createTextNode(part));
} else {
var span = document.createElement('span');
span.className = 'userscript-highlight';
span.textContent = part;
frag.appendChild(span);
}
});
node.parentNode.replaceChild(frag, node);
}
});
} else if (node.nodeType === 1 && node.childNodes) { // element
var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];
if (!skipTags.includes(node.tagName)) {
Array.from(node.childNodes).forEach(highlight);
}
}
}
highlight(document.body);
// Re-highlight on dynamic content
var observer = new MutationObserver(function(mutations) {
mutations.forEach(function(m) {
m.addedNodes.forEach(function(node) {
if (node.nodeType === 1 || node.nodeType === 3) highlight(node);
});
});
});
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '
Refactor to increase readability by Allarious · Pull Request #30 · Certora/Tutorials · GitHub
Skip to content

This repository was archived by the owner on Sep 27, 2023. It is now read-only.

Refactor to increase readability#30
 Open

Allarious
wants to merge
6
commits into

base:master
Choose a base branch

from

 Open


Refactor to increase readability
#30
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
0e37851

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
a83266c

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
1157592

refactored checkStartedToStateTransition to increase readability

Mar 7, 2023
8eae1fa

corrected the checkStartedToStateTransition specification

Mar 7, 2023
3cdd6e8

refactored integrityOfTransfer to improve readability

Mar 7, 2023
e1d25cc

fixed a typo inside auctionBroken

Mar 8, 2023

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 3 additions & 1 deletion
02.Lesson_InvestigateViolations/ERC20/ERC20.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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";
}


Expand Down

14 changes: 9 additions & 5 deletions
02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 == 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()";
}


Expand All@@ -67,9 +69,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()";
}


Expand Down

2 changes: 1 addition & 1 deletion
06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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];
	}

Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Strip utm_, fbclid, gclid, etc. from all links on page
(function() {
var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',
'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',
'ref', 'ref_src', 'source', 'medium', 'campaign'];
function cleanUrl(url) {
try {
var u = new URL(url, window.location.origin);
var changed = false;
trackingParams.forEach(function(p) {
if (u.searchParams.has(p)) {
u.searchParams.delete(p);
changed = true;
}
});
return changed ? u.toString() : url;
} catch (e) {
return url;
}
}
function cleanLinks() {
document.querySelectorAll('a[href]').forEach(function(a) {
var clean = cleanUrl(a.href);
if (clean !== a.href) a.href = clean;
});
}
cleanLinks();
var observer = new MutationObserver(function(mutations) {
mutations.forEach(function(m) {
m.addedNodes.forEach(function(node) {
if (node.nodeType === 1) {
if (node.tagName === 'A') cleanLinks();
node.querySelectorAll('a[href]').forEach(function(a) {
var clean = cleanUrl(a.href);
if (clean !== a.href) a.href = clean;
});
}
});
});
});
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '
Refactor to increase readability by Allarious · Pull Request #30 · Certora/Tutorials · GitHub
Skip to content

This repository was archived by the owner on Sep 27, 2023. It is now read-only.

Refactor to increase readability#30
 Open

Allarious
wants to merge
6
commits into

base:master
Choose a base branch

from

 Open


Refactor to increase readability
#30
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
0e37851

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
a83266c

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
1157592

refactored checkStartedToStateTransition to increase readability

Mar 7, 2023
8eae1fa

corrected the checkStartedToStateTransition specification

Mar 7, 2023
3cdd6e8

refactored integrityOfTransfer to improve readability

Mar 7, 2023
e1d25cc

fixed a typo inside auctionBroken

Mar 8, 2023

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 3 additions & 1 deletion
02.Lesson_InvestigateViolations/ERC20/ERC20.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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";
}


Expand Down

14 changes: 9 additions & 5 deletions
02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 == 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()";
}


Expand All@@ -67,9 +69,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()";
}


Expand Down

2 changes: 1 addition & 1 deletion
06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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];
	}

Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Auto-enable theater mode on YouTube
(function() {
function tryTheater() {
var btn = document.querySelector('button[aria-label="Theater mode"], ytd-player #player button[title="Theater mode"]');
if (btn && !btn.classList.contains('activated')) {
btn.click();
}
}
// Try immediately
tryTheater();
// Try after navigation (SPA)
var lastUrl = location.href;
setInterval(function() {
if (location.href !== lastUrl) {
lastUrl = location.href;
setTimeout(tryTheater, 500);
}
}, 1000);
// Also try on player load
var observer = new MutationObserver(tryTheater);
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '
Refactor to increase readability by Allarious · Pull Request #30 · Certora/Tutorials · GitHub
Skip to content

This repository was archived by the owner on Sep 27, 2023. It is now read-only.

Refactor to increase readability#30
 Open

Allarious
wants to merge
6
commits into

base:master
Choose a base branch

from

 Open


Refactor to increase readability
#30
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
0e37851

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
a83266c

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
1157592

refactored checkStartedToStateTransition to increase readability

Mar 7, 2023
8eae1fa

corrected the checkStartedToStateTransition specification

Mar 7, 2023
3cdd6e8

refactored integrityOfTransfer to improve readability

Mar 7, 2023
e1d25cc

fixed a typo inside auctionBroken

Mar 8, 2023

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 3 additions & 1 deletion
02.Lesson_InvestigateViolations/ERC20/ERC20.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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";
}


Expand Down

14 changes: 9 additions & 5 deletions
02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 == 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()";
}


Expand All@@ -67,9 +69,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()";
}


Expand Down

2 changes: 1 addition & 1 deletion
06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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];
	}

Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Remove or un-stick sticky/fixed headers that block content
(function() {
function unstick() {
document.querySelectorAll('header, nav, [role="banner"], .header, .navbar, .sticky, .fixed-top, [style*="position: fixed"], [style*="position:sticky"]').forEach(function(el) {
if (el.style.position === 'fixed' || el.style.position === 'sticky' || getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {
el.style.position = 'static';
el.style.top = 'auto';
el.style.zIndex = 'auto';
}
});
}
unstick();
var observer = new MutationObserver(unstick);
observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });
})();
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '
Refactor to increase readability by Allarious · Pull Request #30 · Certora/Tutorials · GitHub
Skip to content

This repository was archived by the owner on Sep 27, 2023. It is now read-only.

Refactor to increase readability#30
 Open

Allarious
wants to merge
6
commits into

base:master
Choose a base branch

from

 Open


Refactor to increase readability
#30
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
0e37851

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
a83266c

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
1157592

refactored checkStartedToStateTransition to increase readability

Mar 7, 2023
8eae1fa

corrected the checkStartedToStateTransition specification

Mar 7, 2023
3cdd6e8

refactored integrityOfTransfer to improve readability

Mar 7, 2023
e1d25cc

fixed a typo inside auctionBroken

Mar 8, 2023

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 3 additions & 1 deletion
02.Lesson_InvestigateViolations/ERC20/ERC20.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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";
}


Expand Down

14 changes: 9 additions & 5 deletions
02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 == 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()";
}


Expand All@@ -67,9 +69,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()";
}


Expand Down

2 changes: 1 addition & 1 deletion
06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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];
	}

Expand Down

, 'i');
if (__m === '*' || __re.test(location.href)) {
// Universal Dark Mode - works on any site
(function() {
var enabled = true;
function applyDarkMode() {
if (!enabled) return;
// Create style element if it doesn't exist
var style = document.getElementById('universal-dark-mode-style');
if (!style) {
style = document.createElement('style');
style.id = 'universal-dark-mode-style';
document.head.appendChild(style);
}
// Dark mode CSS - inverts colors but preserves images/video
style.textContent = '
/* Invert everything except media */
html {
filter: invert(1) hue-rotate(180deg) !important;
background: #1a1a2e !important;
}
/* Restore images, videos, iframes, canvas */
img, video, iframe, canvas, svg, picture, [style*="background-image"] {
filter: invert(1) hue-rotate(180deg) !important;
}
/* Preserve specific elements that should not be inverted */
.no-dark-mode, .no-dark-mode *,
[data-theme="light"], [data-theme="light"],
.ace_editor, .ace_editor *,
.CodeMirror, .CodeMirror *,
.monaco-editor, .monaco-editor *,
.markdown-body pre, .markdown-body pre *,
.highlight, .highlight *,
pre code, pre code * {
filter: none !important;
}
/* Fix common UI elements */
.modal, .popup, .dropdown-menu, .tooltip, .popover {
filter: invert(1) hue-rotate(180deg) !important;
background: #2d2d44 !important;
border-color: #444 !important;
}
/* Scrollbars */
::-webkit-scrollbar { background: #1a1a2e !important; }
::-webkit-scrollbar-thumb { background: #444 !important; }
::-webkit-scrollbar-thumb:hover { background: #555 !important; }
/* Selection */
::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }
::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }
';
}
function removeDarkMode() {
var style = document.getElementById('universal-dark-mode-style');
if (style) style.remove();
}
// Toggle with Alt+Shift+D
document.addEventListener('keydown', function(e) {
if (e.altKey && e.shiftKey && e.key === 'D') {
e.preventDefault();
enabled = !enabled;
if (enabled) {
applyDarkMode();
console.log('[Universal Dark Mode] Enabled');
} else {
removeDarkMode();
console.log('[Universal Dark Mode] Disabled');
}
}
});
// Apply on load
applyDarkMode();
// Re-apply on dynamic content
var observer = new MutationObserver(function(mutations) {
if (enabled && !document.getElementById('universal-dark-mode-style')) {
applyDarkMode();
}
});
observer.observe(document.head, { childList: true });
console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');
})();
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();
Refactor to increase readability by Allarious · Pull Request #30 · Certora/Tutorials · GitHub
Skip to content

This repository was archived by the owner on Sep 27, 2023. It is now read-only.

Refactor to increase readability#30
 Open

Allarious
wants to merge
6
commits into

base:master
Choose a base branch

from

 Open


Refactor to increase readability
#30
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


6 commits


Select commit
Hold shift + click to select a range
0e37851

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
a83266c

refactored checkPendingToCancelledOrStarted to increase readability

Mar 7, 2023
1157592

refactored checkStartedToStateTransition to increase readability

Mar 7, 2023
8eae1fa

corrected the checkStartedToStateTransition specification

Mar 7, 2023
3cdd6e8

refactored integrityOfTransfer to improve readability

Mar 7, 2023
e1d25cc

fixed a typo inside auctionBroken

Mar 8, 2023

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


4 changes: 3 additions & 1 deletion
02.Lesson_InvestigateViolations/ERC20/ERC20.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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";
}


Expand Down

14 changes: 9 additions & 5 deletions
02.Lesson_InvestigateViolations/MeetingScheduler/meetings.spec

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 == 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()";
}


Expand All@@ -67,9 +69,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()";
}


Expand Down

2 changes: 1 addition & 1 deletion
06.Lesson_ThinkingProperties/AuctionDemonstration/AuctionBroken.sol

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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];
	}

Expand Down