Support thread locals

[Nadrieril]

This code:

thread_local!(static FOO: u32 = 0);
fn main() {}

Support for this should first be added in hax (https://github.com/cryspen/hax/issues/1311), then should be translated in Charon to a new kind of Global, just like statics and consts (with GlobalKind::ThreadLocal).

[Nadrieril]

thread_local!(static FOO: u32 = 42);

actually expands to

const FOO: ::std::thread::LocalKey<u32> =
    {
        #[inline]
        fn __rust_std_internal_init_fn() -> u32 { 42 }
        unsafe {
            ::std::thread::LocalKey::new(const {
                        if ::std::mem::needs_drop::<u32>() {
                            |__rust_std_internal_init|
                                {
                                    #[thread_local]
                                    static __RUST_STD_INTERNAL_VAL:
                                        ::std::thread::local_impl::LazyStorage<u32, ()> =
                                        ::std::thread::local_impl::LazyStorage::new();
                                    __RUST_STD_INTERNAL_VAL.get_or_init(__rust_std_internal_init,
                                        __rust_std_internal_init_fn)
                                }
                        } else {
                            |__rust_std_internal_init|
                                {
                                    #[thread_local]
                                    static __RUST_STD_INTERNAL_VAL:
                                        ::std::thread::local_impl::LazyStorage<u32, !> =
                                        ::std::thread::local_impl::LazyStorage::new();
                                    __RUST_STD_INTERNAL_VAL.get_or_init(__rust_std_internal_init,
                                        __rust_std_internal_init_fn)
                                }
                        }
                    })
        }
    };

In other words the initializer is put in a function, and that function is put in a special static, and that static is used in a callback to build the final const.

The question then is how much of this is makes sense to hide. Reading the docs here it looks like the complexity is in part for performance so maybe it makes sense to hide some of it? I think I'll wait for a user who has a use for this.