From bebd3e546ab4d11ca16e1ab1e72c50510fcf4150 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 13 Feb 2024 15:45:04 +0100 Subject: [PATCH 01/46] Add some documentation for generic printer --- .../lib/generic_printer/generic_printer_base.ml | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/engine/lib/generic_printer/generic_printer_base.ml b/engine/lib/generic_printer/generic_printer_base.ml index 164442ec8..38c96a00d 100644 --- a/engine/lib/generic_printer/generic_printer_base.ml +++ b/engine/lib/generic_printer/generic_printer_base.ml @@ -3,10 +3,11 @@ open! Ast open PPrint (** Generic printer for the {!module:Ast} ASTs. It uses the [PPrint] -library, and additionaly computes {!Annotation.t}. *) +library, and additionally computes {!Annotation.t}. *) -(** Identifies a position in the AST. This is useful for figuring out -wether we should wrap a chunk of AST in parenthesis. or not *) +(** Identifies a position in the AST. This is useful for figuring out wether we + should wrap a chunk of AST in parenthesis, or not, or for implementing + special treatment of some sub-trees if they occur in a certain context. *) type ast_position = | GenericValue_GType | GenericValue_GConst @@ -68,6 +69,8 @@ type annot_str = string * Annotation.t list [@@deriving show, yojson, eq] ({!NeedsPar}) or not ({!AlreadyPar})? *) type par_state = NeedsPar | AlreadyPar +(** The context of a literal in the AST, does it appear in a pattern ({!Pat}) or + in an expression ({!Expr})?*) type literal_ctx = Pat | Expr module Make (F : Features.T) = struct @@ -108,6 +111,10 @@ module Make (F : Features.T) = struct method compact : output -> unit = fun o -> compact o doc end + (** Print a concrete identifier. + + Differentiates between encounters of the identifier in its own namespace + or a foreign namespace.*) method concrete_ident : concrete_ident fn = fun id -> let current_ns = print#get_current_namespace () in @@ -253,7 +260,10 @@ module Make (F : Features.T) = struct make_hax_error_item i.span i.ident msg |> print#item method items : item list fn = separate_map (twice hardline) print#item + (** Print given list of items, separating them by two newlines each.*) + method attrs : attrs fn = separate_map hardline print#attr + (** Print given list of attributes, separating them by one newline each.*) end type print_object = @@ -273,6 +283,7 @@ module Make (F : Features.T) = struct method printer_name : string method get_span_data : unit -> Annotation.t list + (** The namespace a concrete identifier was defined in. *) method namespace_of_concrete_ident : concrete_ident -> string * string list From 7d9d9fcd68b437e0b4af9597750b4c8fd272a999 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 13 Feb 2024 15:45:22 +0100 Subject: [PATCH 02/46] "Flatten" tuple types in generic type arguments --- engine/backends/proverif/proverif_backend.ml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index fb5e956b7..a3a34c6e5 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -529,6 +529,22 @@ module Print = struct method ty_app f args = print#concrete_ident f ^^ print#generic_values args + method generic_arg_n_tuple n args = + string "tuple" ^^ OCaml.int n ^^ underscore + ^^ separate_map underscore print#generic_value args + + method ty_at : Generic_printer_base.ast_position -> ty fn = + fun position -> + let otherwise = print#par_state position |> print#ty in + match position with + | GenericValue_GType -> ( + fun ty -> + match ty with + | TApp { ident = `TupleType n; args } -> + print#generic_arg_n_tuple n args + | _ -> otherwise ty) + | _ -> otherwise + method ty : Generic_printer_base.par_state -> ty fn = fun ctx ty -> match ty with From 356720ce7cc4354257957feb92e4977d45d53762 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 13 Feb 2024 16:53:19 +0100 Subject: [PATCH 03/46] Running enumeration of wildcards (per print object) --- engine/backends/proverif/proverif_backend.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index a3a34c6e5..e9fecd62c 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -274,6 +274,11 @@ module Print = struct method ty_bool = string "bool" method ty_int _ = string "nat" + val mutable wildcard_index = 0 + + method wildcard = + wildcard_index <- wildcard_index + 1; + string "wildcard" ^^ OCaml.int wildcard_index method pat' : Generic_printer_base.par_state -> pat' fn = fun ctx -> @@ -289,6 +294,9 @@ module Print = struct with | Some (_, translation) -> translation args | None -> super#pat' ctx pat) + | PWild -> + print#wildcard + (* NOTE: Wildcard translation without collisions? *) | _ -> super#pat' ctx pat method tuple_elem_pat' : Generic_printer_base.par_state -> pat' fn = From e8395f2ff82744ef03d77d0c23894cff35f11c52 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 13 Feb 2024 16:54:03 +0100 Subject: [PATCH 04/46] Use parens instead of braces --- engine/backends/proverif/proverif_backend.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index e9fecd62c..2cf9e23ac 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -284,7 +284,7 @@ module Print = struct fun ctx -> let wrap_parens = group - >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces + >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens in fun pat -> match pat with @@ -303,7 +303,7 @@ module Print = struct fun ctx -> let wrap_parens = group - >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces + >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens in function | PBinding { mut; mode; var; typ; subpat } -> @@ -342,7 +342,7 @@ module Print = struct fun ctx e -> let wrap_parens = group - >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces + >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens in match e with (* Translate known functions *) @@ -399,6 +399,13 @@ module Print = struct if_then ^^ break 1 ^^ string "else" ^^ space ^^ (print#expr_at Expr_If_else else_ |> iblock parens)) |> wrap_parens + | Let { monadic; lhs; rhs; body } -> + (Option.map + ~f:(fun monad -> print#expr_monadic_let ~monad) + monadic + |> Option.value ~default:print#expr_let) + ~lhs ~rhs body + |> wrap_parens | _ -> super#expr' ctx e method concrete_ident = print#concrete_ident' ~under_current_ns:false From 05df22897fc88dd9773214b3bf0229f826c670c8 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 13 Feb 2024 16:54:27 +0100 Subject: [PATCH 05/46] Translate logical operations to their PV equivalents --- engine/backends/proverif/proverif_backend.ml | 37 +++++++++++++------- 1 file changed, 25 insertions(+), 12 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 2cf9e23ac..f39f34697 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -347,18 +347,31 @@ module Print = struct match e with (* Translate known functions *) | App { f = { e = GlobalVar name; _ }; args } -> ( - match translate_known_name name ~dict:library_functions with - | Some (name, translation) -> translation args - | None -> ( - match name with - | `Projector (`Concrete name) -> - print#field_accessor name - ^^ iblock parens - (separate_map - (comma ^^ break 1) - (fun arg -> print#expr AlreadyPar arg) - args) - | _ -> super#expr' ctx e)) + match name with + | `Primitive p -> ( + match p with + | LogicalOp And -> + print#expr NeedsPar (List.hd_exn args) + ^^ space ^^ string "&&" ^^ space + ^^ print#expr NeedsPar (List.nth_exn args 1) + | LogicalOp Or -> + print#expr NeedsPar (List.hd_exn args) + ^^ space ^^ string "||" ^^ space + ^^ print#expr NeedsPar (List.nth_exn args 1) + | _ -> empty) + | _ -> ( + match translate_known_name name ~dict:library_functions with + | Some (name, translation) -> translation args + | None -> ( + match name with + | `Projector (`Concrete name) -> + print#field_accessor name + ^^ iblock parens + (separate_map + (comma ^^ break 1) + (fun arg -> print#expr AlreadyPar arg) + args) + | _ -> super#expr' ctx e))) | Construct { constructor; fields; _ } when Global_ident.eq_name Core__result__Result__Ok constructor -> super#expr' ctx (snd (Option.value_exn (List.hd fields))).e From d1a89779744ee7f94d902bbf39b80ee2cdb42676 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 09:17:43 +0100 Subject: [PATCH 06/46] Mark casts as todo --- engine/backends/proverif/proverif_backend.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index f39f34697..d33af2087 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -358,6 +358,7 @@ module Print = struct print#expr NeedsPar (List.hd_exn args) ^^ space ^^ string "||" ^^ space ^^ print#expr NeedsPar (List.nth_exn args 1) + | Cast -> string "todo_cast_as" | _ -> empty) | _ -> ( match translate_known_name name ~dict:library_functions with From d266ad1414d17d7680e616041013b12ddef7103c Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 15 Feb 2024 12:08:57 +0100 Subject: [PATCH 07/46] fix(engine/print-rust): `impl ...` local_idents --- engine/lib/print_rust.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml index feb7961c1..13f9bd8aa 100644 --- a/engine/lib/print_rust.ml +++ b/engine/lib/print_rust.ml @@ -101,7 +101,16 @@ module Raw = struct let pglobal_ident = pglobal_ident' "" let plocal_ident span (e : Local_ident.t) : AnnotatedString.t = - pure span e.name + let name = + match String.chop_prefix ~prefix:"impl " e.name with + | Some name -> + "impl_" + ^ String.map + ~f:(function 'a' .. 'Z' as letter -> letter | _ -> '_') + name + | _ -> e.name + in + pure span name let dmutability span : _ -> AnnotatedString.t = pure span << function Mutable _ -> "mut " | _ -> "" From 3210877f327c5fc711ea8ddf717398260fe99d2e Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 12:09:44 +0100 Subject: [PATCH 08/46] Strip QuestionMarks --- .utils/rebuild.sh | 2 +- engine/backends/proverif/proverif_backend.ml | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/.utils/rebuild.sh b/.utils/rebuild.sh index 48e28b3b6..348621191 100755 --- a/.utils/rebuild.sh +++ b/.utils/rebuild.sh @@ -33,7 +33,7 @@ rust () { cd_rootwise "cli" for i in driver subcommands ../engine/names/extract; do CURRENT="rust/$i" - cargo install --quiet $OFFLINE_FLAG --debug --path $i + cargo install --locked --quiet $OFFLINE_FLAG --debug --path $i done } diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index d33af2087..c2e7a99a6 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -345,6 +345,7 @@ module Print = struct >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens in match e with + | QuestionMark { e; _ } -> print#expr ctx e (* Translate known functions *) | App { f = { e = GlobalVar name; _ }; args } -> ( match name with From ed41c695bd3b59d8389cbdb626c22408c0152135 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 12:10:03 +0100 Subject: [PATCH 09/46] Translate local_ident --- engine/backends/proverif/proverif_backend.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index c2e7a99a6..8a47fff1b 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -575,6 +575,17 @@ module Print = struct | _ -> otherwise ty) | _ -> otherwise + method local_ident e = + match String.chop_prefix ~prefix:"impl " e.name with + | Some name -> + let name = + "impl_" + ^ String.tr ~target:'+' ~replacement:'_' + (String.tr ~target:' ' ~replacement:'_' name) + in + string name + | _ -> super#local_ident e + method ty : Generic_printer_base.par_state -> ty fn = fun ctx ty -> match ty with From 76e25abec051b22a3bafb8ee30db3a4f1f910e2a Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 12:10:22 +0100 Subject: [PATCH 10/46] Take out hoisting --- 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 8a47fff1b..831834339 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -732,7 +732,7 @@ module TransformToInputLanguage = |> Phases.Drop_blocks |> Phases.Drop_references |> Phases.Trivialize_assign_lhs - |> Side_effect_utils.Hoist + (* |> Side_effect_utils.Hoist *) |> Phases.Local_mutation |> Phases.Reject.Continue |> Phases.Reconstruct_question_marks From 640692eb659ed4e94d07d0316b3c2fb014109a46 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 12:10:38 +0100 Subject: [PATCH 11/46] Translate tuples in parameters --- 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 831834339..fa870ae4f 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -567,7 +567,7 @@ module Print = struct fun position -> let otherwise = print#par_state position |> print#ty in match position with - | GenericValue_GType -> ( + | GenericValue_GType | Param_typ -> ( fun ty -> match ty with | TApp { ident = `TupleType n; args } -> From d911b9153c666ea149101f40d25e8bcbd32152fc Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 14:01:07 +0100 Subject: [PATCH 12/46] Insert parens instead of braces --- 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 fa870ae4f..186bd8a76 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -396,7 +396,7 @@ module Print = struct } (*[@ocamlformat "disable"]*) when Global_ident.eq_name Core__ops__try_trait__Try__branch n -> - super#expr' ctx expr.e + print#expr' ctx expr.e | Match { scrutinee; arms } -> separate_map (hardline ^^ string "else ") From 9539bbe11d875c036dc49254e931df0f10ab97d3 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 14:01:23 +0100 Subject: [PATCH 13/46] Treat casts as identity --- 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 186bd8a76..d4a4581c5 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -359,7 +359,7 @@ module Print = struct print#expr NeedsPar (List.hd_exn args) ^^ space ^^ string "||" ^^ space ^^ print#expr NeedsPar (List.nth_exn args 1) - | Cast -> string "todo_cast_as" + | Cast -> print#expr NeedsPar (List.hd_exn args) | _ -> empty) | _ -> ( match translate_known_name name ~dict:library_functions with From 8c36e13085da9539d5697833085622815e325625 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 14:01:36 +0100 Subject: [PATCH 14/46] Translate `never_to_any` as fail --- engine/backends/proverif/proverif_backend.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index d4a4581c5..2836486f5 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -115,6 +115,7 @@ module Print = struct let library_functions : (Concrete_ident_generated.name * (AST.expr list -> document)) list = [ (* (\* Core dependencies *\) *) + (Rust_primitives__hax__never_to_any, fun _ -> string "construct_fail()") (* (Alloc__vec__from_elem, fun args -> string "PLACEHOLDER_library_function"); *) (* ( Alloc__slice__Impl__to_vec, *) (* fun args -> string "PLACEHOLDER_library_function" ); *) From c32cc3e9a6eeb8d354aedc122ba4d93ca053d640 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 15 Feb 2024 13:52:57 +0100 Subject: [PATCH 15/46] feat(backend/proverif): add `assume_item` flag --- cli/driver/src/exporter.rs | 2 +- cli/options/src/lib.rs | 15 +- engine/backends/proverif/proverif_backend.ml | 1237 +++++++++-------- engine/backends/proverif/proverif_backend.mli | 2 +- engine/bin/lib.ml | 4 +- .../generic_printer/generic_printer_base.ml | 10 +- 6 files changed, 670 insertions(+), 600 deletions(-) diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs index 802363231..4e023d31a 100644 --- a/cli/driver/src/exporter.rs +++ b/cli/driver/src/exporter.rs @@ -390,7 +390,7 @@ impl Callbacks for ExtractionCallbacks { } } ExporterCommand::Backend(backend) => { - if matches!(backend.backend, Backend::Easycrypt | Backend::ProVerif) { + if matches!(backend.backend, Backend::Easycrypt | Backend::ProVerif(..)) { eprintln!( "⚠️ Warning: Experimental backend \"{}\" is work in progress.", backend.backend diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs index 58a953e12..c1d8f2b0d 100644 --- a/cli/options/src/lib.rs +++ b/cli/options/src/lib.rs @@ -113,6 +113,17 @@ impl NormalizePaths for PathOrDash { } } +#[derive(JsonSchema, Parser, Debug, Clone, Serialize, Deserialize)] +pub struct ProVerifOptions { + #[arg( + long, + value_parser = parse_inclusion_clause, + value_delimiter = ' ', + allow_hyphen_values(true) + )] + assume_items: Vec, +} + #[derive(JsonSchema, Parser, Debug, Clone, Serialize, Deserialize)] pub struct FStarOptions { /// Set the Z3 per-query resource limit @@ -151,7 +162,7 @@ pub enum Backend { /// Use the EasyCrypt backend (warning: work in progress!) Easycrypt, /// Use the ProVerif backend (warning: work in progress!) - ProVerif, + ProVerif(ProVerifOptions), } impl fmt::Display for Backend { @@ -160,7 +171,7 @@ impl fmt::Display for Backend { Backend::Fstar(..) => write!(f, "fstar"), Backend::Coq => write!(f, "coq"), Backend::Easycrypt => write!(f, "easycrypt"), - Backend::ProVerif => write!(f, "proverif"), + Backend::ProVerif(..) => write!(f, "proverif"), } } } diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 2836486f5..cec87f16a 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -78,7 +78,10 @@ struct let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend)) end -module BackendOptions = Backend.UnitBackendOptions +module BackendOptions = struct + type t = Hax_engine.Types.pro_verif_options +end + open Ast module ProVerifNamePolicy = struct @@ -102,617 +105,673 @@ end module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (ProVerifNamePolicy) open AST -module Print = struct - module GenericPrint = - Generic_printer.Make (InputLanguage) (U.Concrete_ident_view) - - open Generic_printer_base.Make (InputLanguage) - open PPrint - - let iblock f = group >> jump 2 0 >> terminate (break 0) >> f >> group - - (* TODO: Give definitions for core / known library functions, cf issues #447, #448 *) - let library_functions : - (Concrete_ident_generated.name * (AST.expr list -> document)) list = - [ (* (\* Core dependencies *\) *) - (Rust_primitives__hax__never_to_any, fun _ -> string "construct_fail()") - (* (Alloc__vec__from_elem, fun args -> string "PLACEHOLDER_library_function"); *) - (* ( Alloc__slice__Impl__to_vec, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (Core__slice__Impl__len, fun args -> string "PLACEHOLDER_library_function"); *) - (* ( Core__ops__deref__Deref__deref, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Core__ops__index__Index__index, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Rust_primitives__unsize, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Core__num__Impl_9__to_le_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__slice__Impl__into_vec, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__vec__Impl_1__truncate, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__vec__Impl_2__extend_from_slice, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__slice__Impl__concat, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Core__option__Impl__is_some, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::clone::Clone_f_clone *\) *) - (* ( Core__clone__Clone__clone, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::cmp::PartialEq::eq *\) *) - (* ( Core__cmp__PartialEq__eq, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::cmp::PartialEq_f_ne *\) *) - (* ( Core__cmp__PartialEq__ne, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::cmp::PartialOrd::lt *\) *) - (* ( Core__cmp__PartialOrd__lt, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::ops::arith::Add::add *\) *) - (* ( Core__ops__arith__Add__add, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::ops::arith::Sub::sub *\) *) - (* ( Core__ops__arith__Sub__sub, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::option::Option_Option_None_c *\) *) - (* ( Core__option__Option__None, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::option::Option_Option_Some_c *\) *) - (* ( Core__option__Option__Some, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::result::impl__map_err *\) *) - (* ( Core__result__Impl__map_err, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* Crypto dependencies *\) *) - (* (\* hax_lib_protocol::cal::hash *\) *) - (* ( Hax_lib_protocol__crypto__hash, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::hmac *\) *) - (* ( Hax_lib_protocol__crypto__hmac, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::aead_decrypt *\) *) - (* ( Hax_lib_protocol__crypto__aead_decrypt, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::aead_encrypt *\) *) - (* ( Hax_lib_protocol__crypto__aead_encrypt, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::dh_scalar_multiply *\) *) - (* ( Hax_lib_protocol__crypto__dh_scalar_multiply, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::dh_scalar_multiply_base *\) *) - (* ( Hax_lib_protocol__crypto__dh_scalar_multiply_base, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__DHScalar__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__DHElement__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_1__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__AEADKey__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_4__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__AEADIV__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_5__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__AEADTag__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_6__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) ] - - let library_constructors : - (Concrete_ident_generated.name - * ((global_ident * AST.expr) list -> document)) - list = - [ (* ( Core__option__Option__Some, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__option__Option__None, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__ops__range__Range, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::(HashAlgorithm_HashAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HashAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::DHGroup_DHGroup_X25519_c *\) *) - (* ( Hax_lib_protocol__crypto__DHGroup__X25519, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::AEADAlgorithm_AEADAlgorithm_Chacha20Poly1305_c *\) *) - (* ( Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::HMACAlgorithm_HMACAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HMACAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) ] - - let library_constructor_patterns : - (Concrete_ident_generated.name * (field_pat list -> document)) list = - [ (* ( Core__option__Option__Some, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__option__Option__None, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__ops__range__Range, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::(HashAlgorithm_HashAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HashAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::DHGroup_DHGroup_X25519_c *\) *) - (* ( Hax_lib_protocol__crypto__DHGroup__X25519, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::AEADAlgorithm_AEADAlgorithm_Chacha20Poly1305_c *\) *) - (* ( Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::HMACAlgorithm_HMACAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HMACAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) ] - - let library_types : (Concrete_ident_generated.name * document) list = - [ (* (\* hax_lib_protocol::cal::(t_DHScalar *\) *) - (* (Hax_lib_protocol__crypto__DHScalar, string "PLACEHOLDER_library_type"); *) - (* (Core__option__Option, string "PLACEHOLDER_library_type"); *) - (* (Alloc__vec__Vec, string "PLACEHOLDER_library_type"); *) ] - - let assoc_known_name name (known_name, _) = - Global_ident.eq_name known_name name - - let translate_known_name name ~dict = - List.find ~f:(assoc_known_name name) dict - - class print aux = - object (print) - inherit GenericPrint.print as super - - method field_accessor field_name = - string "accessor" ^^ underscore ^^ print#concrete_ident field_name - - method match_arm scrutinee { arm_pat; body } = - let body = print#expr_at Arm_body body in - match arm_pat with - | { p = PWild; _ } -> body - | _ -> - let scrutinee = print#expr_at Expr_Match_scrutinee scrutinee in - let pat = print#pat_at Arm_pat arm_pat |> group in - string "let" ^^ space ^^ pat ^^ string " = " ^^ scrutinee - ^^ string " in " ^^ body - - method ty_bool = string "bool" - method ty_int _ = string "nat" - val mutable wildcard_index = 0 - - method wildcard = - wildcard_index <- wildcard_index + 1; - string "wildcard" ^^ OCaml.int wildcard_index - - method pat' : Generic_printer_base.par_state -> pat' fn = - fun ctx -> - let wrap_parens = - group - >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens - in - fun pat -> - match pat with - | PConstruct { name; args } -> ( - match - translate_known_name name ~dict:library_constructor_patterns - with - | Some (_, translation) -> translation args - | None -> super#pat' ctx pat) - | PWild -> - print#wildcard - (* NOTE: Wildcard translation without collisions? *) - | _ -> super#pat' ctx pat - - method tuple_elem_pat' : Generic_printer_base.par_state -> pat' fn = - fun ctx -> - let wrap_parens = - group - >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens - in - function - | PBinding { mut; mode; var; typ; subpat } -> - let p = print#local_ident var in - p ^^ colon ^^ space ^^ print#ty ctx typ - | p -> print#pat' ctx p - - method tuple_elem_pat : Generic_printer_base.par_state -> pat fn = - fun ctx { p; span; _ } -> - print#with_span ~span (fun _ -> print#tuple_elem_pat' ctx p) - - method tuple_elem_pat_at = print#par_state >> print#tuple_elem_pat - - method! pat_construct_tuple : pat list fn = - List.map ~f:(print#tuple_elem_pat_at Pat_ConstructTuple) - >> print#doc_construct_tuple - - method! expr_app f args _generic_args = - let args = - separate_map - (comma ^^ break 1) - (print#expr_at Expr_App_arg >> group) - args - in - let f = - match f with - | { e = GlobalVar name; _ } -> ( - match name with - | `Projector (`Concrete i) | `Concrete i -> - print#concrete_ident i |> group - | _ -> super#expr_at Expr_App_f f |> group) - in - f ^^ iblock parens args - - method! expr' : Generic_printer_base.par_state -> expr' fn = - fun ctx e -> - let wrap_parens = - group - >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens - in - match e with - | QuestionMark { e; _ } -> print#expr ctx e - (* Translate known functions *) - | App { f = { e = GlobalVar name; _ }; args } -> ( - match name with - | `Primitive p -> ( - match p with - | LogicalOp And -> - print#expr NeedsPar (List.hd_exn args) - ^^ space ^^ string "&&" ^^ space - ^^ print#expr NeedsPar (List.nth_exn args 1) - | LogicalOp Or -> - print#expr NeedsPar (List.hd_exn args) - ^^ space ^^ string "||" ^^ space - ^^ print#expr NeedsPar (List.nth_exn args 1) - | Cast -> print#expr NeedsPar (List.hd_exn args) - | _ -> empty) - | _ -> ( - match translate_known_name name ~dict:library_functions with - | Some (name, translation) -> translation args - | None -> ( - match name with - | `Projector (`Concrete name) -> - print#field_accessor name - ^^ iblock parens - (separate_map - (comma ^^ break 1) - (fun arg -> print#expr AlreadyPar arg) - args) - | _ -> super#expr' ctx e))) - | Construct { constructor; fields; _ } - when Global_ident.eq_name Core__result__Result__Ok constructor -> - super#expr' ctx (snd (Option.value_exn (List.hd fields))).e - | Construct { constructor; _ } - when Global_ident.eq_name Core__result__Result__Err constructor -> - string "construct_fail()" - (* Translate known constructors *) - | Construct { constructor; fields } -> ( - match - translate_known_name constructor ~dict:library_constructors - with - | Some (name, translation) -> translation fields - | None -> super#expr' ctx e) - (* Desugared `?` operator *) - | Match - { - scrutinee = - { e = App { f = { e = GlobalVar n; _ }; args = [ expr ] }; _ }; - arms = _; - } - (*[@ocamlformat "disable"]*) - when Global_ident.eq_name Core__ops__try_trait__Try__branch n -> - print#expr' ctx expr.e - | Match { scrutinee; arms } -> - separate_map - (hardline ^^ string "else ") - (fun { arm; span } -> print#match_arm scrutinee arm) - arms - | If { cond; then_; else_ } -> - let if_then = - (string "if" ^//^ nest 2 (print#expr_at Expr_If_cond cond)) - ^/^ string "then" - ^//^ (print#expr_at Expr_If_then then_ |> parens |> nest 1) - in - (match else_ with - | None -> if_then - | Some else_ -> - if_then ^^ break 1 ^^ string "else" ^^ space - ^^ (print#expr_at Expr_If_else else_ |> iblock parens)) - |> wrap_parens - | Let { monadic; lhs; rhs; body } -> - (Option.map - ~f:(fun monad -> print#expr_monadic_let ~monad) - monadic - |> Option.value ~default:print#expr_let) - ~lhs ~rhs body - |> wrap_parens - | _ -> super#expr' ctx e - - method concrete_ident = print#concrete_ident' ~under_current_ns:false - - method! item' item = - let fun_and_reduc base_name constructor = - let field_prefix = - if constructor.is_record then empty - else print#concrete_ident base_name - in - let fun_args = constructor.arguments in - let fun_args_full = - separate_map - (comma ^^ break 1) - (fun (x, y, _z) -> - 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 -> print#concrete_ident x) - fun_args - in - let fun_args_types = +module type OPTS = sig + val options : Hax_engine.Types.pro_verif_options +end + +module type MAKE = sig + module Preamble : sig + val print : item list -> string + end + + module DataTypes : sig + val print : item list -> string + end + + module Letfuns : sig + val print : item list -> string + end + + module Processes : sig + val print : item list -> string + end + + module Toplevel : sig + val print : item list -> string + end +end + +module Make (Options : OPTS) : MAKE = struct + module Print = struct + module GenericPrint = + Generic_printer.Make (InputLanguage) (U.Concrete_ident_view) + + open Generic_printer_base.Make (InputLanguage) + open PPrint + + let iblock f = group >> jump 2 0 >> terminate (break 0) >> f >> group + + (* TODO: Give definitions for core / known library functions, cf issues #447, #448 *) + let library_functions : + (Concrete_ident_generated.name * (AST.expr list -> document)) list = + [ + (* (\* Core dependencies *\) *) + (Rust_primitives__hax__never_to_any, fun _ -> string "construct_fail()") + (* (Alloc__vec__from_elem, fun args -> string "PLACEHOLDER_library_function"); *) + (* ( Alloc__slice__Impl__to_vec, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (Core__slice__Impl__len, fun args -> string "PLACEHOLDER_library_function"); *) + (* ( Core__ops__deref__Deref__deref, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* ( Core__ops__index__Index__index, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* ( Rust_primitives__unsize, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* ( Core__num__Impl_9__to_le_bytes, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* ( Alloc__slice__Impl__into_vec, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* ( Alloc__vec__Impl_1__truncate, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* ( Alloc__vec__Impl_2__extend_from_slice, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* ( Alloc__slice__Impl__concat, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* ( Core__option__Impl__is_some, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* core::clone::Clone_f_clone *\) *) + (* ( Core__clone__Clone__clone, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* core::cmp::PartialEq::eq *\) *) + (* ( Core__cmp__PartialEq__eq, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* core::cmp::PartialEq_f_ne *\) *) + (* ( Core__cmp__PartialEq__ne, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* core::cmp::PartialOrd::lt *\) *) + (* ( Core__cmp__PartialOrd__lt, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* core::ops::arith::Add::add *\) *) + (* ( Core__ops__arith__Add__add, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* core::ops::arith::Sub::sub *\) *) + (* ( Core__ops__arith__Sub__sub, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* core::option::Option_Option_None_c *\) *) + (* ( Core__option__Option__None, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* core::option::Option_Option_Some_c *\) *) + (* ( Core__option__Option__Some, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* core::result::impl__map_err *\) *) + (* ( Core__result__Impl__map_err, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* Crypto dependencies *\) *) + (* (\* hax_lib_protocol::cal::hash *\) *) + (* ( Hax_lib_protocol__crypto__hash, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* hax_lib_protocol::cal::hmac *\) *) + (* ( Hax_lib_protocol__crypto__hmac, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* hax_lib_protocol::cal::aead_decrypt *\) *) + (* ( Hax_lib_protocol__crypto__aead_decrypt, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* hax_lib_protocol::cal::aead_encrypt *\) *) + (* ( Hax_lib_protocol__crypto__aead_encrypt, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* hax_lib_protocol::cal::dh_scalar_multiply *\) *) + (* ( Hax_lib_protocol__crypto__dh_scalar_multiply, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* hax_lib_protocol::cal::dh_scalar_multiply_base *\) *) + (* ( Hax_lib_protocol__crypto__dh_scalar_multiply_base, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* hax_lib_protocol::cal::impl__DHScalar__from_bytes *\) *) + (* ( Hax_lib_protocol__crypto__Impl__from_bytes, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* hax_lib_protocol::cal::impl__DHElement__from_bytes *\) *) + (* ( Hax_lib_protocol__crypto__Impl_1__from_bytes, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* hax_lib_protocol::cal::impl__AEADKey__from_bytes *\) *) + (* ( Hax_lib_protocol__crypto__Impl_4__from_bytes, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* hax_lib_protocol::cal::impl__AEADIV__from_bytes *\) *) + (* ( Hax_lib_protocol__crypto__Impl_5__from_bytes, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *) + (* (\* hax_lib_protocol::cal::impl__AEADTag__from_bytes *\) *) + (* ( Hax_lib_protocol__crypto__Impl_6__from_bytes, *) + (* fun args -> string "PLACEHOLDER_library_function" ); *); + ] + + let library_constructors : + (Concrete_ident_generated.name + * ((global_ident * AST.expr) list -> document)) + list = + [ (* ( Core__option__Option__Some, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* ( Core__option__Option__None, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* ( Core__ops__range__Range, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* (\* hax_lib_protocol::cal::(HashAlgorithm_HashAlgorithm_Sha256_c *\) *) + (* ( Hax_lib_protocol__crypto__HashAlgorithm__Sha256, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* (\* hax_lib_protocol::cal::DHGroup_DHGroup_X25519_c *\) *) + (* ( Hax_lib_protocol__crypto__DHGroup__X25519, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* (\* hax_lib_protocol::cal::AEADAlgorithm_AEADAlgorithm_Chacha20Poly1305_c *\) *) + (* ( Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* (\* hax_lib_protocol::cal::HMACAlgorithm_HMACAlgorithm_Sha256_c *\) *) + (* ( Hax_lib_protocol__crypto__HMACAlgorithm__Sha256, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) ] + + let library_constructor_patterns : + (Concrete_ident_generated.name * (field_pat list -> document)) list = + [ (* ( Core__option__Option__Some, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* ( Core__option__Option__None, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* ( Core__ops__range__Range, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* (\* hax_lib_protocol::cal::(HashAlgorithm_HashAlgorithm_Sha256_c *\) *) + (* ( Hax_lib_protocol__crypto__HashAlgorithm__Sha256, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* (\* hax_lib_protocol::cal::DHGroup_DHGroup_X25519_c *\) *) + (* ( Hax_lib_protocol__crypto__DHGroup__X25519, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* (\* hax_lib_protocol::cal::AEADAlgorithm_AEADAlgorithm_Chacha20Poly1305_c *\) *) + (* ( Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) + (* (\* hax_lib_protocol::cal::HMACAlgorithm_HMACAlgorithm_Sha256_c *\) *) + (* ( Hax_lib_protocol__crypto__HMACAlgorithm__Sha256, *) + (* fun args -> string "PLACEHOLDER_library_constructor" ); *) ] + + let library_types : (Concrete_ident_generated.name * document) list = + [ (* (\* hax_lib_protocol::cal::(t_DHScalar *\) *) + (* (Hax_lib_protocol__crypto__DHScalar, string "PLACEHOLDER_library_type"); *) + (* (Core__option__Option, string "PLACEHOLDER_library_type"); *) + (* (Alloc__vec__Vec, string "PLACEHOLDER_library_type"); *) ] + + let assoc_known_name name (known_name, _) = + Global_ident.eq_name known_name name + + let translate_known_name name ~dict = + List.find ~f:(assoc_known_name name) dict + + class print aux = + object (print) + inherit GenericPrint.print as super + + method field_accessor field_name = + string "accessor" ^^ underscore ^^ print#concrete_ident field_name + + method match_arm scrutinee { arm_pat; body } = + let body = print#expr_at Arm_body body in + match arm_pat with + | { p = PWild; _ } -> body + | _ -> + let scrutinee = print#expr_at Expr_Match_scrutinee scrutinee in + let pat = print#pat_at Arm_pat arm_pat |> group in + string "let" ^^ space ^^ pat ^^ string " = " ^^ scrutinee + ^^ string " in " ^^ body + + method ty_bool = string "bool" + method ty_int _ = string "nat" + val mutable wildcard_index = 0 + + method wildcard = + wildcard_index <- wildcard_index + 1; + string "wildcard" ^^ OCaml.int wildcard_index + + method pat' : Generic_printer_base.par_state -> pat' fn = + fun ctx -> + let wrap_parens = + group + >> + match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens + in + fun pat -> + match pat with + | PConstruct { name; args } -> ( + match + translate_known_name name ~dict:library_constructor_patterns + with + | Some (_, translation) -> translation args + | None -> super#pat' ctx pat) + | PWild -> + print#wildcard + (* NOTE: Wildcard translation without collisions? *) + | _ -> super#pat' ctx pat + + method tuple_elem_pat' : Generic_printer_base.par_state -> pat' fn = + fun ctx -> + let wrap_parens = + group + >> + match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens + in + function + | PBinding { mut; mode; var; typ; subpat } -> + let p = print#local_ident var in + p ^^ colon ^^ space ^^ print#ty ctx typ + | p -> print#pat' ctx p + + method tuple_elem_pat : Generic_printer_base.par_state -> pat fn = + fun ctx { p; span; _ } -> + print#with_span ~span (fun _ -> print#tuple_elem_pat' ctx p) + + method tuple_elem_pat_at = print#par_state >> print#tuple_elem_pat + + method! pat_construct_tuple : pat list fn = + List.map ~f:(print#tuple_elem_pat_at Pat_ConstructTuple) + >> print#doc_construct_tuple + + method! expr_app f args _generic_args = + let args = separate_map (comma ^^ break 1) - (snd3 >> print#ty_at Param_typ) - fun_args - in - let constructor_name = print#concrete_ident constructor.name in - - let fun_line = - string "fun" ^^ space ^^ constructor_name - ^^ iblock parens fun_args_types - ^^ string ": " - ^^ print#concrete_ident base_name - ^^ space ^^ string "[data]" ^^ dot + (print#expr_at Expr_App_arg >> group) + args in - let reduc_line = - string "reduc forall " ^^ iblock Fn.id fun_args_full ^^ semi + let f = + match f with + | { e = GlobalVar name; _ } -> ( + match name with + | `Projector (`Concrete i) | `Concrete i -> + print#concrete_ident i |> group + | _ -> super#expr_at Expr_App_f f |> group) in - let build_accessor (ident, ty, attr) = - print#field_accessor ident - ^^ iblock parens (constructor_name ^^ iblock parens fun_args_names) - ^^ blank 1 ^^ equals ^^ blank 1 ^^ print#concrete_ident ident - in - let reduc_lines = - separate_map (dot ^^ hardline) - (fun arg -> reduc_line ^^ nest 4 (hardline ^^ build_accessor arg)) - fun_args + f ^^ iblock parens args + + method! expr' : Generic_printer_base.par_state -> expr' fn = + fun ctx e -> + let wrap_parens = + group + >> + match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens + in + match e with + | QuestionMark { e; _ } -> print#expr ctx e + (* Translate known functions *) + | App { f = { e = GlobalVar name; _ }; args } -> ( + match name with + | `Primitive p -> ( + match p with + | LogicalOp And -> + print#expr NeedsPar (List.hd_exn args) + ^^ space ^^ string "&&" ^^ space + ^^ print#expr NeedsPar (List.nth_exn args 1) + | LogicalOp Or -> + print#expr NeedsPar (List.hd_exn args) + ^^ space ^^ string "||" ^^ space + ^^ print#expr NeedsPar (List.nth_exn args 1) + | Cast -> print#expr NeedsPar (List.hd_exn args) + | _ -> empty) + | _ -> ( + match translate_known_name name ~dict:library_functions with + | Some (name, translation) -> translation args + | None -> ( + match name with + | `Projector (`Concrete name) -> + print#field_accessor name + ^^ iblock parens + (separate_map + (comma ^^ break 1) + (fun arg -> print#expr AlreadyPar arg) + args) + | _ -> super#expr' ctx e))) + | Construct { constructor; fields; _ } + when Global_ident.eq_name Core__result__Result__Ok constructor -> + super#expr' ctx (snd (Option.value_exn (List.hd fields))).e + | Construct { constructor; _ } + when Global_ident.eq_name Core__result__Result__Err constructor -> + string "construct_fail()" + (* Translate known constructors *) + | Construct { constructor; fields } -> ( + match + translate_known_name constructor ~dict:library_constructors + with + | Some (name, translation) -> translation fields + | None -> super#expr' ctx e) + (* Desugared `?` operator *) + | Match + { + scrutinee = + { + e = App { f = { e = GlobalVar n; _ }; args = [ expr ] }; + _; + }; + arms = _; + } + (*[@ocamlformat "disable"]*) + when Global_ident.eq_name Core__ops__try_trait__Try__branch n -> + print#expr' ctx expr.e + | Match { scrutinee; arms } -> + separate_map + (hardline ^^ string "else ") + (fun { arm; span } -> print#match_arm scrutinee arm) + arms + | If { cond; then_; else_ } -> + let if_then = + (string "if" ^//^ nest 2 (print#expr_at Expr_If_cond cond)) + ^/^ string "then" + ^//^ (print#expr_at Expr_If_then then_ |> parens |> nest 1) + in + (match else_ with + | None -> if_then + | Some else_ -> + if_then ^^ break 1 ^^ string "else" ^^ space + ^^ (print#expr_at Expr_If_else else_ |> iblock parens)) + |> wrap_parens + | Let { monadic; lhs; rhs; body } -> + (Option.map + ~f:(fun monad -> print#expr_monadic_let ~monad) + monadic + |> Option.value ~default:print#expr_let) + ~lhs ~rhs body + |> wrap_parens + | _ -> super#expr' ctx e + + method concrete_ident = print#concrete_ident' ~under_current_ns:false + + method! item_unwrapped item = + let assume_item = + List.rev Options.options.assume_items + |> List.find ~f:(fun (clause : Types.inclusion_clause) -> + let namespace = clause.namespace in + Concrete_ident.matches_namespace namespace item.ident) + |> Option.map ~f:(fun (clause : Types.inclusion_clause) -> + match clause.kind with Types.Excluded -> false | _ -> true) + |> Option.value ~default:false in - fun_line ^^ hardline ^^ reduc_lines - ^^ if reduc_lines == empty then empty else dot - 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) + let fun_and_reduc base_name constructor = + let field_prefix = + if constructor.is_record then empty + else print#concrete_ident base_name in - string "letfun" ^^ space - ^^ align - (print#concrete_ident name ^^ params_string ^^ space ^^ equals - ^^ 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 } -> - let type_line = - string "type " ^^ print#concrete_ident name ^^ dot + let fun_args = constructor.arguments in + let fun_args_full = + separate_map + (comma ^^ break 1) + (fun (x, y, _z) -> + print#concrete_ident x ^^ string ": " + ^^ print#ty_at Param_typ y) + fun_args in - let type_converter_line = - string "fun " ^^ print#concrete_ident name - ^^ string "_to_bitstring" - ^^ iblock parens (print#concrete_ident name) - ^^ string ": bitstring [typeConverter]." + let fun_args_names = + separate_map + (comma ^^ break 1) + (fst3 >> fun x -> print#concrete_ident x) + fun_args in - if is_struct then - let struct_constructor = List.hd variants in - match struct_constructor with - | None -> empty - | Some constructor -> - type_line ^^ hardline ^^ type_converter_line ^^ hardline - ^^ fun_and_reduc name constructor - else - type_line ^^ hardline ^^ type_converter_line ^^ hardline - ^^ separate_map (hardline ^^ hardline) - (fun variant -> fun_and_reduc name variant) - variants - | _ -> 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 concrete_ident' ~(under_current_ns : bool) : concrete_ident fn = - fun id -> - if under_current_ns then print#name_of_concrete_ident id - else - let crate, path = print#namespace_of_concrete_ident id in - let full_path = crate :: path in - separate_map (underscore ^^ underscore) utf8string full_path - ^^ underscore ^^ underscore - ^^ print#name_of_concrete_ident id - - 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 - 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 (comma ^^ break 1) snd args) - - method generic_values : generic_value list fn = - function - | [] -> empty - | values -> - string "_of" ^^ underscore - ^^ separate_map underscore print#generic_value values - - method ty_app f args = print#concrete_ident f ^^ print#generic_values args - - method generic_arg_n_tuple n args = - string "tuple" ^^ OCaml.int n ^^ underscore - ^^ separate_map underscore print#generic_value args - - method ty_at : Generic_printer_base.ast_position -> ty fn = - fun position -> - let otherwise = print#par_state position |> print#ty in - match position with - | GenericValue_GType | Param_typ -> ( - fun ty -> - match ty with - | TApp { ident = `TupleType n; args } -> - print#generic_arg_n_tuple n args - | _ -> otherwise ty) - | _ -> otherwise - - method local_ident e = - match String.chop_prefix ~prefix:"impl " e.name with - | Some name -> - let name = - "impl_" - ^ String.tr ~target:'+' ~replacement:'_' - (String.tr ~target:' ' ~replacement:'_' name) + let fun_args_types = + separate_map + (comma ^^ break 1) + (snd3 >> print#ty_at Param_typ) + fun_args in - string name - | _ -> super#local_ident e - - 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 - | TInt kind -> print#ty_int kind - (* Translate known types, no args at the moment *) - | TApp { ident; args } -> super#ty ctx ty - (*( - match translate_known_name ident ~dict:library_types with - | Some (_, translation) -> translation - | None -> super#ty ctx ty)*) - | _ -> string "bitstring" - end - - type proverif_aux_info = CrateFns of AST.item list | NoAuxInfo - - include Api (struct - type aux_info = proverif_aux_info - - let new_print aux = (new print aux :> print_object) - end) -end + let constructor_name = print#concrete_ident constructor.name in + + let fun_line = + string "fun" ^^ space ^^ constructor_name + ^^ iblock parens fun_args_types + ^^ string ": " + ^^ print#concrete_ident base_name + ^^ space ^^ string "[data]" ^^ dot + in + let reduc_line = + string "reduc forall " ^^ iblock Fn.id fun_args_full ^^ semi + in + let build_accessor (ident, ty, attr) = + print#field_accessor ident + ^^ iblock parens (constructor_name ^^ iblock parens fun_args_names) + ^^ blank 1 ^^ equals ^^ blank 1 ^^ print#concrete_ident ident + in + let reduc_lines = + separate_map (dot ^^ hardline) + (fun arg -> + reduc_line ^^ nest 4 (hardline ^^ build_accessor arg)) + fun_args + in + fun_line ^^ hardline ^^ reduc_lines + ^^ if reduc_lines == empty then empty else dot + in + match item.v 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 + ^^ align + (print#concrete_ident name ^^ params_string ^^ space + ^^ equals ^^ 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 } -> + let type_line = + string "type " ^^ print#concrete_ident name ^^ dot + in + let type_converter_line = + string "fun " ^^ print#concrete_ident name + ^^ string "_to_bitstring" + ^^ iblock parens (print#concrete_ident name) + ^^ string ": bitstring [typeConverter]." + in + if is_struct then + let struct_constructor = List.hd variants in + match struct_constructor with + | None -> empty + | Some constructor -> + type_line ^^ hardline ^^ type_converter_line ^^ hardline + ^^ fun_and_reduc name constructor + else + type_line ^^ hardline ^^ type_converter_line ^^ hardline + ^^ separate_map (hardline ^^ hardline) + (fun variant -> fun_and_reduc name variant) + variants + | _ -> 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 concrete_ident' ~(under_current_ns : bool) : concrete_ident fn = + fun id -> + if under_current_ns then print#name_of_concrete_ident id + else + let crate, path = print#namespace_of_concrete_ident id in + let full_path = crate :: path in + separate_map (underscore ^^ underscore) utf8string full_path + ^^ underscore ^^ underscore + ^^ print#name_of_concrete_ident id + + 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 + 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 (comma ^^ break 1) snd args) -let filter_crate_functions (items : AST.item list) = - List.filter ~f:(fun item -> [%matches? Fn _] item.v) items + method generic_values : generic_value list fn = + function + | [] -> empty + | values -> + string "_of" ^^ underscore + ^^ separate_map underscore print#generic_value values + + method ty_app f args = + print#concrete_ident f ^^ print#generic_values args + + method generic_arg_n_tuple n args = + string "tuple" ^^ OCaml.int n ^^ underscore + ^^ separate_map underscore print#generic_value args + + method ty_at : Generic_printer_base.ast_position -> ty fn = + fun position -> + let otherwise = print#par_state position |> print#ty in + match position with + | GenericValue_GType | Param_typ -> ( + fun ty -> + match ty with + | TApp { ident = `TupleType n; args } -> + print#generic_arg_n_tuple n args + | _ -> otherwise ty) + | _ -> otherwise + + method local_ident e = + match String.chop_prefix ~prefix:"impl " e.name with + | Some name -> + let name = + "impl_" + ^ String.tr ~target:'+' ~replacement:'_' + (String.tr ~target:' ' ~replacement:'_' name) + in + string name + | _ -> super#local_ident e + + 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 + | TInt kind -> print#ty_int kind + (* Translate known types, no args at the moment *) + | TApp { ident; args } -> super#ty ctx ty + (*( + match translate_known_name ident ~dict:library_types with + | Some (_, translation) -> translation + | None -> super#ty ctx ty)*) + | _ -> string "bitstring" + end + + type proverif_aux_info = CrateFns of AST.item list | NoAuxInfo + + include Api (struct + type aux_info = proverif_aux_info + + let new_print aux = (new print aux :> print_object) + end) + end + + let filter_crate_functions (items : AST.item list) = + List.filter ~f:(fun item -> [%matches? Fn _] item.v) items + + 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 is_process item = + is_process_read item.attrs + || is_process_write item.attrs + || is_process_init item.attrs + + module type Subprinter = sig + val print : AST.item list -> string + end + + module MkSubprinter (Section : sig + val banner : string + val preamble : AST.item list -> string + val contents : AST.item list -> string + end) = + struct + let hline = "(*****************************************)\n" + let banner = hline ^ "(* " ^ Section.banner ^ " *)\n" ^ hline ^ "\n" + + let print items = + banner ^ Section.preamble items ^ Section.contents items ^ "\n\n" + end + + module Preamble = MkSubprinter (struct + let banner = "Preamble" + + let preamble items = + "channel c.\n\ + fun int2bitstring(nat): bitstring.\n\ + type err.\n\ + fun construct_fail() : err\n\ + reduc construct_fail() = fail.\n" + + let contents items = "" + end) -let is_process_read : attrs -> bool = - Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.ProcessRead]) + module DataTypes = MkSubprinter (struct + let banner = "Types and Constructors" + let preamble items = "" -let is_process_write : attrs -> bool = - Attr_payloads.payloads - >> List.exists ~f:(fst >> [%matches? Types.ProcessWrite]) + let filter_data_types items = + List.filter ~f:(fun item -> [%matches? Type _] item.v) items -let is_process_init : attrs -> bool = - Attr_payloads.payloads >> List.exists ~f:(fst >> [%matches? Types.ProcessInit]) + let contents items = + let contents, _ = Print.items NoAuxInfo (filter_data_types items) in + contents + end) -let is_process item = - is_process_read item.attrs - || is_process_write item.attrs - || is_process_init item.attrs + module Letfuns = MkSubprinter (struct + let banner = "Functions" + let preamble items = "" + + let contents items = + let process_letfuns, pure_letfuns = + List.partition_tf ~f:is_process (filter_crate_functions items) + in + let pure_letfuns_print, _ = + Print.items (CrateFns (filter_crate_functions items)) pure_letfuns + in + let process_letfuns_print, _ = + Print.items (CrateFns (filter_crate_functions items)) process_letfuns + in + pure_letfuns_print ^ process_letfuns_print + end) -module type Subprinter = sig - val print : AST.item list -> string -end + module Processes = MkSubprinter (struct + let banner = "Processes" + let preamble items = "" + let process_filter item = [%matches? Fn _] item.v && is_process item -module MkSubprinter (Section : sig - val banner : string - val preamble : AST.item list -> string - val contents : AST.item list -> string -end) = -struct - let hline = "(*****************************************)\n" - let banner = hline ^ "(* " ^ Section.banner ^ " *)\n" ^ hline ^ "\n" + let contents items = + let contents, _ = + Print.items NoAuxInfo (List.filter ~f:process_filter items) + in + contents + end) - let print items = - banner ^ Section.preamble items ^ Section.contents items ^ "\n\n" + module Toplevel = MkSubprinter (struct + let banner = "Top-level process" + let preamble items = "process\n 0\n" + let contents items = "" + end) end -module Preamble = MkSubprinter (struct - let banner = "Preamble" - - let preamble items = - "channel c.\n\ - fun int2bitstring(nat): bitstring.\n\ - type err.\n\ - fun construct_fail() : err\n\ - reduc construct_fail() = fail.\n" - - let contents items = "" -end) - -module DataTypes = MkSubprinter (struct - let banner = "Types and Constructors" - let preamble items = "" - - let filter_data_types items = - List.filter ~f:(fun item -> [%matches? Type _] item.v) items - - let contents items = - let contents, _ = Print.items NoAuxInfo (filter_data_types items) in - contents -end) - -module Letfuns = MkSubprinter (struct - let banner = "Functions" - let preamble items = "" - - let contents items = - let process_letfuns, pure_letfuns = - List.partition_tf ~f:is_process (filter_crate_functions items) - in - let pure_letfuns_print, _ = - Print.items (CrateFns (filter_crate_functions items)) pure_letfuns - in - let process_letfuns_print, _ = - Print.items (CrateFns (filter_crate_functions items)) process_letfuns - in - pure_letfuns_print ^ process_letfuns_print -end) - -module Processes = MkSubprinter (struct - let banner = "Processes" - let preamble items = "" - let process_filter item = [%matches? Fn _] item.v && is_process item - - let contents items = - let contents, _ = - Print.items NoAuxInfo (List.filter ~f:process_filter items) - in - contents -end) - -module Toplevel = MkSubprinter (struct - let banner = "Top-level process" - let preamble items = "process\n 0\n" - let contents items = "" -end) - let translate m (bo : BackendOptions.t) (items : AST.item list) : Types.file list = + let (module M : MAKE) = + (module Make (struct + let options = bo + end)) + in let lib_contents = - Preamble.print items ^ DataTypes.print items ^ Letfuns.print items - ^ Processes.print items + M.Preamble.print items ^ M.DataTypes.print items ^ M.Letfuns.print items + ^ M.Processes.print items in - let analysis_contents = Toplevel.print items in + let analysis_contents = M.Toplevel.print items in let lib_file = Types.{ path = "lib.pvl"; contents = lib_contents } in let analysis_file = Types.{ path = "analysis.pv"; contents = analysis_contents } diff --git a/engine/backends/proverif/proverif_backend.mli b/engine/backends/proverif/proverif_backend.mli index 67448d149..b2475d3db 100644 --- a/engine/backends/proverif/proverif_backend.mli +++ b/engine/backends/proverif/proverif_backend.mli @@ -1,2 +1,2 @@ open Hax_engine.Backend -include T with module BackendOptions = UnitBackendOptions +include T with type BackendOptions.t = Hax_engine.Types.pro_verif_options diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml index d45b035cc..4b1b83a7c 100644 --- a/engine/bin/lib.ml +++ b/engine/bin/lib.ml @@ -86,10 +86,10 @@ let run (options : Types.engine_options) : Types.output = let diagnostics, files = Diagnostics.try_ (fun () -> match options.backend.backend with + | ProVerif opts -> run (module Proverif_backend) opts | Fstar opts -> run (module Fstar_backend) opts | Coq -> run (module Coq_backend) () - | Easycrypt -> run (module Easycrypt_backend) () - | ProVerif -> run (module Proverif_backend) ()) + | Easycrypt -> run (module Easycrypt_backend) ()) in { diagnostics = List.map ~f:Diagnostics.to_thir_diagnostic diagnostics; diff --git a/engine/lib/generic_printer/generic_printer_base.ml b/engine/lib/generic_printer/generic_printer_base.ml index 38c96a00d..27f497fc9 100644 --- a/engine/lib/generic_printer/generic_printer_base.ml +++ b/engine/lib/generic_printer/generic_printer_base.ml @@ -111,10 +111,6 @@ module Make (F : Features.T) = struct method compact : output -> unit = fun o -> compact o doc end - (** Print a concrete identifier. - - Differentiates between encounters of the identifier in its own namespace - or a foreign namespace.*) method concrete_ident : concrete_ident fn = fun id -> let current_ns = print#get_current_namespace () in @@ -123,6 +119,10 @@ module Make (F : Features.T) = struct ~under_current_ns: ([%equal: (string * string list) option] current_ns (Some id_ns)) id + (** Print a concrete identifier. + + Differentiates between encounters of the identifier in its own namespace + or a foreign namespace.*) method assertion_failure : 'any. string -> 'any = fun details -> @@ -283,9 +283,9 @@ module Make (F : Features.T) = struct method printer_name : string method get_span_data : unit -> Annotation.t list - (** The namespace a concrete identifier was defined in. *) method namespace_of_concrete_ident : concrete_ident -> string * string list + (** The namespace a concrete identifier was defined in. *) method par_state : ast_position -> par_state method concrete_ident' : under_current_ns:bool -> concrete_ident fn From 5f0354cd8d77c383b4a906d16866dc8b4e4f9451 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 15:23:44 +0100 Subject: [PATCH 16/46] Ignore clone and unsize --- engine/backends/proverif/proverif_backend.ml | 31 ++++++++++++-------- 1 file changed, 19 insertions(+), 12 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index cec87f16a..ea8a6ba44 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -398,18 +398,25 @@ module Make (Options : OPTS) : MAKE = struct | Cast -> print#expr NeedsPar (List.hd_exn args) | _ -> empty) | _ -> ( - match translate_known_name name ~dict:library_functions with - | Some (name, translation) -> translation args - | None -> ( - match name with - | `Projector (`Concrete name) -> - print#field_accessor name - ^^ iblock parens - (separate_map - (comma ^^ break 1) - (fun arg -> print#expr AlreadyPar arg) - args) - | _ -> super#expr' ctx e))) + if + Global_ident.eq_name Core__clone__Clone__clone name + || Global_ident.eq_name Rust_primitives__unsize name + then print#expr ctx (List.hd_exn args) + else + match + translate_known_name name ~dict:library_functions + with + | Some (name, translation) -> translation args + | None -> ( + match name with + | `Projector (`Concrete name) -> + print#field_accessor name + ^^ iblock parens + (separate_map + (comma ^^ break 1) + (fun arg -> print#expr AlreadyPar arg) + args) + | _ -> super#expr' ctx e))) | Construct { constructor; fields; _ } when Global_ident.eq_name Core__result__Result__Ok constructor -> super#expr' ctx (snd (Option.value_exn (List.hd fields))).e From f5a8c85b5d9af326979387a3fb99a0a77a34284f Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 15:24:45 +0100 Subject: [PATCH 17/46] Translate consts --- engine/backends/proverif/proverif_backend.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index ea8a6ba44..b2a88b135 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -535,6 +535,10 @@ module Make (Options : OPTS) : MAKE = struct in match item.v with (* `fn`s are transformed into `letfun` process macros. *) + | Fn { name; body; params = []; _ } -> + string "const" ^^ space ^^ print#concrete_ident name ^^ colon + ^^ print#ty_at Item_Fn_body body.typ + ^^ dot | Fn { name; generics; body; params } -> let params_string = iblock parens From 96ede8fb92361a8e4d727f87e6c210ec9f4f3a0b Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 15:25:07 +0100 Subject: [PATCH 18/46] Print only signature for assumed items --- engine/backends/proverif/proverif_backend.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index b2a88b135..239539c40 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -540,6 +540,13 @@ module Make (Options : OPTS) : MAKE = struct ^^ print#ty_at Item_Fn_body body.typ ^^ dot | Fn { name; generics; body; params } -> + let body = + if assume_item then + string "unit (* fill_in_body of type: " + ^^ print#ty_at Item_Fn_body body.typ + ^^ string "*)" + else print#expr_at Item_Fn_body body + in let params_string = iblock parens (separate_map (comma ^^ break 1) print#param params) @@ -547,9 +554,7 @@ module Make (Options : OPTS) : MAKE = struct string "letfun" ^^ space ^^ align (print#concrete_ident name ^^ params_string ^^ space - ^^ equals ^^ hardline - ^^ print#expr_at Item_Fn_body body - ^^ dot) + ^^ equals ^^ hardline ^^ body ^^ dot) (* `struct` definitions are transformed into simple constructors and `reduc`s for accessing fields. *) | Type { name; generics; variants; is_struct } -> let type_line = From 83bfb0cac50c0e40f911341b1f4671a8a98be27c Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 15 Feb 2024 13:59:37 +0100 Subject: [PATCH 19/46] fix(engine/?): insert `map_err` only when needed --- .../phase_reconstruct_question_marks.ml | 23 +++++++++++-------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/engine/lib/phases/phase_reconstruct_question_marks.ml b/engine/lib/phases/phase_reconstruct_question_marks.ml index c2bf99dff..43e1f973c 100644 --- a/engine/lib/phases/phase_reconstruct_question_marks.ml +++ b/engine/lib/phases/phase_reconstruct_question_marks.ml @@ -85,16 +85,19 @@ module%inlined_contents Make (FA : Features.T) = struct let map_err (e : expr) (error_dest : ty) impl : expr option = let* success, error_src = expect_result_type e.typ in let* impl = expect_residual_impl_result impl in - let from_typ = TArrow ([ error_src ], error_dest) in - let from = - UA.call ~kind:(AssociatedItem Value) ~impl Core__convert__From__from - [] e.span from_typ - in - let call = - UA.call Core__result__Impl__map_err [ e; from ] e.span - (make_result_type success error_dest) - in - Some call + if [%equal: ty] error_src error_dest then + Some e + else + let from_typ = TArrow ([ error_src ], error_dest) in + let from = + UA.call ~kind:(AssociatedItem Value) ~impl Core__convert__From__from + [] e.span from_typ + in + let call = + UA.call Core__result__Impl__map_err [ e; from ] e.span + (make_result_type success error_dest) + in + Some call (** [extract e] returns [Some (x, ty)] if [e] was a `y?` desugared by rustc. `y` is `x` plus possibly a coercion. [ty] is From 7a1678d61fff78f4d949f065bb7b5f74d04ef3b8 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 16:40:18 +0100 Subject: [PATCH 20/46] Construct fail as bitstring --- engine/backends/proverif/proverif_backend.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 239539c40..0d5f52e08 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -721,9 +721,11 @@ module Make (Options : OPTS) : MAKE = struct let preamble items = "channel c.\n\ fun int2bitstring(nat): bitstring.\n\ - type err.\n\ - fun construct_fail() : err\n\ - reduc construct_fail() = fail.\n" + fun construct_fail() : bitstring\n\ + reduc construct_fail() = fail.\n\n\ + \ const empty: bitstring.\n\n\ + \ type unimplemented.\n\n\ + \ const Unimplemented: unimplemented.\n" let contents items = "" end) From 299a9356dd349040c44c9ca92003f7038fbed714 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 16:40:33 +0100 Subject: [PATCH 21/46] Special treatment for Vec, Core, Option --- engine/backends/proverif/proverif_backend.ml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 0d5f52e08..55a9e6a7e 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -661,6 +661,15 @@ module Make (Options : OPTS) : MAKE = struct | TParam i -> print#local_ident i | TInt kind -> print#ty_int kind (* Translate known types, no args at the moment *) + | TApp { ident; args } + when Global_ident.eq_name Alloc__vec__Vec ident -> + string "bitstring" + | TApp { ident; args } + when Global_ident.eq_name Core__option__Option ident -> + string "Option" + | TApp { ident; args } + when Global_ident.eq_name Core__result__Result ident -> + string "Result" | TApp { ident; args } -> super#ty ctx ty (*( match translate_known_name ident ~dict:library_types with From 4fdd5308062dede6e3ff7a1fe7874914dad94968 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 16:41:24 +0100 Subject: [PATCH 22/46] Translate int constants as bitstrings --- engine/backends/proverif/proverif_backend.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 55a9e6a7e..3c9ef93cc 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -535,6 +535,9 @@ module Make (Options : OPTS) : MAKE = struct in match item.v with (* `fn`s are transformed into `letfun` process macros. *) + | Fn { name; body = { typ = TInt _; _ }; params = []; _ } -> + string "const" ^^ space ^^ print#concrete_ident name ^^ colon + ^^ string "bitstring" ^^ dot | Fn { name; body; params = []; _ } -> string "const" ^^ space ^^ print#concrete_ident name ^^ colon ^^ print#ty_at Item_Fn_body body.typ From 48ce86e41722f3dfddbe52db06196696ed840a5f Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 17:16:01 +0100 Subject: [PATCH 23/46] Unwrap result (WIP) --- 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 3c9ef93cc..89508b199 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -381,7 +381,8 @@ module Make (Options : OPTS) : MAKE = struct match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens in match e with - | QuestionMark { e; _ } -> print#expr ctx e + | QuestionMark { e; _ } -> + string "unwrap_result" ^^ iblock parens (print#expr ctx e) (* Translate known functions *) | App { f = { e = GlobalVar name; _ }; args } -> ( match name with From d62161ce1caf75ce788daab48151f54f699a0ab3 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 17:16:24 +0100 Subject: [PATCH 24/46] Generate type defaults --- engine/backends/proverif/proverif_backend.ml | 39 ++++++++++---------- 1 file changed, 19 insertions(+), 20 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 89508b199..40956ec9d 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -546,7 +546,9 @@ module Make (Options : OPTS) : MAKE = struct | Fn { name; generics; body; params } -> let body = if assume_item then - string "unit (* fill_in_body of type: " + print#ty_at Item_Fn_body body.typ + ^^ string "_default()" + ^^ string "(* fill_in_body of type: " ^^ print#ty_at Item_Fn_body body.typ ^^ string "*)" else print#expr_at Item_Fn_body body @@ -570,15 +572,23 @@ module Make (Options : OPTS) : MAKE = struct ^^ iblock parens (print#concrete_ident name) ^^ string ": bitstring [typeConverter]." in + let default_line = + string "const " ^^ print#concrete_ident name + ^^ string "_default_c" ^^ colon ^^ print#concrete_ident name + ^^ dot ^^ hardline ^^ string "letfun " + ^^ print#concrete_ident name ^^ string "_default() = " + ^^ print#concrete_ident name ^^ string "_default_c" ^^ dot + in if is_struct then let struct_constructor = List.hd variants in match struct_constructor with | None -> empty | Some constructor -> - type_line ^^ hardline ^^ type_converter_line ^^ hardline + type_line ^^ hardline ^^ type_converter_line ^^ hardline ^^ default_line ^^ hardline ^^ fun_and_reduc name constructor else type_line ^^ hardline ^^ type_converter_line ^^ hardline + ^^ default_line ^^ hardline ^^ separate_map (hardline ^^ hardline) (fun variant -> fun_and_reduc name variant) variants @@ -631,21 +641,7 @@ module Make (Options : OPTS) : MAKE = struct method ty_app f args = print#concrete_ident f ^^ print#generic_values args - method generic_arg_n_tuple n args = - string "tuple" ^^ OCaml.int n ^^ underscore - ^^ separate_map underscore print#generic_value args - - method ty_at : Generic_printer_base.ast_position -> ty fn = - fun position -> - let otherwise = print#par_state position |> print#ty in - match position with - | GenericValue_GType | Param_typ -> ( - fun ty -> - match ty with - | TApp { ident = `TupleType n; args } -> - print#generic_arg_n_tuple n args - | _ -> otherwise ty) - | _ -> otherwise + method ty_tuple _ _ = string "bitstring" method local_ident e = match String.chop_prefix ~prefix:"impl " e.name with @@ -736,9 +732,12 @@ module Make (Options : OPTS) : MAKE = struct fun int2bitstring(nat): bitstring.\n\ fun construct_fail() : bitstring\n\ reduc construct_fail() = fail.\n\n\ - \ const empty: bitstring.\n\n\ - \ type unimplemented.\n\n\ - \ const Unimplemented: unimplemented.\n" + const empty: bitstring.\n\n\ + type unimplemented.\n\n\ + const Unimplemented: unimplemented.\n\n\ + \ letfun bitstring_default() = empty.\n\n\ + \ letfun nat_default() = 0.\n\n\ + \ letfun bool_default() = false.\n" let contents items = "" end) From 7c7fb6a019a5d6ff217bb2fe3a3cbd5d389ed363 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 20:11:23 +0100 Subject: [PATCH 25/46] Type conversions around results --- engine/backends/proverif/proverif_backend.ml | 43 ++++++++++++++++---- 1 file changed, 35 insertions(+), 8 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 40956ec9d..babac8def 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -381,8 +381,20 @@ module Make (Options : OPTS) : MAKE = struct match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens in match e with - | QuestionMark { e; _ } -> - string "unwrap_result" ^^ iblock parens (print#expr ctx e) + | QuestionMark { e; return_typ; _ } -> + let inner_type = + match return_typ with + | TApp { args; _ } -> + let g_type = List.hd_exn args in + print#generic_value g_type + in + inner_type ^^ string "_from_bitstring" + ^^ iblock parens + (string "unwrap_result" + (*^^ iblock parens + inner_type ^^ string "_to_bitstring"*) + ^^ iblock parens (print#expr ctx e)) + (* ) *) (* Translate known functions *) | App { f = { e = GlobalVar name; _ }; args } -> ( match name with @@ -420,10 +432,16 @@ module Make (Options : OPTS) : MAKE = struct | _ -> super#expr' ctx e))) | Construct { constructor; fields; _ } when Global_ident.eq_name Core__result__Result__Ok constructor -> - super#expr' ctx (snd (Option.value_exn (List.hd fields))).e + let inner_expr = snd (Option.value_exn (List.hd fields)) in + let inner_expr_type_doc = print#ty AlreadyPar inner_expr.typ in + let inner_expr_doc = super#expr ctx inner_expr in + string "Ok" + ^^ iblock parens + (inner_expr_type_doc ^^ string "_to_bitstring" + ^^ iblock parens inner_expr_doc) | Construct { constructor; _ } when Global_ident.eq_name Core__result__Result__Err constructor -> - string "construct_fail()" + string "Err()" (* Translate known constructors *) | Construct { constructor; fields } -> ( match @@ -566,12 +584,18 @@ module Make (Options : OPTS) : MAKE = struct let type_line = string "type " ^^ print#concrete_ident name ^^ dot in - let type_converter_line = + let to_bitstring_converter_line = string "fun " ^^ print#concrete_ident name ^^ string "_to_bitstring" ^^ iblock parens (print#concrete_ident name) ^^ string ": bitstring [typeConverter]." in + let from_bitstring_converter_line = + string "fun " ^^ print#concrete_ident name + ^^ string "_from_bitstring(bitstring)" + ^^ colon ^^ print#concrete_ident name + ^^ string " [typeConverter]" ^^ dot + in let default_line = string "const " ^^ print#concrete_ident name ^^ string "_default_c" ^^ colon ^^ print#concrete_ident name @@ -584,11 +608,14 @@ module Make (Options : OPTS) : MAKE = struct match struct_constructor with | None -> empty | Some constructor -> - type_line ^^ hardline ^^ type_converter_line ^^ hardline ^^ default_line ^^ hardline + type_line ^^ hardline ^^ to_bitstring_converter_line + ^^ hardline ^^ from_bitstring_converter_line ^^ hardline + ^^ default_line ^^ hardline ^^ fun_and_reduc name constructor else - type_line ^^ hardline ^^ type_converter_line ^^ hardline - ^^ default_line ^^ hardline + type_line ^^ hardline ^^ to_bitstring_converter_line ^^ hardline + ^^ from_bitstring_converter_line ^^ hardline ^^ default_line + ^^ hardline ^^ separate_map (hardline ^^ hardline) (fun variant -> fun_and_reduc name variant) variants From 9cfb04f0172c2323a439f5f4ff6b40b1881649d9 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 15 Feb 2024 20:29:29 +0100 Subject: [PATCH 26/46] Translate literal match patterns --- engine/backends/proverif/proverif_backend.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index babac8def..dc63a9d29 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -300,8 +300,13 @@ module Make (Options : OPTS) : MAKE = struct match arm_pat with | { p = PWild; _ } -> body | _ -> + let pat = + match arm_pat with + | { p = PConstant { lit } } -> + iblock parens (string "=" ^^ print#literal Pat lit) + | _ -> print#pat_at Arm_pat arm_pat |> group + in let scrutinee = print#expr_at Expr_Match_scrutinee scrutinee in - let pat = print#pat_at Arm_pat arm_pat |> group in string "let" ^^ space ^^ pat ^^ string " = " ^^ scrutinee ^^ string " in " ^^ body @@ -322,6 +327,7 @@ module Make (Options : OPTS) : MAKE = struct in fun pat -> match pat with + | PConstant { lit } -> string "=" ^^ print#literal Pat lit | PConstruct { name; args } -> ( match translate_known_name name ~dict:library_constructor_patterns @@ -438,7 +444,7 @@ module Make (Options : OPTS) : MAKE = struct string "Ok" ^^ iblock parens (inner_expr_type_doc ^^ string "_to_bitstring" - ^^ iblock parens inner_expr_doc) + ^^ iblock parens inner_expr_doc) | Construct { constructor; _ } when Global_ident.eq_name Core__result__Result__Err constructor -> string "Err()" From 74f8ce726272d3652a9f68b4febdf191a74f7dd9 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:00:11 +0100 Subject: [PATCH 27/46] Allow `construct_base` AST feature --- 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 dc63a9d29..55e0927f7 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -11,6 +11,7 @@ include include On.Question_mark include On.Early_exit include On.Slice + include On.Construct_base end) (struct let backend = Diagnostics.Backend.ProVerif @@ -34,6 +35,7 @@ module SubtypeToInputLanguage and type slice = Features.On.slice and type question_mark = Features.On.question_mark and type macro = Features.On.macro + and type construct_base = Features.On.construct_base (* and type as_pattern = Features.Off.as_pattern *) (* and type nontrivial_lhs = Features.Off.nontrivial_lhs *) (* and type arbitrary_lhs = Features.Off.arbitrary_lhs *) @@ -68,7 +70,6 @@ struct let nontrivial_lhs = reject let arbitrary_lhs = reject let lifetime = reject - let construct_base = reject let monadic_action = reject let monadic_binding = reject let block = reject From 28256e2a982b9a86577ec12c0d23812e8f58385f Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:04:31 +0100 Subject: [PATCH 28/46] Print typed wildcards in all except parameter patterns --- engine/backends/proverif/proverif_backend.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 55e0927f7..4534e3853 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -314,6 +314,7 @@ module Make (Options : OPTS) : MAKE = struct method ty_bool = string "bool" method ty_int _ = string "nat" val mutable wildcard_index = 0 + method typed_wildcard = print#wildcard ^^ string ": bitstring" method wildcard = wildcard_index <- wildcard_index + 1; @@ -336,7 +337,7 @@ module Make (Options : OPTS) : MAKE = struct | Some (_, translation) -> translation args | None -> super#pat' ctx pat) | PWild -> - print#wildcard + print#typed_wildcard (* NOTE: Wildcard translation without collisions? *) | _ -> super#pat' ctx pat @@ -359,6 +360,15 @@ module Make (Options : OPTS) : MAKE = struct method tuple_elem_pat_at = print#par_state >> print#tuple_elem_pat + method pat_at : Generic_printer_base.ast_position -> pat fn = + fun pos pat -> + match pat with + | { p = PWild } -> ( + match pos with + | Param_pat -> print#wildcard + | _ -> print#pat (print#par_state pos) pat) + | _ -> print#pat (print#par_state pos) pat + method! pat_construct_tuple : pat list fn = List.map ~f:(print#tuple_elem_pat_at Pat_ConstructTuple) >> print#doc_construct_tuple From 444c887c7eaba681b4f69cd00441a940743ceef2 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:06:30 +0100 Subject: [PATCH 29/46] Special treatment of `Option` constructors The PV model for `Some` is `fun Some(bitstring): Option.`, so when we encounter `Some(inner_expr)` we wrap `inner_expr` with `T_to_bitstring()`, where `T` is the type of `inner_expr`, except in the case where `T` is a tuple type, since `(inner_tuple_element, ...)` is typed as `bitstring` already by ProVerif. --- engine/backends/proverif/proverif_backend.ml | 23 ++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 4534e3853..2d7eeaa60 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -330,6 +330,29 @@ module Make (Options : OPTS) : MAKE = struct fun pat -> match pat with | PConstant { lit } -> string "=" ^^ print#literal Pat lit + | PConstruct { name; args } + when Global_ident.eq_name Core__option__Option__None name -> + string "None()" + | PConstruct { name; args } + (* Some(expr) -> Some((expr))*) + when Global_ident.eq_name Core__option__Option__Some name -> + let inner_field = List.hd_exn args in + let inner_field_type_doc = + print#ty AlreadyPar inner_field.pat.typ + in + let inner_field_doc = print#pat ctx inner_field.pat in + let inner_block = + match inner_field.pat.typ with + | TApp { ident = `TupleType _ } + (* Tuple types should be translated without conversion from bitstring *) + -> + iblock parens inner_field_doc + | _ -> + iblock parens + (inner_field_type_doc ^^ string "_to_bitstring" + ^^ iblock parens inner_field_doc) + in + string "Some" ^^ inner_block | PConstruct { name; args } -> ( match translate_known_name name ~dict:library_constructor_patterns From 32963dea45a7cf48257c9fbf03b2acb1d1ee7e3c Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:11:48 +0100 Subject: [PATCH 30/46] Replace `QuestionMark` nodes with their contents Part of elision of `Result` types. --- engine/backends/proverif/proverif_backend.ml | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 2d7eeaa60..de387d18b 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -421,20 +421,7 @@ module Make (Options : OPTS) : MAKE = struct match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens in match e with - | QuestionMark { e; return_typ; _ } -> - let inner_type = - match return_typ with - | TApp { args; _ } -> - let g_type = List.hd_exn args in - print#generic_value g_type - in - inner_type ^^ string "_from_bitstring" - ^^ iblock parens - (string "unwrap_result" - (*^^ iblock parens - inner_type ^^ string "_to_bitstring"*) - ^^ iblock parens (print#expr ctx e)) - (* ) *) + | QuestionMark { e; return_typ; _ } -> print#expr ctx e (* Translate known functions *) | App { f = { e = GlobalVar name; _ }; args } -> ( match name with From 4ce1a4128ce6d5eaddc200c3e759f3ede7d84e3c Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:15:23 +0100 Subject: [PATCH 31/46] Formatting --- engine/backends/proverif/proverif_backend.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index de387d18b..e2fc0f6ca 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -494,18 +494,18 @@ module Make (Options : OPTS) : MAKE = struct (hardline ^^ string "else ") (fun { arm; span } -> print#match_arm scrutinee arm) arms - | If { cond; then_; else_ } -> + | If { cond; then_; else_ } -> ( let if_then = (string "if" ^//^ nest 2 (print#expr_at Expr_If_cond cond)) ^/^ string "then" ^//^ (print#expr_at Expr_If_then then_ |> parens |> nest 1) in - (match else_ with + match else_ with | None -> if_then | Some else_ -> if_then ^^ break 1 ^^ string "else" ^^ space - ^^ (print#expr_at Expr_If_else else_ |> iblock parens)) - |> wrap_parens + ^^ (print#expr_at Expr_If_else else_ |> iblock parens) + |> wrap_parens) | Let { monadic; lhs; rhs; body } -> (Option.map ~f:(fun monad -> print#expr_monadic_let ~monad) From cbae3eaec8fd968b31c4394a60b0d4f6764a11b1 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:15:31 +0100 Subject: [PATCH 32/46] Introduce `T_err()` process macros for every extracted type `T` --- engine/backends/proverif/proverif_backend.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index e2fc0f6ca..d9d8aa67c 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -630,6 +630,11 @@ module Make (Options : OPTS) : MAKE = struct ^^ print#concrete_ident name ^^ string "_default() = " ^^ print#concrete_ident name ^^ string "_default_c" ^^ dot in + let err_line = + string "letfun " ^^ print#concrete_ident name + ^^ string "_err() = let x = construct_fail() in " + ^^ print#concrete_ident name ^^ string "_default()" ^^ dot + in if is_struct then let struct_constructor = List.hd variants in match struct_constructor with @@ -637,13 +642,13 @@ module Make (Options : OPTS) : MAKE = struct | Some constructor -> type_line ^^ hardline ^^ to_bitstring_converter_line ^^ hardline ^^ from_bitstring_converter_line ^^ hardline - ^^ default_line ^^ hardline + ^^ default_line ^^ hardline ^^ err_line ^^ hardline ^^ fun_and_reduc name constructor else type_line ^^ hardline ^^ to_bitstring_converter_line ^^ hardline ^^ from_bitstring_converter_line ^^ hardline ^^ default_line ^^ hardline - ^^ separate_map (hardline ^^ hardline) + ^^ separate_map hardline (fun variant -> fun_and_reduc name variant) variants | _ -> empty From 2721d6d6af5476a4d4bd6435583f8f75e37ed73d Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:18:04 +0100 Subject: [PATCH 33/46] Special translation of `Result` types --- engine/backends/proverif/proverif_backend.ml | 43 ++++++++++++++++---- 1 file changed, 36 insertions(+), 7 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index d9d8aa67c..601fbac4b 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -458,17 +458,19 @@ module Make (Options : OPTS) : MAKE = struct args) | _ -> super#expr' ctx e))) | Construct { constructor; fields; _ } - when Global_ident.eq_name Core__result__Result__Ok constructor -> + when Global_ident.eq_name Core__option__Option__None constructor + -> + string "None()" + | Construct { constructor; fields; _ } + when Global_ident.eq_name Core__option__Option__Some constructor + -> let inner_expr = snd (Option.value_exn (List.hd fields)) in let inner_expr_type_doc = print#ty AlreadyPar inner_expr.typ in let inner_expr_doc = super#expr ctx inner_expr in - string "Ok" + string "Some" ^^ iblock parens (inner_expr_type_doc ^^ string "_to_bitstring" ^^ iblock parens inner_expr_doc) - | Construct { constructor; _ } - when Global_ident.eq_name Core__result__Result__Err constructor -> - string "Err()" (* Translate known constructors *) | Construct { constructor; fields } -> ( match @@ -713,6 +715,28 @@ module Make (Options : OPTS) : MAKE = struct string name | _ -> super#local_ident e + method! expr ctx e = + match e.e with + | _ -> ( + match e.typ with + | TApp { ident } + when Global_ident.eq_name Core__result__Result ident -> ( + match e.e with + | Construct { constructor; fields } + when Global_ident.eq_name Core__result__Result__Ok + constructor -> + let inner_expr = + snd (Option.value_exn (List.hd fields)) + in + let inner_expr_doc = super#expr ctx inner_expr in + inner_expr_doc + | Construct { constructor; _ } + when Global_ident.eq_name Core__result__Result__Err + constructor -> + print#ty ctx e.typ ^^ string "_err()" + | _ -> super#expr ctx e (*This cannot happen*)) + | _ -> super#expr ctx e) + method ty : Generic_printer_base.par_state -> ty fn = fun ctx ty -> match ty with @@ -727,8 +751,13 @@ module Make (Options : OPTS) : MAKE = struct when Global_ident.eq_name Core__option__Option ident -> string "Option" | TApp { ident; args } - when Global_ident.eq_name Core__result__Result ident -> - string "Result" + when Global_ident.eq_name Core__result__Result ident -> ( + (* print first of args*) + let result_ok_type = List.hd_exn args in + match result_ok_type with + | GType typ -> print#ty ctx typ + | GConst e -> print#expr ctx e + | _ -> empty (* Do not tranlsate lifetimes *)) | TApp { ident; args } -> super#ty ctx ty (*( match translate_known_name ident ~dict:library_types with From 73c553fd0deeeb6c6c1fc4c5273828b5e2526903 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:18:26 +0100 Subject: [PATCH 34/46] Special translation of `core::convert::Into::into` Assumes it's called with `bitstring` argument --- engine/backends/proverif/proverif_backend.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 601fbac4b..aae27be0a 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -717,6 +717,10 @@ module Make (Options : OPTS) : MAKE = struct method! expr ctx e = match e.e with + | App { f = { e = GlobalVar name; _ }; args } + when Global_ident.eq_name Core__convert__Into__into name -> + print#ty ctx e.typ ^^ string "_from_bitstring" + ^^ iblock parens (print#expr ctx (List.hd_exn args)) | _ -> ( match e.typ with | TApp { ident } From d24b14cb60bfc56f9d162f9d26c332ed43d58857 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:19:09 +0100 Subject: [PATCH 35/46] Translate `unimplemented!()` to appropriate `T_err()` invocation --- engine/backends/proverif/proverif_backend.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index aae27be0a..069f060d3 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -721,6 +721,9 @@ module Make (Options : OPTS) : MAKE = struct when Global_ident.eq_name Core__convert__Into__into name -> print#ty ctx e.typ ^^ string "_from_bitstring" ^^ iblock parens (print#expr ctx (List.hd_exn args)) + | App { f = { e = GlobalVar name; _ }; args } + when Global_ident.eq_name Rust_primitives__hax__never_to_any name -> + print#ty ctx e.typ ^^ string "_err()" | _ -> ( match e.typ with | TApp { ident } From 9b7949b43c7e23afe28b479d7c6feff1d8009e85 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:19:54 +0100 Subject: [PATCH 36/46] Define `core::convert::Into::into` name for the engine --- engine/names/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs index d9b5588ba..e7352ab9a 100644 --- a/engine/names/src/lib.rs +++ b/engine/names/src/lib.rs @@ -28,6 +28,7 @@ fn dummy_hax_concrete_ident_wrapper>(x: I, mu let _: Result<(), u32> = Result::Err(3u8).map_err(u32::from); let _ = [()].into_iter(); + let _: u16 = 6u8.into(); let _ = 1..2; let _ = 1..; let _ = ..; From 4a4275281e304fe8155b761b300a0e984638f48c Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:20:41 +0100 Subject: [PATCH 37/46] Clean up preamble to include handwritten general purpose definitions --- engine/backends/proverif/proverif_backend.ml | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 069f060d3..78bf01839 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -823,16 +823,20 @@ module Make (Options : OPTS) : MAKE = struct let banner = "Preamble" let preamble items = - "channel c.\n\ - fun int2bitstring(nat): bitstring.\n\ + "channel c.\n\n\ fun construct_fail() : bitstring\n\ reduc construct_fail() = fail.\n\n\ - const empty: bitstring.\n\n\ - type unimplemented.\n\n\ - const Unimplemented: unimplemented.\n\n\ - \ letfun bitstring_default() = empty.\n\n\ - \ letfun nat_default() = 0.\n\n\ - \ letfun bool_default() = false.\n" + type Option.\n\ + fun Some(bitstring): Option [data].\n\ + fun None(): Option [data].\n\ + letfun Option_err() = let x = construct_fail() in None().\n\n\ + const empty: bitstring.\n\ + letfun bitstring_default() = empty.\n\ + letfun bitstring_err() = let x = construct_fail() in \ + bitstring_default().\n\n\ + letfun nat_default() = 0.\n\ + fun nat_to_bitstring(nat): bitstring.\n\n\ + letfun bool_default() = false.\n" let contents items = "" end) From 22791a2f35dbd99629ebcc43a8d32cbc227f7cc2 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:21:06 +0100 Subject: [PATCH 38/46] Fix phase ordering --- engine/backends/proverif/proverif_backend.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 78bf01839..30a1d4b1a 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -921,10 +921,10 @@ module TransformToInputLanguage = |> Phases.Drop_blocks |> Phases.Drop_references |> Phases.Trivialize_assign_lhs - (* |> Side_effect_utils.Hoist *) + |> Phases.Reconstruct_question_marks + |> Side_effect_utils.Hoist |> Phases.Local_mutation |> Phases.Reject.Continue - |> Phases.Reconstruct_question_marks |> SubtypeToInputLanguage |> Identity ] From c416ffa0b08226d9542d4015ea1dc553cf90e90d Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:21:32 +0100 Subject: [PATCH 39/46] Remove obsolete placeholder comments --- engine/backends/proverif/proverif_backend.ml | 134 +------------------ 1 file changed, 5 insertions(+), 129 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 30a1d4b1a..c7264beb2 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -145,143 +145,19 @@ module Make (Options : OPTS) : MAKE = struct (* TODO: Give definitions for core / known library functions, cf issues #447, #448 *) let library_functions : (Concrete_ident_generated.name * (AST.expr list -> document)) list = - [ - (* (\* Core dependencies *\) *) - (Rust_primitives__hax__never_to_any, fun _ -> string "construct_fail()") - (* (Alloc__vec__from_elem, fun args -> string "PLACEHOLDER_library_function"); *) - (* ( Alloc__slice__Impl__to_vec, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (Core__slice__Impl__len, fun args -> string "PLACEHOLDER_library_function"); *) - (* ( Core__ops__deref__Deref__deref, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Core__ops__index__Index__index, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Rust_primitives__unsize, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Core__num__Impl_9__to_le_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__slice__Impl__into_vec, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__vec__Impl_1__truncate, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__vec__Impl_2__extend_from_slice, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Alloc__slice__Impl__concat, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* ( Core__option__Impl__is_some, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::clone::Clone_f_clone *\) *) - (* ( Core__clone__Clone__clone, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::cmp::PartialEq::eq *\) *) - (* ( Core__cmp__PartialEq__eq, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::cmp::PartialEq_f_ne *\) *) - (* ( Core__cmp__PartialEq__ne, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::cmp::PartialOrd::lt *\) *) - (* ( Core__cmp__PartialOrd__lt, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::ops::arith::Add::add *\) *) - (* ( Core__ops__arith__Add__add, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::ops::arith::Sub::sub *\) *) - (* ( Core__ops__arith__Sub__sub, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::option::Option_Option_None_c *\) *) - (* ( Core__option__Option__None, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::option::Option_Option_Some_c *\) *) - (* ( Core__option__Option__Some, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* core::result::impl__map_err *\) *) - (* ( Core__result__Impl__map_err, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* Crypto dependencies *\) *) - (* (\* hax_lib_protocol::cal::hash *\) *) - (* ( Hax_lib_protocol__crypto__hash, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::hmac *\) *) - (* ( Hax_lib_protocol__crypto__hmac, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::aead_decrypt *\) *) - (* ( Hax_lib_protocol__crypto__aead_decrypt, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::aead_encrypt *\) *) - (* ( Hax_lib_protocol__crypto__aead_encrypt, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::dh_scalar_multiply *\) *) - (* ( Hax_lib_protocol__crypto__dh_scalar_multiply, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::dh_scalar_multiply_base *\) *) - (* ( Hax_lib_protocol__crypto__dh_scalar_multiply_base, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__DHScalar__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__DHElement__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_1__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__AEADKey__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_4__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__AEADIV__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_5__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *) - (* (\* hax_lib_protocol::cal::impl__AEADTag__from_bytes *\) *) - (* ( Hax_lib_protocol__crypto__Impl_6__from_bytes, *) - (* fun args -> string "PLACEHOLDER_library_function" ); *); - ] + [] let library_constructors : (Concrete_ident_generated.name * ((global_ident * AST.expr) list -> document)) list = - [ (* ( Core__option__Option__Some, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__option__Option__None, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__ops__range__Range, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::(HashAlgorithm_HashAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HashAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::DHGroup_DHGroup_X25519_c *\) *) - (* ( Hax_lib_protocol__crypto__DHGroup__X25519, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::AEADAlgorithm_AEADAlgorithm_Chacha20Poly1305_c *\) *) - (* ( Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::HMACAlgorithm_HMACAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HMACAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) ] + [] let library_constructor_patterns : (Concrete_ident_generated.name * (field_pat list -> document)) list = - [ (* ( Core__option__Option__Some, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__option__Option__None, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* ( Core__ops__range__Range, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::(HashAlgorithm_HashAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HashAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::DHGroup_DHGroup_X25519_c *\) *) - (* ( Hax_lib_protocol__crypto__DHGroup__X25519, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::AEADAlgorithm_AEADAlgorithm_Chacha20Poly1305_c *\) *) - (* ( Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) - (* (\* hax_lib_protocol::cal::HMACAlgorithm_HMACAlgorithm_Sha256_c *\) *) - (* ( Hax_lib_protocol__crypto__HMACAlgorithm__Sha256, *) - (* fun args -> string "PLACEHOLDER_library_constructor" ); *) ] - - let library_types : (Concrete_ident_generated.name * document) list = - [ (* (\* hax_lib_protocol::cal::(t_DHScalar *\) *) - (* (Hax_lib_protocol__crypto__DHScalar, string "PLACEHOLDER_library_type"); *) - (* (Core__option__Option, string "PLACEHOLDER_library_type"); *) - (* (Alloc__vec__Vec, string "PLACEHOLDER_library_type"); *) ] + [] + + let library_types : (Concrete_ident_generated.name * document) list = [] let assoc_known_name name (known_name, _) = Global_ident.eq_name known_name name From 9f5fbea8873df56780ea3cf5e81d2f596ad317cd Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:31:31 +0100 Subject: [PATCH 40/46] Remove unnecessary `?` detection All question marks should be re-sugared by a phase and then treated at another place. --- engine/backends/proverif/proverif_backend.ml | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index c7264beb2..5b9cb015d 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -354,19 +354,6 @@ module Make (Options : OPTS) : MAKE = struct with | Some (name, translation) -> translation fields | None -> super#expr' ctx e) - (* Desugared `?` operator *) - | Match - { - scrutinee = - { - e = App { f = { e = GlobalVar n; _ }; args = [ expr ] }; - _; - }; - arms = _; - } - (*[@ocamlformat "disable"]*) - when Global_ident.eq_name Core__ops__try_trait__Try__branch n -> - print#expr' ctx expr.e | Match { scrutinee; arms } -> separate_map (hardline ^^ string "else ") From 35f9405ac250f05d986ed7d5aa8272f18e91756e Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 14:41:54 +0100 Subject: [PATCH 41/46] Indicate clearly when an inherited method is overridden --- engine/backends/proverif/proverif_backend.ml | 64 +++++++++++--------- 1 file changed, 34 insertions(+), 30 deletions(-) diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 5b9cb015d..e541cd6ea 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -169,6 +169,7 @@ module Make (Options : OPTS) : MAKE = struct object (print) inherit GenericPrint.print as super + (* Backend-specific utilities *) method field_accessor field_name = string "accessor" ^^ underscore ^^ print#concrete_ident field_name @@ -187,16 +188,35 @@ module Make (Options : OPTS) : MAKE = struct string "let" ^^ space ^^ pat ^^ string " = " ^^ scrutinee ^^ string " in " ^^ body - method ty_bool = string "bool" - method ty_int _ = string "nat" val mutable wildcard_index = 0 - method typed_wildcard = print#wildcard ^^ string ": bitstring" method wildcard = wildcard_index <- wildcard_index + 1; string "wildcard" ^^ OCaml.int wildcard_index - method pat' : Generic_printer_base.par_state -> pat' fn = + method typed_wildcard = print#wildcard ^^ string ": bitstring" + + method tuple_elem_pat' : Generic_printer_base.par_state -> pat' fn = + fun ctx -> + let wrap_parens = + group + >> + match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens + in + function + | PBinding { mut; mode; var; typ; subpat } -> + let p = print#local_ident var in + p ^^ colon ^^ space ^^ print#ty ctx typ + | p -> print#pat' ctx p + + method tuple_elem_pat : Generic_printer_base.par_state -> pat fn = + fun ctx { p; span; _ } -> + print#with_span ~span (fun _ -> print#tuple_elem_pat' ctx p) + + method tuple_elem_pat_at = print#par_state >> print#tuple_elem_pat + + (* Overridden methods *) + method! pat' : Generic_printer_base.par_state -> pat' fn = fun ctx -> let wrap_parens = group @@ -240,26 +260,10 @@ module Make (Options : OPTS) : MAKE = struct (* NOTE: Wildcard translation without collisions? *) | _ -> super#pat' ctx pat - method tuple_elem_pat' : Generic_printer_base.par_state -> pat' fn = - fun ctx -> - let wrap_parens = - group - >> - match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock parens - in - function - | PBinding { mut; mode; var; typ; subpat } -> - let p = print#local_ident var in - p ^^ colon ^^ space ^^ print#ty ctx typ - | p -> print#pat' ctx p - - method tuple_elem_pat : Generic_printer_base.par_state -> pat fn = - fun ctx { p; span; _ } -> - print#with_span ~span (fun _ -> print#tuple_elem_pat' ctx p) - - method tuple_elem_pat_at = print#par_state >> print#tuple_elem_pat + method! ty_bool = string "bool" + method! ty_int _ = string "nat" - method pat_at : Generic_printer_base.ast_position -> pat fn = + method! pat_at : Generic_printer_base.ast_position -> pat fn = fun pos pat -> match pat with | { p = PWild } -> ( @@ -380,7 +384,7 @@ module Make (Options : OPTS) : MAKE = struct |> wrap_parens | _ -> super#expr' ctx e - method concrete_ident = print#concrete_ident' ~under_current_ns:false + method! concrete_ident = print#concrete_ident' ~under_current_ns:false method! item_unwrapped item = let assume_item = @@ -527,7 +531,7 @@ module Make (Options : OPTS) : MAKE = struct ^^ space ^^ string "in" ^^ hardline ^^ (print#expr_at Expr_Let_body body |> group) - method concrete_ident' ~(under_current_ns : bool) : concrete_ident fn = + method! concrete_ident' ~(under_current_ns : bool) : concrete_ident fn = fun id -> if under_current_ns then print#name_of_concrete_ident id else @@ -555,19 +559,19 @@ module Make (Options : OPTS) : MAKE = struct print#concrete_ident constructor ^^ iblock parens (separate_map (comma ^^ break 1) snd args) - method generic_values : generic_value list fn = + method! generic_values : generic_value list fn = function | [] -> empty | values -> string "_of" ^^ underscore ^^ separate_map underscore print#generic_value values - method ty_app f args = + method! ty_app f args = print#concrete_ident f ^^ print#generic_values args - method ty_tuple _ _ = string "bitstring" + method! ty_tuple _ _ = string "bitstring" - method local_ident e = + method! local_ident e = match String.chop_prefix ~prefix:"impl " e.name with | Some name -> let name = @@ -607,7 +611,7 @@ module Make (Options : OPTS) : MAKE = struct | _ -> super#expr ctx e (*This cannot happen*)) | _ -> super#expr ctx e) - method ty : Generic_printer_base.par_state -> ty fn = + method! ty : Generic_printer_base.par_state -> ty fn = fun ctx ty -> match ty with | TBool -> print#ty_bool From 6e0b63726f4c2d627bda47e473e51c47a54a07ca Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 15:16:44 +0100 Subject: [PATCH 42/46] Fix merge error --- engine/bin/lib.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml index 27640efa2..5e03c2351 100644 --- a/engine/bin/lib.ml +++ b/engine/bin/lib.ml @@ -90,7 +90,7 @@ let run (options : Types.engine_options) : Types.output = | Fstar opts -> run (module Fstar_backend) opts | Coq -> run (module Coq_backend) () | Ssprove -> run (module Ssprove_backend) () - | Easycrypt -> run (module Easycrypt_backend) () + | Easycrypt -> run (module Easycrypt_backend) ()) in { diagnostics = List.map ~f:Diagnostics.to_thir_diagnostic diagnostics; From 8abb471ef8424ed0557c9457fa204a58726078e1 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 5 Mar 2024 15:17:18 +0100 Subject: [PATCH 43/46] Formatting --- engine/lib/phases/phase_reconstruct_question_marks.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/engine/lib/phases/phase_reconstruct_question_marks.ml b/engine/lib/phases/phase_reconstruct_question_marks.ml index 43e1f973c..c5f0c855a 100644 --- a/engine/lib/phases/phase_reconstruct_question_marks.ml +++ b/engine/lib/phases/phase_reconstruct_question_marks.ml @@ -85,8 +85,7 @@ module%inlined_contents Make (FA : Features.T) = struct let map_err (e : expr) (error_dest : ty) impl : expr option = let* success, error_src = expect_result_type e.typ in let* impl = expect_residual_impl_result impl in - if [%equal: ty] error_src error_dest then - Some e + if [%equal: ty] error_src error_dest then Some e else let from_typ = TArrow ([ error_src ], error_dest) in let from = From 5f15813043863f6f480b3764f2ff71fdcef72a39 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Mon, 11 Mar 2024 10:32:42 +0100 Subject: [PATCH 44/46] Update SSProve side effect snapshot --- .../src/snapshots/toolchain__side-effects into-ssprove.snap | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap index 01ca06526..494f1f86a 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap @@ -1,5 +1,6 @@ --- source: test-harness/src/harness.rs +assertion_line: 214 expression: snapshot info: kind: @@ -18,6 +19,7 @@ info: stderr: true stdout: true include_flag: ~ + backend_options: ~ --- exit = 0 stderr = ''' @@ -64,7 +66,7 @@ Fail Next Obligation. Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) := direct_result_question_mark y := - solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := impl__map_err y f_from in + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := y in Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32). Fail Next Obligation. @@ -221,7 +223,7 @@ Notation "'Build_t_Bar' '[' x ']' '(' 'f_b' ':=' y ')'" := (Build_t_Bar (f_a := Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) := monad_lifting x := solve_lift (run (ifb x >.? (ret_both (123 : int8)) - then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist33 := ControlFlow_Continue (impl__map_err (Result_Err B) f_from) in + then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist33 := ControlFlow_Continue (Result_Err B) in letb hoist34 := Result_Ok hoist33 in letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist35 := v_Break hoist34 in ControlFlow_Continue (never_to_any hoist35) From 0c7ce6f2aaf4b2160777b26c7af38ab71db8fa27 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Mon, 11 Mar 2024 10:34:04 +0100 Subject: [PATCH 45/46] Update FStar side-effect snapshot --- .../toolchain__side-effects into-fstar.snap | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap index e154b698e..4a0d11ab6 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -1,5 +1,6 @@ --- source: test-harness/src/harness.rs +assertion_line: 214 expression: snapshot info: kind: @@ -17,6 +18,8 @@ info: snapshot: stderr: true stdout: true + include_flag: ~ + backend_options: ~ --- exit = 0 stderr = ''' @@ -38,9 +41,7 @@ let add3 (x y z: u32) : u32 = let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32) : Core.Result.t_Result i8 u32 = - Rust_primitives.Hax.Control_flow_monad.Mresult.run (let| _:Prims.unit = - Core.Result.impl__map_err y (Core.Convert.f_from <: u32 -> u32) - in + Rust_primitives.Hax.Control_flow_monad.Mresult.run (let| _:Prims.unit = y in Core.Result.Result_Ok (Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32) <: Core.Result.t_Result (Core.Result.t_Result i8 u32) u32) @@ -225,10 +226,7 @@ let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B = then let! hoist33:t_A = Core.Ops.Control_flow.ControlFlow_Continue - (Core.Result.impl__map_err (Core.Result.Result_Err (B <: t_B) - <: - Core.Result.t_Result t_A t_B) - (Core.Convert.f_from <: t_B -> t_B)) + (Core.Result.Result_Err (B <: t_B) <: Core.Result.t_Result t_A t_B) <: Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_A t_B) (Core.Result.t_Result t_A t_B) From 7a71583a60b8590bb6b3c3e8a9cbe10385c28422 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 13 Mar 2024 08:56:16 +0100 Subject: [PATCH 46/46] Documentation for ProVerif `--assume-items` option --- cli/options/src/lib.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs index dac76cb1a..6a9af7b39 100644 --- a/cli/options/src/lib.rs +++ b/cli/options/src/lib.rs @@ -115,6 +115,14 @@ impl NormalizePaths for PathOrDash { #[derive(JsonSchema, Parser, Debug, Clone, Serialize, Deserialize)] pub struct ProVerifOptions { + /// Items for which hax should extract a default-valued process + /// macro with a corresponding type signature. This flag expects a + /// space-separated list of inclusion clauses. An inclusion clause + /// is a Rust path prefixed with `+`, `+!` or `-`. `-` means + /// implementation only, `+!` means interface only and `+` means + /// implementation and interface. Rust path chunks can be either a + /// concrete string, or a glob (just like bash globs, but with + /// Rust paths). #[arg( long, value_parser = parse_inclusion_clause,