---
title: Achilles' Tent Notes #10
date: '2019-10-28'
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)

---

### Typing Notes

- Oxide doesn't have traits, or associated types
  - Proper syntax for oblivious array types: `obliv [τ; N]`, cases enumerated
    below:
      > **Details:**
      > - `obliv [obliv τ; N]⋮Index<obliv usize>`
      >   An oblivious array with oblivious data and oblivious access is an ORAM
      > - `obliv [obliv τ; N]⋮Index<usize>`
      >   An oblivious array with oblivious data and plain access
      > - `obliv [τ; N]⋮Index<obliv usize>`
      >   An oblivious array with plain data and oblivious access is comparable
      >   to a PIR, as it _could_ simply reveal the whole array
      > - `obliv [τ; N]⋮Index<usize>`
      >   An oblivious array with plain data and plain access only adds a secure
      >   mapping of indices to logical memory addresses. Logical to physical
      >   mappings are still present in the face of compiled Rust
      > - `[obliv τ; N]⋮Index<usize>` is just a normal ol' array of `obliv τ`
      >   types
      > - `[τ; N] ⋮Index<obliv usize>` is not implemented, and should be a type
      >   error

- `obliv ()`, `obliv (T)`, `obliv (T, U)`, and so on...
    - `obliv (T)` should not be equivalent to `obliv T`
    - `obliv (T, U) = (obliv T, obliv U)`, simply structural
    - Rust's `struct` ($$S::\langle\barρ,\barτ\rangle$$) are like tuples, so
      they should be consistent
- `obliv obliv τ`
  - Supports "MPC in the head" nested protocols
  - Might require careful consideration when writing typing rules with
    promotions
- `conceal(τ)` and `reveal(τ)` where `τ: σ → ρ`
  - Initial thought is that it doesn't make sense to allow this, because
    function bodies must be public information in general, more on this below
- Oxide doesn't currently have `enum` or `match`
    - `match` should be able to be represented as if, with an understanding of
      some patterns
    - Enums are "tagged", sum types
    - We could start small and only allow matching for enums, avoiding the
      broader class of "patterns"

### Redex Model

- Started a redex model `(define-language obliv)`
  - Thinking it should be `(define-union-language ...)`
- Example typing judgment:
```racket
[(types Γ e_1 (obliv bool))
 (types Γ e_2 (obliv t))
 (types Γ e_3 (obliv t))
 -------------------------------------------- obliv-if
 (types Γ (obliv-if e_1 e_2 e_3) (obliv t))])
```
- Example reduction rule:
```racket
(--> (in-hole E (obliv-if v_1 (λ (x : t) e_2)
                                (λ (x : t) e_3)))
       (in-hole E (λ (x : t) (obliv-if v_1 e_2 e_3)))
       "obliv-if-λ")
```

#### Public Promotion & Wire Types

- How can I write promotion rules like the following:
```racket
[(types Γ e t)
 (side-condition (public? t))
 ---------------------------- promotion?
 (types Γ e (obliv t))]
```
- New typing forms for `public` and `obliv` wire types
```racket
[t ::=
     num
     bool
     (→ t t)
     ; ----------
     (<public> t)
     (<obliv> t)]
```
  - `(conceal (+ 1 2))` gets you `(<obliv> 3)`
  - `1` used in place of a wire can be public promoted to `(<public> 1)`
    > **Details:**
    > - Public predicate and public values
    > ```racket
    > (mux #t 2 3)
    > ; -promotion>
    > (mux (<public> #t) (<public> 2) (<public> 3))
    > ; -public-mux>
    > (<public> 2)
    > :
    > (<public> num)
    > ```
    > - Public predicate and `obliv` values
    > ```racket
    > (mux #f (conceal 2) (conceal 3))
    > ; -promotion>
    > (mux (<public> #f) (conceal 2) (conceal 3))
    > ; -conceals>
    > (mux (<public> #f) (<obliv> 2) (<obliv> 3))
    > ; -public-mux>
    > (<obliv> 3)
    > :
    > (<obliv> num)
    > ```
    > - `obliv` conditional predicate
    > ```racket
    > (mux (conceal x) 1 2)
    > ; -promotion>
    > (mux (<obliv> x) (<public> 1) (<public> 2))
    > :
    > (<obliv> num)
    > ```
  - `(<public> (→ t t))` is the promotion of any function
  - `(<obliv> (→ t t))` could be the result type of something like
    `(mux p (λ (x : num) x) (λ (x : num) 0))` since which function's value is
    used will be unknown to an observer
  - We may want the ability to send/recv `(<public> v)` at run-time