Skip to main content

Module invariant

Module invariant 

Source

ModulesΒ§

IInvariantTest
Module containing a contract’s types and functions.
campaign πŸ”’
error πŸ”’
replay πŸ”’
result πŸ”’
shrink πŸ”’

StructsΒ§

CheckSequenceOptions
Options controlling how check_sequence evaluates a candidate call sequence.
HandlerAssertionFailure
A handler-side assertion bug: a require/assert inside a fuzzed handler that the campaign reached. Deduped by (reverter, selector) site (Echidna/Medusa semantics), shortest sequence wins on collision.
HandlerReplayOutcome
Result of a strict handler-bug replay: anchor asserts, no earlier call asserts, and the recomputed edge fingerprint identifies which path the assertion took.
InvariantCampaignSeed πŸ”’
Immutable state selected once for a logical invariant campaign and cloned into each worker.
InvariantExecutor
Wrapper around any Executor implementer which provides fuzzing support using [proptest].
InvariantFailureMetrics πŸ”’
Tracks invariant failure counts during a campaign.
InvariantFailures
Stores invariant test failures and revert counts.
InvariantFuzzTestResult
The outcome of an invariant fuzz test
InvariantMetrics
Contains invariant metrics for a single fuzzed selector.
InvariantTest πŸ”’
Contains invariant test data.
InvariantTestData πŸ”’
Contains data collected during invariant test runs.
InvariantTestRun πŸ”’
Contains data for an invariant test run.
InvariantThroughputMetrics πŸ”’
Campaign-level throughput metrics for invariant progress reporting.

EnumsΒ§

FailureKey
Identifies a single entry in the InvariantFailures map. Invariant predicate failures and handler-side assertion bugs share one map keyed by this enum.
InvariantCorpusPersistence πŸ”’
InvariantFuzzError

ConstantsΒ§

DEFAULT_DEPTH_FOR_INVARIANT_WORKER_CAP πŸ”’
Baseline depth used to preserve the previous default-depth worker heuristic.
MIN_ESTIMATED_CALLS_PER_INVARIANT_WORKER πŸ”’
Minimum estimated handler calls assigned to each auto invariant worker.
MIN_RUNS_PER_INVARIANT_WORKER πŸ”’
Minimum number of logical runs assigned to each auto invariant worker at the default invariant depth.

FunctionsΒ§

auto_invariant_worker_count πŸ”’
build_invariant_progress_json πŸ”’
Builds the machine-readable invariant progress payload emitted during a campaign.
call_after_invariant_function πŸ”’
Calls the afterInvariant() function on a contract. Returns call result and if call succeeded. The state after the call is not persisted.
call_invariant_function πŸ”’
Calls the invariant function and returns call result and if succeeded.
check_sequence
Checks if the given call sequence breaks the invariant.
check_sequence_value
Executes a call sequence and returns the optimization value (int256) from the invariant function. Used during shrinking for optimization mode.
collect_data πŸ”’
Collects data from call for fuzzing. However, it first verifies that the sender is not an EOA before inserting it into the dictionary. Otherwise, we flood the dictionary with randomly generated addresses.
execute_tx πŸ”’
Executes a fuzz call and returns the result. Applies any block timestamp (warp) and block number (roll) adjustments before the call.
gas_report_samples_for_worker πŸ”’
handler_site_already_minimal
True iff there is already a HandlerAssertionFailure for site no longer than candidate_len. Used to skip inserting a not-strictly-shorter repro.
invariant_worker_count_with_threads πŸ”’
invariant_worker_runner πŸ”’
invariant_worker_seed πŸ”’
max_invariant_workers_for_campaign πŸ”’
rate_per_sec πŸ”’
Converts a cumulative campaign total into an average per-second rate.
record_new_invariant_failures πŸ”’
Bridges newly-recorded invariant breaks from failures.errors into the pulse failure_metrics so the live progress stream reflects breaks as they happen. Iterates in declaration order so the emitted β€œfailure” events are deterministic.
replay_error
Replays and shrinks a call sequence, collecting logs and traces.
replay_handler_failure_sequence
Replays a handler-bug sequence and returns whether the anchor still asserts on the same path. Rejects sequences with a pre-anchor assertion (would be a different bug).
replay_run
Replays a call sequence for collecting logs and traces. Returns counterexample to be used when the call sequence is a failed scenario.
should_continue_invariant_worker πŸ”’