Module driver 

Driver utilities for the staged verifier pipeline.

The target collector owns selected functions and their callee requirements. The path extractor upgrades a function CFG into SCC-aware path metadata. VerifyDriver prepares paths for two kinds of checks (unsafe checkpoints and struct invariants) and delegates the actual backward/forward/SMT work to the shared VerifyEngine.

Structs

CheckpointCheckView 🔒

Returns whether a function returns the owning struct type (i.e. is a constructor). Borrowed view of all verification inputs for one unsafe checkpoint.

VerifyDriver 🔒

Orchestrates the three-stage verification pipeline (backward data-dependency analysis → forward state simulation → SMT checking) for a single function under analysis.

VerifyRun 🔒

Analysis pass that runs verification and emits function-level summaries.

Functions

property_field_indices 🔒

Collect struct field indices referenced by a property’s contract places.

remap_constructor_contract 🔒

targets_return_value 🔒

Whether an invariant targets the function’s return value (as opposed to a parameter / the receiver). Only Atom invariants carry a first-argument place; And/Or invariants have no target_place, so they are never treated as return-value invariants.