core_models/abstractions/
bit.rs

1//! # Bit Manipulation and Machine Integer Utilities
2//!
3//! This module provides utilities for working with individual bits and machine integer types.
4//! It defines a [`Bit`] enum to represent a single bit (`0` or `1`) along with convenient
5//! conversion implementations between `Bit`, [`bool`], and various primitive integer types.
6//!
7//! In addition, the module introduces the [`MachineInteger`] trait which abstracts over
8//! integer types, providing associated constants:
9//!
10//! - `BITS`: The size of the integer type in bits.
11//! - `SIGNED`: A flag indicating whether the type is signed.
12//!
13//! The [`Bit`] type includes methods for extracting the value of a specific bit from an integer.
14//! For example, [`Bit::of_int`] returns the bit at a given position for a provided integer,
15//! handling both positive and negative values (assuming a two's complement representation).
16//!
17//! # Examples
18//!
19//! ```rust
20//! use core_models::abstractions::bit::{Bit, MachineInteger};
21//!
22//! // Extract the 3rd bit (0-indexed) from an integer.
23//! let bit = Bit::of_int(42, 2);
24//! println!("The extracted bit is: {:?}", bit);
25//!
26//! // Convert Bit to a primitive integer type.
27//! let num: u8 = bit.into();
28//! println!("As an integer: {}", num);
29//! ```
30//!
31//! [`bool`]: https://doc.rust-lang.org/std/primitive.bool.html
32//! [`Bit::of_int`]: enum.Bit.html#method.of_int
33
34/// Represent a bit: `0` or `1`.
35#[derive(Copy, Clone, Eq, PartialEq, Debug)]
36pub enum Bit {
37    Zero,
38    One,
39}
40
41macro_rules! generate_from_bit_impls {
42    ($($ty:ident),*) => {
43        $(impl From<Bit> for $ty {
44            fn from(bit: Bit) -> Self {
45                bool::from(bit) as $ty
46            }
47        })*
48    };
49}
50generate_from_bit_impls!(u8, u16, u32, u64, u128, i8, i16, i32, i64, i128);
51
52impl From<Bit> for bool {
53    fn from(bit: Bit) -> Self {
54        match bit {
55            Bit::Zero => false,
56            Bit::One => true,
57        }
58    }
59}
60
61impl From<bool> for Bit {
62    fn from(b: bool) -> Bit {
63        match b {
64            false => Bit::Zero,
65            true => Bit::One,
66        }
67    }
68}
69
70/// A trait for types that represent machine integers.
71#[hax_lib::attributes]
72pub trait MachineInteger {
73    /// The size of this integer type in bits.
74    #[hax_lib::requires(true)]
75    #[hax_lib::ensures(|bits| bits >= 8)]
76    fn bits() -> u32;
77
78    /// The signedness of this integer type.
79    const SIGNED: bool;
80}
81
82macro_rules! generate_machine_integer_impls {
83    ($($ty:ident),*) => {
84        $(#[hax_lib::exclude]impl MachineInteger for $ty {
85            fn bits() -> u32 { $ty::BITS }
86            #[allow(unused_comparisons)]
87            const SIGNED: bool = $ty::MIN < 0;
88        })*
89    };
90}
91generate_machine_integer_impls!(u8, u16, u32, u64, u128, i8, i16, i32, i64, i128);
92
93#[hax_lib::fstar::replace(
94    r"
95instance impl_MachineInteger_poly (t: inttype): t_MachineInteger (int_t t) =
96  { f_bits = (fun () -> mk_u32 (bits t));
97    f_bits_pre = (fun () -> True);
98    f_bits_post = (fun () r -> r == mk_u32 (bits t));
99    f_SIGNED = signed t }
100"
101)]
102const _: () = {};
103
104#[hax_lib::exclude]
105impl Bit {
106    fn of_raw_int(x: u128, nth: u32) -> Self {
107        if x / 2u128.pow(nth) % 2 == 1 {
108            Self::One
109        } else {
110            Self::Zero
111        }
112    }
113
114    pub fn of_int<T: Into<i128> + MachineInteger>(x: T, nth: u32) -> Bit {
115        let x: i128 = x.into();
116        if x >= 0 {
117            Self::of_raw_int(x as u128, nth)
118        } else {
119            Self::of_raw_int((2i128.pow(T::bits()) + x) as u128, nth)
120        }
121    }
122}
core_models/abstractions/bit.rs

core_models/abstractions/
bit.rs
