fix: examples and tests: never use hax-lib-macros, use hax-lib in…

…stead
hacspec · Oct 10, 2024 · 7e0d95f · 7e0d95f
1 parent c4791b5
commit 7e0d95f
Show file tree

Hide file tree

Showing 17 changed files with 58 additions and 69 deletions.
diff --git a/book/src/tutorial/panic-freedom.md b/book/src/tutorial/panic-freedom.md
@@ -85,7 +85,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/examples/Cargo.toml b/examples/Cargo.toml
@@ -9,7 +9,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
@@ -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
@@ -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
@@ -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-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<u8>) -> ProtocolResult<A0> {
+/// fn init_a(prologue: Vec<u8>) -> ::hax_lib_protocol::ProtocolResult<A0> {
 ///     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<Vec<u8>> for A0 {
-///     type Error = ProtocolError;
+///     type Error = ::hax_lib_protocol::ProtocolError;
 ///     fn try_from(value: Vec<u8>) -> Result<Self, Self::Error> {
 ///         init_a(value)
 ///     }
 /// }
-/// #[hax_lib_macros::exclude]
+/// #[hax_lib::exclude]
 /// impl InitialState for A0 {
-///     fn init(prologue: Option<Vec<u8>>) -> ProtocolResult<Self> {
+///     fn init(prologue: Option<Vec<u8>>) -> ::hax_lib_protocol::ProtocolResult<Self> {
 ///         if let Some(prologue) = prologue {
 ///             prologue.try_into()
 ///         } else {
-///             Err(ProtocolError::InvalidPrologue)
+///             Err(::hax_lib_protocol::ProtocolError::InvalidPrologue)
 ///         }
 ///     }
 /// }
@@ -46,30 +46,30 @@ 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);
     let return_type: syn::Path = parse_macro_input!(attr);
     let name = input.sig.ident;
 
     let expanded = quote!(
-        #[hax_lib_macros::exclude]
+        #[hax_lib::exclude]
         impl TryFrom<Vec<u8>> for #return_type {
-            type Error = ProtocolError;
+            type Error = ::hax_lib_protocol::ProtocolError;
 
             fn try_from(value: Vec<u8>) -> Result<Self, Self::Error> {
                 #name(value)
             }
         }
 
-        #[hax_lib_macros::exclude]
+        #[hax_lib::exclude]
         impl InitialState for #return_type {
-            fn init(prologue: Option<Vec<u8>>) -> ProtocolResult<Self> {
+            fn init(prologue: Option<Vec<u8>>) -> ::hax_lib_protocol::ProtocolResult<Self> {
                 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<B0> {
+/// fn init_b() -> ::hax_lib_protocol::ProtocolResult<B0> {
 ///    Ok(B0 {})
 /// }
 ///
 /// // The following is generated by the macro:
-/// #[hax_lib_macros::exclude]
+/// #[hax_lib::exclude]
 /// impl InitialState for B0 {
-///     fn init(prologue: Option<Vec<u8>>) -> ProtocolResult<Self> {
+///     fn init(prologue: Option<Vec<u8>>) -> ::hax_lib_protocol::ProtocolResult<Self> {
 ///         if let Some(_) = prologue {
-///             Err(ProtocolError::InvalidPrologue)
+///             Err(::hax_lib_protocol::ProtocolError::InvalidPrologue)
 ///         } else {
 ///             init_b()
 ///         }
@@ -111,19 +111,19 @@ 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);
     let return_type: syn::Path = parse_macro_input!(attr);
     let name = input.sig.ident;
 
     let expanded = quote!(
-        #[hax_lib_macros::exclude]
+        #[hax_lib::exclude]
         impl InitialState for #return_type {
-            fn init(prologue: Option<Vec<u8>>) -> ProtocolResult<Self> {
+            fn init(prologue: Option<Vec<u8>>) -> ::hax_lib_protocol::ProtocolResult<Self> {
                 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<A0> for (A1, Message) {
-///    type Error = ProtocolError;
+///    type Error = ::hax_lib_protocol::ProtocolError;
 ///
 ///    fn try_from(value: A0) -> Result<Self, Self::Error> {
 ///       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<Self, Self::Error> {
                 #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<A2> {
+/// fn read_pong(_state: A1, msg: Message) -> ::hax_lib_protocol::ProtocolResult<A2> {
 ///     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<Self, Self::Error> {
 ///         read_pong(state, msg)
 ///     }
 /// }
-/// #[hax_lib_macros::exclude]
+/// #[hax_lib::exclude]
 /// impl ReadState<A2> for A1 {
 ///     type Message = Message;
-///     fn read(self, msg: Message) -> ProtocolResult<A2> {
+///     fn read(self, msg: Message) -> ::hax_lib_protocol::ProtocolResult<A2> {
 ///         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<Self, Self::Error> {
                 #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/tests/Cargo.lock b/tests/Cargo.lock
diff --git 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
@@ -1,12 +1,10 @@
-use hax_lib_macros as hax;
-
-#[hax::opaque_type]
+#[hax_lib::opaque_type]
 struct OpaqueStruct<const X: usize, T, U> {
     field: [T; X],
     other_field: U,
 }
 
-#[hax::opaque_type]
+#[hax_lib::opaque_type]
 enum OpaqueEnum<const X: usize, T, U> {
     A([T; X]),
     B(U),

diff --git 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
@@ -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
@@ -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
@@ -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" }