Code

Harnesses for carrying_mul#114

Code

Merged

celinval merged 61 commits intomodel-checking:mainmodel-checking/verify-rust-std:mainfrom rajathkotyal:c-0011-core-nums-lanfeim-carrying-mulrajathkotyal/verify-rust-std:c-0011-core-nums-lanfeim-carrying-mulCopy head branch name to clipboardOct 26, 2024

+80-4

Commits

Commits on Sep 11, 2024

• Add Kani proofs of unchecked_add for all integer types

  

  yew005

  committed
  1ae4c6d

  Copy full SHA for 1ae4c6d

• Format proof files & Add verification function templates

  

  yew005

  committed
  b553678

  Copy full SHA for b553678

• feat: add i8 uncheck shl verification

  MWDZ

  committed
  4db34e4

  Copy full SHA for 4db34e4

• feat: add i16 and i32 uncheck shl verification

  MWDZ

  committed
  54f5507

  Copy full SHA for 54f5507

Commits on Sep 12, 2024

• added unsafe integer i8 unchecked sub following the template

  lanfeima

  committed
  472da0e

  Copy full SHA for 472da0e

Commits on Sep 16, 2024

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

  

  yew005

  committed
  daaaf7e

  Copy full SHA for daaaf7e

Commits on Sep 18, 2024

• Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsafe-ints

  Yenyun035

  authored
  7bd0e3c

  Copy full SHA for 7bd0e3c

• Add contracts to unchecked_add && Add i8::unchecked_add proof

  

  yew005

  committed
  1c9dbde

  Copy full SHA for 1c9dbde

• Format core::num mod.rs

  

  yew005

  committed
  894231f

  Copy full SHA for 894231f

• Add comment for unchecked_add proofs

  

  yew005

  committed
  2bc4faf

  Copy full SHA for 2bc4faf

Commits on Sep 19, 2024

• Add harnesses for i16,i32,i64,i128 unchecked_add

  

  yew005

  committed
  d9d4b5f

  Copy full SHA for d9d4b5f

• Add harnesses for u8,u16,u32,u64,u128 unchecked_add

  

  yew005

  committed
  07c8b4a

  Copy full SHA for 07c8b4a

• Cleanup misplaced proofs

  

  yew005

  committed
  1fd4c6a

  Copy full SHA for 1fd4c6a

Commits on Sep 20, 2024

• Clean up comment

  

  yew005

  committed
  b360311

  Copy full SHA for b360311

• Format comment

  

  yew005

  committed
  8cbca87

  Copy full SHA for 8cbca87

• Remove before contracts. Fix import in

  

  yew005

  committed
  0eef858

  Copy full SHA for 0eef858

• Fix comment

  

  yew005

  committed
  4858a53

  Copy full SHA for 4858a53

Commits on Sep 23, 2024

• Merge remote-tracking branch 'origin/c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-nums-junfengj-unchecked-shl

  MWDZ

  committed
  8ce3381

  Copy full SHA for 8ce3381

• unchecked multiplication and shift right

  rajathkotyal

  committed
  bbd75f7

  Copy full SHA for bbd75f7

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

  Yenyun035

  authored
  483bdf5

  Copy full SHA for 483bdf5

• Merge branch 'c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-nums-lanfeima-unsafe-ints

  lanfeima

  committed
  71ffd37

  Copy full SHA for 71ffd37

Commits on Sep 24, 2024

• feat: add contract and test case for unchecked_shl in type int and unit

  MWDZ

  committed
  a7d3cc2

  Copy full SHA for a7d3cc2

• added preconditions and postconditions

  lanfeima

  committed
  271afad

  Copy full SHA for 271afad

• add proof functions for unchecked_sub

  lanfeima

  committed
  c7762c2

  Copy full SHA for c7762c2

• Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsafe-ints

  Yenyun035

  authored
  ce35002

  Copy full SHA for ce35002

• Remove ensures contracts && Undo formatting on existing code

  

  yew005

  committed
  d99844d

  Copy full SHA for d99844d

• Add {isize, usize}::unchecked_add harnesses

  

  yew005

  committed
  fbcf49e

  Copy full SHA for fbcf49e

Commits on Sep 25, 2024

• Small fix typo

  rajathkotyal

  authored
  864afa6

  Copy full SHA for 864afa6

Commits on Sep 27, 2024

• Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsafe-ints

  Yenyun035

  authored
  457a2b5

  Copy full SHA for 457a2b5

• Add harness generation macros for unchecked methods && Update unchecked_add harnesses

  

  yew005

  committed
  54a03ef

  Copy full SHA for 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

  Copy full SHA for ae678de

