We should add the --target-dir option to prove-rs, similarly to how it's done for run in #777; it should be used instead of reduce_to. That's based on the suggestion made by @Stevengre:
Since it costs a lot of time to prepare the kmir , what do you think that we provide a file level from_kompiled_kore without reduce_to(start_symbol). Then, we can reuse the kmir for different functions in one file.