Module slicer 

Backward data-dependency slicer.

Given a path tree, a checkpoint, and a property, it walks each path backward to keep only the MIR items that are data-relevant to the property, producing one ProofGoal per path for the symbolic VM to execute forward.

Modules

call_visit 🔒

Call-terminator visiting logic.

types 🔒

Data types for the path-refinement layer.

visitor 🔒

Backward path visitor — walks a finite path backward from a checkpoint and keeps only MIR items that can affect the required property.