• Merge branch 'c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-nums-rajathm-unsafe-ints

  rajathkotyal

  authored
  af6942e

  Copy full SHA for af6942e

Commits on Sep 30, 2024

• Remove unused import safety::ensures

  

  yew005

  committed
  8ee5682

  Copy full SHA for 8ee5682

• unchecked_mul and unchecked_shr proofs (#7)

  Show description for 02d706a
  rajathkotyal

  authored
  02d706a

  Copy full SHA for 02d706a

• Add comments. Fix spacing

  

  yew005

  committed
  dce9e83

  Copy full SHA for dce9e83

Commits on Oct 2, 2024

• Revert "Add comments. Fix spacing"

  Show description for 3880fc7
  rajathkotyal

  committed
  3880fc7

  Copy full SHA for 3880fc7

• Revert "unchecked_mul and unchecked_shr proofs (#7)"

  Show description for 781cb87
  rajathkotyal

  committed
  781cb87

  Copy full SHA for 781cb87

• Add comments. Fix spacing

  rajathkotyal

  committed
  500e8db

  Copy full SHA for 500e8db

• cleaned up code: deleted the previous attempted proofs

  lanfeima

  committed
  1c97825

  Copy full SHA for 1c97825

Commits on Oct 3, 2024

• Merge branch 'c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-nums-lanfeima-unsafe-ints, TODO: need to handle the mod.rs conflict

  lanfeima

  committed
  4572831

  Copy full SHA for 4572831

• feat: merge the latest version

  MWDZ

  committed
  e3eb365

  Copy full SHA for e3eb365

• feat: use macro rules for unchecked_shl harness

  MWDZ

  committed
  2b3771f

  Copy full SHA for 2b3771f

• Merge branch 'c-0011-core-nums-junfengj-unchecked-shl' into c-0011-core-nums-rajathm-unsafe-ints

  MWDZ

  committed
  1a3bf40

  Copy full SHA for 1a3bf40

Commits on Oct 5, 2024

• add interval checks to unchecked_mul

  rajathkotyal

  committed
  49b0a6b

  Copy full SHA for 49b0a6b

• Merge branch 'main' into c-0011-core-nums-rajathm-unsafe-ints

  rajathkotyal

  authored
  7118fa4

  Copy full SHA for 7118fa4

• unchecked neg fix

  rajathkotyal

  committed
  bbb9656

  Copy full SHA for bbb9656

• add missing i8, i16 unchecked_mul

  rajathkotyal

  committed
  cafeea6

  Copy full SHA for cafeea6

Commits on Oct 6, 2024

• Merge branch 'c-0011-core-nums-rajathm-unsafe-ints' into c-0011-core-nums-lanfeima-unsafe-ints

  lanfeima

  committed
  51745e0

  Copy full SHA for 51745e0

• deleted the postconditions of unchecked_sub

  lanfeima

  committed
  7f4421c

  Copy full SHA for 7f4421c

• deleted the postconditions for the unchecked_sub in uint_macros

  lanfeima

  committed
  1331a77

  Copy full SHA for 1331a77

• refacted uncheck_sub harnesses

  lanfeima

  committed
  c413cac

  Copy full SHA for c413cac

Commits on Oct 11, 2024

• updated the branch with the main repository

  lanfeima

  committed
  8ce4a40

  Copy full SHA for 8ce4a40

• Add carrying_mul verification harnesses for u8, u16, u32, and u64

  lanfeima

  committed
  059dc02

  Copy full SHA for 059dc02

• updated the macro args for carrying_mult with initial carrying value

  lanfeima

  committed
  29ea0ce

  Copy full SHA for 29ea0ce

Commits on Oct 15, 2024

• resolved the compile error for carrying_mul

  lanfeima

  committed
  6f7deae

  Copy full SHA for 6f7deae

• deleted the kani submodule for merge

  lanfeima

  committed
  ad031a1

  Copy full SHA for ad031a1

• formatted the style

  lanfeima

  committed
  ddabe95

  Copy full SHA for ddabe95

Commits on Oct 18, 2024

• Added documentation for generate_carrying_mul_intervals macro

  lanfeima

  committed
  27522b4

  Copy full SHA for 27522b4

Commits on Oct 19, 2024

• added full range interval for u8 and u16

  lanfeima

  committed
  604d746

  Copy full SHA for 604d746

Commits on Oct 20, 2024

• reduced the interval for carrying_mul u32,u64

  lanfeima

  committed
  71399d8

  Copy full SHA for 71399d8

Commits on Oct 25, 2024

• Merge branch 'main' into c-0011-core-nums-lanfeim-carrying-mul

  rajathkotyal

  authored
  1253264

  Copy full SHA for 1253264