Repository navigation

Contracts & Harnesses for `unchecked_mul` , `unchecked_sub`, `unchecked_shl` and `unchecked_shr` - #96

Merged

carolynzech merged 55 commits into

model-checking:mainfrom

rajathkotyal:c-0011-core-nums-rajathm-unsafe-ints

Oct 7, 2024

Merged

Contracts & Harnesses for `unchecked_mul` , `unchecked_sub`, `unchecked_shl` and `unchecked_shr`#96
carolynzech merged 55 commits into
model-checking:mainfrom
rajathkotyal:c-0011-core-nums-rajathm-unsafe-ints

Commits on Sep 11, 2024
- Add Kani proofs of unchecked_add for all integer types
  yew005
  committed
  1ae4c6d
- Format proof files & Add verification function templates
  yew005
  committed
  b553678
- feat: add i8 uncheck shl verification
  MWDZ
  committed
  4db34e4
- feat: add i16 and i32 uncheck shl verification
  MWDZ
  committed
  54f5507
Commits on Sep 12, 2024
- added unsafe integer i8 unchecked sub following the template
  lanfeima
  committed
  472da0e
Commits on Sep 16, 2024
- Experiment with two verification approaches in mod.rs of core::num
  yew005
  committed
  daaaf7e
Commits on Sep 18, 2024
- Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsafe-ints
  Yenyun035
  authored
  7bd0e3c
- Add contracts to unchecked_add && Add i8::unchecked_add proof
  yew005
  committed
  1c9dbde
- Format core::num mod.rs
  yew005
  committed
  894231f
- Add comment for unchecked_add proofs
  yew005
  committed
  2bc4faf
Commits on Sep 19, 2024
- Add harnesses for i16,i32,i64,i128 unchecked_add
  yew005
  committed
  d9d4b5f
- Add harnesses for u8,u16,u32,u64,u128 unchecked_add
  yew005
  committed
  07c8b4a
- Cleanup misplaced proofs
  yew005
  committed
  1fd4c6a
Commits on Sep 20, 2024
- Clean up comment
  yew005
  committed
  b360311
- Format comment
  yew005
  committed
  8cbca87
- Remove before contracts. Fix import in
  yew005
  committed
  0eef858
- Fix comment
  yew005
  committed
  4858a53
Commits on Sep 23, 2024
Commits on Sep 24, 2024
- feat: add contract and test case for unchecked_shl in type int and unit
  MWDZ
  committed
  a7d3cc2
- added preconditions and postconditions
  lanfeima
  committed
  271afad
- add proof functions for unchecked_sub
  lanfeima
  committed
  c7762c2
- Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsafe-ints
  Yenyun035
  authored
  ce35002
- Remove ensures contracts && Undo formatting on existing code
  yew005
  committed
  d99844d
- Add {isize, usize}::unchecked_add harnesses
  yew005
  committed
  fbcf49e
Commits on Sep 25, 2024
- Small fix typo
  rajathkotyal
  authored
  864afa6
Commits on Sep 27, 2024
- Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsafe-ints
  Yenyun035
  authored
  457a2b5
- Add harness generation macros for unchecked methods && Update unchecked_add harnesses
  yew005
  committed
  54a03ef
Commits on Sep 29, 2024
- added limits to multiplication proofs, reduced duplicacy in code by using macros to generate proof harnesses
  rajathkotyal
  committed
  ae678de
- Merge branch 'c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-nums-rajathm-unsafe-ints
  rajathkotyal
  authored
  af6942e
Commits on Sep 30, 2024
- Remove unused import safety::ensures
  yew005
  committed
  8ee5682
- unchecked_mul and unchecked_shr proofs (#7)
  rajathkotyal
  authored
  02d706a
- Add comments. Fix spacing
  yew005
  committed
  dce9e83
Commits on Oct 2, 2024
- Revert "Add comments. Fix spacing"
  rajathkotyal
  committed
  3880fc7
- Revert "unchecked_mul and unchecked_shr proofs (#7)"
  rajathkotyal
  committed
  781cb87
- Add comments. Fix spacing
  rajathkotyal
  committed
  500e8db
- cleaned up code: deleted the previous attempted proofs
  lanfeima
  committed
  1c97825
Commits on Oct 3, 2024
Commits on Oct 5, 2024
- add interval checks to unchecked_mul
  rajathkotyal
  committed
  49b0a6b
- Merge branch 'main' into c-0011-core-nums-rajathm-unsafe-ints
  rajathkotyal
  authored
  7118fa4
- unchecked neg fix
  rajathkotyal
  committed
  bbb9656
- add missing i8, i16 unchecked_mul
  rajathkotyal
  committed
  cafeea6
Commits on Oct 6, 2024
Commits on Oct 7, 2024

Commits

Commits on Sep 11, 2024

Commits on Sep 12, 2024

Commits on Sep 16, 2024

Commits on Sep 18, 2024

Commits on Sep 19, 2024

Commits on Sep 20, 2024

Commits on Sep 23, 2024

Commits on Sep 24, 2024

Commits on Sep 25, 2024

Commits on Sep 27, 2024

Commits on Sep 29, 2024

Commits on Sep 30, 2024

Commits on Oct 2, 2024

Commits on Oct 3, 2024

Commits on Oct 5, 2024

Commits on Oct 6, 2024

Commits on Oct 7, 2024