Panicked at 'could not find instance', creusot/src/translation/function/terminator.rs:143:22

[cmester0]

I get the following error message, when running cargo creusot in the concordium-contracts-common crate located Concordium/concordium-contracts-common.

warning: load the `creusot_contract` crate to enable resolution of mutable borrows.

module 
  use Ref
  use mach.int.Int
  use mach.int.Int32
  use mach.int.Int64
  use mach.int.UInt32
  use mach.int.UInt64
  use string.Char
  use floating_point.Single
  use floating_point.Double
  use prelude.Prelude
  type core_marker_phantomdata 't = 
    | Core_Marker_PhantomData

  type creusotcontracts_logic_ghost 't = 
    | CreusotContracts_Logic_Ghost (core_marker_phantomdata 't)

end
module 
  type t   
  use prelude.Prelude
  use Type
  val record (_1 : t) : Type.creusotcontracts_logic_ghost t
end
module 
  type t   
  use prelude.Prelude
  use Type
  let rec cfg record (_1 : t) : Type.creusotcontracts_logic_ghost t = 
  {
    goto BB0
  }

end
thread 'rustc' panicked at 'could not find instance', creusot/src/translation/function/terminator.rs:143:22
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

note: Creusot has panic-ed!
  |
  = note: Oops, that shouldn't have happened, sorry about that.
  = note: Please report this bug over here: https://github.com/xldenis/creusot/issues/new

error: could not compile `concordium-contracts-common`; 1 warning emitted

[xldenis]

Hi @cmester0,

Thanks for reporting this bug, could you do a few things for me please?

1. What SHA of creusot are you using?
2. Can you ensure creusot contracts is compiled properly by running cargo test --test ui "zzz" (yes, I know...)?
3. If all else fails can you try using the mlcfg script in the root of creusot? Point it at your lib.rs and let me know what happens.

[cmester0]

I am using the most reason SHA (eb3ddaae090910afe78db80bb1a0499966892c8c). Test results in

cargo test --test ui "zzz"
    Finished test [unoptimized + debuginfo] target(s) in 0.42s
     Running tests/ui.rs (target/debug/deps/ui-87458c1491cc6535)

[cmester0]

mlcfg results in a bunch of errors:

./mlcfg ../concordium-rust-smart-contracts/concordium-contracts-common/src/lib.rs 
    Finished dev [unoptimized + debuginfo] target(s) in 0.02s
     Running `target/debug/creusot-rustc -Zno-codegen --extern creusot_contracts=./target/debug/libcreusot_contracts.rlib -Ldependency=./target/debug/deps/ --crate-type=lib /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/lib.rs`
error[E0432]: unresolved import `hash`
 --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/impls.rs:8:5
  |
8 | use hash::Hash;
  |     ^^^^ help: a similar path exists: `self::hash`

error[E0432]: unresolved import `cmp`
 --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:6:5
  |
6 | use cmp::Ordering;
  |     ^^^ help: a similar path exists: `self::cmp`

error[E0432]: unresolved import `hash`
 --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:9:5
  |
9 | use hash::Hash;
  |     ^^^^ help: a similar path exists: `self::hash`

error[E0432]: unresolved import `collections`
 --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/impls.rs:5:5
  |
5 | use collections::{BTreeMap, BTreeSet};
  |     ^^^^^^^^^^^ help: a similar path exists: `self::collections`

error[E0432]: unresolved import `collections`
  --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/schema.rs:11:5
   |
11 | use collections::{BTreeMap, BTreeSet};
   |     ^^^^^^^^^^^ help: a similar path exists: `self::collections`

error: cannot determine resolution for the derive macro `Hash`
  --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:29:62
   |
29 | #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
   |                                                              ^^^^
   |
   = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:322:62
    |
322 | #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
    |                                                              ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:448:62
    |
448 | #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
    |                                                              ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:584:62
    |
584 | #[derive(Eq, PartialEq, Copy, Clone, PartialOrd, Ord, Debug, Hash)]
    |                                                              ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:597:62
    |
597 | #[derive(Eq, PartialEq, Copy, Clone, Debug, PartialOrd, Ord, Hash)]
    |                                                              ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:667:45
    |
667 | #[derive(Eq, PartialEq, Copy, Clone, Debug, Hash)]
    |                                             ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:714:32
    |
714 | #[derive(Eq, PartialEq, Debug, Hash)]
    |                                ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:770:45
    |
770 | #[derive(Eq, PartialEq, Copy, Clone, Debug, Hash)]
    |                                             ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:815:39
    |
815 | #[derive(Eq, PartialEq, Debug, Clone, Hash)]
    |                                       ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:853:45
    |
853 | #[derive(Eq, PartialEq, Debug, Clone, Copy, Hash)]
    |                                             ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:887:39
    |
887 | #[derive(Eq, PartialEq, Debug, Clone, Hash)]
    |                                       ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:915:45
    |
915 | #[derive(Eq, PartialEq, Debug, Clone, Copy, Hash)]
    |                                             ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error: cannot determine resolution for the derive macro `Hash`
   --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:919:39
    |
919 | #[derive(Eq, PartialEq, Debug, Clone, Hash)]
    |                                       ^^^^
    |
    = note: import resolution is stuck, try simplifying macro imports

error[E0433]: failed to resolve: use of undeclared crate or module `fnv`
  --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:17:28
   |
17 | pub type HashMap<K, V, S = fnv::FnvBuildHasher> = hashbrown::HashMap<K, V, S>;
   |                            ^^^ use of undeclared crate or module `fnv`

error[E0433]: failed to resolve: use of undeclared crate or module `hashbrown`
  --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:17:51
   |
17 | pub type HashMap<K, V, S = fnv::FnvBuildHasher> = hashbrown::HashMap<K, V, S>;
   |                                                   ^^^^^^^^^ use of undeclared crate or module `hashbrown`

error[E0433]: failed to resolve: use of undeclared crate or module `fnv`
  --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:21:25
   |
21 | pub type HashSet<K, S = fnv::FnvBuildHasher> = hashbrown::HashSet<K, S>;
   |                         ^^^ use of undeclared crate or module `fnv`

error[E0433]: failed to resolve: use of undeclared crate or module `hashbrown`
  --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:21:48
   |
21 | pub type HashSet<K, S = fnv::FnvBuildHasher> = hashbrown::HashSet<K, S>;
   |                                                ^^^^^^^^^ use of undeclared crate or module `hashbrown`

warning: unused import: `collections`
 --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/impls.rs:4:25
  |
4 | use alloc::{boxed::Box, collections, string::String, vec::Vec};
  |                         ^^^^^^^^^^^
  |
  = note: `#[warn(unused_imports)]` on by default

warning: unused import: `hash`
 --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/impls.rs:7:12
  |
7 | use core::{hash, marker, mem::MaybeUninit, slice};
  |            ^^^^

warning: unused import: `collections`
  --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/schema.rs:10:13
   |
10 | use alloc::{collections, string::String, vec::Vec};
   |             ^^^^^^^^^^^

warning: unused import: `cmp`
 --> /home/au538501/Documents/concordium-rust-smart-contracts/concordium-contracts-common/src/types.rs:8:12
  |
8 | use core::{cmp, convert, fmt, hash, iter, ops, str};
  |            ^^^

error: aborting due to 22 previous errors; 4 warnings emitted

Some errors have detailed explanations: E0432, E0433.
For more information about an error, try `rustc --explain E0432`.

[cmester0]

I fixed all the issues by doing the changes recommended by the error messages. It seems that it needs to reference self before it is satisfied with the use path?

[xldenis]

that may be because ./mlcfg doesn't do a lot of the magic that cargo does around crates. I'll need to look into why cargo creusot wasn't working.

[xldenis]

Are you sure that cargo creusot was built on the latest version? The error message doesn't line up with the code properly:

thread 'rustc' panicked at 'could not find instance', creusot/src/translation/function/terminator.rs:143:22

[cmester0]

It works with cargo after changing the use paths from eg. hash::Hash to self::hash::Hash.

[cmester0]

Yes, I made sure to clean, and build from the latest commit before reporting. The misalignment seems strange.

[xldenis]

I built cargo-creusot locally as well using cargo install creusot --path creusot and I was able to translate all of the crate above except for one error on:

Note: Simply building (cargo build) won't update cargo-creusot.

error[creusot]: Pointer casts are currently unsupported
   --> src/traits.rs:138:77
    |
138 |     fn write_u8(&mut self, x: u8) -> Result<(), Self::Err> { self.write_all(&x.to_le_bytes()) }
    |                                                                             ^^^^^^^^^^^^^^^^

error: could not compile `concordium-contracts-common` due to previous error; 1 warning emitted

Doing so required two changes:

1. Set the rust-toolchain to the same as creusot. This is inevitable due to how rustc_private crates work.
2. Add creusot_contracts as a dependency to the concordium contracts crate. This is how cargo creusot distinguishes between crates that are interesting to translate and ones that arent.

[xldenis]

I'm currently working my way through the relevant errors by marking functions as #[trusted].

[xldenis]

Ok! I have the precise set of steps to get the crate as close to compiling as is currently possible with creusot.

1. Install cargo-creusot using cargo install creusot --path creusot.
2. Add a dependency on creusot-contracts, and a feature contracts which enables the creusot-contracts/contracts feature.
3. cargo clean and CREUSOT_CONTINUE=1 cargo creusot --features=contracts.

[xldenis]

I'm quite unhappy with the experience of this process, but that's just the result of creusot having no external users.