# Cache-at-ptr

We present `SEA-IR` built-ins and associated semantics for modelling borrow semantics in `Rust`.

## Intuition

In Safe Rust, a borrow entangles the borrowed pointer and owned pointer caches. This means that whatever is the value of the borrowed pointer cache at end of borrow becomes the cache value of the owned pointer.

In Unsafe Rust, a borrow does not entangle the borrowed pointer and owner pointer caches as-such. In fact the borrowed pointer may be mutated itself to point to a different memory allocation. Thus, this "borrow" is actually "stealing". To refresh the cache of the owned pointer, the only recourse is to "replace" the owned pointer cache with a read from memory.

Next, we present the formal semantics of `borrow`, `return`, `steal` and `replace` operations.

## Semantics

A borrow happens whenever a value is borrowed in Safe Rust.

sym(p1, q0 = borrow p0) == p1.addr, p1.val = p0.addr, nd() && q0.addr, q0.val, q0.ret = p0.addr, p0.val, p1.val

A return happens whenever a borrowed pointer `q` is dropped.

sym(return q == q.val = q.ret)

Note that in `SSA` form `q.val` will actually be the latest version of `q.val`.

A steal is a borrow in Unsafe Rust.

sym(p1, q0 = steal p0) == p1.addr, p1.val = p0.addr, nd() && q0.addr, q0.val = p0.addr, p0.val

A replace is return in Unsafe Rust.

sym(replace p, m0) == p.val = read(p.addr, m0) 

## Example

Let us use the above semantics to prove a property for a libstd function `stack_buffer_copy`. We want to prove that the buffer `buf` is `allocated` at line 17.

fn stack_buffer_copy<R: Read + ?Sized, W: Write + ?Sized>(
    reader: &mut R,
    writer: &mut W,
) -> Result<u64> {
    let mut buf = MaybeUninit::<[u8; DEFAULT_BUF_SIZE]>::uninit();
    // FIXME: #42788
    //
    //   - This creates a (mut) reference to a slice of
    //     _uninitialized_ integers, which is **undefined behavior**
    //
    //   - Only the standard library gets to soundly "ignore" this,
    //     based on its privileged knowledge of unstable rustc
    //     internals;
    unsafe {
        reader.initializer().initialize(buf.assume_init_mut());
    }

    let mut written = 0;
    loop {
        let len = match reader.read(unsafe { buf.assume_init_mut() }) {
            Ok(0) => return Ok(written),
            Ok(len) => len,
            Err(ref e) if e.kind() == ErrorKind::Interrupted => continue,
            Err(e) => return Err(e),
        };
        writer.write_all(unsafe { &buf.assume_init_ref()[..len] })?;
        written += len as u64;
    }
}

Let us convert the `Rust` program into `SEA-IR` form (till line 17). We assume a buffer of unit length to simplify reasoning. Each pointer has a field `val` to store typestate info (e.g. allocation).

fun stack_buffer_copy(reader, writer):
  // b.addr = sp0 && b.val = 1
  b, m0 = alloc buffer 
  // b1.addr, b1.val = b.addr, nd() && br1.addr, br1.val = b.addr, b.val
  b1, br1 = steal b, m0 
  // --- unsafe begins ---
  m1 = write(br1.addr, m0)  // reader.initialize(br1, m0)
  // --- unsafe ends ---
  // assume (b1.val == read(b1.addr, m1))
  replace b1, m1
  // b1.val = 1
  sassert is_alloc (b1)

### Generated formula

b1.val = 1 && b1.val = read(b1.addr, m1) &&  m1 = write(br1.addr, m0) && 
b1.addr, b1.val = b.addr, nd() && br1.addr, br1.val = b.addr, b.val &&
b.addr = sp0 && b.val = 1