A very nice and well-structured post, as always. Small nit: You’re a word in “Not quite how to think about that yet”.
The ‘language levels’ description seems to be very relevant to my electrolysis project, which is all about reasoning about safe code while replacing unsafe code with (hopefully) observationally equivalent code.
The only unsafe parts I encountered when verifying
[T]::len/index. I’d be curious at what level of the hierarchy you would place those.
[T] is, of course, already special in itself, but replacing it with a trait containing only
index_mut should enable safe Rust to provide observationally equivalent impls of it. Because that trait would basically describe any type of sequential list, I’ve axiomatized it as such.
mem::swap is probably more interesting because it feels like we could just make it a trait fn and auto-implement it for any safe type, which would work except for anything containing
&mut. It would probably be easiest to declare it an intrinsic just like most other fns in
mem. Because I don’t have to worry about affine types on the theorem prover side (and currently assume type parameters not to be instantiated by anything containing
&mut), I can have a straightforward implementation.
By now, I’ve moved up to Rust1, completely axiomatizing Vec - again, as a simple inductive list. Which makes me curious about your claim about simulating
Vec just via
Box. By using the latter to create a singly-linked list type, and given the abstracted
[T] trait I’ve described above, shouldn’t contiguous and non-contiguous lists be observationally equal to safe Rust (except for pointer comparisons, which I assume would break many other supposed equalities)?
Moving up to Rust2 would be as easy as assuming
Rc<T> = Arc<T> = T for me, which, again assuming
T does not contain any
&mut, should be a safe axiomatization. There are of course a few fns revealing information about reference counts that I couldn’t implement, but the same would be true for any hypothetical safe Rust implementation.
Rust3 (non-atomic mutation) is probably right out of the window for me because the no-aliasing
&mut guarantees are the whole premise of my project. Rust4 (asynchronous threading) on the other hand shouldn’t be a problem for me exactly because of that premise. And even if I weaken the premise at some point (by, say, optionally introducing a heap managed by separation logic), I will certainly not touch Rust5 (communication between threads and processes) any time soon because that is one of the hardest problems known to formal verification.