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

343510d3a0 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 343510d3a0
  Kixunil:
    ACK 343510d3a0

Tree-SHA512: 398ce3c61ffa3246bd27ae5719b4ac4fda587e87b8645ec8418fdfd039e4ed78d58233faab27bc63df7e2a30bb5467660e77a6e3d3a08fe86e7ff3dd31869ec7
This commit is contained in:
Andrew Poelstra 2024-02-05 23:01:55 +00:00
commit 06dc05c55b
No known key found for this signature in database
GPG Key ID: C588D63CE41B97C1
1 changed files with 1 additions and 1 deletions

View File

@ -1704,7 +1704,7 @@ mod verification {
if n1 <= i64::MAX as u64 {
Ok(SignedAmount::from_sat(n1.try_into().unwrap()))
} else {
Err(ParseAmountError::OutOfRange(OutOfRangeError::too_big(false)))
Err(ParseAmountError::OutOfRange(OutOfRangeError::too_big(true)))
},
);
}