Contracts & Harnesses for unchecked_add

[Yenyun035]

Resolves #59

Changes

• Added contracts for unchecked_add (located in library/core/src/num/int_macros.rs and uint_macros.rs)
• Added a harness for unchecked_add of each integer type
  • i8, i16, i32, i64, i128, isize, u8, u16, u32, u64, u128, usize --- 12 harnesses in total.

Revalidation

1. Per the discussion in Challenge 11: Safety of Methods for Numeric Primitive Types #59, we have to build and run Kani from feature/verify-rust-std branch.
2. To revalidate the verification results, run the following command. <harness_to_run> can be either num::verify to run all harnesses or num::verify::<harness_name> (e.g. check_unchecked_add_i8) to run a specific harness.

kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates

Except isize and usize harnesses passing 1203 checks, all harnesses should pass the same 1229 checks (1200 checks on 09/24/2024):

SUMMARY:
 ** 0 of 1229 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 2.4755886s

Complete - 10 successfully verified harnesses, 0 failures, 10 total.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

That's awesome! Thanks

Have you tried using a macro for generating the harness? I think it will be cleaner, but not a requirement.

[Yenyun035]

I haven't tried withproc_macro. I'll look into it. Thank you for reviewing this PR :)

[celinval]

I haven't tried withproc_macro. I'll look into it. Thank you for reviewing this PR :)

Sorry, my bad. I meant just regular macros

[Yenyun035]

Sorry, my bad. I meant just regular macros

Do you mean "declarative macros"? How could it be used? I guess the macro can take the method to verify and the input type (e.g. i8, i16). I'm not familiar with it. I'll research it more.

[Yenyun035]

@feliperodri @celinval Hello! The previous build failed due to an unused import. I fixed that and all looks good now. Could you approve the workflow? Once it passes the checks, we'll get this PR merged. Thank you :)

[danielhumanmod]

Hi @Yenyun035, I am the member of AWS team 4, after our team merge the main branch with this commit, there is a compiling error happens, like:

error: Failed to resolve checking function i8 :: unchecked_add because Kani currently cannot resolve path including primitive types
    --> /Users/danieltu/Developer/verify-rust-std/library/core/src/num/mod.rs:1596:13
     |
1596 |             #[kani::proof_for_contract($type::$method)]
     |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
...
1645 |     generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8);
     |     ----------------------------------------------------------------------------- in this macro invocation
     |
     = note: this error originates in the attribute macro `kani::proof_for_contract` which comes from the expansion of the macro `generate_unchecked_math_harness` (in Nightly builds, run with -Z macro-backtrace for more info)

I was wondering if this changes using some custom version of Kani?

[QinyuanWu]

Hi @Yenyun035, I am the member of AWS team 4, after our team merge the main branch with this commit, there is a compiling error happens, like:

error: Failed to resolve checking function i8 :: unchecked_add because Kani currently cannot resolve path including primitive types
    --> /Users/danieltu/Developer/verify-rust-std/library/core/src/num/mod.rs:1596:13
     |
1596 |             #[kani::proof_for_contract($type::$method)]
     |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
...
1645 |     generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8);
     |     ----------------------------------------------------------------------------- in this macro invocation
     |
     = note: this error originates in the attribute macro `kani::proof_for_contract` which comes from the expansion of the macro `generate_unchecked_math_harness` (in Nightly builds, run with -Z macro-backtrace for more info)

I was wondering if this changes using some custom version of Kani?

We tried using the -Z macro-backtrace flag but it's not supported in our installed kani version:

error: invalid value 'macro-backtrace' for '--unstable <UNSTABLE_FEATURE>'
  [possible values: stubbing, gen-c, c-ffi, concrete-playback, async-lib, source-coverage, function-contracts, mem-predicates, valid-value-checks, ghost-state, uninit-checks, unstable-options]
which kani
/Users/owo/.cargo/bin/kani

This compilation error prevents us from running any individual harnesses in the library.
@zhassan-aws @feliperodri

[Yenyun035]

@QinyuanWu @danielhumanmod Hi. Regarding your question about kani, yes. In our case, we need to manually build kani from source (features/verify-rust-std branch) to run proofs because the current kani release (installed via cargo install) does not support resolving paths with primitive types. This was discussed in our Challenge Issue #59. Here are our steps to build kani from source:

Build from source code

1. Clone the repo: git clone https://github.com/model-checking/kani.git
2. Cd into kani repo
3. git submodule update --init
4. Install dependencies: ./scripts/setup/macos/install_deps.sh
   • If failed on XCode CLT: try remove and reinstall OR see system settings > software update
   • If you want to Install dependencies manually on MacOS
     • (latest) brew install cbmc
     • (latest) CBMC-viewer
     • Kissat: Run kani/scripts/setup/install_kissat.sh
5. source $HOME/.cargo/env
6. git checkout features/verify-rust-std
7. cargo build-dev
8. For all Kani commands, run with {path/to/kani/repo}/scripts/kani