Update hax

charon/tests/ui/closures.out

@@ -729,7 +729,7 @@ where
     let @2: &'_ (T); // anonymous local
 
     @2 := &*((*(state@1)).0)
-    @0 := {test_crate::{test_crate::Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure<'_, T>} {move (@2)}
+    @0 := {test_crate::{test_crate::Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure<'_, T>[@TraitClause0, @TraitClause1]} {move (@2)}
     drop @2
     return
 }
@@ -744,7 +744,7 @@ where
     let @2: &'_ (T); // anonymous local
 
     @2 := &*((*(state@1)).0)
-    @0 := {test_crate::{test_crate::Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure<'_, T>} {move (@2)}
+    @0 := {test_crate::{test_crate::Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure<'_, T>[@TraitClause0, @TraitClause1]} {move (@2)}
     drop @2
     return
 }
@@ -768,7 +768,7 @@ where
     let @11: (); // anonymous local
 
     @3 := &*(*(x@1))
-    clo@2 := {test_crate::{test_crate::Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure<'_, T>} {move (@3)}
+    clo@2 := {test_crate::{test_crate::Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure<'_, T>[@TraitClause0, @TraitClause1]} {move (@3)}
     drop @3
     @fake_read(clo@2)
     @8 := &clo@2

charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out

@@ -0,0 +1,50 @@
+# Final LLBC before serialization:
+
+#[lang_item("sized")]
+pub trait core::marker::Sized<Self>
+
+pub trait test_crate::PrimeField<Self, Self_Repr>
+{
+    parent_clause0 : [@TraitClause0]: core::marker::Sized<Self_Repr>
+}
+
+pub struct test_crate::SqrtTables<F>
+  where
+      [@TraitClause0]: core::marker::Sized<F>,
+ =
+{
+  F,
+}
+
+fn test_crate::{test_crate::SqrtTables<F>[@TraitClause0]}::sqrt_common::closure<'_0, F, Clause1_Repr>(@1: &'_0 (()), @2: ())
+where
+    [@TraitClause0]: core::marker::Sized<F>,
+    [@TraitClause1]: test_crate::PrimeField<F, Clause1_Repr>,
+{
+    let @0: (); // return
+    let state@1: &'_0 (()); // arg #1
+    let _x@2: (); // arg #2
+
+    @0 := ()
+    @0 := ()
+    return
+}
+
+pub fn test_crate::{test_crate::SqrtTables<F>[@TraitClause0]}::sqrt_common<F, Clause1_Repr>()
+where
+    [@TraitClause0]: core::marker::Sized<F>,
+    [@TraitClause1]: test_crate::PrimeField<F, Clause1_Repr>,
+{
+    let @0: (); // return
+    let _closure@1: fn(()); // local
+
+    _closure@1 := {test_crate::{test_crate::SqrtTables<F>[@TraitClause0]}::sqrt_common::closure<F, Clause1_Repr>[@TraitClause0, @TraitClause1]} {}
+    @fake_read(_closure@1)
+    @0 := ()
+    drop _closure@1
+    @0 := ()
+    return
+}
+
+
+

charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.rs

@@ -0,0 +1,16 @@
+//@ charon-args=--remove-associated-types=*
+//! Regression test for issue https://github.com/AeneasVerif/charon/issues/627
+pub trait PrimeField {
+    type Repr;
+}
+
+pub struct SqrtTables<F>(F);
+
+impl<F> SqrtTables<F> {
+    pub fn sqrt_common()
+    where
+        F: PrimeField,
+    {
+        let _closure = |_x: ()| ();
+    }
+}

charon/tests/ui/simple/closure-inside-impl.out

@@ -0,0 +1,45 @@
+# Final LLBC before serialization:
+
+#[lang_item("sized")]
+pub trait core::marker::Sized<Self>
+
+pub struct test_crate::Foo<F>
+  where
+      [@TraitClause0]: core::marker::Sized<F>,
+ =
+{
+  F,
+}
+
+fn test_crate::{test_crate::Foo<F>[@TraitClause0]}::method::closure<'_0, F, T>(@1: &'_0 (()), @2: ())
+where
+    [@TraitClause0]: core::marker::Sized<F>,
+    [@TraitClause1]: core::marker::Sized<T>,
+{
+    let @0: (); // return
+    let state@1: &'_0 (()); // arg #1
+    let _x@2: (); // arg #2
+
+    @0 := ()
+    @0 := ()
+    return
+}
+
+pub fn test_crate::{test_crate::Foo<F>[@TraitClause0]}::method<F, T>()
+where
+    [@TraitClause0]: core::marker::Sized<F>,
+    [@TraitClause1]: core::marker::Sized<T>,
+{
+    let @0: (); // return
+    let _closure@1: fn(()); // local
+
+    _closure@1 := {test_crate::{test_crate::Foo<F>[@TraitClause0]}::method::closure<F, T>[@TraitClause0, @TraitClause1]} {}
+    @fake_read(_closure@1)
+    @0 := ()
+    drop _closure@1
+    @0 := ()
+    return
+}
+
+
+

charon/tests/ui/simple/closure-inside-impl.rs

@@ -0,0 +1,7 @@
+pub struct Foo<F>(F);
+
+impl<F> Foo<F> {
+    pub fn method<T>() {
+        let _closure = |_x: ()| ();
+    }
+}