Module invariant_breaker 

Invariant Breaker Module

Finds counterexamples to Solidity invariant expressions by generating random variable assignments that make the expression evaluate to false.

Usage

The invariant breaker provides async functions to find counterexamples to Solidity expressions. Use break_invariant() for simple cases or break_invariant_with_config() for custom configuration.

Supported Types

• Bool: true/false values
• UInt: 0 to u64::MAX
• Int: i64::MIN to i64::MAX
• String: random ASCII strings
• Address: 20-byte Ethereum addresses (hex)
• Bytes: variable-length byte arrays (hex)

Examples

Expression	Sample Counterexample
x > 10	x = 5 → (5 > 10)
a && b	a = false, b = true → (false && true)
balance >= amount	balance = 50, amount = 100 → (50 >= 100)

The module uses the Solidity parser, interpreter, and writer from the solidity crate to parse expressions, evaluate them with random values, and generate concrete output.

Structs

InvariantBreakerConfig

InvariantBreakerEntry

InvariantBreakerResult

Enums

InvariantBreakerValue

Functions

break_invariant

break_invariant_with_config