diff --git a/.gitignore b/.gitignore index cd4ab9e5..6f17da16 100644 --- a/.gitignore +++ b/.gitignore @@ -25,6 +25,11 @@ cache/ .certora* .last_confs certora_* +.zip-output-url.txt # mac .DS_Store + +# vim +.*.swp +.*.swo diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/.zip-output-url.txt b/01.Lesson_GettingStarted/ERC20Lesson1/.zip-output-url.txt deleted file mode 100644 index 25b653c4..00000000 --- a/01.Lesson_GettingStarted/ERC20Lesson1/.zip-output-url.txt +++ /dev/null @@ -1 +0,0 @@ -https://prover.certora.com/zipOutput/40726/341b96470a5e450b8e6d220baadbfca9?anonymousKey=d39cf7437cf90ebeab9da1b9143f4e992d6f1f8c diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec b/01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec index 5b2e5d91..63cf21c8 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec +++ b/01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec @@ -1,43 +1,45 @@ -/*** +/** * # ERC20 Example * - * This is an example specification for a generic ERC20 contract. - * To run, execute the following command in terminal/cmd: + * This is an example specification for a generic ERC20 contract. It contains several + * simple rules verifying the integrity of the transfer function. + * To run, execute the following command in terminal: + * + * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0 + * + * One of the rules here is badly phrased, and results in an erroneous fail. + * Understand the counter example provided by the Prover and then run the fixed + * spec: * - * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0 - * - * A simple rule that checks the integrity of the transfer function. - * - * Understand the counter example and then rerun: - * - * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0 + * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0 */ -methods { - // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree - balanceOf(address) returns(uint) envfree - allowance(address,address) returns(uint) envfree - totalSupply() returns(uint) envfree +// The methods block below gives various declarations regarding solidity methods. +methods +{ + // When a function is not using the environment (e.g., `msg.sender`), it can be + // declared as `envfree` + function balanceOf(address) external returns (uint) envfree; + function allowance(address,address) external returns(uint) envfree; + function totalSupply() external returns (uint) envfree; } -//// ## Part 1: Basic rules //////////////////////////////////////////////////// -/// Transfer must move `amount` tokens from the caller's account to `recipient` -rule transferSpec { - address recip; uint amount; +/// @title Transfer must move `amount` tokens from the caller's account to `recipient` +rule transferSpec(address recipient, uint amount) { env e; - address sender = e.msg.sender; - // mathint type that represents an integer of any size; - mathint balance_sender_before = balanceOf(sender); - mathint balance_recip_before = balanceOf(recip); + + // `mathint` is a type that represents an integer of any size + mathint balance_sender_before = balanceOf(e.msg.sender); + mathint balance_recip_before = balanceOf(recipient); - transfer(e, recip, amount); + transfer(e, recipient, amount); - mathint balance_sender_after = balanceOf(sender); - mathint balance_recip_after = balanceOf(recip); + mathint balance_sender_after = balanceOf(e.msg.sender); + mathint balance_recip_after = balanceOf(recipient); - // operations on mathints can never overflow or underflow. + // Operations on mathints can never overflow nor underflow assert balance_sender_after == balance_sender_before - amount, "transfer must decrease sender's balance by amount"; @@ -46,33 +48,39 @@ rule transferSpec { } -/// Transfer must revert if the sender's balance is too small -rule transferReverts { - env e; address recip; uint amount; +/// @title Transfer must revert if the sender's balance is too small +rule transferReverts(address recipient, uint amount) { + env e; require balanceOf(e.msg.sender) < amount; - transfer@withrevert(e, recip, amount); + transfer@withrevert(e, recipient, amount); assert lastReverted, - "transfer(recip,amount) must revert if sender's balance is less than `amount`"; + "transfer(recipient,amount) must revert if sender's balance is less than `amount`"; } -/// Transfer must not revert unless -/// the sender doesn't have enough funds, -/// or the message value is nonzero, -/// or the recipient's balance would overflow, -/// or the message sender is 0, -/// or the recipient is 0 -/// -/// @title Transfer doesn't revert -rule transferDoesntRevert { - env e; address recipient; uint amount; +/** @title Transfer must not revert unless + * - the sender doesn't have enough funds, + * - or the message value is nonzero, + * - or the recipient's balance would overflow, + * - or the message sender is 0, + * - or the recipient is 0 + */ +rule transferDoesntRevert(address recipient, uint amount) { + env e; require balanceOf(e.msg.sender) > amount; - require e.msg.value == 0; - require balanceOf(recipient) + amount < max_uint; + require e.msg.value == 0; // No payment + + // This requirement prevents overflow of recipient's balance. + // We convert `max_uint` to type `mathint` since: + // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`, + // 2. `mathint` can only be compared to another `mathint` + require balanceOf(recipient) + amount < to_mathint(max_uint); + + // Recall that `address(0)` is a special address that in general should not be used require e.msg.sender != 0; require recipient != 0; diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec b/01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec index db1524c9..ab987fcb 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec +++ b/01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec @@ -1,81 +1,86 @@ -/*** - * # ERC20 Example +/** + * # Fixed ERC20 Example * - * This is an example specification for a generic ERC20 contract. - * To run, execute the following command in terminal/cmd: + * This is the fixed version of ERC20.spec. Note the changes in rule `transferSpec`. + * Run using: * - * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0 + * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0 * - * A simple rule that checks the integrity of the transfer function. - * - * Understand the counter example and then rerun: - * - * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0 + * There should be no errors. */ -methods { - // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree - balanceOf(address) returns(uint) envfree - allowance(address,address) returns(uint) envfree - totalSupply() returns(uint) envfree +// The methods block below gives various declarations regarding solidity methods. +methods +{ + // When a function is not using the environment (e.g., `msg.sender`), it can be + // declared as `envfree` + function balanceOf(address) external returns (uint) envfree; + function allowance(address,address) external returns(uint) envfree; + function totalSupply() external returns (uint) envfree; } -//// ## Part 1: Basic rules //////////////////////////////////////////////////// -/// Transfer must move `amount` tokens from the caller's account to `recipient` -rule transferSpec { - address recip; uint256 amount; +/// @title Transfer must move `amount` tokens from the caller's account to `recipient` +rule transferSpec(address recipient, uint amount) { env e; - address sender = e.msg.sender; - // mathint type that represents an integer of any size; - mathint balance_sender_before = balanceOf(sender); - mathint balance_recip_before = balanceOf(recip); + + // `mathint` is a type that represents an integer of any size + mathint balance_sender_before = balanceOf(e.msg.sender); + mathint balance_recip_before = balanceOf(recipient); - transfer(e, recip, amount); + transfer(e, recipient, amount); - mathint balance_sender_after = balanceOf(sender); - mathint balance_recip_after = balanceOf(recip); + mathint balance_sender_after = balanceOf(e.msg.sender); + mathint balance_recip_after = balanceOf(recipient); - // operations on mathints can never overflow or underflow. - assert recip != sender => balance_sender_after == balance_sender_before - amount, + address sender = e.msg.sender; // A convenient alias + + // Operations on mathints can never overflow or underflow. + assert recipient != sender => balance_sender_after == balance_sender_before - amount, "transfer must decrease sender's balance by amount"; - assert recip != sender => balance_recip_after == balance_recip_before + amount, + assert recipient != sender => balance_recip_after == balance_recip_before + amount, "transfer must increase recipient's balance by amount"; - assert recip == sender => balance_sender_after == balance_sender_before, + assert recipient == sender => balance_sender_after == balance_sender_before, "transfer must not change sender's balancer when transferring to self"; } -/// Transfer must revert if the sender's balance is too small -rule transferReverts { - env e; address recip; uint amount; +/// @title Transfer must revert if the sender's balance is too small +rule transferReverts(address recipient, uint amount) { + env e; require balanceOf(e.msg.sender) < amount; - transfer@withrevert(e, recip, amount); + transfer@withrevert(e, recipient, amount); assert lastReverted, - "transfer(recip,amount) must revert if sender's balance is less than `amount`"; + "transfer(recipient,amount) must revert if sender's balance is less than `amount`"; } -/// Transfer must not revert unless -/// the sender doesn't have enough funds, -/// or the message value is nonzero, -/// or the recipient's balance would overflow, -/// or the message sender is 0, -/// or the recipient is 0 -/// -/// @title Transfer doesn't revert -rule transferDoesntRevert { - env e; address recipient; uint amount; +/** @title Transfer must not revert unless + * - the sender doesn't have enough funds, + * - or the message value is nonzero, + * - or the recipient's balance would overflow, + * - or the message sender is 0, + * - or the recipient is 0 + */ +rule transferDoesntRevert(address recipient, uint amount) { + env e; require balanceOf(e.msg.sender) > amount; - require e.msg.value == 0; - require balanceOf(recipient) + amount < max_uint; + require e.msg.value == 0; // No payment + + // This requirement prevents overflow of recipient's balance. + // We convert `max_uint` to type `mathint` since: + // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`, + // 2. `mathint` can only be compared to another `mathint` + require balanceOf(recipient) + amount < to_mathint(max_uint); + + // Recall that `address(0)` is a special address that in general should not be used require e.msg.sender != 0; require recipient != 0; diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec b/01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec index 57fa40f7..d663758d 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec +++ b/01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec @@ -1,41 +1,53 @@ -/*** - * # ERC20 Example +/** + * # ERC20 Parametric Example * - * This is an example specification for a generic ERC20 contract. - * - * To simulate the execution of all functions in the main contract, - * you can define a method argument in the rule and use it in a statement. - * Run: - * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "parametric rule" + * Another example specification for an ERC20 contract. This one using a parametric rule, + * which is a rule that encompasses all the methods in the current contract. It is called + * parametric since one of the rule's parameters is the current contract method. + * To run enter: * + * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule" + * + * The `onlyHolderCanChangeAllowance` fails for one of the methods. Look at the Prover + * results and understand the counter example - which discovers a weakness in the + * current contract. */ -methods { - // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree - balanceOf(address) returns(uint) envfree - allowance(address,address) returns(uint) envfree - totalSupply() returns(uint) envfree +// The methods block below gives various declarations regarding solidity methods. +methods +{ + // When a function is not using the environment (e.g., `msg.sender`), it can be + // declared as `envfree` + function balanceOf(address) external returns (uint) envfree; + function allowance(address,address) external returns(uint) envfree; + function totalSupply() external returns (uint) envfree; } -//// ## Part 2: parametric rules /////////////////////////////////////////////// - -/// If `approve` changes a holder's allowance, then it was called by the holder -rule onlyHolderCanChangeAllowance { - address holder; address spender; +/// @title If `approve` changes a holder's allowance, then it was called by the holder +rule onlyHolderCanChangeAllowance(address holder, address spender, method f) { + // The allowance before the method was called mathint allowance_before = allowance(holder, spender); - method f; env e; calldataarg args; + env e; + calldataarg args; // Arguments for the method f f(e, args); + // The allowance after the method was called 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 == approve(address,uint).selector || f.selector == increaseAllowance(address,uint).selector), - "only approve and increaseAllowance can increase allowances"; + "only the sender can change its own allowance"; + + // Assert that if the allowance changed then `approve` or `increaseAllowance` was called. + 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"; } diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/TotalGreaterThanUser.spec b/01.Lesson_GettingStarted/ERC20Lesson1/TotalGreaterThanUser.spec index c3bca467..8ac75aca 100644 --- a/01.Lesson_GettingStarted/ERC20Lesson1/TotalGreaterThanUser.spec +++ b/01.Lesson_GettingStarted/ERC20Lesson1/TotalGreaterThanUser.spec @@ -1,33 +1,40 @@ /** - Specification file for Certora Prover + * # Total Supply Over-Approximation Example + * + * The rules here are intended to verify that an ERC20's `totalSupply` method follows + * the basic property: + * For and `address user` we have `totalSupply() >= balanceOf(user)`. + * + * First run only the rule `totalSupplyAfterMint`: + * + * certoraRun ERC20.sol --verify ERC20:TotalGreaterThanUser.spec --solc --rule totalSupplyAfterMint + * + * This rule will fail due to the Prover's tendency to over-approximate the states. + * Now run the fixed rule `totalSupplyAfterMintWithPrecondition`: + * + * certoraRun ERC20.sol --verify ERC20:TotalGreaterThanUser.spec --solc --rule totalSupplyAfterMintWithPrecondition + * + * Do you understand why the second rule passed? + */ - - First run only the rule totalSupplyAfterDeposit on the ERC20 contract: - certoraRun ERC20.sol --verify ERC20:TotalGreaterThanUser.spec --solc solc8.0 --rule totalSupplyAfterMint - - This rule shows that when the initial state the totalSupply was smaller than the user's balance, there is a violation. - - By adding a precondition we can verify this rule. - run: - - certoraRun ERC20.sol --verify ERC20:TotalGreaterThanUser.spec --solc solc8.0 --rule totalSupplyAfterMintWithPrecondition - -**/ - -methods { - // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree - balanceOf(address) returns(uint) envfree - allowance(address,address) returns(uint) envfree - totalSupply() returns(uint) envfree +// The methods block below gives various declarations regarding solidity methods. +methods +{ + // When a function is not using the environment (e.g., `msg.sender`), it can be + // declared as `envfree` + function balanceOf(address) external returns (uint) envfree; + function allowance(address,address) external returns(uint) envfree; + function totalSupply() external returns (uint) envfree; } + +/// @title Total supply after mint is at least the balance of the receiving account rule totalSupplyAfterMint(address account, uint256 amount) { env e; - // Additional variables to aid in understanding violation: - - // uint256 userBalanceBefore = balanceOf(account); - // uint256 totalBefore = totalSupply(); + // Additional variables can aid in understanding violation, like the two below: + uint256 userBalanceBefore = balanceOf(account); + uint256 totalBefore = totalSupply(); mint(e, account, amount); @@ -35,18 +42,21 @@ rule totalSupplyAfterMint(address account, uint256 amount) { uint256 totalAfter = totalSupply(); // Verify that the total supply of the system is at least the current balance of the account. - assert ( totalAfter >= userBalanceAfter, "Total supply are less than a user's balance " ); + assert totalAfter >= userBalanceAfter, "total supply is less than a user's balance"; } - +/** @title Total supply after mint is at least the balance of the receiving account, with + * precondition. + */ rule totalSupplyAfterMintWithPrecondition(address account, uint256 amount) { env e; uint256 userBalanceBefore = balanceOf(account); uint256 totalBefore = totalSupply(); - // Assume that in the current state before calling mint, the total supply of the system is at least the user balance. + // Assume that in the current state before calling mint, the total supply of the + // system is at least the user balance. require totalBefore >= userBalanceBefore; mint(e, account, amount); @@ -55,6 +65,6 @@ rule totalSupplyAfterMintWithPrecondition(address account, uint256 amount) { uint256 totalAfter = totalSupply(); // Verify that the total supply of the system is at least the current balance of the account. - assert ( totalAfter >= userBalanceAfter, "Total supply are less than a user's balance " ); + assert totalAfter >= userBalanceAfter, "total supply is less than a user's balance "; } diff --git a/01.Lesson_GettingStarted/ERC20Lesson1/resource_errors.json b/01.Lesson_GettingStarted/ERC20Lesson1/resource_errors.json deleted file mode 100644 index d9bd7923..00000000 --- a/01.Lesson_GettingStarted/ERC20Lesson1/resource_errors.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "topics": [] -} \ No newline at end of file diff --git a/01.Lesson_GettingStarted/README.md b/01.Lesson_GettingStarted/README.md index dfc369fc..794f7aaa 100644 --- a/01.Lesson_GettingStarted/README.md +++ b/01.Lesson_GettingStarted/README.md @@ -46,7 +46,7 @@ Clone your repository to your local machine so you'll have everything you need o
-> :information_source: The Certora team's recommends using VSCode as your main editor for writing specifications and browsing through contracts during the course. As part of the everyday work, you'll need convenient access to terminal, .spec editor - preferably with SLP extension, and a solidity editor - preferably with extension that has adequate support for reading and writing solidity code. +> :information_source: The Certora team recommends using VSCode as your main editor for writing specifications and browsing through contracts during the course. As part of the everyday work, you'll need convenient access to terminal, .spec editor - preferably with SLP extension, and a solidity editor - preferably with extension that has adequate support for reading and writing solidity code. You may, however, choose to work with any other (textual) editor of your choice or split the work between several editors, just know that the SLP is currently only supported through VSCode.
@@ -61,22 +61,47 @@ You may, however, choose to work with any other (textual) editor of your choice --- -## Running Scripts +## Running the Prover Using Configuration Files
-Writing the `certoraRun` command in a terminal every time we want to execute a run can be tiresome and uneasy on the eyes. Moreover, since a typical run of a single rule in real-life systems takes minutes to finish, we often work on 2 rules in parallel. +For larger projects, the command line for running the Certora Prover can become large +and cumbersome. It is therefore recommended to use _configuration files_ instead. +These are [JSON5](https://json5.org/) files (with ".conf" extension) that hold the +parameters and options for the Certora Prover. Here is an example conf file: -For that reason, we often write a shell script of the run command that includes all the settings and options we need for a run. There are 4 advantages for using a script: +```json5 +{ + "files": [ + "src/contracts/Strategy.sol", + "src/contracts/Data.sol", + ], + "verify": "Strategy:certora/specs/StrategyVrification.spec", + "send_only": false, + "optimistic_loop": true, + "loop_iter": "2", + "rule_sanity": "basic", + // Note: json5 supports comments! + "solc": "solc8.8", + "msg": "Strategy verification" +} +``` + +Now running the Certora Prover is simply entering +```bash +certoraRun config_file.conf +``` + +There are other reasons to prefer configuration files over directly using CLI: +1. They are easier to read and sometimes can be more friendly to edit. +2. Since the configuration files are [JSON5](https://json5.org/), they support comments. +3. We can include them in our git repository for version control. -1. It is easier to read and sometimes can be more friendly to edit. -2. It can save a large chunk of code that's stored in a known place, as opposed to a terminal command that can be pushed down the stack and disappear after intense use of the terminal. -3. It can be uploaded to git or sent along with the specifications for others to use, instead of forcing them to write the command -4. It allows a more advanced execution of run commands, e.g. running the exact same rule on every contract in a given directory (we will talk about sanity rule in the future).
-- [ ] Follow the instructions on [RunScriptExample](RunScriptExample) to learn how to write run scripts, and how to execute the prover using scripts. +- [ ] Follow the instructions on [RunConfExample](RunConfExample) to learn how to + execute the prover using configuration files.
diff --git a/01.Lesson_GettingStarted/RunScriptExample/README.md b/01.Lesson_GettingStarted/RunConfExample/README.md similarity index 57% rename from 01.Lesson_GettingStarted/RunScriptExample/README.md rename to 01.Lesson_GettingStarted/RunConfExample/README.md index de560a5e..9baf23a1 100644 --- a/01.Lesson_GettingStarted/RunScriptExample/README.md +++ b/01.Lesson_GettingStarted/RunConfExample/README.md @@ -1,12 +1,12 @@ -# Learn How To Run The Prover Using A Script +# Learn How To Run The Prover Using A configuration file -
+## Using command line Let's recap the basic structure of the `certoraRun` command: - It starts with the command `certoraRun`. -- Right after we specify the relative path to the solidity file that holds the contract we'd like to verify - ``. +- Right after we specify the relative path to the solidity file that holds the contract we'd like to verify - `` (meaning relative to the current working directory). - Next, we write the contract we desire to verify, separated from the solidity file path by full colon - `:`. We do it since a single solidity file can contain multiple contracts. @@ -16,17 +16,23 @@ Let's recap the basic structure of the `certoraRun` command: - After we specify the contract we'd like to verify again, we need to specify the `spec` file according to which we want to verify the contract - `` -At the end the run command should look something like that: +At the end the run command should look something like that (assuming our current working directory +is `01.Lesson_GettingStarted/`): ```CVL certoraRun ERC20Lesson1/ERC20.sol:ERC20 --verify ERC20:ERC20Lesson1/Parametric.spec ``` -
+## Using a configuration file + +- [ ] Open the config file [verifyERC20](verifyERC20.conf) and read it. The format used is + [JSON5](https://json5.org/). Make sure that you understand all fields and the + data they require. -- [ ] Open the shell script [verifyERC20](verifyERC20.sh) and read it. Make sure that you understand each line, and that you are familiar with every flag. +- [ ] In general, to use a config file, simply enter: `certoraRun ` - - [ ] Do you recognize this run command? This is the last run in ERC20Lesson1. +> :bulb: If using relative paths in the config file, they should be relative to the + current working directory where you enter `certoraRun`.
@@ -34,10 +40,11 @@ certoraRun ERC20Lesson1/ERC20.sol:ERC20 --verify ERC20:ERC20Lesson1/Parametric.s
-- [ ] In your VSCode terminal change directory to `01.Lesson_GettingStarted`, and execute the script: +- [ ] In your VSCode terminal change directory to `01.Lesson_GettingStarted/ERC20Lesson1/`, + and execute the command -``` sh -sh RunScriptExample/verifyERC20.sh "This is a run executed through a shell script" +```bash +certoraRun ../RunConfExample/verifyERC20.conf ``` > :memo: You can check the verification report to see that it really is the same run. @@ -54,12 +61,14 @@ sh RunScriptExample/verifyERC20.sh "This is a run executed through a shell scri
-- [ ] Create a script that runs the entire `TotalGreaterThanUser.spec` specification file with solidity compiler 8.0 and a message string "My first Certora shell script". Save the script in `RunScriptExample` with the name "myOwnVerificationScript1" and execute the script. +- [ ] Create a config that runs the entire `TotalGreaterThanUser.spec` specification file with solidity compiler 8.0 and a message string "My first Certora conf". + Save the config in `RunConfExample` folder with the name `myOwnVerificationConf.conf` and run it.
-- [ ] Change the contract name from ERC20 to NewERC20 (without changing the file name) and create a script that runs `TotalGreaterThanUser.spec` specification file with solidity compiler 8.0 and a message of your choice taken as an input. Save the script in `RunScriptExample` with the name "myOwnVerificationScript2" and execute the script. +- [ ] Change the contract name from ERC20 to NewERC20 (without changing the file name) and create a config that runs `TotalGreaterThanUser.spec` specification file with solidity compiler 8.0. + Modify the previously created config file accordingly and verify that it still runs.
- > :bulb: If you were checking the call trace in each of the runs you made, you may have noticed that the counter examples supplied by the prover are distinct in each run. + > :bulb: If you were checking the call trace in each of the runs you made, you may have noticed that the counter examples supplied by the Prover are distinct in each run. diff --git a/01.Lesson_GettingStarted/RunConfExample/verifyERC20.conf b/01.Lesson_GettingStarted/RunConfExample/verifyERC20.conf new file mode 100644 index 00000000..592a706a --- /dev/null +++ b/01.Lesson_GettingStarted/RunConfExample/verifyERC20.conf @@ -0,0 +1,27 @@ +// Note. All paths are relative to the current working directory from which you invoke the +// `certoraRun` command. In the example below it is assumed your current working directory +// is: 01.Lesson_GettingStarted/ERC20Lesson1 +// To run, enter: +// certoraRun ../RunConfExample/verifyERC20.conf +{ + // "files" - a list of solidity files for the Prover to read. Place here the path + // to the current contracts, and any other needed conract. + "files": [ + "ERC20.sol" + ], + + // "verify" - a string of the form ":" + "verify": "ERC20:Parametric.spec", + + // "solc" - the sSolidity compiler to use + "solc": "solc8.0", + + // "rule" - a list of rule names to verify, if omitted all rules in the spec will be + // tested + "rule": [ + "onlyHolderCanChangeAllowance" + ], + + // "msg" - a message to display in the Prover's output web pages + "msg": "Parametric rule - allowance change verification" +} diff --git a/01.Lesson_GettingStarted/RunScriptExample/verifyERC20.sh b/01.Lesson_GettingStarted/RunScriptExample/verifyERC20.sh deleted file mode 100755 index 3f61c868..00000000 --- a/01.Lesson_GettingStarted/RunScriptExample/verifyERC20.sh +++ /dev/null @@ -1,12 +0,0 @@ -# format: : --verify : - -certoraRun ERC20Lesson1/ERC20.sol:ERC20 --verify ERC20:ERC20Lesson1/Parametric.spec \ - --solc solc8.0 \ - --rule onlyHolderCanChangeAllowance \ - --msg "$1" - -# At the end of each line a backsalsh (\) is used for line continuation - to split overly long lines. -# more on backslash before new line here: https://superuser.com/questions/794963/in-a-linux-shell-why-does-backslash-newline-not-introduce-whitespace#:~:text=The%20Backslash%2Dnewline%20is%20used,purposes%20of%20executing%20the%20script. - -# The $1 is the first argument given to the script, so we can change the msg of a run without changing the actual script -# more on $1 here: https://bash.cyberciti.biz/guide/$1 \ No newline at end of file