# Go Linear Typesystem

## Statement Judgment

Expression judgment: X; M; L $\vdash$ e: T | X'
Statement judgement: X; M; L $\vdash$ s | X'; M'; L'

------------------------------- Declaration
X;M;L |- var x T | X;M, x: T; T


X;M;L |- s1 | X';M';L'         X';M';L' |- s2 | X''; M''; L''
------------------------------------------------------------- Seq
X;M;L |- s1; s2 | X''; M''; L''


X;M;L |- e: M(x) | X'
---------------------------- Var-Assignment
X;M;L |- x = e | X';M;L


X;M;L |- e1: *T | X'    X';M;L |- e2: T | X''              
---------------------------- Pointer-Assignment
X;M;L |- *e1 = e2 | X'';M;L

## Stack

X: map[variables]stack[set[Locations]]

var x! int 
x = 5
// {x: [{x}]}

var x! int
var a *int = &mut x
var b *int = &mut (*a)
// {x: [b, a, x]}
var something = *a
// {x: [a, x]}

func foo() {
  var z = bar()
  // {x: [z, x]}
}

func bar() (*int) {
    var x int
    return &mut x 
}

func foo(b bool) {
  var x! int
  var y! int
  var z = bar(&x, &y, b)
  // ???
}

func foo2(b bool) {
  var x! int
  var y! int
  var z = *bar(&x, &y, b)
  // ???
}

func bar(x, y *int, b bool) (*int) {
    if b {
      return x
    } else {
      return y
    }
}

# Felix Design

## Notations

