Lean backend [M2] - 1/3 - First proofs

engine/backends/lean/dune

@@ -0,0 +1,21 @@
+(library
+ (name lean_backend)
+ (package hax-engine)
+ (wrapped false)
+ (libraries hax_engine base)
+ (preprocess
+  (pps
+   ppx_yojson_conv
+   ppx_sexp_conv
+   ppx_compare
+   ppx_hash
+   ppx_deriving.show
+   ppx_deriving.eq
+   ppx_inline
+   ppx_functor_application
+   ppx_matches)))
+
+(env
+ (_
+  (flags
+   (:standard -w -A))))

engine/backends/lean/lean_backend.ml

@@ -0,0 +1,132 @@
+open Hax_engine
+open Utils
+open Base
+
+include
+  Backend.Make
+    (struct
+      open Features
+      include Off
+      include On.Monadic_binding
+      include On.Slice
+      include On.Macro
+      include On.Construct_base
+      include On.Quote
+      include On.Dyn
+      include On.Unsafe
+    end)
+    (struct
+      let backend = Diagnostics.Backend.FStar
+    end)
+
+module SubtypeToInputLanguage
+    (FA :
+      Features.T
+        with type mutable_reference = Features.Off.mutable_reference
+         and type continue = Features.Off.continue
+         and type break = Features.Off.break
+         and type mutable_reference = Features.Off.mutable_reference
+         and type mutable_pointer = Features.Off.mutable_pointer
+         and type mutable_variable = Features.Off.mutable_variable
+         and type reference = Features.Off.reference
+         and type raw_pointer = Features.Off.raw_pointer
+         and type early_exit = Features.Off.early_exit
+         and type question_mark = Features.Off.question_mark
+         and type as_pattern = Features.Off.as_pattern
+         and type lifetime = Features.Off.lifetime
+         and type monadic_action = Features.Off.monadic_action
+         and type arbitrary_lhs = Features.Off.arbitrary_lhs
+         and type nontrivial_lhs = Features.Off.nontrivial_lhs
+         and type loop = Features.Off.loop
+         and type block = Features.Off.block
+         and type for_loop = Features.Off.for_loop
+         and type while_loop = Features.Off.while_loop
+         and type for_index_loop = Features.Off.for_index_loop
+         and type state_passing_loop = Features.Off.state_passing_loop
+         and type fold_like_loop = Features.Off.fold_like_loop
+         and type match_guard = Features.Off.match_guard
+         and type trait_item_default = Features.Off.trait_item_default) =
+struct
+  module FB = InputLanguage
+
+  include
+    Subtype.Make (FA) (FB)
+      (struct
+        module A = FA
+        module B = FB
+        include Features.SUBTYPE.Id
+        include Features.SUBTYPE.On.Monadic_binding
+        include Features.SUBTYPE.On.Construct_base
+        include Features.SUBTYPE.On.Slice
+        include Features.SUBTYPE.On.Macro
+        include Features.SUBTYPE.On.Quote
+        include Features.SUBTYPE.On.Dyn
+        include Features.SUBTYPE.On.Unsafe
+      end)
+
+  let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
+end
+
+module AST = Ast.Make (InputLanguage)
+
+module BackendOptions = struct
+  type t = Hax_engine.Types.f_star_options_for__null
+end
+
+open Ast
+module U = Ast_utils.Make (InputLanguage)
+module Visitors = Ast_visitors.Make (InputLanguage)
+open AST
+
+module Context = struct
+  type t = {
+    current_namespace : string list;
+    items : item list;
+    interface_mode : bool;
+    line_width : int;
+  }
+end
+
+open Phase_utils
+module DepGraphR = Dependencies.Make (Features.Rust)
+
+module TransformToInputLanguage =
+  [%functor_application
+    Phases.Reject.RawOrMutPointer(Features.Rust)
+  |> Phases.Transform_hax_lib_inline
+  |> Phases.Specialize
+  |> Phases.Drop_sized_trait
+  |> Phases.Simplify_question_marks
+  |> Phases.And_mut_defsite
+  |> Phases.Reconstruct_asserts
+  |> Phases.Reconstruct_for_loops
+  |> Phases.Reconstruct_while_loops
+  |> Phases.Direct_and_mut
+  |> Phases.Reject.Arbitrary_lhs
+  |> Phases.Drop_blocks
+  |> Phases.Drop_match_guards
+  |> Phases.Drop_references
+  |> Phases.Trivialize_assign_lhs
+  |> Side_effect_utils.Hoist
+  |> Phases.Hoist_disjunctive_patterns
+  |> Phases.Simplify_match_return
+  |> Phases.Local_mutation
+  |> Phases.Rewrite_control_flow
+  |> Phases.Drop_return_break_continue
+  |> Phases.Functionalize_loops
+  |> Phases.Reject.Question_mark
+  |> Phases.Reject.As_pattern
+  |> Phases.Traits_specs
+  |> Phases.Simplify_hoisting
+  |> Phases.Newtype_as_refinement
+  |> Phases.Reject.Trait_item_default
+  |> Phases.Bundle_cycles
+  |> Phases.Reorder_fields
+  |> Phases.Sort_items
+  |> SubtypeToInputLanguage
+  |> Identity
+  ]
+  [@ocamlformat "disable"]
+
+let apply_phases (items : Ast.Rust.item list) : AST.item list =
+  TransformToInputLanguage.ditems items

engine/bin/dune

