Counterexample Generation

Generating counterexamples for failing proofs in Kontrol

Overview

Counterexample generation is a new experimental feature in Kontrol that helps developers understand why their proofs fail by providing concrete examples of inputs and execution paths that violate the properties being tested. It enables the users to easily reproduce the failing test case with Foundry and is essential for debugging and improving smart contract verification.

What Are Counterexamples?

A counterexample in the context of formal verification is a concrete execution trace that demonstrates how a property can be violated. In Kontrol, counterexamples show input values that lead to property violations and the path conditions that should be satisfied for the failure to occur.

How Counterexample Generation Works

Kontrol generates counterexamples by:

1. Analyzing failed proofs: When a proof fails, Kontrol identifies the specific execution path that led to the failure and generates the model that demonstrates the concrete values that symbolic variables should take for the failure to happen

2. Extracting concrete values: Symbolic variables are instantiated with concrete values that trigger the failure

3. Constructing execution trace: The complete execution path is reconstructed with concrete values in the form of a Foundry test case and is saved in a new file

Basic Usage

Experimental Feature: Counterexample generation is currently experimental, and dynamically-sized types like bytes of variable length, mappings, and arrays are not supported. The KontrolTest contract generated by kontrol init includes some auxiliary functions that allow setting up symbolic storage for these types manually.

Step 1: Enable Counterexample Generation

Counterexample generation is enabled by providing the --generate-counterexample option to kontrol prove. When a proof fails, Kontrol automatically generates concrete counterexample test functions:

kontrol prove --function testMyProperty --generate-counterexample

Step 2: Generated Counterexample Functions

When a proof fails, Kontrol generates a new Solidity test file with concrete counterexample functions. For example, let's consider the following failing test:

Original Failing Test:

function test_storage_setup(
    uint256 totalSupply, 
    uint256 _totalSupply, 
    address _owner, 
    uint256 _currentUser_id, 
    address _currentUser_wallet, 
    bool _currentUser_isActive, 
    uint256 _anotherTotalSupply
) public {
    assert(totalSupply != 0);

    simpleStorageStorageSetup(address(simpleStorage), _totalSupply, _owner, _currentUser_id, _currentUser_wallet, _currentUser_isActive);
    assert(simpleStorage.totalSupply() == _anotherTotalSupply);
}

This proof, when executed with kontrol prove --no-fail-fast, will result in two failing nodes: one for the violation of assert(totalSupply != 0), and one for assert(simpleStorage.totalSupply() == _anotherTotalSupply). When executed with --generate-counterexample, kontrol prove will generate a file named SimpleStorageTestCounterexampleTest.t.sol with these two functions:

Generated Counterexample Functions:

function test_storage_setup_ce0() public {
    // Counterexample values from failed proof:
    uint256 totalSupply = 0;
    uint256 _totalSupply = 0;
    address _owner = address(0);
    uint256 _currentUser_id = 0;
    address _currentUser_wallet = address(0);
    bool _currentUser_isActive = false;
    uint256 _anotherTotalSupply = 0;

    assert(totalSupply != 0);

    simpleStorageStorageSetup(address(simpleStorage), _totalSupply, _owner, _currentUser_id, _currentUser_wallet, _currentUser_isActive);
    assert(simpleStorage.totalSupply() == _anotherTotalSupply);
}

function test_storage_setup_ce1() public {
    // Counterexample values from failed proof:
    uint256 totalSupply = 1;
    uint256 _totalSupply = 1;
    address _owner = address(0);
    uint256 _currentUser_id = 0;
    address _currentUser_wallet = address(0);
    bool _currentUser_isActive = false;
    uint256 _anotherTotalSupply = 0;

    assert(totalSupply != 0);

    simpleStorageStorageSetup(address(simpleStorage), _totalSupply, _owner, _currentUser_id, _currentUser_wallet, _currentUser_isActive);
    assert(simpleStorage.totalSupply() == _anotherTotalSupply);
}

These tests can now be concretely executed with Foundry to reproduce the failing test cases:

forge test --match-test test_storage_setup_ce0
forge test --match-test test_storage_setup_ce1

Key Features:

• Multiple failing nodes: Generates indexed counterexample functions (_ce0, _ce1) for different failure scenarios

• Concrete values: Automatically maps symbolic variables of supported types to concrete values that trigger the failure. Supported types including uint and int of any width, address, bool, bytes of fixed length, and struct variables

• Automatic file generation: Creates {OriginalTestContractName}CounterexampleTest.t.sol in the same directory as the original proof contract

• Type conversion: Properly handles Solidity type conversions between SMT model assignments (usually of int type) and Solidity types

Generated Files

The counterexample generation creates a new test file with the naming pattern:

• Original file: MyContractTest.t.sol

• Generated file: MyContractTestCounterexampleTest.t.sol

The generated file is placed in the same directory as the original test file to maintain accurate import paths.

Development Workflow

1. Write property: Define the property you want to verify

2. Run initial proof: kontrol prove --function testProperty --generate-counterexample

3. Analyze counterexample: If it fails, examine the generated counterexample

4. Fix the issue: Use the counterexample to validate, identify, and fix the problem using Foundry's concrete execution for faster iteration

5. Re-run proof: Verify the fix resolves the counterexample

6. Iterate: Repeat until the proof passes

Related Features

• Structured Symbolic Storage Generation - Automated storage setup

• Symbolic Storage - Manual storage management

• Debugging Failing Proofs - General debugging guide

References

• Kontrol Cheatcodes Reference