aptos Prover Question

[yue1823]

Discord user ID

.yue.

Describe your question in detail.

when i trying to use aptos move prove ,show this error

Therefore , I use this command source ~/.profile
Then I get another error

Anyone can help me to solve this error

What error, if any, are you getting?

No response

What have you tried or looked at? Or how can we reproduce the error?

No response

Which operating system are you using?

macOS Macbook Pro m1 Arm

Which SDK or tool are you using? (if any)

Aptos CLI

Describe your environment or tooling in detail

aptos move prove on idea

[WGB5445]

Can you mark your system, version and computer architecture? This may be more helpful in solving the problem.

Also, have you tried restarting the terminal or computer? At first glance, it seems that it may be due to an environment variable issue.

[yue1823]

i am using macbook m1 arm , restart seems not help in this situation ( I try it )

[MoonShiesty]

dont think this is related to your environment

can you post your source-code/specs you're proving?

ive seen this error before can't remember how to reproduce. dont remember the details but i think it happens when you call non-spec functions outside of your module in a spec. i imagine if you start to comment out the specs and re-run the prover itll work again at some point

[yue1823]

I am not set any spec in /source ,actually I don't know what's the spec you are refer to

[yue1823]

[yue1823]

the error is for this one
#[lint::allow_unsafe_randomness]
but i dont think this would be the reason of prove error

[MoonShiesty]

im just starting to learn the prover, and have no idea how attributes are processed. i imagine aptos needs to add something to randomness.spec.move

i also see that aptos added this attribute to aptos-core at the end of june, id double check you're using the latest aptos-core and cli

for now you should be able to turn off verification for that function instead of at the module scope, and see if you can prove the rest of your project

try putting this at the top of the function that uses allow_unsafe_randomness, and turn back on verification at the module level:
pragma verify = false

[yue1823]

if i add

spec module {
        pragma verify = false; // TODO: see issue <url>
    }

[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 16 verification conditions
[INFO] running solver
[INFO] 1.625s build, 3.977s trafo, 0.048s gen, 6.090s verify, total 11.741s
{
"Result": "Success"
}

[0xbrw]

@yue1823 can you share your entire code file and the commands you ran so I can try to reproduce the error on my side?

[yue1823]

game.zip

[package]
name = "chips"
version = "1.0.0"
authors = []

[addresses]
dapp="0x2"
admin="0x555"
admin1="0xeee"
admin2="0xa51"
[dev-addresses]

[dependencies.AptosFramework]
git = "https://github.com/aptos-labs/aptos-core.git"
rev = "mainnet"
subdir = "aptos-move/framework/aptos-framework"

[dependencies.AptosTokenObjects]
git = "https://github.com/aptos-labs/aptos-core.git"
#git = "https://gitee.com/WGB5445/aptos-core.git"
rev = "mainnet"
subdir = "aptos-move/framework/aptos-token-objects"

[dev-dependencies]

please dont share to others

[0xbrw]

I was able to run the aptos prover against your code.

[INFO] preparing module 0x1::game
[INFO] preparing module 0x2::helper
[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 16 verification conditions
[INFO] running solver
[INFO] 11.909s build, 21.845s trafo, 0.296s gen, 38.918s verify, total 72.969s
{
  "Result": "Success"
}

The problem occurs if you have installation issues with the move prover. A good way to test is to run the prover in the example here: https://aptos.dev/en/build/cli/setup-cli/install-move-prover If that works, you can copy over your project to the /move-examples sub-directory and run the prover from there

[yue1823]

You run success results since I set
‘
spec module {
pragma verify = false; // TODO: see issue
}
‘
on lowest of my code, could you try to close it and run again?

[wrwg]

Please follow the instructions on how to install the Move Prover auxiliary tools here. If the variable BOGGIE_EXE is not set, it indicates that the tools are not correctly configured. Unfortunately, for this you need to fork the aptos-core repo. (However, you only need the source to execute a shell script in there, no build of anything needed inside there.)

We are working on making this experience better.

[wrwg]

@yue1823 @bwdotcom there is 2nd issue apart of setting up the Move Prover correctly, thanks for brining it up! I isolated the cause and opened a bug for it. Fix should be forthcoming, you can follow along at the bug.

[yue1823]

i also find this error from my code when i try to use batch_transfer_coins<CoinA>() this function ,seems is a bug like yours report