From 5db9f2940329f959fd6d0d88d6861509204c2807 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Fri, 5 Dec 2025 17:06:49 +0100 Subject: [PATCH 1/6] fix: typo --- rust-engine/src/ast.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/rust-engine/src/ast.rs b/rust-engine/src/ast.rs index 40c9dc358..14a698cd3 100644 --- a/rust-engine/src/ast.rs +++ b/rust-engine/src/ast.rs @@ -1131,9 +1131,9 @@ pub struct GenericParam { /// Generic parameters and constraints (contained between `<>` in function declarations) #[derive_group_for_ast] pub struct Generics { - /// A vector of genreric parameters. + /// A vector of generic parameters. pub params: Vec, - /// A vector of genreric constraints. + /// A vector of generic constraints. pub constraints: Vec, } From 834b35a7c8fc25764ec322c82641c0b85f503731 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Fri, 5 Dec 2025 17:07:53 +0100 Subject: [PATCH 2/6] refactor(lean): rename function --- rust-engine/src/backends/lean.rs | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index c3329bd37..869cd2a1c 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -243,7 +243,7 @@ const _: () = { }; } - // Methods for handling arguments of variants (or struct constructor) + // Extra methods, specific to the LeanPrinter impl LeanPrinter { /// Prints arguments a variant or constructor of struct, using named or unamed arguments based /// on the `is_record` flag. Used for both expressions and patterns @@ -326,14 +326,11 @@ const _: () = { docs!["do", line!(), body].group() } - /// Produces a fresh name for a constraint on an associated type. It needs a fresh name to - /// be added as an extra field - fn fresh_constraint_name( - &self, - associated_type_name: &String, - constraint: &ImplIdent, - ) -> String { - format!("_constr_{}_{}", associated_type_name, constraint.name) + /// Produces a name for a constraint on an trait-level constraint, or an associated + /// type. The name is obtained by combining the type it applies to and the name of the + /// constraint (and should be unique) + fn constraint_name(&self, type_name: &String, constraint: &ImplIdent) -> String { + format!("_constr_{}_{}", type_name, constraint.name) } /// Turns an expression of type `RustM T` into one of type `T` (out of the monad), providing @@ -1018,7 +1015,7 @@ set_option linter.unusedVariables false .map(|constraint: &GenericConstraint| { match constraint { GenericConstraint::Type(tc_constraint) => docs![ - self.fresh_constraint_name(&self.render_last(name), tc_constraint), + self.constraint_name(&self.render_last(name), tc_constraint), " :", line!(), constraint @@ -1126,7 +1123,7 @@ set_option linter.unusedVariables false concat!(constraints.iter().map(|c| docs![ hardline!(), docs![ - self.fresh_constraint_name(&name, c), + self.constraint_name(&name, c), reflow!(" :"), line!(), &c.goal From 55059902a29cd05271a81cd62eea8105e3cc462d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Fri, 5 Dec 2025 17:09:44 +0100 Subject: [PATCH 3/6] fix(lean): make trait-level params explicit parameters of fields --- hax-lib/proof-libs/lean/Hax/Core/Convert.lean | 22 ++- .../lean/Hax/Core/Ops/Function.lean | 2 +- hax-lib/proof-libs/lean/Hax/Lib.lean | 4 +- rust-engine/src/backends/lean.rs | 174 +++++++++------- .../toolchain__lean-tests into-lean.snap | 185 ++++++++---------- tests/lean-tests/src/constants.rs | 33 +--- tests/lean-tests/src/traits.rs | 30 +-- 7 files changed, 202 insertions(+), 248 deletions(-) diff --git a/hax-lib/proof-libs/lean/Hax/Core/Convert.lean b/hax-lib/proof-libs/lean/Hax/Core/Convert.lean index 3e76fd19b..1826cc505 100644 --- a/hax-lib/proof-libs/lean/Hax/Core/Convert.lean +++ b/hax-lib/proof-libs/lean/Hax/Core/Convert.lean @@ -12,9 +12,13 @@ open Std.Do set_option mvcgen.warning false -/- Warning : this function has been specialized, it should be turned into a typeclass -/ -def Core.Convert.TryInto.try_into {α n} (a: Array α) : - RustM (Core.Result.Result (Vector α n) Core.Array.TryFromSliceError) := +namespace Core.Convert + +class TryInto (Self: Type) (T: Type) {E: Type} where + try_into (Self T) : Self → (RustM (Core.Result.Result T E)) + +instance {α : Type} {n : Nat} : TryInto (RustSlice α) (RustArray α n) (E := Core.Array.TryFromSliceError) where + try_into a := pure ( if h: a.size = n then Core.Result.Result.Ok (a.toVector.cast h) @@ -22,12 +26,18 @@ def Core.Convert.TryInto.try_into {α n} (a: Array α) : .Err Core.Array.TryFromSliceError.array.TryFromSliceError ) +#check fun {α : Type} {n: Nat} (a: RustSlice α) => TryInto.try_into (RustSlice α) (RustArray α n) a + +#check fun {α n} => (inferInstance : TryInto (RustSlice α) (RustArray α n)) + @[spec] -theorem Core.Convert.TryInto.try_into.spec {α n} (a: Array α) : +theorem TryInto.try_into.spec {α : Type} {n: Nat} (a: RustSlice α) : (h: a.size = n) → ⦃ ⌜ True ⌝ ⦄ - ( Core.Convert.TryInto.try_into a) + (TryInto.try_into (RustSlice α) (RustArray α n) (E := Core.Array.TryFromSliceError) a ) ⦃ ⇓ r => ⌜ r = .Ok (a.toVector.cast h) ⌝ ⦄ := by intro h - mvcgen [Core.Result.Impl.unwrap.spec, Core.Convert.TryInto.try_into] + mvcgen [TryInto.try_into] grind + +end Core.Convert diff --git a/hax-lib/proof-libs/lean/Hax/Core/Ops/Function.lean b/hax-lib/proof-libs/lean/Hax/Core/Ops/Function.lean index b3e56fd8a..e3139c696 100644 --- a/hax-lib/proof-libs/lean/Hax/Core/Ops/Function.lean +++ b/hax-lib/proof-libs/lean/Hax/Core/Ops/Function.lean @@ -16,7 +16,7 @@ class FnOnce (Self Args : Type) {Output: Type} where class Fn (Self Args : Type) {Output: Type} where [_constr_10219838627318688691 : (FnOnce Self Args (Output := Output))] - call : Self -> Args -> RustM Output + call (Self Args) : Self -> Args -> RustM Output instance {α β} : FnOnce (α → RustM β) α (Output := β) where Output := β diff --git a/hax-lib/proof-libs/lean/Hax/Lib.lean b/hax-lib/proof-libs/lean/Hax/Lib.lean index 789b710e0..184bd7dd5 100644 --- a/hax-lib/proof-libs/lean/Hax/Lib.lean +++ b/hax-lib/proof-libs/lean/Hax/Lib.lean @@ -421,7 +421,7 @@ section Cast /-- Hax-introduced explicit cast. It is partial (returns a `RustM`) -/ @[simp, spec] -def Core.Convert.From.from {α β} [Coe α (RustM β)] (x:α) : (RustM β) := x +def Core.Convert.From.from (β α) [Coe α (RustM β)] (x:α) : (RustM β) := x /-- Rust-supported casts on base types -/ class Cast (α β: Type) where @@ -883,7 +883,7 @@ end RustVectors -- Miscellaneous -def Core.Ops.Deref.Deref.deref {α Allocator} (v: Alloc.Vec.Vec α Allocator) +def Core.Ops.Deref.Deref.deref {α Allocator} (β : Type) (v: Alloc.Vec.Vec α Allocator) : RustM (Array α) := pure v diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 869cd2a1c..582283894 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -356,6 +356,90 @@ const _: () = { } } } + + /// Print trait items, adding trait-level params as extra arguments + fn trait_item_with_trait_params( + &self, + trait_generics: &Vec, + TraitItem { + meta: _, + kind, + generics: item_generics, + ident, + }: &TraitItem, + ) -> DocBuilder { + { + let name = self.render_last(ident); + let trait_generics = intersperse!( + trait_generics + .iter() + .map(|GenericParam { ident, .. }| ident), + softline!() + ) + .parens() + .group() + .append(line!()); + docs![match kind { + TraitItemKind::Fn(ty) => { + docs![ + name, + softline!(), + trait_generics, + item_generics, + ":", + line!(), + ty + ] + .group() + .nest(INDENT) + } + TraitItemKind::Type(constraints) => { + docs![ + name.clone(), + reflow!(" : Type"), + concat!(constraints.iter().map(|c| docs![ + hardline!(), + docs![ + self.constraint_name(&name, c), + reflow!(" :"), + line!(), + &c.goal + ] + .group() + .nest(INDENT) + .brackets() + ])) + ] + } + TraitItemKind::Default { params, body } => docs![ + docs![ + name, + softline!(), + trait_generics, + item_generics, + zip_right!(params, line!()).group(), + docs![": RustM ", body.ty].group(), + line!(), + ":= do", + ] + .group(), + line!(), + body, + ] + .group() + .nest(INDENT), + TraitItemKind::Resugared(_) => { + unreachable!("This backend has no resugaring for trait items") + } + }] + } + } + } + + impl ToDocument for (Vec, &TraitItem) { + fn to_document(&self, printer: &LeanPrinter) -> DocBuilder { + printer.trait_item_with_trait_params(&self.0, self.1) + } } impl PrettyAst for LeanPrinter { @@ -483,7 +567,7 @@ set_option linter.unusedVariables false args, generic_args, bounds_impls: _, - trait_: _, + trait_, } => { match (&args[..], &generic_args[..], head.kind()) { ([arg], [], ExprKind::GlobalId(LIFT)) => docs![reflow!("← "), arg].parens(), @@ -494,6 +578,9 @@ set_option linter.unusedVariables false // Fallback for any application docs![ head, + trait_ + .as_ref() + .map(|(impl_expr, _)| zip_left!(line!(), &impl_expr.goal.args)), zip_left!(line!(), generic_args).group(), zip_left!(line!(), args).group(), ] @@ -995,20 +1082,20 @@ set_option linter.unusedVariables false generics, items, } => { - // Type parameters are also parameters of the class, but constraints are fields of the class docs![ docs![ - docs![reflow!("class "), name], - (!generics.params.is_empty()).then_some(docs![ - line!(), - intersperse!(&generics.params, line!()).group() - ]), + reflow!("class "), + name, + // Trait-level type parameters are also parameters of the class (but + // constraints are fields of the class) + zip_left!(line!(), &generics.params), line!(), "where" ] .group(), - hardline!(), - (!generics.constraints.is_empty()).then_some(docs![zip_right!( + zip_left!( + hardline!(), + // Trait-level constraints are extra fields of the class generics .constraints .iter() @@ -1025,17 +1112,14 @@ set_option linter.unusedVariables false GenericConstraint::Lifetime(_) => unreachable_by_invariant!(Drop_references), GenericConstraint::Projection(_) => emit_error!(issue 1710, "Unsupported equality constraints on associated types"), } - }), - hardline!() - )]), - intersperse!( + })), + zip_left!( + hardline!(), items.iter().filter(|item| { // TODO: should be treated directly by name rendering, see : // https://github.com/cryspen/hax/issues/1646 - !(item.ident.is_precondition() || item.ident.is_postcondition()) - }), - hardline!() - ) + !(item.ident.is_precondition() || item.ident.is_postcondition()) + }).map(|item| docs![(generics.params.clone(), item)] )), ] .nest(INDENT) } @@ -1100,62 +1184,6 @@ set_option linter.unusedVariables false docs![meta, body] } - fn trait_item( - &self, - TraitItem { - meta: _, - kind, - generics, - ident, - }: &TraitItem, - ) -> DocBuilder { - let name = self.render_last(ident); - docs![match kind { - TraitItemKind::Fn(ty) => { - docs![name, softline!(), generics, ":", line!(), ty] - .group() - .nest(INDENT) - } - TraitItemKind::Type(constraints) => { - docs![ - name.clone(), - reflow!(" : Type"), - concat!(constraints.iter().map(|c| docs![ - hardline!(), - docs![ - self.constraint_name(&name, c), - reflow!(" :"), - line!(), - &c.goal - ] - .group() - .nest(INDENT) - .brackets() - ])) - ] - } - TraitItemKind::Default { params, body } => docs![ - docs![ - name, - softline!(), - generics, - zip_right!(params, line!()).group(), - docs![": RustM ", body.ty].group(), - line!(), - ":= do", - ] - .group(), - line!(), - body, - ] - .group() - .nest(INDENT), - TraitItemKind::Resugared(_) => { - unreachable!("This backend has no resugaring for trait items") - } - }] - } - fn impl_item( &self, ImplItem { diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap index ad80cd3ec..ad5b9309d 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap @@ -92,11 +92,18 @@ set_option mvcgen.warning false set_option linter.unusedVariables false class Lean_tests.Traits.Trait_level_args.T1 - (Self : Type) (A : Type) (B : Type) + (Self : Type) + (A : Type) + (B : Type) where - f1 (C : Type) (D : Type) : (Self -> RustM Rust_primitives.Hax.Tuple0) - f2 (C : Type) (D : Type) : (Self -> A -> RustM Rust_primitives.Hax.Tuple0) - f3 (C : Type) (D : Type) : + f1 (Self A B) + (C : Type) (D : Type) : + (Self -> RustM Rust_primitives.Hax.Tuple0) + f2 (Self A B) + (C : Type) (D : Type) : + (Self -> A -> RustM Rust_primitives.Hax.Tuple0) + f3 (Self A B) + (C : Type) (D : Type) : (Self -> A -> B -> RustM Rust_primitives.Hax.Tuple0) instance Lean_tests.Traits.Trait_level_args.Impl : @@ -110,31 +117,6 @@ instance Lean_tests.Traits.Trait_level_args.Impl : (pure Rust_primitives.Hax.Tuple0.mk) -/-- -error: Application type mismatch: The argument - x -has type - U -of sort `Type` but is expected to have type - Type -of sort `Type 1` in the application - T1.f1 C D x ---- -error: Application type mismatch: The argument - x -has type - U -of sort `Type` but is expected to have type - Type -of sort `Type 1` in the application - T1.f2 C D x ---- -error: failed to synthesize - T1 A ?m.19 C - -Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. --/ -#guard_msgs in def Lean_tests.Traits.Trait_level_args.test (A : Type) @@ -148,19 +130,19 @@ def Lean_tests.Traits.Trait_level_args.test (b : B) : RustM Rust_primitives.Hax.Tuple0 := do - let _ ← (Lean_tests.Traits.Trait_level_args.T1.f1 C D x); - let _ ← (Lean_tests.Traits.Trait_level_args.T1.f2 C D x a); - let _ ← (Lean_tests.Traits.Trait_level_args.T1.f3 C D x a b); + let _ ← (Lean_tests.Traits.Trait_level_args.T1.f1 U A B C D x); + let _ ← (Lean_tests.Traits.Trait_level_args.T1.f2 U A B C D x a); + let _ ← (Lean_tests.Traits.Trait_level_args.T1.f3 U A B C D x a b); (pure Rust_primitives.Hax.Tuple0.mk) class Lean_tests.Traits.Overlapping_methods.T1 (Self : Type) where - f : (Self -> RustM usize) + f (Self) : (Self -> RustM usize) class Lean_tests.Traits.Overlapping_methods.T2 (Self : Type) where - f : (Self -> RustM usize) + f (Self) : (Self -> RustM usize) class Lean_tests.Traits.Overlapping_methods.T3 (Self : Type) where - f : (Self -> RustM usize) + f (Self) : (Self -> RustM usize) instance Lean_tests.Traits.Overlapping_methods.Impl : Lean_tests.Traits.Overlapping_methods.T1 u32 @@ -182,28 +164,28 @@ def Lean_tests.Traits.Overlapping_methods.test : RustM usize := do let x : u32 := (9 : u32); - ((← ((← (Lean_tests.Traits.Overlapping_methods.T1.f x)) - +? (← (Lean_tests.Traits.Overlapping_methods.T2.f x)))) - +? (← (Lean_tests.Traits.Overlapping_methods.T3.f x))) + ((← ((← (Lean_tests.Traits.Overlapping_methods.T1.f u32 x)) + +? (← (Lean_tests.Traits.Overlapping_methods.T2.f u32 x)))) + +? (← (Lean_tests.Traits.Overlapping_methods.T3.f u32 x))) class Lean_tests.Traits.Inheritance.T1 (Self : Type) where - f1 : (Self -> RustM usize) + f1 (Self) : (Self -> RustM usize) class Lean_tests.Traits.Inheritance.T2 (Self : Type) where - f2 : (Self -> RustM usize) + f2 (Self) : (Self -> RustM usize) class Lean_tests.Traits.Inheritance.T3 (Self : Type) where [_constr_T3_i0 : (Lean_tests.Traits.Inheritance.T2 Self)] [_constr_T3_i1 : (Lean_tests.Traits.Inheritance.T1 Self)] - f3 : (Self -> RustM usize) + f3 (Self) : (Self -> RustM usize) class Lean_tests.Traits.Inheritance.Tp1 (Self : Type) where - f1 : (Self -> RustM usize) + f1 (Self) : (Self -> RustM usize) class Lean_tests.Traits.Inheritance.Tp2 (Self : Type) where [_constr_Tp2_i0 : (Lean_tests.Traits.Inheritance.Tp1 Self)] [_constr_Tp2_i1 : (Lean_tests.Traits.Inheritance.T3 Self)] - fp2 : (Self -> RustM usize) + fp2 (Self) : (Self -> RustM usize) structure Lean_tests.Traits.Inheritance.S where @@ -232,20 +214,25 @@ instance Lean_tests.Traits.Inheritance.Impl_4 : Lean_tests.Traits.Inheritance.Tp2 Lean_tests.Traits.Inheritance.S where fp2 (self : Lean_tests.Traits.Inheritance.S) := do - ((← ((← ((← (Lean_tests.Traits.Inheritance.Tp1.f1 self)) - +? (← (Lean_tests.Traits.Inheritance.T1.f1 self)))) - +? (← (Lean_tests.Traits.Inheritance.T2.f2 self)))) - +? (← (Lean_tests.Traits.Inheritance.T3.f3 self))) + ((← ((← ((← (Lean_tests.Traits.Inheritance.Tp1.f1 + Lean_tests.Traits.Inheritance.S self)) + +? (← (Lean_tests.Traits.Inheritance.T1.f1 + Lean_tests.Traits.Inheritance.S self)))) + +? (← (Lean_tests.Traits.Inheritance.T2.f2 + Lean_tests.Traits.Inheritance.S self)))) + +? (← (Lean_tests.Traits.Inheritance.T3.f3 + Lean_tests.Traits.Inheritance.S self))) def Lean_tests.Traits.Inheritance.test (_ : Rust_primitives.Hax.Tuple0) : RustM usize := do let s : Lean_tests.Traits.Inheritance.S := Lean_tests.Traits.Inheritance.S.mk; - ((← (Lean_tests.Traits.Inheritance.T3.f3 s)) +? (1 : usize)) + ((← (Lean_tests.Traits.Inheritance.T3.f3 Lean_tests.Traits.Inheritance.S s)) + +? (1 : usize)) class Lean_tests.Traits.Default.Easy (Self : Type) where - dft (self : Self) : RustM usize := do (pure (32 : usize)) + dft (Self) (self : Self) : RustM usize := do (pure (32 : usize)) instance Lean_tests.Traits.Default.Impl : Lean_tests.Traits.Default.Easy usize @@ -258,14 +245,16 @@ instance Lean_tests.Traits.Default.Impl_1 : class Lean_tests.Traits.Default.T1 (Self : Type) where - f1 : (Self -> RustM usize) - f2 (self : Self) : RustM usize := do (pure (1 : usize)) - f3 (A : Type) (self : Self) (x : A) : RustM usize := do (pure (1 : usize)) - f4 (A : Type) [(Lean_tests.Traits.Default.Easy A)] (self : Self) + f1 (Self) : (Self -> RustM usize) + f2 (Self) (self : Self) : RustM usize := do (pure (1 : usize)) + f3 (Self) (A : Type) (self : Self) (x : A) : RustM usize := do + (pure (1 : usize)) + f4 (Self) + (A : Type) [(Lean_tests.Traits.Default.Easy A)] (self : Self) (x : A) : RustM usize := do - ((← (Lean_tests.Traits.Default.Easy.dft x)) +? (1 : usize)) + ((← (Lean_tests.Traits.Default.Easy.dft A x)) +? (1 : usize)) structure Lean_tests.Traits.Default.S (A : Type) where _0 : usize @@ -298,15 +287,15 @@ instance Lean_tests.Traits.Default.Impl_4 : (pure (0 : usize)) class Lean_tests.Traits.Bounds.T1 (Self : Type) where - f1 : (Self -> RustM usize) + f1 (Self) : (Self -> RustM usize) class Lean_tests.Traits.Bounds.T2 (Self : Type) where - f2 : (Self -> RustM usize) + f2 (Self) : (Self -> RustM usize) class Lean_tests.Traits.Bounds.Test (Self : Type) (T : Type) where [_constr_Test_i0 : (Lean_tests.Traits.Bounds.T2 Self)] [_constr_Test_i1 : (Lean_tests.Traits.Bounds.T1 T)] - f_test : (Self -> T -> RustM usize) + f_test (Self T) : (Self -> T -> RustM usize) structure Lean_tests.Traits.Bounds.S1 where @@ -332,8 +321,9 @@ instance Lean_tests.Traits.Bounds.Impl_2 : f_test (self : Lean_tests.Traits.Bounds.S2) (x : Lean_tests.Traits.Bounds.S1) := do - ((← ((← (Lean_tests.Traits.Bounds.T1.f1 x)) - +? (← (Lean_tests.Traits.Bounds.T2.f2 self)))) + ((← ((← (Lean_tests.Traits.Bounds.T1.f1 Lean_tests.Traits.Bounds.S1 x)) + +? (← (Lean_tests.Traits.Bounds.T2.f2 + Lean_tests.Traits.Bounds.S2 self)))) +? (1 : usize)) def Lean_tests.Traits.Bounds.test @@ -341,12 +331,14 @@ def Lean_tests.Traits.Bounds.test (x2 : Lean_tests.Traits.Bounds.S2) : RustM usize := do - ((← (Lean_tests.Traits.Bounds.Test.f_test x2 x1)) - +? (← (Lean_tests.Traits.Bounds.T1.f1 x1))) + ((← (Lean_tests.Traits.Bounds.Test.f_test + Lean_tests.Traits.Bounds.S2 + Lean_tests.Traits.Bounds.S1 x2 x1)) + +? (← (Lean_tests.Traits.Bounds.T1.f1 Lean_tests.Traits.Bounds.S1 x1))) class Lean_tests.Traits.Basic.T1 (Self : Type) where - f1 : (Self -> RustM usize) - f2 : (Self -> Self -> RustM usize) + f1 (Self) : (Self -> RustM usize) + f2 (Self) : (Self -> Self -> RustM usize) structure Lean_tests.Traits.Basic.S where @@ -364,15 +356,13 @@ def Lean_tests.Traits.Basic.f (T : Type) [(Lean_tests.Traits.Basic.T1 T)] (x : T) : RustM usize := do - ((← (Lean_tests.Traits.Basic.T1.f1 x)) - +? (← (Lean_tests.Traits.Basic.T1.f2 x x))) + ((← (Lean_tests.Traits.Basic.T1.f1 T x)) + +? (← (Lean_tests.Traits.Basic.T1.f2 T x x))) class Lean_tests.Traits.Associated_types.Foo (Self : Type) (T : Type) where - class Lean_tests.Traits.Associated_types.Bar (Self : Type) where - structure Lean_tests.Traits.Associated_types.S where @@ -388,14 +378,15 @@ instance Lean_tests.Traits.Associated_types.Impl_3 (A : Type) : class Lean_tests.Traits.Associated_types.T1 (Self : Type) where T : Type - f : (Self -> T -> RustM T) + f (Self) : (Self -> T -> RustM T) class Lean_tests.Traits.Associated_types.T3 (Self : Type) where T : Type [_constr_T_i0 : (Lean_tests.Traits.Associated_types.Bar T)] Tp : Type [_constr_Tp_i0 : (Lean_tests.Traits.Associated_types.Foo Tp T)] - f (A : Type) [(Lean_tests.Traits.Associated_types.Bar A)] : + f (Self) + (A : Type) [(Lean_tests.Traits.Associated_types.Bar A)] : (Self -> T -> Tp -> RustM usize) instance Lean_tests.Traits.Associated_types.Impl : @@ -408,7 +399,7 @@ instance Lean_tests.Traits.Associated_types.Impl : class Lean_tests.Traits.Associated_types.T2 (Self : Type) where T : Type [_constr_T_i0 : (Lean_tests.Traits.Associated_types.T1 T)] - f : (Self -> T -> RustM usize) + f (Self) : (Self -> T -> RustM usize) instance Lean_tests.Traits.Associated_types.Impl_1 : Lean_tests.Traits.Associated_types.T2 Lean_tests.Traits.Associated_types.S @@ -692,6 +683,8 @@ def Lean_tests.Loops.Errors.loop4 (← (Rust_primitives.Hax.Folds.fold_range_return (0 : u32) (← (Core.Ops.Function.Fn.call + (Rust_primitives.Hax.Tuple0 -> RustM u32) + (Rust_primitives.Hax.Tuple1 Rust_primitives.Hax.Tuple0) f (Rust_primitives.Hax.Tuple1.mk Rust_primitives.Hax.Tuple0.mk))) (fun e _ => (do (pure true) : RustM Bool)) @@ -805,9 +798,10 @@ def Lean_tests.Constants.Const_parameters.test -- Trait definition class Lean_tests.Constants.Const_parameters.T - (Self : Type) (N_TRAIT : usize) + (Self : Type) + (N_TRAIT : usize) where - f (N_FIELD : usize) : (Self -> RustM usize) + f (Self N_TRAIT) (N_FIELD : usize) : (Self -> RustM usize) -- Struct definition structure Lean_tests.Constants.Const_parameters.S (N : usize) where @@ -824,35 +818,6 @@ instance Lean_tests.Constants.Const_parameters.Impl (N_TRAIT : usize) : (N_TRAIT -? N_FIELD) -/-- -error: Application type mismatch: The argument - s -has type - S 10 -but is expected to have type - usize -in the application - T.f 1 s ---- -error: Application type mismatch: The argument - x -has type - A -but is expected to have type - usize -in the application - T.f 11 x ---- -error: Application type mismatch: The argument - x -has type - A -but is expected to have type - usize -in the application - T.f 4 x --/ -#guard_msgs in def Lean_tests.Constants.Const_parameters.test2 (N2 : usize) (A : Type) [(Lean_tests.Constants.Const_parameters.T A (N2))] (x @@ -863,11 +828,15 @@ def Lean_tests.Constants.Const_parameters.test2 let s : (Lean_tests.Constants.Const_parameters.S ((10 : usize))) := (Lean_tests.Constants.Const_parameters.S.mk (9 : u32)); let _ ← - ((← (Lean_tests.Constants.Const_parameters.T.f ((1 : usize)) s)) - +? (← (Lean_tests.Constants.Const_parameters.T.f ((11 : usize)) x))); + ((← (Lean_tests.Constants.Const_parameters.T.f + (Lean_tests.Constants.Const_parameters.S ((10 : usize))) + ((10 : usize)) ((1 : usize)) s)) + +? (← (Lean_tests.Constants.Const_parameters.T.f + A + (N2) ((11 : usize)) x))); let s : (Lean_tests.Constants.Const_parameters.S ((3 : usize))) := (Lean_tests.Constants.Const_parameters.S.mk (9 : u32)); - (Lean_tests.Constants.Const_parameters.T.f ((4 : usize)) x) + (Lean_tests.Constants.Const_parameters.T.f A (N2) ((4 : usize)) x) def Lean_tests.Constants.C1 : u32 := RustM.of_isOk (do (pure (5678 : u32))) (by rfl) @@ -923,9 +892,15 @@ def Lean_tests.closure (_ : Rust_primitives.Hax.Tuple0) : RustM i32 := do let f2 : (i32 -> i32 -> RustM i32) := (fun y z => (do ((← (y +? x)) +? z) : RustM i32)); let res1 : i32 ← - (Core.Ops.Function.Fn.call f1 (Rust_primitives.Hax.Tuple1.mk (1 : i32))); + (Core.Ops.Function.Fn.call + (i32 -> RustM i32) + (Rust_primitives.Hax.Tuple1 i32) + f1 + (Rust_primitives.Hax.Tuple1.mk (1 : i32))); let res2 : i32 ← (Core.Ops.Function.Fn.call + (i32 -> i32 -> RustM i32) + (Rust_primitives.Hax.Tuple2 i32 i32) f2 (Rust_primitives.Hax.Tuple2.mk (2 : i32) (3 : i32))); (res1 +? res2) diff --git a/tests/lean-tests/src/constants.rs b/tests/lean-tests/src/constants.rs index 48afed0c4..024aaf7c3 100644 --- a/tests/lean-tests/src/constants.rs +++ b/tests/lean-tests/src/constants.rs @@ -46,38 +46,7 @@ mod const_parameters { } } - #[hax_lib::lean::before( - " -/-- -error: Application type mismatch: The argument - s -has type - S 10 -but is expected to have type - usize -in the application - T.f 1 s ---- -error: Application type mismatch: The argument - x -has type - A -but is expected to have type - usize -in the application - T.f 11 x ---- -error: Application type mismatch: The argument - x -has type - A -but is expected to have type - usize -in the application - T.f 4 x --/ -#guard_msgs in" - )] + #[hax_lib::lean::before("")] fn test2>(x: A) -> usize { let s = S::(9); let _ = s.f::<1>() + x.f::<{ 1 + N1 }>(); diff --git a/tests/lean-tests/src/traits.rs b/tests/lean-tests/src/traits.rs index 7a43caa80..588e757fa 100644 --- a/tests/lean-tests/src/traits.rs +++ b/tests/lean-tests/src/traits.rs @@ -272,35 +272,7 @@ mod trait_level_args { fn f3(&self, x: &u32, y: &u64) {} } - #[hax_lib::lean::before( - " -/-- -error: Application type mismatch: The argument - x -has type - U -of sort `Type` but is expected to have type - Type -of sort `Type 1` in the application - T1.f1 C D x ---- -error: Application type mismatch: The argument - x -has type - U -of sort `Type` but is expected to have type - Type -of sort `Type 1` in the application - T1.f2 C D x ---- -error: failed to synthesize - T1 A ?m.19 C - -Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. --/ -#guard_msgs in" - )] - + #[hax_lib::lean::before("")] fn test>(x: U, a: &A, b: &B) -> () { x.f1::(); x.f2::(a); From 5a8ab7735aa969d435564840cd096aa180bcec0b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 8 Dec 2025 14:42:54 +0100 Subject: [PATCH 4/6] chore: Changelog --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index dc4d8cbff..0d2c492cf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -37,6 +37,8 @@ Changes to the Lean backend: - Add support for binding subpatterns in match constructs (#1790) - Add error when using patterns in function parameters (#1792) - Add support for constant parameters to functions and traits (#1797) + - Make trait-level arguments explicit for all trait functions, adding them as + extra parameters (#1803) Miscellaneous: - Reserve extraction folder for auto-generated files in Lean examples (#1754) From 59056213d77dd83ee88be3b8cba0c11ed7f13f04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 8 Dec 2025 17:11:34 +0100 Subject: [PATCH 5/6] test: update snapshot --- ...toolchain__lean-core-models into-lean.snap | 24 +++++++++++++------ 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/test-harness/src/snapshots/toolchain__lean-core-models into-lean.snap b/test-harness/src/snapshots/toolchain__lean-core-models into-lean.snap index 0767dcd26..f54990851 100644 --- a/test-harness/src/snapshots/toolchain__lean-core-models into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-core-models into-lean.snap @@ -107,16 +107,19 @@ def Lean_core_models.Result.tests Lean_core_models.Result.E1 u32 (u32 -> RustM (Core.Result.Result u32 Lean_core_models.Result.E1)) - (← (Core.Clone.Clone.clone v1)) + (← (Core.Clone.Clone.clone + (Core.Result.Result u32 Lean_core_models.Result.E1) v1)) (fun x => (do (pure (Core.Result.Result.Ok (← (x +? (1 : u32))))) : RustM (Core.Result.Result u32 Lean_core_models.Result.E1)))); let v12 : u32 ← (Core.Result.Impl.unwrap u32 u32 - (← (Core.Clone.Clone.clone (Core.Result.Result.Ok (0 : u32))))); + (← (Core.Clone.Clone.clone + (Core.Result.Result u32 u32) (Core.Result.Result.Ok (0 : u32))))); let v13 : u32 ← (Core.Result.Impl.expect u32 u32 - (← (Core.Clone.Clone.clone (Core.Result.Result.Ok (0 : u32)))) + (← (Core.Clone.Clone.clone + (Core.Result.Result u32 u32) (Core.Result.Result.Ok (0 : u32)))) "Should be Ok"); match (← (Core.Result.Impl.map @@ -156,12 +159,12 @@ def Lean_core_models.Option.test let o2 : (Core.Option.Option i32) := Core.Option.Option.None; let o3 : Bool ← (Core.Option.Impl.is_some_and i32 (i32 -> RustM Bool) - (← (Core.Clone.Clone.clone o1)) + (← (Core.Clone.Clone.clone (Core.Option.Option i32) o1)) (fun x => (do (Rust_primitives.Hax.Machine_int.eq x (0 : i32)) : RustM Bool))); let o3 : Bool ← (Core.Option.Impl.is_none_or i32 (i32 -> RustM Bool) - (← (Core.Clone.Clone.clone o1)) + (← (Core.Clone.Clone.clone (Core.Option.Option i32) o1)) (fun x => (do (Rust_primitives.Hax.Machine_int.eq x (0 : i32)) : RustM Bool))); let o4 : i32 ← @@ -245,7 +248,8 @@ def Lean_core_models.Default.Structs.test (_ : Rust_primitives.Hax.Tuple0) : RustM Lean_core_models.Default.Structs.S := do - (Core.Default.Default.default Rust_primitives.Hax.Tuple0.mk) + (Core.Default.Default.default + Lean_core_models.Default.Structs.S Rust_primitives.Hax.Tuple0.mk) inductive Lean_core_models.Default.Enums.E (T : Type) : Type | C1 : u32 -> Lean_core_models.Default.Enums.E (T : Type) @@ -258,7 +262,7 @@ instance Lean_core_models.Default.Enums.Impl where default (_ : Rust_primitives.Hax.Tuple0) := do (pure (Lean_core_models.Default.Enums.E.C2 - (← (Core.Default.Default.default Rust_primitives.Hax.Tuple0.mk)))) + (← (Core.Default.Default.default T Rust_primitives.Hax.Tuple0.mk)))) def Lean_core_models.Function.test (_ : Rust_primitives.Hax.Tuple0) @@ -269,12 +273,18 @@ def Lean_core_models.Function.test let f_2_tuple : ((Rust_primitives.Hax.Tuple2 u32 u32) -> RustM u32) := (fun ⟨x, y⟩ => (do (x +? y) : RustM u32)); ((← ((← (Core.Ops.Function.Fn.call + (u32 -> RustM u32) + (Rust_primitives.Hax.Tuple1 u32) f_1 (Rust_primitives.Hax.Tuple1.mk (0 : u32)))) +? (← (Core.Ops.Function.Fn.call + (u32 -> u32 -> RustM u32) + (Rust_primitives.Hax.Tuple2 u32 u32) f_2 (Rust_primitives.Hax.Tuple2.mk (1 : u32) (2 : u32)))))) +? (← (Core.Ops.Function.Fn.call + ((Rust_primitives.Hax.Tuple2 u32 u32) -> RustM u32) + (Rust_primitives.Hax.Tuple1 (Rust_primitives.Hax.Tuple2 u32 u32)) f_2_tuple (Rust_primitives.Hax.Tuple1.mk (Rust_primitives.Hax.Tuple2.mk (1 : u32) (2 : u32))))))''' From 8960e7da303c050617b8a5541fa817a3a81919e6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Blaudeau?= Date: Mon, 8 Dec 2025 17:20:18 +0100 Subject: [PATCH 6/6] refactor: clippy --- rust-engine/src/backends/lean.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 582283894..2b2b55774 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -360,7 +360,7 @@ const _: () = { /// Print trait items, adding trait-level params as extra arguments fn trait_item_with_trait_params( &self, - trait_generics: &Vec, + trait_generics: &[GenericParam], TraitItem { meta: _, kind,