elicitation_kani 0.11.1

//! Kani formal verification proofs for elicitation contracts.
//!
//! This crate contains 386 proof harnesses verifying contract invariants
//! using the Kani model checker's symbolic execution engine.
//!
//! # Architecture
//!
//! Kani proofs are organized by type category:
//! - **Primitives**: strings, integers, floats, chars, bools
//! - **Collections**: Vec, HashMap, HashSet, arrays, tuples
//! - **DateTime**: chrono, time, jiff DateTime types
//! - **Network**: IP addresses, MAC addresses, socket addresses
//! - **External**: URLs, UUIDs, regex, paths
//! - **Mechanisms**: Contract composition and verification
//! - **Third-party**: clap, sqlx, tokio, egui, UI typestate types
//!
//! # Running Proofs
//!
//! ```bash
//! # All proofs (386 harnesses)
//! cargo kani -p elicitation_kani --all-features
//!
//! # Specific module
//! cargo kani -p elicitation_kani --harness verify_string_non_empty
//!
//! # With specific features
//! cargo kani -p elicitation_kani --features uuid,url
//! ```
//!
//! # Proof Strategy
//!
//! For each contract type T, we prove:
//! 1. **Construction Safety**: `T::new(x)` succeeds ⟹ invariant holds
//! 2. **Invalid Rejection**: `T::new(x)` fails ⟹ invariant violated
//! 3. **Accessor Correctness**: `t.get()` returns validated value
//! 4. **Unwrap Correctness**: `t.into_inner()` returns validated value
//!
//! # Global Configuration
//!
//! Run with global unwind bound to prevent memchr infinite loops:
//! ```bash
//! cargo kani -p elicitation_kani --all-features -- --default-unwind 20
//! ```

// Harness helper utilities (bounded_string, bounded_vec, kani_arbitrary!)
pub mod harness_helpers;

// Re-export verification framework from main crate
pub use elicitation::verification::Contract;
#[cfg(not(creusot))]
pub use elicitation::verification::WithContract;
pub use elicitation::verification::contracts;

// Proof modules (organized by type category)
#[cfg(kani)]
mod bools;
#[cfg(kani)]
mod chars;
#[cfg(kani)]
mod collections;
#[cfg(kani)]
mod durations;
#[cfg(kani)]
mod errors;
#[cfg(kani)]
mod floats;
#[cfg(kani)]
mod integers;
#[cfg(kani)]
mod ipaddr_bytes;
#[cfg(kani)]
mod macaddr;
#[cfg(kani)]
mod mechanisms;
#[cfg(kani)]
mod networks;
#[cfg(kani)]
mod socketaddr;
#[cfg(kani)]
mod strings;
#[cfg(kani)]
mod systemtime;
#[cfg(kani)]
mod unit;
#[cfg(kani)]
mod utf8;

// Test whether manual tracing span injection survives Kani DFCC
#[cfg(kani)]
mod tracing_span_test;

// Feature-gated proof modules
#[cfg(all(kani, unix))]
mod pathbytes;

#[cfg(all(kani, feature = "uuid"))]
mod uuid_bytes;

#[cfg(all(kani, feature = "url"))]
mod urlbytes;
#[cfg(all(kani, feature = "url"))]
mod urls;

// Serde boundary consistency proofs (require verification + serde_json)
#[cfg(all(kani, feature = "serde_json"))]
mod serde_boundary;

#[cfg(all(kani, feature = "regex"))]
mod regexbytes;
#[cfg(all(kani, feature = "regex"))]
mod regexes;

#[cfg(all(kani, feature = "chrono"))]
mod datetimes_chrono;

#[cfg(all(kani, feature = "time"))]
mod datetimes_time;

#[cfg(all(kani, feature = "jiff"))]
mod datetimes_jiff;

#[cfg(all(kani, feature = "clap-types"))]
mod clap_types;

#[cfg(all(kani, feature = "sqlx-types"))]
mod sqlx_types;

#[cfg(all(kani, feature = "tokio-types"))]
mod tokio_types;

#[cfg(all(kani, feature = "egui-types"))]
mod egui_types;

#[cfg(all(kani, feature = "ratatui"))]
mod ratatui_types;

#[cfg(all(kani, feature = "geo-types"))]
mod geo_types;

#[cfg(all(kani, feature = "georaster-types"))]
mod georaster_types;

#[cfg(all(kani, feature = "geojson-types"))]
mod geojson_types;

#[cfg(all(kani, feature = "rstar-types"))]
mod rstar_types;

#[cfg(all(kani, feature = "proj-types"))]
mod proj_types;

#[cfg(all(kani, feature = "wkt-types"))]
mod wkt_types;

#[cfg(all(kani, feature = "wkb-types"))]
mod wkb_types;

#[cfg(all(kani, feature = "winit-types"))]
mod winit_types;

#[cfg(all(kani, feature = "wgpu-types"))]
mod wgpu_types;

#[cfg(all(kani, feature = "palette"))]
mod palette_types;

#[cfg(all(kani, feature = "ui-types"))]
mod ui_types;

// Vec trust-boundary empirical investigation
#[cfg(kani)]
mod vec_boundary;

// Synthetic diagnostic theories for BTreeMap/HashMap drop-glue in enums
#[cfg(kani)]
mod diag;