Repository navigation

Proofs for `Vec::swap_remove`, `Option::as_slice`, and `VecDeque::swap` - #212

Merged

tautschnig merged 64 commits into

model-checking:mainfrom

stogaru:usage_proofs

Dec 12, 2024

Merged

Proofs for `Vec::swap_remove`, `Option::as_slice`, and `VecDeque::swap`#212
tautschnig merged 64 commits into
model-checking:mainfrom
stogaru:usage_proofs

Commits on Oct 7, 2024
- added common codes for all proof of contracts
  xsxszab
  committed
  9a8993d
- implemented integer type proof for contract for fn add, sub and offset
  xsxszab
  committed
  55950bb
Commits on Oct 9, 2024
- Merge branch 'main' into verify/ptr_mut
  stogaru
  committed
  ce13e8f
- Adds proofs for tuple types
  stogaru
  committed
  3682858
- Renames harnesses
  stogaru
  committed
  a6d4d62
- Added unit type proofs for mut ptr
  MayureshJoshi25
  committed
  dec8c30
Commits on Oct 11, 2024
Commits on Oct 12, 2024
- Fixes a typo
  stogaru
  committed
  82345de
- Removes an unnecessary attribute
  stogaru
  committed
  656209b
- Merge pull request #9 from stogaru/verify/ptr_mut_combined
  stogaru
  authored
  46e839c
Commits on Oct 23, 2024
- refactored function contracts for add, sub and offset using the same_allocation api, modified their proof for harness accordingly
  xsxszab
  committed
  96a8a2e
- merged macros for add, sub and offset
  xsxszab
  committed
  852e96f
Commits on Oct 24, 2024
- updated function contracts and proof for contracts for add(), sub() and offset()
  xsxszab
  committed
  04bd61e
Commits on Oct 31, 2024
- added support for unit type pointers
  xsxszab
  committed
  7557fc5
Commits on Nov 6, 2024
- updated function contracts, removed unnecessary kani::assmue
  xsxszab
  committed
  76b2311
- added comments to function contracts
  xsxszab
  committed
  cb6a177
Commits on Nov 7, 2024
- Merge pull request #12 from stogaru/verify/ptr_mut_refactor_harness
  xsxszab
  authored
  6385d4a
- added comments for magic numbers
  xsxszab
  committed
  a079a7a
- Merge branch 'main' into verify/ptr_mut
  stogaru
  authored
  214f84d
Commits on Nov 15, 2024
- updated proofs using pointer generator
  xsxszab
  committed
  51ded41
- fixed typos in comments
  xsxszab
  committed
  fb6215e
- rustfmt formatting
  xsxszab
  committed
  f229fd9
- reverse unnecessary rustfmt formatting
  xsxszab
  committed
  20fffa3
Commits on Nov 16, 2024
- temporary disabled check_mut_add_u8 test
  xsxszab
  committed
  b9054a8
Commits on Nov 27, 2024
- Clarified preconditions with additional notes
  xsxszab
  committed
  b528b0e
- added tracking issue info for the pointer generator bug
  xsxszab
  committed
  9b90b23
- Merge branch 'main' into verify/ptr_mut
  tautschnig
  authored
  b3b0620
Commits on Nov 29, 2024
- Proof for VecDeque swap
  stogaru
  committed
  6dc7db5
Commits on Nov 30, 2024
- Corrects a bug in the proof.
  stogaru
  committed
  46648ac
Commits on Dec 2, 2024
- Add proof for String:remove
  szlee118
  committed
  afe1b16
Commits on Dec 3, 2024
- Use any_array at creation
  szlee118
  committed
  80b3f91
Commits on Dec 5, 2024
- align mut_ptr with usage_proofs branch
  szlee118
  committed
  6e97438
- Copied file from usage_proofs to verify/string_remove
  szlee118
  committed
  f581759
- Merge branch 'usage_proofs' into verify/string_remove
  szlee118
  committed
  5de632a
- Fix of any_where usage, hardcode constant
  szlee118
  committed
  081474e
Commits on Dec 6, 2024
- Add a newline at the end of the file
  stogaru
  committed
  9563408
- Add extra assertion and remove redundant assume
  szlee118
  committed
  51e903d
- Add description
  szlee118
  committed
  8ec384e
- Remove redundant white line
  szlee118
  committed
  ee06313
- Added proof for vec::swap_remove
  MayureshJoshi25
  committed
  160d9d7
- Update mod.rs
  stogaru
  authored
  5082a92
- Merge pull request #22 from stogaru/verify/string_remove
  stogaru
  authored
  f552676
- Merge pull request #24 from stogaru/verify/vecdeque_swap
  stogaru
  authored
  41c3927
- Merge pull request #25 from stogaru/verify/vec_swap_remove_usage_v2
  stogaru
  authored
  b42123d
- Adds a proof for Option::as_slice
  stogaru
  committed
  1851037
- Merge branch 'main' into usage_proofs
  stogaru
  authored
  b9d950c
Commits on Dec 8, 2024
- Updates challenge 3
  stogaru
  committed
  e784b5e
- Merge branch 'main' into usage_proofs
  stogaru
  authored
  e9ca2e8
Commits on Dec 9, 2024
- Merge branch 'main' into usage_proofs
  stogaru
  authored
  67d4965
- Merge branch 'main' into usage_proofs
  szlee118
  authored
  7089335
Commits on Dec 10, 2024
- Update library/alloc/src/string.rs
  
  szlee118
  and
  feliperodri
  authored
  cab796a
- Merge branch 'main' into usage_proofs
  szlee118
  authored
  6fc9d20
Commits on Dec 11, 2024
- Removes a comment
  stogaru
  committed
  33ae4f4
- Symbolic checking for remaining elements
  stogaru
  committed
  0c36fee
- Update check_remove harness with description and change array size
  szlee118
  committed
  3405ee3
- Merge branch 'usage_proofs' of https://github.com/stogaru/verify-rust-std into usage_proofs
  szlee118
  committed
  a07478d
Commits on Dec 12, 2024
- Merge branch 'main' into usage_proofs
  szlee118
  authored
  c334c96
- Removes String remove harness
  stogaru
  committed
  ed1e26e
- Merge branch 'main' into usage_proofs
  stogaru
  authored
  991a76b

Commits

Commits on Oct 7, 2024

Commits on Oct 9, 2024

Commits on Oct 11, 2024

Commits on Oct 12, 2024

Commits on Oct 23, 2024

Commits on Oct 24, 2024

Commits on Oct 31, 2024

Commits on Nov 6, 2024

Commits on Nov 7, 2024

Commits on Nov 15, 2024

Commits on Nov 16, 2024

Commits on Nov 27, 2024

Commits on Nov 29, 2024

Commits on Nov 30, 2024

Commits on Dec 2, 2024

Commits on Dec 3, 2024

Commits on Dec 5, 2024

Commits on Dec 6, 2024

Commits on Dec 8, 2024

Commits on Dec 9, 2024

Commits on Dec 10, 2024

Commits on Dec 11, 2024

Commits on Dec 12, 2024