Equality of ZST values

language design
3

Yes I think answering that question would answer my question, or would even be stronger than my question (because it'd be saying all ZST representations are equal): is this function sound?

pub fn value<T>() -> T {
   if T::IS_ZST {
      unsafe { std::mem::transmute(()) }
   else {
      panic!("not a ZST")
   }
}

The problem is arising when attempting formal verification of std's implementation of Vec, and would require some background into techniques that exist today for that. Basically, it comes down to: if I successfully push a value into a vector, and then pop that value from the same vector, is it guaranteed to be the same value? I want to think that any sane specification of vec would ensure that, but it would not be ensured if there is not a unique value for a ZST.

PS: I'm using "value" in the exact same sense as that used in the UCGs or MiniRust

2 Likes