### Setup Virtual Environment for Beta Version

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Instructions for setting up a Python virtual environment to manage and switch between beta and production versions of the Certora Prover CLI.

```shell
pipinstallvirtualenv
virtualenvcertora-beta
sourcecertora-beta/bin/activate
pip3installcertora-cli-beta
```

--------------------------------

### Example Foundry setUp() with Contract Instantiation

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_foundry-integration.html.md

Illustrates a typical Foundry test contract's setUp() function where a new instance of another contract is created. This pattern requires specific configuration in the Certora Prover's .conf file for proper verification.

```solidity
contract TestContract is Test {
  MyContract myContract;
  function setUp() external {
    myContract = new MyContract();
  }
  ...
}
```

--------------------------------

### Install Certora Prover Beta Version

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Commands to uninstall the stable version and install the beta version of the Certora Prover CLI. It is not recommended to have both installed simultaneously.

```shell
pipuninstallcertora-cli
pipinstallcertora-cli-beta
```

--------------------------------

### Install Certora Prover CLI

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Installs the Certora Prover command-line interface package using pip. It is recommended to use a Python virtual environment.

```shell
pip3installcertora-cli
```

--------------------------------

### Get Help for Certora Runner

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_erc20_example.html.md

This command displays the help message for the `certoraRun` tool, providing information about its syntax, available options, and usage. It's a valuable command for understanding the full capabilities of the Prover's command-line interface.

```bash
certoraRun --help
```

--------------------------------

### Certora Prover Configuration File Example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_multicontract_index.html.md

An example of a Certora Prover configuration file (`.conf`) used to run verification specifically on the `Pool` contract without providing the source code for the `Asset` contract. This setup is intended to demonstrate the handling of unresolved method calls.

```bash
$certoraRun JustPool.conf
```

--------------------------------

### Setup Virtual Environment for Certora Soroban Prover

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_sunbeam_troubleshooting.html.md

This snippet demonstrates how to set up and activate a Python virtual environment (venv) to resolve issues with running the `certoraSorobanProver`. It includes commands to create the venv, activate it, and install project dependencies.

```shell
cd projectDir
python3 -m venv .venv
source .venv/bin/activate
pip3 install -r requirements.txt
certoraSorobanProver path/to/prover_config.conf
```

--------------------------------

### Clone Certora Tutorials Repository

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_tutorials.html.md

This command clones the Certora tutorials repository to allow users to work through guided lessons and exercises for the Certora Prover. It is essential for hands-on learning of installation and basic usage.

```git
git clone https://github.com/Certora/tutorials-code
```

--------------------------------

### List Hidden Files (Bash)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

This command lists all files and directories in the current directory, including hidden ones (those starting with a dot). It's used to verify the creation of files like `.zshenv` or `.profile`.

```bash
ls -a
```

--------------------------------

### Example Certora Equivalence Check Command

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_equiv-check_index.html.md

An example demonstrating the `certoraEqCheck` command for a specific test case. It points to a configuration file and the functions to be compared.

```shell
certoraEqCheck conf Test/EqCheck/testGood.conf BasicMathGood:add BasicMathBad:add_mult
```

--------------------------------

### Install and Use Solidity Compiler with solc-select

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install_evm_compiler.html.md

This snippet demonstrates how to install and manage different versions of the Solidity compiler using the `solc-select` tool. It covers installation, downloading specific versions, and setting the active version for use.

```shell
pip install solc-select
solc-select install 0.8.0
solc-select use 0.8.0
```

--------------------------------

### Install Rosetta on MacOS

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_erc20_example.html.md

This command is used on MacOS systems to install Rosetta, a software translation process that allows applications built for Intel processors to run on Apple silicon Macs. This is a prerequisite if you encounter a 'Bad CPU type in executable' error when running certain commands.

```bash
softwareupdate --install-rosetta
```

--------------------------------

### Clone Certora Examples Repository

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_tutorials.html.md

This command clones the Certora examples repository, which contains various examples of the Certora Verification Language (CVL). These examples are useful for understanding different specification patterns and functionalities.

```git
git clone https://github.com/Certora/Examples
```

--------------------------------

### Test Certora Platform Tools Installation

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_solana_installation.html.md

Verifies the installation of Certora Platform Tools by using the `certora-sbf` command to download and install the necessary tools without initiating a build process. This confirms that the tools can be accessed and managed correctly.

```shell
cargo certora-sbf --no-build
```

--------------------------------

### Check Python Version

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Command to check the installed Python 3 version. Ensure it is 3.8.16 or newer for compatibility.

```shell
python3--version
```

--------------------------------

### Edit .profile for Permanent Key (Bash)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

This command opens the `.profile` file in the `nano` text editor, enabling users to add the `export CERTORAKEY` command for persistent environment variable setting on Linux. Changes are saved upon exiting nano.

```bash
nano .profile
```

--------------------------------

### Certora Prover Configuration File Example (JSON5)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_config_files.html.md

An example of a Certora Prover configuration file written in JSON5 format. This file specifies the Solidity files to analyze, the verification target, and other Prover options. JSON5 supports comments, making configuration more readable.

