Module extraction 

SMT-verified function-extraction transform.

Extracts a pure fixed-width-integer sub-block of an over-budget free function into a helper function — and COMMITS the extraction ONLY when the OxiZ-backed equivalence oracle PROVES the rewrite preserves the enclosing function’s semantics. This realises the project’s core proposal: only execute proven refactorings.

Pipeline (per over-budget free function):

1. detector::find_candidate — locate a maximal contiguous pure-integer run with clean, integer-typed live-in/live-out sets.
2. rewriter::rewrite — synthesise the helper ItemFn and the rewritten enclosing function that calls it.
3. gate::verify_and_decide — prove the rewrite equivalent (whole-function inline-back proof, falling back to a componentwise block proof). Commit only on a Verified; a Refuted (a rewriter/detector bug) is a skip.

On a committing verdict the input syn::File is mutated in place: the original Item::Fn is replaced by the rewritten function and the helper is inserted as a sibling Item::Fn. The committed helper is a normal free function that later flows through module_generator unchanged.

Scope of this cut: free functions only. Impl-method extraction (impl … { fn … }) is out of scope here and is intentionally skipped.

Gated behind the off-by-default smt cargo feature.

Enums

ExtractionOutcome

The outcome of attempting to extract a pure block from one function.

Functions

extract_pure_blocks

Extract a pure block from every over-budget free function in file, committing each extraction only when proven equivalence-preserving.

print_report

Print a per-outcome human-readable report to stdout.