Types as Contracts

Yep, and I acknowledge it’s tough. Well, tough to implement in a way that’s coherent between validation and actual optimization. On the optimization side, the pointer field in a Vec<T> is already a Unique<T>; if loads through Unique pointers are given LLVM noalias metadata, I think that’s enough to let LLVM make the optimization in question. (Which AFAIK was part of the original motivation for Unique, given the comment about aliasing guarantees, but isn't currently implemented, as Unique isn't a lang item.) But it seems like validation would have to use a totally separate mechanism to indicate the range of addresses to lock, given that that depends on the separate len field.

Also, I guess there are weird semantic corner cases. Consider this code:

let vec: Vec<i32> = vec![1, 2, 3];
let mut foo: i32 = 1;
let out_of_range_index = vec.as_ptr().offset_to(&mut foo as *const i32).unwrap() as usize;
let read1 = *vec.get_unchecked(out_of_range_index); // this reads `foo`
foo = 2;
let read2 = *vec.get_unchecked(out_of_range_index); // ditto

As far as I can tell, under your model, this code is perfectly legal - at least if the Vec contents happen to be located before foo in memory, so that vec.get_unchecked(out_of_range_index) doesn't wrap around the address space. Even if the Vec contents were write locked, that wouldn't cause any conflict with accesses to a different memory region. But if LLVM optimized multiple accesses to the same index, it could coalesce read1 and read2 into one read, even though the value changed in between.

Then again, that isn't just an issue for Vec, but any kind of array, including fixed-length arrays, which I'd assume your proposal already covers. Yet it would be highly desirable for Rust's semantics to allow taking advantage of LLVM's existing noalias functionality. Perhaps that code would have aliasing assumptions disabled due to using unsafe? Or perhaps it should just be independently considered UB to index a slice out of bounds (even using get_unchecked), regardless of aliasing?