Achilles' Tent Notes #8 written by Nathan Lilienthal on October 13, 2019.
- Achilles’ Tent Notes #8
- Achilles’ Tent Notes #9
- Achilles’ Tent Notes #10
- Achilles’ Tent Notes #11
- Achilles’ Tent Notes #12
- Achilles’ Tent Notes #13
fn
type returns fromobliv 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 }
- Wrapped in new closure which calls an
panic!
withinobliv 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 value0/x
being distinct to do their own checking - obliv-c for example, just crashes when you divide by 0
- Currently ruled out of Oxide (has
- Obliv compound types (i.e.
obliv Option<T>
orobliv (T, U)
), what aboutCell<T>
- The idea of an
obliv enum
in general is interesting (along withobliv 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 heterogeneousobliv [T; n]
- Oxide doesn’t have a notion of
Cell
, or interior mutability in general
- The idea of an
obliv fn
ideally shouldn’t be needed (needfrz
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 inobliv
contexts:static mut X: u32 = 0; // f is *not* obliv safe. fn f() { unsafe { X = 2; } }
- 2 stage borrow’s
reserved
is similar tofreeze