crucible/
cryptol.rs

1use core::cell::UnsafeCell;
2
3/// Load a Cryptol definition.  `module_path` must be the path to a Cryptol module file, and `name`
4/// must be an identifier defined within that module.  The type parameter `F` must be a function
5/// pointer type matching the type of the Cryptol definition.  For example, if the Cryptol
6/// definition has type `[8] -> [8] -> [8]`, then `F` must be `fn(u8, u8) -> u8`, `fn(i8, i8) ->
7/// u8`, or some similar combination.
8pub fn load<F>(module_path: &str, name: &str) -> F {
9    unimplemented!("cryptol::load")
10}
11
12/// Load the Cryptol function `name` from `module_path` and install it as an override for the
13/// function `f`.  `f` must be a function definition, not a function pointer or closure, and its
14/// signature must match the signature of the Cryptol function.  For example, if the Cryptol
15/// definition has type `[8] -> [8] -> [8]`, then `f` must have the signature `fn(u8, u8) -> u8`,
16/// `fn(i8, i8) -> u8`, or some similar combination.
17pub fn override_<F>(f: F, module_path: &str, name: &str) {
18    unimplemented!("cryptol::override")
19}
20
21/// Mark the given Cryptol name to be treated as uninterpreted for the duration
22/// of the current test.
23pub fn uninterp(name: &str) {
24    unimplemented!("cryptol::uninterp")
25}
26
27#[doc(hidden)]
28#[macro_export]
29macro_rules! cryptol_function_name {
30    ($custom_name:expr, $ident:ident) => { $custom_name };
31    ($ident:ident) => { stringify!($ident) };
32}
33
34#[macro_export]
35macro_rules! cryptol {
36
37    // This pattern does not support const-generics, so its expression is
38    // not processed by format!. Therefore its use of curly braces will not
39    // need to be escaped.
40    (
41        path $path:expr;
42
43        $(#[$attr:meta])*
44        $pub_:vis fn $name:ident
45                ( $($arg_name:ident : $arg_ty:ty),* )
46                $( -> $ret_ty:ty )?
47                $(= $cryptol_name:expr)? ;
48        $($rest:tt)*
49    ) => {
50        $(#[$attr])*
51        #[allow(unconditional_recursion)]
52        $pub_ fn $name($($arg_name: $arg_ty),*) $(-> $ret_ty)? {
53            // The first call to `$name` loads the Cryptol definition and installs it as an
54            // override for `$name` itself.  The recursive call below, and all future calls to
55            // `$name`, will dispatch directly to the Cryptol override.
56            $crate::cryptol::override_(
57                $name,
58                $path,
59                $crate::cryptol_function_name!($($cryptol_name,)? $name),
60            );
61            $name($($arg_name),*)
62        }
63        $crate::cryptol! { path $path; $($rest)* }
64    };
65
66    // This pattern supports definitions with const generics. The cryptol
67    // expression will be processed by format! which will allow the generic
68    // parameters to be accessed by name, e.g. `{N}`. Any regular use of
69    // curly braces in the expression will need to be escaped,
70    // e.g. `{{` or `}}`.
71    (
72        path $path:expr;
73
74        $(#[$attr:meta])*
75        $pub_:vis fn $name:ident
76                < $(const $N:ident: $N_ty:ty),* >
77                ( $($arg_name:ident : $arg_ty:ty),* )
78                $( -> $ret_ty:ty )?
79                = $cryptol_name:expr ;
80        $($rest:tt)*
81    ) => {
82        $(#[$attr])*
83        #[allow(unconditional_recursion)]
84        $pub_ fn $name< $(const $N: $N_ty),* >($($arg_name: $arg_ty),*) $(-> $ret_ty)? {
85            $crate::cryptol::override_(
86                $name::< $($N),* >,
87                $path,
88                &format!($cryptol_name),
89            );
90            $name::< $($N),* >($($arg_name),*)
91        }
92        $crate::cryptol! { path $path; $($rest)* }
93    };
94
95    (
96        path $path:expr;
97    ) => {
98    };
99}
100
101/// Convert all what4 expressions within `x` to saw-core and back.  The resulting expressions will
102/// be equivalent but not necessarily identical.
103pub fn munge<T>(x: T) -> T {
104    x
105}
crucible/cryptol.rs

crucible/
cryptol.rs
