Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

sui move prove is unable to filter modules for verification #14325

Closed
rockbmb opened this issue Oct 18, 2023 · 1 comment
Closed

sui move prove is unable to filter modules for verification #14325

rockbmb opened this issue Oct 18, 2023 · 1 comment
Assignees
Labels

Comments

@rockbmb
Copy link
Contributor

rockbmb commented Oct 18, 2023

Steps to Reproduce Issue

  1. sui move new mre1
  2. Create the following two modules in sources:
    2.1. sources/five.move
    module mre1::five {
        public(friend) fun five(): u256 { 5 }
    
        spec five {
            // this function never aborts
            aborts_if false;
    
            // purposefully wrong!
            ensures result == 4;
        }
    }
    2.2. sources/seven.move
    module mre1::seven {
        public(friend) fun seven(): u256 { 7 }
    
        spec seven {
            // this function never aborts
            aborts_if false;
    
            ensures result == 7;
        }
    }
  3. Run (cd mre1; sui move prove)
  4. Run (cd mre1; sui move prove --target five)

Expected Result

Recall that sui move prove --help outputs

Options:
  -p, --path <PACKAGE_PATH>                     Path to a package which the command should be run with respect to
  -t, --target <TARGET_FILTER>                  The target filter used to prune the modules to verify. Modules with a name that contains this string will be part of verification
  ...

Meaning that sui move prove --target five should only run the Move Prover for the mre1::five module.

The expected result for both commands, sui move prove and sui move prove --target five is that both find the error with the purposefully incorrect specification of mre1::five::five.

Actual Result

The command sui move prove finds the aforementioned error, while sui move prove --target five fails with

Duplicate package entry for 'mre1'

System Information

$ lsb_release -a
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 20.04.6 LTS
Release:        20.04
Codename:       focal

$ rustc --version
rustc 1.73.0 (cc66ad468 2023-10-03)

$ sui --version
sui 1.12.0-1b5f809a1
@rockbmb
Copy link
Contributor Author

rockbmb commented Jan 11, 2024

Support for the prover is being sunset, so this can be closed; see #15480

@rockbmb rockbmb closed this as completed Jan 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

3 participants