diff --git a/CLIFlags/Helpers/Fibonacci.spec b/CLIFlags/Helpers/Fibonacci.spec index 7a536745..424725bf 100644 --- a/CLIFlags/Helpers/Fibonacci.spec +++ b/CLIFlags/Helpers/Fibonacci.spec @@ -2,13 +2,12 @@ methods { function fibonacci(uint32) external returns (uint32) envfree; } -rule fibonacciMonotonicallyIncreasing { +rule fibonacciMonotonicallyIncreasing() { uint32 i1; uint32 i2; - assert i2 > i1 => fibonacci(i2) >= fibonacci(i1); } -rule fifthFibonacciElementIsFive { +rule fifthFibonacciElementIsFive() { assert fibonacci(5) == 5; } diff --git a/CLIFlags/Helpers/auto_dispatcher/AutoDispatcherExample.spec b/CLIFlags/Helpers/auto_dispatcher/AutoDispatcherExample.spec index 0a4feb72..94a28d41 100644 --- a/CLIFlags/Helpers/auto_dispatcher/AutoDispatcherExample.spec +++ b/CLIFlags/Helpers/auto_dispatcher/AutoDispatcherExample.spec @@ -4,8 +4,7 @@ using E as e; rule r(uint n) { env environ; uint ret = foo(environ, n); - assert currentContract.i == d || currentContract.i == e, "optimistic dispatching should promise this"; assert currentContract.i == d => ret == n; assert currentContract.i == e => ret == n + 1; -} \ No newline at end of file +} diff --git a/CVLByExample/AddressFunctionCall/AddressCall.spec b/CVLByExample/AddressFunctionCall/AddressCall.spec index f7597595..fd4394a7 100644 --- a/CVLByExample/AddressFunctionCall/AddressCall.spec +++ b/CVLByExample/AddressFunctionCall/AddressCall.spec @@ -1,7 +1,7 @@ using A as a; using B as b; -rule AddressCall { +rule AddressCall() { env e; address x; assert x.foo(e) >= 1 && x.foo(e) <= 2; diff --git a/CVLByExample/ConfInheritance/MainSpec.spec b/CVLByExample/ConfInheritance/MainSpec.spec index f6ee6195..3cecc68d 100644 --- a/CVLByExample/ConfInheritance/MainSpec.spec +++ b/CVLByExample/ConfInheritance/MainSpec.spec @@ -5,7 +5,7 @@ */ methods { - function currentBid() external returns uint256 envfree; + function currentBid() external returns (uint256) envfree; } /// @title Basic rules //////////////////////////////////////////////////// @@ -20,7 +20,7 @@ methods { rule bidIncreasesAssets() { env e; require(e.msg.sender != currentContract); - require(e.msg.value > currentBid() ); + require(e.msg.value > currentBid()); uint256 balanceBefore = nativeBalances[currentContract]; bid(e); assert nativeBalances[currentContract] > balanceBefore; @@ -37,8 +37,8 @@ rule bidSuccessfullyExpectVacuous() { env e; uint256 balanceBefore = nativeBalances[currentContract]; require(e.msg.sender != currentContract); - require(e.msg.value > 0 && e.msg.value > balanceBefore); - require (balanceBefore > 0); + require(e.msg.value > 0 && e.msg.value > balanceBefore); + require(balanceBefore > 0); bid(e); assert nativeBalances[currentContract] >= balanceBefore; } diff --git a/CVLByExample/ContractAlias/ContractAlias.spec b/CVLByExample/ContractAlias/ContractAlias.spec index e6d2ab6f..6fd9cc20 100644 --- a/CVLByExample/ContractAlias/ContractAlias.spec +++ b/CVLByExample/ContractAlias/ContractAlias.spec @@ -1,8 +1,10 @@ import "Imported.spec"; -methods { function A.Always1() internal returns (uint) => ALWAYS(2);} +methods { + function A.Always1() internal returns (uint) => ALWAYS(2); +} -rule verifySummaryOnAlias(){ +rule verifySummaryOnAlias() { env e; assert 2 == Always1(e); -} \ No newline at end of file +} diff --git a/CVLByExample/ContractAlias/Imported.spec b/CVLByExample/ContractAlias/Imported.spec index 27700aea..58e1398d 100644 --- a/CVLByExample/ContractAlias/Imported.spec +++ b/CVLByExample/ContractAlias/Imported.spec @@ -1 +1 @@ -using ContractA as A; \ No newline at end of file +using ContractA as A; diff --git a/CVLByExample/Ecrecover/ecrecover.spec b/CVLByExample/Ecrecover/ecrecover.spec index 6d75da2a..91946232 100644 --- a/CVLByExample/Ecrecover/ecrecover.spec +++ b/CVLByExample/Ecrecover/ecrecover.spec @@ -11,7 +11,6 @@ Example for ecrecover Methods that are not declared here are assumed to be dependent on env. */ - /*** # ecrecover properties: # 1. zero value: ecrecover(0, v, r, s) == 0 @@ -27,26 +26,21 @@ Example for ecrecover where s' != s **/ - - methods { function isSigned(address _addr, bytes32 msgHash, uint8 v, bytes32 r, bytes32 s) external returns (bool) envfree; function executeMyFunctionFromSignature(uint8 v, bytes32 r, bytes32 s, address owner, uint256 myParam, uint256 deadline) external; - function getHash(address owner, uint256 myParam, uint256 deadline) external returns(bytes32) envfree; + function getHash(address owner, uint256 myParam, uint256 deadline) external returns (bytes32) envfree; } - function ecrecoverAxioms() { - // zero value: - require (forall uint8 v. forall bytes32 r. forall bytes32 s. ecrecover(to_bytes32(0), v, r, s) == 0); - // uniqueness of signature - require (forall uint8 v. forall bytes32 r. forall bytes32 s. forall bytes32 h1. forall bytes32 h2. - h1 != h2 => ecrecover(h1, v, r, s) != 0 => ecrecover(h2, v, r, s) == 0); - // dependency on r and s - require (forall bytes32 h. forall uint8 v. forall bytes32 s. forall bytes32 r1. forall bytes32 r2. - r1 != r2 => ecrecover(h, v, r1, s) != 0 => ecrecover(h, v, r2, s) == 0); - require (forall bytes32 h. forall uint8 v. forall bytes32 r. forall bytes32 s1. forall bytes32 s2. - s1 != s2 => ecrecover(h, v, r, s1) != 0 => ecrecover(h, v, r, s2) == 0); + + // zero value: + require(forall uint8 v. forall bytes32 r. forall bytes32 s. ecrecover(to_bytes32(0), v, r, s) == 0); + // uniqueness of signature + require(forall uint8 v. forall bytes32 r. forall bytes32 s. forall bytes32 h1. forall bytes32 h2. h1 != h2 => ecrecover(h1, v, r, s) != 0 => ecrecover(h2, v, r, s) == 0); + // dependency on r and s + require(forall bytes32 h. forall uint8 v. forall bytes32 s. forall bytes32 r1. forall bytes32 r2. r1 != r2 => ecrecover(h, v, r1, s) != 0 => ecrecover(h, v, r2, s) == 0); + require(forall bytes32 h. forall uint8 v. forall bytes32 r. forall bytes32 s1. forall bytes32 s2. s1 != s2 => ecrecover(h, v, r, s1) != 0 => ecrecover(h, v, r, s2) == 0); } /* @@ -54,99 +48,100 @@ function ecrecoverAxioms() { */ rule zeroValue() { ecrecoverAxioms(); - bytes32 msgHash; uint8 v; bytes32 r; bytes32 s; - assert ecrecover(to_bytes32(0), v, r, s ) == 0; + bytes32 msgHash; + uint8 v; + bytes32 r; + bytes32 s; + assert ecrecover(to_bytes32(0), v, r, s) == 0; } - - - rule deterministic() { ecrecoverAxioms(); - bytes32 msgHash; uint8 v; bytes32 r; bytes32 s; - assert ecrecover(msgHash, v, r, s ) == ecrecover(msgHash, v, r, s ); + bytes32 msgHash; + uint8 v; + bytes32 r; + bytes32 s; + assert ecrecover(msgHash, v, r, s) == ecrecover(msgHash, v, r, s); } rule uniqueness() { ecrecoverAxioms(); - bytes32 msgHashA; bytes32 msgHashB; uint8 v; bytes32 r; bytes32 s; - require msgHashA != msgHashB; + bytes32 msgHashA; + bytes32 msgHashB; + uint8 v; + bytes32 r; + bytes32 s; + require msgHashA != msgHashB; assert ecrecover(msgHashA, v, r, s) != 0 => ecrecover(msgHashB, v, r, s) == 0; } rule dependencyOnS() { ecrecoverAxioms(); - bytes32 msgHash; uint8 v; bytes32 r; bytes32 s1; bytes32 s2; - require s1 != s2; + bytes32 msgHash; + uint8 v; + bytes32 r; + bytes32 s1; + bytes32 s2; + require s1 != s2; assert ecrecover(msgHash, v, r, s1) != 0 => ecrecover(msgHash, v, r, s2) == 0; //!= ecrecover(msgHash, v, r, s1) ; } rule dependencyOnR() { ecrecoverAxioms(); - bytes32 msgHash; uint8 v; bytes32 r1; bytes32 r2; bytes32 s; - require r1 != r2; - assert ecrecover(msgHash, v, r1, s) != 0 => ecrecover(msgHash, v, r2, s) == 0 ; + bytes32 msgHash; + uint8 v; + bytes32 r1; + bytes32 r2; + bytes32 s; + require r1 != r2; + assert ecrecover(msgHash, v, r1, s) != 0 => ecrecover(msgHash, v, r2, s) == 0; } // Rules for a function that checks signature -rule singleVerifier () -{ +rule singleVerifier() { ecrecoverAxioms(); - bytes32 msgHash; uint8 v; bytes32 r; bytes32 s; - address addr1; - address addr2; - require addr1 != addr2 && addr1!=0 && addr2!=0 ; - assert isSigned(addr1, msgHash, v, r, s ) => !isSigned(addr2, msgHash, v, r, s ) ; - + bytes32 msgHash; + uint8 v; + bytes32 r; + bytes32 s; + address addr1; + address addr2; + require addr1 != addr2 && addr1 != 0 && addr2 != 0; + assert isSigned(addr1, msgHash, v, r, s) => !isSigned(addr2, msgHash, v, r, s); } - -rule ownerSignatureIsUnique () { +rule ownerSignatureIsUnique() { ecrecoverAxioms(); - bytes32 msgHashA; bytes32 msgHashB; - uint8 v; bytes32 r; bytes32 s; - address addr; - require msgHashA != msgHashB; + bytes32 msgHashA; + bytes32 msgHashB; + uint8 v; + bytes32 r; + bytes32 s; + address addr; + require msgHashA != msgHashB; require addr != 0; - assert isSigned(addr, msgHashA, v, r, s ) => !isSigned(addr, msgHashB, v, r, s ); + assert isSigned(addr, msgHashA, v, r, s) => !isSigned(addr, msgHashB, v, r, s); } -rule hashIsUnique( - address ownerA, - uint256 myParamA, - uint256 deadlineA, - address ownerB, - uint256 myParamB, - uint256 deadlineB -) { - bytes32 hashA = getHash(ownerA, myParamA, deadlineA); +rule hashIsUnique(address ownerA, uint256 myParamA, uint256 deadlineA, address ownerB, uint256 myParamB, uint256 deadlineB) { + bytes32 hashA = getHash(ownerA, myParamA, deadlineA); bytes32 hashB = getHash(ownerB, myParamB, deadlineB); - assert hashA == hashB => ( ownerA == ownerB && - myParamA == myParamB && - deadlineA == deadlineB ); + assert hashA == hashB => (ownerA == ownerB && myParamA == myParamB && deadlineA == deadlineB); } - /*** # High level property : there is only single owner that can be used A rule which proves that for a given set of parameters only a single owner can execute . This property is implemented as a relational property - it compares two different executions on the same state. */ -rule onlySingleUserCanExecute(uint8 v, - bytes32 r, - bytes32 s, - address alice, - address bob, - uint256 myParam, - uint256 deadline) { - +rule onlySingleUserCanExecute(uint8 v, bytes32 r, bytes32 s, address alice, address bob, uint256 myParam, uint256 deadline) { env e1; env e2; ecrecoverAxioms(); //save the current state - storage init = lastStorage; + storage init = lastStorage; //execute and assume succeeded address temp = ecrecover(getHash(bob, myParam, deadline), v, r, s); executeMyFunctionFromSignature(e1, v, r, s, alice, myParam, deadline); @@ -154,28 +149,20 @@ rule onlySingleUserCanExecute(uint8 v, executeMyFunctionFromSignature@withrevert(e2, v, r, s, bob, myParam, deadline) at init; bool success = !lastReverted; //if it succeeded it must be the same owner, or an unrealistic hash collision - assert success => ( alice==bob ) ; + assert success => (alice == bob); } - /*** # High level property : Owner must be the signer of the hash A rule which proves that for a given set of parameters only a single owner can execute . This property is implemented as a relational property - it compares two different executions on the same state. */ -rule ownerIsSigner(uint8 v, - bytes32 r, - bytes32 s, - address owner, - uint256 myParam, - uint256 deadline) { - +rule ownerIsSigner(uint8 v, bytes32 r, bytes32 s, address owner, uint256 myParam, uint256 deadline) { env e; ecrecoverAxioms(); //execute and assume succeeded address signer = ecrecover(getHash(owner, myParam, deadline), v, r, s); executeMyFunctionFromSignature(e, v, r, s, owner, myParam, deadline); - assert owner == signer; } @@ -183,54 +170,44 @@ rule ownerIsSigner(uint8 v, # High level property : params and deadline are signed make sure the param and deadline are part of the signature */ -rule signedParamAndDeadline(uint8 v, - bytes32 r, - bytes32 s, - address owner, - uint256 myParamA, - uint256 deadlineA, - uint256 myParamB, - uint256 deadlineB) { - +rule signedParamAndDeadline(uint8 v, bytes32 r, bytes32 s, address owner, uint256 myParamA, uint256 deadlineA, uint256 myParamB, uint256 deadlineB) { env e1; env e2; ecrecoverAxioms(); //save the current state - storage init = lastStorage; + storage init = lastStorage; //execute and assume succeeded executeMyFunctionFromSignature(e1, v, r, s, owner, myParamA, deadlineA); // compare another execution on the same state, look at reverting paths executeMyFunctionFromSignature@withrevert(e2, v, r, s, owner, myParamB, deadlineB) at init; bool success = !lastReverted; //if it succeeded it must be the same owner, or an unrealistic hash collision - assert success => ( myParamA==myParamB && deadlineA == deadlineB); + assert success => (myParamA == myParamB && deadlineA == deadlineB); } - /*** A signer can sign two different messages, in this case they have different signature **/ rule twoDifferent() { ecrecoverAxioms(); - bytes32 msgHashA; uint8 vA; bytes32 rA; bytes32 sA; - bytes32 msgHashB; uint8 vB; bytes32 rB; bytes32 sB; - require msgHashA != msgHashB; + bytes32 msgHashA; + uint8 vA; + bytes32 rA; + bytes32 sA; + bytes32 msgHashB; + uint8 vB; + bytes32 rB; + bytes32 sB; + require msgHashA != msgHashB; require ecrecover(msgHashA, vA, rA, sA) != 0 && ecrecover(msgHashB, vB, rB, sB) != 0; - satisfy ecrecover(msgHashA, vA, rA, sA) == ecrecover(msgHashB, vB, rB, sB); - assert ecrecover(msgHashA, vA, rA, sA) == ecrecover(msgHashB, vB, rB, sB) => - (rA != rB || sA != sB || vA != vB ); + satisfy ecrecover(msgHashA, vA, rA, sA) == ecrecover(msgHashB, vB, rB, sB); + assert ecrecover(msgHashA, vA, rA, sA) == ecrecover(msgHashB, vB, rB, sB) => (rA != rB || sA != sB || vA != vB); } /** Once a message is executed, it can not be executed again **/ -rule signedMessagesExecutedOnce(uint8 v, - bytes32 r, - bytes32 s, - address signer, - uint256 myParam, - uint256 deadline) { - +rule signedMessagesExecutedOnce(uint8 v, bytes32 r, bytes32 s, address signer, uint256 myParam, uint256 deadline) { env e1; env e2; ecrecoverAxioms(); @@ -239,40 +216,28 @@ rule signedMessagesExecutedOnce(uint8 v, //attemp to execute again, on a possible different env executeMyFunctionFromSignature@withrevert(e2, v, r, s, signer, myParam, deadline); bool reverted = lastReverted; - assert reverted ; + assert reverted; } -rule checkHash( - address bob, - uint256 myParam, - uint256 deadline) { - +rule checkHash(address bob, uint256 myParam, uint256 deadline) { env e1; ecrecoverAxioms(); //execute and assume succeeded assert getHash(bob, myParam, deadline) == getHash(bob, myParam, deadline); } -rule CheckRevertCondition(uint8 v, - bytes32 r, - bytes32 s, - address owner, - uint256 myParam, - uint256 deadline) { - +rule CheckRevertCondition(uint8 v, bytes32 r, bytes32 s, address owner, uint256 myParam, uint256 deadline) { env e; ecrecoverAxioms(); - + //execute and assume succeeded address signer = ecrecover(getHash(owner, myParam, deadline), v, r, s); - bool msgValue = e.msg.value != 0; bool signerIsZero = signer == 0; - bool signerDiffFromOwner = signer != owner; + bool signerDiffFromOwner = signer != owner; bool noncesOverflow = currentContract.nonces[owner] + 1 > max_uint256; bool blockTimestampPassDeadline = e.block.timestamp >= deadline; - - bool shouldRevert = noncesOverflow || msgValue || signerIsZero || signerDiffFromOwner || signerDiffFromOwner || blockTimestampPassDeadline ; + bool shouldRevert = noncesOverflow || msgValue || signerIsZero || signerDiffFromOwner || signerDiffFromOwner || blockTimestampPassDeadline; executeMyFunctionFromSignature@withrevert(e, v, r, s, owner, myParam, deadline); assert shouldRevert <=> lastReverted; } diff --git a/CVLByExample/ExtensionContracts/ExtensionContracts.spec b/CVLByExample/ExtensionContracts/ExtensionContracts.spec index 488f394c..89fbd0ba 100644 --- a/CVLByExample/ExtensionContracts/ExtensionContracts.spec +++ b/CVLByExample/ExtensionContracts/ExtensionContracts.spec @@ -54,18 +54,22 @@ rule parametricRule(method f) { satisfy true; } -invariant specificPreservedInv() base1.inExtension2 == 0 { - // Verify the specific preserved on an extension contract function works. - // Without this preserved the invariant should fail on this function. - preserved _.setInExtension2(uint256 _num) with (env e) { - require _num == 0; +invariant specificPreservedInv() + base1.inExtension2 == 0 { + + // Verify the specific preserved on an extension contract function works. + // Without this preserved the invariant should fail on this function. + preserved _.setInExtension2(uint256 _num) with (env e) { + require _num == 0; + } } -} -invariant genericPreservedInv() base1.inExtension2 == 0 { - // Should make all invariant rules vacuous (including the rule from - // the extension contract's function) - preserved { - require false; +invariant genericPreservedInv() + base1.inExtension2 == 0 { + + // Should make all invariant rules vacuous (including the rule from + // the extension contract's function) + preserved { + require false; + } } -} \ No newline at end of file diff --git a/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec b/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec index b16caa84..c17db001 100644 --- a/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec +++ b/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec @@ -2,9 +2,9 @@ hook Sstore currentContract.dontUseMe uint256 newVal (uint256 oldVal) { assert false, "the hook shouldn't be called"; } -rule resetZeroesAllFunds(address to,uint256 amount) { - env e; - require exists address a. currentContract.funds[a] > 0; - reset_storage currentContract; - assert forall address a. currentContract.funds[a] == 0, "all funds should be zero"; -} \ No newline at end of file +rule resetZeroesAllFunds(address to, uint256 amount) { + env e; + require exists address a. currentContract.funds[a] > 0; + reset_storage currentContract; + assert forall address a. currentContract.funds[a] == 0, "all funds should be zero"; +} diff --git a/CVLByExample/Immutable/Immutable.spec b/CVLByExample/Immutable/Immutable.spec index de38fe8b..3946e84f 100644 --- a/CVLByExample/Immutable/Immutable.spec +++ b/CVLByExample/Immutable/Immutable.spec @@ -1,7 +1,7 @@ using Owner as owner; // Access private immutable via linking (variable must be referenced in the code!) -rule ownerNeverChangedUsingLinking(env e, method f, calldataarg arg){ +rule ownerNeverChangedUsingLinking(env e, method f, calldataarg arg) { address currentOwner; require currentOwner == owner; f(e, arg); @@ -9,37 +9,28 @@ rule ownerNeverChangedUsingLinking(env e, method f, calldataarg arg){ } // Access private immutable via direct storage access (variable must be referenced in the code!) -rule ownerNeverChangedUsingDirectStorageAccess(env e){ +rule ownerNeverChangedUsingDirectStorageAccess(env e) { method f; calldataarg args; - address directOwner = currentContract.OWNER; - f(e, args); - assert directOwner == currentContract.OWNER; } // Access public immutable via direct storage access -rule uintNeverChangedDirectStorageAccess(env e){ +rule uintNeverChangedDirectStorageAccess(env e) { method f; calldataarg args; - uint256 myUint = currentContract.MY_UINT; - f(e, args); - assert myUint == currentContract.MY_UINT; } // Access public immutable via getter -rule uintNeverChangedGetter(env e){ +rule uintNeverChangedGetter(env e) { method f; calldataarg args; - uint256 myUint = currentContract.MY_UINT(e); - f(e, args); - assert myUint == currentContract.MY_UINT(e); -} \ No newline at end of file +} diff --git a/CVLByExample/Import/certora/specs/base.spec b/CVLByExample/Import/certora/specs/base.spec index 591a11db..9f5fd9ed 100644 --- a/CVLByExample/Import/certora/specs/base.spec +++ b/CVLByExample/Import/certora/specs/base.spec @@ -1,21 +1,22 @@ methods { - function minusSevenSomeUInt() external envfree; - function someUInt() external returns (uint256) envfree; + function minusSevenSomeUInt() external envfree; + function someUInt() external returns (uint256) envfree; } /// @notice Invariant in Base to be overridden by importing in `Sub` contract. -invariant invInBase() someUInt() >= 7 { - preserved { - require (someUInt() < 30); // @notice Explicit preserved block - } -} +invariant invInBase() + someUInt() >= 7 { + preserved { + require(someUInt() < 30); // @notice Explicit preserved block + } + } /// @notice A rule to be used in the importing contract `Sub` as is. rule ruleInBase() { - uint256 before = someUInt(); - minusSevenSomeUInt(); - uint256 after = someUInt(); - assert (before >=7) => (before - after == 7); + uint256 before = someUInt(); + minusSevenSomeUInt(); + uint256 after = someUInt(); + assert (before >= 7) => (before - after == 7); } /// Definition for demonstrating definition override in the importing contract `Sub`. @@ -23,30 +24,28 @@ definition filterDef(method f) returns bool = f.selector == sig:someUInt().selec /// CVL function to be overridden in the importing contract `Sub`. function callF(env eF, calldataarg args, method f) { - f(eF, args); + f(eF, args); } /// A rule calling one parameteric function filtered to `someInt`. -rule parametricRuleInBase(method f) filtered { f -> filterDef(f) } -{ - env eF; - calldataarg args; - uint256 before = someUInt(); - callF(eF, args, f); - uint256 after = someUInt(); - assert ((before >=7) => (before - after <= 7), "Unexpected result of one call to a parametric function"); +rule parametricRuleInBase(method f) +filtered { f -> filterDef(f) } { + env eF; + calldataarg args; + uint256 before = someUInt(); + callF(eF, args, f); + uint256 after = someUInt(); + assert (before >= 7) => (before - after <= 7), "Unexpected result of one call to a parametric function"; } /// @notice f is filtered to `someInt` but g can be any function. -rule twoParametricRuleInBase(method f, method g) filtered { f -> filterDef(f) } -{ - env eF; - calldataarg args; - uint256 before = someUInt(); - callF(eF, args, f); - callF(eF, args, g); - uint256 after = someUInt(); - assert ((before >=7) => (before - after <= 7), "Unexpected result of two calls to parametric functions"); +rule twoParametricRuleInBase(method f, method g) +filtered { f -> filterDef(f) } { + env eF; + calldataarg args; + uint256 before = someUInt(); + callF(eF, args, f); + callF(eF, args, g); + uint256 after = someUInt(); + assert (before >= 7) => (before - after <= 7), "Unexpected result of two calls to parametric functions"; } - - diff --git a/CVLByExample/Import/certora/specs/sub.spec b/CVLByExample/Import/certora/specs/sub.spec index 8d4ea028..0622bc67 100644 --- a/CVLByExample/Import/certora/specs/sub.spec +++ b/CVLByExample/Import/certora/specs/sub.spec @@ -1,24 +1,27 @@ import "base.spec"; // @notice Imports all the elements defined in "base.spec", excluding rules and invariants; methods { - function twiceSomeUInt() external returns uint256 envfree; + function twiceSomeUInt() external returns (uint256) envfree; } // @notice Overriding the definition of `f` from `Base.spec` to `twiceSomeUInt()` override definition filterDef(method f) returns bool = f.selector == sig:twiceSomeUInt().selector; -use invariant invInBase // @notice Imports the invariant invInBase +// @notice Overriding the preserved block in base.spec +use invariant invInBase { - preserved minusSevenSomeUInt() { // @notice Overriding the preserved block in base.spec - requireInvariant dividedBy7(); - require someUInt() > 14; + preserved minusSevenSomeUInt() { + requireInvariant dividedBy7(); + require someUInt() > 14; } -} +} // @notice Imports the invariant invInBase -invariant dividedBy7() twiceSomeUInt() % 7 == 0; +invariant dividedBy7() + twiceSomeUInt() % 7 == 0; -methods { // @notice The methods in the methods block in `base.spec` are automatically added to this block - function plusSevenSomeUInt() external returns (bool) envfree; +methods { + // @notice The methods in the methods block in `base.spec` are automatically added to this block + function plusSevenSomeUInt() external returns (bool) envfree; } use rule ruleInBase; // @notice Imports the rule `ruleInBase` @@ -26,17 +29,19 @@ use rule ruleInBase; // @notice Imports the rule `ruleInBase` use rule parametricRuleInBase; // @notice Imports the rule `parametricRuleInBase` // Returns true when `h` is the function `plusSevenSoneInt`. + definition isPlusSevenSomeUInt(method h) returns bool = h.selector == sig:plusSevenSomeUInt().selector; // Using a definition of the importing spec for overriding the filters from the imported spec. -use rule twoParametricRuleInBase filtered { f -> isPlusSevenSomeUInt(f), // @notice Override the filter of f - g -> filterDef(g) // @notice Add a filter to g (using an overridden definition) - } +use rule twoParametricRuleInBase // @notice Add a filter to g (using an overridden definition) + +filtered { f -> isPlusSevenSomeUInt(f), g -> filterDef(g) } // @notice Override the filter of f // Adding `@withrevert` to the imported function and restricting `msg.value`. // This will revert because callF is non payable so the `require` cannot hold. -override function callF(env eF, calldataarg args, method f) { // @notice Should make ruleInBase fail - require eF.msg.value > 0; - f@withrevert(eF, args); - assert !lastReverted; +override function callF(env eF, calldataarg args, method f) { + // @notice Should make ruleInBase fail + require eF.msg.value > 0; + f@withrevert(eF, args); + assert !lastReverted; } diff --git a/CVLByExample/Invariant/certora/specs/BallGame.spec b/CVLByExample/Invariant/certora/specs/BallGame.spec index deb36b23..262ecf9d 100644 --- a/CVLByExample/Invariant/certora/specs/BallGame.spec +++ b/CVLByExample/Invariant/certora/specs/BallGame.spec @@ -1,8 +1,7 @@ methods { - function ballPosition() external returns(uint8) envfree; + function ballPosition() external returns (uint8) envfree; } /// The ball should never get to player 2 - too weak version. -invariant playerTwoNeverReceivesBall() +invariant playerTwoNeverReceivesBall() ballPosition() != 2; - diff --git a/CVLByExample/Invariant/certora/specs/BallGameCorrect.spec b/CVLByExample/Invariant/certora/specs/BallGameCorrect.spec index 728c61b4..084cda96 100644 --- a/CVLByExample/Invariant/certora/specs/BallGameCorrect.spec +++ b/CVLByExample/Invariant/certora/specs/BallGameCorrect.spec @@ -1,10 +1,8 @@ methods { - function ballPosition() external returns(uint8) envfree; - function pass() external envfree; + function ballPosition() external returns (uint8) envfree; + function pass() external envfree; } /// The ball should never get to player 2 - strenghened invariant -invariant playerTwoNeverReceivesBall() +invariant playerTwoNeverReceivesBall() ballPosition() == 1 || ballPosition() == 3; - - diff --git a/CVLByExample/LastReverted/RevertingConditions.spec b/CVLByExample/LastReverted/RevertingConditions.spec index 0485a977..83cbfd68 100644 --- a/CVLByExample/LastReverted/RevertingConditions.spec +++ b/CVLByExample/LastReverted/RevertingConditions.spec @@ -1,35 +1,27 @@ methods { function balanceOf(address) external returns (uint256) envfree; - function transfer(address,uint256) external returns (bool); - function approve(address,uint256) external returns (bool); + function transfer(address, uint256) external returns (bool); + function approve(address, uint256) external returns (bool); } -rule transferRevertingConditions { +rule transferRevertingConditions() { env e; address recipient; uint256 amount; - require e.msg.sender != recipient; - uint256 balanceBefore = balanceOf(e.msg.sender); - transfer@withrevert(e, recipient, amount); bool transferReverted = lastReverted; - assert to_mathint(balanceOf(e.msg.sender)) > balanceBefore - amount => transferReverted; } -rule approveRevertingConditions { +rule approveRevertingConditions() { env e; address spender; uint256 amount; - require e.msg.value == 0; - bool ownerIsZero = e.msg.sender == 0; bool spenderIsZero = spender == 0; - approve@withrevert(e, spender, amount); - assert lastReverted <=> ownerIsZero || spenderIsZero; -} \ No newline at end of file +} diff --git a/CVLByExample/LastReverted/RevertingConditionsForgotWithRevert.spec b/CVLByExample/LastReverted/RevertingConditionsForgotWithRevert.spec index 7b771849..5dd8fbdf 100644 --- a/CVLByExample/LastReverted/RevertingConditionsForgotWithRevert.spec +++ b/CVLByExample/LastReverted/RevertingConditionsForgotWithRevert.spec @@ -1,34 +1,26 @@ methods { function balanceOf(address) external returns (uint256) envfree; - function transfer(address,uint256) external returns (bool); - function approve(address,uint256) external returns (bool); + function transfer(address, uint256) external returns (bool); + function approve(address, uint256) external returns (bool); } -rule transferRevertingConditions { +rule transferRevertingConditions() { env e; address recipient; uint256 amount; - require e.msg.sender != recipient; - uint256 balanceBefore = balanceOf(e.msg.sender); - transfer@withrevert(e, recipient, amount); - assert to_mathint(balanceOf(e.msg.sender)) > balanceBefore - amount => lastReverted; } -rule approveRevertingConditions { +rule approveRevertingConditions() { env e; address spender; uint256 amount; - require e.msg.value == 0; - bool ownerIsZero = e.msg.sender == 0; bool spenderIsZero = spender == 0; - approve@withrevert(e, spender, amount); - assert lastReverted <=> ownerIsZero || spenderIsZero; -} \ No newline at end of file +} diff --git a/CVLByExample/NativeBalances/certora/specs/Auction.spec b/CVLByExample/NativeBalances/certora/specs/Auction.spec index f6ee6195..3cecc68d 100644 --- a/CVLByExample/NativeBalances/certora/specs/Auction.spec +++ b/CVLByExample/NativeBalances/certora/specs/Auction.spec @@ -5,7 +5,7 @@ */ methods { - function currentBid() external returns uint256 envfree; + function currentBid() external returns (uint256) envfree; } /// @title Basic rules //////////////////////////////////////////////////// @@ -20,7 +20,7 @@ methods { rule bidIncreasesAssets() { env e; require(e.msg.sender != currentContract); - require(e.msg.value > currentBid() ); + require(e.msg.value > currentBid()); uint256 balanceBefore = nativeBalances[currentContract]; bid(e); assert nativeBalances[currentContract] > balanceBefore; @@ -37,8 +37,8 @@ rule bidSuccessfullyExpectVacuous() { env e; uint256 balanceBefore = nativeBalances[currentContract]; require(e.msg.sender != currentContract); - require(e.msg.value > 0 && e.msg.value > balanceBefore); - require (balanceBefore > 0); + require(e.msg.value > 0 && e.msg.value > balanceBefore); + require(balanceBefore > 0); bid(e); assert nativeBalances[currentContract] >= balanceBefore; } diff --git a/CVLByExample/NativeCodeSize/NativeCodesize.spec b/CVLByExample/NativeCodeSize/NativeCodesize.spec index f3cb7393..4f769d26 100644 --- a/CVLByExample/NativeCodeSize/NativeCodesize.spec +++ b/CVLByExample/NativeCodeSize/NativeCodesize.spec @@ -4,4 +4,4 @@ rule nativeCodesizeContractExample(env e) { rule nativeCodesizeEOAExample(env e) { assert nativeCodesize[e.msg.sender] == 0 => e.msg.sender != currentContract; // EOA address therefore cant be the current contract -} \ No newline at end of file +} diff --git a/CVLByExample/Optional/certora/specs/Base.spec b/CVLByExample/Optional/certora/specs/Base.spec index 09f672df..f37b3b05 100644 --- a/CVLByExample/Optional/certora/specs/Base.spec +++ b/CVLByExample/Optional/certora/specs/Base.spec @@ -1,9 +1,9 @@ - methods { + // `optional` makes the run skip the call to `bar` when `Partial` is the contract used in the `verify` option, because // `bar()` is not defined in `Partial`. - function bar(uint256 _x) external returns(uint256) envfree optional; - function foo(uint256 _x) external returns(uint256) envfree; + function bar(uint256 _x) external returns (uint256) envfree optional; + function foo(uint256 _x) external returns (uint256) envfree; } /** @@ -16,24 +16,23 @@ methods { // When the main contract is `Base` the rule passes. // When the main contract is `Partial` this rule is skipped. rule checkBar() { - bar@withrevert(5); - satisfy true; + bar@withrevert(5); + satisfy true; } // When the main contract is `Partial` the rule instantiates only the functions present in `Partial` and passes. rule parametericCheckBar(method f) { - calldataarg args; - env e; - f(e,args); - satisfy true; + calldataarg args; + env e; + f(e, args); + satisfy true; } // One of the functions is not defined in `Partial`. // When the main contract is `Base` the rule passes. // When the main contract is `Partial` the rule is skipped. rule useBothFunctions(uint256 x) { - uint256 fooResult = foo(require_uint256(x + 45)); // This is performed in both contracts because `foo` is defined. - uint256 barResult = bar(x); - - assert (fooResult == barResult, "Functions have different results"); + uint256 fooResult = foo(require_uint256(x + 45)); // This is performed in both contracts because `foo` is defined. + uint256 barResult = bar(x); + assert fooResult == barResult, "Functions have different results"; } diff --git a/CVLByExample/PreciseBitwiseOps/PreciseBitwiseOps.spec b/CVLByExample/PreciseBitwiseOps/PreciseBitwiseOps.spec index e976acf2..c7358bef 100644 --- a/CVLByExample/PreciseBitwiseOps/PreciseBitwiseOps.spec +++ b/CVLByExample/PreciseBitwiseOps/PreciseBitwiseOps.spec @@ -1,12 +1,10 @@ methods { function setBorrowing(uint256, bool) external envfree; - function isBorrowing(uint256) external returns bool envfree; + function isBorrowing(uint256) external returns (bool) envfree; } - // checks the integrity of set Borrowing function and correct retrieval of the corresponding getter -rule setBorrowing(uint256 reserveIndex, bool borrowing) -{ - setBorrowing(reserveIndex, borrowing); - assert isBorrowing(reserveIndex) == borrowing, "unexpected result"; -} \ No newline at end of file +rule setBorrowing(uint256 reserveIndex, bool borrowing) { + setBorrowing(reserveIndex, borrowing); + assert isBorrowing(reserveIndex) == borrowing, "unexpected result"; +} diff --git a/CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec b/CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec index 2122829e..32470ee8 100644 --- a/CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec +++ b/CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec @@ -12,21 +12,27 @@ methods { ghost mapping(address => address) ghostNext { init_state axiom forall address x. ghostNext[x] == 0; } + ghost mapping(address => address) ghostPrev { init_state axiom forall address x. ghostPrev[x] == 0; } + ghost mapping(address => uint256) ghostValue { init_state axiom forall address x. ghostValue[x] == 0; } + ghost address ghostHead { init_state axiom ghostHead == 0; } + ghost address ghostTail { init_state axiom ghostTail == 0; } + ghost nextstar(address, address) returns bool { init_state axiom forall address x. forall address y. nextstar(x, y) == (x == y); } + ghost prevstar(address, address) returns bool { init_state axiom forall address x. forall address y. prevstar(x, y) == (x == y); } @@ -36,6 +42,7 @@ ghost prevstar(address, address) returns bool { hook Sstore currentContract.dll.head address newHead { ghostHead = newHead; } + hook Sstore currentContract.dll.tail address newTail { ghostTail = newTail; } @@ -47,6 +54,7 @@ hook Sstore currentContract.dll.accounts[KEY address key].next address newNext { hook Sstore currentContract.dll.accounts[KEY address key].prev address newPrev { ghostPrev[key] = newPrev; } + hook Sstore currentContract.dll.accounts[KEY address key].value uint256 newValue { ghostValue[key] = newValue; } @@ -54,15 +62,19 @@ hook Sstore currentContract.dll.accounts[KEY address key].value uint256 newValue hook Sload address head currentContract.dll.head { require ghostHead == head; } + hook Sload address tail currentContract.dll.tail { require ghostTail == tail; } + hook Sload address next currentContract.dll.accounts[KEY address key].next { require ghostNext[key] == next; } + hook Sload address prev currentContract.dll.accounts[KEY address key].prev { require ghostPrev[key] == prev; } + hook Sload uint256 value currentContract.dll.accounts[KEY address key].value { require ghostValue[key] == value; } @@ -70,44 +82,34 @@ hook Sload uint256 value currentContract.dll.accounts[KEY address key].value { // INVARIANTS invariant nextPrevMatch() + // either list is empty, and both head and tail are 0, - ((ghostHead == 0 && ghostTail == 0) - // or both head and tail are set and their prev resp. next points to 0. - || (ghostHead != 0 && ghostTail != 0 && ghostNext[ghostTail] == 0 && ghostPrev[ghostHead] == 0 - && ghostValue[ghostHead] != 0 && ghostValue[ghostTail] != 0)) + // for all addresses: - && (forall address a. - // either the address is not part of the list and every field is 0. - (ghostNext[a] == 0 && ghostPrev[a] == 0 && ghostValue[a] == 0) - // or the address is part of the list, address is non-zero, value is non-zero, - // and prev and next pointer are linked correctly. - || (a != 0 && ghostValue[a] != 0 - && ((a == ghostHead && ghostPrev[a] == 0) || ghostNext[ghostPrev[a]] == a) - && ((a == ghostTail && ghostNext[a] == 0) || ghostPrev[ghostNext[a]] == a))); - + + // or both head and tail are set and their prev resp. next points to 0. + ((ghostHead == 0 && ghostTail == 0) || (ghostHead != 0 && ghostTail != 0 && ghostNext[ghostTail] == 0 && ghostPrev[ghostHead] == 0 && ghostValue[ghostHead] != 0 && ghostValue[ghostTail] != 0)) && (forall address a. + // or the address is part of the list, address is non-zero, value is non-zero, + // and prev and next pointer are linked correctly. + (ghostNext[a] == 0 && ghostPrev[a] == 0 && ghostValue[a] == 0) || (a != 0 && ghostValue[a] != 0 && ((a == ghostHead && ghostPrev[a] == 0) || ghostNext[ghostPrev[a]] == a) && ((a == ghostTail && ghostNext[a] == 0) || ghostPrev[ghostNext[a]] == a))) + // either the address is not part of the list and every field is 0. + ; invariant inList() - (ghostHead != 0 => ghostValue[ghostHead] != 0) - && (ghostTail != 0 => ghostValue[ghostTail] != 0) - && (forall address a. ghostNext[a] != 0 => ghostValue[ghostNext[a]] != 0) - && (forall address a. ghostPrev[a] != 0 => ghostValue[ghostPrev[a]] != 0) - { + (ghostHead != 0 => ghostValue[ghostHead] != 0) && (ghostTail != 0 => ghostValue[ghostTail] != 0) && (forall address a. ghostNext[a] != 0 => ghostValue[ghostNext[a]] != 0) && (forall address a. ghostPrev[a] != 0 => ghostValue[ghostPrev[a]] != 0) { preserved { requireInvariant nextPrevMatch(); } } -rule insert_preserves_old { +rule insert_preserves_old() { address newElem; address oldElem; uint256 newValue; uint256 maxIter; bool oldInList = ghostValue[oldElem] != 0; - require oldElem != newElem; - insertSorted(newElem, newValue, maxIter); - assert oldInList == (ghostValue[oldElem] != 0); } @@ -115,9 +117,7 @@ rule insert_adds_new() { address newElem; uint256 newValue; uint256 maxIter; - insertSorted(newElem, newValue, maxIter); - assert ghostValue[newElem] != 0; assert ghostValue[newElem] == newValue; } @@ -126,43 +126,32 @@ rule insert_does_not_revert() { address newElem; uint256 newValue; uint256 maxIter; - require newElem != 0; require ghostValue[newElem] == 0; require newValue != 0; - insertSorted@withrevert(newElem, newValue, maxIter); - assert !lastReverted; } -rule remove_preserves_old { +rule remove_preserves_old() { address elem; address oldElem; bool oldInList = ghostValue[oldElem] != 0; - require oldElem != elem; - remove(elem); - assert oldInList == (ghostValue[oldElem] != 0); } rule remove_deletes() { address elem; - remove(elem); - assert ghostValue[elem] == 0; } rule remove_does_not_revert() { address elem; - require elem != 0; require ghostValue[elem] != 0; - remove@withrevert(elem); - assert !lastReverted; } diff --git a/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec b/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec index 04b9aea2..f77996be 100644 --- a/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec +++ b/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec @@ -16,10 +16,12 @@ methods { ghost mapping(mathint => bytes32) ghostValues { init_state axiom forall mathint x. ghostValues[x] == to_bytes32(0); } + // ghost field for the indexes map ghost mapping(bytes32 => uint256) ghostIndexes { init_state axiom forall bytes32 x. ghostIndexes[x] == 0; } + // ghost field for the length of the values array (stored in offset 0) ghost uint256 ghostLength { init_state axiom ghostLength == 0; @@ -32,10 +34,12 @@ ghost uint256 ghostLength { hook Sstore currentContract.set._inner._values.length uint256 newLength { ghostLength = newLength; } + // Store hook to synchronize ghostValues array with set._inner._values. hook Sstore currentContract.set._inner._values[INDEX uint256 index] bytes32 newValue { ghostValues[index] = newValue; } + // Store hook to synchronize ghostIndexes array with set._inner._indexes. hook Sstore currentContract.set._inner._indexes[KEY bytes32 value] uint256 newIndex { ghostIndexes[value] = newIndex; @@ -53,9 +57,11 @@ hook Sstore currentContract.set._inner._indexes[KEY bytes32 value] uint256 newIn hook Sload uint256 length currentContract.set._inner._values.length { require ghostLength == length; } + hook Sload bytes32 value currentContract.set._inner._values[INDEX uint256 index] { require ghostValues[index] == value; } + hook Sload uint256 index currentContract.set._inner._indexes[KEY bytes32 value] { require ghostIndexes[value] == index; } @@ -67,151 +73,114 @@ hook Sload uint256 index currentContract.set._inner._indexes[KEY bytes32 value] // and indexes[values[i]] = i+1 for all valid indexes i. invariant setInvariant() - (forall uint256 index. 0 <= index && index < ghostLength => to_mathint(ghostIndexes[ghostValues[index]]) == index + 1) - && (forall bytes32 value. ghostIndexes[value] == 0 || - (ghostValues[ghostIndexes[value] - 1] == value && ghostIndexes[value] >= 1 && ghostIndexes[value] <= ghostLength)); + (forall uint256 index. 0 <= index && index < ghostLength => to_mathint(ghostIndexes[ghostValues[index]]) == index + 1) && (forall bytes32 value. ghostIndexes[value] == 0 || (ghostValues[ghostIndexes[value] - 1] == value && ghostIndexes[value] >= 1 && ghostIndexes[value] <= ghostLength)); // DEFINITION // Returns, whether a value is in the set. definition inSet(bytes32 value) returns bool = (ghostIndexes[value] != 0); - // RULES -rule containsEqualsInSet() -{ +rule containsEqualsInSet() { bytes32 value; bool result = contains@withrevert(value); - assert !lastReverted, "contains should never revert"; assert result == inSet(value), "result should indicate whether value is in set"; } -rule lengthEqualsGhost() -{ +rule lengthEqualsGhost() { uint256 len = length@withrevert(); assert !lastReverted, "length() should never revert"; assert len == ghostLength, "length() should return the length of the values list"; } -rule addFresh() -{ +rule addFresh() { bytes32 value; bytes32 other; - require other != value; - require !inSet(value); bool otherInSet = inSet(other); bool result = add@withrevert(value); - assert !lastReverted, "addFresh() should never revert"; assert result && inSet(value), "value should have been added to list"; assert otherInSet == inSet(other), "no other value should be added or removed"; } -rule addAlreadyIn() -{ +rule addAlreadyIn() { bytes32 value; bytes32 other; - require other != value; - require inSet(value); bool otherInSet = inSet(other); bool result = add@withrevert(value); - assert !lastReverted, "addFresh() should never revert"; assert !result && inSet(value), "addFresh should return false if element in list"; assert otherInSet == inSet(other), "no other value should be added or removed"; } -rule removeSuccess() -{ +rule removeSuccess() { bytes32 value; bytes32 other; - requireInvariant setInvariant(); require other != value; - require inSet(value); bool otherInSet = inSet(other); bool result = remove@withrevert(value); - assert !lastReverted, "remove() should never revert"; assert result && !inSet(value), "remove should remove element from list"; assert otherInSet == inSet(other), "no other value should be added or removed"; } -rule removeFail() -{ +rule removeFail() { bytes32 value; bytes32 other; - require other != value; - require !inSet(value); bool otherInSet = inSet(other); bool result = remove@withrevert(value); - assert !lastReverted, "remove() should never revert"; assert !result && !inSet(value), "remove should return false if element was not in list"; assert otherInSet == inSet(other), "no other value should be added or removed"; } -rule elemAtSuccess() -{ +rule elemAtSuccess() { bytes32 value; uint256 index; - requireInvariant setInvariant(); require index < ghostLength; - value = elemAt@withrevert(index); - assert !lastReverted, "elemAt() should not revert for valid index"; assert inSet(value), "elemAt() should return a value from the set"; } -rule elemAtFail() -{ +rule elemAtFail() { bytes32 value; uint256 index; - require index >= ghostLength; - value = elemAt@withrevert(index); - assert lastReverted, "elemAt() should revert for invalid index"; } -rule elementsUnique() -{ +rule elementsUnique() { bytes32 value1; bytes32 value2; uint256 index1; uint256 index2; - requireInvariant setInvariant(); require index1 != index2; - value1 = elemAt(index1); value2 = elemAt(index2); - assert value1 != value2, "all elements in the list should be different"; } -rule everyElementReachable() -{ +rule everyElementReachable() { bytes32 value; bytes32 result; uint256 index; - requireInvariant setInvariant(); require inSet(value); index = assert_uint256(ghostIndexes[value] - 1); - result = elemAt@withrevert(index); assert !lastReverted, "elemAt should not revert for valid index"; assert result == value, "every value should be at its corresponding index"; diff --git a/CVLByExample/QuantifierExamples/SinglyLinkedList/certora/spec/list-reach.spec b/CVLByExample/QuantifierExamples/SinglyLinkedList/certora/spec/list-reach.spec index 4d541d1a..63612d02 100644 --- a/CVLByExample/QuantifierExamples/SinglyLinkedList/certora/spec/list-reach.spec +++ b/CVLByExample/QuantifierExamples/SinglyLinkedList/certora/spec/list-reach.spec @@ -1,6 +1,5 @@ // Specification for reachability for a linked list implementation. - // Method block: all methods don't need environment methods { @@ -35,26 +34,19 @@ ghost bytes32 ghostHead { definition isSucc(bytes32 a, bytes32 b) returns bool = reach(a, b) && a != b && (forall bytes32 X. reach(a, X) && reach(X, b) => (a == X || b == X)); -definition reachSuccInvariant(bytes32 key) returns bool = - (key == to_bytes32(0) && ghostSucc[key] == to_bytes32(0)) - || (key != to_bytes32(0) && isSucc(key, ghostSucc[key])); +definition reachSuccInvariant(bytes32 key) returns bool = (key == to_bytes32(0) && ghostSucc[key] == to_bytes32(0)) || (key != to_bytes32(0) && isSucc(key, ghostSucc[key])); -definition updateSucc(bytes32 a, bytes32 b) returns bool = forall bytes32 X. forall bytes32 Y. reach@new(X, Y) == - (X == Y || - (reach@old(X, Y) && !(reach@old(X, a) && a != Y && reach@old(a, Y))) || - (reach@old(X, a) && reach@old(b, Y))); +definition updateSucc(bytes32 a, bytes32 b) returns bool = forall bytes32 X. forall bytes32 Y. reach@new(X, Y) == (X == Y || (reach@old(X, Y) && !(reach@old(X, a) && a != Y && reach@old(a, Y))) || (reach@old(X, a) && reach@old(b, Y))); hook Sstore currentContract.list.elements[KEY bytes32 key].nextKey bytes32 newNextKey { bytes32 otherKey; - require reachSuccInvariant(otherKey); - assert !reach(newNextKey,key), "Setting next introduces cycle"; - + assert !reach(newNextKey, key), "Setting next introduces cycle"; + // update ghost successor ghostSucc[key] = newNextKey; // update ghost reachability havoc reach assuming updateSucc(key, newNextKey); - assert reachSuccInvariant(otherKey), "Successor invariant not preserved"; } @@ -79,38 +71,29 @@ hook Sload uint256 valueValid currentContract.list.elements[KEY bytes32 key].val require valueValid != 0 <=> ghostValid[key]; } - invariant inListIffValid() - forall bytes32 key. key != to_bytes32(0) => ghostValid[key] == reach(ghostHead, key) - { + forall bytes32 key. key != to_bytes32(0) => ghostValid[key] == reach(ghostHead, key) { preserved { requireInvariant reach_invariant(); } } invariant reach_invariant() - forall bytes32 X. forall bytes32 Y. forall bytes32 Z. ( - reach(X, X) - && (reach(X,Y) && reach (Y, X) => X == Y) - && (reach(X,Y) && reach (Y, Z) => reach(X, Z)) - && (reach(X,Y) && reach (X, Z) => (reach(Y,Z) || reach(Z,Y))) - ) - { + forall bytes32 X. forall bytes32 Y. forall bytes32 Z. (reach(X, X) && (reach(X, Y) && reach(Y, X) => X == Y) && (reach(X, Y) && reach(Y, Z) => reach(X, Z)) && (reach(X, Y) && reach(X, Z) => (reach(Y, Z) || reach(Z, Y)))) { preserved { requireInvariant inListIffValid(); } } invariant reach_succ(bytes32 key) - reachSuccInvariant(key) - { + reachSuccInvariant(key) { preserved { requireInvariant reach_invariant(); requireInvariant inListIffValid(); } } -rule checkGetSucc { +rule checkGetSucc() { bytes32 key; bytes32 afterKey = getSucc(key); requireInvariant reach_invariant(); @@ -119,22 +102,21 @@ rule checkGetSucc { // Rules for full correctness of API calls. -rule checkInsertHead { +rule checkInsertHead() { bytes32 key; bytes32 afterKey; bytes32 headKey = head(); requireInvariant inListIffValid(); requireInvariant reach_invariant(); - + // inserts at head require afterKey == to_bytes32(0); insertAfter(key, afterKey); - assert reach(key, headKey); assert reach(ghostHead, headKey); } -rule checkInsertSuccessor { +rule checkInsertSuccessor() { bytes32 key; bytes32 afterKey; requireInvariant reach_invariant(); @@ -146,51 +128,46 @@ rule checkInsertSuccessor { assert reach(afterKey, key); } - -rule checkInsert { +rule checkInsert() { bytes32 key; bytes32 afterKey; bytes32 randoBoi; requireInvariant reach_invariant(); requireInvariant inListIffValid(); - require reach(ghostHead, randoBoi); insertAfter(key, afterKey); assert reach(ghostHead, randoBoi), "Element from the list was lost"; assert reach(ghostHead, key), "Key was not inserted"; } -rule checkInsertRevertsWhenExists { +rule checkInsertRevertsWhenExists() { bytes32 key; bytes32 afterKey; requireInvariant reach_invariant(); requireInvariant inListIffValid(); require ghostValid[key]; - insertAfter@withrevert(key, afterKey); assert lastReverted, "insert should revert"; } -rule checkInsertRevertsWhenAfterKeyNotExists { +rule checkInsertRevertsWhenAfterKeyNotExists() { bytes32 key; bytes32 afterKey; requireInvariant reach_invariant(); requireInvariant inListIffValid(); require afterKey != to_bytes32(0); require !ghostValid[afterKey]; - insertAfter@withrevert(key, afterKey); assert lastReverted, "insert can revert"; } -rule checkInsertSucceedsOtherwise { +rule checkInsertSucceedsOtherwise() { bytes32 key; bytes32 afterKey; requireInvariant reach_invariant(); requireInvariant inListIffValid(); require afterKey == to_bytes32(0) || ghostValid[afterKey]; require key != to_bytes32(0) && !ghostValid[key]; - insertAfter@withrevert(key, afterKey); assert !lastReverted, "insert should not revert"; } diff --git a/CVLByExample/Reentrancy/certora/spec/NoGuardSafety.spec b/CVLByExample/Reentrancy/certora/spec/NoGuardSafety.spec index cad0f9fb..706d14f3 100644 --- a/CVLByExample/Reentrancy/certora/spec/NoGuardSafety.spec +++ b/CVLByExample/Reentrancy/certora/spec/NoGuardSafety.spec @@ -3,42 +3,42 @@ * We verify this by hooking on calls and store operations, and checking for a call within two store operations. **/ - persistent ghost bool called_extcall; + persistent ghost bool storage_access_before_call; + persistent ghost bool storage_access_after_call; // We are hooking here on "CALL" opcodes in order to capture if there was a storage access before or/and after a call -hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { +hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength, uint rc) { called_extcall = true; } // For every store set storage_access_before_call or storage_access_after_call according to the call state hook ALL_SSTORE(uint loc, uint v) { if (!called_extcall) { - storage_access_before_call = true; + storage_access_before_call = true; } else { - storage_access_after_call = true; + storage_access_after_call = true; } -} +} // For every load set storage_access_before_call or storage_access_after_call according to the call state -hook ALL_SLOAD(uint loc) uint v { +hook ALL_SLOAD(uint loc, uint v) { if (!called_extcall) { - storage_access_before_call = true; + storage_access_before_call = true; } else { - storage_access_after_call = true; + storage_access_after_call = true; } -} +} // Check that after calling a function we are either before or after the `call` rule reentrancySafety(method f) { + // start with all flags false - require !called_extcall && !storage_access_before_call && - !storage_access_after_call; - + require !called_extcall && !storage_access_before_call && !storage_access_after_call; calldataarg args; env e; - f(e,args); + f(e, args); assert !(storage_access_before_call && storage_access_after_call), "Reentrancy weakness exists"; } diff --git a/CVLByExample/Reentrancy/certora/spec/Reentrancy.spec b/CVLByExample/Reentrancy/certora/spec/Reentrancy.spec index 31ebd274..21e70c48 100644 --- a/CVLByExample/Reentrancy/certora/spec/Reentrancy.spec +++ b/CVLByExample/Reentrancy/certora/spec/Reentrancy.spec @@ -1,23 +1,23 @@ persistent ghost bool called_extcall; + persistent ghost bool g_reverted; + persistent ghost uint32 g_sighash; // we are hooking here on "CALL" opcodes in order to simulate reentrancy to a non-view function and check that the function reverts -hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { +hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength, uint rc) { called_extcall = true; env e; bool cond; - if (g_sighash == sig:withdrawAll().selector) { withdrawAll@withrevert(e); // concrete name g_reverted = lastReverted; - } - else if (g_sighash == sig:withdraw(uint256).selector) { + } else if (g_sighash == sig:withdraw(uint256).selector) { calldataarg args; withdraw@withrevert(e, args); // concrete name g_reverted = lastReverted; - } - else { + } else { + // fallback case g_reverted = true; } @@ -26,10 +26,12 @@ hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, ui // The main rule - // we filter only for non-view methods as only state modifying methods // are dangerous for the specific reentrancy scenarios. -rule no_reentrancy(method f, method g) filtered { f-> !f.isView, g -> !g.isView } { +rule no_reentrancy(method f, method g) +filtered { f -> !f.isView, g -> !g.isView } { require !called_extcall; require !g_reverted; - env e; calldataarg args; + env e; + calldataarg args; require g_sighash == g.selector; f@withrevert(e, args); diff --git a/CVLByExample/RevertKeyWord/example.spec b/CVLByExample/RevertKeyWord/example.spec index a6a1f9bf..15863d79 100644 --- a/CVLByExample/RevertKeyWord/example.spec +++ b/CVLByExample/RevertKeyWord/example.spec @@ -2,10 +2,11 @@ // 1. Declare the contract methods we want to verify/inspect // --------------------------------------------------------- methods { + // Contract functions that may revert function foo(bool) external envfree; - function canRevert(bool) external returns bool envfree; - + function canRevert(bool) external returns (bool) envfree; + // For demonstrating summary usage function callSummarizeMe(bool) external envfree; function summarizeMe(bool b) external => cvlSummarizeMe(b); @@ -35,11 +36,11 @@ function cvlSummarizeMe(bool b) { // --------------------------------------------------------- // 4. Example rule: calling 'foo' with @withrevert // --------------------------------------------------------- -rule testFooWithRevert { +rule testFooWithRevert() { bool condition; // Using @withrevert to capture whether 'foo' reverts foo@withrevert(condition); - + // 'foo' reverts when 'condition' is false assert lastReverted <=> !condition; } @@ -47,11 +48,11 @@ rule testFooWithRevert { // --------------------------------------------------------- // 5. Example rule: calling a CVL function with @withrevert // --------------------------------------------------------- -rule testCvlFunctionWithRevert { +rule testCvlFunctionWithRevert() { bool condition; // If 'cvlFunctionThatMayRevert' reverts, 'lastReverted' is set to true cvlFunctionThatMayRevert@withrevert(condition); - + // Check that 'lastReverted' matches whether 'condition' was false assert lastReverted <=> !condition; } @@ -60,15 +61,16 @@ rule testCvlFunctionWithRevert { // 6. Demonstration #1 for canRevert: inline approach // --------------------------------------------------------- function wrapperForCanRevertInline(bool condition) returns bool { + // Here we call canRevert WITH @withrevert internally canRevert@withrevert(condition); return lastReverted; // We return the revert status } -rule testCanRevertInline { +rule testCanRevertInline() { bool condition; bool outcome = wrapperForCanRevertInline(condition); - + // 'outcome' is true exactly when 'condition' is false (i.e., canRevert reverts) assert outcome <=> !condition; } @@ -82,11 +84,11 @@ function wrapperForCanRevertBubble(bool condition) { canRevert(condition); } -rule testCanRevertBubbleUp { +rule testCanRevertBubbleUp() { bool condition; // We call the wrapper with @withrevert, so if 'canRevert' reverts, it bubbles up wrapperForCanRevertBubble@withrevert(condition); - + // If 'condition' is false => 'canRevert' reverts => bubble up => lastReverted = true assert lastReverted <=> !condition; } @@ -97,12 +99,12 @@ rule testCanRevertBubbleUp { // The contract function callSummarizeMe(b) calls summarizeMe(b), // which is summarized by cvlSummarizeMe(b). That summary reverts // if b == false. We'll use the 'rule sanity basic' flag to see the call trace. -rule testCallSummarizeMe{ +rule testCallSummarizeMe() { bool condition; // Because summarizeMe is mapped to cvlSummarizeMe in CVL (which can revert), -// calling callSummarizeMe with @withrevert will set lastReverted if condition == false. + // calling callSummarizeMe with @withrevert will set lastReverted if condition == false. callSummarizeMe@withrevert(condition); - + // If condition is false => revert => lastReverted = true // If condition is true => no revert => lastReverted = false assert lastReverted <=> !condition; diff --git a/CVLByExample/Storage/certora/specs/storage.spec b/CVLByExample/Storage/certora/specs/storage.spec index ff2fabac..64ba3bf6 100644 --- a/CVLByExample/Storage/certora/specs/storage.spec +++ b/CVLByExample/Storage/certora/specs/storage.spec @@ -8,11 +8,11 @@ 3. The relation between the balances of the sender and the receiver of a transaction. 4. Changes in ghost storage. */ - + using Bank as bank; methods { - function balanceOfAccount(address user, uint account) external returns(uint) envfree; + function balanceOfAccount(address user, uint account) external returns (uint) envfree; /// Definition of a function with struct as an argument function addCustomer(BankAccountRecord.Customer) external envfree; function getNumberOfAccounts(address) external returns (uint256) envfree; @@ -29,7 +29,7 @@ rule storageChangesByWithdrawFromNonEmptyAccount() { require balanceOfAccount(e.msg.sender, accountNum) > 0; withdraw(e, accountNum); storage after = lastStorage; - assert (init != after, "withdraw from non-empty account does not change storage"); + assert init != after, "withdraw from non-empty account does not change storage"; } /// This rule demonstrates comparing full storage after a transaction with possible revert. @@ -40,10 +40,9 @@ rule storageDoesNotChangeByWithdrawWhenRevert() { env e; storage init = lastStorage; uint256 accountNum; - withdraw@withrevert(e, accountNum); storage after = lastStorage; - assert (lastReverted => init == after, "Storage changes after revert."); + assert lastReverted => init == after, "Storage changes after revert."; } /// This rule demonstrates how to verify changes in the full storage when changing data structures of the current contract. @@ -55,7 +54,7 @@ rule addingCustomersChangesStorage(BankAccountRecord.Customer c1, BankAccountRec storage afterC1 = lastStorage; addCustomer(c2); storage afterC2 = lastStorage; - assert (afterC1 != afterC2, "Storage after adding one customer is the same as storage after adding two."); + assert afterC1 != afterC2, "Storage after adding one customer is the same as storage after adding two."; } /// Witness for different storage after each customer addition. @@ -81,17 +80,16 @@ rule integrityOfStoragePerCustomer(BankAccountRecord.Customer c1, BankAccountRec storage afterC1 = lastStorage; addCustomer(c2); storage afterC2 = lastStorage; - + // comparing the storage of `bank` after one and two additions. - assert (afterC1[bank] != afterC2[bank], "Adding a customer does not affect storage of bank"); + assert afterC1[bank] != afterC2[bank], "Adding a customer does not affect storage of bank"; // comparing the storage of the current contract to its storage at the initial state. // currentContract is the same as `bank`. - assert (init[currentContract] != lastStorage[currentContract], "Adding a customer does not affect storage of the current contract"); + assert init[currentContract] != lastStorage[currentContract], "Adding a customer does not affect storage of the current contract"; // comparing the storage of the nativeBalances to nativeBalances at the initial state. - assert (init[nativeBalances] == lastStorage[nativeBalances], "Change in storage affects native balances"); + assert init[nativeBalances] == lastStorage[nativeBalances], "Change in storage affects native balances"; } - /// This rule demonstrates how to call `deposit` (can be any transaction) twice from the same state by restoring the storage to /// its initial state before the second call. rule storageAfterTwoDepositFromInitDoesNotChange() { @@ -107,10 +105,9 @@ rule storageAfterTwoDepositFromInitDoesNotChange() { // corresponds to a single entry is used instead. uint256 afterCallBalance = nativeBalances[bank]; deposit(e, bankAccount) at initStorage; - assert (nativeBalances[bank] == afterCallBalance, "Different native balances from same initial storage"); - assert(lastStorage[bank] == afterCallStorage[bank], "Different native storage from same initial storage"); - assert(lastStorage[nativeBalances] == afterCallStorage[nativeBalances], - "Different storage of native balances after call from same initial storage"); + assert nativeBalances[bank] == afterCallBalance, "Different native balances from same initial storage"; + assert lastStorage[bank] == afterCallStorage[bank], "Different native storage from same initial storage"; + assert lastStorage[nativeBalances] == afterCallStorage[nativeBalances], "Different storage of native balances after call from same initial storage"; } /// Two withdrawals are sequentially called where both start from the initial state. Therefore, the storage after each of the @@ -130,10 +127,9 @@ rule storageAfterTwoWithdrawalsFromInitDoesNotChange() { // corresponds to a single entry is used instead. uint256 afterCallBalance = nativeBalances[bank]; withdraw(e, bankAccount) at initStorage; - assert (nativeBalances[bank] == afterCallBalance, "Different native balances from same initial storage"); - assert(lastStorage[bank] == afterCallStorage[bank], "Different native storage from same initial storage"); - assert(lastStorage[nativeBalances] == afterCallStorage[nativeBalances], - "Different storage of native balances after call from same initial storage"); + assert nativeBalances[bank] == afterCallBalance, "Different native balances from same initial storage"; + assert lastStorage[bank] == afterCallStorage[bank], "Different native storage from same initial storage"; + assert lastStorage[nativeBalances] == afterCallStorage[nativeBalances], "Different storage of native balances after call from same initial storage"; } /// Mirror on a struct _customers[a].accounts[i].accountBalance @@ -148,7 +144,7 @@ ghost mapping(address => mathint) numOfOperations { /// hook on a complex data structure, a mapping to a struct with a dynamic array hook Sstore _customers[KEY address a].accounts[INDEX uint256 i].accountBalance uint256 new_value (uint old_value) { - require old_value == accountBalanceMirror[a][i]; // Need this inorder to sync on insert of new element + require old_value == accountBalanceMirror[a][i]; // Need this inorder to sync on insert of new element accountBalanceMirror[a][i] = new_value; numOfOperations[a] = old_value + 1; } @@ -165,7 +161,5 @@ rule ghostStorageComparison() { // corresponding to a single entry is used instead. deposit(e, bankAccount); storage afterTwoDeposits = lastStorage; - assert(afterTwoDeposits[numOfOperations] == afterOneDeposit[numOfOperations], "ghost storage changes after each deposit"); + assert afterTwoDeposits[numOfOperations] == afterOneDeposit[numOfOperations], "ghost storage changes after each deposit"; } - - diff --git a/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.spec b/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.spec index 69ea61d3..af82c74c 100644 --- a/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.spec +++ b/CVLByExample/Summarization/CalledContractAndExecutingContract/CalledContractAndExecutingContract.spec @@ -10,18 +10,19 @@ // the rules then check that all ghosts are updated correctly. // All assertions should pass. - -using Primary as primary; +using Primary as primary; using Secondary as secondary; -using Tertiary as tertiary; +using Tertiary as tertiary; methods { - function _.calleeInternal() internal with (env e) => saveContracts(calledContract, executingContract, e.msg.sender) expect void; - function _.calleeExternal() external with (env e) => saveContracts(calledContract, executingContract, e.msg.sender) expect void ALL; + function _.calleeInternal() internal with(env e) => saveContracts(calledContract, executingContract, e.msg.sender) expect void; + function _.calleeExternal() external with(env e) => saveContracts(calledContract, executingContract, e.msg.sender) expect void ALL; } ghost address called; + ghost address executing; + ghost address sender; function saveContracts(address _called, address _executing, address _sender) { @@ -94,7 +95,7 @@ rule libraryExternalFromSecondary(env e) { } rule secondaryToPrimaryFromSpec(env e) { - secondary.callPrimaryExternal(e,primary); + secondary.callPrimaryExternal(e, primary); assert called == primary; assert executing == secondary; assert sender == secondary; diff --git a/CVLByExample/Summarization/GhostSummary/GhostMapping/certora/specs/NotSummarized.spec b/CVLByExample/Summarization/GhostSummary/GhostMapping/certora/specs/NotSummarized.spec index 29ccd880..5eea948b 100644 --- a/CVLByExample/Summarization/GhostSummary/GhostMapping/certora/specs/NotSummarized.spec +++ b/CVLByExample/Summarization/GhostSummary/GhostMapping/certora/specs/NotSummarized.spec @@ -1,14 +1,14 @@ methods { - function balance(address account) external returns(uint256) envfree; + function balance(address account) external returns (uint256) envfree; function advanceDays(uint256 n) external envfree; } // A rule for verifying that balance calculation is monotonic with respect to time. // This rule fails because of the overapproximation done by the solver. rule yield_monotonic(address a, uint256 n) { - uint256 y1 = balance(a); - require n >= 0; - advanceDays(n); - uint256 y2 = balance(a); - assert (y2 >= y1, "balance is not monotonic with respect to time"); + uint256 y1 = balance(a); + require n >= 0; + advanceDays(n); + uint256 y2 = balance(a); + assert y2 >= y1, "balance is not monotonic with respect to time"; } diff --git a/CVLByExample/Summarization/GhostSummary/GhostMapping/certora/specs/WithGhostSummary.spec b/CVLByExample/Summarization/GhostSummary/GhostMapping/certora/specs/WithGhostSummary.spec index c1644954..9cc99d7a 100644 --- a/CVLByExample/Summarization/GhostSummary/GhostMapping/certora/specs/WithGhostSummary.spec +++ b/CVLByExample/Summarization/GhostSummary/GhostMapping/certora/specs/WithGhostSummary.spec @@ -1,27 +1,27 @@ methods { - // tell the tool to use a ghost function as the summary for the function - function continuous_interest(uint256 p, uint256 r, uint256 t) internal returns (uint256) => - ghost_interest[p][r][t]; - function balance(address account) external returns(uint256) envfree; + + // tell the tool to use a ghost function as the summary for the function + function continuous_interest(uint256 p, uint256 r, uint256 t) internal returns (uint256) => ghost_interest[p][r][t]; + function balance(address account) external returns (uint256) envfree; function advanceDays(uint256 n) external envfree; } // define the ghost function ghost mapping(uint256 => mapping(uint256 => mapping(uint256 => uint256))) ghost_interest { - // add an axiom describing monotonicity of ghost_interest - axiom forall uint256 p. forall uint256 r. forall uint256 t1. forall uint256 t2. - t2 >= t1 => ghost_interest[p][r][t2] >= ghost_interest[p][r][t1]; + + // add an axiom describing monotonicity of ghost_interest + axiom forall uint256 p. forall uint256 r. forall uint256 t1. forall uint256 t2. t2 >= t1 => ghost_interest[p][r][t2] >= ghost_interest[p][r][t1]; } rule yield_monotonic(address a, uint256 n) { - // internally, when this calls continuous_interest, the function will - // be summarized as ghost_interest - uint256 y1 = balance(a); - require n >= 0; - advanceDays(n); - // internally, when this calls continuous_interest, the function will - // be summarized as ghost_interest - uint256 y2 = balance(a); - assert (y2 >= y1, "balance is not monotonic with respect to time"); + + // internally, when this calls continuous_interest, the function will + // be summarized as ghost_interest + uint256 y1 = balance(a); + require n >= 0; + advanceDays(n); + // internally, when this calls continuous_interest, the function will + // be summarized as ghost_interest + uint256 y2 = balance(a); + assert y2 >= y1, "balance is not monotonic with respect to time"; } - diff --git a/CVLByExample/Summarization/GhostSummary/GhostSums/ghostSums.spec b/CVLByExample/Summarization/GhostSummary/GhostSums/ghostSums.spec index 14f4ee2e..0ab4cf5f 100644 --- a/CVLByExample/Summarization/GhostSummary/GhostSums/ghostSums.spec +++ b/CVLByExample/Summarization/GhostSummary/GhostSums/ghostSums.spec @@ -6,7 +6,7 @@ hook Sstore currentContract.balances[KEY address a] uint256 newVal { mirrorBalances[a] = newVal; } -hook Sload uint256 val currentContract.balances[KEY address a] { +hook Sload uint256 val currentContract.balances[KEY address a] { require mirrorBalances[a] == val; } diff --git a/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/SummarizedSqrRoot.spec b/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/SummarizedSqrRoot.spec index 048d3d1c..3372adf8 100644 --- a/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/SummarizedSqrRoot.spec +++ b/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/SummarizedSqrRoot.spec @@ -3,11 +3,12 @@ methods { } // A precise summarization of sqrt -ghost floorSqrt(uint256) returns uint256 { - // sqrt(x)^2 <= x - axiom forall uint256 x. floorSqrt(x)*floorSqrt(x) <= to_mathint(x) && - // sqrt(x+1)^2 > x - (floorSqrt(x) + 1)*(floorSqrt(x) + 1) > to_mathint(x); +ghost floorSqrt(uint256) returns uint256 { + + // sqrt(x)^2 <= x + axiom forall uint256 x. floorSqrt(x) * floorSqrt(x) <= to_mathint(x) && (floorSqrt(x) + 1) * (floorSqrt(x) + 1) > to_mathint(x) + // sqrt(x+1)^2 > x + ; } rule addLiquidityMonotonicity(uint256 amount0, uint256 amount1, uint256 amount2, uint256 amount3) { @@ -15,7 +16,5 @@ rule addLiquidityMonotonicity(uint256 amount0, uint256 amount1, uint256 amount2, storage initStorage = lastStorage; uint256 firstAdd = addLiquidity(e, amount0, amount1); uint256 secondAdd = addLiquidity(e, amount2, amount3) at initStorage; - assert ((amount0 <= amount2 || amount1 <= amount3) => - (firstAdd <= secondAdd), - "addLiquidity is not monotonic"); + assert (amount0 <= amount2 || amount1 <= amount3) => (firstAdd <= secondAdd), "addLiquidity is not monotonic"; } diff --git a/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/UnsummarizedSqrRoot.spec b/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/UnsummarizedSqrRoot.spec index 0ec58611..087bc070 100644 --- a/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/UnsummarizedSqrRoot.spec +++ b/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/UnsummarizedSqrRoot.spec @@ -3,7 +3,5 @@ rule addLiquidityMonotonicity(uint256 amount0, uint256 amount1, uint256 amount2, storage initStorage = lastStorage; uint256 firstAdd = addLiquidity(e, amount0, amount1); uint256 secondAdd = addLiquidity(e, amount2, amount3) at initStorage; - assert ((amount0 <= amount2 || amount1 <= amount3) => - (firstAdd <= secondAdd), - "addLiquidity is not monotonic"); + assert (amount0 <= amount2 || amount1 <= amount3) => (firstAdd <= secondAdd), "addLiquidity is not monotonic"; } diff --git a/CVLByExample/Summarization/Keywords/certora/specs/AlwaysSummary.spec b/CVLByExample/Summarization/Keywords/certora/specs/AlwaysSummary.spec index be8d38e4..876a43d6 100644 --- a/CVLByExample/Summarization/Keywords/certora/specs/AlwaysSummary.spec +++ b/CVLByExample/Summarization/Keywords/certora/specs/AlwaysSummary.spec @@ -1,15 +1,15 @@ // ALWAYS function summary methods { - function _.get1() external => ALWAYS(7); // Since IntGetter is an interface and not a contract, `_` is the only way to refer to it. - function getFromG1() external returns (uint256) envfree; - function getFromG2() external returns (uint256) envfree; + function _.get1() external => ALWAYS(7); // Since IntGetter is an interface and not a contract, `_` is the only way to refer to it. + function getFromG1() external returns (uint256) envfree; + function getFromG2() external returns (uint256) envfree; } -rule isGet1Always7 { - assert (getFromG1() == 7, "Summaried to 7 but not always 7"); // Should be verified +rule isGet1Always7() { + assert getFromG1() == 7, "Summaried to 7 but not always 7"; // Should be verified } -rule isGet2Always7 { - assert (getFromG2() == 7, "Not summarized not always 7"); // Should be violated +rule isGet2Always7() { + assert getFromG2() == 7, "Not summarized not always 7"; // Should be violated } diff --git a/CVLByExample/Summarization/Keywords/certora/specs/AlwaysVsConstant.spec b/CVLByExample/Summarization/Keywords/certora/specs/AlwaysVsConstant.spec index 6c6de904..0b0c54f2 100644 --- a/CVLByExample/Summarization/Keywords/certora/specs/AlwaysVsConstant.spec +++ b/CVLByExample/Summarization/Keywords/certora/specs/AlwaysVsConstant.spec @@ -1,34 +1,29 @@ - +error dummy file:14:1: Illegal character: ​ +error dummy file:18:1: Illegal character: ​ +error dummy file:23:1: Illegal character: ​ // ALWAYS vs. CONSTANT: methods { - function _.get1() external => ALWAYS(7); - function _.get2() external => CONSTANT; - function getFromG1() external returns (uint256) envfree; - function getFromG2() external returns (uint256) envfree; + function _.get1() external => ALWAYS(7); + function _.get2() external => CONSTANT; + function getFromG1() external returns (uint256) envfree; + function getFromG2() external returns (uint256) envfree; } - -​rule constantVsAlways { - assert (getFromG2() == getFromG1(), "getFromG1() != getFromG2()"); // Should be violated +rule constantVsAlways() { + assert getFromG2() == getFromG1(), "getFromG1() != getFromG2()"; // Should be violated } -​rule constantCanbeAnyValue { - satisfy getFromG2() == getFromG1(); +rule constantCanbeAnyValue() { + satisfy getFromG2() == getFromG1(); } - -​rule constantDoesNotChange(method f) { - uint256 g2Before = getFromG2(); - - env e; - calldataarg args; - f(e,args); - - assert getFromG2() == g2Before; +rule constantDoesNotChange(method f) { + uint256 g2Before = getFromG2(); + env e; + calldataarg args; + f(e, args); + assert getFromG2() == g2Before; } - - - diff --git a/CVLByExample/Summarization/Keywords/certora/specs/AssertFalse.spec b/CVLByExample/Summarization/Keywords/certora/specs/AssertFalse.spec index d916e9ea..35d414bf 100644 --- a/CVLByExample/Summarization/Keywords/certora/specs/AssertFalse.spec +++ b/CVLByExample/Summarization/Keywords/certora/specs/AssertFalse.spec @@ -1,13 +1,13 @@ methods { - unresolved external in A.execute(address x, bytes calldata data) => DISPATCH [ + unresolved external in A.execute(address x, bytes calldata data) => DISPATCH[ Dummy._ ] default ASSERT_FALSE; } -rule AssertFalse { +rule AssertFalse() { env e; address x; bytes data; currentContract.execute(e, x, data); - assert true; // This should never be reached because the assert should fail due to no appropriate implementation in Dummy contract to resolve the unresolved call. -} + assert true; // This should never be reached because the assert should fail due to no appropriate implementation in Dummy contract to resolve the unresolved call. +} diff --git a/CVLByExample/Summarization/Keywords/certora/specs/ConstantVSNondet.spec b/CVLByExample/Summarization/Keywords/certora/specs/ConstantVSNondet.spec index 3f4b64ca..8926db60 100644 --- a/CVLByExample/Summarization/Keywords/certora/specs/ConstantVSNondet.spec +++ b/CVLByExample/Summarization/Keywords/certora/specs/ConstantVSNondet.spec @@ -1,20 +1,23 @@ +error dummy file:12:1: Illegal character: ​ +error dummy file:17:1: Illegal character: ​ // CONSTANT vs. NONDET: methods { - function _.get1() external => CONSTANT; - function _.get2() external => NONDET; - - function getFromG1() external returns (uint256) envfree; - function getFromG2() external returns (uint256) envfree; + function _.get1() external => CONSTANT; + function _.get2() external => NONDET; + function getFromG1() external returns (uint256) envfree; + function getFromG2() external returns (uint256) envfree; } -​rule checkConstantSummary { - // Should be verified - two calls return the same value - assert (getFromG1() == getFromG1(), "getFromG1() != getFromG1() with CONSTANT summary"); +rule checkConstantSummary() { + + // Should be verified - two calls return the same value + assert getFromG1() == getFromG1(), "getFromG1() != getFromG1() with CONSTANT summary"; } -​rule checkNondetSummary { - // Should be violated - two calls may return different values - assert (getFromG2() == getFromG2(), "getFromG2() != getFromG2() with NONDET summary"); +rule checkNondetSummary() { + + // Should be violated - two calls may return different values + assert getFromG2() == getFromG2(), "getFromG2() != getFromG2() with NONDET summary"; } diff --git a/CVLByExample/Summarization/Keywords/certora/specs/DispatcherFallbackInlining.spec b/CVLByExample/Summarization/Keywords/certora/specs/DispatcherFallbackInlining.spec index 33c4e15a..f2da1432 100644 --- a/CVLByExample/Summarization/Keywords/certora/specs/DispatcherFallbackInlining.spec +++ b/CVLByExample/Summarization/Keywords/certora/specs/DispatcherFallbackInlining.spec @@ -5,26 +5,22 @@ methods { function _.noSuchFun() external => DISPATCHER(optimistic=false, use_fallback=true); } -rule fallback_should_be_reached_with_flag { +rule fallback_should_be_reached_with_flag() { env e; - + // Instead of linking `CallsExternalContract:a=IntGetterImpl` which would make the callee resolved which would skip the DISPATCHER summary, // do this `require` to force at runtime the callee to always be `IntGetterImpl`. require currentContract.a == impl1; - foo(e); uint n = impl1.var1; assert n == 5; } -rule fallback_should_never_be_reached { +rule fallback_should_never_be_reached() { env e; - require currentContract.a == impl2; - require impl2.anothervar1 != 5; - foo(e); uint n = impl2.anothervar1; assert n != 5; -} \ No newline at end of file +} diff --git a/CVLByExample/Summarization/Keywords/certora/specs/NoSummary.spec b/CVLByExample/Summarization/Keywords/certora/specs/NoSummary.spec index 62a95a86..39b50026 100644 --- a/CVLByExample/Summarization/Keywords/certora/specs/NoSummary.spec +++ b/CVLByExample/Summarization/Keywords/certora/specs/NoSummary.spec @@ -1,8 +1,8 @@ methods { function setXA(uint256) external envfree; - function getXA() external returns(uint256) envfree; + function getXA() external returns (uint256) envfree; function setXB(uint256) external envfree; - function getXB() external returns(uint256) envfree; + function getXB() external returns (uint256) envfree; } /** @@ -12,7 +12,5 @@ rule checkNoSummarization() { uint256 xOfBBefore = getXB(); setXA(5); uint256 xOfBAfter = getXB(); - assert (xOfBBefore == xOfBAfter, "DISPATCHER(true) summarizations changes values of unchanged contract."); + assert xOfBBefore == xOfBAfter, "DISPATCHER(true) summarizations changes values of unchanged contract."; } - - diff --git a/CVLByExample/Summarization/Keywords/certora/specs/NondetVsHavoc.spec b/CVLByExample/Summarization/Keywords/certora/specs/NondetVsHavoc.spec index 00838a08..6060028c 100644 --- a/CVLByExample/Summarization/Keywords/certora/specs/NondetVsHavoc.spec +++ b/CVLByExample/Summarization/Keywords/certora/specs/NondetVsHavoc.spec @@ -1,40 +1,33 @@ +error dummy file:6:2: Illegal character: ​ methods { - function _.set1() external => NONDET; - function _.set2() external => HAVOC_ALL; - function getFromG1() external returns (uint256) envfree; - function getFromG2() external returns (uint256) envfree; -}​ + function _.set1() external => NONDET; + function _.set2() external => HAVOC_ALL; + function getFromG1() external returns (uint256) envfree; + function getFromG2() external returns (uint256) envfree; +} /*** check which function changes which variable in intGetterImpl */ rule checkChangeG1(method f) { - uint256 g1Before = getFromG1(); - - env e; - calldataarg args; - f(e,args); - - uint256 g1After = getFromG1(); - assert (g1Before == g1After, "get1 changed"); // Should fail only on set2 - + uint256 g1Before = getFromG1(); + env e; + calldataarg args; + f(e, args); + uint256 g1After = getFromG1(); + assert g1Before == g1After, "get1 changed"; // Should fail only on set2 + } /*** check which function changes which variable in intGetterImpl */ rule checkChangeG2(method f) { - uint256 g2Before = getFromG2(); - - env e; - calldataarg args; - f(e,args); - - uint256 g2After = getFromG2(); - assert (g2Before == g2After, "get2 changed"); // Should fail only on set2 - + uint256 g2Before = getFromG2(); + env e; + calldataarg args; + f(e, args); + uint256 g2After = getFromG2(); + assert g2Before == g2After, "get2 changed"; // Should fail only on set2 + } - - - - diff --git a/CVLByExample/Summarization/Keywords/certora/specs/WithDispatcher.spec b/CVLByExample/Summarization/Keywords/certora/specs/WithDispatcher.spec index 840b0ec6..5283d634 100644 --- a/CVLByExample/Summarization/Keywords/certora/specs/WithDispatcher.spec +++ b/CVLByExample/Summarization/Keywords/certora/specs/WithDispatcher.spec @@ -2,8 +2,8 @@ methods { function _.x() external => DISPATCHER(true); function _.dummyB() external => DISPATCHER(true); function setXA(uint256 _x) external envfree; - function getXB() external returns(uint256) envfree; - function getDummyB() external returns(uint256) envfree; + function getXB() external returns (uint256) envfree; + function getDummyB() external returns (uint256) envfree; } /** @@ -13,14 +13,12 @@ rule checkDispatcherUnresolvedSummarizationResult() { uint256 xOfBBefore = getXB(); setXA(5); uint256 xOfBAfter = getXB(); - assert (xOfBBefore == xOfBAfter, "DISPATCHER(true) summarizations changes values of unchanged contract."); + assert xOfBBefore == xOfBAfter, "DISPATCHER(true) summarizations changes values of unchanged contract."; } // getDummyB appears only in calleeB so the rule passes also in the configuration where calleeB does not have a link, // since the dispatcher finds only one function with the signature given in the summarization. rule checkDispatcherUniqueSummarizationResult() { uint256 dummyB = getDummyB(); - - assert (dummyB == 222, "DISPATCHER(true) summarizations changes values of unchanged contract."); + assert dummyB == 222, "DISPATCHER(true) summarizations changes values of unchanged contract."; } - diff --git a/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec b/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec index 45f0aaaa..3ef4587b 100644 --- a/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec +++ b/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec @@ -3,33 +3,34 @@ */ methods { + // functions declared in TestLibrary - function TestLibrary.calleeInternal() internal returns bool => ALWAYS(true); + function TestLibrary.calleeInternal() internal returns (bool) => ALWAYS(true); function _.calleeExternal() external => ALWAYS(true) ALL; // functions declared in IUnresolved - function _.calleeOverloadedInInterfaceExternal() external => ALWAYS(true) UNRESOLVED; + function _.calleeOverloadedInInterfaceExternal() external => ALWAYS(true) UNRESOLVED; // functions from the contract Test. - function callInternal() external returns bool; - function callExternal() external returns bool; - function callIOverloadedInInterfaceExternal() external returns bool; + function callInternal() external returns (bool); + function callExternal() external returns (bool); + function callIOverloadedInInterfaceExternal() external returns (bool); } // Call summarized internal function. -rule callInternal(env e) { - assert (callInternal(e), "Internal function summarization is not applied"); +rule callInternal(env e) { + assert callInternal(e), "Internal function summarization is not applied"; } // Call summarized external function -rule callExternal(env e) { - assert (callExternal(e), "External function summarization is not applied"); +rule callExternal(env e) { + assert callExternal(e), "External function summarization is not applied"; } // Call resolved function which is not summarized. -rule callOverloadedInInterfaceExternal(env e) { - assert (callOverloadedInInterfaceExternal(e), "Resolved function is not summarized"); +rule callOverloadedInInterfaceExternal(env e) { + assert callOverloadedInInterfaceExternal(e), "Resolved function is not summarized"; } // Call unresolved and therefore summarized function. -rule callIOverloadedInInterfaceExternal(env e) { - assert (callIOverloadedInInterfaceExternal(e), "Unresolved function not summarized as expected") ; +rule callIOverloadedInInterfaceExternal(env e) { + assert callIOverloadedInInterfaceExternal(e), "Unresolved function not summarized as expected"; } diff --git a/CVLByExample/Summarization/MultiContract/certora/specs/FunctionSummary.spec b/CVLByExample/Summarization/MultiContract/certora/specs/FunctionSummary.spec index cd898871..95ed20bb 100644 --- a/CVLByExample/Summarization/MultiContract/certora/specs/FunctionSummary.spec +++ b/CVLByExample/Summarization/MultiContract/certora/specs/FunctionSummary.spec @@ -3,18 +3,19 @@ */ using Impl1 as impl1; using Impl2 as impl2; + methods { // A wildcard method entry may not specify return types in the method signature. // The summarized functions belong to other contracts and therefore defined as `external`. // Functions of other contracts function _.summarizedByFunction() external => summary() expect uint256 ALL; - function _.notSummarized() external optional envfree; + function _.notSummarized() external optional envfree; // functions of the main contract - function callByFunctionInCalled1() external returns(uint256) envfree; - function callByFunctionInCalled2() external returns(uint256) envfree; - function callnotSummarizedInCalled1() external returns(uint256) envfree; -} + function callByFunctionInCalled1() external returns (uint256) envfree; + function callByFunctionInCalled2() external returns (uint256) envfree; + function callnotSummarizedInCalled1() external returns (uint256) envfree; +} // Function to be used as function summary. function summary() returns uint256 { @@ -22,17 +23,16 @@ function summary() returns uint256 { } // Calling summarized function of `Impl1` contract. Should pass. -rule checkA { - assert (callByFunctionInCalled1() == 6, "Function summary does not work"); +rule checkA() { + assert callByFunctionInCalled1() == 6, "Function summary does not work"; } // Calling summarized function of `Impl2` contract. Should pass. -rule checkB { - assert (callByFunctionInCalled2() == 6, "Function summary does not work"); +rule checkB() { + assert callByFunctionInCalled2() == 6, "Function summary does not work"; } // Not summarized. Should pass. -rule checkNotSummarized(){ - assert (callnotSummarizedInCalled1() == 3, "wrong result for not-summarized function"); +rule checkNotSummarized() { + assert callnotSummarizedInCalled1() == 3, "wrong result for not-summarized function"; } - diff --git a/CVLByExample/Summarization/MultiContract/certora/specs/InternalExternalSummary.spec b/CVLByExample/Summarization/MultiContract/certora/specs/InternalExternalSummary.spec index 6239d354..b8fa0083 100644 --- a/CVLByExample/Summarization/MultiContract/certora/specs/InternalExternalSummary.spec +++ b/CVLByExample/Summarization/MultiContract/certora/specs/InternalExternalSummary.spec @@ -5,51 +5,53 @@ using Impl1 as impl1; using Impl2 as impl2; + methods { - - function Impl1.summarizedExternal() external returns(uint256) envfree => ALWAYS(1); - function Impl2.summarizedExternal() external returns(uint256) envfree; + function Impl1.summarizedExternal() external returns (uint256) envfree => ALWAYS(1); + function Impl2.summarizedExternal() external returns (uint256) envfree; // Methods of the main contract. // If the contract name is omitted, the default is currentContract - function summarizedExternal() external returns(uint256) envfree => ALWAYS(15) ALL; + function summarizedExternal() external returns (uint256) envfree => ALWAYS(15) ALL; // envfree is not allowed on internal functions. - function summarizedInternal() internal returns(uint256) => ALWAYS(16) ALL; - function callSummarizedExternalInCalled1() external returns(uint256) envfree; - function callSummarizedExternalInCalled2() external returns(uint256) envfree; - function callSummarizedExternalInCaller() external returns(uint256) envfree; - function callSummarizedInternalInCaller() external returns(uint256) envfree; + function summarizedInternal() internal returns (uint256) => ALWAYS(16) ALL; + function callSummarizedExternalInCalled1() external returns (uint256) envfree; + function callSummarizedExternalInCalled2() external returns (uint256) envfree; + function callSummarizedExternalInCaller() external returns (uint256) envfree; + function callSummarizedInternalInCaller() external returns (uint256) envfree; } -rule checkExternalSummarizations(){ - // The functions of `impl1` and the current contract are summarized but the function of impl2 is not. - // This call uses the summarization so the assertion should pass. - assert (callSummarizedExternalInCalled1() == 1, "wrong result for summarized function"); +rule checkExternalSummarizations() { + + // The functions of `impl1` and the current contract are summarized but the function of impl2 is not. + // This call uses the summarization so the assertion should pass. + assert callSummarizedExternalInCalled1() == 1, "wrong result for summarized function"; // The following call uses the original function result. Should pass. - assert (callSummarizedExternalInCalled2() == 5, "wrong result for not-summarized function"); + assert callSummarizedExternalInCalled2() == 5, "wrong result for not-summarized function"; } // Shows when external summarization is not applied. rule checkSummarizedExternalInCaller() { + // The call used here calls the external summarizedExternal() which uses the internal summarizedExternal() // which is not summarized. Therefore the assertion fails. - assert (callSummarizedExternalInCaller() == 15, "ALWAYS summary does not apply for external function called from the contract"); + assert callSummarizedExternalInCaller() == 15, "ALWAYS summary does not apply for external function called from the contract"; // If the function is called from CVL rather than from contract code then it is never replaced by a summary. // Therefore this particular one is not replaced. But since the run is with the option `multi_assert_check`, the previous assertion is assumed to hold // when checking the next assertion and therefore it passes. - assert (summarizedExternal() == 15, "ALWAYS summary does not apply for function called from CVL"); + assert summarizedExternal() == 15, "ALWAYS summary does not apply for function called from CVL"; } // The summary does not apply when called from CVL so the rule should fail. rule checkSummarizedCalledFromCVL() { + // If the function is called from CVL rather than from contract code then it is never replaced by a summary. // So this one is not replaced. - assert (summarizedExternal() == 15, "ALWAYS summary does not apply for function called from CVL"); + assert summarizedExternal() == 15, "ALWAYS summary does not apply for function called from CVL"; } // The public function summarizedInternal in contract Main calls the internal function summarizedInternal // which is summarized. rule checkSummarizedInternalInCaller() { env e; - assert (callSummarizedInternalInCaller() == 16, "Summarization of internal function does not take effect."); + assert callSummarizedInternalInCaller() == 16, "Summarization of internal function does not take effect."; } - diff --git a/CVLByExample/Summarization/UserDefinedReturnType/LibraryVSContractSummary.spec b/CVLByExample/Summarization/UserDefinedReturnType/LibraryVSContractSummary.spec index d8204266..69afe413 100644 --- a/CVLByExample/Summarization/UserDefinedReturnType/LibraryVSContractSummary.spec +++ b/CVLByExample/Summarization/UserDefinedReturnType/LibraryVSContractSummary.spec @@ -5,19 +5,19 @@ * location specifiers) then we should summarize both regardless of whether their sighashes are the same or not). */ methods { + // should summarize both contract and lib functions function _.funcWithStruct(CalledLibrary.S s) external => ALWAYS(1) ALL; - + // should summarize both contract and lib functions function _.funcWithEnum(CalledLibrary.E e) external => ALWAYS(4) ALL; - + // should summarize only the lib function function _.funcWithStorage(uint[] storage s) external => ALWAYS(2) ALL; - + // should summarize only the contract function (in the context of a library, no location // means _not_ storage, so that shouldn't be summarized here) function _.funcWithStorage(uint[] s) external => ALWAYS(3) ALL; - function callLibFuncWithStruct(CalledLibrary.S s) external returns (uint) envfree; function callLibFuncWithEnum(CalledLibrary.E e) external returns (uint) envfree; function callLibFuncWithStorage() external returns (uint) envfree; @@ -26,37 +26,36 @@ methods { function callContractFuncWithStorage() external returns (uint) envfree; } -rule r1 { +rule r1() { CalledLibrary.S s; uint v = callLibFuncWithStruct(s); assert v == 1; } -rule r2 { +rule r2() { CalledLibrary.S s; uint v = callContractFuncWithStruct(s); assert v == 1; } -rule r3 { +rule r3() { uint v = callLibFuncWithStorage(); assert v == 2; } -rule r4 { +rule r4() { uint v = callContractFuncWithStorage(); assert v == 3; } -rule r5 { +rule r5() { CalledLibrary.E e; uint v = callLibFuncWithEnum(e); assert v == 4; } -rule r6 { +rule r6() { CalledLibrary.E e; uint v = callContractFuncWithEnum(e); assert v == 4; } - diff --git a/CVLByExample/Summarization/UserDefinedReturnType/UserDefinedTypeSummarization.spec b/CVLByExample/Summarization/UserDefinedReturnType/UserDefinedTypeSummarization.spec index 105607fa..2df2b8d6 100644 --- a/CVLByExample/Summarization/UserDefinedReturnType/UserDefinedTypeSummarization.spec +++ b/CVLByExample/Summarization/UserDefinedReturnType/UserDefinedTypeSummarization.spec @@ -1,22 +1,20 @@ methods { + // Summarized functions from library function CalledLibrary.getLoc(CalledLibrary.S memory record) internal returns (CalledLibrary.E) => getOppositeLoc(record); // A struct return type summarization function CalledLibrary.toStruct(uint256 _x, bool _b, CalledLibrary.E _loc) internal returns (CalledLibrary.S memory) => getDoubledStruct(_x, _b, _loc); // An array return type summarization. - function CalledLibrary.idArray(uint256 min, uint256 max) internal returns (uint256[] memory) => doubledArray(min, max); - + function CalledLibrary.idArray(uint256 min, uint256 max) internal returns (uint256[] memory) => doubledArray(min, max); function callGetLoc(CalledLibrary.S record) external returns (CalledLibrary.E) envfree; function callToStruct(uint256 _x, bool _b, CalledLibrary.E _loc) external returns (CalledLibrary.S memory) envfree; function callIdArray(uint256 min, uint256 max) external returns (uint256[] memory) envfree; - } function getOppositeLoc(CalledLibrary.S s) returns CalledLibrary.E { if (s.loc == CalledLibrary.E.FIRST) { return CalledLibrary.E.SECOND; } - return CalledLibrary.E.FIRST; } @@ -29,23 +27,22 @@ function getDoubledStruct(uint256 _x, bool _b, CalledLibrary.E _loc) returns Cal } function doubledArray(uint256 min, uint256 max) returns uint256[] { - return [0,2]; + return [0, 2]; } rule checkLoc(CalledLibrary.S record) { - assert (callGetLoc(record) != record.loc, "enum function not summarized"); + assert callGetLoc(record) != record.loc, "enum function not summarized"; } rule checkStructField(uint256 _x, bool _b, CalledLibrary.E _loc) { CalledLibrary.S newStruct = callToStruct(_x, _b, _loc); - assert (newStruct.x % 2 == 0, "Summary for struct return type function is not applied"); + assert newStruct.x % 2 == 0, "Summary for struct return type function is not applied"; } rule checkArray() { uint256 min; uint256 max; - require max > min; uint256[] arr = callIdArray(min, max); - assert (arr.length > 0, "Summary for array return type function is not applied"); + assert arr.length > 0, "Summary for array return type function is not applied"; } diff --git a/CVLByExample/Summarization/WildcardVsExact/specs/WildcardVsExact.spec b/CVLByExample/Summarization/WildcardVsExact/specs/WildcardVsExact.spec index cdff934d..a30c1688 100644 --- a/CVLByExample/Summarization/WildcardVsExact/specs/WildcardVsExact.spec +++ b/CVLByExample/Summarization/WildcardVsExact/specs/WildcardVsExact.spec @@ -3,13 +3,13 @@ using B as B; methods { function callAFunc() external returns (uint256) envfree; function _.toBeSummarized() external => ALWAYS(5) ALL; - function B.toBeSummarized() external returns(uint256) => ALWAYS(7) ALL; + function B.toBeSummarized() external returns (uint256) => ALWAYS(7) ALL; } -rule isFive { +rule isFive() { assert callAFunc() == 5; } -rule isSeven { +rule isSeven() { assert callAFunc() == 7; -} \ No newline at end of file +} diff --git a/CVLByExample/Summarization/WithEnv/WithEnvCVLFunctionSummary/withEnvSummary.spec b/CVLByExample/Summarization/WithEnv/WithEnvCVLFunctionSummary/withEnvSummary.spec index ababd1fd..1ec48497 100644 --- a/CVLByExample/Summarization/WithEnv/WithEnvCVLFunctionSummary/withEnvSummary.spec +++ b/CVLByExample/Summarization/WithEnv/WithEnvCVLFunctionSummary/withEnvSummary.spec @@ -3,26 +3,25 @@ */ methods { - // Summarization by a CVL function. The result is non-deterministic because the CVL function is not deterministic. - function reduceBalance(uint256 amount) internal returns (uint256) with (env e) => cvlReduceBalance(e, amount); + + // Summarization by a CVL function. The result is non-deterministic because the CVL function is not deterministic. + function reduceBalance(uint256 amount) internal returns (uint256) with(env e) => cvlReduceBalance(e, amount); } // CVL function used for summarization. -function cvlReduceBalance(env e, uint256 amount) returns uint256 { - uint256 poolBalance = getBalance(e, currentContract); - require (poolBalance != 0); - require (amount != 0); - uint256 amountOut = decr(e); - return amountOut; +function cvlReduceBalance(env e, uint256 amount) returns uint256 { + uint256 poolBalance = getBalance(e, currentContract); + require(poolBalance != 0); + require(amount != 0); + uint256 amountOut = decr(e); + return amountOut; } // A rule that demonstrates the use of the summarization. rule checkReduceBalance() { - env e; - uint256 amountBefore = getBalance(e, e.msg.sender); - uint256 amount; - callReduceBalance(e, amount); - assert (getBalance(e, e.msg.sender) == assert_uint256(amountBefore - 1), "Withdraw failed"); + env e; + uint256 amountBefore = getBalance(e, e.msg.sender); + uint256 amount; + callReduceBalance(e, amount); + assert getBalance(e, e.msg.sender) == assert_uint256(amountBefore - 1), "Withdraw failed"; } - - diff --git a/CVLByExample/Summarization/WithEnv/WithEnvGhostSummary/WithEnv.spec b/CVLByExample/Summarization/WithEnv/WithEnvGhostSummary/WithEnv.spec index 4a924a36..fbc272a1 100644 --- a/CVLByExample/Summarization/WithEnv/WithEnvGhostSummary/WithEnv.spec +++ b/CVLByExample/Summarization/WithEnv/WithEnvGhostSummary/WithEnv.spec @@ -2,16 +2,16 @@ Example for ghost summary using `with env`. */ - methods { - // Summarization by a ghost. - // This summarization makes the result of balanceOf deterministic. For the same user and timestamp - // balanceOf is the same. - function balanceOf(address user) internal returns (uint256) with (env e) => - discount_ghost[user][e.block.timestamp]; + + // Summarization by a ghost. + // This summarization makes the result of balanceOf deterministic. For the same user and timestamp + // balanceOf is the same. + function balanceOf(address user) internal returns (uint256) with(env e) => discount_ghost[user][e.block.timestamp]; } -ghost mapping(address => mapping (uint256 => uint256)) discount_ghost; +ghost mapping(address => mapping(uint256 => uint256)) discount_ghost; + ghost mapping(uint256 => uint256) index_ghost; /** @@ -25,24 +25,23 @@ function indexAtTimestamp(uint256 timestamp) returns uint256 { * Query discount_ghost for the [user]'s balance of discount token at [timestamp] **/ function balanceOfDiscountTokenAtTimestamp(address user, uint256 timestamp) returns uint256 { - return discount_ghost[user][timestamp]; + return discount_ghost[user][timestamp]; } /** * @title proves that the user's balance of debt token (as reported by GhoVariableDebtToken::balanceOf) can't increase by calling any external non-mint function. **/ rule nonMintFunctionCantIncreaseBalance(method f) { - address user; - uint256 ts1; - uint256 ts2; - env e; - require(e.block.timestamp == ts2); - require(ts2 >= ts1); - uint256 balanceBeforeOp = callBalanceOf(e, user); - calldataarg args; - f(e,args); - mathint balanceAfterOp = balanceOf(e, user); - mathint allowedDiff = indexAtTimestamp(ts2) / 5; - assert(balanceAfterOp <= balanceBeforeOp + allowedDiff); + address user; + uint256 ts1; + uint256 ts2; + env e; + require(e.block.timestamp == ts2); + require(ts2 >= ts1); + uint256 balanceBeforeOp = callBalanceOf(e, user); + calldataarg args; + f(e, args); + mathint balanceAfterOp = balanceOf(e, user); + mathint allowedDiff = indexAtTimestamp(ts2) / 5; + assert(balanceAfterOp <= balanceBeforeOp + allowedDiff); } - diff --git a/CVLByExample/Teams/NoPreserved.spec b/CVLByExample/Teams/NoPreserved.spec index 6310b37d..900115e9 100644 --- a/CVLByExample/Teams/NoPreserved.spec +++ b/CVLByExample/Teams/NoPreserved.spec @@ -5,7 +5,6 @@ methods { function leaderOf(uint8) external returns (address) envfree; } - /** @title If a team does not exist it has not players * This invariant cannot be proven without a preserved block. */ diff --git a/CVLByExample/Teams/Teams.spec b/CVLByExample/Teams/Teams.spec index 4e2d6f25..bd752f6b 100644 --- a/CVLByExample/Teams/Teams.spec +++ b/CVLByExample/Teams/Teams.spec @@ -4,63 +4,36 @@ methods { function leaderOf(uint8) external returns (address) envfree; } - /// @title The team's leader is part of the team invariant leaderBelongsToTeam(uint8 teamId) (teamId != 0 && leaderOf(teamId) != 0) => teamOf(leaderOf(teamId)) == teamId; - /// @title Address zero is not in any team invariant addressZeroNotPlayer() teamOf(0) == 0; - /// @title If a team does not exist it has not players invariant nonExistTeamHasNoPlayers(uint8 teamId, address player) - (teamId != 0 && leaderOf(teamId) == 0) => teamOf(player) != teamId - { + (teamId != 0 && leaderOf(teamId) == 0) => teamOf(player) != teamId { preserved { requireInvariant addressZeroNotPlayer(); } } - /// @return If the four addresses are all different from each other -function fourDifferentAddresses( - address a, - address b, - address c, - address d -) returns bool { - return ( - a != b && a != c && a != d && - b != c && b != d && - c != d - ); +function fourDifferentAddresses(address a, address b, address c, address d) returns bool { + return (a != b && a != c && a != d && b != c && b != d && c != d); } - /// @return If all players are on the same team function sameTeam(address a, address b, address c) returns bool { return teamOf(a) == teamOf(b) && teamOf(b) == teamOf(c); } - /// @title A team has at most three players invariant teamHasMaxThreePlayers(address a, address b, address c, address d) - ( - teamOf(a) != 0 && - fourDifferentAddresses(a, b, c, d) && - sameTeam(a, b, c) - => teamOf(d) != teamOf(a) - ) - { - preserved createTeam( - address leader, - address playerA, - address playerB, - uint8 teamId - ) with (env e) { + (teamOf(a) != 0 && fourDifferentAddresses(a, b, c, d) && sameTeam(a, b, c) => teamOf(d) != teamOf(a)) { + preserved createTeam(address leader, address playerA, address playerB, uint8 teamId) with (env e) { requireInvariant nonExistTeamHasNoPlayers(teamId, a); requireInvariant nonExistTeamHasNoPlayers(teamId, b); requireInvariant nonExistTeamHasNoPlayers(teamId, c); diff --git a/CVLByExample/TransientStorage/Hooks/Mutexer.spec b/CVLByExample/TransientStorage/Hooks/Mutexer.spec index 0340aac7..76870825 100644 --- a/CVLByExample/TransientStorage/Hooks/Mutexer.spec +++ b/CVLByExample/TransientStorage/Hooks/Mutexer.spec @@ -1,5 +1,4 @@ methods { - function lockValue() external returns (uint256) envfree; function getContractLock() external returns (uint256) envfree; } @@ -14,7 +13,7 @@ hook ALL_TSTORE(uint loc, uint v) { } } -hook ALL_TLOAD(uint loc) uint v { +hook ALL_TLOAD(uint loc, uint v) { if (loc == getContractLock() && executingContract == currentContract) { require contract_lock_status == isLocked(v); } @@ -24,11 +23,10 @@ invariant lockStatusDontChange() !contract_lock_status; // if contract was locked function call always reverted -rule checkContractLockReverts(){ +rule checkContractLockReverts() { env e; require contract_lock_status; // require contract is locked - + contractLevelAccess@withrevert(e); - assert lastReverted; -} \ No newline at end of file +} diff --git a/CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec b/CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec index 08d71c3d..ff2635c7 100644 --- a/CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec +++ b/CVLByExample/TransientStorage/PreservedonTransactionBoundary/WithPreservedOnTransaction.spec @@ -1,14 +1,13 @@ -invariant isUnlocked(env e) - getLock(e) == 0; +invariant isUnlocked(env e) + getLock(e) == 0; invariant deltaZeroWhenUnlocked(env e) getLock(e) == 0 => getDelta(e) == 0; invariant deltaEqualsStorage(env e) - getDelta(e) == currentContract.storageValue -{ - preserved onTransactionBoundary with(env e2) { - requireInvariant isUnlocked(e2); - requireInvariant deltaZeroWhenUnlocked(e2); - } -} \ No newline at end of file + getDelta(e) == currentContract.storageValue { + preserved onTransactionBoundary with (env e2) { + requireInvariant isUnlocked(e2); + requireInvariant deltaZeroWhenUnlocked(e2); + } + } diff --git a/CVLByExample/TrustedMethodsAnalysis/trustedMethod.spec b/CVLByExample/TrustedMethodsAnalysis/trustedMethod.spec index 4f0b6d5a..8fe752be 100644 --- a/CVLByExample/TrustedMethodsAnalysis/trustedMethod.spec +++ b/CVLByExample/TrustedMethodsAnalysis/trustedMethod.spec @@ -1 +1 @@ -use builtin rule trustedMethods; \ No newline at end of file +use builtin rule trustedMethods; diff --git a/CVLByExample/Types/StoreToArray/StoreToArray.spec b/CVLByExample/Types/StoreToArray/StoreToArray.spec index 0dde0861..b06b4bc6 100644 --- a/CVLByExample/Types/StoreToArray/StoreToArray.spec +++ b/CVLByExample/Types/StoreToArray/StoreToArray.spec @@ -1,6 +1,6 @@ ghost mapping(uint256 => uint256) userArray; rule returnTuple(env e, uint256 y) { - (userArray[y],_) = tuple(e); + userArray[y], _ = tuple(e); assert userArray[y] == 2; -} \ No newline at end of file +} diff --git a/CVLByExample/Types/Strings/String.spec b/CVLByExample/Types/Strings/String.spec index 8630fa97..1ac815ec 100644 --- a/CVLByExample/Types/Strings/String.spec +++ b/CVLByExample/Types/Strings/String.spec @@ -1,9 +1,7 @@ -rule cvlStringEqComparisonToEVMType { - env e; - string r1; - - string r2 = "Blurp"; - r1 = getBlurp(e); - - assert r1 == r2, "Should succeed"; -} \ No newline at end of file +rule cvlStringEqComparisonToEVMType() { + env e; + string r1; + string r2 = Blurp; + r1 = getBlurp(e); + assert r1 == r2, "Should succeed"; +} diff --git a/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec b/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec index 13fabcc5..e448d41f 100644 --- a/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec +++ b/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec @@ -10,19 +10,18 @@ * 5. structs in cvl functions - passing and returning. * 6. struct as a parameter of preserved function. */ - -using Bank as bank; // bank is the same as currentContract. +using Bank as bank; // bank is the same as currentContract. methods { - /// Definition of a user-defined solidity method returning a struct - function getCustomer(address a) external returns(BankAccountRecord.Customer) envfree; + + /// Definition of a user-defined solidity method returning a struct + function getCustomer(address a) external returns (BankAccountRecord.Customer) envfree; /// Definition of a function with struct as an argument function addCustomer(BankAccountRecord.Customer) external envfree; - - function balanceOf(address) external returns(uint) envfree; - function balanceOfAccount(address, uint) external returns(uint) envfree; - function totalSupply() external returns(uint) envfree; + function balanceOf(address) external returns (uint) envfree; + function balanceOfAccount(address, uint) external returns (uint) envfree; + function totalSupply() external returns (uint) envfree; function getNumberOfAccounts(address) external returns (uint256) envfree; function isCustomer(address) external returns (bool) envfree; } @@ -42,7 +41,7 @@ function integrityOfCustomerInsertion(BankAccountRecord.Customer c1) returns boo @param a - customer's address @param accountId - account number */ - function getAccount(address a, uint256 accountInd) returns BankAccountRecord.BankAccount { +function getAccount(address a, uint256 accountInd) returns BankAccountRecord.BankAccount { BankAccountRecord.Customer c = bank.getCustomer(a); return c.accounts[accountInd]; } @@ -52,15 +51,15 @@ function getAccountNumberAndBalance(address a, uint256 accountInd) returns (uint env e; BankAccountRecord.Customer c = getCustomer(a); BankAccountRecord.BankAccount account = getAccount(e.msg.sender, accountInd); - return (account.accountNumber, account.accountBalance) ; + return (account.accountNumber, account.accountBalance); } /** You can define rule parameters of a user defined type. */ -rule correctCustomerInsertion(BankAccountRecord.Customer c1){ +rule correctCustomerInsertion(BankAccountRecord.Customer c1) { bool correct = integrityOfCustomerInsertion(c1); - assert (correct, "Bad customer insertion"); + assert correct, "Bad customer insertion"; } /// Example for assigning to a tuple. @@ -70,13 +69,10 @@ rule updateOfBlacklist() { address user1; uint256 account; uint256 account1; - uint256 ind = addToBlackList(e, user, account); - user1 = currentContract.blackList[ind].id; account1 = currentContract.blackList[ind].account; - - assert (user == user1 && account == account1, "Customer in black list is not the one added."); + assert user == user1 && account == account1, "Customer in black list is not the one added."; } /// Example for struct parameter and nested struct member reference @@ -85,9 +81,8 @@ rule witnessForIntegrityOfTransferFromCustomerAccount(BankAccountRecord.Customer uint256 accountNum; address to; uint256 toAccount; - require c.accounts[accountNum].accountBalance > 0; - transfer(e, to, assert_uint256(c.accounts[accountNum].accountBalance/2), accountNum, toAccount); + transfer(e, to, assert_uint256(c.accounts[accountNum].accountBalance / 2), accountNum, toAccount); satisfy c.accounts[accountNum].accountBalance < balanceOfAccount(to, toAccount); } @@ -96,13 +91,12 @@ rule witnessForIntegrityOfTransferFromCustomerAccount(BankAccountRecord.Customer rule integrityOfCustomerKeyRule(address a, method f) { env e; calldataarg args; - BankAccountRecord.Customer c = getCustomer(a); + BankAccountRecord.Customer c = getCustomer(a); require c.id == a || c.id == 0; - f(e,args); + f(e, args); assert c.id == a || c.id == 0; } - /// Represent the sum of all accounts of all users /// sum _customers[a].accounts[i].accountBalance persistent ghost mathint sumBalances { @@ -114,9 +108,9 @@ persistent ghost mapping(address => mapping(uint256 => uint256)) accountBalanceM init_state axiom forall address a. forall uint256 i. accountBalanceMirror[a][i] == 0; } - /// Number of accounts per user ghost mapping(address => uint256) numOfAccounts { + // assumption: it's infeasible to grow the list to these many elements. axiom forall address a. numOfAccounts[a] < max_uint256; init_state axiom forall address a. numOfAccounts[a] == 0; @@ -124,8 +118,7 @@ ghost mapping(address => uint256) numOfAccounts { /// Store hook to synchronize numOfAccounts with the length of the customers[KEY address a].accounts array. hook Sstore _customers[KEY address user].accounts.length uint256 newLength { - if (newLength > numOfAccounts[user]) - require accountBalanceMirror[user][require_uint256(newLength-1)] == 0 ; + if (newLength > numOfAccounts[user]) require accountBalanceMirror[user][require_uint256(newLength - 1)] == 0; numOfAccounts[user] = newLength; } @@ -133,40 +126,37 @@ hook Sstore _customers[KEY address user].accounts.length uint256 newLength { An internal step check to verify that our ghost works as expected, it should mirror the number of accounts. Once the sload is defined, this invariant becomes a tautology */ -invariant checkNumOfAccounts(address user) +invariant checkNumOfAccounts(address user) numOfAccounts[user] == bank.getNumberOfAccounts(user); /// This Sload is required in order to eliminate adding unintializaed account balance to sumBalances. hook Sload uint256 length _customers[KEY address user].accounts.length { - require numOfAccounts[user] == length; + require numOfAccounts[user] == length; } /// hook on a complex data structure, a mapping to a struct with a dynamic array hook Sstore _customers[KEY address a].accounts[INDEX uint256 i].accountBalance uint256 new_value (uint old_value) { - require old_value == accountBalanceMirror[a][i]; // Need this inorder to sync on insert of new element - sumBalances = sumBalances + new_value - old_value ; + require old_value == accountBalanceMirror[a][i]; // Need this inorder to sync on insert of new element + sumBalances = sumBalances + new_value - old_value; accountBalanceMirror[a][i] = new_value; } /// Sload on a struct field. -hook Sload uint256 value _customers[KEY address a].accounts[INDEX uint256 i].accountBalance { +hook Sload uint256 value _customers[KEY address a].accounts[INDEX uint256 i].accountBalance { + // when balance load, safely assume it is less than the sum of all values require value <= sumBalances; - require i <= numOfAccounts[a]-1; + require i <= numOfAccounts[a] - 1; } /// Non-customers have no account. -invariant emptyAccount(address user) - !isCustomer(user) => ( - getNumberOfAccounts(user) == 0 && - (forall uint256 i. accountBalanceMirror[user][i] == 0 )) ; +invariant emptyAccount(address user) + !isCustomer(user) => (getNumberOfAccounts(user) == 0 && (forall uint256 i. accountBalanceMirror[user][i] == 0)); /// struct as a parameter of preserved function. invariant totalSupplyEqSumBalances() - totalSupply() == sumBalances - { - preserved addCustomer(BankAccountRecord.Customer c) - { + totalSupply() == sumBalances { + preserved addCustomer(BankAccountRecord.Customer c) { requireInvariant emptyAccount(c.id); } } @@ -174,8 +164,9 @@ invariant totalSupplyEqSumBalances() /// Comparing nativeBalances of current contract. invariant solvency() totalSupply() <= nativeBalances[currentContract] { + // safely assume that Bank doesn't call itself - preserved with (env e){ + preserved with (env e) { require e.msg.sender != currentContract; } } diff --git a/CVLByExample/Types/Structs/DirectStorageAccessToFields/RootStruct.spec b/CVLByExample/Types/Structs/DirectStorageAccessToFields/RootStruct.spec index 0a006e52..ee425d4e 100644 --- a/CVLByExample/Types/Structs/DirectStorageAccessToFields/RootStruct.spec +++ b/CVLByExample/Types/Structs/DirectStorageAccessToFields/RootStruct.spec @@ -11,9 +11,7 @@ function workOnSCVL(uint x, RootStruct.Simple s) { rule checkWorkOnS(uint x) { require x < 3; - env e; workOnSExt(e, x); - assert rootStruct.s.b1; } diff --git a/CVLByExample/UnresolvedCallSummarization/TrusterLenderPool.spec b/CVLByExample/UnresolvedCallSummarization/TrusterLenderPool.spec index b997d18a..979ef3d7 100644 --- a/CVLByExample/UnresolvedCallSummarization/TrusterLenderPool.spec +++ b/CVLByExample/UnresolvedCallSummarization/TrusterLenderPool.spec @@ -1,12 +1,10 @@ - using DamnValuableToken as token; -methods{ +methods { function token.totalSupply() external returns (uint256) envfree; function token.allowance(address, address) external returns (uint256) envfree; - - unresolved external in TrusterLenderPool.flashLoan(uint256,address,address,bytes) => DISPATCH(use_fallback=true) [ - token.approve(address, uint256), + unresolved external in TrusterLenderPool.flashLoan(uint256, address, address, bytes) => DISPATCH(use_fallback)[ + token.approve(address, uint256)(address, uint256), currentContract._ ] default NONDET; } @@ -18,10 +16,8 @@ methods{ */ invariant poolAllowanceAlwaysZero(address user) - token.allowance(currentContract, user) == 0 - { - preserved with (env e) - { + token.allowance(currentContract, user) == 0 { + preserved with (env e) { require e.msg.sender != currentContract; - } - } \ No newline at end of file + } + } diff --git a/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec b/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec index f8111ba8..9b3c71da 100644 --- a/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec +++ b/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec @@ -8,7 +8,6 @@ using DummyERC20A as _token0; using DummyERC20B as _token1; using ConstantProductPool as _pool; - /* Declaration of methods that are used in the rules. `envfree` indicates that the method is not dependent on the environment (`msg.value`, `msg.sender`). @@ -16,11 +15,11 @@ using ConstantProductPool as _pool; environment. */ -methods{ +methods { function token0() external returns (address) envfree; function token1() external returns (address) envfree; - function allowance(address,address) external returns (uint256) envfree; - function totalSupply() external returns (uint256) envfree; + function allowance(address, address) external returns (uint256) envfree; + function totalSupply() external returns (uint256) envfree; function swap(address tokenIn, address recipient) external returns (uint256) envfree; //calls to external contracts @@ -30,15 +29,14 @@ methods{ function _token1.allowance(address owner, address spender) external returns (uint256) envfree; function _token0.transfer(address, uint) external; function _token1.transfer(address, uint) external; - + //external calls to be resolved by dispatcher - taking into account all available implementations function _.transferFrom(address sender, address recipient, uint256 amount) external => DISPATCHER(true); function _.balanceOf(address) external => DISPATCHER(true); - } // a cvl function for precondition assumptions -function setup(env e){ +function setup(env e) { address zero_address = 0; uint256 MINIMUM_LIQUIDITY = 1000; require totalSupply() == 0 || currentContract._balances[zero_address] == MINIMUM_LIQUIDITY, "Either pool is empty or minimum liquidity is locked"; @@ -47,7 +45,6 @@ function setup(env e){ require _token1 == token1(), "Token1 reference must match contract's token1"; } - /* Property: For all possible scenarios of swapping token1 for token0, the balance of the recipient is updated as expected. @@ -71,7 +68,7 @@ rule integrityOfSwap(address recipient) { uint256 balanceBefore = _token0.balanceOf(recipient); uint256 amountOut = swap(_token1, recipient); uint256 balanceAfter = _token0.balanceOf(recipient); - assert (recipient != currentContract) => balanceAfter == balanceBefore + amountOut; + assert (recipient != currentContract) => balanceAfter == balanceBefore + amountOut; } /* @@ -92,18 +89,16 @@ rule noDecreaseByOther(method f, address account) { env e; setup(e); require e.msg.sender != account, "Sender must be different from account to test unauthorized access"; - require account != currentContract, "Account must not be the pool contract to properly test balance changes"; - uint256 allowance = allowance(account, e.msg.sender); - + require account != currentContract, "Account must not be the pool contract to properly test balance changes"; + uint256 allowance = allowance(account, e.msg.sender); uint256 before = currentContract._balances[account]; calldataarg args; - f(e,args); /* check on all possible arguments */ + f(e, args); /* check on all possible arguments */ uint256 after = currentContract._balances[account]; /* logic implication : true when: (a) the left hand side is false or (b) right hand side is true */ - assert after < before => (e.msg.sender == account || allowance >= (before-after)) ; + assert after < before => (e.msg.sender == account || allowance >= (before - after)); } - /* Property: For both token0 and token1 the balance of the system is at least as much as the reserves. @@ -120,20 +115,18 @@ Formula: */ invariant balanceGreaterThanReserve() - (currentContract.reserve0 <= _token0.balanceOf(currentContract))&& - (currentContract.reserve1 <= _token1.balanceOf(currentContract)) - { - preserved with (env e){ - setup(e); + (currentContract.reserve0 <= _token0.balanceOf(currentContract)) && (currentContract.reserve1 <= _token1.balanceOf(currentContract)) { + preserved with (env e) { + setup(e); } - + // This preserved is safe because transferFrom is called from the currentContract whose code is known and // it is not msg.sender. It would not be safe to do if the call was to a function of an unresolved contract. - preserved _.transferFrom(address sender, address recipient,uint256 amount) with (env e1) { + preserved _.transferFrom(address sender, address recipient, uint256 amount) with (env e1) { requireInvariant allowanceOfPoolAlwaysZero(e1.msg.sender); require e1.msg.sender != currentContract, "The pool does not call itself"; } - + // This preserved is safe because transfer is called from the currentContract whose code is known and // it is not msg.sender. preserved _.transfer(address recipient, uint256 amount) with (env e2) { @@ -142,20 +135,19 @@ invariant balanceGreaterThanReserve() } invariant allowanceOfPoolAlwaysZero(address a) - _token0.allowance(_pool, a) == 0 && _token1.allowance(_pool, a) == 0 - { + _token0.allowance(_pool, a) == 0 && _token1.allowance(_pool, a) == 0 { + // This preserved is safe because we know the code in the pool contract. preserved _.approve(address spender, uint256 amount) with (env e1) { require e1.msg.sender != _pool, "Sender must not be the pool contract for approve calls"; } - + // This preserved is safe because we know the code in the pool contract. preserved _.increaseAllowance(address spender, uint256 addedValue) with (env e2) { require e2.msg.sender != _pool, "Sender must not be the pool contract for increaseAllowance calls"; } } - /* Property: Integrity of totalSupply with respect to the amount of reserves. @@ -170,17 +162,13 @@ Formula: */ invariant integrityOfTotalSupply() - - (totalSupply() == 0 <=> currentContract.reserve0 == 0) && - (totalSupply() == 0 <=> currentContract.reserve1 == 0) - { - preserved with (env e){ + (totalSupply() == 0 <=> currentContract.reserve0 == 0) && (totalSupply() == 0 <=> currentContract.reserve1 == 0) { + preserved with (env e) { requireInvariant balanceGreaterThanReserve(); setup(e); } } - /* Property: Monotonicity of mint. @@ -208,13 +196,12 @@ rule monotonicityOfMint(uint256 x, uint256 y, address recipient) { require recipient != currentContract, "Recipient must not be the pool contract to properly test external balance changes"; require x > y, "First amount must be greater than second amount to test monotonicity"; token.transfer(eT0, currentContract, x); - uint256 amountOut0 = mint(eM,recipient); + uint256 amountOut0 = mint(eM, recipient); uint256 balanceAfter1 = currentContract._balances[recipient]; - token.transfer(eT0, currentContract, y) at init; - uint256 amountOut2 = mint(eM,recipient); - uint256 balanceAfter2 = currentContract._balances[recipient]; - assert balanceAfter1 >= balanceAfter2; + uint256 amountOut2 = mint(eM, recipient); + uint256 balanceAfter2 = currentContract._balances[recipient]; + assert balanceAfter1 >= balanceAfter2; } /* @@ -230,22 +217,21 @@ Formula: */ -ghost mathint sumBalances{ +ghost mathint sumBalances { + // assuming value zero at the initial state before constructor - init_state axiom sumBalances == 0; + init_state axiom sumBalances == 0; } - /* here we state when and how the ghost is updated */ hook Sstore _balances[KEY address a] uint256 new_balance // the old value that balances[a] holds before the store - (uint256 old_balance) { - sumBalances = sumBalances + new_balance - old_balance; +(uint256 old_balance) { + sumBalances = sumBalances + new_balance - old_balance; } -invariant sumFunds() - sumBalances == totalSupply(); - +invariant sumFunds() + sumBalances == totalSupply(); /* Property: Full withdraw example @@ -261,20 +247,17 @@ rule possibleToFullyWithdraw(address sender, uint256 amount) { setup(eM); address token; require token == _token0 || token == _token1, "Token must be either token0 or token1"; - uint256 balanceBefore = token.balanceOf(eT0,sender); - + uint256 balanceBefore = token.balanceOf(eT0, sender); require eM.msg.sender == sender, "Message sender must be the same as the user to perform withdrawal"; require eT0.msg.sender == sender, "Message sender must be the same as the user to perform transfer"; require amount > 0, "Amount must be positive to test meaningful deposit and withdrawal"; token.transfer(eT0, currentContract, amount); - uint256 amountOut0 = mint(eM,sender); + uint256 amountOut0 = mint(eM, sender); // immediately withdraw burnSingle(eM, _token0, amountOut0, sender); satisfy (balanceBefore == token.balanceOf(eT0, sender)); } - - /* Property: Zero withdraw has no effect diff --git a/DEFI/ERC20/certora/specs/ERC20Broken.spec b/DEFI/ERC20/certora/specs/ERC20Broken.spec index 2b0b5b51..73bad126 100644 --- a/DEFI/ERC20/certora/specs/ERC20Broken.spec +++ b/DEFI/ERC20/certora/specs/ERC20Broken.spec @@ -5,52 +5,41 @@ */ methods { - function balanceOf(address) external returns(uint) envfree; - function allowance(address,address) external returns(uint) envfree; - function totalSupply() external returns(uint) envfree; - function transferFrom(address,address,uint) external returns(bool) envfree; + function balanceOf(address) external returns (uint) envfree; + function allowance(address, address) external returns (uint) envfree; + function totalSupply() external returns (uint) envfree; + function transferFrom(address, address, uint) external returns (bool) envfree; } //// ## Part 1: Basic Rules //////////////////////////////////////////////////// /// Transfer must move `amount` tokens from the caller's account to `recipient` -rule transferSpec { - address sender; address recip; uint amount; - +rule transferSpec() { + address sender; + address recip; + uint amount; env e; require e.msg.sender == sender; - mathint balance_sender_before = balanceOf(sender); mathint balance_recip_before = balanceOf(recip); - transfer(e, recip, amount); - mathint balance_sender_after = balanceOf(sender); mathint balance_recip_after = balanceOf(recip); - require sender != recip; - - assert balance_sender_after == balance_sender_before - amount, - "transfer must decrease sender's balance by amount"; - - assert balance_recip_after == balance_recip_before + amount, - "transfer must increase recipient's balance by amount"; + assert balance_sender_after == balance_sender_before - amount, "transfer must decrease sender's balance by amount"; + assert balance_recip_after == balance_recip_before + amount, "transfer must increase recipient's balance by amount"; } - /// Transfer must revert if the sender's balance is too small -rule transferReverts { - env e; address recip; uint amount; - +rule transferReverts() { + env e; + address recip; + uint amount; require balanceOf(e.msg.sender) < amount; - transfer@withrevert(e, recip, amount); - - assert lastReverted, - "transfer(recip,amount) must revert if sender's balance is less than `amount`"; + assert lastReverted, "transfer(recip,amount) must revert if sender's balance is less than `amount`"; } - /// Transfer shouldn't revert unless /// the sender doesn't have enough funds, /// or the message value is nonzero, @@ -59,15 +48,15 @@ rule transferReverts { /// or the recipient is 0 /// /// @title Transfer doesn't revert -rule transferDoesntRevert { - env e; address recipient; uint amount; - +rule transferDoesntRevert() { + env e; + address recipient; + uint amount; require balanceOf(e.msg.sender) > amount; require e.msg.value == 0; require balanceOf(recipient) + amount < max_uint; require e.msg.sender != 0; require recipient != 0; - transfer@withrevert(e, recipient, amount); assert !lastReverted; } @@ -75,37 +64,30 @@ rule transferDoesntRevert { //// ## Part 2: Parametric Rules /////////////////////////////////////////////// /// If `approve` changes a holder's allowance, then it was called by the holder -rule onlyHolderCanChangeAllowance { - address holder; address spender; - +rule onlyHolderCanChangeAllowance() { + address holder; + address spender; mathint allowance_before = allowance(holder, spender); - - method f; env e; calldataarg args; // was: env e; uint256 amount; - f(e, args); // was: approve(e, spender, amount); - + method f; + env e; + calldataarg args; // was: env e; uint256 amount; + f(e, args); // was: approve(e, spender, amount); + mathint allowance_after = allowance(holder, spender); - - assert allowance_after > allowance_before => e.msg.sender == holder, - "approve must only change the sender's allowance"; - - assert allowance_after > allowance_before => - (f.selector == sig:approve(address,uint).selector || f.selector == sig:increaseAllowance(address,uint).selector), - "only approve and increaseAllowance can increase allowances"; + assert allowance_after > allowance_before => e.msg.sender == holder, "approve must only change the sender's allowance"; + assert allowance_after > allowance_before => (f.selector == sig:approve(address, uint).selector || f.selector == sig:increaseAllowance(address, uint).selector), "only approve and increaseAllowance can increase allowances"; } -rule onlyApproveIncreasesAllowance { - address holder; address spender; - +rule onlyApproveIncreasesAllowance() { + address holder; + address spender; mathint allowance_before = allowance(holder, spender); - - method f; env e; calldataarg args; - f(e, args); - + method f; + env e; + calldataarg args; + f(e, args); mathint allowance_after = allowance(holder, spender); - - satisfy allowance_after > allowance_before => - (f.selector == sig:approve(address,uint).selector), - "only approve and increaseAllowance can increase allowances"; + satisfy allowance_after > allowance_before => (f.selector == sig:approve(address, uint).selector), "only approve and increaseAllowance can increase allowances"; } //// ## Part 3: Ghosts and Hooks /////////////////////////////////////////////// @@ -115,6 +97,7 @@ ghost mathint sum_of_balances { } hook Sstore _balances[KEY address a] uint new_value (uint old_value) { + // when balance changes, update ghost sum_of_balances = sum_of_balances + new_value - old_value; } @@ -123,19 +106,17 @@ hook Sstore _balances[KEY address a] uint new_value (uint old_value) { /// @dev This rule is unsound! invariant balancesBoundedByTotalSupply(address alice, address bob) - balanceOf(alice) + balanceOf(bob) <= totalSupply() -{ - preserved transfer(address recip, uint256 amount) with (env e) { - require recip == alice || recip == bob; - require e.msg.sender == alice || e.msg.sender == bob; + balanceOf(alice) + balanceOf(bob) <= totalSupply() { + preserved transfer(address recip, uint256 amount) with (env e) { + require recip == alice || recip == bob; + require e.msg.sender == alice || e.msg.sender == bob; + } + preserved transferFrom(address from, address to, uint256 amount) { + require from == alice || from == bob; + require to == alice || to == bob; + } } - preserved transferFrom(address from, address to, uint256 amount) { - require from == alice || from == bob; - require to == alice || to == bob; - } -} - /** `totalSupply()` returns the sum of `balanceOf(u)` over all users `u`. */ invariant totalSupplyIsSumOfBalances() totalSupply() == sum_of_balances; @@ -147,16 +128,11 @@ rule requireHidesOverflow() { env e; uint256 amount1; uint256 amount2; - storage initial = lastStorage; addAmount(e, amount1); addAmount(e, amount2); storage afterTwoSteps = lastStorage; - addAmount(e, require_uint256(amount1 + amount2)) at initial; storage afterOneStep = lastStorage; assert afterOneStep == afterTwoSteps; } - - - diff --git a/DEFI/ERC20/certora/specs/ERC20Fixed.spec b/DEFI/ERC20/certora/specs/ERC20Fixed.spec index c914f12c..ef5ecb25 100644 --- a/DEFI/ERC20/certora/specs/ERC20Fixed.spec +++ b/DEFI/ERC20/certora/specs/ERC20Fixed.spec @@ -5,53 +5,41 @@ */ methods { - function balanceOf(address) external returns(uint) envfree; - function allowance(address,address) external returns(uint) envfree; - function totalSupply() external returns(uint) envfree; - function add(uint256 x, uint256 y) external returns(uint256) envfree; + function balanceOf(address) external returns (uint) envfree; + function allowance(address, address) external returns (uint) envfree; + function totalSupply() external returns (uint) envfree; + function add(uint256 x, uint256 y) external returns (uint256) envfree; } //// ## Part 1: Basic Rules //////////////////////////////////////////////////// /// Transfer must move `amount` tokens from the caller's account to `recipient` -rule transferSpec { - address sender; address recip; uint amount; - +rule transferSpec() { + address sender; + address recip; + uint amount; env e; require e.msg.sender == sender; - mathint balance_sender_before = balanceOf(sender); mathint balance_recip_before = balanceOf(recip); - transfer(e, recip, amount); - mathint balance_sender_after = balanceOf(sender); mathint balance_recip_after = balanceOf(recip); - require sender != recip; - - assert balance_sender_after == balance_sender_before - amount, - "transfer must decrease sender's balance by amount"; - - assert balance_recip_after == balance_recip_before + amount, - "transfer must increase recipient's balance by amount"; + assert balance_sender_after == balance_sender_before - amount, "transfer must decrease sender's balance by amount"; + assert balance_recip_after == balance_recip_before + amount, "transfer must increase recipient's balance by amount"; } - - /// Transfer must revert if the sender's balance is too small -rule transferReverts { - env e; address recip; uint amount; - +rule transferReverts() { + env e; + address recip; + uint amount; require balanceOf(e.msg.sender) < amount; - transfer@withrevert(e, recip, amount); - - assert lastReverted, - "transfer(recip,amount) must revert if sender's balance is less than `amount`"; + assert lastReverted, "transfer(recip,amount) must revert if sender's balance is less than `amount`"; } - /// Transfer shouldn't revert unless /// the sender doesn't have enough funds, /// or the message value is nonzero, @@ -60,15 +48,15 @@ rule transferReverts { /// or the recipient is 0 /// /// @title Transfer doesn't revert -rule transferDoesntRevert { - env e; address recipient; uint amount; - +rule transferDoesntRevert() { + env e; + address recipient; + uint amount; require balanceOf(e.msg.sender) > amount; require e.msg.value == 0; require balanceOf(recipient) + amount < max_uint; require e.msg.sender != 0; require recipient != 0; - transfer@withrevert(e, recipient, amount); assert !lastReverted; } @@ -76,21 +64,18 @@ rule transferDoesntRevert { //// ## Part 2: Parametric Rules /////////////////////////////////////////////// /// If `approve` changes a holder's allowance, then it was called by the holder -rule onlyHolderCanChangeAllowance { - address holder; address spender; - +rule onlyHolderCanChangeAllowance() { + address holder; + address spender; mathint allowance_before = allowance(holder, spender); - method f; env e; calldataarg args; // was: env e; uint256 amount; - f(e, args); // was: approve(e, spender, amount); - + method f; + env e; + calldataarg args; // was: env e; uint256 amount; + f(e, args); // was: approve(e, spender, amount); + mathint allowance_after = allowance(holder, spender); - - assert allowance_after > allowance_before => e.msg.sender == holder, - "approve must only change the sender's allowance"; - - assert allowance_after > allowance_before => - (f.selector == sig:approve(address,uint).selector || f.selector == sig:increaseAllowance(address,uint).selector), - "only approve and increaseAllowance can increase allowances"; + assert allowance_after > allowance_before => e.msg.sender == holder, "approve must only change the sender's allowance"; + assert allowance_after > allowance_before => (f.selector == sig:approve(address, uint).selector || f.selector == sig:increaseAllowance(address, uint).selector), "only approve and increaseAllowance can increase allowances"; } //// ## Part 3: Ghosts and Hooks /////////////////////////////////////////////// @@ -100,13 +85,14 @@ persistent ghost mathint sum_of_balances { } hook Sstore _balances[KEY address a] uint new_value (uint old_value) { + // when balance changes, update ghost sum_of_balances = sum_of_balances + new_value - old_value; } // This `sload` makes `sum_of_balances >= balance` hold at the beginning of each rule. -hook Sload uint256 balance _balances[KEY address a] { - require sum_of_balances >= balance; +hook Sload uint256 balance _balances[KEY address a] { + require sum_of_balances >= balance; } //// ## Part 4: Invariants @@ -117,7 +103,7 @@ invariant totalSupplyIsSumOfBalances() // satisfy examples // Generate an example trace for a first deposit operation that succeeds. -rule satisfyFirstDepositSucceeds(){ +rule satisfyFirstDepositSucceeds() { env e; require totalSupply() == 0; deposit(e); @@ -135,10 +121,13 @@ rule satisfyLastWithdrawSucceeds() { } // A witness with several function calls. -rule satisfyWithManyOps(){ - env e; env e1; env e2; env e3; - address recipient; uint amount; - +rule satisfyWithManyOps() { + env e; + env e1; + env e2; + env e3; + address recipient; + uint amount; requireInvariant totalSupplyIsSumOfBalances(); // The following two requirement are to avoid overflow exmaples. require balanceOf(e.msg.sender) > e.msg.value + 10 * amount; @@ -148,18 +137,15 @@ rule satisfyWithManyOps(){ deposit(e1); depositTo(e2, recipient, amount); transfer(e3, recipient, amount); - assert totalSupply() > 0; + assert totalSupply() > 0; } - - // A non-vacuous example where transfer() does not revert. -rule satisfyVacuityCorrection { - env e; address recip; uint amount; - +rule satisfyVacuityCorrection() { + env e; + address recip; + uint amount; require balanceOf(e.msg.sender) > 0; - transfer(e, recip, amount); - satisfy balanceOf(e.msg.sender) == 0; -} \ No newline at end of file +} diff --git a/DEFI/ERC20/certora/specs/ERC20FixedNoPersistsGhost.spec b/DEFI/ERC20/certora/specs/ERC20FixedNoPersistsGhost.spec index 2221999d..245d0854 100644 --- a/DEFI/ERC20/certora/specs/ERC20FixedNoPersistsGhost.spec +++ b/DEFI/ERC20/certora/specs/ERC20FixedNoPersistsGhost.spec @@ -9,18 +9,16 @@ rule noOverflow() { env e; uint256 amount1; uint256 amount2; - + // requireInvariant totalSupplyIsSumOfBalances(); - + storage initial = lastStorage; addAmount(e, amount1); - addAmount(e, amount2); + addAmount(e, amount2); storage afterTwoSteps = lastStorage; - addAmount(e, assert_uint256(amount1 + amount2)) at initial; storage afterOneStep = lastStorage; assert afterOneStep == afterTwoSteps; - } // addAmount() uses `unchecked` therefore is not checking for overflow. The `assert_uint256(amount1 + amount2))` @@ -29,14 +27,11 @@ rule catchOverflow() { env e; uint256 amount1; uint256 amount2; - storage initial = lastStorage; addAmount(e, amount1); addAmount(e, amount2); storage afterTwoSteps = lastStorage; - addAmount(e, assert_uint256(amount1 + amount2)) at initial; storage afterOneStep = lastStorage; assert afterOneStep == afterTwoSteps; - -} \ No newline at end of file +} diff --git a/DEFI/ERC20/certora/specs/ERC20Full.spec b/DEFI/ERC20/certora/specs/ERC20Full.spec index 32c97de2..fd5494c1 100644 --- a/DEFI/ERC20/certora/specs/ERC20Full.spec +++ b/DEFI/ERC20/certora/specs/ERC20Full.spec @@ -18,17 +18,17 @@ environment. methods { function totalSupply() external returns (uint256) envfree; function balanceOf(address) external returns (uint256) envfree; - function allowance(address,address) external returns (uint256) envfree; + function allowance(address, address) external returns (uint256) envfree; function nonces(address) external returns (uint256) envfree; function contractOwner() external returns (address) envfree; - function permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external; - function approve(address,uint256) external returns bool; - function transfer(address,uint256) external returns bool; - function transferFrom(address,address,uint256) external returns bool; - + function permit(address, address, uint256, uint256, uint8, bytes32, bytes32) external; + function approve(address, uint256) external returns (bool); + function transfer(address, uint256) external returns (bool); + function transferFrom(address, address, uint256) external returns (bool); + // exposed for FV - function mint(address,uint256) external; - function burn(address,uint256) external; + function mint(address, uint256) external; + function burn(address, uint256) external; } /* @@ -38,30 +38,17 @@ methods { */ // functionality -definition canIncreaseAllowance(method f) returns bool = - f.selector == sig:approve(address,uint256).selector || - f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector; +definition canIncreaseAllowance(method f) returns bool = f.selector == sig:approve(address, uint256).selector || f.selector == sig:permit(address, address, uint256, uint256, uint8, bytes32, bytes32).selector; -definition canDecreaseAllowance(method f) returns bool = - f.selector == sig:approve(address,uint256).selector || - f.selector == sig:transferFrom(address,address,uint256).selector || - f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector; +definition canDecreaseAllowance(method f) returns bool = f.selector == sig:approve(address, uint256).selector || f.selector == sig:transferFrom(address, address, uint256).selector || f.selector == sig:permit(address, address, uint256, uint256, uint8, bytes32, bytes32).selector; -definition canIncreaseBalance(method f) returns bool = - f.selector == sig:mint(address,uint256).selector || - f.selector == sig:transfer(address,uint256).selector || - f.selector == sig:transferFrom(address,address,uint256).selector; +definition canIncreaseBalance(method f) returns bool = f.selector == sig:mint(address, uint256).selector || f.selector == sig:transfer(address, uint256).selector || f.selector == sig:transferFrom(address, address, uint256).selector; -definition canDecreaseBalance(method f) returns bool = - f.selector == sig:burn(address,uint256).selector || - f.selector == sig:transfer(address,uint256).selector || - f.selector == sig:transferFrom(address,address,uint256).selector; +definition canDecreaseBalance(method f) returns bool = f.selector == sig:burn(address, uint256).selector || f.selector == sig:transfer(address, uint256).selector || f.selector == sig:transferFrom(address, address, uint256).selector; -definition canIncreaseTotalSupply(method f) returns bool = - f.selector == sig:mint(address,uint256).selector; +definition canIncreaseTotalSupply(method f) returns bool = f.selector == sig:mint(address, uint256).selector; -definition canDecreaseTotalSupply(method f) returns bool = - f.selector == sig:burn(address,uint256).selector; +definition canDecreaseTotalSupply(method f) returns bool = f.selector == sig:burn(address, uint256).selector; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -74,7 +61,7 @@ ghost mathint sumOfBalances { } ghost mathint numberOfChangesOfBalances { - init_state axiom numberOfChangesOfBalances == 0; + init_state axiom numberOfChangesOfBalances == 0; } // having an initial state where Alice initial balance is larger than totalSupply, which @@ -103,7 +90,7 @@ invariant totalSupplyIsSumOfBalances() │ Rule: contract owner never change │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule contractOwnerNeverChange(env e){ +rule contractOwnerNeverChange(env e) { address owner = contractOwner(); method f; calldataarg args; @@ -117,14 +104,12 @@ rule contractOwnerNeverChange(env e){ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule totalSupplyNeverOverflow(env e, method f, calldataarg args) filtered{f -> canIncreaseTotalSupply(f) }{ - uint256 totalSupplyBefore = totalSupply(); - - f(e, args); - - uint256 totalSupplyAfter = totalSupply(); - - assert totalSupplyBefore <= totalSupplyAfter; +rule totalSupplyNeverOverflow(env e, method f, calldataarg args) +filtered { f -> canIncreaseTotalSupply(f) } { + uint256 totalSupplyBefore = totalSupply(); + f(e, args); + uint256 totalSupplyAfter = totalSupply(); + assert totalSupplyBefore <= totalSupplyAfter; } /* @@ -133,34 +118,29 @@ rule totalSupplyNeverOverflow(env e, method f, calldataarg args) filtered{f -> c └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule noMethodChangesMoreThanTwoBalances(method f) { - env e; - mathint numberOfChangesOfBalancesBefore = numberOfChangesOfBalances; - calldataarg args; - f(e,args); - mathint numberOfChangesOfBalancesAfter = numberOfChangesOfBalances; - assert numberOfChangesOfBalancesAfter <= numberOfChangesOfBalancesBefore + 2; + env e; + mathint numberOfChangesOfBalancesBefore = numberOfChangesOfBalances; + calldataarg args; + f(e, args); + mathint numberOfChangesOfBalancesAfter = numberOfChangesOfBalances; + assert numberOfChangesOfBalancesAfter <= numberOfChangesOfBalancesBefore + 2; } - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rules: only approve, permit and transferFrom can change allowance | └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule onlyAllowedMethodsMayChangeAllowance(env e) { - address addr1; - address addr2; - uint256 allowanceBefore = allowance(addr1, addr2); - + address addr1; + address addr2; + uint256 allowanceBefore = allowance(addr1, addr2); method f; calldataarg args; - - f(e,args); - + f(e, args); uint256 allowanceAfter = allowance(addr1, addr2); - assert allowanceAfter > allowanceBefore => canIncreaseAllowance(f), "should not increase allowance"; - assert allowanceAfter < allowanceBefore => canDecreaseAllowance(f), "should not decrease allowance"; + assert allowanceAfter < allowanceBefore => canDecreaseAllowance(f), "should not decrease allowance"; } /* @@ -168,17 +148,14 @@ rule onlyAllowedMethodsMayChangeAllowance(env e) { │ Rules: only mint, burn, transfer and transferFrom can change user balance | └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule onlyAllowedMethodsMayChangeBalance(env e){ +rule onlyAllowedMethodsMayChangeBalance(env e) { requireInvariant totalSupplyIsSumOfBalances(); - method f; calldataarg args; - address holder; uint256 balanceBefore = balanceOf(holder); f(e, args); uint256 balanceAfter = balanceOf(holder); - assert balanceAfter > balanceBefore => canIncreaseBalance(f); assert balanceAfter < balanceBefore => canDecreaseBalance(f); } @@ -188,14 +165,12 @@ rule onlyAllowedMethodsMayChangeBalance(env e){ │ Rules: only contract owner can burn or mint │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule onlyOwnerMintOrBurn(env e){ +rule onlyOwnerMintOrBurn(env e) { method f; calldataarg args; - f(e, args); - - assert f.selector == sig:mint(address,uint256).selector => e.msg.sender == contractOwner(); - assert f.selector == sig:burn(address,uint256).selector => e.msg.sender == contractOwner(); + assert f.selector == sig:mint(address, uint256).selector => e.msg.sender == contractOwner(); + assert f.selector == sig:burn(address, uint256).selector => e.msg.sender == contractOwner(); } /* @@ -205,14 +180,11 @@ rule onlyOwnerMintOrBurn(env e){ */ rule onlyAllowedMethodsMayChangeTotalSupply(env e) { requireInvariant totalSupplyIsSumOfBalances(); - method f; calldataarg args; - uint256 totalSupplyBefore = totalSupply(); f(e, args); uint256 totalSupplyAfter = totalSupply(); - assert totalSupplyAfter > totalSupplyBefore => canIncreaseTotalSupply(f); assert totalSupplyAfter < totalSupplyBefore => canDecreaseTotalSupply(f); } @@ -222,38 +194,28 @@ rule onlyAllowedMethodsMayChangeTotalSupply(env e) { │ Rules: Find and show a path for each method. │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule reachability(method f) -{ - env e; - calldataarg args; - f(e,args); - satisfy true; +rule reachability(method f) { + env e; + calldataarg args; + f(e, args); + satisfy true; } - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rules: only the token holder or an approved third party can reduce an account's balance │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule onlyAuthorizedCanTransfer(env e, method f) filtered { f -> canDecreaseBalance(f) } { +rule onlyAuthorizedCanTransfer(env e, method f) +filtered { f -> canDecreaseBalance(f) } { requireInvariant totalSupplyIsSumOfBalances(); - calldataarg args; address account; - uint256 allowanceBefore = allowance(account, e.msg.sender); - uint256 balanceBefore = balanceOf(account); + uint256 balanceBefore = balanceOf(account); f(e, args); - uint256 balanceAfter = balanceOf(account); - - assert ( - balanceAfter < balanceBefore - ) => ( - f.selector == sig:burn(address,uint256).selector || - e.msg.sender == account || - balanceBefore - balanceAfter <= allowanceBefore - ); + uint256 balanceAfter = balanceOf(account); + assert (balanceAfter < balanceBefore) => (f.selector == sig:burn(address, uint256).selector || e.msg.sender == account || balanceBefore - balanceAfter <= allowanceBefore); } /* @@ -266,28 +228,13 @@ rule onlyHolderOfSpenderCanChangeAllowance(env e) { calldataarg args; address holder; address spender; - uint256 allowanceBefore = allowance(holder, spender); f(e, args); uint256 allowanceAfter = allowance(holder, spender); - - assert ( - allowanceAfter > allowanceBefore - ) => ( - (f.selector == sig:approve(address,uint256).selector && e.msg.sender == holder) || - (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) - ); - - assert ( - allowanceAfter < allowanceBefore - ) => ( - (f.selector == sig:transferFrom(address,address,uint256).selector && e.msg.sender == spender) || - (f.selector == sig:approve(address,uint256).selector && e.msg.sender == holder ) || - (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) - ); + assert (allowanceAfter > allowanceBefore) => ((f.selector == sig:approve(address, uint256).selector && e.msg.sender == holder) || (f.selector == sig:permit(address, address, uint256, uint256, uint8, bytes32, bytes32).selector)); + assert (allowanceAfter < allowanceBefore) => ((f.selector == sig:transferFrom(address, address, uint256).selector && e.msg.sender == spender) || (f.selector == sig:approve(address, uint256).selector && e.msg.sender == holder) || (f.selector == sig:permit(address, address, uint256, uint256, uint8, bytes32, bytes32).selector)); } - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Rules: mint behavior and side effects │ @@ -295,37 +242,34 @@ rule onlyHolderOfSpenderCanChangeAllowance(env e) { */ rule mintIntegrity(env e) { requireInvariant totalSupplyIsSumOfBalances(); - address to; uint256 amount; - + // cache state - uint256 toBalanceBefore = balanceOf(to); - uint256 totalSupplyBefore = totalSupply(); - + uint256 toBalanceBefore = balanceOf(to); + uint256 totalSupplyBefore = totalSupply(); + // run transaction mint(e, to, amount); - + // check outcome - + // assert contract owner was the one called assert e.msg.sender == contractOwner(), "Only contract owner can call mint."; - + // updates balance and totalSupply - assert balanceOf(to) == toBalanceBefore + amount; + assert balanceOf(to) == toBalanceBefore + amount; assert totalSupply() == totalSupplyBefore + amount; } rule mintRevertingConditions(env e) { - address account; + address account; uint256 amount; - - require totalSupply() + amount <= max_uint; // proof in totalSupplyNeverOverflow - - bool nonOwner = e.msg.sender != contractOwner(); - bool payable = e.msg.value != 0; + require totalSupply() + amount <= max_uint; // proof in totalSupplyNeverOverflow + + bool nonOwner = e.msg.sender != contractOwner(); + bool payable = e.msg.value != 0; bool isExpectedToRevert = nonOwner || payable; - mint@withrevert(e, account, amount); // if(lastReverted){ @@ -338,14 +282,11 @@ rule mintRevertingConditions(env e) { } rule mintDoesNotAffectThirdParty(env e) { - address addr1; - uint256 amount; - + address addr1; + uint256 amount; address addr2; require addr1 != addr2; - - uint256 before = balanceOf(addr2); - + uint256 before = balanceOf(addr2); mint(e, addr1, amount); assert balanceOf(addr2) == before; } @@ -357,36 +298,33 @@ rule mintDoesNotAffectThirdParty(env e) { */ rule burnIntegrity(env e) { requireInvariant totalSupplyIsSumOfBalances(); - address from; uint256 amount; - + // cache state - uint256 fromBalanceBefore = balanceOf(from); - uint256 totalSupplyBefore = totalSupply(); - + uint256 fromBalanceBefore = balanceOf(from); + uint256 totalSupplyBefore = totalSupply(); + // run transaction burn(e, from, amount); - + // check outcome - + // assert contract owner was the one called assert e.msg.sender == contractOwner(), "Only contract owner can call burn."; - + // updates balance and totalSupply - assert balanceOf(from) == fromBalanceBefore - amount; - assert totalSupply() == totalSupplyBefore - amount; + assert balanceOf(from) == fromBalanceBefore - amount; + assert totalSupply() == totalSupplyBefore - amount; } rule burnRevertingConditions(env e) { - address account; + address account; uint256 amount; - - bool notOwner = e.msg.sender != contractOwner(); - bool payable = e.msg.value != 0; + bool notOwner = e.msg.sender != contractOwner(); + bool payable = e.msg.value != 0; bool notEnoughBalance = balanceOf(account) < amount; bool isExpectedToRevert = notEnoughBalance || payable || notOwner; - burn@withrevert(e, account, amount); // if(lastReverted) { // assert isExpectedToRevert; @@ -394,20 +332,17 @@ rule burnRevertingConditions(env e) { // else { // assert !isExpectedToRevert; // } - + assert lastReverted <=> isExpectedToRevert; } -rule burnDoesNotAffectThirdParty( env e) { - address addr1; - uint256 amount; - +rule burnDoesNotAffectThirdParty(env e) { + address addr1; + uint256 amount; address addr2; require addr1 != addr2; - uint256 before = balanceOf(addr2); - - burn(e, addr1, amount); + burn(e, addr1, amount); assert balanceOf(addr2) == before; } @@ -418,56 +353,51 @@ rule burnDoesNotAffectThirdParty( env e) { */ rule transferIntegrity(env e) { requireInvariant totalSupplyIsSumOfBalances(); - address holder = e.msg.sender; address recipient; uint256 amount; - + // cache state - uint256 holderBalanceBefore = balanceOf(holder); + uint256 holderBalanceBefore = balanceOf(holder); uint256 recipientBalanceBefore = balanceOf(recipient); - + // run transaction transfer(e, recipient, amount); - + // check outcome - + // balances of holder and recipient are updated - assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount); } // We are checking just that if transfer(10) works, then also transfer(5);transfer(5) works. //We do not check the other direction (does not make sense becase of overflow reverts, i.e. does not hold) rule transferIsOneWayAdditive(env e) { - address recipient; - uint256 amount_a; + address recipient; + uint256 amount_a; uint256 amount_b; - mathint sum_amount = amount_a + amount_b; - require sum_amount < max_uint256; - storage init = lastStorage; // saves storage - - transfer(e, recipient, assert_uint256(sum_amount)); - storage after1 = lastStorage; - - transfer@withrevert(e, recipient, amount_a) at init; // restores storage - assert !lastReverted; //if the transfer passed with sum, it should pass with both summands individually - transfer@withrevert(e, recipient, amount_b); - assert !lastReverted; - storage after2 = lastStorage; - - assert after1[currentContract] == after2[currentContract]; + mathint sum_amount = amount_a + amount_b; + require sum_amount < max_uint256; + storage init = lastStorage; // saves storage + + transfer(e, recipient, assert_uint256(sum_amount)); + storage after1 = lastStorage; + transfer@withrevert(e, recipient, amount_a) at init; // restores storage + assert !lastReverted; //if the transfer passed with sum, it should pass with both summands individually + transfer@withrevert(e, recipient, amount_b); + assert !lastReverted; + storage after2 = lastStorage; + assert after1[currentContract] == after2[currentContract]; } // overflow is not possible (sumOfBlances = totalSupply <= maxuint) rule transferRevertingConditions(env e) { - uint256 amount; - address account; - - bool payable = e.msg.value != 0; + uint256 amount; + address account; + bool payable = e.msg.value != 0; bool notEnoughBalance = balanceOf(e.msg.sender) < amount; bool isExpectedToRevert = payable || notEnoughBalance; - transfer@withrevert(e, account, amount); // if(lastReverted) { // assert isExpectedToRevert; @@ -475,20 +405,17 @@ rule transferRevertingConditions(env e) { // else { // assert !isExpectedToRevert; // } - + assert lastReverted <=> isExpectedToRevert; } -rule transferDoesNotAffectThirdParty( env e) { - address addr1; - uint256 amount; - +rule transferDoesNotAffectThirdParty(env e) { + address addr1; + uint256 amount; address addr2; require addr1 != addr2 && addr2 != e.msg.sender; - uint256 before = balanceOf(addr2); - - transfer(e, addr1, amount); + transfer(e, addr1, amount); assert balanceOf(addr2) == before; } @@ -499,100 +426,87 @@ rule transferDoesNotAffectThirdParty( env e) { */ rule transferFromIntegrity(env e) { requireInvariant totalSupplyIsSumOfBalances(); - address spender = e.msg.sender; address holder; address recipient; uint256 amount; - + // cache state - uint256 allowanceBefore = allowance(holder, spender); - uint256 holderBalanceBefore = balanceOf(holder); + uint256 allowanceBefore = allowance(holder, spender); + uint256 holderBalanceBefore = balanceOf(holder); uint256 recipientBalanceBefore = balanceOf(recipient); - + // run transaction transferFrom(e, holder, recipient, amount); - + // allowance is valid & updated assert allowanceBefore >= amount; assert allowance(holder, spender) == (allowanceBefore == max_uint256 ? max_uint256 : allowanceBefore - amount); - + // balances of holder and recipient are updated - assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert balanceOf(holder) == holderBalanceBefore - (holder == recipient ? 0 : amount); assert balanceOf(recipient) == recipientBalanceBefore + (holder == recipient ? 0 : amount); } // overflow is not possible (sumOfBlances = totalSupply <= maxuint) rule transferFromRevertingConditions(env e) { address owner; - address spender = e.msg.sender; - address recepient; - - uint256 allowed = allowance(owner, spender); - uint256 transfered; - - bool sendEthToNotPayable = e.msg.value != 0; - bool allowanceIsLow = allowed < transfered; + address spender = e.msg.sender; + address recepient; + uint256 allowed = allowance(owner, spender); + uint256 transfered; + bool sendEthToNotPayable = e.msg.value != 0; + bool allowanceIsLow = allowed < transfered; bool notEnoughBalance = balanceOf(owner) < transfered; - - bool isExpectedToRevert = sendEthToNotPayable || allowanceIsLow || notEnoughBalance; - - transferFrom@withrevert(e, owner, recepient, transfered); - + bool isExpectedToRevert = sendEthToNotPayable || allowanceIsLow || notEnoughBalance; + transferFrom@withrevert(e, owner, recepient, transfered); + // if(lastReverted) { // assert isExpectedToRevert; // } else { // assert !(isExpectedToRevert); // } - + assert lastReverted <=> isExpectedToRevert; } rule transferFromDoesNotAffectThirdParty(env e) { - address spender = e.msg.sender; - address owner; - address recepient; - address thirdParty; + address spender = e.msg.sender; + address owner; + address recepient; + address thirdParty; address everyUser; - - require thirdParty != owner && thirdParty != recepient && thirdParty != spender; - - uint256 thirdPartyBalanceBefore = balanceOf(thirdParty); + require thirdParty != owner && thirdParty != recepient && thirdParty != spender; + uint256 thirdPartyBalanceBefore = balanceOf(thirdParty); uint256 thirdPartyAllowanceBefore = allowance(thirdParty, everyUser); - uint256 transfered; - - transferFrom(e, owner, recepient, transfered); - - uint256 thirdPartyBalanceAfter = balanceOf(thirdParty); - uint256 thirdPartyAllowanceAfter = allowance(thirdParty, everyUser); - - assert thirdPartyBalanceBefore == thirdPartyBalanceAfter; + transferFrom(e, owner, recepient, transfered); + uint256 thirdPartyBalanceAfter = balanceOf(thirdParty); + uint256 thirdPartyAllowanceAfter = allowance(thirdParty, everyUser); + assert thirdPartyBalanceBefore == thirdPartyBalanceAfter; assert thirdPartyAllowanceBefore == thirdPartyAllowanceAfter; } // We are checking just that if transfer(10) works, then also transfer(5);transfer(5) works. //We do not check the other direction (does not make sense becase of overflow reverts, i.e. does not hold) rule transferFromIsOneWayAdditive(env e) { - address recipient; + address recipient; address owner; address spender = e.msg.sender; - uint256 amount_a; + uint256 amount_a; uint256 amount_b; - mathint sum_amount = amount_a + amount_b; - require sum_amount < max_uint256; - storage init = lastStorage; // saves storage - - transferFrom(e, owner, recipient, assert_uint256(sum_amount)); - storage after1 = lastStorage; - - transferFrom@withrevert(e, owner, recipient, amount_a) at init; // restores storage - assert !lastReverted; //if the transfer passed with sum, it should pass with both summands individually - transferFrom@withrevert(e, owner, recipient, amount_b); - assert !lastReverted; - storage after2 = lastStorage; - - assert after1[currentContract] == after2[currentContract]; + mathint sum_amount = amount_a + amount_b; + require sum_amount < max_uint256; + storage init = lastStorage; // saves storage + + transferFrom(e, owner, recipient, assert_uint256(sum_amount)); + storage after1 = lastStorage; + transferFrom@withrevert(e, owner, recipient, amount_a) at init; // restores storage + assert !lastReverted; //if the transfer passed with sum, it should pass with both summands individually + transferFrom@withrevert(e, owner, recipient, amount_b); + assert !lastReverted; + storage after2 = lastStorage; + assert after1[currentContract] == after2[currentContract]; } /* @@ -604,46 +518,37 @@ rule approveIntegrity(env e) { address holder = e.msg.sender; address spender; uint256 amount; - approve(e, spender, amount); - assert allowance(holder, spender) == amount; } rule approveRevertingConditions(env e) { - address spender; - address owner = e.msg.sender; - uint256 amount; - - bool payable = e.msg.value != 0; - bool isExpectedToRevert = payable; - - approve@withrevert(e, spender, amount); - - // if(lastReverted){ - // assert isExpectedToRevert; - // } else { - // assert !isExpectedToRevert; - // } - + address spender; + address owner = e.msg.sender; + uint256 amount; + bool payable = e.msg.value != 0; + bool isExpectedToRevert = payable; + approve@withrevert(e, spender, amount); + + // if(lastReverted){ + // assert isExpectedToRevert; + // } else { + // assert !isExpectedToRevert; + // } + assert lastReverted <=> isExpectedToRevert; } rule approveDoesNotAffectThirdParty(env e) { - address spender; - address owner = e.msg.sender; - address thirdParty; - address everyUser; - + address spender; + address owner = e.msg.sender; + address thirdParty; + address everyUser; require thirdParty != owner && thirdParty != spender; - uint amount; - uint256 thirdPartyAllowanceBefore = allowance(thirdParty, everyUser); - - approve(e, spender, amount); - - uint256 thirdPartyAllowanceAfter = allowance(thirdParty, everyUser); - + uint256 thirdPartyAllowanceBefore = allowance(thirdParty, everyUser); + approve(e, spender, amount); + uint256 thirdPartyAllowanceAfter = allowance(thirdParty, everyUser); assert thirdPartyAllowanceBefore == thirdPartyAllowanceBefore; } @@ -660,38 +565,37 @@ rule permitIntegrity(env e) { uint8 v; bytes32 r; bytes32 s; - + // cache state - uint256 nonceBefore = nonces(holder); + uint256 nonceBefore = nonces(holder); // sanity: nonce overflow, which possible in theory, is assumed to be impossible in practice - require nonceBefore < max_uint256; + require nonceBefore < max_uint256; // run transaction permit(e, holder, spender, amount, deadline, v, r, s); - + // check outcome - + // allowance and nonce are updated assert allowance(holder, spender) == amount; assert nonces(holder) == nonceBefore + 1; - + // deadline was respected assert deadline >= e.block.timestamp; } -rule permitRevertWhenDeadlineExpiers(env e){ - address owner; - address spender; - uint256 value; - uint256 deadline; - uint8 v; - bytes32 r; - bytes32 s; - - require deadline < e.block.timestamp; - permit@withrevert(e,owner,spender,value,deadline,v,r,s); - assert lastReverted; +rule permitRevertWhenDeadlineExpiers(env e) { + address owner; + address spender; + uint256 value; + uint256 deadline; + uint8 v; + bytes32 r; + bytes32 s; + require deadline < e.block.timestamp; + permit@withrevert(e, owner, spender, value, deadline, v, r, s); + assert lastReverted; } rule permitDoesNotAffectThirdParty(env e) { @@ -702,25 +606,18 @@ rule permitDoesNotAffectThirdParty(env e) { uint8 v; bytes32 r; bytes32 s; - address thirdParty; address everyUser; - require thirdParty != holder && thirdParty != spender; - - uint256 thirdPartyAllowanceBefore = allowance(thirdParty, everyUser); - - approve(e, spender, amount); - - uint256 thirdPartyAllowanceAfter = allowance(thirdParty, everyUser); - + uint256 thirdPartyAllowanceBefore = allowance(thirdParty, everyUser); + approve(e, spender, amount); + uint256 thirdPartyAllowanceAfter = allowance(thirdParty, everyUser); assert thirdPartyAllowanceBefore == thirdPartyAllowanceBefore; } -rule permitDenialOfService(){ +rule permitDenialOfService() { env e1; env e2; - address clientHolder; address clientSpender; uint256 clientAmount; @@ -728,7 +625,6 @@ rule permitDenialOfService(){ uint8 clientV; bytes32 clientR; bytes32 clientS; - address attackerHolder; address attackerSpender; uint256 attackerAmount; @@ -736,25 +632,19 @@ rule permitDenialOfService(){ uint8 attackerV; bytes32 attackerR; bytes32 attackerS; - require e1.msg.sender != e2.msg.sender; - storage init = lastStorage; - permit(e1, clientHolder, clientSpender, clientAmount, clientDeadline, clientV, clientR, clientS); // if pass not reverted permit(e2, attackerHolder, attackerSpender, attackerAmount, attackerDeadline, attackerV, attackerR, attackerS) at init; // attacker attack - + permit(e1, clientHolder, clientSpender, clientAmount, clientDeadline, clientV, clientR, clientS); - satisfy true; } - -rule permitFrontRun(){ +rule permitFrontRun() { env e1; env e2; - address clientHolder; address clientSpender; uint256 clientAmount; @@ -762,7 +652,6 @@ rule permitFrontRun(){ uint8 clientV; bytes32 clientR; bytes32 clientS; - address attackerHolder; address attackerSpender; uint256 attackerAmount; @@ -770,16 +659,12 @@ rule permitFrontRun(){ uint8 attackerV; bytes32 attackerR; bytes32 attackerS; - require e1.msg.sender != e2.msg.sender; - storage init = lastStorage; - permit(e1, clientHolder, clientSpender, clientAmount, clientDeadline, clientV, clientR, clientS); // if pass not reverted permit(e2, attackerHolder, attackerSpender, attackerAmount, attackerDeadline, attackerV, attackerR, attackerS) at init; // attacker attack - + permit@withrevert(e1, clientHolder, clientSpender, clientAmount, clientDeadline, clientV, clientR, clientS); - assert !lastReverted, "Cannot sign permit with same signature"; -} \ No newline at end of file +} diff --git a/DEFI/ERC4626/certora/specs/ERC4626.spec b/DEFI/ERC4626/certora/specs/ERC4626.spec index 682efd97..d6ae401c 100644 --- a/DEFI/ERC4626/certora/specs/ERC4626.spec +++ b/DEFI/ERC4626/certora/specs/ERC4626.spec @@ -5,12 +5,10 @@ * */ - // reference from the spec to additional contracts used in the verification -using DummyERC20A as ERC20a; -using DummyERC20B as ERC20b; - +using DummyERC20A as ERC20a; +using DummyERC20B as ERC20b; /* Declaration of methods that are used in the rules. envfree indicate that @@ -18,48 +16,41 @@ using DummyERC20B as ERC20b; Methods that are not declared here are assumed to be dependent on env. */ methods { - function name() external returns string envfree; - function symbol() external returns string envfree; - function decimals() external returns uint8 envfree; - function asset() external returns address envfree; - - function totalSupply() external returns uint256 envfree; - function balanceOf(address) external returns uint256 envfree; - function nonces(address) external returns uint256 envfree; - - function approve(address,uint256) external returns bool; - function deposit(uint256,address) external; - function mint(uint256,address) external; - function withdraw(uint256,address,address) external; - function redeem(uint256,address,address) external; - - function totalAssets() external returns uint256 envfree; - function userAssets(address) external returns uint256 envfree; - function convertToShares(uint256) external returns uint256 envfree; - function convertToAssets(uint256) external returns uint256 envfree; - function previewDeposit(uint256) external returns uint256 envfree; - function previewMint(uint256) external returns uint256 envfree; - function previewWithdraw(uint256) external returns uint256 envfree; - function previewRedeem(uint256) external returns uint256 envfree; - - function maxDeposit(address) external returns uint256 envfree; - function maxMint(address) external returns uint256 envfree; - function maxWithdraw(address) external returns uint256 envfree; - function maxRedeem(address) external returns uint256 envfree; - - function permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external; - function DOMAIN_SEPARATOR() external returns bytes32; - + function name() external returns (string) envfree; + function symbol() external returns (string) envfree; + function decimals() external returns (uint8) envfree; + function asset() external returns (address) envfree; + function totalSupply() external returns (uint256) envfree; + function balanceOf(address) external returns (uint256) envfree; + function nonces(address) external returns (uint256) envfree; + function approve(address, uint256) external returns (bool); + function deposit(uint256, address) external; + function mint(uint256, address) external; + function withdraw(uint256, address, address) external; + function redeem(uint256, address, address) external; + function totalAssets() external returns (uint256) envfree; + function userAssets(address) external returns (uint256) envfree; + function convertToShares(uint256) external returns (uint256) envfree; + function convertToAssets(uint256) external returns (uint256) envfree; + function previewDeposit(uint256) external returns (uint256) envfree; + function previewMint(uint256) external returns (uint256) envfree; + function previewWithdraw(uint256) external returns (uint256) envfree; + function previewRedeem(uint256) external returns (uint256) envfree; + function maxDeposit(address) external returns (uint256) envfree; + function maxMint(address) external returns (uint256) envfree; + function maxWithdraw(address) external returns (uint256) envfree; + function maxRedeem(address) external returns (uint256) envfree; + function permit(address, address, uint256, uint256, uint8, bytes32, bytes32) external; + function DOMAIN_SEPARATOR() external returns (bytes32); + //// #ERC20 methods - function _.balanceOf(address) external => DISPATCHER(true); - function _.transfer(address,uint256) external => DISPATCHER(true); - function _.transferFrom(address,address,uint256) external => DISPATCHER(true); - - function ERC20a.balanceOf(address) external returns uint256 envfree; - function ERC20a.allowance(address, address) external returns uint256 envfree; - function ERC20a.transferFrom(address,address,uint256) external returns bool; - - function ERC20b.allowance(address, address) external returns uint256 envfree; + function _.balanceOf(address) external => DISPATCHER(true); + function _.transfer(address, uint256) external => DISPATCHER(true); + function _.transferFrom(address, address, uint256) external => DISPATCHER(true); + function ERC20a.balanceOf(address) external returns (uint256) envfree; + function ERC20a.allowance(address, address) external returns (uint256) envfree; + function ERC20a.transferFrom(address, address, uint256) external returns (bool); + function ERC20b.allowance(address, address) external returns (uint256) envfree; } //////////////////////////////////////////////////////////////////////////////// @@ -67,16 +58,16 @@ methods { //////////////////////////////////////////////////////////////////////////////// persistent ghost bool callMade; -persistent ghost bool delegatecallMade; +persistent ghost bool delegatecallMade; -hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { +hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength, uint rc) { if (addr != currentContract.asset) { callMade = true; } } -hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { +hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength, uint rc) { delegatecallMade = true; } @@ -84,15 +75,12 @@ hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint r This rule proves there are no instances in the code in which the user can act as the contract. By proving this rule we can safely assume in our spec that e.msg.sender != currentContract. */ -rule noDynamicCalls { +rule noDynamicCalls() { method f; env e; calldataarg args; - require !callMade && !delegatecallMade; - f(e, args); - assert !callMade && !delegatecallMade; } @@ -100,89 +88,69 @@ rule noDynamicCalls { //// # asset To shares mathematical properties ///// //////////////////////////////////////////////////////////////////////////////// -rule conversionOfZero { +rule conversionOfZero() { uint256 convertZeroShares = convertToAssets(0); uint256 convertZeroAssets = convertToShares(0); - - assert convertZeroShares == 0, - "converting zero shares must return zero assets"; - assert convertZeroAssets == 0, - "converting zero assets must return zero shares"; + assert convertZeroShares == 0, "converting zero shares must return zero assets"; + assert convertZeroAssets == 0, "converting zero assets must return zero shares"; } rule convertToAssetsWeakAdditivity() { - uint256 sharesA; uint256 sharesB; - require sharesA + sharesB < max_uint128 - && convertToAssets(sharesA) + convertToAssets(sharesB) < max_uint256 - && convertToAssets(require_uint256(sharesA + sharesB)) < max_uint256; - assert convertToAssets(sharesA) + convertToAssets(sharesB) <= convertToAssets(require_uint256(sharesA + sharesB)), - "converting sharesA and sharesB to assets then summing them must yield a smaller or equal result to summing them then converting"; + uint256 sharesA; + uint256 sharesB; + require sharesA + sharesB < max_uint128 && convertToAssets(sharesA) + convertToAssets(sharesB) < max_uint256 && convertToAssets(require_uint256(sharesA + sharesB)) < max_uint256; + assert convertToAssets(sharesA) + convertToAssets(sharesB) <= convertToAssets(require_uint256(sharesA + sharesB)), "converting sharesA and sharesB to assets then summing them must yield a smaller or equal result to summing them then converting"; } rule convertToSharesWeakAdditivity() { - uint256 assetsA; uint256 assetsB; - require assetsA + assetsB < max_uint128 - && convertToAssets(assetsA) + convertToAssets(assetsB) < max_uint256 - && convertToAssets(require_uint256(assetsA + assetsB)) < max_uint256; - assert convertToAssets(assetsA) + convertToAssets(assetsB) <= convertToAssets(require_uint256(assetsA + assetsB)), - "converting assetsA and assetsB to shares then summing them must yield a smaller or equal result to summing them then converting"; + uint256 assetsA; + uint256 assetsB; + require assetsA + assetsB < max_uint128 && convertToAssets(assetsA) + convertToAssets(assetsB) < max_uint256 && convertToAssets(require_uint256(assetsA + assetsB)) < max_uint256; + assert convertToAssets(assetsA) + convertToAssets(assetsB) <= convertToAssets(require_uint256(assetsA + assetsB)), "converting assetsA and assetsB to shares then summing them must yield a smaller or equal result to summing them then converting"; } -rule conversionWeakMonotonicity { - uint256 smallerShares; uint256 largerShares; - uint256 smallerAssets; uint256 largerAssets; - - assert smallerShares < largerShares => convertToAssets(smallerShares) <= convertToAssets(largerShares), - "converting more shares must yield equal or greater assets"; - assert smallerAssets < largerAssets => convertToShares(smallerAssets) <= convertToShares(largerAssets), - "converting more assets must yield equal or greater shares"; +rule conversionWeakMonotonicity() { + uint256 smallerShares; + uint256 largerShares; + uint256 smallerAssets; + uint256 largerAssets; + assert smallerShares < largerShares => convertToAssets(smallerShares) <= convertToAssets(largerShares), "converting more shares must yield equal or greater assets"; + assert smallerAssets < largerAssets => convertToShares(smallerAssets) <= convertToShares(largerAssets), "converting more assets must yield equal or greater shares"; } rule conversionWeakIntegrity() { uint256 sharesOrAssets; - assert convertToShares(convertToAssets(sharesOrAssets)) <= sharesOrAssets, - "converting shares to assets then back to shares must return shares less than or equal to the original amount"; - assert convertToAssets(convertToShares(sharesOrAssets)) <= sharesOrAssets, - "converting assets to shares then back to assets must return assets less than or equal to the original amount"; + assert convertToShares(convertToAssets(sharesOrAssets)) <= sharesOrAssets, "converting shares to assets then back to shares must return shares less than or equal to the original amount"; + assert convertToAssets(convertToShares(sharesOrAssets)) <= sharesOrAssets, "converting assets to shares then back to assets must return assets less than or equal to the original amount"; } -rule convertToCorrectness(uint256 amount, uint256 shares) -{ +rule convertToCorrectness(uint256 amount, uint256 shares) { assert amount >= convertToAssets(convertToShares(amount)); assert shares >= convertToShares(convertToAssets(shares)); } - //////////////////////////////////////////////////////////////////////////////// //// # Unit Test ///// //////////////////////////////////////////////////////////////////////////////// rule depositMonotonicity() { - env e; storage start = lastStorage; - - uint256 smallerAssets; uint256 largerAssets; + env e; + storage start = lastStorage; + uint256 smallerAssets; + uint256 largerAssets; address receiver; - require currentContract != e.msg.sender && currentContract != receiver; - + require currentContract != e.msg.sender && currentContract != receiver; safeAssumptions(e, e.msg.sender, receiver); - deposit(e, smallerAssets, receiver); - uint256 smallerShares = balanceOf(receiver) ; - + uint256 smallerShares = balanceOf(receiver); deposit(e, largerAssets, receiver) at start; - uint256 largerShares = balanceOf(receiver) ; - - assert smallerAssets < largerAssets => smallerShares <= largerShares, - "when supply tokens outnumber asset tokens, a larger deposit of assets must produce an equal or greater number of shares"; + uint256 largerShares = balanceOf(receiver); + assert smallerAssets < largerAssets => smallerShares <= largerShares, "when supply tokens outnumber asset tokens, a larger deposit of assets must produce an equal or greater number of shares"; } - -rule zeroDepositZeroShares(uint assets, address receiver) -{ +rule zeroDepositZeroShares(uint assets, address receiver) { env e; - - uint shares = deposit(e,assets, receiver); - + uint shares = deposit(e, assets, receiver); assert shares == 0 <=> assets == 0; } @@ -191,107 +159,90 @@ rule zeroDepositZeroShares(uint assets, address receiver) //////////////////////////////////////////////////////////////////////////////// invariant assetsMoreThanSupply() - totalAssets() >= totalSupply() - { + totalAssets() >= totalSupply() { preserved with (env e) { require e.msg.sender != currentContract; address any; - safeAssumptions(e, any , e.msg.sender); + safeAssumptions(e, any, e.msg.sender); } } -invariant noAssetsIfNoSupply() - (userAssets(currentContract) == 0 => totalSupply() == 0) && - (totalAssets() == 0 => (totalSupply() == 0)) { +invariant noAssetsIfNoSupply() + (userAssets(currentContract) == 0 => totalSupply() == 0) && (totalAssets() == 0 => (totalSupply() == 0)) { preserved with (env e) { address any; safeAssumptions(e, any, e.msg.sender); } } +// see defition in "helpers and miscellaneous" section invariant noSupplyIfNoAssets() - noSupplyIfNoAssetsDef() // see defition in "helpers and miscellaneous" section - { + noSupplyIfNoAssetsDef() { preserved with (env e) { safeAssumptions(e, _, e.msg.sender); } } - - ghost mathint sumOfBalances { init_state axiom sumOfBalances == 0; } -hook Sstore balanceOf[KEY address addy] uint256 newValue (uint256 oldValue) { +hook Sstore balanceOf[KEY address addy] uint256 newValue (uint256 oldValue) { sumOfBalances = sumOfBalances + newValue - oldValue; } -hook Sload uint256 val balanceOf[KEY address addy] { +hook Sload uint256 val balanceOf[KEY address addy] { require sumOfBalances >= val; } invariant totalSupplyIsSumOfBalances() totalSupply() == sumOfBalances; - - //////////////////////////////////////////////////////////////////////////////// //// # State Transition ///// //////////////////////////////////////////////////////////////////////////////// - rule totalsMonotonicity() { - method f; env e; calldataarg args; - require e.msg.sender != currentContract; + method f; + env e; + calldataarg args; + require e.msg.sender != currentContract; uint256 totalSupplyBefore = totalSupply(); uint256 totalAssetsBefore = totalAssets(); address receiver; safeAssumptions(e, receiver, e.msg.sender); callReceiverFunctions(f, e, receiver); - uint256 totalSupplyAfter = totalSupply(); uint256 totalAssetsAfter = totalAssets(); // possibly assert totalSupply and totalAssets must not change in opposite directions - assert totalSupplyBefore < totalSupplyAfter <=> totalAssetsBefore < totalAssetsAfter, - "if totalSupply changes by a larger amount, the corresponding change in totalAssets must remain the same or grow"; - assert totalSupplyAfter == totalSupplyBefore => totalAssetsBefore == totalAssetsAfter, - "equal size changes to totalSupply must yield equal size changes to totalAssets"; + assert totalSupplyBefore < totalSupplyAfter <=> totalAssetsBefore < totalAssetsAfter, "if totalSupply changes by a larger amount, the corresponding change in totalAssets must remain the same or grow"; + assert totalSupplyAfter == totalSupplyBefore => totalAssetsBefore == totalAssetsAfter, "equal size changes to totalSupply must yield equal size changes to totalAssets"; } rule underlyingCannotChange() { address originalAsset = asset(); - - method f; env e; calldataarg args; + method f; + env e; + calldataarg args; f(e, args); - address newAsset = asset(); - - assert originalAsset == newAsset, - "the underlying asset of a contract must not change"; + assert originalAsset == newAsset, "the underlying asset of a contract must not change"; } //////////////////////////////////////////////////////////////////////////////// //// # High Level ///// //////////////////////////////////////////////////////////////////////////////// - -rule dustFavorsTheHouse(uint assetsIn ) -{ +rule dustFavorsTheHouse(uint assetsIn) { env e; - require e.msg.sender != currentContract; - safeAssumptions(e,e.msg.sender,e.msg.sender); + safeAssumptions(e, e.msg.sender, e.msg.sender); uint256 totalSupplyBefore = totalSupply(); - uint balanceBefore = ERC20a.balanceOf(currentContract); - - uint shares = deposit(e,assetsIn, e.msg.sender); - uint assetsOut = redeem(e,shares,e.msg.sender,e.msg.sender); - + uint shares = deposit(e, assetsIn, e.msg.sender); + uint assetsOut = redeem(e, shares, e.msg.sender, e.msg.sender); uint balanceAfter = ERC20a.balanceOf(currentContract); - assert balanceAfter >= balanceBefore; } @@ -299,24 +250,22 @@ rule dustFavorsTheHouse(uint assetsIn ) //// # Risk Analysis ///////// //////////////////////////////////////////////////////////////////////////////// - invariant vaultSolvency() - totalAssets() >= totalSupply() && userAssets(currentContract) >= totalAssets() { - preserved with(env e){ + totalAssets() >= totalSupply() && userAssets(currentContract) >= totalAssets() { + preserved with (env e) { requireInvariant zeroAllowanceOnAssets(e.msg.sender); requireInvariant totalSupplyIsSumOfBalances(); require e.msg.sender != currentContract; - require currentContract != asset(); + require currentContract != asset(); } } - - -rule redeemingAllValidity() { - address owner; - uint256 shares; require shares == balanceOf(owner); - - env e; safeAssumptions(e, _, owner); +rule redeemingAllValidity() { + address owner; + uint256 shares; + require shares == balanceOf(owner); + env e; + safeAssumptions(e, _, owner); redeem(e, shares, _, owner); uint256 ownerBalanceAfter = balanceOf(owner); assert ownerBalanceAfter == 0; @@ -324,7 +273,7 @@ rule redeemingAllValidity() { invariant zeroAllowanceOnAssets(address user) ERC20a.allowance(currentContract, user) == 0 && ERC20b.allowance(currentContract, user) == 0 { - preserved with(env e) { + preserved with (env e) { require e.msg.sender != currentContract; } } @@ -334,89 +283,60 @@ invariant zeroAllowanceOnAssets(address user) //////////////////////////////////////////////////////////////////////////////// rule contributingProducesShares(method f) -filtered { - f -> f.selector == sig:deposit(uint256,address).selector - || f.selector == sig:mint(uint256,address).selector -} -{ - env e; uint256 assets; uint256 shares; - address contributor; require contributor == e.msg.sender; +filtered { f -> f.selector == sig:deposit(uint256, address).selector || f.selector == sig:mint(uint256, address).selector } { + env e; + uint256 assets; + uint256 shares; + address contributor; + require contributor == e.msg.sender; address receiver; - require currentContract != contributor - && currentContract != receiver; - + require currentContract != contributor && currentContract != receiver; require previewDeposit(assets) + balanceOf(receiver) <= max_uint256; // safe assumption because call to _mint will revert if totalSupply += amount overflows require shares + balanceOf(receiver) <= max_uint256; // same as above - + safeAssumptions(e, contributor, receiver); - uint256 contributorAssetsBefore = userAssets(contributor); uint256 receiverSharesBefore = balanceOf(receiver); - callContributionMethods(e, f, assets, shares, receiver); - uint256 contributorAssetsAfter = userAssets(contributor); uint256 receiverSharesAfter = balanceOf(receiver); - - assert contributorAssetsBefore > contributorAssetsAfter <=> receiverSharesBefore < receiverSharesAfter, - "a contributor's assets must decrease if and only if the receiver's shares increase"; + assert contributorAssetsBefore > contributorAssetsAfter <=> receiverSharesBefore < receiverSharesAfter, "a contributor's assets must decrease if and only if the receiver's shares increase"; } rule onlyContributionMethodsReduceAssets(method f) { - address user; require user != currentContract; + address user; + require user != currentContract; uint256 userAssetsBefore = userAssets(user); - - env e; + env e; calldataarg args; safeAssumptions(e, user, _); - f(e, args); - uint256 userAssetsAfter = userAssets(user); - - assert userAssetsBefore > userAssetsAfter => - (f.selector == sig:deposit(uint256,address).selector || - f.selector == sig:mint(uint256,address).selector || - f.contract == ERC20a || f.contract == ERC20b), - "a user's assets must not go down except on calls to contribution methods or calls directly to the asset."; + assert userAssetsBefore > userAssetsAfter => (f.selector == sig:deposit(uint256, address).selector || f.selector == sig:mint(uint256, address).selector || f.contract == ERC20a || f.contract == ERC20b), "a user's assets must not go down except on calls to contribution methods or calls directly to the asset."; } rule reclaimingProducesAssets(method f) -filtered { - f -> f.selector == sig:withdraw(uint256,address,address).selector - || f.selector == sig:redeem(uint256,address,address).selector -} -{ - env e; uint256 assets; uint256 shares; - address receiver; address owner; - require currentContract != e.msg.sender - && currentContract != receiver - && currentContract != owner; - +filtered { f -> f.selector == sig:withdraw(uint256, address, address).selector || f.selector == sig:redeem(uint256, address, address).selector } { + env e; + uint256 assets; + uint256 shares; + address receiver; + address owner; + require currentContract != e.msg.sender && currentContract != receiver && currentContract != owner; safeAssumptions(e, receiver, owner); - uint256 ownerSharesBefore = balanceOf(owner); uint256 receiverAssetsBefore = userAssets(receiver); - callReclaimingMethods(e, f, assets, shares, receiver, owner); - uint256 ownerSharesAfter = balanceOf(owner); uint256 receiverAssetsAfter = userAssets(receiver); - - assert ownerSharesBefore > ownerSharesAfter <=> receiverAssetsBefore < receiverAssetsAfter, - "an owner's shares must decrease if and only if the receiver's assets increase"; + assert ownerSharesBefore > ownerSharesAfter <=> receiverAssetsBefore < receiverAssetsAfter, "an owner's shares must decrease if and only if the receiver's assets increase"; } - - //////////////////////////////////////////////////////////////////////////////// //// # helpers and miscellaneous ////////// //////////////////////////////////////////////////////////////////////////////// -definition noSupplyIfNoAssetsDef() returns bool = - ( userAssets(currentContract) == 0 => totalSupply() == 0 ) && - ( totalAssets() == 0 <=> ( totalSupply() == 0 )); - +definition noSupplyIfNoAssetsDef() returns bool = (userAssets(currentContract) == 0 => totalSupply() == 0) && (totalAssets() == 0 <=> (totalSupply() == 0)); function safeAssumptions(env e, address receiver, address owner) { require currentContract != asset(); // Although this is not disallowed, we assume the contract's underlying asset is not the contract itself @@ -425,27 +345,22 @@ function safeAssumptions(env e, address receiver, address owner) { requireInvariant noAssetsIfNoSupply(); requireInvariant noSupplyIfNoAssets(); requireInvariant assetsMoreThanSupply(); - - require e.msg.sender != currentContract; // This is proved by rule noDynamicCalls + require e.msg.sender != currentContract; // This is proved by rule noDynamicCalls requireInvariant zeroAllowanceOnAssets(e.msg.sender); - - require ( (receiver != owner => balanceOf(owner) + balanceOf(receiver) <= totalSupply()) && - balanceOf(receiver) <= totalSupply() && - balanceOf(owner) <= totalSupply()); + require((receiver != owner => balanceOf(owner) + balanceOf(receiver) <= totalSupply()) && balanceOf(receiver) <= totalSupply() && balanceOf(owner) <= totalSupply()); } - // A helper function to set the receiver function callReceiverFunctions(method f, env e, address receiver) { uint256 amount; - if (f.selector == sig:deposit(uint256,address).selector) { + if (f.selector == sig:deposit(uint256, address).selector) { deposit(e, amount, receiver); - } else if (f.selector == sig:mint(uint256,address).selector) { + } else if (f.selector == sig:mint(uint256, address).selector) { mint(e, amount, receiver); - } else if (f.selector == sig:withdraw(uint256,address,address).selector) { + } else if (f.selector == sig:withdraw(uint256, address, address).selector) { address owner; withdraw(e, amount, receiver, owner); - } else if (f.selector == sig:redeem(uint256,address,address).selector) { + } else if (f.selector == sig:redeem(uint256, address, address).selector) { address owner; redeem(e, amount, receiver, owner); } else { @@ -454,42 +369,36 @@ function callReceiverFunctions(method f, env e, address receiver) { } } - function callContributionMethods(env e, method f, uint256 assets, uint256 shares, address receiver) { - if (f.selector == sig:deposit(uint256,address).selector) { + if (f.selector == sig:deposit(uint256, address).selector) { deposit(e, assets, receiver); } - if (f.selector == sig:mint(uint256,address).selector) { + if (f.selector == sig:mint(uint256, address).selector) { mint(e, shares, receiver); } } function callReclaimingMethods(env e, method f, uint256 assets, uint256 shares, address receiver, address owner) { - if (f.selector == sig:withdraw(uint256,address,address).selector) { + if (f.selector == sig:withdraw(uint256, address, address).selector) { withdraw(e, assets, receiver, owner); } - if (f.selector == sig:redeem(uint256,address,address).selector) { + if (f.selector == sig:redeem(uint256, address, address).selector) { redeem(e, shares, receiver, owner); } } function callFunctionsWithReceiverAndOwner(env e, method f, uint256 assets, uint256 shares, address receiver, address owner) { - if (f.selector == sig:withdraw(uint256,address,address).selector) { + if (f.selector == sig:withdraw(uint256, address, address).selector) { withdraw(e, assets, receiver, owner); - } - else if (f.selector == sig:redeem(uint256,address,address).selector) { + } else if (f.selector == sig:redeem(uint256, address, address).selector) { redeem(e, shares, receiver, owner); - } - else if (f.selector == sig:deposit(uint256,address).selector) { + } else if (f.selector == sig:deposit(uint256, address).selector) { deposit(e, assets, receiver); - } - else if (f.selector == sig:mint(uint256,address).selector) { + } else if (f.selector == sig:mint(uint256, address).selector) { mint(e, shares, receiver); - } - else if (f.selector == sig:transferFrom(address,address,uint256).selector) { + } else if (f.selector == sig:transferFrom(address, address, uint256).selector) { transferFrom(e, owner, receiver, shares); - } - else { + } else { calldataarg args; f(e, args); } diff --git a/DEFI/LiquidityPool/certora/helpers/erc20.spec b/DEFI/LiquidityPool/certora/helpers/erc20.spec index 387d28ca..3c35882e 100644 --- a/DEFI/LiquidityPool/certora/helpers/erc20.spec +++ b/DEFI/LiquidityPool/certora/helpers/erc20.spec @@ -11,13 +11,13 @@ */ methods { - function _.name() external => DISPATCHER(true); - function _.symbol() external => DISPATCHER(true); - function _.decimals() external => DISPATCHER(true); - function _.totalSupply() external => DISPATCHER(true); - function _.balanceOf(address) external => DISPATCHER(true); - function _.allowance(address,address) external => DISPATCHER(true); - function _.approve(address,uint256) external => DISPATCHER(true); - function _.transfer(address,uint256) external => DISPATCHER(true); - function _.transferFrom(address,address,uint256) external => DISPATCHER(true); + function _.name() external => DISPATCHER(true); + function _.symbol() external => DISPATCHER(true); + function _.decimals() external => DISPATCHER(true); + function _.totalSupply() external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.allowance(address, address) external => DISPATCHER(true); + function _.approve(address, uint256) external => DISPATCHER(true); + function _.transfer(address, uint256) external => DISPATCHER(true); + function _.transferFrom(address, address, uint256) external => DISPATCHER(true); } diff --git a/DEFI/LiquidityPool/certora/specs/Full.spec b/DEFI/LiquidityPool/certora/specs/Full.spec index 8b9f7e02..028072ec 100644 --- a/DEFI/LiquidityPool/certora/specs/Full.spec +++ b/DEFI/LiquidityPool/certora/specs/Full.spec @@ -1,3 +1,4 @@ +error dummy file:240:72: Illegal character: \ /*** This example is a full spec for LiquidityPool. To run this use Certora cli with the conf file runFullPoll.conf @@ -10,25 +11,22 @@ See https://docs.certora.com for a complete guide. using Asset as underlying; using TrivialReceiver as _TrivialReceiver; -methods -{ - function balanceOf(address) external returns(uint256) envfree; - function totalSupply() external returns(uint256) envfree; - function transfer(address, uint256) external returns(bool); - function transferFrom(address, address, uint256) external returns(bool); - function amountToShares(uint256) external returns(uint256) envfree; - function sharesToAmount(uint256) external returns(uint256) envfree; - function depositedAmount() external returns(uint256) envfree; - function deposit(uint256) external returns(uint256); - function withdraw(uint256) external returns(uint256); - function calcPremium(uint256) external returns (uint256) envfree; - - function _.executeOperation(uint256,uint256,address) external => DISPATCHER(true); - function flashLoan(address, uint256) external; - - function underlying.balanceOf(address) external returns(uint256) envfree; - function underlying.allowance(address, address) external returns(uint256) envfree; - function underlying.totalSupply() external returns(uint256) envfree; +methods { + function balanceOf(address) external returns (uint256) envfree; + function totalSupply() external returns (uint256) envfree; + function transfer(address, uint256) external returns (bool); + function transferFrom(address, address, uint256) external returns (bool); + function amountToShares(uint256) external returns (uint256) envfree; + function sharesToAmount(uint256) external returns (uint256) envfree; + function depositedAmount() external returns (uint256) envfree; + function deposit(uint256) external returns (uint256); + function withdraw(uint256) external returns (uint256); + function calcPremium(uint256) external returns (uint256) envfree; + function _.executeOperation(uint256, uint256, address) external => DISPATCHER(true); + function flashLoan(address, uint256) external; + function underlying.balanceOf(address) external returns (uint256) envfree; + function underlying.allowance(address, address) external returns (uint256) envfree; + function underlying.totalSupply() external returns (uint256) envfree; } /* @@ -37,12 +35,11 @@ methods └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ definition lock_on() returns bool = ghostReentrancyStatus == 2; -definition poll_functions(method f) returns bool = f.selector == sig:withdraw(uint256).selector || - f.selector == sig:deposit(uint256).selector || - f.selector == sig:flashLoan(address, uint256).selector; +definition poll_functions(method f) returns bool = f.selector == sig:withdraw(uint256).selector || f.selector == sig:deposit(uint256).selector || f.selector == sig:flashLoan(address, uint256).selector; ghost uint256 ghostReentrancyStatus; + ghost bool lock_status_on_call; hook Sload uint256 status currentContract._status { @@ -54,18 +51,16 @@ hook Sstore currentContract._status uint256 status { } // we are hooking here on "CALL" opcodes in order to simulate reentrancy to a non-view function and check that the function reverts -hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { - lock_status_on_call = lock_on(); +hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength, uint rc) { + lock_status_on_call = lock_on(); } // this rule prove the assumption e.msg.sender != currentContract; -rule reentrancyCheck(env e, method f, calldataarg args) filtered{f -> poll_functions(f)}{ +rule reentrancyCheck(env e, method f, calldataarg args) +filtered { f -> poll_functions(f) } { bool lockBefore = lock_on(); - f(e, args); - bool lockAfter = lock_on(); - assert !lockBefore && !lockAfter; assert lock_status_on_call; } @@ -75,45 +70,37 @@ rule reentrancyCheck(env e, method f, calldataarg args) filtered{f -> poll_funct │ Deposite │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule depositIntegrity(env e){ - +rule depositIntegrity(env e) { require e.msg.sender != currentContract; // this assumption must hold to avoid shares dilute attack - + uint256 amount; uint256 clientBalanceBefore = underlying.balanceOf(e.msg.sender); uint256 clientSharesBefore = balanceOf(e.msg.sender); - uint256 depositedShares = deposit(e, amount); - uint256 clientBalanceAfter = underlying.balanceOf(e.msg.sender); uint256 clientSharesAfter = balanceOf(e.msg.sender); - assert (amount == 0) => (depositedShares == 0) && (clientBalanceBefore == clientBalanceAfter) && (clientSharesBefore == clientSharesAfter); assert (amount > 0) => (clientBalanceBefore - amount == clientBalanceAfter) && (clientSharesBefore + depositedShares == clientSharesAfter); } -rule depositRevertConditions(env e){ - +rule depositRevertConditions(env e) { require e.msg.sender != currentContract; // this assumption must hold to avoid shares dilute attack - + uint256 amount; uint256 clientBalanceBefore = underlying.balanceOf(e.msg.sender); uint256 clientSharesBefore = balanceOf(e.msg.sender); - bool underFlow = clientBalanceBefore - amount < 0; bool emptyPool = totalSupply() == 0 || depositedAmount() == 0; bool clientSharesOverflow = (clientSharesBefore + amount > max_uint256 && emptyPool) || clientSharesBefore + amountToShares(amount) > max_uint256; bool totalSharesOverflow = totalSupply() + amountToShares(amount) > max_uint256; bool contractUnderlyingOverflow = underlying.balanceOf(currentContract) + amount > max_uint256 || depositedAmount() + amount > max_uint256; - bool overflow = clientSharesOverflow || totalSharesOverflow || contractUnderlyingOverflow; + bool overflow = clientSharesOverflow || totalSharesOverflow || contractUnderlyingOverflow; bool payable = e.msg.value != 0; bool reentrancy = lock_on(); bool notEnoughAllowance = underlying.allowance(e.msg.sender, currentContract) < amount; bool zeroShares = amountToShares(amount) == 0 && !emptyPool; bool expectedRevert = underFlow || overflow || payable || reentrancy || notEnoughAllowance || zeroShares; - deposit@withrevert(e, amount); - assert lastReverted <=> expectedRevert; } @@ -121,24 +108,19 @@ rule depositGreaterThanZeroWithMinted(env e) { uint256 amount; require amount > 0; uint256 amountMinted = deposit(e, amount); - assert amount > 0 <=> amountMinted > 0; } -rule splitDepositFavoursTheContract(env e){ +rule splitDepositFavoursTheContract(env e) { uint256 wholeAmount; - uint256 amountA; + uint256 amountA; uint256 amountB; require amountA + amountB == wholeAmount; requireInvariant totalSharesIsZeroWithUnderlyingDeposited(); - storage init = lastStorage; - uint256 wholeShares = deposit(e, wholeAmount); - uint256 sharesA = deposit(e, amountA) at init; uint256 sharesB = deposit(e, amountB); - assert wholeShares >= sharesA + sharesB; } @@ -147,32 +129,25 @@ rule splitDepositFavoursTheContract(env e){ │ Withdraw │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule withdrawIntegrity(env e){ - +rule withdrawIntegrity(env e) { require e.msg.sender != currentContract; // this assumption must hold to avoid shares dilute attack - + uint256 shares; uint256 clientBalanceBefore = underlying.balanceOf(e.msg.sender); uint256 clientSharesBefore = balanceOf(e.msg.sender); - uint256 withdrawAmount = withdraw(e, shares); - uint256 clientBalanceAfter = underlying.balanceOf(e.msg.sender); uint256 clientSharesAfter = balanceOf(e.msg.sender); - - assert (shares == 0) => (withdrawAmount == 0) && (clientBalanceBefore == clientBalanceAfter) && (clientSharesBefore == clientSharesAfter); assert (shares > 0) => (clientBalanceBefore + withdrawAmount == clientBalanceAfter) && (clientSharesBefore - shares == clientSharesAfter); } -rule withdrawRevertConditions(env e){ - +rule withdrawRevertConditions(env e) { require e.msg.sender != currentContract; // this assumption must hold to avoid shares dilute attack - + uint256 amount; uint256 clientBalanceBefore = underlying.balanceOf(e.msg.sender); uint256 clientSharesBefore = balanceOf(e.msg.sender); - bool clientBalanceUnderflow = clientSharesBefore - amount < 0; bool poolUnderflow = underlying.balanceOf(currentContract) - sharesToAmount(amount) < 0 || totalSupply() - amount < 0; bool underflow = clientBalanceUnderflow || poolUnderflow; @@ -183,61 +158,49 @@ rule withdrawRevertConditions(env e){ bool zeroAmount = sharesToAmount(amount) == 0; bool poolIsEmpty = underlying.balanceOf(currentContract) == 0; bool expectedRevert = poolIsEmpty || underflow || overflow || payable || reentrancy || notEnoughAllowance || zeroAmount; - withdraw@withrevert(e, amount); - assert lastReverted <=> expectedRevert; } -rule splitWithdrawFavoursTheContract(env e){ +rule splitWithdrawFavoursTheContract(env e) { uint256 wholeShares; - uint256 sharesA; + uint256 sharesA; uint256 sharesB; require sharesA + sharesB == wholeShares; - storage init = lastStorage; - uint256 wholeAmount = withdraw(e, wholeShares); - uint256 amountA = withdraw(e, sharesA) at init; uint256 amountB = withdraw(e, sharesB); - assert wholeAmount >= amountA + amountB; } - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ FlashLoan, need to ask Nurit for interesting rules, pretty much depended on implementation │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule flashLoanIntegrity(env e){ +rule flashLoanIntegrity(env e) { require e.msg.sender != currentContract; // this assumption must hold to avoid shares dilute attack - + address receiver; uint256 amount; - - uint256 contractUnderlyingBalanceBefore = underlying.balanceOf(currentContract); + uint256 contractUnderlyingBalanceBefore = underlying.balanceOf(currentContract); uint256 contractSharesBefore = balanceOf(currentContract); - flashLoan(e, receiver, amount); - uint256 contractUnderlyingBalanceAfter = underlying.balanceOf(currentContract); uint256 contractSharesAfter = balanceOf(currentContract); - assert (amount == 0) => contractUnderlyingBalanceBefore == contractUnderlyingBalanceAfter; assert (amount > 0) => contractUnderlyingBalanceBefore < contractUnderlyingBalanceAfter; assert contractSharesBefore == contractSharesAfter; } -rule flashLoanRevertConditions(env e){ +rule flashLoanRevertConditions(env e) { require e.msg.sender != currentContract; // this assumption must hold to avoid shares dilute attack - + address receiver; uint256 amount; - bool noPremium = calcPremium(amount) == 0; - bool receiverIsNotIFlashloanAddress = receiver != _TrivialReceiver;\ + bool receiverIsNotIFlashloanAddress = receiver != _TrivialReceiver; bool payable = e.msg.value != 0; bool reentrancy = lock_on(); bool clientUnderflow = underlying.balanceOf(e.msg.sender) - calcPremium(amount) < 0; @@ -248,9 +211,7 @@ rule flashLoanRevertConditions(env e){ bool overflow = poolBlanceOverflow || clientBalanceOverflow; bool notEnoughAllowance = underlying.allowance(e.msg.sender, currentContract) < calcPremium(amount) + amount || underlying.allowance(currentContract, currentContract) < amount; bool isExpectedToRevert = notEnoughAllowance || overflow || underflow || noPremium || receiverIsNotIFlashloanAddress || payable || reentrancy; - flashLoan@withrevert(e, receiver, amount); - assert isExpectedToRevert <=> lastReverted; } @@ -259,12 +220,11 @@ rule flashLoanRevertConditions(env e){ │ Find and show a path for each method. │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule reachability(method f) -{ - env e; - calldataarg args; - f(e,args); - satisfy true; +rule reachability(method f) { + env e; + calldataarg args; + f(e, args); + satisfy true; } /* @@ -273,9 +233,8 @@ rule reachability(method f) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant totalSharesLessThanUnderlyingBalance() - totalSupply() <= underlying.balanceOf(currentContract) - { - preserved with(env e) { + totalSupply() <= underlying.balanceOf(currentContract) { + preserved with (env e) { require e.msg.sender != currentContract; requireInvariant totalSharesLessThanDepositedAmount(); requireInvariant depositedAmountLessThanContractUnderlyingAsset(); @@ -296,9 +255,8 @@ invariant totalSharesLessThanDepositedAmount() └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant depositedAmountLessThanContractUnderlyingAsset() - depositedAmount() <= underlying.balanceOf(currentContract) - { - preserved with(env e) { + depositedAmount() <= underlying.balanceOf(currentContract) { + preserved with (env e) { require e.msg.sender != currentContract; } } @@ -309,7 +267,7 @@ invariant depositedAmountLessThanContractUnderlyingAsset() └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant totalSharesIsZeroWithUnderlyingDeposited() - totalSupply() == 0 <=> depositedAmount() == 0; + totalSupply() == 0 <=> depositedAmount() == 0; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -321,14 +279,12 @@ ghost mathint sumOfShares { init_state axiom sumOfShares == 0; } -hook Sstore _balanceOf[KEY address user] uint256 newSharesBalance (uint256 oldSharesBalance) -{ +hook Sstore _balanceOf[KEY address user] uint256 newSharesBalance (uint256 oldSharesBalance) { sumOfShares = sumOfShares + newSharesBalance - oldSharesBalance; } invariant totalSharesEqualSumOfShares() - totalSupply() == sumOfShares; - + totalSupply() == sumOfShares; /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -352,21 +308,16 @@ invariant totalIsSumBalances() │ Client shares and balance anti-monotonicity ((increase and decrease) or (decrease and increase)) │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule sharesAndBalanceConsistency(env e, method f) filtered { - f -> f.selector != sig:transfer(address,uint256).selector && - f.selector != sig:transferFrom(address,address,uint256).selector - } { +rule sharesAndBalanceConsistency(env e, method f) +filtered { f -> f.selector != sig:transfer(address, uint256).selector && f.selector != sig:transferFrom(address, address, uint256).selector } { require e.msg.sender != currentContract; // this assumption must hold to avoid shares dilute attack - + uint256 UnderlyingBalanceBefore = underlying.balanceOf(e.msg.sender); uint256 SharesBefore = balanceOf(e.msg.sender); - calldataarg args; f(e, args); - uint256 UnderlyingBalanceAfter = underlying.balanceOf(e.msg.sender); uint256 SharesAfter = balanceOf(e.msg.sender); - assert UnderlyingBalanceBefore < UnderlyingBalanceAfter <=> SharesBefore > SharesAfter; } @@ -380,12 +331,9 @@ rule moreSharesMoreWithdraw(env e) { uint256 sharesY; uint256 amountX; uint256 amountY; - storage init = lastStorage; - amountX = withdraw(e, sharesX); amountY = withdraw(e, sharesY) at init; - assert sharesX > sharesY => amountX >= amountY; } @@ -396,14 +344,11 @@ rule moreSharesMoreWithdraw(env e) { */ rule amountRoundingTripFavoursContract(env e) { requireInvariant totalSharesIsZeroWithUnderlyingDeposited(); - uint256 clientAmountBefore = underlying.balanceOf(e.msg.sender); uint256 contractAmountBefore = underlying.balanceOf(currentContract); - uint256 clientShares = deposit(e, clientAmountBefore); uint256 clientAmountAfter = withdraw(e, clientShares); uint256 contractAmountAfter = underlying.balanceOf(currentContract); - assert clientAmountBefore >= clientAmountAfter; assert contractAmountBefore <= contractAmountAfter; } @@ -415,22 +360,20 @@ Bug fixed by calculating deposit amount and use in in the conversions instead of rule sharesRoundingTripFavoursContract(env e) { uint256 clientSharesBefore = balanceOf(e.msg.sender); uint256 contractSharesBefore = balanceOf(currentContract); - requireInvariant totalSharesLessThanDepositedAmount(); require e.msg.sender != currentContract; // this assumption must hold to avoid shares dilute attack - + uint256 depositedAmount = depositedAmount(); - uint256 clientAmount = withdraw(e, clientSharesBefore); uint256 clientSharesAfter = deposit(e, clientAmount); uint256 contractSharesAfter = balanceOf(currentContract); - + /* if client is last and first depositor he will get more shares but still he wont be able to withdraw more underlying asset than deposited amount (which in that case its only his deposit) as proved in noClientHasSharesWithMoreValueThanDepositedAmount invariant. - */ - assert (clientAmount == depositedAmount) => clientSharesBefore <= clientSharesAfter; + */ + assert (clientAmount == depositedAmount) => clientSharesBefore <= clientSharesAfter; // all other states assert (clientAmount < depositedAmount) => clientSharesBefore >= clientSharesAfter; @@ -441,34 +384,34 @@ rule sharesRoundingTripFavoursContract(env e) { prove bug fix */ invariant noClientHasSharesWithMoreValueThanDepositedAmount(address a) - sharesToAmount(balanceOf(a)) <= depositedAmount() - { - preserved with(env e) { - require balanceOf(a) + balanceOf(e.msg.sender) < totalSupply(); - } - preserved transferFrom(address sender, address recipient, uint256 amount) with (env e) { - require balanceOf(sender) + balanceOf(e.msg.sender) + balanceOf(recipient) < totalSupply(); - } - } + sharesToAmount(balanceOf(a)) <= depositedAmount() { + preserved with (env e) { + require balanceOf(a) + balanceOf(e.msg.sender) < totalSupply(); + } + preserved transferFrom(address sender, address recipient, uint256 amount) with (env e) { + require balanceOf(sender) + balanceOf(e.msg.sender) + balanceOf(recipient) < totalSupply(); + } + } + /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Conversions are monotonic increasing functions. │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule amountToSharesConversion(env e){ +rule amountToSharesConversion(env e) { uint256 amountA; uint256 amountB; assert amountA <= amountB => amountToShares(amountA) <= amountToShares(amountB); } -rule sharesToAmountConversion(env e){ +rule sharesToAmountConversion(env e) { uint256 sharesA; uint256 sharesB; assert sharesA <= sharesB => sharesToAmount(sharesA) <= sharesToAmount(sharesB); } -rule calculatePremium(env e){ +rule calculatePremium(env e) { uint256 amountA; uint256 amountB; assert amountA <= amountB => calcPremium(amountA) <= calcPremium(amountB); @@ -479,22 +422,15 @@ rule calculatePremium(env e){ │ ThirdParty not affected. │ │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule thirdPartyNotAffected(env e, method f, calldataarg args) filtered { - f -> f.selector != sig:transfer(address,uint256).selector && - f.selector != sig:transferFrom(address,address,uint256).selector - }{ +rule thirdPartyNotAffected(env e, method f, calldataarg args) +filtered { f -> f.selector != sig:transfer(address, uint256).selector && f.selector != sig:transferFrom(address, address, uint256).selector } { address thirdParty; - - require thirdParty != currentContract && thirdParty != e.msg.sender; - + require thirdParty != currentContract && thirdParty != e.msg.sender; uint256 thirdPartyBalanceBefore = underlying.balanceOf(thirdParty); uint256 thirdPartySharesBefore = balanceOf(thirdParty); - f(e, args); - uint256 thirdPartyBalanceAfter = underlying.balanceOf(thirdParty); uint256 thirdPartySharesAfter = balanceOf(thirdParty); - - assert (thirdPartyBalanceAfter == thirdPartyBalanceBefore); - assert (thirdPartySharesAfter == thirdPartySharesBefore); -} \ No newline at end of file + assert(thirdPartyBalanceAfter == thirdPartyBalanceBefore); + assert(thirdPartySharesAfter == thirdPartySharesBefore); +} diff --git a/DEFI/LiquidityPool/certora/specs/flashLoan_dispatcher.spec b/DEFI/LiquidityPool/certora/specs/flashLoan_dispatcher.spec index 9d88096c..4c00d983 100644 --- a/DEFI/LiquidityPool/certora/specs/flashLoan_dispatcher.spec +++ b/DEFI/LiquidityPool/certora/specs/flashLoan_dispatcher.spec @@ -23,25 +23,20 @@ using Asset as underlying; methods { - function balanceOf(address) external returns(uint256) envfree; - function underlying.balanceOf(address) external returns(uint256) envfree; - function _.executeOperation(uint256,uint256,address) external => DISPATCHER(true); + function balanceOf(address) external returns (uint256) envfree; + function underlying.balanceOf(address) external returns (uint256) envfree; + function _.executeOperation(uint256, uint256, address) external => DISPATCHER(true); } /// flash loans must increase the pool's underlying asset balance, assuming the /// receiver has no pool balance. -rule flashLoanIncreasesBalance { - address receiver; uint256 amount; env e; - +rule flashLoanIncreasesBalance() { + address receiver; + uint256 amount; + env e; require e.msg.sender != currentContract; - mathint balance_before = underlying.balanceOf(currentContract); - flashLoan(e, receiver, amount); - mathint balance_after = underlying.balanceOf(currentContract); - - assert balance_after >= balance_before, - "flash loans must not decrease the contract's underlying balance"; + assert balance_after >= balance_before, "flash loans must not decrease the contract's underlying balance"; } - diff --git a/DEFI/LiquidityPool/certora/specs/pool_havoc.spec b/DEFI/LiquidityPool/certora/specs/pool_havoc.spec index a1792d88..8b1a9232 100644 --- a/DEFI/LiquidityPool/certora/specs/pool_havoc.spec +++ b/DEFI/LiquidityPool/certora/specs/pool_havoc.spec @@ -9,33 +9,24 @@ /// See [the multi-contract section of the user guide](https://docs.certora.com/en/latest/docs/user-guide/multicontract/index.html) for a complete /// discussion of this example. -methods -{ - function balanceOf(address) external returns(uint256) envfree; - function totalSupply() external returns(uint256) envfree; - function transfer(address, uint256) external returns(bool); - function transferFrom(address, address, uint256) external returns(bool); - - function deposit(uint256) external returns(uint256); - function withdraw(uint256) external returns(uint256); - function assetBalance() external returns(uint256) envfree; - +methods { + function balanceOf(address) external returns (uint256) envfree; + function totalSupply() external returns (uint256) envfree; + function transfer(address, uint256) external returns (bool); + function transferFrom(address, address, uint256) external returns (bool); + function deposit(uint256) external returns (uint256); + function withdraw(uint256) external returns (uint256); + function assetBalance() external returns (uint256) envfree; function flashLoan(address, uint256) external; } /// `deposit` must increase the pool's underlying asset balance -rule integrityOfDeposit { - +rule integrityOfDeposit() { mathint balance_before = assetBalance(); - - env e; uint256 amount; + env e; + uint256 amount; require e.msg.sender != currentContract; - deposit(e, amount); - mathint balance_after = assetBalance(); - - assert balance_after == balance_before + amount, - "deposit must increase the underlying balance of the pool"; -} - + assert balance_after == balance_before + amount, "deposit must increase the underlying balance of the pool"; +} diff --git a/DEFI/LiquidityPool/certora/specs/pool_link.spec b/DEFI/LiquidityPool/certora/specs/pool_link.spec index 141618d6..7e26a6a4 100644 --- a/DEFI/LiquidityPool/certora/specs/pool_link.spec +++ b/DEFI/LiquidityPool/certora/specs/pool_link.spec @@ -13,34 +13,24 @@ using Asset as underlying; -methods -{ - function balanceOf(address) external returns(uint256) envfree; - function totalSupply() external returns(uint256) envfree; - function transfer(address, uint256) external returns(bool); - function transferFrom(address, address, uint256) external returns(bool); - - function deposit(uint256) external returns(uint256); - function withdraw(uint256) external returns(uint256); - +methods { + function balanceOf(address) external returns (uint256) envfree; + function totalSupply() external returns (uint256) envfree; + function transfer(address, uint256) external returns (bool); + function transferFrom(address, address, uint256) external returns (bool); + function deposit(uint256) external returns (uint256); + function withdraw(uint256) external returns (uint256); function flashLoan(address, uint256) external; - - function underlying.balanceOf(address) external returns(uint256) envfree; + function underlying.balanceOf(address) external returns (uint256) envfree; } /// `deposit` must increase the pool's underlying asset balance -rule integrityOfDeposit { - +rule integrityOfDeposit() { mathint balance_before = underlying.balanceOf(currentContract); - - env e; uint256 amount; + env e; + uint256 amount; require e.msg.sender != currentContract; - deposit(e, amount); - mathint balance_after = underlying.balanceOf(currentContract); - - assert balance_after == balance_before + amount, - "deposit must increase the underlying balance of the pool"; + assert balance_after == balance_before + amount, "deposit must increase the underlying balance of the pool"; } - diff --git a/DEFI/LiquidityPool/certora/specs/strong_inv.spec b/DEFI/LiquidityPool/certora/specs/strong_inv.spec index 3f916782..0ecf290c 100644 --- a/DEFI/LiquidityPool/certora/specs/strong_inv.spec +++ b/DEFI/LiquidityPool/certora/specs/strong_inv.spec @@ -1,23 +1,20 @@ using Asset as underlying; -methods -{ - function underlying.balanceOf(address) external returns(uint256) envfree; - function depositedAmount() external returns(uint256) envfree; +methods { + function underlying.balanceOf(address) external returns (uint256) envfree; + function depositedAmount() external returns (uint256) envfree; } -strong invariant strongDepositedAmountLessThanContractUnderlyingAsset() - depositedAmount() <= underlying.balanceOf(currentContract) - { - preserved with(env e) { +invariant strongDepositedAmountLessThanContractUnderlyingAsset() + depositedAmount() <= underlying.balanceOf(currentContract) { + preserved with (env e) { require e.msg.sender != currentContract; } } -weak invariant weakDepositedAmountLessThanContractUnderlyingAsset() - depositedAmount() <= underlying.balanceOf(currentContract) - { - preserved with(env e) { +invariant weakDepositedAmountLessThanContractUnderlyingAsset() + depositedAmount() <= underlying.balanceOf(currentContract) { + preserved with (env e) { require e.msg.sender != currentContract; } - } \ No newline at end of file + } diff --git a/FoundryIntegration/SimpleDappTest/certora/foundry.spec b/FoundryIntegration/SimpleDappTest/certora/foundry.spec index e826c461..e2382333 100644 --- a/FoundryIntegration/SimpleDappTest/certora/foundry.spec +++ b/FoundryIntegration/SimpleDappTest/certora/foundry.spec @@ -2,4 +2,4 @@ use builtin rule verifyFoundryFuzzTestsNoRevert; override function init_fuzz_tests(method f, env e) { reset_storage currentContract; -} \ No newline at end of file +} diff --git a/RealBugsFound/MakerDao/certora/specs/Vat.spec b/RealBugsFound/MakerDao/certora/specs/Vat.spec index 47452c4e..b05d5d9a 100644 --- a/RealBugsFound/MakerDao/certora/specs/Vat.spec +++ b/RealBugsFound/MakerDao/certora/specs/Vat.spec @@ -7,6 +7,7 @@ methods { // sumOfVaultDebtGhost gives the current sum over all debt assigned to a vault. ghost sumOfVaultDebtGhost() returns uint256 { + // Here we state that the sum is 0 before contructor. init_state axiom sumOfVaultDebtGhost() == 0; } @@ -27,8 +28,7 @@ hook Sload uint256 v currentContract.ilks[KEY bytes32 ilk].(offset 0) { // Updating ArtGhost in sync with sumOfVaultDebtGhost. hook Sstore currentContract.ilks[KEY bytes32 ilk].(offset 0) uint256 newArt (uint256 oldArt) { - havoc sumOfVaultDebtGhost assuming sumOfVaultDebtGhost@new() == sumOfVaultDebtGhost@old() + - (newArt * rateGhost[ilk]) - (oldArt * rateGhost[ilk]); + havoc sumOfVaultDebtGhost assuming sumOfVaultDebtGhost@new() == sumOfVaultDebtGhost@old() + (newArt * rateGhost[ilk]) - (oldArt * rateGhost[ilk]); ArtGhost[ilk] = newArt; } @@ -38,17 +38,15 @@ hook Sload uint256 v currentContract.ilks[KEY bytes32 ilk].(offset 32) { // Updating RateGhost in sync with sumOfVaultDebtGhost. hook Sstore currentContract.ilks[KEY bytes32 ilk].(offset 32) uint256 newRate (uint256 oldRate) { - havoc sumOfVaultDebtGhost assuming sumOfVaultDebtGhost@new() == - sumOfVaultDebtGhost@old() + (ArtGhost[ilk] * newRate) - (ArtGhost[ilk] * oldRate); + havoc sumOfVaultDebtGhost assuming sumOfVaultDebtGhost@new() == sumOfVaultDebtGhost@old() + (ArtGhost[ilk] * newRate) - (ArtGhost[ilk] * oldRate); rateGhost[ilk] = newRate; } - // DAI is backed by debt. Debt is either assigned to a Vault, meaning it is associated with a lien against some collateral asset, // or it is “unbacked” (also: “bad”), meaning it is the protocol’s (i.e., MKR holders’) responsibility. // This invariant states that these two sources of debt, when added, should equal the sum of all DAI balances. // vice is the total bad debt. // debt is the sum over all DAI balances. invariant fundamental_equation_of_dai() - debt() == vice() + sumOfVaultDebtGhost() - filtered { f -> !f.isFallback } + debt() == vice() + sumOfVaultDebtGhost() + filtered { f -> !f.isFallback }; diff --git a/RevertConditions/MsgValue/NonPayableRevert.spec b/RevertConditions/MsgValue/NonPayableRevert.spec index af128bd5..e788b7e2 100644 --- a/RevertConditions/MsgValue/NonPayableRevert.spec +++ b/RevertConditions/MsgValue/NonPayableRevert.spec @@ -2,16 +2,14 @@ methods { function justANonPayableFunction() external; } -rule NonPayableRevertingConditions { +rule NonPayableRevertingConditions() { env e; justANonPayableFunction@withrevert(e); - assert lastReverted <=> e.msg.value > 0; } -rule NonPayableRevertExample { +rule NonPayableRevertExample() { env e; justANonPayableFunction@withrevert(e); - assert !lastReverted; -} \ No newline at end of file +} diff --git a/RevertConditions/ReturnSize/ReturnSize.spec b/RevertConditions/ReturnSize/ReturnSize.spec index eee3e41a..661e5447 100644 --- a/RevertConditions/ReturnSize/ReturnSize.spec +++ b/RevertConditions/ReturnSize/ReturnSize.spec @@ -1,15 +1,12 @@ -methods{ +methods { function _.execute(uint) external => NONDET; } -rule returnSizeRevertConditions() -{ +rule returnSizeRevertConditions() { env e; address contract; uint x; - callerFunction@withrevert(e, contract, x); bool isReverted = lastReverted; - assert !isReverted <=> e.msg.value == 0; -} \ No newline at end of file +} diff --git a/RevertConditions/SafeMath/SafeMathReverts.spec b/RevertConditions/SafeMath/SafeMathReverts.spec index 4e071bb3..bfb232a4 100644 --- a/RevertConditions/SafeMath/SafeMathReverts.spec +++ b/RevertConditions/SafeMath/SafeMathReverts.spec @@ -5,32 +5,23 @@ methods { function value() external returns (uint256) envfree; } -rule increaseValueRevertingConditions { +rule increaseValueRevertingConditions() { uint256 amount; - uint256 valueBefore = value(); - increaseValue@withrevert(amount); - assert lastReverted <=> valueBefore + amount > max_uint256; } -rule decreaseValueRevertingConditions { +rule decreaseValueRevertingConditions() { uint256 amount; - uint256 valueBefore = value(); - decreaseValue@withrevert(amount); - - assert lastReverted <=> valueBefore - amount < 0; // (valueBefore - amount) is a mathint and can be negative. + assert lastReverted <=> valueBefore - amount < 0; // (valueBefore - amount) is a mathint and can be negative. } -rule divideValueRevertingConditions { +rule divideValueRevertingConditions() { uint256 divideBy; - uint256 valueBefore = value(); - divideValue@withrevert(divideBy); - assert lastReverted <=> divideBy == 0; } diff --git a/RevertConditions/String/StrIssueExample.spec b/RevertConditions/String/StrIssueExample.spec index 8186d3fe..986ae989 100644 --- a/RevertConditions/String/StrIssueExample.spec +++ b/RevertConditions/String/StrIssueExample.spec @@ -27,10 +27,9 @@ * (2) Bytes and String Layout in Storage: * https://docs.soliditylang.org/en/stable/internals/layout_in_storage.html#bytes-and-string */ - methods { - function arrayLength() external returns (uint256) envfree; - } - +methods { + function arrayLength() external returns (uint256) envfree; +} /// @title Verifies the `push` function reverts only if value is sent rule verifyPush(uint256 xx, string yy) { @@ -40,14 +39,10 @@ rule verifyPush(uint256 xx, string yy) { assert isReverted <=> (e.msg.value != 0); } - /// @title Verifies `getData` reverts only if value is sent or bad index rule verifyGetData(uint256 index) { env e; getData@withrevert(e, index); bool isReverted = lastReverted; - assert isReverted <=> ( - (e.msg.value != 0) || - (index >= arrayLength()) - ); + assert isReverted <=> ((e.msg.value != 0) || (index >= arrayLength())); } diff --git a/RevertConditions/String/StrIssueInvariant.spec b/RevertConditions/String/StrIssueInvariant.spec index 84ecd1c0..5ebdd5d0 100644 --- a/RevertConditions/String/StrIssueInvariant.spec +++ b/RevertConditions/String/StrIssueInvariant.spec @@ -4,21 +4,18 @@ * to storage. This invariant fails, because of the `dirty` function. */ - /// @title Checks that `encoded` is a valid encoding of the first 32 bytes of a string function isLegalEncoding(uint256 encoded) returns bool { - mathint doubleStrLen = (encoded % 256); // Double string length for short strings + mathint doubleStrLen = (encoded % 256); // Double string length for short strings bool isOdd = encoded % 2 == 1; return (encoded > 64 && isOdd) || (doubleStrLen <= 62 && !isOdd); } - /// @title Ghost updated by legality of string encoding is legal ghost bool isLegalStr { init_state axiom isLegalStr; } - /// @title Hook activated when the string in field `y` is written hook Sstore structArray[INDEX uint256 index].(offset 32) bytes32 str { uint256 encoded; @@ -26,7 +23,6 @@ hook Sstore structArray[INDEX uint256 index].(offset 32) bytes32 str { isLegalStr = isLegalStr && isLegalEncoding(encoded); } - /** @title All reads and writes to string `y` are legal * @notice This invariant is violated by the function `dirty`. * @notice In `solc` versions higher than 0.8.10 the Prover will have diff --git a/RevertConditions/String/StrIssuePersistent.spec b/RevertConditions/String/StrIssuePersistent.spec index 9fc56ab3..889d434a 100644 --- a/RevertConditions/String/StrIssuePersistent.spec +++ b/RevertConditions/String/StrIssuePersistent.spec @@ -11,19 +11,16 @@ * by reverts and we can use it in our revert condition rules. */ - /// @title Checks that `encoded` is a valid encoding of the first 32 bytes of a string function isLegalEncoding(uint256 encoded) returns bool { - mathint strLen = (encoded % 256) / 2; // The string length for short strings only + mathint strLen = (encoded % 256) / 2; // The string length for short strings only bool isOdd = encoded % 2 == 1; return (encoded > 64 && isOdd) || (strLen <= 31 && !isOdd); } - /// Persistent ghost denoting legality of string encoding persistent ghost bool legalStr; - /// @title Hook activated when the string in field `y` is read hook Sload bytes32 str structArray[INDEX uint256 index].(offset 32) { uint256 encoded; @@ -31,31 +28,25 @@ hook Sload bytes32 str structArray[INDEX uint256 index].(offset 32) { legalStr = isLegalEncoding(encoded) && legalStr; } - /// @title Checks when the `push` function reverts rule VerifyPush(uint256 xx, string yy) { + // When a revert occurs, `legalStr` will not revert because it is `persistent`. legalStr = true; - env e; - push@withrevert(e, xx, yy); bool isReverted = lastReverted; - + // Note that transferring funds to non-payable function can also cause revert. assert isReverted <=> (!legalStr || e.msg.value != 0); } - /// @title An example of reverting due to bad string rule VerifyGetDataExample(uint256 index) { legalStr = true; - env e; // This require prevents a revert unrelated to the string encoding require e.msg.value == 0; - getData@withrevert(e, index); - - satisfy !legalStr; // The example must have reverted + satisfy !legalStr; // The example must have reverted } diff --git a/RevertConditions/TargetCall/TargetCall.spec b/RevertConditions/TargetCall/TargetCall.spec index 00a1746d..29b0689e 100644 --- a/RevertConditions/TargetCall/TargetCall.spec +++ b/RevertConditions/TargetCall/TargetCall.spec @@ -1,10 +1,6 @@ - -rule targetCallRevertConditions() -{ +rule targetCallRevertConditions() { env e; - forward@withrevert(e); bool isReverted = lastReverted; - assert !isReverted <=> e.msg.value == 0; -} \ No newline at end of file +}