Merge pull request sushi-labs#80 from Certora/MasterChefV2-April-15

certora update spec
richard-xtek · Apr 19, 2021 · 6f84e57 · 6f84e57
2 parents 48488f2 + 028c608
commit 6f84e57
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 4 deletions.
diff --git a/spec/MasterChefV2.spec b/spec/MasterChefV2.spec
@@ -53,8 +53,7 @@ methods {
 	SUSHI() returns (address) envfree
 
 	// Rewarder
-	// SIG_ON_SUSHI_REWARD = 0xbb6cc2ef; // onSushiReward(uint256,address,uint256)
-	0xbb6cc2ef => NONDET
+	onSushiReward(uint256, address, uint256, uint256) => NONDET
 
 	// MasterChefV1
 	deposit(uint256 pid, uint256 amount) => NONDET
@@ -244,6 +243,8 @@ rule preserveTotalAssetOfUser(method f, uint256 pid, address user,
 		withdraw(e, pid, amount, to);
 	} else if (f.selector == emergencyWithdraw(uint256, address).selector) {
 		emergencyWithdraw(e, pid, to);
+	} else if (f.selector == withdrawAndHarvest(uint256,uint256,address).selector) {
+		withdrawAndHarvest(e, pid, amount, to);
 	} else {
 		calldataarg args;
 		f(e, args);
@@ -386,7 +387,10 @@ function callFunctionWithParams(method f, uint256 pid, address sender, address t
 		harvest(e, pid, to);
 	} else if (f.selector == emergencyWithdraw(uint256, address).selector) {
 		emergencyWithdraw(e, pid, to);
-	} else {
+	} else if (f.selector == withdrawAndHarvest(uint256,uint256,address).selector) {
+		withdrawAndHarvest(e, pid, amount, to);
+	}
+	else {
 		calldataarg args;
 		f(e,args);
 	}

diff --git a/spec/scripts/applyHarnesses.sh b/spec/scripts/applyHarnesses.sh
diff --git a/spec/scripts/runMasterChefV2.sh b/spec/scripts/runMasterChefV2.sh
@@ -1 +1 @@
-certoraRun spec/harnesses/MasterChefV2Harness.sol spec/harnesses/DummyERC20A.sol spec/harnesses/DummyERC20B.sol spec/harnesses/DummySUSHI.sol --link MasterChefV2Harness:SUSHI=DummySUSHI --settings -assumeUnwindCond,-enableStorageAnalysis=true,-ciMode=true --verify MasterChefV2Harness:spec/MasterChefV2.spec --cache MasterChefV2 --msg "MasterChefV2"
+certoraRun spec/harnesses/MasterChefV2Harness.sol spec/harnesses/DummyERC20A.sol spec/harnesses/DummyERC20B.sol spec/harnesses/DummySUSHI.sol --link MasterChefV2Harness:SUSHI=DummySUSHI --settings -assumeUnwindCond,-enableStorageAnalysis=true,-ciMode=true --verify MasterChefV2Harness:spec/MasterChefV2.spec --cache MasterChefV2 --msg "MasterChefV2"
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		certoraRun spec/harnesses/MasterChefV2Harness.sol spec/harnesses/DummyERC20A.sol spec/harnesses/DummyERC20B.sol spec/harnesses/DummySUSHI.sol --link MasterChefV2Harness:SUSHI=DummySUSHI --settings -assumeUnwindCond,-enableStorageAnalysis=true,-ciMode=true --verify MasterChefV2Harness:spec/MasterChefV2.spec --cache MasterChefV2 --msg "MasterChefV2"
		certoraRun spec/harnesses/MasterChefV2Harness.sol spec/harnesses/DummyERC20A.sol spec/harnesses/DummyERC20B.sol spec/harnesses/DummySUSHI.sol --link MasterChefV2Harness:SUSHI=DummySUSHI --settings -assumeUnwindCond,-enableStorageAnalysis=true,-ciMode=true --verify MasterChefV2Harness:spec/MasterChefV2.spec --cache MasterChefV2 --msg "MasterChefV2"