---
title: Achilles' Tent Notes #9
date: '2019-10-15'
collection: research
---

- [Achilles' Tent Notes #8](/research/2019-10-13-achilles-8)
- [**Achilles' Tent Notes #9**](/research/2019-10-15-achilles-9)
- [Achilles' Tent Notes #10](/research/2019-10-28-achilles-10)
- [Achilles' Tent Notes #11](/research/2019-11-11-achilles-11)
- [Achilles' Tent Notes #12](/research/2019-12-02-achilles-12)
- [Achilles' Tent Notes #13](/research/2019-12-13-achilles-13)

---

### Surface Obliv-Rust

Below are the first highlights for `obliv` additions to the surface Rust language.

- New type:
```rust
type Obliv<T>;
// or simply
type obliv τ
```
- New `obliv if` expression:
```rust
obliv if e1 { e2 } else { e3 }
```
```rust
fn add(x: obliv u32, y: obliv u32) -> obliv u32 {
    obliv if x == y {
        x * 2
    } else {
        x + y
    }
}
```
- New `obliv match` expression:
```rust
obliv match e { ... }
```
```rust
fn oadd1(i: obliv Option<u32>) -> obliv Option<u32> {
    obliv match i {
        Some(n) => Some(n + 1),
        None => None,
    }
}
```
- Either a new function declaration:
```rust
obliv fn foo(a: &u32, b: &mut u32) -> &mut u32
```
  Or, a new reference qualifier in signature:
```rust
fn bar(a: &u32, b: &frz u32) -> &frz u32
// `baz` is forbidden in obliv context, has &mut.
fn baz(a: &u32, b: &mut u32)
// `bat` also has an &mut making it forbidden in obliv context,
// however takes an &frz, what does this mean?
fn bat(a: &mut u32, b: &frz u32)
```

### Formal Obliv-Oxide

Together with changes to the underlying Oxide formalism. Please note that this
section is **incomplete** with respect to syntax, and possibly semantics.
Please read as notes.

1. Syntax
```
ω ::= uniq | frzn | shrd
```
We must be able to "freeze" references until we "thaw" them in an `always`
block. We can interpret `uniq` as unique **and** mutable, `frzn` as unique
**but not** mutable, and finally `shrd` as simply immutable.
```
obliv τ ::= obliv bool | obliv int | ...
             | obliv [τ; n]
             | obliv [obliv τ; n]
```
Oblivious base types are defined, I'm using `int` as a placeholder for more
underlying numeric (and other sized) types. As well as a composite `obliv []`
type. Also note that both
[PIR](https://en.wikipedia.org/wiki/Private_information_retrieval) and
[ORAM](https://en.wikipedia.org/wiki/Oblivious_RAM) structures fit these types
respectively.
```
e ::= ...
       | conceal(e)
       | reveal(e)
       | obliv if e1 { e2 } else { e3 }
       | always { e }
```
2. Typing Rules
##### <span style="background: lightgrey;">`conceal`</span> & <span style="background: lightgrey;">`reveal`</span> primitives:
```
           e: τ              e: obliv τ
-------------------      ------------
conceal(e): obliv τ      reveal(e): τ
```
##### <span style="background: lightgrey;">`obliv if`</span>:
```
        e1: obliv bool     e2, e3: τ
----------------------------------------
obliv if e1 { e2 } else { e3 } : obliv τ
```
And, returning functions (The case is the same for functions of no arguments):
```
       e1: obliv bool         e2, e3: fn(τ*) -> τ
-------------------------------------------------
obliv if e1 { e2 } else { e3 }: fn(τ*) -> obliv τ
```
However, I'm unsure still at this time if the next rule should result in type
`fn(&frz)` or `fn(&mut)`.
```
       e1: obliv bool         e2, e3: fn(mut τ*) -> τ
-----------------------------------------------------
obliv if e1 { e2 } else { e3 }: fn(frz τ*) -> obliv τ
```
Do we need the notion of a function with explicit `fn foo(mut x: u32, frz:
u32)`? Trait definition functions, for example, don't allow patterns in the
arguments.
##### <span style="background: lightgrey;">`always`</span>: TODO
3. Operational semantics
```
obliv if e1 { |a1,...,an| e2 } else { |a1,...,an| e3 } =>
|a1,...,an| { obliv if e1 { e2 } else { e3 } }
```
This is a somewhat straightforward reduction, if you ignore the details of
`&frz` and `&mut` for a moment:
```
obliv if e1 { |&a1,...,&an| e2 } else { |&a1,...,&an| e3 } =>
|&a1,...,&an| { obliv if e1 { e2 } else { e3 } }
```
4. Safety

### Math

- `obliv num / obliv num` should never panic
  - The `impl Div` for oblivious types should have a well defined division by 0 value. Users can choose a well behaved `n/d` for short syntax, and manually check for `if d == 0`
  - Otherwise, `checked_div` will be available which returns an `obliv Option`, forcing the user to handle the `n/0` case

### Open Questions
- What is an `obliv &`, if anything
- [`fiat-crypto`](https://github.com/mit-plv/fiat-crypto) Rust extraction
  - Still need to play with running the extraction more
  - Questions about what types to expose for the underlying algebraic structures
- Possibly use [λ-rust](https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf) for some parts of Rust that Oxide doesn't reason about, e.g. `unsafe`