Skip to content

Commit e72512f

Browse files
satiscugcatsatiscugcat
committed
Removing hax dependencies
1 parent c72c1ca commit e72512f

File tree

4 files changed

+11
-95
lines changed

4 files changed

+11
-95
lines changed

‎testable-simd-models/Cargo.toml‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ readme = "README.md"
1010

1111
[dependencies]
1212
rand = "0.9"
13-
hax-lib = { git = "https://github.com/cryspen/hax/" }
1413
pastey = "0.1.0"
1514

1615
[lints.rust]

‎testable-simd-models/src/abstractions/bit.rs‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -107,12 +107,8 @@ impl From<bool> for Bit {
107107
}
108108

109109
/// A trait for types that represent machine integers.
110-
111-
#[hax_lib::attributes]
112110
pub trait MachineInteger {
113111
/// The size of this integer type in bits.
114-
#[hax_lib::requires(true)]
115-
#[hax_lib::ensures(|bits| bits >= 8)]
116112
fn bits() -> u32;
117113

118114
/// The signedness of this integer type.
@@ -188,7 +184,7 @@ macro_rules! generate_umachine_integer_impls {
188184
generate_imachine_integer_impls!(i8, i16, i32, i64, i128);
189185
generate_umachine_integer_impls!(u8, u16, u32, u64, u128);
190186

191-
#[hax_lib::exclude]
187+
192188
impl Bit {
193189
fn of_raw_int(x: u128, nth: u32) -> Self {
194190
if x / 2u128.pow(nth) % 2 == 1 {

‎testable-simd-models/src/abstractions/bitvec.rs‎

Lines changed: 7 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,6 @@ use super::funarr::*;
44

55
use std::fmt::Formatter;
66

7-
// This is required due to some hax-lib inconsistencies with versus without `cfg(hax)`.
8-
#[cfg(hax)]
9-
use hax_lib::{int, ToInt};
107

118
// TODO: this module uses `u128/i128` as mathematic integers. We should use `hax_lib::int` or bigint.
129

@@ -20,12 +17,10 @@ use hax_lib::{int, ToInt};
2017
/// The [`Debug`] implementation for `BitVec` pretty-prints the bits in groups of eight,
2118
/// making the bit pattern more human-readable. The type also implements indexing,
2219
/// allowing for easy access to individual bits.
23-
#[hax_lib::fstar::before("noeq")]
2420
#[derive(Copy, Clone, Eq, PartialEq)]
2521
pub struct BitVec<const N: u64>(FunArray<N, Bit>);
2622

27-
/// Pretty prints a bit slice by group of 8
28-
#[hax_lib::exclude]
23+
/// Pretty prints a bit slice by group of 8#[hax_lib::exclude]
2924
fn bit_slice_to_string(bits: &[Bit]) -> String {
3025
bits.iter()
3126
.map(|bit| match bit {
@@ -41,24 +36,23 @@ fn bit_slice_to_string(bits: &[Bit]) -> String {
4136
.into()
4237
}
4338

44-
#[hax_lib::exclude]
39+
4540
impl<const N: u64> core::fmt::Debug for BitVec<N> {
4641
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), std::fmt::Error> {
4742
write!(f, "{}", bit_slice_to_string(&self.0.as_vec()))
4843
}
4944
}
5045

51-
#[hax_lib::attributes]
46+
5247
impl<const N: u64> core::ops::Index<u64> for BitVec<N> {
5348
type Output = Bit;
54-
#[requires(index < N)]
5549
fn index(&self, index: u64) -> &Self::Output {
5650
self.0.get(index)
5751
}
5852
}
5953

6054
/// Convert a bit slice into an unsigned number.
61-
#[hax_lib::exclude]
55+
6256
fn u128_int_from_bit_slice(bits: &[Bit]) -> u128 {
6357
bits.iter()
6458
.enumerate()
@@ -67,7 +61,6 @@ fn u128_int_from_bit_slice(bits: &[Bit]) -> u128 {
6761
}
6862

6963
/// Convert a bit slice into a machine integer of type `T`.
70-
#[hax_lib::exclude]
7164
fn int_from_bit_slice<T: TryFrom<i128> + MachineInteger + Copy>(bits: &[Bit]) -> T {
7265
debug_assert!(bits.len() <= T::bits() as usize);
7366
let result = if T::SIGNED {
@@ -87,27 +80,6 @@ fn int_from_bit_slice<T: TryFrom<i128> + MachineInteger + Copy>(bits: &[Bit]) ->
8780
};
8881
n
8982
}
90-
91-
macro_rules! impl_pointwise {
92-
($n:literal, $($i:literal)*) => {
93-
impl BitVec<$n> {
94-
pub fn pointwise(self) -> Self {
95-
Self::from_fn(|i| match i {
96-
$($i => self[$i],)*
97-
_ => unreachable!(),
98-
})
99-
}
100-
}
101-
};
102-
}
103-
104-
impl_pointwise!(128, 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127);
105-
impl_pointwise!(256, 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255);
106-
107-
/// An F* attribute that indiquates a rewritting lemma should be applied
108-
pub const REWRITE_RULE: () = {};
109-
110-
#[hax_lib::exclude]
11183
impl<const N: u64> BitVec<N> {
11284
/// Constructor for BitVec. `BitVec::<N>::from_fn` constructs a bitvector out of a function that takes usizes smaller than `N` and produces bits.
11385
pub fn from_fn<F: Fn(u64) -> Bit>(f: F) -> Self {
@@ -148,26 +120,21 @@ impl<const N: u64> BitVec<N> {
148120
}
149121
}
150122

151-
#[hax_lib::attributes]
123+
152124
impl<const N: u64> BitVec<N> {
153-
#[hax_lib::requires(CHUNK > 0 && CHUNK.to_int() * SHIFTS.to_int() == N.to_int())]
125+
154126
pub fn chunked_shift<const CHUNK: u64, const SHIFTS: u64>(
155127
self,
156128
shl: FunArray<SHIFTS, i128>,
157129
) -> BitVec<N> {
158-
#[hax_lib::requires(CHUNK > 0 && CHUNK.to_int() * SHIFTS.to_int() == N.to_int())]
130+
159131
fn chunked_shift<const N: u64, const CHUNK: u64, const SHIFTS: u64>(
160132
bitvec: BitVec<N>,
161133
shl: FunArray<SHIFTS, i128>,
162134
) -> BitVec<N> {
163135
BitVec::from_fn(|i| {
164136
let nth_bit = i % CHUNK;
165137
let nth_chunk = i / CHUNK;
166-
hax_lib::assert_prop!(nth_chunk.to_int() <= SHIFTS.to_int() - int!(1));
167-
hax_lib::assert_prop!(
168-
nth_chunk.to_int() * CHUNK.to_int()
169-
<= (SHIFTS.to_int() - int!(1)) * CHUNK.to_int()
170-
);
171138
let shift: i128 = if nth_chunk < SHIFTS {
172139
shl[nth_chunk]
173140
} else {
@@ -176,10 +143,6 @@ impl<const N: u64> BitVec<N> {
176143
let local_index = (nth_bit as i128).wrapping_sub(shift);
177144
if local_index < CHUNK as i128 && local_index >= 0 {
178145
let local_index = local_index as u64;
179-
hax_lib::assert_prop!(
180-
nth_chunk.to_int() * CHUNK.to_int() + local_index.to_int()
181-
< SHIFTS.to_int() * CHUNK.to_int()
182-
);
183146
bitvec[nth_chunk * CHUNK + local_index]
184147
} else {
185148
Bit::Zero
@@ -215,7 +178,6 @@ pub mod int_vec_interp {
215178
pub type $name = FunArray<$m, $ty>;
216179
pastey::paste! {
217180
const _: () = {
218-
#[hax_lib::opaque]
219181
impl BitVec<$n> {
220182
#[doc = concat!("Conversion from ", stringify!($ty), " vectors of size ", stringify!($m), "to bit vectors of size ", stringify!($n))]
221183
pub fn [< from_ $name >](iv: $name) -> BitVec<$n> {
@@ -250,26 +212,6 @@ pub mod int_vec_interp {
250212
FunArray::from_fn(|_| value)
251213
}
252214
}
253-
254-
255-
256-
#[doc = concat!("Lemma that asserts that applying ", stringify!(BitVec::<$n>::from)," and then ", stringify!($name::from), " is the identity.")]
257-
#[hax_lib::fstar::before("[@@ $SIMPLIFICATION_LEMMA ]")]
258-
#[hax_lib::opaque]
259-
#[hax_lib::lemma]
260-
// #[hax_lib::fstar::smt_pat($name::from(BitVec::<$n>::from(x)))]
261-
pub fn lemma_cancel_iv(x: $name) -> Proof<{
262-
hax_lib::eq(BitVec::[< to_ $name >](BitVec::[<from_ $name>](x)), x)
263-
}> {}
264-
#[doc = concat!("Lemma that asserts that applying ", stringify!($name::from)," and then ", stringify!(BitVec::<$n>::from), " is the identity.")]
265-
#[hax_lib::fstar::before("[@@ $SIMPLIFICATION_LEMMA ]")]
266-
#[hax_lib::opaque]
267-
#[hax_lib::lemma]
268-
// #[hax_lib::fstar::smt_pat(BitVec::<$n>::from($name::from(x)))]
269-
pub fn lemma_cancel_bv(x: BitVec<$n>) -> Proof<{
270-
hax_lib::eq(BitVec::[< from_ $name >](BitVec::[<to_ $name>](x)), x)
271-
// hax_lib::eq(BitVec::<$n>::from($name::from(x)), x)
272-
}> {}
273215
};
274216
}
275217
)*

‎testable-simd-models/src/abstractions/funarr.rs‎

Lines changed: 3 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,9 @@
33
/// `FunArray<N, T>` represents an array of `T` values of length `N`, where `N` is a compile-time constant.
44
/// Internally, it uses a fixed-length array of `Option<T>` with a maximum capacity of 512 elements.
55
/// Unused elements beyond `N` are filled with `None`.
6-
///
7-
/// This type is integrated with F* through various `#[hax_lib::fstar::replace]` attributes to support
8-
/// formal verification workflows.
96
#[derive(Copy, Clone, Eq, PartialEq)]
107
pub struct FunArray<const N: u64, T>([Option<T>; 512]);
118

12-
#[hax_lib::exclude]
139
impl<const N: u64, T> FunArray<N, T> {
1410
/// Gets a reference to the element at index `i`.
1511
pub fn get(&self, i: u64) -> &T {
@@ -56,24 +52,7 @@ impl<const N: u64, T> FunArray<N, T> {
5652
}
5753
}
5854

59-
macro_rules! impl_pointwise {
60-
($n:literal, $($i:literal)*) => {
61-
impl<T: Copy> FunArray<$n, T> {
62-
pub fn pointwise(self) -> Self {
63-
Self::from_fn(|i| match i {
64-
$($i => self[$i],)*
65-
_ => unreachable!(),
66-
})
67-
}
68-
}
69-
};
70-
}
7155

72-
impl_pointwise!(4, 0 1 2 3);
73-
impl_pointwise!(8, 0 1 2 3 4 5 6 7);
74-
impl_pointwise!(16, 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15);
75-
76-
#[hax_lib::exclude]
7756
impl<const N: u64, T: Clone> TryFrom<Vec<T>> for FunArray<N, T> {
7857
type Error = ();
7958
fn try_from(v: Vec<T>) -> Result<Self, ()> {
@@ -85,17 +64,17 @@ impl<const N: u64, T: Clone> TryFrom<Vec<T>> for FunArray<N, T> {
8564
}
8665
}
8766

88-
#[hax_lib::exclude]
67+
8968
impl<const N: u64, T: core::fmt::Debug + Clone> core::fmt::Debug for FunArray<N, T> {
9069
fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
9170
write!(f, "{:?}", self.as_vec())
9271
}
9372
}
9473

95-
#[hax_lib::attributes]
74+
9675
impl<const N: u64, T> core::ops::Index<u64> for FunArray<N, T> {
9776
type Output = T;
98-
#[requires(index < N)]
77+
9978
fn index(&self, index: u64) -> &Self::Output {
10079
self.get(index)
10180
}

0 commit comments

Comments
 (0)