Description

Filtering of verification target using aptos move prove -f does not work when the target module calls a public(package) function from a callee module because when a filter is applied, only the target module is treated as primary.

This PR tries to resolve the issue by recording all modules that are filtered out when building the model and then allowing the target module to call public(package) functions defined in them.

close #15772.

How Has This Been Tested?

Manually execute aptos move prove -f.

Key Areas to Review

Whether there is a better way to fix the issue more generally.

Type of Change

• New feature
• Bug fix
• Breaking change
• Performance improvement
• Refactoring
• Dependency update
• Documentation update
• Tests

Which Components or Systems Does This Change Impact?

• Validator Node
• Full Node (API, Indexer, etc.)
• Move/Aptos Virtual Machine
• Aptos Framework
• Aptos CLI/SDK
• Developer Infrastructure
• Move Compiler
• Move prover

Checklist

• I have read and followed the CONTRIBUTING doc
• I have performed a self-review of my own code
• I have commented my code, particularly in hard-to-understand areas
• I identified and added all stakeholders and component owners affected by this change as reviewers
• I tested both happy and unhappy path of the functionality
• I have made corresponding changes to the documentation