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

[danilych]

#512
The bug was that we run create_and_process_bytecode for get target for create log files, and we not filter specs per visibility so it was cause of a lot of bugs like lack of ghosts even if some specs not included.

[cursor]

You have run out of free Bugbot PR reviews for this billing cycle. This will reset on March 1.

To receive reviews on all of your PRs, visit the Cursor dashboard to activate Pro and start your 14-day free trial.

[Copilot]

Pull request overview

This PR refactors the spec hierarchy log generation to create log files per verification target rather than processing all specs at once. The change improves the accuracy of spec hierarchy logs by ensuring each target (function or module) gets its own filtered context during verification.

Changes:

• Moved spec hierarchy log generation from the initialization phase to the verification phase
• Refactored spec_hierarchy::display_spec_hierarchy to support per-spec log writing via new write_spec_hierarchy_log function
• Removed premature spec hierarchy generation from sui-prover/prove.rs that used unfiltered targets

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.

File	Description
crates/sui-prover/src/prove.rs	Removed early spec hierarchy generation code and unnecessary imports (create_and_process_bytecode, FunctionHolderTarget, spec_hierarchy)
crates/move-stackless-bytecode/src/spec_hierarchy.rs	Added write_spec_hierarchy_log function for per-spec logging and refactored display_spec_hierarchy to use it
crates/move-prover-boogie-backend/src/generator.rs	Added write_spec_hierarchy_logs function that generates hierarchy logs during verification with properly filtered targets (only during AssertsMode::Check to avoid duplicates)

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[andreistefanescu]

👍

[danilych]

@claude internal tests failed in CI, is it related my changes? I checked, tests pass locally.

[claude]

Claude finished @danilych's task in 7s —— View job

---

CI Failure Analysis

• Check CI status for this PR
• Examine failed test logs
• Analyze root cause
• Determine if this is related to PR changes
• Provide recommendation

---

Summary

YES, the CI failure is related to your changes. The test move_test__vec_map_remove is failing because of how the PR changes target processing.

Failure Details

Failed Test: move_test__vec_map_remove
Error: prover::ensures does not hold at line 15: ensures(!m.contains(&10))

Test Code:

fun foo(m: &mut vec_map::VecMap<u64, u8>) {
  m.remove(&10);
}

#[spec(prove)]
fun foo_spec(m: &mut vec_map::VecMap<u64, u8>) {
  requires(m.contains(&10));
  foo(m);
  ensures(!m.contains(&10));  // ← Verification fails here
}

Root Cause

The PR removes the early call to create_and_process_bytecode with FunctionHolderTarget::All and instead only processes targets per-function with FunctionHolderTarget::Function.

Key Behavioral Change:

Before (main branch):

// In prove.rs - processes ALL targets together upfront
let (targets, _) = create_and_process_bytecode(
    &options, &model, &package_targets,
    FunctionHolderTarget::All  // ← Processes all specs together
);
spec_hierarchy::display_spec_hierarchy(&model, &targets, output_dir);

After (this PR):

// In generator.rs - processes per function during verification
let (mut targets, _) = create_and_process_bytecode(
    options, env, package_targets,
    FunctionHolderTarget::Function(*qid)  // ← Only processes this function
);

Why This Breaks Verification

When using FunctionHolderTarget::Function, the target filtering logic (function_target_pipeline.rs:530-537) excludes specs that are:

1. In a different module than the target
2. Not explicitly related via #[spec(include)]
3. Not marked as "system specs" (only includes modules at address 0x0 in SPECS_MODULES_NAMES)

VecMap is in the Sui framework (address 0x2) and is NOT in the SPECS_MODULES_NAMES list, so its specs/ghost state may not be properly included when verifying user functions that depend on it.

Recommendations

1. Short-term: You need to either:

   • Keep the early FunctionHolderTarget::All processing for ghost/spec initialization (but skip log file generation)
   • OR modify the filtering logic to always include Sui framework specs (vec_map, vec_set, table, etc.)

2. Medium-term: The test snapshot needs to be updated IF the failure is expected behavior, OR the code needs to be fixed if this is a regression.

Next Steps

Could you clarify the intended behavior? The PR description mentions fixing "lack of ghosts" bugs, but this change seems to introduce a new issue with VecMap verification.

The simplest fix might be to restore the early FunctionHolderTarget::All processing in prove.rs, but modify it to skip the spec hierarchy log generation (since that's now done per-function).

---