Module loop_sensitivity 

Loop-sensitivity planning for the staged verifier.

The planner runs before path extraction in verify --postfix-repeat auto. It keeps the decision about loop depth separate from individual safety-tag checkers: tags still describe what must hold, while this module decides whether the checked value depends on loop-carried MIR state.

Pipeline role

VerifyTargetCollector ──► LoopSensitivityAnalyzer ──► VerifyDriver
       (sinks)                 (repeat plan)             (paths + checks)

The normal verifier is path-bounded: PathExtractor receives a numeric allow_repeat and enumerates only that many extra SCC postfix repetitions. In auto mode, this module chooses that number from MIR structure instead of from an already-failed tag-specific retry loop.

Current abstraction

The planner now has two internal hint streams:

• DataflowDistanceHint: a sink depends on loop-carried state, and the planner estimates how many loop backedges are needed for that state to reach the sink.
• NumericRangeHint: a numeric/index obligation depends on induction-style state, and the planner estimates the first iteration that can witness a range violation.

RepeatPlan is the single product consumed by the driver. It calibrates both hint kinds into the PathEnumerator’s allow_repeat budget and picks the maximum, so detector-specific details stay inside this module.

Structs

ComparisonFact 🔒

A MIR comparison that feeds a boolean branch.

DataflowDistanceHint 🔒

A loop-carried dataflow hint.

LocalDependencyIndex 🔒

Whole-function local dependency index.

LoopComponent 🔒

A non-trivial SCC in the MIR control-flow graph.

LoopLocalSummary 🔒

Local assignment and transfer summary for one loop SCC.

LoopNumericSummary 🔒

Numeric induction summary for one loop SCC.

LoopSensitivityAnalyzer 🔒

Computes the repeat plan for one verification target.

NumericRangeHint 🔒

A numeric/index range hint.

RepeatPlan 🔒

Unified product of the auto loop-sensitivity pass for one function target.

SafetySink 🔒

One safety obligation whose arguments have been bound to caller MIR locals.

SwitchSuccessor 🔒

Switch successor annotated with the boolean value that selects it.

Enums

NumericTerm 🔒

Small numeric term language for loop guards.

RepeatStrategy

User-selected policy for SCC postfix repetition.

Constants

BRANCH_SENSITIVE_BACKEDGES 🔒

Backedge budget used when an internally branched SCC has loop-carried assignments into a checked sink.

DEFAULT_LOOP_CARRIED_BACKEDGES 🔒

Fallback loop-carried distance used when a sink is loop-sensitive but the local transfer graph is too imprecise to calculate a better distance.

DEFAULT_NUMERIC_WITNESS_ITERATION 🔒

Conservative first numeric witness when an index obligation is known to be induction-sensitive but the current summary cannot yet recover a concrete symbolic bound.

MAX_AUTO_REPEAT 🔒

Upper bound for repeat selected by auto mode.

MIN_DATAFLOW_REPEAT 🔒

The first repeat depth that reliably exposes the existing delayed loop-carried pointer/state fixtures.

Functions

block_reaches_component 🔒

Return whether start can reach any block in component.

ceil_div_i128 🔒

Integer ceil-div for positive operands.

collect_assigned_locals 🔒

Collect locals directly redefined by statements or call destinations.

collect_entry_lower_bounds 🔒

Collect numeric lower bounds that hold on paths entering this SCC.

collect_loop_guard_upper_bounds 🔒

Collect loop-guard upper bounds for induction locals.

collect_operand_sources 🔒

Add the local read by a MIR operand, if any.

collect_rvalue_sources 🔒

Add local operands referenced by an rvalue to out.

comparison_fact 🔒

Extract a simple comparison from an rvalue.

component_has_internal_branch 🔒

Return true when a component contains a real in-loop branch.

component_reaches_checkpoint 🔒

Returns true if any block in component can reach checkpoint via CFG edges.

estimate_branch_sensitive_backedges 🔒

Estimate extra budget needed when a loop-carried sink is controlled by internal SCC branches.

estimate_dataflow_backedges 🔒

Estimate how far loop-carried state must travel before reaching a sink.

estimate_inbound_witness 🔒

Estimate an index-range witness for InBound.

estimate_valid_num_witness 🔒

Estimate the first violating iteration for a simple ValidNum sink.

expr_const_i128 🔒

Extract a contract integer constant small enough for the planner model.

expr_is_place 🔒

Return true when a contract expression is a plain numeric place.

first_field_projection 🔒

Return the first field projected from a place.

flatten_or_property 🔒

Collect the non-Or leaf properties of a (possibly compound) property tree.

graph_reaches_any 🔒

Return whether a loop SCC can reach a given checkpoint block.

increment_source_and_step 🔒

Extract local +/- const from an arithmetic rvalue.

local_is_argument 🔒

Return true if local is a function argument local.

loop_components 🔒

Extract loop SCCs from PathGraph.

lower_bound_from_branch 🔒

Infer a local lower bound from taking one boolean branch of a comparison.

max_state_distance_from 🔒

DFS over dependency edges, counting only loop-carried state locals.

numeric_term_from_operand 🔒

Convert a MIR operand into the planner’s small numeric term language.

numeric_term_lower_bound 🔒

Resolve a known lower bound for a numeric term.

operand_const_i128 🔒

Return the local used by an operand when the operand is a plain local place. Extract an integer constant from an operand.

place_is_indirect_write 🔒

Return true when an assignment writes through a pointer/reference.

plain_copy_source 🔒

Return the source local for a plain local copy/move rvalue.

repeat_for_backedges 🔒

Convert loop backedge distance to PathEnumerator::allow_repeat.

repeat_for_witness_iteration 🔒

Convert a 1-based loop-body witness iteration to allow_repeat.

resolve_local_copy 🔒

Follow plain copy chains for a local.

resolve_numeric_term 🔒

Follow copy chains inside a numeric term.

rvalue_const_i128 🔒

Extract a direct constant assignment from an rvalue.

rvalue_projection_source 🔒

Return the source temp for tmp.field_index.

simple_upper_bound_violation_value 🔒

Match x < C, x <= C, and their constant-on-left equivalents.

switch_successors 🔒

Return all explicit and otherwise successors of a bool-like switch.

valid_num_violation_value 🔒

Extract the lowest value that violates a simple upper-bound ValidNum.

witness_iteration_for_threshold 🔒

Compute the first 1-based iteration where init + step * iteration reaches violation_value.