```json5
{
"files":[
"ERC20.sol"
],
"verify":"ERC20:ERC20.spec",
"wait_for_results":"all",
"rule_sanity":"basic",
// Note: json5 supports comments!
"msg":"First run using .conf file"
}
```

--------------------------------

### Simple For Loop Unrolling Example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_gaps.html.md

Demonstrates a basic for loop in Solidity-like syntax that the Certora Prover can automatically infer the number of iterations for.

```solidity
uintx;
for(uinti=0;i<3;i++){
x++;
}
```

--------------------------------

### Install Gambit using Cargo

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Installs Gambit globally using the Cargo package manager. Assumes the Gambit repository has been cloned. Installs Gambit to a globally visible location on your PATH.

```bash
cargo install --path .
```

--------------------------------

### Add Python Path on Linux

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Steps to add a specified directory to the user's PATH on Linux by modifying the .profile file.

```shell
cd~
nano.profile
PATH="$PATH:/specified/path/in/warning"
source.profile
```

--------------------------------

### Run Certora Prover Command

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_erc20_example.html.md

This command initiates the Certora Prover to verify the ERC20 contract using a fixed specification. It specifies the output file and the contract to verify.

```shell
certoraRunERC20.sol--verifyERC20:ERC20Fixed.spec--solcsolc8.0
```

--------------------------------

### Method Summarization Syntax Example in Certora Prover

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_approx_summarization.html.md

This example demonstrates the syntax for method summarization in the Certora Prover. Method summarization allows users to provide a high-level description of a method's behavior to aid solvers in reasoning and prevent timeouts. This specific example illustrates summarization for a complex function.

```CVL
/**
 * Summarizes the behavior of the `complexFunction`.
 * This is a placeholder and should be replaced with actual CVL code.
 */
def complexFunction(a: int, b: int) returns int {
  // TODO: Provide a concise, high-level description of the behavior
  // For example, specify post-conditions or invariants.
  // Example:
  // ensure ret >= 0;
  // assume a > 0;
  return a + b;
}
```

--------------------------------

### Create/Edit .zshenv for Permanent Key (Bash)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

This command opens the `.zshenv` file in the `nano` text editor, allowing the user to add the `export CERTORAKEY` command for persistent environment variable setting on macOS. The changes are saved by exiting nano.

```bash
nano .zshenv
```

--------------------------------

### Install Certora Prover CLI

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Installs the Certora Prover command-line interface using pip. It is recommended to use a Python virtual environment for package installations.

```bash
pip3 install certora-cli-beta
```

--------------------------------

### Navigate to Home Directory (Bash)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

This command changes the current directory to the user's home directory. It's a standard shell command used in preparation for creating or modifying configuration files in the home directory on Unix-like systems.

```bash
cd ~
```

--------------------------------

### Rule for Possible Full Withdrawal - Certora CVL

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_satisfy.html.md

This Certora CVL rule demonstrates how to produce a positive example showing a full withdrawal of assets from a pool. It uses `satisfy` statements to guide the Prover. The rule requires the amount to be greater than zero to ensure a meaningful example.

```CVL
rule possibleToFullyWithdraw(address sender, uint256 amount) {
  env eT0;
  env eM;
  setup(eM);
  address token;
  require token == _token0 || token == _token1;
  uint256 balanceBefore = token.balanceOf(eT0, sender);
  require eM.msg.sender == sender;
  require eT0.msg.sender == sender;
  require amount > 0;
  token.transfer(eT0, currentContract, amount);
  uint256 amountOut0 = mint(eM, sender);
  // immediately withdraw 
  burnSingle(eM, _token0, amountOut0, sender);
  satisfy(balanceBefore == token.balanceOf(eT0, sender));
}
```

--------------------------------

### Install certora-cli for Mutation Verifier

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_gambit_mutation-verifier.html.md

Installs the Certora Prover command-line interface tool, which is required to run the mutation verifier. It also provides instructions on how to upgrade the tool if it's already installed and the `certoraMutate` command is missing.

```shell
pip install certora-cli
```

```shell
pip install --upgrade certora-cli
```

--------------------------------

### Check Java Version

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Command to check the installed Java Development Kit (JDK) version. Requires JDK 11 or newer.

```shell
java-version
```

--------------------------------

### Install Rust using Official Script

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_solana_installation.html.md

Installs the Rust programming language and its associated build tools using the official installation script. This is a prerequisite for many Rust-based development tools, including the Certora Prover.

```shell
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
```

--------------------------------

### Add Python Path on macOS

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Steps to add a specified directory to the system's PATH on macOS to resolve warnings about scripts not being found.

```shell
cd/etc/paths.d
sudonanoPythonForProver
/specified/path/in/warning
echo$PATH
```

--------------------------------

### Example Usage: Certora Verification with Dynamic Contract Creation

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

This example demonstrates how to run Certora verification for contracts C and Foo, enabling dynamic contract creation with a bound of 1 and automatic dispatcher summaries. It combines the --dynamic_bound and --dynamic_dispatch options for comprehensive contract creation modeling.

```cli
certoraRunC.solFoo.sol--verifyC:C.spec--dynamic_bound1--dynamic_dispatch
```

