Skip to content

specs(thread safe queue): trivial specs for existence#1

Merged
liamjdavis merged 1 commit intomainfrom
liamjdavis/trivial-thread-safe-queue-proofs
Feb 4, 2026
Merged

specs(thread safe queue): trivial specs for existence#1
liamjdavis merged 1 commit intomainfrom
liamjdavis/trivial-thread-safe-queue-proofs

Conversation

@liamjdavis
Copy link
Contributor

This pull request adds new specs to ensure correct behavior of the QueueConfig struct in the thread-safe queue module. The main focus is on verifying the Clone implementation and direct construction of the config.

Tests and verification improvements:

  • Added clone_queue_config spec to verify that cloning a QueueConfig preserves the max_queue_size field, along with a proof function check_clone_config to assert this behavior.
  • Added check_construct_config spec to verify that a QueueConfig can be constructed directly with a specified max_queue_size, and that the value is correctly set.

@liamjdavis liamjdavis merged commit 82c8404 into main Feb 4, 2026
1 check passed
@liamjdavis liamjdavis deleted the liamjdavis/trivial-thread-safe-queue-proofs branch February 4, 2026 22:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant