Remove unnecessary line from noise test manifest

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

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" }
+
 

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);

hax-lib-protocol-macros/src/lib.rs

@@ -216,21 +216,22 @@ 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())
             }
         }
 
         #[hax_lib_macros::exclude]
         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()
             }
         }
     );

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.

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" }
 
 

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);