--------------------------------

### Configure Contract Linking for Foundry setUp() in Certora Prover

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_foundry-integration.html.md

Demonstrates how to configure the Certora Prover's .conf file to link contract instances created within Foundry's setUp() function. This ensures the Prover can correctly resolve calls to these instances during verification.

```json
{
  "files": [
    "...",
    "path/to/MyContract.sol"
  ],
  "link": [
    "...",
    "TestContract:myContract=MyContract"
  ]
}
```

--------------------------------

### Retrieve Zipped Job Output URL (Example)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_portal_secrets.html.md

This example demonstrates how to construct the URL to download zipped job input and output files. It replaces the standard 'output' endpoint with 'zipOutput'. Ensure you are logged in with appropriate authorization to avoid 'Forbidden' errors.

```url
https://vaas-stg.certora.com/zipOutput/65540/270dce9623d492937d82/?anonymousKey=6edb93d7abae7871f1c3be3b10863d64d2d72fef
```

--------------------------------

### Apply Environment Variable Changes (Linux Bash)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

This command sources the `.profile` script, applying any defined environment variables, including the Certora access key, to the current Linux shell session. This ensures the variable is recognized without needing to restart the terminal.

```bash
source .profile
```

--------------------------------

### Install 'just' build tool

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Installs the 'just' command-line build tool using Cargo, Rust's package manager. 'just' is often used for automating development tasks and managing project workflows.

```shell
cargo install just

```

--------------------------------

### CVL Example: Simple Function Summary

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_methods.html.md

This example demonstrates a basic summary declaration in CVL. The `=> ALWAYS(0)` part replaces calls to the function `f` with a constant value of 0, simplifying verification.

```solidity
functionf(uint)externalreturns(uint)=>ALWAYS(0);
```

--------------------------------

### CVL Example: Expression Function Summary

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_methods.html.md

This example shows how to use an expression summary in CVL. It replaces calls to function `f` with a call to a CVL function `cvl_function`, passing the original argument `x`. This allows for more complex replacements than simple constant values.

```solidity
functionf(uintx)externalreturns(uint)=>cvl_function(x);
```

--------------------------------

### Install Specific Rust Toolchains

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_solana_installation.html.md

Installs specific versions of the Rust toolchain required for Certora Prover operations. This ensures compatibility with the necessary Rust compiler versions for building and running Certora tools.

```shell
rustup toolchain install 1.79
rustup toolchain install 1.75
rustup toolchain install 1.81
```

--------------------------------

### Gambit Run with JSON Configuration

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

This example demonstrates how to run Gambit using a JSON configuration file. The command specifies the JSON file, which contains various Gambit arguments and configurations, including filename, sourceroot, and solc_remappings.

```shell
gambit mutate --json benchmarks/config-jsons/test1.json
```

--------------------------------

### Install Certora Solana SBF Tool

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_solana_installation.html.md

Installs the `cargo-certora-sbf` subcommand, which is part of the Certora Platform Tools for Solana development. This command requires Rust version 1.81 or higher.

```shell
cargo +1.81 install cargo-certora-sbf
```

--------------------------------

### Install Rust Toolchain

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Installs the Rust programming language and its associated toolchain using the official rustup installer script. This is a prerequisite for many Rust-based development environments.

```shell
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

```

--------------------------------

### CVL Rule Example: ruleexample

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_methods.html.md

An example of a CVL rule named ruleexample. It demonstrates access control by requiring the message sender to match a predefined sender address and then processes an event 'e'.

```cvl
ruleexample{
...enve;
addresssender;
requiree.msg.sender==sender;
c.process(e);
}
```

--------------------------------

### Using Pattern Matching for Method Summaries

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_multicontract_index.html.md

This example illustrates how to use pattern matching with underscores (`_`) in method summaries to cover multiple similar methods across different contracts. Instead of specifying each method individually, a wildcard can be used for the contract name or method name to simplify the summary definition.

```Solidity
    // Instead of:
    // underlying.balanceOf
    // Use patterns for broader coverage:
    // Asset.balanceOf
    // Or even more general:
    // _.balanceOf  // Applies to all balanceOf methods
```

--------------------------------

### Displaying Certora Prover Help Information

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_running.html.md

To view a concise summary of all available options and commands for the `certoraRun` utility, use the `--help` flag. This is useful for understanding the full capabilities of the tool.

```shell
certoraRun--help
```

--------------------------------

### Example usage of depth option in Certora Prover (CLI)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

An example demonstrating how to set the `depth` option when running the Certora Prover with specific contract and specification files.

```bash
certoraRunBank.sol--verifyBank:bank.spec--prover_args'-depth 5'
```

--------------------------------

### Certora CLI: Display Version

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Shows the version of the local installation of `certora-cli`. This is useful for checking if an installation is up-to-date or for debugging version-related issues. The latest version can be installed using `pip install --upgrade certora-cli`.

```cli
certoraRun--version
```

--------------------------------

### Example: Verifying Contract Creation with dynamic_bound

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

This example demonstrates how to use the `dynamic_bound` option when verifying a contract 'C' that creates instances of contract 'Foo'. It specifies that 'Foo' should be cloned at most 1 time during verification.

