feat(lean): Add support for namespaces

CHANGELOG.md

@@ -30,6 +30,8 @@ Changes to the Lean backend:
  - Use the explicit monadic phase to insert `pure` and `←` only on demand, and
    not introduce extra `do` block (#1746)
  - Rename `Result` monad to `RustM` to avoid confusion with Rust `Result` type (#1768)
+ - Add support for default methods of traits (#1777)
+ - Gather definitions in namespaces, shortening names (#1780)
 
 Miscellaneous:
 - Reserve extraction folder for auto-generated files in Lean examples (#1754)

engine/backends/lean/lean_backend.ml

@@ -14,6 +14,7 @@ include
       include On.Quote
       include On.Dyn
       include On.Unsafe
+      include On.Trait_item_default
     end)
     (struct
       let backend = Diagnostics.Backend.FStar
@@ -45,7 +46,7 @@ module SubtypeToInputLanguage
          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) =
+         and type trait_item_default = Features.On.trait_item_default) =
 struct
   module FB = InputLanguage
 
@@ -120,7 +121,6 @@ module TransformToInputLanguage =
   |> Phases.Traits_specs
   |> Phases.Simplify_hoisting
   |> Phases.Newtype_as_refinement
-  |> Phases.Reject.Trait_item_default
   |> Phases.Bundle_cycles
   |> Phases.Reorder_fields
   |> Phases.Sort_items

examples/lean_chacha20/Makefile

@@ -6,5 +6,5 @@ default:
    lake build)
 
 clean:
-	-rm -f proofs/lean/extraction/lean_chacha20.lean
+	-rm -f proofs/lean/extraction/
 	-cd proofs/lean && lake clean

rust-engine/Cargo.toml

@@ -22,3 +22,4 @@ pretty = "0.12"
 derive_generic_visitor = "0.3.0"
 pastey = "0.1.0"
 camino = "1.1.11"
+capitalize = "0.3.4"