Kani panicked in codegen/rvalue

[TomMD]

thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:1317:9:error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:1317:9:
                                assertion `left == right` failed
                                  left: 48
                                 right: 41.


assertion `left == right` failed
  left: 48
 right: 41
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: <der::error::Error as std::fmt::Debug>::fmt
_RNvXs9_NtCslefA7hYQHvl_3der5errorNtB5_5ErrorNtNtCscBmSNMcqgUz_4core3fmt5Debug3fmtCsg8FMlfzrjoY_7rslip10
[Kani] current codegen location: Loc { file: "$HOME/.cargo/registry/src/index.crates.io-6f17d22bba15001f/der-0.7.9/src/error.rs", function: None, start_line: 18, start_col: Some(23), end_line: 18, end_col: Some(28) }
error: could not compile `rslip10` (lib test)
error: Failed to compile `rslip10` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:1317:9:
                                assertion `left == right` failed
                                  left: 48
                                 right: 41.

This is when running cargo kani --package my_package --tests and, evidently, kani has an issue with the latest der crate.

[TomMD]

I've tried to reproduce this or similar failing without the my_package and with just der but failed.

If the above failure is not sufficient for understanding the problem then let's close this ticket, there just isn't time to make a minimum reproducer on my side at this time.

[adpaco]

Hi @TomMD , thanks for the bug report!

I haven't been able to reproduce this issue using the examples in the der documentation because they don't compile for me (i.e., the example here). I'll try looking for more examples later but it'd be really helpful if you could share some more information.

We don't need the reproducer to be minimal, but can you at least share with us what APIs from der you were using? Are you using any features from that crate? My understanding is the rslip10 method is a test function you're defining. But if you were, for example, just deriving the Encode and Decode impls it shouldn't be too hard to write a reproducer on our own.

[TomMD]

@adpaco-aws Well that's far too engaging of a response for me to not make a reproducer. This is short in code but very much not minimal since it uses a larger, upstream, library which might actually be a bit different than der all together.

Cargo.toml:

[package]
name = "bip32-kani"
version = "0.1.0"
edition = "2021"

[dependencies]
bip32 = "0.5.1"

src/lib.rs:

#[cfg(kani)]
mod proofs {
    use bip32::XPrv;

    #[kani::proof]
    fn demonstrate_kani_bug() {
        let seed1: [u8;32] = kani::any();
        let seed2: [u8;32] = kani::any();
        let xpriv1 = XPrv::new(&seed1[..]).unwrap();
        let xpriv2 = XPrv::new(&seed2[..]).unwrap();
        let child_index: bip32::ChildNumber = bip32::ChildNumber(kani::any());
        let child1 = xpriv1.derive_child(child_index).unwrap().to_string(bip32::Prefix::XPRV);
        let child2 = xpriv2.derive_child(child_index).unwrap().to_string(bip32::Prefix::XPRV);
        assert_eq!(child1, child2);
    }
}

(the property is obviously bogus, I'm just triggering the bug with this code)

Execution:

$ cargo kani
Kani Rust Verifier 0.52.0 (cargo plugin)
   Compiling bip32-kani v0.1.0 ($HOME/dev/bip32-kani)
thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:1317:9:
assertion `left == right` failederror: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:1317:9:
                                assertion `left == right` failed
                                  left: 48
                                 right: 41.


  left: 48
 right: 41
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: <der::error::Error as std::fmt::Debug>::fmt
_RNvXs9_NtCs7kgvvemOeEF_3der5errorNtB5_5ErrorNtNtCscBmSNMcqgUz_4core3fmt5Debug3fmtCs7P5cwQHAw26_10bip32_kani
[Kani] current codegen location: Loc { file: "$HOME/.cargo/registry/src/index.crates.io-6f17d22bba15001f/der-0.7.9/src/error.rs", function: None, start_line: 18, start_col: Some(23), end_line: 18, end_col: Some(28) }
error: could not compile `bip32-kani` (lib)
error: Failed to compile `bip32_kani` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:1317:9:
                                assertion `left == right` failed
                                  left: 48
                                 right: 41.

[adpaco]

Hey @TomMD , thanks so much for taking the time to submit a reproducer!

I'm able to confirm that Kani crashes with this code. It's not a problem if it uses other dependencies, for now we just need something to trigger the failure for debugging purposes. We will take it from here! 😄

[zhassan-aws]

This is a duplicate of #2857 (same crash signature).