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 and Harnesses for <*const T>::add, sub and offset #166

Merged
merged 61 commits into from
Dec 3, 2024
Merged

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

merged 61 commits into from
Dec 3, 2024

Conversation

xsxszab
Copy link

@xsxszab xsxszab commented Nov 15, 2024

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.

szlee118 and others added 30 commits September 12, 2024 18:34
@szlee118
Add verification contract for *const T::add and *const T::add
500f249
@xsxszab
Update const_ptr.rs
99701ff
@stogaru
Merge branch 'model-checking:main' into test
31c82a9
@stogaru
Changes generic type to i32 in proof.
f84b7a6 
Refactors by removing unused crates and importing safety crate
@szlee118
Remove unneeded file
a839820
added comments for function contracts and harnesses
21e0ab8
@stogaru
Merge branch 'main' into verify/ptr_const_offset
b54ce9e
@xsxszab
reverted library code format change and removed unnecessary comments
0c0078f
@xsxszab
added macros for verifying all integer types for offset and add
a192129
@xsxszab
implemented function contract and integer type proofs for fn sub
2ef5923
@szlee118
Add verification of slice type proofs for fn offset
f1602aa
@xsxszab
add TODOs for proof for contracts
1b467d5
@xsxszab
verified *mut T::offset for all integer types
9461027
@szlee118
Add verification of slice type proofs for fn add and sub
159137b
@szlee118
Remove commented code
df56d18
@xsxszab
removed unnecessary comments
eab0a15
@xsxszab
reverted changes to mut_ptr.rs
e07040f
@xsxszab
removed necessary comments
0ff52b5
@xsxszab
aligned format for mut_ptr.rs
ccd5c3c
@xsxszab
aligned format for mut_ptr.rs
180a276
@xsxszab
Merge pull request #1 from stogaru/verify/ptr_const_integer_types
6a85e3e 
Verify/ptr const integer types
@xsxszab
Merge branch 'model-checking:main' into verify/ptr_const_offset
6853284
@stogaru
Adds proofs for composite type - tuple
fb79caf
@stogaru
Change function proof names
7d05c96
@stogaru
Merge pull request #2 from stogaru/verify/ptr_const_composite
8e49dcd 
Adds proofs for composite type - tuple
@szlee118
Merge branch 'verify/ptr_const_offset' into verify/ptr_const_slice_type
9af0e39
@szlee118
Merge pull request #4 from stogaru/verify/ptr_const_slice_type
31532c9 
Verify/ptr const slice type
@MayureshJoshi25
Added changes for *const T::add & *const::sub verifying unit type
f9f5371
@MayureshJoshi25
Updated proofs for const ptr (unit type)
eab900e
@stogaru
Merge branch 'verify/ptr_const' into verify/ptr_const_unit_type
05c0fdd
@feliperodri feliperodri removed their assignment Nov 27, 2024
@feliperodri
Copy link

@xsxszab could you solve the conflicts?

@szlee118
Copy link

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

@szlee118 szlee118 mentioned this pull request Nov 28, 2024
Merged
feliperodri
feliperodri reviewed Nov 28, 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
library/core/src/ptr/const_ptr.rs Outdated Show resolved Hide resolved
library/core/src/ptr/const_ptr.rs Outdated Show resolved Hide resolved
tautschnig
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
feliperodri
feliperodri approved these changes Dec 3, 2024
View reviewed changes
library/core/src/ptr/const_ptr.rs Outdated Show resolved Hide resolved
@xsxszab xsxszab mentioned this pull request Dec 3, 2024
Merged
@tautschnig tautschnig enabled auto-merge (squash) December 3, 2024 14:20
@tautschnig tautschnig merged commit d0d9de2 into model-checking:main Dec 3, 2024
9 checks passed
tautschnig pushed a commit that referenced this pull request Dec 4, 2024
@xsxszab
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@celinval celinval celinval left review comments

@szlee118 szlee118 szlee118 left review comments

@feliperodri feliperodri feliperodri approved these changes

@Eh2406 Eh2406 Eh2406 left review comments

@tautschnig tautschnig tautschnig approved these changes

Assignees

@xsxszab xsxszab

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
8 participants
@xsxszab @stogaru @feliperodri @szlee118 @tautschnig @Eh2406 @celinval @MayureshJoshi25