From 0f95c1569d6ddcf977213bec6ee662689435f35c Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 21 Nov 2023 13:48:37 +0100 Subject: [PATCH 1/8] Extend ProVerif boilerplate by state type. --- engine/backends/proverif/proverif_backend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 00b5620a6..b540c602c 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -133,7 +133,7 @@ end 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.\n\n" ^ contents +let insert_preamble contents = "channel c.\ntype state.\n" ^ contents let translate m (bo : BackendOptions.t) (items : AST.item list) : Types.file list = From cf473b4845440d45c4335f56a17912820be81584 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 21 Nov 2023 13:50:37 +0100 Subject: [PATCH 2/8] Simple translation of `structs` to `fun`s and `reduc`s --- engine/backends/proverif/proverif_backend.ml | 27 ++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index b540c602c..7408c50bb 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -113,15 +113,38 @@ module Print = struct method ty_bool = string "bool" method ty_int _ = string "bitstring" + method! item' item = + let fun_and_reduc name variants = + let constructor = List.hd variants in + match constructor with + | None -> empty + | Some constructor -> + let field_prefix = if constructor.is_record then string "" else print#concrete_ident name in + let fun_args = constructor.arguments in + let fun_args_full = separate_map (comma ^^ break 1) (fun (x, y, _z) -> field_prefix ^^ print#concrete_ident x ^^ string ": " ^^ print#ty_at Param_typ y) fun_args in + let fun_args_names = separate_map (comma ^^ break 1) (fst3 >> (fun x -> field_prefix ^^ print#concrete_ident x)) fun_args in + let fun_args_types = separate_map (comma ^^ break 1) (snd3 >> print#ty_at Param_typ) fun_args in + let fun_line = string "fun" ^^ space ^^ print#concrete_ident name ^^ (iblock parens fun_args_types) ^^ string ": state." in + let reduc_line = string "reduc forall " ^^ (iblock Fn.id fun_args_full) ^^ string ";" in + let build_accessor (ident, ty, attr) = string "accessor_" ^^ print#concrete_ident name ^^ string "_" ^^ print#concrete_ident ident ^^ iblock parens fun_args_names ^^ string " = " ^^ field_prefix ^^ print#concrete_ident ident in + let reduc_lines = separate_map (string "." ^^ hardline) (fun arg -> reduc_line ^^ (nest 4 (hardline ^^ (build_accessor arg)))) fun_args + in + fun_line ^^ hardline ^^ reduc_lines ^^ string "." + in match item with + (* `fn`s are transformed into `letfun` process macros. *) | Fn { name; generics; body; params } -> let params_string = iblock parens (separate_map (comma ^^ break 1) print#param params) in string "letfun" ^^ space ^^ print#concrete_ident name - ^^ params_string ^^ string " = 0." - | _ -> string "" + ^^ params_string ^^ string " =" ^^ nest 4 (hardline ^^ print#expr_at Item_Fn_body body ^^ string ".") + (* `struct` definitions are transformed into simple constructors and `reduc`s for accessing fields. *) + | Type {name; generics; variants; is_struct} -> + if is_struct then fun_and_reduc name variants else empty + | _ -> empty + end include Api (struct From 5a8adb192eab55d748278131426614033b8462b6 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 21 Nov 2023 13:53:25 +0100 Subject: [PATCH 3/8] ProVerif: Basic struct translation test --- tests/Cargo.lock | 4 ++++ tests/Cargo.toml | 3 ++- tests/proverif-basic-structs/Cargo.toml | 11 +++++++++++ tests/proverif-basic-structs/src/lib.rs | 13 +++++++++++++ 4 files changed, 30 insertions(+), 1 deletion(-) create mode 100644 tests/proverif-basic-structs/Cargo.toml create mode 100644 tests/proverif-basic-structs/src/lib.rs diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 5da19ad74..b96f861d3 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -265,6 +265,10 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "proverif-basic-structs" +version = "0.1.0" + [[package]] name = "proverif-minimal" version = "0.1.0" diff --git a/tests/Cargo.toml b/tests/Cargo.toml index d7879e02c..108febc8a 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -22,6 +22,7 @@ members = [ "traits", "reordering", "nested-derefs", - "proverif-minimal" + "proverif-minimal", + "proverif-basic-structs" ] resolver = "2" diff --git a/tests/proverif-basic-structs/Cargo.toml b/tests/proverif-basic-structs/Cargo.toml new file mode 100644 index 000000000..183dae7e9 --- /dev/null +++ b/tests/proverif-basic-structs/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "proverif-basic-structs" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] + +[package.metadata.hax-tests] +into."pro-verif" = { broken = false, snapshot = "none" } diff --git a/tests/proverif-basic-structs/src/lib.rs b/tests/proverif-basic-structs/src/lib.rs new file mode 100644 index 000000000..8036edc23 --- /dev/null +++ b/tests/proverif-basic-structs/src/lib.rs @@ -0,0 +1,13 @@ +// Record struct with single field +struct A_initial { + x: u8, +} + +// Record struct with multiple fields +struct A { + one: usize, + two: usize, +} + +// Non-record struct +struct B(usize); From 7524e436959fde1bda50f210add7055f261490b9 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 21 Nov 2023 13:57:29 +0100 Subject: [PATCH 4/8] Remove test warning --- tests/proverif-basic-structs/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/proverif-basic-structs/src/lib.rs b/tests/proverif-basic-structs/src/lib.rs index 8036edc23..2b278202c 100644 --- a/tests/proverif-basic-structs/src/lib.rs +++ b/tests/proverif-basic-structs/src/lib.rs @@ -1,5 +1,5 @@ // Record struct with single field -struct A_initial { +struct Ainitial { x: u8, } From ab76dfbe1ddd0604c2f603ce4521566795ad3daf Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 21 Nov 2023 14:22:11 +0100 Subject: [PATCH 5/8] Ocamlformat --- engine/backends/proverif/proverif_backend.ml | 70 +++++++++++++++----- 1 file changed, 53 insertions(+), 17 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 7408c50bb..6f093a2b1 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -113,25 +113,61 @@ module Print = struct method ty_bool = string "bool" method ty_int _ = string "bitstring" - method! item' item = - let fun_and_reduc name variants = + let fun_and_reduc name variants = let constructor = List.hd variants in match constructor with | None -> empty | Some constructor -> - let field_prefix = if constructor.is_record then string "" else print#concrete_ident name in - let fun_args = constructor.arguments in - let fun_args_full = separate_map (comma ^^ break 1) (fun (x, y, _z) -> field_prefix ^^ print#concrete_ident x ^^ string ": " ^^ print#ty_at Param_typ y) fun_args in - let fun_args_names = separate_map (comma ^^ break 1) (fst3 >> (fun x -> field_prefix ^^ print#concrete_ident x)) fun_args in - let fun_args_types = separate_map (comma ^^ break 1) (snd3 >> print#ty_at Param_typ) fun_args in - let fun_line = string "fun" ^^ space ^^ print#concrete_ident name ^^ (iblock parens fun_args_types) ^^ string ": state." in - let reduc_line = string "reduc forall " ^^ (iblock Fn.id fun_args_full) ^^ string ";" in - let build_accessor (ident, ty, attr) = string "accessor_" ^^ print#concrete_ident name ^^ string "_" ^^ print#concrete_ident ident ^^ iblock parens fun_args_names ^^ string " = " ^^ field_prefix ^^ print#concrete_ident ident in - let reduc_lines = separate_map (string "." ^^ hardline) (fun arg -> reduc_line ^^ (nest 4 (hardline ^^ (build_accessor arg)))) fun_args - in - fun_line ^^ hardline ^^ reduc_lines ^^ string "." - in + let field_prefix = + if constructor.is_record then string "" + else print#concrete_ident name + in + let fun_args = constructor.arguments in + let fun_args_full = + separate_map + (comma ^^ break 1) + (fun (x, y, _z) -> + field_prefix ^^ print#concrete_ident x ^^ string ": " + ^^ print#ty_at Param_typ y) + fun_args + in + let fun_args_names = + separate_map + (comma ^^ break 1) + (fst3 >> fun x -> field_prefix ^^ print#concrete_ident x) + fun_args + in + let fun_args_types = + separate_map + (comma ^^ break 1) + (snd3 >> print#ty_at Param_typ) + fun_args + in + let fun_line = + string "fun" ^^ space ^^ print#concrete_ident name + ^^ iblock parens fun_args_types + ^^ string ": state." + in + let reduc_line = + string "reduc forall " ^^ iblock Fn.id fun_args_full + ^^ string ";" + in + let build_accessor (ident, ty, attr) = + string "accessor_" ^^ print#concrete_ident name ^^ string "_" + ^^ print#concrete_ident ident + ^^ iblock parens fun_args_names + ^^ string " = " ^^ field_prefix ^^ print#concrete_ident ident + in + let reduc_lines = + separate_map + (string "." ^^ hardline) + (fun arg -> + reduc_line ^^ nest 4 (hardline ^^ build_accessor arg)) + fun_args + in + fun_line ^^ hardline ^^ reduc_lines ^^ string "." + in match item with (* `fn`s are transformed into `letfun` process macros. *) | Fn { name; generics; body; params } -> @@ -139,12 +175,12 @@ module Print = struct iblock parens (separate_map (comma ^^ break 1) print#param params) in string "letfun" ^^ space ^^ print#concrete_ident name - ^^ params_string ^^ string " =" ^^ nest 4 (hardline ^^ print#expr_at Item_Fn_body body ^^ string ".") + ^^ params_string ^^ string " =" + ^^ nest 4 (hardline ^^ print#expr_at Item_Fn_body body ^^ string ".") (* `struct` definitions are transformed into simple constructors and `reduc`s for accessing fields. *) - | Type {name; generics; variants; is_struct} -> + | Type { name; generics; variants; is_struct } -> if is_struct then fun_and_reduc name variants else empty | _ -> empty - end include Api (struct From d19cfb34b0a61bbb1897771629ca10b0056777d9 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 21 Nov 2023 14:32:00 +0100 Subject: [PATCH 6/8] Fix accessor definition --- engine/backends/proverif/proverif_backend.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 6f093a2b1..69214491d 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -156,7 +156,8 @@ module Print = struct let build_accessor (ident, ty, attr) = string "accessor_" ^^ print#concrete_ident name ^^ string "_" ^^ print#concrete_ident ident - ^^ iblock parens fun_args_names + ^^ iblock parens + (print#concrete_ident name ^^ iblock parens fun_args_names) ^^ string " = " ^^ field_prefix ^^ print#concrete_ident ident in let reduc_lines = From 3f79e4ffca7f75c67dd41687dad8c2e2b85d3b95 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 22 Nov 2023 09:05:35 +0100 Subject: [PATCH 7/8] Use more of `PPrint`s character combinators --- engine/backends/proverif/proverif_backend.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 69214491d..c34c72ebc 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -120,7 +120,7 @@ module Print = struct | None -> empty | Some constructor -> let field_prefix = - if constructor.is_record then string "" + if constructor.is_record then empty else print#concrete_ident name in let fun_args = constructor.arguments in @@ -151,23 +151,23 @@ module Print = struct in let reduc_line = string "reduc forall " ^^ iblock Fn.id fun_args_full - ^^ string ";" + ^^ semi in let build_accessor (ident, ty, attr) = - string "accessor_" ^^ print#concrete_ident name ^^ string "_" + string "accessor_" ^^ print#concrete_ident name ^^ underscore ^^ print#concrete_ident ident ^^ iblock parens (print#concrete_ident name ^^ iblock parens fun_args_names) - ^^ string " = " ^^ field_prefix ^^ print#concrete_ident ident + ^^ blank 1 ^^ equals ^^ blank 1 ^^ field_prefix ^^ print#concrete_ident ident in let reduc_lines = separate_map - (string "." ^^ hardline) + (dot ^^ hardline) (fun arg -> reduc_line ^^ nest 4 (hardline ^^ build_accessor arg)) fun_args in - fun_line ^^ hardline ^^ reduc_lines ^^ string "." + fun_line ^^ hardline ^^ reduc_lines ^^ dot in match item with (* `fn`s are transformed into `letfun` process macros. *) @@ -176,8 +176,8 @@ module Print = struct iblock parens (separate_map (comma ^^ break 1) print#param params) in string "letfun" ^^ space ^^ print#concrete_ident name - ^^ params_string ^^ string " =" - ^^ nest 4 (hardline ^^ print#expr_at Item_Fn_body body ^^ string ".") + ^^ params_string ^/^ equals + ^^ nest 4 (hardline ^^ print#expr_at Item_Fn_body body ^^ dot) (* `struct` definitions are transformed into simple constructors and `reduc`s for accessing fields. *) | Type { name; generics; variants; is_struct } -> if is_struct then fun_and_reduc name variants else empty From 1c6afc628f3edfea391a8b7912ab66f1e4ebfa1f Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 22 Nov 2023 09:08:02 +0100 Subject: [PATCH 8/8] Formatting --- engine/backends/proverif/proverif_backend.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index c34c72ebc..a8c2c1791 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -150,19 +150,18 @@ module Print = struct ^^ string ": state." in let reduc_line = - string "reduc forall " ^^ iblock Fn.id fun_args_full - ^^ semi + string "reduc forall " ^^ iblock Fn.id fun_args_full ^^ semi in let build_accessor (ident, ty, attr) = string "accessor_" ^^ print#concrete_ident name ^^ underscore ^^ print#concrete_ident ident ^^ iblock parens (print#concrete_ident name ^^ iblock parens fun_args_names) - ^^ blank 1 ^^ equals ^^ blank 1 ^^ field_prefix ^^ print#concrete_ident ident + ^^ blank 1 ^^ equals ^^ blank 1 ^^ field_prefix + ^^ print#concrete_ident ident in let reduc_lines = - separate_map - (dot ^^ hardline) + separate_map (dot ^^ hardline) (fun arg -> reduc_line ^^ nest 4 (hardline ^^ build_accessor arg)) fun_args