```cli
certoraRunC.solFoo.sol--verifyC:C.spec--dynamic_bound1
```

--------------------------------

### Solidity Contract Example with Struct Return

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_cvl2_changes.html?highlight=cvl2.md

A Solidity contract example defining a struct and functions that return this struct or multiple uint values. This serves as context for CVL specifications.

```solidity
contractExample{
structS{
uintfirstField;
uintsecondField;
boolthirdField;
}
functionf()returns(S){...}
functiong()returns(uint,uint){...}
}

```

--------------------------------

### Certora Prover Output Example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_running.html.md

This snippet shows a typical output from the Certora Prover during a verification run. It indicates that the job has been submitted to the server and provides a link to monitor the progress and view the final results on the Certora platform.

```text
... Job submitted to server
Follow your job at https://prover.certora.com
Once the job is completed, the results will be available at https://prover.certora.com/...
```

--------------------------------

### Certora Rule Example with Clogging and Assertions

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_solana_output.html.md

A Rust example demonstrating the use of `nondet` for non-deterministic values, `clog!` for logging variable states, `cvlr_assume!` for assumptions, and `cvlr_assert!` for assertions. This is useful for analyzing counterexamples.

```Rust
#[rule]
pubfnrule_fail_call_trace(){
letamount1:u64=nondet();
letamount2:u64=nondet();
cvlr_assume!(amount1>100);
cvlr_assume!(amount2!=10);
clog!(amount1,amount2);
cvlr_assert!(amount1<100);
cvlr_assert!(amount2<100);
}
```

--------------------------------

### Set Certora Key Environment Variable

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Sets a temporary environment variable for the Certora Key, which is required for authentication. An alternative method for persistent storage is available in the Certora Prover installation guide.

```bash
export CERTORAKEY=<personal_access_key>
```

--------------------------------

### CVL Direct Storage Havoc Example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_expr.html.md

Shows an example of using direct storage havoc in CVL, which allows arbitrary modification of storage variables during verification. This can be useful for testing boundary conditions and exploring state space.

```cvl
havoc s.balance;
havoc s.owner;
```

--------------------------------

### Certora Prover Configuration (Example)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson3_violations_erc20_bugs.html.md

This example shows how to configure the Certora Prover for running specifications, particularly when dealing with strings. Adding `'optimistic_loop': true` to the configuration file or using the `--optimistic_loop` flag is crucial for avoiding violations related to string manipulation within the prover.

```json
{
  "verify_mode": "continuous",
  "solc_version": "0.8.10",
  "optimistic_loop": true,
  "contracts": {
    "ERC20": {
      "spec_file": "./ERC20.spec",
      "source_file": "./ERC20.sol"
    }
  }
}
```

--------------------------------

### Solidity Hashing Example Contract

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_expr.html.md

An example Solidity contract featuring different hashing schemes using keccak256. It demonstrates hashing encoded primitives and raw byte signatures, illustrating various ways to use keccak256 for data integrity.

```Solidity
contractHashingExample{
structSignedMessage{
addresssender;
uint256nonce;
bytessignature;
}
mapping(bytes32=>uint256)messageToValue;
functionhashingScheme1(SignedMessagememorys)publicpurereturns(bytes32){
returnkeccak256(abi.encode(s.sender,s.nonce));
}
functionhashingScheme2(SignedMessagememorys)publicpurereturns(bytes32){
returnkeccak256(s.signature);
}
functionhashingScheme3(SignedMessagememorys)publicpurereturns(bytes32){
returnkeccak256(abi.encode(s.sender,s.nonce,keccak256(s.signature)));
}
functionhashingScheme4(SignedMessagememorys)publicpurereturns(bytes32){
returnkeccak256(abi.encode(s.sender,s.nonce,s.signature));
}}
```

--------------------------------

### Install CVL 1 Package Version

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_cvl2_migration.html.md

This command installs a specific version of the certora-cli Python package, pinning it to a version lower than 4.0.0 to continue using CVL 1. It's useful for users who are not yet ready to migrate their specifications to CVL 2.

```shell
pip install 'certora-cli<4.0.0'
```

--------------------------------

### Run Certora Prover for ERC20 Contract

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_erc20_example.html.md

This command initiates the verification process for an ERC20 contract. It specifies the Solidity contract, the verification specification file, and the Solidity compiler version. It's intended for simple cases, with config files recommended for complex scenarios.

```bash
certoraRunERC20.sol--verifyERC20:ERC20.spec--solcsolc8.0
```

--------------------------------

### CVL Foundry Integration Example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_hooks.html.md

Illustrates the basic integration of Certora Verification Language (CVL) with Foundry, a popular Ethereum development toolkit. This allows for specifying verification properties directly within a Foundry project, streamlining the verification workflow. The example shows how to import CVL rules.

```solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import "forge-std/Test.sol";
import "../src/MyContract.sol"; // Assuming MyContract.sol is in the src directory

contract MyContractTest is Test {
    MyContract public myContract;

    function setUp() public {
        myContract = new MyContract();
    }

    // Example: A test case that leverages CVL verification (conceptual)
    // In a real scenario, you would run `forge test --match-contract MyContractTest --no-commit`
    // and Certora's integration would pick up the CVL rules associated with MyContract.
    function test_complex_logic() public {
        // Call contract functions here and potentially assert expected outcomes.
        // CVL rules defined for MyContract will be checked by the Certora Prover.
        myContract.performAction(10);
    }
}
```

--------------------------------

### Specify Certora Prover Version

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

This example demonstrates how to specify a particular release version of the Certora Prover to use for verification, ensuring consistent testing across different environments.

```bash
certoraRunMyContract.sol--verifyMyContract:MySpec.spec--prover_versionrelease/10April2025
```

--------------------------------

### EVM Opcode Hook Example: EXTCODESIZE

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_hooks.html.md

This example demonstrates an EVM opcode hook for the EXTCODESIZE instruction. The hook executes immediately after the opcode is run, binding the opcode's address argument to `addr` and its return value to `v` within the hook's body.

```cvl
hookEXTCODESIZE(addressaddr)uintv{...}
```

--------------------------------

### Parametric Rule Example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

This code snippet provides an example of a parametric rule in Certora's specification language. It defines conditions based on method calls and state changes, demonstrating how to use method invocations within rules.

```solidity
rule {
  method f;
  event e;
  calldataarg args;
  address owner;
  address spender;
  mathint allowance_before = allowance(owner, spender);
  f(e, args);
  mathint allowance_after = allowance(owner, spender);
  assert allowance_after > allowance_before => e.msg.sender == owner;
}
```

--------------------------------

### CVL Specification File Example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_hooks.html.md

A basic example of a Certora Verification Language (CVL) specification file. CVL is used to define properties and rules for smart contract verification. This snippet demonstrates the structure of a specification, including imports, methods, and rules.

```cvl
import "path/to/your/contract.sol";

{
  // Declare your contract
  MyContract c;

  // Define conditions or properties here
  rule simple_rule() {
    require true;
    ensure c.someFunction() == 42;
  }
}
```

--------------------------------

### CVL Assert and Require Examples

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_statements.html.md

Illustrates the usage of 'assert' and 'require' statements within CVL rules. The first example demonstrates asserting the success of a 'withdraw' function, while the second verifies a post-condition on total funds after a 'deposit'.

```cvl
rule withdraw_succeeds{
  enve;
  // invoke function withdraw and assume that it does not revert
  bool success = withdraw(e);
  assert success, "withdraw must succeed";
}
rule totalFundsAfterDeposit(uint256 amount){
  enve;
  deposit(e, amount);
  uint256 userFundsAfter = getFunds(e, e.msg.sender);
  uint256 totalAfter = getTotalFunds(e);
  // Verify that the total funds of the system is at least the current funds of the msg.sender.
  assert totalAfter >= userFundsAfter;
}

```

--------------------------------

### Complex While Loop Example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_gaps.html.md

Presents a more complex while loop with an `true` condition and an internal break, showcasing scenarios where loop unrolling becomes less clear.

```solidity
uintx;// global state variable
uinti=0;
while(true){
x++;// if x overflows, we exit the loop and revert. But is this the loop condition?
if(i>=3){
break;
}
i+=1;
}
```

--------------------------------

### Run Certora Prover Rules (Shell)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_ci.html.md

This snippet demonstrates how to use the `certoraRun` command to execute specific verification rules or entire configuration files. It highlights the use of paths to configuration files and options to include or exclude specific rules.

```shell
certoraRun path-to-conf1.conf --rule rule1
certoraRun path-to-conf1.conf --exclude_rule rule2
certoraRun path-to-conf2.conf
```

--------------------------------

### Adding Helper Variables for Debugging (Certora Rule)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_preconditions.html.md

This snippet demonstrates how to add helper variables ('userBalanceBefore', 'totalBefore') to a Certora rule before a mint operation. This aids in understanding counter-examples by capturing state before the operation.

```spec
uint256userBalanceBefore=balanceOf(account);
uint256totalBefore=totalSupply();
```

--------------------------------

### CVL Exact Method Entry Example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_methods.html.md

An example of an exact method block entry in Certora CVL. This pattern matches a specific external function ('f') of a particular contract ('C') and requires a return type specification that must match the contract's function signature. It can include optional summaries and annotations.

```cvl
methods{
functionC.f(uintx)externalreturns(uint);
}
```

--------------------------------

### Running Certora Prover with a Configuration File (CLI)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_config_files.html.md

Demonstrates how to execute the Certora Prover using a previously defined configuration file. This command simplifies the process by referencing the .conf file instead of listing all arguments on the command line.

```bash
certoraRunsample_conf.conf
```

--------------------------------

### Display Help for Certora Solana Prover

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_solana_options.html.md

This command displays a help message for the Certora Solana Prover utility, providing a summary of available options and commands. It's useful for understanding the tool's capabilities.

```bash
certoraSolanaProver --help
```

--------------------------------

### Specify Receiver Contract in CVL2 Methods Block

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_cvl2_migration.html.md

In CVL2, method summaries are contract-specific. This example shows how to explicitly specify the receiver contract for a method summary. If no contract is specified, 'currentContract' is used by default. This ensures summaries are applied to the intended contract.

```CVL2
methods{
function ExampleContract.exampleMethod(uint) external returns(uint);
}
```

--------------------------------

### Running Certora Prover Command

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson1_prerequisites_formal_verification.html.md

The command to execute the Certora Prover on the 'sisters.spec' rule file. This command specifies the Solidity compiler version and the specific rule to verify. Ensure you are in the correct directory before running.

```bash
certoraRunEmpty.sol--verifyEmpty:sisters.spec--solcsolc8.0--rulesistersBirthMonths

```

--------------------------------

### Get Asset Balance in Liquidity Pool Contract

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_multicontract_index.html.md

Retrieves the current balance of the underlying asset held within the liquidity pool. This function is part of the IPool.sol contract and returns a uint256 representing the asset amount. It utilizes the asset's balanceOf function.

```solidity
function assetBalance() public view returns (uint256) {
  return asset.balanceOf(address(this));
}
```

--------------------------------

### Certora Prover Command for ERC20 Verification

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_running.html.md

This command initiates a verification process using the Certora Prover. It specifies the contract to verify and the corresponding specification file. The command assumes you are running it from a specific directory within the repository.

```bash
certoraRun contracts/correct/ERC20Fixed.sol --verify ERC20Fixed:certora/specs/ERC20Fixed.spec
```

--------------------------------

### ITeams Interface Definition

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_invariants.html.md

Defines the interface for managing teams, including functions to get a player's team, a team's leader, create teams, and change a team's leader. It specifies return values for unassigned players or non-existent teams.

```solidity
interface ITeams {
    /// @return The team id of the player
    /// @notice Return value of 0 means the player has not been assigned to a team
    function teamOf(address player) external view returns (uint8);

    /// @return The team leader
    /// @notice Return value of zero means the team has not been created
    function leaderOf(uint8 teamId) external view returns (address);

    /// @dev Players must not be assigned to any team
    /// @dev The team must not exist before the call
    function createTeam(
        address leader,
        address playerA,
        address playerB,
        uint8 teamId
    ) external;

    /// @notice Change the team's leader
    /// @dev Only the current leader may call this function
    /// @dev The new leader must be a member of the tem
    function changeLeader(address newLeader) external;
}
```

--------------------------------

### Basic Certora Prover Run Command

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_running.html.md

The `certoraRun` utility is used to invoke the contract compiler and send the verification job to Certora's servers. This is the most common command for initiating a verification process.

```shell
certoraRuncontractFile:contractName--verifycontractName:specFile
```

--------------------------------

### Solidity Contract Example with Interface Argument

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_cvl2_changes.html?highlight=cvl2.md

A sample Solidity contract snippet demonstrating a function that takes an interface type as an argument.

```Solidity
functionlistToken(IERC20token)internal{
  // implementation
}
```

--------------------------------

### Apply Environment Variable Changes (Bash)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

This command sources the specified shell script (e.g., `.zshenv` or `.profile`), applying any environment variable changes defined within it to the current shell session. This is necessary after modifying configuration files to make the changes active immediately.

```bash
source .zshenv
```

--------------------------------

### Basic Gambit Configuration JSON

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

A simple JSON object representing Gambit mutation options, mapping CLI options to key-value pairs. Boolean flags are set to true. This example specifies the Solidity file to mutate.

```json
{
"filename":"benchmarks/BinaryOpMutation/BinaryOpMutation.sol"
}
```

--------------------------------

### Add wabt to PATH

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Updates the system's PATH environment variable to include the binary directory of the WebAssembly Binary Toolkit (wabt). This makes tools like 'wasm2wat' accessible from the terminal.

```shell
export PATH=~/path/to/wabt/bin:$PATH

```

--------------------------------

### Generate Multiple Examples with multi_example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

The `multi_example` option instructs the Certora Prover to generate several counterexamples for failed assertions or witnesses for successful verifications. This is useful for debugging complex rules by revealing different control-flow paths or logical reasons for rule violations or adherence. It helps in identifying edge cases and refining specifications.

```shell
certoraRunMyContract.sol--verifyMyContract:MyContract.spec--multi_example
```

--------------------------------

### Wildcard Receiver Contract in CVL2 Methods Block

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_cvl2_migration.html.md

This example demonstrates how to use a wildcard receiver '_' in CVL2's methods block to apply a summary to methods with a given signature across all contracts. Note that wildcard entries cannot specify return types and may require an 'expect' clause when used with CVL functions or ghosts.

```CVL2
methods{
function _.exampleMethod(uint) external => NONDET;
}
```

--------------------------------

### Mutate Single Solidity File (Example)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Mutates a single Solidity file using the `--filename` (or `-f`) option. The file must be in the current working directory or a subdirectory. Use `--sourceroot` for arbitrary directories.

```bash
gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol
```

--------------------------------

### Build Gambit Release Binary

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Builds a release version of Gambit. This command generates a `gambit` binary in the `gambit/target/release/` directory, which can be manually placed on the PATH or invoked directly.

```bash
cargo build --release
```

--------------------------------

