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

Added <dyn Trait> Proof for Contracts for byte_add, byte_sub, and byte_offset #188

Merged
merged 33 commits into from
Dec 9, 2024
Merged

Added <dyn Trait> Proof for Contracts for byte_add, byte_sub, and byte_offset #188

merged 33 commits into from
Dec 9, 2024

Conversation

xsxszab
Copy link

@xsxszab xsxszab commented Nov 27, 2024 •
edited
Loading

Towards #76

This pull request impelments proof for contracts for byte_add, byte_sub and byte_offset for <dyn Trait>. Both const and mut versions are included.

It serves as an addition to an existing PR but is submitted separately to avoid disrupting the ongoing review process for that PR.

stogaru and others added 19 commits November 14, 2024 14:53
@stogaru
Adds contracts for byte_add, byte_sub and byte_offset
0ccf81e 
- Also adds proofs verifying unit, int and composite types.
@stogaru
Removes unnecessary rustfmt formnatting
aec0394
@stogaru
Adds comment for amgic numbers
60ba93e
@stogaru
Adds some comments
57c591f
@stogaru
Adds slice harnesses
a02ed87
@stogaru
Adds contracts for byte_offset, byte_add and byte_sub
2fdebd6 
- Adds harnesses for int, unit, composite and slice types
@stogaru
Runs rustfmt
cd0a134
@stogaru
Merge branch 'main' into verify/ptr_mut_byte
4aa89da
@stogaru
Merge branch 'main' into verify/ptr_mut_byte
fdfad2c
@stogaru
Some refactoring
40eb29d
@stogaru
Refactors the function contracts
81fe7c9
@stogaru
Merge branch 'main' into verify/ptr_const_byte
bee4503
@stogaru
Merge branch 'main' into verify/ptr_mut_byte
52963f7
@stogaru
Merge branch 'main' into verify/ptr_const_byte
38066e1
@stogaru
Merge branch 'verify/ptr_const_byte' into verify/ptr_mut_byte
2d32b07
@stogaru
Addresses commennts on PR
5e4f616
@stogaru
Merge branch 'main' into verify/ptr_mut_byte
dea6e0e
@xsxszab
Implemented proof for contracts for dyn trait for byte_add, byte_sub …
7e979cb 
…and byte_offset
@xsxszab
Reverted unnecessary changes to minimize conflict.
c98d839
@xsxszab xsxszab marked this pull request as ready for review November 27, 2024 08:07
@xsxszab xsxszab requested a review from a team as a code owner November 27, 2024 08:07
@feliperodri feliperodri self-assigned this Nov 27, 2024
@tautschnig
Copy link
Member

@xsxszab Please resolve conflicts.

tautschnig
tautschnig approved these changes 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/mut_ptr.rs Outdated Show resolved Hide resolved
library/core/src/ptr/mut_ptr.rs Outdated Show resolved Hide resolved
library/core/src/ptr/mut_ptr.rs Outdated Show resolved Hide resolved
library/core/src/ptr/mut_ptr.rs Outdated Show resolved Hide resolved
@xsxszab xsxszab marked this pull request as draft November 29, 2024 05:29
feliperodri
feliperodri requested changes Dec 5, 2024
View reviewed changes
Copy link

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some clean up is required before merging it.

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/mut_ptr.rs Outdated Show resolved Hide resolved
library/core/src/ptr/mut_ptr.rs Outdated Show resolved Hide resolved
library/core/src/ptr/mut_ptr.rs Outdated Show resolved Hide resolved
@xsxszab xsxszab marked this pull request as ready for review December 6, 2024 01:07
@xsxszab
Copy link
Author

xsxszab commented Dec 6, 2024 •
edited
Loading

Please Note that PR #168 mistakenly removed mut proofs for unit, integer and composite types for add, sub and offset. The changes have been reverted as part of this PR during merging.

@feliperodri feliperodri enabled auto-merge (squash) December 6, 2024 05:24
feliperodri
feliperodri approved these changes Dec 7, 2024
View reviewed changes
Copy link

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

trigger review

@feliperodri feliperodri removed their assignment Dec 8, 2024
@stogaru stogaru mentioned this pull request Dec 8, 2024
Merged
auto-merge was automatically disabled December 9, 2024 17:41

Head branch was pushed to by a user without write access

feliperodri
feliperodri approved these changes Dec 9, 2024
View reviewed changes
Copy link

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

@feliperodri feliperodri enabled auto-merge (squash) December 9, 2024 18:51
@feliperodri feliperodri merged commit 6077459 into model-checking:main Dec 9, 2024
9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@stogaru stogaru stogaru left review comments

@ayrustogaru ayrustogaru ayrustogaru left review comments

@feliperodri feliperodri feliperodri approved these changes

@tautschnig tautschnig tautschnig approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@xsxszab @tautschnig @feliperodri @ayrustogaru @stogaru