core_models/abstractions/mod.rs
1//! This module provides abstractions that are useful for writting
2//! specifications in minicore. Currently it provides two abstractions: bits and
3//! bit vectors.
4//!
5//! # Examples
6//!
7//! Converting an integer to a bit vector and back:
8//!
9//! ```rust
10//! use core_models::abstractions::{bit::{Bit, MachineInteger}, bitvec::BitVec};
11//!
12//! // Create a BitVec from a machine integer (using the integer's bit-width)
13//! let bv = BitVec::<16>::from_int(42u16);
14//! println!("BitVec: {:?}", bv);
15//!
16//! // Convert the BitVec back into a machine integer
17//! let n: u16 = bv.to_int();
18//! println!("Integer: {}", n);
19//!
20//! assert!(n == 42);
21//! ```
22
23pub mod bit;
24pub mod bitvec;
25pub mod funarr;