AU-COBRA / coq-rust-extraction

Coq plugin for extracting Rust code
MIT License
10 stars 3 forks source link

Consider being even more ridiculously leaky #20

Open workingjubilee opened 8 months ago

workingjubilee commented 8 months ago

Currently, you use bumpalo, which is a reasonable choice, but you can achieve much the same end result via Box::leak.

At the moment, there's no particular reason to do this aside from eliminating the dependency, and I did it by hand when reducing the binom.v extraction into a compiletest for rustc.

However, if you arrived at a point where you had a proof that this was the last remaining reference, you could coerce the reference to a pointer, then cast_mut and upgrade it to the original Box via Box::from_raw, so it can be deallocated. This is something a simple bump allocator would not meaningfully facilitate.