[Rust] Prevent allocated block from outliving allocator

[btj]

[btj]

The current spec for Box::leak is unsound: it currently produces a regular points-to chunk, whose validity is unbounded in time, whereas in reality the memory provided by Box::leak is valid only as long as the allocator is alive.

The spec should instead be something like

        fn leak<'a>(b: Box<T, A>) -> &'a mut T;
        //@ req Box_in::<T, A>(?t, b, ?alloc_id, ?value);
        //@ ens points_to_at_lft(alloc_id.lft, result, value) &*& std::alloc::alloc_block_in(alloc_id, result as *u8, std::alloc::Layout::new_::<T>()) &*& result as *_ as usize != 0;
        //@ on_unwind_ens false;

where points_to_at_lft(k, p, v) asserts ownership of the place at p with value v, but only until the end of lifetime k. An allocator identifier alloc_id includes the allocator's lifetime alloc_id.lft.

We would need lemmas like the following:

lem open_points_to_at_lft<T>(p: *T);
    req [?f]points_to_at_lft(?k, p, ?v) &*& [?q]lifetime_token(k);
    ens [f](*p |-> v) &*& close_points_to_at_lft_token(f, k, p, q);

lem close_points_to_at_lft<T>(p: *T);
    req close_points_to_at_lft_token(?f, ?k, p, ?q) &*& [f](*p |-> ?v);
    ens [f]points_to_at_lft(k, p, v) &*& [q]lifetime_token(k);

as well as lemmas for converting between a points_to_at_lft chunk for a struct and chunks for the fields and a padding chunk.

[btj]

The current spec for lemma Box::separate_contents is unsound for the same reason.