core_models/
lib.rs

1//! `core-models`: A Rust Model for the `core` Library
2//!
3//! `core-models` is a simplified, self-contained model of Rust’s `core` library. It aims to provide
4//! a purely Rust-based specification of `core`'s fundamental operations, making them easier to
5//! understand, analyze, and formally verify. Unlike `core`, which may rely on platform-specific
6//! intrinsics and compiler magic, `core-models` expresses everything in plain Rust, prioritizing
7//! clarity and explicitness over efficiency.
8//!
9//! ## Key Features
10//!
11//! - **Partial Modeling**: `core-models` includes only a subset of `core`, focusing on modeling
12//!   fundamental operations rather than providing a complete replacement.
13//! - **Exact Signatures**: Any item that exists in both `core-models` and `core` has the same type signature,
14//!   ensuring compatibility with formal verification efforts.
15//! - **Purely Functional Approach**: Where possible, `core-models` favors functional programming principles,
16//!   avoiding unnecessary mutation and side effects to facilitate formal reasoning.
17//! - **Explicit Implementations**: Even low-level operations, such as SIMD, are modeled explicitly using
18//!   Rust constructs like bit arrays and partial maps.
19//! - **Extra Abstractions**: `core-models` includes additional helper types and functions to support
20//!   modeling. These extra items are marked appropriately to distinguish them from `core` definitions.
21//!
22//! ## Intended Use
23//!
24//! `core-models` is designed as a reference model for formal verification and reasoning about Rust programs.
25//! By providing a readable, well-specified version of `core`'s behavior, it serves as a foundation for
26//! proof assistants and other verification tools.
27
28// This recursion limit is necessary for macro `core-models::core_arch::x86::interpretations::int_vec::tests::mk!`.
29// We test functions with const generics, the macro generate a test per possible (const generic) control value.
30#![recursion_limit = "2048"]
31pub mod abstractions;
32pub mod core_arch;
33
34pub use core_arch as arch;
35
36pub mod helpers;