hax_engine_names/
lib.rs

1#![allow(dead_code)]
2#![feature(try_trait_v2)]
3#![feature(allocator_api)]
4
5extern crate alloc;
6/* This is a dummy Rust file. Every path used in this file will be
7 * exported and made available automatically in OCaml. */
8
9mod crypto_abstractions;
10
11fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mut y: I) {
12    let _: core::result::Result<u8, u8> = core::result::Result::Ok(0);
13    let _: core::result::Result<u8, u8> = core::result::Result::Err(0);
14    let _ = x.fold(0, |a, b| a + b);
15    let _ = y.next();
16    let _: core::ops::ControlFlow<u8> = core::ops::ControlFlow::Break(0);
17    let _: core::ops::ControlFlow<u8> = core::ops::ControlFlow::Continue(());
18    let mut v = vec![()];
19    v[0];
20    v[0] = ();
21    use std::ops::FromResidual;
22    let _ = Result::<String, i64>::from_residual(Err(3u8));
23    let _ = Box::new(());
24    let _: Option<alloc::alloc::Global> = None;
25    let _: Option<()> = Some(());
26    let _: Option<()> = None;
27    let _ = Option::<()>::None.is_some();
28    let _: Result<(), u32> = Result::Err(3u8).map_err(u32::from);
29    assert!(true);
30    assert_eq!(1, 1);
31    hax_lib::assert!(true);
32    hax_lib::_internal_loop_invariant(|_: usize| true);
33    hax_lib::_internal_while_loop_invariant(hax_lib::Prop::from(true));
34    hax_lib::_internal_loop_decreases(hax_lib::Int::_unsafe_from_str("0"));
35
36    fn props() {
37        use hax_lib::prop::*;
38        let x = Prop::from_bool(true);
39        constructors::from_bool(true);
40        constructors::and(x, x);
41        constructors::or(x, x);
42        constructors::not(x);
43        constructors::eq(x, x);
44        constructors::ne(x, x);
45        constructors::implies(x, x);
46        constructors::forall(|_: ()| x);
47        constructors::exists(|_: ()| x);
48
49        Prop::from_bool(true);
50        Prop::and(x, x);
51        Prop::or(x, x);
52        Prop::not(x);
53        Prop::eq(x, x);
54        Prop::ne(x, x);
55        Prop::implies(x, x);
56
57        true.to_prop();
58
59        forall(|_: ()| x);
60        exists(|_: ()| x);
61        implies(x, x);
62    }
63
64    let _ = [()].into_iter();
65    let _: u16 = 6u8.into();
66    let _ = 1..2;
67    let _ = 1..;
68    let _ = ..;
69    let _ = ..1;
70
71    let _ = [
72        std::ops::ControlFlow::Break(()),
73        std::ops::ControlFlow::Continue(()),
74    ];
75
76    fn iterator_functions<It: Iterator + Clone>(it: It) {
77        let _ = it.clone().step_by(2);
78        let _ = it.clone().enumerate();
79        let _ = [()].chunks_exact(2);
80        let _ = [()].iter();
81        let _ = (&[()] as &[()]).iter();
82    }
83
84    {
85        use hax_lib::*;
86        let a: Int = 3u8.lift();
87        let _: Int = 3u8.to_int();
88        let _ = a.clone().pow2();
89        let _ = Int::_unsafe_from_str("1");
90        let _: u32 = a.concretize();
91    }
92
93    fn question_mark_result<A, B: From<A>>(x: A) -> Result<(), B> {
94        Err(x)?;
95        Ok(())
96    }
97
98    let _ = hax_lib::inline("");
99    let _: () = hax_lib::inline_unsafe("");
100    let _: () = hax_lib::any_to_unit(());
101    use hax_lib::{RefineAs, Refinement};
102
103    fn refinements<T: Refinement + Clone, U: RefineAs<T>>(x: T, y: U) -> T {
104        let _ = x.clone().get_mut();
105        T::new(x.get());
106        y.into_checked()
107    }
108
109    const _: () = {
110        use core::{cmp::*, ops::*};
111        fn arith<
112            X: Add<Output = X>
113                + Sub<Output = X>
114                + Mul<Output = X>
115                + Div<Output = X>
116                + Rem<Output = X>
117                + BitXor<Output = X>
118                + BitAnd<Output = X>
119                + BitOr<Output = X>
120                + Shl<Output = X>
121                + Shr<Output = X>
122                + Neg<Output = X>
123                + Not<Output = X>
124                + PartialOrd
125                + Copy,
126        >(
127            x: X,
128        ) -> X {
129            let _ = x < x && x > x && x <= x && x >= x && x == x && x != x;
130            (x ^ x & !x) + x / x * x - x | (-x) % x << x >> x
131        }
132    };
133
134    fn dummy<T: core::ops::Try<Output = ()>>(z: T) {
135        let _ = T::from_output(());
136        let _ = z.branch();
137    }
138
139    let s: &str = "123";
140    let ptr: *const u8 = s.as_ptr();
141
142    unsafe {
143        let _ = *ptr.offset(1) as char;
144    }
145
146    const _: () = {
147        use std::ops::DerefMut;
148        fn f<T: DerefMut>(x: T) {
149            let _: &mut _ = { x }.deref_mut();
150        }
151    };
152}
153
154macro_rules! impl_arith {
155    ($name:ident$(,)?) => {
156        mod $name {
157            fn add() {}
158            fn sub() {}
159            fn mul() {}
160            fn div() {}
161            fn rem() {}
162            fn neg() {}
163            fn bit_xor() {}
164            fn bit_and() {}
165            fn bit_or() {}
166            fn shl() {}
167            fn shr() {}
168            fn eq() {}
169            fn lt() {}
170            fn le() {}
171            fn ne() {}
172            fn ge() {}
173            fn gt() {}
174        }
175    };
176    ($name:ident,$($rest:tt)*) => {
177        impl_arith!($name);
178        impl_arith!($($rest)*);
179    }
180}
181
182impl_arith!(u8, u16, u32, u64, u128, usize);
183impl_arith!(i8, i16, i32, i64, i128, isize);
184
185fn offset() {}
186
187fn unsize() {}
188
189/// Hax additions
190mod hax {
191    fn failure() {}
192    struct Failure;
193    enum Never {}
194
195    // Only useful when HAX_CORE_EXTRACTION_MODE in `on`
196    enum MutRef {}
197
198    struct Tuple2(u8, u8);
199    fn deref_op() {}
200    fn cast_op() {}
201    fn logical_op_and() {}
202    fn logical_op_or() {}
203
204    fn while_loop() {}
205    fn while_loop_cf() {}
206    fn while_loop_return() {}
207    fn repeat() {}
208    fn update_at() {}
209    mod monomorphized_update_at {
210        fn update_at_usize() {}
211        fn update_at_range() {}
212        fn update_at_range_from() {}
213        fn update_at_range_to() {}
214        fn update_at_range_full() {}
215    }
216    // TODO: Should that live here? (this is F* specific)
217    fn array_of_list() {}
218    fn never_to_any() {}
219
220    mod folds {
221        fn fold_range() {}
222        fn fold_range_cf() {}
223        fn fold_range_return() {}
224        fn fold_range_step_by() {}
225        fn fold_range_step_by_cf() {}
226        fn fold_range_step_by_return() {}
227        fn fold_enumerated_slice() {}
228        fn fold_enumerated_slice_cf() {}
229        fn fold_enumerated_slice_return() {}
230        fn fold_enumerated_chunked_slice() {}
231        fn fold_enumerated_chunked_slice_cf() {}
232        fn fold_enumerated_chunked_slice_return() {}
233        fn fold_chunked_slice() {}
234        fn fold_chunked_slice_cf() {}
235        fn fold_chunked_slice_return() {}
236        fn fold_cf() {}
237        fn fold_return() {}
238    }
239
240    /// The engine uses this `dropped_body` symbol as a marker value
241    /// to signal that a item was extracted without body.
242    fn dropped_body() {}
243
244    mod int {
245        fn add() {}
246        fn sub() {}
247        fn div() {}
248        fn mul() {}
249        fn rem() {}
250        fn neg() {}
251
252        fn le() {}
253        fn lt() {}
254        fn ge() {}
255        fn gt() {}
256
257        fn eq() {}
258        fn ne() {}
259
260        fn from_machine() {}
261        fn into_machine() {}
262    }
263
264    mod machine_int {
265        fn add() {}
266        fn sub() {}
267        fn div() {}
268        fn mul() {}
269        fn rem() {}
270
271        fn not() {}
272        fn bitxor() {}
273        fn bitor() {}
274        fn bitand() {}
275        fn shl() {}
276        fn shr() {}
277
278        fn eq() {}
279        fn ne() {}
280        fn le() {}
281        fn lt() {}
282        fn ge() {}
283        fn gt() {}
284    }
285
286    mod control_flow_monad {
287        trait ControlFlowMonad {
288            fn lift() {}
289        }
290        mod mexception {
291            fn run() {}
292        }
293        mod mresult {
294            fn run() {}
295        }
296        mod moption {
297            fn run() {}
298        }
299    }
300    fn box_new() {}
301}
hax_engine_names/lib.rs

hax_engine_names/
lib.rs
