move-language / move

Apache License 2.0
2.25k stars 685 forks source link

[Prover] internal boogie error for `type_info` #701

Closed junkil-park closed 1 year ago

junkil-park commented 1 year ago

How to reproduce

Uncomment this line https://github.com/aptos-labs/aptos-core/pull/5712/files#diff-2f8d5cc984e8ad9aeddd19f91aeb2bb0a8421a8429399426631774b0218423b2R139.

Run Prover, and it will produces the following error:

$  move prove
[INFO] preparing module 0x1::debug
[INFO] preparing module 0x1::math128
[INFO] preparing module 0x1::math64
[INFO] preparing module 0x1::type_info
[INFO] preparing module 0x1::from_bcs
[INFO] preparing module 0x1::any
[INFO] preparing module 0x1::aptos_hash
[INFO] preparing module 0x1::bls12381
[INFO] preparing module 0x1::capability
[INFO] preparing module 0x1::comparator
[INFO] preparing module 0x1::copyable_any
[INFO] preparing module 0x1::ed25519
[INFO] preparing module 0x1::multi_ed25519
[INFO] preparing module 0x1::simple_map
[INFO] preparing module 0x1::pool_u64
[INFO] preparing module 0x1::ristretto255
[INFO] preparing module 0x1::secp256k1
[INFO] preparing module 0x1::table
[INFO] preparing module 0x1::table_with_length
[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 167 verification conditions
[INFO] running solver
Error: [internal] boogie exited with compilation errors:
output.bpl(6041,68): Error: cannot refer to a global variable in this context: #0_info
1 name resolution errors detected in **output.bpl**

Expected output

Prover produces no error.

junkil-park commented 1 year ago

Use the native spec functionspec_is_struct<T>() instead, and the issue is gone.