specs(thread_safe_queue): producer registration and unregistration with concurrency

[liamjdavis]

This pull request significantly expands and clarifies the documentation and verification approach for the Erdos Graph engine, focusing on formal verification practices with Verus. It adds a detailed explanation of the differences between formal verification and testing, introduces a style guide and naming conventions, outlines which Verus features are usable given the external code constraints, and provides many new and improved property-based proofs for the ThreadSafeQueue API.

The most important changes are:

Documentation and Guidelines:

• Expanded CONTRIBUTING.md to clearly distinguish between formal verification and testing, including purpose, structure, and writing approach, with illustrative examples.
• Added comprehensive guidelines on which Verus features can and cannot be used when verifying external Rust code, including recommended workarounds and patterns for specifying and verifying properties.
• Introduced a style guide covering naming conventions for proof functions, concise commenting practices, and usage of uninterpreted spec functions and external type specifications.

Verification Patterns and Examples:

• Added detailed examples to CONTRIBUTING.md of properties that can be verified (sequential behavior, functional correctness, limited concurrency properties) and those that cannot (true concurrency, deadlock freedom, liveness), with concrete proof sketches for ThreadSafeQueue.

Property-Based Proofs and Specs:

• In verified/src/thread_safe_queue_specs.rs, introduced uninterpreted spec functions and exec wrappers for key ThreadSafeQueue operations (active_producer_count, producers_finished, queue_size), and added external type specifications for opaque types.
• Added a comprehensive suite of property-based proof functions verifying behaviors such as producer registration/unregistration, state transitions, state isolation, sequential consistency, and atomicity for the queue API.

Code and Comment Style Improvements:

• Refactored comments and function names throughout the verification code to follow the new concise style guide, replacing verbose explanations with short, clear phrases and consistent naming (e.g., check_*, verify_*).

These changes make the verification process more robust, maintainable, and accessible for contributors.