From 9312e47fbb8b9e5aba31ad13aa0ea7a374c6940d Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 13 Dec 2023 09:01:18 +0100 Subject: [PATCH 01/14] Introduce helper library for Protocol traits --- Cargo.lock | 4 ++++ Cargo.toml | 1 + hax-lib-protocol/Cargo.toml | 13 +++++++++++++ hax-lib-protocol/src/lib.rs | 24 ++++++++++++++++++++++++ 4 files changed, 42 insertions(+) create mode 100644 hax-lib-protocol/Cargo.toml create mode 100644 hax-lib-protocol/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock index a582a8bc1..0596ff073 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -535,6 +535,10 @@ dependencies = [ "uuid", ] +[[package]] +name = "hax-lib-protocol" +version = "0.1.0-pre.1" + [[package]] name = "hax-lint" version = "0.1.0-pre.1" diff --git a/Cargo.toml b/Cargo.toml index 50c29c170..5765b335a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -13,6 +13,7 @@ members = [ "hax-lib", "hax-lib-macros", "hax-lib-macros/types", + "hax-lib-protocol", ] exclude = ["tests"] resolver = "2" diff --git a/hax-lib-protocol/Cargo.toml b/hax-lib-protocol/Cargo.toml new file mode 100644 index 000000000..8f5c11cda --- /dev/null +++ b/hax-lib-protocol/Cargo.toml @@ -0,0 +1,13 @@ +[package] +name = "hax-lib-protocol" +version.workspace = true +authors.workspace = true +license.workspace = true +homepage.workspace = true +edition.workspace = true +repository.workspace = true +readme.workspace = true + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/hax-lib-protocol/src/lib.rs b/hax-lib-protocol/src/lib.rs new file mode 100644 index 000000000..1af93d998 --- /dev/null +++ b/hax-lib-protocol/src/lib.rs @@ -0,0 +1,24 @@ +#[derive(Debug)] +pub enum ProtocolError { + InvalidMessage, + InvalidPrologue, +} + +pub type ProtocolResult = Result; + +pub trait InitialState { + fn init(prologue: Option>) -> ProtocolResult + where + Self: Sized; +} + +pub trait WriteState { + type NextState; + type Message; + fn write(self) -> ProtocolResult<(Self::NextState, Self::Message)>; +} + +pub trait ReadState { + type Message; + fn read(self, msg: Self::Message) -> ProtocolResult; +} From d2e1e2cfb5ce6e166aa3e659f14ae6d42e04b652 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 13 Dec 2023 09:21:33 +0100 Subject: [PATCH 02/14] Macro helper crate for automatically implementing protocol traits --- Cargo.lock | 10 + Cargo.toml | 1 + hax-lib-protocol-macros/Cargo.toml | 25 +++ hax-lib-protocol-macros/src/lib.rs | 300 +++++++++++++++++++++++++++++ 4 files changed, 336 insertions(+) create mode 100644 hax-lib-protocol-macros/Cargo.toml create mode 100644 hax-lib-protocol-macros/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock index 0596ff073..76a4fad3b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -539,6 +539,16 @@ dependencies = [ name = "hax-lib-protocol" version = "0.1.0-pre.1" +[[package]] +name = "hax-lib-protocol-macros" +version = "0.1.0-pre.1" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.38", +] + [[package]] name = "hax-lint" version = "0.1.0-pre.1" diff --git a/Cargo.toml b/Cargo.toml index 5765b335a..cb56b0837 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,6 +14,7 @@ members = [ "hax-lib-macros", "hax-lib-macros/types", "hax-lib-protocol", + "hax-lib-protocol-macros" ] exclude = ["tests"] resolver = "2" diff --git a/hax-lib-protocol-macros/Cargo.toml b/hax-lib-protocol-macros/Cargo.toml new file mode 100644 index 000000000..0cb376255 --- /dev/null +++ b/hax-lib-protocol-macros/Cargo.toml @@ -0,0 +1,25 @@ +[package] +name = "hax-lib-protocol-macros" +version.workspace = true +authors.workspace = true +license.workspace = true +homepage.workspace = true +edition.workspace = true +repository.workspace = true +readme.workspace = true + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[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", + "extra-traits", + "parsing", +] } diff --git a/hax-lib-protocol-macros/src/lib.rs b/hax-lib-protocol-macros/src/lib.rs new file mode 100644 index 000000000..3ae4d6d0b --- /dev/null +++ b/hax-lib-protocol-macros/src/lib.rs @@ -0,0 +1,300 @@ +use quote::quote; +use syn::{parse, parse_macro_input}; + +/// This macro takes an `fn` as the basis of an `InitialState` implementation for the state type that is returned by the `fn` (on success). +/// +/// The `fn` is expected to build the state type from a `Vec`. +/// +/// Example: +/// ```ignore +/// pub struct A0 { +/// data: u8, +/// } +/// +/// #[hax_lib_protocol_macros::init(A0)] +/// fn init_a(prologue: Vec) -> ProtocolResult { +/// if prologue.len() < 1 { +/// return Err(ProtocolError::InvalidPrologue); +/// } +/// Ok(A0 { data: prologue[0] }) +/// } +/// +/// // The following generated by macro: +/// #[hax_lib_macros::exclude] +/// impl TryFrom> for A0 { +/// type Error = ProtocolError; +/// fn try_from(value: Vec) -> Result { +/// init_a(value) +/// } +/// } +/// #[hax_lib_macros::exclude] +/// impl InitialState for A0 { +/// fn init(prologue: Option>) -> ProtocolResult { +/// if let Some(prologue) = prologue { +/// prologue.try_into() +/// } else { +/// Err(ProtocolError::InvalidPrologue) +/// } +/// } +/// } +/// ``` +#[proc_macro_attribute] +pub fn init( + attr: proc_macro::TokenStream, + item: proc_macro::TokenStream, +) -> proc_macro::TokenStream { + let mut output = quote!(#[hax_lib_macros::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] + impl TryFrom> for #return_type { + type Error = ProtocolError; + + fn try_from(value: Vec) -> Result { + #name(value) + } + } + + #[hax_lib_macros::exclude] + impl InitialState for #return_type { + fn init(prologue: Option>) -> ProtocolResult { + if let Some(prologue) = prologue { + prologue.try_into() + } else { + Err(ProtocolError::InvalidPrologue) + } + } + } + ); + output.extend(expanded); + + return output.into(); +} + +/// This macro takes an `fn` as the basis of an `InitialState` implementation for the state type that is returned by the `fn` (on success). +/// +/// The `fn` is expected to build the state type without additional input. +/// Example: +/// ```ignore +/// pub struct B0 {} +/// +/// #[hax_lib_protocol_macros::init_empty(B0)] +/// fn init_b() -> ProtocolResult { +/// Ok(B0 {}) +/// } +/// +/// // The following generated by macro: +/// #[hax_lib_macros::exclude] +/// impl InitialState for B0 { +/// fn init(prologue: Option>) -> ProtocolResult { +/// if let Some(_) = prologue { +/// Err(ProtocolError::InvalidPrologue) +/// } else { +/// init_b() +/// } +/// } +/// } +/// ``` +#[proc_macro_error::proc_macro_error] +#[proc_macro_attribute] +pub fn init_empty( + attr: proc_macro::TokenStream, + item: proc_macro::TokenStream, +) -> proc_macro::TokenStream { + let mut output = quote!(#[hax_lib_macros::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] + impl InitialState for #return_type { + fn init(prologue: Option>) -> ProtocolResult { + if let Some(_) = prologue { + Err(ProtocolError::InvalidPrologue) + } else { + #name() + } + } + } + ); + output.extend(expanded); + + return output.into(); +} + +/// A structure to parse transition tuples from `read` and `write` macros. +struct Transition { + /// `Path` to the current state type of the transition. + pub current_state: syn::Path, + /// `Path` to the destination state type of the transition. + pub next_state: syn::Path, + /// `Path` to the message type this transition is based on. + pub message_type: syn::Path, +} + +impl syn::parse::Parse for Transition { + fn parse(input: parse::ParseStream) -> syn::Result { + use syn::spanned::Spanned; + let punctuated = + syn::punctuated::Punctuated::::parse_terminated(input)?; + if punctuated.len() != 3 { + Err(syn::Error::new( + punctuated.span(), + "Insufficient number of arguments", + )) + } else { + let mut args = punctuated.into_iter(); + Ok(Self { + current_state: args.next().unwrap(), + next_state: args.next().unwrap(), + message_type: args.next().unwrap(), + }) + } + } +} + +/// Macro deriving a `WriteState` implementation for the origin state type, generating a message of `message_type` and a new state, as indicated by the transition tuple. +/// +/// Example: +/// ```ignore +/// #[hax_lib_protocol_macros::write(A0, A1, Message)] +/// fn write_ping(state: A0) -> ProtocolResult<(A1, Message)> { +/// Ok((A1 {}, Message::Ping(state.data))) +/// } +/// +/// // The following generated by macro: +/// #[hax_lib_macros::exclude] +/// impl TryFrom for (A1, Message) { +/// type Error = ProtocolError; +/// +/// fn try_from(value: A0) -> Result { +/// write_ping(value) +/// } +/// } +/// +/// #[hax_lib_macros::exclude] +/// impl WriteState for A0 { +/// type NextState = A1; +/// type Message = Message; +/// +/// fn write(self) -> ProtocolResult<(Self::NextState, Message)> { +/// self.try_into() +/// } +/// } +/// ``` +#[proc_macro_attribute] +pub fn write( + attr: proc_macro::TokenStream, + item: proc_macro::TokenStream, +) -> proc_macro::TokenStream { + let mut output = quote!(#[hax_lib_macros::process_write]); + output.extend(proc_macro2::TokenStream::from(item.clone())); + + let input: syn::ItemFn = parse_macro_input!(item); + let Transition { + current_state, + next_state, + message_type, + } = parse_macro_input!(attr); + + let name = input.sig.ident; + + let expanded = quote!( + #[hax_lib_macros::exclude] + impl TryFrom<#current_state> for (#next_state, #message_type) { + type Error = ProtocolError; + + fn try_from(value: #current_state) -> Result { + #name(value) + } + } + + #[hax_lib_macros::exclude] + impl WriteState for #current_state { + type NextState = #next_state; + type Message = #message_type; + + fn write(self) -> ProtocolResult<(Self::NextState, Self::Message)> { + self.try_into() + } + } + ); + output.extend(expanded); + + return output.into(); +} + +/// Macro deriving a `ReadState` implementation for the destination state type, consuming a message of `message_type` and the current state, as indicated by the transition tuple. +/// +/// Example: +/// ```ignore +/// #[hax_lib_protocol_macros::read(A1, A2, Message)] +/// fn read_pong(_state: A1, msg: Message) -> ProtocolResult { +/// match msg { +/// Message::Ping(_) => Err(ProtocolError::InvalidMessage), +/// Message::Pong(received) => Ok(A2 { received }), +/// } +/// } +/// // The following generated by macro: +/// #[hax_lib_macros::exclude] +/// impl TryFrom<(A1, Message)> for A2 { +/// type Error = ProtocolError; +/// fn try_from((state, msg): (A1, Message)) -> Result { +/// read_pong(state, msg) +/// } +/// } +/// #[hax_lib_macros::exclude] +/// impl ReadState for A1 { +/// type Message = Message; +/// fn read(self, msg: Message) -> ProtocolResult { +/// A2::try_from((self, msg)) +/// } +/// } +/// ``` +#[proc_macro_attribute] +pub fn read( + attr: proc_macro::TokenStream, + item: proc_macro::TokenStream, +) -> proc_macro::TokenStream { + let mut output = quote!(#[hax_lib_macros::process_read]); + output.extend(proc_macro2::TokenStream::from(item.clone())); + + let input: syn::ItemFn = parse_macro_input!(item); + let Transition { + current_state, + next_state, + message_type, + } = parse_macro_input!(attr); + + let name = input.sig.ident; + + let expanded = quote!( + #[hax_lib_macros::exclude] + impl TryFrom<(#current_state, #message_type)> for #next_state { + type Error = ProtocolError; + + fn try_from((state, msg): (#current_state, #message_type)) -> Result { + #name(state, msg) + } + } + + #[hax_lib_macros::exclude] + impl ReadState<#next_state> for #current_state { + type Message = #message_type; + fn read(self, msg: Self::Message) -> ProtocolResult<#next_state> { + #next_state::try_from((self, msg)) + } + } + ); + output.extend(expanded); + + return output.into(); +} From 767b5bd123b967241c19fb72a6b6e0532e9e7ffc Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Mon, 18 Dec 2023 15:54:35 +0100 Subject: [PATCH 03/14] ProVerif: Ping Pong example --- tests/Cargo.lock | 23 ++++++ tests/Cargo.toml | 6 +- tests/proverif/ping-pong/Cargo.toml | 11 +++ tests/proverif/ping-pong/src/a.rs | 97 ++++++++++++++++++++++++ tests/proverif/ping-pong/src/b.rs | 111 ++++++++++++++++++++++++++++ tests/proverif/ping-pong/src/lib.rs | 23 ++++++ 6 files changed, 269 insertions(+), 2 deletions(-) create mode 100644 tests/proverif/ping-pong/Cargo.toml create mode 100644 tests/proverif/ping-pong/src/a.rs create mode 100644 tests/proverif/ping-pong/src/b.rs create mode 100644 tests/proverif/ping-pong/src/lib.rs diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 454628b31..b6b739251 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -106,6 +106,20 @@ dependencies = [ "uuid", ] +[[package]] +name = "hax-lib-protocol" +version = "0.1.0-pre.1" + +[[package]] +name = "hax-lib-protocol-macros" +version = "0.1.0-pre.1" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.28", +] + [[package]] name = "if-let" version = "0.1.0" @@ -237,6 +251,15 @@ dependencies = [ name = "pattern-or" version = "0.1.0" +[[package]] +name = "ping-pong" +version = "0.1.0" +dependencies = [ + "hax-lib-macros", + "hax-lib-protocol", + "hax-lib-protocol-macros", +] + [[package]] name = "proc-macro-error" version = "1.0.4" diff --git a/tests/Cargo.toml b/tests/Cargo.toml index 108febc8a..6ceda9e77 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -22,7 +22,9 @@ members = [ "traits", "reordering", "nested-derefs", - "proverif-minimal", - "proverif-basic-structs" + "proverif/minimal", + "proverif/basic-structs", + "proverif/fn-to-letfun", + "proverif/ping-pong" ] resolver = "2" diff --git a/tests/proverif/ping-pong/Cargo.toml b/tests/proverif/ping-pong/Cargo.toml new file mode 100644 index 000000000..5254a8911 --- /dev/null +++ b/tests/proverif/ping-pong/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "ping-pong" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +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/ping-pong/src/a.rs b/tests/proverif/ping-pong/src/a.rs new file mode 100644 index 000000000..0f72e5f24 --- /dev/null +++ b/tests/proverif/ping-pong/src/a.rs @@ -0,0 +1,97 @@ +use hax_lib_protocol::*; + +use crate::Message; + +// ==== A states ==== +pub struct A0 { + data: u8, +} + +pub struct A1 {} + +pub struct A2 { + #[allow(dead_code)] + received: u8, +} + +// ==== A initialization ==== +#[hax_lib_protocol_macros::init(A0)] +fn init_a(prologue: Vec) -> ProtocolResult { + if prologue.len() < 1 { + Err(ProtocolError::InvalidPrologue) + } else { + Ok(A0 { data: prologue[0] }) + } +} + +// The following generated by macro: +/* #[hax_lib_macros::exclude] +impl TryFrom> for A0 { + type Error = ProtocolError; + + fn try_from(value: Vec) -> Result { + init_a(value) + } +} + +#[hax_lib_macros::exclude] +impl InitialState for A0 { + fn init(prologue: Option>) -> ProtocolResult { + if let Some(prologue) = prologue { + prologue.try_into() + } else { + Err(ProtocolError::InvalidPrologue) + } + } +} */ + +// ==== A state transistion functions ==== +#[hax_lib_protocol_macros::write(A0, A1, Message)] +fn write_ping(state: A0) -> ProtocolResult<(A1, Message)> { + Ok((A1 {}, Message::Ping(state.data))) +} + +// The following generated by macro: +/*#[hax_lib_macros::exclude] +impl TryFrom for (A1, Message) { + type Error = ProtocolError; + + fn try_from(value: A0) -> Result { + write_ping(value) + } +} + +#[hax_lib_macros::exclude] +impl WriteState for A0 { + type NextState = A1; + type Message = Message; + + fn write(self) -> ProtocolResult<(Self::NextState, Message)> { + self.try_into() + } +}*/ + +#[hax_lib_protocol_macros::read(A1, A2, Message)] +fn read_pong(_state: A1, msg: Message) -> ProtocolResult { + match msg { + Message::Ping(_) => Err(ProtocolError::InvalidMessage), + Message::Pong(received) => Ok(A2 { received }), + } +} + +// The following generated by macro: +/*#[hax_lib_macros::exclude] +impl TryFrom<(A1, Message)> for A2 { + type Error = ProtocolError; + + fn try_from((state, msg): (A1, Message)) -> Result { + read_pong(state, msg) + } +} +#[hax_lib_macros::exclude] +impl ReadState for A1 { + type Message = Message; + fn read(self, msg: Message) -> ProtocolResult { + A2::try_from((self, msg)) + } +}*/ diff --git a/tests/proverif/ping-pong/src/b.rs b/tests/proverif/ping-pong/src/b.rs new file mode 100644 index 000000000..edd234679 --- /dev/null +++ b/tests/proverif/ping-pong/src/b.rs @@ -0,0 +1,111 @@ +use hax_lib_protocol::*; + +use crate::Message; + +// ==== B states ==== +pub struct B0 {} + +pub struct B1 { + received: u8, +} + +// An alternative successor of B0 to show read alternatives +pub struct B1alt {} + +pub struct B2 {} + +// ==== B initialization ==== +#[hax_lib_protocol_macros::init_empty(B0)] +fn init_b() -> ProtocolResult { + Ok(B0 {}) +} + +// The following generated by macro: +// #[hax_lib_macros::exclude] +// impl InitialState for B0 { +// fn init(prologue: Option>) -> ProtocolResult { +// if let Some(_) = prologue { +// Err(ProtocolError::InvalidPrologue) +// } else { +// init_b() +// } +// } +// } + +// ==== B state transistion functions ==== +#[hax_lib_protocol_macros::read(B0, B1, Message)] +fn read_ping(_state: B0, msg: Message) -> ProtocolResult { + match msg { + Message::Ping(received) => Ok(B1 { received }), + Message::Pong(_) => Err(ProtocolError::InvalidMessage), + } +} + +// The following generated by macro: +/*#[hax_lib_macros::exclude] +impl TryFrom<(B0, Message)> for B1 { + type Error = ProtocolError; + + fn try_from((state, msg): (B0, Message)) -> Result { + read_ping(state, msg) + } +} + +#[hax_lib_macros::exclude] +impl ReadState for B0 { + type Message = Message; + fn read(self, msg: Message) -> Result { + B1::try_from((self, msg)) + } +}*/ + +#[hax_lib_protocol_macros::read(B0, B1alt, Message)] +fn read_ping_alt(_state: B0, msg: Message) -> ProtocolResult { + match msg { + Message::Ping(received) if received == 42 => Ok(B1alt {}), + _ => Err(ProtocolError::InvalidMessage), + } +} + +// The following generated by macro: +/*#[hax_lib_macros::exclude] +impl TryFrom<(B0, Message)> for B1alt { + type Error = ProtocolError; + + fn try_from((state, msg): (B0, Message)) -> Result { + read_ping_alt(state, msg) + } +} + +#[hax_lib_macros::exclude] +impl ReadState for B0 { + type Message = Message; + fn read(self, msg: Message) -> Result { + B1alt::try_from((self, msg)) + } +}*/ + +#[hax_lib_protocol_macros::write(B1, B2, Message)] +fn write_pong(state: B1) -> ProtocolResult<(B2, Message)> { + Ok((B2 {}, Message::Pong(state.received))) +} + +// The following generated by macro: +/*#[hax_lib_macros::exclude] +impl TryFrom for (B2, Message) { + type Error = ProtocolError; + + fn try_from(value: B1) -> Result { + write_pong(value) + } +} + +#[hax_lib_macros::exclude] +impl WriteState for B1 { + type Message = Message; + type NextState = B2; + + fn write(self) -> Result<(Self::NextState, Message), ProtocolError> { + self.try_into() + } +}*/ diff --git a/tests/proverif/ping-pong/src/lib.rs b/tests/proverif/ping-pong/src/lib.rs new file mode 100644 index 000000000..f72bfd4da --- /dev/null +++ b/tests/proverif/ping-pong/src/lib.rs @@ -0,0 +1,23 @@ +mod a; +mod b; + +#[hax_lib_macros::protocol_messages] +pub enum Message { + Ping(u8), + Pong(u8), +} + +#[test] +fn run() { + use a::A0; + use b::{B0, B1}; + use hax_lib_protocol::{InitialState, ReadState, WriteState}; + let a = A0::init(Some(vec![1])).unwrap(); + let b = B0::init(None).unwrap(); + + let (a, msg) = a.write().unwrap(); + let b: B1 = b.read(msg).unwrap(); + + let (_b, msg) = b.write().unwrap(); + let _a = a.read(msg).unwrap(); +} From 0d65ca53e977f19857ee3aa55f79439c68b6d67f Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 20 Dec 2023 13:54:37 +0100 Subject: [PATCH 04/14] Move ProVerif tests to subdirectory --- .../{proverif-basic-structs => proverif/basic-structs}/Cargo.toml | 0 .../{proverif-basic-structs => proverif/basic-structs}/src/lib.rs | 0 tests/{proverif-minimal => proverif/minimal}/Cargo.toml | 0 tests/{proverif-minimal => proverif/minimal}/src/lib.rs | 0 4 files changed, 0 insertions(+), 0 deletions(-) rename tests/{proverif-basic-structs => proverif/basic-structs}/Cargo.toml (100%) rename tests/{proverif-basic-structs => proverif/basic-structs}/src/lib.rs (100%) rename tests/{proverif-minimal => proverif/minimal}/Cargo.toml (100%) rename tests/{proverif-minimal => proverif/minimal}/src/lib.rs (100%) diff --git a/tests/proverif-basic-structs/Cargo.toml b/tests/proverif/basic-structs/Cargo.toml similarity index 100% rename from tests/proverif-basic-structs/Cargo.toml rename to tests/proverif/basic-structs/Cargo.toml diff --git a/tests/proverif-basic-structs/src/lib.rs b/tests/proverif/basic-structs/src/lib.rs similarity index 100% rename from tests/proverif-basic-structs/src/lib.rs rename to tests/proverif/basic-structs/src/lib.rs diff --git a/tests/proverif-minimal/Cargo.toml b/tests/proverif/minimal/Cargo.toml similarity index 100% rename from tests/proverif-minimal/Cargo.toml rename to tests/proverif/minimal/Cargo.toml diff --git a/tests/proverif-minimal/src/lib.rs b/tests/proverif/minimal/src/lib.rs similarity index 100% rename from tests/proverif-minimal/src/lib.rs rename to tests/proverif/minimal/src/lib.rs From 5e0f517d2e94336ad68a2487867362e2c438b951 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 20 Dec 2023 14:50:59 +0100 Subject: [PATCH 05/14] Fix ProVerif test locations --- tests/Cargo.toml | 7 ++-- .../Cargo.toml | 0 .../src/lib.rs | 0 .../minimal => proverif-minimal}/Cargo.toml | 0 .../minimal => proverif-minimal}/src/lib.rs | 0 tests/proverif-ping-pong/Cargo.toml | 11 ++++++ tests/proverif-ping-pong/pingpong.pv | 39 +++++++++++++++++++ .../ping-pong => proverif-ping-pong}/src/a.rs | 0 .../ping-pong => proverif-ping-pong}/src/b.rs | 0 .../src/lib.rs | 0 tests/proverif/ping-pong/Cargo.toml | 11 ------ 11 files changed, 53 insertions(+), 15 deletions(-) rename tests/{proverif/basic-structs => proverif-basic-structs}/Cargo.toml (100%) rename tests/{proverif/basic-structs => proverif-basic-structs}/src/lib.rs (100%) rename tests/{proverif/minimal => proverif-minimal}/Cargo.toml (100%) rename tests/{proverif/minimal => proverif-minimal}/src/lib.rs (100%) create mode 100644 tests/proverif-ping-pong/Cargo.toml create mode 100644 tests/proverif-ping-pong/pingpong.pv rename tests/{proverif/ping-pong => proverif-ping-pong}/src/a.rs (100%) rename tests/{proverif/ping-pong => proverif-ping-pong}/src/b.rs (100%) rename tests/{proverif/ping-pong => proverif-ping-pong}/src/lib.rs (100%) delete mode 100644 tests/proverif/ping-pong/Cargo.toml diff --git a/tests/Cargo.toml b/tests/Cargo.toml index 6ceda9e77..56a0a52a7 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -22,9 +22,8 @@ members = [ "traits", "reordering", "nested-derefs", - "proverif/minimal", - "proverif/basic-structs", - "proverif/fn-to-letfun", - "proverif/ping-pong" + "proverif-minimal", + "proverif-basic-structs", + "proverif-ping-pong" ] resolver = "2" diff --git a/tests/proverif/basic-structs/Cargo.toml b/tests/proverif-basic-structs/Cargo.toml similarity index 100% rename from tests/proverif/basic-structs/Cargo.toml rename to tests/proverif-basic-structs/Cargo.toml diff --git a/tests/proverif/basic-structs/src/lib.rs b/tests/proverif-basic-structs/src/lib.rs similarity index 100% rename from tests/proverif/basic-structs/src/lib.rs rename to tests/proverif-basic-structs/src/lib.rs diff --git a/tests/proverif/minimal/Cargo.toml b/tests/proverif-minimal/Cargo.toml similarity index 100% rename from tests/proverif/minimal/Cargo.toml rename to tests/proverif-minimal/Cargo.toml diff --git a/tests/proverif/minimal/src/lib.rs b/tests/proverif-minimal/src/lib.rs similarity index 100% rename from tests/proverif/minimal/src/lib.rs rename to tests/proverif-minimal/src/lib.rs diff --git a/tests/proverif-ping-pong/Cargo.toml b/tests/proverif-ping-pong/Cargo.toml new file mode 100644 index 000000000..4eda5a938 --- /dev/null +++ b/tests/proverif-ping-pong/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "ping-pong" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +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-ping-pong/pingpong.pv b/tests/proverif-ping-pong/pingpong.pv new file mode 100644 index 000000000..580ebf491 --- /dev/null +++ b/tests/proverif-ping-pong/pingpong.pv @@ -0,0 +1,39 @@ +set attacker = passive. +channel c. + +type ping_t. +type pong_t. + +fun new_ping(): ping_t. +fun ping2pong(ping_t): pong_t. + +event PingSent(ping_t). +event PingReceived(ping_t). +event PongSent(pong_t). +event PongReceived(pong_t). + +query p: ping_t; + event(PingReceived(p)) ==> event(PingSent(p)). + + + +let A = + ( + let ping = new_ping() in + event PingSent(ping); + out(c, ping) + ) | ( + in(c, pong: pong_t); + event PongReceived(pong) + ). + +let B = + in(c, ping: ping_t); + event PingReceived(ping); + let pong = ping2pong(ping) in + event PongSent(pong); + out(c, pong); + 0. + +process + A | B \ No newline at end of file diff --git a/tests/proverif/ping-pong/src/a.rs b/tests/proverif-ping-pong/src/a.rs similarity index 100% rename from tests/proverif/ping-pong/src/a.rs rename to tests/proverif-ping-pong/src/a.rs diff --git a/tests/proverif/ping-pong/src/b.rs b/tests/proverif-ping-pong/src/b.rs similarity index 100% rename from tests/proverif/ping-pong/src/b.rs rename to tests/proverif-ping-pong/src/b.rs diff --git a/tests/proverif/ping-pong/src/lib.rs b/tests/proverif-ping-pong/src/lib.rs similarity index 100% rename from tests/proverif/ping-pong/src/lib.rs rename to tests/proverif-ping-pong/src/lib.rs diff --git a/tests/proverif/ping-pong/Cargo.toml b/tests/proverif/ping-pong/Cargo.toml deleted file mode 100644 index 5254a8911..000000000 --- a/tests/proverif/ping-pong/Cargo.toml +++ /dev/null @@ -1,11 +0,0 @@ -[package] -name = "ping-pong" -version = "0.1.0" -edition = "2021" - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[dependencies] -hax-lib-protocol = { path = "../../../hax-lib-protocol" } -hax-lib-protocol-macros = { path = "../../../hax-lib-protocol-macros" } -hax-lib-macros = { path = "../../../hax-lib-macros" } From 489e238a80e1ae9ba7d1a2173f31a2402d2a56af Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 13 Dec 2023 08:59:00 +0100 Subject: [PATCH 06/14] Introduce `hax-lib` attribute macros to mark process components --- engine/backends/proverif/proverif_backend.ml | 93 +++++++++++++++++++- engine/lib/attr_payloads.ml | 14 ++- hax-lib-macros/src/lib.rs | 36 ++++++++ hax-lib-macros/types/src/lib.rs | 8 ++ 4 files changed, 148 insertions(+), 3 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index a8c2c1791..7a3625130 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -181,6 +181,71 @@ module Print = struct | Type { name; generics; variants; is_struct } -> if is_struct then fun_and_reduc name variants else empty | _ -> empty + + method! expr_let : lhs:pat -> rhs:expr -> expr fn = + fun ~lhs ~rhs body -> + string "let" ^^ space + ^^ iblock Fn.id (print#pat_at Expr_Let_lhs lhs) + ^^ space ^^ equals ^^ space + ^^ iblock Fn.id (print#expr_at Expr_Let_rhs rhs) + ^^ space ^^ string "in" ^^ hardline + ^^ (print#expr_at Expr_Let_body body |> group) + + method! doc_construct_inductive + : is_record:bool -> + is_struct:bool -> + constructor:concrete_ident -> + base:document option -> + (global_ident * document) list fn = + fun ~is_record ~is_struct:_ ~constructor ~base:_ args -> + if is_record then + string "t_" + (* FIXME: How do I get at the ident from the struct definition instead? *) + ^^ print#concrete_ident constructor + ^^ iblock parens + (separate_map + (break 0 ^^ comma) + (fun (field, body) -> iblock Fn.id body |> group) + args) + else + print#concrete_ident constructor + ^^ iblock parens (separate_map (break 0) snd args) + + method ty : Generic_printer_base.par_state -> ty fn = + fun ctx ty -> + match ty with + | TBool -> print#ty_bool + | TParam i -> print#local_ident i + | TApp _ -> super#ty ctx ty + | _ -> string "bitstring" + + method! expr_app : expr -> expr list -> generic_value list fn = + fun f args _generic_args -> + let dummy_fn = + match List.length args with + | n when n < 8 -> string "dummy_fn_" ^^ PPrint.OCaml.int n + | _ -> string "not_supported" + in + let args = + separate_map + (comma ^^ break 1) + (print#expr_at Expr_App_arg >> group) + args + in + let f = print#expr_at Expr_App_f f |> group in + f ^^ iblock parens args + + method! literal : Generic_printer_base.literal_ctx -> literal fn = + fun _ctx -> function + | String s -> string "no char literals in ProVerif" + | Char c -> string "no char literals in ProVerif" + | Int { value; negative; _ } -> + string "int2bitstring" + ^^ iblock parens + (string value |> precede (if negative then minus else empty)) + | Float { value; kind; negative } -> + string "no float literals in ProVerif" + | Bool b -> OCaml.bool b end include Api (struct @@ -194,10 +259,34 @@ let insert_top_level contents = contents ^ "\n\nprocess\n 0\n" (* Insert ProVerif code that will be necessary in any development.*) let insert_preamble contents = "channel c.\ntype state.\n" ^ contents +let is_process_read : attrs -> bool = + Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.ProcessRead]) + +let is_process_write : attrs -> bool = + Attr_payloads.payloads + >> List.exists ~f:(fst >> [%matches? Types.ProcessWrite]) + +let is_process_init : attrs -> bool = + Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.ProcessInit]) + let translate m (bo : BackendOptions.t) (items : AST.item list) : Types.file list = - let contents, _ = Print.items items in - let contents = contents |> insert_top_level |> insert_preamble in + let processes, rest = + List.partition_tf + ~f:(fun item -> [%matches? Fn _] item.v && is_process_read item.attrs) + items + in + let letfuns, rest = + List.partition_tf ~f:(fun item -> [%matches? Fn _] item.v) rest + in + let letfun_content, _ = Print.items letfuns in + let process_content, _ = Print.items processes in + let contents, _ = Print.items rest in + let contents = + contents ^ "\n(* Process Macros *)\n\n" ^ letfun_content + ^ "\n(* Processes *)" ^ process_content + |> insert_top_level |> insert_preamble + in let file = Types.{ path = "output.pv"; contents } in [ file ] diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml index 1fc2fa8f5..e1e308346 100644 --- a/engine/lib/attr_payloads.ml +++ b/engine/lib/attr_payloads.ml @@ -37,7 +37,15 @@ end module AssocRole = struct module T = struct - type t = Requires | Ensures | Decreases | Refine + type t = + | Requires + | Ensures + | Decreases + | Refine + | ProcessRead + | ProcessWrite + | ProcessInit + | ProtocolMessages [@@deriving show, yojson, compare, sexp, eq] end @@ -54,6 +62,10 @@ module AssocRole = struct | Ensures -> Ensures | Decreases -> Decreases | Refine -> Refine + | ProcessRead -> ProcessRead + | ProcessWrite -> ProcessWrite + | ProcessInit -> ProcessInit + | ProtocolMessages -> ProtocolMessages end module MakeBase (Error : Phase_utils.ERROR) = struct diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs index 1ff405108..f9ce51f80 100644 --- a/hax-lib-macros/src/lib.rs +++ b/hax-lib-macros/src/lib.rs @@ -474,3 +474,39 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr quote! { #item }.into() } + +/// A marker indicating a `fn` as a ProVerif process read. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn process_read(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let item: ItemFn = parse_macro_input!(item); + let attr = AttrPayload::ProcessRead; + quote! {#attr #item}.into() +} + +/// A marker indicating a `fn` as a ProVerif process write. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn process_write(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let item: ItemFn = parse_macro_input!(item); + let attr = AttrPayload::ProcessWrite; + quote! {#attr #item}.into() +} + +/// A marker indicating a `fn` as a ProVerif process initialization. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn process_init(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let item: ItemFn = parse_macro_input!(item); + let attr = AttrPayload::ProcessInit; + quote! {#attr #item}.into() +} + +/// A marker indicating an `enum` as describing the protocol messages. +#[proc_macro_error] +#[proc_macro_attribute] +pub fn protocol_messages(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream { + let item: ItemEnum = parse_macro_input!(item); + let attr = AttrPayload::ProtocolMessages; + quote! {#attr #item}.into() +} diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib-macros/types/src/lib.rs index 639fa0d8c..1caf0ce29 100644 --- a/hax-lib-macros/types/src/lib.rs +++ b/hax-lib-macros/types/src/lib.rs @@ -50,6 +50,10 @@ pub enum AssociationRole { Ensures, Decreases, Refine, + ProcessRead, + ProcessWrite, + ProcessInit, + ProtocolMessages } /// Hax only understands one attribute: `#[hax::json(PAYLOAD)]` where @@ -67,6 +71,10 @@ pub enum AttrPayload { /// Mark an item as a lemma statement to prove in the backend Lemma, Language, + ProcessRead, + ProcessWrite, + ProcessInit, + ProtocolMessages } pub const HAX_TOOL: &str = "_hax"; From f64697ff927b2d77ebfda007835a04870df41e8b Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 20 Dec 2023 16:40:29 +0100 Subject: [PATCH 07/14] Formatting --- hax-lib-macros/types/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib-macros/types/src/lib.rs index 1caf0ce29..293aee2b7 100644 --- a/hax-lib-macros/types/src/lib.rs +++ b/hax-lib-macros/types/src/lib.rs @@ -53,7 +53,7 @@ pub enum AssociationRole { ProcessRead, ProcessWrite, ProcessInit, - ProtocolMessages + ProtocolMessages, } /// Hax only understands one attribute: `#[hax::json(PAYLOAD)]` where @@ -74,7 +74,7 @@ pub enum AttrPayload { ProcessRead, ProcessWrite, ProcessInit, - ProtocolMessages + ProtocolMessages, } pub const HAX_TOOL: &str = "_hax"; From c5b82cb4f090e1f9392172a692520b1415fba07f Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 2 Jan 2024 13:39:22 +0100 Subject: [PATCH 08/14] Break long comment lines --- hax-lib-protocol-macros/src/lib.rs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/hax-lib-protocol-macros/src/lib.rs b/hax-lib-protocol-macros/src/lib.rs index 3ae4d6d0b..dec3412fa 100644 --- a/hax-lib-protocol-macros/src/lib.rs +++ b/hax-lib-protocol-macros/src/lib.rs @@ -1,7 +1,8 @@ use quote::quote; use syn::{parse, parse_macro_input}; -/// This macro takes an `fn` as the basis of an `InitialState` implementation for the state type that is returned by the `fn` (on success). +/// This macro takes an `fn` as the basis of an `InitialState` implementation +/// for the state type that is returned by the `fn` (on success). /// /// The `fn` is expected to build the state type from a `Vec`. /// @@ -76,7 +77,8 @@ pub fn init( return output.into(); } -/// This macro takes an `fn` as the basis of an `InitialState` implementation for the state type that is returned by the `fn` (on success). +/// This macro takes an `fn` as the basis of an `InitialState` implementation +/// for the state type that is returned by the `fn` (on success). /// /// The `fn` is expected to build the state type without additional input. /// Example: @@ -161,7 +163,9 @@ impl syn::parse::Parse for Transition { } } -/// Macro deriving a `WriteState` implementation for the origin state type, generating a message of `message_type` and a new state, as indicated by the transition tuple. +/// Macro deriving a `WriteState` implementation for the origin state type, +/// generating a message of `message_type` and a new state, as indicated by the +/// transition tuple. /// /// Example: /// ```ignore @@ -232,7 +236,9 @@ pub fn write( return output.into(); } -/// Macro deriving a `ReadState` implementation for the destination state type, consuming a message of `message_type` and the current state, as indicated by the transition tuple. +/// Macro deriving a `ReadState` implementation for the destination state type, +/// consuming a message of `message_type` and the current state, as indicated by +/// the transition tuple. /// /// Example: /// ```ignore From 5f2c353a83bf771a526b6345d91c417dd1cbc791 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 2 Jan 2024 13:40:47 +0100 Subject: [PATCH 09/14] Fix sentence --- hax-lib-protocol-macros/src/lib.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/hax-lib-protocol-macros/src/lib.rs b/hax-lib-protocol-macros/src/lib.rs index dec3412fa..c033361da 100644 --- a/hax-lib-protocol-macros/src/lib.rs +++ b/hax-lib-protocol-macros/src/lib.rs @@ -20,7 +20,7 @@ use syn::{parse, parse_macro_input}; /// Ok(A0 { data: prologue[0] }) /// } /// -/// // The following generated by macro: +/// // The following is generated by the macro: /// #[hax_lib_macros::exclude] /// impl TryFrom> for A0 { /// type Error = ProtocolError; @@ -90,7 +90,7 @@ pub fn init( /// Ok(B0 {}) /// } /// -/// // The following generated by macro: +/// // The following is generated by the macro: /// #[hax_lib_macros::exclude] /// impl InitialState for B0 { /// fn init(prologue: Option>) -> ProtocolResult { @@ -174,7 +174,7 @@ impl syn::parse::Parse for Transition { /// Ok((A1 {}, Message::Ping(state.data))) /// } /// -/// // The following generated by macro: +/// // The following is generated by the macro: /// #[hax_lib_macros::exclude] /// impl TryFrom for (A1, Message) { /// type Error = ProtocolError; @@ -249,7 +249,7 @@ pub fn write( /// Message::Pong(received) => Ok(A2 { received }), /// } /// } -/// // The following generated by macro: +/// // The following is generated by the macro: /// #[hax_lib_macros::exclude] /// impl TryFrom<(A1, Message)> for A2 { /// type Error = ProtocolError; From 6d881c94ab6ecc5e3b02ba6b7cb7f3c98e37c54e Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 2 Jan 2024 13:41:52 +0100 Subject: [PATCH 10/14] Explain expected signature for `hax_protocol::init` macro --- hax-lib-protocol-macros/src/lib.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/hax-lib-protocol-macros/src/lib.rs b/hax-lib-protocol-macros/src/lib.rs index c033361da..d2969a9db 100644 --- a/hax-lib-protocol-macros/src/lib.rs +++ b/hax-lib-protocol-macros/src/lib.rs @@ -4,7 +4,9 @@ use syn::{parse, parse_macro_input}; /// This macro takes an `fn` as the basis of an `InitialState` implementation /// for the state type that is returned by the `fn` (on success). /// -/// The `fn` is expected to build the state type from a `Vec`. +/// The `fn` is expected to build the state type from a `Vec`, i.e. the +/// signature should be compatible with `TryFrom>` for the state type +/// given as argument to the macro. /// /// Example: /// ```ignore From 7a1feb982e0a6a6d9b27ea71ae06fcfa14fecbb5 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 2 Jan 2024 15:04:16 +0100 Subject: [PATCH 11/14] Document attribute argument `Path` requirement --- hax-lib-protocol-macros/src/lib.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/hax-lib-protocol-macros/src/lib.rs b/hax-lib-protocol-macros/src/lib.rs index d2969a9db..db9945abe 100644 --- a/hax-lib-protocol-macros/src/lib.rs +++ b/hax-lib-protocol-macros/src/lib.rs @@ -4,9 +4,9 @@ use syn::{parse, parse_macro_input}; /// This macro takes an `fn` as the basis of an `InitialState` implementation /// for the state type that is returned by the `fn` (on success). /// -/// The `fn` is expected to build the state type from a `Vec`, i.e. the -/// signature should be compatible with `TryFrom>` for the state type -/// given as argument to the macro. +/// The `fn` is expected to build the state type specified as a `Path` attribute +/// argument from a `Vec`, i.e. the signature should be compatible with +/// `TryFrom>` for the state type given as argument to the macro. /// /// Example: /// ```ignore @@ -82,7 +82,8 @@ pub fn init( /// This macro takes an `fn` as the basis of an `InitialState` implementation /// for the state type that is returned by the `fn` (on success). /// -/// The `fn` is expected to build the state type without additional input. +/// The `fn` is expected to build the state type specified as a `Path` attribute +/// argument without additional input. /// Example: /// ```ignore /// pub struct B0 {} From d896068443fabac7d1637d3962c711810aa36f48 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 2 Jan 2024 15:05:08 +0100 Subject: [PATCH 12/14] Add documentation for protocol traits --- hax-lib-protocol/src/lib.rs | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/hax-lib-protocol/src/lib.rs b/hax-lib-protocol/src/lib.rs index 1af93d998..19a7ca804 100644 --- a/hax-lib-protocol/src/lib.rs +++ b/hax-lib-protocol/src/lib.rs @@ -1,24 +1,54 @@ +//! This crate provides types and traits for implementing a protocol state +//! machine. +//! +//! + +/// A protocol error type. #[derive(Debug)] pub enum ProtocolError { + /// On receiving an unexpected message, i.e. one that does not allow a state + /// transition from the current state. InvalidMessage, + /// On receiving invalid initialization data. InvalidPrologue, } pub type ProtocolResult = Result; +/// A trait for protocol initial states. pub trait InitialState { + /// Initializes the state given initialization data in `prologue`. + /// + /// Errors on invalid initialization data. fn init(prologue: Option>) -> ProtocolResult where Self: Sized; } +/// A state where a message must be written before transitioning to the next state. +/// +/// `WriteState` can only be implemented once by every state type, implying that +/// in any protocol party state, if a message is to be written, that message and +/// the state the party is in after writing the message are uniquely determined. pub trait WriteState { + /// The uniquely determined state that is transitioned to after writing the message. type NextState; + /// The type of the message that is being written. type Message; + /// Produce the message to be written when transitioning to the next state. fn write(self) -> ProtocolResult<(Self::NextState, Self::Message)>; } +/// A state where a message must be read before transitioning to the next state. +/// +/// A state type may implement `ReadState` multiple times, for different +/// instances of `NextState`, allowing the following state to depend on the +/// message that was received. pub trait ReadState { + /// The type of message to be read. type Message; + + /// Generate the next state based on the current state and the received + /// message. fn read(self, msg: Self::Message) -> ProtocolResult; } From b97baeec4a77e77d0d9b4ee086c4d5179a39dacb Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 2 Jan 2024 15:07:59 +0100 Subject: [PATCH 13/14] Missing newline --- tests/proverif-ping-pong/pingpong.pv | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tests/proverif-ping-pong/pingpong.pv b/tests/proverif-ping-pong/pingpong.pv index 580ebf491..bd6d7a6cb 100644 --- a/tests/proverif-ping-pong/pingpong.pv +++ b/tests/proverif-ping-pong/pingpong.pv @@ -36,4 +36,5 @@ let B = 0. process - A | B \ No newline at end of file + A | B + \ No newline at end of file From c66445d70f8866b4245e569359656c44a1580812 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 2 Jan 2024 15:14:12 +0100 Subject: [PATCH 14/14] More crate-level comments --- hax-lib-protocol/src/lib.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/hax-lib-protocol/src/lib.rs b/hax-lib-protocol/src/lib.rs index 19a7ca804..d58a6ed58 100644 --- a/hax-lib-protocol/src/lib.rs +++ b/hax-lib-protocol/src/lib.rs @@ -1,7 +1,10 @@ //! This crate provides types and traits for implementing a protocol state //! machine. //! -//! +//! A protocol party is conceived of as having a set of possible states, one of +//! which is the initial state. Transitioning to a different state is possible +//! either through receiving and processing a message or through writing a +//! message. /// A protocol error type. #[derive(Debug)]