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

Close Challenges 6 & 14; remove optional correctness work in Challenge 12 #247

Merged
merged 23 commits into from
Mar 21, 2025
Merged

Close Challenges 6 & 14; remove optional correctness work in Challenge 12 #247

merged 23 commits into from
Mar 21, 2025

Conversation

thanhnguyen-aws
Copy link

@thanhnguyen-aws thanhnguyen-aws commented Feb 17, 2025 •
edited by carolynzech
Loading

In this PR, I refined the existing challenges by:

  • Added the missing contracts and harnesses for 3 functions write, write_bytes, write_unaligned for the NonNull challenge, then changed the status of this challenge to "resolved".
  • Edited some descriptions of smallsort
  • Removed the (optional) correctness checking in NonZero challenge.
  • Resolved the Safety of Primitive Conversions challenge.
    I don't add more functions to existing challenge to keep each challenge under manageable size. I will create other challenges for functions inside the same modules as the existing ones.

Resolves #53
Resolves #220

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

@thanhnguyen-aws thanhnguyen-aws requested a review from a team as a code owner February 17, 2025 18:11
carolynzech
carolynzech requested changes Mar 3, 2025
View reviewed changes
Copy link

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

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

I haven't reviewed the harnesses in-depth yet; focused on the contracts and other changes for now.

carolynzech
carolynzech reviewed Mar 17, 2025
View reviewed changes
@tautschnig tautschnig self-assigned this Mar 18, 2025
@tautschnig tautschnig removed their assignment Mar 18, 2025
@carolynzech carolynzech changed the title Refine challenges Close Challenges 6 & 14; remove optional correctness work in Challenge 12 Mar 21, 2025
@carolynzech carolynzech enabled auto-merge March 21, 2025 19:42
@carolynzech carolynzech added this pull request to the merge queue Mar 21, 2025
Merged via the queue into model-checking:main with commit 00169b7 Mar 21, 2025
15 of 18 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig approved these changes

@carolynzech carolynzech carolynzech approved these changes

Assignees

@carolynzech carolynzech

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Challenge 14: Safety of Primitive Conversions Challenge 6: Safety of NonNull
3 participants
@thanhnguyen-aws @tautschnig @carolynzech