nixpulvis - Achilles' Tent Notes #8

Achilles' Tent Notes #8 written by Nathan Lilienthal on October 13, 2019.

fn type returns from obliv if

Wrapped in new closure which calls an obliv if inside when called:

obliv if p { |a...| e1 } else { |a...| e2 }
|a...| { obliv if p { e1 } else { e2 }

panic! within obliv if
- Currently ruled out of Oxide (has abort instead, which cannot be rescued from)
- The Output for division of obliv types should handle division by zero explicitly:
```
impl<T> Div for obliv T {
   type Output = Option<T>;
   fn div(self, rhs: Self) -> Self::Output { ... }
}
if let Some(n) = obliv 5 / obliv 0 {
  // never hit
} else {
  // handle division by zero
}
```
- Otherwise we just state that x/0 == 0. This will cause user who care about the value 0/x being distinct to do their own checking
- obliv-c for example, just crashes when you divide by 0
Obliv compound types (i.e. obliv Option<T> or obliv (T, U)), what about Cell<T>
- The idea of an obliv enum in general is interesting (along with obliv match)
- obliv (T, U) oblivious tuple, not to be confused with a plain tuple of oblivious types, (obliv T, obliv U) is tricky because tuples are heterogeneous
- obliv [T; n]
- Oxide doesn’t have a notion of Cell, or interior mutability in general
obliv fn ideally shouldn’t be needed (need frz qualifier?)
- In obliv-c it exists to limit mutation from the outside, whereas we should be reasoning about the mutability of arguments in a closure
- static mut items (which are unsafe) allow security leaks if allowed in obliv contexts:
```
static mut X: u32 = 0;
// f is *not* obliv safe.
fn f() {
  unsafe {
      X = 2;
  }
}
```
2 stage borrow’s reserved is similar to freeze
- Currently &'a mut T could really be viewed as RefMut<'r, 'w, T> with explicit lifetimes for reading and writing.