Skip to content

Conversation

btj
Copy link

@btj btj commented Jul 24, 2025

Adds a VeriFast solution for challenge 19 (RawVec).

Note: this proof does not prove semantic well-typedness of the non-unsafe RawVecInner methods listed in the challenge, because they do not satisfy any meaningful kind of semantic well-typedness; see the discussion at #283.

Resolves #283

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

@btj btj requested a review from a team as a code owner July 24, 2025 05:12
Copy link
Member

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

Approving having reviewed VeriFast's internal library specs (with comments in verifast/verifast#863).

@tautschnig
Copy link
Member

@btj Please add to this PR a commit that marks the challenge as resolved in doc/src/challenges/0019-rawvec.md (cf. #224 for how this was done for challenge 9).

@tautschnig tautschnig added this pull request to the merge queue Aug 14, 2025
Merged via the queue into model-checking:main with commit f66ba41 Aug 14, 2025
26 checks passed
@btj btj deleted the verifast-raw-vec branch August 14, 2025 19:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

5 participants