feat(specs): helixdb and chrono axiomatic stubs and ingestion sepcs

[liamjdavis]

This pull request introduces a robust framework for specifying and verifying code that depends on external libraries in the erdos-graph project. It establishes a pattern for creating abstract stub types and axiomatic wrappers for third-party dependencies, and demonstrates this approach for chrono, helix_db, and ingestion-related types. The PR also adds detailed specifications and verification checks for date range chunking and checkpoint logic. The most important changes are grouped below.

Documentation and Patterns for External Library Stubbing:

• Expanded CONTRIBUTING.md with a detailed guide on how to create and use abstract stub types for external libraries, including directory layout, step-by-step instructions, common pitfalls, and when to use open spec fn vs. uninterp spec fn. [1] [2] [3]

Axiomatic Stubs for External Libraries:

• Added verified/src/axioms/chrono_stubs.rs with abstract representations and specifications for chrono::DateTime and chrono::Duration, including ordering and arithmetic operations, and basic proof lemmas.
• Added verified/src/axioms/helix_db.rs with an abstract type for the Helix graph engine and uninterpreted spec functions for node and edge counts, along with an external constructor and verification check.
• Added verified/src/axioms/ingestion_types.rs with abstract stubs for publication records and ingestion config, including uninterpreted predicates for string fields and open spec functions for validity.
• Registered all new axiom modules in verified/src/axioms/mod.rs.

Specification and Verification of Ingestion Logic:

• Added verified/src/ingestion_specs.rs with axiomatic wrappers for checkpoint logic and chunking date ranges, including detailed postconditions capturing coverage, contiguity, ordering, and edge cases. Includes proof lemmas and a suite of verification checks for these properties.

Integration and Module Registration:

• Registered new modules in verified/src/lib.rs to make axioms and ingestion specifications available throughout the crate.…ingestion specs