feat(lean): add proof attribute

CHANGELOG.md

@@ -47,6 +47,7 @@ Changes to the Lean backend:
    extra parameters (#1803)
  - Add generation of specs from requires/ensures-annotations (#1815)
  - Add support for nonliteral array sizes (#1826)
+ - Add `hax_lib::lean::proof` attribute (#1831)
 
 Miscellaneous:
 - Reserve extraction folder for auto-generated files in Lean examples (#1754)

hax-lib/build.rs

@@ -9,6 +9,10 @@ pub use hax_lib_macros::fstar_smt_pat as smt_pat;
 pub use hax_lib_macros::fstar_postprocess_with as postprocess_with;
 ";
 
+const LEAN_EXTRA: &str = r"
+pub use hax_lib_macros::lean_proof as proof;
+";
+
 fn main() {
     let code = |backend: &str, extra: &str| {
         format!(
@@ -43,7 +47,7 @@ pub mod {backend} {{
             code("fstar", FSTAR_EXTRA),
             code("proverif", ""),
             code("coq", ""),
-            code("lean", ""),
+            code("lean", LEAN_EXTRA),
         ]
         .join("\n"),
     )

hax-lib/macros/src/dummy.rs

@@ -6,7 +6,7 @@ use quote::quote;
 use syn::{visit_mut::VisitMut, *};
 
 macro_rules! identity_proc_macro_attribute {
-    ($($name:ident,)*) => {
+    ($($name:ident),*$(,)?) => {
         $(
             #[proc_macro_attribute]
             pub fn $name(_attr: TokenStream, item: TokenStream) -> TokenStream {
@@ -52,6 +52,7 @@ identity_proc_macro_attribute!(
     proverif_after,
     fstar_smt_pat,
     fstar_postprocess_with,
+    lean_proof,
 );
 
 #[proc_macro]

hax-lib/macros/src/implementation.rs

@@ -9,15 +9,15 @@ mod prelude {
     pub use crate::hax_paths::*;
     pub use crate::syn_ext::*;
     pub use proc_macro as pm;
-    pub use proc_macro2::*;
     pub use proc_macro_error2::*;
+    pub use proc_macro2::*;
     pub use quote::*;
     pub use std::collections::HashSet;
     pub use syn::spanned::Spanned;
     pub use syn::{visit_mut::VisitMut, *};
 
-    pub use hax_lib_macros_types::*;
     pub use AttrPayload::Language as AttrHaxLang;
+    pub use hax_lib_macros_types::*;
     pub type FnLike = syn::ImplItemFn;
 }
 
@@ -249,7 +249,7 @@ pub fn modeled_by(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStre
 #[proc_macro_attribute]
 pub fn lemma(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
     let mut item: syn::ItemFn = parse_macro_input!(item as ItemFn);
-    use syn::{spanned::Spanned, GenericArgument, PathArguments, ReturnType};
+    use syn::{GenericArgument, PathArguments, ReturnType, spanned::Spanned};
 
     fn add_allow_unused_variables_to_args(func: &mut syn::ItemFn) {
         let attr: syn::Attribute = parse_quote!(#[allow(unused_variables)]);
@@ -823,6 +823,16 @@ pub fn int(payload: pm::TokenStream) -> pm::TokenStream {
     quote! {::hax_lib::int::Int::_unsafe_from_str(#digits)}.into()
 }
 
+/// This macro inserts a verbatim Lean proof into the extracted code.
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn lean_proof(payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+    let item: ItemFn = parse_macro_input!(item);
+    let payload = parse_macro_input!(payload as LitStr).value();
+    let attr = AttrPayload::Proof(payload);
+    quote! {#attr #item}.into()
+}
+
 macro_rules! make_quoting_item_proc_macro {
     ($backend:ident, $macro_name:ident, $position:expr, $cfg_name:ident) => {
         #[doc = concat!("This macro inlines verbatim ", stringify!($backend)," code before a Rust item.")]

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

@@ -133,6 +133,7 @@ pub enum AttrPayload {
     ProcessRead,
     ProcessWrite,
     ProcessInit,
+    Proof(String),
     ProtocolMessages,
     PVConstructor,
     PVHandwritten,

rust-engine/src/backends/lean.rs

@@ -4,12 +4,15 @@
 //! Pretty::Doc type, which can in turn be exported to string (or, eventually,
 //! source maps).
 
+use hax_lib_macros_types::AttrPayload;
 use std::collections::HashSet;
 use std::sync::LazyLock;
 
 use super::prelude::*;
 use crate::{
     ast::identifiers::global_id::view::{ConstructorKind, PathSegment, TypeDefKind},
+    attributes::hax_attributes,
+    names::rust_primitives::hax::explicit_monadic::{lift, pure},
     phase::*,
 };
 
@@ -19,7 +22,6 @@ mod binops {
     pub use crate::names::rust_primitives::hax::{logical_op_and, logical_op_or};
 }
 
-use crate::names::rust_primitives::hax::explicit_monadic::{lift, pure};
 const LIFT: GlobalId = lift;
 const PURE: GlobalId = pure;
 
@@ -470,6 +472,15 @@ const _: () = {
             if spec.precondition.is_none() && spec.postcondition.is_none() {
                 nil!()
             } else {
+                let proofs: Vec<&String> = hax_attributes(&item.meta.attributes)
+                    .flat_map(|attr| match attr {
+                        AttrPayload::Proof(proof) => Some(proof),
+                        _ => None,
+                    })
+                    .collect();
+                if proofs.len() > 1 {
+                    emit_error!("Only one proof attribute per item is allowed.");
+                }
                 docs![
                     hardline!(),
                     hardline!(),
@@ -542,9 +553,17 @@ const _: () = {
                         hardline!(),
                         "pureEnsures := by constructor; intros; mvcgen <;> try grind",
                         hardline!(),
-                        docs!["contract := by mvcgen[", name, "] <;> try grind"]
-                            .group()
-                            .nest(INDENT),
+                        docs![
+                            "contract :=",
+                            line!(),
+                            if proofs.is_empty() {
+                                docs!["by mvcgen[", name, "] <;> try grind"]
+                            } else {
+                                docs![intersperse!(proofs, nil!())]
+                            }
+                        ]
+                        .group()
+                        .nest(INDENT),
                         hardline!(),
                     ]
                     .nest(INDENT)

test-harness/src/snapshots/toolchain__lean-tests into-lean.snap

@@ -886,6 +886,19 @@ def Lean_tests.Specs.test.spec (x : u8)  :
   contract := by mvcgen[Lean_tests.Specs.test] <;> try grind
 }
 
+def Lean_tests.Specs.test_proof (x : u8) : RustM u8 := do (pure x)
+
+@[spec]
+def Lean_tests.Specs.test_proof.spec (x : u8)  :
+    Spec
+      (requires := (Rust_primitives.Hax.Machine_int.gt x (0 : u8)))
+      (ensures := fun r => (Rust_primitives.Hax.Machine_int.eq r x))
+      (Lean_tests.Specs.test_proof (x : u8) ) := {
+  pureRequires := by constructor; mvcgen <;> try grind
+  pureEnsures := by constructor; intros; mvcgen <;> try grind
+  contract := by unfold Lean_tests.Specs.test_proof; hax_bv_decide
+}
+
 structure Lean_tests.Monadic.S where
   f : u32
 

tests/lean-tests/proofs/lean/lakefile.toml

@@ -0,0 +1,11 @@
+name = "Lean_tests"
+version = "0.1.0"
+defaultTargets = ["Lean_tests"]
+
+[[lean_lib]]
+name = "Lean_tests"
+roots = ["extraction.Lean_tests"]
+
+[[require]]
+name = "Hax"
+path = "../../../../hax-lib/proof-libs/lean"

tests/lean-tests/proofs/lean/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.23.0

tests/lean-tests/src/specs.rs

@@ -3,3 +3,10 @@
 fn test(x: u8) -> u8 {
     x
 }
+
+#[hax_lib::requires(x > 0)]
+#[hax_lib::ensures(|r| r == x)]
+#[hax_lib::lean::proof("by unfold Lean_tests.Specs.test_proof; hax_bv_decide")]
+fn test_proof(x: u8) -> u8 {
+    x
+}