Merge rust-bitcoin/rust-bitcoin#2430: Fix kani test

4383202f23 CI: Add a job to build kani proofs (Tobin C. Harding)
96d3bbd065 Fix kani test (Tobin C. Harding)

Pull request description:

  Recently (in #2379) we patched the `ParseAmountError` but we don't check kani code on every pull request so we broke it.

  Fix kani test to use the new `OutOfRangeError`.

  EDIT: Attempt, as a separate patch, to add a job that runs on each PR to build the kani test code.

  Close: #2424

ACKs for top commit:
  Kixunil:
    ACK 4383202f23
  apoelstra:
    ACK 4383202f23

Tree-SHA512: dcddcb0d52201efb3246733e9f164f5acde22df256fc4985b23050628ab9ae9c20a80ecd4ab468558b0a8708dacf6f7af099e8303cf4f73e1557e454c351aa34
This commit is contained in:
Andrew Poelstra 2024-02-01 13:53:36 +00:00
commit 05e21a2f39
No known key found for this signature in database
GPG Key ID: C588D63CE41B97C1
2 changed files with 15 additions and 1 deletions

View File

@ -163,3 +163,14 @@ jobs:
env: env:
DO_WASM: true DO_WASM: true
run: cd hashes && ./contrib/test.sh run: cd hashes && ./contrib/test.sh
Kani:
runs-on: ubuntu-20.04
steps:
- name: 'Checkout your code.'
uses: actions/checkout@v4
- name: 'Kani build proofs'
uses: model-checking/kani-github-action@v1.1
with:
args: '--only-codegen'

View File

@ -1755,7 +1755,10 @@ mod verification {
if n1 >= 0 { if n1 >= 0 {
Ok(Amount::from_sat(n1.try_into().unwrap())) Ok(Amount::from_sat(n1.try_into().unwrap()))
} else { } else {
Err(ParseAmountError::Negative) Err(OutOfRangeError {
is_signed: true,
is_greater_than_max: false
})
}, },
); );
} }