Is it possible to unchecked unwrap Option with safety?

help
1

Summary: Use lifetimes to differentiate variables and construct proof for different Option variable to provide safe uncheck unwrap interface. Is it possible? Is there any flaw? Could we fix that?

According to Lifetime(a) = lifetime(b) iff (a=b)?, in many circumstances, we can discriminate two variable with their lifetime. It occur to me that maybe we can use it to implement a sort of dependent type of the variable.
So I attempt to wrote these code:

/// solidify the lifetime.
pub struct FixRange<'a,T: 'a> (Invariant<&'a T>);
/// ensure that value don't change in lifetiem 'a
pub struct FixObj<'a,T: 'a> (&'a T, FixRange<'a, T>);

macro_rules! fix { ($x:ident, $f:ident) => (let reference = &$x; let $f = FixObj::new(&reference);) }

/// T should be an Option<U>
/// In the range of Fix<'a, T>, guarantee the T is not empty.
#[derive(Clone, Copy)]               
pub struct OptionNotNonProof<'a, T: 'a> (FixRange<'a, T>);

pub fn check<'a, U: 'a>(fx: FixObj<'a, Option<U>>) -> Option<OptionNotNonProof<'a, Option<U>>> {
    match fx.get() {
        Some(_) => Some(OptionNotNonProof(fx.get_range())),
        None => None,
    }
}
pub fn prechecked_unwrap<'a: 'b, 'b, U>(fx:  &'b FixObj<'a, Option<U>>, proof: OptionNotNonProof<'a, Option<U>>) -> &'b U {
    match fx.get() {
        Some(x) => x,
        None => unreachable!(),
    }
}

And for usage:

let a: Option<u8> = Some(42);
/// one liner to define fixobj.
fix!(a,fa);

let z = check(fa);
if let Some(proof) = z {
	println!("Got proof.");
	println!("proof size: {}", mem::size_of_val(&proof));
	// Do something...
	println!("unwrap with proof: {}", prechecked_unwrap(&fa,proof));
} else {
	println!("No proof.");
}

Now the most important question is: Are these code safe? Any opinion is appreciated.

My thought on that question is as follow:

Interface:
For user outside of this mod, only interface they could use to construct a proof object is:

pub fn check<'a, U: 'a>(fx: FixObj<'a, Option<U>>) -> Option<OptionNotNonProof<'a, Option<U>>>

Also, the fields of OptionNotNonProof is private, so users should not be able to construct value of this type on their own.

Lifetime:
FixObj could differentiate references with different lifetimes:

let a: u8 = 1;
let ra = &a;                                                
let mut fa = FixObj::new(&ra);                                  
let ra2 = &a;                               
let mut fa2 = FixObj::new(&ra2);

// both won't compile
// fa2 = fa;
// fa = fa2;

Also, the proof object can only not be used for another reference with different lifetime.

let a: Option<u8> = Some(42);
fix!(a,fa);
let b: Option<u8> = None;
fix!(b,fb);

if let Some(proof) = check(fa) {
        // won't compile
	// The proof is for fa only, and cannot be used for fb.
	// println!("unwrap with proof: {}", prechecked_unwrap(&fb,proof));
} else {}

However, two flaw might crack the code. As mentioned here, variables of 'static and variables binded together in one let can have same lifetime.
So we can create some counterexample:

/// However can be crack with group bind.
let (a,b) = (42 as u8, 1 as u8);
let (ra, rb) = (&a, &b);
let (mut fa, mut fb) = (FixObj::new(&ra),FixObj::new(&rb));
fa = fb;

Is there a way we can fix that?

Codes can be found here.

2

I highly doubt this has anything to do with them being assigned on the same line, but need more time to work it out.

4

Thanks for your reply.

According to this post, being assigned with same statement is one cause of same lifetime.

However according to this, some compiler compromise will also cause two variable share same lifetime.

Here is another piece of code which could compile but are not binded in same line.

let a = 42 as u8; let b = 1 as u8;
let ra = &a; let rb = &b;
let mut fa = FixObj::new(&ra); let mut fb = FixObj::new(&rb);
5

Yes, that makes more sense.

The way I see it is not that the compiler is assigning them the same lifetime. It's that the fa = fb line forces the fa and fb to have the same lifetime parameter, and the expression FixObj::new(&ra) (and the other one) basically "coerces" &ra to have this shared lifetime that borrows from both ra and rb. (although strictly speaking this is not a coercion, but rather assigning a value of a subtype to a supertype).

Shameless plug: I've been writing about this model of lifetimes in a blog series, and will soon be covering lifetime inference.

I believe you can change the macro and API to something safer which truly guarantees that every FixObj has a distinct lifetime. Hang on just a minute...

7

Okay. I was working on this for a bit until I realized I might be making things unnecessarily complicated.

The following might be all you need for a fix:

  • Make the constructor of FixObj unsafe.
  • Make the macro use an unsafe block to call it, since it seems to work (though I'm not sure what the proof of correctness is here... anybody got a guess?).
impl<'a,T: 'a> FixObj<'a, T> {
    /// If this method is ever called twice with FixRanges
    /// that share the same lifetime, behavior is undefined.
    ///
    /// See the `fix!` macro for a safe wrapper.
    pub fn new_unchecked(c: &'a &'a T) -> Self { FixObj(c, FixRange::new(c)) }
}

The way I was trying to solve it makes it easier to prove that the macro is sound:

  • Have the macro define a new value (of type ()) and borrow it. Use that lifetime to distinguish FixObjs.
  • Completely forget about the relationship between the borrow of the option and the lifetime of FixRange.

That strategy is employed here.

Also, @eaglgenes101 deleted his post, but it is correct. Surely you intend to use unsafe { unchecked_unreachable() } rather than unreachable!(), or else there's no point to this..

8