search

pontem-network / dove

🛠️ Diem/Pontem Move package manager
MIT License
35 stars 13 forks source link

[PONC-69] Move prover integration #55

Closed vitvakatu closed 3 years ago

vitvakatu commented 3 years ago

Added dove prove subcommand that runs move-prover on project sources and dependencies.

This functionality is hidden behind prover feature-gate until move-prover will be fixed.

villesundell commented 3 years ago

Thank you for providing "dove prove", much anticipated here! :+1:

However, {{sender}} seems to be unsupported:

 16 │ address {{sender}} {
    │         ^ Unexpected '{'
vitvakatu commented 3 years ago

@villesundell hello, nice catch and thank you for testing! I will implement support for it.

villesundell commented 3 years ago

Thank you for fixing this so quickly :slightly_smiling_face:

However, now I get the following when running "dove prove" in https://github.com/taoheorg/taohe repository:

thread 'main' panicked at 'assertion failed: self.fun_table.insert(name, entry).is_none()', /home/ville/.cargo/git/checkouts/diem-f4eb8cae7023c917/8e60a94/language/move-model/src/builder/model_builder.rs:273:9
stack backtrace:
   0:     0x558877326b90 - std::backtrace_rs::backtrace::libunwind::trace::h25e12e0d899beba0
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/../../backtrace/src/backtrace/libunwind.rs:90:5
   1:     0x558877326b90 - std::backtrace_rs::backtrace::trace_unsynchronized::h70e61195d6ae3df6
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x558877326b90 - std::sys_common::backtrace::_print_fmt::hba93ab80d779695a
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/sys_common/backtrace.rs:67:5
   3:     0x558877326b90 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::hf092b5883b4b2e50
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/sys_common/backtrace.rs:46:22
   4:     0x55887734d09c - core::fmt::write::hf68bc350a8f2f0dc
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/core/src/fmt/mod.rs:1078:17
   5:     0x55887731ded2 - std::io::Write::write_fmt::hf66811b1bc767436
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/io/mod.rs:1517:15
   6:     0x558877329225 - std::sys_common::backtrace::_print::hd425a11bfe1f20f8
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/sys_common/backtrace.rs:49:5
   7:     0x558877329225 - std::sys_common::backtrace::print::h6d678795c1e61e13
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/sys_common/backtrace.rs:36:9
   8:     0x558877329225 - std::panicking::default_hook::{{closure}}::h78a02a4a0dee5e7e
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/panicking.rs:208:50
   9:     0x558877328d7a - std::panicking::default_hook::h56eb7eda02f355a7
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/panicking.rs:225:9
  10:     0x5588773299c1 - std::panicking::rust_panic_with_hook::hb27ea14285131c61
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/panicking.rs:591:17
  11:     0x5588773294d7 - std::panicking::begin_panic_handler::{{closure}}::hc552fcee62aad17f
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/panicking.rs:495:13
  12:     0x55887732704c - std::sys_common::backtrace::__rust_end_short_backtrace::hb9f0aa9a78e885a0
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/sys_common/backtrace.rs:141:18
  13:     0x558877329469 - rust_begin_unwind
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/panicking.rs:493:5
  14:     0x55887734afc1 - core::panicking::panic_fmt::h12ac4570ea43d06f
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/core/src/panicking.rs:92:14
  15:     0x55887734af0d - core::panicking::panic::h72bd72f6f4a70105
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/core/src/panicking.rs:50:5
  16:     0x558875cb8bdc - move_model::builder::model_builder::ModelBuilder::define_fun::h7bcb02c21224c038
                               at /home/ville/.cargo/git/checkouts/diem-f4eb8cae7023c917/8e60a94/language/move-model/src/builder/model_builder.rs:273:9
  17:     0x558875bd2e63 - move_model::builder::module_builder::ModuleBuilder::decl_ana_fun::h3a5c8f21048e10cb
                               at /home/ville/.cargo/git/checkouts/diem-f4eb8cae7023c917/8e60a94/language/move-model/src/builder/module_builder.rs:327:9
  18:     0x558875bd1d80 - move_model::builder::module_builder::ModuleBuilder::decl_ana::haa6f872ad78d676d
                               at /home/ville/.cargo/git/checkouts/diem-f4eb8cae7023c917/8e60a94/language/move-model/src/builder/module_builder.rs:258:13
  19:     0x558875bd0c39 - move_model::builder::module_builder::ModuleBuilder::translate::hc0faf440f3c77ba7
                               at /home/ville/.cargo/git/checkouts/diem-f4eb8cae7023c917/8e60a94/language/move-model/src/builder/module_builder.rs:151:9
  20:     0x558875c3f7ef - move_model::run_spec_checker::h4623d4d504df0cc3
                               at /home/ville/.cargo/git/checkouts/diem-f4eb8cae7023c917/8e60a94/language/move-model/src/lib.rs:257:9
  21:     0x558875c3dfb8 - move_model::run_model_builder::h47d42bd19fba4430
                               at /home/ville/.cargo/git/checkouts/diem-f4eb8cae7023c917/8e60a94/language/move-model/src/lib.rs:109:5
  22:     0x55887510d78f - move_prover::run_move_prover::hb3a053385c211b93
                               at /home/ville/.cargo/git/checkouts/diem-f4eb8cae7023c917/8e60a94/language/move-prover/src/lib.rs:63:30
  23:     0x55887510f3d9 - move_prover::run_move_prover_errors_to_stderr::hb1447eb18c9b90e1
                               at /home/ville/.cargo/git/checkouts/diem-f4eb8cae7023c917/8e60a94/language/move-prover/src/lib.rs:189:5
  24:     0x5588745f7fec - <dove::cmd::prover::Prove as dove::cmd::Cmd>::apply::h8514440d8417ed21
                               at /home/ville/projects/move-tools/dove/src/cmd/prover.rs:66:9
  25:     0x55887458fb0b - dove::cmd::Cmd::execute::h4b5bf1d63c07d019
                               at /home/ville/projects/move-tools/dove/src/cmd/mod.rs:52:9
  26:     0x55887457b547 - dove::cli::execute::hd41f78457adb82d2
                               at /home/ville/projects/move-tools/dove/src/cli.rs:98:31
  27:     0x558874588f6e - dove::main::ha10c087db2e2f9b6
                               at /home/ville/projects/move-tools/dove/src/bin/dove.rs:12:15
  28:     0x5588745890cb - core::ops::function::FnOnce::call_once::hcbb4334a454cc095
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/core/src/ops/function.rs:227:5
  29:     0x55887458ec5e - std::sys_common::backtrace::__rust_begin_short_backtrace::h5a0bf3f0fbce474f
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/sys_common/backtrace.rs:125:18
  30:     0x558874589bd1 - std::rt::lang_start::{{closure}}::he517921b4ecdff04
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/rt.rs:66:18
  31:     0x558877329ed7 - core::ops::function::impls::<impl core::ops::function::FnOnce<A> for &F>::call_once::h78040f802d89ccdc
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/core/src/ops/function.rs:259:13
  32:     0x558877329ed7 - std::panicking::try::do_call::h6853cad536dd09a1
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/panicking.rs:379:40
  33:     0x558877329ed7 - std::panicking::try::h827495f03a9fbb9a
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/panicking.rs:343:19
  34:     0x558877329ed7 - std::panic::catch_unwind::h4bdf17571090eb17
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/panic.rs:396:14
  35:     0x558877329ed7 - std::rt::lang_start_internal::h2f319c33bb013f29
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/rt.rs:51:25
  36:     0x558874589ba7 - std::rt::lang_start::h0eee56c186f7cfe9
                               at /rustc/cb75ad5db02783e8b0222fee363c5f63f7e2cf5b/library/std/src/rt.rs:65:5
  37:     0x55887458900a - main
  38:     0x7fd4449010b3 - __libc_start_main
  39:     0x55887457aa9e - _start
  40:                0x0 - <unknown>
vitvakatu commented 3 years ago

@villesundell I'm afraid a bit more work is needed in this PR. move-prover is under active development right now, and we're using not the latest available version. But thank you for participating, I will look into it.

vitvakatu commented 3 years ago

@villesundell I'm sorry, but the current state of move-prover (as for diem v1.2.0) is completely unusable and couldn't pass its own tests. Eventually we will move to more recent diem version, but until then this prove subcommand will be hidden behind an undocumented feature-gate.

Regarding your issue with panic on your taohe project - I was able to debug it and (partially) fix it. The reason is in repeating function names in script files: for some reason, prover wants unique names across all scripts and modules.