Create log file per target, not run checks for all specs at all

crates/move-prover-boogie-backend/src/generator.rs

@@ -314,6 +314,8 @@ fn generate_function_bpl<W: WriteColor>(
     let target_type = FunctionHolderTarget::Function(*qid);
     let (mut targets, _) = create_and_process_bytecode(options, env, package_targets, target_type);
 
+    write_spec_hierarchy_logs(env, &targets, &options, asserts_mode);
+
     check_errors(
         env,
         &options,
@@ -378,6 +380,8 @@ fn generate_module_bpl<W: WriteColor>(
 
     let (mut targets, _) = create_and_process_bytecode(options, env, package_targets, target_type);
 
+    write_spec_hierarchy_logs(env, &targets, &options, asserts_mode);
+
     check_errors(
         env,
         &options,
@@ -731,6 +735,20 @@ pub async fn verify_boogie(
     Ok(())
 }
 
+/// Write spec hierarchy log files for all specs in the given targets.
+/// Only writes during `AssertsMode::Check` to avoid duplicate writes.
+fn write_spec_hierarchy_logs(
+    env: &GlobalEnv,
+    targets: &FunctionTargetsHolder,
+    options: &Options,
+    asserts_mode: AssertsMode,
+) {
+    if asserts_mode == AssertsMode::Check {
+        let output_dir = Path::new(&options.output_path);
+        spec_hierarchy::display_spec_hierarchy(env, targets, output_dir);
+    }
+}
+
 /// Create bytecode and process it.
 pub fn create_and_process_bytecode(
     options: &Options,

crates/move-stackless-bytecode/src/spec_hierarchy.rs

@@ -30,56 +30,57 @@ struct CallInfo {
     spec_id: Option<QualifiedId<FunId>>,
 }
 
-/// Generates and writes specification hierarchy trees to log files.
+/// Writes the hierarchy log file for a single spec using already-built targets.
 ///
-/// For each spec in the targets, creates a `.log.txt` file in the output directory
-/// showing the complete call hierarchy including:
-/// - All functions called by the spec's underlying implementation
-/// - Spec properties (prove, no_opaque) for functions that have specs
-/// - System functions are excluded (stdlib, Sui framework, etc.)
-/// - Tree structure with proper indentation using box-drawing characters
-///
-/// # Tree Traversal
-/// - Recurses into functions without specs to find nested specs
-/// - Stops recursing at opaque specs (specs without `no_opaque`)
-/// - Recurses into `no_opaque` specs since the prover uses their implementation
-/// - Prevents infinite recursion by tracking displayed functions
+/// This is designed to be called during verification, reusing the
+/// `FunctionTargetsHolder` that was already created with proper per-spec
+/// filtering (e.g. `FunctionHolderTarget::Function`).
 ///
 /// # Arguments
-/// * `env` - Global environment containing all function and module information
-/// * `targets` - Holder containing all specs and their relationships
+/// * `env` - Global environment
+/// * `targets` - Targets holder with spec mappings (already built for this spec's context)
+/// * `spec_id` - The spec to write the hierarchy for
 /// * `output_dir` - Directory where .log.txt files will be written
-pub fn display_spec_hierarchy(env: &GlobalEnv, targets: &FunctionTargetsHolder, output_dir: &Path) {
+pub fn write_spec_hierarchy_log(
+    env: &GlobalEnv,
+    targets: &FunctionTargetsHolder,
+    spec_id: &QualifiedId<FunId>,
+    output_dir: &Path,
+) {
     let excluded_addresses = get_excluded_addresses();
+    let spec_env = env.get_function(*spec_id);
+    let spec_name = spec_env.get_full_name_str();
 
-    for spec_id in targets.specs() {
-        let spec_env = env.get_function(*spec_id);
-        let spec_name = spec_env.get_full_name_str();
+    if let Some(fun_id) = targets.get_fun_by_spec(spec_id) {
+        let func_env = env.get_function(*fun_id);
+        let header = func_env.get_full_name_str();
+        write_spec_log_file(
+            env,
+            targets,
+            &func_env,
+            spec_name,
+            &header,
+            output_dir,
+            &excluded_addresses,
+        );
+    } else if targets.is_scenario_spec(spec_id) {
+        let header = format!("{} {}", spec_env.get_full_name_str(), SCENARIO_LABEL);
+        write_spec_log_file(
+            env,
+            targets,
+            &spec_env,
+            spec_name,
+            &header,
+            output_dir,
+            &excluded_addresses,
+        );
+    }
+}
 
-        if let Some(fun_id) = targets.get_fun_by_spec(spec_id) {
-            let func_env = env.get_function(*fun_id);
-            let header = func_env.get_full_name_str();
-            write_spec_log_file(
-                env,
-                targets,
-                &func_env,
-                spec_name,
-                &header,
-                output_dir,
-                &excluded_addresses,
-            );
-        } else if targets.is_scenario_spec(spec_id) {
-            let header = format!("{} {}", spec_env.get_full_name_str(), SCENARIO_LABEL);
-            write_spec_log_file(
-                env,
-                targets,
-                &spec_env,
-                spec_name,
-                &header,
-                output_dir,
-                &excluded_addresses,
-            );
-        }
+/// Writes hierarchy log files for all specs in the given targets.
+pub fn display_spec_hierarchy(env: &GlobalEnv, targets: &FunctionTargetsHolder, output_dir: &Path) {
+    for spec_id in targets.specs() {
+        write_spec_hierarchy_log(env, targets, spec_id, output_dir);
     }
 }
 

crates/sui-prover/src/prove.rs

@@ -10,11 +10,9 @@ use move_core_types::account_address::AccountAddress;
 use move_model::model::GlobalEnv;
 use move_package::{BuildConfig as MoveBuildConfig, LintFlag};
 use move_prover_boogie_backend::boogie_backend::options::BoogieFileMode;
-use move_prover_boogie_backend::generator::{create_and_process_bytecode, run_boogie_gen};
+use move_prover_boogie_backend::generator::run_boogie_gen;
 use move_stackless_bytecode::function_stats;
-use move_stackless_bytecode::function_target_pipeline::FunctionHolderTarget;
 use move_stackless_bytecode::package_targets::PackageTargets;
-use move_stackless_bytecode::spec_hierarchy;
 use move_stackless_bytecode::target_filter::TargetFilterOptions;
 use std::{
     collections::BTreeMap,
@@ -184,21 +182,6 @@ pub async fn execute(
         return Ok(());
     }
 
-    let mut options = move_prover_boogie_backend::generator_options::Options::default();
-    options.filter = filter.clone();
-    let (targets, _) = create_and_process_bytecode(
-        &options,
-        &model,
-        &package_targets,
-        FunctionHolderTarget::All,
-    );
-
-    let output_dir = std::path::Path::new(&options.output_path);
-    if !output_dir.exists() {
-        std::fs::create_dir_all(output_dir)?;
-    }
-    spec_hierarchy::display_spec_hierarchy(&model, &targets, output_dir);
-
     execute_backend_boogie(model, &general_config, remote_config, boogie_config, filter).await
 }