Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Contracts & Harnesses for unchecked_add #91

Merged
merged 27 commits into from
Oct 4, 2024
Merged

Contracts & Harnesses for unchecked_add #91

merged 27 commits into from
Oct 4, 2024

Commits on Sep 11, 2024

  1. Add Kani proofs of unchecked_add for all integer types

    yew005 committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    1ae4c6d View commit details
    Browse the repository at this point in the history

  2. Format proof files & Add verification function templates

    yew005 committed Sep 11, 2024
    Configuration menu
    Copy the full SHA
    b553678 View commit details
    Browse the repository at this point in the history

Commits on Sep 16, 2024

  1. Experiment with two verification approaches in mod.rs of core::num

    yew005 committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    daaaf7e View commit details
    Browse the repository at this point in the history

Commits on Sep 18, 2024

  1. Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsa… 

    …fe-ints
    @Yenyun035
    Yenyun035 authored Sep 18, 2024
    Configuration menu
    Copy the full SHA
    7bd0e3c View commit details
    Browse the repository at this point in the history

  2. Add contracts to unchecked_add && Add i8::unchecked_add proof

    yew005 committed Sep 18, 2024
    Configuration menu
    Copy the full SHA
    1c9dbde View commit details
    Browse the repository at this point in the history

  3. Format core::num mod.rs

    yew005 committed Sep 18, 2024
    Configuration menu
    Copy the full SHA
    894231f View commit details
    Browse the repository at this point in the history

  4. Add comment for unchecked_add proofs

    yew005 committed Sep 18, 2024
    Configuration menu
    Copy the full SHA
    2bc4faf View commit details
    Browse the repository at this point in the history

Commits on Sep 19, 2024

  1. Add harnesses for i16,i32,i64,i128 unchecked_add

    yew005 committed Sep 19, 2024
    Configuration menu
    Copy the full SHA
    d9d4b5f View commit details
    Browse the repository at this point in the history

  2. Add harnesses for u8,u16,u32,u64,u128 unchecked_add

    yew005 committed Sep 19, 2024
    Configuration menu
    Copy the full SHA
    07c8b4a View commit details
    Browse the repository at this point in the history

  3. Cleanup misplaced proofs

    yew005 committed Sep 19, 2024
    Configuration menu
    Copy the full SHA
    1fd4c6a View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2024

  1. Clean up comment

    yew005 committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    b360311 View commit details
    Browse the repository at this point in the history

  2. Format comment

    yew005 committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    8cbca87 View commit details
    Browse the repository at this point in the history

  3. Remove before contracts. Fix import in

    yew005 committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    0eef858 View commit details
    Browse the repository at this point in the history

  4. Fix comment

    yew005 committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    4858a53 View commit details
    Browse the repository at this point in the history

Commits on Sep 23, 2024

  1. Merge branch 'main' into c-0011-core-nums-yenyunw-unsafe-ints

    @Yenyun035
    Yenyun035 authored Sep 23, 2024
    Configuration menu
    Copy the full SHA
    483bdf5 View commit details
    Browse the repository at this point in the history

Commits on Sep 24, 2024

  1. Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsa… 

    …fe-ints
    @Yenyun035
    Yenyun035 authored Sep 24, 2024
    Configuration menu
    Copy the full SHA
    ce35002 View commit details
    Browse the repository at this point in the history

  2. Remove ensures contracts && Undo formatting on existing code

    yew005 committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    d99844d View commit details
    Browse the repository at this point in the history

  3. Add {isize, usize}::unchecked_add harnesses

    yew005 committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    fbcf49e View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2024

  1. Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsa… 

    …fe-ints
    @Yenyun035
    Yenyun035 authored Sep 27, 2024
    Configuration menu
    Copy the full SHA
    457a2b5 View commit details
    Browse the repository at this point in the history

  2. Add harness generation macros for unchecked methods && Update uncheck… 

    …ed_add harnesses
    yew005 committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    54a03ef View commit details
    Browse the repository at this point in the history

Commits on Sep 30, 2024

  1. Remove unused import safety::ensures

    yew005 committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    8ee5682 View commit details
    Browse the repository at this point in the history

  2. unchecked_mul and unchecked_shr proofs (#7) 

    * Added harnesses for unchecked multiplication (`unchecked_mul`) and shift right (`unchecked_shr`)
* Added a macro and input limits for multiplication proofs
* Reduced duplicity in code by using macros to generate proof harnesses
    @rajathkotyal
    rajathkotyal authored Sep 30, 2024
    Configuration menu
    Copy the full SHA
    02d706a View commit details
    Browse the repository at this point in the history

  3. Add comments. Fix spacing

    yew005 committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    dce9e83 View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2024

  1. Revert "Add comments. Fix spacing" 

    This reverts commit dce9e83.
    @rajathkotyal
    rajathkotyal committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    3880fc7 View commit details
    Browse the repository at this point in the history

  2. Revert "unchecked_mul and unchecked_shr proofs (#7)" 

    This reverts commit 02d706a.
    @rajathkotyal
    rajathkotyal committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    781cb87 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'main' into c-0011-core-nums-yenyunw-unsafe-ints

    @Yenyun035
    Yenyun035 authored Oct 2, 2024
    Configuration menu
    Copy the full SHA
    715e940 View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2024

  1. Change generate_unchecked_neg_harness macro

    yew005 committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    a3bf6d1 View commit details
    Browse the repository at this point in the history