- `~=` is unequal.
- `(\x. e)` is a lambda function, e.g. `(\x. x + 1)` is function that increases the argument by one.
- Functions are applied without parentheses, e.g. `(\x. x + 1) 4` is 5.
- `f[e -> e']` is a function update that updates the function f at e with e'. For instance, `(\x. x + 1)[3 -> 3]` increases a number by one 1 except if the argument is 3, then it returns 3.
- Functions can use Haskell style pattern matching.
- `[]` is the empty list
- `X # Y` is a list with the element x as the head and the list y as the tail.
- `fold` is Haskell's fold function.

   fold f e [] = e
   fold f e (x # xs) = f (fold f xs) x 

- `map` applies a function to an option

  map none f = none
  map (some x) f = some (f x)

- `[ x | A x ]` is a list that contains all values that satisfy `A`, e.g. [ x | 10 > x && x > 5 ] is the list of all values between 10 and 5. Technically, the condition must be satisfied only by a finite set of values, but I am currently not rigorous about that.

- `adt` defines an adt, e.g. an int option is defined as `adt int_option = some_int int | none_int`

- `type` defines a type alias, i.e. we use it to give a more complex type a name, e.g. `type int_set = int => bool`, defines that the type `int_set` is a functions from ints to bools.

- `nat` is the type of natural numbers.

## Stack

/** Frame is a layer of the stack. Block is for permission conversions. */
adt Frame = Write Location | Read (Location => bool) | Block

/** We manage a "location stack" for each location */
type Stacks = Location => Frame list

### Interpretation

The locations in the domain of the stack represent disjoint locations. The locations in the location stacks represent potential pointers to these disjoint locations. A pointer p is in the location stack of a location l if access to l is necessary to justify accessing p. We distinguish between two kinds of accesses, namely read and write accesses, which are captured by two different entry kinds in the location stack.

Note that if a pointer is in multiple location stacks for different locations, then access to all of these locations is necessary to justify access to the pointer. This might be useful for joining stacks of different CFG-branches. Consider the following example:

x! := 5; y! := 4; var p *(int!)°
if some_complex_condition {
  p = &x
} else {
  p = &y
}
// (*)

At `(*)` the stacks could be $[\&x \rightarrow [\textsf{Write}\;p, \textsf{Write}\;\&x], \&y \rightarrow [\textsf{Write}\;p, \textsf{Write}\;\&y]$. Alternatively, we might want to over-approximate, resulting in the stacks $[\&x \rightarrow [\textsf{Write}\;\&x], \&y \rightarrow [\textsf{Write}\;\&y]$ to enforce that every pointer is at most in a single location stack.

The special stack layer `Block` might be a good approach to enable conversions with permission reasoning. Converting a pointer to permission reasoning requires write access and then blocks all necessary locations stacks. Alternatively, we might be able to just delete all locations stacks that are necessary to justify a conversion.

### Functions

/** Frame is a layer of the stack. Block is for permission conversions. */
adt Frame = Write Location | Read (Location => bool) | Block

/** We manage a "location stack" for each location */
type Stacks = Location => Frame list

/** checks whether a frame contains a location */
def has :: Frame => Location => bool 
  has (Write l) x = l == x
  has (Read ls) x = ls x
  has Block _ = false

/** find pointer with read access in a location stack.  
  * Returns how many layers have to be removed to get the frame with the pointer,
  * but returns none if the pointer is not found. 
  */
def read_floc :: Frame list => Location => nat option 
  read_floc [] x = none
  read_floc (Block # s) = none
  read_floc (f # s) x = if has f x then some 0 else map (read_floc s x) (\n. n+1)

/** find pointer with write access in a location stack.  
  * Returns how many layers have to be removed to get the frame with the pointer,
  * but returns none if the pointer is not found. 
  */
def write_floc :: Frame list => Location => nat option 
  write_floc [] x = none
  write_floc (Block # s) = none
  write_floc (f # s) x = if f == Write x then some 0 else map (write_floc s x) (\n. n+1)

/** find pointer with read access in all stacks.
  * Returns list with all found accesses.
  * A location-number pair indicates the location stack and layer where the access was found.
  */
def read_loc :: Stacks => Location => (Location x nat) list 
  loc s x = [ (l, n) | read_floc (s l) x = some n ]

/** find pointer with write access in all stacks.
  * Returns list with all found accesses.
  * A location-number pair indicates the stack and layer where the access was found.
  */
def write_loc :: Stacks => Location => (Location x nat) list 
  write_loc s x = [ (l, n) | write_floc (s l) x = some n ]

/** utility function that applies a stack transformation iteratively to all found accesses.
    Returns none if no access was found.
    This assumes that a pointer does not occur multiple times on the same location stack! */
def upd :: Stacks => (Location x nat) list => (Stacks => (Location x nat) => Stacks) => Stacks option
  upd s x f = if x == [] then none else some (fold f s x)

/** pop frames such that read access for the location is active 
    Returns none if read access is not possible. */
def read_activate :: Stacks => Location => Stacks option
  read_activate s x = upd s (read_loc s x) (\s' (l,n). s'[l -> drop n (s' l)])

/** pop frames such that write access for the location is active. 
    Returns none if write access is not possible. */  
def write_activate :: Stacks => Location => Stacks option
  write_activate s x = upd s (write_loc s x) (\s' (l,n). s'[l -> drop n (s' l)])

/** pushes a read frame to the location stack */
def read_push :: Frame list => Location => Frame list 
  read_push (Read ls # s) x = Read ls[x -> true] # s
  read_push s x = Read empty[x -> true] # s

/** pushes a write frame to the location stack */
def write_push :: Frame list => Location => Frame list 
  write_push s x = Write x # s

/** adds an immutable borrow from x to y in the stack. Returns none if this is not possible. */
def immutable_borrow_to :: Stacks => Location => Location => Stacks option 
  immutable_borrow_to s x y = upd s (read_loc s x) (\s' (l,n). s'[l -> read_push (drop n (s' l)) x])

/** adds a mutable borrow from x to y in the stack. Returns none if this is not possible. */
def mutable_borrow_to :: Stacks => Location => Location => Stacks option 
  mutable_borrow_to s x y = upd s (write_loc s x) (\s' (l,n). s'[l -> write_push (drop n (s' l)) x])

/** One idea to merge two stacks, takes the common tail of all location stacks */
def merge1 :: Stacks => Stacks => Stacks 
  merge1 s s' = \l. common_tail (s l) (s' l)
    
    where common_tail returns the common tail of two lists, e.g.
      common_tail [1,2,3,4,5] [9,4,5] = [4,5]
      common_tail [1,2,3] [3,2,1] = []

/** One idea to merge two stacks, takes the larger location stack if it exists,
    otherwise the common tail. */
def merge2 :: Stacks => Stacks => Stacks
  merge2 s s' = \l. let t = common_tail (s l) (s' l) in
                    if t == s l then s' l
                    else if t == s' l then s l
                    else t

## Old Expression Judgment

For simplicity, I write `C> e: T M` for the typing judgment $C \vdash e: T\;M$.

M ::= ° (exclusive) | @ (shared)
S: Var => T M

S> e: *T°            S> e: T@             S> e: T@           S(x) == T M
---------- Deref     ----------- Ref      --------- Read     ------------ Var
S> *e: T@            S> &e: *T°           S> e: T°           S> x: T M

S> e: St M     St.f: T
------------------------ Field
S> e.f: T M

S> e: [n]T M      S> e': int°
------------------------------ Index
S> e[e']: T M

S> e1: T1°   ... S> eN: TN°    f: (T1,...,Tn) => T
---------------------------------------------------- Call (includes bool/int/... operations)
S> f(e1,...,eN): T° 

Also subsumes the following:

S> e1: T1°   ... S> eN: TN°    Lit: (T1,...,Tn) => T // signature of the literal
----------------------------------------------------- Alloc Literal
S> &Lit{e1, ..., eN}: *T°

S> e1: T1°   ... S> eN: TN°    Lit: (T1,...,Tn) => T // signature of the literal
----------------------------------------------------- Literal
S> L{e1, ..., eN}: T°

S> e: T°
--------------- New
S> new(e): *T° 

## Old Statement Judgment

S> s1    S> s2 
---------------- Seq
S> s1;s2

S[x -> T M]> s 
------------------ Decl
S> var x M T in s

S> e: T M     S> e': T°
----------------------- Assignment
S> e = e'

S> e: bool°    S> s1    S> s2
------------------------------ If
S> if e { s1 } else { s2 }

S> e: bool°    S> s
-------------------- Loop
S> while e { s } 

## New Expression Judgment

Z ::= ° (exclusive) | @ (shared) | ! (mutable linear) | ? (immutable linear)
M ::= ° (exclusive) | @ (shared)
A ::= ! (mutable linear) | ? (immutable linear)

X: Stacks
S: Var => T Z
t: Location

The expression typing judgment is split into a reading expression typing judgment and a writing expression typing judgment. The writing judgment is used for the left-hand side of assignments. The reading judgment is used for everything else. The reading judgment has additionally a target `t`, indicating the target of the assignment, if the expression is read in the right-hand side of an assignment. If the expression is not read inside the right-hand side of an assignment, then the target is `_`. Writing judgments do not have a target. Syntactically, we distinguish writing and reading judgment based on whether the judgment has a target or not.

Rust types are interpreted as follows:

&T -> *(T?)°
&mut T -> *(T!)°

### Read Judgment

X;S;t> e: *(T Z)° | X'
--------------------- Deref
X;S;t> *e: T Z | X'

X;S;t> e: T@ | X'
---------------- Shared Read
X;S;t> e: T° | X'

X;S;t> e: T A | X'     read_activate X' &e == some X''
------------------------------------------------------ Linear Read 
X;S;t> e: T° | X'

// note &*x is equal to x. More such equations increase completeness, but we are also sound without them.
// these equations can also over approximate: e.g. &e.f = &e and &e[i] = &e

X;S;t> e: T@ | X'
----------------------- Shared Ref
X;S;t> &e: *(T@)° | X'

X;S;t> e: T A | X'     t ~= _  immutable_borrow_to X' &e t == some X''
--------------------------------------------------------------------- Linear Immutable Ref
X;S;t> &e: *(T?)° | X''

X;S;t> e: T A | X'     t ~= _    mutable_borrow_to X' &e t == some X''
---------------------------------------------------------------------- Linear Mutable Ref
X;S;t> &e: *(T!)° | X''

S(x) == T Z
---------------- Var
X;S;t> x: T Z | X

X;S;t> e: St Z | X'    St.f: T
------------------------------- Field
X;S;t> e.f: T Z | X'

X;S;t> e: [n]T Z | X'    X';S;t> e': int° | X''
------------------------------------------------- Index
X;S;t> e[e']: T Z | X''

X;S;t> e1: T1° | X1   ... X`N-1`;S;t> eN: TN° | XN   f: (T1,...,Tn) => T
---------------------------------------------------- Call (includes bool/int/... operations)
X;S;t> f(e1,...,eN): T° | ??? // what is the worst that can happen based on the signature?

### Write Judgment

X;S;_> e: *(T Z)° | X'
---------------------- Deref // note read judgment in premise
X;S> *e: T Z | X'

X;S> e: T@ | X'
---------------- Shared Write
X;S> e: T° | X'

X;S> e: T A | X'     write_activate X' &e == some X''
------------------------------------------------------ Linear Write 
X;S> e: T° | X'

S(x) == T Z
---------------- Var
X;S> x: T Z | X

X;S> e: St Z | X'    St.f: T
------------------------------- Field
X;S> e.f: T Z | X'

X;S> e: [n]T Z | X'    X';S;t> e': int° | X''
------------------------------------------------- Index
X;S> e[e']: T Z | X''

## New Statement Judgment

X;S> s1 | X'    X';S> s2 | X''
-------------------------- Seq
X;S> s1;s2 | X''

X;S[x -> T M]> s | X'
-------------------------- Decl
X;S> var x M T in s | X'

X[&x -> [Write &x]];S[x -> T!]> s | X'
--------------------------------------- Linear mutable Decl
X;S> var x! T in s | X'

X[&x -> [Read {&x}]];S[x -> T?]> s | X'
------------------------------------------ Linear immutable Decl
X;S> var x? T in s | X'

X;S> e: T° | X'    X';S;e> e': T° | X'' // what is the target, is "e" sufficient?
------------------------------------------- Assignment
X;S> e = e' | X''

X;S> e: bool° | X'    X';S> s1 | X''    X';S> s2 | X'''
-------------------------------------------------------- If
X;S> if e { s1 } else { s2 } | merge X'' X''' // merge both stacks, not yet defined

X;S> e: bool° | X'   X';S> s | X''
------------------------------------ Loop
X;S> while e { s } | merge X' X'' // unsure

## Example

### Example 1

y! := 5 // [&y -> [Write &y]]

_ = y // ok
y = ... // ok

p := &y

_ = *p // ok
*p = ... // ok

### Example 2

x@ := 5
y! := &x

_ = y // ok
*y = ... // ok
y = ... // ok


p := &y

_ = *p // ok
*p = ... // ok

S = [x: @int, y: *(@int)!, p: *(*(int@)!)°]



----------- Var
y: *(int@)!
----------- Linear Read // succeeds with stack [&y -> [Write &y]]
y: *(int@)°
------
_ = y



----------- Var
y: *(int@)!
----------- Linear Read // succeeds with stack [&y -> [Write &y]]
y: *(int@)°
----------- Deref
*y: int@
----------- Read // not the linear read
*y: int°
------
_ = *y


----------- Var
y: *(int@)!
----------- Linear Read // succeeds with stack [&y -> [Write &y]]
y: *(int@)°
----------- Deref
*y: int@
----------- Write // not the linear write
*y: int°
------
*y = _



----------- Var
y: *(int@)!
----------- Linear Write // succeeds with stack [&y -> [Write &y]]
y: *(int@)°
------
y = _



---------------- Var
p: *(*(int@)!)°
------------- Deref
*p: *(int@)!
------------- Linear Read // succeeds with stack [&y -> [Write p, Write &y]] since &*p = p
*p: *(int@)°
-------
_ = *p
// would fail with access to y after borrow as then stack does not contain p anymore



---------------- Var
p: *(*(int@)!)°
------------- Deref
*p: *(int@)!
------------- Linear Write // succeeds with stack [&y -> [Write p, Write &y]] since &*p = p
*p: *(int@)°
-------
*p = _

### Example 3

x := 5
p := &x
q := &p

can_take_reference(x)
can_take_reference(*e)
can_take_reference(e) ==> can_take_reference(e.f)
can_take_reference(e) ==> can_take_reference(e[e'])

## Problems

Currently, borrows do not yet work well. For instance, in `x! := 5; y! := 6; p := &x; p = &y`, the second assignment to p currently does not delete the borrow of x to p.