@@ -5,6 +5,7 @@
  (libraries
   hax_engine
   fstar_backend
+  lean_backend
   coq_backend
   ssprove_backend
   easycrypt_backend

engine/bin/lib.ml

@@ -257,7 +257,7 @@ let engine () =
       Printexc.raise_with_backtrace exn bt
 
 module ExportRustAst = Export_ast.Make (Features.Rust)
-module ExportFStarAst = Export_ast.Make (Fstar_backend.InputLanguage)
+module ExportLeanAst = Export_ast.Make (Lean_backend.InputLanguage)
 
 (** Entry point for interacting with the Rust hax engine *)
 let driver_for_rust_engine () : unit =
@@ -272,26 +272,16 @@ let driver_for_rust_engine () : unit =
   match query.kind with
   | Types.ImportThir { input; apply_phases } ->
       (* Note: `apply_phases` comes from the type `QueryKind` in
-      `ocaml_engine.rs`. This is a temporary flag that applies some phases while
-      importing THIR. In the future (when #1550 is merged), we will be able to
-      import THIR and then apply phases. *)
+       `ocaml_engine.rs`. This is a temporary flag that applies some phases while
+       importing THIR. In the future (when #1550 is merged), we will be able to
+       import THIR and then apply phases. *)
       let imported_items = import_thir_items [] input in
       let rust_ast_items =
         if apply_phases then
-          let imported_items =
-            (* TODO: this let binding is applying the phases from the F* backend *)
-            Fstar_backend.apply_phases
-              {
-                cli_extension = EmptyStructempty_args_extension;
-                fuel = Int64.zero;
-                ifuel = Int64.zero;
-                interfaces = [];
-                line_width = 80;
-                z3rlimit = Int64.zero;
-              }
-              imported_items
-          in
-          List.concat_map ~f:ExportFStarAst.ditem imported_items
+          let imported_items = Lean_backend.apply_phases imported_items in
+          List.concat_map
+            ~f:(fun item -> ExportLeanAst.ditem item)
+            imported_items
         else List.concat_map ~f:ExportRustAst.ditem imported_items
       in
       let response = Rust_engine_types.ImportThir { output = rust_ast_items } in

examples/default.nix

@@ -8,6 +8,7 @@
   hax-env,
   jq,
   proverif,
+  lean4,
 }: let
   commonArgs = import ./commonArgs.nix {inherit craneLib lib;};
   cargoArtifacts = craneLib.buildDepsOnly commonArgs;
@@ -29,7 +30,7 @@ in
         make
       '';
       buildInputs = [
-        hax hax-env fstar jq
+        hax hax-env fstar jq lean4
         (proverif.overrideDerivation (_: {
           patches = [ ./proverif-psk/pv_div_by_zero_fix.diff ];
         }))

hax-lib/build.rs

@@ -43,6 +43,7 @@ pub mod {backend} {{
             code("fstar", FSTAR_EXTRA),
             code("proverif", ""),
             code("coq", ""),
+            code("lean", ""),
         ]
         .join("\n"),
     )

hax-lib/macros/src/dummy.rs

@@ -36,15 +36,19 @@ identity_proc_macro_attribute!(
     refinement_type,
     fstar_replace,
     coq_replace,
+    lean_replace,
     proverif_replace,
     fstar_replace_body,
     coq_replace_body,
+    lean_replace_body,
     proverif_replace_body,
     fstar_before,
     coq_before,
+    lean_before,
     proverif_before,
     fstar_after,
     coq_after,
+    lean_after,
     proverif_after,
     fstar_smt_pat,
     fstar_postprocess_with,
@@ -59,6 +63,10 @@ pub fn coq_expr(_payload: TokenStream) -> TokenStream {
     quote! { () }.into()
 }
 #[proc_macro]
+pub fn lean_expr(_payload: TokenStream) -> TokenStream {
+    quote! { () }.into()
+}
+#[proc_macro]
 pub fn proverif_expr(_payload: TokenStream) -> TokenStream {
     quote! { () }.into()
 }
@@ -84,6 +92,10 @@ pub fn coq_unsafe_expr(_payload: TokenStream) -> TokenStream {
     unsafe_expr()
 }
 #[proc_macro]
+pub fn lean_unsafe_expr(_payload: TokenStream) -> TokenStream {
+    unsafe_expr()
+}
+#[proc_macro]
 pub fn proverif_unsafe_expr(_payload: TokenStream) -> TokenStream {
     unsafe_expr()
 }
@@ -97,6 +109,10 @@ pub fn coq_prop_expr(_payload: TokenStream) -> TokenStream {
     quote! {::hax_lib::Prop::from_bool(true)}.into()
 }
 #[proc_macro]
+pub fn lean_prop_expr(_payload: TokenStream) -> TokenStream {
+    quote! {::hax_lib::Prop::from_bool(true)}.into()
+}
+#[proc_macro]
 pub fn proverif_prop_expr(_payload: TokenStream) -> TokenStream {
     quote! {::hax_lib::Prop::from_bool(true)}.into()
 }

hax-lib/macros/src/implementation.rs

@@ -989,7 +989,7 @@ macro_rules! make_quoting_proc_macro {
     }
 }
 
-make_quoting_proc_macro!(fstar coq proverif);
+make_quoting_proc_macro!(fstar coq proverif lean);
 
 /// Marks a newtype `struct RefinedT(T);` as a refinement type. The
 /// struct should have exactly one unnamed private field.

hax-lib/macros/src/utils.rs

@@ -10,6 +10,7 @@ impl ToTokens for HaxQuantifiers {
         quote! {
             use ::hax_lib::fstar::prop as fstar;
             use ::hax_lib::coq::prop as coq;
+            use ::hax_lib::lean::prop as lean;
             use ::hax_lib::proverif::prop as proverif;
         }
         .to_tokens(tokens)