Contracts and Harnesses for `<*const T>::add`, `sub` and `offset` by xsxszab · Pull Request #166 · model-checking/verify-rust-std

xsxszab · 2024-11-15T05:04:00Z

Towards #76

Summary

Adds contracts for <*const T>::add, sub and offset.
Adds proof for contracts for above methods, verifying following pointee types:
- All integer types
- Tuples (representing composite types)
- Slices
- Unit type

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

Refactors by removing unused crates and importing safety crate

Verify/ptr const integer types

Adds proofs for composite type - tuple

Verify/ptr const slice type

feliperodri · 2024-11-28T03:21:55Z

@xsxszab could you solve the conflicts?

szlee118 · 2024-11-28T04:12:11Z

@feliperodri Conflicts resolved, and I removed the comment stating performance reason improperly.

library/core/src/ptr/const_ptr.rs

…plication.

… integer, composite and unit types verification

library/core/src/ptr/const_ptr.rs

…tion; Rearranged proofs

…et` (#203) **Summary** This PR synchronizes updates from PR #166 and applies them to `mut` function contracts and proof for contracts.

szlee118 and others added 30 commits September 12, 2024 18:34

Add verification contract for *const T::add and *const T::add

500f249

Update const_ptr.rs

99701ff

Merge branch 'model-checking:main' into test

31c82a9

Changes generic type to i32 in proof.

f84b7a6

Refactors by removing unused crates and importing safety crate

Remove unneeded file

a839820

added comments for function contracts and harnesses

21e0ab8

Merge branch 'main' into verify/ptr_const_offset

b54ce9e

reverted library code format change and removed unnecessary comments

0c0078f

added macros for verifying all integer types for offset and add

a192129

implemented function contract and integer type proofs for fn sub

2ef5923

Add verification of slice type proofs for fn offset

f1602aa

add TODOs for proof for contracts

1b467d5

verified *mut T::offset for all integer types

9461027

Add verification of slice type proofs for fn add and sub

159137b

Remove commented code

df56d18

removed unnecessary comments

eab0a15

reverted changes to mut_ptr.rs

e07040f

removed necessary comments

0ff52b5

aligned format for mut_ptr.rs

ccd5c3c

aligned format for mut_ptr.rs

180a276

Merge pull request #1 from stogaru/verify/ptr_const_integer_types

6a85e3e

Verify/ptr const integer types

Merge branch 'model-checking:main' into verify/ptr_const_offset

6853284

Adds proofs for composite type - tuple

fb79caf

Change function proof names

7d05c96

Merge pull request #2 from stogaru/verify/ptr_const_composite

8e49dcd

Adds proofs for composite type - tuple

Merge branch 'verify/ptr_const_offset' into verify/ptr_const_slice_type

9af0e39

Merge pull request #4 from stogaru/verify/ptr_const_slice_type

31532c9

Verify/ptr const slice type

Added changes for *const T::add & *const::sub verifying unit type

f9f5371

Updated proofs for const ptr (unit type)

eab900e

Merge branch 'verify/ptr_const' into verify/ptr_const_unit_type

05c0fdd

feliperodri removed their assignment Nov 27, 2024

xsxszab added 2 commits November 26, 2024 22:49

Reformatted code using rustfmt.

5edd16e

Reverted unnecessary rustfmt formatting

dd2a8eb

Merge branch 'main' into verify/ptr_const

7b83329

szlee118 mentioned this pull request Nov 28, 2024

Harnesses verifying slice types for add, sub and offset #179

Merged

xsxszab added 2 commits November 28, 2024 09:54

Resolved compilation error after previous merge.

576483f

Enhanced comments to clarify proof for contracts.

330f06b

tautschnig unassigned xsxszab Nov 28, 2024

feliperodri reviewed Nov 28, 2024

View reviewed changes

xsxszab added 5 commits November 28, 2024 19:10

Refactored macro for generating slice type verifications to reduce du…

43a456b

…plication.

Fixed proof naming issue in previous commit; Refactored the macro for…

90fc86a

… integer, composite and unit types verification

Formatted code using rustfmt.

9a2ee76

Fixed function naming issues after refactoring.

d783dac

Fixed issues in comments

d7ee4d0

tautschnig approved these changes Dec 1, 2024

View reviewed changes

library/core/src/ptr/const_ptr.rs Outdated Show resolved Hide resolved

library/core/src/ptr/const_ptr.rs Outdated Show resolved Hide resolved

library/core/src/ptr/const_ptr.rs Outdated Show resolved Hide resolved

Refactored contracts to improve performance

6ee7941

feliperodri approved these changes Dec 3, 2024

View reviewed changes

library/core/src/ptr/const_ptr.rs Outdated Show resolved Hide resolved

feliperodri assigned xsxszab Dec 3, 2024

celinval reviewed Dec 3, 2024

View reviewed changes

library/core/src/ptr/const_ptr.rs Outdated Show resolved Hide resolved

xsxszab added 3 commits December 2, 2024 21:05

Replaced kani::mem::same_allocation with core::ub_checks::same_alloca…

0573c74

…tion; Rearranged proofs

Rearranged proofs, moving the unit type proof to the top

81afaf9

Refactored function contracts for better readability.

36ef494

xsxszab mentioned this pull request Dec 3, 2024

Refactor Contracts and Harnesses for <*mut T>::add, sub and offset #203

Merged

Merge branch 'main' into verify/ptr_const

b213847

tautschnig approved these changes Dec 3, 2024

View reviewed changes

tautschnig enabled auto-merge (squash) December 3, 2024 14:20

tautschnig merged commit d0d9de2 into model-checking:main Dec 3, 2024

tautschnig pushed a commit that referenced this pull request Dec 4, 2024

Refactor Contracts and Harnesses for <*mut T>::add, sub and `offs…

2338dad

…et` (#203) **Summary** This PR synchronizes updates from PR #166 and applies them to `mut` function contracts and proof for contracts.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Contracts and Harnesses for `<*const T>::add`, `sub` and `offset`#166

Contracts and Harnesses for `<*const T>::add`, `sub` and `offset`#166
tautschnig merged 61 commits intomodel-checking:mainfrom
stogaru:verify/ptr_const

xsxszab commented Nov 15, 2024

Uh oh!

feliperodri commented Nov 28, 2024

Uh oh!

szlee118 commented Nov 28, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

Conversation

xsxszab commented Nov 15, 2024

Uh oh!

feliperodri commented Nov 28, 2024

Uh oh!

szlee118 commented Nov 28, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants