diff --git a/Cargo.lock b/Cargo.lock
index f1b5c3267..91ec94bdd 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2,6 +2,15 @@
 # It is not intended for manual editing.
 version = 3
 
+[[package]]
+name = "abstract_integers"
+version = "0.1.5"
+source = "git+https://github.com/hacspec/hacspec.git#bb5b411dced2dfe5c7601674153de4545c783c10"
+dependencies = [
+ "num",
+ "num-bigint",
+]
+
 [[package]]
 name = "aho-corasick"
 version = "1.1.2"
@@ -405,6 +414,81 @@ dependencies = [
  "wasi",
 ]
 
+[[package]]
+name = "hacspec-chacha20"
+version = "0.1.0"
+source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982"
+dependencies = [
+ "hacspec-lib",
+]
+
+[[package]]
+name = "hacspec-chacha20poly1305"
+version = "0.1.0"
+source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982"
+dependencies = [
+ "hacspec-chacha20",
+ "hacspec-lib",
+ "hacspec-poly1305",
+]
+
+[[package]]
+name = "hacspec-curve25519"
+version = "0.1.0"
+source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982"
+dependencies = [
+ "hacspec-lib",
+]
+
+[[package]]
+name = "hacspec-derive"
+version = "0.1.0"
+source = "git+https://github.com/hacspec/hacspec.git#bb5b411dced2dfe5c7601674153de4545c783c10"
+dependencies = [
+ "hacspec-lib",
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+]
+
+[[package]]
+name = "hacspec-hmac"
+version = "0.1.0"
+source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982"
+dependencies = [
+ "hacspec-lib",
+ "hacspec-sha256",
+]
+
+[[package]]
+name = "hacspec-lib"
+version = "0.1.0-beta.1"
+source = "git+https://github.com/hacspec/hacspec.git#bb5b411dced2dfe5c7601674153de4545c783c10"
+dependencies = [
+ "abstract_integers",
+ "num",
+ "secret_integers",
+]
+
+[[package]]
+name = "hacspec-poly1305"
+version = "0.1.0"
+source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982"
+dependencies = [
+ "hacspec-lib",
+]
+
+[[package]]
+name = "hacspec-sha256"
+version = "0.1.0"
+source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982"
+dependencies = [
+ "abstract_integers",
+ "hacspec-derive",
+ "hacspec-lib",
+ "secret_integers",
+]
+
 [[package]]
 name = "hashbrown"
 version = "0.14.2"
