move-language / move

Apache License 2.0
2.25k stars 685 forks source link

[Prover] `boogie_helpers.rs` panics for generic axioms #700

Closed junkil-park closed 1 year ago

junkil-park commented 1 year ago

How to reproduce

Uncomment the axioms here: https://github.com/aptos-labs/aptos-core/pull/5712/files#diff-1ae5dcd6645422049524d26540de53b5f1e45aa68d0a74f727b265a22e4dee3fR13

Run Prover, and it will produce the following error:

RUST_BACKTRACE=1 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
thread 'main' panicked at 'unexpected type', language/move-prover/boogie-backend/src/boogie_helpers.rs:194:35
stack backtrace:
   0: rust_begin_unwind
             at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/std/src/panicking.rs:584:5
   1: core::panicking::panic_fmt
             at /rustc/897e37553bba8b42751c67658967889d11ecd120/library/core/src/panicking.rs:142:14
   2: move_prover_boogie_backend::boogie_helpers::boogie_type
   3: core::ops::function::impls::<impl core::ops::function::FnOnce<A> for &mut F>::call_once
   4: <core::iter::adapters::flatten::FlatMap<I,U,F> as core::iter::traits::iterator::Iterator>::next
   5: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
   6: <alloc::collections::btree::set::BTreeSet<T> as core::iter::traits::collect::FromIterator<T>>::from_iter
   7: move_prover_boogie_backend::add_prelude
   8: move_prover::generate_boogie
   9: move_prover::run_move_prover_with_model
  10: move_cli::base::prove::run_move_prover
  11: move_cli::base::prove::Prove::execute
  12: move_cli::run_cli
  13: move_cli::move_cli
  14: move::main
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Expected result

Prover produces no error.

junkil-park commented 1 year ago

The panic happens at this line: https://github.com/move-language/move/blob/main/language/move-prover/boogie-backend/src/boogie_helpers.rs#L194

For some reason, Prover concretizes a type parameter T into Primitive(Range). This causes the panic.