rust-bitcoin / rust-bitcoin / 7800336497

83%

push

github

Merge rust-bitcoin/rust-bitcoin#2450: kani: fix Amount overflow test

<a class=hub.com/rust-bitcoin/rust-bitcoin/commit/<a class="double-link" href="https://git"><a class=hub.com/rust-bitcoin/rust-bitcoin/commit/343510d3a017f770cdbfbaa7057c8d109773a575">343510d3a kani: fix Amount overflow test (Andrew Poelstra)

Pull request description:

  Our Kani CI job is currently failing. See https://github.com/rust-bitcoin/rust-bitcoin/actions/runs/7770495422/job/21190756253

  This fixes one of the issues; the other is that we're hitting a multiplication assertion in the test we added in https://github.com/rust-bitcoin/rust-bitcoin/pull/2393 which I'm unsure how to deal with.

  For reference, testing this was a bit of a PITA. I needed to

  ```
  # Ok, these steps are easy/obvious
  cargo install kani-verifier
  cargo kani
  ```

  This will give you an error located in core/panic.rs or something with the description `This is a placeholder message; Kani doesn't support message formatted at runtime` which is not super helpful. To get the actual failure, you need to write

  ```
  cargo kani --enable-unstable --concrete-playback=inplace
  ```

  which will add a weird unit test which calls into Kani to exercise the original test with a specific input value. Because it calls into Kani you can't just run it with `cargo test`. You need to run

  ```
  RUST_BACKTRACE=1 CARGO_INCREMENTAL=0 cargo kani playback -Z concrete-playback -- kani_concrete_playback_check_div_rem_8626518785677487871
  ```

  where `CARGO_INCREMENTAL=0` disables incremental compilation (this was causing rustc to flame out with a "filename too long" error because it was trying to create some intermediate file with multiple hashes and crate names in it), and the `kani_concrete_playback_123456789` thing is the name of the test that gets added (which you can easily find by reading `git diff`).

ACKs for top commit:
  tcharding:
    ACK 343510d3a017f770cdbfbaa7057c8d109773a575
  Kixunil:
    ACK 343510d3a017f770cdbfbaa7057c8d109773a575

Tree-SHA512: 398ce3c61b8645ec84df7e2a30bb5467660e77a... (continued)

19326 of 22967 relevant lines covered (84.15%)

16811.07 hits per line