@@ -486,6 +570,15 @@ dependencies = [
 [[package]]
 name = "hax-engine-names"
 version = "0.1.0-pre.1"
+dependencies = [
+ "hacspec-chacha20",
+ "hacspec-chacha20poly1305",
+ "hacspec-curve25519",
+ "hacspec-hmac",
+ "hacspec-lib",
+ "hacspec-poly1305",
+ "hacspec-sha256",
+]
 
 [[package]]
 name = "hax-engine-names-extract"
@@ -793,6 +886,82 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "num"
+version = "0.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b05180d69e3da0e530ba2a1dae5110317e49e3b7f3d41be227dc5f92e49ee7af"
+dependencies = [
+ "num-bigint",
+ "num-complex",
+ "num-integer",
+ "num-iter",
+ "num-rational",
+ "num-traits",
+]
+
+[[package]]
+name = "num-bigint"
+version = "0.4.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "608e7659b5c3d7cba262d894801b9ec9d00de989e8a82bd4bef91d08da45cdc0"
+dependencies = [
+ "autocfg",
+ "num-integer",
+ "num-traits",
+]
+
+[[package]]
+name = "num-complex"
+version = "0.4.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ba157ca0885411de85d6ca030ba7e2a83a28636056c7c699b07c8b6f7383214"
+dependencies = [
+ "num-traits",
+]
+
+[[package]]
+name = "num-integer"
+version = "0.1.45"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "225d3389fb3509a24c93f5c29eb6bde2586b98d9f016636dff58d7c6f7569cd9"
+dependencies = [
+ "autocfg",
+ "num-traits",
+]
+
+[[package]]
+name = "num-iter"
+version = "0.1.43"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7d03e6c028c5dc5cac6e2dec0efda81fc887605bb3d884578bb6d6bf7514e252"
+dependencies = [
+ "autocfg",
+ "num-integer",
+ "num-traits",
+]
+
+[[package]]
+name = "num-rational"
+version = "0.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0638a1c9d0a3c0914158145bc76cff373a75a627e6ecbfb71cbe6f453a5a19b0"
+dependencies = [
+ "autocfg",
+ "num-bigint",
+ "num-integer",
+ "num-traits",
+]
+
+[[package]]
+name = "num-traits"
+version = "0.2.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "39e3200413f237f41ab11ad6d161bc7239c84dcb631773ccd7de3dfe4b5c267c"
+dependencies = [
+ "autocfg",
+]
+
 [[package]]
 name = "num_cpus"
 version = "1.16.0"
@@ -1037,6 +1206,11 @@ version = "1.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
 
+[[package]]
+name = "secret_integers"
+version = "0.1.7"
+source = "git+https://github.com/hacspec/hacspec.git#bb5b411dced2dfe5c7601674153de4545c783c10"
+
 [[package]]
 name = "semver"
 version = "1.0.20"
diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml
index aee50ed0e..33f196945 100644
--- a/engine/backends/proverif/proverif_backend.ml
+++ b/engine/backends/proverif/proverif_backend.ml
@@ -194,7 +194,7 @@ module Print = struct
             ^^ iblock parens fun_args_types
             ^^ string ": "
             ^^ print#concrete_ident base_name
-            ^^ dot
+            ^^ string " [data]" ^^ dot
           in
           let reduc_line =
             string "reduc forall " ^^ iblock Fn.id fun_args_full ^^ semi
diff --git a/engine/names/Cargo.toml b/engine/names/Cargo.toml
index 6082c8200..d0fe961d9 100644
--- a/engine/names/Cargo.toml
+++ b/engine/names/Cargo.toml
@@ -10,4 +10,12 @@ readme.workspace = true
 description = "Dummy crate containing all the Rust names the hax engine should be aware of"
 
 [dependencies]
+hacspec-lib = { git = "https://github.com/hacspec/hacspec.git" }
+hacspec-chacha20 = { git = "https://github.com/hacspec/specs", version = "0.1.0" }
+hacspec-poly1305 = { git = "https://github.com/hacspec/specs", version = "0.1.0" }
+hacspec-chacha20poly1305 = { git = "https://github.com/hacspec/specs", version = "0.1.0" }
+hacspec-curve25519 = { git = "https://github.com/hacspec/specs", version = "0.1.0" }
+hacspec-sha256 = { git = "https://github.com/hacspec/specs", version = "0.1.0" }
+hacspec-hmac = { git = "https://github.com/hacspec/specs", version = "0.1.0" }
+
 
diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs
index 973f779d3..b41759d3c 100644
--- a/engine/names/src/lib.rs
+++ b/engine/names/src/lib.rs
@@ -1,11 +1,55 @@
 #![allow(dead_code)]
 #![feature(try_trait_v2)]
 #![feature(allocator_api)]
+
+use hacspec_chacha20::{ChaChaIV, ChaChaKey};
+use hacspec_chacha20poly1305::{chacha20_poly1305_decrypt, chacha20_poly1305_encrypt};
+use hacspec_curve25519::{
+    x25519_scalarmult, x25519_secret_to_public, X25519SerializedPoint, X25519SerializedScalar,
+};
+use hacspec_hmac::hmac;
+use hacspec_lib::{U64_from_usize, U64_to_le_bytes};
+use hacspec_poly1305::Poly1305Tag;
+use hacspec_sha256::sha256;
 extern crate alloc;
 /* This is a dummy Rust file. Every path used in this file will be
  * exported and made available automatically in OCaml. */
 
 fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mut y: I) {
+    // Names for the noise example
+    let iv = ChaChaIV::from_seq(&hacspec_lib::Seq::new(0));
+    let key = ChaChaKey::from_seq(&hacspec_lib::Seq::new(0));
+    let seq = hacspec_lib::Seq::from_hex("ff");
+    let msg = hacspec_lib::Seq::from_slice(&seq, 0, 1);
+
+    let aad = msg.concat(&seq);
+    let (cipher_text, tag) = chacha20_poly1305_encrypt(key, iv, &aad, &msg);
+    let _ = chacha20_poly1305_decrypt(key, iv, &aad, &cipher_text, tag);
+    let _ = cipher_text.len();
+
+    let p = X25519SerializedPoint::from_seq(&msg);
+    let s: X25519SerializedScalar = X25519SerializedScalar::from_seq(&msg);
+    x25519_scalarmult(s, p);
+    x25519_secret_to_public(s);
+
+    let _ = hmac(&seq, &msg);
+    msg.slice(0, 1);
+    let _ = hacspec_lib::Seq::from_seq(&msg);
+
+    let _ = U64_to_le_bytes(U64_from_usize(1));
+
+    let _ = Poly1305Tag::from_seq(&msg);
+
+    let _ = sha256(&msg);
+    let _ = cipher_text.clone();
+
+    enum E {
+        E,
+    }
+
+    let _: Result<(), E> = Err(E::E).map_err(|e| e);
+    // End noise example
+
     let _: core::result::Result<u8, u8> = core::result::Result::Ok(0);
     let _: core::result::Result<u8, u8> = core::result::Result::Err(0);
     let _ = x.fold(0, |a, b| a + b);
diff --git a/hax-lib-protocol-macros/src/lib.rs b/hax-lib-protocol-macros/src/lib.rs
index db9945abe..436a87ff3 100644
--- a/hax-lib-protocol-macros/src/lib.rs
+++ b/hax-lib-protocol-macros/src/lib.rs
@@ -216,11 +216,11 @@ pub fn write(
 
     let expanded = quote!(
         #[hax_lib_macros::exclude]
-        impl TryFrom<#current_state> for (#next_state, #message_type) {
+        impl TryFrom<(#current_state, dyn Into<Option<Vec<u8>>>)> for (#next_state, #message_type) {
             type Error = ProtocolError;
 
-            fn try_from(value: #current_state) -> Result<Self, Self::Error> {
-                #name(value)
+            fn try_from((state, payload): (#current_state, impl Into<Option<Vec<u8>>>)) -> Result<Self, Self::Error> {
+                #name(value, payload.into())
             }
         }
 
@@ -228,9 +228,10 @@ pub fn write(
         impl WriteState for #current_state {
             type NextState = #next_state;
             type Message = #message_type;
+            type Payload = Vec<u8>;
 
-            fn write(self) -> ProtocolResult<(Self::NextState, Self::Message)> {
-                self.try_into()
+            fn write(self, payload: Into<Option<Self::Payload>>) -> ProtocolResult<(Self::NextState, Self::Message)> {
+                (self, payload).try_into()
             }
         }
     );
diff --git a/hax-lib-protocol/src/lib.rs b/hax-lib-protocol/src/lib.rs
index d58a6ed58..95fca867c 100644
--- a/hax-lib-protocol/src/lib.rs
+++ b/hax-lib-protocol/src/lib.rs
@@ -38,8 +38,13 @@ pub trait WriteState {
     type NextState;
     /// The type of the message that is being written.
     type Message;
+    /// An external payload that can potentially be incorporated into the message.
+    type Payload;
     /// Produce the message to be written when transitioning to the next state.
-    fn write(self) -> ProtocolResult<(Self::NextState, Self::Message)>;
+    fn write(
+        self,
+        payload: impl Into<Option<&[u8]>>,
+    ) -> ProtocolResult<(Self::NextState, Self::Message)>;
 }
 
 /// A state where a message must be read before transitioning to the next state.
diff --git a/tests/Cargo.lock b/tests/Cargo.lock
index ac5da0078..c3d22b3a4 100644
--- a/tests/Cargo.lock
+++ b/tests/Cargo.lock
@@ -52,6 +52,10 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
 
+[[package]]
+name = "basic-structs"
+version = "0.1.0"
+
 [[package]]
 name = "bitflags"
 version = "1.3.2"
@@ -70,10 +74,6 @@ version = "0.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5"
 
-[[package]]
-name = "basic-structs"
-version = "0.1.0"
-
 [[package]]
 name = "cfg-if"
 version = "1.0.0"
@@ -509,6 +509,7 @@ dependencies = [
  "hacspec-lib",
  "hacspec-poly1305",
  "hacspec-sha256",
+ "hax-lib-macros",
  "rand",
  "rayon",
  "serde",
diff --git a/tests/proverif-noise/Cargo.toml b/tests/proverif-noise/Cargo.toml
index d9e8a8795..b2a224c34 100644
--- a/tests/proverif-noise/Cargo.toml
+++ b/tests/proverif-noise/Cargo.toml
@@ -7,9 +7,6 @@ license = "MIT OR Apache-2.0"
 description = "hacspec chacha20 poly1305 authenticated encryption"
 readme = "README.md"
 
-[lib]
-git = "https://github.com/hacspec/specs"
-
 [dependencies]
 hacspec-lib = { git = "https://github.com/hacspec/hacspec.git" }
 hacspec-chacha20 = { git = "https://github.com/hacspec/specs", version = "0.1.0" }
@@ -19,8 +16,8 @@ hacspec-curve25519 = { git = "https://github.com/hacspec/specs", version = "0.1.
 hacspec-sha256 = { git = "https://github.com/hacspec/specs", version = "0.1.0" }
 hacspec-hmac = { git = "https://github.com/hacspec/specs", version = "0.1.0" }
 hacspec-hkdf = { git = "https://github.com/hacspec/specs", version = "0.1.0" }
-hax-lib-protocol = { path = "../../hax-lib-protocol" }
-hax-lib-protocol-macros = { path = "../../hax-lib-protocol-macros" }
+#hax-lib-protocol = { path = "../../hax-lib-protocol" }
+#hax-lib-protocol-macros = { path = "../../hax-lib-protocol-macros" }
 hax-lib-macros = { path = "../../hax-lib-macros" }
 
 
diff --git a/tests/proverif-noise/src/lib.rs b/tests/proverif-noise/src/lib.rs
index 735225745..296a5b7b6 100644
--- a/tests/proverif-noise/src/lib.rs
+++ b/tests/proverif-noise/src/lib.rs
@@ -1,8 +1,5 @@
-#![feature(proc_macro_hygiene)]
-#[hax_lib_macros::exclude]
 pub mod noise_crypto;
 pub mod noise_kkpsk0;
-#[hax_lib_macros::exclude]
 pub mod noise_lib;
 use hacspec_lib::*;
 bytes!(ProtocolName, 36);
diff --git a/tests/proverif-noise/src/noise_kkpsk0.rs b/tests/proverif-noise/src/noise_kkpsk0.rs
index 6047a4a90..571e08e9a 100644
--- a/tests/proverif-noise/src/noise_kkpsk0.rs
+++ b/tests/proverif-noise/src/noise_kkpsk0.rs
@@ -99,8 +99,8 @@ pub fn write_message1(
     payload: &Seq<U8>,
 ) -> Result<(HandshakeStateI1, Seq<U8>), Error> {
     let HandshakeStateI0 { st, psk, s, e, rs } = hs;
-    let st = mix_key_and_hash(st, &psk);
-    let st = mix_hash(st, &e.public_key);
+    let mut st = mix_key_and_hash(st, &psk);
+    st = mix_hash(st, &e.public_key);
     let st = mix_key(st, &e.public_key);
     let es = dh(&e, &rs);
     let st = mix_key(st, &es);
@@ -199,11 +199,13 @@ pub fn write_transport(
     Ok((tx, ciphertext))
 }
 
+pub struct ReadTransport(Transport, Seq<U8>);
+
 pub fn read_transport(
     tx: Transport,
     ad: &Seq<U8>,
     ciphertext: &Seq<U8>,
-) -> Result<(Transport, Seq<U8>), Error> {
+) -> Result<ReadTransport, Error> {
     let Transport {
         send,
         recv,
@@ -215,5 +217,5 @@ pub fn read_transport(
         recv,
         handshake_hash,
     };
-    Ok((tx, payload))
+    Ok(ReadTransport(tx, payload))
 }
diff --git a/tests/proverif-ping-pong/src/a.rs b/tests/proverif-ping-pong/src/a.rs
index 0f72e5f24..1b1b36353 100644
--- a/tests/proverif-ping-pong/src/a.rs
+++ b/tests/proverif-ping-pong/src/a.rs
@@ -47,7 +47,7 @@ impl InitialState for A0 {
 
 // ==== A state transistion functions ====
 #[hax_lib_protocol_macros::write(A0, A1, Message)]
-fn write_ping(state: A0) -> ProtocolResult<(A1, Message)> {
+fn write_ping(state: A0, _payload: &[u8]) -> ProtocolResult<(A1, Message)> {
     Ok((A1 {}, Message::Ping(state.data)))
 }
 
@@ -56,8 +56,8 @@ fn write_ping(state: A0) -> ProtocolResult<(A1, Message)> {
 impl TryFrom<A0> for (A1, Message) {
     type Error = ProtocolError;
 
-    fn try_from(value: A0) -> Result<Self, Self::Error> {
-        write_ping(value)
+    fn try_from((state, payload): (A0, &[u8])) -> Result<Self, Self::Error> {
+        write_ping(value, payload.into())
     }
 }