### Certora DISPATCHER Summary for executeOperation

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_multicontract_index.html.md

This configuration sets a DISPATCHER summary for the `executeOperation` method. It instructs the Certora Prover to try all contracts in the scene that implement this method when encountering an external call, to resolve unknown receivers.

```CVL
methods{
function _.executeOperation(uint256, uint256, address) external => DISPATCHER(true);
}
```

--------------------------------

### Install 'rustfilt' crate

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Installs the 'rustfilt' crate using Cargo. This tool is useful for demangling Rust symbol names, which can aid in debugging and understanding compiler output.

```shell
cargo install rustfilt

```

--------------------------------

### Add Solidity Executable Folder to PATH on macOS

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install_evm_compiler.html.md

This snippet shows how to add the directory containing Solidity executables to the system's PATH on macOS. This allows the `solc` command to be recognized without specifying the full path.

```shell
cd /etc/paths.d
sudo nano SolidityCertoraProver
/full/path/to/solc/executable/folder
echo $PATH
```

--------------------------------

### Check Python Version

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Checks the currently installed version of Python 3. This command is useful to ensure the Python version meets the requirements for installing the Certora Prover.

```bash
python3 --version
```

--------------------------------

### Run Certora Prover (Solana - Sources)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_solana_usage.html.md

Command to execute the Certora Prover using the 'running from sources' configuration. This command initiates the verification process by referencing a configuration file that points to a build script for compiling the Solana project.

```bash
certoraSolanaProversources_config.conf
```

--------------------------------

### Solidity: Basic Loop Unrolling Example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_approx_loops.html.md

Demonstrates how a simple Solidity for loop can be unrolled by the Certora Prover when the number of iterations is constant. The original loop is replaced by multiple sequential executions of its body.

```solidity
for(uint i=0; i<3; i++)
  j++;

```

```solidity
j++;
j++;
j++;

```

--------------------------------

### Install Vyper Compiler using Pip

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install_evm_compiler.html.md

Installs the Vyper compiler, an EVM-compatible Pythonic smart contract language, using pip. This is a common method for obtaining the compiler for development.

```bash
pip install vyper
```

--------------------------------

### Solidity: Example of Low-Level Contract Creation

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

An assembly snippet demonstrating how a contract `Foo` might be created using low-level `create` calls. This code is relevant when using the `--prototype` flag in the Certora CLI to specify the contract type for verification.

```solidity
assembly{
let ptr:=mload(0x40)
mstore(ptr,0x3d602d80600a3d3981f3363d3d373d3d3d363d73000000000000000000000000)
mstore(add(ptr,0x14),shl(0x60,implementation))
mstore(add(ptr,0x28),0x5af43d82803e903d91602b57fd5bf30000000000000000000000000000000000)
instance:=create(0,ptr,0x37)
}

```

--------------------------------

### Certora Configuration File Example (JSON)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_equiv-check_index.html.md

A standard Certora configuration file (`.conf`) in JSON format. It specifies settings like disabled type checking, files to include, prover options, and server details.

```json
{
  "disable_local_typechecking": true,
  "files": [
    "BasicMathGood.sol",
    "BasicMathBad.sol"
  ],
  "msg": "Equivalence Check",
  "optimistic_loop": true,
  "loop_iter": "4",
  "process": "emv",
  "send_only": true,
  "short_output": true,
  "rule_sanity": "basic",
  "solc": "solc8.0",
  "solc_optimize": "200",
  "server": "staging",
  "prover_version": "master"
}
```

--------------------------------

### Simplified Certora Prover Run Command (Matching Filename and Contract Name)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_running.html.md

If the contract file name matches the contract name (e.g., `MyContract.sol` for `MyContract`), the `certoraRun` command can be simplified by omitting the contract name from the `contractFile` argument.

```shell
certoraRuncontractFile--verifycontractName:specFile
```

--------------------------------

### Trivial Invariant Check Example

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_checking_sanity.html?highlight=rule%20sanity.md

This example shows a trivial invariant that holds in all possible states, not just reachable ones. The Certora Prover suggests converting such invariants into rules for efficiency. This example uses a custom language.

```certora
invariantsquaresNonNeg(intx)
x*x>=0;

```

--------------------------------

### CVL Hook Example: Storage Access

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_hooks.html.md

An example of using hooks in CVL to intercept storage access. Hooks allow for fine-grained control and observation of contract execution, particularly useful for analyzing state changes or simulating specific storage behaviors. This example shows how to hook into all storage loads.

```cvl
hook storage_access(addr: address, slot: uint256) returns (bool) {
  // Example: Log or modify storage access
  // This hook would be called for every storage load operation.
  // Returning true allows the operation, false would typically revert or alter behavior.
  return true;
}
```

--------------------------------

### Select Solidity Compiler Version

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_erc20_example.html.md

This command uses the `solc-select` tool to set the active Solidity compiler version. This is useful when you want to ensure your contract is compiled with a specific version without explicitly passing it via the `--solc` argument in `certoraRun`.

```bash
solc-select use 0.8.0
```

--------------------------------

### Check Java Version

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Checks the currently installed version of Java. This is a prerequisite for the Certora Prover, and version 11 or later is required.

