milksad
/
rust-bitcoin-unsafe-fast
14
0
Fork 0
Code Issues Pull Requests Activity

Merge rust-bitcoin/rust-bitcoin#2686: Fix kani codegen CI job 

0f0bd91929 kani: Pin version to 0.48.0 (Tobin C. Harding)
5981b15902 kani: Rename tests (Tobin C. Harding)
17bacc6fb6 kani: Remove redundant import (Tobin C. Harding)

Pull request description:

  Fix the current failing Kani job on todays PRs.

  FTR our daily `kani` job has been red for ages, perhaps since we created the `units` crate? But today the `--codege-only` job broke (on all PRs). `kani` released a new version 10 days ago, pinning to the previous version seems to resolve the issue. I raised a bug report but did not investigate further.

  - Patch 1: Remove redundant import
  - Patch 2: Rename the tests
  - Patch 3: Pin kani version

  File bug report: https://github.com/model-checking/kani/issues/3142

  PR is CI only, can go in with one ack.

  (Patch 2 is the result of debugging the _real_ kani failure we have at the moment, I'll save the rant for the PR that fixes it.)

ACKs for top commit:
  apoelstra:
    ACK 0f0bd91929 though I wonder if we shoud comment out the test in rust.yml and file an issue
  sanket1729:
    utACK 0f0bd91929

Tree-SHA512: 1e510dd53f3474dd4891792e312444cec57239c865e4cd7d144932713b3ce2e66806a37b88d55ecaa514292ac936de569cc9126c773048a5a930c6c822faad29
This commit is contained in:
Andrew Poelstra 2024-04-16 19:51:45 +00:00
parent f18bd22489 0f0bd91929
commit 87b674be45
No known key found for this signature in database
GPG Key ID: C588D63CE41B97C1
2 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.github/workflows/rust.yml vendored
View File

@ -236,4 +236,5 @@ jobs:
- name: 'Kani build proofs'
uses: model-checking/kani-github-action@v1.1
with:
kani-version: '0.48.0'
args: '--only-codegen'

9
units/src/amount.rs
View File

@ -1885,7 +1885,6 @@ pub mod serde {
#[cfg(kani)]
mod verification {
use std::cmp;
use std::convert::TryInto;
use super::*;
@ -1903,7 +1902,7 @@ mod verification {
// CI it fails, so we need to set it higher.
#[kani::unwind(4)]
#[kani::proof]
fn u_amount_add_homomorphic() {
fn u_amount_homomorphic() {
let n1 = kani::any::<u64>();
let n2 = kani::any::<u64>();
kani::assume(n1.checked_add(n2).is_some()); // assume we don't overflow in the actual test
@ -1933,7 +1932,7 @@ mod verification {
#[kani::unwind(4)]
#[kani::proof]
fn u_amount_add_homomorphic_checked() {
fn u_amount_homomorphic_checked() {
let n1 = kani::any::<u64>();
let n2 = kani::any::<u64>();
assert_eq!(
@ -1948,7 +1947,7 @@ mod verification {
#[kani::unwind(4)]
#[kani::proof]
fn s_amount_add_homomorphic() {
fn s_amount_homomorphic() {
let n1 = kani::any::<i64>();
let n2 = kani::any::<i64>();
kani::assume(n1.checked_add(n2).is_some()); // assume we don't overflow in the actual test
@ -1981,7 +1980,7 @@ mod verification {
#[kani::unwind(4)]
#[kani::proof]
fn s_amount_add_homomorphic_checked() {
fn s_amount_homomorphic_checked() {
let n1 = kani::any::<i64>();
let n2 = kani::any::<i64>();
assert_eq!(