diff --git a/.cargo/config.toml b/.cargo/config.toml new file mode 100644 index 000000000..f1b4954a2 --- /dev/null +++ b/.cargo/config.toml @@ -0,0 +1,2 @@ +[build] +rustflags = ["--cfg", "hax"] diff --git a/.utils/jq_utils.jq b/.utils/jq_utils.jq new file mode 100644 index 000000000..bb37a98fe --- /dev/null +++ b/.utils/jq_utils.jq @@ -0,0 +1,27 @@ +# Removes a field from an object at any depth +def remove_field(field): + walk(if type == "object" and has(field) then del(.[field]) else . end); + +# Remove `table_id` indirections whenever a value is found +def thir_drop_table_id_nodes: + walk(if type == "object" and has("cache_id") and has("value") and .value then .value else . end); + +# Prints a THIR def_id as a string, useful for searching +def thir_str_of_def_id_contents: + ( + [.krate] + + [ + .path.[] + | try (.disambiguator as $d | .data | . as $data | keys | .[0] | $data[.] + (if $d > 0 then "#" + $d else "" end)) + | select(type == "string")] + ) | join("::"); + +# Prints all THIR def_ids +def thir_str_of_def_ids: + thir_drop_table_id_nodes | walk( + # if type == "object" and has("contents") and (.contents | type) == "object" and .contents | has("krate") and .contents | has("path") then + if try(. as $o | ($o.contents.krate | type == "string") and ($o.contents.path | type == "array")) catch false then + .contents | thir_str_of_def_id_contents + else + . + end); diff --git a/Cargo.toml b/Cargo.toml index ceca15b72..52243d79a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -6,8 +6,8 @@ members = [ "cli/driver", "test-harness", "hax-lib", - "hax-lib-macros", - "hax-lib-macros/types", + "hax-lib/macros", + "hax-lib/macros/types", "hax-lib-protocol", "hax-lib-protocol-macros", "hax-bounded-integers", @@ -23,8 +23,8 @@ default-members = [ "cli/driver", "test-harness", "hax-lib", - "hax-lib-macros", - "hax-lib-macros/types", + "hax-lib/macros", + "hax-lib/macros/types", "hax-lib-protocol", "hax-lib-protocol-macros", "engine/names", @@ -74,8 +74,8 @@ annotate-snippets = "0.11" hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-alpha.1", default-features = false } hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0-alpha.1" } hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0-alpha.1" } -hax-lib-macros-types = { path = "hax-lib-macros/types", version = "=0.1.0-alpha.1" } -hax-lib-macros = { path = "hax-lib-macros", version = "=0.1.0-alpha.1" } +hax-lib-macros = { path = "hax-lib/macros", version = "=0.1.0-alpha.1" } +hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0-alpha.1" } hax-lib = { path = "hax-lib", version = "=0.1.0-alpha.1" } hax-engine-names = { path = "engine/names", version = "=0.1.0-alpha.1" } hax-types = { path = "hax-types", version = "=0.1.0-alpha.1" } diff --git a/book/src/tutorial/panic-freedom.md b/book/src/tutorial/panic-freedom.md index ab996f58d..0ec0d5284 100644 --- a/book/src/tutorial/panic-freedom.md +++ b/book/src/tutorial/panic-freedom.md @@ -86,7 +86,7 @@ anything might happen: the function might panic, might run forever, erase your disk, or anything. The helper crate -[hax-lib-macros](https://github.com/hacspec/hax/tree/main/hax-lib-macros) +[hax-lib](https://github.com/hacspec/hax/tree/main/hax-lib) provdes the `requires` [proc-macro](https://doc.rust-lang.org/reference/procedural-macros.html) which lets user writting pre-conditions directly in Rust. diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs index 75b5625aa..d5e8f563f 100644 --- a/engine/names/extract/build.rs +++ b/engine/names/extract/build.rs @@ -17,8 +17,8 @@ mod id_table { #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)] pub struct Node { - value: Arc, - id: u32, + pub value: Arc, + pub id: u32, } impl std::ops::Deref for Node { @@ -84,6 +84,7 @@ fn def_id_to_str(def_id: &DefId) -> (Value, String) { } else { &def_id.krate }; + // Update the crate name in the json output as well. let mut json = serde_json::to_value(def_id).unwrap(); json["contents"]["value"]["krate"] = Value::String(crate_name.to_owned()); @@ -97,6 +98,15 @@ fn def_id_to_str(def_id: &DefId) -> (Value, String) { (json, path) } +/// Checks whether a def id refers to a macro or not. +/// We don't want to extract macro names. +fn is_macro(did: &DefId) -> bool { + let Some(last) = did.contents.value.path.last() else { + return false; + }; + matches!(last.data, DefPathItem::MacroNs { .. }) +} + fn reader_to_str(s: String) -> String { let json: Value = match serde_json::from_str(&s) { Ok(v) => v, @@ -107,6 +117,7 @@ fn reader_to_str(s: String) -> String { let def_ids = def_ids .into_iter() + .filter(|did| !is_macro(did)) .map(|did| { let (json, krate_name) = def_id_to_str(&did); (serde_json::to_string(&json).unwrap(), krate_name) diff --git a/examples/Cargo.toml b/examples/Cargo.toml index 2c18893ce..9b7eceb41 100644 --- a/examples/Cargo.toml +++ b/examples/Cargo.toml @@ -10,7 +10,6 @@ members = [ resolver = "2" [workspace.dependencies] -hax-lib-macros = { path = "../hax-lib-macros" } hax-lib = { path = "../hax-lib" } hax-bounded-integers = { path = "../hax-bounded-integers" } diff --git a/examples/kyber_compress/Cargo.toml b/examples/kyber_compress/Cargo.toml index 3749fb057..d75e9a435 100644 --- a/examples/kyber_compress/Cargo.toml +++ b/examples/kyber_compress/Cargo.toml @@ -6,5 +6,4 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -hax-lib-macros.workspace = true hax-lib.workspace = true diff --git a/examples/sha256/Cargo.toml b/examples/sha256/Cargo.toml index 61daf9da1..76cf227cd 100644 --- a/examples/sha256/Cargo.toml +++ b/examples/sha256/Cargo.toml @@ -8,4 +8,4 @@ edition = "2021" path = "src/sha256.rs" [dependencies] -hax-lib-macros.workspace = true +hax-lib.workspace = true diff --git a/examples/sha256/src/sha256.rs b/examples/sha256/src/sha256.rs index 970975c86..54a35259d 100644 --- a/examples/sha256/src/sha256.rs +++ b/examples/sha256/src/sha256.rs @@ -1,4 +1,3 @@ -use hax_lib_macros as hax; use std::convert::TryInto; const BLOCK_SIZE: usize = 64; @@ -50,7 +49,7 @@ const HASH_INIT: Hash = [ 0x5be0cd19u32, ]; -#[hax::requires(i < 4)] +#[hax_lib::requires(i < 4)] pub fn sigma(x: u32, i: usize, op: usize) -> u32 { let mut tmp: u32 = x.rotate_right(OP_TABLE[3 * i + 2].into()); if op == 0 { diff --git a/hax-lib-macros/Cargo.toml b/hax-lib-macros/Cargo.toml deleted file mode 100644 index 90350bf24..000000000 --- a/hax-lib-macros/Cargo.toml +++ /dev/null @@ -1,30 +0,0 @@ -[package] -name = "hax-lib-macros" -version.workspace = true -authors.workspace = true -license.workspace = true -homepage.workspace = true -edition.workspace = true -repository.workspace = true -readme = "README.md" -description = "Hax-specific proc-macros for Rust programs" - -[lib] -proc-macro = true - -[dependencies] -proc-macro-error = "1.0.4" -proc-macro2.workspace = true -quote.workspace = true -syn = { version = "2.0", features = [ - "full", - "visit-mut", - "visit", - "extra-traits", - "parsing", -] } -hax-lib-macros-types.workspace = true -paste = "1.0.15" - -[dev-dependencies] -hax-lib = { path = "../hax-lib" } diff --git a/hax-lib-protocol-macros/src/lib.rs b/hax-lib-protocol-macros/src/lib.rs index 75d39ad12..50c59039f 100644 --- a/hax-lib-protocol-macros/src/lib.rs +++ b/hax-lib-protocol-macros/src/lib.rs @@ -15,28 +15,28 @@ use syn::{parse, parse_macro_input}; /// } /// /// #[hax_lib_protocol_macros::init(A0)] -/// fn init_a(prologue: Vec) -> ProtocolResult { +/// fn init_a(prologue: Vec) -> ::hax_lib_protocol::ProtocolResult { /// if prologue.len() < 1 { -/// return Err(ProtocolError::InvalidPrologue); +/// return Err(::hax_lib_protocol::ProtocolError::InvalidPrologue); /// } /// Ok(A0 { data: prologue[0] }) /// } /// /// // The following is generated by the macro: -/// #[hax_lib_macros::exclude] +/// #[hax_lib::exclude] /// impl TryFrom> for A0 { -/// type Error = ProtocolError; +/// type Error = ::hax_lib_protocol::ProtocolError; /// fn try_from(value: Vec) -> Result { /// init_a(value) /// } /// } -/// #[hax_lib_macros::exclude] +/// #[hax_lib::exclude] /// impl InitialState for A0 { -/// fn init(prologue: Option>) -> ProtocolResult { +/// fn init(prologue: Option>) -> ::hax_lib_protocol::ProtocolResult { /// if let Some(prologue) = prologue { /// prologue.try_into() /// } else { -/// Err(ProtocolError::InvalidPrologue) +/// Err(::hax_lib_protocol::ProtocolError::InvalidPrologue) /// } /// } /// } @@ -46,7 +46,7 @@ pub fn init( attr: proc_macro::TokenStream, item: proc_macro::TokenStream, ) -> proc_macro::TokenStream { - let mut output = quote!(#[hax_lib_macros::process_init]); + let mut output = quote!(#[hax_lib::process_init]); output.extend(proc_macro2::TokenStream::from(item.clone())); let input: syn::ItemFn = parse_macro_input!(item); @@ -54,22 +54,22 @@ pub fn init( let name = input.sig.ident; let expanded = quote!( - #[hax_lib_macros::exclude] + #[hax_lib::exclude] impl TryFrom> for #return_type { - type Error = ProtocolError; + type Error = ::hax_lib_protocol::ProtocolError; fn try_from(value: Vec) -> Result { #name(value) } } - #[hax_lib_macros::exclude] + #[hax_lib::exclude] impl InitialState for #return_type { - fn init(prologue: Option>) -> ProtocolResult { + fn init(prologue: Option>) -> ::hax_lib_protocol::ProtocolResult { if let Some(prologue) = prologue { prologue.try_into() } else { - Err(ProtocolError::InvalidPrologue) + Err(::hax_lib_protocol::ProtocolError::InvalidPrologue) } } } @@ -89,16 +89,16 @@ pub fn init( /// pub struct B0 {} /// /// #[hax_lib_protocol_macros::init_empty(B0)] -/// fn init_b() -> ProtocolResult { +/// fn init_b() -> ::hax_lib_protocol::ProtocolResult { /// Ok(B0 {}) /// } /// /// // The following is generated by the macro: -/// #[hax_lib_macros::exclude] +/// #[hax_lib::exclude] /// impl InitialState for B0 { -/// fn init(prologue: Option>) -> ProtocolResult { +/// fn init(prologue: Option>) -> ::hax_lib_protocol::ProtocolResult { /// if let Some(_) = prologue { -/// Err(ProtocolError::InvalidPrologue) +/// Err(::hax_lib_protocol::ProtocolError::InvalidPrologue) /// } else { /// init_b() /// } @@ -111,7 +111,7 @@ pub fn init_empty( attr: proc_macro::TokenStream, item: proc_macro::TokenStream, ) -> proc_macro::TokenStream { - let mut output = quote!(#[hax_lib_macros::process_init]); + let mut output = quote!(#[hax_lib::process_init]); output.extend(proc_macro2::TokenStream::from(item.clone())); let input: syn::ItemFn = parse_macro_input!(item); @@ -119,11 +119,11 @@ pub fn init_empty( let name = input.sig.ident; let expanded = quote!( - #[hax_lib_macros::exclude] + #[hax_lib::exclude] impl InitialState for #return_type { - fn init(prologue: Option>) -> ProtocolResult { + fn init(prologue: Option>) -> ::hax_lib_protocol::ProtocolResult { if let Some(_) = prologue { - Err(ProtocolError::InvalidPrologue) + Err(::hax_lib_protocol::ProtocolError::InvalidPrologue) } else { #name() } @@ -173,26 +173,26 @@ impl syn::parse::Parse for Transition { /// Example: /// ```ignore /// #[hax_lib_protocol_macros::write(A0, A1, Message)] -/// fn write_ping(state: A0) -> ProtocolResult<(A1, Message)> { +/// fn write_ping(state: A0) -> ::hax_lib_protocol::ProtocolResult<(A1, Message)> { /// Ok((A1 {}, Message::Ping(state.data))) /// } /// /// // The following is generated by the macro: -/// #[hax_lib_macros::exclude] +/// #[hax_lib::exclude] /// impl TryFrom for (A1, Message) { -/// type Error = ProtocolError; +/// type Error = ::hax_lib_protocol::ProtocolError; /// /// fn try_from(value: A0) -> Result { /// write_ping(value) /// } /// } /// -/// #[hax_lib_macros::exclude] +/// #[hax_lib::exclude] /// impl WriteState for A0 { /// type NextState = A1; /// type Message = Message; /// -/// fn write(self) -> ProtocolResult<(Self::NextState, Message)> { +/// fn write(self) -> ::hax_lib_protocol::ProtocolResult<(Self::NextState, Message)> { /// self.try_into() /// } /// } @@ -202,7 +202,7 @@ pub fn write( attr: proc_macro::TokenStream, item: proc_macro::TokenStream, ) -> proc_macro::TokenStream { - let mut output = quote!(#[hax_lib_macros::process_write]); + let mut output = quote!(#[hax_lib::process_write]); output.extend(proc_macro2::TokenStream::from(item.clone())); let input: syn::ItemFn = parse_macro_input!(item); @@ -215,21 +215,21 @@ pub fn write( let name = input.sig.ident; let expanded = quote!( - #[hax_lib_macros::exclude] + #[hax_lib::exclude] impl TryFrom<#current_state> for (#next_state, #message_type) { - type Error = ProtocolError; + type Error = ::hax_lib_protocol::ProtocolError; fn try_from(value: #current_state) -> Result { #name(value) } } - #[hax_lib_macros::exclude] + #[hax_lib::exclude] impl WriteState for #current_state { type NextState = #next_state; type Message = #message_type; - fn write(self) -> ProtocolResult<(Self::NextState, Self::Message)> { + fn write(self) -> ::hax_lib_protocol::ProtocolResult<(Self::NextState, Self::Message)> { self.try_into() } } @@ -246,24 +246,24 @@ pub fn write( /// Example: /// ```ignore /// #[hax_lib_protocol_macros::read(A1, A2, Message)] -/// fn read_pong(_state: A1, msg: Message) -> ProtocolResult { +/// fn read_pong(_state: A1, msg: Message) -> ::hax_lib_protocol::ProtocolResult { /// match msg { -/// Message::Ping(_) => Err(ProtocolError::InvalidMessage), +/// Message::Ping(_) => Err(::hax_lib_protocol::ProtocolError::InvalidMessage), /// Message::Pong(received) => Ok(A2 { received }), /// } /// } /// // The following is generated by the macro: -/// #[hax_lib_macros::exclude] +/// #[hax_lib::exclude] /// impl TryFrom<(A1, Message)> for A2 { -/// type Error = ProtocolError; +/// type Error = ::hax_lib_protocol::ProtocolError; /// fn try_from((state, msg): (A1, Message)) -> Result { /// read_pong(state, msg) /// } /// } -/// #[hax_lib_macros::exclude] +/// #[hax_lib::exclude] /// impl ReadState for A1 { /// type Message = Message; -/// fn read(self, msg: Message) -> ProtocolResult { +/// fn read(self, msg: Message) -> ::hax_lib_protocol::ProtocolResult { /// A2::try_from((self, msg)) /// } /// } @@ -273,7 +273,7 @@ pub fn read( attr: proc_macro::TokenStream, item: proc_macro::TokenStream, ) -> proc_macro::TokenStream { - let mut output = quote!(#[hax_lib_macros::process_read]); + let mut output = quote!(#[hax_lib::process_read]); output.extend(proc_macro2::TokenStream::from(item.clone())); let input: syn::ItemFn = parse_macro_input!(item); @@ -286,19 +286,19 @@ pub fn read( let name = input.sig.ident; let expanded = quote!( - #[hax_lib_macros::exclude] + #[hax_lib::exclude] impl TryFrom<(#current_state, #message_type)> for #next_state { - type Error = ProtocolError; + type Error = ::hax_lib_protocol::ProtocolError; fn try_from((state, msg): (#current_state, #message_type)) -> Result { #name(state, msg) } } - #[hax_lib_macros::exclude] + #[hax_lib::exclude] impl ReadState<#next_state> for #current_state { type Message = #message_type; - fn read(self, msg: Self::Message) -> ProtocolResult<#next_state> { + fn read(self, msg: Self::Message) -> ::hax_lib_protocol::ProtocolResult<#next_state> { #next_state::try_from((self, msg)) } } diff --git a/hax-lib/Cargo.toml b/hax-lib/Cargo.toml index 5207f0e7b..384f19b24 100644 --- a/hax-lib/Cargo.toml +++ b/hax-lib/Cargo.toml @@ -9,11 +9,14 @@ repository.workspace = true readme = "README.md" description = "Hax-specific helpers for Rust programs" -[dependencies] -hax-lib-macros = { workspace = true, optional = true } + +[target.'cfg(hax)'.dependencies] num-bigint = { version = "0.4.3", default-features = false } num-traits = { version = "0.2.15", default-features = false } +[dependencies] +hax-lib-macros = { workspace = true, optional = true } + [features] default = ["macros"] macros = ["dep:hax-lib-macros"] diff --git a/hax-lib-macros/Cargo.lock b/hax-lib/macros/Cargo.lock similarity index 100% rename from hax-lib-macros/Cargo.lock rename to hax-lib/macros/Cargo.lock diff --git a/hax-lib/macros/Cargo.toml b/hax-lib/macros/Cargo.toml new file mode 100644 index 000000000..b6bb28229 --- /dev/null +++ b/hax-lib/macros/Cargo.toml @@ -0,0 +1,30 @@ +[package] +name = "hax-lib-macros" +version.workspace = true +authors.workspace = true +license.workspace = true +homepage.workspace = true +edition.workspace = true +repository.workspace = true +readme = "README.md" +description = "Hax-specific proc-macros for Rust programs" + +[lib] +proc-macro = true + +[target.'cfg(hax)'.dependencies] +proc-macro-error = { version = "1.0.4" } +hax-lib-macros-types = { workspace = true } +paste = { version = "1.0.15" } +syn = { version = "2.0", features = ["full", "visit-mut", "visit"] } + +[dependencies] +syn = { version = "2.0", features = ["full", "visit-mut"] } +proc-macro2 = { workspace = true } +quote = { workspace = true } + +[dev-dependencies] +hax-lib = { path = ".." } + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(hax)', 'cfg(doc_cfg)'] } diff --git a/hax-lib-macros/README.md b/hax-lib/macros/README.md similarity index 100% rename from hax-lib-macros/README.md rename to hax-lib/macros/README.md diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs new file mode 100644 index 000000000..5134763c6 --- /dev/null +++ b/hax-lib/macros/src/dummy.rs @@ -0,0 +1,171 @@ +mod hax_paths; + +use hax_paths::*; +use proc_macro::{TokenStream, TokenTree}; +use quote::quote; +use syn::{visit_mut::VisitMut, *}; + +macro_rules! identity_proc_macro_attribute { + ($($name:ident,)*) => { + $( + #[proc_macro_attribute] + pub fn $name(_attr: TokenStream, item: TokenStream) -> TokenStream { + item + } + )* + } +} + +identity_proc_macro_attribute!( + fstar_options, + fstar_verification_status, + include, + exclude, + requires, + ensures, + pv_handwritten, + pv_constructor, + protocol_messages, + process_init, + process_write, + process_read, + opaque_type, + refinement_type, + fstar_replace, + coq_replace, + proverif_replace, + fstar_before, + coq_before, + proverif_before, + fstar_after, + coq_after, + proverif_after, +); + +#[proc_macro] +pub fn fstar_expr(_payload: TokenStream) -> TokenStream { + quote! { () }.into() +} +#[proc_macro] +pub fn coq_expr(_payload: TokenStream) -> TokenStream { + quote! { () }.into() +} +#[proc_macro] +pub fn proverif_expr(_payload: TokenStream) -> TokenStream { + quote! { () }.into() +} + +#[proc_macro_attribute] +pub fn lemma(_attr: TokenStream, _item: TokenStream) -> TokenStream { + quote! {}.into() +} + +fn unsafe_expr() -> TokenStream { + // `*_unsafe_expr("")` are macro generating a Rust expression of any type, that will be replaced by `` in the backends. + // This should be used solely in hax-only contextes. + // If this macro is used, that means the user broke this rule. + quote! { ::std::compile_error!("`hax_lib::unsafe_expr` has no meaning outside of hax extraction, please use it solely on hax-only places.") }.into() +} + +#[proc_macro] +pub fn fstar_unsafe_expr(_payload: TokenStream) -> TokenStream { + unsafe_expr() +} +#[proc_macro] +pub fn coq_unsafe_expr(_payload: TokenStream) -> TokenStream { + unsafe_expr() +} +#[proc_macro] +pub fn proverif_unsafe_expr(_payload: TokenStream) -> TokenStream { + unsafe_expr() +} + +fn not_hax_attribute(attr: &syn::Attribute) -> bool { + if let Meta::List(ml) = &attr.meta { + !matches!(expects_path_decoration(&ml.path), Ok(Some(_))) + } else { + true + } +} + +fn not_refine_attribute(attr: &syn::Attribute) -> bool { + if let Meta::List(ml) = &attr.meta { + !matches!(expects_refine(&ml.path), Ok(Some(_))) + } else { + true + } +} + +#[proc_macro_attribute] +pub fn attributes(_attr: TokenStream, item: TokenStream) -> TokenStream { + let item: Item = parse_macro_input!(item); + + struct AttrVisitor; + + use syn::visit_mut; + impl VisitMut for AttrVisitor { + fn visit_item_trait_mut(&mut self, item: &mut ItemTrait) { + for ti in item.items.iter_mut() { + if let TraitItem::Fn(fun) = ti { + fun.attrs.retain(not_hax_attribute) + } + } + visit_mut::visit_item_trait_mut(self, item); + } + fn visit_type_mut(&mut self, _type: &mut Type) {} + fn visit_item_impl_mut(&mut self, item: &mut ItemImpl) { + for ii in item.items.iter_mut() { + if let ImplItem::Fn(fun) = ii { + fun.attrs.retain(not_hax_attribute) + } + } + visit_mut::visit_item_impl_mut(self, item); + } + fn visit_item_mut(&mut self, item: &mut Item) { + visit_mut::visit_item_mut(self, item); + + match item { + Item::Struct(s) => { + for field in s.fields.iter_mut() { + field.attrs.retain(not_refine_attribute) + } + } + _ => (), + } + } + } + + let mut item = item; + AttrVisitor.visit_item_mut(&mut item); + + quote! { #item }.into() +} + +#[proc_macro] +pub fn int(payload: TokenStream) -> TokenStream { + let mut tokens = payload.into_iter().peekable(); + let negative = matches!(tokens.peek(), Some(TokenTree::Punct(p)) if p.as_char() == '-'); + if negative { + tokens.next(); + } + let [lit @ TokenTree::Literal(_)] = &tokens.collect::>()[..] else { + return quote! { ::std::compile_error!("Expected exactly one numeric literal") }.into(); + }; + let lit: proc_macro2::TokenStream = TokenStream::from(lit.clone()).into(); + quote! {::hax_lib::int::Int(#lit)}.into() +} + +#[proc_macro_attribute] +pub fn impl_fn_decoration(_attr: TokenStream, _item: TokenStream) -> TokenStream { + quote! { ::std::compile_error!("`impl_fn_decoration` is an internal macro and should never be used directly.") }.into() +} + +#[proc_macro_attribute] +pub fn trait_fn_decoration(_attr: TokenStream, _item: TokenStream) -> TokenStream { + quote! { ::std::compile_error!("`trait_fn_decoration` is an internal macro and should never be used directly.") }.into() +} + +#[proc_macro] +pub fn loop_invariant(_predicate: TokenStream) -> TokenStream { + quote! {}.into() +} diff --git a/hax-lib/macros/src/hax_paths.rs b/hax-lib/macros/src/hax_paths.rs new file mode 100644 index 000000000..96b6fea75 --- /dev/null +++ b/hax-lib/macros/src/hax_paths.rs @@ -0,0 +1,55 @@ +//! This module defines the `ImplFnDecoration` structure and utils +//! around it. + +use syn::spanned::Spanned; +use syn::*; + +fn expect_simple_path(path: &Path) -> Option> { + let mut chunks = vec![]; + if path.leading_colon.is_some() { + chunks.push(String::new()) + } + for segment in &path.segments { + chunks.push(format!("{}", segment.ident)); + if !matches!(segment.arguments, PathArguments::None) { + return None; + } + } + Some(chunks) +} + +/// The various strings allowed as decoration kinds. +pub const DECORATION_KINDS: &[&str] = &["decreases", "ensures", "requires"]; + +/// Expects a `Path` to be a decoration kind: `::hax_lib::`, +/// `hax_lib::` or `` in (with `KIND` in +/// `DECORATION_KINDS`). +pub fn expects_path_decoration(path: &Path) -> Result> { + expects_hax_path(DECORATION_KINDS, path) +} + +/// Expects a path to be `[[::]hax_lib]::refine` +pub fn expects_refine(path: &Path) -> Result> { + expects_hax_path(&["refine"], path) +} + +/// Expects a `Path` to be a hax path: `::hax_lib::`, +/// `hax_lib::` or `` in (with `KW` in `allowlist`). +pub fn expects_hax_path(allowlist: &[&str], path: &Path) -> Result> { + let path_span = path.span(); + let path = expect_simple_path(path) + .ok_or_else(|| Error::new(path_span, "Expected a simple path, with no `<...>`."))?; + Ok( + match path + .iter() + .map(|x| x.as_str()) + .collect::>() + .as_slice() + { + [kw] | ["", "hax_lib", kw] | ["hax_lib", kw] if allowlist.contains(kw) => { + Some(kw.to_string()) + } + _ => None, + }, + ) +} diff --git a/hax-lib-macros/src/impl_fn_decoration.rs b/hax-lib/macros/src/impl_fn_decoration.rs similarity index 71% rename from hax-lib-macros/src/impl_fn_decoration.rs rename to hax-lib/macros/src/impl_fn_decoration.rs index da39b500c..2eb3970a3 100644 --- a/hax-lib-macros/src/impl_fn_decoration.rs +++ b/hax-lib/macros/src/impl_fn_decoration.rs @@ -13,32 +13,6 @@ pub struct ImplFnDecoration { pub self_ty: Type, } -/// The various strings allowed as decoration kinds. -pub const DECORATION_KINDS: &[&str] = &["decreases", "ensures", "requires"]; - -/// Expects a `Path` to be a decoration kind: `::hax_lib::`, -/// `hax_lib::` or `` in (with `KIND` in -/// `DECORATION_KINDS`). -pub fn expects_path_decoration(path: &Path) -> Result> { - let path_span = path.span(); - let path = path - .expect_simple_path() - .ok_or_else(|| Error::new(path_span, "Expected a simple path, with no `<...>`."))?; - Ok( - match path - .iter() - .map(|x| x.as_str()) - .collect::>() - .as_slice() - { - [kw] | ["", "hax_lib", kw] | ["hax_lib", kw] if DECORATION_KINDS.contains(kw) => { - Some(kw.to_string()) - } - _ => None, - }, - ) -} - impl parse::Parse for ImplFnDecoration { fn parse(input: parse::ParseStream) -> Result { let parse_next = || -> Result<_> { diff --git a/hax-lib-macros/src/lib.rs b/hax-lib/macros/src/implementation.rs similarity index 99% rename from hax-lib-macros/src/lib.rs rename to hax-lib/macros/src/implementation.rs index a69da2fce..f71f1891c 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib/macros/src/implementation.rs @@ -1,3 +1,4 @@ +mod hax_paths; mod impl_fn_decoration; mod quote; mod rewrite_self; @@ -5,6 +6,7 @@ mod syn_ext; mod utils; mod prelude { + pub use crate::hax_paths::*; pub use crate::syn_ext::*; pub use proc_macro as pm; pub use proc_macro2::*; @@ -567,7 +569,7 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr let prev = &idents[0..=i]; let refine: Option<(&mut Attribute, Expr)> = field.attrs.iter_mut().find_map(|attr| { - if attr.path().ends_with("refine") { + if let Ok(Some(_)) = expects_refine(attr.path()) { let payload = attr.parse_args().ok()?; Some((attr, payload)) } else { @@ -891,7 +893,7 @@ pub fn refinement_type(mut attr: pm::TokenStream, item: pm::TokenStream) -> pm:: fields.len() ); }; - if field.vis != syn::Visibility::Inherited { + if !matches!(field.vis, syn::Visibility::Inherited) { proc_macro_error::abort!(field.vis.span(), "This field was expected to be private"); } diff --git a/hax-lib/macros/src/lib.rs b/hax-lib/macros/src/lib.rs new file mode 100644 index 000000000..ec7b1f1b1 --- /dev/null +++ b/hax-lib/macros/src/lib.rs @@ -0,0 +1,8 @@ +// Proc-macros must "reside in the root of the crate": whence the use +// of `std::include!` instead of proper module declaration. + +#[cfg(hax)] +std::include!("implementation.rs"); + +#[cfg(not(hax))] +std::include!("dummy.rs"); diff --git a/hax-lib-macros/src/quote.rs b/hax-lib/macros/src/quote.rs similarity index 100% rename from hax-lib-macros/src/quote.rs rename to hax-lib/macros/src/quote.rs diff --git a/hax-lib-macros/src/rewrite_self.rs b/hax-lib/macros/src/rewrite_self.rs similarity index 100% rename from hax-lib-macros/src/rewrite_self.rs rename to hax-lib/macros/src/rewrite_self.rs diff --git a/hax-lib-macros/src/syn_ext.rs b/hax-lib/macros/src/syn_ext.rs similarity index 68% rename from hax-lib-macros/src/syn_ext.rs rename to hax-lib/macros/src/syn_ext.rs index 316ab84f1..690fdabef 100644 --- a/hax-lib-macros/src/syn_ext.rs +++ b/hax-lib/macros/src/syn_ext.rs @@ -22,40 +22,6 @@ impl Parse for ExprClosure1 { } } -pub trait PathExt { - /// Checks whether a `syn::Path` ends with a certain ident. This - /// is a bit bad: we have no way of differentiating an Hax - /// attribute from an attribute from another crate that share a - /// common name. - fn ends_with(&self, i: &str) -> bool; - - /// Expects a simple path (no `<...>`). - fn expect_simple_path(&self) -> Option>; -} - -impl PathExt for Path { - fn ends_with(&self, i: &str) -> bool { - matches!(self.segments.iter().last(), Some(PathSegment { - ident, - arguments: PathArguments::None, - }) if i == ident.to_string().as_str()) - } - - fn expect_simple_path(&self) -> Option> { - let mut chunks = vec![]; - if self.leading_colon.is_some() { - chunks.push(String::new()) - } - for segment in &self.segments { - chunks.push(format!("{}", segment.ident)); - if !matches!(segment.arguments, PathArguments::None) { - return None; - } - } - Some(chunks) - } -} - /// Utility trait to extract an `Ident` from various syn types pub trait ExpectIdent { /// Is `self` an `Ident`? diff --git a/hax-lib-macros/src/utils.rs b/hax-lib/macros/src/utils.rs similarity index 100% rename from hax-lib-macros/src/utils.rs rename to hax-lib/macros/src/utils.rs diff --git a/hax-lib-macros/types/Cargo.toml b/hax-lib/macros/types/Cargo.toml similarity index 100% rename from hax-lib-macros/types/Cargo.toml rename to hax-lib/macros/types/Cargo.toml diff --git a/hax-lib-macros/types/README.md b/hax-lib/macros/types/README.md similarity index 100% rename from hax-lib-macros/types/README.md rename to hax-lib/macros/types/README.md diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib/macros/types/src/lib.rs similarity index 100% rename from hax-lib-macros/types/src/lib.rs rename to hax-lib/macros/types/src/lib.rs diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs new file mode 100644 index 000000000..2d462f547 --- /dev/null +++ b/hax-lib/src/dummy.rs @@ -0,0 +1,108 @@ +#[cfg(feature = "macros")] +pub use crate::proc_macros::*; + +#[macro_export] +macro_rules! debug_assert { + ($($arg:tt)*) => { + ::core::debug_assert!($($arg)*); + }; +} + +#[macro_export] +macro_rules! assert { + ($($arg:tt)*) => { + ::core::assert!($($arg)*); + }; +} + +#[macro_export] +macro_rules! assume { + ($formula:expr) => { + () + }; +} + +pub fn forall(_f: impl Fn(T) -> bool) -> bool { + true +} + +pub fn exists(_f: impl Fn(T) -> bool) -> bool { + true +} + +pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool { + !lhs || rhs() +} + +#[doc(hidden)] +pub fn inline(_: &str) {} + +#[doc(hidden)] +pub fn inline_unsafe(_: &str) -> T { + unreachable!() +} + +#[doc(hidden)] +pub fn _internal_loop_invariant bool>(_: P) {} + +pub trait Refinement { + type InnerType; + fn new(x: Self::InnerType) -> Self; + fn get(self) -> Self::InnerType; + fn get_mut(&mut self) -> &mut Self::InnerType; + fn invariant(value: Self::InnerType) -> bool; +} + +pub trait RefineAs { + fn into_checked(self) -> RefinedType; +} + +pub mod int { + #[derive(Clone, Copy)] + pub struct Int(pub u8); + + impl Int { + pub fn new(x: impl Into) -> Self { + Int(x.into()) + } + pub fn get(self) -> u8 { + self.0 + } + } + + impl Int {} + impl Int {} + impl Int {} + impl Int {} + + impl Int { + pub fn pow2(self) -> Self { + self + } + pub fn _unsafe_from_str(_s: &str) -> Self { + Int(0) + } + } + + pub trait Abstraction { + type AbstractType; + fn lift(self) -> Self::AbstractType; + } + + pub trait Concretization { + fn concretize(self) -> T; + } + + impl Abstraction for u8 { + type AbstractType = Int; + fn lift(self) -> Self::AbstractType { + Int(0) + } + } + + impl Concretization for Int { + fn concretize(self) -> u32 { + 0 + } + } +} diff --git a/hax-lib/src/implementation.rs b/hax-lib/src/implementation.rs new file mode 100644 index 000000000..8afd9eca7 --- /dev/null +++ b/hax-lib/src/implementation.rs @@ -0,0 +1,173 @@ +pub mod int; + +#[cfg(feature = "macros")] +pub use crate::proc_macros::*; + +#[doc(hidden)] +#[cfg(hax)] +#[macro_export] +macro_rules! proxy_macro_if_not_hax { + ($macro:path, no, $($arg:tt)*) => { + () + }; + ($macro:path, $f:expr, $cond:expr$(, $($arg:tt)*)?) => { + $f($cond) + }; +} + +#[cfg(not(debug_assertions))] +#[doc(hidden)] +#[cfg(not(hax))] +#[macro_export] +macro_rules! proxy_macro_if_not_hax { + ($macro:path, $f:expr, $($arg:tt)*) => {}; +} + +#[cfg(debug_assertions)] +#[doc(hidden)] +#[cfg(not(hax))] +#[macro_export] +macro_rules! proxy_macro_if_not_hax { + ($macro:path, $f:expr, $($arg:tt)*) => { + $macro!($($arg)*) + }; +} + +#[macro_export] +/// Proxy to `std::debug_assert!`. Compiled with `hax`, this +/// disappears. +macro_rules! debug_assert { + ($($arg:tt)*) => { + $crate::proxy_macro_if_not_hax!(::core::debug_assert, no, $($arg)*) + }; +} + +#[macro_export] +/// Proxy to `std::assert!`. Compiled with `hax`, this is transformed +/// into a `assert` in the backend. +macro_rules! assert { + ($($arg:tt)*) => { + $crate::proxy_macro_if_not_hax!(::core::assert, $crate::assert, $($arg)*) + }; +} + +#[doc(hidden)] +#[cfg(hax)] +/// This function exists only when compiled with `hax`, and is not +/// meant to be used directly. It is called by `assert!` only in +/// appropriate situations. +pub fn assert(_formula: bool) {} + +#[doc(hidden)] +#[cfg(hax)] +/// This function exists only when compiled with `hax`, and is not +/// meant to be used directly. It is called by `assume!` only in +/// appropriate situations. +pub fn assume(_formula: bool) {} + +#[cfg(hax)] +#[macro_export] +macro_rules! assume { + ($formula:expr) => { + $crate::assume($formula) + }; +} + +/// Assume a boolean formula holds. In Rust, this is expanded to the +/// expression `()`. While extracted with Hax, this gets expanded to a +/// call to an `assume` function. +/// +/// # Example: +/// +/// ```rust +/// fn sum(x: u32, y: u32) -> u32 { +/// hax_lib::assume!(x < 4242 && y < 424242); +/// x + y +/// } +/// ``` +#[cfg(not(hax))] +#[macro_export] +macro_rules! assume { + ($formula:expr) => { + () + }; +} + +/// The universal quantifier. This should be used only for Hax code: in +/// Rust, this is always true. +/// +/// # Example: +/// +/// The Rust expression `forall(|x: T| phi(x))` corresponds to `∀ (x: T), phi(x)`. +pub fn forall(_f: impl Fn(T) -> bool) -> bool { + true +} + +/// The existential quantifier. This should be used only for Hax code: in +/// Rust, this is always true. +/// +/// # Example: +/// +/// The Rust expression `exists(|x: T| phi(x))` corresponds to `∃ (x: T), phi(x)`. +pub fn exists(_f: impl Fn(T) -> bool) -> bool { + true +} + +/// The logical implication `a ==> b`. +pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool { + !lhs || rhs() +} + +/// Dummy function that carries a string to be printed as such in the output language +#[doc(hidden)] +pub fn inline(_: &str) {} + +/// Similar to `inline`, but allows for any type. Do not use directly. +#[doc(hidden)] +pub fn inline_unsafe(_: &str) -> T { + unreachable!() +} + +/// A dummy function that holds a loop invariant. +#[doc(hidden)] +pub fn _internal_loop_invariant bool>(_: P) {} + +/// A type that implements `Refinement` should be a newtype for a +/// type `T`. The field holding the value of type `T` should be +/// private, and `Refinement` should be the only interface to the +/// type. +/// +/// Please never implement this trait yourself, use the +/// `refinement_type` macro instead. +pub trait Refinement { + /// The base type + type InnerType; + /// Smart constructor capturing an invariant. Its extraction will + /// yield a proof obligation. + fn new(x: Self::InnerType) -> Self; + /// Destructor for the refined type + fn get(self) -> Self::InnerType; + /// Gets a mutable reference to a refinement + fn get_mut(&mut self) -> &mut Self::InnerType; + /// Tests wether a value satisfies the refinement + fn invariant(value: Self::InnerType) -> bool; +} + +/// A utilitary trait that provides a `into_checked` method on traits +/// that have a refined counter part. This trait is parametrized by a +/// type `Target`: a base type can be refined in multiple ways. +/// +/// Please never implement this trait yourself, use the +/// `refinement_type` macro instead. +pub trait RefineAs { + /// Smart constructor for `RefinedType`, checking the invariant + /// `RefinedType::invariant`. The check is done statically via + /// extraction to hax: extracted code will yield static proof + /// obligations. + /// + /// In addition, in debug mode, the invariant is checked at + /// run-time, unless this behavior was disabled when defining the + /// refinement type `RefinedType` with the `refinement_type` macro + /// and its `no_debug_runtime_check` option. + fn into_checked(self) -> RefinedType; +} diff --git a/hax-lib/src/lib.rs b/hax-lib/src/lib.rs index 1b2b1b4d1..304ace616 100644 --- a/hax-lib/src/lib.rs +++ b/hax-lib/src/lib.rs @@ -15,178 +15,14 @@ #![no_std] -pub mod int; - #[cfg(feature = "macros")] mod proc_macros; -#[cfg(feature = "macros")] -pub use proc_macros::*; - -#[doc(hidden)] -#[cfg(hax)] -#[macro_export] -macro_rules! proxy_macro_if_not_hax { - ($macro:path, no, $($arg:tt)*) => { - () - }; - ($macro:path, $f:expr, $cond:expr$(, $($arg:tt)*)?) => { - $f($cond) - }; -} -#[cfg(not(debug_assertions))] -#[doc(hidden)] -#[cfg(not(hax))] -#[macro_export] -macro_rules! proxy_macro_if_not_hax { - ($macro:path, $f:expr, $($arg:tt)*) => {}; -} +// hax engine relies on `hax-lib` names: to avoid cluttering names with +// an additional `implementation` in all paths, we `include!` instead +// of doing conditional `mod` and `pub use`. -#[cfg(debug_assertions)] -#[doc(hidden)] #[cfg(not(hax))] -#[macro_export] -macro_rules! proxy_macro_if_not_hax { - ($macro:path, $f:expr, $($arg:tt)*) => { - $macro!($($arg)*) - }; -} - -#[macro_export] -/// Proxy to `std::debug_assert!`. Compiled with `hax`, this -/// disappears. -macro_rules! debug_assert { - ($($arg:tt)*) => { - $crate::proxy_macro_if_not_hax!(::core::debug_assert, no, $($arg)*) - }; -} - -#[macro_export] -/// Proxy to `std::assert!`. Compiled with `hax`, this is transformed -/// into a `assert` in the backend. -macro_rules! assert { - ($($arg:tt)*) => { - $crate::proxy_macro_if_not_hax!(::core::assert, $crate::assert, $($arg)*) - }; -} - -#[doc(hidden)] -#[cfg(hax)] -/// This function exists only when compiled with `hax`, and is not -/// meant to be used directly. It is called by `assert!` only in -/// appropriate situations. -pub fn assert(_formula: bool) {} - -#[doc(hidden)] -#[cfg(hax)] -/// This function exists only when compiled with `hax`, and is not -/// meant to be used directly. It is called by `assume!` only in -/// appropriate situations. -pub fn assume(_formula: bool) {} - +core::include!("dummy.rs"); #[cfg(hax)] -#[macro_export] -macro_rules! assume { - ($formula:expr) => { - $crate::assume($formula) - }; -} - -/// Assume a boolean formula holds. In Rust, this is expanded to the -/// expression `()`. While extracted with Hax, this gets expanded to a -/// call to an `assume` function. -/// -/// # Example: -/// -/// ```rust -/// fn sum(x: u32, y: u32) -> u32 { -/// hax_lib::assume!(x < 4242 && y < 424242); -/// x + y -/// } -/// ``` -#[cfg(not(hax))] -#[macro_export] -macro_rules! assume { - ($formula:expr) => { - () - }; -} - -/// The universal quantifier. This should be used only for Hax code: in -/// Rust, this is always true. -/// -/// # Example: -/// -/// The Rust expression `forall(|x: T| phi(x))` corresponds to `∀ (x: T), phi(x)`. -pub fn forall(_f: impl Fn(T) -> bool) -> bool { - true -} - -/// The existential quantifier. This should be used only for Hax code: in -/// Rust, this is always true. -/// -/// # Example: -/// -/// The Rust expression `exists(|x: T| phi(x))` corresponds to `∃ (x: T), phi(x)`. -pub fn exists(_f: impl Fn(T) -> bool) -> bool { - true -} - -/// The logical implication `a ==> b`. -pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool { - !lhs || rhs() -} - -/// Dummy function that carries a string to be printed as such in the output language -#[doc(hidden)] -pub fn inline(_: &str) {} - -/// Similar to `inline`, but allows for any type. Do not use directly. -#[doc(hidden)] -pub fn inline_unsafe(_: &str) -> T { - unreachable!() -} - -/// A dummy function that holds a loop invariant. -#[doc(hidden)] -pub fn _internal_loop_invariant bool>(_: P) {} - -/// A type that implements `Refinement` should be a newtype for a -/// type `T`. The field holding the value of type `T` should be -/// private, and `Refinement` should be the only interface to the -/// type. -/// -/// Please never implement this trait yourself, use the -/// `refinement_type` macro instead. -pub trait Refinement { - /// The base type - type InnerType; - /// Smart constructor capturing an invariant. Its extraction will - /// yield a proof obligation. - fn new(x: Self::InnerType) -> Self; - /// Destructor for the refined type - fn get(self) -> Self::InnerType; - /// Gets a mutable reference to a refinement - fn get_mut(&mut self) -> &mut Self::InnerType; - /// Tests wether a value satisfies the refinement - fn invariant(value: Self::InnerType) -> bool; -} - -/// A utilitary trait that provides a `into_checked` method on traits -/// that have a refined counter part. This trait is parametrized by a -/// type `Target`: a base type can be refined in multiple ways. -/// -/// Please never implement this trait yourself, use the -/// `refinement_type` macro instead. -pub trait RefineAs { - /// Smart constructor for `RefinedType`, checking the invariant - /// `RefinedType::invariant`. The check is done statically via - /// extraction to hax: extracted code will yield static proof - /// obligations. - /// - /// In addition, in debug mode, the invariant is checked at - /// run-time, unless this behavior was disabled when defining the - /// refinement type `RefinedType` with the `refinement_type` macro - /// and its `no_debug_runtime_check` option. - fn into_checked(self) -> RefinedType; -} +core::include!("implementation.rs"); diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 3fd42cefa..5fcbe4dc7 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -35,7 +35,6 @@ name = "attribute-opaque" version = "0.1.0" dependencies = [ "hax-lib", - "hax-lib-macros", "serde", ] @@ -400,7 +399,6 @@ name = "interface-only" version = "0.1.0" dependencies = [ "hax-lib", - "hax-lib-macros", ] [[package]] @@ -546,7 +544,7 @@ version = "0.1.0" dependencies = [ "criterion", "hacspec-dev", - "hax-lib-macros", + "hax-lib", "hax-lib-protocol", "hax-lib-protocol-macros", "rand", @@ -670,7 +668,7 @@ version = "0.1.0" name = "ping-pong" version = "0.1.0" dependencies = [ - "hax-lib-macros", + "hax-lib", "hax-lib-protocol", "hax-lib-protocol-macros", ] @@ -785,7 +783,7 @@ dependencies = [ name = "raw-attributes" version = "0.1.0" dependencies = [ - "hax-lib-macros", + "hax-lib", ] [[package]] diff --git a/tests/attribute-opaque/Cargo.toml b/tests/attribute-opaque/Cargo.toml index 4385bd9cc..ae6565c9b 100644 --- a/tests/attribute-opaque/Cargo.toml +++ b/tests/attribute-opaque/Cargo.toml @@ -4,7 +4,6 @@ version = "0.1.0" edition = "2021" [dependencies] -hax-lib-macros = { path = "../../hax-lib-macros" } hax-lib = { path = "../../hax-lib" } serde = { version = "1.0", features = ["derive"] } diff --git a/tests/attribute-opaque/src/lib.rs b/tests/attribute-opaque/src/lib.rs index d1de26773..7840b4fa8 100644 --- a/tests/attribute-opaque/src/lib.rs +++ b/tests/attribute-opaque/src/lib.rs @@ -1,12 +1,10 @@ -use hax_lib_macros as hax; - -#[hax::opaque_type] +#[hax_lib::opaque_type] struct OpaqueStruct { field: [T; X], other_field: U, } -#[hax::opaque_type] +#[hax_lib::opaque_type] enum OpaqueEnum { A([T; X]), B(U), diff --git a/tests/cli/interface-only/Cargo.toml b/tests/cli/interface-only/Cargo.toml index 8d36bd687..afef45f84 100644 --- a/tests/cli/interface-only/Cargo.toml +++ b/tests/cli/interface-only/Cargo.toml @@ -4,7 +4,6 @@ version = "0.1.0" edition = "2021" [dependencies] -hax-lib-macros = { path = "../../../hax-lib-macros" } hax-lib = { path = "../../../hax-lib" } [package.metadata.hax-tests] diff --git a/tests/cli/interface-only/src/lib.rs b/tests/cli/interface-only/src/lib.rs index 8805b203a..3c7e790b2 100644 --- a/tests/cli/interface-only/src/lib.rs +++ b/tests/cli/interface-only/src/lib.rs @@ -1,15 +1,13 @@ #![allow(dead_code)] -use hax_lib as hax; - /// This item contains unsafe blocks and raw references, two features /// not supported by hax. Thanks to the `-i` flag and the `+:` /// modifier, `f` is still extractable as an interface. /// /// Expressions within type are still extracted, as well as pre- and /// post-conditions. -#[hax::requires(x < 254)] -#[hax::ensures(|r| r[0] > x)] +#[hax_lib::requires(x < 254)] +#[hax_lib::ensures(|r| r[0] > x)] fn f(x: u8) -> [u8; 4] { let y = x as *const i8; diff --git a/tests/proverif-noise/Cargo.toml b/tests/proverif-noise/Cargo.toml index ab65750ba..0547c6e7b 100644 --- a/tests/proverif-noise/Cargo.toml +++ b/tests/proverif-noise/Cargo.toml @@ -10,7 +10,7 @@ readme = "README.md" [dependencies] hax-lib-protocol = { path = "../../hax-lib-protocol" } hax-lib-protocol-macros = { path = "../../hax-lib-protocol-macros" } -hax-lib-macros = { path = "../../hax-lib-macros" } +hax-lib = { path = "../../hax-lib" } [dev-dependencies] diff --git a/tests/proverif-ping-pong/Cargo.toml b/tests/proverif-ping-pong/Cargo.toml index 4eda5a938..a7a7efc9c 100644 --- a/tests/proverif-ping-pong/Cargo.toml +++ b/tests/proverif-ping-pong/Cargo.toml @@ -8,4 +8,4 @@ edition = "2021" [dependencies] hax-lib-protocol = { path = "../../hax-lib-protocol" } hax-lib-protocol-macros = { path = "../../hax-lib-protocol-macros" } -hax-lib-macros = { path = "../../hax-lib-macros" } +hax-lib = { path = "../../hax-lib" } diff --git a/tests/proverif-ping-pong/src/a.rs b/tests/proverif-ping-pong/src/a.rs index 79616f4d2..657c680fb 100644 --- a/tests/proverif-ping-pong/src/a.rs +++ b/tests/proverif-ping-pong/src/a.rs @@ -1,4 +1,4 @@ -use hax_lib_protocol::state_machine::*; +use hax_lib_protocol::{state_machine::*, ProtocolError, ProtocolResult}; use crate::Message; diff --git a/tests/proverif-ping-pong/src/b.rs b/tests/proverif-ping-pong/src/b.rs index 5d950d638..7e5c083df 100644 --- a/tests/proverif-ping-pong/src/b.rs +++ b/tests/proverif-ping-pong/src/b.rs @@ -1,4 +1,4 @@ -use hax_lib_protocol::state_machine::*; +use hax_lib_protocol::{state_machine::*, ProtocolError, ProtocolResult}; use crate::Message; diff --git a/tests/proverif-ping-pong/src/lib.rs b/tests/proverif-ping-pong/src/lib.rs index e6570e81c..64bb7a7b7 100644 --- a/tests/proverif-ping-pong/src/lib.rs +++ b/tests/proverif-ping-pong/src/lib.rs @@ -1,7 +1,7 @@ mod a; mod b; -#[hax_lib_macros::protocol_messages] +#[hax_lib::protocol_messages] pub enum Message { Ping(u8), Pong(u8), diff --git a/tests/raw-attributes/Cargo.toml b/tests/raw-attributes/Cargo.toml index 1508b3de0..ec83206a8 100644 --- a/tests/raw-attributes/Cargo.toml +++ b/tests/raw-attributes/Cargo.toml @@ -4,7 +4,7 @@ version = "0.1.0" edition = "2021" [dependencies] -hax-lib-macros = { path = "../../hax-lib-macros" } +hax-lib = { path = "../../hax-lib" } [package.metadata.hax-tests] into."fstar" = { snapshot = "none" }