```bash
java -version
```

--------------------------------

### Mapping CLI options to JSON: Multiple Arguments (List)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_prover_cli_conf-file-api.html.md

Demonstrates how CLI options that accept multiple arguments, like `--packages`, are translated into JSON arrays. Each element in the array corresponds to one argument.

```shell
certoraRun--packages@balancer-labs/v2-solidity-utils=pkg/solidity-utils\n@balancer-labs/v2-vault=pkg/vault
```

```json
{
"packages":[
"@balancer-labs/v2-solidity-utils=pkg/solidity-utils",
"@balancer-labs/v2-vault=pkg/vault"
]
}
```

--------------------------------

### Require Statement Example in CVL

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_statements.html.md

An example showcasing the require statement in CVL. It enforces that an amount must be greater than zero, influencing subsequent satisfiability checks.

```cvl
uint256amount;
requireamount>0;
satisfyamount>=0;
```

--------------------------------

### Run Certora Prover (Solana - Pre-built)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_solana_usage.html.md

Command to execute the Certora Prover for verifying pre-built Solana contracts. This command uses a configuration file that specifies pre-compiled contract files for the verification process.

```bash
certoraSolanaProverprebuilt_config.conf
```

--------------------------------

### Run Certora Soroban Prover with Configuration File

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_sunbeam_usage.html.md

This command demonstrates how to execute the Certora Soroban Prover using a .conf file. The command assumes the user is in the directory containing the configuration files and specifies the configuration file to be used for the verification process.

```bash
cd projects/path/to/conf/files
certoraSorobanProver filename.conf
```

--------------------------------

### CVL Examples of Logical Operators

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson1_prerequisites_propositional_logic.html.md

Provides side-by-side examples of complex propositional logic statements in both mathematical notation and their CVL equivalents, showcasing disjunction, implication, conjunction, and negation.

```CVL
(Q||R)=>(P&&S)
```

```CVL
(P=>(Q||R))&&(!P=>S)
```

--------------------------------

### Basic Mutation Configuration JSON

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_gambit_mutation-verifier.html.md

A JSON configuration file snippet demonstrating basic mutation testing setup. It specifies the files to verify, the verification target, and a 'mutations' object which includes Gambit for generating mutants with a specified number and filename.

```json
{
"files":[
"contracts/ERC20.sol"
],
"verify":"ERC20:certora/spec/ERC20.spec",
"msg":"ERC20Rules",
"mutations":{
"gambit":[
{
"filename":"contracts/ERC20.sol",
"num_mutants":5
}
],
"msg":"basic mutation configuration"
}
}

```

--------------------------------

### Assert Statement Example in CVL

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_statements.html.md

An example demonstrating the usage of the assert statement in CVL. It verifies that a balance variable remains positive, ensuring a minimum balance is maintained.

```cvl
uint256balance;
assertbalance>0;
```

--------------------------------

### Certora Run Command for Total Supply Rule

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_preconditions.html.md

This command executes a specific rule ('totalSupplyAfterMint') within the 'ERC20:TotalGreaterThanUser.spec' file using the Certora Prover with Solidity compiler version 8.0.

```bash
certoraRunERC20.sol--verifyERC20:TotalGreaterThanUser.spec--solcsolc8.0--ruletotalSupplyAfterMint
```

--------------------------------

### Run Parametric Rule Verification with Certora Runner (CLI)

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_parametric.html.md

This command demonstrates how to run a parametric rule verification using `certoraRun`. It specifies the contract, the Verilog specification file (`Parametric.spec`), the Solc version, and a message for the verification run.

```shell
certoraRunERC20.sol--verifyERC20:Parametric.spec--solcsolc8.0--msg"Parametric rule"
```

--------------------------------

### Certora Run Command with Precondition and Message

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_preconditions.html.md

This command executes the 'totalSupplyAfterMintWithPrecondition' rule using Certora Prover. It specifies the Solidity compiler version and includes a custom message for the run, useful for tracking and identification.

```bash
certoraRunERC20.sol--verifyERC20:TotalGreaterThanUser.spec--solcsolc8.0--ruletotalSupplyAfterMintWithPrecondition--msg"running with precondition"
```

--------------------------------

### Solidity: Example contract with enum

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_cvl_cvl2_changes.html.md

This is a sample Solidity contract snippet that defines an enum 'Permission' and a function 'f' that takes this enum as an argument. This serves as context for the CVL methods block examples.

```Solidity
contractExample{
enumPermission{READ,WRITE};
functionf(Permissionp)internal{...}
}

```

--------------------------------

### Add Solidity Executable Folder to PATH on Linux

Source: https://github.com/zgc-zgc/cerdtst/blob/master/docs.certora.com_en_latest_docs_user-guide_install_evm_compiler.html.md

This snippet demonstrates how to append the directory containing Solidity executables to the PATH environment variable in a Linux system by modifying the `.profile` file. It includes steps to edit the file, add the path, and source the profile to apply changes.

```shell
cd ~
nano .profile
PATH="$PATH:/full/path/to/solc/executable/folder"
nano .profile
source .profile
```